============================== Prover9 =============================== Prover9 (32) version June-2007, June 2007. Process 20586 was started by zalta on mally, Fri Jul 27 15:11:14 2007 The command was "prove". ============================== end of head =========================== ============================== INPUT ================================= formulas(assumptions). (all x (object(x) -> -relation1(x))). (all x (object(x) -> -relation2(x))). (all F (relation1(F) -> -relation2(F))). (all x all F (exemplifies1(F,x) -> relation1(F) & object(x))). (all x all y all R (exemplifies2(R,x,y) -> relation2(R) & object(x) & object(y))). (all x all F (is_the(x,F) -> relation1(F) & object(x))). relation1(e). relation1(conceivable). relation1(nonegreater). relation2(greaterthan). (all x (object(x) -> (exemplifies1(nonegreater,x) <-> exemplifies1(conceivable,x) & -(exists y (object(y) & exemplifies2(greaterthan,y,x) & exemplifies1(conceivable,y)))))). (exists x (object(x) & exemplifies1(nonegreater,x))). (exists x (object(x) & exemplifies1(nonegreater,x))) -> (exists x (object(x) & exemplifies1(nonegreater,x) & (all y (object(y) -> (exemplifies1(nonegreater,y) -> y = x))))). (all F (relation1(F) -> ((exists x (object(x) & exemplifies1(F,x) & (all y (object(y) -> (exemplifies1(F,y) -> y = x))))) -> (exists x (object(x) & is_the(x,F)))))). (all F (relation1(F) -> ((exists x (object(x) & is_the(x,F))) -> (all y (object(y) -> (is_the(y,F) -> exemplifies1(F,y))))))). (all x (object(x) -> (is_the(x,nonegreater) & -exemplifies1(e,x) -> (exists y (object(y) & exemplifies2(greaterthan,y,x) & exemplifies1(conceivable,y)))))). is_the(g,nonegreater). end_of_list. formulas(goals). exemplifies1(e,g). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all x (object(x) -> -relation1(x))) # label(non_clause). [assumption]. 2 (all x (object(x) -> -relation2(x))) # label(non_clause). [assumption]. 3 (all F (relation1(F) -> -relation2(F))) # label(non_clause). [assumption]. 4 (all x all F (exemplifies1(F,x) -> relation1(F) & object(x))) # label(non_clause). [assumption]. 5 (all x all y all R (exemplifies2(R,x,y) -> relation2(R) & object(x) & object(y))) # label(non_clause). [assumption]. 6 (all x all F (is_the(x,F) -> relation1(F) & object(x))) # label(non_clause). [assumption]. 7 (all x (object(x) -> (exemplifies1(nonegreater,x) <-> exemplifies1(conceivable,x) & -(exists y (object(y) & exemplifies2(greaterthan,y,x) & exemplifies1(conceivable,y)))))) # label(non_clause). [assumption]. 8 (exists x (object(x) & exemplifies1(nonegreater,x))) # label(non_clause). [assumption]. 9 (exists x (object(x) & exemplifies1(nonegreater,x))) -> (exists x (object(x) & exemplifies1(nonegreater,x) & (all y (object(y) -> (exemplifies1(nonegreater,y) -> y = x))))) # label(non_clause). [assumption]. 10 (all F (relation1(F) -> ((exists x (object(x) & exemplifies1(F,x) & (all y (object(y) -> (exemplifies1(F,y) -> y = x))))) -> (exists x (object(x) & is_the(x,F)))))) # label(non_clause). [assumption]. 11 (all F (relation1(F) -> ((exists x (object(x) & is_the(x,F))) -> (all y (object(y) -> (is_the(y,F) -> exemplifies1(F,y))))))) # label(non_clause). [assumption]. 12 (all x (object(x) -> (is_the(x,nonegreater) & -exemplifies1(e,x) -> (exists y (object(y) & exemplifies2(greaterthan,y,x) & exemplifies1(conceivable,y)))))) # label(non_clause). [assumption]. 13 exemplifies1(e,g) # 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). -object(x) | -relation1(x). [clausify(1)]. -object(x) | -relation2(x). [clausify(2)]. -relation1(x) | -relation2(x). [clausify(3)]. -exemplifies1(x,y) | relation1(x). [clausify(4)]. -exemplifies1(x,y) | object(y). [clausify(4)]. -exemplifies2(x,y,z) | relation2(x). [clausify(5)]. -exemplifies2(x,y,z) | object(y). [clausify(5)]. -exemplifies2(x,y,z) | object(z). [clausify(5)]. -is_the(x,y) | relation1(y). [clausify(6)]. -is_the(x,y) | object(x). [clausify(6)]. relation1(e). [assumption]. relation1(conceivable). [assumption]. relation1(nonegreater). [assumption]. relation2(greaterthan). [assumption]. -object(x) | -exemplifies1(nonegreater,x) | exemplifies1(conceivable,x). [clausify(7)]. -object(x) | -exemplifies1(nonegreater,x) | -object(y) | -exemplifies2(greaterthan,y,x) | -exemplifies1(conceivable,y). [clausify(7)]. -object(x) | exemplifies1(nonegreater,x) | -exemplifies1(conceivable,x) | object(f1(x)). [clausify(7)]. -object(x) | exemplifies1(nonegreater,x) | -exemplifies1(conceivable,x) | exemplifies2(greaterthan,f1(x),x). [clausify(7)]. -object(x) | exemplifies1(nonegreater,x) | -exemplifies1(conceivable,x) | exemplifies1(conceivable,f1(x)). [clausify(7)]. object(c1). [clausify(8)]. exemplifies1(nonegreater,c1). [clausify(8)]. -object(x) | -exemplifies1(nonegreater,x) | object(c2). [clausify(9)]. -object(x) | -exemplifies1(nonegreater,x) | exemplifies1(nonegreater,c2). [clausify(9)]. -object(x) | -exemplifies1(nonegreater,x) | -object(y) | -exemplifies1(nonegreater,y) | y = c2. [clausify(9)]. -relation1(x) | -object(y) | -exemplifies1(x,y) | object(f2(x,y)) | object(f3(x)). [clausify(10)]. -relation1(x) | -object(y) | -exemplifies1(x,y) | object(f2(x,y)) | is_the(f3(x),x). [clausify(10)]. -relation1(x) | -object(y) | -exemplifies1(x,y) | exemplifies1(x,f2(x,y)) | object(f3(x)). [clausify(10)]. -relation1(x) | -object(y) | -exemplifies1(x,y) | exemplifies1(x,f2(x,y)) | is_the(f3(x),x). [clausify(10)]. -relation1(x) | -object(y) | -exemplifies1(x,y) | f2(x,y) != y | object(f3(x)). [clausify(10)]. -relation1(x) | -object(y) | -exemplifies1(x,y) | f2(x,y) != y | is_the(f3(x),x). [clausify(10)]. -relation1(x) | -object(y) | -is_the(y,x) | -object(z) | -is_the(z,x) | exemplifies1(x,z). [clausify(11)]. -object(x) | -is_the(x,nonegreater) | exemplifies1(e,x) | object(f4(x)). [clausify(12)]. -object(x) | -is_the(x,nonegreater) | exemplifies1(e,x) | exemplifies2(greaterthan,f4(x),x). [clausify(12)]. -object(x) | -is_the(x,nonegreater) | exemplifies1(e,x) | exemplifies1(conceivable,f4(x)). [clausify(12)]. is_the(g,nonegreater). [assumption]. -exemplifies1(e,g). [deny(13)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating relation1/1 14 -exemplifies1(x,y) | relation1(x). [clausify(4)]. 15 -object(x) | -relation1(x). [clausify(1)]. 16 -relation1(x) | -relation2(x). [clausify(3)]. Derived: -exemplifies1(x,y) | -object(x). [resolve(14,b,15,b)]. Derived: -exemplifies1(x,y) | -relation2(x). [resolve(14,b,16,a)]. 17 -is_the(x,y) | relation1(y). [clausify(6)]. Derived: -is_the(x,y) | -object(y). [resolve(17,b,15,b)]. Derived: -is_the(x,y) | -relation2(y). [resolve(17,b,16,a)]. 18 relation1(e). [assumption]. Derived: -object(e). [resolve(18,a,15,b)]. Derived: -relation2(e). [resolve(18,a,16,a)]. 19 relation1(conceivable). [assumption]. Derived: -object(conceivable). [resolve(19,a,15,b)]. Derived: -relation2(conceivable). [resolve(19,a,16,a)]. 20 relation1(nonegreater). [assumption]. Derived: -object(nonegreater). [resolve(20,a,15,b)]. Derived: -relation2(nonegreater). [resolve(20,a,16,a)]. 21 -relation1(x) | -object(y) | -exemplifies1(x,y) | object(f2(x,y)) | object(f3(x)). [clausify(10)]. Derived: -object(x) | -exemplifies1(y,x) | object(f2(y,x)) | object(f3(y)) | -exemplifies1(y,z). [resolve(21,a,14,b)]. 22 -relation1(x) | -object(y) | -exemplifies1(x,y) | object(f2(x,y)) | is_the(f3(x),x). [clausify(10)]. Derived: -object(x) | -exemplifies1(y,x) | object(f2(y,x)) | is_the(f3(y),y) | -exemplifies1(y,z). [resolve(22,a,14,b)]. 23 -relation1(x) | -object(y) | -exemplifies1(x,y) | exemplifies1(x,f2(x,y)) | object(f3(x)). [clausify(10)]. Derived: -object(x) | -exemplifies1(y,x) | exemplifies1(y,f2(y,x)) | object(f3(y)) | -exemplifies1(y,z). [resolve(23,a,14,b)]. 24 -relation1(x) | -object(y) | -exemplifies1(x,y) | exemplifies1(x,f2(x,y)) | is_the(f3(x),x). [clausify(10)]. Derived: -object(x) | -exemplifies1(y,x) | exemplifies1(y,f2(y,x)) | is_the(f3(y),y) | -exemplifies1(y,z). [resolve(24,a,14,b)]. 25 -relation1(x) | -object(y) | -exemplifies1(x,y) | f2(x,y) != y | object(f3(x)). [clausify(10)]. Derived: -object(x) | -exemplifies1(y,x) | f2(y,x) != x | object(f3(y)) | -exemplifies1(y,z). [resolve(25,a,14,b)]. 26 -relation1(x) | -object(y) | -exemplifies1(x,y) | f2(x,y) != y | is_the(f3(x),x). [clausify(10)]. Derived: -object(x) | -exemplifies1(y,x) | f2(y,x) != x | is_the(f3(y),y) | -exemplifies1(y,z). [resolve(26,a,14,b)]. 27 -relation1(x) | -object(y) | -is_the(y,x) | -object(z) | -is_the(z,x) | exemplifies1(x,z). [clausify(11)]. Derived: -object(x) | -is_the(x,y) | -object(z) | -is_the(z,y) | exemplifies1(y,z) | -exemplifies1(y,u). [resolve(27,a,14,b)]. Derived: -object(x) | -is_the(x,y) | -object(z) | -is_the(z,y) | exemplifies1(y,z) | -is_the(u,y). [resolve(27,a,17,b)]. ============================== end predicate elimination ============= Auto_denials: (non-Horn, no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ =, object, relation2, exemplifies1, is_the, exemplifies2 ]). Function symbol precedence: function_order([ nonegreater, conceivable, e, greaterthan, g, c1, c2, f2, f1, f3, f4 ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(binary_resolution). % (non-Horn) % set(positive_inference). % (non-Horn) % set(positive_inference) -> assign(literal_selection, maximal_negative). % 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: formulas(usable). end_of_list. formulas(sos). 28 -object(x) | -relation2(x). [clausify(2)]. 29 -exemplifies1(x,y) | object(y). [clausify(4)]. 30 -exemplifies2(x,y,z) | relation2(x). [clausify(5)]. 31 -exemplifies2(x,y,z) | object(y). [clausify(5)]. 32 -exemplifies2(x,y,z) | object(z). [clausify(5)]. 33 -is_the(x,y) | object(x). [clausify(6)]. 34 relation2(greaterthan). [assumption]. 35 -object(x) | -exemplifies1(nonegreater,x) | exemplifies1(conceivable,x). [clausify(7)]. 36 -object(x) | -exemplifies1(nonegreater,x) | -object(y) | -exemplifies2(greaterthan,y,x) | -exemplifies1(conceivable,y). [clausify(7)]. 37 -object(x) | exemplifies1(nonegreater,x) | -exemplifies1(conceivable,x) | object(f1(x)). [clausify(7)]. 38 -object(x) | exemplifies1(nonegreater,x) | -exemplifies1(conceivable,x) | exemplifies2(greaterthan,f1(x),x). [clausify(7)]. 39 -object(x) | exemplifies1(nonegreater,x) | -exemplifies1(conceivable,x) | exemplifies1(conceivable,f1(x)). [clausify(7)]. 40 object(c1). [clausify(8)]. 41 exemplifies1(nonegreater,c1). [clausify(8)]. 42 -object(x) | -exemplifies1(nonegreater,x) | object(c2). [clausify(9)]. 43 -object(x) | -exemplifies1(nonegreater,x) | exemplifies1(nonegreater,c2). [clausify(9)]. 46 -object(x) | -is_the(x,nonegreater) | exemplifies1(e,x) | object(f4(x)). [clausify(12)]. 47 -object(x) | -is_the(x,nonegreater) | exemplifies1(e,x) | exemplifies2(greaterthan,f4(x),x). [clausify(12)]. 48 -object(x) | -is_the(x,nonegreater) | exemplifies1(e,x) | exemplifies1(conceivable,f4(x)). [clausify(12)]. 49 is_the(g,nonegreater). [assumption]. 50 -exemplifies1(e,g). [deny(13)]. 51 -exemplifies1(x,y) | -object(x). [resolve(14,b,15,b)]. 52 -exemplifies1(x,y) | -relation2(x). [resolve(14,b,16,a)]. 53 -is_the(x,y) | -object(y). [resolve(17,b,15,b)]. 54 -is_the(x,y) | -relation2(y). [resolve(17,b,16,a)]. 55 -object(e). [resolve(18,a,15,b)]. 56 -relation2(e). [resolve(18,a,16,a)]. 57 -object(conceivable). [resolve(19,a,15,b)]. 58 -relation2(conceivable). [resolve(19,a,16,a)]. 59 -object(nonegreater). [resolve(20,a,15,b)]. 60 -relation2(nonegreater). [resolve(20,a,16,a)]. 69 -object(x) | -exemplifies1(nonegreater,x) | -exemplifies2(greaterthan,x,x) | -exemplifies1(conceivable,x). [factor(36,a,c)]. 70 -object(x) | -exemplifies1(nonegreater,x) | c2 = x. [factor(45,a,c),merge(c)]. 71 -object(x) | -exemplifies1(y,x) | object(f2(y,x)) | object(f3(y)). [factor(61,b,e)]. 72 -object(x) | -exemplifies1(y,x) | object(f2(y,x)) | is_the(f3(y),y). [factor(62,b,e)]. 73 -object(x) | -exemplifies1(y,x) | exemplifies1(y,f2(y,x)) | object(f3(y)). [factor(63,b,e)]. 74 -object(x) | -exemplifies1(y,x) | exemplifies1(y,f2(y,x)) | is_the(f3(y),y). [factor(64,b,e)]. 75 -object(x) | -exemplifies1(y,x) | f2(y,x) != x | object(f3(y)). [factor(65,b,e)]. 76 -object(x) | -exemplifies1(y,x) | f2(y,x) != x | is_the(f3(y),y). [factor(66,b,e)]. 79 -object(x) | -is_the(x,y) | exemplifies1(y,x). [factor(78,b,d)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=4): 28 -object(x) | -relation2(x). [clausify(2)]. given #2 (I,wt=5): 29 -exemplifies1(x,y) | object(y). [clausify(4)]. given #3 (I,wt=6): 30 -exemplifies2(x,y,z) | relation2(x). [clausify(5)]. given #4 (I,wt=6): 31 -exemplifies2(x,y,z) | object(y). [clausify(5)]. given #5 (I,wt=6): 32 -exemplifies2(x,y,z) | object(z). [clausify(5)]. given #6 (I,wt=5): 33 -is_the(x,y) | object(x). [clausify(6)]. given #7 (I,wt=2): 34 relation2(greaterthan). [assumption]. given #8 (I,wt=8): 35 -object(x) | -exemplifies1(nonegreater,x) | exemplifies1(conceivable,x). [clausify(7)]. given #9 (I,wt=14): 36 -object(x) | -exemplifies1(nonegreater,x) | -object(y) | -exemplifies2(greaterthan,y,x) | -exemplifies1(conceivable,y). [clausify(7)]. given #10 (I,wt=11): 37 -object(x) | exemplifies1(nonegreater,x) | -exemplifies1(conceivable,x) | object(f1(x)). [clausify(7)]. given #11 (I,wt=13): 38 -object(x) | exemplifies1(nonegreater,x) | -exemplifies1(conceivable,x) | exemplifies2(greaterthan,f1(x),x). [clausify(7)]. given #12 (I,wt=12): 39 -object(x) | exemplifies1(nonegreater,x) | -exemplifies1(conceivable,x) | exemplifies1(conceivable,f1(x)). [clausify(7)]. given #13 (I,wt=2): 40 object(c1). [clausify(8)]. given #14 (I,wt=3): 41 exemplifies1(nonegreater,c1). [clausify(8)]. given #15 (I,wt=7): 42 -object(x) | -exemplifies1(nonegreater,x) | object(c2). [clausify(9)]. given #16 (I,wt=8): 43 -object(x) | -exemplifies1(nonegreater,x) | exemplifies1(nonegreater,c2). [clausify(9)]. given #17 (I,wt=11): 46 -object(x) | -is_the(x,nonegreater) | exemplifies1(e,x) | object(f4(x)). [clausify(12)]. given #18 (I,wt=13): 47 -object(x) | -is_the(x,nonegreater) | exemplifies1(e,x) | exemplifies2(greaterthan,f4(x),x). [clausify(12)]. given #19 (I,wt=12): 48 -object(x) | -is_the(x,nonegreater) | exemplifies1(e,x) | exemplifies1(conceivable,f4(x)). [clausify(12)]. given #20 (I,wt=3): 49 is_the(g,nonegreater). [assumption]. given #21 (I,wt=3): 50 -exemplifies1(e,g). [deny(13)]. given #22 (I,wt=5): 51 -exemplifies1(x,y) | -object(x). [resolve(14,b,15,b)]. given #23 (I,wt=5): 52 -exemplifies1(x,y) | -relation2(x). [resolve(14,b,16,a)]. given #24 (I,wt=5): 53 -is_the(x,y) | -object(y). [resolve(17,b,15,b)]. given #25 (I,wt=5): 54 -is_the(x,y) | -relation2(y). [resolve(17,b,16,a)]. given #26 (I,wt=2): 55 -object(e). [resolve(18,a,15,b)]. given #27 (I,wt=2): 56 -relation2(e). [resolve(18,a,16,a)]. given #28 (I,wt=2): 57 -object(conceivable). [resolve(19,a,15,b)]. given #29 (I,wt=2): 58 -relation2(conceivable). [resolve(19,a,16,a)]. given #30 (I,wt=2): 59 -object(nonegreater). [resolve(20,a,15,b)]. given #31 (I,wt=2): 60 -relation2(nonegreater). [resolve(20,a,16,a)]. given #32 (I,wt=12): 69 -object(x) | -exemplifies1(nonegreater,x) | -exemplifies2(greaterthan,x,x) | -exemplifies1(conceivable,x). [factor(36,a,c)]. given #33 (I,wt=8): 70 -object(x) | -exemplifies1(nonegreater,x) | c2 = x. [factor(45,a,c),merge(c)]. given #34 (I,wt=12): 71 -object(x) | -exemplifies1(y,x) | object(f2(y,x)) | object(f3(y)). [factor(61,b,e)]. given #35 (I,wt=13): 72 -object(x) | -exemplifies1(y,x) | object(f2(y,x)) | is_the(f3(y),y). [factor(62,b,e)]. given #36 (I,wt=13): 73 -object(x) | -exemplifies1(y,x) | exemplifies1(y,f2(y,x)) | object(f3(y)). [factor(63,b,e)]. given #37 (I,wt=14): 74 -object(x) | -exemplifies1(y,x) | exemplifies1(y,f2(y,x)) | is_the(f3(y),y). [factor(64,b,e)]. given #38 (I,wt=13): 75 -object(x) | -exemplifies1(y,x) | f2(y,x) != x | object(f3(y)). [factor(65,b,e)]. given #39 (I,wt=14): 76 -object(x) | -exemplifies1(y,x) | f2(y,x) != x | is_the(f3(y),y). [factor(66,b,e)]. given #40 (I,wt=8): 79 -object(x) | -is_the(x,y) | exemplifies1(y,x). [factor(78,b,d)]. given #41 (A,wt=2): 80 -object(greaterthan). [resolve(34,a,28,b)]. given #42 (F,wt=2): 81 -relation2(c1). [ur(28,a,40,a)]. given #43 (F,wt=3): 92 -exemplifies1(c1,x). [ur(51,b,40,a)]. given #44 (F,wt=3): 93 -exemplifies1(greaterthan,x). [ur(52,b,34,a)]. given #45 (F,wt=3): 94 -is_the(x,c1). [ur(53,b,40,a)]. given #46 (T,wt=2): 88 object(g). [resolve(49,a,33,a)]. given #47 (T,wt=3): 82 exemplifies1(conceivable,c1). [resolve(41,a,35,b),unit_del(a,40)]. given #48 (T,wt=3): 89 object(f4(g)). [back_unit_del(87),unit_del(a,88)]. given #49 (T,wt=3): 111 c2 = c1. [resolve(70,b,41,a),unit_del(a,40)]. given #50 (A,wt=5): 90 exemplifies2(greaterthan,f4(g),g). [back_unit_del(86),unit_del(a,88)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.01) seconds. % Length of proof is 26. % Level of proof is 6. % Maximum clause weight is 16. % Given clauses 50. 6 (all x all F (is_the(x,F) -> relation1(F) & object(x))) # label(non_clause). [assumption]. 7 (all x (object(x) -> (exemplifies1(nonegreater,x) <-> exemplifies1(conceivable,x) & -(exists y (object(y) & exemplifies2(greaterthan,y,x) & exemplifies1(conceivable,y)))))) # label(non_clause). [assumption]. 11 (all F (relation1(F) -> ((exists x (object(x) & is_the(x,F))) -> (all y (object(y) -> (is_the(y,F) -> exemplifies1(F,y))))))) # label(non_clause). [assumption]. 12 (all x (object(x) -> (is_the(x,nonegreater) & -exemplifies1(e,x) -> (exists y (object(y) & exemplifies2(greaterthan,y,x) & exemplifies1(conceivable,y)))))) # label(non_clause). [assumption]. 13 exemplifies1(e,g) # label(non_clause) # label(goal). [goal]. 17 -is_the(x,y) | relation1(y). [clausify(6)]. 27 -relation1(x) | -object(y) | -is_the(y,x) | -object(z) | -is_the(z,x) | exemplifies1(x,z). [clausify(11)]. 33 -is_the(x,y) | object(x). [clausify(6)]. 36 -object(x) | -exemplifies1(nonegreater,x) | -object(y) | -exemplifies2(greaterthan,y,x) | -exemplifies1(conceivable,y). [clausify(7)]. 46 -object(x) | -is_the(x,nonegreater) | exemplifies1(e,x) | object(f4(x)). [clausify(12)]. 47 -object(x) | -is_the(x,nonegreater) | exemplifies1(e,x) | exemplifies2(greaterthan,f4(x),x). [clausify(12)]. 48 -object(x) | -is_the(x,nonegreater) | exemplifies1(e,x) | exemplifies1(conceivable,f4(x)). [clausify(12)]. 49 is_the(g,nonegreater). [assumption]. 50 -exemplifies1(e,g). [deny(13)]. 68 -object(x) | -is_the(x,y) | -object(z) | -is_the(z,y) | exemplifies1(y,z) | -is_the(u,y). [resolve(27,a,17,b)]. 78 -object(x) | -is_the(x,y) | exemplifies1(y,x) | -is_the(z,y). [factor(68,a,c),merge(c)]. 79 -object(x) | -is_the(x,y) | exemplifies1(y,x). [factor(78,b,d)]. 85 -object(g) | exemplifies1(conceivable,f4(g)). [resolve(49,a,48,b),unit_del(b,50)]. 86 -object(g) | exemplifies2(greaterthan,f4(g),g). [resolve(49,a,47,b),unit_del(b,50)]. 87 -object(g) | object(f4(g)). [resolve(49,a,46,b),unit_del(b,50)]. 88 object(g). [resolve(49,a,33,a)]. 89 object(f4(g)). [back_unit_del(87),unit_del(a,88)]. 90 exemplifies2(greaterthan,f4(g),g). [back_unit_del(86),unit_del(a,88)]. 91 exemplifies1(conceivable,f4(g)). [back_unit_del(85),unit_del(a,88)]. 119 exemplifies1(nonegreater,g). [resolve(79,b,49,a),unit_del(a,88)]. 139 $F. [resolve(90,a,36,d),unit_del(a,88),unit_del(b,119),unit_del(c,89),unit_del(d,91)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=50. Generated=147. Kept=110. proofs=1. Usable=47. Sos=44. Demods=1. Limbo=0, Disabled=73. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=36. Back_subsumed=13. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1 (0 lex), Back_demodulated=3. Back_unit_deleted=3. Demod_attempts=258. Demod_rewrites=3. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=45. Nonunit_bsub_feature_tests=154. Megabytes=0.13. User_CPU=0.01, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 20586 exit (max_proofs) Fri Jul 27 15:11:14 2007