% This input file is for Otter 3.0.4. % % Theorem. Robbins algebras satisfy % % exists C exists D, n(C+D)=n(C). % % This is not a search. It is a proof-check. The steps of the % proof are included in the "hints" list to lead Otter directly % to the proof. % % The purpose of this job is to construct a proof object that can % be checked by the proof checker. op(500, xfy, +). set(build_proof_object). set(para_from). set(para_into). clear(para_from_right). clear(para_into_right). set(order_eq). % assign(pick_given_ratio, 1). assign(max_weight, 60). assign(max_mem, 16000). clear(print_kept). clear(print_new_demod). clear(print_back_demod). set(input_sos_first). % assign(max_proofs, 20). list(usable). x = x. x + y = y + x. % Commutativity end_of_list. list(demodulators). (x + y) + z = x + (y + z). % Associativity end_of_list. list(sos). (x + y) + z = x + (y + z). % Associativity n(n(n(x) + y) + n(x + y)) = y. % Robbins n(x + y) != n(x). % Denial of Winker condition end_of_list. list(passive). % n(n(n(A) + B) + n(A + B)) != B | $ans(s_3). % (wt=13) [] % n(n(n(A + B) + n(A) + B) + B) != n(A + B) | $ans(s_5). % (wt=18) [para(3,3)] % n(n(n(n(A) + B) + A + B) + B) != n(n(A) + B) | $ans(s_6). % (wt=19) [para(3,3)] % n(n(n(n(A) + B) + A + B + B) + n(n(A) + B)) != B | $ans(s_24). % (wt=21) [para(6,3)] % n(n(n(n(n(A) + B) + A + B + B) + n(n(A) + B) + C) + n(B + C)) != C | $ans(s_47). % (wt=29) [para(24,3)] % n(n(n(n(A) + B) + n(n(A) + B) + A + B + B) + B) != n(n(A) + B) | $ans(s_48). % (wt=27) [para(24,3)] % n(n(n(n(A) + B) + n(n(A) + B) + A + B + B + B) + n(n(A) + B)) != B | $ans(s_146). % (wt=29) [para(48,3)] % n(n(n(n(n(A) + B) + A + B + B) + n(n(A) + B) + n(B + C) + C) + C) != n(B + C) | $ans(s_250). % (wt=34) [para(47,3)] % n(n(n(n(n(n(A) + B) + A + B + B) + n(n(A) + B) + n(B + C) + C) + C + D) + n(n(B + C) + D)) != D | $ans(s_996). % (wt=42) [para(250,3)] % n(n(n(n(A) + A) + A + A + A) + A) != n(n(A) + A) | $ans(s_16379). % (wt=21) [para(5,996),demod([3])] % n(n(n(n(n(A) + A) + A + A + A) + A + B) + n(n(n(A) + A) + B)) != B | $ans(s_16387). % (wt=29) [para(16379,3)] % n(n(n(n(A) + A) + A + A + A + A) + n(n(A) + A)) != A | $ans(s_16388). % (wt=23) [para(16379,3)] % n(n(n(n(A) + A) + n(n(A) + A) + A + A + A + A) + A) != n(n(A) + A) | $ans(s_16393). % (wt=29) [para(16388,3)] % n(n(n(n(n(A) + A) + n(n(A) + A) + A + A + A + A) + A + B) + n(n(n(A) + A) + B)) != B | $ans(s_16426). % (wt=37) [para(16393,3)] % n(n(n(n(n(A) + A) + n(n(A) + A) + A + A + A + A) + n(n(n(A) + A) + A + A + A) + A) + A) != n(n(n(A) + A) + n(n(A) + A) + A + A + A + A) | $ans(s_17547). % (wt=60) [para(146,16387)] % n(n(n(A) + A) + n(n(A) + A) + A + A + A + A) != n(n(n(A) + A) + A + A + A) | $ans(s_17666). % (wt=33) [para(24,16426),demod([17547])] end_of_list. list(hints). n(n(n(x) + y) + n(x + y)) = y. % Robbins n(x + y) != n(x). % denial x + (y + z) = y + (x + z). % AC helper % The rest of the hints are from the Otter proofs of the % individual steps of the AC proof. % ss5.out % 2 [] x+y=y+x. % 4 [] n(n(n(x)+y)+n(x+y))=y. % 5 [] n(n(n(A+B)+n(A)+B)+B)!=n(A+B). n(n(n(x)+y)+n(y+x))=y. % 10 [para_into,4.1.1.1.2.1,2.1.1] n(n(x+y)+n(n(y)+x))=x. % 88 [para_into,10.1.1.1,2.1.1] n(n(n(x+y)+n(x)+y)+y)=n(x+y). % 433 [para_into,88.1.1.1.2,4.1.1] % 434 [binary,433.1,5.1] $F. % ss6.out % 2 [] x+y=y+x. % 4 [] n(n(n(x)+y)+n(x+y))=y. % 5 [] n(n(n(n(A)+B)+A+B)+B)!=n(n(A)+B). n(n(n(x)+y)+n(y+x))=y. % 10 [para_into,4.1.1.1.2.1,2.1.1] n(n(x+y)+n(n(x)+y))=y. % 12 [para_into,4.1.1.1,2.1.1] n(n(x+y)+n(n(y)+x))=x. % 88 [para_into,10.1.1.1,2.1.1] n(n(n(n(x)+y)+x+y)+y)=n(n(x)+y). % 427 [para_into,88.1.1.1.2,12.1.1] % 428 [binary,427.1,5.1] $F. % ss24.out % 1 [] (x+y)+z=x+y+z. % 2 [] x+y=y+x. % 4 [] n(n(n(x)+y)+n(x+y))=y. % 5 [] n(n(n(n(x)+y)+x+y)+y)=n(n(x)+y). % 6 [] n(n(n(n(A)+B)+A+B+B)+n(n(A)+B))!=B. n(n(x+y)+n(n(x)+y))=y. % 13 [para_into,4.1.1.1,2.1.1] n(n(n(n(x)+y)+x+y+y)+n(n(x)+y))=y. % 151 [para_into,13.1.1.1.2,5.1.1,demod,1,1] % 152 [binary,151.1,6.1] $F. % ss47.out % 1 [] (x+y)+z=x+y+z. % 2 [] x+y=y+x. % 4 [] n(n(n(x)+y)+n(x+y))=y. % 5 [] n(n(n(n(x)+y)+x+y+y)+n(n(x)+y))=y. % 6 [] n(n(n(n(n(A)+B)+A+B+B)+n(n(A)+B)+C)+n(B+C))!=C. n(n(x+y)+n(n(x)+y))=y. % 13 [para_into,4.1.1.1,2.1.1] n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+z)+n(y+z))=z. % 156 [para_into,13.1.1.1.2.1.1,5.1.1,demod,1] % 157 [binary,156.1,6.1] $F. % ss48.out % 2 [] x+y=y+x. % 4 [] n(n(n(x)+y)+n(x+y))=y. % 5 [] n(n(n(n(x)+y)+x+y+y)+n(n(x)+y))=y. % 6 [] n(n(n(n(A)+B)+n(n(A)+B)+A+B+B)+B)!=n(n(A)+B). n(n(n(x)+y)+n(y+x))=y. % 11 [para_into,4.1.1.1.2.1,2.1.1] n(n(x+y)+n(n(y)+x))=x. % 98 [para_into,11.1.1.1,2.1.1] n(n(n(n(x)+y)+n(n(x)+y)+x+y+y)+y)=n(n(x)+y). % 401 [para_into,98.1.1.1.2,5.1.1] % 402 [binary,401.1,6.1] $F. % ss146.out % 1 [] (x+y)+z=x+y+z. % 2 [] x+y=y+x. % 4 [] n(n(n(x)+y)+n(x+y))=y. % 5 [] n(n(n(n(x)+y)+n(n(x)+y)+x+y+y)+y)=n(n(x)+y). % 6 [] n(n(n(n(A)+B)+n(n(A)+B)+A+B+B+B)+n(n(A)+B))!=B. n(n(x+y)+n(n(x)+y))=y. % 13 [para_into,4.1.1.1,2.1.1] n(n(n(n(x)+y)+n(n(x)+y)+x+y+y+y)+n(n(x)+y))=y. % 154 [para_into,13.1.1.1.2,5.1.1,demod,1,1,1,1] % 155 [binary,154.1,6.1] $F. % sss250.out % 1 [] (x+y)+z=x+y+z. % 2 [] x+y=y+x. % 4 [] n(n(n(x)+y)+n(x+y))=y. % 5 [] n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+z)+n(y+z))=z. % 6 [] n(n(n(n(n(A)+B)+A+B+B)+n(n(A)+B)+n(B+C)+C)+C)!=n(B+C). n(n(x+y)+n(n(x)+y))=y. % 16 [para_into,4.1.1.1,2.1.1] n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+z+n(y+z))+z)=n(y+z). % 35 [para_into,16.1.1.1.2,5.1.1,demod,1,1] n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+n(y+z)+z)+z)=n(y+z). % 45 [para_into,35.1.1.1.1.1.2.2,2.1.1] % 46 [binary,45.1,6.1] $F. % ss996.out % 1 [] (x+y)+z=x+y+z. % 2 [] x+y=y+x. % 4 [] n(n(n(x)+y)+n(x+y))=y. % 5 [] n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+n(y+z)+z)+z)=n(y+z). % 6 [] n(n(n(n(n(n(A)+B)+A+B+B)+n(n(A)+B)+n(B+C)+C)+C+D)+n(n(B+C)+D))!=D. n(n(x+y)+n(n(x)+y))=y. % 13 [para_into,4.1.1.1,2.1.1] n(n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+n(y+z)+z)+z+u)+n(n(y+z)+u))=u. % 152 [para_into,13.1.1.1.2.1.1,5.1.1,demod,1] % 153 [binary,152.1,6.1] $F. % sss16379.out % 1 [] (x+y)+z=x+y+z. % 3 [] x+y=y+x. % 5 [] x+y+z=y+x+z. % 6 [] n(n(n(x)+y)+n(x+y))=y. % 7 [] n(n(n(x+y)+n(x)+y)+y)=n(x+y). % 8 [] n(n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+n(y+z)+z)+z+u)+n(n(y+z)+u))=u. % 9 [] n(n(n(n(A)+A)+A+A+A)+A)!=n(n(A)+A). n(n(x+y)+n(n(x)+y))=y. % 26 [para_into,6.1.1.1,3.1.1] n(n(n(x+y+z)+y+n(x)+z)+y+z)=n(x+y+z). % 34 [para_into,7.1.1.1.1.1.2,5.1.1] n(n(n(x+y+z)+y+n(x)+z)+z+y)=n(x+y+z). % 122 [para_into,34.1.1.1.2,3.1.1] n(n(n(x+y+z)+x+n(z)+y)+y+x)=n(z+x+y). % 138 [para_into,122.1.1.1.1.1.1.1,3.1.1,demod,1] n(n(x+x+n(n(x)+x)+x)+n(n(x+x)+n(n(x)+x)))=n(n(x)+x). % 186 [para_from,138.1.1,8.1.1.1.1,demod,1] n(n(x+x+n(n(x)+x)+x)+x)=n(n(x)+x). % 202 [para_into,186.1.1.1.2,26.1.1] n(n(x+n(n(x)+x)+x+x)+x)=n(n(x)+x). % 214 [para_into,202.1.1.1.1.1.2,5.1.1] n(n(n(n(x)+x)+x+x+x)+x)=n(n(x)+x). % 233 [para_into,214.1.1.1.1.1,5.1.1] % 234 [binary,233.1,9.1] $F. % ss16387.out % 1 [] (x+y)+z=x+y+z. % 2 [] x+y=y+x. % 4 [] n(n(n(x)+y)+n(x+y))=y. % 5 [] n(n(n(n(x)+x)+x+x+x)+x)=n(n(x)+x). % 6 [] n(n(n(n(n(A)+A)+A+A+A)+A+B)+n(n(n(A)+A)+B))!=B. n(n(x+y)+n(n(x)+y))=y. % 13 [para_into,4.1.1.1,2.1.1] n(n(n(n(n(x)+x)+x+x+x)+x+y)+n(n(n(x)+x)+y))=y. % 133 [para_into,13.1.1.1.2.1.1,5.1.1,demod,1] % 134 [binary,133.1,6.1] $F. % ss16388.out % 1 [] (x+y)+z=x+y+z. % 2 [] x+y=y+x. % 4 [] n(n(n(x)+y)+n(x+y))=y. % 5 [] n(n(n(n(x)+x)+x+x+x)+x)=n(n(x)+x). % 6 [] n(n(n(n(A)+A)+A+A+A+A)+n(n(A)+A))!=A. n(n(x+y)+n(n(x)+y))=y. % 13 [para_into,4.1.1.1,2.1.1] n(n(n(n(x)+x)+x+x+x+x)+n(n(x)+x))=x. % 139 [para_into,13.1.1.1.2,5.1.1,demod,1,1,1] % 140 [binary,139.1,6.1] $F. % ss16393.out % 2 [] x+y=y+x. % 4 [] n(n(n(x)+y)+n(x+y))=y. % 5 [] n(n(n(n(x)+x)+x+x+x+x)+n(n(x)+x))=x. % 6 [] n(n(n(n(A)+A)+n(n(A)+A)+A+A+A+A)+A)!=n(n(A)+A). n(n(n(x)+y)+n(y+x))=y. % 11 [para_into,4.1.1.1.2.1,2.1.1] n(n(x+y)+n(n(y)+x))=x. % 82 [para_into,11.1.1.1,2.1.1] n(n(n(n(x)+x)+n(n(x)+x)+x+x+x+x)+x)=n(n(x)+x). % 377 [para_into,82.1.1.1.2,5.1.1] % 378 [binary,377.1,6.1] $F. % ss16426.out % 1 [] (x+y)+z=x+y+z. % 2 [] x+y=y+x. % 4 [] n(n(n(x)+y)+n(x+y))=y. % 5 [] n(n(n(n(x)+x)+n(n(x)+x)+x+x+x+x)+x)=n(n(x)+x). % 6 [] n(n(n(n(n(A)+A)+n(n(A)+A)+A+A+A+A)+A+B)+n(n(n(A)+A)+B))!=B. n(n(x+y)+n(n(x)+y))=y. % 13 [para_into,4.1.1.1,2.1.1] n(n(n(n(n(x)+x)+n(n(x)+x)+x+x+x+x)+x+y)+n(n(n(x)+x)+y))=y. % 132 [para_into,13.1.1.1.2.1.1,5.1.1,demod,1] % 133 [binary,132.1,6.1] $F. % sss17547.out % 1 [] (x+y)+z=x+y+z. % 2 [] x+y=y+x. % 4 [] n(n(n(n(x)+y)+n(n(x)+y)+x+y+y+y)+n(n(x)+y))=y. % 5 [] n(n(n(n(n(x)+x)+x+x+x)+x+y)+n(n(n(x)+x)+y))=y. % 6 [] n(n(n(n(n(A)+A)+n(n(A)+A)+A+A+A+A)+n(n(n(A)+A)+A+A+A)+A)+A)!=n(n(n(A)+A)+n(n(A)+A)+A+A+A+A). n(n(n(x)+y)+n(n(n(x)+y)+n(n(x)+y)+x+y+y+y))=y. % 18 [para_into,4.1.1.1,2.1.1] n(n(n(n(n(x)+x)+x+x+x)+x+n(n(n(x)+x)+n(n(x)+x)+x+x+x+x))+x)=n(n(n(x)+x)+n(n(x)+x)+x+x+x+x). % 35 [para_from,18.1.1,5.1.1.1.2] n(n(x+n(n(n(x)+x)+n(n(x)+x)+x+x+x+x)+n(n(n(x)+x)+x+x+x))+x)=n(n(n(x)+x)+n(n(x)+x)+x+x+x+x). % 42 [para_into,35.1.1.1.1.1,2.1.1,demod,1] n(n(n(n(n(x)+x)+n(n(x)+x)+x+x+x+x)+n(n(n(x)+x)+x+x+x)+x)+x)=n(n(n(x)+x)+n(n(x)+x)+x+x+x+x). % 50 [para_into,42.1.1.1.1.1,2.1.1,demod,1] % 51 [binary,50.1,6.1] $F. % sss17666.out % 2 [] x+y=y+x. % 4 [] n(n(n(n(x)+y)+x+y+y)+n(n(x)+y))=y. % 5 [] n(n(n(n(n(x)+x)+n(n(x)+x)+x+x+x+x)+x+y)+n(n(n(x)+x)+y))=y. % 6 [] n(n(n(n(n(x)+x)+n(n(x)+x)+x+x+x+x)+n(n(n(x)+x)+x+x+x)+x)+x)=n(n(n(x)+x)+n(n(x)+x)+x+x+x+x). % 7 [] n(n(n(A)+A)+n(n(A)+A)+A+A+A+A)!=n(n(n(A)+A)+A+A+A). n(n(n(x)+y)+n(n(n(x)+y)+x+y+y))=y. % 22 [para_into,4.1.1.1,2.1.1] n(n(n(n(n(x)+x)+n(n(x)+x)+x+x+x+x)+x+n(n(n(x)+x)+x+x+x))+x)=n(n(n(x)+x)+n(n(x)+x)+x+x+x+x). % 38 [para_into,6.1.1.1.1.1.2,2.1.1] n(n(n(n(n(x)+x)+n(n(x)+x)+x+x+x+x)+x+n(n(n(x)+x)+x+x+x))+x)=n(n(n(x)+x)+x+x+x). % 53 [para_from,22.1.1,5.1.1.1.2] n(n(n(x)+x)+n(n(x)+x)+x+x+x+x)=n(n(n(x)+x)+x+x+x). % 71 [para_into,53.1.1,38.1.1] % 72 [binary,71.1,7.1] $F. % ss_last.out % 2 [] x+y=y+x. % 3 [] (x+y)+z=x+y+z. % 5 [] n(x+y)!=n(x). % 6 [] n(n(n(x)+x)+n(n(x)+x)+x+x+x+x)=n(n(n(x)+x)+x+x+x). n(x+y)!=n(y). % 9 [para_into,5.1.1.1,2.1.1] n(x+y+z)!=n(z). % 10 [para_into,9.1.1.1,3.1.1] n(n(x+n(x))+n(n(x)+x)+x+x+x+x)=n(n(n(x)+x)+x+x+x). % 11 [para_into,6.1.1.1.1.1,2.1.1] n(x+y+z)!=n(y). % 21 [para_into,10.1.1.1.2,2.1.1] n(x+y+z+u)!=n(y+z). % 28 [para_into,21.1.1.1.2,3.1.1] n(n(n(x)+x)+x+x+x)=n(n(x+n(x))+n(x+n(x))+x+x+x+x). % 32 [para_into,11.1.1.1.2.1.1,2.1.1,flip.1] n(x+y+z+u)!=n(y+u). % 98 [para_into,28.1.1.1.2.2,2.1.1] n(n(x+n(x))+n(x+n(x))+x+x+x+x)=n(n(x+n(x))+x+x+x). % 119 [para_into,32.1.1.1.1.1,2.1.1,flip.1] % 121 [binary,119.1,98.1] $F. end_of_list. % END OF HINTS assign(bsub_hint_wt, 0).