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.