%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG055+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n011.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 : Tue Sep 29 09:21:01 AM UTC 2026
% Result : Theorem 0.19s 0.36s
% Output : Refutation 0.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 180
% Syntax : Number of formulae : 477 ( 57 unt; 174 def)
% Number of atoms : 3095 (2207 equ)
% Maximal formula atoms : 425 ( 6 avg)
% Number of connectives : 4314 (1696 ~;1211 |;1373 &)
% ( 34 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 176 ( 174 usr; 175 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(f1,axiom,
( ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e4 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3
| op(e0,e1) = e4 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3
| op(e0,e2) = e4 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3
| op(e0,e3) = e4 )
& ( op(e0,e4) = e0
| op(e0,e4) = e1
| op(e0,e4) = e2
| op(e0,e4) = e3
| op(e0,e4) = e4 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3
| op(e1,e0) = e4 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3
| op(e1,e1) = e4 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3
| op(e1,e2) = e4 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3
| op(e1,e3) = e4 )
& ( op(e1,e4) = e0
| op(e1,e4) = e1
| op(e1,e4) = e2
| op(e1,e4) = e3
| op(e1,e4) = e4 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3
| op(e2,e0) = e4 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3
| op(e2,e1) = e4 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3
| op(e2,e2) = e4 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3
| op(e2,e3) = e4 )
& ( op(e2,e4) = e0
| op(e2,e4) = e1
| op(e2,e4) = e2
| op(e2,e4) = e3
| op(e2,e4) = e4 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3
| op(e3,e0) = e4 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3
| op(e3,e1) = e4 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3
| op(e3,e2) = e4 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3
| op(e3,e3) = e4 )
& ( op(e3,e4) = e0
| op(e3,e4) = e1
| op(e3,e4) = e2
| op(e3,e4) = e3
| op(e3,e4) = e4 )
& ( op(e4,e0) = e0
| op(e4,e0) = e1
| op(e4,e0) = e2
| op(e4,e0) = e3
| op(e4,e0) = e4 )
& ( op(e4,e1) = e0
| op(e4,e1) = e1
| op(e4,e1) = e2
| op(e4,e1) = e3
| op(e4,e1) = e4 )
& ( op(e4,e2) = e0
| op(e4,e2) = e1
| op(e4,e2) = e2
| op(e4,e2) = e3
| op(e4,e2) = e4 )
& ( op(e4,e3) = e0
| op(e4,e3) = e1
| op(e4,e3) = e2
| op(e4,e3) = e3
| op(e4,e3) = e4 )
& ( op(e4,e4) = e0
| op(e4,e4) = e1
| op(e4,e4) = e2
| op(e4,e4) = e3
| op(e4,e4) = e4 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( op(unit,e0) = e0
& op(e0,unit) = e0
& op(unit,e1) = e1
& op(e1,unit) = e1
& op(unit,e2) = e2
& op(e2,unit) = e2
& op(unit,e3) = e3
& op(e3,unit) = e3
& op(unit,e4) = e4
& op(e4,unit) = e4
& ( unit = e0
| unit = e1
| unit = e2
| unit = e3
| unit = e4 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f4,axiom,
( op(e0,e0) != op(e1,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e4,e0)
& op(e1,e0) != op(e2,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e4,e0)
& op(e2,e0) != op(e3,e0)
& op(e2,e0) != op(e4,e0)
& op(e3,e0) != op(e4,e0)
& op(e0,e1) != op(e1,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e4,e1)
& op(e1,e1) != op(e2,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e4,e1)
& op(e2,e1) != op(e3,e1)
& op(e2,e1) != op(e4,e1)
& op(e3,e1) != op(e4,e1)
& op(e0,e2) != op(e1,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e4,e2)
& op(e1,e2) != op(e2,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e4,e2)
& op(e2,e2) != op(e3,e2)
& op(e2,e2) != op(e4,e2)
& op(e3,e2) != op(e4,e2)
& op(e0,e3) != op(e1,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e4,e3)
& op(e1,e3) != op(e2,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e4,e3)
& op(e2,e3) != op(e3,e3)
& op(e2,e3) != op(e4,e3)
& op(e3,e3) != op(e4,e3)
& op(e0,e4) != op(e1,e4)
& op(e0,e4) != op(e2,e4)
& op(e0,e4) != op(e3,e4)
& op(e0,e4) != op(e4,e4)
& op(e1,e4) != op(e2,e4)
& op(e1,e4) != op(e3,e4)
& op(e1,e4) != op(e4,e4)
& op(e2,e4) != op(e3,e4)
& op(e2,e4) != op(e4,e4)
& op(e3,e4) != op(e4,e4)
& op(e0,e0) != op(e0,e1)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e4)
& op(e0,e1) != op(e0,e2)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e4)
& op(e0,e2) != op(e0,e3)
& op(e0,e2) != op(e0,e4)
& op(e0,e3) != op(e0,e4)
& op(e1,e0) != op(e1,e1)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e4)
& op(e1,e1) != op(e1,e2)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e4)
& op(e1,e2) != op(e1,e3)
& op(e1,e2) != op(e1,e4)
& op(e1,e3) != op(e1,e4)
& op(e2,e0) != op(e2,e1)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e4)
& op(e2,e1) != op(e2,e2)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e4)
& op(e2,e2) != op(e2,e3)
& op(e2,e2) != op(e2,e4)
& op(e2,e3) != op(e2,e4)
& op(e3,e0) != op(e3,e1)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e4)
& op(e3,e1) != op(e3,e2)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e4)
& op(e3,e2) != op(e3,e3)
& op(e3,e2) != op(e3,e4)
& op(e3,e3) != op(e3,e4)
& op(e4,e0) != op(e4,e1)
& op(e4,e0) != op(e4,e2)
& op(e4,e0) != op(e4,e3)
& op(e4,e0) != op(e4,e4)
& op(e4,e1) != op(e4,e2)
& op(e4,e1) != op(e4,e3)
& op(e4,e1) != op(e4,e4)
& op(e4,e2) != op(e4,e3)
& op(e4,e2) != op(e4,e4)
& op(e4,e3) != op(e4,e4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e0 != e4
& e1 != e2
& e1 != e3
& e1 != e4
& e2 != e3
& e2 != e4
& e3 != e4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( e0 = op(op(e2,e2),op(e2,e2))
& e1 = op(op(e2,op(e2,e2)),op(e2,e2))
& e3 = op(e2,op(e2,e2))
& e4 = op(e2,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(f7,conjecture,
~ ( ( ( op(e0,op(e0,e0)) != e0
& op(e0,op(e0,e0)) = e0 )
| ( op(e1,op(e1,e0)) != e0
& op(e0,op(e1,e0)) = e1 )
| ( op(e2,op(e2,e0)) != e0
& op(e0,op(e2,e0)) = e2 )
| ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 ) )
& ( ( op(e0,op(e0,e1)) != e1
& op(e1,op(e0,e1)) = e0 )
| ( op(e1,op(e1,e1)) != e1
& op(e1,op(e1,e1)) = e1 )
| ( op(e2,op(e2,e1)) != e1
& op(e1,op(e2,e1)) = e2 )
| ( op(e3,op(e3,e1)) != e1
& op(e1,op(e3,e1)) = e3 )
| ( op(e4,op(e4,e1)) != e1
& op(e1,op(e4,e1)) = e4 ) )
& ( ( op(e0,op(e0,e2)) != e2
& op(e2,op(e0,e2)) = e0 )
| ( op(e1,op(e1,e2)) != e2
& op(e2,op(e1,e2)) = e1 )
| ( op(e2,op(e2,e2)) != e2
& op(e2,op(e2,e2)) = e2 )
| ( op(e3,op(e3,e2)) != e2
& op(e2,op(e3,e2)) = e3 )
| ( op(e4,op(e4,e2)) != e2
& op(e2,op(e4,e2)) = e4 ) )
& ( ( op(e0,op(e0,e3)) != e3
& op(e3,op(e0,e3)) = e0 )
| ( op(e1,op(e1,e3)) != e3
& op(e3,op(e1,e3)) = e1 )
| ( op(e2,op(e2,e3)) != e3
& op(e3,op(e2,e3)) = e2 )
| ( op(e3,op(e3,e3)) != e3
& op(e3,op(e3,e3)) = e3 )
| ( op(e4,op(e4,e3)) != e3
& op(e3,op(e4,e3)) = e4 ) )
& ( ( op(e0,op(e0,e4)) != e4
& op(e4,op(e0,e4)) = e0 )
| ( op(e1,op(e1,e4)) != e4
& op(e4,op(e1,e4)) = e1 )
| ( op(e2,op(e2,e4)) != e4
& op(e4,op(e2,e4)) = e2 )
| ( op(e3,op(e3,e4)) != e4
& op(e4,op(e3,e4)) = e3 )
| ( op(e4,op(e4,e4)) != e4
& op(e4,op(e4,e4)) = e4 ) )
& ( ( ( op(e0,e0) != e0
| ( op(e0,e0) = e0
& e0 != unit ) )
& ( op(e0,e1) != e0
| ( op(e0,e0) = e1
& e0 != unit ) )
& ( op(e0,e2) != e0
| ( op(e0,e0) = e2
& e0 != unit ) )
& ( op(e0,e3) != e0
| ( op(e0,e0) = e3
& e0 != unit ) )
& ( op(e0,e4) != e0
| ( op(e0,e0) = e4
& e0 != unit ) )
& ( op(e1,e0) != e0
| ( op(e1,e0) = e0
& e0 != unit ) )
& ( op(e1,e1) != e0
| ( op(e1,e0) = e1
& e0 != unit ) )
& ( op(e1,e2) != e0
| ( op(e1,e0) = e2
& e0 != unit ) )
& ( op(e1,e3) != e0
| ( op(e1,e0) = e3
& e0 != unit ) )
& ( op(e1,e4) != e0
| ( op(e1,e0) = e4
& e0 != unit ) )
& ( op(e2,e0) != e0
| ( op(e2,e0) = e0
& e0 != unit ) )
& ( op(e2,e1) != e0
| ( op(e2,e0) = e1
& e0 != unit ) )
& ( op(e2,e2) != e0
| ( op(e2,e0) = e2
& e0 != unit ) )
& ( op(e2,e3) != e0
| ( op(e2,e0) = e3
& e0 != unit ) )
& ( op(e2,e4) != e0
| ( op(e2,e0) = e4
& e0 != unit ) )
& ( op(e3,e0) != e0
| ( op(e3,e0) = e0
& e0 != unit ) )
& ( op(e3,e1) != e0
| ( op(e3,e0) = e1
& e0 != unit ) )
& ( op(e3,e2) != e0
| ( op(e3,e0) = e2
& e0 != unit ) )
& ( op(e3,e3) != e0
| ( op(e3,e0) = e3
& e0 != unit ) )
& ( op(e3,e4) != e0
| ( op(e3,e0) = e4
& e0 != unit ) )
& ( op(e4,e0) != e0
| ( op(e4,e0) = e0
& e0 != unit ) )
& ( op(e4,e1) != e0
| ( op(e4,e0) = e1
& e0 != unit ) )
& ( op(e4,e2) != e0
| ( op(e4,e0) = e2
& e0 != unit ) )
& ( op(e4,e3) != e0
| ( op(e4,e0) = e3
& e0 != unit ) )
& ( op(e4,e4) != e0
| ( op(e4,e0) = e4
& e0 != unit ) ) )
| ( ( op(e0,e0) != e1
| ( op(e0,e1) = e0
& e1 != unit ) )
& ( op(e0,e1) != e1
| ( op(e0,e1) = e1
& e1 != unit ) )
& ( op(e0,e2) != e1
| ( op(e0,e1) = e2
& e1 != unit ) )
& ( op(e0,e3) != e1
| ( op(e0,e1) = e3
& e1 != unit ) )
& ( op(e0,e4) != e1
| ( op(e0,e1) = e4
& e1 != unit ) )
& ( op(e1,e0) != e1
| ( op(e1,e1) = e0
& e1 != unit ) )
& ( op(e1,e1) != e1
| ( op(e1,e1) = e1
& e1 != unit ) )
& ( op(e1,e2) != e1
| ( op(e1,e1) = e2
& e1 != unit ) )
& ( op(e1,e3) != e1
| ( op(e1,e1) = e3
& e1 != unit ) )
& ( op(e1,e4) != e1
| ( op(e1,e1) = e4
& e1 != unit ) )
& ( op(e2,e0) != e1
| ( op(e2,e1) = e0
& e1 != unit ) )
& ( op(e2,e1) != e1
| ( op(e2,e1) = e1
& e1 != unit ) )
& ( op(e2,e2) != e1
| ( op(e2,e1) = e2
& e1 != unit ) )
& ( op(e2,e3) != e1
| ( op(e2,e1) = e3
& e1 != unit ) )
& ( op(e2,e4) != e1
| ( op(e2,e1) = e4
& e1 != unit ) )
& ( op(e3,e0) != e1
| ( op(e3,e1) = e0
& e1 != unit ) )
& ( op(e3,e1) != e1
| ( op(e3,e1) = e1
& e1 != unit ) )
& ( op(e3,e2) != e1
| ( op(e3,e1) = e2
& e1 != unit ) )
& ( op(e3,e3) != e1
| ( op(e3,e1) = e3
& e1 != unit ) )
& ( op(e3,e4) != e1
| ( op(e3,e1) = e4
& e1 != unit ) )
& ( op(e4,e0) != e1
| ( op(e4,e1) = e0
& e1 != unit ) )
& ( op(e4,e1) != e1
| ( op(e4,e1) = e1
& e1 != unit ) )
& ( op(e4,e2) != e1
| ( op(e4,e1) = e2
& e1 != unit ) )
& ( op(e4,e3) != e1
| ( op(e4,e1) = e3
& e1 != unit ) )
& ( op(e4,e4) != e1
| ( op(e4,e1) = e4
& e1 != unit ) ) )
| ( ( op(e0,e0) != e2
| ( op(e0,e2) = e0
& e2 != unit ) )
& ( op(e0,e1) != e2
| ( op(e0,e2) = e1
& e2 != unit ) )
& ( op(e0,e2) != e2
| ( op(e0,e2) = e2
& e2 != unit ) )
& ( op(e0,e3) != e2
| ( op(e0,e2) = e3
& e2 != unit ) )
& ( op(e0,e4) != e2
| ( op(e0,e2) = e4
& e2 != unit ) )
& ( op(e1,e0) != e2
| ( op(e1,e2) = e0
& e2 != unit ) )
& ( op(e1,e1) != e2
| ( op(e1,e2) = e1
& e2 != unit ) )
& ( op(e1,e2) != e2
| ( op(e1,e2) = e2
& e2 != unit ) )
& ( op(e1,e3) != e2
| ( op(e1,e2) = e3
& e2 != unit ) )
& ( op(e1,e4) != e2
| ( op(e1,e2) = e4
& e2 != unit ) )
& ( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit ) )
& ( op(e2,e1) != e2
| ( op(e2,e2) = e1
& e2 != unit ) )
& ( op(e2,e2) != e2
| ( op(e2,e2) = e2
& e2 != unit ) )
& ( op(e2,e3) != e2
| ( op(e2,e2) = e3
& e2 != unit ) )
& ( op(e2,e4) != e2
| ( op(e2,e2) = e4
& e2 != unit ) )
& ( op(e3,e0) != e2
| ( op(e3,e2) = e0
& e2 != unit ) )
& ( op(e3,e1) != e2
| ( op(e3,e2) = e1
& e2 != unit ) )
& ( op(e3,e2) != e2
| ( op(e3,e2) = e2
& e2 != unit ) )
& ( op(e3,e3) != e2
| ( op(e3,e2) = e3
& e2 != unit ) )
& ( op(e3,e4) != e2
| ( op(e3,e2) = e4
& e2 != unit ) )
& ( op(e4,e0) != e2
| ( op(e4,e2) = e0
& e2 != unit ) )
& ( op(e4,e1) != e2
| ( op(e4,e2) = e1
& e2 != unit ) )
& ( op(e4,e2) != e2
| ( op(e4,e2) = e2
& e2 != unit ) )
& ( op(e4,e3) != e2
| ( op(e4,e2) = e3
& e2 != unit ) )
& ( op(e4,e4) != e2
| ( op(e4,e2) = e4
& e2 != unit ) ) )
| ( ( op(e0,e0) != e3
| ( op(e0,e3) = e0
& e3 != unit ) )
& ( op(e0,e1) != e3
| ( op(e0,e3) = e1
& e3 != unit ) )
& ( op(e0,e2) != e3
| ( op(e0,e3) = e2
& e3 != unit ) )
& ( op(e0,e3) != e3
| ( op(e0,e3) = e3
& e3 != unit ) )
& ( op(e0,e4) != e3
| ( op(e0,e3) = e4
& e3 != unit ) )
& ( op(e1,e0) != e3
| ( op(e1,e3) = e0
& e3 != unit ) )
& ( op(e1,e1) != e3
| ( op(e1,e3) = e1
& e3 != unit ) )
& ( op(e1,e2) != e3
| ( op(e1,e3) = e2
& e3 != unit ) )
& ( op(e1,e3) != e3
| ( op(e1,e3) = e3
& e3 != unit ) )
& ( op(e1,e4) != e3
| ( op(e1,e3) = e4
& e3 != unit ) )
& ( op(e2,e0) != e3
| ( op(e2,e3) = e0
& e3 != unit ) )
& ( op(e2,e1) != e3
| ( op(e2,e3) = e1
& e3 != unit ) )
& ( op(e2,e2) != e3
| ( op(e2,e3) = e2
& e3 != unit ) )
& ( op(e2,e3) != e3
| ( op(e2,e3) = e3
& e3 != unit ) )
& ( op(e2,e4) != e3
| ( op(e2,e3) = e4
& e3 != unit ) )
& ( op(e3,e0) != e3
| ( op(e3,e3) = e0
& e3 != unit ) )
& ( op(e3,e1) != e3
| ( op(e3,e3) = e1
& e3 != unit ) )
& ( op(e3,e2) != e3
| ( op(e3,e3) = e2
& e3 != unit ) )
& ( op(e3,e3) != e3
| ( op(e3,e3) = e3
& e3 != unit ) )
& ( op(e3,e4) != e3
| ( op(e3,e3) = e4
& e3 != unit ) )
& ( op(e4,e0) != e3
| ( op(e4,e3) = e0
& e3 != unit ) )
& ( op(e4,e1) != e3
| ( op(e4,e3) = e1
& e3 != unit ) )
& ( op(e4,e2) != e3
| ( op(e4,e3) = e2
& e3 != unit ) )
& ( op(e4,e3) != e3
| ( op(e4,e3) = e3
& e3 != unit ) )
& ( op(e4,e4) != e3
| ( op(e4,e3) = e4
& e3 != unit ) ) )
| ( ( op(e0,e0) != e4
| ( op(e0,e4) = e0
& e4 != unit ) )
& ( op(e0,e1) != e4
| ( op(e0,e4) = e1
& e4 != unit ) )
& ( op(e0,e2) != e4
| ( op(e0,e4) = e2
& e4 != unit ) )
& ( op(e0,e3) != e4
| ( op(e0,e4) = e3
& e4 != unit ) )
& ( op(e0,e4) != e4
| ( op(e0,e4) = e4
& e4 != unit ) )
& ( op(e1,e0) != e4
| ( op(e1,e4) = e0
& e4 != unit ) )
& ( op(e1,e1) != e4
| ( op(e1,e4) = e1
& e4 != unit ) )
& ( op(e1,e2) != e4
| ( op(e1,e4) = e2
& e4 != unit ) )
& ( op(e1,e3) != e4
| ( op(e1,e4) = e3
& e4 != unit ) )
& ( op(e1,e4) != e4
| ( op(e1,e4) = e4
& e4 != unit ) )
& ( op(e2,e0) != e4
| ( op(e2,e4) = e0
& e4 != unit ) )
& ( op(e2,e1) != e4
| ( op(e2,e4) = e1
& e4 != unit ) )
& ( op(e2,e2) != e4
| ( op(e2,e4) = e2
& e4 != unit ) )
& ( op(e2,e3) != e4
| ( op(e2,e4) = e3
& e4 != unit ) )
& ( op(e2,e4) != e4
| ( op(e2,e4) = e4
& e4 != unit ) )
& ( op(e3,e0) != e4
| ( op(e3,e4) = e0
& e4 != unit ) )
& ( op(e3,e1) != e4
| ( op(e3,e4) = e1
& e4 != unit ) )
& ( op(e3,e2) != e4
| ( op(e3,e4) = e2
& e4 != unit ) )
& ( op(e3,e3) != e4
| ( op(e3,e4) = e3
& e4 != unit ) )
& ( op(e3,e4) != e4
| ( op(e3,e4) = e4
& e4 != unit ) )
& ( op(e4,e0) != e4
| ( op(e4,e4) = e0
& e4 != unit ) )
& ( op(e4,e1) != e4
| ( op(e4,e4) = e1
& e4 != unit ) )
& ( op(e4,e2) != e4
| ( op(e4,e4) = e2
& e4 != unit ) )
& ( op(e4,e3) != e4
| ( op(e4,e4) = e3
& e4 != unit ) )
& ( op(e4,e4) != e4
| ( op(e4,e4) = e4
& e4 != unit ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f8,negated_conjecture,
~ ~ ( ( ( op(e0,op(e0,e0)) != e0
& op(e0,op(e0,e0)) = e0 )
| ( op(e1,op(e1,e0)) != e0
& op(e0,op(e1,e0)) = e1 )
| ( op(e2,op(e2,e0)) != e0
& op(e0,op(e2,e0)) = e2 )
| ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 ) )
& ( ( op(e0,op(e0,e1)) != e1
& op(e1,op(e0,e1)) = e0 )
| ( op(e1,op(e1,e1)) != e1
& op(e1,op(e1,e1)) = e1 )
| ( op(e2,op(e2,e1)) != e1
& op(e1,op(e2,e1)) = e2 )
| ( op(e3,op(e3,e1)) != e1
& op(e1,op(e3,e1)) = e3 )
| ( op(e4,op(e4,e1)) != e1
& op(e1,op(e4,e1)) = e4 ) )
& ( ( op(e0,op(e0,e2)) != e2
& op(e2,op(e0,e2)) = e0 )
| ( op(e1,op(e1,e2)) != e2
& op(e2,op(e1,e2)) = e1 )
| ( op(e2,op(e2,e2)) != e2
& op(e2,op(e2,e2)) = e2 )
| ( op(e3,op(e3,e2)) != e2
& op(e2,op(e3,e2)) = e3 )
| ( op(e4,op(e4,e2)) != e2
& op(e2,op(e4,e2)) = e4 ) )
& ( ( op(e0,op(e0,e3)) != e3
& op(e3,op(e0,e3)) = e0 )
| ( op(e1,op(e1,e3)) != e3
& op(e3,op(e1,e3)) = e1 )
| ( op(e2,op(e2,e3)) != e3
& op(e3,op(e2,e3)) = e2 )
| ( op(e3,op(e3,e3)) != e3
& op(e3,op(e3,e3)) = e3 )
| ( op(e4,op(e4,e3)) != e3
& op(e3,op(e4,e3)) = e4 ) )
& ( ( op(e0,op(e0,e4)) != e4
& op(e4,op(e0,e4)) = e0 )
| ( op(e1,op(e1,e4)) != e4
& op(e4,op(e1,e4)) = e1 )
| ( op(e2,op(e2,e4)) != e4
& op(e4,op(e2,e4)) = e2 )
| ( op(e3,op(e3,e4)) != e4
& op(e4,op(e3,e4)) = e3 )
| ( op(e4,op(e4,e4)) != e4
& op(e4,op(e4,e4)) = e4 ) )
& ( ( ( op(e0,e0) != e0
| ( op(e0,e0) = e0
& e0 != unit ) )
& ( op(e0,e1) != e0
| ( op(e0,e0) = e1
& e0 != unit ) )
& ( op(e0,e2) != e0
| ( op(e0,e0) = e2
& e0 != unit ) )
& ( op(e0,e3) != e0
| ( op(e0,e0) = e3
& e0 != unit ) )
& ( op(e0,e4) != e0
| ( op(e0,e0) = e4
& e0 != unit ) )
& ( op(e1,e0) != e0
| ( op(e1,e0) = e0
& e0 != unit ) )
& ( op(e1,e1) != e0
| ( op(e1,e0) = e1
& e0 != unit ) )
& ( op(e1,e2) != e0
| ( op(e1,e0) = e2
& e0 != unit ) )
& ( op(e1,e3) != e0
| ( op(e1,e0) = e3
& e0 != unit ) )
& ( op(e1,e4) != e0
| ( op(e1,e0) = e4
& e0 != unit ) )
& ( op(e2,e0) != e0
| ( op(e2,e0) = e0
& e0 != unit ) )
& ( op(e2,e1) != e0
| ( op(e2,e0) = e1
& e0 != unit ) )
& ( op(e2,e2) != e0
| ( op(e2,e0) = e2
& e0 != unit ) )
& ( op(e2,e3) != e0
| ( op(e2,e0) = e3
& e0 != unit ) )
& ( op(e2,e4) != e0
| ( op(e2,e0) = e4
& e0 != unit ) )
& ( op(e3,e0) != e0
| ( op(e3,e0) = e0
& e0 != unit ) )
& ( op(e3,e1) != e0
| ( op(e3,e0) = e1
& e0 != unit ) )
& ( op(e3,e2) != e0
| ( op(e3,e0) = e2
& e0 != unit ) )
& ( op(e3,e3) != e0
| ( op(e3,e0) = e3
& e0 != unit ) )
& ( op(e3,e4) != e0
| ( op(e3,e0) = e4
& e0 != unit ) )
& ( op(e4,e0) != e0
| ( op(e4,e0) = e0
& e0 != unit ) )
& ( op(e4,e1) != e0
| ( op(e4,e0) = e1
& e0 != unit ) )
& ( op(e4,e2) != e0
| ( op(e4,e0) = e2
& e0 != unit ) )
& ( op(e4,e3) != e0
| ( op(e4,e0) = e3
& e0 != unit ) )
& ( op(e4,e4) != e0
| ( op(e4,e0) = e4
& e0 != unit ) ) )
| ( ( op(e0,e0) != e1
| ( op(e0,e1) = e0
& e1 != unit ) )
& ( op(e0,e1) != e1
| ( op(e0,e1) = e1
& e1 != unit ) )
& ( op(e0,e2) != e1
| ( op(e0,e1) = e2
& e1 != unit ) )
& ( op(e0,e3) != e1
| ( op(e0,e1) = e3
& e1 != unit ) )
& ( op(e0,e4) != e1
| ( op(e0,e1) = e4
& e1 != unit ) )
& ( op(e1,e0) != e1
| ( op(e1,e1) = e0
& e1 != unit ) )
& ( op(e1,e1) != e1
| ( op(e1,e1) = e1
& e1 != unit ) )
& ( op(e1,e2) != e1
| ( op(e1,e1) = e2
& e1 != unit ) )
& ( op(e1,e3) != e1
| ( op(e1,e1) = e3
& e1 != unit ) )
& ( op(e1,e4) != e1
| ( op(e1,e1) = e4
& e1 != unit ) )
& ( op(e2,e0) != e1
| ( op(e2,e1) = e0
& e1 != unit ) )
& ( op(e2,e1) != e1
| ( op(e2,e1) = e1
& e1 != unit ) )
& ( op(e2,e2) != e1
| ( op(e2,e1) = e2
& e1 != unit ) )
& ( op(e2,e3) != e1
| ( op(e2,e1) = e3
& e1 != unit ) )
& ( op(e2,e4) != e1
| ( op(e2,e1) = e4
& e1 != unit ) )
& ( op(e3,e0) != e1
| ( op(e3,e1) = e0
& e1 != unit ) )
& ( op(e3,e1) != e1
| ( op(e3,e1) = e1
& e1 != unit ) )
& ( op(e3,e2) != e1
| ( op(e3,e1) = e2
& e1 != unit ) )
& ( op(e3,e3) != e1
| ( op(e3,e1) = e3
& e1 != unit ) )
& ( op(e3,e4) != e1
| ( op(e3,e1) = e4
& e1 != unit ) )
& ( op(e4,e0) != e1
| ( op(e4,e1) = e0
& e1 != unit ) )
& ( op(e4,e1) != e1
| ( op(e4,e1) = e1
& e1 != unit ) )
& ( op(e4,e2) != e1
| ( op(e4,e1) = e2
& e1 != unit ) )
& ( op(e4,e3) != e1
| ( op(e4,e1) = e3
& e1 != unit ) )
& ( op(e4,e4) != e1
| ( op(e4,e1) = e4
& e1 != unit ) ) )
| ( ( op(e0,e0) != e2
| ( op(e0,e2) = e0
& e2 != unit ) )
& ( op(e0,e1) != e2
| ( op(e0,e2) = e1
& e2 != unit ) )
& ( op(e0,e2) != e2
| ( op(e0,e2) = e2
& e2 != unit ) )
& ( op(e0,e3) != e2
| ( op(e0,e2) = e3
& e2 != unit ) )
& ( op(e0,e4) != e2
| ( op(e0,e2) = e4
& e2 != unit ) )
& ( op(e1,e0) != e2
| ( op(e1,e2) = e0
& e2 != unit ) )
& ( op(e1,e1) != e2
| ( op(e1,e2) = e1
& e2 != unit ) )
& ( op(e1,e2) != e2
| ( op(e1,e2) = e2
& e2 != unit ) )
& ( op(e1,e3) != e2
| ( op(e1,e2) = e3
& e2 != unit ) )
& ( op(e1,e4) != e2
| ( op(e1,e2) = e4
& e2 != unit ) )
& ( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit ) )
& ( op(e2,e1) != e2
| ( op(e2,e2) = e1
& e2 != unit ) )
& ( op(e2,e2) != e2
| ( op(e2,e2) = e2
& e2 != unit ) )
& ( op(e2,e3) != e2
| ( op(e2,e2) = e3
& e2 != unit ) )
& ( op(e2,e4) != e2
| ( op(e2,e2) = e4
& e2 != unit ) )
& ( op(e3,e0) != e2
| ( op(e3,e2) = e0
& e2 != unit ) )
& ( op(e3,e1) != e2
| ( op(e3,e2) = e1
& e2 != unit ) )
& ( op(e3,e2) != e2
| ( op(e3,e2) = e2
& e2 != unit ) )
& ( op(e3,e3) != e2
| ( op(e3,e2) = e3
& e2 != unit ) )
& ( op(e3,e4) != e2
| ( op(e3,e2) = e4
& e2 != unit ) )
& ( op(e4,e0) != e2
| ( op(e4,e2) = e0
& e2 != unit ) )
& ( op(e4,e1) != e2
| ( op(e4,e2) = e1
& e2 != unit ) )
& ( op(e4,e2) != e2
| ( op(e4,e2) = e2
& e2 != unit ) )
& ( op(e4,e3) != e2
| ( op(e4,e2) = e3
& e2 != unit ) )
& ( op(e4,e4) != e2
| ( op(e4,e2) = e4
& e2 != unit ) ) )
| ( ( op(e0,e0) != e3
| ( op(e0,e3) = e0
& e3 != unit ) )
& ( op(e0,e1) != e3
| ( op(e0,e3) = e1
& e3 != unit ) )
& ( op(e0,e2) != e3
| ( op(e0,e3) = e2
& e3 != unit ) )
& ( op(e0,e3) != e3
| ( op(e0,e3) = e3
& e3 != unit ) )
& ( op(e0,e4) != e3
| ( op(e0,e3) = e4
& e3 != unit ) )
& ( op(e1,e0) != e3
| ( op(e1,e3) = e0
& e3 != unit ) )
& ( op(e1,e1) != e3
| ( op(e1,e3) = e1
& e3 != unit ) )
& ( op(e1,e2) != e3
| ( op(e1,e3) = e2
& e3 != unit ) )
& ( op(e1,e3) != e3
| ( op(e1,e3) = e3
& e3 != unit ) )
& ( op(e1,e4) != e3
| ( op(e1,e3) = e4
& e3 != unit ) )
& ( op(e2,e0) != e3
| ( op(e2,e3) = e0
& e3 != unit ) )
& ( op(e2,e1) != e3
| ( op(e2,e3) = e1
& e3 != unit ) )
& ( op(e2,e2) != e3
| ( op(e2,e3) = e2
& e3 != unit ) )
& ( op(e2,e3) != e3
| ( op(e2,e3) = e3
& e3 != unit ) )
& ( op(e2,e4) != e3
| ( op(e2,e3) = e4
& e3 != unit ) )
& ( op(e3,e0) != e3
| ( op(e3,e3) = e0
& e3 != unit ) )
& ( op(e3,e1) != e3
| ( op(e3,e3) = e1
& e3 != unit ) )
& ( op(e3,e2) != e3
| ( op(e3,e3) = e2
& e3 != unit ) )
& ( op(e3,e3) != e3
| ( op(e3,e3) = e3
& e3 != unit ) )
& ( op(e3,e4) != e3
| ( op(e3,e3) = e4
& e3 != unit ) )
& ( op(e4,e0) != e3
| ( op(e4,e3) = e0
& e3 != unit ) )
& ( op(e4,e1) != e3
| ( op(e4,e3) = e1
& e3 != unit ) )
& ( op(e4,e2) != e3
| ( op(e4,e3) = e2
& e3 != unit ) )
& ( op(e4,e3) != e3
| ( op(e4,e3) = e3
& e3 != unit ) )
& ( op(e4,e4) != e3
| ( op(e4,e3) = e4
& e3 != unit ) ) )
| ( ( op(e0,e0) != e4
| ( op(e0,e4) = e0
& e4 != unit ) )
& ( op(e0,e1) != e4
| ( op(e0,e4) = e1
& e4 != unit ) )
& ( op(e0,e2) != e4
| ( op(e0,e4) = e2
& e4 != unit ) )
& ( op(e0,e3) != e4
| ( op(e0,e4) = e3
& e4 != unit ) )
& ( op(e0,e4) != e4
| ( op(e0,e4) = e4
& e4 != unit ) )
& ( op(e1,e0) != e4
| ( op(e1,e4) = e0
& e4 != unit ) )
& ( op(e1,e1) != e4
| ( op(e1,e4) = e1
& e4 != unit ) )
& ( op(e1,e2) != e4
| ( op(e1,e4) = e2
& e4 != unit ) )
& ( op(e1,e3) != e4
| ( op(e1,e4) = e3
& e4 != unit ) )
& ( op(e1,e4) != e4
| ( op(e1,e4) = e4
& e4 != unit ) )
& ( op(e2,e0) != e4
| ( op(e2,e4) = e0
& e4 != unit ) )
& ( op(e2,e1) != e4
| ( op(e2,e4) = e1
& e4 != unit ) )
& ( op(e2,e2) != e4
| ( op(e2,e4) = e2
& e4 != unit ) )
& ( op(e2,e3) != e4
| ( op(e2,e4) = e3
& e4 != unit ) )
& ( op(e2,e4) != e4
| ( op(e2,e4) = e4
& e4 != unit ) )
& ( op(e3,e0) != e4
| ( op(e3,e4) = e0
& e4 != unit ) )
& ( op(e3,e1) != e4
| ( op(e3,e4) = e1
& e4 != unit ) )
& ( op(e3,e2) != e4
| ( op(e3,e4) = e2
& e4 != unit ) )
& ( op(e3,e3) != e4
| ( op(e3,e4) = e3
& e4 != unit ) )
& ( op(e3,e4) != e4
| ( op(e3,e4) = e4
& e4 != unit ) )
& ( op(e4,e0) != e4
| ( op(e4,e4) = e0
& e4 != unit ) )
& ( op(e4,e1) != e4
| ( op(e4,e4) = e1
& e4 != unit ) )
& ( op(e4,e2) != e4
| ( op(e4,e4) = e2
& e4 != unit ) )
& ( op(e4,e3) != e4
| ( op(e4,e4) = e3
& e4 != unit ) )
& ( op(e4,e4) != e4
| ( op(e4,e4) = e4
& e4 != unit ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f7]) ).
fof(f9,plain,
( ( ( op(e0,op(e0,e0)) != e0
& op(e0,op(e0,e0)) = e0 )
| ( op(e1,op(e1,e0)) != e0
& op(e0,op(e1,e0)) = e1 )
| ( op(e2,op(e2,e0)) != e0
& op(e0,op(e2,e0)) = e2 )
| ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 ) )
& ( ( op(e0,op(e0,e1)) != e1
& op(e1,op(e0,e1)) = e0 )
| ( op(e1,op(e1,e1)) != e1
& op(e1,op(e1,e1)) = e1 )
| ( op(e2,op(e2,e1)) != e1
& op(e1,op(e2,e1)) = e2 )
| ( op(e3,op(e3,e1)) != e1
& op(e1,op(e3,e1)) = e3 )
| ( op(e4,op(e4,e1)) != e1
& op(e1,op(e4,e1)) = e4 ) )
& ( ( op(e0,op(e0,e2)) != e2
& op(e2,op(e0,e2)) = e0 )
| ( op(e1,op(e1,e2)) != e2
& op(e2,op(e1,e2)) = e1 )
| ( op(e2,op(e2,e2)) != e2
& op(e2,op(e2,e2)) = e2 )
| ( op(e3,op(e3,e2)) != e2
& op(e2,op(e3,e2)) = e3 )
| ( op(e4,op(e4,e2)) != e2
& op(e2,op(e4,e2)) = e4 ) )
& ( ( op(e0,op(e0,e3)) != e3
& op(e3,op(e0,e3)) = e0 )
| ( op(e1,op(e1,e3)) != e3
& op(e3,op(e1,e3)) = e1 )
| ( op(e2,op(e2,e3)) != e3
& op(e3,op(e2,e3)) = e2 )
| ( op(e3,op(e3,e3)) != e3
& op(e3,op(e3,e3)) = e3 )
| ( op(e4,op(e4,e3)) != e3
& op(e3,op(e4,e3)) = e4 ) )
& ( ( op(e0,op(e0,e4)) != e4
& op(e4,op(e0,e4)) = e0 )
| ( op(e1,op(e1,e4)) != e4
& op(e4,op(e1,e4)) = e1 )
| ( op(e2,op(e2,e4)) != e4
& op(e4,op(e2,e4)) = e2 )
| ( op(e3,op(e3,e4)) != e4
& op(e4,op(e3,e4)) = e3 )
| ( op(e4,op(e4,e4)) != e4
& op(e4,op(e4,e4)) = e4 ) )
& ( ( ( op(e0,e0) != e0
| ( op(e0,e0) = e0
& e0 != unit ) )
& ( op(e0,e1) != e0
| ( op(e0,e0) = e1
& e0 != unit ) )
& ( op(e0,e2) != e0
| ( op(e0,e0) = e2
& e0 != unit ) )
& ( op(e0,e3) != e0
| ( op(e0,e0) = e3
& e0 != unit ) )
& ( op(e0,e4) != e0
| ( op(e0,e0) = e4
& e0 != unit ) )
& ( op(e1,e0) != e0
| ( op(e1,e0) = e0
& e0 != unit ) )
& ( op(e1,e1) != e0
| ( op(e1,e0) = e1
& e0 != unit ) )
& ( op(e1,e2) != e0
| ( op(e1,e0) = e2
& e0 != unit ) )
& ( op(e1,e3) != e0
| ( op(e1,e0) = e3
& e0 != unit ) )
& ( op(e1,e4) != e0
| ( op(e1,e0) = e4
& e0 != unit ) )
& ( op(e2,e0) != e0
| ( op(e2,e0) = e0
& e0 != unit ) )
& ( op(e2,e1) != e0
| ( op(e2,e0) = e1
& e0 != unit ) )
& ( op(e2,e2) != e0
| ( op(e2,e0) = e2
& e0 != unit ) )
& ( op(e2,e3) != e0
| ( op(e2,e0) = e3
& e0 != unit ) )
& ( op(e2,e4) != e0
| ( op(e2,e0) = e4
& e0 != unit ) )
& ( op(e3,e0) != e0
| ( op(e3,e0) = e0
& e0 != unit ) )
& ( op(e3,e1) != e0
| ( op(e3,e0) = e1
& e0 != unit ) )
& ( op(e3,e2) != e0
| ( op(e3,e0) = e2
& e0 != unit ) )
& ( op(e3,e3) != e0
| ( op(e3,e0) = e3
& e0 != unit ) )
& ( op(e3,e4) != e0
| ( op(e3,e0) = e4
& e0 != unit ) )
& ( op(e4,e0) != e0
| ( op(e4,e0) = e0
& e0 != unit ) )
& ( op(e4,e1) != e0
| ( op(e4,e0) = e1
& e0 != unit ) )
& ( op(e4,e2) != e0
| ( op(e4,e0) = e2
& e0 != unit ) )
& ( op(e4,e3) != e0
| ( op(e4,e0) = e3
& e0 != unit ) )
& ( op(e4,e4) != e0
| ( op(e4,e0) = e4
& e0 != unit ) ) )
| ( ( op(e0,e0) != e1
| ( op(e0,e1) = e0
& e1 != unit ) )
& ( op(e0,e1) != e1
| ( op(e0,e1) = e1
& e1 != unit ) )
& ( op(e0,e2) != e1
| ( op(e0,e1) = e2
& e1 != unit ) )
& ( op(e0,e3) != e1
| ( op(e0,e1) = e3
& e1 != unit ) )
& ( op(e0,e4) != e1
| ( op(e0,e1) = e4
& e1 != unit ) )
& ( op(e1,e0) != e1
| ( op(e1,e1) = e0
& e1 != unit ) )
& ( op(e1,e1) != e1
| ( op(e1,e1) = e1
& e1 != unit ) )
& ( op(e1,e2) != e1
| ( op(e1,e1) = e2
& e1 != unit ) )
& ( op(e1,e3) != e1
| ( op(e1,e1) = e3
& e1 != unit ) )
& ( op(e1,e4) != e1
| ( op(e1,e1) = e4
& e1 != unit ) )
& ( op(e2,e0) != e1
| ( op(e2,e1) = e0
& e1 != unit ) )
& ( op(e2,e1) != e1
| ( op(e2,e1) = e1
& e1 != unit ) )
& ( op(e2,e2) != e1
| ( op(e2,e1) = e2
& e1 != unit ) )
& ( op(e2,e3) != e1
| ( op(e2,e1) = e3
& e1 != unit ) )
& ( op(e2,e4) != e1
| ( op(e2,e1) = e4
& e1 != unit ) )
& ( op(e3,e0) != e1
| ( op(e3,e1) = e0
& e1 != unit ) )
& ( op(e3,e1) != e1
| ( op(e3,e1) = e1
& e1 != unit ) )
& ( op(e3,e2) != e1
| ( op(e3,e1) = e2
& e1 != unit ) )
& ( op(e3,e3) != e1
| ( op(e3,e1) = e3
& e1 != unit ) )
& ( op(e3,e4) != e1
| ( op(e3,e1) = e4
& e1 != unit ) )
& ( op(e4,e0) != e1
| ( op(e4,e1) = e0
& e1 != unit ) )
& ( op(e4,e1) != e1
| ( op(e4,e1) = e1
& e1 != unit ) )
& ( op(e4,e2) != e1
| ( op(e4,e1) = e2
& e1 != unit ) )
& ( op(e4,e3) != e1
| ( op(e4,e1) = e3
& e1 != unit ) )
& ( op(e4,e4) != e1
| ( op(e4,e1) = e4
& e1 != unit ) ) )
| ( ( op(e0,e0) != e2
| ( op(e0,e2) = e0
& e2 != unit ) )
& ( op(e0,e1) != e2
| ( op(e0,e2) = e1
& e2 != unit ) )
& ( op(e0,e2) != e2
| ( op(e0,e2) = e2
& e2 != unit ) )
& ( op(e0,e3) != e2
| ( op(e0,e2) = e3
& e2 != unit ) )
& ( op(e0,e4) != e2
| ( op(e0,e2) = e4
& e2 != unit ) )
& ( op(e1,e0) != e2
| ( op(e1,e2) = e0
& e2 != unit ) )
& ( op(e1,e1) != e2
| ( op(e1,e2) = e1
& e2 != unit ) )
& ( op(e1,e2) != e2
| ( op(e1,e2) = e2
& e2 != unit ) )
& ( op(e1,e3) != e2
| ( op(e1,e2) = e3
& e2 != unit ) )
& ( op(e1,e4) != e2
| ( op(e1,e2) = e4
& e2 != unit ) )
& ( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit ) )
& ( op(e2,e1) != e2
| ( op(e2,e2) = e1
& e2 != unit ) )
& ( op(e2,e2) != e2
| ( op(e2,e2) = e2
& e2 != unit ) )
& ( op(e2,e3) != e2
| ( op(e2,e2) = e3
& e2 != unit ) )
& ( op(e2,e4) != e2
| ( op(e2,e2) = e4
& e2 != unit ) )
& ( op(e3,e0) != e2
| ( op(e3,e2) = e0
& e2 != unit ) )
& ( op(e3,e1) != e2
| ( op(e3,e2) = e1
& e2 != unit ) )
& ( op(e3,e2) != e2
| ( op(e3,e2) = e2
& e2 != unit ) )
& ( op(e3,e3) != e2
| ( op(e3,e2) = e3
& e2 != unit ) )
& ( op(e3,e4) != e2
| ( op(e3,e2) = e4
& e2 != unit ) )
& ( op(e4,e0) != e2
| ( op(e4,e2) = e0
& e2 != unit ) )
& ( op(e4,e1) != e2
| ( op(e4,e2) = e1
& e2 != unit ) )
& ( op(e4,e2) != e2
| ( op(e4,e2) = e2
& e2 != unit ) )
& ( op(e4,e3) != e2
| ( op(e4,e2) = e3
& e2 != unit ) )
& ( op(e4,e4) != e2
| ( op(e4,e2) = e4
& e2 != unit ) ) )
| ( ( op(e0,e0) != e3
| ( op(e0,e3) = e0
& e3 != unit ) )
& ( op(e0,e1) != e3
| ( op(e0,e3) = e1
& e3 != unit ) )
& ( op(e0,e2) != e3
| ( op(e0,e3) = e2
& e3 != unit ) )
& ( op(e0,e3) != e3
| ( op(e0,e3) = e3
& e3 != unit ) )
& ( op(e0,e4) != e3
| ( op(e0,e3) = e4
& e3 != unit ) )
& ( op(e1,e0) != e3
| ( op(e1,e3) = e0
& e3 != unit ) )
& ( op(e1,e1) != e3
| ( op(e1,e3) = e1
& e3 != unit ) )
& ( op(e1,e2) != e3
| ( op(e1,e3) = e2
& e3 != unit ) )
& ( op(e1,e3) != e3
| ( op(e1,e3) = e3
& e3 != unit ) )
& ( op(e1,e4) != e3
| ( op(e1,e3) = e4
& e3 != unit ) )
& ( op(e2,e0) != e3
| ( op(e2,e3) = e0
& e3 != unit ) )
& ( op(e2,e1) != e3
| ( op(e2,e3) = e1
& e3 != unit ) )
& ( op(e2,e2) != e3
| ( op(e2,e3) = e2
& e3 != unit ) )
& ( op(e2,e3) != e3
| ( op(e2,e3) = e3
& e3 != unit ) )
& ( op(e2,e4) != e3
| ( op(e2,e3) = e4
& e3 != unit ) )
& ( op(e3,e0) != e3
| ( op(e3,e3) = e0
& e3 != unit ) )
& ( op(e3,e1) != e3
| ( op(e3,e3) = e1
& e3 != unit ) )
& ( op(e3,e2) != e3
| ( op(e3,e3) = e2
& e3 != unit ) )
& ( op(e3,e3) != e3
| ( op(e3,e3) = e3
& e3 != unit ) )
& ( op(e3,e4) != e3
| ( op(e3,e3) = e4
& e3 != unit ) )
& ( op(e4,e0) != e3
| ( op(e4,e3) = e0
& e3 != unit ) )
& ( op(e4,e1) != e3
| ( op(e4,e3) = e1
& e3 != unit ) )
& ( op(e4,e2) != e3
| ( op(e4,e3) = e2
& e3 != unit ) )
& ( op(e4,e3) != e3
| ( op(e4,e3) = e3
& e3 != unit ) )
& ( op(e4,e4) != e3
| ( op(e4,e3) = e4
& e3 != unit ) ) )
| ( ( op(e0,e0) != e4
| ( op(e0,e4) = e0
& e4 != unit ) )
& ( op(e0,e1) != e4
| ( op(e0,e4) = e1
& e4 != unit ) )
& ( op(e0,e2) != e4
| ( op(e0,e4) = e2
& e4 != unit ) )
& ( op(e0,e3) != e4
| ( op(e0,e4) = e3
& e4 != unit ) )
& ( op(e0,e4) != e4
| ( op(e0,e4) = e4
& e4 != unit ) )
& ( op(e1,e0) != e4
| ( op(e1,e4) = e0
& e4 != unit ) )
& ( op(e1,e1) != e4
| ( op(e1,e4) = e1
& e4 != unit ) )
& ( op(e1,e2) != e4
| ( op(e1,e4) = e2
& e4 != unit ) )
& ( op(e1,e3) != e4
| ( op(e1,e4) = e3
& e4 != unit ) )
& ( op(e1,e4) != e4
| ( op(e1,e4) = e4
& e4 != unit ) )
& ( op(e2,e0) != e4
| ( op(e2,e4) = e0
& e4 != unit ) )
& ( op(e2,e1) != e4
| ( op(e2,e4) = e1
& e4 != unit ) )
& ( op(e2,e2) != e4
| ( op(e2,e4) = e2
& e4 != unit ) )
& ( op(e2,e3) != e4
| ( op(e2,e4) = e3
& e4 != unit ) )
& ( op(e2,e4) != e4
| ( op(e2,e4) = e4
& e4 != unit ) )
& ( op(e3,e0) != e4
| ( op(e3,e4) = e0
& e4 != unit ) )
& ( op(e3,e1) != e4
| ( op(e3,e4) = e1
& e4 != unit ) )
& ( op(e3,e2) != e4
| ( op(e3,e4) = e2
& e4 != unit ) )
& ( op(e3,e3) != e4
| ( op(e3,e4) = e3
& e4 != unit ) )
& ( op(e3,e4) != e4
| ( op(e3,e4) = e4
& e4 != unit ) )
& ( op(e4,e0) != e4
| ( op(e4,e4) = e0
& e4 != unit ) )
& ( op(e4,e1) != e4
| ( op(e4,e4) = e1
& e4 != unit ) )
& ( op(e4,e2) != e4
| ( op(e4,e4) = e2
& e4 != unit ) )
& ( op(e4,e3) != e4
| ( op(e4,e4) = e3
& e4 != unit ) )
& ( op(e4,e4) != e4
| ( op(e4,e4) = e4
& e4 != unit ) ) ) ) ),
inference(flattening,[],[f8]) ).
fof(f10,definition,
( op(e4,e4) != e4
| ( op(e4,e4) = e4
& e4 != unit )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f11,definition,
( op(e4,e3) != e4
| ( op(e4,e4) = e3
& e4 != unit )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f12,definition,
( op(e4,e2) != e4
| ( op(e4,e4) = e2
& e4 != unit )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f13,definition,
( op(e4,e1) != e4
| ( op(e4,e4) = e1
& e4 != unit )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f14,definition,
( op(e4,e0) != e4
| ( op(e4,e4) = e0
& e4 != unit )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f15,definition,
( op(e3,e4) != e4
| ( op(e3,e4) = e4
& e4 != unit )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f16,definition,
( op(e3,e3) != e4
| ( op(e3,e4) = e3
& e4 != unit )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f17,definition,
( op(e3,e2) != e4
| ( op(e3,e4) = e2
& e4 != unit )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f18,definition,
( op(e3,e1) != e4
| ( op(e3,e4) = e1
& e4 != unit )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f19,definition,
( op(e3,e0) != e4
| ( op(e3,e4) = e0
& e4 != unit )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f20,definition,
( op(e2,e4) != e4
| ( op(e2,e4) = e4
& e4 != unit )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f21,definition,
( op(e2,e3) != e4
| ( op(e2,e4) = e3
& e4 != unit )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f22,definition,
( op(e2,e2) != e4
| ( op(e2,e4) = e2
& e4 != unit )
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f23,definition,
( op(e2,e1) != e4
| ( op(e2,e4) = e1
& e4 != unit )
| ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f24,definition,
( op(e2,e0) != e4
| ( op(e2,e4) = e0
& e4 != unit )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f25,definition,
( op(e1,e4) != e4
| ( op(e1,e4) = e4
& e4 != unit )
| ~ sP15 ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f26,definition,
( op(e1,e3) != e4
| ( op(e1,e4) = e3
& e4 != unit )
| ~ sP16 ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f27,definition,
( op(e1,e2) != e4
| ( op(e1,e4) = e2
& e4 != unit )
| ~ sP17 ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f28,definition,
( op(e1,e1) != e4
| ( op(e1,e4) = e1
& e4 != unit )
| ~ sP18 ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f29,definition,
( op(e1,e0) != e4
| ( op(e1,e4) = e0
& e4 != unit )
| ~ sP19 ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f30,definition,
( op(e0,e4) != e4
| ( op(e0,e4) = e4
& e4 != unit )
| ~ sP20 ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f31,definition,
( op(e0,e3) != e4
| ( op(e0,e4) = e3
& e4 != unit )
| ~ sP21 ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f32,definition,
( op(e0,e2) != e4
| ( op(e0,e4) = e2
& e4 != unit )
| ~ sP22 ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f33,definition,
( op(e0,e1) != e4
| ( op(e0,e4) = e1
& e4 != unit )
| ~ sP23 ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f34,definition,
( op(e0,e0) != e4
| ( op(e0,e4) = e0
& e4 != unit )
| ~ sP24 ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f35,definition,
( op(e4,e4) != e3
| ( op(e4,e3) = e4
& e3 != unit )
| ~ sP25 ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f36,definition,
( op(e4,e3) != e3
| ( op(e4,e3) = e3
& e3 != unit )
| ~ sP26 ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f37,definition,
( op(e4,e2) != e3
| ( op(e4,e3) = e2
& e3 != unit )
| ~ sP27 ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f38,definition,
( op(e4,e1) != e3
| ( op(e4,e3) = e1
& e3 != unit )
| ~ sP28 ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f39,definition,
( op(e4,e0) != e3
| ( op(e4,e3) = e0
& e3 != unit )
| ~ sP29 ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f40,definition,
( op(e3,e4) != e3
| ( op(e3,e3) = e4
& e3 != unit )
| ~ sP30 ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f41,definition,
( op(e3,e3) != e3
| ( op(e3,e3) = e3
& e3 != unit )
| ~ sP31 ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f42,definition,
( op(e3,e2) != e3
| ( op(e3,e3) = e2
& e3 != unit )
| ~ sP32 ),
introduced(definition,[new_symbols(definition,[sP32])],[predicate_definition_introduction]) ).
fof(f43,definition,
( op(e3,e1) != e3
| ( op(e3,e3) = e1
& e3 != unit )
| ~ sP33 ),
introduced(definition,[new_symbols(definition,[sP33])],[predicate_definition_introduction]) ).
fof(f44,definition,
( op(e3,e0) != e3
| ( op(e3,e3) = e0
& e3 != unit )
| ~ sP34 ),
introduced(definition,[new_symbols(definition,[sP34])],[predicate_definition_introduction]) ).
fof(f45,definition,
( op(e2,e4) != e3
| ( op(e2,e3) = e4
& e3 != unit )
| ~ sP35 ),
introduced(definition,[new_symbols(definition,[sP35])],[predicate_definition_introduction]) ).
fof(f46,definition,
( op(e2,e3) != e3
| ( op(e2,e3) = e3
& e3 != unit )
| ~ sP36 ),
introduced(definition,[new_symbols(definition,[sP36])],[predicate_definition_introduction]) ).
fof(f47,definition,
( op(e2,e2) != e3
| ( op(e2,e3) = e2
& e3 != unit )
| ~ sP37 ),
introduced(definition,[new_symbols(definition,[sP37])],[predicate_definition_introduction]) ).
fof(f48,definition,
( op(e2,e1) != e3
| ( op(e2,e3) = e1
& e3 != unit )
| ~ sP38 ),
introduced(definition,[new_symbols(definition,[sP38])],[predicate_definition_introduction]) ).
fof(f49,definition,
( op(e2,e0) != e3
| ( op(e2,e3) = e0
& e3 != unit )
| ~ sP39 ),
introduced(definition,[new_symbols(definition,[sP39])],[predicate_definition_introduction]) ).
fof(f50,definition,
( op(e1,e4) != e3
| ( op(e1,e3) = e4
& e3 != unit )
| ~ sP40 ),
introduced(definition,[new_symbols(definition,[sP40])],[predicate_definition_introduction]) ).
fof(f51,definition,
( op(e1,e3) != e3
| ( op(e1,e3) = e3
& e3 != unit )
| ~ sP41 ),
introduced(definition,[new_symbols(definition,[sP41])],[predicate_definition_introduction]) ).
fof(f52,definition,
( op(e1,e2) != e3
| ( op(e1,e3) = e2
& e3 != unit )
| ~ sP42 ),
introduced(definition,[new_symbols(definition,[sP42])],[predicate_definition_introduction]) ).
fof(f53,definition,
( op(e1,e1) != e3
| ( op(e1,e3) = e1
& e3 != unit )
| ~ sP43 ),
introduced(definition,[new_symbols(definition,[sP43])],[predicate_definition_introduction]) ).
fof(f54,definition,
( op(e1,e0) != e3
| ( op(e1,e3) = e0
& e3 != unit )
| ~ sP44 ),
introduced(definition,[new_symbols(definition,[sP44])],[predicate_definition_introduction]) ).
fof(f55,definition,
( op(e0,e4) != e3
| ( op(e0,e3) = e4
& e3 != unit )
| ~ sP45 ),
introduced(definition,[new_symbols(definition,[sP45])],[predicate_definition_introduction]) ).
fof(f56,definition,
( op(e0,e3) != e3
| ( op(e0,e3) = e3
& e3 != unit )
| ~ sP46 ),
introduced(definition,[new_symbols(definition,[sP46])],[predicate_definition_introduction]) ).
fof(f57,definition,
( op(e0,e2) != e3
| ( op(e0,e3) = e2
& e3 != unit )
| ~ sP47 ),
introduced(definition,[new_symbols(definition,[sP47])],[predicate_definition_introduction]) ).
fof(f58,definition,
( op(e0,e1) != e3
| ( op(e0,e3) = e1
& e3 != unit )
| ~ sP48 ),
introduced(definition,[new_symbols(definition,[sP48])],[predicate_definition_introduction]) ).
fof(f59,definition,
( op(e0,e0) != e3
| ( op(e0,e3) = e0
& e3 != unit )
| ~ sP49 ),
introduced(definition,[new_symbols(definition,[sP49])],[predicate_definition_introduction]) ).
fof(f60,definition,
( op(e4,e4) != e2
| ( op(e4,e2) = e4
& e2 != unit )
| ~ sP50 ),
introduced(definition,[new_symbols(definition,[sP50])],[predicate_definition_introduction]) ).
fof(f61,definition,
( op(e4,e3) != e2
| ( op(e4,e2) = e3
& e2 != unit )
| ~ sP51 ),
introduced(definition,[new_symbols(definition,[sP51])],[predicate_definition_introduction]) ).
fof(f62,definition,
( op(e4,e2) != e2
| ( op(e4,e2) = e2
& e2 != unit )
| ~ sP52 ),
introduced(definition,[new_symbols(definition,[sP52])],[predicate_definition_introduction]) ).
fof(f63,definition,
( op(e4,e1) != e2
| ( op(e4,e2) = e1
& e2 != unit )
| ~ sP53 ),
introduced(definition,[new_symbols(definition,[sP53])],[predicate_definition_introduction]) ).
fof(f64,definition,
( op(e4,e0) != e2
| ( op(e4,e2) = e0
& e2 != unit )
| ~ sP54 ),
introduced(definition,[new_symbols(definition,[sP54])],[predicate_definition_introduction]) ).
fof(f65,definition,
( op(e3,e4) != e2
| ( op(e3,e2) = e4
& e2 != unit )
| ~ sP55 ),
introduced(definition,[new_symbols(definition,[sP55])],[predicate_definition_introduction]) ).
fof(f66,definition,
( op(e3,e3) != e2
| ( op(e3,e2) = e3
& e2 != unit )
| ~ sP56 ),
introduced(definition,[new_symbols(definition,[sP56])],[predicate_definition_introduction]) ).
fof(f67,definition,
( op(e3,e2) != e2
| ( op(e3,e2) = e2
& e2 != unit )
| ~ sP57 ),
introduced(definition,[new_symbols(definition,[sP57])],[predicate_definition_introduction]) ).
fof(f68,definition,
( op(e3,e1) != e2
| ( op(e3,e2) = e1
& e2 != unit )
| ~ sP58 ),
introduced(definition,[new_symbols(definition,[sP58])],[predicate_definition_introduction]) ).
fof(f69,definition,
( op(e3,e0) != e2
| ( op(e3,e2) = e0
& e2 != unit )
| ~ sP59 ),
introduced(definition,[new_symbols(definition,[sP59])],[predicate_definition_introduction]) ).
fof(f70,definition,
( op(e2,e4) != e2
| ( op(e2,e2) = e4
& e2 != unit )
| ~ sP60 ),
introduced(definition,[new_symbols(definition,[sP60])],[predicate_definition_introduction]) ).
fof(f71,definition,
( op(e2,e3) != e2
| ( op(e2,e2) = e3
& e2 != unit )
| ~ sP61 ),
introduced(definition,[new_symbols(definition,[sP61])],[predicate_definition_introduction]) ).
fof(f72,definition,
( op(e2,e2) != e2
| ( op(e2,e2) = e2
& e2 != unit )
| ~ sP62 ),
introduced(definition,[new_symbols(definition,[sP62])],[predicate_definition_introduction]) ).
fof(f73,definition,
( op(e2,e1) != e2
| ( op(e2,e2) = e1
& e2 != unit )
| ~ sP63 ),
introduced(definition,[new_symbols(definition,[sP63])],[predicate_definition_introduction]) ).
fof(f74,definition,
( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit )
| ~ sP64 ),
introduced(definition,[new_symbols(definition,[sP64])],[predicate_definition_introduction]) ).
fof(f75,definition,
( op(e1,e4) != e2
| ( op(e1,e2) = e4
& e2 != unit )
| ~ sP65 ),
introduced(definition,[new_symbols(definition,[sP65])],[predicate_definition_introduction]) ).
fof(f76,definition,
( op(e1,e3) != e2
| ( op(e1,e2) = e3
& e2 != unit )
| ~ sP66 ),
introduced(definition,[new_symbols(definition,[sP66])],[predicate_definition_introduction]) ).
fof(f77,definition,
( op(e1,e2) != e2
| ( op(e1,e2) = e2
& e2 != unit )
| ~ sP67 ),
introduced(definition,[new_symbols(definition,[sP67])],[predicate_definition_introduction]) ).
fof(f78,definition,
( op(e1,e1) != e2
| ( op(e1,e2) = e1
& e2 != unit )
| ~ sP68 ),
introduced(definition,[new_symbols(definition,[sP68])],[predicate_definition_introduction]) ).
fof(f79,definition,
( op(e1,e0) != e2
| ( op(e1,e2) = e0
& e2 != unit )
| ~ sP69 ),
introduced(definition,[new_symbols(definition,[sP69])],[predicate_definition_introduction]) ).
fof(f80,definition,
( op(e0,e4) != e2
| ( op(e0,e2) = e4
& e2 != unit )
| ~ sP70 ),
introduced(definition,[new_symbols(definition,[sP70])],[predicate_definition_introduction]) ).
fof(f81,definition,
( op(e0,e3) != e2
| ( op(e0,e2) = e3
& e2 != unit )
| ~ sP71 ),
introduced(definition,[new_symbols(definition,[sP71])],[predicate_definition_introduction]) ).
fof(f82,definition,
( op(e0,e2) != e2
| ( op(e0,e2) = e2
& e2 != unit )
| ~ sP72 ),
introduced(definition,[new_symbols(definition,[sP72])],[predicate_definition_introduction]) ).
fof(f83,definition,
( op(e0,e1) != e2
| ( op(e0,e2) = e1
& e2 != unit )
| ~ sP73 ),
introduced(definition,[new_symbols(definition,[sP73])],[predicate_definition_introduction]) ).
fof(f84,definition,
( op(e0,e0) != e2
| ( op(e0,e2) = e0
& e2 != unit )
| ~ sP74 ),
introduced(definition,[new_symbols(definition,[sP74])],[predicate_definition_introduction]) ).
fof(f85,definition,
( op(e4,e4) != e1
| ( op(e4,e1) = e4
& e1 != unit )
| ~ sP75 ),
introduced(definition,[new_symbols(definition,[sP75])],[predicate_definition_introduction]) ).
fof(f86,definition,
( op(e4,e3) != e1
| ( op(e4,e1) = e3
& e1 != unit )
| ~ sP76 ),
introduced(definition,[new_symbols(definition,[sP76])],[predicate_definition_introduction]) ).
fof(f87,definition,
( op(e4,e2) != e1
| ( op(e4,e1) = e2
& e1 != unit )
| ~ sP77 ),
introduced(definition,[new_symbols(definition,[sP77])],[predicate_definition_introduction]) ).
fof(f88,definition,
( op(e4,e1) != e1
| ( op(e4,e1) = e1
& e1 != unit )
| ~ sP78 ),
introduced(definition,[new_symbols(definition,[sP78])],[predicate_definition_introduction]) ).
fof(f89,definition,
( op(e4,e0) != e1
| ( op(e4,e1) = e0
& e1 != unit )
| ~ sP79 ),
introduced(definition,[new_symbols(definition,[sP79])],[predicate_definition_introduction]) ).
fof(f90,definition,
( op(e3,e4) != e1
| ( op(e3,e1) = e4
& e1 != unit )
| ~ sP80 ),
introduced(definition,[new_symbols(definition,[sP80])],[predicate_definition_introduction]) ).
fof(f91,definition,
( op(e3,e3) != e1
| ( op(e3,e1) = e3
& e1 != unit )
| ~ sP81 ),
introduced(definition,[new_symbols(definition,[sP81])],[predicate_definition_introduction]) ).
fof(f92,definition,
( op(e3,e2) != e1
| ( op(e3,e1) = e2
& e1 != unit )
| ~ sP82 ),
introduced(definition,[new_symbols(definition,[sP82])],[predicate_definition_introduction]) ).
fof(f93,definition,
( op(e3,e1) != e1
| ( op(e3,e1) = e1
& e1 != unit )
| ~ sP83 ),
introduced(definition,[new_symbols(definition,[sP83])],[predicate_definition_introduction]) ).
fof(f94,definition,
( op(e3,e0) != e1
| ( op(e3,e1) = e0
& e1 != unit )
| ~ sP84 ),
introduced(definition,[new_symbols(definition,[sP84])],[predicate_definition_introduction]) ).
fof(f95,definition,
( op(e2,e4) != e1
| ( op(e2,e1) = e4
& e1 != unit )
| ~ sP85 ),
introduced(definition,[new_symbols(definition,[sP85])],[predicate_definition_introduction]) ).
fof(f96,definition,
( op(e2,e3) != e1
| ( op(e2,e1) = e3
& e1 != unit )
| ~ sP86 ),
introduced(definition,[new_symbols(definition,[sP86])],[predicate_definition_introduction]) ).
fof(f97,definition,
( op(e2,e2) != e1
| ( op(e2,e1) = e2
& e1 != unit )
| ~ sP87 ),
introduced(definition,[new_symbols(definition,[sP87])],[predicate_definition_introduction]) ).
fof(f98,definition,
( op(e2,e1) != e1
| ( op(e2,e1) = e1
& e1 != unit )
| ~ sP88 ),
introduced(definition,[new_symbols(definition,[sP88])],[predicate_definition_introduction]) ).
fof(f99,definition,
( op(e2,e0) != e1
| ( op(e2,e1) = e0
& e1 != unit )
| ~ sP89 ),
introduced(definition,[new_symbols(definition,[sP89])],[predicate_definition_introduction]) ).
fof(f100,definition,
( op(e1,e4) != e1
| ( op(e1,e1) = e4
& e1 != unit )
| ~ sP90 ),
introduced(definition,[new_symbols(definition,[sP90])],[predicate_definition_introduction]) ).
fof(f101,definition,
( op(e1,e3) != e1
| ( op(e1,e1) = e3
& e1 != unit )
| ~ sP91 ),
introduced(definition,[new_symbols(definition,[sP91])],[predicate_definition_introduction]) ).
fof(f102,definition,
( op(e1,e2) != e1
| ( op(e1,e1) = e2
& e1 != unit )
| ~ sP92 ),
introduced(definition,[new_symbols(definition,[sP92])],[predicate_definition_introduction]) ).
fof(f103,definition,
( op(e1,e1) != e1
| ( op(e1,e1) = e1
& e1 != unit )
| ~ sP93 ),
introduced(definition,[new_symbols(definition,[sP93])],[predicate_definition_introduction]) ).
fof(f104,definition,
( op(e1,e0) != e1
| ( op(e1,e1) = e0
& e1 != unit )
| ~ sP94 ),
introduced(definition,[new_symbols(definition,[sP94])],[predicate_definition_introduction]) ).
fof(f105,definition,
( op(e0,e4) != e1
| ( op(e0,e1) = e4
& e1 != unit )
| ~ sP95 ),
introduced(definition,[new_symbols(definition,[sP95])],[predicate_definition_introduction]) ).
fof(f106,definition,
( op(e0,e3) != e1
| ( op(e0,e1) = e3
& e1 != unit )
| ~ sP96 ),
introduced(definition,[new_symbols(definition,[sP96])],[predicate_definition_introduction]) ).
fof(f107,definition,
( op(e0,e2) != e1
| ( op(e0,e1) = e2
& e1 != unit )
| ~ sP97 ),
introduced(definition,[new_symbols(definition,[sP97])],[predicate_definition_introduction]) ).
fof(f108,definition,
( op(e0,e1) != e1
| ( op(e0,e1) = e1
& e1 != unit )
| ~ sP98 ),
introduced(definition,[new_symbols(definition,[sP98])],[predicate_definition_introduction]) ).
fof(f109,definition,
( op(e0,e0) != e1
| ( op(e0,e1) = e0
& e1 != unit )
| ~ sP99 ),
introduced(definition,[new_symbols(definition,[sP99])],[predicate_definition_introduction]) ).
fof(f110,definition,
( op(e4,e4) != e0
| ( op(e4,e0) = e4
& e0 != unit )
| ~ sP100 ),
introduced(definition,[new_symbols(definition,[sP100])],[predicate_definition_introduction]) ).
fof(f111,definition,
( op(e4,e3) != e0
| ( op(e4,e0) = e3
& e0 != unit )
| ~ sP101 ),
introduced(definition,[new_symbols(definition,[sP101])],[predicate_definition_introduction]) ).
fof(f112,definition,
( op(e4,e2) != e0
| ( op(e4,e0) = e2
& e0 != unit )
| ~ sP102 ),
introduced(definition,[new_symbols(definition,[sP102])],[predicate_definition_introduction]) ).
fof(f113,definition,
( op(e4,e1) != e0
| ( op(e4,e0) = e1
& e0 != unit )
| ~ sP103 ),
introduced(definition,[new_symbols(definition,[sP103])],[predicate_definition_introduction]) ).
fof(f114,definition,
( op(e4,e0) != e0
| ( op(e4,e0) = e0
& e0 != unit )
| ~ sP104 ),
introduced(definition,[new_symbols(definition,[sP104])],[predicate_definition_introduction]) ).
fof(f115,definition,
( op(e3,e4) != e0
| ( op(e3,e0) = e4
& e0 != unit )
| ~ sP105 ),
introduced(definition,[new_symbols(definition,[sP105])],[predicate_definition_introduction]) ).
fof(f116,definition,
( op(e3,e3) != e0
| ( op(e3,e0) = e3
& e0 != unit )
| ~ sP106 ),
introduced(definition,[new_symbols(definition,[sP106])],[predicate_definition_introduction]) ).
fof(f117,definition,
( op(e3,e2) != e0
| ( op(e3,e0) = e2
& e0 != unit )
| ~ sP107 ),
introduced(definition,[new_symbols(definition,[sP107])],[predicate_definition_introduction]) ).
fof(f118,definition,
( op(e3,e1) != e0
| ( op(e3,e0) = e1
& e0 != unit )
| ~ sP108 ),
introduced(definition,[new_symbols(definition,[sP108])],[predicate_definition_introduction]) ).
fof(f119,definition,
( op(e3,e0) != e0
| ( op(e3,e0) = e0
& e0 != unit )
| ~ sP109 ),
introduced(definition,[new_symbols(definition,[sP109])],[predicate_definition_introduction]) ).
fof(f120,definition,
( op(e2,e4) != e0
| ( op(e2,e0) = e4
& e0 != unit )
| ~ sP110 ),
introduced(definition,[new_symbols(definition,[sP110])],[predicate_definition_introduction]) ).
fof(f121,definition,
( op(e2,e3) != e0
| ( op(e2,e0) = e3
& e0 != unit )
| ~ sP111 ),
introduced(definition,[new_symbols(definition,[sP111])],[predicate_definition_introduction]) ).
fof(f122,definition,
( op(e2,e2) != e0
| ( op(e2,e0) = e2
& e0 != unit )
| ~ sP112 ),
introduced(definition,[new_symbols(definition,[sP112])],[predicate_definition_introduction]) ).
fof(f123,definition,
( op(e2,e1) != e0
| ( op(e2,e0) = e1
& e0 != unit )
| ~ sP113 ),
introduced(definition,[new_symbols(definition,[sP113])],[predicate_definition_introduction]) ).
fof(f124,definition,
( op(e2,e0) != e0
| ( op(e2,e0) = e0
& e0 != unit )
| ~ sP114 ),
introduced(definition,[new_symbols(definition,[sP114])],[predicate_definition_introduction]) ).
fof(f125,definition,
( op(e1,e4) != e0
| ( op(e1,e0) = e4
& e0 != unit )
| ~ sP115 ),
introduced(definition,[new_symbols(definition,[sP115])],[predicate_definition_introduction]) ).
fof(f126,definition,
( op(e1,e3) != e0
| ( op(e1,e0) = e3
& e0 != unit )
| ~ sP116 ),
introduced(definition,[new_symbols(definition,[sP116])],[predicate_definition_introduction]) ).
fof(f127,definition,
( op(e1,e2) != e0
| ( op(e1,e0) = e2
& e0 != unit )
| ~ sP117 ),
introduced(definition,[new_symbols(definition,[sP117])],[predicate_definition_introduction]) ).
fof(f128,definition,
( op(e1,e1) != e0
| ( op(e1,e0) = e1
& e0 != unit )
| ~ sP118 ),
introduced(definition,[new_symbols(definition,[sP118])],[predicate_definition_introduction]) ).
fof(f129,definition,
( op(e1,e0) != e0
| ( op(e1,e0) = e0
& e0 != unit )
| ~ sP119 ),
introduced(definition,[new_symbols(definition,[sP119])],[predicate_definition_introduction]) ).
fof(f130,definition,
( op(e0,e4) != e0
| ( op(e0,e0) = e4
& e0 != unit )
| ~ sP120 ),
introduced(definition,[new_symbols(definition,[sP120])],[predicate_definition_introduction]) ).
fof(f131,definition,
( op(e0,e3) != e0
| ( op(e0,e0) = e3
& e0 != unit )
| ~ sP121 ),
introduced(definition,[new_symbols(definition,[sP121])],[predicate_definition_introduction]) ).
fof(f132,definition,
( op(e0,e2) != e0
| ( op(e0,e0) = e2
& e0 != unit )
| ~ sP122 ),
introduced(definition,[new_symbols(definition,[sP122])],[predicate_definition_introduction]) ).
fof(f133,definition,
( op(e0,e1) != e0
| ( op(e0,e0) = e1
& e0 != unit )
| ~ sP123 ),
introduced(definition,[new_symbols(definition,[sP123])],[predicate_definition_introduction]) ).
fof(f134,definition,
( op(e0,e0) != e0
| ( op(e0,e0) = e0
& e0 != unit )
| ~ sP124 ),
introduced(definition,[new_symbols(definition,[sP124])],[predicate_definition_introduction]) ).
fof(f135,definition,
( ( sP24
& sP23
& sP22
& sP21
& sP20
& sP19
& sP18
& sP17
& sP16
& sP15
& sP14
& sP13
& sP12
& sP11
& sP10
& sP9
& sP8
& sP7
& sP6
& sP5
& sP4
& sP3
& sP2
& sP1
& sP0 )
| ~ sP125 ),
introduced(definition,[new_symbols(definition,[sP125])],[predicate_definition_introduction]) ).
fof(f136,definition,
( ( sP49
& sP48
& sP47
& sP46
& sP45
& sP44
& sP43
& sP42
& sP41
& sP40
& sP39
& sP38
& sP37
& sP36
& sP35
& sP34
& sP33
& sP32
& sP31
& sP30
& sP29
& sP28
& sP27
& sP26
& sP25 )
| ~ sP126 ),
introduced(definition,[new_symbols(definition,[sP126])],[predicate_definition_introduction]) ).
fof(f137,definition,
( ( sP74
& sP73
& sP72
& sP71
& sP70
& sP69
& sP68
& sP67
& sP66
& sP65
& sP64
& sP63
& sP62
& sP61
& sP60
& sP59
& sP58
& sP57
& sP56
& sP55
& sP54
& sP53
& sP52
& sP51
& sP50 )
| ~ sP127 ),
introduced(definition,[new_symbols(definition,[sP127])],[predicate_definition_introduction]) ).
fof(f138,definition,
( ( sP99
& sP98
& sP97
& sP96
& sP95
& sP94
& sP93
& sP92
& sP91
& sP90
& sP89
& sP88
& sP87
& sP86
& sP85
& sP84
& sP83
& sP82
& sP81
& sP80
& sP79
& sP78
& sP77
& sP76
& sP75 )
| ~ sP128 ),
introduced(definition,[new_symbols(definition,[sP128])],[predicate_definition_introduction]) ).
fof(f139,definition,
( ( sP124
& sP123
& sP122
& sP121
& sP120
& sP119
& sP118
& sP117
& sP116
& sP115
& sP114
& sP113
& sP112
& sP111
& sP110
& sP109
& sP108
& sP107
& sP106
& sP105
& sP104
& sP103
& sP102
& sP101
& sP100 )
| ~ sP129 ),
introduced(definition,[new_symbols(definition,[sP129])],[predicate_definition_introduction]) ).
fof(f140,definition,
( ( op(e4,op(e4,e4)) != e4
& op(e4,op(e4,e4)) = e4 )
| ~ sP130 ),
introduced(definition,[new_symbols(definition,[sP130])],[predicate_definition_introduction]) ).
fof(f141,definition,
( ( op(e3,op(e3,e4)) != e4
& op(e4,op(e3,e4)) = e3 )
| ~ sP131 ),
introduced(definition,[new_symbols(definition,[sP131])],[predicate_definition_introduction]) ).
fof(f142,definition,
( ( op(e4,op(e4,e3)) != e3
& op(e3,op(e4,e3)) = e4 )
| ~ sP132 ),
introduced(definition,[new_symbols(definition,[sP132])],[predicate_definition_introduction]) ).
fof(f143,definition,
( ( op(e3,op(e3,e3)) != e3
& op(e3,op(e3,e3)) = e3 )
| ~ sP133 ),
introduced(definition,[new_symbols(definition,[sP133])],[predicate_definition_introduction]) ).
fof(f144,definition,
( ( op(e4,op(e4,e2)) != e2
& op(e2,op(e4,e2)) = e4 )
| ~ sP134 ),
introduced(definition,[new_symbols(definition,[sP134])],[predicate_definition_introduction]) ).
fof(f145,definition,
( ( op(e3,op(e3,e2)) != e2
& op(e2,op(e3,e2)) = e3 )
| ~ sP135 ),
introduced(definition,[new_symbols(definition,[sP135])],[predicate_definition_introduction]) ).
fof(f146,definition,
( ( op(e4,op(e4,e1)) != e1
& op(e1,op(e4,e1)) = e4 )
| ~ sP136 ),
introduced(definition,[new_symbols(definition,[sP136])],[predicate_definition_introduction]) ).
fof(f147,definition,
( ( op(e3,op(e3,e1)) != e1
& op(e1,op(e3,e1)) = e3 )
| ~ sP137 ),
introduced(definition,[new_symbols(definition,[sP137])],[predicate_definition_introduction]) ).
fof(f148,definition,
( ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 )
| ~ sP138 ),
introduced(definition,[new_symbols(definition,[sP138])],[predicate_definition_introduction]) ).
fof(f149,definition,
( ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ~ sP139 ),
introduced(definition,[new_symbols(definition,[sP139])],[predicate_definition_introduction]) ).
fof(f150,plain,
( ( ( op(e0,op(e0,e0)) != e0
& op(e0,op(e0,e0)) = e0 )
| ( op(e1,op(e1,e0)) != e0
& op(e0,op(e1,e0)) = e1 )
| ( op(e2,op(e2,e0)) != e0
& op(e0,op(e2,e0)) = e2 )
| sP139
| sP138 )
& ( ( op(e0,op(e0,e1)) != e1
& op(e1,op(e0,e1)) = e0 )
| ( op(e1,op(e1,e1)) != e1
& op(e1,op(e1,e1)) = e1 )
| ( op(e2,op(e2,e1)) != e1
& op(e1,op(e2,e1)) = e2 )
| sP137
| sP136 )
& ( ( op(e0,op(e0,e2)) != e2
& op(e2,op(e0,e2)) = e0 )
| ( op(e1,op(e1,e2)) != e2
& op(e2,op(e1,e2)) = e1 )
| ( op(e2,op(e2,e2)) != e2
& op(e2,op(e2,e2)) = e2 )
| sP135
| sP134 )
& ( ( op(e0,op(e0,e3)) != e3
& op(e3,op(e0,e3)) = e0 )
| ( op(e1,op(e1,e3)) != e3
& op(e3,op(e1,e3)) = e1 )
| ( op(e2,op(e2,e3)) != e3
& op(e3,op(e2,e3)) = e2 )
| sP133
| sP132 )
& ( ( op(e0,op(e0,e4)) != e4
& op(e4,op(e0,e4)) = e0 )
| ( op(e1,op(e1,e4)) != e4
& op(e4,op(e1,e4)) = e1 )
| ( op(e2,op(e2,e4)) != e4
& op(e4,op(e2,e4)) = e2 )
| sP131
| sP130 )
& ( sP129
| sP128
| sP127
| sP126
| sP125 ) ),
inference(definition_folding,[],[f9,f149,f148,f147,f146,f145,f144,f143,f142,f141,f140,f139,f138,f137,f136,f135,f134,f133,f132,f131,f130,f129,f128,f127,f126,f125,f124,f123,f122,f121,f120,f119,f118,f117,f116,f115,f114,f113,f112,f111,f110,f109,f108,f107,f106,f105,f104,f103,f102,f101,f100,f99,f98,f97,f96,f95,f94,f93,f92,f91,f90,f89,f88,f87,f86,f85,f84,f83,f82,f81,f80,f79,f78,f77,f76,f75,f74,f73,f72,f71,f70,f69,f68,f67,f66,f65,f64,f63,f62,f61,f60,f59,f58,f57,f56,f55,f54,f53,f52,f51,f50,f49,f48,f47,f46,f45,f44,f43,f42,f41,f40,f39,f38,f37,f36,f35,f34,f33,f32,f31,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10]) ).
fof(f161,plain,
( ( sP124
& sP123
& sP122
& sP121
& sP120
& sP119
& sP118
& sP117
& sP116
& sP115
& sP114
& sP113
& sP112
& sP111
& sP110
& sP109
& sP108
& sP107
& sP106
& sP105
& sP104
& sP103
& sP102
& sP101
& sP100 )
| ~ sP129 ),
inference(nnf_transformation,[],[f139]) ).
fof(f162,plain,
( ( sP99
& sP98
& sP97
& sP96
& sP95
& sP94
& sP93
& sP92
& sP91
& sP90
& sP89
& sP88
& sP87
& sP86
& sP85
& sP84
& sP83
& sP82
& sP81
& sP80
& sP79
& sP78
& sP77
& sP76
& sP75 )
| ~ sP128 ),
inference(nnf_transformation,[],[f138]) ).
fof(f163,plain,
( ( sP74
& sP73
& sP72
& sP71
& sP70
& sP69
& sP68
& sP67
& sP66
& sP65
& sP64
& sP63
& sP62
& sP61
& sP60
& sP59
& sP58
& sP57
& sP56
& sP55
& sP54
& sP53
& sP52
& sP51
& sP50 )
| ~ sP127 ),
inference(nnf_transformation,[],[f137]) ).
fof(f164,plain,
( ( sP49
& sP48
& sP47
& sP46
& sP45
& sP44
& sP43
& sP42
& sP41
& sP40
& sP39
& sP38
& sP37
& sP36
& sP35
& sP34
& sP33
& sP32
& sP31
& sP30
& sP29
& sP28
& sP27
& sP26
& sP25 )
| ~ sP126 ),
inference(nnf_transformation,[],[f136]) ).
fof(f165,plain,
( ( sP24
& sP23
& sP22
& sP21
& sP20
& sP19
& sP18
& sP17
& sP16
& sP15
& sP14
& sP13
& sP12
& sP11
& sP10
& sP9
& sP8
& sP7
& sP6
& sP5
& sP4
& sP3
& sP2
& sP1
& sP0 )
| ~ sP125 ),
inference(nnf_transformation,[],[f135]) ).
fof(f190,plain,
( op(e4,e4) != e0
| ( op(e4,e0) = e4
& e0 != unit )
| ~ sP100 ),
inference(nnf_transformation,[],[f110]) ).
fof(f210,plain,
( op(e3,e4) != e1
| ( op(e3,e1) = e4
& e1 != unit )
| ~ sP80 ),
inference(nnf_transformation,[],[f90]) ).
fof(f213,plain,
( op(e4,e2) != e1
| ( op(e4,e1) = e2
& e1 != unit )
| ~ sP77 ),
inference(nnf_transformation,[],[f87]) ).
fof(f214,plain,
( op(e4,e3) != e1
| ( op(e4,e1) = e3
& e1 != unit )
| ~ sP76 ),
inference(nnf_transformation,[],[f86]) ).
fof(f226,plain,
( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit )
| ~ sP64 ),
inference(nnf_transformation,[],[f74]) ).
fof(f227,plain,
( op(e2,e1) != e2
| ( op(e2,e2) = e1
& e2 != unit )
| ~ sP63 ),
inference(nnf_transformation,[],[f73]) ).
fof(f255,plain,
( op(e2,e4) != e3
| ( op(e2,e3) = e4
& e3 != unit )
| ~ sP35 ),
inference(nnf_transformation,[],[f45]) ).
fof(f278,plain,
( op(e2,e2) != e4
| ( op(e2,e4) = e2
& e4 != unit )
| ~ sP12 ),
inference(nnf_transformation,[],[f22]) ).
fof(f292,plain,
( e0 = op(e4,e3)
| e1 = op(e4,e3)
| e2 = op(e4,e3)
| e3 = op(e4,e3)
| e4 = op(e4,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f293,plain,
( e0 = op(e4,e2)
| e1 = op(e4,e2)
| e2 = op(e4,e2)
| e3 = op(e4,e2)
| e4 = op(e4,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f294,plain,
( e0 = op(e4,e1)
| e1 = op(e4,e1)
| e2 = op(e4,e1)
| e3 = op(e4,e1)
| e4 = op(e4,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f316,plain,
( e0 = unit
| e1 = unit
| e2 = unit
| e3 = unit
| e4 = unit ),
inference(cnf_transformation,[],[f2]) ).
fof(f317,plain,
e4 = op(e4,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f318,plain,
e4 = op(unit,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f320,plain,
e3 = op(unit,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f321,plain,
e2 = op(e2,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f322,plain,
e2 = op(unit,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f324,plain,
e1 = op(unit,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f377,plain,
op(e4,e3) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f378,plain,
op(e4,e2) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f380,plain,
op(e4,e1) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f381,plain,
op(e4,e1) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f382,plain,
op(e4,e1) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f384,plain,
op(e4,e0) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f385,plain,
op(e4,e0) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f386,plain,
op(e4,e0) != op(e4,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f399,plain,
op(e2,e2) != op(e2,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f443,plain,
op(e0,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f453,plain,
op(e0,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f463,plain,
op(e0,e1) != op(e4,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f477,plain,
e3 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f479,plain,
e2 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f480,plain,
e1 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f483,plain,
e0 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f487,plain,
e4 = op(e2,e2),
inference(cnf_transformation,[],[f6]) ).
fof(f488,plain,
e3 = op(e2,op(e2,e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f489,plain,
e1 = op(op(e2,op(e2,e2)),op(e2,e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f490,plain,
e0 = op(op(e2,e2),op(e2,e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f511,plain,
( sP100
| ~ sP129 ),
inference(cnf_transformation,[],[f161]) ).
fof(f537,plain,
( sP76
| ~ sP128 ),
inference(cnf_transformation,[],[f162]) ).
fof(f538,plain,
( sP77
| ~ sP128 ),
inference(cnf_transformation,[],[f162]) ).
fof(f541,plain,
( sP80
| ~ sP128 ),
inference(cnf_transformation,[],[f162]) ).
fof(f574,plain,
( sP63
| ~ sP127 ),
inference(cnf_transformation,[],[f163]) ).
fof(f575,plain,
( sP64
| ~ sP127 ),
inference(cnf_transformation,[],[f163]) ).
fof(f596,plain,
( sP35
| ~ sP126 ),
inference(cnf_transformation,[],[f164]) ).
fof(f623,plain,
( sP12
| ~ sP125 ),
inference(cnf_transformation,[],[f165]) ).
fof(f684,plain,
( e0 != op(e4,e4)
| e0 != unit
| ~ sP100 ),
inference(cnf_transformation,[],[f190]) ).
fof(f685,plain,
( e0 != op(e4,e4)
| e4 = op(e4,e0)
| ~ sP100 ),
inference(cnf_transformation,[],[f190]) ).
fof(f724,plain,
( e1 != op(e3,e4)
| e1 != unit
| ~ sP80 ),
inference(cnf_transformation,[],[f210]) ).
fof(f731,plain,
( e1 != op(e4,e2)
| e2 = op(e4,e1)
| ~ sP77 ),
inference(cnf_transformation,[],[f213]) ).
fof(f733,plain,
( e1 != op(e4,e3)
| e3 = op(e4,e1)
| ~ sP76 ),
inference(cnf_transformation,[],[f214]) ).
fof(f757,plain,
( e2 != op(e2,e0)
| e0 = op(e2,e2)
| ~ sP64 ),
inference(cnf_transformation,[],[f226]) ).
fof(f759,plain,
( e2 != op(e2,e1)
| e1 = op(e2,e2)
| ~ sP63 ),
inference(cnf_transformation,[],[f227]) ).
fof(f815,plain,
( e3 != op(e2,e4)
| e4 = op(e2,e3)
| ~ sP35 ),
inference(cnf_transformation,[],[f255]) ).
fof(f861,plain,
( e4 != op(e2,e2)
| e2 = op(e2,e4)
| ~ sP12 ),
inference(cnf_transformation,[],[f278]) ).
fof(f886,plain,
( sP129
| sP128
| sP127
| sP126
| sP125 ),
inference(cnf_transformation,[],[f150]) ).
fof(f933,plain,
e4 = op(e2,e2),
inference(global_subsumption,[],[f487]) ).
fof(f937,definition,
( spl140_1
<=> sP125 ),
introduced(definition,[new_symbols(definition,[spl140_1])],[avatar_definition]) ).
fof(f941,definition,
( spl140_2
<=> sP126 ),
introduced(definition,[new_symbols(definition,[spl140_2])],[avatar_definition]) ).
fof(f945,definition,
( spl140_3
<=> sP127 ),
introduced(definition,[new_symbols(definition,[spl140_3])],[avatar_definition]) ).
fof(f949,definition,
( spl140_4
<=> sP128 ),
introduced(definition,[new_symbols(definition,[spl140_4])],[avatar_definition]) ).
fof(f953,definition,
( spl140_5
<=> sP129 ),
introduced(definition,[new_symbols(definition,[spl140_5])],[avatar_definition]) ).
fof(f956,plain,
( spl140_1
| spl140_2
| spl140_3
| spl140_4
| spl140_5 ),
inference(avatar_split_clause,[],[f886,f953,f949,f945,f941,f937]) ).
fof(f1034,definition,
( spl140_23
<=> e0 = unit ),
introduced(definition,[new_symbols(definition,[spl140_23])],[avatar_definition]) ).
fof(f1035,plain,
( e0 = unit
| ~ spl140_23 ),
inference(avatar_component_clause,[],[f1034]) ).
fof(f1036,plain,
( e0 != unit
| spl140_23 ),
inference(avatar_component_clause,[],[f1034]) ).
fof(f1056,definition,
( spl140_28
<=> e1 = unit ),
introduced(definition,[new_symbols(definition,[spl140_28])],[avatar_definition]) ).
fof(f1057,plain,
( e1 = unit
| ~ spl140_28 ),
inference(avatar_component_clause,[],[f1056]) ).
fof(f1058,plain,
( e1 != unit
| spl140_28 ),
inference(avatar_component_clause,[],[f1056]) ).
fof(f1069,definition,
( spl140_31
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl140_31])],[avatar_definition]) ).
fof(f1070,plain,
( e1 = op(e0,e1)
| ~ spl140_31 ),
inference(avatar_component_clause,[],[f1069]) ).
fof(f1071,plain,
( e1 != op(e0,e1)
| spl140_31 ),
inference(avatar_component_clause,[],[f1069]) ).
fof(f1078,definition,
( spl140_33
<=> e2 = unit ),
introduced(definition,[new_symbols(definition,[spl140_33])],[avatar_definition]) ).
fof(f1079,plain,
( e2 = unit
| ~ spl140_33 ),
inference(avatar_component_clause,[],[f1078]) ).
fof(f1080,plain,
( e2 != unit
| spl140_33 ),
inference(avatar_component_clause,[],[f1078]) ).
fof(f1100,definition,
( spl140_38
<=> e3 = unit ),
introduced(definition,[new_symbols(definition,[spl140_38])],[avatar_definition]) ).
fof(f1101,plain,
( e3 = unit
| ~ spl140_38 ),
inference(avatar_component_clause,[],[f1100]) ).
fof(f1102,plain,
( e3 != unit
| spl140_38 ),
inference(avatar_component_clause,[],[f1100]) ).
fof(f1122,definition,
( spl140_43
<=> e4 = unit ),
introduced(definition,[new_symbols(definition,[spl140_43])],[avatar_definition]) ).
fof(f1123,plain,
( e4 = unit
| ~ spl140_43 ),
inference(avatar_component_clause,[],[f1122]) ).
fof(f1124,plain,
( e4 != unit
| spl140_43 ),
inference(avatar_component_clause,[],[f1122]) ).
fof(f1167,definition,
( spl140_51
<=> sP100 ),
introduced(definition,[new_symbols(definition,[spl140_51])],[avatar_definition]) ).
fof(f1169,plain,
( sP100
| ~ spl140_51 ),
inference(avatar_component_clause,[],[f1167]) ).
fof(f1170,plain,
( ~ spl140_5
| spl140_51 ),
inference(avatar_split_clause,[],[f511,f1167,f953]) ).
fof(f1172,definition,
( spl140_52
<=> e2 = op(e4,op(e2,e4)) ),
introduced(definition,[new_symbols(definition,[spl140_52])],[avatar_definition]) ).
fof(f1173,plain,
( e2 != op(e4,op(e2,e4))
| spl140_52 ),
inference(avatar_component_clause,[],[f1172]) ).
fof(f1174,plain,
( e2 = op(e4,op(e2,e4))
| ~ spl140_52 ),
inference(avatar_component_clause,[],[f1172]) ).
fof(f1187,definition,
( spl140_55
<=> e4 = op(e2,op(e2,e4)) ),
introduced(definition,[new_symbols(definition,[spl140_55])],[avatar_definition]) ).
fof(f1188,plain,
( e4 = op(e2,op(e2,e4))
| ~ spl140_55 ),
inference(avatar_component_clause,[],[f1187]) ).
fof(f1189,plain,
( e4 != op(e2,op(e2,e4))
| spl140_55 ),
inference(avatar_component_clause,[],[f1187]) ).
fof(f1304,definition,
( spl140_76
<=> e2 = op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl140_76])],[avatar_definition]) ).
fof(f1305,plain,
( e2 != op(e2,op(e2,e2))
| spl140_76 ),
inference(avatar_component_clause,[],[f1304]) ).
fof(f1306,plain,
( e2 = op(e2,op(e2,e2))
| ~ spl140_76 ),
inference(avatar_component_clause,[],[f1304]) ).
fof(f1445,definition,
( spl140_97
<=> sP76 ),
introduced(definition,[new_symbols(definition,[spl140_97])],[avatar_definition]) ).
fof(f1447,plain,
( sP76
| ~ spl140_97 ),
inference(avatar_component_clause,[],[f1445]) ).
fof(f1448,plain,
( ~ spl140_4
| spl140_97 ),
inference(avatar_split_clause,[],[f537,f1445,f949]) ).
fof(f1450,definition,
( spl140_98
<=> sP77 ),
introduced(definition,[new_symbols(definition,[spl140_98])],[avatar_definition]) ).
fof(f1452,plain,
( sP77
| ~ spl140_98 ),
inference(avatar_component_clause,[],[f1450]) ).
fof(f1453,plain,
( ~ spl140_4
| spl140_98 ),
inference(avatar_split_clause,[],[f538,f1450,f949]) ).
fof(f1465,definition,
( spl140_101
<=> sP80 ),
introduced(definition,[new_symbols(definition,[spl140_101])],[avatar_definition]) ).
fof(f1467,plain,
( sP80
| ~ spl140_101 ),
inference(avatar_component_clause,[],[f1465]) ).
fof(f1468,plain,
( ~ spl140_4
| spl140_101 ),
inference(avatar_split_clause,[],[f541,f1465,f949]) ).
fof(f1623,definition,
( spl140_132
<=> sP63 ),
introduced(definition,[new_symbols(definition,[spl140_132])],[avatar_definition]) ).
fof(f1625,plain,
( sP63
| ~ spl140_132 ),
inference(avatar_component_clause,[],[f1623]) ).
fof(f1626,plain,
( ~ spl140_3
| spl140_132 ),
inference(avatar_split_clause,[],[f574,f1623,f945]) ).
fof(f1628,definition,
( spl140_133
<=> sP64 ),
introduced(definition,[new_symbols(definition,[spl140_133])],[avatar_definition]) ).
fof(f1630,plain,
( sP64
| ~ spl140_133 ),
inference(avatar_component_clause,[],[f1628]) ).
fof(f1631,plain,
( ~ spl140_3
| spl140_133 ),
inference(avatar_split_clause,[],[f575,f1628,f945]) ).
fof(f1724,definition,
( spl140_152
<=> sP35 ),
introduced(definition,[new_symbols(definition,[spl140_152])],[avatar_definition]) ).
fof(f1727,plain,
( ~ spl140_2
| spl140_152 ),
inference(avatar_split_clause,[],[f596,f1724,f941]) ).
fof(f1817,plain,
( e2 = e3
| ~ spl140_76 ),
inference(forward_demodulation,[],[f488,f1306]) ).
fof(f1818,plain,
( $false
| ~ spl140_76 ),
inference(forward_subsumption_resolution,[],[f1817,f479]) ).
fof(f1819,plain,
~ spl140_76,
inference(avatar_contradiction_clause,[],[f1818]) ).
fof(f1820,plain,
( e2 != op(e2,e4)
| spl140_76 ),
inference(forward_demodulation,[],[f1305,f933]) ).
fof(f1821,plain,
e3 = op(e2,e4),
inference(forward_demodulation,[],[f488,f933]) ).
fof(f1827,plain,
( e4 = op(e2,e3)
| ~ spl140_55 ),
inference(superposition,[],[f1188,f1821]) ).
fof(f1837,plain,
( e4 != op(e2,e2)
| ~ spl140_55 ),
inference(superposition,[],[f399,f1827]) ).
fof(f1846,plain,
( $false
| ~ spl140_55 ),
inference(forward_subsumption_resolution,[],[f1837,f933]) ).
fof(f1847,plain,
~ spl140_55,
inference(avatar_contradiction_clause,[],[f1846]) ).
fof(f1848,plain,
( e4 != op(e2,e3)
| spl140_55 ),
inference(forward_demodulation,[],[f1189,f1821]) ).
fof(f1849,plain,
e0 = op(e4,e4),
inference(forward_demodulation,[],[f490,f933]) ).
fof(f1850,plain,
e0 != op(e4,e3),
inference(superposition,[],[f377,f1849]) ).
fof(f1851,plain,
e0 != op(e4,e2),
inference(superposition,[],[f378,f1849]) ).
fof(f1852,plain,
e0 != op(e4,e1),
inference(superposition,[],[f380,f1849]) ).
fof(f1860,plain,
e1 = op(op(e2,e4),e4),
inference(forward_demodulation,[],[f489,f933]) ).
fof(f1861,plain,
e1 = op(e3,e4),
inference(forward_demodulation,[],[f1860,f1821]) ).
fof(f1947,plain,
( e4 = op(e4,e0)
| ~ sP100 ),
inference(forward_subsumption_resolution,[],[f685,f1849]) ).
fof(f1948,plain,
( e4 = op(e4,e0)
| ~ spl140_51 ),
inference(forward_subsumption_resolution,[],[f1947,f1169]) ).
fof(f2017,plain,
( e1 != op(e4,e3)
| e3 = op(e4,e1)
| ~ spl140_97 ),
inference(forward_subsumption_resolution,[],[f733,f1447]) ).
fof(f2064,plain,
( e2 != op(e2,e1)
| e1 = op(e2,e2)
| ~ spl140_132 ),
inference(forward_subsumption_resolution,[],[f759,f1625]) ).
fof(f2065,plain,
( e1 = e4
| e2 != op(e2,e1)
| ~ spl140_132 ),
inference(forward_demodulation,[],[f2064,f933]) ).
fof(f2066,plain,
( e2 != op(e2,e1)
| ~ spl140_132 ),
inference(forward_subsumption_resolution,[],[f2065,f480]) ).
fof(f2144,plain,
( e4 = op(e2,e3)
| ~ sP35 ),
inference(forward_subsumption_resolution,[],[f815,f1821]) ).
fof(f2145,plain,
( ~ sP35
| spl140_55 ),
inference(forward_subsumption_resolution,[],[f2144,f1848]) ).
fof(f2148,plain,
( ~ spl140_152
| spl140_55 ),
inference(avatar_split_clause,[],[f2145,f1187,f1724]) ).
fof(f2174,plain,
( e2 = op(e2,e4)
| ~ sP12 ),
inference(forward_subsumption_resolution,[],[f861,f933]) ).
fof(f2175,plain,
( ~ sP12
| spl140_76 ),
inference(forward_subsumption_resolution,[],[f2174,f1820]) ).
fof(f2196,definition,
( spl140_187
<=> e4 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl140_187])],[avatar_definition]) ).
fof(f2197,plain,
( e4 = op(e4,e1)
| ~ spl140_187 ),
inference(avatar_component_clause,[],[f2196]) ).
fof(f2198,plain,
( e4 != op(e4,e1)
| spl140_187 ),
inference(avatar_component_clause,[],[f2196]) ).
fof(f2201,plain,
( e1 = unit
| e2 = unit
| e3 = unit
| e4 = unit
| spl140_23 ),
inference(forward_subsumption_resolution,[],[f316,f1036]) ).
fof(f2202,plain,
( e2 = unit
| e3 = unit
| e4 = unit
| spl140_23
| spl140_28 ),
inference(forward_subsumption_resolution,[],[f2201,f1058]) ).
fof(f2203,plain,
( e3 = unit
| e4 = unit
| spl140_23
| spl140_28
| spl140_33 ),
inference(forward_subsumption_resolution,[],[f2202,f1080]) ).
fof(f2204,plain,
( e4 = unit
| spl140_23
| spl140_28
| spl140_33
| spl140_38 ),
inference(forward_subsumption_resolution,[],[f2203,f1102]) ).
fof(f2205,plain,
( $false
| spl140_23
| spl140_28
| spl140_33
| spl140_38
| spl140_43 ),
inference(forward_subsumption_resolution,[],[f2204,f1124]) ).
fof(f2206,plain,
( spl140_23
| spl140_28
| spl140_33
| spl140_38
| spl140_43 ),
inference(avatar_contradiction_clause,[],[f2205]) ).
fof(f2215,plain,
( e0 != unit
| ~ sP100 ),
inference(forward_subsumption_resolution,[],[f684,f1849]) ).
fof(f2223,plain,
( e0 != unit
| ~ spl140_51 ),
inference(forward_subsumption_resolution,[],[f2215,f1169]) ).
fof(f2227,plain,
( ~ spl140_23
| ~ spl140_51 ),
inference(avatar_split_clause,[],[f2223,f1167,f1034]) ).
fof(f2232,plain,
( e1 != unit
| ~ sP80 ),
inference(forward_subsumption_resolution,[],[f724,f1861]) ).
fof(f2241,plain,
( e1 != unit
| ~ spl140_101 ),
inference(forward_subsumption_resolution,[],[f2232,f1467]) ).
fof(f2247,plain,
( ~ spl140_28
| ~ spl140_101 ),
inference(avatar_split_clause,[],[f2241,f1465,f1056]) ).
fof(f2330,plain,
( e4 = op(e4,e4)
| ~ spl140_43 ),
inference(superposition,[],[f317,f1123]) ).
fof(f2357,plain,
( e0 = e4
| ~ spl140_43 ),
inference(forward_demodulation,[],[f2330,f1849]) ).
fof(f2364,plain,
( $false
| ~ spl140_43 ),
inference(forward_subsumption_resolution,[],[f2357,f483]) ).
fof(f2365,plain,
~ spl140_43,
inference(avatar_contradiction_clause,[],[f2364]) ).
fof(f2366,plain,
( e2 != op(e4,e3)
| spl140_52 ),
inference(forward_demodulation,[],[f1173,f1821]) ).
fof(f2368,plain,
( e1 != op(e4,e2)
| e2 = op(e4,e1)
| ~ spl140_98 ),
inference(forward_subsumption_resolution,[],[f731,f1452]) ).
fof(f2405,definition,
( spl140_195
<=> e4 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl140_195])],[avatar_definition]) ).
fof(f2406,plain,
( e4 = op(e4,e3)
| ~ spl140_195 ),
inference(avatar_component_clause,[],[f2405]) ).
fof(f2410,definition,
( spl140_196
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl140_196])],[avatar_definition]) ).
fof(f2411,plain,
( e2 = op(e0,e2)
| ~ spl140_196 ),
inference(avatar_component_clause,[],[f2410]) ).
fof(f2412,plain,
( e2 != op(e0,e2)
| spl140_196 ),
inference(avatar_component_clause,[],[f2410]) ).
fof(f2430,definition,
( spl140_200
<=> e2 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl140_200])],[avatar_definition]) ).
fof(f2432,plain,
( e2 != op(e4,e1)
| spl140_200 ),
inference(avatar_component_clause,[],[f2430]) ).
fof(f2435,definition,
( spl140_201
<=> e2 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl140_201])],[avatar_definition]) ).
fof(f2436,plain,
( e2 = op(e4,e2)
| ~ spl140_201 ),
inference(avatar_component_clause,[],[f2435]) ).
fof(f2437,plain,
( e2 != op(e4,e2)
| spl140_201 ),
inference(avatar_component_clause,[],[f2435]) ).
fof(f2440,plain,
( e4 = op(e2,e4)
| ~ spl140_33 ),
inference(superposition,[],[f318,f1079]) ).
fof(f2459,plain,
( e3 = e4
| ~ spl140_33 ),
inference(forward_demodulation,[],[f2440,f1821]) ).
fof(f2462,plain,
( $false
| ~ spl140_33 ),
inference(forward_subsumption_resolution,[],[f2459,f477]) ).
fof(f2463,plain,
~ spl140_33,
inference(avatar_contradiction_clause,[],[f2462]) ).
fof(f2496,definition,
( spl140_207
<=> e1 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl140_207])],[avatar_definition]) ).
fof(f2497,plain,
( e1 = op(e4,e1)
| ~ spl140_207 ),
inference(avatar_component_clause,[],[f2496]) ).
fof(f2498,plain,
( e1 != op(e4,e1)
| spl140_207 ),
inference(avatar_component_clause,[],[f2496]) ).
fof(f2501,definition,
( spl140_208
<=> e1 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl140_208])],[avatar_definition]) ).
fof(f2502,plain,
( e1 = op(e4,e3)
| ~ spl140_208 ),
inference(avatar_component_clause,[],[f2501]) ).
fof(f2503,plain,
( e1 != op(e4,e3)
| spl140_208 ),
inference(avatar_component_clause,[],[f2501]) ).
fof(f2506,definition,
( spl140_209
<=> e1 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl140_209])],[avatar_definition]) ).
fof(f2508,plain,
( e1 != op(e4,e2)
| spl140_209 ),
inference(avatar_component_clause,[],[f2506]) ).
fof(f2510,plain,
( e4 = op(e4,e1)
| ~ spl140_28 ),
inference(superposition,[],[f317,f1057]) ).
fof(f2514,plain,
( e2 = op(e2,e1)
| ~ spl140_28 ),
inference(superposition,[],[f321,f1057]) ).
fof(f2528,plain,
( $false
| ~ spl140_28
| ~ spl140_132 ),
inference(forward_subsumption_resolution,[],[f2514,f2066]) ).
fof(f2529,plain,
( ~ spl140_28
| ~ spl140_132 ),
inference(avatar_contradiction_clause,[],[f2528]) ).
fof(f2606,plain,
( spl140_187
| ~ spl140_28 ),
inference(avatar_split_clause,[],[f2510,f1056,f2196]) ).
fof(f2608,plain,
( e4 != op(e4,e0)
| ~ spl140_187 ),
inference(superposition,[],[f386,f2197]) ).
fof(f2617,plain,
( $false
| ~ spl140_51
| ~ spl140_187 ),
inference(forward_subsumption_resolution,[],[f2608,f1948]) ).
fof(f2618,plain,
( ~ spl140_51
| ~ spl140_187 ),
inference(avatar_contradiction_clause,[],[f2617]) ).
fof(f2633,plain,
( ~ sP125
| spl140_76 ),
inference(forward_subsumption_resolution,[],[f623,f2175]) ).
fof(f2641,plain,
( ~ spl140_1
| spl140_76 ),
inference(avatar_split_clause,[],[f2633,f1304,f937]) ).
fof(f2643,plain,
( e2 != op(e2,e0)
| e0 = op(e2,e2)
| ~ spl140_133 ),
inference(forward_subsumption_resolution,[],[f757,f1630]) ).
fof(f2655,plain,
( e0 = e4
| e2 != op(e2,e0)
| ~ spl140_133 ),
inference(forward_demodulation,[],[f2643,f933]) ).
fof(f2658,plain,
( e2 != op(e2,e0)
| ~ spl140_133 ),
inference(forward_subsumption_resolution,[],[f2655,f483]) ).
fof(f2685,definition,
( spl140_215
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl140_215])],[avatar_definition]) ).
fof(f2686,plain,
( e3 = op(e0,e3)
| ~ spl140_215 ),
inference(avatar_component_clause,[],[f2685]) ).
fof(f2687,plain,
( e3 != op(e0,e3)
| spl140_215 ),
inference(avatar_component_clause,[],[f2685]) ).
fof(f2701,definition,
( spl140_218
<=> e3 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl140_218])],[avatar_definition]) ).
fof(f2702,plain,
( e3 = op(e4,e3)
| ~ spl140_218 ),
inference(avatar_component_clause,[],[f2701]) ).
fof(f2703,plain,
( e3 != op(e4,e3)
| spl140_218 ),
inference(avatar_component_clause,[],[f2701]) ).
fof(f2716,definition,
( spl140_221
<=> e3 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl140_221])],[avatar_definition]) ).
fof(f2717,plain,
( e3 = op(e4,e2)
| ~ spl140_221 ),
inference(avatar_component_clause,[],[f2716]) ).
fof(f2721,plain,
( e4 = op(e3,e4)
| ~ spl140_38 ),
inference(superposition,[],[f318,f1101]) ).
fof(f2746,plain,
( e1 = e4
| ~ spl140_38 ),
inference(forward_demodulation,[],[f2721,f1861]) ).
fof(f2747,plain,
( $false
| ~ spl140_38 ),
inference(forward_subsumption_resolution,[],[f2746,f480]) ).
fof(f2748,plain,
~ spl140_38,
inference(avatar_contradiction_clause,[],[f2747]) ).
fof(f2793,plain,
( e4 = op(e4,e0)
| ~ spl140_23 ),
inference(superposition,[],[f317,f1035]) ).
fof(f2796,plain,
( e3 = op(e0,e3)
| ~ spl140_23 ),
inference(superposition,[],[f320,f1035]) ).
fof(f2797,plain,
( e2 = op(e2,e0)
| ~ spl140_23 ),
inference(superposition,[],[f321,f1035]) ).
fof(f2798,plain,
( e2 = op(e0,e2)
| ~ spl140_23 ),
inference(superposition,[],[f322,f1035]) ).
fof(f2800,plain,
( e1 = op(e0,e1)
| ~ spl140_23 ),
inference(superposition,[],[f324,f1035]) ).
fof(f2811,plain,
( $false
| ~ spl140_23
| spl140_31 ),
inference(forward_subsumption_resolution,[],[f2800,f1071]) ).
fof(f2812,plain,
( ~ spl140_23
| spl140_31 ),
inference(avatar_contradiction_clause,[],[f2811]) ).
fof(f2815,plain,
( $false
| ~ spl140_23
| spl140_196 ),
inference(forward_subsumption_resolution,[],[f2798,f2412]) ).
fof(f2816,plain,
( ~ spl140_23
| spl140_196 ),
inference(avatar_contradiction_clause,[],[f2815]) ).
fof(f2817,plain,
( $false
| ~ spl140_23
| ~ spl140_133 ),
inference(forward_subsumption_resolution,[],[f2797,f2658]) ).
fof(f2818,plain,
( ~ spl140_23
| ~ spl140_133 ),
inference(avatar_contradiction_clause,[],[f2817]) ).
fof(f2819,plain,
( $false
| ~ spl140_23
| spl140_215 ),
inference(forward_subsumption_resolution,[],[f2796,f2687]) ).
fof(f2820,plain,
( ~ spl140_23
| spl140_215 ),
inference(avatar_contradiction_clause,[],[f2819]) ).
fof(f2823,plain,
( $false
| ~ spl140_23
| ~ spl140_187 ),
inference(forward_subsumption_resolution,[],[f2793,f2608]) ).
fof(f2824,plain,
( ~ spl140_23
| ~ spl140_187 ),
inference(avatar_contradiction_clause,[],[f2823]) ).
fof(f2834,definition,
( spl140_230
<=> e4 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl140_230])],[avatar_definition]) ).
fof(f2836,plain,
( e4 != op(e4,e2)
| spl140_230 ),
inference(avatar_component_clause,[],[f2834]) ).
fof(f3009,plain,
( e4 != op(e4,e2)
| ~ spl140_23 ),
inference(superposition,[],[f385,f2793]) ).
fof(f3018,plain,
( ~ spl140_230
| ~ spl140_23 ),
inference(avatar_split_clause,[],[f3009,f1034,f2834]) ).
fof(f3070,plain,
( e0 = op(e4,e3)
| e2 = op(e4,e3)
| e3 = op(e4,e3)
| e4 = op(e4,e3)
| spl140_208 ),
inference(forward_subsumption_resolution,[],[f292,f2503]) ).
fof(f3073,plain,
( e0 = op(e4,e3)
| e3 = op(e4,e3)
| e4 = op(e4,e3)
| spl140_52
| spl140_208 ),
inference(forward_subsumption_resolution,[],[f3070,f2366]) ).
fof(f3074,plain,
( e0 = op(e4,e3)
| e4 = op(e4,e3)
| spl140_52
| spl140_208
| spl140_218 ),
inference(forward_subsumption_resolution,[],[f3073,f2703]) ).
fof(f3075,plain,
( e4 = op(e4,e3)
| spl140_52
| spl140_208
| spl140_218 ),
inference(global_subsumption,[],[f3074,f1850]) ).
fof(f3076,plain,
( spl140_195
| spl140_52
| spl140_208
| spl140_218 ),
inference(avatar_split_clause,[],[f3075,f2701,f2501,f1172,f2405]) ).
fof(f3079,plain,
( e4 != op(e4,e0)
| ~ spl140_195 ),
inference(superposition,[],[f384,f2406]) ).
fof(f3090,plain,
( $false
| ~ spl140_23
| ~ spl140_195 ),
inference(forward_subsumption_resolution,[],[f3079,f2793]) ).
fof(f3091,plain,
( ~ spl140_23
| ~ spl140_195 ),
inference(avatar_contradiction_clause,[],[f3090]) ).
fof(f3108,plain,
( e3 = op(e4,e1)
| ~ spl140_97
| ~ spl140_208 ),
inference(forward_subsumption_resolution,[],[f2017,f2502]) ).
fof(f3120,plain,
( e1 = op(e4,e2)
| e2 = op(e4,e2)
| e3 = op(e4,e2)
| e4 = op(e4,e2) ),
inference(forward_subsumption_resolution,[],[f293,f1851]) ).
fof(f3131,plain,
( e2 != op(e0,e2)
| ~ spl140_201 ),
inference(superposition,[],[f453,f2436]) ).
fof(f3140,plain,
( $false
| ~ spl140_196
| ~ spl140_201 ),
inference(forward_subsumption_resolution,[],[f3131,f2411]) ).
fof(f3141,plain,
( ~ spl140_196
| ~ spl140_201 ),
inference(avatar_contradiction_clause,[],[f3140]) ).
fof(f3143,plain,
( e1 != op(e4,e2)
| ~ spl140_98
| spl140_200 ),
inference(forward_subsumption_resolution,[],[f2368,f2432]) ).
fof(f3146,plain,
( ~ spl140_209
| ~ spl140_98
| spl140_200 ),
inference(avatar_split_clause,[],[f3143,f2430,f1450,f2506]) ).
fof(f3148,plain,
( e2 = e3
| e1 != op(e4,e2)
| ~ spl140_97
| ~ spl140_98
| ~ spl140_208 ),
inference(forward_demodulation,[],[f2368,f3108]) ).
fof(f3149,plain,
( e1 != op(e4,e2)
| ~ spl140_97
| ~ spl140_98
| ~ spl140_208 ),
inference(forward_subsumption_resolution,[],[f3148,f479]) ).
fof(f3150,plain,
( ~ spl140_209
| ~ spl140_97
| ~ spl140_98
| ~ spl140_208 ),
inference(avatar_split_clause,[],[f3149,f2501,f1450,f1445,f2506]) ).
fof(f3228,plain,
( e3 != op(e0,e3)
| ~ spl140_218 ),
inference(superposition,[],[f443,f2702]) ).
fof(f3233,plain,
( $false
| ~ spl140_215
| ~ spl140_218 ),
inference(forward_subsumption_resolution,[],[f3228,f2686]) ).
fof(f3234,plain,
( ~ spl140_215
| ~ spl140_218 ),
inference(avatar_contradiction_clause,[],[f3233]) ).
fof(f3238,plain,
( e1 = op(e4,e2)
| e3 = op(e4,e2)
| e4 = op(e4,e2)
| spl140_201 ),
inference(forward_subsumption_resolution,[],[f3120,f2437]) ).
fof(f3239,plain,
( e1 = op(e4,e2)
| e3 = op(e4,e2)
| spl140_201
| spl140_230 ),
inference(forward_subsumption_resolution,[],[f3238,f2836]) ).
fof(f3241,plain,
( e2 = op(e4,e3)
| ~ spl140_52 ),
inference(forward_demodulation,[],[f1174,f1821]) ).
fof(f3244,plain,
( e2 != op(e4,e1)
| ~ spl140_52 ),
inference(superposition,[],[f381,f3241]) ).
fof(f3256,plain,
( ~ spl140_200
| ~ spl140_52 ),
inference(avatar_split_clause,[],[f3244,f1172,f2430]) ).
fof(f3257,plain,
( e3 = op(e4,e2)
| spl140_201
| spl140_209
| spl140_230 ),
inference(forward_subsumption_resolution,[],[f3239,f2508]) ).
fof(f3258,plain,
( spl140_221
| spl140_201
| spl140_209
| spl140_230 ),
inference(avatar_split_clause,[],[f3257,f2834,f2506,f2435,f2716]) ).
fof(f3277,plain,
( e1 = op(e4,e1)
| e2 = op(e4,e1)
| e3 = op(e4,e1)
| e4 = op(e4,e1) ),
inference(forward_subsumption_resolution,[],[f294,f1852]) ).
fof(f3278,plain,
( e2 = op(e4,e1)
| e3 = op(e4,e1)
| e4 = op(e4,e1)
| spl140_207 ),
inference(forward_subsumption_resolution,[],[f3277,f2498]) ).
fof(f3279,plain,
( e3 = op(e4,e1)
| e4 = op(e4,e1)
| spl140_200
| spl140_207 ),
inference(forward_subsumption_resolution,[],[f3278,f2432]) ).
fof(f3284,plain,
( e3 = op(e4,e1)
| spl140_187
| spl140_200
| spl140_207 ),
inference(forward_subsumption_resolution,[],[f3279,f2198]) ).
fof(f3287,definition,
( spl140_234
<=> e3 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl140_234])],[avatar_definition]) ).
fof(f3288,plain,
( e3 = op(e4,e1)
| ~ spl140_234 ),
inference(avatar_component_clause,[],[f3287]) ).
fof(f3289,plain,
( e3 != op(e4,e1)
| spl140_234 ),
inference(avatar_component_clause,[],[f3287]) ).
fof(f3291,plain,
( spl140_234
| spl140_187
| spl140_200
| spl140_207 ),
inference(avatar_split_clause,[],[f3284,f2496,f2430,f2196,f3287]) ).
fof(f3292,plain,
( e3 != op(e4,e2)
| ~ spl140_234 ),
inference(superposition,[],[f382,f3288]) ).
fof(f3303,plain,
( $false
| ~ spl140_221
| ~ spl140_234 ),
inference(forward_subsumption_resolution,[],[f3292,f2717]) ).
fof(f3304,plain,
( ~ spl140_221
| ~ spl140_234 ),
inference(avatar_contradiction_clause,[],[f3303]) ).
fof(f3313,plain,
( e1 != op(e0,e1)
| ~ spl140_207 ),
inference(superposition,[],[f463,f2497]) ).
fof(f3318,plain,
( $false
| ~ spl140_31
| ~ spl140_207 ),
inference(forward_subsumption_resolution,[],[f3313,f1070]) ).
fof(f3319,plain,
( ~ spl140_31
| ~ spl140_207 ),
inference(avatar_contradiction_clause,[],[f3318]) ).
fof(f3325,plain,
( e1 != op(e4,e3)
| ~ spl140_97
| spl140_234 ),
inference(forward_subsumption_resolution,[],[f2017,f3289]) ).
fof(f3328,plain,
( ~ spl140_208
| ~ spl140_97
| spl140_234 ),
inference(avatar_split_clause,[],[f3325,f3287,f1445,f2501]) ).
cnf(s645,plain,
( spl140_1
| spl140_2
| spl140_3
| spl140_4
| spl140_5 ),
inference(sat_conversion,[],[f956]) ).
cnf(s826,plain,
( ~ spl140_5
| spl140_51 ),
inference(sat_conversion,[],[f1170]) ).
cnf(s1031,plain,
( ~ spl140_4
| spl140_97 ),
inference(sat_conversion,[],[f1448]) ).
cnf(s1035,plain,
( ~ spl140_4
| spl140_98 ),
inference(sat_conversion,[],[f1453]) ).
cnf(s1047,plain,
( ~ spl140_4
| spl140_101 ),
inference(sat_conversion,[],[f1468]) ).
cnf(s1181,plain,
( ~ spl140_3
| spl140_132 ),
inference(sat_conversion,[],[f1626]) ).
cnf(s1185,plain,
( ~ spl140_3
| spl140_133 ),
inference(sat_conversion,[],[f1631]) ).
cnf(s1265,plain,
( ~ spl140_2
| spl140_152 ),
inference(sat_conversion,[],[f1727]) ).
cnf(s1410,plain,
~ spl140_76,
inference(sat_conversion,[],[f1819]) ).
cnf(s1445,plain,
~ spl140_55,
inference(sat_conversion,[],[f1847]) ).
cnf(s1681,plain,
( spl140_55
| ~ spl140_152 ),
inference(sat_conversion,[],[f2148]) ).
cnf(s1702,plain,
( spl140_23
| spl140_28
| spl140_33
| spl140_38
| spl140_43 ),
inference(sat_conversion,[],[f2206]) ).
cnf(s1710,plain,
( ~ spl140_23
| ~ spl140_51 ),
inference(sat_conversion,[],[f2227]) ).
cnf(s1719,plain,
( ~ spl140_28
| ~ spl140_101 ),
inference(sat_conversion,[],[f2247]) ).
cnf(s1774,plain,
~ spl140_43,
inference(sat_conversion,[],[f2365]) ).
cnf(s1843,plain,
~ spl140_33,
inference(sat_conversion,[],[f2463]) ).
cnf(s1893,plain,
( ~ spl140_28
| ~ spl140_132 ),
inference(sat_conversion,[],[f2529]) ).
cnf(s1964,plain,
( ~ spl140_28
| spl140_187 ),
inference(sat_conversion,[],[f2606]) ).
cnf(s1969,plain,
( ~ spl140_51
| ~ spl140_187 ),
inference(sat_conversion,[],[f2618]) ).
cnf(s2013,plain,
( ~ spl140_1
| spl140_76 ),
inference(sat_conversion,[],[f2641]) ).
cnf(s2126,plain,
~ spl140_38,
inference(sat_conversion,[],[f2748]) ).
cnf(s2175,plain,
( ~ spl140_23
| spl140_31 ),
inference(sat_conversion,[],[f2812]) ).
cnf(s2177,plain,
( ~ spl140_23
| spl140_196 ),
inference(sat_conversion,[],[f2816]) ).
cnf(s2178,plain,
( ~ spl140_23
| ~ spl140_133 ),
inference(sat_conversion,[],[f2818]) ).
cnf(s2179,plain,
( ~ spl140_23
| spl140_215 ),
inference(sat_conversion,[],[f2820]) ).
cnf(s2182,plain,
( ~ spl140_23
| ~ spl140_187 ),
inference(sat_conversion,[],[f2824]) ).
cnf(s2324,plain,
( ~ spl140_23
| ~ spl140_230 ),
inference(sat_conversion,[],[f3018]) ).
cnf(s2364,plain,
( spl140_52
| spl140_195
| spl140_208
| spl140_218 ),
inference(sat_conversion,[],[f3076]) ).
cnf(s2369,plain,
( ~ spl140_23
| ~ spl140_195 ),
inference(sat_conversion,[],[f3091]) ).
cnf(s2387,plain,
( ~ spl140_196
| ~ spl140_201 ),
inference(sat_conversion,[],[f3141]) ).
cnf(s2396,plain,
( ~ spl140_98
| spl140_200
| ~ spl140_209 ),
inference(sat_conversion,[],[f3146]) ).
cnf(s2400,plain,
( ~ spl140_97
| ~ spl140_98
| ~ spl140_208
| ~ spl140_209 ),
inference(sat_conversion,[],[f3150]) ).
cnf(s2444,plain,
( ~ spl140_215
| ~ spl140_218 ),
inference(sat_conversion,[],[f3234]) ).
cnf(s2466,plain,
( ~ spl140_52
| ~ spl140_200 ),
inference(sat_conversion,[],[f3256]) ).
cnf(s2470,plain,
( spl140_201
| spl140_209
| spl140_221
| spl140_230 ),
inference(sat_conversion,[],[f3258]) ).
cnf(s2485,plain,
( spl140_187
| spl140_200
| spl140_207
| spl140_234 ),
inference(sat_conversion,[],[f3291]) ).
cnf(s2488,plain,
( ~ spl140_221
| ~ spl140_234 ),
inference(sat_conversion,[],[f3304]) ).
cnf(s2497,plain,
( ~ spl140_31
| ~ spl140_207 ),
inference(sat_conversion,[],[f3319]) ).
cnf(s2511,plain,
( ~ spl140_97
| ~ spl140_208
| spl140_234 ),
inference(sat_conversion,[],[f3328]) ).
cnf(s2512,plain,
( spl140_23
| spl140_28 ),
inference(rat,[],[s1702,s1774,s2126,s1843]) ).
cnf(s2515,plain,
~ spl140_152,
inference(rat,[],[s1681,s1445]) ).
cnf(s2516,plain,
~ spl140_1,
inference(rat,[],[s2013,s1410]) ).
cnf(s2517,plain,
~ spl140_2,
inference(rat,[],[s1265,s2515]) ).
cnf(s2519,plain,
( spl140_3
| spl140_4
| spl140_5 ),
inference(rat,[],[s645,s2517,s2516]) ).
cnf(s2520,plain,
~ spl140_51,
inference(rat,[],[s2512,s1964,s1710,s1969]) ).
cnf(s2521,plain,
~ spl140_5,
inference(rat,[],[s826,s2520]) ).
cnf(s2522,plain,
( ~ spl140_208
| ~ spl140_4 ),
inference(rat,[],[s2470,s2488,s2400,s2511,s1035,s1031,s2324,s2387,s2177,s2512,s1719,s1047]) ).
cnf(s2523,plain,
~ spl140_4,
inference(rat,[],[s2470,s2488,s2396,s2485,s2466,s2364,s2522,s2497,s2387,s2444,s2175,s2177,s2179,s2182,s2324,s2369,s2512,s1719,s1035,s1047]) ).
cnf(s2524,plain,
spl140_3,
inference(rat,[],[s2519,s2521,s2523]) ).
cnf(s2535,plain,
spl140_133,
inference(rat,[],[s1185,s2524]) ).
cnf(s2536,plain,
spl140_132,
inference(rat,[],[s1181,s2524]) ).
cnf(s2552,plain,
~ spl140_23,
inference(rat,[],[s2178,s2535]) ).
cnf(s2554,plain,
~ spl140_28,
inference(rat,[],[s1893,s2536]) ).
cnf(s2555,plain,
$false,
inference(rat,[],[s2512,s2554,s2552]) ).
fof(f3329,plain,
$false,
inference(avatar_sat_refutation,[],[s2555]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG055+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n011.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 19:21:31 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.36 % (3690134)Will run a generic schedule for satisfiability detection.
% 0.19/0.36 % (3690139)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1876995013_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.36 % (3690140)% WARNING: option uhcvi not known.
% 0.19/0.36 % (3690140)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1050193060:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.36 % (3690141)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=354429844:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.36 % (3690142)dis+10_1_sil=32000:sp=arity:random_seed=2350732460:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.36 % (3690145)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2749351036:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.36 % (3690143)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3614661506:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.36 % (3690144)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3522388127:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.36 % Detected minimum model sizes of [5]
% 0.19/0.36 % Detected maximum model sizes of [max]
% 0.19/0.36 % TRYING [5]
% 0.19/0.36 % TRYING [6]
% 0.19/0.36 % TRYING [7]
% 0.19/0.36 % (3690142)Instruction limit reached!
% 0.19/0.36 % (3690142)------------------------------
% 0.19/0.36 % (3690142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.36 % (3690142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.36 % (3690142)CaDiCaL version: 2.1.3
% 0.19/0.36 % (3690142)Termination reason: Instruction limit
% 0.19/0.36 % (3690142)Termination phase: Saturation
% 0.19/0.36 % (3690142)Time elapsed: 0.055 s
% 0.19/0.36 % (3690142)Peak memory usage: 13 MB
% 0.19/0.36 % (3690142)Instructions burned: 104 (million)
% 0.19/0.36 % (3690143)Instruction limit reached!
% 0.19/0.36 % (3690143)------------------------------
% 0.19/0.36 % (3690143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.36 % (3690143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.36 % (3690143)CaDiCaL version: 2.1.3
% 0.19/0.36 % (3690143)Termination reason: Instruction limit
% 0.19/0.36 % (3690143)Termination phase: Saturation
% 0.19/0.36 % (3690143)Time elapsed: 0.058 s
% 0.19/0.36 % (3690143)Peak memory usage: 13 MB
% 0.19/0.36 % (3690143)Instructions burned: 117 (million)
% 0.19/0.36 % (3690141) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3690134-3690141"...
% 0.19/0.36 % (3690144)Instruction limit reached!
% 0.19/0.36 % (3690144)------------------------------
% 0.19/0.36 % (3690144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.36 % (3690144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.36 % (3690144)CaDiCaL version: 2.1.3
% 0.19/0.36 % (3690144)Termination reason: Instruction limit
% 0.19/0.36 % (3690144)Termination phase: Saturation
% 0.19/0.36 % (3690144)Time elapsed: 0.063 s
% 0.19/0.36 % (3690144)Peak memory usage: 13 MB
% 0.19/0.36 % (3690144)Instructions burned: 131 (million)
% 0.19/0.36 % TRYING [8]
% 0.19/0.36 % (3690153)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1984959491:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.19/0.36 % (3690141)...printing done.
% 0.19/0.36 % (3690154)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1269180632:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 0.19/0.36 % (3690141)Refutation found. Thanks to Tanya!
% 0.19/0.36 % SZS status Theorem for theBenchmark
% 0.19/0.36 % SZS output start Proof for theBenchmark
% See solution above
% 0.88/0.36 % (3690141)------------------------------
% 0.88/0.36 % (3690141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.36 % (3690141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.36 % (3690141)CaDiCaL version: 2.1.3
% 0.88/0.36 % (3690141)Termination reason: Refutation
% 0.88/0.36 % (3690141)Time elapsed: 0.076 s
% 0.88/0.36 % (3690141)Peak memory usage: 14 MB
% 0.88/0.36 % (3690141)Instructions burned: 150 (million)
% 0.88/0.36 % (3690134)Success in time 0.122 s
% 0.88/0.36 % Vampire exiting
%------------------------------------------------------------------------------