============================== Prover9 =============================== Prover9 (64) version 2008-06A, June 2008. Process 23428 was started by veroff on pengy, Tue Jul 8 08:19:51 2008 The command was "prover9 -f 5.5.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file 5.5.in clear(auto). % clear(auto) -> clear(auto_inference). % clear(auto) -> clear(auto_setup). % clear(auto_setup) -> clear(predicate_elim). % clear(auto_setup) -> 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(para_units_only). % set(para_units_only) -> assign(para_lit_limit, 1). set(para_from_small). 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 => y) => ((y => z) => (x => z)) = 1 # label("(BCK1)"). 1 => x = x # label("(BCK2)"). x => 1 = 1 # label("(BCK3)"). x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). x * 1 = x # label("(M1)"). x * y = y * x # label("(M2)"). (x * y) * z = x * (y * z) # label("(M3)"). (x * y) => z = x => (y => z) # label("(P)"). x ^ 1 = x # label("(D10)"). x ^ ((x => y) => y) = x # label("(3.7)"). (x ^ y) => y = 1 # label("(3.11)"). x v 0 = x # label("(D9)"). ~ x = x => 0 # label("(~ def)"). x => (x => (x => y)) = x => (x => y) # label("(E_2)"). (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). ~ ~ x = x # label("(DN)"). ((x => (x => y)) ^ (~ y => (~ y => ~ x))) => (x => y) = 1 # label("(5.6)"). (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')"). x => ((x => y) => y) = 1 # label("(BCK5)"). x => x = 1 # label("(3.16)"). x => (y => x) = 1 # label("(3.17)"). x => (y => z) = y => (x => z) # label("(3.18)"). (x * y) v (x * z) = x * (y v z) # label("(4.1)"). (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). (x * (x => y)) v y = y # label("(4.3)"). (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). ((x => y) * z) => (x => (y * z)) = 1 # label("(4.5)"). end_of_list. formulas(goals). (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y # label("N"). end_of_list. formulas(hints). (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y. x v y = y v x. x * 1 = x. ~ x = x => 0. x => 0 = ~ x. ~ ~ x = x. ((x => (x => y)) ^ (~ y => (~ y => ~ x))) => (x => y) = 1. x => (y => x) = 1. x => (y => z) = y => (x => z). (x => y) ^ (x => z) = x => (y ^ z). (x * (x => y)) v y = y. (x => y) ^ (z => y) = (x v z) => y. x => ~ y = y => (x => 0). x => (y => 0) = y => ~ x. x => (((x => (x => y)) ^ (~ y => (~ y => ~ x))) => y) = 1. x = x v (y * (y => x)). x v (y * (y => x)) = x. (x => y) v (y * 1) = x => y. (x => y) v (z * (x => (z => y))) = x => y. x => ~ y = y => ~ x. x => y = ~ y => ~ x. ~ x => ~ y = y => x. (x => y) v y = x => y. x => y = y v (x => y). x v (y => x) = y => x. (x => y) v (x => (z => y)) = z => (x => y). x => (((x => (x => y)) ^ (~ y => (x => y))) => y) = 1. x => (((x => (x => y)) ^ (x => (~ y => y))) => y) = 1. x => ((x => ((x => y) ^ (~ y => y))) => y) = 1. x => ((x => ((x v ~ y) => y)) => y) = 1. (x => y) v ((x => ((x v ~ y) => y)) * 1) = x => y. (x => y) v (x => ((x v ~ y) => y)) = x => y. x => y = (x v ~ y) => (x => y). (x v ~ y) => (x => y) = x => y. (x => (x => y)) ^ (~ y => (x => y)) = x => y. end_of_list. WARNING, function symbols in function_order (lex) command not found in formulas: ->. WARNING, function symbols in function_order (lex) command not found in formulas: ->. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y # label("N") # 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 => y) => ((y => z) => (x => z)) = 1 # label("(BCK1)"). [assumption]. 1 => x = x # label("(BCK2)"). [assumption]. x => 1 = 1 # label("(BCK3)"). [assumption]. x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). [assumption]. x * 1 = x # label("(M1)"). [assumption]. x * y = y * x # label("(M2)"). [assumption]. (x * y) * z = x * (y * z) # label("(M3)"). [assumption]. (x * y) => z = x => (y => z) # label("(P)"). [assumption]. x ^ 1 = x # label("(D10)"). [assumption]. x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. (x ^ y) => y = 1 # label("(3.11)"). [assumption]. x v 0 = x # label("(D9)"). [assumption]. ~ x = x => 0 # label("(~ def)"). [assumption]. x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [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 = x # label("(DN)"). [assumption]. ((x => (x => y)) ^ (~ y => (~ y => ~ x))) => (x => y) = 1 # label("(5.6)"). [assumption]. (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')"). [assumption]. x => ((x => y) => y) = 1 # label("(BCK5)"). [assumption]. x => x = 1 # label("(3.16)"). [assumption]. x => (y => x) = 1 # label("(3.17)"). [assumption]. x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. (x * y) v (x * z) = x * (y v z) # label("(4.1)"). [assumption]. (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). [assumption]. (x * (x => y)) v y = y # label("(4.3)"). [assumption]. (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. ((x => y) * z) => (x => (y * z)) = 1 # label("(4.5)"). [assumption]. c1 => c2 != (c1 => (c1 => c2)) ^ (~ c2 => (~ c2 => ~ c1)) # label("N"). [deny(1)]. end_of_list. formulas(demodulators). end_of_list. % 35 hints input. Auto_denials: % copying label "N" to answer in negative clause Term ordering decisions: Function symbol KB weights: 0=1. 1=1. c1=1. c2=1. *=1. ^=1. =>=1. v=1. ~=1. Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ 0, 1, c1, c2, *, ^, =>, v, ~ ]). Skipping inverse_order, because there is a function_order (lex) command. kept: 2 (x v y) v z = x v (y v z) # label("(D1)"). [assumption]. kept: 3 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. % Operation v is commutative; C redundancy checks enabled. kept: 4 x v y = y v x # label("(D3)"). [assumption]. % Operation ^ is commutative; C redundancy checks enabled. kept: 5 x ^ y = y ^ x # label("(D4)"). [assumption]. kept: 6 x v (x ^ y) = x # label("(D5)"). [assumption]. kept: 7 x ^ (x v y) = x # label("(D6)"). [assumption]. kept: 8 (x => y) => ((y => z) => (x => z)) = 1 # label("(BCK1)"). [assumption]. kept: 9 1 => x = x # label("(BCK2)"). [assumption]. kept: 10 x => 1 = 1 # label("(BCK3)"). [assumption]. kept: 11 x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). [assumption]. kept: 12 x * 1 = x # label("(M1)"). [assumption]. % Operation * is commutative; C redundancy checks enabled. kept: 13 x * y = y * x # label("(M2)"). [assumption]. kept: 14 (x * y) * z = x * (y * z) # label("(M3)"). [assumption]. kept: 15 (x * y) => z = x => (y => z) # label("(P)"). [assumption]. kept: 16 x ^ 1 = x # label("(D10)"). [assumption]. kept: 17 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. kept: 18 (x ^ y) => y = 1 # label("(3.11)"). [assumption]. kept: 19 x v 0 = x # label("(D9)"). [assumption]. 20 ~ x = x => 0 # label("(~ def)"). [assumption]. kept: 21 x => 0 = ~ x. [copy(20),flip(a)]. kept: 22 x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [assumption]. kept: 23 (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). [assumption]. kept: 24 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). [assumption]. kept: 25 ~ ~ x = x # label("(DN)"). [assumption]. kept: 26 ((x => (x => y)) ^ (~ y => (~ y => ~ x))) => (x => y) = 1 # label("(5.6)"). [assumption]. kept: 27 (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')"). [assumption]. kept: 28 x => ((x => y) => y) = 1 # label("(BCK5)"). [assumption]. kept: 29 x => x = 1 # label("(3.16)"). [assumption]. kept: 30 x => (y => x) = 1 # label("(3.17)"). [assumption]. kept: 31 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. kept: 32 (x * y) v (x * z) = x * (y v z) # label("(4.1)"). [assumption]. kept: 33 (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). [assumption]. kept: 34 (x * (x => y)) v y = y # label("(4.3)"). [assumption]. kept: 35 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. kept: 36 ((x => y) * z) => (x => (y * z)) = 1 # label("(4.5)"). [assumption]. 37 c1 => c2 != (c1 => (c1 => c2)) ^ (~ c2 => (~ c2 => ~ c1)) # label("N") # answer("N"). [deny(1)]. kept: 38 (c1 => (c1 => c2)) ^ (~ c2 => (~ c2 => ~ c1)) != c1 => c2 # answer("N"). [copy(37),flip(a)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 38 (c1 => (c1 => c2)) ^ (~ c2 => (~ c2 => ~ c1)) != c1 => c2 # answer("N"). [copy(37),flip(a)]. end_of_list. formulas(sos). 2 (x v y) v z = x v (y v z) # label("(D1)"). [assumption]. 3 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. 4 x v y = y v x # label("(D3)"). [assumption]. 5 x ^ y = y ^ x # label("(D4)"). [assumption]. 6 x v (x ^ y) = x # label("(D5)"). [assumption]. 7 x ^ (x v y) = x # label("(D6)"). [assumption]. 8 (x => y) => ((y => z) => (x => z)) = 1 # label("(BCK1)"). [assumption]. 9 1 => x = x # label("(BCK2)"). [assumption]. 10 x => 1 = 1 # label("(BCK3)"). [assumption]. 11 x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). [assumption]. 12 x * 1 = x # label("(M1)"). [assumption]. 13 x * y = y * x # label("(M2)"). [assumption]. 14 (x * y) * z = x * (y * z) # label("(M3)"). [assumption]. 15 (x * y) => z = x => (y => z) # label("(P)"). [assumption]. 16 x ^ 1 = x # label("(D10)"). [assumption]. 17 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. 18 (x ^ y) => y = 1 # label("(3.11)"). [assumption]. 19 x v 0 = x # label("(D9)"). [assumption]. 21 x => 0 = ~ x. [copy(20),flip(a)]. 22 x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [assumption]. 23 (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). [assumption]. 24 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). [assumption]. 25 ~ ~ x = x # label("(DN)"). [assumption]. 26 ((x => (x => y)) ^ (~ y => (~ y => ~ x))) => (x => y) = 1 # label("(5.6)"). [assumption]. 27 (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')"). [assumption]. 28 x => ((x => y) => y) = 1 # label("(BCK5)"). [assumption]. 29 x => x = 1 # label("(3.16)"). [assumption]. 30 x => (y => x) = 1 # label("(3.17)"). [assumption]. 31 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. 32 (x * y) v (x * z) = x * (y v z) # label("(4.1)"). [assumption]. 33 (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). [assumption]. 34 (x * (x => y)) v y = y # label("(4.3)"). [assumption]. 35 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. 36 ((x => y) * z) => (x => (y * z)) = 1 # label("(4.5)"). [assumption]. end_of_list. formulas(demodulators). end_of_list. % 35 hints processed (6 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.02 seconds. given #1 (I,wt=11): 2 (x v y) v z = x v (y v z) # label("(D1)"). [assumption]. given #2 (I,wt=11): 3 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. given #3 (I,wt=7): 4 x v y = y v x # label("(D3)"). [assumption]. given #4 (I,wt=7): 5 x ^ y = y ^ x # label("(D4)"). [assumption]. given #5 (I,wt=7): 6 x v (x ^ y) = x # label("(D5)"). [assumption]. given #6 (I,wt=7): 7 x ^ (x v y) = x # label("(D6)"). [assumption]. given #7 (I,wt=13): 8 (x => y) => ((y => z) => (x => z)) = 1 # label("(BCK1)"). [assumption]. given #8 (I,wt=5): 9 1 => x = x # label("(BCK2)"). [assumption]. given #9 (I,wt=5): 10 x => 1 = 1 # label("(BCK3)"). [assumption]. given #10 (I,wt=13): 11 x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). [assumption]. given #11 (I,wt=5): 12 x * 1 = x # label("(M1)"). [assumption]. given #12 (I,wt=7): 13 x * y = y * x # label("(M2)"). [assumption]. given #13 (I,wt=11): 14 (x * y) * z = x * (y * z) # label("(M3)"). [assumption]. given #14 (I,wt=11): 15 (x * y) => z = x => (y => z) # label("(P)"). [assumption]. given #15 (I,wt=5): 16 x ^ 1 = x # label("(D10)"). [assumption]. given #16 (I,wt=9): 17 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. given #17 (I,wt=7): 18 (x ^ y) => y = 1 # label("(3.11)"). [assumption]. given #18 (I,wt=5): 19 x v 0 = x # label("(D9)"). [assumption]. given #19 (I,wt=6): 21 x => 0 = ~ x. [copy(20),flip(a)]. given #20 (I,wt=13): 22 x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [assumption]. given #21 (I,wt=13): 23 (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). [assumption]. given #22 (I,wt=13): 24 (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). [assumption]. given #23 (I,wt=5): 25 ~ ~ x = x # label("(DN)"). [assumption]. given #24 (I,wt=20): 26 ((x => (x => y)) ^ (~ y => (~ y => ~ x))) => (x => y) = 1 # label("(5.6)"). [assumption]. given #25 (I,wt=13): 27 (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')"). [assumption]. given #26 (I,wt=9): 28 x => ((x => y) => y) = 1 # label("(BCK5)"). [assumption]. given #27 (I,wt=5): 29 x => x = 1 # label("(3.16)"). [assumption]. given #28 (I,wt=7): 30 x => (y => x) = 1 # label("(3.17)"). [assumption]. given #29 (I,wt=11): 31 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. given #30 (I,wt=13): 32 (x * y) v (x * z) = x * (y v z) # label("(4.1)"). [assumption]. given #31 (I,wt=13): 33 (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). [assumption]. given #32 (I,wt=9): 34 (x * (x => y)) v y = y # label("(4.3)"). [assumption]. given #33 (I,wt=13): 35 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. given #34 (I,wt=13): 36 ((x => y) * z) => (x => (y * z)) = 1 # label("(4.5)"). [assumption]. given #35 (H,wt=9): 1137 x v (y * (y => x)) = x. [para(34(a,1),4(a,1)),flip(a)]. given #36 (H,wt=10): 959 x => (y => 0) = y => ~ x. [para(21(a,1),31(a,1,2)),flip(a)]. given #37 (H,wt=9): 1691 x => ~ y = y => ~ x. [para(21(a,1),959(a,1,2))]. given #38 (H,wt=9): 1766 ~ x => ~ y = y => x. [para(25(a,1),1691(a,1,2)),flip(a)]. given #39 (H,wt=11): 1609 (x => y) v (y * 1) = x => y. [para(30(a,1),1137(a,1,2,2))]. given #40 (H,wt=9): 1912 (x => y) v y = x => y. [para(12(a,1),1609(a,1,2))]. given #41 (H,wt=9): 2020 x v (y => x) = y => x. [para(1912(a,1),4(a,1)),flip(a)]. given #42 (H,wt=15): 1612 (x => y) v (z * (x => (z => y))) = x => y. [para(31(a,1),1137(a,1,2,2))]. given #43 (H,wt=15): 2181 (x => y) v (x => (z => y)) = z => (x => y). [para(31(a,1),2020(a,1,2))]. given #44 (H,wt=20): 967 x => (((x => (x => y)) ^ (~ y => (~ y => ~ x))) => y) = 1. [para(31(a,1),26(a,1))]. given #45 (H,wt=18): 2752 x => (((x => (x => y)) ^ (~ y => (x => y))) => y) = 1. [para(1766(a,1),967(a,1,2,1,2,2))]. given #46 (H,wt=18): 2911 x => (((x => (x => y)) ^ (x => (~ y => y))) => y) = 1. [para(31(a,1),2752(a,1,2,1,2))]. given #47 (H,wt=16): 3122 x => ((x => ((x => y) ^ (~ y => y))) => y) = 1. [para(33(a,1),2911(a,1,2,1))]. given #48 (H,wt=14): 3330 x => ((x => ((x v ~ y) => y)) => y) = 1. [para(35(a,1),3122(a,1,2,1,2))]. given #49 (H,wt=18): 3539 (x => y) v ((x => ((x v ~ y) => y)) * 1) = x => y. [para(3330(a,1),1612(a,1,2,2))]. given #50 (H,wt=16): 3602 (x => y) v (x => ((x v ~ y) => y)) = x => y. [para(12(a,1),3539(a,1,2))]. given #51 (H,wt=12): 3999 (x v ~ y) => (x => y) = x => y. [para(3602(a,1),2181(a,1)),flip(a)]. given #52 (H,wt=16): 4142 (x => (x => y)) ^ (~ y => (x => y)) = x => y. [para(3999(a,1),35(a,2))]. -------- Proof 1 -------- "N". ============================== PROOF ================================= % Proof 1 at 0.17 (+ 0.01) seconds: "N". % Length of proof is 34. % Level of proof is 14. % Maximum clause weight is 20. % Given clauses 52. 1 (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y # label("N") # label(non_clause) # label(goal). [goal]. 4 x v y = y v x # label("(D3)"). [assumption]. 12 x * 1 = x # label("(M1)"). [assumption]. 20 ~ x = x => 0 # label("(~ def)"). [assumption]. 21 x => 0 = ~ x. [copy(20),flip(a)]. 25 ~ ~ x = x # label("(DN)"). [assumption]. 26 ((x => (x => y)) ^ (~ y => (~ y => ~ x))) => (x => y) = 1 # label("(5.6)"). [assumption]. 30 x => (y => x) = 1 # label("(3.17)"). [assumption]. 31 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. 33 (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). [assumption]. 34 (x * (x => y)) v y = y # label("(4.3)"). [assumption]. 35 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. 37 c1 => c2 != (c1 => (c1 => c2)) ^ (~ c2 => (~ c2 => ~ c1)) # label("N") # answer("N"). [deny(1)]. 38 (c1 => (c1 => c2)) ^ (~ c2 => (~ c2 => ~ c1)) != c1 => c2 # answer("N"). [copy(37),flip(a)]. 959 x => (y => 0) = y => ~ x. [para(21(a,1),31(a,1,2)),flip(a)]. 967 x => (((x => (x => y)) ^ (~ y => (~ y => ~ x))) => y) = 1. [para(31(a,1),26(a,1))]. 1137 x v (y * (y => x)) = x. [para(34(a,1),4(a,1)),flip(a)]. 1609 (x => y) v (y * 1) = x => y. [para(30(a,1),1137(a,1,2,2))]. 1612 (x => y) v (z * (x => (z => y))) = x => y. [para(31(a,1),1137(a,1,2,2))]. 1691 x => ~ y = y => ~ x. [para(21(a,1),959(a,1,2))]. 1766 ~ x => ~ y = y => x. [para(25(a,1),1691(a,1,2)),flip(a)]. 1912 (x => y) v y = x => y. [para(12(a,1),1609(a,1,2))]. 2020 x v (y => x) = y => x. [para(1912(a,1),4(a,1)),flip(a)]. 2181 (x => y) v (x => (z => y)) = z => (x => y). [para(31(a,1),2020(a,1,2))]. 2752 x => (((x => (x => y)) ^ (~ y => (x => y))) => y) = 1. [para(1766(a,1),967(a,1,2,1,2,2))]. 2911 x => (((x => (x => y)) ^ (x => (~ y => y))) => y) = 1. [para(31(a,1),2752(a,1,2,1,2))]. 3122 x => ((x => ((x => y) ^ (~ y => y))) => y) = 1. [para(33(a,1),2911(a,1,2,1))]. 3330 x => ((x => ((x v ~ y) => y)) => y) = 1. [para(35(a,1),3122(a,1,2,1,2))]. 3539 (x => y) v ((x => ((x v ~ y) => y)) * 1) = x => y. [para(3330(a,1),1612(a,1,2,2))]. 3602 (x => y) v (x => ((x v ~ y) => y)) = x => y. [para(12(a,1),3539(a,1,2))]. 3999 (x v ~ y) => (x => y) = x => y. [para(3602(a,1),2181(a,1)),flip(a)]. 4142 (x => (x => y)) ^ (~ y => (x => y)) = x => y. [para(3999(a,1),35(a,2))]. 4417 (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y. [para(1766(a,2),4142(a,1,2,2))]. 4418 $F # answer("N"). [resolve(4417,a,38,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=52. Generated=5321. Kept=4414. proofs=1. Usable=53. Sos=4153. Demods=0. Limbo=168, Disabled=74. Hints=35. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=907. Back_subsumed=39. 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=6.80. User_CPU=0.17, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED THEOREM PROVED Exiting with 1 proof. ------ process 23428 exit (max_proofs) ------  Process 23428 exit (max_proofs) Tue Jul 8 08:19:54 2008