============================== FOF-Prover9 =========================== FOF-Prover9 (32) version 2008-05A, May 2008. Process 21503 was started by mccune on cleo, Wed May 7 22:14:41 2008 The command was "/home/mccune/LADR/bin/fof-prover9 -f ALG033+1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file ALG033+1.in assign(max_seconds,120). set(prolog_style_variables). formulas(assumptions). e0 != e1 & e0 != e2 & e0 != e3 & e0 != e4 & e0 != e5 & e1 != e2 & e1 != e3 & e1 != e4 & e1 != e5 & e2 != e3 & e2 != e4 & e2 != e5 & e3 != e4 & e3 != e5 & e4 != e5. op(e0,e0) = e0 & op(e0,e1) = e1 & op(e0,e2) = e2 & op(e0,e3) = e3 & op(e0,e4) = e4 & op(e0,e5) = e5 & op(e1,e0) = e1 & op(e1,e1) = e0 & op(e1,e2) = e3 & op(e1,e3) = e2 & op(e1,e4) = e5 & op(e1,e5) = e4 & op(e2,e0) = e2 & op(e2,e1) = e4 & op(e2,e2) = e0 & op(e2,e3) = e5 & op(e2,e4) = e1 & op(e2,e5) = e3 & op(e3,e0) = e3 & op(e3,e1) = e5 & op(e3,e2) = e1 & op(e3,e3) = e4 & op(e3,e4) = e0 & op(e3,e5) = e2 & op(e4,e0) = e4 & op(e4,e1) = e2 & op(e4,e2) = e5 & op(e4,e3) = e0 & op(e4,e4) = e3 & op(e4,e5) = e1 & op(e5,e0) = e5 & op(e5,e1) = e3 & op(e5,e2) = e4 & op(e5,e3) = e1 & op(e5,e4) = e2 & op(e5,e5) = e0. unit = e0. inv(e0) = e0 & inv(e1) = e1 & inv(e2) = e2 & inv(e3) = e4 & inv(e4) = e3 & inv(e5) = e5. -(-(op(e0,e0) = op(e0,e0) & op(e0,e1) = op(e1,e0) & op(e0,e2) = op(e2,e0) & op(e0,e3) = op(e3,e0) & op(e0,e4) = op(e4,e0) & op(e0,e5) = op(e5,e0) & op(e1,e0) = op(e0,e1) & op(e1,e1) = op(e1,e1) & op(e1,e2) = op(e2,e1) & op(e1,e3) = op(e3,e1) & op(e1,e4) = op(e4,e1) & op(e1,e5) = op(e5,e1) & op(e2,e0) = op(e0,e2) & op(e2,e1) = op(e1,e2) & op(e2,e2) = op(e2,e2) & op(e2,e3) = op(e3,e2) & op(e2,e4) = op(e4,e2) & op(e2,e5) = op(e5,e2) & op(e3,e0) = op(e0,e3) & op(e3,e1) = op(e1,e3) & op(e3,e2) = op(e2,e3) & op(e3,e3) = op(e3,e3) & op(e3,e4) = op(e4,e3) & op(e3,e5) = op(e5,e3) & op(e4,e0) = op(e0,e4) & op(e4,e1) = op(e1,e4) & op(e4,e2) = op(e2,e4) & op(e4,e3) = op(e3,e4) & op(e4,e4) = op(e4,e4) & op(e4,e5) = op(e5,e4) & op(e5,e0) = op(e0,e5) & op(e5,e1) = op(e1,e5) & op(e5,e2) = op(e2,e5) & op(e5,e3) = op(e3,e5) & op(e5,e4) = op(e4,e5) & op(e5,e5) = op(e5,e5)) & (op(e0,e0) = e0 | op(e0,e0) = e1 | op(e0,e0) = e2 | op(e0,e0) = e3 | op(e0,e0) = e4 | op(e0,e0) = e5) & (op(e0,e1) = e0 | op(e0,e1) = e1 | op(e0,e1) = e2 | op(e0,e1) = e3 | op(e0,e1) = e4 | op(e0,e1) = e5) & (op(e0,e2) = e0 | op(e0,e2) = e1 | op(e0,e2) = e2 | op(e0,e2) = e3 | op(e0,e2) = e4 | op(e0,e2) = e5) & (op(e0,e3) = e0 | op(e0,e3) = e1 | op(e0,e3) = e2 | op(e0,e3) = e3 | op(e0,e3) = e4 | op(e0,e3) = e5) & (op(e0,e4) = e0 | op(e0,e4) = e1 | op(e0,e4) = e2 | op(e0,e4) = e3 | op(e0,e4) = e4 | op(e0,e4) = e5) & (op(e0,e5) = e0 | op(e0,e5) = e1 | op(e0,e5) = e2 | op(e0,e5) = e3 | op(e0,e5) = e4 | op(e0,e5) = e5) & (op(e1,e0) = e0 | op(e1,e0) = e1 | op(e1,e0) = e2 | op(e1,e0) = e3 | op(e1,e0) = e4 | op(e1,e0) = e5) & (op(e1,e1) = e0 | op(e1,e1) = e1 | op(e1,e1) = e2 | op(e1,e1) = e3 | op(e1,e1) = e4 | op(e1,e1) = e5) & (op(e1,e2) = e0 | op(e1,e2) = e1 | op(e1,e2) = e2 | op(e1,e2) = e3 | op(e1,e2) = e4 | op(e1,e2) = e5) & (op(e1,e3) = e0 | op(e1,e3) = e1 | op(e1,e3) = e2 | op(e1,e3) = e3 | op(e1,e3) = e4 | op(e1,e3) = e5) & (op(e1,e4) = e0 | op(e1,e4) = e1 | op(e1,e4) = e2 | op(e1,e4) = e3 | op(e1,e4) = e4 | op(e1,e4) = e5) & (op(e1,e5) = e0 | op(e1,e5) = e1 | op(e1,e5) = e2 | op(e1,e5) = e3 | op(e1,e5) = e4 | op(e1,e5) = e5) & (op(e2,e0) = e0 | op(e2,e0) = e1 | op(e2,e0) = e2 | op(e2,e0) = e3 | op(e2,e0) = e4 | op(e2,e0) = e5) & (op(e2,e1) = e0 | op(e2,e1) = e1 | op(e2,e1) = e2 | op(e2,e1) = e3 | op(e2,e1) = e4 | op(e2,e1) = e5) & (op(e2,e2) = e0 | op(e2,e2) = e1 | op(e2,e2) = e2 | op(e2,e2) = e3 | op(e2,e2) = e4 | op(e2,e2) = e5) & (op(e2,e3) = e0 | op(e2,e3) = e1 | op(e2,e3) = e2 | op(e2,e3) = e3 | op(e2,e3) = e4 | op(e2,e3) = e5) & (op(e2,e4) = e0 | op(e2,e4) = e1 | op(e2,e4) = e2 | op(e2,e4) = e3 | op(e2,e4) = e4 | op(e2,e4) = e5) & (op(e2,e5) = e0 | op(e2,e5) = e1 | op(e2,e5) = e2 | op(e2,e5) = e3 | op(e2,e5) = e4 | op(e2,e5) = e5) & (op(e3,e0) = e0 | op(e3,e0) = e1 | op(e3,e0) = e2 | op(e3,e0) = e3 | op(e3,e0) = e4 | op(e3,e0) = e5) & (op(e3,e1) = e0 | op(e3,e1) = e1 | op(e3,e1) = e2 | op(e3,e1) = e3 | op(e3,e1) = e4 | op(e3,e1) = e5) & (op(e3,e2) = e0 | op(e3,e2) = e1 | op(e3,e2) = e2 | op(e3,e2) = e3 | op(e3,e2) = e4 | op(e3,e2) = e5) & (op(e3,e3) = e0 | op(e3,e3) = e1 | op(e3,e3) = e2 | op(e3,e3) = e3 | op(e3,e3) = e4 | op(e3,e3) = e5) & (op(e3,e4) = e0 | op(e3,e4) = e1 | op(e3,e4) = e2 | op(e3,e4) = e3 | op(e3,e4) = e4 | op(e3,e4) = e5) & (op(e3,e5) = e0 | op(e3,e5) = e1 | op(e3,e5) = e2 | op(e3,e5) = e3 | op(e3,e5) = e4 | op(e3,e5) = e5) & (op(e4,e0) = e0 | op(e4,e0) = e1 | op(e4,e0) = e2 | op(e4,e0) = e3 | op(e4,e0) = e4 | op(e4,e0) = e5) & (op(e4,e1) = e0 | op(e4,e1) = e1 | op(e4,e1) = e2 | op(e4,e1) = e3 | op(e4,e1) = e4 | op(e4,e1) = e5) & (op(e4,e2) = e0 | op(e4,e2) = e1 | op(e4,e2) = e2 | op(e4,e2) = e3 | op(e4,e2) = e4 | op(e4,e2) = e5) & (op(e4,e3) = e0 | op(e4,e3) = e1 | op(e4,e3) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 | op(e4,e3) = e5) & (op(e4,e4) = e0 | op(e4,e4) = e1 | op(e4,e4) = e2 | op(e4,e4) = e3 | op(e4,e4) = e4 | op(e4,e4) = e5) & (op(e4,e5) = e0 | op(e4,e5) = e1 | op(e4,e5) = e2 | op(e4,e5) = e3 | op(e4,e5) = e4 | op(e4,e5) = e5) & (op(e5,e0) = e0 | op(e5,e0) = e1 | op(e5,e0) = e2 | op(e5,e0) = e3 | op(e5,e0) = e4 | op(e5,e0) = e5) & (op(e5,e1) = e0 | op(e5,e1) = e1 | op(e5,e1) = e2 | op(e5,e1) = e3 | op(e5,e1) = e4 | op(e5,e1) = e5) & (op(e5,e2) = e0 | op(e5,e2) = e1 | op(e5,e2) = e2 | op(e5,e2) = e3 | op(e5,e2) = e4 | op(e5,e2) = e5) & (op(e5,e3) = e0 | op(e5,e3) = e1 | op(e5,e3) = e2 | op(e5,e3) = e3 | op(e5,e3) = e4 | op(e5,e3) = e5) & (op(e5,e4) = e0 | op(e5,e4) = e1 | op(e5,e4) = e2 | op(e5,e4) = e3 | op(e5,e4) = e4 | op(e5,e4) = e5) & (op(e5,e5) = e0 | op(e5,e5) = e1 | op(e5,e5) = e2 | op(e5,e5) = e3 | op(e5,e5) = e4 | op(e5,e5) = e5) & op(op(e0,e0),e0) = op(e0,op(e0,e0)) & op(op(e0,e0),e1) = op(e0,op(e0,e1)) & op(op(e0,e0),e2) = op(e0,op(e0,e2)) & op(op(e0,e0),e3) = op(e0,op(e0,e3)) & op(op(e0,e0),e4) = op(e0,op(e0,e4)) & op(op(e0,e0),e5) = op(e0,op(e0,e5)) & op(op(e0,e1),e0) = op(e0,op(e1,e0)) & op(op(e0,e1),e1) = op(e0,op(e1,e1)) & op(op(e0,e1),e2) = op(e0,op(e1,e2)) & op(op(e0,e1),e3) = op(e0,op(e1,e3)) & op(op(e0,e1),e4) = op(e0,op(e1,e4)) & op(op(e0,e1),e5) = op(e0,op(e1,e5)) & op(op(e0,e2),e0) = op(e0,op(e2,e0)) & op(op(e0,e2),e1) = op(e0,op(e2,e1)) & op(op(e0,e2),e2) = op(e0,op(e2,e2)) & op(op(e0,e2),e3) = op(e0,op(e2,e3)) & op(op(e0,e2),e4) = op(e0,op(e2,e4)) & op(op(e0,e2),e5) = op(e0,op(e2,e5)) & op(op(e0,e3),e0) = op(e0,op(e3,e0)) & op(op(e0,e3),e1) = op(e0,op(e3,e1)) & op(op(e0,e3),e2) = op(e0,op(e3,e2)) & op(op(e0,e3),e3) = op(e0,op(e3,e3)) & op(op(e0,e3),e4) = op(e0,op(e3,e4)) & op(op(e0,e3),e5) = op(e0,op(e3,e5)) & op(op(e0,e4),e0) = op(e0,op(e4,e0)) & op(op(e0,e4),e1) = op(e0,op(e4,e1)) & op(op(e0,e4),e2) = op(e0,op(e4,e2)) & op(op(e0,e4),e3) = op(e0,op(e4,e3)) & op(op(e0,e4),e4) = op(e0,op(e4,e4)) & op(op(e0,e4),e5) = op(e0,op(e4,e5)) & op(op(e0,e5),e0) = op(e0,op(e5,e0)) & op(op(e0,e5),e1) = op(e0,op(e5,e1)) & op(op(e0,e5),e2) = op(e0,op(e5,e2)) & op(op(e0,e5),e3) = op(e0,op(e5,e3)) & op(op(e0,e5),e4) = op(e0,op(e5,e4)) & op(op(e0,e5),e5) = op(e0,op(e5,e5)) & op(op(e1,e0),e0) = op(e1,op(e0,e0)) & op(op(e1,e0),e1) = op(e1,op(e0,e1)) & op(op(e1,e0),e2) = op(e1,op(e0,e2)) & op(op(e1,e0),e3) = op(e1,op(e0,e3)) & op(op(e1,e0),e4) = op(e1,op(e0,e4)) & op(op(e1,e0),e5) = op(e1,op(e0,e5)) & op(op(e1,e1),e0) = op(e1,op(e1,e0)) & op(op(e1,e1),e1) = op(e1,op(e1,e1)) & op(op(e1,e1),e2) = op(e1,op(e1,e2)) & op(op(e1,e1),e3) = op(e1,op(e1,e3)) & op(op(e1,e1),e4) = op(e1,op(e1,e4)) & op(op(e1,e1),e5) = op(e1,op(e1,e5)) & op(op(e1,e2),e0) = op(e1,op(e2,e0)) & op(op(e1,e2),e1) = op(e1,op(e2,e1)) & op(op(e1,e2),e2) = op(e1,op(e2,e2)) & op(op(e1,e2),e3) = op(e1,op(e2,e3)) & op(op(e1,e2),e4) = op(e1,op(e2,e4)) & op(op(e1,e2),e5) = op(e1,op(e2,e5)) & op(op(e1,e3),e0) = op(e1,op(e3,e0)) & op(op(e1,e3),e1) = op(e1,op(e3,e1)) & op(op(e1,e3),e2) = op(e1,op(e3,e2)) & op(op(e1,e3),e3) = op(e1,op(e3,e3)) & op(op(e1,e3),e4) = op(e1,op(e3,e4)) & op(op(e1,e3),e5) = op(e1,op(e3,e5)) & op(op(e1,e4),e0) = op(e1,op(e4,e0)) & op(op(e1,e4),e1) = op(e1,op(e4,e1)) & op(op(e1,e4),e2) = op(e1,op(e4,e2)) & op(op(e1,e4),e3) = op(e1,op(e4,e3)) & op(op(e1,e4),e4) = op(e1,op(e4,e4)) & op(op(e1,e4),e5) = op(e1,op(e4,e5)) & op(op(e1,e5),e0) = op(e1,op(e5,e0)) & op(op(e1,e5),e1) = op(e1,op(e5,e1)) & op(op(e1,e5),e2) = op(e1,op(e5,e2)) & op(op(e1,e5),e3) = op(e1,op(e5,e3)) & op(op(e1,e5),e4) = op(e1,op(e5,e4)) & op(op(e1,e5),e5) = op(e1,op(e5,e5)) & op(op(e2,e0),e0) = op(e2,op(e0,e0)) & op(op(e2,e0),e1) = op(e2,op(e0,e1)) & op(op(e2,e0),e2) = op(e2,op(e0,e2)) & op(op(e2,e0),e3) = op(e2,op(e0,e3)) & op(op(e2,e0),e4) = op(e2,op(e0,e4)) & op(op(e2,e0),e5) = op(e2,op(e0,e5)) & op(op(e2,e1),e0) = op(e2,op(e1,e0)) & op(op(e2,e1),e1) = op(e2,op(e1,e1)) & op(op(e2,e1),e2) = op(e2,op(e1,e2)) & op(op(e2,e1),e3) = op(e2,op(e1,e3)) & op(op(e2,e1),e4) = op(e2,op(e1,e4)) & op(op(e2,e1),e5) = op(e2,op(e1,e5)) & op(op(e2,e2),e0) = op(e2,op(e2,e0)) & op(op(e2,e2),e1) = op(e2,op(e2,e1)) & op(op(e2,e2),e2) = op(e2,op(e2,e2)) & op(op(e2,e2),e3) = op(e2,op(e2,e3)) & op(op(e2,e2),e4) = op(e2,op(e2,e4)) & op(op(e2,e2),e5) = op(e2,op(e2,e5)) & op(op(e2,e3),e0) = op(e2,op(e3,e0)) & op(op(e2,e3),e1) = op(e2,op(e3,e1)) & op(op(e2,e3),e2) = op(e2,op(e3,e2)) & op(op(e2,e3),e3) = op(e2,op(e3,e3)) & op(op(e2,e3),e4) = op(e2,op(e3,e4)) & op(op(e2,e3),e5) = op(e2,op(e3,e5)) & op(op(e2,e4),e0) = op(e2,op(e4,e0)) & op(op(e2,e4),e1) = op(e2,op(e4,e1)) & op(op(e2,e4),e2) = op(e2,op(e4,e2)) & op(op(e2,e4),e3) = op(e2,op(e4,e3)) & op(op(e2,e4),e4) = op(e2,op(e4,e4)) & op(op(e2,e4),e5) = op(e2,op(e4,e5)) & op(op(e2,e5),e0) = op(e2,op(e5,e0)) & op(op(e2,e5),e1) = op(e2,op(e5,e1)) & op(op(e2,e5),e2) = op(e2,op(e5,e2)) & op(op(e2,e5),e3) = op(e2,op(e5,e3)) & op(op(e2,e5),e4) = op(e2,op(e5,e4)) & op(op(e2,e5),e5) = op(e2,op(e5,e5)) & op(op(e3,e0),e0) = op(e3,op(e0,e0)) & op(op(e3,e0),e1) = op(e3,op(e0,e1)) & op(op(e3,e0),e2) = op(e3,op(e0,e2)) & op(op(e3,e0),e3) = op(e3,op(e0,e3)) & op(op(e3,e0),e4) = op(e3,op(e0,e4)) & op(op(e3,e0),e5) = op(e3,op(e0,e5)) & op(op(e3,e1),e0) = op(e3,op(e1,e0)) & op(op(e3,e1),e1) = op(e3,op(e1,e1)) & op(op(e3,e1),e2) = op(e3,op(e1,e2)) & op(op(e3,e1),e3) = op(e3,op(e1,e3)) & op(op(e3,e1),e4) = op(e3,op(e1,e4)) & op(op(e3,e1),e5) = op(e3,op(e1,e5)) & op(op(e3,e2),e0) = op(e3,op(e2,e0)) & op(op(e3,e2),e1) = op(e3,op(e2,e1)) & op(op(e3,e2),e2) = op(e3,op(e2,e2)) & op(op(e3,e2),e3) = op(e3,op(e2,e3)) & op(op(e3,e2),e4) = op(e3,op(e2,e4)) & op(op(e3,e2),e5) = op(e3,op(e2,e5)) & op(op(e3,e3),e0) = op(e3,op(e3,e0)) & op(op(e3,e3),e1) = op(e3,op(e3,e1)) & op(op(e3,e3),e2) = op(e3,op(e3,e2)) & op(op(e3,e3),e3) = op(e3,op(e3,e3)) & op(op(e3,e3),e4) = op(e3,op(e3,e4)) & op(op(e3,e3),e5) = op(e3,op(e3,e5)) & op(op(e3,e4),e0) = op(e3,op(e4,e0)) & op(op(e3,e4),e1) = op(e3,op(e4,e1)) & op(op(e3,e4),e2) = op(e3,op(e4,e2)) & op(op(e3,e4),e3) = op(e3,op(e4,e3)) & op(op(e3,e4),e4) = op(e3,op(e4,e4)) & op(op(e3,e4),e5) = op(e3,op(e4,e5)) & op(op(e3,e5),e0) = op(e3,op(e5,e0)) & op(op(e3,e5),e1) = op(e3,op(e5,e1)) & op(op(e3,e5),e2) = op(e3,op(e5,e2)) & op(op(e3,e5),e3) = op(e3,op(e5,e3)) & op(op(e3,e5),e4) = op(e3,op(e5,e4)) & op(op(e3,e5),e5) = op(e3,op(e5,e5)) & op(op(e4,e0),e0) = op(e4,op(e0,e0)) & op(op(e4,e0),e1) = op(e4,op(e0,e1)) & op(op(e4,e0),e2) = op(e4,op(e0,e2)) & op(op(e4,e0),e3) = op(e4,op(e0,e3)) & op(op(e4,e0),e4) = op(e4,op(e0,e4)) & op(op(e4,e0),e5) = op(e4,op(e0,e5)) & op(op(e4,e1),e0) = op(e4,op(e1,e0)) & op(op(e4,e1),e1) = op(e4,op(e1,e1)) & op(op(e4,e1),e2) = op(e4,op(e1,e2)) & op(op(e4,e1),e3) = op(e4,op(e1,e3)) & op(op(e4,e1),e4) = op(e4,op(e1,e4)) & op(op(e4,e1),e5) = op(e4,op(e1,e5)) & op(op(e4,e2),e0) = op(e4,op(e2,e0)) & op(op(e4,e2),e1) = op(e4,op(e2,e1)) & op(op(e4,e2),e2) = op(e4,op(e2,e2)) & op(op(e4,e2),e3) = op(e4,op(e2,e3)) & op(op(e4,e2),e4) = op(e4,op(e2,e4)) & op(op(e4,e2),e5) = op(e4,op(e2,e5)) & op(op(e4,e3),e0) = op(e4,op(e3,e0)) & op(op(e4,e3),e1) = op(e4,op(e3,e1)) & op(op(e4,e3),e2) = op(e4,op(e3,e2)) & op(op(e4,e3),e3) = op(e4,op(e3,e3)) & op(op(e4,e3),e4) = op(e4,op(e3,e4)) & op(op(e4,e3),e5) = op(e4,op(e3,e5)) & op(op(e4,e4),e0) = op(e4,op(e4,e0)) & op(op(e4,e4),e1) = op(e4,op(e4,e1)) & op(op(e4,e4),e2) = op(e4,op(e4,e2)) & op(op(e4,e4),e3) = op(e4,op(e4,e3)) & op(op(e4,e4),e4) = op(e4,op(e4,e4)) & op(op(e4,e4),e5) = op(e4,op(e4,e5)) & op(op(e4,e5),e0) = op(e4,op(e5,e0)) & op(op(e4,e5),e1) = op(e4,op(e5,e1)) & op(op(e4,e5),e2) = op(e4,op(e5,e2)) & op(op(e4,e5),e3) = op(e4,op(e5,e3)) & op(op(e4,e5),e4) = op(e4,op(e5,e4)) & op(op(e4,e5),e5) = op(e4,op(e5,e5)) & op(op(e5,e0),e0) = op(e5,op(e0,e0)) & op(op(e5,e0),e1) = op(e5,op(e0,e1)) & op(op(e5,e0),e2) = op(e5,op(e0,e2)) & op(op(e5,e0),e3) = op(e5,op(e0,e3)) & op(op(e5,e0),e4) = op(e5,op(e0,e4)) & op(op(e5,e0),e5) = op(e5,op(e0,e5)) & op(op(e5,e1),e0) = op(e5,op(e1,e0)) & op(op(e5,e1),e1) = op(e5,op(e1,e1)) & op(op(e5,e1),e2) = op(e5,op(e1,e2)) & op(op(e5,e1),e3) = op(e5,op(e1,e3)) & op(op(e5,e1),e4) = op(e5,op(e1,e4)) & op(op(e5,e1),e5) = op(e5,op(e1,e5)) & op(op(e5,e2),e0) = op(e5,op(e2,e0)) & op(op(e5,e2),e1) = op(e5,op(e2,e1)) & op(op(e5,e2),e2) = op(e5,op(e2,e2)) & op(op(e5,e2),e3) = op(e5,op(e2,e3)) & op(op(e5,e2),e4) = op(e5,op(e2,e4)) & op(op(e5,e2),e5) = op(e5,op(e2,e5)) & op(op(e5,e3),e0) = op(e5,op(e3,e0)) & op(op(e5,e3),e1) = op(e5,op(e3,e1)) & op(op(e5,e3),e2) = op(e5,op(e3,e2)) & op(op(e5,e3),e3) = op(e5,op(e3,e3)) & op(op(e5,e3),e4) = op(e5,op(e3,e4)) & op(op(e5,e3),e5) = op(e5,op(e3,e5)) & op(op(e5,e4),e0) = op(e5,op(e4,e0)) & op(op(e5,e4),e1) = op(e5,op(e4,e1)) & op(op(e5,e4),e2) = op(e5,op(e4,e2)) & op(op(e5,e4),e3) = op(e5,op(e4,e3)) & op(op(e5,e4),e4) = op(e5,op(e4,e4)) & op(op(e5,e4),e5) = op(e5,op(e4,e5)) & op(op(e5,e5),e0) = op(e5,op(e5,e0)) & op(op(e5,e5),e1) = op(e5,op(e5,e1)) & op(op(e5,e5),e2) = op(e5,op(e5,e2)) & op(op(e5,e5),e3) = op(e5,op(e5,e3)) & op(op(e5,e5),e4) = op(e5,op(e5,e4)) & op(op(e5,e5),e5) = op(e5,op(e5,e5)) & op(unit,e0) = e0 & op(e0,unit) = e0 & op(unit,e1) = e1 & op(e1,unit) = e1 & op(unit,e2) = e2 & op(e2,unit) = e2 & op(unit,e3) = e3 & op(e3,unit) = e3 & op(unit,e4) = e4 & op(e4,unit) = e4 & op(unit,e5) = e5 & op(e5,unit) = e5 & (unit = e0 | unit = e1 | unit = e2 | unit = e3 | unit = e4 | unit = e5) & op(e0,inv(e0)) = unit & op(inv(e0),e0) = unit & op(e1,inv(e1)) = unit & op(inv(e1),e1) = unit & op(e2,inv(e2)) = unit & op(inv(e2),e2) = unit & op(e3,inv(e3)) = unit & op(inv(e3),e3) = unit & op(e4,inv(e4)) = unit & op(inv(e4),e4) = unit & op(e5,inv(e5)) = unit & op(inv(e5),e5) = unit & (inv(e0) = e0 | inv(e0) = e1 | inv(e0) = e2 | inv(e0) = e3 | inv(e0) = e4 | inv(e0) = e5) & (inv(e1) = e0 | inv(e1) = e1 | inv(e1) = e2 | inv(e1) = e3 | inv(e1) = e4 | inv(e1) = e5) & (inv(e2) = e0 | inv(e2) = e1 | inv(e2) = e2 | inv(e2) = e3 | inv(e2) = e4 | inv(e2) = e5) & (inv(e3) = e0 | inv(e3) = e1 | inv(e3) = e2 | inv(e3) = e3 | inv(e3) = e4 | inv(e3) = e5) & (inv(e4) = e0 | inv(e4) = e1 | inv(e4) = e2 | inv(e4) = e3 | inv(e4) = e4 | inv(e4) = e5) & (inv(e5) = e0 | inv(e5) = e1 | inv(e5) = e2 | inv(e5) = e3 | inv(e5) = e4 | inv(e5) = e5)). end_of_list. ============================== end of input ========================== % clear(auto_denials), because it is incompatiable with FOF reduction. Attempting problem reduction; original problem has = <1156,58>. Problem reduction (1.60 sec) gives 241 independent subproblems: ( <95,79> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> <76,59> ). Max nnf_size of subproblems is 95; max cnf_max is 79. ============================== FOF REDUCTION MULTISEARCH ============= Subproblem 1 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & =(op(e0,e0),op(e0,e0)) & =(op(e1,e0),op(e0,e1)) & =(op(e2,e0),op(e0,e2)) & =(op(e3,e0),op(e0,e3)) & =(op(e4,e0),op(e0,e4)) & =(op(e5,e0),op(e0,e5)) & =(op(e1,e1),op(e1,e1)) & =(op(e2,e1),op(e1,e2)) & =(op(e3,e1),op(e1,e3)) & =(op(e4,e1),op(e1,e4)) & =(op(e5,e1),op(e1,e5)) & =(op(e2,e2),op(e2,e2)) & =(op(e3,e2),op(e2,e3)) & =(op(e4,e2),op(e2,e4)) & =(op(e5,e2),op(e2,e5)) & =(op(e3,e3),op(e3,e3)) & =(op(e4,e3),op(e3,e4)) & =(op(e5,e3),op(e3,e5)) & =(op(e4,e4),op(e4,e4)) & =(op(e5,e4),op(e4,e5)) & =(op(e5,e5),op(e5,e5))). Max_seconds is 119 for this subproblem. Child search process 21504 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(e0,e0) = op(e0,e0). [assumption]. op(e1,e0) = op(e0,e1). [assumption]. op(e2,e0) = op(e0,e2). [assumption]. op(e3,e0) = op(e0,e3). [assumption]. op(e4,e0) = op(e0,e4). [assumption]. op(e5,e0) = op(e0,e5). [assumption]. op(e1,e1) = op(e1,e1). [assumption]. op(e2,e1) = op(e1,e2). [assumption]. op(e3,e1) = op(e1,e3). [assumption]. op(e4,e1) = op(e1,e4). [assumption]. op(e5,e1) = op(e1,e5). [assumption]. op(e2,e2) = op(e2,e2). [assumption]. op(e3,e2) = op(e2,e3). [assumption]. op(e4,e2) = op(e2,e4). [assumption]. op(e5,e2) = op(e2,e5). [assumption]. op(e3,e3) = op(e3,e3). [assumption]. op(e4,e3) = op(e3,e4). [assumption]. op(e5,e3) = op(e3,e5). [assumption]. op(e4,e4) = op(e4,e4). [assumption]. op(e5,e4) = op(e4,e5). [assumption]. op(e5,e5) = op(e5,e5). [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, e5, unit, op, inv ]). 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 6. % Level of proof is 2. % Maximum clause weight is 5. % Given clauses 0. 13 e4 != e3. [assumption]. 24 op(e1,e2) = e3. [assumption]. 29 op(e2,e1) = e4. [assumption]. 66 op(e2,e1) = op(e1,e2). [assumption]. 67 e4 = e3. [copy(66),rewrite([29(3),24(4)])]. 68 $F. [resolve(67,a,13,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=66. Kept=59. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=66. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=7. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=486. Demod_rewrites=16. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21504 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 2 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e0),e0),op(e0,op(e0,e0)))). Max_seconds is 119 for this subproblem. Child search process 21505 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(op(e0,e0),e0) != op(e0,op(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, e5, unit, op, inv ]). 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. 16 op(e0,e0) = e0. [assumption]. 59 op(op(e0,e0),e0) != op(e0,op(e0,e0)). [assumption]. 60 $F. [copy(59),rewrite([16(3),16(3),16(5),16(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=59. Kept=58. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=59. 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=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=419. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21505 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 3 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e0),e1),op(e0,op(e0,e1)))). Max_seconds is 119 for this subproblem. Child search process 21506 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(op(e0,e0),e1) != op(e0,op(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, e5, unit, op, inv ]). 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(e0,e0) = e0. [assumption]. 17 op(e0,e1) = e1. [assumption]. 59 op(op(e0,e0),e1) != op(e0,op(e0,e1)). [assumption]. 60 $F. [copy(59),rewrite([16(3),17(3),17(5),17(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=59. Kept=58. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=59. 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=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=419. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21506 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 4 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e0),e2),op(e0,op(e0,e2)))). Max_seconds is 119 for this subproblem. Child search process 21507 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(op(e0,e0),e2) != op(e0,op(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, e5, unit, op, inv ]). 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(e0,e0) = e0. [assumption]. 18 op(e0,e2) = e2. [assumption]. 59 op(op(e0,e0),e2) != op(e0,op(e0,e2)). [assumption]. 60 $F. [copy(59),rewrite([16(3),18(3),18(5),18(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=59. Kept=58. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=59. 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=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=419. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21507 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 5 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e0),e3),op(e0,op(e0,e3)))). Max_seconds is 119 for this subproblem. Child search process 21508 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(op(e0,e0),e3) != op(e0,op(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, e5, unit, op, inv ]). 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(e0,e0) = e0. [assumption]. 19 op(e0,e3) = e3. [assumption]. 59 op(op(e0,e0),e3) != op(e0,op(e0,e3)). [assumption]. 60 $F. [copy(59),rewrite([16(3),19(3),19(5),19(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=59. Kept=58. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=59. 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=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=419. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21508 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 6 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e0),e4),op(e0,op(e0,e4)))). Max_seconds is 119 for this subproblem. Child search process 21509 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(op(e0,e0),e4) != op(e0,op(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, e5, unit, op, inv ]). 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(e0,e0) = e0. [assumption]. 20 op(e0,e4) = e4. [assumption]. 59 op(op(e0,e0),e4) != op(e0,op(e0,e4)). [assumption]. 60 $F. [copy(59),rewrite([16(3),20(3),20(5),20(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=59. Kept=58. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=59. 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=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=419. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21509 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 7 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e0),e5),op(e0,op(e0,e5)))). Max_seconds is 119 for this subproblem. Child search process 21510 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(op(e0,e0),e5) != op(e0,op(e0,e5)). [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, e5, unit, op, inv ]). 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(e0,e0) = e0. [assumption]. 21 op(e0,e5) = e5. [assumption]. 59 op(op(e0,e0),e5) != op(e0,op(e0,e5)). [assumption]. 60 $F. [copy(59),rewrite([16(3),21(3),21(5),21(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=59. Kept=58. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=59. 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=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=419. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21510 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 8 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e1),e0),op(e0,op(e1,e0)))). Max_seconds is 119 for this subproblem. Child search process 21511 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(op(e0,e1),e0) != op(e0,op(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, e5, unit, op, inv ]). 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. 17 op(e0,e1) = e1. [assumption]. 22 op(e1,e0) = e1. [assumption]. 59 op(op(e0,e1),e0) != op(e0,op(e1,e0)). [assumption]. 60 $F. [copy(59),rewrite([17(3),22(3),22(5),17(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=59. Kept=58. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=59. 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=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=419. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21511 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 9 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e1),e1),op(e0,op(e1,e1)))). Max_seconds is 119 for this subproblem. Child search process 21512 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(op(e0,e1),e1) != op(e0,op(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, e5, unit, op, inv ]). 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. 16 op(e0,e0) = e0. [assumption]. 17 op(e0,e1) = e1. [assumption]. 23 op(e1,e1) = e0. [assumption]. 59 op(op(e0,e1),e1) != op(e0,op(e1,e1)). [assumption]. 60 $F. [copy(59),rewrite([17(3),23(3),23(5),16(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=59. Kept=58. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=59. 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=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=419. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21512 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 10 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e1),e2),op(e0,op(e1,e2)))). Max_seconds is 119 for this subproblem. Child search process 21513 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(op(e0,e1),e2) != op(e0,op(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, e5, unit, op, inv ]). 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. 17 op(e0,e1) = e1. [assumption]. 19 op(e0,e3) = e3. [assumption]. 24 op(e1,e2) = e3. [assumption]. 59 op(op(e0,e1),e2) != op(e0,op(e1,e2)). [assumption]. 60 $F. [copy(59),rewrite([17(3),24(3),24(5),19(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=59. Kept=58. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=59. 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=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=419. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21513 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 11 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e1),e3),op(e0,op(e1,e3)))). Max_seconds is 119 for this subproblem. Child search process 21514 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(op(e0,e1),e3) != op(e0,op(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, e5, unit, op, inv ]). 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. 17 op(e0,e1) = e1. [assumption]. 18 op(e0,e2) = e2. [assumption]. 25 op(e1,e3) = e2. [assumption]. 59 op(op(e0,e1),e3) != op(e0,op(e1,e3)). [assumption]. 60 $F. [copy(59),rewrite([17(3),25(3),25(5),18(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=59. Kept=58. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=59. 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=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=419. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21514 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 12 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e1),e4),op(e0,op(e1,e4)))). Max_seconds is 119 for this subproblem. Child search process 21515 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(op(e0,e1),e4) != op(e0,op(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, e5, unit, op, inv ]). 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. 17 op(e0,e1) = e1. [assumption]. 21 op(e0,e5) = e5. [assumption]. 26 op(e1,e4) = e5. [assumption]. 59 op(op(e0,e1),e4) != op(e0,op(e1,e4)). [assumption]. 60 $F. [copy(59),rewrite([17(3),26(3),26(5),21(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=59. Kept=58. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=59. 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=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=419. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21515 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 13 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e1),e5),op(e0,op(e1,e5)))). Max_seconds is 119 for this subproblem. Child search process 21516 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(op(e0,e1),e5) != op(e0,op(e1,e5)). [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, e5, unit, op, inv ]). 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. 17 op(e0,e1) = e1. [assumption]. 20 op(e0,e4) = e4. [assumption]. 27 op(e1,e5) = e4. [assumption]. 59 op(op(e0,e1),e5) != op(e0,op(e1,e5)). [assumption]. 60 $F. [copy(59),rewrite([17(3),27(3),27(5),20(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=59. Kept=58. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=59. 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=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=419. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21516 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 14 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e2),e0),op(e0,op(e2,e0)))). Max_seconds is 119 for this subproblem. Child search process 21517 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(op(e0,e2),e0) != op(e0,op(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, e5, unit, op, inv ]). 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(e0,e2) = e2. [assumption]. 28 op(e2,e0) = e2. [assumption]. 59 op(op(e0,e2),e0) != op(e0,op(e2,e0)). [assumption]. 60 $F. [copy(59),rewrite([18(3),28(3),28(5),18(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=59. Kept=58. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=59. 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=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=419. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21517 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 15 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e2),e1),op(e0,op(e2,e1)))). Max_seconds is 119 for this subproblem. Child search process 21518 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(op(e0,e2),e1) != op(e0,op(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, e5, unit, op, inv ]). 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. 18 op(e0,e2) = e2. [assumption]. 20 op(e0,e4) = e4. [assumption]. 29 op(e2,e1) = e4. [assumption]. 59 op(op(e0,e2),e1) != op(e0,op(e2,e1)). [assumption]. 60 $F. [copy(59),rewrite([18(3),29(3),29(5),20(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=59. Kept=58. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=59. 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=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=419. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21518 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 16 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e2),e2),op(e0,op(e2,e2)))). Max_seconds is 119 for this subproblem. Child search process 21519 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(op(e0,e2),e2) != op(e0,op(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, e5, unit, op, inv ]). 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. 16 op(e0,e0) = e0. [assumption]. 18 op(e0,e2) = e2. [assumption]. 30 op(e2,e2) = e0. [assumption]. 59 op(op(e0,e2),e2) != op(e0,op(e2,e2)). [assumption]. 60 $F. [copy(59),rewrite([18(3),30(3),30(5),16(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=59. Kept=58. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=59. 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=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=419. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21519 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 17 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e2),e3),op(e0,op(e2,e3)))). Max_seconds is 119 for this subproblem. Child search process 21520 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(op(e0,e2),e3) != op(e0,op(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, e5, unit, op, inv ]). 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. 18 op(e0,e2) = e2. [assumption]. 21 op(e0,e5) = e5. [assumption]. 31 op(e2,e3) = e5. [assumption]. 59 op(op(e0,e2),e3) != op(e0,op(e2,e3)). [assumption]. 60 $F. [copy(59),rewrite([18(3),31(3),31(5),21(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=59. Kept=58. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=59. 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=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=419. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21520 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 18 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e2),e4),op(e0,op(e2,e4)))). Max_seconds is 119 for this subproblem. Child search process 21521 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(op(e0,e2),e4) != op(e0,op(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, e5, unit, op, inv ]). 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. 17 op(e0,e1) = e1. [assumption]. 18 op(e0,e2) = e2. [assumption]. 32 op(e2,e4) = e1. [assumption]. 59 op(op(e0,e2),e4) != op(e0,op(e2,e4)). [assumption]. 60 $F. [copy(59),rewrite([18(3),32(3),32(5),17(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=59. Kept=58. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=59. 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=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=419. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21521 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 19 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e2),e5),op(e0,op(e2,e5)))). Max_seconds is 119 for this subproblem. Child search process 21522 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(op(e0,e2),e5) != op(e0,op(e2,e5)). [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, e5, unit, op, inv ]). 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. 18 op(e0,e2) = e2. [assumption]. 19 op(e0,e3) = e3. [assumption]. 33 op(e2,e5) = e3. [assumption]. 59 op(op(e0,e2),e5) != op(e0,op(e2,e5)). [assumption]. 60 $F. [copy(59),rewrite([18(3),33(3),33(5),19(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=59. Kept=58. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=59. 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=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=419. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21522 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 20 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e3),e0),op(e0,op(e3,e0)))). Max_seconds is 119 for this subproblem. Child search process 21523 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(op(e0,e3),e0) != op(e0,op(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, e5, unit, op, inv ]). 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(e0,e3) = e3. [assumption]. 34 op(e3,e0) = e3. [assumption]. 59 op(op(e0,e3),e0) != op(e0,op(e3,e0)). [assumption]. 60 $F. [copy(59),rewrite([19(3),34(3),34(5),19(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=59. Kept=58. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=59. 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=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=419. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21523 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 21 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e3),e1),op(e0,op(e3,e1)))). Max_seconds is 119 for this subproblem. Child search process 21524 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(op(e0,e3),e1) != op(e0,op(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, e5, unit, op, inv ]). 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. 19 op(e0,e3) = e3. [assumption]. 21 op(e0,e5) = e5. [assumption]. 35 op(e3,e1) = e5. [assumption]. 59 op(op(e0,e3),e1) != op(e0,op(e3,e1)). [assumption]. 60 $F. [copy(59),rewrite([19(3),35(3),35(5),21(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=59. Kept=58. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=59. 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=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=419. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21524 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 22 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e3),e2),op(e0,op(e3,e2)))). Max_seconds is 119 for this subproblem. Child search process 21525 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2. [assumption]. op(e5,e5) = e0. [assumption]. unit = e0. [assumption]. inv(e0) = e0. [assumption]. inv(e1) = e1. [assumption]. inv(e2) = e2. [assumption]. inv(e3) = e4. [assumption]. inv(e4) = e3. [assumption]. inv(e5) = e5. [assumption]. op(op(e0,e3),e2) != op(e0,op(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, e5, unit, op, inv ]). 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. 17 op(e0,e1) = e1. [assumption]. 19 op(e0,e3) = e3. [assumption]. 36 op(e3,e2) = e1. [assumption]. 59 op(op(e0,e3),e2) != op(e0,op(e3,e2)). [assumption]. 60 $F. [copy(59),rewrite([19(3),36(3),36(5),17(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=59. Kept=58. proofs=1. Usable=0. Sos=0. Demods=43. Limbo=58, Disabled=59. 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=43 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=419. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.43. User_CPU=0.00, System_CPU=0.00, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21525 exit (max_proofs) Wed May 7 22:14:43 2008 ============================== continuing FOF reduction multisearch == Subproblem 23 of 241 (negated): (- =(e1,e0) & - =(e2,e0) & - =(e3,e0) & - =(e4,e0) & - =(e5,e0) & - =(e2,e1) & - =(e3,e1) & - =(e4,e1) & - =(e5,e1) & - =(e3,e2) & - =(e4,e2) & - =(e5,e2) & - =(e4,e3) & - =(e5,e3) & - =(e5,e4) & =(op(e0,e0),e0) & =(op(e0,e1),e1) & =(op(e0,e2),e2) & =(op(e0,e3),e3) & =(op(e0,e4),e4) & =(op(e0,e5),e5) & =(op(e1,e0),e1) & =(op(e1,e1),e0) & =(op(e1,e2),e3) & =(op(e1,e3),e2) & =(op(e1,e4),e5) & =(op(e1,e5),e4) & =(op(e2,e0),e2) & =(op(e2,e1),e4) & =(op(e2,e2),e0) & =(op(e2,e3),e5) & =(op(e2,e4),e1) & =(op(e2,e5),e3) & =(op(e3,e0),e3) & =(op(e3,e1),e5) & =(op(e3,e2),e1) & =(op(e3,e3),e4) & =(op(e3,e4),e0) & =(op(e3,e5),e2) & =(op(e4,e0),e4) & =(op(e4,e1),e2) & =(op(e4,e2),e5) & =(op(e4,e3),e0) & =(op(e4,e4),e3) & =(op(e4,e5),e1) & =(op(e5,e0),e5) & =(op(e5,e1),e3) & =(op(e5,e2),e4) & =(op(e5,e3),e1) & =(op(e5,e4),e2) & =(op(e5,e5),e0) & =(unit,e0) & =(inv(e0),e0) & =(inv(e1),e1) & =(inv(e2),e2) & =(inv(e3),e4) & =(inv(e4),e3) & =(inv(e5),e5) & - =(op(op(e0,e3),e3),op(e0,op(e3,e3)))). Max_seconds is 119 for this subproblem. Child search process 21526 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]. e5 != e0. [assumption]. e2 != e1. [assumption]. e3 != e1. [assumption]. e4 != e1. [assumption]. e5 != e1. [assumption]. e3 != e2. [assumption]. e4 != e2. [assumption]. e5 != e2. [assumption]. e4 != e3. [assumption]. e5 != e3. [assumption]. e5 != e4. [assumption]. op(e0,e0) = e0. [assumption]. op(e0,e1) = e1. [assumption]. op(e0,e2) = e2. [assumption]. op(e0,e3) = e3. [assumption]. op(e0,e4) = e4. [assumption]. op(e0,e5) = e5. [assumption]. op(e1,e0) = e1. [assumption]. op(e1,e1) = e0. [assumption]. op(e1,e2) = e3. [assumption]. op(e1,e3) = e2. [assumption]. op(e1,e4) = e5. [assumption]. op(e1,e5) = e4. [assumption]. op(e2,e0) = e2. [assumption]. op(e2,e1) = e4. [assumption]. op(e2,e2) = e0. [assumption]. op(e2,e3) = e5. [assumption]. op(e2,e4) = e1. [assumption]. op(e2,e5) = e3. [assumption]. op(e3,e0) = e3. [assumption]. op(e3,e1) = e5. [assumption]. op(e3,e2) = e1. [assumption]. op(e3,e3) = e4. [assumption]. op(e3,e4) = e0. [assumption]. op(e3,e5) = e2. [assumption]. op(e4,e0) = e4. [assumption]. op(e4,e1) = e2. [assumption]. op(e4,e2) = e5. [assumption]. op(e4,e3) = e0. [assumption]. op(e4,e4) = e3. [assumption]. op(e4,e5) = e1. [assumption]. op(e5,e0) = e5. [assumption]. op(e5,e1) = e3. [assumption]. op(e5,e2) = e4. [assumption]. op(e5,e3) = e1. [assumption]. op(e5,e4) = e2.