%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG090+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.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:09:33 AM UTC 2026
% Result : Theorem 1.19s 0.71s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 190
% Syntax : Number of formulae : 890 ( 200 unt; 187 def)
% Number of atoms : 4103 (2268 equ)
% Maximal formula atoms : 415 ( 4 avg)
% Number of connectives : 5490 (2277 ~;1934 |;1172 &)
% ( 107 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 96 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 189 ( 187 usr; 187 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 3 ( 0 sgn 3 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
( op(e0,e0) = e0
& op(e0,e1) = e1
& op(e0,e2) = e2
& op(e0,e3) = e3
& op(e0,e4) = e4
& op(e1,e0) = e1
& op(e1,e1) = e4
& op(e1,e2) = e0
& op(e1,e3) = e2
& op(e1,e4) = e3
& op(e2,e0) = e2
& op(e2,e1) = e0
& op(e2,e2) = e3
& op(e2,e3) = e4
& op(e2,e4) = e1
& op(e3,e0) = e3
& op(e3,e1) = e2
& op(e3,e2) = e4
& op(e3,e3) = e1
& op(e3,e4) = e0
& op(e4,e0) = e4
& op(e4,e1) = e3
& op(e4,e2) = e1
& op(e4,e3) = e0
& op(e4,e4) = e2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
unit = e0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f4,conjecture,
( ( op(e0,e0) = e0
| op(e1,e1) = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e0) = e1
| op(e1,e1) = e1
| op(e2,e2) = e1
| op(e3,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e0) = e2
| op(e1,e1) = e2
| op(e2,e2) = e2
| op(e3,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e0) = e3
| op(e1,e1) = e3
| op(e2,e2) = e3
| op(e3,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e0) = e4
| op(e1,e1) = e4
| op(e2,e2) = e4
| op(e3,e3) = e4
| op(e4,e4) = e4 )
& ( 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 )
& 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 )
& ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0
| op(e0,e4) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0
| op(e4,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1
| op(e0,e4) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1
| op(e4,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2
| op(e0,e4) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2
| op(e4,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3
| op(e0,e4) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3
| op(e4,e0) = e3 )
& ( op(e0,e0) = e4
| op(e0,e1) = e4
| op(e0,e2) = e4
| op(e0,e3) = e4
| op(e0,e4) = e4 )
& ( op(e0,e0) = e4
| op(e1,e0) = e4
| op(e2,e0) = e4
| op(e3,e0) = e4
| op(e4,e0) = e4 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0
| op(e1,e4) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0
| op(e4,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1
| op(e1,e4) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1
| op(e4,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2
| op(e1,e4) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2
| op(e4,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3
| op(e1,e4) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3
| op(e4,e1) = e3 )
& ( op(e1,e0) = e4
| op(e1,e1) = e4
| op(e1,e2) = e4
| op(e1,e3) = e4
| op(e1,e4) = e4 )
& ( op(e0,e1) = e4
| op(e1,e1) = e4
| op(e2,e1) = e4
| op(e3,e1) = e4
| op(e4,e1) = e4 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0
| op(e2,e4) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0
| op(e4,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1
| op(e2,e4) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1
| op(e4,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2
| op(e2,e4) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2
| op(e4,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3
| op(e2,e4) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3
| op(e4,e2) = e3 )
& ( op(e2,e0) = e4
| op(e2,e1) = e4
| op(e2,e2) = e4
| op(e2,e3) = e4
| op(e2,e4) = e4 )
& ( op(e0,e2) = e4
| op(e1,e2) = e4
| op(e2,e2) = e4
| op(e3,e2) = e4
| op(e4,e2) = e4 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0
| op(e3,e4) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0
| op(e4,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1
| op(e3,e4) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1
| op(e4,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2
| op(e3,e4) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2
| op(e4,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3
| op(e3,e4) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3
| op(e4,e3) = e3 )
& ( op(e3,e0) = e4
| op(e3,e1) = e4
| op(e3,e2) = e4
| op(e3,e3) = e4
| op(e3,e4) = e4 )
& ( op(e0,e3) = e4
| op(e1,e3) = e4
| op(e2,e3) = e4
| op(e3,e3) = e4
| op(e4,e3) = e4 )
& ( op(e4,e0) = e0
| op(e4,e1) = e0
| op(e4,e2) = e0
| op(e4,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e4) = e0
| op(e1,e4) = e0
| op(e2,e4) = e0
| op(e3,e4) = e0
| op(e4,e4) = e0 )
& ( op(e4,e0) = e1
| op(e4,e1) = e1
| op(e4,e2) = e1
| op(e4,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e4) = e1
| op(e1,e4) = e1
| op(e2,e4) = e1
| op(e3,e4) = e1
| op(e4,e4) = e1 )
& ( op(e4,e0) = e2
| op(e4,e1) = e2
| op(e4,e2) = e2
| op(e4,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e4) = e2
| op(e1,e4) = e2
| op(e2,e4) = e2
| op(e3,e4) = e2
| op(e4,e4) = e2 )
& ( op(e4,e0) = e3
| op(e4,e1) = e3
| op(e4,e2) = e3
| op(e4,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e4) = e3
| op(e1,e4) = e3
| op(e2,e4) = e3
| op(e3,e4) = e3
| op(e4,e4) = e3 )
& ( op(e4,e0) = e4
| op(e4,e1) = e4
| op(e4,e2) = e4
| op(e4,e3) = e4
| op(e4,e4) = e4 )
& ( op(e0,e4) = e4
| op(e1,e4) = e4
| op(e2,e4) = e4
| op(e3,e4) = e4
| op(e4,e4) = e4 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f5,negated_conjecture,
~ ( ( op(e0,e0) = e0
| op(e1,e1) = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e0) = e1
| op(e1,e1) = e1
| op(e2,e2) = e1
| op(e3,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e0) = e2
| op(e1,e1) = e2
| op(e2,e2) = e2
| op(e3,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e0) = e3
| op(e1,e1) = e3
| op(e2,e2) = e3
| op(e3,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e0) = e4
| op(e1,e1) = e4
| op(e2,e2) = e4
| op(e3,e3) = e4
| op(e4,e4) = e4 )
& ( 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 )
& 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 )
& ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0
| op(e0,e4) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0
| op(e4,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1
| op(e0,e4) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1
| op(e4,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2
| op(e0,e4) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2
| op(e4,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3
| op(e0,e4) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3
| op(e4,e0) = e3 )
& ( op(e0,e0) = e4
| op(e0,e1) = e4
| op(e0,e2) = e4
| op(e0,e3) = e4
| op(e0,e4) = e4 )
& ( op(e0,e0) = e4
| op(e1,e0) = e4
| op(e2,e0) = e4
| op(e3,e0) = e4
| op(e4,e0) = e4 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0
| op(e1,e4) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0
| op(e4,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1
| op(e1,e4) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1
| op(e4,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2
| op(e1,e4) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2
| op(e4,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3
| op(e1,e4) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3
| op(e4,e1) = e3 )
& ( op(e1,e0) = e4
| op(e1,e1) = e4
| op(e1,e2) = e4
| op(e1,e3) = e4
| op(e1,e4) = e4 )
& ( op(e0,e1) = e4
| op(e1,e1) = e4
| op(e2,e1) = e4
| op(e3,e1) = e4
| op(e4,e1) = e4 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0
| op(e2,e4) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0
| op(e4,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1
| op(e2,e4) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1
| op(e4,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2
| op(e2,e4) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2
| op(e4,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3
| op(e2,e4) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3
| op(e4,e2) = e3 )
& ( op(e2,e0) = e4
| op(e2,e1) = e4
| op(e2,e2) = e4
| op(e2,e3) = e4
| op(e2,e4) = e4 )
& ( op(e0,e2) = e4
| op(e1,e2) = e4
| op(e2,e2) = e4
| op(e3,e2) = e4
| op(e4,e2) = e4 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0
| op(e3,e4) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0
| op(e4,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1
| op(e3,e4) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1
| op(e4,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2
| op(e3,e4) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2
| op(e4,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3
| op(e3,e4) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3
| op(e4,e3) = e3 )
& ( op(e3,e0) = e4
| op(e3,e1) = e4
| op(e3,e2) = e4
| op(e3,e3) = e4
| op(e3,e4) = e4 )
& ( op(e0,e3) = e4
| op(e1,e3) = e4
| op(e2,e3) = e4
| op(e3,e3) = e4
| op(e4,e3) = e4 )
& ( op(e4,e0) = e0
| op(e4,e1) = e0
| op(e4,e2) = e0
| op(e4,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e4) = e0
| op(e1,e4) = e0
| op(e2,e4) = e0
| op(e3,e4) = e0
| op(e4,e4) = e0 )
& ( op(e4,e0) = e1
| op(e4,e1) = e1
| op(e4,e2) = e1
| op(e4,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e4) = e1
| op(e1,e4) = e1
| op(e2,e4) = e1
| op(e3,e4) = e1
| op(e4,e4) = e1 )
& ( op(e4,e0) = e2
| op(e4,e1) = e2
| op(e4,e2) = e2
| op(e4,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e4) = e2
| op(e1,e4) = e2
| op(e2,e4) = e2
| op(e3,e4) = e2
| op(e4,e4) = e2 )
& ( op(e4,e0) = e3
| op(e4,e1) = e3
| op(e4,e2) = e3
| op(e4,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e4) = e3
| op(e1,e4) = e3
| op(e2,e4) = e3
| op(e3,e4) = e3
| op(e4,e4) = e3 )
& ( op(e4,e0) = e4
| op(e4,e1) = e4
| op(e4,e2) = e4
| op(e4,e3) = e4
| op(e4,e4) = e4 )
& ( op(e0,e4) = e4
| op(e1,e4) = e4
| op(e2,e4) = e4
| op(e3,e4) = e4
| op(e4,e4) = e4 ) ),
inference(negated_conjecture,[status(cth)],[f4]) ).
fof(f6,plain,
( ( e0 != op(e0,e0)
& e0 != op(e1,e1)
& e0 != op(e2,e2)
& e0 != op(e3,e3)
& e0 != op(e4,e4) )
| ( e1 != op(e0,e0)
& e1 != op(e1,e1)
& e1 != op(e2,e2)
& e1 != op(e3,e3)
& e1 != op(e4,e4) )
| ( e2 != op(e0,e0)
& e2 != op(e1,e1)
& e2 != op(e2,e2)
& e2 != op(e3,e3)
& e2 != op(e4,e4) )
| ( e3 != op(e0,e0)
& e3 != op(e1,e1)
& e3 != op(e2,e2)
& e3 != op(e3,e3)
& e3 != op(e4,e4) )
| ( e4 != op(e0,e0)
& e4 != op(e1,e1)
& e4 != op(e2,e2)
& e4 != op(e3,e3)
& e4 != op(e4,e4) )
| ( e0 != op(e0,e0)
& e1 != op(e0,e0)
& e2 != op(e0,e0)
& e3 != op(e0,e0)
& e4 != op(e0,e0) )
| ( e0 != op(e0,e1)
& e1 != op(e0,e1)
& e2 != op(e0,e1)
& e3 != op(e0,e1)
& e4 != op(e0,e1) )
| ( e0 != op(e0,e2)
& e1 != op(e0,e2)
& e2 != op(e0,e2)
& e3 != op(e0,e2)
& e4 != op(e0,e2) )
| ( e0 != op(e0,e3)
& e1 != op(e0,e3)
& e2 != op(e0,e3)
& e3 != op(e0,e3)
& e4 != op(e0,e3) )
| ( e0 != op(e0,e4)
& e1 != op(e0,e4)
& e2 != op(e0,e4)
& e3 != op(e0,e4)
& e4 != op(e0,e4) )
| ( e0 != op(e1,e0)
& e1 != op(e1,e0)
& e2 != op(e1,e0)
& e3 != op(e1,e0)
& e4 != op(e1,e0) )
| ( e0 != op(e1,e1)
& e1 != op(e1,e1)
& e2 != op(e1,e1)
& e3 != op(e1,e1)
& e4 != op(e1,e1) )
| ( e0 != op(e1,e2)
& e1 != op(e1,e2)
& e2 != op(e1,e2)
& e3 != op(e1,e2)
& e4 != op(e1,e2) )
| ( e0 != op(e1,e3)
& e1 != op(e1,e3)
& e2 != op(e1,e3)
& e3 != op(e1,e3)
& e4 != op(e1,e3) )
| ( e0 != op(e1,e4)
& e1 != op(e1,e4)
& e2 != op(e1,e4)
& e3 != op(e1,e4)
& e4 != op(e1,e4) )
| ( e0 != op(e2,e0)
& e1 != op(e2,e0)
& e2 != op(e2,e0)
& e3 != op(e2,e0)
& e4 != op(e2,e0) )
| ( e0 != op(e2,e1)
& e1 != op(e2,e1)
& e2 != op(e2,e1)
& e3 != op(e2,e1)
& e4 != op(e2,e1) )
| ( e0 != op(e2,e2)
& e1 != op(e2,e2)
& e2 != op(e2,e2)
& e3 != op(e2,e2)
& e4 != op(e2,e2) )
| ( e0 != op(e2,e3)
& e1 != op(e2,e3)
& e2 != op(e2,e3)
& e3 != op(e2,e3)
& e4 != op(e2,e3) )
| ( e0 != op(e2,e4)
& e1 != op(e2,e4)
& e2 != op(e2,e4)
& e3 != op(e2,e4)
& e4 != op(e2,e4) )
| ( e0 != op(e3,e0)
& e1 != op(e3,e0)
& e2 != op(e3,e0)
& e3 != op(e3,e0)
& e4 != op(e3,e0) )
| ( e0 != op(e3,e1)
& e1 != op(e3,e1)
& e2 != op(e3,e1)
& e3 != op(e3,e1)
& e4 != op(e3,e1) )
| ( e0 != op(e3,e2)
& e1 != op(e3,e2)
& e2 != op(e3,e2)
& e3 != op(e3,e2)
& e4 != op(e3,e2) )
| ( e0 != op(e3,e3)
& e1 != op(e3,e3)
& e2 != op(e3,e3)
& e3 != op(e3,e3)
& e4 != op(e3,e3) )
| ( e0 != op(e3,e4)
& e1 != op(e3,e4)
& e2 != op(e3,e4)
& e3 != op(e3,e4)
& e4 != op(e3,e4) )
| ( e0 != op(e4,e0)
& e1 != op(e4,e0)
& e2 != op(e4,e0)
& e3 != op(e4,e0)
& e4 != op(e4,e0) )
| ( e0 != op(e4,e1)
& e1 != op(e4,e1)
& e2 != op(e4,e1)
& e3 != op(e4,e1)
& e4 != op(e4,e1) )
| ( e0 != op(e4,e2)
& e1 != op(e4,e2)
& e2 != op(e4,e2)
& e3 != op(e4,e2)
& e4 != op(e4,e2) )
| ( e0 != op(e4,e3)
& e1 != op(e4,e3)
& e2 != op(e4,e3)
& e3 != op(e4,e3)
& e4 != op(e4,e3) )
| ( e0 != op(e4,e4)
& e1 != op(e4,e4)
& e2 != op(e4,e4)
& e3 != op(e4,e4)
& e4 != op(e4,e4) )
| e0 != op(unit,e0)
| e0 != op(e0,unit)
| e1 != op(unit,e1)
| e1 != op(e1,unit)
| e2 != op(unit,e2)
| e2 != op(e2,unit)
| e3 != op(unit,e3)
| e3 != op(e3,unit)
| e4 != op(unit,e4)
| e4 != op(e4,unit)
| ( e0 != unit
& e1 != unit
& e2 != unit
& e3 != unit
& e4 != unit )
| ( e0 != op(e0,e0)
& e0 != op(e0,e1)
& e0 != op(e0,e2)
& e0 != op(e0,e3)
& e0 != op(e0,e4) )
| ( e0 != op(e0,e0)
& e0 != op(e1,e0)
& e0 != op(e2,e0)
& e0 != op(e3,e0)
& e0 != op(e4,e0) )
| ( e1 != op(e0,e0)
& e1 != op(e0,e1)
& e1 != op(e0,e2)
& e1 != op(e0,e3)
& e1 != op(e0,e4) )
| ( e1 != op(e0,e0)
& e1 != op(e1,e0)
& e1 != op(e2,e0)
& e1 != op(e3,e0)
& e1 != op(e4,e0) )
| ( e2 != op(e0,e0)
& e2 != op(e0,e1)
& e2 != op(e0,e2)
& e2 != op(e0,e3)
& e2 != op(e0,e4) )
| ( e2 != op(e0,e0)
& e2 != op(e1,e0)
& e2 != op(e2,e0)
& e2 != op(e3,e0)
& e2 != op(e4,e0) )
| ( e3 != op(e0,e0)
& e3 != op(e0,e1)
& e3 != op(e0,e2)
& e3 != op(e0,e3)
& e3 != op(e0,e4) )
| ( e3 != op(e0,e0)
& e3 != op(e1,e0)
& e3 != op(e2,e0)
& e3 != op(e3,e0)
& e3 != op(e4,e0) )
| ( e4 != op(e0,e0)
& e4 != op(e0,e1)
& e4 != op(e0,e2)
& e4 != op(e0,e3)
& e4 != op(e0,e4) )
| ( e4 != op(e0,e0)
& e4 != op(e1,e0)
& e4 != op(e2,e0)
& e4 != op(e3,e0)
& e4 != op(e4,e0) )
| ( e0 != op(e1,e0)
& e0 != op(e1,e1)
& e0 != op(e1,e2)
& e0 != op(e1,e3)
& e0 != op(e1,e4) )
| ( e0 != op(e0,e1)
& e0 != op(e1,e1)
& e0 != op(e2,e1)
& e0 != op(e3,e1)
& e0 != op(e4,e1) )
| ( e1 != op(e1,e0)
& e1 != op(e1,e1)
& e1 != op(e1,e2)
& e1 != op(e1,e3)
& e1 != op(e1,e4) )
| ( e1 != op(e0,e1)
& e1 != op(e1,e1)
& e1 != op(e2,e1)
& e1 != op(e3,e1)
& e1 != op(e4,e1) )
| ( e2 != op(e1,e0)
& e2 != op(e1,e1)
& e2 != op(e1,e2)
& e2 != op(e1,e3)
& e2 != op(e1,e4) )
| ( e2 != op(e0,e1)
& e2 != op(e1,e1)
& e2 != op(e2,e1)
& e2 != op(e3,e1)
& e2 != op(e4,e1) )
| ( e3 != op(e1,e0)
& e3 != op(e1,e1)
& e3 != op(e1,e2)
& e3 != op(e1,e3)
& e3 != op(e1,e4) )
| ( e3 != op(e0,e1)
& e3 != op(e1,e1)
& e3 != op(e2,e1)
& e3 != op(e3,e1)
& e3 != op(e4,e1) )
| ( e4 != op(e1,e0)
& e4 != op(e1,e1)
& e4 != op(e1,e2)
& e4 != op(e1,e3)
& e4 != op(e1,e4) )
| ( e4 != op(e0,e1)
& e4 != op(e1,e1)
& e4 != op(e2,e1)
& e4 != op(e3,e1)
& e4 != op(e4,e1) )
| ( e0 != op(e2,e0)
& e0 != op(e2,e1)
& e0 != op(e2,e2)
& e0 != op(e2,e3)
& e0 != op(e2,e4) )
| ( e0 != op(e0,e2)
& e0 != op(e1,e2)
& e0 != op(e2,e2)
& e0 != op(e3,e2)
& e0 != op(e4,e2) )
| ( e1 != op(e2,e0)
& e1 != op(e2,e1)
& e1 != op(e2,e2)
& e1 != op(e2,e3)
& e1 != op(e2,e4) )
| ( e1 != op(e0,e2)
& e1 != op(e1,e2)
& e1 != op(e2,e2)
& e1 != op(e3,e2)
& e1 != op(e4,e2) )
| ( e2 != op(e2,e0)
& e2 != op(e2,e1)
& e2 != op(e2,e2)
& e2 != op(e2,e3)
& e2 != op(e2,e4) )
| ( e2 != op(e0,e2)
& e2 != op(e1,e2)
& e2 != op(e2,e2)
& e2 != op(e3,e2)
& e2 != op(e4,e2) )
| ( e3 != op(e2,e0)
& e3 != op(e2,e1)
& e3 != op(e2,e2)
& e3 != op(e2,e3)
& e3 != op(e2,e4) )
| ( e3 != op(e0,e2)
& e3 != op(e1,e2)
& e3 != op(e2,e2)
& e3 != op(e3,e2)
& e3 != op(e4,e2) )
| ( e4 != op(e2,e0)
& e4 != op(e2,e1)
& e4 != op(e2,e2)
& e4 != op(e2,e3)
& e4 != op(e2,e4) )
| ( e4 != op(e0,e2)
& e4 != op(e1,e2)
& e4 != op(e2,e2)
& e4 != op(e3,e2)
& e4 != op(e4,e2) )
| ( e0 != op(e3,e0)
& e0 != op(e3,e1)
& e0 != op(e3,e2)
& e0 != op(e3,e3)
& e0 != op(e3,e4) )
| ( e0 != op(e0,e3)
& e0 != op(e1,e3)
& e0 != op(e2,e3)
& e0 != op(e3,e3)
& e0 != op(e4,e3) )
| ( e1 != op(e3,e0)
& e1 != op(e3,e1)
& e1 != op(e3,e2)
& e1 != op(e3,e3)
& e1 != op(e3,e4) )
| ( e1 != op(e0,e3)
& e1 != op(e1,e3)
& e1 != op(e2,e3)
& e1 != op(e3,e3)
& e1 != op(e4,e3) )
| ( e2 != op(e3,e0)
& e2 != op(e3,e1)
& e2 != op(e3,e2)
& e2 != op(e3,e3)
& e2 != op(e3,e4) )
| ( e2 != op(e0,e3)
& e2 != op(e1,e3)
& e2 != op(e2,e3)
& e2 != op(e3,e3)
& e2 != op(e4,e3) )
| ( e3 != op(e3,e0)
& e3 != op(e3,e1)
& e3 != op(e3,e2)
& e3 != op(e3,e3)
& e3 != op(e3,e4) )
| ( e3 != op(e0,e3)
& e3 != op(e1,e3)
& e3 != op(e2,e3)
& e3 != op(e3,e3)
& e3 != op(e4,e3) )
| ( e4 != op(e3,e0)
& e4 != op(e3,e1)
& e4 != op(e3,e2)
& e4 != op(e3,e3)
& e4 != op(e3,e4) )
| ( e4 != op(e0,e3)
& e4 != op(e1,e3)
& e4 != op(e2,e3)
& e4 != op(e3,e3)
& e4 != op(e4,e3) )
| ( e0 != op(e4,e0)
& e0 != op(e4,e1)
& e0 != op(e4,e2)
& e0 != op(e4,e3)
& e0 != op(e4,e4) )
| ( e0 != op(e0,e4)
& e0 != op(e1,e4)
& e0 != op(e2,e4)
& e0 != op(e3,e4)
& e0 != op(e4,e4) )
| ( e1 != op(e4,e0)
& e1 != op(e4,e1)
& e1 != op(e4,e2)
& e1 != op(e4,e3)
& e1 != op(e4,e4) )
| ( e1 != op(e0,e4)
& e1 != op(e1,e4)
& e1 != op(e2,e4)
& e1 != op(e3,e4)
& e1 != op(e4,e4) )
| ( e2 != op(e4,e0)
& e2 != op(e4,e1)
& e2 != op(e4,e2)
& e2 != op(e4,e3)
& e2 != op(e4,e4) )
| ( e2 != op(e0,e4)
& e2 != op(e1,e4)
& e2 != op(e2,e4)
& e2 != op(e3,e4)
& e2 != op(e4,e4) )
| ( e3 != op(e4,e0)
& e3 != op(e4,e1)
& e3 != op(e4,e2)
& e3 != op(e4,e3)
& e3 != op(e4,e4) )
| ( e3 != op(e0,e4)
& e3 != op(e1,e4)
& e3 != op(e2,e4)
& e3 != op(e3,e4)
& e3 != op(e4,e4) )
| ( e4 != op(e4,e0)
& e4 != op(e4,e1)
& e4 != op(e4,e2)
& e4 != op(e4,e3)
& e4 != op(e4,e4) )
| ( e4 != op(e0,e4)
& e4 != op(e1,e4)
& e4 != op(e2,e4)
& e4 != op(e3,e4)
& e4 != op(e4,e4) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f7,definition,
( ( e4 != op(e0,e4)
& e4 != op(e1,e4)
& e4 != op(e2,e4)
& e4 != op(e3,e4)
& e4 != op(e4,e4) )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f8,definition,
( ( e4 != op(e4,e0)
& e4 != op(e4,e1)
& e4 != op(e4,e2)
& e4 != op(e4,e3)
& e4 != op(e4,e4) )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f9,definition,
( ( e3 != op(e0,e4)
& e3 != op(e1,e4)
& e3 != op(e2,e4)
& e3 != op(e3,e4)
& e3 != op(e4,e4) )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f10,definition,
( ( e3 != op(e4,e0)
& e3 != op(e4,e1)
& e3 != op(e4,e2)
& e3 != op(e4,e3)
& e3 != op(e4,e4) )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f11,definition,
( ( e2 != op(e0,e4)
& e2 != op(e1,e4)
& e2 != op(e2,e4)
& e2 != op(e3,e4)
& e2 != op(e4,e4) )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f12,definition,
( ( e2 != op(e4,e0)
& e2 != op(e4,e1)
& e2 != op(e4,e2)
& e2 != op(e4,e3)
& e2 != op(e4,e4) )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f13,definition,
( ( e1 != op(e0,e4)
& e1 != op(e1,e4)
& e1 != op(e2,e4)
& e1 != op(e3,e4)
& e1 != op(e4,e4) )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f14,definition,
( ( e1 != op(e4,e0)
& e1 != op(e4,e1)
& e1 != op(e4,e2)
& e1 != op(e4,e3)
& e1 != op(e4,e4) )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f15,definition,
( ( e0 != op(e0,e4)
& e0 != op(e1,e4)
& e0 != op(e2,e4)
& e0 != op(e3,e4)
& e0 != op(e4,e4) )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f16,definition,
( ( e0 != op(e4,e0)
& e0 != op(e4,e1)
& e0 != op(e4,e2)
& e0 != op(e4,e3)
& e0 != op(e4,e4) )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f17,definition,
( ( e4 != op(e0,e3)
& e4 != op(e1,e3)
& e4 != op(e2,e3)
& e4 != op(e3,e3)
& e4 != op(e4,e3) )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f18,definition,
( ( e4 != op(e3,e0)
& e4 != op(e3,e1)
& e4 != op(e3,e2)
& e4 != op(e3,e3)
& e4 != op(e3,e4) )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f19,definition,
( ( e3 != op(e0,e3)
& e3 != op(e1,e3)
& e3 != op(e2,e3)
& e3 != op(e3,e3)
& e3 != op(e4,e3) )
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f20,definition,
( ( e3 != op(e3,e0)
& e3 != op(e3,e1)
& e3 != op(e3,e2)
& e3 != op(e3,e3)
& e3 != op(e3,e4) )
| ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f21,definition,
( ( e2 != op(e0,e3)
& e2 != op(e1,e3)
& e2 != op(e2,e3)
& e2 != op(e3,e3)
& e2 != op(e4,e3) )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f22,definition,
( ( e2 != op(e3,e0)
& e2 != op(e3,e1)
& e2 != op(e3,e2)
& e2 != op(e3,e3)
& e2 != op(e3,e4) )
| ~ sP15 ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f23,definition,
( ( e1 != op(e0,e3)
& e1 != op(e1,e3)
& e1 != op(e2,e3)
& e1 != op(e3,e3)
& e1 != op(e4,e3) )
| ~ sP16 ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f24,definition,
( ( e1 != op(e3,e0)
& e1 != op(e3,e1)
& e1 != op(e3,e2)
& e1 != op(e3,e3)
& e1 != op(e3,e4) )
| ~ sP17 ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f25,definition,
( ( e0 != op(e0,e3)
& e0 != op(e1,e3)
& e0 != op(e2,e3)
& e0 != op(e3,e3)
& e0 != op(e4,e3) )
| ~ sP18 ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f26,definition,
( ( e0 != op(e3,e0)
& e0 != op(e3,e1)
& e0 != op(e3,e2)
& e0 != op(e3,e3)
& e0 != op(e3,e4) )
| ~ sP19 ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f27,definition,
( ( e4 != op(e0,e2)
& e4 != op(e1,e2)
& e4 != op(e2,e2)
& e4 != op(e3,e2)
& e4 != op(e4,e2) )
| ~ sP20 ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f28,definition,
( ( e4 != op(e2,e0)
& e4 != op(e2,e1)
& e4 != op(e2,e2)
& e4 != op(e2,e3)
& e4 != op(e2,e4) )
| ~ sP21 ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f29,definition,
( ( e3 != op(e0,e2)
& e3 != op(e1,e2)
& e3 != op(e2,e2)
& e3 != op(e3,e2)
& e3 != op(e4,e2) )
| ~ sP22 ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f30,definition,
( ( e3 != op(e2,e0)
& e3 != op(e2,e1)
& e3 != op(e2,e2)
& e3 != op(e2,e3)
& e3 != op(e2,e4) )
| ~ sP23 ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f31,definition,
( ( e2 != op(e0,e2)
& e2 != op(e1,e2)
& e2 != op(e2,e2)
& e2 != op(e3,e2)
& e2 != op(e4,e2) )
| ~ sP24 ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f32,definition,
( ( e2 != op(e2,e0)
& e2 != op(e2,e1)
& e2 != op(e2,e2)
& e2 != op(e2,e3)
& e2 != op(e2,e4) )
| ~ sP25 ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f33,definition,
( ( e1 != op(e0,e2)
& e1 != op(e1,e2)
& e1 != op(e2,e2)
& e1 != op(e3,e2)
& e1 != op(e4,e2) )
| ~ sP26 ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f34,definition,
( ( e1 != op(e2,e0)
& e1 != op(e2,e1)
& e1 != op(e2,e2)
& e1 != op(e2,e3)
& e1 != op(e2,e4) )
| ~ sP27 ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f35,definition,
( ( e0 != op(e0,e2)
& e0 != op(e1,e2)
& e0 != op(e2,e2)
& e0 != op(e3,e2)
& e0 != op(e4,e2) )
| ~ sP28 ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f36,definition,
( ( e0 != op(e2,e0)
& e0 != op(e2,e1)
& e0 != op(e2,e2)
& e0 != op(e2,e3)
& e0 != op(e2,e4) )
| ~ sP29 ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f37,definition,
( ( e4 != op(e0,e1)
& e4 != op(e1,e1)
& e4 != op(e2,e1)
& e4 != op(e3,e1)
& e4 != op(e4,e1) )
| ~ sP30 ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f38,definition,
( ( e4 != op(e1,e0)
& e4 != op(e1,e1)
& e4 != op(e1,e2)
& e4 != op(e1,e3)
& e4 != op(e1,e4) )
| ~ sP31 ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f39,definition,
( ( e3 != op(e0,e1)
& e3 != op(e1,e1)
& e3 != op(e2,e1)
& e3 != op(e3,e1)
& e3 != op(e4,e1) )
| ~ sP32 ),
introduced(definition,[new_symbols(definition,[sP32])],[predicate_definition_introduction]) ).
fof(f40,definition,
( ( e3 != op(e1,e0)
& e3 != op(e1,e1)
& e3 != op(e1,e2)
& e3 != op(e1,e3)
& e3 != op(e1,e4) )
| ~ sP33 ),
introduced(definition,[new_symbols(definition,[sP33])],[predicate_definition_introduction]) ).
fof(f41,definition,
( ( e2 != op(e0,e1)
& e2 != op(e1,e1)
& e2 != op(e2,e1)
& e2 != op(e3,e1)
& e2 != op(e4,e1) )
| ~ sP34 ),
introduced(definition,[new_symbols(definition,[sP34])],[predicate_definition_introduction]) ).
fof(f42,definition,
( ( e2 != op(e1,e0)
& e2 != op(e1,e1)
& e2 != op(e1,e2)
& e2 != op(e1,e3)
& e2 != op(e1,e4) )
| ~ sP35 ),
introduced(definition,[new_symbols(definition,[sP35])],[predicate_definition_introduction]) ).
fof(f43,definition,
( ( e1 != op(e0,e1)
& e1 != op(e1,e1)
& e1 != op(e2,e1)
& e1 != op(e3,e1)
& e1 != op(e4,e1) )
| ~ sP36 ),
introduced(definition,[new_symbols(definition,[sP36])],[predicate_definition_introduction]) ).
fof(f44,definition,
( ( e1 != op(e1,e0)
& e1 != op(e1,e1)
& e1 != op(e1,e2)
& e1 != op(e1,e3)
& e1 != op(e1,e4) )
| ~ sP37 ),
introduced(definition,[new_symbols(definition,[sP37])],[predicate_definition_introduction]) ).
fof(f45,definition,
( ( e0 != op(e0,e1)
& e0 != op(e1,e1)
& e0 != op(e2,e1)
& e0 != op(e3,e1)
& e0 != op(e4,e1) )
| ~ sP38 ),
introduced(definition,[new_symbols(definition,[sP38])],[predicate_definition_introduction]) ).
fof(f46,definition,
( ( e0 != op(e1,e0)
& e0 != op(e1,e1)
& e0 != op(e1,e2)
& e0 != op(e1,e3)
& e0 != op(e1,e4) )
| ~ sP39 ),
introduced(definition,[new_symbols(definition,[sP39])],[predicate_definition_introduction]) ).
fof(f47,definition,
( ( e4 != op(e0,e0)
& e4 != op(e1,e0)
& e4 != op(e2,e0)
& e4 != op(e3,e0)
& e4 != op(e4,e0) )
| ~ sP40 ),
introduced(definition,[new_symbols(definition,[sP40])],[predicate_definition_introduction]) ).
fof(f48,definition,
( ( e4 != op(e0,e0)
& e4 != op(e0,e1)
& e4 != op(e0,e2)
& e4 != op(e0,e3)
& e4 != op(e0,e4) )
| ~ sP41 ),
introduced(definition,[new_symbols(definition,[sP41])],[predicate_definition_introduction]) ).
fof(f49,definition,
( ( e3 != op(e0,e0)
& e3 != op(e1,e0)
& e3 != op(e2,e0)
& e3 != op(e3,e0)
& e3 != op(e4,e0) )
| ~ sP42 ),
introduced(definition,[new_symbols(definition,[sP42])],[predicate_definition_introduction]) ).
fof(f50,definition,
( ( e3 != op(e0,e0)
& e3 != op(e0,e1)
& e3 != op(e0,e2)
& e3 != op(e0,e3)
& e3 != op(e0,e4) )
| ~ sP43 ),
introduced(definition,[new_symbols(definition,[sP43])],[predicate_definition_introduction]) ).
fof(f51,definition,
( ( e2 != op(e0,e0)
& e2 != op(e1,e0)
& e2 != op(e2,e0)
& e2 != op(e3,e0)
& e2 != op(e4,e0) )
| ~ sP44 ),
introduced(definition,[new_symbols(definition,[sP44])],[predicate_definition_introduction]) ).
fof(f52,definition,
( ( e2 != op(e0,e0)
& e2 != op(e0,e1)
& e2 != op(e0,e2)
& e2 != op(e0,e3)
& e2 != op(e0,e4) )
| ~ sP45 ),
introduced(definition,[new_symbols(definition,[sP45])],[predicate_definition_introduction]) ).
fof(f53,definition,
( ( e1 != op(e0,e0)
& e1 != op(e1,e0)
& e1 != op(e2,e0)
& e1 != op(e3,e0)
& e1 != op(e4,e0) )
| ~ sP46 ),
introduced(definition,[new_symbols(definition,[sP46])],[predicate_definition_introduction]) ).
fof(f54,definition,
( ( e1 != op(e0,e0)
& e1 != op(e0,e1)
& e1 != op(e0,e2)
& e1 != op(e0,e3)
& e1 != op(e0,e4) )
| ~ sP47 ),
introduced(definition,[new_symbols(definition,[sP47])],[predicate_definition_introduction]) ).
fof(f55,definition,
( ( e0 != op(e0,e0)
& e0 != op(e1,e0)
& e0 != op(e2,e0)
& e0 != op(e3,e0)
& e0 != op(e4,e0) )
| ~ sP48 ),
introduced(definition,[new_symbols(definition,[sP48])],[predicate_definition_introduction]) ).
fof(f56,definition,
( ( e0 != op(e0,e0)
& e0 != op(e0,e1)
& e0 != op(e0,e2)
& e0 != op(e0,e3)
& e0 != op(e0,e4) )
| ~ sP49 ),
introduced(definition,[new_symbols(definition,[sP49])],[predicate_definition_introduction]) ).
fof(f57,definition,
( ( e0 != unit
& e1 != unit
& e2 != unit
& e3 != unit
& e4 != unit )
| ~ sP50 ),
introduced(definition,[new_symbols(definition,[sP50])],[predicate_definition_introduction]) ).
fof(f58,definition,
( ( e0 != op(e4,e4)
& e1 != op(e4,e4)
& e2 != op(e4,e4)
& e3 != op(e4,e4)
& e4 != op(e4,e4) )
| ~ sP51 ),
introduced(definition,[new_symbols(definition,[sP51])],[predicate_definition_introduction]) ).
fof(f59,definition,
( ( e0 != op(e4,e3)
& e1 != op(e4,e3)
& e2 != op(e4,e3)
& e3 != op(e4,e3)
& e4 != op(e4,e3) )
| ~ sP52 ),
introduced(definition,[new_symbols(definition,[sP52])],[predicate_definition_introduction]) ).
fof(f60,definition,
( ( e0 != op(e4,e2)
& e1 != op(e4,e2)
& e2 != op(e4,e2)
& e3 != op(e4,e2)
& e4 != op(e4,e2) )
| ~ sP53 ),
introduced(definition,[new_symbols(definition,[sP53])],[predicate_definition_introduction]) ).
fof(f61,definition,
( ( e0 != op(e4,e1)
& e1 != op(e4,e1)
& e2 != op(e4,e1)
& e3 != op(e4,e1)
& e4 != op(e4,e1) )
| ~ sP54 ),
introduced(definition,[new_symbols(definition,[sP54])],[predicate_definition_introduction]) ).
fof(f62,definition,
( ( e0 != op(e4,e0)
& e1 != op(e4,e0)
& e2 != op(e4,e0)
& e3 != op(e4,e0)
& e4 != op(e4,e0) )
| ~ sP55 ),
introduced(definition,[new_symbols(definition,[sP55])],[predicate_definition_introduction]) ).
fof(f63,definition,
( ( e0 != op(e3,e4)
& e1 != op(e3,e4)
& e2 != op(e3,e4)
& e3 != op(e3,e4)
& e4 != op(e3,e4) )
| ~ sP56 ),
introduced(definition,[new_symbols(definition,[sP56])],[predicate_definition_introduction]) ).
fof(f64,definition,
( ( e0 != op(e3,e3)
& e1 != op(e3,e3)
& e2 != op(e3,e3)
& e3 != op(e3,e3)
& e4 != op(e3,e3) )
| ~ sP57 ),
introduced(definition,[new_symbols(definition,[sP57])],[predicate_definition_introduction]) ).
fof(f65,definition,
( ( e0 != op(e3,e2)
& e1 != op(e3,e2)
& e2 != op(e3,e2)
& e3 != op(e3,e2)
& e4 != op(e3,e2) )
| ~ sP58 ),
introduced(definition,[new_symbols(definition,[sP58])],[predicate_definition_introduction]) ).
fof(f66,definition,
( ( e0 != op(e3,e1)
& e1 != op(e3,e1)
& e2 != op(e3,e1)
& e3 != op(e3,e1)
& e4 != op(e3,e1) )
| ~ sP59 ),
introduced(definition,[new_symbols(definition,[sP59])],[predicate_definition_introduction]) ).
fof(f67,definition,
( ( e0 != op(e3,e0)
& e1 != op(e3,e0)
& e2 != op(e3,e0)
& e3 != op(e3,e0)
& e4 != op(e3,e0) )
| ~ sP60 ),
introduced(definition,[new_symbols(definition,[sP60])],[predicate_definition_introduction]) ).
fof(f68,definition,
( ( e0 != op(e2,e4)
& e1 != op(e2,e4)
& e2 != op(e2,e4)
& e3 != op(e2,e4)
& e4 != op(e2,e4) )
| ~ sP61 ),
introduced(definition,[new_symbols(definition,[sP61])],[predicate_definition_introduction]) ).
fof(f69,definition,
( ( e0 != op(e2,e3)
& e1 != op(e2,e3)
& e2 != op(e2,e3)
& e3 != op(e2,e3)
& e4 != op(e2,e3) )
| ~ sP62 ),
introduced(definition,[new_symbols(definition,[sP62])],[predicate_definition_introduction]) ).
fof(f70,definition,
( ( e0 != op(e2,e2)
& e1 != op(e2,e2)
& e2 != op(e2,e2)
& e3 != op(e2,e2)
& e4 != op(e2,e2) )
| ~ sP63 ),
introduced(definition,[new_symbols(definition,[sP63])],[predicate_definition_introduction]) ).
fof(f71,definition,
( ( e0 != op(e2,e1)
& e1 != op(e2,e1)
& e2 != op(e2,e1)
& e3 != op(e2,e1)
& e4 != op(e2,e1) )
| ~ sP64 ),
introduced(definition,[new_symbols(definition,[sP64])],[predicate_definition_introduction]) ).
fof(f72,definition,
( ( e0 != op(e2,e0)
& e1 != op(e2,e0)
& e2 != op(e2,e0)
& e3 != op(e2,e0)
& e4 != op(e2,e0) )
| ~ sP65 ),
introduced(definition,[new_symbols(definition,[sP65])],[predicate_definition_introduction]) ).
fof(f73,definition,
( ( e0 != op(e1,e4)
& e1 != op(e1,e4)
& e2 != op(e1,e4)
& e3 != op(e1,e4)
& e4 != op(e1,e4) )
| ~ sP66 ),
introduced(definition,[new_symbols(definition,[sP66])],[predicate_definition_introduction]) ).
fof(f74,definition,
( ( e0 != op(e1,e3)
& e1 != op(e1,e3)
& e2 != op(e1,e3)
& e3 != op(e1,e3)
& e4 != op(e1,e3) )
| ~ sP67 ),
introduced(definition,[new_symbols(definition,[sP67])],[predicate_definition_introduction]) ).
fof(f75,definition,
( ( e0 != op(e1,e2)
& e1 != op(e1,e2)
& e2 != op(e1,e2)
& e3 != op(e1,e2)
& e4 != op(e1,e2) )
| ~ sP68 ),
introduced(definition,[new_symbols(definition,[sP68])],[predicate_definition_introduction]) ).
fof(f76,definition,
( ( e0 != op(e1,e1)
& e1 != op(e1,e1)
& e2 != op(e1,e1)
& e3 != op(e1,e1)
& e4 != op(e1,e1) )
| ~ sP69 ),
introduced(definition,[new_symbols(definition,[sP69])],[predicate_definition_introduction]) ).
fof(f77,definition,
( ( e0 != op(e1,e0)
& e1 != op(e1,e0)
& e2 != op(e1,e0)
& e3 != op(e1,e0)
& e4 != op(e1,e0) )
| ~ sP70 ),
introduced(definition,[new_symbols(definition,[sP70])],[predicate_definition_introduction]) ).
fof(f78,definition,
( ( e0 != op(e0,e4)
& e1 != op(e0,e4)
& e2 != op(e0,e4)
& e3 != op(e0,e4)
& e4 != op(e0,e4) )
| ~ sP71 ),
introduced(definition,[new_symbols(definition,[sP71])],[predicate_definition_introduction]) ).
fof(f79,definition,
( ( e0 != op(e0,e3)
& e1 != op(e0,e3)
& e2 != op(e0,e3)
& e3 != op(e0,e3)
& e4 != op(e0,e3) )
| ~ sP72 ),
introduced(definition,[new_symbols(definition,[sP72])],[predicate_definition_introduction]) ).
fof(f80,definition,
( ( e0 != op(e0,e2)
& e1 != op(e0,e2)
& e2 != op(e0,e2)
& e3 != op(e0,e2)
& e4 != op(e0,e2) )
| ~ sP73 ),
introduced(definition,[new_symbols(definition,[sP73])],[predicate_definition_introduction]) ).
fof(f81,definition,
( ( e0 != op(e0,e1)
& e1 != op(e0,e1)
& e2 != op(e0,e1)
& e3 != op(e0,e1)
& e4 != op(e0,e1) )
| ~ sP74 ),
introduced(definition,[new_symbols(definition,[sP74])],[predicate_definition_introduction]) ).
fof(f82,definition,
( ( e0 != op(e0,e0)
& e1 != op(e0,e0)
& e2 != op(e0,e0)
& e3 != op(e0,e0)
& e4 != op(e0,e0) )
| ~ sP75 ),
introduced(definition,[new_symbols(definition,[sP75])],[predicate_definition_introduction]) ).
fof(f83,definition,
( ( e4 != op(e0,e0)
& e4 != op(e1,e1)
& e4 != op(e2,e2)
& e4 != op(e3,e3)
& e4 != op(e4,e4) )
| ~ sP76 ),
introduced(definition,[new_symbols(definition,[sP76])],[predicate_definition_introduction]) ).
fof(f84,definition,
( ( e3 != op(e0,e0)
& e3 != op(e1,e1)
& e3 != op(e2,e2)
& e3 != op(e3,e3)
& e3 != op(e4,e4) )
| ~ sP77 ),
introduced(definition,[new_symbols(definition,[sP77])],[predicate_definition_introduction]) ).
fof(f85,definition,
( ( e2 != op(e0,e0)
& e2 != op(e1,e1)
& e2 != op(e2,e2)
& e2 != op(e3,e3)
& e2 != op(e4,e4) )
| ~ sP78 ),
introduced(definition,[new_symbols(definition,[sP78])],[predicate_definition_introduction]) ).
fof(f86,definition,
( ( e1 != op(e0,e0)
& e1 != op(e1,e1)
& e1 != op(e2,e2)
& e1 != op(e3,e3)
& e1 != op(e4,e4) )
| ~ sP79 ),
introduced(definition,[new_symbols(definition,[sP79])],[predicate_definition_introduction]) ).
fof(f87,plain,
( ( e0 != op(e0,e0)
& e0 != op(e1,e1)
& e0 != op(e2,e2)
& e0 != op(e3,e3)
& e0 != op(e4,e4) )
| sP79
| sP78
| sP77
| sP76
| sP75
| sP74
| sP73
| sP72
| sP71
| sP70
| sP69
| sP68
| sP67
| sP66
| sP65
| sP64
| sP63
| sP62
| sP61
| sP60
| sP59
| sP58
| sP57
| sP56
| sP55
| sP54
| sP53
| sP52
| sP51
| e0 != op(unit,e0)
| e0 != op(e0,unit)
| e1 != op(unit,e1)
| e1 != op(e1,unit)
| e2 != op(unit,e2)
| e2 != op(e2,unit)
| e3 != op(unit,e3)
| e3 != op(e3,unit)
| e4 != op(unit,e4)
| e4 != op(e4,unit)
| sP50
| sP49
| sP48
| sP47
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP39
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP29
| sP28
| sP27
| sP26
| sP25
| sP24
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(definition_folding,[],[f6,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,f9,f8,f7]) ).
fof(f88,plain,
( ( e1 != op(e0,e0)
& e1 != op(e1,e1)
& e1 != op(e2,e2)
& e1 != op(e3,e3)
& e1 != op(e4,e4) )
| ~ sP79 ),
inference(nnf_transformation,[],[f86]) ).
fof(f89,plain,
( ( e2 != op(e0,e0)
& e2 != op(e1,e1)
& e2 != op(e2,e2)
& e2 != op(e3,e3)
& e2 != op(e4,e4) )
| ~ sP78 ),
inference(nnf_transformation,[],[f85]) ).
fof(f90,plain,
( ( e3 != op(e0,e0)
& e3 != op(e1,e1)
& e3 != op(e2,e2)
& e3 != op(e3,e3)
& e3 != op(e4,e4) )
| ~ sP77 ),
inference(nnf_transformation,[],[f84]) ).
fof(f91,plain,
( ( e4 != op(e0,e0)
& e4 != op(e1,e1)
& e4 != op(e2,e2)
& e4 != op(e3,e3)
& e4 != op(e4,e4) )
| ~ sP76 ),
inference(nnf_transformation,[],[f83]) ).
fof(f92,plain,
( ( e0 != op(e0,e0)
& e1 != op(e0,e0)
& e2 != op(e0,e0)
& e3 != op(e0,e0)
& e4 != op(e0,e0) )
| ~ sP75 ),
inference(nnf_transformation,[],[f82]) ).
fof(f93,plain,
( ( e0 != op(e0,e1)
& e1 != op(e0,e1)
& e2 != op(e0,e1)
& e3 != op(e0,e1)
& e4 != op(e0,e1) )
| ~ sP74 ),
inference(nnf_transformation,[],[f81]) ).
fof(f94,plain,
( ( e0 != op(e0,e2)
& e1 != op(e0,e2)
& e2 != op(e0,e2)
& e3 != op(e0,e2)
& e4 != op(e0,e2) )
| ~ sP73 ),
inference(nnf_transformation,[],[f80]) ).
fof(f95,plain,
( ( e0 != op(e0,e3)
& e1 != op(e0,e3)
& e2 != op(e0,e3)
& e3 != op(e0,e3)
& e4 != op(e0,e3) )
| ~ sP72 ),
inference(nnf_transformation,[],[f79]) ).
fof(f96,plain,
( ( e0 != op(e0,e4)
& e1 != op(e0,e4)
& e2 != op(e0,e4)
& e3 != op(e0,e4)
& e4 != op(e0,e4) )
| ~ sP71 ),
inference(nnf_transformation,[],[f78]) ).
fof(f97,plain,
( ( e0 != op(e1,e0)
& e1 != op(e1,e0)
& e2 != op(e1,e0)
& e3 != op(e1,e0)
& e4 != op(e1,e0) )
| ~ sP70 ),
inference(nnf_transformation,[],[f77]) ).
fof(f98,plain,
( ( e0 != op(e1,e1)
& e1 != op(e1,e1)
& e2 != op(e1,e1)
& e3 != op(e1,e1)
& e4 != op(e1,e1) )
| ~ sP69 ),
inference(nnf_transformation,[],[f76]) ).
fof(f99,plain,
( ( e0 != op(e1,e2)
& e1 != op(e1,e2)
& e2 != op(e1,e2)
& e3 != op(e1,e2)
& e4 != op(e1,e2) )
| ~ sP68 ),
inference(nnf_transformation,[],[f75]) ).
fof(f100,plain,
( ( e0 != op(e1,e3)
& e1 != op(e1,e3)
& e2 != op(e1,e3)
& e3 != op(e1,e3)
& e4 != op(e1,e3) )
| ~ sP67 ),
inference(nnf_transformation,[],[f74]) ).
fof(f101,plain,
( ( e0 != op(e1,e4)
& e1 != op(e1,e4)
& e2 != op(e1,e4)
& e3 != op(e1,e4)
& e4 != op(e1,e4) )
| ~ sP66 ),
inference(nnf_transformation,[],[f73]) ).
fof(f102,plain,
( ( e0 != op(e2,e0)
& e1 != op(e2,e0)
& e2 != op(e2,e0)
& e3 != op(e2,e0)
& e4 != op(e2,e0) )
| ~ sP65 ),
inference(nnf_transformation,[],[f72]) ).
fof(f103,plain,
( ( e0 != op(e2,e1)
& e1 != op(e2,e1)
& e2 != op(e2,e1)
& e3 != op(e2,e1)
& e4 != op(e2,e1) )
| ~ sP64 ),
inference(nnf_transformation,[],[f71]) ).
fof(f104,plain,
( ( e0 != op(e2,e2)
& e1 != op(e2,e2)
& e2 != op(e2,e2)
& e3 != op(e2,e2)
& e4 != op(e2,e2) )
| ~ sP63 ),
inference(nnf_transformation,[],[f70]) ).
fof(f105,plain,
( ( e0 != op(e2,e3)
& e1 != op(e2,e3)
& e2 != op(e2,e3)
& e3 != op(e2,e3)
& e4 != op(e2,e3) )
| ~ sP62 ),
inference(nnf_transformation,[],[f69]) ).
fof(f106,plain,
( ( e0 != op(e2,e4)
& e1 != op(e2,e4)
& e2 != op(e2,e4)
& e3 != op(e2,e4)
& e4 != op(e2,e4) )
| ~ sP61 ),
inference(nnf_transformation,[],[f68]) ).
fof(f107,plain,
( ( e0 != op(e3,e0)
& e1 != op(e3,e0)
& e2 != op(e3,e0)
& e3 != op(e3,e0)
& e4 != op(e3,e0) )
| ~ sP60 ),
inference(nnf_transformation,[],[f67]) ).
fof(f108,plain,
( ( e0 != op(e3,e1)
& e1 != op(e3,e1)
& e2 != op(e3,e1)
& e3 != op(e3,e1)
& e4 != op(e3,e1) )
| ~ sP59 ),
inference(nnf_transformation,[],[f66]) ).
fof(f109,plain,
( ( e0 != op(e3,e2)
& e1 != op(e3,e2)
& e2 != op(e3,e2)
& e3 != op(e3,e2)
& e4 != op(e3,e2) )
| ~ sP58 ),
inference(nnf_transformation,[],[f65]) ).
fof(f110,plain,
( ( e0 != op(e3,e3)
& e1 != op(e3,e3)
& e2 != op(e3,e3)
& e3 != op(e3,e3)
& e4 != op(e3,e3) )
| ~ sP57 ),
inference(nnf_transformation,[],[f64]) ).
fof(f111,plain,
( ( e0 != op(e3,e4)
& e1 != op(e3,e4)
& e2 != op(e3,e4)
& e3 != op(e3,e4)
& e4 != op(e3,e4) )
| ~ sP56 ),
inference(nnf_transformation,[],[f63]) ).
fof(f112,plain,
( ( e0 != op(e4,e0)
& e1 != op(e4,e0)
& e2 != op(e4,e0)
& e3 != op(e4,e0)
& e4 != op(e4,e0) )
| ~ sP55 ),
inference(nnf_transformation,[],[f62]) ).
fof(f113,plain,
( ( e0 != op(e4,e1)
& e1 != op(e4,e1)
& e2 != op(e4,e1)
& e3 != op(e4,e1)
& e4 != op(e4,e1) )
| ~ sP54 ),
inference(nnf_transformation,[],[f61]) ).
fof(f114,plain,
( ( e0 != op(e4,e2)
& e1 != op(e4,e2)
& e2 != op(e4,e2)
& e3 != op(e4,e2)
& e4 != op(e4,e2) )
| ~ sP53 ),
inference(nnf_transformation,[],[f60]) ).
fof(f115,plain,
( ( e0 != op(e4,e3)
& e1 != op(e4,e3)
& e2 != op(e4,e3)
& e3 != op(e4,e3)
& e4 != op(e4,e3) )
| ~ sP52 ),
inference(nnf_transformation,[],[f59]) ).
fof(f116,plain,
( ( e0 != op(e4,e4)
& e1 != op(e4,e4)
& e2 != op(e4,e4)
& e3 != op(e4,e4)
& e4 != op(e4,e4) )
| ~ sP51 ),
inference(nnf_transformation,[],[f58]) ).
fof(f117,plain,
( ( e0 != unit
& e1 != unit
& e2 != unit
& e3 != unit
& e4 != unit )
| ~ sP50 ),
inference(nnf_transformation,[],[f57]) ).
fof(f118,plain,
( ( e0 != op(e0,e0)
& e0 != op(e0,e1)
& e0 != op(e0,e2)
& e0 != op(e0,e3)
& e0 != op(e0,e4) )
| ~ sP49 ),
inference(nnf_transformation,[],[f56]) ).
fof(f119,plain,
( ( e0 != op(e0,e0)
& e0 != op(e1,e0)
& e0 != op(e2,e0)
& e0 != op(e3,e0)
& e0 != op(e4,e0) )
| ~ sP48 ),
inference(nnf_transformation,[],[f55]) ).
fof(f120,plain,
( ( e1 != op(e0,e0)
& e1 != op(e0,e1)
& e1 != op(e0,e2)
& e1 != op(e0,e3)
& e1 != op(e0,e4) )
| ~ sP47 ),
inference(nnf_transformation,[],[f54]) ).
fof(f121,plain,
( ( e1 != op(e0,e0)
& e1 != op(e1,e0)
& e1 != op(e2,e0)
& e1 != op(e3,e0)
& e1 != op(e4,e0) )
| ~ sP46 ),
inference(nnf_transformation,[],[f53]) ).
fof(f122,plain,
( ( e2 != op(e0,e0)
& e2 != op(e0,e1)
& e2 != op(e0,e2)
& e2 != op(e0,e3)
& e2 != op(e0,e4) )
| ~ sP45 ),
inference(nnf_transformation,[],[f52]) ).
fof(f123,plain,
( ( e2 != op(e0,e0)
& e2 != op(e1,e0)
& e2 != op(e2,e0)
& e2 != op(e3,e0)
& e2 != op(e4,e0) )
| ~ sP44 ),
inference(nnf_transformation,[],[f51]) ).
fof(f124,plain,
( ( e3 != op(e0,e0)
& e3 != op(e0,e1)
& e3 != op(e0,e2)
& e3 != op(e0,e3)
& e3 != op(e0,e4) )
| ~ sP43 ),
inference(nnf_transformation,[],[f50]) ).
fof(f125,plain,
( ( e3 != op(e0,e0)
& e3 != op(e1,e0)
& e3 != op(e2,e0)
& e3 != op(e3,e0)
& e3 != op(e4,e0) )
| ~ sP42 ),
inference(nnf_transformation,[],[f49]) ).
fof(f126,plain,
( ( e4 != op(e0,e0)
& e4 != op(e0,e1)
& e4 != op(e0,e2)
& e4 != op(e0,e3)
& e4 != op(e0,e4) )
| ~ sP41 ),
inference(nnf_transformation,[],[f48]) ).
fof(f127,plain,
( ( e4 != op(e0,e0)
& e4 != op(e1,e0)
& e4 != op(e2,e0)
& e4 != op(e3,e0)
& e4 != op(e4,e0) )
| ~ sP40 ),
inference(nnf_transformation,[],[f47]) ).
fof(f128,plain,
( ( e0 != op(e1,e0)
& e0 != op(e1,e1)
& e0 != op(e1,e2)
& e0 != op(e1,e3)
& e0 != op(e1,e4) )
| ~ sP39 ),
inference(nnf_transformation,[],[f46]) ).
fof(f129,plain,
( ( e0 != op(e0,e1)
& e0 != op(e1,e1)
& e0 != op(e2,e1)
& e0 != op(e3,e1)
& e0 != op(e4,e1) )
| ~ sP38 ),
inference(nnf_transformation,[],[f45]) ).
fof(f130,plain,
( ( e1 != op(e1,e0)
& e1 != op(e1,e1)
& e1 != op(e1,e2)
& e1 != op(e1,e3)
& e1 != op(e1,e4) )
| ~ sP37 ),
inference(nnf_transformation,[],[f44]) ).
fof(f131,plain,
( ( e1 != op(e0,e1)
& e1 != op(e1,e1)
& e1 != op(e2,e1)
& e1 != op(e3,e1)
& e1 != op(e4,e1) )
| ~ sP36 ),
inference(nnf_transformation,[],[f43]) ).
fof(f132,plain,
( ( e2 != op(e1,e0)
& e2 != op(e1,e1)
& e2 != op(e1,e2)
& e2 != op(e1,e3)
& e2 != op(e1,e4) )
| ~ sP35 ),
inference(nnf_transformation,[],[f42]) ).
fof(f133,plain,
( ( e2 != op(e0,e1)
& e2 != op(e1,e1)
& e2 != op(e2,e1)
& e2 != op(e3,e1)
& e2 != op(e4,e1) )
| ~ sP34 ),
inference(nnf_transformation,[],[f41]) ).
fof(f134,plain,
( ( e3 != op(e1,e0)
& e3 != op(e1,e1)
& e3 != op(e1,e2)
& e3 != op(e1,e3)
& e3 != op(e1,e4) )
| ~ sP33 ),
inference(nnf_transformation,[],[f40]) ).
fof(f135,plain,
( ( e3 != op(e0,e1)
& e3 != op(e1,e1)
& e3 != op(e2,e1)
& e3 != op(e3,e1)
& e3 != op(e4,e1) )
| ~ sP32 ),
inference(nnf_transformation,[],[f39]) ).
fof(f136,plain,
( ( e4 != op(e1,e0)
& e4 != op(e1,e1)
& e4 != op(e1,e2)
& e4 != op(e1,e3)
& e4 != op(e1,e4) )
| ~ sP31 ),
inference(nnf_transformation,[],[f38]) ).
fof(f137,plain,
( ( e4 != op(e0,e1)
& e4 != op(e1,e1)
& e4 != op(e2,e1)
& e4 != op(e3,e1)
& e4 != op(e4,e1) )
| ~ sP30 ),
inference(nnf_transformation,[],[f37]) ).
fof(f138,plain,
( ( e0 != op(e2,e0)
& e0 != op(e2,e1)
& e0 != op(e2,e2)
& e0 != op(e2,e3)
& e0 != op(e2,e4) )
| ~ sP29 ),
inference(nnf_transformation,[],[f36]) ).
fof(f139,plain,
( ( e0 != op(e0,e2)
& e0 != op(e1,e2)
& e0 != op(e2,e2)
& e0 != op(e3,e2)
& e0 != op(e4,e2) )
| ~ sP28 ),
inference(nnf_transformation,[],[f35]) ).
fof(f140,plain,
( ( e1 != op(e2,e0)
& e1 != op(e2,e1)
& e1 != op(e2,e2)
& e1 != op(e2,e3)
& e1 != op(e2,e4) )
| ~ sP27 ),
inference(nnf_transformation,[],[f34]) ).
fof(f141,plain,
( ( e1 != op(e0,e2)
& e1 != op(e1,e2)
& e1 != op(e2,e2)
& e1 != op(e3,e2)
& e1 != op(e4,e2) )
| ~ sP26 ),
inference(nnf_transformation,[],[f33]) ).
fof(f142,plain,
( ( e2 != op(e2,e0)
& e2 != op(e2,e1)
& e2 != op(e2,e2)
& e2 != op(e2,e3)
& e2 != op(e2,e4) )
| ~ sP25 ),
inference(nnf_transformation,[],[f32]) ).
fof(f143,plain,
( ( e2 != op(e0,e2)
& e2 != op(e1,e2)
& e2 != op(e2,e2)
& e2 != op(e3,e2)
& e2 != op(e4,e2) )
| ~ sP24 ),
inference(nnf_transformation,[],[f31]) ).
fof(f144,plain,
( ( e3 != op(e2,e0)
& e3 != op(e2,e1)
& e3 != op(e2,e2)
& e3 != op(e2,e3)
& e3 != op(e2,e4) )
| ~ sP23 ),
inference(nnf_transformation,[],[f30]) ).
fof(f145,plain,
( ( e3 != op(e0,e2)
& e3 != op(e1,e2)
& e3 != op(e2,e2)
& e3 != op(e3,e2)
& e3 != op(e4,e2) )
| ~ sP22 ),
inference(nnf_transformation,[],[f29]) ).
fof(f146,plain,
( ( e4 != op(e2,e0)
& e4 != op(e2,e1)
& e4 != op(e2,e2)
& e4 != op(e2,e3)
& e4 != op(e2,e4) )
| ~ sP21 ),
inference(nnf_transformation,[],[f28]) ).
fof(f147,plain,
( ( e4 != op(e0,e2)
& e4 != op(e1,e2)
& e4 != op(e2,e2)
& e4 != op(e3,e2)
& e4 != op(e4,e2) )
| ~ sP20 ),
inference(nnf_transformation,[],[f27]) ).
fof(f148,plain,
( ( e0 != op(e3,e0)
& e0 != op(e3,e1)
& e0 != op(e3,e2)
& e0 != op(e3,e3)
& e0 != op(e3,e4) )
| ~ sP19 ),
inference(nnf_transformation,[],[f26]) ).
fof(f149,plain,
( ( e0 != op(e0,e3)
& e0 != op(e1,e3)
& e0 != op(e2,e3)
& e0 != op(e3,e3)
& e0 != op(e4,e3) )
| ~ sP18 ),
inference(nnf_transformation,[],[f25]) ).
fof(f150,plain,
( ( e1 != op(e3,e0)
& e1 != op(e3,e1)
& e1 != op(e3,e2)
& e1 != op(e3,e3)
& e1 != op(e3,e4) )
| ~ sP17 ),
inference(nnf_transformation,[],[f24]) ).
fof(f151,plain,
( ( e1 != op(e0,e3)
& e1 != op(e1,e3)
& e1 != op(e2,e3)
& e1 != op(e3,e3)
& e1 != op(e4,e3) )
| ~ sP16 ),
inference(nnf_transformation,[],[f23]) ).
fof(f152,plain,
( ( e2 != op(e3,e0)
& e2 != op(e3,e1)
& e2 != op(e3,e2)
& e2 != op(e3,e3)
& e2 != op(e3,e4) )
| ~ sP15 ),
inference(nnf_transformation,[],[f22]) ).
fof(f153,plain,
( ( e2 != op(e0,e3)
& e2 != op(e1,e3)
& e2 != op(e2,e3)
& e2 != op(e3,e3)
& e2 != op(e4,e3) )
| ~ sP14 ),
inference(nnf_transformation,[],[f21]) ).
fof(f154,plain,
( ( e3 != op(e3,e0)
& e3 != op(e3,e1)
& e3 != op(e3,e2)
& e3 != op(e3,e3)
& e3 != op(e3,e4) )
| ~ sP13 ),
inference(nnf_transformation,[],[f20]) ).
fof(f155,plain,
( ( e3 != op(e0,e3)
& e3 != op(e1,e3)
& e3 != op(e2,e3)
& e3 != op(e3,e3)
& e3 != op(e4,e3) )
| ~ sP12 ),
inference(nnf_transformation,[],[f19]) ).
fof(f156,plain,
( ( e4 != op(e3,e0)
& e4 != op(e3,e1)
& e4 != op(e3,e2)
& e4 != op(e3,e3)
& e4 != op(e3,e4) )
| ~ sP11 ),
inference(nnf_transformation,[],[f18]) ).
fof(f157,plain,
( ( e4 != op(e0,e3)
& e4 != op(e1,e3)
& e4 != op(e2,e3)
& e4 != op(e3,e3)
& e4 != op(e4,e3) )
| ~ sP10 ),
inference(nnf_transformation,[],[f17]) ).
fof(f158,plain,
( ( e0 != op(e4,e0)
& e0 != op(e4,e1)
& e0 != op(e4,e2)
& e0 != op(e4,e3)
& e0 != op(e4,e4) )
| ~ sP9 ),
inference(nnf_transformation,[],[f16]) ).
fof(f159,plain,
( ( e0 != op(e0,e4)
& e0 != op(e1,e4)
& e0 != op(e2,e4)
& e0 != op(e3,e4)
& e0 != op(e4,e4) )
| ~ sP8 ),
inference(nnf_transformation,[],[f15]) ).
fof(f160,plain,
( ( e1 != op(e4,e0)
& e1 != op(e4,e1)
& e1 != op(e4,e2)
& e1 != op(e4,e3)
& e1 != op(e4,e4) )
| ~ sP7 ),
inference(nnf_transformation,[],[f14]) ).
fof(f161,plain,
( ( e1 != op(e0,e4)
& e1 != op(e1,e4)
& e1 != op(e2,e4)
& e1 != op(e3,e4)
& e1 != op(e4,e4) )
| ~ sP6 ),
inference(nnf_transformation,[],[f13]) ).
fof(f162,plain,
( ( e2 != op(e4,e0)
& e2 != op(e4,e1)
& e2 != op(e4,e2)
& e2 != op(e4,e3)
& e2 != op(e4,e4) )
| ~ sP5 ),
inference(nnf_transformation,[],[f12]) ).
fof(f163,plain,
( ( e2 != op(e0,e4)
& e2 != op(e1,e4)
& e2 != op(e2,e4)
& e2 != op(e3,e4)
& e2 != op(e4,e4) )
| ~ sP4 ),
inference(nnf_transformation,[],[f11]) ).
fof(f164,plain,
( ( e3 != op(e4,e0)
& e3 != op(e4,e1)
& e3 != op(e4,e2)
& e3 != op(e4,e3)
& e3 != op(e4,e4) )
| ~ sP3 ),
inference(nnf_transformation,[],[f10]) ).
fof(f165,plain,
( ( e3 != op(e0,e4)
& e3 != op(e1,e4)
& e3 != op(e2,e4)
& e3 != op(e3,e4)
& e3 != op(e4,e4) )
| ~ sP2 ),
inference(nnf_transformation,[],[f9]) ).
fof(f166,plain,
( ( e4 != op(e4,e0)
& e4 != op(e4,e1)
& e4 != op(e4,e2)
& e4 != op(e4,e3)
& e4 != op(e4,e4) )
| ~ sP1 ),
inference(nnf_transformation,[],[f8]) ).
fof(f167,plain,
( ( e4 != op(e0,e4)
& e4 != op(e1,e4)
& e4 != op(e2,e4)
& e4 != op(e3,e4)
& e4 != op(e4,e4) )
| ~ sP0 ),
inference(nnf_transformation,[],[f7]) ).
fof(f178,plain,
e2 = op(e4,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f179,plain,
e0 = op(e4,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f180,plain,
e1 = op(e4,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f181,plain,
e3 = op(e4,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f182,plain,
e4 = op(e4,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f183,plain,
e0 = op(e3,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f184,plain,
e1 = op(e3,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f185,plain,
e4 = op(e3,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f186,plain,
e2 = op(e3,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f187,plain,
e3 = op(e3,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f188,plain,
e1 = op(e2,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f189,plain,
e4 = op(e2,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f190,plain,
e3 = op(e2,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f191,plain,
e0 = op(e2,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f192,plain,
e2 = op(e2,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f193,plain,
e3 = op(e1,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f194,plain,
e2 = op(e1,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f195,plain,
e0 = op(e1,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f196,plain,
e4 = op(e1,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f197,plain,
e1 = op(e1,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f198,plain,
e4 = op(e0,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f199,plain,
e3 = op(e0,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f200,plain,
e2 = op(e0,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f201,plain,
e1 = op(e0,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f202,plain,
e0 = op(e0,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f203,plain,
e0 = unit,
inference(cnf_transformation,[],[f3]) ).
fof(f205,plain,
( e1 != op(e3,e3)
| ~ sP79 ),
inference(cnf_transformation,[],[f88]) ).
fof(f209,plain,
( e2 != op(e4,e4)
| ~ sP78 ),
inference(cnf_transformation,[],[f89]) ).
fof(f216,plain,
( e3 != op(e2,e2)
| ~ sP77 ),
inference(cnf_transformation,[],[f90]) ).
fof(f222,plain,
( e4 != op(e1,e1)
| ~ sP76 ),
inference(cnf_transformation,[],[f91]) ).
fof(f228,plain,
( e0 != op(e0,e0)
| ~ sP75 ),
inference(cnf_transformation,[],[f92]) ).
fof(f232,plain,
( e1 != op(e0,e1)
| ~ sP74 ),
inference(cnf_transformation,[],[f93]) ).
fof(f236,plain,
( e2 != op(e0,e2)
| ~ sP73 ),
inference(cnf_transformation,[],[f94]) ).
fof(f240,plain,
( e3 != op(e0,e3)
| ~ sP72 ),
inference(cnf_transformation,[],[f95]) ).
fof(f244,plain,
( e4 != op(e0,e4)
| ~ sP71 ),
inference(cnf_transformation,[],[f96]) ).
fof(f252,plain,
( e1 != op(e1,e0)
| ~ sP70 ),
inference(cnf_transformation,[],[f97]) ).
fof(f254,plain,
( e4 != op(e1,e1)
| ~ sP69 ),
inference(cnf_transformation,[],[f98]) ).
fof(f263,plain,
( e0 != op(e1,e2)
| ~ sP68 ),
inference(cnf_transformation,[],[f99]) ).
fof(f266,plain,
( e2 != op(e1,e3)
| ~ sP67 ),
inference(cnf_transformation,[],[f100]) ).
fof(f270,plain,
( e3 != op(e1,e4)
| ~ sP66 ),
inference(cnf_transformation,[],[f101]) ).
fof(f276,plain,
( e2 != op(e2,e0)
| ~ sP65 ),
inference(cnf_transformation,[],[f102]) ).
fof(f283,plain,
( e0 != op(e2,e1)
| ~ sP64 ),
inference(cnf_transformation,[],[f103]) ).
fof(f285,plain,
( e3 != op(e2,e2)
| ~ sP63 ),
inference(cnf_transformation,[],[f104]) ).
fof(f289,plain,
( e4 != op(e2,e3)
| ~ sP62 ),
inference(cnf_transformation,[],[f105]) ).
fof(f297,plain,
( e1 != op(e2,e4)
| ~ sP61 ),
inference(cnf_transformation,[],[f106]) ).
fof(f300,plain,
( e3 != op(e3,e0)
| ~ sP60 ),
inference(cnf_transformation,[],[f107]) ).
fof(f306,plain,
( e2 != op(e3,e1)
| ~ sP59 ),
inference(cnf_transformation,[],[f108]) ).
fof(f309,plain,
( e4 != op(e3,e2)
| ~ sP58 ),
inference(cnf_transformation,[],[f109]) ).
fof(f317,plain,
( e1 != op(e3,e3)
| ~ sP57 ),
inference(cnf_transformation,[],[f110]) ).
fof(f323,plain,
( e0 != op(e3,e4)
| ~ sP56 ),
inference(cnf_transformation,[],[f111]) ).
fof(f324,plain,
( e4 != op(e4,e0)
| ~ sP55 ),
inference(cnf_transformation,[],[f112]) ).
fof(f330,plain,
( e3 != op(e4,e1)
| ~ sP54 ),
inference(cnf_transformation,[],[f113]) ).
fof(f337,plain,
( e1 != op(e4,e2)
| ~ sP53 ),
inference(cnf_transformation,[],[f114]) ).
fof(f343,plain,
( e0 != op(e4,e3)
| ~ sP52 ),
inference(cnf_transformation,[],[f115]) ).
fof(f346,plain,
( e2 != op(e4,e4)
| ~ sP51 ),
inference(cnf_transformation,[],[f116]) ).
fof(f353,plain,
( e0 != unit
| ~ sP50 ),
inference(cnf_transformation,[],[f117]) ).
fof(f358,plain,
( e0 != op(e0,e0)
| ~ sP49 ),
inference(cnf_transformation,[],[f118]) ).
fof(f363,plain,
( e0 != op(e0,e0)
| ~ sP48 ),
inference(cnf_transformation,[],[f119]) ).
fof(f367,plain,
( e1 != op(e0,e1)
| ~ sP47 ),
inference(cnf_transformation,[],[f120]) ).
fof(f372,plain,
( e1 != op(e1,e0)
| ~ sP46 ),
inference(cnf_transformation,[],[f121]) ).
fof(f376,plain,
( e2 != op(e0,e2)
| ~ sP45 ),
inference(cnf_transformation,[],[f122]) ).
fof(f381,plain,
( e2 != op(e2,e0)
| ~ sP44 ),
inference(cnf_transformation,[],[f123]) ).
fof(f385,plain,
( e3 != op(e0,e3)
| ~ sP43 ),
inference(cnf_transformation,[],[f124]) ).
fof(f390,plain,
( e3 != op(e3,e0)
| ~ sP42 ),
inference(cnf_transformation,[],[f125]) ).
fof(f394,plain,
( e4 != op(e0,e4)
| ~ sP41 ),
inference(cnf_transformation,[],[f126]) ).
fof(f399,plain,
( e4 != op(e4,e0)
| ~ sP40 ),
inference(cnf_transformation,[],[f127]) ).
fof(f406,plain,
( e0 != op(e1,e2)
| ~ sP39 ),
inference(cnf_transformation,[],[f128]) ).
fof(f411,plain,
( e0 != op(e2,e1)
| ~ sP38 ),
inference(cnf_transformation,[],[f129]) ).
fof(f418,plain,
( e1 != op(e1,e0)
| ~ sP37 ),
inference(cnf_transformation,[],[f130]) ).
fof(f423,plain,
( e1 != op(e0,e1)
| ~ sP36 ),
inference(cnf_transformation,[],[f131]) ).
fof(f425,plain,
( e2 != op(e1,e3)
| ~ sP35 ),
inference(cnf_transformation,[],[f132]) ).
fof(f430,plain,
( e2 != op(e3,e1)
| ~ sP34 ),
inference(cnf_transformation,[],[f133]) ).
fof(f434,plain,
( e3 != op(e1,e4)
| ~ sP33 ),
inference(cnf_transformation,[],[f134]) ).
fof(f439,plain,
( e3 != op(e4,e1)
| ~ sP32 ),
inference(cnf_transformation,[],[f135]) ).
fof(f447,plain,
( e4 != op(e1,e1)
| ~ sP31 ),
inference(cnf_transformation,[],[f136]) ).
fof(f452,plain,
( e4 != op(e1,e1)
| ~ sP30 ),
inference(cnf_transformation,[],[f137]) ).
fof(f457,plain,
( e0 != op(e2,e1)
| ~ sP29 ),
inference(cnf_transformation,[],[f138]) ).
fof(f462,plain,
( e0 != op(e1,e2)
| ~ sP28 ),
inference(cnf_transformation,[],[f139]) ).
fof(f464,plain,
( e1 != op(e2,e4)
| ~ sP27 ),
inference(cnf_transformation,[],[f140]) ).
fof(f469,plain,
( e1 != op(e4,e2)
| ~ sP26 ),
inference(cnf_transformation,[],[f141]) ).
fof(f478,plain,
( e2 != op(e2,e0)
| ~ sP25 ),
inference(cnf_transformation,[],[f142]) ).
fof(f483,plain,
( e2 != op(e0,e2)
| ~ sP24 ),
inference(cnf_transformation,[],[f143]) ).
fof(f486,plain,
( e3 != op(e2,e2)
| ~ sP23 ),
inference(cnf_transformation,[],[f144]) ).
fof(f491,plain,
( e3 != op(e2,e2)
| ~ sP22 ),
inference(cnf_transformation,[],[f145]) ).
fof(f495,plain,
( e4 != op(e2,e3)
| ~ sP21 ),
inference(cnf_transformation,[],[f146]) ).
fof(f500,plain,
( e4 != op(e3,e2)
| ~ sP20 ),
inference(cnf_transformation,[],[f147]) ).
fof(f504,plain,
( e0 != op(e3,e4)
| ~ sP19 ),
inference(cnf_transformation,[],[f148]) ).
fof(f509,plain,
( e0 != op(e4,e3)
| ~ sP18 ),
inference(cnf_transformation,[],[f149]) ).
fof(f515,plain,
( e1 != op(e3,e3)
| ~ sP17 ),
inference(cnf_transformation,[],[f150]) ).
fof(f520,plain,
( e1 != op(e3,e3)
| ~ sP16 ),
inference(cnf_transformation,[],[f151]) ).
fof(f527,plain,
( e2 != op(e3,e1)
| ~ sP15 ),
inference(cnf_transformation,[],[f152]) ).
fof(f532,plain,
( e2 != op(e1,e3)
| ~ sP14 ),
inference(cnf_transformation,[],[f153]) ).
fof(f538,plain,
( e3 != op(e3,e0)
| ~ sP13 ),
inference(cnf_transformation,[],[f154]) ).
fof(f543,plain,
( e3 != op(e0,e3)
| ~ sP12 ),
inference(cnf_transformation,[],[f155]) ).
fof(f546,plain,
( e4 != op(e3,e2)
| ~ sP11 ),
inference(cnf_transformation,[],[f156]) ).
fof(f551,plain,
( e4 != op(e2,e3)
| ~ sP10 ),
inference(cnf_transformation,[],[f157]) ).
fof(f555,plain,
( e0 != op(e4,e3)
| ~ sP9 ),
inference(cnf_transformation,[],[f158]) ).
fof(f560,plain,
( e0 != op(e3,e4)
| ~ sP8 ),
inference(cnf_transformation,[],[f159]) ).
fof(f566,plain,
( e1 != op(e4,e2)
| ~ sP7 ),
inference(cnf_transformation,[],[f160]) ).
fof(f571,plain,
( e1 != op(e2,e4)
| ~ sP6 ),
inference(cnf_transformation,[],[f161]) ).
fof(f574,plain,
( e2 != op(e4,e4)
| ~ sP5 ),
inference(cnf_transformation,[],[f162]) ).
fof(f579,plain,
( e2 != op(e4,e4)
| ~ sP4 ),
inference(cnf_transformation,[],[f163]) ).
fof(f587,plain,
( e3 != op(e4,e1)
| ~ sP3 ),
inference(cnf_transformation,[],[f164]) ).
fof(f592,plain,
( e3 != op(e1,e4)
| ~ sP2 ),
inference(cnf_transformation,[],[f165]) ).
fof(f598,plain,
( e4 != op(e4,e0)
| ~ sP1 ),
inference(cnf_transformation,[],[f166]) ).
fof(f603,plain,
( e4 != op(e0,e4)
| ~ sP0 ),
inference(cnf_transformation,[],[f167]) ).
fof(f608,plain,
( e0 != op(e0,e0)
| sP79
| sP78
| sP77
| sP76
| sP75
| sP74
| sP73
| sP72
| sP71
| sP70
| sP69
| sP68
| sP67
| sP66
| sP65
| sP64
| sP63
| sP62
| sP61
| sP60
| sP59
| sP58
| sP57
| sP56
| sP55
| sP54
| sP53
| sP52
| sP51
| e0 != op(unit,e0)
| e0 != op(e0,unit)
| e1 != op(unit,e1)
| e1 != op(e1,unit)
| e2 != op(unit,e2)
| e2 != op(e2,unit)
| e3 != op(unit,e3)
| e3 != op(e3,unit)
| e4 != op(unit,e4)
| e4 != op(e4,unit)
| sP50
| sP49
| sP48
| sP47
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP39
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP29
| sP28
| sP27
| sP26
| sP25
| sP24
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f87]) ).
fof(f613,plain,
unit = op(unit,unit),
inference(definition_unfolding,[],[f202,f203,f203,f203]) ).
fof(f614,plain,
e1 = op(unit,e1),
inference(definition_unfolding,[],[f201,f203]) ).
fof(f615,plain,
e2 = op(unit,e2),
inference(definition_unfolding,[],[f200,f203]) ).
fof(f616,plain,
e3 = op(unit,e3),
inference(definition_unfolding,[],[f199,f203]) ).
fof(f617,plain,
e4 = op(unit,e4),
inference(definition_unfolding,[],[f198,f203]) ).
fof(f618,plain,
e1 = op(e1,unit),
inference(definition_unfolding,[],[f197,f203]) ).
fof(f619,plain,
op(e1,e2) = unit,
inference(definition_unfolding,[],[f195,f203]) ).
fof(f620,plain,
e2 = op(e2,unit),
inference(definition_unfolding,[],[f192,f203]) ).
fof(f621,plain,
op(e2,e1) = unit,
inference(definition_unfolding,[],[f191,f203]) ).
fof(f622,plain,
e3 = op(e3,unit),
inference(definition_unfolding,[],[f187,f203]) ).
fof(f623,plain,
op(e3,e4) = unit,
inference(definition_unfolding,[],[f183,f203]) ).
fof(f624,plain,
e4 = op(e4,unit),
inference(definition_unfolding,[],[f182,f203]) ).
fof(f625,plain,
op(e4,e3) = unit,
inference(definition_unfolding,[],[f179,f203]) ).
fof(f630,plain,
( unit != op(unit,unit)
| ~ sP75 ),
inference(definition_unfolding,[],[f228,f203,f203,f203]) ).
fof(f636,plain,
( e1 != op(unit,e1)
| ~ sP74 ),
inference(definition_unfolding,[],[f232,f203]) ).
fof(f642,plain,
( e2 != op(unit,e2)
| ~ sP73 ),
inference(definition_unfolding,[],[f236,f203]) ).
fof(f648,plain,
( e3 != op(unit,e3)
| ~ sP72 ),
inference(definition_unfolding,[],[f240,f203]) ).
fof(f654,plain,
( e4 != op(unit,e4)
| ~ sP71 ),
inference(definition_unfolding,[],[f244,f203]) ).
fof(f656,plain,
( e1 != op(e1,unit)
| ~ sP70 ),
inference(definition_unfolding,[],[f252,f203]) ).
fof(f661,plain,
( op(e1,e2) != unit
| ~ sP68 ),
inference(definition_unfolding,[],[f263,f203]) ).
fof(f666,plain,
( e2 != op(e2,unit)
| ~ sP65 ),
inference(definition_unfolding,[],[f276,f203]) ).
fof(f669,plain,
( op(e2,e1) != unit
| ~ sP64 ),
inference(definition_unfolding,[],[f283,f203]) ).
fof(f676,plain,
( e3 != op(e3,unit)
| ~ sP60 ),
inference(definition_unfolding,[],[f300,f203]) ).
fof(f681,plain,
( op(e3,e4) != unit
| ~ sP56 ),
inference(definition_unfolding,[],[f323,f203]) ).
fof(f686,plain,
( e4 != op(e4,unit)
| ~ sP55 ),
inference(definition_unfolding,[],[f324,f203]) ).
fof(f689,plain,
( op(e4,e3) != unit
| ~ sP52 ),
inference(definition_unfolding,[],[f343,f203]) ).
fof(f691,plain,
( unit != unit
| ~ sP50 ),
inference(definition_unfolding,[],[f353,f203]) ).
fof(f692,plain,
( unit != op(unit,unit)
| ~ sP49 ),
inference(definition_unfolding,[],[f358,f203,f203,f203]) ).
fof(f697,plain,
( unit != op(unit,unit)
| ~ sP48 ),
inference(definition_unfolding,[],[f363,f203,f203,f203]) ).
fof(f703,plain,
( e1 != op(unit,e1)
| ~ sP47 ),
inference(definition_unfolding,[],[f367,f203]) ).
fof(f708,plain,
( e1 != op(e1,unit)
| ~ sP46 ),
inference(definition_unfolding,[],[f372,f203]) ).
fof(f714,plain,
( e2 != op(unit,e2)
| ~ sP45 ),
inference(definition_unfolding,[],[f376,f203]) ).
fof(f719,plain,
( e2 != op(e2,unit)
| ~ sP44 ),
inference(definition_unfolding,[],[f381,f203]) ).
fof(f725,plain,
( e3 != op(unit,e3)
| ~ sP43 ),
inference(definition_unfolding,[],[f385,f203]) ).
fof(f730,plain,
( e3 != op(e3,unit)
| ~ sP42 ),
inference(definition_unfolding,[],[f390,f203]) ).
fof(f736,plain,
( e4 != op(unit,e4)
| ~ sP41 ),
inference(definition_unfolding,[],[f394,f203]) ).
fof(f741,plain,
( e4 != op(e4,unit)
| ~ sP40 ),
inference(definition_unfolding,[],[f399,f203]) ).
fof(f744,plain,
( op(e1,e2) != unit
| ~ sP39 ),
inference(definition_unfolding,[],[f406,f203]) ).
fof(f749,plain,
( op(e2,e1) != unit
| ~ sP38 ),
inference(definition_unfolding,[],[f411,f203]) ).
fof(f752,plain,
( e1 != op(e1,unit)
| ~ sP37 ),
inference(definition_unfolding,[],[f418,f203]) ).
fof(f753,plain,
( e1 != op(unit,e1)
| ~ sP36 ),
inference(definition_unfolding,[],[f423,f203]) ).
fof(f761,plain,
( op(e2,e1) != unit
| ~ sP29 ),
inference(definition_unfolding,[],[f457,f203]) ).
fof(f766,plain,
( op(e1,e2) != unit
| ~ sP28 ),
inference(definition_unfolding,[],[f462,f203]) ).
fof(f772,plain,
( e2 != op(e2,unit)
| ~ sP25 ),
inference(definition_unfolding,[],[f478,f203]) ).
fof(f773,plain,
( e2 != op(unit,e2)
| ~ sP24 ),
inference(definition_unfolding,[],[f483,f203]) ).
fof(f782,plain,
( op(e3,e4) != unit
| ~ sP19 ),
inference(definition_unfolding,[],[f504,f203]) ).
fof(f787,plain,
( op(e4,e3) != unit
| ~ sP18 ),
inference(definition_unfolding,[],[f509,f203]) ).
fof(f792,plain,
( e3 != op(e3,unit)
| ~ sP13 ),
inference(definition_unfolding,[],[f538,f203]) ).
fof(f793,plain,
( e3 != op(unit,e3)
| ~ sP12 ),
inference(definition_unfolding,[],[f543,f203]) ).
fof(f799,plain,
( op(e4,e3) != unit
| ~ sP9 ),
inference(definition_unfolding,[],[f555,f203]) ).
fof(f804,plain,
( op(e3,e4) != unit
| ~ sP8 ),
inference(definition_unfolding,[],[f560,f203]) ).
fof(f812,plain,
( e4 != op(e4,unit)
| ~ sP1 ),
inference(definition_unfolding,[],[f598,f203]) ).
fof(f813,plain,
( e4 != op(unit,e4)
| ~ sP0 ),
inference(definition_unfolding,[],[f603,f203]) ).
fof(f814,plain,
( unit != op(unit,unit)
| sP79
| sP78
| sP77
| sP76
| sP75
| sP74
| sP73
| sP72
| sP71
| sP70
| sP69
| sP68
| sP67
| sP66
| sP65
| sP64
| sP63
| sP62
| sP61
| sP60
| sP59
| sP58
| sP57
| sP56
| sP55
| sP54
| sP53
| sP52
| sP51
| unit != op(unit,unit)
| unit != op(unit,unit)
| e1 != op(unit,e1)
| e1 != op(e1,unit)
| e2 != op(unit,e2)
| e2 != op(e2,unit)
| e3 != op(unit,e3)
| e3 != op(e3,unit)
| e4 != op(unit,e4)
| e4 != op(e4,unit)
| sP50
| sP49
| sP48
| sP47
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP39
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP29
| sP28
| sP27
| sP26
| sP25
| sP24
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(definition_unfolding,[],[f608,f203,f203,f203,f203,f203,f203,f203]) ).
fof(f819,definition,
! [X0,X1] :
( sQ80_eqProxy(X0,X1)
<=> X0 = X1 ),
introduced(definition,[new_symbols(definition,[sQ80_eqProxy])],[equality_proxy_definition]) ).
fof(f830,plain,
sQ80_eqProxy(unit,op(unit,unit)),
inference(equality_proxy_replacement,[],[f613,f819]) ).
fof(f831,plain,
sQ80_eqProxy(e1,op(unit,e1)),
inference(equality_proxy_replacement,[],[f614,f819]) ).
fof(f832,plain,
sQ80_eqProxy(e2,op(unit,e2)),
inference(equality_proxy_replacement,[],[f615,f819]) ).
fof(f833,plain,
sQ80_eqProxy(e3,op(unit,e3)),
inference(equality_proxy_replacement,[],[f616,f819]) ).
fof(f834,plain,
sQ80_eqProxy(e4,op(unit,e4)),
inference(equality_proxy_replacement,[],[f617,f819]) ).
fof(f835,plain,
sQ80_eqProxy(e1,op(e1,unit)),
inference(equality_proxy_replacement,[],[f618,f819]) ).
fof(f836,plain,
sQ80_eqProxy(e4,op(e1,e1)),
inference(equality_proxy_replacement,[],[f196,f819]) ).
fof(f837,plain,
sQ80_eqProxy(op(e1,e2),unit),
inference(equality_proxy_replacement,[],[f619,f819]) ).
fof(f838,plain,
sQ80_eqProxy(e2,op(e1,e3)),
inference(equality_proxy_replacement,[],[f194,f819]) ).
fof(f839,plain,
sQ80_eqProxy(e3,op(e1,e4)),
inference(equality_proxy_replacement,[],[f193,f819]) ).
fof(f840,plain,
sQ80_eqProxy(e2,op(e2,unit)),
inference(equality_proxy_replacement,[],[f620,f819]) ).
fof(f841,plain,
sQ80_eqProxy(op(e2,e1),unit),
inference(equality_proxy_replacement,[],[f621,f819]) ).
fof(f842,plain,
sQ80_eqProxy(e3,op(e2,e2)),
inference(equality_proxy_replacement,[],[f190,f819]) ).
fof(f843,plain,
sQ80_eqProxy(e4,op(e2,e3)),
inference(equality_proxy_replacement,[],[f189,f819]) ).
fof(f844,plain,
sQ80_eqProxy(e1,op(e2,e4)),
inference(equality_proxy_replacement,[],[f188,f819]) ).
fof(f845,plain,
sQ80_eqProxy(e3,op(e3,unit)),
inference(equality_proxy_replacement,[],[f622,f819]) ).
fof(f846,plain,
sQ80_eqProxy(e2,op(e3,e1)),
inference(equality_proxy_replacement,[],[f186,f819]) ).
fof(f847,plain,
sQ80_eqProxy(e4,op(e3,e2)),
inference(equality_proxy_replacement,[],[f185,f819]) ).
fof(f848,plain,
sQ80_eqProxy(e1,op(e3,e3)),
inference(equality_proxy_replacement,[],[f184,f819]) ).
fof(f849,plain,
sQ80_eqProxy(op(e3,e4),unit),
inference(equality_proxy_replacement,[],[f623,f819]) ).
fof(f850,plain,
sQ80_eqProxy(e4,op(e4,unit)),
inference(equality_proxy_replacement,[],[f624,f819]) ).
fof(f851,plain,
sQ80_eqProxy(e3,op(e4,e1)),
inference(equality_proxy_replacement,[],[f181,f819]) ).
fof(f852,plain,
sQ80_eqProxy(e1,op(e4,e2)),
inference(equality_proxy_replacement,[],[f180,f819]) ).
fof(f853,plain,
sQ80_eqProxy(op(e4,e3),unit),
inference(equality_proxy_replacement,[],[f625,f819]) ).
fof(f854,plain,
sQ80_eqProxy(e2,op(e4,e4)),
inference(equality_proxy_replacement,[],[f178,f819]) ).
fof(f858,plain,
( ~ sQ80_eqProxy(e1,op(e3,e3))
| ~ sP79 ),
inference(equality_proxy_replacement,[],[f205,f819]) ).
fof(f864,plain,
( ~ sQ80_eqProxy(e2,op(e4,e4))
| ~ sP78 ),
inference(equality_proxy_replacement,[],[f209,f819]) ).
fof(f867,plain,
( ~ sQ80_eqProxy(e3,op(e2,e2))
| ~ sP77 ),
inference(equality_proxy_replacement,[],[f216,f819]) ).
fof(f871,plain,
( ~ sQ80_eqProxy(e4,op(e1,e1))
| ~ sP76 ),
inference(equality_proxy_replacement,[],[f222,f819]) ).
fof(f875,plain,
( ~ sQ80_eqProxy(unit,op(unit,unit))
| ~ sP75 ),
inference(equality_proxy_replacement,[],[f630,f819]) ).
fof(f881,plain,
( ~ sQ80_eqProxy(e1,op(unit,e1))
| ~ sP74 ),
inference(equality_proxy_replacement,[],[f636,f819]) ).
fof(f887,plain,
( ~ sQ80_eqProxy(e2,op(unit,e2))
| ~ sP73 ),
inference(equality_proxy_replacement,[],[f642,f819]) ).
fof(f893,plain,
( ~ sQ80_eqProxy(e3,op(unit,e3))
| ~ sP72 ),
inference(equality_proxy_replacement,[],[f648,f819]) ).
fof(f899,plain,
( ~ sQ80_eqProxy(e4,op(unit,e4))
| ~ sP71 ),
inference(equality_proxy_replacement,[],[f654,f819]) ).
fof(f901,plain,
( ~ sQ80_eqProxy(e1,op(e1,unit))
| ~ sP70 ),
inference(equality_proxy_replacement,[],[f656,f819]) ).
fof(f909,plain,
( ~ sQ80_eqProxy(e4,op(e1,e1))
| ~ sP69 ),
inference(equality_proxy_replacement,[],[f254,f819]) ).
fof(f910,plain,
( ~ sQ80_eqProxy(op(e1,e2),unit)
| ~ sP68 ),
inference(equality_proxy_replacement,[],[f661,f819]) ).
fof(f917,plain,
( ~ sQ80_eqProxy(e2,op(e1,e3))
| ~ sP67 ),
inference(equality_proxy_replacement,[],[f266,f819]) ).
fof(f923,plain,
( ~ sQ80_eqProxy(e3,op(e1,e4))
| ~ sP66 ),
inference(equality_proxy_replacement,[],[f270,f819]) ).
fof(f927,plain,
( ~ sQ80_eqProxy(e2,op(e2,unit))
| ~ sP65 ),
inference(equality_proxy_replacement,[],[f666,f819]) ).
fof(f930,plain,
( ~ sQ80_eqProxy(op(e2,e1),unit)
| ~ sP64 ),
inference(equality_proxy_replacement,[],[f669,f819]) ).
fof(f938,plain,
( ~ sQ80_eqProxy(e3,op(e2,e2))
| ~ sP63 ),
inference(equality_proxy_replacement,[],[f285,f819]) ).
fof(f944,plain,
( ~ sQ80_eqProxy(e4,op(e2,e3))
| ~ sP62 ),
inference(equality_proxy_replacement,[],[f289,f819]) ).
fof(f946,plain,
( ~ sQ80_eqProxy(e1,op(e2,e4))
| ~ sP61 ),
inference(equality_proxy_replacement,[],[f297,f819]) ).
fof(f953,plain,
( ~ sQ80_eqProxy(e3,op(e3,unit))
| ~ sP60 ),
inference(equality_proxy_replacement,[],[f676,f819]) ).
fof(f957,plain,
( ~ sQ80_eqProxy(e2,op(e3,e1))
| ~ sP59 ),
inference(equality_proxy_replacement,[],[f306,f819]) ).
fof(f964,plain,
( ~ sQ80_eqProxy(e4,op(e3,e2))
| ~ sP58 ),
inference(equality_proxy_replacement,[],[f309,f819]) ).
fof(f966,plain,
( ~ sQ80_eqProxy(e1,op(e3,e3))
| ~ sP57 ),
inference(equality_proxy_replacement,[],[f317,f819]) ).
fof(f970,plain,
( ~ sQ80_eqProxy(op(e3,e4),unit)
| ~ sP56 ),
inference(equality_proxy_replacement,[],[f681,f819]) ).
fof(f979,plain,
( ~ sQ80_eqProxy(e4,op(e4,unit))
| ~ sP55 ),
inference(equality_proxy_replacement,[],[f686,f819]) ).
fof(f983,plain,
( ~ sQ80_eqProxy(e3,op(e4,e1))
| ~ sP54 ),
inference(equality_proxy_replacement,[],[f330,f819]) ).
fof(f986,plain,
( ~ sQ80_eqProxy(e1,op(e4,e2))
| ~ sP53 ),
inference(equality_proxy_replacement,[],[f337,f819]) ).
fof(f990,plain,
( ~ sQ80_eqProxy(op(e4,e3),unit)
| ~ sP52 ),
inference(equality_proxy_replacement,[],[f689,f819]) ).
fof(f997,plain,
( ~ sQ80_eqProxy(e2,op(e4,e4))
| ~ sP51 ),
inference(equality_proxy_replacement,[],[f346,f819]) ).
fof(f1000,plain,
( ~ sQ80_eqProxy(unit,unit)
| ~ sP50 ),
inference(equality_proxy_replacement,[],[f691,f819]) ).
fof(f1005,plain,
( ~ sQ80_eqProxy(unit,op(unit,unit))
| ~ sP49 ),
inference(equality_proxy_replacement,[],[f692,f819]) ).
fof(f1010,plain,
( ~ sQ80_eqProxy(unit,op(unit,unit))
| ~ sP48 ),
inference(equality_proxy_replacement,[],[f697,f819]) ).
fof(f1016,plain,
( ~ sQ80_eqProxy(e1,op(unit,e1))
| ~ sP47 ),
inference(equality_proxy_replacement,[],[f703,f819]) ).
fof(f1021,plain,
( ~ sQ80_eqProxy(e1,op(e1,unit))
| ~ sP46 ),
inference(equality_proxy_replacement,[],[f708,f819]) ).
fof(f1027,plain,
( ~ sQ80_eqProxy(e2,op(unit,e2))
| ~ sP45 ),
inference(equality_proxy_replacement,[],[f714,f819]) ).
fof(f1032,plain,
( ~ sQ80_eqProxy(e2,op(e2,unit))
| ~ sP44 ),
inference(equality_proxy_replacement,[],[f719,f819]) ).
fof(f1038,plain,
( ~ sQ80_eqProxy(e3,op(unit,e3))
| ~ sP43 ),
inference(equality_proxy_replacement,[],[f725,f819]) ).
fof(f1043,plain,
( ~ sQ80_eqProxy(e3,op(e3,unit))
| ~ sP42 ),
inference(equality_proxy_replacement,[],[f730,f819]) ).
fof(f1049,plain,
( ~ sQ80_eqProxy(e4,op(unit,e4))
| ~ sP41 ),
inference(equality_proxy_replacement,[],[f736,f819]) ).
fof(f1054,plain,
( ~ sQ80_eqProxy(e4,op(e4,unit))
| ~ sP40 ),
inference(equality_proxy_replacement,[],[f741,f819]) ).
fof(f1057,plain,
( ~ sQ80_eqProxy(op(e1,e2),unit)
| ~ sP39 ),
inference(equality_proxy_replacement,[],[f744,f819]) ).
fof(f1062,plain,
( ~ sQ80_eqProxy(op(e2,e1),unit)
| ~ sP38 ),
inference(equality_proxy_replacement,[],[f749,f819]) ).
fof(f1065,plain,
( ~ sQ80_eqProxy(e1,op(e1,unit))
| ~ sP37 ),
inference(equality_proxy_replacement,[],[f752,f819]) ).
fof(f1070,plain,
( ~ sQ80_eqProxy(e1,op(unit,e1))
| ~ sP36 ),
inference(equality_proxy_replacement,[],[f753,f819]) ).
fof(f1078,plain,
( ~ sQ80_eqProxy(e2,op(e1,e3))
| ~ sP35 ),
inference(equality_proxy_replacement,[],[f425,f819]) ).
fof(f1083,plain,
( ~ sQ80_eqProxy(e2,op(e3,e1))
| ~ sP34 ),
inference(equality_proxy_replacement,[],[f430,f819]) ).
fof(f1089,plain,
( ~ sQ80_eqProxy(e3,op(e1,e4))
| ~ sP33 ),
inference(equality_proxy_replacement,[],[f434,f819]) ).
fof(f1094,plain,
( ~ sQ80_eqProxy(e3,op(e4,e1))
| ~ sP32 ),
inference(equality_proxy_replacement,[],[f439,f819]) ).
fof(f1096,plain,
( ~ sQ80_eqProxy(e4,op(e1,e1))
| ~ sP31 ),
inference(equality_proxy_replacement,[],[f447,f819]) ).
fof(f1101,plain,
( ~ sQ80_eqProxy(e4,op(e1,e1))
| ~ sP30 ),
inference(equality_proxy_replacement,[],[f452,f819]) ).
fof(f1106,plain,
( ~ sQ80_eqProxy(op(e2,e1),unit)
| ~ sP29 ),
inference(equality_proxy_replacement,[],[f761,f819]) ).
fof(f1111,plain,
( ~ sQ80_eqProxy(op(e1,e2),unit)
| ~ sP28 ),
inference(equality_proxy_replacement,[],[f766,f819]) ).
fof(f1119,plain,
( ~ sQ80_eqProxy(e1,op(e2,e4))
| ~ sP27 ),
inference(equality_proxy_replacement,[],[f464,f819]) ).
fof(f1124,plain,
( ~ sQ80_eqProxy(e1,op(e4,e2))
| ~ sP26 ),
inference(equality_proxy_replacement,[],[f469,f819]) ).
fof(f1125,plain,
( ~ sQ80_eqProxy(e2,op(e2,unit))
| ~ sP25 ),
inference(equality_proxy_replacement,[],[f772,f819]) ).
fof(f1130,plain,
( ~ sQ80_eqProxy(e2,op(unit,e2))
| ~ sP24 ),
inference(equality_proxy_replacement,[],[f773,f819]) ).
fof(f1137,plain,
( ~ sQ80_eqProxy(e3,op(e2,e2))
| ~ sP23 ),
inference(equality_proxy_replacement,[],[f486,f819]) ).
fof(f1142,plain,
( ~ sQ80_eqProxy(e3,op(e2,e2))
| ~ sP22 ),
inference(equality_proxy_replacement,[],[f491,f819]) ).
fof(f1148,plain,
( ~ sQ80_eqProxy(e4,op(e2,e3))
| ~ sP21 ),
inference(equality_proxy_replacement,[],[f495,f819]) ).
fof(f1153,plain,
( ~ sQ80_eqProxy(e4,op(e3,e2))
| ~ sP20 ),
inference(equality_proxy_replacement,[],[f500,f819]) ).
fof(f1159,plain,
( ~ sQ80_eqProxy(op(e3,e4),unit)
| ~ sP19 ),
inference(equality_proxy_replacement,[],[f782,f819]) ).
fof(f1164,plain,
( ~ sQ80_eqProxy(op(e4,e3),unit)
| ~ sP18 ),
inference(equality_proxy_replacement,[],[f787,f819]) ).
fof(f1168,plain,
( ~ sQ80_eqProxy(e1,op(e3,e3))
| ~ sP17 ),
inference(equality_proxy_replacement,[],[f515,f819]) ).
fof(f1173,plain,
( ~ sQ80_eqProxy(e1,op(e3,e3))
| ~ sP16 ),
inference(equality_proxy_replacement,[],[f520,f819]) ).
fof(f1176,plain,
( ~ sQ80_eqProxy(e2,op(e3,e1))
| ~ sP15 ),
inference(equality_proxy_replacement,[],[f527,f819]) ).
fof(f1181,plain,
( ~ sQ80_eqProxy(e2,op(e1,e3))
| ~ sP14 ),
inference(equality_proxy_replacement,[],[f532,f819]) ).
fof(f1185,plain,
( ~ sQ80_eqProxy(e3,op(e3,unit))
| ~ sP13 ),
inference(equality_proxy_replacement,[],[f792,f819]) ).
fof(f1190,plain,
( ~ sQ80_eqProxy(e3,op(unit,e3))
| ~ sP12 ),
inference(equality_proxy_replacement,[],[f793,f819]) ).
fof(f1197,plain,
( ~ sQ80_eqProxy(e4,op(e3,e2))
| ~ sP11 ),
inference(equality_proxy_replacement,[],[f546,f819]) ).
fof(f1202,plain,
( ~ sQ80_eqProxy(e4,op(e2,e3))
| ~ sP10 ),
inference(equality_proxy_replacement,[],[f551,f819]) ).
fof(f1208,plain,
( ~ sQ80_eqProxy(op(e4,e3),unit)
| ~ sP9 ),
inference(equality_proxy_replacement,[],[f799,f819]) ).
fof(f1213,plain,
( ~ sQ80_eqProxy(op(e3,e4),unit)
| ~ sP8 ),
inference(equality_proxy_replacement,[],[f804,f819]) ).
fof(f1217,plain,
( ~ sQ80_eqProxy(e1,op(e4,e2))
| ~ sP7 ),
inference(equality_proxy_replacement,[],[f566,f819]) ).
fof(f1222,plain,
( ~ sQ80_eqProxy(e1,op(e2,e4))
| ~ sP6 ),
inference(equality_proxy_replacement,[],[f571,f819]) ).
fof(f1229,plain,
( ~ sQ80_eqProxy(e2,op(e4,e4))
| ~ sP5 ),
inference(equality_proxy_replacement,[],[f574,f819]) ).
fof(f1234,plain,
( ~ sQ80_eqProxy(e2,op(e4,e4))
| ~ sP4 ),
inference(equality_proxy_replacement,[],[f579,f819]) ).
fof(f1236,plain,
( ~ sQ80_eqProxy(e3,op(e4,e1))
| ~ sP3 ),
inference(equality_proxy_replacement,[],[f587,f819]) ).
fof(f1241,plain,
( ~ sQ80_eqProxy(e3,op(e1,e4))
| ~ sP2 ),
inference(equality_proxy_replacement,[],[f592,f819]) ).
fof(f1245,plain,
( ~ sQ80_eqProxy(e4,op(e4,unit))
| ~ sP1 ),
inference(equality_proxy_replacement,[],[f812,f819]) ).
fof(f1250,plain,
( ~ sQ80_eqProxy(e4,op(unit,e4))
| ~ sP0 ),
inference(equality_proxy_replacement,[],[f813,f819]) ).
fof(f1255,plain,
( ~ sQ80_eqProxy(unit,op(unit,unit))
| sP79
| sP78
| sP77
| sP76
| sP75
| sP74
| sP73
| sP72
| sP71
| sP70
| sP69
| sP68
| sP67
| sP66
| sP65
| sP64
| sP63
| sP62
| sP61
| sP60
| sP59
| sP58
| sP57
| sP56
| sP55
| sP54
| sP53
| sP52
| sP51
| ~ sQ80_eqProxy(unit,op(unit,unit))
| ~ sQ80_eqProxy(unit,op(unit,unit))
| ~ sQ80_eqProxy(e1,op(unit,e1))
| ~ sQ80_eqProxy(e1,op(e1,unit))
| ~ sQ80_eqProxy(e2,op(unit,e2))
| ~ sQ80_eqProxy(e2,op(e2,unit))
| ~ sQ80_eqProxy(e3,op(unit,e3))
| ~ sQ80_eqProxy(e3,op(e3,unit))
| ~ sQ80_eqProxy(e4,op(unit,e4))
| ~ sQ80_eqProxy(e4,op(e4,unit))
| sP50
| sP49
| sP48
| sP47
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP39
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP29
| sP28
| sP27
| sP26
| sP25
| sP24
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(equality_proxy_replacement,[],[f814,f819,f819,f819,f819,f819,f819,f819,f819,f819,f819,f819]) ).
fof(f1260,plain,
! [X0] : sQ80_eqProxy(X0,X0),
inference(equality_proxy_axiom,[],[f819]) ).
fof(f1266,plain,
( ~ sQ80_eqProxy(unit,op(unit,unit))
| sP79
| sP78
| sP77
| sP76
| sP75
| sP74
| sP73
| sP72
| sP71
| sP70
| sP69
| sP68
| sP67
| sP66
| sP65
| sP64
| sP63
| sP62
| sP61
| sP60
| sP59
| sP58
| sP57
| sP56
| sP55
| sP54
| sP53
| sP52
| sP51
| ~ sQ80_eqProxy(e1,op(unit,e1))
| ~ sQ80_eqProxy(e1,op(e1,unit))
| ~ sQ80_eqProxy(e2,op(unit,e2))
| ~ sQ80_eqProxy(e2,op(e2,unit))
| ~ sQ80_eqProxy(e3,op(unit,e3))
| ~ sQ80_eqProxy(e3,op(e3,unit))
| ~ sQ80_eqProxy(e4,op(unit,e4))
| ~ sQ80_eqProxy(e4,op(e4,unit))
| sP50
| sP49
| sP48
| sP47
| sP46
| sP45
| sP44
| sP43
| sP42
| sP41
| sP40
| sP39
| sP38
| sP37
| sP36
| sP35
| sP34
| sP33
| sP32
| sP31
| sP30
| sP29
| sP28
| sP27
| sP26
| sP25
| sP24
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(duplicate_literal_removal,[],[f1255]) ).
fof(f1268,definition,
( spl81_1
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl81_1])],[avatar_definition]) ).
fof(f1271,definition,
( spl81_2
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl81_2])],[avatar_definition]) ).
fof(f1274,definition,
( spl81_3
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl81_3])],[avatar_definition]) ).
fof(f1277,definition,
( spl81_4
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl81_4])],[avatar_definition]) ).
fof(f1280,definition,
( spl81_5
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl81_5])],[avatar_definition]) ).
fof(f1283,definition,
( spl81_6
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl81_6])],[avatar_definition]) ).
fof(f1286,definition,
( spl81_7
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl81_7])],[avatar_definition]) ).
fof(f1289,definition,
( spl81_8
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl81_8])],[avatar_definition]) ).
fof(f1292,definition,
( spl81_9
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl81_9])],[avatar_definition]) ).
fof(f1295,definition,
( spl81_10
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl81_10])],[avatar_definition]) ).
fof(f1298,definition,
( spl81_11
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl81_11])],[avatar_definition]) ).
fof(f1301,definition,
( spl81_12
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl81_12])],[avatar_definition]) ).
fof(f1304,definition,
( spl81_13
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl81_13])],[avatar_definition]) ).
fof(f1307,definition,
( spl81_14
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl81_14])],[avatar_definition]) ).
fof(f1310,definition,
( spl81_15
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl81_15])],[avatar_definition]) ).
fof(f1313,definition,
( spl81_16
<=> sP15 ),
introduced(definition,[new_symbols(definition,[spl81_16])],[avatar_definition]) ).
fof(f1316,definition,
( spl81_17
<=> sP16 ),
introduced(definition,[new_symbols(definition,[spl81_17])],[avatar_definition]) ).
fof(f1319,definition,
( spl81_18
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl81_18])],[avatar_definition]) ).
fof(f1322,definition,
( spl81_19
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl81_19])],[avatar_definition]) ).
fof(f1325,definition,
( spl81_20
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl81_20])],[avatar_definition]) ).
fof(f1328,definition,
( spl81_21
<=> sP20 ),
introduced(definition,[new_symbols(definition,[spl81_21])],[avatar_definition]) ).
fof(f1331,definition,
( spl81_22
<=> sP21 ),
introduced(definition,[new_symbols(definition,[spl81_22])],[avatar_definition]) ).
fof(f1334,definition,
( spl81_23
<=> sP22 ),
introduced(definition,[new_symbols(definition,[spl81_23])],[avatar_definition]) ).
fof(f1337,definition,
( spl81_24
<=> sP23 ),
introduced(definition,[new_symbols(definition,[spl81_24])],[avatar_definition]) ).
fof(f1340,definition,
( spl81_25
<=> sP24 ),
introduced(definition,[new_symbols(definition,[spl81_25])],[avatar_definition]) ).
fof(f1343,definition,
( spl81_26
<=> sP25 ),
introduced(definition,[new_symbols(definition,[spl81_26])],[avatar_definition]) ).
fof(f1346,definition,
( spl81_27
<=> sP26 ),
introduced(definition,[new_symbols(definition,[spl81_27])],[avatar_definition]) ).
fof(f1349,definition,
( spl81_28
<=> sP27 ),
introduced(definition,[new_symbols(definition,[spl81_28])],[avatar_definition]) ).
fof(f1352,definition,
( spl81_29
<=> sP28 ),
introduced(definition,[new_symbols(definition,[spl81_29])],[avatar_definition]) ).
fof(f1355,definition,
( spl81_30
<=> sP29 ),
introduced(definition,[new_symbols(definition,[spl81_30])],[avatar_definition]) ).
fof(f1358,definition,
( spl81_31
<=> sP30 ),
introduced(definition,[new_symbols(definition,[spl81_31])],[avatar_definition]) ).
fof(f1361,definition,
( spl81_32
<=> sP31 ),
introduced(definition,[new_symbols(definition,[spl81_32])],[avatar_definition]) ).
fof(f1364,definition,
( spl81_33
<=> sP32 ),
introduced(definition,[new_symbols(definition,[spl81_33])],[avatar_definition]) ).
fof(f1367,definition,
( spl81_34
<=> sP33 ),
introduced(definition,[new_symbols(definition,[spl81_34])],[avatar_definition]) ).
fof(f1370,definition,
( spl81_35
<=> sP34 ),
introduced(definition,[new_symbols(definition,[spl81_35])],[avatar_definition]) ).
fof(f1373,definition,
( spl81_36
<=> sP35 ),
introduced(definition,[new_symbols(definition,[spl81_36])],[avatar_definition]) ).
fof(f1376,definition,
( spl81_37
<=> sP36 ),
introduced(definition,[new_symbols(definition,[spl81_37])],[avatar_definition]) ).
fof(f1379,definition,
( spl81_38
<=> sP37 ),
introduced(definition,[new_symbols(definition,[spl81_38])],[avatar_definition]) ).
fof(f1382,definition,
( spl81_39
<=> sP38 ),
introduced(definition,[new_symbols(definition,[spl81_39])],[avatar_definition]) ).
fof(f1385,definition,
( spl81_40
<=> sP39 ),
introduced(definition,[new_symbols(definition,[spl81_40])],[avatar_definition]) ).
fof(f1388,definition,
( spl81_41
<=> sP40 ),
introduced(definition,[new_symbols(definition,[spl81_41])],[avatar_definition]) ).
fof(f1391,definition,
( spl81_42
<=> sP41 ),
introduced(definition,[new_symbols(definition,[spl81_42])],[avatar_definition]) ).
fof(f1394,definition,
( spl81_43
<=> sP42 ),
introduced(definition,[new_symbols(definition,[spl81_43])],[avatar_definition]) ).
fof(f1397,definition,
( spl81_44
<=> sP43 ),
introduced(definition,[new_symbols(definition,[spl81_44])],[avatar_definition]) ).
fof(f1400,definition,
( spl81_45
<=> sP44 ),
introduced(definition,[new_symbols(definition,[spl81_45])],[avatar_definition]) ).
fof(f1403,definition,
( spl81_46
<=> sP45 ),
introduced(definition,[new_symbols(definition,[spl81_46])],[avatar_definition]) ).
fof(f1406,definition,
( spl81_47
<=> sP46 ),
introduced(definition,[new_symbols(definition,[spl81_47])],[avatar_definition]) ).
fof(f1409,definition,
( spl81_48
<=> sP47 ),
introduced(definition,[new_symbols(definition,[spl81_48])],[avatar_definition]) ).
fof(f1412,definition,
( spl81_49
<=> sP48 ),
introduced(definition,[new_symbols(definition,[spl81_49])],[avatar_definition]) ).
fof(f1415,definition,
( spl81_50
<=> sP49 ),
introduced(definition,[new_symbols(definition,[spl81_50])],[avatar_definition]) ).
fof(f1418,definition,
( spl81_51
<=> sP50 ),
introduced(definition,[new_symbols(definition,[spl81_51])],[avatar_definition]) ).
fof(f1421,definition,
( spl81_52
<=> sQ80_eqProxy(e4,op(e4,unit)) ),
introduced(definition,[new_symbols(definition,[spl81_52])],[avatar_definition]) ).
fof(f1422,plain,
( ~ sQ80_eqProxy(e4,op(e4,unit))
| spl81_52 ),
inference(avatar_component_clause,[],[f1421]) ).
fof(f1424,definition,
( spl81_53
<=> sQ80_eqProxy(e4,op(unit,e4)) ),
introduced(definition,[new_symbols(definition,[spl81_53])],[avatar_definition]) ).
fof(f1425,plain,
( ~ sQ80_eqProxy(e4,op(unit,e4))
| spl81_53 ),
inference(avatar_component_clause,[],[f1424]) ).
fof(f1427,definition,
( spl81_54
<=> sQ80_eqProxy(e3,op(e3,unit)) ),
introduced(definition,[new_symbols(definition,[spl81_54])],[avatar_definition]) ).
fof(f1428,plain,
( ~ sQ80_eqProxy(e3,op(e3,unit))
| spl81_54 ),
inference(avatar_component_clause,[],[f1427]) ).
fof(f1430,definition,
( spl81_55
<=> sQ80_eqProxy(e3,op(unit,e3)) ),
introduced(definition,[new_symbols(definition,[spl81_55])],[avatar_definition]) ).
fof(f1431,plain,
( ~ sQ80_eqProxy(e3,op(unit,e3))
| spl81_55 ),
inference(avatar_component_clause,[],[f1430]) ).
fof(f1433,definition,
( spl81_56
<=> sQ80_eqProxy(e2,op(e2,unit)) ),
introduced(definition,[new_symbols(definition,[spl81_56])],[avatar_definition]) ).
fof(f1434,plain,
( ~ sQ80_eqProxy(e2,op(e2,unit))
| spl81_56 ),
inference(avatar_component_clause,[],[f1433]) ).
fof(f1436,definition,
( spl81_57
<=> sQ80_eqProxy(e2,op(unit,e2)) ),
introduced(definition,[new_symbols(definition,[spl81_57])],[avatar_definition]) ).
fof(f1437,plain,
( ~ sQ80_eqProxy(e2,op(unit,e2))
| spl81_57 ),
inference(avatar_component_clause,[],[f1436]) ).
fof(f1439,definition,
( spl81_58
<=> sQ80_eqProxy(e1,op(e1,unit)) ),
introduced(definition,[new_symbols(definition,[spl81_58])],[avatar_definition]) ).
fof(f1440,plain,
( ~ sQ80_eqProxy(e1,op(e1,unit))
| spl81_58 ),
inference(avatar_component_clause,[],[f1439]) ).
fof(f1442,definition,
( spl81_59
<=> sQ80_eqProxy(e1,op(unit,e1)) ),
introduced(definition,[new_symbols(definition,[spl81_59])],[avatar_definition]) ).
fof(f1443,plain,
( ~ sQ80_eqProxy(e1,op(unit,e1))
| spl81_59 ),
inference(avatar_component_clause,[],[f1442]) ).
fof(f1445,definition,
( spl81_60
<=> sQ80_eqProxy(unit,op(unit,unit)) ),
introduced(definition,[new_symbols(definition,[spl81_60])],[avatar_definition]) ).
fof(f1446,plain,
( ~ sQ80_eqProxy(unit,op(unit,unit))
| spl81_60 ),
inference(avatar_component_clause,[],[f1445]) ).
fof(f1448,definition,
( spl81_61
<=> sP51 ),
introduced(definition,[new_symbols(definition,[spl81_61])],[avatar_definition]) ).
fof(f1451,definition,
( spl81_62
<=> sP52 ),
introduced(definition,[new_symbols(definition,[spl81_62])],[avatar_definition]) ).
fof(f1454,definition,
( spl81_63
<=> sP53 ),
introduced(definition,[new_symbols(definition,[spl81_63])],[avatar_definition]) ).
fof(f1457,definition,
( spl81_64
<=> sP54 ),
introduced(definition,[new_symbols(definition,[spl81_64])],[avatar_definition]) ).
fof(f1460,definition,
( spl81_65
<=> sP55 ),
introduced(definition,[new_symbols(definition,[spl81_65])],[avatar_definition]) ).
fof(f1463,definition,
( spl81_66
<=> sP56 ),
introduced(definition,[new_symbols(definition,[spl81_66])],[avatar_definition]) ).
fof(f1466,definition,
( spl81_67
<=> sP57 ),
introduced(definition,[new_symbols(definition,[spl81_67])],[avatar_definition]) ).
fof(f1469,definition,
( spl81_68
<=> sP58 ),
introduced(definition,[new_symbols(definition,[spl81_68])],[avatar_definition]) ).
fof(f1472,definition,
( spl81_69
<=> sP59 ),
introduced(definition,[new_symbols(definition,[spl81_69])],[avatar_definition]) ).
fof(f1475,definition,
( spl81_70
<=> sP60 ),
introduced(definition,[new_symbols(definition,[spl81_70])],[avatar_definition]) ).
fof(f1478,definition,
( spl81_71
<=> sP61 ),
introduced(definition,[new_symbols(definition,[spl81_71])],[avatar_definition]) ).
fof(f1481,definition,
( spl81_72
<=> sP62 ),
introduced(definition,[new_symbols(definition,[spl81_72])],[avatar_definition]) ).
fof(f1484,definition,
( spl81_73
<=> sP63 ),
introduced(definition,[new_symbols(definition,[spl81_73])],[avatar_definition]) ).
fof(f1487,definition,
( spl81_74
<=> sP64 ),
introduced(definition,[new_symbols(definition,[spl81_74])],[avatar_definition]) ).
fof(f1490,definition,
( spl81_75
<=> sP65 ),
introduced(definition,[new_symbols(definition,[spl81_75])],[avatar_definition]) ).
fof(f1493,definition,
( spl81_76
<=> sP66 ),
introduced(definition,[new_symbols(definition,[spl81_76])],[avatar_definition]) ).
fof(f1496,definition,
( spl81_77
<=> sP67 ),
introduced(definition,[new_symbols(definition,[spl81_77])],[avatar_definition]) ).
fof(f1499,definition,
( spl81_78
<=> sP68 ),
introduced(definition,[new_symbols(definition,[spl81_78])],[avatar_definition]) ).
fof(f1502,definition,
( spl81_79
<=> sP69 ),
introduced(definition,[new_symbols(definition,[spl81_79])],[avatar_definition]) ).
fof(f1505,definition,
( spl81_80
<=> sP70 ),
introduced(definition,[new_symbols(definition,[spl81_80])],[avatar_definition]) ).
fof(f1508,definition,
( spl81_81
<=> sP71 ),
introduced(definition,[new_symbols(definition,[spl81_81])],[avatar_definition]) ).
fof(f1511,definition,
( spl81_82
<=> sP72 ),
introduced(definition,[new_symbols(definition,[spl81_82])],[avatar_definition]) ).
fof(f1514,definition,
( spl81_83
<=> sP73 ),
introduced(definition,[new_symbols(definition,[spl81_83])],[avatar_definition]) ).
fof(f1517,definition,
( spl81_84
<=> sP74 ),
introduced(definition,[new_symbols(definition,[spl81_84])],[avatar_definition]) ).
fof(f1520,definition,
( spl81_85
<=> sP75 ),
introduced(definition,[new_symbols(definition,[spl81_85])],[avatar_definition]) ).
fof(f1523,definition,
( spl81_86
<=> sP76 ),
introduced(definition,[new_symbols(definition,[spl81_86])],[avatar_definition]) ).
fof(f1526,definition,
( spl81_87
<=> sP77 ),
introduced(definition,[new_symbols(definition,[spl81_87])],[avatar_definition]) ).
fof(f1529,definition,
( spl81_88
<=> sP78 ),
introduced(definition,[new_symbols(definition,[spl81_88])],[avatar_definition]) ).
fof(f1532,definition,
( spl81_89
<=> sP79 ),
introduced(definition,[new_symbols(definition,[spl81_89])],[avatar_definition]) ).
fof(f1550,plain,
( spl81_1
| spl81_2
| spl81_3
| spl81_4
| spl81_5
| spl81_6
| spl81_7
| spl81_8
| spl81_9
| spl81_10
| spl81_11
| spl81_12
| spl81_13
| spl81_14
| spl81_15
| spl81_16
| spl81_17
| spl81_18
| spl81_19
| spl81_20
| spl81_21
| spl81_22
| spl81_23
| spl81_24
| spl81_25
| spl81_26
| spl81_27
| spl81_28
| spl81_29
| spl81_30
| spl81_31
| spl81_32
| spl81_33
| spl81_34
| spl81_35
| spl81_36
| spl81_37
| spl81_38
| spl81_39
| spl81_40
| spl81_41
| spl81_42
| spl81_43
| spl81_44
| spl81_45
| spl81_46
| spl81_47
| spl81_48
| spl81_49
| spl81_50
| spl81_51
| ~ spl81_52
| ~ spl81_53
| ~ spl81_54
| ~ spl81_55
| ~ spl81_56
| ~ spl81_57
| ~ spl81_58
| ~ spl81_59
| spl81_61
| spl81_62
| spl81_63
| spl81_64
| spl81_65
| spl81_66
| spl81_67
| spl81_68
| spl81_69
| spl81_70
| spl81_71
| spl81_72
| spl81_73
| spl81_74
| spl81_75
| spl81_76
| spl81_77
| spl81_78
| spl81_79
| spl81_80
| spl81_81
| spl81_82
| spl81_83
| spl81_84
| spl81_85
| spl81_86
| spl81_87
| spl81_88
| spl81_89
| ~ spl81_60 ),
inference(avatar_split_clause,[],[f1266,f1445,f1532,f1529,f1526,f1523,f1520,f1517,f1514,f1511,f1508,f1505,f1502,f1499,f1496,f1493,f1490,f1487,f1484,f1481,f1478,f1475,f1472,f1469,f1466,f1463,f1460,f1457,f1454,f1451,f1448,f1442,f1439,f1436,f1433,f1430,f1427,f1424,f1421,f1418,f1415,f1412,f1409,f1406,f1403,f1400,f1397,f1394,f1391,f1388,f1385,f1382,f1379,f1376,f1373,f1370,f1367,f1364,f1361,f1358,f1355,f1352,f1349,f1346,f1343,f1340,f1337,f1334,f1331,f1328,f1325,f1322,f1319,f1316,f1313,f1310,f1307,f1304,f1301,f1298,f1295,f1292,f1289,f1286,f1283,f1280,f1277,f1274,f1271,f1268]) ).
fof(f1568,plain,
( ~ spl81_1
| ~ spl81_53 ),
inference(avatar_split_clause,[],[f1250,f1424,f1268]) ).
fof(f1583,plain,
( ~ spl81_2
| ~ spl81_52 ),
inference(avatar_split_clause,[],[f1245,f1421,f1271]) ).
fof(f1598,definition,
( spl81_104
<=> sQ80_eqProxy(e3,op(e1,e4)) ),
introduced(definition,[new_symbols(definition,[spl81_104])],[avatar_definition]) ).
fof(f1599,plain,
( ~ sQ80_eqProxy(e3,op(e1,e4))
| spl81_104 ),
inference(avatar_component_clause,[],[f1598]) ).
fof(f1600,plain,
( ~ spl81_3
| ~ spl81_104 ),
inference(avatar_split_clause,[],[f1241,f1598,f1274]) ).
fof(f1616,definition,
( spl81_108
<=> sQ80_eqProxy(e3,op(e4,e1)) ),
introduced(definition,[new_symbols(definition,[spl81_108])],[avatar_definition]) ).
fof(f1617,plain,
( ~ sQ80_eqProxy(e3,op(e4,e1))
| spl81_108 ),
inference(avatar_component_clause,[],[f1616]) ).
fof(f1618,plain,
( ~ spl81_4
| ~ spl81_108 ),
inference(avatar_split_clause,[],[f1236,f1616,f1277]) ).
fof(f1625,definition,
( spl81_110
<=> sQ80_eqProxy(e2,op(e4,e4)) ),
introduced(definition,[new_symbols(definition,[spl81_110])],[avatar_definition]) ).
fof(f1626,plain,
( ~ sQ80_eqProxy(e2,op(e4,e4))
| spl81_110 ),
inference(avatar_component_clause,[],[f1625]) ).
fof(f1627,plain,
( ~ spl81_5
| ~ spl81_110 ),
inference(avatar_split_clause,[],[f1234,f1625,f1280]) ).
fof(f1645,plain,
( ~ spl81_6
| ~ spl81_110 ),
inference(avatar_split_clause,[],[f1229,f1625,f1283]) ).
fof(f1672,definition,
( spl81_121
<=> sQ80_eqProxy(e1,op(e2,e4)) ),
introduced(definition,[new_symbols(definition,[spl81_121])],[avatar_definition]) ).
fof(f1673,plain,
( ~ sQ80_eqProxy(e1,op(e2,e4))
| spl81_121 ),
inference(avatar_component_clause,[],[f1672]) ).
fof(f1674,plain,
( ~ spl81_7
| ~ spl81_121 ),
inference(avatar_split_clause,[],[f1222,f1672,f1286]) ).
fof(f1690,definition,
( spl81_125
<=> sQ80_eqProxy(e1,op(e4,e2)) ),
introduced(definition,[new_symbols(definition,[spl81_125])],[avatar_definition]) ).
fof(f1691,plain,
( ~ sQ80_eqProxy(e1,op(e4,e2))
| spl81_125 ),
inference(avatar_component_clause,[],[f1690]) ).
fof(f1692,plain,
( ~ spl81_8
| ~ spl81_125 ),
inference(avatar_split_clause,[],[f1217,f1690,f1289]) ).
fof(f1704,definition,
( spl81_128
<=> sQ80_eqProxy(op(e3,e4),unit) ),
introduced(definition,[new_symbols(definition,[spl81_128])],[avatar_definition]) ).
fof(f1705,plain,
( ~ sQ80_eqProxy(op(e3,e4),unit)
| spl81_128 ),
inference(avatar_component_clause,[],[f1704]) ).
fof(f1706,plain,
( ~ spl81_9
| ~ spl81_128 ),
inference(avatar_split_clause,[],[f1213,f1704,f1292]) ).
fof(f1722,definition,
( spl81_132
<=> sQ80_eqProxy(op(e4,e3),unit) ),
introduced(definition,[new_symbols(definition,[spl81_132])],[avatar_definition]) ).
fof(f1723,plain,
( ~ sQ80_eqProxy(op(e4,e3),unit)
| spl81_132 ),
inference(avatar_component_clause,[],[f1722]) ).
fof(f1724,plain,
( ~ spl81_10
| ~ spl81_132 ),
inference(avatar_split_clause,[],[f1208,f1722,f1295]) ).
fof(f1744,definition,
( spl81_137
<=> sQ80_eqProxy(e4,op(e2,e3)) ),
introduced(definition,[new_symbols(definition,[spl81_137])],[avatar_definition]) ).
fof(f1745,plain,
( ~ sQ80_eqProxy(e4,op(e2,e3))
| spl81_137 ),
inference(avatar_component_clause,[],[f1744]) ).
fof(f1746,plain,
( ~ spl81_11
| ~ spl81_137 ),
inference(avatar_split_clause,[],[f1202,f1744,f1298]) ).
fof(f1759,definition,
( spl81_140
<=> sQ80_eqProxy(e4,op(e3,e2)) ),
introduced(definition,[new_symbols(definition,[spl81_140])],[avatar_definition]) ).
fof(f1760,plain,
( ~ sQ80_eqProxy(e4,op(e3,e2))
| spl81_140 ),
inference(avatar_component_clause,[],[f1759]) ).
fof(f1761,plain,
( ~ spl81_12
| ~ spl81_140 ),
inference(avatar_split_clause,[],[f1197,f1759,f1301]) ).
fof(f1784,plain,
( ~ spl81_13
| ~ spl81_55 ),
inference(avatar_split_clause,[],[f1190,f1430,f1304]) ).
fof(f1796,plain,
( ~ spl81_14
| ~ spl81_54 ),
inference(avatar_split_clause,[],[f1185,f1427,f1307]) ).
fof(f1808,definition,
( spl81_150
<=> sQ80_eqProxy(e2,op(e1,e3)) ),
introduced(definition,[new_symbols(definition,[spl81_150])],[avatar_definition]) ).
fof(f1809,plain,
( ~ sQ80_eqProxy(e2,op(e1,e3))
| spl81_150 ),
inference(avatar_component_clause,[],[f1808]) ).
fof(f1810,plain,
( ~ spl81_15
| ~ spl81_150 ),
inference(avatar_split_clause,[],[f1181,f1808,f1310]) ).
fof(f1823,definition,
( spl81_153
<=> sQ80_eqProxy(e2,op(e3,e1)) ),
introduced(definition,[new_symbols(definition,[spl81_153])],[avatar_definition]) ).
fof(f1824,plain,
( ~ sQ80_eqProxy(e2,op(e3,e1))
| spl81_153 ),
inference(avatar_component_clause,[],[f1823]) ).
fof(f1825,plain,
( ~ spl81_16
| ~ spl81_153 ),
inference(avatar_split_clause,[],[f1176,f1823,f1313]) ).
fof(f1833,definition,
( spl81_155
<=> sQ80_eqProxy(e1,op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl81_155])],[avatar_definition]) ).
fof(f1834,plain,
( ~ sQ80_eqProxy(e1,op(e3,e3))
| spl81_155 ),
inference(avatar_component_clause,[],[f1833]) ).
fof(f1835,plain,
( ~ spl81_17
| ~ spl81_155 ),
inference(avatar_split_clause,[],[f1173,f1833,f1316]) ).
fof(f1850,plain,
( ~ spl81_18
| ~ spl81_155 ),
inference(avatar_split_clause,[],[f1168,f1833,f1319]) ).
fof(f1864,plain,
( ~ spl81_19
| ~ spl81_132 ),
inference(avatar_split_clause,[],[f1164,f1722,f1322]) ).
fof(f1879,plain,
( ~ spl81_20
| ~ spl81_128 ),
inference(avatar_split_clause,[],[f1159,f1704,f1325]) ).
fof(f1895,plain,
( ~ spl81_21
| ~ spl81_140 ),
inference(avatar_split_clause,[],[f1153,f1759,f1328]) ).
fof(f1910,plain,
( ~ spl81_22
| ~ spl81_137 ),
inference(avatar_split_clause,[],[f1148,f1744,f1331]) ).
fof(f1924,definition,
( spl81_173
<=> sQ80_eqProxy(e3,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl81_173])],[avatar_definition]) ).
fof(f1925,plain,
( ~ sQ80_eqProxy(e3,op(e2,e2))
| spl81_173 ),
inference(avatar_component_clause,[],[f1924]) ).
fof(f1926,plain,
( ~ spl81_23
| ~ spl81_173 ),
inference(avatar_split_clause,[],[f1142,f1924,f1334]) ).
fof(f1938,plain,
( ~ spl81_24
| ~ spl81_173 ),
inference(avatar_split_clause,[],[f1137,f1924,f1337]) ).
fof(f1958,plain,
( ~ spl81_25
| ~ spl81_57 ),
inference(avatar_split_clause,[],[f1130,f1436,f1340]) ).
fof(f1967,plain,
( ~ spl81_26
| ~ spl81_56 ),
inference(avatar_split_clause,[],[f1125,f1433,f1343]) ).
fof(f1969,plain,
( ~ spl81_27
| ~ spl81_125 ),
inference(avatar_split_clause,[],[f1124,f1690,f1346]) ).
fof(f1984,plain,
( ~ spl81_28
| ~ spl81_121 ),
inference(avatar_split_clause,[],[f1119,f1672,f1349]) ).
fof(f2000,definition,
( spl81_186
<=> sQ80_eqProxy(op(e1,e2),unit) ),
introduced(definition,[new_symbols(definition,[spl81_186])],[avatar_definition]) ).
fof(f2001,plain,
( ~ sQ80_eqProxy(op(e1,e2),unit)
| spl81_186 ),
inference(avatar_component_clause,[],[f2000]) ).
fof(f2002,plain,
( ~ spl81_29
| ~ spl81_186 ),
inference(avatar_split_clause,[],[f1111,f2000,f1352]) ).
fof(f2012,definition,
( spl81_188
<=> sQ80_eqProxy(op(e2,e1),unit) ),
introduced(definition,[new_symbols(definition,[spl81_188])],[avatar_definition]) ).
fof(f2013,plain,
( ~ sQ80_eqProxy(op(e2,e1),unit)
| spl81_188 ),
inference(avatar_component_clause,[],[f2012]) ).
fof(f2014,plain,
( ~ spl81_30
| ~ spl81_188 ),
inference(avatar_split_clause,[],[f1106,f2012,f1355]) ).
fof(f2024,definition,
( spl81_190
<=> sQ80_eqProxy(e4,op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl81_190])],[avatar_definition]) ).
fof(f2025,plain,
( ~ sQ80_eqProxy(e4,op(e1,e1))
| spl81_190 ),
inference(avatar_component_clause,[],[f2024]) ).
fof(f2026,plain,
( ~ spl81_31
| ~ spl81_190 ),
inference(avatar_split_clause,[],[f1101,f2024,f1358]) ).
fof(f2035,plain,
( ~ spl81_32
| ~ spl81_190 ),
inference(avatar_split_clause,[],[f1096,f2024,f1361]) ).
fof(f2041,plain,
( ~ spl81_33
| ~ spl81_108 ),
inference(avatar_split_clause,[],[f1094,f1616,f1364]) ).
fof(f2053,plain,
( ~ spl81_34
| ~ spl81_104 ),
inference(avatar_split_clause,[],[f1089,f1598,f1367]) ).
fof(f2063,plain,
( ~ spl81_35
| ~ spl81_153 ),
inference(avatar_split_clause,[],[f1083,f1823,f1370]) ).
fof(f2075,plain,
( ~ spl81_36
| ~ spl81_150 ),
inference(avatar_split_clause,[],[f1078,f1808,f1373]) ).
fof(f2090,plain,
( ~ spl81_37
| ~ spl81_59 ),
inference(avatar_split_clause,[],[f1070,f1442,f1376]) ).
fof(f2096,plain,
( ~ spl81_38
| ~ spl81_58 ),
inference(avatar_split_clause,[],[f1065,f1439,f1379]) ).
fof(f2100,plain,
( ~ spl81_39
| ~ spl81_188 ),
inference(avatar_split_clause,[],[f1062,f2012,f1382]) ).
fof(f2109,plain,
( ~ spl81_40
| ~ spl81_186 ),
inference(avatar_split_clause,[],[f1057,f2000,f1385]) ).
fof(f2116,plain,
( ~ spl81_41
| ~ spl81_52 ),
inference(avatar_split_clause,[],[f1054,f1421,f1388]) ).
fof(f2125,plain,
( ~ spl81_42
| ~ spl81_53 ),
inference(avatar_split_clause,[],[f1049,f1424,f1391]) ).
fof(f2132,plain,
( ~ spl81_43
| ~ spl81_54 ),
inference(avatar_split_clause,[],[f1043,f1427,f1394]) ).
fof(f2141,plain,
( ~ spl81_44
| ~ spl81_55 ),
inference(avatar_split_clause,[],[f1038,f1430,f1397]) ).
fof(f2148,plain,
( ~ spl81_45
| ~ spl81_56 ),
inference(avatar_split_clause,[],[f1032,f1433,f1400]) ).
fof(f2157,plain,
( ~ spl81_46
| ~ spl81_57 ),
inference(avatar_split_clause,[],[f1027,f1436,f1403]) ).
fof(f2164,plain,
( ~ spl81_47
| ~ spl81_58 ),
inference(avatar_split_clause,[],[f1021,f1439,f1406]) ).
fof(f2173,plain,
( ~ spl81_48
| ~ spl81_59 ),
inference(avatar_split_clause,[],[f1016,f1442,f1409]) ).
fof(f2180,plain,
( ~ spl81_49
| ~ spl81_60 ),
inference(avatar_split_clause,[],[f1010,f1445,f1412]) ).
fof(f2186,plain,
( ~ spl81_50
| ~ spl81_60 ),
inference(avatar_split_clause,[],[f1005,f1445,f1415]) ).
fof(f2205,definition,
( spl81_210
<=> sQ80_eqProxy(unit,unit) ),
introduced(definition,[new_symbols(definition,[spl81_210])],[avatar_definition]) ).
fof(f2206,plain,
( ~ sQ80_eqProxy(unit,unit)
| spl81_210 ),
inference(avatar_component_clause,[],[f2205]) ).
fof(f2207,plain,
( ~ spl81_51
| ~ spl81_210 ),
inference(avatar_split_clause,[],[f1000,f2205,f1418]) ).
fof(f2211,plain,
( ~ spl81_61
| ~ spl81_110 ),
inference(avatar_split_clause,[],[f997,f1625,f1448]) ).
fof(f2219,plain,
( ~ spl81_62
| ~ spl81_132 ),
inference(avatar_split_clause,[],[f990,f1722,f1451]) ).
fof(f2224,plain,
( ~ spl81_63
| ~ spl81_125 ),
inference(avatar_split_clause,[],[f986,f1690,f1454]) ).
fof(f2228,plain,
( ~ spl81_64
| ~ spl81_108 ),
inference(avatar_split_clause,[],[f983,f1616,f1457]) ).
fof(f2233,plain,
( ~ spl81_65
| ~ spl81_52 ),
inference(avatar_split_clause,[],[f979,f1421,f1460]) ).
fof(f2243,plain,
( ~ spl81_66
| ~ spl81_128 ),
inference(avatar_split_clause,[],[f970,f1704,f1463]) ).
fof(f2248,plain,
( ~ spl81_67
| ~ spl81_155 ),
inference(avatar_split_clause,[],[f966,f1833,f1466]) ).
fof(f2251,plain,
( ~ spl81_68
| ~ spl81_140 ),
inference(avatar_split_clause,[],[f964,f1759,f1469]) ).
fof(f2259,plain,
( ~ spl81_69
| ~ spl81_153 ),
inference(avatar_split_clause,[],[f957,f1823,f1472]) ).
fof(f2264,plain,
( ~ spl81_70
| ~ spl81_54 ),
inference(avatar_split_clause,[],[f953,f1427,f1475]) ).
fof(f2272,plain,
( ~ spl81_71
| ~ spl81_121 ),
inference(avatar_split_clause,[],[f946,f1672,f1478]) ).
fof(f2275,plain,
( ~ spl81_72
| ~ spl81_137 ),
inference(avatar_split_clause,[],[f944,f1744,f1481]) ).
fof(f2282,plain,
( ~ spl81_73
| ~ spl81_173 ),
inference(avatar_split_clause,[],[f938,f1924,f1484]) ).
fof(f2291,plain,
( ~ spl81_74
| ~ spl81_188 ),
inference(avatar_split_clause,[],[f930,f2012,f1487]) ).
fof(f2295,plain,
( ~ spl81_75
| ~ spl81_56 ),
inference(avatar_split_clause,[],[f927,f1433,f1490]) ).
fof(f2300,plain,
( ~ spl81_76
| ~ spl81_104 ),
inference(avatar_split_clause,[],[f923,f1598,f1493]) ).
fof(f2307,plain,
( ~ spl81_77
| ~ spl81_150 ),
inference(avatar_split_clause,[],[f917,f1808,f1496]) ).
fof(f2315,plain,
( ~ spl81_78
| ~ spl81_186 ),
inference(avatar_split_clause,[],[f910,f2000,f1499]) ).
fof(f2317,plain,
( ~ spl81_79
| ~ spl81_190 ),
inference(avatar_split_clause,[],[f909,f2024,f1502]) ).
fof(f2326,plain,
( ~ spl81_80
| ~ spl81_58 ),
inference(avatar_split_clause,[],[f901,f1439,f1505]) ).
fof(f2329,plain,
( ~ spl81_81
| ~ spl81_53 ),
inference(avatar_split_clause,[],[f899,f1424,f1508]) ).
fof(f2336,plain,
( ~ spl81_82
| ~ spl81_55 ),
inference(avatar_split_clause,[],[f893,f1430,f1511]) ).
fof(f2343,plain,
( ~ spl81_83
| ~ spl81_57 ),
inference(avatar_split_clause,[],[f887,f1436,f1514]) ).
fof(f2350,plain,
( ~ spl81_84
| ~ spl81_59 ),
inference(avatar_split_clause,[],[f881,f1442,f1517]) ).
fof(f2357,plain,
( ~ spl81_85
| ~ spl81_60 ),
inference(avatar_split_clause,[],[f875,f1445,f1520]) ).
fof(f2362,plain,
( ~ spl81_86
| ~ spl81_190 ),
inference(avatar_split_clause,[],[f871,f2024,f1523]) ).
fof(f2367,plain,
( ~ spl81_87
| ~ spl81_173 ),
inference(avatar_split_clause,[],[f867,f1924,f1526]) ).
fof(f2371,plain,
( ~ spl81_88
| ~ spl81_110 ),
inference(avatar_split_clause,[],[f864,f1625,f1529]) ).
fof(f2378,plain,
( ~ spl81_89
| ~ spl81_155 ),
inference(avatar_split_clause,[],[f858,f1833,f1532]) ).
fof(f2386,plain,
( $false
| spl81_52 ),
inference(resolution,[],[f850,f1422]) ).
fof(f2387,plain,
spl81_52,
inference(avatar_contradiction_clause,[],[f2386]) ).
fof(f2388,plain,
( $false
| spl81_53 ),
inference(resolution,[],[f1425,f834]) ).
fof(f2389,plain,
spl81_53,
inference(avatar_contradiction_clause,[],[f2388]) ).
fof(f2390,plain,
( $false
| spl81_54 ),
inference(resolution,[],[f1428,f845]) ).
fof(f2391,plain,
spl81_54,
inference(avatar_contradiction_clause,[],[f2390]) ).
fof(f2392,plain,
( $false
| spl81_55 ),
inference(resolution,[],[f1431,f833]) ).
fof(f2393,plain,
spl81_55,
inference(avatar_contradiction_clause,[],[f2392]) ).
fof(f2394,plain,
( $false
| spl81_56 ),
inference(resolution,[],[f1434,f840]) ).
fof(f2395,plain,
spl81_56,
inference(avatar_contradiction_clause,[],[f2394]) ).
fof(f2396,plain,
( $false
| spl81_57 ),
inference(resolution,[],[f1437,f832]) ).
fof(f2397,plain,
spl81_57,
inference(avatar_contradiction_clause,[],[f2396]) ).
fof(f2398,plain,
( $false
| spl81_58 ),
inference(resolution,[],[f1440,f835]) ).
fof(f2399,plain,
spl81_58,
inference(avatar_contradiction_clause,[],[f2398]) ).
fof(f2400,plain,
( $false
| spl81_59 ),
inference(resolution,[],[f1443,f831]) ).
fof(f2401,plain,
spl81_59,
inference(avatar_contradiction_clause,[],[f2400]) ).
fof(f2402,plain,
( $false
| spl81_60 ),
inference(resolution,[],[f1446,f830]) ).
fof(f2403,plain,
spl81_60,
inference(avatar_contradiction_clause,[],[f2402]) ).
fof(f2404,plain,
( $false
| spl81_110 ),
inference(resolution,[],[f854,f1626]) ).
fof(f2405,plain,
spl81_110,
inference(avatar_contradiction_clause,[],[f2404]) ).
fof(f2406,plain,
( $false
| spl81_121 ),
inference(resolution,[],[f1673,f844]) ).
fof(f2407,plain,
spl81_121,
inference(avatar_contradiction_clause,[],[f2406]) ).
fof(f2431,plain,
( $false
| spl81_125 ),
inference(resolution,[],[f1691,f852]) ).
fof(f2433,plain,
spl81_125,
inference(avatar_contradiction_clause,[],[f2431]) ).
fof(f2439,plain,
( $false
| spl81_128 ),
inference(resolution,[],[f1705,f849]) ).
fof(f2441,plain,
spl81_128,
inference(avatar_contradiction_clause,[],[f2439]) ).
fof(f2445,plain,
( $false
| spl81_132 ),
inference(resolution,[],[f1723,f853]) ).
fof(f2447,plain,
spl81_132,
inference(avatar_contradiction_clause,[],[f2445]) ).
fof(f2451,plain,
( $false
| spl81_108 ),
inference(resolution,[],[f1617,f851]) ).
fof(f2453,plain,
spl81_108,
inference(avatar_contradiction_clause,[],[f2451]) ).
fof(f2461,plain,
( $false
| spl81_137 ),
inference(resolution,[],[f1745,f843]) ).
fof(f2463,plain,
spl81_137,
inference(avatar_contradiction_clause,[],[f2461]) ).
fof(f2467,plain,
( $false
| spl81_140 ),
inference(resolution,[],[f1760,f847]) ).
fof(f2469,plain,
spl81_140,
inference(avatar_contradiction_clause,[],[f2467]) ).
fof(f2475,plain,
( $false
| spl81_150 ),
inference(resolution,[],[f1809,f838]) ).
fof(f2477,plain,
spl81_150,
inference(avatar_contradiction_clause,[],[f2475]) ).
fof(f2481,plain,
( $false
| spl81_153 ),
inference(resolution,[],[f1824,f846]) ).
fof(f2483,plain,
spl81_153,
inference(avatar_contradiction_clause,[],[f2481]) ).
fof(f2485,plain,
( $false
| spl81_155 ),
inference(resolution,[],[f1834,f848]) ).
fof(f2487,plain,
spl81_155,
inference(avatar_contradiction_clause,[],[f2485]) ).
fof(f2493,plain,
( $false
| spl81_173 ),
inference(resolution,[],[f1925,f842]) ).
fof(f2495,plain,
spl81_173,
inference(avatar_contradiction_clause,[],[f2493]) ).
fof(f2501,plain,
( $false
| spl81_186 ),
inference(resolution,[],[f2001,f837]) ).
fof(f2503,plain,
spl81_186,
inference(avatar_contradiction_clause,[],[f2501]) ).
fof(f2507,plain,
( $false
| spl81_188 ),
inference(resolution,[],[f2013,f841]) ).
fof(f2509,plain,
spl81_188,
inference(avatar_contradiction_clause,[],[f2507]) ).
fof(f2513,plain,
( $false
| spl81_190 ),
inference(resolution,[],[f2025,f836]) ).
fof(f2515,plain,
spl81_190,
inference(avatar_contradiction_clause,[],[f2513]) ).
fof(f2516,plain,
( $false
| spl81_104 ),
inference(resolution,[],[f1599,f839]) ).
fof(f2518,plain,
spl81_104,
inference(avatar_contradiction_clause,[],[f2516]) ).
fof(f2519,plain,
( $false
| spl81_210 ),
inference(resolution,[],[f2206,f1260]) ).
fof(f2521,plain,
spl81_210,
inference(avatar_contradiction_clause,[],[f2519]) ).
cnf(s5,plain,
( spl81_1
| spl81_2
| spl81_3
| spl81_4
| spl81_5
| spl81_6
| spl81_7
| spl81_8
| spl81_9
| spl81_10
| spl81_11
| spl81_12
| spl81_13
| spl81_14
| spl81_15
| spl81_16
| spl81_17
| spl81_18
| spl81_19
| spl81_20
| spl81_21
| spl81_22
| spl81_23
| spl81_24
| spl81_25
| spl81_26
| spl81_27
| spl81_28
| spl81_29
| spl81_30
| spl81_31
| spl81_32
| spl81_33
| spl81_34
| spl81_35
| spl81_36
| spl81_37
| spl81_38
| spl81_39
| spl81_40
| spl81_41
| spl81_42
| spl81_43
| spl81_44
| spl81_45
| spl81_46
| spl81_47
| spl81_48
| spl81_49
| spl81_50
| spl81_51
| ~ spl81_52
| ~ spl81_53
| ~ spl81_54
| ~ spl81_55
| ~ spl81_56
| ~ spl81_57
| ~ spl81_58
| ~ spl81_59
| ~ spl81_60
| spl81_61
| spl81_62
| spl81_63
| spl81_64
| spl81_65
| spl81_66
| spl81_67
| spl81_68
| spl81_69
| spl81_70
| spl81_71
| spl81_72
| spl81_73
| spl81_74
| spl81_75
| spl81_76
| spl81_77
| spl81_78
| spl81_79
| spl81_80
| spl81_81
| spl81_82
| spl81_83
| spl81_84
| spl81_85
| spl81_86
| spl81_87
| spl81_88
| spl81_89 ),
inference(sat_conversion,[],[f1550]) ).
cnf(s10,plain,
( ~ spl81_1
| ~ spl81_53 ),
inference(sat_conversion,[],[f1568]) ).
cnf(s15,plain,
( ~ spl81_2
| ~ spl81_52 ),
inference(sat_conversion,[],[f1583]) ).
cnf(s19,plain,
( ~ spl81_3
| ~ spl81_104 ),
inference(sat_conversion,[],[f1600]) ).
cnf(s24,plain,
( ~ spl81_4
| ~ spl81_108 ),
inference(sat_conversion,[],[f1618]) ).
cnf(s26,plain,
( ~ spl81_5
| ~ spl81_110 ),
inference(sat_conversion,[],[f1627]) ).
cnf(s31,plain,
( ~ spl81_6
| ~ spl81_110 ),
inference(sat_conversion,[],[f1645]) ).
cnf(s38,plain,
( ~ spl81_7
| ~ spl81_121 ),
inference(sat_conversion,[],[f1674]) ).
cnf(s43,plain,
( ~ spl81_8
| ~ spl81_125 ),
inference(sat_conversion,[],[f1692]) ).
cnf(s47,plain,
( ~ spl81_9
| ~ spl81_128 ),
inference(sat_conversion,[],[f1706]) ).
cnf(s52,plain,
( ~ spl81_10
| ~ spl81_132 ),
inference(sat_conversion,[],[f1724]) ).
cnf(s58,plain,
( ~ spl81_11
| ~ spl81_137 ),
inference(sat_conversion,[],[f1746]) ).
cnf(s63,plain,
( ~ spl81_12
| ~ spl81_140 ),
inference(sat_conversion,[],[f1761]) ).
cnf(s70,plain,
( ~ spl81_13
| ~ spl81_55 ),
inference(sat_conversion,[],[f1784]) ).
cnf(s75,plain,
( ~ spl81_14
| ~ spl81_54 ),
inference(sat_conversion,[],[f1796]) ).
cnf(s79,plain,
( ~ spl81_15
| ~ spl81_150 ),
inference(sat_conversion,[],[f1810]) ).
cnf(s84,plain,
( ~ spl81_16
| ~ spl81_153 ),
inference(sat_conversion,[],[f1825]) ).
cnf(s87,plain,
( ~ spl81_17
| ~ spl81_155 ),
inference(sat_conversion,[],[f1835]) ).
cnf(s92,plain,
( ~ spl81_18
| ~ spl81_155 ),
inference(sat_conversion,[],[f1850]) ).
cnf(s96,plain,
( ~ spl81_19
| ~ spl81_132 ),
inference(sat_conversion,[],[f1864]) ).
cnf(s101,plain,
( ~ spl81_20
| ~ spl81_128 ),
inference(sat_conversion,[],[f1879]) ).
cnf(s107,plain,
( ~ spl81_21
| ~ spl81_140 ),
inference(sat_conversion,[],[f1895]) ).
cnf(s112,plain,
( ~ spl81_22
| ~ spl81_137 ),
inference(sat_conversion,[],[f1910]) ).
cnf(s118,plain,
( ~ spl81_23
| ~ spl81_173 ),
inference(sat_conversion,[],[f1926]) ).
cnf(s123,plain,
( ~ spl81_24
| ~ spl81_173 ),
inference(sat_conversion,[],[f1938]) ).
cnf(s130,plain,
( ~ spl81_25
| ~ spl81_57 ),
inference(sat_conversion,[],[f1958]) ).
cnf(s135,plain,
( ~ spl81_26
| ~ spl81_56 ),
inference(sat_conversion,[],[f1967]) ).
cnf(s136,plain,
( ~ spl81_27
| ~ spl81_125 ),
inference(sat_conversion,[],[f1969]) ).
cnf(s141,plain,
( ~ spl81_28
| ~ spl81_121 ),
inference(sat_conversion,[],[f1984]) ).
cnf(s149,plain,
( ~ spl81_29
| ~ spl81_186 ),
inference(sat_conversion,[],[f2002]) ).
cnf(s154,plain,
( ~ spl81_30
| ~ spl81_188 ),
inference(sat_conversion,[],[f2014]) ).
cnf(s159,plain,
( ~ spl81_31
| ~ spl81_190 ),
inference(sat_conversion,[],[f2026]) ).
cnf(s164,plain,
( ~ spl81_32
| ~ spl81_190 ),
inference(sat_conversion,[],[f2035]) ).
cnf(s166,plain,
( ~ spl81_33
| ~ spl81_108 ),
inference(sat_conversion,[],[f2041]) ).
cnf(s171,plain,
( ~ spl81_34
| ~ spl81_104 ),
inference(sat_conversion,[],[f2053]) ).
cnf(s177,plain,
( ~ spl81_35
| ~ spl81_153 ),
inference(sat_conversion,[],[f2063]) ).
cnf(s182,plain,
( ~ spl81_36
| ~ spl81_150 ),
inference(sat_conversion,[],[f2075]) ).
cnf(s190,plain,
( ~ spl81_37
| ~ spl81_59 ),
inference(sat_conversion,[],[f2090]) ).
cnf(s195,plain,
( ~ spl81_38
| ~ spl81_58 ),
inference(sat_conversion,[],[f2096]) ).
cnf(s198,plain,
( ~ spl81_39
| ~ spl81_188 ),
inference(sat_conversion,[],[f2100]) ).
cnf(s203,plain,
( ~ spl81_40
| ~ spl81_186 ),
inference(sat_conversion,[],[f2109]) ).
cnf(s206,plain,
( ~ spl81_41
| ~ spl81_52 ),
inference(sat_conversion,[],[f2116]) ).
cnf(s211,plain,
( ~ spl81_42
| ~ spl81_53 ),
inference(sat_conversion,[],[f2125]) ).
cnf(s217,plain,
( ~ spl81_43
| ~ spl81_54 ),
inference(sat_conversion,[],[f2132]) ).
cnf(s222,plain,
( ~ spl81_44
| ~ spl81_55 ),
inference(sat_conversion,[],[f2141]) ).
cnf(s228,plain,
( ~ spl81_45
| ~ spl81_56 ),
inference(sat_conversion,[],[f2148]) ).
cnf(s233,plain,
( ~ spl81_46
| ~ spl81_57 ),
inference(sat_conversion,[],[f2157]) ).
cnf(s239,plain,
( ~ spl81_47
| ~ spl81_58 ),
inference(sat_conversion,[],[f2164]) ).
cnf(s244,plain,
( ~ spl81_48
| ~ spl81_59 ),
inference(sat_conversion,[],[f2173]) ).
cnf(s250,plain,
( ~ spl81_49
| ~ spl81_60 ),
inference(sat_conversion,[],[f2180]) ).
cnf(s255,plain,
( ~ spl81_50
| ~ spl81_60 ),
inference(sat_conversion,[],[f2186]) ).
cnf(s260,plain,
( ~ spl81_51
| ~ spl81_210 ),
inference(sat_conversion,[],[f2207]) ).
cnf(s263,plain,
( ~ spl81_61
| ~ spl81_110 ),
inference(sat_conversion,[],[f2211]) ).
cnf(s270,plain,
( ~ spl81_62
| ~ spl81_132 ),
inference(sat_conversion,[],[f2219]) ).
cnf(s274,plain,
( ~ spl81_63
| ~ spl81_125 ),
inference(sat_conversion,[],[f2224]) ).
cnf(s277,plain,
( ~ spl81_64
| ~ spl81_108 ),
inference(sat_conversion,[],[f2228]) ).
cnf(s281,plain,
( ~ spl81_52
| ~ spl81_65 ),
inference(sat_conversion,[],[f2233]) ).
cnf(s290,plain,
( ~ spl81_66
| ~ spl81_128 ),
inference(sat_conversion,[],[f2243]) ).
cnf(s294,plain,
( ~ spl81_67
| ~ spl81_155 ),
inference(sat_conversion,[],[f2248]) ).
cnf(s296,plain,
( ~ spl81_68
| ~ spl81_140 ),
inference(sat_conversion,[],[f2251]) ).
cnf(s303,plain,
( ~ spl81_69
| ~ spl81_153 ),
inference(sat_conversion,[],[f2259]) ).
cnf(s307,plain,
( ~ spl81_54
| ~ spl81_70 ),
inference(sat_conversion,[],[f2264]) ).
cnf(s314,plain,
( ~ spl81_71
| ~ spl81_121 ),
inference(sat_conversion,[],[f2272]) ).
cnf(s316,plain,
( ~ spl81_72
| ~ spl81_137 ),
inference(sat_conversion,[],[f2275]) ).
cnf(s322,plain,
( ~ spl81_73
| ~ spl81_173 ),
inference(sat_conversion,[],[f2282]) ).
cnf(s330,plain,
( ~ spl81_74
| ~ spl81_188 ),
inference(sat_conversion,[],[f2291]) ).
cnf(s333,plain,
( ~ spl81_56
| ~ spl81_75 ),
inference(sat_conversion,[],[f2295]) ).
cnf(s337,plain,
( ~ spl81_76
| ~ spl81_104 ),
inference(sat_conversion,[],[f2300]) ).
cnf(s343,plain,
( ~ spl81_77
| ~ spl81_150 ),
inference(sat_conversion,[],[f2307]) ).
cnf(s350,plain,
( ~ spl81_78
| ~ spl81_186 ),
inference(sat_conversion,[],[f2315]) ).
cnf(s351,plain,
( ~ spl81_79
| ~ spl81_190 ),
inference(sat_conversion,[],[f2317]) ).
cnf(s359,plain,
( ~ spl81_58
| ~ spl81_80 ),
inference(sat_conversion,[],[f2326]) ).
cnf(s361,plain,
( ~ spl81_53
| ~ spl81_81 ),
inference(sat_conversion,[],[f2329]) ).
cnf(s367,plain,
( ~ spl81_55
| ~ spl81_82 ),
inference(sat_conversion,[],[f2336]) ).
cnf(s373,plain,
( ~ spl81_57
| ~ spl81_83 ),
inference(sat_conversion,[],[f2343]) ).
cnf(s379,plain,
( ~ spl81_59
| ~ spl81_84 ),
inference(sat_conversion,[],[f2350]) ).
cnf(s385,plain,
( ~ spl81_60
| ~ spl81_85 ),
inference(sat_conversion,[],[f2357]) ).
cnf(s389,plain,
( ~ spl81_86
| ~ spl81_190 ),
inference(sat_conversion,[],[f2362]) ).
cnf(s393,plain,
( ~ spl81_87
| ~ spl81_173 ),
inference(sat_conversion,[],[f2367]) ).
cnf(s396,plain,
( ~ spl81_88
| ~ spl81_110 ),
inference(sat_conversion,[],[f2371]) ).
cnf(s402,plain,
( ~ spl81_89
| ~ spl81_155 ),
inference(sat_conversion,[],[f2378]) ).
cnf(s410,plain,
spl81_52,
inference(sat_conversion,[],[f2387]) ).
cnf(s411,plain,
spl81_53,
inference(sat_conversion,[],[f2389]) ).
cnf(s412,plain,
spl81_54,
inference(sat_conversion,[],[f2391]) ).
cnf(s413,plain,
spl81_55,
inference(sat_conversion,[],[f2393]) ).
cnf(s414,plain,
spl81_56,
inference(sat_conversion,[],[f2395]) ).
cnf(s415,plain,
spl81_57,
inference(sat_conversion,[],[f2397]) ).
cnf(s416,plain,
spl81_58,
inference(sat_conversion,[],[f2399]) ).
cnf(s417,plain,
spl81_59,
inference(sat_conversion,[],[f2401]) ).
cnf(s418,plain,
spl81_60,
inference(sat_conversion,[],[f2403]) ).
cnf(s419,plain,
spl81_110,
inference(sat_conversion,[],[f2405]) ).
cnf(s420,plain,
spl81_121,
inference(sat_conversion,[],[f2407]) ).
cnf(s421,plain,
spl81_125,
inference(sat_conversion,[],[f2433]) ).
cnf(s422,plain,
spl81_128,
inference(sat_conversion,[],[f2441]) ).
cnf(s423,plain,
spl81_132,
inference(sat_conversion,[],[f2447]) ).
cnf(s424,plain,
spl81_108,
inference(sat_conversion,[],[f2453]) ).
cnf(s425,plain,
spl81_137,
inference(sat_conversion,[],[f2463]) ).
cnf(s426,plain,
spl81_140,
inference(sat_conversion,[],[f2469]) ).
cnf(s427,plain,
spl81_150,
inference(sat_conversion,[],[f2477]) ).
cnf(s428,plain,
spl81_153,
inference(sat_conversion,[],[f2483]) ).
cnf(s429,plain,
spl81_155,
inference(sat_conversion,[],[f2487]) ).
cnf(s430,plain,
spl81_173,
inference(sat_conversion,[],[f2495]) ).
cnf(s431,plain,
spl81_186,
inference(sat_conversion,[],[f2503]) ).
cnf(s432,plain,
spl81_188,
inference(sat_conversion,[],[f2509]) ).
cnf(s433,plain,
spl81_190,
inference(sat_conversion,[],[f2515]) ).
cnf(s434,plain,
spl81_104,
inference(sat_conversion,[],[f2518]) ).
cnf(s435,plain,
spl81_210,
inference(sat_conversion,[],[f2521]) ).
cnf(s436,plain,
~ spl81_89,
inference(rat,[],[s402,s429]) ).
cnf(s437,plain,
~ spl81_88,
inference(rat,[],[s396,s419]) ).
cnf(s438,plain,
~ spl81_87,
inference(rat,[],[s393,s430]) ).
cnf(s439,plain,
~ spl81_86,
inference(rat,[],[s389,s433]) ).
cnf(s440,plain,
~ spl81_85,
inference(rat,[],[s385,s418]) ).
cnf(s441,plain,
~ spl81_84,
inference(rat,[],[s379,s417]) ).
cnf(s442,plain,
~ spl81_83,
inference(rat,[],[s373,s415]) ).
cnf(s443,plain,
~ spl81_82,
inference(rat,[],[s367,s413]) ).
cnf(s444,plain,
~ spl81_81,
inference(rat,[],[s361,s411]) ).
cnf(s445,plain,
~ spl81_80,
inference(rat,[],[s359,s416]) ).
cnf(s446,plain,
~ spl81_79,
inference(rat,[],[s351,s433]) ).
cnf(s447,plain,
~ spl81_78,
inference(rat,[],[s350,s431]) ).
cnf(s448,plain,
~ spl81_77,
inference(rat,[],[s343,s427]) ).
cnf(s449,plain,
~ spl81_76,
inference(rat,[],[s337,s434]) ).
cnf(s450,plain,
~ spl81_75,
inference(rat,[],[s333,s414]) ).
cnf(s451,plain,
~ spl81_74,
inference(rat,[],[s330,s432]) ).
cnf(s452,plain,
~ spl81_73,
inference(rat,[],[s322,s430]) ).
cnf(s453,plain,
~ spl81_72,
inference(rat,[],[s316,s425]) ).
cnf(s454,plain,
~ spl81_71,
inference(rat,[],[s314,s420]) ).
cnf(s455,plain,
~ spl81_70,
inference(rat,[],[s307,s412]) ).
cnf(s456,plain,
~ spl81_69,
inference(rat,[],[s303,s428]) ).
cnf(s457,plain,
~ spl81_68,
inference(rat,[],[s296,s426]) ).
cnf(s458,plain,
~ spl81_67,
inference(rat,[],[s294,s429]) ).
cnf(s459,plain,
~ spl81_66,
inference(rat,[],[s290,s422]) ).
cnf(s460,plain,
~ spl81_65,
inference(rat,[],[s281,s410]) ).
cnf(s461,plain,
~ spl81_64,
inference(rat,[],[s277,s424]) ).
cnf(s462,plain,
~ spl81_63,
inference(rat,[],[s274,s421]) ).
cnf(s463,plain,
~ spl81_62,
inference(rat,[],[s270,s423]) ).
cnf(s464,plain,
~ spl81_61,
inference(rat,[],[s263,s419]) ).
cnf(s465,plain,
~ spl81_51,
inference(rat,[],[s260,s435]) ).
cnf(s466,plain,
~ spl81_50,
inference(rat,[],[s255,s418]) ).
cnf(s467,plain,
~ spl81_49,
inference(rat,[],[s250,s418]) ).
cnf(s468,plain,
~ spl81_48,
inference(rat,[],[s244,s417]) ).
cnf(s469,plain,
~ spl81_47,
inference(rat,[],[s239,s416]) ).
cnf(s470,plain,
~ spl81_46,
inference(rat,[],[s233,s415]) ).
cnf(s471,plain,
~ spl81_45,
inference(rat,[],[s228,s414]) ).
cnf(s472,plain,
~ spl81_44,
inference(rat,[],[s222,s413]) ).
cnf(s473,plain,
~ spl81_43,
inference(rat,[],[s217,s412]) ).
cnf(s474,plain,
~ spl81_42,
inference(rat,[],[s211,s411]) ).
cnf(s475,plain,
~ spl81_41,
inference(rat,[],[s206,s410]) ).
cnf(s476,plain,
~ spl81_40,
inference(rat,[],[s203,s431]) ).
cnf(s477,plain,
~ spl81_39,
inference(rat,[],[s198,s432]) ).
cnf(s478,plain,
~ spl81_38,
inference(rat,[],[s195,s416]) ).
cnf(s479,plain,
~ spl81_37,
inference(rat,[],[s190,s417]) ).
cnf(s480,plain,
~ spl81_36,
inference(rat,[],[s182,s427]) ).
cnf(s481,plain,
~ spl81_35,
inference(rat,[],[s177,s428]) ).
cnf(s482,plain,
~ spl81_34,
inference(rat,[],[s171,s434]) ).
cnf(s483,plain,
~ spl81_33,
inference(rat,[],[s166,s424]) ).
cnf(s484,plain,
~ spl81_32,
inference(rat,[],[s164,s433]) ).
cnf(s485,plain,
~ spl81_31,
inference(rat,[],[s159,s433]) ).
cnf(s486,plain,
~ spl81_30,
inference(rat,[],[s154,s432]) ).
cnf(s487,plain,
~ spl81_29,
inference(rat,[],[s149,s431]) ).
cnf(s488,plain,
~ spl81_28,
inference(rat,[],[s141,s420]) ).
cnf(s489,plain,
~ spl81_27,
inference(rat,[],[s136,s421]) ).
cnf(s490,plain,
~ spl81_26,
inference(rat,[],[s135,s414]) ).
cnf(s491,plain,
~ spl81_25,
inference(rat,[],[s130,s415]) ).
cnf(s492,plain,
~ spl81_24,
inference(rat,[],[s123,s430]) ).
cnf(s493,plain,
~ spl81_23,
inference(rat,[],[s118,s430]) ).
cnf(s494,plain,
~ spl81_22,
inference(rat,[],[s112,s425]) ).
cnf(s495,plain,
~ spl81_21,
inference(rat,[],[s107,s426]) ).
cnf(s496,plain,
~ spl81_20,
inference(rat,[],[s101,s422]) ).
cnf(s497,plain,
~ spl81_19,
inference(rat,[],[s96,s423]) ).
cnf(s498,plain,
~ spl81_18,
inference(rat,[],[s92,s429]) ).
cnf(s499,plain,
~ spl81_17,
inference(rat,[],[s87,s429]) ).
cnf(s500,plain,
~ spl81_16,
inference(rat,[],[s84,s428]) ).
cnf(s501,plain,
~ spl81_15,
inference(rat,[],[s79,s427]) ).
cnf(s502,plain,
~ spl81_14,
inference(rat,[],[s75,s412]) ).
cnf(s503,plain,
~ spl81_13,
inference(rat,[],[s70,s413]) ).
cnf(s504,plain,
~ spl81_12,
inference(rat,[],[s63,s426]) ).
cnf(s505,plain,
~ spl81_11,
inference(rat,[],[s58,s425]) ).
cnf(s506,plain,
~ spl81_10,
inference(rat,[],[s52,s423]) ).
cnf(s507,plain,
~ spl81_9,
inference(rat,[],[s47,s422]) ).
cnf(s508,plain,
~ spl81_8,
inference(rat,[],[s43,s421]) ).
cnf(s509,plain,
~ spl81_7,
inference(rat,[],[s38,s420]) ).
cnf(s510,plain,
~ spl81_6,
inference(rat,[],[s31,s419]) ).
cnf(s511,plain,
~ spl81_5,
inference(rat,[],[s26,s419]) ).
cnf(s512,plain,
~ spl81_4,
inference(rat,[],[s24,s424]) ).
cnf(s513,plain,
~ spl81_3,
inference(rat,[],[s19,s434]) ).
cnf(s514,plain,
~ spl81_2,
inference(rat,[],[s15,s410]) ).
cnf(s515,plain,
~ spl81_1,
inference(rat,[],[s10,s411]) ).
cnf(s516,plain,
$false,
inference(rat,[],[s5,s436,s437,s438,s439,s440,s441,s442,s443,s444,s445,s446,s447,s448,s449,s450,s451,s452,s453,s454,s455,s456,s457,s458,s459,s460,s461,s462,s463,s464,s418,s417,s416,s415,s414,s413,s412,s411,s410,s465,s466,s467,s468,s469,s470,s471,s472,s473,s474,s475,s476,s477,s478,s479,s480,s481,s482,s483,s484,s485,s486,s487,s488,s489,s490,s491,s492,s493,s494,s495,s496,s497,s498,s499,s500,s501,s502,s503,s504,s505,s506,s507,s508,s509,s510,s511,s512,s513,s514,s515]) ).
fof(f2522,plain,
$false,
inference(avatar_sat_refutation,[],[s516]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG090+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n007.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.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 19:23:55 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.19/0.71 % (2730621)Detected formulas, will run a generic FOF schedule.
% 1.19/0.71 % (2730632)dis-21_1_sil=8000:lcm=predicate:random_seed=412408474:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 1.19/0.71 % (2730632)First to succeed.
% 1.19/0.71 % (2730631)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3304537685:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 1.19/0.71 % (2730627)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3236330666:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 1.19/0.71 % (2730630)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2233199710:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 1.19/0.71 % (2730629)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4124672075:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 1.19/0.71 % (2730626)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1173549515:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 1.19/0.71 % (2730628)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1830559800:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 1.19/0.71 % (2730632)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2730621"
% 1.19/0.71 % (2730631)Also succeeded, but the first one will report.
% 1.19/0.71 % (2730630)Also succeeded, but the first one will report.
% 1.19/0.71 % (2730629)Refutation not found, incomplete strategy
% 1.19/0.71 % (2730629)------------------------------
% 1.19/0.71 % (2730629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.19/0.71 % (2730629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.19/0.71 % (2730629)CaDiCaL version: 2.1.3
% 1.19/0.71 % (2730629)Termination reason: Refutation not found, incomplete strategy
% 1.19/0.71 % (2730629)Time elapsed: 0.034 s
% 1.19/0.71 % (2730629)Peak memory usage: 90 MB
% 1.19/0.71 % (2730629)Instructions burned: 71 (million)
% 1.19/0.71 % (2730632)Refutation found. Thanks to Tanya!
% 1.19/0.71 % SZS status Theorem for theBenchmark
% 1.19/0.71 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/0.90 % (2730632)------------------------------
% 0.18/0.90 % (2730632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/0.90 % (2730632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.90 % (2730632)CaDiCaL version: 2.1.3
% 0.18/0.90 % (2730632)Termination reason: Refutation
% 0.18/0.90 % (2730632)Time elapsed: 0.016 s
% 0.18/0.90 % (2730632)Peak memory usage: 90 MB
% 0.18/0.90 % (2730632)Instructions burned: 59 (million)
% 0.18/0.90 % (2730632)------------------------------
% 0.18/0.90 % (2730632)------------------------------
% 0.18/0.90 % (2730621)Success in time 0.299 s
% 0.18/0.90 % Vampire exiting
%------------------------------------------------------------------------------