%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : KRS043+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n019.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 11:41:31 AM UTC 2026
% Result : Satisfiable 7.93s 2.06s
% Output : Saturation 7.93s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u447,axiom,
ca_Ax14(sK0(i2003_11_14_17_16_14536)) ).
cnf(u369,axiom,
( ~ rr(sK0(i2003_11_14_17_16_14536),X0)
| i2003_11_14_17_16_14536 = X0 ) ).
cnf(u381,axiom,
cp1(i2003_11_14_17_16_14536) ).
cnf(u385,axiom,
ca_Cx1(i2003_11_14_17_16_14536) ).
cnf(u313,axiom,
cSatisfiable(i2003_11_14_17_16_14536) ).
cnf(u395,axiom,
( ~ ra_Px5(X0,X1)
| ~ ca_Cx1(X0) ) ).
cnf(u413,axiom,
~ ra_Px6(i2003_11_14_17_16_14536,X0) ).
cnf(u423,axiom,
~ ra_Px3(i2003_11_14_17_16_14536,X0) ).
cnf(u269,axiom,
( ~ cp3(X0)
| ca_Cx3(X0) ) ).
cnf(u469,axiom,
( cp5(X0)
| cp5xcomp(X0) ) ).
cnf(u279,axiom,
( ra_Px4(X0,sK8(X0))
| ~ cp5xcomp(X0) ) ).
cnf(u396,axiom,
( ~ cp2(X0)
| ~ ca_Cx1(X0) ) ).
cnf(u362,axiom,
i2003_11_14_17_16_14536 = sK11(sK0(i2003_11_14_17_16_14536)) ).
cnf(u406,axiom,
( ~ ca_Cx1(X0)
| ca_Cx2(X0) ) ).
cnf(u291,axiom,
( cp2xcomp(X0)
| ~ ca_Cx1(X0) ) ).
cnf(u408,axiom,
ca_Cx2(i2003_11_14_17_16_14536) ).
cnf(u262,axiom,
( ra_Px5(X0,sK1(X0))
| ~ cp2(X0) ) ).
cnf(u418,axiom,
~ ra_Px2(i2003_11_14_17_16_14536,X0) ).
cnf(u264,axiom,
( ~ cp2(X0)
| ca_Cx2(X0) ) ).
cnf(u436,axiom,
( ca_Cx1xcomp(X0)
| ca_Cx1(X0) ) ).
cnf(u274,axiom,
( ~ cp4(X0)
| cp5xcomp(X0) ) ).
cnf(u292,axiom,
( ~ ca_Cx1(X0)
| cp5xcomp(X0) ) ).
cnf(u302,axiom,
( ra_Px2(X0,sK15(X0))
| ~ ca_Cx2xcomp(X0) ) ).
cnf(u477,axiom,
( ~ ra_Px6(X0,X1)
| ca_Cx3(X0) ) ).
cnf(u287,axiom,
( ra_Px1(X0,sK12(X0))
| ~ ca_Cx1(X0) ) ).
cnf(u487,axiom,
( cp2xcomp(X0)
| ca_Cx2(X0) ) ).
cnf(u289,axiom,
( cp4xcomp(X0)
| ~ ca_Cx1(X0) ) ).
cnf(u299,axiom,
( ~ ca_Cx2(X0)
| cp3xcomp(X0) ) ).
cnf(u460,axiom,
( ~ cSatisfiable(X1)
| rr(X0,sK9(X0))
| ~ rr(X0,sK11(sK0(X1)))
| ca_Ax14(X0) ) ).
cnf(u426,axiom,
~ ca_Cx3xcomp(i2003_11_14_17_16_14536) ).
cnf(u272,axiom,
( ~ cp4(X0)
| ~ ra_Px7(X0,X2) ) ).
cnf(u355,axiom,
( ~ cSatisfiable(X0)
| sK11(sK0(X0)) = X1
| ~ rr(sK0(X0),X1) ) ).
cnf(u282,axiom,
( cp1(sK11(X0))
| ~ ca_Ax14(X0) ) ).
cnf(u300,axiom,
( ~ ca_Cx2(X0)
| cp5xcomp(X0) ) ).
cnf(u310,axiom,
( ~ ra_Px3(X0,X1)
| ca_Cx3xcomp(X0) ) ).
cnf(u312,axiom,
( rinvR(X0,X1)
| ~ rr(X1,X0) ) ).
cnf(u356,axiom,
( ~ rr(sK0(i2003_11_14_17_16_14536),X0)
| sK11(sK0(i2003_11_14_17_16_14536)) = X0 ) ).
cnf(u286,axiom,
( sK9(X0) != sK10(X0)
| ~ rr(X0,X1)
| ~ cp1(X1)
| ca_Ax14(X0) ) ).
cnf(u497,axiom,
( ca_Cx3xcomp(X0)
| ca_Cx3(X0) ) ).
cnf(u397,axiom,
( ~ cSatisfiable(X1)
| cSatisfiable(X0)
| ~ rinvR(X0,sK0(X1)) ) ).
cnf(u407,axiom,
( ~ ca_Ax14(X0)
| ca_Cx2(sK11(X0)) ) ).
cnf(u409,axiom,
( ~ cSatisfiable(X0)
| ca_Cx2(sK11(sK0(X0))) ) ).
cnf(u263,axiom,
( ~ ra_Px5(X0,X1)
| cp2(X0) ) ).
cnf(u419,axiom,
~ ca_Cx2xcomp(i2003_11_14_17_16_14536) ).
cnf(u265,axiom,
( ~ cp2xcomp(X0)
| ~ ra_Px5(X0,X2) ) ).
cnf(u390,axiom,
( ~ ra_Px6(X0,X1)
| ~ ca_Cx1(X0) ) ).
cnf(u275,axiom,
( ra_Px7(X0,sK6(X0))
| ~ cp4xcomp(X0) ) ).
cnf(u392,axiom,
( cp5xcomp(sK11(X0))
| ~ ca_Ax14(X0) ) ).
cnf(u293,axiom,
( ~ cp2xcomp(X0)
| ~ cp5xcomp(X0)
| ca_Cx1(X0)
| ~ cp3xcomp(X0)
| ~ cp4xcomp(X0) ) ).
cnf(u490,axiom,
( ~ ra_Px5(X0,X1)
| ca_Cx2(X0) ) ).
cnf(u258,axiom,
( ca_Ax14(sK0(X0))
| ~ cSatisfiable(X0) ) ).
cnf(u276,axiom,
( ~ ra_Px7(X0,X1)
| cp4xcomp(X0) ) ).
cnf(u415,axiom,
~ cp3(i2003_11_14_17_16_14536) ).
cnf(u271,axiom,
( ra_Px6(X0,sK4(X0))
| cp3xcomp(X0) ) ).
cnf(u427,axiom,
( ~ cSatisfiable(X0)
| ca_Cx3(sK11(sK0(X0)))
| ~ cp4xcomp(sK11(sK0(X0))) ) ).
cnf(u273,axiom,
( ra_Px7(X0,sK5(X0))
| cp4(X0) ) ).
cnf(u473,axiom,
( cp3(X0)
| cp3xcomp(X0) ) ).
cnf(u283,axiom,
( rr(X0,sK11(X0))
| ~ ca_Ax14(X0) ) ).
cnf(u256,axiom,
( ~ xsd_string(X0)
| ~ xsd_integer(X0) ) ).
cnf(u483,axiom,
( cp4xcomp(X0)
| cp5xcomp(X0) ) ).
cnf(u301,axiom,
( ~ cp4xcomp(X0)
| ~ cp5xcomp(X0)
| ~ cp3xcomp(X0)
| ca_Cx2(X0) ) ).
cnf(u311,axiom,
( ~ rinvR(X0,X1)
| rr(X1,X0) ) ).
cnf(u266,axiom,
( ra_Px5(X0,sK2(X0))
| cp2xcomp(X0) ) ).
cnf(u438,axiom,
( ~ ca_Ax14(X1)
| ca_Ax14(X0)
| rr(X0,sK10(X0))
| ~ rr(X0,sK11(X1)) ) ).
cnf(u284,axiom,
( ~ cp1(X1)
| ~ rr(X0,X1)
| ca_Ax14(X0)
| rr(X0,sK10(X0)) ) ).
cnf(u440,axiom,
( ~ ca_Ax14(X1)
| ca_Ax14(X0)
| rr(X0,sK9(X0))
| ~ rr(X0,sK11(X1)) ) ).
cnf(u294,axiom,
( ~ ca_Cx1xcomp(X0)
| ~ ra_Px1(X0,X2) ) ).
cnf(u494,axiom,
( ca_Cx2xcomp(X0)
| ca_Cx2(X0) ) ).
cnf(u296,axiom,
( ~ ca_Cx2(X0)
| ~ ra_Px2(X0,X2) ) ).
cnf(u306,axiom,
( ~ cp5xcomp(X0)
| ca_Cx3(X0)
| ~ cp4xcomp(X0) ) ).
cnf(u277,axiom,
( ~ cp5(X0)
| ~ ra_Px4(X0,X2) ) ).
cnf(u481,axiom,
( cp4(X0)
| cp4xcomp(X0) ) ).
cnf(u309,axiom,
( ra_Px3(X0,sK17(X0))
| ~ ca_Cx3xcomp(X0) ) ).
cnf(u391,axiom,
( ~ cp3(X0)
| ~ ca_Cx1(X0) ) ).
cnf(u393,axiom,
cp5xcomp(i2003_11_14_17_16_14536) ).
cnf(u421,axiom,
( ~ ca_Ax14(X0)
| ~ cp4xcomp(sK11(X0))
| ca_Cx3(sK11(X0)) ) ).
cnf(u304,axiom,
( ~ ca_Cx3(X0)
| cp4xcomp(X0) ) ).
cnf(u259,axiom,
( rinvR(X0,sK0(X0))
| ~ cSatisfiable(X0) ) ).
cnf(u358,axiom,
( ca_Cx1(sK11(X0))
| ~ ca_Ax14(X0) ) ).
cnf(u268,axiom,
( ~ ra_Px6(X0,X1)
| cp3(X0) ) ).
cnf(u260,axiom,
( ~ ca_Ax14(X1)
| ~ rinvR(X0,X1)
| cSatisfiable(X0) ) ).
cnf(u270,axiom,
( ~ cp3xcomp(X0)
| ~ ra_Px6(X0,X2) ) ).
cnf(u474,axiom,
( cp3xcomp(X0)
| ca_Cx3(X0) ) ).
cnf(u411,axiom,
cp4xcomp(i2003_11_14_17_16_14536) ).
cnf(u257,axiom,
( xsd_string(X0)
| xsd_integer(X0) ) ).
cnf(u457,axiom,
( ~ cSatisfiable(X1)
| rr(X0,sK10(X0))
| ~ rr(X0,sK11(sK0(X1)))
| ca_Ax14(X0) ) ).
cnf(u267,axiom,
( ra_Px6(X0,sK3(X0))
| ~ cp3(X0) ) ).
cnf(u439,axiom,
( ~ rr(X0,i2003_11_14_17_16_14536)
| ca_Ax14(X0)
| rr(X0,sK10(X0)) ) ).
cnf(u285,axiom,
( ~ cp1(X1)
| ~ rr(X0,X1)
| ca_Ax14(X0)
| rr(X0,sK9(X0)) ) ).
cnf(u441,axiom,
( ~ rr(X0,i2003_11_14_17_16_14536)
| ca_Ax14(X0)
| rr(X0,sK9(X0)) ) ).
cnf(u295,axiom,
( ra_Px1(X0,sK13(X0))
| ca_Cx1xcomp(X0) ) ).
cnf(u412,axiom,
cp3xcomp(i2003_11_14_17_16_14536) ).
cnf(u297,axiom,
( ra_Px2(X0,sK14(X0))
| ca_Cx2(X0) ) ).
cnf(u422,axiom,
ca_Cx3(i2003_11_14_17_16_14536) ).
cnf(u307,axiom,
( ~ ca_Cx3(X0)
| ~ ra_Px3(X0,X2) ) ).
cnf(u278,axiom,
( ra_Px4(X0,sK7(X0))
| cp5(X0) ) ).
cnf(u280,axiom,
( ~ ra_Px4(X0,X1)
| cp5xcomp(X0) ) ).
cnf(u290,axiom,
( cp3xcomp(X0)
| ~ ca_Cx1(X0) ) ).
cnf(u308,axiom,
( ra_Px3(X0,sK16(X0))
| ca_Cx3(X0) ) ).
cnf(u303,axiom,
( ~ ra_Px2(X0,X1)
| ca_Cx2xcomp(X0) ) ).
cnf(u305,axiom,
( ~ ca_Cx3(X0)
| cp5xcomp(X0) ) ).
cnf(u359,axiom,
( ~ cSatisfiable(X0)
| rr(sK0(X0),X0) ) ).
cnf(u361,axiom,
rr(sK0(i2003_11_14_17_16_14536),i2003_11_14_17_16_14536) ).
cnf(u486,axiom,
( cp2(X0)
| cp2xcomp(X0) ) ).
cnf(u288,axiom,
( ~ ra_Px1(X0,X1)
| ca_Cx1(X0) ) ).
cnf(u298,axiom,
( ~ ca_Cx2(X0)
| cp4xcomp(X0) ) ).
cnf(u261,axiom,
( ~ cp1(X0)
| ca_Cx1(X0) ) ).
cnf(u281,axiom,
( ~ rr(X0,X6)
| ~ rr(X0,X5)
| X5 = X6
| ~ ca_Ax14(X0) ) ).
cnf(u354,axiom,
( ~ ca_Ax14(X0)
| ~ rr(X0,X1)
| sK11(X0) = X1 ) ).
cnf(u398,axiom,
( ~ rinvR(X0,sK0(i2003_11_14_17_16_14536))
| cSatisfiable(X0) ) ).
cnf(u400,axiom,
( ~ rr(sK0(i2003_11_14_17_16_14536),X0)
| cSatisfiable(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS043+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.36 % Computer : n019.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 13:17:19 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 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.38/1.87 % (3091805)Detected formulas, will run a generic FOF schedule.
% 6.38/1.87 % (3091883)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=877314664:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 6.38/1.87 % (3091888)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=277134404:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 6.38/1.87 % (3091889)dis-21_1_sil=8000:lcm=predicate:random_seed=1528221415:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 6.38/1.87 % (3091885)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=4260262206:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 6.38/1.87 % (3091886)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2434530470:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 6.38/1.87 % (3091884)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=3217103351:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 6.38/1.87 % (3091887)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3578482948:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 6.38/1.87 % (3091887)Refutation not found, incomplete strategy
% 6.38/1.87 % (3091887)------------------------------
% 6.38/1.87 % (3091887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.38/1.87 % (3091887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.87 % (3091887)CaDiCaL version: 2.1.3
% 6.38/1.87 % (3091886)Refutation not found, incomplete strategy
% 6.38/1.87 % (3091886)------------------------------
% 6.38/1.87 % (3091886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.38/1.87 % (3091887)Termination reason: Refutation not found, incomplete strategy
% 6.38/1.87 % (3091887)Time elapsed: 0.0000 s
% 6.38/1.87 % (3091887)Peak memory usage: 86 MB
% 6.38/1.87 % (3091886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.87 % (3091886)CaDiCaL version: 2.1.3
% 6.38/1.87 % (3091886)Termination reason: Refutation not found, incomplete strategy
% 6.38/1.87 % (3091886)Time elapsed: 0.0000 s
% 6.38/1.87 % (3091886)Peak memory usage: 86 MB
% 6.38/1.87 % (3091889)Instruction limit reached!
% 6.38/1.87 % (3091889)------------------------------
% 6.38/1.87 % (3091889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.38/1.87 % (3091889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.87 % (3091889)CaDiCaL version: 2.1.3
% 6.38/1.87 % (3091889)Termination reason: Instruction limit
% 6.38/1.87 % (3091889)Termination phase: Saturation
% 6.38/1.87 % (3091889)Time elapsed: 0.055 s
% 6.38/1.87 % (3091889)Peak memory usage: 88 MB
% 6.38/1.87 % (3091889)Instructions burned: 130 (million)
% 6.38/1.87 % (3091888)Instruction limit reached!
% 6.38/1.87 % (3091888)------------------------------
% 6.38/1.87 % (3091888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.38/1.87 % (3091888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.87 % (3091888)CaDiCaL version: 2.1.3
% 6.38/1.87 % (3091888)Termination reason: Instruction limit
% 6.38/1.87 % (3091888)Termination phase: Saturation
% 6.38/1.87 % (3091888)Time elapsed: 0.073 s
% 6.38/1.87 % (3091888)Peak memory usage: 88 MB
% 6.38/1.87 % (3091888)Instructions burned: 140 (million)
% 6.38/1.87 % (3091897)lrs+10_1_sil=8000:sp=occurrence:random_seed=638438809:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 6.38/1.87 % (3091897)Refutation not found, incomplete strategy
% 6.38/1.87 % (3091897)------------------------------
% 6.38/1.87 % (3091897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.38/1.87 % (3091897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.87 % (3091897)CaDiCaL version: 2.1.3
% 6.38/1.87 % (3091897)Termination reason: Refutation not found, incomplete strategy
% 6.38/1.87 % (3091897)Time elapsed: 0.001 s
% 6.38/1.87 % (3091897)Peak memory usage: 86 MB
% 6.38/1.87 % (3091898)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2969655665:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 6.38/1.87 % (3091898)Refutation not found, incomplete strategy
% 6.38/1.87 % (3091898)------------------------------
% 6.38/1.87 % (3091898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.38/1.87 % (3091898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.87 % (3091898)CaDiCaL version: 2.1.3
% 6.38/1.87 % (3091898)Termination reason: Refutation not found, incomplete strategy
% 6.38/1.87 % (3091898)Time elapsed: 0.001 s
% 6.38/1.87 % (3091898)Peak memory usage: 87 MB
% 6.38/1.87 % (3091886)------------------------------
% 6.38/1.87 % (3091886)------------------------------
% 6.38/1.87 % (3091887)------------------------------
% 6.38/1.87 % (3091887)------------------------------
% 6.38/1.87 % (3091901)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1367519136:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 6.38/1.87 % (3091902)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=396908895:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 6.38/1.87 % (3091901)Refutation not found, incomplete strategy
% 6.38/1.87 % (3091901)------------------------------
% 6.38/1.87 % (3091901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.38/1.87 % (3091901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.87 % (3091901)CaDiCaL version: 2.1.3
% 6.38/1.87 % (3091901)Termination reason: Refutation not found, incomplete strategy
% 6.38/1.87 % (3091901)Time elapsed: 0.001 s
% 6.38/1.87 % (3091901)Peak memory usage: 86 MB
% 6.38/1.87 % (3091897)------------------------------
% 6.38/1.87 % (3091897)------------------------------
% 6.38/1.87 % (3091898)------------------------------
% 6.38/1.87 % (3091898)------------------------------
% 6.38/1.87 % (3091902)Instruction limit reached!
% 6.38/1.87 % (3091902)------------------------------
% 6.38/1.87 % (3091902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.38/1.87 % (3091902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.87 % (3091902)CaDiCaL version: 2.1.3
% 6.38/1.87 % (3091902)Termination reason: Instruction limit
% 6.38/1.87 % (3091902)Termination phase: Saturation
% 6.38/1.87 % (3091902)Time elapsed: 0.127 s
% 6.38/1.87 % (3091902)Peak memory usage: 88 MB
% 6.38/1.87 % (3091902)Instructions burned: 249 (million)
% 6.38/1.87 % (3091905)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3250916162:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 6.38/1.87 % (3091905)Refutation not found, incomplete strategy
% 6.38/1.87 % (3091905)------------------------------
% 6.38/1.87 % (3091905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.38/1.87 % (3091905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.87 % (3091905)CaDiCaL version: 2.1.3
% 6.38/1.87 % (3091905)Termination reason: Refutation not found, incomplete strategy
% 6.38/1.87 % (3091905)Time elapsed: 0.001 s
% 6.38/1.87 % (3091905)Peak memory usage: 86 MB
% 6.38/1.87 % (3091885)Refutation not found, incomplete strategy
% 6.38/1.87 % (3091885)------------------------------
% 6.38/1.87 % (3091885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.38/1.87 % (3091885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.87 % (3091885)CaDiCaL version: 2.1.3
% 6.38/1.87 % (3091885)Termination reason: Refutation not found, incomplete strategy
% 6.38/1.87 % (3091885)Time elapsed: 0.558 s
% 6.38/1.87 % (3091885)Peak memory usage: 127 MB
% 6.38/1.87 % (3091885)Instructions burned: 837 (million)
% 6.38/1.87 % (3091906)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3392651885:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 6.38/1.87 % (3091901)------------------------------
% 6.38/1.87 % (3091901)------------------------------
% 6.38/1.87 % (3091884)First to succeed.
% 6.38/1.87 % (3091884)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3091805"
% 6.38/1.87 % (3091907)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3085000218:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 6.38/1.87 % (3091907)Refutation not found, incomplete strategy
% 6.38/1.87 % (3091907)------------------------------
% 6.38/1.87 % (3091907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.38/1.87 % (3091907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/2.06 % (3091907)CaDiCaL version: 2.1.3
% 7.93/2.06 % (3091907)Termination reason: Refutation not found, incomplete strategy
% 7.93/2.06 % (3091907)Time elapsed: 0.002 s
% 7.93/2.06 % (3091907)Peak memory usage: 88 MB
% 7.93/2.06 % (3091907)Instructions burned: 2 (million)
% 7.93/2.06 % (3091911)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1887752319:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 7.93/2.06 % (3091911)Refutation not found, incomplete strategy
% 7.93/2.06 % (3091911)------------------------------
% 7.93/2.06 % (3091911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/2.06 % (3091911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/2.06 % (3091911)CaDiCaL version: 2.1.3
% 7.93/2.06 % (3091911)Termination reason: Refutation not found, incomplete strategy
% 7.93/2.06 % (3091911)Time elapsed: 0.002 s
% 7.93/2.06 % (3091911)Peak memory usage: 88 MB
% 7.93/2.06 % (3091911)Instructions burned: 3 (million)
% 7.93/2.06 % (3091905)------------------------------
% 7.93/2.06 % (3091905)------------------------------
% 7.93/2.06 % (3091885)------------------------------
% 7.93/2.06 % (3091885)------------------------------
% 7.93/2.06 % (3091907)------------------------------
% 7.93/2.06 % (3091907)------------------------------
% 7.93/2.06 % SZS status Satisfiable for theBenchmark
% 7.93/2.06 % SZS output start Saturation.
% See solution above
% 7.93/2.07 % SZS output start Definitions and Model Updates.
% 7.93/2.07 for all groundings,
% 7.93/2.07 whenever cowlThing(X0) is false, set cowlThing(X0) to true
% 7.93/2.07 for all groundings, until fixed point,
% 7.93/2.07 whenever cowlThing(X1) | ~cowlThing(X1) is false, set cowlThing(X1) to true
% 7.93/2.07 for all groundings,
% 7.93/2.07 whenever ~cowlNothing(X0) is false, set ~cowlNothing(X0) to true
% 7.93/2.07 for all groundings, until fixed point,
% 7.93/2.07 whenever cowlNothing(X1) | ~cowlNothing(X1) is false, set ~cowlNothing(X1) to true
% 7.93/2.07 % SZS output end Definitions and Model Updates.
% 7.93/2.07 % (3091884)------------------------------
% 7.93/2.07 % (3091884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/2.07 % (3091884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/2.07 % (3091884)CaDiCaL version: 2.1.3
% 7.93/2.07 % (3091884)Termination reason: Satisfiable
% 7.93/2.07 % (3091884)Time elapsed: 0.637 s
% 7.93/2.07 % (3091884)Peak memory usage: 128 MB
% 7.93/2.07 % (3091884)Instructions burned: 943 (million)
% 7.93/2.07 % (3091884)------------------------------
% 7.93/2.07 % (3091884)------------------------------
% 7.93/2.07 % (3091805)Success in time 1.034 s
% 7.93/2.07 % Vampire exiting
%------------------------------------------------------------------------------