============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13068 was started by mccune on cleo.thornwood, Mon Jun 19 16:41:01 2006 The command was "/home/mccune/bin/prover9 -f RBA-2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file RBA-2.in assign(new_constants,1). clauses(sos). x + y = y + x. (x + y) + z = x + (y + z). ((x + y) ' + (x + y ') ') ' = x # label(Robbins). c + c = c. end_of_list. set(restrict_denials). clauses(goals). (x + y ') ' + (x ' + y ') ' = y # answer(Huntington). end_of_list. ============================== end of input ========================== ============================== PROCESS GOALS ========================= % Each goal clause was negated; the result (to be placed in sos): clauses(negated_goals). (c1 + c2 ') ' + (c1 ' + c2 ') ' != c2 # answer(Huntington). end_of_list. ============================== end of process goals ================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 x + y = y + x. [input]. 2 (x + y) + z = x + (y + z). [input]. 3 ((x + y) ' + (x + y ') ') ' = x # label(Robbins). [input]. 4 c + c = c. [input]. 5 (c1 + c2 ') ' + (c1 ' + c2 ') ' != c2 # answer(Huntington). [clausify]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). Auto_denials: no changes. % Restrict denials; moving clauses to denials list: clauses(denials). 5 (c1 + c2 ') ' + (c1 ' + c2 ') ' != c2 # answer(Huntington). [clausify]. end_of_list. Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c, c1, c2, +, ' ]). After inverse_order: Function symbol precedence: lex([ c, c1, c2, +, ' ]). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: no changes. % Operation + is commutative; redundancy checks enabled. % Operation + is associative-commutative; redundancy checks enabled. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 6 x + y = y + x. [input]. 7 (x + y) + z = x + (y + z). [input]. 8 ((x + y) ' + (x + y ') ') ' = x # label(Robbins). [input]. 9 c + c = c. [input]. end_of_list. clauses(demodulators). 6 x + y = y + x. [input]. % (lex-dep) 7 (x + y) + z = x + (y + z). [input]. 8 ((x + y) ' + (x + y ') ') ' = x # label(Robbins). [input]. 9 c + c = c. [input]. end_of_list. clauses(denials). 10 (c1 + c2 ') ' + (c1 ' + c2 ') ' != c2 # answer(Huntington). [clausify]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 6 x + y = y + x. [input]. given #2 (I,wt=11): 7 (x + y) + z = x + (y + z). [input]. given #3 (I,wt=13): 8 ((x + y) ' + (x + y ') ') ' = x # label(Robbins). [input]. given #4 (I,wt=5): 9 c + c = c. [input]. given #5 (T,wt=9): 18 c + (c + x) = c + x. [para(9(a,1),7(a,1,1)),flip(a)]. given #6 (A,wt=11): 11 x + (y + z) = y + (x + z). [para(6(a,1),7(a,1,1)),demod(7(2))]. given #7 (F,wt=9): 19 c + (x + c) = x + c. [para(9(a,1),7(a,2,2)),demod(6(4))]. given #8 (F,wt=11): 20 (c ' + (c + c ') ') ' = c. [para(9(a,1),8(a,1,1,1,1))]. given #9 (T,wt=13): 12 ((x + y) ' + (y + x ') ') ' = y. [para(6(a,1),8(a,1,1,1,1))]. given #10 (T,wt=13): 13 ((x + y) ' + (y ' + x) ') ' = x. [para(6(a,1),8(a,1,1,2,1))]. given #11 (A,wt=19): 14 ((x + (y + z)) ' + (x + (y + z ')) ') ' = x + y. [para(7(a,1),8(a,1,1,1,1)),demod(7(6))]. given #12 (F,wt=13): 21 c + (x + (c + y)) = x + (c + y). [para(18(a,1),7(a,2,2)),demod(11(5),7(4))]. given #13 (F,wt=13): 24 c + (x + (y + c)) = c + (x + y). [para(7(a,1),19(a,1,2)),demod(6(8))]. given #14 (T,wt=13): 29 ((x + y) ' + (x ' + y) ') ' = y. [para(6(a,1),12(a,1,1,2,1))]. given #15 (T,wt=13): 30 ((x + y ') ' + (y + x) ') ' = x. [para(6(a,1),12(a,1,1))]. given #16 (A,wt=20): 15 (x + ((x + y) ' + (x + y ') ' ') ') ' = (x + y) '. [para(8(a,1),8(a,1,1,1))]. given #17 (F,wt=13): 45 ((x ' + y) ' + (y + x) ') ' = y. [para(6(a,1),13(a,1,1))]. given #18 (F,wt=14): 28 (c + (c + (c ' + c ')) ') ' = c '. [para(20(a,1),8(a,1,1,2)),demod(11(7),6(10))]. given #19 (T,wt=11): 200 (c + (c + c ') ') ' = c '. [para(28(a,1),15(a,2)),demod(191(10),191(18),15(23))]. given #20 (T,wt=14): 191 (c + (c ' + c ')) ' = (c + c ') '. [para(28(a,1),12(a,1,1,1)),demod(6(13),190(14),6(4)),flip(a)]. given #21 (A,wt=21): 16 ((x + y) ' + (x + ((y + z) ' + (y + z ') ')) ') ' = x. [para(8(a,1),8(a,1,1,2,1,2)),demod(6(11))]. given #22 (F,wt=15): 22 ((c + x) ' + (c + (c + x) ') ') ' = c. [para(18(a,1),8(a,1,1,1,1))]. given #23 (F,wt=15): 25 ((x + c) ' + (c + (x + c) ') ') ' = c. [para(19(a,1),8(a,1,1,1,1))]. given #24 (T,wt=15): 193 (c ' + (c + (c + c ') ' ') ') ' = c. [para(28(a,1),13(a,1,1,1)),demod(191(10),6(10))]. given #25 (T,wt=15): 287 ((x + c) ' + (c + (c + x) ') ') ' = c. [para(6(a,1),22(a,1,1,1,1))]. given #26 (A,wt=18): 17 (x + (x + (y ' + (x + y) ')) ') ' = (x + y) '. [para(8(a,1),8(a,1,1,2)),demod(6(5),7(5),6(7))]. given #27 (F,wt=15): 288 ((c + x) ' + (c + (x + c) ') ') ' = c. [para(6(a,1),22(a,1,1,2,1,2,1))]. given #28 (F,wt=16): 26 (c + (c ' + (c + c ') ' ') ') ' = c '. [para(20(a,1),8(a,1,1,1))]. given #29 (T,wt=17): 23 ((x + (y + z)) ' + (y + (x + z) ') ') ' = y. [para(11(a,1),8(a,1,1,1,1))]. given #30 (T,wt=17): 31 ((x + (y + z)) ' + (z + (x + y) ') ') ' = z. [para(7(a,1),12(a,1,1,1,1))]. given #31 (A,wt=19): 27 ((x + c) ' + (x + (c ' + (c + c ') ')) ') ' = x. [para(20(a,1),8(a,1,1,2,1,2)),demod(6(14))]. given #32 (F,wt=17): 38 ((c + x) ' + (c + (x + c ')) ') ' = c + x. [para(18(a,1),12(a,1,1,1,1)),demod(7(8))]. given #33 (F,wt=9): 563 c + (c + c ') ' = c. [para(200(a,1),38(a,1,1,1)),demod(6(11),526(15)),flip(a)]. given #34 (T,wt=13): 574 c + ((c + c ') ' + x) = c + x. [para(563(a,1),7(a,1,1)),flip(a)]. given #35 (T,wt=9): 582 (c + c ') ' + x = x. [para(574(a,1),12(a,1,1,1,1)),demod(6(12),101(15)),flip(a)]. given #36 (A,wt=19): 32 ((x + (y + z)) ' + (y + (z + x ')) ') ' = y + z. [para(7(a,1),12(a,1,1,2,1))]. given #37 (F,wt=5): 605 c ' ' = c. [para(582(a,1),30(a,1,1)),demod(9(3))]. given #38 (F,wt=9): 599 x + (c + c ') ' = x. [para(582(a,1),6(a,1)),flip(a)]. given #39 (T,wt=10): 610 (x ' + x ') ' ' = x '. [para(582(a,1),17(a,1,1,2,1,2,2,1)),demod(582(14),582(10),582(11))]. given #40 (T,wt=7): 666 (x + x) ' ' = x. [para(8(a,1),610(a,1,1,1,1)),demod(8(7),8(10))]. given #41 (A,wt=20): 33 (x + ((y + x) ' + (x + y ') ' ') ') ' = (y + x) '. [para(12(a,1),8(a,1,1,1))]. given #42 (F,wt=11): 595 (c + c ') ' ' = c + c '. [back_demod(211),demod(582(11))]. given #43 (F,wt=11): 607 (c + c ') ' = (x + x ') '. [para(582(a,1),16(a,1,1,1,1)),demod(582(13),8(8),6(2)),flip(a)]. NOTE: New constant: 0 (x + x ') ' = c_0. [new_symbol(810)]. NOTE: New Function symbol precedence: lex([ c, c1, c2, c_0, +, ' ]). given #44 (T,wt=5): 767 x ' ' = x. [para(607(a,2),13(a,1,1,2)),demod(6(3),6(10),582(10),759(5)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.14 (+ 0.00) seconds: Huntington. % Length of proof is 29. % Level of proof is 13. % Maximum clause weight is 21. % Given clauses 44. 6 x + y = y + x. [input]. 7 (x + y) + z = x + (y + z). [input]. 8 ((x + y) ' + (x + y ') ') ' = x # label(Robbins). [input]. 9 c + c = c. [input]. 10 (c1 + c2 ') ' + (c1 ' + c2 ') ' != c2 # answer(Huntington). [clausify]. 11 x + (y + z) = y + (x + z). [para(6(a,1),7(a,1,1)),demod(7(2))]. 12 ((x + y) ' + (y + x ') ') ' = y. [para(6(a,1),8(a,1,1,1,1))]. 13 ((x + y) ' + (y ' + x) ') ' = x. [para(6(a,1),8(a,1,1,2,1))]. 15 (x + ((x + y) ' + (x + y ') ' ') ') ' = (x + y) '. [para(8(a,1),8(a,1,1,1))]. 16 ((x + y) ' + (x + ((y + z) ' + (y + z ') ')) ') ' = x. [para(8(a,1),8(a,1,1,2,1,2)),demod(6(11))]. 18 c + (c + x) = c + x. [para(9(a,1),7(a,1,1)),flip(a)]. 20 (c ' + (c + c ') ') ' = c. [para(9(a,1),8(a,1,1,1,1))]. 27 ((x + c) ' + (x + (c ' + (c + c ') ')) ') ' = x. [para(20(a,1),8(a,1,1,2,1,2)),demod(6(14))]. 28 (c + (c + (c ' + c ')) ') ' = c '. [para(20(a,1),8(a,1,1,2)),demod(11(7),6(10))]. 29 ((x + y) ' + (x ' + y) ') ' = y. [para(6(a,1),12(a,1,1,2,1))]. 38 ((c + x) ' + (c + (x + c ')) ') ' = c + x. [para(18(a,1),12(a,1,1,1,1)),demod(7(8))]. 101 ((c + x) ' + (c ' + ((c + c ') ' + x)) ') ' = x. [para(20(a,1),29(a,1,1,2,1,1)),demod(7(9),6(14))]. 190 (c ' + (c + (c ' + c ')) ') ' = c. [para(28(a,1),8(a,1,1,2)),demod(18(9),6(11))]. 191 (c + (c ' + c ')) ' = (c + c ') '. [para(28(a,1),12(a,1,1,1)),demod(6(13),190(14),6(4)),flip(a)]. 200 (c + (c + c ') ') ' = c '. [para(28(a,1),15(a,2)),demod(191(10),191(18),15(23))]. 526 (c ' + (c + (c ' + (c + c ') ')) ') ' = c. [para(9(a,1),27(a,1,1,1,1))]. 563 c + (c + c ') ' = c. [para(200(a,1),38(a,1,1,1)),demod(6(11),526(15)),flip(a)]. 574 c + ((c + c ') ' + x) = c + x. [para(563(a,1),7(a,1,1)),flip(a)]. 582 (c + c ') ' + x = x. [para(574(a,1),12(a,1,1,1,1)),demod(6(12),101(15)),flip(a)]. 607 (c + c ') ' = (x + x ') '. [para(582(a,1),16(a,1,1,1,1)),demod(582(13),8(8),6(2)),flip(a)]. 759 (x + x ' ') ' ' = x. [para(607(a,2),8(a,1,1,1)),demod(582(10))]. 767 x ' ' = x. [para(607(a,2),13(a,1,1,2)),demod(6(3),6(10),582(10),759(5)),flip(a)]. 914 (x + y) ' + (x ' + y) ' = y '. [para(29(a,1),767(a,1,1)),flip(a)]. 927 $F # answer(Huntington). [back_demod(10),demod(914(12),767(3)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=44. Generated=2651. Kept=921. proofs=1. Usable=19. Sos=381. Demods=413. Denials=0. Limbo=13, Disabled=513. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=1729. Back_subsumed=34. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=919 (4 lex), Back_demodulated=474. Back_unit_deleted=0. Demod_attempts=55131. Demod_rewrites=5847. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=1.19. User_CPU=0.14, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13068 exit (max_proofs) Mon Jun 19 16:41:01 2006