set(auto).

assign(nest_penalty, 2).
assign(max_weight, 25).

assign(max_seconds, 3600).

set(x_proofs).

clauses(sos).

% lattice theory

x v y = y v x.
(x v y) v z = x v (y v z).
x ^ y = y ^ x.
(x ^ y) ^ z = x^ (y ^ z).
x ^ (x v y) = x.
x v (x ^ y) = x.

end_of_list.

clauses(hints).
% Arguments: probs1.out
% 207 hints were constructed from the clauses in 30 proofs.
% Length of proof is 43.  (138.19 + 1.20 seconds) H2.
% Length of proof is 34.  (354.19 + 2.86 seconds) H80.
% Length of proof is 40.  (0.38 + 0.00 seconds) H3.
% Length of proof is 11.  (0.00 + 0.01 seconds) H1.
% Length of proof is 35.  (527.00 + 4.14 seconds) H2.
% Length of proof is 40.  (0.42 + 0.01 seconds) H3.
% Length of proof is 31.  (50.47 + 0.54 seconds) H55.
% Length of proof is 25.  (2.72 + 0.02 seconds) H58.
% Length of proof is 14.  (0.03 + 0.00 seconds) H64.
% Length of proof is 29.  (33.03 + 0.41 seconds) H55.
% Length of proof is 35.  (7.54 + 0.17 seconds) H58.
% Length of proof is 35.  (0.06 + 0.00 seconds) H64.
% Length of proof is 33.  (0.06 + 0.00 seconds) H68.
% Length of proof is 43.  (8.75 + 0.17 seconds) H2.
% Length of proof is 26.  (0.89 + 0.00 seconds) H3.
% Length of proof is 42.  (8.45 + 0.14 seconds) H55.
% Length of proof is 18.  (0.22 + 0.00 seconds) H58.
% Length of proof is 32.  (0.13 + 0.00 seconds) H64.
% Length of proof is 22.  (0.13 + 0.00 seconds) H68.
% Length of proof is 11.  (0.01 + 0.00 seconds) H1.
% Length of proof is 43.  (18.38 + 0.25 seconds) H2.
% Length of proof is 37.  (0.53 + 0.02 seconds) H3.
% Length of proof is 37.  (13.62 + 0.21 seconds) H51.
% Length of proof is 31.  (4.62 + 0.08 seconds) H55.
% Length of proof is 41.  (13.69 + 0.19 seconds) H58.
% Length of proof is 17.  (0.09 + 0.00 seconds) H64.
% Length of proof is 11.  (0.00 + 0.00 seconds) H68.
% Length of proof is 42.  (2.02 + 0.05 seconds) H18.
% Length of proof is 39.  (115.20 + 1.13 seconds) H80.
% Length of proof is 42.  (542.50 + 4.23 seconds) H2.
(x ^ y) v (x ^ z) = x ^ ((x ^ y) v ((x ^ z) v (y ^ (x v z)))) # label(7).
A ^ (B v (A ^ C)) != A ^ (B v (C ^ ((A ^ (B v C)) v (B ^ C)))) # label(8).
x v y = y v x # label(9).
(x v y) v z = x v (y v z) # label(10).
x ^ y = y ^ x # label(11).
(x ^ y) ^ z = x ^ (y ^ z) # label(12).
x ^ (x v y) = x # label(13).
x v (x ^ y) = x # label(14).
x ^ ((x ^ y) v ((x ^ z) v (y ^ (x v z)))) = (x ^ y) v (x ^ z) # label(15).
A ^ (B v (C ^ ((B ^ C) v (A ^ (B v C))))) != A ^ (B v (A ^ C)) # label(16).
x v (y v z) = y v (x v z) # label(17).
x ^ (y ^ z) = y ^ (x ^ z) # label(18).
x ^ (y v x) = x # label(19).
(x v y) ^ (x v (y v z)) = x v y # label(20).
x ^ ((x v y) ^ z) = x ^ z # label(21).
x ^ (y ^ ((x ^ y) v z)) = x ^ y # label(22).
x v (y ^ x) = x # label(25).
x ^ ((x ^ y) v ((x ^ z) v (y ^ (z v x)))) = (x ^ y) v (x ^ z) # label(29).
x ^ (x ^ y) = x ^ y # label(33).
x ^ (y v (z v x)) = x # label(39).
x ^ ((y v x) ^ z) = x ^ z # label(40).
x v ((y ^ x) v z) = x v z # label(46).
x ^ (y ^ (z v x)) = y ^ x # label(63).
(x ^ y) v (x ^ (z ^ y)) = x ^ y # label(64).
(x ^ y) v (x ^ (z v y)) = x ^ (y v (x ^ (z v y))) # label(70).
(x v y) ^ (y v (x v z)) = y v x # label(84).
(x ^ y) v ((x v z) ^ y) = (x v z) ^ y # label(105).
x ^ (y ^ ((y ^ x) v z)) = x ^ y # label(115).
x ^ (y v (x ^ (z v y))) = x ^ (z v y) # label(176).
(x ^ y) v (x ^ (z v y)) = x ^ (z v y) # label(185).
x ^ ((x ^ y) v ((z ^ x) v (y ^ (z v x)))) = (x ^ y) v (x ^ z) # label(265).
(x ^ y) v (z ^ (y ^ x)) = x ^ y # label(438).
x v ((x v y) ^ (x v z)) = (x v y) ^ (x v z) # label(524).
x ^ ((y ^ x) v (y ^ z)) = x ^ y # label(569).
x ^ ((y ^ z) v (y ^ x)) = x ^ y # label(583).
x v ((y v x) ^ (y v z)) = x v y # label(1013).
x v ((y v (z ^ x)) ^ (y v u)) = x v y # label(1031).
(x ^ (y v z)) v (z ^ x) = x ^ (y v z) # label(1629).
x v (y ^ ((y ^ z) v (u ^ x))) = x v (y ^ z) # label(2457).
(x ^ y) v (z v (y ^ (u v x))) = z v (y ^ (u v x)) # label(3277).
(x ^ y) v (x ^ z) = x ^ ((z ^ x) v (y ^ (z v x))) # label(3345).
x v (y ^ ((x ^ y) v (z ^ (x v y)))) = x v (y ^ z) # label(9379).
$F # label(9380).
(A ^ B) v (A ^ C) != A ^ ((A ^ B) v (C ^ (A v (B ^ (A v C))))) # label(8).
A ^ ((A ^ B) v (C ^ (A v (B ^ (A v C))))) != (A ^ B) v (A ^ C) # label(16).
x ^ x = x # label(27).
x v x = x # label(28).
x ^ ((x ^ y) v ((x ^ z) v ((x v z) ^ y))) = (x ^ y) v (x ^ z) # label(32).
x ^ (y ^ x) = y ^ x # label(35).
x v (y v x) = y v x # label(38).
x v (y v (x ^ z)) = y v x # label(43).
x ^ (y ^ (z ^ x)) = y ^ (z ^ x) # label(57).
x ^ (y ^ (x v z)) = y ^ x # label(61).
x v (y v (z v x)) = y v (z v x) # label(66).
(x v y) ^ (z ^ y) = z ^ y # label(123).
(x ^ y) v (z v y) = z v y # label(138).
(x v y) ^ (z ^ (x v (y ^ u))) = z ^ (x v (y ^ u)) # label(253).
(x ^ y) v (z v ((x v u) ^ y)) = z v ((x v u) ^ y) # label(277).
(x ^ y) v (x ^ z) = x ^ ((x ^ z) v ((x v z) ^ y)) # label(288).
x ^ ((x ^ y) v ((x v y) ^ z)) = (x ^ y) v (x ^ z) # label(8569).
x ^ ((x ^ y) v (z ^ (x v (y ^ u)))) = (x ^ y) v (z ^ x) # label(9785).
x ^ (y v (z ^ (x v u))) = x ^ (y v (z ^ (x v (z ^ (y v u))))) # label(7).
A ^ (B v (A ^ C)) != A ^ (B v (C ^ (B v (A ^ (C v (A ^ B)))))) # label(8).
x ^ (y v (z ^ (x v (z ^ (y v u))))) = x ^ (y v (z ^ (x v u))) # label(15).
A ^ (B v (C ^ (B v (A ^ (C v (A ^ B)))))) != A ^ (B v (A ^ C)) # label(16).
x ^ (y v (z ^ (x v (z ^ y)))) = x ^ (y v (z ^ (x v (y ^ u)))) # label(32).
x v (x v y) = x v y # label(37).
x ^ (y v (z ^ (x v (z ^ y)))) = x ^ (y v (z ^ (x v y))) # label(40).
x ^ (y v (z ^ (x v (y ^ u)))) = x ^ (y v (z ^ (x v y))) # label(43).
A ^ (B v (C ^ (B v (A ^ (B v C))))) != A ^ (B v (A ^ C)) # label(44).
x ^ (y v (z ^ (x v (y v u)))) = x ^ (y v (z ^ (x v u))) # label(62).
(x v y) ^ ((z ^ x) v y) = (z ^ x) v y # label(142).
x ^ ((y ^ x) v (z ^ x)) = (y ^ x) v (z ^ x) # label(467).
x ^ ((x ^ y) v (z ^ y)) = x ^ y # label(563).
x v ((x v y) ^ (y v z)) = x v y # label(574).
x ^ ((y ^ z) v (x ^ z)) = x ^ z # label(607).
x v (y ^ (x v (z ^ y))) = x v (z ^ y) # label(766).
x ^ (y v (z ^ (y v x))) = x ^ (y v (z ^ x)) # label(1003).
x ^ (y v (z ^ (x v u))) = x ^ (y v ((x ^ z) v (z ^ u))) # label(7).
A ^ (B v (C ^ (A v D))) != A ^ (B v (C ^ (A v (C ^ D)))) # label(8).
x ^ (y v ((x ^ z) v (z ^ u))) = x ^ (y v (z ^ (x v u))) # label(15).
A ^ (B v (C ^ (A v (C ^ D)))) != A ^ (B v (C ^ (A v D))) # label(16).
x ^ (y v (z ^ (x v (z ^ u)))) = x ^ (y v (z ^ (x v u))) # label(59).
x v ((x ^ y) v z) = x v z # label(23).
x ^ ((x ^ y) v ((y ^ z) v u)) = x ^ (u v (y ^ (x v z))) # label(30).
x ^ (y v ((x ^ z) v (u ^ z))) = x ^ (y v (z ^ (x v u))) # label(32).
x ^ ((x ^ y) v (z v (y ^ u))) = x ^ (z v (y ^ (x v u))) # label(48).
x v (y ^ (z ^ x)) = x # label(54).
(x v y) ^ (y v x) = x v y # label(96).
x v (y v (z ^ (y v x))) = x v y # label(110).
x ^ (y ^ (z v (y ^ (x v u)))) = x ^ y # label(363).
x ^ ((x ^ y) v (z ^ (x v y))) = x ^ ((x ^ z) v (y ^ (x v z))) # label(608).
x v (y v (z ^ (y v (x ^ u)))) = x v y # label(706).
(x ^ y) v (x ^ (z v (y ^ (x v u)))) = x ^ (z v (y ^ (x v u))) # label(5115).
x v (y ^ ((y ^ x) v (z ^ (y v x)))) = x v (y ^ z) # label(9662).
x v (y ^ ((y ^ x) v (z ^ (x v y)))) = x v (y ^ z) # label(10269).
x ^ (y v ((z ^ x) v (z ^ u))) = x ^ (y v (z ^ (x v u))) # label(31).
x ^ ((x ^ y) v (y ^ z)) = x ^ (y ^ (x v z)) # label(41).
x v (y v (z ^ (x v y))) = x v y # label(53).
x v (y v (z ^ x)) = y v x # label(55).
x ^ ((x ^ y) v (y ^ z)) = y ^ x # label(70).
x ^ ((y ^ z) v (x ^ y)) = y ^ x # label(230).
x ^ ((y ^ z) v (x ^ z)) = z ^ x # label(407).
A ^ (B v (C ^ (B v (A ^ C)))) != A ^ (B v (A ^ C)) # label(636).
x ^ (y v z) = x ^ (y v (x ^ (z v (x ^ y)))) # label(7).
A v (B ^ (A v C)) != A v (B ^ (C v (A ^ (C v B)))) # label(8).
x ^ (y v (x ^ (z v (x ^ y)))) = x ^ (y v z) # label(15).
A v (B ^ (C v (A ^ (B v C)))) != A v (B ^ (A v C)) # label(16).
(x ^ y) v (x ^ (y ^ z)) = x ^ y # label(26).
x ^ (y v (x ^ ((x ^ y) v z))) = x ^ (y v z) # label(29).
(x v y) ^ ((x ^ z) v y) = (x ^ z) v y # label(113).
x ^ (y v (x ^ ((y ^ x) v z))) = x ^ (y v z) # label(281).
(x ^ y) v (z v (x ^ (y v u))) = z v (x ^ (y v u)) # label(309).
(x ^ (y v z)) v (x ^ ((y ^ u) v z)) = x ^ (y v z) # label(628).
x v (y ^ ((x ^ y) v z)) = x v (y ^ (x v z)) # label(4747).
x v (y ^ (z v (x ^ (y v u)))) = x v (y ^ (z v x)) # label(9109).
A ^ (B v C) != A ^ (B v ((A v B) ^ (C v (A ^ B)))) # label(8).
A ^ (B v ((A v B) ^ (C v (A ^ B)))) != A ^ (B v C) # label(16).
(x v y) ^ (x v (z v y)) = x v y # label(45).
x ^ (((x v y) ^ z) v (x ^ (u v (x ^ z)))) = x ^ (((x v y) ^ z) v u) # label(105).
x ^ ((y ^ (z ^ u)) v (x ^ u)) = x ^ u # label(188).
(x v y) ^ (z v (y v x)) = x v y # label(471).
(x v (y ^ z)) ^ (z v x) = x v (y ^ z) # label(1899).
x ^ ((y ^ (z v (u ^ v))) v (x ^ (v v z))) = x ^ (v v z) # label(3971).
x ^ (y v ((x v z) ^ (u v (x ^ y)))) = x ^ (y v u) # label(4023).
A ^ (B v C) != A ^ (B v (A ^ (C v (A ^ (B v (A ^ C)))))) # label(8).
A ^ (B v (A ^ (B v C))) != A ^ (B v C) # label(16).
x ^ (y v (x ^ (y v z))) = x ^ (y v z) # label(189).
x ^ (y v z) = (x ^ (z v (x ^ y))) v (x ^ (y v (x ^ z))) # label(7).
(x ^ (y v (x ^ z))) v (x ^ (z v (x ^ y))) = x ^ (z v y) # label(15).
(x ^ (y v (x ^ z))) v (x ^ ((x ^ y) v z)) = x ^ (y v z) # label(29).
x v (y ^ ((y ^ x) v z)) = x v (y ^ (x v z)) # label(289).
(x ^ (y v z)) v (x ^ (z v (x ^ (y v z)))) = x ^ (y v z) # label(75).
(x v y) ^ (x v (z ^ y)) = x v (z ^ y) # label(152).
x v (y ^ (z v (y ^ x))) = x v (y ^ (z v x)) # label(290).
(x ^ (y v z)) v (x ^ (y v (u ^ z))) = x ^ (y v z) # label(756).
x ^ (y v ((x v z) ^ (u v y))) = x ^ (u v y) # label(1378).
x ^ (y v ((x v z) ^ (u v (x ^ y)))) = x ^ (u v y) # label(6407).
A ^ (B v (A ^ (C v (A ^ (B v (A ^ C)))))) != A ^ (B v C) # label(16).
(x ^ (y v z)) v (x ^ (y v (x ^ (y v z)))) = x ^ (y v z) # label(282).
A ^ (B v C) != A ^ (B v (A ^ (C v (A ^ B)))) # label(8).
A ^ (B v (A ^ (C v (A ^ B)))) != A ^ (B v C) # label(16).
x ^ (y v (z ^ (y v u))) = x ^ (y v (z ^ (u v (x ^ y)))) # label(7).
x ^ (y v (z ^ (u v (x ^ y)))) = x ^ (y v (z ^ (y v u))) # label(15).
x ^ (y v (z ^ ((x ^ y) v u))) = x ^ (y v (z ^ (y v u))) # label(29).
x ^ (y v (z ^ (u v (x ^ y)))) = x ^ (y v (z ^ (u v y))) # label(30).
x ^ (y v ((z v (x ^ y)) ^ u)) = x ^ (y v (u ^ (y v z))) # label(32).
x ^ ((x ^ y) v (z ^ x)) = (x ^ y) v (z ^ x) # label(397).
x ^ (y v (x ^ (z v y))) = x ^ (y v z) # label(421).
x ^ ((y ^ x) v (z ^ y)) = x ^ y # label(439).
x ^ ((y ^ z) v (z ^ x)) = x ^ z # label(440).
x v (y ^ (x v (y ^ z))) = x v (y ^ z) # label(824).
x ^ ((y ^ z) v (y ^ (x v u))) = x ^ y # label(548).
x ^ (y v (z ^ (y v (x ^ (z v u))))) = x ^ (y v (z ^ x)) # label(1747).
x ^ (y v (z ^ (x v y))) = x ^ (y v (z ^ x)) # label(295).
A v (B ^ (C v (A ^ B))) != A v (B ^ (A v C)) # label(304).
x v (y ^ (z v (y ^ x))) = x v (y ^ (x v z)) # label(2482).
x v (y ^ (z v (x ^ y))) = x v (y ^ (x v z)) # label(6697).
A ^ (B v ((A v B) ^ (B v C))) != A ^ (B v C) # label(35).
(x ^ y) v ((z v x) ^ y) = (z v x) ^ y # label(116).
x v ((y v x) ^ (x v z)) = (y v x) ^ (x v z) # label(630).
A ^ (B v (A ^ (C v (A ^ (B v C))))) != A ^ (B v C) # label(35).
(x ^ y) v (x ^ (y v z)) = x ^ (y v z) # label(155).
x ^ (y v (z ^ (u v (x ^ (y v u))))) = x ^ (y v (z ^ (y v u))) # label(304).
x ^ (y v (z ^ (x v u))) = x ^ ((x ^ (y v (x ^ z))) v (z ^ u)) # label(7).
x ^ ((x ^ (y v (x ^ z))) v (z ^ u)) = x ^ (y v (z ^ (x v u))) # label(15).
x ^ ((x ^ ((x ^ y) v z)) v (y ^ u)) = x ^ (z v (y ^ (x v u))) # label(29).
x ^ ((x ^ (y v (z ^ x))) v (z ^ u)) = x ^ (y v (z ^ (x v u))) # label(31).
x ^ ((x ^ y) v (y ^ z)) = x ^ y # label(35).
x ^ (y v (x v z)) = x # label(40).
x ^ ((y ^ z) v (x ^ y)) = x ^ y # label(134).
x ^ (y v (x ^ ((x ^ y) v z))) = x ^ (z v y) # label(266).
A ^ (B v (C ^ (A v D))) != A ^ (B v ((A ^ C) v (C ^ D))) # label(8).
A ^ (B v ((A ^ C) v (C ^ D))) != A ^ (B v (C ^ (A v D))) # label(16).
x ^ ((x ^ (y v (x ^ z))) v (u ^ z)) = x ^ (y v (z ^ (x v u))) # label(32).
x ^ (y v (z ^ (x v (u ^ z)))) = x ^ (y v (z ^ (x v u))) # label(60).
x ^ (y ^ (z v ((x v u) ^ y))) = x ^ y # label(382).
(x v y) ^ (z ^ x) = z ^ x # label(109).
(x v y) ^ (x v (y ^ z)) = x v (y ^ z) # label(179).
x ^ ((x ^ (y v z)) v (u ^ y)) = x ^ (y v z) # label(242).
x ^ (y v (x ^ (z v (y ^ x)))) = x ^ (z v y) # label(430).
(x ^ (y v z)) v (x ^ (y v (z ^ u))) = x ^ (y v z) # label(940).
x v (y ^ (z v (x ^ y))) = x v (y ^ (z v x)) # label(5480).
x ^ (y v (x ^ (z v (x ^ y)))) = x ^ (z v y) # label(39).
x ^ (((x v y) ^ z) v (z ^ u)) = x ^ z # label(142).
x v ((y v x) ^ (z v y)) = x v y # label(1159).
x v ((y v z) ^ (z v x)) = x v z # label(1247).
(A ^ B) v (A ^ C) != A ^ ((A ^ B) v ((A ^ C) v (B ^ (A v C)))) # label(8).
(x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v y))) # label(15).
A ^ ((A ^ B) v ((A ^ C) v (B ^ (A v C)))) != (A ^ B) v (A ^ C) # label(16).
x ^ ((y ^ (x v z)) v (z ^ (x v y))) = (x ^ z) v (x ^ y) # label(29).
(x ^ y) v (y ^ (x ^ z)) = y ^ x # label(190).
x ^ ((x ^ y) v (x ^ z)) = (x ^ y) v (x ^ z) # label(255).
x ^ (y v ((z v y) ^ x)) = x ^ (z v y) # label(1089).
(x ^ (y v z)) v (y ^ x) = x ^ (y v z) # label(1524).
x ^ ((y ^ (x v z)) v ((x ^ y) v (x ^ z))) = (x ^ y) v (x ^ z) # label(2589).
(x ^ (y v z)) v ((y ^ x) v u) = (x ^ (y v z)) v u # label(3283).
(x ^ y) v (z v (y ^ (x v u))) = z v (y ^ (x v u)) # label(3284).
(x ^ y) v (x ^ z) = x ^ ((x ^ z) v (y ^ (x v z))) # label(3309).
A ^ ((A ^ C) v (B ^ (A v C))) != (A ^ B) v (A ^ C) # label(3310).
x v ((y v z) ^ (y v x)) = x v y # label(749).
x ^ (y v ((y v z) ^ x)) = x ^ (y v z) # label(1088).
(x ^ y) v (x ^ z) = x ^ ((x ^ y) v (z ^ (x v y))) # label(2557).
(x ^ y) v (x ^ z) = x ^ ((x ^ y) v (z ^ (x v (y ^ u)))) # label(9336).
x ^ ((y ^ (z v x)) v (z ^ (x v y))) = (x ^ z) v (x ^ y) # label(245).
(x ^ y) v (x ^ z) = x ^ ((x ^ y) v (z ^ (y v x))) # label(8875).
(x ^ y) v (x ^ z) = x ^ ((y ^ x) v (z ^ (y v x))) # label(9819).
end_of_list.