%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR269+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 : n007.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:13 AM UTC 2026
% Result : Theorem 36.07s 6.04s
% Output : Refutation 37.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 21
% Syntax : Number of formulae : 113 ( 35 unt; 5 def)
% Number of atoms : 563 ( 9 equ)
% Maximal formula atoms : 80 ( 4 avg)
% Number of connectives : 659 ( 209 ~; 199 |; 218 &)
% ( 26 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 6 prp; 0-7 aty)
% Number of functors : 15 ( 15 usr; 11 con; 0-2 aty)
% Number of variables : 287 ( 0 sgn 275 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : p__d__subclass(X0,X0),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',predefinitionsA8) ).
fof(f4,axiom,
! [X0,X1,X2] :
( ( p__d__instance(X0,X1)
& p__d__subclass(X1,X2) )
=> p__d__instance(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',predefinitionsA12) ).
fof(f5,axiom,
! [X0,X1] :
( p__d__disjoint(X0,X1)
<=> ! [X2] :
( ~ p__d__instance(X2,X0)
| ~ p__d__instance(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',predefinitionsA15) ).
fof(f6,axiom,
( ! [X0,X1,X2] :
( p__d__partition3(X0,X1,X2)
<=> ( p__d__exhaustiveDecomposition3(X0,X1,X2)
& p__d__disjointDecomposition3(X0,X1,X2) ) )
& ! [X0,X1,X2,X3] :
( p__d__partition4(X0,X1,X2,X3)
<=> ( p__d__exhaustiveDecomposition4(X0,X1,X2,X3)
& p__d__disjointDecomposition4(X0,X1,X2,X3) ) )
& ! [X0,X1,X2,X3,X4] :
( p__d__partition5(X0,X1,X2,X3,X4)
<=> ( p__d__exhaustiveDecomposition5(X0,X1,X2,X3,X4)
& p__d__disjointDecomposition5(X0,X1,X2,X3,X4) ) )
& ! [X0,X1,X2,X3,X4,X5] :
( p__d__partition6(X0,X1,X2,X3,X4,X5)
<=> ( p__d__exhaustiveDecomposition6(X0,X1,X2,X3,X4,X5)
& p__d__disjointDecomposition6(X0,X1,X2,X3,X4,X5) ) )
& ! [X0,X1,X2,X3,X4,X5,X6] :
( p__d__partition7(X0,X1,X2,X3,X4,X5,X6)
<=> ( p__d__exhaustiveDecomposition7(X0,X1,X2,X3,X4,X5,X6)
& p__d__disjointDecomposition7(X0,X1,X2,X3,X4,X5,X6) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',predefinitionsA18) ).
fof(f8,axiom,
( ! [X0,X1,X2] :
( p__d__disjointDecomposition3(X0,X1,X2)
<=> p__d__disjoint(X1,X2) )
& ! [X0,X1,X2,X3] :
( p__d__disjointDecomposition4(X0,X1,X2,X3)
<=> ( p__d__disjoint(X1,X2)
& p__d__disjoint(X1,X3)
& p__d__disjoint(X2,X3) ) )
& ! [X0,X1,X2,X3,X4] :
( p__d__disjointDecomposition5(X0,X1,X2,X3,X4)
<=> ( p__d__disjoint(X1,X2)
& p__d__disjoint(X1,X3)
& p__d__disjoint(X1,X4)
& p__d__disjoint(X2,X3)
& p__d__disjoint(X2,X4)
& p__d__disjoint(X3,X4) ) )
& ! [X0,X1,X2,X3,X4,X5] :
( p__d__disjointDecomposition6(X0,X1,X2,X3,X4,X5)
<=> ( p__d__disjoint(X1,X2)
& p__d__disjoint(X1,X3)
& p__d__disjoint(X1,X4)
& p__d__disjoint(X1,X5)
& p__d__disjoint(X2,X3)
& p__d__disjoint(X2,X4)
& p__d__disjoint(X2,X5)
& p__d__disjoint(X3,X4)
& p__d__disjoint(X3,X5)
& p__d__disjoint(X4,X5) ) )
& ! [X0,X1,X2,X3,X4,X5,X6] :
( p__d__disjointDecomposition7(X0,X1,X2,X3,X4,X5,X6)
<=> ( p__d__disjoint(X1,X2)
& p__d__disjoint(X1,X3)
& p__d__disjoint(X1,X4)
& p__d__disjoint(X1,X5)
& p__d__disjoint(X1,X6)
& p__d__disjoint(X2,X3)
& p__d__disjoint(X2,X4)
& p__d__disjoint(X2,X5)
& p__d__disjoint(X2,X6)
& p__d__disjoint(X3,X4)
& p__d__disjoint(X3,X5)
& p__d__disjoint(X3,X6)
& p__d__disjoint(X4,X5)
& p__d__disjoint(X4,X6)
& p__d__disjoint(X5,X6) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',predefinitionsA24) ).
fof(f107,axiom,
p__d__partition3(c__Entity,c__Physical,c__Abstract),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA173) ).
fof(f110,axiom,
! [X0] :
( p__d__subclass(X0,c__Entity)
=> ? [X1] : p__d__instance(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA176) ).
fof(f115,axiom,
p__d__subclass(c__Object,c__Physical),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA181) ).
fof(f239,axiom,
p__d__subclass(c__Abstract,c__Entity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA330) ).
fof(f241,axiom,
p__d__subclass(c__Quantity,c__Abstract),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA332) ).
fof(f452,axiom,
p__d__subclass(c__PhysicalQuantity,c__Quantity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA561) ).
fof(f454,axiom,
p__d__subclass(c__ConstantQuantity,c__PhysicalQuantity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA563) ).
fof(f1054,axiom,
p__d__subclass(c__AngleMeasure,c__ConstantQuantity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA1539) ).
fof(f1056,axiom,
p__d__subclass(c__PlaneAngleMeasure,c__AngleMeasure),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA1541) ).
fof(f7433,conjecture,
? [X0] :
( p__d__instance(X0,c__PlaneAngleMeasure)
& ! [X1] :
( p__d__instance(X1,c__Object)
=> ( ? [X2] :
( p__d__instance(X2,c__Attribute)
& p__d__instance(X2,c__RightAngle)
& p__attribute(X1,X2) )
=> X0 != X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antonymPattern20028) ).
fof(f7434,negated_conjecture,
~ ? [X0] :
( p__d__instance(X0,c__PlaneAngleMeasure)
& ! [X1] :
( p__d__instance(X1,c__Object)
=> ( ? [X2] :
( p__d__instance(X2,c__Attribute)
& p__d__instance(X2,c__RightAngle)
& p__attribute(X1,X2) )
=> 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] :
( ~ p__d__instance(X0,c__PlaneAngleMeasure)
| ? [X1] :
( X0 = X1
& ? [X2] :
( p__d__instance(X2,c__Attribute)
& p__d__instance(X2,c__RightAngle)
& p__attribute(X1,X2) )
& p__d__instance(X1,c__Object) ) ),
inference(ennf_transformation,[],[f7434]) ).
fof(f11601,plain,
! [X0] :
( ~ p__d__instance(X0,c__PlaneAngleMeasure)
| ? [X1] :
( X0 = X1
& ? [X2] :
( p__d__instance(X2,c__Attribute)
& p__d__instance(X2,c__RightAngle)
& p__attribute(X1,X2) )
& p__d__instance(X1,c__Object) ) ),
inference(flattening,[],[f11600]) ).
fof(f11658,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(f11659,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,[],[f11658]) ).
fof(f11660,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))],[f11659]) ).
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(nnf_transformation,[],[f7435]) ).
fof(f11662,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,[],[f11661]) ).
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(nnf_transformation,[],[f7437]) ).
fof(f11667,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,[],[f11666]) ).
fof(f11722,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,
! [X0] :
( ~ p__d__instance(X0,c__PlaneAngleMeasure)
| ( sK1263(X0) = X0
& p__d__instance(sK1264(X0),c__Attribute)
& p__d__instance(sK1264(X0),c__RightAngle)
& p__attribute(sK1263(X0),sK1264(X0))
& p__d__instance(sK1263(X0),c__Object) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1263,sK1264]),skolemize(X1,sK1263(X0)),skolemize(X2,sK1264(X0))],[f11601]) ).
fof(f13401,plain,
! [X0] : p__d__subclass(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f13402,plain,
! [X2,X0,X1] :
( ~ p__d__subclass(X1,X2)
| ~ p__d__subclass(X0,X1)
| p__d__subclass(X0,X2) ),
inference(cnf_transformation,[],[f7450]) ).
fof(f13404,plain,
! [X2,X0,X1] :
( ~ p__d__instance(X0,X1)
| p__d__instance(X0,X2)
| ~ p__d__subclass(X1,X2) ),
inference(cnf_transformation,[],[f7454]) ).
fof(f13405,plain,
! [X3,X0,X1] :
( ~ p__d__disjoint(X0,X1)
| ~ p__d__instance(X3,X1)
| ~ p__d__instance(X3,X0) ),
inference(cnf_transformation,[],[f11660]) ).
fof(f13420,plain,
! [X2,X0,X1] :
( ~ p__d__partition3(X0,X1,X2)
| p__d__disjointDecomposition3(X0,X1,X2) ),
inference(cnf_transformation,[],[f11662]) ).
fof(f13491,plain,
! [X2,X0,X1] :
( ~ p__d__disjointDecomposition3(X0,X1,X2)
| p__d__disjoint(X1,X2) ),
inference(cnf_transformation,[],[f11667]) ).
fof(f13679,plain,
p__d__partition3(c__Entity,c__Physical,c__Abstract),
inference(cnf_transformation,[],[f107]) ).
fof(f13682,plain,
! [X0] :
( p__d__instance(sK60(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(cnf_transformation,[],[f11722]) ).
fof(f13691,plain,
p__d__subclass(c__Object,c__Physical),
inference(cnf_transformation,[],[f115]) ).
fof(f13853,plain,
p__d__subclass(c__Abstract,c__Entity),
inference(cnf_transformation,[],[f239]) ).
fof(f13855,plain,
p__d__subclass(c__Quantity,c__Abstract),
inference(cnf_transformation,[],[f241]) ).
fof(f14076,plain,
p__d__subclass(c__PhysicalQuantity,c__Quantity),
inference(cnf_transformation,[],[f452]) ).
fof(f14078,plain,
p__d__subclass(c__ConstantQuantity,c__PhysicalQuantity),
inference(cnf_transformation,[],[f454]) ).
fof(f14819,plain,
p__d__subclass(c__AngleMeasure,c__ConstantQuantity),
inference(cnf_transformation,[],[f1054]) ).
fof(f14821,plain,
p__d__subclass(c__PlaneAngleMeasure,c__AngleMeasure),
inference(cnf_transformation,[],[f1056]) ).
fof(f24207,plain,
! [X0] :
( p__d__instance(sK1263(X0),c__Object)
| ~ p__d__instance(X0,c__PlaneAngleMeasure) ),
inference(cnf_transformation,[],[f13400]) ).
fof(f24211,plain,
! [X0] :
( ~ p__d__instance(X0,c__PlaneAngleMeasure)
| sK1263(X0) = X0 ),
inference(cnf_transformation,[],[f13400]) ).
fof(f27624,plain,
p__d__disjointDecomposition3(c__Entity,c__Physical,c__Abstract),
inference(resolution,[],[f13679,f13420]) ).
fof(f27630,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Abstract)
| p__d__subclass(X0,c__Entity) ),
inference(resolution,[],[f13853,f13402]) ).
fof(f27654,plain,
p__d__disjoint(c__Physical,c__Abstract),
inference(resolution,[],[f13491,f27624]) ).
fof(f27655,plain,
! [X0] :
( ~ p__d__instance(X0,c__Abstract)
| ~ p__d__instance(X0,c__Physical) ),
inference(resolution,[],[f27654,f13405]) ).
fof(f27671,plain,
! [X0,X1] :
( p__d__instance(sK1263(X0),X1)
| ~ p__d__instance(X0,c__PlaneAngleMeasure)
| ~ p__d__subclass(c__Object,X1) ),
inference(resolution,[],[f24207,f13404]) ).
fof(f27682,plain,
p__d__subclass(c__Quantity,c__Entity),
inference(resolution,[],[f13855,f27630]) ).
fof(f27683,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Quantity)
| p__d__subclass(X0,c__Abstract) ),
inference(resolution,[],[f13855,f13402]) ).
fof(f27784,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Quantity)
| p__d__subclass(X0,c__Entity) ),
inference(resolution,[],[f27682,f13402]) ).
fof(f27854,plain,
( ~ p__d__subclass(c__PlaneAngleMeasure,c__Entity)
| sK60(c__PlaneAngleMeasure) = sK1263(sK60(c__PlaneAngleMeasure)) ),
inference(resolution,[],[f13682,f24211]) ).
fof(f27855,plain,
! [X0,X1] :
( p__d__instance(sK60(X0),X1)
| ~ p__d__subclass(X0,c__Entity)
| ~ p__d__subclass(X0,X1) ),
inference(resolution,[],[f13682,f13404]) ).
fof(f27857,definition,
( spl1265_50
<=> sK60(c__PlaneAngleMeasure) = sK1263(sK60(c__PlaneAngleMeasure)) ),
introduced(definition,[new_symbols(definition,[spl1265_50])],[avatar_definition]) ).
fof(f27859,plain,
( sK60(c__PlaneAngleMeasure) = sK1263(sK60(c__PlaneAngleMeasure))
| ~ spl1265_50 ),
inference(avatar_component_clause,[],[f27857]) ).
fof(f27861,definition,
( spl1265_51
<=> p__d__subclass(c__PlaneAngleMeasure,c__Entity) ),
introduced(definition,[new_symbols(definition,[spl1265_51])],[avatar_definition]) ).
fof(f27862,plain,
( p__d__subclass(c__PlaneAngleMeasure,c__Entity)
| ~ spl1265_51 ),
inference(avatar_component_clause,[],[f27861]) ).
fof(f27863,plain,
( ~ p__d__subclass(c__PlaneAngleMeasure,c__Entity)
| spl1265_51 ),
inference(avatar_component_clause,[],[f27861]) ).
fof(f27864,plain,
( spl1265_50
| ~ spl1265_51 ),
inference(avatar_split_clause,[],[f27854,f27861,f27857]) ).
fof(f27932,plain,
p__d__subclass(c__PhysicalQuantity,c__Abstract),
inference(resolution,[],[f14076,f27683]) ).
fof(f28421,plain,
! [X0] :
( ~ p__d__subclass(X0,c__ConstantQuantity)
| p__d__subclass(X0,c__PhysicalQuantity) ),
inference(resolution,[],[f14078,f13402]) ).
fof(f30022,plain,
p__d__subclass(c__PhysicalQuantity,c__Entity),
inference(resolution,[],[f27784,f14076]) ).
fof(f30024,plain,
! [X0] :
( ~ p__d__subclass(X0,c__PhysicalQuantity)
| p__d__subclass(X0,c__Entity) ),
inference(resolution,[],[f30022,f13402]) ).
fof(f33342,plain,
! [X0] :
( ~ p__d__subclass(X0,c__PhysicalQuantity)
| p__d__subclass(X0,c__Abstract) ),
inference(resolution,[],[f27932,f13402]) ).
fof(f33370,plain,
! [X0] :
( ~ p__d__subclass(X0,c__AngleMeasure)
| p__d__subclass(X0,c__ConstantQuantity) ),
inference(resolution,[],[f14819,f13402]) ).
fof(f33382,plain,
p__d__subclass(c__PlaneAngleMeasure,c__ConstantQuantity),
inference(resolution,[],[f33370,f14821]) ).
fof(f33383,plain,
p__d__subclass(c__PlaneAngleMeasure,c__PhysicalQuantity),
inference(resolution,[],[f33382,f28421]) ).
fof(f43222,plain,
p__d__subclass(c__PlaneAngleMeasure,c__Abstract),
inference(resolution,[],[f33383,f33342]) ).
fof(f43223,plain,
p__d__subclass(c__PlaneAngleMeasure,c__Entity),
inference(resolution,[],[f33383,f30024]) ).
fof(f43237,plain,
( $false
| spl1265_51 ),
inference(forward_subsumption_resolution,[],[f43223,f27863]) ).
fof(f43238,plain,
spl1265_51,
inference(avatar_contradiction_clause,[],[f43237]) ).
fof(f43239,plain,
( ! [X0] :
( p__d__instance(sK60(c__PlaneAngleMeasure),X0)
| ~ p__d__instance(sK60(c__PlaneAngleMeasure),c__PlaneAngleMeasure)
| ~ p__d__subclass(c__Object,X0) )
| ~ spl1265_50 ),
inference(superposition,[],[f27671,f27859]) ).
fof(f43243,definition,
( spl1265_2167
<=> p__d__instance(sK60(c__PlaneAngleMeasure),c__PlaneAngleMeasure) ),
introduced(definition,[new_symbols(definition,[spl1265_2167])],[avatar_definition]) ).
fof(f43244,plain,
( p__d__instance(sK60(c__PlaneAngleMeasure),c__PlaneAngleMeasure)
| ~ spl1265_2167 ),
inference(avatar_component_clause,[],[f43243]) ).
fof(f43245,plain,
( ~ p__d__instance(sK60(c__PlaneAngleMeasure),c__PlaneAngleMeasure)
| spl1265_2167 ),
inference(avatar_component_clause,[],[f43243]) ).
fof(f43257,definition,
( spl1265_2170
<=> ! [X0] :
( p__d__instance(sK60(c__PlaneAngleMeasure),X0)
| ~ p__d__subclass(c__Object,X0) ) ),
introduced(definition,[new_symbols(definition,[spl1265_2170])],[avatar_definition]) ).
fof(f43258,plain,
( ! [X0] :
( p__d__instance(sK60(c__PlaneAngleMeasure),X0)
| ~ p__d__subclass(c__Object,X0) )
| ~ spl1265_2170 ),
inference(avatar_component_clause,[],[f43257]) ).
fof(f43259,plain,
( ~ spl1265_2167
| spl1265_2170
| ~ spl1265_50 ),
inference(avatar_split_clause,[],[f43239,f27857,f43257,f43243]) ).
fof(f43262,plain,
( ! [X0] :
( ~ p__d__subclass(X0,c__PlaneAngleMeasure)
| p__d__subclass(X0,c__Entity) )
| ~ spl1265_51 ),
inference(resolution,[],[f27862,f13402]) ).
fof(f43288,plain,
( ~ p__d__subclass(c__PlaneAngleMeasure,c__Entity)
| ~ p__d__subclass(c__PlaneAngleMeasure,c__PlaneAngleMeasure)
| spl1265_2167 ),
inference(resolution,[],[f43245,f27855]) ).
fof(f43289,plain,
( ~ p__d__subclass(c__PlaneAngleMeasure,c__PlaneAngleMeasure)
| ~ spl1265_51
| spl1265_2167 ),
inference(forward_subsumption_resolution,[],[f43288,f43262]) ).
fof(f43292,plain,
( $false
| ~ spl1265_51
| spl1265_2167 ),
inference(forward_subsumption_resolution,[],[f43289,f13401]) ).
fof(f43293,plain,
( ~ spl1265_51
| spl1265_2167 ),
inference(avatar_contradiction_clause,[],[f43292]) ).
fof(f43369,plain,
( ! [X0] :
( p__d__instance(sK60(c__PlaneAngleMeasure),X0)
| ~ p__d__subclass(c__PlaneAngleMeasure,X0) )
| ~ spl1265_2167 ),
inference(resolution,[],[f43244,f13404]) ).
fof(f48128,plain,
( ~ p__d__instance(sK60(c__PlaneAngleMeasure),c__Physical)
| ~ p__d__subclass(c__PlaneAngleMeasure,c__Abstract)
| ~ spl1265_2167 ),
inference(resolution,[],[f27655,f43369]) ).
fof(f48149,plain,
( ~ p__d__instance(sK60(c__PlaneAngleMeasure),c__Physical)
| ~ spl1265_2167 ),
inference(forward_subsumption_resolution,[],[f48128,f43222]) ).
fof(f48151,definition,
( spl1265_2848
<=> p__d__instance(sK60(c__PlaneAngleMeasure),c__Physical) ),
introduced(definition,[new_symbols(definition,[spl1265_2848])],[avatar_definition]) ).
fof(f48153,plain,
( ~ p__d__instance(sK60(c__PlaneAngleMeasure),c__Physical)
| spl1265_2848 ),
inference(avatar_component_clause,[],[f48151]) ).
fof(f48166,plain,
( ~ spl1265_2848
| ~ spl1265_2167 ),
inference(avatar_split_clause,[],[f48149,f43243,f48151]) ).
fof(f48167,plain,
( ~ p__d__subclass(c__Object,c__Physical)
| ~ spl1265_2170
| spl1265_2848 ),
inference(resolution,[],[f48153,f43258]) ).
fof(f48172,plain,
( $false
| ~ spl1265_2170
| spl1265_2848 ),
inference(forward_subsumption_resolution,[],[f48167,f13691]) ).
fof(f48173,plain,
( ~ spl1265_2170
| spl1265_2848 ),
inference(avatar_contradiction_clause,[],[f48172]) ).
cnf(s27,plain,
( spl1265_50
| ~ spl1265_51 ),
inference(sat_conversion,[],[f27864]) ).
cnf(s1121,plain,
spl1265_51,
inference(sat_conversion,[],[f43238]) ).
cnf(s1124,plain,
( ~ spl1265_50
| ~ spl1265_2167
| spl1265_2170 ),
inference(sat_conversion,[],[f43259]) ).
cnf(s1127,plain,
( ~ spl1265_51
| spl1265_2167 ),
inference(sat_conversion,[],[f43293]) ).
cnf(s1517,plain,
( ~ spl1265_2167
| ~ spl1265_2848 ),
inference(sat_conversion,[],[f48166]) ).
cnf(s1518,plain,
( ~ spl1265_2170
| spl1265_2848 ),
inference(sat_conversion,[],[f48173]) ).
cnf(s1519,plain,
spl1265_2167,
inference(rat,[],[s1127,s1121]) ).
cnf(s1520,plain,
~ spl1265_2848,
inference(rat,[],[s1517,s1519]) ).
cnf(s1521,plain,
~ spl1265_2170,
inference(rat,[],[s1518,s1520]) ).
cnf(s1522,plain,
~ spl1265_50,
inference(rat,[],[s1124,s1519,s1521]) ).
cnf(s1537,plain,
$false,
inference(rat,[],[s27,s1121,s1522]) ).
fof(f48174,plain,
$false,
inference(avatar_sat_refutation,[],[s1537]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR269+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.17 % Computer : n007.cluster.edu
% 0.10/0.17 % Model : x86_64 x86_64
% 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.17 % Memory : 8046.5625MB
% 0.10/0.17 % OS : Linux 6.8.0-71-generic
% 0.10/0.17 % CPULimit : 300
% 0.10/0.17 % WCLimit : 300
% 0.10/0.17 % DateTime : Mon Sep 28 23:54:26 UTC 2026
% 0.10/0.17 % CPUTime :
% 0.10/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.20 Running first-order theorem proving
% 0.10/0.20 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
% 10.29/2.25 % (2980216)Detected formulas, will run a generic FOF schedule.
% 10.29/2.25 % (2980225)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1673945124:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 10.29/2.25 % (2980225)Instruction limit reached!
% 10.29/2.25 % (2980225)------------------------------
% 10.29/2.25 % (2980225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.29/2.25 % (2980225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.29/2.25 % (2980225)CaDiCaL version: 2.1.3
% 10.29/2.25 % (2980225)Termination reason: Instruction limit
% 10.29/2.25 % (2980225)Termination phase: Saturation
% 10.29/2.25 % (2980225)Time elapsed: 0.033 s
% 10.29/2.25 % (2980225)Peak memory usage: 93 MB
% 10.29/2.25 % (2980225)Instructions burned: 123 (million)
% 10.29/2.25 % (2980226)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=342779117:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 10.29/2.25 % (2980222)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=3646356914:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 10.29/2.25 % (2980221)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=3730066542:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 10.29/2.25 % (2980224)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=913211487:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 10.29/2.25 % (2980223)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=1793748329:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 10.29/2.25 % (2980227)dis-21_1_sil=8000:lcm=predicate:random_seed=3610357747: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)
% 10.29/2.25 % (2980224)Refutation not found, incomplete strategy
% 10.29/2.25 % (2980224)------------------------------
% 10.29/2.25 % (2980224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.29/2.25 % (2980224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.29/2.25 % (2980224)CaDiCaL version: 2.1.3
% 10.29/2.25 % (2980224)Termination reason: Refutation not found, incomplete strategy
% 10.29/2.25 % (2980224)Time elapsed: 0.017 s
% 10.29/2.25 % (2980224)Peak memory usage: 94 MB
% 10.29/2.25 % (2980224)Instructions burned: 24 (million)
% 10.29/2.25 % (2980229)lrs+10_1_sil=8000:sp=occurrence:random_seed=4092980854:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 10.29/2.25 % (2980227)Instruction limit reached!
% 10.29/2.25 % (2980227)------------------------------
% 10.29/2.25 % (2980227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.29/2.25 % (2980227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.29/2.25 % (2980227)CaDiCaL version: 2.1.3
% 10.29/2.25 % (2980227)Termination reason: Instruction limit
% 10.29/2.25 % (2980227)Termination phase: Saturation
% 10.29/2.25 % (2980227)Time elapsed: 0.077 s
% 10.29/2.25 % (2980227)Peak memory usage: 95 MB
% 10.29/2.25 % (2980227)Instructions burned: 129 (million)
% 10.29/2.25 % (2980226)Instruction limit reached!
% 10.29/2.25 % (2980226)------------------------------
% 10.29/2.25 % (2980226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.29/2.25 % (2980226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.29/2.25 % (2980226)CaDiCaL version: 2.1.3
% 10.29/2.25 % (2980226)Termination reason: Instruction limit
% 10.29/2.25 % (2980226)Termination phase: Preprocessing 3
% 10.29/2.25 % (2980226)Time elapsed: 0.094 s
% 10.29/2.25 % (2980226)Peak memory usage: 94 MB
% 10.29/2.25 % (2980226)Instructions burned: 139 (million)
% 10.29/2.25 % (2980229)Instruction limit reached!
% 10.29/2.25 % (2980229)------------------------------
% 10.29/2.25 % (2980229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.29/2.25 % (2980229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.29/2.25 % (2980229)CaDiCaL version: 2.1.3
% 10.29/2.25 % (2980229)Termination reason: Instruction limit
% 10.29/2.25 % (2980229)Termination phase: Saturation
% 10.29/2.25 % (2980229)Time elapsed: 0.099 s
% 10.29/2.25 % (2980229)Peak memory usage: 97 MB
% 10.29/2.25 % (2980229)Instructions burned: 285 (million)
% 12.70/2.65 % (2980237)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2894936673:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 12.70/2.65 % (2980238)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3161350565:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 12.70/2.65 % (2980238)Refutation not found, incomplete strategy
% 12.70/2.65 % (2980238)------------------------------
% 12.70/2.65 % (2980238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.70/2.65 % (2980238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.70/2.65 % (2980238)CaDiCaL version: 2.1.3
% 12.70/2.65 % (2980238)Termination reason: Refutation not found, incomplete strategy
% 12.70/2.65 % (2980238)Time elapsed: 0.018 s
% 12.70/2.65 % (2980238)Peak memory usage: 94 MB
% 12.70/2.65 % (2980238)Instructions burned: 22 (million)
% 12.70/2.65 % (2980237)Refutation not found, incomplete strategy
% 12.70/2.65 % (2980237)------------------------------
% 12.70/2.65 % (2980237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.70/2.65 % (2980237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.70/2.65 % (2980237)CaDiCaL version: 2.1.3
% 12.70/2.65 % (2980237)Termination reason: Refutation not found, incomplete strategy
% 12.70/2.65 % (2980237)Time elapsed: 0.032 s
% 12.70/2.65 % (2980237)Peak memory usage: 94 MB
% 12.70/2.65 % (2980237)Instructions burned: 61 (million)
% 12.70/2.65 % (2980224)------------------------------
% 12.70/2.65 % (2980224)------------------------------
% 12.70/2.65 % (2980239)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=507967388:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 12.70/2.65 % (2980239)Instruction limit reached!
% 12.70/2.65 % (2980239)------------------------------
% 12.70/2.65 % (2980239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.70/2.65 % (2980239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.70/2.65 % (2980239)CaDiCaL version: 2.1.3
% 12.70/2.65 % (2980239)Termination reason: Instruction limit
% 12.70/2.65 % (2980239)Termination phase: Saturation
% 12.70/2.65 % (2980239)Time elapsed: 0.078 s
% 12.70/2.65 % (2980239)Peak memory usage: 98 MB
% 12.70/2.65 % (2980239)Instructions burned: 251 (million)
% 12.70/2.65 % (2980243)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3670219381:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 12.70/2.65 % (2980243)Refutation not found, incomplete strategy
% 12.70/2.65 % (2980243)------------------------------
% 12.70/2.65 % (2980243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.70/2.65 % (2980243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.70/2.65 % (2980243)CaDiCaL version: 2.1.3
% 12.70/2.65 % (2980243)Termination reason: Refutation not found, incomplete strategy
% 12.70/2.65 % (2980243)Time elapsed: 0.025 s
% 12.70/2.65 % (2980243)Peak memory usage: 94 MB
% 12.70/2.65 % (2980243)Instructions burned: 36 (million)
% 12.70/2.65 % (2980244)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1908153953:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 12.70/2.65 % (2980238)------------------------------
% 12.70/2.65 % (2980238)------------------------------
% 12.70/2.65 % (2980237)------------------------------
% 12.70/2.65 % (2980237)------------------------------
% 12.70/2.65 % (2980248)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=887460575:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 12.70/2.65 % (2980247)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1392532840:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 12.70/2.65 % (2980243)------------------------------
% 12.70/2.65 % (2980243)------------------------------
% 12.70/2.65 % (2980247)Instruction limit reached!
% 12.70/2.65 % (2980247)------------------------------
% 12.70/2.65 % (2980247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.70/2.65 % (2980247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.70/2.65 % (2980247)CaDiCaL version: 2.1.3
% 12.70/2.65 % (2980247)Termination reason: Instruction limit
% 12.70/2.65 % (2980247)Termination phase: Saturation
% 12.70/2.65 % (2980247)Time elapsed: 0.063 s
% 12.70/2.65 % (2980247)Peak memory usage: 94 MB
% 12.70/2.65 % (2980247)Instructions burned: 113 (million)
% 12.70/2.65 % (2980223)Refutation not found, incomplete strategy
% 31.71/5.25 % (2980223)------------------------------
% 31.71/5.25 % (2980223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.71/5.25 % (2980223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.71/5.25 % (2980223)CaDiCaL version: 2.1.3
% 31.71/5.25 % (2980223)Termination reason: Refutation not found, incomplete strategy
% 31.71/5.25 % (2980223)Time elapsed: 0.691 s
% 31.71/5.25 % (2980223)Peak memory usage: 144 MB
% 31.71/5.25 % (2980223)Instructions burned: 1028 (million)
% 31.71/5.25 % (2980248)Instruction limit reached!
% 31.71/5.25 % (2980248)------------------------------
% 31.71/5.25 % (2980248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.71/5.25 % (2980248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.71/5.25 % (2980248)CaDiCaL version: 2.1.3
% 31.71/5.25 % (2980248)Termination reason: Instruction limit
% 31.71/5.25 % (2980248)Termination phase: Property scanning
% 31.71/5.25 % (2980248)Time elapsed: 0.077 s
% 31.71/5.25 % (2980248)Peak memory usage: 96 MB
% 31.71/5.25 % (2980248)Instructions burned: 128 (million)
% 31.71/5.25 % (2980251)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2212260662:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 31.71/5.25 % (2980252)lrs+10_1_sil=8000:sp=occurrence:random_seed=3089391810:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 31.71/5.25 % (2980253)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2760990854:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 31.71/5.25 % (2980253)Refutation not found, incomplete strategy
% 31.71/5.25 % (2980253)------------------------------
% 31.71/5.25 % (2980253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.71/5.25 % (2980253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.71/5.25 % (2980253)CaDiCaL version: 2.1.3
% 31.71/5.25 % (2980253)Termination reason: Refutation not found, incomplete strategy
% 31.71/5.25 % (2980253)Time elapsed: 0.016 s
% 31.71/5.25 % (2980253)Peak memory usage: 94 MB
% 31.71/5.25 % (2980253)Instructions burned: 20 (million)
% 31.71/5.25 % (2980251)Instruction limit reached!
% 31.71/5.25 % (2980251)------------------------------
% 31.71/5.25 % (2980251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.71/5.25 % (2980251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.71/5.25 % (2980251)CaDiCaL version: 2.1.3
% 31.71/5.25 % (2980251)Termination reason: Instruction limit
% 31.71/5.25 % (2980251)Termination phase: Property scanning
% 31.71/5.25 % (2980251)Time elapsed: 0.062 s
% 31.71/5.25 % (2980251)Peak memory usage: 92 MB
% 31.71/5.25 % (2980251)Instructions burned: 116 (million)
% 31.71/5.25 % (2980223)------------------------------
% 31.71/5.25 % (2980223)------------------------------
% 31.71/5.25 % (2980257)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2739055777:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 31.71/5.25 % (2980258)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1461008756:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 31.71/5.25 % (2980253)------------------------------
% 31.71/5.25 % (2980253)------------------------------
% 31.71/5.25 % (2980258)Refutation not found, incomplete strategy
% 31.71/5.25 % (2980258)------------------------------
% 31.71/5.25 % (2980258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.71/5.25 % (2980258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.71/5.25 % (2980258)CaDiCaL version: 2.1.3
% 31.71/5.25 % (2980258)Termination reason: Refutation not found, incomplete strategy
% 31.71/5.25 % (2980258)Time elapsed: 0.019 s
% 31.71/5.25 % (2980258)Peak memory usage: 94 MB
% 31.71/5.25 % (2980258)Instructions burned: 24 (million)
% 31.71/5.25 % (2980261)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1211967137:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 31.71/5.25 % (2980244)Instruction limit reached!
% 31.71/5.25 % (2980244)------------------------------
% 31.71/5.25 % (2980244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.71/5.25 % (2980244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.71/5.25 % (2980244)CaDiCaL version: 2.1.3
% 31.71/5.25 % (2980244)Termination reason: Instruction limit
% 31.71/5.25 % (2980244)Termination phase: Saturation
% 36.07/6.04 % (2980244)Time elapsed: 0.854 s
% 36.07/6.04 % (2980244)Peak memory usage: 213 MB
% 36.07/6.04 % (2980244)Instructions burned: 2350 (million)
% 36.07/6.04 % (2980252)Instruction limit reached!
% 36.07/6.04 % (2980252)------------------------------
% 36.07/6.04 % (2980252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.07/6.04 % (2980252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/6.04 % (2980252)CaDiCaL version: 2.1.3
% 36.07/6.04 % (2980252)Termination reason: Instruction limit
% 36.07/6.04 % (2980252)Termination phase: Saturation
% 36.07/6.04 % (2980252)Time elapsed: 0.514 s
% 36.07/6.04 % (2980252)Peak memory usage: 104 MB
% 36.07/6.04 % (2980252)Instructions burned: 908 (million)
% 36.07/6.04 % (2980258)------------------------------
% 36.07/6.04 % (2980258)------------------------------
% 36.07/6.04 % (2980263)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2203452186:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 36.07/6.04 % (2980264)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=1984806285:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 36.07/6.04 % (2980265)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=361330716:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 36.07/6.04 % (2980264)Instruction limit reached!
% 36.07/6.04 % (2980264)------------------------------
% 36.07/6.04 % (2980264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.07/6.04 % (2980264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/6.04 % (2980264)CaDiCaL version: 2.1.3
% 36.07/6.04 % (2980264)Termination reason: Instruction limit
% 36.07/6.04 % (2980264)Termination phase: Preprocessing 3
% 36.07/6.04 % (2980264)Time elapsed: 0.076 s
% 36.07/6.04 % (2980264)Peak memory usage: 93 MB
% 36.07/6.04 % (2980264)Instructions burned: 127 (million)
% 36.07/6.04 % (2980261)Instruction limit reached!
% 36.07/6.04 % (2980261)------------------------------
% 36.07/6.04 % (2980261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.07/6.04 % (2980261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/6.04 % (2980261)CaDiCaL version: 2.1.3
% 36.07/6.04 % (2980261)Termination reason: Instruction limit
% 36.07/6.04 % (2980261)Termination phase: Saturation
% 36.07/6.04 % (2980261)Time elapsed: 0.303 s
% 36.07/6.04 % (2980261)Peak memory usage: 100 MB
% 36.07/6.04 % (2980261)Instructions burned: 593 (million)
% 36.07/6.04 % (2980265)Instruction limit reached!
% 36.07/6.04 % (2980265)------------------------------
% 36.07/6.04 % (2980265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.07/6.04 % (2980265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/6.04 % (2980265)CaDiCaL version: 2.1.3
% 36.07/6.04 % (2980265)Termination reason: Instruction limit
% 36.07/6.04 % (2980265)Termination phase: Preprocessing 2
% 36.07/6.04 % (2980265)Time elapsed: 0.067 s
% 36.07/6.04 % (2980265)Peak memory usage: 92 MB
% 36.07/6.04 % (2980265)Instructions burned: 134 (million)
% 36.07/6.04 % (2980270)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=802341439:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2981 on theBenchmark for (2981ds/431Mi)
% 36.07/6.04 % (2980269)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1823939045:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/141Mi)
% 36.07/6.04 % (2980271)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=3997561496:i=6060:aac=none:ins=25_2981 on theBenchmark for (2981ds/6060Mi)
% 36.07/6.04 % (2980269)Refutation not found, incomplete strategy
% 36.07/6.04 % (2980269)------------------------------
% 36.07/6.04 % (2980269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.07/6.04 % (2980269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/6.04 % (2980269)CaDiCaL version: 2.1.3
% 36.07/6.04 % (2980269)Termination reason: Refutation not found, incomplete strategy
% 36.07/6.04 % (2980269)Time elapsed: 0.017 s
% 36.07/6.04 % (2980269)Peak memory usage: 94 MB
% 36.07/6.04 % (2980269)Instructions burned: 24 (million)
% 36.07/6.04 % (2980270)Refutation not found, incomplete strategy
% 36.07/6.04 % (2980270)------------------------------
% 36.07/6.04 % (2980270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.07/6.04 % (2980270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/6.04 % (2980270)CaDiCaL version: 2.1.3
% 36.07/6.04 % (2980270)Termination reason: Refutation not found, incomplete strategy
% 36.07/6.04 % (2980270)Time elapsed: 0.024 s
% 36.07/6.04 % (2980270)Peak memory usage: 94 MB
% 36.07/6.04 % (2980270)Instructions burned: 34 (million)
% 36.07/6.04 % (2980269)------------------------------
% 36.07/6.04 % (2980269)------------------------------
% 36.07/6.04 % (2980270)------------------------------
% 36.07/6.04 % (2980270)------------------------------
% 36.07/6.04 % (2980275)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=2388922085:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2977 on theBenchmark for (2977ds/150Mi)
% 36.07/6.04 % (2980276)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1752476089:i=14155:bd=all_2977 on theBenchmark for (2977ds/14155Mi)
% 36.07/6.04 % (2980275)Instruction limit reached!
% 36.07/6.04 % (2980275)------------------------------
% 36.07/6.04 % (2980275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.07/6.04 % (2980275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/6.04 % (2980275)CaDiCaL version: 2.1.3
% 36.07/6.04 % (2980275)Termination reason: Instruction limit
% 36.07/6.04 % (2980275)Termination phase: Property scanning
% 36.07/6.04 % (2980275)Time elapsed: 0.092 s
% 36.07/6.04 % (2980275)Peak memory usage: 96 MB
% 36.07/6.04 % (2980275)Instructions burned: 152 (million)
% 36.07/6.04 % (2980279)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1883277168:i=667:av=off:fsr=off_2975 on theBenchmark for (2975ds/667Mi)
% 36.07/6.04 % (2980279)Instruction limit reached!
% 36.07/6.04 % (2980279)------------------------------
% 36.07/6.04 % (2980279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.07/6.04 % (2980279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/6.04 % (2980279)CaDiCaL version: 2.1.3
% 36.07/6.04 % (2980279)Termination reason: Instruction limit
% 36.07/6.04 % (2980279)Termination phase: Saturation
% 36.07/6.04 % (2980279)Time elapsed: 0.353 s
% 36.07/6.04 % (2980279)Peak memory usage: 105 MB
% 36.07/6.04 % (2980279)Instructions burned: 669 (million)
% 36.07/6.04 % (2980281)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=1574081109:s2a=on:i=185:s2at=1.8:fdi=4_2970 on theBenchmark for (2970ds/185Mi)
% 36.07/6.04 % (2980281)Instruction limit reached!
% 36.07/6.04 % (2980281)------------------------------
% 36.07/6.04 % (2980281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.07/6.04 % (2980281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/6.04 % (2980281)CaDiCaL version: 2.1.3
% 36.07/6.04 % (2980281)Termination reason: Instruction limit
% 36.07/6.04 % (2980281)Termination phase: Property scanning
% 36.07/6.04 % (2980281)Time elapsed: 0.119 s
% 36.07/6.04 % (2980281)Peak memory usage: 97 MB
% 36.07/6.04 % (2980281)Instructions burned: 185 (million)
% 36.07/6.04 % (2980283)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3478026822:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2967 on theBenchmark for (2967ds/193Mi)
% 36.07/6.04 % (2980283)Instruction limit reached!
% 36.07/6.04 % (2980283)------------------------------
% 36.07/6.04 % (2980283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.07/6.04 % (2980283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/6.04 % (2980283)CaDiCaL version: 2.1.3
% 36.07/6.04 % (2980283)Termination reason: Instruction limit
% 36.07/6.04 % (2980283)Termination phase: Saturation
% 36.07/6.04 % (2980283)Time elapsed: 0.107 s
% 36.07/6.04 % (2980283)Peak memory usage: 95 MB
% 36.07/6.04 % (2980283)Instructions burned: 193 (million)
% 36.07/6.04 % (2980285)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=202812557:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2965 on theBenchmark for (2965ds/4850Mi)
% 36.07/6.04 % (2980257)Instruction limit reached!
% 36.07/6.04 % (2980257)------------------------------
% 36.07/6.04 % (2980257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.07/6.04 % (2980257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.07/6.04 % (2980257)CaDiCaL version: 2.1.3
% 36.07/6.04 % (2980257)Termination reason: Instruction limit
% 36.07/6.04 % (2980257)Termination phase: Saturation
% 36.07/6.04 % (2980257)Time elapsed: 3.281 s
% 36.07/6.04 % (2980257)Peak memory usage: 226 MB
% 36.07/6.04 % (2980257)Instructions burned: 5203 (million)
% 36.07/6.04 % (2980287)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=4127452198:i=12111:sd=1:ss=included_2953 on theBenchmark for (2953ds/12111Mi)
% 36.07/6.04 % (2980221)First to succeed.
% 36.07/6.04 % (2980221)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2980216"
% 36.07/6.04 % (2980221)Refutation found. Thanks to Tanya!
% 36.07/6.04 % SZS status Theorem for theBenchmark
% 36.07/6.04 % SZS output start Proof for theBenchmark
% See solution above
% 37.73/6.23 % (2980221)------------------------------
% 37.73/6.23 % (2980221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.73/6.23 % (2980221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.73/6.23 % (2980221)CaDiCaL version: 2.1.3
% 37.73/6.23 % (2980221)Termination reason: Refutation
% 37.73/6.23 % (2980221)Time elapsed: 4.782 s
% 37.73/6.23 % (2980221)Peak memory usage: 238 MB
% 37.73/6.23 % (2980221)Instructions burned: 7637 (million)
% 37.73/6.23 % (2980221)------------------------------
% 37.73/6.23 % (2980221)------------------------------
% 37.73/6.23 % (2980216)Success in time 5.387 s
% 37.73/6.23 % Vampire exiting
%------------------------------------------------------------------------------