%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG092+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:21:28 AM UTC 2026
% Result : Theorem 0.19s 0.28s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 124
% Syntax : Number of formulae : 718 ( 202 unt; 120 def)
% Number of atoms : 3267 (1692 equ)
% Maximal formula atoms : 440 ( 4 avg)
% Number of connectives : 3981 (1432 ~;1842 |; 587 &)
% ( 120 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 98 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 201 ( 199 usr; 200 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e0 != e4
& e1 != e2
& e1 != e3
& e1 != e4
& e2 != e3
& e2 != e4
& e3 != e4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
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) = e3
& op(e1,e3) = e0
& op(e1,e4) = e2
& op(e2,e0) = e2
& op(e2,e1) = e0
& op(e2,e2) = e4
& op(e2,e3) = e1
& op(e2,e4) = e3
& op(e3,e0) = e3
& op(e3,e1) = e2
& op(e3,e2) = e0
& op(e3,e3) = e4
& op(e3,e4) = e1
& op(e4,e0) = e4
& op(e4,e1) = e3
& op(e4,e2) = e1
& op(e4,e3) = e2
& op(e4,e4) = e0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
unit = e0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
fof(f4,conjecture,
( ( ( op(e0,op(e0,e0)) != e0
& op(e0,op(e0,e0)) = e0 )
| ( op(e1,op(e1,e0)) != e0
& op(e0,op(e1,e0)) = e1 )
| ( op(e2,op(e2,e0)) != e0
& op(e0,op(e2,e0)) = e2 )
| ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 ) )
& ( ( op(e0,op(e0,e1)) != e1
& op(e1,op(e0,e1)) = e0 )
| ( op(e1,op(e1,e1)) != e1
& op(e1,op(e1,e1)) = e1 )
| ( op(e2,op(e2,e1)) != e1
& op(e1,op(e2,e1)) = e2 )
| ( op(e3,op(e3,e1)) != e1
& op(e1,op(e3,e1)) = e3 )
| ( op(e4,op(e4,e1)) != e1
& op(e1,op(e4,e1)) = e4 ) )
& ( ( op(e0,op(e0,e2)) != e2
& op(e2,op(e0,e2)) = e0 )
| ( op(e1,op(e1,e2)) != e2
& op(e2,op(e1,e2)) = e1 )
| ( op(e2,op(e2,e2)) != e2
& op(e2,op(e2,e2)) = e2 )
| ( op(e3,op(e3,e2)) != e2
& op(e2,op(e3,e2)) = e3 )
| ( op(e4,op(e4,e2)) != e2
& op(e2,op(e4,e2)) = e4 ) )
& ( ( op(e0,op(e0,e3)) != e3
& op(e3,op(e0,e3)) = e0 )
| ( op(e1,op(e1,e3)) != e3
& op(e3,op(e1,e3)) = e1 )
| ( op(e2,op(e2,e3)) != e3
& op(e3,op(e2,e3)) = e2 )
| ( op(e3,op(e3,e3)) != e3
& op(e3,op(e3,e3)) = e3 )
| ( op(e4,op(e4,e3)) != e3
& op(e3,op(e4,e3)) = e4 ) )
& ( ( op(e0,op(e0,e4)) != e4
& op(e4,op(e0,e4)) = e0 )
| ( op(e1,op(e1,e4)) != e4
& op(e4,op(e1,e4)) = e1 )
| ( op(e2,op(e2,e4)) != e4
& op(e4,op(e2,e4)) = e2 )
| ( op(e3,op(e3,e4)) != e4
& op(e4,op(e3,e4)) = e3 )
| ( op(e4,op(e4,e4)) != e4
& op(e4,op(e4,e4)) = e4 ) )
& ( op(e0,e0) = e0
| op(e0,e0) = 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/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f5,negated_conjecture,
~ ( ( ( op(e0,op(e0,e0)) != e0
& op(e0,op(e0,e0)) = e0 )
| ( op(e1,op(e1,e0)) != e0
& op(e0,op(e1,e0)) = e1 )
| ( op(e2,op(e2,e0)) != e0
& op(e0,op(e2,e0)) = e2 )
| ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 ) )
& ( ( op(e0,op(e0,e1)) != e1
& op(e1,op(e0,e1)) = e0 )
| ( op(e1,op(e1,e1)) != e1
& op(e1,op(e1,e1)) = e1 )
| ( op(e2,op(e2,e1)) != e1
& op(e1,op(e2,e1)) = e2 )
| ( op(e3,op(e3,e1)) != e1
& op(e1,op(e3,e1)) = e3 )
| ( op(e4,op(e4,e1)) != e1
& op(e1,op(e4,e1)) = e4 ) )
& ( ( op(e0,op(e0,e2)) != e2
& op(e2,op(e0,e2)) = e0 )
| ( op(e1,op(e1,e2)) != e2
& op(e2,op(e1,e2)) = e1 )
| ( op(e2,op(e2,e2)) != e2
& op(e2,op(e2,e2)) = e2 )
| ( op(e3,op(e3,e2)) != e2
& op(e2,op(e3,e2)) = e3 )
| ( op(e4,op(e4,e2)) != e2
& op(e2,op(e4,e2)) = e4 ) )
& ( ( op(e0,op(e0,e3)) != e3
& op(e3,op(e0,e3)) = e0 )
| ( op(e1,op(e1,e3)) != e3
& op(e3,op(e1,e3)) = e1 )
| ( op(e2,op(e2,e3)) != e3
& op(e3,op(e2,e3)) = e2 )
| ( op(e3,op(e3,e3)) != e3
& op(e3,op(e3,e3)) = e3 )
| ( op(e4,op(e4,e3)) != e3
& op(e3,op(e4,e3)) = e4 ) )
& ( ( op(e0,op(e0,e4)) != e4
& op(e4,op(e0,e4)) = e0 )
| ( op(e1,op(e1,e4)) != e4
& op(e4,op(e1,e4)) = e1 )
| ( op(e2,op(e2,e4)) != e4
& op(e4,op(e2,e4)) = e2 )
| ( op(e3,op(e3,e4)) != e4
& op(e4,op(e3,e4)) = e3 )
| ( op(e4,op(e4,e4)) != e4
& op(e4,op(e4,e4)) = e4 ) )
& ( op(e0,e0) = e0
| op(e0,e0) = 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,op(e0,e0))
| e0 != op(e0,op(e0,e0)) )
& ( e0 = op(e1,op(e1,e0))
| e1 != op(e0,op(e1,e0)) )
& ( e0 = op(e2,op(e2,e0))
| e2 != op(e0,op(e2,e0)) )
& ( e0 = op(e3,op(e3,e0))
| e3 != op(e0,op(e3,e0)) )
& ( e0 = op(e4,op(e4,e0))
| e4 != op(e0,op(e4,e0)) ) )
| ( ( e1 = op(e0,op(e0,e1))
| e0 != op(e1,op(e0,e1)) )
& ( e1 = op(e1,op(e1,e1))
| e1 != op(e1,op(e1,e1)) )
& ( e1 = op(e2,op(e2,e1))
| e2 != op(e1,op(e2,e1)) )
& ( e1 = op(e3,op(e3,e1))
| e3 != op(e1,op(e3,e1)) )
& ( e1 = op(e4,op(e4,e1))
| e4 != op(e1,op(e4,e1)) ) )
| ( ( e2 = op(e0,op(e0,e2))
| e0 != op(e2,op(e0,e2)) )
& ( e2 = op(e1,op(e1,e2))
| e1 != op(e2,op(e1,e2)) )
& ( e2 = op(e2,op(e2,e2))
| e2 != op(e2,op(e2,e2)) )
& ( e2 = op(e3,op(e3,e2))
| e3 != op(e2,op(e3,e2)) )
& ( e2 = op(e4,op(e4,e2))
| e4 != op(e2,op(e4,e2)) ) )
| ( ( e3 = op(e0,op(e0,e3))
| e0 != op(e3,op(e0,e3)) )
& ( e3 = op(e1,op(e1,e3))
| e1 != op(e3,op(e1,e3)) )
& ( e3 = op(e2,op(e2,e3))
| e2 != op(e3,op(e2,e3)) )
& ( e3 = op(e3,op(e3,e3))
| e3 != op(e3,op(e3,e3)) )
& ( e3 = op(e4,op(e4,e3))
| e4 != op(e3,op(e4,e3)) ) )
| ( ( e4 = op(e0,op(e0,e4))
| e0 != op(e4,op(e0,e4)) )
& ( e4 = op(e1,op(e1,e4))
| e1 != op(e4,op(e1,e4)) )
& ( e4 = op(e2,op(e2,e4))
| e2 != op(e4,op(e2,e4)) )
& ( e4 = op(e3,op(e3,e4))
| e3 != op(e4,op(e3,e4)) )
& ( e4 = op(e4,op(e4,e4))
| e4 != op(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(f8,plain,
e2 != e4,
inference(cnf_transformation,[],[f1]) ).
fof(f13,plain,
e0 != e4,
inference(cnf_transformation,[],[f1]) ).
fof(f14,plain,
e0 != e3,
inference(cnf_transformation,[],[f1]) ).
fof(f15,plain,
e0 != e2,
inference(cnf_transformation,[],[f1]) ).
fof(f16,plain,
e0 != e1,
inference(cnf_transformation,[],[f1]) ).
fof(f17,plain,
e0 = op(e4,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f18,plain,
e2 = op(e4,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f19,plain,
e1 = op(e4,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f20,plain,
e3 = op(e4,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f21,plain,
e4 = op(e4,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f22,plain,
e1 = op(e3,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f23,plain,
e4 = op(e3,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f24,plain,
e0 = op(e3,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f25,plain,
e2 = op(e3,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f26,plain,
e3 = op(e3,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f27,plain,
e3 = op(e2,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f28,plain,
e1 = op(e2,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f29,plain,
e4 = op(e2,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f30,plain,
e0 = op(e2,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f31,plain,
e2 = op(e2,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f32,plain,
e2 = op(e1,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f33,plain,
e0 = op(e1,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f34,plain,
e3 = op(e1,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f35,plain,
e4 = op(e1,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f36,plain,
e1 = op(e1,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f37,plain,
e4 = op(e0,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f38,plain,
e3 = op(e0,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f39,plain,
e2 = op(e0,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f40,plain,
e1 = op(e0,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f41,plain,
e0 = op(e0,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f42,plain,
e0 = unit,
inference(cnf_transformation,[],[f3]) ).
fof(f43,plain,
( e1 != op(e0,op(e1,e0))
| e0 = op(e1,op(e1,e0))
| ~ sP78 ),
inference(cnf_transformation,[],[f6]) ).
fof(f49,plain,
( e3 != op(e1,op(e3,e1))
| e1 = op(e3,op(e3,e1))
| ~ sP77 ),
inference(cnf_transformation,[],[f6]) ).
fof(f52,plain,
( e1 != op(e2,op(e1,e2))
| e2 = op(e1,op(e1,e2))
| ~ sP76 ),
inference(cnf_transformation,[],[f6]) ).
fof(f57,plain,
( e2 != op(e3,op(e2,e3))
| e3 = op(e2,op(e2,e3))
| ~ sP75 ),
inference(cnf_transformation,[],[f6]) ).
fof(f62,plain,
( e3 != op(e4,op(e3,e4))
| e4 = op(e3,op(e3,e4))
| ~ sP74 ),
inference(cnf_transformation,[],[f6]) ).
fof(f67,plain,
( e0 != op(e0,e0)
| ~ sP73 ),
inference(cnf_transformation,[],[f6]) ).
fof(f71,plain,
( e1 != op(e0,e1)
| ~ sP72 ),
inference(cnf_transformation,[],[f6]) ).
fof(f75,plain,
( e2 != op(e0,e2)
| ~ sP71 ),
inference(cnf_transformation,[],[f6]) ).
fof(f79,plain,
( e3 != op(e0,e3)
| ~ sP70 ),
inference(cnf_transformation,[],[f6]) ).
fof(f83,plain,
( e4 != op(e0,e4)
| ~ sP69 ),
inference(cnf_transformation,[],[f6]) ).
fof(f91,plain,
( e1 != op(e1,e0)
| ~ sP68 ),
inference(cnf_transformation,[],[f6]) ).
fof(f93,plain,
( e4 != op(e1,e1)
| ~ sP67 ),
inference(cnf_transformation,[],[f6]) ).
fof(f99,plain,
( e3 != op(e1,e2)
| ~ sP66 ),
inference(cnf_transformation,[],[f6]) ).
fof(f107,plain,
( e0 != op(e1,e3)
| ~ sP65 ),
inference(cnf_transformation,[],[f6]) ).
fof(f110,plain,
( e2 != op(e1,e4)
| ~ sP64 ),
inference(cnf_transformation,[],[f6]) ).
fof(f115,plain,
( e2 != op(e2,e0)
| ~ sP63 ),
inference(cnf_transformation,[],[f6]) ).
fof(f122,plain,
( e0 != op(e2,e1)
| ~ sP62 ),
inference(cnf_transformation,[],[f6]) ).
fof(f123,plain,
( e4 != op(e2,e2)
| ~ sP61 ),
inference(cnf_transformation,[],[f6]) ).
fof(f131,plain,
( e1 != op(e2,e3)
| ~ sP60 ),
inference(cnf_transformation,[],[f6]) ).
fof(f134,plain,
( e3 != op(e2,e4)
| ~ sP59 ),
inference(cnf_transformation,[],[f6]) ).
fof(f139,plain,
( e3 != op(e3,e0)
| ~ sP58 ),
inference(cnf_transformation,[],[f6]) ).
fof(f145,plain,
( e2 != op(e3,e1)
| ~ sP57 ),
inference(cnf_transformation,[],[f6]) ).
fof(f152,plain,
( e0 != op(e3,e2)
| ~ sP56 ),
inference(cnf_transformation,[],[f6]) ).
fof(f153,plain,
( e4 != op(e3,e3)
| ~ sP55 ),
inference(cnf_transformation,[],[f6]) ).
fof(f161,plain,
( e1 != op(e3,e4)
| ~ sP54 ),
inference(cnf_transformation,[],[f6]) ).
fof(f163,plain,
( e4 != op(e4,e0)
| ~ sP53 ),
inference(cnf_transformation,[],[f6]) ).
fof(f169,plain,
( e3 != op(e4,e1)
| ~ sP52 ),
inference(cnf_transformation,[],[f6]) ).
fof(f176,plain,
( e1 != op(e4,e2)
| ~ sP51 ),
inference(cnf_transformation,[],[f6]) ).
fof(f180,plain,
( e2 != op(e4,e3)
| ~ sP50 ),
inference(cnf_transformation,[],[f6]) ).
fof(f187,plain,
( e0 != op(e4,e4)
| ~ sP49 ),
inference(cnf_transformation,[],[f6]) ).
fof(f192,plain,
( e0 != unit
| ~ sP48 ),
inference(cnf_transformation,[],[f6]) ).
fof(f197,plain,
( e0 != op(e0,e0)
| ~ sP47 ),
inference(cnf_transformation,[],[f6]) ).
fof(f202,plain,
( e0 != op(e0,e0)
| ~ sP46 ),
inference(cnf_transformation,[],[f6]) ).
fof(f206,plain,
( e1 != op(e0,e1)
| ~ sP45 ),
inference(cnf_transformation,[],[f6]) ).
fof(f211,plain,
( e1 != op(e1,e0)
| ~ sP44 ),
inference(cnf_transformation,[],[f6]) ).
fof(f215,plain,
( e2 != op(e0,e2)
| ~ sP43 ),
inference(cnf_transformation,[],[f6]) ).
fof(f220,plain,
( e2 != op(e2,e0)
| ~ sP42 ),
inference(cnf_transformation,[],[f6]) ).
fof(f224,plain,
( e3 != op(e0,e3)
| ~ sP41 ),
inference(cnf_transformation,[],[f6]) ).
fof(f229,plain,
( e3 != op(e3,e0)
| ~ sP40 ),
inference(cnf_transformation,[],[f6]) ).
fof(f233,plain,
( e4 != op(e0,e4)
| ~ sP39 ),
inference(cnf_transformation,[],[f6]) ).
fof(f238,plain,
( e4 != op(e4,e0)
| ~ sP38 ),
inference(cnf_transformation,[],[f6]) ).
fof(f244,plain,
( e0 != op(e1,e3)
| ~ sP37 ),
inference(cnf_transformation,[],[f6]) ).
fof(f250,plain,
( e0 != op(e2,e1)
| ~ sP36 ),
inference(cnf_transformation,[],[f6]) ).
fof(f257,plain,
( e1 != op(e1,e0)
| ~ sP35 ),
inference(cnf_transformation,[],[f6]) ).
fof(f262,plain,
( e1 != op(e0,e1)
| ~ sP34 ),
inference(cnf_transformation,[],[f6]) ).
fof(f263,plain,
( e2 != op(e1,e4)
| ~ sP33 ),
inference(cnf_transformation,[],[f6]) ).
fof(f269,plain,
( e2 != op(e3,e1)
| ~ sP32 ),
inference(cnf_transformation,[],[f6]) ).
fof(f275,plain,
( e3 != op(e1,e2)
| ~ sP31 ),
inference(cnf_transformation,[],[f6]) ).
fof(f278,plain,
( e3 != op(e4,e1)
| ~ sP30 ),
inference(cnf_transformation,[],[f6]) ).
fof(f286,plain,
( e4 != op(e1,e1)
| ~ sP29 ),
inference(cnf_transformation,[],[f6]) ).
fof(f291,plain,
( e4 != op(e1,e1)
| ~ sP28 ),
inference(cnf_transformation,[],[f6]) ).
fof(f296,plain,
( e0 != op(e2,e1)
| ~ sP27 ),
inference(cnf_transformation,[],[f6]) ).
fof(f299,plain,
( e0 != op(e3,e2)
| ~ sP26 ),
inference(cnf_transformation,[],[f6]) ).
fof(f304,plain,
( e1 != op(e2,e3)
| ~ sP25 ),
inference(cnf_transformation,[],[f6]) ).
fof(f308,plain,
( e1 != op(e4,e2)
| ~ sP24 ),
inference(cnf_transformation,[],[f6]) ).
fof(f317,plain,
( e2 != op(e2,e0)
| ~ sP23 ),
inference(cnf_transformation,[],[f6]) ).
fof(f322,plain,
( e2 != op(e0,e2)
| ~ sP22 ),
inference(cnf_transformation,[],[f6]) ).
fof(f323,plain,
( e3 != op(e2,e4)
| ~ sP21 ),
inference(cnf_transformation,[],[f6]) ).
fof(f331,plain,
( e3 != op(e1,e2)
| ~ sP20 ),
inference(cnf_transformation,[],[f6]) ).
fof(f335,plain,
( e4 != op(e2,e2)
| ~ sP19 ),
inference(cnf_transformation,[],[f6]) ).
fof(f340,plain,
( e4 != op(e2,e2)
| ~ sP18 ),
inference(cnf_transformation,[],[f6]) ).
fof(f345,plain,
( e0 != op(e3,e2)
| ~ sP17 ),
inference(cnf_transformation,[],[f6]) ).
fof(f351,plain,
( e0 != op(e1,e3)
| ~ sP16 ),
inference(cnf_transformation,[],[f6]) ).
fof(f353,plain,
( e1 != op(e3,e4)
| ~ sP15 ),
inference(cnf_transformation,[],[f6]) ).
fof(f360,plain,
( e1 != op(e2,e3)
| ~ sP14 ),
inference(cnf_transformation,[],[f6]) ).
fof(f366,plain,
( e2 != op(e3,e1)
| ~ sP13 ),
inference(cnf_transformation,[],[f6]) ).
fof(f368,plain,
( e2 != op(e4,e3)
| ~ sP12 ),
inference(cnf_transformation,[],[f6]) ).
fof(f377,plain,
( e3 != op(e3,e0)
| ~ sP11 ),
inference(cnf_transformation,[],[f6]) ).
fof(f382,plain,
( e3 != op(e0,e3)
| ~ sP10 ),
inference(cnf_transformation,[],[f6]) ).
fof(f384,plain,
( e4 != op(e3,e3)
| ~ sP9 ),
inference(cnf_transformation,[],[f6]) ).
fof(f389,plain,
( e4 != op(e3,e3)
| ~ sP8 ),
inference(cnf_transformation,[],[f6]) ).
fof(f393,plain,
( e0 != op(e4,e4)
| ~ sP7 ),
inference(cnf_transformation,[],[f6]) ).
fof(f398,plain,
( e0 != op(e4,e4)
| ~ sP6 ),
inference(cnf_transformation,[],[f6]) ).
fof(f405,plain,
( e1 != op(e4,e2)
| ~ sP5 ),
inference(cnf_transformation,[],[f6]) ).
fof(f409,plain,
( e1 != op(e3,e4)
| ~ sP4 ),
inference(cnf_transformation,[],[f6]) ).
fof(f414,plain,
( e2 != op(e4,e3)
| ~ sP3 ),
inference(cnf_transformation,[],[f6]) ).
fof(f421,plain,
( e2 != op(e1,e4)
| ~ sP2 ),
inference(cnf_transformation,[],[f6]) ).
fof(f426,plain,
( e3 != op(e4,e1)
| ~ sP1 ),
inference(cnf_transformation,[],[f6]) ).
fof(f430,plain,
( e3 != op(e2,e4)
| ~ sP0 ),
inference(cnf_transformation,[],[f6]) ).
fof(f437,plain,
( e4 != op(e0,e4)
| e4 != op(e4,e0)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13
| sP14
| sP15
| sP16
| sP17
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23
| sP24
| sP25
| sP26
| sP27
| sP28
| sP29
| sP30
| sP31
| sP32
| sP33
| sP34
| sP35
| sP36
| sP37
| sP38
| sP39
| sP40
| sP41
| sP42
| sP43
| sP44
| sP45
| sP46
| sP47
| sP48
| e4 != op(e4,unit)
| e4 != op(unit,e4)
| e3 != op(e3,unit)
| e3 != op(unit,e3)
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| e0 != op(e0,unit)
| e0 != op(unit,e0)
| sP49
| sP50
| sP51
| sP52
| sP53
| sP54
| sP55
| sP56
| sP57
| sP58
| sP59
| sP60
| sP61
| sP62
| sP63
| sP64
| sP65
| sP66
| sP67
| sP68
| sP69
| sP70
| sP71
| sP72
| sP73
| sP74
| sP75
| sP76
| sP77
| sP78 ),
inference(cnf_transformation,[],[f6]) ).
fof(f458,plain,
e1 != unit,
inference(definition_unfolding,[],[f16,f42]) ).
fof(f459,plain,
e2 != unit,
inference(definition_unfolding,[],[f15,f42]) ).
fof(f460,plain,
e3 != unit,
inference(definition_unfolding,[],[f14,f42]) ).
fof(f461,plain,
e4 != unit,
inference(definition_unfolding,[],[f13,f42]) ).
fof(f462,plain,
unit = op(unit,unit),
inference(definition_unfolding,[],[f41,f42,f42,f42]) ).
fof(f463,plain,
e1 = op(unit,e1),
inference(definition_unfolding,[],[f40,f42]) ).
fof(f464,plain,
e2 = op(unit,e2),
inference(definition_unfolding,[],[f39,f42]) ).
fof(f465,plain,
e3 = op(unit,e3),
inference(definition_unfolding,[],[f38,f42]) ).
fof(f466,plain,
e4 = op(unit,e4),
inference(definition_unfolding,[],[f37,f42]) ).
fof(f467,plain,
e1 = op(e1,unit),
inference(definition_unfolding,[],[f36,f42]) ).
fof(f468,plain,
op(e1,e3) = unit,
inference(definition_unfolding,[],[f33,f42]) ).
fof(f469,plain,
e2 = op(e2,unit),
inference(definition_unfolding,[],[f31,f42]) ).
fof(f470,plain,
op(e2,e1) = unit,
inference(definition_unfolding,[],[f30,f42]) ).
fof(f471,plain,
e3 = op(e3,unit),
inference(definition_unfolding,[],[f26,f42]) ).
fof(f472,plain,
op(e3,e2) = unit,
inference(definition_unfolding,[],[f24,f42]) ).
fof(f473,plain,
e4 = op(e4,unit),
inference(definition_unfolding,[],[f21,f42]) ).
fof(f474,plain,
op(e4,e4) = unit,
inference(definition_unfolding,[],[f17,f42]) ).
fof(f495,plain,
( e4 != op(unit,e4)
| e4 != op(e4,unit)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13
| sP14
| sP15
| sP16
| sP17
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23
| sP24
| sP25
| sP26
| sP27
| sP28
| sP29
| sP30
| sP31
| sP32
| sP33
| sP34
| sP35
| sP36
| sP37
| sP38
| sP39
| sP40
| sP41
| sP42
| sP43
| sP44
| sP45
| sP46
| sP47
| sP48
| e4 != op(e4,unit)
| e4 != op(unit,e4)
| e3 != op(e3,unit)
| e3 != op(unit,e3)
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| unit != op(unit,unit)
| unit != op(unit,unit)
| sP49
| sP50
| sP51
| sP52
| sP53
| sP54
| sP55
| sP56
| sP57
| sP58
| sP59
| sP60
| sP61
| sP62
| sP63
| sP64
| sP65
| sP66
| sP67
| sP68
| sP69
| sP70
| sP71
| sP72
| sP73
| sP74
| sP75
| sP76
| sP77
| sP78 ),
inference(definition_unfolding,[],[f437,f42,f42,f42,f42,f42,f42]) ).
fof(f510,plain,
( op(e4,e4) != unit
| ~ sP6 ),
inference(definition_unfolding,[],[f398,f42]) ).
fof(f515,plain,
( op(e4,e4) != unit
| ~ sP7 ),
inference(definition_unfolding,[],[f393,f42]) ).
fof(f518,plain,
( e3 != op(unit,e3)
| ~ sP10 ),
inference(definition_unfolding,[],[f382,f42]) ).
fof(f519,plain,
( e3 != op(e3,unit)
| ~ sP11 ),
inference(definition_unfolding,[],[f377,f42]) ).
fof(f525,plain,
( op(e1,e3) != unit
| ~ sP16 ),
inference(definition_unfolding,[],[f351,f42]) ).
fof(f531,plain,
( op(e3,e2) != unit
| ~ sP17 ),
inference(definition_unfolding,[],[f345,f42]) ).
fof(f538,plain,
( e2 != op(unit,e2)
| ~ sP22 ),
inference(definition_unfolding,[],[f322,f42]) ).
fof(f539,plain,
( e2 != op(e2,unit)
| ~ sP23 ),
inference(definition_unfolding,[],[f317,f42]) ).
fof(f545,plain,
( op(e3,e2) != unit
| ~ sP26 ),
inference(definition_unfolding,[],[f299,f42]) ).
fof(f548,plain,
( op(e2,e1) != unit
| ~ sP27 ),
inference(definition_unfolding,[],[f296,f42]) ).
fof(f558,plain,
( e1 != op(unit,e1)
| ~ sP34 ),
inference(definition_unfolding,[],[f262,f42]) ).
fof(f559,plain,
( e1 != op(e1,unit)
| ~ sP35 ),
inference(definition_unfolding,[],[f257,f42]) ).
fof(f562,plain,
( op(e2,e1) != unit
| ~ sP36 ),
inference(definition_unfolding,[],[f250,f42]) ).
fof(f568,plain,
( op(e1,e3) != unit
| ~ sP37 ),
inference(definition_unfolding,[],[f244,f42]) ).
fof(f574,plain,
( e4 != op(e4,unit)
| ~ sP38 ),
inference(definition_unfolding,[],[f238,f42]) ).
fof(f579,plain,
( e4 != op(unit,e4)
| ~ sP39 ),
inference(definition_unfolding,[],[f233,f42]) ).
fof(f583,plain,
( e3 != op(e3,unit)
| ~ sP40 ),
inference(definition_unfolding,[],[f229,f42]) ).
fof(f588,plain,
( e3 != op(unit,e3)
| ~ sP41 ),
inference(definition_unfolding,[],[f224,f42]) ).
fof(f592,plain,
( e2 != op(e2,unit)
| ~ sP42 ),
inference(definition_unfolding,[],[f220,f42]) ).
fof(f597,plain,
( e2 != op(unit,e2)
| ~ sP43 ),
inference(definition_unfolding,[],[f215,f42]) ).
fof(f601,plain,
( e1 != op(e1,unit)
| ~ sP44 ),
inference(definition_unfolding,[],[f211,f42]) ).
fof(f606,plain,
( e1 != op(unit,e1)
| ~ sP45 ),
inference(definition_unfolding,[],[f206,f42]) ).
fof(f610,plain,
( unit != op(unit,unit)
| ~ sP46 ),
inference(definition_unfolding,[],[f202,f42,f42,f42]) ).
fof(f615,plain,
( unit != op(unit,unit)
| ~ sP47 ),
inference(definition_unfolding,[],[f197,f42,f42,f42]) ).
fof(f620,plain,
( unit != unit
| ~ sP48 ),
inference(definition_unfolding,[],[f192,f42]) ).
fof(f621,plain,
( op(e4,e4) != unit
| ~ sP49 ),
inference(definition_unfolding,[],[f187,f42]) ).
fof(f629,plain,
( e4 != op(e4,unit)
| ~ sP53 ),
inference(definition_unfolding,[],[f163,f42]) ).
fof(f632,plain,
( op(e3,e2) != unit
| ~ sP56 ),
inference(definition_unfolding,[],[f152,f42]) ).
fof(f637,plain,
( e3 != op(e3,unit)
| ~ sP58 ),
inference(definition_unfolding,[],[f139,f42]) ).
fof(f642,plain,
( op(e2,e1) != unit
| ~ sP62 ),
inference(definition_unfolding,[],[f122,f42]) ).
fof(f645,plain,
( e2 != op(e2,unit)
| ~ sP63 ),
inference(definition_unfolding,[],[f115,f42]) ).
fof(f649,plain,
( op(e1,e3) != unit
| ~ sP65 ),
inference(definition_unfolding,[],[f107,f42]) ).
fof(f653,plain,
( e1 != op(e1,unit)
| ~ sP68 ),
inference(definition_unfolding,[],[f91,f42]) ).
fof(f661,plain,
( e4 != op(unit,e4)
| ~ sP69 ),
inference(definition_unfolding,[],[f83,f42]) ).
fof(f665,plain,
( e3 != op(unit,e3)
| ~ sP70 ),
inference(definition_unfolding,[],[f79,f42]) ).
fof(f669,plain,
( e2 != op(unit,e2)
| ~ sP71 ),
inference(definition_unfolding,[],[f75,f42]) ).
fof(f673,plain,
( e1 != op(unit,e1)
| ~ sP72 ),
inference(definition_unfolding,[],[f71,f42]) ).
fof(f677,plain,
( unit != op(unit,unit)
| ~ sP73 ),
inference(definition_unfolding,[],[f67,f42,f42,f42]) ).
fof(f689,plain,
( e1 != op(unit,op(e1,unit))
| unit = op(e1,op(e1,unit))
| ~ sP78 ),
inference(definition_unfolding,[],[f43,f42,f42,f42,f42]) ).
fof(f710,plain,
( e4 != op(unit,e4)
| e4 != op(e4,unit)
| sP0
| ~ sP1
| ~ sP2
| ~ sP3
| sP4
| ~ sP5
| sP6
| ~ sP7
| ~ sP8
| sP9
| sP10
| sP11
| ~ sP12
| sP13
| ~ sP14
| ~ sP15
| ~ sP16
| sP17
| ~ sP18
| ~ sP19
| sP20
| ~ sP21
| sP22
| sP23
| ~ sP24
| sP25
| sP26
| sP27
| ~ sP28
| sP29
| sP30
| ~ sP31
| sP32
| ~ sP33
| sP34
| sP35
| sP36
| sP37
| sP38
| sP39
| sP40
| ~ sP41
| ~ sP42
| sP43
| ~ sP44
| sP45
| ~ sP46
| ~ sP47
| sP48
| e4 != op(e4,unit)
| e4 != op(unit,e4)
| e3 != op(e3,unit)
| e3 != op(unit,e3)
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| unit != op(unit,unit)
| unit != op(unit,unit)
| sP49
| sP50
| ~ sP51
| ~ sP52
| sP53
| ~ sP54
| sP55
| sP56
| ~ sP57
| sP58
| ~ sP59
| sP60
| sP61
| ~ sP62
| sP63
| sP64
| ~ sP65
| ~ sP66
| sP67
| sP68
| ~ sP69
| sP70
| ~ sP71
| sP72
| sP73
| sP74
| ~ sP75
| sP76
| sP77
| ~ sP78 ),
inference(consistent_polarity_flipping,[],[f495]) ).
fof(f716,plain,
( e3 != op(e4,e1)
| sP1 ),
inference(consistent_polarity_flipping,[],[f426]) ).
fof(f721,plain,
( e2 != op(e1,e4)
| sP2 ),
inference(consistent_polarity_flipping,[],[f421]) ).
fof(f728,plain,
( e2 != op(e4,e3)
| sP3 ),
inference(consistent_polarity_flipping,[],[f414]) ).
fof(f732,plain,
( e1 != op(e4,e2)
| sP5 ),
inference(consistent_polarity_flipping,[],[f405]) ).
fof(f739,plain,
( op(e4,e4) != unit
| sP7 ),
inference(consistent_polarity_flipping,[],[f515]) ).
fof(f743,plain,
( e4 != op(e3,e3)
| sP8 ),
inference(consistent_polarity_flipping,[],[f389]) ).
fof(f749,plain,
( e2 != op(e4,e3)
| sP12 ),
inference(consistent_polarity_flipping,[],[f368]) ).
fof(f752,plain,
( e1 != op(e2,e3)
| sP14 ),
inference(consistent_polarity_flipping,[],[f360]) ).
fof(f759,plain,
( e1 != op(e3,e4)
| sP15 ),
inference(consistent_polarity_flipping,[],[f353]) ).
fof(f761,plain,
( op(e1,e3) != unit
| sP16 ),
inference(consistent_polarity_flipping,[],[f525]) ).
fof(f767,plain,
( e4 != op(e2,e2)
| sP18 ),
inference(consistent_polarity_flipping,[],[f340]) ).
fof(f772,plain,
( e4 != op(e2,e2)
| sP19 ),
inference(consistent_polarity_flipping,[],[f335]) ).
fof(f779,plain,
( e3 != op(e2,e4)
| sP21 ),
inference(consistent_polarity_flipping,[],[f323]) ).
fof(f784,plain,
( e1 != op(e4,e2)
| sP24 ),
inference(consistent_polarity_flipping,[],[f308]) ).
fof(f786,plain,
( e4 != op(e1,e1)
| sP28 ),
inference(consistent_polarity_flipping,[],[f291]) ).
fof(f792,plain,
( e3 != op(e1,e2)
| sP31 ),
inference(consistent_polarity_flipping,[],[f275]) ).
fof(f799,plain,
( e2 != op(e1,e4)
| sP33 ),
inference(consistent_polarity_flipping,[],[f263]) ).
fof(f803,plain,
( e3 != op(unit,e3)
| sP41 ),
inference(consistent_polarity_flipping,[],[f588]) ).
fof(f807,plain,
( e2 != op(e2,unit)
| sP42 ),
inference(consistent_polarity_flipping,[],[f592]) ).
fof(f811,plain,
( e1 != op(e1,unit)
| sP44 ),
inference(consistent_polarity_flipping,[],[f601]) ).
fof(f815,plain,
( unit != op(unit,unit)
| sP46 ),
inference(consistent_polarity_flipping,[],[f610]) ).
fof(f820,plain,
( unit != op(unit,unit)
| sP47 ),
inference(consistent_polarity_flipping,[],[f615]) ).
fof(f826,plain,
( e1 != op(e4,e2)
| sP51 ),
inference(consistent_polarity_flipping,[],[f176]) ).
fof(f833,plain,
( e3 != op(e4,e1)
| sP52 ),
inference(consistent_polarity_flipping,[],[f169]) ).
fof(f836,plain,
( e1 != op(e3,e4)
| sP54 ),
inference(consistent_polarity_flipping,[],[f161]) ).
fof(f842,plain,
( e2 != op(e3,e1)
| sP57 ),
inference(consistent_polarity_flipping,[],[f145]) ).
fof(f848,plain,
( e3 != op(e2,e4)
| sP59 ),
inference(consistent_polarity_flipping,[],[f134]) ).
fof(f850,plain,
( op(e2,e1) != unit
| sP62 ),
inference(consistent_polarity_flipping,[],[f642]) ).
fof(f855,plain,
( op(e1,e3) != unit
| sP65 ),
inference(consistent_polarity_flipping,[],[f649]) ).
fof(f863,plain,
( e3 != op(e1,e2)
| sP66 ),
inference(consistent_polarity_flipping,[],[f99]) ).
fof(f869,plain,
( e4 != op(unit,e4)
| sP69 ),
inference(consistent_polarity_flipping,[],[f661]) ).
fof(f872,plain,
( e2 != op(unit,e2)
| sP71 ),
inference(consistent_polarity_flipping,[],[f669]) ).
fof(f876,plain,
( e2 != op(e3,op(e2,e3))
| e3 = op(e2,op(e2,e3))
| sP75 ),
inference(consistent_polarity_flipping,[],[f57]) ).
fof(f882,plain,
( e1 != op(unit,op(e1,unit))
| unit = op(e1,op(e1,unit))
| sP78 ),
inference(consistent_polarity_flipping,[],[f689]) ).
fof(f883,plain,
~ sP48,
inference(trivial_inequality_removal,[],[f620]) ).
fof(f888,plain,
( e4 != op(unit,e4)
| e4 != op(e4,unit)
| sP0
| ~ sP1
| ~ sP2
| ~ sP3
| sP4
| ~ sP5
| sP6
| ~ sP7
| ~ sP8
| sP9
| sP10
| sP11
| ~ sP12
| sP13
| ~ sP14
| ~ sP15
| ~ sP16
| sP17
| ~ sP18
| ~ sP19
| sP20
| ~ sP21
| sP22
| sP23
| ~ sP24
| sP25
| sP26
| sP27
| ~ sP28
| sP29
| sP30
| ~ sP31
| sP32
| ~ sP33
| sP34
| sP35
| sP36
| sP37
| sP38
| sP39
| sP40
| ~ sP41
| ~ sP42
| sP43
| ~ sP44
| sP45
| ~ sP46
| ~ sP47
| sP48
| e3 != op(e3,unit)
| e3 != op(unit,e3)
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| unit != op(unit,unit)
| sP49
| sP50
| ~ sP51
| ~ sP52
| sP53
| ~ sP54
| sP55
| sP56
| ~ sP57
| sP58
| ~ sP59
| sP60
| sP61
| ~ sP62
| sP63
| sP64
| ~ sP65
| ~ sP66
| sP67
| sP68
| ~ sP69
| sP70
| ~ sP71
| sP72
| sP73
| sP74
| ~ sP75
| sP76
| sP77
| ~ sP78 ),
inference(duplicate_literal_removal,[],[f710]) ).
fof(f910,definition,
( spl79_1
<=> sP78 ),
introduced(definition,[new_symbols(definition,[spl79_1])],[avatar_definition]) ).
fof(f914,definition,
( spl79_2
<=> unit = op(e1,op(e1,unit)) ),
introduced(definition,[new_symbols(definition,[spl79_2])],[avatar_definition]) ).
fof(f916,plain,
( unit = op(e1,op(e1,unit))
| ~ spl79_2 ),
inference(avatar_component_clause,[],[f914]) ).
fof(f918,definition,
( spl79_3
<=> e1 = op(unit,op(e1,unit)) ),
introduced(definition,[new_symbols(definition,[spl79_3])],[avatar_definition]) ).
fof(f920,plain,
( e1 != op(unit,op(e1,unit))
| spl79_3 ),
inference(avatar_component_clause,[],[f918]) ).
fof(f921,plain,
( spl79_1
| spl79_2
| ~ spl79_3 ),
inference(avatar_split_clause,[],[f882,f918,f914,f910]) ).
fof(f950,definition,
( spl79_10
<=> sP77 ),
introduced(definition,[new_symbols(definition,[spl79_10])],[avatar_definition]) ).
fof(f972,definition,
( spl79_15
<=> e1 = op(e3,op(e3,e1)) ),
introduced(definition,[new_symbols(definition,[spl79_15])],[avatar_definition]) ).
fof(f974,plain,
( e1 = op(e3,op(e3,e1))
| ~ spl79_15 ),
inference(avatar_component_clause,[],[f972]) ).
fof(f976,definition,
( spl79_16
<=> e3 = op(e1,op(e3,e1)) ),
introduced(definition,[new_symbols(definition,[spl79_16])],[avatar_definition]) ).
fof(f978,plain,
( e3 != op(e1,op(e3,e1))
| spl79_16 ),
inference(avatar_component_clause,[],[f976]) ).
fof(f979,plain,
( ~ spl79_10
| spl79_15
| ~ spl79_16 ),
inference(avatar_split_clause,[],[f49,f976,f972,f950]) ).
fof(f990,definition,
( spl79_19
<=> sP76 ),
introduced(definition,[new_symbols(definition,[spl79_19])],[avatar_definition]) ).
fof(f1003,definition,
( spl79_22
<=> e2 = op(e1,op(e1,e2)) ),
introduced(definition,[new_symbols(definition,[spl79_22])],[avatar_definition]) ).
fof(f1005,plain,
( e2 = op(e1,op(e1,e2))
| ~ spl79_22 ),
inference(avatar_component_clause,[],[f1003]) ).
fof(f1007,definition,
( spl79_23
<=> e1 = op(e2,op(e1,e2)) ),
introduced(definition,[new_symbols(definition,[spl79_23])],[avatar_definition]) ).
fof(f1009,plain,
( e1 != op(e2,op(e1,e2))
| spl79_23 ),
inference(avatar_component_clause,[],[f1007]) ).
fof(f1010,plain,
( ~ spl79_19
| spl79_22
| ~ spl79_23 ),
inference(avatar_split_clause,[],[f52,f1007,f1003,f990]) ).
fof(f1030,definition,
( spl79_28
<=> sP75 ),
introduced(definition,[new_symbols(definition,[spl79_28])],[avatar_definition]) ).
fof(f1052,definition,
( spl79_33
<=> e3 = op(e2,op(e2,e3)) ),
introduced(definition,[new_symbols(definition,[spl79_33])],[avatar_definition]) ).
fof(f1054,plain,
( e3 = op(e2,op(e2,e3))
| ~ spl79_33 ),
inference(avatar_component_clause,[],[f1052]) ).
fof(f1056,definition,
( spl79_34
<=> e2 = op(e3,op(e2,e3)) ),
introduced(definition,[new_symbols(definition,[spl79_34])],[avatar_definition]) ).
fof(f1058,plain,
( e2 != op(e3,op(e2,e3))
| spl79_34 ),
inference(avatar_component_clause,[],[f1056]) ).
fof(f1059,plain,
( spl79_28
| spl79_33
| ~ spl79_34 ),
inference(avatar_split_clause,[],[f876,f1056,f1052,f1030]) ).
fof(f1070,definition,
( spl79_37
<=> sP74 ),
introduced(definition,[new_symbols(definition,[spl79_37])],[avatar_definition]) ).
fof(f1101,definition,
( spl79_44
<=> e4 = op(e3,op(e3,e4)) ),
introduced(definition,[new_symbols(definition,[spl79_44])],[avatar_definition]) ).
fof(f1103,plain,
( e4 = op(e3,op(e3,e4))
| ~ spl79_44 ),
inference(avatar_component_clause,[],[f1101]) ).
fof(f1105,definition,
( spl79_45
<=> e3 = op(e4,op(e3,e4)) ),
introduced(definition,[new_symbols(definition,[spl79_45])],[avatar_definition]) ).
fof(f1107,plain,
( e3 != op(e4,op(e3,e4))
| spl79_45 ),
inference(avatar_component_clause,[],[f1105]) ).
fof(f1108,plain,
( ~ spl79_37
| spl79_44
| ~ spl79_45 ),
inference(avatar_split_clause,[],[f62,f1105,f1101,f1070]) ).
fof(f1110,definition,
( spl79_46
<=> sP73 ),
introduced(definition,[new_symbols(definition,[spl79_46])],[avatar_definition]) ).
fof(f1134,definition,
( spl79_51
<=> unit = op(unit,unit) ),
introduced(definition,[new_symbols(definition,[spl79_51])],[avatar_definition]) ).
fof(f1137,plain,
( ~ spl79_46
| ~ spl79_51 ),
inference(avatar_split_clause,[],[f677,f1134,f1110]) ).
fof(f1139,definition,
( spl79_52
<=> sP72 ),
introduced(definition,[new_symbols(definition,[spl79_52])],[avatar_definition]) ).
fof(f1158,definition,
( spl79_56
<=> e1 = op(unit,e1) ),
introduced(definition,[new_symbols(definition,[spl79_56])],[avatar_definition]) ).
fof(f1159,plain,
( e1 = op(unit,e1)
| ~ spl79_56 ),
inference(avatar_component_clause,[],[f1158]) ).
fof(f1161,plain,
( ~ spl79_52
| ~ spl79_56 ),
inference(avatar_split_clause,[],[f673,f1158,f1139]) ).
fof(f1168,definition,
( spl79_58
<=> sP71 ),
introduced(definition,[new_symbols(definition,[spl79_58])],[avatar_definition]) ).
fof(f1182,definition,
( spl79_61
<=> e2 = op(unit,e2) ),
introduced(definition,[new_symbols(definition,[spl79_61])],[avatar_definition]) ).
fof(f1185,plain,
( spl79_58
| ~ spl79_61 ),
inference(avatar_split_clause,[],[f872,f1182,f1168]) ).
fof(f1197,definition,
( spl79_64
<=> sP70 ),
introduced(definition,[new_symbols(definition,[spl79_64])],[avatar_definition]) ).
fof(f1206,definition,
( spl79_66
<=> e3 = op(unit,e3) ),
introduced(definition,[new_symbols(definition,[spl79_66])],[avatar_definition]) ).
fof(f1209,plain,
( ~ spl79_64
| ~ spl79_66 ),
inference(avatar_split_clause,[],[f665,f1206,f1197]) ).
fof(f1226,definition,
( spl79_70
<=> sP69 ),
introduced(definition,[new_symbols(definition,[spl79_70])],[avatar_definition]) ).
fof(f1230,definition,
( spl79_71
<=> e4 = op(unit,e4) ),
introduced(definition,[new_symbols(definition,[spl79_71])],[avatar_definition]) ).
fof(f1233,plain,
( spl79_70
| ~ spl79_71 ),
inference(avatar_split_clause,[],[f869,f1230,f1226]) ).
fof(f1255,definition,
( spl79_76
<=> sP68 ),
introduced(definition,[new_symbols(definition,[spl79_76])],[avatar_definition]) ).
fof(f1274,definition,
( spl79_80
<=> e1 = op(e1,unit) ),
introduced(definition,[new_symbols(definition,[spl79_80])],[avatar_definition]) ).
fof(f1275,plain,
( e1 = op(e1,unit)
| ~ spl79_80 ),
inference(avatar_component_clause,[],[f1274]) ).
fof(f1277,plain,
( ~ spl79_76
| ~ spl79_80 ),
inference(avatar_split_clause,[],[f653,f1274,f1255]) ).
fof(f1284,definition,
( spl79_82
<=> sP67 ),
introduced(definition,[new_symbols(definition,[spl79_82])],[avatar_definition]) ).
fof(f1288,definition,
( spl79_83
<=> e4 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl79_83])],[avatar_definition]) ).
fof(f1289,plain,
( e4 = op(e1,e1)
| ~ spl79_83 ),
inference(avatar_component_clause,[],[f1288]) ).
fof(f1291,plain,
( ~ spl79_82
| ~ spl79_83 ),
inference(avatar_split_clause,[],[f93,f1288,f1284]) ).
fof(f1308,definition,
( spl79_87
<=> op(e1,e1) = unit ),
introduced(definition,[new_symbols(definition,[spl79_87])],[avatar_definition]) ).
fof(f1309,plain,
( op(e1,e1) = unit
| ~ spl79_87 ),
inference(avatar_component_clause,[],[f1308]) ).
fof(f1313,definition,
( spl79_88
<=> sP66 ),
introduced(definition,[new_symbols(definition,[spl79_88])],[avatar_definition]) ).
fof(f1322,definition,
( spl79_90
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl79_90])],[avatar_definition]) ).
fof(f1323,plain,
( e3 = op(e1,e2)
| ~ spl79_90 ),
inference(avatar_component_clause,[],[f1322]) ).
fof(f1325,plain,
( spl79_88
| ~ spl79_90 ),
inference(avatar_split_clause,[],[f863,f1322,f1313]) ).
fof(f1342,definition,
( spl79_94
<=> sP65 ),
introduced(definition,[new_symbols(definition,[spl79_94])],[avatar_definition]) ).
fof(f1366,definition,
( spl79_99
<=> op(e1,e3) = unit ),
introduced(definition,[new_symbols(definition,[spl79_99])],[avatar_definition]) ).
fof(f1367,plain,
( op(e1,e3) = unit
| ~ spl79_99 ),
inference(avatar_component_clause,[],[f1366]) ).
fof(f1369,plain,
( spl79_94
| ~ spl79_99 ),
inference(avatar_split_clause,[],[f855,f1366,f1342]) ).
fof(f1371,definition,
( spl79_100
<=> sP64 ),
introduced(definition,[new_symbols(definition,[spl79_100])],[avatar_definition]) ).
fof(f1385,definition,
( spl79_103
<=> e2 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl79_103])],[avatar_definition]) ).
fof(f1388,plain,
( ~ spl79_100
| ~ spl79_103 ),
inference(avatar_split_clause,[],[f110,f1385,f1371]) ).
fof(f1400,definition,
( spl79_106
<=> sP63 ),
introduced(definition,[new_symbols(definition,[spl79_106])],[avatar_definition]) ).
fof(f1414,definition,
( spl79_109
<=> e2 = op(e2,unit) ),
introduced(definition,[new_symbols(definition,[spl79_109])],[avatar_definition]) ).
fof(f1417,plain,
( ~ spl79_106
| ~ spl79_109 ),
inference(avatar_split_clause,[],[f645,f1414,f1400]) ).
fof(f1429,definition,
( spl79_112
<=> sP62 ),
introduced(definition,[new_symbols(definition,[spl79_112])],[avatar_definition]) ).
fof(f1453,definition,
( spl79_117
<=> op(e2,e1) = unit ),
introduced(definition,[new_symbols(definition,[spl79_117])],[avatar_definition]) ).
fof(f1454,plain,
( op(e2,e1) = unit
| ~ spl79_117 ),
inference(avatar_component_clause,[],[f1453]) ).
fof(f1456,plain,
( spl79_112
| ~ spl79_117 ),
inference(avatar_split_clause,[],[f850,f1453,f1429]) ).
fof(f1458,definition,
( spl79_118
<=> sP61 ),
introduced(definition,[new_symbols(definition,[spl79_118])],[avatar_definition]) ).
fof(f1462,definition,
( spl79_119
<=> e4 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl79_119])],[avatar_definition]) ).
fof(f1465,plain,
( ~ spl79_118
| ~ spl79_119 ),
inference(avatar_split_clause,[],[f123,f1462,f1458]) ).
fof(f1487,definition,
( spl79_124
<=> sP60 ),
introduced(definition,[new_symbols(definition,[spl79_124])],[avatar_definition]) ).
fof(f1506,definition,
( spl79_128
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl79_128])],[avatar_definition]) ).
fof(f1507,plain,
( e1 = op(e2,e3)
| ~ spl79_128 ),
inference(avatar_component_clause,[],[f1506]) ).
fof(f1509,plain,
( ~ spl79_124
| ~ spl79_128 ),
inference(avatar_split_clause,[],[f131,f1506,f1487]) ).
fof(f1516,definition,
( spl79_130
<=> sP59 ),
introduced(definition,[new_symbols(definition,[spl79_130])],[avatar_definition]) ).
fof(f1525,definition,
( spl79_132
<=> e3 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl79_132])],[avatar_definition]) ).
fof(f1528,plain,
( spl79_130
| ~ spl79_132 ),
inference(avatar_split_clause,[],[f848,f1525,f1516]) ).
fof(f1545,definition,
( spl79_136
<=> sP58 ),
introduced(definition,[new_symbols(definition,[spl79_136])],[avatar_definition]) ).
fof(f1554,definition,
( spl79_138
<=> e3 = op(e3,unit) ),
introduced(definition,[new_symbols(definition,[spl79_138])],[avatar_definition]) ).
fof(f1557,plain,
( ~ spl79_136
| ~ spl79_138 ),
inference(avatar_split_clause,[],[f637,f1554,f1545]) ).
fof(f1574,definition,
( spl79_142
<=> sP57 ),
introduced(definition,[new_symbols(definition,[spl79_142])],[avatar_definition]) ).
fof(f1578,definition,
( spl79_143
<=> e4 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl79_143])],[avatar_definition]) ).
fof(f1579,plain,
( e4 = op(e3,e1)
| ~ spl79_143 ),
inference(avatar_component_clause,[],[f1578]) ).
fof(f1588,definition,
( spl79_145
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl79_145])],[avatar_definition]) ).
fof(f1589,plain,
( e2 = op(e3,e1)
| ~ spl79_145 ),
inference(avatar_component_clause,[],[f1588]) ).
fof(f1591,plain,
( spl79_142
| ~ spl79_145 ),
inference(avatar_split_clause,[],[f842,f1588,f1574]) ).
fof(f1603,definition,
( spl79_148
<=> sP56 ),
introduced(definition,[new_symbols(definition,[spl79_148])],[avatar_definition]) ).
fof(f1627,definition,
( spl79_153
<=> op(e3,e2) = unit ),
introduced(definition,[new_symbols(definition,[spl79_153])],[avatar_definition]) ).
fof(f1628,plain,
( op(e3,e2) = unit
| ~ spl79_153 ),
inference(avatar_component_clause,[],[f1627]) ).
fof(f1630,plain,
( ~ spl79_148
| ~ spl79_153 ),
inference(avatar_split_clause,[],[f632,f1627,f1603]) ).
fof(f1632,definition,
( spl79_154
<=> sP55 ),
introduced(definition,[new_symbols(definition,[spl79_154])],[avatar_definition]) ).
fof(f1636,definition,
( spl79_155
<=> e4 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl79_155])],[avatar_definition]) ).
fof(f1639,plain,
( ~ spl79_154
| ~ spl79_155 ),
inference(avatar_split_clause,[],[f153,f1636,f1632]) ).
fof(f1661,definition,
( spl79_160
<=> sP54 ),
introduced(definition,[new_symbols(definition,[spl79_160])],[avatar_definition]) ).
fof(f1680,definition,
( spl79_164
<=> e1 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl79_164])],[avatar_definition]) ).
fof(f1681,plain,
( e1 = op(e3,e4)
| ~ spl79_164 ),
inference(avatar_component_clause,[],[f1680]) ).
fof(f1683,plain,
( spl79_160
| ~ spl79_164 ),
inference(avatar_split_clause,[],[f836,f1680,f1661]) ).
fof(f1690,definition,
( spl79_166
<=> sP53 ),
introduced(definition,[new_symbols(definition,[spl79_166])],[avatar_definition]) ).
fof(f1694,definition,
( spl79_167
<=> e4 = op(e4,unit) ),
introduced(definition,[new_symbols(definition,[spl79_167])],[avatar_definition]) ).
fof(f1697,plain,
( ~ spl79_166
| ~ spl79_167 ),
inference(avatar_split_clause,[],[f629,f1694,f1690]) ).
fof(f1719,definition,
( spl79_172
<=> sP52 ),
introduced(definition,[new_symbols(definition,[spl79_172])],[avatar_definition]) ).
fof(f1728,definition,
( spl79_174
<=> e3 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl79_174])],[avatar_definition]) ).
fof(f1729,plain,
( e3 = op(e4,e1)
| ~ spl79_174 ),
inference(avatar_component_clause,[],[f1728]) ).
fof(f1731,plain,
( spl79_172
| ~ spl79_174 ),
inference(avatar_split_clause,[],[f833,f1728,f1719]) ).
fof(f1748,definition,
( spl79_178
<=> sP51 ),
introduced(definition,[new_symbols(definition,[spl79_178])],[avatar_definition]) ).
fof(f1767,definition,
( spl79_182
<=> e1 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl79_182])],[avatar_definition]) ).
fof(f1770,plain,
( spl79_178
| ~ spl79_182 ),
inference(avatar_split_clause,[],[f826,f1767,f1748]) ).
fof(f1777,definition,
( spl79_184
<=> sP50 ),
introduced(definition,[new_symbols(definition,[spl79_184])],[avatar_definition]) ).
fof(f1791,definition,
( spl79_187
<=> e2 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl79_187])],[avatar_definition]) ).
fof(f1794,plain,
( ~ spl79_184
| ~ spl79_187 ),
inference(avatar_split_clause,[],[f180,f1791,f1777]) ).
fof(f1806,definition,
( spl79_190
<=> sP49 ),
introduced(definition,[new_symbols(definition,[spl79_190])],[avatar_definition]) ).
fof(f1830,definition,
( spl79_195
<=> op(e4,e4) = unit ),
introduced(definition,[new_symbols(definition,[spl79_195])],[avatar_definition]) ).
fof(f1833,plain,
( ~ spl79_190
| ~ spl79_195 ),
inference(avatar_split_clause,[],[f621,f1830,f1806]) ).
fof(f1835,definition,
( spl79_196
<=> sP48 ),
introduced(definition,[new_symbols(definition,[spl79_196])],[avatar_definition]) ).
fof(f1839,definition,
( spl79_197
<=> e4 = unit ),
introduced(definition,[new_symbols(definition,[spl79_197])],[avatar_definition]) ).
fof(f1841,plain,
( e4 != unit
| spl79_197 ),
inference(avatar_component_clause,[],[f1839]) ).
fof(f1844,definition,
( spl79_198
<=> e3 = unit ),
introduced(definition,[new_symbols(definition,[spl79_198])],[avatar_definition]) ).
fof(f1846,plain,
( e3 != unit
| spl79_198 ),
inference(avatar_component_clause,[],[f1844]) ).
fof(f1849,definition,
( spl79_199
<=> e2 = unit ),
introduced(definition,[new_symbols(definition,[spl79_199])],[avatar_definition]) ).
fof(f1851,plain,
( e2 != unit
| spl79_199 ),
inference(avatar_component_clause,[],[f1849]) ).
fof(f1854,definition,
( spl79_200
<=> e1 = unit ),
introduced(definition,[new_symbols(definition,[spl79_200])],[avatar_definition]) ).
fof(f1856,plain,
( e1 != unit
| spl79_200 ),
inference(avatar_component_clause,[],[f1854]) ).
fof(f1858,plain,
~ spl79_196,
inference(avatar_split_clause,[],[f883,f1835]) ).
fof(f1860,definition,
( spl79_201
<=> sP47 ),
introduced(definition,[new_symbols(definition,[spl79_201])],[avatar_definition]) ).
fof(f1867,plain,
( spl79_201
| ~ spl79_51 ),
inference(avatar_split_clause,[],[f820,f1134,f1860]) ).
fof(f1869,definition,
( spl79_202
<=> sP46 ),
introduced(definition,[new_symbols(definition,[spl79_202])],[avatar_definition]) ).
fof(f1876,plain,
( spl79_202
| ~ spl79_51 ),
inference(avatar_split_clause,[],[f815,f1134,f1869]) ).
fof(f1878,definition,
( spl79_203
<=> sP45 ),
introduced(definition,[new_symbols(definition,[spl79_203])],[avatar_definition]) ).
fof(f1884,plain,
( ~ spl79_203
| ~ spl79_56 ),
inference(avatar_split_clause,[],[f606,f1158,f1878]) ).
fof(f1887,definition,
( spl79_204
<=> sP44 ),
introduced(definition,[new_symbols(definition,[spl79_204])],[avatar_definition]) ).
fof(f1893,plain,
( spl79_204
| ~ spl79_80 ),
inference(avatar_split_clause,[],[f811,f1274,f1887]) ).
fof(f1896,definition,
( spl79_205
<=> sP43 ),
introduced(definition,[new_symbols(definition,[spl79_205])],[avatar_definition]) ).
fof(f1901,plain,
( ~ spl79_205
| ~ spl79_61 ),
inference(avatar_split_clause,[],[f597,f1182,f1896]) ).
fof(f1905,definition,
( spl79_206
<=> sP42 ),
introduced(definition,[new_symbols(definition,[spl79_206])],[avatar_definition]) ).
fof(f1910,plain,
( spl79_206
| ~ spl79_109 ),
inference(avatar_split_clause,[],[f807,f1414,f1905]) ).
fof(f1914,definition,
( spl79_207
<=> sP41 ),
introduced(definition,[new_symbols(definition,[spl79_207])],[avatar_definition]) ).
fof(f1918,plain,
( spl79_207
| ~ spl79_66 ),
inference(avatar_split_clause,[],[f803,f1206,f1914]) ).
fof(f1923,definition,
( spl79_208
<=> sP40 ),
introduced(definition,[new_symbols(definition,[spl79_208])],[avatar_definition]) ).
fof(f1927,plain,
( ~ spl79_208
| ~ spl79_138 ),
inference(avatar_split_clause,[],[f583,f1554,f1923]) ).
fof(f1932,definition,
( spl79_209
<=> sP39 ),
introduced(definition,[new_symbols(definition,[spl79_209])],[avatar_definition]) ).
fof(f1935,plain,
( ~ spl79_209
| ~ spl79_71 ),
inference(avatar_split_clause,[],[f579,f1230,f1932]) ).
fof(f1941,definition,
( spl79_210
<=> sP38 ),
introduced(definition,[new_symbols(definition,[spl79_210])],[avatar_definition]) ).
fof(f1944,plain,
( ~ spl79_210
| ~ spl79_167 ),
inference(avatar_split_clause,[],[f574,f1694,f1941]) ).
fof(f1950,definition,
( spl79_211
<=> sP37 ),
introduced(definition,[new_symbols(definition,[spl79_211])],[avatar_definition]) ).
fof(f1954,plain,
( ~ spl79_211
| ~ spl79_99 ),
inference(avatar_split_clause,[],[f568,f1366,f1950]) ).
fof(f1959,definition,
( spl79_212
<=> sP36 ),
introduced(definition,[new_symbols(definition,[spl79_212])],[avatar_definition]) ).
fof(f1964,plain,
( ~ spl79_212
| ~ spl79_117 ),
inference(avatar_split_clause,[],[f562,f1453,f1959]) ).
fof(f1968,definition,
( spl79_213
<=> sP35 ),
introduced(definition,[new_symbols(definition,[spl79_213])],[avatar_definition]) ).
fof(f1975,plain,
( ~ spl79_213
| ~ spl79_80 ),
inference(avatar_split_clause,[],[f559,f1274,f1968]) ).
fof(f1977,definition,
( spl79_214
<=> sP34 ),
introduced(definition,[new_symbols(definition,[spl79_214])],[avatar_definition]) ).
fof(f1984,plain,
( ~ spl79_214
| ~ spl79_56 ),
inference(avatar_split_clause,[],[f558,f1158,f1977]) ).
fof(f1986,definition,
( spl79_215
<=> sP33 ),
introduced(definition,[new_symbols(definition,[spl79_215])],[avatar_definition]) ).
fof(f1989,plain,
( spl79_215
| ~ spl79_103 ),
inference(avatar_split_clause,[],[f799,f1385,f1986]) ).
fof(f1995,definition,
( spl79_216
<=> sP32 ),
introduced(definition,[new_symbols(definition,[spl79_216])],[avatar_definition]) ).
fof(f1999,plain,
( ~ spl79_216
| ~ spl79_145 ),
inference(avatar_split_clause,[],[f269,f1588,f1995]) ).
fof(f2004,definition,
( spl79_217
<=> sP31 ),
introduced(definition,[new_symbols(definition,[spl79_217])],[avatar_definition]) ).
fof(f2009,plain,
( spl79_217
| ~ spl79_90 ),
inference(avatar_split_clause,[],[f792,f1322,f2004]) ).
fof(f2013,definition,
( spl79_218
<=> sP30 ),
introduced(definition,[new_symbols(definition,[spl79_218])],[avatar_definition]) ).
fof(f2016,plain,
( ~ spl79_218
| ~ spl79_174 ),
inference(avatar_split_clause,[],[f278,f1728,f2013]) ).
fof(f2022,definition,
( spl79_219
<=> sP29 ),
introduced(definition,[new_symbols(definition,[spl79_219])],[avatar_definition]) ).
fof(f2028,plain,
( ~ spl79_219
| ~ spl79_83 ),
inference(avatar_split_clause,[],[f286,f1288,f2022]) ).
fof(f2031,definition,
( spl79_220
<=> sP28 ),
introduced(definition,[new_symbols(definition,[spl79_220])],[avatar_definition]) ).
fof(f2037,plain,
( spl79_220
| ~ spl79_83 ),
inference(avatar_split_clause,[],[f786,f1288,f2031]) ).
fof(f2040,definition,
( spl79_221
<=> sP27 ),
introduced(definition,[new_symbols(definition,[spl79_221])],[avatar_definition]) ).
fof(f2046,plain,
( ~ spl79_221
| ~ spl79_117 ),
inference(avatar_split_clause,[],[f548,f1453,f2040]) ).
fof(f2049,definition,
( spl79_222
<=> sP26 ),
introduced(definition,[new_symbols(definition,[spl79_222])],[avatar_definition]) ).
fof(f2053,plain,
( ~ spl79_222
| ~ spl79_153 ),
inference(avatar_split_clause,[],[f545,f1627,f2049]) ).
fof(f2058,definition,
( spl79_223
<=> sP25 ),
introduced(definition,[new_symbols(definition,[spl79_223])],[avatar_definition]) ).
fof(f2062,plain,
( ~ spl79_223
| ~ spl79_128 ),
inference(avatar_split_clause,[],[f304,f1506,f2058]) ).
fof(f2067,definition,
( spl79_224
<=> sP24 ),
introduced(definition,[new_symbols(definition,[spl79_224])],[avatar_definition]) ).
fof(f2070,plain,
( spl79_224
| ~ spl79_182 ),
inference(avatar_split_clause,[],[f784,f1767,f2067]) ).
fof(f2076,definition,
( spl79_225
<=> sP23 ),
introduced(definition,[new_symbols(definition,[spl79_225])],[avatar_definition]) ).
fof(f2083,plain,
( ~ spl79_225
| ~ spl79_109 ),
inference(avatar_split_clause,[],[f539,f1414,f2076]) ).
fof(f2085,definition,
( spl79_226
<=> sP22 ),
introduced(definition,[new_symbols(definition,[spl79_226])],[avatar_definition]) ).
fof(f2092,plain,
( ~ spl79_226
| ~ spl79_61 ),
inference(avatar_split_clause,[],[f538,f1182,f2085]) ).
fof(f2094,definition,
( spl79_227
<=> sP21 ),
introduced(definition,[new_symbols(definition,[spl79_227])],[avatar_definition]) ).
fof(f2097,plain,
( spl79_227
| ~ spl79_132 ),
inference(avatar_split_clause,[],[f779,f1525,f2094]) ).
fof(f2103,definition,
( spl79_228
<=> sP20 ),
introduced(definition,[new_symbols(definition,[spl79_228])],[avatar_definition]) ).
fof(f2109,plain,
( ~ spl79_228
| ~ spl79_90 ),
inference(avatar_split_clause,[],[f331,f1322,f2103]) ).
fof(f2112,definition,
( spl79_229
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl79_229])],[avatar_definition]) ).
fof(f2117,plain,
( spl79_229
| ~ spl79_119 ),
inference(avatar_split_clause,[],[f772,f1462,f2112]) ).
fof(f2121,definition,
( spl79_230
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl79_230])],[avatar_definition]) ).
fof(f2126,plain,
( spl79_230
| ~ spl79_119 ),
inference(avatar_split_clause,[],[f767,f1462,f2121]) ).
fof(f2130,definition,
( spl79_231
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl79_231])],[avatar_definition]) ).
fof(f2135,plain,
( ~ spl79_231
| ~ spl79_153 ),
inference(avatar_split_clause,[],[f531,f1627,f2130]) ).
fof(f2139,definition,
( spl79_232
<=> sP16 ),
introduced(definition,[new_symbols(definition,[spl79_232])],[avatar_definition]) ).
fof(f2145,plain,
( spl79_232
| ~ spl79_99 ),
inference(avatar_split_clause,[],[f761,f1366,f2139]) ).
fof(f2148,definition,
( spl79_233
<=> sP15 ),
introduced(definition,[new_symbols(definition,[spl79_233])],[avatar_definition]) ).
fof(f2151,plain,
( spl79_233
| ~ spl79_164 ),
inference(avatar_split_clause,[],[f759,f1680,f2148]) ).
fof(f2157,definition,
( spl79_234
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl79_234])],[avatar_definition]) ).
fof(f2162,plain,
( spl79_234
| ~ spl79_128 ),
inference(avatar_split_clause,[],[f752,f1506,f2157]) ).
fof(f2166,definition,
( spl79_235
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl79_235])],[avatar_definition]) ).
fof(f2172,plain,
( ~ spl79_235
| ~ spl79_145 ),
inference(avatar_split_clause,[],[f366,f1588,f2166]) ).
fof(f2175,definition,
( spl79_236
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl79_236])],[avatar_definition]) ).
fof(f2178,plain,
( spl79_236
| ~ spl79_187 ),
inference(avatar_split_clause,[],[f749,f1791,f2175]) ).
fof(f2184,definition,
( spl79_237
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl79_237])],[avatar_definition]) ).
fof(f2191,plain,
( ~ spl79_237
| ~ spl79_138 ),
inference(avatar_split_clause,[],[f519,f1554,f2184]) ).
fof(f2193,definition,
( spl79_238
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl79_238])],[avatar_definition]) ).
fof(f2200,plain,
( ~ spl79_238
| ~ spl79_66 ),
inference(avatar_split_clause,[],[f518,f1206,f2193]) ).
fof(f2202,definition,
( spl79_239
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl79_239])],[avatar_definition]) ).
fof(f2206,plain,
( ~ spl79_239
| ~ spl79_155 ),
inference(avatar_split_clause,[],[f384,f1636,f2202]) ).
fof(f2211,definition,
( spl79_240
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl79_240])],[avatar_definition]) ).
fof(f2215,plain,
( spl79_240
| ~ spl79_155 ),
inference(avatar_split_clause,[],[f743,f1636,f2211]) ).
fof(f2220,definition,
( spl79_241
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl79_241])],[avatar_definition]) ).
fof(f2223,plain,
( spl79_241
| ~ spl79_195 ),
inference(avatar_split_clause,[],[f739,f1830,f2220]) ).
fof(f2229,definition,
( spl79_242
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl79_242])],[avatar_definition]) ).
fof(f2232,plain,
( ~ spl79_242
| ~ spl79_195 ),
inference(avatar_split_clause,[],[f510,f1830,f2229]) ).
fof(f2238,definition,
( spl79_243
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl79_243])],[avatar_definition]) ).
fof(f2243,plain,
( spl79_243
| ~ spl79_182 ),
inference(avatar_split_clause,[],[f732,f1767,f2238]) ).
fof(f2247,definition,
( spl79_244
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl79_244])],[avatar_definition]) ).
fof(f2251,plain,
( ~ spl79_244
| ~ spl79_164 ),
inference(avatar_split_clause,[],[f409,f1680,f2247]) ).
fof(f2256,definition,
( spl79_245
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl79_245])],[avatar_definition]) ).
fof(f2260,plain,
( spl79_245
| ~ spl79_187 ),
inference(avatar_split_clause,[],[f728,f1791,f2256]) ).
fof(f2265,definition,
( spl79_246
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl79_246])],[avatar_definition]) ).
fof(f2271,plain,
( spl79_246
| ~ spl79_103 ),
inference(avatar_split_clause,[],[f721,f1385,f2265]) ).
fof(f2274,definition,
( spl79_247
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl79_247])],[avatar_definition]) ).
fof(f2280,plain,
( spl79_247
| ~ spl79_174 ),
inference(avatar_split_clause,[],[f716,f1728,f2274]) ).
fof(f2283,definition,
( spl79_248
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl79_248])],[avatar_definition]) ).
fof(f2288,plain,
( ~ spl79_248
| ~ spl79_132 ),
inference(avatar_split_clause,[],[f430,f1525,f2283]) ).
fof(f2295,plain,
( ~ spl79_1
| spl79_10
| spl79_19
| ~ spl79_28
| spl79_37
| spl79_46
| spl79_52
| ~ spl79_58
| spl79_64
| ~ spl79_70
| spl79_76
| spl79_82
| ~ spl79_88
| ~ spl79_94
| spl79_100
| spl79_106
| ~ spl79_112
| spl79_118
| spl79_124
| ~ spl79_130
| spl79_136
| ~ spl79_142
| spl79_148
| spl79_154
| ~ spl79_160
| spl79_166
| ~ spl79_172
| ~ spl79_178
| spl79_184
| spl79_190
| ~ spl79_51
| ~ spl79_56
| ~ spl79_80
| ~ spl79_61
| ~ spl79_109
| ~ spl79_66
| ~ spl79_138
| spl79_196
| ~ spl79_201
| ~ spl79_202
| spl79_203
| ~ spl79_204
| spl79_205
| ~ spl79_206
| ~ spl79_207
| spl79_208
| spl79_209
| spl79_210
| spl79_211
| spl79_212
| spl79_213
| spl79_214
| ~ spl79_215
| spl79_216
| ~ spl79_217
| spl79_218
| spl79_219
| ~ spl79_220
| spl79_221
| spl79_222
| spl79_223
| ~ spl79_224
| spl79_225
| spl79_226
| ~ spl79_227
| spl79_228
| ~ spl79_229
| ~ spl79_230
| spl79_231
| ~ spl79_232
| ~ spl79_233
| ~ spl79_234
| spl79_235
| ~ spl79_236
| spl79_237
| spl79_238
| spl79_239
| ~ spl79_240
| ~ spl79_241
| spl79_242
| ~ spl79_243
| spl79_244
| ~ spl79_245
| ~ spl79_246
| ~ spl79_247
| spl79_248
| ~ spl79_167
| ~ spl79_71 ),
inference(avatar_split_clause,[],[f888,f1230,f1694,f2283,f2274,f2265,f2256,f2247,f2238,f2229,f2220,f2211,f2202,f2193,f2184,f2175,f2166,f2157,f2148,f2139,f2130,f2121,f2112,f2103,f2094,f2085,f2076,f2067,f2058,f2049,f2040,f2031,f2022,f2013,f2004,f1995,f1986,f1977,f1968,f1959,f1950,f1941,f1932,f1923,f1914,f1905,f1896,f1887,f1878,f1869,f1860,f1835,f1554,f1206,f1414,f1182,f1274,f1158,f1134,f1806,f1777,f1748,f1719,f1690,f1661,f1632,f1603,f1574,f1545,f1516,f1487,f1458,f1429,f1400,f1371,f1342,f1313,f1284,f1255,f1226,f1197,f1168,f1139,f1110,f1070,f1030,f990,f950,f910]) ).
fof(f2316,plain,
spl79_195,
inference(avatar_split_clause,[],[f474,f1830]) ).
fof(f2317,plain,
spl79_187,
inference(avatar_split_clause,[],[f18,f1791]) ).
fof(f2318,plain,
spl79_182,
inference(avatar_split_clause,[],[f19,f1767]) ).
fof(f2319,plain,
spl79_174,
inference(avatar_split_clause,[],[f20,f1728]) ).
fof(f2320,plain,
spl79_167,
inference(avatar_split_clause,[],[f473,f1694]) ).
fof(f2321,plain,
spl79_164,
inference(avatar_split_clause,[],[f22,f1680]) ).
fof(f2322,plain,
spl79_155,
inference(avatar_split_clause,[],[f23,f1636]) ).
fof(f2323,plain,
spl79_153,
inference(avatar_split_clause,[],[f472,f1627]) ).
fof(f2324,plain,
spl79_145,
inference(avatar_split_clause,[],[f25,f1588]) ).
fof(f2325,plain,
spl79_138,
inference(avatar_split_clause,[],[f471,f1554]) ).
fof(f2326,plain,
spl79_132,
inference(avatar_split_clause,[],[f27,f1525]) ).
fof(f2327,plain,
spl79_128,
inference(avatar_split_clause,[],[f28,f1506]) ).
fof(f2328,plain,
spl79_119,
inference(avatar_split_clause,[],[f29,f1462]) ).
fof(f2329,plain,
spl79_117,
inference(avatar_split_clause,[],[f470,f1453]) ).
fof(f2330,plain,
spl79_109,
inference(avatar_split_clause,[],[f469,f1414]) ).
fof(f2331,plain,
spl79_103,
inference(avatar_split_clause,[],[f32,f1385]) ).
fof(f2332,plain,
spl79_99,
inference(avatar_split_clause,[],[f468,f1366]) ).
fof(f2333,plain,
spl79_90,
inference(avatar_split_clause,[],[f34,f1322]) ).
fof(f2334,plain,
spl79_83,
inference(avatar_split_clause,[],[f35,f1288]) ).
fof(f2335,plain,
spl79_80,
inference(avatar_split_clause,[],[f467,f1274]) ).
fof(f2336,plain,
spl79_71,
inference(avatar_split_clause,[],[f466,f1230]) ).
fof(f2337,plain,
spl79_66,
inference(avatar_split_clause,[],[f465,f1206]) ).
fof(f2338,plain,
spl79_61,
inference(avatar_split_clause,[],[f464,f1182]) ).
fof(f2339,plain,
spl79_56,
inference(avatar_split_clause,[],[f463,f1158]) ).
fof(f2340,plain,
spl79_51,
inference(avatar_split_clause,[],[f462,f1134]) ).
fof(f2341,plain,
~ spl79_197,
inference(avatar_split_clause,[],[f461,f1839]) ).
fof(f2342,plain,
~ spl79_198,
inference(avatar_split_clause,[],[f460,f1844]) ).
fof(f2343,plain,
~ spl79_199,
inference(avatar_split_clause,[],[f459,f1849]) ).
fof(f2344,plain,
~ spl79_200,
inference(avatar_split_clause,[],[f458,f1854]) ).
fof(f2345,plain,
( e1 != op(unit,e1)
| spl79_3
| ~ spl79_80 ),
inference(forward_demodulation,[],[f920,f1275]) ).
fof(f2346,plain,
( $false
| spl79_3
| ~ spl79_56
| ~ spl79_80 ),
inference(forward_subsumption_resolution,[],[f2345,f1159]) ).
fof(f2347,plain,
( spl79_3
| ~ spl79_56
| ~ spl79_80 ),
inference(avatar_contradiction_clause,[],[f2346]) ).
fof(f2367,plain,
( e2 != op(e3,e1)
| spl79_34
| ~ spl79_128 ),
inference(forward_demodulation,[],[f1058,f1507]) ).
fof(f2368,plain,
( $false
| spl79_34
| ~ spl79_128
| ~ spl79_145 ),
inference(forward_subsumption_resolution,[],[f2367,f1589]) ).
fof(f2369,plain,
( spl79_34
| ~ spl79_128
| ~ spl79_145 ),
inference(avatar_contradiction_clause,[],[f2368]) ).
fof(f2371,plain,
( e1 != op(e2,e3)
| spl79_23
| ~ spl79_90 ),
inference(forward_demodulation,[],[f1009,f1323]) ).
fof(f2376,plain,
( $false
| spl79_23
| ~ spl79_90
| ~ spl79_128 ),
inference(forward_subsumption_resolution,[],[f2371,f1507]) ).
fof(f2377,plain,
( spl79_23
| ~ spl79_90
| ~ spl79_128 ),
inference(avatar_contradiction_clause,[],[f2376]) ).
fof(f2380,plain,
( e2 = op(e1,e3)
| ~ spl79_22
| ~ spl79_90 ),
inference(forward_demodulation,[],[f1005,f1323]) ).
fof(f2382,plain,
( e2 = unit
| ~ spl79_22
| ~ spl79_90
| ~ spl79_99 ),
inference(forward_demodulation,[],[f2380,f1367]) ).
fof(f2383,plain,
( $false
| ~ spl79_22
| ~ spl79_90
| ~ spl79_99
| spl79_199 ),
inference(forward_subsumption_resolution,[],[f2382,f1851]) ).
fof(f2384,plain,
( ~ spl79_22
| ~ spl79_90
| ~ spl79_99
| spl79_199 ),
inference(avatar_contradiction_clause,[],[f2383]) ).
fof(f2386,plain,
( e3 = op(e2,e1)
| ~ spl79_33
| ~ spl79_128 ),
inference(forward_demodulation,[],[f1054,f1507]) ).
fof(f2388,plain,
( e3 = unit
| ~ spl79_33
| ~ spl79_117
| ~ spl79_128 ),
inference(forward_demodulation,[],[f2386,f1454]) ).
fof(f2389,plain,
( $false
| ~ spl79_33
| ~ spl79_117
| ~ spl79_128
| spl79_198 ),
inference(forward_subsumption_resolution,[],[f2388,f1846]) ).
fof(f2390,plain,
( ~ spl79_33
| ~ spl79_117
| ~ spl79_128
| spl79_198 ),
inference(avatar_contradiction_clause,[],[f2389]) ).
fof(f2395,plain,
( e3 != op(e4,e1)
| spl79_45
| ~ spl79_164 ),
inference(forward_demodulation,[],[f1107,f1681]) ).
fof(f2403,plain,
( $false
| spl79_45
| ~ spl79_164
| ~ spl79_174 ),
inference(forward_subsumption_resolution,[],[f2395,f1729]) ).
fof(f2404,plain,
( spl79_45
| ~ spl79_164
| ~ spl79_174 ),
inference(avatar_contradiction_clause,[],[f2403]) ).
fof(f2411,plain,
( e4 = op(e3,e1)
| ~ spl79_44
| ~ spl79_164 ),
inference(forward_demodulation,[],[f1103,f1681]) ).
fof(f2415,plain,
( spl79_143
| ~ spl79_44
| ~ spl79_164 ),
inference(avatar_split_clause,[],[f2411,f1680,f1101,f1578]) ).
fof(f2421,plain,
( e2 = e4
| ~ spl79_143
| ~ spl79_145 ),
inference(superposition,[],[f1579,f1589]) ).
fof(f2427,plain,
( op(e1,e1) = unit
| ~ spl79_2
| ~ spl79_80 ),
inference(forward_demodulation,[],[f916,f1275]) ).
fof(f2432,plain,
( spl79_87
| ~ spl79_2
| ~ spl79_80 ),
inference(avatar_split_clause,[],[f2427,f1274,f914,f1308]) ).
fof(f2448,plain,
( $false
| ~ spl79_143
| ~ spl79_145 ),
inference(forward_subsumption_resolution,[],[f2421,f8]) ).
fof(f2449,plain,
( ~ spl79_143
| ~ spl79_145 ),
inference(avatar_contradiction_clause,[],[f2448]) ).
fof(f2452,plain,
( e4 = unit
| ~ spl79_83
| ~ spl79_87 ),
inference(superposition,[],[f1309,f1289]) ).
fof(f2456,plain,
( $false
| ~ spl79_83
| ~ spl79_87
| spl79_197 ),
inference(forward_subsumption_resolution,[],[f2452,f1841]) ).
fof(f2457,plain,
( ~ spl79_83
| ~ spl79_87
| spl79_197 ),
inference(avatar_contradiction_clause,[],[f2456]) ).
fof(f2461,plain,
( e3 != op(e1,e2)
| spl79_16
| ~ spl79_145 ),
inference(forward_demodulation,[],[f978,f1589]) ).
fof(f2466,plain,
( $false
| spl79_16
| ~ spl79_90
| ~ spl79_145 ),
inference(forward_subsumption_resolution,[],[f2461,f1323]) ).
fof(f2467,plain,
( spl79_16
| ~ spl79_90
| ~ spl79_145 ),
inference(avatar_contradiction_clause,[],[f2466]) ).
fof(f2469,plain,
( e1 = op(e3,e2)
| ~ spl79_15
| ~ spl79_145 ),
inference(forward_demodulation,[],[f974,f1589]) ).
fof(f2471,plain,
( e1 = unit
| ~ spl79_15
| ~ spl79_145
| ~ spl79_153 ),
inference(forward_demodulation,[],[f2469,f1628]) ).
fof(f2472,plain,
( $false
| ~ spl79_15
| ~ spl79_145
| ~ spl79_153
| spl79_200 ),
inference(forward_subsumption_resolution,[],[f2471,f1856]) ).
fof(f2473,plain,
( ~ spl79_15
| ~ spl79_145
| ~ spl79_153
| spl79_200 ),
inference(avatar_contradiction_clause,[],[f2472]) ).
cnf(s1,plain,
( spl79_1
| spl79_2
| ~ spl79_3 ),
inference(sat_conversion,[],[f921]) ).
cnf(s7,plain,
( ~ spl79_10
| spl79_15
| ~ spl79_16 ),
inference(sat_conversion,[],[f979]) ).
cnf(s10,plain,
( ~ spl79_19
| spl79_22
| ~ spl79_23 ),
inference(sat_conversion,[],[f1010]) ).
cnf(s15,plain,
( spl79_28
| spl79_33
| ~ spl79_34 ),
inference(sat_conversion,[],[f1059]) ).
cnf(s20,plain,
( ~ spl79_37
| spl79_44
| ~ spl79_45 ),
inference(sat_conversion,[],[f1108]) ).
cnf(s25,plain,
( ~ spl79_46
| ~ spl79_51 ),
inference(sat_conversion,[],[f1137]) ).
cnf(s29,plain,
( ~ spl79_52
| ~ spl79_56 ),
inference(sat_conversion,[],[f1161]) ).
cnf(s33,plain,
( spl79_58
| ~ spl79_61 ),
inference(sat_conversion,[],[f1185]) ).
cnf(s37,plain,
( ~ spl79_64
| ~ spl79_66 ),
inference(sat_conversion,[],[f1209]) ).
cnf(s41,plain,
( spl79_70
| ~ spl79_71 ),
inference(sat_conversion,[],[f1233]) ).
cnf(s49,plain,
( ~ spl79_76
| ~ spl79_80 ),
inference(sat_conversion,[],[f1277]) ).
cnf(s51,plain,
( ~ spl79_82
| ~ spl79_83 ),
inference(sat_conversion,[],[f1291]) ).
cnf(s57,plain,
( spl79_88
| ~ spl79_90 ),
inference(sat_conversion,[],[f1325]) ).
cnf(s65,plain,
( spl79_94
| ~ spl79_99 ),
inference(sat_conversion,[],[f1369]) ).
cnf(s68,plain,
( ~ spl79_100
| ~ spl79_103 ),
inference(sat_conversion,[],[f1388]) ).
cnf(s73,plain,
( ~ spl79_106
| ~ spl79_109 ),
inference(sat_conversion,[],[f1417]) ).
cnf(s80,plain,
( spl79_112
| ~ spl79_117 ),
inference(sat_conversion,[],[f1456]) ).
cnf(s81,plain,
( ~ spl79_118
| ~ spl79_119 ),
inference(sat_conversion,[],[f1465]) ).
cnf(s89,plain,
( ~ spl79_124
| ~ spl79_128 ),
inference(sat_conversion,[],[f1509]) ).
cnf(s92,plain,
( spl79_130
| ~ spl79_132 ),
inference(sat_conversion,[],[f1528]) ).
cnf(s97,plain,
( ~ spl79_136
| ~ spl79_138 ),
inference(sat_conversion,[],[f1557]) ).
cnf(s103,plain,
( spl79_142
| ~ spl79_145 ),
inference(sat_conversion,[],[f1591]) ).
cnf(s110,plain,
( ~ spl79_148
| ~ spl79_153 ),
inference(sat_conversion,[],[f1630]) ).
cnf(s111,plain,
( ~ spl79_154
| ~ spl79_155 ),
inference(sat_conversion,[],[f1639]) ).
cnf(s119,plain,
( spl79_160
| ~ spl79_164 ),
inference(sat_conversion,[],[f1683]) ).
cnf(s121,plain,
( ~ spl79_166
| ~ spl79_167 ),
inference(sat_conversion,[],[f1697]) ).
cnf(s127,plain,
( spl79_172
| ~ spl79_174 ),
inference(sat_conversion,[],[f1731]) ).
cnf(s134,plain,
( spl79_178
| ~ spl79_182 ),
inference(sat_conversion,[],[f1770]) ).
cnf(s138,plain,
( ~ spl79_184
| ~ spl79_187 ),
inference(sat_conversion,[],[f1794]) ).
cnf(s145,plain,
( ~ spl79_190
| ~ spl79_195 ),
inference(sat_conversion,[],[f1833]) ).
cnf(s150,plain,
~ spl79_196,
inference(sat_conversion,[],[f1858]) ).
cnf(s155,plain,
( ~ spl79_51
| spl79_201 ),
inference(sat_conversion,[],[f1867]) ).
cnf(s160,plain,
( ~ spl79_51
| spl79_202 ),
inference(sat_conversion,[],[f1876]) ).
cnf(s164,plain,
( ~ spl79_56
| ~ spl79_203 ),
inference(sat_conversion,[],[f1884]) ).
cnf(s169,plain,
( ~ spl79_80
| spl79_204 ),
inference(sat_conversion,[],[f1893]) ).
cnf(s173,plain,
( ~ spl79_61
| ~ spl79_205 ),
inference(sat_conversion,[],[f1901]) ).
cnf(s178,plain,
( ~ spl79_109
| spl79_206 ),
inference(sat_conversion,[],[f1910]) ).
cnf(s182,plain,
( ~ spl79_66
| spl79_207 ),
inference(sat_conversion,[],[f1918]) ).
cnf(s187,plain,
( ~ spl79_138
| ~ spl79_208 ),
inference(sat_conversion,[],[f1927]) ).
cnf(s191,plain,
( ~ spl79_71
| ~ spl79_209 ),
inference(sat_conversion,[],[f1935]) ).
cnf(s196,plain,
( ~ spl79_167
| ~ spl79_210 ),
inference(sat_conversion,[],[f1944]) ).
cnf(s202,plain,
( ~ spl79_99
| ~ spl79_211 ),
inference(sat_conversion,[],[f1954]) ).
cnf(s208,plain,
( ~ spl79_117
| ~ spl79_212 ),
inference(sat_conversion,[],[f1964]) ).
cnf(s215,plain,
( ~ spl79_80
| ~ spl79_213 ),
inference(sat_conversion,[],[f1975]) ).
cnf(s220,plain,
( ~ spl79_56
| ~ spl79_214 ),
inference(sat_conversion,[],[f1984]) ).
cnf(s221,plain,
( ~ spl79_103
| spl79_215 ),
inference(sat_conversion,[],[f1989]) ).
cnf(s227,plain,
( ~ spl79_145
| ~ spl79_216 ),
inference(sat_conversion,[],[f1999]) ).
cnf(s233,plain,
( ~ spl79_90
| spl79_217 ),
inference(sat_conversion,[],[f2009]) ).
cnf(s236,plain,
( ~ spl79_174
| ~ spl79_218 ),
inference(sat_conversion,[],[f2016]) ).
cnf(s244,plain,
( ~ spl79_83
| ~ spl79_219 ),
inference(sat_conversion,[],[f2028]) ).
cnf(s249,plain,
( ~ spl79_83
| spl79_220 ),
inference(sat_conversion,[],[f2037]) ).
cnf(s254,plain,
( ~ spl79_117
| ~ spl79_221 ),
inference(sat_conversion,[],[f2046]) ).
cnf(s257,plain,
( ~ spl79_153
| ~ spl79_222 ),
inference(sat_conversion,[],[f2053]) ).
cnf(s262,plain,
( ~ spl79_128
| ~ spl79_223 ),
inference(sat_conversion,[],[f2062]) ).
cnf(s266,plain,
( ~ spl79_182
| spl79_224 ),
inference(sat_conversion,[],[f2070]) ).
cnf(s275,plain,
( ~ spl79_109
| ~ spl79_225 ),
inference(sat_conversion,[],[f2083]) ).
cnf(s280,plain,
( ~ spl79_61
| ~ spl79_226 ),
inference(sat_conversion,[],[f2092]) ).
cnf(s281,plain,
( ~ spl79_132
| spl79_227 ),
inference(sat_conversion,[],[f2097]) ).
cnf(s289,plain,
( ~ spl79_90
| ~ spl79_228 ),
inference(sat_conversion,[],[f2109]) ).
cnf(s293,plain,
( ~ spl79_119
| spl79_229 ),
inference(sat_conversion,[],[f2117]) ).
cnf(s298,plain,
( ~ spl79_119
| spl79_230 ),
inference(sat_conversion,[],[f2126]) ).
cnf(s303,plain,
( ~ spl79_153
| ~ spl79_231 ),
inference(sat_conversion,[],[f2135]) ).
cnf(s309,plain,
( ~ spl79_99
| spl79_232 ),
inference(sat_conversion,[],[f2145]) ).
cnf(s311,plain,
( ~ spl79_164
| spl79_233 ),
inference(sat_conversion,[],[f2151]) ).
cnf(s318,plain,
( ~ spl79_128
| spl79_234 ),
inference(sat_conversion,[],[f2162]) ).
cnf(s324,plain,
( ~ spl79_145
| ~ spl79_235 ),
inference(sat_conversion,[],[f2172]) ).
cnf(s326,plain,
( ~ spl79_187
| spl79_236 ),
inference(sat_conversion,[],[f2178]) ).
cnf(s335,plain,
( ~ spl79_138
| ~ spl79_237 ),
inference(sat_conversion,[],[f2191]) ).
cnf(s340,plain,
( ~ spl79_66
| ~ spl79_238 ),
inference(sat_conversion,[],[f2200]) ).
cnf(s342,plain,
( ~ spl79_155
| ~ spl79_239 ),
inference(sat_conversion,[],[f2206]) ).
cnf(s347,plain,
( ~ spl79_155
| spl79_240 ),
inference(sat_conversion,[],[f2215]) ).
cnf(s351,plain,
( ~ spl79_195
| spl79_241 ),
inference(sat_conversion,[],[f2223]) ).
cnf(s356,plain,
( ~ spl79_195
| ~ spl79_242 ),
inference(sat_conversion,[],[f2232]) ).
cnf(s363,plain,
( ~ spl79_182
| spl79_243 ),
inference(sat_conversion,[],[f2243]) ).
cnf(s367,plain,
( ~ spl79_164
| ~ spl79_244 ),
inference(sat_conversion,[],[f2251]) ).
cnf(s372,plain,
( ~ spl79_187
| spl79_245 ),
inference(sat_conversion,[],[f2260]) ).
cnf(s379,plain,
( ~ spl79_103
| spl79_246 ),
inference(sat_conversion,[],[f2271]) ).
cnf(s384,plain,
( ~ spl79_174
| spl79_247 ),
inference(sat_conversion,[],[f2280]) ).
cnf(s388,plain,
( ~ spl79_132
| ~ spl79_248 ),
inference(sat_conversion,[],[f2288]) ).
cnf(s395,plain,
( ~ spl79_1
| spl79_10
| spl79_19
| ~ spl79_28
| spl79_37
| spl79_46
| ~ spl79_51
| spl79_52
| ~ spl79_56
| ~ spl79_58
| ~ spl79_61
| spl79_64
| ~ spl79_66
| ~ spl79_70
| ~ spl79_71
| spl79_76
| ~ spl79_80
| spl79_82
| ~ spl79_88
| ~ spl79_94
| spl79_100
| spl79_106
| ~ spl79_109
| ~ spl79_112
| spl79_118
| spl79_124
| ~ spl79_130
| spl79_136
| ~ spl79_138
| ~ spl79_142
| spl79_148
| spl79_154
| ~ spl79_160
| spl79_166
| ~ spl79_167
| ~ spl79_172
| ~ spl79_178
| spl79_184
| spl79_190
| spl79_196
| ~ spl79_201
| ~ spl79_202
| spl79_203
| ~ spl79_204
| spl79_205
| ~ spl79_206
| ~ spl79_207
| spl79_208
| spl79_209
| spl79_210
| spl79_211
| spl79_212
| spl79_213
| spl79_214
| ~ spl79_215
| spl79_216
| ~ spl79_217
| spl79_218
| spl79_219
| ~ spl79_220
| spl79_221
| spl79_222
| spl79_223
| ~ spl79_224
| spl79_225
| spl79_226
| ~ spl79_227
| spl79_228
| ~ spl79_229
| ~ spl79_230
| spl79_231
| ~ spl79_232
| ~ spl79_233
| ~ spl79_234
| spl79_235
| ~ spl79_236
| spl79_237
| spl79_238
| spl79_239
| ~ spl79_240
| ~ spl79_241
| spl79_242
| ~ spl79_243
| spl79_244
| ~ spl79_245
| ~ spl79_246
| ~ spl79_247
| spl79_248 ),
inference(sat_conversion,[],[f2295]) ).
cnf(s416,plain,
spl79_195,
inference(sat_conversion,[],[f2316]) ).
cnf(s417,plain,
spl79_187,
inference(sat_conversion,[],[f2317]) ).
cnf(s418,plain,
spl79_182,
inference(sat_conversion,[],[f2318]) ).
cnf(s419,plain,
spl79_174,
inference(sat_conversion,[],[f2319]) ).
cnf(s420,plain,
spl79_167,
inference(sat_conversion,[],[f2320]) ).
cnf(s421,plain,
spl79_164,
inference(sat_conversion,[],[f2321]) ).
cnf(s422,plain,
spl79_155,
inference(sat_conversion,[],[f2322]) ).
cnf(s423,plain,
spl79_153,
inference(sat_conversion,[],[f2323]) ).
cnf(s424,plain,
spl79_145,
inference(sat_conversion,[],[f2324]) ).
cnf(s425,plain,
spl79_138,
inference(sat_conversion,[],[f2325]) ).
cnf(s426,plain,
spl79_132,
inference(sat_conversion,[],[f2326]) ).
cnf(s427,plain,
spl79_128,
inference(sat_conversion,[],[f2327]) ).
cnf(s428,plain,
spl79_119,
inference(sat_conversion,[],[f2328]) ).
cnf(s429,plain,
spl79_117,
inference(sat_conversion,[],[f2329]) ).
cnf(s430,plain,
spl79_109,
inference(sat_conversion,[],[f2330]) ).
cnf(s431,plain,
spl79_103,
inference(sat_conversion,[],[f2331]) ).
cnf(s432,plain,
spl79_99,
inference(sat_conversion,[],[f2332]) ).
cnf(s433,plain,
spl79_90,
inference(sat_conversion,[],[f2333]) ).
cnf(s434,plain,
spl79_83,
inference(sat_conversion,[],[f2334]) ).
cnf(s435,plain,
spl79_80,
inference(sat_conversion,[],[f2335]) ).
cnf(s436,plain,
spl79_71,
inference(sat_conversion,[],[f2336]) ).
cnf(s437,plain,
spl79_66,
inference(sat_conversion,[],[f2337]) ).
cnf(s438,plain,
spl79_61,
inference(sat_conversion,[],[f2338]) ).
cnf(s439,plain,
spl79_56,
inference(sat_conversion,[],[f2339]) ).
cnf(s440,plain,
spl79_51,
inference(sat_conversion,[],[f2340]) ).
cnf(s441,plain,
~ spl79_197,
inference(sat_conversion,[],[f2341]) ).
cnf(s442,plain,
~ spl79_198,
inference(sat_conversion,[],[f2342]) ).
cnf(s443,plain,
~ spl79_199,
inference(sat_conversion,[],[f2343]) ).
cnf(s444,plain,
~ spl79_200,
inference(sat_conversion,[],[f2344]) ).
cnf(s445,plain,
( spl79_3
| ~ spl79_56
| ~ spl79_80 ),
inference(sat_conversion,[],[f2347]) ).
cnf(s451,plain,
( spl79_34
| ~ spl79_128
| ~ spl79_145 ),
inference(sat_conversion,[],[f2369]) ).
cnf(s453,plain,
( spl79_23
| ~ spl79_90
| ~ spl79_128 ),
inference(sat_conversion,[],[f2377]) ).
cnf(s454,plain,
( ~ spl79_22
| ~ spl79_90
| ~ spl79_99
| spl79_199 ),
inference(sat_conversion,[],[f2384]) ).
cnf(s455,plain,
( ~ spl79_33
| ~ spl79_117
| ~ spl79_128
| spl79_198 ),
inference(sat_conversion,[],[f2390]) ).
cnf(s459,plain,
( spl79_45
| ~ spl79_164
| ~ spl79_174 ),
inference(sat_conversion,[],[f2404]) ).
cnf(s462,plain,
( ~ spl79_44
| spl79_143
| ~ spl79_164 ),
inference(sat_conversion,[],[f2415]) ).
cnf(s464,plain,
( ~ spl79_2
| ~ spl79_80
| spl79_87 ),
inference(sat_conversion,[],[f2432]) ).
cnf(s474,plain,
( ~ spl79_143
| ~ spl79_145 ),
inference(sat_conversion,[],[f2449]) ).
cnf(s477,plain,
( ~ spl79_83
| ~ spl79_87
| spl79_197 ),
inference(sat_conversion,[],[f2457]) ).
cnf(s480,plain,
( spl79_16
| ~ spl79_90
| ~ spl79_145 ),
inference(sat_conversion,[],[f2467]) ).
cnf(s481,plain,
( ~ spl79_15
| ~ spl79_145
| ~ spl79_153
| spl79_200 ),
inference(sat_conversion,[],[f2473]) ).
cnf(s482,plain,
spl79_3,
inference(rat,[],[s445,s439,s435]) ).
cnf(s483,plain,
~ spl79_87,
inference(rat,[],[s477,s441,s434]) ).
cnf(s484,plain,
~ spl79_2,
inference(rat,[],[s464,s435,s483]) ).
cnf(s486,plain,
~ spl79_22,
inference(rat,[],[s454,s443,s433,s432]) ).
cnf(s490,plain,
spl79_23,
inference(rat,[],[s453,s433,s427]) ).
cnf(s491,plain,
~ spl79_33,
inference(rat,[],[s455,s442,s429,s427]) ).
cnf(s494,plain,
~ spl79_143,
inference(rat,[],[s474,s424]) ).
cnf(s495,plain,
spl79_16,
inference(rat,[],[s480,s433,s424]) ).
cnf(s496,plain,
spl79_34,
inference(rat,[],[s451,s427,s424]) ).
cnf(s497,plain,
~ spl79_15,
inference(rat,[],[s481,s444,s424,s423]) ).
cnf(s498,plain,
~ spl79_44,
inference(rat,[],[s462,s494,s421]) ).
cnf(s500,plain,
spl79_45,
inference(rat,[],[s459,s421,s419]) ).
cnf(s524,plain,
( ~ spl79_1
| spl79_10
| spl79_19
| ~ spl79_28
| spl79_37
| spl79_46
| spl79_52
| ~ spl79_58
| spl79_64
| ~ spl79_70
| spl79_76
| spl79_82
| ~ spl79_88
| ~ spl79_94
| spl79_100
| spl79_106
| ~ spl79_112
| spl79_118
| spl79_124
| ~ spl79_130
| spl79_136
| ~ spl79_142
| spl79_148
| spl79_154
| ~ spl79_160
| spl79_166
| ~ spl79_172
| ~ spl79_178
| spl79_184
| spl79_190
| spl79_196
| ~ spl79_201
| ~ spl79_202
| spl79_203
| ~ spl79_204
| spl79_205
| ~ spl79_206
| ~ spl79_207
| spl79_208
| spl79_209
| spl79_210
| spl79_211
| spl79_212
| spl79_213
| spl79_214
| ~ spl79_215
| spl79_216
| ~ spl79_217
| spl79_218
| spl79_219
| ~ spl79_220
| spl79_221
| spl79_222
| spl79_223
| ~ spl79_224
| spl79_225
| spl79_226
| ~ spl79_227
| spl79_228
| ~ spl79_229
| ~ spl79_230
| spl79_231
| ~ spl79_232
| ~ spl79_233
| ~ spl79_234
| spl79_235
| ~ spl79_236
| spl79_237
| spl79_238
| spl79_239
| ~ spl79_240
| ~ spl79_241
| spl79_242
| ~ spl79_243
| spl79_244
| ~ spl79_245
| ~ spl79_246
| ~ spl79_247
| spl79_248 ),
inference(rat,[],[s395,s420,s425,s430,s435,s436,s437,s438,s439,s440]) ).
cnf(s529,plain,
~ spl79_248,
inference(rat,[],[s388,s426]) ).
cnf(s530,plain,
spl79_247,
inference(rat,[],[s384,s419]) ).
cnf(s531,plain,
spl79_246,
inference(rat,[],[s379,s431]) ).
cnf(s532,plain,
spl79_245,
inference(rat,[],[s372,s417]) ).
cnf(s533,plain,
~ spl79_244,
inference(rat,[],[s367,s421]) ).
cnf(s534,plain,
spl79_243,
inference(rat,[],[s363,s418]) ).
cnf(s535,plain,
~ spl79_242,
inference(rat,[],[s356,s416]) ).
cnf(s536,plain,
spl79_241,
inference(rat,[],[s351,s416]) ).
cnf(s537,plain,
spl79_240,
inference(rat,[],[s347,s422]) ).
cnf(s538,plain,
~ spl79_239,
inference(rat,[],[s342,s422]) ).
cnf(s539,plain,
~ spl79_238,
inference(rat,[],[s340,s437]) ).
cnf(s540,plain,
~ spl79_237,
inference(rat,[],[s335,s425]) ).
cnf(s541,plain,
spl79_236,
inference(rat,[],[s326,s417]) ).
cnf(s542,plain,
~ spl79_235,
inference(rat,[],[s324,s424]) ).
cnf(s543,plain,
spl79_234,
inference(rat,[],[s318,s427]) ).
cnf(s544,plain,
spl79_233,
inference(rat,[],[s311,s421]) ).
cnf(s545,plain,
spl79_232,
inference(rat,[],[s309,s432]) ).
cnf(s546,plain,
~ spl79_231,
inference(rat,[],[s303,s423]) ).
cnf(s547,plain,
spl79_230,
inference(rat,[],[s298,s428]) ).
cnf(s548,plain,
spl79_229,
inference(rat,[],[s293,s428]) ).
cnf(s549,plain,
~ spl79_228,
inference(rat,[],[s289,s433]) ).
cnf(s550,plain,
spl79_227,
inference(rat,[],[s281,s426]) ).
cnf(s551,plain,
~ spl79_226,
inference(rat,[],[s280,s438]) ).
cnf(s552,plain,
~ spl79_225,
inference(rat,[],[s275,s430]) ).
cnf(s553,plain,
spl79_224,
inference(rat,[],[s266,s418]) ).
cnf(s554,plain,
~ spl79_223,
inference(rat,[],[s262,s427]) ).
cnf(s555,plain,
~ spl79_222,
inference(rat,[],[s257,s423]) ).
cnf(s556,plain,
~ spl79_221,
inference(rat,[],[s254,s429]) ).
cnf(s557,plain,
spl79_220,
inference(rat,[],[s249,s434]) ).
cnf(s558,plain,
~ spl79_219,
inference(rat,[],[s244,s434]) ).
cnf(s559,plain,
~ spl79_218,
inference(rat,[],[s236,s419]) ).
cnf(s560,plain,
spl79_217,
inference(rat,[],[s233,s433]) ).
cnf(s561,plain,
~ spl79_216,
inference(rat,[],[s227,s424]) ).
cnf(s562,plain,
spl79_215,
inference(rat,[],[s221,s431]) ).
cnf(s563,plain,
~ spl79_214,
inference(rat,[],[s220,s439]) ).
cnf(s564,plain,
~ spl79_213,
inference(rat,[],[s215,s435]) ).
cnf(s565,plain,
~ spl79_212,
inference(rat,[],[s208,s429]) ).
cnf(s566,plain,
~ spl79_211,
inference(rat,[],[s202,s432]) ).
cnf(s567,plain,
~ spl79_210,
inference(rat,[],[s196,s420]) ).
cnf(s568,plain,
~ spl79_209,
inference(rat,[],[s191,s436]) ).
cnf(s569,plain,
~ spl79_208,
inference(rat,[],[s187,s425]) ).
cnf(s570,plain,
spl79_207,
inference(rat,[],[s182,s437]) ).
cnf(s571,plain,
spl79_206,
inference(rat,[],[s178,s430]) ).
cnf(s572,plain,
~ spl79_205,
inference(rat,[],[s173,s438]) ).
cnf(s573,plain,
spl79_204,
inference(rat,[],[s169,s435]) ).
cnf(s574,plain,
~ spl79_203,
inference(rat,[],[s164,s439]) ).
cnf(s575,plain,
spl79_202,
inference(rat,[],[s160,s440]) ).
cnf(s576,plain,
spl79_201,
inference(rat,[],[s155,s440]) ).
cnf(s577,plain,
~ spl79_190,
inference(rat,[],[s145,s416]) ).
cnf(s578,plain,
~ spl79_184,
inference(rat,[],[s138,s417]) ).
cnf(s579,plain,
spl79_178,
inference(rat,[],[s134,s418]) ).
cnf(s580,plain,
spl79_172,
inference(rat,[],[s127,s419]) ).
cnf(s581,plain,
~ spl79_166,
inference(rat,[],[s121,s420]) ).
cnf(s582,plain,
spl79_160,
inference(rat,[],[s119,s421]) ).
cnf(s583,plain,
~ spl79_154,
inference(rat,[],[s111,s422]) ).
cnf(s584,plain,
~ spl79_148,
inference(rat,[],[s110,s423]) ).
cnf(s585,plain,
spl79_142,
inference(rat,[],[s103,s424]) ).
cnf(s586,plain,
~ spl79_136,
inference(rat,[],[s97,s425]) ).
cnf(s587,plain,
spl79_130,
inference(rat,[],[s92,s426]) ).
cnf(s588,plain,
~ spl79_124,
inference(rat,[],[s89,s427]) ).
cnf(s589,plain,
~ spl79_118,
inference(rat,[],[s81,s428]) ).
cnf(s590,plain,
spl79_112,
inference(rat,[],[s80,s429]) ).
cnf(s591,plain,
~ spl79_106,
inference(rat,[],[s73,s430]) ).
cnf(s592,plain,
~ spl79_100,
inference(rat,[],[s68,s431]) ).
cnf(s593,plain,
spl79_94,
inference(rat,[],[s65,s432]) ).
cnf(s594,plain,
spl79_88,
inference(rat,[],[s57,s433]) ).
cnf(s595,plain,
~ spl79_82,
inference(rat,[],[s51,s434]) ).
cnf(s596,plain,
~ spl79_76,
inference(rat,[],[s49,s435]) ).
cnf(s597,plain,
spl79_70,
inference(rat,[],[s41,s436]) ).
cnf(s598,plain,
~ spl79_64,
inference(rat,[],[s37,s437]) ).
cnf(s599,plain,
spl79_58,
inference(rat,[],[s33,s438]) ).
cnf(s600,plain,
~ spl79_52,
inference(rat,[],[s29,s439]) ).
cnf(s601,plain,
~ spl79_46,
inference(rat,[],[s25,s440]) ).
cnf(s602,plain,
~ spl79_37,
inference(rat,[],[s20,s500,s498]) ).
cnf(s603,plain,
spl79_28,
inference(rat,[],[s15,s496,s491]) ).
cnf(s604,plain,
~ spl79_19,
inference(rat,[],[s10,s490,s486]) ).
cnf(s605,plain,
~ spl79_10,
inference(rat,[],[s7,s495,s497]) ).
cnf(s606,plain,
~ spl79_1,
inference(rat,[],[s524,s529,s530,s531,s532,s533,s534,s535,s536,s537,s538,s539,s540,s541,s542,s543,s544,s545,s546,s547,s548,s549,s550,s551,s552,s553,s554,s555,s556,s557,s558,s559,s560,s561,s562,s563,s564,s565,s566,s567,s568,s569,s570,s571,s572,s573,s574,s575,s576,s150,s577,s578,s579,s580,s581,s582,s583,s584,s585,s586,s587,s588,s589,s590,s591,s592,s593,s594,s595,s596,s597,s598,s599,s600,s601,s602,s603,s604,s605]) ).
cnf(s614,plain,
$false,
inference(rat,[],[s1,s482,s484,s606]) ).
fof(f2474,plain,
$false,
inference(avatar_sat_refutation,[],[s614]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG092+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 % Computer : n005.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 19:26:17 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.28 % (1068753)Will run a generic schedule for satisfiability detection.
% 0.19/0.28 % (1068759)% WARNING: option uhcvi not known.
% 0.19/0.28 % (1068759)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2721725563:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.28 % (1068761)dis+10_1_sil=32000:sp=arity:random_seed=1250705235:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.28 % (1068758)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4250838549_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.28 % (1068760)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=233527170:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.28 % (1068762)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=333821693:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.28 % (1068763)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=48826056:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.28 % (1068764)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1983383716:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.28 % (1068759) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1068753-1068759"...
% 0.19/0.28 % (1068759)...printing done.
% 0.19/0.28 % (1068759)Refutation found. Thanks to Tanya!
% 0.19/0.28 % SZS status Theorem for theBenchmark
% 0.19/0.28 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/0.29 % (1068759)------------------------------
% 0.19/0.29 % (1068759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.29 % (1068759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.29 % (1068759)CaDiCaL version: 2.1.3
% 0.19/0.29 % (1068759)Termination reason: Refutation
% 0.19/0.29 % (1068759)Time elapsed: 0.019 s
% 0.19/0.29 % (1068759)Peak memory usage: 14 MB
% 0.19/0.29 % (1068759)Instructions burned: 68 (million)
% 0.19/0.29 % (1068753)Success in time 0.053 s
% 0.19/0.29 % Vampire exiting
%------------------------------------------------------------------------------