============================== Prover9 =============================== Prover9 (64) version Aug-2007, Aug 2007. Process 32355 was started by veroff on io, Mon Jan 21 11:14:39 2008 The command was "prover9 -f 3.1_alt.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file 3.1_alt.in clear(auto). % clear(auto) -> clear(auto_inference). % clear(auto_inference) -> clear(predicate_elim). % clear(auto_inference) -> assign(eq_defs, pass). % clear(auto) -> clear(auto_limits). % clear(auto_limits) -> assign(max_weight, 2147483647). % clear(auto_limits) -> assign(sos_limit, -1). % clear(auto) -> clear(auto_denials). % clear(auto) -> clear(auto_process). op(400,infix,[^,v,"->","=>",*]). op(200,prefix,[~,-]). lex([0,1,*,^,=>,->,v,~,-]). assign(order,kbo). set(lex_order_vars). set(paramodulation). % set(paramodulation) -> set(back_demod). set(para_units_only). % set(para_units_only) -> assign(para_lit_limit, 1). clear(back_demod). set(hyper_resolution). % set(hyper_resolution) -> set(pos_hyper_resolution). set(auto_denials). set(restrict_denials). formulas(assumptions). (x v y) v z = x v (y v z) # label("(D1)"). (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). x v y = y v x # label("(D3)"). x ^ y = y ^ x # label("(D4)"). x v (x ^ y) = x # label("(D5)"). x ^ (x v y) = x # label("(D6)"). (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). x v 0 = x # label("(D9)"). x ^ 1 = x # label("(D10)"). x ^ 0 = 0 # label("(2.1)"). ~ x v ~ y = ~ (x ^ y) # label("(DM1)"). ~ x ^ ~ y = ~ (x v y) # label("(DM2)"). ~ ~ x = x # label("(DN)"). ~ 1 = 0 # label("(2.2)"). (x ^ ~ x) ^ (y v ~ y) = x ^ ~ x # label("(N1)"). x -> x = 1 # label("(N2)"). (x -> y) ^ (~ x v y) = ~ x v y # label("(N3)"). x ^ (~ x v y) = x ^ (x -> y) # label("(N4)"). (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)"). (x ^ y) -> z = x -> (y -> z) # label("(N6)"). -x = x -> 0 # label("(N7)"). x * y = ~ (x -> ~ y) v ~ (y -> ~ x) # label("(* def)"). x => y = (x -> y) ^ (~ y -> ~ x) # label("(=> def)"). x -> 1 = 1 # label("(3.1)"). 1 -> x = x # label("(3.2)"). (x -> y) -> (x -> z) = x -> (y -> z) # label("(3.3)"). x -> (y -> z) = y -> (x -> z) # label("(3.4)"). x -> (x -> y) = x -> y # label("(3.5)"). (x -> y) ^ (z -> y) = (x v z) -> y # label("(3.6)"). x ^ ((x => y) => y) = x # label("(3.7)"). x -> ~ (x -> y) = x -> ~ y # label("(3.8)"). ~ (x -> y) -> z = x -> (~ y -> z) # label("(3.9)"). 1 => x = x # label("(BCK2)"). x => 1 = 1 # label("(BCK3)"). x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). end_of_list. formulas(goals). (x ^ y) -> y = 1 # label("(3.10)"). (x ^ y) => y = 1 # label("(3.11)"). ~ x => ~ y = y => x # label("(3.12)"). (x => y) ^ y = y # label("(3.13)"). x => (x ^ y) = x => y # label("(3.14)"). end_of_list. formulas(hints). (x ^ y) -> y = 1 # label("(3.10)"). (x ^ y) => y = 1 # label("(3.11)"). ~ x => ~ y = y => x # label("(3.12)"). (x => y) ^ y = y # label("(3.13)"). x => (x ^ y) = x => y # label("(3.14)"). (x -> ~ y) ^ (y -> ~ x) = x => ~ y. 1 ^ (x -> y) = x -> (x ^ y). (x => y) ^ z = (x -> y) ^ ((~ y -> ~ x) ^ z). (x -> y) ^ ((~ y -> ~ x) ^ z) = (x => y) ^ z. x ^ (y v ~ x) = x ^ (x -> y). (~ x -> ~ y) ^ (y -> x) = y => x. x v (y ^ x) = x. x ^ (y v x) = x. (x -> y) ^ (x -> 1) = x -> y. x = 1 ^ x. 1 ^ x = x. 1 ^ (x -> y) = (y v x) -> y. x ^ (y -> x) = (1 v y) -> x. 1 v x = 1. x ^ (y v (z v x)) = x. x ^ (y v (x v z)) = x. x -> (x ^ y) = x -> y. (x -> y) ^ (~ (x ^ y) -> ~ x) = x => (x ^ y). x -> x = x -> (x v y). x -> (x v y) = x -> x. x -> (x ^ (x -> y)) = x -> y. x -> (x v y) = 1. ~ x -> ~ (x ^ y) = 1. x -> (y v x) = 1. (x ^ y) -> y = 1. ((x ^ y) -> x) ^ 1 = (x ^ y) => x. (x v y) -> x = y -> x. ~ (x ^ y) -> ~ x = ~ y -> ~ x. x ^ (y -> x) = 1 -> x. x ^ (y -> x) = x. x = (y -> x) ^ x. (x -> y) ^ y = y. (x -> y) v y = x -> y. x -> (y -> x) = 1. (x -> (y -> x)) ^ (x -> 1) = 1. x ^ (y -> (x v z)) = x. (x -> (y -> x)) ^ 1 = 1. x -> (x ^ (x -> y)) = x -> (y v ~ x). (x -> ~ y) ^ (y -> ~ x) = y => ~ x. (x -> (y -> x)) ^ 1 = (x ^ y) => x. (x ^ y) => x = 1. (x ^ y) => y = 1. x -> (y v ~ x) = x -> y. x -> (~ x v y) = x -> y. ~ x ^ (x -> y) = ~ x. x ^ (~ x -> y) = ~ ~ x. x ^ (~ x -> y) = x. x = (~ x -> y) ^ x. (~ x -> y) ^ x = x. x => ~ y = y => ~ x. x => y = ~ y => ~ x. ~ x => ~ y = y => x. (x -> y) ^ y = (x => y) ^ y. (x => y) ^ y = y. (x -> y) ^ (~ y -> ~ x) = x => (x ^ y). x => (x ^ y) = x => y. end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (x ^ y) -> y = 1 # label("(3.10)") # label(non_clause) # label(goal). [goal]. 2 (x ^ y) => y = 1 # label("(3.11)") # label(non_clause) # label(goal). [goal]. 3 ~ x => ~ y = y => x # label("(3.12)") # label(non_clause) # label(goal). [goal]. 4 (x => y) ^ y = y # label("(3.13)") # label(non_clause) # label(goal). [goal]. 5 x => (x ^ y) = x => y # label("(3.14)") # 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 v y) v z = x v (y v z) # label("(D1)"). [assumption]. (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. x v y = y v x # label("(D3)"). [assumption]. x ^ y = y ^ x # label("(D4)"). [assumption]. x v (x ^ y) = x # label("(D5)"). [assumption]. x ^ (x v y) = x # label("(D6)"). [assumption]. (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). [assumption]. (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). [assumption]. x v 0 = x # label("(D9)"). [assumption]. x ^ 1 = x # label("(D10)"). [assumption]. x ^ 0 = 0 # label("(2.1)"). [assumption]. ~ x v ~ y = ~ (x ^ y) # label("(DM1)"). [assumption]. ~ x ^ ~ y = ~ (x v y) # label("(DM2)"). [assumption]. ~ ~ x = x # label("(DN)"). [assumption]. ~ 1 = 0 # label("(2.2)"). [assumption]. (x ^ ~ x) ^ (y v ~ y) = x ^ ~ x # label("(N1)"). [assumption]. x -> x = 1 # label("(N2)"). [assumption]. (x -> y) ^ (~ x v y) = ~ x v y # label("(N3)"). [assumption]. x ^ (~ x v y) = x ^ (x -> y) # label("(N4)"). [assumption]. (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)"). [assumption]. (x ^ y) -> z = x -> (y -> z) # label("(N6)"). [assumption]. -x = x -> 0 # label("(N7)"). [assumption]. x * y = ~ (x -> ~ y) v ~ (y -> ~ x) # label("(* def)"). [assumption]. x => y = (x -> y) ^ (~ y -> ~ x) # label("(=> def)"). [assumption]. x -> 1 = 1 # label("(3.1)"). [assumption]. 1 -> x = x # label("(3.2)"). [assumption]. (x -> y) -> (x -> z) = x -> (y -> z) # label("(3.3)"). [assumption]. x -> (y -> z) = y -> (x -> z) # label("(3.4)"). [assumption]. x -> (x -> y) = x -> y # label("(3.5)"). [assumption]. (x -> y) ^ (z -> y) = (x v z) -> y # label("(3.6)"). [assumption]. x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. x -> ~ (x -> y) = x -> ~ y # label("(3.8)"). [assumption]. ~ (x -> y) -> z = x -> (~ y -> z) # label("(3.9)"). [assumption]. 1 => x = x # label("(BCK2)"). [assumption]. x => 1 = 1 # label("(BCK3)"). [assumption]. x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). [assumption]. (c1 ^ c2) -> c2 != 1 # label("(3.10)"). [deny(1)]. (c3 ^ c4) => c4 != 1 # label("(3.11)"). [deny(2)]. ~ c5 => ~ c6 != c6 => c5 # label("(3.12)"). [deny(3)]. (c7 => c8) ^ c8 != c8 # label("(3.13)"). [deny(4)]. c9 => (c9 ^ c10) != c9 => c10 # label("(3.14)"). [deny(5)]. end_of_list. formulas(demodulators). end_of_list.  WARNING: denials share constants (see output). % 61 hints input. Auto_denials: % copying label "(3.10)" to answer in negative clause % copying label "(3.11)" to answer in negative clause % copying label "(3.12)" to answer in negative clause % copying label "(3.13)" to answer in negative clause % copying label "(3.14)" to answer in negative clause % assign(max_proofs, 5). % (Horn set with more than one neg. clause) WARNING, because some of the denials share constants, some of the denials or their descendents may be subsumed, preventing the target number of proofs from being found. The shared constants are: 1. Term ordering decisions: Function symbol KB weights: 0=1. 1=1. c1=1. c2=1. c3=1. c4=1. c5=1. c6=1. c7=1. c8=1. c9=1. c10=1. *=1. ^=1. =>=1. ->=1. v=1. ~=1. -=1. Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ 0, 1, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, *, ^, =>, ->, v, ~, - ]). Skipping inverse_order, because there is a function_order (lex) command. % Operation v is commutative; C redundancy checks enabled. % Operation ^ is commutative; C redundancy checks enabled. restricted denial: (wt=7): 45 (c1 ^ c2) -> c2 != 1 # label("(3.10)") # answer("(3.10)"). [deny(1)]. restricted denial: (wt=7): 46 (c3 ^ c4) => c4 != 1 # label("(3.11)") # answer("(3.11)"). [deny(2)]. restricted denial: (wt=9): 47 ~ c5 => ~ c6 != c6 => c5 # label("(3.12)") # answer("(3.12)"). [deny(3)]. restricted denial: (wt=7): 48 (c7 => c8) ^ c8 != c8 # label("(3.13)") # answer("(3.13)"). [deny(4)]. restricted denial: (wt=9): 49 c9 => (c9 ^ c10) != c9 => c10 # label("(3.14)") # answer("(3.14)"). [deny(5)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 45 (c1 ^ c2) -> c2 != 1 # label("(3.10)") # answer("(3.10)"). [deny(1)]. 46 (c3 ^ c4) => c4 != 1 # label("(3.11)") # answer("(3.11)"). [deny(2)]. 47 ~ c5 => ~ c6 != c6 => c5 # label("(3.12)") # answer("(3.12)"). [deny(3)]. 48 (c7 => c8) ^ c8 != c8 # label("(3.13)") # answer("(3.13)"). [deny(4)]. 49 c9 => (c9 ^ c10) != c9 => c10 # label("(3.14)") # answer("(3.14)"). [deny(5)]. end_of_list. formulas(sos). 6 (x v y) v z = x v (y v z) # label("(D1)"). [assumption]. 7 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. 8 x v y = y v x # label("(D3)"). [assumption]. 9 x ^ y = y ^ x # label("(D4)"). [assumption]. 10 x v (x ^ y) = x # label("(D5)"). [assumption]. 11 x ^ (x v y) = x # label("(D6)"). [assumption]. 12 (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). [assumption]. 13 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). [assumption]. 14 x v 0 = x # label("(D9)"). [assumption]. 15 x ^ 1 = x # label("(D10)"). [assumption]. 16 x ^ 0 = 0 # label("(2.1)"). [assumption]. 17 ~ x v ~ y = ~ (x ^ y) # label("(DM1)"). [assumption]. 18 ~ x ^ ~ y = ~ (x v y) # label("(DM2)"). [assumption]. 19 ~ ~ x = x # label("(DN)"). [assumption]. 20 ~ 1 = 0 # label("(2.2)"). [assumption]. 21 (x ^ ~ x) ^ (y v ~ y) = x ^ ~ x # label("(N1)"). [assumption]. 22 x -> x = 1 # label("(N2)"). [assumption]. 23 (x -> y) ^ (~ x v y) = ~ x v y # label("(N3)"). [assumption]. 24 x ^ (~ x v y) = x ^ (x -> y) # label("(N4)"). [assumption]. 25 (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)"). [assumption]. 26 (x ^ y) -> z = x -> (y -> z) # label("(N6)"). [assumption]. 28 x -> 0 = -x. [copy(27),flip(a)]. 30 ~ (x -> ~ y) v ~ (y -> ~ x) = x * y. [copy(29),flip(a)]. 32 (x -> y) ^ (~ y -> ~ x) = x => y. [copy(31),flip(a)]. 33 x -> 1 = 1 # label("(3.1)"). [assumption]. 34 1 -> x = x # label("(3.2)"). [assumption]. 35 (x -> y) -> (x -> z) = x -> (y -> z) # label("(3.3)"). [assumption]. 36 x -> (y -> z) = y -> (x -> z) # label("(3.4)"). [assumption]. 37 x -> (x -> y) = x -> y # label("(3.5)"). [assumption]. 38 (x -> y) ^ (z -> y) = (x v z) -> y # label("(3.6)"). [assumption]. 39 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. 40 x -> ~ (x -> y) = x -> ~ y # label("(3.8)"). [assumption]. 41 ~ (x -> y) -> z = x -> (~ y -> z) # label("(3.9)"). [assumption]. 42 1 => x = x # label("(BCK2)"). [assumption]. 43 x => 1 = 1 # label("(BCK3)"). [assumption]. 44 x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). [assumption]. end_of_list. formulas(demodulators). end_of_list. % 61 hints processed (11 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=11): 6 (x v y) v z = x v (y v z) # label("(D1)"). [assumption]. given #2 (I,wt=11): 7 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. given #3 (I,wt=7): 8 x v y = y v x # label("(D3)"). [assumption]. given #4 (I,wt=7): 9 x ^ y = y ^ x # label("(D4)"). [assumption]. given #5 (I,wt=7): 10 x v (x ^ y) = x # label("(D5)"). [assumption]. given #6 (I,wt=7): 11 x ^ (x v y) = x # label("(D6)"). [assumption]. given #7 (I,wt=13): 12 (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). [assumption]. given #8 (I,wt=13): 13 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). [assumption]. given #9 (I,wt=5): 14 x v 0 = x # label("(D9)"). [assumption]. given #10 (I,wt=5): 15 x ^ 1 = x # label("(D10)"). [assumption]. given #11 (I,wt=5): 16 x ^ 0 = 0 # label("(2.1)"). [assumption]. given #12 (I,wt=10): 17 ~ x v ~ y = ~ (x ^ y) # label("(DM1)"). [assumption]. given #13 (I,wt=10): 18 ~ x ^ ~ y = ~ (x v y) # label("(DM2)"). [assumption]. given #14 (I,wt=5): 19 ~ ~ x = x # label("(DN)"). [assumption]. given #15 (I,wt=4): 20 ~ 1 = 0 # label("(2.2)"). [assumption]. given #16 (I,wt=14): 21 (x ^ ~ x) ^ (y v ~ y) = x ^ ~ x # label("(N1)"). [assumption]. given #17 (I,wt=5): 22 x -> x = 1 # label("(N2)"). [assumption]. given #18 (I,wt=13): 23 (x -> y) ^ (~ x v y) = ~ x v y # label("(N3)"). [assumption]. given #19 (I,wt=12): 24 x ^ (~ x v y) = x ^ (x -> y) # label("(N4)"). [assumption]. given #20 (I,wt=13): 25 (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)"). [assumption]. given #21 (I,wt=11): 26 (x ^ y) -> z = x -> (y -> z) # label("(N6)"). [assumption]. given #22 (I,wt=6): 28 x -> 0 = -x. [copy(27),flip(a)]. given #23 (I,wt=15): 30 ~ (x -> ~ y) v ~ (y -> ~ x) = x * y. [copy(29),flip(a)]. given #24 (I,wt=13): 32 (x -> y) ^ (~ y -> ~ x) = x => y. [copy(31),flip(a)]. given #25 (I,wt=5): 33 x -> 1 = 1 # label("(3.1)"). [assumption]. given #26 (I,wt=5): 34 1 -> x = x # label("(3.2)"). [assumption]. given #27 (I,wt=13): 35 (x -> y) -> (x -> z) = x -> (y -> z) # label("(3.3)"). [assumption]. given #28 (I,wt=11): 36 x -> (y -> z) = y -> (x -> z) # label("(3.4)"). [assumption]. given #29 (I,wt=9): 37 x -> (x -> y) = x -> y # label("(3.5)"). [assumption]. given #30 (I,wt=13): 38 (x -> y) ^ (z -> y) = (x v z) -> y # label("(3.6)"). [assumption]. given #31 (I,wt=9): 39 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. given #32 (I,wt=11): 40 x -> ~ (x -> y) = x -> ~ y # label("(3.8)"). [assumption]. given #33 (I,wt=13): 41 ~ (x -> y) -> z = x -> (~ y -> z) # label("(3.9)"). [assumption]. given #34 (I,wt=5): 42 1 => x = x # label("(BCK2)"). [assumption]. given #35 (I,wt=5): 43 x => 1 = 1 # label("(BCK3)"). [assumption]. given #36 (I,wt=13): 44 x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). [assumption]. given #37 (H,wt=5): 122 1 ^ x = x. [para(15(a,1),9(a,1)),flip(a)]. given #38 (H,wt=5): 543 1 v x = 1. [para(122(a,1),10(a,1,2))]. given #39 (H,wt=7): 69 x v (y ^ x) = x. [para(9(a,1),10(a,1,2))]. given #40 (H,wt=7): 74 x ^ (y v x) = x. [para(8(a,1),11(a,1,2))]. given #41 (H,wt=9): 589 x ^ (y v (z v x)) = x. [para(6(a,1),74(a,1,2))]. given #42 (H,wt=9): 611 x ^ (y v (x v z)) = x. [para(8(a,1),589(a,1,2,2))]. given #43 (H,wt=11): 238 (x -> y) ^ (x -> 1) = x -> y. [para(15(a,1),25(a,2,2))]. given #44 (H,wt=11): 243 1 ^ (x -> y) = x -> (x ^ y). [para(22(a,1),25(a,1,1))]. given #45 (H,wt=9): 734 x -> (x ^ y) = x -> y. [para(243(a,1),122(a,1))]. given #46 (H,wt=9): 745 x -> (x v y) = x -> x. [para(11(a,1),734(a,1,2)),flip(a)]. given #47 (H,wt=7): 798 x -> (x v y) = 1. [para(22(a,1),745(a,2))]. given #48 (H,wt=7): 831 x -> (y v x) = 1. [para(8(a,1),798(a,1,2))]. -------- Proof 1 -------- "(3.10)". ============================== PROOF ================================= % Proof 1 at 0.04 (+ 0.00) seconds: "(3.10)". % Length of proof is 18. % Level of proof is 7. % Maximum clause weight is 13. % Given clauses 48. 1 (x ^ y) -> y = 1 # label("(3.10)") # label(non_clause) # label(goal). [goal]. 8 x v y = y v x # label("(D3)"). [assumption]. 9 x ^ y = y ^ x # label("(D4)"). [assumption]. 10 x v (x ^ y) = x # label("(D5)"). [assumption]. 11 x ^ (x v y) = x # label("(D6)"). [assumption]. 15 x ^ 1 = x # label("(D10)"). [assumption]. 22 x -> x = 1 # label("(N2)"). [assumption]. 25 (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)"). [assumption]. 45 (c1 ^ c2) -> c2 != 1 # label("(3.10)") # answer("(3.10)"). [deny(1)]. 69 x v (y ^ x) = x. [para(9(a,1),10(a,1,2))]. 122 1 ^ x = x. [para(15(a,1),9(a,1)),flip(a)]. 243 1 ^ (x -> y) = x -> (x ^ y). [para(22(a,1),25(a,1,1))]. 734 x -> (x ^ y) = x -> y. [para(243(a,1),122(a,1))]. 745 x -> (x v y) = x -> x. [para(11(a,1),734(a,1,2)),flip(a)]. 798 x -> (x v y) = 1. [para(22(a,1),745(a,2))]. 831 x -> (y v x) = 1. [para(8(a,1),798(a,1,2))]. 883 (x ^ y) -> y = 1 # label("(3.10)"). [para(69(a,1),831(a,1,2))]. 884 $F # answer("(3.10)"). [resolve(883,a,45,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 45 given #49 (H,wt=7): 883 (x ^ y) -> y = 1 # label("(3.10)"). [para(69(a,1),831(a,1,2))]. given #50 (H,wt=9): 833 ~ x -> ~ (x ^ y) = 1. [para(17(a,1),798(a,1,2))]. given #51 (H,wt=11): 416 1 ^ (x -> y) = (y v x) -> y. [para(22(a,1),38(a,1,1))]. given #52 (H,wt=9): 1016 (x v y) -> x = y -> x. [para(416(a,1),122(a,1))]. given #53 (H,wt=11): 433 x ^ (y -> x) = (1 v y) -> x. [para(34(a,1),38(a,1,1))]. given #54 (H,wt=9): 1145 x ^ (y -> x) = 1 -> x. [para(543(a,1),433(a,2,1))]. given #55 (H,wt=7): 1189 x ^ (y -> x) = x. [para(34(a,1),1145(a,2))]. given #56 (H,wt=7): 1215 (x -> y) ^ y = y. [para(1189(a,1),9(a,1)),flip(a)]. given #57 (H,wt=7): 1230 x -> (y -> x) = 1. [para(1189(a,1),883(a,1,1))]. given #58 (H,wt=9): 1225 (x -> y) v y = x -> y. [para(1189(a,1),69(a,1,2))]. given #59 (H,wt=9): 1319 x ^ (y -> (x v z)) = x. [para(1225(a,1),611(a,1,2))]. given #60 (H,wt=11): 774 x -> (x ^ (x -> y)) = x -> y. [para(37(a,1),734(a,2))]. given #61 (H,wt=11): 1277 (x -> (y -> x)) ^ (x -> 1) = 1. [para(1230(a,1),238(a,2))]. given #62 (H,wt=9): 1456 (x -> (y -> x)) ^ 1 = 1. [para(33(a,1),1277(a,1,2))]. given #63 (H,wt=12): 213 x ^ (y v ~ x) = x ^ (x -> y). [para(8(a,1),24(a,1,2))]. given #64 (H,wt=13): 299 (~ x -> ~ y) ^ (y -> x) = y => x. [para(32(a,1),9(a,1)),flip(a)]. given #65 (H,wt=13): 941 ((x ^ y) -> x) ^ 1 = (x ^ y) => x. [para(833(a,1),32(a,1,2))]. given #66 (H,wt=13): 1040 ~ (x ^ y) -> ~ x = ~ y -> ~ x. [para(17(a,1),1016(a,1,1))]. given #67 (H,wt=13): 1630 (x -> (y -> x)) ^ 1 = (x ^ y) => x. [para(26(a,1),941(a,1,1))]. given #68 (H,wt=7): 1818 (x ^ y) => x = 1. [para(1630(a,1),1456(a,1))]. -------- Proof 2 -------- "(3.11)". ============================== PROOF ================================= % Proof 2 at 0.08 (+ 0.00) seconds: "(3.11)". % Length of proof is 38. % Level of proof is 12. % Maximum clause weight is 13. % Given clauses 68. 2 (x ^ y) => y = 1 # label("(3.11)") # label(non_clause) # label(goal). [goal]. 8 x v y = y v x # label("(D3)"). [assumption]. 9 x ^ y = y ^ x # label("(D4)"). [assumption]. 10 x v (x ^ y) = x # label("(D5)"). [assumption]. 11 x ^ (x v y) = x # label("(D6)"). [assumption]. 15 x ^ 1 = x # label("(D10)"). [assumption]. 17 ~ x v ~ y = ~ (x ^ y) # label("(DM1)"). [assumption]. 22 x -> x = 1 # label("(N2)"). [assumption]. 25 (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)"). [assumption]. 26 (x ^ y) -> z = x -> (y -> z) # label("(N6)"). [assumption]. 31 x => y = (x -> y) ^ (~ y -> ~ x) # label("(=> def)"). [assumption]. 32 (x -> y) ^ (~ y -> ~ x) = x => y. [copy(31),flip(a)]. 33 x -> 1 = 1 # label("(3.1)"). [assumption]. 34 1 -> x = x # label("(3.2)"). [assumption]. 38 (x -> y) ^ (z -> y) = (x v z) -> y # label("(3.6)"). [assumption]. 46 (c3 ^ c4) => c4 != 1 # label("(3.11)") # answer("(3.11)"). [deny(2)]. 69 x v (y ^ x) = x. [para(9(a,1),10(a,1,2))]. 122 1 ^ x = x. [para(15(a,1),9(a,1)),flip(a)]. 238 (x -> y) ^ (x -> 1) = x -> y. [para(15(a,1),25(a,2,2))]. 243 1 ^ (x -> y) = x -> (x ^ y). [para(22(a,1),25(a,1,1))]. 433 x ^ (y -> x) = (1 v y) -> x. [para(34(a,1),38(a,1,1))]. 543 1 v x = 1. [para(122(a,1),10(a,1,2))]. 734 x -> (x ^ y) = x -> y. [para(243(a,1),122(a,1))]. 745 x -> (x v y) = x -> x. [para(11(a,1),734(a,1,2)),flip(a)]. 798 x -> (x v y) = 1. [para(22(a,1),745(a,2))]. 831 x -> (y v x) = 1. [para(8(a,1),798(a,1,2))]. 833 ~ x -> ~ (x ^ y) = 1. [para(17(a,1),798(a,1,2))]. 883 (x ^ y) -> y = 1 # label("(3.10)"). [para(69(a,1),831(a,1,2))]. 941 ((x ^ y) -> x) ^ 1 = (x ^ y) => x. [para(833(a,1),32(a,1,2))]. 1145 x ^ (y -> x) = 1 -> x. [para(543(a,1),433(a,2,1))]. 1189 x ^ (y -> x) = x. [para(34(a,1),1145(a,2))]. 1230 x -> (y -> x) = 1. [para(1189(a,1),883(a,1,1))]. 1277 (x -> (y -> x)) ^ (x -> 1) = 1. [para(1230(a,1),238(a,2))]. 1456 (x -> (y -> x)) ^ 1 = 1. [para(33(a,1),1277(a,1,2))]. 1630 (x -> (y -> x)) ^ 1 = (x ^ y) => x. [para(26(a,1),941(a,1,1))]. 1818 (x ^ y) => x = 1. [para(1630(a,1),1456(a,1))]. 1829 (x ^ y) => y = 1 # label("(3.11)"). [para(9(a,1),1818(a,1,1))]. 1830 $F # answer("(3.11)"). [resolve(1829,a,46,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 46 given #69 (H,wt=7): 1829 (x ^ y) => y = 1 # label("(3.11)"). [para(9(a,1),1818(a,1,1))]. given #70 (H,wt=14): 305 (x -> ~ y) ^ (y -> ~ x) = x => ~ y. [para(19(a,1),32(a,1,2,1))]. given #71 (H,wt=14): 1535 x -> (x ^ (x -> y)) = x -> (y v ~ x). [para(213(a,1),734(a,1,2))]. given #72 (H,wt=10): 1996 x -> (y v ~ x) = x -> y. [para(1535(a,1),774(a,1))]. given #73 (H,wt=10): 2006 x -> (~ x v y) = x -> y. [para(8(a,1),1996(a,1,2))]. given #74 (H,wt=9): 2133 ~ x ^ (x -> y) = ~ x. [para(2006(a,1),1319(a,1,2))]. given #75 (H,wt=10): 2154 x ^ (~ x -> y) = ~ ~ x. [para(19(a,1),2133(a,1,1))]. given #76 (H,wt=8): 2191 x ^ (~ x -> y) = x. [para(19(a,1),2154(a,2))]. given #77 (H,wt=8): 2218 (~ x -> y) ^ x = x. [para(2191(a,1),9(a,1)),flip(a)]. given #78 (H,wt=14): 1558 (x -> ~ y) ^ (y -> ~ x) = y => ~ x. [para(19(a,1),299(a,1,1,1))]. given #79 (H,wt=9): 2306 x => ~ y = y => ~ x. [para(1558(a,1),305(a,1))]. -------- Proof 3 -------- "(3.12)". ============================== PROOF ================================= % Proof 3 at 0.10 (+ 0.00) seconds: "(3.12)". % Length of proof is 12. % Level of proof is 6. % Maximum clause weight is 14. % Given clauses 79. 3 ~ x => ~ y = y => x # label("(3.12)") # label(non_clause) # label(goal). [goal]. 9 x ^ y = y ^ x # label("(D4)"). [assumption]. 19 ~ ~ x = x # label("(DN)"). [assumption]. 31 x => y = (x -> y) ^ (~ y -> ~ x) # label("(=> def)"). [assumption]. 32 (x -> y) ^ (~ y -> ~ x) = x => y. [copy(31),flip(a)]. 47 ~ c5 => ~ c6 != c6 => c5 # label("(3.12)") # answer("(3.12)"). [deny(3)]. 299 (~ x -> ~ y) ^ (y -> x) = y => x. [para(32(a,1),9(a,1)),flip(a)]. 305 (x -> ~ y) ^ (y -> ~ x) = x => ~ y. [para(19(a,1),32(a,1,2,1))]. 1558 (x -> ~ y) ^ (y -> ~ x) = y => ~ x. [para(19(a,1),299(a,1,1,1))]. 2306 x => ~ y = y => ~ x. [para(1558(a,1),305(a,1))]. 2307 ~ x => ~ y = y => x # label("(3.12)"). [para(19(a,1),2306(a,1,2)),flip(a)]. 2308 $F # answer("(3.12)"). [resolve(2307,a,47,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 47 given #80 (H,wt=9): 2307 ~ x => ~ y = y => x # label("(3.12)"). [para(19(a,1),2306(a,1,2)),flip(a)]. given #81 (H,wt=17): 297 (x -> y) ^ ((~ y -> ~ x) ^ z) = (x => y) ^ z. [para(32(a,1),7(a,1,1)),flip(a)]. given #82 (H,wt=11): 2429 (x -> y) ^ y = (x => y) ^ y. [para(2218(a,1),297(a,1,2))]. -------- Proof 4 -------- "(3.13)". ============================== PROOF ================================= % Proof 4 at 0.10 (+ 0.00) seconds: "(3.13)". % Length of proof is 45. % Level of proof is 13. % Maximum clause weight is 17. % Given clauses 82. 4 (x => y) ^ y = y # label("(3.13)") # label(non_clause) # label(goal). [goal]. 6 (x v y) v z = x v (y v z) # label("(D1)"). [assumption]. 7 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. 8 x v y = y v x # label("(D3)"). [assumption]. 9 x ^ y = y ^ x # label("(D4)"). [assumption]. 10 x v (x ^ y) = x # label("(D5)"). [assumption]. 11 x ^ (x v y) = x # label("(D6)"). [assumption]. 15 x ^ 1 = x # label("(D10)"). [assumption]. 19 ~ ~ x = x # label("(DN)"). [assumption]. 22 x -> x = 1 # label("(N2)"). [assumption]. 24 x ^ (~ x v y) = x ^ (x -> y) # label("(N4)"). [assumption]. 25 (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)"). [assumption]. 31 x => y = (x -> y) ^ (~ y -> ~ x) # label("(=> def)"). [assumption]. 32 (x -> y) ^ (~ y -> ~ x) = x => y. [copy(31),flip(a)]. 34 1 -> x = x # label("(3.2)"). [assumption]. 37 x -> (x -> y) = x -> y # label("(3.5)"). [assumption]. 38 (x -> y) ^ (z -> y) = (x v z) -> y # label("(3.6)"). [assumption]. 48 (c7 => c8) ^ c8 != c8 # label("(3.13)") # answer("(3.13)"). [deny(4)]. 69 x v (y ^ x) = x. [para(9(a,1),10(a,1,2))]. 74 x ^ (y v x) = x. [para(8(a,1),11(a,1,2))]. 122 1 ^ x = x. [para(15(a,1),9(a,1)),flip(a)]. 213 x ^ (y v ~ x) = x ^ (x -> y). [para(8(a,1),24(a,1,2))]. 243 1 ^ (x -> y) = x -> (x ^ y). [para(22(a,1),25(a,1,1))]. 297 (x -> y) ^ ((~ y -> ~ x) ^ z) = (x => y) ^ z. [para(32(a,1),7(a,1,1)),flip(a)]. 433 x ^ (y -> x) = (1 v y) -> x. [para(34(a,1),38(a,1,1))]. 543 1 v x = 1. [para(122(a,1),10(a,1,2))]. 589 x ^ (y v (z v x)) = x. [para(6(a,1),74(a,1,2))]. 611 x ^ (y v (x v z)) = x. [para(8(a,1),589(a,1,2,2))]. 734 x -> (x ^ y) = x -> y. [para(243(a,1),122(a,1))]. 774 x -> (x ^ (x -> y)) = x -> y. [para(37(a,1),734(a,2))]. 1145 x ^ (y -> x) = 1 -> x. [para(543(a,1),433(a,2,1))]. 1189 x ^ (y -> x) = x. [para(34(a,1),1145(a,2))]. 1215 (x -> y) ^ y = y. [para(1189(a,1),9(a,1)),flip(a)]. 1225 (x -> y) v y = x -> y. [para(1189(a,1),69(a,1,2))]. 1319 x ^ (y -> (x v z)) = x. [para(1225(a,1),611(a,1,2))]. 1535 x -> (x ^ (x -> y)) = x -> (y v ~ x). [para(213(a,1),734(a,1,2))]. 1996 x -> (y v ~ x) = x -> y. [para(1535(a,1),774(a,1))]. 2006 x -> (~ x v y) = x -> y. [para(8(a,1),1996(a,1,2))]. 2133 ~ x ^ (x -> y) = ~ x. [para(2006(a,1),1319(a,1,2))]. 2154 x ^ (~ x -> y) = ~ ~ x. [para(19(a,1),2133(a,1,1))]. 2191 x ^ (~ x -> y) = x. [para(19(a,1),2154(a,2))]. 2218 (~ x -> y) ^ x = x. [para(2191(a,1),9(a,1)),flip(a)]. 2429 (x -> y) ^ y = (x => y) ^ y. [para(2218(a,1),297(a,1,2))]. 2474 (x => y) ^ y = y # label("(3.13)"). [para(2429(a,1),1215(a,1))]. 2475 $F # answer("(3.13)"). [resolve(2474,a,48,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 48 given #83 (H,wt=7): 2474 (x => y) ^ y = y # label("(3.13)"). [para(2429(a,1),1215(a,1))]. given #84 (H,wt=17): 761 (x -> y) ^ (~ (x ^ y) -> ~ x) = x => (x ^ y). [para(734(a,1),32(a,1,1))]. given #85 (H,wt=15): 2614 (x -> y) ^ (~ y -> ~ x) = x => (x ^ y). [para(1040(a,1),761(a,1,2))]. -------- Proof 5 -------- "(3.14)". ============================== PROOF ================================= % Proof 5 at 0.11 (+ 0.01) seconds: "(3.14)". % Length of proof is 20. % Level of proof is 6. % Maximum clause weight is 17. % Given clauses 85. 5 x => (x ^ y) = x => y # label("(3.14)") # label(non_clause) # label(goal). [goal]. 9 x ^ y = y ^ x # label("(D4)"). [assumption]. 15 x ^ 1 = x # label("(D10)"). [assumption]. 17 ~ x v ~ y = ~ (x ^ y) # label("(DM1)"). [assumption]. 22 x -> x = 1 # label("(N2)"). [assumption]. 25 (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)"). [assumption]. 31 x => y = (x -> y) ^ (~ y -> ~ x) # label("(=> def)"). [assumption]. 32 (x -> y) ^ (~ y -> ~ x) = x => y. [copy(31),flip(a)]. 38 (x -> y) ^ (z -> y) = (x v z) -> y # label("(3.6)"). [assumption]. 49 c9 => (c9 ^ c10) != c9 => c10 # label("(3.14)") # answer("(3.14)"). [deny(5)]. 122 1 ^ x = x. [para(15(a,1),9(a,1)),flip(a)]. 243 1 ^ (x -> y) = x -> (x ^ y). [para(22(a,1),25(a,1,1))]. 416 1 ^ (x -> y) = (y v x) -> y. [para(22(a,1),38(a,1,1))]. 734 x -> (x ^ y) = x -> y. [para(243(a,1),122(a,1))]. 761 (x -> y) ^ (~ (x ^ y) -> ~ x) = x => (x ^ y). [para(734(a,1),32(a,1,1))]. 1016 (x v y) -> x = y -> x. [para(416(a,1),122(a,1))]. 1040 ~ (x ^ y) -> ~ x = ~ y -> ~ x. [para(17(a,1),1016(a,1,1))]. 2614 (x -> y) ^ (~ y -> ~ x) = x => (x ^ y). [para(1040(a,1),761(a,1,2))]. 2668 x => (x ^ y) = x => y # label("(3.14)"). [para(2614(a,1),32(a,1))]. 2669 $F # answer("(3.14)"). [resolve(2668,a,49,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=85. Generated=3496. Kept=2656. proofs=5. Usable=86. Sos=2508. Demods=0. Limbo=27, Disabled=75. Hints=61. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=840. Back_subsumed=30. 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=1. Megabytes=3.36. User_CPU=0.11, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED THEOREM PROVED Exiting with 5 proofs. ------ process 32355 exit (max_proofs) ------  Process 32355 exit (max_proofs) Mon Jan 21 11:14:39 2008