============================== Prover9 =============================== Prover9 (64) version 2009-02A, February 2009. Process 25766 was started by veroff on proof, Sun Sep 20 07:31:00 2009 The command was "prover9 -f 2.3.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file 2.3.in op(400,infix,[^,v,"=>",*]). op(200,prefix,~). lex([0,1,*,^,=>,v,~]). assign(order,kbo). set(lex_order_vars). set(para_units_only). % set(para_units_only) -> assign(para_lit_limit, 1). clear(back_demod). set(restrict_denials). formulas(assumptions). x => ((x => y) => y) = 1 # label("(A1)[= 1]"). (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]"). (x ^ y) => x = 1 # label("(A3)[= 1]"). (x ^ y) => y = 1 # label("(A4)[= 1]"). ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). x => (x v y) = 1 # label("(A6)[= 1]"). y => (x v y) = 1 # label("(A7)[= 1]"). ((x => z) ^ (y => z)) => ((x v y) => z) = 1 # label("(A8)[= 1]"). (x ^ (y v z)) => ((x ^ y) v z) = 1 # label("(A9)[= 1]"). ~ ~ x => x = 1 # label("(A10)[= 1]"). (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). x => (y => x) = 1 # label("(A12)[= 1]"). ((x => (x => y)) ^ (~ y => (x => y))) => (x => y) = 1 # label("(A13)[= 1]"). (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)"). (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)"). (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)"). end_of_list. formulas(goals). x => x = y => y # label("(7)"). ~ x = x => ~ (y => y) # label("(8)"). x => y = ~ y => ~ x # label("(9)"). end_of_list. formulas(hints). x => 1 = 1. 1 = (1 => x) => x. (1 => x) => x = 1. x => ~ y = y => ~ x. 1 = ((x => 1) => y) => y. ((x => 1) => y) => y = 1. 1 => x = x. x => x = 1. 1 = x => (y => y). x => (y => y) = 1. x => x = y => y. (x => 1) => y = y. (x => x) => y = y. ~ x = x => ~ (y => y). x => ~ (y => y) = ~ x. end_of_list. WARNING, function symbols in function_order (lex) command not found in formulas: 0, *. WARNING, function symbols in function_order (lex) command not found in formulas: 0, *. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 2 (all x all y (x = 1 & y = 1 -> x ^ y = 1)) # label("(4)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 4 x => x = y => y # label("(7)") # label(non_clause) # label(goal). [goal]. 5 ~ x = x => ~ (y => y) # label("(8)") # label(non_clause) # label(goal). [goal]. 6 x => y = ~ y => ~ x # label("(9)") # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]"). [assumption]. (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. (x ^ y) => y = 1 # label("(A4)[= 1]"). [assumption]. ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. x => (x v y) = 1 # label("(A6)[= 1]"). [assumption]. x => (y v x) = 1 # label("(A7)[= 1]"). [assumption]. ((x => y) ^ (z => y)) => ((x v z) => y) = 1 # label("(A8)[= 1]"). [assumption]. (x ^ (y v z)) => ((x ^ y) v z) = 1 # label("(A9)[= 1]"). [assumption]. ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. ((x => (x => y)) ^ (~ y => (x => y))) => (x => y) = 1 # label("(A13)[= 1]"). [assumption]. x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. x != 1 | y != 1 | x ^ y = 1 # label("(4)"). [clausify(2)]. x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. c2 => c2 != c1 => c1 # label("(7)"). [deny(4)]. ~ c3 != c3 => ~ (c4 => c4) # label("(8)"). [deny(5)]. ~ c6 => ~ c5 != c5 => c6 # label("(9)"). [deny(6)]. end_of_list. formulas(demodulators). end_of_list. % 15 hints input. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % copying label "(7)" to answer in negative clause % copying label "(8)" to answer in negative clause % copying label "(9)" to answer in negative clause % assign(max_proofs, 3). % (Horn set with more than one neg. clause) Term ordering decisions: Function symbol KB weights: 1=1. c1=1. c2=1. c3=1. c4=1. c5=1. c6=1. ^=1. =>=1. v=1. ~=1. Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ 1, c1, c2, c3, c4, c5, c6, ^, =>, v, ~ ]). Skipping inverse_order, because there is a function_order (lex) command. Skipping unfold_eq, because there is a function_order (lex) command. Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(hyper_resolution). % (nonunit Horn with equality) % set(hyper_resolution) -> set(pos_hyper_resolution). % set(neg_ur_resolution). % (nonunit Horn with equality) Auto_process settings: (no changes). kept: 7 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. kept: 8 (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]"). [assumption]. kept: 9 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. kept: 10 (x ^ y) => y = 1 # label("(A4)[= 1]"). [assumption]. kept: 11 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. kept: 12 x => (x v y) = 1 # label("(A6)[= 1]"). [assumption]. kept: 13 x => (y v x) = 1 # label("(A7)[= 1]"). [assumption]. kept: 14 ((x => y) ^ (z => y)) => ((x v z) => y) = 1 # label("(A8)[= 1]"). [assumption]. kept: 15 (x ^ (y v z)) => ((x ^ y) v z) = 1 # label("(A9)[= 1]"). [assumption]. kept: 16 ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. kept: 17 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. kept: 18 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. kept: 19 ((x => (x => y)) ^ (~ y => (x => y))) => (x => y) = 1 # label("(A13)[= 1]"). [assumption]. 20 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. kept: 21 1 != x | x => y != 1 | 1 = y. [copy(20),flip(a),flip(c)]. 22 x != 1 | y != 1 | x ^ y = 1 # label("(4)"). [clausify(2)]. kept: 23 1 != x | 1 != y | x ^ y = 1. [copy(22),flip(a),flip(b)]. kept: 24 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. kept: 25 c2 => c2 != c1 => c1 # label("(7)") # answer("(7)"). [deny(4)]. 26 ~ c3 != c3 => ~ (c4 => c4) # label("(8)") # answer("(8)"). [deny(5)]. kept: 27 c3 => ~ (c4 => c4) != ~ c3 # answer("(8)"). [copy(26),flip(a)]. kept: 28 ~ c6 => ~ c5 != c5 => c6 # label("(9)") # answer("(9)"). [deny(6)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 25 c2 => c2 != c1 => c1 # label("(7)") # answer("(7)"). [deny(4)]. 27 c3 => ~ (c4 => c4) != ~ c3 # answer("(8)"). [copy(26),flip(a)]. 28 ~ c6 => ~ c5 != c5 => c6 # label("(9)") # answer("(9)"). [deny(6)]. end_of_list. formulas(sos). 7 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. 8 (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]"). [assumption]. 9 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. 10 (x ^ y) => y = 1 # label("(A4)[= 1]"). [assumption]. 11 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. 12 x => (x v y) = 1 # label("(A6)[= 1]"). [assumption]. 13 x => (y v x) = 1 # label("(A7)[= 1]"). [assumption]. 14 ((x => y) ^ (z => y)) => ((x v z) => y) = 1 # label("(A8)[= 1]"). [assumption]. 15 (x ^ (y v z)) => ((x ^ y) v z) = 1 # label("(A9)[= 1]"). [assumption]. 16 ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. 17 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. 18 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. 19 ((x => (x => y)) ^ (~ y => (x => y))) => (x => y) = 1 # label("(A13)[= 1]"). [assumption]. 21 1 != x | x => y != 1 | 1 = y. [copy(20),flip(a),flip(c)]. 23 1 != x | 1 != y | x ^ y = 1. [copy(22),flip(a),flip(b)]. 24 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. end_of_list. formulas(demodulators). end_of_list. % 11 hints (15 processed, 4 redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=9): 7 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. given #2 (I,wt=13): 8 (x => y) => ((y => z) => (x => z)) = 1 # label("(A2)[= 1]"). [assumption]. given #3 (I,wt=7): 9 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. given #4 (I,wt=7): 10 (x ^ y) => y = 1 # label("(A4)[= 1]"). [assumption]. given #5 (I,wt=15): 11 ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 # label("(A5)[= 1]"). [assumption]. given #6 (I,wt=7): 12 x => (x v y) = 1 # label("(A6)[= 1]"). [assumption]. given #7 (I,wt=7): 13 x => (y v x) = 1 # label("(A7)[= 1]"). [assumption]. given #8 (I,wt=15): 14 ((x => y) ^ (z => y)) => ((x v z) => y) = 1 # label("(A8)[= 1]"). [assumption]. given #9 (I,wt=13): 15 (x ^ (y v z)) => ((x ^ y) v z) = 1 # label("(A9)[= 1]"). [assumption]. given #10 (I,wt=7): 16 ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. given #11 (I,wt=11): 17 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. given #12 (I,wt=7): 18 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. given #13 (I,wt=18): 19 ((x => (x => y)) ^ (~ y => (x => y))) => (x => y) = 1 # label("(A13)[= 1]"). [assumption]. given #14 (I,wt=11): 21 1 != x | x => y != 1 | 1 = y. [copy(20),flip(a),flip(c)]. given #15 (I,wt=11): 23 1 != x | 1 != y | x ^ y = 1. [copy(22),flip(a),flip(b)]. given #16 (I,wt=13): 24 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. given #17 (H,wt=5): 137 x => 1 = 1. [para(9(a,1),18(a,1,2))]. given #18 (H,wt=7): 249 (1 => x) => x = 1. [hyper(21,a,xx,b,7,a),flip(a)]. given #19 (H,wt=5): 484 1 => x = x. [hyper(24,a,18,a,b,249,a)]. given #20 (H,wt=5): 539 x => x = 1. [para(484(a,1),18(a,1,2))]. given #21 (H,wt=7): 575 x => (y => y) = 1. [hyper(21,a,539,a(flip),b,18,a),flip(a)]. -------- Proof 1 -------- "(7)". ============================== PROOF ================================= % Proof 1 at 0.02 (+ 0.00) seconds: "(7)". % Length of proof is 15. % Level of proof is 8. % Maximum clause weight is 13. % Given clauses 21. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 4 x => x = y => y # label("(7)") # label(non_clause) # label(goal). [goal]. 7 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. 18 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. 20 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 21 1 != x | x => y != 1 | 1 = y. [copy(20),flip(a),flip(c)]. 24 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 25 c2 => c2 != c1 => c1 # label("(7)") # answer("(7)"). [deny(4)]. 249 (1 => x) => x = 1. [hyper(21,a,xx,b,7,a),flip(a)]. 484 1 => x = x. [hyper(24,a,18,a,b,249,a)]. 539 x => x = 1. [para(484(a,1),18(a,1,2))]. 575 x => (y => y) = 1. [hyper(21,a,539,a(flip),b,18,a),flip(a)]. 585 x => x = y => y. [hyper(24,a,575,a,b,575,a)]. 586 $F # answer("(7)"). [resolve(585,a,25,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 25 given #22 (H,wt=7): 585 x => x = y => y. [hyper(24,a,575,a,b,575,a)]. given #23 (H,wt=9): 446 x => ~ y = y => ~ x. [hyper(24,a,17,a,b,17,a)]. given #24 (H,wt=9): 480 ((x => 1) => y) => y = 1. [hyper(21,a,137,a(flip),b,7,a),flip(a)]. given #25 (H,wt=7): 658 (x => 1) => y = y. [hyper(24,a,18,a,b,480,a)]. given #26 (H,wt=7): 723 (x => x) => y = y. [para(585(a,1),658(a,1,1))]. -------- Proof 2 -------- "(8)". ============================== PROOF ================================= % Proof 2 at 0.03 (+ 0.00) seconds: "(8)". % Length of proof is 24. % Level of proof is 10. % Maximum clause weight is 13. % Given clauses 26. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 5 ~ x = x => ~ (y => y) # label("(8)") # label(non_clause) # label(goal). [goal]. 7 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. 9 (x ^ y) => x = 1 # label("(A3)[= 1]"). [assumption]. 17 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. 18 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. 20 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 21 1 != x | x => y != 1 | 1 = y. [copy(20),flip(a),flip(c)]. 24 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 26 ~ c3 != c3 => ~ (c4 => c4) # label("(8)") # answer("(8)"). [deny(5)]. 27 c3 => ~ (c4 => c4) != ~ c3 # answer("(8)"). [copy(26),flip(a)]. 137 x => 1 = 1. [para(9(a,1),18(a,1,2))]. 249 (1 => x) => x = 1. [hyper(21,a,xx,b,7,a),flip(a)]. 446 x => ~ y = y => ~ x. [hyper(24,a,17,a,b,17,a)]. 480 ((x => 1) => y) => y = 1. [hyper(21,a,137,a(flip),b,7,a),flip(a)]. 484 1 => x = x. [hyper(24,a,18,a,b,249,a)]. 539 x => x = 1. [para(484(a,1),18(a,1,2))]. 575 x => (y => y) = 1. [hyper(21,a,539,a(flip),b,18,a),flip(a)]. 585 x => x = y => y. [hyper(24,a,575,a,b,575,a)]. 658 (x => 1) => y = y. [hyper(24,a,18,a,b,480,a)]. 723 (x => x) => y = y. [para(585(a,1),658(a,1,1))]. 735 x => ~ (y => y) = ~ x. [para(723(a,1),446(a,1)),flip(a)]. 736 $F # answer("(8)"). [resolve(735,a,27,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 26x 27 given #27 (H,wt=9): 735 x => ~ (y => y) = ~ x. [para(723(a,1),446(a,1)),flip(a)]. given #28 (A,wt=11): 29 x => (1 => ((x => y) => y)) = 1. [para(7(a,1),7(a,1,2,1))]. given #29 (T,wt=5): 247 x v 1 = 1. [hyper(21,a,xx,b,13,a),flip(a)]. given #30 (T,wt=5): 248 1 v x = 1. [hyper(21,a,xx,b,12,a),flip(a)]. given #31 (T,wt=5): 445 1 ^ 1 = 1. [hyper(23,a,xx,b,xx)]. given #32 (T,wt=7): 461 1 ^ (x => 1) = 1. [hyper(23,a,xx,b,137,a(flip))]. given #33 (A,wt=15): 30 (x => y) => (1 => ((y => z) => (x => z))) = 1. [para(8(a,1),7(a,1,2,1))]. given #34 (T,wt=7): 475 (x => 1) ^ 1 = 1. [hyper(23,a,137,a(flip),b,xx)]. given #35 (T,wt=7): 476 x => (y => 1) = 1. [hyper(21,a,137,a(flip),b,18,a),flip(a)]. given #36 (T,wt=7): 477 x v (y => 1) = 1. [hyper(21,a,137,a(flip),b,13,a),flip(a)]. given #37 (T,wt=7): 478 (x => 1) v y = 1. [hyper(21,a,137,a(flip),b,12,a),flip(a)]. given #38 (A,wt=15): 31 1 => ((((x => y) => y) => z) => (x => z)) = 1. [para(7(a,1),8(a,1,1))]. given #39 (T,wt=7): 558 1 ^ (x => x) = 1. [hyper(23,a,xx,b,539,a(flip))]. given #40 (T,wt=7): 574 (x => x) ^ 1 = 1. [hyper(23,a,539,a(flip),b,xx)]. given #41 (T,wt=7): 576 x => ~ ~ x = 1. [hyper(21,a,539,a(flip),b,17,a),flip(a)]. given #42 (T,wt=5): 1730 ~ ~ x = x. [hyper(24,a,16,a,b,576,a),flip(a)]. -------- Proof 3 -------- "(9)". ============================== PROOF ================================= % Proof 3 at 0.05 (+ 0.00) seconds: "(9)". % Length of proof is 19. % Level of proof is 9. % Maximum clause weight is 13. % Given clauses 42. 1 (all x all y (x = 1 & x => y = 1 -> y = 1)) # label("(3)") # label(non_clause). [assumption]. 3 (all x all y (x => y = 1 & y => x = 1 -> x = y)) # label("(5)") # label(non_clause). [assumption]. 6 x => y = ~ y => ~ x # label("(9)") # label(non_clause) # label(goal). [goal]. 7 x => ((x => y) => y) = 1 # label("(A1)[= 1]"). [assumption]. 16 ~ ~ x => x = 1 # label("(A10)[= 1]"). [assumption]. 17 (x => ~ y) => (y => ~ x) = 1 # label("(A11)[= 1]"). [assumption]. 18 x => (y => x) = 1 # label("(A12)[= 1]"). [assumption]. 20 x != 1 | x => y != 1 | y = 1 # label("(3)"). [clausify(1)]. 21 1 != x | x => y != 1 | 1 = y. [copy(20),flip(a),flip(c)]. 24 x => y != 1 | y => x != 1 | y = x # label("(5)"). [clausify(3)]. 28 ~ c6 => ~ c5 != c5 => c6 # label("(9)") # answer("(9)"). [deny(6)]. 249 (1 => x) => x = 1. [hyper(21,a,xx,b,7,a),flip(a)]. 446 x => ~ y = y => ~ x. [hyper(24,a,17,a,b,17,a)]. 484 1 => x = x. [hyper(24,a,18,a,b,249,a)]. 539 x => x = 1. [para(484(a,1),18(a,1,2))]. 576 x => ~ ~ x = 1. [hyper(21,a,539,a(flip),b,17,a),flip(a)]. 1730 ~ ~ x = x. [hyper(24,a,16,a,b,576,a),flip(a)]. 1929 ~ x => ~ y = y => x. [para(1730(a,1),446(a,1,2)),flip(a)]. 1930 $F # answer("(9)"). [resolve(1929,a,28,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=42. Generated=3081. Kept=1918. proofs=3. Usable=43. Sos=1667. Demods=0. Limbo=80, Disabled=146. Hints=15. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=1163. Back_subsumed=125. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=3. Megabytes=2.27. User_CPU=0.05, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED THEOREM PROVED Exiting with 3 proofs. ------ process 25766 exit (max_proofs) ------  Process 25766 exit (max_proofs) Sun Sep 20 07:31:01 2009