%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP011+4 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n005.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 11:28:02 AM UTC 2026
% Result : Theorem 69.41s 13.90s
% Output : Refutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 23
% Syntax : Number of formulae : 175 ( 19 unt; 13 def)
% Number of atoms : 525 ( 200 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 576 ( 226 ~; 276 |; 51 &)
% ( 19 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 16 ( 14 usr; 14 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 8 con; 0-5 aty)
% Number of variables : 218 ( 0 sgn 202 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Eho_2Enotfalse) ).
fof(f5,axiom,
! [X0] :
( s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Eho_2Ebool__cases__ax) ).
fof(f126,axiom,
! [X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
=> s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ENOT__F) ).
fof(f139,axiom,
( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) != s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
& s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) != s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2EBOOL__EQ__DISTINCT) ).
fof(f140,axiom,
! [X0] :
( ( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,X0)
<=> p(s(tyop_2Emin_2Ebool,X0)) )
& ( s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
<=> p(s(tyop_2Emin_2Ebool,X0)) )
& ( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,X0)
<=> ~ p(s(tyop_2Emin_2Ebool,X0)) )
& ( s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
<=> ~ p(s(tyop_2Emin_2Ebool,X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2EEQ__CLAUSES) ).
fof(f1222,axiom,
! [X0,X1,X2,X3,X4] :
( p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4))))
<=> ( ( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)
& s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) )
| ? [X5,X6] :
( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X5)))
& s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,X6)))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,X5))),s(X1,X6)))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eoption_2EOPTREL__def) ).
fof(f1230,axiom,
! [X0,X1,X2] :
( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X1))) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X2)))
<=> s(X0,X1) = s(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eoption_2ESOME__11) ).
fof(f1231,axiom,
! [X0,X1] : s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eoption_2ENOT__NONE__SOME) ).
fof(f1269,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ! [X6,X7] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X5),s(X0,X6))),s(X1,X7))))
=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X4),s(X0,X6))),s(X1,X7)))) )
=> ( p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X5),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X2))))
=> p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X4),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X2)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eoption_2EOPTREL__MONO) ).
fof(f12253,conjecture,
! [X0,X1,X2,X3] :
( s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0))) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
& s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X2))),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0))) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
& s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X1))))) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
& s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X2))),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X1))))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(X0,X2))),s(X0,X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Equotient__option_2EOPTION__REL__def) ).
fof(f12254,negated_conjecture,
~ ! [X0,X1,X2,X3] :
( s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0))) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
& s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X2))),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0))) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
& s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X1))))) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
& s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X2))),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X1))))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(X0,X2))),s(X0,X1))) ),
inference(negated_conjecture,[status(cth)],[f12253]) ).
fof(f12452,plain,
? [X0,X1,X2,X3] :
( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) != s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)))
| s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) != s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X2))),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)))
| s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) != s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X1)))))
| s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(X0,X2))),s(X0,X1))) != s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X2))),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X1))))) ),
inference(ennf_transformation,[],[f12254]) ).
fof(f12768,plain,
! [X0] :
( s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
| p(s(tyop_2Emin_2Ebool,X0)) ),
inference(ennf_transformation,[],[f126]) ).
fof(f12783,plain,
! [X0,X1,X2,X3,X4,X5] :
( p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X4),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X2))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X5),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X2))))
| ? [X6,X7] :
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X4),s(X0,X6))),s(X1,X7))))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X5),s(X0,X6))),s(X1,X7)))) ) ),
inference(ennf_transformation,[],[f1269]) ).
fof(f12784,plain,
! [X0,X1,X2,X3,X4,X5] :
( p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X4),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X2))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X5),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X2))))
| ? [X6,X7] :
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X4),s(X0,X6))),s(X1,X7))))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X5),s(X0,X6))),s(X1,X7)))) ) ),
inference(flattening,[],[f12783]) ).
fof(f14331,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) != s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0)))
| s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) != s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0)))
| s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) != s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))
| s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(sK81,sK83))),s(sK81,sK82))) != s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK81,sK82,sK83,sK84]),skolemize(X0,sK81),skolemize(X1,sK82),skolemize(X2,sK83),skolemize(X3,sK84)],[f12452]) ).
fof(f14845,plain,
! [X0] :
( ( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,X0)
| ~ p(s(tyop_2Emin_2Ebool,X0)) )
& ( p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,X0) != s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) )
& ( s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
| ~ p(s(tyop_2Emin_2Ebool,X0)) )
& ( p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,X0) != s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) )
& ( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,X0)
| p(s(tyop_2Emin_2Ebool,X0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,X0) != s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) )
& ( s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
| p(s(tyop_2Emin_2Ebool,X0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,X0) != s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ) ),
inference(nnf_transformation,[],[f140]) ).
fof(f14846,plain,
! [X0] :
( ( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,X0)
| ~ p(s(tyop_2Emin_2Ebool,X0)) )
& ( p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,X0) != s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) )
& ( s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
| ~ p(s(tyop_2Emin_2Ebool,X0)) )
& ( p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,X0) != s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) )
& ( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,X0)
| p(s(tyop_2Emin_2Ebool,X0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,X0) != s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) )
& ( s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
| p(s(tyop_2Emin_2Ebool,X0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,X0) != s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ) ),
inference(flattening,[],[f14845]) ).
fof(f14912,plain,
! [X0,X1,X2] :
( ( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X1))) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X2)))
| s(X0,X1) != s(X0,X2) )
& ( s(X0,X1) = s(X0,X2)
| s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X1))) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X2))) ) ),
inference(nnf_transformation,[],[f1230]) ).
fof(f14930,plain,
! [X0,X1,X2,X3,X4,X5] :
( p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X4),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X2))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X5),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X2))))
| ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X4),s(X0,sK315(X0,X1,X4,X5)))),s(X1,sK316(X0,X1,X4,X5)))))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X5),s(X0,sK315(X0,X1,X4,X5)))),s(X1,sK316(X0,X1,X4,X5))))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK315,sK316]),skolemize(X6,sK315(X0,X1,X4,X5)),skolemize(X7,sK316(X0,X1,X4,X5))],[f12784]) ).
fof(f14931,plain,
! [X0,X1,X2,X3,X4] :
( ( p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4))))
| ( ( s(tyop_2Eoption_2Eoption(X0),X3) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)
| s(tyop_2Eoption_2Eoption(X1),X4) != s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) )
& ! [X5,X6] :
( s(tyop_2Eoption_2Eoption(X0),X3) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X5)))
| s(tyop_2Eoption_2Eoption(X1),X4) != s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,X6)))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,X5))),s(X1,X6)))) ) ) )
& ( ( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)
& s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) )
| ? [X5,X6] :
( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X5)))
& s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,X6)))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,X5))),s(X1,X6)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4)))) ) ),
inference(nnf_transformation,[],[f1222]) ).
fof(f14932,plain,
! [X0,X1,X2,X3,X4] :
( ( p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4))))
| ( ( s(tyop_2Eoption_2Eoption(X0),X3) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)
| s(tyop_2Eoption_2Eoption(X1),X4) != s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) )
& ! [X5,X6] :
( s(tyop_2Eoption_2Eoption(X0),X3) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X5)))
| s(tyop_2Eoption_2Eoption(X1),X4) != s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,X6)))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,X5))),s(X1,X6)))) ) ) )
& ( ( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)
& s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) )
| ? [X5,X6] :
( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X5)))
& s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,X6)))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,X5))),s(X1,X6)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4)))) ) ),
inference(flattening,[],[f14931]) ).
fof(f14933,plain,
! [X0,X1,X2,X3,X4] :
( ( p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4))))
| ( ( s(tyop_2Eoption_2Eoption(X0),X3) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)
| s(tyop_2Eoption_2Eoption(X1),X4) != s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) )
& ! [X5,X6] :
( s(tyop_2Eoption_2Eoption(X0),X3) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X5)))
| s(tyop_2Eoption_2Eoption(X1),X4) != s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,X6)))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,X5))),s(X1,X6)))) ) ) )
& ( ( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)
& s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) )
| ? [X7,X8] :
( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X7)))
& s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,X8)))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,X7))),s(X1,X8)))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4)))) ) ),
inference(rectify,[],[f14932]) ).
fof(f14934,plain,
! [X0,X1,X2,X3,X4] :
( ( p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4))))
| ( ( s(tyop_2Eoption_2Eoption(X0),X3) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)
| s(tyop_2Eoption_2Eoption(X1),X4) != s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) )
& ! [X5,X6] :
( s(tyop_2Eoption_2Eoption(X0),X3) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X5)))
| s(tyop_2Eoption_2Eoption(X1),X4) != s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,X6)))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,X5))),s(X1,X6)))) ) ) )
& ( ( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)
& s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) )
| ( s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,sK317(X0,X1,X2,X3,X4))))
& s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,sK318(X0,X1,X2,X3,X4))))
& p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,sK317(X0,X1,X2,X3,X4)))),s(X1,sK318(X0,X1,X2,X3,X4))))) )
| ~ p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK317,sK318]),skolemize(X7,sK317(X0,X1,X2,X3,X4)),skolemize(X8,sK318(X0,X1,X2,X3,X4))],[f14933]) ).
fof(f17564,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) != s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0)))
| s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) != s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0)))
| s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) != s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))
| s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(sK81,sK83))),s(sK81,sK82))) != s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))) ),
inference(cnf_transformation,[],[f14331]) ).
fof(f18705,plain,
! [X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,X0) != s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ),
inference(cnf_transformation,[],[f14846]) ).
fof(f18710,plain,
! [X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) ),
inference(cnf_transformation,[],[f14846]) ).
fof(f18713,plain,
s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) != s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0),
inference(cnf_transformation,[],[f139]) ).
fof(f18776,plain,
! [X0] :
( s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ),
inference(cnf_transformation,[],[f5]) ).
fof(f18930,plain,
! [X0] :
( p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ),
inference(cnf_transformation,[],[f12768]) ).
fof(f18941,plain,
~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
inference(cnf_transformation,[],[f4]) ).
fof(f18957,plain,
! [X0,X1] : s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X1))) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),
inference(cnf_transformation,[],[f1231]) ).
fof(f18958,plain,
! [X2,X0,X1] :
( s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X1))) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X2)))
| s(X0,X1) = s(X0,X2) ),
inference(cnf_transformation,[],[f14912]) ).
fof(f18975,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X5),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X2))))
| p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X4),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X2))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X5),s(X0,sK315(X0,X1,X4,X5)))),s(X1,sK316(X0,X1,X4,X5))))) ),
inference(cnf_transformation,[],[f14930]) ).
fof(f18977,plain,
! [X2,X3,X0,X1,X4] :
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,sK317(X0,X1,X2,X3,X4)))),s(X1,sK318(X0,X1,X2,X3,X4)))))
| s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0)
| ~ p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4)))) ),
inference(cnf_transformation,[],[f14934]) ).
fof(f18978,plain,
! [X2,X3,X0,X1,X4] :
( ~ p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4))))
| s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,sK318(X0,X1,X2,X3,X4))))
| s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) ),
inference(cnf_transformation,[],[f14934]) ).
fof(f18979,plain,
! [X2,X3,X0,X1,X4] :
( ~ p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4))))
| s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,sK317(X0,X1,X2,X3,X4))))
| s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0) ),
inference(cnf_transformation,[],[f14934]) ).
fof(f18981,plain,
! [X2,X3,X0,X1,X4] :
( ~ p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4))))
| s(tyop_2Eoption_2Eoption(X1),X4) = s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,sK318(X0,X1,X2,X3,X4))))
| s(tyop_2Eoption_2Eoption(X0),X3) = s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0) ),
inference(cnf_transformation,[],[f14934]) ).
fof(f18983,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( s(tyop_2Eoption_2Eoption(X1),X4) != s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,X6)))
| s(tyop_2Eoption_2Eoption(X0),X3) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X5)))
| p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,X5))),s(X1,X6)))) ),
inference(cnf_transformation,[],[f14934]) ).
fof(f18984,plain,
! [X2,X3,X0,X1,X4] :
( s(tyop_2Eoption_2Eoption(X1),X4) != s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0)
| s(tyop_2Eoption_2Eoption(X0),X3) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)
| p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4)))) ),
inference(cnf_transformation,[],[f14934]) ).
fof(f25684,definition,
( spl2180_7
<=> ! [X0] : ~ p(s(tyop_2Emin_2Ebool,X0)) ),
introduced(definition,[new_symbols(definition,[spl2180_7])],[avatar_definition]) ).
fof(f25685,plain,
( ! [X0] : ~ p(s(tyop_2Emin_2Ebool,X0))
| ~ spl2180_7 ),
inference(avatar_component_clause,[],[f25684]) ).
fof(f25805,definition,
( spl2180_36
<=> s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(sK81,sK83))),s(sK81,sK82))) = s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))) ),
introduced(definition,[new_symbols(definition,[spl2180_36])],[avatar_definition]) ).
fof(f25807,plain,
( s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(sK81,sK83))),s(sK81,sK82))) != s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))
| spl2180_36 ),
inference(avatar_component_clause,[],[f25805]) ).
fof(f25809,definition,
( spl2180_37
<=> s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))) ),
introduced(definition,[new_symbols(definition,[spl2180_37])],[avatar_definition]) ).
fof(f25811,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) != s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))
| spl2180_37 ),
inference(avatar_component_clause,[],[f25809]) ).
fof(f25813,definition,
( spl2180_38
<=> s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0))) ),
introduced(definition,[new_symbols(definition,[spl2180_38])],[avatar_definition]) ).
fof(f25815,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) != s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0)))
| spl2180_38 ),
inference(avatar_component_clause,[],[f25813]) ).
fof(f25817,definition,
( spl2180_39
<=> s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0))) ),
introduced(definition,[new_symbols(definition,[spl2180_39])],[avatar_definition]) ).
fof(f25819,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) != s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0)))
| spl2180_39 ),
inference(avatar_component_clause,[],[f25817]) ).
fof(f25820,plain,
( ~ spl2180_36
| ~ spl2180_37
| ~ spl2180_38
| ~ spl2180_39 ),
inference(avatar_split_clause,[],[f17564,f25817,f25813,f25809,f25805]) ).
fof(f26591,plain,
! [X2,X3,X0,X1] :
( s(tyop_2Eoption_2Eoption(X0),X1) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0)
| p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool)),X3),s(tyop_2Eoption_2Eoption(X0),X1),s(tyop_2Eoption_2Eoption(X2),c_2Eoption_2ENONE_2E0)))) ),
inference(equality_resolution,[],[f18984]) ).
fof(f26593,plain,
! [X0,X1] :
( s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,X1)
| s(tyop_2Emin_2Ebool,X1) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ),
inference(superposition,[],[f18776,f18776]) ).
fof(f26627,plain,
! [X2,X3,X0,X1,X4,X5] :
( p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4))))
| p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X5),s(X0,sK315(X0,X1,X2,X5)))),s(X1,sK316(X0,X1,X2,X5)))))
| s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X5),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4))) ),
inference(resolution,[],[f18975,f18930]) ).
fof(f26629,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4))))
| s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X5),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4))) )
| ~ spl2180_7 ),
inference(forward_subsumption_resolution,[],[f26627,f25685]) ).
fof(f26630,plain,
( ! [X3,X0,X1,X4,X5] : s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X5),s(tyop_2Eoption_2Eoption(X0),X3),s(tyop_2Eoption_2Eoption(X1),X4)))
| ~ spl2180_7 ),
inference(forward_subsumption_resolution,[],[f26629,f25685]) ).
fof(f26717,plain,
( ! [X0] :
( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) != s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0)))
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) )
| spl2180_38 ),
inference(superposition,[],[f25815,f26593]) ).
fof(f26745,plain,
( ! [X0] :
( s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0)))
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) )
| spl2180_38 ),
inference(trivial_inequality_removal,[],[f26717]) ).
fof(f26765,plain,
( ! [X0] :
( s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) )
| ~ spl2180_7
| spl2180_38 ),
inference(forward_demodulation,[],[f26745,f26630]) ).
fof(f26766,plain,
( ! [X0] : s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
| ~ spl2180_7
| spl2180_38 ),
inference(duplicate_literal_removal,[],[f26765]) ).
fof(f26781,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) != s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
| ~ spl2180_7
| spl2180_38 ),
inference(superposition,[],[f25815,f26766]) ).
fof(f26799,plain,
( $false
| ~ spl2180_7
| spl2180_38 ),
inference(trivial_inequality_removal,[],[f26781]) ).
fof(f26800,plain,
( ~ spl2180_7
| spl2180_38 ),
inference(avatar_contradiction_clause,[],[f26799]) ).
fof(f26829,plain,
! [X2,X0,X1] : p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0)))),
inference(equality_resolution,[],[f26591]) ).
fof(f26835,plain,
! [X2,X0,X1] : s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0))),
inference(resolution,[],[f26829,f18710]) ).
fof(f26904,plain,
! [X2,X3,X0,X1,X4,X5] :
( s(tyop_2Eoption_2Eoption(X0),X1) != s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X2)))
| p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X3,tyop_2Emin_2Ebool)),X4),s(tyop_2Eoption_2Eoption(X0),X1),s(tyop_2Eoption_2Eoption(X3),c_2Eoption_2ESOME_2E1(s(X3,X5))))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X3,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X3,tyop_2Emin_2Ebool)),X4),s(X0,X2))),s(X3,X5)))) ),
inference(equality_resolution,[],[f18983]) ).
fof(f26915,plain,
! [X2,X3,X0,X1,X4] :
( p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ESOME_2E1(s(X0,X3))),s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ESOME_2E1(s(X1,X4))))))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(X0,X3))),s(X1,X4)))) ),
inference(equality_resolution,[],[f26904]) ).
fof(f27032,plain,
( ! [X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK318(sK81,sK81,sK84,c_2Eoption_2ESOME_2E1(s(sK81,sK83)),c_2Eoption_2ENONE_2E0))))
| s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83)))
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) )
| spl2180_38 ),
inference(superposition,[],[f18981,f26745]) ).
fof(f27060,plain,
( ! [X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK318(sK81,sK81,sK84,c_2Eoption_2ESOME_2E1(s(sK81,sK83)),c_2Eoption_2ENONE_2E0))))
| s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))) )
| spl2180_38 ),
inference(forward_subsumption_resolution,[],[f27032,f18705]) ).
fof(f27078,plain,
( ! [X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK318(sK81,sK81,sK84,c_2Eoption_2ESOME_2E1(s(sK81,sK83)),c_2Eoption_2ENONE_2E0)))) )
| spl2180_38 ),
inference(forward_subsumption_resolution,[],[f27060,f18957]) ).
fof(f27089,plain,
( ! [X0] : ~ p(s(tyop_2Emin_2Ebool,X0))
| spl2180_38 ),
inference(forward_subsumption_resolution,[],[f27078,f18957]) ).
fof(f27091,plain,
( spl2180_7
| spl2180_38 ),
inference(avatar_split_clause,[],[f27089,f25813,f25684]) ).
fof(f27092,plain,
( $false
| spl2180_39 ),
inference(forward_subsumption_resolution,[],[f25819,f26835]) ).
fof(f27093,plain,
spl2180_39,
inference(avatar_contradiction_clause,[],[f27092]) ).
fof(f27113,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) != s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(sK81,sK83))),s(sK81,sK82)))
| s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))
| spl2180_36 ),
inference(superposition,[],[f25807,f18776]) ).
fof(f27115,definition,
( spl2180_45
<=> s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))) ),
introduced(definition,[new_symbols(definition,[spl2180_45])],[avatar_definition]) ).
fof(f27116,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) != s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))
| spl2180_45 ),
inference(avatar_component_clause,[],[f27115]) ).
fof(f27117,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))
| ~ spl2180_45 ),
inference(avatar_component_clause,[],[f27115]) ).
fof(f27119,definition,
( spl2180_46
<=> s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(sK81,sK83))),s(sK81,sK82))) ),
introduced(definition,[new_symbols(definition,[spl2180_46])],[avatar_definition]) ).
fof(f27122,plain,
( spl2180_45
| ~ spl2180_46
| spl2180_36 ),
inference(avatar_split_clause,[],[f27113,f25805,f27119,f27115]) ).
fof(f27129,definition,
( spl2180_48
<=> ! [X0] :
( s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ) ),
introduced(definition,[new_symbols(definition,[spl2180_48])],[avatar_definition]) ).
fof(f27130,plain,
( ! [X0] :
( s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) )
| ~ spl2180_48 ),
inference(avatar_component_clause,[],[f27129]) ).
fof(f27132,definition,
( spl2180_49
<=> s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(sK81,sK83))),s(sK81,sK82))) ),
introduced(definition,[new_symbols(definition,[spl2180_49])],[avatar_definition]) ).
fof(f27133,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(sK81,sK83))),s(sK81,sK82)))
| ~ spl2180_49 ),
inference(avatar_component_clause,[],[f27132]) ).
fof(f27134,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) != s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(sK81,sK83))),s(sK81,sK82)))
| spl2180_49 ),
inference(avatar_component_clause,[],[f27132]) ).
fof(f27138,plain,
( ! [X0] :
( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) != s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) )
| spl2180_37 ),
inference(superposition,[],[f25811,f26593]) ).
fof(f27142,plain,
( ! [X0] :
( s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) )
| spl2180_37 ),
inference(trivial_inequality_removal,[],[f27138]) ).
fof(f27175,definition,
( spl2180_51
<=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(sK81,sK83))),s(sK81,sK82)))) ),
introduced(definition,[new_symbols(definition,[spl2180_51])],[avatar_definition]) ).
fof(f27176,plain,
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(sK81,sK83))),s(sK81,sK82))))
| ~ spl2180_51 ),
inference(avatar_component_clause,[],[f27175]) ).
fof(f27177,plain,
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(sK81,sK83))),s(sK81,sK82))))
| spl2180_51 ),
inference(avatar_component_clause,[],[f27175]) ).
fof(f27185,definition,
( spl2180_52
<=> s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK317(sK81,sK81,sK84,c_2Eoption_2ESOME_2E1(s(sK81,sK83)),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))) ),
introduced(definition,[new_symbols(definition,[spl2180_52])],[avatar_definition]) ).
fof(f27187,plain,
( s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK317(sK81,sK81,sK84,c_2Eoption_2ESOME_2E1(s(sK81,sK83)),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))))
| ~ spl2180_52 ),
inference(avatar_component_clause,[],[f27185]) ).
fof(f27190,definition,
( spl2180_53
<=> s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK318(sK81,sK81,sK84,c_2Eoption_2ESOME_2E1(s(sK81,sK83)),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))) ),
introduced(definition,[new_symbols(definition,[spl2180_53])],[avatar_definition]) ).
fof(f27192,plain,
( s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK318(sK81,sK81,sK84,c_2Eoption_2ESOME_2E1(s(sK81,sK83)),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))))
| ~ spl2180_53 ),
inference(avatar_component_clause,[],[f27190]) ).
fof(f27223,plain,
( ! [X2,X0,X1] :
( p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))))
| s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0))) )
| spl2180_37 ),
inference(superposition,[],[f26829,f27142]) ).
fof(f27243,plain,
( ! [X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK317(sK81,sK81,sK84,c_2Eoption_2ENONE_2E0,c_2Eoption_2ESOME_2E1(s(sK81,sK82))))))
| s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) )
| spl2180_37 ),
inference(superposition,[],[f18979,f27142]) ).
fof(f27269,plain,
( ! [X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK317(sK81,sK81,sK84,c_2Eoption_2ENONE_2E0,c_2Eoption_2ESOME_2E1(s(sK81,sK82))))))
| s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))) )
| spl2180_37 ),
inference(forward_subsumption_resolution,[],[f27243,f18705]) ).
fof(f27275,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
| p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))))
| spl2180_37 ),
inference(forward_demodulation,[],[f27223,f26835]) ).
fof(f27282,plain,
( ! [X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK317(sK81,sK81,sK84,c_2Eoption_2ENONE_2E0,c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))) )
| spl2180_37 ),
inference(forward_subsumption_resolution,[],[f27269,f18957]) ).
fof(f27288,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))))
| spl2180_37 ),
inference(forward_subsumption_resolution,[],[f27275,f18713]) ).
fof(f27289,plain,
( ! [X0] : ~ p(s(tyop_2Emin_2Ebool,X0))
| spl2180_37 ),
inference(forward_subsumption_resolution,[],[f27282,f18957]) ).
fof(f27296,plain,
( spl2180_7
| spl2180_37 ),
inference(avatar_split_clause,[],[f27289,f25809,f25684]) ).
fof(f27341,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(sK81,sK83))),s(sK81,sK82)))
| spl2180_51 ),
inference(resolution,[],[f27177,f18930]) ).
fof(f27350,plain,
( $false
| spl2180_49
| spl2180_51 ),
inference(forward_subsumption_resolution,[],[f27341,f27134]) ).
fof(f27351,plain,
( spl2180_49
| spl2180_51 ),
inference(avatar_contradiction_clause,[],[f27350]) ).
fof(f27386,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(sK81,sK83))),s(sK81,sK82)))
| ~ spl2180_51 ),
inference(resolution,[],[f27176,f18710]) ).
fof(f27394,plain,
( spl2180_46
| ~ spl2180_51 ),
inference(avatar_split_clause,[],[f27386,f27175,f27119]) ).
fof(f27451,plain,
( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(sK81,sK83))),s(sK81,sK82))))
| ~ spl2180_45 ),
inference(superposition,[],[f26915,f27117]) ).
fof(f27459,plain,
( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(sK81,sK83))),s(sK81,sK82))))
| ~ spl2180_45 ),
inference(forward_subsumption_resolution,[],[f27451,f18941]) ).
fof(f27464,plain,
( $false
| ~ spl2180_45
| ~ spl2180_51 ),
inference(forward_subsumption_resolution,[],[f27459,f27176]) ).
fof(f27465,plain,
( ~ spl2180_45
| ~ spl2180_51 ),
inference(avatar_contradiction_clause,[],[f27464]) ).
fof(f27493,plain,
( ! [X2,X0,X1] :
( p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))))
| s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2),s(tyop_2Eoption_2Eoption(X0),c_2Eoption_2ENONE_2E0),s(tyop_2Eoption_2Eoption(X1),c_2Eoption_2ENONE_2E0))) )
| ~ spl2180_48 ),
inference(superposition,[],[f26829,f27130]) ).
fof(f27516,plain,
( ! [X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK318(sK81,sK81,sK84,c_2Eoption_2ESOME_2E1(s(sK81,sK83)),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))))
| s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) )
| ~ spl2180_48 ),
inference(superposition,[],[f18978,f27130]) ).
fof(f27517,plain,
( ! [X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK317(sK81,sK81,sK84,c_2Eoption_2ESOME_2E1(s(sK81,sK83)),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))))
| s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) )
| ~ spl2180_48 ),
inference(superposition,[],[f18979,f27130]) ).
fof(f27555,plain,
( ! [X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK317(sK81,sK81,sK84,c_2Eoption_2ESOME_2E1(s(sK81,sK83)),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))))
| s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))) )
| ~ spl2180_48 ),
inference(forward_subsumption_resolution,[],[f27517,f18705]) ).
fof(f27556,plain,
( ! [X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK318(sK81,sK81,sK84,c_2Eoption_2ESOME_2E1(s(sK81,sK83)),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))))
| s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))) )
| ~ spl2180_48 ),
inference(forward_subsumption_resolution,[],[f27516,f18705]) ).
fof(f27564,definition,
( spl2180_59
<=> p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))) ),
introduced(definition,[new_symbols(definition,[spl2180_59])],[avatar_definition]) ).
fof(f27566,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))))
| ~ spl2180_59 ),
inference(avatar_component_clause,[],[f27564]) ).
fof(f27568,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
| p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))))
| ~ spl2180_48 ),
inference(forward_demodulation,[],[f27493,f26835]) ).
fof(f27573,plain,
( ! [X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK317(sK81,sK81,sK84,c_2Eoption_2ESOME_2E1(s(sK81,sK83)),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))) )
| ~ spl2180_48 ),
inference(forward_subsumption_resolution,[],[f27555,f18957]) ).
fof(f27574,plain,
( ! [X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK318(sK81,sK81,sK84,c_2Eoption_2ESOME_2E1(s(sK81,sK83)),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))) )
| ~ spl2180_48 ),
inference(forward_subsumption_resolution,[],[f27556,f18957]) ).
fof(f27576,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))))
| ~ spl2180_48 ),
inference(forward_subsumption_resolution,[],[f27568,f18713]) ).
fof(f27579,plain,
( spl2180_52
| spl2180_7
| ~ spl2180_48 ),
inference(avatar_split_clause,[],[f27573,f27129,f25684,f27185]) ).
fof(f27580,plain,
( spl2180_53
| spl2180_7
| ~ spl2180_48 ),
inference(avatar_split_clause,[],[f27574,f27129,f25684,f27190]) ).
fof(f27581,plain,
( spl2180_59
| ~ spl2180_48 ),
inference(avatar_split_clause,[],[f27576,f27129,f27564]) ).
fof(f27584,plain,
( ! [X0] :
( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) != s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) )
| spl2180_45 ),
inference(superposition,[],[f27116,f26593]) ).
fof(f27588,plain,
( ! [X0] :
( s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) )
| spl2180_45 ),
inference(trivial_inequality_removal,[],[f27584]) ).
fof(f28835,plain,
( ! [X0] :
( s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))) != s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,X0)))
| s(sK81,sK317(sK81,sK81,sK84,c_2Eoption_2ESOME_2E1(s(sK81,sK83)),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))) = s(sK81,X0) )
| ~ spl2180_52 ),
inference(superposition,[],[f18958,f27187]) ).
fof(f28836,plain,
( ! [X0] :
( s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))) != s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,X0)))
| s(sK81,sK318(sK81,sK81,sK84,c_2Eoption_2ESOME_2E1(s(sK81,sK83)),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))) = s(sK81,X0) )
| ~ spl2180_53 ),
inference(superposition,[],[f18958,f27192]) ).
fof(f28849,plain,
( s(sK81,sK83) = s(sK81,sK317(sK81,sK81,sK84,c_2Eoption_2ESOME_2E1(s(sK81,sK83)),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))
| ~ spl2180_52 ),
inference(equality_resolution,[],[f28835]) ).
fof(f28889,plain,
( s(sK81,sK82) = s(sK81,sK318(sK81,sK81,sK84,c_2Eoption_2ESOME_2E1(s(sK81,sK83)),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))
| ~ spl2180_53 ),
inference(equality_resolution,[],[f28836]) ).
fof(f28894,plain,
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(sK81,sK317(sK81,sK81,sK84,c_2Eoption_2ESOME_2E1(s(sK81,sK83)),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))),s(sK81,sK82))))
| s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ENONE_2E0) = s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))))
| ~ spl2180_53 ),
inference(superposition,[],[f18977,f28889]) ).
fof(f28917,plain,
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(sK81,sK317(sK81,sK81,sK84,c_2Eoption_2ESOME_2E1(s(sK81,sK83)),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))),s(sK81,sK82))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82))))))
| ~ spl2180_53 ),
inference(forward_subsumption_resolution,[],[f28894,f18957]) ).
fof(f28919,plain,
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(sK81,sK317(sK81,sK81,sK84,c_2Eoption_2ESOME_2E1(s(sK81,sK83)),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))),s(sK81,sK82))))
| ~ spl2180_53
| ~ spl2180_59 ),
inference(forward_subsumption_resolution,[],[f28917,f27566]) ).
fof(f28921,plain,
( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(sK81,sK83))),s(sK81,sK82))))
| ~ spl2180_52
| ~ spl2180_53
| ~ spl2180_59 ),
inference(forward_demodulation,[],[f28919,f28849]) ).
fof(f28923,plain,
( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| ~ spl2180_49
| ~ spl2180_52
| ~ spl2180_53
| ~ spl2180_59 ),
inference(forward_demodulation,[],[f28921,f27133]) ).
fof(f28926,plain,
( $false
| ~ spl2180_49
| ~ spl2180_52
| ~ spl2180_53
| ~ spl2180_59 ),
inference(forward_subsumption_resolution,[],[f28923,f18941]) ).
fof(f28927,plain,
( ~ spl2180_49
| ~ spl2180_52
| ~ spl2180_53
| ~ spl2180_59 ),
inference(avatar_contradiction_clause,[],[f28926]) ).
fof(f28947,plain,
( spl2180_48
| spl2180_45 ),
inference(avatar_split_clause,[],[f27588,f27115,f27129]) ).
fof(f28956,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) != s(tyop_2Emin_2Ebool,c_2Eoption_2EOPTREL_2E3(s(tyop_2Emin_2Efun(sK81,tyop_2Emin_2Efun(sK81,tyop_2Emin_2Ebool)),sK84),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK83))),s(tyop_2Eoption_2Eoption(sK81),c_2Eoption_2ESOME_2E1(s(sK81,sK82)))))
| spl2180_36
| ~ spl2180_49 ),
inference(forward_demodulation,[],[f25807,f27133]) ).
fof(f28961,plain,
( $false
| ~ spl2180_7
| ~ spl2180_48 ),
inference(forward_subsumption_resolution,[],[f27576,f25685]) ).
fof(f28962,plain,
( ~ spl2180_7
| ~ spl2180_48 ),
inference(avatar_contradiction_clause,[],[f28961]) ).
fof(f28966,plain,
( $false
| spl2180_36
| ~ spl2180_45
| ~ spl2180_49 ),
inference(forward_subsumption_resolution,[],[f28956,f27117]) ).
fof(f28967,plain,
( spl2180_36
| ~ spl2180_45
| ~ spl2180_49 ),
inference(avatar_contradiction_clause,[],[f28966]) ).
fof(f28973,plain,
( $false
| ~ spl2180_7
| spl2180_37 ),
inference(forward_subsumption_resolution,[],[f27288,f25685]) ).
fof(f28974,plain,
( ~ spl2180_7
| spl2180_37 ),
inference(avatar_contradiction_clause,[],[f28973]) ).
cnf(s34,plain,
( ~ spl2180_36
| ~ spl2180_37
| ~ spl2180_38
| ~ spl2180_39 ),
inference(sat_conversion,[],[f25820]) ).
cnf(s36,plain,
( ~ spl2180_7
| spl2180_38 ),
inference(sat_conversion,[],[f26800]) ).
cnf(s42,plain,
( spl2180_7
| spl2180_38 ),
inference(sat_conversion,[],[f27091]) ).
cnf(s43,plain,
spl2180_39,
inference(sat_conversion,[],[f27093]) ).
cnf(s44,plain,
( spl2180_36
| spl2180_45
| ~ spl2180_46 ),
inference(sat_conversion,[],[f27122]) ).
cnf(s59,plain,
( spl2180_7
| spl2180_37 ),
inference(sat_conversion,[],[f27296]) ).
cnf(s60,plain,
( spl2180_49
| spl2180_51 ),
inference(sat_conversion,[],[f27351]) ).
cnf(s64,plain,
( spl2180_46
| ~ spl2180_51 ),
inference(sat_conversion,[],[f27394]) ).
cnf(s65,plain,
( ~ spl2180_45
| ~ spl2180_51 ),
inference(sat_conversion,[],[f27465]) ).
cnf(s73,plain,
( spl2180_7
| ~ spl2180_48
| spl2180_52 ),
inference(sat_conversion,[],[f27579]) ).
cnf(s74,plain,
( spl2180_7
| ~ spl2180_48
| spl2180_53 ),
inference(sat_conversion,[],[f27580]) ).
cnf(s75,plain,
( ~ spl2180_48
| spl2180_59 ),
inference(sat_conversion,[],[f27581]) ).
cnf(s77,plain,
( ~ spl2180_49
| ~ spl2180_52
| ~ spl2180_53
| ~ spl2180_59 ),
inference(sat_conversion,[],[f28927]) ).
cnf(s85,plain,
( spl2180_45
| spl2180_48 ),
inference(sat_conversion,[],[f28947]) ).
cnf(s89,plain,
( ~ spl2180_7
| ~ spl2180_48 ),
inference(sat_conversion,[],[f28962]) ).
cnf(s91,plain,
( spl2180_36
| ~ spl2180_45
| ~ spl2180_49 ),
inference(sat_conversion,[],[f28967]) ).
cnf(s93,plain,
( ~ spl2180_7
| spl2180_37 ),
inference(sat_conversion,[],[f28974]) ).
cnf(s95,plain,
( ~ spl2180_36
| ~ spl2180_37
| ~ spl2180_38 ),
inference(rat,[],[s34,s43]) ).
cnf(s96,plain,
( spl2180_45
| spl2180_7 ),
inference(rat,[],[s60,s77,s64,s73,s74,s75,s44,s85,s95,s42,s59]) ).
cnf(s97,plain,
spl2180_7,
inference(rat,[],[s60,s91,s65,s96,s95,s42,s59]) ).
cnf(s99,plain,
spl2180_37,
inference(rat,[],[s93,s97]) ).
cnf(s101,plain,
~ spl2180_48,
inference(rat,[],[s89,s97]) ).
cnf(s102,plain,
spl2180_38,
inference(rat,[],[s36,s97]) ).
cnf(s104,plain,
spl2180_45,
inference(rat,[],[s85,s101]) ).
cnf(s105,plain,
~ spl2180_36,
inference(rat,[],[s95,s99,s102]) ).
cnf(s117,plain,
~ spl2180_51,
inference(rat,[],[s65,s104]) ).
cnf(s118,plain,
~ spl2180_49,
inference(rat,[],[s91,s105,s104]) ).
cnf(s119,plain,
$false,
inference(rat,[],[s60,s117,s118]) ).
fof(f28977,plain,
$false,
inference(avatar_sat_refutation,[],[s119]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP011+4 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.16/0.42 % Computer : n005.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Sun Sep 27 11:57:32 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.42 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.16/0.47 Running first-order theorem proving
% 0.16/0.47 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.70/7.04 % (3864668)Detected formulas, will run a generic FOF schedule.
% 21.70/7.04 % (3864678)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2869813010:s2a=on:i=139:gtg=position_2965 on theBenchmark for (2965ds/139Mi)
% 21.70/7.04 % (3864678)Instruction limit reached!
% 21.70/7.04 % (3864678)------------------------------
% 21.70/7.04 % (3864678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.70/7.04 % (3864678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.70/7.04 % (3864678)CaDiCaL version: 2.1.3
% 21.70/7.04 % (3864678)Termination reason: Instruction limit
% 21.70/7.04 % (3864678)Termination phase: Property scanning
% 21.70/7.04 % (3864678)Time elapsed: 0.054 s
% 21.70/7.04 % (3864678)Peak memory usage: 105 MB
% 21.70/7.04 % (3864678)Instructions burned: 141 (million)
% 21.70/7.04 % (3864674)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3708922891:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2965 on theBenchmark for (2965ds/134677Mi)
% 21.70/7.04 % (3864673)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2307599232:i=141193_2965 on theBenchmark for (2965ds/141193Mi)
% 21.70/7.04 % (3864675)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2636011030:i=141695:sd=1:nm=32:gsp=on:ss=included_2965 on theBenchmark for (2965ds/141695Mi)
% 21.70/7.04 % (3864676)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2326624566:i=109:sd=1:ins=1:gsp=on:ss=axioms_2965 on theBenchmark for (2965ds/109Mi)
% 21.70/7.04 % (3864677)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4057406110:i=119:av=off:ss=axioms_2965 on theBenchmark for (2965ds/119Mi)
% 21.70/7.04 % (3864679)dis-21_1_sil=8000:lcm=predicate:random_seed=3994934752:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2965 on theBenchmark for (2965ds/129Mi)
% 21.70/7.04 % (3864676)Instruction limit reached!
% 21.70/7.04 % (3864676)------------------------------
% 21.70/7.04 % (3864676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.70/7.04 % (3864676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.70/7.04 % (3864676)CaDiCaL version: 2.1.3
% 21.70/7.04 % (3864676)Termination reason: Instruction limit
% 21.70/7.04 % (3864676)Termination phase: SInE selection
% 21.70/7.04 % (3864676)Time elapsed: 0.095 s
% 21.70/7.04 % (3864676)Peak memory usage: 105 MB
% 21.70/7.04 % (3864676)Instructions burned: 110 (million)
% 21.70/7.04 % (3864677)Instruction limit reached!
% 21.70/7.04 % (3864677)------------------------------
% 21.70/7.04 % (3864677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.70/7.04 % (3864677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.70/7.04 % (3864677)CaDiCaL version: 2.1.3
% 21.70/7.04 % (3864677)Termination reason: Instruction limit
% 21.70/7.04 % (3864677)Termination phase: SInE selection
% 21.70/7.04 % (3864677)Time elapsed: 0.101 s
% 21.70/7.04 % (3864677)Peak memory usage: 105 MB
% 21.70/7.04 % (3864677)Instructions burned: 119 (million)
% 21.70/7.04 % (3864681)lrs+10_1_sil=8000:sp=occurrence:random_seed=1266439084:i=285:sd=3:ss=axioms:sgt=8_2962 on theBenchmark for (2962ds/285Mi)
% 21.70/7.04 % (3864679)Instruction limit reached!
% 21.70/7.04 % (3864679)------------------------------
% 21.70/7.04 % (3864679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.70/7.04 % (3864679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.70/7.04 % (3864679)CaDiCaL version: 2.1.3
% 21.70/7.04 % (3864679)Termination reason: Instruction limit
% 21.70/7.04 % (3864679)Termination phase: SInE selection
% 21.70/7.04 % (3864679)Time elapsed: 0.110 s
% 21.70/7.04 % (3864679)Peak memory usage: 105 MB
% 21.70/7.04 % (3864679)Instructions burned: 130 (million)
% 21.70/7.04 % (3864689)lrs+1011_1_sil=32000:sp=occurrence:random_seed=683202330:i=325:sd=1:ss=axioms:sgt=32_2961 on theBenchmark for (2961ds/325Mi)
% 21.70/7.04 % (3864681)Instruction limit reached!
% 21.70/7.04 % (3864681)------------------------------
% 21.70/7.04 % (3864681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.70/7.04 % (3864681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.70/7.04 % (3864681)CaDiCaL version: 2.1.3
% 21.70/7.04 % (3864681)Termination reason: Instruction limit
% 31.27/8.41 % (3864681)Termination phase: Property scanning
% 31.27/8.41 % (3864681)Time elapsed: 0.251 s
% 31.27/8.41 % (3864681)Peak memory usage: 111 MB
% 31.27/8.41 % (3864681)Instructions burned: 287 (million)
% 31.27/8.41 % (3864688)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1064631922:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2961 on theBenchmark for (2961ds/157Mi)
% 31.27/8.41 % (3864691)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2854689559:s2a=on:i=248:s2at=1.23:gtg=position_2961 on theBenchmark for (2961ds/248Mi)
% 31.27/8.41 % (3864688)Instruction limit reached!
% 31.27/8.41 % (3864688)------------------------------
% 31.27/8.41 % (3864688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.27/8.41 % (3864688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.27/8.41 % (3864688)CaDiCaL version: 2.1.3
% 31.27/8.41 % (3864688)Termination reason: Instruction limit
% 31.27/8.41 % (3864688)Termination phase: Property scanning
% 31.27/8.41 % (3864688)Time elapsed: 0.119 s
% 31.27/8.41 % (3864688)Peak memory usage: 105 MB
% 31.27/8.41 % (3864688)Instructions burned: 157 (million)
% 31.27/8.41 % (3864689)Instruction limit reached!
% 31.27/8.41 % (3864689)------------------------------
% 31.27/8.41 % (3864689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.27/8.41 % (3864689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.27/8.41 % (3864689)CaDiCaL version: 2.1.3
% 31.27/8.41 % (3864689)Termination reason: Instruction limit
% 31.27/8.41 % (3864689)Termination phase: Saturation
% 31.27/8.41 % (3864689)Time elapsed: 0.172 s
% 31.27/8.41 % (3864689)Peak memory usage: 113 MB
% 31.27/8.41 % (3864689)Instructions burned: 327 (million)
% 31.27/8.41 % (3864694)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1698968311:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2958 on theBenchmark for (2958ds/294Mi)
% 31.27/8.41 % (3864691)Instruction limit reached!
% 31.27/8.41 % (3864691)------------------------------
% 31.27/8.41 % (3864691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.27/8.41 % (3864691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.27/8.41 % (3864691)CaDiCaL version: 2.1.3
% 31.27/8.41 % (3864691)Termination reason: Instruction limit
% 31.27/8.41 % (3864691)Termination phase: Property scanning
% 31.27/8.41 % (3864691)Time elapsed: 0.197 s
% 31.27/8.41 % (3864691)Peak memory usage: 105 MB
% 31.27/8.41 % (3864691)Instructions burned: 248 (million)
% 31.27/8.41 % (3864696)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1141256563:i=2350_2957 on theBenchmark for (2957ds/2350Mi)
% 31.27/8.41 % (3864694)Instruction limit reached!
% 31.27/8.41 % (3864694)------------------------------
% 31.27/8.41 % (3864694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.27/8.41 % (3864694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.27/8.41 % (3864694)CaDiCaL version: 2.1.3
% 31.27/8.41 % (3864694)Termination reason: Instruction limit
% 31.27/8.41 % (3864694)Termination phase: Preprocessing 3
% 31.27/8.41 % (3864694)Time elapsed: 0.235 s
% 31.27/8.41 % (3864694)Peak memory usage: 110 MB
% 31.27/8.41 % (3864694)Instructions burned: 294 (million)
% 31.27/8.41 % (3864697)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=522250422:cts=off:i=113:fsr=off:ss=included:sgt=4_2957 on theBenchmark for (2957ds/113Mi)
% 31.27/8.41 % (3864699)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1501869904:i=127:av=off:fsr=off:sup=off_2956 on theBenchmark for (2956ds/127Mi)
% 31.27/8.41 % (3864697)Instruction limit reached!
% 31.27/8.41 % (3864697)------------------------------
% 31.27/8.41 % (3864697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.27/8.41 % (3864697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.27/8.41 % (3864697)CaDiCaL version: 2.1.3
% 31.27/8.41 % (3864697)Termination reason: Instruction limit
% 31.27/8.41 % (3864697)Termination phase: SInE selection
% 31.27/8.41 % (3864697)Time elapsed: 0.100 s
% 31.27/8.41 % (3864697)Peak memory usage: 105 MB
% 31.27/8.41 % (3864697)Instructions burned: 113 (million)
% 31.27/8.41 % (3864699)Instruction limit reached!
% 31.27/8.41 % (3864699)------------------------------
% 31.27/8.41 % (3864699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.27/8.41 % (3864699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.27/8.41 % (3864699)CaDiCaL version: 2.1.3
% 69.41/13.90 % (3864699)Termination reason: Instruction limit
% 69.41/13.90 % (3864699)Termination phase: Preprocessing 1
% 69.41/13.90 % (3864699)Time elapsed: 0.140 s
% 69.41/13.90 % (3864699)Peak memory usage: 109 MB
% 69.41/13.90 % (3864699)Instructions burned: 127 (million)
% 69.41/13.90 % (3864703)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4153150341:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2954 on theBenchmark for (2954ds/114Mi)
% 69.41/13.90 % (3864705)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1683767036:i=437:sd=1:aac=none:ss=included_2952 on theBenchmark for (2952ds/437Mi)
% 69.41/13.90 % (3864703)Instruction limit reached!
% 69.41/13.90 % (3864703)------------------------------
% 69.41/13.90 % (3864703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.41/13.90 % (3864703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.41/13.90 % (3864703)CaDiCaL version: 2.1.3
% 69.41/13.90 % (3864703)Termination reason: Instruction limit
% 69.41/13.90 % (3864703)Termination phase: Property scanning
% 69.41/13.90 % (3864703)Time elapsed: 0.087 s
% 69.41/13.90 % (3864703)Peak memory usage: 105 MB
% 69.41/13.90 % (3864703)Instructions burned: 114 (million)
% 69.41/13.90 % (3864704)lrs+10_1_sil=8000:sp=occurrence:random_seed=3896461539:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2953 on theBenchmark for (2953ds/907Mi)
% 69.41/13.90 % (3864708)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3316069060:i=5202:ss=axioms:sgt=16_2951 on theBenchmark for (2951ds/5202Mi)
% 69.41/13.90 % (3864705)Instruction limit reached!
% 69.41/13.90 % (3864705)------------------------------
% 69.41/13.90 % (3864705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.41/13.90 % (3864705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.41/13.90 % (3864705)CaDiCaL version: 2.1.3
% 69.41/13.90 % (3864705)Termination reason: Instruction limit
% 69.41/13.90 % (3864705)Termination phase: Saturation
% 69.41/13.90 % (3864705)Time elapsed: 0.390 s
% 69.41/13.90 % (3864705)Peak memory usage: 114 MB
% 69.41/13.90 % (3864705)Instructions burned: 438 (million)
% 69.41/13.90 % (3864711)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4218216786:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2947 on theBenchmark for (2947ds/134Mi)
% 69.41/13.90 % (3864696)Instruction limit reached!
% 69.41/13.90 % (3864696)------------------------------
% 69.41/13.90 % (3864696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.41/13.90 % (3864696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.41/13.90 % (3864696)CaDiCaL version: 2.1.3
% 69.41/13.90 % (3864696)Termination reason: Instruction limit
% 69.41/13.90 % (3864696)Termination phase: Property scanning
% 69.41/13.90 % (3864696)Time elapsed: 1.027 s
% 69.41/13.90 % (3864696)Peak memory usage: 152 MB
% 69.41/13.90 % (3864696)Instructions burned: 2351 (million)
% 69.41/13.90 % (3864711)Instruction limit reached!
% 69.41/13.90 % (3864711)------------------------------
% 69.41/13.90 % (3864711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.41/13.90 % (3864711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.41/13.90 % (3864711)CaDiCaL version: 2.1.3
% 69.41/13.90 % (3864711)Termination reason: Instruction limit
% 69.41/13.90 % (3864711)Termination phase: SInE selection
% 69.41/13.90 % (3864711)Time elapsed: 0.080 s
% 69.41/13.90 % (3864711)Peak memory usage: 105 MB
% 69.41/13.90 % (3864711)Instructions burned: 134 (million)
% 69.41/13.90 % (3864704)Instruction limit reached!
% 69.41/13.90 % (3864704)------------------------------
% 69.41/13.90 % (3864704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.41/13.90 % (3864704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.41/13.90 % (3864704)CaDiCaL version: 2.1.3
% 69.41/13.90 % (3864704)Termination reason: Instruction limit
% 69.41/13.90 % (3864704)Termination phase: Saturation
% 69.41/13.90 % (3864704)Time elapsed: 0.774 s
% 69.41/13.90 % (3864704)Peak memory usage: 118 MB
% 69.41/13.90 % (3864704)Instructions burned: 907 (million)
% 69.41/13.90 % (3864714)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=564658629:st=3:i=13193:sd=3:ss=axioms_2944 on theBenchmark for (2944ds/13193Mi)
% 69.41/13.90 % (3864713)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2228736041:st=8:i=592:sd=3:ep=RST:ss=axioms_2944 on theBenchmark for (2944ds/592Mi)
% 69.41/13.90 % (3864715)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2150108992:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2943 on theBenchmark for (2943ds/125Mi)
% 69.41/13.90 % (3864713)Instruction limit reached!
% 69.41/13.90 % (3864713)------------------------------
% 69.41/13.90 % (3864713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.41/13.90 % (3864713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.41/13.90 % (3864713)CaDiCaL version: 2.1.3
% 69.41/13.90 % (3864713)Termination reason: Instruction limit
% 69.41/13.90 % (3864713)Termination phase: Preprocessing 3
% 69.41/13.90 % (3864713)Time elapsed: 0.325 s
% 69.41/13.90 % (3864713)Peak memory usage: 113 MB
% 69.41/13.90 % (3864713)Instructions burned: 594 (million)
% 69.41/13.90 % (3864715)Instruction limit reached!
% 69.41/13.90 % (3864715)------------------------------
% 69.41/13.90 % (3864715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.41/13.90 % (3864715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.41/13.90 % (3864715)CaDiCaL version: 2.1.3
% 69.41/13.90 % (3864715)Termination reason: Instruction limit
% 69.41/13.90 % (3864715)Termination phase: Property scanning
% 69.41/13.90 % (3864715)Time elapsed: 0.098 s
% 69.41/13.90 % (3864715)Peak memory usage: 106 MB
% 69.41/13.90 % (3864715)Instructions burned: 126 (million)
% 69.41/13.90 % (3864719)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2079439308:i=134:gtgl=5:slsql=off:gtg=exists_sym_2939 on theBenchmark for (2939ds/134Mi)
% 69.41/13.90 % (3864719)Instruction limit reached!
% 69.41/13.90 % (3864719)------------------------------
% 69.41/13.90 % (3864719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.41/13.90 % (3864719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.41/13.90 % (3864719)CaDiCaL version: 2.1.3
% 69.41/13.90 % (3864719)Termination reason: Instruction limit
% 69.41/13.90 % (3864719)Termination phase: Property scanning
% 69.41/13.90 % (3864719)Time elapsed: 0.057 s
% 69.41/13.90 % (3864719)Peak memory usage: 105 MB
% 69.41/13.90 % (3864719)Instructions burned: 143 (million)
% 69.41/13.90 % (3864720)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4136598792:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2939 on theBenchmark for (2939ds/141Mi)
% 69.41/13.90 % (3864722)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3895956735:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2936 on theBenchmark for (2936ds/431Mi)
% 69.41/13.90 % (3864720)Instruction limit reached!
% 69.41/13.90 % (3864720)------------------------------
% 69.41/13.90 % (3864720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.41/13.90 % (3864720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.41/13.90 % (3864720)CaDiCaL version: 2.1.3
% 69.41/13.90 % (3864720)Termination reason: Instruction limit
% 69.41/13.90 % (3864720)Termination phase: SInE selection
% 69.41/13.90 % (3864720)Time elapsed: 0.126 s
% 69.41/13.90 % (3864720)Peak memory usage: 105 MB
% 69.41/13.90 % (3864720)Instructions burned: 141 (million)
% 69.41/13.90 % (3864725)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2251335493:i=6060:aac=none:ins=25_2934 on theBenchmark for (2934ds/6060Mi)
% 69.41/13.90 % (3864722)Instruction limit reached!
% 69.41/13.90 % (3864722)------------------------------
% 69.41/13.90 % (3864722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.41/13.90 % (3864722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.41/13.90 % (3864722)CaDiCaL version: 2.1.3
% 69.41/13.90 % (3864722)Termination reason: Instruction limit
% 69.41/13.90 % (3864722)Termination phase: Saturation
% 69.41/13.90 % (3864722)Time elapsed: 0.388 s
% 69.41/13.90 % (3864722)Peak memory usage: 113 MB
% 69.41/13.90 % (3864722)Instructions burned: 432 (million)
% 69.41/13.90 % (3864727)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1487897507:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2931 on theBenchmark for (2931ds/150Mi)
% 69.41/13.90 % (3864727)Instruction limit reached!
% 69.41/13.90 % (3864727)------------------------------
% 69.41/13.90 % (3864727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.41/13.90 % (3864727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.41/13.90 % (3864727)CaDiCaL version: 2.1.3
% 69.41/13.90 % (3864727)Termination reason: Instruction limit
% 69.41/13.90 % (3864727)Termination phase: SInE selection
% 69.41/13.90 % (3864727)Time elapsed: 0.135 s
% 69.41/13.90 % (3864727)Peak memory usage: 105 MB
% 69.41/13.90 % (3864727)Instructions burned: 151 (million)
% 69.41/13.90 % (3864729)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1257140778:i=14155:bd=all_2926 on theBenchmark for (2926ds/14155Mi)
% 69.41/13.90 % (3864708)Instruction limit reached!
% 69.41/13.90 % (3864708)------------------------------
% 69.41/13.90 % (3864708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.41/13.90 % (3864708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.41/13.90 % (3864708)CaDiCaL version: 2.1.3
% 69.41/13.90 % (3864708)Termination reason: Instruction limit
% 69.41/13.90 % (3864708)Termination phase: Saturation
% 69.41/13.90 % (3864708)Time elapsed: 3.430 s
% 69.41/13.90 % (3864708)Peak memory usage: 241 MB
% 69.41/13.90 % (3864708)Instructions burned: 5203 (million)
% 69.41/13.90 % (3864731)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=4168440136:i=667:av=off:fsr=off_2913 on theBenchmark for (2913ds/667Mi)
% 69.41/13.90 % (3864731)Instruction limit reached!
% 69.41/13.90 % (3864731)------------------------------
% 69.41/13.90 % (3864731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.41/13.90 % (3864731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.41/13.90 % (3864731)CaDiCaL version: 2.1.3
% 69.41/13.90 % (3864731)Termination reason: Instruction limit
% 69.41/13.90 % (3864731)Termination phase: NewCNF
% 69.41/13.90 % (3864731)Time elapsed: 0.398 s
% 69.41/13.90 % (3864731)Peak memory usage: 123 MB
% 69.41/13.90 % (3864731)Instructions burned: 669 (million)
% 69.41/13.90 % (3864733)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=194304099:s2a=on:i=185:s2at=1.8:fdi=4_2908 on theBenchmark for (2908ds/185Mi)
% 69.41/13.90 % (3864733)Instruction limit reached!
% 69.41/13.90 % (3864733)------------------------------
% 69.41/13.90 % (3864733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.41/13.90 % (3864733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.41/13.90 % (3864733)CaDiCaL version: 2.1.3
% 69.41/13.90 % (3864733)Termination reason: Instruction limit
% 69.41/13.90 % (3864733)Termination phase: SInE selection
% 69.41/13.90 % (3864733)Time elapsed: 0.100 s
% 69.41/13.90 % (3864733)Peak memory usage: 105 MB
% 69.41/13.90 % (3864733)Instructions burned: 187 (million)
% 69.41/13.90 % (3864735)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1374087115:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2905 on theBenchmark for (2905ds/193Mi)
% 69.41/13.90 % (3864735)Instruction limit reached!
% 69.41/13.90 % (3864735)------------------------------
% 69.41/13.90 % (3864735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.41/13.90 % (3864735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.41/13.90 % (3864735)CaDiCaL version: 2.1.3
% 69.41/13.90 % (3864735)Termination reason: Instruction limit
% 69.41/13.90 % (3864735)Termination phase: SInE selection
% 69.41/13.90 % (3864735)Time elapsed: 0.102 s
% 69.41/13.90 % (3864735)Peak memory usage: 105 MB
% 69.41/13.90 % (3864735)Instructions burned: 194 (million)
% 69.41/13.90 % (3864737)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=429838895:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2902 on theBenchmark for (2902ds/4850Mi)
% 69.41/13.90 % (3864725)Instruction limit reached!
% 69.41/13.90 % (3864725)------------------------------
% 69.41/13.90 % (3864725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.41/13.90 % (3864725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.41/13.90 % (3864725)CaDiCaL version: 2.1.3
% 69.41/13.90 % (3864725)Termination reason: Instruction limit
% 69.41/13.90 % (3864725)Termination phase: Saturation
% 69.41/13.90 % (3864725)Time elapsed: 4.694 s
% 69.41/13.90 % (3864725)Peak memory usage: 154 MB
% 69.41/13.90 % (3864725)Instructions burned: 6060 (million)
% 69.41/13.90 % (3864739)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=4238877158:i=12111:sd=1:ss=included_2885 on theBenchmark for (2885ds/12111Mi)
% 69.41/13.90 % (3864714)First to succeed.
% 69.41/13.90 % (3864714)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3864668"
% 69.41/13.90 % (3864714)Refutation found. Thanks to Tanya!
% 69.41/13.90 % SZS status Theorem for theBenchmark
% 69.41/13.90 % SZS output start Proof for theBenchmark
% See solution above
% 0.23/14.14 % (3864714)------------------------------
% 0.23/14.14 % (3864714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.23/14.14 % (3864714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/14.14 % (3864714)CaDiCaL version: 2.1.3
% 0.23/14.14 % (3864714)Termination reason: Refutation
% 0.23/14.14 % (3864714)Time elapsed: 6.614 s
% 0.23/14.14 % (3864714)Peak memory usage: 310 MB
% 0.23/14.14 % (3864714)Instructions burned: 7061 (million)
% 0.23/14.14 % (3864714)------------------------------
% 0.23/14.14 % (3864714)------------------------------
% 0.23/14.14 % (3864668)Success in time 12.842 s
% 0.23/14.14 % Vampire exiting
%------------------------------------------------------------------------------