%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG065+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 : n018.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:13 AM UTC 2026
% Result : Theorem 0.21s 0.30s
% Output : Refutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 53
% Syntax : Number of formulae : 353 ( 92 unt; 47 def)
% Number of atoms : 1403 ( 923 equ)
% Maximal formula atoms : 125 ( 3 avg)
% Number of connectives : 1682 ( 632 ~; 651 |; 362 &)
% ( 37 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 4 avg)
% Maximal term depth : 3 ( 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(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/sandbox/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/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( e0 = op(op(e4,e2),op(e4,e2))
& e1 = op(e4,e2)
& e3 = op(e2,e4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
fof(f7,conjecture,
~ ( ( 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 )
& ( ( 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 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f8,negated_conjecture,
~ ~ ( ( 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 )
& ( ( 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 ) ) ),
inference(negated_conjecture,[status(cth)],[f7]) ).
fof(f9,plain,
( ( 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 )
& ( ( 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 ) ) ),
inference(flattening,[],[f8]) ).
fof(f10,definition,
( ( op(e4,op(e4,e4)) != e4
& op(e4,op(e4,e4)) = e4 )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f11,definition,
( ( op(e3,op(e3,e4)) != e4
& op(e4,op(e3,e4)) = e3 )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f12,definition,
( ( op(e4,op(e4,e3)) != e3
& op(e3,op(e4,e3)) = e4 )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f13,definition,
( ( op(e3,op(e3,e3)) != e3
& op(e3,op(e3,e3)) = e3 )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f14,definition,
( ( op(e4,op(e4,e2)) != e2
& op(e2,op(e4,e2)) = e4 )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f15,definition,
( ( op(e3,op(e3,e2)) != e2
& op(e2,op(e3,e2)) = e3 )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f16,definition,
( ( op(e4,op(e4,e1)) != e1
& op(e1,op(e4,e1)) = e4 )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f17,definition,
( ( op(e3,op(e3,e1)) != e1
& op(e1,op(e3,e1)) = e3 )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f18,definition,
( ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f19,definition,
( ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f20,plain,
( ( 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 )
& ( ( 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 )
| sP9
| sP8 )
& ( ( 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 )
| sP7
| sP6 )
& ( ( 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 )
| sP5
| sP4 )
& ( ( 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 )
| sP3
| sP2 )
& ( ( 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 )
| sP1
| sP0 ) ),
inference(definition_folding,[],[f9,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10]) ).
fof(f21,plain,
( ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ~ sP9 ),
inference(nnf_transformation,[],[f19]) ).
fof(f22,plain,
( ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 )
| ~ sP8 ),
inference(nnf_transformation,[],[f18]) ).
fof(f31,plain,
( e0 = op(e4,e4)
| e1 = op(e4,e4)
| e2 = op(e4,e4)
| e3 = op(e4,e4)
| e4 = op(e4,e4) ),
inference(cnf_transformation,[],[f1]) ).
fof(f32,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(f37,plain,
( e0 = op(e3,e3)
| e1 = op(e3,e3)
| e2 = op(e3,e3)
| e3 = op(e3,e3)
| e4 = op(e3,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f38,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(f43,plain,
( e0 = op(e2,e2)
| e1 = op(e2,e2)
| e2 = op(e2,e2)
| e3 = op(e2,e2)
| e4 = op(e2,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f56,plain,
( e0 = unit
| e1 = unit
| e2 = unit
| e3 = unit
| e4 = unit ),
inference(cnf_transformation,[],[f2]) ).
fof(f57,plain,
e4 = op(e4,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f58,plain,
e4 = op(unit,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f59,plain,
e3 = op(e3,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f60,plain,
e3 = op(unit,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f61,plain,
e2 = op(e2,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f62,plain,
e2 = op(unit,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f63,plain,
e1 = op(e1,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f65,plain,
e0 = op(e0,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f117,plain,
op(e4,e3) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f119,plain,
op(e4,e2) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f124,plain,
op(e4,e0) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f126,plain,
op(e4,e0) != op(e4,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f129,plain,
op(e3,e2) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f135,plain,
op(e3,e0) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f136,plain,
op(e3,e0) != op(e3,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f138,plain,
op(e2,e2) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f145,plain,
op(e2,e0) != op(e2,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f153,plain,
op(e1,e0) != op(e1,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f154,plain,
op(e1,e0) != op(e1,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f169,plain,
op(e2,e4) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f173,plain,
op(e0,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f177,plain,
op(e3,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f183,plain,
op(e0,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f184,plain,
op(e0,e3) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f187,plain,
op(e3,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f188,plain,
op(e2,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f189,plain,
op(e2,e2) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f190,plain,
op(e1,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f194,plain,
op(e0,e2) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f206,plain,
op(e0,e1) != op(e1,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f220,plain,
e1 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f227,plain,
e3 = op(e2,e4),
inference(cnf_transformation,[],[f6]) ).
fof(f228,plain,
e1 = op(e4,e2),
inference(cnf_transformation,[],[f6]) ).
fof(f229,plain,
e0 = op(op(e4,e2),op(e4,e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f231,plain,
( e0 != op(e3,op(e3,e0))
| ~ sP9 ),
inference(cnf_transformation,[],[f21]) ).
fof(f233,plain,
( e0 != op(e4,op(e4,e0))
| ~ sP8 ),
inference(cnf_transformation,[],[f22]) ).
fof(f285,plain,
( e0 = op(e0,op(e0,e0))
| e0 != op(e1,op(e1,e0))
| e0 != op(e2,op(e2,e0))
| sP9
| sP8 ),
inference(cnf_transformation,[],[f20]) ).
fof(f289,plain,
( e0 != op(e0,op(e0,e0))
| e0 != op(e1,op(e1,e0))
| e0 != op(e2,op(e2,e0))
| sP9
| sP8 ),
inference(cnf_transformation,[],[f20]) ).
fof(f291,plain,
( e3 != op(e4,e4)
| e4 = op(e4,e3) ),
inference(cnf_transformation,[],[f20]) ).
fof(f292,plain,
( e2 != op(e4,e4)
| e4 = op(e4,e2) ),
inference(cnf_transformation,[],[f20]) ).
fof(f293,plain,
( e1 != op(e4,e4)
| e4 = op(e4,e1) ),
inference(cnf_transformation,[],[f20]) ).
fof(f294,plain,
( e0 != op(e4,e4)
| e4 = op(e4,e0) ),
inference(cnf_transformation,[],[f20]) ).
fof(f295,plain,
( e4 != op(e3,e3)
| e3 = op(e3,e4) ),
inference(cnf_transformation,[],[f20]) ).
fof(f298,plain,
( e1 != op(e3,e3)
| e3 = op(e3,e1) ),
inference(cnf_transformation,[],[f20]) ).
fof(f299,plain,
( e0 != op(e3,e3)
| e3 = op(e3,e0) ),
inference(cnf_transformation,[],[f20]) ).
fof(f309,plain,
( e0 != op(e1,e1)
| e1 = op(e1,e0) ),
inference(cnf_transformation,[],[f20]) ).
fof(f318,plain,
( e0 != op(e1,op(e1,e0))
| e0 != op(e2,op(e2,e0))
| sP9
| sP8 ),
inference(global_subsumption,[],[f289,f285]) ).
fof(f321,plain,
e3 = op(e2,e4),
inference(global_subsumption,[],[f227]) ).
fof(f322,plain,
e1 = op(e4,e2),
inference(global_subsumption,[],[f228]) ).
fof(f326,plain,
e3 = op(e2,e4),
inference(global_subsumption,[],[f227]) ).
fof(f328,definition,
( spl10_1
<=> e4 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl10_1])],[avatar_definition]) ).
fof(f329,plain,
( e4 != op(e4,e3)
| spl10_1 ),
inference(avatar_component_clause,[],[f328]) ).
fof(f330,plain,
( e4 = op(e4,e3)
| ~ spl10_1 ),
inference(avatar_component_clause,[],[f328]) ).
fof(f332,definition,
( spl10_2
<=> e3 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl10_2])],[avatar_definition]) ).
fof(f334,plain,
( e3 != op(e4,e4)
| spl10_2 ),
inference(avatar_component_clause,[],[f332]) ).
fof(f335,plain,
( spl10_1
| ~ spl10_2 ),
inference(avatar_split_clause,[],[f291,f332,f328]) ).
fof(f339,plain,
( e4 != op(e4,e0)
| ~ spl10_1 ),
inference(superposition,[],[f124,f330]) ).
fof(f344,definition,
( spl10_3
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl10_3])],[avatar_definition]) ).
fof(f346,plain,
( ~ sP9
| spl10_3 ),
inference(avatar_component_clause,[],[f344]) ).
fof(f348,definition,
( spl10_4
<=> e0 = op(e3,op(e3,e0)) ),
introduced(definition,[new_symbols(definition,[spl10_4])],[avatar_definition]) ).
fof(f350,plain,
( e0 != op(e3,op(e3,e0))
| spl10_4 ),
inference(avatar_component_clause,[],[f348]) ).
fof(f351,plain,
( ~ spl10_3
| ~ spl10_4 ),
inference(avatar_split_clause,[],[f231,f348,f344]) ).
fof(f353,definition,
( spl10_5
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl10_5])],[avatar_definition]) ).
fof(f355,plain,
( ~ sP8
| spl10_5 ),
inference(avatar_component_clause,[],[f353]) ).
fof(f357,definition,
( spl10_6
<=> e0 = op(e4,op(e4,e0)) ),
introduced(definition,[new_symbols(definition,[spl10_6])],[avatar_definition]) ).
fof(f359,plain,
( e0 != op(e4,op(e4,e0))
| spl10_6 ),
inference(avatar_component_clause,[],[f357]) ).
fof(f360,plain,
( ~ spl10_5
| ~ spl10_6 ),
inference(avatar_split_clause,[],[f233,f357,f353]) ).
fof(f412,definition,
( spl10_17
<=> e3 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl10_17])],[avatar_definition]) ).
fof(f414,plain,
( e3 = op(e3,e4)
| ~ spl10_17 ),
inference(avatar_component_clause,[],[f412]) ).
fof(f416,definition,
( spl10_18
<=> e4 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl10_18])],[avatar_definition]) ).
fof(f418,plain,
( e4 != op(e3,e3)
| spl10_18 ),
inference(avatar_component_clause,[],[f416]) ).
fof(f419,plain,
( spl10_17
| ~ spl10_18 ),
inference(avatar_split_clause,[],[f295,f416,f412]) ).
fof(f424,plain,
( e3 != op(e2,e4)
| ~ spl10_17 ),
inference(superposition,[],[f169,f414]) ).
fof(f435,plain,
( $false
| ~ spl10_17 ),
inference(global_subsumption,[],[f424,f326]) ).
fof(f436,plain,
~ spl10_17,
inference(avatar_contradiction_clause,[],[f435]) ).
fof(f438,definition,
( spl10_19
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl10_19])],[avatar_definition]) ).
fof(f439,plain,
( e3 != op(e3,e2)
| spl10_19 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f442,definition,
( spl10_20
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl10_20])],[avatar_definition]) ).
fof(f443,plain,
( e2 = op(e3,e3)
| ~ spl10_20 ),
inference(avatar_component_clause,[],[f442]) ).
fof(f444,plain,
( e2 != op(e3,e3)
| spl10_20 ),
inference(avatar_component_clause,[],[f442]) ).
fof(f451,definition,
( spl10_21
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl10_21])],[avatar_definition]) ).
fof(f453,plain,
( e3 = op(e3,e1)
| ~ spl10_21 ),
inference(avatar_component_clause,[],[f451]) ).
fof(f455,definition,
( spl10_22
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl10_22])],[avatar_definition]) ).
fof(f457,plain,
( e1 != op(e3,e3)
| spl10_22 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f458,plain,
( spl10_21
| ~ spl10_22 ),
inference(avatar_split_clause,[],[f298,f455,f451]) ).
fof(f473,definition,
( spl10_24
<=> e4 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl10_24])],[avatar_definition]) ).
fof(f475,plain,
( e4 != op(e2,e2)
| spl10_24 ),
inference(avatar_component_clause,[],[f473]) ).
fof(f485,definition,
( spl10_26
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl10_26])],[avatar_definition]) ).
fof(f487,plain,
( e3 != op(e2,e2)
| spl10_26 ),
inference(avatar_component_clause,[],[f485]) ).
fof(f499,definition,
( spl10_27
<=> e1 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl10_27])],[avatar_definition]) ).
fof(f500,plain,
( e1 != op(e1,e4)
| spl10_27 ),
inference(avatar_component_clause,[],[f499]) ).
fof(f501,plain,
( e1 = op(e1,e4)
| ~ spl10_27 ),
inference(avatar_component_clause,[],[f499]) ).
fof(f509,plain,
( e1 != op(e1,e0)
| ~ spl10_27 ),
inference(superposition,[],[f153,f501]) ).
fof(f513,plain,
( e0 != op(e1,e1)
| ~ spl10_27 ),
inference(forward_subsumption_resolution,[],[f309,f509]) ).
fof(f562,definition,
( spl10_35
<=> e0 = op(e2,op(e2,e0)) ),
introduced(definition,[new_symbols(definition,[spl10_35])],[avatar_definition]) ).
fof(f564,plain,
( e0 != op(e2,op(e2,e0))
| spl10_35 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f566,plain,
( e0 != op(e1,op(e1,e0))
| e0 != op(e2,op(e2,e0))
| sP8
| spl10_3 ),
inference(forward_subsumption_resolution,[],[f318,f346]) ).
fof(f567,plain,
( e0 != op(e1,op(e1,e0))
| e0 != op(e2,op(e2,e0))
| spl10_3
| spl10_5 ),
inference(forward_subsumption_resolution,[],[f566,f355]) ).
fof(f569,definition,
( spl10_36
<=> e0 = op(e1,op(e1,e0)) ),
introduced(definition,[new_symbols(definition,[spl10_36])],[avatar_definition]) ).
fof(f571,plain,
( e0 != op(e1,op(e1,e0))
| spl10_36 ),
inference(avatar_component_clause,[],[f569]) ).
fof(f572,plain,
( ~ spl10_35
| ~ spl10_36
| spl10_3
| spl10_5 ),
inference(avatar_split_clause,[],[f567,f353,f344,f569,f562]) ).
fof(f577,definition,
( spl10_37
<=> e2 = op(e4,op(e2,e4)) ),
introduced(definition,[new_symbols(definition,[spl10_37])],[avatar_definition]) ).
fof(f578,plain,
( e2 != op(e4,op(e2,e4))
| spl10_37 ),
inference(avatar_component_clause,[],[f577]) ).
fof(f579,plain,
( e2 = op(e4,op(e2,e4))
| ~ spl10_37 ),
inference(avatar_component_clause,[],[f577]) ).
fof(f627,definition,
( spl10_44
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl10_44])],[avatar_definition]) ).
fof(f628,plain,
( e2 != op(e3,e2)
| spl10_44 ),
inference(avatar_component_clause,[],[f627]) ).
fof(f629,plain,
( e2 = op(e3,e2)
| ~ spl10_44 ),
inference(avatar_component_clause,[],[f627]) ).
fof(f658,plain,
( e2 != op(e0,e2)
| ~ spl10_44 ),
inference(superposition,[],[f194,f629]) ).
fof(f736,plain,
e3 != op(e2,e2),
inference(superposition,[],[f138,f321]) ).
fof(f743,plain,
~ spl10_26,
inference(avatar_split_clause,[],[f736,f485]) ).
fof(f760,plain,
( e2 != op(e4,e3)
| spl10_37 ),
inference(forward_demodulation,[],[f578,f321]) ).
fof(f779,plain,
e1 != op(e1,e2),
inference(superposition,[],[f190,f322]) ).
fof(f780,plain,
e1 != op(e2,e2),
inference(superposition,[],[f188,f322]) ).
fof(f781,plain,
e0 = op(e1,e1),
inference(forward_demodulation,[],[f229,f322]) ).
fof(f782,plain,
( $false
| ~ spl10_27 ),
inference(forward_subsumption_resolution,[],[f781,f513]) ).
fof(f783,plain,
~ spl10_27,
inference(avatar_contradiction_clause,[],[f782]) ).
fof(f785,plain,
e1 = op(e1,e0),
inference(global_subsumption,[],[f309,f781]) ).
fof(f806,definition,
( spl10_56
<=> e4 = unit ),
introduced(definition,[new_symbols(definition,[spl10_56])],[avatar_definition]) ).
fof(f808,plain,
( e4 = unit
| ~ spl10_56 ),
inference(avatar_component_clause,[],[f806]) ).
fof(f810,definition,
( spl10_57
<=> e3 = unit ),
introduced(definition,[new_symbols(definition,[spl10_57])],[avatar_definition]) ).
fof(f812,plain,
( e3 = unit
| ~ spl10_57 ),
inference(avatar_component_clause,[],[f810]) ).
fof(f814,definition,
( spl10_58
<=> e2 = unit ),
introduced(definition,[new_symbols(definition,[spl10_58])],[avatar_definition]) ).
fof(f816,plain,
( e2 = unit
| ~ spl10_58 ),
inference(avatar_component_clause,[],[f814]) ).
fof(f818,definition,
( spl10_59
<=> e1 = unit ),
introduced(definition,[new_symbols(definition,[spl10_59])],[avatar_definition]) ).
fof(f820,plain,
( e1 = unit
| ~ spl10_59 ),
inference(avatar_component_clause,[],[f818]) ).
fof(f822,definition,
( spl10_60
<=> e0 = unit ),
introduced(definition,[new_symbols(definition,[spl10_60])],[avatar_definition]) ).
fof(f824,plain,
( e0 = unit
| ~ spl10_60 ),
inference(avatar_component_clause,[],[f822]) ).
fof(f825,plain,
( spl10_56
| spl10_57
| spl10_58
| spl10_59
| spl10_60 ),
inference(avatar_split_clause,[],[f56,f822,f818,f814,f810,f806]) ).
fof(f832,plain,
( e1 = op(e1,e4)
| ~ spl10_56 ),
inference(superposition,[],[f63,f808]) ).
fof(f842,plain,
( $false
| spl10_27
| ~ spl10_56 ),
inference(forward_subsumption_resolution,[],[f832,f500]) ).
fof(f843,plain,
( spl10_27
| ~ spl10_56 ),
inference(avatar_contradiction_clause,[],[f842]) ).
fof(f863,plain,
( e1 = op(e1,e3)
| ~ spl10_57 ),
inference(superposition,[],[f63,f812]) ).
fof(f903,plain,
( e1 != op(e1,e0)
| ~ spl10_57 ),
inference(superposition,[],[f154,f863]) ).
fof(f913,plain,
( $false
| ~ spl10_57 ),
inference(forward_subsumption_resolution,[],[f903,f785]) ).
fof(f914,plain,
~ spl10_57,
inference(avatar_contradiction_clause,[],[f913]) ).
fof(f924,plain,
( e1 = op(e1,e2)
| ~ spl10_58 ),
inference(superposition,[],[f63,f816]) ).
fof(f936,plain,
( $false
| ~ spl10_58 ),
inference(forward_subsumption_resolution,[],[f924,f779]) ).
fof(f937,plain,
~ spl10_58,
inference(avatar_contradiction_clause,[],[f936]) ).
fof(f980,plain,
( e4 = op(e4,e0)
| ~ spl10_60 ),
inference(superposition,[],[f57,f824]) ).
fof(f985,plain,
( e2 = op(e0,e2)
| ~ spl10_60 ),
inference(superposition,[],[f62,f824]) ).
fof(f998,plain,
( $false
| ~ spl10_44
| ~ spl10_60 ),
inference(forward_subsumption_resolution,[],[f985,f658]) ).
fof(f999,plain,
( ~ spl10_44
| ~ spl10_60 ),
inference(avatar_contradiction_clause,[],[f998]) ).
fof(f1004,plain,
( $false
| ~ spl10_1
| ~ spl10_60 ),
inference(forward_subsumption_resolution,[],[f980,f339]) ).
fof(f1005,plain,
( ~ spl10_1
| ~ spl10_60 ),
inference(avatar_contradiction_clause,[],[f1004]) ).
fof(f1011,plain,
( e1 = e4
| e2 != op(e4,e4) ),
inference(forward_demodulation,[],[f292,f322]) ).
fof(f1012,plain,
e2 != op(e4,e4),
inference(forward_subsumption_resolution,[],[f1011,f220]) ).
fof(f1023,plain,
( e3 != op(e3,e0)
| ~ spl10_21 ),
inference(superposition,[],[f136,f453]) ).
fof(f1029,definition,
( spl10_63
<=> e4 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl10_63])],[avatar_definition]) ).
fof(f1031,plain,
( e4 = op(e4,e1)
| ~ spl10_63 ),
inference(avatar_component_clause,[],[f1029]) ).
fof(f1033,definition,
( spl10_64
<=> e1 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl10_64])],[avatar_definition]) ).
fof(f1035,plain,
( e1 != op(e4,e4)
| spl10_64 ),
inference(avatar_component_clause,[],[f1033]) ).
fof(f1036,plain,
( spl10_63
| ~ spl10_64 ),
inference(avatar_split_clause,[],[f293,f1033,f1029]) ).
fof(f1038,plain,
( e4 != op(e4,e0)
| ~ spl10_63 ),
inference(superposition,[],[f126,f1031]) ).
fof(f1048,definition,
( spl10_65
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl10_65])],[avatar_definition]) ).
fof(f1049,plain,
( e2 != op(e2,e0)
| spl10_65 ),
inference(avatar_component_clause,[],[f1048]) ).
fof(f1050,plain,
( e2 = op(e2,e0)
| ~ spl10_65 ),
inference(avatar_component_clause,[],[f1048]) ).
fof(f1052,definition,
( spl10_66
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl10_66])],[avatar_definition]) ).
fof(f1054,plain,
( e0 != op(e2,e2)
| spl10_66 ),
inference(avatar_component_clause,[],[f1052]) ).
fof(f1058,plain,
( e0 != op(e2,e2)
| spl10_35
| ~ spl10_65 ),
inference(superposition,[],[f564,f1050]) ).
fof(f1061,plain,
( ~ spl10_66
| spl10_35
| ~ spl10_65 ),
inference(avatar_split_clause,[],[f1058,f1048,f562,f1052]) ).
fof(f1117,plain,
( e0 = op(e0,e1)
| ~ spl10_59 ),
inference(superposition,[],[f65,f820]) ).
fof(f1126,plain,
e0 != op(e0,e1),
inference(superposition,[],[f206,f781]) ).
fof(f1132,plain,
( $false
| ~ spl10_59 ),
inference(global_subsumption,[],[f1126,f1117]) ).
fof(f1133,plain,
~ spl10_59,
inference(avatar_contradiction_clause,[],[f1132]) ).
fof(f1134,plain,
( e4 = op(e4,e0)
| ~ spl10_60 ),
inference(superposition,[],[f57,f824]) ).
fof(f1135,plain,
( e4 = op(e0,e4)
| ~ spl10_60 ),
inference(superposition,[],[f58,f824]) ).
fof(f1136,plain,
( e3 = op(e3,e0)
| ~ spl10_60 ),
inference(superposition,[],[f59,f824]) ).
fof(f1137,plain,
( e3 = op(e0,e3)
| ~ spl10_60 ),
inference(superposition,[],[f60,f824]) ).
fof(f1138,plain,
( e2 = op(e2,e0)
| ~ spl10_60 ),
inference(superposition,[],[f61,f824]) ).
fof(f1152,plain,
( $false
| ~ spl10_21
| ~ spl10_60 ),
inference(forward_subsumption_resolution,[],[f1136,f1023]) ).
fof(f1153,plain,
( ~ spl10_21
| ~ spl10_60 ),
inference(avatar_contradiction_clause,[],[f1152]) ).
fof(f1154,plain,
( $false
| ~ spl10_60
| ~ spl10_63 ),
inference(forward_subsumption_resolution,[],[f1134,f1038]) ).
fof(f1155,plain,
( ~ spl10_60
| ~ spl10_63 ),
inference(avatar_contradiction_clause,[],[f1154]) ).
fof(f1173,definition,
( spl10_69
<=> e4 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl10_69])],[avatar_definition]) ).
fof(f1175,plain,
( e4 = op(e4,e0)
| ~ spl10_69 ),
inference(avatar_component_clause,[],[f1173]) ).
fof(f1177,definition,
( spl10_70
<=> e0 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl10_70])],[avatar_definition]) ).
fof(f1178,plain,
( e0 = op(e4,e4)
| ~ spl10_70 ),
inference(avatar_component_clause,[],[f1177]) ).
fof(f1179,plain,
( e0 != op(e4,e4)
| spl10_70 ),
inference(avatar_component_clause,[],[f1177]) ).
fof(f1180,plain,
( spl10_69
| ~ spl10_70 ),
inference(avatar_split_clause,[],[f294,f1177,f1173]) ).
fof(f1188,definition,
( spl10_71
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl10_71])],[avatar_definition]) ).
fof(f1190,plain,
( e3 = op(e3,e0)
| ~ spl10_71 ),
inference(avatar_component_clause,[],[f1188]) ).
fof(f1192,definition,
( spl10_72
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl10_72])],[avatar_definition]) ).
fof(f1193,plain,
( e0 = op(e3,e3)
| ~ spl10_72 ),
inference(avatar_component_clause,[],[f1192]) ).
fof(f1194,plain,
( e0 != op(e3,e3)
| spl10_72 ),
inference(avatar_component_clause,[],[f1192]) ).
fof(f1195,plain,
( spl10_71
| ~ spl10_72 ),
inference(avatar_split_clause,[],[f299,f1192,f1188]) ).
fof(f1196,plain,
( e3 != op(e3,e2)
| ~ spl10_71 ),
inference(superposition,[],[f135,f1190]) ).
fof(f1201,plain,
( e0 != op(e3,e3)
| spl10_4
| ~ spl10_71 ),
inference(superposition,[],[f350,f1190]) ).
fof(f1205,plain,
( ~ spl10_72
| spl10_4
| ~ spl10_71 ),
inference(avatar_split_clause,[],[f1201,f1188,f348,f1192]) ).
fof(f1243,plain,
( $false
| ~ spl10_60
| spl10_65 ),
inference(forward_subsumption_resolution,[],[f1138,f1049]) ).
fof(f1244,plain,
( ~ spl10_60
| spl10_65 ),
inference(avatar_contradiction_clause,[],[f1243]) ).
fof(f1245,plain,
( e2 != op(e2,e2)
| ~ spl10_65 ),
inference(superposition,[],[f145,f1050]) ).
fof(f1266,plain,
( e1 = op(e4,e4)
| e2 = op(e4,e4)
| e3 = op(e4,e4)
| e4 = op(e4,e4)
| spl10_70 ),
inference(forward_subsumption_resolution,[],[f31,f1179]) ).
fof(f1267,plain,
( e2 = op(e4,e4)
| e3 = op(e4,e4)
| e4 = op(e4,e4)
| spl10_64
| spl10_70 ),
inference(forward_subsumption_resolution,[],[f1266,f1035]) ).
fof(f1268,plain,
( e3 = op(e4,e4)
| e4 = op(e4,e4)
| spl10_64
| spl10_70 ),
inference(forward_subsumption_resolution,[],[f1267,f1012]) ).
fof(f1269,plain,
( e4 = op(e4,e4)
| spl10_2
| spl10_64
| spl10_70 ),
inference(forward_subsumption_resolution,[],[f1268,f334]) ).
fof(f1275,plain,
( e4 != op(e0,e4)
| spl10_2
| spl10_64
| spl10_70 ),
inference(superposition,[],[f173,f1269]) ).
fof(f1280,plain,
( $false
| spl10_2
| ~ spl10_60
| spl10_64
| spl10_70 ),
inference(forward_subsumption_resolution,[],[f1275,f1135]) ).
fof(f1281,plain,
( spl10_2
| ~ spl10_60
| spl10_64
| spl10_70 ),
inference(avatar_contradiction_clause,[],[f1280]) ).
fof(f1302,plain,
( e0 = op(e4,e3)
| e1 = op(e4,e3)
| e3 = op(e4,e3)
| e4 = op(e4,e3)
| spl10_37 ),
inference(forward_subsumption_resolution,[],[f32,f760]) ).
fof(f1303,plain,
( e0 = op(e4,e3)
| e1 = op(e4,e3)
| e3 = op(e4,e3)
| spl10_1
| spl10_37 ),
inference(forward_subsumption_resolution,[],[f1302,f329]) ).
fof(f1305,definition,
( spl10_73
<=> e3 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl10_73])],[avatar_definition]) ).
fof(f1307,plain,
( e3 = op(e4,e3)
| ~ spl10_73 ),
inference(avatar_component_clause,[],[f1305]) ).
fof(f1309,definition,
( spl10_74
<=> e1 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl10_74])],[avatar_definition]) ).
fof(f1311,plain,
( e1 = op(e4,e3)
| ~ spl10_74 ),
inference(avatar_component_clause,[],[f1309]) ).
fof(f1313,definition,
( spl10_75
<=> e0 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl10_75])],[avatar_definition]) ).
fof(f1315,plain,
( e0 = op(e4,e3)
| ~ spl10_75 ),
inference(avatar_component_clause,[],[f1313]) ).
fof(f1316,plain,
( spl10_73
| spl10_74
| spl10_75
| spl10_1
| spl10_37 ),
inference(avatar_split_clause,[],[f1303,f577,f328,f1313,f1309,f1305]) ).
fof(f1323,plain,
( e3 != op(e0,e3)
| ~ spl10_73 ),
inference(superposition,[],[f183,f1307]) ).
fof(f1326,plain,
( $false
| ~ spl10_60
| ~ spl10_73 ),
inference(forward_subsumption_resolution,[],[f1323,f1137]) ).
fof(f1327,plain,
( ~ spl10_60
| ~ spl10_73 ),
inference(avatar_contradiction_clause,[],[f1326]) ).
fof(f1331,plain,
( e1 != op(e4,e2)
| ~ spl10_74 ),
inference(superposition,[],[f119,f1311]) ).
fof(f1342,plain,
( $false
| ~ spl10_74 ),
inference(forward_subsumption_resolution,[],[f1331,f322]) ).
fof(f1343,plain,
~ spl10_74,
inference(avatar_contradiction_clause,[],[f1342]) ).
fof(f1344,plain,
( e0 != op(e4,e4)
| ~ spl10_75 ),
inference(superposition,[],[f117,f1315]) ).
fof(f1357,plain,
( $false
| ~ spl10_70
| ~ spl10_75 ),
inference(forward_subsumption_resolution,[],[f1344,f1178]) ).
fof(f1358,plain,
( ~ spl10_70
| ~ spl10_75 ),
inference(avatar_contradiction_clause,[],[f1357]) ).
fof(f1359,plain,
( e2 = op(e4,e3)
| ~ spl10_37 ),
inference(forward_demodulation,[],[f579,f321]) ).
fof(f1439,plain,
( e1 = op(e3,e3)
| e2 = op(e3,e3)
| e3 = op(e3,e3)
| e4 = op(e3,e3)
| spl10_72 ),
inference(forward_subsumption_resolution,[],[f37,f1194]) ).
fof(f1440,plain,
( e2 = op(e3,e3)
| e3 = op(e3,e3)
| e4 = op(e3,e3)
| spl10_22
| spl10_72 ),
inference(forward_subsumption_resolution,[],[f1439,f457]) ).
fof(f1441,plain,
( e3 = op(e3,e3)
| e4 = op(e3,e3)
| spl10_20
| spl10_22
| spl10_72 ),
inference(forward_subsumption_resolution,[],[f1440,f444]) ).
fof(f1442,plain,
( e3 = op(e3,e3)
| spl10_18
| spl10_20
| spl10_22
| spl10_72 ),
inference(forward_subsumption_resolution,[],[f1441,f418]) ).
fof(f1450,plain,
( e3 != op(e0,e3)
| spl10_18
| spl10_20
| spl10_22
| spl10_72 ),
inference(superposition,[],[f184,f1442]) ).
fof(f1455,plain,
( $false
| spl10_18
| spl10_20
| spl10_22
| ~ spl10_60
| spl10_72 ),
inference(forward_subsumption_resolution,[],[f1450,f1137]) ).
fof(f1456,plain,
( spl10_18
| spl10_20
| spl10_22
| ~ spl10_60
| spl10_72 ),
inference(avatar_contradiction_clause,[],[f1455]) ).
fof(f1460,plain,
( ~ spl10_19
| ~ spl10_71 ),
inference(avatar_split_clause,[],[f1196,f1188,f438]) ).
fof(f1471,plain,
( e2 != op(e4,e3)
| ~ spl10_20 ),
inference(superposition,[],[f177,f443]) ).
fof(f1479,plain,
( $false
| ~ spl10_20
| ~ spl10_37 ),
inference(forward_subsumption_resolution,[],[f1471,f1359]) ).
fof(f1480,plain,
( ~ spl10_20
| ~ spl10_37 ),
inference(avatar_contradiction_clause,[],[f1479]) ).
fof(f1495,plain,
( e0 != op(e3,e2)
| ~ spl10_72 ),
inference(superposition,[],[f129,f1193]) ).
fof(f1507,plain,
( e1 = op(e3,e2)
| e2 = op(e3,e2)
| e3 = op(e3,e2)
| e4 = op(e3,e2)
| ~ spl10_72 ),
inference(forward_subsumption_resolution,[],[f38,f1495]) ).
fof(f1508,plain,
( e1 = op(e3,e2)
| e3 = op(e3,e2)
| e4 = op(e3,e2)
| spl10_44
| ~ spl10_72 ),
inference(forward_subsumption_resolution,[],[f1507,f628]) ).
fof(f1509,plain,
( e1 = op(e3,e2)
| e4 = op(e3,e2)
| spl10_19
| spl10_44
| ~ spl10_72 ),
inference(forward_subsumption_resolution,[],[f1508,f439]) ).
fof(f1511,definition,
( spl10_80
<=> e4 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl10_80])],[avatar_definition]) ).
fof(f1513,plain,
( e4 = op(e3,e2)
| ~ spl10_80 ),
inference(avatar_component_clause,[],[f1511]) ).
fof(f1515,definition,
( spl10_81
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl10_81])],[avatar_definition]) ).
fof(f1517,plain,
( e1 = op(e3,e2)
| ~ spl10_81 ),
inference(avatar_component_clause,[],[f1515]) ).
fof(f1518,plain,
( spl10_80
| spl10_81
| spl10_19
| spl10_44
| ~ spl10_72 ),
inference(avatar_split_clause,[],[f1509,f1192,f627,f438,f1515,f1511]) ).
fof(f1552,plain,
( e1 != op(e4,e2)
| ~ spl10_81 ),
inference(superposition,[],[f187,f1517]) ).
fof(f1560,plain,
( $false
| ~ spl10_81 ),
inference(forward_subsumption_resolution,[],[f1552,f322]) ).
fof(f1561,plain,
~ spl10_81,
inference(avatar_contradiction_clause,[],[f1560]) ).
fof(f1563,plain,
( e4 != op(e2,e2)
| ~ spl10_80 ),
inference(superposition,[],[f189,f1513]) ).
fof(f1628,plain,
( e1 = op(e2,e2)
| e2 = op(e2,e2)
| e3 = op(e2,e2)
| e4 = op(e2,e2)
| spl10_66 ),
inference(forward_subsumption_resolution,[],[f43,f1054]) ).
fof(f1629,plain,
( e2 = op(e2,e2)
| e3 = op(e2,e2)
| e4 = op(e2,e2)
| spl10_66 ),
inference(forward_subsumption_resolution,[],[f1628,f780]) ).
fof(f1630,plain,
( e3 = op(e2,e2)
| e4 = op(e2,e2)
| ~ spl10_65
| spl10_66 ),
inference(forward_subsumption_resolution,[],[f1629,f1245]) ).
fof(f1631,plain,
( e4 = op(e2,e2)
| spl10_26
| ~ spl10_65
| spl10_66 ),
inference(forward_subsumption_resolution,[],[f1630,f487]) ).
fof(f1632,plain,
( $false
| spl10_24
| spl10_26
| ~ spl10_65
| spl10_66 ),
inference(forward_subsumption_resolution,[],[f1631,f475]) ).
fof(f1633,plain,
( spl10_24
| spl10_26
| ~ spl10_65
| spl10_66 ),
inference(avatar_contradiction_clause,[],[f1632]) ).
fof(f1634,plain,
( ~ spl10_24
| ~ spl10_80 ),
inference(avatar_split_clause,[],[f1563,f1511,f473]) ).
fof(f1636,plain,
( e0 != op(e1,e1)
| spl10_36 ),
inference(forward_demodulation,[],[f571,f785]) ).
fof(f1642,plain,
( $false
| spl10_36 ),
inference(forward_subsumption_resolution,[],[f1636,f781]) ).
fof(f1643,plain,
spl10_36,
inference(avatar_contradiction_clause,[],[f1642]) ).
fof(f1656,plain,
( e0 != op(e4,e4)
| spl10_6
| ~ spl10_69 ),
inference(forward_demodulation,[],[f359,f1175]) ).
fof(f1663,plain,
( $false
| spl10_6
| ~ spl10_69
| ~ spl10_70 ),
inference(forward_subsumption_resolution,[],[f1656,f1178]) ).
fof(f1664,plain,
( spl10_6
| ~ spl10_69
| ~ spl10_70 ),
inference(avatar_contradiction_clause,[],[f1663]) ).
cnf(s340,plain,
( spl10_1
| ~ spl10_2 ),
inference(sat_conversion,[],[f335]) ).
cnf(s423,plain,
( ~ spl10_3
| ~ spl10_4 ),
inference(sat_conversion,[],[f351]) ).
cnf(s427,plain,
( ~ spl10_5
| ~ spl10_6 ),
inference(sat_conversion,[],[f360]) ).
cnf(s460,plain,
( spl10_17
| ~ spl10_18 ),
inference(sat_conversion,[],[f419]) ).
cnf(s474,plain,
~ spl10_17,
inference(sat_conversion,[],[f436]) ).
cnf(s492,plain,
( spl10_21
| ~ spl10_22 ),
inference(sat_conversion,[],[f458]) ).
cnf(s605,plain,
( spl10_3
| spl10_5
| ~ spl10_35
| ~ spl10_36 ),
inference(sat_conversion,[],[f572]) ).
cnf(s713,plain,
~ spl10_26,
inference(sat_conversion,[],[f743]) ).
cnf(s743,plain,
~ spl10_27,
inference(sat_conversion,[],[f783]) ).
cnf(s771,plain,
( spl10_56
| spl10_57
| spl10_58
| spl10_59
| spl10_60 ),
inference(sat_conversion,[],[f825]) ).
cnf(s777,plain,
( spl10_27
| ~ spl10_56 ),
inference(sat_conversion,[],[f843]) ).
cnf(s811,plain,
~ spl10_57,
inference(sat_conversion,[],[f914]) ).
cnf(s823,plain,
~ spl10_58,
inference(sat_conversion,[],[f937]) ).
cnf(s850,plain,
( ~ spl10_44
| ~ spl10_60 ),
inference(sat_conversion,[],[f999]) ).
cnf(s853,plain,
( ~ spl10_1
| ~ spl10_60 ),
inference(sat_conversion,[],[f1005]) ).
cnf(s911,plain,
( spl10_63
| ~ spl10_64 ),
inference(sat_conversion,[],[f1036]) ).
cnf(s933,plain,
( spl10_35
| ~ spl10_65
| ~ spl10_66 ),
inference(sat_conversion,[],[f1061]) ).
cnf(s986,plain,
~ spl10_59,
inference(sat_conversion,[],[f1133]) ).
cnf(s996,plain,
( ~ spl10_21
| ~ spl10_60 ),
inference(sat_conversion,[],[f1153]) ).
cnf(s998,plain,
( ~ spl10_60
| ~ spl10_63 ),
inference(sat_conversion,[],[f1155]) ).
cnf(s1027,plain,
( spl10_69
| ~ spl10_70 ),
inference(sat_conversion,[],[f1180]) ).
cnf(s1033,plain,
( spl10_71
| ~ spl10_72 ),
inference(sat_conversion,[],[f1195]) ).
cnf(s1038,plain,
( spl10_4
| ~ spl10_71
| ~ spl10_72 ),
inference(sat_conversion,[],[f1205]) ).
cnf(s1060,plain,
( ~ spl10_60
| spl10_65 ),
inference(sat_conversion,[],[f1244]) ).
cnf(s1081,plain,
( spl10_2
| ~ spl10_60
| spl10_64
| spl10_70 ),
inference(sat_conversion,[],[f1281]) ).
cnf(s1094,plain,
( spl10_1
| spl10_37
| spl10_73
| spl10_74
| spl10_75 ),
inference(sat_conversion,[],[f1316]) ).
cnf(s1097,plain,
( ~ spl10_60
| ~ spl10_73 ),
inference(sat_conversion,[],[f1327]) ).
cnf(s1106,plain,
~ spl10_74,
inference(sat_conversion,[],[f1343]) ).
cnf(s1113,plain,
( ~ spl10_70
| ~ spl10_75 ),
inference(sat_conversion,[],[f1358]) ).
cnf(s1146,plain,
( spl10_18
| spl10_20
| spl10_22
| ~ spl10_60
| spl10_72 ),
inference(sat_conversion,[],[f1456]) ).
cnf(s1154,plain,
( ~ spl10_19
| ~ spl10_71 ),
inference(sat_conversion,[],[f1460]) ).
cnf(s1165,plain,
( ~ spl10_20
| ~ spl10_37 ),
inference(sat_conversion,[],[f1480]) ).
cnf(s1190,plain,
( spl10_19
| spl10_44
| ~ spl10_72
| spl10_80
| spl10_81 ),
inference(sat_conversion,[],[f1518]) ).
cnf(s1208,plain,
~ spl10_81,
inference(sat_conversion,[],[f1561]) ).
cnf(s1238,plain,
( spl10_24
| spl10_26
| ~ spl10_65
| spl10_66 ),
inference(sat_conversion,[],[f1633]) ).
cnf(s1244,plain,
( ~ spl10_24
| ~ spl10_80 ),
inference(sat_conversion,[],[f1634]) ).
cnf(s1249,plain,
spl10_36,
inference(sat_conversion,[],[f1643]) ).
cnf(s1253,plain,
( spl10_6
| ~ spl10_69
| ~ spl10_70 ),
inference(sat_conversion,[],[f1664]) ).
cnf(s1255,plain,
( spl10_19
| spl10_44
| ~ spl10_72
| spl10_80 ),
inference(rat,[],[s1190,s1208]) ).
cnf(s1256,plain,
( spl10_1
| spl10_37
| spl10_73
| spl10_75 ),
inference(rat,[],[s1094,s1106]) ).
cnf(s1257,plain,
( spl10_56
| spl10_60 ),
inference(rat,[],[s771,s986,s823,s811]) ).
cnf(s1258,plain,
~ spl10_56,
inference(rat,[],[s777,s743]) ).
cnf(s1259,plain,
spl10_60,
inference(rat,[],[s1257,s1258]) ).
cnf(s1261,plain,
~ spl10_73,
inference(rat,[],[s1097,s1259]) ).
cnf(s1262,plain,
spl10_65,
inference(rat,[],[s1060,s1259]) ).
cnf(s1264,plain,
~ spl10_63,
inference(rat,[],[s998,s1259]) ).
cnf(s1265,plain,
~ spl10_21,
inference(rat,[],[s996,s1259]) ).
cnf(s1270,plain,
~ spl10_1,
inference(rat,[],[s853,s1259]) ).
cnf(s1272,plain,
~ spl10_44,
inference(rat,[],[s850,s1259]) ).
cnf(s1273,plain,
~ spl10_64,
inference(rat,[],[s911,s1264]) ).
cnf(s1277,plain,
( spl10_3
| spl10_5
| ~ spl10_35 ),
inference(rat,[],[s605,s1249]) ).
cnf(s1280,plain,
~ spl10_22,
inference(rat,[],[s492,s1265]) ).
cnf(s1281,plain,
~ spl10_18,
inference(rat,[],[s460,s474]) ).
cnf(s1282,plain,
~ spl10_2,
inference(rat,[],[s340,s1270]) ).
cnf(s1283,plain,
spl10_70,
inference(rat,[],[s1081,s1273,s1259,s1282]) ).
cnf(s1284,plain,
~ spl10_75,
inference(rat,[],[s1113,s1283]) ).
cnf(s1285,plain,
spl10_69,
inference(rat,[],[s1027,s1283]) ).
cnf(s1287,plain,
spl10_37,
inference(rat,[],[s1256,s1270,s1261,s1284]) ).
cnf(s1288,plain,
spl10_6,
inference(rat,[],[s1253,s1283,s1285]) ).
cnf(s1289,plain,
~ spl10_20,
inference(rat,[],[s1165,s1287]) ).
cnf(s1290,plain,
~ spl10_5,
inference(rat,[],[s427,s1288]) ).
cnf(s1291,plain,
spl10_72,
inference(rat,[],[s1146,s1281,s1259,s1280,s1289]) ).
cnf(s1293,plain,
spl10_71,
inference(rat,[],[s1033,s1291]) ).
cnf(s1294,plain,
~ spl10_19,
inference(rat,[],[s1154,s1293]) ).
cnf(s1295,plain,
spl10_4,
inference(rat,[],[s1038,s1291,s1293]) ).
cnf(s1296,plain,
spl10_80,
inference(rat,[],[s1255,s1291,s1272,s1294]) ).
cnf(s1297,plain,
~ spl10_3,
inference(rat,[],[s423,s1295]) ).
cnf(s1298,plain,
~ spl10_24,
inference(rat,[],[s1244,s1296]) ).
cnf(s1300,plain,
~ spl10_35,
inference(rat,[],[s1277,s1290,s1297]) ).
cnf(s1301,plain,
spl10_66,
inference(rat,[],[s1238,s713,s1262,s1298]) ).
cnf(s1303,plain,
$false,
inference(rat,[],[s933,s1262,s1301,s1300]) ).
fof(f1667,plain,
$false,
inference(avatar_sat_refutation,[],[s1303]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG065+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.11/0.18 % Computer : n018.cluster.edu
% 0.11/0.18 % Model : x86_64 x86_64
% 0.11/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.18 % Memory : 8046.5625MB
% 0.11/0.18 % OS : Linux 6.8.0-71-generic
% 0.11/0.18 % CPULimit : 300
% 0.11/0.18 % WCLimit : 300
% 0.11/0.18 % DateTime : Mon Sep 28 19:26:40 UTC 2026
% 0.11/0.18 % CPUTime :
% 0.11/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.22 Running first-order model finding
% 0.11/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.30 % (3688085)Will run a generic schedule for satisfiability detection.
% 0.21/0.30 % (3688096)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=262847855:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.21/0.30 % (3688091)% WARNING: option uhcvi not known.
% 0.21/0.30 % (3688092)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=419962406:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.21/0.30 % (3688093)dis+10_1_sil=32000:sp=arity:random_seed=3931617464:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.21/0.30 % (3688090)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3014899721_2999 on theBenchmark for (2999ds/0Mi)
% 0.21/0.30 % (3688091)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2625285346:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.21/0.30 % (3688095)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2460341716:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.21/0.30 % (3688094)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3228483499:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.21/0.30 % Detected minimum model sizes of [5]
% 0.21/0.30 % Detected maximum model sizes of [max]
% 0.21/0.30 % TRYING [5]
% 0.21/0.30 % (3688092) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3688085-3688092"...
% 0.21/0.30 % (3688096)Instruction limit reached!
% 0.21/0.30 % (3688096)------------------------------
% 0.21/0.30 % (3688096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (3688096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (3688096)CaDiCaL version: 2.1.3
% 0.21/0.30 % (3688096)Termination reason: Instruction limit
% 0.21/0.30 % (3688096)Termination phase: Saturation
% 0.21/0.30 % (3688096)Time elapsed: 0.048 s
% 0.21/0.30 % (3688096)Peak memory usage: 14 MB
% 0.21/0.30 % (3688096)Instructions burned: 161 (million)
% 0.21/0.30 % (3688094) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3688085-3688094"...
% 0.21/0.30 % TRYING [6]
% 0.21/0.30 % (3688092)...printing done.
% 0.21/0.30 % (3688092)Refutation found. Thanks to Tanya!
% 0.21/0.30 % SZS status Theorem for theBenchmark
% 0.21/0.30 % SZS output start Proof for theBenchmark
% See solution above
% 0.21/0.31 % (3688092)------------------------------
% 0.21/0.31 % (3688092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.31 % (3688092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.31 % (3688092)CaDiCaL version: 2.1.3
% 0.21/0.31 % (3688092)Termination reason: Refutation
% 0.21/0.31 % (3688092)Time elapsed: 0.047 s
% 0.21/0.31 % (3688092)Peak memory usage: 13 MB
% 0.21/0.31 % (3688092)Instructions burned: 88 (million)
% 0.21/0.31 % (3688085)Success in time 0.082 s
% 0.21/0.31 % Vampire exiting
%------------------------------------------------------------------------------