%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG055+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 : n026.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:21 AM UTC 2026
% Result : Theorem 1.73s 0.68s
% Output : CNFRefutation 1.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 10
% Syntax : Number of formulae : 131 ( 44 unt; 4 def)
% Number of atoms : 1793 (1727 equ)
% Maximal formula atoms : 425 ( 13 avg)
% Number of connectives : 2687 (1025 ~; 787 |; 871 &)
% ( 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(e2,e2)
& e3 = op(e2,op(e2,e2))
& e1 = op(op(e2,op(e2,e2)),op(e2,e2))
& e0 = op(op(e2,e2),op(e2,e2)) ),
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,op(e4,e4)) = e4
& op(e4,op(e4,e4)) != e4 )
| ( op(e4,op(e3,e4)) = e3
& op(e3,op(e3,e4)) != e4 )
| ( op(e4,op(e2,e4)) = e2
& op(e2,op(e2,e4)) != e4 )
| ( op(e4,op(e1,e4)) = e1
& op(e1,op(e1,e4)) != e4 )
| ( op(e4,op(e0,e4)) = e0
& op(e0,op(e0,e4)) != e4 ) )
& ( ( op(e3,op(e4,e3)) = e4
& op(e4,op(e4,e3)) != e3 )
| ( op(e3,op(e3,e3)) = e3
& op(e3,op(e3,e3)) != e3 )
| ( op(e3,op(e2,e3)) = e2
& op(e2,op(e2,e3)) != e3 )
| ( op(e3,op(e1,e3)) = e1
& op(e1,op(e1,e3)) != e3 )
| ( op(e3,op(e0,e3)) = e0
& op(e0,op(e0,e3)) != e3 ) )
& ( ( op(e2,op(e4,e2)) = e4
& op(e4,op(e4,e2)) != e2 )
| ( op(e2,op(e3,e2)) = e3
& op(e3,op(e3,e2)) != e2 )
| ( op(e2,op(e2,e2)) = e2
& op(e2,op(e2,e2)) != e2 )
| ( op(e2,op(e1,e2)) = e1
& op(e1,op(e1,e2)) != e2 )
| ( op(e2,op(e0,e2)) = e0
& op(e0,op(e0,e2)) != e2 ) )
& ( ( op(e1,op(e4,e1)) = e4
& op(e4,op(e4,e1)) != e1 )
| ( op(e1,op(e3,e1)) = e3
& op(e3,op(e3,e1)) != e1 )
| ( op(e1,op(e2,e1)) = e2
& op(e2,op(e2,e1)) != e1 )
| ( op(e1,op(e1,e1)) = e1
& op(e1,op(e1,e1)) != e1 )
| ( op(e1,op(e0,e1)) = e0
& op(e0,op(e0,e1)) != e1 ) )
& ( ( op(e0,op(e4,e0)) = e4
& op(e4,op(e4,e0)) != e0 )
| ( op(e0,op(e3,e0)) = e3
& op(e3,op(e3,e0)) != e0 )
| ( op(e0,op(e2,e0)) = e2
& op(e2,op(e2,e0)) != e0 )
| ( op(e0,op(e1,e0)) = e1
& op(e1,op(e1,e0)) != e0 )
| ( op(e0,op(e0,e0)) = e0
& op(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,op(e4,e4)) = e4
& op(e4,op(e4,e4)) != e4 )
| ( op(e4,op(e3,e4)) = e3
& op(e3,op(e3,e4)) != e4 )
| ( op(e4,op(e2,e4)) = e2
& op(e2,op(e2,e4)) != e4 )
| ( op(e4,op(e1,e4)) = e1
& op(e1,op(e1,e4)) != e4 )
| ( op(e4,op(e0,e4)) = e0
& op(e0,op(e0,e4)) != e4 ) )
& ( ( op(e3,op(e4,e3)) = e4
& op(e4,op(e4,e3)) != e3 )
| ( op(e3,op(e3,e3)) = e3
& op(e3,op(e3,e3)) != e3 )
| ( op(e3,op(e2,e3)) = e2
& op(e2,op(e2,e3)) != e3 )
| ( op(e3,op(e1,e3)) = e1
& op(e1,op(e1,e3)) != e3 )
| ( op(e3,op(e0,e3)) = e0
& op(e0,op(e0,e3)) != e3 ) )
& ( ( op(e2,op(e4,e2)) = e4
& op(e4,op(e4,e2)) != e2 )
| ( op(e2,op(e3,e2)) = e3
& op(e3,op(e3,e2)) != e2 )
| ( op(e2,op(e2,e2)) = e2
& op(e2,op(e2,e2)) != e2 )
| ( op(e2,op(e1,e2)) = e1
& op(e1,op(e1,e2)) != e2 )
| ( op(e2,op(e0,e2)) = e0
& op(e0,op(e0,e2)) != e2 ) )
& ( ( op(e1,op(e4,e1)) = e4
& op(e4,op(e4,e1)) != e1 )
| ( op(e1,op(e3,e1)) = e3
& op(e3,op(e3,e1)) != e1 )
| ( op(e1,op(e2,e1)) = e2
& op(e2,op(e2,e1)) != e1 )
| ( op(e1,op(e1,e1)) = e1
& op(e1,op(e1,e1)) != e1 )
| ( op(e1,op(e0,e1)) = e0
& op(e0,op(e0,e1)) != e1 ) )
& ( ( op(e0,op(e4,e0)) = e4
& op(e4,op(e4,e0)) != e0 )
| ( op(e0,op(e3,e0)) = e3
& op(e3,op(e3,e0)) != e0 )
| ( op(e0,op(e2,e0)) = e2
& op(e2,op(e2,e0)) != e0 )
| ( op(e0,op(e1,e0)) = e1
& op(e1,op(e1,e0)) != e0 )
| ( op(e0,op(e0,e0)) = e0
& op(e0,op(e0,e0)) != e0 ) ) ),
inference(assume_negation,[status(cth)],[co1]) ).
cnf(c_19,plain,
( op(e2,e1) = e4
| op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 ),
inference(clausify,[status(thm)],[ax1]) ).
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_38,plain,
op(e2,unit) = e2,
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_111,plain,
op(e2,e1) != op(e0,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_112,plain,
op(e0,e1) != op(e2,e1),
inference(copy,[status(thm)],[c_111]) ).
cnf(c_116,plain,
op(e2,e1) != op(e1,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_117,plain,
op(e1,e1) != op(e2,e1),
inference(copy,[status(thm)],[c_116]) ).
cnf(c_206,plain,
op(e2,e1) != op(e2,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_212,plain,
op(e2,e2) != op(e2,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_213,plain,
op(e2,e1) != op(e2,e2),
inference(copy,[status(thm)],[c_212]) ).
cnf(c_215,plain,
op(e2,e4) != op(e2,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_216,plain,
op(e2,e1) != op(e2,e4),
inference(copy,[status(thm)],[c_215]) ).
cnf(c_217,plain,
op(e2,e3) != op(e2,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_231,plain,
op(e3,e4) != op(e3,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_232,plain,
op(e3,e1) != op(e3,e4),
inference(copy,[status(thm)],[c_231]) ).
cnf(c_238,plain,
op(e4,e1) != op(e4,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_258,plain,
e4 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_259,plain,
e0 != e4,
inference(copy,[status(thm)],[c_258]) ).
cnf(c_263,plain,
e4 != e1,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_264,plain,
e1 != e4,
inference(copy,[status(thm)],[c_263]) ).
cnf(c_265,plain,
e3 != e2,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_266,plain,
e4 != e2,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_267,plain,
e2 != e4,
inference(copy,[status(thm)],[c_266]) ).
cnf(c_270,plain,
op(op(e2,e2),op(e2,e2)) = e0,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_271,plain,
op(op(e2,op(e2,e2)),op(e2,e2)) = e1,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_272,plain,
op(e2,op(e2,e2)) = e3,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_273,plain,
op(e2,e2) = e4,
inference(clausify,[status(thm)],[ax6]) ).
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_376,negated_conjecture,
( op(e2,e4) = e2
| op(e2,e2) != 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_1918,negated_conjecture,
( op(e2,e4) = e2
| e4 != e4
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_273,c_376]) ).
cnf(c_377,negated_conjecture,
( op(e2,e4) = e2
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(copy,[status(thm)],[c_1918]) ).
cnf(c_408,negated_conjecture,
( op(e2,e3) = e4
| op(e2,e4) != e3
| ~ defn_30 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_30]) ).
cnf(c_459,negated_conjecture,
( op(e2,e2) = e1
| op(e2,e1) != e2
| ~ defn_20 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_20]) ).
cnf(c_1919,negated_conjecture,
( e4 = e1
| op(e2,e1) != e2
| ~ defn_20 ),
inference(paramod,[status(thm)],[c_273,c_459]) ).
cnf(c_1920,negated_conjecture,
( e1 = e4
| op(e2,e1) != e2
| ~ defn_20 ),
inference(copy,[status(thm)],[c_1919]) ).
cnf(c_460,negated_conjecture,
( op(e2,e1) != e2
| ~ defn_20 ),
inference(resolve,[status(thm)],[c_264,c_1920]) ).
cnf(c_462,negated_conjecture,
( op(e2,e2) = e0
| op(e2,e0) != e2
| ~ defn_20 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_20]) ).
cnf(c_1921,negated_conjecture,
( e4 = e0
| op(e2,e0) != e2
| ~ defn_20 ),
inference(paramod,[status(thm)],[c_273,c_462]) ).
cnf(c_1922,negated_conjecture,
( e0 = e4
| op(e2,e0) != e2
| ~ defn_20 ),
inference(copy,[status(thm)],[c_1921]) ).
cnf(c_463,negated_conjecture,
( op(e2,e0) != e2
| ~ defn_20 ),
inference(resolve,[status(thm)],[c_259,c_1922]) ).
cnf(c_491,negated_conjecture,
( unit != e1
| op(e3,e4) != e1
| ~ defn_10 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_10]) ).
cnf(c_517,negated_conjecture,
( op(e1,e1) = e0
| op(e1,e0) != e1
| ~ defn_10 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_10]) ).
cnf(c_527,negated_conjecture,
( unit != e0
| op(e4,e4) != e0
| ~ defn_00 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_00]) ).
cnf(c_528,negated_conjecture,
( op(e4,e0) = e4
| op(e4,e4) != e0
| ~ defn_00 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_00]) ).
cnf(c_1923,plain,
op(op(e2,e4),op(e2,e2)) = e1,
inference(paramod,[status(thm)],[c_273,c_271]) ).
cnf(c_572,plain,
op(op(e2,e4),e4) = e1,
inference(paramod,[status(thm)],[c_273,c_1923]) ).
cnf(c_573,plain,
op(e2,e4) = e3,
inference(paramod,[status(thm)],[c_273,c_272]) ).
cnf(c_1924,plain,
op(e4,op(e2,e2)) = e0,
inference(paramod,[status(thm)],[c_273,c_270]) ).
cnf(c_574,plain,
op(e4,e4) = e0,
inference(paramod,[status(thm)],[c_273,c_1924]) ).
cnf(c_575,plain,
op(e2,e3) != e4,
inference(paramod,[status(thm)],[c_273,c_217]) ).
cnf(c_576,plain,
op(e2,e1) != e4,
inference(paramod,[status(thm)],[c_273,c_213]) ).
cnf(c_589,plain,
op(e3,e4) = e1,
inference(paramod,[status(thm)],[c_573,c_572]) ).
cnf(c_1925,negated_conjecture,
( op(e2,e3) = e4
| e3 != e3
| ~ defn_30 ),
inference(paramod,[status(thm)],[c_573,c_408]) ).
cnf(c_1926,negated_conjecture,
( op(e2,e3) = e4
| ~ defn_30 ),
inference(copy,[status(thm)],[c_1925]) ).
cnf(c_590,negated_conjecture,
~ defn_30,
inference(resolve,[status(thm)],[c_575,c_1926]) ).
cnf(c_1927,negated_conjecture,
( e3 = e2
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_573,c_377]) ).
cnf(c_1928,negated_conjecture,
( e3 = e2
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_590,c_1927]) ).
cnf(c_591,negated_conjecture,
( defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_265,c_1928]) ).
cnf(c_601,plain,
op(e2,e1) != e3,
inference(paramod,[status(thm)],[c_573,c_216]) ).
cnf(c_1929,negated_conjecture,
( op(e4,e0) = e4
| e0 != e0
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_574,c_528]) ).
cnf(c_607,negated_conjecture,
( op(e4,e0) = e4
| ~ defn_00 ),
inference(copy,[status(thm)],[c_1929]) ).
cnf(c_1930,negated_conjecture,
( unit != e0
| e0 != e0
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_574,c_527]) ).
cnf(c_608,negated_conjecture,
( unit != e0
| ~ defn_00 ),
inference(copy,[status(thm)],[c_1930]) ).
cnf(c_1931,plain,
( op(e2,e1) = e4
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 ),
inference(resolve,[status(thm)],[c_601,c_19]) ).
cnf(c_622,plain,
( op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 ),
inference(resolve,[status(thm)],[c_576,c_1931]) ).
cnf(c_1932,negated_conjecture,
( unit != e1
| e1 != e1
| ~ defn_10 ),
inference(paramod,[status(thm)],[c_589,c_491]) ).
cnf(c_635,negated_conjecture,
( unit != e1
| ~ defn_10 ),
inference(copy,[status(thm)],[c_1932]) ).
cnf(c_638,plain,
op(e3,e1) != e1,
inference(paramod,[status(thm)],[c_589,c_232]) ).
cnf(c_1933,plain,
( op(e3,e1) = e1
| unit = e4
| unit = e2
| unit = e1
| unit = e0 ),
inference(paramod,[status(thm)],[c_43,c_35]) ).
cnf(c_679,plain,
( unit = e4
| unit = e2
| unit = e1
| unit = e0 ),
inference(resolve,[status(thm)],[c_638,c_1933]) ).
cnf(c_829,plain,
( op(e2,e0) != e2
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_591,c_463]) ).
cnf(c_830,plain,
( op(e2,e1) != e2
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_591,c_460]) ).
cnf(c_1233,plain,
( op(e2,e1) = e2
| unit = e4
| unit = e2
| unit = e0 ),
inference(paramod,[status(thm)],[c_679,c_38]) ).
cnf(c_1237,plain,
( op(e4,e1) = e4
| unit = e4
| unit = e2
| unit = e0 ),
inference(paramod,[status(thm)],[c_679,c_42]) ).
cnf(c_1406,plain,
( defn_10
| defn_00
| unit = e4
| unit = e2
| unit = e0 ),
inference(resolve,[status(thm)],[c_1233,c_830]) ).
cnf(c_1415,plain,
( unit != e1
| defn_00
| unit = e4
| unit = e2
| unit = e0 ),
inference(resolve,[status(thm)],[c_1406,c_635]) ).
cnf(c_1934,plain,
( unit = e4
| unit = e2
| unit = e0
| defn_00
| unit = e4
| unit = e2
| unit = e0 ),
inference(resolve,[status(thm)],[c_1415,c_679]) ).
cnf(c_1935,plain,
( unit = e4
| unit = e2
| defn_00
| unit = e4
| unit = e2
| unit = e0 ),
inference(copy,[status(thm)],[c_1934]) ).
cnf(c_1936,plain,
( unit = e4
| defn_00
| unit = e4
| unit = e2
| unit = e0 ),
inference(copy,[status(thm)],[c_1935]) ).
cnf(c_1422,plain,
( defn_00
| unit = e4
| unit = e2
| unit = e0 ),
inference(copy,[status(thm)],[c_1936]) ).
cnf(c_1424,plain,
( op(e4,e0) = e4
| unit = e4
| unit = e2
| unit = e0 ),
inference(resolve,[status(thm)],[c_1422,c_607]) ).
cnf(c_1937,plain,
( e4 != op(e4,e0)
| unit = e4
| unit = e2
| unit = e0 ),
inference(paramod,[status(thm)],[c_1237,c_238]) ).
cnf(c_1459,plain,
( op(e4,e0) != e4
| unit = e4
| unit = e2
| unit = e0 ),
inference(copy,[status(thm)],[c_1937]) ).
cnf(c_1938,plain,
( unit = e4
| unit = e2
| unit = e0
| unit = e4
| unit = e2
| unit = e0 ),
inference(resolve,[status(thm)],[c_1459,c_1424]) ).
cnf(c_1939,plain,
( unit = e4
| unit = e2
| unit = e4
| unit = e2
| unit = e0 ),
inference(copy,[status(thm)],[c_1938]) ).
cnf(c_1940,plain,
( unit = e4
| unit = e4
| unit = e2
| unit = e0 ),
inference(copy,[status(thm)],[c_1939]) ).
cnf(c_1488,plain,
( unit = e4
| unit = e2
| unit = e0 ),
inference(copy,[status(thm)],[c_1940]) ).
cnf(c_1494,plain,
( op(e0,e1) = e1
| unit = e4
| unit = e2 ),
inference(paramod,[status(thm)],[c_1488,c_35]) ).
cnf(c_1495,plain,
( op(e1,e0) = e1
| unit = e4
| unit = e2 ),
inference(paramod,[status(thm)],[c_1488,c_36]) ).
cnf(c_1497,plain,
( op(e2,e0) = e2
| unit = e4
| unit = e2 ),
inference(paramod,[status(thm)],[c_1488,c_38]) ).
cnf(c_1941,plain,
( e1 != op(e2,e1)
| unit = e4
| unit = e2 ),
inference(paramod,[status(thm)],[c_1494,c_112]) ).
cnf(c_1509,plain,
( op(e2,e1) != e1
| unit = e4
| unit = e2 ),
inference(copy,[status(thm)],[c_1941]) ).
cnf(c_1535,plain,
( defn_10
| defn_00
| unit = e4
| unit = e2 ),
inference(resolve,[status(thm)],[c_1497,c_829]) ).
cnf(c_1539,plain,
( op(e2,e1) != e2
| unit = e4
| unit = e2 ),
inference(paramod,[status(thm)],[c_1497,c_206]) ).
cnf(c_1544,plain,
( op(e1,e1) = e0
| op(e1,e0) != e1
| defn_00
| unit = e4
| unit = e2 ),
inference(resolve,[status(thm)],[c_1535,c_517]) ).
cnf(c_1582,plain,
( op(e2,e1) = e2
| op(e2,e1) = e0
| unit = e4
| unit = e2 ),
inference(resolve,[status(thm)],[c_1509,c_622]) ).
cnf(c_1878,plain,
( op(e1,e1) != e0
| op(e2,e1) = e2
| unit = e4
| unit = e2 ),
inference(paramod,[status(thm)],[c_1582,c_117]) ).
cnf(c_1942,plain,
( unit = e4
| unit = e2
| op(e1,e1) = e0
| defn_00
| unit = e4
| unit = e2 ),
inference(resolve,[status(thm)],[c_1544,c_1495]) ).
cnf(c_1943,plain,
( unit = e4
| op(e1,e1) = e0
| defn_00
| unit = e4
| unit = e2 ),
inference(copy,[status(thm)],[c_1942]) ).
cnf(c_1894,plain,
( op(e1,e1) = e0
| defn_00
| unit = e4
| unit = e2 ),
inference(copy,[status(thm)],[c_1943]) ).
cnf(c_1898,plain,
( unit != e0
| op(e1,e1) = e0
| unit = e4
| unit = e2 ),
inference(resolve,[status(thm)],[c_1894,c_608]) ).
cnf(c_1944,plain,
( unit = e4
| unit = e2
| op(e1,e1) = e0
| unit = e4
| unit = e2 ),
inference(resolve,[status(thm)],[c_1898,c_1488]) ).
cnf(c_1945,plain,
( unit = e4
| op(e1,e1) = e0
| unit = e4
| unit = e2 ),
inference(copy,[status(thm)],[c_1944]) ).
cnf(c_1903,plain,
( op(e1,e1) = e0
| unit = e4
| unit = e2 ),
inference(copy,[status(thm)],[c_1945]) ).
cnf(c_1946,plain,
( op(e2,e1) = e2
| unit = e4
| unit = e2
| unit = e4
| unit = e2 ),
inference(resolve,[status(thm)],[c_1903,c_1878]) ).
cnf(c_1947,plain,
( op(e2,e1) = e2
| unit = e4
| unit = e4
| unit = e2 ),
inference(copy,[status(thm)],[c_1946]) ).
cnf(c_1904,plain,
( op(e2,e1) = e2
| unit = e4
| unit = e2 ),
inference(copy,[status(thm)],[c_1947]) ).
cnf(c_1948,plain,
( unit = e4
| unit = e2
| unit = e4
| unit = e2 ),
inference(resolve,[status(thm)],[c_1904,c_1539]) ).
cnf(c_1949,plain,
( unit = e4
| unit = e4
| unit = e2 ),
inference(copy,[status(thm)],[c_1948]) ).
cnf(c_1909,plain,
( unit = e4
| unit = e2 ),
inference(copy,[status(thm)],[c_1949]) ).
cnf(c_1950,plain,
( op(e2,e2) = e2
| unit = e4 ),
inference(paramod,[status(thm)],[c_1909,c_37]) ).
cnf(c_1951,plain,
( e4 = e2
| unit = e4 ),
inference(paramod,[status(thm)],[c_273,c_1950]) ).
cnf(c_1952,plain,
( e2 = e4
| unit = e4 ),
inference(copy,[status(thm)],[c_1951]) ).
cnf(c_1916,plain,
unit = e4,
inference(resolve,[status(thm)],[c_267,c_1952]) ).
cnf(c_1953,plain,
op(e4,e4) = e4,
inference(paramod,[status(thm)],[c_1916,c_42]) ).
cnf(c_1954,plain,
e0 = e4,
inference(paramod,[status(thm)],[c_574,c_1953]) ).
cnf(c_1917,plain,
$false,
inference(resolve,[status(thm)],[c_259,c_1954]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG055+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.08/0.35 % Computer : n026.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 21:05:10 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.35 % Process 1945986 was started by sandbox2 on n026,
% 0.08/0.35 % Sat Sep 26 21:05:10 2026
% 0.08/0.35 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.40
% 0.12/0.40 % From the command line: assign(max_seconds, 300).
% 1.73/0.68
% 1.73/0.68 % given #500 (T,wt=11): 1509 unit = e2 | unit = e4 | op(e2,e1) != e1. [para(1494(c,1),112(a,1)),flip(c)].
% 1.73/0.68
% 1.73/0.68 % SZS status Theorem for theBenchmark
% 1.73/0.68
% 1.73/0.68 % Proof 1 at 0.21 (+ 0.05) seconds.
% 1.73/0.68 % Length of proof is 89.
% 1.73/0.68 % Level of proof is 21.
% 1.73/0.68 % Maximum clause weight is 25.000.
% 1.73/0.68 % Given clauses 712.
% 1.73/0.68
% 1.73/0.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------