%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU278+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.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 12:48:08 PM UTC 2026
% Result : Theorem 50.57s 15.82s
% Output : Refutation 106.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 8
% Syntax : Number of formulae : 125 ( 10 unt; 3 def)
% Number of atoms : 698 ( 111 equ)
% Maximal formula atoms : 15 ( 5 avg)
% Number of connectives : 982 ( 409 ~; 421 |; 129 &)
% ( 12 <=>; 9 =>; 0 <=; 2 <~>)
% Maximal formula depth : 18 ( 9 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 3 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 3 con; 0-4 aty)
% Number of variables : 413 ( 0 sgn 312 !; 101 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f28,axiom,
! [X0] :
( relation(X0)
<=> ! [X1] :
~ ( in(X1,X0)
& ! [X2,X3] : X1 != ordered_pair(X2,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_relat_1) ).
fof(f199,conjecture,
! [X0,X1,X2] :
( ( relation(X1)
& relation(X2)
& function(X2) )
=> ? [X3] :
( relation(X3)
& ! [X4,X5] :
( in(ordered_pair(X4,X5),X3)
<=> ( in(X4,X0)
& in(X5,X0)
& in(ordered_pair(apply(X2,X4),apply(X2,X5)),X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_relat_1__e6_21__wellord2) ).
fof(f200,negated_conjecture,
~ ! [X0,X1,X2] :
( ( relation(X1)
& relation(X2)
& function(X2) )
=> ? [X3] :
( relation(X3)
& ! [X4,X5] :
( in(ordered_pair(X4,X5),X3)
<=> ( in(X4,X0)
& in(X5,X0)
& in(ordered_pair(apply(X2,X4),apply(X2,X5)),X1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f199]) ).
fof(f201,axiom,
! [X0,X1,X2] :
( ( relation(X1)
& relation(X2)
& function(X2) )
=> ( ! [X3,X4,X5] :
( ( X3 = X4
& ? [X6,X7] :
( X4 = ordered_pair(X6,X7)
& in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1) )
& X3 = X5
& ? [X8,X9] :
( X5 = ordered_pair(X8,X9)
& in(ordered_pair(apply(X2,X8),apply(X2,X9)),X1) ) )
=> X4 = X5 )
=> ? [X3] :
! [X4] :
( in(X4,X3)
<=> ? [X5] :
( in(X5,cartesian_product2(X0,X0))
& X5 = X4
& ? [X10,X11] :
( X4 = ordered_pair(X10,X11)
& in(ordered_pair(apply(X2,X10),apply(X2,X11)),X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_tarski__e6_21__wellord2__1) ).
fof(f206,axiom,
! [X0,X1,X2,X3] :
( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
<=> ( in(X0,X2)
& in(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t106_zfmisc_1) ).
fof(f276,axiom,
! [X0,X1,X2,X3] :
( ordered_pair(X0,X1) = ordered_pair(X2,X3)
=> ( X0 = X2
& X1 = X3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_zfmisc_1) ).
fof(f366,plain,
! [X0,X1,X2] :
( ( relation(X1)
& relation(X2)
& function(X2) )
=> ( ! [X3,X4,X5] :
( ( X3 = X4
& ? [X6,X7] :
( X4 = ordered_pair(X6,X7)
& in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1) )
& X3 = X5
& ? [X8,X9] :
( X5 = ordered_pair(X8,X9)
& in(ordered_pair(apply(X2,X8),apply(X2,X9)),X1) ) )
=> X4 = X5 )
=> ? [X10] :
! [X11] :
( in(X11,X10)
<=> ? [X12] :
( in(X12,cartesian_product2(X0,X0))
& X11 = X12
& ? [X13,X14] :
( ordered_pair(X13,X14) = X11
& in(ordered_pair(apply(X2,X13),apply(X2,X14)),X1) ) ) ) ) ),
inference(rectify,[],[f201]) ).
fof(f403,plain,
! [X0] :
( relation(X0)
<=> ! [X1] :
( ~ in(X1,X0)
| ? [X2,X3] : ordered_pair(X2,X3) = X1 ) ),
inference(ennf_transformation,[],[f28]) ).
fof(f529,plain,
? [X0,X1,X2] :
( ! [X3] :
( ~ relation(X3)
| ? [X4,X5] :
( in(ordered_pair(X4,X5),X3)
<~> ( in(X4,X0)
& in(X5,X0)
& in(ordered_pair(apply(X2,X4),apply(X2,X5)),X1) ) ) )
& relation(X1)
& relation(X2)
& function(X2) ),
inference(ennf_transformation,[],[f200]) ).
fof(f530,plain,
? [X0,X1,X2] :
( ! [X3] :
( ~ relation(X3)
| ? [X4,X5] :
( in(ordered_pair(X4,X5),X3)
<~> ( in(X4,X0)
& in(X5,X0)
& in(ordered_pair(apply(X2,X4),apply(X2,X5)),X1) ) ) )
& relation(X1)
& relation(X2)
& function(X2) ),
inference(flattening,[],[f529]) ).
fof(f531,plain,
! [X0,X1,X2] :
( ? [X10] :
! [X11] :
( in(X11,X10)
<=> ? [X12] :
( in(X12,cartesian_product2(X0,X0))
& X11 = X12
& ? [X13,X14] :
( ordered_pair(X13,X14) = X11
& in(ordered_pair(apply(X2,X13),apply(X2,X14)),X1) ) ) )
| ? [X3,X4,X5] :
( X4 != X5
& X3 = X4
& ? [X6,X7] :
( X4 = ordered_pair(X6,X7)
& in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1) )
& X3 = X5
& ? [X8,X9] :
( X5 = ordered_pair(X8,X9)
& in(ordered_pair(apply(X2,X8),apply(X2,X9)),X1) ) )
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(ennf_transformation,[],[f366]) ).
fof(f532,plain,
! [X0,X1,X2] :
( ? [X10] :
! [X11] :
( in(X11,X10)
<=> ? [X12] :
( in(X12,cartesian_product2(X0,X0))
& X11 = X12
& ? [X13,X14] :
( ordered_pair(X13,X14) = X11
& in(ordered_pair(apply(X2,X13),apply(X2,X14)),X1) ) ) )
| ? [X3,X4,X5] :
( X4 != X5
& X3 = X4
& ? [X6,X7] :
( X4 = ordered_pair(X6,X7)
& in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1) )
& X3 = X5
& ? [X8,X9] :
( X5 = ordered_pair(X8,X9)
& in(ordered_pair(apply(X2,X8),apply(X2,X9)),X1) ) )
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(flattening,[],[f531]) ).
fof(f631,plain,
! [X0,X1,X2,X3] :
( ( X0 = X2
& X1 = X3 )
| ordered_pair(X2,X3) != ordered_pair(X0,X1) ),
inference(ennf_transformation,[],[f276]) ).
fof(f723,definition,
! [X1,X2] :
( ? [X3,X4,X5] :
( X4 != X5
& X3 = X4
& ? [X6,X7] :
( X4 = ordered_pair(X6,X7)
& in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1) )
& X3 = X5
& ? [X8,X9] :
( X5 = ordered_pair(X8,X9)
& in(ordered_pair(apply(X2,X8),apply(X2,X9)),X1) ) )
| ~ sP2(X1,X2) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f724,plain,
! [X0,X1,X2] :
( ? [X10] :
! [X11] :
( in(X11,X10)
<=> ? [X12] :
( in(X12,cartesian_product2(X0,X0))
& X11 = X12
& ? [X13,X14] :
( ordered_pair(X13,X14) = X11
& in(ordered_pair(apply(X2,X13),apply(X2,X14)),X1) ) ) )
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(definition_folding,[],[f532,f723]) ).
fof(f767,plain,
! [X0] :
( ( relation(X0)
| ? [X1] :
( in(X1,X0)
& ! [X2,X3] : ordered_pair(X2,X3) != X1 ) )
& ( ! [X1] :
( ~ in(X1,X0)
| ? [X2,X3] : ordered_pair(X2,X3) = X1 )
| ~ relation(X0) ) ),
inference(nnf_transformation,[],[f403]) ).
fof(f768,plain,
! [X0] :
( ( relation(X0)
| ? [X1] :
( in(X1,X0)
& ! [X2,X3] : ordered_pair(X2,X3) != X1 ) )
& ( ! [X4] :
( ~ in(X4,X0)
| ? [X5,X6] : ordered_pair(X5,X6) = X4 )
| ~ relation(X0) ) ),
inference(rectify,[],[f767]) ).
fof(f769,plain,
! [X0] :
( ( relation(X0)
| ( in(sK25(X0),X0)
& ! [X2,X3] : ordered_pair(X2,X3) != sK25(X0) ) )
& ( ! [X4] :
( ~ in(X4,X0)
| ordered_pair(sK26(X4),sK27(X4)) = X4 )
| ~ relation(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25,sK26,sK27]),skolemize(X1,sK25(X0)),skolemize(X5,sK26(X4)),skolemize(X6,sK27(X4))],[f768]) ).
fof(f930,plain,
? [X0,X1,X2] :
( ! [X3] :
( ~ relation(X3)
| ? [X4,X5] :
( ( ~ in(X4,X0)
| ~ in(X5,X0)
| ~ in(ordered_pair(apply(X2,X4),apply(X2,X5)),X1)
| ~ in(ordered_pair(X4,X5),X3) )
& ( ( in(X4,X0)
& in(X5,X0)
& in(ordered_pair(apply(X2,X4),apply(X2,X5)),X1) )
| in(ordered_pair(X4,X5),X3) ) ) )
& relation(X1)
& relation(X2)
& function(X2) ),
inference(nnf_transformation,[],[f530]) ).
fof(f931,plain,
? [X0,X1,X2] :
( ! [X3] :
( ~ relation(X3)
| ? [X4,X5] :
( ( ~ in(X4,X0)
| ~ in(X5,X0)
| ~ in(ordered_pair(apply(X2,X4),apply(X2,X5)),X1)
| ~ in(ordered_pair(X4,X5),X3) )
& ( ( in(X4,X0)
& in(X5,X0)
& in(ordered_pair(apply(X2,X4),apply(X2,X5)),X1) )
| in(ordered_pair(X4,X5),X3) ) ) )
& relation(X1)
& relation(X2)
& function(X2) ),
inference(flattening,[],[f930]) ).
fof(f932,plain,
( ! [X3] :
( ~ relation(X3)
| ( ( ~ in(sK121(X3),sK118)
| ~ in(sK122(X3),sK118)
| ~ in(ordered_pair(apply(sK120,sK121(X3)),apply(sK120,sK122(X3))),sK119)
| ~ in(ordered_pair(sK121(X3),sK122(X3)),X3) )
& ( ( in(sK121(X3),sK118)
& in(sK122(X3),sK118)
& in(ordered_pair(apply(sK120,sK121(X3)),apply(sK120,sK122(X3))),sK119) )
| in(ordered_pair(sK121(X3),sK122(X3)),X3) ) ) )
& relation(sK119)
& relation(sK120)
& function(sK120) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK118,sK119,sK120,sK121,sK122]),skolemize(X0,sK118),skolemize(X1,sK119),skolemize(X2,sK120),skolemize(X4,sK121(X3)),skolemize(X5,sK122(X3))],[f931]) ).
fof(f933,plain,
! [X1,X2] :
( ? [X3,X4,X5] :
( X4 != X5
& X3 = X4
& ? [X6,X7] :
( X4 = ordered_pair(X6,X7)
& in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1) )
& X3 = X5
& ? [X8,X9] :
( X5 = ordered_pair(X8,X9)
& in(ordered_pair(apply(X2,X8),apply(X2,X9)),X1) ) )
| ~ sP2(X1,X2) ),
inference(nnf_transformation,[],[f723]) ).
fof(f934,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( X3 != X4
& X2 = X3
& ? [X5,X6] :
( ordered_pair(X5,X6) = X3
& in(ordered_pair(apply(X1,X5),apply(X1,X6)),X0) )
& X2 = X4
& ? [X7,X8] :
( ordered_pair(X7,X8) = X4
& in(ordered_pair(apply(X1,X7),apply(X1,X8)),X0) ) )
| ~ sP2(X0,X1) ),
inference(rectify,[],[f933]) ).
fof(f935,plain,
! [X0,X1] :
( ( sK124(X0,X1) != sK125(X0,X1)
& sK123(X0,X1) = sK124(X0,X1)
& sK124(X0,X1) = ordered_pair(sK126(X0,X1),sK127(X0,X1))
& in(ordered_pair(apply(X1,sK126(X0,X1)),apply(X1,sK127(X0,X1))),X0)
& sK123(X0,X1) = sK125(X0,X1)
& sK125(X0,X1) = ordered_pair(sK128(X0,X1),sK129(X0,X1))
& in(ordered_pair(apply(X1,sK128(X0,X1)),apply(X1,sK129(X0,X1))),X0) )
| ~ sP2(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK123,sK124,sK125,sK126,sK127,sK128,sK129]),skolemize(X2,sK123(X0,X1)),skolemize(X3,sK124(X0,X1)),skolemize(X4,sK125(X0,X1)),skolemize(X5,sK126(X0,X1)),skolemize(X6,sK127(X0,X1)),skolemize(X7,sK128(X0,X1)),skolemize(X8,sK129(X0,X1))],[f934]) ).
fof(f936,plain,
! [X0,X1,X2] :
( ? [X10] :
! [X11] :
( ( in(X11,X10)
| ! [X12] :
( ~ in(X12,cartesian_product2(X0,X0))
| X11 != X12
| ! [X13,X14] :
( ordered_pair(X13,X14) != X11
| ~ in(ordered_pair(apply(X2,X13),apply(X2,X14)),X1) ) ) )
& ( ? [X12] :
( in(X12,cartesian_product2(X0,X0))
& X11 = X12
& ? [X13,X14] :
( ordered_pair(X13,X14) = X11
& in(ordered_pair(apply(X2,X13),apply(X2,X14)),X1) ) )
| ~ in(X11,X10) ) )
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(nnf_transformation,[],[f724]) ).
fof(f937,plain,
! [X0,X1,X2] :
( ? [X3] :
! [X4] :
( ( in(X4,X3)
| ! [X5] :
( ~ in(X5,cartesian_product2(X0,X0))
| X4 != X5
| ! [X6,X7] :
( ordered_pair(X6,X7) != X4
| ~ in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1) ) ) )
& ( ? [X8] :
( in(X8,cartesian_product2(X0,X0))
& X4 = X8
& ? [X9,X10] :
( ordered_pair(X9,X10) = X4
& in(ordered_pair(apply(X2,X9),apply(X2,X10)),X1) ) )
| ~ in(X4,X3) ) )
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(rectify,[],[f936]) ).
fof(f938,plain,
! [X0,X1,X2] :
( ! [X4] :
( ( in(X4,sK130(X0,X1,X2))
| ! [X5] :
( ~ in(X5,cartesian_product2(X0,X0))
| X4 != X5
| ! [X6,X7] :
( ordered_pair(X6,X7) != X4
| ~ in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1) ) ) )
& ( ( in(sK131(X0,X1,X2,X4),cartesian_product2(X0,X0))
& sK131(X0,X1,X2,X4) = X4
& ordered_pair(sK132(X1,X2,X4),sK133(X1,X2,X4)) = X4
& in(ordered_pair(apply(X2,sK132(X1,X2,X4)),apply(X2,sK133(X1,X2,X4))),X1) )
| ~ in(X4,sK130(X0,X1,X2)) ) )
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK130,sK131,sK132,sK133]),skolemize(X3,sK130(X0,X1,X2)),skolemize(X8,sK131(X0,X1,X2,X4)),skolemize(X9,sK132(X1,X2,X4)),skolemize(X10,sK133(X1,X2,X4))],[f937]) ).
fof(f956,plain,
! [X0,X1,X2,X3] :
( ( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) )
& ( ( in(X0,X2)
& in(X1,X3) )
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ) ),
inference(nnf_transformation,[],[f206]) ).
fof(f957,plain,
! [X0,X1,X2,X3] :
( ( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) )
& ( ( in(X0,X2)
& in(X1,X3) )
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ) ),
inference(flattening,[],[f956]) ).
fof(f1109,plain,
! [X2,X3,X0] :
( ordered_pair(X2,X3) != sK25(X0)
| relation(X0) ),
inference(cnf_transformation,[],[f769]) ).
fof(f1110,plain,
! [X0] :
( in(sK25(X0),X0)
| relation(X0) ),
inference(cnf_transformation,[],[f769]) ).
fof(f1494,plain,
function(sK120),
inference(cnf_transformation,[],[f932]) ).
fof(f1495,plain,
relation(sK120),
inference(cnf_transformation,[],[f932]) ).
fof(f1496,plain,
relation(sK119),
inference(cnf_transformation,[],[f932]) ).
fof(f1497,plain,
! [X3] :
( in(ordered_pair(apply(sK120,sK121(X3)),apply(sK120,sK122(X3))),sK119)
| ~ relation(X3)
| in(ordered_pair(sK121(X3),sK122(X3)),X3) ),
inference(cnf_transformation,[],[f932]) ).
fof(f1498,plain,
! [X3] :
( in(ordered_pair(sK121(X3),sK122(X3)),X3)
| in(sK122(X3),sK118)
| ~ relation(X3) ),
inference(cnf_transformation,[],[f932]) ).
fof(f1499,plain,
! [X3] :
( in(ordered_pair(sK121(X3),sK122(X3)),X3)
| in(sK121(X3),sK118)
| ~ relation(X3) ),
inference(cnf_transformation,[],[f932]) ).
fof(f1500,plain,
! [X3] :
( ~ in(ordered_pair(apply(sK120,sK121(X3)),apply(sK120,sK122(X3))),sK119)
| ~ in(sK121(X3),sK118)
| ~ in(sK122(X3),sK118)
| ~ relation(X3)
| ~ in(ordered_pair(sK121(X3),sK122(X3)),X3) ),
inference(cnf_transformation,[],[f932]) ).
fof(f1503,plain,
! [X0,X1] :
( sK123(X0,X1) = sK125(X0,X1)
| ~ sP2(X0,X1) ),
inference(cnf_transformation,[],[f935]) ).
fof(f1506,plain,
! [X0,X1] :
( sK123(X0,X1) = sK124(X0,X1)
| ~ sP2(X0,X1) ),
inference(cnf_transformation,[],[f935]) ).
fof(f1507,plain,
! [X0,X1] :
( sK124(X0,X1) != sK125(X0,X1)
| ~ sP2(X0,X1) ),
inference(cnf_transformation,[],[f935]) ).
fof(f1508,plain,
! [X2,X0,X1,X4] :
( in(ordered_pair(apply(X2,sK132(X1,X2,X4)),apply(X2,sK133(X1,X2,X4))),X1)
| ~ in(X4,sK130(X0,X1,X2))
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(cnf_transformation,[],[f938]) ).
fof(f1509,plain,
! [X2,X0,X1,X4] :
( ordered_pair(sK132(X1,X2,X4),sK133(X1,X2,X4)) = X4
| ~ in(X4,sK130(X0,X1,X2))
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(cnf_transformation,[],[f938]) ).
fof(f1510,plain,
! [X2,X0,X1,X4] :
( sK131(X0,X1,X2,X4) = X4
| ~ in(X4,sK130(X0,X1,X2))
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(cnf_transformation,[],[f938]) ).
fof(f1511,plain,
! [X2,X0,X1,X4] :
( in(sK131(X0,X1,X2,X4),cartesian_product2(X0,X0))
| ~ in(X4,sK130(X0,X1,X2))
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(cnf_transformation,[],[f938]) ).
fof(f1512,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( in(X4,sK130(X0,X1,X2))
| ~ in(X5,cartesian_product2(X0,X0))
| X4 != X5
| ordered_pair(X6,X7) != X4
| ~ in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1)
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(cnf_transformation,[],[f938]) ).
fof(f1539,plain,
! [X2,X3,X0,X1] :
( ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
| in(X1,X3) ),
inference(cnf_transformation,[],[f957]) ).
fof(f1540,plain,
! [X2,X3,X0,X1] :
( ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
| in(X0,X2) ),
inference(cnf_transformation,[],[f957]) ).
fof(f1541,plain,
! [X2,X3,X0,X1] :
( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) ),
inference(cnf_transformation,[],[f957]) ).
fof(f1642,plain,
! [X2,X3,X0,X1] :
( ordered_pair(X2,X3) != ordered_pair(X0,X1)
| X1 = X3 ),
inference(cnf_transformation,[],[f631]) ).
fof(f1643,plain,
! [X2,X3,X0,X1] :
( ordered_pair(X2,X3) != ordered_pair(X0,X1)
| X0 = X2 ),
inference(cnf_transformation,[],[f631]) ).
fof(f1894,plain,
! [X2,X0,X1,X6,X7,X5] :
( in(X5,sK130(X0,X1,X2))
| ~ in(X5,cartesian_product2(X0,X0))
| ordered_pair(X6,X7) != X5
| ~ in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1)
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(equality_resolution,[],[f1512]) ).
fof(f1895,plain,
! [X2,X0,X1,X6,X7] :
( ~ in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1)
| ~ in(ordered_pair(X6,X7),cartesian_product2(X0,X0))
| in(ordered_pair(X6,X7),sK130(X0,X1,X2))
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(equality_resolution,[],[f1894]) ).
fof(f1960,plain,
! [X0,X1] :
( ~ in(ordered_pair(sK121(X0),sK122(X0)),cartesian_product2(X1,X1))
| in(ordered_pair(sK121(X0),sK122(X0)),sK130(X1,sK119,sK120))
| sP2(sK119,sK120)
| ~ relation(sK119)
| ~ relation(sK120)
| ~ function(sK120)
| ~ relation(X0)
| in(ordered_pair(sK121(X0),sK122(X0)),X0) ),
inference(resolution,[],[f1895,f1497]) ).
fof(f1961,plain,
! [X0,X1] :
( ~ in(ordered_pair(sK121(X0),sK122(X0)),cartesian_product2(X1,X1))
| in(ordered_pair(sK121(X0),sK122(X0)),sK130(X1,sK119,sK120))
| sP2(sK119,sK120)
| ~ relation(sK120)
| ~ function(sK120)
| ~ relation(X0)
| in(ordered_pair(sK121(X0),sK122(X0)),X0) ),
inference(forward_subsumption_resolution,[],[f1960,f1496]) ).
fof(f1962,plain,
! [X0,X1] :
( ~ in(ordered_pair(sK121(X0),sK122(X0)),cartesian_product2(X1,X1))
| in(ordered_pair(sK121(X0),sK122(X0)),sK130(X1,sK119,sK120))
| sP2(sK119,sK120)
| ~ function(sK120)
| ~ relation(X0)
| in(ordered_pair(sK121(X0),sK122(X0)),X0) ),
inference(forward_subsumption_resolution,[],[f1961,f1495]) ).
fof(f1963,plain,
! [X0,X1] :
( ~ in(ordered_pair(sK121(X0),sK122(X0)),cartesian_product2(X1,X1))
| in(ordered_pair(sK121(X0),sK122(X0)),sK130(X1,sK119,sK120))
| sP2(sK119,sK120)
| ~ relation(X0)
| in(ordered_pair(sK121(X0),sK122(X0)),X0) ),
inference(forward_subsumption_resolution,[],[f1962,f1494]) ).
fof(f1965,definition,
( spl170_3
<=> sP2(sK119,sK120) ),
introduced(definition,[new_symbols(definition,[spl170_3])],[avatar_definition]) ).
fof(f1967,plain,
( sP2(sK119,sK120)
| ~ spl170_3 ),
inference(avatar_component_clause,[],[f1965]) ).
fof(f1969,definition,
( spl170_4
<=> ! [X0,X1] :
( ~ in(ordered_pair(sK121(X0),sK122(X0)),cartesian_product2(X1,X1))
| in(ordered_pair(sK121(X0),sK122(X0)),X0)
| ~ relation(X0)
| in(ordered_pair(sK121(X0),sK122(X0)),sK130(X1,sK119,sK120)) ) ),
introduced(definition,[new_symbols(definition,[spl170_4])],[avatar_definition]) ).
fof(f1970,plain,
( ! [X0,X1] :
( in(ordered_pair(sK121(X0),sK122(X0)),sK130(X1,sK119,sK120))
| in(ordered_pair(sK121(X0),sK122(X0)),X0)
| ~ relation(X0)
| ~ in(ordered_pair(sK121(X0),sK122(X0)),cartesian_product2(X1,X1)) )
| ~ spl170_4 ),
inference(avatar_component_clause,[],[f1969]) ).
fof(f1971,plain,
( spl170_3
| spl170_4 ),
inference(avatar_split_clause,[],[f1963,f1969,f1965]) ).
fof(f2144,plain,
! [X0,X1] :
( sK124(X0,X1) = sK125(X0,X1)
| ~ sP2(X0,X1)
| ~ sP2(X0,X1) ),
inference(superposition,[],[f1506,f1503]) ).
fof(f2145,plain,
! [X0,X1] :
( sK124(X0,X1) = sK125(X0,X1)
| ~ sP2(X0,X1) ),
inference(duplicate_literal_removal,[],[f2144]) ).
fof(f2147,plain,
! [X0,X1] : ~ sP2(X0,X1),
inference(forward_subsumption_resolution,[],[f2145,f1507]) ).
fof(f2149,plain,
( $false
| ~ spl170_3 ),
inference(resolution,[],[f2147,f1967]) ).
fof(f2150,plain,
~ spl170_3,
inference(avatar_contradiction_clause,[],[f2149]) ).
fof(f2152,plain,
( ! [X0] :
( in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),sK130(X0,sK119,sK120))
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0)) )
| ~ spl170_4 ),
inference(factoring,[],[f1970]) ).
fof(f2244,plain,
! [X2,X3,X0,X1] :
( in(X0,cartesian_product2(X1,X1))
| ~ in(X0,sK130(X1,X2,X3))
| sP2(X2,X3)
| ~ relation(X2)
| ~ relation(X3)
| ~ function(X3)
| ~ in(X0,sK130(X1,X2,X3))
| sP2(X2,X3)
| ~ relation(X2)
| ~ relation(X3)
| ~ function(X3) ),
inference(superposition,[],[f1511,f1510]) ).
fof(f2245,plain,
! [X2,X3,X0,X1] :
( in(X0,cartesian_product2(X1,X1))
| ~ in(X0,sK130(X1,X2,X3))
| sP2(X2,X3)
| ~ relation(X2)
| ~ relation(X3)
| ~ function(X3) ),
inference(duplicate_literal_removal,[],[f2244]) ).
fof(f2246,plain,
! [X2,X3,X0,X1] :
( ~ in(X0,sK130(X1,X2,X3))
| in(X0,cartesian_product2(X1,X1))
| ~ relation(X2)
| ~ relation(X3)
| ~ function(X3) ),
inference(forward_subsumption_resolution,[],[f2245,f2147]) ).
fof(f2249,plain,
! [X2,X0,X1] :
( in(ordered_pair(sK121(sK130(X0,X1,X2)),sK122(sK130(X0,X1,X2))),cartesian_product2(X0,X0))
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2)
| in(sK121(sK130(X0,X1,X2)),sK118)
| ~ relation(sK130(X0,X1,X2)) ),
inference(resolution,[],[f2246,f1499]) ).
fof(f2250,plain,
! [X2,X0,X1] :
( in(ordered_pair(sK121(sK130(X0,X1,X2)),sK122(sK130(X0,X1,X2))),cartesian_product2(X0,X0))
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2)
| in(sK122(sK130(X0,X1,X2)),sK118)
| ~ relation(sK130(X0,X1,X2)) ),
inference(resolution,[],[f2246,f1498]) ).
fof(f2324,plain,
! [X2,X3,X0,X1,X4] :
( sK25(X3) != X0
| relation(X3)
| ~ in(X0,sK130(X4,X1,X2))
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(superposition,[],[f1109,f1509]) ).
fof(f2326,plain,
! [X2,X3,X0,X1,X4] :
( sK25(X3) != X0
| relation(X3)
| ~ in(X0,sK130(X4,X1,X2))
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(forward_subsumption_resolution,[],[f2324,f2147]) ).
fof(f2337,plain,
! [X2,X3,X0,X1] :
( ~ in(sK25(X0),sK130(X1,X2,X3))
| relation(X0)
| ~ relation(X2)
| ~ relation(X3)
| ~ function(X3) ),
inference(equality_resolution,[],[f2326]) ).
fof(f2370,plain,
! [X2,X0,X1] :
( in(sK122(sK130(X0,X1,X2)),sK118)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2)
| in(sK122(sK130(X0,X1,X2)),X0)
| ~ relation(sK130(X0,X1,X2)) ),
inference(resolution,[],[f1539,f2250]) ).
fof(f2386,plain,
! [X2,X0,X1] :
( in(sK121(sK130(X0,X1,X2)),sK118)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2)
| in(sK121(sK130(X0,X1,X2)),X0)
| ~ relation(sK130(X0,X1,X2)) ),
inference(resolution,[],[f1540,f2249]) ).
fof(f2397,plain,
! [X2,X0,X1] :
( relation(sK130(X0,X1,X2))
| relation(sK130(X0,X1,X2))
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(resolution,[],[f1110,f2337]) ).
fof(f2408,plain,
! [X2,X0,X1] :
( relation(sK130(X0,X1,X2))
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(duplicate_literal_removal,[],[f2397]) ).
fof(f2525,plain,
! [X2,X3,X0,X1,X4,X5] :
( ordered_pair(X1,X2) != X0
| sK133(X3,X4,X0) = X2
| ~ in(X0,sK130(X5,X3,X4))
| sP2(X3,X4)
| ~ relation(X3)
| ~ relation(X4)
| ~ function(X4) ),
inference(superposition,[],[f1642,f1509]) ).
fof(f2528,plain,
! [X2,X3,X0,X1,X4,X5] :
( ordered_pair(X1,X2) != X0
| sK133(X3,X4,X0) = X2
| ~ in(X0,sK130(X5,X3,X4))
| ~ relation(X3)
| ~ relation(X4)
| ~ function(X4) ),
inference(forward_subsumption_resolution,[],[f2525,f2147]) ).
fof(f2696,plain,
! [X2,X3,X0,X1,X4,X5] :
( ordered_pair(X1,X2) != X0
| sK132(X3,X4,X0) = X1
| ~ in(X0,sK130(X5,X3,X4))
| sP2(X3,X4)
| ~ relation(X3)
| ~ relation(X4)
| ~ function(X4) ),
inference(superposition,[],[f1643,f1509]) ).
fof(f2699,plain,
! [X2,X3,X0,X1,X4,X5] :
( ordered_pair(X1,X2) != X0
| sK132(X3,X4,X0) = X1
| ~ in(X0,sK130(X5,X3,X4))
| ~ relation(X3)
| ~ relation(X4)
| ~ function(X4) ),
inference(forward_subsumption_resolution,[],[f2696,f2147]) ).
fof(f2878,plain,
! [X2,X3,X0,X1,X4] :
( ~ in(ordered_pair(X2,X3),sK130(X4,X0,X1))
| sK133(X0,X1,ordered_pair(X2,X3)) = X3
| ~ relation(X0)
| ~ relation(X1)
| ~ function(X1) ),
inference(equality_resolution,[],[f2528]) ).
fof(f2881,plain,
( ! [X0] :
( sK122(sK130(X0,sK119,sK120)) = sK133(sK119,sK120,ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))))
| ~ relation(sK119)
| ~ relation(sK120)
| ~ function(sK120)
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0)) )
| ~ spl170_4 ),
inference(resolution,[],[f2878,f2152]) ).
fof(f2905,plain,
( ! [X0] :
( sK122(sK130(X0,sK119,sK120)) = sK133(sK119,sK120,ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))))
| ~ relation(sK120)
| ~ function(sK120)
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0)) )
| ~ spl170_4 ),
inference(forward_subsumption_resolution,[],[f2881,f1496]) ).
fof(f2908,plain,
( ! [X0] :
( sK122(sK130(X0,sK119,sK120)) = sK133(sK119,sK120,ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))))
| ~ function(sK120)
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0)) )
| ~ spl170_4 ),
inference(forward_subsumption_resolution,[],[f2905,f1495]) ).
fof(f2910,plain,
( ! [X0] :
( sK122(sK130(X0,sK119,sK120)) = sK133(sK119,sK120,ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))))
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0)) )
| ~ spl170_4 ),
inference(forward_subsumption_resolution,[],[f2908,f1494]) ).
fof(f2925,plain,
( ! [X0,X1] :
( in(ordered_pair(apply(sK120,sK132(sK119,sK120,ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))))),apply(sK120,sK122(sK130(X0,sK119,sK120)))),sK119)
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),sK130(X1,sK119,sK120))
| sP2(sK119,sK120)
| ~ relation(sK119)
| ~ relation(sK120)
| ~ function(sK120)
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0)) )
| ~ spl170_4 ),
inference(superposition,[],[f1508,f2910]) ).
fof(f2926,plain,
( ! [X0,X1] :
( in(ordered_pair(apply(sK120,sK132(sK119,sK120,ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))))),apply(sK120,sK122(sK130(X0,sK119,sK120)))),sK119)
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),sK130(X1,sK119,sK120))
| ~ relation(sK119)
| ~ relation(sK120)
| ~ function(sK120)
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0)) )
| ~ spl170_4 ),
inference(forward_subsumption_resolution,[],[f2925,f2147]) ).
fof(f2928,plain,
( ! [X0,X1] :
( in(ordered_pair(apply(sK120,sK132(sK119,sK120,ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))))),apply(sK120,sK122(sK130(X0,sK119,sK120)))),sK119)
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),sK130(X1,sK119,sK120))
| ~ relation(sK120)
| ~ function(sK120)
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0)) )
| ~ spl170_4 ),
inference(forward_subsumption_resolution,[],[f2926,f1496]) ).
fof(f2930,plain,
( ! [X0,X1] :
( in(ordered_pair(apply(sK120,sK132(sK119,sK120,ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))))),apply(sK120,sK122(sK130(X0,sK119,sK120)))),sK119)
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),sK130(X1,sK119,sK120))
| ~ function(sK120)
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0)) )
| ~ spl170_4 ),
inference(forward_subsumption_resolution,[],[f2928,f1495]) ).
fof(f2932,plain,
( ! [X0,X1] :
( in(ordered_pair(apply(sK120,sK132(sK119,sK120,ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))))),apply(sK120,sK122(sK130(X0,sK119,sK120)))),sK119)
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),sK130(X1,sK119,sK120))
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0)) )
| ~ spl170_4 ),
inference(forward_subsumption_resolution,[],[f2930,f1494]) ).
fof(f3335,plain,
! [X2,X3,X0,X1,X4] :
( ~ in(ordered_pair(X2,X3),sK130(X4,X0,X1))
| sK132(X0,X1,ordered_pair(X2,X3)) = X2
| ~ relation(X0)
| ~ relation(X1)
| ~ function(X1) ),
inference(equality_resolution,[],[f2699]) ).
fof(f3338,plain,
( ! [X0] :
( sK121(sK130(X0,sK119,sK120)) = sK132(sK119,sK120,ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))))
| ~ relation(sK119)
| ~ relation(sK120)
| ~ function(sK120)
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0)) )
| ~ spl170_4 ),
inference(resolution,[],[f3335,f2152]) ).
fof(f3363,plain,
( ! [X0] :
( sK121(sK130(X0,sK119,sK120)) = sK132(sK119,sK120,ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))))
| ~ relation(sK120)
| ~ function(sK120)
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0)) )
| ~ spl170_4 ),
inference(forward_subsumption_resolution,[],[f3338,f1496]) ).
fof(f3366,plain,
( ! [X0] :
( sK121(sK130(X0,sK119,sK120)) = sK132(sK119,sK120,ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))))
| ~ function(sK120)
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0)) )
| ~ spl170_4 ),
inference(forward_subsumption_resolution,[],[f3363,f1495]) ).
fof(f3368,plain,
( ! [X0] :
( sK121(sK130(X0,sK119,sK120)) = sK132(sK119,sK120,ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))))
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0)) )
| ~ spl170_4 ),
inference(forward_subsumption_resolution,[],[f3366,f1494]) ).
fof(f3390,plain,
( ! [X0,X1] :
( in(ordered_pair(apply(sK120,sK121(sK130(X0,sK119,sK120))),apply(sK120,sK122(sK130(X0,sK119,sK120)))),sK119)
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),sK130(X1,sK119,sK120))
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0))
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0)) )
| ~ spl170_4 ),
inference(superposition,[],[f2932,f3368]) ).
fof(f3393,plain,
( ! [X0,X1] :
( in(ordered_pair(apply(sK120,sK121(sK130(X0,sK119,sK120))),apply(sK120,sK122(sK130(X0,sK119,sK120)))),sK119)
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),sK130(X1,sK119,sK120))
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0)) )
| ~ spl170_4 ),
inference(duplicate_literal_removal,[],[f3390]) ).
fof(f3539,plain,
! [X0,X1] :
( in(sK122(sK130(sK118,X0,X1)),sK118)
| ~ relation(X0)
| ~ relation(X1)
| ~ function(X1)
| ~ relation(sK130(sK118,X0,X1)) ),
inference(factoring,[],[f2370]) ).
fof(f3540,plain,
! [X0,X1] :
( in(sK122(sK130(sK118,X0,X1)),sK118)
| ~ relation(X0)
| ~ relation(X1)
| ~ function(X1) ),
inference(forward_subsumption_resolution,[],[f3539,f2408]) ).
fof(f3546,plain,
! [X0,X1] :
( in(sK121(sK130(sK118,X0,X1)),sK118)
| ~ relation(X0)
| ~ relation(X1)
| ~ function(X1)
| ~ relation(sK130(sK118,X0,X1)) ),
inference(factoring,[],[f2386]) ).
fof(f3547,plain,
! [X0,X1] :
( in(sK121(sK130(sK118,X0,X1)),sK118)
| ~ relation(X0)
| ~ relation(X1)
| ~ function(X1) ),
inference(forward_subsumption_resolution,[],[f3546,f2408]) ).
fof(f7803,plain,
( ! [X0,X1] :
( ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),sK130(X1,sK119,sK120))
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0))
| ~ in(sK121(sK130(X0,sK119,sK120)),sK118)
| ~ in(sK122(sK130(X0,sK119,sK120)),sK118)
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),sK130(X0,sK119,sK120)) )
| ~ spl170_4 ),
inference(resolution,[],[f3393,f1500]) ).
fof(f7819,plain,
( ! [X0,X1] :
( ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),sK130(X1,sK119,sK120))
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0))
| ~ in(sK121(sK130(X0,sK119,sK120)),sK118)
| ~ in(sK122(sK130(X0,sK119,sK120)),sK118)
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),sK130(X0,sK119,sK120)) )
| ~ spl170_4 ),
inference(duplicate_literal_removal,[],[f7803]) ).
fof(f7825,plain,
( ! [X0,X1] :
( ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),sK130(X1,sK119,sK120))
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0))
| ~ in(sK121(sK130(X0,sK119,sK120)),sK118)
| ~ in(sK122(sK130(X0,sK119,sK120)),sK118) )
| ~ spl170_4 ),
inference(forward_subsumption_resolution,[],[f7819,f2152]) ).
fof(f7834,plain,
( ! [X0] :
( ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0))
| ~ in(sK121(sK130(X0,sK119,sK120)),sK118)
| ~ in(sK122(sK130(X0,sK119,sK120)),sK118)
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0)) )
| ~ spl170_4 ),
inference(resolution,[],[f7825,f2152]) ).
fof(f7848,plain,
( ! [X0] :
( ~ in(ordered_pair(sK121(sK130(X0,sK119,sK120)),sK122(sK130(X0,sK119,sK120))),cartesian_product2(X0,X0))
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(sK121(sK130(X0,sK119,sK120)),sK118)
| ~ in(sK122(sK130(X0,sK119,sK120)),sK118) )
| ~ spl170_4 ),
inference(duplicate_literal_removal,[],[f7834]) ).
fof(f7854,plain,
( ! [X0] :
( ~ in(sK122(sK130(X0,sK119,sK120)),sK118)
| ~ in(sK121(sK130(X0,sK119,sK120)),sK118)
| ~ relation(sK130(X0,sK119,sK120))
| ~ in(sK121(sK130(X0,sK119,sK120)),X0)
| ~ in(sK122(sK130(X0,sK119,sK120)),X0) )
| ~ spl170_4 ),
inference(resolution,[],[f7848,f1541]) ).
fof(f7867,plain,
( ~ in(sK121(sK130(sK118,sK119,sK120)),sK118)
| ~ relation(sK130(sK118,sK119,sK120))
| ~ in(sK121(sK130(sK118,sK119,sK120)),sK118)
| ~ in(sK122(sK130(sK118,sK119,sK120)),sK118)
| ~ relation(sK119)
| ~ relation(sK120)
| ~ function(sK120)
| ~ spl170_4 ),
inference(resolution,[],[f7854,f3540]) ).
fof(f7870,plain,
( ~ in(sK121(sK130(sK118,sK119,sK120)),sK118)
| ~ relation(sK130(sK118,sK119,sK120))
| ~ in(sK122(sK130(sK118,sK119,sK120)),sK118)
| ~ relation(sK119)
| ~ relation(sK120)
| ~ function(sK120)
| ~ spl170_4 ),
inference(duplicate_literal_removal,[],[f7867]) ).
fof(f7874,plain,
( ~ relation(sK130(sK118,sK119,sK120))
| ~ in(sK122(sK130(sK118,sK119,sK120)),sK118)
| ~ relation(sK119)
| ~ relation(sK120)
| ~ function(sK120)
| ~ spl170_4 ),
inference(forward_subsumption_resolution,[],[f7870,f3547]) ).
fof(f7876,plain,
( ~ in(sK122(sK130(sK118,sK119,sK120)),sK118)
| ~ relation(sK119)
| ~ relation(sK120)
| ~ function(sK120)
| ~ spl170_4 ),
inference(forward_subsumption_resolution,[],[f7874,f2408]) ).
fof(f7878,plain,
( ~ relation(sK119)
| ~ relation(sK120)
| ~ function(sK120)
| ~ spl170_4 ),
inference(forward_subsumption_resolution,[],[f7876,f3540]) ).
fof(f7881,plain,
( ~ relation(sK120)
| ~ function(sK120)
| ~ spl170_4 ),
inference(forward_subsumption_resolution,[],[f7878,f1496]) ).
fof(f7882,plain,
( ~ function(sK120)
| ~ spl170_4 ),
inference(forward_subsumption_resolution,[],[f7881,f1495]) ).
fof(f7883,plain,
( $false
| ~ spl170_4 ),
inference(forward_subsumption_resolution,[],[f7882,f1494]) ).
fof(f7884,plain,
~ spl170_4,
inference(avatar_contradiction_clause,[],[f7883]) ).
cnf(s2,plain,
( spl170_3
| spl170_4 ),
inference(sat_conversion,[],[f1971]) ).
cnf(s5,plain,
~ spl170_3,
inference(sat_conversion,[],[f2150]) ).
cnf(s40,plain,
~ spl170_4,
inference(sat_conversion,[],[f7884]) ).
cnf(s43,plain,
$false,
inference(rat,[],[s2,s40,s5]) ).
fof(f7885,plain,
$false,
inference(avatar_sat_refutation,[],[s43]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU278+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n007.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 28 04:25:40 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.92/2.79 % (2024047)Detected formulas, will run a generic FOF schedule.
% 12.92/2.79 % (2024055)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2141842836:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.92/2.79 % (2024055)Instruction limit reached!
% 12.92/2.79 % (2024055)------------------------------
% 12.92/2.79 % (2024055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.92/2.79 % (2024055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.92/2.79 % (2024055)CaDiCaL version: 2.1.3
% 12.92/2.79 % (2024055)Termination reason: Instruction limit
% 12.92/2.79 % (2024055)Termination phase: Saturation
% 12.92/2.79 % (2024055)Time elapsed: 0.037 s
% 12.92/2.79 % (2024055)Peak memory usage: 90 MB
% 12.92/2.79 % (2024055)Instructions burned: 110 (million)
% 12.92/2.79 % (2024054)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=3711507534:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.92/2.79 % (2024056)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4294454987:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.92/2.79 % (2024052)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=2345937664:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.92/2.79 % (2024058)dis-21_1_sil=8000:lcm=predicate:random_seed=45352339:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 12.92/2.79 % (2024053)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=139166753:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.92/2.79 % (2024057)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4267547736:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.92/2.79 % (2024058)Instruction limit reached!
% 12.92/2.79 % (2024058)------------------------------
% 12.92/2.79 % (2024058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.92/2.79 % (2024058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.92/2.79 % (2024058)CaDiCaL version: 2.1.3
% 12.92/2.79 % (2024058)Termination reason: Instruction limit
% 12.92/2.79 % (2024058)Termination phase: Saturation
% 12.92/2.79 % (2024058)Time elapsed: 0.072 s
% 12.92/2.79 % (2024058)Peak memory usage: 91 MB
% 12.92/2.79 % (2024058)Instructions burned: 130 (million)
% 12.92/2.79 % (2024056)Instruction limit reached!
% 12.92/2.79 % (2024056)------------------------------
% 12.92/2.79 % (2024056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.92/2.79 % (2024056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.92/2.79 % (2024056)CaDiCaL version: 2.1.3
% 12.92/2.79 % (2024056)Termination reason: Instruction limit
% 12.92/2.79 % (2024056)Termination phase: Saturation
% 12.92/2.79 % (2024056)Time elapsed: 0.073 s
% 12.92/2.79 % (2024056)Peak memory usage: 89 MB
% 12.92/2.79 % (2024056)Instructions burned: 120 (million)
% 12.92/2.79 % (2024057)Instruction limit reached!
% 12.92/2.79 % (2024057)------------------------------
% 12.92/2.79 % (2024057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.92/2.79 % (2024057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.92/2.79 % (2024057)CaDiCaL version: 2.1.3
% 12.92/2.79 % (2024057)Termination reason: Instruction limit
% 12.92/2.79 % (2024057)Termination phase: Saturation
% 12.92/2.79 % (2024057)Time elapsed: 0.093 s
% 12.92/2.79 % (2024057)Peak memory usage: 90 MB
% 12.92/2.79 % (2024057)Instructions burned: 140 (million)
% 12.92/2.79 % (2024065)lrs+10_1_sil=8000:sp=occurrence:random_seed=3054194729:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 12.92/2.79 % (2024065)Instruction limit reached!
% 12.92/2.79 % (2024065)------------------------------
% 12.92/2.79 % (2024065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.92/2.79 % (2024065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.92/2.79 % (2024065)CaDiCaL version: 2.1.3
% 12.92/2.79 % (2024065)Termination reason: Instruction limit
% 12.92/2.79 % (2024065)Termination phase: Saturation
% 12.92/2.79 % (2024065)Time elapsed: 0.102 s
% 12.92/2.79 % (2024065)Peak memory usage: 94 MB
% 12.92/2.79 % (2024065)Instructions burned: 286 (million)
% 20.48/3.82 % (2024068)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1252537097:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 20.48/3.82 % (2024067)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4136128122:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 20.48/3.82 % (2024067)Refutation not found, incomplete strategy
% 20.48/3.82 % (2024067)------------------------------
% 20.48/3.82 % (2024067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.48/3.82 % (2024067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.82 % (2024067)CaDiCaL version: 2.1.3
% 20.48/3.82 % (2024067)Termination reason: Refutation not found, incomplete strategy
% 20.48/3.82 % (2024067)Time elapsed: 0.006 s
% 20.48/3.82 % (2024067)Peak memory usage: 89 MB
% 20.48/3.82 % (2024067)Instructions burned: 7 (million)
% 20.48/3.82 % (2024069)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=3212836784:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 20.48/3.82 % (2024071)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2668234863:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 20.48/3.82 % (2024069)Instruction limit reached!
% 20.48/3.82 % (2024069)------------------------------
% 20.48/3.82 % (2024069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.48/3.82 % (2024069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.82 % (2024069)CaDiCaL version: 2.1.3
% 20.48/3.82 % (2024069)Termination reason: Instruction limit
% 20.48/3.82 % (2024069)Termination phase: Saturation
% 20.48/3.82 % (2024069)Time elapsed: 0.139 s
% 20.48/3.82 % (2024069)Peak memory usage: 92 MB
% 20.48/3.82 % (2024069)Instructions burned: 249 (million)
% 20.48/3.82 % (2024071)Instruction limit reached!
% 20.48/3.82 % (2024071)------------------------------
% 20.48/3.82 % (2024071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.48/3.82 % (2024071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.82 % (2024071)CaDiCaL version: 2.1.3
% 20.48/3.82 % (2024071)Termination reason: Instruction limit
% 20.48/3.82 % (2024071)Termination phase: Saturation
% 20.48/3.82 % (2024071)Time elapsed: 0.100 s
% 20.48/3.82 % (2024071)Peak memory usage: 91 MB
% 20.48/3.82 % (2024071)Instructions burned: 296 (million)
% 20.48/3.82 % (2024068)Instruction limit reached!
% 20.48/3.82 % (2024068)------------------------------
% 20.48/3.82 % (2024068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.48/3.82 % (2024068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.82 % (2024068)CaDiCaL version: 2.1.3
% 20.48/3.82 % (2024068)Termination reason: Instruction limit
% 20.48/3.82 % (2024068)Termination phase: Saturation
% 20.48/3.82 % (2024068)Time elapsed: 0.225 s
% 20.48/3.82 % (2024068)Peak memory usage: 93 MB
% 20.48/3.82 % (2024068)Instructions burned: 327 (million)
% 20.48/3.82 % (2024067)------------------------------
% 20.48/3.82 % (2024067)------------------------------
% 20.48/3.82 % (2024077)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1487739552:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 20.48/3.82 % (2024076)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2026564825:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 20.48/3.82 % (2024077)Instruction limit reached!
% 20.48/3.82 % (2024077)------------------------------
% 20.48/3.82 % (2024077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.48/3.82 % (2024077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.82 % (2024077)CaDiCaL version: 2.1.3
% 20.48/3.82 % (2024077)Termination reason: Instruction limit
% 20.48/3.82 % (2024077)Termination phase: Saturation
% 20.48/3.82 % (2024077)Time elapsed: 0.039 s
% 20.48/3.82 % (2024077)Peak memory usage: 91 MB
% 20.48/3.82 % (2024077)Instructions burned: 115 (million)
% 20.48/3.82 % (2024078)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1742569448:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 20.48/3.82 % (2024079)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3814060914:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 20.48/3.82 % (2024078)Instruction limit reached!
% 20.48/3.82 % (2024078)------------------------------
% 20.48/3.82 % (2024078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.36/7.21 % (2024078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.36/7.21 % (2024078)CaDiCaL version: 2.1.3
% 45.36/7.21 % (2024078)Termination reason: Instruction limit
% 45.36/7.21 % (2024078)Termination phase: Saturation
% 45.36/7.21 % (2024078)Time elapsed: 0.066 s
% 45.36/7.21 % (2024078)Peak memory usage: 90 MB
% 45.36/7.21 % (2024078)Instructions burned: 127 (million)
% 45.36/7.21 % (2024079)Instruction limit reached!
% 45.36/7.21 % (2024079)------------------------------
% 45.36/7.21 % (2024079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.36/7.21 % (2024079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.36/7.21 % (2024079)CaDiCaL version: 2.1.3
% 45.36/7.21 % (2024079)Termination reason: Instruction limit
% 45.36/7.21 % (2024079)Termination phase: Saturation
% 45.36/7.21 % (2024079)Time elapsed: 0.072 s
% 45.36/7.21 % (2024079)Peak memory usage: 89 MB
% 45.36/7.21 % (2024079)Instructions burned: 114 (million)
% 45.36/7.21 % (2024082)lrs+10_1_sil=8000:sp=occurrence:random_seed=576344681:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 45.36/7.21 % (2024085)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2849212448:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 45.36/7.21 % (2024086)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2836579803:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 45.36/7.21 % (2024082)Instruction limit reached!
% 45.36/7.21 % (2024082)------------------------------
% 45.36/7.21 % (2024082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.36/7.21 % (2024082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.36/7.21 % (2024082)CaDiCaL version: 2.1.3
% 45.36/7.21 % (2024082)Termination reason: Instruction limit
% 45.36/7.21 % (2024082)Termination phase: Saturation
% 45.36/7.21 % (2024082)Time elapsed: 0.308 s
% 45.36/7.21 % (2024082)Peak memory usage: 103 MB
% 45.36/7.21 % (2024082)Instructions burned: 909 (million)
% 45.36/7.21 % (2024085)Instruction limit reached!
% 45.36/7.21 % (2024085)------------------------------
% 45.36/7.21 % (2024085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.36/7.21 % (2024085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.36/7.21 % (2024085)CaDiCaL version: 2.1.3
% 45.36/7.21 % (2024085)Termination reason: Instruction limit
% 45.36/7.21 % (2024085)Termination phase: Saturation
% 45.36/7.21 % (2024085)Time elapsed: 0.266 s
% 45.36/7.21 % (2024085)Peak memory usage: 93 MB
% 45.36/7.21 % (2024085)Instructions burned: 438 (million)
% 45.36/7.21 % (2024090)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1239088477:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 45.36/7.21 % (2024090)Instruction limit reached!
% 45.36/7.21 % (2024090)------------------------------
% 45.36/7.21 % (2024090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.36/7.21 % (2024090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.36/7.21 % (2024090)CaDiCaL version: 2.1.3
% 45.36/7.21 % (2024090)Termination reason: Instruction limit
% 45.36/7.21 % (2024090)Termination phase: Saturation
% 45.36/7.21 % (2024090)Time elapsed: 0.043 s
% 45.36/7.21 % (2024090)Peak memory usage: 92 MB
% 45.36/7.21 % (2024090)Instructions burned: 137 (million)
% 45.36/7.21 % (2024091)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1261704526:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 45.36/7.21 % (2024093)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2521907468:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi)
% 45.36/7.21 % (2024091)Instruction limit reached!
% 45.36/7.21 % (2024091)------------------------------
% 45.36/7.21 % (2024091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.36/7.21 % (2024091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.36/7.21 % (2024091)CaDiCaL version: 2.1.3
% 45.36/7.21 % (2024091)Termination reason: Instruction limit
% 45.36/7.21 % (2024091)Termination phase: Saturation
% 45.36/7.21 % (2024091)Time elapsed: 0.329 s
% 45.36/7.21 % (2024091)Peak memory usage: 95 MB
% 45.36/7.21 % (2024091)Instructions burned: 592 (million)
% 45.36/7.21 % (2024096)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=1529600840:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/125Mi)
% 71.27/10.97 % (2024096)Instruction limit reached!
% 71.27/10.97 % (2024096)------------------------------
% 71.27/10.97 % (2024096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.27/10.97 % (2024096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.27/10.97 % (2024096)CaDiCaL version: 2.1.3
% 71.27/10.97 % (2024096)Termination reason: Instruction limit
% 71.27/10.97 % (2024096)Termination phase: Saturation
% 71.27/10.97 % (2024096)Time elapsed: 0.091 s
% 71.27/10.97 % (2024096)Peak memory usage: 91 MB
% 71.27/10.97 % (2024096)Instructions burned: 125 (million)
% 71.27/10.97 % (2024076)Instruction limit reached!
% 71.27/10.97 % (2024076)------------------------------
% 71.27/10.97 % (2024076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.27/10.97 % (2024076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.27/10.97 % (2024076)CaDiCaL version: 2.1.3
% 71.27/10.97 % (2024076)Termination reason: Instruction limit
% 71.27/10.97 % (2024076)Termination phase: Saturation
% 71.27/10.97 % (2024076)Time elapsed: 1.439 s
% 71.27/10.97 % (2024076)Peak memory usage: 144 MB
% 71.27/10.97 % (2024076)Instructions burned: 2351 (million)
% 71.27/10.97 % (2024098)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1507124524:i=134:gtgl=5:slsql=off:gtg=exists_sym_2979 on theBenchmark for (2979ds/134Mi)
% 71.27/10.97 % (2024098)Instruction limit reached!
% 71.27/10.97 % (2024098)------------------------------
% 71.27/10.97 % (2024098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.27/10.97 % (2024098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.27/10.97 % (2024098)CaDiCaL version: 2.1.3
% 71.27/10.97 % (2024098)Termination reason: Instruction limit
% 71.27/10.97 % (2024098)Termination phase: Saturation
% 71.27/10.97 % (2024098)Time elapsed: 0.080 s
% 71.27/10.97 % (2024098)Peak memory usage: 91 MB
% 71.27/10.97 % (2024098)Instructions burned: 134 (million)
% 71.27/10.97 % (2024099)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=103302201:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/141Mi)
% 71.27/10.97 % (2024099)Instruction limit reached!
% 71.27/10.97 % (2024099)------------------------------
% 71.27/10.97 % (2024099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.27/10.97 % (2024099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.27/10.97 % (2024099)CaDiCaL version: 2.1.3
% 71.27/10.97 % (2024099)Termination reason: Instruction limit
% 71.27/10.97 % (2024099)Termination phase: Saturation
% 71.27/10.97 % (2024099)Time elapsed: 0.086 s
% 71.27/10.97 % (2024099)Peak memory usage: 92 MB
% 71.27/10.97 % (2024099)Instructions burned: 142 (million)
% 71.27/10.97 % (2024101)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=164898544:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2977 on theBenchmark for (2977ds/431Mi)
% 71.27/10.97 % (2024103)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=2784205724:i=6060:aac=none:ins=25_2975 on theBenchmark for (2975ds/6060Mi)
% 71.27/10.97 % (2024101)Instruction limit reached!
% 71.27/10.97 % (2024101)------------------------------
% 71.27/10.97 % (2024101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.27/10.97 % (2024101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.27/10.97 % (2024101)CaDiCaL version: 2.1.3
% 71.27/10.97 % (2024101)Termination reason: Instruction limit
% 71.27/10.97 % (2024101)Termination phase: Saturation
% 71.27/10.97 % (2024101)Time elapsed: 0.252 s
% 71.27/10.97 % (2024101)Peak memory usage: 94 MB
% 71.27/10.97 % (2024101)Instructions burned: 431 (million)
% 71.27/10.97 % (2024106)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=3669581626:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2972 on theBenchmark for (2972ds/150Mi)
% 71.27/10.97 % (2024106)Instruction limit reached!
% 71.27/10.97 % (2024106)------------------------------
% 71.27/10.97 % (2024106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.27/10.97 % (2024106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.27/10.97 % (2024106)CaDiCaL version: 2.1.3
% 71.27/10.97 % (2024106)Termination reason: Instruction limit
% 71.27/10.97 % (2024106)Termination phase: Saturation
% 96.09/14.46 % (2024106)Time elapsed: 0.090 s
% 96.09/14.46 % (2024106)Peak memory usage: 91 MB
% 96.09/14.46 % (2024106)Instructions burned: 151 (million)
% 96.09/14.46 % (2024108)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=573096262:i=14155:bd=all_2970 on theBenchmark for (2970ds/14155Mi)
% 96.09/14.46 % (2024086)Instruction limit reached!
% 96.09/14.46 % (2024086)------------------------------
% 96.09/14.46 % (2024086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.09/14.46 % (2024086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.09/14.46 % (2024086)CaDiCaL version: 2.1.3
% 96.09/14.46 % (2024086)Termination reason: Instruction limit
% 96.09/14.46 % (2024086)Termination phase: Saturation
% 96.09/14.46 % (2024086)Time elapsed: 3.148 s
% 96.09/14.46 % (2024086)Peak memory usage: 165 MB
% 96.09/14.46 % (2024086)Instructions burned: 5203 (million)
% 96.09/14.46 % (2024110)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=71017127:i=667:av=off:fsr=off_2957 on theBenchmark for (2957ds/667Mi)
% 96.09/14.46 % (2024110)Instruction limit reached!
% 96.09/14.46 % (2024110)------------------------------
% 96.09/14.46 % (2024110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.09/14.46 % (2024110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.09/14.46 % (2024110)CaDiCaL version: 2.1.3
% 96.09/14.46 % (2024110)Termination reason: Instruction limit
% 96.09/14.46 % (2024110)Termination phase: Saturation
% 96.09/14.46 % (2024110)Time elapsed: 0.307 s
% 96.09/14.46 % (2024110)Peak memory usage: 90 MB
% 96.09/14.46 % (2024110)Instructions burned: 668 (million)
% 96.09/14.46 % (2024112)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=2901549332:s2a=on:i=185:s2at=1.8:fdi=4_2953 on theBenchmark for (2953ds/185Mi)
% 96.09/14.46 % (2024112)Instruction limit reached!
% 96.09/14.46 % (2024112)------------------------------
% 96.09/14.46 % (2024112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.09/14.46 % (2024112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.09/14.46 % (2024112)CaDiCaL version: 2.1.3
% 96.09/14.46 % (2024112)Termination reason: Instruction limit
% 96.09/14.46 % (2024112)Termination phase: Saturation
% 96.09/14.46 % (2024112)Time elapsed: 0.112 s
% 96.09/14.46 % (2024112)Peak memory usage: 92 MB
% 96.09/14.46 % (2024112)Instructions burned: 185 (million)
% 96.09/14.46 % (2024114)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2926597845:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2950 on theBenchmark for (2950ds/193Mi)
% 96.09/14.46 % (2024114)Instruction limit reached!
% 96.09/14.46 % (2024114)------------------------------
% 96.09/14.46 % (2024114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.09/14.46 % (2024114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.09/14.46 % (2024114)CaDiCaL version: 2.1.3
% 96.09/14.46 % (2024114)Termination reason: Instruction limit
% 96.09/14.46 % (2024114)Termination phase: Saturation
% 96.09/14.46 % (2024114)Time elapsed: 0.109 s
% 96.09/14.46 % (2024114)Peak memory usage: 92 MB
% 96.09/14.46 % (2024114)Instructions burned: 195 (million)
% 96.09/14.46 % (2024116)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=821881962:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2947 on theBenchmark for (2947ds/4850Mi)
% 96.09/14.46 % (2024093)Instruction limit reached!
% 96.09/14.46 % (2024093)------------------------------
% 96.09/14.46 % (2024093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.09/14.46 % (2024093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.09/14.46 % (2024093)CaDiCaL version: 2.1.3
% 96.09/14.46 % (2024093)Termination reason: Instruction limit
% 96.09/14.46 % (2024093)Termination phase: Saturation
% 96.09/14.46 % (2024093)Time elapsed: 4.371 s
% 96.09/14.46 % (2024093)Peak memory usage: 239 MB
% 96.09/14.46 % (2024093)Instructions burned: 13194 (million)
% 96.09/14.46 % (2024118)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1302568595:i=12111:sd=1:ss=included_2941 on theBenchmark for (2941ds/12111Mi)
% 96.09/14.46 % (2024103)Instruction limit reached!
% 96.09/14.46 % (2024103)------------------------------
% 96.09/14.46 % (2024103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.09/14.46 % (2024103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.57/15.82 % (2024103)CaDiCaL version: 2.1.3
% 50.57/15.82 % (2024103)Termination reason: Instruction limit
% 50.57/15.82 % (2024103)Termination phase: Saturation
% 50.57/15.82 % (2024103)Time elapsed: 3.759 s
% 50.57/15.82 % (2024103)Peak memory usage: 174 MB
% 50.57/15.82 % (2024103)Instructions burned: 6061 (million)
% 50.57/15.82 % (2024120)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1392214832:i=319:kws=precedence:fsr=off_2936 on theBenchmark for (2936ds/319Mi)
% 50.57/15.82 % (2024120)Instruction limit reached!
% 50.57/15.82 % (2024120)------------------------------
% 50.57/15.82 % (2024120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.57/15.82 % (2024120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.57/15.82 % (2024120)CaDiCaL version: 2.1.3
% 50.57/15.82 % (2024120)Termination reason: Instruction limit
% 50.57/15.82 % (2024120)Termination phase: Saturation
% 50.57/15.82 % (2024120)Time elapsed: 0.194 s
% 50.57/15.82 % (2024120)Peak memory usage: 93 MB
% 50.57/15.82 % (2024120)Instructions burned: 319 (million)
% 50.57/15.82 % (2024122)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3511565192:i=2064:ep=RST_2932 on theBenchmark for (2932ds/2064Mi)
% 50.57/15.82 % (2024122)Instruction limit reached!
% 50.57/15.82 % (2024122)------------------------------
% 50.57/15.82 % (2024122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.57/15.82 % (2024122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.57/15.82 % (2024122)CaDiCaL version: 2.1.3
% 50.57/15.82 % (2024122)Termination reason: Instruction limit
% 50.57/15.82 % (2024122)Termination phase: Saturation
% 50.57/15.82 % (2024122)Time elapsed: 1.045 s
% 50.57/15.82 % (2024122)Peak memory usage: 136 MB
% 50.57/15.82 % (2024122)Instructions burned: 2065 (million)
% 50.57/15.82 % (2024124)dis-1011_128_sil=32000:random_seed=876805453:i=3706:ep=RST:av=off_2920 on theBenchmark for (2920ds/3706Mi)
% 50.57/15.82 % (2024116)Instruction limit reached!
% 50.57/15.82 % (2024116)------------------------------
% 50.57/15.82 % (2024116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.57/15.82 % (2024116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.57/15.82 % (2024116)CaDiCaL version: 2.1.3
% 50.57/15.82 % (2024116)Termination reason: Instruction limit
% 50.57/15.82 % (2024116)Termination phase: Saturation
% 50.57/15.82 % (2024116)Time elapsed: 2.858 s
% 50.57/15.82 % (2024116)Peak memory usage: 153 MB
% 50.57/15.82 % (2024116)Instructions burned: 4850 (million)
% 50.57/15.82 % (2024126)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3826025834:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2916 on theBenchmark for (2916ds/757Mi)
% 50.57/15.82 % (2024126)Instruction limit reached!
% 50.57/15.82 % (2024126)------------------------------
% 50.57/15.82 % (2024126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.57/15.82 % (2024126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.57/15.82 % (2024126)CaDiCaL version: 2.1.3
% 50.57/15.82 % (2024126)Termination reason: Instruction limit
% 50.57/15.82 % (2024126)Termination phase: Saturation
% 50.57/15.82 % (2024126)Time elapsed: 0.531 s
% 50.57/15.82 % (2024126)Peak memory usage: 109 MB
% 50.57/15.82 % (2024126)Instructions burned: 757 (million)
% 50.57/15.82 % (2024128)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1542448796:i=13913:ss=axioms:sgt=8_2909 on theBenchmark for (2909ds/13913Mi)
% 50.57/15.82 % (2024118)Instruction limit reached!
% 50.57/15.82 % (2024118)------------------------------
% 50.57/15.82 % (2024118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.57/15.82 % (2024118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.57/15.82 % (2024118)CaDiCaL version: 2.1.3
% 50.57/15.82 % (2024118)Termination reason: Instruction limit
% 50.57/15.82 % (2024118)Termination phase: Saturation
% 50.57/15.82 % (2024118)Time elapsed: 3.653 s
% 50.57/15.82 % (2024118)Peak memory usage: 221 MB
% 50.57/15.82 % (2024118)Instructions burned: 12112 (million)
% 50.57/15.82 % (2024130)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1752129670:i=9925:aac=none_2903 on theBenchmark for (2903ds/9925Mi)
% 50.57/15.82 % (2024124)Instruction limit reached!
% 50.57/15.82 % (2024124)------------------------------
% 50.57/15.82 % (2024124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.57/15.82 % (2024124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.57/15.82 % (2024124)CaDiCaL version: 2.1.3
% 50.57/15.82 % (2024124)Termination reason: Instruction limit
% 50.57/15.82 % (2024124)Termination phase: Saturation
% 50.57/15.82 % (2024124)Time elapsed: 2.024 s
% 50.57/15.82 % (2024124)Peak memory usage: 107 MB
% 50.57/15.82 % (2024124)Instructions burned: 3706 (million)
% 50.57/15.82 % (2024132)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=257236098:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2898 on theBenchmark for (2898ds/2479Mi)
% 50.57/15.82 % (2024108)Instruction limit reached!
% 50.57/15.82 % (2024108)------------------------------
% 50.57/15.82 % (2024108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.57/15.82 % (2024108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.57/15.82 % (2024108)CaDiCaL version: 2.1.3
% 50.57/15.82 % (2024108)Termination reason: Instruction limit
% 50.57/15.82 % (2024108)Termination phase: Saturation
% 50.57/15.82 % (2024108)Time elapsed: 8.031 s
% 50.57/15.82 % (2024108)Peak memory usage: 259 MB
% 50.57/15.82 % (2024108)Instructions burned: 14156 (million)
% 50.57/15.82 % (2024134)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2176975127:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2888 on theBenchmark for (2888ds/440Mi)
% 50.57/15.82 % (2024134)Instruction limit reached!
% 50.57/15.82 % (2024134)------------------------------
% 50.57/15.82 % (2024134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.57/15.82 % (2024134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.57/15.82 % (2024134)CaDiCaL version: 2.1.3
% 50.57/15.82 % (2024134)Termination reason: Instruction limit
% 50.57/15.82 % (2024134)Termination phase: Saturation
% 50.57/15.82 % (2024134)Time elapsed: 0.252 s
% 50.57/15.82 % (2024134)Peak memory usage: 94 MB
% 50.57/15.82 % (2024134)Instructions burned: 441 (million)
% 50.57/15.82 % (2024136)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=4177806121:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2884 on theBenchmark for (2884ds/11145Mi)
% 50.57/15.82 % (2024132)Instruction limit reached!
% 50.57/15.82 % (2024132)------------------------------
% 50.57/15.82 % (2024132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.57/15.82 % (2024132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.57/15.82 % (2024132)CaDiCaL version: 2.1.3
% 50.57/15.82 % (2024132)Termination reason: Instruction limit
% 50.57/15.82 % (2024132)Termination phase: Saturation
% 50.57/15.82 % (2024132)Time elapsed: 1.518 s
% 50.57/15.82 % (2024132)Peak memory usage: 111 MB
% 50.57/15.82 % (2024132)Instructions burned: 2480 (million)
% 50.57/15.82 % (2024138)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=2191111494:cts=off:i=3034:av=off:er=known:fsd=on_2881 on theBenchmark for (2881ds/3034Mi)
% 50.57/15.82 % (2024130)Instruction limit reached!
% 50.57/15.82 % (2024130)------------------------------
% 50.57/15.82 % (2024130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.57/15.82 % (2024130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.57/15.82 % (2024130)CaDiCaL version: 2.1.3
% 50.57/15.82 % (2024130)Termination reason: Instruction limit
% 50.57/15.82 % (2024130)Termination phase: Saturation
% 50.57/15.82 % (2024130)Time elapsed: 3.063 s
% 50.57/15.82 % (2024130)Peak memory usage: 207 MB
% 50.57/15.82 % (2024130)Instructions burned: 9926 (million)
% 50.57/15.82 % (2024140)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1619578020:st=2:s2a=on:i=524:s2at=2:ss=axioms_2871 on theBenchmark for (2871ds/524Mi)
% 50.57/15.82 % (2024140)Instruction limit reached!
% 50.57/15.82 % (2024140)------------------------------
% 50.57/15.82 % (2024140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.57/15.82 % (2024140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.57/15.82 % (2024140)CaDiCaL version: 2.1.3
% 50.57/15.82 % (2024140)Termination reason: Instruction limit
% 50.57/15.82 % (2024140)Termination phase: Saturation
% 50.57/15.82 % (2024140)Time elapsed: 0.152 s
% 50.57/15.82 % (2024140)Peak memory usage: 96 MB
% 50.57/15.82 % (2024140)Instructions burned: 524 (million)
% 50.57/15.82 % (2024142)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3877513699:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2868 on theBenchmark for (2868ds/1016Mi)
% 50.57/15.82 % (2024142)Instruction limit reached!
% 50.57/15.82 % (2024142)------------------------------
% 50.57/15.82 % (2024142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.57/15.82 % (2024142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.57/15.82 % (2024142)CaDiCaL version: 2.1.3
% 50.57/15.82 % (2024142)Termination reason: Instruction limit
% 50.57/15.82 % (2024142)Termination phase: Saturation
% 50.57/15.82 % (2024142)Time elapsed: 0.319 s
% 50.57/15.82 % (2024142)Peak memory usage: 122 MB
% 50.57/15.82 % (2024142)Instructions burned: 1017 (million)
% 50.57/15.82 % (2024144)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3633487392:i=14123:bd=preordered:ins=4_2863 on theBenchmark for (2863ds/14123Mi)
% 50.57/15.82 % (2024138)Instruction limit reached!
% 50.57/15.82 % (2024138)------------------------------
% 50.57/15.82 % (2024138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.57/15.82 % (2024138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.57/15.82 % (2024138)CaDiCaL version: 2.1.3
% 50.57/15.82 % (2024138)Termination reason: Instruction limit
% 50.57/15.82 % (2024138)Termination phase: Saturation
% 50.57/15.82 % (2024138)Time elapsed: 1.810 s
% 50.57/15.82 % (2024138)Peak memory usage: 141 MB
% 50.57/15.82 % (2024138)Instructions burned: 3034 (million)
% 50.57/15.82 % (2024146)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=104074166:i=5781:kws=precedence:bd=all:rawr=on_2861 on theBenchmark for (2861ds/5781Mi)
% 50.57/15.82 % (2024144)First to succeed.
% 50.57/15.82 % (2024144)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2024047"
% 50.57/15.82 % (2024144)Refutation found. Thanks to Tanya!
% 50.57/15.82 % SZS status Theorem for theBenchmark
% 50.57/15.82 % SZS output start Proof for theBenchmark
% See solution above
% 106.60/15.92 % (2024144)------------------------------
% 106.60/15.92 % (2024144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.60/15.92 % (2024144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.60/15.92 % (2024144)CaDiCaL version: 2.1.3
% 106.60/15.92 % (2024144)Termination reason: Refutation
% 106.60/15.92 % (2024144)Time elapsed: 1.027 s
% 106.60/15.92 % (2024144)Peak memory usage: 151 MB
% 106.60/15.92 % (2024144)Instructions burned: 3022 (million)
% 106.60/15.92 % (2024144)------------------------------
% 106.60/15.92 % (2024144)------------------------------
% 106.60/15.92 % (2024047)Success in time 14.968 s
% 106.60/15.92 % Vampire exiting
%------------------------------------------------------------------------------