%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG059+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 : n001.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.96s 0.38s
% Output : Refutation 0.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 262
% Syntax : Number of formulae : 1064 ( 101 unt; 256 def)
% Number of atoms : 5290 (2765 equ)
% Maximal formula atoms : 450 ( 4 avg)
% Number of connectives : 6805 (2579 ~;2612 |;1512 &)
% ( 102 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 258 ( 256 usr; 257 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(op(e2,e2),e2),op(op(e2,e2),e2))
& e1 = op(op(e2,e2),e2)
& e3 = op(e2,e2)
& e4 = op(op(e2,e2),op(e2,e2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(f7,conjecture,
~ ( ( ( ( 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 ) ) ) )
& ( ( op(e0,e0) != op(e0,e0)
& op(op(e0,e0),e0) = e0
& op(op(e0,e0),e0) != e0 )
| ( op(e1,e0) != op(e0,e1)
& op(op(e0,e1),e1) = e0
& op(op(e0,e1),e0) != e1 )
| ( op(e2,e0) != op(e0,e2)
& op(op(e0,e2),e2) = e0
& op(op(e0,e2),e0) != e2 )
| ( op(e3,e0) != op(e0,e3)
& op(op(e0,e3),e3) = e0
& op(op(e0,e3),e0) != e3 )
| ( op(e4,e0) != op(e0,e4)
& op(op(e0,e4),e4) = e0
& op(op(e0,e4),e0) != e4 )
| ( op(e0,e1) != op(e1,e0)
& op(op(e1,e0),e0) = e1
& op(op(e1,e0),e1) != e0 )
| ( op(e1,e1) != op(e1,e1)
& op(op(e1,e1),e1) = e1
& op(op(e1,e1),e1) != e1 )
| ( op(e2,e1) != op(e1,e2)
& op(op(e1,e2),e2) = e1
& op(op(e1,e2),e1) != e2 )
| ( op(e3,e1) != op(e1,e3)
& op(op(e1,e3),e3) = e1
& op(op(e1,e3),e1) != e3 )
| ( op(e4,e1) != op(e1,e4)
& op(op(e1,e4),e4) = e1
& op(op(e1,e4),e1) != e4 )
| ( op(e0,e2) != op(e2,e0)
& op(op(e2,e0),e0) = e2
& op(op(e2,e0),e2) != e0 )
| ( op(e1,e2) != op(e2,e1)
& op(op(e2,e1),e1) = e2
& op(op(e2,e1),e2) != e1 )
| ( op(e2,e2) != op(e2,e2)
& op(op(e2,e2),e2) = e2
& op(op(e2,e2),e2) != e2 )
| ( op(e3,e2) != op(e2,e3)
& op(op(e2,e3),e3) = e2
& op(op(e2,e3),e2) != e3 )
| ( op(e4,e2) != op(e2,e4)
& op(op(e2,e4),e4) = e2
& op(op(e2,e4),e2) != e4 )
| ( op(e0,e3) != op(e3,e0)
& op(op(e3,e0),e0) = e3
& op(op(e3,e0),e3) != e0 )
| ( op(e1,e3) != op(e3,e1)
& op(op(e3,e1),e1) = e3
& op(op(e3,e1),e3) != e1 )
| ( op(e2,e3) != op(e3,e2)
& op(op(e3,e2),e2) = e3
& op(op(e3,e2),e3) != e2 )
| ( op(e3,e3) != op(e3,e3)
& op(op(e3,e3),e3) = e3
& op(op(e3,e3),e3) != e3 )
| ( op(e4,e3) != op(e3,e4)
& op(op(e3,e4),e4) = e3
& op(op(e3,e4),e3) != e4 )
| ( op(e0,e4) != op(e4,e0)
& op(op(e4,e0),e0) = e4
& op(op(e4,e0),e4) != e0 )
| ( op(e1,e4) != op(e4,e1)
& op(op(e4,e1),e1) = e4
& op(op(e4,e1),e4) != e1 )
| ( op(e2,e4) != op(e4,e2)
& op(op(e4,e2),e2) = e4
& op(op(e4,e2),e4) != e2 )
| ( op(e3,e4) != op(e4,e3)
& op(op(e4,e3),e3) = e4
& op(op(e4,e3),e4) != e3 )
| ( op(e4,e4) != op(e4,e4)
& op(op(e4,e4),e4) = e4
& op(op(e4,e4),e4) != e4 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f8,negated_conjecture,
~ ~ ( ( ( ( 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 ) ) ) )
& ( ( op(e0,e0) != op(e0,e0)
& op(op(e0,e0),e0) = e0
& op(op(e0,e0),e0) != e0 )
| ( op(e1,e0) != op(e0,e1)
& op(op(e0,e1),e1) = e0
& op(op(e0,e1),e0) != e1 )
| ( op(e2,e0) != op(e0,e2)
& op(op(e0,e2),e2) = e0
& op(op(e0,e2),e0) != e2 )
| ( op(e3,e0) != op(e0,e3)
& op(op(e0,e3),e3) = e0
& op(op(e0,e3),e0) != e3 )
| ( op(e4,e0) != op(e0,e4)
& op(op(e0,e4),e4) = e0
& op(op(e0,e4),e0) != e4 )
| ( op(e0,e1) != op(e1,e0)
& op(op(e1,e0),e0) = e1
& op(op(e1,e0),e1) != e0 )
| ( op(e1,e1) != op(e1,e1)
& op(op(e1,e1),e1) = e1
& op(op(e1,e1),e1) != e1 )
| ( op(e2,e1) != op(e1,e2)
& op(op(e1,e2),e2) = e1
& op(op(e1,e2),e1) != e2 )
| ( op(e3,e1) != op(e1,e3)
& op(op(e1,e3),e3) = e1
& op(op(e1,e3),e1) != e3 )
| ( op(e4,e1) != op(e1,e4)
& op(op(e1,e4),e4) = e1
& op(op(e1,e4),e1) != e4 )
| ( op(e0,e2) != op(e2,e0)
& op(op(e2,e0),e0) = e2
& op(op(e2,e0),e2) != e0 )
| ( op(e1,e2) != op(e2,e1)
& op(op(e2,e1),e1) = e2
& op(op(e2,e1),e2) != e1 )
| ( op(e2,e2) != op(e2,e2)
& op(op(e2,e2),e2) = e2
& op(op(e2,e2),e2) != e2 )
| ( op(e3,e2) != op(e2,e3)
& op(op(e2,e3),e3) = e2
& op(op(e2,e3),e2) != e3 )
| ( op(e4,e2) != op(e2,e4)
& op(op(e2,e4),e4) = e2
& op(op(e2,e4),e2) != e4 )
| ( op(e0,e3) != op(e3,e0)
& op(op(e3,e0),e0) = e3
& op(op(e3,e0),e3) != e0 )
| ( op(e1,e3) != op(e3,e1)
& op(op(e3,e1),e1) = e3
& op(op(e3,e1),e3) != e1 )
| ( op(e2,e3) != op(e3,e2)
& op(op(e3,e2),e2) = e3
& op(op(e3,e2),e3) != e2 )
| ( op(e3,e3) != op(e3,e3)
& op(op(e3,e3),e3) = e3
& op(op(e3,e3),e3) != e3 )
| ( op(e4,e3) != op(e3,e4)
& op(op(e3,e4),e4) = e3
& op(op(e3,e4),e3) != e4 )
| ( op(e0,e4) != op(e4,e0)
& op(op(e4,e0),e0) = e4
& op(op(e4,e0),e4) != e0 )
| ( op(e1,e4) != op(e4,e1)
& op(op(e4,e1),e1) = e4
& op(op(e4,e1),e4) != e1 )
| ( op(e2,e4) != op(e4,e2)
& op(op(e4,e2),e2) = e4
& op(op(e4,e2),e4) != e2 )
| ( op(e3,e4) != op(e4,e3)
& op(op(e4,e3),e3) = e4
& op(op(e4,e3),e4) != e3 )
| ( op(e4,e4) != op(e4,e4)
& op(op(e4,e4),e4) = e4
& op(op(e4,e4),e4) != e4 ) ) ),
inference(negated_conjecture,[status(cth)],[f7]) ).
fof(f9,plain,
( ( ( ( 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 ) ) ) )
& ( ( op(e0,e0) != op(e0,e0)
& op(op(e0,e0),e0) = e0
& op(op(e0,e0),e0) != e0 )
| ( op(e1,e0) != op(e0,e1)
& op(op(e0,e1),e1) = e0
& op(op(e0,e1),e0) != e1 )
| ( op(e2,e0) != op(e0,e2)
& op(op(e0,e2),e2) = e0
& op(op(e0,e2),e0) != e2 )
| ( op(e3,e0) != op(e0,e3)
& op(op(e0,e3),e3) = e0
& op(op(e0,e3),e0) != e3 )
| ( op(e4,e0) != op(e0,e4)
& op(op(e0,e4),e4) = e0
& op(op(e0,e4),e0) != e4 )
| ( op(e0,e1) != op(e1,e0)
& op(op(e1,e0),e0) = e1
& op(op(e1,e0),e1) != e0 )
| ( op(e1,e1) != op(e1,e1)
& op(op(e1,e1),e1) = e1
& op(op(e1,e1),e1) != e1 )
| ( op(e2,e1) != op(e1,e2)
& op(op(e1,e2),e2) = e1
& op(op(e1,e2),e1) != e2 )
| ( op(e3,e1) != op(e1,e3)
& op(op(e1,e3),e3) = e1
& op(op(e1,e3),e1) != e3 )
| ( op(e4,e1) != op(e1,e4)
& op(op(e1,e4),e4) = e1
& op(op(e1,e4),e1) != e4 )
| ( op(e0,e2) != op(e2,e0)
& op(op(e2,e0),e0) = e2
& op(op(e2,e0),e2) != e0 )
| ( op(e1,e2) != op(e2,e1)
& op(op(e2,e1),e1) = e2
& op(op(e2,e1),e2) != e1 )
| ( op(e2,e2) != op(e2,e2)
& op(op(e2,e2),e2) = e2
& op(op(e2,e2),e2) != e2 )
| ( op(e3,e2) != op(e2,e3)
& op(op(e2,e3),e3) = e2
& op(op(e2,e3),e2) != e3 )
| ( op(e4,e2) != op(e2,e4)
& op(op(e2,e4),e4) = e2
& op(op(e2,e4),e2) != e4 )
| ( op(e0,e3) != op(e3,e0)
& op(op(e3,e0),e0) = e3
& op(op(e3,e0),e3) != e0 )
| ( op(e1,e3) != op(e3,e1)
& op(op(e3,e1),e1) = e3
& op(op(e3,e1),e3) != e1 )
| ( op(e2,e3) != op(e3,e2)
& op(op(e3,e2),e2) = e3
& op(op(e3,e2),e3) != e2 )
| ( op(e3,e3) != op(e3,e3)
& op(op(e3,e3),e3) = e3
& op(op(e3,e3),e3) != e3 )
| ( op(e4,e3) != op(e3,e4)
& op(op(e3,e4),e4) = e3
& op(op(e3,e4),e3) != e4 )
| ( op(e0,e4) != op(e4,e0)
& op(op(e4,e0),e0) = e4
& op(op(e4,e0),e4) != e0 )
| ( op(e1,e4) != op(e4,e1)
& op(op(e4,e1),e1) = e4
& op(op(e4,e1),e4) != e1 )
| ( op(e2,e4) != op(e4,e2)
& op(op(e4,e2),e2) = e4
& op(op(e4,e2),e4) != e2 )
| ( op(e3,e4) != op(e4,e3)
& op(op(e4,e3),e3) = e4
& op(op(e4,e3),e4) != e3 )
| ( op(e4,e4) != op(e4,e4)
& op(op(e4,e4),e4) = e4
& op(op(e4,e4),e4) != e4 ) ) ),
inference(flattening,[],[f8]) ).
fof(f10,definition,
( ( op(e4,e4) != op(e4,e4)
& op(op(e4,e4),e4) = e4
& op(op(e4,e4),e4) != e4 )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f11,definition,
( ( op(e3,e4) != op(e4,e3)
& op(op(e4,e3),e3) = e4
& op(op(e4,e3),e4) != e3 )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f12,definition,
( ( op(e2,e4) != op(e4,e2)
& op(op(e4,e2),e2) = e4
& op(op(e4,e2),e4) != e2 )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f13,definition,
( ( op(e1,e4) != op(e4,e1)
& op(op(e4,e1),e1) = e4
& op(op(e4,e1),e4) != e1 )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f14,definition,
( ( op(e0,e4) != op(e4,e0)
& op(op(e4,e0),e0) = e4
& op(op(e4,e0),e4) != e0 )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f15,definition,
( ( op(e4,e3) != op(e3,e4)
& op(op(e3,e4),e4) = e3
& op(op(e3,e4),e3) != e4 )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f16,definition,
( ( op(e3,e3) != op(e3,e3)
& op(op(e3,e3),e3) = e3
& op(op(e3,e3),e3) != e3 )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f17,definition,
( ( op(e2,e3) != op(e3,e2)
& op(op(e3,e2),e2) = e3
& op(op(e3,e2),e3) != e2 )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f18,definition,
( ( op(e1,e3) != op(e3,e1)
& op(op(e3,e1),e1) = e3
& op(op(e3,e1),e3) != e1 )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f19,definition,
( ( op(e0,e3) != op(e3,e0)
& op(op(e3,e0),e0) = e3
& op(op(e3,e0),e3) != e0 )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f20,definition,
( ( op(e4,e2) != op(e2,e4)
& op(op(e2,e4),e4) = e2
& op(op(e2,e4),e2) != e4 )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f21,definition,
( ( op(e3,e2) != op(e2,e3)
& op(op(e2,e3),e3) = e2
& op(op(e2,e3),e2) != e3 )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f22,definition,
( ( op(e2,e2) != op(e2,e2)
& op(op(e2,e2),e2) = e2
& op(op(e2,e2),e2) != e2 )
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f23,definition,
( ( op(e1,e2) != op(e2,e1)
& op(op(e2,e1),e1) = e2
& op(op(e2,e1),e2) != e1 )
| ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f24,definition,
( ( op(e0,e2) != op(e2,e0)
& op(op(e2,e0),e0) = e2
& op(op(e2,e0),e2) != e0 )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f25,definition,
( ( op(e4,e1) != op(e1,e4)
& op(op(e1,e4),e4) = e1
& op(op(e1,e4),e1) != e4 )
| ~ sP15 ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f26,definition,
( ( op(e3,e1) != op(e1,e3)
& op(op(e1,e3),e3) = e1
& op(op(e1,e3),e1) != e3 )
| ~ sP16 ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f27,definition,
( ( op(e2,e1) != op(e1,e2)
& op(op(e1,e2),e2) = e1
& op(op(e1,e2),e1) != e2 )
| ~ sP17 ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f28,definition,
( ( op(e1,e1) != op(e1,e1)
& op(op(e1,e1),e1) = e1
& op(op(e1,e1),e1) != e1 )
| ~ sP18 ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f29,definition,
( ( op(e0,e1) != op(e1,e0)
& op(op(e1,e0),e0) = e1
& op(op(e1,e0),e1) != e0 )
| ~ sP19 ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f30,definition,
( ( op(e4,e0) != op(e0,e4)
& op(op(e0,e4),e4) = e0
& op(op(e0,e4),e0) != e4 )
| ~ sP20 ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f31,definition,
( ( op(e3,e0) != op(e0,e3)
& op(op(e0,e3),e3) = e0
& op(op(e0,e3),e0) != e3 )
| ~ sP21 ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f32,definition,
( ( op(e2,e0) != op(e0,e2)
& op(op(e0,e2),e2) = e0
& op(op(e0,e2),e0) != e2 )
| ~ sP22 ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f33,definition,
( ( op(e1,e0) != op(e0,e1)
& op(op(e0,e1),e1) = e0
& op(op(e0,e1),e0) != e1 )
| ~ sP23 ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f34,definition,
( op(e4,e4) != e4
| ( op(e4,e4) = e4
& e4 != unit )
| ~ sP24 ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f35,definition,
( op(e4,e3) != e4
| ( op(e4,e4) = e3
& e4 != unit )
| ~ sP25 ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f36,definition,
( op(e4,e2) != e4
| ( op(e4,e4) = e2
& e4 != unit )
| ~ sP26 ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f37,definition,
( op(e4,e1) != e4
| ( op(e4,e4) = e1
& e4 != unit )
| ~ sP27 ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f38,definition,
( op(e4,e0) != e4
| ( op(e4,e4) = e0
& e4 != unit )
| ~ sP28 ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f39,definition,
( op(e3,e4) != e4
| ( op(e3,e4) = e4
& e4 != unit )
| ~ sP29 ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f40,definition,
( op(e3,e3) != e4
| ( op(e3,e4) = e3
& e4 != unit )
| ~ sP30 ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f41,definition,
( op(e3,e2) != e4
| ( op(e3,e4) = e2
& e4 != unit )
| ~ sP31 ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f42,definition,
( op(e3,e1) != e4
| ( op(e3,e4) = e1
& e4 != unit )
| ~ sP32 ),
introduced(definition,[new_symbols(definition,[sP32])],[predicate_definition_introduction]) ).
fof(f43,definition,
( op(e3,e0) != e4
| ( op(e3,e4) = e0
& e4 != unit )
| ~ sP33 ),
introduced(definition,[new_symbols(definition,[sP33])],[predicate_definition_introduction]) ).
fof(f44,definition,
( op(e2,e4) != e4
| ( op(e2,e4) = e4
& e4 != unit )
| ~ sP34 ),
introduced(definition,[new_symbols(definition,[sP34])],[predicate_definition_introduction]) ).
fof(f45,definition,
( op(e2,e3) != e4
| ( op(e2,e4) = e3
& e4 != unit )
| ~ sP35 ),
introduced(definition,[new_symbols(definition,[sP35])],[predicate_definition_introduction]) ).
fof(f46,definition,
( op(e2,e2) != e4
| ( op(e2,e4) = e2
& e4 != unit )
| ~ sP36 ),
introduced(definition,[new_symbols(definition,[sP36])],[predicate_definition_introduction]) ).
fof(f47,definition,
( op(e2,e1) != e4
| ( op(e2,e4) = e1
& e4 != unit )
| ~ sP37 ),
introduced(definition,[new_symbols(definition,[sP37])],[predicate_definition_introduction]) ).
fof(f48,definition,
( op(e2,e0) != e4
| ( op(e2,e4) = e0
& e4 != unit )
| ~ sP38 ),
introduced(definition,[new_symbols(definition,[sP38])],[predicate_definition_introduction]) ).
fof(f49,definition,
( op(e1,e4) != e4
| ( op(e1,e4) = e4
& e4 != unit )
| ~ sP39 ),
introduced(definition,[new_symbols(definition,[sP39])],[predicate_definition_introduction]) ).
fof(f50,definition,
( op(e1,e3) != e4
| ( op(e1,e4) = e3
& e4 != unit )
| ~ sP40 ),
introduced(definition,[new_symbols(definition,[sP40])],[predicate_definition_introduction]) ).
fof(f51,definition,
( op(e1,e2) != e4
| ( op(e1,e4) = e2
& e4 != unit )
| ~ sP41 ),
introduced(definition,[new_symbols(definition,[sP41])],[predicate_definition_introduction]) ).
fof(f52,definition,
( op(e1,e1) != e4
| ( op(e1,e4) = e1
& e4 != unit )
| ~ sP42 ),
introduced(definition,[new_symbols(definition,[sP42])],[predicate_definition_introduction]) ).
fof(f53,definition,
( op(e1,e0) != e4
| ( op(e1,e4) = e0
& e4 != unit )
| ~ sP43 ),
introduced(definition,[new_symbols(definition,[sP43])],[predicate_definition_introduction]) ).
fof(f54,definition,
( op(e0,e4) != e4
| ( op(e0,e4) = e4
& e4 != unit )
| ~ sP44 ),
introduced(definition,[new_symbols(definition,[sP44])],[predicate_definition_introduction]) ).
fof(f55,definition,
( op(e0,e3) != e4
| ( op(e0,e4) = e3
& e4 != unit )
| ~ sP45 ),
introduced(definition,[new_symbols(definition,[sP45])],[predicate_definition_introduction]) ).
fof(f56,definition,
( op(e0,e2) != e4
| ( op(e0,e4) = e2
& e4 != unit )
| ~ sP46 ),
introduced(definition,[new_symbols(definition,[sP46])],[predicate_definition_introduction]) ).
fof(f57,definition,
( op(e0,e1) != e4
| ( op(e0,e4) = e1
& e4 != unit )
| ~ sP47 ),
introduced(definition,[new_symbols(definition,[sP47])],[predicate_definition_introduction]) ).
fof(f58,definition,
( op(e0,e0) != e4
| ( op(e0,e4) = e0
& e4 != unit )
| ~ sP48 ),
introduced(definition,[new_symbols(definition,[sP48])],[predicate_definition_introduction]) ).
fof(f59,definition,
( op(e4,e4) != e3
| ( op(e4,e3) = e4
& e3 != unit )
| ~ sP49 ),
introduced(definition,[new_symbols(definition,[sP49])],[predicate_definition_introduction]) ).
fof(f60,definition,
( op(e4,e3) != e3
| ( op(e4,e3) = e3
& e3 != unit )
| ~ sP50 ),
introduced(definition,[new_symbols(definition,[sP50])],[predicate_definition_introduction]) ).
fof(f61,definition,
( op(e4,e2) != e3
| ( op(e4,e3) = e2
& e3 != unit )
| ~ sP51 ),
introduced(definition,[new_symbols(definition,[sP51])],[predicate_definition_introduction]) ).
fof(f62,definition,
( op(e4,e1) != e3
| ( op(e4,e3) = e1
& e3 != unit )
| ~ sP52 ),
introduced(definition,[new_symbols(definition,[sP52])],[predicate_definition_introduction]) ).
fof(f63,definition,
( op(e4,e0) != e3
| ( op(e4,e3) = e0
& e3 != unit )
| ~ sP53 ),
introduced(definition,[new_symbols(definition,[sP53])],[predicate_definition_introduction]) ).
fof(f64,definition,
( op(e3,e4) != e3
| ( op(e3,e3) = e4
& e3 != unit )
| ~ sP54 ),
introduced(definition,[new_symbols(definition,[sP54])],[predicate_definition_introduction]) ).
fof(f65,definition,
( op(e3,e3) != e3
| ( op(e3,e3) = e3
& e3 != unit )
| ~ sP55 ),
introduced(definition,[new_symbols(definition,[sP55])],[predicate_definition_introduction]) ).
fof(f66,definition,
( op(e3,e2) != e3
| ( op(e3,e3) = e2
& e3 != unit )
| ~ sP56 ),
introduced(definition,[new_symbols(definition,[sP56])],[predicate_definition_introduction]) ).
fof(f67,definition,
( op(e3,e1) != e3
| ( op(e3,e3) = e1
& e3 != unit )
| ~ sP57 ),
introduced(definition,[new_symbols(definition,[sP57])],[predicate_definition_introduction]) ).
fof(f68,definition,
( op(e3,e0) != e3
| ( op(e3,e3) = e0
& e3 != unit )
| ~ sP58 ),
introduced(definition,[new_symbols(definition,[sP58])],[predicate_definition_introduction]) ).
fof(f69,definition,
( op(e2,e4) != e3
| ( op(e2,e3) = e4
& e3 != unit )
| ~ sP59 ),
introduced(definition,[new_symbols(definition,[sP59])],[predicate_definition_introduction]) ).
fof(f70,definition,
( op(e2,e3) != e3
| ( op(e2,e3) = e3
& e3 != unit )
| ~ sP60 ),
introduced(definition,[new_symbols(definition,[sP60])],[predicate_definition_introduction]) ).
fof(f71,definition,
( op(e2,e2) != e3
| ( op(e2,e3) = e2
& e3 != unit )
| ~ sP61 ),
introduced(definition,[new_symbols(definition,[sP61])],[predicate_definition_introduction]) ).
fof(f72,definition,
( op(e2,e1) != e3
| ( op(e2,e3) = e1
& e3 != unit )
| ~ sP62 ),
introduced(definition,[new_symbols(definition,[sP62])],[predicate_definition_introduction]) ).
fof(f73,definition,
( op(e2,e0) != e3
| ( op(e2,e3) = e0
& e3 != unit )
| ~ sP63 ),
introduced(definition,[new_symbols(definition,[sP63])],[predicate_definition_introduction]) ).
fof(f74,definition,
( op(e1,e4) != e3
| ( op(e1,e3) = e4
& e3 != unit )
| ~ sP64 ),
introduced(definition,[new_symbols(definition,[sP64])],[predicate_definition_introduction]) ).
fof(f75,definition,
( op(e1,e3) != e3
| ( op(e1,e3) = e3
& e3 != unit )
| ~ sP65 ),
introduced(definition,[new_symbols(definition,[sP65])],[predicate_definition_introduction]) ).
fof(f76,definition,
( op(e1,e2) != e3
| ( op(e1,e3) = e2
& e3 != unit )
| ~ sP66 ),
introduced(definition,[new_symbols(definition,[sP66])],[predicate_definition_introduction]) ).
fof(f77,definition,
( op(e1,e1) != e3
| ( op(e1,e3) = e1
& e3 != unit )
| ~ sP67 ),
introduced(definition,[new_symbols(definition,[sP67])],[predicate_definition_introduction]) ).
fof(f78,definition,
( op(e1,e0) != e3
| ( op(e1,e3) = e0
& e3 != unit )
| ~ sP68 ),
introduced(definition,[new_symbols(definition,[sP68])],[predicate_definition_introduction]) ).
fof(f79,definition,
( op(e0,e4) != e3
| ( op(e0,e3) = e4
& e3 != unit )
| ~ sP69 ),
introduced(definition,[new_symbols(definition,[sP69])],[predicate_definition_introduction]) ).
fof(f80,definition,
( op(e0,e3) != e3
| ( op(e0,e3) = e3
& e3 != unit )
| ~ sP70 ),
introduced(definition,[new_symbols(definition,[sP70])],[predicate_definition_introduction]) ).
fof(f81,definition,
( op(e0,e2) != e3
| ( op(e0,e3) = e2
& e3 != unit )
| ~ sP71 ),
introduced(definition,[new_symbols(definition,[sP71])],[predicate_definition_introduction]) ).
fof(f82,definition,
( op(e0,e1) != e3
| ( op(e0,e3) = e1
& e3 != unit )
| ~ sP72 ),
introduced(definition,[new_symbols(definition,[sP72])],[predicate_definition_introduction]) ).
fof(f83,definition,
( op(e0,e0) != e3
| ( op(e0,e3) = e0
& e3 != unit )
| ~ sP73 ),
introduced(definition,[new_symbols(definition,[sP73])],[predicate_definition_introduction]) ).
fof(f84,definition,
( op(e4,e4) != e2
| ( op(e4,e2) = e4
& e2 != unit )
| ~ sP74 ),
introduced(definition,[new_symbols(definition,[sP74])],[predicate_definition_introduction]) ).
fof(f85,definition,
( op(e4,e3) != e2
| ( op(e4,e2) = e3
& e2 != unit )
| ~ sP75 ),
introduced(definition,[new_symbols(definition,[sP75])],[predicate_definition_introduction]) ).
fof(f86,definition,
( op(e4,e2) != e2
| ( op(e4,e2) = e2
& e2 != unit )
| ~ sP76 ),
introduced(definition,[new_symbols(definition,[sP76])],[predicate_definition_introduction]) ).
fof(f87,definition,
( op(e4,e1) != e2
| ( op(e4,e2) = e1
& e2 != unit )
| ~ sP77 ),
introduced(definition,[new_symbols(definition,[sP77])],[predicate_definition_introduction]) ).
fof(f88,definition,
( op(e4,e0) != e2
| ( op(e4,e2) = e0
& e2 != unit )
| ~ sP78 ),
introduced(definition,[new_symbols(definition,[sP78])],[predicate_definition_introduction]) ).
fof(f89,definition,
( op(e3,e4) != e2
| ( op(e3,e2) = e4
& e2 != unit )
| ~ sP79 ),
introduced(definition,[new_symbols(definition,[sP79])],[predicate_definition_introduction]) ).
fof(f90,definition,
( op(e3,e3) != e2
| ( op(e3,e2) = e3
& e2 != unit )
| ~ sP80 ),
introduced(definition,[new_symbols(definition,[sP80])],[predicate_definition_introduction]) ).
fof(f91,definition,
( op(e3,e2) != e2
| ( op(e3,e2) = e2
& e2 != unit )
| ~ sP81 ),
introduced(definition,[new_symbols(definition,[sP81])],[predicate_definition_introduction]) ).
fof(f92,definition,
( op(e3,e1) != e2
| ( op(e3,e2) = e1
& e2 != unit )
| ~ sP82 ),
introduced(definition,[new_symbols(definition,[sP82])],[predicate_definition_introduction]) ).
fof(f93,definition,
( op(e3,e0) != e2
| ( op(e3,e2) = e0
& e2 != unit )
| ~ sP83 ),
introduced(definition,[new_symbols(definition,[sP83])],[predicate_definition_introduction]) ).
fof(f94,definition,
( op(e2,e4) != e2
| ( op(e2,e2) = e4
& e2 != unit )
| ~ sP84 ),
introduced(definition,[new_symbols(definition,[sP84])],[predicate_definition_introduction]) ).
fof(f95,definition,
( op(e2,e3) != e2
| ( op(e2,e2) = e3
& e2 != unit )
| ~ sP85 ),
introduced(definition,[new_symbols(definition,[sP85])],[predicate_definition_introduction]) ).
fof(f96,definition,
( op(e2,e2) != e2
| ( op(e2,e2) = e2
& e2 != unit )
| ~ sP86 ),
introduced(definition,[new_symbols(definition,[sP86])],[predicate_definition_introduction]) ).
fof(f97,definition,
( op(e2,e1) != e2
| ( op(e2,e2) = e1
& e2 != unit )
| ~ sP87 ),
introduced(definition,[new_symbols(definition,[sP87])],[predicate_definition_introduction]) ).
fof(f98,definition,
( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit )
| ~ sP88 ),
introduced(definition,[new_symbols(definition,[sP88])],[predicate_definition_introduction]) ).
fof(f99,definition,
( op(e1,e4) != e2
| ( op(e1,e2) = e4
& e2 != unit )
| ~ sP89 ),
introduced(definition,[new_symbols(definition,[sP89])],[predicate_definition_introduction]) ).
fof(f100,definition,
( op(e1,e3) != e2
| ( op(e1,e2) = e3
& e2 != unit )
| ~ sP90 ),
introduced(definition,[new_symbols(definition,[sP90])],[predicate_definition_introduction]) ).
fof(f101,definition,
( op(e1,e2) != e2
| ( op(e1,e2) = e2
& e2 != unit )
| ~ sP91 ),
introduced(definition,[new_symbols(definition,[sP91])],[predicate_definition_introduction]) ).
fof(f102,definition,
( op(e1,e1) != e2
| ( op(e1,e2) = e1
& e2 != unit )
| ~ sP92 ),
introduced(definition,[new_symbols(definition,[sP92])],[predicate_definition_introduction]) ).
fof(f103,definition,
( op(e1,e0) != e2
| ( op(e1,e2) = e0
& e2 != unit )
| ~ sP93 ),
introduced(definition,[new_symbols(definition,[sP93])],[predicate_definition_introduction]) ).
fof(f104,definition,
( op(e0,e4) != e2
| ( op(e0,e2) = e4
& e2 != unit )
| ~ sP94 ),
introduced(definition,[new_symbols(definition,[sP94])],[predicate_definition_introduction]) ).
fof(f105,definition,
( op(e0,e3) != e2
| ( op(e0,e2) = e3
& e2 != unit )
| ~ sP95 ),
introduced(definition,[new_symbols(definition,[sP95])],[predicate_definition_introduction]) ).
fof(f106,definition,
( op(e0,e2) != e2
| ( op(e0,e2) = e2
& e2 != unit )
| ~ sP96 ),
introduced(definition,[new_symbols(definition,[sP96])],[predicate_definition_introduction]) ).
fof(f107,definition,
( op(e0,e1) != e2
| ( op(e0,e2) = e1
& e2 != unit )
| ~ sP97 ),
introduced(definition,[new_symbols(definition,[sP97])],[predicate_definition_introduction]) ).
fof(f108,definition,
( op(e0,e0) != e2
| ( op(e0,e2) = e0
& e2 != unit )
| ~ sP98 ),
introduced(definition,[new_symbols(definition,[sP98])],[predicate_definition_introduction]) ).
fof(f109,definition,
( op(e4,e4) != e1
| ( op(e4,e1) = e4
& e1 != unit )
| ~ sP99 ),
introduced(definition,[new_symbols(definition,[sP99])],[predicate_definition_introduction]) ).
fof(f110,definition,
( op(e4,e3) != e1
| ( op(e4,e1) = e3
& e1 != unit )
| ~ sP100 ),
introduced(definition,[new_symbols(definition,[sP100])],[predicate_definition_introduction]) ).
fof(f111,definition,
( op(e4,e2) != e1
| ( op(e4,e1) = e2
& e1 != unit )
| ~ sP101 ),
introduced(definition,[new_symbols(definition,[sP101])],[predicate_definition_introduction]) ).
fof(f112,definition,
( op(e4,e1) != e1
| ( op(e4,e1) = e1
& e1 != unit )
| ~ sP102 ),
introduced(definition,[new_symbols(definition,[sP102])],[predicate_definition_introduction]) ).
fof(f113,definition,
( op(e4,e0) != e1
| ( op(e4,e1) = e0
& e1 != unit )
| ~ sP103 ),
introduced(definition,[new_symbols(definition,[sP103])],[predicate_definition_introduction]) ).
fof(f114,definition,
( op(e3,e4) != e1
| ( op(e3,e1) = e4
& e1 != unit )
| ~ sP104 ),
introduced(definition,[new_symbols(definition,[sP104])],[predicate_definition_introduction]) ).
fof(f115,definition,
( op(e3,e3) != e1
| ( op(e3,e1) = e3
& e1 != unit )
| ~ sP105 ),
introduced(definition,[new_symbols(definition,[sP105])],[predicate_definition_introduction]) ).
fof(f116,definition,
( op(e3,e2) != e1
| ( op(e3,e1) = e2
& e1 != unit )
| ~ sP106 ),
introduced(definition,[new_symbols(definition,[sP106])],[predicate_definition_introduction]) ).
fof(f117,definition,
( op(e3,e1) != e1
| ( op(e3,e1) = e1
& e1 != unit )
| ~ sP107 ),
introduced(definition,[new_symbols(definition,[sP107])],[predicate_definition_introduction]) ).
fof(f118,definition,
( op(e3,e0) != e1
| ( op(e3,e1) = e0
& e1 != unit )
| ~ sP108 ),
introduced(definition,[new_symbols(definition,[sP108])],[predicate_definition_introduction]) ).
fof(f119,definition,
( op(e2,e4) != e1
| ( op(e2,e1) = e4
& e1 != unit )
| ~ sP109 ),
introduced(definition,[new_symbols(definition,[sP109])],[predicate_definition_introduction]) ).
fof(f120,definition,
( op(e2,e3) != e1
| ( op(e2,e1) = e3
& e1 != unit )
| ~ sP110 ),
introduced(definition,[new_symbols(definition,[sP110])],[predicate_definition_introduction]) ).
fof(f121,definition,
( op(e2,e2) != e1
| ( op(e2,e1) = e2
& e1 != unit )
| ~ sP111 ),
introduced(definition,[new_symbols(definition,[sP111])],[predicate_definition_introduction]) ).
fof(f122,definition,
( op(e2,e1) != e1
| ( op(e2,e1) = e1
& e1 != unit )
| ~ sP112 ),
introduced(definition,[new_symbols(definition,[sP112])],[predicate_definition_introduction]) ).
fof(f123,definition,
( op(e2,e0) != e1
| ( op(e2,e1) = e0
& e1 != unit )
| ~ sP113 ),
introduced(definition,[new_symbols(definition,[sP113])],[predicate_definition_introduction]) ).
fof(f124,definition,
( op(e1,e4) != e1
| ( op(e1,e1) = e4
& e1 != unit )
| ~ sP114 ),
introduced(definition,[new_symbols(definition,[sP114])],[predicate_definition_introduction]) ).
fof(f125,definition,
( op(e1,e3) != e1
| ( op(e1,e1) = e3
& e1 != unit )
| ~ sP115 ),
introduced(definition,[new_symbols(definition,[sP115])],[predicate_definition_introduction]) ).
fof(f126,definition,
( op(e1,e2) != e1
| ( op(e1,e1) = e2
& e1 != unit )
| ~ sP116 ),
introduced(definition,[new_symbols(definition,[sP116])],[predicate_definition_introduction]) ).
fof(f127,definition,
( op(e1,e1) != e1
| ( op(e1,e1) = e1
& e1 != unit )
| ~ sP117 ),
introduced(definition,[new_symbols(definition,[sP117])],[predicate_definition_introduction]) ).
fof(f128,definition,
( op(e1,e0) != e1
| ( op(e1,e1) = e0
& e1 != unit )
| ~ sP118 ),
introduced(definition,[new_symbols(definition,[sP118])],[predicate_definition_introduction]) ).
fof(f129,definition,
( op(e0,e4) != e1
| ( op(e0,e1) = e4
& e1 != unit )
| ~ sP119 ),
introduced(definition,[new_symbols(definition,[sP119])],[predicate_definition_introduction]) ).
fof(f130,definition,
( op(e0,e3) != e1
| ( op(e0,e1) = e3
& e1 != unit )
| ~ sP120 ),
introduced(definition,[new_symbols(definition,[sP120])],[predicate_definition_introduction]) ).
fof(f131,definition,
( op(e0,e2) != e1
| ( op(e0,e1) = e2
& e1 != unit )
| ~ sP121 ),
introduced(definition,[new_symbols(definition,[sP121])],[predicate_definition_introduction]) ).
fof(f132,definition,
( op(e0,e1) != e1
| ( op(e0,e1) = e1
& e1 != unit )
| ~ sP122 ),
introduced(definition,[new_symbols(definition,[sP122])],[predicate_definition_introduction]) ).
fof(f133,definition,
( op(e0,e0) != e1
| ( op(e0,e1) = e0
& e1 != unit )
| ~ sP123 ),
introduced(definition,[new_symbols(definition,[sP123])],[predicate_definition_introduction]) ).
fof(f134,definition,
( op(e4,e4) != e0
| ( op(e4,e0) = e4
& e0 != unit )
| ~ sP124 ),
introduced(definition,[new_symbols(definition,[sP124])],[predicate_definition_introduction]) ).
fof(f135,definition,
( op(e4,e3) != e0
| ( op(e4,e0) = e3
& e0 != unit )
| ~ sP125 ),
introduced(definition,[new_symbols(definition,[sP125])],[predicate_definition_introduction]) ).
fof(f136,definition,
( op(e4,e2) != e0
| ( op(e4,e0) = e2
& e0 != unit )
| ~ sP126 ),
introduced(definition,[new_symbols(definition,[sP126])],[predicate_definition_introduction]) ).
fof(f137,definition,
( op(e4,e1) != e0
| ( op(e4,e0) = e1
& e0 != unit )
| ~ sP127 ),
introduced(definition,[new_symbols(definition,[sP127])],[predicate_definition_introduction]) ).
fof(f138,definition,
( op(e4,e0) != e0
| ( op(e4,e0) = e0
& e0 != unit )
| ~ sP128 ),
introduced(definition,[new_symbols(definition,[sP128])],[predicate_definition_introduction]) ).
fof(f139,definition,
( op(e3,e4) != e0
| ( op(e3,e0) = e4
& e0 != unit )
| ~ sP129 ),
introduced(definition,[new_symbols(definition,[sP129])],[predicate_definition_introduction]) ).
fof(f140,definition,
( op(e3,e3) != e0
| ( op(e3,e0) = e3
& e0 != unit )
| ~ sP130 ),
introduced(definition,[new_symbols(definition,[sP130])],[predicate_definition_introduction]) ).
fof(f141,definition,
( op(e3,e2) != e0
| ( op(e3,e0) = e2
& e0 != unit )
| ~ sP131 ),
introduced(definition,[new_symbols(definition,[sP131])],[predicate_definition_introduction]) ).
fof(f142,definition,
( op(e3,e1) != e0
| ( op(e3,e0) = e1
& e0 != unit )
| ~ sP132 ),
introduced(definition,[new_symbols(definition,[sP132])],[predicate_definition_introduction]) ).
fof(f143,definition,
( op(e3,e0) != e0
| ( op(e3,e0) = e0
& e0 != unit )
| ~ sP133 ),
introduced(definition,[new_symbols(definition,[sP133])],[predicate_definition_introduction]) ).
fof(f144,definition,
( op(e2,e4) != e0
| ( op(e2,e0) = e4
& e0 != unit )
| ~ sP134 ),
introduced(definition,[new_symbols(definition,[sP134])],[predicate_definition_introduction]) ).
fof(f145,definition,
( op(e2,e3) != e0
| ( op(e2,e0) = e3
& e0 != unit )
| ~ sP135 ),
introduced(definition,[new_symbols(definition,[sP135])],[predicate_definition_introduction]) ).
fof(f146,definition,
( op(e2,e2) != e0
| ( op(e2,e0) = e2
& e0 != unit )
| ~ sP136 ),
introduced(definition,[new_symbols(definition,[sP136])],[predicate_definition_introduction]) ).
fof(f147,definition,
( op(e2,e1) != e0
| ( op(e2,e0) = e1
& e0 != unit )
| ~ sP137 ),
introduced(definition,[new_symbols(definition,[sP137])],[predicate_definition_introduction]) ).
fof(f148,definition,
( op(e2,e0) != e0
| ( op(e2,e0) = e0
& e0 != unit )
| ~ sP138 ),
introduced(definition,[new_symbols(definition,[sP138])],[predicate_definition_introduction]) ).
fof(f149,definition,
( op(e1,e4) != e0
| ( op(e1,e0) = e4
& e0 != unit )
| ~ sP139 ),
introduced(definition,[new_symbols(definition,[sP139])],[predicate_definition_introduction]) ).
fof(f150,definition,
( op(e1,e3) != e0
| ( op(e1,e0) = e3
& e0 != unit )
| ~ sP140 ),
introduced(definition,[new_symbols(definition,[sP140])],[predicate_definition_introduction]) ).
fof(f151,definition,
( op(e1,e2) != e0
| ( op(e1,e0) = e2
& e0 != unit )
| ~ sP141 ),
introduced(definition,[new_symbols(definition,[sP141])],[predicate_definition_introduction]) ).
fof(f152,definition,
( op(e1,e1) != e0
| ( op(e1,e0) = e1
& e0 != unit )
| ~ sP142 ),
introduced(definition,[new_symbols(definition,[sP142])],[predicate_definition_introduction]) ).
fof(f153,definition,
( op(e1,e0) != e0
| ( op(e1,e0) = e0
& e0 != unit )
| ~ sP143 ),
introduced(definition,[new_symbols(definition,[sP143])],[predicate_definition_introduction]) ).
fof(f154,definition,
( op(e0,e4) != e0
| ( op(e0,e0) = e4
& e0 != unit )
| ~ sP144 ),
introduced(definition,[new_symbols(definition,[sP144])],[predicate_definition_introduction]) ).
fof(f155,definition,
( op(e0,e3) != e0
| ( op(e0,e0) = e3
& e0 != unit )
| ~ sP145 ),
introduced(definition,[new_symbols(definition,[sP145])],[predicate_definition_introduction]) ).
fof(f156,definition,
( op(e0,e2) != e0
| ( op(e0,e0) = e2
& e0 != unit )
| ~ sP146 ),
introduced(definition,[new_symbols(definition,[sP146])],[predicate_definition_introduction]) ).
fof(f157,definition,
( op(e0,e1) != e0
| ( op(e0,e0) = e1
& e0 != unit )
| ~ sP147 ),
introduced(definition,[new_symbols(definition,[sP147])],[predicate_definition_introduction]) ).
fof(f158,definition,
( op(e0,e0) != e0
| ( op(e0,e0) = e0
& e0 != unit )
| ~ sP148 ),
introduced(definition,[new_symbols(definition,[sP148])],[predicate_definition_introduction]) ).
fof(f159,definition,
( ( sP48
& sP47
& sP46
& sP45
& sP44
& sP43
& sP42
& sP41
& sP40
& sP39
& sP38
& sP37
& sP36
& sP35
& sP34
& sP33
& sP32
& sP31
& sP30
& sP29
& sP28
& sP27
& sP26
& sP25
& sP24 )
| ~ sP149 ),
introduced(definition,[new_symbols(definition,[sP149])],[predicate_definition_introduction]) ).
fof(f160,definition,
( ( sP73
& sP72
& sP71
& sP70
& sP69
& sP68
& sP67
& sP66
& sP65
& sP64
& sP63
& sP62
& sP61
& sP60
& sP59
& sP58
& sP57
& sP56
& sP55
& sP54
& sP53
& sP52
& sP51
& sP50
& sP49 )
| ~ sP150 ),
introduced(definition,[new_symbols(definition,[sP150])],[predicate_definition_introduction]) ).
fof(f161,definition,
( ( sP98
& sP97
& sP96
& sP95
& sP94
& sP93
& sP92
& sP91
& sP90
& sP89
& sP88
& sP87
& sP86
& sP85
& sP84
& sP83
& sP82
& sP81
& sP80
& sP79
& sP78
& sP77
& sP76
& sP75
& sP74 )
| ~ sP151 ),
introduced(definition,[new_symbols(definition,[sP151])],[predicate_definition_introduction]) ).
fof(f162,definition,
( ( sP123
& sP122
& sP121
& sP120
& sP119
& sP118
& sP117
& sP116
& sP115
& sP114
& sP113
& sP112
& sP111
& sP110
& sP109
& sP108
& sP107
& sP106
& sP105
& sP104
& sP103
& sP102
& sP101
& sP100
& sP99 )
| ~ sP152 ),
introduced(definition,[new_symbols(definition,[sP152])],[predicate_definition_introduction]) ).
fof(f163,definition,
( ( sP148
& sP147
& sP146
& sP145
& sP144
& sP143
& sP142
& sP141
& sP140
& sP139
& sP138
& sP137
& sP136
& sP135
& sP134
& sP133
& sP132
& sP131
& sP130
& sP129
& sP128
& sP127
& sP126
& sP125
& sP124 )
| ~ sP153 ),
introduced(definition,[new_symbols(definition,[sP153])],[predicate_definition_introduction]) ).
fof(f164,plain,
( ( sP153
| sP152
| sP151
| sP150
| sP149 )
& ( ( op(e0,e0) != op(e0,e0)
& op(op(e0,e0),e0) = e0
& op(op(e0,e0),e0) != e0 )
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ) ),
inference(definition_folding,[],[f9,f163,f162,f161,f160,f159,f158,f157,f156,f155,f154,f153,f152,f151,f150,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(f165,plain,
( ( sP148
& sP147
& sP146
& sP145
& sP144
& sP143
& sP142
& sP141
& sP140
& sP139
& sP138
& sP137
& sP136
& sP135
& sP134
& sP133
& sP132
& sP131
& sP130
& sP129
& sP128
& sP127
& sP126
& sP125
& sP124 )
| ~ sP153 ),
inference(nnf_transformation,[],[f163]) ).
fof(f166,plain,
( ( sP123
& sP122
& sP121
& sP120
& sP119
& sP118
& sP117
& sP116
& sP115
& sP114
& sP113
& sP112
& sP111
& sP110
& sP109
& sP108
& sP107
& sP106
& sP105
& sP104
& sP103
& sP102
& sP101
& sP100
& sP99 )
| ~ sP152 ),
inference(nnf_transformation,[],[f162]) ).
fof(f167,plain,
( ( sP98
& sP97
& sP96
& sP95
& sP94
& sP93
& sP92
& sP91
& sP90
& sP89
& sP88
& sP87
& sP86
& sP85
& sP84
& sP83
& sP82
& sP81
& sP80
& sP79
& sP78
& sP77
& sP76
& sP75
& sP74 )
| ~ sP151 ),
inference(nnf_transformation,[],[f161]) ).
fof(f168,plain,
( ( sP73
& sP72
& sP71
& sP70
& sP69
& sP68
& sP67
& sP66
& sP65
& sP64
& sP63
& sP62
& sP61
& sP60
& sP59
& sP58
& sP57
& sP56
& sP55
& sP54
& sP53
& sP52
& sP51
& sP50
& sP49 )
| ~ sP150 ),
inference(nnf_transformation,[],[f160]) ).
fof(f169,plain,
( ( sP48
& sP47
& sP46
& sP45
& sP44
& sP43
& sP42
& sP41
& sP40
& sP39
& sP38
& sP37
& sP36
& sP35
& sP34
& sP33
& sP32
& sP31
& sP30
& sP29
& sP28
& sP27
& sP26
& sP25
& sP24 )
| ~ sP149 ),
inference(nnf_transformation,[],[f159]) ).
fof(f170,plain,
( op(e0,e0) != e0
| ( op(e0,e0) = e0
& e0 != unit )
| ~ sP148 ),
inference(nnf_transformation,[],[f158]) ).
fof(f176,plain,
( op(e1,e1) != e0
| ( op(e1,e0) = e1
& e0 != unit )
| ~ sP142 ),
inference(nnf_transformation,[],[f152]) ).
fof(f204,plain,
( op(e1,e4) != e1
| ( op(e1,e1) = e4
& e1 != unit )
| ~ sP114 ),
inference(nnf_transformation,[],[f124]) ).
fof(f208,plain,
( op(e2,e3) != e1
| ( op(e2,e1) = e3
& e1 != unit )
| ~ sP110 ),
inference(nnf_transformation,[],[f120]) ).
fof(f209,plain,
( op(e2,e4) != e1
| ( op(e2,e1) = e4
& e1 != unit )
| ~ sP109 ),
inference(nnf_transformation,[],[f119]) ).
fof(f212,plain,
( op(e3,e2) != e1
| ( op(e3,e1) = e2
& e1 != unit )
| ~ sP106 ),
inference(nnf_transformation,[],[f116]) ).
fof(f214,plain,
( op(e3,e4) != e1
| ( op(e3,e1) = e4
& e1 != unit )
| ~ sP104 ),
inference(nnf_transformation,[],[f114]) ).
fof(f217,plain,
( op(e4,e2) != e1
| ( op(e4,e1) = e2
& e1 != unit )
| ~ sP101 ),
inference(nnf_transformation,[],[f111]) ).
fof(f218,plain,
( op(e4,e3) != e1
| ( op(e4,e1) = e3
& e1 != unit )
| ~ sP100 ),
inference(nnf_transformation,[],[f110]) ).
fof(f219,plain,
( op(e4,e4) != e1
| ( op(e4,e1) = e4
& e1 != unit )
| ~ sP99 ),
inference(nnf_transformation,[],[f109]) ).
fof(f230,plain,
( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit )
| ~ sP88 ),
inference(nnf_transformation,[],[f98]) ).
fof(f234,plain,
( op(e2,e4) != e2
| ( op(e2,e2) = e4
& e2 != unit )
| ~ sP84 ),
inference(nnf_transformation,[],[f94]) ).
fof(f257,plain,
( op(e2,e2) != e3
| ( op(e2,e3) = e2
& e3 != unit )
| ~ sP61 ),
inference(nnf_transformation,[],[f71]) ).
fof(f260,plain,
( op(e3,e0) != e3
| ( op(e3,e3) = e0
& e3 != unit )
| ~ sP58 ),
inference(nnf_transformation,[],[f68]) ).
fof(f288,plain,
( op(e3,e3) != e4
| ( op(e3,e4) = e3
& e4 != unit )
| ~ sP30 ),
inference(nnf_transformation,[],[f40]) ).
fof(f295,plain,
( ( op(e1,e0) != op(e0,e1)
& op(op(e0,e1),e1) = e0
& op(op(e0,e1),e0) != e1 )
| ~ sP23 ),
inference(nnf_transformation,[],[f33]) ).
fof(f296,plain,
( ( op(e2,e0) != op(e0,e2)
& op(op(e0,e2),e2) = e0
& op(op(e0,e2),e0) != e2 )
| ~ sP22 ),
inference(nnf_transformation,[],[f32]) ).
fof(f297,plain,
( ( op(e3,e0) != op(e0,e3)
& op(op(e0,e3),e3) = e0
& op(op(e0,e3),e0) != e3 )
| ~ sP21 ),
inference(nnf_transformation,[],[f31]) ).
fof(f298,plain,
( ( op(e4,e0) != op(e0,e4)
& op(op(e0,e4),e4) = e0
& op(op(e0,e4),e0) != e4 )
| ~ sP20 ),
inference(nnf_transformation,[],[f30]) ).
fof(f299,plain,
( ( op(e0,e1) != op(e1,e0)
& op(op(e1,e0),e0) = e1
& op(op(e1,e0),e1) != e0 )
| ~ sP19 ),
inference(nnf_transformation,[],[f29]) ).
fof(f300,plain,
( ( op(e1,e1) != op(e1,e1)
& op(op(e1,e1),e1) = e1
& op(op(e1,e1),e1) != e1 )
| ~ sP18 ),
inference(nnf_transformation,[],[f28]) ).
fof(f301,plain,
( ( op(e2,e1) != op(e1,e2)
& op(op(e1,e2),e2) = e1
& op(op(e1,e2),e1) != e2 )
| ~ sP17 ),
inference(nnf_transformation,[],[f27]) ).
fof(f302,plain,
( ( op(e3,e1) != op(e1,e3)
& op(op(e1,e3),e3) = e1
& op(op(e1,e3),e1) != e3 )
| ~ sP16 ),
inference(nnf_transformation,[],[f26]) ).
fof(f303,plain,
( ( op(e4,e1) != op(e1,e4)
& op(op(e1,e4),e4) = e1
& op(op(e1,e4),e1) != e4 )
| ~ sP15 ),
inference(nnf_transformation,[],[f25]) ).
fof(f304,plain,
( ( op(e0,e2) != op(e2,e0)
& op(op(e2,e0),e0) = e2
& op(op(e2,e0),e2) != e0 )
| ~ sP14 ),
inference(nnf_transformation,[],[f24]) ).
fof(f305,plain,
( ( op(e1,e2) != op(e2,e1)
& op(op(e2,e1),e1) = e2
& op(op(e2,e1),e2) != e1 )
| ~ sP13 ),
inference(nnf_transformation,[],[f23]) ).
fof(f306,plain,
( ( op(e2,e2) != op(e2,e2)
& op(op(e2,e2),e2) = e2
& op(op(e2,e2),e2) != e2 )
| ~ sP12 ),
inference(nnf_transformation,[],[f22]) ).
fof(f307,plain,
( ( op(e3,e2) != op(e2,e3)
& op(op(e2,e3),e3) = e2
& op(op(e2,e3),e2) != e3 )
| ~ sP11 ),
inference(nnf_transformation,[],[f21]) ).
fof(f308,plain,
( ( op(e4,e2) != op(e2,e4)
& op(op(e2,e4),e4) = e2
& op(op(e2,e4),e2) != e4 )
| ~ sP10 ),
inference(nnf_transformation,[],[f20]) ).
fof(f309,plain,
( ( op(e0,e3) != op(e3,e0)
& op(op(e3,e0),e0) = e3
& op(op(e3,e0),e3) != e0 )
| ~ sP9 ),
inference(nnf_transformation,[],[f19]) ).
fof(f310,plain,
( ( op(e1,e3) != op(e3,e1)
& op(op(e3,e1),e1) = e3
& op(op(e3,e1),e3) != e1 )
| ~ sP8 ),
inference(nnf_transformation,[],[f18]) ).
fof(f311,plain,
( ( op(e2,e3) != op(e3,e2)
& op(op(e3,e2),e2) = e3
& op(op(e3,e2),e3) != e2 )
| ~ sP7 ),
inference(nnf_transformation,[],[f17]) ).
fof(f312,plain,
( ( op(e3,e3) != op(e3,e3)
& op(op(e3,e3),e3) = e3
& op(op(e3,e3),e3) != e3 )
| ~ sP6 ),
inference(nnf_transformation,[],[f16]) ).
fof(f313,plain,
( ( op(e4,e3) != op(e3,e4)
& op(op(e3,e4),e4) = e3
& op(op(e3,e4),e3) != e4 )
| ~ sP5 ),
inference(nnf_transformation,[],[f15]) ).
fof(f314,plain,
( ( op(e0,e4) != op(e4,e0)
& op(op(e4,e0),e0) = e4
& op(op(e4,e0),e4) != e0 )
| ~ sP4 ),
inference(nnf_transformation,[],[f14]) ).
fof(f315,plain,
( ( op(e1,e4) != op(e4,e1)
& op(op(e4,e1),e1) = e4
& op(op(e4,e1),e4) != e1 )
| ~ sP3 ),
inference(nnf_transformation,[],[f13]) ).
fof(f316,plain,
( ( op(e2,e4) != op(e4,e2)
& op(op(e4,e2),e2) = e4
& op(op(e4,e2),e4) != e2 )
| ~ sP2 ),
inference(nnf_transformation,[],[f12]) ).
fof(f317,plain,
( ( op(e3,e4) != op(e4,e3)
& op(op(e4,e3),e3) = e4
& op(op(e4,e3),e4) != e3 )
| ~ sP1 ),
inference(nnf_transformation,[],[f11]) ).
fof(f318,plain,
( ( op(e4,e4) != op(e4,e4)
& op(op(e4,e4),e4) = e4
& op(op(e4,e4),e4) != e4 )
| ~ sP0 ),
inference(nnf_transformation,[],[f10]) ).
fof(f319,plain,
( e0 = op(e4,e4)
| e1 = op(e4,e4)
| e2 = op(e4,e4)
| e3 = op(e4,e4)
| e4 = op(e4,e4) ),
inference(cnf_transformation,[],[f1]) ).
fof(f320,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(f321,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(f324,plain,
( e0 = op(e3,e4)
| e1 = op(e3,e4)
| e2 = op(e3,e4)
| e3 = op(e3,e4)
| e4 = op(e3,e4) ),
inference(cnf_transformation,[],[f1]) ).
fof(f329,plain,
( e0 = op(e2,e4)
| e1 = op(e2,e4)
| e2 = op(e2,e4)
| e3 = op(e2,e4)
| e4 = op(e2,e4) ),
inference(cnf_transformation,[],[f1]) ).
fof(f330,plain,
( e0 = op(e2,e3)
| e1 = op(e2,e3)
| e2 = op(e2,e3)
| e3 = op(e2,e3)
| e4 = op(e2,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f334,plain,
( e0 = op(e1,e4)
| e1 = op(e1,e4)
| e2 = op(e1,e4)
| e3 = op(e1,e4)
| e4 = op(e1,e4) ),
inference(cnf_transformation,[],[f1]) ).
fof(f335,plain,
( e0 = op(e1,e3)
| e1 = op(e1,e3)
| e2 = op(e1,e3)
| e3 = op(e1,e3)
| e4 = op(e1,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f336,plain,
( e0 = op(e1,e2)
| e1 = op(e1,e2)
| e2 = op(e1,e2)
| e3 = op(e1,e2)
| e4 = op(e1,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f344,plain,
( e0 = unit
| e1 = unit
| e2 = unit
| e3 = unit
| e4 = unit ),
inference(cnf_transformation,[],[f2]) ).
fof(f345,plain,
e4 = op(e4,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f346,plain,
e4 = op(unit,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f347,plain,
e3 = op(e3,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f348,plain,
e3 = op(unit,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f349,plain,
e2 = op(e2,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f350,plain,
e2 = op(unit,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f351,plain,
e1 = op(e1,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f352,plain,
e1 = op(unit,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f353,plain,
e0 = op(e0,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f405,plain,
op(e4,e3) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f407,plain,
op(e4,e2) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f411,plain,
op(e4,e0) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f413,plain,
op(e4,e0) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f414,plain,
op(e4,e0) != op(e4,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f415,plain,
op(e3,e3) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f418,plain,
op(e3,e1) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f419,plain,
op(e3,e1) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f421,plain,
op(e3,e0) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f430,plain,
op(e2,e1) != op(e2,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f432,plain,
op(e2,e0) != op(e2,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f435,plain,
op(e1,e3) != op(e1,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f436,plain,
op(e1,e2) != op(e1,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f437,plain,
op(e1,e2) != op(e1,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f438,plain,
op(e1,e1) != op(e1,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f439,plain,
op(e1,e1) != op(e1,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f440,plain,
op(e1,e1) != op(e1,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f441,plain,
op(e1,e0) != op(e1,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f442,plain,
op(e1,e0) != op(e1,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f455,plain,
op(e3,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f456,plain,
op(e2,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f457,plain,
op(e2,e4) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f458,plain,
op(e1,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f460,plain,
op(e1,e4) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f463,plain,
op(e0,e4) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f464,plain,
op(e0,e4) != op(e1,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f465,plain,
op(e3,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f467,plain,
op(e2,e3) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f468,plain,
op(e1,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f469,plain,
op(e1,e3) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f470,plain,
op(e1,e3) != op(e2,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f471,plain,
op(e0,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f473,plain,
op(e0,e3) != op(e2,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f474,plain,
op(e0,e3) != op(e1,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f476,plain,
op(e2,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f479,plain,
op(e1,e2) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f481,plain,
op(e0,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f485,plain,
op(e3,e1) != op(e4,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f505,plain,
e3 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f506,plain,
e2 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f507,plain,
e2 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f509,plain,
e1 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f511,plain,
e0 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f512,plain,
e0 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f514,plain,
e0 != e1,
inference(cnf_transformation,[],[f5]) ).
fof(f515,plain,
e4 = op(op(e2,e2),op(e2,e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f516,plain,
e3 = op(e2,e2),
inference(cnf_transformation,[],[f6]) ).
fof(f517,plain,
e1 = op(op(e2,e2),e2),
inference(cnf_transformation,[],[f6]) ).
fof(f518,plain,
e0 = op(op(op(e2,e2),e2),op(op(e2,e2),e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f537,plain,
( sP142
| ~ sP153 ),
inference(cnf_transformation,[],[f165]) ).
fof(f543,plain,
( sP148
| ~ sP153 ),
inference(cnf_transformation,[],[f165]) ).
fof(f544,plain,
( sP99
| ~ sP152 ),
inference(cnf_transformation,[],[f166]) ).
fof(f545,plain,
( sP100
| ~ sP152 ),
inference(cnf_transformation,[],[f166]) ).
fof(f546,plain,
( sP101
| ~ sP152 ),
inference(cnf_transformation,[],[f166]) ).
fof(f549,plain,
( sP104
| ~ sP152 ),
inference(cnf_transformation,[],[f166]) ).
fof(f551,plain,
( sP106
| ~ sP152 ),
inference(cnf_transformation,[],[f166]) ).
fof(f554,plain,
( sP109
| ~ sP152 ),
inference(cnf_transformation,[],[f166]) ).
fof(f555,plain,
( sP110
| ~ sP152 ),
inference(cnf_transformation,[],[f166]) ).
fof(f559,plain,
( sP114
| ~ sP152 ),
inference(cnf_transformation,[],[f166]) ).
fof(f579,plain,
( sP84
| ~ sP151 ),
inference(cnf_transformation,[],[f167]) ).
fof(f583,plain,
( sP88
| ~ sP151 ),
inference(cnf_transformation,[],[f167]) ).
fof(f603,plain,
( sP58
| ~ sP150 ),
inference(cnf_transformation,[],[f168]) ).
fof(f606,plain,
( sP61
| ~ sP150 ),
inference(cnf_transformation,[],[f168]) ).
fof(f625,plain,
( sP30
| ~ sP149 ),
inference(cnf_transformation,[],[f169]) ).
fof(f644,plain,
( e0 != op(e0,e0)
| e0 != unit
| ~ sP148 ),
inference(cnf_transformation,[],[f170]) ).
fof(f657,plain,
( e0 != op(e1,e1)
| e1 = op(e1,e0)
| ~ sP142 ),
inference(cnf_transformation,[],[f176]) ).
fof(f713,plain,
( e1 != op(e1,e4)
| e4 = op(e1,e1)
| ~ sP114 ),
inference(cnf_transformation,[],[f204]) ).
fof(f721,plain,
( e1 != op(e2,e3)
| e3 = op(e2,e1)
| ~ sP110 ),
inference(cnf_transformation,[],[f208]) ).
fof(f723,plain,
( e1 != op(e2,e4)
| e4 = op(e2,e1)
| ~ sP109 ),
inference(cnf_transformation,[],[f209]) ).
fof(f729,plain,
( e1 != op(e3,e2)
| e2 = op(e3,e1)
| ~ sP106 ),
inference(cnf_transformation,[],[f212]) ).
fof(f733,plain,
( e1 != op(e3,e4)
| e4 = op(e3,e1)
| ~ sP104 ),
inference(cnf_transformation,[],[f214]) ).
fof(f739,plain,
( e1 != op(e4,e2)
| e2 = op(e4,e1)
| ~ sP101 ),
inference(cnf_transformation,[],[f217]) ).
fof(f741,plain,
( e1 != op(e4,e3)
| e3 = op(e4,e1)
| ~ sP100 ),
inference(cnf_transformation,[],[f218]) ).
fof(f743,plain,
( e1 != op(e4,e4)
| e4 = op(e4,e1)
| ~ sP99 ),
inference(cnf_transformation,[],[f219]) ).
fof(f765,plain,
( e2 != op(e2,e0)
| e0 = op(e2,e2)
| ~ sP88 ),
inference(cnf_transformation,[],[f230]) ).
fof(f773,plain,
( e2 != op(e2,e4)
| e4 = op(e2,e2)
| ~ sP84 ),
inference(cnf_transformation,[],[f234]) ).
fof(f819,plain,
( e3 != op(e2,e2)
| e2 = op(e2,e3)
| ~ sP61 ),
inference(cnf_transformation,[],[f257]) ).
fof(f825,plain,
( e3 != op(e3,e0)
| e0 = op(e3,e3)
| ~ sP58 ),
inference(cnf_transformation,[],[f260]) ).
fof(f880,plain,
( e4 != op(e3,e3)
| e4 != unit
| ~ sP30 ),
inference(cnf_transformation,[],[f288]) ).
fof(f881,plain,
( e4 != op(e3,e3)
| e3 = op(e3,e4)
| ~ sP30 ),
inference(cnf_transformation,[],[f288]) ).
fof(f896,plain,
( op(e0,e1) != op(e1,e0)
| ~ sP23 ),
inference(cnf_transformation,[],[f295]) ).
fof(f898,plain,
( e0 = op(op(e0,e2),e2)
| ~ sP22 ),
inference(cnf_transformation,[],[f296]) ).
fof(f902,plain,
( op(e0,e3) != op(e3,e0)
| ~ sP21 ),
inference(cnf_transformation,[],[f297]) ).
fof(f903,plain,
( e4 != op(op(e0,e4),e0)
| ~ sP20 ),
inference(cnf_transformation,[],[f298]) ).
fof(f906,plain,
( e0 != op(op(e1,e0),e1)
| ~ sP19 ),
inference(cnf_transformation,[],[f299]) ).
fof(f911,plain,
( op(e1,e1) != op(e1,e1)
| ~ sP18 ),
inference(cnf_transformation,[],[f300]) ).
fof(f914,plain,
( op(e1,e2) != op(e2,e1)
| ~ sP17 ),
inference(cnf_transformation,[],[f301]) ).
fof(f917,plain,
( op(e1,e3) != op(e3,e1)
| ~ sP16 ),
inference(cnf_transformation,[],[f302]) ).
fof(f920,plain,
( op(e1,e4) != op(e4,e1)
| ~ sP15 ),
inference(cnf_transformation,[],[f303]) ).
fof(f923,plain,
( op(e0,e2) != op(e2,e0)
| ~ sP14 ),
inference(cnf_transformation,[],[f304]) ).
fof(f925,plain,
( e2 = op(op(e2,e1),e1)
| ~ sP13 ),
inference(cnf_transformation,[],[f305]) ).
fof(f929,plain,
( op(e2,e2) != op(e2,e2)
| ~ sP12 ),
inference(cnf_transformation,[],[f306]) ).
fof(f931,plain,
( e2 = op(op(e2,e3),e3)
| ~ sP11 ),
inference(cnf_transformation,[],[f307]) ).
fof(f933,plain,
( e4 != op(op(e2,e4),e2)
| ~ sP10 ),
inference(cnf_transformation,[],[f308]) ).
fof(f938,plain,
( op(e0,e3) != op(e3,e0)
| ~ sP9 ),
inference(cnf_transformation,[],[f309]) ).
fof(f941,plain,
( op(e1,e3) != op(e3,e1)
| ~ sP8 ),
inference(cnf_transformation,[],[f310]) ).
fof(f942,plain,
( e2 != op(op(e3,e2),e3)
| ~ sP7 ),
inference(cnf_transformation,[],[f311]) ).
fof(f947,plain,
( op(e3,e3) != op(e3,e3)
| ~ sP6 ),
inference(cnf_transformation,[],[f312]) ).
fof(f949,plain,
( e3 = op(op(e3,e4),e4)
| ~ sP5 ),
inference(cnf_transformation,[],[f313]) ).
fof(f953,plain,
( op(e0,e4) != op(e4,e0)
| ~ sP4 ),
inference(cnf_transformation,[],[f314]) ).
fof(f955,plain,
( e4 = op(op(e4,e1),e1)
| ~ sP3 ),
inference(cnf_transformation,[],[f315]) ).
fof(f958,plain,
( e4 = op(op(e4,e2),e2)
| ~ sP2 ),
inference(cnf_transformation,[],[f316]) ).
fof(f961,plain,
( e4 = op(op(e4,e3),e3)
| ~ sP1 ),
inference(cnf_transformation,[],[f317]) ).
fof(f965,plain,
( op(e4,e4) != op(e4,e4)
| ~ sP0 ),
inference(cnf_transformation,[],[f318]) ).
fof(f966,plain,
( e0 != op(op(e0,e0),e0)
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f164]) ).
fof(f969,plain,
( sP153
| sP152
| sP151
| sP150
| sP149 ),
inference(cnf_transformation,[],[f164]) ).
fof(f971,plain,
~ sP0,
inference(trivial_inequality_removal,[],[f965]) ).
fof(f972,plain,
~ sP6,
inference(trivial_inequality_removal,[],[f947]) ).
fof(f973,plain,
~ sP12,
inference(trivial_inequality_removal,[],[f929]) ).
fof(f974,plain,
~ sP18,
inference(trivial_inequality_removal,[],[f911]) ).
fof(f980,plain,
e3 = op(e2,e2),
inference(global_subsumption,[],[f516]) ).
fof(f985,definition,
( spl154_1
<=> sP149 ),
introduced(definition,[new_symbols(definition,[spl154_1])],[avatar_definition]) ).
fof(f989,definition,
( spl154_2
<=> sP150 ),
introduced(definition,[new_symbols(definition,[spl154_2])],[avatar_definition]) ).
fof(f993,definition,
( spl154_3
<=> sP151 ),
introduced(definition,[new_symbols(definition,[spl154_3])],[avatar_definition]) ).
fof(f997,definition,
( spl154_4
<=> sP152 ),
introduced(definition,[new_symbols(definition,[spl154_4])],[avatar_definition]) ).
fof(f1001,definition,
( spl154_5
<=> sP153 ),
introduced(definition,[new_symbols(definition,[spl154_5])],[avatar_definition]) ).
fof(f1004,plain,
( spl154_1
| spl154_2
| spl154_3
| spl154_4
| spl154_5 ),
inference(avatar_split_clause,[],[f969,f1001,f997,f993,f989,f985]) ).
fof(f1006,definition,
( spl154_6
<=> sP23 ),
introduced(definition,[new_symbols(definition,[spl154_6])],[avatar_definition]) ).
fof(f1008,plain,
( ~ sP23
| spl154_6 ),
inference(avatar_component_clause,[],[f1006]) ).
fof(f1015,definition,
( spl154_8
<=> sP22 ),
introduced(definition,[new_symbols(definition,[spl154_8])],[avatar_definition]) ).
fof(f1017,plain,
( ~ sP22
| spl154_8 ),
inference(avatar_component_clause,[],[f1015]) ).
fof(f1024,definition,
( spl154_10
<=> sP21 ),
introduced(definition,[new_symbols(definition,[spl154_10])],[avatar_definition]) ).
fof(f1026,plain,
( ~ sP21
| spl154_10 ),
inference(avatar_component_clause,[],[f1024]) ).
fof(f1033,definition,
( spl154_12
<=> sP20 ),
introduced(definition,[new_symbols(definition,[spl154_12])],[avatar_definition]) ).
fof(f1035,plain,
( ~ sP20
| spl154_12 ),
inference(avatar_component_clause,[],[f1033]) ).
fof(f1037,definition,
( spl154_13
<=> e4 = op(op(e0,e4),e0) ),
introduced(definition,[new_symbols(definition,[spl154_13])],[avatar_definition]) ).
fof(f1039,plain,
( e4 != op(op(e0,e4),e0)
| spl154_13 ),
inference(avatar_component_clause,[],[f1037]) ).
fof(f1040,plain,
( ~ spl154_12
| ~ spl154_13 ),
inference(avatar_split_clause,[],[f903,f1037,f1033]) ).
fof(f1042,definition,
( spl154_14
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl154_14])],[avatar_definition]) ).
fof(f1044,plain,
( ~ sP19
| spl154_14 ),
inference(avatar_component_clause,[],[f1042]) ).
fof(f1046,definition,
( spl154_15
<=> e0 = op(op(e1,e0),e1) ),
introduced(definition,[new_symbols(definition,[spl154_15])],[avatar_definition]) ).
fof(f1048,plain,
( e0 != op(op(e1,e0),e1)
| spl154_15 ),
inference(avatar_component_clause,[],[f1046]) ).
fof(f1049,plain,
( ~ spl154_14
| ~ spl154_15 ),
inference(avatar_split_clause,[],[f906,f1046,f1042]) ).
fof(f1051,definition,
( spl154_16
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl154_16])],[avatar_definition]) ).
fof(f1060,definition,
( spl154_18
<=> sP16 ),
introduced(definition,[new_symbols(definition,[spl154_18])],[avatar_definition]) ).
fof(f1062,plain,
( ~ sP16
| spl154_18 ),
inference(avatar_component_clause,[],[f1060]) ).
fof(f1069,definition,
( spl154_20
<=> sP15 ),
introduced(definition,[new_symbols(definition,[spl154_20])],[avatar_definition]) ).
fof(f1071,plain,
( ~ sP15
| spl154_20 ),
inference(avatar_component_clause,[],[f1069]) ).
fof(f1078,definition,
( spl154_22
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl154_22])],[avatar_definition]) ).
fof(f1080,plain,
( ~ sP14
| spl154_22 ),
inference(avatar_component_clause,[],[f1078]) ).
fof(f1087,definition,
( spl154_24
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl154_24])],[avatar_definition]) ).
fof(f1089,plain,
( ~ sP13
| spl154_24 ),
inference(avatar_component_clause,[],[f1087]) ).
fof(f1096,definition,
( spl154_26
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl154_26])],[avatar_definition]) ).
fof(f1098,plain,
( ~ sP11
| spl154_26 ),
inference(avatar_component_clause,[],[f1096]) ).
fof(f1105,definition,
( spl154_28
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl154_28])],[avatar_definition]) ).
fof(f1107,plain,
( ~ sP10
| spl154_28 ),
inference(avatar_component_clause,[],[f1105]) ).
fof(f1109,definition,
( spl154_29
<=> e4 = op(op(e2,e4),e2) ),
introduced(definition,[new_symbols(definition,[spl154_29])],[avatar_definition]) ).
fof(f1111,plain,
( e4 != op(op(e2,e4),e2)
| spl154_29 ),
inference(avatar_component_clause,[],[f1109]) ).
fof(f1112,plain,
( ~ spl154_28
| ~ spl154_29 ),
inference(avatar_split_clause,[],[f933,f1109,f1105]) ).
fof(f1114,definition,
( spl154_30
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl154_30])],[avatar_definition]) ).
fof(f1116,plain,
( ~ sP9
| spl154_30 ),
inference(avatar_component_clause,[],[f1114]) ).
fof(f1123,definition,
( spl154_32
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl154_32])],[avatar_definition]) ).
fof(f1125,plain,
( ~ sP8
| spl154_32 ),
inference(avatar_component_clause,[],[f1123]) ).
fof(f1132,definition,
( spl154_34
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl154_34])],[avatar_definition]) ).
fof(f1134,plain,
( ~ sP7
| spl154_34 ),
inference(avatar_component_clause,[],[f1132]) ).
fof(f1136,definition,
( spl154_35
<=> e2 = op(op(e3,e2),e3) ),
introduced(definition,[new_symbols(definition,[spl154_35])],[avatar_definition]) ).
fof(f1137,plain,
( e2 = op(op(e3,e2),e3)
| ~ spl154_35 ),
inference(avatar_component_clause,[],[f1136]) ).
fof(f1138,plain,
( e2 != op(op(e3,e2),e3)
| spl154_35 ),
inference(avatar_component_clause,[],[f1136]) ).
fof(f1139,plain,
( ~ spl154_34
| ~ spl154_35 ),
inference(avatar_split_clause,[],[f942,f1136,f1132]) ).
fof(f1141,definition,
( spl154_36
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl154_36])],[avatar_definition]) ).
fof(f1143,plain,
( ~ sP5
| spl154_36 ),
inference(avatar_component_clause,[],[f1141]) ).
fof(f1150,definition,
( spl154_38
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl154_38])],[avatar_definition]) ).
fof(f1152,plain,
( ~ sP4
| spl154_38 ),
inference(avatar_component_clause,[],[f1150]) ).
fof(f1159,definition,
( spl154_40
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl154_40])],[avatar_definition]) ).
fof(f1161,plain,
( ~ sP3
| spl154_40 ),
inference(avatar_component_clause,[],[f1159]) ).
fof(f1168,definition,
( spl154_42
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl154_42])],[avatar_definition]) ).
fof(f1170,plain,
( ~ sP2
| spl154_42 ),
inference(avatar_component_clause,[],[f1168]) ).
fof(f1177,definition,
( spl154_44
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl154_44])],[avatar_definition]) ).
fof(f1179,plain,
( ~ sP1
| spl154_44 ),
inference(avatar_component_clause,[],[f1177]) ).
fof(f1186,definition,
( spl154_46
<=> sP148 ),
introduced(definition,[new_symbols(definition,[spl154_46])],[avatar_definition]) ).
fof(f1188,plain,
( ~ sP148
| spl154_46 ),
inference(avatar_component_clause,[],[f1186]) ).
fof(f1190,definition,
( spl154_47
<=> e0 = unit ),
introduced(definition,[new_symbols(definition,[spl154_47])],[avatar_definition]) ).
fof(f1191,plain,
( e0 = unit
| ~ spl154_47 ),
inference(avatar_component_clause,[],[f1190]) ).
fof(f1192,plain,
( e0 != unit
| spl154_47 ),
inference(avatar_component_clause,[],[f1190]) ).
fof(f1194,definition,
( spl154_48
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl154_48])],[avatar_definition]) ).
fof(f1195,plain,
( e0 = op(e0,e0)
| ~ spl154_48 ),
inference(avatar_component_clause,[],[f1194]) ).
fof(f1196,plain,
( e0 != op(e0,e0)
| spl154_48 ),
inference(avatar_component_clause,[],[f1194]) ).
fof(f1197,plain,
( ~ spl154_46
| ~ spl154_47
| ~ spl154_48 ),
inference(avatar_split_clause,[],[f644,f1194,f1190,f1186]) ).
fof(f1242,definition,
( spl154_51
<=> op(e1,e3) = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl154_51])],[avatar_definition]) ).
fof(f1243,plain,
( op(e1,e3) = op(e3,e1)
| ~ spl154_51 ),
inference(avatar_component_clause,[],[f1242]) ).
fof(f1244,plain,
( op(e1,e3) != op(e3,e1)
| spl154_51 ),
inference(avatar_component_clause,[],[f1242]) ).
fof(f1245,plain,
( ~ spl154_18
| ~ spl154_51 ),
inference(avatar_split_clause,[],[f917,f1242,f1060]) ).
fof(f1251,definition,
( spl154_53
<=> e1 = unit ),
introduced(definition,[new_symbols(definition,[spl154_53])],[avatar_definition]) ).
fof(f1252,plain,
( e1 = unit
| ~ spl154_53 ),
inference(avatar_component_clause,[],[f1251]) ).
fof(f1253,plain,
( e1 != unit
| spl154_53 ),
inference(avatar_component_clause,[],[f1251]) ).
fof(f1264,definition,
( spl154_56
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl154_56])],[avatar_definition]) ).
fof(f1265,plain,
( e1 = op(e0,e1)
| ~ spl154_56 ),
inference(avatar_component_clause,[],[f1264]) ).
fof(f1266,plain,
( e1 != op(e0,e1)
| spl154_56 ),
inference(avatar_component_clause,[],[f1264]) ).
fof(f1274,definition,
( spl154_58
<=> e2 = unit ),
introduced(definition,[new_symbols(definition,[spl154_58])],[avatar_definition]) ).
fof(f1275,plain,
( e2 = unit
| ~ spl154_58 ),
inference(avatar_component_clause,[],[f1274]) ).
fof(f1276,plain,
( e2 != unit
| spl154_58 ),
inference(avatar_component_clause,[],[f1274]) ).
fof(f1296,definition,
( spl154_63
<=> e3 = unit ),
introduced(definition,[new_symbols(definition,[spl154_63])],[avatar_definition]) ).
fof(f1297,plain,
( e3 = unit
| ~ spl154_63 ),
inference(avatar_component_clause,[],[f1296]) ).
fof(f1298,plain,
( e3 != unit
| spl154_63 ),
inference(avatar_component_clause,[],[f1296]) ).
fof(f1318,definition,
( spl154_68
<=> e4 = unit ),
introduced(definition,[new_symbols(definition,[spl154_68])],[avatar_definition]) ).
fof(f1319,plain,
( e4 = unit
| ~ spl154_68 ),
inference(avatar_component_clause,[],[f1318]) ).
fof(f1320,plain,
( e4 != unit
| spl154_68 ),
inference(avatar_component_clause,[],[f1318]) ).
fof(f1426,definition,
( spl154_90
<=> sP142 ),
introduced(definition,[new_symbols(definition,[spl154_90])],[avatar_definition]) ).
fof(f1428,plain,
( sP142
| ~ spl154_90 ),
inference(avatar_component_clause,[],[f1426]) ).
fof(f1429,plain,
( ~ spl154_5
| spl154_90 ),
inference(avatar_split_clause,[],[f537,f1426,f1001]) ).
fof(f1451,plain,
( ~ sP153
| spl154_46 ),
inference(forward_subsumption_resolution,[],[f543,f1188]) ).
fof(f1452,plain,
( ~ spl154_5
| spl154_46 ),
inference(avatar_split_clause,[],[f1451,f1186,f1001]) ).
fof(f1454,definition,
( spl154_95
<=> sP99 ),
introduced(definition,[new_symbols(definition,[spl154_95])],[avatar_definition]) ).
fof(f1456,plain,
( sP99
| ~ spl154_95 ),
inference(avatar_component_clause,[],[f1454]) ).
fof(f1457,plain,
( ~ spl154_4
| spl154_95 ),
inference(avatar_split_clause,[],[f544,f1454,f997]) ).
fof(f1459,definition,
( spl154_96
<=> sP100 ),
introduced(definition,[new_symbols(definition,[spl154_96])],[avatar_definition]) ).
fof(f1461,plain,
( sP100
| ~ spl154_96 ),
inference(avatar_component_clause,[],[f1459]) ).
fof(f1462,plain,
( ~ spl154_4
| spl154_96 ),
inference(avatar_split_clause,[],[f545,f1459,f997]) ).
fof(f1464,definition,
( spl154_97
<=> sP101 ),
introduced(definition,[new_symbols(definition,[spl154_97])],[avatar_definition]) ).
fof(f1466,plain,
( sP101
| ~ spl154_97 ),
inference(avatar_component_clause,[],[f1464]) ).
fof(f1467,plain,
( ~ spl154_4
| spl154_97 ),
inference(avatar_split_clause,[],[f546,f1464,f997]) ).
fof(f1479,definition,
( spl154_100
<=> sP104 ),
introduced(definition,[new_symbols(definition,[spl154_100])],[avatar_definition]) ).
fof(f1481,plain,
( sP104
| ~ spl154_100 ),
inference(avatar_component_clause,[],[f1479]) ).
fof(f1482,plain,
( ~ spl154_4
| spl154_100 ),
inference(avatar_split_clause,[],[f549,f1479,f997]) ).
fof(f1489,definition,
( spl154_102
<=> sP106 ),
introduced(definition,[new_symbols(definition,[spl154_102])],[avatar_definition]) ).
fof(f1491,plain,
( sP106
| ~ spl154_102 ),
inference(avatar_component_clause,[],[f1489]) ).
fof(f1492,plain,
( ~ spl154_4
| spl154_102 ),
inference(avatar_split_clause,[],[f551,f1489,f997]) ).
fof(f1504,definition,
( spl154_105
<=> sP109 ),
introduced(definition,[new_symbols(definition,[spl154_105])],[avatar_definition]) ).
fof(f1506,plain,
( sP109
| ~ spl154_105 ),
inference(avatar_component_clause,[],[f1504]) ).
fof(f1507,plain,
( ~ spl154_4
| spl154_105 ),
inference(avatar_split_clause,[],[f554,f1504,f997]) ).
fof(f1509,definition,
( spl154_106
<=> sP110 ),
introduced(definition,[new_symbols(definition,[spl154_106])],[avatar_definition]) ).
fof(f1511,plain,
( sP110
| ~ spl154_106 ),
inference(avatar_component_clause,[],[f1509]) ).
fof(f1512,plain,
( ~ spl154_4
| spl154_106 ),
inference(avatar_split_clause,[],[f555,f1509,f997]) ).
fof(f1529,definition,
( spl154_110
<=> sP114 ),
introduced(definition,[new_symbols(definition,[spl154_110])],[avatar_definition]) ).
fof(f1531,plain,
( sP114
| ~ spl154_110 ),
inference(avatar_component_clause,[],[f1529]) ).
fof(f1532,plain,
( ~ spl154_4
| spl154_110 ),
inference(avatar_split_clause,[],[f559,f1529,f997]) ).
fof(f1620,definition,
( spl154_128
<=> sP84 ),
introduced(definition,[new_symbols(definition,[spl154_128])],[avatar_definition]) ).
fof(f1622,plain,
( sP84
| ~ spl154_128 ),
inference(avatar_component_clause,[],[f1620]) ).
fof(f1623,plain,
( ~ spl154_3
| spl154_128 ),
inference(avatar_split_clause,[],[f579,f1620,f993]) ).
fof(f1640,definition,
( spl154_132
<=> sP88 ),
introduced(definition,[new_symbols(definition,[spl154_132])],[avatar_definition]) ).
fof(f1642,plain,
( sP88
| ~ spl154_132 ),
inference(avatar_component_clause,[],[f1640]) ).
fof(f1643,plain,
( ~ spl154_3
| spl154_132 ),
inference(avatar_split_clause,[],[f583,f1640,f993]) ).
fof(f1731,definition,
( spl154_150
<=> sP58 ),
introduced(definition,[new_symbols(definition,[spl154_150])],[avatar_definition]) ).
fof(f1733,plain,
( sP58
| ~ spl154_150 ),
inference(avatar_component_clause,[],[f1731]) ).
fof(f1734,plain,
( ~ spl154_2
| spl154_150 ),
inference(avatar_split_clause,[],[f603,f1731,f989]) ).
fof(f1746,definition,
( spl154_153
<=> sP61 ),
introduced(definition,[new_symbols(definition,[spl154_153])],[avatar_definition]) ).
fof(f1748,plain,
( sP61
| ~ spl154_153 ),
inference(avatar_component_clause,[],[f1746]) ).
fof(f1749,plain,
( ~ spl154_2
| spl154_153 ),
inference(avatar_split_clause,[],[f606,f1746,f989]) ).
fof(f1826,plain,
e1 = op(e3,e2),
inference(forward_demodulation,[],[f517,f980]) ).
fof(f1828,plain,
e1 != op(e1,e2),
inference(superposition,[],[f479,f1826]) ).
fof(f1832,plain,
e4 = op(e3,e3),
inference(forward_demodulation,[],[f515,f980]) ).
fof(f1834,plain,
e4 != op(e3,e1),
inference(superposition,[],[f419,f1832]) ).
fof(f1836,plain,
e4 != op(e2,e3),
inference(superposition,[],[f467,f1832]) ).
fof(f1837,plain,
e4 != op(e1,e3),
inference(superposition,[],[f469,f1832]) ).
fof(f1860,plain,
( e0 != op(e1,e1)
| e1 = op(e1,e0)
| ~ spl154_90 ),
inference(forward_subsumption_resolution,[],[f657,f1428]) ).
fof(f1862,definition,
( spl154_167
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl154_167])],[avatar_definition]) ).
fof(f1863,plain,
( e1 != op(e1,e0)
| spl154_167 ),
inference(avatar_component_clause,[],[f1862]) ).
fof(f1864,plain,
( e1 = op(e1,e0)
| ~ spl154_167 ),
inference(avatar_component_clause,[],[f1862]) ).
fof(f1866,definition,
( spl154_168
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl154_168])],[avatar_definition]) ).
fof(f1867,plain,
( e0 = op(e1,e1)
| ~ spl154_168 ),
inference(avatar_component_clause,[],[f1866]) ).
fof(f1869,plain,
( spl154_167
| ~ spl154_168
| ~ spl154_90 ),
inference(avatar_split_clause,[],[f1860,f1426,f1866,f1862]) ).
fof(f1893,definition,
( spl154_170
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl154_170])],[avatar_definition]) ).
fof(f1894,plain,
( e0 = op(e2,e3)
| ~ spl154_170 ),
inference(avatar_component_clause,[],[f1893]) ).
fof(f1895,plain,
( e0 != op(e2,e3)
| spl154_170 ),
inference(avatar_component_clause,[],[f1893]) ).
fof(f1907,definition,
( spl154_172
<=> e0 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl154_172])],[avatar_definition]) ).
fof(f1909,plain,
( e0 != op(e2,e4)
| spl154_172 ),
inference(avatar_component_clause,[],[f1907]) ).
fof(f1966,definition,
( spl154_178
<=> e0 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl154_178])],[avatar_definition]) ).
fof(f1968,plain,
( e0 != op(e1,e2)
| spl154_178 ),
inference(avatar_component_clause,[],[f1966]) ).
fof(f2007,definition,
( spl154_182
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl154_182])],[avatar_definition]) ).
fof(f2008,plain,
( e1 = op(e1,e3)
| ~ spl154_182 ),
inference(avatar_component_clause,[],[f2007]) ).
fof(f2009,plain,
( e1 != op(e1,e3)
| spl154_182 ),
inference(avatar_component_clause,[],[f2007]) ).
fof(f2018,plain,
( e1 != op(e1,e4)
| e4 = op(e1,e1)
| ~ spl154_110 ),
inference(forward_subsumption_resolution,[],[f713,f1531]) ).
fof(f2028,plain,
( e1 != op(e2,e4)
| e4 = op(e2,e1)
| ~ spl154_105 ),
inference(forward_subsumption_resolution,[],[f723,f1506]) ).
fof(f2030,definition,
( spl154_183
<=> e4 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl154_183])],[avatar_definition]) ).
fof(f2032,plain,
( e4 = op(e2,e1)
| ~ spl154_183 ),
inference(avatar_component_clause,[],[f2030]) ).
fof(f2034,definition,
( spl154_184
<=> e1 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl154_184])],[avatar_definition]) ).
fof(f2035,plain,
( e1 = op(e2,e4)
| ~ spl154_184 ),
inference(avatar_component_clause,[],[f2034]) ).
fof(f2036,plain,
( e1 != op(e2,e4)
| spl154_184 ),
inference(avatar_component_clause,[],[f2034]) ).
fof(f2037,plain,
( spl154_183
| ~ spl154_184
| ~ spl154_105 ),
inference(avatar_split_clause,[],[f2028,f1504,f2034,f2030]) ).
fof(f2049,plain,
( e2 = op(e3,e1)
| ~ sP106 ),
inference(forward_subsumption_resolution,[],[f729,f1826]) ).
fof(f2050,plain,
( e2 = op(e3,e1)
| ~ spl154_102 ),
inference(forward_subsumption_resolution,[],[f2049,f1491]) ).
fof(f2056,plain,
( e2 != op(e1,e3)
| spl154_51
| ~ spl154_102 ),
inference(superposition,[],[f1244,f2050]) ).
fof(f2065,plain,
( e1 != op(e3,e4)
| ~ sP104 ),
inference(forward_subsumption_resolution,[],[f733,f1834]) ).
fof(f2066,plain,
( e1 != op(e3,e4)
| ~ spl154_100 ),
inference(forward_subsumption_resolution,[],[f2065,f1481]) ).
fof(f2070,plain,
( e1 != op(e4,e3)
| e3 = op(e4,e1)
| ~ spl154_96 ),
inference(forward_subsumption_resolution,[],[f741,f1461]) ).
fof(f2072,definition,
( spl154_185
<=> e3 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl154_185])],[avatar_definition]) ).
fof(f2074,plain,
( e3 = op(e4,e1)
| ~ spl154_185 ),
inference(avatar_component_clause,[],[f2072]) ).
fof(f2076,definition,
( spl154_186
<=> e1 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl154_186])],[avatar_definition]) ).
fof(f2077,plain,
( e1 = op(e4,e3)
| ~ spl154_186 ),
inference(avatar_component_clause,[],[f2076]) ).
fof(f2078,plain,
( e1 != op(e4,e3)
| spl154_186 ),
inference(avatar_component_clause,[],[f2076]) ).
fof(f2079,plain,
( spl154_185
| ~ spl154_186
| ~ spl154_96 ),
inference(avatar_split_clause,[],[f2070,f1459,f2076,f2072]) ).
fof(f2090,plain,
( e1 != op(e2,e3)
| e3 = op(e2,e1)
| ~ spl154_106 ),
inference(forward_subsumption_resolution,[],[f721,f1511]) ).
fof(f2095,definition,
( spl154_187
<=> e4 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl154_187])],[avatar_definition]) ).
fof(f2097,plain,
( e4 = op(e1,e1)
| ~ spl154_187 ),
inference(avatar_component_clause,[],[f2095]) ).
fof(f2099,definition,
( spl154_188
<=> e1 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl154_188])],[avatar_definition]) ).
fof(f2100,plain,
( e1 = op(e1,e4)
| ~ spl154_188 ),
inference(avatar_component_clause,[],[f2099]) ).
fof(f2101,plain,
( e1 != op(e1,e4)
| spl154_188 ),
inference(avatar_component_clause,[],[f2099]) ).
fof(f2102,plain,
( spl154_187
| ~ spl154_188
| ~ spl154_110 ),
inference(avatar_split_clause,[],[f2018,f1529,f2099,f2095]) ).
fof(f2116,plain,
( e1 != op(e4,e4)
| e4 = op(e4,e1)
| ~ spl154_95 ),
inference(forward_subsumption_resolution,[],[f743,f1456]) ).
fof(f2136,definition,
( spl154_191
<=> e4 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl154_191])],[avatar_definition]) ).
fof(f2137,plain,
( e4 != op(e0,e2)
| spl154_191 ),
inference(avatar_component_clause,[],[f2136]) ).
fof(f2138,plain,
( e4 = op(e0,e2)
| ~ spl154_191 ),
inference(avatar_component_clause,[],[f2136]) ).
fof(f2154,plain,
( e2 != op(e2,e4)
| e4 = op(e2,e2)
| ~ spl154_128 ),
inference(forward_subsumption_resolution,[],[f773,f1622]) ).
fof(f2155,plain,
( e3 = e4
| e2 != op(e2,e4)
| ~ spl154_128 ),
inference(forward_demodulation,[],[f2154,f980]) ).
fof(f2156,plain,
( e2 != op(e2,e4)
| ~ spl154_128 ),
inference(forward_subsumption_resolution,[],[f2155,f505]) ).
fof(f2172,definition,
( spl154_193
<=> e4 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl154_193])],[avatar_definition]) ).
fof(f2173,plain,
( e4 != op(e4,e2)
| spl154_193 ),
inference(avatar_component_clause,[],[f2172]) ).
fof(f2174,plain,
( e4 = op(e4,e2)
| ~ spl154_193 ),
inference(avatar_component_clause,[],[f2172]) ).
fof(f2176,definition,
( spl154_194
<=> e2 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl154_194])],[avatar_definition]) ).
fof(f2177,plain,
( e2 = op(e4,e4)
| ~ spl154_194 ),
inference(avatar_component_clause,[],[f2176]) ).
fof(f2178,plain,
( e2 != op(e4,e4)
| spl154_194 ),
inference(avatar_component_clause,[],[f2176]) ).
fof(f2200,plain,
( e2 = op(e2,e3)
| ~ sP61 ),
inference(forward_subsumption_resolution,[],[f819,f980]) ).
fof(f2211,plain,
( e3 != op(e3,e0)
| e0 = op(e3,e3)
| ~ spl154_150 ),
inference(forward_subsumption_resolution,[],[f825,f1733]) ).
fof(f2212,plain,
( e0 = e4
| e3 != op(e3,e0)
| ~ spl154_150 ),
inference(forward_demodulation,[],[f2211,f1832]) ).
fof(f2213,plain,
( e3 != op(e3,e0)
| ~ spl154_150 ),
inference(forward_subsumption_resolution,[],[f2212,f511]) ).
fof(f2226,definition,
( spl154_195
<=> e4 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl154_195])],[avatar_definition]) ).
fof(f2227,plain,
( e4 != op(e4,e3)
| spl154_195 ),
inference(avatar_component_clause,[],[f2226]) ).
fof(f2228,plain,
( e4 = op(e4,e3)
| ~ spl154_195 ),
inference(avatar_component_clause,[],[f2226]) ).
fof(f2230,definition,
( spl154_196
<=> e3 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl154_196])],[avatar_definition]) ).
fof(f2231,plain,
( e3 = op(e4,e4)
| ~ spl154_196 ),
inference(avatar_component_clause,[],[f2230]) ).
fof(f2232,plain,
( e3 != op(e4,e4)
| spl154_196 ),
inference(avatar_component_clause,[],[f2230]) ).
fof(f2237,plain,
( e4 != op(e3,e3)
| ~ spl154_195 ),
inference(superposition,[],[f465,f2228]) ).
fof(f2243,plain,
( $false
| ~ spl154_195 ),
inference(forward_subsumption_resolution,[],[f2237,f1832]) ).
fof(f2244,plain,
~ spl154_195,
inference(avatar_contradiction_clause,[],[f2243]) ).
fof(f2261,plain,
( e3 = op(e3,e4)
| ~ sP30 ),
inference(forward_subsumption_resolution,[],[f881,f1832]) ).
fof(f2263,definition,
( spl154_198
<=> sP30 ),
introduced(definition,[new_symbols(definition,[spl154_198])],[avatar_definition]) ).
fof(f2265,plain,
( ~ sP30
| spl154_198 ),
inference(avatar_component_clause,[],[f2263]) ).
fof(f2267,definition,
( spl154_199
<=> e3 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl154_199])],[avatar_definition]) ).
fof(f2268,plain,
( e3 != op(e3,e4)
| spl154_199 ),
inference(avatar_component_clause,[],[f2267]) ).
fof(f2269,plain,
( e3 = op(e3,e4)
| ~ spl154_199 ),
inference(avatar_component_clause,[],[f2267]) ).
fof(f2270,plain,
( ~ spl154_198
| spl154_199 ),
inference(avatar_split_clause,[],[f2261,f2267,f2263]) ).
fof(f2281,plain,
e0 = op(op(e3,e2),op(e3,e2)),
inference(forward_demodulation,[],[f518,f980]) ).
fof(f2282,plain,
e0 = op(e1,e1),
inference(forward_demodulation,[],[f2281,f1826]) ).
fof(f2288,plain,
( e1 != op(e4,e2)
| e2 = op(e4,e1)
| ~ spl154_97 ),
inference(forward_subsumption_resolution,[],[f739,f1466]) ).
fof(f2301,plain,
spl154_168,
inference(avatar_split_clause,[],[f2282,f1866]) ).
fof(f2302,plain,
( e0 = e4
| ~ spl154_168
| ~ spl154_187 ),
inference(superposition,[],[f1867,f2097]) ).
fof(f2303,plain,
( e0 != op(e1,e2)
| ~ spl154_168 ),
inference(superposition,[],[f440,f1867]) ).
fof(f2313,plain,
( $false
| ~ spl154_168
| ~ spl154_187 ),
inference(forward_subsumption_resolution,[],[f2302,f511]) ).
fof(f2314,plain,
( ~ spl154_168
| ~ spl154_187 ),
inference(avatar_contradiction_clause,[],[f2313]) ).
fof(f2317,plain,
( ~ spl154_178
| ~ spl154_168 ),
inference(avatar_split_clause,[],[f2303,f1866,f1966]) ).
fof(f2320,definition,
( spl154_201
<=> e4 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl154_201])],[avatar_definition]) ).
fof(f2321,plain,
( e4 != op(e4,e0)
| spl154_201 ),
inference(avatar_component_clause,[],[f2320]) ).
fof(f2322,plain,
( e4 = op(e4,e0)
| ~ spl154_201 ),
inference(avatar_component_clause,[],[f2320]) ).
fof(f2324,definition,
( spl154_202
<=> e0 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl154_202])],[avatar_definition]) ).
fof(f2325,plain,
( e0 = op(e4,e4)
| ~ spl154_202 ),
inference(avatar_component_clause,[],[f2324]) ).
fof(f2326,plain,
( e0 != op(e4,e4)
| spl154_202 ),
inference(avatar_component_clause,[],[f2324]) ).
fof(f2328,plain,
( e4 != op(e4,e2)
| ~ spl154_201 ),
inference(superposition,[],[f413,f2322]) ).
fof(f2337,plain,
( $false
| ~ spl154_193
| ~ spl154_201 ),
inference(forward_subsumption_resolution,[],[f2328,f2174]) ).
fof(f2338,plain,
( ~ spl154_193
| ~ spl154_201 ),
inference(avatar_contradiction_clause,[],[f2337]) ).
fof(f2347,definition,
( spl154_203
<=> e4 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl154_203])],[avatar_definition]) ).
fof(f2348,plain,
( e4 != op(e1,e2)
| spl154_203 ),
inference(avatar_component_clause,[],[f2347]) ).
fof(f2349,plain,
( e4 = op(e1,e2)
| ~ spl154_203 ),
inference(avatar_component_clause,[],[f2347]) ).
fof(f2351,definition,
( spl154_204
<=> e2 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl154_204])],[avatar_definition]) ).
fof(f2352,plain,
( e2 = op(e1,e4)
| ~ spl154_204 ),
inference(avatar_component_clause,[],[f2351]) ).
fof(f2353,plain,
( e2 != op(e1,e4)
| spl154_204 ),
inference(avatar_component_clause,[],[f2351]) ).
fof(f2374,plain,
( e1 = unit
| e2 = unit
| e3 = unit
| e4 = unit
| spl154_47 ),
inference(forward_subsumption_resolution,[],[f344,f1192]) ).
fof(f2375,plain,
( e2 = unit
| e3 = unit
| e4 = unit
| spl154_47
| spl154_53 ),
inference(forward_subsumption_resolution,[],[f2374,f1253]) ).
fof(f2376,plain,
( e3 = unit
| e4 = unit
| spl154_47
| spl154_53
| spl154_58 ),
inference(forward_subsumption_resolution,[],[f2375,f1276]) ).
fof(f2377,plain,
( e4 = unit
| spl154_47
| spl154_53
| spl154_58
| spl154_63 ),
inference(forward_subsumption_resolution,[],[f2376,f1298]) ).
fof(f2378,plain,
( $false
| spl154_47
| spl154_53
| spl154_58
| spl154_63
| spl154_68 ),
inference(forward_subsumption_resolution,[],[f2377,f1320]) ).
fof(f2379,plain,
( spl154_47
| spl154_53
| spl154_58
| spl154_63
| spl154_68 ),
inference(avatar_contradiction_clause,[],[f2378]) ).
fof(f2389,definition,
( spl154_208
<=> e4 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl154_208])],[avatar_definition]) ).
fof(f2390,plain,
( e4 = op(e0,e4)
| ~ spl154_208 ),
inference(avatar_component_clause,[],[f2389]) ).
fof(f2398,definition,
( spl154_210
<=> e4 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl154_210])],[avatar_definition]) ).
fof(f2399,plain,
( e4 = op(e1,e4)
| ~ spl154_210 ),
inference(avatar_component_clause,[],[f2398]) ).
fof(f2407,definition,
( spl154_212
<=> e4 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl154_212])],[avatar_definition]) ).
fof(f2409,plain,
( e4 != op(e2,e4)
| spl154_212 ),
inference(avatar_component_clause,[],[f2407]) ).
fof(f2416,definition,
( spl154_214
<=> e4 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl154_214])],[avatar_definition]) ).
fof(f2417,plain,
( e4 = op(e3,e4)
| ~ spl154_214 ),
inference(avatar_component_clause,[],[f2416]) ).
fof(f2418,plain,
( e4 != op(e3,e4)
| spl154_214 ),
inference(avatar_component_clause,[],[f2416]) ).
fof(f2425,definition,
( spl154_216
<=> e4 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl154_216])],[avatar_definition]) ).
fof(f2426,plain,
( e4 = op(e4,e4)
| ~ spl154_216 ),
inference(avatar_component_clause,[],[f2425]) ).
fof(f2433,plain,
( e2 = op(e2,e4)
| ~ spl154_68 ),
inference(superposition,[],[f349,f1319]) ).
fof(f2435,plain,
( e1 = op(e1,e4)
| ~ spl154_68 ),
inference(superposition,[],[f351,f1319]) ).
fof(f2445,plain,
( $false
| ~ spl154_68
| spl154_188 ),
inference(forward_subsumption_resolution,[],[f2435,f2101]) ).
fof(f2446,plain,
( ~ spl154_68
| spl154_188 ),
inference(avatar_contradiction_clause,[],[f2445]) ).
fof(f2447,plain,
( $false
| ~ spl154_68
| ~ spl154_128 ),
inference(forward_subsumption_resolution,[],[f2433,f2156]) ).
fof(f2448,plain,
( ~ spl154_68
| ~ spl154_128 ),
inference(avatar_contradiction_clause,[],[f2447]) ).
fof(f2480,plain,
( e3 = op(e3,e0)
| ~ spl154_47 ),
inference(superposition,[],[f347,f1191]) ).
fof(f2484,plain,
( e1 = op(e1,e0)
| ~ spl154_47 ),
inference(superposition,[],[f351,f1191]) ).
fof(f2486,plain,
( e0 = op(e0,e0)
| ~ spl154_47 ),
inference(superposition,[],[f353,f1191]) ).
fof(f2494,plain,
( $false
| ~ spl154_47
| spl154_48 ),
inference(forward_subsumption_resolution,[],[f2486,f1196]) ).
fof(f2495,plain,
( ~ spl154_47
| spl154_48 ),
inference(avatar_contradiction_clause,[],[f2494]) ).
fof(f2496,plain,
( $false
| ~ spl154_47
| spl154_167 ),
inference(forward_subsumption_resolution,[],[f2484,f1863]) ).
fof(f2497,plain,
( ~ spl154_47
| spl154_167 ),
inference(avatar_contradiction_clause,[],[f2496]) ).
fof(f2500,plain,
( $false
| ~ spl154_47
| ~ spl154_150 ),
inference(forward_subsumption_resolution,[],[f2480,f2213]) ).
fof(f2501,plain,
( ~ spl154_47
| ~ spl154_150 ),
inference(avatar_contradiction_clause,[],[f2500]) ).
fof(f2559,definition,
( spl154_219
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl154_219])],[avatar_definition]) ).
fof(f2560,plain,
( e2 = op(e0,e2)
| ~ spl154_219 ),
inference(avatar_component_clause,[],[f2559]) ).
fof(f2561,plain,
( e2 != op(e0,e2)
| spl154_219 ),
inference(avatar_component_clause,[],[f2559]) ).
fof(f2565,definition,
( spl154_220
<=> e2 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl154_220])],[avatar_definition]) ).
fof(f2566,plain,
( e2 = op(e4,e2)
| ~ spl154_220 ),
inference(avatar_component_clause,[],[f2565]) ).
fof(f2567,plain,
( e2 != op(e4,e2)
| spl154_220 ),
inference(avatar_component_clause,[],[f2565]) ).
fof(f2571,plain,
( e3 = op(e3,e2)
| ~ spl154_58 ),
inference(superposition,[],[f347,f1275]) ).
fof(f2590,plain,
( e1 = e3
| ~ spl154_58 ),
inference(forward_demodulation,[],[f2571,f1826]) ).
fof(f2595,plain,
( $false
| ~ spl154_58 ),
inference(forward_subsumption_resolution,[],[f2590,f509]) ).
fof(f2596,plain,
~ spl154_58,
inference(avatar_contradiction_clause,[],[f2595]) ).
fof(f2598,definition,
( spl154_221
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl154_221])],[avatar_definition]) ).
fof(f2599,plain,
( e3 = op(e0,e3)
| ~ spl154_221 ),
inference(avatar_component_clause,[],[f2598]) ).
fof(f2600,plain,
( e3 != op(e0,e3)
| spl154_221 ),
inference(avatar_component_clause,[],[f2598]) ).
fof(f2603,definition,
( spl154_222
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl154_222])],[avatar_definition]) ).
fof(f2604,plain,
( e3 = op(e1,e3)
| ~ spl154_222 ),
inference(avatar_component_clause,[],[f2603]) ).
fof(f2605,plain,
( e3 != op(e1,e3)
| spl154_222 ),
inference(avatar_component_clause,[],[f2603]) ).
fof(f2608,definition,
( spl154_223
<=> e3 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl154_223])],[avatar_definition]) ).
fof(f2610,plain,
( e3 != op(e2,e3)
| spl154_223 ),
inference(avatar_component_clause,[],[f2608]) ).
fof(f2614,definition,
( spl154_224
<=> e3 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl154_224])],[avatar_definition]) ).
fof(f2615,plain,
( e3 = op(e4,e3)
| ~ spl154_224 ),
inference(avatar_component_clause,[],[f2614]) ).
fof(f2616,plain,
( e3 != op(e4,e3)
| spl154_224 ),
inference(avatar_component_clause,[],[f2614]) ).
fof(f2618,plain,
( e4 = op(e4,e3)
| ~ spl154_63 ),
inference(superposition,[],[f345,f1297]) ).
fof(f2639,plain,
( $false
| ~ spl154_63
| spl154_195 ),
inference(forward_subsumption_resolution,[],[f2618,f2227]) ).
fof(f2640,plain,
( ~ spl154_63
| spl154_195 ),
inference(avatar_contradiction_clause,[],[f2639]) ).
fof(f2643,plain,
( e2 != op(e2,e0)
| e0 = op(e2,e2)
| ~ spl154_132 ),
inference(forward_subsumption_resolution,[],[f765,f1642]) ).
fof(f2648,plain,
( e0 = e3
| e2 != op(e2,e0)
| ~ spl154_132 ),
inference(forward_demodulation,[],[f2643,f980]) ).
fof(f2650,plain,
( e2 != op(e2,e0)
| ~ spl154_132 ),
inference(forward_subsumption_resolution,[],[f2648,f512]) ).
fof(f2652,definition,
( spl154_225
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl154_225])],[avatar_definition]) ).
fof(f2653,plain,
( e3 = op(e3,e0)
| ~ spl154_225 ),
inference(avatar_component_clause,[],[f2652]) ).
fof(f2657,definition,
( spl154_226
<=> e0 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl154_226])],[avatar_definition]) ).
fof(f2658,plain,
( e0 = op(e1,e3)
| ~ spl154_226 ),
inference(avatar_component_clause,[],[f2657]) ).
fof(f2659,plain,
( e0 != op(e1,e3)
| spl154_226 ),
inference(avatar_component_clause,[],[f2657]) ).
fof(f2662,definition,
( spl154_227
<=> e0 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl154_227])],[avatar_definition]) ).
fof(f2663,plain,
( e0 = op(e1,e4)
| ~ spl154_227 ),
inference(avatar_component_clause,[],[f2662]) ).
fof(f2664,plain,
( e0 != op(e1,e4)
| spl154_227 ),
inference(avatar_component_clause,[],[f2662]) ).
fof(f2667,plain,
( e4 = op(e0,e4)
| ~ spl154_47 ),
inference(superposition,[],[f346,f1191]) ).
fof(f2668,plain,
( e3 = op(e3,e0)
| ~ spl154_47 ),
inference(superposition,[],[f347,f1191]) ).
fof(f2669,plain,
( e3 = op(e0,e3)
| ~ spl154_47 ),
inference(superposition,[],[f348,f1191]) ).
fof(f2670,plain,
( e2 = op(e2,e0)
| ~ spl154_47 ),
inference(superposition,[],[f349,f1191]) ).
fof(f2671,plain,
( e2 = op(e0,e2)
| ~ spl154_47 ),
inference(superposition,[],[f350,f1191]) ).
fof(f2673,plain,
( e1 = op(e0,e1)
| ~ spl154_47 ),
inference(superposition,[],[f352,f1191]) ).
fof(f2680,plain,
( $false
| ~ spl154_47
| spl154_56 ),
inference(forward_subsumption_resolution,[],[f2673,f1266]) ).
fof(f2681,plain,
( ~ spl154_47
| spl154_56 ),
inference(avatar_contradiction_clause,[],[f2680]) ).
fof(f2682,plain,
( $false
| ~ spl154_47
| spl154_219 ),
inference(forward_subsumption_resolution,[],[f2671,f2561]) ).
fof(f2683,plain,
( ~ spl154_47
| spl154_219 ),
inference(avatar_contradiction_clause,[],[f2682]) ).
fof(f2684,plain,
( $false
| ~ spl154_47
| ~ spl154_132 ),
inference(forward_subsumption_resolution,[],[f2670,f2650]) ).
fof(f2685,plain,
( ~ spl154_47
| ~ spl154_132 ),
inference(avatar_contradiction_clause,[],[f2684]) ).
fof(f2686,plain,
( $false
| ~ spl154_47
| spl154_221 ),
inference(forward_subsumption_resolution,[],[f2669,f2600]) ).
fof(f2687,plain,
( ~ spl154_47
| spl154_221 ),
inference(avatar_contradiction_clause,[],[f2686]) ).
fof(f2717,plain,
( e3 != op(e2,e3)
| ~ spl154_221 ),
inference(superposition,[],[f473,f2599]) ).
fof(f2723,plain,
( spl154_208
| ~ spl154_47 ),
inference(avatar_split_clause,[],[f2667,f1190,f2389]) ).
fof(f2728,plain,
( e4 != op(e2,e4)
| ~ spl154_208 ),
inference(superposition,[],[f463,f2390]) ).
fof(f2733,plain,
( ~ spl154_212
| ~ spl154_208 ),
inference(avatar_split_clause,[],[f2728,f2389,f2407]) ).
fof(f2734,plain,
( spl154_225
| ~ spl154_47 ),
inference(avatar_split_clause,[],[f2668,f1190,f2652]) ).
fof(f2754,plain,
( e1 = op(e4,e4)
| e2 = op(e4,e4)
| e3 = op(e4,e4)
| e4 = op(e4,e4)
| spl154_202 ),
inference(forward_subsumption_resolution,[],[f319,f2326]) ).
fof(f2766,plain,
( e1 = op(e4,e4)
| e3 = op(e4,e4)
| e4 = op(e4,e4)
| spl154_194
| spl154_202 ),
inference(forward_subsumption_resolution,[],[f2754,f2178]) ).
fof(f2769,plain,
( e1 = op(e4,e4)
| e4 = op(e4,e4)
| spl154_194
| spl154_196
| spl154_202 ),
inference(forward_subsumption_resolution,[],[f2766,f2232]) ).
fof(f2771,definition,
( spl154_228
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl154_228])],[avatar_definition]) ).
fof(f2773,plain,
( e3 = op(e2,e1)
| ~ spl154_228 ),
inference(avatar_component_clause,[],[f2771]) ).
fof(f2775,definition,
( spl154_229
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl154_229])],[avatar_definition]) ).
fof(f2777,plain,
( e1 != op(e2,e3)
| spl154_229 ),
inference(avatar_component_clause,[],[f2775]) ).
fof(f2778,plain,
( spl154_228
| ~ spl154_229
| ~ spl154_106 ),
inference(avatar_split_clause,[],[f2090,f1509,f2775,f2771]) ).
fof(f2779,plain,
( e3 != op(e2,e2)
| ~ spl154_228 ),
inference(superposition,[],[f430,f2773]) ).
fof(f2785,plain,
( $false
| ~ spl154_228 ),
inference(forward_subsumption_resolution,[],[f2779,f980]) ).
fof(f2786,plain,
~ spl154_228,
inference(avatar_contradiction_clause,[],[f2785]) ).
fof(f2788,definition,
( spl154_230
<=> e4 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl154_230])],[avatar_definition]) ).
fof(f2790,plain,
( e4 = op(e4,e1)
| ~ spl154_230 ),
inference(avatar_component_clause,[],[f2788]) ).
fof(f2792,definition,
( spl154_231
<=> e1 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl154_231])],[avatar_definition]) ).
fof(f2794,plain,
( e1 != op(e4,e4)
| spl154_231 ),
inference(avatar_component_clause,[],[f2792]) ).
fof(f2795,plain,
( spl154_230
| ~ spl154_231
| ~ spl154_95 ),
inference(avatar_split_clause,[],[f2116,f1454,f2792,f2788]) ).
fof(f2797,plain,
( e4 != op(e4,e0)
| ~ spl154_230 ),
inference(superposition,[],[f414,f2790]) ).
fof(f2805,plain,
( $false
| ~ spl154_201
| ~ spl154_230 ),
inference(forward_subsumption_resolution,[],[f2797,f2322]) ).
fof(f2806,plain,
( ~ spl154_201
| ~ spl154_230 ),
inference(avatar_contradiction_clause,[],[f2805]) ).
fof(f2808,definition,
( spl154_232
<=> e2 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl154_232])],[avatar_definition]) ).
fof(f2809,plain,
( e2 != op(e4,e1)
| spl154_232 ),
inference(avatar_component_clause,[],[f2808]) ).
fof(f2810,plain,
( e2 = op(e4,e1)
| ~ spl154_232 ),
inference(avatar_component_clause,[],[f2808]) ).
fof(f2812,definition,
( spl154_233
<=> e1 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl154_233])],[avatar_definition]) ).
fof(f2814,plain,
( e1 != op(e4,e2)
| spl154_233 ),
inference(avatar_component_clause,[],[f2812]) ).
fof(f2815,plain,
( spl154_232
| ~ spl154_233
| ~ spl154_97 ),
inference(avatar_split_clause,[],[f2288,f1464,f2812,f2808]) ).
fof(f2818,plain,
( e2 != op(e3,e1)
| ~ spl154_232 ),
inference(superposition,[],[f485,f2810]) ).
fof(f2825,plain,
( $false
| ~ spl154_102
| ~ spl154_232 ),
inference(forward_subsumption_resolution,[],[f2818,f2050]) ).
fof(f2826,plain,
( ~ spl154_102
| ~ spl154_232 ),
inference(avatar_contradiction_clause,[],[f2825]) ).
fof(f2829,definition,
( spl154_234
<=> e3 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl154_234])],[avatar_definition]) ).
fof(f2830,plain,
( e3 != op(e4,e2)
| spl154_234 ),
inference(avatar_component_clause,[],[f2829]) ).
fof(f2831,plain,
( e3 = op(e4,e2)
| ~ spl154_234 ),
inference(avatar_component_clause,[],[f2829]) ).
fof(f2833,definition,
( spl154_235
<=> e2 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl154_235])],[avatar_definition]) ).
fof(f2835,plain,
( e2 != op(e4,e3)
| spl154_235 ),
inference(avatar_component_clause,[],[f2833]) ).
fof(f2838,plain,
( e3 != op(e2,e2)
| ~ spl154_234 ),
inference(superposition,[],[f476,f2831]) ).
fof(f2845,plain,
( $false
| ~ spl154_234 ),
inference(forward_subsumption_resolution,[],[f2838,f980]) ).
fof(f2846,plain,
~ spl154_234,
inference(avatar_contradiction_clause,[],[f2845]) ).
fof(f2848,plain,
( e4 = op(e4,e4)
| spl154_194
| spl154_196
| spl154_202
| spl154_231 ),
inference(forward_subsumption_resolution,[],[f2769,f2794]) ).
fof(f2849,plain,
( spl154_216
| spl154_194
| spl154_196
| spl154_202
| spl154_231 ),
inference(avatar_split_clause,[],[f2848,f2792,f2324,f2230,f2176,f2425]) ).
fof(f2853,plain,
( e2 != op(e4,e3)
| ~ spl154_194 ),
inference(superposition,[],[f405,f2177]) ).
fof(f2874,plain,
( ~ spl154_235
| ~ spl154_194 ),
inference(avatar_split_clause,[],[f2853,f2176,f2833]) ).
fof(f2876,plain,
( e0 = op(e4,e3)
| e2 = op(e4,e3)
| e3 = op(e4,e3)
| e4 = op(e4,e3)
| spl154_186 ),
inference(forward_subsumption_resolution,[],[f320,f2078]) ).
fof(f2878,plain,
( e0 = op(e4,e3)
| e2 = op(e4,e3)
| e4 = op(e4,e3)
| spl154_186
| spl154_224 ),
inference(forward_subsumption_resolution,[],[f2876,f2616]) ).
fof(f2879,plain,
( e0 = op(e4,e3)
| e2 = op(e4,e3)
| spl154_186
| spl154_195
| spl154_224 ),
inference(forward_subsumption_resolution,[],[f2878,f2227]) ).
fof(f2880,plain,
( e0 = op(e4,e3)
| spl154_186
| spl154_195
| spl154_224
| spl154_235 ),
inference(forward_subsumption_resolution,[],[f2879,f2835]) ).
fof(f2881,plain,
( e0 != op(e4,e2)
| spl154_186
| spl154_195
| spl154_224
| spl154_235 ),
inference(superposition,[],[f407,f2880]) ).
fof(f2902,plain,
( e0 = op(e4,e2)
| e2 = op(e4,e2)
| e3 = op(e4,e2)
| e4 = op(e4,e2)
| spl154_233 ),
inference(forward_subsumption_resolution,[],[f321,f2814]) ).
fof(f2904,plain,
( e0 = op(e4,e2)
| e3 = op(e4,e2)
| e4 = op(e4,e2)
| spl154_220
| spl154_233 ),
inference(forward_subsumption_resolution,[],[f2902,f2567]) ).
fof(f2905,plain,
( e0 = op(e4,e2)
| e4 = op(e4,e2)
| spl154_220
| spl154_233
| spl154_234 ),
inference(forward_subsumption_resolution,[],[f2904,f2830]) ).
fof(f2906,plain,
( e0 = op(e4,e2)
| spl154_193
| spl154_220
| spl154_233
| spl154_234 ),
inference(forward_subsumption_resolution,[],[f2905,f2173]) ).
fof(f2907,plain,
( $false
| spl154_186
| spl154_193
| spl154_195
| spl154_220
| spl154_224
| spl154_233
| spl154_234
| spl154_235 ),
inference(forward_subsumption_resolution,[],[f2906,f2881]) ).
fof(f2908,plain,
( spl154_186
| spl154_193
| spl154_195
| spl154_220
| spl154_224
| spl154_233
| spl154_234
| spl154_235 ),
inference(avatar_contradiction_clause,[],[f2907]) ).
fof(f2952,plain,
( e3 != op(e3,e0)
| ~ spl154_199 ),
inference(superposition,[],[f421,f2269]) ).
fof(f2959,plain,
( $false
| ~ spl154_199
| ~ spl154_225 ),
inference(forward_subsumption_resolution,[],[f2952,f2653]) ).
fof(f2960,plain,
( ~ spl154_199
| ~ spl154_225 ),
inference(avatar_contradiction_clause,[],[f2959]) ).
fof(f2965,plain,
( e0 = op(e3,e4)
| e2 = op(e3,e4)
| e3 = op(e3,e4)
| e4 = op(e3,e4)
| ~ spl154_100 ),
inference(forward_subsumption_resolution,[],[f324,f2066]) ).
fof(f2969,definition,
( spl154_236
<=> e0 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl154_236])],[avatar_definition]) ).
fof(f2970,plain,
( e0 != op(e3,e4)
| spl154_236 ),
inference(avatar_component_clause,[],[f2969]) ).
fof(f2971,plain,
( e0 = op(e3,e4)
| ~ spl154_236 ),
inference(avatar_component_clause,[],[f2969]) ).
fof(f2977,plain,
( e0 != op(e2,e4)
| ~ spl154_236 ),
inference(superposition,[],[f457,f2971]) ).
fof(f3011,plain,
( e1 = op(e2,e3)
| e2 = op(e2,e3)
| e3 = op(e2,e3)
| e4 = op(e2,e3)
| spl154_170 ),
inference(forward_subsumption_resolution,[],[f330,f1895]) ).
fof(f3012,plain,
( e2 = op(e2,e3)
| e3 = op(e2,e3)
| e4 = op(e2,e3)
| spl154_170
| spl154_229 ),
inference(forward_subsumption_resolution,[],[f3011,f2777]) ).
fof(f3013,plain,
( e2 = op(e2,e3)
| e4 = op(e2,e3)
| spl154_170
| spl154_223
| spl154_229 ),
inference(forward_subsumption_resolution,[],[f3012,f2610]) ).
fof(f3014,plain,
( e2 = op(e2,e3)
| spl154_170
| spl154_223
| spl154_229 ),
inference(forward_subsumption_resolution,[],[f3013,f1836]) ).
fof(f3017,plain,
( e2 != op(e2,e0)
| spl154_170
| spl154_223
| spl154_229 ),
inference(superposition,[],[f432,f3014]) ).
fof(f3022,plain,
( $false
| ~ spl154_47
| spl154_170
| spl154_223
| spl154_229 ),
inference(forward_subsumption_resolution,[],[f3017,f2670]) ).
fof(f3023,plain,
( ~ spl154_47
| spl154_170
| spl154_223
| spl154_229 ),
inference(avatar_contradiction_clause,[],[f3022]) ).
fof(f3026,plain,
( ~ spl154_223
| ~ spl154_221 ),
inference(avatar_split_clause,[],[f2717,f2598,f2608]) ).
fof(f3033,definition,
( spl154_237
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl154_237])],[avatar_definition]) ).
fof(f3034,plain,
( e2 != op(e2,e3)
| spl154_237 ),
inference(avatar_component_clause,[],[f3033]) ).
fof(f3035,plain,
( e2 = op(e2,e3)
| ~ spl154_237 ),
inference(avatar_component_clause,[],[f3033]) ).
fof(f3044,plain,
( e1 = op(e1,e4)
| e2 = op(e1,e4)
| e3 = op(e1,e4)
| e4 = op(e1,e4)
| spl154_227 ),
inference(forward_subsumption_resolution,[],[f334,f2664]) ).
fof(f3045,plain,
( e2 = op(e1,e4)
| e3 = op(e1,e4)
| e4 = op(e1,e4)
| spl154_188
| spl154_227 ),
inference(forward_subsumption_resolution,[],[f3044,f2101]) ).
fof(f3046,plain,
( e3 = op(e1,e4)
| e4 = op(e1,e4)
| spl154_188
| spl154_204
| spl154_227 ),
inference(forward_subsumption_resolution,[],[f3045,f2353]) ).
fof(f3050,definition,
( spl154_238
<=> e3 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl154_238])],[avatar_definition]) ).
fof(f3052,plain,
( e3 = op(e1,e4)
| ~ spl154_238 ),
inference(avatar_component_clause,[],[f3050]) ).
fof(f3053,plain,
( spl154_210
| spl154_238
| spl154_188
| spl154_204
| spl154_227 ),
inference(avatar_split_clause,[],[f3046,f2662,f2351,f2099,f3050,f2398]) ).
fof(f3064,plain,
( e1 = op(e1,e3)
| e2 = op(e1,e3)
| e3 = op(e1,e3)
| e4 = op(e1,e3)
| spl154_226 ),
inference(forward_subsumption_resolution,[],[f335,f2659]) ).
fof(f3065,plain,
( e2 = op(e1,e3)
| e3 = op(e1,e3)
| e4 = op(e1,e3)
| spl154_182
| spl154_226 ),
inference(forward_subsumption_resolution,[],[f3064,f2009]) ).
fof(f3066,plain,
( e3 = op(e1,e3)
| e4 = op(e1,e3)
| spl154_51
| ~ spl154_102
| spl154_182
| spl154_226 ),
inference(forward_subsumption_resolution,[],[f3065,f2056]) ).
fof(f3067,plain,
( e4 = op(e1,e3)
| spl154_51
| ~ spl154_102
| spl154_182
| spl154_222
| spl154_226 ),
inference(forward_subsumption_resolution,[],[f3066,f2605]) ).
fof(f3068,plain,
( $false
| spl154_51
| ~ spl154_102
| spl154_182
| spl154_222
| spl154_226 ),
inference(forward_subsumption_resolution,[],[f3067,f1837]) ).
fof(f3069,plain,
( spl154_51
| ~ spl154_102
| spl154_182
| spl154_222
| spl154_226 ),
inference(avatar_contradiction_clause,[],[f3068]) ).
fof(f3077,plain,
( e4 != op(e0,e4)
| ~ spl154_210 ),
inference(superposition,[],[f464,f2399]) ).
fof(f3082,plain,
( $false
| ~ spl154_208
| ~ spl154_210 ),
inference(forward_subsumption_resolution,[],[f3077,f2390]) ).
fof(f3083,plain,
( ~ spl154_208
| ~ spl154_210 ),
inference(avatar_contradiction_clause,[],[f3082]) ).
fof(f3096,plain,
( e3 != op(e0,e3)
| ~ spl154_222 ),
inference(superposition,[],[f474,f2604]) ).
fof(f3104,plain,
( $false
| ~ spl154_221
| ~ spl154_222 ),
inference(forward_subsumption_resolution,[],[f3096,f2599]) ).
fof(f3105,plain,
( ~ spl154_221
| ~ spl154_222 ),
inference(avatar_contradiction_clause,[],[f3104]) ).
fof(f3108,plain,
( e0 = op(e1,e3)
| e2 = op(e1,e3)
| e3 = op(e1,e3)
| e4 = op(e1,e3)
| spl154_182 ),
inference(forward_subsumption_resolution,[],[f335,f2009]) ).
fof(f3116,plain,
( e0 != op(e1,e1)
| ~ spl154_226 ),
inference(superposition,[],[f439,f2658]) ).
fof(f3130,plain,
( $false
| ~ spl154_168
| ~ spl154_226 ),
inference(forward_subsumption_resolution,[],[f3116,f1867]) ).
fof(f3131,plain,
( ~ spl154_168
| ~ spl154_226 ),
inference(avatar_contradiction_clause,[],[f3130]) ).
fof(f3133,plain,
( e2 = op(e1,e3)
| ~ spl154_51
| ~ spl154_102 ),
inference(forward_demodulation,[],[f1243,f2050]) ).
fof(f3141,plain,
( e0 = op(e2,e2)
| ~ sP22
| ~ spl154_219 ),
inference(forward_demodulation,[],[f898,f2560]) ).
fof(f3151,plain,
( e0 = e3
| ~ sP22
| ~ spl154_219 ),
inference(forward_demodulation,[],[f3141,f980]) ).
fof(f3156,plain,
( ~ sP22
| ~ spl154_219 ),
inference(forward_subsumption_resolution,[],[f3151,f512]) ).
fof(f3280,plain,
( e0 != op(e1,e1)
| spl154_15
| ~ spl154_167 ),
inference(forward_demodulation,[],[f1048,f1864]) ).
fof(f3286,plain,
( $false
| spl154_15
| ~ spl154_167
| ~ spl154_168 ),
inference(forward_subsumption_resolution,[],[f3280,f1867]) ).
fof(f3287,plain,
( spl154_15
| ~ spl154_167
| ~ spl154_168 ),
inference(avatar_contradiction_clause,[],[f3286]) ).
fof(f3339,plain,
( e4 != op(e1,e2)
| spl154_29
| ~ spl154_184 ),
inference(forward_demodulation,[],[f1111,f2035]) ).
fof(f3345,plain,
( $false
| spl154_29
| ~ spl154_184
| ~ spl154_203 ),
inference(forward_subsumption_resolution,[],[f3339,f2349]) ).
fof(f3346,plain,
( spl154_29
| ~ spl154_184
| ~ spl154_203 ),
inference(avatar_contradiction_clause,[],[f3345]) ).
fof(f3410,plain,
( ~ spl154_8
| ~ spl154_219 ),
inference(avatar_split_clause,[],[f3156,f2559,f1015]) ).
fof(f3480,plain,
( e4 = op(e1,e3)
| ~ sP1
| ~ spl154_186 ),
inference(forward_demodulation,[],[f961,f2077]) ).
fof(f3483,plain,
( ~ sP1
| ~ spl154_186 ),
inference(forward_subsumption_resolution,[],[f3480,f1837]) ).
fof(f3486,plain,
( ~ spl154_44
| ~ spl154_186 ),
inference(avatar_split_clause,[],[f3483,f2076,f1177]) ).
fof(f3487,plain,
( e3 != op(e1,e4)
| ~ sP15
| ~ spl154_185 ),
inference(forward_demodulation,[],[f920,f2074]) ).
fof(f3540,plain,
( ~ spl154_20
| ~ spl154_238
| ~ spl154_185 ),
inference(avatar_split_clause,[],[f3487,f2072,f3050,f1069]) ).
fof(f3542,plain,
( e2 != op(e0,e2)
| ~ sP14
| ~ spl154_47 ),
inference(forward_demodulation,[],[f923,f2670]) ).
fof(f3548,plain,
( ~ sP14
| ~ spl154_47
| ~ spl154_219 ),
inference(forward_subsumption_resolution,[],[f3542,f2560]) ).
fof(f3587,plain,
( ~ spl154_22
| ~ spl154_47
| ~ spl154_219 ),
inference(avatar_split_clause,[],[f3548,f2559,f1190,f1078]) ).
fof(f3590,plain,
( e4 = op(e0,e2)
| ~ sP2
| spl154_193
| spl154_220
| spl154_233
| spl154_234 ),
inference(forward_demodulation,[],[f958,f2906]) ).
fof(f3594,plain,
( ~ sP2
| spl154_191
| spl154_193
| spl154_220
| spl154_233
| spl154_234 ),
inference(forward_subsumption_resolution,[],[f3590,f2137]) ).
fof(f3602,plain,
( ~ spl154_42
| spl154_191
| spl154_193
| spl154_220
| spl154_233
| spl154_234 ),
inference(avatar_split_clause,[],[f3594,f2829,f2812,f2565,f2172,f2136,f1168]) ).
fof(f3603,plain,
( e4 != op(e4,e0)
| spl154_13
| ~ spl154_208 ),
inference(forward_demodulation,[],[f1039,f2390]) ).
fof(f3609,plain,
( $false
| spl154_13
| ~ spl154_201
| ~ spl154_208 ),
inference(forward_subsumption_resolution,[],[f3603,f2322]) ).
fof(f3610,plain,
( spl154_13
| ~ spl154_201
| ~ spl154_208 ),
inference(avatar_contradiction_clause,[],[f3609]) ).
fof(f3673,plain,
( e4 != op(e0,e4)
| ~ sP4
| ~ spl154_201 ),
inference(forward_demodulation,[],[f953,f2322]) ).
fof(f3678,plain,
( ~ sP4
| ~ spl154_201
| ~ spl154_208 ),
inference(forward_subsumption_resolution,[],[f3673,f2390]) ).
fof(f3686,plain,
( ~ spl154_38
| ~ spl154_201
| ~ spl154_208 ),
inference(avatar_split_clause,[],[f3678,f2389,f2320,f1150]) ).
fof(f3688,plain,
( e4 != op(e1,e2)
| ~ sP17
| ~ spl154_183 ),
inference(forward_demodulation,[],[f914,f2032]) ).
fof(f3693,plain,
( ~ sP17
| ~ spl154_183
| ~ spl154_203 ),
inference(forward_subsumption_resolution,[],[f3688,f2349]) ).
fof(f3742,plain,
( ~ spl154_16
| ~ spl154_183
| ~ spl154_203 ),
inference(avatar_split_clause,[],[f3693,f2347,f2030,f1051]) ).
fof(f3744,plain,
( e3 != op(e0,e3)
| ~ sP9
| ~ spl154_225 ),
inference(forward_demodulation,[],[f938,f2653]) ).
fof(f3750,plain,
( ~ sP9
| ~ spl154_221
| ~ spl154_225 ),
inference(forward_subsumption_resolution,[],[f3744,f2599]) ).
fof(f3775,plain,
( ~ spl154_30
| ~ spl154_221
| ~ spl154_225 ),
inference(avatar_split_clause,[],[f3750,f2652,f2598,f1114]) ).
fof(f3777,plain,
( e3 != op(e0,e3)
| ~ sP21
| ~ spl154_225 ),
inference(forward_demodulation,[],[f902,f2653]) ).
fof(f3781,plain,
( e0 != op(op(e0,e0),e0)
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0
| spl154_6 ),
inference(forward_subsumption_resolution,[],[f966,f1008]) ).
fof(f3784,plain,
( ~ sP21
| ~ spl154_221
| ~ spl154_225 ),
inference(forward_subsumption_resolution,[],[f3777,f2599]) ).
fof(f3788,plain,
( e0 != op(op(e0,e0),e0)
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0
| spl154_6
| spl154_8 ),
inference(forward_subsumption_resolution,[],[f3781,f1017]) ).
fof(f3792,plain,
( e0 != op(op(e0,e0),e0)
| sP21
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0
| spl154_6
| spl154_8
| spl154_12 ),
inference(forward_subsumption_resolution,[],[f3788,f1035]) ).
fof(f3795,plain,
( e0 != op(op(e0,e0),e0)
| sP21
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0
| spl154_6
| spl154_8
| spl154_12
| spl154_14 ),
inference(forward_subsumption_resolution,[],[f3792,f1044]) ).
fof(f3798,plain,
( e0 != op(op(e0,e0),e0)
| sP21
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0
| spl154_6
| spl154_8
| spl154_12
| spl154_14 ),
inference(forward_subsumption_resolution,[],[f3795,f974]) ).
fof(f3849,plain,
( e2 = e4
| ~ spl154_191
| ~ spl154_219 ),
inference(forward_demodulation,[],[f2138,f2560]) ).
fof(f3857,plain,
( $false
| ~ spl154_191
| ~ spl154_219 ),
inference(forward_subsumption_resolution,[],[f3849,f506]) ).
fof(f3858,plain,
( ~ spl154_191
| ~ spl154_219 ),
inference(avatar_contradiction_clause,[],[f3857]) ).
fof(f3869,plain,
( e0 != op(op(e0,e0),e0)
| sP21
| sP17
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0
| spl154_6
| spl154_8
| spl154_12
| spl154_14
| spl154_18 ),
inference(forward_subsumption_resolution,[],[f3798,f1062]) ).
fof(f3872,plain,
( e0 != op(op(e0,e0),e0)
| sP21
| sP17
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0
| spl154_6
| spl154_8
| spl154_12
| spl154_14
| spl154_18
| spl154_20 ),
inference(forward_subsumption_resolution,[],[f3869,f1071]) ).
fof(f3875,plain,
( e0 != op(op(e0,e0),e0)
| sP21
| sP17
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0
| spl154_6
| spl154_8
| spl154_12
| spl154_14
| spl154_18
| spl154_20
| spl154_22 ),
inference(forward_subsumption_resolution,[],[f3872,f1080]) ).
fof(f3878,plain,
( e0 != op(op(e0,e0),e0)
| sP21
| sP17
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0
| spl154_6
| spl154_8
| spl154_12
| spl154_14
| spl154_18
| spl154_20
| spl154_22
| spl154_24 ),
inference(forward_subsumption_resolution,[],[f3875,f1089]) ).
fof(f3881,plain,
( e0 != op(op(e0,e0),e0)
| sP21
| sP17
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0
| spl154_6
| spl154_8
| spl154_12
| spl154_14
| spl154_18
| spl154_20
| spl154_22
| spl154_24 ),
inference(forward_subsumption_resolution,[],[f3878,f973]) ).
fof(f3884,plain,
( e0 != op(op(e0,e0),e0)
| sP21
| sP17
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0
| spl154_6
| spl154_8
| spl154_12
| spl154_14
| spl154_18
| spl154_20
| spl154_22
| spl154_24
| spl154_26 ),
inference(forward_subsumption_resolution,[],[f3881,f1098]) ).
fof(f3887,plain,
( e0 != op(op(e0,e0),e0)
| sP21
| sP17
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0
| spl154_6
| spl154_8
| spl154_12
| spl154_14
| spl154_18
| spl154_20
| spl154_22
| spl154_24
| spl154_26
| spl154_28 ),
inference(forward_subsumption_resolution,[],[f3884,f1107]) ).
fof(f3890,plain,
( e0 != op(op(e0,e0),e0)
| sP21
| sP17
| sP9
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0
| spl154_6
| spl154_8
| spl154_12
| spl154_14
| spl154_18
| spl154_20
| spl154_22
| spl154_24
| spl154_26
| spl154_28
| spl154_32 ),
inference(forward_subsumption_resolution,[],[f3887,f1125]) ).
fof(f3893,plain,
( e0 != op(op(e0,e0),e0)
| sP21
| sP17
| sP9
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0
| spl154_6
| spl154_8
| spl154_12
| spl154_14
| spl154_18
| spl154_20
| spl154_22
| spl154_24
| spl154_26
| spl154_28
| spl154_32
| spl154_34 ),
inference(forward_subsumption_resolution,[],[f3890,f1134]) ).
fof(f3896,plain,
( e0 != op(op(e0,e0),e0)
| sP21
| sP17
| sP9
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0
| spl154_6
| spl154_8
| spl154_12
| spl154_14
| spl154_18
| spl154_20
| spl154_22
| spl154_24
| spl154_26
| spl154_28
| spl154_32
| spl154_34 ),
inference(forward_subsumption_resolution,[],[f3893,f972]) ).
fof(f3899,plain,
( e0 != op(op(e0,e0),e0)
| sP21
| sP17
| sP9
| sP4
| sP3
| sP2
| sP1
| sP0
| spl154_6
| spl154_8
| spl154_12
| spl154_14
| spl154_18
| spl154_20
| spl154_22
| spl154_24
| spl154_26
| spl154_28
| spl154_32
| spl154_34
| spl154_36 ),
inference(forward_subsumption_resolution,[],[f3896,f1143]) ).
fof(f3902,plain,
( e0 != op(op(e0,e0),e0)
| sP21
| sP17
| sP9
| sP3
| sP2
| sP1
| sP0
| spl154_6
| spl154_8
| spl154_12
| spl154_14
| spl154_18
| spl154_20
| spl154_22
| spl154_24
| spl154_26
| spl154_28
| spl154_32
| spl154_34
| spl154_36
| spl154_38 ),
inference(forward_subsumption_resolution,[],[f3899,f1152]) ).
fof(f3904,plain,
( e0 != op(op(e0,e0),e0)
| sP21
| sP17
| sP9
| sP2
| sP1
| sP0
| spl154_6
| spl154_8
| spl154_12
| spl154_14
| spl154_18
| spl154_20
| spl154_22
| spl154_24
| spl154_26
| spl154_28
| spl154_32
| spl154_34
| spl154_36
| spl154_38
| spl154_40 ),
inference(forward_subsumption_resolution,[],[f3902,f1161]) ).
fof(f3906,plain,
( e0 != op(op(e0,e0),e0)
| sP21
| sP17
| sP9
| sP2
| sP0
| spl154_6
| spl154_8
| spl154_12
| spl154_14
| spl154_18
| spl154_20
| spl154_22
| spl154_24
| spl154_26
| spl154_28
| spl154_32
| spl154_34
| spl154_36
| spl154_38
| spl154_40
| spl154_44 ),
inference(forward_subsumption_resolution,[],[f3904,f1179]) ).
fof(f3908,plain,
( e0 != op(op(e0,e0),e0)
| sP21
| sP17
| sP9
| sP2
| spl154_6
| spl154_8
| spl154_12
| spl154_14
| spl154_18
| spl154_20
| spl154_22
| spl154_24
| spl154_26
| spl154_28
| spl154_32
| spl154_34
| spl154_36
| spl154_38
| spl154_40
| spl154_44 ),
inference(forward_subsumption_resolution,[],[f3906,f971]) ).
fof(f3909,plain,
( e0 != op(e0,e0)
| sP21
| sP17
| sP9
| sP2
| spl154_6
| spl154_8
| spl154_12
| spl154_14
| spl154_18
| spl154_20
| spl154_22
| spl154_24
| spl154_26
| spl154_28
| spl154_32
| spl154_34
| spl154_36
| spl154_38
| spl154_40
| spl154_44
| ~ spl154_48 ),
inference(forward_demodulation,[],[f3908,f1195]) ).
fof(f3910,plain,
( sP21
| sP17
| sP9
| sP2
| spl154_6
| spl154_8
| spl154_12
| spl154_14
| spl154_18
| spl154_20
| spl154_22
| spl154_24
| spl154_26
| spl154_28
| spl154_32
| spl154_34
| spl154_36
| spl154_38
| spl154_40
| spl154_44
| ~ spl154_48 ),
inference(forward_subsumption_resolution,[],[f3909,f1195]) ).
fof(f3911,plain,
( ~ spl154_10
| ~ spl154_221
| ~ spl154_225 ),
inference(avatar_split_clause,[],[f3784,f2652,f2598,f1024]) ).
fof(f3918,plain,
( sP17
| sP9
| sP2
| spl154_6
| spl154_8
| spl154_10
| spl154_12
| spl154_14
| spl154_18
| spl154_20
| spl154_22
| spl154_24
| spl154_26
| spl154_28
| spl154_32
| spl154_34
| spl154_36
| spl154_38
| spl154_40
| spl154_44
| ~ spl154_48 ),
inference(forward_subsumption_resolution,[],[f3910,f1026]) ).
fof(f3919,plain,
( sP17
| sP2
| spl154_6
| spl154_8
| spl154_10
| spl154_12
| spl154_14
| spl154_18
| spl154_20
| spl154_22
| spl154_24
| spl154_26
| spl154_28
| spl154_30
| spl154_32
| spl154_34
| spl154_36
| spl154_38
| spl154_40
| spl154_44
| ~ spl154_48 ),
inference(forward_subsumption_resolution,[],[f3918,f1116]) ).
fof(f3920,plain,
( sP17
| spl154_6
| spl154_8
| spl154_10
| spl154_12
| spl154_14
| spl154_18
| spl154_20
| spl154_22
| spl154_24
| spl154_26
| spl154_28
| spl154_30
| spl154_32
| spl154_34
| spl154_36
| spl154_38
| spl154_40
| spl154_42
| spl154_44
| ~ spl154_48 ),
inference(forward_subsumption_resolution,[],[f3919,f1170]) ).
fof(f3921,plain,
( spl154_16
| spl154_6
| spl154_8
| spl154_10
| spl154_12
| spl154_14
| spl154_18
| spl154_20
| spl154_22
| spl154_24
| spl154_26
| spl154_28
| spl154_30
| spl154_32
| spl154_34
| spl154_36
| spl154_38
| spl154_40
| spl154_42
| spl154_44
| ~ spl154_48 ),
inference(avatar_split_clause,[],[f3920,f1194,f1177,f1168,f1159,f1150,f1141,f1132,f1123,f1114,f1105,f1096,f1087,f1078,f1069,f1060,f1042,f1033,f1024,f1015,f1006,f1051]) ).
fof(f3926,plain,
( e3 != op(e1,e2)
| ~ spl154_238 ),
inference(superposition,[],[f436,f3052]) ).
fof(f3937,plain,
( e2 != op(e1,e2)
| ~ spl154_51
| ~ spl154_102 ),
inference(superposition,[],[f437,f3133]) ).
fof(f3958,plain,
( e1 = op(e1,e2)
| e2 = op(e1,e2)
| e3 = op(e1,e2)
| e4 = op(e1,e2)
| spl154_178 ),
inference(forward_subsumption_resolution,[],[f336,f1968]) ).
fof(f3959,plain,
( e2 = op(e1,e2)
| e3 = op(e1,e2)
| e4 = op(e1,e2)
| spl154_178 ),
inference(forward_subsumption_resolution,[],[f3958,f1828]) ).
fof(f3960,plain,
( e3 = op(e1,e2)
| e4 = op(e1,e2)
| ~ spl154_51
| ~ spl154_102
| spl154_178 ),
inference(forward_subsumption_resolution,[],[f3959,f3937]) ).
fof(f3961,plain,
( e4 = op(e1,e2)
| ~ spl154_51
| ~ spl154_102
| spl154_178
| ~ spl154_238 ),
inference(forward_subsumption_resolution,[],[f3960,f3926]) ).
fof(f3962,plain,
( $false
| ~ spl154_51
| ~ spl154_102
| spl154_178
| spl154_203
| ~ spl154_238 ),
inference(forward_subsumption_resolution,[],[f3961,f2348]) ).
fof(f3963,plain,
( ~ spl154_51
| ~ spl154_102
| spl154_178
| spl154_203
| ~ spl154_238 ),
inference(avatar_contradiction_clause,[],[f3962]) ).
fof(f3968,plain,
( e2 = op(e4,e1)
| ~ sP13
| ~ spl154_183 ),
inference(forward_demodulation,[],[f925,f2032]) ).
fof(f3973,plain,
( ~ sP13
| ~ spl154_183
| spl154_232 ),
inference(forward_subsumption_resolution,[],[f3968,f2809]) ).
fof(f4012,plain,
( ~ spl154_24
| ~ spl154_183
| spl154_232 ),
inference(avatar_split_clause,[],[f3973,f2808,f2030,f1087]) ).
fof(f4015,plain,
( e4 = op(e3,e1)
| ~ sP3
| ~ spl154_185 ),
inference(forward_demodulation,[],[f955,f2074]) ).
fof(f4019,plain,
( ~ sP3
| ~ spl154_185 ),
inference(forward_subsumption_resolution,[],[f4015,f1834]) ).
fof(f4030,plain,
( ~ spl154_40
| ~ spl154_185 ),
inference(avatar_split_clause,[],[f4019,f2072,f1159]) ).
fof(f4057,plain,
( e3 != op(e1,e4)
| ~ spl154_196 ),
inference(superposition,[],[f458,f2231]) ).
fof(f4063,plain,
( ~ spl154_238
| ~ spl154_196 ),
inference(avatar_split_clause,[],[f4057,f2230,f3050]) ).
fof(f4072,plain,
( e2 != op(e1,e3)
| ~ spl154_204 ),
inference(superposition,[],[f435,f2352]) ).
fof(f4141,plain,
( e2 != op(e1,e3)
| spl154_35 ),
inference(forward_demodulation,[],[f1138,f1826]) ).
fof(f4144,plain,
( e2 = op(e1,e3)
| e3 = op(e1,e3)
| e4 = op(e1,e3)
| spl154_182
| spl154_226 ),
inference(forward_subsumption_resolution,[],[f3108,f2659]) ).
fof(f4145,plain,
( e3 = op(e1,e3)
| e4 = op(e1,e3)
| spl154_182
| ~ spl154_204
| spl154_226 ),
inference(forward_subsumption_resolution,[],[f4144,f4072]) ).
fof(f4146,plain,
( e3 = op(e1,e3)
| spl154_182
| ~ spl154_204
| spl154_226 ),
inference(forward_subsumption_resolution,[],[f4145,f1837]) ).
fof(f4147,plain,
( spl154_222
| spl154_182
| ~ spl154_204
| spl154_226 ),
inference(avatar_split_clause,[],[f4146,f2657,f2351,f2007,f2603]) ).
fof(f4161,plain,
( e0 = op(e2,e4)
| e2 = op(e2,e4)
| e3 = op(e2,e4)
| e4 = op(e2,e4)
| spl154_184 ),
inference(forward_subsumption_resolution,[],[f329,f2036]) ).
fof(f4165,plain,
( ~ spl154_172
| ~ spl154_236 ),
inference(avatar_split_clause,[],[f2977,f2969,f1907]) ).
fof(f4167,definition,
( spl154_244
<=> e3 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl154_244])],[avatar_definition]) ).
fof(f4168,plain,
( e3 != op(e2,e4)
| spl154_244 ),
inference(avatar_component_clause,[],[f4167]) ).
fof(f4192,plain,
( e1 = op(e1,e1)
| ~ spl154_53 ),
inference(superposition,[],[f351,f1252]) ).
fof(f4205,plain,
( e0 = e1
| ~ spl154_53
| ~ spl154_168 ),
inference(forward_demodulation,[],[f4192,f1867]) ).
fof(f4214,plain,
( $false
| ~ spl154_53
| ~ spl154_168 ),
inference(forward_subsumption_resolution,[],[f4205,f514]) ).
fof(f4215,plain,
( ~ spl154_53
| ~ spl154_168 ),
inference(avatar_contradiction_clause,[],[f4214]) ).
fof(f4216,plain,
( e1 = op(e1,e3)
| e2 = op(e1,e3)
| e3 = op(e1,e3)
| e4 = op(e1,e3)
| spl154_226 ),
inference(forward_subsumption_resolution,[],[f335,f2659]) ).
fof(f4222,plain,
( ~ sP149
| spl154_198 ),
inference(forward_subsumption_resolution,[],[f625,f2265]) ).
fof(f4231,plain,
( ~ spl154_1
| spl154_198 ),
inference(avatar_split_clause,[],[f4222,f2263,f985]) ).
fof(f4236,plain,
( e4 != unit
| ~ sP30 ),
inference(forward_subsumption_resolution,[],[f880,f1832]) ).
fof(f4241,plain,
( e0 = op(e2,e4)
| e2 = op(e2,e4)
| e3 = op(e2,e4)
| spl154_184
| spl154_212 ),
inference(forward_subsumption_resolution,[],[f4161,f2409]) ).
fof(f4256,plain,
( e1 = op(e1,e3)
| e2 = op(e1,e3)
| e3 = op(e1,e3)
| spl154_226 ),
inference(forward_subsumption_resolution,[],[f4216,f1837]) ).
fof(f4262,plain,
( ~ spl154_198
| ~ spl154_68 ),
inference(avatar_split_clause,[],[f4236,f1318,f2263]) ).
fof(f4313,plain,
( e1 = op(e1,e3)
| e3 = op(e1,e3)
| spl154_35
| spl154_226 ),
inference(forward_subsumption_resolution,[],[f4256,f4141]) ).
fof(f4314,plain,
( e1 = op(e1,e3)
| spl154_35
| spl154_222
| spl154_226 ),
inference(forward_subsumption_resolution,[],[f4313,f2605]) ).
fof(f4315,plain,
( spl154_182
| spl154_35
| spl154_222
| spl154_226 ),
inference(avatar_split_clause,[],[f4314,f2657,f2603,f1136,f2007]) ).
fof(f4319,plain,
( e3 = op(e4,e3)
| ~ spl154_68 ),
inference(superposition,[],[f348,f1319]) ).
fof(f4332,plain,
( $false
| ~ spl154_68
| spl154_224 ),
inference(forward_subsumption_resolution,[],[f4319,f2616]) ).
fof(f4333,plain,
( ~ spl154_68
| spl154_224 ),
inference(avatar_contradiction_clause,[],[f4332]) ).
fof(f4370,plain,
( e1 != op(e1,e0)
| ~ spl154_182 ),
inference(superposition,[],[f442,f2008]) ).
fof(f4378,plain,
( $false
| ~ spl154_167
| ~ spl154_182 ),
inference(forward_subsumption_resolution,[],[f4370,f1864]) ).
fof(f4379,plain,
( ~ spl154_167
| ~ spl154_182 ),
inference(avatar_contradiction_clause,[],[f4378]) ).
fof(f4381,plain,
( e2 = op(e1,e3)
| ~ spl154_35 ),
inference(forward_demodulation,[],[f1137,f1826]) ).
fof(f4385,plain,
( e1 != op(e1,e3)
| ~ spl154_188 ),
inference(superposition,[],[f435,f2100]) ).
fof(f4388,plain,
( e1 != op(e1,e0)
| ~ spl154_188 ),
inference(superposition,[],[f441,f2100]) ).
fof(f4395,plain,
( $false
| ~ spl154_167
| ~ spl154_188 ),
inference(forward_subsumption_resolution,[],[f4388,f1864]) ).
fof(f4396,plain,
( ~ spl154_167
| ~ spl154_188 ),
inference(avatar_contradiction_clause,[],[f4395]) ).
fof(f4406,plain,
( e2 != op(e2,e3)
| ~ spl154_35 ),
inference(superposition,[],[f470,f4381]) ).
fof(f4413,plain,
( $false
| ~ spl154_35
| ~ spl154_237 ),
inference(forward_subsumption_resolution,[],[f4406,f3035]) ).
fof(f4414,plain,
( ~ spl154_35
| ~ spl154_237 ),
inference(avatar_contradiction_clause,[],[f4413]) ).
fof(f4418,plain,
( ~ spl154_182
| ~ spl154_188 ),
inference(avatar_split_clause,[],[f4385,f2099,f2007]) ).
fof(f4424,plain,
( e4 != op(e4,e0)
| ~ spl154_216 ),
inference(superposition,[],[f411,f2426]) ).
fof(f4435,plain,
( $false
| ~ spl154_201
| ~ spl154_216 ),
inference(forward_subsumption_resolution,[],[f4424,f2322]) ).
fof(f4436,plain,
( ~ spl154_201
| ~ spl154_216 ),
inference(avatar_contradiction_clause,[],[f4435]) ).
fof(f4496,plain,
( e2 != op(e0,e2)
| ~ spl154_220 ),
inference(superposition,[],[f481,f2566]) ).
fof(f4501,plain,
( $false
| ~ spl154_219
| ~ spl154_220 ),
inference(forward_subsumption_resolution,[],[f4496,f2560]) ).
fof(f4502,plain,
( ~ spl154_219
| ~ spl154_220 ),
inference(avatar_contradiction_clause,[],[f4501]) ).
fof(f4522,plain,
( e3 != op(e1,e3)
| ~ spl154_224 ),
inference(superposition,[],[f468,f2615]) ).
fof(f4523,plain,
( e3 != op(e0,e3)
| ~ spl154_224 ),
inference(superposition,[],[f471,f2615]) ).
fof(f4527,plain,
( $false
| ~ spl154_222
| ~ spl154_224 ),
inference(forward_subsumption_resolution,[],[f4522,f2604]) ).
fof(f4528,plain,
( ~ spl154_222
| ~ spl154_224 ),
inference(avatar_contradiction_clause,[],[f4527]) ).
fof(f4530,plain,
( e2 = op(e1,e3)
| ~ spl154_35 ),
inference(forward_demodulation,[],[f1137,f1826]) ).
fof(f4531,plain,
( e2 = op(e2,e3)
| ~ spl154_153 ),
inference(forward_subsumption_resolution,[],[f2200,f1748]) ).
fof(f4709,definition,
( spl154_248
<=> op(e0,e1) = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl154_248])],[avatar_definition]) ).
fof(f4711,plain,
( op(e0,e1) != op(e1,e0)
| spl154_248 ),
inference(avatar_component_clause,[],[f4709]) ).
fof(f4712,plain,
( ~ spl154_6
| ~ spl154_248 ),
inference(avatar_split_clause,[],[f896,f4709,f1006]) ).
fof(f4734,plain,
( $false
| ~ spl154_153
| spl154_237 ),
inference(forward_subsumption_resolution,[],[f4531,f3034]) ).
fof(f4735,plain,
( ~ spl154_153
| spl154_237 ),
inference(avatar_contradiction_clause,[],[f4734]) ).
fof(f4737,plain,
( e2 != op(e3,e1)
| ~ sP8
| ~ spl154_35 ),
inference(forward_demodulation,[],[f941,f4530]) ).
fof(f4750,definition,
( spl154_249
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl154_249])],[avatar_definition]) ).
fof(f4751,plain,
( e2 = op(e3,e1)
| ~ spl154_249 ),
inference(avatar_component_clause,[],[f4750]) ).
fof(f4752,plain,
( e2 != op(e3,e1)
| spl154_249 ),
inference(avatar_component_clause,[],[f4750]) ).
fof(f4753,plain,
( ~ spl154_32
| ~ spl154_249
| ~ spl154_35 ),
inference(avatar_split_clause,[],[f4737,f1136,f4750,f1123]) ).
fof(f4757,plain,
( ~ spl154_221
| ~ spl154_224 ),
inference(avatar_split_clause,[],[f4523,f2614,f2598]) ).
fof(f4779,plain,
( e4 = op(e4,e0)
| ~ spl154_47 ),
inference(superposition,[],[f345,f1191]) ).
fof(f4793,plain,
( $false
| ~ spl154_47
| spl154_201 ),
inference(forward_subsumption_resolution,[],[f4779,f2321]) ).
fof(f4794,plain,
( ~ spl154_47
| spl154_201 ),
inference(avatar_contradiction_clause,[],[f4793]) ).
fof(f4801,plain,
( ~ sP106
| spl154_249 ),
inference(forward_subsumption_resolution,[],[f2049,f4752]) ).
fof(f4802,plain,
( $false
| ~ spl154_102
| spl154_249 ),
inference(forward_subsumption_resolution,[],[f4801,f1491]) ).
fof(f4803,plain,
( ~ spl154_102
| spl154_249 ),
inference(avatar_contradiction_clause,[],[f4802]) ).
fof(f4876,plain,
( e1 != op(e0,e1)
| ~ spl154_167
| spl154_248 ),
inference(superposition,[],[f4711,f1864]) ).
fof(f4877,plain,
( $false
| ~ spl154_56
| ~ spl154_167
| spl154_248 ),
inference(forward_subsumption_resolution,[],[f4876,f1265]) ).
fof(f4878,plain,
( ~ spl154_56
| ~ spl154_167
| spl154_248 ),
inference(avatar_contradiction_clause,[],[f4877]) ).
fof(f4943,plain,
( e4 != op(e3,e3)
| ~ spl154_214 ),
inference(superposition,[],[f415,f2417]) ).
fof(f4957,plain,
( $false
| ~ spl154_214 ),
inference(forward_subsumption_resolution,[],[f4943,f1832]) ).
fof(f4958,plain,
~ spl154_214,
inference(avatar_contradiction_clause,[],[f4957]) ).
fof(f4961,plain,
( e2 = op(e3,e4)
| e3 = op(e3,e4)
| e4 = op(e3,e4)
| ~ spl154_100
| spl154_236 ),
inference(forward_subsumption_resolution,[],[f2965,f2970]) ).
fof(f4963,plain,
( e2 = op(e3,e4)
| e4 = op(e3,e4)
| ~ spl154_100
| spl154_199
| spl154_236 ),
inference(forward_subsumption_resolution,[],[f4961,f2268]) ).
fof(f4974,plain,
( e0 != op(e1,e1)
| ~ spl154_227 ),
inference(superposition,[],[f438,f2663]) ).
fof(f4982,plain,
( $false
| ~ spl154_168
| ~ spl154_227 ),
inference(forward_subsumption_resolution,[],[f4974,f1867]) ).
fof(f4983,plain,
( ~ spl154_168
| ~ spl154_227 ),
inference(avatar_contradiction_clause,[],[f4982]) ).
fof(f4991,plain,
( e3 != op(e2,e4)
| ~ spl154_238 ),
inference(superposition,[],[f460,f3052]) ).
fof(f5002,plain,
( e2 = op(e3,e4)
| ~ spl154_100
| spl154_199
| spl154_214
| spl154_236 ),
inference(forward_subsumption_resolution,[],[f4963,f2418]) ).
fof(f5009,plain,
( e0 != op(e3,e4)
| ~ spl154_202 ),
inference(superposition,[],[f455,f2325]) ).
fof(f5024,plain,
( e2 != op(e3,e1)
| ~ spl154_100
| spl154_199
| spl154_214
| spl154_236 ),
inference(superposition,[],[f418,f5002]) ).
fof(f5033,plain,
( $false
| ~ spl154_100
| spl154_199
| spl154_214
| spl154_236
| ~ spl154_249 ),
inference(forward_subsumption_resolution,[],[f5024,f4751]) ).
fof(f5034,plain,
( ~ spl154_100
| spl154_199
| spl154_214
| spl154_236
| ~ spl154_249 ),
inference(avatar_contradiction_clause,[],[f5033]) ).
fof(f5039,plain,
( ~ spl154_236
| ~ spl154_202 ),
inference(avatar_split_clause,[],[f5009,f2324,f2969]) ).
fof(f5045,plain,
( e2 != op(e2,e4)
| ~ spl154_194 ),
inference(superposition,[],[f456,f2177]) ).
fof(f5103,plain,
( e2 = op(e2,e4)
| e3 = op(e2,e4)
| spl154_172
| spl154_184
| spl154_212 ),
inference(forward_subsumption_resolution,[],[f4241,f1909]) ).
fof(f5104,plain,
( e3 = op(e2,e4)
| spl154_172
| spl154_184
| ~ spl154_194
| spl154_212 ),
inference(forward_subsumption_resolution,[],[f5103,f5045]) ).
fof(f5105,plain,
( $false
| spl154_172
| spl154_184
| ~ spl154_194
| spl154_212
| spl154_244 ),
inference(forward_subsumption_resolution,[],[f5104,f4168]) ).
fof(f5106,plain,
( spl154_172
| spl154_184
| ~ spl154_194
| spl154_212
| spl154_244 ),
inference(avatar_contradiction_clause,[],[f5105]) ).
fof(f5107,plain,
( ~ spl154_244
| ~ spl154_238 ),
inference(avatar_split_clause,[],[f4991,f3050,f4167]) ).
fof(f5111,plain,
( e2 = op(e0,e3)
| ~ sP11
| ~ spl154_170 ),
inference(forward_demodulation,[],[f931,f1894]) ).
fof(f5117,plain,
( e2 = e3
| ~ sP11
| ~ spl154_170
| ~ spl154_221 ),
inference(forward_demodulation,[],[f5111,f2599]) ).
fof(f5122,plain,
( ~ sP11
| ~ spl154_170
| ~ spl154_221 ),
inference(forward_subsumption_resolution,[],[f5117,f507]) ).
fof(f5150,plain,
( ~ spl154_26
| ~ spl154_170
| ~ spl154_221 ),
inference(avatar_split_clause,[],[f5122,f2598,f1893,f1096]) ).
fof(f5154,plain,
( e3 = op(e0,e4)
| ~ sP5
| ~ spl154_236 ),
inference(forward_demodulation,[],[f949,f2971]) ).
fof(f5158,plain,
( e3 = e4
| ~ sP5
| ~ spl154_208
| ~ spl154_236 ),
inference(forward_demodulation,[],[f5154,f2390]) ).
fof(f5162,plain,
( ~ sP5
| ~ spl154_208
| ~ spl154_236 ),
inference(forward_subsumption_resolution,[],[f5158,f505]) ).
fof(f5176,plain,
( ~ spl154_36
| ~ spl154_208
| ~ spl154_236 ),
inference(avatar_split_clause,[],[f5162,f2969,f2389,f1141]) ).
cnf(s720,plain,
( spl154_1
| spl154_2
| spl154_3
| spl154_4
| spl154_5 ),
inference(sat_conversion,[],[f1004]) ).
cnf(s767,plain,
( ~ spl154_12
| ~ spl154_13 ),
inference(sat_conversion,[],[f1040]) ).
cnf(s771,plain,
( ~ spl154_14
| ~ spl154_15 ),
inference(sat_conversion,[],[f1049]) ).
cnf(s799,plain,
( ~ spl154_28
| ~ spl154_29 ),
inference(sat_conversion,[],[f1112]) ).
cnf(s811,plain,
( ~ spl154_34
| ~ spl154_35 ),
inference(sat_conversion,[],[f1139]) ).
cnf(s835,plain,
( ~ spl154_46
| ~ spl154_47
| ~ spl154_48 ),
inference(sat_conversion,[],[f1197]) ).
cnf(s849,plain,
( ~ spl154_18
| ~ spl154_51 ),
inference(sat_conversion,[],[f1245]) ).
cnf(s961,plain,
( ~ spl154_5
| spl154_90 ),
inference(sat_conversion,[],[f1429]) ).
cnf(s986,plain,
( ~ spl154_5
| spl154_46 ),
inference(sat_conversion,[],[f1452]) ).
cnf(s991,plain,
( ~ spl154_4
| spl154_95 ),
inference(sat_conversion,[],[f1457]) ).
cnf(s995,plain,
( ~ spl154_4
| spl154_96 ),
inference(sat_conversion,[],[f1462]) ).
cnf(s999,plain,
( ~ spl154_4
| spl154_97 ),
inference(sat_conversion,[],[f1467]) ).
cnf(s1011,plain,
( ~ spl154_4
| spl154_100 ),
inference(sat_conversion,[],[f1482]) ).
cnf(s1019,plain,
( ~ spl154_4
| spl154_102 ),
inference(sat_conversion,[],[f1492]) ).
cnf(s1031,plain,
( ~ spl154_4
| spl154_105 ),
inference(sat_conversion,[],[f1507]) ).
cnf(s1035,plain,
( ~ spl154_4
| spl154_106 ),
inference(sat_conversion,[],[f1512]) ).
cnf(s1051,plain,
( ~ spl154_4
| spl154_110 ),
inference(sat_conversion,[],[f1532]) ).
cnf(s1127,plain,
( ~ spl154_3
| spl154_128 ),
inference(sat_conversion,[],[f1623]) ).
cnf(s1143,plain,
( ~ spl154_3
| spl154_132 ),
inference(sat_conversion,[],[f1643]) ).
cnf(s1219,plain,
( ~ spl154_2
| spl154_150 ),
inference(sat_conversion,[],[f1734]) ).
cnf(s1231,plain,
( ~ spl154_2
| spl154_153 ),
inference(sat_conversion,[],[f1749]) ).
cnf(s1407,plain,
( ~ spl154_90
| spl154_167
| ~ spl154_168 ),
inference(sat_conversion,[],[f1869]) ).
cnf(s1522,plain,
( ~ spl154_105
| spl154_183
| ~ spl154_184 ),
inference(sat_conversion,[],[f2037]) ).
cnf(s1557,plain,
( ~ spl154_96
| spl154_185
| ~ spl154_186 ),
inference(sat_conversion,[],[f2079]) ).
cnf(s1574,plain,
( ~ spl154_110
| spl154_187
| ~ spl154_188 ),
inference(sat_conversion,[],[f2102]) ).
cnf(s1668,plain,
~ spl154_195,
inference(sat_conversion,[],[f2244]) ).
cnf(s1681,plain,
( ~ spl154_198
| spl154_199 ),
inference(sat_conversion,[],[f2270]) ).
cnf(s1722,plain,
spl154_168,
inference(sat_conversion,[],[f2301]) ).
cnf(s1727,plain,
( ~ spl154_168
| ~ spl154_187 ),
inference(sat_conversion,[],[f2314]) ).
cnf(s1735,plain,
( ~ spl154_168
| ~ spl154_178 ),
inference(sat_conversion,[],[f2317]) ).
cnf(s1746,plain,
( ~ spl154_193
| ~ spl154_201 ),
inference(sat_conversion,[],[f2338]) ).
cnf(s1776,plain,
( spl154_47
| spl154_53
| spl154_58
| spl154_63
| spl154_68 ),
inference(sat_conversion,[],[f2379]) ).
cnf(s1808,plain,
( ~ spl154_68
| spl154_188 ),
inference(sat_conversion,[],[f2446]) ).
cnf(s1810,plain,
( ~ spl154_68
| ~ spl154_128 ),
inference(sat_conversion,[],[f2448]) ).
cnf(s1838,plain,
( ~ spl154_47
| spl154_48 ),
inference(sat_conversion,[],[f2495]) ).
cnf(s1840,plain,
( ~ spl154_47
| spl154_167 ),
inference(sat_conversion,[],[f2497]) ).
cnf(s1844,plain,
( ~ spl154_47
| ~ spl154_150 ),
inference(sat_conversion,[],[f2501]) ).
cnf(s1911,plain,
~ spl154_58,
inference(sat_conversion,[],[f2596]) ).
cnf(s1954,plain,
( ~ spl154_63
| spl154_195 ),
inference(sat_conversion,[],[f2640]) ).
cnf(s1996,plain,
( ~ spl154_47
| spl154_56 ),
inference(sat_conversion,[],[f2681]) ).
cnf(s1998,plain,
( ~ spl154_47
| spl154_219 ),
inference(sat_conversion,[],[f2683]) ).
cnf(s1999,plain,
( ~ spl154_47
| ~ spl154_132 ),
inference(sat_conversion,[],[f2685]) ).
cnf(s2000,plain,
( ~ spl154_47
| spl154_221 ),
inference(sat_conversion,[],[f2687]) ).
cnf(s2021,plain,
( ~ spl154_47
| spl154_208 ),
inference(sat_conversion,[],[f2723]) ).
cnf(s2026,plain,
( ~ spl154_208
| ~ spl154_212 ),
inference(sat_conversion,[],[f2733]) ).
cnf(s2030,plain,
( ~ spl154_47
| spl154_225 ),
inference(sat_conversion,[],[f2734]) ).
cnf(s2057,plain,
( ~ spl154_106
| spl154_228
| ~ spl154_229 ),
inference(sat_conversion,[],[f2778]) ).
cnf(s2060,plain,
~ spl154_228,
inference(sat_conversion,[],[f2786]) ).
cnf(s2066,plain,
( ~ spl154_95
| spl154_230
| ~ spl154_231 ),
inference(sat_conversion,[],[f2795]) ).
cnf(s2069,plain,
( ~ spl154_201
| ~ spl154_230 ),
inference(sat_conversion,[],[f2806]) ).
cnf(s2075,plain,
( ~ spl154_97
| spl154_232
| ~ spl154_233 ),
inference(sat_conversion,[],[f2815]) ).
cnf(s2078,plain,
( ~ spl154_102
| ~ spl154_232 ),
inference(sat_conversion,[],[f2826]) ).
cnf(s2087,plain,
~ spl154_234,
inference(sat_conversion,[],[f2846]) ).
cnf(s2094,plain,
( spl154_194
| spl154_196
| spl154_202
| spl154_216
| spl154_231 ),
inference(sat_conversion,[],[f2849]) ).
cnf(s2109,plain,
( ~ spl154_194
| ~ spl154_235 ),
inference(sat_conversion,[],[f2874]) ).
cnf(s2127,plain,
( spl154_186
| spl154_193
| spl154_195
| spl154_220
| spl154_224
| spl154_233
| spl154_234
| spl154_235 ),
inference(sat_conversion,[],[f2908]) ).
cnf(s2140,plain,
( ~ spl154_199
| ~ spl154_225 ),
inference(sat_conversion,[],[f2960]) ).
cnf(s2164,plain,
( ~ spl154_47
| spl154_170
| spl154_223
| spl154_229 ),
inference(sat_conversion,[],[f3023]) ).
cnf(s2169,plain,
( ~ spl154_221
| ~ spl154_223 ),
inference(sat_conversion,[],[f3026]) ).
cnf(s2190,plain,
( spl154_188
| spl154_204
| spl154_210
| spl154_227
| spl154_238 ),
inference(sat_conversion,[],[f3053]) ).
cnf(s2193,plain,
( spl154_51
| ~ spl154_102
| spl154_182
| spl154_222
| spl154_226 ),
inference(sat_conversion,[],[f3069]) ).
cnf(s2203,plain,
( ~ spl154_208
| ~ spl154_210 ),
inference(sat_conversion,[],[f3083]) ).
cnf(s2214,plain,
( ~ spl154_221
| ~ spl154_222 ),
inference(sat_conversion,[],[f3105]) ).
cnf(s2234,plain,
( ~ spl154_168
| ~ spl154_226 ),
inference(sat_conversion,[],[f3131]) ).
cnf(s2257,plain,
( spl154_15
| ~ spl154_167
| ~ spl154_168 ),
inference(sat_conversion,[],[f3287]) ).
cnf(s2264,plain,
( spl154_29
| ~ spl154_184
| ~ spl154_203 ),
inference(sat_conversion,[],[f3346]) ).
cnf(s2276,plain,
( ~ spl154_8
| ~ spl154_219 ),
inference(sat_conversion,[],[f3410]) ).
cnf(s2311,plain,
( ~ spl154_44
| ~ spl154_186 ),
inference(sat_conversion,[],[f3486]) ).
cnf(s2328,plain,
( ~ spl154_20
| ~ spl154_185
| ~ spl154_238 ),
inference(sat_conversion,[],[f3540]) ).
cnf(s2337,plain,
( ~ spl154_22
| ~ spl154_47
| ~ spl154_219 ),
inference(sat_conversion,[],[f3587]) ).
cnf(s2346,plain,
( ~ spl154_42
| spl154_191
| spl154_193
| spl154_220
| spl154_233
| spl154_234 ),
inference(sat_conversion,[],[f3602]) ).
cnf(s2349,plain,
( spl154_13
| ~ spl154_201
| ~ spl154_208 ),
inference(sat_conversion,[],[f3610]) ).
cnf(s2364,plain,
( ~ spl154_38
| ~ spl154_201
| ~ spl154_208 ),
inference(sat_conversion,[],[f3686]) ).
cnf(s2374,plain,
( ~ spl154_16
| ~ spl154_183
| ~ spl154_203 ),
inference(sat_conversion,[],[f3742]) ).
cnf(s2383,plain,
( ~ spl154_30
| ~ spl154_221
| ~ spl154_225 ),
inference(sat_conversion,[],[f3775]) ).
cnf(s2394,plain,
( ~ spl154_191
| ~ spl154_219 ),
inference(sat_conversion,[],[f3858]) ).
cnf(s2411,plain,
( ~ spl154_10
| ~ spl154_221
| ~ spl154_225 ),
inference(sat_conversion,[],[f3911]) ).
cnf(s2427,plain,
( spl154_6
| spl154_8
| spl154_10
| spl154_12
| spl154_14
| spl154_16
| spl154_18
| spl154_20
| spl154_22
| spl154_24
| spl154_26
| spl154_28
| spl154_30
| spl154_32
| spl154_34
| spl154_36
| spl154_38
| spl154_40
| spl154_42
| spl154_44
| ~ spl154_48 ),
inference(sat_conversion,[],[f3921]) ).
cnf(s2449,plain,
( ~ spl154_51
| ~ spl154_102
| spl154_178
| spl154_203
| ~ spl154_238 ),
inference(sat_conversion,[],[f3963]) ).
cnf(s2468,plain,
( ~ spl154_24
| ~ spl154_183
| spl154_232 ),
inference(sat_conversion,[],[f4012]) ).
cnf(s2478,plain,
( ~ spl154_40
| ~ spl154_185 ),
inference(sat_conversion,[],[f4030]) ).
cnf(s2523,plain,
( ~ spl154_196
| ~ spl154_238 ),
inference(sat_conversion,[],[f4063]) ).
cnf(s2615,plain,
( spl154_182
| ~ spl154_204
| spl154_222
| spl154_226 ),
inference(sat_conversion,[],[f4147]) ).
cnf(s2635,plain,
( ~ spl154_172
| ~ spl154_236 ),
inference(sat_conversion,[],[f4165]) ).
cnf(s2658,plain,
( ~ spl154_53
| ~ spl154_168 ),
inference(sat_conversion,[],[f4215]) ).
cnf(s2700,plain,
( ~ spl154_1
| spl154_198 ),
inference(sat_conversion,[],[f4231]) ).
cnf(s2733,plain,
( ~ spl154_68
| ~ spl154_198 ),
inference(sat_conversion,[],[f4262]) ).
cnf(s2801,plain,
( spl154_35
| spl154_182
| spl154_222
| spl154_226 ),
inference(sat_conversion,[],[f4315]) ).
cnf(s2813,plain,
( ~ spl154_68
| spl154_224 ),
inference(sat_conversion,[],[f4333]) ).
cnf(s2841,plain,
( ~ spl154_167
| ~ spl154_182 ),
inference(sat_conversion,[],[f4379]) ).
cnf(s2854,plain,
( ~ spl154_167
| ~ spl154_188 ),
inference(sat_conversion,[],[f4396]) ).
cnf(s2863,plain,
( ~ spl154_35
| ~ spl154_237 ),
inference(sat_conversion,[],[f4414]) ).
cnf(s2869,plain,
( ~ spl154_182
| ~ spl154_188 ),
inference(sat_conversion,[],[f4418]) ).
cnf(s2878,plain,
( ~ spl154_201
| ~ spl154_216 ),
inference(sat_conversion,[],[f4436]) ).
cnf(s2912,plain,
( ~ spl154_219
| ~ spl154_220 ),
inference(sat_conversion,[],[f4502]) ).
cnf(s2917,plain,
( ~ spl154_222
| ~ spl154_224 ),
inference(sat_conversion,[],[f4528]) ).
cnf(s2988,plain,
( ~ spl154_6
| ~ spl154_248 ),
inference(sat_conversion,[],[f4712]) ).
cnf(s3002,plain,
( ~ spl154_153
| spl154_237 ),
inference(sat_conversion,[],[f4735]) ).
cnf(s3064,plain,
( ~ spl154_32
| ~ spl154_35
| ~ spl154_249 ),
inference(sat_conversion,[],[f4753]) ).
cnf(s3082,plain,
( ~ spl154_221
| ~ spl154_224 ),
inference(sat_conversion,[],[f4757]) ).
cnf(s3120,plain,
( ~ spl154_47
| spl154_201 ),
inference(sat_conversion,[],[f4794]) ).
cnf(s3125,plain,
( ~ spl154_102
| spl154_249 ),
inference(sat_conversion,[],[f4803]) ).
cnf(s3159,plain,
( ~ spl154_56
| ~ spl154_167
| spl154_248 ),
inference(sat_conversion,[],[f4878]) ).
cnf(s3176,plain,
~ spl154_214,
inference(sat_conversion,[],[f4958]) ).
cnf(s3187,plain,
( ~ spl154_168
| ~ spl154_227 ),
inference(sat_conversion,[],[f4983]) ).
cnf(s3213,plain,
( ~ spl154_100
| spl154_199
| spl154_214
| spl154_236
| ~ spl154_249 ),
inference(sat_conversion,[],[f5034]) ).
cnf(s3218,plain,
( ~ spl154_202
| ~ spl154_236 ),
inference(sat_conversion,[],[f5039]) ).
cnf(s3237,plain,
( spl154_172
| spl154_184
| ~ spl154_194
| spl154_212
| spl154_244 ),
inference(sat_conversion,[],[f5106]) ).
cnf(s3244,plain,
( ~ spl154_238
| ~ spl154_244 ),
inference(sat_conversion,[],[f5107]) ).
cnf(s3263,plain,
( ~ spl154_26
| ~ spl154_170
| ~ spl154_221 ),
inference(sat_conversion,[],[f5150]) ).
cnf(s3273,plain,
( ~ spl154_36
| ~ spl154_208
| ~ spl154_236 ),
inference(sat_conversion,[],[f5176]) ).
cnf(s3278,plain,
( ~ spl154_106
| ~ spl154_229 ),
inference(rat,[],[s2057,s2060]) ).
cnf(s3279,plain,
( spl154_47
| spl154_53
| spl154_63
| spl154_68 ),
inference(rat,[],[s1776,s1911]) ).
cnf(s3280,plain,
~ spl154_227,
inference(rat,[],[s3187,s1722]) ).
cnf(s3281,plain,
~ spl154_53,
inference(rat,[],[s2658,s1722]) ).
cnf(s3282,plain,
~ spl154_226,
inference(rat,[],[s2234,s1722]) ).
cnf(s3283,plain,
~ spl154_178,
inference(rat,[],[s1735,s1722]) ).
cnf(s3284,plain,
~ spl154_187,
inference(rat,[],[s1727,s1722]) ).
cnf(s3285,plain,
~ spl154_63,
inference(rat,[],[s1954,s1668]) ).
cnf(s3289,plain,
( ~ spl154_110
| ~ spl154_188 ),
inference(rat,[],[s1574,s3284]) ).
cnf(s3292,plain,
( ~ spl154_90
| spl154_167 ),
inference(rat,[],[s1407,s1722]) ).
cnf(s3293,plain,
~ spl154_5,
inference(rat,[],[s835,s1838,s3279,s1808,s2854,s3292,s961,s986,s3281,s3285]) ).
cnf(s3294,plain,
~ spl154_4,
inference(rat,[],[s2427,s2328,s2478,s2374,s2468,s799,s1557,s2311,s1522,s2264,s2127,s3237,s2109,s2094,s2523,s3244,s849,s2449,s3263,s2190,s3064,s811,s3273,s2635,s3218,s771,s2193,s2988,s2346,s2164,s2615,s2801,s3213,s2066,s767,s2257,s2841,s3159,s2337,s2276,s2394,s2912,s2169,s2214,s2383,s2411,s3082,s2026,s2203,s2140,s1746,s2069,s2349,s2364,s2878,s1838,s1840,s1996,s1998,s2000,s2021,s2030,s3120,s3279,s2075,s1808,s2078,s3125,s3278,s3289,s991,s995,s999,s1011,s1019,s1031,s1035,s1051,s1668,s2087,s3283,s3280,s3282,s3176,s1722,s3281,s3285]) ).
cnf(s3295,plain,
~ spl154_3,
inference(rat,[],[s3279,s1810,s1999,s1127,s1143,s3281,s3285]) ).
cnf(s3296,plain,
~ spl154_2,
inference(rat,[],[s2801,s2869,s2917,s1808,s2813,s3279,s2863,s1844,s3002,s1219,s1231,s3282,s3281,s3285]) ).
cnf(s3297,plain,
spl154_1,
inference(rat,[],[s720,s3293,s3294,s3295,s3296]) ).
cnf(s3298,plain,
spl154_198,
inference(rat,[],[s2700,s3297]) ).
cnf(s3300,plain,
~ spl154_68,
inference(rat,[],[s2733,s3298]) ).
cnf(s3301,plain,
spl154_199,
inference(rat,[],[s1681,s3298]) ).
cnf(s3302,plain,
spl154_47,
inference(rat,[],[s3279,s3285,s3281,s3300]) ).
cnf(s3304,plain,
~ spl154_225,
inference(rat,[],[s2140,s3301]) ).
cnf(s3315,plain,
$false,
inference(rat,[],[s2030,s3304,s3302]) ).
fof(f5177,plain,
$false,
inference(avatar_sat_refutation,[],[s3315]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG059+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.18 % Computer : n001.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 19:28:34 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.21 Running first-order model finding
% 0.07/0.21 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.96/0.38 % (649966)Will run a generic schedule for satisfiability detection.
% 0.96/0.38 % (649976)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1945902415:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.96/0.38 % (649972)% WARNING: option uhcvi not known.
% 0.96/0.38 % (649971)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1629141750_2999 on theBenchmark for (2999ds/0Mi)
% 0.96/0.38 % (649973)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3270496532:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.96/0.38 % (649974)dis+10_1_sil=32000:sp=arity:random_seed=462907633:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.96/0.38 % (649972)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2588206124:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.96/0.38 % (649977)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=56277509:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.96/0.38 % (649975)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3917004587:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.96/0.38 % (649976)Instruction limit reached!
% 0.96/0.38 % (649976)------------------------------
% 0.96/0.38 % (649976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.96/0.38 % (649976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.96/0.38 % (649976)CaDiCaL version: 2.1.3
% 0.96/0.38 % (649976)Termination reason: Instruction limit
% 0.96/0.38 % (649976)Termination phase: Saturation
% 0.96/0.38 % (649976)Time elapsed: 0.035 s
% 0.96/0.38 % (649976)Peak memory usage: 14 MB
% 0.96/0.38 % (649976)Instructions burned: 134 (million)
% 0.96/0.38 % Detected minimum model sizes of [5]
% 0.96/0.38 % Detected maximum model sizes of [max]
% 0.96/0.38 % TRYING [5]
% 0.96/0.38 % (649985)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3615873452:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.96/0.38 % (649974)Instruction limit reached!
% 0.96/0.38 % (649974)------------------------------
% 0.96/0.38 % (649974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.96/0.38 % (649974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.96/0.38 % (649974)CaDiCaL version: 2.1.3
% 0.96/0.38 % (649974)Termination reason: Instruction limit
% 0.96/0.38 % (649974)Termination phase: Saturation
% 0.96/0.38 % (649974)Time elapsed: 0.053 s
% 0.96/0.38 % (649974)Peak memory usage: 13 MB
% 0.96/0.38 % (649974)Instructions burned: 104 (million)
% 0.96/0.38 % Detected minimum model sizes of [5]
% 0.96/0.38 % Detected maximum model sizes of [max]
% 0.96/0.38 % TRYING [5]
% 0.96/0.38 % TRYING [6]
% 0.96/0.38 % (649975)Instruction limit reached!
% 0.96/0.38 % (649975)------------------------------
% 0.96/0.38 % (649975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.96/0.38 % (649975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.96/0.38 % (649975)CaDiCaL version: 2.1.3
% 0.96/0.38 % (649975)Termination reason: Instruction limit
% 0.96/0.38 % (649975)Termination phase: Saturation
% 0.96/0.38 % (649975)Time elapsed: 0.059 s
% 0.96/0.38 % (649975)Peak memory usage: 13 MB
% 0.96/0.38 % (649975)Instructions burned: 117 (million)
% 0.96/0.38 % TRYING [6]
% 0.96/0.38 % (649987)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3351292474:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.96/0.38 % (649988)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3003209692:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 0.96/0.38 % (649977)Instruction limit reached!
% 0.96/0.38 % (649977)------------------------------
% 0.96/0.38 % (649977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.96/0.38 % (649977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.96/0.38 % (649977)CaDiCaL version: 2.1.3
% 0.96/0.38 % (649977)Termination reason: Instruction limit
% 0.96/0.38 % (649977)Termination phase: Saturation
% 0.96/0.38 % (649977)Time elapsed: 0.085 s
% 0.96/0.38 % (649977)Peak memory usage: 15 MB
% 0.96/0.38 % (649977)Instructions burned: 159 (million)
% 0.96/0.38 % TRYING [7]
% 0.96/0.38 % TRYING [7]
% 0.96/0.38 % (649973) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-649966-649973"...
% 0.96/0.38 % (649991)ott-21_1_sil=16000:fs=off:random_seed=2635203543:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.96/0.38 % TRYING [8]
% 0.96/0.38 % (649973)...printing done.
% 0.96/0.38 % (649973)Refutation found. Thanks to Tanya!
% 0.96/0.38 % SZS status Theorem for theBenchmark
% 0.96/0.38 % SZS output start Proof for theBenchmark
% See solution above
% 0.96/0.38 % (649973)------------------------------
% 0.96/0.38 % (649973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.96/0.38 % (649973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.96/0.38 % (649973)CaDiCaL version: 2.1.3
% 0.96/0.38 % (649973)Termination reason: Refutation
% 0.96/0.38 % (649973)Time elapsed: 0.116 s
% 0.96/0.38 % (649973)Peak memory usage: 15 MB
% 0.96/0.38 % (649973)Instructions burned: 227 (million)
% 0.96/0.38 % (649966)Success in time 0.157 s
% 0.96/0.38 % Vampire exiting
%------------------------------------------------------------------------------