%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR177+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n004.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:01 AM UTC 2026
% Result : Theorem 42.77s 10.91s
% Output : Refutation 72.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 21
% Syntax : Number of formulae : 106 ( 44 unt; 2 def)
% Number of atoms : 519 ( 0 equ)
% Maximal formula atoms : 80 ( 4 avg)
% Number of connectives : 613 ( 200 ~; 185 |; 202 &)
% ( 23 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 21 ( 20 usr; 3 prp; 0-7 aty)
% Number of functors : 15 ( 15 usr; 13 con; 0-2 aty)
% Number of variables : 288 ( 0 sgn 283 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : p__d__subclass(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',predefinitionsA7) ).
fof(f2,axiom,
! [X0,X1,X2] :
( ( p__d__subclass(X0,X1)
& p__d__subclass(X1,X2) )
=> p__d__subclass(X0,X2) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',predefinitionsA24) ).
fof(f107,axiom,
p__d__partition3(c__Entity,c__Physical,c__Abstract),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA173) ).
fof(f110,axiom,
! [X0] :
( p__d__subclass(X0,c__Entity)
=> ? [X1] : p__d__instance(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA176) ).
fof(f233,axiom,
p__d__subclass(c__Process,c__Physical),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA324) ).
fof(f239,axiom,
p__d__subclass(c__Abstract,c__Entity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA330) ).
fof(f242,axiom,
p__d__subclass(c__Attribute,c__Abstract),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA333) ).
fof(f254,axiom,
p__d__subclass(c__InternalAttribute,c__Attribute),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA351) ).
fof(f1582,axiom,
p__d__subclass(c__BiologicalProcess,c__InternalChange),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA2309) ).
fof(f1585,axiom,
p__d__subclass(c__PhysiologicProcess,c__BiologicalProcess),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA2312) ).
fof(f1591,axiom,
p__d__subclass(c__OrganismProcess,c__PhysiologicProcess),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA2318) ).
fof(f1592,axiom,
p__d__subclass(c__Birth,c__OrganismProcess),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA2319) ).
fof(f1859,axiom,
p__d__subclass(c__InternalChange,c__Process),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA2644) ).
fof(f2662,axiom,
p__d__subclass(c__BiologicalAttribute,c__InternalAttribute),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA3659) ).
fof(f7433,conjecture,
! [X0] :
( ~ p__d__subclass(X0,c__Birth)
| ~ p__d__subclass(X0,c__BiologicalAttribute) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',negatedCommonSubclassEvent0106) ).
fof(f7434,negated_conjecture,
~ ! [X0] :
( ~ p__d__subclass(X0,c__Birth)
| ~ p__d__subclass(X0,c__BiologicalAttribute) ),
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(f7437,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(f7449,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f7450,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7449]) ).
fof(f7453,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f7454,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7453]) ).
fof(f7503,plain,
! [X0] :
( ? [X1] : p__d__instance(X1,X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(ennf_transformation,[],[f110]) ).
fof(f11600,plain,
? [X0] :
( p__d__subclass(X0,c__Birth)
& p__d__subclass(X0,c__BiologicalAttribute) ),
inference(ennf_transformation,[],[f7434]) ).
fof(f11657,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(f11658,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,[],[f11657]) ).
fof(f11659,plain,
! [X0,X1] :
( ( p__d__disjoint(X0,X1)
| ( p__d__instance(sK36(X0,X1),X0)
& p__d__instance(sK36(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,[sK36]),skolemize(X2,sK36(X0,X1))],[f11658]) ).
fof(f11660,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(f11661,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,[],[f11660]) ).
fof(f11665,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,[],[f7437]) ).
fof(f11666,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,[],[f11665]) ).
fof(f11721,plain,
! [X0] :
( p__d__instance(sK60(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK60]),skolemize(X1,sK60(X0))],[f7503]) ).
fof(f13399,plain,
( p__d__subclass(sK1263,c__Birth)
& p__d__subclass(sK1263,c__BiologicalAttribute) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1263]),skolemize(X0,sK1263)],[f11600]) ).
fof(f13400,plain,
! [X0] : p__d__subclass(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f13401,plain,
! [X2,X0,X1] :
( ~ p__d__subclass(X1,X2)
| ~ p__d__subclass(X0,X1)
| p__d__subclass(X0,X2) ),
inference(cnf_transformation,[],[f7450]) ).
fof(f13403,plain,
! [X2,X0,X1] :
( ~ p__d__instance(X0,X1)
| p__d__instance(X0,X2)
| ~ p__d__subclass(X1,X2) ),
inference(cnf_transformation,[],[f7454]) ).
fof(f13404,plain,
! [X3,X0,X1] :
( ~ p__d__disjoint(X0,X1)
| ~ p__d__instance(X3,X1)
| ~ p__d__instance(X3,X0) ),
inference(cnf_transformation,[],[f11659]) ).
fof(f13419,plain,
! [X2,X0,X1] :
( ~ p__d__partition3(X0,X1,X2)
| p__d__disjointDecomposition3(X0,X1,X2) ),
inference(cnf_transformation,[],[f11661]) ).
fof(f13490,plain,
! [X2,X0,X1] :
( ~ p__d__disjointDecomposition3(X0,X1,X2)
| p__d__disjoint(X1,X2) ),
inference(cnf_transformation,[],[f11666]) ).
fof(f13678,plain,
p__d__partition3(c__Entity,c__Physical,c__Abstract),
inference(cnf_transformation,[],[f107]) ).
fof(f13681,plain,
! [X0] :
( p__d__instance(sK60(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(cnf_transformation,[],[f11721]) ).
fof(f13843,plain,
p__d__subclass(c__Process,c__Physical),
inference(cnf_transformation,[],[f233]) ).
fof(f13852,plain,
p__d__subclass(c__Abstract,c__Entity),
inference(cnf_transformation,[],[f239]) ).
fof(f13855,plain,
p__d__subclass(c__Attribute,c__Abstract),
inference(cnf_transformation,[],[f242]) ).
fof(f13867,plain,
p__d__subclass(c__InternalAttribute,c__Attribute),
inference(cnf_transformation,[],[f254]) ).
fof(f15453,plain,
p__d__subclass(c__BiologicalProcess,c__InternalChange),
inference(cnf_transformation,[],[f1582]) ).
fof(f15457,plain,
p__d__subclass(c__PhysiologicProcess,c__BiologicalProcess),
inference(cnf_transformation,[],[f1585]) ).
fof(f15465,plain,
p__d__subclass(c__OrganismProcess,c__PhysiologicProcess),
inference(cnf_transformation,[],[f1591]) ).
fof(f15466,plain,
p__d__subclass(c__Birth,c__OrganismProcess),
inference(cnf_transformation,[],[f1592]) ).
fof(f15881,plain,
p__d__subclass(c__InternalChange,c__Process),
inference(cnf_transformation,[],[f1859]) ).
fof(f16930,plain,
p__d__subclass(c__BiologicalAttribute,c__InternalAttribute),
inference(cnf_transformation,[],[f2662]) ).
fof(f24206,plain,
p__d__subclass(sK1263,c__BiologicalAttribute),
inference(cnf_transformation,[],[f13399]) ).
fof(f24207,plain,
p__d__subclass(sK1263,c__Birth),
inference(cnf_transformation,[],[f13399]) ).
fof(f27601,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Abstract)
| p__d__subclass(X0,c__Entity) ),
inference(resolution,[],[f13401,f13852]) ).
fof(f27611,plain,
! [X0] :
( ~ p__d__subclass(X0,c__BiologicalAttribute)
| p__d__subclass(X0,c__InternalAttribute) ),
inference(resolution,[],[f13401,f16930]) ).
fof(f27618,plain,
! [X0] :
( ~ p__d__subclass(X0,sK1263)
| p__d__subclass(X0,c__Birth) ),
inference(resolution,[],[f13401,f24207]) ).
fof(f27634,plain,
p__d__subclass(sK1263,c__InternalAttribute),
inference(resolution,[],[f27611,f24206]) ).
fof(f27868,plain,
p__d__disjointDecomposition3(c__Entity,c__Physical,c__Abstract),
inference(resolution,[],[f13678,f13419]) ).
fof(f27869,plain,
p__d__disjoint(c__Physical,c__Abstract),
inference(resolution,[],[f27868,f13490]) ).
fof(f27870,plain,
! [X0] :
( ~ p__d__instance(X0,c__Abstract)
| ~ p__d__instance(X0,c__Physical) ),
inference(resolution,[],[f27869,f13404]) ).
fof(f27941,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Process)
| p__d__subclass(X0,c__Physical) ),
inference(resolution,[],[f13843,f13401]) ).
fof(f28003,plain,
! [X0] :
( ~ p__d__subclass(X0,c__InternalAttribute)
| p__d__subclass(X0,c__Attribute) ),
inference(resolution,[],[f13867,f13401]) ).
fof(f28032,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Attribute)
| p__d__subclass(X0,c__Abstract) ),
inference(resolution,[],[f13855,f13401]) ).
fof(f31030,plain,
! [X0,X1] :
( p__d__instance(sK60(X0),X1)
| ~ p__d__subclass(X0,c__Entity)
| ~ p__d__subclass(X0,X1) ),
inference(resolution,[],[f13681,f13403]) ).
fof(f31057,plain,
! [X2,X0,X1] :
( ~ p__d__subclass(X1,X2)
| ~ p__d__subclass(X0,X1)
| p__d__instance(sK60(X0),X2)
| ~ p__d__subclass(X0,c__Entity) ),
inference(resolution,[],[f31030,f13403]) ).
fof(f31170,plain,
! [X0] :
( p__d__instance(sK60(X0),c__OrganismProcess)
| ~ p__d__subclass(X0,c__Birth)
| ~ p__d__subclass(X0,c__Entity) ),
inference(resolution,[],[f31057,f15466]) ).
fof(f31337,plain,
! [X0] :
( p__d__instance(sK60(X0),c__BiologicalAttribute)
| ~ p__d__subclass(X0,sK1263)
| ~ p__d__subclass(X0,c__Entity) ),
inference(resolution,[],[f31057,f24206]) ).
fof(f31379,plain,
! [X0,X1] :
( p__d__instance(sK60(X0),X1)
| ~ p__d__subclass(X0,c__Entity)
| ~ p__d__subclass(X0,sK1263)
| ~ p__d__subclass(c__BiologicalAttribute,X1) ),
inference(resolution,[],[f31337,f13403]) ).
fof(f32873,plain,
! [X0,X1] :
( p__d__instance(sK60(X0),X1)
| ~ p__d__subclass(X0,c__Entity)
| ~ p__d__subclass(X0,c__Birth)
| ~ p__d__subclass(c__OrganismProcess,X1) ),
inference(resolution,[],[f31170,f13403]) ).
fof(f35178,plain,
p__d__subclass(c__BiologicalAttribute,c__Attribute),
inference(resolution,[],[f28003,f16930]) ).
fof(f35180,plain,
p__d__subclass(sK1263,c__Attribute),
inference(resolution,[],[f28003,f27634]) ).
fof(f35183,plain,
p__d__subclass(c__BiologicalAttribute,c__Abstract),
inference(resolution,[],[f35178,f28032]) ).
fof(f35206,plain,
p__d__subclass(sK1263,c__Abstract),
inference(resolution,[],[f35180,f28032]) ).
fof(f35220,plain,
p__d__subclass(sK1263,c__Entity),
inference(resolution,[],[f35206,f27601]) ).
fof(f35235,plain,
! [X0] :
( ~ p__d__subclass(X0,sK1263)
| p__d__subclass(X0,c__Entity) ),
inference(resolution,[],[f35220,f13401]) ).
fof(f37644,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Entity)
| ~ p__d__subclass(X0,sK1263)
| ~ p__d__subclass(c__BiologicalAttribute,c__Abstract)
| ~ p__d__instance(sK60(X0),c__Physical) ),
inference(resolution,[],[f31379,f27870]) ).
fof(f37719,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Entity)
| ~ p__d__subclass(X0,sK1263)
| ~ p__d__instance(sK60(X0),c__Physical) ),
inference(forward_subsumption_resolution,[],[f37644,f35183]) ).
fof(f37932,plain,
! [X0] :
( ~ p__d__instance(sK60(X0),c__Physical)
| ~ p__d__subclass(X0,sK1263) ),
inference(forward_subsumption_resolution,[],[f37719,f35235]) ).
fof(f38751,definition,
( spl1264_1558
<=> ! [X0] : ~ p__d__subclass(X0,sK1263) ),
introduced(definition,[new_symbols(definition,[spl1264_1558])],[avatar_definition]) ).
fof(f38752,plain,
( ! [X0] : ~ p__d__subclass(X0,sK1263)
| ~ spl1264_1558 ),
inference(avatar_component_clause,[],[f38751]) ).
fof(f41599,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Entity)
| ~ p__d__subclass(X0,c__Birth)
| ~ p__d__subclass(c__OrganismProcess,c__Physical)
| ~ p__d__subclass(X0,sK1263) ),
inference(resolution,[],[f32873,f37932]) ).
fof(f41936,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Birth)
| ~ p__d__subclass(c__OrganismProcess,c__Physical)
| ~ p__d__subclass(X0,sK1263) ),
inference(forward_subsumption_resolution,[],[f41599,f35235]) ).
fof(f41978,definition,
( spl1264_2016
<=> p__d__subclass(c__OrganismProcess,c__Physical) ),
introduced(definition,[new_symbols(definition,[spl1264_2016])],[avatar_definition]) ).
fof(f41980,plain,
( ~ p__d__subclass(c__OrganismProcess,c__Physical)
| spl1264_2016 ),
inference(avatar_component_clause,[],[f41978]) ).
fof(f41985,plain,
! [X0] :
( ~ p__d__subclass(c__OrganismProcess,c__Physical)
| ~ p__d__subclass(X0,sK1263) ),
inference(forward_subsumption_resolution,[],[f41936,f27618]) ).
fof(f41986,plain,
( spl1264_1558
| ~ spl1264_2016 ),
inference(avatar_split_clause,[],[f41985,f41978,f38751]) ).
fof(f45303,plain,
! [X0] :
( ~ p__d__subclass(X0,c__InternalChange)
| p__d__subclass(X0,c__Process) ),
inference(resolution,[],[f15881,f13401]) ).
fof(f45314,plain,
p__d__subclass(c__BiologicalProcess,c__Process),
inference(resolution,[],[f45303,f15453]) ).
fof(f45333,plain,
p__d__subclass(c__BiologicalProcess,c__Physical),
inference(resolution,[],[f45314,f27941]) ).
fof(f48949,plain,
! [X0] :
( ~ p__d__subclass(X0,c__BiologicalProcess)
| p__d__subclass(X0,c__Physical) ),
inference(resolution,[],[f45333,f13401]) ).
fof(f66838,plain,
! [X0] :
( ~ p__d__subclass(X0,c__PhysiologicProcess)
| p__d__subclass(X0,c__BiologicalProcess) ),
inference(resolution,[],[f15457,f13401]) ).
fof(f123965,plain,
p__d__subclass(c__OrganismProcess,c__BiologicalProcess),
inference(resolution,[],[f15465,f66838]) ).
fof(f123978,plain,
p__d__subclass(c__OrganismProcess,c__Physical),
inference(resolution,[],[f123965,f48949]) ).
fof(f123995,plain,
( $false
| spl1264_2016 ),
inference(forward_subsumption_resolution,[],[f123978,f41980]) ).
fof(f123996,plain,
spl1264_2016,
inference(avatar_contradiction_clause,[],[f123995]) ).
fof(f124006,plain,
( $false
| ~ spl1264_1558 ),
inference(resolution,[],[f38752,f13400]) ).
fof(f124007,plain,
~ spl1264_1558,
inference(avatar_contradiction_clause,[],[f124006]) ).
cnf(s1073,plain,
( spl1264_1558
| ~ spl1264_2016 ),
inference(sat_conversion,[],[f41986]) ).
cnf(s6625,plain,
spl1264_2016,
inference(sat_conversion,[],[f123996]) ).
cnf(s6627,plain,
~ spl1264_1558,
inference(sat_conversion,[],[f124007]) ).
cnf(s6646,plain,
$false,
inference(rat,[],[s1073,s6625,s6627]) ).
fof(f124008,plain,
$false,
inference(avatar_sat_refutation,[],[s6646]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR177+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n004.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:40:54 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.70/2.62 % (905064)Detected formulas, will run a generic FOF schedule.
% 12.70/2.62 % (905071)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=2642476975:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 12.70/2.62 % (905074)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1836309420:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 12.70/2.62 % (905073)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1922689832:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 12.70/2.62 % (905070)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=4250377277:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 12.70/2.62 % (905075)dis-21_1_sil=8000:lcm=predicate:random_seed=2418231116: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)
% 12.70/2.62 % (905069)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=3518960126:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 12.70/2.62 % (905072)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1903550761:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 12.70/2.62 % (905072)Refutation not found, incomplete strategy
% 12.70/2.62 % (905072)------------------------------
% 12.70/2.62 % (905072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.70/2.62 % (905072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.70/2.62 % (905072)CaDiCaL version: 2.1.3
% 12.70/2.62 % (905072)Termination reason: Refutation not found, incomplete strategy
% 12.70/2.62 % (905072)Time elapsed: 0.017 s
% 12.70/2.62 % (905072)Peak memory usage: 94 MB
% 12.70/2.62 % (905072)Instructions burned: 24 (million)
% 12.70/2.62 % (905073)Instruction limit reached!
% 12.70/2.62 % (905073)------------------------------
% 12.70/2.62 % (905073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.70/2.62 % (905073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.70/2.62 % (905073)CaDiCaL version: 2.1.3
% 12.70/2.62 % (905073)Termination reason: Instruction limit
% 12.70/2.62 % (905073)Termination phase: Saturation
% 12.70/2.62 % (905073)Time elapsed: 0.061 s
% 12.70/2.62 % (905073)Peak memory usage: 93 MB
% 12.70/2.62 % (905073)Instructions burned: 119 (million)
% 12.70/2.62 % (905075)Instruction limit reached!
% 12.70/2.62 % (905075)------------------------------
% 12.70/2.62 % (905075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.70/2.62 % (905075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.70/2.62 % (905075)CaDiCaL version: 2.1.3
% 12.70/2.62 % (905075)Termination reason: Instruction limit
% 12.70/2.62 % (905075)Termination phase: Saturation
% 12.70/2.62 % (905075)Time elapsed: 0.072 s
% 12.70/2.62 % (905075)Peak memory usage: 95 MB
% 12.70/2.62 % (905075)Instructions burned: 129 (million)
% 12.70/2.62 % (905074)Instruction limit reached!
% 12.70/2.62 % (905074)------------------------------
% 12.70/2.62 % (905074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.70/2.62 % (905074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.70/2.62 % (905074)CaDiCaL version: 2.1.3
% 12.70/2.62 % (905074)Termination reason: Instruction limit
% 12.70/2.62 % (905074)Termination phase: Preprocessing 3
% 12.70/2.62 % (905074)Time elapsed: 0.090 s
% 12.70/2.62 % (905074)Peak memory usage: 94 MB
% 12.70/2.62 % (905074)Instructions burned: 140 (million)
% 12.70/2.62 % (905083)lrs+10_1_sil=8000:sp=occurrence:random_seed=1134821780:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 12.70/2.62 % (905084)lrs+10_1_sil=32000:urr=on:br=off:random_seed=280139561:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 12.70/2.62 % (905085)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3815049941:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 12.70/2.62 % (905085)Refutation not found, incomplete strategy
% 12.70/2.62 % (905085)------------------------------
% 12.70/2.62 % (905085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.70/2.62 % (905084)Refutation not found, incomplete strategy
% 12.70/2.62 % (905084)------------------------------
% 20.50/3.76 % (905084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.50/3.76 % (905085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.50/3.76 % (905084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.50/3.76 % (905085)CaDiCaL version: 2.1.3
% 20.50/3.76 % (905085)Termination reason: Refutation not found, incomplete strategy
% 20.50/3.76 % (905085)Time elapsed: 0.016 s
% 20.50/3.76 % (905084)CaDiCaL version: 2.1.3
% 20.50/3.76 % (905085)Peak memory usage: 94 MB
% 20.50/3.76 % (905084)Termination reason: Refutation not found, incomplete strategy
% 20.50/3.76 % (905084)Time elapsed: 0.033 s
% 20.50/3.76 % (905085)Instructions burned: 20 (million)
% 20.50/3.76 % (905084)Peak memory usage: 94 MB
% 20.50/3.76 % (905084)Instructions burned: 61 (million)
% 20.50/3.76 % (905072)------------------------------
% 20.50/3.76 % (905072)------------------------------
% 20.50/3.76 % (905083)Instruction limit reached!
% 20.50/3.76 % (905083)------------------------------
% 20.50/3.76 % (905083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.50/3.76 % (905083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.50/3.76 % (905083)CaDiCaL version: 2.1.3
% 20.50/3.76 % (905083)Termination reason: Instruction limit
% 20.50/3.76 % (905083)Termination phase: Saturation
% 20.50/3.76 % (905083)Time elapsed: 0.169 s
% 20.50/3.76 % (905083)Peak memory usage: 97 MB
% 20.50/3.76 % (905083)Instructions burned: 285 (million)
% 20.50/3.76 % (905089)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=1511392801:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 20.50/3.76 % (905090)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2460036279:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 20.50/3.76 % (905084)------------------------------
% 20.50/3.76 % (905084)------------------------------
% 20.50/3.76 % (905085)------------------------------
% 20.50/3.76 % (905085)------------------------------
% 20.50/3.76 % (905090)Instruction limit reached!
% 20.50/3.76 % (905090)------------------------------
% 20.50/3.76 % (905090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.50/3.76 % (905090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.50/3.76 % (905090)CaDiCaL version: 2.1.3
% 20.50/3.76 % (905090)Termination reason: Instruction limit
% 20.50/3.76 % (905090)Termination phase: Saturation
% 20.50/3.76 % (905090)Time elapsed: 0.074 s
% 20.50/3.76 % (905090)Peak memory usage: 94 MB
% 20.50/3.76 % (905090)Instructions burned: 297 (million)
% 20.50/3.76 % (905089)Instruction limit reached!
% 20.50/3.76 % (905089)------------------------------
% 20.50/3.76 % (905089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.50/3.76 % (905089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.50/3.76 % (905089)CaDiCaL version: 2.1.3
% 20.50/3.76 % (905089)Termination reason: Instruction limit
% 20.50/3.76 % (905089)Termination phase: Saturation
% 20.50/3.76 % (905089)Time elapsed: 0.138 s
% 20.50/3.76 % (905089)Peak memory usage: 98 MB
% 20.50/3.76 % (905089)Instructions burned: 249 (million)
% 20.50/3.76 % (905094)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=387626367:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 20.50/3.76 % (905093)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2749109323:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 20.50/3.76 % (905095)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3274749099:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 20.50/3.76 % (905095)Instruction limit reached!
% 20.50/3.76 % (905095)------------------------------
% 20.50/3.76 % (905095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.50/3.76 % (905095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.50/3.76 % (905095)CaDiCaL version: 2.1.3
% 20.50/3.76 % (905095)Termination reason: Instruction limit
% 20.50/3.76 % (905095)Termination phase: Property scanning
% 20.50/3.76 % (905095)Time elapsed: 0.044 s
% 20.50/3.76 % (905095)Peak memory usage: 96 MB
% 20.50/3.76 % (905095)Instructions burned: 129 (million)
% 20.50/3.76 % (905096)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1408101892:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 20.50/3.76 % (905094)Instruction limit reached!
% 20.50/3.76 % (905094)------------------------------
% 46.34/7.30 % (905094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.34/7.30 % (905094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.34/7.30 % (905094)CaDiCaL version: 2.1.3
% 46.34/7.30 % (905094)Termination reason: Instruction limit
% 46.34/7.30 % (905094)Termination phase: Saturation
% 46.34/7.30 % (905094)Time elapsed: 0.064 s
% 46.34/7.30 % (905094)Peak memory usage: 94 MB
% 46.34/7.30 % (905094)Instructions burned: 115 (million)
% 46.34/7.30 % (905096)Instruction limit reached!
% 46.34/7.30 % (905096)------------------------------
% 46.34/7.30 % (905096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.34/7.30 % (905096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.34/7.30 % (905096)CaDiCaL version: 2.1.3
% 46.34/7.30 % (905096)Termination reason: Instruction limit
% 46.34/7.30 % (905096)Termination phase: Equality resolution with deletion
% 46.34/7.30 % (905096)Time elapsed: 0.061 s
% 46.34/7.30 % (905096)Peak memory usage: 91 MB
% 46.34/7.30 % (905096)Instructions burned: 116 (million)
% 46.34/7.30 % (905100)lrs+10_1_sil=8000:sp=occurrence:random_seed=648684740:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 46.34/7.30 % (905102)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2079313547:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 46.34/7.30 % (905102)Refutation not found, incomplete strategy
% 46.34/7.30 % (905102)------------------------------
% 46.34/7.30 % (905102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.34/7.30 % (905102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.34/7.30 % (905102)CaDiCaL version: 2.1.3
% 46.34/7.30 % (905102)Termination reason: Refutation not found, incomplete strategy
% 46.34/7.30 % (905102)Time elapsed: 0.017 s
% 46.34/7.30 % (905102)Peak memory usage: 93 MB
% 46.34/7.30 % (905102)Instructions burned: 20 (million)
% 46.34/7.30 % (905103)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1528981660:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 46.34/7.30 % (905102)------------------------------
% 46.34/7.30 % (905102)------------------------------
% 46.34/7.30 % (905107)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=693072949:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2985 on theBenchmark for (2985ds/134Mi)
% 46.34/7.30 % (905107)Refutation not found, incomplete strategy
% 46.34/7.30 % (905107)------------------------------
% 46.34/7.30 % (905107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.34/7.30 % (905107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.34/7.30 % (905107)CaDiCaL version: 2.1.3
% 46.34/7.30 % (905107)Termination reason: Refutation not found, incomplete strategy
% 46.34/7.30 % (905107)Time elapsed: 0.018 s
% 46.34/7.30 % (905107)Peak memory usage: 94 MB
% 46.34/7.30 % (905107)Instructions burned: 26 (million)
% 46.34/7.30 % (905100)Instruction limit reached!
% 46.34/7.30 % (905100)------------------------------
% 46.34/7.30 % (905100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.34/7.30 % (905100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.34/7.30 % (905100)CaDiCaL version: 2.1.3
% 46.34/7.30 % (905100)Termination reason: Instruction limit
% 46.34/7.30 % (905100)Termination phase: Saturation
% 46.34/7.30 % (905100)Time elapsed: 0.518 s
% 46.34/7.30 % (905100)Peak memory usage: 111 MB
% 46.34/7.30 % (905100)Instructions burned: 909 (million)
% 46.34/7.30 % (905109)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1910661535:st=8:i=592:sd=3:ep=RST:ss=axioms_2983 on theBenchmark for (2983ds/592Mi)
% 46.34/7.30 % (905107)------------------------------
% 46.34/7.30 % (905107)------------------------------
% 46.34/7.30 % (905109)Refutation not found, incomplete strategy
% 46.34/7.30 % (905109)------------------------------
% 46.34/7.30 % (905109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.34/7.30 % (905109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.34/7.30 % (905109)CaDiCaL version: 2.1.3
% 46.34/7.30 % (905109)Termination reason: Refutation not found, incomplete strategy
% 46.34/7.30 % (905109)Time elapsed: 0.068 s
% 46.34/7.30 % (905109)Peak memory usage: 95 MB
% 46.34/7.30 % (905109)Instructions burned: 111 (million)
% 46.34/7.30 % (905111)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2276111940:st=3:i=13193:sd=3:ss=axioms_2981 on theBenchmark for (2981ds/13193Mi)
% 68.46/10.45 % (905109)------------------------------
% 68.46/10.45 % (905109)------------------------------
% 68.46/10.45 % (905113)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=1852503725:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/125Mi)
% 68.46/10.45 % (905113)Instruction limit reached!
% 68.46/10.45 % (905113)------------------------------
% 68.46/10.45 % (905113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.46/10.45 % (905113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.46/10.45 % (905113)CaDiCaL version: 2.1.3
% 68.46/10.45 % (905113)Termination reason: Instruction limit
% 68.46/10.45 % (905113)Termination phase: Preprocessing 3
% 68.46/10.45 % (905113)Time elapsed: 0.081 s
% 68.46/10.45 % (905113)Peak memory usage: 93 MB
% 68.46/10.45 % (905113)Instructions burned: 126 (million)
% 68.46/10.45 % (905093)Instruction limit reached!
% 68.46/10.45 % (905093)------------------------------
% 68.46/10.45 % (905093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.46/10.45 % (905093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.46/10.45 % (905093)CaDiCaL version: 2.1.3
% 68.46/10.45 % (905093)Termination reason: Instruction limit
% 68.46/10.45 % (905093)Termination phase: Saturation
% 68.46/10.45 % (905093)Time elapsed: 1.433 s
% 68.46/10.45 % (905093)Peak memory usage: 179 MB
% 68.46/10.45 % (905093)Instructions burned: 2351 (million)
% 68.46/10.45 % (905115)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=693469119:i=134:gtgl=5:slsql=off:gtg=exists_sym_2977 on theBenchmark for (2977ds/134Mi)
% 68.46/10.45 % (905115)Instruction limit reached!
% 68.46/10.45 % (905115)------------------------------
% 68.46/10.45 % (905115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.46/10.45 % (905115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.46/10.45 % (905115)CaDiCaL version: 2.1.3
% 68.46/10.45 % (905115)Termination reason: Instruction limit
% 68.46/10.45 % (905115)Termination phase: Preprocessing 2
% 68.46/10.45 % (905115)Time elapsed: 0.069 s
% 68.46/10.45 % (905115)Peak memory usage: 92 MB
% 68.46/10.45 % (905115)Instructions burned: 135 (million)
% 68.46/10.45 % (905116)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3947250050:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/141Mi)
% 68.46/10.45 % (905116)Refutation not found, incomplete strategy
% 68.46/10.45 % (905116)------------------------------
% 68.46/10.45 % (905116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.46/10.45 % (905116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.46/10.45 % (905116)CaDiCaL version: 2.1.3
% 68.46/10.45 % (905116)Termination reason: Refutation not found, incomplete strategy
% 68.46/10.45 % (905116)Time elapsed: 0.018 s
% 68.46/10.45 % (905116)Peak memory usage: 94 MB
% 68.46/10.45 % (905116)Instructions burned: 24 (million)
% 68.46/10.45 % (905118)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2853659452:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2975 on theBenchmark for (2975ds/431Mi)
% 68.46/10.45 % (905118)Refutation not found, incomplete strategy
% 68.46/10.45 % (905118)------------------------------
% 68.46/10.45 % (905118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.46/10.45 % (905118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.46/10.45 % (905118)CaDiCaL version: 2.1.3
% 68.46/10.45 % (905118)Termination reason: Refutation not found, incomplete strategy
% 68.46/10.45 % (905118)Time elapsed: 0.016 s
% 68.46/10.45 % (905118)Peak memory usage: 94 MB
% 68.46/10.45 % (905118)Instructions burned: 20 (million)
% 68.46/10.45 % (905116)------------------------------
% 68.46/10.45 % (905116)------------------------------
% 68.46/10.45 % (905118)------------------------------
% 68.46/10.45 % (905118)------------------------------
% 68.46/10.45 % (905121)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=2219926790:i=6060:aac=none:ins=25_2972 on theBenchmark for (2972ds/6060Mi)
% 68.46/10.45 % (905122)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=3766575541:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2971 on theBenchmark for (2971ds/150Mi)
% 68.46/10.45 % (905122)Instruction limit reached!
% 42.77/10.91 % (905122)------------------------------
% 42.77/10.91 % (905122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.77/10.91 % (905122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.77/10.91 % (905122)CaDiCaL version: 2.1.3
% 42.77/10.91 % (905122)Termination reason: Instruction limit
% 42.77/10.91 % (905122)Termination phase: Property scanning
% 42.77/10.91 % (905122)Time elapsed: 0.085 s
% 42.77/10.91 % (905122)Peak memory usage: 96 MB
% 42.77/10.91 % (905122)Instructions burned: 151 (million)
% 42.77/10.91 % (905125)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3170608552:i=14155:bd=all_2969 on theBenchmark for (2969ds/14155Mi)
% 42.77/10.91 % (905103)Instruction limit reached!
% 42.77/10.91 % (905103)------------------------------
% 42.77/10.91 % (905103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.77/10.91 % (905103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.77/10.91 % (905103)CaDiCaL version: 2.1.3
% 42.77/10.91 % (905103)Termination reason: Instruction limit
% 42.77/10.91 % (905103)Termination phase: Saturation
% 42.77/10.91 % (905103)Time elapsed: 3.368 s
% 42.77/10.91 % (905103)Peak memory usage: 225 MB
% 42.77/10.91 % (905103)Instructions burned: 5203 (million)
% 42.77/10.91 % (905127)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=289057694:i=667:av=off:fsr=off_2954 on theBenchmark for (2954ds/667Mi)
% 42.77/10.91 % (905127)Instruction limit reached!
% 42.77/10.91 % (905127)------------------------------
% 42.77/10.91 % (905127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.77/10.91 % (905127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.77/10.91 % (905127)CaDiCaL version: 2.1.3
% 42.77/10.91 % (905127)Termination reason: Instruction limit
% 42.77/10.91 % (905127)Termination phase: Saturation
% 42.77/10.91 % (905127)Time elapsed: 0.338 s
% 42.77/10.91 % (905127)Peak memory usage: 103 MB
% 42.77/10.91 % (905127)Instructions burned: 668 (million)
% 42.77/10.91 % (905129)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=2017749934:s2a=on:i=185:s2at=1.8:fdi=4_2949 on theBenchmark for (2949ds/185Mi)
% 42.77/10.91 % (905129)Instruction limit reached!
% 42.77/10.91 % (905129)------------------------------
% 42.77/10.91 % (905129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.77/10.91 % (905129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.77/10.91 % (905129)CaDiCaL version: 2.1.3
% 42.77/10.91 % (905129)Termination reason: Instruction limit
% 42.77/10.91 % (905129)Termination phase: Property scanning
% 42.77/10.91 % (905129)Time elapsed: 0.117 s
% 42.77/10.91 % (905129)Peak memory usage: 96 MB
% 42.77/10.91 % (905129)Instructions burned: 187 (million)
% 42.77/10.91 % (905131)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2427841383:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2946 on theBenchmark for (2946ds/193Mi)
% 42.77/10.91 % (905131)Instruction limit reached!
% 42.77/10.91 % (905131)------------------------------
% 42.77/10.91 % (905131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.77/10.91 % (905131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.77/10.91 % (905131)CaDiCaL version: 2.1.3
% 42.77/10.91 % (905131)Termination reason: Instruction limit
% 42.77/10.91 % (905131)Termination phase: Saturation
% 42.77/10.91 % (905131)Time elapsed: 0.108 s
% 42.77/10.91 % (905131)Peak memory usage: 95 MB
% 42.77/10.91 % (905131)Instructions burned: 193 (million)
% 42.77/10.91 % (905133)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=447006625:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2944 on theBenchmark for (2944ds/4850Mi)
% 42.77/10.91 % (905121)Instruction limit reached!
% 42.77/10.91 % (905121)------------------------------
% 42.77/10.91 % (905121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.77/10.91 % (905121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.77/10.91 % (905121)CaDiCaL version: 2.1.3
% 42.77/10.91 % (905121)Termination reason: Instruction limit
% 42.77/10.91 % (905121)Termination phase: Saturation
% 42.77/10.91 % (905121)Time elapsed: 3.553 s
% 42.77/10.91 % (905121)Peak memory usage: 245 MB
% 42.77/10.91 % (905121)Instructions burned: 6061 (million)
% 42.77/10.91 % (905135)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3820486008:i=12111:sd=1:ss=included_2935 on theBenchmark for (2935ds/12111Mi)
% 42.77/10.91 % (905135)Refutation not found, incomplete strategy
% 42.77/10.91 % (905135)------------------------------
% 42.77/10.91 % (905135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.77/10.91 % (905135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.77/10.91 % (905135)CaDiCaL version: 2.1.3
% 42.77/10.91 % (905135)Termination reason: Refutation not found, incomplete strategy
% 42.77/10.91 % (905135)Time elapsed: 0.667 s
% 42.77/10.91 % (905135)Peak memory usage: 144 MB
% 42.77/10.91 % (905135)Instructions burned: 1030 (million)
% 42.77/10.91 % (905135)------------------------------
% 42.77/10.91 % (905135)------------------------------
% 42.77/10.91 % (905137)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2819518480:i=319:kws=precedence:fsr=off_2924 on theBenchmark for (2924ds/319Mi)
% 42.77/10.91 % (905137)Instruction limit reached!
% 42.77/10.91 % (905137)------------------------------
% 42.77/10.91 % (905137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.77/10.91 % (905137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.77/10.91 % (905137)CaDiCaL version: 2.1.3
% 42.77/10.91 % (905137)Termination reason: Instruction limit
% 42.77/10.91 % (905137)Termination phase: Saturation
% 42.77/10.91 % (905137)Time elapsed: 0.157 s
% 42.77/10.91 % (905137)Peak memory usage: 101 MB
% 42.77/10.91 % (905137)Instructions burned: 320 (million)
% 42.77/10.91 % (905139)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1890392433:i=2064:ep=RST_2921 on theBenchmark for (2921ds/2064Mi)
% 42.77/10.91 % (905133)Instruction limit reached!
% 42.77/10.91 % (905133)------------------------------
% 42.77/10.91 % (905133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.77/10.91 % (905133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.77/10.91 % (905133)CaDiCaL version: 2.1.3
% 42.77/10.91 % (905133)Termination reason: Instruction limit
% 42.77/10.91 % (905133)Termination phase: Saturation
% 42.77/10.91 % (905133)Time elapsed: 2.300 s
% 42.77/10.91 % (905133)Peak memory usage: 110 MB
% 42.77/10.91 % (905133)Instructions burned: 4851 (million)
% 42.77/10.91 % (905141)dis-1011_128_sil=32000:random_seed=1492586888:i=3706:ep=RST:av=off_2920 on theBenchmark for (2920ds/3706Mi)
% 42.77/10.91 % (905139)Refutation not found, incomplete strategy
% 42.77/10.91 % (905139)------------------------------
% 42.77/10.91 % (905139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.77/10.91 % (905139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.77/10.91 % (905139)CaDiCaL version: 2.1.3
% 42.77/10.91 % (905139)Termination reason: Refutation not found, incomplete strategy
% 42.77/10.91 % (905139)Time elapsed: 0.210 s
% 42.77/10.91 % (905139)Peak memory usage: 105 MB
% 42.77/10.91 % (905139)Instructions burned: 413 (million)
% 42.77/10.91 % (905139)------------------------------
% 42.77/10.91 % (905139)------------------------------
% 42.77/10.91 % (905143)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=212665270:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2915 on theBenchmark for (2915ds/757Mi)
% 42.77/10.91 % (905143)Instruction limit reached!
% 42.77/10.91 % (905143)------------------------------
% 42.77/10.91 % (905143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.77/10.91 % (905143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.77/10.91 % (905143)CaDiCaL version: 2.1.3
% 42.77/10.91 % (905143)Termination reason: Instruction limit
% 42.77/10.91 % (905143)Termination phase: Saturation
% 42.77/10.91 % (905143)Time elapsed: 0.407 s
% 42.77/10.91 % (905143)Peak memory usage: 107 MB
% 42.77/10.91 % (905143)Instructions burned: 757 (million)
% 42.77/10.91 % (905145)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4025627501:i=13913:ss=axioms:sgt=8_2910 on theBenchmark for (2910ds/13913Mi)
% 42.77/10.91 % (905141)Instruction limit reached!
% 42.77/10.91 % (905141)------------------------------
% 42.77/10.91 % (905141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.77/10.91 % (905141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.77/10.91 % (905141)CaDiCaL version: 2.1.3
% 42.77/10.91 % (905141)Termination reason: Instruction limit
% 42.77/10.91 % (905141)Termination phase: Saturation
% 42.77/10.91 % (905141)Time elapsed: 1.673 s
% 42.77/10.91 % (905141)Peak memory usage: 109 MB
% 42.77/10.91 % (905141)Instructions burned: 3707 (million)
% 42.77/10.91 % (905111)Instruction limit reached!
% 42.77/10.91 % (905111)------------------------------
% 42.77/10.91 % (905111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.77/10.91 % (905111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.77/10.91 % (905111)CaDiCaL version: 2.1.3
% 42.77/10.91 % (905111)Termination reason: Instruction limit
% 42.77/10.91 % (905111)Termination phase: Saturation
% 42.77/10.91 % (905111)Time elapsed: 7.953 s
% 42.77/10.91 % (905111)Peak memory usage: 255 MB
% 42.77/10.91 % (905111)Instructions burned: 13193 (million)
% 42.77/10.91 % (905147)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3102239977:i=9925:aac=none_2902 on theBenchmark for (2902ds/9925Mi)
% 42.77/10.91 % (905069)First to succeed.
% 42.77/10.91 % (905069)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-905064"
% 42.77/10.91 % (905149)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3146872440:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2900 on theBenchmark for (2900ds/2479Mi)
% 42.77/10.91 % (905149)Refutation not found, incomplete strategy
% 42.77/10.91 % (905149)------------------------------
% 42.77/10.91 % (905149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.77/10.91 % (905149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.77/10.91 % (905149)CaDiCaL version: 2.1.3
% 42.77/10.91 % (905149)Termination reason: Refutation not found, incomplete strategy
% 42.77/10.91 % (905149)Time elapsed: 0.029 s
% 42.77/10.91 % (905149)Peak memory usage: 94 MB
% 42.77/10.91 % (905149)Instructions burned: 42 (million)
% 42.77/10.91 % (905069)Refutation found. Thanks to Tanya!
% 42.77/10.91 % SZS status Theorem for theBenchmark
% 42.77/10.91 % SZS output start Proof for theBenchmark
% See solution above
% 72.20/11.11 % (905069)------------------------------
% 72.20/11.11 % (905069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.20/11.11 % (905069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.20/11.11 % (905069)CaDiCaL version: 2.1.3
% 72.20/11.11 % (905069)Termination reason: Refutation
% 72.20/11.11 % (905069)Time elapsed: 9.734 s
% 72.20/11.11 % (905069)Peak memory usage: 299 MB
% 72.20/11.11 % (905069)Instructions burned: 30827 (million)
% 72.20/11.11 % (905069)------------------------------
% 72.20/11.11 % (905069)------------------------------
% 72.20/11.11 % (905064)Success in time 10.238 s
% 72.20/11.11 % Vampire exiting
%------------------------------------------------------------------------------