%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG067+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.20s 0.28s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 64
% Syntax : Number of formulae : 296 ( 58 unt; 60 def)
% Number of atoms : 1360 ( 731 equ)
% Maximal formula atoms : 125 ( 4 avg)
% Number of connectives : 1572 ( 508 ~; 654 |; 350 &)
% ( 60 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 85 ( 83 usr; 84 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 5 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(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(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,e0) = e0
& op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e0
& op(e0,e1) != e0 )
| ( op(e0,e0) = e2
& op(e2,e2) = e0
& op(e0,e2) != e0 )
| ( op(e0,e0) = e3
& op(e3,e3) = e0
& op(e0,e3) != e0 )
| ( op(e0,e0) = e4
& op(e4,e4) = e0
& op(e0,e4) != e0 )
| ( op(e1,e1) = e0
& op(e0,e0) = e1
& op(e1,e0) != e1 )
| ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e1,e1) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 )
| ( op(e1,e1) = e3
& op(e3,e3) = e1
& op(e1,e3) != e1 )
| ( op(e1,e1) = e4
& op(e4,e4) = e1
& op(e1,e4) != e1 )
| ( op(e2,e2) = e0
& op(e0,e0) = e2
& op(e2,e0) != e2 )
| ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != e2 )
| ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e2,e2) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 )
| ( op(e3,e3) = e0
& op(e0,e0) = e3
& op(e3,e0) != e3 )
| ( op(e3,e3) = e1
& op(e1,e1) = e3
& op(e3,e1) != e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e3
& op(e3,e2) != e3 )
| ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ( op(e3,e3) = e4
& op(e4,e4) = e3
& op(e3,e4) != e3 )
| ( op(e4,e4) = e0
& op(e0,e0) = e4
& op(e4,e0) != e4 )
| ( op(e4,e4) = e1
& op(e1,e1) = e4
& op(e4,e1) != e4 )
| ( op(e4,e4) = e2
& op(e2,e2) = e4
& op(e4,e2) != e4 )
| ( op(e4,e4) = e3
& op(e3,e3) = e4
& op(e4,e3) != e4 )
| ( op(e4,e4) = e4
& op(e4,e4) = e4
& op(e4,e4) != e4 ) ) ),
file('/export/starexec/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,e0) = e0
& op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e0
& op(e0,e1) != e0 )
| ( op(e0,e0) = e2
& op(e2,e2) = e0
& op(e0,e2) != e0 )
| ( op(e0,e0) = e3
& op(e3,e3) = e0
& op(e0,e3) != e0 )
| ( op(e0,e0) = e4
& op(e4,e4) = e0
& op(e0,e4) != e0 )
| ( op(e1,e1) = e0
& op(e0,e0) = e1
& op(e1,e0) != e1 )
| ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e1,e1) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 )
| ( op(e1,e1) = e3
& op(e3,e3) = e1
& op(e1,e3) != e1 )
| ( op(e1,e1) = e4
& op(e4,e4) = e1
& op(e1,e4) != e1 )
| ( op(e2,e2) = e0
& op(e0,e0) = e2
& op(e2,e0) != e2 )
| ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != e2 )
| ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e2,e2) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 )
| ( op(e3,e3) = e0
& op(e0,e0) = e3
& op(e3,e0) != e3 )
| ( op(e3,e3) = e1
& op(e1,e1) = e3
& op(e3,e1) != e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e3
& op(e3,e2) != e3 )
| ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ( op(e3,e3) = e4
& op(e4,e4) = e3
& op(e3,e4) != e3 )
| ( op(e4,e4) = e0
& op(e0,e0) = e4
& op(e4,e0) != e4 )
| ( op(e4,e4) = e1
& op(e1,e1) = e4
& op(e4,e1) != e4 )
| ( op(e4,e4) = e2
& op(e2,e2) = e4
& op(e4,e2) != e4 )
| ( op(e4,e4) = e3
& op(e3,e3) = e4
& op(e4,e3) != e4 )
| ( op(e4,e4) = e4
& op(e4,e4) = e4
& op(e4,e4) != e4 ) ) ),
inference(negated_conjecture,[status(cth)],[f7]) ).
fof(f9,plain,
( ( op(e0,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,e0) = e0
& op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e0
& op(e0,e1) != e0 )
| ( op(e0,e0) = e2
& op(e2,e2) = e0
& op(e0,e2) != e0 )
| ( op(e0,e0) = e3
& op(e3,e3) = e0
& op(e0,e3) != e0 )
| ( op(e0,e0) = e4
& op(e4,e4) = e0
& op(e0,e4) != e0 )
| ( op(e1,e1) = e0
& op(e0,e0) = e1
& op(e1,e0) != e1 )
| ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e1,e1) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 )
| ( op(e1,e1) = e3
& op(e3,e3) = e1
& op(e1,e3) != e1 )
| ( op(e1,e1) = e4
& op(e4,e4) = e1
& op(e1,e4) != e1 )
| ( op(e2,e2) = e0
& op(e0,e0) = e2
& op(e2,e0) != e2 )
| ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != e2 )
| ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e2,e2) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 )
| ( op(e3,e3) = e0
& op(e0,e0) = e3
& op(e3,e0) != e3 )
| ( op(e3,e3) = e1
& op(e1,e1) = e3
& op(e3,e1) != e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e3
& op(e3,e2) != e3 )
| ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ( op(e3,e3) = e4
& op(e4,e4) = e3
& op(e3,e4) != e3 )
| ( op(e4,e4) = e0
& op(e0,e0) = e4
& op(e4,e0) != e4 )
| ( op(e4,e4) = e1
& op(e1,e1) = e4
& op(e4,e1) != e4 )
| ( op(e4,e4) = e2
& op(e2,e2) = e4
& op(e4,e2) != e4 )
| ( op(e4,e4) = e3
& op(e3,e3) = e4
& op(e4,e3) != e4 )
| ( op(e4,e4) = e4
& op(e4,e4) = e4
& op(e4,e4) != e4 ) ) ),
inference(flattening,[],[f8]) ).
fof(f34,plain,
( e4 = op(e4,e4)
| e3 = op(e4,e4)
| e2 = op(e4,e4)
| e1 = op(e4,e4)
| e0 = op(e4,e4) ),
inference(cnf_transformation,[],[f1]) ).
fof(f97,plain,
op(e4,e2) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f117,plain,
op(e2,e2) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f147,plain,
op(e2,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f148,plain,
op(e2,e4) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f167,plain,
op(e2,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f169,plain,
op(e1,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f206,plain,
e3 = op(e2,e4),
inference(cnf_transformation,[],[f6]) ).
fof(f207,plain,
e1 = op(e4,e2),
inference(cnf_transformation,[],[f6]) ).
fof(f208,plain,
e0 = op(op(e4,e2),op(e4,e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f209,plain,
( e0 != op(e0,e0)
| ~ sP22 ),
inference(cnf_transformation,[],[f9]) ).
fof(f211,plain,
( e0 = op(e0,e0)
| ~ sP22 ),
inference(cnf_transformation,[],[f9]) ).
fof(f212,plain,
( e0 != op(e0,e1)
| ~ sP21 ),
inference(cnf_transformation,[],[f9]) ).
fof(f214,plain,
( op(e0,e0) = e1
| ~ sP21 ),
inference(cnf_transformation,[],[f9]) ).
fof(f215,plain,
( e0 != op(e0,e2)
| ~ sP20 ),
inference(cnf_transformation,[],[f9]) ).
fof(f217,plain,
( op(e0,e0) = e2
| ~ sP20 ),
inference(cnf_transformation,[],[f9]) ).
fof(f218,plain,
( e0 != op(e0,e3)
| ~ sP19 ),
inference(cnf_transformation,[],[f9]) ).
fof(f220,plain,
( op(e0,e0) = e3
| ~ sP19 ),
inference(cnf_transformation,[],[f9]) ).
fof(f221,plain,
( e0 != op(e0,e4)
| ~ sP18 ),
inference(cnf_transformation,[],[f9]) ).
fof(f223,plain,
( op(e0,e0) = e4
| ~ sP18 ),
inference(cnf_transformation,[],[f9]) ).
fof(f224,plain,
( e1 != op(e1,e0)
| ~ sP17 ),
inference(cnf_transformation,[],[f9]) ).
fof(f227,plain,
( e1 != op(e1,e1)
| ~ sP16 ),
inference(cnf_transformation,[],[f9]) ).
fof(f229,plain,
( e1 = op(e1,e1)
| ~ sP16 ),
inference(cnf_transformation,[],[f9]) ).
fof(f232,plain,
( e2 = op(e1,e1)
| ~ sP15 ),
inference(cnf_transformation,[],[f9]) ).
fof(f233,plain,
( e1 != op(e1,e3)
| ~ sP14 ),
inference(cnf_transformation,[],[f9]) ).
fof(f235,plain,
( e3 = op(e1,e1)
| ~ sP14 ),
inference(cnf_transformation,[],[f9]) ).
fof(f237,plain,
( e1 = op(e4,e4)
| ~ sP13 ),
inference(cnf_transformation,[],[f9]) ).
fof(f239,plain,
( e2 != op(e2,e0)
| ~ sP12 ),
inference(cnf_transformation,[],[f9]) ).
fof(f241,plain,
( e0 = op(e2,e2)
| ~ sP12 ),
inference(cnf_transformation,[],[f9]) ).
fof(f244,plain,
( e1 = op(e2,e2)
| ~ sP11 ),
inference(cnf_transformation,[],[f9]) ).
fof(f245,plain,
( e2 != op(e2,e2)
| ~ sP10 ),
inference(cnf_transformation,[],[f9]) ).
fof(f247,plain,
( e2 = op(e2,e2)
| ~ sP10 ),
inference(cnf_transformation,[],[f9]) ).
fof(f250,plain,
( e3 = op(e2,e2)
| ~ sP9 ),
inference(cnf_transformation,[],[f9]) ).
fof(f251,plain,
( e2 != op(e2,e4)
| ~ sP8 ),
inference(cnf_transformation,[],[f9]) ).
fof(f253,plain,
( e4 = op(e2,e2)
| ~ sP8 ),
inference(cnf_transformation,[],[f9]) ).
fof(f254,plain,
( e3 != op(e3,e0)
| ~ sP7 ),
inference(cnf_transformation,[],[f9]) ).
fof(f256,plain,
( e0 = op(e3,e3)
| ~ sP7 ),
inference(cnf_transformation,[],[f9]) ).
fof(f257,plain,
( e3 != op(e3,e1)
| ~ sP6 ),
inference(cnf_transformation,[],[f9]) ).
fof(f259,plain,
( e1 = op(e3,e3)
| ~ sP6 ),
inference(cnf_transformation,[],[f9]) ).
fof(f261,plain,
( e3 = op(e2,e2)
| ~ sP5 ),
inference(cnf_transformation,[],[f9]) ).
fof(f263,plain,
( e3 != op(e3,e3)
| ~ sP4 ),
inference(cnf_transformation,[],[f9]) ).
fof(f265,plain,
( e3 = op(e3,e3)
| ~ sP4 ),
inference(cnf_transformation,[],[f9]) ).
fof(f268,plain,
( e4 = op(e3,e3)
| ~ sP3 ),
inference(cnf_transformation,[],[f9]) ).
fof(f269,plain,
( e4 != op(e4,e0)
| ~ sP2 ),
inference(cnf_transformation,[],[f9]) ).
fof(f271,plain,
( e0 = op(e4,e4)
| ~ sP2 ),
inference(cnf_transformation,[],[f9]) ).
fof(f274,plain,
( e1 = op(e4,e4)
| ~ sP1 ),
inference(cnf_transformation,[],[f9]) ).
fof(f275,plain,
( e4 != op(e4,e2)
| ~ sP0 ),
inference(cnf_transformation,[],[f9]) ).
fof(f277,plain,
( e2 = op(e4,e4)
| ~ sP0 ),
inference(cnf_transformation,[],[f9]) ).
fof(f283,plain,
( e4 = op(e4,e4)
| e3 = op(e4,e4)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13
| sP14
| sP15
| sP16
| sP17
| sP18
| sP19
| sP20
| sP21
| sP22 ),
inference(cnf_transformation,[],[f9]) ).
fof(f286,plain,
( e4 != op(e4,e4)
| e3 = op(e4,e4)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13
| sP14
| sP15
| sP16
| sP17
| sP18
| sP19
| sP20
| sP21
| sP22 ),
inference(cnf_transformation,[],[f9]) ).
fof(f287,plain,
( e0 = op(e0,e1)
| op(e0,e0) != e1 ),
inference(cnf_transformation,[],[f9]) ).
fof(f288,plain,
( e0 = op(e0,e2)
| op(e0,e0) != e2 ),
inference(cnf_transformation,[],[f9]) ).
fof(f289,plain,
( e0 = op(e0,e3)
| op(e0,e0) != e3 ),
inference(cnf_transformation,[],[f9]) ).
fof(f290,plain,
( e0 = op(e0,e4)
| op(e0,e0) != e4 ),
inference(cnf_transformation,[],[f9]) ).
fof(f291,plain,
( e1 = op(e1,e0)
| e0 != op(e1,e1) ),
inference(cnf_transformation,[],[f9]) ).
fof(f292,plain,
( e1 = op(e1,e2)
| e2 != op(e1,e1) ),
inference(cnf_transformation,[],[f9]) ).
fof(f293,plain,
( e1 = op(e1,e3)
| e3 != op(e1,e1) ),
inference(cnf_transformation,[],[f9]) ).
fof(f295,plain,
( e2 = op(e2,e0)
| e0 != op(e2,e2) ),
inference(cnf_transformation,[],[f9]) ).
fof(f298,plain,
( e2 = op(e2,e4)
| e4 != op(e2,e2) ),
inference(cnf_transformation,[],[f9]) ).
fof(f299,plain,
( e3 = op(e3,e0)
| e0 != op(e3,e3) ),
inference(cnf_transformation,[],[f9]) ).
fof(f300,plain,
( e3 = op(e3,e1)
| e1 != op(e3,e3) ),
inference(cnf_transformation,[],[f9]) ).
fof(f302,plain,
( e3 = op(e3,e4)
| e4 != op(e3,e3) ),
inference(cnf_transformation,[],[f9]) ).
fof(f303,plain,
( e4 = op(e4,e0)
| e0 != op(e4,e4) ),
inference(cnf_transformation,[],[f9]) ).
fof(f305,plain,
( e4 = op(e4,e2)
| e2 != op(e4,e4) ),
inference(cnf_transformation,[],[f9]) ).
fof(f308,definition,
( spl23_1
<=> sP22 ),
introduced(definition,[new_symbols(definition,[spl23_1])],[avatar_definition]) ).
fof(f312,definition,
( spl23_2
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl23_2])],[avatar_definition]) ).
fof(f315,plain,
( ~ spl23_1
| ~ spl23_2 ),
inference(avatar_split_clause,[],[f209,f312,f308]) ).
fof(f317,plain,
( ~ spl23_1
| spl23_2 ),
inference(avatar_split_clause,[],[f211,f312,f308]) ).
fof(f319,definition,
( spl23_3
<=> sP21 ),
introduced(definition,[new_symbols(definition,[spl23_3])],[avatar_definition]) ).
fof(f323,definition,
( spl23_4
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl23_4])],[avatar_definition]) ).
fof(f326,plain,
( ~ spl23_3
| ~ spl23_4 ),
inference(avatar_split_clause,[],[f212,f323,f319]) ).
fof(f328,definition,
( spl23_5
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl23_5])],[avatar_definition]) ).
fof(f333,definition,
( spl23_6
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl23_6])],[avatar_definition]) ).
fof(f336,plain,
( ~ spl23_3
| spl23_6 ),
inference(avatar_split_clause,[],[f214,f333,f319]) ).
fof(f338,definition,
( spl23_7
<=> sP20 ),
introduced(definition,[new_symbols(definition,[spl23_7])],[avatar_definition]) ).
fof(f342,definition,
( spl23_8
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl23_8])],[avatar_definition]) ).
fof(f345,plain,
( ~ spl23_7
| ~ spl23_8 ),
inference(avatar_split_clause,[],[f215,f342,f338]) ).
fof(f347,definition,
( spl23_9
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl23_9])],[avatar_definition]) ).
fof(f352,definition,
( spl23_10
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl23_10])],[avatar_definition]) ).
fof(f355,plain,
( ~ spl23_7
| spl23_10 ),
inference(avatar_split_clause,[],[f217,f352,f338]) ).
fof(f357,definition,
( spl23_11
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl23_11])],[avatar_definition]) ).
fof(f361,definition,
( spl23_12
<=> e0 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl23_12])],[avatar_definition]) ).
fof(f364,plain,
( ~ spl23_11
| ~ spl23_12 ),
inference(avatar_split_clause,[],[f218,f361,f357]) ).
fof(f366,definition,
( spl23_13
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl23_13])],[avatar_definition]) ).
fof(f371,definition,
( spl23_14
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl23_14])],[avatar_definition]) ).
fof(f374,plain,
( ~ spl23_11
| spl23_14 ),
inference(avatar_split_clause,[],[f220,f371,f357]) ).
fof(f376,definition,
( spl23_15
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl23_15])],[avatar_definition]) ).
fof(f380,definition,
( spl23_16
<=> e0 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl23_16])],[avatar_definition]) ).
fof(f383,plain,
( ~ spl23_15
| ~ spl23_16 ),
inference(avatar_split_clause,[],[f221,f380,f376]) ).
fof(f385,definition,
( spl23_17
<=> e0 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl23_17])],[avatar_definition]) ).
fof(f390,definition,
( spl23_18
<=> op(e0,e0) = e4 ),
introduced(definition,[new_symbols(definition,[spl23_18])],[avatar_definition]) ).
fof(f393,plain,
( ~ spl23_15
| spl23_18 ),
inference(avatar_split_clause,[],[f223,f390,f376]) ).
fof(f395,definition,
( spl23_19
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl23_19])],[avatar_definition]) ).
fof(f399,definition,
( spl23_20
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl23_20])],[avatar_definition]) ).
fof(f402,plain,
( ~ spl23_19
| ~ spl23_20 ),
inference(avatar_split_clause,[],[f224,f399,f395]) ).
fof(f406,definition,
( spl23_21
<=> sP16 ),
introduced(definition,[new_symbols(definition,[spl23_21])],[avatar_definition]) ).
fof(f410,definition,
( spl23_22
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl23_22])],[avatar_definition]) ).
fof(f413,plain,
( ~ spl23_21
| ~ spl23_22 ),
inference(avatar_split_clause,[],[f227,f410,f406]) ).
fof(f415,plain,
( ~ spl23_21
| spl23_22 ),
inference(avatar_split_clause,[],[f229,f410,f406]) ).
fof(f417,definition,
( spl23_23
<=> sP15 ),
introduced(definition,[new_symbols(definition,[spl23_23])],[avatar_definition]) ).
fof(f421,definition,
( spl23_24
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl23_24])],[avatar_definition]) ).
fof(f426,definition,
( spl23_25
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl23_25])],[avatar_definition]) ).
fof(f431,definition,
( spl23_26
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl23_26])],[avatar_definition]) ).
fof(f434,plain,
( ~ spl23_23
| spl23_26 ),
inference(avatar_split_clause,[],[f232,f431,f417]) ).
fof(f436,definition,
( spl23_27
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl23_27])],[avatar_definition]) ).
fof(f440,definition,
( spl23_28
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl23_28])],[avatar_definition]) ).
fof(f443,plain,
( ~ spl23_27
| ~ spl23_28 ),
inference(avatar_split_clause,[],[f233,f440,f436]) ).
fof(f445,definition,
( spl23_29
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl23_29])],[avatar_definition]) ).
fof(f450,definition,
( spl23_30
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl23_30])],[avatar_definition]) ).
fof(f453,plain,
( ~ spl23_27
| spl23_30 ),
inference(avatar_split_clause,[],[f235,f450,f436]) ).
fof(f455,definition,
( spl23_31
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl23_31])],[avatar_definition]) ).
fof(f464,definition,
( spl23_33
<=> e1 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl23_33])],[avatar_definition]) ).
fof(f467,plain,
( ~ spl23_31
| spl23_33 ),
inference(avatar_split_clause,[],[f237,f464,f455]) ).
fof(f474,definition,
( spl23_35
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl23_35])],[avatar_definition]) ).
fof(f478,definition,
( spl23_36
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl23_36])],[avatar_definition]) ).
fof(f481,plain,
( ~ spl23_35
| ~ spl23_36 ),
inference(avatar_split_clause,[],[f239,f478,f474]) ).
fof(f483,plain,
( ~ spl23_35
| spl23_9 ),
inference(avatar_split_clause,[],[f241,f347,f474]) ).
fof(f485,definition,
( spl23_37
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl23_37])],[avatar_definition]) ).
fof(f494,plain,
( ~ spl23_37
| spl23_25 ),
inference(avatar_split_clause,[],[f244,f426,f485]) ).
fof(f496,definition,
( spl23_39
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl23_39])],[avatar_definition]) ).
fof(f500,definition,
( spl23_40
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl23_40])],[avatar_definition]) ).
fof(f503,plain,
( ~ spl23_39
| ~ spl23_40 ),
inference(avatar_split_clause,[],[f245,f500,f496]) ).
fof(f505,plain,
( ~ spl23_39
| spl23_40 ),
inference(avatar_split_clause,[],[f247,f500,f496]) ).
fof(f507,definition,
( spl23_41
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl23_41])],[avatar_definition]) ).
fof(f521,definition,
( spl23_44
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl23_44])],[avatar_definition]) ).
fof(f524,plain,
( ~ spl23_41
| spl23_44 ),
inference(avatar_split_clause,[],[f250,f521,f507]) ).
fof(f526,definition,
( spl23_45
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl23_45])],[avatar_definition]) ).
fof(f530,definition,
( spl23_46
<=> e2 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl23_46])],[avatar_definition]) ).
fof(f533,plain,
( ~ spl23_45
| ~ spl23_46 ),
inference(avatar_split_clause,[],[f251,f530,f526]) ).
fof(f535,definition,
( spl23_47
<=> e2 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl23_47])],[avatar_definition]) ).
fof(f540,definition,
( spl23_48
<=> e4 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl23_48])],[avatar_definition]) ).
fof(f543,plain,
( ~ spl23_45
| spl23_48 ),
inference(avatar_split_clause,[],[f253,f540,f526]) ).
fof(f545,definition,
( spl23_49
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl23_49])],[avatar_definition]) ).
fof(f549,definition,
( spl23_50
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl23_50])],[avatar_definition]) ).
fof(f552,plain,
( ~ spl23_49
| ~ spl23_50 ),
inference(avatar_split_clause,[],[f254,f549,f545]) ).
fof(f554,plain,
( ~ spl23_49
| spl23_13 ),
inference(avatar_split_clause,[],[f256,f366,f545]) ).
fof(f556,definition,
( spl23_51
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl23_51])],[avatar_definition]) ).
fof(f560,definition,
( spl23_52
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl23_52])],[avatar_definition]) ).
fof(f563,plain,
( ~ spl23_51
| ~ spl23_52 ),
inference(avatar_split_clause,[],[f257,f560,f556]) ).
fof(f565,plain,
( ~ spl23_51
| spl23_29 ),
inference(avatar_split_clause,[],[f259,f445,f556]) ).
fof(f567,definition,
( spl23_53
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl23_53])],[avatar_definition]) ).
fof(f575,plain,
( ~ spl23_53
| spl23_44 ),
inference(avatar_split_clause,[],[f261,f521,f567]) ).
fof(f578,definition,
( spl23_55
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl23_55])],[avatar_definition]) ).
fof(f582,definition,
( spl23_56
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl23_56])],[avatar_definition]) ).
fof(f585,plain,
( ~ spl23_55
| ~ spl23_56 ),
inference(avatar_split_clause,[],[f263,f582,f578]) ).
fof(f587,plain,
( ~ spl23_55
| spl23_56 ),
inference(avatar_split_clause,[],[f265,f582,f578]) ).
fof(f589,definition,
( spl23_57
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl23_57])],[avatar_definition]) ).
fof(f593,definition,
( spl23_58
<=> e3 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl23_58])],[avatar_definition]) ).
fof(f598,definition,
( spl23_59
<=> e3 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl23_59])],[avatar_definition]) ).
fof(f603,definition,
( spl23_60
<=> e4 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl23_60])],[avatar_definition]) ).
fof(f606,plain,
( ~ spl23_57
| spl23_60 ),
inference(avatar_split_clause,[],[f268,f603,f589]) ).
fof(f608,definition,
( spl23_61
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl23_61])],[avatar_definition]) ).
fof(f612,definition,
( spl23_62
<=> e4 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl23_62])],[avatar_definition]) ).
fof(f615,plain,
( ~ spl23_61
| ~ spl23_62 ),
inference(avatar_split_clause,[],[f269,f612,f608]) ).
fof(f617,plain,
( ~ spl23_61
| spl23_17 ),
inference(avatar_split_clause,[],[f271,f385,f608]) ).
fof(f619,definition,
( spl23_63
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl23_63])],[avatar_definition]) ).
fof(f628,plain,
( ~ spl23_63
| spl23_33 ),
inference(avatar_split_clause,[],[f274,f464,f619]) ).
fof(f630,definition,
( spl23_65
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl23_65])],[avatar_definition]) ).
fof(f634,definition,
( spl23_66
<=> e4 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl23_66])],[avatar_definition]) ).
fof(f637,plain,
( ~ spl23_65
| ~ spl23_66 ),
inference(avatar_split_clause,[],[f275,f634,f630]) ).
fof(f639,plain,
( ~ spl23_65
| spl23_47 ),
inference(avatar_split_clause,[],[f277,f535,f630]) ).
fof(f645,definition,
( spl23_68
<=> e4 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl23_68])],[avatar_definition]) ).
fof(f653,plain,
( spl23_1
| spl23_3
| spl23_7
| spl23_11
| spl23_15
| spl23_19
| spl23_21
| spl23_23
| spl23_27
| spl23_31
| spl23_35
| spl23_37
| spl23_39
| spl23_41
| spl23_45
| spl23_49
| spl23_51
| spl23_53
| spl23_55
| spl23_57
| spl23_61
| spl23_63
| spl23_65
| spl23_59
| spl23_68 ),
inference(avatar_split_clause,[],[f283,f645,f598,f630,f619,f608,f589,f578,f567,f556,f545,f526,f507,f496,f485,f474,f455,f436,f417,f406,f395,f376,f357,f338,f319,f308]) ).
fof(f656,plain,
( spl23_1
| spl23_3
| spl23_7
| spl23_11
| spl23_15
| spl23_19
| spl23_21
| spl23_23
| spl23_27
| spl23_31
| spl23_35
| spl23_37
| spl23_39
| spl23_41
| spl23_45
| spl23_49
| spl23_51
| spl23_53
| spl23_55
| spl23_57
| spl23_61
| spl23_63
| spl23_65
| spl23_59
| ~ spl23_68 ),
inference(avatar_split_clause,[],[f286,f645,f598,f630,f619,f608,f589,f578,f567,f556,f545,f526,f507,f496,f485,f474,f455,f436,f417,f406,f395,f376,f357,f338,f319,f308]) ).
fof(f657,plain,
( ~ spl23_6
| spl23_4 ),
inference(avatar_split_clause,[],[f287,f323,f333]) ).
fof(f658,plain,
( ~ spl23_10
| spl23_8 ),
inference(avatar_split_clause,[],[f288,f342,f352]) ).
fof(f659,plain,
( ~ spl23_14
| spl23_12 ),
inference(avatar_split_clause,[],[f289,f361,f371]) ).
fof(f660,plain,
( ~ spl23_18
| spl23_16 ),
inference(avatar_split_clause,[],[f290,f380,f390]) ).
fof(f661,plain,
( ~ spl23_5
| spl23_20 ),
inference(avatar_split_clause,[],[f291,f399,f328]) ).
fof(f662,plain,
( ~ spl23_26
| spl23_24 ),
inference(avatar_split_clause,[],[f292,f421,f431]) ).
fof(f663,plain,
( ~ spl23_30
| spl23_28 ),
inference(avatar_split_clause,[],[f293,f440,f450]) ).
fof(f665,plain,
( ~ spl23_9
| spl23_36 ),
inference(avatar_split_clause,[],[f295,f478,f347]) ).
fof(f668,plain,
( ~ spl23_48
| spl23_46 ),
inference(avatar_split_clause,[],[f298,f530,f540]) ).
fof(f669,plain,
( ~ spl23_13
| spl23_50 ),
inference(avatar_split_clause,[],[f299,f549,f366]) ).
fof(f670,plain,
( ~ spl23_29
| spl23_52 ),
inference(avatar_split_clause,[],[f300,f560,f445]) ).
fof(f672,plain,
( ~ spl23_60
| spl23_58 ),
inference(avatar_split_clause,[],[f302,f593,f603]) ).
fof(f673,plain,
( ~ spl23_17
| spl23_62 ),
inference(avatar_split_clause,[],[f303,f612,f385]) ).
fof(f675,plain,
( ~ spl23_47
| spl23_66 ),
inference(avatar_split_clause,[],[f305,f634,f535]) ).
fof(f677,plain,
e0 = op(e1,e1),
inference(forward_demodulation,[],[f208,f207]) ).
fof(f678,plain,
e1 != op(e4,e4),
inference(forward_demodulation,[],[f97,f207]) ).
fof(f683,plain,
e3 != op(e2,e2),
inference(forward_demodulation,[],[f117,f206]) ).
fof(f686,plain,
e3 != op(e4,e4),
inference(forward_demodulation,[],[f147,f206]) ).
fof(f687,plain,
e3 != op(e3,e4),
inference(forward_demodulation,[],[f148,f206]) ).
fof(f691,plain,
e1 != op(e2,e2),
inference(forward_demodulation,[],[f167,f207]) ).
fof(f692,plain,
e1 != op(e1,e2),
inference(forward_demodulation,[],[f169,f207]) ).
fof(f1071,plain,
( spl23_17
| spl23_33
| spl23_47
| spl23_59
| spl23_68 ),
inference(avatar_split_clause,[],[f34,f645,f598,f535,f464,f385]) ).
fof(f1072,plain,
spl23_5,
inference(avatar_split_clause,[],[f677,f328]) ).
fof(f1073,plain,
~ spl23_33,
inference(avatar_split_clause,[],[f678,f464]) ).
fof(f1078,plain,
~ spl23_44,
inference(avatar_split_clause,[],[f683,f521]) ).
fof(f1081,plain,
~ spl23_59,
inference(avatar_split_clause,[],[f686,f598]) ).
fof(f1082,plain,
~ spl23_58,
inference(avatar_split_clause,[],[f687,f593]) ).
fof(f1086,plain,
~ spl23_25,
inference(avatar_split_clause,[],[f691,f426]) ).
fof(f1087,plain,
~ spl23_24,
inference(avatar_split_clause,[],[f692,f421]) ).
cnf(s1,plain,
( ~ spl23_1
| ~ spl23_2 ),
inference(sat_conversion,[],[f315]) ).
cnf(s3,plain,
( ~ spl23_1
| spl23_2 ),
inference(sat_conversion,[],[f317]) ).
cnf(s4,plain,
( ~ spl23_3
| ~ spl23_4 ),
inference(sat_conversion,[],[f326]) ).
cnf(s6,plain,
( ~ spl23_3
| spl23_6 ),
inference(sat_conversion,[],[f336]) ).
cnf(s7,plain,
( ~ spl23_7
| ~ spl23_8 ),
inference(sat_conversion,[],[f345]) ).
cnf(s9,plain,
( ~ spl23_7
| spl23_10 ),
inference(sat_conversion,[],[f355]) ).
cnf(s10,plain,
( ~ spl23_11
| ~ spl23_12 ),
inference(sat_conversion,[],[f364]) ).
cnf(s12,plain,
( ~ spl23_11
| spl23_14 ),
inference(sat_conversion,[],[f374]) ).
cnf(s13,plain,
( ~ spl23_15
| ~ spl23_16 ),
inference(sat_conversion,[],[f383]) ).
cnf(s15,plain,
( ~ spl23_15
| spl23_18 ),
inference(sat_conversion,[],[f393]) ).
cnf(s16,plain,
( ~ spl23_19
| ~ spl23_20 ),
inference(sat_conversion,[],[f402]) ).
cnf(s19,plain,
( ~ spl23_21
| ~ spl23_22 ),
inference(sat_conversion,[],[f413]) ).
cnf(s21,plain,
( ~ spl23_21
| spl23_22 ),
inference(sat_conversion,[],[f415]) ).
cnf(s24,plain,
( ~ spl23_23
| spl23_26 ),
inference(sat_conversion,[],[f434]) ).
cnf(s25,plain,
( ~ spl23_27
| ~ spl23_28 ),
inference(sat_conversion,[],[f443]) ).
cnf(s27,plain,
( ~ spl23_27
| spl23_30 ),
inference(sat_conversion,[],[f453]) ).
cnf(s29,plain,
( ~ spl23_31
| spl23_33 ),
inference(sat_conversion,[],[f467]) ).
cnf(s31,plain,
( ~ spl23_35
| ~ spl23_36 ),
inference(sat_conversion,[],[f481]) ).
cnf(s33,plain,
( spl23_9
| ~ spl23_35 ),
inference(sat_conversion,[],[f483]) ).
cnf(s36,plain,
( spl23_25
| ~ spl23_37 ),
inference(sat_conversion,[],[f494]) ).
cnf(s37,plain,
( ~ spl23_39
| ~ spl23_40 ),
inference(sat_conversion,[],[f503]) ).
cnf(s39,plain,
( ~ spl23_39
| spl23_40 ),
inference(sat_conversion,[],[f505]) ).
cnf(s42,plain,
( ~ spl23_41
| spl23_44 ),
inference(sat_conversion,[],[f524]) ).
cnf(s43,plain,
( ~ spl23_45
| ~ spl23_46 ),
inference(sat_conversion,[],[f533]) ).
cnf(s45,plain,
( ~ spl23_45
| spl23_48 ),
inference(sat_conversion,[],[f543]) ).
cnf(s46,plain,
( ~ spl23_49
| ~ spl23_50 ),
inference(sat_conversion,[],[f552]) ).
cnf(s48,plain,
( spl23_13
| ~ spl23_49 ),
inference(sat_conversion,[],[f554]) ).
cnf(s49,plain,
( ~ spl23_51
| ~ spl23_52 ),
inference(sat_conversion,[],[f563]) ).
cnf(s51,plain,
( spl23_29
| ~ spl23_51 ),
inference(sat_conversion,[],[f565]) ).
cnf(s53,plain,
( spl23_44
| ~ spl23_53 ),
inference(sat_conversion,[],[f575]) ).
cnf(s55,plain,
( ~ spl23_55
| ~ spl23_56 ),
inference(sat_conversion,[],[f585]) ).
cnf(s57,plain,
( ~ spl23_55
| spl23_56 ),
inference(sat_conversion,[],[f587]) ).
cnf(s60,plain,
( ~ spl23_57
| spl23_60 ),
inference(sat_conversion,[],[f606]) ).
cnf(s61,plain,
( ~ spl23_61
| ~ spl23_62 ),
inference(sat_conversion,[],[f615]) ).
cnf(s63,plain,
( spl23_17
| ~ spl23_61 ),
inference(sat_conversion,[],[f617]) ).
cnf(s66,plain,
( spl23_33
| ~ spl23_63 ),
inference(sat_conversion,[],[f628]) ).
cnf(s67,plain,
( ~ spl23_65
| ~ spl23_66 ),
inference(sat_conversion,[],[f637]) ).
cnf(s69,plain,
( spl23_47
| ~ spl23_65 ),
inference(sat_conversion,[],[f639]) ).
cnf(s75,plain,
( spl23_1
| spl23_3
| spl23_7
| spl23_11
| spl23_15
| spl23_19
| spl23_21
| spl23_23
| spl23_27
| spl23_31
| spl23_35
| spl23_37
| spl23_39
| spl23_41
| spl23_45
| spl23_49
| spl23_51
| spl23_53
| spl23_55
| spl23_57
| spl23_59
| spl23_61
| spl23_63
| spl23_65
| spl23_68 ),
inference(sat_conversion,[],[f653]) ).
cnf(s78,plain,
( spl23_1
| spl23_3
| spl23_7
| spl23_11
| spl23_15
| spl23_19
| spl23_21
| spl23_23
| spl23_27
| spl23_31
| spl23_35
| spl23_37
| spl23_39
| spl23_41
| spl23_45
| spl23_49
| spl23_51
| spl23_53
| spl23_55
| spl23_57
| spl23_59
| spl23_61
| spl23_63
| spl23_65
| ~ spl23_68 ),
inference(sat_conversion,[],[f656]) ).
cnf(s79,plain,
( spl23_4
| ~ spl23_6 ),
inference(sat_conversion,[],[f657]) ).
cnf(s80,plain,
( spl23_8
| ~ spl23_10 ),
inference(sat_conversion,[],[f658]) ).
cnf(s81,plain,
( spl23_12
| ~ spl23_14 ),
inference(sat_conversion,[],[f659]) ).
cnf(s82,plain,
( spl23_16
| ~ spl23_18 ),
inference(sat_conversion,[],[f660]) ).
cnf(s83,plain,
( ~ spl23_5
| spl23_20 ),
inference(sat_conversion,[],[f661]) ).
cnf(s84,plain,
( spl23_24
| ~ spl23_26 ),
inference(sat_conversion,[],[f662]) ).
cnf(s85,plain,
( spl23_28
| ~ spl23_30 ),
inference(sat_conversion,[],[f663]) ).
cnf(s87,plain,
( ~ spl23_9
| spl23_36 ),
inference(sat_conversion,[],[f665]) ).
cnf(s90,plain,
( spl23_46
| ~ spl23_48 ),
inference(sat_conversion,[],[f668]) ).
cnf(s91,plain,
( ~ spl23_13
| spl23_50 ),
inference(sat_conversion,[],[f669]) ).
cnf(s92,plain,
( ~ spl23_29
| spl23_52 ),
inference(sat_conversion,[],[f670]) ).
cnf(s94,plain,
( spl23_58
| ~ spl23_60 ),
inference(sat_conversion,[],[f672]) ).
cnf(s95,plain,
( ~ spl23_17
| spl23_62 ),
inference(sat_conversion,[],[f673]) ).
cnf(s97,plain,
( ~ spl23_47
| spl23_66 ),
inference(sat_conversion,[],[f675]) ).
cnf(s152,plain,
( spl23_17
| spl23_33
| spl23_47
| spl23_59
| spl23_68 ),
inference(sat_conversion,[],[f1071]) ).
cnf(s153,plain,
spl23_5,
inference(sat_conversion,[],[f1072]) ).
cnf(s154,plain,
~ spl23_33,
inference(sat_conversion,[],[f1073]) ).
cnf(s159,plain,
~ spl23_44,
inference(sat_conversion,[],[f1078]) ).
cnf(s162,plain,
~ spl23_59,
inference(sat_conversion,[],[f1081]) ).
cnf(s163,plain,
~ spl23_58,
inference(sat_conversion,[],[f1082]) ).
cnf(s167,plain,
~ spl23_25,
inference(sat_conversion,[],[f1086]) ).
cnf(s168,plain,
~ spl23_24,
inference(sat_conversion,[],[f1087]) ).
cnf(s186,plain,
( spl23_17
| spl23_47
| spl23_68 ),
inference(rat,[],[s152,s162,s154]) ).
cnf(s212,plain,
~ spl23_60,
inference(rat,[],[s94,s163]) ).
cnf(s213,plain,
~ spl23_26,
inference(rat,[],[s84,s168]) ).
cnf(s214,plain,
spl23_20,
inference(rat,[],[s83,s153]) ).
cnf(s215,plain,
( spl23_1
| spl23_3
| spl23_7
| spl23_11
| spl23_15
| spl23_19
| spl23_21
| spl23_23
| spl23_27
| spl23_31
| spl23_35
| spl23_37
| spl23_39
| spl23_41
| spl23_45
| spl23_49
| spl23_51
| spl23_53
| spl23_55
| spl23_57
| spl23_61
| spl23_63
| spl23_65
| ~ spl23_68 ),
inference(rat,[],[s78,s162]) ).
cnf(s217,plain,
( spl23_1
| spl23_3
| spl23_7
| spl23_11
| spl23_15
| spl23_19
| spl23_21
| spl23_23
| spl23_27
| spl23_31
| spl23_35
| spl23_37
| spl23_39
| spl23_41
| spl23_45
| spl23_49
| spl23_51
| spl23_53
| spl23_55
| spl23_57
| spl23_61
| spl23_63
| spl23_65
| spl23_68 ),
inference(rat,[],[s75,s162]) ).
cnf(s221,plain,
~ spl23_63,
inference(rat,[],[s66,s154]) ).
cnf(s222,plain,
~ spl23_57,
inference(rat,[],[s60,s212]) ).
cnf(s223,plain,
~ spl23_53,
inference(rat,[],[s53,s159]) ).
cnf(s224,plain,
~ spl23_41,
inference(rat,[],[s42,s159]) ).
cnf(s225,plain,
~ spl23_37,
inference(rat,[],[s36,s167]) ).
cnf(s226,plain,
~ spl23_31,
inference(rat,[],[s29,s154]) ).
cnf(s227,plain,
~ spl23_23,
inference(rat,[],[s24,s213]) ).
cnf(s228,plain,
~ spl23_19,
inference(rat,[],[s16,s214]) ).
cnf(s229,plain,
( spl23_47
| spl23_55
| spl23_45
| spl23_39
| spl23_51
| spl23_27
| spl23_21
| spl23_17
| spl23_15
| spl23_49
| spl23_11
| spl23_35
| spl23_7
| spl23_3
| spl23_1 ),
inference(rat,[],[s215,s69,s186,s63,s228,s227,s226,s225,s224,s223,s222,s221]) ).
cnf(s230,plain,
( spl23_65
| spl23_55
| spl23_1
| spl23_3
| spl23_7
| spl23_11
| spl23_15
| spl23_35
| spl23_21
| spl23_27
| spl23_49
| spl23_51
| spl23_39
| spl23_61
| spl23_45 ),
inference(rat,[],[s215,s217,s221,s222,s223,s224,s225,s226,s227,s228]) ).
cnf(s231,plain,
( spl23_55
| spl23_45
| spl23_39
| spl23_51
| spl23_27
| spl23_21
| spl23_17
| spl23_15
| spl23_49
| spl23_11
| spl23_35
| spl23_7
| spl23_3
| spl23_1 ),
inference(rat,[],[s230,s67,s97,s229,s63]) ).
cnf(s232,plain,
~ spl23_55,
inference(rat,[],[s55,s57]) ).
cnf(s233,plain,
~ spl23_45,
inference(rat,[],[s90,s43,s45]) ).
cnf(s234,plain,
~ spl23_39,
inference(rat,[],[s37,s39]) ).
cnf(s235,plain,
~ spl23_51,
inference(rat,[],[s92,s49,s51]) ).
cnf(s236,plain,
~ spl23_27,
inference(rat,[],[s85,s25,s27]) ).
cnf(s237,plain,
~ spl23_21,
inference(rat,[],[s19,s21]) ).
cnf(s238,plain,
~ spl23_65,
inference(rat,[],[s97,s67,s69]) ).
cnf(s239,plain,
( spl23_15
| spl23_49
| spl23_1
| spl23_11
| spl23_35
| spl23_7
| spl23_3 ),
inference(rat,[],[s61,s95,s230,s231,s233,s236,s235,s237,s238,s234,s232]) ).
cnf(s241,plain,
~ spl23_49,
inference(rat,[],[s91,s46,s48]) ).
cnf(s242,plain,
~ spl23_15,
inference(rat,[],[s82,s13,s15]) ).
cnf(s243,plain,
~ spl23_11,
inference(rat,[],[s81,s10,s12]) ).
cnf(s244,plain,
~ spl23_35,
inference(rat,[],[s87,s31,s33]) ).
cnf(s245,plain,
~ spl23_7,
inference(rat,[],[s80,s7,s9]) ).
cnf(s246,plain,
~ spl23_3,
inference(rat,[],[s79,s4,s6]) ).
cnf(s247,plain,
spl23_1,
inference(rat,[],[s239,s244,s243,s242,s241,s245,s246]) ).
cnf(s248,plain,
spl23_2,
inference(rat,[],[s3,s247]) ).
cnf(s249,plain,
$false,
inference(rat,[],[s1,s248,s247]) ).
fof(f1121,plain,
$false,
inference(avatar_sat_refutation,[],[s249]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG067+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n018.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 19:26:55 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.28 % (3688499)Will run a generic schedule for satisfiability detection.
% 0.20/0.28 % (3688508)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2017276277:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.20/0.28 % (3688505)% WARNING: option uhcvi not known.
% 0.20/0.28 % (3688504)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2121883041_2999 on theBenchmark for (2999ds/0Mi)
% 0.20/0.28 % (3688505)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3880279648:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.20/0.28 % (3688508) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3688499-3688508"...
% 0.20/0.28 % (3688506)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1589900624:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.20/0.28 % (3688507)dis+10_1_sil=32000:sp=arity:random_seed=890617105:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.20/0.28 % (3688509)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2307804237:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.20/0.28 % (3688510)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=470109559:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.20/0.28 % (3688508)...printing done.
% 0.20/0.28 % (3688508)Refutation found. Thanks to Tanya!
% 0.20/0.28 % SZS status Theorem for theBenchmark
% 0.20/0.28 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/0.28 % (3688508)------------------------------
% 0.20/0.28 % (3688508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.28 % (3688508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.28 % (3688508)CaDiCaL version: 2.1.3
% 0.20/0.28 % (3688508)Termination reason: Refutation
% 0.20/0.28 % (3688508)Time elapsed: 0.009 s
% 0.20/0.28 % (3688508)Peak memory usage: 13 MB
% 0.20/0.28 % (3688508)Instructions burned: 34 (million)
% 0.20/0.28 % (3688499)Success in time 0.05 s
% 0.20/0.28 % Vampire exiting
%------------------------------------------------------------------------------