============================== FOF-Prover9 =========================== FOF-Prover9 (32) version March-2007, March 2007. Process 20860 was started by mccune on cleo, Mon Mar 19 17:01:17 2007 The command was "/home/mccune/bin/fof-prover9 -f ALG043+1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file ALG043+1.in set(prolog_style_variables). formulas(assumptions). e0 != e1 & e0 != e2 & e0 != e3 & e1 != e2 & e1 != e3 & e2 != e3. op(e0,e0) = e0 & op(e0,e1) = e1 & op(e0,e2) = e2 & op(e0,e3) = e3 & op(e1,e0) = e1 & op(e1,e1) = e0 & op(e1,e2) = e3 & op(e1,e3) = e2 & op(e2,e0) = e2 & op(e2,e1) = e3 & op(e2,e2) = e0 & op(e2,e3) = e1 & op(e3,e0) = e3 & op(e3,e1) = e2 & op(e3,e2) = e1 & op(e3,e3) = e0. unit = e0. -((op(e0,e0) = e0 & op(e1,e1) = e0 & op(e2,e2) = e0 & op(e3,e3) = e0 | op(e0,e0) = e1 & op(e1,e1) = e1 & op(e2,e2) = e1 & op(e3,e3) = e1 | op(e0,e0) = e2 & op(e1,e1) = e2 & op(e2,e2) = e2 & op(e3,e3) = e2 | op(e0,e0) = e3 & op(e1,e1) = e3 & op(e2,e2) = e3 & op(e3,e3) = e3) & (op(e0,e0) = e0 | op(e0,e0) = e1 | op(e0,e0) = e2 | op(e0,e0) = e3) & (op(e0,e1) = e0 | op(e0,e1) = e1 | op(e0,e1) = e2 | op(e0,e1) = e3) & (op(e0,e2) = e0 | op(e0,e2) = e1 | op(e0,e2) = e2 | op(e0,e2) = e3) & (op(e0,e3) = e0 | op(e0,e3) = e1 | op(e0,e3) = e2 | op(e0,e3) = e3) & (op(e1,e0) = e0 | op(e1,e0) = e1 | op(e1,e0) = e2 | op(e1,e0) = e3) & (op(e1,e1) = e0 | op(e1,e1) = e1 | op(e1,e1) = e2 | op(e1,e1) = e3) & (op(e1,e2) = e0 | op(e1,e2) = e1 | op(e1,e2) = e2 | op(e1,e2) = e3) & (op(e1,e3) = e0 | op(e1,e3) = e1 | op(e1,e3) = e2 | op(e1,e3) = e3) & (op(e2,e0) = e0 | op(e2,e0) = e1 | op(e2,e0) = e2 | op(e2,e0) = e3) & (op(e2,e1) = e0 | op(e2,e1) = e1 | op(e2,e1) = e2 | op(e2,e1) = e3) & (op(e2,e2) = e0 | op(e2,e2) = e1 | op(e2,e2) = e2 | op(e2,e2) = e3) & (op(e2,e3) = e0 | op(e2,e3) = e1 | op(e2,e3) = e2 | op(e2,e3) = e3) & (op(e3,e0) = e0 | op(e3,e0) = e1 | op(e3,e0) = e2 | op(e3,e0) = e3) & (op(e3,e1) = e0 | op(e3,e1) = e1 | op(e3,e1) = e2 | op(e3,e1) = e3) & (op(e3,e2) = e0 | op(e3,e2) = e1 | op(e3,e2) = e2 | op(e3,e2) = e3) & (op(e3,e3) = e0 | op(e3,e3) = e1 | op(e3,e3) = e2 | op(e3,e3) = e3) & op(unit,e0) = e0 & op(e0,unit) = e0 & op(unit,e1) = e1 & op(e1,unit) = e1 & op(unit,e2) = e2 & op(e2,unit) = e2 & op(unit,e3) = e3 & op(e3,unit) = e3 & (unit = e0 | unit = e1 | unit = e2 | unit = e3) & (op(e0,e0) = e0 | op(e0,e1) = e0 | op(e0,e2) = e0 | op(e0,e3) = e0) & (op(e0,e0) = e0 | op(e1,e0) = e0 | op(e2,e0) = e0 | op(e3,e0) = e0) & (op(e0,e0) = e1 | op(e0,e1) = e1 | op(e0,e2) = e1 | op(e0,e3) = e1) & (op(e0,e0) = e1 | op(e1,e0) = e1 | op(e2,e0) = e1 | op(e3,e0) = e1) & (op(e0,e0) = e2 | op(e0,e1) = e2 | op(e0,e2) = e2 | op(e0,e3) = e2) & (op(e0,e0) = e2 | op(e1,e0) = e2 | op(e2,e0) = e2 | op(e3,e0) = e2) & (op(e0,e0) = e3 | op(e0,e1) = e3 | op(e0,e2) = e3 | op(e0,e3) = e3) & (op(e0,e0) = e3 | op(e1,e0) = e3 | op(e2,e0) = e3 | op(e3,e0) = e3) & (op(e1,e0) = e0 | op(e1,e1) = e0 | op(e1,e2) = e0 | op(e1,e3) = e0) & (op(e0,e1) = e0 | op(e1,e1) = e0 | op(e2,e1) = e0 | op(e3,e1) = e0) & (op(e1,e0) = e1 | op(e1,e1) = e1 | op(e1,e2) = e1 | op(e1,e3) = e1) & (op(e0,e1) = e1 | op(e1,e1) = e1 | op(e2,e1) = e1 | op(e3,e1) = e1) & (op(e1,e0) = e2 | op(e1,e1) = e2 | op(e1,e2) = e2 | op(e1,e3) = e2) & (op(e0,e1) = e2 | op(e1,e1) = e2 | op(e2,e1) = e2 | op(e3,e1) = e2) & (op(e1,e0) = e3 | op(e1,e1) = e3 | op(e1,e2) = e3 | op(e1,e3) = e3) & (op(e0,e1) = e3 | op(e1,e1) = e3 | op(e2,e1) = e3 | op(e3,e1) = e3) & (op(e2,e0) = e0 | op(e2,e1) = e0 | op(e2,e2) = e0 | op(e2,e3) = e0) & (op(e0,e2) = e0 | op(e1,e2) = e0 | op(e2,e2) = e0 | op(e3,e2) = e0) & (op(e2,e0) = e1 | op(e2,e1) = e1 | op(e2,e2) = e1 | op(e2,e3) = e1) & (op(e0,e2) = e1 | op(e1,e2) = e1 | op(e2,e2) = e1 | op(e3,e2) = e1) & (op(e2,e0) = e2 | op(e2,e1) = e2 | op(e2,e2) = e2 | op(e2,e3) = e2) & (op(e0,e2) = e2 | op(e1,e2) = e2 | op(e2,e2) = e2 | op(e3,e2) = e2) & (op(e2,e0) = e3 | op(e2,e1) = e3 | op(e2,e2) = e3 | op(e2,e3) = e3) & (op(e0,e2) = e3 | op(e1,e2) = e3 | op(e2,e2) = e3 | op(e3,e2) = e3) & (op(e3,e0) = e0 | op(e3,e1) = e0 | op(e3,e2) = e0 | op(e3,e3) = e0) & (op(e0,e3) = e0 | op(e1,e3) = e0 | op(e2,e3) = e0 | op(e3,e3) = e0) & (op(e3,e0) = e1 | op(e3,e1) = e1 | op(e3,e2) = e1 | op(e3,e3) = e1) & (op(e0,e3) = e1 | op(e1,e3) = e1 | op(e2,e3) = e1 | op(e3,e3) = e1) & (op(e3,e0) = e2 | op(e3,e1) = e2 | op(e3,e2) = e2 | op(e3,e3) = e2) & (op(e0,e3) = e2 | op(e1,e3) = e2 | op(e2,e3) = e2 | op(e3,e3) = e2) & (op(e3,e0) = e3 | op(e3,e1) = e3 | op(e3,e2) = e3 | op(e3,e3) = e3) & (op(e0,e3) = e3 | op(e1,e3) = e3 | op(e2,e3) = e3 | op(e3,e3) = e3)). end_of_list. ============================== end of input ========================== % clear(auto_denials), because it is incompatiable with FOF reduction. Attempting problem reduction; original problem has = <529,23>. Problem reduction (0.07 sec) gives 8 independent subproblems: ( <32,24> <32,24> <32,24> <32,24> <32,24> <32,24> <32,24> <32,24> ). Max nnf_size of subproblems is 32; max cnf_max is 24. ============================== FOF REDUCTION MULTISEARCH ============= Subproblem 1 of 8 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e2,e1) & - =(e3,e1) & - =(e3,e2) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e2,e0),e2) & =(op(e2,e1),e3) & =(op(e2,e2),e0) & =(op(e2,e3),e1) & =(op(e3,e0),e3) & =(op(e3,e1),e2) & =(op(e3,e2),e1) & =(op(e3,e3),e0) & =(unit,e0) & - =(op(unit,e0),e0)). Child search process 20861 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e3 != e2. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e3. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e1. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e2. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e0. [assumption]. unit = e0. [assumption]. op(unit,e0) != e0. [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ e0, e1, e2, e3, unit, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 4. % Level of proof is 1. % Maximum clause weight is 5. % Given clauses 0. 7 op(e0,e0) = e0. [assumption]. 23 unit = e0. [assumption]. 24 op(unit,e0) != e0. [assumption]. 25 $F. [copy(24),rewrite(23(1),7(3)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=24. Kept=23. proofs=1. Usable=0. Sos=0. Demods=17. Limbo=23, Disabled=24. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=0. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=17 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=163. Demod_rewrites=2. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.33. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 20861 exit (max_proofs) Mon Mar 19 17:01:17 2007 ============================== continuing FOF reduction multisearch == Subproblem 2 of 8 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e2,e1) & - =(e3,e1) & - =(e3,e2) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e2,e0),e2) & =(op(e2,e1),e3) & =(op(e2,e2),e0) & =(op(e2,e3),e1) & =(op(e3,e0),e3) & =(op(e3,e1),e2) & =(op(e3,e2),e1) & =(op(e3,e3),e0) & =(unit,e0) & - =(op(e0,unit),e0)). Child search process 20862 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e3 != e2. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e3. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e1. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e2. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e0. [assumption]. unit = e0. [assumption]. op(e0,unit) != e0. [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ e0, e1, e2, e3, unit, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 4. % Level of proof is 1. % Maximum clause weight is 5. % Given clauses 0. 7 op(e0,e0) = e0. [assumption]. 23 unit = e0. [assumption]. 24 op(e0,unit) != e0. [assumption]. 25 $F. [copy(24),rewrite(23(2),7(3)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=24. Kept=23. proofs=1. Usable=0. Sos=0. Demods=17. Limbo=23, Disabled=24. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=0. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=17 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=163. Demod_rewrites=2. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.33. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 20862 exit (max_proofs) Mon Mar 19 17:01:17 2007 ============================== continuing FOF reduction multisearch == Subproblem 3 of 8 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e2,e1) & - =(e3,e1) & - =(e3,e2) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e2,e0),e2) & =(op(e2,e1),e3) & =(op(e2,e2),e0) & =(op(e2,e3),e1) & =(op(e3,e0),e3) & =(op(e3,e1),e2) & =(op(e3,e2),e1) & =(op(e3,e3),e0) & =(unit,e0) & - =(op(unit,e1),e1)). Child search process 20863 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e3 != e2. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e3. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e1. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e2. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e0. [assumption]. unit = e0. [assumption]. op(unit,e1) != e1. [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ e0, e1, e2, e3, unit, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 4. % Level of proof is 1. % Maximum clause weight is 5. % Given clauses 0. 8 op(e0,e1) = e1. [assumption]. 23 unit = e0. [assumption]. 24 op(unit,e1) != e1. [assumption]. 25 $F. [copy(24),rewrite(23(1),8(3)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=24. Kept=23. proofs=1. Usable=0. Sos=0. Demods=17. Limbo=23, Disabled=24. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=0. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=17 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=163. Demod_rewrites=2. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.33. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 20863 exit (max_proofs) Mon Mar 19 17:01:17 2007 ============================== continuing FOF reduction multisearch == Subproblem 4 of 8 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e2,e1) & - =(e3,e1) & - =(e3,e2) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e2,e0),e2) & =(op(e2,e1),e3) & =(op(e2,e2),e0) & =(op(e2,e3),e1) & =(op(e3,e0),e3) & =(op(e3,e1),e2) & =(op(e3,e2),e1) & =(op(e3,e3),e0) & =(unit,e0) & - =(op(e1,unit),e1)). Child search process 20864 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e3 != e2. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e3. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e1. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e2. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e0. [assumption]. unit = e0. [assumption]. op(e1,unit) != e1. [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ e0, e1, e2, e3, unit, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 4. % Level of proof is 1. % Maximum clause weight is 5. % Given clauses 0. 11 op(e1,e0) = e1. [assumption]. 23 unit = e0. [assumption]. 24 op(e1,unit) != e1. [assumption]. 25 $F. [copy(24),rewrite(23(2),11(3)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=24. Kept=23. proofs=1. Usable=0. Sos=0. Demods=17. Limbo=23, Disabled=24. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=0. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=17 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=163. Demod_rewrites=2. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.33. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 20864 exit (max_proofs) Mon Mar 19 17:01:17 2007 ============================== continuing FOF reduction multisearch == Subproblem 5 of 8 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e2,e1) & - =(e3,e1) & - =(e3,e2) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e2,e0),e2) & =(op(e2,e1),e3) & =(op(e2,e2),e0) & =(op(e2,e3),e1) & =(op(e3,e0),e3) & =(op(e3,e1),e2) & =(op(e3,e2),e1) & =(op(e3,e3),e0) & =(unit,e0) & - =(op(unit,e2),e2)). Child search process 20865 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e3 != e2. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e3. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e1. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e2. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e0. [assumption]. unit = e0. [assumption]. op(unit,e2) != e2. [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ e0, e1, e2, e3, unit, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 4. % Level of proof is 1. % Maximum clause weight is 5. % Given clauses 0. 9 op(e0,e2) = e2. [assumption]. 23 unit = e0. [assumption]. 24 op(unit,e2) != e2. [assumption]. 25 $F. [copy(24),rewrite(23(1),9(3)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=24. Kept=23. proofs=1. Usable=0. Sos=0. Demods=17. Limbo=23, Disabled=24. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=0. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=17 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=163. Demod_rewrites=2. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.33. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 20865 exit (max_proofs) Mon Mar 19 17:01:17 2007 ============================== continuing FOF reduction multisearch == Subproblem 6 of 8 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e2,e1) & - =(e3,e1) & - =(e3,e2) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e2,e0),e2) & =(op(e2,e1),e3) & =(op(e2,e2),e0) & =(op(e2,e3),e1) & =(op(e3,e0),e3) & =(op(e3,e1),e2) & =(op(e3,e2),e1) & =(op(e3,e3),e0) & =(unit,e0) & - =(op(e2,unit),e2)). Child search process 20866 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e3 != e2. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e3. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e1. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e2. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e0. [assumption]. unit = e0. [assumption]. op(e2,unit) != e2. [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ e0, e1, e2, e3, unit, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 4. % Level of proof is 1. % Maximum clause weight is 5. % Given clauses 0. 15 op(e2,e0) = e2. [assumption]. 23 unit = e0. [assumption]. 24 op(e2,unit) != e2. [assumption]. 25 $F. [copy(24),rewrite(23(2),15(3)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=24. Kept=23. proofs=1. Usable=0. Sos=0. Demods=17. Limbo=23, Disabled=24. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=0. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=17 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=163. Demod_rewrites=2. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.33. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 20866 exit (max_proofs) Mon Mar 19 17:01:17 2007 ============================== continuing FOF reduction multisearch == Subproblem 7 of 8 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e2,e1) & - =(e3,e1) & - =(e3,e2) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e2,e0),e2) & =(op(e2,e1),e3) & =(op(e2,e2),e0) & =(op(e2,e3),e1) & =(op(e3,e0),e3) & =(op(e3,e1),e2) & =(op(e3,e2),e1) & =(op(e3,e3),e0) & =(unit,e0) & - =(op(unit,e3),e3)). Child search process 20867 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e3 != e2. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e3. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e1. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e2. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e0. [assumption]. unit = e0. [assumption]. op(unit,e3) != e3. [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ e0, e1, e2, e3, unit, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 4. % Level of proof is 1. % Maximum clause weight is 5. % Given clauses 0. 10 op(e0,e3) = e3. [assumption]. 23 unit = e0. [assumption]. 24 op(unit,e3) != e3. [assumption]. 25 $F. [copy(24),rewrite(23(1),10(3)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=24. Kept=23. proofs=1. Usable=0. Sos=0. Demods=17. Limbo=23, Disabled=24. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=0. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=17 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=163. Demod_rewrites=2. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.33. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 20867 exit (max_proofs) Mon Mar 19 17:01:17 2007 ============================== continuing FOF reduction multisearch == Subproblem 8 of 8 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e2,e1) & - =(e3,e1) & - =(e3,e2) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e2,e0),e2) & =(op(e2,e1),e3) & =(op(e2,e2),e0) & =(op(e2,e3),e1) & =(op(e3,e0),e3) & =(op(e3,e1),e2) & =(op(e3,e2),e1) & =(op(e3,e3),e0) & =(unit,e0) & - =(op(e3,unit),e3)). Child search process 20868 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e3 != e2. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e3. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e1. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e2. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e0. [assumption]. unit = e0. [assumption]. op(e3,unit) != e3. [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ e0, e1, e2, e3, unit, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 4. % Level of proof is 1. % Maximum clause weight is 5. % Given clauses 0. 19 op(e3,e0) = e3. [assumption]. 23 unit = e0. [assumption]. 24 op(e3,unit) != e3. [assumption]. 25 $F. [copy(24),rewrite(23(2),19(3)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=24. Kept=23. proofs=1. Usable=0. Sos=0. Demods=17. Limbo=23, Disabled=24. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=0. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=17 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=163. Demod_rewrites=2. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.33. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 20868 exit (max_proofs) Mon Mar 19 17:01:17 2007 ============================== end of multisearch ==================== All 8 subproblems have been proved, so we are done. Total user_CPU=0.08, system_CPU=0.01, wall_clock=0. THEOREM PROVED Exiting. Process 20860 exit (max_proofs) Mon Mar 19 17:01:17 2007