%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP021+1 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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:35:53 AM UTC 2026
% Result : Theorem 11.66s 3.80s
% Output : Refutation 11.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 27
% Syntax : Number of formulae : 183 ( 27 unt; 16 def)
% Number of atoms : 461 ( 61 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 462 ( 184 ~; 233 |; 14 &)
% ( 28 <=>; 2 =>; 0 <=; 1 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 21 ( 19 usr; 17 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 7 con; 0-3 aty)
% Number of variables : 115 ( 0 sgn 112 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',reserved_2Eho_2Ebool__cases__ax) ).
fof(f27,axiom,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2ETRUTH) ).
fof(f36,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/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2EEQ__CLAUSES) ).
fof(f37,axiom,
! [X0,X1,X2] :
( s(X0,c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0),s(X0,X1),s(X0,X2))) = s(X0,X1)
& s(X0,c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0),s(X0,X1),s(X0,X2))) = s(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2ECOND__CLAUSES) ).
fof(f41,axiom,
! [X0,X1,X2] :
( ( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))))
& p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2)))) )
=> p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X2)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eextreal_2Ele__trans) ).
fof(f42,axiom,
! [X0,X1] :
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X0)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eextreal_2Ele__total) ).
fof(f43,axiom,
! [X0,X1] : s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))) = s(tyop_2Eextreal_2Eextreal,c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))),s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X0))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eextreal_2Eextreal__max__def) ).
fof(f51,axiom,
! [X0,X1,X2] :
( ( p(s(tyop_2Emin_2Ebool,X2))
<=> ( p(s(tyop_2Emin_2Ebool,X1))
| p(s(tyop_2Emin_2Ebool,X0)) ) )
<=> ( ( p(s(tyop_2Emin_2Ebool,X2))
| ~ p(s(tyop_2Emin_2Ebool,X1)) )
& ( p(s(tyop_2Emin_2Ebool,X2))
| ~ p(s(tyop_2Emin_2Ebool,X0)) )
& ( p(s(tyop_2Emin_2Ebool,X1))
| p(s(tyop_2Emin_2Ebool,X0))
| ~ p(s(tyop_2Emin_2Ebool,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Esat_2Edc__disj) ).
fof(f52,axiom,
! [X0,X1,X2] :
( ( p(s(tyop_2Emin_2Ebool,X2))
<=> ( p(s(tyop_2Emin_2Ebool,X1))
=> p(s(tyop_2Emin_2Ebool,X0)) ) )
<=> ( ( p(s(tyop_2Emin_2Ebool,X2))
| p(s(tyop_2Emin_2Ebool,X1)) )
& ( p(s(tyop_2Emin_2Ebool,X2))
| ~ p(s(tyop_2Emin_2Ebool,X0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,X1))
| p(s(tyop_2Emin_2Ebool,X0))
| ~ p(s(tyop_2Emin_2Ebool,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Esat_2Edc__imp) ).
fof(f54,conjecture,
! [X0,X1,X2] :
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2))),s(tyop_2Eextreal_2Eextreal,X0))))
<=> ( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X0))))
& p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X2),s(tyop_2Eextreal_2Eextreal,X0)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eextreal_2Emax__le) ).
fof(f55,negated_conjecture,
~ ! [X0,X1,X2] :
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2))),s(tyop_2Eextreal_2Eextreal,X0))))
<=> ( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X0))))
& p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X2),s(tyop_2Eextreal_2Eextreal,X0)))) ) ),
inference(negated_conjecture,[status(cth)],[f54]) ).
fof(f68,plain,
! [X0,X1,X2] :
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X2))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2)))) ),
inference(ennf_transformation,[],[f41]) ).
fof(f69,plain,
! [X0,X1,X2] :
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X2))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2)))) ),
inference(flattening,[],[f68]) ).
fof(f78,plain,
! [X0,X1,X2] :
( ( p(s(tyop_2Emin_2Ebool,X2))
<=> ( p(s(tyop_2Emin_2Ebool,X0))
| ~ p(s(tyop_2Emin_2Ebool,X1)) ) )
<=> ( ( p(s(tyop_2Emin_2Ebool,X2))
| p(s(tyop_2Emin_2Ebool,X1)) )
& ( p(s(tyop_2Emin_2Ebool,X2))
| ~ p(s(tyop_2Emin_2Ebool,X0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,X1))
| p(s(tyop_2Emin_2Ebool,X0))
| ~ p(s(tyop_2Emin_2Ebool,X2)) ) ) ),
inference(ennf_transformation,[],[f52]) ).
fof(f79,plain,
? [X0,X1,X2] :
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2))),s(tyop_2Eextreal_2Eextreal,X0))))
<~> ( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X0))))
& p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X2),s(tyop_2Eextreal_2Eextreal,X0)))) ) ),
inference(ennf_transformation,[],[f55]) ).
fof(f84,plain,
~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
inference(cnf_transformation,[],[f4]) ).
fof(f85,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_2ET_2E0) ),
inference(cnf_transformation,[],[f5]) ).
fof(f125,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
inference(cnf_transformation,[],[f27]) ).
fof(f144,plain,
! [X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) ),
inference(cnf_transformation,[],[f36]) ).
fof(f145,plain,
! [X0] :
( p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,X0) != s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) ),
inference(cnf_transformation,[],[f36]) ).
fof(f148,plain,
! [X0] :
( p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ),
inference(cnf_transformation,[],[f36]) ).
fof(f149,plain,
! [X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,X0) != s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ),
inference(cnf_transformation,[],[f36]) ).
fof(f150,plain,
! [X2,X0,X1] : s(X0,X2) = s(X0,c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0),s(X0,X1),s(X0,X2))),
inference(cnf_transformation,[],[f37]) ).
fof(f151,plain,
! [X2,X0,X1] : s(X0,X1) = s(X0,c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0),s(X0,X1),s(X0,X2))),
inference(cnf_transformation,[],[f37]) ).
fof(f152,plain,
! [X2,X0,X1] :
( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X2)))) ),
inference(cnf_transformation,[],[f69]) ).
fof(f153,plain,
! [X0,X1] :
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X0))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1)))) ),
inference(cnf_transformation,[],[f42]) ).
fof(f154,plain,
! [X0,X1] : s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))) = s(tyop_2Eextreal_2Eextreal,c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))),s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X0))),
inference(cnf_transformation,[],[f43]) ).
fof(f181,plain,
! [X2,X0] :
( p(s(tyop_2Emin_2Ebool,X0))
| sP5(X2,X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f183,plain,
! [X2,X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| p(s(tyop_2Emin_2Ebool,X2))
| ~ sP5(X2,X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f199,plain,
! [X2,X0] :
( p(s(tyop_2Emin_2Ebool,X0))
| sP7(X2,X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f201,plain,
! [X2,X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| p(s(tyop_2Emin_2Ebool,X2))
| ~ sP7(X2,X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f214,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK11),s(tyop_2Eextreal_2Eextreal,sK9))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK9))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))),s(tyop_2Eextreal_2Eextreal,sK9)))) ),
inference(cnf_transformation,[],[f79]) ).
fof(f215,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK11),s(tyop_2Eextreal_2Eextreal,sK9))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))),s(tyop_2Eextreal_2Eextreal,sK9)))) ),
inference(cnf_transformation,[],[f79]) ).
fof(f216,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK9))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))),s(tyop_2Eextreal_2Eextreal,sK9)))) ),
inference(cnf_transformation,[],[f79]) ).
fof(f220,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)),
inference(consistent_polarity_flipping,[],[f84]) ).
fof(f251,plain,
~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
inference(consistent_polarity_flipping,[],[f125]) ).
fof(f268,plain,
! [X0] :
( s(tyop_2Emin_2Ebool,X0) != s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
| p(s(tyop_2Emin_2Ebool,X0)) ),
inference(consistent_polarity_flipping,[],[f149]) ).
fof(f269,plain,
! [X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f272,plain,
! [X0] :
( s(tyop_2Emin_2Ebool,X0) != s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
| ~ p(s(tyop_2Emin_2Ebool,X0)) ),
inference(consistent_polarity_flipping,[],[f145]) ).
fof(f273,plain,
! [X0] :
( p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) ),
inference(consistent_polarity_flipping,[],[f144]) ).
fof(f276,plain,
! [X2,X0,X1] :
( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X2))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X2)))) ),
inference(consistent_polarity_flipping,[],[f152]) ).
fof(f277,plain,
! [X0,X1] :
( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X0)))) ),
inference(consistent_polarity_flipping,[],[f153]) ).
fof(f313,plain,
! [X2,X0] :
( ~ p(s(tyop_2Emin_2Ebool,X2))
| p(s(tyop_2Emin_2Ebool,X0))
| sP5(X2,X0) ),
inference(consistent_polarity_flipping,[],[f183]) ).
fof(f315,plain,
! [X2,X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| ~ sP5(X2,X0) ),
inference(consistent_polarity_flipping,[],[f181]) ).
fof(f331,plain,
! [X2,X0] :
( ~ p(s(tyop_2Emin_2Ebool,X2))
| p(s(tyop_2Emin_2Ebool,X0))
| sP7(X2,X0) ),
inference(consistent_polarity_flipping,[],[f201]) ).
fof(f333,plain,
! [X2,X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| ~ sP7(X2,X0) ),
inference(consistent_polarity_flipping,[],[f199]) ).
fof(f337,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK9))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))),s(tyop_2Eextreal_2Eextreal,sK9)))) ),
inference(consistent_polarity_flipping,[],[f216]) ).
fof(f338,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK11),s(tyop_2Eextreal_2Eextreal,sK9))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))),s(tyop_2Eextreal_2Eextreal,sK9)))) ),
inference(consistent_polarity_flipping,[],[f215]) ).
fof(f339,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK11),s(tyop_2Eextreal_2Eextreal,sK9))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK9))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))),s(tyop_2Eextreal_2Eextreal,sK9)))) ),
inference(consistent_polarity_flipping,[],[f214]) ).
fof(f341,definition,
( spl12_1
<=> p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))),s(tyop_2Eextreal_2Eextreal,sK9)))) ),
introduced(definition,[new_symbols(definition,[spl12_1])],[avatar_definition]) ).
fof(f342,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))),s(tyop_2Eextreal_2Eextreal,sK9))))
| spl12_1 ),
inference(avatar_component_clause,[],[f341]) ).
fof(f343,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))),s(tyop_2Eextreal_2Eextreal,sK9))))
| ~ spl12_1 ),
inference(avatar_component_clause,[],[f341]) ).
fof(f345,definition,
( spl12_2
<=> p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK9)))) ),
introduced(definition,[new_symbols(definition,[spl12_2])],[avatar_definition]) ).
fof(f346,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK9))))
| spl12_2 ),
inference(avatar_component_clause,[],[f345]) ).
fof(f347,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK9))))
| ~ spl12_2 ),
inference(avatar_component_clause,[],[f345]) ).
fof(f349,definition,
( spl12_3
<=> p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK11),s(tyop_2Eextreal_2Eextreal,sK9)))) ),
introduced(definition,[new_symbols(definition,[spl12_3])],[avatar_definition]) ).
fof(f350,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK11),s(tyop_2Eextreal_2Eextreal,sK9))))
| spl12_3 ),
inference(avatar_component_clause,[],[f349]) ).
fof(f351,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK11),s(tyop_2Eextreal_2Eextreal,sK9))))
| ~ spl12_3 ),
inference(avatar_component_clause,[],[f349]) ).
fof(f352,plain,
( spl12_1
| spl12_2
| spl12_3 ),
inference(avatar_split_clause,[],[f339,f349,f345,f341]) ).
fof(f353,plain,
( ~ spl12_1
| ~ spl12_3 ),
inference(avatar_split_clause,[],[f338,f349,f341]) ).
fof(f354,plain,
( ~ spl12_1
| ~ spl12_2 ),
inference(avatar_split_clause,[],[f337,f345,f341]) ).
fof(f356,definition,
( spl12_4
<=> ! [X0] : ~ p(s(tyop_2Emin_2Ebool,X0)) ),
introduced(definition,[new_symbols(definition,[spl12_4])],[avatar_definition]) ).
fof(f357,plain,
( ! [X0] : ~ p(s(tyop_2Emin_2Ebool,X0))
| ~ spl12_4 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f363,definition,
( spl12_6
<=> ! [X1] : p(s(tyop_2Emin_2Ebool,X1)) ),
introduced(definition,[new_symbols(definition,[spl12_6])],[avatar_definition]) ).
fof(f364,plain,
( ! [X1] : p(s(tyop_2Emin_2Ebool,X1))
| ~ spl12_6 ),
inference(avatar_component_clause,[],[f363]) ).
fof(f399,definition,
( spl12_15
<=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ),
introduced(definition,[new_symbols(definition,[spl12_15])],[avatar_definition]) ).
fof(f400,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| spl12_15 ),
inference(avatar_component_clause,[],[f399]) ).
fof(f403,definition,
( spl12_16
<=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ),
introduced(definition,[new_symbols(definition,[spl12_16])],[avatar_definition]) ).
fof(f405,plain,
( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| ~ spl12_16 ),
inference(avatar_component_clause,[],[f403]) ).
fof(f420,plain,
~ spl12_15,
inference(avatar_split_clause,[],[f251,f399]) ).
fof(f421,plain,
spl12_16,
inference(avatar_split_clause,[],[f220,f403]) ).
fof(f441,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK9)))
| ~ spl12_2 ),
inference(resolution,[],[f269,f347]) ).
fof(f529,plain,
! [X0,X1] :
( s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,X1)
| s(tyop_2Emin_2Ebool,X1) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) ),
inference(superposition,[],[f85,f85]) ).
fof(f565,plain,
! [X0] :
( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) != s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) ),
inference(equality_factoring,[],[f85]) ).
fof(f570,definition,
( spl12_17
<=> ! [X0] : s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) ),
introduced(definition,[new_symbols(definition,[spl12_17])],[avatar_definition]) ).
fof(f571,plain,
( ! [X0] : s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
| ~ spl12_17 ),
inference(avatar_component_clause,[],[f570]) ).
fof(f573,definition,
( spl12_18
<=> s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ),
introduced(definition,[new_symbols(definition,[spl12_18])],[avatar_definition]) ).
fof(f575,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) != s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
| spl12_18 ),
inference(avatar_component_clause,[],[f573]) ).
fof(f576,plain,
( spl12_17
| ~ spl12_18 ),
inference(avatar_split_clause,[],[f565,f573,f570]) ).
fof(f597,definition,
( spl12_20
<=> ! [X1] :
( p(s(tyop_2Emin_2Ebool,X1))
| sP7(c_2Ebool_2EF_2E0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl12_20])],[avatar_definition]) ).
fof(f598,plain,
( ! [X1] :
( p(s(tyop_2Emin_2Ebool,X1))
| sP7(c_2Ebool_2EF_2E0,X1) )
| ~ spl12_20 ),
inference(avatar_component_clause,[],[f597]) ).
fof(f1531,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK11),s(tyop_2Eextreal_2Eextreal,sK9)))
| spl12_3 ),
inference(resolution,[],[f350,f273]) ).
fof(f1560,plain,
( ! [X0] : s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
| ~ spl12_4 ),
inference(backward_subsumption_resolution,[],[f273,f357]) ).
fof(f1596,plain,
( spl12_17
| ~ spl12_4 ),
inference(avatar_split_clause,[],[f1560,f356,f570]) ).
fof(f1649,definition,
( spl12_24
<=> s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))),s(tyop_2Eextreal_2Eextreal,sK9))) ),
introduced(definition,[new_symbols(definition,[spl12_24])],[avatar_definition]) ).
fof(f1651,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))),s(tyop_2Eextreal_2Eextreal,sK9)))
| ~ spl12_24 ),
inference(avatar_component_clause,[],[f1649]) ).
fof(f1669,plain,
( ! [X0,X1] : ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))))
| ~ spl12_6 ),
inference(backward_subsumption_resolution,[],[f277,f364]) ).
fof(f1691,plain,
( $false
| ~ spl12_6 ),
inference(forward_subsumption_resolution,[],[f1669,f364]) ).
fof(f1692,plain,
~ spl12_6,
inference(avatar_contradiction_clause,[],[f1691]) ).
fof(f1798,plain,
! [X0,X1] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| p(s(tyop_2Emin_2Ebool,X1))
| sP5(c_2Ebool_2EF_2E0,X1)
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) ),
inference(superposition,[],[f313,f85]) ).
fof(f1804,plain,
! [X0,X1] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| p(s(tyop_2Emin_2Ebool,X1))
| sP5(c_2Ebool_2EF_2E0,X1) ),
inference(forward_subsumption_resolution,[],[f1798,f272]) ).
fof(f1807,definition,
( spl12_25
<=> ! [X1] :
( p(s(tyop_2Emin_2Ebool,X1))
| sP5(c_2Ebool_2EF_2E0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl12_25])],[avatar_definition]) ).
fof(f1808,plain,
( ! [X1] :
( p(s(tyop_2Emin_2Ebool,X1))
| sP5(c_2Ebool_2EF_2E0,X1) )
| ~ spl12_25 ),
inference(avatar_component_clause,[],[f1807]) ).
fof(f1809,plain,
( spl12_25
| spl12_4 ),
inference(avatar_split_clause,[],[f1804,f356,f1807]) ).
fof(f1830,plain,
! [X0,X1] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| p(s(tyop_2Emin_2Ebool,X1))
| sP7(c_2Ebool_2EF_2E0,X1)
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) ),
inference(superposition,[],[f331,f85]) ).
fof(f1836,plain,
! [X0,X1] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| p(s(tyop_2Emin_2Ebool,X1))
| sP7(c_2Ebool_2EF_2E0,X1) ),
inference(forward_subsumption_resolution,[],[f1830,f272]) ).
fof(f1839,plain,
( spl12_20
| spl12_4 ),
inference(avatar_split_clause,[],[f1836,f356,f597]) ).
fof(f2856,plain,
! [X0,X1] :
( s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))) = s(tyop_2Eextreal_2Eextreal,c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0),s(tyop_2Eextreal_2Eextreal,X1),s(tyop_2Eextreal_2Eextreal,X0)))
| s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))) ),
inference(superposition,[],[f154,f85]) ).
fof(f2881,plain,
! [X0,X1] :
( s(tyop_2Eextreal_2Eextreal,X0) = s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1)))
| s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,X1))) ),
inference(forward_demodulation,[],[f2856,f150]) ).
fof(f9445,definition,
( spl12_56
<=> sP7(c_2Ebool_2EF_2E0,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))),s(tyop_2Eextreal_2Eextreal,sK9))) ),
introduced(definition,[new_symbols(definition,[spl12_56])],[avatar_definition]) ).
fof(f9447,plain,
( sP7(c_2Ebool_2EF_2E0,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))),s(tyop_2Eextreal_2Eextreal,sK9)))
| ~ spl12_56 ),
inference(avatar_component_clause,[],[f9445]) ).
fof(f11743,plain,
( ! [X0] :
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,X0))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,sK9)))) )
| ~ spl12_2 ),
inference(resolution,[],[f347,f276]) ).
fof(f11780,plain,
( sP7(c_2Ebool_2EF_2E0,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))),s(tyop_2Eextreal_2Eextreal,sK9)))
| spl12_1
| ~ spl12_20 ),
inference(resolution,[],[f342,f598]) ).
fof(f11794,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))),s(tyop_2Eextreal_2Eextreal,sK9)))
| spl12_1 ),
inference(superposition,[],[f342,f85]) ).
fof(f11795,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))),s(tyop_2Eextreal_2Eextreal,sK9)))
| spl12_1
| ~ spl12_16 ),
inference(forward_subsumption_resolution,[],[f11794,f405]) ).
fof(f11798,plain,
( spl12_56
| spl12_1
| ~ spl12_20 ),
inference(avatar_split_clause,[],[f11780,f597,f341,f9445]) ).
fof(f11799,plain,
( spl12_24
| spl12_1
| ~ spl12_16 ),
inference(avatar_split_clause,[],[f11795,f403,f341,f1649]) ).
fof(f12596,plain,
( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))))
| ~ spl12_2
| spl12_3 ),
inference(superposition,[],[f11743,f1531]) ).
fof(f12600,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))))
| ~ spl12_2
| spl12_3
| spl12_15 ),
inference(forward_subsumption_resolution,[],[f12596,f400]) ).
fof(f12759,plain,
( ! [X0] : ~ sP5(X0,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11)))
| ~ spl12_2
| spl12_3
| spl12_15 ),
inference(resolution,[],[f12600,f315]) ).
fof(f12890,plain,
( ! [X0] :
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK11),s(tyop_2Eextreal_2Eextreal,X0))))
| p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,X0),s(tyop_2Eextreal_2Eextreal,sK9)))) )
| ~ spl12_3 ),
inference(resolution,[],[f351,f276]) ).
fof(f12909,plain,
( ! [X0] : ~ sP7(X0,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK11),s(tyop_2Eextreal_2Eextreal,sK9)))
| ~ spl12_3 ),
inference(resolution,[],[f351,f333]) ).
fof(f13580,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK11),s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))))))
| spl12_1
| ~ spl12_3 ),
inference(resolution,[],[f12890,f342]) ).
fof(f19939,definition,
( spl12_118
<=> s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK9))) ),
introduced(definition,[new_symbols(definition,[spl12_118])],[avatar_definition]) ).
fof(f19941,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK9)))
| ~ spl12_118 ),
inference(avatar_component_clause,[],[f19939]) ).
fof(f21439,plain,
( ! [X0] :
( s(tyop_2Emin_2Ebool,X0) != s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
| p(s(tyop_2Emin_2Ebool,X0)) )
| ~ spl12_17 ),
inference(superposition,[],[f268,f571]) ).
fof(f21888,plain,
( ! [X0] : p(s(tyop_2Emin_2Ebool,X0))
| ~ spl12_17 ),
inference(forward_subsumption_resolution,[],[f21439,f571]) ).
fof(f21925,plain,
( spl12_6
| ~ spl12_17 ),
inference(avatar_split_clause,[],[f21888,f570,f363]) ).
fof(f28875,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK9)))
| s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11)))
| ~ spl12_24 ),
inference(superposition,[],[f1651,f2881]) ).
fof(f53871,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK11),s(tyop_2Eextreal_2Eextreal,sK10))))
| s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11)))
| spl12_1
| ~ spl12_3 ),
inference(superposition,[],[f13580,f2881]) ).
fof(f53880,definition,
( spl12_225
<=> s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))) ),
introduced(definition,[new_symbols(definition,[spl12_225])],[avatar_definition]) ).
fof(f53882,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11)))
| ~ spl12_225 ),
inference(avatar_component_clause,[],[f53880]) ).
fof(f53884,definition,
( spl12_226
<=> p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK11),s(tyop_2Eextreal_2Eextreal,sK10)))) ),
introduced(definition,[new_symbols(definition,[spl12_226])],[avatar_definition]) ).
fof(f53886,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK11),s(tyop_2Eextreal_2Eextreal,sK10))))
| ~ spl12_226 ),
inference(avatar_component_clause,[],[f53884]) ).
fof(f53887,plain,
( spl12_225
| spl12_226
| spl12_1
| ~ spl12_3 ),
inference(avatar_split_clause,[],[f53871,f349,f341,f53884,f53880]) ).
fof(f54348,plain,
( s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))) = s(tyop_2Eextreal_2Eextreal,c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0),s(tyop_2Eextreal_2Eextreal,sK11),s(tyop_2Eextreal_2Eextreal,sK10)))
| ~ spl12_225 ),
inference(superposition,[],[f154,f53882]) ).
fof(f54531,plain,
( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| sP5(c_2Ebool_2EF_2E0,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11)))
| ~ spl12_25
| ~ spl12_225 ),
inference(superposition,[],[f1808,f53882]) ).
fof(f54791,plain,
( sP5(c_2Ebool_2EF_2E0,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11)))
| spl12_15
| ~ spl12_25
| ~ spl12_225 ),
inference(forward_subsumption_resolution,[],[f54531,f400]) ).
fof(f54801,plain,
( s(tyop_2Eextreal_2Eextreal,sK11) = s(tyop_2Eextreal_2Eextreal,c_2Eextreal_2Eextreal__max_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11)))
| ~ spl12_225 ),
inference(forward_demodulation,[],[f54348,f151]) ).
fof(f55735,plain,
( sP7(c_2Ebool_2EF_2E0,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK11),s(tyop_2Eextreal_2Eextreal,sK9)))
| ~ spl12_56
| ~ spl12_225 ),
inference(superposition,[],[f9447,f54801]) ).
fof(f55910,plain,
( $false
| ~ spl12_3
| ~ spl12_56
| ~ spl12_225 ),
inference(forward_subsumption_resolution,[],[f55735,f12909]) ).
fof(f55911,plain,
( ~ spl12_3
| ~ spl12_56
| ~ spl12_225 ),
inference(avatar_contradiction_clause,[],[f55910]) ).
fof(f63451,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11))))
| ~ spl12_226 ),
inference(resolution,[],[f53886,f277]) ).
fof(f68630,plain,
( ! [X0] :
( ~ p(s(tyop_2Emin_2Ebool,X0))
| s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11)))
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) )
| ~ spl12_226 ),
inference(superposition,[],[f63451,f529]) ).
fof(f68635,plain,
( ! [X0] :
( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11)))
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) )
| ~ spl12_226 ),
inference(forward_subsumption_resolution,[],[f68630,f273]) ).
fof(f68640,plain,
( spl12_17
| spl12_225
| ~ spl12_226 ),
inference(avatar_split_clause,[],[f68635,f53884,f53880,f570]) ).
fof(f68656,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
| ~ spl12_2
| ~ spl12_118 ),
inference(forward_demodulation,[],[f441,f19941]) ).
fof(f68861,plain,
( $false
| ~ spl12_2
| spl12_18
| ~ spl12_118 ),
inference(forward_subsumption_resolution,[],[f68656,f575]) ).
fof(f68862,plain,
( ~ spl12_2
| spl12_18
| ~ spl12_118 ),
inference(avatar_contradiction_clause,[],[f68861]) ).
fof(f68936,plain,
( spl12_225
| spl12_118
| ~ spl12_24 ),
inference(avatar_split_clause,[],[f28875,f1649,f19939,f53880]) ).
fof(f71076,plain,
( $false
| ~ spl12_2
| spl12_3
| spl12_15
| ~ spl12_25
| ~ spl12_225 ),
inference(forward_subsumption_resolution,[],[f54791,f12759]) ).
fof(f71077,plain,
( ~ spl12_2
| spl12_3
| spl12_15
| ~ spl12_25
| ~ spl12_225 ),
inference(avatar_contradiction_clause,[],[f71076]) ).
fof(f71503,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK9))))
| s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11)))
| ~ spl12_1 ),
inference(superposition,[],[f343,f2881]) ).
fof(f71511,plain,
( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK10),s(tyop_2Eextreal_2Eextreal,sK11)))
| ~ spl12_1
| spl12_2 ),
inference(forward_subsumption_resolution,[],[f71503,f346]) ).
fof(f71512,plain,
( spl12_225
| ~ spl12_1
| spl12_2 ),
inference(avatar_split_clause,[],[f71511,f345,f341,f53880]) ).
fof(f122718,plain,
( p(s(tyop_2Emin_2Ebool,c_2Eextreal_2Eextreal__le_2E2(s(tyop_2Eextreal_2Eextreal,sK11),s(tyop_2Eextreal_2Eextreal,sK9))))
| ~ spl12_1
| ~ spl12_225 ),
inference(superposition,[],[f343,f54801]) ).
fof(f122935,plain,
( $false
| ~ spl12_1
| spl12_3
| ~ spl12_225 ),
inference(forward_subsumption_resolution,[],[f122718,f350]) ).
fof(f122936,plain,
( ~ spl12_1
| spl12_3
| ~ spl12_225 ),
inference(avatar_contradiction_clause,[],[f122935]) ).
cnf(s1,plain,
( spl12_1
| spl12_2
| spl12_3 ),
inference(sat_conversion,[],[f352]) ).
cnf(s2,plain,
( ~ spl12_1
| ~ spl12_3 ),
inference(sat_conversion,[],[f353]) ).
cnf(s3,plain,
( ~ spl12_1
| ~ spl12_2 ),
inference(sat_conversion,[],[f354]) ).
cnf(s28,plain,
~ spl12_15,
inference(sat_conversion,[],[f420]) ).
cnf(s29,plain,
spl12_16,
inference(sat_conversion,[],[f421]) ).
cnf(s37,plain,
( spl12_17
| ~ spl12_18 ),
inference(sat_conversion,[],[f576]) ).
cnf(s47,plain,
( ~ spl12_4
| spl12_17 ),
inference(sat_conversion,[],[f1596]) ).
cnf(s55,plain,
~ spl12_6,
inference(sat_conversion,[],[f1692]) ).
cnf(s58,plain,
( spl12_4
| spl12_25 ),
inference(sat_conversion,[],[f1809]) ).
cnf(s62,plain,
( spl12_4
| spl12_20 ),
inference(sat_conversion,[],[f1839]) ).
cnf(s442,plain,
( spl12_1
| ~ spl12_20
| spl12_56 ),
inference(sat_conversion,[],[f11798]) ).
cnf(s444,plain,
( spl12_1
| ~ spl12_16
| spl12_24 ),
inference(sat_conversion,[],[f11799]) ).
cnf(s910,plain,
( spl12_6
| ~ spl12_17 ),
inference(sat_conversion,[],[f21925]) ).
cnf(s1429,plain,
( spl12_1
| ~ spl12_3
| spl12_225
| spl12_226 ),
inference(sat_conversion,[],[f53887]) ).
cnf(s1455,plain,
( ~ spl12_3
| ~ spl12_56
| ~ spl12_225 ),
inference(sat_conversion,[],[f55911]) ).
cnf(s1496,plain,
( spl12_17
| spl12_225
| ~ spl12_226 ),
inference(sat_conversion,[],[f68640]) ).
cnf(s1593,plain,
( ~ spl12_2
| spl12_18
| ~ spl12_118 ),
inference(sat_conversion,[],[f68862]) ).
cnf(s1664,plain,
( ~ spl12_24
| spl12_118
| spl12_225 ),
inference(sat_conversion,[],[f68936]) ).
cnf(s1895,plain,
( ~ spl12_2
| spl12_3
| spl12_15
| ~ spl12_25
| ~ spl12_225 ),
inference(sat_conversion,[],[f71077]) ).
cnf(s2198,plain,
( ~ spl12_1
| spl12_2
| spl12_225 ),
inference(sat_conversion,[],[f71512]) ).
cnf(s3427,plain,
( ~ spl12_1
| spl12_3
| ~ spl12_225 ),
inference(sat_conversion,[],[f122936]) ).
cnf(s3444,plain,
~ spl12_17,
inference(rat,[],[s910,s55]) ).
cnf(s3452,plain,
~ spl12_4,
inference(rat,[],[s47,s3444]) ).
cnf(s3520,plain,
spl12_20,
inference(rat,[],[s62,s3452]) ).
cnf(s3522,plain,
spl12_25,
inference(rat,[],[s58,s3452]) ).
cnf(s3525,plain,
~ spl12_18,
inference(rat,[],[s37,s3444]) ).
cnf(s3539,plain,
( ~ spl12_3
| spl12_225
| spl12_1 ),
inference(rat,[],[s1496,s1429,s3444]) ).
cnf(s3540,plain,
( ~ spl12_3
| spl12_1 ),
inference(rat,[],[s3539,s1455,s442,s3520]) ).
cnf(s3541,plain,
spl12_1,
inference(rat,[],[s1664,s1895,s1593,s1,s3540,s444,s28,s3522,s3525,s29]) ).
cnf(s3637,plain,
~ spl12_2,
inference(rat,[],[s3,s3541]) ).
cnf(s3638,plain,
~ spl12_3,
inference(rat,[],[s2,s3541]) ).
cnf(s3648,plain,
spl12_225,
inference(rat,[],[s2198,s3541,s3637]) ).
cnf(s3652,plain,
$false,
inference(rat,[],[s3427,s3541,s3648,s3638]) ).
fof(f122939,plain,
$false,
inference(avatar_sat_refutation,[],[s3652]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : ITP021+1 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.04/0.30 % Computer : n012.cluster.edu
% 0.04/0.30 % Model : x86_64 x86_64
% 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30 % Memory : 8046.5625MB
% 0.04/0.30 % OS : Linux 6.8.0-71-generic
% 0.04/0.30 % CPULimit : 300
% 0.04/0.30 % WCLimit : 300
% 0.04/0.30 % DateTime : Sun Sep 27 12:06:19 UTC 2026
% 0.04/0.30 % CPUTime :
% 0.04/0.30 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.04/0.32 Running first-order model finding
% 0.04/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.47/1.15 % (2269732)Will run a generic schedule for satisfiability detection.
% 5.47/1.15 % (2269738)% WARNING: option uhcvi not known.
% 5.47/1.15 % (2269737)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=578711477_2999 on theBenchmark for (2999ds/0Mi)
% 5.47/1.15 % (2269741)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3985421106:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.47/1.15 % (2269739)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=407933452:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.47/1.15 % (2269738)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1988550666:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.47/1.15 % (2269740)dis+10_1_sil=32000:sp=arity:random_seed=962634913:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.47/1.15 % (2269742)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4208191612:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.47/1.15 % (2269743)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1282023716:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.47/1.15 % TRYING [1]
% 5.47/1.15 % TRYING [2]
% 5.47/1.15 % (2269740)Instruction limit reached!
% 5.47/1.15 % (2269740)------------------------------
% 5.47/1.15 % (2269740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.47/1.15 % (2269740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.47/1.15 % (2269740)CaDiCaL version: 2.1.3
% 5.47/1.15 % (2269740)Termination reason: Instruction limit
% 5.47/1.15 % (2269740)Termination phase: Saturation
% 5.47/1.15 % (2269740)Time elapsed: 0.033 s
% 5.47/1.15 % (2269740)Peak memory usage: 12 MB
% 5.47/1.15 % (2269740)Instructions burned: 103 (million)
% 5.47/1.15 % (2269741)Instruction limit reached!
% 5.47/1.15 % (2269741)------------------------------
% 5.47/1.15 % (2269741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.47/1.15 % (2269741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.47/1.15 % (2269741)CaDiCaL version: 2.1.3
% 5.47/1.15 % (2269741)Termination reason: Instruction limit
% 5.47/1.15 % (2269741)Termination phase: Saturation
% 5.47/1.15 % (2269741)Time elapsed: 0.037 s
% 5.47/1.15 % (2269741)Peak memory usage: 12 MB
% 5.47/1.15 % (2269741)Instructions burned: 119 (million)
% 5.47/1.15 % (2269742)Instruction limit reached!
% 5.47/1.15 % (2269742)------------------------------
% 5.47/1.15 % (2269742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.47/1.15 % (2269742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.47/1.15 % (2269742)CaDiCaL version: 2.1.3
% 5.47/1.15 % (2269742)Termination reason: Instruction limit
% 5.47/1.15 % (2269742)Termination phase: Saturation
% 5.47/1.15 % (2269742)Time elapsed: 0.039 s
% 5.47/1.15 % (2269742)Peak memory usage: 12 MB
% 5.47/1.15 % (2269742)Instructions burned: 133 (million)
% 5.47/1.15 % TRYING [3]
% 5.47/1.15 % (2269751)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4044877216:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.47/1.15 % (2269752)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1230520392:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 5.47/1.15 % (2269753)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2915473598:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 5.47/1.15 % (2269743)Instruction limit reached!
% 5.47/1.15 % (2269743)------------------------------
% 5.47/1.15 % (2269743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.47/1.15 % (2269743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.47/1.15 % (2269743)CaDiCaL version: 2.1.3
% 5.47/1.15 % (2269743)Termination reason: Instruction limit
% 5.47/1.15 % (2269743)Termination phase: Saturation
% 5.47/1.15 % (2269743)Time elapsed: 0.052 s
% 5.47/1.15 % (2269743)Peak memory usage: 13 MB
% 5.47/1.15 % (2269743)Instructions burned: 160 (million)
% 5.47/1.15 % (2269757)ott-21_1_sil=16000:fs=off:random_seed=397624419:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 5.47/1.15 % TRYING [1]
% 5.47/1.15 % TRYING [2]
% 5.47/1.15 % TRYING [3]
% 5.47/1.15 % (2269752)Instruction limit reached!
% 5.47/1.15 % (2269752)------------------------------
% 5.47/1.15 % (2269752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.47/1.15 % (2269752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.57/3.16 % (2269752)CaDiCaL version: 2.1.3
% 19.57/3.16 % (2269752)Termination reason: Instruction limit
% 19.57/3.16 % (2269752)Termination phase: Saturation
% 19.57/3.16 % (2269752)Time elapsed: 0.041 s
% 19.57/3.16 % (2269752)Peak memory usage: 13 MB
% 19.57/3.16 % (2269752)Instructions burned: 133 (million)
% 19.57/3.16 % (2269759)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4055306014:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 19.57/3.16 % (2269757)Instruction limit reached!
% 19.57/3.16 % (2269757)------------------------------
% 19.57/3.16 % (2269757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.57/3.16 % (2269757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.57/3.16 % (2269757)CaDiCaL version: 2.1.3
% 19.57/3.16 % (2269757)Termination reason: Instruction limit
% 19.57/3.16 % (2269757)Termination phase: Saturation
% 19.57/3.16 % (2269757)Time elapsed: 0.048 s
% 19.57/3.16 % (2269757)Peak memory usage: 13 MB
% 19.57/3.16 % (2269757)Instructions burned: 183 (million)
% 19.57/3.16 % (2269761)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=353852292:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 19.57/3.16 % TRYING [1]
% 19.57/3.16 % TRYING [2]
% 19.57/3.16 % TRYING [3]
% 19.57/3.16 % (2269753)Instruction limit reached!
% 19.57/3.16 % (2269753)------------------------------
% 19.57/3.16 % (2269753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.57/3.16 % (2269753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.57/3.16 % (2269753)CaDiCaL version: 2.1.3
% 19.57/3.16 % (2269753)Termination reason: Instruction limit
% 19.57/3.16 % (2269753)Termination phase: Saturation
% 19.57/3.16 % (2269753)Time elapsed: 0.201 s
% 19.57/3.16 % (2269753)Peak memory usage: 16 MB
% 19.57/3.16 % (2269753)Instructions burned: 686 (million)
% 19.57/3.16 % (2269751)Instruction limit reached!
% 19.57/3.16 % (2269751)------------------------------
% 19.57/3.16 % (2269751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.57/3.16 % (2269751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.57/3.16 % (2269751)CaDiCaL version: 2.1.3
% 19.57/3.16 % (2269751)Termination reason: Instruction limit
% 19.57/3.16 % (2269751)Termination phase: Finite model building SAT solving
% 19.57/3.16 % (2269751)Time elapsed: 0.208 s
% 19.57/3.16 % (2269751)Peak memory usage: 35 MB
% 19.57/3.16 % (2269751)Instructions burned: 714 (million)
% 19.57/3.16 % (2269759)Instruction limit reached!
% 19.57/3.16 % (2269759)------------------------------
% 19.57/3.16 % (2269759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.57/3.16 % (2269759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.57/3.16 % (2269759)CaDiCaL version: 2.1.3
% 19.57/3.16 % (2269759)Termination reason: Instruction limit
% 19.57/3.16 % (2269759)Termination phase: Saturation
% 19.57/3.16 % (2269759)Time elapsed: 0.154 s
% 19.57/3.16 % (2269759)Peak memory usage: 14 MB
% 19.57/3.16 % (2269759)Instructions burned: 478 (million)
% 19.57/3.16 % TRYING [4]
% 19.57/3.16 % (2269763)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1057078042:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 19.57/3.16 % (2269764)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1277090673:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 19.57/3.16 % (2269765)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2835871309:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 19.57/3.16 % (2269761)Instruction limit reached!
% 19.57/3.16 % (2269761)------------------------------
% 19.57/3.16 % (2269761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.57/3.16 % (2269761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.57/3.16 % (2269761)CaDiCaL version: 2.1.3
% 19.57/3.16 % (2269761)Termination reason: Instruction limit
% 19.57/3.16 % (2269761)Termination phase: Finite model building SAT solving
% 19.57/3.16 % (2269761)Time elapsed: 0.201 s
% 19.57/3.16 % (2269761)Peak memory usage: 30 MB
% 19.57/3.16 % (2269761)Instructions burned: 866 (million)
% 19.57/3.16 % (2269769)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2022273405:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 19.57/3.16 % (2269765)Instruction limit reached!
% 19.57/3.16 % (2269765)------------------------------
% 19.57/3.16 % (2269765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.66/3.80 % (2269765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.66/3.80 % (2269765)CaDiCaL version: 2.1.3
% 11.66/3.80 % (2269765)Termination reason: Instruction limit
% 11.66/3.80 % (2269765)Termination phase: Saturation
% 11.66/3.80 % (2269765)Time elapsed: 0.216 s
% 11.66/3.80 % (2269765)Peak memory usage: 16 MB
% 11.66/3.80 % (2269765)Instructions burned: 694 (million)
% 11.66/3.80 % (2269771)fmb+10_1_sil=64000:random_seed=759547645:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 11.66/3.80 % (2269764)Instruction limit reached!
% 11.66/3.80 % (2269764)------------------------------
% 11.66/3.80 % (2269764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.66/3.80 % (2269764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.66/3.80 % (2269764)CaDiCaL version: 2.1.3
% 11.66/3.80 % (2269764)Termination reason: Instruction limit
% 11.66/3.80 % (2269764)Termination phase: Finite model building constraint generation
% 11.66/3.80 % (2269764)Time elapsed: 0.238 s
% 11.66/3.80 % (2269764)Peak memory usage: 101 MB
% 11.66/3.80 % (2269764)Instructions burned: 890 (million)
% 11.66/3.80 % TRYING [1]
% 11.66/3.80 % (2269773)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3364713040:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 11.66/3.80 % TRYING [2]
% 11.66/3.80 % (2269773)Cannot represent all propositional literals internally
% 11.66/3.80 % (2269773)Refutation not found, incomplete strategy
% 11.66/3.80 % (2269773)------------------------------
% 11.66/3.80 % (2269773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.66/3.80 % (2269773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.66/3.80 % (2269773)CaDiCaL version: 2.1.3
% 11.66/3.80 % (2269773)Termination reason: Refutation not found, incomplete strategy
% 11.66/3.80 % (2269773)Time elapsed: 0.026 s
% 11.66/3.80 % (2269773)Peak memory usage: 12 MB
% 11.66/3.80 % (2269773)Instructions burned: 103 (million)
% 11.66/3.80 % (2269773)------------------------------
% 11.66/3.80 % (2269773)------------------------------
% 11.66/3.80 % (2269775)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3371422600:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 11.66/3.80 % TRYING [3]
% 11.66/3.80 % TRYING [8]
% 11.66/3.80 % (2269769)Instruction limit reached!
% 11.66/3.80 % (2269769)------------------------------
% 11.66/3.80 % (2269769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.66/3.80 % (2269769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.66/3.80 % (2269769)CaDiCaL version: 2.1.3
% 11.66/3.80 % (2269769)Termination reason: Instruction limit
% 11.66/3.80 % (2269769)Termination phase: Saturation
% 11.66/3.80 % (2269769)Time elapsed: 0.272 s
% 11.66/3.80 % (2269769)Peak memory usage: 18 MB
% 11.66/3.80 % (2269769)Instructions burned: 881 (million)
% 11.66/3.80 % (2269763)Instruction limit reached!
% 11.66/3.80 % (2269763)------------------------------
% 11.66/3.80 % (2269763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.66/3.80 % (2269763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.66/3.80 % (2269763)CaDiCaL version: 2.1.3
% 11.66/3.80 % (2269763)Termination reason: Instruction limit
% 11.66/3.80 % (2269763)Termination phase: Saturation
% 11.66/3.80 % (2269763)Time elapsed: 0.353 s
% 11.66/3.80 % (2269763)Peak memory usage: 21 MB
% 11.66/3.80 % (2269763)Instructions burned: 1179 (million)
% 11.66/3.80 % (2269777)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1974426137:i=5131_2993 on theBenchmark for (2993ds/5131Mi)
% 11.66/3.80 % (2269778)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3495954468:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi)
% 11.66/3.80 % (2269775)Instruction limit reached!
% 11.66/3.80 % (2269775)------------------------------
% 11.66/3.80 % (2269775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.66/3.80 % (2269775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.66/3.80 % (2269775)CaDiCaL version: 2.1.3
% 11.66/3.80 % (2269775)Termination reason: Instruction limit
% 11.66/3.80 % (2269775)Termination phase: Finite model building constraint generation
% 11.66/3.80 % (2269775)Time elapsed: 0.191 s
% 11.66/3.80 % (2269775)Peak memory usage: 76 MB
% 11.66/3.80 % (2269775)Instructions burned: 920 (million)
% 11.66/3.80 % (2269781)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3569734216:i=6324_2992 on theBenchmark for (2992ds/6324Mi)
% 11.66/3.80 % (2269781)Cannot represent all propositional literals internally
% 11.66/3.80 % (2269781)Refutation not found, incomplete strategy
% 11.66/3.80 % (2269781)------------------------------
% 11.66/3.80 % (2269781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.66/3.80 % (2269781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.66/3.80 % (2269781)CaDiCaL version: 2.1.3
% 11.66/3.80 % (2269781)Termination reason: Refutation not found, incomplete strategy
% 11.66/3.80 % (2269781)Time elapsed: 0.027 s
% 11.66/3.80 % (2269781)Peak memory usage: 12 MB
% 11.66/3.80 % (2269781)Instructions burned: 104 (million)
% 11.66/3.80 % (2269781)------------------------------
% 11.66/3.80 % (2269781)------------------------------
% 11.66/3.80 % TRYING [4]
% 11.66/3.80 % (2269783)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=330627407:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi)
% 11.66/3.80 % TRYING [16]
% 11.66/3.80 % (2269778)Instruction limit reached!
% 11.66/3.80 % (2269778)------------------------------
% 11.66/3.80 % (2269778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.66/3.80 % (2269778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.66/3.80 % (2269778)CaDiCaL version: 2.1.3
% 11.66/3.80 % (2269778)Termination reason: Instruction limit
% 11.66/3.80 % (2269778)Termination phase: Saturation
% 11.66/3.80 % (2269778)Time elapsed: 0.391 s
% 11.66/3.80 % (2269778)Peak memory usage: 25 MB
% 11.66/3.80 % (2269778)Instructions burned: 1472 (million)
% 11.66/3.80 % (2269785)ott-2_1_sil=16000:newcnf=on:random_seed=2603249069:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi)
% 11.66/3.80 % (2269783)Instruction limit reached!
% 11.66/3.80 % (2269783)------------------------------
% 11.66/3.80 % (2269783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.66/3.80 % (2269783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.66/3.80 % (2269783)CaDiCaL version: 2.1.3
% 11.66/3.80 % (2269783)Termination reason: Instruction limit
% 11.66/3.80 % (2269783)Termination phase: Finite model building constraint generation
% 11.66/3.80 % (2269783)Time elapsed: 0.424 s
% 11.66/3.80 % (2269783)Peak memory usage: 128 MB
% 11.66/3.80 % (2269783)Instructions burned: 2178 (million)
% 11.66/3.80 % (2269787)ott+10_1_sil=32000:tgt=ground:random_seed=3532366490:i=5114:av=off_2987 on theBenchmark for (2987ds/5114Mi)
% 11.66/3.80 % (2269785)Instruction limit reached!
% 11.66/3.80 % (2269785)------------------------------
% 11.66/3.80 % (2269785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.66/3.80 % (2269785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.66/3.80 % (2269785)CaDiCaL version: 2.1.3
% 11.66/3.80 % (2269785)Termination reason: Instruction limit
% 11.66/3.80 % (2269785)Termination phase: Saturation
% 11.66/3.80 % (2269785)Time elapsed: 0.249 s
% 11.66/3.80 % (2269785)Peak memory usage: 16 MB
% 11.66/3.80 % (2269785)Instructions burned: 870 (million)
% 11.66/3.80 % (2269789)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2053660690:i=54282_2986 on theBenchmark for (2986ds/54282Mi)
% 11.66/3.80 % TRYING [1]
% 11.66/3.80 % TRYING [2]
% 11.66/3.80 % TRYING [3]
% 11.66/3.80 % TRYING [4]
% 11.66/3.80 % (2269777)Instruction limit reached!
% 11.66/3.80 % (2269777)------------------------------
% 11.66/3.80 % (2269777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.66/3.80 % (2269777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.66/3.80 % (2269777)CaDiCaL version: 2.1.3
% 11.66/3.80 % (2269777)Termination reason: Instruction limit
% 11.66/3.80 % (2269777)Termination phase: Saturation
% 11.66/3.80 % (2269777)Time elapsed: 1.400 s
% 11.66/3.80 % (2269777)Peak memory usage: 29 MB
% 11.66/3.80 % (2269777)Instructions burned: 5134 (million)
% 11.66/3.80 % (2269791)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=101948558:i=3512:aac=none_2979 on theBenchmark for (2979ds/3512Mi)
% 11.66/3.80 % (2269787)Instruction limit reached!
% 11.66/3.80 % (2269787)------------------------------
% 11.66/3.80 % (2269787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.66/3.80 % (2269787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.66/3.80 % (2269787)CaDiCaL version: 2.1.3
% 11.66/3.80 % (2269787)Termination reason: Instruction limit
% 11.66/3.80 % (2269787)Termination phase: Saturation
% 11.66/3.80 % (2269787)Time elapsed: 1.540 s
% 11.66/3.80 % (2269787)Peak memory usage: 33 MB
% 11.66/3.80 % (2269787)Instructions burned: 5115 (million)
% 11.66/3.80 % (2269793)dis+21_1_sil=32000:sas=cadical:random_seed=3160574298:i=3773:amm=off_2971 on theBenchmark for (2971ds/3773Mi)
% 11.66/3.80 % (2269791)Instruction limit reached!
% 11.66/3.80 % (2269791)------------------------------
% 11.66/3.80 % (2269791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.66/3.80 % (2269791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.66/3.80 % (2269791)CaDiCaL version: 2.1.3
% 11.66/3.80 % (2269791)Termination reason: Instruction limit
% 11.66/3.80 % (2269791)Termination phase: Saturation
% 11.66/3.80 % (2269791)Time elapsed: 0.996 s
% 11.66/3.80 % (2269791)Peak memory usage: 23 MB
% 11.66/3.80 % (2269791)Instructions burned: 3514 (million)
% 11.66/3.80 % (2269795)ott+11_1_sil=16000:gs=on:random_seed=639028679:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2969 on theBenchmark for (2969ds/2251Mi)
% 11.66/3.80 % TRYING [5]
% 11.66/3.80 % (2269738) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2269732-2269738"...
% 11.66/3.80 % (2269738)...printing done.
% 11.66/3.80 % (2269738)Refutation found. Thanks to Tanya!
% 11.66/3.80 % SZS status Theorem for theBenchmark
% 11.66/3.80 % SZS output start Proof for theBenchmark
% See solution above
% 11.66/3.80 % (2269738)------------------------------
% 11.66/3.80 % (2269738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.66/3.80 % (2269738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.66/3.80 % (2269738)CaDiCaL version: 2.1.3
% 11.66/3.80 % (2269738)Termination reason: Refutation
% 11.66/3.80 % (2269738)Time elapsed: 3.429 s
% 11.66/3.80 % (2269738)Peak memory usage: 66 MB
% 11.66/3.80 % (2269738)Instructions burned: 11701 (million)
% 11.66/3.80 % (2269732)Success in time 3.476 s
% 11.66/3.80 % Vampire exiting
%------------------------------------------------------------------------------