%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : COL131+1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n017.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:38:04 AM UTC 2026
% Result : CounterSatisfiable 22.51s 3.95s
% Output : Saturation 22.51s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u108,axiom,
a(a(a(s,a(s,X0)),X1),a(k,X2)) = a(a(X0,a(X1,a(k,X2))),X2) ).
cnf(u100,negated_conjecture,
a(a(a(a(a(a(a(sK0,X2),X2),X2),X2),k),a(k,s)),a(a(s,k),a(a(sK1,k),k))) = a(a(a(a(sK0,k),a(s,k)),a(s,X2)),s) ).
cnf(u132,negated_conjecture,
a(a(X1,a(s,X1)),s) = a(a(a(a(s,a(X0,a(a(a(sK0,X0),a(sK3,sK0)),k))),s),X1),s) ).
cnf(u13,negated_conjecture,
a(k,a(a(s,k),k)) = a(a(a(a(a(a(a(sK2,X23),X22),X25),X24),a(a(s,a(a(a(a(a(a(a(X22,a(X23,s)),a(X23,s)),X23),sK2),sK2),sK1),k)),sK2)),s),sK1) ).
cnf(u92,negated_conjecture,
a(a(a(a(X1,a(a(a(sK0,X1),a(sK3,sK0)),k)),X0),a(s,X2)),s) = a(a(a(a(a(a(a(sK0,X2),X2),X2),X2),X0),a(k,s)),a(a(s,k),a(a(X0,k),k))) ).
cnf(u79,negated_conjecture,
a(a(a(s,a(a(a(a(a(a(sK0,X2),X2),X2),X2),a(X1,k)),a(k,s))),X3),a(a(s,k),a(a(a(X1,sK1),k),k))) = a(a(a(a(a(X0,a(a(a(sK0,X0),a(sK3,sK0)),k)),a(X1,a(a(sK0,k),a(s,k)))),a(s,X2)),s),a(X3,a(a(s,k),a(a(a(X1,sK1),k),k)))) ).
cnf(u52,axiom,
a(a(a(s,X1),a(k,X0)),X2) = a(a(X1,X2),X0) ).
cnf(u53,axiom,
a(X0,a(X1,X2)) = a(a(a(s,a(k,X0)),X1),X2) ).
cnf(u169,negated_conjecture,
a(a(X2,s),s) = a(a(a(X0,s),X2),s) ).
cnf(u44,negated_conjecture,
a(a(a(a(X9,a(a(a(sK0,X9),a(sK3,sK0)),k)),a(X8,a(a(sK0,k),a(s,k)))),a(s,X10)),s) = a(a(a(a(a(a(a(sK0,X10),X10),X10),X10),a(X8,k)),a(k,s)),a(a(s,k),a(a(a(X8,sK1),k),k))) ).
cnf(u102,axiom,
a(a(X0,X1),X0) = a(a(a(a(s,s),k),X0),X1) ).
cnf(u89,negated_conjecture,
a(a(a(a(a(a(sK0,a(a(s,k),X0)),a(sK3,sK0)),k),a(X1,a(a(sK0,k),a(s,k)))),a(s,X2)),s) = a(a(a(X1,a(a(sK0,k),a(s,k))),a(s,X2)),s) ).
cnf(u46,axiom,
a(a(a(s,a(a(s,X0),X2)),X3),X1) = a(a(a(X0,X1),a(X2,X1)),a(X3,X1)) ).
cnf(u213,negated_conjecture,
s = a(a(X0,X2),a(X1,X2)) ).
cnf(u215,negated_conjecture,
s = a(a(X0,X2),X1) ).
cnf(u74,negated_conjecture,
a(a(a(a(X0,a(a(a(sK0,X0),a(sK3,sK0)),k)),a(k,a(a(sK0,k),a(s,k)))),a(s,X1)),s) = a(a(a(a(a(a(a(sK0,X1),X1),X1),X1),a(k,k)),a(k,s)),a(a(s,k),a(sK1,k))) ).
cnf(u66,negated_conjecture,
a(a(a(a(a(a(a(sK0,a(X1,a(a(sK0,k),a(s,k)))),a(X1,a(a(sK0,k),a(s,k)))),a(X1,a(a(sK0,k),a(s,k)))),a(X1,a(a(sK0,k),a(s,k)))),a(X1,k)),a(k,s)),a(a(s,k),a(a(a(X1,sK1),k),k))) = a(a(a(a(s,a(X0,a(a(a(sK0,X0),a(sK3,sK0)),k))),s),a(X1,a(a(sK0,k),a(s,k)))),s) ).
cnf(u65,negated_conjecture,
a(a(a(a(a(a(a(sK0,X1),X1),X1),X1),a(X0,k)),a(k,s)),a(a(s,k),a(a(a(X0,sK1),k),k))) = a(a(a(X0,a(a(sK0,k),a(s,k))),a(s,X1)),s) ).
cnf(u76,negated_conjecture,
a(a(a(a(X0,a(a(a(sK0,X0),a(sK3,sK0)),k)),a(s,a(a(sK0,k),a(s,k)))),a(s,X1)),s) = a(a(a(a(a(a(a(sK0,X1),X1),X1),X1),a(s,k)),a(k,s)),a(a(s,k),a(a(sK1,k),a(k,k)))) ).
cnf(u159,negated_conjecture,
s = a(s,X0) ).
cnf(u78,negated_conjecture,
a(a(a(s,X3),a(a(a(a(a(a(sK0,X2),X2),X2),X2),a(X1,k)),a(k,s))),a(a(s,k),a(a(a(X1,sK1),k),k))) = a(a(X3,a(a(s,k),a(a(a(X1,sK1),k),k))),a(a(a(a(X0,a(a(a(sK0,X0),a(sK3,sK0)),k)),a(X1,a(a(sK0,k),a(s,k)))),a(s,X2)),s)) ).
cnf(u236,negated_conjecture,
s = X0 ).
cnf(u82,negated_conjecture,
a(a(a(a(X2,a(a(a(sK0,X2),a(sK3,sK0)),k)),a(a(a(s,X0),X1),a(a(sK0,k),a(s,k)))),a(s,X3)),s) = a(a(a(a(a(a(a(sK0,X3),X3),X3),X3),a(a(X0,k),a(X1,k))),a(k,s)),a(a(s,k),a(a(a(a(X0,sK1),a(X1,sK1)),k),k))) ).
cnf(u57,axiom,
a(X0,X1) = a(a(a(s,a(s,k)),X0),X1) ).
cnf(u58,axiom,
a(a(a(s,X1),a(a(s,k),X2)),X0) = a(a(X1,X0),X0) ).
cnf(u151,negated_conjecture,
a(a(s,X0),s) = a(a(X1,a(s,X0)),s) ).
cnf(u51,axiom,
a(a(a(s,k),X1),X0) = X0 ).
cnf(u20,axiom,
a(a(k,X0),X1) = X0 ).
cnf(u12,negated_conjecture,
a(s,a(a(X27,a(s,a(s,X26))),k)) = a(a(a(a(a(a(a(sK3,X26),X27),X26),X26),a(a(s,sK0),sK1)),a(k,X28)),a(a(a(a(a(a(X28,s),k),sK1),X26),k),s)) ).
cnf(u95,negated_conjecture,
a(a(a(a(X0,a(a(a(sK0,X0),a(sK3,sK0)),k)),a(a(sK0,k),a(s,k))),a(s,X2)),s) = a(a(a(a(sK0,k),a(s,k)),a(s,X2)),s) ).
cnf(u176,negated_conjecture,
s = a(a(X1,s),s) ).
cnf(u131,negated_conjecture,
a(a(X0,a(s,X1)),s) = a(a(a(a(a(sK0,k),a(sK3,sK0)),k),a(s,X1)),s) ).
cnf(u263,negated_conjecture,
X0 = X1 ).
cnf(u49,axiom,
a(a(a(s,X3),a(X0,X2)),a(X1,X2)) = a(a(X3,a(X1,X2)),a(a(a(s,X0),X1),X2)) ).
cnf(u109,axiom,
a(a(a(s,X3),a(a(s,X0),a(k,X2))),X1) = a(a(X3,X1),a(a(X0,X1),X2)) ).
cnf(u41,negated_conjecture,
a(s,a(a(s,a(a(sK3,a(k,X21)),a(a(a(a(a(a(a(a(a(X21,sK3),sK1),sK2),sK1),k),k),X19),sK0),sK0))),a(a(a(a(a(X20,sK2),sK1),X19),X20),X21))) = a(a(a(a(a(a(a(a(a(a(sK2,X21),X20),X20),X20),a(a(a(a(s,sK1),s),a(a(sK0,a(a(X19,s),s)),s)),sK3)),X20),a(a(s,a(s,sK1)),a(s,s))),a(a(s,a(X18,k)),X20)),s),a(a(a(X20,sK0),k),k)) ).
cnf(u48,axiom,
a(a(a(s,X3),a(a(s,X0),X2)),X1) = a(a(X3,X1),a(a(X0,X1),a(X2,X1))) ).
cnf(u35,negated_conjecture,
a(a(a(X7,s),a(sK3,a(a(s,s),sK3))),sK3) = a(a(a(a(a(a(a(sK0,X7),X6),X5),X6),a(X5,a(s,a(a(a(a(sK0,s),k),s),k)))),sK2),k) ).
cnf(u45,axiom,
a(a(X1,X2),a(a(X0,X1),X2)) = a(a(a(a(s,s),X0),X1),X2) ).
cnf(u200,negated_conjecture,
a(s,X1) = X1 ).
cnf(u37,negated_conjecture,
a(a(a(a(a(a(a(sK1,X12),X13),X12),X12),a(sK2,a(sK0,s))),X14),k) = a(a(a(X14,a(X13,a(s,X13))),a(k,k)),s) ).
cnf(u126,negated_conjecture,
a(a(X1,a(s,X2)),s) = a(a(a(X0,X1),a(s,X2)),s) ).
cnf(u73,negated_conjecture,
a(a(a(a(X1,a(a(a(sK0,X1),a(sK3,sK0)),k)),a(a(s,X0),a(a(sK0,k),a(s,k)))),a(s,X2)),s) = a(a(a(a(a(a(a(sK0,X2),X2),X2),X2),a(a(s,X0),k)),a(k,s)),a(a(s,k),a(a(a(X0,k),a(sK1,k)),k))) ).
cnf(u124,negated_conjecture,
a(a(a(a(X0,a(a(sK0,k),a(s,k))),X1),a(s,X3)),s) = a(a(a(a(a(a(a(sK0,X3),X3),X3),X3),a(a(X0,k),X1)),a(k,s)),a(a(s,k),a(a(a(a(X0,sK1),X1),k),k))) ).
cnf(u75,negated_conjecture,
a(a(a(a(X0,a(a(a(sK0,X0),a(sK3,sK0)),k)),a(a(s,k),a(a(sK0,k),a(s,k)))),a(s,X1)),s) = a(a(a(a(a(a(a(sK0,X1),X1),X1),X1),a(a(s,k),k)),a(k,s)),a(a(s,k),a(k,k))) ).
cnf(u31,negated_conjecture,
a(s,a(a(s,sK3),a(X29,sK1))) = a(a(a(a(a(a(a(sK3,X31),X31),X31),X32),a(a(a(a(sK0,a(X29,sK2)),a(s,s)),X30),s)),X29),s) ).
cnf(u77,negated_conjecture,
a(a(a(a(X0,a(a(a(sK0,X0),a(sK3,sK0)),k)),a(X1,a(a(sK0,k),a(s,k)))),a(s,X2)),s) = a(a(a(a(X3,a(a(a(sK0,X3),a(sK3,sK0)),k)),a(X1,a(a(sK0,k),a(s,k)))),a(s,X2)),s) ).
cnf(u47,axiom,
a(a(a(s,a(X0,X2)),X3),a(X1,X2)) = a(a(a(a(s,X0),X1),X2),a(X3,a(X1,X2))) ).
cnf(u19,axiom,
a(a(a(s,X0),X1),X2) = a(a(X0,X2),a(X1,X2)) ).
cnf(u158,negated_conjecture,
a(a(X0,a(s,X1)),s) = a(a(X0,s),a(a(s,X1),s)) ).
cnf(u150,negated_conjecture,
a(X0,s) = a(a(X0,a(s,X1)),s) ).
cnf(u110,axiom,
a(a(a(s,a(a(s,X0),a(k,X2))),X3),X1) = a(a(a(X0,X1),X2),a(X3,X1)) ).
cnf(u136,negated_conjecture,
a(a(a(a(a(a(sK0,s),a(sK3,sK0)),k),a(s,X0)),X1),s) = a(X1,s) ).
cnf(u15,negated_conjecture,
a(k,a(a(sK3,sK3),sK0)) = a(a(a(a(a(a(a(a(sK1,X15),X15),X16),X15),a(sK1,a(k,k))),a(a(a(X17,X17),a(sK0,s)),a(k,sK1))),a(sK1,k)),s) ).
cnf(u96,negated_conjecture,
a(a(a(a(X1,a(a(a(sK0,X1),a(sK3,sK0)),k)),X0),a(s,X2)),s) = a(a(X0,a(s,X2)),s) ).
cnf(u59,axiom,
a(a(a(s,a(a(s,k),X1)),X2),X0) = a(X0,a(X2,X0)) ).
cnf(u90,negated_conjecture,
a(a(a(X0,a(X1,a(a(sK0,k),a(s,k)))),a(s,X2)),s) = a(a(a(X1,a(a(sK0,k),a(s,k))),a(s,X2)),s) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COL131+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.17 % Computer : n017.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Mon Sep 28 21:37:06 UTC 2026
% 0.09/0.17 % CPUTime :
% 0.09/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running first-order theorem proving
% 0.09/0.21 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
% 12.93/2.51 % (4063969)Detected formulas, will run a generic FOF schedule.
% 12.93/2.51 % (4063980)dis-21_1_sil=8000:lcm=predicate:random_seed=2717440813: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)
% 12.93/2.51 % (4063980)Refutation not found, incomplete strategy
% 12.93/2.51 % (4063980)------------------------------
% 12.93/2.51 % (4063980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.93/2.51 % (4063980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.93/2.51 % (4063980)CaDiCaL version: 2.1.3
% 12.93/2.51 % (4063980)Termination reason: Refutation not found, incomplete strategy
% 12.93/2.51 % (4063980)Time elapsed: 0.001 s
% 12.93/2.51 % (4063980)Peak memory usage: 88 MB
% 12.93/2.51 % (4063980)Instructions burned: 3 (million)
% 12.93/2.51 % (4063979)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4015663330:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.93/2.51 % (4063978)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1424674006:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.93/2.51 % (4063974)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=4072915228:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.93/2.51 % (4063976)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=2186331239:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.93/2.51 % (4063975)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=471855337:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.93/2.51 % (4063977)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2747354184:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.93/2.51 % (4063977)Instruction limit reached!
% 12.93/2.51 % (4063977)------------------------------
% 12.93/2.51 % (4063977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.93/2.51 % (4063977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.93/2.51 % (4063977)CaDiCaL version: 2.1.3
% 12.93/2.51 % (4063977)Termination reason: Instruction limit
% 12.93/2.51 % (4063977)Termination phase: Saturation
% 12.93/2.51 % (4063977)Time elapsed: 0.063 s
% 12.93/2.51 % (4063977)Peak memory usage: 89 MB
% 12.93/2.51 % (4063977)Instructions burned: 111 (million)
% 12.93/2.51 % (4063978)Instruction limit reached!
% 12.93/2.51 % (4063978)------------------------------
% 12.93/2.51 % (4063978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.93/2.51 % (4063978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.93/2.51 % (4063978)CaDiCaL version: 2.1.3
% 12.93/2.51 % (4063978)Termination reason: Instruction limit
% 12.93/2.51 % (4063978)Termination phase: Saturation
% 12.93/2.51 % (4063978)Time elapsed: 0.065 s
% 12.93/2.51 % (4063978)Peak memory usage: 88 MB
% 12.93/2.51 % (4063978)Instructions burned: 119 (million)
% 12.93/2.51 % (4063979)Instruction limit reached!
% 12.93/2.51 % (4063979)------------------------------
% 12.93/2.51 % (4063979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.93/2.51 % (4063979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.93/2.51 % (4063979)CaDiCaL version: 2.1.3
% 12.93/2.51 % (4063979)Termination reason: Instruction limit
% 12.93/2.51 % (4063979)Termination phase: Saturation
% 12.93/2.51 % (4063979)Time elapsed: 0.075 s
% 12.93/2.51 % (4063979)Peak memory usage: 89 MB
% 12.93/2.51 % (4063979)Instructions burned: 139 (million)
% 12.93/2.51 % (4063980)------------------------------
% 12.93/2.51 % (4063980)------------------------------
% 12.93/2.51 % (4063989)lrs+10_1_sil=32000:urr=on:br=off:random_seed=742036220:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 12.93/2.51 % (4063988)lrs+10_1_sil=8000:sp=occurrence:random_seed=1707983645:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 12.93/2.51 % (4063991)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=2250881884:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 12.93/2.51 % (4063990)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1691505410:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 19.50/3.45 % (4063991)Instruction limit reached!
% 19.50/3.45 % (4063991)------------------------------
% 19.50/3.45 % (4063991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.50/3.45 % (4063991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.50/3.45 % (4063991)CaDiCaL version: 2.1.3
% 19.50/3.45 % (4063991)Termination reason: Instruction limit
% 19.50/3.45 % (4063991)Termination phase: Saturation
% 19.50/3.45 % (4063991)Time elapsed: 0.076 s
% 19.50/3.45 % (4063991)Peak memory usage: 91 MB
% 19.50/3.45 % (4063991)Instructions burned: 250 (million)
% 19.50/3.45 % (4063989)Instruction limit reached!
% 19.50/3.45 % (4063989)------------------------------
% 19.50/3.45 % (4063989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.50/3.45 % (4063989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.50/3.45 % (4063989)CaDiCaL version: 2.1.3
% 19.50/3.45 % (4063989)Termination reason: Instruction limit
% 19.50/3.45 % (4063989)Termination phase: Saturation
% 19.50/3.45 % (4063989)Time elapsed: 0.093 s
% 19.50/3.45 % (4063989)Peak memory usage: 90 MB
% 19.50/3.45 % (4063989)Instructions burned: 157 (million)
% 19.50/3.45 % (4063988)Instruction limit reached!
% 19.50/3.45 % (4063988)------------------------------
% 19.50/3.45 % (4063988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.50/3.45 % (4063988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.50/3.45 % (4063988)CaDiCaL version: 2.1.3
% 19.50/3.45 % (4063988)Termination reason: Instruction limit
% 19.50/3.45 % (4063988)Termination phase: Saturation
% 19.50/3.45 % (4063988)Time elapsed: 0.167 s
% 19.50/3.45 % (4063988)Peak memory usage: 91 MB
% 19.50/3.45 % (4063988)Instructions burned: 286 (million)
% 19.50/3.45 % (4063996)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=441718295:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 19.50/3.45 % (4063990)Instruction limit reached!
% 19.50/3.45 % (4063990)------------------------------
% 19.50/3.45 % (4063990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.50/3.45 % (4063990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.50/3.45 % (4063990)CaDiCaL version: 2.1.3
% 19.50/3.45 % (4063990)Termination reason: Instruction limit
% 19.50/3.45 % (4063990)Termination phase: Saturation
% 19.50/3.45 % (4063990)Time elapsed: 0.190 s
% 19.50/3.45 % (4063990)Peak memory usage: 92 MB
% 19.50/3.45 % (4063990)Instructions burned: 325 (million)
% 19.50/3.45 % (4063997)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=343469863:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 19.50/3.45 % (4063996)Instruction limit reached!
% 19.50/3.45 % (4063996)------------------------------
% 19.50/3.45 % (4063996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.50/3.45 % (4063996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.50/3.45 % (4063996)CaDiCaL version: 2.1.3
% 19.50/3.45 % (4063996)Termination reason: Instruction limit
% 19.50/3.45 % (4063996)Termination phase: Saturation
% 19.50/3.45 % (4063996)Time elapsed: 0.091 s
% 19.50/3.45 % (4063996)Peak memory usage: 91 MB
% 19.50/3.45 % (4063996)Instructions burned: 295 (million)
% 19.50/3.45 % (4063998)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3555653536:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 19.50/3.45 % (4064000)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4287464598:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 19.50/3.45 % (4064000)Refutation not found, incomplete strategy
% 19.50/3.45 % (4064000)------------------------------
% 19.50/3.45 % (4064000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.50/3.45 % (4064000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.50/3.45 % (4064000)CaDiCaL version: 2.1.3
% 19.50/3.45 % (4064000)Termination reason: Refutation not found, incomplete strategy
% 19.50/3.45 % (4064000)Time elapsed: 0.003 s
% 19.50/3.45 % (4064000)Peak memory usage: 87 MB
% 19.50/3.45 % (4064000)Instructions burned: 3 (million)
% 19.50/3.45 % (4063998)Instruction limit reached!
% 19.50/3.45 % (4063998)------------------------------
% 19.50/3.45 % (4063998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.50/3.45 % (4063998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.50/3.45 % (4063998)CaDiCaL version: 2.1.3
% 21.27/3.75 % (4063998)Termination reason: Instruction limit
% 21.27/3.75 % (4063998)Termination phase: Saturation
% 21.27/3.75 % (4063998)Time elapsed: 0.072 s
% 21.27/3.75 % (4063998)Peak memory usage: 89 MB
% 21.27/3.75 % (4063998)Instructions burned: 113 (million)
% 21.27/3.75 % (4064002)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=108313916:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 21.27/3.75 % (4064002)Instruction limit reached!
% 21.27/3.75 % (4064002)------------------------------
% 21.27/3.75 % (4064002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.27/3.75 % (4064002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.27/3.75 % (4064002)CaDiCaL version: 2.1.3
% 21.27/3.75 % (4064002)Termination reason: Instruction limit
% 21.27/3.75 % (4064002)Termination phase: Saturation
% 21.27/3.75 % (4064002)Time elapsed: 0.063 s
% 21.27/3.75 % (4064002)Peak memory usage: 89 MB
% 21.27/3.75 % (4064002)Instructions burned: 115 (million)
% 21.27/3.75 % (4064005)lrs+10_1_sil=8000:sp=occurrence:random_seed=247808782:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 21.27/3.75 % (4064000)------------------------------
% 21.27/3.75 % (4064000)------------------------------
% 21.27/3.75 % (4064007)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1185989832:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 21.27/3.75 % (4064009)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3428033660:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 21.27/3.75 % (4064007)Instruction limit reached!
% 21.27/3.75 % (4064007)------------------------------
% 21.27/3.75 % (4064007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.27/3.75 % (4064007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.27/3.75 % (4064007)CaDiCaL version: 2.1.3
% 21.27/3.75 % (4064007)Termination reason: Instruction limit
% 21.27/3.75 % (4064007)Termination phase: Saturation
% 21.27/3.75 % (4064007)Time elapsed: 0.234 s
% 21.27/3.75 % (4064007)Peak memory usage: 92 MB
% 21.27/3.75 % (4064007)Instructions burned: 437 (million)
% 21.27/3.75 % (4064005)Instruction limit reached!
% 21.27/3.75 % (4064005)------------------------------
% 21.27/3.75 % (4064005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.27/3.75 % (4064005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.27/3.75 % (4064005)CaDiCaL version: 2.1.3
% 21.27/3.75 % (4064005)Termination reason: Instruction limit
% 21.27/3.75 % (4064005)Termination phase: Saturation
% 21.27/3.75 % (4064005)Time elapsed: 0.515 s
% 21.27/3.75 % (4064005)Peak memory usage: 98 MB
% 21.27/3.75 % (4064005)Instructions burned: 908 (million)
% 21.27/3.75 % (4064012)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2096673702:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 21.27/3.75 % (4064012)Refutation not found, incomplete strategy
% 21.27/3.75 % (4064012)------------------------------
% 21.27/3.75 % (4064012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.27/3.75 % (4064012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.27/3.75 % (4064012)CaDiCaL version: 2.1.3
% 21.27/3.75 % (4064012)Termination reason: Refutation not found, incomplete strategy
% 21.27/3.75 % (4064012)Time elapsed: 0.003 s
% 21.27/3.75 % (4064012)Peak memory usage: 88 MB
% 21.27/3.75 % (4064012)Instructions burned: 4 (million)
% 21.27/3.75 % (4064014)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=214779657:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 21.27/3.75 % (4064014)Refutation not found, incomplete strategy
% 21.27/3.75 % (4064014)------------------------------
% 21.27/3.75 % (4064014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.27/3.75 % (4064014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.27/3.75 % (4064014)CaDiCaL version: 2.1.3
% 21.27/3.75 % (4064014)Termination reason: Refutation not found, incomplete strategy
% 21.27/3.75 % (4064014)Time elapsed: 0.002 s
% 21.27/3.75 % (4064014)Peak memory usage: 88 MB
% 21.27/3.75 % (4064014)Instructions burned: 3 (million)
% 21.27/3.75 % (4064012)------------------------------
% 21.27/3.75 % (4064012)------------------------------
% 21.27/3.75 % (4064014)------------------------------
% 21.27/3.75 % (4064014)------------------------------
% 21.27/3.75 % (4064016)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4289119832:st=3:i=13193:sd=3:ss=axioms_2982 on theBenchmark for (2982ds/13193Mi)
% 21.27/3.75 % (4063997)Instruction limit reached!
% 21.27/3.75 % (4063997)------------------------------
% 21.27/3.75 % (4063997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.27/3.75 % (4063997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.27/3.75 % (4063997)CaDiCaL version: 2.1.3
% 21.27/3.75 % (4063997)Termination reason: Instruction limit
% 21.27/3.75 % (4063997)Termination phase: Saturation
% 21.27/3.75 % (4063997)Time elapsed: 1.360 s
% 21.27/3.75 % (4063997)Peak memory usage: 142 MB
% 21.27/3.75 % (4063997)Instructions burned: 2351 (million)
% 21.27/3.75 % (4064018)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=4279343828:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/125Mi)
% 21.27/3.75 % (4064018)Instruction limit reached!
% 21.27/3.75 % (4064018)------------------------------
% 21.27/3.75 % (4064018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.27/3.75 % (4064018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.27/3.75 % (4064018)CaDiCaL version: 2.1.3
% 21.27/3.75 % (4064018)Termination reason: Instruction limit
% 21.27/3.75 % (4064018)Termination phase: Saturation
% 21.27/3.75 % (4064018)Time elapsed: 0.074 s
% 21.27/3.75 % (4064018)Peak memory usage: 90 MB
% 21.27/3.75 % (4064018)Instructions burned: 126 (million)
% 21.27/3.75 % (4064019)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2185701413:i=134:gtgl=5:slsql=off:gtg=exists_sym_2980 on theBenchmark for (2980ds/134Mi)
% 21.27/3.75 % (4064019)Instruction limit reached!
% 21.27/3.75 % (4064019)------------------------------
% 21.27/3.75 % (4064019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.27/3.75 % (4064019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.27/3.75 % (4064019)CaDiCaL version: 2.1.3
% 21.27/3.75 % (4064019)Termination reason: Instruction limit
% 21.27/3.75 % (4064019)Termination phase: Saturation
% 21.27/3.75 % (4064019)Time elapsed: 0.078 s
% 21.27/3.75 % (4064019)Peak memory usage: 90 MB
% 21.27/3.75 % (4064019)Instructions burned: 135 (million)
% 21.27/3.75 % (4064021)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1447356630:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/141Mi)
% 21.27/3.75 % (4064021)Refutation not found, incomplete strategy
% 21.27/3.75 % (4064021)------------------------------
% 21.27/3.75 % (4064021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.27/3.75 % (4064021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.27/3.75 % (4064021)CaDiCaL version: 2.1.3
% 21.27/3.75 % (4064021)Termination reason: Refutation not found, incomplete strategy
% 21.27/3.75 % (4064021)Time elapsed: 0.002 s
% 21.27/3.75 % (4064021)Peak memory usage: 88 MB
% 21.27/3.75 % (4064021)Instructions burned: 2 (million)
% 21.27/3.75 % (4064023)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=574244858:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2977 on theBenchmark for (2977ds/431Mi)
% 21.27/3.75 % (4064023)Refutation not found, incomplete strategy
% 21.27/3.75 % (4064023)------------------------------
% 21.27/3.75 % (4064023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.27/3.75 % (4064023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.27/3.75 % (4064023)CaDiCaL version: 2.1.3
% 21.27/3.75 % (4064023)Termination reason: Refutation not found, incomplete strategy
% 21.27/3.75 % (4064023)Time elapsed: 0.003 s
% 21.27/3.75 % (4064023)Peak memory usage: 88 MB
% 21.27/3.75 % (4064023)Instructions burned: 4 (million)
% 21.27/3.75 % (4064021)------------------------------
% 21.27/3.75 % (4064021)------------------------------
% 21.27/3.75 % (4064023)------------------------------
% 21.27/3.75 % (4064023)------------------------------
% 21.27/3.75 % (4064026)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=697259128:i=6060:aac=none:ins=25_2975 on theBenchmark for (2975ds/6060Mi)
% 21.27/3.75 % (4064027)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=1676643688:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2973 on theBenchmark for (2973ds/150Mi)
% 22.51/3.95 % (4064016)First to succeed.
% 22.51/3.95 % (4064016)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4063969"
% 22.51/3.95 % (4064027)Instruction limit reached!
% 22.51/3.95 % (4064027)------------------------------
% 22.51/3.95 % (4064027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.51/3.95 % (4064027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.51/3.95 % (4064027)CaDiCaL version: 2.1.3
% 22.51/3.95 % (4064027)Termination reason: Instruction limit
% 22.51/3.95 % (4064027)Termination phase: Saturation
% 22.51/3.95 % (4064027)Time elapsed: 0.090 s
% 22.51/3.95 % (4064027)Peak memory usage: 90 MB
% 22.51/3.95 % (4064027)Instructions burned: 151 (million)
% 22.51/3.95 % (4064030)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2531934271:i=14155:bd=all_2971 on theBenchmark for (2971ds/14155Mi)
% 22.51/3.95 % SZS status CounterSatisfiable for theBenchmark
% 22.51/3.95 % SZS output start Saturation.
% See solution above
% 22.51/3.95 % SZS output start Definitions and Model Updates.
% 22.51/3.95 % SZS output end Definitions and Model Updates.
% 22.51/3.95 % (4064016)------------------------------
% 22.51/3.95 % (4064016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.51/3.95 % (4064016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.51/3.95 % (4064016)CaDiCaL version: 2.1.3
% 22.51/3.95 % (4064016)Termination reason: Satisfiable
% 22.51/3.95 % (4064016)Time elapsed: 0.966 s
% 22.51/3.95 % (4064016)Peak memory usage: 135 MB
% 22.51/3.95 % (4064016)Instructions burned: 1527 (million)
% 22.51/3.95 % (4064016)------------------------------
% 22.51/3.95 % (4064016)------------------------------
% 22.51/3.95 % (4063969)Success in time 3.097 s
% 22.51/3.95 % Vampire exiting
%------------------------------------------------------------------------------