%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : COL106-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:37:59 AM UTC 2026
% Result : Unsatisfiable 77.13s 11.85s
% Output : Refutation 79.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 16
% Syntax : Number of formulae : 71 ( 16 unt; 5 def)
% Number of atoms : 166 ( 57 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 158 ( 63 ~; 90 |; 0 &)
% ( 5 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 6 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 7 con; 0-4 aty)
% Number of variables : 41 ( 0 sgn 41 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(X0,X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| X2 = c_Comb_Ocomb_Oop_A_D_D(X0,X1)
| X0 = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X2)
| X0 = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(X0,X1,X2)),v_sko__uTG(X0,X1,X2))
| X2 = c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(X0,X1,X2),v_sko__uTH(X0,X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_OAp__parcontractE_0) ).
fof(f2,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(X0,X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_Comb_Ocomb_Oop_A_D_D(X0,X1) = X2
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X2) = X0
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(X0,X1,X2)),v_sko__uTG(X0,X1,X2)) = X0
| c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(X0,X1,X2),v_sko__uTH(X0,X1,X2)) = X2 ),
inference(reorient_equations,[],[f1]) ).
fof(f5,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(X0,X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(X0,v_sko__uTI(X0,X1,X2),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| X2 = c_Comb_Ocomb_Oop_A_D_D(X0,X1)
| X0 = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X2)
| X0 = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(X0,X1,X2)),v_sko__uTG(X0,X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_OAp__parcontractE_2) ).
fof(f6,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X0,v_sko__uTI(X0,X1,X2),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(X0,X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_Comb_Ocomb_Oop_A_D_D(X0,X1) = X2
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X2) = X0
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(X0,X1,X2)),v_sko__uTG(X0,X1,X2)) = X0 ),
inference(reorient_equations,[],[f5]) ).
fof(f15,axiom,
! [X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X0),X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| X1 = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_OK1__parcontractD__dest_0) ).
fof(f16,plain,
! [X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X0),X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(X0,X1)) = X1 ),
inference(reorient_equations,[],[f15]) ).
fof(f17,axiom,
! [X0,X1] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X0),X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(X0,v_sko__uTE(X0,X1),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_OK1__parcontractD__dest_1) ).
fof(f29,axiom,
! [X0] : c_in(c_Pair(X0,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_Oparcontract_Ointros__1_0) ).
fof(f30,axiom,
! [X0,X1] : c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X0),X1),X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_Oparcontract_Ointros__2_0) ).
fof(f58,axiom,
! [X0,X1] : c_Comb_Ocomb_OK != c_Comb_Ocomb_Oop_A_D_D(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_Ocomb_Odistinct__3__iff1_0) ).
fof(f59,plain,
! [X0,X1] : c_Comb_Ocomb_Oop_A_D_D(X0,X1) != c_Comb_Ocomb_OK,
inference(reorient_equations,[],[f58]) ).
fof(f64,axiom,
! [X2,X3,X0,X1] :
( c_Comb_Ocomb_Oop_A_D_D(X0,X1) != c_Comb_Ocomb_Oop_A_D_D(X2,X3)
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_Ocomb_Oinject__iff1_0) ).
fof(f65,axiom,
! [X2,X3,X0,X1] :
( c_Comb_Ocomb_Oop_A_D_D(X0,X1) != c_Comb_Ocomb_Oop_A_D_D(X2,X3)
| X1 = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_Ocomb_Oinject__iff1_1) ).
fof(f1503,negated_conjecture,
c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya),v_xb,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1504,negated_conjecture,
! [X0] :
( ~ c_in(c_Pair(v_xb,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_x,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f1506,plain,
~ c_in(c_Pair(v_x,v_xb,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(resolution,[],[f1504,f29]) ).
fof(f1511,definition,
( spl0_1
<=> v_xb = c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f1513,plain,
( v_xb = c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb))
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f1511]) ).
fof(f1519,definition,
( spl0_3
<=> c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f1520,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| spl0_3 ),
inference(avatar_component_clause,[],[f1519]) ).
fof(f1521,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f1519]) ).
fof(f1523,definition,
( spl0_4
<=> c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya) = v_xb ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f1524,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya) != v_xb
| spl0_4 ),
inference(avatar_component_clause,[],[f1523]) ).
fof(f1525,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya) = v_xb
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f1523]) ).
fof(f1543,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya) = v_xb
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb))
| v_xb = c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)) ),
inference(resolution,[],[f2,f1503]) ).
fof(f1550,definition,
( spl0_5
<=> c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f1551,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb))
| spl0_5 ),
inference(avatar_component_clause,[],[f1550]) ).
fof(f1552,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb))
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f1550]) ).
fof(f1553,plain,
( spl0_1
| spl0_5
| spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f1543,f1523,f1519,f1550,f1511]) ).
fof(f1613,plain,
( ! [X0,X1] :
( c_Comb_Ocomb_Oop_A_D_D(X0,X1) != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x)
| v_xb = X1 )
| ~ spl0_3 ),
inference(superposition,[],[f65,f1521]) ).
fof(f1616,plain,
( v_x = v_xb
| ~ spl0_3 ),
inference(equality_resolution,[],[f1613]) ).
fof(f1619,plain,
( ~ c_in(c_Pair(v_x,v_x,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_3 ),
inference(backward_demodulation,[],[f1506,f1616]) ).
fof(f1670,plain,
( $false
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f1619,f29]) ).
fof(f1671,plain,
~ spl0_3,
inference(avatar_contradiction_clause,[],[f1670]) ).
fof(f1696,plain,
( c_in(c_Pair(v_xb,v_x,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_4 ),
inference(superposition,[],[f30,f1525]) ).
fof(f1712,plain,
( ~ c_in(c_Pair(v_x,v_x,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_4 ),
inference(resolution,[],[f1696,f1504]) ).
fof(f1715,plain,
( $false
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f1712,f29]) ).
fof(f1716,plain,
~ spl0_4,
inference(avatar_contradiction_clause,[],[f1715]) ).
fof(f1722,plain,
( ! [X0,X1] :
( c_Comb_Ocomb_Oop_A_D_D(X0,X1) != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x)
| v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb) = X1 )
| ~ spl0_5 ),
inference(superposition,[],[f65,f1552]) ).
fof(f1727,plain,
( v_x = v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)
| ~ spl0_5 ),
inference(equality_resolution,[],[f1722]) ).
fof(f1731,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_x)
| ~ spl0_5 ),
inference(backward_demodulation,[],[f1552,f1727]) ).
fof(f1761,plain,
( ! [X0,X1] :
( c_Comb_Ocomb_Oop_A_D_D(X0,X1) != c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x)
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)) = X0 )
| ~ spl0_5 ),
inference(superposition,[],[f64,f1731]) ).
fof(f1764,plain,
( c_Comb_Ocomb_OK = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb))
| ~ spl0_5 ),
inference(equality_resolution,[],[f1761]) ).
fof(f1765,plain,
( $false
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f1764,f59]) ).
fof(f1766,plain,
~ spl0_5,
inference(avatar_contradiction_clause,[],[f1765]) ).
fof(f3460,definition,
( spl0_53
<=> c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f3461,plain,
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| spl0_53 ),
inference(avatar_component_clause,[],[f3460]) ).
fof(f3462,plain,
( c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f3460]) ).
fof(f3483,plain,
( c_in(c_Pair(v_x,v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_53 ),
inference(resolution,[],[f3462,f17]) ).
fof(f3486,plain,
( v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)))
| ~ spl0_53 ),
inference(resolution,[],[f3462,f16]) ).
fof(f3518,plain,
( ! [X0] : c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),X0),v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_53 ),
inference(superposition,[],[f30,f3486]) ).
fof(f3547,plain,
( c_in(c_Pair(v_xb,v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_1
| ~ spl0_53 ),
inference(superposition,[],[f3518,f1513]) ).
fof(f3551,plain,
( ~ c_in(c_Pair(v_x,v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ spl0_1
| ~ spl0_53 ),
inference(resolution,[],[f3547,f1504]) ).
fof(f3555,plain,
( $false
| ~ spl0_1
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f3551,f3483]) ).
fof(f3556,plain,
( ~ spl0_1
| ~ spl0_53 ),
inference(avatar_contradiction_clause,[],[f3555]) ).
fof(f3631,plain,
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya),v_xb,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya) = v_xb
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb))
| spl0_53 ),
inference(resolution,[],[f3461,f6]) ).
fof(f3634,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya) = v_xb
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb))
| spl0_53 ),
inference(forward_subsumption_resolution,[],[f3631,f1503]) ).
fof(f3636,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)
| c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb))
| spl0_4
| spl0_53 ),
inference(forward_subsumption_resolution,[],[f3634,f1524]) ).
fof(f3638,plain,
( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb))
| spl0_3
| spl0_4
| spl0_53 ),
inference(forward_subsumption_resolution,[],[f3636,f1520]) ).
fof(f3641,plain,
( $false
| spl0_3
| spl0_4
| spl0_5
| spl0_53 ),
inference(forward_subsumption_resolution,[],[f3638,f1551]) ).
fof(f3642,plain,
( spl0_3
| spl0_4
| spl0_5
| spl0_53 ),
inference(avatar_contradiction_clause,[],[f3641]) ).
cnf(s2,plain,
( spl0_1
| spl0_3
| spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f1553]) ).
cnf(s3,plain,
~ spl0_3,
inference(sat_conversion,[],[f1671]) ).
cnf(s4,plain,
~ spl0_4,
inference(sat_conversion,[],[f1716]) ).
cnf(s5,plain,
~ spl0_5,
inference(sat_conversion,[],[f1766]) ).
cnf(s58,plain,
( ~ spl0_1
| ~ spl0_53 ),
inference(sat_conversion,[],[f3556]) ).
cnf(s63,plain,
( spl0_3
| spl0_4
| spl0_5
| spl0_53 ),
inference(sat_conversion,[],[f3642]) ).
cnf(s69,plain,
spl0_53,
inference(rat,[],[s63,s4,s5,s3]) ).
cnf(s70,plain,
~ spl0_1,
inference(rat,[],[s58,s69]) ).
cnf(s71,plain,
$false,
inference(rat,[],[s2,s5,s4,s3,s70]) ).
fof(f3643,plain,
$false,
inference(avatar_sat_refutation,[],[s71]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COL106-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.19 % Computer : n020.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Mon Sep 28 21:40:19 UTC 2026
% 0.10/0.19 % CPUTime :
% 0.10/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.23 Running first-order theorem proving
% 0.10/0.23 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.14/2.44 % (598446)Input is clausal, will run a generic CNF schedule.
% 12.14/2.44 % (598587)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2864074149:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 12.14/2.44 % (598586)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=118818989:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 12.14/2.44 % (598596)dis-21_1_sil=8000:lcm=predicate:random_seed=2103681933:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 12.14/2.44 % (598592)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4189289854:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 12.14/2.44 % (598594)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=753570695:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 12.14/2.44 % (598590)lrs+10_1_sil=8000:sp=occurrence:random_seed=3082562534:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 12.14/2.44 % (598588)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=924040124:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 12.14/2.44 % (598590)Refutation not found, incomplete strategy
% 12.14/2.44 % (598590)------------------------------
% 12.14/2.44 % (598590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.14/2.44 % (598590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.14/2.44 % (598590)CaDiCaL version: 2.1.3
% 12.14/2.44 % (598590)Termination reason: Refutation not found, incomplete strategy
% 12.14/2.44 % (598590)Time elapsed: 0.003 s
% 12.14/2.44 % (598590)Peak memory usage: 88 MB
% 12.14/2.44 % (598590)Instructions burned: 3 (million)
% 12.14/2.44 % (598592)Refutation not found, incomplete strategy
% 12.14/2.44 % (598592)------------------------------
% 12.14/2.44 % (598592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.14/2.44 % (598592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.14/2.44 % (598592)CaDiCaL version: 2.1.3
% 12.14/2.44 % (598592)Termination reason: Refutation not found, incomplete strategy
% 12.14/2.44 % (598592)Time elapsed: 0.005 s
% 12.14/2.44 % (598592)Peak memory usage: 88 MB
% 12.14/2.44 % (598592)Instructions burned: 6 (million)
% 12.14/2.44 % (598596)Instruction limit reached!
% 12.14/2.44 % (598596)------------------------------
% 12.14/2.44 % (598596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.14/2.44 % (598596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.14/2.44 % (598596)CaDiCaL version: 2.1.3
% 12.14/2.44 % (598596)Termination reason: Instruction limit
% 12.14/2.44 % (598596)Termination phase: Saturation
% 12.14/2.44 % (598596)Time elapsed: 0.066 s
% 12.14/2.44 % (598596)Peak memory usage: 89 MB
% 12.14/2.44 % (598596)Instructions burned: 117 (million)
% 12.14/2.44 % (598594)Instruction limit reached!
% 12.14/2.44 % (598594)------------------------------
% 12.14/2.44 % (598594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.14/2.44 % (598594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.14/2.44 % (598594)CaDiCaL version: 2.1.3
% 12.14/2.44 % (598594)Termination reason: Instruction limit
% 12.14/2.44 % (598594)Termination phase: Saturation
% 12.14/2.44 % (598594)Time elapsed: 0.097 s
% 12.14/2.44 % (598594)Peak memory usage: 90 MB
% 12.14/2.44 % (598594)Instructions burned: 181 (million)
% 12.14/2.44 % (598638)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1590226607:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 12.14/2.44 % (598638)Refutation not found, incomplete strategy
% 12.14/2.44 % (598638)------------------------------
% 12.14/2.44 % (598638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.14/2.44 % (598638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.14/2.44 % (598638)CaDiCaL version: 2.1.3
% 12.14/2.44 % (598638)Termination reason: Refutation not found, incomplete strategy
% 12.14/2.44 % (598638)Time elapsed: 0.003 s
% 12.14/2.44 % (598638)Peak memory usage: 88 MB
% 12.14/2.44 % (598638)Instructions burned: 3 (million)
% 12.14/2.44 % (598590)------------------------------
% 12.14/2.44 % (598590)------------------------------
% 24.01/4.04 % (598592)------------------------------
% 24.01/4.04 % (598592)------------------------------
% 24.01/4.04 % (598639)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=285242220:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 24.01/4.04 % (598639)Instruction limit reached!
% 24.01/4.04 % (598639)------------------------------
% 24.01/4.04 % (598639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.01/4.04 % (598639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.01/4.04 % (598639)CaDiCaL version: 2.1.3
% 24.01/4.04 % (598639)Termination reason: Instruction limit
% 24.01/4.04 % (598639)Termination phase: Saturation
% 24.01/4.04 % (598639)Time elapsed: 0.104 s
% 24.01/4.04 % (598639)Peak memory usage: 90 MB
% 24.01/4.04 % (598639)Instructions burned: 189 (million)
% 24.01/4.04 % (598689)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2729092718:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 24.01/4.04 % (598690)lrs+10_64_to=lpo:sil=8000:random_seed=3610826765:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 24.01/4.04 % (598689)Refutation not found, incomplete strategy
% 24.01/4.04 % (598689)------------------------------
% 24.01/4.04 % (598689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.01/4.04 % (598689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.01/4.04 % (598689)CaDiCaL version: 2.1.3
% 24.01/4.04 % (598689)Termination reason: Refutation not found, incomplete strategy
% 24.01/4.04 % (598689)Time elapsed: 0.005 s
% 24.01/4.04 % (598689)Peak memory usage: 88 MB
% 24.01/4.04 % (598689)Instructions burned: 7 (million)
% 24.01/4.04 % (598638)------------------------------
% 24.01/4.04 % (598638)------------------------------
% 24.01/4.04 % (598690)Instruction limit reached!
% 24.01/4.04 % (598690)------------------------------
% 24.01/4.04 % (598690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.01/4.04 % (598690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.01/4.04 % (598690)CaDiCaL version: 2.1.3
% 24.01/4.04 % (598690)Termination reason: Instruction limit
% 24.01/4.04 % (598690)Termination phase: Saturation
% 24.01/4.04 % (598690)Time elapsed: 0.079 s
% 24.01/4.04 % (598690)Peak memory usage: 89 MB
% 24.01/4.04 % (598690)Instructions burned: 126 (million)
% 24.01/4.04 % (598691)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2650526453:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 24.01/4.04 % (598694)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2530853085:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 24.01/4.04 % (598695)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2084125244:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 24.01/4.04 % (598691)Instruction limit reached!
% 24.01/4.04 % (598691)------------------------------
% 24.01/4.04 % (598691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.01/4.04 % (598691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.01/4.04 % (598691)CaDiCaL version: 2.1.3
% 24.01/4.04 % (598691)Termination reason: Instruction limit
% 24.01/4.04 % (598691)Termination phase: Saturation
% 24.01/4.04 % (598691)Time elapsed: 0.123 s
% 24.01/4.04 % (598691)Peak memory usage: 90 MB
% 24.01/4.04 % (598691)Instructions burned: 194 (million)
% 24.01/4.04 % (598689)------------------------------
% 24.01/4.04 % (598689)------------------------------
% 24.01/4.04 % (598694)Instruction limit reached!
% 24.01/4.04 % (598694)------------------------------
% 24.01/4.04 % (598694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.01/4.04 % (598694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.01/4.04 % (598694)CaDiCaL version: 2.1.3
% 24.01/4.04 % (598694)Termination reason: Instruction limit
% 24.01/4.04 % (598694)Termination phase: Saturation
% 24.01/4.04 % (598694)Time elapsed: 0.090 s
% 24.01/4.04 % (598694)Peak memory usage: 91 MB
% 24.01/4.04 % (598694)Instructions burned: 158 (million)
% 24.01/4.04 % (598699)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=954018452:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 24.01/4.04 % (598700)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2972609803:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 34.92/5.63 % (598699)Instruction limit reached!
% 34.92/5.63 % (598699)------------------------------
% 34.92/5.63 % (598699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.92/5.63 % (598699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.92/5.63 % (598699)CaDiCaL version: 2.1.3
% 34.92/5.63 % (598699)Termination reason: Instruction limit
% 34.92/5.63 % (598699)Termination phase: Saturation
% 34.92/5.63 % (598699)Time elapsed: 0.049 s
% 34.92/5.63 % (598699)Peak memory usage: 89 MB
% 34.92/5.63 % (598699)Instructions burned: 107 (million)
% 34.92/5.63 % (598701)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3767087432:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 34.92/5.63 % (598700)Instruction limit reached!
% 34.92/5.63 % (598700)------------------------------
% 34.92/5.63 % (598700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.92/5.63 % (598700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.92/5.63 % (598700)CaDiCaL version: 2.1.3
% 34.92/5.63 % (598700)Termination reason: Instruction limit
% 34.92/5.63 % (598700)Termination phase: Saturation
% 34.92/5.63 % (598700)Time elapsed: 0.066 s
% 34.92/5.63 % (598700)Peak memory usage: 90 MB
% 34.92/5.63 % (598700)Instructions burned: 108 (million)
% 34.92/5.63 % (598701)Instruction limit reached!
% 34.92/5.63 % (598701)------------------------------
% 34.92/5.63 % (598701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.92/5.63 % (598701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.92/5.63 % (598701)CaDiCaL version: 2.1.3
% 34.92/5.63 % (598701)Termination reason: Instruction limit
% 34.92/5.63 % (598701)Termination phase: Saturation
% 34.92/5.63 % (598701)Time elapsed: 0.127 s
% 34.92/5.63 % (598701)Peak memory usage: 89 MB
% 34.92/5.63 % (598701)Instructions burned: 244 (million)
% 34.92/5.63 % (598704)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1432385101:cond=fast:i=5208:av=off_2989 on theBenchmark for (2989ds/5208Mi)
% 34.92/5.63 % (598706)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2323609573:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 34.92/5.63 % (598706)Refutation not found, incomplete strategy
% 34.92/5.63 % (598706)------------------------------
% 34.92/5.63 % (598706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.92/5.63 % (598706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.92/5.63 % (598706)CaDiCaL version: 2.1.3
% 34.92/5.63 % (598706)Termination reason: Refutation not found, incomplete strategy
% 34.92/5.63 % (598706)Time elapsed: 0.004 s
% 34.92/5.63 % (598706)Peak memory usage: 89 MB
% 34.92/5.63 % (598706)Instructions burned: 4 (million)
% 34.92/5.63 % (598707)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1025586779:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 34.92/5.63 % (598706)------------------------------
% 34.92/5.63 % (598706)------------------------------
% 34.92/5.63 % (598707)Instruction limit reached!
% 34.92/5.63 % (598707)------------------------------
% 34.92/5.63 % (598707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.92/5.63 % (598707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.92/5.63 % (598707)CaDiCaL version: 2.1.3
% 34.92/5.63 % (598707)Termination reason: Instruction limit
% 34.92/5.63 % (598707)Termination phase: Saturation
% 34.92/5.63 % (598707)Time elapsed: 0.257 s
% 34.92/5.63 % (598707)Peak memory usage: 98 MB
% 34.92/5.63 % (598707)Instructions burned: 500 (million)
% 34.92/5.63 % (598711)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3538264667:i=191:fgj=on:bd=all_2985 on theBenchmark for (2985ds/191Mi)
% 34.92/5.63 % (598712)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1984939879:i=264:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/264Mi)
% 34.92/5.63 % (598711)Instruction limit reached!
% 34.92/5.63 % (598711)------------------------------
% 34.92/5.63 % (598711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.92/5.63 % (598711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.92/5.63 % (598711)CaDiCaL version: 2.1.3
% 34.92/5.63 % (598711)Termination reason: Instruction limit
% 34.92/5.63 % (598711)Termination phase: Saturation
% 57.75/8.94 % (598711)Time elapsed: 0.134 s
% 57.75/8.94 % (598711)Peak memory usage: 92 MB
% 57.75/8.94 % (598711)Instructions burned: 192 (million)
% 57.75/8.94 % (598712)Instruction limit reached!
% 57.75/8.94 % (598712)------------------------------
% 57.75/8.94 % (598712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.75/8.94 % (598712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.75/8.94 % (598712)CaDiCaL version: 2.1.3
% 57.75/8.94 % (598712)Termination reason: Instruction limit
% 57.75/8.94 % (598712)Termination phase: Saturation
% 57.75/8.94 % (598712)Time elapsed: 0.147 s
% 57.75/8.94 % (598712)Peak memory usage: 92 MB
% 57.75/8.94 % (598712)Instructions burned: 264 (million)
% 57.75/8.94 % (598715)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2587276686:cond=on:i=156:bs=on:gtg=exists_all:er=known_2982 on theBenchmark for (2982ds/156Mi)
% 57.75/8.94 % (598715)Instruction limit reached!
% 57.75/8.94 % (598715)------------------------------
% 57.75/8.94 % (598715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.75/8.94 % (598715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.75/8.94 % (598715)CaDiCaL version: 2.1.3
% 57.75/8.94 % (598715)Termination reason: Instruction limit
% 57.75/8.94 % (598715)Termination phase: Saturation
% 57.75/8.94 % (598715)Time elapsed: 0.095 s
% 57.75/8.94 % (598715)Peak memory usage: 90 MB
% 57.75/8.94 % (598715)Instructions burned: 157 (million)
% 57.75/8.94 % (598716)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=575349412:i=3256:kws=precedence:bd=preordered:av=off_2981 on theBenchmark for (2981ds/3256Mi)
% 57.75/8.94 % (598718)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2577123849:i=537:av=off:ss=included_2979 on theBenchmark for (2979ds/537Mi)
% 57.75/8.94 % (598718)Instruction limit reached!
% 57.75/8.94 % (598718)------------------------------
% 57.75/8.94 % (598718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.75/8.94 % (598718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.75/8.94 % (598718)CaDiCaL version: 2.1.3
% 57.75/8.94 % (598718)Termination reason: Instruction limit
% 57.75/8.94 % (598718)Termination phase: Saturation
% 57.75/8.94 % (598718)Time elapsed: 0.284 s
% 57.75/8.94 % (598718)Peak memory usage: 94 MB
% 57.75/8.94 % (598718)Instructions burned: 538 (million)
% 57.75/8.94 % (598721)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3231717412:i=180:bd=preordered:av=off_2975 on theBenchmark for (2975ds/180Mi)
% 57.75/8.94 % (598721)Instruction limit reached!
% 57.75/8.94 % (598721)------------------------------
% 57.75/8.94 % (598721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.75/8.94 % (598721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.75/8.94 % (598721)CaDiCaL version: 2.1.3
% 57.75/8.94 % (598721)Termination reason: Instruction limit
% 57.75/8.94 % (598721)Termination phase: Saturation
% 57.75/8.94 % (598721)Time elapsed: 0.101 s
% 57.75/8.94 % (598721)Peak memory usage: 95 MB
% 57.75/8.94 % (598721)Instructions burned: 182 (million)
% 57.75/8.94 % (598723)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=3029460244:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2972 on theBenchmark for (2972ds/10307Mi)
% 57.75/8.94 % (598695)Instruction limit reached!
% 57.75/8.94 % (598695)------------------------------
% 57.75/8.94 % (598695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.75/8.94 % (598695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.75/8.94 % (598695)CaDiCaL version: 2.1.3
% 57.75/8.94 % (598695)Termination reason: Instruction limit
% 57.75/8.94 % (598695)Termination phase: Saturation
% 57.75/8.94 % (598695)Time elapsed: 2.168 s
% 57.75/8.94 % (598695)Peak memory usage: 148 MB
% 57.75/8.94 % (598695)Instructions burned: 3395 (million)
% 57.75/8.94 % (598725)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=576835150:i=412:gtgl=4:gtg=exists_all_2970 on theBenchmark for (2970ds/412Mi)
% 57.75/8.94 % (598725)Instruction limit reached!
% 57.75/8.94 % (598725)------------------------------
% 57.75/8.94 % (598725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.75/8.94 % (598725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.13/11.85 % (598725)CaDiCaL version: 2.1.3
% 77.13/11.85 % (598725)Termination reason: Instruction limit
% 77.13/11.85 % (598725)Termination phase: Saturation
% 77.13/11.85 % (598725)Time elapsed: 0.215 s
% 77.13/11.85 % (598725)Peak memory usage: 96 MB
% 77.13/11.85 % (598725)Instructions burned: 413 (million)
% 77.13/11.85 % (598727)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=2007903581:s2pl=no:i=8478:s2at=4:nm=6_2966 on theBenchmark for (2966ds/8478Mi)
% 77.13/11.85 % (598716)Instruction limit reached!
% 77.13/11.85 % (598716)------------------------------
% 77.13/11.85 % (598716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.13/11.85 % (598716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.13/11.85 % (598716)CaDiCaL version: 2.1.3
% 77.13/11.85 % (598716)Termination reason: Instruction limit
% 77.13/11.85 % (598716)Termination phase: Saturation
% 77.13/11.85 % (598716)Time elapsed: 1.888 s
% 77.13/11.85 % (598716)Peak memory usage: 152 MB
% 77.13/11.85 % (598716)Instructions burned: 3257 (million)
% 77.13/11.85 % (598729)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=1278727230:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2960 on theBenchmark for (2960ds/303Mi)
% 77.13/11.85 % (598704)Instruction limit reached!
% 77.13/11.85 % (598704)------------------------------
% 77.13/11.85 % (598704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.13/11.85 % (598704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.13/11.85 % (598704)CaDiCaL version: 2.1.3
% 77.13/11.85 % (598704)Termination reason: Instruction limit
% 77.13/11.85 % (598704)Termination phase: Saturation
% 77.13/11.85 % (598704)Time elapsed: 3.083 s
% 77.13/11.85 % (598704)Peak memory usage: 156 MB
% 77.13/11.85 % (598704)Instructions burned: 5209 (million)
% 77.13/11.85 % (598729)Instruction limit reached!
% 77.13/11.85 % (598729)------------------------------
% 77.13/11.85 % (598729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.13/11.85 % (598729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.13/11.85 % (598729)CaDiCaL version: 2.1.3
% 77.13/11.85 % (598729)Termination reason: Instruction limit
% 77.13/11.85 % (598729)Termination phase: Saturation
% 77.13/11.85 % (598729)Time elapsed: 0.155 s
% 77.13/11.85 % (598729)Peak memory usage: 93 MB
% 77.13/11.85 % (598729)Instructions burned: 303 (million)
% 77.13/11.85 % (598731)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3426563162:st=4:i=720:sd=3:fsr=off:ss=axioms_2957 on theBenchmark for (2957ds/720Mi)
% 77.13/11.85 % (598732)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3041525443:i=598:bs=on:bd=preordered:av=off:ss=axioms_2957 on theBenchmark for (2957ds/598Mi)
% 77.13/11.85 % (598732)Instruction limit reached!
% 77.13/11.85 % (598732)------------------------------
% 77.13/11.85 % (598732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.13/11.85 % (598732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.13/11.85 % (598732)CaDiCaL version: 2.1.3
% 77.13/11.85 % (598732)Termination reason: Instruction limit
% 77.13/11.85 % (598732)Termination phase: Saturation
% 77.13/11.85 % (598732)Time elapsed: 0.328 s
% 77.13/11.85 % (598732)Peak memory usage: 95 MB
% 77.13/11.85 % (598732)Instructions burned: 598 (million)
% 77.13/11.85 % (598731)Instruction limit reached!
% 77.13/11.85 % (598731)------------------------------
% 77.13/11.85 % (598731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.13/11.85 % (598731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.13/11.85 % (598731)CaDiCaL version: 2.1.3
% 77.13/11.85 % (598731)Termination reason: Instruction limit
% 77.13/11.85 % (598731)Termination phase: Saturation
% 77.13/11.85 % (598731)Time elapsed: 0.380 s
% 77.13/11.85 % (598731)Peak memory usage: 98 MB
% 77.13/11.85 % (598731)Instructions burned: 721 (million)
% 77.13/11.85 % (598735)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2402178352:i=2989:sd=3:ss=axioms:sgt=60_2952 on theBenchmark for (2952ds/2989Mi)
% 77.13/11.85 % (598736)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=1225782128:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2952 on theBenchmark for (2952ds/1997Mi)
% 77.13/11.85 % (598736)Instruction limit reached!
% 77.13/11.85 % (598736)------------------------------
% 77.13/11.85 % (598736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.13/11.85 % (598736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.13/11.85 % (598736)CaDiCaL version: 2.1.3
% 77.13/11.85 % (598736)Termination reason: Instruction limit
% 77.13/11.85 % (598736)Termination phase: Saturation
% 77.13/11.85 % (598736)Time elapsed: 1.283 s
% 77.13/11.85 % (598736)Peak memory usage: 138 MB
% 77.13/11.85 % (598736)Instructions burned: 1997 (million)
% 77.13/11.85 % (598739)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=2186402934:i=2088:bd=preordered:av=off_2937 on theBenchmark for (2937ds/2088Mi)
% 77.13/11.85 % (598735)Instruction limit reached!
% 77.13/11.85 % (598735)------------------------------
% 77.13/11.85 % (598735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.13/11.85 % (598735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.13/11.85 % (598735)CaDiCaL version: 2.1.3
% 77.13/11.85 % (598735)Termination reason: Instruction limit
% 77.13/11.85 % (598735)Termination phase: Saturation
% 77.13/11.85 % (598735)Time elapsed: 1.822 s
% 77.13/11.85 % (598735)Peak memory usage: 144 MB
% 77.13/11.85 % (598735)Instructions burned: 2989 (million)
% 77.13/11.85 % (598741)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3158668862:i=1098:nicw=on_2932 on theBenchmark for (2932ds/1098Mi)
% 77.13/11.85 % (598741)Instruction limit reached!
% 77.13/11.85 % (598741)------------------------------
% 77.13/11.85 % (598741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.13/11.85 % (598741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.13/11.85 % (598741)CaDiCaL version: 2.1.3
% 77.13/11.85 % (598741)Termination reason: Instruction limit
% 77.13/11.85 % (598741)Termination phase: Saturation
% 77.13/11.85 % (598741)Time elapsed: 0.597 s
% 77.13/11.85 % (598741)Peak memory usage: 105 MB
% 77.13/11.85 % (598741)Instructions burned: 1099 (million)
% 77.13/11.85 % (598743)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1415326157:i=433:bd=preordered_2924 on theBenchmark for (2924ds/433Mi)
% 77.13/11.85 % (598739)Instruction limit reached!
% 77.13/11.85 % (598739)------------------------------
% 77.13/11.85 % (598739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.13/11.85 % (598739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.13/11.85 % (598739)CaDiCaL version: 2.1.3
% 77.13/11.85 % (598739)Termination reason: Instruction limit
% 77.13/11.85 % (598739)Termination phase: Saturation
% 77.13/11.85 % (598739)Time elapsed: 1.288 s
% 77.13/11.85 % (598739)Peak memory usage: 140 MB
% 77.13/11.85 % (598739)Instructions burned: 2089 (million)
% 77.13/11.85 % (598745)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=4041083601:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2922 on theBenchmark for (2922ds/2942Mi)
% 77.13/11.85 % (598743)Instruction limit reached!
% 77.13/11.85 % (598743)------------------------------
% 77.13/11.85 % (598743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.13/11.85 % (598743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.13/11.85 % (598743)CaDiCaL version: 2.1.3
% 77.13/11.85 % (598743)Termination reason: Instruction limit
% 77.13/11.85 % (598743)Termination phase: Saturation
% 77.13/11.85 % (598743)Time elapsed: 0.260 s
% 77.13/11.85 % (598743)Peak memory usage: 94 MB
% 77.13/11.85 % (598743)Instructions burned: 434 (million)
% 77.13/11.85 % (598747)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=645655541:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2920 on theBenchmark for (2920ds/6922Mi)
% 77.13/11.85 % (598727)Instruction limit reached!
% 77.13/11.85 % (598727)------------------------------
% 77.13/11.85 % (598727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.13/11.85 % (598727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.13/11.85 % (598727)CaDiCaL version: 2.1.3
% 77.13/11.85 % (598727)Termination reason: Instruction limit
% 77.13/11.85 % (598727)Termination phase: Saturation
% 77.13/11.85 % (598727)Time elapsed: 4.734 s
% 77.13/11.85 % (598727)Peak memory usage: 198 MB
% 77.13/11.85 % (598727)Instructions burned: 8478 (million)
% 77.13/11.85 % (598749)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=1738819226:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2917 on theBenchmark for (2917ds/596Mi)
% 77.13/11.85 % (598749)Instruction limit reached!
% 77.13/11.85 % (598749)------------------------------
% 77.13/11.85 % (598749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.13/11.85 % (598749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.13/11.85 % (598749)CaDiCaL version: 2.1.3
% 77.13/11.85 % (598749)Termination reason: Instruction limit
% 77.13/11.85 % (598749)Termination phase: Saturation
% 77.13/11.85 % (598749)Time elapsed: 0.325 s
% 77.13/11.85 % (598749)Peak memory usage: 97 MB
% 77.13/11.85 % (598749)Instructions burned: 596 (million)
% 77.13/11.85 % (598751)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=255075636:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2912 on theBenchmark for (2912ds/4123Mi)
% 77.13/11.85 % (598723)Instruction limit reached!
% 77.13/11.85 % (598723)------------------------------
% 77.13/11.85 % (598723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.13/11.85 % (598723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.13/11.85 % (598723)CaDiCaL version: 2.1.3
% 77.13/11.85 % (598723)Termination reason: Instruction limit
% 77.13/11.85 % (598723)Termination phase: Saturation
% 77.13/11.85 % (598723)Time elapsed: 6.516 s
% 77.13/11.85 % (598723)Peak memory usage: 163 MB
% 77.13/11.85 % (598723)Instructions burned: 10307 (million)
% 77.13/11.85 % (598753)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2345682194:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2905 on theBenchmark for (2905ds/16411Mi)
% 77.13/11.85 % (598745)Instruction limit reached!
% 77.13/11.85 % (598745)------------------------------
% 77.13/11.85 % (598745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.13/11.85 % (598745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.13/11.85 % (598745)CaDiCaL version: 2.1.3
% 77.13/11.85 % (598745)Termination reason: Instruction limit
% 77.13/11.85 % (598745)Termination phase: Saturation
% 77.13/11.85 % (598745)Time elapsed: 1.792 s
% 77.13/11.85 % (598745)Peak memory usage: 144 MB
% 77.13/11.85 % (598745)Instructions burned: 2943 (million)
% 77.13/11.85 % (598755)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3860908107:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2903 on theBenchmark for (2903ds/1670Mi)
% 77.13/11.85 % (598753)First to succeed.
% 77.13/11.85 % (598753)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-598446"
% 77.13/11.85 % (598755)Instruction limit reached!
% 77.13/11.85 % (598755)------------------------------
% 77.13/11.85 % (598755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.13/11.85 % (598755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.13/11.85 % (598755)CaDiCaL version: 2.1.3
% 77.13/11.85 % (598755)Termination reason: Instruction limit
% 77.13/11.85 % (598755)Termination phase: Saturation
% 77.13/11.85 % (598755)Time elapsed: 1.023 s
% 77.13/11.85 % (598755)Peak memory usage: 138 MB
% 77.13/11.85 % (598755)Instructions burned: 1670 (million)
% 77.13/11.85 % (598757)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=3160270034:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2891 on theBenchmark for (2891ds/1722Mi)
% 77.13/11.85 % (598753)Refutation found. Thanks to Tanya!
% 77.13/11.85 % SZS status Unsatisfiable for theBenchmark
% 77.13/11.85 % SZS output start Proof for theBenchmark
% See solution above
% 79.48/12.05 % (598753)------------------------------
% 79.48/12.05 % (598753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.48/12.05 % (598753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.48/12.05 % (598753)CaDiCaL version: 2.1.3
% 79.48/12.05 % (598753)Termination reason: Refutation
% 79.48/12.05 % (598753)Time elapsed: 1.276 s
% 79.48/12.05 % (598753)Peak memory usage: 138 MB
% 79.48/12.05 % (598753)Instructions burned: 2040 (million)
% 79.48/12.05 % (598753)------------------------------
% 79.48/12.05 % (598753)------------------------------
% 79.48/12.05 % (598446)Success in time 11.17 s
% 79.48/12.05 % Vampire exiting
%------------------------------------------------------------------------------