============================== Prover9 =============================== Prover9 (64) version 2009-11A, November 2009. Process 34657 was started by zalta on frege.local, Tue May 2 19:54:41 2017 The command was "prover9". ============================== end of head =========================== ============================== INPUT ================================= formulas(assumptions). (all x (Object(x) -> (Ex1(none_greater,x) <-> Ex1(conceivable,x) & -(exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y)))))). Relation1(none_greater). (exists x (Object(x) & Ex1(none_greater,x))). -(exists x (Object(x) & Is_the(x,none_greater) & Ex1(e,x))) -> (all x (Object(x) & Is_the(x,none_greater) -> (exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y))))). (exists x (Object(x) & Ex1(none_greater,x))) -> (exists x (Object(x) & Ex1(none_greater,x) & (all y (Object(y) -> (Ex1(none_greater,y) -> Ex2(id,y,x)))))). (all x all F (Object(x) & Relation1(F) -> (Is_the(x,F) <-> Ex1(F,x) & (all z (Object(z) & Ex1(F,z) -> Ex2(id,x,z)))))). (all x all y (Object(x) & Object(y) -> (Ex2(id,x,y) <-> x = y))). end_of_list. formulas(goals). (exists x (Object(x) & Is_the(x,none_greater) & Ex1(e,x))). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all x (Object(x) -> (Ex1(none_greater,x) <-> Ex1(conceivable,x) & -(exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y)))))) # label(non_clause). [assumption]. 2 (exists x (Object(x) & Ex1(none_greater,x))) # label(non_clause). [assumption]. 3 -(exists x (Object(x) & Is_the(x,none_greater) & Ex1(e,x))) -> (all x (Object(x) & Is_the(x,none_greater) -> (exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y))))) # label(non_clause). [assumption]. 4 (exists x (Object(x) & Ex1(none_greater,x))) -> (exists x (Object(x) & Ex1(none_greater,x) & (all y (Object(y) -> (Ex1(none_greater,y) -> Ex2(id,y,x)))))) # label(non_clause). [assumption]. 5 (all x all F (Object(x) & Relation1(F) -> (Is_the(x,F) <-> Ex1(F,x) & (all z (Object(z) & Ex1(F,z) -> Ex2(id,x,z)))))) # label(non_clause). [assumption]. 6 (all x all y (Object(x) & Object(y) -> (Ex2(id,x,y) <-> x = y))) # label(non_clause). [assumption]. 7 (exists x (Object(x) & Is_the(x,none_greater) & Ex1(e,x))) # 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) | -Ex1(none_greater,x) | Ex1(conceivable,x). [clausify(1)]. -Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex2(greater_than,y,x) | -Ex1(conceivable,y). [clausify(1)]. -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Object(f1(x)). [clausify(1)]. -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex2(greater_than,f1(x),x). [clausify(1)]. -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex1(conceivable,f1(x)). [clausify(1)]. Relation1(none_greater). [assumption]. Object(c1). [clausify(2)]. Ex1(none_greater,c1). [clausify(2)]. Object(c2) | -Object(x) | -Is_the(x,none_greater) | Object(f2(x)). [clausify(3)]. Object(c2) | -Object(x) | -Is_the(x,none_greater) | Ex2(greater_than,f2(x),x). [clausify(3)]. Object(c2) | -Object(x) | -Is_the(x,none_greater) | Ex1(conceivable,f2(x)). [clausify(3)]. Is_the(c2,none_greater) | -Object(x) | -Is_the(x,none_greater) | Object(f2(x)). [clausify(3)]. Is_the(c2,none_greater) | -Object(x) | -Is_the(x,none_greater) | Ex2(greater_than,f2(x),x). [clausify(3)]. Is_the(c2,none_greater) | -Object(x) | -Is_the(x,none_greater) | Ex1(conceivable,f2(x)). [clausify(3)]. Ex1(e,c2) | -Object(x) | -Is_the(x,none_greater) | Object(f2(x)). [clausify(3)]. Ex1(e,c2) | -Object(x) | -Is_the(x,none_greater) | Ex2(greater_than,f2(x),x). [clausify(3)]. Ex1(e,c2) | -Object(x) | -Is_the(x,none_greater) | Ex1(conceivable,f2(x)). [clausify(3)]. -Object(x) | -Ex1(none_greater,x) | Object(c3). [clausify(4)]. -Object(x) | -Ex1(none_greater,x) | Ex1(none_greater,c3). [clausify(4)]. -Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex1(none_greater,y) | Ex2(id,y,c3). [clausify(4)]. -Object(x) | -Relation1(y) | -Is_the(x,y) | Ex1(y,x). [clausify(5)]. -Object(x) | -Relation1(y) | -Is_the(x,y) | -Object(z) | -Ex1(y,z) | Ex2(id,x,z). [clausify(5)]. -Object(x) | -Relation1(y) | Is_the(x,y) | -Ex1(y,x) | Object(f3(x,y)). [clausify(5)]. -Object(x) | -Relation1(y) | Is_the(x,y) | -Ex1(y,x) | Ex1(y,f3(x,y)). [clausify(5)]. -Object(x) | -Relation1(y) | Is_the(x,y) | -Ex1(y,x) | -Ex2(id,x,f3(x,y)). [clausify(5)]. -Object(x) | -Object(y) | -Ex2(id,x,y) | y = x. [clausify(6)]. -Object(x) | -Object(y) | Ex2(id,x,y) | y != x. [clausify(6)]. -Object(x) | -Is_the(x,none_greater) | -Ex1(e,x). [deny(7)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating Relation1/1 8 -Object(x) | -Relation1(y) | -Is_the(x,y) | Ex1(y,x). [clausify(5)]. 9 Relation1(none_greater). [assumption]. Derived: -Object(x) | -Is_the(x,none_greater) | Ex1(none_greater,x). [resolve(8,b,9,a)]. 10 -Object(x) | -Relation1(y) | -Is_the(x,y) | -Object(z) | -Ex1(y,z) | Ex2(id,x,z). [clausify(5)]. Derived: -Object(x) | -Is_the(x,none_greater) | -Object(y) | -Ex1(none_greater,y) | Ex2(id,x,y). [resolve(10,b,9,a)]. 11 -Object(x) | -Relation1(y) | Is_the(x,y) | -Ex1(y,x) | Object(f3(x,y)). [clausify(5)]. Derived: -Object(x) | Is_the(x,none_greater) | -Ex1(none_greater,x) | Object(f3(x,none_greater)). [resolve(11,b,9,a)]. 12 -Object(x) | -Relation1(y) | Is_the(x,y) | -Ex1(y,x) | Ex1(y,f3(x,y)). [clausify(5)]. Derived: -Object(x) | Is_the(x,none_greater) | -Ex1(none_greater,x) | Ex1(none_greater,f3(x,none_greater)). [resolve(12,b,9,a)]. 13 -Object(x) | -Relation1(y) | Is_the(x,y) | -Ex1(y,x) | -Ex2(id,x,f3(x,y)). [clausify(5)]. Derived: -Object(x) | Is_the(x,none_greater) | -Ex1(none_greater,x) | -Ex2(id,x,f3(x,none_greater)). [resolve(13,b,9,a)]. ============================== end predicate elimination ============= Auto_denials: (non-Horn, no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ =, Object, Ex1, Is_the, Ex2 ]). Function symbol precedence: function_order([ none_greater, conceivable, id, greater_than, e, c1, c2, c3, f3, f1, f2 ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(unit_deletion). % (non-Horn) kept: 14 -Object(x) | -Ex1(none_greater,x) | Ex1(conceivable,x). [clausify(1)]. kept: 15 -Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex2(greater_than,y,x) | -Ex1(conceivable,y). [clausify(1)]. kept: 16 -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Object(f1(x)). [clausify(1)]. kept: 17 -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex2(greater_than,f1(x),x). [clausify(1)]. kept: 18 -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex1(conceivable,f1(x)). [clausify(1)]. kept: 19 Object(c1). [clausify(2)]. kept: 20 Ex1(none_greater,c1). [clausify(2)]. kept: 21 Object(c2) | -Object(x) | -Is_the(x,none_greater) | Object(f2(x)). [clausify(3)]. kept: 22 Object(c2) | -Object(x) | -Is_the(x,none_greater) | Ex2(greater_than,f2(x),x). [clausify(3)]. kept: 23 Object(c2) | -Object(x) | -Is_the(x,none_greater) | Ex1(conceivable,f2(x)). [clausify(3)]. kept: 24 Is_the(c2,none_greater) | -Object(x) | -Is_the(x,none_greater) | Object(f2(x)). [clausify(3)]. kept: 25 Is_the(c2,none_greater) | -Object(x) | -Is_the(x,none_greater) | Ex2(greater_than,f2(x),x). [clausify(3)]. kept: 26 Is_the(c2,none_greater) | -Object(x) | -Is_the(x,none_greater) | Ex1(conceivable,f2(x)). [clausify(3)]. kept: 27 Ex1(e,c2) | -Object(x) | -Is_the(x,none_greater) | Object(f2(x)). [clausify(3)]. kept: 28 Ex1(e,c2) | -Object(x) | -Is_the(x,none_greater) | Ex2(greater_than,f2(x),x). [clausify(3)]. kept: 29 Ex1(e,c2) | -Object(x) | -Is_the(x,none_greater) | Ex1(conceivable,f2(x)). [clausify(3)]. kept: 30 -Object(x) | -Ex1(none_greater,x) | Object(c3). [clausify(4)]. kept: 31 -Object(x) | -Ex1(none_greater,x) | Ex1(none_greater,c3). [clausify(4)]. kept: 32 -Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex1(none_greater,y) | Ex2(id,y,c3). [clausify(4)]. kept: 33 -Object(x) | -Object(y) | -Ex2(id,x,y) | y = x. [clausify(6)]. kept: 34 -Object(x) | -Object(y) | Ex2(id,x,y) | y != x. [clausify(6)]. kept: 35 -Object(x) | -Is_the(x,none_greater) | -Ex1(e,x). [deny(7)]. kept: 36 -Object(x) | -Is_the(x,none_greater) | Ex1(none_greater,x). [resolve(8,b,9,a)]. kept: 37 -Object(x) | -Is_the(x,none_greater) | -Object(y) | -Ex1(none_greater,y) | Ex2(id,x,y). [resolve(10,b,9,a)]. kept: 38 -Object(x) | Is_the(x,none_greater) | -Ex1(none_greater,x) | Object(f3(x,none_greater)). [resolve(11,b,9,a)]. kept: 39 -Object(x) | Is_the(x,none_greater) | -Ex1(none_greater,x) | Ex1(none_greater,f3(x,none_greater)). [resolve(12,b,9,a)]. kept: 40 -Object(x) | Is_the(x,none_greater) | -Ex1(none_greater,x) | -Ex2(id,x,f3(x,none_greater)). [resolve(13,b,9,a)]. kept: 41 -Object(x) | -Ex1(none_greater,x) | -Ex2(greater_than,x,x) | -Ex1(conceivable,x). [factor(15,a,c)]. kept: 42 -Object(x) | -Ex1(none_greater,x) | Ex2(id,x,c3). [factor(32,a,c),merge(c)]. kept: 43 -Object(x) | Ex2(id,x,x). [factor(34,a,b),xx(c)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 14 -Object(x) | -Ex1(none_greater,x) | Ex1(conceivable,x). [clausify(1)]. 15 -Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex2(greater_than,y,x) | -Ex1(conceivable,y). [clausify(1)]. 16 -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Object(f1(x)). [clausify(1)]. 17 -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex2(greater_than,f1(x),x). [clausify(1)]. 18 -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex1(conceivable,f1(x)). [clausify(1)]. 19 Object(c1). [clausify(2)]. 20 Ex1(none_greater,c1). [clausify(2)]. 21 Object(c2) | -Object(x) | -Is_the(x,none_greater) | Object(f2(x)). [clausify(3)]. 22 Object(c2) | -Object(x) | -Is_the(x,none_greater) | Ex2(greater_than,f2(x),x). [clausify(3)]. 23 Object(c2) | -Object(x) | -Is_the(x,none_greater) | Ex1(conceivable,f2(x)). [clausify(3)]. 24 Is_the(c2,none_greater) | -Object(x) | -Is_the(x,none_greater) | Object(f2(x)). [clausify(3)]. 25 Is_the(c2,none_greater) | -Object(x) | -Is_the(x,none_greater) | Ex2(greater_than,f2(x),x). [clausify(3)]. 26 Is_the(c2,none_greater) | -Object(x) | -Is_the(x,none_greater) | Ex1(conceivable,f2(x)). [clausify(3)]. 27 Ex1(e,c2) | -Object(x) | -Is_the(x,none_greater) | Object(f2(x)). [clausify(3)]. 28 Ex1(e,c2) | -Object(x) | -Is_the(x,none_greater) | Ex2(greater_than,f2(x),x). [clausify(3)]. 29 Ex1(e,c2) | -Object(x) | -Is_the(x,none_greater) | Ex1(conceivable,f2(x)). [clausify(3)]. 30 -Object(x) | -Ex1(none_greater,x) | Object(c3). [clausify(4)]. 31 -Object(x) | -Ex1(none_greater,x) | Ex1(none_greater,c3). [clausify(4)]. 33 -Object(x) | -Object(y) | -Ex2(id,x,y) | y = x. [clausify(6)]. 34 -Object(x) | -Object(y) | Ex2(id,x,y) | y != x. [clausify(6)]. 35 -Object(x) | -Is_the(x,none_greater) | -Ex1(e,x). [deny(7)]. 36 -Object(x) | -Is_the(x,none_greater) | Ex1(none_greater,x). [resolve(8,b,9,a)]. 37 -Object(x) | -Is_the(x,none_greater) | -Object(y) | -Ex1(none_greater,y) | Ex2(id,x,y). [resolve(10,b,9,a)]. 38 -Object(x) | Is_the(x,none_greater) | -Ex1(none_greater,x) | Object(f3(x,none_greater)). [resolve(11,b,9,a)]. 39 -Object(x) | Is_the(x,none_greater) | -Ex1(none_greater,x) | Ex1(none_greater,f3(x,none_greater)). [resolve(12,b,9,a)]. 40 -Object(x) | Is_the(x,none_greater) | -Ex1(none_greater,x) | -Ex2(id,x,f3(x,none_greater)). [resolve(13,b,9,a)]. 41 -Object(x) | -Ex1(none_greater,x) | -Ex2(greater_than,x,x) | -Ex1(conceivable,x). [factor(15,a,c)]. 42 -Object(x) | -Ex1(none_greater,x) | Ex2(id,x,c3). [factor(32,a,c),merge(c)]. 43 -Object(x) | Ex2(id,x,x). [factor(34,a,b),xx(c)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=8): 14 -Object(x) | -Ex1(none_greater,x) | Ex1(conceivable,x). [clausify(1)]. given #2 (I,wt=14): 15 -Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex2(greater_than,y,x) | -Ex1(conceivable,y). [clausify(1)]. given #3 (I,wt=11): 16 -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Object(f1(x)). [clausify(1)]. given #4 (I,wt=13): 17 -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex2(greater_than,f1(x),x). [clausify(1)]. given #5 (I,wt=12): 18 -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex1(conceivable,f1(x)). [clausify(1)]. given #6 (I,wt=2): 19 Object(c1). [clausify(2)]. given #7 (I,wt=3): 20 Ex1(none_greater,c1). [clausify(2)]. given #8 (I,wt=10): 21 Object(c2) | -Object(x) | -Is_the(x,none_greater) | Object(f2(x)). [clausify(3)]. given #9 (I,wt=12): 22 Object(c2) | -Object(x) | -Is_the(x,none_greater) | Ex2(greater_than,f2(x),x). [clausify(3)]. given #10 (I,wt=11): 23 Object(c2) | -Object(x) | -Is_the(x,none_greater) | Ex1(conceivable,f2(x)). [clausify(3)]. given #11 (I,wt=11): 24 Is_the(c2,none_greater) | -Object(x) | -Is_the(x,none_greater) | Object(f2(x)). [clausify(3)]. given #12 (I,wt=13): 25 Is_the(c2,none_greater) | -Object(x) | -Is_the(x,none_greater) | Ex2(greater_than,f2(x),x). [clausify(3)]. given #13 (I,wt=12): 26 Is_the(c2,none_greater) | -Object(x) | -Is_the(x,none_greater) | Ex1(conceivable,f2(x)). [clausify(3)]. given #14 (I,wt=11): 27 Ex1(e,c2) | -Object(x) | -Is_the(x,none_greater) | Object(f2(x)). [clausify(3)]. given #15 (I,wt=13): 28 Ex1(e,c2) | -Object(x) | -Is_the(x,none_greater) | Ex2(greater_than,f2(x),x). [clausify(3)]. given #16 (I,wt=12): 29 Ex1(e,c2) | -Object(x) | -Is_the(x,none_greater) | Ex1(conceivable,f2(x)). [clausify(3)]. given #17 (I,wt=7): 30 -Object(x) | -Ex1(none_greater,x) | Object(c3). [clausify(4)]. given #18 (I,wt=8): 31 -Object(x) | -Ex1(none_greater,x) | Ex1(none_greater,c3). [clausify(4)]. given #19 (I,wt=11): 33 -Object(x) | -Object(y) | -Ex2(id,x,y) | y = x. [clausify(6)]. given #20 (I,wt=11): 34 -Object(x) | -Object(y) | Ex2(id,x,y) | y != x. [clausify(6)]. given #21 (I,wt=8): 35 -Object(x) | -Is_the(x,none_greater) | -Ex1(e,x). [deny(7)]. given #22 (I,wt=8): 36 -Object(x) | -Is_the(x,none_greater) | Ex1(none_greater,x). [resolve(8,b,9,a)]. given #23 (I,wt=14): 37 -Object(x) | -Is_the(x,none_greater) | -Object(y) | -Ex1(none_greater,y) | Ex2(id,x,y). [resolve(10,b,9,a)]. given #24 (I,wt=12): 38 -Object(x) | Is_the(x,none_greater) | -Ex1(none_greater,x) | Object(f3(x,none_greater)). [resolve(11,b,9,a)]. given #25 (I,wt=13): 39 -Object(x) | Is_the(x,none_greater) | -Ex1(none_greater,x) | Ex1(none_greater,f3(x,none_greater)). [resolve(12,b,9,a)]. given #26 (I,wt=14): 40 -Object(x) | Is_the(x,none_greater) | -Ex1(none_greater,x) | -Ex2(id,x,f3(x,none_greater)). [resolve(13,b,9,a)]. given #27 (I,wt=12): 41 -Object(x) | -Ex1(none_greater,x) | -Ex2(greater_than,x,x) | -Ex1(conceivable,x). [factor(15,a,c)]. given #28 (I,wt=9): 42 -Object(x) | -Ex1(none_greater,x) | Ex2(id,x,c3). [factor(32,a,c),merge(c)]. given #29 (I,wt=6): 43 -Object(x) | Ex2(id,x,x). [factor(34,a,b),xx(c)]. given #30 (A,wt=3): 44 Ex1(conceivable,c1). [resolve(20,a,14,b),unit_del(a,19)]. given #31 (F,wt=4): 53 -Ex2(greater_than,c1,c1). [ur(41,a,19,a,b,20,a,d,44,a)]. given #32 (T,wt=2): 45 Object(c3). [resolve(30,b,20,a),unit_del(a,19)]. given #33 (T,wt=3): 46 Ex1(none_greater,c3). [resolve(31,b,20,a),unit_del(a,19)]. given #34 (T,wt=3): 59 Ex1(conceivable,c3). [resolve(46,a,14,b),unit_del(a,45)]. given #35 (T,wt=4): 51 Ex2(id,c1,c3). [resolve(42,b,20,a),unit_del(a,19)]. given #36 (A,wt=9): 47 -Object(x) | Ex2(id,c1,x) | c1 != x. [resolve(34,a,19,a),flip(c)]. given #37 (T,wt=3): 63 c3 = c1. [resolve(51,a,33,c),unit_del(a,19),unit_del(b,45)]. given #38 (T,wt=4): 52 Ex2(id,c1,c1). [resolve(43,a,19,a)]. given #39 (T,wt=7): 49 Is_the(c1,none_greater) | Object(f3(c1,none_greater)). [resolve(38,c,20,a),unit_del(a,19)]. given #40 (T,wt=7): 66 Object(f3(c1,none_greater)) | -Ex1(e,c1). [resolve(49,a,35,b),unit_del(b,19)]. given #41 (A,wt=9): 48 -Object(x) | Ex2(id,x,c1) | c1 != x. [resolve(34,b,19,a)]. given #42 (T,wt=8): 50 Is_the(c1,none_greater) | Ex1(none_greater,f3(c1,none_greater)). [resolve(39,c,20,a),unit_del(a,19)]. given #43 (T,wt=8): 77 Ex1(none_greater,f3(c1,none_greater)) | -Ex1(e,c1). [resolve(50,a,35,b),unit_del(b,19)]. given #44 (T,wt=9): 64 -Object(x) | -Ex1(none_greater,x) | Ex2(id,x,c1). [back_rewrite(42),rewrite([63(5)])]. given #45 (T,wt=9): 75 Object(f3(c1,none_greater)) | Object(c2) | Object(f2(c1)). [resolve(49,a,21,c),unit_del(c,19)]. given #46 (A,wt=13): 65 Object(f3(c1,none_greater)) | -Object(x) | -Ex1(none_greater,x) | Ex2(id,c1,x). [resolve(49,a,37,b),unit_del(b,19)]. given #47 (T,wt=10): 69 Object(f3(c1,none_greater)) | Ex1(e,c2) | Object(f2(c1)). [resolve(49,a,27,c),unit_del(c,19)]. given #48 (T,wt=10): 72 Object(f3(c1,none_greater)) | Is_the(c2,none_greater) | Object(f2(c1)). [resolve(49,a,24,c),unit_del(c,19)]. given #49 (T,wt=10): 73 Object(f3(c1,none_greater)) | Object(c2) | Ex1(conceivable,f2(c1)). [resolve(49,a,23,c),unit_del(c,19)]. given #50 (T,wt=10): 86 Ex1(none_greater,f3(c1,none_greater)) | Object(c2) | Object(f2(c1)). [resolve(50,a,21,c),unit_del(c,19)]. given #51 (A,wt=11): 67 Object(f3(c1,none_greater)) | Ex1(e,c2) | Ex1(conceivable,f2(c1)). [resolve(49,a,29,c),unit_del(c,19)]. given #52 (T,wt=11): 70 Object(f3(c1,none_greater)) | Is_the(c2,none_greater) | Ex1(conceivable,f2(c1)). [resolve(49,a,26,c),unit_del(c,19)]. given #53 (T,wt=11): 74 Object(f3(c1,none_greater)) | Object(c2) | Ex2(greater_than,f2(c1),c1). [resolve(49,a,22,c),unit_del(c,19)]. given #54 (T,wt=11): 80 Ex1(none_greater,f3(c1,none_greater)) | Ex1(e,c2) | Object(f2(c1)). [resolve(50,a,27,c),unit_del(c,19)]. given #55 (T,wt=11): 83 Ex1(none_greater,f3(c1,none_greater)) | Is_the(c2,none_greater) | Object(f2(c1)). [resolve(50,a,24,c),unit_del(c,19)]. given #56 (A,wt=12): 68 Object(f3(c1,none_greater)) | Ex1(e,c2) | Ex2(greater_than,f2(c1),c1). [resolve(49,a,28,c),unit_del(c,19)]. given #57 (T,wt=11): 84 Ex1(none_greater,f3(c1,none_greater)) | Object(c2) | Ex1(conceivable,f2(c1)). [resolve(50,a,23,c),unit_del(c,19)]. given #58 (T,wt=12): 71 Object(f3(c1,none_greater)) | Is_the(c2,none_greater) | Ex2(greater_than,f2(c1),c1). [resolve(49,a,25,c),unit_del(c,19)]. given #59 (T,wt=12): 78 Ex1(none_greater,f3(c1,none_greater)) | Ex1(e,c2) | Ex1(conceivable,f2(c1)). [resolve(50,a,29,c),unit_del(c,19)]. given #60 (T,wt=12): 81 Ex1(none_greater,f3(c1,none_greater)) | Is_the(c2,none_greater) | Ex1(conceivable,f2(c1)). [resolve(50,a,26,c),unit_del(c,19)]. given #61 (A,wt=14): 76 Ex1(none_greater,f3(c1,none_greater)) | -Object(x) | -Ex1(none_greater,x) | Ex2(id,c1,x). [resolve(50,a,37,b),unit_del(b,19)]. given #62 (T,wt=12): 85 Ex1(none_greater,f3(c1,none_greater)) | Object(c2) | Ex2(greater_than,f2(c1),c1). [resolve(50,a,22,c),unit_del(c,19)]. given #63 (T,wt=12): 89 Object(f3(c1,none_greater)) | Object(c2) | Ex2(id,f2(c1),f2(c1)). [resolve(75,c,43,a)]. given #64 (T,wt=12): 93 Object(f3(c1,none_greater)) | Object(f2(c1)) | -Object(c2) | Ex1(none_greater,c2). [resolve(72,b,36,b)]. given #65 (T,wt=12): 94 Object(f3(c1,none_greater)) | Object(f2(c1)) | -Object(c2) | -Ex1(e,c2). [resolve(72,b,35,b)]. given #66 (A,wt=13): 79 Ex1(none_greater,f3(c1,none_greater)) | Ex1(e,c2) | Ex2(greater_than,f2(c1),c1). [resolve(50,a,28,c),unit_del(c,19)]. given #67 (T,wt=9): 119 Object(f3(c1,none_greater)) | Object(f2(c1)) | -Object(c2). [resolve(94,d,69,b),merge(d),merge(e)]. given #68 (T,wt=13): 82 Ex1(none_greater,f3(c1,none_greater)) | Is_the(c2,none_greater) | Ex2(greater_than,f2(c1),c1). [resolve(50,a,25,c),unit_del(c,19)]. given #69 (T,wt=13): 103 Object(f3(c1,none_greater)) | Ex1(conceivable,f2(c1)) | -Object(c2) | Ex1(none_greater,c2). [resolve(70,b,36,b)]. given #70 (T,wt=13): 104 Object(f3(c1,none_greater)) | Ex1(conceivable,f2(c1)) | -Object(c2) | -Ex1(e,c2). [resolve(70,b,35,b)]. given #71 (A,wt=15): 87 Object(f3(c1,none_greater)) | Object(c2) | Ex2(id,f2(c1),c1) | f2(c1) != c1. [resolve(75,c,48,a),flip(d)]. given #72 (T,wt=10): 123 Object(f3(c1,none_greater)) | Ex1(conceivable,f2(c1)) | -Object(c2). [resolve(104,d,67,b),merge(d),merge(e)]. given #73 (T,wt=13): 105 Object(f3(c1,none_greater)) | Object(c2) | -Object(f2(c1)) | -Ex1(conceivable,f2(c1)). [resolve(74,c,15,d),unit_del(c,19),unit_del(d,20)]. given #74 (T,wt=9): 125 Object(f3(c1,none_greater)) | Object(c2) | -Object(f2(c1)). [resolve(105,d,73,c),merge(d),merge(e)]. given #75 (T,wt=6): 126 Object(f3(c1,none_greater)) | Object(c2). [resolve(125,c,75,c),merge(c),merge(d)]. given #76 (A,wt=15): 98 Object(c2) | Object(f2(c1)) | -Object(f3(c1,none_greater)) | Ex2(id,f3(c1,none_greater),c1). [resolve(86,a,64,b)]. given #77 (T,wt=10): 129 Object(c2) | Ex2(id,f3(c1,none_greater),f3(c1,none_greater)). [resolve(126,a,43,a)]. given #78 (T,wt=11): 132 Object(c2) | Object(f2(c1)) | Ex2(id,f3(c1,none_greater),c1). [resolve(98,c,126,a),merge(d)]. given #79 (T,wt=13): 107 Ex1(none_greater,f3(c1,none_greater)) | Object(f2(c1)) | -Object(c2) | Ex1(none_greater,c2). [resolve(83,b,36,b)]. given #80 (T,wt=13): 108 Ex1(none_greater,f3(c1,none_greater)) | Object(f2(c1)) | -Object(c2) | -Ex1(e,c2). [resolve(83,b,35,b)]. given #81 (A,wt=21): 99 Object(c2) | Object(f2(c1)) | -Object(f3(c1,none_greater)) | Is_the(f3(c1,none_greater),none_greater) | Ex1(none_greater,f3(f3(c1,none_greater),none_greater)). [resolve(86,a,39,c)]. given #82 (T,wt=10): 134 Ex1(none_greater,f3(c1,none_greater)) | Object(f2(c1)) | -Object(c2). [resolve(108,d,80,b),merge(d),merge(e)]. given #83 (T,wt=13): 127 Object(c2) | Ex2(id,f3(c1,none_greater),c1) | f3(c1,none_greater) != c1. [resolve(126,a,48,a),flip(c)]. given #84 (T,wt=13): 128 Object(c2) | Ex2(id,c1,f3(c1,none_greater)) | f3(c1,none_greater) != c1. [resolve(126,a,47,a),flip(c)]. given #85 (T,wt=14): 101 Object(c2) | Object(f2(c1)) | -Object(f3(c1,none_greater)) | Ex1(conceivable,f3(c1,none_greater)). [resolve(86,a,14,b)]. given #86 (A,wt=20): 100 Object(c2) | Object(f2(c1)) | -Object(f3(c1,none_greater)) | Is_the(f3(c1,none_greater),none_greater) | Object(f3(f3(c1,none_greater),none_greater)). [resolve(86,a,38,c)]. given #87 (T,wt=10): 136 Object(c2) | Object(f2(c1)) | Ex1(conceivable,f3(c1,none_greater)). [resolve(101,c,126,a),merge(d)]. given #88 (T,wt=14): 109 Object(f3(c1,none_greater)) | Ex1(e,c2) | -Object(f2(c1)) | -Ex1(conceivable,f2(c1)). [resolve(68,c,15,d),unit_del(c,19),unit_del(d,20)]. given #89 (T,wt=14): 113 Object(f3(c1,none_greater)) | Is_the(c2,none_greater) | -Object(f2(c1)) | -Ex1(conceivable,f2(c1)). [resolve(71,c,15,d),unit_del(c,19),unit_del(d,20)]. given #90 (T,wt=14): 115 Ex1(none_greater,f3(c1,none_greater)) | Ex1(conceivable,f2(c1)) | -Object(c2) | Ex1(none_greater,c2). [resolve(81,b,36,b)]. given #91 (A,wt=19): 110 Ex1(none_greater,f3(c1,none_greater)) | Object(c2) | -Object(f2(c1)) | Ex1(none_greater,f2(c1)) | Ex1(conceivable,f1(f2(c1))). [resolve(84,c,18,c)]. given #92 (T,wt=14): 116 Ex1(none_greater,f3(c1,none_greater)) | Ex1(conceivable,f2(c1)) | -Object(c2) | -Ex1(e,c2). [resolve(81,b,35,b)]. given #93 (T,wt=11): 138 Ex1(none_greater,f3(c1,none_greater)) | Ex1(conceivable,f2(c1)) | -Object(c2). [resolve(116,d,78,b),merge(d),merge(e)]. given #94 (T,wt=14): 117 Ex1(none_greater,f3(c1,none_greater)) | Object(c2) | -Object(f2(c1)) | -Ex1(conceivable,f2(c1)). [resolve(85,c,15,d),unit_del(c,19),unit_del(d,20)]. given #95 (T,wt=10): 139 Ex1(none_greater,f3(c1,none_greater)) | Object(c2) | -Object(f2(c1)). [resolve(117,d,84,c),merge(d),merge(e)]. given #96 (A,wt=15): 120 Ex1(none_greater,f3(c1,none_greater)) | Ex1(e,c2) | -Object(f2(c1)) | -Ex1(conceivable,f2(c1)). [resolve(79,c,15,d),unit_del(c,19),unit_del(d,20)]. given #97 (T,wt=14): 133 Object(c2) | Object(f2(c1)) | -Object(f3(c1,none_greater)) | f3(c1,none_greater) = c1. [resolve(132,c,33,c),flip(e),unit_del(d,19)]. given #98 (T,wt=10): 140 Object(c2) | Object(f2(c1)) | f3(c1,none_greater) = c1. [resolve(133,c,126,a),merge(d)]. given #99 (T,wt=12): 141 Object(c2) | f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)). [resolve(140,b,139,c),merge(d)]. given #100 (T,wt=13): 144 Object(c2) | f3(c1,none_greater) = c1 | Ex2(id,f2(c1),f2(c1)). [resolve(140,b,43,a)]. given #101 (A,wt=15): 121 Ex1(none_greater,f3(c1,none_greater)) | Is_the(c2,none_greater) | -Object(f2(c1)) | -Ex1(conceivable,f2(c1)). [resolve(82,c,15,d),unit_del(c,19),unit_del(d,20)]. given #102 (T,wt=15): 130 Object(c2) | -Object(x) | Ex2(id,x,f3(c1,none_greater)) | f3(c1,none_greater) != x. [resolve(126,a,34,b)]. given #103 (T,wt=15): 131 Object(c2) | -Object(x) | Ex2(id,f3(c1,none_greater),x) | f3(c1,none_greater) != x. [resolve(126,a,34,a),flip(d)]. given #104 (T,wt=16): 137 Object(c2) | Object(f2(c1)) | Is_the(f3(c1,none_greater),none_greater) | Object(f3(f3(c1,none_greater),none_greater)). [resolve(100,c,126,a),merge(e)]. given #105 (T,wt=16): 142 Object(c2) | f3(c1,none_greater) = c1 | Ex2(id,f2(c1),c1) | f2(c1) != c1. [resolve(140,b,48,a),flip(d)]. given #106 (A,wt=17): 135 Object(c2) | Object(f2(c1)) | Is_the(f3(c1,none_greater),none_greater) | Ex1(none_greater,f3(f3(c1,none_greater),none_greater)). [resolve(99,c,126,a),merge(e)]. given #107 (T,wt=16): 143 Object(c2) | f3(c1,none_greater) = c1 | Ex2(id,c1,f2(c1)) | f2(c1) != c1. [resolve(140,b,47,a),flip(d)]. given #108 (T,wt=16): 150 Object(c2) | f3(c1,none_greater) = c1 | -Object(f3(c1,none_greater)) | Ex1(conceivable,f3(c1,none_greater)). [resolve(141,c,14,b)]. given #109 (T,wt=12): 175 Object(c2) | f3(c1,none_greater) = c1 | Ex1(conceivable,f3(c1,none_greater)). [resolve(150,c,126,a),merge(d)]. given #110 (T,wt=17): 147 Object(c2) | f3(c1,none_greater) = c1 | -Object(f3(c1,none_greater)) | Ex2(id,f3(c1,none_greater),c1). [resolve(141,c,64,b)]. given #111 (A,wt=18): 145 Object(c2) | f3(c1,none_greater) = c1 | -Object(x) | Ex2(id,x,f2(c1)) | f2(c1) != x. [resolve(140,b,34,b)]. given #112 (T,wt=13): 176 Object(c2) | f3(c1,none_greater) = c1 | Ex2(id,f3(c1,none_greater),c1). [resolve(147,c,126,a),merge(d)]. given #113 (T,wt=11): 177 Object(c2) | f3(c1,none_greater) = c1 | -Object(f3(c1,none_greater)). [resolve(176,c,33,c),flip(e),merge(e),unit_del(d,19)]. given #114 (T,wt=7): 178 Object(c2) | f3(c1,none_greater) = c1. [resolve(177,c,126,a),merge(c)]. given #115 (T,wt=9): 185 f3(c1,none_greater) = c1 | Ex2(id,c2,c2). [resolve(178,a,43,a)]. given #116 (A,wt=26): 153 Object(c2) | Object(f2(c1)) | Object(f3(f3(c1,none_greater),none_greater)) | -Object(f3(c1,none_greater)) | -Object(x) | -Ex1(none_greater,x) | Ex2(id,f3(c1,none_greater),x). [resolve(137,c,37,b)]. given #117 (T,wt=12): 182 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)) | Object(f2(c1)). [resolve(178,a,119,c)]. given #118 (T,wt=12): 183 f3(c1,none_greater) = c1 | Ex2(id,c2,c1) | c2 != c1. [resolve(178,a,48,a),flip(c)]. given #119 (T,wt=12): 184 f3(c1,none_greater) = c1 | Ex2(id,c1,c2) | c2 != c1. [resolve(178,a,47,a),flip(c)]. given #120 (T,wt=13): 180 f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)) | Object(f2(c1)). [resolve(178,a,134,c)]. given #121 (A,wt=20): 154 Object(c2) | Object(f2(c1)) | Object(f3(f3(c1,none_greater),none_greater)) | -Object(f3(c1,none_greater)) | -Ex1(e,f3(c1,none_greater)). [resolve(137,c,35,b)]. given #122 (T,wt=13): 181 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)) | Ex1(conceivable,f2(c1)). [resolve(178,a,123,c)]. given #123 (T,wt=14): 179 f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)) | Ex1(conceivable,f2(c1)). [resolve(178,a,138,c)]. given #124 (T,wt=14): 186 f3(c1,none_greater) = c1 | -Object(x) | Ex2(id,x,c2) | c2 != x. [resolve(178,a,34,b)]. given #125 (T,wt=14): 187 f3(c1,none_greater) = c1 | -Object(x) | Ex2(id,c2,x) | c2 != x. [resolve(178,a,34,a),flip(d)]. given #126 (A,wt=21): 161 Object(c2) | Object(f2(c1)) | Object(f3(f3(c1,none_greater),none_greater)) | -Object(f3(c1,none_greater)) | Ex1(conceivable,f2(f3(c1,none_greater))). [resolve(137,c,23,c),merge(d)]. given #127 (T,wt=15): 190 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)) | Ex2(id,f2(c1),f2(c1)). [resolve(182,c,43,a)]. given #128 (T,wt=15): 199 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)) | Is_the(c2,none_greater) | -Object(f2(c1)). [resolve(181,c,113,d),merge(c)]. given #129 (T,wt=12): 212 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)) | Is_the(c2,none_greater). [resolve(199,d,182,c),merge(d),merge(e)]. given #130 (T,wt=14): 214 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)) | -Object(c2) | Ex1(none_greater,c2). [resolve(212,c,36,b)]. given #131 (A,wt=24): 162 Object(c2) | Object(f2(c1)) | Object(f3(f3(c1,none_greater),none_greater)) | -Object(f3(c1,none_greater)) | Ex2(greater_than,f2(f3(c1,none_greater)),f3(c1,none_greater)). [resolve(137,c,22,c),merge(d)]. given #132 (T,wt=12): 219 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)) | Ex1(none_greater,c2). [resolve(214,c,178,a),merge(d)]. given #133 (T,wt=14): 215 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)) | -Object(c2) | -Ex1(e,c2). [resolve(212,c,35,b)]. given #134 (T,wt=14): 224 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)) | -Object(c2) | Ex1(conceivable,c2). [resolve(219,c,14,b)]. given #135 (T,wt=12): 225 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)) | Ex1(conceivable,c2). [resolve(224,c,178,a),merge(d)]. given #136 (A,wt=20): 163 Object(c2) | Object(f2(c1)) | Object(f3(f3(c1,none_greater),none_greater)) | -Object(f3(c1,none_greater)) | Object(f2(f3(c1,none_greater))). [resolve(137,c,21,c),merge(d)]. given #137 (T,wt=15): 200 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)) | Ex1(e,c2) | -Object(f2(c1)). [resolve(181,c,109,d),merge(c)]. given #138 (T,wt=12): 227 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)) | Ex1(e,c2). [resolve(200,d,182,c),merge(d),merge(e)]. given #139 (T,wt=11): 228 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)) | -Object(c2). [resolve(227,c,215,d),merge(c),merge(d)]. given #140 (T,wt=9): 229 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)). [resolve(228,c,178,a),merge(c)]. given #141 (A,wt=27): 164 Object(c2) | Object(f2(c1)) | Ex1(none_greater,f3(f3(c1,none_greater),none_greater)) | -Object(f3(c1,none_greater)) | -Object(x) | -Ex1(none_greater,x) | Ex2(id,f3(c1,none_greater),x). [resolve(135,c,37,b)]. given #142 (T,wt=13): 232 f3(c1,none_greater) = c1 | Ex2(id,f3(c1,none_greater),f3(c1,none_greater)). [resolve(229,b,43,a)]. given #143 (T,wt=16): 204 f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)) | Is_the(c2,none_greater) | -Object(f2(c1)). [resolve(179,c,121,d),merge(c)]. given #144 (T,wt=16): 205 f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)) | Ex1(e,c2) | -Object(f2(c1)). [resolve(179,c,120,d),merge(c)]. given #145 (T,wt=16): 226 Object(c2) | Object(f2(c1)) | Object(f3(f3(c1,none_greater),none_greater)) | Object(f2(f3(c1,none_greater))). [resolve(163,d,126,a),merge(e)]. given #146 (A,wt=21): 165 Object(c2) | Object(f2(c1)) | Ex1(none_greater,f3(f3(c1,none_greater),none_greater)) | -Object(f3(c1,none_greater)) | -Ex1(e,f3(c1,none_greater)). [resolve(135,c,35,b)]. given #147 (T,wt=16): 230 f3(c1,none_greater) = c1 | Ex2(id,c2,f3(c1,none_greater)) | f3(c1,none_greater) != c2. [resolve(229,b,187,b),flip(d),merge(b)]. given #148 (T,wt=16): 231 f3(c1,none_greater) = c1 | Ex2(id,f3(c1,none_greater),c2) | f3(c1,none_greater) != c2. [resolve(229,b,186,b),flip(d),merge(b)]. given #149 (T,wt=17): 196 f3(c1,none_greater) = c1 | Object(f2(c1)) | -Object(f3(c1,none_greater)) | Ex1(conceivable,f3(c1,none_greater)). [resolve(180,b,14,b)]. given #150 (T,wt=13): 242 f3(c1,none_greater) = c1 | Object(f2(c1)) | Ex1(conceivable,f3(c1,none_greater)). [resolve(196,c,229,b),merge(d)]. given #151 (A,wt=22): 172 Object(c2) | Object(f2(c1)) | Ex1(none_greater,f3(f3(c1,none_greater),none_greater)) | -Object(f3(c1,none_greater)) | Ex1(conceivable,f2(f3(c1,none_greater))). [resolve(135,c,23,c),merge(d)]. given #152 (T,wt=17): 211 Object(c2) | Object(f2(c1)) | Object(f3(f3(c1,none_greater),none_greater)) | Ex1(conceivable,f2(f3(c1,none_greater))). [resolve(161,d,126,a),merge(e)]. given #153 (T,wt=18): 193 f3(c1,none_greater) = c1 | Object(f2(c1)) | -Object(f3(c1,none_greater)) | Ex2(id,f3(c1,none_greater),c1). [resolve(180,b,64,b)]. given #154 (T,wt=14): 247 f3(c1,none_greater) = c1 | Object(f2(c1)) | Ex2(id,f3(c1,none_greater),c1). [resolve(193,c,229,b),merge(d)]. given #155 (T,wt=12): 248 f3(c1,none_greater) = c1 | Object(f2(c1)) | -Object(f3(c1,none_greater)). [resolve(247,c,33,c),flip(e),merge(e),unit_del(d,19)]. given #156 (A,wt=25): 173 Object(c2) | Object(f2(c1)) | Ex1(none_greater,f3(f3(c1,none_greater),none_greater)) | -Object(f3(c1,none_greater)) | Ex2(greater_than,f2(f3(c1,none_greater)),f3(c1,none_greater)). [resolve(135,c,22,c),merge(d)]. given #157 (T,wt=8): 249 f3(c1,none_greater) = c1 | Object(f2(c1)). [resolve(248,c,229,b),merge(c)]. given #158 (T,wt=11): 257 f3(c1,none_greater) = c1 | Ex2(id,f2(c1),f2(c1)). [resolve(249,b,43,a)]. given #159 (T,wt=13): 251 f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)) | Ex1(e,c2). [resolve(249,b,205,d),merge(b)]. given #160 (T,wt=13): 252 f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)) | Is_the(c2,none_greater). [resolve(249,b,204,d),merge(b)]. given #161 (A,wt=21): 174 Object(c2) | Object(f2(c1)) | Ex1(none_greater,f3(f3(c1,none_greater),none_greater)) | -Object(f3(c1,none_greater)) | Object(f2(f3(c1,none_greater))). [resolve(135,c,21,c),merge(d)]. given #162 (T,wt=14): 253 f3(c1,none_greater) = c1 | Ex2(id,c2,f2(c1)) | f2(c1) != c2. [resolve(249,b,187,b),flip(d),merge(b)]. given #163 (T,wt=14): 254 f3(c1,none_greater) = c1 | Ex2(id,f2(c1),c2) | f2(c1) != c2. [resolve(249,b,186,b),flip(d),merge(b)]. given #164 (T,wt=14): 255 f3(c1,none_greater) = c1 | Ex2(id,f2(c1),c1) | f2(c1) != c1. [resolve(249,b,48,a),flip(c)]. given #165 (T,wt=14): 256 f3(c1,none_greater) = c1 | Ex2(id,c1,f2(c1)) | f2(c1) != c1. [resolve(249,b,47,a),flip(c)]. given #166 (A,wt=22): 206 f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)) | -Object(f2(c1)) | Ex1(none_greater,f2(c1)) | Ex1(conceivable,f1(f2(c1))). [resolve(179,c,18,c)]. given #167 (T,wt=15): 261 f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)) | -Object(c2) | Ex1(none_greater,c2). [resolve(252,c,36,b)]. given #168 (T,wt=13): 265 f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)) | Ex1(none_greater,c2). [resolve(261,c,178,a),merge(d)]. given #169 (T,wt=15): 262 f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)) | -Object(c2) | -Ex1(e,c2). [resolve(252,c,35,b)]. given #170 (T,wt=12): 270 f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)) | -Object(c2). [resolve(262,d,251,c),merge(d),merge(e)]. given #171 (A,wt=20): 220 Object(c2) | Object(f2(c1)) | Object(f3(f3(c1,none_greater),none_greater)) | Ex2(greater_than,f2(f3(c1,none_greater)),f3(c1,none_greater)). [resolve(162,d,126,a),merge(e)]. given #172 (T,wt=10): 271 f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)). [resolve(270,c,178,a),merge(c)]. given #173 (T,wt=14): 276 f3(c1,none_greater) = c1 | -Object(f3(c1,none_greater)) | Ex1(conceivable,f3(c1,none_greater)). [resolve(271,b,14,b)]. given #174 (T,wt=10): 277 f3(c1,none_greater) = c1 | Ex1(conceivable,f3(c1,none_greater)). [resolve(276,b,229,b),merge(c)]. given #175 (T,wt=15): 273 f3(c1,none_greater) = c1 | -Object(f3(c1,none_greater)) | Ex2(id,f3(c1,none_greater),c1). [resolve(271,b,64,b)]. given #176 (A,wt=18): 233 f3(c1,none_greater) = c1 | -Object(x) | Ex2(id,x,f3(c1,none_greater)) | f3(c1,none_greater) != x. [resolve(229,b,34,b)]. given #177 (T,wt=11): 278 f3(c1,none_greater) = c1 | Ex2(id,f3(c1,none_greater),c1). [resolve(273,b,229,b),merge(c)]. given #178 (T,wt=9): 280 f3(c1,none_greater) = c1 | -Object(f3(c1,none_greater)). [resolve(278,b,33,c),flip(d),merge(d),unit_del(c,19)]. given #179 (T,wt=5): 281 f3(c1,none_greater) = c1. [resolve(280,b,229,b),merge(b)]. given #180 (T,wt=3): 282 Is_the(c1,none_greater). [para(281(a,1),40(d,3)),unit_del(a,19),unit_del(c,20),unit_del(d,52)]. given #181 (A,wt=9): 283 -Object(x) | -Ex1(none_greater,x) | Ex2(id,c1,x). [resolve(282,a,37,b),unit_del(a,19)]. given #182 (F,wt=3): 284 -Ex1(e,c1). [resolve(282,a,35,b),unit_del(a,19)]. given #183 (T,wt=5): 293 Object(c2) | Object(f2(c1)). [resolve(282,a,21,c),unit_del(b,19)]. given #184 (T,wt=6): 287 Ex1(e,c2) | Object(f2(c1)). [resolve(282,a,27,c),unit_del(b,19)]. given #185 (T,wt=6): 290 Is_the(c2,none_greater) | Object(f2(c1)). [resolve(282,a,24,c),unit_del(b,19)]. given #186 (T,wt=6): 291 Object(c2) | Ex1(conceivable,f2(c1)). [resolve(282,a,23,c),unit_del(b,19)]. given #187 (A,wt=7): 285 Ex1(e,c2) | Ex1(conceivable,f2(c1)). [resolve(282,a,29,c),unit_del(b,19)]. given #188 (T,wt=7): 288 Is_the(c2,none_greater) | Ex1(conceivable,f2(c1)). [resolve(282,a,26,c),unit_del(b,19)]. given #189 (T,wt=7): 292 Object(c2) | Ex2(greater_than,f2(c1),c1). [resolve(282,a,22,c),unit_del(b,19)]. given #190 (T,wt=8): 286 Ex1(e,c2) | Ex2(greater_than,f2(c1),c1). [resolve(282,a,28,c),unit_del(b,19)]. given #191 (T,wt=8): 289 Is_the(c2,none_greater) | Ex2(greater_than,f2(c1),c1). [resolve(282,a,25,c),unit_del(b,19)]. given #192 (A,wt=11): 294 Object(c2) | Ex2(id,f2(c1),c1) | f2(c1) != c1. [resolve(293,b,48,a),flip(c)]. given #193 (T,wt=8): 296 Object(c2) | Ex2(id,f2(c1),f2(c1)). [resolve(293,b,43,a)]. given #194 (T,wt=8): 300 Object(f2(c1)) | -Object(c2) | Ex1(none_greater,c2). [resolve(290,a,36,b)]. given #195 (T,wt=8): 301 Object(f2(c1)) | -Object(c2) | -Ex1(e,c2). [resolve(290,a,35,b)]. given #196 (T,wt=5): 311 Object(f2(c1)) | -Object(c2). [resolve(301,c,287,a),merge(c)]. given #197 (A,wt=11): 295 Object(c2) | Ex2(id,c1,f2(c1)) | f2(c1) != c1. [resolve(293,b,47,a),flip(c)]. given #198 (T,wt=9): 306 Ex1(conceivable,f2(c1)) | -Object(c2) | Ex1(none_greater,c2). [resolve(288,a,36,b)]. given #199 (T,wt=9): 307 Ex1(conceivable,f2(c1)) | -Object(c2) | -Ex1(e,c2). [resolve(288,a,35,b)]. given #200 (T,wt=6): 312 Ex1(conceivable,f2(c1)) | -Object(c2). [resolve(307,c,285,a),merge(c)]. given #201 (T,wt=9): 308 Object(c2) | -Object(f2(c1)) | -Ex1(conceivable,f2(c1)). [resolve(292,b,15,d),unit_del(b,19),unit_del(c,20)]. given #202 (A,wt=13): 297 Object(c2) | -Object(x) | Ex2(id,x,f2(c1)) | f2(c1) != x. [resolve(293,b,34,b)]. given #203 (T,wt=5): 313 Object(c2) | -Object(f2(c1)). [resolve(308,c,291,b),merge(c)]. given #204 (T,wt=2): 314 Object(c2). [resolve(313,b,293,b),merge(b)]. given #205 (T,wt=3): 316 Object(f2(c1)). [back_unit_del(311),unit_del(b,314)]. given #206 (T,wt=3): 317 Is_the(c2,none_greater). [back_unit_del(310),unit_del(b,316),unit_del(c,315)]. ============================== PROOF ================================= % Proof 1 at 0.03 (+ 0.01) seconds. % Length of proof is 134. % Level of proof is 40. % Maximum clause weight is 18.000. % Given clauses 206. 1 (all x (Object(x) -> (Ex1(none_greater,x) <-> Ex1(conceivable,x) & -(exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y)))))) # label(non_clause). [assumption]. 2 (exists x (Object(x) & Ex1(none_greater,x))) # label(non_clause). [assumption]. 3 -(exists x (Object(x) & Is_the(x,none_greater) & Ex1(e,x))) -> (all x (Object(x) & Is_the(x,none_greater) -> (exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y))))) # label(non_clause). [assumption]. 4 (exists x (Object(x) & Ex1(none_greater,x))) -> (exists x (Object(x) & Ex1(none_greater,x) & (all y (Object(y) -> (Ex1(none_greater,y) -> Ex2(id,y,x)))))) # label(non_clause). [assumption]. 5 (all x all F (Object(x) & Relation1(F) -> (Is_the(x,F) <-> Ex1(F,x) & (all z (Object(z) & Ex1(F,z) -> Ex2(id,x,z)))))) # label(non_clause). [assumption]. 6 (all x all y (Object(x) & Object(y) -> (Ex2(id,x,y) <-> x = y))) # label(non_clause). [assumption]. 7 (exists x (Object(x) & Is_the(x,none_greater) & Ex1(e,x))) # label(non_clause) # label(goal). [goal]. 9 Relation1(none_greater). [assumption]. 11 -Object(x) | -Relation1(y) | Is_the(x,y) | -Ex1(y,x) | Object(f3(x,y)). [clausify(5)]. 12 -Object(x) | -Relation1(y) | Is_the(x,y) | -Ex1(y,x) | Ex1(y,f3(x,y)). [clausify(5)]. 13 -Object(x) | -Relation1(y) | Is_the(x,y) | -Ex1(y,x) | -Ex2(id,x,f3(x,y)). [clausify(5)]. 15 -Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex2(greater_than,y,x) | -Ex1(conceivable,y). [clausify(1)]. 19 Object(c1). [clausify(2)]. 20 Ex1(none_greater,c1). [clausify(2)]. 21 Object(c2) | -Object(x) | -Is_the(x,none_greater) | Object(f2(x)). [clausify(3)]. 22 Object(c2) | -Object(x) | -Is_the(x,none_greater) | Ex2(greater_than,f2(x),x). [clausify(3)]. 23 Object(c2) | -Object(x) | -Is_the(x,none_greater) | Ex1(conceivable,f2(x)). [clausify(3)]. 24 Is_the(c2,none_greater) | -Object(x) | -Is_the(x,none_greater) | Object(f2(x)). [clausify(3)]. 25 Is_the(c2,none_greater) | -Object(x) | -Is_the(x,none_greater) | Ex2(greater_than,f2(x),x). [clausify(3)]. 26 Is_the(c2,none_greater) | -Object(x) | -Is_the(x,none_greater) | Ex1(conceivable,f2(x)). [clausify(3)]. 27 Ex1(e,c2) | -Object(x) | -Is_the(x,none_greater) | Object(f2(x)). [clausify(3)]. 28 Ex1(e,c2) | -Object(x) | -Is_the(x,none_greater) | Ex2(greater_than,f2(x),x). [clausify(3)]. 29 Ex1(e,c2) | -Object(x) | -Is_the(x,none_greater) | Ex1(conceivable,f2(x)). [clausify(3)]. 30 -Object(x) | -Ex1(none_greater,x) | Object(c3). [clausify(4)]. 32 -Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex1(none_greater,y) | Ex2(id,y,c3). [clausify(4)]. 33 -Object(x) | -Object(y) | -Ex2(id,x,y) | y = x. [clausify(6)]. 34 -Object(x) | -Object(y) | Ex2(id,x,y) | y != x. [clausify(6)]. 35 -Object(x) | -Is_the(x,none_greater) | -Ex1(e,x). [deny(7)]. 38 -Object(x) | Is_the(x,none_greater) | -Ex1(none_greater,x) | Object(f3(x,none_greater)). [resolve(11,b,9,a)]. 39 -Object(x) | Is_the(x,none_greater) | -Ex1(none_greater,x) | Ex1(none_greater,f3(x,none_greater)). [resolve(12,b,9,a)]. 40 -Object(x) | Is_the(x,none_greater) | -Ex1(none_greater,x) | -Ex2(id,x,f3(x,none_greater)). [resolve(13,b,9,a)]. 42 -Object(x) | -Ex1(none_greater,x) | Ex2(id,x,c3). [factor(32,a,c),merge(c)]. 43 -Object(x) | Ex2(id,x,x). [factor(34,a,b),xx(c)]. 45 Object(c3). [resolve(30,b,20,a),unit_del(a,19)]. 49 Is_the(c1,none_greater) | Object(f3(c1,none_greater)). [resolve(38,c,20,a),unit_del(a,19)]. 50 Is_the(c1,none_greater) | Ex1(none_greater,f3(c1,none_greater)). [resolve(39,c,20,a),unit_del(a,19)]. 51 Ex2(id,c1,c3). [resolve(42,b,20,a),unit_del(a,19)]. 52 Ex2(id,c1,c1). [resolve(43,a,19,a)]. 63 c3 = c1. [resolve(51,a,33,c),unit_del(a,19),unit_del(b,45)]. 64 -Object(x) | -Ex1(none_greater,x) | Ex2(id,x,c1). [back_rewrite(42),rewrite([63(5)])]. 67 Object(f3(c1,none_greater)) | Ex1(e,c2) | Ex1(conceivable,f2(c1)). [resolve(49,a,29,c),unit_del(c,19)]. 68 Object(f3(c1,none_greater)) | Ex1(e,c2) | Ex2(greater_than,f2(c1),c1). [resolve(49,a,28,c),unit_del(c,19)]. 69 Object(f3(c1,none_greater)) | Ex1(e,c2) | Object(f2(c1)). [resolve(49,a,27,c),unit_del(c,19)]. 70 Object(f3(c1,none_greater)) | Is_the(c2,none_greater) | Ex1(conceivable,f2(c1)). [resolve(49,a,26,c),unit_del(c,19)]. 71 Object(f3(c1,none_greater)) | Is_the(c2,none_greater) | Ex2(greater_than,f2(c1),c1). [resolve(49,a,25,c),unit_del(c,19)]. 72 Object(f3(c1,none_greater)) | Is_the(c2,none_greater) | Object(f2(c1)). [resolve(49,a,24,c),unit_del(c,19)]. 73 Object(f3(c1,none_greater)) | Object(c2) | Ex1(conceivable,f2(c1)). [resolve(49,a,23,c),unit_del(c,19)]. 74 Object(f3(c1,none_greater)) | Object(c2) | Ex2(greater_than,f2(c1),c1). [resolve(49,a,22,c),unit_del(c,19)]. 75 Object(f3(c1,none_greater)) | Object(c2) | Object(f2(c1)). [resolve(49,a,21,c),unit_del(c,19)]. 78 Ex1(none_greater,f3(c1,none_greater)) | Ex1(e,c2) | Ex1(conceivable,f2(c1)). [resolve(50,a,29,c),unit_del(c,19)]. 79 Ex1(none_greater,f3(c1,none_greater)) | Ex1(e,c2) | Ex2(greater_than,f2(c1),c1). [resolve(50,a,28,c),unit_del(c,19)]. 80 Ex1(none_greater,f3(c1,none_greater)) | Ex1(e,c2) | Object(f2(c1)). [resolve(50,a,27,c),unit_del(c,19)]. 81 Ex1(none_greater,f3(c1,none_greater)) | Is_the(c2,none_greater) | Ex1(conceivable,f2(c1)). [resolve(50,a,26,c),unit_del(c,19)]. 82 Ex1(none_greater,f3(c1,none_greater)) | Is_the(c2,none_greater) | Ex2(greater_than,f2(c1),c1). [resolve(50,a,25,c),unit_del(c,19)]. 83 Ex1(none_greater,f3(c1,none_greater)) | Is_the(c2,none_greater) | Object(f2(c1)). [resolve(50,a,24,c),unit_del(c,19)]. 84 Ex1(none_greater,f3(c1,none_greater)) | Object(c2) | Ex1(conceivable,f2(c1)). [resolve(50,a,23,c),unit_del(c,19)]. 85 Ex1(none_greater,f3(c1,none_greater)) | Object(c2) | Ex2(greater_than,f2(c1),c1). [resolve(50,a,22,c),unit_del(c,19)]. 86 Ex1(none_greater,f3(c1,none_greater)) | Object(c2) | Object(f2(c1)). [resolve(50,a,21,c),unit_del(c,19)]. 94 Object(f3(c1,none_greater)) | Object(f2(c1)) | -Object(c2) | -Ex1(e,c2). [resolve(72,b,35,b)]. 98 Object(c2) | Object(f2(c1)) | -Object(f3(c1,none_greater)) | Ex2(id,f3(c1,none_greater),c1). [resolve(86,a,64,b)]. 104 Object(f3(c1,none_greater)) | Ex1(conceivable,f2(c1)) | -Object(c2) | -Ex1(e,c2). [resolve(70,b,35,b)]. 105 Object(f3(c1,none_greater)) | Object(c2) | -Object(f2(c1)) | -Ex1(conceivable,f2(c1)). [resolve(74,c,15,d),unit_del(c,19),unit_del(d,20)]. 108 Ex1(none_greater,f3(c1,none_greater)) | Object(f2(c1)) | -Object(c2) | -Ex1(e,c2). [resolve(83,b,35,b)]. 109 Object(f3(c1,none_greater)) | Ex1(e,c2) | -Object(f2(c1)) | -Ex1(conceivable,f2(c1)). [resolve(68,c,15,d),unit_del(c,19),unit_del(d,20)]. 113 Object(f3(c1,none_greater)) | Is_the(c2,none_greater) | -Object(f2(c1)) | -Ex1(conceivable,f2(c1)). [resolve(71,c,15,d),unit_del(c,19),unit_del(d,20)]. 116 Ex1(none_greater,f3(c1,none_greater)) | Ex1(conceivable,f2(c1)) | -Object(c2) | -Ex1(e,c2). [resolve(81,b,35,b)]. 117 Ex1(none_greater,f3(c1,none_greater)) | Object(c2) | -Object(f2(c1)) | -Ex1(conceivable,f2(c1)). [resolve(85,c,15,d),unit_del(c,19),unit_del(d,20)]. 119 Object(f3(c1,none_greater)) | Object(f2(c1)) | -Object(c2). [resolve(94,d,69,b),merge(d),merge(e)]. 120 Ex1(none_greater,f3(c1,none_greater)) | Ex1(e,c2) | -Object(f2(c1)) | -Ex1(conceivable,f2(c1)). [resolve(79,c,15,d),unit_del(c,19),unit_del(d,20)]. 121 Ex1(none_greater,f3(c1,none_greater)) | Is_the(c2,none_greater) | -Object(f2(c1)) | -Ex1(conceivable,f2(c1)). [resolve(82,c,15,d),unit_del(c,19),unit_del(d,20)]. 123 Object(f3(c1,none_greater)) | Ex1(conceivable,f2(c1)) | -Object(c2). [resolve(104,d,67,b),merge(d),merge(e)]. 125 Object(f3(c1,none_greater)) | Object(c2) | -Object(f2(c1)). [resolve(105,d,73,c),merge(d),merge(e)]. 126 Object(f3(c1,none_greater)) | Object(c2). [resolve(125,c,75,c),merge(c),merge(d)]. 132 Object(c2) | Object(f2(c1)) | Ex2(id,f3(c1,none_greater),c1). [resolve(98,c,126,a),merge(d)]. 133 Object(c2) | Object(f2(c1)) | -Object(f3(c1,none_greater)) | f3(c1,none_greater) = c1. [resolve(132,c,33,c),flip(e),unit_del(d,19)]. 134 Ex1(none_greater,f3(c1,none_greater)) | Object(f2(c1)) | -Object(c2). [resolve(108,d,80,b),merge(d),merge(e)]. 138 Ex1(none_greater,f3(c1,none_greater)) | Ex1(conceivable,f2(c1)) | -Object(c2). [resolve(116,d,78,b),merge(d),merge(e)]. 139 Ex1(none_greater,f3(c1,none_greater)) | Object(c2) | -Object(f2(c1)). [resolve(117,d,84,c),merge(d),merge(e)]. 140 Object(c2) | Object(f2(c1)) | f3(c1,none_greater) = c1. [resolve(133,c,126,a),merge(d)]. 141 Object(c2) | f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)). [resolve(140,b,139,c),merge(d)]. 147 Object(c2) | f3(c1,none_greater) = c1 | -Object(f3(c1,none_greater)) | Ex2(id,f3(c1,none_greater),c1). [resolve(141,c,64,b)]. 176 Object(c2) | f3(c1,none_greater) = c1 | Ex2(id,f3(c1,none_greater),c1). [resolve(147,c,126,a),merge(d)]. 177 Object(c2) | f3(c1,none_greater) = c1 | -Object(f3(c1,none_greater)). [resolve(176,c,33,c),flip(e),merge(e),unit_del(d,19)]. 178 Object(c2) | f3(c1,none_greater) = c1. [resolve(177,c,126,a),merge(c)]. 179 f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)) | Ex1(conceivable,f2(c1)). [resolve(178,a,138,c)]. 180 f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)) | Object(f2(c1)). [resolve(178,a,134,c)]. 181 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)) | Ex1(conceivable,f2(c1)). [resolve(178,a,123,c)]. 182 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)) | Object(f2(c1)). [resolve(178,a,119,c)]. 193 f3(c1,none_greater) = c1 | Object(f2(c1)) | -Object(f3(c1,none_greater)) | Ex2(id,f3(c1,none_greater),c1). [resolve(180,b,64,b)]. 199 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)) | Is_the(c2,none_greater) | -Object(f2(c1)). [resolve(181,c,113,d),merge(c)]. 200 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)) | Ex1(e,c2) | -Object(f2(c1)). [resolve(181,c,109,d),merge(c)]. 204 f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)) | Is_the(c2,none_greater) | -Object(f2(c1)). [resolve(179,c,121,d),merge(c)]. 205 f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)) | Ex1(e,c2) | -Object(f2(c1)). [resolve(179,c,120,d),merge(c)]. 212 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)) | Is_the(c2,none_greater). [resolve(199,d,182,c),merge(d),merge(e)]. 215 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)) | -Object(c2) | -Ex1(e,c2). [resolve(212,c,35,b)]. 227 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)) | Ex1(e,c2). [resolve(200,d,182,c),merge(d),merge(e)]. 228 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)) | -Object(c2). [resolve(227,c,215,d),merge(c),merge(d)]. 229 f3(c1,none_greater) = c1 | Object(f3(c1,none_greater)). [resolve(228,c,178,a),merge(c)]. 247 f3(c1,none_greater) = c1 | Object(f2(c1)) | Ex2(id,f3(c1,none_greater),c1). [resolve(193,c,229,b),merge(d)]. 248 f3(c1,none_greater) = c1 | Object(f2(c1)) | -Object(f3(c1,none_greater)). [resolve(247,c,33,c),flip(e),merge(e),unit_del(d,19)]. 249 f3(c1,none_greater) = c1 | Object(f2(c1)). [resolve(248,c,229,b),merge(c)]. 251 f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)) | Ex1(e,c2). [resolve(249,b,205,d),merge(b)]. 252 f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)) | Is_the(c2,none_greater). [resolve(249,b,204,d),merge(b)]. 262 f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)) | -Object(c2) | -Ex1(e,c2). [resolve(252,c,35,b)]. 270 f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)) | -Object(c2). [resolve(262,d,251,c),merge(d),merge(e)]. 271 f3(c1,none_greater) = c1 | Ex1(none_greater,f3(c1,none_greater)). [resolve(270,c,178,a),merge(c)]. 273 f3(c1,none_greater) = c1 | -Object(f3(c1,none_greater)) | Ex2(id,f3(c1,none_greater),c1). [resolve(271,b,64,b)]. 278 f3(c1,none_greater) = c1 | Ex2(id,f3(c1,none_greater),c1). [resolve(273,b,229,b),merge(c)]. 280 f3(c1,none_greater) = c1 | -Object(f3(c1,none_greater)). [resolve(278,b,33,c),flip(d),merge(d),unit_del(c,19)]. 281 f3(c1,none_greater) = c1. [resolve(280,b,229,b),merge(b)]. 282 Is_the(c1,none_greater). [para(281(a,1),40(d,3)),unit_del(a,19),unit_del(c,20),unit_del(d,52)]. 285 Ex1(e,c2) | Ex1(conceivable,f2(c1)). [resolve(282,a,29,c),unit_del(b,19)]. 286 Ex1(e,c2) | Ex2(greater_than,f2(c1),c1). [resolve(282,a,28,c),unit_del(b,19)]. 287 Ex1(e,c2) | Object(f2(c1)). [resolve(282,a,27,c),unit_del(b,19)]. 288 Is_the(c2,none_greater) | Ex1(conceivable,f2(c1)). [resolve(282,a,26,c),unit_del(b,19)]. 289 Is_the(c2,none_greater) | Ex2(greater_than,f2(c1),c1). [resolve(282,a,25,c),unit_del(b,19)]. 290 Is_the(c2,none_greater) | Object(f2(c1)). [resolve(282,a,24,c),unit_del(b,19)]. 291 Object(c2) | Ex1(conceivable,f2(c1)). [resolve(282,a,23,c),unit_del(b,19)]. 292 Object(c2) | Ex2(greater_than,f2(c1),c1). [resolve(282,a,22,c),unit_del(b,19)]. 293 Object(c2) | Object(f2(c1)). [resolve(282,a,21,c),unit_del(b,19)]. 301 Object(f2(c1)) | -Object(c2) | -Ex1(e,c2). [resolve(290,a,35,b)]. 307 Ex1(conceivable,f2(c1)) | -Object(c2) | -Ex1(e,c2). [resolve(288,a,35,b)]. 308 Object(c2) | -Object(f2(c1)) | -Ex1(conceivable,f2(c1)). [resolve(292,b,15,d),unit_del(b,19),unit_del(c,20)]. 309 Ex1(e,c2) | -Object(f2(c1)) | -Ex1(conceivable,f2(c1)). [resolve(286,b,15,d),unit_del(b,19),unit_del(c,20)]. 310 Is_the(c2,none_greater) | -Object(f2(c1)) | -Ex1(conceivable,f2(c1)). [resolve(289,b,15,d),unit_del(b,19),unit_del(c,20)]. 311 Object(f2(c1)) | -Object(c2). [resolve(301,c,287,a),merge(c)]. 312 Ex1(conceivable,f2(c1)) | -Object(c2). [resolve(307,c,285,a),merge(c)]. 313 Object(c2) | -Object(f2(c1)). [resolve(308,c,291,b),merge(c)]. 314 Object(c2). [resolve(313,b,293,b),merge(b)]. 315 Ex1(conceivable,f2(c1)). [back_unit_del(312),unit_del(b,314)]. 316 Object(f2(c1)). [back_unit_del(311),unit_del(b,314)]. 317 Is_the(c2,none_greater). [back_unit_del(310),unit_del(b,316),unit_del(c,315)]. 318 Ex1(e,c2). [back_unit_del(309),unit_del(b,316),unit_del(c,315)]. 331 $F. [resolve(317,a,35,b),unit_del(a,314),unit_del(b,318)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=206. Generated=612. Kept=317. proofs=1. Usable=31. Sos=12. Demods=2. Limbo=2, Disabled=305. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=294. Back_subsumed=194. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=2 (0 lex), Back_demodulated=74. Back_unit_deleted=4. Demod_attempts=9172. Demod_rewrites=159. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=764. Nonunit_bsub_feature_tests=591. Megabytes=0.54. User_CPU=0.03, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 34657 exit (max_proofs) Tue May 2 19:54:41 2017