%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR228+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.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:44:08 AM UTC 2026
% Result : Theorem 17.90s 5.04s
% Output : Refutation 32.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 23
% Syntax : Number of formulae : 119 ( 36 unt; 5 def)
% Number of atoms : 574 ( 7 equ)
% Maximal formula atoms : 80 ( 4 avg)
% Number of connectives : 687 ( 232 ~; 222 |; 204 &)
% ( 26 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 25 ( 23 usr; 6 prp; 0-7 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 285 ( 0 sgn 277 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2] :
( ( p__d__subclass(X0,X1)
& p__d__subclass(X1,X2) )
=> p__d__subclass(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',predefinitionsA8) ).
fof(f4,axiom,
! [X0,X1,X2] :
( ( p__d__instance(X0,X1)
& p__d__subclass(X1,X2) )
=> p__d__instance(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',predefinitionsA12) ).
fof(f5,axiom,
! [X0,X1] :
( p__d__disjoint(X0,X1)
<=> ! [X2] :
( ~ p__d__instance(X2,X0)
| ~ p__d__instance(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',predefinitionsA15) ).
fof(f6,axiom,
( ! [X0,X1,X2] :
( p__d__partition3(X0,X1,X2)
<=> ( p__d__exhaustiveDecomposition3(X0,X1,X2)
& p__d__disjointDecomposition3(X0,X1,X2) ) )
& ! [X0,X1,X2,X3] :
( p__d__partition4(X0,X1,X2,X3)
<=> ( p__d__exhaustiveDecomposition4(X0,X1,X2,X3)
& p__d__disjointDecomposition4(X0,X1,X2,X3) ) )
& ! [X0,X1,X2,X3,X4] :
( p__d__partition5(X0,X1,X2,X3,X4)
<=> ( p__d__exhaustiveDecomposition5(X0,X1,X2,X3,X4)
& p__d__disjointDecomposition5(X0,X1,X2,X3,X4) ) )
& ! [X0,X1,X2,X3,X4,X5] :
( p__d__partition6(X0,X1,X2,X3,X4,X5)
<=> ( p__d__exhaustiveDecomposition6(X0,X1,X2,X3,X4,X5)
& p__d__disjointDecomposition6(X0,X1,X2,X3,X4,X5) ) )
& ! [X0,X1,X2,X3,X4,X5,X6] :
( p__d__partition7(X0,X1,X2,X3,X4,X5,X6)
<=> ( p__d__exhaustiveDecomposition7(X0,X1,X2,X3,X4,X5,X6)
& p__d__disjointDecomposition7(X0,X1,X2,X3,X4,X5,X6) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',predefinitionsA18) ).
fof(f8,axiom,
( ! [X0,X1,X2] :
( p__d__disjointDecomposition3(X0,X1,X2)
<=> p__d__disjoint(X1,X2) )
& ! [X0,X1,X2,X3] :
( p__d__disjointDecomposition4(X0,X1,X2,X3)
<=> ( p__d__disjoint(X1,X2)
& p__d__disjoint(X1,X3)
& p__d__disjoint(X2,X3) ) )
& ! [X0,X1,X2,X3,X4] :
( p__d__disjointDecomposition5(X0,X1,X2,X3,X4)
<=> ( p__d__disjoint(X1,X2)
& p__d__disjoint(X1,X3)
& p__d__disjoint(X1,X4)
& p__d__disjoint(X2,X3)
& p__d__disjoint(X2,X4)
& p__d__disjoint(X3,X4) ) )
& ! [X0,X1,X2,X3,X4,X5] :
( p__d__disjointDecomposition6(X0,X1,X2,X3,X4,X5)
<=> ( p__d__disjoint(X1,X2)
& p__d__disjoint(X1,X3)
& p__d__disjoint(X1,X4)
& p__d__disjoint(X1,X5)
& p__d__disjoint(X2,X3)
& p__d__disjoint(X2,X4)
& p__d__disjoint(X2,X5)
& p__d__disjoint(X3,X4)
& p__d__disjoint(X3,X5)
& p__d__disjoint(X4,X5) ) )
& ! [X0,X1,X2,X3,X4,X5,X6] :
( p__d__disjointDecomposition7(X0,X1,X2,X3,X4,X5,X6)
<=> ( p__d__disjoint(X1,X2)
& p__d__disjoint(X1,X3)
& p__d__disjoint(X1,X4)
& p__d__disjoint(X1,X5)
& p__d__disjoint(X1,X6)
& p__d__disjoint(X2,X3)
& p__d__disjoint(X2,X4)
& p__d__disjoint(X2,X5)
& p__d__disjoint(X2,X6)
& p__d__disjoint(X3,X4)
& p__d__disjoint(X3,X5)
& p__d__disjoint(X3,X6)
& p__d__disjoint(X4,X5)
& p__d__disjoint(X4,X6)
& p__d__disjoint(X5,X6) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',predefinitionsA24) ).
fof(f107,axiom,
p__d__partition3(c__Entity,c__Physical,c__Abstract),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA173) ).
fof(f110,axiom,
! [X0] :
( p__d__subclass(X0,c__Entity)
=> ? [X1] : p__d__instance(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA176) ).
fof(f112,axiom,
p__d__subclass(c__Physical,c__Entity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA178) ).
fof(f113,axiom,
p__d__partition3(c__Physical,c__Object,c__Process),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA179) ).
fof(f115,axiom,
p__d__subclass(c__Object,c__Physical),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA181) ).
fof(f233,axiom,
p__d__subclass(c__Process,c__Physical),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA324) ).
fof(f239,axiom,
p__d__subclass(c__Abstract,c__Entity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA330) ).
fof(f1677,axiom,
p__d__subclass(c__Motion,c__Process),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2422) ).
fof(f1721,axiom,
p__d__subclass(c__Transfer,c__Translocation),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2472) ).
fof(f1726,axiom,
p__d__subclass(c__Removing,c__Transfer),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2477) ).
fof(f1729,axiom,
p__d__subclass(c__Putting,c__Transfer),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2481) ).
fof(f1746,axiom,
p__d__subclass(c__Translocation,c__Motion),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2505) ).
fof(f7433,conjecture,
? [X0,X1] :
( ~ p__d__instance(X1,c__Putting)
& ~ p__d__instance(X0,c__Removing)
& X0 != X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antonymPattern31444) ).
fof(f7434,negated_conjecture,
~ ? [X0,X1] :
( ~ p__d__instance(X1,c__Putting)
& ~ p__d__instance(X0,c__Removing)
& X0 != X1 ),
inference(negated_conjecture,[status(cth)],[f7433]) ).
fof(f7435,plain,
( ! [X0,X1,X2] :
( p__d__disjointDecomposition3(X0,X1,X2)
<=> p__d__disjoint(X1,X2) )
& ! [X3,X4,X5,X6] :
( p__d__disjointDecomposition4(X3,X4,X5,X6)
<=> ( p__d__disjoint(X4,X5)
& p__d__disjoint(X4,X6)
& p__d__disjoint(X5,X6) ) )
& ! [X7,X8,X9,X10,X11] :
( p__d__disjointDecomposition5(X7,X8,X9,X10,X11)
<=> ( p__d__disjoint(X8,X9)
& p__d__disjoint(X8,X10)
& p__d__disjoint(X8,X11)
& p__d__disjoint(X9,X10)
& p__d__disjoint(X9,X11)
& p__d__disjoint(X10,X11) ) )
& ! [X12,X13,X14,X15,X16,X17] :
( p__d__disjointDecomposition6(X12,X13,X14,X15,X16,X17)
<=> ( p__d__disjoint(X13,X14)
& p__d__disjoint(X13,X15)
& p__d__disjoint(X13,X16)
& p__d__disjoint(X13,X17)
& p__d__disjoint(X14,X15)
& p__d__disjoint(X14,X16)
& p__d__disjoint(X14,X17)
& p__d__disjoint(X15,X16)
& p__d__disjoint(X15,X17)
& p__d__disjoint(X16,X17) ) )
& ! [X18,X19,X20,X21,X22,X23,X24] :
( p__d__disjointDecomposition7(X18,X19,X20,X21,X22,X23,X24)
<=> ( p__d__disjoint(X19,X20)
& p__d__disjoint(X19,X21)
& p__d__disjoint(X19,X22)
& p__d__disjoint(X19,X23)
& p__d__disjoint(X19,X24)
& p__d__disjoint(X20,X21)
& p__d__disjoint(X20,X22)
& p__d__disjoint(X20,X23)
& p__d__disjoint(X20,X24)
& p__d__disjoint(X21,X22)
& p__d__disjoint(X21,X23)
& p__d__disjoint(X21,X24)
& p__d__disjoint(X22,X23)
& p__d__disjoint(X22,X24)
& p__d__disjoint(X23,X24) ) ) ),
inference(rectify,[],[f8]) ).
fof(f7436,plain,
( ! [X0,X1,X2] :
( p__d__partition3(X0,X1,X2)
<=> ( p__d__exhaustiveDecomposition3(X0,X1,X2)
& p__d__disjointDecomposition3(X0,X1,X2) ) )
& ! [X3,X4,X5,X6] :
( p__d__partition4(X3,X4,X5,X6)
<=> ( p__d__exhaustiveDecomposition4(X3,X4,X5,X6)
& p__d__disjointDecomposition4(X3,X4,X5,X6) ) )
& ! [X7,X8,X9,X10,X11] :
( p__d__partition5(X7,X8,X9,X10,X11)
<=> ( p__d__exhaustiveDecomposition5(X7,X8,X9,X10,X11)
& p__d__disjointDecomposition5(X7,X8,X9,X10,X11) ) )
& ! [X12,X13,X14,X15,X16,X17] :
( p__d__partition6(X12,X13,X14,X15,X16,X17)
<=> ( p__d__exhaustiveDecomposition6(X12,X13,X14,X15,X16,X17)
& p__d__disjointDecomposition6(X12,X13,X14,X15,X16,X17) ) )
& ! [X18,X19,X20,X21,X22,X23,X24] :
( p__d__partition7(X18,X19,X20,X21,X22,X23,X24)
<=> ( p__d__exhaustiveDecomposition7(X18,X19,X20,X21,X22,X23,X24)
& p__d__disjointDecomposition7(X18,X19,X20,X21,X22,X23,X24) ) ) ),
inference(rectify,[],[f6]) ).
fof(f7446,plain,
! [X0,X1] :
( p__d__instance(X1,c__Putting)
| p__d__instance(X0,c__Removing)
| X0 = X1 ),
inference(ennf_transformation,[],[f7434]) ).
fof(f7455,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f7456,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7455]) ).
fof(f7457,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f7458,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7457]) ).
fof(f10335,plain,
! [X0] :
( ? [X1] : p__d__instance(X1,X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(ennf_transformation,[],[f110]) ).
fof(f11082,plain,
! [X0,X1] :
( ( p__d__disjoint(X0,X1)
| ? [X2] :
( p__d__instance(X2,X0)
& p__d__instance(X2,X1) ) )
& ( ! [X2] :
( ~ p__d__instance(X2,X0)
| ~ p__d__instance(X2,X1) )
| ~ p__d__disjoint(X0,X1) ) ),
inference(nnf_transformation,[],[f5]) ).
fof(f11083,plain,
! [X0,X1] :
( ( p__d__disjoint(X0,X1)
| ? [X2] :
( p__d__instance(X2,X0)
& p__d__instance(X2,X1) ) )
& ( ! [X3] :
( ~ p__d__instance(X3,X0)
| ~ p__d__instance(X3,X1) )
| ~ p__d__disjoint(X0,X1) ) ),
inference(rectify,[],[f11082]) ).
fof(f11084,plain,
! [X0,X1] :
( ( p__d__disjoint(X0,X1)
| ( p__d__instance(sK115(X0,X1),X0)
& p__d__instance(sK115(X0,X1),X1) ) )
& ( ! [X3] :
( ~ p__d__instance(X3,X0)
| ~ p__d__instance(X3,X1) )
| ~ p__d__disjoint(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK115]),skolemize(X2,sK115(X0,X1))],[f11083]) ).
fof(f11274,plain,
( ! [X0,X1,X2] :
( ( p__d__disjointDecomposition3(X0,X1,X2)
| ~ p__d__disjoint(X1,X2) )
& ( p__d__disjoint(X1,X2)
| ~ p__d__disjointDecomposition3(X0,X1,X2) ) )
& ! [X3,X4,X5,X6] :
( ( p__d__disjointDecomposition4(X3,X4,X5,X6)
| ~ p__d__disjoint(X4,X5)
| ~ p__d__disjoint(X4,X6)
| ~ p__d__disjoint(X5,X6) )
& ( ( p__d__disjoint(X4,X5)
& p__d__disjoint(X4,X6)
& p__d__disjoint(X5,X6) )
| ~ p__d__disjointDecomposition4(X3,X4,X5,X6) ) )
& ! [X7,X8,X9,X10,X11] :
( ( p__d__disjointDecomposition5(X7,X8,X9,X10,X11)
| ~ p__d__disjoint(X8,X9)
| ~ p__d__disjoint(X8,X10)
| ~ p__d__disjoint(X8,X11)
| ~ p__d__disjoint(X9,X10)
| ~ p__d__disjoint(X9,X11)
| ~ p__d__disjoint(X10,X11) )
& ( ( p__d__disjoint(X8,X9)
& p__d__disjoint(X8,X10)
& p__d__disjoint(X8,X11)
& p__d__disjoint(X9,X10)
& p__d__disjoint(X9,X11)
& p__d__disjoint(X10,X11) )
| ~ p__d__disjointDecomposition5(X7,X8,X9,X10,X11) ) )
& ! [X12,X13,X14,X15,X16,X17] :
( ( p__d__disjointDecomposition6(X12,X13,X14,X15,X16,X17)
| ~ p__d__disjoint(X13,X14)
| ~ p__d__disjoint(X13,X15)
| ~ p__d__disjoint(X13,X16)
| ~ p__d__disjoint(X13,X17)
| ~ p__d__disjoint(X14,X15)
| ~ p__d__disjoint(X14,X16)
| ~ p__d__disjoint(X14,X17)
| ~ p__d__disjoint(X15,X16)
| ~ p__d__disjoint(X15,X17)
| ~ p__d__disjoint(X16,X17) )
& ( ( p__d__disjoint(X13,X14)
& p__d__disjoint(X13,X15)
& p__d__disjoint(X13,X16)
& p__d__disjoint(X13,X17)
& p__d__disjoint(X14,X15)
& p__d__disjoint(X14,X16)
& p__d__disjoint(X14,X17)
& p__d__disjoint(X15,X16)
& p__d__disjoint(X15,X17)
& p__d__disjoint(X16,X17) )
| ~ p__d__disjointDecomposition6(X12,X13,X14,X15,X16,X17) ) )
& ! [X18,X19,X20,X21,X22,X23,X24] :
( ( p__d__disjointDecomposition7(X18,X19,X20,X21,X22,X23,X24)
| ~ p__d__disjoint(X19,X20)
| ~ p__d__disjoint(X19,X21)
| ~ p__d__disjoint(X19,X22)
| ~ p__d__disjoint(X19,X23)
| ~ p__d__disjoint(X19,X24)
| ~ p__d__disjoint(X20,X21)
| ~ p__d__disjoint(X20,X22)
| ~ p__d__disjoint(X20,X23)
| ~ p__d__disjoint(X20,X24)
| ~ p__d__disjoint(X21,X22)
| ~ p__d__disjoint(X21,X23)
| ~ p__d__disjoint(X21,X24)
| ~ p__d__disjoint(X22,X23)
| ~ p__d__disjoint(X22,X24)
| ~ p__d__disjoint(X23,X24) )
& ( ( p__d__disjoint(X19,X20)
& p__d__disjoint(X19,X21)
& p__d__disjoint(X19,X22)
& p__d__disjoint(X19,X23)
& p__d__disjoint(X19,X24)
& p__d__disjoint(X20,X21)
& p__d__disjoint(X20,X22)
& p__d__disjoint(X20,X23)
& p__d__disjoint(X20,X24)
& p__d__disjoint(X21,X22)
& p__d__disjoint(X21,X23)
& p__d__disjoint(X21,X24)
& p__d__disjoint(X22,X23)
& p__d__disjoint(X22,X24)
& p__d__disjoint(X23,X24) )
| ~ p__d__disjointDecomposition7(X18,X19,X20,X21,X22,X23,X24) ) ) ),
inference(nnf_transformation,[],[f7435]) ).
fof(f11275,plain,
( ! [X0,X1,X2] :
( ( p__d__disjointDecomposition3(X0,X1,X2)
| ~ p__d__disjoint(X1,X2) )
& ( p__d__disjoint(X1,X2)
| ~ p__d__disjointDecomposition3(X0,X1,X2) ) )
& ! [X3,X4,X5,X6] :
( ( p__d__disjointDecomposition4(X3,X4,X5,X6)
| ~ p__d__disjoint(X4,X5)
| ~ p__d__disjoint(X4,X6)
| ~ p__d__disjoint(X5,X6) )
& ( ( p__d__disjoint(X4,X5)
& p__d__disjoint(X4,X6)
& p__d__disjoint(X5,X6) )
| ~ p__d__disjointDecomposition4(X3,X4,X5,X6) ) )
& ! [X7,X8,X9,X10,X11] :
( ( p__d__disjointDecomposition5(X7,X8,X9,X10,X11)
| ~ p__d__disjoint(X8,X9)
| ~ p__d__disjoint(X8,X10)
| ~ p__d__disjoint(X8,X11)
| ~ p__d__disjoint(X9,X10)
| ~ p__d__disjoint(X9,X11)
| ~ p__d__disjoint(X10,X11) )
& ( ( p__d__disjoint(X8,X9)
& p__d__disjoint(X8,X10)
& p__d__disjoint(X8,X11)
& p__d__disjoint(X9,X10)
& p__d__disjoint(X9,X11)
& p__d__disjoint(X10,X11) )
| ~ p__d__disjointDecomposition5(X7,X8,X9,X10,X11) ) )
& ! [X12,X13,X14,X15,X16,X17] :
( ( p__d__disjointDecomposition6(X12,X13,X14,X15,X16,X17)
| ~ p__d__disjoint(X13,X14)
| ~ p__d__disjoint(X13,X15)
| ~ p__d__disjoint(X13,X16)
| ~ p__d__disjoint(X13,X17)
| ~ p__d__disjoint(X14,X15)
| ~ p__d__disjoint(X14,X16)
| ~ p__d__disjoint(X14,X17)
| ~ p__d__disjoint(X15,X16)
| ~ p__d__disjoint(X15,X17)
| ~ p__d__disjoint(X16,X17) )
& ( ( p__d__disjoint(X13,X14)
& p__d__disjoint(X13,X15)
& p__d__disjoint(X13,X16)
& p__d__disjoint(X13,X17)
& p__d__disjoint(X14,X15)
& p__d__disjoint(X14,X16)
& p__d__disjoint(X14,X17)
& p__d__disjoint(X15,X16)
& p__d__disjoint(X15,X17)
& p__d__disjoint(X16,X17) )
| ~ p__d__disjointDecomposition6(X12,X13,X14,X15,X16,X17) ) )
& ! [X18,X19,X20,X21,X22,X23,X24] :
( ( p__d__disjointDecomposition7(X18,X19,X20,X21,X22,X23,X24)
| ~ p__d__disjoint(X19,X20)
| ~ p__d__disjoint(X19,X21)
| ~ p__d__disjoint(X19,X22)
| ~ p__d__disjoint(X19,X23)
| ~ p__d__disjoint(X19,X24)
| ~ p__d__disjoint(X20,X21)
| ~ p__d__disjoint(X20,X22)
| ~ p__d__disjoint(X20,X23)
| ~ p__d__disjoint(X20,X24)
| ~ p__d__disjoint(X21,X22)
| ~ p__d__disjoint(X21,X23)
| ~ p__d__disjoint(X21,X24)
| ~ p__d__disjoint(X22,X23)
| ~ p__d__disjoint(X22,X24)
| ~ p__d__disjoint(X23,X24) )
& ( ( p__d__disjoint(X19,X20)
& p__d__disjoint(X19,X21)
& p__d__disjoint(X19,X22)
& p__d__disjoint(X19,X23)
& p__d__disjoint(X19,X24)
& p__d__disjoint(X20,X21)
& p__d__disjoint(X20,X22)
& p__d__disjoint(X20,X23)
& p__d__disjoint(X20,X24)
& p__d__disjoint(X21,X22)
& p__d__disjoint(X21,X23)
& p__d__disjoint(X21,X24)
& p__d__disjoint(X22,X23)
& p__d__disjoint(X22,X24)
& p__d__disjoint(X23,X24) )
| ~ p__d__disjointDecomposition7(X18,X19,X20,X21,X22,X23,X24) ) ) ),
inference(flattening,[],[f11274]) ).
fof(f11276,plain,
( ! [X0,X1,X2] :
( ( p__d__partition3(X0,X1,X2)
| ~ p__d__exhaustiveDecomposition3(X0,X1,X2)
| ~ p__d__disjointDecomposition3(X0,X1,X2) )
& ( ( p__d__exhaustiveDecomposition3(X0,X1,X2)
& p__d__disjointDecomposition3(X0,X1,X2) )
| ~ p__d__partition3(X0,X1,X2) ) )
& ! [X3,X4,X5,X6] :
( ( p__d__partition4(X3,X4,X5,X6)
| ~ p__d__exhaustiveDecomposition4(X3,X4,X5,X6)
| ~ p__d__disjointDecomposition4(X3,X4,X5,X6) )
& ( ( p__d__exhaustiveDecomposition4(X3,X4,X5,X6)
& p__d__disjointDecomposition4(X3,X4,X5,X6) )
| ~ p__d__partition4(X3,X4,X5,X6) ) )
& ! [X7,X8,X9,X10,X11] :
( ( p__d__partition5(X7,X8,X9,X10,X11)
| ~ p__d__exhaustiveDecomposition5(X7,X8,X9,X10,X11)
| ~ p__d__disjointDecomposition5(X7,X8,X9,X10,X11) )
& ( ( p__d__exhaustiveDecomposition5(X7,X8,X9,X10,X11)
& p__d__disjointDecomposition5(X7,X8,X9,X10,X11) )
| ~ p__d__partition5(X7,X8,X9,X10,X11) ) )
& ! [X12,X13,X14,X15,X16,X17] :
( ( p__d__partition6(X12,X13,X14,X15,X16,X17)
| ~ p__d__exhaustiveDecomposition6(X12,X13,X14,X15,X16,X17)
| ~ p__d__disjointDecomposition6(X12,X13,X14,X15,X16,X17) )
& ( ( p__d__exhaustiveDecomposition6(X12,X13,X14,X15,X16,X17)
& p__d__disjointDecomposition6(X12,X13,X14,X15,X16,X17) )
| ~ p__d__partition6(X12,X13,X14,X15,X16,X17) ) )
& ! [X18,X19,X20,X21,X22,X23,X24] :
( ( p__d__partition7(X18,X19,X20,X21,X22,X23,X24)
| ~ p__d__exhaustiveDecomposition7(X18,X19,X20,X21,X22,X23,X24)
| ~ p__d__disjointDecomposition7(X18,X19,X20,X21,X22,X23,X24) )
& ( ( p__d__exhaustiveDecomposition7(X18,X19,X20,X21,X22,X23,X24)
& p__d__disjointDecomposition7(X18,X19,X20,X21,X22,X23,X24) )
| ~ p__d__partition7(X18,X19,X20,X21,X22,X23,X24) ) ) ),
inference(nnf_transformation,[],[f7436]) ).
fof(f11277,plain,
( ! [X0,X1,X2] :
( ( p__d__partition3(X0,X1,X2)
| ~ p__d__exhaustiveDecomposition3(X0,X1,X2)
| ~ p__d__disjointDecomposition3(X0,X1,X2) )
& ( ( p__d__exhaustiveDecomposition3(X0,X1,X2)
& p__d__disjointDecomposition3(X0,X1,X2) )
| ~ p__d__partition3(X0,X1,X2) ) )
& ! [X3,X4,X5,X6] :
( ( p__d__partition4(X3,X4,X5,X6)
| ~ p__d__exhaustiveDecomposition4(X3,X4,X5,X6)
| ~ p__d__disjointDecomposition4(X3,X4,X5,X6) )
& ( ( p__d__exhaustiveDecomposition4(X3,X4,X5,X6)
& p__d__disjointDecomposition4(X3,X4,X5,X6) )
| ~ p__d__partition4(X3,X4,X5,X6) ) )
& ! [X7,X8,X9,X10,X11] :
( ( p__d__partition5(X7,X8,X9,X10,X11)
| ~ p__d__exhaustiveDecomposition5(X7,X8,X9,X10,X11)
| ~ p__d__disjointDecomposition5(X7,X8,X9,X10,X11) )
& ( ( p__d__exhaustiveDecomposition5(X7,X8,X9,X10,X11)
& p__d__disjointDecomposition5(X7,X8,X9,X10,X11) )
| ~ p__d__partition5(X7,X8,X9,X10,X11) ) )
& ! [X12,X13,X14,X15,X16,X17] :
( ( p__d__partition6(X12,X13,X14,X15,X16,X17)
| ~ p__d__exhaustiveDecomposition6(X12,X13,X14,X15,X16,X17)
| ~ p__d__disjointDecomposition6(X12,X13,X14,X15,X16,X17) )
& ( ( p__d__exhaustiveDecomposition6(X12,X13,X14,X15,X16,X17)
& p__d__disjointDecomposition6(X12,X13,X14,X15,X16,X17) )
| ~ p__d__partition6(X12,X13,X14,X15,X16,X17) ) )
& ! [X18,X19,X20,X21,X22,X23,X24] :
( ( p__d__partition7(X18,X19,X20,X21,X22,X23,X24)
| ~ p__d__exhaustiveDecomposition7(X18,X19,X20,X21,X22,X23,X24)
| ~ p__d__disjointDecomposition7(X18,X19,X20,X21,X22,X23,X24) )
& ( ( p__d__exhaustiveDecomposition7(X18,X19,X20,X21,X22,X23,X24)
& p__d__disjointDecomposition7(X18,X19,X20,X21,X22,X23,X24) )
| ~ p__d__partition7(X18,X19,X20,X21,X22,X23,X24) ) ) ),
inference(flattening,[],[f11276]) ).
fof(f12291,plain,
! [X0] :
( p__d__instance(sK1107(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1107]),skolemize(X1,sK1107(X0))],[f10335]) ).
fof(f12551,plain,
! [X0,X1] :
( p__d__instance(X1,c__Putting)
| p__d__instance(X0,c__Removing)
| X0 = X1 ),
inference(cnf_transformation,[],[f7446]) ).
fof(f12584,plain,
p__d__subclass(c__Removing,c__Transfer),
inference(cnf_transformation,[],[f1726]) ).
fof(f12598,plain,
p__d__subclass(c__Putting,c__Transfer),
inference(cnf_transformation,[],[f1729]) ).
fof(f12599,plain,
! [X2,X0,X1] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(cnf_transformation,[],[f7456]) ).
fof(f12600,plain,
! [X2,X0,X1] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(cnf_transformation,[],[f7458]) ).
fof(f12661,plain,
p__d__subclass(c__Transfer,c__Translocation),
inference(cnf_transformation,[],[f1721]) ).
fof(f12809,plain,
p__d__subclass(c__Process,c__Physical),
inference(cnf_transformation,[],[f233]) ).
fof(f12810,plain,
p__d__subclass(c__Object,c__Physical),
inference(cnf_transformation,[],[f115]) ).
fof(f12966,plain,
! [X3,X0,X1] :
( ~ p__d__disjoint(X0,X1)
| ~ p__d__instance(X3,X1)
| ~ p__d__instance(X3,X0) ),
inference(cnf_transformation,[],[f11084]) ).
fof(f13236,plain,
p__d__partition3(c__Physical,c__Object,c__Process),
inference(cnf_transformation,[],[f113]) ).
fof(f13969,plain,
! [X2,X0,X1] :
( ~ p__d__disjointDecomposition3(X0,X1,X2)
| p__d__disjoint(X1,X2) ),
inference(cnf_transformation,[],[f11275]) ).
fof(f13983,plain,
! [X2,X0,X1] :
( p__d__disjointDecomposition3(X0,X1,X2)
| ~ p__d__partition3(X0,X1,X2) ),
inference(cnf_transformation,[],[f11277]) ).
fof(f14802,plain,
p__d__subclass(c__Translocation,c__Motion),
inference(cnf_transformation,[],[f1746]) ).
fof(f14804,plain,
p__d__subclass(c__Motion,c__Process),
inference(cnf_transformation,[],[f1677]) ).
fof(f17879,plain,
p__d__subclass(c__Abstract,c__Entity),
inference(cnf_transformation,[],[f239]) ).
fof(f17880,plain,
p__d__partition3(c__Entity,c__Physical,c__Abstract),
inference(cnf_transformation,[],[f107]) ).
fof(f19879,plain,
p__d__subclass(c__Physical,c__Entity),
inference(cnf_transformation,[],[f112]) ).
fof(f19882,plain,
! [X0] :
( p__d__instance(sK1107(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(cnf_transformation,[],[f12291]) ).
fof(f22982,plain,
! [X2,X0,X1] :
( ~ p__d__partition3(X2,X0,X1)
| p__d__disjoint(X0,X1) ),
inference(resolution,[],[f13969,f13983]) ).
fof(f23258,plain,
p__d__disjoint(c__Physical,c__Abstract),
inference(resolution,[],[f17880,f22982]) ).
fof(f23311,plain,
p__d__disjoint(c__Object,c__Process),
inference(resolution,[],[f13236,f22982]) ).
fof(f23313,plain,
! [X0] :
( ~ p__d__instance(X0,c__Process)
| ~ p__d__instance(X0,c__Object) ),
inference(resolution,[],[f23311,f12966]) ).
fof(f23356,plain,
! [X0] :
( ~ p__d__instance(X0,c__Abstract)
| ~ p__d__instance(X0,c__Physical) ),
inference(resolution,[],[f23258,f12966]) ).
fof(f24391,plain,
( ~ p__d__instance(sK1107(c__Abstract),c__Physical)
| ~ p__d__subclass(c__Abstract,c__Entity) ),
inference(resolution,[],[f23356,f19882]) ).
fof(f24392,plain,
~ p__d__instance(sK1107(c__Abstract),c__Physical),
inference(forward_subsumption_resolution,[],[f24391,f17879]) ).
fof(f24393,plain,
! [X0] :
( ~ p__d__instance(sK1107(c__Abstract),X0)
| ~ p__d__subclass(X0,c__Physical) ),
inference(resolution,[],[f24392,f12599]) ).
fof(f24642,definition,
( spl1215_254
<=> p__d__subclass(c__Removing,c__Physical) ),
introduced(definition,[new_symbols(definition,[spl1215_254])],[avatar_definition]) ).
fof(f24643,plain,
( p__d__subclass(c__Removing,c__Physical)
| ~ spl1215_254 ),
inference(avatar_component_clause,[],[f24642]) ).
fof(f24644,plain,
( ~ p__d__subclass(c__Removing,c__Physical)
| spl1215_254 ),
inference(avatar_component_clause,[],[f24642]) ).
fof(f24658,plain,
( ! [X0] :
( ~ p__d__subclass(c__Removing,X0)
| ~ p__d__subclass(X0,c__Physical) )
| spl1215_254 ),
inference(resolution,[],[f24644,f12600]) ).
fof(f24662,plain,
( ~ p__d__subclass(c__Transfer,c__Physical)
| spl1215_254 ),
inference(resolution,[],[f24658,f12584]) ).
fof(f24670,plain,
( ! [X0] :
( ~ p__d__subclass(c__Transfer,X0)
| ~ p__d__subclass(X0,c__Physical) )
| spl1215_254 ),
inference(resolution,[],[f24662,f12600]) ).
fof(f24673,plain,
( ~ p__d__subclass(c__Translocation,c__Physical)
| spl1215_254 ),
inference(resolution,[],[f24670,f12661]) ).
fof(f24674,plain,
( ! [X0] :
( ~ p__d__subclass(c__Translocation,X0)
| ~ p__d__subclass(X0,c__Physical) )
| spl1215_254 ),
inference(resolution,[],[f24673,f12600]) ).
fof(f24677,plain,
( ~ p__d__subclass(c__Motion,c__Physical)
| spl1215_254 ),
inference(resolution,[],[f24674,f14802]) ).
fof(f24680,plain,
( ! [X0] :
( ~ p__d__subclass(c__Motion,X0)
| ~ p__d__subclass(X0,c__Physical) )
| spl1215_254 ),
inference(resolution,[],[f24677,f12600]) ).
fof(f24870,plain,
! [X0,X1] :
( ~ p__d__instance(X0,c__Object)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,c__Process) ),
inference(resolution,[],[f23313,f12599]) ).
fof(f25008,plain,
( ~ p__d__subclass(c__Process,c__Physical)
| spl1215_254 ),
inference(resolution,[],[f24680,f14804]) ).
fof(f25009,plain,
( $false
| spl1215_254 ),
inference(forward_subsumption_resolution,[],[f25008,f12809]) ).
fof(f25010,plain,
spl1215_254,
inference(avatar_contradiction_clause,[],[f25009]) ).
fof(f29715,plain,
! [X0] :
( ~ p__d__instance(sK1107(c__Object),X0)
| ~ p__d__subclass(X0,c__Process)
| ~ p__d__subclass(c__Object,c__Entity) ),
inference(resolution,[],[f24870,f19882]) ).
fof(f29726,definition,
( spl1215_998
<=> p__d__subclass(c__Object,c__Entity) ),
introduced(definition,[new_symbols(definition,[spl1215_998])],[avatar_definition]) ).
fof(f29727,plain,
( p__d__subclass(c__Object,c__Entity)
| ~ spl1215_998 ),
inference(avatar_component_clause,[],[f29726]) ).
fof(f29728,plain,
( ~ p__d__subclass(c__Object,c__Entity)
| spl1215_998 ),
inference(avatar_component_clause,[],[f29726]) ).
fof(f29730,definition,
( spl1215_999
<=> ! [X0] :
( ~ p__d__instance(sK1107(c__Object),X0)
| ~ p__d__subclass(X0,c__Process) ) ),
introduced(definition,[new_symbols(definition,[spl1215_999])],[avatar_definition]) ).
fof(f29731,plain,
( ! [X0] :
( ~ p__d__instance(sK1107(c__Object),X0)
| ~ p__d__subclass(X0,c__Process) )
| ~ spl1215_999 ),
inference(avatar_component_clause,[],[f29730]) ).
fof(f29732,plain,
( ~ spl1215_998
| spl1215_999 ),
inference(avatar_split_clause,[],[f29715,f29730,f29726]) ).
fof(f29733,plain,
( ! [X0] :
( ~ p__d__subclass(c__Object,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl1215_998 ),
inference(resolution,[],[f29728,f12600]) ).
fof(f29736,plain,
( ~ p__d__subclass(c__Physical,c__Entity)
| spl1215_998 ),
inference(resolution,[],[f29733,f12810]) ).
fof(f29737,plain,
( $false
| spl1215_998 ),
inference(forward_subsumption_resolution,[],[f29736,f19879]) ).
fof(f29738,plain,
spl1215_998,
inference(avatar_contradiction_clause,[],[f29737]) ).
fof(f29749,plain,
( ! [X0] :
( ~ p__d__subclass(c__Putting,c__Process)
| p__d__instance(X0,c__Removing)
| sK1107(c__Object) = X0 )
| ~ spl1215_999 ),
inference(resolution,[],[f29731,f12551]) ).
fof(f29751,definition,
( spl1215_1000
<=> ! [X0] :
( p__d__instance(X0,c__Removing)
| sK1107(c__Object) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl1215_1000])],[avatar_definition]) ).
fof(f29752,plain,
( ! [X0] :
( sK1107(c__Object) = X0
| p__d__instance(X0,c__Removing) )
| ~ spl1215_1000 ),
inference(avatar_component_clause,[],[f29751]) ).
fof(f29754,definition,
( spl1215_1001
<=> p__d__subclass(c__Putting,c__Process) ),
introduced(definition,[new_symbols(definition,[spl1215_1001])],[avatar_definition]) ).
fof(f29756,plain,
( ~ p__d__subclass(c__Putting,c__Process)
| spl1215_1001 ),
inference(avatar_component_clause,[],[f29754]) ).
fof(f29757,plain,
( spl1215_1000
| ~ spl1215_1001
| ~ spl1215_999 ),
inference(avatar_split_clause,[],[f29749,f29730,f29754,f29751]) ).
fof(f29787,plain,
( ! [X0] :
( ~ p__d__subclass(c__Putting,X0)
| ~ p__d__subclass(X0,c__Process) )
| spl1215_1001 ),
inference(resolution,[],[f29756,f12600]) ).
fof(f29792,plain,
( ~ p__d__subclass(c__Transfer,c__Process)
| spl1215_1001 ),
inference(resolution,[],[f29787,f12598]) ).
fof(f29798,plain,
( ! [X0] :
( ~ p__d__subclass(c__Transfer,X0)
| ~ p__d__subclass(X0,c__Process) )
| spl1215_1001 ),
inference(resolution,[],[f29792,f12600]) ).
fof(f29801,plain,
( ~ p__d__subclass(c__Translocation,c__Process)
| spl1215_1001 ),
inference(resolution,[],[f29798,f12661]) ).
fof(f29802,plain,
( ! [X0] :
( ~ p__d__subclass(c__Translocation,X0)
| ~ p__d__subclass(X0,c__Process) )
| spl1215_1001 ),
inference(resolution,[],[f29801,f12600]) ).
fof(f29805,plain,
( ~ p__d__subclass(c__Motion,c__Process)
| spl1215_1001 ),
inference(resolution,[],[f29802,f14802]) ).
fof(f29806,plain,
( $false
| spl1215_1001 ),
inference(forward_subsumption_resolution,[],[f29805,f14804]) ).
fof(f29807,plain,
spl1215_1001,
inference(avatar_contradiction_clause,[],[f29806]) ).
fof(f29828,plain,
( ! [X0] :
( p__d__instance(X0,c__Object)
| ~ p__d__subclass(c__Object,c__Entity)
| p__d__instance(X0,c__Removing) )
| ~ spl1215_1000 ),
inference(superposition,[],[f19882,f29752]) ).
fof(f29829,plain,
( ! [X0] :
( p__d__instance(X0,c__Removing)
| p__d__instance(X0,c__Object) )
| ~ spl1215_998
| ~ spl1215_1000 ),
inference(forward_subsumption_resolution,[],[f29828,f29727]) ).
fof(f29857,plain,
( p__d__instance(sK1107(c__Abstract),c__Object)
| ~ p__d__subclass(c__Removing,c__Physical)
| ~ spl1215_998
| ~ spl1215_1000 ),
inference(resolution,[],[f29829,f24393]) ).
fof(f29863,plain,
( p__d__instance(sK1107(c__Abstract),c__Object)
| ~ spl1215_254
| ~ spl1215_998
| ~ spl1215_1000 ),
inference(forward_subsumption_resolution,[],[f29857,f24643]) ).
fof(f29869,plain,
( ~ p__d__subclass(c__Object,c__Physical)
| ~ spl1215_254
| ~ spl1215_998
| ~ spl1215_1000 ),
inference(resolution,[],[f29863,f24393]) ).
fof(f29874,plain,
( $false
| ~ spl1215_254
| ~ spl1215_998
| ~ spl1215_1000 ),
inference(forward_subsumption_resolution,[],[f29869,f12810]) ).
fof(f29875,plain,
( ~ spl1215_254
| ~ spl1215_998
| ~ spl1215_1000 ),
inference(avatar_contradiction_clause,[],[f29874]) ).
cnf(s156,plain,
spl1215_254,
inference(sat_conversion,[],[f25010]) ).
cnf(s526,plain,
( ~ spl1215_998
| spl1215_999 ),
inference(sat_conversion,[],[f29732]) ).
cnf(s527,plain,
spl1215_998,
inference(sat_conversion,[],[f29738]) ).
cnf(s528,plain,
( ~ spl1215_999
| spl1215_1000
| ~ spl1215_1001 ),
inference(sat_conversion,[],[f29757]) ).
cnf(s534,plain,
spl1215_1001,
inference(sat_conversion,[],[f29807]) ).
cnf(s538,plain,
( ~ spl1215_254
| ~ spl1215_998
| ~ spl1215_1000 ),
inference(sat_conversion,[],[f29875]) ).
cnf(s539,plain,
( ~ spl1215_999
| spl1215_1000 ),
inference(rat,[],[s528,s534]) ).
cnf(s540,plain,
spl1215_999,
inference(rat,[],[s526,s527]) ).
cnf(s541,plain,
spl1215_1000,
inference(rat,[],[s539,s540]) ).
cnf(s542,plain,
~ spl1215_254,
inference(rat,[],[s538,s527,s541]) ).
cnf(s546,plain,
$false,
inference(rat,[],[s156,s542]) ).
fof(f29876,plain,
$false,
inference(avatar_sat_refutation,[],[s546]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR228+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n015.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 23:52:32 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/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
% 7.24/1.71 % (3156385)Detected formulas, will run a generic FOF schedule.
% 7.24/1.71 % (3156395)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2128872929:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 7.24/1.71 % (3156396)dis-21_1_sil=8000:lcm=predicate:random_seed=3120107597: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)
% 7.24/1.71 % (3156394)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=198239257:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 7.24/1.71 % (3156390)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=4274505904:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 7.24/1.71 % (3156393)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=653697688:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 7.24/1.71 % (3156391)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=1065831812:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 7.24/1.71 % (3156392)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=3054622118:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 7.24/1.71 % (3156393)Refutation not found, incomplete strategy
% 7.24/1.71 % (3156393)------------------------------
% 7.24/1.71 % (3156393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.24/1.71 % (3156393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.24/1.71 % (3156393)CaDiCaL version: 2.1.3
% 7.24/1.71 % (3156393)Termination reason: Refutation not found, incomplete strategy
% 7.24/1.71 % (3156393)Time elapsed: 0.016 s
% 7.24/1.71 % (3156393)Peak memory usage: 94 MB
% 7.24/1.71 % (3156393)Instructions burned: 23 (million)
% 7.24/1.71 % (3156395)Instruction limit reached!
% 7.24/1.71 % (3156395)------------------------------
% 7.24/1.71 % (3156395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.24/1.71 % (3156395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.24/1.71 % (3156395)CaDiCaL version: 2.1.3
% 7.24/1.71 % (3156395)Termination reason: Instruction limit
% 7.24/1.71 % (3156395)Termination phase: Preprocessing 3
% 7.24/1.71 % (3156395)Time elapsed: 0.046 s
% 7.24/1.71 % (3156395)Peak memory usage: 94 MB
% 7.24/1.71 % (3156395)Instructions burned: 140 (million)
% 7.24/1.71 % (3156394)Instruction limit reached!
% 7.24/1.71 % (3156394)------------------------------
% 7.24/1.71 % (3156394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.24/1.71 % (3156394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.24/1.71 % (3156394)CaDiCaL version: 2.1.3
% 7.24/1.71 % (3156394)Termination reason: Instruction limit
% 7.24/1.71 % (3156394)Termination phase: Saturation
% 7.24/1.71 % (3156394)Time elapsed: 0.064 s
% 7.24/1.71 % (3156394)Peak memory usage: 93 MB
% 7.24/1.71 % (3156394)Instructions burned: 123 (million)
% 7.24/1.71 % (3156396)Instruction limit reached!
% 7.24/1.71 % (3156396)------------------------------
% 7.24/1.71 % (3156396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.24/1.71 % (3156396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.24/1.71 % (3156396)CaDiCaL version: 2.1.3
% 7.24/1.71 % (3156396)Termination reason: Instruction limit
% 7.24/1.71 % (3156396)Termination phase: Saturation
% 7.24/1.71 % (3156396)Time elapsed: 0.077 s
% 7.24/1.71 % (3156396)Peak memory usage: 95 MB
% 7.24/1.71 % (3156396)Instructions burned: 130 (million)
% 7.24/1.71 % (3156404)lrs+10_1_sil=8000:sp=occurrence:random_seed=1597633315:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 7.24/1.71 % (3156404)Refutation not found, incomplete strategy
% 7.24/1.71 % (3156404)------------------------------
% 7.24/1.71 % (3156404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.24/1.71 % (3156404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.24/1.71 % (3156404)CaDiCaL version: 2.1.3
% 7.24/1.71 % (3156404)Termination reason: Refutation not found, incomplete strategy
% 7.24/1.71 % (3156404)Time elapsed: 0.011 s
% 7.24/1.71 % (3156404)Peak memory usage: 94 MB
% 7.24/1.71 % (3156404)Instructions burned: 23 (million)
% 13.27/2.41 % (3156405)lrs+10_1_sil=32000:urr=on:br=off:random_seed=764952613:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 13.27/2.41 % (3156406)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2802917221:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 13.27/2.41 % (3156406)Refutation not found, incomplete strategy
% 13.27/2.41 % (3156406)------------------------------
% 13.27/2.41 % (3156406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.27/2.41 % (3156406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.27/2.41 % (3156406)CaDiCaL version: 2.1.3
% 13.27/2.41 % (3156406)Termination reason: Refutation not found, incomplete strategy
% 13.27/2.41 % (3156406)Time elapsed: 0.019 s
% 13.27/2.41 % (3156406)Peak memory usage: 94 MB
% 13.27/2.41 % (3156406)Instructions burned: 23 (million)
% 13.27/2.41 % (3156393)------------------------------
% 13.27/2.41 % (3156393)------------------------------
% 13.27/2.41 % (3156405)Refutation not found, incomplete strategy
% 13.27/2.41 % (3156405)------------------------------
% 13.27/2.41 % (3156405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.27/2.41 % (3156405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.27/2.41 % (3156405)CaDiCaL version: 2.1.3
% 13.27/2.41 % (3156405)Termination reason: Refutation not found, incomplete strategy
% 13.27/2.41 % (3156405)Time elapsed: 0.033 s
% 13.27/2.41 % (3156405)Peak memory usage: 94 MB
% 13.27/2.41 % (3156405)Instructions burned: 60 (million)
% 13.27/2.41 % (3156404)------------------------------
% 13.27/2.41 % (3156404)------------------------------
% 13.27/2.41 % (3156410)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=100053295:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 13.27/2.41 % (3156411)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1923162818:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 13.27/2.41 % (3156411)Refutation not found, incomplete strategy
% 13.27/2.41 % (3156411)------------------------------
% 13.27/2.41 % (3156411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.27/2.41 % (3156411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.27/2.41 % (3156411)CaDiCaL version: 2.1.3
% 13.27/2.41 % (3156411)Termination reason: Refutation not found, incomplete strategy
% 13.27/2.41 % (3156411)Time elapsed: 0.013 s
% 13.27/2.41 % (3156411)Peak memory usage: 94 MB
% 13.27/2.41 % (3156411)Instructions burned: 35 (million)
% 13.27/2.41 % (3156406)------------------------------
% 13.27/2.41 % (3156406)------------------------------
% 13.27/2.41 % (3156405)------------------------------
% 13.27/2.41 % (3156405)------------------------------
% 13.27/2.41 % (3156410)Instruction limit reached!
% 13.27/2.41 % (3156410)------------------------------
% 13.27/2.41 % (3156410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.27/2.41 % (3156410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.27/2.41 % (3156410)CaDiCaL version: 2.1.3
% 13.27/2.41 % (3156410)Termination reason: Instruction limit
% 13.27/2.41 % (3156410)Termination phase: Saturation
% 13.27/2.41 % (3156410)Time elapsed: 0.136 s
% 13.27/2.41 % (3156410)Peak memory usage: 99 MB
% 13.27/2.41 % (3156410)Instructions burned: 248 (million)
% 13.27/2.41 % (3156411)------------------------------
% 13.27/2.41 % (3156411)------------------------------
% 13.27/2.41 % (3156392)Refutation not found, incomplete strategy
% 13.27/2.41 % (3156392)------------------------------
% 13.27/2.41 % (3156392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.27/2.41 % (3156392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.27/2.41 % (3156392)CaDiCaL version: 2.1.3
% 13.27/2.41 % (3156392)Termination reason: Refutation not found, incomplete strategy
% 13.27/2.41 % (3156392)Time elapsed: 0.647 s
% 13.27/2.41 % (3156392)Peak memory usage: 144 MB
% 13.27/2.41 % (3156392)Instructions burned: 957 (million)
% 13.27/2.41 % (3156414)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4226448564:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 13.27/2.41 % (3156415)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4179030639:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 13.27/2.41 % (3156391)Refutation not found, incomplete strategy
% 13.27/2.41 % (3156391)------------------------------
% 13.27/2.41 % (3156391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.94/3.35 % (3156391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.94/3.35 % (3156391)CaDiCaL version: 2.1.3
% 19.94/3.35 % (3156391)Termination reason: Refutation not found, incomplete strategy
% 19.94/3.35 % (3156391)Time elapsed: 0.721 s
% 19.94/3.35 % (3156391)Peak memory usage: 146 MB
% 19.94/3.35 % (3156391)Instructions burned: 1054 (million)
% 19.94/3.35 % (3156416)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=482671075:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 19.94/3.35 % (3156417)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2406131730:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 19.94/3.35 % (3156415)Instruction limit reached!
% 19.94/3.35 % (3156415)------------------------------
% 19.94/3.35 % (3156415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.94/3.35 % (3156415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.94/3.35 % (3156415)CaDiCaL version: 2.1.3
% 19.94/3.35 % (3156415)Termination reason: Instruction limit
% 19.94/3.35 % (3156415)Termination phase: Saturation
% 19.94/3.35 % (3156415)Time elapsed: 0.067 s
% 19.94/3.35 % (3156415)Peak memory usage: 94 MB
% 19.94/3.35 % (3156415)Instructions burned: 114 (million)
% 19.94/3.35 % (3156417)Instruction limit reached!
% 19.94/3.35 % (3156417)------------------------------
% 19.94/3.35 % (3156417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.94/3.35 % (3156417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.94/3.35 % (3156417)CaDiCaL version: 2.1.3
% 19.94/3.35 % (3156417)Termination reason: Instruction limit
% 19.94/3.35 % (3156417)Termination phase: Property scanning
% 19.94/3.35 % (3156417)Time elapsed: 0.034 s
% 19.94/3.35 % (3156417)Peak memory usage: 92 MB
% 19.94/3.35 % (3156417)Instructions burned: 118 (million)
% 19.94/3.35 % (3156416)Instruction limit reached!
% 19.94/3.35 % (3156416)------------------------------
% 19.94/3.35 % (3156416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.94/3.35 % (3156416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.94/3.35 % (3156416)CaDiCaL version: 2.1.3
% 19.94/3.35 % (3156416)Termination reason: Instruction limit
% 19.94/3.35 % (3156416)Termination phase: Property scanning
% 19.94/3.35 % (3156416)Time elapsed: 0.077 s
% 19.94/3.35 % (3156416)Peak memory usage: 96 MB
% 19.94/3.35 % (3156416)Instructions burned: 128 (million)
% 19.94/3.35 % (3156392)------------------------------
% 19.94/3.35 % (3156392)------------------------------
% 19.94/3.35 % (3156423)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2486547636:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 19.94/3.35 % (3156423)Refutation not found, incomplete strategy
% 19.94/3.35 % (3156423)------------------------------
% 19.94/3.35 % (3156423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.94/3.35 % (3156423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.94/3.35 % (3156423)CaDiCaL version: 2.1.3
% 19.94/3.35 % (3156423)Termination reason: Refutation not found, incomplete strategy
% 19.94/3.35 % (3156423)Time elapsed: 0.009 s
% 19.94/3.35 % (3156423)Peak memory usage: 94 MB
% 19.94/3.35 % (3156423)Instructions burned: 19 (million)
% 19.94/3.35 % (3156422)lrs+10_1_sil=8000:sp=occurrence:random_seed=2371859723:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 19.94/3.35 % (3156422)Refutation not found, incomplete strategy
% 19.94/3.35 % (3156422)------------------------------
% 19.94/3.35 % (3156422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.94/3.35 % (3156422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.94/3.35 % (3156422)CaDiCaL version: 2.1.3
% 19.94/3.35 % (3156422)Termination reason: Refutation not found, incomplete strategy
% 19.94/3.35 % (3156422)Time elapsed: 0.031 s
% 19.94/3.35 % (3156422)Peak memory usage: 95 MB
% 19.94/3.35 % (3156422)Instructions burned: 40 (million)
% 19.94/3.35 % (3156391)------------------------------
% 19.94/3.35 % (3156391)------------------------------
% 19.94/3.35 % (3156424)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1078506117:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 19.94/3.35 % (3156423)------------------------------
% 19.94/3.35 % (3156423)------------------------------
% 19.94/3.35 % (3156426)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2252882786:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 17.90/5.04 % (3156426)Refutation not found, incomplete strategy
% 17.90/5.04 % (3156426)------------------------------
% 17.90/5.04 % (3156426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.90/5.04 % (3156426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.90/5.04 % (3156426)CaDiCaL version: 2.1.3
% 17.90/5.04 % (3156426)Termination reason: Refutation not found, incomplete strategy
% 17.90/5.04 % (3156426)Time elapsed: 0.018 s
% 17.90/5.04 % (3156426)Peak memory usage: 94 MB
% 17.90/5.04 % (3156426)Instructions burned: 24 (million)
% 17.90/5.04 % (3156429)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3972711444:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi)
% 17.90/5.04 % (3156430)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3924204389:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi)
% 17.90/5.04 % (3156422)------------------------------
% 17.90/5.04 % (3156422)------------------------------
% 17.90/5.04 % (3156426)------------------------------
% 17.90/5.04 % (3156426)------------------------------
% 17.90/5.04 % (3156434)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=2561455455:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 17.90/5.04 % (3156434)Refutation not found, incomplete strategy
% 17.90/5.04 % (3156434)------------------------------
% 17.90/5.04 % (3156434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.90/5.04 % (3156434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.90/5.04 % (3156434)CaDiCaL version: 2.1.3
% 17.90/5.04 % (3156434)Termination reason: Refutation not found, incomplete strategy
% 17.90/5.04 % (3156434)Time elapsed: 0.044 s
% 17.90/5.04 % (3156434)Peak memory usage: 94 MB
% 17.90/5.04 % (3156434)Instructions burned: 79 (million)
% 17.90/5.04 % (3156429)Instruction limit reached!
% 17.90/5.04 % (3156429)------------------------------
% 17.90/5.04 % (3156429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.90/5.04 % (3156429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.90/5.04 % (3156429)CaDiCaL version: 2.1.3
% 17.90/5.04 % (3156429)Termination reason: Instruction limit
% 17.90/5.04 % (3156429)Termination phase: Saturation
% 17.90/5.04 % (3156429)Time elapsed: 0.330 s
% 17.90/5.04 % (3156429)Peak memory usage: 98 MB
% 17.90/5.04 % (3156429)Instructions burned: 594 (million)
% 17.90/5.04 % (3156435)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=143391440:i=134:gtgl=5:slsql=off:gtg=exists_sym_2984 on theBenchmark for (2984ds/134Mi)
% 17.90/5.04 % (3156435)Instruction limit reached!
% 17.90/5.04 % (3156435)------------------------------
% 17.90/5.04 % (3156435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.90/5.04 % (3156435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.90/5.04 % (3156435)CaDiCaL version: 2.1.3
% 17.90/5.04 % (3156435)Termination reason: Instruction limit
% 17.90/5.04 % (3156435)Termination phase: Preprocessing 2
% 17.90/5.04 % (3156435)Time elapsed: 0.072 s
% 17.90/5.04 % (3156435)Peak memory usage: 92 MB
% 17.90/5.04 % (3156435)Instructions burned: 134 (million)
% 17.90/5.04 % (3156437)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1004449179:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/141Mi)
% 17.90/5.04 % (3156434)------------------------------
% 17.90/5.04 % (3156434)------------------------------
% 17.90/5.04 % (3156437)Refutation not found, incomplete strategy
% 17.90/5.04 % (3156437)------------------------------
% 17.90/5.04 % (3156437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.90/5.04 % (3156437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.90/5.04 % (3156437)CaDiCaL version: 2.1.3
% 17.90/5.04 % (3156437)Termination reason: Refutation not found, incomplete strategy
% 17.90/5.04 % (3156437)Time elapsed: 0.018 s
% 17.90/5.04 % (3156437)Peak memory usage: 94 MB
% 17.90/5.04 % (3156437)Instructions burned: 23 (million)
% 17.90/5.04 % (3156439)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=183193121:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2982 on theBenchmark for (2982ds/431Mi)
% 17.90/5.04 % (3156439)Refutation not found, incomplete strategy
% 17.90/5.04 % (3156439)------------------------------
% 17.90/5.04 % (3156439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.90/5.04 % (3156439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.90/5.04 % (3156439)CaDiCaL version: 2.1.3
% 17.90/5.04 % (3156439)Termination reason: Refutation not found, incomplete strategy
% 17.90/5.04 % (3156439)Time elapsed: 0.017 s
% 17.90/5.04 % (3156439)Peak memory usage: 94 MB
% 17.90/5.04 % (3156439)Instructions burned: 21 (million)
% 17.90/5.04 % (3156441)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=383114976:i=6060:aac=none:ins=25_2981 on theBenchmark for (2981ds/6060Mi)
% 17.90/5.04 % (3156437)------------------------------
% 17.90/5.04 % (3156437)------------------------------
% 17.90/5.04 % (3156439)------------------------------
% 17.90/5.04 % (3156439)------------------------------
% 17.90/5.04 % (3156444)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=1069422314:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2978 on theBenchmark for (2978ds/150Mi)
% 17.90/5.04 % (3156414)Instruction limit reached!
% 17.90/5.04 % (3156414)------------------------------
% 17.90/5.04 % (3156414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.90/5.04 % (3156414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.90/5.04 % (3156414)CaDiCaL version: 2.1.3
% 17.90/5.04 % (3156414)Termination reason: Instruction limit
% 17.90/5.04 % (3156414)Termination phase: Saturation
% 17.90/5.04 % (3156414)Time elapsed: 1.458 s
% 17.90/5.04 % (3156414)Peak memory usage: 209 MB
% 17.90/5.04 % (3156414)Instructions burned: 2350 (million)
% 17.90/5.04 % (3156444)Instruction limit reached!
% 17.90/5.04 % (3156444)------------------------------
% 17.90/5.04 % (3156444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.90/5.04 % (3156444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.90/5.04 % (3156444)CaDiCaL version: 2.1.3
% 17.90/5.04 % (3156444)Termination reason: Instruction limit
% 17.90/5.04 % (3156444)Termination phase: Property scanning
% 17.90/5.04 % (3156444)Time elapsed: 0.089 s
% 17.90/5.04 % (3156444)Peak memory usage: 96 MB
% 17.90/5.04 % (3156444)Instructions burned: 151 (million)
% 17.90/5.04 % (3156445)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=340638163:i=14155:bd=all_2977 on theBenchmark for (2977ds/14155Mi)
% 17.90/5.04 % (3156447)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1577742194:i=667:av=off:fsr=off_2976 on theBenchmark for (2976ds/667Mi)
% 17.90/5.04 % (3156449)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=2978614552:s2a=on:i=185:s2at=1.8:fdi=4_2976 on theBenchmark for (2976ds/185Mi)
% 17.90/5.04 % (3156449)Instruction limit reached!
% 17.90/5.04 % (3156449)------------------------------
% 17.90/5.04 % (3156449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.90/5.04 % (3156449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.90/5.04 % (3156449)CaDiCaL version: 2.1.3
% 17.90/5.04 % (3156449)Termination reason: Instruction limit
% 17.90/5.04 % (3156449)Termination phase: Property scanning
% 17.90/5.04 % (3156449)Time elapsed: 0.114 s
% 17.90/5.04 % (3156449)Peak memory usage: 97 MB
% 17.90/5.04 % (3156449)Instructions burned: 186 (million)
% 17.90/5.04 % (3156452)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3299357266:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2973 on theBenchmark for (2973ds/193Mi)
% 17.90/5.04 % (3156447)Instruction limit reached!
% 17.90/5.04 % (3156447)------------------------------
% 17.90/5.04 % (3156447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.90/5.04 % (3156447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.90/5.04 % (3156447)CaDiCaL version: 2.1.3
% 17.90/5.04 % (3156447)Termination reason: Instruction limit
% 17.90/5.04 % (3156447)Termination phase: Saturation
% 17.90/5.04 % (3156447)Time elapsed: 0.359 s
% 17.90/5.04 % (3156447)Peak memory usage: 104 MB
% 17.90/5.04 % (3156447)Instructions burned: 668 (million)
% 17.90/5.04 % (3156452)Instruction limit reached!
% 17.90/5.04 % (3156452)------------------------------
% 17.90/5.04 % (3156452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.90/5.04 % (3156452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.90/5.04 % (3156452)CaDiCaL version: 2.1.3
% 17.90/5.04 % (3156452)Termination reason: Instruction limit
% 17.90/5.04 % (3156452)Termination phase: Saturation
% 17.90/5.04 % (3156452)Time elapsed: 0.087 s
% 17.90/5.04 % (3156452)Peak memory usage: 94 MB
% 17.90/5.04 % (3156452)Instructions burned: 195 (million)
% 17.90/5.04 % (3156454)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1792671848:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2971 on theBenchmark for (2971ds/4850Mi)
% 17.90/5.04 % (3156455)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=206070840:i=12111:sd=1:ss=included_2970 on theBenchmark for (2970ds/12111Mi)
% 17.90/5.04 % (3156454)Refutation not found, incomplete strategy
% 17.90/5.04 % (3156454)------------------------------
% 17.90/5.04 % (3156454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.90/5.04 % (3156454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.90/5.04 % (3156454)CaDiCaL version: 2.1.3
% 17.90/5.04 % (3156454)Termination reason: Refutation not found, incomplete strategy
% 17.90/5.04 % (3156454)Time elapsed: 0.104 s
% 17.90/5.04 % (3156454)Peak memory usage: 98 MB
% 17.90/5.04 % (3156454)Instructions burned: 167 (million)
% 17.90/5.04 % (3156454)------------------------------
% 17.90/5.04 % (3156454)------------------------------
% 17.90/5.04 % (3156458)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3248911964:i=319:kws=precedence:fsr=off_2966 on theBenchmark for (2966ds/319Mi)
% 17.90/5.04 % (3156458)Instruction limit reached!
% 17.90/5.04 % (3156458)------------------------------
% 17.90/5.04 % (3156458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.90/5.04 % (3156458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.90/5.04 % (3156458)CaDiCaL version: 2.1.3
% 17.90/5.04 % (3156458)Termination reason: Instruction limit
% 17.90/5.04 % (3156458)Termination phase: Saturation
% 17.90/5.04 % (3156458)Time elapsed: 0.156 s
% 17.90/5.04 % (3156458)Peak memory usage: 101 MB
% 17.90/5.04 % (3156458)Instructions burned: 319 (million)
% 17.90/5.04 % (3156455)Refutation not found, incomplete strategy
% 17.90/5.04 % (3156455)------------------------------
% 17.90/5.04 % (3156455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.90/5.04 % (3156455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.90/5.04 % (3156455)CaDiCaL version: 2.1.3
% 17.90/5.04 % (3156455)Termination reason: Refutation not found, incomplete strategy
% 17.90/5.04 % (3156455)Time elapsed: 0.685 s
% 17.90/5.04 % (3156455)Peak memory usage: 146 MB
% 17.90/5.04 % (3156455)Instructions burned: 1025 (million)
% 17.90/5.04 % (3156460)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2644231362:i=2064:ep=RST_2962 on theBenchmark for (2962ds/2064Mi)
% 17.90/5.04 % (3156455)------------------------------
% 17.90/5.04 % (3156455)------------------------------
% 17.90/5.04 % (3156462)dis-1011_128_sil=32000:random_seed=3946774297:i=3706:ep=RST:av=off_2959 on theBenchmark for (2959ds/3706Mi)
% 17.90/5.04 % (3156424)First to succeed.
% 17.90/5.04 % (3156424)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3156385"
% 17.90/5.04 % (3156424)Refutation found. Thanks to Tanya!
% 17.90/5.04 % SZS status Theorem for theBenchmark
% 17.90/5.04 % SZS output start Proof for theBenchmark
% See solution above
% 32.62/5.25 % (3156424)------------------------------
% 32.62/5.25 % (3156424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.62/5.25 % (3156424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.62/5.25 % (3156424)CaDiCaL version: 2.1.3
% 32.62/5.25 % (3156424)Termination reason: Refutation
% 32.62/5.25 % (3156424)Time elapsed: 3.127 s
% 32.62/5.25 % (3156424)Peak memory usage: 219 MB
% 32.62/5.25 % (3156424)Instructions burned: 4870 (million)
% 32.62/5.25 % (3156424)------------------------------
% 32.62/5.25 % (3156424)------------------------------
% 32.62/5.25 % (3156385)Success in time 4.616 s
% 32.62/5.25 % Vampire exiting
%------------------------------------------------------------------------------