============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13073 was started by mccune on cleo.thornwood, Mon Jun 19 16:41:11 2006 The command was "/home/mccune/bin/prover9 -f steam.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file steam.in formulas(sos). (all x (Wolf(x) -> animal(x))). (all x (Fox(x) -> animal(x))). (all x (Bird(x) -> animal(x))). (all x (Caterpillar(x) -> animal(x))). (all x (Snail(x) -> animal(x))). (all x (Grain(x) -> plant(x))). (exists x (Wolf(x))). (exists x (Fox(x))). (exists x (Bird(x))). (exists x (Caterpillar(x))). (exists x (Snail(x))). (exists x (Grain(x))). (all x (animal(x) -> (all y (plant(y) -> eats(x,y))) | (all z (animal(z) & Smaller(z,x) & (exists u (plant(u) & eats(z,u))) -> eats(x,z))))). (all x all y (Caterpillar(x) & Bird(y) -> Smaller(x,y))). (all x all y (Snail(x) & Bird(y) -> Smaller(x,y))). (all x all y (Bird(x) & Fox(y) -> Smaller(x,y))). (all x all y (Fox(x) & Wolf(y) -> Smaller(x,y))). (all x all y (Bird(x) & Caterpillar(y) -> eats(x,y))). (all x (Caterpillar(x) -> (exists y (plant(y) & eats(x,y))))). (all x (Snail(x) -> (exists y (plant(y) & eats(x,y))))). (all x all y (Wolf(x) & Fox(y) -> - eats(x,y))). (all x all y (Wolf(x) & Grain(y) -> - eats(x,y))). (all x all y (Bird(x) & Snail(y) -> - eats(x,y))). end_of_list. formulas(goals). (exists x exists y (animal(x) & animal(y) & eats(x,y) & (all z (Grain(z) -> eats(y,z))))). end_of_list. ============================== end of input ========================== ============================== PROCESS GOALS ========================= % Each goal formula was negated; the result (to be placed in sos): clauses(negated_goals). - animal(x) | - animal(y) | - eats(x,y) | Grain(f3(x,y)). - animal(x) | - animal(y) | - eats(x,y) | - eats(y,f3(x,y)). end_of_list. ============================== end of process goals ================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 - Wolf(x) | animal(x). [clausify]. 2 - Fox(x) | animal(x). [clausify]. 3 - Bird(x) | animal(x). [clausify]. 4 - Caterpillar(x) | animal(x). [clausify]. 5 - Snail(x) | animal(x). [clausify]. 6 - Grain(x) | plant(x). [clausify]. 7 Wolf(c1). [clausify]. 8 Fox(c2). [clausify]. 9 Bird(c3). [clausify]. 10 Caterpillar(c4). [clausify]. 11 Snail(c5). [clausify]. 12 Grain(c6). [clausify]. 13 - animal(x) | - plant(y) | eats(x,y) | - animal(z) | - Smaller(z,x) | - plant(u) | - eats(z,u) | eats(x,z). [clausify]. 14 - Caterpillar(x) | - Bird(y) | Smaller(x,y). [clausify]. 15 - Snail(x) | - Bird(y) | Smaller(x,y). [clausify]. 16 - Bird(x) | - Fox(y) | Smaller(x,y). [clausify]. 17 - Fox(x) | - Wolf(y) | Smaller(x,y). [clausify]. 18 - Bird(x) | - Caterpillar(y) | eats(x,y). [clausify]. 19 - Caterpillar(x) | plant(f1(x)). [clausify]. 20 - Caterpillar(x) | eats(x,f1(x)). [clausify]. 21 - Snail(x) | plant(f2(x)). [clausify]. 22 - Snail(x) | eats(x,f2(x)). [clausify]. 23 - Wolf(x) | - Fox(y) | - eats(x,y). [clausify]. 24 - Wolf(x) | - Grain(y) | - eats(x,y). [clausify]. 25 - Bird(x) | - Snail(y) | - eats(x,y). [clausify]. 26 - animal(x) | - animal(y) | - eats(x,y) | Grain(f3(x,y)). [clausify]. 27 - animal(x) | - animal(y) | - eats(x,y) | - eats(y,f3(x,y)). [clausify]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: Wolf/1 Fox/1 Bird/1 Caterpillar/1 Snail/1 Grain/1 Smaller/2. Auto_denials: no changes. Term ordering decisions: Relation symbol precedence: lex([ animal, plant, eats, Smaller, Grain, Snail, Caterpillar, Bird, Fox, Wolf ]). Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, f3, f1, f2 ]). After inverse_order: Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, f3, f1, f2 ]). Unfolding symbols: (none). Auto_inference settings: % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(back_unit_deletion). % (non-Horn) % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 60 - animal(x) | - animal(y) | - eats(x,y) | - eats(y,f3(x,y)). [clausify]. 61 animal(c1). [resolve(7,a,1,a)]. 62 animal(c2). [resolve(8,a,2,a)]. 63 - eats(c1,c2). [resolve(30,a,8,a)]. 64 animal(c3). [resolve(9,a,3,a)]. 65 animal(c4). [resolve(10,a,4,a)]. 66 plant(f1(c4)). [resolve(19,a,10,a)]. 67 eats(c4,f1(c4)). [resolve(20,a,10,a)]. 68 eats(c3,c4). [resolve(39,a,10,a)]. 69 animal(c5). [resolve(11,a,5,a)]. 70 plant(f2(c5)). [resolve(21,a,11,a)]. 71 eats(c5,f2(c5)). [resolve(22,a,11,a)]. 72 - eats(c3,c5). [resolve(40,a,11,a)]. 73 plant(c6). [resolve(12,a,6,a)]. 74 - animal(x) | - animal(y) | - eats(x,y) | plant(f3(x,y)). [resolve(26,d,6,a)]. 75 - eats(c1,c6). [resolve(31,a,12,a)]. 76 - eats(c1,f3(x,y)) | - animal(x) | - animal(y) | - eats(x,y). [resolve(31,a,26,d)]. 77 - plant(x) | eats(c1,x) | - plant(y) | - eats(c2,y). [copy(56),unit_del(a,61),unit_del(d,62),unit_del(g,63)]. 78 - plant(x) | eats(c2,x) | - plant(y) | - eats(c3,y) | eats(c2,c3). [copy(57),unit_del(a,62),unit_del(d,64)]. 79 - plant(x) | eats(c3,x) | - plant(y) | - eats(c5,y). [copy(59),unit_del(a,64),unit_del(d,69),unit_del(g,72)]. 80 - animal(x) | - eats(x,x) | - eats(x,f3(x,x)). [factor(60,a,b)]. 81 - animal(x) | - eats(x,x) | plant(f3(x,x)). [factor(74,a,b)]. 82 - eats(c1,f3(x,x)) | - animal(x) | - eats(x,x). [factor(76,b,c)]. 83 - plant(x) | eats(c1,x) | - eats(c2,x). [factor(77,a,c)]. 84 - plant(x) | eats(c2,x) | - eats(c3,x) | eats(c2,c3). [factor(78,a,c)]. 85 - plant(c3) | eats(c2,c3) | - plant(x) | - eats(c3,x). [factor(78,b,e)]. 86 - plant(x) | eats(c3,x) | - eats(c5,x). [factor(79,a,c)]. 87 - plant(c3) | eats(c2,c3) | - eats(c3,c3). [factor(84,b,d)]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=12): 60 - animal(x) | - animal(y) | - eats(x,y) | - eats(y,f3(x,y)). [clausify]. given #2 (I,wt=2): 61 animal(c1). [resolve(7,a,1,a)]. given #3 (I,wt=2): 62 animal(c2). [resolve(8,a,2,a)]. given #4 (I,wt=3): 63 - eats(c1,c2). [resolve(30,a,8,a)]. given #5 (I,wt=2): 64 animal(c3). [resolve(9,a,3,a)]. given #6 (I,wt=2): 65 animal(c4). [resolve(10,a,4,a)]. given #7 (I,wt=3): 66 plant(f1(c4)). [resolve(19,a,10,a)]. given #8 (I,wt=4): 67 eats(c4,f1(c4)). [resolve(20,a,10,a)]. given #9 (I,wt=3): 68 eats(c3,c4). [resolve(39,a,10,a)]. given #10 (I,wt=2): 69 animal(c5). [resolve(11,a,5,a)]. given #11 (I,wt=3): 70 plant(f2(c5)). [resolve(21,a,11,a)]. given #12 (I,wt=4): 71 eats(c5,f2(c5)). [resolve(22,a,11,a)]. given #13 (I,wt=3): 72 - eats(c3,c5). [resolve(40,a,11,a)]. given #14 (I,wt=2): 73 plant(c6). [resolve(12,a,6,a)]. given #15 (I,wt=11): 74 - animal(x) | - animal(y) | - eats(x,y) | plant(f3(x,y)). [resolve(26,d,6,a)]. given #16 (I,wt=3): 75 - eats(c1,c6). [resolve(31,a,12,a)]. given #17 (I,wt=12): 76 - eats(c1,f3(x,y)) | - animal(x) | - animal(y) | - eats(x,y). [resolve(31,a,26,d)]. given #18 (I,wt=10): 77 - plant(x) | eats(c1,x) | - plant(y) | - eats(c2,y). [copy(56),unit_del(a,61),unit_del(d,62),unit_del(g,63)]. given #19 (I,wt=13): 78 - plant(x) | eats(c2,x) | - plant(y) | - eats(c3,y) | eats(c2,c3). [copy(57),unit_del(a,62),unit_del(d,64)]. given #20 (I,wt=10): 79 - plant(x) | eats(c3,x) | - plant(y) | - eats(c5,y). [copy(59),unit_del(a,64),unit_del(d,69),unit_del(g,72)]. given #21 (I,wt=10): 80 - animal(x) | - eats(x,x) | - eats(x,f3(x,x)). [factor(60,a,b)]. given #22 (I,wt=9): 81 - animal(x) | - eats(x,x) | plant(f3(x,x)). [factor(74,a,b)]. given #23 (I,wt=10): 82 - eats(c1,f3(x,x)) | - animal(x) | - eats(x,x). [factor(76,b,c)]. given #24 (I,wt=8): 83 - plant(x) | eats(c1,x) | - eats(c2,x). [factor(77,a,c)]. given #25 (I,wt=11): 84 - plant(x) | eats(c2,x) | - eats(c3,x) | eats(c2,c3). [factor(78,a,c)]. given #26 (I,wt=10): 85 - plant(c3) | eats(c2,c3) | - plant(x) | - eats(c3,x). [factor(78,b,e)]. given #27 (I,wt=8): 87 - plant(c3) | eats(c2,c3) | - eats(c3,c3). [factor(84,b,d)]. given #28 (F,wt=2): 104 - plant(c5). [ur(79,b,72,a,c,70,a,d,71,a)]. given #29 (T,wt=4): 92 plant(f3(c3,c4)). [resolve(74,c,68,a),unit_del(a,64),unit_del(b,65)]. given #30 (T,wt=5): 103 - plant(x) | eats(c3,x). [resolve(79,d,71,a),unit_del(c,70)]. given #31 (A,wt=10): 88 - animal(f1(c4)) | - eats(f1(c4),f3(c4,f1(c4))). [resolve(67,a,60,c),unit_del(a,65)]. given #32 (F,wt=3): 97 - eats(c2,c6). [ur(77,a,73,a,b,75,a,c,73,a)]. given #33 (F,wt=4): 98 - eats(c2,f2(c5)). [ur(77,a,73,a,b,75,a,c,70,a)]. given #34 (T,wt=3): 107 eats(c3,c6). [resolve(103,a,73,a)]. given #35 (T,wt=3): 111 eats(c2,c3). [resolve(107,a,84,c),unit_del(a,73),unit_del(b,97)]. given #36 (A,wt=5): 89 - eats(c4,f3(c3,c4)). [resolve(68,a,60,c),unit_del(a,64),unit_del(b,65)]. given #37 (F,wt=2): 120 - plant(c3). [ur(77,a,73,a,b,75,a,d,111,a)]. given #38 (F,wt=4): 99 - eats(c2,f1(c4)). [ur(77,a,73,a,b,75,a,c,66,a)]. given #39 (T,wt=4): 108 eats(c3,f2(c5)). [resolve(103,a,70,a)]. given #40 (T,wt=4): 109 eats(c3,f1(c4)). [resolve(103,a,66,a)]. given #41 (A,wt=10): 90 - animal(f2(c5)) | - eats(f2(c5),f3(c5,f2(c5))). [resolve(71,a,60,c),unit_del(a,69)]. given #42 (F,wt=5): 95 - eats(c1,f3(c3,c4)). [resolve(76,d,68,a),unit_del(b,64),unit_del(c,65)]. given #43 (F,wt=5): 105 - eats(c2,f3(c3,c4)). [ur(77,a,73,a,b,75,a,c,92,a)]. given #44 (T,wt=4): 118 plant(f3(c2,c3)). [resolve(111,a,74,c),unit_del(a,62),unit_del(b,64)]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 55. % Level of proof is 9. % Maximum clause weight is 13. % Given clauses 44. 1 - Wolf(x) | animal(x). [clausify]. 2 - Fox(x) | animal(x). [clausify]. 3 - Bird(x) | animal(x). [clausify]. 5 - Snail(x) | animal(x). [clausify]. 6 - Grain(x) | plant(x). [clausify]. 7 Wolf(c1). [clausify]. 8 Fox(c2). [clausify]. 9 Bird(c3). [clausify]. 11 Snail(c5). [clausify]. 12 Grain(c6). [clausify]. 13 - animal(x) | - plant(y) | eats(x,y) | - animal(z) | - Smaller(z,x) | - plant(u) | - eats(z,u) | eats(x,z). [clausify]. 15 - Snail(x) | - Bird(y) | Smaller(x,y). [clausify]. 16 - Bird(x) | - Fox(y) | Smaller(x,y). [clausify]. 17 - Fox(x) | - Wolf(y) | Smaller(x,y). [clausify]. 21 - Snail(x) | plant(f2(x)). [clausify]. 22 - Snail(x) | eats(x,f2(x)). [clausify]. 23 - Wolf(x) | - Fox(y) | - eats(x,y). [clausify]. 24 - Wolf(x) | - Grain(y) | - eats(x,y). [clausify]. 25 - Bird(x) | - Snail(y) | - eats(x,y). [clausify]. 26 - animal(x) | - animal(y) | - eats(x,y) | Grain(f3(x,y)). [clausify]. 29 - Fox(x) | Smaller(x,c1). [resolve(17,b,7,a)]. 30 - Fox(x) | - eats(c1,x). [resolve(23,a,7,a)]. 31 - Grain(x) | - eats(c1,x). [resolve(24,a,7,a)]. 33 - Bird(x) | Smaller(x,c2). [resolve(16,b,8,a)]. 34 Smaller(c2,c1). [resolve(29,a,8,a)]. 38 - Snail(x) | Smaller(x,c3). [resolve(15,b,9,a)]. 40 - Snail(x) | - eats(c3,x). [resolve(25,a,9,a)]. 41 Smaller(c3,c2). [resolve(33,a,9,a)]. 50 Smaller(c5,c3). [resolve(38,a,11,a)]. 56 - animal(c1) | - plant(x) | eats(c1,x) | - animal(c2) | - plant(y) | - eats(c2,y) | eats(c1,c2). [resolve(34,a,13,e)]. 57 - animal(c2) | - plant(x) | eats(c2,x) | - animal(c3) | - plant(y) | - eats(c3,y) | eats(c2,c3). [resolve(41,a,13,e)]. 59 - animal(c3) | - plant(x) | eats(c3,x) | - animal(c5) | - plant(y) | - eats(c5,y) | eats(c3,c5). [resolve(50,a,13,e)]. 60 - animal(x) | - animal(y) | - eats(x,y) | - eats(y,f3(x,y)). [clausify]. 61 animal(c1). [resolve(7,a,1,a)]. 62 animal(c2). [resolve(8,a,2,a)]. 63 - eats(c1,c2). [resolve(30,a,8,a)]. 64 animal(c3). [resolve(9,a,3,a)]. 69 animal(c5). [resolve(11,a,5,a)]. 70 plant(f2(c5)). [resolve(21,a,11,a)]. 71 eats(c5,f2(c5)). [resolve(22,a,11,a)]. 72 - eats(c3,c5). [resolve(40,a,11,a)]. 73 plant(c6). [resolve(12,a,6,a)]. 74 - animal(x) | - animal(y) | - eats(x,y) | plant(f3(x,y)). [resolve(26,d,6,a)]. 75 - eats(c1,c6). [resolve(31,a,12,a)]. 77 - plant(x) | eats(c1,x) | - plant(y) | - eats(c2,y). [copy(56),unit_del(a,61),unit_del(d,62),unit_del(g,63)]. 78 - plant(x) | eats(c2,x) | - plant(y) | - eats(c3,y) | eats(c2,c3). [copy(57),unit_del(a,62),unit_del(d,64)]. 79 - plant(x) | eats(c3,x) | - plant(y) | - eats(c5,y). [copy(59),unit_del(a,64),unit_del(d,69),unit_del(g,72)]. 84 - plant(x) | eats(c2,x) | - eats(c3,x) | eats(c2,c3). [factor(78,a,c)]. 97 - eats(c2,c6). [ur(77,a,73,a,b,75,a,c,73,a)]. 103 - plant(x) | eats(c3,x). [resolve(79,d,71,a),unit_del(c,70)]. 107 eats(c3,c6). [resolve(103,a,73,a)]. 111 eats(c2,c3). [resolve(107,a,84,c),unit_del(a,73),unit_del(b,97)]. 118 plant(f3(c2,c3)). [resolve(111,a,74,c),unit_del(a,62),unit_del(b,64)]. 119 - eats(c3,f3(c2,c3)). [resolve(111,a,60,c),unit_del(a,62),unit_del(b,64)]. 127 $F. [resolve(118,a,103,a),unit_del(a,119)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=44. Generated=85. Kept=67. proofs=1. Usable=39. Sos=16. Demods=0. Denials=0. Limbo=0, Disabled=70. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=17. Back_subsumed=12. 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=9. Nonunit_bsub_feature_tests=66. Megabytes=0.08. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13073 exit (max_proofs) Mon Jun 19 16:41:11 2006