%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG062+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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 0.15s 15.75s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 10
% Syntax : Number of formulae : 139 ( 63 unt; 4 def)
% Number of atoms : 1729 (1688 equ)
% Maximal formula atoms : 400 ( 12 avg)
% Number of connectives : 2560 ( 970 ~; 765 |; 821 &)
% ( 4 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 5 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(ax1,axiom,
( ( op(e4,e4) = e4
| op(e4,e4) = e3
| op(e4,e4) = e2
| op(e4,e4) = e1
| op(e4,e4) = e0 )
& ( op(e4,e3) = e4
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e1
| op(e4,e3) = e0 )
& ( op(e4,e2) = e4
| op(e4,e2) = e3
| op(e4,e2) = e2
| op(e4,e2) = e1
| op(e4,e2) = e0 )
& ( op(e4,e1) = e4
| op(e4,e1) = e3
| op(e4,e1) = e2
| op(e4,e1) = e1
| op(e4,e1) = e0 )
& ( op(e4,e0) = e4
| op(e4,e0) = e3
| op(e4,e0) = e2
| op(e4,e0) = e1
| op(e4,e0) = e0 )
& ( op(e3,e4) = e4
| op(e3,e4) = e3
| op(e3,e4) = e2
| op(e3,e4) = e1
| op(e3,e4) = e0 )
& ( op(e3,e3) = e4
| op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 )
& ( op(e3,e2) = e4
| op(e3,e2) = e3
| op(e3,e2) = e2
| op(e3,e2) = e1
| op(e3,e2) = e0 )
& ( op(e3,e1) = e4
| op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e1
| op(e3,e1) = e0 )
& ( op(e3,e0) = e4
| op(e3,e0) = e3
| op(e3,e0) = e2
| op(e3,e0) = e1
| op(e3,e0) = e0 )
& ( op(e2,e4) = e4
| op(e2,e4) = e3
| op(e2,e4) = e2
| op(e2,e4) = e1
| op(e2,e4) = e0 )
& ( op(e2,e3) = e4
| op(e2,e3) = e3
| op(e2,e3) = e2
| op(e2,e3) = e1
| op(e2,e3) = e0 )
& ( op(e2,e2) = e4
| op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 )
& ( op(e2,e1) = e4
| op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 )
& ( op(e2,e0) = e4
| op(e2,e0) = e3
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 )
& ( op(e1,e4) = e4
| op(e1,e4) = e3
| op(e1,e4) = e2
| op(e1,e4) = e1
| op(e1,e4) = e0 )
& ( op(e1,e3) = e4
| op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e0 )
& ( op(e1,e2) = e4
| op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e1
| op(e1,e2) = e0 )
& ( op(e1,e1) = e4
| op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 )
& ( op(e1,e0) = e4
| op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e1
| op(e1,e0) = e0 )
& ( op(e0,e4) = e4
| op(e0,e4) = e3
| op(e0,e4) = e2
| op(e0,e4) = e1
| op(e0,e4) = e0 )
& ( op(e0,e3) = e4
| op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| op(e0,e3) = e0 )
& ( op(e0,e2) = e4
| op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 )
& ( op(e0,e1) = e4
| op(e0,e1) = e3
| op(e0,e1) = e2
| op(e0,e1) = e1
| op(e0,e1) = e0 )
& ( op(e0,e0) = e4
| op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ) ),
file('theBenchmark.p',ax1) ).
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(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(e1,e1)
& e3 = op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1)))
& e2 = op(op(e1,e1),op(e1,e1))
& e0 = op(e1,op(op(e1,e1),op(e1,e1))) ),
file('theBenchmark.p',ax6) ).
fof(co1,conjecture,
~ ( ( ( ( ( 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 ) ) )
& ( op(e4,e4) = e4
| op(e3,e3) = e4
| op(e2,e2) = e4
| op(e1,e1) = e4
| op(e0,e0) = e4 )
& ( op(e4,e4) = e3
| op(e3,e3) = e3
| op(e2,e2) = e3
| op(e1,e1) = e3
| op(e0,e0) = e3 )
& ( op(e4,e4) = e2
| op(e3,e3) = e2
| op(e2,e2) = e2
| op(e1,e1) = e2
| op(e0,e0) = e2 )
& ( op(e4,e4) = e1
| op(e3,e3) = e1
| op(e2,e2) = e1
| op(e1,e1) = e1
| op(e0,e0) = e1 )
& ( op(e4,e4) = e0
| op(e3,e3) = e0
| op(e2,e2) = e0
| op(e1,e1) = e0
| op(e0,e0) = e0 ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ~ ( ( ( ( ( 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 ) ) )
& ( op(e4,e4) = e4
| op(e3,e3) = e4
| op(e2,e2) = e4
| op(e1,e1) = e4
| op(e0,e0) = e4 )
& ( op(e4,e4) = e3
| op(e3,e3) = e3
| op(e2,e2) = e3
| op(e1,e1) = e3
| op(e0,e0) = e3 )
& ( op(e4,e4) = e2
| op(e3,e3) = e2
| op(e2,e2) = e2
| op(e1,e1) = e2
| op(e0,e0) = e2 )
& ( op(e4,e4) = e1
| op(e3,e3) = e1
| op(e2,e2) = e1
| op(e1,e1) = e1
| op(e0,e0) = e1 )
& ( op(e4,e4) = e0
| op(e3,e3) = e0
| op(e2,e2) = e0
| op(e1,e1) = e0
| op(e0,e0) = e0 ) ),
inference(assume_negation,[status(cth)],[co1]) ).
cnf(c_17,plain,
( op(e1,e4) = e4
| op(e1,e4) = e3
| op(e1,e4) = e2
| op(e1,e4) = e1
| op(e1,e4) = e0 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_30,plain,
( op(e4,e2) = e4
| op(e4,e2) = e3
| op(e4,e2) = e2
| op(e4,e2) = e1
| op(e4,e2) = e0 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_33,plain,
op(unit,e0) = e0,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_34,plain,
op(e0,unit) = e0,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_36,plain,
op(e1,unit) = e1,
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_97,plain,
op(e3,e0) != op(e0,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_124,plain,
op(e1,e2) != op(e0,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_125,plain,
op(e0,e2) != op(e1,e2),
inference(copy,[status(thm)],[c_124]) ).
cnf(c_132,plain,
op(e4,e2) != op(e1,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_133,plain,
op(e1,e2) != op(e4,e2),
inference(copy,[status(thm)],[c_132]) ).
cnf(c_135,plain,
op(e4,e2) != op(e2,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_136,plain,
op(e2,e2) != op(e4,e2),
inference(copy,[status(thm)],[c_135]) ).
cnf(c_142,plain,
op(e3,e3) != op(e0,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_162,plain,
op(e4,e4) != op(e1,e4),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_163,plain,
op(e1,e4) != op(e4,e4),
inference(copy,[status(thm)],[c_162]) ).
cnf(c_186,plain,
op(e1,e2) != op(e1,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_188,plain,
op(e1,e4) != op(e1,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_189,plain,
op(e1,e0) != op(e1,e4),
inference(copy,[status(thm)],[c_188]) ).
cnf(c_191,plain,
op(e1,e3) != op(e1,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_192,plain,
op(e1,e4) != op(e1,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_193,plain,
op(e1,e1) != op(e1,e4),
inference(copy,[status(thm)],[c_192]) ).
cnf(c_195,plain,
op(e1,e4) != op(e1,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_196,plain,
op(e1,e2) != op(e1,e4),
inference(copy,[status(thm)],[c_195]) ).
cnf(c_231,plain,
op(e4,e2) != op(e4,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_237,plain,
op(e4,e4) != op(e4,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_238,plain,
op(e4,e1) != op(e4,e4),
inference(copy,[status(thm)],[c_237]) ).
cnf(c_240,plain,
op(e4,e4) != op(e4,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_241,plain,
op(e4,e2) != op(e4,e4),
inference(copy,[status(thm)],[c_240]) ).
cnf(c_246,plain,
e2 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_247,plain,
e3 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_248,plain,
e4 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_249,plain,
e0 != e4,
inference(copy,[status(thm)],[c_248]) ).
cnf(c_255,plain,
e4 != e2,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_256,plain,
e2 != e4,
inference(copy,[status(thm)],[c_255]) ).
cnf(c_259,plain,
op(e1,op(op(e1,e1),op(e1,e1))) = e0,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_260,plain,
op(op(e1,e1),op(e1,e1)) = e2,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_261,plain,
op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1))) = e3,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_1598,plain,
op(e2,op(op(e1,e1),op(e1,e1))) = e3,
inference(paramod,[status(thm)],[c_260,c_261]) ).
cnf(c_262,plain,
op(e2,e2) = e3,
inference(paramod,[status(thm)],[c_260,c_1598]) ).
cnf(c_263,plain,
op(e1,e1) = e4,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_264,negated_conjecture,
( op(e4,e4) = e0
| op(e3,e3) = e0
| op(e2,e2) = e0
| op(e1,e1) = e0
| op(e0,e0) = e0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_1599,negated_conjecture,
( op(e4,e4) = e0
| op(e3,e3) = e0
| op(e2,e2) = e0
| e4 = e0
| op(e0,e0) = e0 ),
inference(paramod,[status(thm)],[c_263,c_264]) ).
cnf(c_1600,negated_conjecture,
( op(e4,e4) = e0
| op(e3,e3) = e0
| e3 = e0
| e4 = e0
| op(e0,e0) = e0 ),
inference(paramod,[status(thm)],[c_262,c_1599]) ).
cnf(c_1601,negated_conjecture,
( op(e4,e4) = e0
| op(e3,e3) = e0
| e3 = e0
| e0 = e4
| op(e0,e0) = e0 ),
inference(copy,[status(thm)],[c_1600]) ).
cnf(c_1602,negated_conjecture,
( op(e4,e4) = e0
| op(e3,e3) = e0
| e3 = e0
| op(e0,e0) = e0 ),
inference(resolve,[status(thm)],[c_249,c_1601]) ).
cnf(c_265,negated_conjecture,
( op(e4,e4) = e0
| op(e3,e3) = e0
| op(e0,e0) = e0 ),
inference(resolve,[status(thm)],[c_247,c_1602]) ).
fof(def_defn_00,definition,
( defn_00
<=> ( ( unit != e0
| op(e4,e4) != e0 )
& ( op(e4,e0) = e4
| op(e4,e4) != e0 )
& ( unit != e0
| op(e4,e3) != e0 )
& ( op(e4,e0) = e3
| op(e4,e3) != e0 )
& ( unit != e0
| op(e4,e2) != e0 )
& ( op(e4,e0) = e2
| op(e4,e2) != e0 )
& ( unit != e0
| op(e4,e1) != e0 )
& ( op(e4,e0) = e1
| op(e4,e1) != e0 )
& ( unit != e0
| op(e4,e0) != e0 )
& ( unit != e0
| op(e3,e4) != e0 )
& ( op(e3,e0) = e4
| op(e3,e4) != e0 )
& ( unit != e0
| op(e3,e3) != e0 )
& ( op(e3,e0) = e3
| op(e3,e3) != e0 )
& ( unit != e0
| op(e3,e2) != e0 )
& ( op(e3,e0) = e2
| op(e3,e2) != e0 )
& ( unit != e0
| op(e3,e1) != e0 )
& ( op(e3,e0) = e1
| op(e3,e1) != e0 )
& ( unit != e0
| op(e3,e0) != e0 )
& ( unit != e0
| op(e2,e4) != e0 )
& ( op(e2,e0) = e4
| op(e2,e4) != e0 )
& ( unit != e0
| op(e2,e3) != e0 )
& ( op(e2,e0) = e3
| op(e2,e3) != e0 )
& ( unit != e0
| op(e2,e2) != e0 )
& ( op(e2,e0) = e2
| op(e2,e2) != e0 )
& ( unit != e0
| op(e2,e1) != e0 )
& ( op(e2,e0) = e1
| op(e2,e1) != e0 )
& ( unit != e0
| op(e2,e0) != e0 )
& ( unit != e0
| op(e1,e4) != e0 )
& ( op(e1,e0) = e4
| op(e1,e4) != e0 )
& ( unit != e0
| op(e1,e3) != e0 )
& ( op(e1,e0) = e3
| op(e1,e3) != e0 )
& ( unit != e0
| op(e1,e2) != e0 )
& ( op(e1,e0) = e2
| op(e1,e2) != e0 )
& ( unit != e0
| op(e1,e1) != e0 )
& ( op(e1,e0) = e1
| op(e1,e1) != e0 )
& ( unit != e0
| op(e1,e0) != e0 )
& ( unit != e0
| op(e0,e4) != e0 )
& ( op(e0,e0) = e4
| op(e0,e4) != e0 )
& ( unit != e0
| op(e0,e3) != e0 )
& ( op(e0,e0) = e3
| op(e0,e3) != e0 )
& ( unit != e0
| op(e0,e2) != e0 )
& ( op(e0,e0) = e2
| op(e0,e2) != e0 )
& ( unit != e0
| op(e0,e1) != e0 )
& ( op(e0,e0) = e1
| op(e0,e1) != e0 )
& ( unit != e0
| op(e0,e0) != e0 ) ) ),
introduced(definition,[new_symbols(definition,[defn_00])],[]) ).
fof(def_defn_10,definition,
( defn_10
<=> ( ( unit != e1
| op(e4,e4) != e1 )
& ( op(e4,e1) = e4
| op(e4,e4) != e1 )
& ( unit != e1
| op(e4,e3) != e1 )
& ( op(e4,e1) = e3
| op(e4,e3) != e1 )
& ( unit != e1
| op(e4,e2) != e1 )
& ( op(e4,e1) = e2
| op(e4,e2) != e1 )
& ( unit != e1
| op(e4,e1) != e1 )
& ( unit != e1
| op(e4,e0) != e1 )
& ( op(e4,e1) = e0
| op(e4,e0) != e1 )
& ( unit != e1
| op(e3,e4) != e1 )
& ( op(e3,e1) = e4
| op(e3,e4) != e1 )
& ( unit != e1
| op(e3,e3) != e1 )
& ( op(e3,e1) = e3
| op(e3,e3) != e1 )
& ( unit != e1
| op(e3,e2) != e1 )
& ( op(e3,e1) = e2
| op(e3,e2) != e1 )
& ( unit != e1
| op(e3,e1) != e1 )
& ( unit != e1
| op(e3,e0) != e1 )
& ( op(e3,e1) = e0
| op(e3,e0) != e1 )
& ( unit != e1
| op(e2,e4) != e1 )
& ( op(e2,e1) = e4
| op(e2,e4) != e1 )
& ( unit != e1
| op(e2,e3) != e1 )
& ( op(e2,e1) = e3
| op(e2,e3) != e1 )
& ( unit != e1
| op(e2,e2) != e1 )
& ( op(e2,e1) = e2
| op(e2,e2) != e1 )
& ( unit != e1
| op(e2,e1) != e1 )
& ( unit != e1
| op(e2,e0) != e1 )
& ( op(e2,e1) = e0
| op(e2,e0) != e1 )
& ( unit != e1
| op(e1,e4) != e1 )
& ( op(e1,e1) = e4
| op(e1,e4) != e1 )
& ( unit != e1
| op(e1,e3) != e1 )
& ( op(e1,e1) = e3
| op(e1,e3) != e1 )
& ( unit != e1
| op(e1,e2) != e1 )
& ( op(e1,e1) = e2
| op(e1,e2) != e1 )
& ( unit != e1
| op(e1,e1) != e1 )
& ( unit != e1
| op(e1,e0) != e1 )
& ( op(e1,e1) = e0
| op(e1,e0) != e1 )
& ( unit != e1
| op(e0,e4) != e1 )
& ( op(e0,e1) = e4
| op(e0,e4) != e1 )
& ( unit != e1
| op(e0,e3) != e1 )
& ( op(e0,e1) = e3
| op(e0,e3) != e1 )
& ( unit != e1
| op(e0,e2) != e1 )
& ( op(e0,e1) = e2
| op(e0,e2) != e1 )
& ( unit != e1
| op(e0,e1) != e1 )
& ( unit != e1
| op(e0,e0) != e1 )
& ( op(e0,e1) = e0
| op(e0,e0) != e1 ) ) ),
introduced(definition,[new_symbols(definition,[defn_10])],[]) ).
fof(def_defn_20,definition,
( defn_20
<=> ( ( unit != e2
| op(e4,e4) != e2 )
& ( op(e4,e2) = e4
| op(e4,e4) != e2 )
& ( unit != e2
| op(e4,e3) != e2 )
& ( op(e4,e2) = e3
| op(e4,e3) != e2 )
& ( unit != e2
| op(e4,e2) != e2 )
& ( unit != e2
| op(e4,e1) != e2 )
& ( op(e4,e2) = e1
| op(e4,e1) != e2 )
& ( unit != e2
| op(e4,e0) != e2 )
& ( op(e4,e2) = e0
| op(e4,e0) != e2 )
& ( unit != e2
| op(e3,e4) != e2 )
& ( op(e3,e2) = e4
| op(e3,e4) != e2 )
& ( unit != e2
| op(e3,e3) != e2 )
& ( op(e3,e2) = e3
| op(e3,e3) != e2 )
& ( unit != e2
| op(e3,e2) != e2 )
& ( unit != e2
| op(e3,e1) != e2 )
& ( op(e3,e2) = e1
| op(e3,e1) != e2 )
& ( unit != e2
| op(e3,e0) != e2 )
& ( op(e3,e2) = e0
| op(e3,e0) != e2 )
& ( unit != e2
| op(e2,e4) != e2 )
& ( op(e2,e2) = e4
| op(e2,e4) != e2 )
& ( unit != e2
| op(e2,e3) != e2 )
& ( op(e2,e2) = e3
| op(e2,e3) != e2 )
& ( unit != e2
| op(e2,e2) != e2 )
& ( unit != e2
| op(e2,e1) != e2 )
& ( op(e2,e2) = e1
| op(e2,e1) != e2 )
& ( unit != e2
| op(e2,e0) != e2 )
& ( op(e2,e2) = e0
| op(e2,e0) != e2 )
& ( unit != e2
| op(e1,e4) != e2 )
& ( op(e1,e2) = e4
| op(e1,e4) != e2 )
& ( unit != e2
| op(e1,e3) != e2 )
& ( op(e1,e2) = e3
| op(e1,e3) != e2 )
& ( unit != e2
| op(e1,e2) != e2 )
& ( unit != e2
| op(e1,e1) != e2 )
& ( op(e1,e2) = e1
| op(e1,e1) != e2 )
& ( unit != e2
| op(e1,e0) != e2 )
& ( op(e1,e2) = e0
| op(e1,e0) != e2 )
& ( unit != e2
| op(e0,e4) != e2 )
& ( op(e0,e2) = e4
| op(e0,e4) != e2 )
& ( unit != e2
| op(e0,e3) != e2 )
& ( op(e0,e2) = e3
| op(e0,e3) != e2 )
& ( unit != e2
| op(e0,e2) != e2 )
& ( unit != e2
| op(e0,e1) != e2 )
& ( op(e0,e2) = e1
| op(e0,e1) != e2 )
& ( unit != e2
| op(e0,e0) != e2 )
& ( op(e0,e2) = e0
| op(e0,e0) != e2 ) ) ),
introduced(definition,[new_symbols(definition,[defn_20])],[]) ).
fof(def_defn_30,definition,
( defn_30
<=> ( ( unit != e3
| op(e4,e4) != e3 )
& ( op(e4,e3) = e4
| op(e4,e4) != e3 )
& ( unit != e3
| op(e4,e3) != e3 )
& ( unit != e3
| op(e4,e2) != e3 )
& ( op(e4,e3) = e2
| op(e4,e2) != e3 )
& ( unit != e3
| op(e4,e1) != e3 )
& ( op(e4,e3) = e1
| op(e4,e1) != e3 )
& ( unit != e3
| op(e4,e0) != e3 )
& ( op(e4,e3) = e0
| op(e4,e0) != e3 )
& ( unit != e3
| op(e3,e4) != e3 )
& ( op(e3,e3) = e4
| op(e3,e4) != e3 )
& ( unit != e3
| op(e3,e3) != e3 )
& ( unit != e3
| op(e3,e2) != e3 )
& ( op(e3,e3) = e2
| op(e3,e2) != e3 )
& ( unit != e3
| op(e3,e1) != e3 )
& ( op(e3,e3) = e1
| op(e3,e1) != e3 )
& ( unit != e3
| op(e3,e0) != e3 )
& ( op(e3,e3) = e0
| op(e3,e0) != e3 )
& ( unit != e3
| op(e2,e4) != e3 )
& ( op(e2,e3) = e4
| op(e2,e4) != e3 )
& ( unit != e3
| op(e2,e3) != e3 )
& ( unit != e3
| op(e2,e2) != e3 )
& ( op(e2,e3) = e2
| op(e2,e2) != e3 )
& ( unit != e3
| op(e2,e1) != e3 )
& ( op(e2,e3) = e1
| op(e2,e1) != e3 )
& ( unit != e3
| op(e2,e0) != e3 )
& ( op(e2,e3) = e0
| op(e2,e0) != e3 )
& ( unit != e3
| op(e1,e4) != e3 )
& ( op(e1,e3) = e4
| op(e1,e4) != e3 )
& ( unit != e3
| op(e1,e3) != e3 )
& ( unit != e3
| op(e1,e2) != e3 )
& ( op(e1,e3) = e2
| op(e1,e2) != e3 )
& ( unit != e3
| op(e1,e1) != e3 )
& ( op(e1,e3) = e1
| op(e1,e1) != e3 )
& ( unit != e3
| op(e1,e0) != e3 )
& ( op(e1,e3) = e0
| op(e1,e0) != e3 )
& ( unit != e3
| op(e0,e4) != e3 )
& ( op(e0,e3) = e4
| op(e0,e4) != e3 )
& ( unit != e3
| op(e0,e3) != e3 )
& ( unit != e3
| op(e0,e2) != e3 )
& ( op(e0,e3) = e2
| op(e0,e2) != e3 )
& ( unit != e3
| op(e0,e1) != e3 )
& ( op(e0,e3) = e1
| op(e0,e1) != e3 )
& ( unit != e3
| op(e0,e0) != e3 )
& ( op(e0,e3) = e0
| op(e0,e0) != e3 ) ) ),
introduced(definition,[new_symbols(definition,[defn_30])],[]) ).
cnf(c_283,negated_conjecture,
( op(e1,e4) = e1
| op(e1,e1) != e4
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_00,def_defn_10,def_defn_20,def_defn_30]) ).
cnf(c_1603,negated_conjecture,
( op(e1,e4) = e1
| e4 != e4
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_263,c_283]) ).
cnf(c_284,negated_conjecture,
( op(e1,e4) = e1
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(copy,[status(thm)],[c_1603]) ).
cnf(c_329,negated_conjecture,
( op(e1,e3) = e4
| op(e1,e4) != e3
| ~ defn_30 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_30]) ).
cnf(c_339,negated_conjecture,
( op(e4,e2) = e4
| op(e4,e4) != e2
| ~ defn_20 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_20]) ).
cnf(c_391,negated_conjecture,
( op(e4,e1) = e2
| op(e4,e2) != e1
| ~ defn_10 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_10]) ).
cnf(c_465,negated_conjecture,
( unit != e0
| op(e1,e2) != e0
| ~ defn_00 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_00]) ).
cnf(c_1604,plain,
op(e1,op(e4,op(e1,e1))) = e0,
inference(paramod,[status(thm)],[c_263,c_259]) ).
cnf(c_479,plain,
op(e1,op(e4,e4)) = e0,
inference(paramod,[status(thm)],[c_263,c_1604]) ).
cnf(c_1605,plain,
e3 != op(e4,e2),
inference(paramod,[status(thm)],[c_262,c_136]) ).
cnf(c_484,plain,
op(e4,e2) != e3,
inference(copy,[status(thm)],[c_1605]) ).
cnf(c_1606,plain,
op(e4,op(e1,e1)) = e2,
inference(paramod,[status(thm)],[c_263,c_260]) ).
cnf(c_496,plain,
op(e4,e4) = e2,
inference(paramod,[status(thm)],[c_263,c_1606]) ).
cnf(c_1607,plain,
e4 != op(e1,e4),
inference(paramod,[status(thm)],[c_263,c_193]) ).
cnf(c_497,plain,
op(e1,e4) != e4,
inference(copy,[status(thm)],[c_1607]) ).
cnf(c_498,plain,
op(e1,e3) != e4,
inference(paramod,[status(thm)],[c_263,c_191]) ).
cnf(c_525,plain,
( op(e4,e2) = e4
| op(e4,e2) = e2
| op(e4,e2) = e1
| op(e4,e2) = e0 ),
inference(resolve,[status(thm)],[c_484,c_30]) ).
cnf(c_534,plain,
op(e1,e2) = e0,
inference(paramod,[status(thm)],[c_496,c_479]) ).
cnf(c_1608,negated_conjecture,
( op(e4,e2) = e4
| e2 != e2
| ~ defn_20 ),
inference(paramod,[status(thm)],[c_496,c_339]) ).
cnf(c_535,negated_conjecture,
( op(e4,e2) = e4
| ~ defn_20 ),
inference(copy,[status(thm)],[c_1608]) ).
cnf(c_1609,negated_conjecture,
( e2 = e0
| op(e3,e3) = e0
| op(e0,e0) = e0 ),
inference(paramod,[status(thm)],[c_496,c_265]) ).
cnf(c_540,negated_conjecture,
( op(e3,e3) = e0
| op(e0,e0) = e0 ),
inference(resolve,[status(thm)],[c_246,c_1609]) ).
cnf(c_542,plain,
op(e4,e2) != e2,
inference(paramod,[status(thm)],[c_496,c_241]) ).
cnf(c_543,plain,
op(e4,e1) != e2,
inference(paramod,[status(thm)],[c_496,c_238]) ).
cnf(c_547,plain,
op(e1,e4) != e2,
inference(paramod,[status(thm)],[c_496,c_163]) ).
cnf(c_1610,plain,
( op(e1,e4) = e4
| op(e1,e4) = e3
| op(e1,e4) = e1
| op(e1,e4) = e0 ),
inference(resolve,[status(thm)],[c_547,c_17]) ).
cnf(c_555,plain,
( op(e1,e4) = e3
| op(e1,e4) = e1
| op(e1,e4) = e0 ),
inference(resolve,[status(thm)],[c_497,c_1610]) ).
cnf(c_556,negated_conjecture,
( op(e1,e4) != e3
| ~ defn_30 ),
inference(resolve,[status(thm)],[c_498,c_329]) ).
cnf(c_1611,negated_conjecture,
( unit != e0
| e0 != e0
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_534,c_465]) ).
cnf(c_577,negated_conjecture,
( unit != e0
| ~ defn_00 ),
inference(copy,[status(thm)],[c_1611]) ).
cnf(c_1612,plain,
e0 != op(e1,e4),
inference(paramod,[status(thm)],[c_534,c_196]) ).
cnf(c_578,plain,
op(e1,e4) != e0,
inference(copy,[status(thm)],[c_1612]) ).
cnf(c_1613,plain,
e0 != op(e1,e0),
inference(paramod,[status(thm)],[c_534,c_186]) ).
cnf(c_580,plain,
op(e1,e0) != e0,
inference(copy,[status(thm)],[c_1613]) ).
cnf(c_1614,plain,
e0 != op(e4,e2),
inference(paramod,[status(thm)],[c_534,c_133]) ).
cnf(c_581,plain,
op(e4,e2) != e0,
inference(copy,[status(thm)],[c_1614]) ).
cnf(c_583,plain,
op(e0,e2) != e0,
inference(paramod,[status(thm)],[c_534,c_125]) ).
cnf(c_1615,plain,
( op(e4,e2) = e4
| op(e4,e2) = e2
| op(e4,e2) = e1 ),
inference(resolve,[status(thm)],[c_581,c_525]) ).
cnf(c_586,plain,
( op(e4,e2) = e4
| op(e4,e2) = e1 ),
inference(resolve,[status(thm)],[c_542,c_1615]) ).
cnf(c_588,negated_conjecture,
( op(e4,e2) != e1
| ~ defn_10 ),
inference(resolve,[status(thm)],[c_543,c_391]) ).
cnf(c_599,plain,
( op(e1,e4) = e3
| op(e1,e4) = e1 ),
inference(resolve,[status(thm)],[c_578,c_555]) ).
cnf(c_613,plain,
( op(e3,e0) = e0
| unit = e4
| unit = e2
| unit = e1
| unit = e0 ),
inference(paramod,[status(thm)],[c_43,c_33]) ).
cnf(c_614,plain,
( op(e0,e3) = e0
| unit = e4
| unit = e2
| unit = e1
| unit = e0 ),
inference(paramod,[status(thm)],[c_43,c_34]) ).
cnf(c_1616,plain,
( e0 != op(e0,e3)
| op(e0,e0) = e0 ),
inference(paramod,[status(thm)],[c_540,c_142]) ).
cnf(c_746,plain,
( op(e0,e3) != e0
| op(e0,e0) = e0 ),
inference(copy,[status(thm)],[c_1616]) ).
cnf(c_774,plain,
( op(e1,e4) = e1
| defn_20
| defn_10
| defn_00
| op(e1,e4) != e3 ),
inference(resolve,[status(thm)],[c_556,c_284]) ).
cnf(c_1617,plain,
( e0 != op(e0,e0)
| unit = e4
| unit = e2
| unit = e1
| unit = e0 ),
inference(paramod,[status(thm)],[c_613,c_97]) ).
cnf(c_990,plain,
( op(e0,e0) != e0
| unit = e4
| unit = e2
| unit = e1
| unit = e0 ),
inference(copy,[status(thm)],[c_1617]) ).
cnf(c_1025,plain,
( unit = e4
| unit = e2
| unit = e1
| unit = e0
| op(e0,e0) = e0 ),
inference(resolve,[status(thm)],[c_746,c_614]) ).
cnf(c_1618,plain,
( op(e1,e4) = e1
| op(e1,e4) = e1
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_774,c_599]) ).
cnf(c_1102,plain,
( op(e1,e4) = e1
| defn_20
| defn_10
| defn_00 ),
inference(copy,[status(thm)],[c_1618]) ).
cnf(c_1106,plain,
( op(e4,e2) = e4
| op(e1,e4) = e1
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_1102,c_535]) ).
cnf(c_1116,plain,
( op(e4,e2) != e1
| op(e4,e2) = e4
| op(e1,e4) = e1
| defn_00 ),
inference(resolve,[status(thm)],[c_1106,c_588]) ).
cnf(c_1619,plain,
( op(e4,e2) = e4
| op(e4,e2) = e4
| op(e1,e4) = e1
| defn_00 ),
inference(resolve,[status(thm)],[c_1116,c_586]) ).
cnf(c_1406,plain,
( op(e4,e2) = e4
| op(e1,e4) = e1
| defn_00 ),
inference(copy,[status(thm)],[c_1619]) ).
cnf(c_1407,plain,
( unit != e0
| op(e4,e2) = e4
| op(e1,e4) = e1 ),
inference(resolve,[status(thm)],[c_1406,c_577]) ).
cnf(c_1620,plain,
( unit = e4
| unit = e2
| unit = e1
| unit = e0
| unit = e4
| unit = e2
| unit = e1
| unit = e0 ),
inference(resolve,[status(thm)],[c_1025,c_990]) ).
cnf(c_1621,plain,
( unit = e4
| unit = e2
| unit = e1
| unit = e4
| unit = e2
| unit = e1
| unit = e0 ),
inference(copy,[status(thm)],[c_1620]) ).
cnf(c_1622,plain,
( unit = e4
| unit = e2
| unit = e4
| unit = e2
| unit = e1
| unit = e0 ),
inference(copy,[status(thm)],[c_1621]) ).
cnf(c_1623,plain,
( unit = e4
| unit = e4
| unit = e2
| unit = e1
| unit = e0 ),
inference(copy,[status(thm)],[c_1622]) ).
cnf(c_1480,plain,
( unit = e4
| unit = e2
| unit = e1
| unit = e0 ),
inference(copy,[status(thm)],[c_1623]) ).
cnf(c_1624,plain,
( op(e0,e2) = e0
| unit = e4
| unit = e1
| unit = e0 ),
inference(paramod,[status(thm)],[c_1480,c_34]) ).
cnf(c_1483,plain,
( unit = e4
| unit = e1
| unit = e0 ),
inference(resolve,[status(thm)],[c_583,c_1624]) ).
cnf(c_1484,plain,
( op(e4,e2) = e4
| op(e1,e4) = e1
| unit = e4
| unit = e1 ),
inference(resolve,[status(thm)],[c_1483,c_1407]) ).
cnf(c_1487,plain,
( op(e1,e0) = e1
| unit = e4
| unit = e1 ),
inference(paramod,[status(thm)],[c_1483,c_36]) ).
cnf(c_1493,plain,
( op(e4,e0) = e4
| unit = e4
| unit = e1 ),
inference(paramod,[status(thm)],[c_1483,c_42]) ).
cnf(c_1625,plain,
( e1 != op(e1,e4)
| unit = e4
| unit = e1 ),
inference(paramod,[status(thm)],[c_1487,c_189]) ).
cnf(c_1514,plain,
( op(e1,e4) != e1
| unit = e4
| unit = e1 ),
inference(copy,[status(thm)],[c_1625]) ).
cnf(c_1553,plain,
( op(e4,e2) != e4
| unit = e4
| unit = e1 ),
inference(paramod,[status(thm)],[c_1493,c_231]) ).
cnf(c_1626,plain,
( unit = e4
| unit = e1
| op(e4,e2) = e4
| unit = e4
| unit = e1 ),
inference(resolve,[status(thm)],[c_1484,c_1514]) ).
cnf(c_1627,plain,
( unit = e4
| op(e4,e2) = e4
| unit = e4
| unit = e1 ),
inference(copy,[status(thm)],[c_1626]) ).
cnf(c_1593,plain,
( op(e4,e2) = e4
| unit = e4
| unit = e1 ),
inference(copy,[status(thm)],[c_1627]) ).
cnf(c_1628,plain,
( unit = e4
| unit = e1
| unit = e4
| unit = e1 ),
inference(resolve,[status(thm)],[c_1593,c_1553]) ).
cnf(c_1629,plain,
( unit = e4
| unit = e4
| unit = e1 ),
inference(copy,[status(thm)],[c_1628]) ).
cnf(c_1594,plain,
( unit = e4
| unit = e1 ),
inference(copy,[status(thm)],[c_1629]) ).
cnf(c_1630,plain,
( op(e1,e0) = e0
| unit = e4 ),
inference(paramod,[status(thm)],[c_1594,c_33]) ).
cnf(c_1595,plain,
unit = e4,
inference(resolve,[status(thm)],[c_580,c_1630]) ).
cnf(c_1631,plain,
op(e4,e4) = e4,
inference(paramod,[status(thm)],[c_1595,c_42]) ).
cnf(c_1632,plain,
e2 = e4,
inference(paramod,[status(thm)],[c_496,c_1631]) ).
cnf(c_1597,plain,
$false,
inference(resolve,[status(thm)],[c_256,c_1632]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG062+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/15.40 % Computer : n006.cluster.edu
% 0.12/15.40 % Model : x86_64 x86_64
% 0.12/15.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/15.40 % Memory : 8046.5625MB
% 0.12/15.40 % OS : Linux 6.8.0-71-generic
% 0.15/15.40 % CPULimit : 300
% 0.15/15.40 % WCLimit : 300
% 0.15/15.40 % DateTime : Sat Sep 26 21:03:51 UTC 2026
% 0.15/15.40 % CPUTime :
% 0.15/15.40 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.15/15.40 % Process 2113719 was started by sandbox2 on n006,
% 0.15/15.40 % Sat Sep 26 21:03:51 2026
% 0.15/15.40 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.15/15.44
% 0.15/15.44 % From the command line: assign(max_seconds, 300).
% 0.15/15.75
% 0.15/15.75 % given #500 (T,wt=15): 1379 op(e0,e0) = e0 | op(e4,e0) = e0 | op(e0,e4) = e0. [resolve(1325,c,1038,c),merge(c)].
% 0.15/15.75
% 0.15/15.75 % SZS status Theorem for theBenchmark
% 0.15/15.75
% 0.15/15.75 % Proof 1 at 0.24 (+ 0.05) seconds.
% 0.15/15.75 % Length of proof is 99.
% 0.15/15.75 % Level of proof is 15.
% 0.15/15.75 % Maximum clause weight is 25.000.
% 0.15/15.75 % Given clauses 654.
% 0.15/15.75
% 0.15/15.75 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------