============================== FOF-Prover9 =========================== FOF-Prover9 (32) version 2009-11A, November 2009. Process 23612 was started by mccune on cleo, Tue Nov 3 16:59:10 2009 The command was "/home/mccune/LADR/bin/fof-prover9 -f andrews.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file andrews.in assign(max_seconds,30). formulas(goals). ((exists x all y (p(x) <-> p(y))) <-> ((exists u q(u)) <-> (all v p(v)))) <-> ((exists w all z (q(z) <-> q(w))) <-> ((exists x1 p(x1)) <-> (all x2 q(x2)))). end_of_list. ============================== end of input ========================== % clear(auto_denials), because it is incompatiable with FOF reduction. Attempting problem reduction; original problem has = <210,16384>. Problem reduction (0.01 sec) gives 32 independent subproblems: ( <38,8> <38,8> <37,10> <39,10> <40,8> <40,8> <39,10> <41,10> <39,10> <39,10> <38,12> <40,12> <39,10> <39,10> <38,12> <40,12> <38,8> <40,8> <39,10> <39,10> <38,8> <40,8> <39,10> <39,10> <37,10> <39,10> <38,12> <38,12> <39,10> <41,10> <40,12> <40,12> ). Max nnf_size of subproblems is 41; max cnf_max is 12. ============================== FOF REDUCTION MULTISEARCH ============= Subproblem 1 of 32 (negated): ((exists x ((p(x) | (all y (- p(y)))) & (- p(x) | (all y (p(y)))))) & (exists u q(u)) & (all v p(v)) & (exists w ((- q(w) | (all z (q(z)))) & (q(w) | (all z (- q(z)))))) & (exists x1 p(x1)) & (exists x2 - q(x2))). Max_seconds is 30 for this subproblem. Child search process 23613 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(c1) | -p(x). [assumption]. -p(c1) | p(x). [assumption]. q(c2). [assumption]. p(x). [assumption]. -q(c3) | q(x). [assumption]. q(c3) | -q(x). [assumption]. p(c4). [assumption]. -q(c5). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, c2, c3, c4, c5 ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(neg_binary_resolution). % (HNE depth_diff=0) % clear(ordered_res). % (HNE depth_diff=0) % set(ur_resolution). % (HNE depth_diff=0) % set(ur_resolution) -> set(pos_ur_resolution). % set(ur_resolution) -> set(neg_ur_resolution). Auto_process settings: (no changes). kept: 1 p(c1) | -p(x). [assumption]. kept: 2 -p(c1) | p(x). [assumption]. kept: 3 q(c2). [assumption]. kept: 4 p(x). [assumption]. kept: 5 -q(c3) | q(x). [assumption]. kept: 6 q(c3) | -q(x). [assumption]. kept: 7 -q(c5). [assumption]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 3 q(c2). [assumption]. 4 p(x). [assumption]. 5 -q(c3) | q(x). [assumption]. 6 q(c3) | -q(x). [assumption]. 7 -q(c5). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=2): 3 q(c2). [assumption]. given #2 (I,wt=2): 4 p(x). [assumption]. given #3 (I,wt=4): 5 -q(c3) | q(x). [assumption]. given #4 (I,wt=4): 6 q(c3) | -q(x). [assumption]. given #5 (I,wt=2): 7 -q(c5). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 7. % Level of proof is 2. % Maximum clause weight is 4.000. % Given clauses 5. 3 q(c2). [assumption]. 5 -q(c3) | q(x). [assumption]. 6 q(c3) | -q(x). [assumption]. 7 -q(c5). [assumption]. 8 q(c3). [ur(6,b,3,a)]. 9 -q(c3). [resolve(7,a,5,b)]. 10 $F. [resolve(9,a,8,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=5. Generated=10. Kept=9. proofs=1. Usable=4. Sos=1. Demods=0. Limbo=0, Disabled=11. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=1. Back_subsumed=3. 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=7. Megabytes=0.10. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23613 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 2 of 32 (negated): ((exists x ((p(x) | (all y (- p(y)))) & (- p(x) | (all y (p(y)))))) & (exists u q(u)) & (all v p(v)) & (exists w ((- q(w) | (all z (q(z)))) & (q(w) | (all z (- q(z)))))) & (all x1 - p(x1)) & (all x2 q(x2))). Max_seconds is 30 for this subproblem. Child search process 23614 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(c1) | -p(x). [assumption]. -p(c1) | p(x). [assumption]. q(c2). [assumption]. p(x). [assumption]. -q(c3) | q(x). [assumption]. q(c3) | -q(x). [assumption]. -p(x). [assumption]. q(x). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ q, p ]). Function symbol precedence: function_order([ c1, c2, c3 ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(neg_binary_resolution). % (HNE depth_diff=0) % clear(ordered_res). % (HNE depth_diff=0) % set(ur_resolution). % (HNE depth_diff=0) % set(ur_resolution) -> set(pos_ur_resolution). % set(ur_resolution) -> set(neg_ur_resolution). Auto_process settings: (no changes). kept: 1 p(c1) | -p(x). [assumption]. kept: 2 -p(c1) | p(x). [assumption]. kept: 3 q(c2). [assumption]. kept: 4 p(x). [assumption]. kept: 5 -q(c3) | q(x). [assumption]. kept: 6 q(c3) | -q(x). [assumption]. kept: 7 -p(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 2.000. % Given clauses 0. 4 p(x). [assumption]. 7 -p(x). [assumption]. 8 $F. [resolve(7,a,4,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=7. Kept=7. proofs=1. Usable=0. Sos=0. Demods=0. Limbo=6, Disabled=7. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=0. Back_subsumed=0. 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=0. Megabytes=0.10. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23614 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 3 of 32 (negated): ((exists x ((p(x) | (all y (- p(y)))) & (- p(x) | (all y (p(y)))))) & (exists u q(u)) & (all v p(v)) & (all w ((- q(w) & (exists z (q(z)))) | (q(w) & (exists z (- q(z)))))) & (exists x1 p(x1)) & (all x2 q(x2))). Max_seconds is 30 for this subproblem. Child search process 23615 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(c1) | -p(x). [assumption]. -p(c1) | p(x). [assumption]. q(c2). [assumption]. p(x). [assumption]. -q(x) | -q(f2(x)). [assumption]. q(f1(x)) | q(x). [assumption]. q(f1(x)) | -q(f2(x)). [assumption]. p(c3). [assumption]. q(x). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, c2, c3, f1, f2 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(c1) | -p(x). [assumption]. kept: 2 -p(c1) | p(x). [assumption]. kept: 3 q(c2). [assumption]. kept: 4 p(x). [assumption]. kept: 5 -q(x) | -q(f2(x)). [assumption]. kept: 6 q(f1(x)) | q(x). [assumption]. kept: 7 q(f1(x)) | -q(f2(x)). [assumption]. kept: 8 q(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 5.000. % Given clauses 0. 5 -q(x) | -q(f2(x)). [assumption]. 8 q(x). [assumption]. 9 $F. [back_unit_del(5),unit_del(a,8),unit_del(b,8)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=10. Kept=8. proofs=1. Usable=0. Sos=1. Demods=0. Limbo=1, Disabled=15. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=1. Back_subsumed=5. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=1. 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=9. Megabytes=0.10. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23615 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 4 of 32 (negated): ((exists x ((p(x) | (all y (- p(y)))) & (- p(x) | (all y (p(y)))))) & (exists u q(u)) & (all v p(v)) & (all w ((- q(w) & (exists z (q(z)))) | (q(w) & (exists z (- q(z)))))) & (all x1 - p(x1)) & (exists x2 - q(x2))). Max_seconds is 30 for this subproblem. Child search process 23616 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(c1) | -p(x). [assumption]. -p(c1) | p(x). [assumption]. q(c2). [assumption]. p(x). [assumption]. -q(x) | -q(f2(x)). [assumption]. q(f1(x)) | q(x). [assumption]. q(f1(x)) | -q(f2(x)). [assumption]. -p(x). [assumption]. -q(c3). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, c2, c3, f1, f2 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(c1) | -p(x). [assumption]. kept: 2 -p(c1) | p(x). [assumption]. kept: 3 q(c2). [assumption]. kept: 4 p(x). [assumption]. kept: 5 -q(x) | -q(f2(x)). [assumption]. kept: 6 q(f1(x)) | q(x). [assumption]. kept: 7 q(f1(x)) | -q(f2(x)). [assumption]. 8 -p(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 2.000. % Given clauses 0. 4 p(x). [assumption]. 8 -p(x). [assumption]. 9 $F. [copy(8),unit_del(a,4)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=8. Kept=7. proofs=1. Usable=0. Sos=0. Demods=0. Limbo=7, Disabled=8. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=0. Back_subsumed=0. 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=0. Megabytes=0.10. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23616 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 5 of 32 (negated): ((exists x ((p(x) | (all y (- p(y)))) & (- p(x) | (all y (p(y)))))) & (all u - q(u)) & (exists v - p(v)) & (exists w ((- q(w) | (all z (q(z)))) & (q(w) | (all z (- q(z)))))) & (exists x1 p(x1)) & (exists x2 - q(x2))). Max_seconds is 30 for this subproblem. Child search process 23617 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(c1) | -p(x). [assumption]. -p(c1) | p(x). [assumption]. -q(x). [assumption]. -p(c2). [assumption]. -q(c3) | q(x). [assumption]. q(c3) | -q(x). [assumption]. p(c4). [assumption]. -q(c5). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, c2, c3, c4, c5 ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(neg_binary_resolution). % (HNE depth_diff=0) % clear(ordered_res). % (HNE depth_diff=0) % set(ur_resolution). % (HNE depth_diff=0) % set(ur_resolution) -> set(pos_ur_resolution). % set(ur_resolution) -> set(neg_ur_resolution). Auto_process settings: (no changes). kept: 1 p(c1) | -p(x). [assumption]. kept: 2 -p(c1) | p(x). [assumption]. kept: 3 -q(x). [assumption]. kept: 4 -p(c2). [assumption]. kept: 5 p(c4). [assumption]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 p(c1) | -p(x). [assumption]. 2 -p(c1) | p(x). [assumption]. 3 -q(x). [assumption]. 4 -p(c2). [assumption]. 5 p(c4). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=4): 1 p(c1) | -p(x). [assumption]. given #2 (I,wt=4): 2 -p(c1) | p(x). [assumption]. given #3 (I,wt=2): 3 -q(x). [assumption]. given #4 (I,wt=2): 4 -p(c2). [assumption]. given #5 (I,wt=2): 5 p(c4). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 7. % Level of proof is 2. % Maximum clause weight is 4.000. % Given clauses 5. 1 p(c1) | -p(x). [assumption]. 2 -p(c1) | p(x). [assumption]. 4 -p(c2). [assumption]. 5 p(c4). [assumption]. 6 -p(c1). [resolve(4,a,2,b)]. 7 p(c1). [ur(1,b,5,a)]. 8 $F. [resolve(7,a,6,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=5. Generated=11. Kept=7. proofs=1. Usable=4. Sos=1. Demods=0. Limbo=0, Disabled=9. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=4. 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=3. Megabytes=0.10. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23617 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 6 of 32 (negated): ((exists x ((p(x) | (all y (- p(y)))) & (- p(x) | (all y (p(y)))))) & (all u - q(u)) & (exists v - p(v)) & (exists w ((- q(w) | (all z (q(z)))) & (q(w) | (all z (- q(z)))))) & (all x1 - p(x1)) & (all x2 q(x2))). Max_seconds is 30 for this subproblem. Child search process 23618 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(c1) | -p(x). [assumption]. -p(c1) | p(x). [assumption]. -q(x). [assumption]. -p(c2). [assumption]. -q(c3) | q(x). [assumption]. q(c3) | -q(x). [assumption]. -p(x). [assumption]. q(x). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ q, p ]). Function symbol precedence: function_order([ c1, c2, c3 ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(neg_binary_resolution). % (HNE depth_diff=0) % clear(ordered_res). % (HNE depth_diff=0) % set(ur_resolution). % (HNE depth_diff=0) % set(ur_resolution) -> set(pos_ur_resolution). % set(ur_resolution) -> set(neg_ur_resolution). Auto_process settings: (no changes). kept: 1 p(c1) | -p(x). [assumption]. kept: 2 -p(c1) | p(x). [assumption]. kept: 3 -q(x). [assumption]. kept: 4 -p(c2). [assumption]. kept: 5 -p(x). [assumption]. kept: 6 q(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 2.000. % Given clauses 0. 3 -q(x). [assumption]. 6 q(x). [assumption]. 7 $F. [resolve(6,a,3,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=8. Kept=6. proofs=1. Usable=0. Sos=0. Demods=0. Limbo=5, Disabled=8. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=2. Back_subsumed=0. 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=0. Megabytes=0.10. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23618 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 7 of 32 (negated): ((exists x ((p(x) | (all y (- p(y)))) & (- p(x) | (all y (p(y)))))) & (all u - q(u)) & (exists v - p(v)) & (all w ((- q(w) & (exists z (q(z)))) | (q(w) & (exists z (- q(z)))))) & (exists x1 p(x1)) & (all x2 q(x2))). Max_seconds is 30 for this subproblem. Child search process 23619 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(c1) | -p(x). [assumption]. -p(c1) | p(x). [assumption]. -q(x). [assumption]. -p(c2). [assumption]. -q(x) | -q(f2(x)). [assumption]. q(f1(x)) | q(x). [assumption]. q(f1(x)) | -q(f2(x)). [assumption]. p(c3). [assumption]. q(x). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, c2, c3, f1, f2 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(c1) | -p(x). [assumption]. kept: 2 -p(c1) | p(x). [assumption]. kept: 3 -q(x). [assumption]. kept: 4 -p(c2). [assumption]. 5 q(f1(x)) | q(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 2.000. % Given clauses 0. 3 -q(x). [assumption]. 5 q(f1(x)) | q(x). [assumption]. 6 $F. [copy(5),unit_del(a,3),unit_del(b,3)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=6. Kept=4. proofs=1. Usable=0. Sos=0. Demods=0. Limbo=4, Disabled=6. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=1. Back_subsumed=0. 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=0. Megabytes=0.10. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23619 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 8 of 32 (negated): ((exists x ((p(x) | (all y (- p(y)))) & (- p(x) | (all y (p(y)))))) & (all u - q(u)) & (exists v - p(v)) & (all w ((- q(w) & (exists z (q(z)))) | (q(w) & (exists z (- q(z)))))) & (all x1 - p(x1)) & (exists x2 - q(x2))). Max_seconds is 30 for this subproblem. Child search process 23620 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(c1) | -p(x). [assumption]. -p(c1) | p(x). [assumption]. -q(x). [assumption]. -p(c2). [assumption]. -q(x) | -q(f2(x)). [assumption]. q(f1(x)) | q(x). [assumption]. q(f1(x)) | -q(f2(x)). [assumption]. -p(x). [assumption]. -q(c3). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, c2, c3, f1, f2 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(c1) | -p(x). [assumption]. kept: 2 -p(c1) | p(x). [assumption]. kept: 3 -q(x). [assumption]. kept: 4 -p(c2). [assumption]. 5 q(f1(x)) | q(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 2.000. % Given clauses 0. 3 -q(x). [assumption]. 5 q(f1(x)) | q(x). [assumption]. 6 $F. [copy(5),unit_del(a,3),unit_del(b,3)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=6. Kept=4. proofs=1. Usable=0. Sos=0. Demods=0. Limbo=4, Disabled=6. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=1. Back_subsumed=0. 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=0. Megabytes=0.10. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23620 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 9 of 32 (negated): ((all x ((p(x) & (exists y (- p(y)))) | (- p(x) & (exists y (p(y)))))) & (exists u q(u)) & (exists v - p(v)) & (exists w ((- q(w) | (all z (q(z)))) & (q(w) | (all z (- q(z)))))) & (exists x1 p(x1)) & (exists x2 - q(x2))). Max_seconds is 30 for this subproblem. Child search process 23621 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(x) | p(f2(x)). [assumption]. -p(f1(x)) | -p(x). [assumption]. -p(f1(x)) | p(f2(x)). [assumption]. q(c1). [assumption]. -p(c2). [assumption]. -q(c3) | q(x). [assumption]. q(c3) | -q(x). [assumption]. p(c4). [assumption]. -q(c5). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, c2, c3, c4, c5, f1, f2 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(x) | p(f2(x)). [assumption]. kept: 2 -p(f1(x)) | -p(x). [assumption]. kept: 3 -p(f1(x)) | p(f2(x)). [assumption]. kept: 4 q(c1). [assumption]. kept: 5 -p(c2). [assumption]. kept: 6 -q(c3) | q(x). [assumption]. kept: 7 q(c3) | -q(x). [assumption]. kept: 8 p(c4). [assumption]. kept: 9 -q(c5). [assumption]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 p(x) | p(f2(x)). [assumption]. 2 -p(f1(x)) | -p(x). [assumption]. 3 -p(f1(x)) | p(f2(x)). [assumption]. 4 q(c1). [assumption]. 5 -p(c2). [assumption]. 6 -q(c3) | q(x). [assumption]. 7 q(c3) | -q(x). [assumption]. 8 p(c4). [assumption]. 9 -q(c5). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=5): 1 p(x) | p(f2(x)). [assumption]. given #2 (I,wt=5): 2 -p(f1(x)) | -p(x). [assumption]. given #3 (I,wt=6): 3 -p(f1(x)) | p(f2(x)). [assumption]. given #4 (I,wt=2): 4 q(c1). [assumption]. given #5 (I,wt=2): 5 -p(c2). [assumption]. given #6 (I,wt=4): 6 -q(c3) | q(x). [assumption]. given #7 (I,wt=4): 7 q(c3) | -q(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 7. % Level of proof is 3. % Maximum clause weight is 4.000. % Given clauses 7. 4 q(c1). [assumption]. 6 -q(c3) | q(x). [assumption]. 7 q(c3) | -q(x). [assumption]. 9 -q(c5). [assumption]. 10 q(c3). [resolve(7,b,4,a)]. 11 q(x). [back_unit_del(6),unit_del(a,10)]. 12 $F. [resolve(11,a,9,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=7. Generated=11. Kept=11. proofs=1. Usable=5. Sos=2. Demods=0. Limbo=1, Disabled=11. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=0. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=1. 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=6. Megabytes=0.11. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23621 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 10 of 32 (negated): ((all x ((p(x) & (exists y (- p(y)))) | (- p(x) & (exists y (p(y)))))) & (exists u q(u)) & (exists v - p(v)) & (exists w ((- q(w) | (all z (q(z)))) & (q(w) | (all z (- q(z)))))) & (all x1 - p(x1)) & (all x2 q(x2))). Max_seconds is 30 for this subproblem. Child search process 23622 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(x) | p(f2(x)). [assumption]. -p(f1(x)) | -p(x). [assumption]. -p(f1(x)) | p(f2(x)). [assumption]. q(c1). [assumption]. -p(c2). [assumption]. -q(c3) | q(x). [assumption]. q(c3) | -q(x). [assumption]. -p(x). [assumption]. q(x). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ q, p ]). Function symbol precedence: function_order([ c1, c2, c3, f1, f2 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(x) | p(f2(x)). [assumption]. kept: 2 -p(f1(x)) | -p(x). [assumption]. kept: 3 -p(f1(x)) | p(f2(x)). [assumption]. kept: 4 q(c1). [assumption]. kept: 5 -p(c2). [assumption]. kept: 6 -q(c3) | q(x). [assumption]. kept: 7 q(c3) | -q(x). [assumption]. kept: 8 -p(x). [assumption]. kept: 9 q(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 5.000. % Given clauses 0. 1 p(x) | p(f2(x)). [assumption]. 8 -p(x). [assumption]. 10 $F. [back_unit_del(1),unit_del(a,8),unit_del(b,8)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=10. Kept=9. proofs=1. Usable=0. Sos=3. Demods=0. Limbo=2, Disabled=13. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=0. Back_subsumed=3. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=1. 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=7. Megabytes=0.10. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23622 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 11 of 32 (negated): ((all x ((p(x) & (exists y (- p(y)))) | (- p(x) & (exists y (p(y)))))) & (exists u q(u)) & (exists v - p(v)) & (all w ((- q(w) & (exists z (q(z)))) | (q(w) & (exists z (- q(z)))))) & (exists x1 p(x1)) & (all x2 q(x2))). Max_seconds is 30 for this subproblem. Child search process 23623 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(x) | p(f2(x)). [assumption]. -p(f1(x)) | -p(x). [assumption]. -p(f1(x)) | p(f2(x)). [assumption]. q(c1). [assumption]. -p(c2). [assumption]. -q(x) | -q(f4(x)). [assumption]. q(f3(x)) | q(x). [assumption]. q(f3(x)) | -q(f4(x)). [assumption]. p(c3). [assumption]. q(x). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ q, p ]). Function symbol precedence: function_order([ c1, c2, c3, f1, f2, f3, f4 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(x) | p(f2(x)). [assumption]. kept: 2 -p(f1(x)) | -p(x). [assumption]. kept: 3 -p(f1(x)) | p(f2(x)). [assumption]. kept: 4 q(c1). [assumption]. kept: 5 -p(c2). [assumption]. kept: 6 -q(x) | -q(f4(x)). [assumption]. kept: 7 q(f3(x)) | q(x). [assumption]. kept: 8 q(f3(x)) | -q(f4(x)). [assumption]. kept: 9 p(c3). [assumption]. kept: 10 q(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 5.000. % Given clauses 0. 6 -q(x) | -q(f4(x)). [assumption]. 10 q(x). [assumption]. 11 $F. [back_unit_del(6),unit_del(a,10),unit_del(b,10)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=11. Kept=10. proofs=1. Usable=0. Sos=5. Demods=0. Limbo=1, Disabled=14. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=0. Back_subsumed=3. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=1. 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=8. Megabytes=0.11. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23623 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 12 of 32 (negated): ((all x ((p(x) & (exists y (- p(y)))) | (- p(x) & (exists y (p(y)))))) & (exists u q(u)) & (exists v - p(v)) & (all w ((- q(w) & (exists z (q(z)))) | (q(w) & (exists z (- q(z)))))) & (all x1 - p(x1)) & (exists x2 - q(x2))). Max_seconds is 30 for this subproblem. Child search process 23624 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(x) | p(f2(x)). [assumption]. -p(f1(x)) | -p(x). [assumption]. -p(f1(x)) | p(f2(x)). [assumption]. q(c1). [assumption]. -p(c2). [assumption]. -q(x) | -q(f4(x)). [assumption]. q(f3(x)) | q(x). [assumption]. q(f3(x)) | -q(f4(x)). [assumption]. -p(x). [assumption]. -q(c3). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ q, p ]). Function symbol precedence: function_order([ c1, c2, c3, f1, f2, f3, f4 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(x) | p(f2(x)). [assumption]. kept: 2 -p(f1(x)) | -p(x). [assumption]. kept: 3 -p(f1(x)) | p(f2(x)). [assumption]. kept: 4 q(c1). [assumption]. kept: 5 -p(c2). [assumption]. kept: 6 -q(x) | -q(f4(x)). [assumption]. kept: 7 q(f3(x)) | q(x). [assumption]. kept: 8 q(f3(x)) | -q(f4(x)). [assumption]. kept: 9 -p(x). [assumption]. kept: 10 -q(c3). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 5.000. % Given clauses 0. 1 p(x) | p(f2(x)). [assumption]. 9 -p(x). [assumption]. 11 $F. [back_unit_del(1),unit_del(a,9),unit_del(b,9)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=11. Kept=10. proofs=1. Usable=0. Sos=4. Demods=0. Limbo=2, Disabled=14. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=0. Back_subsumed=3. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=1. 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=8. Megabytes=0.11. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23624 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 13 of 32 (negated): ((all x ((p(x) & (exists y (- p(y)))) | (- p(x) & (exists y (p(y)))))) & (all u - q(u)) & (all v p(v)) & (exists w ((- q(w) | (all z (q(z)))) & (q(w) | (all z (- q(z)))))) & (exists x1 p(x1)) & (exists x2 - q(x2))). Max_seconds is 30 for this subproblem. Child search process 23625 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(x) | p(f2(x)). [assumption]. -p(f1(x)) | -p(x). [assumption]. -p(f1(x)) | p(f2(x)). [assumption]. -q(x). [assumption]. p(x). [assumption]. -q(c1) | q(x). [assumption]. q(c1) | -q(x). [assumption]. p(c2). [assumption]. -q(c3). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, c2, c3, f1, f2 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(x) | p(f2(x)). [assumption]. kept: 2 -p(f1(x)) | -p(x). [assumption]. kept: 3 -p(f1(x)) | p(f2(x)). [assumption]. kept: 4 -q(x). [assumption]. kept: 5 p(x). [assumption]. 6 -q(c1) | q(x). [assumption]. 7 q(c1) | -q(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 5.000. % Given clauses 0. 2 -p(f1(x)) | -p(x). [assumption]. 5 p(x). [assumption]. 8 $F. [back_unit_del(2),unit_del(a,5),unit_del(b,5)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=10. Kept=5. proofs=1. Usable=0. Sos=1. Demods=0. Limbo=1, Disabled=12. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=4. Back_subsumed=2. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=1. 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=5. Megabytes=0.10. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23625 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 14 of 32 (negated): ((all x ((p(x) & (exists y (- p(y)))) | (- p(x) & (exists y (p(y)))))) & (all u - q(u)) & (all v p(v)) & (exists w ((- q(w) | (all z (q(z)))) & (q(w) | (all z (- q(z)))))) & (all x1 - p(x1)) & (all x2 q(x2))). Max_seconds is 30 for this subproblem. Child search process 23626 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(x) | p(f2(x)). [assumption]. -p(f1(x)) | -p(x). [assumption]. -p(f1(x)) | p(f2(x)). [assumption]. -q(x). [assumption]. p(x). [assumption]. -q(c1) | q(x). [assumption]. q(c1) | -q(x). [assumption]. -p(x). [assumption]. q(x). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, f1, f2 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(x) | p(f2(x)). [assumption]. kept: 2 -p(f1(x)) | -p(x). [assumption]. kept: 3 -p(f1(x)) | p(f2(x)). [assumption]. kept: 4 -q(x). [assumption]. kept: 5 p(x). [assumption]. 6 -q(c1) | q(x). [assumption]. 7 q(c1) | -q(x). [assumption]. 8 -p(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 2.000. % Given clauses 0. 5 p(x). [assumption]. 8 -p(x). [assumption]. 9 $F. [copy(8),unit_del(a,5)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=8. Kept=5. proofs=1. Usable=0. Sos=0. Demods=0. Limbo=5, Disabled=8. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=2. Back_subsumed=0. 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=0. Megabytes=0.10. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23626 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 15 of 32 (negated): ((all x ((p(x) & (exists y (- p(y)))) | (- p(x) & (exists y (p(y)))))) & (all u - q(u)) & (all v p(v)) & (all w ((- q(w) & (exists z (q(z)))) | (q(w) & (exists z (- q(z)))))) & (exists x1 p(x1)) & (all x2 q(x2))). Max_seconds is 30 for this subproblem. Child search process 23627 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(x) | p(f2(x)). [assumption]. -p(f1(x)) | -p(x). [assumption]. -p(f1(x)) | p(f2(x)). [assumption]. -q(x). [assumption]. p(x). [assumption]. -q(x) | -q(f4(x)). [assumption]. q(f3(x)) | q(x). [assumption]. q(f3(x)) | -q(f4(x)). [assumption]. p(c1). [assumption]. q(x). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, f1, f2, f3, f4 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(x) | p(f2(x)). [assumption]. kept: 2 -p(f1(x)) | -p(x). [assumption]. kept: 3 -p(f1(x)) | p(f2(x)). [assumption]. kept: 4 -q(x). [assumption]. kept: 5 p(x). [assumption]. 6 q(f3(x)) | q(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 2.000. % Given clauses 0. 4 -q(x). [assumption]. 6 q(f3(x)) | q(x). [assumption]. 7 $F. [copy(6),unit_del(a,4),unit_del(b,4)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=7. Kept=5. proofs=1. Usable=0. Sos=0. Demods=0. Limbo=5, Disabled=7. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=1. Back_subsumed=0. 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=0. Megabytes=0.10. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23627 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 16 of 32 (negated): ((all x ((p(x) & (exists y (- p(y)))) | (- p(x) & (exists y (p(y)))))) & (all u - q(u)) & (all v p(v)) & (all w ((- q(w) & (exists z (q(z)))) | (q(w) & (exists z (- q(z)))))) & (all x1 - p(x1)) & (exists x2 - q(x2))). Max_seconds is 30 for this subproblem. Child search process 23628 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(x) | p(f2(x)). [assumption]. -p(f1(x)) | -p(x). [assumption]. -p(f1(x)) | p(f2(x)). [assumption]. -q(x). [assumption]. p(x). [assumption]. -q(x) | -q(f4(x)). [assumption]. q(f3(x)) | q(x). [assumption]. q(f3(x)) | -q(f4(x)). [assumption]. -p(x). [assumption]. -q(c1). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, f1, f2, f3, f4 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(x) | p(f2(x)). [assumption]. kept: 2 -p(f1(x)) | -p(x). [assumption]. kept: 3 -p(f1(x)) | p(f2(x)). [assumption]. kept: 4 -q(x). [assumption]. kept: 5 p(x). [assumption]. 6 q(f3(x)) | q(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 2.000. % Given clauses 0. 4 -q(x). [assumption]. 6 q(f3(x)) | q(x). [assumption]. 7 $F. [copy(6),unit_del(a,4),unit_del(b,4)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=7. Kept=5. proofs=1. Usable=0. Sos=0. Demods=0. Limbo=5, Disabled=7. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=1. Back_subsumed=0. 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=0. Megabytes=0.10. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23628 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 17 of 32 (negated): ((exists x ((p(x) | (all y (- p(y)))) & (- p(x) | (all y (p(y)))))) & (exists u q(u)) & (exists v - p(v)) & (exists w ((- q(w) | (all z (q(z)))) & (q(w) | (all z (- q(z)))))) & (exists x1 p(x1)) & (all x2 q(x2))). Max_seconds is 30 for this subproblem. Child search process 23629 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(c1) | -p(x). [assumption]. -p(c1) | p(x). [assumption]. q(c2). [assumption]. -p(c3). [assumption]. -q(c4) | q(x). [assumption]. q(c4) | -q(x). [assumption]. p(c5). [assumption]. q(x). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ q, p ]). Function symbol precedence: function_order([ c1, c2, c3, c4, c5 ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(neg_binary_resolution). % (HNE depth_diff=0) % clear(ordered_res). % (HNE depth_diff=0) % set(ur_resolution). % (HNE depth_diff=0) % set(ur_resolution) -> set(pos_ur_resolution). % set(ur_resolution) -> set(neg_ur_resolution). Auto_process settings: (no changes). kept: 1 p(c1) | -p(x). [assumption]. kept: 2 -p(c1) | p(x). [assumption]. kept: 3 q(c2). [assumption]. kept: 4 -p(c3). [assumption]. kept: 5 -q(c4) | q(x). [assumption]. kept: 6 q(c4) | -q(x). [assumption]. kept: 7 p(c5). [assumption]. kept: 8 q(x). [assumption]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 p(c1) | -p(x). [assumption]. 2 -p(c1) | p(x). [assumption]. 4 -p(c3). [assumption]. 7 p(c5). [assumption]. 8 q(x). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=4): 1 p(c1) | -p(x). [assumption]. given #2 (I,wt=4): 2 -p(c1) | p(x). [assumption]. given #3 (I,wt=2): 4 -p(c3). [assumption]. given #4 (I,wt=2): 7 p(c5). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 7. % Level of proof is 2. % Maximum clause weight is 4.000. % Given clauses 4. 1 p(c1) | -p(x). [assumption]. 2 -p(c1) | p(x). [assumption]. 4 -p(c3). [assumption]. 7 p(c5). [assumption]. 9 -p(c1). [resolve(4,a,2,b)]. 10 p(c1). [ur(1,b,7,a)]. 11 $F. [resolve(10,a,9,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=4. Generated=11. Kept=10. proofs=1. Usable=3. Sos=2. Demods=0. Limbo=0, Disabled=12. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=1. Back_subsumed=4. 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=7. Megabytes=0.11. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23629 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 18 of 32 (negated): ((exists x ((p(x) | (all y (- p(y)))) & (- p(x) | (all y (p(y)))))) & (exists u q(u)) & (exists v - p(v)) & (exists w ((- q(w) | (all z (q(z)))) & (q(w) | (all z (- q(z)))))) & (all x1 - p(x1)) & (exists x2 - q(x2))). Max_seconds is 30 for this subproblem. Child search process 23630 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(c1) | -p(x). [assumption]. -p(c1) | p(x). [assumption]. q(c2). [assumption]. -p(c3). [assumption]. -q(c4) | q(x). [assumption]. q(c4) | -q(x). [assumption]. -p(x). [assumption]. -q(c5). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ q, p ]). Function symbol precedence: function_order([ c1, c2, c3, c4, c5 ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(neg_binary_resolution). % (HNE depth_diff=0) % clear(ordered_res). % (HNE depth_diff=0) % set(ur_resolution). % (HNE depth_diff=0) % set(ur_resolution) -> set(pos_ur_resolution). % set(ur_resolution) -> set(neg_ur_resolution). Auto_process settings: (no changes). kept: 1 p(c1) | -p(x). [assumption]. kept: 2 -p(c1) | p(x). [assumption]. kept: 3 q(c2). [assumption]. kept: 4 -p(c3). [assumption]. kept: 5 -q(c4) | q(x). [assumption]. kept: 6 q(c4) | -q(x). [assumption]. kept: 7 -p(x). [assumption]. kept: 8 -q(c5). [assumption]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 3 q(c2). [assumption]. 5 -q(c4) | q(x). [assumption]. 6 q(c4) | -q(x). [assumption]. 7 -p(x). [assumption]. 8 -q(c5). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=2): 3 q(c2). [assumption]. given #2 (I,wt=4): 5 -q(c4) | q(x). [assumption]. given #3 (I,wt=4): 6 q(c4) | -q(x). [assumption]. given #4 (I,wt=2): 7 -p(x). [assumption]. given #5 (I,wt=2): 8 -q(c5). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 7. % Level of proof is 2. % Maximum clause weight is 4.000. % Given clauses 5. 3 q(c2). [assumption]. 5 -q(c4) | q(x). [assumption]. 6 q(c4) | -q(x). [assumption]. 8 -q(c5). [assumption]. 9 q(c4). [ur(6,b,3,a)]. 10 -q(c4). [resolve(8,a,5,b)]. 11 $F. [resolve(10,a,9,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=5. Generated=10. Kept=10. proofs=1. Usable=4. Sos=1. Demods=0. Limbo=0, Disabled=12. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=0. Back_subsumed=4. 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=7. Megabytes=0.11. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23630 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 19 of 32 (negated): ((exists x ((p(x) | (all y (- p(y)))) & (- p(x) | (all y (p(y)))))) & (exists u q(u)) & (exists v - p(v)) & (all w ((- q(w) & (exists z (q(z)))) | (q(w) & (exists z (- q(z)))))) & (exists x1 p(x1)) & (exists x2 - q(x2))). Max_seconds is 30 for this subproblem. Child search process 23631 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(c1) | -p(x). [assumption]. -p(c1) | p(x). [assumption]. q(c2). [assumption]. -p(c3). [assumption]. -q(x) | -q(f2(x)). [assumption]. q(f1(x)) | q(x). [assumption]. q(f1(x)) | -q(f2(x)). [assumption]. p(c4). [assumption]. -q(c5). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, c2, c3, c4, c5, f1, f2 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(c1) | -p(x). [assumption]. kept: 2 -p(c1) | p(x). [assumption]. kept: 3 q(c2). [assumption]. kept: 4 -p(c3). [assumption]. kept: 5 -q(x) | -q(f2(x)). [assumption]. kept: 6 q(f1(x)) | q(x). [assumption]. kept: 7 q(f1(x)) | -q(f2(x)). [assumption]. kept: 8 p(c4). [assumption]. kept: 9 -q(c5). [assumption]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 p(c1) | -p(x). [assumption]. 2 -p(c1) | p(x). [assumption]. 3 q(c2). [assumption]. 4 -p(c3). [assumption]. 5 -q(x) | -q(f2(x)). [assumption]. 6 q(f1(x)) | q(x). [assumption]. 7 q(f1(x)) | -q(f2(x)). [assumption]. 8 p(c4). [assumption]. 9 -q(c5). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=4): 1 p(c1) | -p(x). [assumption]. given #2 (I,wt=4): 2 -p(c1) | p(x). [assumption]. given #3 (I,wt=2): 3 q(c2). [assumption]. given #4 (I,wt=2): 4 -p(c3). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 7. % Level of proof is 3. % Maximum clause weight is 4.000. % Given clauses 4. 1 p(c1) | -p(x). [assumption]. 2 -p(c1) | p(x). [assumption]. 4 -p(c3). [assumption]. 8 p(c4). [assumption]. 10 -p(c1). [ur(2,b,4,a)]. 11 -p(x). [back_unit_del(1),unit_del(a,10)]. 12 $F. [resolve(11,a,8,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=4. Generated=11. Kept=11. proofs=1. Usable=2. Sos=5. Demods=0. Limbo=1, Disabled=11. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=0. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=1. 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=6. Megabytes=0.11. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23631 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 20 of 32 (negated): ((exists x ((p(x) | (all y (- p(y)))) & (- p(x) | (all y (p(y)))))) & (exists u q(u)) & (exists v - p(v)) & (all w ((- q(w) & (exists z (q(z)))) | (q(w) & (exists z (- q(z)))))) & (all x1 - p(x1)) & (all x2 q(x2))). Max_seconds is 30 for this subproblem. Child search process 23632 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(c1) | -p(x). [assumption]. -p(c1) | p(x). [assumption]. q(c2). [assumption]. -p(c3). [assumption]. -q(x) | -q(f2(x)). [assumption]. q(f1(x)) | q(x). [assumption]. q(f1(x)) | -q(f2(x)). [assumption]. -p(x). [assumption]. q(x). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ q, p ]). Function symbol precedence: function_order([ c1, c2, c3, f1, f2 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(c1) | -p(x). [assumption]. kept: 2 -p(c1) | p(x). [assumption]. kept: 3 q(c2). [assumption]. kept: 4 -p(c3). [assumption]. kept: 5 -q(x) | -q(f2(x)). [assumption]. kept: 6 q(f1(x)) | q(x). [assumption]. kept: 7 q(f1(x)) | -q(f2(x)). [assumption]. kept: 8 -p(x). [assumption]. kept: 9 q(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 5.000. % Given clauses 0. 5 -q(x) | -q(f2(x)). [assumption]. 9 q(x). [assumption]. 10 $F. [back_unit_del(5),unit_del(a,9),unit_del(b,9)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=10. Kept=9. proofs=1. Usable=0. Sos=1. Demods=0. Limbo=1, Disabled=16. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=0. Back_subsumed=6. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=1. 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=9. Megabytes=0.11. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23632 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 21 of 32 (negated): ((exists x ((p(x) | (all y (- p(y)))) & (- p(x) | (all y (p(y)))))) & (all u - q(u)) & (all v p(v)) & (exists w ((- q(w) | (all z (q(z)))) & (q(w) | (all z (- q(z)))))) & (exists x1 p(x1)) & (all x2 q(x2))). Max_seconds is 30 for this subproblem. Child search process 23633 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(c1) | -p(x). [assumption]. -p(c1) | p(x). [assumption]. -q(x). [assumption]. p(x). [assumption]. -q(c2) | q(x). [assumption]. q(c2) | -q(x). [assumption]. p(c3). [assumption]. q(x). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, c2, c3 ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(neg_binary_resolution). % (HNE depth_diff=0) % clear(ordered_res). % (HNE depth_diff=0) % set(ur_resolution). % (HNE depth_diff=0) % set(ur_resolution) -> set(pos_ur_resolution). % set(ur_resolution) -> set(neg_ur_resolution). Auto_process settings: (no changes). kept: 1 p(c1) | -p(x). [assumption]. kept: 2 -p(c1) | p(x). [assumption]. kept: 3 -q(x). [assumption]. kept: 4 p(x). [assumption]. kept: 5 q(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 2.000. % Given clauses 0. 3 -q(x). [assumption]. 5 q(x). [assumption]. 6 $F. [resolve(5,a,3,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=8. Kept=5. proofs=1. Usable=0. Sos=0. Demods=0. Limbo=4, Disabled=8. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=3. Back_subsumed=0. 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=0. Megabytes=0.10. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23633 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 22 of 32 (negated): ((exists x ((p(x) | (all y (- p(y)))) & (- p(x) | (all y (p(y)))))) & (all u - q(u)) & (all v p(v)) & (exists w ((- q(w) | (all z (q(z)))) & (q(w) | (all z (- q(z)))))) & (all x1 - p(x1)) & (exists x2 - q(x2))). Max_seconds is 30 for this subproblem. Child search process 23634 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(c1) | -p(x). [assumption]. -p(c1) | p(x). [assumption]. -q(x). [assumption]. p(x). [assumption]. -q(c2) | q(x). [assumption]. q(c2) | -q(x). [assumption]. -p(x). [assumption]. -q(c3). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, c2, c3 ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(neg_binary_resolution). % (HNE depth_diff=0) % clear(ordered_res). % (HNE depth_diff=0) % set(ur_resolution). % (HNE depth_diff=0) % set(ur_resolution) -> set(pos_ur_resolution). % set(ur_resolution) -> set(neg_ur_resolution). Auto_process settings: (no changes). kept: 1 p(c1) | -p(x). [assumption]. kept: 2 -p(c1) | p(x). [assumption]. kept: 3 -q(x). [assumption]. kept: 4 p(x). [assumption]. kept: 5 -p(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 2.000. % Given clauses 0. 4 p(x). [assumption]. 5 -p(x). [assumption]. 6 $F. [resolve(5,a,4,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=7. Kept=5. proofs=1. Usable=0. Sos=0. Demods=0. Limbo=4, Disabled=7. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=2. Back_subsumed=0. 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=0. Megabytes=0.10. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23634 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 23 of 32 (negated): ((exists x ((p(x) | (all y (- p(y)))) & (- p(x) | (all y (p(y)))))) & (all u - q(u)) & (all v p(v)) & (all w ((- q(w) & (exists z (q(z)))) | (q(w) & (exists z (- q(z)))))) & (exists x1 p(x1)) & (exists x2 - q(x2))). Max_seconds is 30 for this subproblem. Child search process 23635 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(c1) | -p(x). [assumption]. -p(c1) | p(x). [assumption]. -q(x). [assumption]. p(x). [assumption]. -q(x) | -q(f2(x)). [assumption]. q(f1(x)) | q(x). [assumption]. q(f1(x)) | -q(f2(x)). [assumption]. p(c2). [assumption]. -q(c3). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, c2, c3, f1, f2 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(c1) | -p(x). [assumption]. kept: 2 -p(c1) | p(x). [assumption]. kept: 3 -q(x). [assumption]. kept: 4 p(x). [assumption]. 5 q(f1(x)) | q(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 2.000. % Given clauses 0. 3 -q(x). [assumption]. 5 q(f1(x)) | q(x). [assumption]. 6 $F. [copy(5),unit_del(a,3),unit_del(b,3)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=6. Kept=4. proofs=1. Usable=0. Sos=0. Demods=0. Limbo=4, Disabled=6. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=1. Back_subsumed=0. 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=0. Megabytes=0.10. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23635 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 24 of 32 (negated): ((exists x ((p(x) | (all y (- p(y)))) & (- p(x) | (all y (p(y)))))) & (all u - q(u)) & (all v p(v)) & (all w ((- q(w) & (exists z (q(z)))) | (q(w) & (exists z (- q(z)))))) & (all x1 - p(x1)) & (all x2 q(x2))). Max_seconds is 30 for this subproblem. Child search process 23636 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(c1) | -p(x). [assumption]. -p(c1) | p(x). [assumption]. -q(x). [assumption]. p(x). [assumption]. -q(x) | -q(f2(x)). [assumption]. q(f1(x)) | q(x). [assumption]. q(f1(x)) | -q(f2(x)). [assumption]. -p(x). [assumption]. q(x). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, f1, f2 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(c1) | -p(x). [assumption]. kept: 2 -p(c1) | p(x). [assumption]. kept: 3 -q(x). [assumption]. kept: 4 p(x). [assumption]. 5 q(f1(x)) | q(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 2.000. % Given clauses 0. 3 -q(x). [assumption]. 5 q(f1(x)) | q(x). [assumption]. 6 $F. [copy(5),unit_del(a,3),unit_del(b,3)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=6. Kept=4. proofs=1. Usable=0. Sos=0. Demods=0. Limbo=4, Disabled=6. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=1. Back_subsumed=0. 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=0. Megabytes=0.10. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23636 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 25 of 32 (negated): ((all x ((p(x) & (exists y (- p(y)))) | (- p(x) & (exists y (p(y)))))) & (exists u q(u)) & (all v p(v)) & (exists w ((- q(w) | (all z (q(z)))) & (q(w) | (all z (- q(z)))))) & (exists x1 p(x1)) & (all x2 q(x2))). Max_seconds is 30 for this subproblem. Child search process 23637 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(x) | p(f2(x)). [assumption]. -p(f1(x)) | -p(x). [assumption]. -p(f1(x)) | p(f2(x)). [assumption]. q(c1). [assumption]. p(x). [assumption]. -q(c2) | q(x). [assumption]. q(c2) | -q(x). [assumption]. p(c3). [assumption]. q(x). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, c2, c3, f1, f2 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(x) | p(f2(x)). [assumption]. kept: 2 -p(f1(x)) | -p(x). [assumption]. kept: 3 -p(f1(x)) | p(f2(x)). [assumption]. kept: 4 q(c1). [assumption]. kept: 5 p(x). [assumption]. kept: 6 -q(c2) | q(x). [assumption]. kept: 7 q(c2) | -q(x). [assumption]. kept: 8 q(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 5.000. % Given clauses 0. 2 -p(f1(x)) | -p(x). [assumption]. 5 p(x). [assumption]. 9 $F. [back_unit_del(2),unit_del(a,5),unit_del(b,5)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=10. Kept=8. proofs=1. Usable=0. Sos=1. Demods=0. Limbo=4, Disabled=12. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=1. Back_subsumed=2. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=1. 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=5. Megabytes=0.11. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23637 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 26 of 32 (negated): ((all x ((p(x) & (exists y (- p(y)))) | (- p(x) & (exists y (p(y)))))) & (exists u q(u)) & (all v p(v)) & (exists w ((- q(w) | (all z (q(z)))) & (q(w) | (all z (- q(z)))))) & (all x1 - p(x1)) & (exists x2 - q(x2))). Max_seconds is 30 for this subproblem. Child search process 23638 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(x) | p(f2(x)). [assumption]. -p(f1(x)) | -p(x). [assumption]. -p(f1(x)) | p(f2(x)). [assumption]. q(c1). [assumption]. p(x). [assumption]. -q(c2) | q(x). [assumption]. q(c2) | -q(x). [assumption]. -p(x). [assumption]. -q(c3). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, c2, c3, f1, f2 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(x) | p(f2(x)). [assumption]. kept: 2 -p(f1(x)) | -p(x). [assumption]. kept: 3 -p(f1(x)) | p(f2(x)). [assumption]. kept: 4 q(c1). [assumption]. kept: 5 p(x). [assumption]. kept: 6 -q(c2) | q(x). [assumption]. kept: 7 q(c2) | -q(x). [assumption]. 8 -p(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 2.000. % Given clauses 0. 5 p(x). [assumption]. 8 -p(x). [assumption]. 9 $F. [copy(8),unit_del(a,5)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=8. Kept=7. proofs=1. Usable=0. Sos=0. Demods=0. Limbo=7, Disabled=8. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=0. Back_subsumed=0. 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=0. Megabytes=0.11. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23638 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 27 of 32 (negated): ((all x ((p(x) & (exists y (- p(y)))) | (- p(x) & (exists y (p(y)))))) & (exists u q(u)) & (all v p(v)) & (all w ((- q(w) & (exists z (q(z)))) | (q(w) & (exists z (- q(z)))))) & (exists x1 p(x1)) & (exists x2 - q(x2))). Max_seconds is 30 for this subproblem. Child search process 23639 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(x) | p(f2(x)). [assumption]. -p(f1(x)) | -p(x). [assumption]. -p(f1(x)) | p(f2(x)). [assumption]. q(c1). [assumption]. p(x). [assumption]. -q(x) | -q(f4(x)). [assumption]. q(f3(x)) | q(x). [assumption]. q(f3(x)) | -q(f4(x)). [assumption]. p(c2). [assumption]. -q(c3). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, c2, c3, f1, f2, f3, f4 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(x) | p(f2(x)). [assumption]. kept: 2 -p(f1(x)) | -p(x). [assumption]. kept: 3 -p(f1(x)) | p(f2(x)). [assumption]. kept: 4 q(c1). [assumption]. kept: 5 p(x). [assumption]. kept: 6 -q(x) | -q(f4(x)). [assumption]. kept: 7 q(f3(x)) | q(x). [assumption]. kept: 8 q(f3(x)) | -q(f4(x)). [assumption]. kept: 9 -q(c3). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 5.000. % Given clauses 0. 2 -p(f1(x)) | -p(x). [assumption]. 5 p(x). [assumption]. 10 $F. [back_unit_del(2),unit_del(a,5),unit_del(b,5)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=11. Kept=9. proofs=1. Usable=0. Sos=1. Demods=0. Limbo=5, Disabled=13. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=1. Back_subsumed=2. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=1. 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=5. Megabytes=0.11. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23639 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 28 of 32 (negated): ((all x ((p(x) & (exists y (- p(y)))) | (- p(x) & (exists y (p(y)))))) & (exists u q(u)) & (all v p(v)) & (all w ((- q(w) & (exists z (q(z)))) | (q(w) & (exists z (- q(z)))))) & (all x1 - p(x1)) & (all x2 q(x2))). Max_seconds is 30 for this subproblem. Child search process 23640 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(x) | p(f2(x)). [assumption]. -p(f1(x)) | -p(x). [assumption]. -p(f1(x)) | p(f2(x)). [assumption]. q(c1). [assumption]. p(x). [assumption]. -q(x) | -q(f4(x)). [assumption]. q(f3(x)) | q(x). [assumption]. q(f3(x)) | -q(f4(x)). [assumption]. -p(x). [assumption]. q(x). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ q, p ]). Function symbol precedence: function_order([ c1, f1, f2, f3, f4 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(x) | p(f2(x)). [assumption]. kept: 2 -p(f1(x)) | -p(x). [assumption]. kept: 3 -p(f1(x)) | p(f2(x)). [assumption]. kept: 4 q(c1). [assumption]. kept: 5 p(x). [assumption]. kept: 6 -q(x) | -q(f4(x)). [assumption]. kept: 7 q(f3(x)) | q(x). [assumption]. kept: 8 q(f3(x)) | -q(f4(x)). [assumption]. 9 -p(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 2.000. % Given clauses 0. 5 p(x). [assumption]. 9 -p(x). [assumption]. 10 $F. [copy(9),unit_del(a,5)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=9. Kept=8. proofs=1. Usable=0. Sos=0. Demods=0. Limbo=8, Disabled=9. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=0. Back_subsumed=0. 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=0. Megabytes=0.11. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23640 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 29 of 32 (negated): ((all x ((p(x) & (exists y (- p(y)))) | (- p(x) & (exists y (p(y)))))) & (all u - q(u)) & (exists v - p(v)) & (exists w ((- q(w) | (all z (q(z)))) & (q(w) | (all z (- q(z)))))) & (exists x1 p(x1)) & (all x2 q(x2))). Max_seconds is 30 for this subproblem. Child search process 23641 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(x) | p(f2(x)). [assumption]. -p(f1(x)) | -p(x). [assumption]. -p(f1(x)) | p(f2(x)). [assumption]. -q(x). [assumption]. -p(c1). [assumption]. -q(c2) | q(x). [assumption]. q(c2) | -q(x). [assumption]. p(c3). [assumption]. q(x). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, c2, c3, f1, f2 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(x) | p(f2(x)). [assumption]. kept: 2 -p(f1(x)) | -p(x). [assumption]. kept: 3 -p(f1(x)) | p(f2(x)). [assumption]. kept: 4 -q(x). [assumption]. kept: 5 -p(c1). [assumption]. 6 -q(c2) | q(x). [assumption]. 7 q(c2) | -q(x). [assumption]. kept: 8 p(c3). [assumption]. 9 q(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 2.000. % Given clauses 0. 4 -q(x). [assumption]. 9 q(x). [assumption]. 10 $F. [copy(9),unit_del(a,4)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=9. Kept=6. proofs=1. Usable=0. Sos=0. Demods=0. Limbo=6, Disabled=9. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=2. Back_subsumed=0. 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=0. Megabytes=0.11. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23641 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 30 of 32 (negated): ((all x ((p(x) & (exists y (- p(y)))) | (- p(x) & (exists y (p(y)))))) & (all u - q(u)) & (exists v - p(v)) & (exists w ((- q(w) | (all z (q(z)))) & (q(w) | (all z (- q(z)))))) & (all x1 - p(x1)) & (exists x2 - q(x2))). Max_seconds is 30 for this subproblem. Child search process 23642 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(x) | p(f2(x)). [assumption]. -p(f1(x)) | -p(x). [assumption]. -p(f1(x)) | p(f2(x)). [assumption]. -q(x). [assumption]. -p(c1). [assumption]. -q(c2) | q(x). [assumption]. q(c2) | -q(x). [assumption]. -p(x). [assumption]. -q(c3). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, c2, c3, f1, f2 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(x) | p(f2(x)). [assumption]. kept: 2 -p(f1(x)) | -p(x). [assumption]. kept: 3 -p(f1(x)) | p(f2(x)). [assumption]. kept: 4 -q(x). [assumption]. kept: 5 -p(c1). [assumption]. 6 -q(c2) | q(x). [assumption]. 7 q(c2) | -q(x). [assumption]. kept: 8 -p(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 5.000. % Given clauses 0. 1 p(x) | p(f2(x)). [assumption]. 8 -p(x). [assumption]. 9 $F. [back_unit_del(1),unit_del(a,8),unit_del(b,8)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=10. Kept=6. proofs=1. Usable=0. Sos=1. Demods=0. Limbo=1, Disabled=13. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=3. Back_subsumed=3. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=1. 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=5. Megabytes=0.11. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23642 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 31 of 32 (negated): ((all x ((p(x) & (exists y (- p(y)))) | (- p(x) & (exists y (p(y)))))) & (all u - q(u)) & (exists v - p(v)) & (all w ((- q(w) & (exists z (q(z)))) | (q(w) & (exists z (- q(z)))))) & (exists x1 p(x1)) & (exists x2 - q(x2))). Max_seconds is 30 for this subproblem. Child search process 23643 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(x) | p(f2(x)). [assumption]. -p(f1(x)) | -p(x). [assumption]. -p(f1(x)) | p(f2(x)). [assumption]. -q(x). [assumption]. -p(c1). [assumption]. -q(x) | -q(f4(x)). [assumption]. q(f3(x)) | q(x). [assumption]. q(f3(x)) | -q(f4(x)). [assumption]. p(c2). [assumption]. -q(c3). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ p, q ]). Function symbol precedence: function_order([ c1, c2, c3, f1, f2, f3, f4 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(x) | p(f2(x)). [assumption]. kept: 2 -p(f1(x)) | -p(x). [assumption]. kept: 3 -p(f1(x)) | p(f2(x)). [assumption]. kept: 4 -q(x). [assumption]. kept: 5 -p(c1). [assumption]. 6 q(f3(x)) | q(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 2.000. % Given clauses 0. 4 -q(x). [assumption]. 6 q(f3(x)) | q(x). [assumption]. 7 $F. [copy(6),unit_del(a,4),unit_del(b,4)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=7. Kept=5. proofs=1. Usable=0. Sos=0. Demods=0. Limbo=5, Disabled=7. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=1. Back_subsumed=0. 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=0. Megabytes=0.11. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23643 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== continuing FOF reduction multisearch == Subproblem 32 of 32 (negated): ((all x ((p(x) & (exists y (- p(y)))) | (- p(x) & (exists y (p(y)))))) & (all u - q(u)) & (exists v - p(v)) & (all w ((- q(w) & (exists z (q(z)))) | (q(w) & (exists z (- q(z)))))) & (all x1 - p(x1)) & (all x2 q(x2))). Max_seconds is 30 for this subproblem. Child search process 23644 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). p(x) | p(f2(x)). [assumption]. -p(f1(x)) | -p(x). [assumption]. -p(f1(x)) | p(f2(x)). [assumption]. -q(x). [assumption]. -p(c1). [assumption]. -q(x) | -q(f4(x)). [assumption]. q(f3(x)) | q(x). [assumption]. q(f3(x)) | -q(f4(x)). [assumption]. -p(x). [assumption]. q(x). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ q, p ]). Function symbol precedence: function_order([ c1, f1, f2, f3, f4 ]). After inverse_order: (no changes). 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(unit_deletion). % (non-Horn) kept: 1 p(x) | p(f2(x)). [assumption]. kept: 2 -p(f1(x)) | -p(x). [assumption]. kept: 3 -p(f1(x)) | p(f2(x)). [assumption]. kept: 4 -q(x). [assumption]. kept: 5 -p(c1). [assumption]. 6 q(f3(x)) | q(x). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 2.000. % Given clauses 0. 4 -q(x). [assumption]. 6 q(f3(x)) | q(x). [assumption]. 7 $F. [copy(6),unit_del(a,4),unit_del(b,4)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=7. Kept=5. proofs=1. Usable=0. Sos=0. Demods=0. Limbo=5, Disabled=7. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=1. Back_subsumed=0. 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=0. Megabytes=0.11. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 23644 exit (max_proofs) Tue Nov 3 16:59:10 2009 ============================== end of multisearch ==================== All 32 subproblems have been proved, so we are done. Total user_CPU=0.05, system_CPU=0.02, wall_clock=0. THEOREM PROVED Exiting. Process 23612 exit (max_proofs) Tue Nov 3 16:59:10 2009