%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG054+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:21:00 AM UTC 2026
% Result : Theorem 0.07s 0.27s
% Output : Refutation 0.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 53
% Syntax : Number of formulae : 408 ( 51 unt; 47 def)
% Number of atoms : 1563 ( 849 equ)
% Maximal formula atoms : 250 ( 3 avg)
% Number of connectives : 1712 ( 557 ~; 926 |; 182 &)
% ( 47 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 54 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 49 ( 47 usr; 48 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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',ax3) ).
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/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( e0 = op(e1,op(op(e1,e1),op(e1,e1)))
& e2 = op(op(e1,e1),op(e1,e1))
& e3 = op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1)))
& e4 = op(e1,e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
fof(f7,conjecture,
~ ( ( op(e0,e0) = e0
| op(e1,e1) = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e0) = e1
| op(e1,e1) = e1
| op(e2,e2) = e1
| op(e3,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e0) = e2
| op(e1,e1) = e2
| op(e2,e2) = e2
| op(e3,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e0) = e3
| op(e1,e1) = e3
| op(e2,e2) = e3
| op(e3,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e0) = e4
| op(e1,e1) = e4
| op(e2,e2) = e4
| op(e3,e3) = e4
| op(e4,e4) = e4 )
& ( op(e0,e0) != e0
| op(e0,e0) = e0 )
& ( op(e0,e0) != e1
| op(e0,e1) = e0 )
& ( op(e0,e0) != e2
| op(e0,e2) = e0 )
& ( op(e0,e0) != e3
| op(e0,e3) = e0 )
& ( op(e0,e0) != e4
| op(e0,e4) = e0 )
& ( op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e1,e1) != e1
| op(e1,e1) = e1 )
& ( op(e1,e1) != e2
| op(e1,e2) = e1 )
& ( op(e1,e1) != e3
| op(e1,e3) = e1 )
& ( op(e1,e1) != e4
| op(e1,e4) = e1 )
& ( op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e2,e2) != e2
| op(e2,e2) = e2 )
& ( op(e2,e2) != e3
| op(e2,e3) = e2 )
& ( op(e2,e2) != e4
| op(e2,e4) = e2 )
& ( op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e3,e3) != e1
| op(e3,e1) = e3 )
& ( op(e3,e3) != e2
| op(e3,e2) = e3 )
& ( op(e3,e3) != e3
| op(e3,e3) = e3 )
& ( op(e3,e3) != e4
| op(e3,e4) = e3 )
& ( op(e4,e4) != e0
| op(e4,e0) = e4 )
& ( op(e4,e4) != e1
| op(e4,e1) = e4 )
& ( op(e4,e4) != e2
| op(e4,e2) = e4 )
& ( op(e4,e4) != e3
| op(e4,e3) = e4 )
& ( op(e4,e4) != e4
| op(e4,e4) = e4 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f8,negated_conjecture,
~ ~ ( ( op(e0,e0) = e0
| op(e1,e1) = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e0) = e1
| op(e1,e1) = e1
| op(e2,e2) = e1
| op(e3,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e0) = e2
| op(e1,e1) = e2
| op(e2,e2) = e2
| op(e3,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e0) = e3
| op(e1,e1) = e3
| op(e2,e2) = e3
| op(e3,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e0) = e4
| op(e1,e1) = e4
| op(e2,e2) = e4
| op(e3,e3) = e4
| op(e4,e4) = e4 )
& ( op(e0,e0) != e0
| op(e0,e0) = e0 )
& ( op(e0,e0) != e1
| op(e0,e1) = e0 )
& ( op(e0,e0) != e2
| op(e0,e2) = e0 )
& ( op(e0,e0) != e3
| op(e0,e3) = e0 )
& ( op(e0,e0) != e4
| op(e0,e4) = e0 )
& ( op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e1,e1) != e1
| op(e1,e1) = e1 )
& ( op(e1,e1) != e2
| op(e1,e2) = e1 )
& ( op(e1,e1) != e3
| op(e1,e3) = e1 )
& ( op(e1,e1) != e4
| op(e1,e4) = e1 )
& ( op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e2,e2) != e2
| op(e2,e2) = e2 )
& ( op(e2,e2) != e3
| op(e2,e3) = e2 )
& ( op(e2,e2) != e4
| op(e2,e4) = e2 )
& ( op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e3,e3) != e1
| op(e3,e1) = e3 )
& ( op(e3,e3) != e2
| op(e3,e2) = e3 )
& ( op(e3,e3) != e3
| op(e3,e3) = e3 )
& ( op(e3,e3) != e4
| op(e3,e4) = e3 )
& ( op(e4,e4) != e0
| op(e4,e0) = e4 )
& ( op(e4,e4) != e1
| op(e4,e1) = e4 )
& ( op(e4,e4) != e2
| op(e4,e2) = e4 )
& ( op(e4,e4) != e3
| op(e4,e3) = e4 )
& ( op(e4,e4) != e4
| op(e4,e4) = e4 ) ),
inference(negated_conjecture,[status(cth)],[f7]) ).
fof(f9,plain,
( ( op(e0,e0) = e0
| op(e1,e1) = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e0) = e1
| op(e1,e1) = e1
| op(e2,e2) = e1
| op(e3,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e0) = e2
| op(e1,e1) = e2
| op(e2,e2) = e2
| op(e3,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e0) = e3
| op(e1,e1) = e3
| op(e2,e2) = e3
| op(e3,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e0) = e4
| op(e1,e1) = e4
| op(e2,e2) = e4
| op(e3,e3) = e4
| op(e4,e4) = e4 )
& ( op(e0,e0) != e0
| op(e0,e0) = e0 )
& ( op(e0,e0) != e1
| op(e0,e1) = e0 )
& ( op(e0,e0) != e2
| op(e0,e2) = e0 )
& ( op(e0,e0) != e3
| op(e0,e3) = e0 )
& ( op(e0,e0) != e4
| op(e0,e4) = e0 )
& ( op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e1,e1) != e1
| op(e1,e1) = e1 )
& ( op(e1,e1) != e2
| op(e1,e2) = e1 )
& ( op(e1,e1) != e3
| op(e1,e3) = e1 )
& ( op(e1,e1) != e4
| op(e1,e4) = e1 )
& ( op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e2,e2) != e2
| op(e2,e2) = e2 )
& ( op(e2,e2) != e3
| op(e2,e3) = e2 )
& ( op(e2,e2) != e4
| op(e2,e4) = e2 )
& ( op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e3,e3) != e1
| op(e3,e1) = e3 )
& ( op(e3,e3) != e2
| op(e3,e2) = e3 )
& ( op(e3,e3) != e3
| op(e3,e3) = e3 )
& ( op(e3,e3) != e4
| op(e3,e4) = e3 )
& ( op(e4,e4) != e0
| op(e4,e0) = e4 )
& ( op(e4,e4) != e1
| op(e4,e1) = e4 )
& ( op(e4,e4) != e2
| op(e4,e2) = e4 )
& ( op(e4,e4) != e3
| op(e4,e3) = e4 )
& ( op(e4,e4) != e4
| op(e4,e4) = e4 ) ),
inference(flattening,[],[f8]) ).
fof(f10,plain,
( op(e0,e0) = e4
| op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| e0 = op(e0,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f35,plain,
( e4 = unit
| e3 = unit
| e2 = unit
| e1 = unit
| e0 = unit ),
inference(cnf_transformation,[],[f2]) ).
fof(f37,plain,
e4 = op(unit,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f39,plain,
e3 = op(unit,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f41,plain,
e2 = op(unit,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f42,plain,
e1 = op(e1,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f43,plain,
e1 = op(unit,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f60,plain,
( e2 = op(e1,e4)
| e2 = op(e1,e3)
| e2 = op(e1,e2)
| e2 = op(e1,e1)
| e2 = op(e1,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f62,plain,
( e3 = op(e1,e4)
| e3 = op(e1,e3)
| e3 = op(e1,e2)
| e3 = op(e1,e1)
| e3 = op(e1,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f196,plain,
e3 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f197,plain,
e2 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f198,plain,
e2 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f199,plain,
e1 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f200,plain,
e1 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f201,plain,
e1 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f202,plain,
e0 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f203,plain,
e0 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f204,plain,
e0 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f205,plain,
e0 != e1,
inference(cnf_transformation,[],[f5]) ).
fof(f206,plain,
e4 = op(e1,e1),
inference(cnf_transformation,[],[f6]) ).
fof(f208,plain,
e2 = op(op(e1,e1),op(e1,e1)),
inference(cnf_transformation,[],[f6]) ).
fof(f209,plain,
e0 = op(e1,op(op(e1,e1),op(e1,e1))),
inference(cnf_transformation,[],[f6]) ).
fof(f210,plain,
( e0 = op(e4,e4)
| e0 = op(e3,e3)
| e0 = op(e2,e2)
| e0 = op(e1,e1)
| e0 = op(e0,e0) ),
inference(cnf_transformation,[],[f9]) ).
fof(f211,plain,
( e1 = op(e4,e4)
| e1 = op(e3,e3)
| e1 = op(e2,e2)
| e1 = op(e1,e1)
| op(e0,e0) = e1 ),
inference(cnf_transformation,[],[f9]) ).
fof(f212,plain,
( e2 = op(e4,e4)
| e2 = op(e3,e3)
| e2 = op(e2,e2)
| e2 = op(e1,e1)
| op(e0,e0) = e2 ),
inference(cnf_transformation,[],[f9]) ).
fof(f213,plain,
( e3 = op(e4,e4)
| e3 = op(e3,e3)
| e3 = op(e2,e2)
| e3 = op(e1,e1)
| op(e0,e0) = e3 ),
inference(cnf_transformation,[],[f9]) ).
fof(f215,plain,
( e0 = op(e0,e1)
| op(e0,e0) != e1 ),
inference(cnf_transformation,[],[f9]) ).
fof(f216,plain,
( e0 = op(e0,e2)
| op(e0,e0) != e2 ),
inference(cnf_transformation,[],[f9]) ).
fof(f217,plain,
( e0 = op(e0,e3)
| op(e0,e0) != e3 ),
inference(cnf_transformation,[],[f9]) ).
fof(f218,plain,
( e0 = op(e0,e4)
| op(e0,e0) != e4 ),
inference(cnf_transformation,[],[f9]) ).
fof(f220,plain,
( e1 = op(e1,e2)
| e2 != op(e1,e1) ),
inference(cnf_transformation,[],[f9]) ).
fof(f222,plain,
( e1 = op(e1,e4)
| e4 != op(e1,e1) ),
inference(cnf_transformation,[],[f9]) ).
fof(f236,definition,
( spl0_1
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f238,plain,
( e0 = op(e0,e0)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f236]) ).
fof(f240,definition,
( spl0_2
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f242,plain,
( e0 = op(e1,e1)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f240]) ).
fof(f244,definition,
( spl0_3
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f246,plain,
( e0 = op(e2,e2)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f244]) ).
fof(f248,definition,
( spl0_4
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f250,plain,
( e0 = op(e3,e3)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f252,definition,
( spl0_5
<=> e0 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f254,plain,
( e0 = op(e4,e4)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f252]) ).
fof(f255,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4
| spl0_5 ),
inference(avatar_split_clause,[],[f210,f252,f248,f244,f240,f236]) ).
fof(f257,definition,
( spl0_6
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f259,plain,
( op(e0,e0) = e1
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f261,definition,
( spl0_7
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f263,plain,
( e1 = op(e1,e1)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f265,definition,
( spl0_8
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f267,plain,
( e1 = op(e2,e2)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f269,definition,
( spl0_9
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f271,plain,
( e1 = op(e3,e3)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f269]) ).
fof(f273,definition,
( spl0_10
<=> e1 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f275,plain,
( e1 = op(e4,e4)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f273]) ).
fof(f276,plain,
( spl0_6
| spl0_7
| spl0_8
| spl0_9
| spl0_10 ),
inference(avatar_split_clause,[],[f211,f273,f269,f265,f261,f257]) ).
fof(f278,definition,
( spl0_11
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f280,plain,
( op(e0,e0) = e2
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f278]) ).
fof(f282,definition,
( spl0_12
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f286,definition,
( spl0_13
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f288,plain,
( e2 = op(e2,e2)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f286]) ).
fof(f290,definition,
( spl0_14
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f292,plain,
( e2 = op(e3,e3)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f294,definition,
( spl0_15
<=> e2 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f296,plain,
( e2 = op(e4,e4)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f294]) ).
fof(f297,plain,
( spl0_11
| spl0_12
| spl0_13
| spl0_14
| spl0_15 ),
inference(avatar_split_clause,[],[f212,f294,f290,f286,f282,f278]) ).
fof(f299,definition,
( spl0_16
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f301,plain,
( op(e0,e0) = e3
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f299]) ).
fof(f303,definition,
( spl0_17
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f305,plain,
( e3 = op(e1,e1)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f303]) ).
fof(f307,definition,
( spl0_18
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f309,plain,
( e3 = op(e2,e2)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f307]) ).
fof(f311,definition,
( spl0_19
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f313,plain,
( e3 = op(e3,e3)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f311]) ).
fof(f315,definition,
( spl0_20
<=> e3 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f317,plain,
( e3 = op(e4,e4)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f318,plain,
( spl0_16
| spl0_17
| spl0_18
| spl0_19
| spl0_20 ),
inference(avatar_split_clause,[],[f213,f315,f311,f307,f303,f299]) ).
fof(f320,definition,
( spl0_21
<=> op(e0,e0) = e4 ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f324,definition,
( spl0_22
<=> e4 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f326,plain,
( e4 = op(e1,e1)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f324]) ).
fof(f336,definition,
( spl0_25
<=> e4 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f337,plain,
( e4 != op(e4,e4)
| spl0_25 ),
inference(avatar_component_clause,[],[f336]) ).
fof(f338,plain,
( e4 = op(e4,e4)
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f336]) ).
fof(f341,definition,
( spl0_26
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f343,plain,
( e0 = op(e0,e1)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f341]) ).
fof(f344,plain,
( ~ spl0_6
| spl0_26 ),
inference(avatar_split_clause,[],[f215,f341,f257]) ).
fof(f346,definition,
( spl0_27
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f348,plain,
( e0 = op(e0,e2)
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f346]) ).
fof(f349,plain,
( ~ spl0_11
| spl0_27 ),
inference(avatar_split_clause,[],[f216,f346,f278]) ).
fof(f351,definition,
( spl0_28
<=> e0 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f353,plain,
( e0 = op(e0,e3)
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f351]) ).
fof(f354,plain,
( ~ spl0_16
| spl0_28 ),
inference(avatar_split_clause,[],[f217,f351,f299]) ).
fof(f356,definition,
( spl0_29
<=> e0 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f358,plain,
( e0 = op(e0,e4)
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f359,plain,
( ~ spl0_21
| spl0_29 ),
inference(avatar_split_clause,[],[f218,f356,f320]) ).
fof(f361,definition,
( spl0_30
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f362,plain,
( e1 != op(e1,e0)
| spl0_30 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f363,plain,
( e1 = op(e1,e0)
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f366,definition,
( spl0_31
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f367,plain,
( e1 != op(e1,e2)
| spl0_31 ),
inference(avatar_component_clause,[],[f366]) ).
fof(f368,plain,
( e1 = op(e1,e2)
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f366]) ).
fof(f369,plain,
( ~ spl0_12
| spl0_31 ),
inference(avatar_split_clause,[],[f220,f366,f282]) ).
fof(f371,definition,
( spl0_32
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f372,plain,
( e1 != op(e1,e3)
| spl0_32 ),
inference(avatar_component_clause,[],[f371]) ).
fof(f373,plain,
( e1 = op(e1,e3)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f371]) ).
fof(f376,definition,
( spl0_33
<=> e1 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f378,plain,
( e1 = op(e1,e4)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f376]) ).
fof(f379,plain,
( ~ spl0_22
| spl0_33 ),
inference(avatar_split_clause,[],[f222,f376,f324]) ).
fof(f440,plain,
spl0_22,
inference(avatar_split_clause,[],[f206,f324]) ).
fof(f441,plain,
e0 = op(e1,e2),
inference(forward_demodulation,[],[f209,f208]) ).
fof(f461,definition,
( spl0_50
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f462,plain,
( e1 != op(e0,e1)
| spl0_50 ),
inference(avatar_component_clause,[],[f461]) ).
fof(f463,plain,
( e1 = op(e0,e1)
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f461]) ).
fof(f495,definition,
( spl0_58
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f496,plain,
( e2 != op(e0,e2)
| spl0_58 ),
inference(avatar_component_clause,[],[f495]) ).
fof(f497,plain,
( e2 = op(e0,e2)
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f495]) ).
fof(f508,definition,
( spl0_61
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f510,plain,
( e2 = op(e1,e0)
| ~ spl0_61 ),
inference(avatar_component_clause,[],[f508]) ).
fof(f538,definition,
( spl0_68
<=> e3 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f540,plain,
( e3 = op(e1,e0)
| ~ spl0_68 ),
inference(avatar_component_clause,[],[f538]) ).
fof(f581,definition,
( spl0_78
<=> e0 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f583,plain,
( e0 = op(e1,e2)
| ~ spl0_78 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f621,definition,
( spl0_87
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f623,plain,
( e2 = op(e1,e2)
| ~ spl0_87 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f625,definition,
( spl0_88
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f627,plain,
( e2 = op(e1,e3)
| ~ spl0_88 ),
inference(avatar_component_clause,[],[f625]) ).
fof(f629,definition,
( spl0_89
<=> e2 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f631,plain,
( e2 = op(e1,e4)
| ~ spl0_89 ),
inference(avatar_component_clause,[],[f629]) ).
fof(f632,plain,
( spl0_61
| spl0_12
| spl0_87
| spl0_88
| spl0_89 ),
inference(avatar_split_clause,[],[f60,f629,f625,f621,f282,f508]) ).
fof(f643,definition,
( spl0_92
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f645,plain,
( e3 = op(e1,e2)
| ~ spl0_92 ),
inference(avatar_component_clause,[],[f643]) ).
fof(f647,definition,
( spl0_93
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f649,plain,
( e3 = op(e1,e3)
| ~ spl0_93 ),
inference(avatar_component_clause,[],[f647]) ).
fof(f651,definition,
( spl0_94
<=> e3 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f653,plain,
( e3 = op(e1,e4)
| ~ spl0_94 ),
inference(avatar_component_clause,[],[f651]) ).
fof(f654,plain,
( spl0_68
| spl0_17
| spl0_92
| spl0_93
| spl0_94 ),
inference(avatar_split_clause,[],[f62,f651,f647,f643,f303,f538]) ).
fof(f813,definition,
( spl0_126
<=> e0 = unit ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f815,plain,
( e0 = unit
| ~ spl0_126 ),
inference(avatar_component_clause,[],[f813]) ).
fof(f817,definition,
( spl0_127
<=> e1 = unit ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f819,plain,
( e1 = unit
| ~ spl0_127 ),
inference(avatar_component_clause,[],[f817]) ).
fof(f821,definition,
( spl0_128
<=> e2 = unit ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f823,plain,
( e2 = unit
| ~ spl0_128 ),
inference(avatar_component_clause,[],[f821]) ).
fof(f825,definition,
( spl0_129
<=> e3 = unit ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f827,plain,
( e3 = unit
| ~ spl0_129 ),
inference(avatar_component_clause,[],[f825]) ).
fof(f829,definition,
( spl0_130
<=> e4 = unit ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f831,plain,
( e4 = unit
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f829]) ).
fof(f832,plain,
( spl0_126
| spl0_127
| spl0_128
| spl0_129
| spl0_130 ),
inference(avatar_split_clause,[],[f35,f829,f825,f821,f817,f813]) ).
fof(f833,plain,
( spl0_1
| spl0_6
| spl0_11
| spl0_16
| spl0_21 ),
inference(avatar_split_clause,[],[f10,f320,f299,f278,f257,f236]) ).
fof(f858,plain,
spl0_78,
inference(avatar_split_clause,[],[f441,f581]) ).
fof(f859,plain,
( e1 = e2
| ~ spl0_6
| ~ spl0_11 ),
inference(forward_demodulation,[],[f280,f259]) ).
fof(f861,plain,
( e0 = e2
| ~ spl0_3
| ~ spl0_13 ),
inference(forward_demodulation,[],[f288,f246]) ).
fof(f862,plain,
( e0 = e2
| ~ spl0_4
| ~ spl0_14 ),
inference(forward_demodulation,[],[f292,f250]) ).
fof(f864,plain,
( e1 = e3
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_demodulation,[],[f301,f259]) ).
fof(f866,plain,
( e0 = e3
| ~ spl0_3
| ~ spl0_18 ),
inference(forward_demodulation,[],[f309,f246]) ).
fof(f867,plain,
( e0 = e3
| ~ spl0_4
| ~ spl0_19 ),
inference(forward_demodulation,[],[f313,f250]) ).
fof(f870,plain,
( e1 = e4
| ~ spl0_7
| ~ spl0_22 ),
inference(forward_demodulation,[],[f326,f263]) ).
fof(f873,plain,
( e0 = e4
| ~ spl0_5
| ~ spl0_25 ),
inference(forward_demodulation,[],[f338,f254]) ).
fof(f874,plain,
( e0 = e1
| ~ spl0_31
| ~ spl0_78 ),
inference(forward_demodulation,[],[f583,f368]) ).
fof(f875,plain,
( $false
| ~ spl0_6
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f859,f201]) ).
fof(f876,plain,
( ~ spl0_6
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f875]) ).
fof(f879,plain,
( $false
| ~ spl0_3
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f861,f204]) ).
fof(f880,plain,
( ~ spl0_3
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f879]) ).
fof(f881,plain,
( $false
| ~ spl0_4
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f862,f204]) ).
fof(f882,plain,
( ~ spl0_4
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f881]) ).
fof(f885,plain,
( $false
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f864,f200]) ).
fof(f886,plain,
( ~ spl0_6
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f885]) ).
fof(f889,plain,
( $false
| ~ spl0_3
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f866,f203]) ).
fof(f890,plain,
( ~ spl0_3
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f889]) ).
fof(f891,plain,
( $false
| ~ spl0_4
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f867,f203]) ).
fof(f892,plain,
( ~ spl0_4
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f891]) ).
fof(f897,plain,
( $false
| ~ spl0_7
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f870,f199]) ).
fof(f898,plain,
( ~ spl0_7
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f897]) ).
fof(f903,plain,
( $false
| ~ spl0_5
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f873,f202]) ).
fof(f904,plain,
( ~ spl0_5
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f903]) ).
fof(f905,plain,
( $false
| ~ spl0_31
| ~ spl0_78 ),
inference(forward_subsumption_resolution,[],[f874,f205]) ).
fof(f906,plain,
( ~ spl0_31
| ~ spl0_78 ),
inference(avatar_contradiction_clause,[],[f905]) ).
fof(f915,plain,
( e3 = e4
| ~ spl0_17
| ~ spl0_22 ),
inference(forward_demodulation,[],[f326,f305]) ).
fof(f916,plain,
( e2 = e3
| ~ spl0_11
| ~ spl0_16 ),
inference(forward_demodulation,[],[f301,f280]) ).
fof(f918,plain,
( e1 = e2
| ~ spl0_9
| ~ spl0_14 ),
inference(forward_demodulation,[],[f292,f271]) ).
fof(f919,plain,
( e1 = e3
| ~ spl0_9
| ~ spl0_19 ),
inference(forward_demodulation,[],[f313,f271]) ).
fof(f921,plain,
( e1 = e2
| ~ spl0_8
| ~ spl0_13 ),
inference(forward_demodulation,[],[f288,f267]) ).
fof(f922,plain,
( e1 = e3
| ~ spl0_8
| ~ spl0_18 ),
inference(forward_demodulation,[],[f309,f267]) ).
fof(f930,plain,
( $false
| ~ spl0_17
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f915,f196]) ).
fof(f931,plain,
( ~ spl0_17
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f930]) ).
fof(f932,plain,
( $false
| ~ spl0_11
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f916,f198]) ).
fof(f933,plain,
( ~ spl0_11
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f932]) ).
fof(f936,plain,
( $false
| ~ spl0_9
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f918,f201]) ).
fof(f937,plain,
( ~ spl0_9
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f936]) ).
fof(f938,plain,
( $false
| ~ spl0_9
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f919,f200]) ).
fof(f939,plain,
( ~ spl0_9
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f938]) ).
fof(f942,plain,
( $false
| ~ spl0_8
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f921,f201]) ).
fof(f943,plain,
( ~ spl0_8
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f942]) ).
fof(f944,plain,
( $false
| ~ spl0_8
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f922,f200]) ).
fof(f945,plain,
( ~ spl0_8
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f944]) ).
fof(f954,plain,
( e1 = e4
| ~ spl0_10
| ~ spl0_25 ),
inference(forward_demodulation,[],[f338,f275]) ).
fof(f962,plain,
( e0 = e2
| ~ spl0_78
| ~ spl0_87 ),
inference(forward_demodulation,[],[f623,f583]) ).
fof(f965,plain,
( e2 = e3
| ~ spl0_14
| ~ spl0_19 ),
inference(forward_demodulation,[],[f313,f292]) ).
fof(f970,plain,
( $false
| ~ spl0_10
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f954,f199]) ).
fof(f971,plain,
( ~ spl0_10
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f970]) ).
fof(f980,plain,
( $false
| ~ spl0_78
| ~ spl0_87 ),
inference(forward_subsumption_resolution,[],[f962,f204]) ).
fof(f981,plain,
( ~ spl0_78
| ~ spl0_87 ),
inference(avatar_contradiction_clause,[],[f980]) ).
fof(f986,plain,
( $false
| ~ spl0_14
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f965,f198]) ).
fof(f987,plain,
( ~ spl0_14
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f986]) ).
fof(f995,plain,
( e0 = e2
| ~ spl0_27
| ~ spl0_58 ),
inference(forward_demodulation,[],[f497,f348]) ).
fof(f996,plain,
( e1 = e2
| ~ spl0_30
| ~ spl0_61 ),
inference(forward_demodulation,[],[f510,f363]) ).
fof(f999,plain,
( e1 = e3
| ~ spl0_30
| ~ spl0_68 ),
inference(forward_demodulation,[],[f540,f363]) ).
fof(f1005,plain,
( e2 = e4
| ~ spl0_15
| ~ spl0_25 ),
inference(forward_demodulation,[],[f338,f296]) ).
fof(f1010,plain,
( $false
| ~ spl0_27
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f995,f204]) ).
fof(f1011,plain,
( ~ spl0_27
| ~ spl0_58 ),
inference(avatar_contradiction_clause,[],[f1010]) ).
fof(f1012,plain,
( $false
| ~ spl0_30
| ~ spl0_61 ),
inference(forward_subsumption_resolution,[],[f996,f201]) ).
fof(f1013,plain,
( ~ spl0_30
| ~ spl0_61 ),
inference(avatar_contradiction_clause,[],[f1012]) ).
fof(f1016,plain,
( $false
| ~ spl0_30
| ~ spl0_68 ),
inference(forward_subsumption_resolution,[],[f999,f200]) ).
fof(f1017,plain,
( ~ spl0_30
| ~ spl0_68 ),
inference(avatar_contradiction_clause,[],[f1016]) ).
fof(f1028,plain,
( $false
| ~ spl0_15
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f1005,f197]) ).
fof(f1029,plain,
( ~ spl0_15
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f1028]) ).
fof(f1039,plain,
( e2 = e3
| ~ spl0_61
| ~ spl0_68 ),
inference(forward_demodulation,[],[f540,f510]) ).
fof(f1048,plain,
( $false
| ~ spl0_61
| ~ spl0_68 ),
inference(forward_subsumption_resolution,[],[f1039,f198]) ).
fof(f1049,plain,
( ~ spl0_61
| ~ spl0_68 ),
inference(avatar_contradiction_clause,[],[f1048]) ).
fof(f1062,plain,
( e1 = e2
| ~ spl0_32
| ~ spl0_88 ),
inference(forward_demodulation,[],[f627,f373]) ).
fof(f1076,plain,
( $false
| ~ spl0_32
| ~ spl0_88 ),
inference(forward_subsumption_resolution,[],[f1062,f201]) ).
fof(f1077,plain,
( ~ spl0_32
| ~ spl0_88 ),
inference(avatar_contradiction_clause,[],[f1076]) ).
fof(f1090,plain,
( e1 = e3
| ~ spl0_32
| ~ spl0_93 ),
inference(forward_demodulation,[],[f649,f373]) ).
fof(f1102,plain,
( $false
| ~ spl0_32
| ~ spl0_93 ),
inference(forward_subsumption_resolution,[],[f1090,f200]) ).
fof(f1103,plain,
( ~ spl0_32
| ~ spl0_93 ),
inference(avatar_contradiction_clause,[],[f1102]) ).
fof(f1143,plain,
( e0 = e3
| ~ spl0_1
| ~ spl0_16 ),
inference(forward_demodulation,[],[f301,f238]) ).
fof(f1153,plain,
( $false
| ~ spl0_1
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1143,f203]) ).
fof(f1154,plain,
( ~ spl0_1
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1153]) ).
fof(f1161,plain,
( e0 = e1
| ~ spl0_4
| ~ spl0_9 ),
inference(forward_demodulation,[],[f250,f271]) ).
fof(f1165,plain,
( $false
| ~ spl0_4
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f1161,f205]) ).
fof(f1166,plain,
( ~ spl0_4
| ~ spl0_9 ),
inference(avatar_contradiction_clause,[],[f1165]) ).
fof(f1201,plain,
( e0 = e4
| ~ spl0_2
| ~ spl0_22 ),
inference(superposition,[],[f326,f242]) ).
fof(f1208,plain,
( $false
| ~ spl0_2
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f1201,f202]) ).
fof(f1209,plain,
( ~ spl0_2
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f1208]) ).
fof(f1215,plain,
( e0 = e2
| ~ spl0_1
| ~ spl0_11 ),
inference(forward_demodulation,[],[f280,f238]) ).
fof(f1217,plain,
( $false
| ~ spl0_1
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f1215,f204]) ).
fof(f1218,plain,
( ~ spl0_1
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f1217]) ).
fof(f1254,plain,
( e4 = op(e4,e4)
| ~ spl0_130 ),
inference(superposition,[],[f37,f831]) ).
fof(f1258,plain,
( $false
| spl0_25
| ~ spl0_130 ),
inference(forward_subsumption_resolution,[],[f1254,f337]) ).
fof(f1259,plain,
( spl0_25
| ~ spl0_130 ),
inference(avatar_contradiction_clause,[],[f1258]) ).
fof(f1263,plain,
( e3 = e4
| ~ spl0_20
| ~ spl0_25 ),
inference(forward_demodulation,[],[f338,f317]) ).
fof(f1269,plain,
( e3 = e4
| ~ spl0_20
| ~ spl0_130 ),
inference(forward_demodulation,[],[f1254,f317]) ).
fof(f1270,plain,
( $false
| ~ spl0_20
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f1263,f196]) ).
fof(f1271,plain,
( ~ spl0_20
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f1270]) ).
fof(f1276,plain,
( $false
| ~ spl0_20
| ~ spl0_130 ),
inference(forward_subsumption_resolution,[],[f1269,f196]) ).
fof(f1277,plain,
( ~ spl0_20
| ~ spl0_130 ),
inference(avatar_contradiction_clause,[],[f1276]) ).
fof(f1283,plain,
( e4 = op(e1,e4)
| ~ spl0_127 ),
inference(superposition,[],[f37,f819]) ).
fof(f1285,plain,
( e1 = e4
| ~ spl0_33
| ~ spl0_127 ),
inference(forward_demodulation,[],[f1283,f378]) ).
fof(f1286,plain,
( $false
| ~ spl0_33
| ~ spl0_127 ),
inference(forward_subsumption_resolution,[],[f1285,f199]) ).
fof(f1287,plain,
( ~ spl0_33
| ~ spl0_127 ),
inference(avatar_contradiction_clause,[],[f1286]) ).
fof(f1324,plain,
( e3 = op(e0,e3)
| ~ spl0_126 ),
inference(superposition,[],[f39,f815]) ).
fof(f1325,plain,
( e0 = e3
| ~ spl0_28
| ~ spl0_126 ),
inference(forward_demodulation,[],[f1324,f353]) ).
fof(f1326,plain,
( $false
| ~ spl0_28
| ~ spl0_126 ),
inference(forward_subsumption_resolution,[],[f1325,f203]) ).
fof(f1327,plain,
( ~ spl0_28
| ~ spl0_126 ),
inference(avatar_contradiction_clause,[],[f1326]) ).
fof(f1366,plain,
( e1 = op(e1,e2)
| ~ spl0_128 ),
inference(superposition,[],[f42,f823]) ).
fof(f1367,plain,
( $false
| spl0_31
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f1366,f367]) ).
fof(f1368,plain,
( spl0_31
| ~ spl0_128 ),
inference(avatar_contradiction_clause,[],[f1367]) ).
fof(f1377,plain,
( e4 = op(e0,e4)
| ~ spl0_126 ),
inference(superposition,[],[f37,f815]) ).
fof(f1381,plain,
( e2 = op(e0,e2)
| ~ spl0_126 ),
inference(superposition,[],[f41,f815]) ).
fof(f1382,plain,
( e1 = op(e1,e0)
| ~ spl0_126 ),
inference(superposition,[],[f42,f815]) ).
fof(f1384,plain,
( $false
| spl0_30
| ~ spl0_126 ),
inference(forward_subsumption_resolution,[],[f1382,f362]) ).
fof(f1385,plain,
( spl0_30
| ~ spl0_126 ),
inference(avatar_contradiction_clause,[],[f1384]) ).
fof(f1386,plain,
( $false
| spl0_58
| ~ spl0_126 ),
inference(forward_subsumption_resolution,[],[f1381,f496]) ).
fof(f1387,plain,
( spl0_58
| ~ spl0_126 ),
inference(avatar_contradiction_clause,[],[f1386]) ).
fof(f1407,plain,
( e1 = op(e0,e1)
| ~ spl0_126 ),
inference(superposition,[],[f43,f815]) ).
fof(f1408,plain,
( $false
| spl0_50
| ~ spl0_126 ),
inference(forward_subsumption_resolution,[],[f1407,f462]) ).
fof(f1409,plain,
( spl0_50
| ~ spl0_126 ),
inference(avatar_contradiction_clause,[],[f1408]) ).
fof(f1437,plain,
( e0 = e3
| ~ spl0_78
| ~ spl0_92 ),
inference(forward_demodulation,[],[f645,f583]) ).
fof(f1439,plain,
( $false
| ~ spl0_78
| ~ spl0_92 ),
inference(forward_subsumption_resolution,[],[f1437,f203]) ).
fof(f1440,plain,
( ~ spl0_78
| ~ spl0_92 ),
inference(avatar_contradiction_clause,[],[f1439]) ).
fof(f1441,plain,
( e1 = e2
| ~ spl0_33
| ~ spl0_89 ),
inference(forward_demodulation,[],[f631,f378]) ).
fof(f1444,plain,
( $false
| ~ spl0_33
| ~ spl0_89 ),
inference(forward_subsumption_resolution,[],[f1441,f201]) ).
fof(f1445,plain,
( ~ spl0_33
| ~ spl0_89 ),
inference(avatar_contradiction_clause,[],[f1444]) ).
fof(f1476,plain,
( e0 = e4
| ~ spl0_29
| ~ spl0_126 ),
inference(forward_demodulation,[],[f1377,f358]) ).
fof(f1479,plain,
( $false
| ~ spl0_29
| ~ spl0_126 ),
inference(forward_subsumption_resolution,[],[f1476,f202]) ).
fof(f1480,plain,
( ~ spl0_29
| ~ spl0_126 ),
inference(avatar_contradiction_clause,[],[f1479]) ).
fof(f1496,plain,
( e0 = e1
| ~ spl0_26
| ~ spl0_50 ),
inference(forward_demodulation,[],[f343,f463]) ).
fof(f1497,plain,
( $false
| ~ spl0_26
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f1496,f205]) ).
fof(f1498,plain,
( ~ spl0_26
| ~ spl0_50 ),
inference(avatar_contradiction_clause,[],[f1497]) ).
fof(f1501,plain,
( e0 = e1
| ~ spl0_1
| ~ spl0_6 ),
inference(superposition,[],[f259,f238]) ).
fof(f1506,plain,
( $false
| ~ spl0_1
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f1501,f205]) ).
fof(f1507,plain,
( ~ spl0_1
| ~ spl0_6 ),
inference(avatar_contradiction_clause,[],[f1506]) ).
fof(f1522,plain,
( e1 = op(e1,e3)
| ~ spl0_129 ),
inference(superposition,[],[f42,f827]) ).
fof(f1533,plain,
( $false
| spl0_32
| ~ spl0_129 ),
inference(forward_subsumption_resolution,[],[f1522,f372]) ).
fof(f1534,plain,
( spl0_32
| ~ spl0_129 ),
inference(avatar_contradiction_clause,[],[f1533]) ).
fof(f1553,plain,
( e1 = e3
| ~ spl0_33
| ~ spl0_94 ),
inference(forward_demodulation,[],[f653,f378]) ).
fof(f1574,plain,
( $false
| ~ spl0_33
| ~ spl0_94 ),
inference(forward_subsumption_resolution,[],[f1553,f200]) ).
fof(f1575,plain,
( ~ spl0_33
| ~ spl0_94 ),
inference(avatar_contradiction_clause,[],[f1574]) ).
fof(f1617,plain,
( e0 = e1
| ~ spl0_3
| ~ spl0_8 ),
inference(superposition,[],[f267,f246]) ).
fof(f1622,plain,
( $false
| ~ spl0_3
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f1617,f205]) ).
fof(f1623,plain,
( ~ spl0_3
| ~ spl0_8 ),
inference(avatar_contradiction_clause,[],[f1622]) ).
fof(f1632,plain,
( e2 = e3
| ~ spl0_88
| ~ spl0_93 ),
inference(forward_demodulation,[],[f649,f627]) ).
fof(f1654,plain,
( $false
| ~ spl0_88
| ~ spl0_93 ),
inference(forward_subsumption_resolution,[],[f1632,f198]) ).
fof(f1655,plain,
( ~ spl0_88
| ~ spl0_93 ),
inference(avatar_contradiction_clause,[],[f1654]) ).
fof(f1662,plain,
( e2 = e3
| ~ spl0_13
| ~ spl0_18 ),
inference(forward_demodulation,[],[f309,f288]) ).
fof(f1692,plain,
( $false
| ~ spl0_13
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1662,f198]) ).
fof(f1693,plain,
( ~ spl0_13
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1692]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f255]) ).
cnf(s2,plain,
( spl0_6
| spl0_7
| spl0_8
| spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f276]) ).
cnf(s3,plain,
( spl0_11
| spl0_12
| spl0_13
| spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f297]) ).
cnf(s4,plain,
( spl0_16
| spl0_17
| spl0_18
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f318]) ).
cnf(s6,plain,
( ~ spl0_6
| spl0_26 ),
inference(sat_conversion,[],[f344]) ).
cnf(s7,plain,
( ~ spl0_11
| spl0_27 ),
inference(sat_conversion,[],[f349]) ).
cnf(s8,plain,
( ~ spl0_16
| spl0_28 ),
inference(sat_conversion,[],[f354]) ).
cnf(s9,plain,
( ~ spl0_21
| spl0_29 ),
inference(sat_conversion,[],[f359]) ).
cnf(s11,plain,
( ~ spl0_12
| spl0_31 ),
inference(sat_conversion,[],[f369]) ).
cnf(s13,plain,
( ~ spl0_22
| spl0_33 ),
inference(sat_conversion,[],[f379]) ).
cnf(s26,plain,
spl0_22,
inference(sat_conversion,[],[f440]) ).
cnf(s41,plain,
( spl0_12
| spl0_61
| spl0_87
| spl0_88
| spl0_89 ),
inference(sat_conversion,[],[f632]) ).
cnf(s43,plain,
( spl0_17
| spl0_68
| spl0_92
| spl0_93
| spl0_94 ),
inference(sat_conversion,[],[f654]) ).
cnf(s77,plain,
( spl0_126
| spl0_127
| spl0_128
| spl0_129
| spl0_130 ),
inference(sat_conversion,[],[f832]) ).
cnf(s78,plain,
( spl0_1
| spl0_6
| spl0_11
| spl0_16
| spl0_21 ),
inference(sat_conversion,[],[f833]) ).
cnf(s103,plain,
spl0_78,
inference(sat_conversion,[],[f858]) ).
cnf(s104,plain,
( ~ spl0_6
| ~ spl0_11 ),
inference(sat_conversion,[],[f876]) ).
cnf(s106,plain,
( ~ spl0_3
| ~ spl0_13 ),
inference(sat_conversion,[],[f880]) ).
cnf(s107,plain,
( ~ spl0_4
| ~ spl0_14 ),
inference(sat_conversion,[],[f882]) ).
cnf(s109,plain,
( ~ spl0_6
| ~ spl0_16 ),
inference(sat_conversion,[],[f886]) ).
cnf(s111,plain,
( ~ spl0_3
| ~ spl0_18 ),
inference(sat_conversion,[],[f890]) ).
cnf(s112,plain,
( ~ spl0_4
| ~ spl0_19 ),
inference(sat_conversion,[],[f892]) ).
cnf(s115,plain,
( ~ spl0_7
| ~ spl0_22 ),
inference(sat_conversion,[],[f898]) ).
cnf(s118,plain,
( ~ spl0_5
| ~ spl0_25 ),
inference(sat_conversion,[],[f904]) ).
cnf(s119,plain,
( ~ spl0_31
| ~ spl0_78 ),
inference(sat_conversion,[],[f906]) ).
cnf(s123,plain,
( ~ spl0_17
| ~ spl0_22 ),
inference(sat_conversion,[],[f931]) ).
cnf(s124,plain,
( ~ spl0_11
| ~ spl0_16 ),
inference(sat_conversion,[],[f933]) ).
cnf(s126,plain,
( ~ spl0_9
| ~ spl0_14 ),
inference(sat_conversion,[],[f937]) ).
cnf(s127,plain,
( ~ spl0_9
| ~ spl0_19 ),
inference(sat_conversion,[],[f939]) ).
cnf(s129,plain,
( ~ spl0_8
| ~ spl0_13 ),
inference(sat_conversion,[],[f943]) ).
cnf(s130,plain,
( ~ spl0_8
| ~ spl0_18 ),
inference(sat_conversion,[],[f945]) ).
cnf(s133,plain,
( ~ spl0_10
| ~ spl0_25 ),
inference(sat_conversion,[],[f971]) ).
cnf(s138,plain,
( ~ spl0_78
| ~ spl0_87 ),
inference(sat_conversion,[],[f981]) ).
cnf(s141,plain,
( ~ spl0_14
| ~ spl0_19 ),
inference(sat_conversion,[],[f987]) ).
cnf(s143,plain,
( ~ spl0_27
| ~ spl0_58 ),
inference(sat_conversion,[],[f1011]) ).
cnf(s144,plain,
( ~ spl0_30
| ~ spl0_61 ),
inference(sat_conversion,[],[f1013]) ).
cnf(s146,plain,
( ~ spl0_30
| ~ spl0_68 ),
inference(sat_conversion,[],[f1017]) ).
cnf(s152,plain,
( ~ spl0_15
| ~ spl0_25 ),
inference(sat_conversion,[],[f1029]) ).
cnf(s156,plain,
( ~ spl0_61
| ~ spl0_68 ),
inference(sat_conversion,[],[f1049]) ).
cnf(s163,plain,
( ~ spl0_32
| ~ spl0_88 ),
inference(sat_conversion,[],[f1077]) ).
cnf(s167,plain,
( ~ spl0_32
| ~ spl0_93 ),
inference(sat_conversion,[],[f1103]) ).
cnf(s178,plain,
( ~ spl0_1
| ~ spl0_16 ),
inference(sat_conversion,[],[f1154]) ).
cnf(s182,plain,
( ~ spl0_4
| ~ spl0_9 ),
inference(sat_conversion,[],[f1166]) ).
cnf(s190,plain,
( ~ spl0_2
| ~ spl0_22 ),
inference(sat_conversion,[],[f1209]) ).
cnf(s192,plain,
( ~ spl0_1
| ~ spl0_11 ),
inference(sat_conversion,[],[f1218]) ).
cnf(s199,plain,
( spl0_25
| ~ spl0_130 ),
inference(sat_conversion,[],[f1259]) ).
cnf(s201,plain,
( ~ spl0_20
| ~ spl0_25 ),
inference(sat_conversion,[],[f1271]) ).
cnf(s204,plain,
( ~ spl0_20
| ~ spl0_130 ),
inference(sat_conversion,[],[f1277]) ).
cnf(s205,plain,
( ~ spl0_33
| ~ spl0_127 ),
inference(sat_conversion,[],[f1287]) ).
cnf(s211,plain,
( ~ spl0_28
| ~ spl0_126 ),
inference(sat_conversion,[],[f1327]) ).
cnf(s219,plain,
( spl0_31
| ~ spl0_128 ),
inference(sat_conversion,[],[f1368]) ).
cnf(s220,plain,
( spl0_30
| ~ spl0_126 ),
inference(sat_conversion,[],[f1385]) ).
cnf(s221,plain,
( spl0_58
| ~ spl0_126 ),
inference(sat_conversion,[],[f1387]) ).
cnf(s225,plain,
( spl0_50
| ~ spl0_126 ),
inference(sat_conversion,[],[f1409]) ).
cnf(s230,plain,
( ~ spl0_78
| ~ spl0_92 ),
inference(sat_conversion,[],[f1440]) ).
cnf(s231,plain,
( ~ spl0_33
| ~ spl0_89 ),
inference(sat_conversion,[],[f1445]) ).
cnf(s236,plain,
( ~ spl0_29
| ~ spl0_126 ),
inference(sat_conversion,[],[f1480]) ).
cnf(s239,plain,
( ~ spl0_26
| ~ spl0_50 ),
inference(sat_conversion,[],[f1498]) ).
cnf(s241,plain,
( ~ spl0_1
| ~ spl0_6 ),
inference(sat_conversion,[],[f1507]) ).
cnf(s245,plain,
( spl0_32
| ~ spl0_129 ),
inference(sat_conversion,[],[f1534]) ).
cnf(s253,plain,
( ~ spl0_33
| ~ spl0_94 ),
inference(sat_conversion,[],[f1575]) ).
cnf(s262,plain,
( ~ spl0_3
| ~ spl0_8 ),
inference(sat_conversion,[],[f1623]) ).
cnf(s265,plain,
( ~ spl0_88
| ~ spl0_93 ),
inference(sat_conversion,[],[f1655]) ).
cnf(s269,plain,
( ~ spl0_13
| ~ spl0_18 ),
inference(sat_conversion,[],[f1693]) ).
cnf(s277,plain,
~ spl0_92,
inference(rat,[],[s230,s103]) ).
cnf(s278,plain,
~ spl0_87,
inference(rat,[],[s138,s103]) ).
cnf(s279,plain,
~ spl0_31,
inference(rat,[],[s119,s103]) ).
cnf(s280,plain,
~ spl0_128,
inference(rat,[],[s219,s279]) ).
cnf(s281,plain,
( spl0_126
| spl0_127
| spl0_129
| spl0_130 ),
inference(rat,[],[s77,s280]) ).
cnf(s285,plain,
( spl0_17
| spl0_68
| spl0_93
| spl0_94 ),
inference(rat,[],[s43,s277]) ).
cnf(s286,plain,
( spl0_12
| spl0_61
| spl0_88
| spl0_89 ),
inference(rat,[],[s41,s278]) ).
cnf(s288,plain,
~ spl0_2,
inference(rat,[],[s190,s26]) ).
cnf(s289,plain,
~ spl0_17,
inference(rat,[],[s123,s26]) ).
cnf(s290,plain,
~ spl0_7,
inference(rat,[],[s115,s26]) ).
cnf(s291,plain,
spl0_33,
inference(rat,[],[s13,s26]) ).
cnf(s292,plain,
~ spl0_94,
inference(rat,[],[s253,s291]) ).
cnf(s293,plain,
~ spl0_89,
inference(rat,[],[s231,s291]) ).
cnf(s294,plain,
~ spl0_127,
inference(rat,[],[s205,s291]) ).
cnf(s296,plain,
~ spl0_12,
inference(rat,[],[s11,s279]) ).
cnf(s297,plain,
( spl0_16
| spl0_18
| spl0_19
| spl0_20 ),
inference(rat,[],[s4,s289]) ).
cnf(s298,plain,
( spl0_11
| spl0_13
| spl0_14
| spl0_15 ),
inference(rat,[],[s3,s296]) ).
cnf(s299,plain,
( spl0_6
| spl0_8
| spl0_9
| spl0_10 ),
inference(rat,[],[s2,s290]) ).
cnf(s300,plain,
( spl0_1
| spl0_3
| spl0_4
| spl0_5 ),
inference(rat,[],[s1,s288]) ).
cnf(s301,plain,
( ~ spl0_126
| spl0_11
| spl0_6
| spl0_1 ),
inference(rat,[],[s78,s8,s9,s211,s236]) ).
cnf(s302,plain,
~ spl0_32,
inference(rat,[],[s156,s286,s285,s163,s167,s296,s293,s289,s292]) ).
cnf(s303,plain,
~ spl0_129,
inference(rat,[],[s245,s302]) ).
cnf(s304,plain,
( ~ spl0_4
| spl0_10
| spl0_15
| spl0_11
| spl0_6 ),
inference(rat,[],[s129,s298,s299,s107,s182]) ).
cnf(s305,plain,
( spl0_11
| spl0_6
| spl0_1 ),
inference(rat,[],[s126,s298,s299,s106,s262,s300,s304,s118,s133,s152,s199,s281,s301,s303,s294]) ).
cnf(s306,plain,
( ~ spl0_4
| spl0_10
| spl0_20
| spl0_16
| spl0_6 ),
inference(rat,[],[s130,s297,s299,s112,s182]) ).
cnf(s307,plain,
( spl0_6
| spl0_1 ),
inference(rat,[],[s127,s297,s299,s111,s262,s300,s306,s118,s133,s199,s204,s281,s221,s143,s7,s124,s305,s303,s294]) ).
cnf(s308,plain,
( ~ spl0_4
| ~ spl0_6 ),
inference(rat,[],[s269,s298,s297,s107,s112,s109,s104,s204,s152,s199,s281,s225,s239,s6,s303,s294]) ).
cnf(s309,plain,
spl0_1,
inference(rat,[],[s141,s298,s297,s106,s111,s300,s308,s118,s152,s199,s204,s281,s225,s239,s6,s104,s109,s307,s294,s303]) ).
cnf(s310,plain,
~ spl0_6,
inference(rat,[],[s241,s309]) ).
cnf(s311,plain,
~ spl0_11,
inference(rat,[],[s192,s309]) ).
cnf(s312,plain,
~ spl0_16,
inference(rat,[],[s178,s309]) ).
cnf(s314,plain,
( ~ spl0_8
| ~ spl0_25 ),
inference(rat,[],[s141,s298,s297,s129,s130,s201,s152,s311,s312]) ).
cnf(s315,plain,
~ spl0_25,
inference(rat,[],[s269,s298,s297,s126,s127,s299,s314,s133,s152,s201,s311,s312,s310]) ).
cnf(s316,plain,
~ spl0_130,
inference(rat,[],[s199,s315]) ).
cnf(s317,plain,
spl0_126,
inference(rat,[],[s281,s303,s294,s316]) ).
cnf(s324,plain,
spl0_30,
inference(rat,[],[s220,s317]) ).
cnf(s336,plain,
~ spl0_68,
inference(rat,[],[s146,s324]) ).
cnf(s337,plain,
~ spl0_61,
inference(rat,[],[s144,s324]) ).
cnf(s340,plain,
spl0_93,
inference(rat,[],[s285,s292,s289,s336]) ).
cnf(s341,plain,
spl0_88,
inference(rat,[],[s286,s293,s296,s337]) ).
cnf(s343,plain,
$false,
inference(rat,[],[s265,s340,s341]) ).
fof(f1708,plain,
$false,
inference(avatar_sat_refutation,[],[s343]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG054+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.18 % Computer : n019.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 19:21:18 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.21 Running first-order model finding
% 0.07/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.27 % (140481)Will run a generic schedule for satisfiability detection.
% 0.07/0.27 % (140490)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3482950341:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.07/0.27 % (140486)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=886687387_2999 on theBenchmark for (2999ds/0Mi)
% 0.07/0.27 % (140488)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3429200568:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.07/0.27 % (140489)dis+10_1_sil=32000:sp=arity:random_seed=3477340163:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.07/0.27 % (140491)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1373286953:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.07/0.27 % (140492)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1909563385:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.07/0.27 % (140487)% WARNING: option uhcvi not known.
% 0.07/0.27 % (140490) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-140481-140490"...
% 0.07/0.27 % (140490)...printing done.
% 0.07/0.27 % (140487)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=432198118:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.07/0.27 % (140490)Refutation found. Thanks to Tanya!
% 0.07/0.27 % SZS status Theorem for theBenchmark
% 0.07/0.27 % SZS output start Proof for theBenchmark
% See solution above
% 0.07/0.27 % (140490)------------------------------
% 0.07/0.27 % (140490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.07/0.27 % (140490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.07/0.27 % (140490)CaDiCaL version: 2.1.3
% 0.07/0.27 % (140490)Termination reason: Refutation
% 0.07/0.27 % (140490)Time elapsed: 0.015 s
% 0.07/0.27 % (140490)Peak memory usage: 13 MB
% 0.07/0.27 % (140490)Instructions burned: 53 (million)
% 0.07/0.27 % (140481)Success in time 0.048 s
% 0.07/0.27 % Vampire exiting
%------------------------------------------------------------------------------