%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG058+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 06:49:22 AM UTC 2026
% Result : Theorem 2.14s 2.80s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 52
% Number of leaves : 20
% Syntax : Number of formulae : 215 ( 80 unt; 14 def)
% Number of atoms : 1983 (1739 equ)
% Maximal formula atoms : 450 ( 9 avg)
% Number of connectives : 2541 ( 773 ~; 964 |; 790 &)
% ( 14 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 15 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax2,axiom,
( ( unit = e4
| unit = e3
| unit = e2
| unit = e1
| unit = e0 )
& op(e4,unit) = e4
& op(unit,e4) = e4
& op(e3,unit) = e3
& op(unit,e3) = e3
& op(e2,unit) = e2
& op(unit,e2) = e2
& op(e1,unit) = e1
& op(unit,e1) = e1
& op(e0,unit) = e0
& op(unit,e0) = e0 ),
file('theBenchmark.p',ax2) ).
fof(ax3,axiom,
( ( op(e4,e4) = e4
| op(e3,e4) = e4
| op(e2,e4) = e4
| op(e1,e4) = e4
| op(e0,e4) = e4 )
& ( op(e4,e4) = e4
| op(e4,e3) = e4
| op(e4,e2) = e4
| op(e4,e1) = e4
| op(e4,e0) = e4 )
& ( op(e4,e4) = e3
| op(e3,e4) = e3
| op(e2,e4) = e3
| op(e1,e4) = e3
| op(e0,e4) = e3 )
& ( op(e4,e4) = e3
| op(e4,e3) = e3
| op(e4,e2) = e3
| op(e4,e1) = e3
| op(e4,e0) = e3 )
& ( op(e4,e4) = e2
| op(e3,e4) = e2
| op(e2,e4) = e2
| op(e1,e4) = e2
| op(e0,e4) = e2 )
& ( op(e4,e4) = e2
| op(e4,e3) = e2
| op(e4,e2) = e2
| op(e4,e1) = e2
| op(e4,e0) = e2 )
& ( op(e4,e4) = e1
| op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| op(e0,e4) = e1 )
& ( op(e4,e4) = e1
| op(e4,e3) = e1
| op(e4,e2) = e1
| op(e4,e1) = e1
| op(e4,e0) = e1 )
& ( op(e4,e4) = e0
| op(e3,e4) = e0
| op(e2,e4) = e0
| op(e1,e4) = e0
| op(e0,e4) = e0 )
& ( op(e4,e4) = e0
| op(e4,e3) = e0
| op(e4,e2) = e0
| op(e4,e1) = e0
| op(e4,e0) = e0 )
& ( op(e4,e3) = e4
| op(e3,e3) = e4
| op(e2,e3) = e4
| op(e1,e3) = e4
| op(e0,e3) = e4 )
& ( op(e3,e4) = e4
| op(e3,e3) = e4
| op(e3,e2) = e4
| op(e3,e1) = e4
| op(e3,e0) = e4 )
& ( op(e4,e3) = e3
| op(e3,e3) = e3
| op(e2,e3) = e3
| op(e1,e3) = e3
| op(e0,e3) = e3 )
& ( op(e3,e4) = e3
| op(e3,e3) = e3
| op(e3,e2) = e3
| op(e3,e1) = e3
| op(e3,e0) = e3 )
& ( op(e4,e3) = e2
| op(e3,e3) = e2
| op(e2,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2 )
& ( op(e3,e4) = e2
| op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 )
& ( op(e4,e3) = e1
| op(e3,e3) = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 )
& ( op(e3,e4) = e1
| op(e3,e3) = e1
| op(e3,e2) = e1
| op(e3,e1) = e1
| op(e3,e0) = e1 )
& ( op(e4,e3) = e0
| op(e3,e3) = e0
| op(e2,e3) = e0
| op(e1,e3) = e0
| op(e0,e3) = e0 )
& ( op(e3,e4) = e0
| op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 )
& ( op(e4,e2) = e4
| op(e3,e2) = e4
| op(e2,e2) = e4
| op(e1,e2) = e4
| op(e0,e2) = e4 )
& ( op(e2,e4) = e4
| op(e2,e3) = e4
| op(e2,e2) = e4
| op(e2,e1) = e4
| op(e2,e0) = e4 )
& ( op(e4,e2) = e3
| op(e3,e2) = e3
| op(e2,e2) = e3
| op(e1,e2) = e3
| op(e0,e2) = e3 )
& ( op(e2,e4) = e3
| op(e2,e3) = e3
| op(e2,e2) = e3
| op(e2,e1) = e3
| op(e2,e0) = e3 )
& ( op(e4,e2) = e2
| op(e3,e2) = e2
| op(e2,e2) = e2
| op(e1,e2) = e2
| op(e0,e2) = e2 )
& ( op(e2,e4) = e2
| op(e2,e3) = e2
| op(e2,e2) = e2
| op(e2,e1) = e2
| op(e2,e0) = e2 )
& ( op(e4,e2) = e1
| op(e3,e2) = e1
| op(e2,e2) = e1
| op(e1,e2) = e1
| op(e0,e2) = e1 )
& ( op(e2,e4) = e1
| op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 )
& ( op(e4,e2) = e0
| op(e3,e2) = e0
| op(e2,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 )
& ( op(e2,e4) = e0
| op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 )
& ( op(e4,e1) = e4
| op(e3,e1) = e4
| op(e2,e1) = e4
| op(e1,e1) = e4
| op(e0,e1) = e4 )
& ( op(e1,e4) = e4
| op(e1,e3) = e4
| op(e1,e2) = e4
| op(e1,e1) = e4
| op(e1,e0) = e4 )
& ( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(e0,e1) = e3 )
& ( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 )
& ( op(e4,e1) = e2
| op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(e0,e1) = e2 )
& ( op(e1,e4) = e2
| op(e1,e3) = e2
| op(e1,e2) = e2
| op(e1,e1) = e2
| op(e1,e0) = e2 )
& ( op(e4,e1) = e1
| op(e3,e1) = e1
| op(e2,e1) = e1
| op(e1,e1) = e1
| op(e0,e1) = e1 )
& ( op(e1,e4) = e1
| op(e1,e3) = e1
| op(e1,e2) = e1
| op(e1,e1) = e1
| op(e1,e0) = e1 )
& ( op(e4,e1) = e0
| op(e3,e1) = e0
| op(e2,e1) = e0
| op(e1,e1) = e0
| op(e0,e1) = e0 )
& ( op(e1,e4) = e0
| op(e1,e3) = e0
| op(e1,e2) = e0
| op(e1,e1) = e0
| op(e1,e0) = e0 )
& ( op(e4,e0) = e4
| op(e3,e0) = e4
| op(e2,e0) = e4
| op(e1,e0) = e4
| op(e0,e0) = e4 )
& ( op(e0,e4) = e4
| op(e0,e3) = e4
| op(e0,e2) = e4
| op(e0,e1) = e4
| op(e0,e0) = e4 )
& ( op(e4,e0) = e3
| op(e3,e0) = e3
| op(e2,e0) = e3
| op(e1,e0) = e3
| op(e0,e0) = e3 )
& ( op(e0,e4) = e3
| op(e0,e3) = e3
| op(e0,e2) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 )
& ( op(e4,e0) = e2
| op(e3,e0) = e2
| op(e2,e0) = e2
| op(e1,e0) = e2
| op(e0,e0) = e2 )
& ( op(e0,e4) = e2
| op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 )
& ( op(e4,e0) = e1
| op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e0) = e1 )
& ( op(e0,e4) = e1
| op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(e0,e0) = e1 )
& ( op(e4,e0) = e0
| op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0
| op(e0,e0) = e0 )
& ( op(e0,e4) = e0
| op(e0,e3) = e0
| op(e0,e2) = e0
| op(e0,e1) = e0
| op(e0,e0) = e0 ) ),
file('theBenchmark.p',ax3) ).
fof(ax4,axiom,
( op(e4,e3) != op(e4,e4)
& op(e4,e2) != op(e4,e4)
& op(e4,e2) != op(e4,e3)
& op(e4,e1) != op(e4,e4)
& op(e4,e1) != op(e4,e3)
& op(e4,e1) != op(e4,e2)
& op(e4,e0) != op(e4,e4)
& op(e4,e0) != op(e4,e3)
& op(e4,e0) != op(e4,e2)
& op(e4,e0) != op(e4,e1)
& op(e3,e3) != op(e3,e4)
& op(e3,e2) != op(e3,e4)
& op(e3,e2) != op(e3,e3)
& op(e3,e1) != op(e3,e4)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e0) != op(e3,e4)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e1)
& op(e2,e3) != op(e2,e4)
& op(e2,e2) != op(e2,e4)
& op(e2,e2) != op(e2,e3)
& op(e2,e1) != op(e2,e4)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e0) != op(e2,e4)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e1)
& op(e1,e3) != op(e1,e4)
& op(e1,e2) != op(e1,e4)
& op(e1,e2) != op(e1,e3)
& op(e1,e1) != op(e1,e4)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e0) != op(e1,e4)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e1)
& op(e0,e3) != op(e0,e4)
& op(e0,e2) != op(e0,e4)
& op(e0,e2) != op(e0,e3)
& op(e0,e1) != op(e0,e4)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e0) != op(e0,e4)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e1)
& op(e3,e4) != op(e4,e4)
& op(e2,e4) != op(e4,e4)
& op(e2,e4) != op(e3,e4)
& op(e1,e4) != op(e4,e4)
& op(e1,e4) != op(e3,e4)
& op(e1,e4) != op(e2,e4)
& op(e0,e4) != op(e4,e4)
& op(e0,e4) != op(e3,e4)
& op(e0,e4) != op(e2,e4)
& op(e0,e4) != op(e1,e4)
& op(e3,e3) != op(e4,e3)
& op(e2,e3) != op(e4,e3)
& op(e2,e3) != op(e3,e3)
& op(e1,e3) != op(e4,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e0,e3) != op(e4,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e1,e3)
& op(e3,e2) != op(e4,e2)
& op(e2,e2) != op(e4,e2)
& op(e2,e2) != op(e3,e2)
& op(e1,e2) != op(e4,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e0,e2) != op(e4,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e1,e2)
& op(e3,e1) != op(e4,e1)
& op(e2,e1) != op(e4,e1)
& op(e2,e1) != op(e3,e1)
& op(e1,e1) != op(e4,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e0,e1) != op(e4,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e1,e1)
& op(e3,e0) != op(e4,e0)
& op(e2,e0) != op(e4,e0)
& op(e2,e0) != op(e3,e0)
& op(e1,e0) != op(e4,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e0,e0) != op(e4,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e1,e0) ),
file('theBenchmark.p',ax4) ).
fof(ax5,axiom,
( e3 != e4
& e2 != e4
& e2 != e3
& e1 != e4
& e1 != e3
& e1 != e2
& e0 != e4
& e0 != e3
& e0 != e2
& e0 != e1 ),
file('theBenchmark.p',ax5) ).
fof(ax6,axiom,
( e4 = op(op(e2,e2),op(e2,e2))
& e3 = op(e2,e2)
& e1 = op(op(e2,e2),e2)
& e0 = op(op(op(e2,e2),e2),op(op(e2,e2),e2)) ),
file('theBenchmark.p',ax6) ).
fof(co1,conjecture,
~ ( ( ( op(e4,e4) != e4
& op(e4,e4) = e4
& op(e4,e4) = e4 )
| ( op(e4,e3) != e4
& op(e3,e3) = e4
& op(e4,e4) = e3 )
| ( op(e4,e2) != e4
& op(e2,e2) = e4
& op(e4,e4) = e2 )
| ( op(e4,e1) != e4
& op(e1,e1) = e4
& op(e4,e4) = e1 )
| ( op(e4,e0) != e4
& op(e0,e0) = e4
& op(e4,e4) = e0 )
| ( op(e3,e4) != e3
& op(e4,e4) = e3
& op(e3,e3) = e4 )
| ( op(e3,e3) != e3
& op(e3,e3) = e3
& op(e3,e3) = e3 )
| ( op(e3,e2) != e3
& op(e2,e2) = e3
& op(e3,e3) = e2 )
| ( op(e3,e1) != e3
& op(e1,e1) = e3
& op(e3,e3) = e1 )
| ( op(e3,e0) != e3
& op(e0,e0) = e3
& op(e3,e3) = e0 )
| ( op(e2,e4) != e2
& op(e4,e4) = e2
& op(e2,e2) = e4 )
| ( op(e2,e3) != e2
& op(e3,e3) = e2
& op(e2,e2) = e3 )
| ( op(e2,e2) != e2
& op(e2,e2) = e2
& op(e2,e2) = e2 )
| ( op(e2,e1) != e2
& op(e1,e1) = e2
& op(e2,e2) = e1 )
| ( op(e2,e0) != e2
& op(e0,e0) = e2
& op(e2,e2) = e0 )
| ( op(e1,e4) != e1
& op(e4,e4) = e1
& op(e1,e1) = e4 )
| ( op(e1,e3) != e1
& op(e3,e3) = e1
& op(e1,e1) = e3 )
| ( op(e1,e2) != e1
& op(e2,e2) = e1
& op(e1,e1) = e2 )
| ( op(e1,e1) != e1
& op(e1,e1) = e1
& op(e1,e1) = e1 )
| ( op(e1,e0) != e1
& op(e0,e0) = e1
& op(e1,e1) = e0 )
| ( op(e0,e4) != e0
& op(e4,e4) = e0
& op(e0,e0) = e4 )
| ( op(e0,e3) != e0
& op(e3,e3) = e0
& op(e0,e0) = e3 )
| ( op(e0,e2) != e0
& op(e2,e2) = e0
& op(e0,e0) = e2 )
| ( op(e0,e1) != e0
& op(e1,e1) = e0
& op(e0,e0) = e1 )
| ( op(e0,e0) != e0
& op(e0,e0) = e0
& op(e0,e0) = e0 ) )
& ( ( ( ( e4 != unit
& op(e4,e4) = e4 )
| op(e4,e4) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e3 )
| op(e4,e3) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e2 )
| op(e4,e2) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e1 )
| op(e4,e1) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e0 )
| op(e4,e0) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e4 )
| op(e3,e4) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e3 )
| op(e3,e3) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e2 )
| op(e3,e2) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e1 )
| op(e3,e1) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e0 )
| op(e3,e0) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e4 )
| op(e2,e4) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e3 )
| op(e2,e3) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e2 )
| op(e2,e2) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e1 )
| op(e2,e1) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e0 )
| op(e2,e0) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e4 )
| op(e1,e4) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e3 )
| op(e1,e3) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e2 )
| op(e1,e2) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e1 )
| op(e1,e1) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e0 )
| op(e1,e0) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e4 )
| op(e0,e4) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e3 )
| op(e0,e3) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e2 )
| op(e0,e2) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e1 )
| op(e0,e1) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e0 )
| op(e0,e0) != e4 ) )
| ( ( ( e3 != unit
& op(e4,e3) = e4 )
| op(e4,e4) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e3 )
| op(e4,e3) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e2 )
| op(e4,e2) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e1 )
| op(e4,e1) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e0 )
| op(e4,e0) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e4 )
| op(e3,e4) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e3 )
| op(e3,e3) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e2 )
| op(e3,e2) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e1 )
| op(e3,e1) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e0 )
| op(e3,e0) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e4 )
| op(e2,e4) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e3 )
| op(e2,e3) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e2 )
| op(e2,e2) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e1 )
| op(e2,e1) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e0 )
| op(e2,e0) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e4 )
| op(e1,e4) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e3 )
| op(e1,e3) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e2 )
| op(e1,e2) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e1 )
| op(e1,e1) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e0 )
| op(e1,e0) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e4 )
| op(e0,e4) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e3 )
| op(e0,e3) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e2 )
| op(e0,e2) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e1 )
| op(e0,e1) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e0 )
| op(e0,e0) != e3 ) )
| ( ( ( e2 != unit
& op(e4,e2) = e4 )
| op(e4,e4) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e3 )
| op(e4,e3) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e2 )
| op(e4,e2) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e1 )
| op(e4,e1) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e0 )
| op(e4,e0) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e4 )
| op(e3,e4) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e3 )
| op(e3,e3) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e2 )
| op(e3,e2) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e1 )
| op(e3,e1) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e0 )
| op(e3,e0) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e4 )
| op(e2,e4) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e3 )
| op(e2,e3) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e2 )
| op(e2,e2) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e1 )
| op(e2,e1) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e0 )
| op(e2,e0) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e4 )
| op(e1,e4) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e3 )
| op(e1,e3) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e2 )
| op(e1,e2) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e1 )
| op(e1,e1) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e0 )
| op(e1,e0) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e4 )
| op(e0,e4) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e3 )
| op(e0,e3) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e2 )
| op(e0,e2) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e1 )
| op(e0,e1) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e0 )
| op(e0,e0) != e2 ) )
| ( ( ( e1 != unit
& op(e4,e1) = e4 )
| op(e4,e4) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e3 )
| op(e4,e3) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e2 )
| op(e4,e2) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e1 )
| op(e4,e1) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e0 )
| op(e4,e0) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e4 )
| op(e3,e4) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e3 )
| op(e3,e3) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e2 )
| op(e3,e2) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e1 )
| op(e3,e1) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e0 )
| op(e3,e0) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e4 )
| op(e2,e4) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e3 )
| op(e2,e3) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e2 )
| op(e2,e2) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e1 )
| op(e2,e1) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e0 )
| op(e2,e0) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e4 )
| op(e1,e4) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e3 )
| op(e1,e3) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e2 )
| op(e1,e2) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e1 )
| op(e1,e1) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e0 )
| op(e1,e0) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e4 )
| op(e0,e4) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e3 )
| op(e0,e3) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e2 )
| op(e0,e2) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e1 )
| op(e0,e1) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e0 )
| op(e0,e0) != e1 ) )
| ( ( ( e0 != unit
& op(e4,e0) = e4 )
| op(e4,e4) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e3 )
| op(e4,e3) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e2 )
| op(e4,e2) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e1 )
| op(e4,e1) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e0 )
| op(e4,e0) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e4 )
| op(e3,e4) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e3 )
| op(e3,e3) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e2 )
| op(e3,e2) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e1 )
| op(e3,e1) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e0 )
| op(e3,e0) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e4 )
| op(e2,e4) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e3 )
| op(e2,e3) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e2 )
| op(e2,e2) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e1 )
| op(e2,e1) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e0 )
| op(e2,e0) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e4 )
| op(e1,e4) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e3 )
| op(e1,e3) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e2 )
| op(e1,e2) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e1 )
| op(e1,e1) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e0 )
| op(e1,e0) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e4 )
| op(e0,e4) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e3 )
| op(e0,e3) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e2 )
| op(e0,e2) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e1 )
| op(e0,e1) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e0 )
| op(e0,e0) != e0 ) ) ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ~ ( ( ( op(e4,e4) != e4
& op(e4,e4) = e4
& op(e4,e4) = e4 )
| ( op(e4,e3) != e4
& op(e3,e3) = e4
& op(e4,e4) = e3 )
| ( op(e4,e2) != e4
& op(e2,e2) = e4
& op(e4,e4) = e2 )
| ( op(e4,e1) != e4
& op(e1,e1) = e4
& op(e4,e4) = e1 )
| ( op(e4,e0) != e4
& op(e0,e0) = e4
& op(e4,e4) = e0 )
| ( op(e3,e4) != e3
& op(e4,e4) = e3
& op(e3,e3) = e4 )
| ( op(e3,e3) != e3
& op(e3,e3) = e3
& op(e3,e3) = e3 )
| ( op(e3,e2) != e3
& op(e2,e2) = e3
& op(e3,e3) = e2 )
| ( op(e3,e1) != e3
& op(e1,e1) = e3
& op(e3,e3) = e1 )
| ( op(e3,e0) != e3
& op(e0,e0) = e3
& op(e3,e3) = e0 )
| ( op(e2,e4) != e2
& op(e4,e4) = e2
& op(e2,e2) = e4 )
| ( op(e2,e3) != e2
& op(e3,e3) = e2
& op(e2,e2) = e3 )
| ( op(e2,e2) != e2
& op(e2,e2) = e2
& op(e2,e2) = e2 )
| ( op(e2,e1) != e2
& op(e1,e1) = e2
& op(e2,e2) = e1 )
| ( op(e2,e0) != e2
& op(e0,e0) = e2
& op(e2,e2) = e0 )
| ( op(e1,e4) != e1
& op(e4,e4) = e1
& op(e1,e1) = e4 )
| ( op(e1,e3) != e1
& op(e3,e3) = e1
& op(e1,e1) = e3 )
| ( op(e1,e2) != e1
& op(e2,e2) = e1
& op(e1,e1) = e2 )
| ( op(e1,e1) != e1
& op(e1,e1) = e1
& op(e1,e1) = e1 )
| ( op(e1,e0) != e1
& op(e0,e0) = e1
& op(e1,e1) = e0 )
| ( op(e0,e4) != e0
& op(e4,e4) = e0
& op(e0,e0) = e4 )
| ( op(e0,e3) != e0
& op(e3,e3) = e0
& op(e0,e0) = e3 )
| ( op(e0,e2) != e0
& op(e2,e2) = e0
& op(e0,e0) = e2 )
| ( op(e0,e1) != e0
& op(e1,e1) = e0
& op(e0,e0) = e1 )
| ( op(e0,e0) != e0
& op(e0,e0) = e0
& op(e0,e0) = e0 ) )
& ( ( ( ( e4 != unit
& op(e4,e4) = e4 )
| op(e4,e4) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e3 )
| op(e4,e3) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e2 )
| op(e4,e2) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e1 )
| op(e4,e1) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e0 )
| op(e4,e0) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e4 )
| op(e3,e4) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e3 )
| op(e3,e3) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e2 )
| op(e3,e2) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e1 )
| op(e3,e1) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e0 )
| op(e3,e0) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e4 )
| op(e2,e4) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e3 )
| op(e2,e3) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e2 )
| op(e2,e2) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e1 )
| op(e2,e1) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e0 )
| op(e2,e0) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e4 )
| op(e1,e4) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e3 )
| op(e1,e3) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e2 )
| op(e1,e2) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e1 )
| op(e1,e1) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e0 )
| op(e1,e0) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e4 )
| op(e0,e4) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e3 )
| op(e0,e3) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e2 )
| op(e0,e2) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e1 )
| op(e0,e1) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e0 )
| op(e0,e0) != e4 ) )
| ( ( ( e3 != unit
& op(e4,e3) = e4 )
| op(e4,e4) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e3 )
| op(e4,e3) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e2 )
| op(e4,e2) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e1 )
| op(e4,e1) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e0 )
| op(e4,e0) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e4 )
| op(e3,e4) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e3 )
| op(e3,e3) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e2 )
| op(e3,e2) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e1 )
| op(e3,e1) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e0 )
| op(e3,e0) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e4 )
| op(e2,e4) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e3 )
| op(e2,e3) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e2 )
| op(e2,e2) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e1 )
| op(e2,e1) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e0 )
| op(e2,e0) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e4 )
| op(e1,e4) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e3 )
| op(e1,e3) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e2 )
| op(e1,e2) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e1 )
| op(e1,e1) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e0 )
| op(e1,e0) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e4 )
| op(e0,e4) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e3 )
| op(e0,e3) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e2 )
| op(e0,e2) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e1 )
| op(e0,e1) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e0 )
| op(e0,e0) != e3 ) )
| ( ( ( e2 != unit
& op(e4,e2) = e4 )
| op(e4,e4) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e3 )
| op(e4,e3) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e2 )
| op(e4,e2) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e1 )
| op(e4,e1) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e0 )
| op(e4,e0) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e4 )
| op(e3,e4) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e3 )
| op(e3,e3) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e2 )
| op(e3,e2) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e1 )
| op(e3,e1) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e0 )
| op(e3,e0) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e4 )
| op(e2,e4) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e3 )
| op(e2,e3) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e2 )
| op(e2,e2) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e1 )
| op(e2,e1) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e0 )
| op(e2,e0) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e4 )
| op(e1,e4) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e3 )
| op(e1,e3) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e2 )
| op(e1,e2) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e1 )
| op(e1,e1) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e0 )
| op(e1,e0) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e4 )
| op(e0,e4) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e3 )
| op(e0,e3) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e2 )
| op(e0,e2) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e1 )
| op(e0,e1) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e0 )
| op(e0,e0) != e2 ) )
| ( ( ( e1 != unit
& op(e4,e1) = e4 )
| op(e4,e4) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e3 )
| op(e4,e3) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e2 )
| op(e4,e2) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e1 )
| op(e4,e1) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e0 )
| op(e4,e0) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e4 )
| op(e3,e4) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e3 )
| op(e3,e3) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e2 )
| op(e3,e2) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e1 )
| op(e3,e1) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e0 )
| op(e3,e0) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e4 )
| op(e2,e4) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e3 )
| op(e2,e3) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e2 )
| op(e2,e2) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e1 )
| op(e2,e1) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e0 )
| op(e2,e0) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e4 )
| op(e1,e4) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e3 )
| op(e1,e3) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e2 )
| op(e1,e2) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e1 )
| op(e1,e1) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e0 )
| op(e1,e0) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e4 )
| op(e0,e4) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e3 )
| op(e0,e3) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e2 )
| op(e0,e2) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e1 )
| op(e0,e1) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e0 )
| op(e0,e0) != e1 ) )
| ( ( ( e0 != unit
& op(e4,e0) = e4 )
| op(e4,e4) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e3 )
| op(e4,e3) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e2 )
| op(e4,e2) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e1 )
| op(e4,e1) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e0 )
| op(e4,e0) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e4 )
| op(e3,e4) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e3 )
| op(e3,e3) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e2 )
| op(e3,e2) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e1 )
| op(e3,e1) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e0 )
| op(e3,e0) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e4 )
| op(e2,e4) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e3 )
| op(e2,e3) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e2 )
| op(e2,e2) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e1 )
| op(e2,e1) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e0 )
| op(e2,e0) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e4 )
| op(e1,e4) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e3 )
| op(e1,e3) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e2 )
| op(e1,e2) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e1 )
| op(e1,e1) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e0 )
| op(e1,e0) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e4 )
| op(e0,e4) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e3 )
| op(e0,e3) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e2 )
| op(e0,e2) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e1 )
| op(e0,e1) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e0 )
| op(e0,e0) != e0 ) ) ) ),
inference(assume_negation,[status(cth)],[co1]) ).
cnf(c_33,plain,
op(unit,e0) = e0,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_35,plain,
op(unit,e1) = e1,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_36,plain,
op(e1,unit) = e1,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_37,plain,
op(unit,e2) = e2,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_39,plain,
op(unit,e3) = e3,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_40,plain,
op(e3,unit) = e3,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_41,plain,
op(unit,e4) = e4,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_42,plain,
op(e4,unit) = e4,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_43,plain,
( unit = e4
| unit = e3
| unit = e2
| unit = e1
| unit = e0 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_61,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(e0,e1) = e3 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_74,plain,
( op(e3,e4) = e0
| op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_84,plain,
( op(e4,e4) = e0
| op(e4,e3) = e0
| op(e4,e2) = e0
| op(e4,e1) = e0
| op(e4,e0) = e0 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_111,plain,
op(e4,e0) != op(e3,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_112,plain,
op(e3,e0) != op(e4,e0),
inference(copy,[status(thm)],[c_111]) ).
cnf(c_122,plain,
op(e3,e1) != op(e1,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_123,plain,
op(e1,e1) != op(e3,e1),
inference(copy,[status(thm)],[c_122]) ).
cnf(c_124,plain,
op(e4,e1) != op(e1,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_125,plain,
op(e1,e1) != op(e4,e1),
inference(copy,[status(thm)],[c_124]) ).
cnf(c_141,plain,
op(e3,e2) != op(e1,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_142,plain,
op(e1,e2) != op(e3,e2),
inference(copy,[status(thm)],[c_141]) ).
cnf(c_189,plain,
op(e0,e1) != op(e0,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_194,plain,
op(e0,e4) != op(e0,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_195,plain,
op(e0,e0) != op(e0,e4),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_208,plain,
op(e1,e1) != op(e1,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_234,plain,
op(e2,e2) != op(e2,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_235,plain,
op(e2,e1) != op(e2,e2),
inference(copy,[status(thm)],[c_234]) ).
cnf(c_246,plain,
op(e3,e1) != op(e3,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_253,plain,
op(e3,e2) != op(e3,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_254,plain,
op(e3,e1) != op(e3,e2),
inference(copy,[status(thm)],[c_253]) ).
cnf(c_276,plain,
op(e4,e4) != op(e4,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_277,plain,
op(e4,e1) != op(e4,e4),
inference(copy,[status(thm)],[c_276]) ).
cnf(c_284,plain,
e1 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_285,plain,
e2 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_286,plain,
e0 != e2,
inference(copy,[status(thm)],[c_285]) ).
cnf(c_287,plain,
e3 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_288,plain,
e0 != e3,
inference(copy,[status(thm)],[c_287]) ).
cnf(c_289,plain,
e4 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_290,plain,
e0 != e4,
inference(copy,[status(thm)],[c_289]) ).
cnf(c_293,plain,
e3 != e1,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_294,plain,
e1 != e3,
inference(copy,[status(thm)],[c_293]) ).
cnf(c_295,plain,
e4 != e1,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_296,plain,
e1 != e4,
inference(copy,[status(thm)],[c_295]) ).
cnf(c_299,plain,
e4 != e2,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_300,plain,
e2 != e4,
inference(copy,[status(thm)],[c_299]) ).
cnf(c_301,plain,
e4 != e3,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_302,plain,
e3 != e4,
inference(copy,[status(thm)],[c_301]) ).
cnf(c_303,plain,
op(op(op(e2,e2),e2),op(op(e2,e2),e2)) = e0,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_304,plain,
op(op(e2,e2),e2) = e1,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_305,plain,
op(e2,e2) = e3,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_306,plain,
op(op(e2,e2),op(e2,e2)) = e4,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_1812,plain,
op(e3,op(e2,e2)) = e4,
inference(paramod,[status(thm)],[c_305,c_306]) ).
cnf(c_307,plain,
op(e3,e3) = e4,
inference(paramod,[status(thm)],[c_305,c_1812]) ).
fof(def_defn_40,definition,
( defn_40
<=> ( op(e0,e1) != e0
& op(e1,e1) = e0
& op(e0,e0) = e1 ) ),
introduced(definition,[new_symbols(definition,[defn_40])],[]) ).
fof(def_defn_50,definition,
( defn_50
<=> ( op(e0,e2) != e0
& op(e2,e2) = e0
& op(e0,e0) = e2 ) ),
introduced(definition,[new_symbols(definition,[defn_50])],[]) ).
fof(def_defn_60,definition,
( defn_60
<=> ( op(e0,e3) != e0
& op(e3,e3) = e0
& op(e0,e0) = e3 ) ),
introduced(definition,[new_symbols(definition,[defn_60])],[]) ).
fof(def_defn_70,definition,
( defn_70
<=> ( op(e0,e4) != e0
& op(e4,e4) = e0
& op(e0,e0) = e4 ) ),
introduced(definition,[new_symbols(definition,[defn_70])],[]) ).
fof(def_defn_80,definition,
( defn_80
<=> ( op(e1,e0) != e1
& op(e0,e0) = e1
& op(e1,e1) = e0 ) ),
introduced(definition,[new_symbols(definition,[defn_80])],[]) ).
fof(def_defn_90,definition,
( defn_90
<=> ( op(e1,e2) != e1
& op(e2,e2) = e1
& op(e1,e1) = e2 ) ),
introduced(definition,[new_symbols(definition,[defn_90])],[]) ).
fof(def_defn_100,definition,
( defn_100
<=> ( op(e1,e3) != e1
& op(e3,e3) = e1
& op(e1,e1) = e3 ) ),
introduced(definition,[new_symbols(definition,[defn_100])],[]) ).
fof(def_defn_110,definition,
( defn_110
<=> ( op(e1,e4) != e1
& op(e4,e4) = e1
& op(e1,e1) = e4 ) ),
introduced(definition,[new_symbols(definition,[defn_110])],[]) ).
fof(def_defn_120,definition,
( defn_120
<=> ( op(e2,e0) != e2
& op(e0,e0) = e2
& op(e2,e2) = e0 ) ),
introduced(definition,[new_symbols(definition,[defn_120])],[]) ).
fof(def_defn_130,definition,
( defn_130
<=> ( op(e2,e1) != e2
& op(e1,e1) = e2
& op(e2,e2) = e1 ) ),
introduced(definition,[new_symbols(definition,[defn_130])],[]) ).
fof(def_defn_140,definition,
( defn_140
<=> ( op(e2,e3) != e2
& op(e3,e3) = e2
& op(e2,e2) = e3 ) ),
introduced(definition,[new_symbols(definition,[defn_140])],[]) ).
fof(def_defn_150,definition,
( defn_150
<=> ( op(e2,e4) != e2
& op(e4,e4) = e2
& op(e2,e2) = e4 ) ),
introduced(definition,[new_symbols(definition,[defn_150])],[]) ).
fof(def_defn_160,definition,
( defn_160
<=> ( op(e3,e0) != e3
& op(e0,e0) = e3
& op(e3,e3) = e0 ) ),
introduced(definition,[new_symbols(definition,[defn_160])],[]) ).
fof(def_defn_170,definition,
( defn_170
<=> ( op(e3,e1) != e3
& op(e1,e1) = e3
& op(e3,e3) = e1 ) ),
introduced(definition,[new_symbols(definition,[defn_170])],[]) ).
cnf(c_398,negated_conjecture,
( op(e2,e2) = e4
| op(e1,e1) = e4
| op(e0,e0) = e4
| op(e4,e4) = e3
| op(e3,e3) = e2
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_40,def_defn_50,def_defn_60,def_defn_70,def_defn_80,def_defn_90,def_defn_100,def_defn_110,def_defn_120,def_defn_130,def_defn_140,def_defn_150,def_defn_160,def_defn_170]) ).
cnf(c_1813,negated_conjecture,
( op(e2,e2) = e4
| op(e1,e1) = e4
| op(e0,e0) = e4
| op(e4,e4) = e3
| e4 = e2
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40 ),
inference(paramod,[status(thm)],[c_307,c_398]) ).
cnf(c_1814,negated_conjecture,
( e3 = e4
| op(e1,e1) = e4
| op(e0,e0) = e4
| op(e4,e4) = e3
| e4 = e2
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40 ),
inference(paramod,[status(thm)],[c_305,c_1813]) ).
cnf(c_1815,negated_conjecture,
( e3 = e4
| op(e1,e1) = e4
| op(e0,e0) = e4
| op(e4,e4) = e3
| e2 = e4
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40 ),
inference(copy,[status(thm)],[c_1814]) ).
cnf(c_1816,negated_conjecture,
( e3 = e4
| op(e1,e1) = e4
| op(e0,e0) = e4
| op(e4,e4) = e3
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40 ),
inference(resolve,[status(thm)],[c_300,c_1815]) ).
cnf(c_399,negated_conjecture,
( op(e1,e1) = e4
| op(e0,e0) = e4
| op(e4,e4) = e3
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40 ),
inference(resolve,[status(thm)],[c_302,c_1816]) ).
cnf(c_594,negated_conjecture,
( op(e3,e3) = e1
| ~ defn_170 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_170]) ).
cnf(c_1817,negated_conjecture,
( e4 = e1
| ~ defn_170 ),
inference(paramod,[status(thm)],[c_307,c_594]) ).
cnf(c_1818,negated_conjecture,
( e1 = e4
| ~ defn_170 ),
inference(copy,[status(thm)],[c_1817]) ).
cnf(c_595,negated_conjecture,
~ defn_170,
inference(resolve,[status(thm)],[c_296,c_1818]) ).
cnf(c_598,negated_conjecture,
( op(e3,e3) = e0
| ~ defn_160 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_160]) ).
cnf(c_1819,negated_conjecture,
( e4 = e0
| ~ defn_160 ),
inference(paramod,[status(thm)],[c_307,c_598]) ).
cnf(c_1820,negated_conjecture,
( e0 = e4
| ~ defn_160 ),
inference(copy,[status(thm)],[c_1819]) ).
cnf(c_599,negated_conjecture,
~ defn_160,
inference(resolve,[status(thm)],[c_290,c_1820]) ).
cnf(c_602,negated_conjecture,
( op(e2,e2) = e4
| ~ defn_150 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_150]) ).
cnf(c_1821,negated_conjecture,
( e3 = e4
| ~ defn_150 ),
inference(paramod,[status(thm)],[c_305,c_602]) ).
cnf(c_603,negated_conjecture,
~ defn_150,
inference(resolve,[status(thm)],[c_302,c_1821]) ).
cnf(c_605,negated_conjecture,
( op(e3,e3) = e2
| ~ defn_140 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_140]) ).
cnf(c_1822,negated_conjecture,
( e4 = e2
| ~ defn_140 ),
inference(paramod,[status(thm)],[c_307,c_605]) ).
cnf(c_1823,negated_conjecture,
( e2 = e4
| ~ defn_140 ),
inference(copy,[status(thm)],[c_1822]) ).
cnf(c_606,negated_conjecture,
~ defn_140,
inference(resolve,[status(thm)],[c_300,c_1823]) ).
cnf(c_610,negated_conjecture,
( op(e2,e2) = e1
| ~ defn_130 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_130]) ).
cnf(c_1824,negated_conjecture,
( e3 = e1
| ~ defn_130 ),
inference(paramod,[status(thm)],[c_305,c_610]) ).
cnf(c_1825,negated_conjecture,
( e1 = e3
| ~ defn_130 ),
inference(copy,[status(thm)],[c_1824]) ).
cnf(c_611,negated_conjecture,
~ defn_130,
inference(resolve,[status(thm)],[c_294,c_1825]) ).
cnf(c_614,negated_conjecture,
( op(e2,e2) = e0
| ~ defn_120 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_120]) ).
cnf(c_1826,negated_conjecture,
( e3 = e0
| ~ defn_120 ),
inference(paramod,[status(thm)],[c_305,c_614]) ).
cnf(c_1827,negated_conjecture,
( e0 = e3
| ~ defn_120 ),
inference(copy,[status(thm)],[c_1826]) ).
cnf(c_615,negated_conjecture,
~ defn_120,
inference(resolve,[status(thm)],[c_288,c_1827]) ).
cnf(c_618,negated_conjecture,
( op(e1,e1) = e4
| ~ defn_110 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_110]) ).
cnf(c_620,negated_conjecture,
( op(e3,e3) = e1
| ~ defn_100 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_100]) ).
cnf(c_1828,negated_conjecture,
( e4 = e1
| ~ defn_100 ),
inference(paramod,[status(thm)],[c_307,c_620]) ).
cnf(c_1829,negated_conjecture,
( e1 = e4
| ~ defn_100 ),
inference(copy,[status(thm)],[c_1828]) ).
cnf(c_621,negated_conjecture,
~ defn_100,
inference(resolve,[status(thm)],[c_296,c_1829]) ).
cnf(c_623,negated_conjecture,
( op(e2,e2) = e1
| ~ defn_90 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_90]) ).
cnf(c_1830,negated_conjecture,
( e3 = e1
| ~ defn_90 ),
inference(paramod,[status(thm)],[c_305,c_623]) ).
cnf(c_1831,negated_conjecture,
( e1 = e3
| ~ defn_90 ),
inference(copy,[status(thm)],[c_1830]) ).
cnf(c_624,negated_conjecture,
~ defn_90,
inference(resolve,[status(thm)],[c_294,c_1831]) ).
cnf(c_626,negated_conjecture,
( op(e0,e0) = e1
| ~ defn_80 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_80]) ).
cnf(c_630,negated_conjecture,
( op(e0,e0) = e4
| ~ defn_70 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_70]) ).
cnf(c_632,negated_conjecture,
( op(e3,e3) = e0
| ~ defn_60 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_60]) ).
cnf(c_1832,negated_conjecture,
( e4 = e0
| ~ defn_60 ),
inference(paramod,[status(thm)],[c_307,c_632]) ).
cnf(c_1833,negated_conjecture,
( e0 = e4
| ~ defn_60 ),
inference(copy,[status(thm)],[c_1832]) ).
cnf(c_633,negated_conjecture,
~ defn_60,
inference(resolve,[status(thm)],[c_290,c_1833]) ).
cnf(c_635,negated_conjecture,
( op(e2,e2) = e0
| ~ defn_50 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_50]) ).
cnf(c_1834,negated_conjecture,
( e3 = e0
| ~ defn_50 ),
inference(paramod,[status(thm)],[c_305,c_635]) ).
cnf(c_1835,negated_conjecture,
( e0 = e3
| ~ defn_50 ),
inference(copy,[status(thm)],[c_1834]) ).
cnf(c_636,negated_conjecture,
~ defn_50,
inference(resolve,[status(thm)],[c_288,c_1835]) ).
cnf(c_639,negated_conjecture,
( op(e0,e0) = e1
| ~ defn_40 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_40]) ).
cnf(c_1836,plain,
op(op(e3,e2),op(op(e2,e2),e2)) = e0,
inference(paramod,[status(thm)],[c_305,c_303]) ).
cnf(c_816,plain,
op(op(e3,e2),op(e3,e2)) = e0,
inference(paramod,[status(thm)],[c_305,c_1836]) ).
cnf(c_817,plain,
op(e3,e2) = e1,
inference(paramod,[status(thm)],[c_305,c_304]) ).
cnf(c_820,plain,
op(e2,e1) != e3,
inference(paramod,[status(thm)],[c_305,c_235]) ).
cnf(c_1837,plain,
( op(e3,e4) = e0
| op(e3,e3) = e0
| e1 = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(paramod,[status(thm)],[c_817,c_74]) ).
cnf(c_1838,plain,
( op(e3,e4) = e0
| e4 = e0
| e1 = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(paramod,[status(thm)],[c_307,c_1837]) ).
cnf(c_1839,plain,
( op(e3,e4) = e0
| e0 = e4
| e1 = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(copy,[status(thm)],[c_1838]) ).
cnf(c_1840,plain,
( op(e3,e4) = e0
| e0 = e4
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(resolve,[status(thm)],[c_284,c_1839]) ).
cnf(c_845,plain,
( op(e3,e4) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(resolve,[status(thm)],[c_290,c_1840]) ).
cnf(c_1841,negated_conjecture,
( op(e1,e1) = e4
| op(e0,e0) = e4
| op(e4,e4) = e3
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_40 ),
inference(resolve,[status(thm)],[c_636,c_399]) ).
cnf(c_1842,negated_conjecture,
( op(e1,e1) = e4
| op(e0,e0) = e4
| op(e4,e4) = e3
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_40 ),
inference(resolve,[status(thm)],[c_633,c_1841]) ).
cnf(c_1843,negated_conjecture,
( op(e1,e1) = e4
| op(e0,e0) = e4
| op(e4,e4) = e3
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_80
| defn_70
| defn_40 ),
inference(resolve,[status(thm)],[c_624,c_1842]) ).
cnf(c_1844,negated_conjecture,
( op(e1,e1) = e4
| op(e0,e0) = e4
| op(e4,e4) = e3
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_80
| defn_70
| defn_40 ),
inference(resolve,[status(thm)],[c_621,c_1843]) ).
cnf(c_1845,negated_conjecture,
( op(e1,e1) = e4
| op(e0,e0) = e4
| op(e4,e4) = e3
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_110
| defn_80
| defn_70
| defn_40 ),
inference(resolve,[status(thm)],[c_615,c_1844]) ).
cnf(c_1846,negated_conjecture,
( op(e1,e1) = e4
| op(e0,e0) = e4
| op(e4,e4) = e3
| defn_170
| defn_160
| defn_150
| defn_140
| defn_110
| defn_80
| defn_70
| defn_40 ),
inference(resolve,[status(thm)],[c_611,c_1845]) ).
cnf(c_1847,negated_conjecture,
( op(e1,e1) = e4
| op(e0,e0) = e4
| op(e4,e4) = e3
| defn_170
| defn_160
| defn_150
| defn_110
| defn_80
| defn_70
| defn_40 ),
inference(resolve,[status(thm)],[c_606,c_1846]) ).
cnf(c_1848,negated_conjecture,
( op(e1,e1) = e4
| op(e0,e0) = e4
| op(e4,e4) = e3
| defn_170
| defn_160
| defn_110
| defn_80
| defn_70
| defn_40 ),
inference(resolve,[status(thm)],[c_603,c_1847]) ).
cnf(c_1849,negated_conjecture,
( op(e1,e1) = e4
| op(e0,e0) = e4
| op(e4,e4) = e3
| defn_170
| defn_110
| defn_80
| defn_70
| defn_40 ),
inference(resolve,[status(thm)],[c_599,c_1848]) ).
cnf(c_850,negated_conjecture,
( op(e1,e1) = e4
| op(e0,e0) = e4
| op(e4,e4) = e3
| defn_110
| defn_80
| defn_70
| defn_40 ),
inference(resolve,[status(thm)],[c_595,c_1849]) ).
cnf(c_1850,plain,
op(e1,op(e3,e2)) = e0,
inference(paramod,[status(thm)],[c_817,c_816]) ).
cnf(c_855,plain,
op(e1,e1) = e0,
inference(paramod,[status(thm)],[c_817,c_1850]) ).
cnf(c_861,plain,
op(e3,e1) != e1,
inference(paramod,[status(thm)],[c_817,c_254]) ).
cnf(c_864,plain,
op(e1,e2) != e1,
inference(paramod,[status(thm)],[c_817,c_142]) ).
cnf(c_1851,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| e0 = e3
| op(e0,e1) = e3 ),
inference(paramod,[status(thm)],[c_855,c_61]) ).
cnf(c_1852,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| op(e0,e1) = e3 ),
inference(resolve,[status(thm)],[c_288,c_1851]) ).
cnf(c_870,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e0,e1) = e3 ),
inference(resolve,[status(thm)],[c_820,c_1852]) ).
cnf(c_1853,negated_conjecture,
( e0 = e4
| op(e0,e0) = e4
| op(e4,e4) = e3
| defn_110
| defn_80
| defn_70
| defn_40 ),
inference(paramod,[status(thm)],[c_855,c_850]) ).
cnf(c_902,negated_conjecture,
( op(e0,e0) = e4
| op(e4,e4) = e3
| defn_110
| defn_80
| defn_70
| defn_40 ),
inference(resolve,[status(thm)],[c_290,c_1853]) ).
cnf(c_1854,negated_conjecture,
( e0 = e4
| ~ defn_110 ),
inference(paramod,[status(thm)],[c_855,c_618]) ).
cnf(c_908,negated_conjecture,
~ defn_110,
inference(resolve,[status(thm)],[c_290,c_1854]) ).
cnf(c_1855,plain,
e0 != op(e1,e0),
inference(paramod,[status(thm)],[c_855,c_208]) ).
cnf(c_912,plain,
op(e1,e0) != e0,
inference(copy,[status(thm)],[c_1855]) ).
cnf(c_1856,plain,
e0 != op(e4,e1),
inference(paramod,[status(thm)],[c_855,c_125]) ).
cnf(c_913,plain,
op(e4,e1) != e0,
inference(copy,[status(thm)],[c_1856]) ).
cnf(c_1857,plain,
e0 != op(e3,e1),
inference(paramod,[status(thm)],[c_855,c_123]) ).
cnf(c_914,plain,
op(e3,e1) != e0,
inference(copy,[status(thm)],[c_1857]) ).
cnf(c_928,negated_conjecture,
( op(e0,e0) = e4
| op(e4,e4) = e3
| defn_80
| defn_70
| defn_40 ),
inference(resolve,[status(thm)],[c_908,c_902]) ).
cnf(c_942,plain,
( op(e4,e4) = e0
| op(e4,e3) = e0
| op(e4,e2) = e0
| op(e4,e0) = e0 ),
inference(resolve,[status(thm)],[c_913,c_84]) ).
cnf(c_945,plain,
( op(e3,e4) = e0
| op(e3,e0) = e0 ),
inference(resolve,[status(thm)],[c_914,c_845]) ).
cnf(c_1858,plain,
( op(e1,e0) = e0
| unit = e4
| unit = e3
| unit = e2
| unit = e0 ),
inference(paramod,[status(thm)],[c_43,c_33]) ).
cnf(c_952,plain,
( unit = e4
| unit = e3
| unit = e2
| unit = e0 ),
inference(resolve,[status(thm)],[c_912,c_1858]) ).
cnf(c_1191,plain,
( op(e0,e0) = e1
| op(e0,e0) = e4
| op(e4,e4) = e3
| defn_70
| defn_40 ),
inference(resolve,[status(thm)],[c_928,c_626]) ).
cnf(c_1859,plain,
( e0 != op(e4,e0)
| op(e3,e4) = e0 ),
inference(paramod,[status(thm)],[c_945,c_112]) ).
cnf(c_1244,plain,
( op(e4,e0) != e0
| op(e3,e4) = e0 ),
inference(copy,[status(thm)],[c_1859]) ).
cnf(c_1262,plain,
( op(e0,e1) = e1
| unit = e4
| unit = e3
| unit = e2 ),
inference(paramod,[status(thm)],[c_952,c_35]) ).
cnf(c_1267,plain,
( op(e3,e0) = e3
| unit = e4
| unit = e3
| unit = e2 ),
inference(paramod,[status(thm)],[c_952,c_40]) ).
cnf(c_1268,plain,
( op(e0,e4) = e4
| unit = e4
| unit = e3
| unit = e2 ),
inference(paramod,[status(thm)],[c_952,c_41]) ).
cnf(c_1285,plain,
( op(e4,e4) = e0
| op(e4,e3) = e0
| op(e4,e2) = e0
| op(e3,e4) = e0 ),
inference(resolve,[status(thm)],[c_1244,c_942]) ).
cnf(c_1860,plain,
( e1 != op(e0,e0)
| unit = e4
| unit = e3
| unit = e2 ),
inference(paramod,[status(thm)],[c_1262,c_189]) ).
cnf(c_1363,plain,
( op(e0,e0) != e1
| unit = e4
| unit = e3
| unit = e2 ),
inference(copy,[status(thm)],[c_1860]) ).
cnf(c_1861,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| e1 = e3
| unit = e4
| unit = e3
| unit = e2 ),
inference(paramod,[status(thm)],[c_1262,c_870]) ).
cnf(c_1366,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| unit = e4
| unit = e3
| unit = e2 ),
inference(resolve,[status(thm)],[c_294,c_1861]) ).
cnf(c_1401,plain,
( op(e3,e1) != e3
| unit = e4
| unit = e3
| unit = e2 ),
inference(paramod,[status(thm)],[c_1267,c_246]) ).
cnf(c_1406,plain,
( op(e0,e0) != e4
| unit = e4
| unit = e3
| unit = e2 ),
inference(paramod,[status(thm)],[c_1268,c_195]) ).
cnf(c_1862,negated_conjecture,
( op(e0,e0) = e4
| op(e0,e0) = e1
| op(e0,e0) = e4
| op(e4,e4) = e3
| defn_40 ),
inference(resolve,[status(thm)],[c_1191,c_630]) ).
cnf(c_1509,negated_conjecture,
( op(e0,e0) = e1
| op(e0,e0) = e4
| op(e4,e4) = e3
| defn_40 ),
inference(copy,[status(thm)],[c_1862]) ).
cnf(c_1863,negated_conjecture,
( op(e0,e0) = e1
| op(e0,e0) = e1
| op(e0,e0) = e4
| op(e4,e4) = e3 ),
inference(resolve,[status(thm)],[c_1509,c_639]) ).
cnf(c_1510,negated_conjecture,
( op(e0,e0) = e1
| op(e0,e0) = e4
| op(e4,e4) = e3 ),
inference(copy,[status(thm)],[c_1863]) ).
cnf(c_1511,plain,
( unit = e4
| unit = e3
| unit = e2
| op(e0,e0) = e4
| op(e4,e4) = e3 ),
inference(resolve,[status(thm)],[c_1510,c_1363]) ).
cnf(c_1864,plain,
( unit = e4
| unit = e3
| unit = e2
| op(e4,e1) = e3
| unit = e4
| unit = e3
| unit = e2 ),
inference(resolve,[status(thm)],[c_1366,c_1401]) ).
cnf(c_1865,plain,
( unit = e4
| unit = e3
| op(e4,e1) = e3
| unit = e4
| unit = e3
| unit = e2 ),
inference(copy,[status(thm)],[c_1864]) ).
cnf(c_1866,plain,
( unit = e4
| op(e4,e1) = e3
| unit = e4
| unit = e3
| unit = e2 ),
inference(copy,[status(thm)],[c_1865]) ).
cnf(c_1731,plain,
( op(e4,e1) = e3
| unit = e4
| unit = e3
| unit = e2 ),
inference(copy,[status(thm)],[c_1866]) ).
cnf(c_1867,plain,
( e3 != op(e4,e4)
| unit = e4
| unit = e3
| unit = e2 ),
inference(paramod,[status(thm)],[c_1731,c_277]) ).
cnf(c_1733,plain,
( op(e4,e4) != e3
| unit = e4
| unit = e3
| unit = e2 ),
inference(copy,[status(thm)],[c_1867]) ).
cnf(c_1868,plain,
( unit = e4
| unit = e3
| unit = e2
| unit = e4
| unit = e3
| unit = e2
| op(e4,e4) = e3 ),
inference(resolve,[status(thm)],[c_1511,c_1406]) ).
cnf(c_1869,plain,
( unit = e4
| unit = e3
| unit = e4
| unit = e3
| unit = e2
| op(e4,e4) = e3 ),
inference(copy,[status(thm)],[c_1868]) ).
cnf(c_1870,plain,
( unit = e4
| unit = e4
| unit = e3
| unit = e2
| op(e4,e4) = e3 ),
inference(copy,[status(thm)],[c_1869]) ).
cnf(c_1772,plain,
( unit = e4
| unit = e3
| unit = e2
| op(e4,e4) = e3 ),
inference(copy,[status(thm)],[c_1870]) ).
cnf(c_1871,plain,
( unit = e4
| unit = e3
| unit = e2
| unit = e4
| unit = e3
| unit = e2 ),
inference(resolve,[status(thm)],[c_1772,c_1733]) ).
cnf(c_1872,plain,
( unit = e4
| unit = e3
| unit = e4
| unit = e3
| unit = e2 ),
inference(copy,[status(thm)],[c_1871]) ).
cnf(c_1873,plain,
( unit = e4
| unit = e4
| unit = e3
| unit = e2 ),
inference(copy,[status(thm)],[c_1872]) ).
cnf(c_1773,plain,
( unit = e4
| unit = e3
| unit = e2 ),
inference(copy,[status(thm)],[c_1873]) ).
cnf(c_1874,plain,
( op(e1,e2) = e1
| unit = e4
| unit = e3 ),
inference(paramod,[status(thm)],[c_1773,c_36]) ).
cnf(c_1777,plain,
( unit = e4
| unit = e3 ),
inference(resolve,[status(thm)],[c_864,c_1874]) ).
cnf(c_1875,plain,
( op(e3,e1) = e1
| unit = e4 ),
inference(paramod,[status(thm)],[c_1777,c_35]) ).
cnf(c_1783,plain,
unit = e4,
inference(resolve,[status(thm)],[c_861,c_1875]) ).
cnf(c_1785,plain,
op(e4,e4) = e4,
inference(paramod,[status(thm)],[c_1783,c_42]) ).
cnf(c_1786,plain,
op(e3,e4) = e3,
inference(paramod,[status(thm)],[c_1783,c_40]) ).
cnf(c_1787,plain,
op(e4,e3) = e3,
inference(paramod,[status(thm)],[c_1783,c_39]) ).
cnf(c_1789,plain,
op(e4,e2) = e2,
inference(paramod,[status(thm)],[c_1783,c_37]) ).
cnf(c_1876,plain,
( op(e4,e4) = e0
| op(e4,e3) = e0
| op(e4,e2) = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_1786,c_1285]) ).
cnf(c_1877,plain,
( op(e4,e4) = e0
| op(e4,e3) = e0
| e2 = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_1789,c_1876]) ).
cnf(c_1878,plain,
( op(e4,e4) = e0
| e3 = e0
| e2 = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_1787,c_1877]) ).
cnf(c_1879,plain,
( e4 = e0
| e3 = e0
| e2 = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_1785,c_1878]) ).
cnf(c_1880,plain,
( e4 = e0
| e3 = e0
| e2 = e0
| e0 = e3 ),
inference(copy,[status(thm)],[c_1879]) ).
cnf(c_1881,plain,
( e4 = e0
| e3 = e0
| e0 = e2
| e0 = e3 ),
inference(copy,[status(thm)],[c_1880]) ).
cnf(c_1882,plain,
( e4 = e0
| e0 = e3
| e0 = e2
| e0 = e3 ),
inference(copy,[status(thm)],[c_1881]) ).
cnf(c_1883,plain,
( e0 = e4
| e0 = e3
| e0 = e2
| e0 = e3 ),
inference(copy,[status(thm)],[c_1882]) ).
cnf(c_1884,plain,
( e0 = e4
| e0 = e2
| e0 = e3 ),
inference(copy,[status(thm)],[c_1883]) ).
cnf(c_1885,plain,
( e0 = e4
| e0 = e2 ),
inference(resolve,[status(thm)],[c_288,c_1884]) ).
cnf(c_1886,plain,
e0 = e4,
inference(resolve,[status(thm)],[c_286,c_1885]) ).
cnf(c_1811,plain,
$false,
inference(resolve,[status(thm)],[c_290,c_1886]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG058+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 21:05:02 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 23490 was started by sandbox on n010,
% 0.09/0.37 % Sat Sep 26 21:05:02 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 2.05/2.38
% 2.05/2.38 % From the command line: assign(max_seconds, 300).
% 2.14/2.80
% 2.14/2.80 % given #500 (T,wt=15): 1534 op(e4,e4) = e3 | op(e4,e4) = e0 | op(e0,e0) = e1. [resolve(1533,a,639,a),merge(d)].
% 2.14/2.80
% 2.14/2.80 % SZS status Theorem for theBenchmark
% 2.14/2.80
% 2.14/2.80 % Proof 1 at 0.30 (+ 0.09) seconds.
% 2.14/2.80 % Length of proof is 125.
% 2.14/2.80 % Level of proof is 16.
% 2.14/2.80 % Maximum clause weight is 29.000.
% 2.14/2.80 % Given clauses 577.
% 2.14/2.80
% 2.14/2.80 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------