Started looper Fri Aug 5 11:16:45 CDT 2005 on theorem.mcs.anl.gov. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% set(auto). assign(constant_weight, 0). assign(max_seconds, 120). 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. % denials (pick one) A v B = A v C. A v B != A v (B ^ C). % denial of SDv % A v B = A v C. (A ^ B) v (A ^ C) != A ^ (B v C). % denial of CDv % A v B = A v C. A ^ ((A ^ B) v C) != (A ^ B) v (A ^ C). % denial of CMv % A ^ B = A ^ C. A ^ B != A ^ (B v C). % denial of SD^ % A ^ B = A ^ C. (A v B) ^ (A v C) != A v (B ^ C). % denial of CD^ % A ^ B = A ^ C. A v ((A v B) ^ C) != (A v B) ^ (A v C). % denial of CM^ end_of_list. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ----------------------------------------------------- x v (y ^ (x v (z ^ (x v y)))) = x v (y ^ z) # label(H68_dual). % Problem 1 -------- Proof 1 -------- (0.00 + 0.00 seconds) -------- PROOF -------- Length of proof is 11. Maximum clause weight is 17. 7 A v B = A v C. [input] 8 A v B != A v (B ^ C). [input] 10 x v y = y v x. [input] 14 x ^ (x v y) = x. [input] 16 A v C = A v B. [copy 7 flip a] 17 A v (B ^ C) != A v B. [copy 8 flip a] 18 x v (y ^ (x v (z ^ (x v y)))) = x v (y ^ z) # label(H68_dual). [input] 21 x ^ (y v x) = x. [para (10 (a 1) 14 (a 1 2))] 58 C ^ (A v B) = C. [para (16 (a 1) 21 (a 1 2))] 63 A v (B ^ C) = A v B. [para (58 (a 1) 18 (a 1 2 2 2)) demod (16 21) flip a] 64 $F. [resolve (63 a 17 a)] -------- end of proof ------- Given=14. Generated=194. Kept=54. Proofs=1. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. Process 27973 exit (max_proofs) Fri Aug 5 11:16:45 2005 label(H68_dual). Proved 0.00 seconds PROBLEM 1 ----------------------------------------------------- x ^ (y v (z ^ (x v (z ^ (y v u))))) = x ^ (y v (z ^ (x v u))) # label(H50). % Problem 2 -------- Proof 1 -------- (0.65 + 0.01 seconds) -------- PROOF -------- Length of proof is 19. Maximum clause weight is 23. 7 A v B = A v C. [input] 8 A v B != A v (B ^ C). [input] 10 x v y = y v x. [input] 11 (x v y) v z = x v (y v z). [input] 12 x ^ y = y ^ x. [input] 14 x ^ (x v y) = x. [input] 15 x v (x ^ y) = x. [input] 16 A v C = A v B. [copy 7 flip a] 17 A v (B ^ C) != A v B. [copy 8 flip a] 18 x ^ (y v (z ^ (x v (z ^ (y v u))))) = x ^ (y v (z ^ (x v u))) # label(H50). [input] 19 x v (y v z) = y v (x v z). [para (10 (a 1) 11 (a 1 1)) demod (11)] 21 x ^ (y v x) = x. [para (10 (a 1) 14 (a 1 2))] 27 x v (y ^ x) = x. [para (12 (a 1) 15 (a 1 2))] 30 x v x = x. [para (14 (a 1) 15 (a 1 2))] 62 C ^ (A v B) = C. [para (16 (a 1) 21 (a 1 2))] 66 x ^ (A v (C ^ (x v B))) = x ^ (A v B). [para (62 (a 1) 18 (a 1 2 2 2 2)) demod (21 16) flip a] 1780 B ^ (A v (B ^ C)) = B. [para (30 (a 1) 66 (a 1 2 2 2)) demod (12 21)] 1797 A v (B ^ C) = A v B. [para (1780 (a 1) 27 (a 1 2)) demod (10 19 15) flip a] 1798 $F. [resolve (1797 a 17 a)] -------- end of proof ------- Given=142. Generated=12231. Kept=1788. Proofs=1. User_CPU=0.65, System_CPU=0.01, Wall_clock=1. Process 27976 exit (max_proofs) Fri Aug 5 11:16:46 2005 label(H50). Proved 0.65 seconds PROBLEM 2 ----------------------------------------------------- x ^ (y v ((x ^ z) v (z ^ u))) = x ^ (y v (z ^ (x v u))) # label(H51). % Problem 3 -------- Proof 1 -------- (0.83 + 0.02 seconds) -------- PROOF -------- Length of proof is 20. Maximum clause weight is 21. 7 A v B = A v C. [input] 8 A v B != A v (B ^ C). [input] 10 x v y = y v x. [input] 11 (x v y) v z = x v (y v z). [input] 12 x ^ y = y ^ x. [input] 14 x ^ (x v y) = x. [input] 15 x v (x ^ y) = x. [input] 16 A v C = A v B. [copy 7 flip a] 17 A v (B ^ C) != A v B. [copy 8 flip a] 18 x ^ (y v ((x ^ z) v (z ^ u))) = x ^ (y v (z ^ (x v u))) # label(H51). [input] 19 x v (y v z) = y v (x v z). [para (10 (a 1) 11 (a 1 1)) demod (11)] 21 x ^ (y v x) = x. [para (10 (a 1) 14 (a 1 2))] 25 x v ((x ^ y) v z) = x v z. [para (15 (a 1) 11 (a 1 1)) flip a] 27 x v (y ^ x) = x. [para (12 (a 1) 15 (a 1 2))] 35 x ^ (y v ((x ^ z) v (z ^ u))) = x ^ (y v (z ^ (u v x))). [para (10 (a 1) 18 (a 2 2 2 2))] 60 C ^ (A v B) = C. [para (16 (a 1) 21 (a 1 2))] 269 B ^ (x v ((A ^ C) v (B ^ C))) = B ^ (x v C). [para (60 (a 1) 35 (a 2 2 2)) demod (12 10)] 2233 B ^ (A v (B ^ C)) = B. [para (16 (a 1) 269 (a 2 2)) demod (25 21)] 2249 A v (B ^ C) = A v B. [para (2233 (a 1) 27 (a 1 2)) demod (10 19 15) flip a] 2250 $F. [resolve (2249 a 17 a)] -------- end of proof ------- Given=188. Generated=18622. Kept=2240. Proofs=1. User_CPU=0.83, System_CPU=0.02, Wall_clock=1. Process 27979 exit (max_proofs) Fri Aug 5 11:16:47 2005 label(H51). Proved 0.83 seconds PROBLEM 3 ----------------------------------------------------- x ^ (y v (z ^ (u v (x ^ y)))) = x ^ (y v (z ^ (y v u))) # label(H76). % Problem 4 -------- Proof 1 -------- (0.12 + 0.00 seconds) -------- PROOF -------- Length of proof is 18. Maximum clause weight is 21. 7 A v B = A v C. [input] 8 A v B != A v (B ^ C). [input] 10 x v y = y v x. [input] 11 (x v y) v z = x v (y v z). [input] 12 x ^ y = y ^ x. [input] 14 x ^ (x v y) = x. [input] 15 x v (x ^ y) = x. [input] 16 A v C = A v B. [copy 7 flip a] 17 A v (B ^ C) != A v B. [copy 8 flip a] 18 x ^ (y v (z ^ (u v (x ^ y)))) = x ^ (y v (z ^ (y v u))) # label(H76). [input] 19 x v (y v z) = y v (x v z). [para (10 (a 1) 11 (a 1 1)) demod (11)] 21 x ^ (y v x) = x. [para (10 (a 1) 14 (a 1 2))] 27 x v (y ^ x) = x. [para (12 (a 1) 15 (a 1 2))] 42 x ^ (y v (z ^ (y v x))) = x ^ (y v (z ^ x)). [para (15 (a 1) 18 (a 1 2 2 2)) flip a] 61 C ^ (A v B) = C. [para (16 (a 1) 21 (a 1 2))] 469 B ^ (A v (B ^ C)) = B. [para (61 (a 1) 42 (a 1 2 2)) demod (16 21 12) flip a] 510 A v (B ^ C) = A v B. [para (469 (a 1) 27 (a 1 2)) demod (10 19 15) flip a] 511 $F. [resolve (510 a 17 a)] -------- end of proof ------- Given=67. Generated=3228. Kept=501. Proofs=1. User_CPU=0.12, System_CPU=0.00, Wall_clock=0. Process 27982 exit (max_proofs) Fri Aug 5 11:16:47 2005 label(H76). Proved 0.12 seconds PROBLEM 4 ----------------------------------------------------- x ^ ((x ^ (y v (x ^ z))) v (z ^ u)) = x ^ (y v (z ^ (x v u))) # label(H79). % Problem 5 -------- Proof 1 -------- (48.42 + 0.18 seconds) -------- PROOF -------- Length of proof is 43. Maximum clause weight is 33. 7 A v B = A v C. [input] 8 A v B != A v (B ^ C). [input] 10 x v y = y v x. [input] 11 (x v y) v z = x v (y v z). [input] 12 x ^ y = y ^ x. [input] 13 (x ^ y) ^ z = x ^ (y ^ z). [input] 14 x ^ (x v y) = x. [input] 15 x v (x ^ y) = x. [input] 16 A v C = A v B. [copy 7 flip a] 17 A v (B ^ C) != A v B. [copy 8 flip a] 18 x ^ ((x ^ (y v (x ^ z))) v (z ^ u)) = x ^ (y v (z ^ (x v u))) # label(H79). [input] 19 x v (y v z) = y v (x v z). [para (10 (a 1) 11 (a 1 1)) demod (11)] 20 x ^ (y ^ z) = y ^ (x ^ z). [para (12 (a 1) 13 (a 1 1)) demod (13)] 21 x ^ (y v x) = x. [para (10 (a 1) 14 (a 1 2))] 25 x v ((x ^ y) v z) = x v z. [para (15 (a 1) 11 (a 1 1)) flip a] 27 x v (y ^ x) = x. [para (12 (a 1) 15 (a 1 2))] 29 x ^ x = x. [para (15 (a 1) 14 (a 1 2))] 30 x v x = x. [para (14 (a 1) 15 (a 1 2))] 32 C v (x v A) = x v (A v B). [para (16 (a 1) 11 (a 2 2)) demod (10)] 34 x ^ ((y ^ z) v (x ^ (u v (x ^ y)))) = x ^ (u v (y ^ (x v z))). [para (10 (a 1) 18 (a 1 2))] 50 x ^ (y ^ x) = y ^ x. [para (29 (a 1) 13 (a 2 2)) demod (12)] 54 x v (y v (x ^ z)) = y v x. [para (15 (a 1) 19 (a 1 2)) flip a] 64 C ^ (A v B) = C. [para (16 (a 1) 21 (a 1 2))] 72 x v ((y ^ x) v z) = x v z. [para (27 (a 1) 11 (a 1 1)) flip a] 73 x v (y v (z ^ (x v y))) = x v y. [para (27 (a 1) 11 (a 1)) flip a] 75 (x ^ (y v (z ^ (x v u)))) v ((x ^ (y v (x ^ z))) v (z ^ u)) = (x ^ (y v (x ^ z))) v (z ^ u). [para (18 (a 1) 27 (a 1 2)) demod (10)] 76 x v (y v (z ^ x)) = y v x. [para (27 (a 1) 19 (a 1 2)) flip a] 84 C ^ (x ^ (A v B)) = x ^ C. [para (64 (a 1) 20 (a 1 2)) flip a] 122 C v (x v (y v A)) = A v (B v (x v y)). [para (11 (a 1) 32 (a 1 2)) demod (19 10)] 172 (x ^ C) v (x ^ (A v B)) = x ^ (A v B). [para (84 (a 1) 27 (a 1 2)) demod (10)] 365 x ^ ((y ^ z) v (x ^ (u v (x ^ y)))) = x ^ (u v (y ^ (z v x))). [para (10 (a 1) 34 (a 2 2 2 2))] 377 x ^ ((y ^ z) v (x ^ y)) = x ^ y. [para (15 (a 1) 34 (a 2 2)) demod (27)] 387 x v ((y ^ (z v u)) v (z ^ ((y ^ u) v (z ^ (x v (z ^ y)))))) = x v (y ^ (z v u)). [para (34 (a 2) 27 (a 1 2)) demod (11)] 3266 (x ^ C) v ((x ^ (A v B)) v y) = (x ^ (A v B)) v y. [para (84 (a 1) 72 (a 1 2 1)) demod (19)] 17644 (x ^ (A v B)) v (A ^ x) = x ^ (A v B). [para (172 (a 1) 387 (a 2)) demod (377 377 3266)] 18103 A v ((x v A) ^ (A v B)) = (x v A) ^ (A v B). [para (21 (a 1) 17644 (a 1 2)) demod (10)] 19066 C v ((x v A) ^ (A v B)) = A v B. [para (18103 (a 1) 122 (a 2 2 2)) demod (10 18103 18103 73)] 19088 B ^ (A v (B ^ (C v (B ^ (x v A))))) = B. [para (19066 (a 1) 365 (a 2 2)) demod (12 21 21)] 19174 A v (B ^ (C v (B ^ (x v A)))) = A v B. [para (19088 (a 1) 27 (a 1 2)) demod (10 19 15) flip a] 19196 A v (B ^ (C v (A ^ B))) = A v B. [para (30 (a 1) 19174 (a 1 2 2 2 2)) demod (12)] 19213 (A ^ B) v (C ^ (A v (B ^ C))) = C v (A ^ B). [para (19196 (a 1) 75 (a 1 1 2)) demod (64 12 50 10 54 10 12 50 10) flip a] 19241 A v (B ^ C) = A v B. [para (19213 (a 1) 76 (a 1 2)) demod (19 10 19 25 19 27 16 19 25) flip a] 19242 $F. [resolve (19241 a 17 a)] -------- end of proof ------- Given=1077. Generated=580285. Kept=19232. Proofs=1. User_CPU=48.42, System_CPU=0.18, Wall_clock=50. Process 27985 exit (max_proofs) Fri Aug 5 11:17:37 2005 label(H79). Proved 48.42 seconds PROBLEM 5 Finished looper Fri Aug 5 11:17:37 CDT 2005 on theorem.mcs.anl.gov.