%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR229+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 : n026.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.59s 5.15s
% Output : Refutation 31.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 23
% Syntax : Number of formulae : 116 ( 33 unt; 5 def)
% Number of atoms : 562 ( 7 equ)
% Maximal formula atoms : 80 ( 4 avg)
% Number of connectives : 669 ( 223 ~; 213 |; 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 : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 279 ( 0 sgn 271 !; 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(f115,axiom,
p__d__subclass(c__Object,c__Physical),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA181) ).
fof(f116,axiom,
p__d__subclass(c__SelfConnectedObject,c__Object),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA182) ).
fof(f171,axiom,
p__d__subclass(c__CorpuscularObject,c__SelfConnectedObject),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA251) ).
fof(f188,axiom,
p__d__subclass(c__ContentBearingPhysical,c__Physical),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA272) ).
fof(f200,axiom,
p__d__subclass(c__Icon,c__ContentBearingPhysical),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA287) ).
fof(f239,axiom,
p__d__subclass(c__Abstract,c__Entity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA330) ).
fof(f2059,axiom,
p__d__subclass(c__OrganicObject,c__CorpuscularObject),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2902) ).
fof(f2170,axiom,
p__d__subclass(c__AnatomicalStructure,c__OrganicObject),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA3024) ).
fof(f2176,axiom,
p__d__subclass(c__BodyPart,c__AnatomicalStructure),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA3031) ).
fof(f7433,conjecture,
? [X0,X1] :
( p__d__instance(X0,c__Icon)
& ~ p__d__instance(X1,c__BodyPart)
& X0 != X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antonymPattern31567) ).
fof(f7434,negated_conjecture,
~ ? [X0,X1] :
( p__d__instance(X0,c__Icon)
& ~ p__d__instance(X1,c__BodyPart)
& X0 != X1 ),
inference(negated_conjecture,[status(cth)],[f7433]) ).
fof(f7435,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(f7436,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(f7446,plain,
! [X0,X1] :
( ~ p__d__instance(X0,c__Icon)
| p__d__instance(X1,c__BodyPart)
| X0 = X1 ),
inference(ennf_transformation,[],[f7434]) ).
fof(f7449,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f7450,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7449]) ).
fof(f7451,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f7452,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7451]) ).
fof(f10265,plain,
! [X0] :
( ? [X1] : p__d__instance(X1,X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(ennf_transformation,[],[f110]) ).
fof(f11037,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(f11038,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,[],[f11037]) ).
fof(f11039,plain,
! [X0,X1] :
( ( p__d__disjoint(X0,X1)
| ( p__d__instance(sK44(X0,X1),X0)
& p__d__instance(sK44(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,[sK44]),skolemize(X2,sK44(X0,X1))],[f11038]) ).
fof(f11242,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,[],[f7435]) ).
fof(f11243,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,[],[f11242]) ).
fof(f11385,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,[],[f7436]) ).
fof(f11386,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,[],[f11385]) ).
fof(f12243,plain,
! [X0] :
( p__d__instance(sK1069(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1069]),skolemize(X1,sK1069(X0))],[f10265]) ).
fof(f12551,plain,
! [X0,X1] :
( p__d__instance(X1,c__BodyPart)
| ~ p__d__instance(X0,c__Icon)
| X0 = X1 ),
inference(cnf_transformation,[],[f7446]) ).
fof(f12562,plain,
p__d__subclass(c__Icon,c__ContentBearingPhysical),
inference(cnf_transformation,[],[f200]) ).
fof(f12563,plain,
! [X2,X0,X1] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(cnf_transformation,[],[f7450]) ).
fof(f12564,plain,
! [X2,X0,X1] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(cnf_transformation,[],[f7452]) ).
fof(f12587,plain,
! [X3,X0,X1] :
( ~ p__d__disjoint(X0,X1)
| ~ p__d__instance(X3,X1)
| ~ p__d__instance(X3,X0) ),
inference(cnf_transformation,[],[f11039]) ).
fof(f12598,plain,
p__d__subclass(c__ContentBearingPhysical,c__Physical),
inference(cnf_transformation,[],[f188]) ).
fof(f12652,plain,
p__d__subclass(c__Object,c__Physical),
inference(cnf_transformation,[],[f115]) ).
fof(f13551,plain,
p__d__subclass(c__SelfConnectedObject,c__Object),
inference(cnf_transformation,[],[f116]) ).
fof(f13742,plain,
! [X2,X0,X1] :
( p__d__disjointDecomposition3(X0,X1,X2)
| ~ p__d__partition3(X0,X1,X2) ),
inference(cnf_transformation,[],[f11243]) ).
fof(f14638,plain,
! [X2,X0,X1] :
( ~ p__d__disjointDecomposition3(X0,X1,X2)
| p__d__disjoint(X1,X2) ),
inference(cnf_transformation,[],[f11386]) ).
fof(f15740,plain,
p__d__subclass(c__AnatomicalStructure,c__OrganicObject),
inference(cnf_transformation,[],[f2170]) ).
fof(f15744,plain,
p__d__subclass(c__OrganicObject,c__CorpuscularObject),
inference(cnf_transformation,[],[f2059]) ).
fof(f15891,plain,
p__d__subclass(c__CorpuscularObject,c__SelfConnectedObject),
inference(cnf_transformation,[],[f171]) ).
fof(f16580,plain,
p__d__subclass(c__BodyPart,c__AnatomicalStructure),
inference(cnf_transformation,[],[f2176]) ).
fof(f17632,plain,
p__d__subclass(c__Abstract,c__Entity),
inference(cnf_transformation,[],[f239]) ).
fof(f17633,plain,
p__d__partition3(c__Entity,c__Physical,c__Abstract),
inference(cnf_transformation,[],[f107]) ).
fof(f19646,plain,
p__d__subclass(c__Physical,c__Entity),
inference(cnf_transformation,[],[f112]) ).
fof(f19649,plain,
! [X0] :
( p__d__instance(sK1069(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(cnf_transformation,[],[f12243]) ).
fof(f22935,plain,
! [X2,X0,X1] :
( ~ p__d__partition3(X2,X0,X1)
| p__d__disjoint(X0,X1) ),
inference(resolution,[],[f14638,f13742]) ).
fof(f23246,plain,
p__d__disjoint(c__Physical,c__Abstract),
inference(resolution,[],[f17633,f22935]) ).
fof(f23410,plain,
! [X0] :
( ~ p__d__instance(X0,c__Abstract)
| ~ p__d__instance(X0,c__Physical) ),
inference(resolution,[],[f23246,f12587]) ).
fof(f23414,plain,
( ~ p__d__instance(sK1069(c__Abstract),c__Physical)
| ~ p__d__subclass(c__Abstract,c__Entity) ),
inference(resolution,[],[f23410,f19649]) ).
fof(f23415,plain,
~ p__d__instance(sK1069(c__Abstract),c__Physical),
inference(forward_subsumption_resolution,[],[f23414,f17632]) ).
fof(f23416,plain,
! [X0] :
( ~ p__d__instance(sK1069(c__Abstract),X0)
| ~ p__d__subclass(X0,c__Physical) ),
inference(resolution,[],[f23415,f12563]) ).
fof(f23418,plain,
! [X0] :
( ~ p__d__subclass(c__BodyPart,c__Physical)
| ~ p__d__instance(X0,c__Icon)
| sK1069(c__Abstract) = X0 ),
inference(resolution,[],[f23416,f12551]) ).
fof(f23422,definition,
( spl1215_83
<=> ! [X0] :
( ~ p__d__instance(X0,c__Icon)
| sK1069(c__Abstract) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl1215_83])],[avatar_definition]) ).
fof(f23423,plain,
( ! [X0] :
( sK1069(c__Abstract) = X0
| ~ p__d__instance(X0,c__Icon) )
| ~ spl1215_83 ),
inference(avatar_component_clause,[],[f23422]) ).
fof(f23425,definition,
( spl1215_84
<=> p__d__subclass(c__BodyPart,c__Physical) ),
introduced(definition,[new_symbols(definition,[spl1215_84])],[avatar_definition]) ).
fof(f23427,plain,
( ~ p__d__subclass(c__BodyPart,c__Physical)
| spl1215_84 ),
inference(avatar_component_clause,[],[f23425]) ).
fof(f23428,plain,
( spl1215_83
| ~ spl1215_84 ),
inference(avatar_split_clause,[],[f23418,f23425,f23422]) ).
fof(f23430,plain,
( ! [X0] :
( ~ p__d__subclass(c__BodyPart,X0)
| ~ p__d__subclass(X0,c__Physical) )
| spl1215_84 ),
inference(resolution,[],[f23427,f12564]) ).
fof(f24960,plain,
( ~ p__d__subclass(c__AnatomicalStructure,c__Physical)
| spl1215_84 ),
inference(resolution,[],[f16580,f23430]) ).
fof(f24973,plain,
( ! [X0] :
( ~ p__d__subclass(c__AnatomicalStructure,X0)
| ~ p__d__subclass(X0,c__Physical) )
| spl1215_84 ),
inference(resolution,[],[f24960,f12564]) ).
fof(f25021,definition,
( spl1215_325
<=> p__d__subclass(c__Icon,c__Entity) ),
introduced(definition,[new_symbols(definition,[spl1215_325])],[avatar_definition]) ).
fof(f25022,plain,
( p__d__subclass(c__Icon,c__Entity)
| ~ spl1215_325 ),
inference(avatar_component_clause,[],[f25021]) ).
fof(f25023,plain,
( ~ p__d__subclass(c__Icon,c__Entity)
| spl1215_325 ),
inference(avatar_component_clause,[],[f25021]) ).
fof(f25028,plain,
( ! [X0] :
( ~ p__d__subclass(c__Icon,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl1215_325 ),
inference(resolution,[],[f25023,f12564]) ).
fof(f25029,plain,
( ~ p__d__subclass(c__ContentBearingPhysical,c__Entity)
| spl1215_325 ),
inference(resolution,[],[f25028,f12562]) ).
fof(f25032,plain,
( ! [X0] :
( ~ p__d__subclass(c__ContentBearingPhysical,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl1215_325 ),
inference(resolution,[],[f25029,f12564]) ).
fof(f25033,plain,
( ~ p__d__subclass(c__Physical,c__Entity)
| spl1215_325 ),
inference(resolution,[],[f25032,f12598]) ).
fof(f25036,plain,
( $false
| spl1215_325 ),
inference(forward_subsumption_resolution,[],[f25033,f19646]) ).
fof(f25037,plain,
spl1215_325,
inference(avatar_contradiction_clause,[],[f25036]) ).
fof(f27418,definition,
( spl1215_659
<=> p__d__instance(sK1069(c__Icon),c__Physical) ),
introduced(definition,[new_symbols(definition,[spl1215_659])],[avatar_definition]) ).
fof(f27419,plain,
( ~ p__d__instance(sK1069(c__Icon),c__Physical)
| spl1215_659 ),
inference(avatar_component_clause,[],[f27418]) ).
fof(f27420,plain,
( p__d__instance(sK1069(c__Icon),c__Physical)
| ~ spl1215_659 ),
inference(avatar_component_clause,[],[f27418]) ).
fof(f28289,plain,
( ~ p__d__subclass(c__OrganicObject,c__Physical)
| spl1215_84 ),
inference(resolution,[],[f15740,f24973]) ).
fof(f28361,plain,
( ! [X0] :
( ~ p__d__subclass(c__OrganicObject,X0)
| ~ p__d__subclass(X0,c__Physical) )
| spl1215_84 ),
inference(resolution,[],[f28289,f12564]) ).
fof(f28362,plain,
( ~ p__d__subclass(c__CorpuscularObject,c__Physical)
| spl1215_84 ),
inference(resolution,[],[f28361,f15744]) ).
fof(f28365,plain,
( ! [X0] :
( ~ p__d__subclass(c__CorpuscularObject,X0)
| ~ p__d__subclass(X0,c__Physical) )
| spl1215_84 ),
inference(resolution,[],[f28362,f12564]) ).
fof(f28366,plain,
( ~ p__d__subclass(c__SelfConnectedObject,c__Physical)
| spl1215_84 ),
inference(resolution,[],[f28365,f15891]) ).
fof(f28370,plain,
( ! [X0] :
( ~ p__d__subclass(c__SelfConnectedObject,X0)
| ~ p__d__subclass(X0,c__Physical) )
| spl1215_84 ),
inference(resolution,[],[f28366,f12564]) ).
fof(f28371,plain,
( ~ p__d__subclass(c__Object,c__Physical)
| spl1215_84 ),
inference(resolution,[],[f28370,f13551]) ).
fof(f28374,plain,
( $false
| spl1215_84 ),
inference(forward_subsumption_resolution,[],[f28371,f12652]) ).
fof(f28375,plain,
spl1215_84,
inference(avatar_contradiction_clause,[],[f28374]) ).
fof(f28380,plain,
( ! [X0] :
( ~ p__d__instance(X0,c__Icon)
| ~ p__d__instance(X0,c__Physical) )
| ~ spl1215_83 ),
inference(superposition,[],[f23415,f23423]) ).
fof(f28423,definition,
( spl1215_802
<=> p__d__instance(sK1069(c__Icon),c__Icon) ),
introduced(definition,[new_symbols(definition,[spl1215_802])],[avatar_definition]) ).
fof(f28424,plain,
( p__d__instance(sK1069(c__Icon),c__Icon)
| ~ spl1215_802 ),
inference(avatar_component_clause,[],[f28423]) ).
fof(f28425,plain,
( ~ p__d__instance(sK1069(c__Icon),c__Icon)
| spl1215_802 ),
inference(avatar_component_clause,[],[f28423]) ).
fof(f28428,plain,
( ~ p__d__subclass(c__Icon,c__Entity)
| spl1215_802 ),
inference(resolution,[],[f28425,f19649]) ).
fof(f28430,plain,
( $false
| ~ spl1215_325
| spl1215_802 ),
inference(forward_subsumption_resolution,[],[f28428,f25022]) ).
fof(f28431,plain,
( ~ spl1215_325
| spl1215_802 ),
inference(avatar_contradiction_clause,[],[f28430]) ).
fof(f28455,plain,
( ~ p__d__instance(sK1069(c__Icon),c__Physical)
| ~ spl1215_83
| ~ spl1215_802 ),
inference(resolution,[],[f28380,f28424]) ).
fof(f28458,plain,
( $false
| ~ spl1215_83
| ~ spl1215_659
| ~ spl1215_802 ),
inference(forward_subsumption_resolution,[],[f28455,f27420]) ).
fof(f28459,plain,
( ~ spl1215_83
| ~ spl1215_659
| ~ spl1215_802 ),
inference(avatar_contradiction_clause,[],[f28458]) ).
fof(f28462,plain,
( ! [X0] :
( ~ p__d__instance(sK1069(c__Icon),X0)
| ~ p__d__subclass(X0,c__Physical) )
| spl1215_659 ),
inference(resolution,[],[f27419,f12563]) ).
fof(f28464,plain,
( ~ p__d__subclass(c__Icon,c__Physical)
| spl1215_659
| ~ spl1215_802 ),
inference(resolution,[],[f28462,f28424]) ).
fof(f28485,plain,
( ! [X0] :
( ~ p__d__subclass(c__Icon,X0)
| ~ p__d__subclass(X0,c__Physical) )
| spl1215_659
| ~ spl1215_802 ),
inference(resolution,[],[f28464,f12564]) ).
fof(f28486,plain,
( ~ p__d__subclass(c__ContentBearingPhysical,c__Physical)
| spl1215_659
| ~ spl1215_802 ),
inference(resolution,[],[f28485,f12562]) ).
fof(f28490,plain,
( $false
| spl1215_659
| ~ spl1215_802 ),
inference(forward_subsumption_resolution,[],[f28486,f12598]) ).
fof(f28491,plain,
( spl1215_659
| ~ spl1215_802 ),
inference(avatar_contradiction_clause,[],[f28490]) ).
cnf(s45,plain,
( spl1215_83
| ~ spl1215_84 ),
inference(sat_conversion,[],[f23428]) ).
cnf(s168,plain,
spl1215_325,
inference(sat_conversion,[],[f25037]) ).
cnf(s420,plain,
spl1215_84,
inference(sat_conversion,[],[f28375]) ).
cnf(s424,plain,
( ~ spl1215_325
| spl1215_802 ),
inference(sat_conversion,[],[f28431]) ).
cnf(s425,plain,
( ~ spl1215_83
| ~ spl1215_659
| ~ spl1215_802 ),
inference(sat_conversion,[],[f28459]) ).
cnf(s428,plain,
( spl1215_659
| ~ spl1215_802 ),
inference(sat_conversion,[],[f28491]) ).
cnf(s435,plain,
spl1215_802,
inference(rat,[],[s424,s168]) ).
cnf(s436,plain,
spl1215_659,
inference(rat,[],[s428,s435]) ).
cnf(s437,plain,
~ spl1215_83,
inference(rat,[],[s425,s435,s436]) ).
cnf(s441,plain,
$false,
inference(rat,[],[s45,s420,s437]) ).
fof(f28492,plain,
$false,
inference(avatar_sat_refutation,[],[s441]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR229+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.09/0.18 % Computer : n026.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 23:51:57 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 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
% 9.14/2.08 % (210684)Detected formulas, will run a generic FOF schedule.
% 9.14/2.08 % (210692)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=11792900:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 9.14/2.08 % (210692)Refutation not found, incomplete strategy
% 9.14/2.08 % (210692)------------------------------
% 9.14/2.08 % (210692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.14/2.08 % (210692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.14/2.08 % (210692)CaDiCaL version: 2.1.3
% 9.14/2.08 % (210692)Termination reason: Refutation not found, incomplete strategy
% 9.14/2.08 % (210692)Time elapsed: 0.010 s
% 9.14/2.08 % (210692)Peak memory usage: 93 MB
% 9.14/2.08 % (210692)Instructions burned: 23 (million)
% 9.14/2.08 % (210691)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=3471962135:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 9.14/2.08 % (210689)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=558981670:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 9.14/2.08 % (210690)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=272375538:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 9.14/2.08 % (210694)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1572723159:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 9.14/2.08 % (210693)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3162563404:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 9.14/2.08 % (210695)dis-21_1_sil=8000:lcm=predicate:random_seed=2085597535:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 9.14/2.08 % (210693)Instruction limit reached!
% 9.14/2.08 % (210693)------------------------------
% 9.14/2.08 % (210693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.14/2.08 % (210693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.14/2.08 % (210693)CaDiCaL version: 2.1.3
% 9.14/2.08 % (210693)Termination reason: Instruction limit
% 9.14/2.08 % (210693)Termination phase: Saturation
% 9.14/2.08 % (210693)Time elapsed: 0.070 s
% 9.14/2.08 % (210693)Peak memory usage: 93 MB
% 9.14/2.08 % (210693)Instructions burned: 119 (million)
% 9.14/2.08 % (210695)Instruction limit reached!
% 9.14/2.08 % (210695)------------------------------
% 9.14/2.08 % (210695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.14/2.08 % (210695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.14/2.08 % (210695)CaDiCaL version: 2.1.3
% 9.14/2.08 % (210695)Termination reason: Instruction limit
% 9.14/2.08 % (210695)Termination phase: Saturation
% 9.14/2.08 % (210695)Time elapsed: 0.072 s
% 9.14/2.08 % (210695)Peak memory usage: 95 MB
% 9.14/2.08 % (210695)Instructions burned: 129 (million)
% 9.14/2.08 % (210694)Instruction limit reached!
% 9.14/2.08 % (210694)------------------------------
% 9.14/2.08 % (210694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.14/2.08 % (210694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.14/2.08 % (210694)CaDiCaL version: 2.1.3
% 9.14/2.08 % (210694)Termination reason: Instruction limit
% 9.14/2.08 % (210694)Termination phase: Preprocessing 3
% 9.14/2.08 % (210694)Time elapsed: 0.091 s
% 9.14/2.08 % (210694)Peak memory usage: 94 MB
% 9.14/2.08 % (210694)Instructions burned: 140 (million)
% 9.14/2.08 % (210692)------------------------------
% 9.14/2.08 % (210692)------------------------------
% 9.14/2.08 % (210703)lrs+10_1_sil=8000:sp=occurrence:random_seed=4195294837:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 9.14/2.08 % (210706)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=2992666729:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 9.14/2.08 % (210704)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1266910167:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 9.14/2.08 % (210703)Refutation not found, incomplete strategy
% 9.14/2.08 % (210703)------------------------------
% 9.14/2.08 % (210703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.52 % (210703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.47/2.52 % (210703)CaDiCaL version: 2.1.3
% 11.47/2.52 % (210703)Termination reason: Refutation not found, incomplete strategy
% 11.47/2.52 % (210703)Time elapsed: 0.021 s
% 11.47/2.52 % (210703)Peak memory usage: 94 MB
% 11.47/2.52 % (210703)Instructions burned: 26 (million)
% 11.47/2.52 % (210705)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2600668849:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 11.47/2.52 % (210704)Refutation not found, incomplete strategy
% 11.47/2.52 % (210704)------------------------------
% 11.47/2.52 % (210704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.52 % (210704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.47/2.52 % (210704)CaDiCaL version: 2.1.3
% 11.47/2.52 % (210704)Termination reason: Refutation not found, incomplete strategy
% 11.47/2.52 % (210704)Time elapsed: 0.032 s
% 11.47/2.52 % (210704)Peak memory usage: 94 MB
% 11.47/2.52 % (210704)Instructions burned: 60 (million)
% 11.47/2.52 % (210705)Refutation not found, incomplete strategy
% 11.47/2.52 % (210705)------------------------------
% 11.47/2.52 % (210705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.52 % (210705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.47/2.52 % (210705)CaDiCaL version: 2.1.3
% 11.47/2.52 % (210705)Termination reason: Refutation not found, incomplete strategy
% 11.47/2.52 % (210705)Time elapsed: 0.017 s
% 11.47/2.52 % (210705)Peak memory usage: 94 MB
% 11.47/2.52 % (210705)Instructions burned: 20 (million)
% 11.47/2.52 % (210706)Instruction limit reached!
% 11.47/2.52 % (210706)------------------------------
% 11.47/2.52 % (210706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.52 % (210706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.47/2.52 % (210706)CaDiCaL version: 2.1.3
% 11.47/2.52 % (210706)Termination reason: Instruction limit
% 11.47/2.52 % (210706)Termination phase: Saturation
% 11.47/2.52 % (210706)Time elapsed: 0.074 s
% 11.47/2.52 % (210706)Peak memory usage: 99 MB
% 11.47/2.52 % (210706)Instructions burned: 252 (million)
% 11.47/2.52 % (210711)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4039372495:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 11.47/2.52 % (210711)Refutation not found, incomplete strategy
% 11.47/2.52 % (210711)------------------------------
% 11.47/2.52 % (210711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.52 % (210711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.47/2.52 % (210711)CaDiCaL version: 2.1.3
% 11.47/2.52 % (210711)Termination reason: Refutation not found, incomplete strategy
% 11.47/2.52 % (210711)Time elapsed: 0.013 s
% 11.47/2.52 % (210711)Peak memory usage: 94 MB
% 11.47/2.52 % (210711)Instructions burned: 33 (million)
% 11.47/2.52 % (210703)------------------------------
% 11.47/2.52 % (210703)------------------------------
% 11.47/2.52 % (210705)------------------------------
% 11.47/2.52 % (210705)------------------------------
% 11.47/2.52 % (210704)------------------------------
% 11.47/2.52 % (210704)------------------------------
% 11.47/2.52 % (210711)------------------------------
% 11.47/2.52 % (210711)------------------------------
% 11.47/2.52 % (210713)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=631043985:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 11.47/2.52 % (210715)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1580970966:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 11.47/2.52 % (210716)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4035314177:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 11.47/2.52 % (210714)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=897405438:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 11.47/2.52 % (210716)Instruction limit reached!
% 11.47/2.52 % (210716)------------------------------
% 11.47/2.52 % (210716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.52 % (210716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.47/2.52 % (210716)CaDiCaL version: 2.1.3
% 11.47/2.52 % (210716)Termination reason: Instruction limit
% 11.47/2.52 % (210716)Termination phase: Property scanning
% 11.47/2.52 % (210716)Time elapsed: 0.031 s
% 17.71/3.30 % (210716)Peak memory usage: 92 MB
% 17.71/3.30 % (210716)Instructions burned: 118 (million)
% 17.71/3.30 % (210691)Refutation not found, incomplete strategy
% 17.71/3.30 % (210691)------------------------------
% 17.71/3.30 % (210691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.71/3.30 % (210691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.71/3.30 % (210691)CaDiCaL version: 2.1.3
% 17.71/3.30 % (210691)Termination reason: Refutation not found, incomplete strategy
% 17.71/3.30 % (210691)Time elapsed: 0.688 s
% 17.71/3.30 % (210691)Peak memory usage: 146 MB
% 17.71/3.30 % (210691)Instructions burned: 1018 (million)
% 17.71/3.30 % (210714)Instruction limit reached!
% 17.71/3.30 % (210714)------------------------------
% 17.71/3.30 % (210714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.71/3.30 % (210714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.71/3.30 % (210714)CaDiCaL version: 2.1.3
% 17.71/3.30 % (210714)Termination reason: Instruction limit
% 17.71/3.30 % (210714)Termination phase: Saturation
% 17.71/3.30 % (210714)Time elapsed: 0.058 s
% 17.71/3.30 % (210714)Peak memory usage: 94 MB
% 17.71/3.30 % (210714)Instructions burned: 113 (million)
% 17.71/3.30 % (210715)Instruction limit reached!
% 17.71/3.30 % (210715)------------------------------
% 17.71/3.30 % (210715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.71/3.30 % (210715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.71/3.30 % (210715)CaDiCaL version: 2.1.3
% 17.71/3.30 % (210715)Termination reason: Instruction limit
% 17.71/3.30 % (210715)Termination phase: Property scanning
% 17.71/3.30 % (210715)Time elapsed: 0.075 s
% 17.71/3.30 % (210715)Peak memory usage: 96 MB
% 17.71/3.30 % (210715)Instructions burned: 128 (million)
% 17.71/3.30 % (210721)lrs+10_1_sil=8000:sp=occurrence:random_seed=2046721976:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 17.71/3.30 % (210722)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1791315341:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 17.71/3.30 % (210722)Refutation not found, incomplete strategy
% 17.71/3.30 % (210722)------------------------------
% 17.71/3.30 % (210722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.71/3.30 % (210722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.71/3.30 % (210722)CaDiCaL version: 2.1.3
% 17.71/3.30 % (210722)Termination reason: Refutation not found, incomplete strategy
% 17.71/3.30 % (210722)Time elapsed: 0.016 s
% 17.71/3.30 % (210722)Peak memory usage: 93 MB
% 17.71/3.30 % (210722)Instructions burned: 19 (million)
% 17.71/3.30 % (210723)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2267412996:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 17.71/3.30 % (210690)Refutation not found, incomplete strategy
% 17.71/3.30 % (210690)------------------------------
% 17.71/3.30 % (210690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.71/3.30 % (210690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.71/3.30 % (210690)CaDiCaL version: 2.1.3
% 17.71/3.30 % (210690)Termination reason: Refutation not found, incomplete strategy
% 17.71/3.30 % (210690)Time elapsed: 0.906 s
% 17.71/3.30 % (210690)Peak memory usage: 138 MB
% 17.71/3.30 % (210690)Instructions burned: 1284 (million)
% 17.71/3.30 % (210691)------------------------------
% 17.71/3.30 % (210691)------------------------------
% 17.71/3.30 % (210721)Instruction limit reached!
% 17.71/3.30 % (210721)------------------------------
% 17.71/3.30 % (210721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.71/3.30 % (210721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.71/3.30 % (210721)CaDiCaL version: 2.1.3
% 17.71/3.30 % (210721)Termination reason: Instruction limit
% 17.71/3.30 % (210721)Termination phase: Saturation
% 17.71/3.30 % (210721)Time elapsed: 0.289 s
% 17.71/3.30 % (210721)Peak memory usage: 104 MB
% 17.71/3.30 % (210721)Instructions burned: 912 (million)
% 17.71/3.30 % (210722)------------------------------
% 17.71/3.30 % (210722)------------------------------
% 17.71/3.30 % (210727)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1408216994:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 17.71/3.30 % (210727)Refutation not found, incomplete strategy
% 17.71/3.30 % (210727)------------------------------
% 17.71/3.30 % (210727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.59/5.15 % (210727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.59/5.15 % (210727)CaDiCaL version: 2.1.3
% 17.59/5.15 % (210727)Termination reason: Refutation not found, incomplete strategy
% 17.59/5.15 % (210727)Time elapsed: 0.019 s
% 17.59/5.15 % (210727)Peak memory usage: 94 MB
% 17.59/5.15 % (210727)Instructions burned: 26 (million)
% 17.59/5.15 % (210728)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1677425263:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 17.59/5.15 % (210690)------------------------------
% 17.59/5.15 % (210690)------------------------------
% 17.59/5.15 % (210730)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1291160801:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi)
% 17.59/5.15 % (210732)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=2791786673:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 17.59/5.15 % (210728)Instruction limit reached!
% 17.59/5.15 % (210728)------------------------------
% 17.59/5.15 % (210728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.59/5.15 % (210728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.59/5.15 % (210728)CaDiCaL version: 2.1.3
% 17.59/5.15 % (210728)Termination reason: Instruction limit
% 17.59/5.15 % (210728)Termination phase: Saturation
% 17.59/5.15 % (210728)Time elapsed: 0.177 s
% 17.59/5.15 % (210728)Peak memory usage: 99 MB
% 17.59/5.15 % (210728)Instructions burned: 593 (million)
% 17.59/5.15 % (210732)Refutation not found, incomplete strategy
% 17.59/5.15 % (210732)------------------------------
% 17.59/5.15 % (210732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.59/5.15 % (210732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.59/5.15 % (210732)CaDiCaL version: 2.1.3
% 17.59/5.15 % (210732)Termination reason: Refutation not found, incomplete strategy
% 17.59/5.15 % (210732)Time elapsed: 0.044 s
% 17.59/5.15 % (210732)Peak memory usage: 94 MB
% 17.59/5.15 % (210732)Instructions burned: 79 (million)
% 17.59/5.15 % (210727)------------------------------
% 17.59/5.15 % (210727)------------------------------
% 17.59/5.15 % (210735)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1980078264:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 17.59/5.15 % (210735)Instruction limit reached!
% 17.59/5.15 % (210735)------------------------------
% 17.59/5.15 % (210735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.59/5.15 % (210735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.59/5.15 % (210735)CaDiCaL version: 2.1.3
% 17.59/5.15 % (210735)Termination reason: Instruction limit
% 17.59/5.15 % (210735)Termination phase: Preprocessing 2
% 17.59/5.15 % (210735)Time elapsed: 0.042 s
% 17.59/5.15 % (210735)Peak memory usage: 92 MB
% 17.59/5.15 % (210735)Instructions burned: 135 (million)
% 17.59/5.15 % (210736)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3594835086:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/141Mi)
% 17.59/5.15 % (210736)Refutation not found, incomplete strategy
% 17.59/5.15 % (210736)------------------------------
% 17.59/5.15 % (210736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.59/5.15 % (210736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.59/5.15 % (210736)CaDiCaL version: 2.1.3
% 17.59/5.15 % (210736)Termination reason: Refutation not found, incomplete strategy
% 17.59/5.15 % (210736)Time elapsed: 0.018 s
% 17.59/5.15 % (210736)Peak memory usage: 93 MB
% 17.59/5.15 % (210736)Instructions burned: 23 (million)
% 17.59/5.15 % (210738)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=200959651:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2982 on theBenchmark for (2982ds/431Mi)
% 17.59/5.15 % (210738)Refutation not found, incomplete strategy
% 17.59/5.15 % (210738)------------------------------
% 17.59/5.15 % (210738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.59/5.15 % (210738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.59/5.15 % (210738)CaDiCaL version: 2.1.3
% 17.59/5.15 % (210738)Termination reason: Refutation not found, incomplete strategy
% 17.59/5.15 % (210738)Time elapsed: 0.010 s
% 17.59/5.15 % (210738)Peak memory usage: 94 MB
% 17.59/5.15 % (210738)Instructions burned: 21 (million)
% 17.59/5.15 % (210732)------------------------------
% 17.59/5.15 % (210732)------------------------------
% 17.59/5.15 % (210738)------------------------------
% 17.59/5.15 % (210738)------------------------------
% 17.59/5.15 % (210741)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=1017565572:i=6060:aac=none:ins=25_2980 on theBenchmark for (2980ds/6060Mi)
% 17.59/5.15 % (210736)------------------------------
% 17.59/5.15 % (210736)------------------------------
% 17.59/5.15 % (210742)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=3224634977:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2979 on theBenchmark for (2979ds/150Mi)
% 17.59/5.15 % (210742)Instruction limit reached!
% 17.59/5.15 % (210742)------------------------------
% 17.59/5.15 % (210742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.59/5.15 % (210742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.59/5.15 % (210742)CaDiCaL version: 2.1.3
% 17.59/5.15 % (210742)Termination reason: Instruction limit
% 17.59/5.15 % (210742)Termination phase: Property scanning
% 17.59/5.15 % (210742)Time elapsed: 0.054 s
% 17.59/5.15 % (210742)Peak memory usage: 96 MB
% 17.59/5.15 % (210742)Instructions burned: 155 (million)
% 17.59/5.15 % (210744)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=773163819:i=14155:bd=all_2979 on theBenchmark for (2979ds/14155Mi)
% 17.59/5.15 % (210746)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3062251444:i=667:av=off:fsr=off_2978 on theBenchmark for (2978ds/667Mi)
% 17.59/5.15 % (210713)Instruction limit reached!
% 17.59/5.15 % (210713)------------------------------
% 17.59/5.15 % (210713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.59/5.15 % (210713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.59/5.15 % (210713)CaDiCaL version: 2.1.3
% 17.59/5.15 % (210713)Termination reason: Instruction limit
% 17.59/5.15 % (210713)Termination phase: Saturation
% 17.59/5.15 % (210713)Time elapsed: 1.461 s
% 17.59/5.15 % (210713)Peak memory usage: 199 MB
% 17.59/5.15 % (210713)Instructions burned: 2351 (million)
% 17.59/5.15 % (210746)Instruction limit reached!
% 17.59/5.15 % (210746)------------------------------
% 17.59/5.15 % (210746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.59/5.15 % (210746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.59/5.15 % (210746)CaDiCaL version: 2.1.3
% 17.59/5.15 % (210746)Termination reason: Instruction limit
% 17.59/5.15 % (210746)Termination phase: Saturation
% 17.59/5.15 % (210746)Time elapsed: 0.190 s
% 17.59/5.15 % (210746)Peak memory usage: 106 MB
% 17.59/5.15 % (210746)Instructions burned: 668 (million)
% 17.59/5.15 % (210749)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=681776704:s2a=on:i=185:s2at=1.8:fdi=4_2976 on theBenchmark for (2976ds/185Mi)
% 17.59/5.15 % (210750)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1323666334:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2975 on theBenchmark for (2975ds/193Mi)
% 17.59/5.15 % (210750)Refutation not found, incomplete strategy
% 17.59/5.15 % (210750)------------------------------
% 17.59/5.15 % (210750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.59/5.15 % (210750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.59/5.15 % (210750)CaDiCaL version: 2.1.3
% 17.59/5.15 % (210750)Termination reason: Refutation not found, incomplete strategy
% 17.59/5.15 % (210750)Time elapsed: 0.020 s
% 17.59/5.15 % (210750)Peak memory usage: 94 MB
% 17.59/5.15 % (210750)Instructions burned: 55 (million)
% 17.59/5.15 % (210749)Instruction limit reached!
% 17.59/5.15 % (210749)------------------------------
% 17.59/5.15 % (210749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.59/5.15 % (210749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.59/5.15 % (210749)CaDiCaL version: 2.1.3
% 17.59/5.15 % (210749)Termination reason: Instruction limit
% 17.59/5.15 % (210749)Termination phase: Property scanning
% 17.59/5.15 % (210749)Time elapsed: 0.120 s
% 17.59/5.15 % (210749)Peak memory usage: 96 MB
% 17.59/5.15 % (210749)Instructions burned: 189 (million)
% 17.59/5.15 % (210750)------------------------------
% 17.59/5.15 % (210750)------------------------------
% 17.59/5.15 % (210753)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3727881993:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2973 on theBenchmark for (2973ds/4850Mi)
% 17.59/5.15 % (210754)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=4231802805:i=12111:sd=1:ss=included_2972 on theBenchmark for (2972ds/12111Mi)
% 17.59/5.15 % (210753)Refutation not found, incomplete strategy
% 17.59/5.15 % (210753)------------------------------
% 17.59/5.15 % (210753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.59/5.15 % (210753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.59/5.15 % (210753)CaDiCaL version: 2.1.3
% 17.59/5.15 % (210753)Termination reason: Refutation not found, incomplete strategy
% 17.59/5.15 % (210753)Time elapsed: 0.102 s
% 17.59/5.15 % (210753)Peak memory usage: 98 MB
% 17.59/5.15 % (210753)Instructions burned: 167 (million)
% 17.59/5.15 % (210753)------------------------------
% 17.59/5.15 % (210753)------------------------------
% 17.59/5.15 % (210754)Refutation not found, incomplete strategy
% 17.59/5.15 % (210754)------------------------------
% 17.59/5.15 % (210754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.59/5.15 % (210754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.59/5.15 % (210754)CaDiCaL version: 2.1.3
% 17.59/5.15 % (210754)Termination reason: Refutation not found, incomplete strategy
% 17.59/5.15 % (210754)Time elapsed: 0.435 s
% 17.59/5.15 % (210754)Peak memory usage: 147 MB
% 17.59/5.15 % (210754)Instructions burned: 1019 (million)
% 17.59/5.15 % (210757)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1098398837:i=319:kws=precedence:fsr=off_2968 on theBenchmark for (2968ds/319Mi)
% 17.59/5.15 % (210754)------------------------------
% 17.59/5.15 % (210754)------------------------------
% 17.59/5.15 % (210757)Instruction limit reached!
% 17.59/5.15 % (210757)------------------------------
% 17.59/5.15 % (210757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.59/5.15 % (210757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.59/5.15 % (210757)CaDiCaL version: 2.1.3
% 17.59/5.15 % (210757)Termination reason: Instruction limit
% 17.59/5.15 % (210757)Termination phase: Saturation
% 17.59/5.15 % (210757)Time elapsed: 0.163 s
% 17.59/5.15 % (210757)Peak memory usage: 101 MB
% 17.59/5.15 % (210757)Instructions burned: 321 (million)
% 17.59/5.15 % (210760)dis-1011_128_sil=32000:random_seed=110900806:i=3706:ep=RST:av=off_2965 on theBenchmark for (2965ds/3706Mi)
% 17.59/5.15 % (210759)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2890107702:i=2064:ep=RST_2965 on theBenchmark for (2965ds/2064Mi)
% 17.59/5.15 % (210759)Instruction limit reached!
% 17.59/5.15 % (210759)------------------------------
% 17.59/5.15 % (210759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.59/5.15 % (210759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.59/5.15 % (210759)CaDiCaL version: 2.1.3
% 17.59/5.15 % (210759)Termination reason: Instruction limit
% 17.59/5.15 % (210759)Termination phase: Saturation
% 17.59/5.15 % (210759)Time elapsed: 0.594 s
% 17.59/5.15 % (210759)Peak memory usage: 115 MB
% 17.59/5.15 % (210759)Instructions burned: 2065 (million)
% 17.59/5.15 % (210723)First to succeed.
% 17.59/5.15 % (210723)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-210684"
% 17.59/5.15 % (210763)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=515661297:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2958 on theBenchmark for (2958ds/757Mi)
% 17.59/5.15 % (210763)Refutation not found, incomplete strategy
% 17.59/5.15 % (210763)------------------------------
% 17.59/5.15 % (210763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.59/5.15 % (210763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.59/5.15 % (210763)CaDiCaL version: 2.1.3
% 17.59/5.15 % (210763)Termination reason: Refutation not found, incomplete strategy
% 17.59/5.15 % (210763)Time elapsed: 0.014 s
% 17.59/5.15 % (210763)Peak memory usage: 94 MB
% 17.59/5.15 % (210763)Instructions burned: 35 (million)
% 17.59/5.15 % (210763)------------------------------
% 17.59/5.15 % (210763)------------------------------
% 17.59/5.15 % (210723)Refutation found. Thanks to Tanya!
% 17.59/5.15 % SZS status Theorem for theBenchmark
% 17.59/5.15 % SZS output start Proof for theBenchmark
% See solution above
% 31.23/5.25 % (210723)------------------------------
% 31.23/5.25 % (210723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.23/5.25 % (210723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.23/5.25 % (210723)CaDiCaL version: 2.1.3
% 31.23/5.25 % (210723)Termination reason: Refutation
% 31.23/5.25 % (210723)Time elapsed: 3.044 s
% 31.23/5.25 % (210723)Peak memory usage: 226 MB
% 31.23/5.25 % (210723)Instructions burned: 4649 (million)
% 31.23/5.25 % (210723)------------------------------
% 31.23/5.25 % (210723)------------------------------
% 31.23/5.25 % (210684)Success in time 4.488 s
% 31.23/5.25 % Vampire exiting
%------------------------------------------------------------------------------