%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG056+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:08:58 AM UTC 2026
% Result : Theorem 6.03s 1.65s
% Output : Refutation 7.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 164
% Syntax : Number of formulae : 807 ( 128 unt; 157 def)
% Number of atoms : 2875 (1490 equ)
% Maximal formula atoms : 250 ( 3 avg)
% Number of connectives : 3227 (1159 ~;1379 |; 566 &)
% ( 123 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 159 ( 157 usr; 158 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e4 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3
| op(e0,e1) = e4 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3
| op(e0,e2) = e4 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3
| op(e0,e3) = e4 )
& ( op(e0,e4) = e0
| op(e0,e4) = e1
| op(e0,e4) = e2
| op(e0,e4) = e3
| op(e0,e4) = e4 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3
| op(e1,e0) = e4 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3
| op(e1,e1) = e4 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3
| op(e1,e2) = e4 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3
| op(e1,e3) = e4 )
& ( op(e1,e4) = e0
| op(e1,e4) = e1
| op(e1,e4) = e2
| op(e1,e4) = e3
| op(e1,e4) = e4 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3
| op(e2,e0) = e4 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3
| op(e2,e1) = e4 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3
| op(e2,e2) = e4 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3
| op(e2,e3) = e4 )
& ( op(e2,e4) = e0
| op(e2,e4) = e1
| op(e2,e4) = e2
| op(e2,e4) = e3
| op(e2,e4) = e4 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3
| op(e3,e0) = e4 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3
| op(e3,e1) = e4 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3
| op(e3,e2) = e4 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3
| op(e3,e3) = e4 )
& ( op(e3,e4) = e0
| op(e3,e4) = e1
| op(e3,e4) = e2
| op(e3,e4) = e3
| op(e3,e4) = e4 )
& ( op(e4,e0) = e0
| op(e4,e0) = e1
| op(e4,e0) = e2
| op(e4,e0) = e3
| op(e4,e0) = e4 )
& ( op(e4,e1) = e0
| op(e4,e1) = e1
| op(e4,e1) = e2
| op(e4,e1) = e3
| op(e4,e1) = e4 )
& ( op(e4,e2) = e0
| op(e4,e2) = e1
| op(e4,e2) = e2
| op(e4,e2) = e3
| op(e4,e2) = e4 )
& ( op(e4,e3) = e0
| op(e4,e3) = e1
| op(e4,e3) = e2
| op(e4,e3) = e3
| op(e4,e3) = e4 )
& ( op(e4,e4) = e0
| op(e4,e4) = e1
| op(e4,e4) = e2
| op(e4,e4) = e3
| op(e4,e4) = e4 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( op(unit,e0) = e0
& op(e0,unit) = e0
& op(unit,e1) = e1
& op(e1,unit) = e1
& op(unit,e2) = e2
& op(e2,unit) = e2
& op(unit,e3) = e3
& op(e3,unit) = e3
& op(unit,e4) = e4
& op(e4,unit) = e4
& ( unit = e0
| unit = e1
| unit = e2
| unit = e3
| unit = e4 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0
| op(e0,e4) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0
| op(e4,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1
| op(e0,e4) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1
| op(e4,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2
| op(e0,e4) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2
| op(e4,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3
| op(e0,e4) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3
| op(e4,e0) = e3 )
& ( op(e0,e0) = e4
| op(e0,e1) = e4
| op(e0,e2) = e4
| op(e0,e3) = e4
| op(e0,e4) = e4 )
& ( op(e0,e0) = e4
| op(e1,e0) = e4
| op(e2,e0) = e4
| op(e3,e0) = e4
| op(e4,e0) = e4 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0
| op(e1,e4) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0
| op(e4,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1
| op(e1,e4) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1
| op(e4,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2
| op(e1,e4) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2
| op(e4,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3
| op(e1,e4) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3
| op(e4,e1) = e3 )
& ( op(e1,e0) = e4
| op(e1,e1) = e4
| op(e1,e2) = e4
| op(e1,e3) = e4
| op(e1,e4) = e4 )
& ( op(e0,e1) = e4
| op(e1,e1) = e4
| op(e2,e1) = e4
| op(e3,e1) = e4
| op(e4,e1) = e4 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0
| op(e2,e4) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0
| op(e4,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1
| op(e2,e4) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1
| op(e4,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2
| op(e2,e4) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2
| op(e4,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3
| op(e2,e4) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3
| op(e4,e2) = e3 )
& ( op(e2,e0) = e4
| op(e2,e1) = e4
| op(e2,e2) = e4
| op(e2,e3) = e4
| op(e2,e4) = e4 )
& ( op(e0,e2) = e4
| op(e1,e2) = e4
| op(e2,e2) = e4
| op(e3,e2) = e4
| op(e4,e2) = e4 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0
| op(e3,e4) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0
| op(e4,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1
| op(e3,e4) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1
| op(e4,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2
| op(e3,e4) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2
| op(e4,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3
| op(e3,e4) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3
| op(e4,e3) = e3 )
& ( op(e3,e0) = e4
| op(e3,e1) = e4
| op(e3,e2) = e4
| op(e3,e3) = e4
| op(e3,e4) = e4 )
& ( op(e0,e3) = e4
| op(e1,e3) = e4
| op(e2,e3) = e4
| op(e3,e3) = e4
| op(e4,e3) = e4 )
& ( op(e4,e0) = e0
| op(e4,e1) = e0
| op(e4,e2) = e0
| op(e4,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e4) = e0
| op(e1,e4) = e0
| op(e2,e4) = e0
| op(e3,e4) = e0
| op(e4,e4) = e0 )
& ( op(e4,e0) = e1
| op(e4,e1) = e1
| op(e4,e2) = e1
| op(e4,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e4) = e1
| op(e1,e4) = e1
| op(e2,e4) = e1
| op(e3,e4) = e1
| op(e4,e4) = e1 )
& ( op(e4,e0) = e2
| op(e4,e1) = e2
| op(e4,e2) = e2
| op(e4,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e4) = e2
| op(e1,e4) = e2
| op(e2,e4) = e2
| op(e3,e4) = e2
| op(e4,e4) = e2 )
& ( op(e4,e0) = e3
| op(e4,e1) = e3
| op(e4,e2) = e3
| op(e4,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e4) = e3
| op(e1,e4) = e3
| op(e2,e4) = e3
| op(e3,e4) = e3
| op(e4,e4) = e3 )
& ( op(e4,e0) = e4
| op(e4,e1) = e4
| op(e4,e2) = e4
| op(e4,e3) = e4
| op(e4,e4) = e4 )
& ( op(e0,e4) = e4
| op(e1,e4) = e4
| op(e2,e4) = e4
| op(e3,e4) = e4
| op(e4,e4) = e4 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( op(e0,e0) != op(e1,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e4,e0)
& op(e1,e0) != op(e2,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e4,e0)
& op(e2,e0) != op(e3,e0)
& op(e2,e0) != op(e4,e0)
& op(e3,e0) != op(e4,e0)
& op(e0,e1) != op(e1,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e4,e1)
& op(e1,e1) != op(e2,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e4,e1)
& op(e2,e1) != op(e3,e1)
& op(e2,e1) != op(e4,e1)
& op(e3,e1) != op(e4,e1)
& op(e0,e2) != op(e1,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e4,e2)
& op(e1,e2) != op(e2,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e4,e2)
& op(e2,e2) != op(e3,e2)
& op(e2,e2) != op(e4,e2)
& op(e3,e2) != op(e4,e2)
& op(e0,e3) != op(e1,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e4,e3)
& op(e1,e3) != op(e2,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e4,e3)
& op(e2,e3) != op(e3,e3)
& op(e2,e3) != op(e4,e3)
& op(e3,e3) != op(e4,e3)
& op(e0,e4) != op(e1,e4)
& op(e0,e4) != op(e2,e4)
& op(e0,e4) != op(e3,e4)
& op(e0,e4) != op(e4,e4)
& op(e1,e4) != op(e2,e4)
& op(e1,e4) != op(e3,e4)
& op(e1,e4) != op(e4,e4)
& op(e2,e4) != op(e3,e4)
& op(e2,e4) != op(e4,e4)
& op(e3,e4) != op(e4,e4)
& op(e0,e0) != op(e0,e1)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e4)
& op(e0,e1) != op(e0,e2)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e4)
& op(e0,e2) != op(e0,e3)
& op(e0,e2) != op(e0,e4)
& op(e0,e3) != op(e0,e4)
& op(e1,e0) != op(e1,e1)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e4)
& op(e1,e1) != op(e1,e2)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e4)
& op(e1,e2) != op(e1,e3)
& op(e1,e2) != op(e1,e4)
& op(e1,e3) != op(e1,e4)
& op(e2,e0) != op(e2,e1)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e4)
& op(e2,e1) != op(e2,e2)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e4)
& op(e2,e2) != op(e2,e3)
& op(e2,e2) != op(e2,e4)
& op(e2,e3) != op(e2,e4)
& op(e3,e0) != op(e3,e1)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e4)
& op(e3,e1) != op(e3,e2)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e4)
& op(e3,e2) != op(e3,e3)
& op(e3,e2) != op(e3,e4)
& op(e3,e3) != op(e3,e4)
& op(e4,e0) != op(e4,e1)
& op(e4,e0) != op(e4,e2)
& op(e4,e0) != op(e4,e3)
& op(e4,e0) != op(e4,e4)
& op(e4,e1) != op(e4,e2)
& op(e4,e1) != op(e4,e3)
& op(e4,e1) != op(e4,e4)
& op(e4,e2) != op(e4,e3)
& op(e4,e2) != op(e4,e4)
& op(e4,e3) != op(e4,e4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e0 != e4
& e1 != e2
& e1 != e3
& e1 != e4
& e2 != e3
& e2 != e4
& e3 != e4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( e0 = op(op(e2,e2),op(e2,e2))
& e1 = op(op(e2,op(e2,e2)),op(e2,e2))
& e3 = op(e2,op(e2,e2))
& e4 = op(e2,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(f7,conjecture,
~ ( ( ( op(e0,op(e0,e0)) != e0
& op(e0,op(e0,e0)) = e0 )
| ( op(e1,op(e1,e0)) != e0
& op(e0,op(e1,e0)) = e1 )
| ( op(e2,op(e2,e0)) != e0
& op(e0,op(e2,e0)) = e2 )
| ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 ) )
& ( ( op(e0,op(e0,e1)) != e1
& op(e1,op(e0,e1)) = e0 )
| ( op(e1,op(e1,e1)) != e1
& op(e1,op(e1,e1)) = e1 )
| ( op(e2,op(e2,e1)) != e1
& op(e1,op(e2,e1)) = e2 )
| ( op(e3,op(e3,e1)) != e1
& op(e1,op(e3,e1)) = e3 )
| ( op(e4,op(e4,e1)) != e1
& op(e1,op(e4,e1)) = e4 ) )
& ( ( op(e0,op(e0,e2)) != e2
& op(e2,op(e0,e2)) = e0 )
| ( op(e1,op(e1,e2)) != e2
& op(e2,op(e1,e2)) = e1 )
| ( op(e2,op(e2,e2)) != e2
& op(e2,op(e2,e2)) = e2 )
| ( op(e3,op(e3,e2)) != e2
& op(e2,op(e3,e2)) = e3 )
| ( op(e4,op(e4,e2)) != e2
& op(e2,op(e4,e2)) = e4 ) )
& ( ( op(e0,op(e0,e3)) != e3
& op(e3,op(e0,e3)) = e0 )
| ( op(e1,op(e1,e3)) != e3
& op(e3,op(e1,e3)) = e1 )
| ( op(e2,op(e2,e3)) != e3
& op(e3,op(e2,e3)) = e2 )
| ( op(e3,op(e3,e3)) != e3
& op(e3,op(e3,e3)) = e3 )
| ( op(e4,op(e4,e3)) != e3
& op(e3,op(e4,e3)) = e4 ) )
& ( ( op(e0,op(e0,e4)) != e4
& op(e4,op(e0,e4)) = e0 )
| ( op(e1,op(e1,e4)) != e4
& op(e4,op(e1,e4)) = e1 )
| ( op(e2,op(e2,e4)) != e4
& op(e4,op(e2,e4)) = e2 )
| ( op(e3,op(e3,e4)) != e4
& op(e4,op(e3,e4)) = e3 )
| ( op(e4,op(e4,e4)) != e4
& op(e4,op(e4,e4)) = e4 ) )
& ( ( op(e0,e0) = e0
& op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e0
& op(e0,e1) != e0 )
| ( op(e0,e0) = e2
& op(e2,e2) = e0
& op(e0,e2) != e0 )
| ( op(e0,e0) = e3
& op(e3,e3) = e0
& op(e0,e3) != e0 )
| ( op(e0,e0) = e4
& op(e4,e4) = e0
& op(e0,e4) != e0 )
| ( op(e1,e1) = e0
& op(e0,e0) = e1
& op(e1,e0) != e1 )
| ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e1,e1) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 )
| ( op(e1,e1) = e3
& op(e3,e3) = e1
& op(e1,e3) != e1 )
| ( op(e1,e1) = e4
& op(e4,e4) = e1
& op(e1,e4) != e1 )
| ( op(e2,e2) = e0
& op(e0,e0) = e2
& op(e2,e0) != e2 )
| ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != e2 )
| ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e2,e2) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 )
| ( op(e3,e3) = e0
& op(e0,e0) = e3
& op(e3,e0) != e3 )
| ( op(e3,e3) = e1
& op(e1,e1) = e3
& op(e3,e1) != e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e3
& op(e3,e2) != e3 )
| ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ( op(e3,e3) = e4
& op(e4,e4) = e3
& op(e3,e4) != e3 )
| ( op(e4,e4) = e0
& op(e0,e0) = e4
& op(e4,e0) != e4 )
| ( op(e4,e4) = e1
& op(e1,e1) = e4
& op(e4,e1) != e4 )
| ( op(e4,e4) = e2
& op(e2,e2) = e4
& op(e4,e2) != e4 )
| ( op(e4,e4) = e3
& op(e3,e3) = e4
& op(e4,e3) != e4 )
| ( op(e4,e4) = e4
& op(e4,e4) = e4
& op(e4,e4) != e4 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f8,negated_conjecture,
~ ~ ( ( ( op(e0,op(e0,e0)) != e0
& op(e0,op(e0,e0)) = e0 )
| ( op(e1,op(e1,e0)) != e0
& op(e0,op(e1,e0)) = e1 )
| ( op(e2,op(e2,e0)) != e0
& op(e0,op(e2,e0)) = e2 )
| ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 ) )
& ( ( op(e0,op(e0,e1)) != e1
& op(e1,op(e0,e1)) = e0 )
| ( op(e1,op(e1,e1)) != e1
& op(e1,op(e1,e1)) = e1 )
| ( op(e2,op(e2,e1)) != e1
& op(e1,op(e2,e1)) = e2 )
| ( op(e3,op(e3,e1)) != e1
& op(e1,op(e3,e1)) = e3 )
| ( op(e4,op(e4,e1)) != e1
& op(e1,op(e4,e1)) = e4 ) )
& ( ( op(e0,op(e0,e2)) != e2
& op(e2,op(e0,e2)) = e0 )
| ( op(e1,op(e1,e2)) != e2
& op(e2,op(e1,e2)) = e1 )
| ( op(e2,op(e2,e2)) != e2
& op(e2,op(e2,e2)) = e2 )
| ( op(e3,op(e3,e2)) != e2
& op(e2,op(e3,e2)) = e3 )
| ( op(e4,op(e4,e2)) != e2
& op(e2,op(e4,e2)) = e4 ) )
& ( ( op(e0,op(e0,e3)) != e3
& op(e3,op(e0,e3)) = e0 )
| ( op(e1,op(e1,e3)) != e3
& op(e3,op(e1,e3)) = e1 )
| ( op(e2,op(e2,e3)) != e3
& op(e3,op(e2,e3)) = e2 )
| ( op(e3,op(e3,e3)) != e3
& op(e3,op(e3,e3)) = e3 )
| ( op(e4,op(e4,e3)) != e3
& op(e3,op(e4,e3)) = e4 ) )
& ( ( op(e0,op(e0,e4)) != e4
& op(e4,op(e0,e4)) = e0 )
| ( op(e1,op(e1,e4)) != e4
& op(e4,op(e1,e4)) = e1 )
| ( op(e2,op(e2,e4)) != e4
& op(e4,op(e2,e4)) = e2 )
| ( op(e3,op(e3,e4)) != e4
& op(e4,op(e3,e4)) = e3 )
| ( op(e4,op(e4,e4)) != e4
& op(e4,op(e4,e4)) = e4 ) )
& ( ( op(e0,e0) = e0
& op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e0
& op(e0,e1) != e0 )
| ( op(e0,e0) = e2
& op(e2,e2) = e0
& op(e0,e2) != e0 )
| ( op(e0,e0) = e3
& op(e3,e3) = e0
& op(e0,e3) != e0 )
| ( op(e0,e0) = e4
& op(e4,e4) = e0
& op(e0,e4) != e0 )
| ( op(e1,e1) = e0
& op(e0,e0) = e1
& op(e1,e0) != e1 )
| ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e1,e1) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 )
| ( op(e1,e1) = e3
& op(e3,e3) = e1
& op(e1,e3) != e1 )
| ( op(e1,e1) = e4
& op(e4,e4) = e1
& op(e1,e4) != e1 )
| ( op(e2,e2) = e0
& op(e0,e0) = e2
& op(e2,e0) != e2 )
| ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != e2 )
| ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e2,e2) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 )
| ( op(e3,e3) = e0
& op(e0,e0) = e3
& op(e3,e0) != e3 )
| ( op(e3,e3) = e1
& op(e1,e1) = e3
& op(e3,e1) != e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e3
& op(e3,e2) != e3 )
| ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ( op(e3,e3) = e4
& op(e4,e4) = e3
& op(e3,e4) != e3 )
| ( op(e4,e4) = e0
& op(e0,e0) = e4
& op(e4,e0) != e4 )
| ( op(e4,e4) = e1
& op(e1,e1) = e4
& op(e4,e1) != e4 )
| ( op(e4,e4) = e2
& op(e2,e2) = e4
& op(e4,e2) != e4 )
| ( op(e4,e4) = e3
& op(e3,e3) = e4
& op(e4,e3) != e4 )
| ( op(e4,e4) = e4
& op(e4,e4) = e4
& op(e4,e4) != e4 ) ) ),
inference(negated_conjecture,[status(cth)],[f7]) ).
fof(f9,plain,
( ( ( op(e0,op(e0,e0)) != e0
& op(e0,op(e0,e0)) = e0 )
| ( op(e1,op(e1,e0)) != e0
& op(e0,op(e1,e0)) = e1 )
| ( op(e2,op(e2,e0)) != e0
& op(e0,op(e2,e0)) = e2 )
| ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 ) )
& ( ( op(e0,op(e0,e1)) != e1
& op(e1,op(e0,e1)) = e0 )
| ( op(e1,op(e1,e1)) != e1
& op(e1,op(e1,e1)) = e1 )
| ( op(e2,op(e2,e1)) != e1
& op(e1,op(e2,e1)) = e2 )
| ( op(e3,op(e3,e1)) != e1
& op(e1,op(e3,e1)) = e3 )
| ( op(e4,op(e4,e1)) != e1
& op(e1,op(e4,e1)) = e4 ) )
& ( ( op(e0,op(e0,e2)) != e2
& op(e2,op(e0,e2)) = e0 )
| ( op(e1,op(e1,e2)) != e2
& op(e2,op(e1,e2)) = e1 )
| ( op(e2,op(e2,e2)) != e2
& op(e2,op(e2,e2)) = e2 )
| ( op(e3,op(e3,e2)) != e2
& op(e2,op(e3,e2)) = e3 )
| ( op(e4,op(e4,e2)) != e2
& op(e2,op(e4,e2)) = e4 ) )
& ( ( op(e0,op(e0,e3)) != e3
& op(e3,op(e0,e3)) = e0 )
| ( op(e1,op(e1,e3)) != e3
& op(e3,op(e1,e3)) = e1 )
| ( op(e2,op(e2,e3)) != e3
& op(e3,op(e2,e3)) = e2 )
| ( op(e3,op(e3,e3)) != e3
& op(e3,op(e3,e3)) = e3 )
| ( op(e4,op(e4,e3)) != e3
& op(e3,op(e4,e3)) = e4 ) )
& ( ( op(e0,op(e0,e4)) != e4
& op(e4,op(e0,e4)) = e0 )
| ( op(e1,op(e1,e4)) != e4
& op(e4,op(e1,e4)) = e1 )
| ( op(e2,op(e2,e4)) != e4
& op(e4,op(e2,e4)) = e2 )
| ( op(e3,op(e3,e4)) != e4
& op(e4,op(e3,e4)) = e3 )
| ( op(e4,op(e4,e4)) != e4
& op(e4,op(e4,e4)) = e4 ) )
& ( ( op(e0,e0) = e0
& op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e0
& op(e0,e1) != e0 )
| ( op(e0,e0) = e2
& op(e2,e2) = e0
& op(e0,e2) != e0 )
| ( op(e0,e0) = e3
& op(e3,e3) = e0
& op(e0,e3) != e0 )
| ( op(e0,e0) = e4
& op(e4,e4) = e0
& op(e0,e4) != e0 )
| ( op(e1,e1) = e0
& op(e0,e0) = e1
& op(e1,e0) != e1 )
| ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e1,e1) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 )
| ( op(e1,e1) = e3
& op(e3,e3) = e1
& op(e1,e3) != e1 )
| ( op(e1,e1) = e4
& op(e4,e4) = e1
& op(e1,e4) != e1 )
| ( op(e2,e2) = e0
& op(e0,e0) = e2
& op(e2,e0) != e2 )
| ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != e2 )
| ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e2,e2) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 )
| ( op(e3,e3) = e0
& op(e0,e0) = e3
& op(e3,e0) != e3 )
| ( op(e3,e3) = e1
& op(e1,e1) = e3
& op(e3,e1) != e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e3
& op(e3,e2) != e3 )
| ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ( op(e3,e3) = e4
& op(e4,e4) = e3
& op(e3,e4) != e3 )
| ( op(e4,e4) = e0
& op(e0,e0) = e4
& op(e4,e0) != e4 )
| ( op(e4,e4) = e1
& op(e1,e1) = e4
& op(e4,e1) != e4 )
| ( op(e4,e4) = e2
& op(e2,e2) = e4
& op(e4,e2) != e4 )
| ( op(e4,e4) = e3
& op(e3,e3) = e4
& op(e4,e3) != e4 )
| ( op(e4,e4) = e4
& op(e4,e4) = e4
& op(e4,e4) != e4 ) ) ),
inference(flattening,[],[f8]) ).
fof(f10,definition,
( ( op(e4,e4) = e4
& op(e4,e4) = e4
& op(e4,e4) != e4 )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f11,definition,
( ( op(e4,e4) = e3
& op(e3,e3) = e4
& op(e4,e3) != e4 )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f12,definition,
( ( op(e4,e4) = e2
& op(e2,e2) = e4
& op(e4,e2) != e4 )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f13,definition,
( ( op(e4,e4) = e1
& op(e1,e1) = e4
& op(e4,e1) != e4 )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f14,definition,
( ( op(e4,e4) = e0
& op(e0,e0) = e4
& op(e4,e0) != e4 )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f15,definition,
( ( op(e3,e3) = e4
& op(e4,e4) = e3
& op(e3,e4) != e3 )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f16,definition,
( ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f17,definition,
( ( op(e3,e3) = e2
& op(e2,e2) = e3
& op(e3,e2) != e3 )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f18,definition,
( ( op(e3,e3) = e1
& op(e1,e1) = e3
& op(e3,e1) != e3 )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f19,definition,
( ( op(e3,e3) = e0
& op(e0,e0) = e3
& op(e3,e0) != e3 )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f20,definition,
( ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f21,definition,
( ( op(e2,e2) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f22,definition,
( ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f23,definition,
( ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != e2 )
| ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f24,definition,
( ( op(e2,e2) = e0
& op(e0,e0) = e2
& op(e2,e0) != e2 )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f25,definition,
( ( op(e1,e1) = e4
& op(e4,e4) = e1
& op(e1,e4) != e1 )
| ~ sP15 ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f26,definition,
( ( op(e1,e1) = e3
& op(e3,e3) = e1
& op(e1,e3) != e1 )
| ~ sP16 ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f27,definition,
( ( op(e1,e1) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 )
| ~ sP17 ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f28,definition,
( ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ~ sP18 ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f29,definition,
( ( op(e1,e1) = e0
& op(e0,e0) = e1
& op(e1,e0) != e1 )
| ~ sP19 ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f30,definition,
( ( op(e0,e0) = e4
& op(e4,e4) = e0
& op(e0,e4) != e0 )
| ~ sP20 ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f31,definition,
( ( op(e0,e0) = e3
& op(e3,e3) = e0
& op(e0,e3) != e0 )
| ~ sP21 ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f32,definition,
( ( op(e0,e0) = e2
& op(e2,e2) = e0
& op(e0,e2) != e0 )
| ~ sP22 ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f33,definition,
( ( op(e0,e0) = e1
& op(e1,e1) = e0
& op(e0,e1) != e0 )
| ~ sP23 ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f34,definition,
( ( op(e4,op(e4,e4)) != e4
& op(e4,op(e4,e4)) = e4 )
| ~ sP24 ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f35,definition,
( ( op(e3,op(e3,e4)) != e4
& op(e4,op(e3,e4)) = e3 )
| ~ sP25 ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f36,definition,
( ( op(e4,op(e4,e3)) != e3
& op(e3,op(e4,e3)) = e4 )
| ~ sP26 ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f37,definition,
( ( op(e3,op(e3,e3)) != e3
& op(e3,op(e3,e3)) = e3 )
| ~ sP27 ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f38,definition,
( ( op(e4,op(e4,e2)) != e2
& op(e2,op(e4,e2)) = e4 )
| ~ sP28 ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f39,definition,
( ( op(e3,op(e3,e2)) != e2
& op(e2,op(e3,e2)) = e3 )
| ~ sP29 ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f40,definition,
( ( op(e4,op(e4,e1)) != e1
& op(e1,op(e4,e1)) = e4 )
| ~ sP30 ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f41,definition,
( ( op(e3,op(e3,e1)) != e1
& op(e1,op(e3,e1)) = e3 )
| ~ sP31 ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f42,definition,
( ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 )
| ~ sP32 ),
introduced(definition,[new_symbols(definition,[sP32])],[predicate_definition_introduction]) ).
fof(f43,definition,
( ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ~ sP33 ),
introduced(definition,[new_symbols(definition,[sP33])],[predicate_definition_introduction]) ).
fof(f44,plain,
( ( ( op(e0,op(e0,e0)) != e0
& op(e0,op(e0,e0)) = e0 )
| ( op(e1,op(e1,e0)) != e0
& op(e0,op(e1,e0)) = e1 )
| ( op(e2,op(e2,e0)) != e0
& op(e0,op(e2,e0)) = e2 )
| sP33
| sP32 )
& ( ( 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 )
| sP31
| sP30 )
& ( ( 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 )
| sP29
| sP28 )
& ( ( 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 )
| sP27
| sP26 )
& ( ( 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 )
| sP25
| sP24 )
& ( ( op(e0,e0) = e0
& op(e0,e0) = e0
& op(e0,e0) != e0 )
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ) ),
inference(definition_folding,[],[f9,f43,f42,f41,f40,f39,f38,f37,f36,f35,f34,f33,f32,f31,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10]) ).
fof(f45,plain,
( ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ~ sP33 ),
inference(nnf_transformation,[],[f43]) ).
fof(f46,plain,
( ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 )
| ~ sP32 ),
inference(nnf_transformation,[],[f42]) ).
fof(f53,plain,
( ( op(e3,op(e3,e4)) != e4
& op(e4,op(e3,e4)) = e3 )
| ~ sP25 ),
inference(nnf_transformation,[],[f35]) ).
fof(f54,plain,
( ( op(e4,op(e4,e4)) != e4
& op(e4,op(e4,e4)) = e4 )
| ~ sP24 ),
inference(nnf_transformation,[],[f34]) ).
fof(f55,plain,
( ( op(e0,e0) = e1
& op(e1,e1) = e0
& op(e0,e1) != e0 )
| ~ sP23 ),
inference(nnf_transformation,[],[f33]) ).
fof(f56,plain,
( ( op(e0,e0) = e2
& op(e2,e2) = e0
& op(e0,e2) != e0 )
| ~ sP22 ),
inference(nnf_transformation,[],[f32]) ).
fof(f57,plain,
( ( op(e0,e0) = e3
& op(e3,e3) = e0
& op(e0,e3) != e0 )
| ~ sP21 ),
inference(nnf_transformation,[],[f31]) ).
fof(f58,plain,
( ( op(e0,e0) = e4
& op(e4,e4) = e0
& op(e0,e4) != e0 )
| ~ sP20 ),
inference(nnf_transformation,[],[f30]) ).
fof(f59,plain,
( ( op(e1,e1) = e0
& op(e0,e0) = e1
& op(e1,e0) != e1 )
| ~ sP19 ),
inference(nnf_transformation,[],[f29]) ).
fof(f60,plain,
( ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ~ sP18 ),
inference(nnf_transformation,[],[f28]) ).
fof(f61,plain,
( ( op(e1,e1) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 )
| ~ sP17 ),
inference(nnf_transformation,[],[f27]) ).
fof(f62,plain,
( ( op(e1,e1) = e3
& op(e3,e3) = e1
& op(e1,e3) != e1 )
| ~ sP16 ),
inference(nnf_transformation,[],[f26]) ).
fof(f63,plain,
( ( op(e1,e1) = e4
& op(e4,e4) = e1
& op(e1,e4) != e1 )
| ~ sP15 ),
inference(nnf_transformation,[],[f25]) ).
fof(f64,plain,
( ( op(e2,e2) = e0
& op(e0,e0) = e2
& op(e2,e0) != e2 )
| ~ sP14 ),
inference(nnf_transformation,[],[f24]) ).
fof(f65,plain,
( ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != e2 )
| ~ sP13 ),
inference(nnf_transformation,[],[f23]) ).
fof(f66,plain,
( ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ~ sP12 ),
inference(nnf_transformation,[],[f22]) ).
fof(f67,plain,
( ( op(e2,e2) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ~ sP11 ),
inference(nnf_transformation,[],[f21]) ).
fof(f68,plain,
( ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 )
| ~ sP10 ),
inference(nnf_transformation,[],[f20]) ).
fof(f69,plain,
( ( op(e3,e3) = e0
& op(e0,e0) = e3
& op(e3,e0) != e3 )
| ~ sP9 ),
inference(nnf_transformation,[],[f19]) ).
fof(f70,plain,
( ( op(e3,e3) = e1
& op(e1,e1) = e3
& op(e3,e1) != e3 )
| ~ sP8 ),
inference(nnf_transformation,[],[f18]) ).
fof(f71,plain,
( ( op(e3,e3) = e2
& op(e2,e2) = e3
& op(e3,e2) != e3 )
| ~ sP7 ),
inference(nnf_transformation,[],[f17]) ).
fof(f72,plain,
( ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ~ sP6 ),
inference(nnf_transformation,[],[f16]) ).
fof(f73,plain,
( ( op(e3,e3) = e4
& op(e4,e4) = e3
& op(e3,e4) != e3 )
| ~ sP5 ),
inference(nnf_transformation,[],[f15]) ).
fof(f74,plain,
( ( op(e4,e4) = e0
& op(e0,e0) = e4
& op(e4,e0) != e4 )
| ~ sP4 ),
inference(nnf_transformation,[],[f14]) ).
fof(f75,plain,
( ( op(e4,e4) = e1
& op(e1,e1) = e4
& op(e4,e1) != e4 )
| ~ sP3 ),
inference(nnf_transformation,[],[f13]) ).
fof(f76,plain,
( ( op(e4,e4) = e2
& op(e2,e2) = e4
& op(e4,e2) != e4 )
| ~ sP2 ),
inference(nnf_transformation,[],[f12]) ).
fof(f77,plain,
( ( op(e4,e4) = e3
& op(e3,e3) = e4
& op(e4,e3) != e4 )
| ~ sP1 ),
inference(nnf_transformation,[],[f11]) ).
fof(f78,plain,
( ( op(e4,e4) = e4
& op(e4,e4) = e4
& op(e4,e4) != e4 )
| ~ sP0 ),
inference(nnf_transformation,[],[f10]) ).
fof(f80,plain,
( e0 = op(e4,e3)
| e1 = op(e4,e3)
| e2 = op(e4,e3)
| e3 = op(e4,e3)
| e4 = op(e4,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f86,plain,
( e0 = op(e3,e2)
| e1 = op(e3,e2)
| e2 = op(e3,e2)
| e3 = op(e3,e2)
| e4 = op(e3,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f92,plain,
( e0 = op(e2,e1)
| e1 = op(e2,e1)
| e2 = op(e2,e1)
| e3 = op(e2,e1)
| e4 = op(e2,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f93,plain,
( e0 = op(e2,e0)
| e1 = op(e2,e0)
| e2 = op(e2,e0)
| e3 = op(e2,e0)
| e4 = op(e2,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f100,plain,
( e0 = op(e0,e3)
| e1 = op(e0,e3)
| e2 = op(e0,e3)
| e3 = op(e0,e3)
| e4 = op(e0,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f101,plain,
( e0 = op(e0,e2)
| e1 = op(e0,e2)
| e2 = op(e0,e2)
| e3 = op(e0,e2)
| e4 = op(e0,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f104,plain,
( e0 = unit
| e1 = unit
| e2 = unit
| e3 = unit
| e4 = unit ),
inference(cnf_transformation,[],[f2]) ).
fof(f105,plain,
e4 = op(e4,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f106,plain,
e4 = op(unit,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f107,plain,
e3 = op(e3,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f108,plain,
e3 = op(unit,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f109,plain,
e2 = op(e2,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f110,plain,
e2 = op(unit,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f111,plain,
e1 = op(e1,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f112,plain,
e1 = op(unit,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f113,plain,
e0 = op(e0,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f114,plain,
e0 = op(unit,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f118,plain,
( e3 = op(e4,e0)
| e3 = op(e4,e1)
| e3 = op(e4,e2)
| e3 = op(e4,e3)
| e3 = op(e4,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f119,plain,
( e2 = op(e0,e4)
| e2 = op(e1,e4)
| e2 = op(e2,e4)
| e2 = op(e3,e4)
| e2 = op(e4,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f155,plain,
( op(e0,e0) = e4
| e4 = op(e1,e0)
| e4 = op(e2,e0)
| e4 = op(e3,e0)
| e4 = op(e4,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f159,plain,
( op(e0,e0) = e2
| e2 = op(e1,e0)
| e2 = op(e2,e0)
| e2 = op(e3,e0)
| e2 = op(e4,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f165,plain,
op(e4,e3) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f166,plain,
op(e4,e2) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f169,plain,
op(e4,e1) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f171,plain,
op(e4,e0) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f172,plain,
op(e4,e0) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f174,plain,
op(e4,e0) != op(e4,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f175,plain,
op(e3,e3) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f176,plain,
op(e3,e2) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f177,plain,
op(e3,e2) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f178,plain,
op(e3,e1) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f180,plain,
op(e3,e1) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f186,plain,
op(e2,e2) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f188,plain,
op(e2,e1) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f190,plain,
op(e2,e1) != op(e2,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f191,plain,
op(e2,e0) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f193,plain,
op(e2,e0) != op(e2,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f194,plain,
op(e2,e0) != op(e2,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f196,plain,
op(e1,e2) != op(e1,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f198,plain,
op(e1,e1) != op(e1,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f201,plain,
op(e1,e0) != op(e1,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f203,plain,
op(e1,e0) != op(e1,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f204,plain,
op(e1,e0) != op(e1,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f205,plain,
op(e0,e3) != op(e0,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f206,plain,
op(e0,e2) != op(e0,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f207,plain,
op(e0,e2) != op(e0,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f209,plain,
op(e0,e1) != op(e0,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f211,plain,
op(e0,e0) != op(e0,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f212,plain,
op(e0,e0) != op(e0,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f214,plain,
op(e0,e0) != op(e0,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f215,plain,
op(e3,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f216,plain,
op(e2,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f228,plain,
op(e1,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f231,plain,
op(e0,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f234,plain,
op(e0,e3) != op(e1,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f237,plain,
op(e2,e2) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f239,plain,
op(e1,e2) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f241,plain,
op(e0,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f242,plain,
op(e0,e2) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f243,plain,
op(e0,e2) != op(e2,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f244,plain,
op(e0,e2) != op(e1,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f245,plain,
op(e3,e1) != op(e4,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f253,plain,
op(e0,e1) != op(e2,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f260,plain,
op(e1,e0) != op(e2,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f266,plain,
e2 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f267,plain,
e2 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f270,plain,
e1 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f273,plain,
e0 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f275,plain,
e4 = op(e2,e2),
inference(cnf_transformation,[],[f6]) ).
fof(f276,plain,
e3 = op(e2,op(e2,e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f277,plain,
e1 = op(op(e2,op(e2,e2)),op(e2,e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f278,plain,
e0 = op(op(e2,e2),op(e2,e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f280,plain,
( e0 != op(e3,op(e3,e0))
| ~ sP33 ),
inference(cnf_transformation,[],[f45]) ).
fof(f281,plain,
( e4 = op(e0,op(e4,e0))
| ~ sP32 ),
inference(cnf_transformation,[],[f46]) ).
fof(f295,plain,
( e3 = op(e4,op(e3,e4))
| ~ sP25 ),
inference(cnf_transformation,[],[f53]) ).
fof(f297,plain,
( e4 = op(e4,op(e4,e4))
| ~ sP24 ),
inference(cnf_transformation,[],[f54]) ).
fof(f298,plain,
( e4 != op(e4,op(e4,e4))
| ~ sP24 ),
inference(cnf_transformation,[],[f54]) ).
fof(f299,plain,
( e0 != op(e0,e1)
| ~ sP23 ),
inference(cnf_transformation,[],[f55]) ).
fof(f301,plain,
( op(e0,e0) = e1
| ~ sP23 ),
inference(cnf_transformation,[],[f55]) ).
fof(f303,plain,
( e0 = op(e2,e2)
| ~ sP22 ),
inference(cnf_transformation,[],[f56]) ).
fof(f304,plain,
( op(e0,e0) = e2
| ~ sP22 ),
inference(cnf_transformation,[],[f56]) ).
fof(f306,plain,
( e0 = op(e3,e3)
| ~ sP21 ),
inference(cnf_transformation,[],[f57]) ).
fof(f307,plain,
( op(e0,e0) = e3
| ~ sP21 ),
inference(cnf_transformation,[],[f57]) ).
fof(f310,plain,
( op(e0,e0) = e4
| ~ sP20 ),
inference(cnf_transformation,[],[f58]) ).
fof(f311,plain,
( e1 != op(e1,e0)
| ~ sP19 ),
inference(cnf_transformation,[],[f59]) ).
fof(f316,plain,
( e1 = op(e1,e1)
| ~ sP18 ),
inference(cnf_transformation,[],[f60]) ).
fof(f319,plain,
( e2 = op(e1,e1)
| ~ sP17 ),
inference(cnf_transformation,[],[f61]) ).
fof(f321,plain,
( e1 = op(e3,e3)
| ~ sP16 ),
inference(cnf_transformation,[],[f62]) ).
fof(f324,plain,
( e1 = op(e4,e4)
| ~ sP15 ),
inference(cnf_transformation,[],[f63]) ).
fof(f326,plain,
( e2 != op(e2,e0)
| ~ sP14 ),
inference(cnf_transformation,[],[f64]) ).
fof(f330,plain,
( e2 = op(e1,e1)
| ~ sP13 ),
inference(cnf_transformation,[],[f65]) ).
fof(f334,plain,
( e2 = op(e2,e2)
| ~ sP12 ),
inference(cnf_transformation,[],[f66]) ).
fof(f337,plain,
( e3 = op(e2,e2)
| ~ sP11 ),
inference(cnf_transformation,[],[f67]) ).
fof(f339,plain,
( e2 = op(e4,e4)
| ~ sP10 ),
inference(cnf_transformation,[],[f68]) ).
fof(f341,plain,
( e3 != op(e3,e0)
| ~ sP9 ),
inference(cnf_transformation,[],[f69]) ).
fof(f346,plain,
( e1 = op(e3,e3)
| ~ sP8 ),
inference(cnf_transformation,[],[f70]) ).
fof(f348,plain,
( e3 = op(e2,e2)
| ~ sP7 ),
inference(cnf_transformation,[],[f71]) ).
fof(f350,plain,
( e3 != op(e3,e3)
| ~ sP6 ),
inference(cnf_transformation,[],[f72]) ).
fof(f352,plain,
( e3 = op(e3,e3)
| ~ sP6 ),
inference(cnf_transformation,[],[f72]) ).
fof(f354,plain,
( e3 = op(e4,e4)
| ~ sP5 ),
inference(cnf_transformation,[],[f73]) ).
fof(f357,plain,
( op(e0,e0) = e4
| ~ sP4 ),
inference(cnf_transformation,[],[f74]) ).
fof(f361,plain,
( e1 = op(e4,e4)
| ~ sP3 ),
inference(cnf_transformation,[],[f75]) ).
fof(f364,plain,
( e2 = op(e4,e4)
| ~ sP2 ),
inference(cnf_transformation,[],[f76]) ).
fof(f367,plain,
( e3 = op(e4,e4)
| ~ sP1 ),
inference(cnf_transformation,[],[f77]) ).
fof(f369,plain,
( e4 = op(e4,e4)
| ~ sP0 ),
inference(cnf_transformation,[],[f78]) ).
fof(f371,plain,
( e0 != op(e0,e0)
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f44]) ).
fof(f373,plain,
( e0 = op(e0,e0)
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f44]) ).
fof(f376,plain,
( e0 = op(e4,op(e0,e4))
| e4 != op(e1,op(e1,e4))
| e2 = op(e4,op(e2,e4))
| sP25
| sP24 ),
inference(cnf_transformation,[],[f44]) ).
fof(f406,plain,
( e0 = op(e0,op(e0,e0))
| e1 = op(e0,op(e1,e0))
| e2 = op(e0,op(e2,e0))
| sP33
| sP32 ),
inference(cnf_transformation,[],[f44]) ).
fof(f410,plain,
( e0 != op(e0,op(e0,e0))
| e1 = op(e0,op(e1,e0))
| e2 = op(e0,op(e2,e0))
| sP33
| sP32 ),
inference(cnf_transformation,[],[f44]) ).
fof(f415,definition,
( spl34_1
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl34_1])],[avatar_definition]) ).
fof(f419,definition,
( spl34_2
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl34_2])],[avatar_definition]) ).
fof(f423,definition,
( spl34_3
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl34_3])],[avatar_definition]) ).
fof(f427,definition,
( spl34_4
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl34_4])],[avatar_definition]) ).
fof(f431,definition,
( spl34_5
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl34_5])],[avatar_definition]) ).
fof(f435,definition,
( spl34_6
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl34_6])],[avatar_definition]) ).
fof(f439,definition,
( spl34_7
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl34_7])],[avatar_definition]) ).
fof(f443,definition,
( spl34_8
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl34_8])],[avatar_definition]) ).
fof(f447,definition,
( spl34_9
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl34_9])],[avatar_definition]) ).
fof(f451,definition,
( spl34_10
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl34_10])],[avatar_definition]) ).
fof(f455,definition,
( spl34_11
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl34_11])],[avatar_definition]) ).
fof(f459,definition,
( spl34_12
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl34_12])],[avatar_definition]) ).
fof(f463,definition,
( spl34_13
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl34_13])],[avatar_definition]) ).
fof(f467,definition,
( spl34_14
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl34_14])],[avatar_definition]) ).
fof(f471,definition,
( spl34_15
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl34_15])],[avatar_definition]) ).
fof(f475,definition,
( spl34_16
<=> sP15 ),
introduced(definition,[new_symbols(definition,[spl34_16])],[avatar_definition]) ).
fof(f479,definition,
( spl34_17
<=> sP16 ),
introduced(definition,[new_symbols(definition,[spl34_17])],[avatar_definition]) ).
fof(f483,definition,
( spl34_18
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl34_18])],[avatar_definition]) ).
fof(f487,definition,
( spl34_19
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl34_19])],[avatar_definition]) ).
fof(f491,definition,
( spl34_20
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl34_20])],[avatar_definition]) ).
fof(f495,definition,
( spl34_21
<=> sP20 ),
introduced(definition,[new_symbols(definition,[spl34_21])],[avatar_definition]) ).
fof(f499,definition,
( spl34_22
<=> sP21 ),
introduced(definition,[new_symbols(definition,[spl34_22])],[avatar_definition]) ).
fof(f503,definition,
( spl34_23
<=> sP22 ),
introduced(definition,[new_symbols(definition,[spl34_23])],[avatar_definition]) ).
fof(f507,definition,
( spl34_24
<=> sP23 ),
introduced(definition,[new_symbols(definition,[spl34_24])],[avatar_definition]) ).
fof(f511,definition,
( spl34_25
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl34_25])],[avatar_definition]) ).
fof(f514,plain,
( spl34_1
| spl34_2
| spl34_3
| spl34_4
| spl34_5
| spl34_6
| spl34_7
| spl34_8
| spl34_9
| spl34_10
| spl34_11
| spl34_12
| spl34_13
| spl34_14
| spl34_15
| spl34_16
| spl34_17
| spl34_18
| spl34_19
| spl34_20
| spl34_21
| spl34_22
| spl34_23
| spl34_24
| ~ spl34_25 ),
inference(avatar_split_clause,[],[f371,f511,f507,f503,f499,f495,f491,f487,f483,f479,f475,f471,f467,f463,f459,f455,f451,f447,f443,f439,f435,f431,f427,f423,f419,f415]) ).
fof(f516,plain,
( spl34_1
| spl34_2
| spl34_3
| spl34_4
| spl34_5
| spl34_6
| spl34_7
| spl34_8
| spl34_9
| spl34_10
| spl34_11
| spl34_12
| spl34_13
| spl34_14
| spl34_15
| spl34_16
| spl34_17
| spl34_18
| spl34_19
| spl34_20
| spl34_21
| spl34_22
| spl34_23
| spl34_24
| spl34_25 ),
inference(avatar_split_clause,[],[f373,f511,f507,f503,f499,f495,f491,f487,f483,f479,f475,f471,f467,f463,f459,f455,f451,f447,f443,f439,f435,f431,f427,f423,f419,f415]) ).
fof(f518,definition,
( spl34_26
<=> sP24 ),
introduced(definition,[new_symbols(definition,[spl34_26])],[avatar_definition]) ).
fof(f522,definition,
( spl34_27
<=> sP25 ),
introduced(definition,[new_symbols(definition,[spl34_27])],[avatar_definition]) ).
fof(f526,definition,
( spl34_28
<=> e2 = op(e4,op(e2,e4)) ),
introduced(definition,[new_symbols(definition,[spl34_28])],[avatar_definition]) ).
fof(f528,plain,
( e2 = op(e4,op(e2,e4))
| ~ spl34_28 ),
inference(avatar_component_clause,[],[f526]) ).
fof(f534,definition,
( spl34_30
<=> e0 = op(e4,op(e0,e4)) ),
introduced(definition,[new_symbols(definition,[spl34_30])],[avatar_definition]) ).
fof(f536,plain,
( e0 = op(e4,op(e0,e4))
| ~ spl34_30 ),
inference(avatar_component_clause,[],[f534]) ).
fof(f544,definition,
( spl34_32
<=> e4 = op(e1,op(e1,e4)) ),
introduced(definition,[new_symbols(definition,[spl34_32])],[avatar_definition]) ).
fof(f546,plain,
( e4 != op(e1,op(e1,e4))
| spl34_32 ),
inference(avatar_component_clause,[],[f544]) ).
fof(f547,plain,
( spl34_26
| spl34_27
| spl34_28
| ~ spl34_32
| spl34_30 ),
inference(avatar_split_clause,[],[f376,f534,f544,f526,f522,f518]) ).
fof(f606,definition,
( spl34_44
<=> e2 = op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl34_44])],[avatar_definition]) ).
fof(f607,plain,
( e2 != op(e2,op(e2,e2))
| spl34_44 ),
inference(avatar_component_clause,[],[f606]) ).
fof(f608,plain,
( e2 = op(e2,op(e2,e2))
| ~ spl34_44 ),
inference(avatar_component_clause,[],[f606]) ).
fof(f670,definition,
( spl34_56
<=> sP32 ),
introduced(definition,[new_symbols(definition,[spl34_56])],[avatar_definition]) ).
fof(f674,definition,
( spl34_57
<=> sP33 ),
introduced(definition,[new_symbols(definition,[spl34_57])],[avatar_definition]) ).
fof(f678,definition,
( spl34_58
<=> e2 = op(e0,op(e2,e0)) ),
introduced(definition,[new_symbols(definition,[spl34_58])],[avatar_definition]) ).
fof(f680,plain,
( e2 = op(e0,op(e2,e0))
| ~ spl34_58 ),
inference(avatar_component_clause,[],[f678]) ).
fof(f682,definition,
( spl34_59
<=> e1 = op(e0,op(e1,e0)) ),
introduced(definition,[new_symbols(definition,[spl34_59])],[avatar_definition]) ).
fof(f684,plain,
( e1 = op(e0,op(e1,e0))
| ~ spl34_59 ),
inference(avatar_component_clause,[],[f682]) ).
fof(f686,definition,
( spl34_60
<=> e0 = op(e0,op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl34_60])],[avatar_definition]) ).
fof(f689,plain,
( spl34_56
| spl34_57
| spl34_58
| spl34_59
| spl34_60 ),
inference(avatar_split_clause,[],[f406,f686,f682,f678,f674,f670]) ).
fof(f701,plain,
( spl34_56
| spl34_57
| spl34_58
| spl34_59
| ~ spl34_60 ),
inference(avatar_split_clause,[],[f410,f686,f682,f678,f674,f670]) ).
fof(f706,definition,
( spl34_63
<=> e4 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl34_63])],[avatar_definition]) ).
fof(f707,plain,
( e4 = op(e4,e4)
| ~ spl34_63 ),
inference(avatar_component_clause,[],[f706]) ).
fof(f710,plain,
( ~ spl34_1
| spl34_63 ),
inference(avatar_split_clause,[],[f369,f706,f415]) ).
fof(f713,definition,
( spl34_64
<=> e4 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl34_64])],[avatar_definition]) ).
fof(f714,plain,
( e4 = op(e4,e3)
| ~ spl34_64 ),
inference(avatar_component_clause,[],[f713]) ).
fof(f723,definition,
( spl34_66
<=> e3 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl34_66])],[avatar_definition]) ).
fof(f725,plain,
( e3 = op(e4,e4)
| ~ spl34_66 ),
inference(avatar_component_clause,[],[f723]) ).
fof(f726,plain,
( ~ spl34_2
| spl34_66 ),
inference(avatar_split_clause,[],[f367,f723,f419]) ).
fof(f733,definition,
( spl34_68
<=> e4 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl34_68])],[avatar_definition]) ).
fof(f735,plain,
( e4 = op(e2,e2)
| ~ spl34_68 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f738,definition,
( spl34_69
<=> e2 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl34_69])],[avatar_definition]) ).
fof(f740,plain,
( e2 = op(e4,e4)
| ~ spl34_69 ),
inference(avatar_component_clause,[],[f738]) ).
fof(f741,plain,
( ~ spl34_3
| spl34_69 ),
inference(avatar_split_clause,[],[f364,f738,f423]) ).
fof(f743,definition,
( spl34_70
<=> e4 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl34_70])],[avatar_definition]) ).
fof(f744,plain,
( e4 = op(e4,e1)
| ~ spl34_70 ),
inference(avatar_component_clause,[],[f743]) ).
fof(f753,definition,
( spl34_72
<=> e1 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl34_72])],[avatar_definition]) ).
fof(f755,plain,
( e1 = op(e4,e4)
| ~ spl34_72 ),
inference(avatar_component_clause,[],[f753]) ).
fof(f756,plain,
( ~ spl34_4
| spl34_72 ),
inference(avatar_split_clause,[],[f361,f753,f427]) ).
fof(f758,definition,
( spl34_73
<=> e4 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl34_73])],[avatar_definition]) ).
fof(f763,definition,
( spl34_74
<=> op(e0,e0) = e4 ),
introduced(definition,[new_symbols(definition,[spl34_74])],[avatar_definition]) ).
fof(f766,plain,
( ~ spl34_5
| spl34_74 ),
inference(avatar_split_clause,[],[f357,f763,f431]) ).
fof(f768,definition,
( spl34_75
<=> e0 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl34_75])],[avatar_definition]) ).
fof(f770,plain,
( e0 = op(e4,e4)
| ~ spl34_75 ),
inference(avatar_component_clause,[],[f768]) ).
fof(f777,plain,
( ~ spl34_6
| spl34_66 ),
inference(avatar_split_clause,[],[f354,f723,f435]) ).
fof(f780,definition,
( spl34_77
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl34_77])],[avatar_definition]) ).
fof(f783,plain,
( ~ spl34_7
| ~ spl34_77 ),
inference(avatar_split_clause,[],[f350,f780,f439]) ).
fof(f785,plain,
( ~ spl34_7
| spl34_77 ),
inference(avatar_split_clause,[],[f352,f780,f439]) ).
fof(f787,definition,
( spl34_78
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl34_78])],[avatar_definition]) ).
fof(f792,definition,
( spl34_79
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl34_79])],[avatar_definition]) ).
fof(f795,plain,
( ~ spl34_8
| spl34_79 ),
inference(avatar_split_clause,[],[f348,f792,f443]) ).
fof(f802,definition,
( spl34_81
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl34_81])],[avatar_definition]) ).
fof(f803,plain,
( e3 = op(e3,e1)
| ~ spl34_81 ),
inference(avatar_component_clause,[],[f802]) ).
fof(f812,definition,
( spl34_83
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl34_83])],[avatar_definition]) ).
fof(f815,plain,
( ~ spl34_9
| spl34_83 ),
inference(avatar_split_clause,[],[f346,f812,f447]) ).
fof(f817,definition,
( spl34_84
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl34_84])],[avatar_definition]) ).
fof(f820,plain,
( ~ spl34_10
| ~ spl34_84 ),
inference(avatar_split_clause,[],[f341,f817,f451]) ).
fof(f822,definition,
( spl34_85
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl34_85])],[avatar_definition]) ).
fof(f827,definition,
( spl34_86
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl34_86])],[avatar_definition]) ).
fof(f829,plain,
( e0 = op(e3,e3)
| ~ spl34_86 ),
inference(avatar_component_clause,[],[f827]) ).
fof(f832,definition,
( spl34_87
<=> e2 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl34_87])],[avatar_definition]) ).
fof(f836,plain,
( ~ spl34_11
| spl34_69 ),
inference(avatar_split_clause,[],[f339,f738,f455]) ).
fof(f844,plain,
( ~ spl34_12
| spl34_79 ),
inference(avatar_split_clause,[],[f337,f792,f459]) ).
fof(f846,definition,
( spl34_89
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl34_89])],[avatar_definition]) ).
fof(f851,plain,
( ~ spl34_13
| spl34_89 ),
inference(avatar_split_clause,[],[f334,f846,f463]) ).
fof(f853,definition,
( spl34_90
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl34_90])],[avatar_definition]) ).
fof(f854,plain,
( e2 = op(e2,e1)
| ~ spl34_90 ),
inference(avatar_component_clause,[],[f853]) ).
fof(f858,definition,
( spl34_91
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl34_91])],[avatar_definition]) ).
fof(f861,plain,
( ~ spl34_14
| spl34_91 ),
inference(avatar_split_clause,[],[f330,f858,f467]) ).
fof(f868,definition,
( spl34_93
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl34_93])],[avatar_definition]) ).
fof(f871,plain,
( ~ spl34_15
| ~ spl34_93 ),
inference(avatar_split_clause,[],[f326,f868,f471]) ).
fof(f873,definition,
( spl34_94
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl34_94])],[avatar_definition]) ).
fof(f878,definition,
( spl34_95
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl34_95])],[avatar_definition]) ).
fof(f887,plain,
( ~ spl34_16
| spl34_72 ),
inference(avatar_split_clause,[],[f324,f753,f475]) ).
fof(f894,plain,
( ~ spl34_17
| spl34_83 ),
inference(avatar_split_clause,[],[f321,f812,f479]) ).
fof(f902,plain,
( ~ spl34_18
| spl34_91 ),
inference(avatar_split_clause,[],[f319,f858,f483]) ).
fof(f904,definition,
( spl34_99
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl34_99])],[avatar_definition]) ).
fof(f905,plain,
( e1 = op(e1,e1)
| ~ spl34_99 ),
inference(avatar_component_clause,[],[f904]) ).
fof(f909,plain,
( ~ spl34_19
| spl34_99 ),
inference(avatar_split_clause,[],[f316,f904,f487]) ).
fof(f911,definition,
( spl34_100
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl34_100])],[avatar_definition]) ).
fof(f914,plain,
( ~ spl34_20
| ~ spl34_100 ),
inference(avatar_split_clause,[],[f311,f911,f491]) ).
fof(f916,definition,
( spl34_101
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl34_101])],[avatar_definition]) ).
fof(f931,plain,
( ~ spl34_21
| spl34_74 ),
inference(avatar_split_clause,[],[f310,f763,f495]) ).
fof(f933,definition,
( spl34_104
<=> e0 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl34_104])],[avatar_definition]) ).
fof(f934,plain,
( e0 = op(e0,e3)
| ~ spl34_104 ),
inference(avatar_component_clause,[],[f933]) ).
fof(f937,plain,
( ~ spl34_22
| spl34_86 ),
inference(avatar_split_clause,[],[f306,f827,f499]) ).
fof(f938,plain,
( ~ spl34_22
| spl34_85 ),
inference(avatar_split_clause,[],[f307,f822,f499]) ).
fof(f940,definition,
( spl34_105
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl34_105])],[avatar_definition]) ).
fof(f944,plain,
( ~ spl34_23
| spl34_95 ),
inference(avatar_split_clause,[],[f303,f878,f503]) ).
fof(f945,plain,
( ~ spl34_23
| spl34_94 ),
inference(avatar_split_clause,[],[f304,f873,f503]) ).
fof(f947,definition,
( spl34_106
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl34_106])],[avatar_definition]) ).
fof(f950,plain,
( ~ spl34_24
| ~ spl34_106 ),
inference(avatar_split_clause,[],[f299,f947,f507]) ).
fof(f952,plain,
( ~ spl34_24
| spl34_101 ),
inference(avatar_split_clause,[],[f301,f916,f507]) ).
fof(f954,definition,
( spl34_107
<=> e4 = op(e4,op(e4,e4)) ),
introduced(definition,[new_symbols(definition,[spl34_107])],[avatar_definition]) ).
fof(f957,plain,
( ~ spl34_26
| spl34_107 ),
inference(avatar_split_clause,[],[f297,f954,f518]) ).
fof(f958,plain,
( ~ spl34_26
| ~ spl34_107 ),
inference(avatar_split_clause,[],[f298,f954,f518]) ).
fof(f960,definition,
( spl34_108
<=> e3 = op(e4,op(e3,e4)) ),
introduced(definition,[new_symbols(definition,[spl34_108])],[avatar_definition]) ).
fof(f962,plain,
( e3 = op(e4,op(e3,e4))
| ~ spl34_108 ),
inference(avatar_component_clause,[],[f960]) ).
fof(f963,plain,
( ~ spl34_27
| spl34_108 ),
inference(avatar_split_clause,[],[f295,f960,f522]) ).
fof(f1026,definition,
( spl34_121
<=> e4 = op(e0,op(e4,e0)) ),
introduced(definition,[new_symbols(definition,[spl34_121])],[avatar_definition]) ).
fof(f1028,plain,
( e4 = op(e0,op(e4,e0))
| ~ spl34_121 ),
inference(avatar_component_clause,[],[f1026]) ).
fof(f1029,plain,
( ~ spl34_56
| spl34_121 ),
inference(avatar_split_clause,[],[f281,f1026,f670]) ).
fof(f1041,definition,
( spl34_124
<=> e0 = op(e3,op(e3,e0)) ),
introduced(definition,[new_symbols(definition,[spl34_124])],[avatar_definition]) ).
fof(f1043,plain,
( e0 != op(e3,op(e3,e0))
| spl34_124 ),
inference(avatar_component_clause,[],[f1041]) ).
fof(f1044,plain,
( ~ spl34_57
| ~ spl34_124 ),
inference(avatar_split_clause,[],[f280,f1041,f674]) ).
fof(f1045,plain,
spl34_68,
inference(avatar_split_clause,[],[f275,f733]) ).
fof(f1051,definition,
( spl34_126
<=> e4 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl34_126])],[avatar_definition]) ).
fof(f1052,plain,
( e4 != op(e2,e4)
| spl34_126 ),
inference(avatar_component_clause,[],[f1051]) ).
fof(f1053,plain,
( e4 = op(e2,e4)
| ~ spl34_126 ),
inference(avatar_component_clause,[],[f1051]) ).
fof(f1055,definition,
( spl34_127
<=> e4 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl34_127])],[avatar_definition]) ).
fof(f1057,plain,
( e4 = op(e1,e4)
| ~ spl34_127 ),
inference(avatar_component_clause,[],[f1055]) ).
fof(f1059,definition,
( spl34_128
<=> e4 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl34_128])],[avatar_definition]) ).
fof(f1061,plain,
( e4 = op(e0,e4)
| ~ spl34_128 ),
inference(avatar_component_clause,[],[f1059]) ).
fof(f1065,definition,
( spl34_129
<=> e3 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl34_129])],[avatar_definition]) ).
fof(f1067,plain,
( e3 = op(e2,e4)
| ~ spl34_129 ),
inference(avatar_component_clause,[],[f1065]) ).
fof(f1078,definition,
( spl34_132
<=> e3 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl34_132])],[avatar_definition]) ).
fof(f1080,plain,
( e3 = op(e4,e3)
| ~ spl34_132 ),
inference(avatar_component_clause,[],[f1078]) ).
fof(f1082,definition,
( spl34_133
<=> e3 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl34_133])],[avatar_definition]) ).
fof(f1084,plain,
( e3 = op(e4,e2)
| ~ spl34_133 ),
inference(avatar_component_clause,[],[f1082]) ).
fof(f1086,definition,
( spl34_134
<=> e3 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl34_134])],[avatar_definition]) ).
fof(f1087,plain,
( e3 != op(e4,e1)
| spl34_134 ),
inference(avatar_component_clause,[],[f1086]) ).
fof(f1088,plain,
( e3 = op(e4,e1)
| ~ spl34_134 ),
inference(avatar_component_clause,[],[f1086]) ).
fof(f1090,definition,
( spl34_135
<=> e3 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl34_135])],[avatar_definition]) ).
fof(f1092,plain,
( e3 = op(e4,e0)
| ~ spl34_135 ),
inference(avatar_component_clause,[],[f1090]) ).
fof(f1093,plain,
( spl34_66
| spl34_132
| spl34_133
| spl34_134
| spl34_135 ),
inference(avatar_split_clause,[],[f118,f1090,f1086,f1082,f1078,f723]) ).
fof(f1095,definition,
( spl34_136
<=> e2 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl34_136])],[avatar_definition]) ).
fof(f1097,plain,
( e2 = op(e3,e4)
| ~ spl34_136 ),
inference(avatar_component_clause,[],[f1095]) ).
fof(f1099,definition,
( spl34_137
<=> e2 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl34_137])],[avatar_definition]) ).
fof(f1101,plain,
( e2 = op(e1,e4)
| ~ spl34_137 ),
inference(avatar_component_clause,[],[f1099]) ).
fof(f1103,definition,
( spl34_138
<=> e2 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl34_138])],[avatar_definition]) ).
fof(f1105,plain,
( e2 = op(e0,e4)
| ~ spl34_138 ),
inference(avatar_component_clause,[],[f1103]) ).
fof(f1106,plain,
( spl34_69
| spl34_136
| spl34_87
| spl34_137
| spl34_138 ),
inference(avatar_split_clause,[],[f119,f1103,f1099,f832,f1095,f738]) ).
fof(f1108,definition,
( spl34_139
<=> e2 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl34_139])],[avatar_definition]) ).
fof(f1110,plain,
( e2 = op(e4,e3)
| ~ spl34_139 ),
inference(avatar_component_clause,[],[f1108]) ).
fof(f1120,definition,
( spl34_142
<=> e2 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl34_142])],[avatar_definition]) ).
fof(f1125,definition,
( spl34_143
<=> e1 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl34_143])],[avatar_definition]) ).
fof(f1127,plain,
( e1 = op(e3,e4)
| ~ spl34_143 ),
inference(avatar_component_clause,[],[f1125]) ).
fof(f1138,definition,
( spl34_146
<=> e1 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl34_146])],[avatar_definition]) ).
fof(f1140,plain,
( e1 = op(e4,e3)
| ~ spl34_146 ),
inference(avatar_component_clause,[],[f1138]) ).
fof(f1168,definition,
( spl34_153
<=> e0 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl34_153])],[avatar_definition]) ).
fof(f1172,definition,
( spl34_154
<=> e0 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl34_154])],[avatar_definition]) ).
fof(f1193,definition,
( spl34_159
<=> e4 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl34_159])],[avatar_definition]) ).
fof(f1194,plain,
( e4 != op(e0,e3)
| spl34_159 ),
inference(avatar_component_clause,[],[f1193]) ).
fof(f1195,plain,
( e4 = op(e0,e3)
| ~ spl34_159 ),
inference(avatar_component_clause,[],[f1193]) ).
fof(f1198,definition,
( spl34_160
<=> e4 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl34_160])],[avatar_definition]) ).
fof(f1200,plain,
( e4 = op(e3,e2)
| ~ spl34_160 ),
inference(avatar_component_clause,[],[f1198]) ).
fof(f1206,definition,
( spl34_162
<=> e4 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl34_162])],[avatar_definition]) ).
fof(f1208,plain,
( e4 = op(e3,e0)
| ~ spl34_162 ),
inference(avatar_component_clause,[],[f1206]) ).
fof(f1215,definition,
( spl34_164
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl34_164])],[avatar_definition]) ).
fof(f1217,plain,
( e3 = op(e1,e3)
| ~ spl34_164 ),
inference(avatar_component_clause,[],[f1215]) ).
fof(f1219,definition,
( spl34_165
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl34_165])],[avatar_definition]) ).
fof(f1221,plain,
( e3 = op(e0,e3)
| ~ spl34_165 ),
inference(avatar_component_clause,[],[f1219]) ).
fof(f1229,definition,
( spl34_167
<=> e2 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl34_167])],[avatar_definition]) ).
fof(f1234,definition,
( spl34_168
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl34_168])],[avatar_definition]) ).
fof(f1236,plain,
( e2 = op(e3,e2)
| ~ spl34_168 ),
inference(avatar_component_clause,[],[f1234]) ).
fof(f1242,definition,
( spl34_170
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl34_170])],[avatar_definition]) ).
fof(f1244,plain,
( e2 = op(e3,e0)
| ~ spl34_170 ),
inference(avatar_component_clause,[],[f1242]) ).
fof(f1251,definition,
( spl34_172
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl34_172])],[avatar_definition]) ).
fof(f1253,plain,
( e1 = op(e0,e3)
| ~ spl34_172 ),
inference(avatar_component_clause,[],[f1251]) ).
fof(f1256,definition,
( spl34_173
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl34_173])],[avatar_definition]) ).
fof(f1260,definition,
( spl34_174
<=> e1 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl34_174])],[avatar_definition]) ).
fof(f1278,definition,
( spl34_178
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl34_178])],[avatar_definition]) ).
fof(f1280,plain,
( e0 = op(e3,e2)
| ~ spl34_178 ),
inference(avatar_component_clause,[],[f1278]) ).
fof(f1295,definition,
( spl34_182
<=> e4 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl34_182])],[avatar_definition]) ).
fof(f1297,plain,
( e4 = op(e0,e2)
| ~ spl34_182 ),
inference(avatar_component_clause,[],[f1295]) ).
fof(f1300,definition,
( spl34_183
<=> e4 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl34_183])],[avatar_definition]) ).
fof(f1302,plain,
( e4 = op(e2,e1)
| ~ spl34_183 ),
inference(avatar_component_clause,[],[f1300]) ).
fof(f1304,definition,
( spl34_184
<=> e4 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl34_184])],[avatar_definition]) ).
fof(f1306,plain,
( e4 = op(e2,e0)
| ~ spl34_184 ),
inference(avatar_component_clause,[],[f1304]) ).
fof(f1313,definition,
( spl34_186
<=> e3 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl34_186])],[avatar_definition]) ).
fof(f1318,definition,
( spl34_187
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl34_187])],[avatar_definition]) ).
fof(f1322,definition,
( spl34_188
<=> e3 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl34_188])],[avatar_definition]) ).
fof(f1327,definition,
( spl34_189
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl34_189])],[avatar_definition]) ).
fof(f1329,plain,
( e2 = op(e1,e2)
| ~ spl34_189 ),
inference(avatar_component_clause,[],[f1327]) ).
fof(f1331,definition,
( spl34_190
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl34_190])],[avatar_definition]) ).
fof(f1333,plain,
( e2 = op(e0,e2)
| ~ spl34_190 ),
inference(avatar_component_clause,[],[f1331]) ).
fof(f1337,definition,
( spl34_191
<=> e1 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl34_191])],[avatar_definition]) ).
fof(f1342,definition,
( spl34_192
<=> e1 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl34_192])],[avatar_definition]) ).
fof(f1346,definition,
( spl34_193
<=> e1 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl34_193])],[avatar_definition]) ).
fof(f1348,plain,
( e1 = op(e2,e0)
| ~ spl34_193 ),
inference(avatar_component_clause,[],[f1346]) ).
fof(f1356,definition,
( spl34_195
<=> e0 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl34_195])],[avatar_definition]) ).
fof(f1358,plain,
( e0 = op(e2,e1)
| ~ spl34_195 ),
inference(avatar_component_clause,[],[f1356]) ).
fof(f1360,definition,
( spl34_196
<=> e0 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl34_196])],[avatar_definition]) ).
fof(f1370,definition,
( spl34_198
<=> e4 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl34_198])],[avatar_definition]) ).
fof(f1385,definition,
( spl34_201
<=> e2 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl34_201])],[avatar_definition]) ).
fof(f1387,plain,
( e2 = op(e0,e1)
| ~ spl34_201 ),
inference(avatar_component_clause,[],[f1385]) ).
fof(f1390,definition,
( spl34_202
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl34_202])],[avatar_definition]) ).
fof(f1392,plain,
( e2 = op(e1,e0)
| ~ spl34_202 ),
inference(avatar_component_clause,[],[f1390]) ).
fof(f1395,definition,
( spl34_203
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl34_203])],[avatar_definition]) ).
fof(f1397,plain,
( e1 = op(e0,e1)
| ~ spl34_203 ),
inference(avatar_component_clause,[],[f1395]) ).
fof(f1402,definition,
( spl34_204
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl34_204])],[avatar_definition]) ).
fof(f1404,plain,
( e0 = op(e1,e0)
| ~ spl34_204 ),
inference(avatar_component_clause,[],[f1402]) ).
fof(f1406,plain,
( spl34_73
| spl34_162
| spl34_184
| spl34_198
| spl34_74 ),
inference(avatar_split_clause,[],[f155,f763,f1370,f1304,f1206,f758]) ).
fof(f1410,plain,
( spl34_142
| spl34_170
| spl34_93
| spl34_202
| spl34_94 ),
inference(avatar_split_clause,[],[f159,f873,f1390,f868,f1242,f1120]) ).
fof(f1417,definition,
( spl34_205
<=> e4 = unit ),
introduced(definition,[new_symbols(definition,[spl34_205])],[avatar_definition]) ).
fof(f1419,plain,
( e4 = unit
| ~ spl34_205 ),
inference(avatar_component_clause,[],[f1417]) ).
fof(f1421,definition,
( spl34_206
<=> e3 = unit ),
introduced(definition,[new_symbols(definition,[spl34_206])],[avatar_definition]) ).
fof(f1423,plain,
( e3 = unit
| ~ spl34_206 ),
inference(avatar_component_clause,[],[f1421]) ).
fof(f1425,definition,
( spl34_207
<=> e2 = unit ),
introduced(definition,[new_symbols(definition,[spl34_207])],[avatar_definition]) ).
fof(f1427,plain,
( e2 = unit
| ~ spl34_207 ),
inference(avatar_component_clause,[],[f1425]) ).
fof(f1429,definition,
( spl34_208
<=> e1 = unit ),
introduced(definition,[new_symbols(definition,[spl34_208])],[avatar_definition]) ).
fof(f1431,plain,
( e1 = unit
| ~ spl34_208 ),
inference(avatar_component_clause,[],[f1429]) ).
fof(f1433,definition,
( spl34_209
<=> e0 = unit ),
introduced(definition,[new_symbols(definition,[spl34_209])],[avatar_definition]) ).
fof(f1435,plain,
( e0 = unit
| ~ spl34_209 ),
inference(avatar_component_clause,[],[f1433]) ).
fof(f1436,plain,
( spl34_205
| spl34_206
| spl34_207
| spl34_208
| spl34_209 ),
inference(avatar_split_clause,[],[f104,f1433,f1429,f1425,f1421,f1417]) ).
fof(f1438,plain,
( spl34_64
| spl34_132
| spl34_139
| spl34_146
| spl34_153 ),
inference(avatar_split_clause,[],[f80,f1168,f1138,f1108,f1078,f713]) ).
fof(f1444,plain,
( spl34_160
| spl34_78
| spl34_168
| spl34_173
| spl34_178 ),
inference(avatar_split_clause,[],[f86,f1278,f1256,f1234,f787,f1198]) ).
fof(f1450,plain,
( spl34_183
| spl34_187
| spl34_90
| spl34_192
| spl34_195 ),
inference(avatar_split_clause,[],[f92,f1356,f1342,f853,f1318,f1300]) ).
fof(f1451,plain,
( spl34_184
| spl34_188
| spl34_93
| spl34_193
| spl34_196 ),
inference(avatar_split_clause,[],[f93,f1360,f1346,f868,f1322,f1304]) ).
fof(f1458,plain,
( spl34_159
| spl34_165
| spl34_167
| spl34_172
| spl34_104 ),
inference(avatar_split_clause,[],[f100,f933,f1251,f1229,f1219,f1193]) ).
fof(f1459,plain,
( spl34_182
| spl34_186
| spl34_190
| spl34_191
| spl34_105 ),
inference(avatar_split_clause,[],[f101,f940,f1337,f1331,f1313,f1295]) ).
fof(f1469,plain,
( e2 = op(e2,e4)
| ~ spl34_205 ),
inference(superposition,[],[f109,f1419]) ).
fof(f1470,plain,
( spl34_87
| ~ spl34_205 ),
inference(avatar_split_clause,[],[f1469,f1417,f832]) ).
fof(f1487,plain,
( e4 != op(e1,e4)
| spl34_32
| ~ spl34_127 ),
inference(superposition,[],[f546,f1057]) ).
fof(f1490,plain,
( $false
| spl34_32
| ~ spl34_127 ),
inference(forward_subsumption_resolution,[],[f1487,f1057]) ).
fof(f1491,plain,
( spl34_32
| ~ spl34_127 ),
inference(avatar_contradiction_clause,[],[f1490]) ).
fof(f1520,plain,
( e4 != op(e4,e0)
| ~ spl34_63 ),
inference(superposition,[],[f171,f707]) ).
fof(f1521,plain,
( ~ spl34_73
| ~ spl34_63 ),
inference(avatar_split_clause,[],[f1520,f706,f758]) ).
fof(f1555,plain,
( e4 != op(e2,e2)
| ~ spl34_126 ),
inference(superposition,[],[f186,f1053]) ).
fof(f1556,plain,
( ~ spl34_68
| ~ spl34_126 ),
inference(avatar_split_clause,[],[f1555,f1051,f733]) ).
fof(f1596,plain,
( e4 = op(e2,e4)
| ~ spl34_207 ),
inference(superposition,[],[f106,f1427]) ).
fof(f1613,plain,
( $false
| spl34_126
| ~ spl34_207 ),
inference(forward_subsumption_resolution,[],[f1596,f1052]) ).
fof(f1614,plain,
( spl34_126
| ~ spl34_207 ),
inference(avatar_contradiction_clause,[],[f1613]) ).
fof(f1624,plain,
( e1 = op(e3,e1)
| ~ spl34_206 ),
inference(superposition,[],[f112,f1423]) ).
fof(f1630,plain,
( spl34_174
| ~ spl34_206 ),
inference(avatar_split_clause,[],[f1624,f1421,f1260]) ).
fof(f1639,plain,
( e4 = op(e4,e0)
| ~ spl34_209 ),
inference(superposition,[],[f105,f1435]) ).
fof(f1640,plain,
( e4 = op(e0,e4)
| ~ spl34_209 ),
inference(superposition,[],[f106,f1435]) ).
fof(f1641,plain,
( e3 = op(e3,e0)
| ~ spl34_209 ),
inference(superposition,[],[f107,f1435]) ).
fof(f1642,plain,
( e3 = op(e0,e3)
| ~ spl34_209 ),
inference(superposition,[],[f108,f1435]) ).
fof(f1643,plain,
( e2 = op(e2,e0)
| ~ spl34_209 ),
inference(superposition,[],[f109,f1435]) ).
fof(f1644,plain,
( e2 = op(e0,e2)
| ~ spl34_209 ),
inference(superposition,[],[f110,f1435]) ).
fof(f1645,plain,
( e1 = op(e1,e0)
| ~ spl34_209 ),
inference(superposition,[],[f111,f1435]) ).
fof(f1646,plain,
( e1 = op(e0,e1)
| ~ spl34_209 ),
inference(superposition,[],[f112,f1435]) ).
fof(f1652,plain,
( spl34_203
| ~ spl34_209 ),
inference(avatar_split_clause,[],[f1646,f1433,f1395]) ).
fof(f1653,plain,
( spl34_100
| ~ spl34_209 ),
inference(avatar_split_clause,[],[f1645,f1433,f911]) ).
fof(f1654,plain,
( spl34_190
| ~ spl34_209 ),
inference(avatar_split_clause,[],[f1644,f1433,f1331]) ).
fof(f1655,plain,
( spl34_93
| ~ spl34_209 ),
inference(avatar_split_clause,[],[f1643,f1433,f868]) ).
fof(f1656,plain,
( spl34_165
| ~ spl34_209 ),
inference(avatar_split_clause,[],[f1642,f1433,f1219]) ).
fof(f1657,plain,
( spl34_84
| ~ spl34_209 ),
inference(avatar_split_clause,[],[f1641,f1433,f817]) ).
fof(f1658,plain,
( spl34_128
| ~ spl34_209 ),
inference(avatar_split_clause,[],[f1640,f1433,f1059]) ).
fof(f1659,plain,
( spl34_73
| ~ spl34_209 ),
inference(avatar_split_clause,[],[f1639,f1433,f758]) ).
fof(f1662,plain,
( e3 = op(e3,e1)
| ~ spl34_208 ),
inference(superposition,[],[f107,f1431]) ).
fof(f1663,plain,
( e3 = op(e1,e3)
| ~ spl34_208 ),
inference(superposition,[],[f108,f1431]) ).
fof(f1664,plain,
( e2 = op(e2,e1)
| ~ spl34_208 ),
inference(superposition,[],[f109,f1431]) ).
fof(f1665,plain,
( e2 = op(e1,e2)
| ~ spl34_208 ),
inference(superposition,[],[f110,f1431]) ).
fof(f1668,plain,
( e0 = op(e0,e1)
| ~ spl34_208 ),
inference(superposition,[],[f113,f1431]) ).
fof(f1669,plain,
( e0 = op(e1,e0)
| ~ spl34_208 ),
inference(superposition,[],[f114,f1431]) ).
fof(f1673,plain,
( spl34_204
| ~ spl34_208 ),
inference(avatar_split_clause,[],[f1669,f1429,f1402]) ).
fof(f1674,plain,
( spl34_106
| ~ spl34_208 ),
inference(avatar_split_clause,[],[f1668,f1429,f947]) ).
fof(f1676,plain,
( spl34_189
| ~ spl34_208 ),
inference(avatar_split_clause,[],[f1665,f1429,f1327]) ).
fof(f1677,plain,
( spl34_90
| ~ spl34_208 ),
inference(avatar_split_clause,[],[f1664,f1429,f853]) ).
fof(f1678,plain,
( spl34_164
| ~ spl34_208 ),
inference(avatar_split_clause,[],[f1663,f1429,f1215]) ).
fof(f1679,plain,
( spl34_81
| ~ spl34_208 ),
inference(avatar_split_clause,[],[f1662,f1429,f802]) ).
fof(f1735,plain,
( e2 != op(e1,e2)
| ~ spl34_137 ),
inference(superposition,[],[f196,f1101]) ).
fof(f1736,plain,
( e2 != op(e1,e1)
| ~ spl34_137 ),
inference(superposition,[],[f198,f1101]) ).
fof(f1747,plain,
( ~ spl34_91
| ~ spl34_137 ),
inference(avatar_split_clause,[],[f1736,f1099,f858]) ).
fof(f1748,plain,
( ~ spl34_189
| ~ spl34_137 ),
inference(avatar_split_clause,[],[f1735,f1099,f1327]) ).
fof(f1790,plain,
( e2 != op(e2,e4)
| spl34_44
| ~ spl34_68 ),
inference(superposition,[],[f607,f735]) ).
fof(f1791,plain,
( ~ spl34_87
| spl34_44
| ~ spl34_68 ),
inference(avatar_split_clause,[],[f1790,f733,f606,f832]) ).
fof(f1793,plain,
( e3 != op(e2,e2)
| ~ spl34_129 ),
inference(superposition,[],[f186,f1067]) ).
fof(f1794,plain,
( e3 != op(e2,e1)
| ~ spl34_129 ),
inference(superposition,[],[f188,f1067]) ).
fof(f1795,plain,
( e3 != op(e2,e0)
| ~ spl34_129 ),
inference(superposition,[],[f191,f1067]) ).
fof(f1796,plain,
( e2 = op(e4,e3)
| ~ spl34_28
| ~ spl34_129 ),
inference(superposition,[],[f528,f1067]) ).
fof(f1803,plain,
( ~ spl34_188
| ~ spl34_129 ),
inference(avatar_split_clause,[],[f1795,f1065,f1322]) ).
fof(f1804,plain,
( ~ spl34_187
| ~ spl34_129 ),
inference(avatar_split_clause,[],[f1794,f1065,f1318]) ).
fof(f1805,plain,
( ~ spl34_79
| ~ spl34_129 ),
inference(avatar_split_clause,[],[f1793,f1065,f792]) ).
fof(f1817,plain,
( e4 != op(e4,e1)
| ~ spl34_64 ),
inference(superposition,[],[f169,f714]) ).
fof(f1927,plain,
( spl34_139
| ~ spl34_28
| ~ spl34_129 ),
inference(avatar_split_clause,[],[f1796,f1065,f526,f1108]) ).
fof(f1939,plain,
( e2 != op(e4,e0)
| ~ spl34_139 ),
inference(superposition,[],[f172,f1110]) ).
fof(f1961,plain,
( e2 = op(e0,e1)
| ~ spl34_58
| ~ spl34_193 ),
inference(superposition,[],[f680,f1348]) ).
fof(f1962,plain,
( spl34_201
| ~ spl34_58
| ~ spl34_193 ),
inference(avatar_split_clause,[],[f1961,f1346,f678,f1385]) ).
fof(f1972,plain,
( e2 != op(e1,e2)
| ~ spl34_168 ),
inference(superposition,[],[f239,f1236]) ).
fof(f2030,plain,
( e0 != op(e2,e2)
| ~ spl34_195 ),
inference(superposition,[],[f190,f1358]) ).
fof(f2042,plain,
( ~ spl34_95
| ~ spl34_195 ),
inference(avatar_split_clause,[],[f2030,f1356,f878]) ).
fof(f2094,plain,
( e3 != op(e3,e1)
| ~ spl34_134 ),
inference(superposition,[],[f245,f1088]) ).
fof(f2100,plain,
( ~ spl34_81
| ~ spl34_134 ),
inference(avatar_split_clause,[],[f2094,f1086,f802]) ).
fof(f2125,plain,
( e3 != op(e0,e3)
| ~ spl34_164 ),
inference(superposition,[],[f234,f1217]) ).
fof(f2133,plain,
( ~ spl34_165
| ~ spl34_164 ),
inference(avatar_split_clause,[],[f2125,f1215,f1219]) ).
fof(f2155,plain,
( e3 != op(e0,e2)
| ~ spl34_133 ),
inference(superposition,[],[f241,f1084]) ).
fof(f2203,plain,
( e3 != op(e2,e4)
| ~ spl34_66 ),
inference(superposition,[],[f216,f725]) ).
fof(f2222,plain,
( op(e0,e0) != e1
| ~ spl34_203 ),
inference(superposition,[],[f214,f1397]) ).
fof(f2230,plain,
( ~ spl34_101
| ~ spl34_203 ),
inference(avatar_split_clause,[],[f2222,f1395,f916]) ).
fof(f2255,plain,
( e1 != op(e3,e4)
| ~ spl34_72 ),
inference(superposition,[],[f215,f755]) ).
fof(f2265,plain,
( ~ spl34_143
| ~ spl34_72 ),
inference(avatar_split_clause,[],[f2255,f753,f1125]) ).
fof(f2289,plain,
( op(e0,e0) != e4
| ~ spl34_128 ),
inference(superposition,[],[f211,f1061]) ).
fof(f2298,plain,
( ~ spl34_74
| ~ spl34_128 ),
inference(avatar_split_clause,[],[f2289,f1059,f763]) ).
fof(f2329,plain,
( e3 != op(e1,e3)
| ~ spl34_132 ),
inference(superposition,[],[f228,f1080]) ).
fof(f2333,plain,
( ~ spl34_164
| ~ spl34_132 ),
inference(avatar_split_clause,[],[f2329,f1078,f1215]) ).
fof(f2334,plain,
( e1 != op(e3,e3)
| ~ spl34_143 ),
inference(superposition,[],[f175,f1127]) ).
fof(f2335,plain,
( e1 != op(e3,e2)
| ~ spl34_143 ),
inference(superposition,[],[f176,f1127]) ).
fof(f2336,plain,
( e1 != op(e3,e1)
| ~ spl34_143 ),
inference(superposition,[],[f178,f1127]) ).
fof(f2343,plain,
( ~ spl34_174
| ~ spl34_143 ),
inference(avatar_split_clause,[],[f2336,f1125,f1260]) ).
fof(f2344,plain,
( ~ spl34_83
| ~ spl34_143 ),
inference(avatar_split_clause,[],[f2334,f1125,f812]) ).
fof(f2351,plain,
( e1 != op(e0,e3)
| ~ spl34_146 ),
inference(superposition,[],[f231,f1140]) ).
fof(f2354,plain,
( ~ spl34_172
| ~ spl34_146 ),
inference(avatar_split_clause,[],[f2351,f1138,f1251]) ).
fof(f2377,plain,
( op(e0,e0) != e3
| ~ spl34_165 ),
inference(superposition,[],[f212,f1221]) ).
fof(f2381,plain,
( ~ spl34_85
| ~ spl34_165 ),
inference(avatar_split_clause,[],[f2377,f1219,f822]) ).
fof(f2386,plain,
( e0 != op(e0,e2)
| ~ spl34_178 ),
inference(superposition,[],[f242,f1280]) ).
fof(f2390,plain,
( ~ spl34_105
| ~ spl34_178 ),
inference(avatar_split_clause,[],[f2386,f1278,f940]) ).
fof(f2433,plain,
( e4 != op(e2,e2)
| ~ spl34_183 ),
inference(superposition,[],[f190,f1302]) ).
fof(f2438,plain,
( $false
| ~ spl34_68
| ~ spl34_183 ),
inference(forward_subsumption_resolution,[],[f2433,f735]) ).
fof(f2439,plain,
( ~ spl34_68
| ~ spl34_183 ),
inference(avatar_contradiction_clause,[],[f2438]) ).
fof(f2442,plain,
( ~ spl34_173
| ~ spl34_143 ),
inference(avatar_split_clause,[],[f2335,f1125,f1256]) ).
fof(f2504,plain,
( e4 != op(e2,e2)
| ~ spl34_160 ),
inference(superposition,[],[f237,f1200]) ).
fof(f2509,plain,
( $false
| ~ spl34_68
| ~ spl34_160 ),
inference(forward_subsumption_resolution,[],[f2504,f735]) ).
fof(f2510,plain,
( ~ spl34_68
| ~ spl34_160 ),
inference(avatar_contradiction_clause,[],[f2509]) ).
fof(f2516,plain,
( e2 != op(e2,e2)
| ~ spl34_190 ),
inference(superposition,[],[f243,f1333]) ).
fof(f2521,plain,
( ~ spl34_89
| ~ spl34_190 ),
inference(avatar_split_clause,[],[f2516,f1331,f846]) ).
fof(f2551,plain,
( op(e0,e0) = e1
| ~ spl34_59
| ~ spl34_204 ),
inference(superposition,[],[f684,f1404]) ).
fof(f2558,plain,
( spl34_101
| ~ spl34_59
| ~ spl34_204 ),
inference(avatar_split_clause,[],[f2551,f1402,f682,f916]) ).
fof(f2562,plain,
( e1 != op(e2,e1)
| ~ spl34_203 ),
inference(superposition,[],[f253,f1397]) ).
fof(f2588,plain,
( e2 != op(e2,e1)
| ~ spl34_201 ),
inference(superposition,[],[f253,f1387]) ).
fof(f2600,plain,
( ~ spl34_90
| ~ spl34_201 ),
inference(avatar_split_clause,[],[f2588,f1385,f853]) ).
fof(f2610,plain,
( ~ spl34_192
| ~ spl34_203 ),
inference(avatar_split_clause,[],[f2562,f1395,f1342]) ).
fof(f2612,plain,
( ~ spl34_142
| ~ spl34_139 ),
inference(avatar_split_clause,[],[f1939,f1108,f1120]) ).
fof(f2736,plain,
( e2 != op(e1,e2)
| ~ spl34_202 ),
inference(superposition,[],[f203,f1392]) ).
fof(f2768,plain,
( e3 = op(e2,e4)
| ~ spl34_68 ),
inference(superposition,[],[f276,f735]) ).
fof(f2773,plain,
( ~ spl34_129
| ~ spl34_66 ),
inference(avatar_split_clause,[],[f2203,f723,f1065]) ).
fof(f2774,plain,
( spl34_129
| ~ spl34_68 ),
inference(avatar_split_clause,[],[f2768,f733,f1065]) ).
fof(f2845,plain,
( e4 != op(e1,e0)
| ~ spl34_127 ),
inference(superposition,[],[f201,f1057]) ).
fof(f2855,plain,
( ~ spl34_198
| ~ spl34_127 ),
inference(avatar_split_clause,[],[f2845,f1055,f1370]) ).
fof(f2948,plain,
( e0 = op(e4,e4)
| ~ spl34_68 ),
inference(superposition,[],[f278,f735]) ).
fof(f2949,plain,
( spl34_75
| ~ spl34_68 ),
inference(avatar_split_clause,[],[f2948,f733,f768]) ).
fof(f2956,plain,
e1 = op(e3,op(e2,e2)),
inference(superposition,[],[f277,f276]) ).
fof(f2958,plain,
( e1 = op(e3,e4)
| ~ spl34_68 ),
inference(superposition,[],[f2956,f735]) ).
fof(f2963,plain,
( spl34_143
| ~ spl34_68 ),
inference(avatar_split_clause,[],[f2958,f733,f1125]) ).
fof(f2965,plain,
( e4 = op(e4,e1)
| ~ spl34_208 ),
inference(superposition,[],[f105,f1431]) ).
fof(f2966,plain,
( e4 = op(e1,e4)
| ~ spl34_208 ),
inference(superposition,[],[f106,f1431]) ).
fof(f2978,plain,
( spl34_127
| ~ spl34_208 ),
inference(avatar_split_clause,[],[f2966,f1429,f1055]) ).
fof(f2979,plain,
( spl34_70
| ~ spl34_208 ),
inference(avatar_split_clause,[],[f2965,f1429,f743]) ).
fof(f2999,plain,
( e2 != op(e0,e3)
| ~ spl34_138 ),
inference(superposition,[],[f205,f1105]) ).
fof(f3000,plain,
( e2 != op(e0,e2)
| ~ spl34_138 ),
inference(superposition,[],[f206,f1105]) ).
fof(f3002,plain,
( op(e0,e0) != e2
| ~ spl34_138 ),
inference(superposition,[],[f211,f1105]) ).
fof(f3004,plain,
( e0 = op(e4,e2)
| ~ spl34_30
| ~ spl34_138 ),
inference(superposition,[],[f536,f1105]) ).
fof(f3012,plain,
( ~ spl34_94
| ~ spl34_138 ),
inference(avatar_split_clause,[],[f3002,f1103,f873]) ).
fof(f3015,plain,
( ~ spl34_190
| ~ spl34_138 ),
inference(avatar_split_clause,[],[f3000,f1103,f1331]) ).
fof(f3040,plain,
( ~ spl34_186
| ~ spl34_133 ),
inference(avatar_split_clause,[],[f2155,f1082,f1313]) ).
fof(f3042,plain,
( spl34_154
| ~ spl34_30
| ~ spl34_138 ),
inference(avatar_split_clause,[],[f3004,f1103,f534,f1172]) ).
fof(f3044,plain,
( ~ spl34_189
| ~ spl34_202 ),
inference(avatar_split_clause,[],[f2736,f1390,f1327]) ).
fof(f3054,plain,
( e1 = e2
| ~ spl34_136
| ~ spl34_143 ),
inference(superposition,[],[f1097,f1127]) ).
fof(f3067,plain,
( $false
| ~ spl34_136
| ~ spl34_143 ),
inference(forward_subsumption_resolution,[],[f3054,f270]) ).
fof(f3068,plain,
( ~ spl34_136
| ~ spl34_143 ),
inference(avatar_contradiction_clause,[],[f3067]) ).
fof(f3111,plain,
( e4 != op(e2,e2)
| ~ spl34_182 ),
inference(superposition,[],[f243,f1297]) ).
fof(f3113,plain,
( $false
| ~ spl34_68
| ~ spl34_182 ),
inference(forward_subsumption_resolution,[],[f3111,f735]) ).
fof(f3114,plain,
( ~ spl34_68
| ~ spl34_182 ),
inference(avatar_contradiction_clause,[],[f3113]) ).
fof(f3116,plain,
( ~ spl34_189
| ~ spl34_168 ),
inference(avatar_split_clause,[],[f1972,f1234,f1327]) ).
fof(f3119,plain,
( e2 = e3
| ~ spl34_44 ),
inference(superposition,[],[f608,f276]) ).
fof(f3124,plain,
( $false
| ~ spl34_44 ),
inference(forward_subsumption_resolution,[],[f3119,f267]) ).
fof(f3125,plain,
~ spl34_44,
inference(avatar_contradiction_clause,[],[f3124]) ).
fof(f3126,plain,
( ~ spl34_70
| ~ spl34_64 ),
inference(avatar_split_clause,[],[f1817,f713,f743]) ).
fof(f3143,plain,
( op(e0,e0) != e4
| ~ spl34_159 ),
inference(superposition,[],[f212,f1195]) ).
fof(f3151,plain,
( ~ spl34_74
| ~ spl34_159 ),
inference(avatar_split_clause,[],[f3143,f1193,f763]) ).
fof(f3174,plain,
( e1 != op(e0,e2)
| ~ spl34_172 ),
inference(superposition,[],[f207,f1253]) ).
fof(f3176,plain,
( op(e0,e0) != e1
| ~ spl34_172 ),
inference(superposition,[],[f212,f1253]) ).
fof(f3188,plain,
( ~ spl34_101
| ~ spl34_172 ),
inference(avatar_split_clause,[],[f3176,f1251,f916]) ).
fof(f3191,plain,
( ~ spl34_191
| ~ spl34_172 ),
inference(avatar_split_clause,[],[f3174,f1251,f1337]) ).
fof(f3200,plain,
( e2 = e4
| ~ spl34_162
| ~ spl34_170 ),
inference(superposition,[],[f1208,f1244]) ).
fof(f3212,plain,
( $false
| ~ spl34_162
| ~ spl34_170 ),
inference(forward_subsumption_resolution,[],[f3200,f266]) ).
fof(f3213,plain,
( ~ spl34_162
| ~ spl34_170 ),
inference(avatar_contradiction_clause,[],[f3212]) ).
fof(f3233,plain,
( e4 != op(e2,e2)
| ~ spl34_184 ),
inference(superposition,[],[f193,f1306]) ).
fof(f3240,plain,
( $false
| ~ spl34_68
| ~ spl34_184 ),
inference(forward_subsumption_resolution,[],[f3233,f735]) ).
fof(f3241,plain,
( ~ spl34_68
| ~ spl34_184 ),
inference(avatar_contradiction_clause,[],[f3240]) ).
fof(f3243,plain,
( e2 != op(e0,e2)
| ~ spl34_189 ),
inference(superposition,[],[f244,f1329]) ).
fof(f3252,plain,
( ~ spl34_190
| ~ spl34_189 ),
inference(avatar_split_clause,[],[f3243,f1327,f1331]) ).
fof(f3301,plain,
( e0 != op(e2,e0)
| ~ spl34_204 ),
inference(superposition,[],[f260,f1404]) ).
fof(f3311,plain,
( ~ spl34_196
| ~ spl34_204 ),
inference(avatar_split_clause,[],[f3301,f1402,f1360]) ).
fof(f3337,plain,
( e4 != op(e4,e0)
| ~ spl34_70 ),
inference(superposition,[],[f174,f744]) ).
fof(f3347,plain,
( ~ spl34_73
| ~ spl34_70 ),
inference(avatar_split_clause,[],[f3337,f743,f758]) ).
fof(f3353,plain,
( e0 = e2
| ~ spl34_69
| ~ spl34_75 ),
inference(superposition,[],[f770,f740]) ).
fof(f3354,plain,
( e0 != op(e4,e3)
| ~ spl34_75 ),
inference(superposition,[],[f165,f770]) ).
fof(f3355,plain,
( e0 != op(e4,e2)
| ~ spl34_75 ),
inference(superposition,[],[f166,f770]) ).
fof(f3371,plain,
( $false
| ~ spl34_69
| ~ spl34_75 ),
inference(forward_subsumption_resolution,[],[f3353,f273]) ).
fof(f3372,plain,
( ~ spl34_69
| ~ spl34_75 ),
inference(avatar_contradiction_clause,[],[f3371]) ).
fof(f3385,plain,
( ~ spl34_153
| ~ spl34_75 ),
inference(avatar_split_clause,[],[f3354,f768,f1168]) ).
fof(f3392,plain,
( ~ spl34_167
| ~ spl34_138 ),
inference(avatar_split_clause,[],[f2999,f1103,f1229]) ).
fof(f3500,plain,
( e3 != op(e3,e2)
| ~ spl34_81 ),
inference(superposition,[],[f180,f803]) ).
fof(f3515,plain,
( e0 != op(e3,e2)
| ~ spl34_86 ),
inference(superposition,[],[f177,f829]) ).
fof(f3530,plain,
( $false
| ~ spl34_86
| ~ spl34_178 ),
inference(forward_subsumption_resolution,[],[f3515,f1280]) ).
fof(f3531,plain,
( ~ spl34_86
| ~ spl34_178 ),
inference(avatar_contradiction_clause,[],[f3530]) ).
fof(f3539,plain,
( e2 != op(e2,e0)
| ~ spl34_90 ),
inference(superposition,[],[f194,f854]) ).
fof(f3549,plain,
( ~ spl34_93
| ~ spl34_90 ),
inference(avatar_split_clause,[],[f3539,f853,f868]) ).
fof(f3596,plain,
( e1 != op(e1,e0)
| ~ spl34_99 ),
inference(superposition,[],[f204,f905]) ).
fof(f3603,plain,
( ~ spl34_100
| ~ spl34_99 ),
inference(avatar_split_clause,[],[f3596,f904,f911]) ).
fof(f3610,plain,
( e0 != op(e0,e1)
| ~ spl34_104 ),
inference(superposition,[],[f209,f934]) ).
fof(f3623,plain,
( ~ spl34_106
| ~ spl34_104 ),
inference(avatar_split_clause,[],[f3610,f933,f947]) ).
fof(f3641,plain,
( e3 = op(e4,e1)
| ~ spl34_108
| ~ spl34_143 ),
inference(superposition,[],[f962,f1127]) ).
fof(f3642,plain,
( $false
| ~ spl34_108
| spl34_134
| ~ spl34_143 ),
inference(forward_subsumption_resolution,[],[f3641,f1087]) ).
fof(f3643,plain,
( ~ spl34_108
| spl34_134
| ~ spl34_143 ),
inference(avatar_contradiction_clause,[],[f3642]) ).
fof(f3660,plain,
( e0 != op(e3,e2)
| spl34_124
| ~ spl34_170 ),
inference(superposition,[],[f1043,f1244]) ).
fof(f3665,plain,
( ~ spl34_178
| spl34_124
| ~ spl34_170 ),
inference(avatar_split_clause,[],[f3660,f1242,f1041,f1278]) ).
fof(f3666,plain,
( ~ spl34_154
| ~ spl34_75 ),
inference(avatar_split_clause,[],[f3355,f768,f1172]) ).
fof(f3667,plain,
( ~ spl34_78
| ~ spl34_81 ),
inference(avatar_split_clause,[],[f3500,f802,f787]) ).
fof(f3678,plain,
( e4 = op(e0,e3)
| ~ spl34_121
| ~ spl34_135 ),
inference(superposition,[],[f1028,f1092]) ).
fof(f3679,plain,
( $false
| ~ spl34_121
| ~ spl34_135
| spl34_159 ),
inference(forward_subsumption_resolution,[],[f3678,f1194]) ).
fof(f3680,plain,
( ~ spl34_121
| ~ spl34_135
| spl34_159 ),
inference(avatar_contradiction_clause,[],[f3679]) ).
cnf(s1,plain,
( spl34_1
| spl34_2
| spl34_3
| spl34_4
| spl34_5
| spl34_6
| spl34_7
| spl34_8
| spl34_9
| spl34_10
| spl34_11
| spl34_12
| spl34_13
| spl34_14
| spl34_15
| spl34_16
| spl34_17
| spl34_18
| spl34_19
| spl34_20
| spl34_21
| spl34_22
| spl34_23
| spl34_24
| ~ spl34_25 ),
inference(sat_conversion,[],[f514]) ).
cnf(s3,plain,
( spl34_1
| spl34_2
| spl34_3
| spl34_4
| spl34_5
| spl34_6
| spl34_7
| spl34_8
| spl34_9
| spl34_10
| spl34_11
| spl34_12
| spl34_13
| spl34_14
| spl34_15
| spl34_16
| spl34_17
| spl34_18
| spl34_19
| spl34_20
| spl34_21
| spl34_22
| spl34_23
| spl34_24
| spl34_25 ),
inference(sat_conversion,[],[f516]) ).
cnf(s6,plain,
( spl34_26
| spl34_27
| spl34_28
| spl34_30
| ~ spl34_32 ),
inference(sat_conversion,[],[f547]) ).
cnf(s36,plain,
( spl34_56
| spl34_57
| spl34_58
| spl34_59
| spl34_60 ),
inference(sat_conversion,[],[f689]) ).
cnf(s40,plain,
( spl34_56
| spl34_57
| spl34_58
| spl34_59
| ~ spl34_60 ),
inference(sat_conversion,[],[f701]) ).
cnf(s45,plain,
( ~ spl34_1
| spl34_63 ),
inference(sat_conversion,[],[f710]) ).
cnf(s49,plain,
( ~ spl34_2
| spl34_66 ),
inference(sat_conversion,[],[f726]) ).
cnf(s52,plain,
( ~ spl34_3
| spl34_69 ),
inference(sat_conversion,[],[f741]) ).
cnf(s55,plain,
( ~ spl34_4
| spl34_72 ),
inference(sat_conversion,[],[f756]) ).
cnf(s57,plain,
( ~ spl34_5
| spl34_74 ),
inference(sat_conversion,[],[f766]) ).
cnf(s60,plain,
( ~ spl34_6
| spl34_66 ),
inference(sat_conversion,[],[f777]) ).
cnf(s62,plain,
( ~ spl34_7
| ~ spl34_77 ),
inference(sat_conversion,[],[f783]) ).
cnf(s64,plain,
( ~ spl34_7
| spl34_77 ),
inference(sat_conversion,[],[f785]) ).
cnf(s66,plain,
( ~ spl34_8
| spl34_79 ),
inference(sat_conversion,[],[f795]) ).
cnf(s70,plain,
( ~ spl34_9
| spl34_83 ),
inference(sat_conversion,[],[f815]) ).
cnf(s71,plain,
( ~ spl34_10
| ~ spl34_84 ),
inference(sat_conversion,[],[f820]) ).
cnf(s75,plain,
( ~ spl34_11
| spl34_69 ),
inference(sat_conversion,[],[f836]) ).
cnf(s79,plain,
( ~ spl34_12
| spl34_79 ),
inference(sat_conversion,[],[f844]) ).
cnf(s82,plain,
( ~ spl34_13
| spl34_89 ),
inference(sat_conversion,[],[f851]) ).
cnf(s84,plain,
( ~ spl34_14
| spl34_91 ),
inference(sat_conversion,[],[f861]) ).
cnf(s86,plain,
( ~ spl34_15
| ~ spl34_93 ),
inference(sat_conversion,[],[f871]) ).
cnf(s90,plain,
( ~ spl34_16
| spl34_72 ),
inference(sat_conversion,[],[f887]) ).
cnf(s93,plain,
( ~ spl34_17
| spl34_83 ),
inference(sat_conversion,[],[f894]) ).
cnf(s97,plain,
( ~ spl34_18
| spl34_91 ),
inference(sat_conversion,[],[f902]) ).
cnf(s100,plain,
( ~ spl34_19
| spl34_99 ),
inference(sat_conversion,[],[f909]) ).
cnf(s101,plain,
( ~ spl34_20
| ~ spl34_100 ),
inference(sat_conversion,[],[f914]) ).
cnf(s106,plain,
( ~ spl34_21
| spl34_74 ),
inference(sat_conversion,[],[f931]) ).
cnf(s108,plain,
( ~ spl34_22
| spl34_86 ),
inference(sat_conversion,[],[f937]) ).
cnf(s109,plain,
( ~ spl34_22
| spl34_85 ),
inference(sat_conversion,[],[f938]) ).
cnf(s111,plain,
( ~ spl34_23
| spl34_95 ),
inference(sat_conversion,[],[f944]) ).
cnf(s112,plain,
( ~ spl34_23
| spl34_94 ),
inference(sat_conversion,[],[f945]) ).
cnf(s113,plain,
( ~ spl34_24
| ~ spl34_106 ),
inference(sat_conversion,[],[f950]) ).
cnf(s115,plain,
( ~ spl34_24
| spl34_101 ),
inference(sat_conversion,[],[f952]) ).
cnf(s116,plain,
( ~ spl34_26
| spl34_107 ),
inference(sat_conversion,[],[f957]) ).
cnf(s117,plain,
( ~ spl34_26
| ~ spl34_107 ),
inference(sat_conversion,[],[f958]) ).
cnf(s118,plain,
( ~ spl34_27
| spl34_108 ),
inference(sat_conversion,[],[f963]) ).
cnf(s132,plain,
( ~ spl34_56
| spl34_121 ),
inference(sat_conversion,[],[f1029]) ).
cnf(s135,plain,
( ~ spl34_57
| ~ spl34_124 ),
inference(sat_conversion,[],[f1044]) ).
cnf(s136,plain,
spl34_68,
inference(sat_conversion,[],[f1045]) ).
cnf(s140,plain,
( spl34_66
| spl34_132
| spl34_133
| spl34_134
| spl34_135 ),
inference(sat_conversion,[],[f1093]) ).
cnf(s141,plain,
( spl34_69
| spl34_87
| spl34_136
| spl34_137
| spl34_138 ),
inference(sat_conversion,[],[f1106]) ).
cnf(s177,plain,
( spl34_73
| spl34_74
| spl34_162
| spl34_184
| spl34_198 ),
inference(sat_conversion,[],[f1406]) ).
cnf(s181,plain,
( spl34_93
| spl34_94
| spl34_142
| spl34_170
| spl34_202 ),
inference(sat_conversion,[],[f1410]) ).
cnf(s187,plain,
( spl34_205
| spl34_206
| spl34_207
| spl34_208
| spl34_209 ),
inference(sat_conversion,[],[f1436]) ).
cnf(s189,plain,
( spl34_64
| spl34_132
| spl34_139
| spl34_146
| spl34_153 ),
inference(sat_conversion,[],[f1438]) ).
cnf(s195,plain,
( spl34_78
| spl34_160
| spl34_168
| spl34_173
| spl34_178 ),
inference(sat_conversion,[],[f1444]) ).
cnf(s201,plain,
( spl34_90
| spl34_183
| spl34_187
| spl34_192
| spl34_195 ),
inference(sat_conversion,[],[f1450]) ).
cnf(s202,plain,
( spl34_93
| spl34_184
| spl34_188
| spl34_193
| spl34_196 ),
inference(sat_conversion,[],[f1451]) ).
cnf(s209,plain,
( spl34_104
| spl34_159
| spl34_165
| spl34_167
| spl34_172 ),
inference(sat_conversion,[],[f1458]) ).
cnf(s210,plain,
( spl34_105
| spl34_182
| spl34_186
| spl34_190
| spl34_191 ),
inference(sat_conversion,[],[f1459]) ).
cnf(s217,plain,
( spl34_87
| ~ spl34_205 ),
inference(sat_conversion,[],[f1470]) ).
cnf(s226,plain,
( spl34_32
| ~ spl34_127 ),
inference(sat_conversion,[],[f1491]) ).
cnf(s237,plain,
( ~ spl34_63
| ~ spl34_73 ),
inference(sat_conversion,[],[f1521]) ).
cnf(s249,plain,
( ~ spl34_68
| ~ spl34_126 ),
inference(sat_conversion,[],[f1556]) ).
cnf(s272,plain,
( spl34_126
| ~ spl34_207 ),
inference(sat_conversion,[],[f1614]) ).
cnf(s276,plain,
( spl34_174
| ~ spl34_206 ),
inference(sat_conversion,[],[f1630]) ).
cnf(s284,plain,
( spl34_203
| ~ spl34_209 ),
inference(sat_conversion,[],[f1652]) ).
cnf(s285,plain,
( spl34_100
| ~ spl34_209 ),
inference(sat_conversion,[],[f1653]) ).
cnf(s286,plain,
( spl34_190
| ~ spl34_209 ),
inference(sat_conversion,[],[f1654]) ).
cnf(s287,plain,
( spl34_93
| ~ spl34_209 ),
inference(sat_conversion,[],[f1655]) ).
cnf(s288,plain,
( spl34_165
| ~ spl34_209 ),
inference(sat_conversion,[],[f1656]) ).
cnf(s289,plain,
( spl34_84
| ~ spl34_209 ),
inference(sat_conversion,[],[f1657]) ).
cnf(s290,plain,
( spl34_128
| ~ spl34_209 ),
inference(sat_conversion,[],[f1658]) ).
cnf(s291,plain,
( spl34_73
| ~ spl34_209 ),
inference(sat_conversion,[],[f1659]) ).
cnf(s292,plain,
( spl34_204
| ~ spl34_208 ),
inference(sat_conversion,[],[f1673]) ).
cnf(s293,plain,
( spl34_106
| ~ spl34_208 ),
inference(sat_conversion,[],[f1674]) ).
cnf(s296,plain,
( spl34_189
| ~ spl34_208 ),
inference(sat_conversion,[],[f1676]) ).
cnf(s297,plain,
( spl34_90
| ~ spl34_208 ),
inference(sat_conversion,[],[f1677]) ).
cnf(s298,plain,
( spl34_164
| ~ spl34_208 ),
inference(sat_conversion,[],[f1678]) ).
cnf(s299,plain,
( spl34_81
| ~ spl34_208 ),
inference(sat_conversion,[],[f1679]) ).
cnf(s329,plain,
( ~ spl34_91
| ~ spl34_137 ),
inference(sat_conversion,[],[f1747]) ).
cnf(s330,plain,
( ~ spl34_137
| ~ spl34_189 ),
inference(sat_conversion,[],[f1748]) ).
cnf(s345,plain,
( spl34_44
| ~ spl34_68
| ~ spl34_87 ),
inference(sat_conversion,[],[f1791]) ).
cnf(s348,plain,
( ~ spl34_129
| ~ spl34_188 ),
inference(sat_conversion,[],[f1803]) ).
cnf(s349,plain,
( ~ spl34_129
| ~ spl34_187 ),
inference(sat_conversion,[],[f1804]) ).
cnf(s350,plain,
( ~ spl34_79
| ~ spl34_129 ),
inference(sat_conversion,[],[f1805]) ).
cnf(s395,plain,
( ~ spl34_28
| ~ spl34_129
| spl34_139 ),
inference(sat_conversion,[],[f1927]) ).
cnf(s407,plain,
( ~ spl34_58
| ~ spl34_193
| spl34_201 ),
inference(sat_conversion,[],[f1962]) ).
cnf(s434,plain,
( ~ spl34_95
| ~ spl34_195 ),
inference(sat_conversion,[],[f2042]) ).
cnf(s468,plain,
( ~ spl34_81
| ~ spl34_134 ),
inference(sat_conversion,[],[f2100]) ).
cnf(s476,plain,
( ~ spl34_164
| ~ spl34_165 ),
inference(sat_conversion,[],[f2133]) ).
cnf(s507,plain,
( ~ spl34_101
| ~ spl34_203 ),
inference(sat_conversion,[],[f2230]) ).
cnf(s519,plain,
( ~ spl34_72
| ~ spl34_143 ),
inference(sat_conversion,[],[f2265]) ).
cnf(s536,plain,
( ~ spl34_74
| ~ spl34_128 ),
inference(sat_conversion,[],[f2298]) ).
cnf(s547,plain,
( ~ spl34_132
| ~ spl34_164 ),
inference(sat_conversion,[],[f2333]) ).
cnf(s553,plain,
( ~ spl34_143
| ~ spl34_174 ),
inference(sat_conversion,[],[f2343]) ).
cnf(s554,plain,
( ~ spl34_83
| ~ spl34_143 ),
inference(sat_conversion,[],[f2344]) ).
cnf(s555,plain,
( ~ spl34_146
| ~ spl34_172 ),
inference(sat_conversion,[],[f2354]) ).
cnf(s564,plain,
( ~ spl34_85
| ~ spl34_165 ),
inference(sat_conversion,[],[f2381]) ).
cnf(s567,plain,
( ~ spl34_105
| ~ spl34_178 ),
inference(sat_conversion,[],[f2390]) ).
cnf(s591,plain,
( ~ spl34_68
| ~ spl34_183 ),
inference(sat_conversion,[],[f2439]) ).
cnf(s602,plain,
( ~ spl34_143
| ~ spl34_173 ),
inference(sat_conversion,[],[f2442]) ).
cnf(s648,plain,
( ~ spl34_68
| ~ spl34_160 ),
inference(sat_conversion,[],[f2510]) ).
cnf(s652,plain,
( ~ spl34_89
| ~ spl34_190 ),
inference(sat_conversion,[],[f2521]) ).
cnf(s660,plain,
( ~ spl34_59
| spl34_101
| ~ spl34_204 ),
inference(sat_conversion,[],[f2558]) ).
cnf(s671,plain,
( ~ spl34_90
| ~ spl34_201 ),
inference(sat_conversion,[],[f2600]) ).
cnf(s687,plain,
( ~ spl34_192
| ~ spl34_203 ),
inference(sat_conversion,[],[f2610]) ).
cnf(s689,plain,
( ~ spl34_139
| ~ spl34_142 ),
inference(sat_conversion,[],[f2612]) ).
cnf(s771,plain,
( ~ spl34_66
| ~ spl34_129 ),
inference(sat_conversion,[],[f2773]) ).
cnf(s773,plain,
( ~ spl34_68
| spl34_129 ),
inference(sat_conversion,[],[f2774]) ).
cnf(s804,plain,
( ~ spl34_127
| ~ spl34_198 ),
inference(sat_conversion,[],[f2855]) ).
cnf(s844,plain,
( ~ spl34_68
| spl34_75 ),
inference(sat_conversion,[],[f2949]) ).
cnf(s862,plain,
( ~ spl34_68
| spl34_143 ),
inference(sat_conversion,[],[f2963]) ).
cnf(s872,plain,
( spl34_127
| ~ spl34_208 ),
inference(sat_conversion,[],[f2978]) ).
cnf(s873,plain,
( spl34_70
| ~ spl34_208 ),
inference(sat_conversion,[],[f2979]) ).
cnf(s882,plain,
( ~ spl34_94
| ~ spl34_138 ),
inference(sat_conversion,[],[f3012]) ).
cnf(s884,plain,
( ~ spl34_138
| ~ spl34_190 ),
inference(sat_conversion,[],[f3015]) ).
cnf(s894,plain,
( ~ spl34_133
| ~ spl34_186 ),
inference(sat_conversion,[],[f3040]) ).
cnf(s900,plain,
( ~ spl34_30
| ~ spl34_138
| spl34_154 ),
inference(sat_conversion,[],[f3042]) ).
cnf(s912,plain,
( ~ spl34_189
| ~ spl34_202 ),
inference(sat_conversion,[],[f3044]) ).
cnf(s922,plain,
( ~ spl34_136
| ~ spl34_143 ),
inference(sat_conversion,[],[f3068]) ).
cnf(s945,plain,
( ~ spl34_68
| ~ spl34_182 ),
inference(sat_conversion,[],[f3114]) ).
cnf(s949,plain,
( ~ spl34_168
| ~ spl34_189 ),
inference(sat_conversion,[],[f3116]) ).
cnf(s962,plain,
~ spl34_44,
inference(sat_conversion,[],[f3125]) ).
cnf(s967,plain,
( ~ spl34_64
| ~ spl34_70 ),
inference(sat_conversion,[],[f3126]) ).
cnf(s988,plain,
( ~ spl34_74
| ~ spl34_159 ),
inference(sat_conversion,[],[f3151]) ).
cnf(s1004,plain,
( ~ spl34_101
| ~ spl34_172 ),
inference(sat_conversion,[],[f3188]) ).
cnf(s1006,plain,
( ~ spl34_172
| ~ spl34_191 ),
inference(sat_conversion,[],[f3191]) ).
cnf(s1014,plain,
( ~ spl34_162
| ~ spl34_170 ),
inference(sat_conversion,[],[f3213]) ).
cnf(s1020,plain,
( ~ spl34_68
| ~ spl34_184 ),
inference(sat_conversion,[],[f3241]) ).
cnf(s1023,plain,
( ~ spl34_189
| ~ spl34_190 ),
inference(sat_conversion,[],[f3252]) ).
cnf(s1049,plain,
( ~ spl34_196
| ~ spl34_204 ),
inference(sat_conversion,[],[f3311]) ).
cnf(s1054,plain,
( ~ spl34_70
| ~ spl34_73 ),
inference(sat_conversion,[],[f3347]) ).
cnf(s1058,plain,
( ~ spl34_69
| ~ spl34_75 ),
inference(sat_conversion,[],[f3372]) ).
cnf(s1087,plain,
( ~ spl34_75
| ~ spl34_153 ),
inference(sat_conversion,[],[f3385]) ).
cnf(s1100,plain,
( ~ spl34_138
| ~ spl34_167 ),
inference(sat_conversion,[],[f3392]) ).
cnf(s1189,plain,
( ~ spl34_86
| ~ spl34_178 ),
inference(sat_conversion,[],[f3531]) ).
cnf(s1193,plain,
( ~ spl34_90
| ~ spl34_93 ),
inference(sat_conversion,[],[f3549]) ).
cnf(s1205,plain,
( ~ spl34_99
| ~ spl34_100 ),
inference(sat_conversion,[],[f3603]) ).
cnf(s1208,plain,
( ~ spl34_104
| ~ spl34_106 ),
inference(sat_conversion,[],[f3623]) ).
cnf(s1212,plain,
( ~ spl34_108
| spl34_134
| ~ spl34_143 ),
inference(sat_conversion,[],[f3643]) ).
cnf(s1222,plain,
( spl34_124
| ~ spl34_170
| ~ spl34_178 ),
inference(sat_conversion,[],[f3665]) ).
cnf(s1223,plain,
( ~ spl34_75
| ~ spl34_154 ),
inference(sat_conversion,[],[f3666]) ).
cnf(s1224,plain,
( ~ spl34_78
| ~ spl34_81 ),
inference(sat_conversion,[],[f3667]) ).
cnf(s1228,plain,
( ~ spl34_121
| ~ spl34_135
| spl34_159 ),
inference(sat_conversion,[],[f3680]) ).
cnf(s1229,plain,
( ~ spl34_68
| ~ spl34_87 ),
inference(rat,[],[s345,s962]) ).
cnf(s1230,plain,
~ spl34_184,
inference(rat,[],[s1020,s136]) ).
cnf(s1231,plain,
~ spl34_182,
inference(rat,[],[s945,s136]) ).
cnf(s1232,plain,
spl34_143,
inference(rat,[],[s862,s136]) ).
cnf(s1233,plain,
spl34_75,
inference(rat,[],[s844,s136]) ).
cnf(s1234,plain,
spl34_129,
inference(rat,[],[s773,s136]) ).
cnf(s1235,plain,
~ spl34_160,
inference(rat,[],[s648,s136]) ).
cnf(s1236,plain,
~ spl34_183,
inference(rat,[],[s591,s136]) ).
cnf(s1238,plain,
~ spl34_87,
inference(rat,[],[s1229,s136]) ).
cnf(s1239,plain,
~ spl34_126,
inference(rat,[],[s249,s136]) ).
cnf(s1241,plain,
~ spl34_136,
inference(rat,[],[s922,s1232]) ).
cnf(s1244,plain,
~ spl34_173,
inference(rat,[],[s602,s1232]) ).
cnf(s1245,plain,
~ spl34_83,
inference(rat,[],[s554,s1232]) ).
cnf(s1246,plain,
~ spl34_174,
inference(rat,[],[s553,s1232]) ).
cnf(s1248,plain,
~ spl34_72,
inference(rat,[],[s519,s1232]) ).
cnf(s1249,plain,
~ spl34_154,
inference(rat,[],[s1223,s1233]) ).
cnf(s1250,plain,
~ spl34_153,
inference(rat,[],[s1087,s1233]) ).
cnf(s1251,plain,
~ spl34_69,
inference(rat,[],[s1058,s1233]) ).
cnf(s1254,plain,
~ spl34_66,
inference(rat,[],[s771,s1234]) ).
cnf(s1257,plain,
~ spl34_79,
inference(rat,[],[s350,s1234]) ).
cnf(s1258,plain,
~ spl34_187,
inference(rat,[],[s349,s1234]) ).
cnf(s1259,plain,
~ spl34_188,
inference(rat,[],[s348,s1234]) ).
cnf(s1260,plain,
~ spl34_205,
inference(rat,[],[s217,s1238]) ).
cnf(s1261,plain,
~ spl34_207,
inference(rat,[],[s272,s1239]) ).
cnf(s1262,plain,
~ spl34_206,
inference(rat,[],[s276,s1246]) ).
cnf(s1263,plain,
~ spl34_17,
inference(rat,[],[s93,s1245]) ).
cnf(s1264,plain,
~ spl34_16,
inference(rat,[],[s90,s1248]) ).
cnf(s1265,plain,
~ spl34_12,
inference(rat,[],[s79,s1257]) ).
cnf(s1266,plain,
~ spl34_11,
inference(rat,[],[s75,s1251]) ).
cnf(s1267,plain,
~ spl34_9,
inference(rat,[],[s70,s1245]) ).
cnf(s1268,plain,
~ spl34_8,
inference(rat,[],[s66,s1257]) ).
cnf(s1269,plain,
~ spl34_6,
inference(rat,[],[s60,s1254]) ).
cnf(s1270,plain,
~ spl34_4,
inference(rat,[],[s55,s1248]) ).
cnf(s1271,plain,
~ spl34_3,
inference(rat,[],[s52,s1251]) ).
cnf(s1272,plain,
~ spl34_2,
inference(rat,[],[s49,s1254]) ).
cnf(s1277,plain,
( spl34_1
| spl34_5
| spl34_7
| spl34_10
| spl34_13
| spl34_14
| spl34_15
| spl34_18
| spl34_19
| spl34_20
| spl34_21
| spl34_22
| spl34_23
| spl34_24
| spl34_25 ),
inference(rat,[],[s3,s1263,s1264,s1265,s1266,s1267,s1268,s1269,s1270,s1271,s1272]) ).
cnf(s1279,plain,
( spl34_1
| spl34_5
| spl34_7
| spl34_10
| spl34_13
| spl34_14
| spl34_15
| spl34_18
| spl34_19
| spl34_20
| spl34_21
| spl34_22
| spl34_23
| spl34_24
| ~ spl34_25 ),
inference(rat,[],[s1,s1263,s1264,s1265,s1266,s1267,s1268,s1269,s1270,s1271,s1272]) ).
cnf(s1280,plain,
( spl34_24
| spl34_23
| spl34_1
| spl34_5
| spl34_7
| spl34_10
| spl34_13
| spl34_14
| spl34_15
| spl34_18
| spl34_19
| spl34_20
| spl34_21
| spl34_22 ),
inference(rat,[],[s1279,s1277]) ).
cnf(s1281,plain,
~ spl34_24,
inference(rat,[],[s187,s284,s293,s507,s113,s115,s1261,s1260,s1262]) ).
cnf(s1282,plain,
~ spl34_23,
inference(rat,[],[s201,s687,s1193,s284,s287,s187,s296,s330,s141,s434,s882,s111,s112,s1258,s1236,s1261,s1260,s1262,s1241,s1238,s1251]) ).
cnf(s1283,plain,
~ spl34_22,
inference(rat,[],[s195,s949,s1224,s296,s299,s187,s288,s1189,s564,s108,s109,s1235,s1244,s1261,s1260,s1262]) ).
cnf(s1284,plain,
( spl34_56
| spl34_59
| spl34_58
| spl34_57 ),
inference(rat,[],[s36,s40]) ).
cnf(s1285,plain,
~ spl34_74,
inference(rat,[],[s1284,s135,s132,s1222,s1228,s181,s140,s689,s894,s189,s660,s210,s555,s1004,s1006,s209,s882,s1100,s567,s407,s141,s195,s202,s1049,s1208,s330,s912,s949,s1023,s671,s1193,s476,s547,s468,s1224,s967,s292,s293,s296,s297,s298,s299,s873,s187,s290,s536,s988,s1254,s1250,s1231,s1241,s1238,s1251,s1235,s1244,s1230,s1259,s1261,s1260,s1262]) ).
cnf(s1286,plain,
~ spl34_21,
inference(rat,[],[s106,s1285]) ).
cnf(s1287,plain,
~ spl34_26,
inference(rat,[],[s116,s117]) ).
cnf(s1288,plain,
( ~ spl34_100
| spl34_18
| spl34_15
| spl34_14
| spl34_13
| spl34_10
| spl34_7
| spl34_5
| spl34_1 ),
inference(rat,[],[s1280,s100,s101,s1205,s1281,s1283,s1286,s1282]) ).
cnf(s1290,plain,
~ spl34_208,
inference(rat,[],[s689,s395,s181,s6,s1014,s882,s900,s118,s177,s804,s141,s1212,s330,s912,s1193,s468,s226,s1054,s296,s297,s299,s872,s873,s1234,s1287,s1249,s1285,s1230,s1241,s1238,s1251,s1232]) ).
cnf(s1291,plain,
spl34_209,
inference(rat,[],[s187,s1262,s1260,s1261,s1290]) ).
cnf(s1292,plain,
spl34_73,
inference(rat,[],[s291,s1291]) ).
cnf(s1294,plain,
spl34_84,
inference(rat,[],[s289,s1291]) ).
cnf(s1296,plain,
spl34_93,
inference(rat,[],[s287,s1291]) ).
cnf(s1297,plain,
spl34_190,
inference(rat,[],[s286,s1291]) ).
cnf(s1298,plain,
spl34_100,
inference(rat,[],[s285,s1291]) ).
cnf(s1302,plain,
~ spl34_63,
inference(rat,[],[s237,s1292]) ).
cnf(s1321,plain,
~ spl34_138,
inference(rat,[],[s884,s1297]) ).
cnf(s1323,plain,
~ spl34_89,
inference(rat,[],[s652,s1297]) ).
cnf(s1337,plain,
spl34_137,
inference(rat,[],[s141,s1251,s1238,s1241,s1321]) ).
cnf(s1343,plain,
~ spl34_91,
inference(rat,[],[s329,s1337]) ).
cnf(s1344,plain,
~ spl34_15,
inference(rat,[],[s86,s1296]) ).
cnf(s1349,plain,
~ spl34_18,
inference(rat,[],[s97,s1343]) ).
cnf(s1350,plain,
~ spl34_14,
inference(rat,[],[s84,s1343]) ).
cnf(s1351,plain,
~ spl34_13,
inference(rat,[],[s82,s1323]) ).
cnf(s1352,plain,
~ spl34_10,
inference(rat,[],[s71,s1294]) ).
cnf(s1353,plain,
~ spl34_7,
inference(rat,[],[s62,s64]) ).
cnf(s1354,plain,
~ spl34_5,
inference(rat,[],[s57,s1285]) ).
cnf(s1355,plain,
spl34_1,
inference(rat,[],[s1288,s1350,s1354,s1349,s1352,s1351,s1298,s1344,s1353]) ).
cnf(s1356,plain,
$false,
inference(rat,[],[s45,s1302,s1355]) ).
fof(f3681,plain,
$false,
inference(avatar_sat_refutation,[],[s1356]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG056+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n001.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 19:27:19 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.23 Running first-order theorem proving
% 0.07/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.65/1.40 % (649086)Detected formulas, will run a generic FOF schedule.
% 4.65/1.40 % (649095)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3425599601:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.65/1.40 % (649095)Instruction limit reached!
% 4.65/1.40 % (649095)------------------------------
% 4.65/1.40 % (649095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.65/1.40 % (649095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.65/1.40 % (649095)CaDiCaL version: 2.1.3
% 4.65/1.40 % (649095)Termination reason: Instruction limit
% 4.65/1.40 % (649095)Termination phase: Saturation
% 4.65/1.40 % (649095)Time elapsed: 0.031 s
% 4.65/1.40 % (649095)Peak memory usage: 88 MB
% 4.65/1.40 % (649095)Instructions burned: 121 (million)
% 4.65/1.40 % (649096)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4207590898:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.65/1.40 % (649094)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1718042739:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.65/1.40 % (649092)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=499389906:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.65/1.40 % (649091)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=4227134294:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.65/1.40 % (649093)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2485017614:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.65/1.40 % (649097)dis-21_1_sil=8000:lcm=predicate:random_seed=2569845366:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 4.65/1.40 % (649094)Refutation not found, incomplete strategy
% 4.65/1.40 % (649094)------------------------------
% 4.65/1.40 % (649094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.65/1.40 % (649094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.65/1.40 % (649094)CaDiCaL version: 2.1.3
% 4.65/1.40 % (649094)Termination reason: Refutation not found, incomplete strategy
% 4.65/1.40 % (649094)Time elapsed: 0.018 s
% 4.65/1.40 % (649094)Peak memory usage: 89 MB
% 4.65/1.40 % (649094)Instructions burned: 37 (million)
% 4.65/1.40 % (649097)Refutation not found, incomplete strategy
% 4.65/1.40 % (649097)------------------------------
% 4.65/1.40 % (649097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.65/1.40 % (649097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.65/1.40 % (649097)CaDiCaL version: 2.1.3
% 4.65/1.40 % (649097)Termination reason: Refutation not found, incomplete strategy
% 4.65/1.40 % (649097)Time elapsed: 0.014 s
% 4.65/1.40 % (649097)Peak memory usage: 89 MB
% 4.65/1.40 % (649097)Instructions burned: 25 (million)
% 4.65/1.40 % (649096)Instruction limit reached!
% 4.65/1.40 % (649096)------------------------------
% 4.65/1.40 % (649096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.65/1.40 % (649096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.65/1.40 % (649096)CaDiCaL version: 2.1.3
% 4.65/1.40 % (649096)Termination reason: Instruction limit
% 4.65/1.40 % (649096)Termination phase: Saturation
% 4.65/1.40 % (649096)Time elapsed: 0.079 s
% 4.65/1.40 % (649096)Peak memory usage: 89 MB
% 4.65/1.40 % (649096)Instructions burned: 141 (million)
% 4.65/1.40 % (649099)lrs+10_1_sil=8000:sp=occurrence:random_seed=1580099896:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 4.65/1.40 % (649099)Instruction limit reached!
% 4.65/1.40 % (649099)------------------------------
% 4.65/1.40 % (649099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.65/1.40 % (649099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.65/1.40 % (649099)CaDiCaL version: 2.1.3
% 4.65/1.40 % (649099)Termination reason: Instruction limit
% 4.65/1.40 % (649099)Termination phase: Saturation
% 4.65/1.40 % (649099)Time elapsed: 0.083 s
% 4.65/1.40 % (649099)Peak memory usage: 90 MB
% 4.65/1.40 % (649099)Instructions burned: 287 (million)
% 4.65/1.40 % (649106)lrs+10_1_sil=32000:urr=on:br=off:random_seed=258402405:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 6.03/1.65 % (649094)------------------------------
% 6.03/1.65 % (649094)------------------------------
% 6.03/1.65 % (649097)------------------------------
% 6.03/1.65 % (649097)------------------------------
% 6.03/1.65 % (649108)lrs+1011_1_sil=32000:sp=occurrence:random_seed=900959493:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 6.03/1.65 % (649106)Instruction limit reached!
% 6.03/1.65 % (649106)------------------------------
% 6.03/1.65 % (649106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.03/1.65 % (649106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.03/1.65 % (649106)CaDiCaL version: 2.1.3
% 6.03/1.65 % (649106)Termination reason: Instruction limit
% 6.03/1.65 % (649106)Termination phase: Saturation
% 6.03/1.65 % (649106)Time elapsed: 0.087 s
% 6.03/1.65 % (649106)Peak memory usage: 90 MB
% 6.03/1.65 % (649106)Instructions burned: 158 (million)
% 6.03/1.65 [W928 19:27:20.344719310 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.03/1.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.03/1.65 [W928 19:27:20.344767827 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.03/1.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.03/1.65 [W928 19:27:20.344806051 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.03/1.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.03/1.65 [W928 19:27:20.344817021 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.03/1.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.03/1.65 [W928 19:27:20.344843841 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.03/1.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.03/1.65 [W928 19:27:20.344854934 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.03/1.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.03/1.65 [W928 19:27:20.345224440 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.03/1.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.03/1.65 [W928 19:27:20.345252141 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.03/1.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.03/1.65 [W928 19:27:20.345290831 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.03/1.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.03/1.65 [W928 19:27:20.345303424 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.03/1.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.03/1.65 [W928 19:27:20.345329484 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.03/1.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.03/1.65 [W928 19:27:20.345341251 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.03/1.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.03/1.65 [W928 19:27:20.345955739 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.03/1.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.03/1.65 [W928 19:27:20.345990116 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.03/1.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.03/1.65 [W928 19:27:20.346035346 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.03/1.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.03/1.65 [W928 19:27:20.346049990 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.03/1.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.03/1.65 [W928 19:27:20.346076347 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.03/1.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.03/1.65 [W928 19:27:20.346087413 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.03/1.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.03/1.65 % (649108)Instruction limit reached!
% 6.03/1.65 % (649108)------------------------------
% 6.03/1.65 % (649108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.03/1.65 % (649108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.03/1.65 % (649108)CaDiCaL version: 2.1.3
% 6.03/1.65 % (649108)Termination reason: Instruction limit
% 6.03/1.65 % (649108)Termination phase: Saturation
% 6.03/1.65 % (649108)Time elapsed: 0.097 s
% 6.03/1.65 % (649108)Peak memory usage: 90 MB
% 6.03/1.65 % (649108)Instructions burned: 328 (million)
% 6.03/1.65 % (649110)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1895996634:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 6.03/1.65 % (649111)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2489433608:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 6.03/1.65 % (649111)Refutation not found, incomplete strategy
% 6.03/1.65 % (649111)------------------------------
% 6.03/1.65 % (649111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.03/1.65 % (649111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.03/1.65 % (649111)CaDiCaL version: 2.1.3
% 6.03/1.65 % (649111)Termination reason: Refutation not found, incomplete strategy
% 6.03/1.65 % (649111)Time elapsed: 0.015 s
% 6.03/1.65 % (649111)Peak memory usage: 89 MB
% 6.03/1.65 % (649111)Instructions burned: 32 (million)
% 6.03/1.65 % (649113)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=562842530:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 6.03/1.65 % (649110)First to succeed.
% 6.03/1.65 % (649110)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-649086"
% 6.03/1.65 % (649114)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=773959551:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 6.03/1.65 % (649114)Instruction limit reached!
% 6.03/1.65 % (649114)------------------------------
% 6.03/1.65 % (649114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.03/1.65 % (649114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.03/1.65 % (649114)CaDiCaL version: 2.1.3
% 6.03/1.65 % (649114)Termination reason: Instruction limit
% 6.03/1.65 % (649114)Termination phase: Saturation
% 6.03/1.65 % (649114)Time elapsed: 0.032 s
% 6.03/1.65 % (649114)Peak memory usage: 90 MB
% 6.03/1.65 % (649114)Instructions burned: 116 (million)
% 6.03/1.65 % (649111)------------------------------
% 6.03/1.65 % (649111)------------------------------
% 6.03/1.65 % (649119)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=932227863:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 6.03/1.65 % (649092)Also succeeded, but the first one will report.
% 6.03/1.65 % (649119)Instruction limit reached!
% 6.03/1.65 % (649119)------------------------------
% 6.03/1.65 % (649119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.03/1.65 % (649119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.03/1.65 % (649119)CaDiCaL version: 2.1.3
% 6.03/1.65 % (649119)Termination reason: Instruction limit
% 6.03/1.65 % (649119)Termination phase: Saturation
% 6.03/1.65 % (649119)Time elapsed: 0.029 s
% 6.03/1.65 % (649119)Peak memory usage: 88 MB
% 6.03/1.65 % (649119)Instructions burned: 127 (million)
% 6.03/1.65 % (649110)Refutation found. Thanks to Tanya!
% 6.03/1.65 % SZS status Theorem for theBenchmark
% 6.03/1.65 % SZS output start Proof for theBenchmark
% See solution above
% 7.42/1.85 % (649110)------------------------------
% 7.42/1.85 % (649110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.42/1.85 % (649110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.85 % (649110)CaDiCaL version: 2.1.3
% 7.42/1.85 % (649110)Termination reason: Refutation
% 7.42/1.85 % (649110)Time elapsed: 0.087 s
% 7.42/1.85 % (649110)Peak memory usage: 91 MB
% 7.42/1.85 % (649110)Instructions burned: 151 (million)
% 7.42/1.85 % (649110)------------------------------
% 7.42/1.85 % (649110)------------------------------
% 7.42/1.85 % (649086)Success in time 0.967 s
% 7.42/1.85 % Vampire exiting
%------------------------------------------------------------------------------