%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR216+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.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:06 AM UTC 2026
% Result : Theorem 18.60s 3.55s
% Output : Refutation 20.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 31
% Syntax : Number of formulae : 121 ( 31 unt; 17 def)
% Number of atoms : 720 ( 6 equ)
% Maximal formula atoms : 50 ( 5 avg)
% Number of connectives : 992 ( 393 ~; 316 |; 215 &)
% ( 26 <=>; 42 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 25 ( 23 usr; 4 prp; 0-4 aty)
% Number of functors : 14 ( 14 usr; 11 con; 0-2 aty)
% Number of variables : 311 ( 0 sgn 299 !; 12 ?)
% 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/sandbox/benchmark/theBenchmark.p',predefinitionsA8) ).
fof(f4,axiom,
! [X0,X1,X2] :
( ( p__d__instance(X0,X1)
& p__d__subclass(X1,X2) )
=> p__d__instance(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',predefinitionsA12) ).
fof(f61,axiom,
( ! [X0,X1] :
( ( p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Attribute) )
=> ( p__contraryAttribute2(X0,X1)
<=> ( ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X0) )
=> ~ p__attribute(X2,X1) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X1) )
=> ~ p__attribute(X2,X0) ) ) ) )
& ! [X0,X1,X3,X4] :
( ( p__d__instance(X4,c__Attribute)
& p__d__instance(X3,c__Attribute)
& p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Attribute) )
=> ( p__contraryAttribute4(X0,X1,X3,X4)
<=> ( ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X0) )
=> ~ p__attribute(X2,X1) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X1) )
=> ~ p__attribute(X2,X0) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X0) )
=> ~ p__attribute(X2,X3) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X3) )
=> ~ p__attribute(X2,X0) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X0) )
=> ~ p__attribute(X2,X4) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X4) )
=> ~ p__attribute(X2,X0) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X1) )
=> ~ p__attribute(X2,X3) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X3) )
=> ~ p__attribute(X2,X1) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X1) )
=> ~ p__attribute(X2,X4) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X4) )
=> ~ p__attribute(X2,X1) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X3) )
=> ~ p__attribute(X2,X4) )
& ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X4) )
=> ~ p__attribute(X2,X3) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA90) ).
fof(f88,axiom,
! [X0,X1,X2] :
( ( p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Attribute)
& p__d__instance(X2,c__Object)
& p__subAttribute(X0,X1)
& p__attribute(X2,X0) )
=> p__attribute(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA140) ).
fof(f89,axiom,
! [X0,X1,X2] :
( ( p__subAttribute(X1,X2)
& p__d__instance(X2,X0) )
=> p__d__instance(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA141) ).
fof(f254,axiom,
p__d__subclass(c__InternalAttribute,c__Attribute),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA351) ).
fof(f2583,axiom,
p__d__subclass(c__PhysicalState,c__InternalAttribute),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA3560) ).
fof(f2584,axiom,
p__contraryAttribute4(c__Solid,c__Liquid,c__Gas,c__Plasma),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA3561) ).
fof(f2585,axiom,
p__d__instance(c__Solid,c__PhysicalState),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA3563) ).
fof(f2591,axiom,
p__subAttribute(c__Gas,c__Fluid),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA3569) ).
fof(f2594,axiom,
p__subAttribute(c__Plasma,c__Fluid),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA3572) ).
fof(f6855,axiom,
! [X0,X1] :
( p__subAttribute(X0,X1)
=> ( p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Attribute) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',typeA2) ).
fof(f6921,axiom,
! [X0,X1] :
( p__attribute(X0,X1)
=> ( p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Object) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',typeA68) ).
fof(f7433,conjecture,
! [X0,X1] :
( ( p__d__instance(X1,c__Object)
& p__d__instance(X0,c__Object) )
=> ( ( p__attribute(X1,c__Gas)
& p__attribute(X0,c__Liquid) )
=> X0 != X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antonymPattern10048) ).
fof(f7434,negated_conjecture,
~ ! [X0,X1] :
( ( p__d__instance(X1,c__Object)
& p__d__instance(X0,c__Object) )
=> ( ( p__attribute(X1,c__Gas)
& p__attribute(X0,c__Liquid) )
=> X0 != X1 ) ),
inference(negated_conjecture,[status(cth)],[f7433]) ).
fof(f7435,plain,
( ! [X0,X1] :
( ( p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Attribute) )
=> ( p__contraryAttribute2(X0,X1)
<=> ( ! [X2] :
( ( p__d__instance(X2,c__Object)
& p__attribute(X2,X0) )
=> ~ p__attribute(X2,X1) )
& ! [X3] :
( ( p__d__instance(X3,c__Object)
& p__attribute(X3,X1) )
=> ~ p__attribute(X3,X0) ) ) ) )
& ! [X4,X5,X6,X7] :
( ( p__d__instance(X7,c__Attribute)
& p__d__instance(X6,c__Attribute)
& p__d__instance(X5,c__Attribute)
& p__d__instance(X4,c__Attribute) )
=> ( p__contraryAttribute4(X4,X5,X6,X7)
<=> ( ! [X8] :
( ( p__d__instance(X8,c__Object)
& p__attribute(X8,X4) )
=> ~ p__attribute(X8,X5) )
& ! [X9] :
( ( p__d__instance(X9,c__Object)
& p__attribute(X9,X5) )
=> ~ p__attribute(X9,X4) )
& ! [X10] :
( ( p__d__instance(X10,c__Object)
& p__attribute(X10,X4) )
=> ~ p__attribute(X10,X6) )
& ! [X11] :
( ( p__d__instance(X11,c__Object)
& p__attribute(X11,X6) )
=> ~ p__attribute(X11,X4) )
& ! [X12] :
( ( p__d__instance(X12,c__Object)
& p__attribute(X12,X4) )
=> ~ p__attribute(X12,X7) )
& ! [X13] :
( ( p__d__instance(X13,c__Object)
& p__attribute(X13,X7) )
=> ~ p__attribute(X13,X4) )
& ! [X14] :
( ( p__d__instance(X14,c__Object)
& p__attribute(X14,X5) )
=> ~ p__attribute(X14,X6) )
& ! [X15] :
( ( p__d__instance(X15,c__Object)
& p__attribute(X15,X6) )
=> ~ p__attribute(X15,X5) )
& ! [X16] :
( ( p__d__instance(X16,c__Object)
& p__attribute(X16,X5) )
=> ~ p__attribute(X16,X7) )
& ! [X17] :
( ( p__d__instance(X17,c__Object)
& p__attribute(X17,X7) )
=> ~ p__attribute(X17,X5) )
& ! [X18] :
( ( p__d__instance(X18,c__Object)
& p__attribute(X18,X6) )
=> ~ p__attribute(X18,X7) )
& ! [X19] :
( ( p__d__instance(X19,c__Object)
& p__attribute(X19,X7) )
=> ~ p__attribute(X19,X6) ) ) ) ) ),
inference(rectify,[],[f61]) ).
fof(f7453,plain,
? [X0,X1] :
( X0 = X1
& p__attribute(X1,c__Gas)
& p__attribute(X0,c__Liquid)
& p__d__instance(X1,c__Object)
& p__d__instance(X0,c__Object) ),
inference(ennf_transformation,[],[f7434]) ).
fof(f7454,plain,
? [X0,X1] :
( X0 = X1
& p__attribute(X1,c__Gas)
& p__attribute(X0,c__Liquid)
& p__d__instance(X1,c__Object)
& p__d__instance(X0,c__Object) ),
inference(flattening,[],[f7453]) ).
fof(f7457,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f7458,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7457]) ).
fof(f7471,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f7472,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7471]) ).
fof(f7475,plain,
! [X0,X1] :
( ( p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Attribute) )
| ~ p__subAttribute(X0,X1) ),
inference(ennf_transformation,[],[f6855]) ).
fof(f7476,plain,
! [X0,X1,X2] :
( p__d__instance(X1,X0)
| ~ p__subAttribute(X1,X2)
| ~ p__d__instance(X2,X0) ),
inference(ennf_transformation,[],[f89]) ).
fof(f7477,plain,
! [X0,X1,X2] :
( p__d__instance(X1,X0)
| ~ p__subAttribute(X1,X2)
| ~ p__d__instance(X2,X0) ),
inference(flattening,[],[f7476]) ).
fof(f7478,plain,
! [X0,X1,X2] :
( p__attribute(X2,X1)
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute)
| ~ p__d__instance(X2,c__Object)
| ~ p__subAttribute(X0,X1)
| ~ p__attribute(X2,X0) ),
inference(ennf_transformation,[],[f88]) ).
fof(f7479,plain,
! [X0,X1,X2] :
( p__attribute(X2,X1)
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute)
| ~ p__d__instance(X2,c__Object)
| ~ p__subAttribute(X0,X1)
| ~ p__attribute(X2,X0) ),
inference(flattening,[],[f7478]) ).
fof(f7501,plain,
( ! [X0,X1] :
( ( p__contraryAttribute2(X0,X1)
<=> ( ! [X2] :
( ~ p__attribute(X2,X1)
| ~ p__d__instance(X2,c__Object)
| ~ p__attribute(X2,X0) )
& ! [X3] :
( ~ p__attribute(X3,X0)
| ~ p__d__instance(X3,c__Object)
| ~ p__attribute(X3,X1) ) ) )
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute) )
& ! [X4,X5,X6,X7] :
( ( p__contraryAttribute4(X4,X5,X6,X7)
<=> ( ! [X8] :
( ~ p__attribute(X8,X5)
| ~ p__d__instance(X8,c__Object)
| ~ p__attribute(X8,X4) )
& ! [X9] :
( ~ p__attribute(X9,X4)
| ~ p__d__instance(X9,c__Object)
| ~ p__attribute(X9,X5) )
& ! [X10] :
( ~ p__attribute(X10,X6)
| ~ p__d__instance(X10,c__Object)
| ~ p__attribute(X10,X4) )
& ! [X11] :
( ~ p__attribute(X11,X4)
| ~ p__d__instance(X11,c__Object)
| ~ p__attribute(X11,X6) )
& ! [X12] :
( ~ p__attribute(X12,X7)
| ~ p__d__instance(X12,c__Object)
| ~ p__attribute(X12,X4) )
& ! [X13] :
( ~ p__attribute(X13,X4)
| ~ p__d__instance(X13,c__Object)
| ~ p__attribute(X13,X7) )
& ! [X14] :
( ~ p__attribute(X14,X6)
| ~ p__d__instance(X14,c__Object)
| ~ p__attribute(X14,X5) )
& ! [X15] :
( ~ p__attribute(X15,X5)
| ~ p__d__instance(X15,c__Object)
| ~ p__attribute(X15,X6) )
& ! [X16] :
( ~ p__attribute(X16,X7)
| ~ p__d__instance(X16,c__Object)
| ~ p__attribute(X16,X5) )
& ! [X17] :
( ~ p__attribute(X17,X5)
| ~ p__d__instance(X17,c__Object)
| ~ p__attribute(X17,X7) )
& ! [X18] :
( ~ p__attribute(X18,X7)
| ~ p__d__instance(X18,c__Object)
| ~ p__attribute(X18,X6) )
& ! [X19] :
( ~ p__attribute(X19,X6)
| ~ p__d__instance(X19,c__Object)
| ~ p__attribute(X19,X7) ) ) )
| ~ p__d__instance(X7,c__Attribute)
| ~ p__d__instance(X6,c__Attribute)
| ~ p__d__instance(X5,c__Attribute)
| ~ p__d__instance(X4,c__Attribute) ) ),
inference(ennf_transformation,[],[f7435]) ).
fof(f7502,plain,
( ! [X0,X1] :
( ( p__contraryAttribute2(X0,X1)
<=> ( ! [X2] :
( ~ p__attribute(X2,X1)
| ~ p__d__instance(X2,c__Object)
| ~ p__attribute(X2,X0) )
& ! [X3] :
( ~ p__attribute(X3,X0)
| ~ p__d__instance(X3,c__Object)
| ~ p__attribute(X3,X1) ) ) )
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute) )
& ! [X4,X5,X6,X7] :
( ( p__contraryAttribute4(X4,X5,X6,X7)
<=> ( ! [X8] :
( ~ p__attribute(X8,X5)
| ~ p__d__instance(X8,c__Object)
| ~ p__attribute(X8,X4) )
& ! [X9] :
( ~ p__attribute(X9,X4)
| ~ p__d__instance(X9,c__Object)
| ~ p__attribute(X9,X5) )
& ! [X10] :
( ~ p__attribute(X10,X6)
| ~ p__d__instance(X10,c__Object)
| ~ p__attribute(X10,X4) )
& ! [X11] :
( ~ p__attribute(X11,X4)
| ~ p__d__instance(X11,c__Object)
| ~ p__attribute(X11,X6) )
& ! [X12] :
( ~ p__attribute(X12,X7)
| ~ p__d__instance(X12,c__Object)
| ~ p__attribute(X12,X4) )
& ! [X13] :
( ~ p__attribute(X13,X4)
| ~ p__d__instance(X13,c__Object)
| ~ p__attribute(X13,X7) )
& ! [X14] :
( ~ p__attribute(X14,X6)
| ~ p__d__instance(X14,c__Object)
| ~ p__attribute(X14,X5) )
& ! [X15] :
( ~ p__attribute(X15,X5)
| ~ p__d__instance(X15,c__Object)
| ~ p__attribute(X15,X6) )
& ! [X16] :
( ~ p__attribute(X16,X7)
| ~ p__d__instance(X16,c__Object)
| ~ p__attribute(X16,X5) )
& ! [X17] :
( ~ p__attribute(X17,X5)
| ~ p__d__instance(X17,c__Object)
| ~ p__attribute(X17,X7) )
& ! [X18] :
( ~ p__attribute(X18,X7)
| ~ p__d__instance(X18,c__Object)
| ~ p__attribute(X18,X6) )
& ! [X19] :
( ~ p__attribute(X19,X6)
| ~ p__d__instance(X19,c__Object)
| ~ p__attribute(X19,X7) ) ) )
| ~ p__d__instance(X7,c__Attribute)
| ~ p__d__instance(X6,c__Attribute)
| ~ p__d__instance(X5,c__Attribute)
| ~ p__d__instance(X4,c__Attribute) ) ),
inference(flattening,[],[f7501]) ).
fof(f7525,plain,
! [X0,X1] :
( ( p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Object) )
| ~ p__attribute(X0,X1) ),
inference(ennf_transformation,[],[f6921]) ).
fof(f7623,definition,
! [X6,X7] :
( sP0(X6,X7)
<=> ! [X19] :
( ~ p__attribute(X19,X6)
| ~ p__d__instance(X19,c__Object)
| ~ p__attribute(X19,X7) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f7624,definition,
! [X7,X6] :
( sP1(X7,X6)
<=> ! [X18] :
( ~ p__attribute(X18,X7)
| ~ p__d__instance(X18,c__Object)
| ~ p__attribute(X18,X6) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f7625,definition,
! [X5,X7] :
( sP2(X5,X7)
<=> ! [X17] :
( ~ p__attribute(X17,X5)
| ~ p__d__instance(X17,c__Object)
| ~ p__attribute(X17,X7) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f7626,definition,
! [X7,X5] :
( sP3(X7,X5)
<=> ! [X16] :
( ~ p__attribute(X16,X7)
| ~ p__d__instance(X16,c__Object)
| ~ p__attribute(X16,X5) ) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f7627,definition,
! [X5,X6] :
( sP4(X5,X6)
<=> ! [X15] :
( ~ p__attribute(X15,X5)
| ~ p__d__instance(X15,c__Object)
| ~ p__attribute(X15,X6) ) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f7628,definition,
! [X6,X5] :
( sP5(X6,X5)
<=> ! [X14] :
( ~ p__attribute(X14,X6)
| ~ p__d__instance(X14,c__Object)
| ~ p__attribute(X14,X5) ) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f7629,definition,
! [X4,X7] :
( sP6(X4,X7)
<=> ! [X13] :
( ~ p__attribute(X13,X4)
| ~ p__d__instance(X13,c__Object)
| ~ p__attribute(X13,X7) ) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f7630,definition,
! [X7,X4] :
( sP7(X7,X4)
<=> ! [X12] :
( ~ p__attribute(X12,X7)
| ~ p__d__instance(X12,c__Object)
| ~ p__attribute(X12,X4) ) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f7631,definition,
! [X4,X6] :
( sP8(X4,X6)
<=> ! [X11] :
( ~ p__attribute(X11,X4)
| ~ p__d__instance(X11,c__Object)
| ~ p__attribute(X11,X6) ) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f7632,definition,
! [X6,X4] :
( sP9(X6,X4)
<=> ! [X10] :
( ~ p__attribute(X10,X6)
| ~ p__d__instance(X10,c__Object)
| ~ p__attribute(X10,X4) ) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f7633,definition,
! [X4,X5] :
( sP10(X4,X5)
<=> ! [X9] :
( ~ p__attribute(X9,X4)
| ~ p__d__instance(X9,c__Object)
| ~ p__attribute(X9,X5) ) ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f7634,definition,
! [X5,X4,X6,X7] :
( sP11(X5,X4,X6,X7)
<=> ( ! [X8] :
( ~ p__attribute(X8,X5)
| ~ p__d__instance(X8,c__Object)
| ~ p__attribute(X8,X4) )
& sP10(X4,X5)
& sP9(X6,X4)
& sP8(X4,X6)
& sP7(X7,X4)
& sP6(X4,X7)
& sP5(X6,X5)
& sP4(X5,X6)
& sP3(X7,X5)
& sP2(X5,X7)
& sP1(X7,X6)
& sP0(X6,X7) ) ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f7635,definition,
! [X7,X6,X4,X5] :
( ( p__contraryAttribute4(X4,X5,X6,X7)
<=> sP11(X5,X4,X6,X7) )
| ~ sP12(X7,X6,X4,X5) ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f7636,definition,
! [X0,X1] :
( sP13(X0,X1)
<=> ! [X3] :
( ~ p__attribute(X3,X0)
| ~ p__d__instance(X3,c__Object)
| ~ p__attribute(X3,X1) ) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f7637,plain,
( ! [X0,X1] :
( ( p__contraryAttribute2(X0,X1)
<=> ( ! [X2] :
( ~ p__attribute(X2,X1)
| ~ p__d__instance(X2,c__Object)
| ~ p__attribute(X2,X0) )
& sP13(X0,X1) ) )
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute) )
& ! [X4,X5,X6,X7] :
( sP12(X7,X6,X4,X5)
| ~ p__d__instance(X7,c__Attribute)
| ~ p__d__instance(X6,c__Attribute)
| ~ p__d__instance(X5,c__Attribute)
| ~ p__d__instance(X4,c__Attribute) ) ),
inference(definition_folding,[],[f7502,f7636,f7635,f7634,f7633,f7632,f7631,f7630,f7629,f7628,f7627,f7626,f7625,f7624,f7623]) ).
fof(f7640,plain,
( sK15 = sK16
& p__attribute(sK16,c__Gas)
& p__attribute(sK15,c__Liquid)
& p__d__instance(sK16,c__Object)
& p__d__instance(sK15,c__Object) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16]),skolemize(X0,sK15),skolemize(X1,sK16)],[f7454]) ).
fof(f7658,plain,
! [X7,X6,X4,X5] :
( ( ( p__contraryAttribute4(X4,X5,X6,X7)
| ~ sP11(X5,X4,X6,X7) )
& ( sP11(X5,X4,X6,X7)
| ~ p__contraryAttribute4(X4,X5,X6,X7) ) )
| ~ sP12(X7,X6,X4,X5) ),
inference(nnf_transformation,[],[f7635]) ).
fof(f7659,plain,
! [X0,X1,X2,X3] :
( ( ( p__contraryAttribute4(X2,X3,X1,X0)
| ~ sP11(X3,X2,X1,X0) )
& ( sP11(X3,X2,X1,X0)
| ~ p__contraryAttribute4(X2,X3,X1,X0) ) )
| ~ sP12(X0,X1,X2,X3) ),
inference(rectify,[],[f7658]) ).
fof(f7660,plain,
! [X5,X4,X6,X7] :
( ( sP11(X5,X4,X6,X7)
| ? [X8] :
( p__attribute(X8,X5)
& p__d__instance(X8,c__Object)
& p__attribute(X8,X4) )
| ~ sP10(X4,X5)
| ~ sP9(X6,X4)
| ~ sP8(X4,X6)
| ~ sP7(X7,X4)
| ~ sP6(X4,X7)
| ~ sP5(X6,X5)
| ~ sP4(X5,X6)
| ~ sP3(X7,X5)
| ~ sP2(X5,X7)
| ~ sP1(X7,X6)
| ~ sP0(X6,X7) )
& ( ( ! [X8] :
( ~ p__attribute(X8,X5)
| ~ p__d__instance(X8,c__Object)
| ~ p__attribute(X8,X4) )
& sP10(X4,X5)
& sP9(X6,X4)
& sP8(X4,X6)
& sP7(X7,X4)
& sP6(X4,X7)
& sP5(X6,X5)
& sP4(X5,X6)
& sP3(X7,X5)
& sP2(X5,X7)
& sP1(X7,X6)
& sP0(X6,X7) )
| ~ sP11(X5,X4,X6,X7) ) ),
inference(nnf_transformation,[],[f7634]) ).
fof(f7661,plain,
! [X5,X4,X6,X7] :
( ( sP11(X5,X4,X6,X7)
| ? [X8] :
( p__attribute(X8,X5)
& p__d__instance(X8,c__Object)
& p__attribute(X8,X4) )
| ~ sP10(X4,X5)
| ~ sP9(X6,X4)
| ~ sP8(X4,X6)
| ~ sP7(X7,X4)
| ~ sP6(X4,X7)
| ~ sP5(X6,X5)
| ~ sP4(X5,X6)
| ~ sP3(X7,X5)
| ~ sP2(X5,X7)
| ~ sP1(X7,X6)
| ~ sP0(X6,X7) )
& ( ( ! [X8] :
( ~ p__attribute(X8,X5)
| ~ p__d__instance(X8,c__Object)
| ~ p__attribute(X8,X4) )
& sP10(X4,X5)
& sP9(X6,X4)
& sP8(X4,X6)
& sP7(X7,X4)
& sP6(X4,X7)
& sP5(X6,X5)
& sP4(X5,X6)
& sP3(X7,X5)
& sP2(X5,X7)
& sP1(X7,X6)
& sP0(X6,X7) )
| ~ sP11(X5,X4,X6,X7) ) ),
inference(flattening,[],[f7660]) ).
fof(f7662,plain,
! [X0,X1,X2,X3] :
( ( sP11(X0,X1,X2,X3)
| ? [X4] :
( p__attribute(X4,X0)
& p__d__instance(X4,c__Object)
& p__attribute(X4,X1) )
| ~ sP10(X1,X0)
| ~ sP9(X2,X1)
| ~ sP8(X1,X2)
| ~ sP7(X3,X1)
| ~ sP6(X1,X3)
| ~ sP5(X2,X0)
| ~ sP4(X0,X2)
| ~ sP3(X3,X0)
| ~ sP2(X0,X3)
| ~ sP1(X3,X2)
| ~ sP0(X2,X3) )
& ( ( ! [X5] :
( ~ p__attribute(X5,X0)
| ~ p__d__instance(X5,c__Object)
| ~ p__attribute(X5,X1) )
& sP10(X1,X0)
& sP9(X2,X1)
& sP8(X1,X2)
& sP7(X3,X1)
& sP6(X1,X3)
& sP5(X2,X0)
& sP4(X0,X2)
& sP3(X3,X0)
& sP2(X0,X3)
& sP1(X3,X2)
& sP0(X2,X3) )
| ~ sP11(X0,X1,X2,X3) ) ),
inference(rectify,[],[f7661]) ).
fof(f7663,plain,
! [X0,X1,X2,X3] :
( ( sP11(X0,X1,X2,X3)
| ( p__attribute(sK31(X0,X1),X0)
& p__d__instance(sK31(X0,X1),c__Object)
& p__attribute(sK31(X0,X1),X1) )
| ~ sP10(X1,X0)
| ~ sP9(X2,X1)
| ~ sP8(X1,X2)
| ~ sP7(X3,X1)
| ~ sP6(X1,X3)
| ~ sP5(X2,X0)
| ~ sP4(X0,X2)
| ~ sP3(X3,X0)
| ~ sP2(X0,X3)
| ~ sP1(X3,X2)
| ~ sP0(X2,X3) )
& ( ( ! [X5] :
( ~ p__attribute(X5,X0)
| ~ p__d__instance(X5,c__Object)
| ~ p__attribute(X5,X1) )
& sP10(X1,X0)
& sP9(X2,X1)
& sP8(X1,X2)
& sP7(X3,X1)
& sP6(X1,X3)
& sP5(X2,X0)
& sP4(X0,X2)
& sP3(X3,X0)
& sP2(X0,X3)
& sP1(X3,X2)
& sP0(X2,X3) )
| ~ sP11(X0,X1,X2,X3) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31]),skolemize(X4,sK31(X0,X1))],[f7662]) ).
fof(f7682,plain,
! [X5,X6] :
( ( sP4(X5,X6)
| ? [X15] :
( p__attribute(X15,X5)
& p__d__instance(X15,c__Object)
& p__attribute(X15,X6) ) )
& ( ! [X15] :
( ~ p__attribute(X15,X5)
| ~ p__d__instance(X15,c__Object)
| ~ p__attribute(X15,X6) )
| ~ sP4(X5,X6) ) ),
inference(nnf_transformation,[],[f7627]) ).
fof(f7683,plain,
! [X0,X1] :
( ( sP4(X0,X1)
| ? [X2] :
( p__attribute(X2,X0)
& p__d__instance(X2,c__Object)
& p__attribute(X2,X1) ) )
& ( ! [X3] :
( ~ p__attribute(X3,X0)
| ~ p__d__instance(X3,c__Object)
| ~ p__attribute(X3,X1) )
| ~ sP4(X0,X1) ) ),
inference(rectify,[],[f7682]) ).
fof(f7684,plain,
! [X0,X1] :
( ( sP4(X0,X1)
| ( p__attribute(sK38(X0,X1),X0)
& p__d__instance(sK38(X0,X1),c__Object)
& p__attribute(sK38(X0,X1),X1) ) )
& ( ! [X3] :
( ~ p__attribute(X3,X0)
| ~ p__d__instance(X3,c__Object)
| ~ p__attribute(X3,X1) )
| ~ sP4(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38]),skolemize(X2,sK38(X0,X1))],[f7683]) ).
fof(f7697,plain,
( ! [X0,X1] :
( ( ( p__contraryAttribute2(X0,X1)
| ? [X2] :
( p__attribute(X2,X1)
& p__d__instance(X2,c__Object)
& p__attribute(X2,X0) )
| ~ sP13(X0,X1) )
& ( ( ! [X2] :
( ~ p__attribute(X2,X1)
| ~ p__d__instance(X2,c__Object)
| ~ p__attribute(X2,X0) )
& sP13(X0,X1) )
| ~ p__contraryAttribute2(X0,X1) ) )
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute) )
& ! [X4,X5,X6,X7] :
( sP12(X7,X6,X4,X5)
| ~ p__d__instance(X7,c__Attribute)
| ~ p__d__instance(X6,c__Attribute)
| ~ p__d__instance(X5,c__Attribute)
| ~ p__d__instance(X4,c__Attribute) ) ),
inference(nnf_transformation,[],[f7637]) ).
fof(f7698,plain,
( ! [X0,X1] :
( ( ( p__contraryAttribute2(X0,X1)
| ? [X2] :
( p__attribute(X2,X1)
& p__d__instance(X2,c__Object)
& p__attribute(X2,X0) )
| ~ sP13(X0,X1) )
& ( ( ! [X2] :
( ~ p__attribute(X2,X1)
| ~ p__d__instance(X2,c__Object)
| ~ p__attribute(X2,X0) )
& sP13(X0,X1) )
| ~ p__contraryAttribute2(X0,X1) ) )
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute) )
& ! [X4,X5,X6,X7] :
( sP12(X7,X6,X4,X5)
| ~ p__d__instance(X7,c__Attribute)
| ~ p__d__instance(X6,c__Attribute)
| ~ p__d__instance(X5,c__Attribute)
| ~ p__d__instance(X4,c__Attribute) ) ),
inference(flattening,[],[f7697]) ).
fof(f7699,plain,
( ! [X0,X1] :
( ( ( p__contraryAttribute2(X0,X1)
| ? [X2] :
( p__attribute(X2,X1)
& p__d__instance(X2,c__Object)
& p__attribute(X2,X0) )
| ~ sP13(X0,X1) )
& ( ( ! [X3] :
( ~ p__attribute(X3,X1)
| ~ p__d__instance(X3,c__Object)
| ~ p__attribute(X3,X0) )
& sP13(X0,X1) )
| ~ p__contraryAttribute2(X0,X1) ) )
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute) )
& ! [X4,X5,X6,X7] :
( sP12(X7,X6,X4,X5)
| ~ p__d__instance(X7,c__Attribute)
| ~ p__d__instance(X6,c__Attribute)
| ~ p__d__instance(X5,c__Attribute)
| ~ p__d__instance(X4,c__Attribute) ) ),
inference(rectify,[],[f7698]) ).
fof(f7700,plain,
( ! [X0,X1] :
( ( ( p__contraryAttribute2(X0,X1)
| ( p__attribute(sK43(X0,X1),X1)
& p__d__instance(sK43(X0,X1),c__Object)
& p__attribute(sK43(X0,X1),X0) )
| ~ sP13(X0,X1) )
& ( ( ! [X3] :
( ~ p__attribute(X3,X1)
| ~ p__d__instance(X3,c__Object)
| ~ p__attribute(X3,X0) )
& sP13(X0,X1) )
| ~ p__contraryAttribute2(X0,X1) ) )
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute) )
& ! [X4,X5,X6,X7] :
( sP12(X7,X6,X4,X5)
| ~ p__d__instance(X7,c__Attribute)
| ~ p__d__instance(X6,c__Attribute)
| ~ p__d__instance(X5,c__Attribute)
| ~ p__d__instance(X4,c__Attribute) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43]),skolemize(X2,sK43(X0,X1))],[f7699]) ).
fof(f7762,plain,
p__attribute(sK15,c__Liquid),
inference(cnf_transformation,[],[f7640]) ).
fof(f7763,plain,
p__attribute(sK16,c__Gas),
inference(cnf_transformation,[],[f7640]) ).
fof(f7764,plain,
sK15 = sK16,
inference(cnf_transformation,[],[f7640]) ).
fof(f7766,plain,
! [X2,X0,X1] :
( ~ p__d__instance(X0,X1)
| p__d__instance(X0,X2)
| ~ p__d__subclass(X1,X2) ),
inference(cnf_transformation,[],[f7458]) ).
fof(f7784,plain,
p__subAttribute(c__Gas,c__Fluid),
inference(cnf_transformation,[],[f2591]) ).
fof(f7786,plain,
p__contraryAttribute4(c__Solid,c__Liquid,c__Gas,c__Plasma),
inference(cnf_transformation,[],[f2584]) ).
fof(f7791,plain,
! [X2,X0,X1] :
( ~ p__d__subclass(X1,X2)
| ~ p__d__subclass(X0,X1)
| p__d__subclass(X0,X2) ),
inference(cnf_transformation,[],[f7472]) ).
fof(f7807,plain,
! [X0,X1] :
( ~ p__subAttribute(X0,X1)
| p__d__instance(X1,c__Attribute) ),
inference(cnf_transformation,[],[f7475]) ).
fof(f7808,plain,
! [X2,X0,X1] :
( ~ p__subAttribute(X1,X2)
| p__d__instance(X1,X0)
| ~ p__d__instance(X2,X0) ),
inference(cnf_transformation,[],[f7477]) ).
fof(f7809,plain,
! [X2,X0,X1] :
( p__attribute(X2,X1)
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute)
| ~ p__d__instance(X2,c__Object)
| ~ p__subAttribute(X0,X1)
| ~ p__attribute(X2,X0) ),
inference(cnf_transformation,[],[f7479]) ).
fof(f7812,plain,
p__subAttribute(c__Plasma,c__Fluid),
inference(cnf_transformation,[],[f2594]) ).
fof(f7818,plain,
p__d__instance(c__Solid,c__PhysicalState),
inference(cnf_transformation,[],[f2585]) ).
fof(f7819,plain,
p__d__subclass(c__PhysicalState,c__InternalAttribute),
inference(cnf_transformation,[],[f2583]) ).
fof(f7860,plain,
! [X2,X3,X0,X1] :
( ~ sP12(X0,X1,X2,X3)
| ~ p__contraryAttribute4(X2,X3,X1,X0)
| sP11(X3,X2,X1,X0) ),
inference(cnf_transformation,[],[f7659]) ).
fof(f7866,plain,
! [X2,X3,X0,X1] :
( ~ sP11(X0,X1,X2,X3)
| sP4(X0,X2) ),
inference(cnf_transformation,[],[f7663]) ).
fof(f7901,plain,
! [X3,X0,X1] :
( ~ p__attribute(X3,X0)
| ~ p__d__instance(X3,c__Object)
| ~ p__attribute(X3,X1)
| ~ sP4(X0,X1) ),
inference(cnf_transformation,[],[f7684]) ).
fof(f7921,plain,
! [X6,X7,X4,X5] :
( sP12(X7,X6,X4,X5)
| ~ p__d__instance(X7,c__Attribute)
| ~ p__d__instance(X6,c__Attribute)
| ~ p__d__instance(X5,c__Attribute)
| ~ p__d__instance(X4,c__Attribute) ),
inference(cnf_transformation,[],[f7700]) ).
fof(f7992,plain,
! [X0,X1] :
( ~ p__attribute(X0,X1)
| p__d__instance(X0,c__Object) ),
inference(cnf_transformation,[],[f7525]) ).
fof(f7993,plain,
! [X0,X1] :
( ~ p__attribute(X0,X1)
| p__d__instance(X1,c__Attribute) ),
inference(cnf_transformation,[],[f7525]) ).
fof(f7995,plain,
p__d__subclass(c__InternalAttribute,c__Attribute),
inference(cnf_transformation,[],[f254]) ).
fof(f8225,plain,
p__attribute(sK16,c__Liquid),
inference(definition_unfolding,[],[f7762,f7764]) ).
fof(f8261,plain,
! [X3,X0,X1] :
( ~ sP4(X0,X1)
| ~ p__attribute(X3,X1)
| ~ p__attribute(X3,X0) ),
inference(forward_subsumption_resolution,[],[f7901,f7992]) ).
fof(f8275,plain,
! [X2,X0,X1] :
( p__attribute(X2,X1)
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X2,c__Object)
| ~ p__subAttribute(X0,X1)
| ~ p__attribute(X2,X0) ),
inference(forward_subsumption_resolution,[],[f7809,f7993]) ).
fof(f8284,plain,
! [X2,X0,X1] :
( p__attribute(X2,X1)
| ~ p__d__instance(X2,c__Object)
| ~ p__subAttribute(X0,X1)
| ~ p__attribute(X2,X0) ),
inference(forward_subsumption_resolution,[],[f8275,f7807]) ).
fof(f8289,plain,
! [X2,X0,X1] :
( ~ p__subAttribute(X0,X1)
| p__attribute(X2,X1)
| ~ p__attribute(X2,X0) ),
inference(forward_subsumption_resolution,[],[f8284,f7992]) ).
fof(f8305,plain,
p__d__instance(c__Gas,c__Attribute),
inference(resolution,[],[f7993,f7763]) ).
fof(f8306,plain,
p__d__instance(c__Liquid,c__Attribute),
inference(resolution,[],[f7993,f8225]) ).
fof(f8324,plain,
! [X0] :
( ~ p__d__subclass(c__PhysicalState,X0)
| p__d__instance(c__Solid,X0) ),
inference(resolution,[],[f7818,f7766]) ).
fof(f8356,plain,
! [X2,X3,X0,X1] :
( ~ p__contraryAttribute4(X3,X2,X1,X0)
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X2,c__Attribute)
| ~ p__d__instance(X3,c__Attribute)
| ~ p__d__instance(X0,c__Attribute)
| sP11(X2,X3,X1,X0) ),
inference(resolution,[],[f7921,f7860]) ).
fof(f8357,plain,
( ~ p__d__instance(c__Gas,c__Attribute)
| ~ p__d__instance(c__Liquid,c__Attribute)
| ~ p__d__instance(c__Solid,c__Attribute)
| ~ p__d__instance(c__Plasma,c__Attribute)
| sP11(c__Liquid,c__Solid,c__Gas,c__Plasma) ),
inference(resolution,[],[f8356,f7786]) ).
fof(f8358,plain,
( ~ p__d__instance(c__Liquid,c__Attribute)
| ~ p__d__instance(c__Solid,c__Attribute)
| ~ p__d__instance(c__Plasma,c__Attribute)
| sP11(c__Liquid,c__Solid,c__Gas,c__Plasma) ),
inference(forward_subsumption_resolution,[],[f8357,f8305]) ).
fof(f8359,plain,
( ~ p__d__instance(c__Solid,c__Attribute)
| ~ p__d__instance(c__Plasma,c__Attribute)
| sP11(c__Liquid,c__Solid,c__Gas,c__Plasma) ),
inference(forward_subsumption_resolution,[],[f8358,f8306]) ).
fof(f8361,definition,
( spl109_12
<=> sP11(c__Liquid,c__Solid,c__Gas,c__Plasma) ),
introduced(definition,[new_symbols(definition,[spl109_12])],[avatar_definition]) ).
fof(f8363,plain,
( sP11(c__Liquid,c__Solid,c__Gas,c__Plasma)
| ~ spl109_12 ),
inference(avatar_component_clause,[],[f8361]) ).
fof(f8365,definition,
( spl109_13
<=> p__d__instance(c__Plasma,c__Attribute) ),
introduced(definition,[new_symbols(definition,[spl109_13])],[avatar_definition]) ).
fof(f8367,plain,
( ~ p__d__instance(c__Plasma,c__Attribute)
| spl109_13 ),
inference(avatar_component_clause,[],[f8365]) ).
fof(f8369,definition,
( spl109_14
<=> p__d__instance(c__Solid,c__Attribute) ),
introduced(definition,[new_symbols(definition,[spl109_14])],[avatar_definition]) ).
fof(f8371,plain,
( ~ p__d__instance(c__Solid,c__Attribute)
| spl109_14 ),
inference(avatar_component_clause,[],[f8369]) ).
fof(f8372,plain,
( spl109_12
| ~ spl109_13
| ~ spl109_14 ),
inference(avatar_split_clause,[],[f8359,f8369,f8365,f8361]) ).
fof(f8391,plain,
! [X0] :
( ~ p__d__instance(c__Fluid,X0)
| p__d__instance(c__Plasma,X0) ),
inference(resolution,[],[f7808,f7812]) ).
fof(f8427,plain,
! [X0] :
( ~ p__attribute(X0,c__Gas)
| p__attribute(X0,c__Fluid) ),
inference(resolution,[],[f8289,f7784]) ).
fof(f8430,plain,
p__attribute(sK16,c__Fluid),
inference(resolution,[],[f8427,f7763]) ).
fof(f8435,plain,
p__d__instance(c__Fluid,c__Attribute),
inference(resolution,[],[f8430,f7993]) ).
fof(f8438,plain,
p__d__instance(c__Plasma,c__Attribute),
inference(resolution,[],[f8435,f8391]) ).
fof(f8442,plain,
( $false
| spl109_13 ),
inference(forward_subsumption_resolution,[],[f8438,f8367]) ).
fof(f8443,plain,
spl109_13,
inference(avatar_contradiction_clause,[],[f8442]) ).
fof(f8635,plain,
! [X0] :
( ~ p__d__subclass(X0,c__InternalAttribute)
| p__d__subclass(X0,c__Attribute) ),
inference(resolution,[],[f7995,f7791]) ).
fof(f8646,plain,
p__d__subclass(c__PhysicalState,c__Attribute),
inference(resolution,[],[f8635,f7819]) ).
fof(f8648,plain,
p__d__instance(c__Solid,c__Attribute),
inference(resolution,[],[f8646,f8324]) ).
fof(f8662,plain,
( $false
| spl109_14 ),
inference(forward_subsumption_resolution,[],[f8648,f8371]) ).
fof(f8663,plain,
spl109_14,
inference(avatar_contradiction_clause,[],[f8662]) ).
fof(f8722,plain,
( sP4(c__Liquid,c__Gas)
| ~ spl109_12 ),
inference(resolution,[],[f7866,f8363]) ).
fof(f9072,plain,
( ! [X0] :
( ~ p__attribute(X0,c__Gas)
| ~ p__attribute(X0,c__Liquid) )
| ~ spl109_12 ),
inference(resolution,[],[f8261,f8722]) ).
fof(f9073,plain,
( ~ p__attribute(sK16,c__Liquid)
| ~ spl109_12 ),
inference(resolution,[],[f9072,f7763]) ).
fof(f9078,plain,
( $false
| ~ spl109_12 ),
inference(forward_subsumption_resolution,[],[f9073,f8225]) ).
fof(f9079,plain,
~ spl109_12,
inference(avatar_contradiction_clause,[],[f9078]) ).
cnf(s7,plain,
( spl109_12
| ~ spl109_13
| ~ spl109_14 ),
inference(sat_conversion,[],[f8372]) ).
cnf(s11,plain,
spl109_13,
inference(sat_conversion,[],[f8443]) ).
cnf(s26,plain,
spl109_14,
inference(sat_conversion,[],[f8663]) ).
cnf(s51,plain,
~ spl109_12,
inference(sat_conversion,[],[f9079]) ).
cnf(s52,plain,
$false,
inference(rat,[],[s7,s26,s11,s51]) ).
fof(f9080,plain,
$false,
inference(avatar_sat_refutation,[],[s52]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR216+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n003.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 23:47:28 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.12/1.74 % (2141571)Detected formulas, will run a generic FOF schedule.
% 6.12/1.74 % (2141580)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=272471655:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 6.12/1.74 % (2141580)Instruction limit reached!
% 6.12/1.74 % (2141580)------------------------------
% 6.12/1.74 % (2141580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.12/1.74 % (2141580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.74 % (2141580)CaDiCaL version: 2.1.3
% 6.12/1.74 % (2141580)Termination reason: Instruction limit
% 6.12/1.74 % (2141580)Termination phase: Saturation
% 6.12/1.74 % (2141580)Time elapsed: 0.029 s
% 6.12/1.74 % (2141580)Peak memory usage: 93 MB
% 6.12/1.74 % (2141580)Instructions burned: 122 (million)
% 6.12/1.74 % (2141582)dis-21_1_sil=8000:lcm=predicate:random_seed=2962554155: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)
% 6.12/1.74 % (2141578)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=702347297:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 6.12/1.74 % (2141581)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=956375582:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 6.12/1.74 % (2141579)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3392212117:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 6.12/1.74 % (2141576)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=3805889171:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 6.12/1.74 % (2141577)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=1007627530:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 6.12/1.74 % (2141579)Refutation not found, incomplete strategy
% 6.12/1.74 % (2141579)------------------------------
% 6.12/1.74 % (2141579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.12/1.74 % (2141579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.74 % (2141579)CaDiCaL version: 2.1.3
% 6.12/1.74 % (2141579)Termination reason: Refutation not found, incomplete strategy
% 6.12/1.74 % (2141579)Time elapsed: 0.016 s
% 6.12/1.74 % (2141579)Peak memory usage: 93 MB
% 6.12/1.74 % (2141579)Instructions burned: 24 (million)
% 6.12/1.74 % (2141582)Instruction limit reached!
% 6.12/1.74 % (2141582)------------------------------
% 6.12/1.74 % (2141582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.12/1.74 % (2141582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.74 % (2141582)CaDiCaL version: 2.1.3
% 6.12/1.74 % (2141582)Termination reason: Instruction limit
% 6.12/1.74 % (2141582)Termination phase: Saturation
% 6.12/1.74 % (2141582)Time elapsed: 0.075 s
% 6.12/1.74 % (2141582)Peak memory usage: 95 MB
% 6.12/1.74 % (2141582)Instructions burned: 130 (million)
% 6.12/1.74 % (2141581)Instruction limit reached!
% 6.12/1.74 % (2141581)------------------------------
% 6.12/1.74 % (2141581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.12/1.74 % (2141581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.74 % (2141581)CaDiCaL version: 2.1.3
% 6.12/1.74 % (2141581)Termination reason: Instruction limit
% 6.12/1.74 % (2141581)Termination phase: Preprocessing 3
% 6.12/1.74 % (2141581)Time elapsed: 0.093 s
% 6.12/1.74 % (2141581)Peak memory usage: 94 MB
% 6.12/1.74 % (2141581)Instructions burned: 141 (million)
% 6.12/1.74 % (2141584)lrs+10_1_sil=8000:sp=occurrence:random_seed=2014784250:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 6.12/1.74 % (2141584)Refutation not found, incomplete strategy
% 6.12/1.74 % (2141584)------------------------------
% 6.12/1.74 % (2141584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.12/1.74 % (2141584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.74 % (2141584)CaDiCaL version: 2.1.3
% 6.12/1.74 % (2141584)Termination reason: Refutation not found, incomplete strategy
% 6.12/1.74 % (2141584)Time elapsed: 0.010 s
% 6.12/1.74 % (2141584)Peak memory usage: 94 MB
% 6.12/1.74 % (2141584)Instructions burned: 20 (million)
% 10.72/2.39 % (2141591)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2046111770:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 10.72/2.39 % (2141579)------------------------------
% 10.72/2.39 % (2141579)------------------------------
% 10.72/2.39 % (2141592)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3646643253:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 10.72/2.39 % (2141591)Refutation not found, incomplete strategy
% 10.72/2.39 % (2141591)------------------------------
% 10.72/2.39 % (2141591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.72/2.39 % (2141591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.72/2.39 % (2141591)CaDiCaL version: 2.1.3
% 10.72/2.39 % (2141591)Termination reason: Refutation not found, incomplete strategy
% 10.72/2.39 % (2141591)Time elapsed: 0.032 s
% 10.72/2.39 % (2141591)Peak memory usage: 94 MB
% 10.72/2.39 % (2141591)Instructions burned: 60 (million)
% 10.72/2.39 % (2141592)Refutation not found, incomplete strategy
% 10.72/2.39 % (2141592)------------------------------
% 10.72/2.39 % (2141592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.72/2.39 % (2141592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.72/2.39 % (2141592)CaDiCaL version: 2.1.3
% 10.72/2.39 % (2141592)Termination reason: Refutation not found, incomplete strategy
% 10.72/2.39 % (2141592)Time elapsed: 0.019 s
% 10.72/2.39 % (2141592)Peak memory usage: 94 MB
% 10.72/2.39 % (2141592)Instructions burned: 23 (million)
% 10.72/2.39 % (2141584)------------------------------
% 10.72/2.39 % (2141584)------------------------------
% 10.72/2.39 [W928 23:47:29.889696535 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 10.72/2.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.72/2.39 [W928 23:47:29.889741329 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 10.72/2.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.72/2.39 [W928 23:47:29.889782893 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 10.72/2.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.72/2.39 [W928 23:47:29.889796316 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 10.72/2.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.72/2.39 [W928 23:47:29.889823640 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 10.72/2.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.72/2.39 [W928 23:47:29.889835347 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 10.72/2.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.72/2.39 [W928 23:47:29.889861257 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 10.72/2.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.72/2.39 [W928 23:47:29.889873104 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 10.72/2.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.72/2.39 [W928 23:47:29.889898604 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 16.21/3.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 16.21/3.13 [W928 23:47:29.889909981 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 16.21/3.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 16.21/3.13 [W928 23:47:29.889948045 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 16.21/3.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 16.21/3.13 [W928 23:47:29.889971628 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 16.21/3.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 16.21/3.13 % (2141597)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2349424423:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 16.21/3.13 % (2141596)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=3832727197:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 16.21/3.13 % (2141597)Instruction limit reached!
% 16.21/3.13 % (2141597)------------------------------
% 16.21/3.13 % (2141597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.21/3.13 % (2141597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.21/3.13 % (2141597)CaDiCaL version: 2.1.3
% 16.21/3.13 % (2141597)Termination reason: Instruction limit
% 16.21/3.13 % (2141597)Termination phase: Saturation
% 16.21/3.13 % (2141597)Time elapsed: 0.076 s
% 16.21/3.13 % (2141597)Peak memory usage: 94 MB
% 16.21/3.13 % (2141597)Instructions burned: 298 (million)
% 16.21/3.13 % (2141591)------------------------------
% 16.21/3.13 % (2141591)------------------------------
% 16.21/3.13 % (2141592)------------------------------
% 16.21/3.13 % (2141592)------------------------------
% 16.21/3.13 % (2141596)Instruction limit reached!
% 16.21/3.13 % (2141596)------------------------------
% 16.21/3.13 % (2141596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.21/3.13 % (2141596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.21/3.13 % (2141596)CaDiCaL version: 2.1.3
% 16.21/3.13 % (2141596)Termination reason: Instruction limit
% 16.21/3.13 % (2141596)Termination phase: Saturation
% 16.21/3.13 % (2141596)Time elapsed: 0.127 s
% 16.21/3.13 % (2141596)Peak memory usage: 98 MB
% 16.21/3.13 % (2141596)Instructions burned: 249 (million)
% 16.21/3.13 % (2141578)Refutation not found, incomplete strategy
% 16.21/3.13 % (2141578)------------------------------
% 16.21/3.13 % (2141578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.21/3.13 % (2141578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.21/3.13 % (2141578)CaDiCaL version: 2.1.3
% 16.21/3.13 % (2141578)Termination reason: Refutation not found, incomplete strategy
% 16.21/3.13 % (2141578)Time elapsed: 0.607 s
% 16.21/3.13 % (2141578)Peak memory usage: 147 MB
% 16.21/3.13 % (2141578)Instructions burned: 956 (million)
% 16.21/3.13 % (2141600)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=669785173:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 16.21/3.13 % (2141601)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3633647775:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 16.21/3.13 % (2141602)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1368596662:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 16.21/3.13 % (2141603)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3391066232:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 16.21/3.13 % (2141601)Instruction limit reached!
% 16.21/3.13 % (2141601)------------------------------
% 16.21/3.13 % (2141601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.21/3.13 % (2141601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.55 % (2141601)CaDiCaL version: 2.1.3
% 18.60/3.55 % (2141601)Termination reason: Instruction limit
% 18.60/3.55 % (2141601)Termination phase: Saturation
% 18.60/3.55 % (2141601)Time elapsed: 0.059 s
% 18.60/3.55 % (2141601)Peak memory usage: 94 MB
% 18.60/3.55 % (2141601)Instructions burned: 115 (million)
% 18.60/3.55 % (2141578)------------------------------
% 18.60/3.55 % (2141578)------------------------------
% 18.60/3.55 % (2141602)Instruction limit reached!
% 18.60/3.55 % (2141602)------------------------------
% 18.60/3.55 % (2141602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.60/3.55 % (2141602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.55 % (2141602)CaDiCaL version: 2.1.3
% 18.60/3.55 % (2141602)Termination reason: Instruction limit
% 18.60/3.55 % (2141602)Termination phase: Property scanning
% 18.60/3.55 % (2141602)Time elapsed: 0.079 s
% 18.60/3.55 % (2141602)Peak memory usage: 96 MB
% 18.60/3.55 % (2141602)Instructions burned: 128 (million)
% 18.60/3.55 % (2141603)Instruction limit reached!
% 18.60/3.55 % (2141603)------------------------------
% 18.60/3.55 % (2141603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.60/3.55 % (2141603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.55 % (2141603)CaDiCaL version: 2.1.3
% 18.60/3.55 % (2141603)Termination reason: Instruction limit
% 18.60/3.55 % (2141603)Termination phase: Function definition elimination
% 18.60/3.55 % (2141603)Time elapsed: 0.063 s
% 18.60/3.55 % (2141603)Peak memory usage: 92 MB
% 18.60/3.55 % (2141603)Instructions burned: 115 (million)
% 18.60/3.55 % (2141609)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=140922419:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 18.60/3.55 % (2141608)lrs+10_1_sil=8000:sp=occurrence:random_seed=3500859197:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 18.60/3.55 % (2141609)Refutation not found, incomplete strategy
% 18.60/3.55 % (2141609)------------------------------
% 18.60/3.55 % (2141609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.60/3.55 % (2141609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.55 % (2141609)CaDiCaL version: 2.1.3
% 18.60/3.55 % (2141609)Termination reason: Refutation not found, incomplete strategy
% 18.60/3.55 % (2141609)Time elapsed: 0.009 s
% 18.60/3.55 % (2141609)Peak memory usage: 93 MB
% 18.60/3.55 % (2141609)Instructions burned: 19 (million)
% 18.60/3.55 % (2141610)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=425955033:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 18.60/3.55 % (2141611)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=566766973:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 18.60/3.55 % (2141611)Refutation not found, incomplete strategy
% 18.60/3.55 % (2141611)------------------------------
% 18.60/3.55 % (2141611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.60/3.55 % (2141611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.55 % (2141611)CaDiCaL version: 2.1.3
% 18.60/3.55 % (2141611)Termination reason: Refutation not found, incomplete strategy
% 18.60/3.55 % (2141611)Time elapsed: 0.017 s
% 18.60/3.55 % (2141611)Peak memory usage: 94 MB
% 18.60/3.55 % (2141611)Instructions burned: 24 (million)
% 18.60/3.55 % (2141609)------------------------------
% 18.60/3.55 % (2141609)------------------------------
% 18.60/3.55 % (2141616)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=823741008:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 18.60/3.55 % (2141611)------------------------------
% 18.60/3.55 % (2141611)------------------------------
% 18.60/3.55 % (2141616)Instruction limit reached!
% 18.60/3.55 % (2141616)------------------------------
% 18.60/3.55 % (2141616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.60/3.55 % (2141616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.55 % (2141616)CaDiCaL version: 2.1.3
% 18.60/3.55 % (2141616)Termination reason: Instruction limit
% 18.60/3.55 % (2141616)Termination phase: Saturation
% 18.60/3.55 % (2141616)Time elapsed: 0.157 s
% 18.60/3.55 % (2141616)Peak memory usage: 100 MB
% 18.60/3.55 % (2141616)Instructions burned: 593 (million)
% 18.60/3.55 % (2141608)Instruction limit reached!
% 18.60/3.55 % (2141608)------------------------------
% 18.60/3.55 % (2141608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.60/3.55 % (2141608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.55 % (2141608)CaDiCaL version: 2.1.3
% 18.60/3.55 % (2141608)Termination reason: Instruction limit
% 18.60/3.55 % (2141608)Termination phase: Saturation
% 18.60/3.55 % (2141608)Time elapsed: 0.509 s
% 18.60/3.55 % (2141608)Peak memory usage: 105 MB
% 18.60/3.55 % (2141608)Instructions burned: 907 (million)
% 18.60/3.55 % (2141618)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3619743803:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 18.60/3.55 % (2141619)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=2082088898:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 18.60/3.55 % (2141619)Refutation not found, incomplete strategy
% 18.60/3.55 % (2141619)------------------------------
% 18.60/3.55 % (2141619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.60/3.55 % (2141619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.55 % (2141619)CaDiCaL version: 2.1.3
% 18.60/3.55 % (2141619)Termination reason: Refutation not found, incomplete strategy
% 18.60/3.55 % (2141619)Time elapsed: 0.024 s
% 18.60/3.55 % (2141619)Peak memory usage: 94 MB
% 18.60/3.55 % (2141619)Instructions burned: 79 (million)
% 18.60/3.55 % (2141621)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4145707255:i=134:gtgl=5:slsql=off:gtg=exists_sym_2982 on theBenchmark for (2982ds/134Mi)
% 18.60/3.55 % (2141619)------------------------------
% 18.60/3.55 % (2141619)------------------------------
% 18.60/3.55 % (2141621)Instruction limit reached!
% 18.60/3.55 % (2141621)------------------------------
% 18.60/3.55 % (2141621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.60/3.55 % (2141621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.55 % (2141621)CaDiCaL version: 2.1.3
% 18.60/3.55 % (2141621)Termination reason: Instruction limit
% 18.60/3.55 % (2141621)Termination phase: Preprocessing 2
% 18.60/3.55 % (2141621)Time elapsed: 0.075 s
% 18.60/3.55 % (2141621)Peak memory usage: 92 MB
% 18.60/3.55 % (2141621)Instructions burned: 134 (million)
% 18.60/3.55 % (2141624)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1316051052:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/141Mi)
% 18.60/3.55 % (2141625)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1837544742:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2980 on theBenchmark for (2980ds/431Mi)
% 18.60/3.55 % (2141624)Refutation not found, incomplete strategy
% 18.60/3.55 % (2141624)------------------------------
% 18.60/3.55 % (2141624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.60/3.55 % (2141624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.55 % (2141624)CaDiCaL version: 2.1.3
% 18.60/3.55 % (2141624)Termination reason: Refutation not found, incomplete strategy
% 18.60/3.55 % (2141624)Time elapsed: 0.018 s
% 18.60/3.55 % (2141624)Peak memory usage: 94 MB
% 18.60/3.55 % (2141624)Instructions burned: 23 (million)
% 18.60/3.55 % (2141625)Refutation not found, incomplete strategy
% 18.60/3.55 % (2141625)------------------------------
% 18.60/3.55 % (2141625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.60/3.55 % (2141625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.55 % (2141625)CaDiCaL version: 2.1.3
% 18.60/3.55 % (2141625)Termination reason: Refutation not found, incomplete strategy
% 18.60/3.55 % (2141625)Time elapsed: 0.020 s
% 18.60/3.55 % (2141625)Peak memory usage: 94 MB
% 18.60/3.55 % (2141625)Instructions burned: 22 (million)
% 18.60/3.55 % (2141624)------------------------------
% 18.60/3.55 % (2141624)------------------------------
% 18.60/3.55 % (2141625)------------------------------
% 18.60/3.55 % (2141625)------------------------------
% 18.60/3.55 % (2141600)Instruction limit reached!
% 18.60/3.55 % (2141600)------------------------------
% 18.60/3.55 % (2141600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.60/3.55 % (2141600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.55 % (2141600)CaDiCaL version: 2.1.3
% 18.60/3.55 % (2141600)Termination reason: Instruction limit
% 18.60/3.55 % (2141600)Termination phase: Saturation
% 18.60/3.55 % (2141600)Time elapsed: 1.470 s
% 18.60/3.55 % (2141600)Peak memory usage: 206 MB
% 18.60/3.55 % (2141600)Instructions burned: 2350 (million)
% 18.60/3.55 % (2141628)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=3035742064:i=6060:aac=none:ins=25_2975 on theBenchmark for (2975ds/6060Mi)
% 18.60/3.55 % (2141629)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=3978450828:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2975 on theBenchmark for (2975ds/150Mi)
% 18.60/3.55 % (2141618)First to succeed.
% 18.60/3.55 % (2141618)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2141571"
% 18.60/3.55 % (2141630)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3297696945:i=14155:bd=all_2975 on theBenchmark for (2975ds/14155Mi)
% 18.60/3.55 % (2141629)Instruction limit reached!
% 18.60/3.55 % (2141629)------------------------------
% 18.60/3.55 % (2141629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.60/3.55 % (2141629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.55 % (2141629)CaDiCaL version: 2.1.3
% 18.60/3.55 % (2141629)Termination reason: Instruction limit
% 18.60/3.55 % (2141629)Termination phase: Property scanning
% 18.60/3.55 % (2141629)Time elapsed: 0.086 s
% 18.60/3.55 % (2141629)Peak memory usage: 96 MB
% 18.60/3.55 % (2141629)Instructions burned: 150 (million)
% 18.60/3.55 % (2141634)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=882395136:i=667:av=off:fsr=off_2973 on theBenchmark for (2973ds/667Mi)
% 18.60/3.55 % (2141618)Refutation found. Thanks to Tanya!
% 18.60/3.55 % SZS status Theorem for theBenchmark
% 18.60/3.55 % SZS output start Proof for theBenchmark
% See solution above
% 20.01/3.76 % (2141618)------------------------------
% 20.01/3.76 % (2141618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.01/3.76 % (2141618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.01/3.76 % (2141618)CaDiCaL version: 2.1.3
% 20.01/3.76 % (2141618)Termination reason: Refutation
% 20.01/3.76 % (2141618)Time elapsed: 0.877 s
% 20.01/3.76 % (2141618)Peak memory usage: 150 MB
% 20.01/3.76 % (2141618)Instructions burned: 1310 (million)
% 20.01/3.76 % (2141618)------------------------------
% 20.01/3.76 % (2141618)------------------------------
% 20.01/3.76 % (2141571)Success in time 2.887 s
% 20.01/3.76 % Vampire exiting
%------------------------------------------------------------------------------