============================== Prover9 =============================== Prover9 (64) version 2008-06A, June 2008. Process 23416 was started by veroff on pengy, Tue Jul 8 08:19:41 2008 The command was "prover9 -f 5.1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file 5.1.in op(400,infix,[^,v,"=>",*]). 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). set(hyper_resolution). % set(hyper_resolution) -> set(pos_hyper_resolution). formulas(usable). -P(x => y) | -P(x) | P(y) # label("MP"). end_of_list. formulas(assumptions). P((x => y) => ((y => z) => (x => z))) # label("(A1)"). P((x => (y => z)) => (y => (x => z))) # label("(A2)"). P(x => (y => x)) # label("(A3)"). P(x => (y => (x * y))) # label("(A4)"). P((x => (y => z)) => ((x * y) => z)) # label("(A5)"). P((x ^ y) => x) # label("(A6)"). P((x ^ y) => y) # label("(A7)"). P((x => y) => ((x => z) => (x => (y ^ z)))) # label("(A8)"). P(x => (x v y)) # label("(A9)"). P(y => (x v y)) # label("(A10)"). P((x => z) => ((y => z) => ((x v y) => z))) # label("(A11)"). P(1) # label("(A12)"). P(0 => x) # label("(A13)"). P(A => B). P(B => A). P(C => D). P(D => C). -P((A ^ C) => (B ^ D)) | -P((A v C) => (B v D)). end_of_list. formulas(hints). P((x => y) => ((y => z) => (x => z))). P((x ^ y) => x). P((x ^ y) => y). P((x => y) => ((x => z) => (x => (y ^ z)))). P(x => (x v y)). P(x => (y v x)). P((x => y) => ((z => y) => ((x v z) => y))). P(A => B). P(C => D). P((x => y) => ((x ^ z) => y)). P((x => y) => ((z ^ x) => y)). P((B => x) => (A => x)). P((D => x) => (C => x)). P(A => (B v x)). P((x => (B v y)) => ((A v x) => (B v y))). P(C => (x v D)). P((A ^ x) => B). P(((A ^ x) => y) => ((A ^ x) => (B ^ y))). P((x ^ C) => D). P((A v C) => (B v D)). P((A ^ C) => (B ^ D)). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). -P(x => y) | -P(x) | P(y) # label("MP"). [assumption]. end_of_list. formulas(sos). P((x => y) => ((y => z) => (x => z))) # label("(A1)"). [assumption]. P((x => (y => z)) => (y => (x => z))) # label("(A2)"). [assumption]. P(x => (y => x)) # label("(A3)"). [assumption]. P(x => (y => (x * y))) # label("(A4)"). [assumption]. P((x => (y => z)) => ((x * y) => z)) # label("(A5)"). [assumption]. P((x ^ y) => x) # label("(A6)"). [assumption]. P((x ^ y) => y) # label("(A7)"). [assumption]. P((x => y) => ((x => z) => (x => (y ^ z)))) # label("(A8)"). [assumption]. P(x => (x v y)) # label("(A9)"). [assumption]. P(x => (y v x)) # label("(A10)"). [assumption]. P((x => y) => ((z => y) => ((x v z) => y))) # label("(A11)"). [assumption]. P(1) # label("(A12)"). [assumption]. P(0 => x) # label("(A13)"). [assumption]. P(A => B). [assumption]. P(B => A). [assumption]. P(C => D). [assumption]. P(D => C). [assumption]. -P((A ^ C) => (B ^ D)) | -P((A v C) => (B v D)). [assumption]. end_of_list. formulas(demodulators). end_of_list. % 21 hints input. Term ordering decisions: Predicate symbol precedence: predicate_order([ P ]). Function symbol precedence: function_order([ A, B, C, D, 0, 1, =>, ^, v, * ]). After inverse_order: (no changes). kept: 2 P((x => y) => ((y => z) => (x => z))) # label("(A1)"). [assumption]. kept: 3 P((x => (y => z)) => (y => (x => z))) # label("(A2)"). [assumption]. kept: 4 P(x => (y => x)) # label("(A3)"). [assumption]. kept: 5 P(x => (y => (x * y))) # label("(A4)"). [assumption]. kept: 6 P((x => (y => z)) => ((x * y) => z)) # label("(A5)"). [assumption]. kept: 7 P((x ^ y) => x) # label("(A6)"). [assumption]. kept: 8 P((x ^ y) => y) # label("(A7)"). [assumption]. kept: 9 P((x => y) => ((x => z) => (x => (y ^ z)))) # label("(A8)"). [assumption]. kept: 10 P(x => (x v y)) # label("(A9)"). [assumption]. kept: 11 P(x => (y v x)) # label("(A10)"). [assumption]. kept: 12 P((x => y) => ((z => y) => ((x v z) => y))) # label("(A11)"). [assumption]. kept: 13 P(1) # label("(A12)"). [assumption]. kept: 14 P(0 => x) # label("(A13)"). [assumption]. kept: 15 P(A => B). [assumption]. kept: 16 P(B => A). [assumption]. kept: 17 P(C => D). [assumption]. kept: 18 P(D => C). [assumption]. kept: 19 -P((A ^ C) => (B ^ D)) | -P((A v C) => (B v D)). [assumption]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 1 -P(x => y) | -P(x) | P(y) # label("MP"). [assumption]. end_of_list. formulas(sos). 2 P((x => y) => ((y => z) => (x => z))) # label("(A1)"). [assumption]. 3 P((x => (y => z)) => (y => (x => z))) # label("(A2)"). [assumption]. 4 P(x => (y => x)) # label("(A3)"). [assumption]. 5 P(x => (y => (x * y))) # label("(A4)"). [assumption]. 6 P((x => (y => z)) => ((x * y) => z)) # label("(A5)"). [assumption]. 7 P((x ^ y) => x) # label("(A6)"). [assumption]. 8 P((x ^ y) => y) # label("(A7)"). [assumption]. 9 P((x => y) => ((x => z) => (x => (y ^ z)))) # label("(A8)"). [assumption]. 10 P(x => (x v y)) # label("(A9)"). [assumption]. 11 P(x => (y v x)) # label("(A10)"). [assumption]. 12 P((x => y) => ((z => y) => ((x v z) => y))) # label("(A11)"). [assumption]. 13 P(1) # label("(A12)"). [assumption]. 14 P(0 => x) # label("(A13)"). [assumption]. 15 P(A => B). [assumption]. 16 P(B => A). [assumption]. 17 P(C => D). [assumption]. 18 P(D => C). [assumption]. 19 -P((A ^ C) => (B ^ D)) | -P((A v C) => (B v D)). [assumption]. end_of_list. formulas(demodulators). end_of_list. % 21 hints processed (0 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.02 seconds. given #1 (I,wt=12): 2 P((x => y) => ((y => z) => (x => z))) # label("(A1)"). [assumption]. given #2 (I,wt=12): 3 P((x => (y => z)) => (y => (x => z))) # label("(A2)"). [assumption]. given #3 (I,wt=6): 4 P(x => (y => x)) # label("(A3)"). [assumption]. given #4 (I,wt=8): 5 P(x => (y => (x * y))) # label("(A4)"). [assumption]. given #5 (I,wt=12): 6 P((x => (y => z)) => ((x * y) => z)) # label("(A5)"). [assumption]. given #6 (I,wt=6): 7 P((x ^ y) => x) # label("(A6)"). [assumption]. given #7 (I,wt=6): 8 P((x ^ y) => y) # label("(A7)"). [assumption]. given #8 (I,wt=14): 9 P((x => y) => ((x => z) => (x => (y ^ z)))) # label("(A8)"). [assumption]. given #9 (I,wt=6): 10 P(x => (x v y)) # label("(A9)"). [assumption]. given #10 (I,wt=6): 11 P(x => (y v x)) # label("(A10)"). [assumption]. given #11 (I,wt=14): 12 P((x => y) => ((z => y) => ((x v z) => y))) # label("(A11)"). [assumption]. given #12 (I,wt=2): 13 P(1) # label("(A12)"). [assumption]. given #13 (I,wt=4): 14 P(0 => x) # label("(A13)"). [assumption]. given #14 (I,wt=4): 15 P(A => B). [assumption]. given #15 (I,wt=4): 16 P(B => A). [assumption]. given #16 (I,wt=4): 17 P(C => D). [assumption]. given #17 (I,wt=4): 18 P(D => C). [assumption]. given #18 (I,wt=16): 19 -P((A ^ C) => (B ^ D)) | -P((A v C) => (B v D)). [assumption]. given #19 (H,wt=8): 132 P((B => x) => (A => x)). [hyper(1,a,2,a,b,15,a)]. given #20 (H,wt=6): 165 P(A => (B v x)). [hyper(1,a,132,a,b,10,a)]. given #21 (H,wt=8): 146 P((D => x) => (C => x)). [hyper(1,a,2,a,b,17,a)]. given #22 (H,wt=6): 185 P(C => (x v D)). [hyper(1,a,146,a,b,11,a)]. given #23 (H,wt=10): 49 P((x => y) => ((x ^ z) => y)). [hyper(1,a,2,a,b,7,a)]. given #24 (H,wt=6): 213 P((A ^ x) => B). [hyper(1,a,49,a,b,15,a)]. given #25 (H,wt=10): 54 P((x => y) => ((z ^ x) => y)). [hyper(1,a,2,a,b,8,a)]. given #26 (H,wt=6): 252 P((x ^ C) => D). [hyper(1,a,54,a,b,17,a)]. given #27 (H,wt=14): 168 P((x => (B v y)) => ((A v x) => (B v y))). [hyper(1,a,12,a,b,165,a)]. given #28 (H,wt=8): 287 P((A v C) => (B v D)). [hyper(1,a,168,a,b,185,a)]. given #29 (H,wt=14): 230 P(((A ^ x) => y) => ((A ^ x) => (B ^ y))). [hyper(1,a,9,a,b,213,a)]. given #30 (H,wt=8): 315 P((A ^ C) => (B ^ D)). [hyper(1,a,230,a,b,252,a)]. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.03 (+ 0.01) seconds. % Length of proof is 24. % Level of proof is 5. % Maximum clause weight is 16. % Given clauses 30. 1 -P(x => y) | -P(x) | P(y) # label("MP"). [assumption]. 2 P((x => y) => ((y => z) => (x => z))) # label("(A1)"). [assumption]. 7 P((x ^ y) => x) # label("(A6)"). [assumption]. 8 P((x ^ y) => y) # label("(A7)"). [assumption]. 9 P((x => y) => ((x => z) => (x => (y ^ z)))) # label("(A8)"). [assumption]. 10 P(x => (x v y)) # label("(A9)"). [assumption]. 11 P(x => (y v x)) # label("(A10)"). [assumption]. 12 P((x => y) => ((z => y) => ((x v z) => y))) # label("(A11)"). [assumption]. 15 P(A => B). [assumption]. 17 P(C => D). [assumption]. 19 -P((A ^ C) => (B ^ D)) | -P((A v C) => (B v D)). [assumption]. 49 P((x => y) => ((x ^ z) => y)). [hyper(1,a,2,a,b,7,a)]. 54 P((x => y) => ((z ^ x) => y)). [hyper(1,a,2,a,b,8,a)]. 132 P((B => x) => (A => x)). [hyper(1,a,2,a,b,15,a)]. 146 P((D => x) => (C => x)). [hyper(1,a,2,a,b,17,a)]. 165 P(A => (B v x)). [hyper(1,a,132,a,b,10,a)]. 168 P((x => (B v y)) => ((A v x) => (B v y))). [hyper(1,a,12,a,b,165,a)]. 185 P(C => (x v D)). [hyper(1,a,146,a,b,11,a)]. 213 P((A ^ x) => B). [hyper(1,a,49,a,b,15,a)]. 230 P(((A ^ x) => y) => ((A ^ x) => (B ^ y))). [hyper(1,a,9,a,b,213,a)]. 252 P((x ^ C) => D). [hyper(1,a,54,a,b,17,a)]. 287 P((A v C) => (B v D)). [hyper(1,a,168,a,b,185,a)]. 315 P((A ^ C) => (B ^ D)). [hyper(1,a,230,a,b,252,a)]. 323 $F. [hyper(19,a,315,a,b,287,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=30. Generated=335. Kept=321. proofs=1. Usable=31. Sos=290. Demods=0. Limbo=0, Disabled=19. Hints=21. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=13. Back_subsumed=1. 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=0.63. User_CPU=0.03, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED THEOREM PROVED Exiting with 1 proof. ------ process 23416 exit (max_proofs) ------  Process 23416 exit (max_proofs) Tue Jul 8 08:19:45 2008