============================== FOF-Prover9 =========================== FOF-Prover9 (32) version 2008-05A, May 2008. Process 21754 was started by mccune on cleo, Wed May 7 22:14:44 2008 The command was "/home/mccune/LADR/bin/fof-prover9 -f ALG189+1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file ALG189+1.in assign(max_seconds,30). set(prolog_style_variables). formulas(assumptions). e0 != e1 & e0 != e2 & e0 != e3 & e0 != e4 & e1 != e2 & e1 != e3 & e1 != e4 & e2 != e3 & e2 != e4 & e3 != e4. op(e0,e0) = e0 & op(e0,e1) = e3 & op(e0,e2) = e4 & op(e0,e3) = e2 & op(e0,e4) = e1 & op(e1,e0) = e2 & op(e1,e1) = e1 & op(e1,e2) = e3 & op(e1,e3) = e4 & op(e1,e4) = e0 & op(e2,e0) = e1 & op(e2,e1) = e4 & op(e2,e2) = e2 & op(e2,e3) = e0 & op(e2,e4) = e3 & op(e3,e0) = e4 & op(e3,e1) = e0 & op(e3,e2) = e1 & op(e3,e3) = e3 & op(e3,e4) = e2 & op(e4,e0) = e3 & op(e4,e1) = e2 & op(e4,e2) = e0 & op(e4,e3) = e1 & op(e4,e4) = e4. -(op(op(e0,e0),e0) = e0 & op(op(e0,e1),e1) = e0 & op(op(e0,e2),e2) = e0 & op(op(e0,e3),e3) = e0 & op(op(e0,e4),e4) = e0 & op(op(e1,e0),e0) = e1 & op(op(e1,e1),e1) = e1 & op(op(e1,e2),e2) = e1 & op(op(e1,e3),e3) = e1 & op(op(e1,e4),e4) = e1 & op(op(e2,e0),e0) = e2 & op(op(e2,e1),e1) = e2 & op(op(e2,e2),e2) = e2 & op(op(e2,e3),e3) = e2 & op(op(e2,e4),e4) = e2 & op(op(e3,e0),e0) = e3 & op(op(e3,e1),e1) = e3 & op(op(e3,e2),e2) = e3 & op(op(e3,e3),e3) = e3 & op(op(e3,e4),e4) = e3 & op(op(e4,e0),e0) = e4 & op(op(e4,e1),e1) = e4 & op(op(e4,e2),e2) = e4 & op(op(e4,e3),e3) = e4 & op(op(e4,e4),e4) = e4 & (op(e0,e0) = e0 | op(e0,e0) = e1 | op(e0,e0) = e2 | op(e0,e0) = e3 | op(e0,e0) = e4) & (op(e0,e1) = e0 | op(e0,e1) = e1 | op(e0,e1) = e2 | op(e0,e1) = e3 | op(e0,e1) = e4) & (op(e0,e2) = e0 | op(e0,e2) = e1 | op(e0,e2) = e2 | op(e0,e2) = e3 | op(e0,e2) = e4) & (op(e0,e3) = e0 | op(e0,e3) = e1 | op(e0,e3) = e2 | op(e0,e3) = e3 | op(e0,e3) = e4) & (op(e0,e4) = e0 | op(e0,e4) = e1 | op(e0,e4) = e2 | op(e0,e4) = e3 | op(e0,e4) = e4) & (op(e1,e0) = e0 | op(e1,e0) = e1 | op(e1,e0) = e2 | op(e1,e0) = e3 | op(e1,e0) = e4) & (op(e1,e1) = e0 | op(e1,e1) = e1 | op(e1,e1) = e2 | op(e1,e1) = e3 | op(e1,e1) = e4) & (op(e1,e2) = e0 | op(e1,e2) = e1 | op(e1,e2) = e2 | op(e1,e2) = e3 | op(e1,e2) = e4) & (op(e1,e3) = e0 | op(e1,e3) = e1 | op(e1,e3) = e2 | op(e1,e3) = e3 | op(e1,e3) = e4) & (op(e1,e4) = e0 | op(e1,e4) = e1 | op(e1,e4) = e2 | op(e1,e4) = e3 | op(e1,e4) = e4) & (op(e2,e0) = e0 | op(e2,e0) = e1 | op(e2,e0) = e2 | op(e2,e0) = e3 | op(e2,e0) = e4) & (op(e2,e1) = e0 | op(e2,e1) = e1 | op(e2,e1) = e2 | op(e2,e1) = e3 | op(e2,e1) = e4) & (op(e2,e2) = e0 | op(e2,e2) = e1 | op(e2,e2) = e2 | op(e2,e2) = e3 | op(e2,e2) = e4) & (op(e2,e3) = e0 | op(e2,e3) = e1 | op(e2,e3) = e2 | op(e2,e3) = e3 | op(e2,e3) = e4) & (op(e2,e4) = e0 | op(e2,e4) = e1 | op(e2,e4) = e2 | op(e2,e4) = e3 | op(e2,e4) = e4) & (op(e3,e0) = e0 | op(e3,e0) = e1 | op(e3,e0) = e2 | op(e3,e0) = e3 | op(e3,e0) = e4) & (op(e3,e1) = e0 | op(e3,e1) = e1 | op(e3,e1) = e2 | op(e3,e1) = e3 | op(e3,e1) = e4) & (op(e3,e2) = e0 | op(e3,e2) = e1 | op(e3,e2) = e2 | op(e3,e2) = e3 | op(e3,e2) = e4) & (op(e3,e3) = e0 | op(e3,e3) = e1 | op(e3,e3) = e2 | op(e3,e3) = e3 | op(e3,e3) = e4) & (op(e3,e4) = e0 | op(e3,e4) = e1 | op(e3,e4) = e2 | op(e3,e4) = e3 | op(e3,e4) = e4) & (op(e4,e0) = e0 | op(e4,e0) = e1 | op(e4,e0) = e2 | op(e4,e0) = e3 | op(e4,e0) = e4) & (op(e4,e1) = e0 | op(e4,e1) = e1 | op(e4,e1) = e2 | op(e4,e1) = e3 | op(e4,e1) = e4) & (op(e4,e2) = e0 | op(e4,e2) = e1 | op(e4,e2) = e2 | op(e4,e2) = e3 | op(e4,e2) = e4) & (op(e4,e3) = e0 | op(e4,e3) = e1 | op(e4,e3) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4) & (op(e4,e4) = e0 | op(e4,e4) = e1 | op(e4,e4) = e2 | op(e4,e4) = e3 | op(e4,e4) = e4) & (op(e0,e0) = e0 | op(e0,e1) = e0 | op(e0,e2) = e0 | op(e0,e3) = e0 | op(e0,e4) = e0) & (op(e0,e0) = e0 | op(e1,e0) = e0 | op(e2,e0) = e0 | op(e3,e0) = e0 | op(e4,e0) = e0) & (op(e0,e0) = e1 | op(e0,e1) = e1 | op(e0,e2) = e1 | op(e0,e3) = e1 | op(e0,e4) = e1) & (op(e0,e0) = e1 | op(e1,e0) = e1 | op(e2,e0) = e1 | op(e3,e0) = e1 | op(e4,e0) = e1) & (op(e0,e0) = e2 | op(e0,e1) = e2 | op(e0,e2) = e2 | op(e0,e3) = e2 | op(e0,e4) = e2) & (op(e0,e0) = e2 | op(e1,e0) = e2 | op(e2,e0) = e2 | op(e3,e0) = e2 | op(e4,e0) = e2) & (op(e0,e0) = e3 | op(e0,e1) = e3 | op(e0,e2) = e3 | op(e0,e3) = e3 | op(e0,e4) = e3) & (op(e0,e0) = e3 | op(e1,e0) = e3 | op(e2,e0) = e3 | op(e3,e0) = e3 | op(e4,e0) = e3) & (op(e0,e0) = e4 | op(e0,e1) = e4 | op(e0,e2) = e4 | op(e0,e3) = e4 | op(e0,e4) = e4) & (op(e0,e0) = e4 | op(e1,e0) = e4 | op(e2,e0) = e4 | op(e3,e0) = e4 | op(e4,e0) = e4) & (op(e1,e0) = e0 | op(e1,e1) = e0 | op(e1,e2) = e0 | op(e1,e3) = e0 | op(e1,e4) = e0) & (op(e0,e1) = e0 | op(e1,e1) = e0 | op(e2,e1) = e0 | op(e3,e1) = e0 | op(e4,e1) = e0) & (op(e1,e0) = e1 | op(e1,e1) = e1 | op(e1,e2) = e1 | op(e1,e3) = e1 | op(e1,e4) = e1) & (op(e0,e1) = e1 | op(e1,e1) = e1 | op(e2,e1) = e1 | op(e3,e1) = e1 | op(e4,e1) = e1) & (op(e1,e0) = e2 | op(e1,e1) = e2 | op(e1,e2) = e2 | op(e1,e3) = e2 | op(e1,e4) = e2) & (op(e0,e1) = e2 | op(e1,e1) = e2 | op(e2,e1) = e2 | op(e3,e1) = e2 | op(e4,e1) = e2) & (op(e1,e0) = e3 | op(e1,e1) = e3 | op(e1,e2) = e3 | op(e1,e3) = e3 | op(e1,e4) = e3) & (op(e0,e1) = e3 | op(e1,e1) = e3 | op(e2,e1) = e3 | op(e3,e1) = e3 | op(e4,e1) = e3) & (op(e1,e0) = e4 | op(e1,e1) = e4 | op(e1,e2) = e4 | op(e1,e3) = e4 | op(e1,e4) = e4) & (op(e0,e1) = e4 | op(e1,e1) = e4 | op(e2,e1) = e4 | op(e3,e1) = e4 | op(e4,e1) = e4) & (op(e2,e0) = e0 | op(e2,e1) = e0 | op(e2,e2) = e0 | op(e2,e3) = e0 | op(e2,e4) = e0) & (op(e0,e2) = e0 | op(e1,e2) = e0 | op(e2,e2) = e0 | op(e3,e2) = e0 | op(e4,e2) = e0) & (op(e2,e0) = e1 | op(e2,e1) = e1 | op(e2,e2) = e1 | op(e2,e3) = e1 | op(e2,e4) = e1) & (op(e0,e2) = e1 | op(e1,e2) = e1 | op(e2,e2) = e1 | op(e3,e2) = e1 | op(e4,e2) = e1) & (op(e2,e0) = e2 | op(e2,e1) = e2 | op(e2,e2) = e2 | op(e2,e3) = e2 | op(e2,e4) = e2) & (op(e0,e2) = e2 | op(e1,e2) = e2 | op(e2,e2) = e2 | op(e3,e2) = e2 | op(e4,e2) = e2) & (op(e2,e0) = e3 | op(e2,e1) = e3 | op(e2,e2) = e3 | op(e2,e3) = e3 | op(e2,e4) = e3) & (op(e0,e2) = e3 | op(e1,e2) = e3 | op(e2,e2) = e3 | op(e3,e2) = e3 | op(e4,e2) = e3) & (op(e2,e0) = e4 | op(e2,e1) = e4 | op(e2,e2) = e4 | op(e2,e3) = e4 | op(e2,e4) = e4) & (op(e0,e2) = e4 | op(e1,e2) = e4 | op(e2,e2) = e4 | op(e3,e2) = e4 | op(e4,e2) = e4) & (op(e3,e0) = e0 | op(e3,e1) = e0 | op(e3,e2) = e0 | op(e3,e3) = e0 | op(e3,e4) = e0) & (op(e0,e3) = e0 | op(e1,e3) = e0 | op(e2,e3) = e0 | op(e3,e3) = e0 | op(e4,e3) = e0) & (op(e3,e0) = e1 | op(e3,e1) = e1 | op(e3,e2) = e1 | op(e3,e3) = e1 | op(e3,e4) = e1) & (op(e0,e3) = e1 | op(e1,e3) = e1 | op(e2,e3) = e1 | op(e3,e3) = e1 | op(e4,e3) = e1) & (op(e3,e0) = e2 | op(e3,e1) = e2 | op(e3,e2) = e2 | op(e3,e3) = e2 | op(e3,e4) = e2) & (op(e0,e3) = e2 | op(e1,e3) = e2 | op(e2,e3) = e2 | op(e3,e3) = e2 | op(e4,e3) = e2) & (op(e3,e0) = e3 | op(e3,e1) = e3 | op(e3,e2) = e3 | op(e3,e3) = e3 | op(e3,e4) = e3) & (op(e0,e3) = e3 | op(e1,e3) = e3 | op(e2,e3) = e3 | op(e3,e3) = e3 | op(e4,e3) = e3) & (op(e3,e0) = e4 | op(e3,e1) = e4 | op(e3,e2) = e4 | op(e3,e3) = e4 | op(e3,e4) = e4) & (op(e0,e3) = e4 | op(e1,e3) = e4 | op(e2,e3) = e4 | op(e3,e3) = e4 | op(e4,e3) = e4) & (op(e4,e0) = e0 | op(e4,e1) = e0 | op(e4,e2) = e0 | op(e4,e3) = e0 | op(e4,e4) = e0) & (op(e0,e4) = e0 | op(e1,e4) = e0 | op(e2,e4) = e0 | op(e3,e4) = e0 | op(e4,e4) = e0) & (op(e4,e0) = e1 | op(e4,e1) = e1 | op(e4,e2) = e1 | op(e4,e3) = e1 | op(e4,e4) = e1) & (op(e0,e4) = e1 | op(e1,e4) = e1 | op(e2,e4) = e1 | op(e3,e4) = e1 | op(e4,e4) = e1) & (op(e4,e0) = e2 | op(e4,e1) = e2 | op(e4,e2) = e2 | op(e4,e3) = e2 | op(e4,e4) = e2) & (op(e0,e4) = e2 | op(e1,e4) = e2 | op(e2,e4) = e2 | op(e3,e4) = e2 | op(e4,e4) = e2) & (op(e4,e0) = e3 | op(e4,e1) = e3 | op(e4,e2) = e3 | op(e4,e3) = e3 | op(e4,e4) = e3) & (op(e0,e4) = e3 | op(e1,e4) = e3 | op(e2,e4) = e3 | op(e3,e4) = e3 | op(e4,e4) = e3) & (op(e4,e0) = e4 | op(e4,e1) = e4 | op(e4,e2) = e4 | op(e4,e3) = e4 | op(e4,e4) = e4) & (op(e0,e4) = e4 | op(e1,e4) = e4 | op(e2,e4) = e4 | op(e3,e4) = e4 | op(e4,e4) = e4) & op(op(e0,e0),op(e0,e0)) = e0 & op(op(e1,e0),op(e0,e1)) = e0 & op(op(e2,e0),op(e0,e2)) = e0 & op(op(e3,e0),op(e0,e3)) = e0 & op(op(e4,e0),op(e0,e4)) = e0 & op(op(e0,e1),op(e1,e0)) = e1 & op(op(e1,e1),op(e1,e1)) = e1 & op(op(e2,e1),op(e1,e2)) = e1 & op(op(e3,e1),op(e1,e3)) = e1 & op(op(e4,e1),op(e1,e4)) = e1 & op(op(e0,e2),op(e2,e0)) = e2 & op(op(e1,e2),op(e2,e1)) = e2 & op(op(e2,e2),op(e2,e2)) = e2 & op(op(e3,e2),op(e2,e3)) = e2 & op(op(e4,e2),op(e2,e4)) = e2 & op(op(e0,e3),op(e3,e0)) = e3 & op(op(e1,e3),op(e3,e1)) = e3 & op(op(e2,e3),op(e3,e2)) = e3 & op(op(e3,e3),op(e3,e3)) = e3 & op(op(e4,e3),op(e3,e4)) = e3 & op(op(e0,e4),op(e4,e0)) = e4 & op(op(e1,e4),op(e4,e1)) = e4 & op(op(e2,e4),op(e4,e2)) = e4 & op(op(e3,e4),op(e4,e3)) = e4 & op(op(e4,e4),op(e4,e4)) = e4). end_of_list. ============================== end of input ========================== % clear(auto_denials), because it is incompatiable with FOF reduction. Attempting problem reduction; original problem has = <976,1178063360>. Problem reduction (0.06 sec) gives 50 independent subproblems: ( <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> <48,36> ). Max nnf_size of subproblems is 48; max cnf_max is 36. ============================== FOF REDUCTION MULTISEARCH ============= Subproblem 1 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e0,e0),e0),e0)). Max_seconds is 30 for this subproblem. Child search process 21755 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e0,e0),e0) != e0. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 5. % Given clauses 0. 11 op(e0,e0) = e0. [assumption]. 36 op(op(e0,e0),e0) != e0. [assumption]. 37 $F. [copy(36),rewrite([11(3),11(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21755 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 2 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e0,e1),e1),e0)). Max_seconds is 30 for this subproblem. Child search process 21756 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e0,e1),e1) != e0. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) 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. 12 op(e0,e1) = e3. [assumption]. 27 op(e3,e1) = e0. [assumption]. 36 op(op(e0,e1),e1) != e0. [assumption]. 37 $F. [copy(36),rewrite([12(3),27(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21756 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 3 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e0,e2),e2),e0)). Max_seconds is 30 for this subproblem. Child search process 21757 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e0,e2),e2) != e0. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) 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. 13 op(e0,e2) = e4. [assumption]. 33 op(e4,e2) = e0. [assumption]. 36 op(op(e0,e2),e2) != e0. [assumption]. 37 $F. [copy(36),rewrite([13(3),33(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21757 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 4 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e0,e3),e3),e0)). Max_seconds is 30 for this subproblem. Child search process 21758 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e0,e3),e3) != e0. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) 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. 14 op(e0,e3) = e2. [assumption]. 24 op(e2,e3) = e0. [assumption]. 36 op(op(e0,e3),e3) != e0. [assumption]. 37 $F. [copy(36),rewrite([14(3),24(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21758 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 5 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e0,e4),e4),e0)). Max_seconds is 30 for this subproblem. Child search process 21759 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e0,e4),e4) != e0. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) 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(e0,e4) = e1. [assumption]. 20 op(e1,e4) = e0. [assumption]. 36 op(op(e0,e4),e4) != e0. [assumption]. 37 $F. [copy(36),rewrite([15(3),20(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21759 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 6 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e1,e0),e0),e1)). Max_seconds is 30 for this subproblem. Child search process 21760 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e1,e0),e0) != e1. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) 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. 16 op(e1,e0) = e2. [assumption]. 21 op(e2,e0) = e1. [assumption]. 36 op(op(e1,e0),e0) != e1. [assumption]. 37 $F. [copy(36),rewrite([16(3),21(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21760 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 7 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e1,e1),e1),e1)). Max_seconds is 30 for this subproblem. Child search process 21761 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e1,e1),e1) != e1. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 5. % Given clauses 0. 17 op(e1,e1) = e1. [assumption]. 36 op(op(e1,e1),e1) != e1. [assumption]. 37 $F. [copy(36),rewrite([17(3),17(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21761 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 8 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e1,e2),e2),e1)). Max_seconds is 30 for this subproblem. Child search process 21762 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e1,e2),e2) != e1. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) 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. 18 op(e1,e2) = e3. [assumption]. 28 op(e3,e2) = e1. [assumption]. 36 op(op(e1,e2),e2) != e1. [assumption]. 37 $F. [copy(36),rewrite([18(3),28(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21762 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 9 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e1,e3),e3),e1)). Max_seconds is 30 for this subproblem. Child search process 21763 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e1,e3),e3) != e1. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) 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(e1,e3) = e4. [assumption]. 34 op(e4,e3) = e1. [assumption]. 36 op(op(e1,e3),e3) != e1. [assumption]. 37 $F. [copy(36),rewrite([19(3),34(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21763 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 10 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e1,e4),e4),e1)). Max_seconds is 30 for this subproblem. Child search process 21764 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e1,e4),e4) != e1. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) 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(e0,e4) = e1. [assumption]. 20 op(e1,e4) = e0. [assumption]. 36 op(op(e1,e4),e4) != e1. [assumption]. 37 $F. [copy(36),rewrite([20(3),15(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21764 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 11 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e2,e0),e0),e2)). Max_seconds is 30 for this subproblem. Child search process 21765 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e2,e0),e0) != e2. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) 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. 16 op(e1,e0) = e2. [assumption]. 21 op(e2,e0) = e1. [assumption]. 36 op(op(e2,e0),e0) != e2. [assumption]. 37 $F. [copy(36),rewrite([21(3),16(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21765 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 12 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e2,e1),e1),e2)). Max_seconds is 30 for this subproblem. Child search process 21766 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e2,e1),e1) != e2. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) 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. 22 op(e2,e1) = e4. [assumption]. 32 op(e4,e1) = e2. [assumption]. 36 op(op(e2,e1),e1) != e2. [assumption]. 37 $F. [copy(36),rewrite([22(3),32(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21766 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 13 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e2,e2),e2),e2)). Max_seconds is 30 for this subproblem. Child search process 21767 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e2,e2),e2) != e2. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 5. % Given clauses 0. 23 op(e2,e2) = e2. [assumption]. 36 op(op(e2,e2),e2) != e2. [assumption]. 37 $F. [copy(36),rewrite([23(3),23(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21767 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 14 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e2,e3),e3),e2)). Max_seconds is 30 for this subproblem. Child search process 21768 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e2,e3),e3) != e2. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) 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. 14 op(e0,e3) = e2. [assumption]. 24 op(e2,e3) = e0. [assumption]. 36 op(op(e2,e3),e3) != e2. [assumption]. 37 $F. [copy(36),rewrite([24(3),14(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21768 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 15 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e2,e4),e4),e2)). Max_seconds is 30 for this subproblem. Child search process 21769 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e2,e4),e4) != e2. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) 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. 25 op(e2,e4) = e3. [assumption]. 30 op(e3,e4) = e2. [assumption]. 36 op(op(e2,e4),e4) != e2. [assumption]. 37 $F. [copy(36),rewrite([25(3),30(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21769 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 16 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e3,e0),e0),e3)). Max_seconds is 30 for this subproblem. Child search process 21770 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e3,e0),e0) != e3. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) 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. 26 op(e3,e0) = e4. [assumption]. 31 op(e4,e0) = e3. [assumption]. 36 op(op(e3,e0),e0) != e3. [assumption]. 37 $F. [copy(36),rewrite([26(3),31(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21770 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 17 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e3,e1),e1),e3)). Max_seconds is 30 for this subproblem. Child search process 21771 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e3,e1),e1) != e3. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) 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. 12 op(e0,e1) = e3. [assumption]. 27 op(e3,e1) = e0. [assumption]. 36 op(op(e3,e1),e1) != e3. [assumption]. 37 $F. [copy(36),rewrite([27(3),12(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21771 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 18 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e3,e2),e2),e3)). Max_seconds is 30 for this subproblem. Child search process 21772 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e3,e2),e2) != e3. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) 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. 18 op(e1,e2) = e3. [assumption]. 28 op(e3,e2) = e1. [assumption]. 36 op(op(e3,e2),e2) != e3. [assumption]. 37 $F. [copy(36),rewrite([28(3),18(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21772 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 19 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e3,e3),e3),e3)). Max_seconds is 30 for this subproblem. Child search process 21773 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e3,e3),e3) != e3. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 5. % Given clauses 0. 29 op(e3,e3) = e3. [assumption]. 36 op(op(e3,e3),e3) != e3. [assumption]. 37 $F. [copy(36),rewrite([29(3),29(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21773 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 20 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e3,e4),e4),e3)). Max_seconds is 30 for this subproblem. Child search process 21774 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e3,e4),e4) != e3. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) 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. 25 op(e2,e4) = e3. [assumption]. 30 op(e3,e4) = e2. [assumption]. 36 op(op(e3,e4),e4) != e3. [assumption]. 37 $F. [copy(36),rewrite([30(3),25(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21774 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 21 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e4,e0),e0),e4)). Max_seconds is 30 for this subproblem. Child search process 21775 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e4,e0),e0) != e4. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) 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. 26 op(e3,e0) = e4. [assumption]. 31 op(e4,e0) = e3. [assumption]. 36 op(op(e4,e0),e0) != e4. [assumption]. 37 $F. [copy(36),rewrite([31(3),26(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21775 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 22 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e4,e1),e1),e4)). Max_seconds is 30 for this subproblem. Child search process 21776 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e4,e1),e1) != e4. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) 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. 22 op(e2,e1) = e4. [assumption]. 32 op(e4,e1) = e2. [assumption]. 36 op(op(e4,e1),e1) != e4. [assumption]. 37 $F. [copy(36),rewrite([32(3),22(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21776 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 23 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e4,e2),e2),e4)). Max_seconds is 30 for this subproblem. Child search process 21777 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e4,e2),e2) != e4. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) 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. 13 op(e0,e2) = e4. [assumption]. 33 op(e4,e2) = e0. [assumption]. 36 op(op(e4,e2),e2) != e4. [assumption]. 37 $F. [copy(36),rewrite([33(3),13(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21777 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 24 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e4,e3),e3),e4)). Max_seconds is 30 for this subproblem. Child search process 21778 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e4,e3),e3) != e4. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) 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(e1,e3) = e4. [assumption]. 34 op(e4,e3) = e1. [assumption]. 36 op(op(e4,e3),e3) != e4. [assumption]. 37 $F. [copy(36),rewrite([34(3),19(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21778 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 25 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e4,e4),e4),e4)). Max_seconds is 30 for this subproblem. Child search process 21779 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e4,e4),e4) != e4. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 5. % Given clauses 0. 35 op(e4,e4) = e4. [assumption]. 36 op(op(e4,e4),e4) != e4. [assumption]. 37 $F. [copy(36),rewrite([35(3),35(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=249. 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.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21779 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 26 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e0,e0),op(e0,e0)),e0)). Max_seconds is 30 for this subproblem. Child search process 21780 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e0,e0),op(e0,e0)) != e0. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 3. % Level of proof is 1. % Maximum clause weight is 5. % Given clauses 0. 11 op(e0,e0) = e0. [assumption]. 36 op(op(e0,e0),op(e0,e0)) != e0. [assumption]. 37 $F. [copy(36),rewrite([11(3),11(4),11(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=252. Demod_rewrites=3. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21780 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 27 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e1,e0),op(e0,e1)),e0)). Max_seconds is 30 for this subproblem. Child search process 21781 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e1,e0),op(e0,e1)) != e0. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 5. % Level of proof is 1. % Maximum clause weight is 5. % Given clauses 0. 12 op(e0,e1) = e3. [assumption]. 16 op(e1,e0) = e2. [assumption]. 24 op(e2,e3) = e0. [assumption]. 36 op(op(e1,e0),op(e0,e1)) != e0. [assumption]. 37 $F. [copy(36),rewrite([16(3),12(4),24(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=252. Demod_rewrites=3. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21781 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 28 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e2,e0),op(e0,e2)),e0)). Max_seconds is 30 for this subproblem. Child search process 21782 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e2,e0),op(e0,e2)) != e0. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 5. % Level of proof is 1. % Maximum clause weight is 5. % Given clauses 0. 13 op(e0,e2) = e4. [assumption]. 20 op(e1,e4) = e0. [assumption]. 21 op(e2,e0) = e1. [assumption]. 36 op(op(e2,e0),op(e0,e2)) != e0. [assumption]. 37 $F. [copy(36),rewrite([21(3),13(4),20(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=252. Demod_rewrites=3. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21782 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 29 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e3,e0),op(e0,e3)),e0)). Max_seconds is 30 for this subproblem. Child search process 21783 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e3,e0),op(e0,e3)) != e0. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 5. % Level of proof is 1. % Maximum clause weight is 5. % Given clauses 0. 14 op(e0,e3) = e2. [assumption]. 26 op(e3,e0) = e4. [assumption]. 33 op(e4,e2) = e0. [assumption]. 36 op(op(e3,e0),op(e0,e3)) != e0. [assumption]. 37 $F. [copy(36),rewrite([26(3),14(4),33(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=252. Demod_rewrites=3. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21783 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 30 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e4,e0),op(e0,e4)),e0)). Max_seconds is 30 for this subproblem. Child search process 21784 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e4,e0),op(e0,e4)) != e0. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 5. % Level of proof is 1. % Maximum clause weight is 5. % Given clauses 0. 15 op(e0,e4) = e1. [assumption]. 27 op(e3,e1) = e0. [assumption]. 31 op(e4,e0) = e3. [assumption]. 36 op(op(e4,e0),op(e0,e4)) != e0. [assumption]. 37 $F. [copy(36),rewrite([31(3),15(4),27(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=252. Demod_rewrites=3. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21784 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 31 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e0,e1),op(e1,e0)),e1)). Max_seconds is 30 for this subproblem. Child search process 21785 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e0,e1),op(e1,e0)) != e1. [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([ = ]). Function symbol precedence: function_order([ e0, e1, e2, e3, e4, op ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 5. % Level of proof is 1. % Maximum clause weight is 5. % Given clauses 0. 12 op(e0,e1) = e3. [assumption]. 16 op(e1,e0) = e2. [assumption]. 28 op(e3,e2) = e1. [assumption]. 36 op(op(e0,e1),op(e1,e0)) != e1. [assumption]. 37 $F. [copy(36),rewrite([12(3),16(4),28(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=36. Kept=35. proofs=1. Usable=0. Sos=0. Demods=25. Limbo=35, Disabled=36. 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=25 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=252. Demod_rewrites=3. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.84. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21785 exit (max_proofs) Wed May 7 22:14:44 2008 ============================== continuing FOF reduction multisearch == Subproblem 32 of 50 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e3,e2) & - =(e4,e2) & - =(e4,e3) & =(op(e0,e0),e0) & =(op(e0,e1),e3) & =(op(e0,e2),e4) & =(op(e0,e3),e2) & =(op(e0,e4),e1) & =(op(e1,e0),e2) & =(op(e1,e1),e1) & =(op(e1,e2),e3) & =(op(e1,e3),e4) & =(op(e1,e4),e0) & =(op(e2,e0),e1) & =(op(e2,e1),e4) & =(op(e2,e2),e2) & =(op(e2,e3),e0) & =(op(e2,e4),e3) & =(op(e3,e0),e4) & =(op(e3,e1),e0) & =(op(e3,e2),e1) & =(op(e3,e3),e3) & =(op(e3,e4),e2) & =(op(e4,e0),e3) & =(op(e4,e1),e2) & =(op(e4,e2),e0) & =(op(e4,e3),e1) & =(op(e4,e4),e4) & - =(op(op(e1,e1),op(e1,e1)),e1)). Max_seconds is 30 for this subproblem. Child search process 21786 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). e1 != e0. [assumption]. e2 != e0. [assumption]. e3 != e0. [assumption]. e4 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e4 != e3. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e3. [assumption]. op(e0,e2) = e4. [assumption]. op(e0,e3) = e2. [assumption]. op(e0,e4) = e1. [assumption]. op(e1,e0) = e2. [assumption]. op(e1,e1) = e1. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e4. [assumption]. op(e1,e4) = e0. [assumption]. op(e2,e0) = e1. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e2. [assumption]. op(e2,e3) = e0. [assumption]. op(e2,e4) = e3. [assumption]. op(e3,e0) = e4. [assumption]. op(e3,e1) = e0. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e3. [assumption]. op(e3,e4) = e2. [assumption]. op(e4,e0) = e3. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e0. [assumption]. op(e4,e3) = e1. [assumption]. op(e4,e4) = e4. [assumption]. op(op(e1,e1),op(e1,e1)) != e1. [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINAT