%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR227+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 22.01s 3.96s
% Output : Refutation 22.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 21
% Syntax : Number of formulae : 115 ( 34 unt; 5 def)
% Number of atoms : 562 ( 17 equ)
% Maximal formula atoms : 80 ( 4 avg)
% Number of connectives : 664 ( 217 ~; 214 |; 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 : 10 ( 10 usr; 8 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(f110,axiom,
! [X0] :
( p__d__subclass(X0,c__Entity)
=> ? [X1] : p__d__instance(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA176) ).
fof(f112,axiom,
p__d__subclass(c__Physical,c__Entity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA178) ).
fof(f113,axiom,
p__d__partition3(c__Physical,c__Object,c__Process),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA179) ).
fof(f115,axiom,
p__d__subclass(c__Object,c__Physical),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA181) ).
fof(f233,axiom,
p__d__subclass(c__Process,c__Physical),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA324) ).
fof(f1665,axiom,
p__d__subclass(c__QuantityChange,c__InternalChange),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2400) ).
fof(f1666,axiom,
p__d__partition3(c__QuantityChange,c__Increasing,c__Decreasing),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2401) ).
fof(f1667,axiom,
p__d__subclass(c__Increasing,c__QuantityChange),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2402) ).
fof(f1670,axiom,
p__d__subclass(c__Decreasing,c__QuantityChange),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2408) ).
fof(f1859,axiom,
p__d__subclass(c__InternalChange,c__Process),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2644) ).
fof(f7433,conjecture,
? [X0,X1] :
( p__d__instance(X0,c__QuantityChange)
& ~ p__d__instance(X1,c__Process)
& X0 != X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antonymPattern31406) ).
fof(f7434,negated_conjecture,
~ ? [X0,X1] :
( p__d__instance(X0,c__QuantityChange)
& ~ p__d__instance(X1,c__Process)
& 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(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,X1] :
( ~ p__d__instance(X0,c__QuantityChange)
| p__d__instance(X1,c__Process)
| X0 = X1 ),
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(f13400,plain,
! [X2,X0,X1] :
( ~ p__d__subclass(X1,X2)
| ~ p__d__subclass(X0,X1)
| p__d__subclass(X0,X2) ),
inference(cnf_transformation,[],[f7450]) ).
fof(f13402,plain,
! [X2,X0,X1] :
( ~ p__d__instance(X0,X1)
| p__d__instance(X0,X2)
| ~ p__d__subclass(X1,X2) ),
inference(cnf_transformation,[],[f7454]) ).
fof(f13403,plain,
! [X3,X0,X1] :
( ~ p__d__disjoint(X0,X1)
| ~ p__d__instance(X3,X1)
| ~ p__d__instance(X3,X0) ),
inference(cnf_transformation,[],[f11659]) ).
fof(f13418,plain,
! [X2,X0,X1] :
( ~ p__d__partition3(X0,X1,X2)
| p__d__disjointDecomposition3(X0,X1,X2) ),
inference(cnf_transformation,[],[f11661]) ).
fof(f13489,plain,
! [X2,X0,X1] :
( ~ p__d__disjointDecomposition3(X0,X1,X2)
| p__d__disjoint(X1,X2) ),
inference(cnf_transformation,[],[f11666]) ).
fof(f13680,plain,
! [X0] :
( p__d__instance(sK60(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(cnf_transformation,[],[f11721]) ).
fof(f13683,plain,
p__d__subclass(c__Physical,c__Entity),
inference(cnf_transformation,[],[f112]) ).
fof(f13684,plain,
p__d__partition3(c__Physical,c__Object,c__Process),
inference(cnf_transformation,[],[f113]) ).
fof(f13689,plain,
p__d__subclass(c__Object,c__Physical),
inference(cnf_transformation,[],[f115]) ).
fof(f13842,plain,
p__d__subclass(c__Process,c__Physical),
inference(cnf_transformation,[],[f233]) ).
fof(f15566,plain,
p__d__subclass(c__QuantityChange,c__InternalChange),
inference(cnf_transformation,[],[f1665]) ).
fof(f15567,plain,
p__d__partition3(c__QuantityChange,c__Increasing,c__Decreasing),
inference(cnf_transformation,[],[f1666]) ).
fof(f15568,plain,
p__d__subclass(c__Increasing,c__QuantityChange),
inference(cnf_transformation,[],[f1667]) ).
fof(f15571,plain,
p__d__subclass(c__Decreasing,c__QuantityChange),
inference(cnf_transformation,[],[f1670]) ).
fof(f15880,plain,
p__d__subclass(c__InternalChange,c__Process),
inference(cnf_transformation,[],[f1859]) ).
fof(f24205,plain,
! [X0,X1] :
( ~ p__d__instance(X0,c__QuantityChange)
| p__d__instance(X1,c__Process)
| X0 = X1 ),
inference(cnf_transformation,[],[f11600]) ).
fof(f27610,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Physical)
| p__d__subclass(X0,c__Entity) ),
inference(resolution,[],[f13683,f13400]) ).
fof(f27622,plain,
p__d__subclass(c__Object,c__Entity),
inference(resolution,[],[f27610,f13689]) ).
fof(f27635,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Process)
| p__d__subclass(X0,c__Physical) ),
inference(resolution,[],[f13842,f13400]) ).
fof(f27684,plain,
p__d__disjointDecomposition3(c__Physical,c__Object,c__Process),
inference(resolution,[],[f13684,f13418]) ).
fof(f27685,plain,
p__d__disjoint(c__Object,c__Process),
inference(resolution,[],[f27684,f13489]) ).
fof(f27686,plain,
! [X0] :
( ~ p__d__instance(X0,c__Process)
| ~ p__d__instance(X0,c__Object) ),
inference(resolution,[],[f27685,f13403]) ).
fof(f27699,plain,
p__d__disjointDecomposition3(c__QuantityChange,c__Increasing,c__Decreasing),
inference(resolution,[],[f15567,f13418]) ).
fof(f27700,plain,
p__d__disjoint(c__Increasing,c__Decreasing),
inference(resolution,[],[f27699,f13489]) ).
fof(f27754,plain,
! [X0] :
( ~ p__d__subclass(X0,c__InternalChange)
| p__d__subclass(X0,c__Process) ),
inference(resolution,[],[f15880,f13400]) ).
fof(f27807,plain,
! [X0,X1] :
( p__d__instance(sK60(X0),X1)
| ~ p__d__subclass(X0,c__Entity)
| ~ p__d__subclass(X0,X1) ),
inference(resolution,[],[f13680,f13402]) ).
fof(f27812,definition,
( spl1263_42
<=> p__d__subclass(c__QuantityChange,c__Entity) ),
introduced(definition,[new_symbols(definition,[spl1263_42])],[avatar_definition]) ).
fof(f27813,plain,
( p__d__subclass(c__QuantityChange,c__Entity)
| ~ spl1263_42 ),
inference(avatar_component_clause,[],[f27812]) ).
fof(f27814,plain,
( ~ p__d__subclass(c__QuantityChange,c__Entity)
| spl1263_42 ),
inference(avatar_component_clause,[],[f27812]) ).
fof(f27816,plain,
! [X0,X1] :
( ~ p__d__subclass(X0,c__QuantityChange)
| ~ p__d__subclass(X0,c__Entity)
| p__d__instance(X1,c__Process)
| sK60(X0) = X1 ),
inference(resolution,[],[f27807,f24205]) ).
fof(f27819,plain,
! [X0] :
( ~ p__d__subclass(c__Increasing,c__Entity)
| p__d__instance(X0,c__Process)
| sK60(c__Increasing) = X0 ),
inference(resolution,[],[f27816,f15568]) ).
fof(f27820,plain,
! [X0] :
( ~ p__d__subclass(c__Decreasing,c__Entity)
| p__d__instance(X0,c__Process)
| sK60(c__Decreasing) = X0 ),
inference(resolution,[],[f27816,f15571]) ).
fof(f27822,definition,
( spl1263_43
<=> ! [X0] :
( p__d__instance(X0,c__Process)
| sK60(c__Decreasing) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl1263_43])],[avatar_definition]) ).
fof(f27823,plain,
( ! [X0] :
( p__d__instance(X0,c__Process)
| sK60(c__Decreasing) = X0 )
| ~ spl1263_43 ),
inference(avatar_component_clause,[],[f27822]) ).
fof(f27825,definition,
( spl1263_44
<=> p__d__subclass(c__Decreasing,c__Entity) ),
introduced(definition,[new_symbols(definition,[spl1263_44])],[avatar_definition]) ).
fof(f27826,plain,
( p__d__subclass(c__Decreasing,c__Entity)
| ~ spl1263_44 ),
inference(avatar_component_clause,[],[f27825]) ).
fof(f27827,plain,
( ~ p__d__subclass(c__Decreasing,c__Entity)
| spl1263_44 ),
inference(avatar_component_clause,[],[f27825]) ).
fof(f27828,plain,
( spl1263_43
| ~ spl1263_44 ),
inference(avatar_split_clause,[],[f27820,f27825,f27822]) ).
fof(f27830,definition,
( spl1263_45
<=> ! [X0] :
( p__d__instance(X0,c__Process)
| sK60(c__Increasing) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl1263_45])],[avatar_definition]) ).
fof(f27831,plain,
( ! [X0] :
( p__d__instance(X0,c__Process)
| sK60(c__Increasing) = X0 )
| ~ spl1263_45 ),
inference(avatar_component_clause,[],[f27830]) ).
fof(f27833,definition,
( spl1263_46
<=> p__d__subclass(c__Increasing,c__Entity) ),
introduced(definition,[new_symbols(definition,[spl1263_46])],[avatar_definition]) ).
fof(f27834,plain,
( p__d__subclass(c__Increasing,c__Entity)
| ~ spl1263_46 ),
inference(avatar_component_clause,[],[f27833]) ).
fof(f27835,plain,
( ~ p__d__subclass(c__Increasing,c__Entity)
| spl1263_46 ),
inference(avatar_component_clause,[],[f27833]) ).
fof(f27836,plain,
( spl1263_45
| ~ spl1263_46 ),
inference(avatar_split_clause,[],[f27819,f27833,f27830]) ).
fof(f27849,plain,
! [X0] :
( ~ p__d__instance(X0,c__Decreasing)
| ~ p__d__instance(X0,c__Increasing) ),
inference(resolution,[],[f27700,f13403]) ).
fof(f28297,plain,
p__d__subclass(c__QuantityChange,c__Process),
inference(resolution,[],[f27754,f15566]) ).
fof(f28299,plain,
p__d__subclass(c__QuantityChange,c__Physical),
inference(resolution,[],[f28297,f27635]) ).
fof(f28315,plain,
p__d__subclass(c__QuantityChange,c__Entity),
inference(resolution,[],[f28299,f27610]) ).
fof(f28328,plain,
( $false
| spl1263_42 ),
inference(forward_subsumption_resolution,[],[f28315,f27814]) ).
fof(f28329,plain,
spl1263_42,
inference(avatar_contradiction_clause,[],[f28328]) ).
fof(f28331,plain,
( ! [X0] :
( ~ p__d__subclass(X0,c__QuantityChange)
| p__d__subclass(X0,c__Entity) )
| ~ spl1263_42 ),
inference(resolution,[],[f27813,f13400]) ).
fof(f28343,plain,
( p__d__subclass(c__Increasing,c__Entity)
| ~ spl1263_42 ),
inference(resolution,[],[f28331,f15568]) ).
fof(f28344,plain,
( p__d__subclass(c__Decreasing,c__Entity)
| ~ spl1263_42 ),
inference(resolution,[],[f28331,f15571]) ).
fof(f28345,plain,
( $false
| ~ spl1263_42
| spl1263_44 ),
inference(forward_subsumption_resolution,[],[f28344,f27827]) ).
fof(f28346,plain,
( ~ spl1263_42
| spl1263_44 ),
inference(avatar_contradiction_clause,[],[f28345]) ).
fof(f28347,plain,
( $false
| ~ spl1263_42
| spl1263_46 ),
inference(forward_subsumption_resolution,[],[f28343,f27835]) ).
fof(f28348,plain,
( ~ spl1263_42
| spl1263_46 ),
inference(avatar_contradiction_clause,[],[f28347]) ).
fof(f28385,plain,
( ! [X0] :
( ~ p__d__instance(X0,c__Object)
| sK60(c__Decreasing) = X0 )
| ~ spl1263_43 ),
inference(resolution,[],[f27823,f27686]) ).
fof(f28389,plain,
( ! [X0] :
( ~ p__d__instance(X0,c__Object)
| sK60(c__Increasing) = X0 )
| ~ spl1263_45 ),
inference(resolution,[],[f27831,f27686]) ).
fof(f28393,plain,
( sK60(c__Decreasing) = sK60(c__Object)
| ~ p__d__subclass(c__Object,c__Entity)
| ~ spl1263_43 ),
inference(resolution,[],[f28385,f13680]) ).
fof(f28396,plain,
( sK60(c__Decreasing) = sK60(c__Object)
| ~ spl1263_43 ),
inference(forward_subsumption_resolution,[],[f28393,f27622]) ).
fof(f28402,plain,
( sK60(c__Increasing) = sK60(c__Object)
| ~ p__d__subclass(c__Object,c__Entity)
| ~ spl1263_45 ),
inference(resolution,[],[f28389,f13680]) ).
fof(f28405,plain,
( sK60(c__Increasing) = sK60(c__Object)
| ~ spl1263_45 ),
inference(forward_subsumption_resolution,[],[f28402,f27622]) ).
fof(f28407,plain,
( p__d__instance(sK60(c__Object),c__Increasing)
| ~ p__d__subclass(c__Increasing,c__Entity)
| ~ spl1263_45 ),
inference(superposition,[],[f13680,f28405]) ).
fof(f28408,plain,
( p__d__instance(sK60(c__Object),c__Increasing)
| ~ spl1263_45
| ~ spl1263_46 ),
inference(forward_subsumption_resolution,[],[f28407,f27834]) ).
fof(f28671,plain,
( ~ p__d__instance(sK60(c__Decreasing),c__Increasing)
| ~ p__d__subclass(c__Decreasing,c__Entity) ),
inference(resolution,[],[f27849,f13680]) ).
fof(f28677,plain,
( ~ p__d__instance(sK60(c__Decreasing),c__Increasing)
| ~ spl1263_44 ),
inference(forward_subsumption_resolution,[],[f28671,f27826]) ).
fof(f28678,plain,
( ~ p__d__instance(sK60(c__Object),c__Increasing)
| ~ spl1263_43
| ~ spl1263_44 ),
inference(forward_demodulation,[],[f28677,f28396]) ).
fof(f28679,plain,
( $false
| ~ spl1263_43
| ~ spl1263_44
| ~ spl1263_45
| ~ spl1263_46 ),
inference(forward_subsumption_resolution,[],[f28678,f28408]) ).
fof(f28680,plain,
( ~ spl1263_43
| ~ spl1263_44
| ~ spl1263_45
| ~ spl1263_46 ),
inference(avatar_contradiction_clause,[],[f28679]) ).
cnf(s23,plain,
( spl1263_43
| ~ spl1263_44 ),
inference(sat_conversion,[],[f27828]) ).
cnf(s24,plain,
( spl1263_45
| ~ spl1263_46 ),
inference(sat_conversion,[],[f27836]) ).
cnf(s59,plain,
spl1263_42,
inference(sat_conversion,[],[f28329]) ).
cnf(s61,plain,
( ~ spl1263_42
| spl1263_44 ),
inference(sat_conversion,[],[f28346]) ).
cnf(s62,plain,
( ~ spl1263_42
| spl1263_46 ),
inference(sat_conversion,[],[f28348]) ).
cnf(s85,plain,
( ~ spl1263_43
| ~ spl1263_44
| ~ spl1263_45
| ~ spl1263_46 ),
inference(sat_conversion,[],[f28680]) ).
cnf(s86,plain,
spl1263_46,
inference(rat,[],[s62,s59]) ).
cnf(s87,plain,
spl1263_44,
inference(rat,[],[s61,s59]) ).
cnf(s88,plain,
spl1263_45,
inference(rat,[],[s24,s86]) ).
cnf(s89,plain,
~ spl1263_43,
inference(rat,[],[s85,s86,s87,s88]) ).
cnf(s90,plain,
$false,
inference(rat,[],[s23,s87,s89]) ).
fof(f28681,plain,
$false,
inference(avatar_sat_refutation,[],[s90]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR227+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n026.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 23:51:42 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.98/2.21 % (210199)Detected formulas, will run a generic FOF schedule.
% 9.98/2.21 % (210207)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2547400694:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 9.98/2.21 % (210207)Refutation not found, incomplete strategy
% 9.98/2.21 % (210207)------------------------------
% 9.98/2.21 % (210207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.98/2.21 % (210207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.98/2.21 % (210207)CaDiCaL version: 2.1.3
% 9.98/2.21 % (210207)Termination reason: Refutation not found, incomplete strategy
% 9.98/2.21 % (210207)Time elapsed: 0.010 s
% 9.98/2.21 % (210207)Peak memory usage: 94 MB
% 9.98/2.21 % (210207)Instructions burned: 24 (million)
% 9.98/2.21 % (210208)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=191960295:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 9.98/2.21 % (210209)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=192926155:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 9.98/2.21 % (210206)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=2766012736:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 9.98/2.21 % (210205)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=260334503:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 9.98/2.21 % (210204)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=4151978571:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 9.98/2.21 % (210210)dis-21_1_sil=8000:lcm=predicate:random_seed=3125194426: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.98/2.21 % (210208)Instruction limit reached!
% 9.98/2.21 % (210208)------------------------------
% 9.98/2.21 % (210208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.98/2.22 % (210208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.98/2.22 % (210208)CaDiCaL version: 2.1.3
% 9.98/2.22 % (210208)Termination reason: Instruction limit
% 9.98/2.22 % (210208)Termination phase: Saturation
% 9.98/2.22 % (210208)Time elapsed: 0.066 s
% 9.98/2.22 % (210208)Peak memory usage: 93 MB
% 9.98/2.22 % (210208)Instructions burned: 119 (million)
% 9.98/2.22 % (210209)Instruction limit reached!
% 9.98/2.22 % (210209)------------------------------
% 9.98/2.22 % (210209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.98/2.22 % (210209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.98/2.22 % (210209)CaDiCaL version: 2.1.3
% 9.98/2.22 % (210209)Termination reason: Instruction limit
% 9.98/2.22 % (210209)Termination phase: Preprocessing 3
% 9.98/2.22 % (210209)Time elapsed: 0.088 s
% 9.98/2.22 % (210209)Peak memory usage: 94 MB
% 9.98/2.22 % (210209)Instructions burned: 139 (million)
% 9.98/2.22 % (210210)Instruction limit reached!
% 9.98/2.22 % (210210)------------------------------
% 9.98/2.22 % (210210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.98/2.22 % (210210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.98/2.22 % (210210)CaDiCaL version: 2.1.3
% 9.98/2.22 % (210210)Termination reason: Instruction limit
% 9.98/2.22 % (210210)Termination phase: Saturation
% 9.98/2.22 % (210210)Time elapsed: 0.077 s
% 9.98/2.22 % (210210)Peak memory usage: 95 MB
% 9.98/2.22 % (210210)Instructions burned: 130 (million)
% 9.98/2.22 % (210207)------------------------------
% 9.98/2.22 % (210207)------------------------------
% 9.98/2.22 % (210218)lrs+10_1_sil=8000:sp=occurrence:random_seed=434942316:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 9.98/2.22 % (210221)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=153750306:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 9.98/2.22 % (210220)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4133009585:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 9.98/2.22 % (210219)lrs+10_1_sil=32000:urr=on:br=off:random_seed=611637437:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 9.98/2.22 % (210220)Refutation not found, incomplete strategy
% 13.88/2.96 % (210220)------------------------------
% 13.88/2.96 % (210220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.88/2.96 % (210220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.88/2.96 % (210220)CaDiCaL version: 2.1.3
% 13.88/2.96 % (210220)Termination reason: Refutation not found, incomplete strategy
% 13.88/2.96 % (210220)Time elapsed: 0.016 s
% 13.88/2.96 % (210220)Peak memory usage: 94 MB
% 13.88/2.96 % (210220)Instructions burned: 20 (million)
% 13.88/2.96 % (210219)Refutation not found, incomplete strategy
% 13.88/2.96 % (210219)------------------------------
% 13.88/2.96 % (210219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.88/2.96 % (210219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.88/2.96 % (210219)CaDiCaL version: 2.1.3
% 13.88/2.96 % (210219)Termination reason: Refutation not found, incomplete strategy
% 13.88/2.96 % (210219)Time elapsed: 0.032 s
% 13.88/2.96 % (210219)Peak memory usage: 94 MB
% 13.88/2.96 % (210219)Instructions burned: 61 (million)
% 13.88/2.96 % (210221)Instruction limit reached!
% 13.88/2.96 % (210221)------------------------------
% 13.88/2.96 % (210221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.88/2.96 % (210221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.88/2.96 % (210221)CaDiCaL version: 2.1.3
% 13.88/2.96 % (210221)Termination reason: Instruction limit
% 13.88/2.96 % (210221)Termination phase: Saturation
% 13.88/2.96 % (210221)Time elapsed: 0.073 s
% 13.88/2.96 % (210221)Peak memory usage: 98 MB
% 13.88/2.96 % (210221)Instructions burned: 248 (million)
% 13.88/2.96 % (210218)Instruction limit reached!
% 13.88/2.96 % (210218)------------------------------
% 13.88/2.96 % (210218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.88/2.96 % (210218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.88/2.96 % (210218)CaDiCaL version: 2.1.3
% 13.88/2.96 % (210218)Termination reason: Instruction limit
% 13.88/2.96 % (210218)Termination phase: Saturation
% 13.88/2.96 % (210218)Time elapsed: 0.148 s
% 13.88/2.96 % (210218)Peak memory usage: 95 MB
% 13.88/2.96 % (210218)Instructions burned: 285 (million)
% 13.88/2.96 % (210226)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2330379712:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 13.88/2.96 % (210226)Refutation not found, incomplete strategy
% 13.88/2.96 % (210226)------------------------------
% 13.88/2.96 % (210226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.88/2.96 % (210226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.88/2.96 % (210226)CaDiCaL version: 2.1.3
% 13.88/2.96 % (210226)Termination reason: Refutation not found, incomplete strategy
% 13.88/2.96 % (210226)Time elapsed: 0.013 s
% 13.88/2.96 % (210226)Peak memory usage: 94 MB
% 13.88/2.96 % (210226)Instructions burned: 34 (million)
% 13.88/2.96 % (210227)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1304257061:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 13.88/2.96 % (210220)------------------------------
% 13.88/2.96 % (210220)------------------------------
% 13.88/2.96 % (210219)------------------------------
% 13.88/2.96 % (210219)------------------------------
% 13.88/2.96 % (210226)------------------------------
% 13.88/2.96 % (210226)------------------------------
% 13.88/2.96 % (210230)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2958240481:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 13.88/2.96 % (210232)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1075086014:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 13.88/2.96 % (210231)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1592469100:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 13.88/2.96 % (210232)Instruction limit reached!
% 13.88/2.96 % (210232)------------------------------
% 13.88/2.96 % (210232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.88/2.96 % (210232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.88/2.96 % (210232)CaDiCaL version: 2.1.3
% 13.88/2.96 % (210232)Termination reason: Instruction limit
% 13.88/2.96 % (210232)Termination phase: Property scanning
% 13.88/2.96 % (210232)Time elapsed: 0.032 s
% 13.88/2.96 % (210232)Peak memory usage: 92 MB
% 13.88/2.96 % (210232)Instructions burned: 116 (million)
% 22.01/3.95 % (210230)Instruction limit reached!
% 22.01/3.95 % (210230)------------------------------
% 22.01/3.95 % (210230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.01/3.95 % (210230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.01/3.95 % (210230)CaDiCaL version: 2.1.3
% 22.01/3.95 % (210230)Termination reason: Instruction limit
% 22.01/3.95 % (210230)Termination phase: Saturation
% 22.01/3.95 % (210230)Time elapsed: 0.062 s
% 22.01/3.95 % (210230)Peak memory usage: 94 MB
% 22.01/3.95 % (210230)Instructions burned: 114 (million)
% 22.01/3.95 % (210206)Refutation not found, incomplete strategy
% 22.01/3.95 % (210206)------------------------------
% 22.01/3.95 % (210206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.01/3.95 % (210206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.01/3.95 % (210206)CaDiCaL version: 2.1.3
% 22.01/3.95 % (210206)Termination reason: Refutation not found, incomplete strategy
% 22.01/3.95 % (210206)Time elapsed: 0.691 s
% 22.01/3.95 % (210206)Peak memory usage: 146 MB
% 22.01/3.95 % (210206)Instructions burned: 1018 (million)
% 22.01/3.95 % (210231)Instruction limit reached!
% 22.01/3.95 % (210231)------------------------------
% 22.01/3.95 % (210231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.01/3.95 % (210231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.01/3.95 % (210231)CaDiCaL version: 2.1.3
% 22.01/3.95 % (210231)Termination reason: Instruction limit
% 22.01/3.95 % (210231)Termination phase: Property scanning
% 22.01/3.95 % (210231)Time elapsed: 0.079 s
% 22.01/3.95 % (210231)Peak memory usage: 96 MB
% 22.01/3.95 % (210231)Instructions burned: 129 (million)
% 22.01/3.95 % (210236)lrs+10_1_sil=8000:sp=occurrence:random_seed=2584759094:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 22.01/3.95 % (210237)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2332259707:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 22.01/3.95 % (210237)Refutation not found, incomplete strategy
% 22.01/3.95 % (210237)------------------------------
% 22.01/3.95 % (210237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.01/3.95 % (210237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.01/3.96 % (210237)CaDiCaL version: 2.1.3
% 22.01/3.96 % (210237)Termination reason: Refutation not found, incomplete strategy
% 22.01/3.96 % (210237)Time elapsed: 0.016 s
% 22.01/3.96 % (210237)Peak memory usage: 94 MB
% 22.01/3.96 % (210237)Instructions burned: 19 (million)
% 22.01/3.96 % (210238)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2027456780:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 22.01/3.96 % (210206)------------------------------
% 22.01/3.96 % (210206)------------------------------
% 22.01/3.96 % (210236)Instruction limit reached!
% 22.01/3.96 % (210236)------------------------------
% 22.01/3.96 % (210236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.01/3.96 % (210236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.01/3.96 % (210236)CaDiCaL version: 2.1.3
% 22.01/3.96 % (210236)Termination reason: Instruction limit
% 22.01/3.96 % (210236)Termination phase: Saturation
% 22.01/3.96 % (210236)Time elapsed: 0.314 s
% 22.01/3.96 % (210236)Peak memory usage: 117 MB
% 22.01/3.96 % (210236)Instructions burned: 909 (million)
% 22.01/3.96 % (210237)------------------------------
% 22.01/3.96 % (210237)------------------------------
% 22.01/3.96 % (210242)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1053903797:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 22.01/3.96 % (210242)Refutation not found, incomplete strategy
% 22.01/3.96 % (210242)------------------------------
% 22.01/3.96 % (210242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.01/3.96 % (210242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.01/3.96 % (210242)CaDiCaL version: 2.1.3
% 22.01/3.96 % (210242)Termination reason: Refutation not found, incomplete strategy
% 22.01/3.96 % (210242)Time elapsed: 0.020 s
% 22.01/3.96 % (210242)Peak memory usage: 94 MB
% 22.01/3.96 % (210242)Instructions burned: 25 (million)
% 22.01/3.96 % (210243)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2819836299:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 22.01/3.96 % (210245)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1945199819:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi)
% 22.01/3.96 % (210243)Instruction limit reached!
% 22.01/3.96 % (210243)------------------------------
% 22.01/3.96 % (210243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.01/3.96 % (210243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.01/3.96 % (210243)CaDiCaL version: 2.1.3
% 22.01/3.96 % (210243)Termination reason: Instruction limit
% 22.01/3.96 % (210243)Termination phase: Saturation
% 22.01/3.96 % (210243)Time elapsed: 0.174 s
% 22.01/3.96 % (210243)Peak memory usage: 100 MB
% 22.01/3.96 % (210243)Instructions burned: 592 (million)
% 22.01/3.96 % (210242)------------------------------
% 22.01/3.96 % (210242)------------------------------
% 22.01/3.96 % (210248)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=1927506996:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 22.01/3.96 % (210248)Instruction limit reached!
% 22.01/3.96 % (210248)------------------------------
% 22.01/3.96 % (210248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.01/3.96 % (210248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.01/3.96 % (210248)CaDiCaL version: 2.1.3
% 22.01/3.96 % (210248)Termination reason: Instruction limit
% 22.01/3.96 % (210248)Termination phase: Preprocessing 3
% 22.01/3.96 % (210248)Time elapsed: 0.047 s
% 22.01/3.96 % (210248)Peak memory usage: 93 MB
% 22.01/3.96 % (210248)Instructions burned: 128 (million)
% 22.01/3.96 % (210249)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=898979950:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 22.01/3.96 % (210249)Instruction limit reached!
% 22.01/3.96 % (210249)------------------------------
% 22.01/3.96 % (210249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.01/3.96 % (210249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.01/3.96 % (210249)CaDiCaL version: 2.1.3
% 22.01/3.96 % (210249)Termination reason: Instruction limit
% 22.01/3.96 % (210249)Termination phase: Preprocessing 2
% 22.01/3.96 % (210249)Time elapsed: 0.073 s
% 22.01/3.96 % (210249)Peak memory usage: 92 MB
% 22.01/3.96 % (210249)Instructions burned: 134 (million)
% 22.01/3.96 % (210251)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2784395054:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/141Mi)
% 22.01/3.96 % (210251)Refutation not found, incomplete strategy
% 22.01/3.96 % (210251)------------------------------
% 22.01/3.96 % (210251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.01/3.96 % (210251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.01/3.96 % (210251)CaDiCaL version: 2.1.3
% 22.01/3.96 % (210251)Termination reason: Refutation not found, incomplete strategy
% 22.01/3.96 % (210251)Time elapsed: 0.010 s
% 22.01/3.96 % (210251)Peak memory usage: 94 MB
% 22.01/3.96 % (210251)Instructions burned: 23 (million)
% 22.01/3.96 % (210254)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1961169325:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2981 on theBenchmark for (2981ds/431Mi)
% 22.01/3.96 % (210254)Refutation not found, incomplete strategy
% 22.01/3.96 % (210254)------------------------------
% 22.01/3.96 % (210254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.01/3.96 % (210254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.01/3.96 % (210254)CaDiCaL version: 2.1.3
% 22.01/3.96 % (210254)Termination reason: Refutation not found, incomplete strategy
% 22.01/3.96 % (210254)Time elapsed: 0.016 s
% 22.01/3.96 % (210254)Peak memory usage: 94 MB
% 22.01/3.96 % (210254)Instructions burned: 20 (million)
% 22.01/3.96 % (210251)------------------------------
% 22.01/3.96 % (210251)------------------------------
% 22.01/3.96 % (210256)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=251357849:i=6060:aac=none:ins=25_2979 on theBenchmark for (2979ds/6060Mi)
% 22.01/3.96 % (210254)------------------------------
% 22.01/3.96 % (210254)------------------------------
% 22.01/3.96 % (210227)Instruction limit reached!
% 22.01/3.96 % (210227)------------------------------
% 22.01/3.96 % (210227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.01/3.96 % (210227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.01/3.96 % (210227)CaDiCaL version: 2.1.3
% 22.01/3.96 % (210227)Termination reason: Instruction limit
% 22.01/3.96 % (210227)Termination phase: Saturation
% 22.01/3.96 % (210227)Time elapsed: 1.493 s
% 22.01/3.96 % (210227)Peak memory usage: 213 MB
% 22.01/3.96 % (210227)Instructions burned: 2352 (million)
% 22.01/3.96 % (210258)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=562054325:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2977 on theBenchmark for (2977ds/150Mi)
% 22.01/3.96 % (210259)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2092459350:i=14155:bd=all_2977 on theBenchmark for (2977ds/14155Mi)
% 22.01/3.96 % (210258)Instruction limit reached!
% 22.01/3.96 % (210258)------------------------------
% 22.01/3.96 % (210258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.01/3.96 % (210258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.01/3.96 % (210258)CaDiCaL version: 2.1.3
% 22.01/3.96 % (210258)Termination reason: Instruction limit
% 22.01/3.96 % (210258)Termination phase: Property scanning
% 22.01/3.96 % (210258)Time elapsed: 0.089 s
% 22.01/3.96 % (210258)Peak memory usage: 96 MB
% 22.01/3.96 % (210258)Instructions burned: 152 (million)
% 22.01/3.96 % (210262)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1899541570:i=667:av=off:fsr=off_2974 on theBenchmark for (2974ds/667Mi)
% 22.01/3.96 % (210262)Instruction limit reached!
% 22.01/3.96 % (210262)------------------------------
% 22.01/3.96 % (210262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.01/3.96 % (210262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.01/3.96 % (210262)CaDiCaL version: 2.1.3
% 22.01/3.96 % (210262)Termination reason: Instruction limit
% 22.01/3.96 % (210262)Termination phase: Saturation
% 22.01/3.96 % (210262)Time elapsed: 0.339 s
% 22.01/3.96 % (210262)Peak memory usage: 106 MB
% 22.01/3.96 % (210262)Instructions burned: 668 (million)
% 22.01/3.96 % (210204)First to succeed.
% 22.01/3.96 % (210204)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-210199"
% 22.01/3.96 % (210264)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=2233227993:s2a=on:i=185:s2at=1.8:fdi=4_2970 on theBenchmark for (2970ds/185Mi)
% 22.01/3.96 % (210264)Instruction limit reached!
% 22.01/3.96 % (210264)------------------------------
% 22.01/3.96 % (210264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.01/3.96 % (210264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.01/3.96 % (210264)CaDiCaL version: 2.1.3
% 22.01/3.96 % (210264)Termination reason: Instruction limit
% 22.01/3.96 % (210264)Termination phase: Property scanning
% 22.01/3.96 % (210264)Time elapsed: 0.120 s
% 22.01/3.96 % (210264)Peak memory usage: 97 MB
% 22.01/3.96 % (210264)Instructions burned: 186 (million)
% 22.01/3.96 % (210204)Refutation found. Thanks to Tanya!
% 22.01/3.96 % SZS status Theorem for theBenchmark
% 22.01/3.96 % SZS output start Proof for theBenchmark
% See solution above
% 22.70/4.08 % (210204)------------------------------
% 22.70/4.08 % (210204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.70/4.08 % (210204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.70/4.08 % (210204)CaDiCaL version: 2.1.3
% 22.70/4.08 % (210204)Termination reason: Refutation
% 22.70/4.08 % (210204)Time elapsed: 2.678 s
% 22.70/4.08 % (210204)Peak memory usage: 236 MB
% 22.70/4.08 % (210204)Instructions burned: 4496 (million)
% 22.70/4.08 % (210204)------------------------------
% 22.70/4.08 % (210204)------------------------------
% 22.70/4.08 % (210199)Success in time 3.277 s
% 22.70/4.08 % Vampire exiting
%------------------------------------------------------------------------------