%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG090+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 : n002.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.18s 0.28s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 107
% Syntax : Number of formulae : 600 ( 173 unt; 104 def)
% Number of atoms : 2891 (1536 equ)
% Maximal formula atoms : 415 ( 4 avg)
% Number of connectives : 3514 (1223 ~;1659 |; 528 &)
% ( 104 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 96 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 185 ( 183 usr; 184 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(f2,axiom,
( op(e0,e0) = e0
& op(e0,e1) = e1
& op(e0,e2) = e2
& op(e0,e3) = e3
& op(e0,e4) = e4
& op(e1,e0) = e1
& op(e1,e1) = e4
& op(e1,e2) = e0
& op(e1,e3) = e2
& op(e1,e4) = e3
& op(e2,e0) = e2
& op(e2,e1) = e0
& op(e2,e2) = e3
& op(e2,e3) = e4
& op(e2,e4) = e1
& op(e3,e0) = e3
& op(e3,e1) = e2
& op(e3,e2) = e4
& op(e3,e3) = e1
& op(e3,e4) = e0
& op(e4,e0) = e4
& op(e4,e1) = e3
& op(e4,e2) = e1
& op(e4,e3) = e0
& op(e4,e4) = e2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
unit = e0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
fof(f4,conjecture,
( ( op(e0,e0) = e0
| op(e1,e1) = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e0) = e1
| op(e1,e1) = e1
| op(e2,e2) = e1
| op(e3,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e0) = e2
| op(e1,e1) = e2
| op(e2,e2) = e2
| op(e3,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e0) = e3
| op(e1,e1) = e3
| op(e2,e2) = e3
| op(e3,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e0) = e4
| op(e1,e1) = e4
| op(e2,e2) = e4
| op(e3,e3) = e4
| op(e4,e4) = e4 )
& ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e4 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3
| op(e0,e1) = e4 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3
| op(e0,e2) = e4 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3
| op(e0,e3) = e4 )
& ( op(e0,e4) = e0
| op(e0,e4) = e1
| op(e0,e4) = e2
| op(e0,e4) = e3
| op(e0,e4) = e4 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3
| op(e1,e0) = e4 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3
| op(e1,e1) = e4 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3
| op(e1,e2) = e4 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3
| op(e1,e3) = e4 )
& ( op(e1,e4) = e0
| op(e1,e4) = e1
| op(e1,e4) = e2
| op(e1,e4) = e3
| op(e1,e4) = e4 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3
| op(e2,e0) = e4 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3
| op(e2,e1) = e4 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3
| op(e2,e2) = e4 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3
| op(e2,e3) = e4 )
& ( op(e2,e4) = e0
| op(e2,e4) = e1
| op(e2,e4) = e2
| op(e2,e4) = e3
| op(e2,e4) = e4 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3
| op(e3,e0) = e4 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3
| op(e3,e1) = e4 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3
| op(e3,e2) = e4 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3
| op(e3,e3) = e4 )
& ( op(e3,e4) = e0
| op(e3,e4) = e1
| op(e3,e4) = e2
| op(e3,e4) = e3
| op(e3,e4) = e4 )
& ( op(e4,e0) = e0
| op(e4,e0) = e1
| op(e4,e0) = e2
| op(e4,e0) = e3
| op(e4,e0) = e4 )
& ( op(e4,e1) = e0
| op(e4,e1) = e1
| op(e4,e1) = e2
| op(e4,e1) = e3
| op(e4,e1) = e4 )
& ( op(e4,e2) = e0
| op(e4,e2) = e1
| op(e4,e2) = e2
| op(e4,e2) = e3
| op(e4,e2) = e4 )
& ( op(e4,e3) = e0
| op(e4,e3) = e1
| op(e4,e3) = e2
| op(e4,e3) = e3
| op(e4,e3) = e4 )
& ( op(e4,e4) = e0
| op(e4,e4) = e1
| op(e4,e4) = e2
| op(e4,e4) = e3
| op(e4,e4) = e4 )
& op(unit,e0) = e0
& op(e0,unit) = e0
& op(unit,e1) = e1
& op(e1,unit) = e1
& op(unit,e2) = e2
& op(e2,unit) = e2
& op(unit,e3) = e3
& op(e3,unit) = e3
& op(unit,e4) = e4
& op(e4,unit) = e4
& ( unit = e0
| unit = e1
| unit = e2
| unit = e3
| unit = e4 )
& ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0
| op(e0,e4) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0
| op(e4,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1
| op(e0,e4) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1
| op(e4,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2
| op(e0,e4) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2
| op(e4,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3
| op(e0,e4) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3
| op(e4,e0) = e3 )
& ( op(e0,e0) = e4
| op(e0,e1) = e4
| op(e0,e2) = e4
| op(e0,e3) = e4
| op(e0,e4) = e4 )
& ( op(e0,e0) = e4
| op(e1,e0) = e4
| op(e2,e0) = e4
| op(e3,e0) = e4
| op(e4,e0) = e4 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0
| op(e1,e4) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0
| op(e4,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1
| op(e1,e4) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1
| op(e4,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2
| op(e1,e4) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2
| op(e4,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3
| op(e1,e4) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3
| op(e4,e1) = e3 )
& ( op(e1,e0) = e4
| op(e1,e1) = e4
| op(e1,e2) = e4
| op(e1,e3) = e4
| op(e1,e4) = e4 )
& ( op(e0,e1) = e4
| op(e1,e1) = e4
| op(e2,e1) = e4
| op(e3,e1) = e4
| op(e4,e1) = e4 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0
| op(e2,e4) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0
| op(e4,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1
| op(e2,e4) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1
| op(e4,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2
| op(e2,e4) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2
| op(e4,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3
| op(e2,e4) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3
| op(e4,e2) = e3 )
& ( op(e2,e0) = e4
| op(e2,e1) = e4
| op(e2,e2) = e4
| op(e2,e3) = e4
| op(e2,e4) = e4 )
& ( op(e0,e2) = e4
| op(e1,e2) = e4
| op(e2,e2) = e4
| op(e3,e2) = e4
| op(e4,e2) = e4 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0
| op(e3,e4) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0
| op(e4,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1
| op(e3,e4) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1
| op(e4,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2
| op(e3,e4) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2
| op(e4,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3
| op(e3,e4) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3
| op(e4,e3) = e3 )
& ( op(e3,e0) = e4
| op(e3,e1) = e4
| op(e3,e2) = e4
| op(e3,e3) = e4
| op(e3,e4) = e4 )
& ( op(e0,e3) = e4
| op(e1,e3) = e4
| op(e2,e3) = e4
| op(e3,e3) = e4
| op(e4,e3) = e4 )
& ( op(e4,e0) = e0
| op(e4,e1) = e0
| op(e4,e2) = e0
| op(e4,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e4) = e0
| op(e1,e4) = e0
| op(e2,e4) = e0
| op(e3,e4) = e0
| op(e4,e4) = e0 )
& ( op(e4,e0) = e1
| op(e4,e1) = e1
| op(e4,e2) = e1
| op(e4,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e4) = e1
| op(e1,e4) = e1
| op(e2,e4) = e1
| op(e3,e4) = e1
| op(e4,e4) = e1 )
& ( op(e4,e0) = e2
| op(e4,e1) = e2
| op(e4,e2) = e2
| op(e4,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e4) = e2
| op(e1,e4) = e2
| op(e2,e4) = e2
| op(e3,e4) = e2
| op(e4,e4) = e2 )
& ( op(e4,e0) = e3
| op(e4,e1) = e3
| op(e4,e2) = e3
| op(e4,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e4) = e3
| op(e1,e4) = e3
| op(e2,e4) = e3
| op(e3,e4) = e3
| op(e4,e4) = e3 )
& ( op(e4,e0) = e4
| op(e4,e1) = e4
| op(e4,e2) = e4
| op(e4,e3) = e4
| op(e4,e4) = e4 )
& ( op(e0,e4) = e4
| op(e1,e4) = e4
| op(e2,e4) = e4
| op(e3,e4) = e4
| op(e4,e4) = e4 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f5,negated_conjecture,
~ ( ( op(e0,e0) = e0
| op(e1,e1) = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e0) = e1
| op(e1,e1) = e1
| op(e2,e2) = e1
| op(e3,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e0) = e2
| op(e1,e1) = e2
| op(e2,e2) = e2
| op(e3,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e0) = e3
| op(e1,e1) = e3
| op(e2,e2) = e3
| op(e3,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e0) = e4
| op(e1,e1) = e4
| op(e2,e2) = e4
| op(e3,e3) = e4
| op(e4,e4) = e4 )
& ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e4 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3
| op(e0,e1) = e4 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3
| op(e0,e2) = e4 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3
| op(e0,e3) = e4 )
& ( op(e0,e4) = e0
| op(e0,e4) = e1
| op(e0,e4) = e2
| op(e0,e4) = e3
| op(e0,e4) = e4 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3
| op(e1,e0) = e4 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3
| op(e1,e1) = e4 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3
| op(e1,e2) = e4 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3
| op(e1,e3) = e4 )
& ( op(e1,e4) = e0
| op(e1,e4) = e1
| op(e1,e4) = e2
| op(e1,e4) = e3
| op(e1,e4) = e4 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3
| op(e2,e0) = e4 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3
| op(e2,e1) = e4 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3
| op(e2,e2) = e4 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3
| op(e2,e3) = e4 )
& ( op(e2,e4) = e0
| op(e2,e4) = e1
| op(e2,e4) = e2
| op(e2,e4) = e3
| op(e2,e4) = e4 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3
| op(e3,e0) = e4 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3
| op(e3,e1) = e4 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3
| op(e3,e2) = e4 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3
| op(e3,e3) = e4 )
& ( op(e3,e4) = e0
| op(e3,e4) = e1
| op(e3,e4) = e2
| op(e3,e4) = e3
| op(e3,e4) = e4 )
& ( op(e4,e0) = e0
| op(e4,e0) = e1
| op(e4,e0) = e2
| op(e4,e0) = e3
| op(e4,e0) = e4 )
& ( op(e4,e1) = e0
| op(e4,e1) = e1
| op(e4,e1) = e2
| op(e4,e1) = e3
| op(e4,e1) = e4 )
& ( op(e4,e2) = e0
| op(e4,e2) = e1
| op(e4,e2) = e2
| op(e4,e2) = e3
| op(e4,e2) = e4 )
& ( op(e4,e3) = e0
| op(e4,e3) = e1
| op(e4,e3) = e2
| op(e4,e3) = e3
| op(e4,e3) = e4 )
& ( op(e4,e4) = e0
| op(e4,e4) = e1
| op(e4,e4) = e2
| op(e4,e4) = e3
| op(e4,e4) = e4 )
& op(unit,e0) = e0
& op(e0,unit) = e0
& op(unit,e1) = e1
& op(e1,unit) = e1
& op(unit,e2) = e2
& op(e2,unit) = e2
& op(unit,e3) = e3
& op(e3,unit) = e3
& op(unit,e4) = e4
& op(e4,unit) = e4
& ( unit = e0
| unit = e1
| unit = e2
| unit = e3
| unit = e4 )
& ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0
| op(e0,e4) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0
| op(e4,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1
| op(e0,e4) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1
| op(e4,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2
| op(e0,e4) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2
| op(e4,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3
| op(e0,e4) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3
| op(e4,e0) = e3 )
& ( op(e0,e0) = e4
| op(e0,e1) = e4
| op(e0,e2) = e4
| op(e0,e3) = e4
| op(e0,e4) = e4 )
& ( op(e0,e0) = e4
| op(e1,e0) = e4
| op(e2,e0) = e4
| op(e3,e0) = e4
| op(e4,e0) = e4 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0
| op(e1,e4) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0
| op(e4,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1
| op(e1,e4) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1
| op(e4,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2
| op(e1,e4) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2
| op(e4,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3
| op(e1,e4) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3
| op(e4,e1) = e3 )
& ( op(e1,e0) = e4
| op(e1,e1) = e4
| op(e1,e2) = e4
| op(e1,e3) = e4
| op(e1,e4) = e4 )
& ( op(e0,e1) = e4
| op(e1,e1) = e4
| op(e2,e1) = e4
| op(e3,e1) = e4
| op(e4,e1) = e4 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0
| op(e2,e4) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0
| op(e4,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1
| op(e2,e4) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1
| op(e4,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2
| op(e2,e4) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2
| op(e4,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3
| op(e2,e4) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3
| op(e4,e2) = e3 )
& ( op(e2,e0) = e4
| op(e2,e1) = e4
| op(e2,e2) = e4
| op(e2,e3) = e4
| op(e2,e4) = e4 )
& ( op(e0,e2) = e4
| op(e1,e2) = e4
| op(e2,e2) = e4
| op(e3,e2) = e4
| op(e4,e2) = e4 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0
| op(e3,e4) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0
| op(e4,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1
| op(e3,e4) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1
| op(e4,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2
| op(e3,e4) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2
| op(e4,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3
| op(e3,e4) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3
| op(e4,e3) = e3 )
& ( op(e3,e0) = e4
| op(e3,e1) = e4
| op(e3,e2) = e4
| op(e3,e3) = e4
| op(e3,e4) = e4 )
& ( op(e0,e3) = e4
| op(e1,e3) = e4
| op(e2,e3) = e4
| op(e3,e3) = e4
| op(e4,e3) = e4 )
& ( op(e4,e0) = e0
| op(e4,e1) = e0
| op(e4,e2) = e0
| op(e4,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e4) = e0
| op(e1,e4) = e0
| op(e2,e4) = e0
| op(e3,e4) = e0
| op(e4,e4) = e0 )
& ( op(e4,e0) = e1
| op(e4,e1) = e1
| op(e4,e2) = e1
| op(e4,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e4) = e1
| op(e1,e4) = e1
| op(e2,e4) = e1
| op(e3,e4) = e1
| op(e4,e4) = e1 )
& ( op(e4,e0) = e2
| op(e4,e1) = e2
| op(e4,e2) = e2
| op(e4,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e4) = e2
| op(e1,e4) = e2
| op(e2,e4) = e2
| op(e3,e4) = e2
| op(e4,e4) = e2 )
& ( op(e4,e0) = e3
| op(e4,e1) = e3
| op(e4,e2) = e3
| op(e4,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e4) = e3
| op(e1,e4) = e3
| op(e2,e4) = e3
| op(e3,e4) = e3
| op(e4,e4) = e3 )
& ( op(e4,e0) = e4
| op(e4,e1) = e4
| op(e4,e2) = e4
| op(e4,e3) = e4
| op(e4,e4) = e4 )
& ( op(e0,e4) = e4
| op(e1,e4) = e4
| op(e2,e4) = e4
| op(e3,e4) = e4
| op(e4,e4) = e4 ) ),
inference(negated_conjecture,[status(cth)],[f4]) ).
fof(f6,plain,
( ( e0 != op(e0,e0)
& e0 != op(e1,e1)
& e0 != op(e2,e2)
& e0 != op(e3,e3)
& e0 != op(e4,e4) )
| ( e1 != op(e0,e0)
& e1 != op(e1,e1)
& e1 != op(e2,e2)
& e1 != op(e3,e3)
& e1 != op(e4,e4) )
| ( e2 != op(e0,e0)
& e2 != op(e1,e1)
& e2 != op(e2,e2)
& e2 != op(e3,e3)
& e2 != op(e4,e4) )
| ( e3 != op(e0,e0)
& e3 != op(e1,e1)
& e3 != op(e2,e2)
& e3 != op(e3,e3)
& e3 != op(e4,e4) )
| ( e4 != op(e0,e0)
& e4 != op(e1,e1)
& e4 != op(e2,e2)
& e4 != op(e3,e3)
& e4 != op(e4,e4) )
| ( e0 != op(e0,e0)
& e1 != op(e0,e0)
& e2 != op(e0,e0)
& e3 != op(e0,e0)
& e4 != op(e0,e0) )
| ( e0 != op(e0,e1)
& e1 != op(e0,e1)
& e2 != op(e0,e1)
& e3 != op(e0,e1)
& e4 != op(e0,e1) )
| ( e0 != op(e0,e2)
& e1 != op(e0,e2)
& e2 != op(e0,e2)
& e3 != op(e0,e2)
& e4 != op(e0,e2) )
| ( e0 != op(e0,e3)
& e1 != op(e0,e3)
& e2 != op(e0,e3)
& e3 != op(e0,e3)
& e4 != op(e0,e3) )
| ( e0 != op(e0,e4)
& e1 != op(e0,e4)
& e2 != op(e0,e4)
& e3 != op(e0,e4)
& e4 != op(e0,e4) )
| ( e0 != op(e1,e0)
& e1 != op(e1,e0)
& e2 != op(e1,e0)
& e3 != op(e1,e0)
& e4 != op(e1,e0) )
| ( e0 != op(e1,e1)
& e1 != op(e1,e1)
& e2 != op(e1,e1)
& e3 != op(e1,e1)
& e4 != op(e1,e1) )
| ( e0 != op(e1,e2)
& e1 != op(e1,e2)
& e2 != op(e1,e2)
& e3 != op(e1,e2)
& e4 != op(e1,e2) )
| ( e0 != op(e1,e3)
& e1 != op(e1,e3)
& e2 != op(e1,e3)
& e3 != op(e1,e3)
& e4 != op(e1,e3) )
| ( e0 != op(e1,e4)
& e1 != op(e1,e4)
& e2 != op(e1,e4)
& e3 != op(e1,e4)
& e4 != op(e1,e4) )
| ( e0 != op(e2,e0)
& e1 != op(e2,e0)
& e2 != op(e2,e0)
& e3 != op(e2,e0)
& e4 != op(e2,e0) )
| ( e0 != op(e2,e1)
& e1 != op(e2,e1)
& e2 != op(e2,e1)
& e3 != op(e2,e1)
& e4 != op(e2,e1) )
| ( e0 != op(e2,e2)
& e1 != op(e2,e2)
& e2 != op(e2,e2)
& e3 != op(e2,e2)
& e4 != op(e2,e2) )
| ( e0 != op(e2,e3)
& e1 != op(e2,e3)
& e2 != op(e2,e3)
& e3 != op(e2,e3)
& e4 != op(e2,e3) )
| ( e0 != op(e2,e4)
& e1 != op(e2,e4)
& e2 != op(e2,e4)
& e3 != op(e2,e4)
& e4 != op(e2,e4) )
| ( e0 != op(e3,e0)
& e1 != op(e3,e0)
& e2 != op(e3,e0)
& e3 != op(e3,e0)
& e4 != op(e3,e0) )
| ( e0 != op(e3,e1)
& e1 != op(e3,e1)
& e2 != op(e3,e1)
& e3 != op(e3,e1)
& e4 != op(e3,e1) )
| ( e0 != op(e3,e2)
& e1 != op(e3,e2)
& e2 != op(e3,e2)
& e3 != op(e3,e2)
& e4 != op(e3,e2) )
| ( e0 != op(e3,e3)
& e1 != op(e3,e3)
& e2 != op(e3,e3)
& e3 != op(e3,e3)
& e4 != op(e3,e3) )
| ( e0 != op(e3,e4)
& e1 != op(e3,e4)
& e2 != op(e3,e4)
& e3 != op(e3,e4)
& e4 != op(e3,e4) )
| ( e0 != op(e4,e0)
& e1 != op(e4,e0)
& e2 != op(e4,e0)
& e3 != op(e4,e0)
& e4 != op(e4,e0) )
| ( e0 != op(e4,e1)
& e1 != op(e4,e1)
& e2 != op(e4,e1)
& e3 != op(e4,e1)
& e4 != op(e4,e1) )
| ( e0 != op(e4,e2)
& e1 != op(e4,e2)
& e2 != op(e4,e2)
& e3 != op(e4,e2)
& e4 != op(e4,e2) )
| ( e0 != op(e4,e3)
& e1 != op(e4,e3)
& e2 != op(e4,e3)
& e3 != op(e4,e3)
& e4 != op(e4,e3) )
| ( e0 != op(e4,e4)
& e1 != op(e4,e4)
& e2 != op(e4,e4)
& e3 != op(e4,e4)
& e4 != op(e4,e4) )
| e0 != op(unit,e0)
| e0 != op(e0,unit)
| e1 != op(unit,e1)
| e1 != op(e1,unit)
| e2 != op(unit,e2)
| e2 != op(e2,unit)
| e3 != op(unit,e3)
| e3 != op(e3,unit)
| e4 != op(unit,e4)
| e4 != op(e4,unit)
| ( e0 != unit
& e1 != unit
& e2 != unit
& e3 != unit
& e4 != unit )
| ( e0 != op(e0,e0)
& e0 != op(e0,e1)
& e0 != op(e0,e2)
& e0 != op(e0,e3)
& e0 != op(e0,e4) )
| ( e0 != op(e0,e0)
& e0 != op(e1,e0)
& e0 != op(e2,e0)
& e0 != op(e3,e0)
& e0 != op(e4,e0) )
| ( e1 != op(e0,e0)
& e1 != op(e0,e1)
& e1 != op(e0,e2)
& e1 != op(e0,e3)
& e1 != op(e0,e4) )
| ( e1 != op(e0,e0)
& e1 != op(e1,e0)
& e1 != op(e2,e0)
& e1 != op(e3,e0)
& e1 != op(e4,e0) )
| ( e2 != op(e0,e0)
& e2 != op(e0,e1)
& e2 != op(e0,e2)
& e2 != op(e0,e3)
& e2 != op(e0,e4) )
| ( e2 != op(e0,e0)
& e2 != op(e1,e0)
& e2 != op(e2,e0)
& e2 != op(e3,e0)
& e2 != op(e4,e0) )
| ( e3 != op(e0,e0)
& e3 != op(e0,e1)
& e3 != op(e0,e2)
& e3 != op(e0,e3)
& e3 != op(e0,e4) )
| ( e3 != op(e0,e0)
& e3 != op(e1,e0)
& e3 != op(e2,e0)
& e3 != op(e3,e0)
& e3 != op(e4,e0) )
| ( e4 != op(e0,e0)
& e4 != op(e0,e1)
& e4 != op(e0,e2)
& e4 != op(e0,e3)
& e4 != op(e0,e4) )
| ( e4 != op(e0,e0)
& e4 != op(e1,e0)
& e4 != op(e2,e0)
& e4 != op(e3,e0)
& e4 != op(e4,e0) )
| ( e0 != op(e1,e0)
& e0 != op(e1,e1)
& e0 != op(e1,e2)
& e0 != op(e1,e3)
& e0 != op(e1,e4) )
| ( e0 != op(e0,e1)
& e0 != op(e1,e1)
& e0 != op(e2,e1)
& e0 != op(e3,e1)
& e0 != op(e4,e1) )
| ( e1 != op(e1,e0)
& e1 != op(e1,e1)
& e1 != op(e1,e2)
& e1 != op(e1,e3)
& e1 != op(e1,e4) )
| ( e1 != op(e0,e1)
& e1 != op(e1,e1)
& e1 != op(e2,e1)
& e1 != op(e3,e1)
& e1 != op(e4,e1) )
| ( e2 != op(e1,e0)
& e2 != op(e1,e1)
& e2 != op(e1,e2)
& e2 != op(e1,e3)
& e2 != op(e1,e4) )
| ( e2 != op(e0,e1)
& e2 != op(e1,e1)
& e2 != op(e2,e1)
& e2 != op(e3,e1)
& e2 != op(e4,e1) )
| ( e3 != op(e1,e0)
& e3 != op(e1,e1)
& e3 != op(e1,e2)
& e3 != op(e1,e3)
& e3 != op(e1,e4) )
| ( e3 != op(e0,e1)
& e3 != op(e1,e1)
& e3 != op(e2,e1)
& e3 != op(e3,e1)
& e3 != op(e4,e1) )
| ( e4 != op(e1,e0)
& e4 != op(e1,e1)
& e4 != op(e1,e2)
& e4 != op(e1,e3)
& e4 != op(e1,e4) )
| ( e4 != op(e0,e1)
& e4 != op(e1,e1)
& e4 != op(e2,e1)
& e4 != op(e3,e1)
& e4 != op(e4,e1) )
| ( e0 != op(e2,e0)
& e0 != op(e2,e1)
& e0 != op(e2,e2)
& e0 != op(e2,e3)
& e0 != op(e2,e4) )
| ( e0 != op(e0,e2)
& e0 != op(e1,e2)
& e0 != op(e2,e2)
& e0 != op(e3,e2)
& e0 != op(e4,e2) )
| ( e1 != op(e2,e0)
& e1 != op(e2,e1)
& e1 != op(e2,e2)
& e1 != op(e2,e3)
& e1 != op(e2,e4) )
| ( e1 != op(e0,e2)
& e1 != op(e1,e2)
& e1 != op(e2,e2)
& e1 != op(e3,e2)
& e1 != op(e4,e2) )
| ( e2 != op(e2,e0)
& e2 != op(e2,e1)
& e2 != op(e2,e2)
& e2 != op(e2,e3)
& e2 != op(e2,e4) )
| ( e2 != op(e0,e2)
& e2 != op(e1,e2)
& e2 != op(e2,e2)
& e2 != op(e3,e2)
& e2 != op(e4,e2) )
| ( e3 != op(e2,e0)
& e3 != op(e2,e1)
& e3 != op(e2,e2)
& e3 != op(e2,e3)
& e3 != op(e2,e4) )
| ( e3 != op(e0,e2)
& e3 != op(e1,e2)
& e3 != op(e2,e2)
& e3 != op(e3,e2)
& e3 != op(e4,e2) )
| ( e4 != op(e2,e0)
& e4 != op(e2,e1)
& e4 != op(e2,e2)
& e4 != op(e2,e3)
& e4 != op(e2,e4) )
| ( e4 != op(e0,e2)
& e4 != op(e1,e2)
& e4 != op(e2,e2)
& e4 != op(e3,e2)
& e4 != op(e4,e2) )
| ( e0 != op(e3,e0)
& e0 != op(e3,e1)
& e0 != op(e3,e2)
& e0 != op(e3,e3)
& e0 != op(e3,e4) )
| ( e0 != op(e0,e3)
& e0 != op(e1,e3)
& e0 != op(e2,e3)
& e0 != op(e3,e3)
& e0 != op(e4,e3) )
| ( e1 != op(e3,e0)
& e1 != op(e3,e1)
& e1 != op(e3,e2)
& e1 != op(e3,e3)
& e1 != op(e3,e4) )
| ( e1 != op(e0,e3)
& e1 != op(e1,e3)
& e1 != op(e2,e3)
& e1 != op(e3,e3)
& e1 != op(e4,e3) )
| ( e2 != op(e3,e0)
& e2 != op(e3,e1)
& e2 != op(e3,e2)
& e2 != op(e3,e3)
& e2 != op(e3,e4) )
| ( e2 != op(e0,e3)
& e2 != op(e1,e3)
& e2 != op(e2,e3)
& e2 != op(e3,e3)
& e2 != op(e4,e3) )
| ( e3 != op(e3,e0)
& e3 != op(e3,e1)
& e3 != op(e3,e2)
& e3 != op(e3,e3)
& e3 != op(e3,e4) )
| ( e3 != op(e0,e3)
& e3 != op(e1,e3)
& e3 != op(e2,e3)
& e3 != op(e3,e3)
& e3 != op(e4,e3) )
| ( e4 != op(e3,e0)
& e4 != op(e3,e1)
& e4 != op(e3,e2)
& e4 != op(e3,e3)
& e4 != op(e3,e4) )
| ( e4 != op(e0,e3)
& e4 != op(e1,e3)
& e4 != op(e2,e3)
& e4 != op(e3,e3)
& e4 != op(e4,e3) )
| ( e0 != op(e4,e0)
& e0 != op(e4,e1)
& e0 != op(e4,e2)
& e0 != op(e4,e3)
& e0 != op(e4,e4) )
| ( e0 != op(e0,e4)
& e0 != op(e1,e4)
& e0 != op(e2,e4)
& e0 != op(e3,e4)
& e0 != op(e4,e4) )
| ( e1 != op(e4,e0)
& e1 != op(e4,e1)
& e1 != op(e4,e2)
& e1 != op(e4,e3)
& e1 != op(e4,e4) )
| ( e1 != op(e0,e4)
& e1 != op(e1,e4)
& e1 != op(e2,e4)
& e1 != op(e3,e4)
& e1 != op(e4,e4) )
| ( e2 != op(e4,e0)
& e2 != op(e4,e1)
& e2 != op(e4,e2)
& e2 != op(e4,e3)
& e2 != op(e4,e4) )
| ( e2 != op(e0,e4)
& e2 != op(e1,e4)
& e2 != op(e2,e4)
& e2 != op(e3,e4)
& e2 != op(e4,e4) )
| ( e3 != op(e4,e0)
& e3 != op(e4,e1)
& e3 != op(e4,e2)
& e3 != op(e4,e3)
& e3 != op(e4,e4) )
| ( e3 != op(e0,e4)
& e3 != op(e1,e4)
& e3 != op(e2,e4)
& e3 != op(e3,e4)
& e3 != op(e4,e4) )
| ( e4 != op(e4,e0)
& e4 != op(e4,e1)
& e4 != op(e4,e2)
& e4 != op(e4,e3)
& e4 != op(e4,e4) )
| ( e4 != op(e0,e4)
& e4 != op(e1,e4)
& e4 != op(e2,e4)
& e4 != op(e3,e4)
& e4 != op(e4,e4) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f17,plain,
e2 = op(e4,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f18,plain,
e0 = 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,
e0 = op(e3,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f23,plain,
e1 = op(e3,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f24,plain,
e4 = 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,
e1 = op(e2,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f28,plain,
e4 = op(e2,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f29,plain,
e3 = 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,
e3 = op(e1,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f33,plain,
e2 = op(e1,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f34,plain,
e0 = 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(f47,plain,
( e0 != op(e0,e0)
| ~ sP78 ),
inference(cnf_transformation,[],[f6]) ).
fof(f49,plain,
( e1 != op(e3,e3)
| ~ sP77 ),
inference(cnf_transformation,[],[f6]) ).
fof(f53,plain,
( e2 != op(e4,e4)
| ~ sP76 ),
inference(cnf_transformation,[],[f6]) ).
fof(f60,plain,
( e3 != op(e2,e2)
| ~ sP75 ),
inference(cnf_transformation,[],[f6]) ).
fof(f66,plain,
( e4 != op(e1,e1)
| ~ sP74 ),
inference(cnf_transformation,[],[f6]) ).
fof(f72,plain,
( e0 != op(e0,e0)
| ~ sP73 ),
inference(cnf_transformation,[],[f6]) ).
fof(f76,plain,
( e1 != op(e0,e1)
| ~ sP72 ),
inference(cnf_transformation,[],[f6]) ).
fof(f80,plain,
( e2 != op(e0,e2)
| ~ sP71 ),
inference(cnf_transformation,[],[f6]) ).
fof(f84,plain,
( e3 != op(e0,e3)
| ~ sP70 ),
inference(cnf_transformation,[],[f6]) ).
fof(f88,plain,
( e4 != op(e0,e4)
| ~ sP69 ),
inference(cnf_transformation,[],[f6]) ).
fof(f96,plain,
( e1 != op(e1,e0)
| ~ sP68 ),
inference(cnf_transformation,[],[f6]) ).
fof(f98,plain,
( e4 != op(e1,e1)
| ~ sP67 ),
inference(cnf_transformation,[],[f6]) ).
fof(f107,plain,
( e0 != op(e1,e2)
| ~ sP66 ),
inference(cnf_transformation,[],[f6]) ).
fof(f110,plain,
( e2 != op(e1,e3)
| ~ sP65 ),
inference(cnf_transformation,[],[f6]) ).
fof(f114,plain,
( e3 != op(e1,e4)
| ~ sP64 ),
inference(cnf_transformation,[],[f6]) ).
fof(f120,plain,
( e2 != op(e2,e0)
| ~ sP63 ),
inference(cnf_transformation,[],[f6]) ).
fof(f127,plain,
( e0 != op(e2,e1)
| ~ sP62 ),
inference(cnf_transformation,[],[f6]) ).
fof(f129,plain,
( e3 != op(e2,e2)
| ~ sP61 ),
inference(cnf_transformation,[],[f6]) ).
fof(f133,plain,
( e4 != op(e2,e3)
| ~ sP60 ),
inference(cnf_transformation,[],[f6]) ).
fof(f141,plain,
( e1 != op(e2,e4)
| ~ sP59 ),
inference(cnf_transformation,[],[f6]) ).
fof(f144,plain,
( e3 != op(e3,e0)
| ~ sP58 ),
inference(cnf_transformation,[],[f6]) ).
fof(f150,plain,
( e2 != op(e3,e1)
| ~ sP57 ),
inference(cnf_transformation,[],[f6]) ).
fof(f153,plain,
( e4 != op(e3,e2)
| ~ sP56 ),
inference(cnf_transformation,[],[f6]) ).
fof(f161,plain,
( e1 != op(e3,e3)
| ~ sP55 ),
inference(cnf_transformation,[],[f6]) ).
fof(f167,plain,
( e0 != op(e3,e4)
| ~ sP54 ),
inference(cnf_transformation,[],[f6]) ).
fof(f168,plain,
( e4 != op(e4,e0)
| ~ sP53 ),
inference(cnf_transformation,[],[f6]) ).
fof(f174,plain,
( e3 != op(e4,e1)
| ~ sP52 ),
inference(cnf_transformation,[],[f6]) ).
fof(f181,plain,
( e1 != op(e4,e2)
| ~ sP51 ),
inference(cnf_transformation,[],[f6]) ).
fof(f187,plain,
( e0 != op(e4,e3)
| ~ sP50 ),
inference(cnf_transformation,[],[f6]) ).
fof(f190,plain,
( e2 != op(e4,e4)
| ~ sP49 ),
inference(cnf_transformation,[],[f6]) ).
fof(f197,plain,
( e0 != unit
| ~ sP48 ),
inference(cnf_transformation,[],[f6]) ).
fof(f202,plain,
( e0 != op(e0,e0)
| ~ sP47 ),
inference(cnf_transformation,[],[f6]) ).
fof(f207,plain,
( e0 != op(e0,e0)
| ~ sP46 ),
inference(cnf_transformation,[],[f6]) ).
fof(f211,plain,
( e1 != op(e0,e1)
| ~ sP45 ),
inference(cnf_transformation,[],[f6]) ).
fof(f216,plain,
( e1 != op(e1,e0)
| ~ sP44 ),
inference(cnf_transformation,[],[f6]) ).
fof(f220,plain,
( e2 != op(e0,e2)
| ~ sP43 ),
inference(cnf_transformation,[],[f6]) ).
fof(f225,plain,
( e2 != op(e2,e0)
| ~ sP42 ),
inference(cnf_transformation,[],[f6]) ).
fof(f229,plain,
( e3 != op(e0,e3)
| ~ sP41 ),
inference(cnf_transformation,[],[f6]) ).
fof(f234,plain,
( e3 != op(e3,e0)
| ~ sP40 ),
inference(cnf_transformation,[],[f6]) ).
fof(f238,plain,
( e4 != op(e0,e4)
| ~ sP39 ),
inference(cnf_transformation,[],[f6]) ).
fof(f243,plain,
( e4 != op(e4,e0)
| ~ sP38 ),
inference(cnf_transformation,[],[f6]) ).
fof(f250,plain,
( e0 != op(e1,e2)
| ~ sP37 ),
inference(cnf_transformation,[],[f6]) ).
fof(f255,plain,
( e0 != op(e2,e1)
| ~ sP36 ),
inference(cnf_transformation,[],[f6]) ).
fof(f262,plain,
( e1 != op(e1,e0)
| ~ sP35 ),
inference(cnf_transformation,[],[f6]) ).
fof(f267,plain,
( e1 != op(e0,e1)
| ~ sP34 ),
inference(cnf_transformation,[],[f6]) ).
fof(f269,plain,
( e2 != op(e1,e3)
| ~ sP33 ),
inference(cnf_transformation,[],[f6]) ).
fof(f274,plain,
( e2 != op(e3,e1)
| ~ sP32 ),
inference(cnf_transformation,[],[f6]) ).
fof(f278,plain,
( e3 != op(e1,e4)
| ~ sP31 ),
inference(cnf_transformation,[],[f6]) ).
fof(f283,plain,
( e3 != op(e4,e1)
| ~ sP30 ),
inference(cnf_transformation,[],[f6]) ).
fof(f291,plain,
( e4 != op(e1,e1)
| ~ sP29 ),
inference(cnf_transformation,[],[f6]) ).
fof(f296,plain,
( e4 != op(e1,e1)
| ~ sP28 ),
inference(cnf_transformation,[],[f6]) ).
fof(f301,plain,
( e0 != op(e2,e1)
| ~ sP27 ),
inference(cnf_transformation,[],[f6]) ).
fof(f306,plain,
( e0 != op(e1,e2)
| ~ sP26 ),
inference(cnf_transformation,[],[f6]) ).
fof(f308,plain,
( e1 != op(e2,e4)
| ~ sP25 ),
inference(cnf_transformation,[],[f6]) ).
fof(f313,plain,
( e1 != op(e4,e2)
| ~ sP24 ),
inference(cnf_transformation,[],[f6]) ).
fof(f322,plain,
( e2 != op(e2,e0)
| ~ sP23 ),
inference(cnf_transformation,[],[f6]) ).
fof(f327,plain,
( e2 != op(e0,e2)
| ~ sP22 ),
inference(cnf_transformation,[],[f6]) ).
fof(f330,plain,
( e3 != op(e2,e2)
| ~ sP21 ),
inference(cnf_transformation,[],[f6]) ).
fof(f335,plain,
( e3 != op(e2,e2)
| ~ sP20 ),
inference(cnf_transformation,[],[f6]) ).
fof(f339,plain,
( e4 != op(e2,e3)
| ~ sP19 ),
inference(cnf_transformation,[],[f6]) ).
fof(f344,plain,
( e4 != op(e3,e2)
| ~ sP18 ),
inference(cnf_transformation,[],[f6]) ).
fof(f348,plain,
( e0 != op(e3,e4)
| ~ sP17 ),
inference(cnf_transformation,[],[f6]) ).
fof(f353,plain,
( e0 != op(e4,e3)
| ~ sP16 ),
inference(cnf_transformation,[],[f6]) ).
fof(f359,plain,
( e1 != op(e3,e3)
| ~ sP15 ),
inference(cnf_transformation,[],[f6]) ).
fof(f364,plain,
( e1 != op(e3,e3)
| ~ sP14 ),
inference(cnf_transformation,[],[f6]) ).
fof(f371,plain,
( e2 != op(e3,e1)
| ~ sP13 ),
inference(cnf_transformation,[],[f6]) ).
fof(f376,plain,
( e2 != op(e1,e3)
| ~ sP12 ),
inference(cnf_transformation,[],[f6]) ).
fof(f382,plain,
( e3 != op(e3,e0)
| ~ sP11 ),
inference(cnf_transformation,[],[f6]) ).
fof(f387,plain,
( e3 != op(e0,e3)
| ~ sP10 ),
inference(cnf_transformation,[],[f6]) ).
fof(f390,plain,
( e4 != op(e3,e2)
| ~ sP9 ),
inference(cnf_transformation,[],[f6]) ).
fof(f395,plain,
( e4 != op(e2,e3)
| ~ sP8 ),
inference(cnf_transformation,[],[f6]) ).
fof(f399,plain,
( e0 != op(e4,e3)
| ~ sP7 ),
inference(cnf_transformation,[],[f6]) ).
fof(f404,plain,
( e0 != op(e3,e4)
| ~ sP6 ),
inference(cnf_transformation,[],[f6]) ).
fof(f410,plain,
( e1 != op(e4,e2)
| ~ sP5 ),
inference(cnf_transformation,[],[f6]) ).
fof(f415,plain,
( e1 != op(e2,e4)
| ~ sP4 ),
inference(cnf_transformation,[],[f6]) ).
fof(f418,plain,
( e2 != op(e4,e4)
| ~ sP3 ),
inference(cnf_transformation,[],[f6]) ).
fof(f423,plain,
( e2 != op(e4,e4)
| ~ sP2 ),
inference(cnf_transformation,[],[f6]) ).
fof(f431,plain,
( e3 != op(e4,e1)
| ~ sP1 ),
inference(cnf_transformation,[],[f6]) ).
fof(f436,plain,
( e3 != op(e1,e4)
| ~ sP0 ),
inference(cnf_transformation,[],[f6]) ).
fof(f442,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(f467,plain,
unit = op(unit,unit),
inference(definition_unfolding,[],[f41,f42,f42,f42]) ).
fof(f468,plain,
e1 = op(unit,e1),
inference(definition_unfolding,[],[f40,f42]) ).
fof(f469,plain,
e2 = op(unit,e2),
inference(definition_unfolding,[],[f39,f42]) ).
fof(f470,plain,
e3 = op(unit,e3),
inference(definition_unfolding,[],[f38,f42]) ).
fof(f471,plain,
e4 = op(unit,e4),
inference(definition_unfolding,[],[f37,f42]) ).
fof(f472,plain,
e1 = op(e1,unit),
inference(definition_unfolding,[],[f36,f42]) ).
fof(f473,plain,
op(e1,e2) = unit,
inference(definition_unfolding,[],[f34,f42]) ).
fof(f474,plain,
e2 = op(e2,unit),
inference(definition_unfolding,[],[f31,f42]) ).
fof(f475,plain,
op(e2,e1) = unit,
inference(definition_unfolding,[],[f30,f42]) ).
fof(f476,plain,
e3 = op(e3,unit),
inference(definition_unfolding,[],[f26,f42]) ).
fof(f477,plain,
op(e3,e4) = unit,
inference(definition_unfolding,[],[f22,f42]) ).
fof(f478,plain,
e4 = op(e4,unit),
inference(definition_unfolding,[],[f21,f42]) ).
fof(f479,plain,
op(e4,e3) = unit,
inference(definition_unfolding,[],[f18,f42]) ).
fof(f500,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,[],[f442,f42,f42,f42,f42,f42,f42]) ).
fof(f514,plain,
( op(e3,e4) != unit
| ~ sP6 ),
inference(definition_unfolding,[],[f404,f42]) ).
fof(f519,plain,
( op(e4,e3) != unit
| ~ sP7 ),
inference(definition_unfolding,[],[f399,f42]) ).
fof(f523,plain,
( e3 != op(unit,e3)
| ~ sP10 ),
inference(definition_unfolding,[],[f387,f42]) ).
fof(f524,plain,
( e3 != op(e3,unit)
| ~ sP11 ),
inference(definition_unfolding,[],[f382,f42]) ).
fof(f533,plain,
( op(e4,e3) != unit
| ~ sP16 ),
inference(definition_unfolding,[],[f353,f42]) ).
fof(f538,plain,
( op(e3,e4) != unit
| ~ sP17 ),
inference(definition_unfolding,[],[f348,f42]) ).
fof(f543,plain,
( e2 != op(unit,e2)
| ~ sP22 ),
inference(definition_unfolding,[],[f327,f42]) ).
fof(f544,plain,
( e2 != op(e2,unit)
| ~ sP23 ),
inference(definition_unfolding,[],[f322,f42]) ).
fof(f548,plain,
( op(e1,e2) != unit
| ~ sP26 ),
inference(definition_unfolding,[],[f306,f42]) ).
fof(f553,plain,
( op(e2,e1) != unit
| ~ sP27 ),
inference(definition_unfolding,[],[f301,f42]) ).
fof(f563,plain,
( e1 != op(unit,e1)
| ~ sP34 ),
inference(definition_unfolding,[],[f267,f42]) ).
fof(f564,plain,
( e1 != op(e1,unit)
| ~ sP35 ),
inference(definition_unfolding,[],[f262,f42]) ).
fof(f567,plain,
( op(e2,e1) != unit
| ~ sP36 ),
inference(definition_unfolding,[],[f255,f42]) ).
fof(f572,plain,
( op(e1,e2) != unit
| ~ sP37 ),
inference(definition_unfolding,[],[f250,f42]) ).
fof(f579,plain,
( e4 != op(e4,unit)
| ~ sP38 ),
inference(definition_unfolding,[],[f243,f42]) ).
fof(f584,plain,
( e4 != op(unit,e4)
| ~ sP39 ),
inference(definition_unfolding,[],[f238,f42]) ).
fof(f588,plain,
( e3 != op(e3,unit)
| ~ sP40 ),
inference(definition_unfolding,[],[f234,f42]) ).
fof(f593,plain,
( e3 != op(unit,e3)
| ~ sP41 ),
inference(definition_unfolding,[],[f229,f42]) ).
fof(f597,plain,
( e2 != op(e2,unit)
| ~ sP42 ),
inference(definition_unfolding,[],[f225,f42]) ).
fof(f602,plain,
( e2 != op(unit,e2)
| ~ sP43 ),
inference(definition_unfolding,[],[f220,f42]) ).
fof(f606,plain,
( e1 != op(e1,unit)
| ~ sP44 ),
inference(definition_unfolding,[],[f216,f42]) ).
fof(f611,plain,
( e1 != op(unit,e1)
| ~ sP45 ),
inference(definition_unfolding,[],[f211,f42]) ).
fof(f615,plain,
( unit != op(unit,unit)
| ~ sP46 ),
inference(definition_unfolding,[],[f207,f42,f42,f42]) ).
fof(f620,plain,
( unit != op(unit,unit)
| ~ sP47 ),
inference(definition_unfolding,[],[f202,f42,f42,f42]) ).
fof(f625,plain,
( unit != unit
| ~ sP48 ),
inference(definition_unfolding,[],[f197,f42]) ).
fof(f627,plain,
( op(e4,e3) != unit
| ~ sP50 ),
inference(definition_unfolding,[],[f187,f42]) ).
fof(f634,plain,
( e4 != op(e4,unit)
| ~ sP53 ),
inference(definition_unfolding,[],[f168,f42]) ).
fof(f635,plain,
( op(e3,e4) != unit
| ~ sP54 ),
inference(definition_unfolding,[],[f167,f42]) ).
fof(f642,plain,
( e3 != op(e3,unit)
| ~ sP58 ),
inference(definition_unfolding,[],[f144,f42]) ).
fof(f647,plain,
( op(e2,e1) != unit
| ~ sP62 ),
inference(definition_unfolding,[],[f127,f42]) ).
fof(f650,plain,
( e2 != op(e2,unit)
| ~ sP63 ),
inference(definition_unfolding,[],[f120,f42]) ).
fof(f655,plain,
( op(e1,e2) != unit
| ~ sP66 ),
inference(definition_unfolding,[],[f107,f42]) ).
fof(f658,plain,
( e1 != op(e1,unit)
| ~ sP68 ),
inference(definition_unfolding,[],[f96,f42]) ).
fof(f666,plain,
( e4 != op(unit,e4)
| ~ sP69 ),
inference(definition_unfolding,[],[f88,f42]) ).
fof(f670,plain,
( e3 != op(unit,e3)
| ~ sP70 ),
inference(definition_unfolding,[],[f84,f42]) ).
fof(f674,plain,
( e2 != op(unit,e2)
| ~ sP71 ),
inference(definition_unfolding,[],[f80,f42]) ).
fof(f678,plain,
( e1 != op(unit,e1)
| ~ sP72 ),
inference(definition_unfolding,[],[f76,f42]) ).
fof(f682,plain,
( unit != op(unit,unit)
| ~ sP73 ),
inference(definition_unfolding,[],[f72,f42,f42,f42]) ).
fof(f691,plain,
( unit != op(unit,unit)
| ~ sP78 ),
inference(definition_unfolding,[],[f47,f42,f42,f42]) ).
fof(f716,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,[],[f500]) ).
fof(f725,plain,
( e2 != op(e4,e4)
| sP2 ),
inference(consistent_polarity_flipping,[],[f423]) ).
fof(f728,plain,
( e1 != op(e2,e4)
| sP4 ),
inference(consistent_polarity_flipping,[],[f415]) ).
fof(f734,plain,
( op(e3,e4) != unit
| sP6 ),
inference(consistent_polarity_flipping,[],[f514]) ).
fof(f738,plain,
( e4 != op(e3,e2)
| sP9 ),
inference(consistent_polarity_flipping,[],[f390]) ).
fof(f741,plain,
( e3 != op(unit,e3)
| sP10 ),
inference(consistent_polarity_flipping,[],[f523]) ).
fof(f747,plain,
( e2 != op(e1,e3)
| sP12 ),
inference(consistent_polarity_flipping,[],[f376]) ).
fof(f752,plain,
( e2 != op(e3,e1)
| sP13 ),
inference(consistent_polarity_flipping,[],[f371]) ).
fof(f759,plain,
( e1 != op(e3,e3)
| sP14 ),
inference(consistent_polarity_flipping,[],[f364]) ).
fof(f764,plain,
( e1 != op(e3,e3)
| sP15 ),
inference(consistent_polarity_flipping,[],[f359]) ).
fof(f770,plain,
( op(e4,e3) != unit
| sP16 ),
inference(consistent_polarity_flipping,[],[f533]) ).
fof(f773,plain,
( e3 != op(e2,e2)
| sP20 ),
inference(consistent_polarity_flipping,[],[f335]) ).
fof(f776,plain,
( e2 != op(unit,e2)
| sP22 ),
inference(consistent_polarity_flipping,[],[f543]) ).
fof(f785,plain,
( e1 != op(e4,e2)
| sP24 ),
inference(consistent_polarity_flipping,[],[f313]) ).
fof(f787,plain,
( e4 != op(e1,e1)
| sP29 ),
inference(consistent_polarity_flipping,[],[f291]) ).
fof(f795,plain,
( e3 != op(e4,e1)
| sP30 ),
inference(consistent_polarity_flipping,[],[f283]) ).
fof(f800,plain,
( e3 != op(e1,e4)
| sP31 ),
inference(consistent_polarity_flipping,[],[f278]) ).
fof(f804,plain,
( e2 != op(e3,e1)
| sP32 ),
inference(consistent_polarity_flipping,[],[f274]) ).
fof(f809,plain,
( e2 != op(e1,e3)
| sP33 ),
inference(consistent_polarity_flipping,[],[f269]) ).
fof(f815,plain,
( e4 != op(e4,unit)
| sP38 ),
inference(consistent_polarity_flipping,[],[f579]) ).
fof(f819,plain,
( e3 != op(e3,unit)
| sP40 ),
inference(consistent_polarity_flipping,[],[f588]) ).
fof(f823,plain,
( e2 != op(e2,unit)
| sP42 ),
inference(consistent_polarity_flipping,[],[f597]) ).
fof(f827,plain,
( e1 != op(unit,e1)
| sP45 ),
inference(consistent_polarity_flipping,[],[f611]) ).
fof(f831,plain,
( op(e4,e3) != unit
| sP50 ),
inference(consistent_polarity_flipping,[],[f627]) ).
fof(f837,plain,
( e1 != op(e4,e2)
| sP51 ),
inference(consistent_polarity_flipping,[],[f181]) ).
fof(f845,plain,
( e4 != op(e4,unit)
| sP53 ),
inference(consistent_polarity_flipping,[],[f634]) ).
fof(f846,plain,
( op(e3,e4) != unit
| sP54 ),
inference(consistent_polarity_flipping,[],[f635]) ).
fof(f854,plain,
( e3 != op(e3,unit)
| sP58 ),
inference(consistent_polarity_flipping,[],[f642]) ).
fof(f859,plain,
( e3 != op(e2,e2)
| sP61 ),
inference(consistent_polarity_flipping,[],[f129]) ).
fof(f863,plain,
( e2 != op(e2,unit)
| sP63 ),
inference(consistent_polarity_flipping,[],[f650]) ).
fof(f869,plain,
( e3 != op(e1,e4)
| sP64 ),
inference(consistent_polarity_flipping,[],[f114]) ).
fof(f873,plain,
( e2 != op(e1,e3)
| sP65 ),
inference(consistent_polarity_flipping,[],[f110]) ).
fof(f876,plain,
( op(e1,e2) != unit
| sP66 ),
inference(consistent_polarity_flipping,[],[f655]) ).
fof(f882,plain,
( e1 != op(e1,unit)
| sP68 ),
inference(consistent_polarity_flipping,[],[f658]) ).
fof(f888,plain,
( e2 != op(unit,e2)
| sP71 ),
inference(consistent_polarity_flipping,[],[f674]) ).
fof(f892,plain,
( e4 != op(e1,e1)
| sP74 ),
inference(consistent_polarity_flipping,[],[f66]) ).
fof(f898,plain,
( e3 != op(e2,e2)
| sP75 ),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f904,plain,
( e1 != op(e3,e3)
| sP77 ),
inference(consistent_polarity_flipping,[],[f49]) ).
fof(f906,plain,
( unit != op(unit,unit)
| sP78 ),
inference(consistent_polarity_flipping,[],[f691]) ).
fof(f911,plain,
~ sP48,
inference(trivial_inequality_removal,[],[f625]) ).
fof(f916,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,[],[f716]) ).
fof(f938,definition,
( spl79_1
<=> sP78 ),
introduced(definition,[new_symbols(definition,[spl79_1])],[avatar_definition]) ).
fof(f962,definition,
( spl79_6
<=> unit = op(unit,unit) ),
introduced(definition,[new_symbols(definition,[spl79_6])],[avatar_definition]) ).
fof(f965,plain,
( spl79_1
| ~ spl79_6 ),
inference(avatar_split_clause,[],[f906,f962,f938]) ).
fof(f967,definition,
( spl79_7
<=> sP77 ),
introduced(definition,[new_symbols(definition,[spl79_7])],[avatar_definition]) ).
fof(f976,definition,
( spl79_9
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl79_9])],[avatar_definition]) ).
fof(f979,plain,
( spl79_7
| ~ spl79_9 ),
inference(avatar_split_clause,[],[f904,f976,f967]) ).
fof(f996,definition,
( spl79_13
<=> sP76 ),
introduced(definition,[new_symbols(definition,[spl79_13])],[avatar_definition]) ).
fof(f1000,definition,
( spl79_14
<=> e2 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl79_14])],[avatar_definition]) ).
fof(f1003,plain,
( ~ spl79_13
| ~ spl79_14 ),
inference(avatar_split_clause,[],[f53,f1000,f996]) ).
fof(f1025,definition,
( spl79_19
<=> sP75 ),
introduced(definition,[new_symbols(definition,[spl79_19])],[avatar_definition]) ).
fof(f1039,definition,
( spl79_22
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl79_22])],[avatar_definition]) ).
fof(f1042,plain,
( spl79_19
| ~ spl79_22 ),
inference(avatar_split_clause,[],[f898,f1039,f1025]) ).
fof(f1054,definition,
( spl79_25
<=> sP74 ),
introduced(definition,[new_symbols(definition,[spl79_25])],[avatar_definition]) ).
fof(f1073,definition,
( spl79_29
<=> e4 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl79_29])],[avatar_definition]) ).
fof(f1076,plain,
( spl79_25
| ~ spl79_29 ),
inference(avatar_split_clause,[],[f892,f1073,f1054]) ).
fof(f1083,definition,
( spl79_31
<=> sP73 ),
introduced(definition,[new_symbols(definition,[spl79_31])],[avatar_definition]) ).
fof(f1090,plain,
( ~ spl79_31
| ~ spl79_6 ),
inference(avatar_split_clause,[],[f682,f962,f1083]) ).
fof(f1092,definition,
( spl79_32
<=> sP72 ),
introduced(definition,[new_symbols(definition,[spl79_32])],[avatar_definition]) ).
fof(f1111,definition,
( spl79_36
<=> e1 = op(unit,e1) ),
introduced(definition,[new_symbols(definition,[spl79_36])],[avatar_definition]) ).
fof(f1114,plain,
( ~ spl79_32
| ~ spl79_36 ),
inference(avatar_split_clause,[],[f678,f1111,f1092]) ).
fof(f1121,definition,
( spl79_38
<=> sP71 ),
introduced(definition,[new_symbols(definition,[spl79_38])],[avatar_definition]) ).
fof(f1135,definition,
( spl79_41
<=> e2 = op(unit,e2) ),
introduced(definition,[new_symbols(definition,[spl79_41])],[avatar_definition]) ).
fof(f1138,plain,
( spl79_38
| ~ spl79_41 ),
inference(avatar_split_clause,[],[f888,f1135,f1121]) ).
fof(f1150,definition,
( spl79_44
<=> sP70 ),
introduced(definition,[new_symbols(definition,[spl79_44])],[avatar_definition]) ).
fof(f1159,definition,
( spl79_46
<=> e3 = op(unit,e3) ),
introduced(definition,[new_symbols(definition,[spl79_46])],[avatar_definition]) ).
fof(f1162,plain,
( ~ spl79_44
| ~ spl79_46 ),
inference(avatar_split_clause,[],[f670,f1159,f1150]) ).
fof(f1179,definition,
( spl79_50
<=> sP69 ),
introduced(definition,[new_symbols(definition,[spl79_50])],[avatar_definition]) ).
fof(f1183,definition,
( spl79_51
<=> e4 = op(unit,e4) ),
introduced(definition,[new_symbols(definition,[spl79_51])],[avatar_definition]) ).
fof(f1186,plain,
( ~ spl79_50
| ~ spl79_51 ),
inference(avatar_split_clause,[],[f666,f1183,f1179]) ).
fof(f1208,definition,
( spl79_56
<=> sP68 ),
introduced(definition,[new_symbols(definition,[spl79_56])],[avatar_definition]) ).
fof(f1227,definition,
( spl79_60
<=> e1 = op(e1,unit) ),
introduced(definition,[new_symbols(definition,[spl79_60])],[avatar_definition]) ).
fof(f1230,plain,
( spl79_56
| ~ spl79_60 ),
inference(avatar_split_clause,[],[f882,f1227,f1208]) ).
fof(f1237,definition,
( spl79_62
<=> sP67 ),
introduced(definition,[new_symbols(definition,[spl79_62])],[avatar_definition]) ).
fof(f1240,plain,
( ~ spl79_62
| ~ spl79_29 ),
inference(avatar_split_clause,[],[f98,f1073,f1237]) ).
fof(f1246,definition,
( spl79_63
<=> sP66 ),
introduced(definition,[new_symbols(definition,[spl79_63])],[avatar_definition]) ).
fof(f1270,definition,
( spl79_68
<=> op(e1,e2) = unit ),
introduced(definition,[new_symbols(definition,[spl79_68])],[avatar_definition]) ).
fof(f1273,plain,
( spl79_63
| ~ spl79_68 ),
inference(avatar_split_clause,[],[f876,f1270,f1246]) ).
fof(f1275,definition,
( spl79_69
<=> sP65 ),
introduced(definition,[new_symbols(definition,[spl79_69])],[avatar_definition]) ).
fof(f1289,definition,
( spl79_72
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl79_72])],[avatar_definition]) ).
fof(f1292,plain,
( spl79_69
| ~ spl79_72 ),
inference(avatar_split_clause,[],[f873,f1289,f1275]) ).
fof(f1304,definition,
( spl79_75
<=> sP64 ),
introduced(definition,[new_symbols(definition,[spl79_75])],[avatar_definition]) ).
fof(f1313,definition,
( spl79_77
<=> e3 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl79_77])],[avatar_definition]) ).
fof(f1316,plain,
( spl79_75
| ~ spl79_77 ),
inference(avatar_split_clause,[],[f869,f1313,f1304]) ).
fof(f1333,definition,
( spl79_81
<=> sP63 ),
introduced(definition,[new_symbols(definition,[spl79_81])],[avatar_definition]) ).
fof(f1347,definition,
( spl79_84
<=> e2 = op(e2,unit) ),
introduced(definition,[new_symbols(definition,[spl79_84])],[avatar_definition]) ).
fof(f1350,plain,
( spl79_81
| ~ spl79_84 ),
inference(avatar_split_clause,[],[f863,f1347,f1333]) ).
fof(f1362,definition,
( spl79_87
<=> sP62 ),
introduced(definition,[new_symbols(definition,[spl79_87])],[avatar_definition]) ).
fof(f1386,definition,
( spl79_92
<=> op(e2,e1) = unit ),
introduced(definition,[new_symbols(definition,[spl79_92])],[avatar_definition]) ).
fof(f1389,plain,
( ~ spl79_87
| ~ spl79_92 ),
inference(avatar_split_clause,[],[f647,f1386,f1362]) ).
fof(f1391,definition,
( spl79_93
<=> sP61 ),
introduced(definition,[new_symbols(definition,[spl79_93])],[avatar_definition]) ).
fof(f1395,plain,
( spl79_93
| ~ spl79_22 ),
inference(avatar_split_clause,[],[f859,f1039,f1391]) ).
fof(f1400,definition,
( spl79_94
<=> sP60 ),
introduced(definition,[new_symbols(definition,[spl79_94])],[avatar_definition]) ).
fof(f1404,definition,
( spl79_95
<=> e4 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl79_95])],[avatar_definition]) ).
fof(f1407,plain,
( ~ spl79_94
| ~ spl79_95 ),
inference(avatar_split_clause,[],[f133,f1404,f1400]) ).
fof(f1429,definition,
( spl79_100
<=> sP59 ),
introduced(definition,[new_symbols(definition,[spl79_100])],[avatar_definition]) ).
fof(f1448,definition,
( spl79_104
<=> e1 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl79_104])],[avatar_definition]) ).
fof(f1451,plain,
( ~ spl79_100
| ~ spl79_104 ),
inference(avatar_split_clause,[],[f141,f1448,f1429]) ).
fof(f1458,definition,
( spl79_106
<=> sP58 ),
introduced(definition,[new_symbols(definition,[spl79_106])],[avatar_definition]) ).
fof(f1467,definition,
( spl79_108
<=> e3 = op(e3,unit) ),
introduced(definition,[new_symbols(definition,[spl79_108])],[avatar_definition]) ).
fof(f1470,plain,
( spl79_106
| ~ spl79_108 ),
inference(avatar_split_clause,[],[f854,f1467,f1458]) ).
fof(f1487,definition,
( spl79_112
<=> sP57 ),
introduced(definition,[new_symbols(definition,[spl79_112])],[avatar_definition]) ).
fof(f1501,definition,
( spl79_115
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl79_115])],[avatar_definition]) ).
fof(f1504,plain,
( ~ spl79_112
| ~ spl79_115 ),
inference(avatar_split_clause,[],[f150,f1501,f1487]) ).
fof(f1516,definition,
( spl79_118
<=> sP56 ),
introduced(definition,[new_symbols(definition,[spl79_118])],[avatar_definition]) ).
fof(f1520,definition,
( spl79_119
<=> e4 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl79_119])],[avatar_definition]) ).
fof(f1523,plain,
( ~ spl79_118
| ~ spl79_119 ),
inference(avatar_split_clause,[],[f153,f1520,f1516]) ).
fof(f1545,definition,
( spl79_124
<=> sP55 ),
introduced(definition,[new_symbols(definition,[spl79_124])],[avatar_definition]) ).
fof(f1551,plain,
( ~ spl79_124
| ~ spl79_9 ),
inference(avatar_split_clause,[],[f161,f976,f1545]) ).
fof(f1554,definition,
( spl79_125
<=> sP54 ),
introduced(definition,[new_symbols(definition,[spl79_125])],[avatar_definition]) ).
fof(f1578,definition,
( spl79_130
<=> op(e3,e4) = unit ),
introduced(definition,[new_symbols(definition,[spl79_130])],[avatar_definition]) ).
fof(f1581,plain,
( spl79_125
| ~ spl79_130 ),
inference(avatar_split_clause,[],[f846,f1578,f1554]) ).
fof(f1583,definition,
( spl79_131
<=> sP53 ),
introduced(definition,[new_symbols(definition,[spl79_131])],[avatar_definition]) ).
fof(f1587,definition,
( spl79_132
<=> e4 = op(e4,unit) ),
introduced(definition,[new_symbols(definition,[spl79_132])],[avatar_definition]) ).
fof(f1590,plain,
( spl79_131
| ~ spl79_132 ),
inference(avatar_split_clause,[],[f845,f1587,f1583]) ).
fof(f1612,definition,
( spl79_137
<=> sP52 ),
introduced(definition,[new_symbols(definition,[spl79_137])],[avatar_definition]) ).
fof(f1621,definition,
( spl79_139
<=> e3 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl79_139])],[avatar_definition]) ).
fof(f1624,plain,
( ~ spl79_137
| ~ spl79_139 ),
inference(avatar_split_clause,[],[f174,f1621,f1612]) ).
fof(f1641,definition,
( spl79_143
<=> sP51 ),
introduced(definition,[new_symbols(definition,[spl79_143])],[avatar_definition]) ).
fof(f1660,definition,
( spl79_147
<=> e1 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl79_147])],[avatar_definition]) ).
fof(f1663,plain,
( spl79_143
| ~ spl79_147 ),
inference(avatar_split_clause,[],[f837,f1660,f1641]) ).
fof(f1670,definition,
( spl79_149
<=> sP50 ),
introduced(definition,[new_symbols(definition,[spl79_149])],[avatar_definition]) ).
fof(f1694,definition,
( spl79_154
<=> op(e4,e3) = unit ),
introduced(definition,[new_symbols(definition,[spl79_154])],[avatar_definition]) ).
fof(f1697,plain,
( spl79_149
| ~ spl79_154 ),
inference(avatar_split_clause,[],[f831,f1694,f1670]) ).
fof(f1699,definition,
( spl79_155
<=> sP49 ),
introduced(definition,[new_symbols(definition,[spl79_155])],[avatar_definition]) ).
fof(f1704,plain,
( ~ spl79_155
| ~ spl79_14 ),
inference(avatar_split_clause,[],[f190,f1000,f1699]) ).
fof(f1708,definition,
( spl79_156
<=> sP48 ),
introduced(definition,[new_symbols(definition,[spl79_156])],[avatar_definition]) ).
fof(f1731,plain,
~ spl79_156,
inference(avatar_split_clause,[],[f911,f1708]) ).
fof(f1733,definition,
( spl79_161
<=> sP47 ),
introduced(definition,[new_symbols(definition,[spl79_161])],[avatar_definition]) ).
fof(f1740,plain,
( ~ spl79_161
| ~ spl79_6 ),
inference(avatar_split_clause,[],[f620,f962,f1733]) ).
fof(f1742,definition,
( spl79_162
<=> sP46 ),
introduced(definition,[new_symbols(definition,[spl79_162])],[avatar_definition]) ).
fof(f1749,plain,
( ~ spl79_162
| ~ spl79_6 ),
inference(avatar_split_clause,[],[f615,f962,f1742]) ).
fof(f1751,definition,
( spl79_163
<=> sP45 ),
introduced(definition,[new_symbols(definition,[spl79_163])],[avatar_definition]) ).
fof(f1757,plain,
( spl79_163
| ~ spl79_36 ),
inference(avatar_split_clause,[],[f827,f1111,f1751]) ).
fof(f1760,definition,
( spl79_164
<=> sP44 ),
introduced(definition,[new_symbols(definition,[spl79_164])],[avatar_definition]) ).
fof(f1766,plain,
( ~ spl79_164
| ~ spl79_60 ),
inference(avatar_split_clause,[],[f606,f1227,f1760]) ).
fof(f1769,definition,
( spl79_165
<=> sP43 ),
introduced(definition,[new_symbols(definition,[spl79_165])],[avatar_definition]) ).
fof(f1774,plain,
( ~ spl79_165
| ~ spl79_41 ),
inference(avatar_split_clause,[],[f602,f1135,f1769]) ).
fof(f1778,definition,
( spl79_166
<=> sP42 ),
introduced(definition,[new_symbols(definition,[spl79_166])],[avatar_definition]) ).
fof(f1783,plain,
( spl79_166
| ~ spl79_84 ),
inference(avatar_split_clause,[],[f823,f1347,f1778]) ).
fof(f1787,definition,
( spl79_167
<=> sP41 ),
introduced(definition,[new_symbols(definition,[spl79_167])],[avatar_definition]) ).
fof(f1791,plain,
( ~ spl79_167
| ~ spl79_46 ),
inference(avatar_split_clause,[],[f593,f1159,f1787]) ).
fof(f1796,definition,
( spl79_168
<=> sP40 ),
introduced(definition,[new_symbols(definition,[spl79_168])],[avatar_definition]) ).
fof(f1800,plain,
( spl79_168
| ~ spl79_108 ),
inference(avatar_split_clause,[],[f819,f1467,f1796]) ).
fof(f1805,definition,
( spl79_169
<=> sP39 ),
introduced(definition,[new_symbols(definition,[spl79_169])],[avatar_definition]) ).
fof(f1808,plain,
( ~ spl79_169
| ~ spl79_51 ),
inference(avatar_split_clause,[],[f584,f1183,f1805]) ).
fof(f1814,definition,
( spl79_170
<=> sP38 ),
introduced(definition,[new_symbols(definition,[spl79_170])],[avatar_definition]) ).
fof(f1817,plain,
( spl79_170
| ~ spl79_132 ),
inference(avatar_split_clause,[],[f815,f1587,f1814]) ).
fof(f1823,definition,
( spl79_171
<=> sP37 ),
introduced(definition,[new_symbols(definition,[spl79_171])],[avatar_definition]) ).
fof(f1828,plain,
( ~ spl79_171
| ~ spl79_68 ),
inference(avatar_split_clause,[],[f572,f1270,f1823]) ).
fof(f1832,definition,
( spl79_172
<=> sP36 ),
introduced(definition,[new_symbols(definition,[spl79_172])],[avatar_definition]) ).
fof(f1837,plain,
( ~ spl79_172
| ~ spl79_92 ),
inference(avatar_split_clause,[],[f567,f1386,f1832]) ).
fof(f1841,definition,
( spl79_173
<=> sP35 ),
introduced(definition,[new_symbols(definition,[spl79_173])],[avatar_definition]) ).
fof(f1848,plain,
( ~ spl79_173
| ~ spl79_60 ),
inference(avatar_split_clause,[],[f564,f1227,f1841]) ).
fof(f1850,definition,
( spl79_174
<=> sP34 ),
introduced(definition,[new_symbols(definition,[spl79_174])],[avatar_definition]) ).
fof(f1857,plain,
( ~ spl79_174
| ~ spl79_36 ),
inference(avatar_split_clause,[],[f563,f1111,f1850]) ).
fof(f1859,definition,
( spl79_175
<=> sP33 ),
introduced(definition,[new_symbols(definition,[spl79_175])],[avatar_definition]) ).
fof(f1863,plain,
( spl79_175
| ~ spl79_72 ),
inference(avatar_split_clause,[],[f809,f1289,f1859]) ).
fof(f1868,definition,
( spl79_176
<=> sP32 ),
introduced(definition,[new_symbols(definition,[spl79_176])],[avatar_definition]) ).
fof(f1872,plain,
( spl79_176
| ~ spl79_115 ),
inference(avatar_split_clause,[],[f804,f1501,f1868]) ).
fof(f1877,definition,
( spl79_177
<=> sP31 ),
introduced(definition,[new_symbols(definition,[spl79_177])],[avatar_definition]) ).
fof(f1880,plain,
( spl79_177
| ~ spl79_77 ),
inference(avatar_split_clause,[],[f800,f1313,f1877]) ).
fof(f1886,definition,
( spl79_178
<=> sP30 ),
introduced(definition,[new_symbols(definition,[spl79_178])],[avatar_definition]) ).
fof(f1889,plain,
( spl79_178
| ~ spl79_139 ),
inference(avatar_split_clause,[],[f795,f1621,f1886]) ).
fof(f1895,definition,
( spl79_179
<=> sP29 ),
introduced(definition,[new_symbols(definition,[spl79_179])],[avatar_definition]) ).
fof(f1901,plain,
( spl79_179
| ~ spl79_29 ),
inference(avatar_split_clause,[],[f787,f1073,f1895]) ).
fof(f1904,definition,
( spl79_180
<=> sP28 ),
introduced(definition,[new_symbols(definition,[spl79_180])],[avatar_definition]) ).
fof(f1910,plain,
( ~ spl79_180
| ~ spl79_29 ),
inference(avatar_split_clause,[],[f296,f1073,f1904]) ).
fof(f1913,definition,
( spl79_181
<=> sP27 ),
introduced(definition,[new_symbols(definition,[spl79_181])],[avatar_definition]) ).
fof(f1919,plain,
( ~ spl79_181
| ~ spl79_92 ),
inference(avatar_split_clause,[],[f553,f1386,f1913]) ).
fof(f1922,definition,
( spl79_182
<=> sP26 ),
introduced(definition,[new_symbols(definition,[spl79_182])],[avatar_definition]) ).
fof(f1928,plain,
( ~ spl79_182
| ~ spl79_68 ),
inference(avatar_split_clause,[],[f548,f1270,f1922]) ).
fof(f1931,definition,
( spl79_183
<=> sP25 ),
introduced(definition,[new_symbols(definition,[spl79_183])],[avatar_definition]) ).
fof(f1934,plain,
( ~ spl79_183
| ~ spl79_104 ),
inference(avatar_split_clause,[],[f308,f1448,f1931]) ).
fof(f1940,definition,
( spl79_184
<=> sP24 ),
introduced(definition,[new_symbols(definition,[spl79_184])],[avatar_definition]) ).
fof(f1943,plain,
( spl79_184
| ~ spl79_147 ),
inference(avatar_split_clause,[],[f785,f1660,f1940]) ).
fof(f1949,definition,
( spl79_185
<=> sP23 ),
introduced(definition,[new_symbols(definition,[spl79_185])],[avatar_definition]) ).
fof(f1956,plain,
( ~ spl79_185
| ~ spl79_84 ),
inference(avatar_split_clause,[],[f544,f1347,f1949]) ).
fof(f1958,definition,
( spl79_186
<=> sP22 ),
introduced(definition,[new_symbols(definition,[spl79_186])],[avatar_definition]) ).
fof(f1965,plain,
( spl79_186
| ~ spl79_41 ),
inference(avatar_split_clause,[],[f776,f1135,f1958]) ).
fof(f1967,definition,
( spl79_187
<=> sP21 ),
introduced(definition,[new_symbols(definition,[spl79_187])],[avatar_definition]) ).
fof(f1972,plain,
( ~ spl79_187
| ~ spl79_22 ),
inference(avatar_split_clause,[],[f330,f1039,f1967]) ).
fof(f1976,definition,
( spl79_188
<=> sP20 ),
introduced(definition,[new_symbols(definition,[spl79_188])],[avatar_definition]) ).
fof(f1981,plain,
( spl79_188
| ~ spl79_22 ),
inference(avatar_split_clause,[],[f773,f1039,f1976]) ).
fof(f1985,definition,
( spl79_189
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl79_189])],[avatar_definition]) ).
fof(f1989,plain,
( ~ spl79_189
| ~ spl79_95 ),
inference(avatar_split_clause,[],[f339,f1404,f1985]) ).
fof(f1994,definition,
( spl79_190
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl79_190])],[avatar_definition]) ).
fof(f1998,plain,
( ~ spl79_190
| ~ spl79_119 ),
inference(avatar_split_clause,[],[f344,f1520,f1994]) ).
fof(f2003,definition,
( spl79_191
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl79_191])],[avatar_definition]) ).
fof(f2006,plain,
( ~ spl79_191
| ~ spl79_130 ),
inference(avatar_split_clause,[],[f538,f1578,f2003]) ).
fof(f2012,definition,
( spl79_192
<=> sP16 ),
introduced(definition,[new_symbols(definition,[spl79_192])],[avatar_definition]) ).
fof(f2015,plain,
( spl79_192
| ~ spl79_154 ),
inference(avatar_split_clause,[],[f770,f1694,f2012]) ).
fof(f2021,definition,
( spl79_193
<=> sP15 ),
introduced(definition,[new_symbols(definition,[spl79_193])],[avatar_definition]) ).
fof(f2025,plain,
( spl79_193
| ~ spl79_9 ),
inference(avatar_split_clause,[],[f764,f976,f2021]) ).
fof(f2030,definition,
( spl79_194
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl79_194])],[avatar_definition]) ).
fof(f2034,plain,
( spl79_194
| ~ spl79_9 ),
inference(avatar_split_clause,[],[f759,f976,f2030]) ).
fof(f2039,definition,
( spl79_195
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl79_195])],[avatar_definition]) ).
fof(f2045,plain,
( spl79_195
| ~ spl79_115 ),
inference(avatar_split_clause,[],[f752,f1501,f2039]) ).
fof(f2048,definition,
( spl79_196
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl79_196])],[avatar_definition]) ).
fof(f2054,plain,
( spl79_196
| ~ spl79_72 ),
inference(avatar_split_clause,[],[f747,f1289,f2048]) ).
fof(f2057,definition,
( spl79_197
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl79_197])],[avatar_definition]) ).
fof(f2064,plain,
( ~ spl79_197
| ~ spl79_108 ),
inference(avatar_split_clause,[],[f524,f1467,f2057]) ).
fof(f2066,definition,
( spl79_198
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl79_198])],[avatar_definition]) ).
fof(f2073,plain,
( spl79_198
| ~ spl79_46 ),
inference(avatar_split_clause,[],[f741,f1159,f2066]) ).
fof(f2075,definition,
( spl79_199
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl79_199])],[avatar_definition]) ).
fof(f2080,plain,
( spl79_199
| ~ spl79_119 ),
inference(avatar_split_clause,[],[f738,f1520,f2075]) ).
fof(f2084,definition,
( spl79_200
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl79_200])],[avatar_definition]) ).
fof(f2089,plain,
( ~ spl79_200
| ~ spl79_95 ),
inference(avatar_split_clause,[],[f395,f1404,f2084]) ).
fof(f2093,definition,
( spl79_201
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl79_201])],[avatar_definition]) ).
fof(f2097,plain,
( ~ spl79_201
| ~ spl79_154 ),
inference(avatar_split_clause,[],[f519,f1694,f2093]) ).
fof(f2102,definition,
( spl79_202
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl79_202])],[avatar_definition]) ).
fof(f2106,plain,
( spl79_202
| ~ spl79_130 ),
inference(avatar_split_clause,[],[f734,f1578,f2102]) ).
fof(f2111,definition,
( spl79_203
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl79_203])],[avatar_definition]) ).
fof(f2116,plain,
( ~ spl79_203
| ~ spl79_147 ),
inference(avatar_split_clause,[],[f410,f1660,f2111]) ).
fof(f2120,definition,
( spl79_204
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl79_204])],[avatar_definition]) ).
fof(f2125,plain,
( spl79_204
| ~ spl79_104 ),
inference(avatar_split_clause,[],[f728,f1448,f2120]) ).
fof(f2129,definition,
( spl79_205
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl79_205])],[avatar_definition]) ).
fof(f2132,plain,
( ~ spl79_205
| ~ spl79_14 ),
inference(avatar_split_clause,[],[f418,f1000,f2129]) ).
fof(f2138,definition,
( spl79_206
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl79_206])],[avatar_definition]) ).
fof(f2141,plain,
( spl79_206
| ~ spl79_14 ),
inference(avatar_split_clause,[],[f725,f1000,f2138]) ).
fof(f2147,definition,
( spl79_207
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl79_207])],[avatar_definition]) ).
fof(f2153,plain,
( ~ spl79_207
| ~ spl79_139 ),
inference(avatar_split_clause,[],[f431,f1621,f2147]) ).
fof(f2156,definition,
( spl79_208
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl79_208])],[avatar_definition]) ).
fof(f2162,plain,
( ~ spl79_208
| ~ spl79_77 ),
inference(avatar_split_clause,[],[f436,f1313,f2156]) ).
fof(f2168,plain,
( ~ spl79_1
| ~ spl79_7
| spl79_13
| ~ spl79_19
| ~ spl79_25
| spl79_31
| spl79_32
| ~ spl79_38
| spl79_44
| spl79_50
| ~ spl79_56
| spl79_62
| ~ spl79_63
| ~ spl79_69
| ~ spl79_75
| ~ spl79_81
| spl79_87
| ~ spl79_93
| spl79_94
| spl79_100
| ~ spl79_106
| spl79_112
| spl79_118
| spl79_124
| ~ spl79_125
| ~ spl79_131
| spl79_137
| ~ spl79_143
| ~ spl79_149
| spl79_155
| ~ spl79_6
| ~ spl79_36
| ~ spl79_60
| ~ spl79_41
| ~ spl79_84
| ~ spl79_46
| ~ spl79_108
| spl79_156
| spl79_161
| spl79_162
| ~ spl79_163
| spl79_164
| spl79_165
| ~ spl79_166
| spl79_167
| ~ spl79_168
| spl79_169
| ~ spl79_170
| spl79_171
| spl79_172
| spl79_173
| spl79_174
| ~ spl79_175
| ~ spl79_176
| ~ spl79_177
| ~ spl79_178
| ~ spl79_179
| spl79_180
| spl79_181
| spl79_182
| spl79_183
| ~ spl79_184
| spl79_185
| ~ spl79_186
| spl79_187
| ~ spl79_188
| spl79_189
| spl79_190
| spl79_191
| ~ spl79_192
| ~ spl79_193
| ~ spl79_194
| ~ spl79_195
| ~ spl79_196
| spl79_197
| ~ spl79_198
| ~ spl79_199
| spl79_200
| spl79_201
| ~ spl79_202
| spl79_203
| ~ spl79_204
| spl79_205
| ~ spl79_206
| spl79_207
| spl79_208
| ~ spl79_132
| ~ spl79_51 ),
inference(avatar_split_clause,[],[f916,f1183,f1587,f2156,f2147,f2138,f2129,f2120,f2111,f2102,f2093,f2084,f2075,f2066,f2057,f2048,f2039,f2030,f2021,f2012,f2003,f1994,f1985,f1976,f1967,f1958,f1949,f1940,f1931,f1922,f1913,f1904,f1895,f1886,f1877,f1868,f1859,f1850,f1841,f1832,f1823,f1814,f1805,f1796,f1787,f1778,f1769,f1760,f1751,f1742,f1733,f1708,f1467,f1159,f1347,f1135,f1227,f1111,f962,f1699,f1670,f1641,f1612,f1583,f1554,f1545,f1516,f1487,f1458,f1429,f1400,f1391,f1362,f1333,f1304,f1275,f1246,f1237,f1208,f1179,f1150,f1121,f1092,f1083,f1054,f1025,f996,f967,f938]) ).
fof(f2189,plain,
spl79_14,
inference(avatar_split_clause,[],[f17,f1000]) ).
fof(f2190,plain,
spl79_154,
inference(avatar_split_clause,[],[f479,f1694]) ).
fof(f2191,plain,
spl79_147,
inference(avatar_split_clause,[],[f19,f1660]) ).
fof(f2192,plain,
spl79_139,
inference(avatar_split_clause,[],[f20,f1621]) ).
fof(f2193,plain,
spl79_132,
inference(avatar_split_clause,[],[f478,f1587]) ).
fof(f2194,plain,
spl79_130,
inference(avatar_split_clause,[],[f477,f1578]) ).
fof(f2195,plain,
spl79_9,
inference(avatar_split_clause,[],[f23,f976]) ).
fof(f2196,plain,
spl79_119,
inference(avatar_split_clause,[],[f24,f1520]) ).
fof(f2197,plain,
spl79_115,
inference(avatar_split_clause,[],[f25,f1501]) ).
fof(f2198,plain,
spl79_108,
inference(avatar_split_clause,[],[f476,f1467]) ).
fof(f2199,plain,
spl79_104,
inference(avatar_split_clause,[],[f27,f1448]) ).
fof(f2200,plain,
spl79_95,
inference(avatar_split_clause,[],[f28,f1404]) ).
fof(f2201,plain,
spl79_22,
inference(avatar_split_clause,[],[f29,f1039]) ).
fof(f2202,plain,
spl79_92,
inference(avatar_split_clause,[],[f475,f1386]) ).
fof(f2203,plain,
spl79_84,
inference(avatar_split_clause,[],[f474,f1347]) ).
fof(f2204,plain,
spl79_77,
inference(avatar_split_clause,[],[f32,f1313]) ).
fof(f2205,plain,
spl79_72,
inference(avatar_split_clause,[],[f33,f1289]) ).
fof(f2206,plain,
spl79_68,
inference(avatar_split_clause,[],[f473,f1270]) ).
fof(f2207,plain,
spl79_29,
inference(avatar_split_clause,[],[f35,f1073]) ).
fof(f2208,plain,
spl79_60,
inference(avatar_split_clause,[],[f472,f1227]) ).
fof(f2209,plain,
spl79_51,
inference(avatar_split_clause,[],[f471,f1183]) ).
fof(f2210,plain,
spl79_46,
inference(avatar_split_clause,[],[f470,f1159]) ).
fof(f2211,plain,
spl79_41,
inference(avatar_split_clause,[],[f469,f1135]) ).
fof(f2212,plain,
spl79_36,
inference(avatar_split_clause,[],[f468,f1111]) ).
fof(f2213,plain,
spl79_6,
inference(avatar_split_clause,[],[f467,f962]) ).
cnf(s5,plain,
( spl79_1
| ~ spl79_6 ),
inference(sat_conversion,[],[f965]) ).
cnf(s7,plain,
( spl79_7
| ~ spl79_9 ),
inference(sat_conversion,[],[f979]) ).
cnf(s11,plain,
( ~ spl79_13
| ~ spl79_14 ),
inference(sat_conversion,[],[f1003]) ).
cnf(s18,plain,
( spl79_19
| ~ spl79_22 ),
inference(sat_conversion,[],[f1042]) ).
cnf(s24,plain,
( spl79_25
| ~ spl79_29 ),
inference(sat_conversion,[],[f1076]) ).
cnf(s30,plain,
( ~ spl79_6
| ~ spl79_31 ),
inference(sat_conversion,[],[f1090]) ).
cnf(s34,plain,
( ~ spl79_32
| ~ spl79_36 ),
inference(sat_conversion,[],[f1114]) ).
cnf(s38,plain,
( spl79_38
| ~ spl79_41 ),
inference(sat_conversion,[],[f1138]) ).
cnf(s42,plain,
( ~ spl79_44
| ~ spl79_46 ),
inference(sat_conversion,[],[f1162]) ).
cnf(s46,plain,
( ~ spl79_50
| ~ spl79_51 ),
inference(sat_conversion,[],[f1186]) ).
cnf(s54,plain,
( spl79_56
| ~ spl79_60 ),
inference(sat_conversion,[],[f1230]) ).
cnf(s56,plain,
( ~ spl79_29
| ~ spl79_62 ),
inference(sat_conversion,[],[f1240]) ).
cnf(s65,plain,
( spl79_63
| ~ spl79_68 ),
inference(sat_conversion,[],[f1273]) ).
cnf(s68,plain,
( spl79_69
| ~ spl79_72 ),
inference(sat_conversion,[],[f1292]) ).
cnf(s72,plain,
( spl79_75
| ~ spl79_77 ),
inference(sat_conversion,[],[f1316]) ).
cnf(s78,plain,
( spl79_81
| ~ spl79_84 ),
inference(sat_conversion,[],[f1350]) ).
cnf(s85,plain,
( ~ spl79_87
| ~ spl79_92 ),
inference(sat_conversion,[],[f1389]) ).
cnf(s87,plain,
( ~ spl79_22
| spl79_93 ),
inference(sat_conversion,[],[f1395]) ).
cnf(s91,plain,
( ~ spl79_94
| ~ spl79_95 ),
inference(sat_conversion,[],[f1407]) ).
cnf(s99,plain,
( ~ spl79_100
| ~ spl79_104 ),
inference(sat_conversion,[],[f1451]) ).
cnf(s102,plain,
( spl79_106
| ~ spl79_108 ),
inference(sat_conversion,[],[f1470]) ).
cnf(s108,plain,
( ~ spl79_112
| ~ spl79_115 ),
inference(sat_conversion,[],[f1504]) ).
cnf(s111,plain,
( ~ spl79_118
| ~ spl79_119 ),
inference(sat_conversion,[],[f1523]) ).
cnf(s119,plain,
( ~ spl79_9
| ~ spl79_124 ),
inference(sat_conversion,[],[f1551]) ).
cnf(s125,plain,
( spl79_125
| ~ spl79_130 ),
inference(sat_conversion,[],[f1581]) ).
cnf(s126,plain,
( spl79_131
| ~ spl79_132 ),
inference(sat_conversion,[],[f1590]) ).
cnf(s132,plain,
( ~ spl79_137
| ~ spl79_139 ),
inference(sat_conversion,[],[f1624]) ).
cnf(s139,plain,
( spl79_143
| ~ spl79_147 ),
inference(sat_conversion,[],[f1663]) ).
cnf(s145,plain,
( spl79_149
| ~ spl79_154 ),
inference(sat_conversion,[],[f1697]) ).
cnf(s148,plain,
( ~ spl79_14
| ~ spl79_155 ),
inference(sat_conversion,[],[f1704]) ).
cnf(s155,plain,
~ spl79_156,
inference(sat_conversion,[],[f1731]) ).
cnf(s160,plain,
( ~ spl79_6
| ~ spl79_161 ),
inference(sat_conversion,[],[f1740]) ).
cnf(s165,plain,
( ~ spl79_6
| ~ spl79_162 ),
inference(sat_conversion,[],[f1749]) ).
cnf(s169,plain,
( ~ spl79_36
| spl79_163 ),
inference(sat_conversion,[],[f1757]) ).
cnf(s174,plain,
( ~ spl79_60
| ~ spl79_164 ),
inference(sat_conversion,[],[f1766]) ).
cnf(s178,plain,
( ~ spl79_41
| ~ spl79_165 ),
inference(sat_conversion,[],[f1774]) ).
cnf(s183,plain,
( ~ spl79_84
| spl79_166 ),
inference(sat_conversion,[],[f1783]) ).
cnf(s187,plain,
( ~ spl79_46
| ~ spl79_167 ),
inference(sat_conversion,[],[f1791]) ).
cnf(s192,plain,
( ~ spl79_108
| spl79_168 ),
inference(sat_conversion,[],[f1800]) ).
cnf(s196,plain,
( ~ spl79_51
| ~ spl79_169 ),
inference(sat_conversion,[],[f1808]) ).
cnf(s201,plain,
( ~ spl79_132
| spl79_170 ),
inference(sat_conversion,[],[f1817]) ).
cnf(s208,plain,
( ~ spl79_68
| ~ spl79_171 ),
inference(sat_conversion,[],[f1828]) ).
cnf(s213,plain,
( ~ spl79_92
| ~ spl79_172 ),
inference(sat_conversion,[],[f1837]) ).
cnf(s220,plain,
( ~ spl79_60
| ~ spl79_173 ),
inference(sat_conversion,[],[f1848]) ).
cnf(s225,plain,
( ~ spl79_36
| ~ spl79_174 ),
inference(sat_conversion,[],[f1857]) ).
cnf(s227,plain,
( ~ spl79_72
| spl79_175 ),
inference(sat_conversion,[],[f1863]) ).
cnf(s232,plain,
( ~ spl79_115
| spl79_176 ),
inference(sat_conversion,[],[f1872]) ).
cnf(s236,plain,
( ~ spl79_77
| spl79_177 ),
inference(sat_conversion,[],[f1880]) ).
cnf(s241,plain,
( ~ spl79_139
| spl79_178 ),
inference(sat_conversion,[],[f1889]) ).
cnf(s249,plain,
( ~ spl79_29
| spl79_179 ),
inference(sat_conversion,[],[f1901]) ).
cnf(s254,plain,
( ~ spl79_29
| ~ spl79_180 ),
inference(sat_conversion,[],[f1910]) ).
cnf(s259,plain,
( ~ spl79_92
| ~ spl79_181 ),
inference(sat_conversion,[],[f1919]) ).
cnf(s264,plain,
( ~ spl79_68
| ~ spl79_182 ),
inference(sat_conversion,[],[f1928]) ).
cnf(s266,plain,
( ~ spl79_104
| ~ spl79_183 ),
inference(sat_conversion,[],[f1934]) ).
cnf(s271,plain,
( ~ spl79_147
| spl79_184 ),
inference(sat_conversion,[],[f1943]) ).
cnf(s280,plain,
( ~ spl79_84
| ~ spl79_185 ),
inference(sat_conversion,[],[f1956]) ).
cnf(s285,plain,
( ~ spl79_41
| spl79_186 ),
inference(sat_conversion,[],[f1965]) ).
cnf(s288,plain,
( ~ spl79_22
| ~ spl79_187 ),
inference(sat_conversion,[],[f1972]) ).
cnf(s293,plain,
( ~ spl79_22
| spl79_188 ),
inference(sat_conversion,[],[f1981]) ).
cnf(s297,plain,
( ~ spl79_95
| ~ spl79_189 ),
inference(sat_conversion,[],[f1989]) ).
cnf(s302,plain,
( ~ spl79_119
| ~ spl79_190 ),
inference(sat_conversion,[],[f1998]) ).
cnf(s306,plain,
( ~ spl79_130
| ~ spl79_191 ),
inference(sat_conversion,[],[f2006]) ).
cnf(s311,plain,
( ~ spl79_154
| spl79_192 ),
inference(sat_conversion,[],[f2015]) ).
cnf(s317,plain,
( ~ spl79_9
| spl79_193 ),
inference(sat_conversion,[],[f2025]) ).
cnf(s322,plain,
( ~ spl79_9
| spl79_194 ),
inference(sat_conversion,[],[f2034]) ).
cnf(s329,plain,
( ~ spl79_115
| spl79_195 ),
inference(sat_conversion,[],[f2045]) ).
cnf(s334,plain,
( ~ spl79_72
| spl79_196 ),
inference(sat_conversion,[],[f2054]) ).
cnf(s340,plain,
( ~ spl79_108
| ~ spl79_197 ),
inference(sat_conversion,[],[f2064]) ).
cnf(s345,plain,
( ~ spl79_46
| spl79_198 ),
inference(sat_conversion,[],[f2073]) ).
cnf(s348,plain,
( ~ spl79_119
| spl79_199 ),
inference(sat_conversion,[],[f2080]) ).
cnf(s353,plain,
( ~ spl79_95
| ~ spl79_200 ),
inference(sat_conversion,[],[f2089]) ).
cnf(s357,plain,
( ~ spl79_154
| ~ spl79_201 ),
inference(sat_conversion,[],[f2097]) ).
cnf(s362,plain,
( ~ spl79_130
| spl79_202 ),
inference(sat_conversion,[],[f2106]) ).
cnf(s368,plain,
( ~ spl79_147
| ~ spl79_203 ),
inference(sat_conversion,[],[f2116]) ).
cnf(s373,plain,
( ~ spl79_104
| spl79_204 ),
inference(sat_conversion,[],[f2125]) ).
cnf(s376,plain,
( ~ spl79_14
| ~ spl79_205 ),
inference(sat_conversion,[],[f2132]) ).
cnf(s381,plain,
( ~ spl79_14
| spl79_206 ),
inference(sat_conversion,[],[f2141]) ).
cnf(s389,plain,
( ~ spl79_139
| ~ spl79_207 ),
inference(sat_conversion,[],[f2153]) ).
cnf(s394,plain,
( ~ spl79_77
| ~ spl79_208 ),
inference(sat_conversion,[],[f2162]) ).
cnf(s400,plain,
( ~ spl79_1
| ~ spl79_6
| ~ spl79_7
| spl79_13
| ~ spl79_19
| ~ spl79_25
| spl79_31
| spl79_32
| ~ spl79_36
| ~ spl79_38
| ~ spl79_41
| spl79_44
| ~ spl79_46
| spl79_50
| ~ spl79_51
| ~ spl79_56
| ~ spl79_60
| spl79_62
| ~ spl79_63
| ~ spl79_69
| ~ spl79_75
| ~ spl79_81
| ~ spl79_84
| spl79_87
| ~ spl79_93
| spl79_94
| spl79_100
| ~ spl79_106
| ~ spl79_108
| spl79_112
| spl79_118
| spl79_124
| ~ spl79_125
| ~ spl79_131
| ~ spl79_132
| spl79_137
| ~ spl79_143
| ~ spl79_149
| spl79_155
| spl79_156
| spl79_161
| spl79_162
| ~ spl79_163
| spl79_164
| spl79_165
| ~ spl79_166
| spl79_167
| ~ spl79_168
| spl79_169
| ~ spl79_170
| spl79_171
| spl79_172
| spl79_173
| spl79_174
| ~ spl79_175
| ~ spl79_176
| ~ spl79_177
| ~ spl79_178
| ~ spl79_179
| spl79_180
| spl79_181
| spl79_182
| spl79_183
| ~ spl79_184
| spl79_185
| ~ spl79_186
| spl79_187
| ~ spl79_188
| spl79_189
| spl79_190
| spl79_191
| ~ spl79_192
| ~ spl79_193
| ~ spl79_194
| ~ spl79_195
| ~ spl79_196
| spl79_197
| ~ spl79_198
| ~ spl79_199
| spl79_200
| spl79_201
| ~ spl79_202
| spl79_203
| ~ spl79_204
| spl79_205
| ~ spl79_206
| spl79_207
| spl79_208 ),
inference(sat_conversion,[],[f2168]) ).
cnf(s421,plain,
spl79_14,
inference(sat_conversion,[],[f2189]) ).
cnf(s422,plain,
spl79_154,
inference(sat_conversion,[],[f2190]) ).
cnf(s423,plain,
spl79_147,
inference(sat_conversion,[],[f2191]) ).
cnf(s424,plain,
spl79_139,
inference(sat_conversion,[],[f2192]) ).
cnf(s425,plain,
spl79_132,
inference(sat_conversion,[],[f2193]) ).
cnf(s426,plain,
spl79_130,
inference(sat_conversion,[],[f2194]) ).
cnf(s427,plain,
spl79_9,
inference(sat_conversion,[],[f2195]) ).
cnf(s428,plain,
spl79_119,
inference(sat_conversion,[],[f2196]) ).
cnf(s429,plain,
spl79_115,
inference(sat_conversion,[],[f2197]) ).
cnf(s430,plain,
spl79_108,
inference(sat_conversion,[],[f2198]) ).
cnf(s431,plain,
spl79_104,
inference(sat_conversion,[],[f2199]) ).
cnf(s432,plain,
spl79_95,
inference(sat_conversion,[],[f2200]) ).
cnf(s433,plain,
spl79_22,
inference(sat_conversion,[],[f2201]) ).
cnf(s434,plain,
spl79_92,
inference(sat_conversion,[],[f2202]) ).
cnf(s435,plain,
spl79_84,
inference(sat_conversion,[],[f2203]) ).
cnf(s436,plain,
spl79_77,
inference(sat_conversion,[],[f2204]) ).
cnf(s437,plain,
spl79_72,
inference(sat_conversion,[],[f2205]) ).
cnf(s438,plain,
spl79_68,
inference(sat_conversion,[],[f2206]) ).
cnf(s439,plain,
spl79_29,
inference(sat_conversion,[],[f2207]) ).
cnf(s440,plain,
spl79_60,
inference(sat_conversion,[],[f2208]) ).
cnf(s441,plain,
spl79_51,
inference(sat_conversion,[],[f2209]) ).
cnf(s442,plain,
spl79_46,
inference(sat_conversion,[],[f2210]) ).
cnf(s443,plain,
spl79_41,
inference(sat_conversion,[],[f2211]) ).
cnf(s444,plain,
spl79_36,
inference(sat_conversion,[],[f2212]) ).
cnf(s445,plain,
spl79_6,
inference(sat_conversion,[],[f2213]) ).
cnf(s470,plain,
( ~ spl79_1
| ~ spl79_7
| spl79_13
| ~ spl79_19
| ~ spl79_25
| spl79_31
| spl79_32
| ~ spl79_38
| spl79_44
| spl79_50
| ~ spl79_56
| spl79_62
| ~ spl79_63
| ~ spl79_69
| ~ spl79_75
| ~ spl79_81
| spl79_87
| ~ spl79_93
| spl79_94
| spl79_100
| ~ spl79_106
| spl79_112
| spl79_118
| spl79_124
| ~ spl79_125
| ~ spl79_131
| spl79_137
| ~ spl79_143
| ~ spl79_149
| spl79_155
| spl79_156
| spl79_161
| spl79_162
| ~ spl79_163
| spl79_164
| spl79_165
| ~ spl79_166
| spl79_167
| ~ spl79_168
| spl79_169
| ~ spl79_170
| spl79_171
| spl79_172
| spl79_173
| spl79_174
| ~ spl79_175
| ~ spl79_176
| ~ spl79_177
| ~ spl79_178
| ~ spl79_179
| spl79_180
| spl79_181
| spl79_182
| spl79_183
| ~ spl79_184
| spl79_185
| ~ spl79_186
| spl79_187
| ~ spl79_188
| spl79_189
| spl79_190
| spl79_191
| ~ spl79_192
| ~ spl79_193
| ~ spl79_194
| ~ spl79_195
| ~ spl79_196
| spl79_197
| ~ spl79_198
| ~ spl79_199
| spl79_200
| spl79_201
| ~ spl79_202
| spl79_203
| ~ spl79_204
| spl79_205
| ~ spl79_206
| spl79_207
| spl79_208 ),
inference(rat,[],[s400,s425,s430,s435,s440,s441,s442,s443,s444,s445]) ).
cnf(s475,plain,
~ spl79_208,
inference(rat,[],[s394,s436]) ).
cnf(s476,plain,
~ spl79_207,
inference(rat,[],[s389,s424]) ).
cnf(s477,plain,
spl79_206,
inference(rat,[],[s381,s421]) ).
cnf(s478,plain,
~ spl79_205,
inference(rat,[],[s376,s421]) ).
cnf(s479,plain,
spl79_204,
inference(rat,[],[s373,s431]) ).
cnf(s480,plain,
~ spl79_203,
inference(rat,[],[s368,s423]) ).
cnf(s481,plain,
spl79_202,
inference(rat,[],[s362,s426]) ).
cnf(s482,plain,
~ spl79_201,
inference(rat,[],[s357,s422]) ).
cnf(s483,plain,
~ spl79_200,
inference(rat,[],[s353,s432]) ).
cnf(s484,plain,
spl79_199,
inference(rat,[],[s348,s428]) ).
cnf(s485,plain,
spl79_198,
inference(rat,[],[s345,s442]) ).
cnf(s486,plain,
~ spl79_197,
inference(rat,[],[s340,s430]) ).
cnf(s487,plain,
spl79_196,
inference(rat,[],[s334,s437]) ).
cnf(s488,plain,
spl79_195,
inference(rat,[],[s329,s429]) ).
cnf(s489,plain,
spl79_194,
inference(rat,[],[s322,s427]) ).
cnf(s490,plain,
spl79_193,
inference(rat,[],[s317,s427]) ).
cnf(s491,plain,
spl79_192,
inference(rat,[],[s311,s422]) ).
cnf(s492,plain,
~ spl79_191,
inference(rat,[],[s306,s426]) ).
cnf(s493,plain,
~ spl79_190,
inference(rat,[],[s302,s428]) ).
cnf(s494,plain,
~ spl79_189,
inference(rat,[],[s297,s432]) ).
cnf(s495,plain,
spl79_188,
inference(rat,[],[s293,s433]) ).
cnf(s496,plain,
~ spl79_187,
inference(rat,[],[s288,s433]) ).
cnf(s497,plain,
spl79_186,
inference(rat,[],[s285,s443]) ).
cnf(s498,plain,
~ spl79_185,
inference(rat,[],[s280,s435]) ).
cnf(s499,plain,
spl79_184,
inference(rat,[],[s271,s423]) ).
cnf(s500,plain,
~ spl79_183,
inference(rat,[],[s266,s431]) ).
cnf(s501,plain,
~ spl79_182,
inference(rat,[],[s264,s438]) ).
cnf(s502,plain,
~ spl79_181,
inference(rat,[],[s259,s434]) ).
cnf(s503,plain,
~ spl79_180,
inference(rat,[],[s254,s439]) ).
cnf(s504,plain,
spl79_179,
inference(rat,[],[s249,s439]) ).
cnf(s505,plain,
spl79_178,
inference(rat,[],[s241,s424]) ).
cnf(s506,plain,
spl79_177,
inference(rat,[],[s236,s436]) ).
cnf(s507,plain,
spl79_176,
inference(rat,[],[s232,s429]) ).
cnf(s508,plain,
spl79_175,
inference(rat,[],[s227,s437]) ).
cnf(s509,plain,
~ spl79_174,
inference(rat,[],[s225,s444]) ).
cnf(s510,plain,
~ spl79_173,
inference(rat,[],[s220,s440]) ).
cnf(s511,plain,
~ spl79_172,
inference(rat,[],[s213,s434]) ).
cnf(s512,plain,
~ spl79_171,
inference(rat,[],[s208,s438]) ).
cnf(s513,plain,
spl79_170,
inference(rat,[],[s201,s425]) ).
cnf(s514,plain,
~ spl79_169,
inference(rat,[],[s196,s441]) ).
cnf(s515,plain,
spl79_168,
inference(rat,[],[s192,s430]) ).
cnf(s516,plain,
~ spl79_167,
inference(rat,[],[s187,s442]) ).
cnf(s517,plain,
spl79_166,
inference(rat,[],[s183,s435]) ).
cnf(s518,plain,
~ spl79_165,
inference(rat,[],[s178,s443]) ).
cnf(s519,plain,
~ spl79_164,
inference(rat,[],[s174,s440]) ).
cnf(s520,plain,
spl79_163,
inference(rat,[],[s169,s444]) ).
cnf(s521,plain,
~ spl79_162,
inference(rat,[],[s165,s445]) ).
cnf(s522,plain,
~ spl79_161,
inference(rat,[],[s160,s445]) ).
cnf(s523,plain,
~ spl79_155,
inference(rat,[],[s148,s421]) ).
cnf(s524,plain,
spl79_149,
inference(rat,[],[s145,s422]) ).
cnf(s525,plain,
spl79_143,
inference(rat,[],[s139,s423]) ).
cnf(s526,plain,
~ spl79_137,
inference(rat,[],[s132,s424]) ).
cnf(s527,plain,
spl79_131,
inference(rat,[],[s126,s425]) ).
cnf(s528,plain,
spl79_125,
inference(rat,[],[s125,s426]) ).
cnf(s529,plain,
~ spl79_124,
inference(rat,[],[s119,s427]) ).
cnf(s530,plain,
~ spl79_118,
inference(rat,[],[s111,s428]) ).
cnf(s531,plain,
~ spl79_112,
inference(rat,[],[s108,s429]) ).
cnf(s532,plain,
spl79_106,
inference(rat,[],[s102,s430]) ).
cnf(s533,plain,
~ spl79_100,
inference(rat,[],[s99,s431]) ).
cnf(s534,plain,
~ spl79_94,
inference(rat,[],[s91,s432]) ).
cnf(s535,plain,
spl79_93,
inference(rat,[],[s87,s433]) ).
cnf(s536,plain,
~ spl79_87,
inference(rat,[],[s85,s434]) ).
cnf(s537,plain,
spl79_81,
inference(rat,[],[s78,s435]) ).
cnf(s538,plain,
spl79_75,
inference(rat,[],[s72,s436]) ).
cnf(s539,plain,
spl79_69,
inference(rat,[],[s68,s437]) ).
cnf(s540,plain,
spl79_63,
inference(rat,[],[s65,s438]) ).
cnf(s541,plain,
~ spl79_62,
inference(rat,[],[s56,s439]) ).
cnf(s542,plain,
spl79_56,
inference(rat,[],[s54,s440]) ).
cnf(s543,plain,
~ spl79_50,
inference(rat,[],[s46,s441]) ).
cnf(s544,plain,
~ spl79_44,
inference(rat,[],[s42,s442]) ).
cnf(s545,plain,
spl79_38,
inference(rat,[],[s38,s443]) ).
cnf(s546,plain,
~ spl79_32,
inference(rat,[],[s34,s444]) ).
cnf(s547,plain,
~ spl79_31,
inference(rat,[],[s30,s445]) ).
cnf(s548,plain,
spl79_25,
inference(rat,[],[s24,s439]) ).
cnf(s549,plain,
spl79_19,
inference(rat,[],[s18,s433]) ).
cnf(s550,plain,
~ spl79_13,
inference(rat,[],[s11,s421]) ).
cnf(s551,plain,
spl79_7,
inference(rat,[],[s7,s427]) ).
cnf(s552,plain,
~ spl79_1,
inference(rat,[],[s470,s475,s476,s477,s478,s479,s480,s481,s482,s483,s484,s485,s486,s487,s488,s489,s490,s491,s492,s493,s494,s495,s496,s497,s498,s499,s500,s501,s502,s503,s504,s505,s506,s507,s508,s509,s510,s511,s512,s513,s514,s515,s516,s517,s518,s519,s520,s521,s522,s155,s523,s524,s525,s526,s527,s528,s529,s530,s531,s532,s533,s534,s535,s536,s537,s538,s539,s540,s541,s542,s543,s544,s545,s546,s547,s548,s549,s550,s551]) ).
cnf(s553,plain,
$false,
inference(rat,[],[s5,s445,s552]) ).
fof(f2218,plain,
$false,
inference(avatar_sat_refutation,[],[s553]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG090+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n002.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 19:28:37 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.18/0.28 % (672969)Will run a generic schedule for satisfiability detection.
% 0.18/0.28 % (672975)% WARNING: option uhcvi not known.
% 0.18/0.28 % (672975)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1297332116:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.18/0.28 % (672976)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2024267427:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.18/0.28 % (672974)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3471837625_2999 on theBenchmark for (2999ds/0Mi)
% 0.18/0.28 % (672977)dis+10_1_sil=32000:sp=arity:random_seed=2292029033:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.18/0.28 % (672979)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1596354498:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.18/0.28 % (672978)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=829117984:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.18/0.28 % (672980)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3797023184:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.18/0.28 % (672975) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-672969-672975"...
% 0.18/0.28 % (672975)...printing done.
% 0.18/0.28 % (672976) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-672969-672976"...
% 0.18/0.28 % (672975)Refutation found. Thanks to Tanya!
% 0.18/0.28 % SZS status Theorem for theBenchmark
% 0.18/0.28 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/0.28 % (672975)------------------------------
% 0.18/0.28 % (672975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.28 % (672975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.28 % (672975)CaDiCaL version: 2.1.3
% 0.18/0.28 % (672975)Termination reason: Refutation
% 0.18/0.28 % (672975)Time elapsed: 0.014 s
% 0.18/0.28 % (672975)Peak memory usage: 13 MB
% 0.18/0.28 % (672975)Instructions burned: 55 (million)
% 0.18/0.28 % (672969)Success in time 0.051 s
% 0.18/0.28 % Vampire exiting
%------------------------------------------------------------------------------