%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP442-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/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 10:14:01 AM UTC 2026
% Result : Unsatisfiable 8.32s 1.98s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 6
% Syntax : Number of formulae : 79 ( 79 unt; 4 def)
% Number of atoms : 79 ( 78 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-2 aty)
% Number of variables : 137 ( 137 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
! [X2,X3,X0,X1] : inverse(multiply(X0,multiply(X1,multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,multiply(X0,X1))))))) = X3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
multiply(inverse(a1),a1) != multiply(inverse(b1),b1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms_1) ).
fof(f3,definition,
sF0 = inverse(a1),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f4,plain,
inverse(a1) = sF0,
inference(reorient_equations,[],[f3]) ).
fof(f5,definition,
sF1 = multiply(sF0,a1),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f6,plain,
multiply(sF0,a1) = sF1,
inference(reorient_equations,[],[f5]) ).
fof(f7,definition,
sF2 = inverse(b1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f8,plain,
inverse(b1) = sF2,
inference(reorient_equations,[],[f7]) ).
fof(f9,definition,
sF3 = multiply(sF2,b1),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f10,plain,
multiply(sF2,b1) = sF3,
inference(reorient_equations,[],[f9]) ).
fof(f11,plain,
sF1 != sF3,
inference(definition_folding,[],[f2,f10,f8,f6,f4]) ).
fof(f13,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(X1,multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X0,multiply(X3,X1)))),multiply(multiply(X4,inverse(X4)),X0)))) = X3,
inference(superposition,[],[f1,f1]) ).
fof(f14,plain,
! [X2,X0,X1] : inverse(multiply(X0,multiply(X1,multiply(multiply(a1,sF0),inverse(multiply(X2,multiply(X0,X1))))))) = X2,
inference(superposition,[],[f1,f4]) ).
fof(f15,plain,
! [X2,X0,X1] : inverse(multiply(X0,multiply(X1,multiply(multiply(b1,sF2),inverse(multiply(X2,multiply(X0,X1))))))) = X2,
inference(superposition,[],[f1,f8]) ).
fof(f18,plain,
! [X0] : inverse(multiply(sF0,multiply(a1,multiply(multiply(a1,sF0),inverse(multiply(X0,sF1)))))) = X0,
inference(superposition,[],[f14,f6]) ).
fof(f19,plain,
! [X0] : inverse(multiply(sF2,multiply(b1,multiply(multiply(a1,sF0),inverse(multiply(X0,sF3)))))) = X0,
inference(superposition,[],[f14,f10]) ).
fof(f52,plain,
! [X2,X3,X0,X1,X4,X5] : inverse(multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,multiply(X0,X3)))),multiply(multiply(multiply(X4,inverse(X4)),X2),multiply(multiply(X5,inverse(X5)),X0)))) = X3,
inference(superposition,[],[f1,f13]) ).
fof(f160,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(multiply(a1,sF0),inverse(multiply(X0,multiply(X2,X3)))) = inverse(multiply(multiply(multiply(X1,inverse(X1)),X0),multiply(multiply(multiply(X4,inverse(X4)),X2),multiply(multiply(X5,inverse(X5)),X3)))),
inference(superposition,[],[f52,f14]) ).
fof(f161,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(multiply(b1,sF2),inverse(multiply(X0,multiply(X2,X3)))) = inverse(multiply(multiply(multiply(X1,inverse(X1)),X0),multiply(multiply(multiply(X4,inverse(X4)),X2),multiply(multiply(X5,inverse(X5)),X3)))),
inference(superposition,[],[f52,f15]) ).
fof(f163,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] : multiply(multiply(X6,inverse(X6)),X4) = inverse(multiply(multiply(multiply(X1,inverse(X1)),X0),multiply(multiply(multiply(X7,inverse(X7)),multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,multiply(X4,X0))))),multiply(multiply(X8,inverse(X8)),multiply(multiply(X5,inverse(X5)),X3))))),
inference(superposition,[],[f52,f52]) ).
fof(f206,plain,
! [X2,X3,X0] : multiply(multiply(b1,sF2),inverse(multiply(inverse(multiply(X2,multiply(X0,X3))),multiply(X2,X0)))) = X3,
inference(backward_demodulation,[],[f52,f161]) ).
fof(f211,plain,
! [X2,X3,X0,X6,X4,X5] : multiply(multiply(X6,inverse(X6)),X4) = multiply(multiply(b1,sF2),inverse(multiply(X0,multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,multiply(X4,X0)))),multiply(multiply(X5,inverse(X5)),X3))))),
inference(backward_demodulation,[],[f163,f161]) ).
fof(f214,plain,
! [X2,X3,X0] : multiply(multiply(a1,sF0),inverse(multiply(X0,multiply(X2,X3)))) = multiply(multiply(b1,sF2),inverse(multiply(X0,multiply(X2,X3)))),
inference(backward_demodulation,[],[f161,f160]) ).
fof(f252,plain,
! [X6,X4] : multiply(multiply(X6,inverse(X6)),X4) = multiply(multiply(b1,sF2),X4),
inference(forward_demodulation,[],[f211,f13]) ).
fof(f336,plain,
! [X2,X3,X0] : multiply(multiply(a1,sF0),inverse(multiply(inverse(multiply(X2,multiply(X0,X3))),multiply(X2,X0)))) = X3,
inference(backward_demodulation,[],[f206,f214]) ).
fof(f602,plain,
! [X0] : multiply(X0,inverse(X0)) = inverse(multiply(sF0,multiply(a1,multiply(multiply(a1,sF0),inverse(multiply(multiply(b1,sF2),sF1)))))),
inference(superposition,[],[f18,f252]) ).
fof(f603,plain,
! [X0] : multiply(X0,inverse(X0)) = multiply(b1,sF2),
inference(forward_demodulation,[],[f602,f18]) ).
fof(f727,plain,
! [X0] : multiply(b1,sF2) = multiply(multiply(sF0,multiply(a1,multiply(multiply(a1,sF0),inverse(multiply(X0,sF1))))),X0),
inference(superposition,[],[f603,f18]) ).
fof(f728,plain,
multiply(a1,sF0) = multiply(b1,sF2),
inference(superposition,[],[f603,f4]) ).
fof(f729,plain,
! [X0,X1] : inverse(multiply(X0,multiply(inverse(X0),multiply(multiply(a1,sF0),inverse(multiply(X1,multiply(b1,sF2))))))) = X1,
inference(superposition,[],[f14,f603]) ).
fof(f730,plain,
! [X0,X1] : inverse(multiply(X0,multiply(inverse(X0),multiply(multiply(a1,sF0),inverse(multiply(X1,multiply(a1,sF0))))))) = X1,
inference(backward_demodulation,[],[f729,f728]) ).
fof(f733,plain,
! [X0] : multiply(X0,inverse(X0)) = multiply(a1,sF0),
inference(backward_demodulation,[],[f603,f728]) ).
fof(f734,plain,
! [X0] : multiply(a1,sF0) = multiply(multiply(sF0,multiply(a1,multiply(multiply(a1,sF0),inverse(multiply(X0,sF1))))),X0),
inference(forward_demodulation,[],[f727,f728]) ).
fof(f742,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(X2,multiply(X3,X0))),multiply(X2,X3))) = multiply(multiply(a1,sF0),inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,multiply(a1,sF0))))),
inference(superposition,[],[f336,f336]) ).
fof(f750,plain,
! [X0] : multiply(multiply(a1,sF0),inverse(multiply(inverse(multiply(sF0,multiply(a1,X0))),sF1))) = X0,
inference(superposition,[],[f336,f6]) ).
fof(f767,plain,
! [X0,X1] : multiply(multiply(a1,sF0),inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,multiply(a1,sF0))))) = inverse(multiply(inverse(multiply(sF0,multiply(a1,X0))),sF1)),
inference(superposition,[],[f336,f750]) ).
fof(f768,plain,
! [X2,X3,X0] : inverse(multiply(inverse(multiply(X2,multiply(X3,X0))),multiply(X2,X3))) = inverse(multiply(inverse(multiply(sF0,multiply(a1,X0))),sF1)),
inference(backward_demodulation,[],[f742,f767]) ).
fof(f897,plain,
! [X0,X1] : inverse(multiply(a1,multiply(sF0,X0))) = inverse(multiply(X1,multiply(inverse(X1),multiply(multiply(a1,sF0),inverse(multiply(inverse(multiply(sF0,multiply(a1,X0))),sF1)))))),
inference(superposition,[],[f730,f768]) ).
fof(f903,plain,
! [X0,X1] : inverse(multiply(a1,multiply(sF0,X0))) = inverse(multiply(X1,multiply(inverse(X1),X0))),
inference(forward_demodulation,[],[f897,f750]) ).
fof(f924,plain,
! [X0] : inverse(multiply(b1,multiply(sF2,X0))) = inverse(multiply(a1,multiply(sF0,X0))),
inference(superposition,[],[f903,f8]) ).
fof(f927,plain,
! [X0,X1] : inverse(multiply(inverse(X1),multiply(X0,multiply(multiply(a1,sF0),inverse(multiply(a1,multiply(sF0,X0))))))) = X1,
inference(superposition,[],[f14,f903]) ).
fof(f1072,plain,
! [X0,X1] : multiply(sF0,multiply(a1,multiply(multiply(a1,sF0),inverse(multiply(multiply(X0,X1),sF1))))) = inverse(multiply(X0,multiply(X1,multiply(multiply(a1,sF0),inverse(multiply(a1,sF0)))))),
inference(superposition,[],[f14,f734]) ).
fof(f1082,plain,
multiply(sF0,multiply(a1,multiply(multiply(a1,sF0),inverse(multiply(sF1,sF1))))) = inverse(multiply(sF0,multiply(a1,multiply(multiply(a1,sF0),inverse(multiply(a1,sF0)))))),
inference(superposition,[],[f18,f734]) ).
fof(f1095,plain,
multiply(sF0,multiply(a1,multiply(multiply(a1,sF0),inverse(multiply(sF1,sF1))))) = inverse(multiply(sF0,multiply(a1,multiply(a1,sF0)))),
inference(forward_demodulation,[],[f1082,f733]) ).
fof(f1098,plain,
! [X0,X1] : inverse(multiply(X0,multiply(X1,multiply(a1,sF0)))) = multiply(sF0,multiply(a1,multiply(multiply(a1,sF0),inverse(multiply(multiply(X0,X1),sF1))))),
inference(forward_demodulation,[],[f1072,f733]) ).
fof(f1143,plain,
! [X0,X1] : multiply(b1,multiply(sF2,X0)) = inverse(multiply(inverse(multiply(a1,multiply(sF0,X0))),multiply(X1,multiply(multiply(a1,sF0),inverse(multiply(a1,multiply(sF0,X1))))))),
inference(superposition,[],[f927,f924]) ).
fof(f1145,plain,
! [X2,X0,X1] : multiply(X1,multiply(inverse(X1),X0)) = inverse(multiply(inverse(multiply(a1,multiply(sF0,X0))),multiply(X2,multiply(multiply(a1,sF0),inverse(multiply(a1,multiply(sF0,X2))))))),
inference(superposition,[],[f927,f903]) ).
fof(f1149,plain,
! [X2,X0,X1] : multiply(inverse(X0),multiply(X1,multiply(multiply(a1,sF0),inverse(multiply(a1,multiply(sF0,X1)))))) = inverse(multiply(X0,multiply(X2,multiply(multiply(a1,sF0),inverse(multiply(a1,multiply(sF0,X2))))))),
inference(superposition,[],[f927,f927]) ).
fof(f1150,plain,
! [X0,X1] : multiply(sF0,multiply(a1,multiply(multiply(a1,sF0),inverse(multiply(X0,sF1))))) = inverse(multiply(X0,multiply(X1,multiply(multiply(a1,sF0),inverse(multiply(a1,multiply(sF0,X1))))))),
inference(superposition,[],[f927,f18]) ).
fof(f1151,plain,
! [X0,X1] : multiply(sF2,multiply(b1,multiply(multiply(a1,sF0),inverse(multiply(X0,sF3))))) = inverse(multiply(X0,multiply(X1,multiply(multiply(a1,sF0),inverse(multiply(a1,multiply(sF0,X1))))))),
inference(superposition,[],[f927,f19]) ).
fof(f1172,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(sF0,multiply(a1,X1))),sF1)) = multiply(X0,multiply(multiply(multiply(a1,sF0),inverse(multiply(a1,multiply(sF0,X0)))),X1)),
inference(superposition,[],[f768,f927]) ).
fof(f1195,plain,
! [X1] : multiply(sF2,multiply(b1,multiply(multiply(a1,sF0),inverse(multiply(inverse(X1),sF3))))) = X1,
inference(backward_demodulation,[],[f927,f1151]) ).
fof(f1197,plain,
! [X0] : multiply(sF0,multiply(a1,multiply(multiply(a1,sF0),inverse(multiply(X0,sF1))))) = multiply(sF2,multiply(b1,multiply(multiply(a1,sF0),inverse(multiply(X0,sF3))))),
inference(backward_demodulation,[],[f1151,f1150]) ).
fof(f1198,plain,
! [X0,X1] : multiply(sF0,multiply(a1,multiply(multiply(a1,sF0),inverse(multiply(X0,sF1))))) = multiply(inverse(X0),multiply(X1,multiply(multiply(a1,sF0),inverse(multiply(a1,multiply(sF0,X1)))))),
inference(forward_demodulation,[],[f1149,f1150]) ).
fof(f1202,plain,
! [X0,X1] : multiply(X1,multiply(inverse(X1),X0)) = multiply(sF0,multiply(a1,multiply(multiply(a1,sF0),inverse(multiply(inverse(multiply(a1,multiply(sF0,X0))),sF1))))),
inference(forward_demodulation,[],[f1145,f1150]) ).
fof(f1204,plain,
! [X0] : multiply(b1,multiply(sF2,X0)) = multiply(sF0,multiply(a1,multiply(multiply(a1,sF0),inverse(multiply(inverse(multiply(a1,multiply(sF0,X0))),sF1))))),
inference(forward_demodulation,[],[f1143,f1150]) ).
fof(f1220,plain,
! [X1] : multiply(sF0,multiply(a1,multiply(multiply(a1,sF0),inverse(multiply(inverse(X1),sF1))))) = X1,
inference(backward_demodulation,[],[f1195,f1197]) ).
fof(f1233,plain,
! [X0,X1] : multiply(b1,multiply(sF2,X0)) = multiply(X1,multiply(inverse(X1),X0)),
inference(backward_demodulation,[],[f1202,f1204]) ).
fof(f1235,plain,
! [X0] : multiply(b1,multiply(sF2,X0)) = multiply(a1,multiply(sF0,X0)),
inference(backward_demodulation,[],[f1204,f1220]) ).
fof(f1261,plain,
! [X0,X1] : multiply(a1,multiply(sF0,X0)) = multiply(X1,multiply(inverse(X1),X0)),
inference(backward_demodulation,[],[f1233,f1235]) ).
fof(f1307,plain,
! [X0,X1] : multiply(a1,multiply(sF0,X1)) = multiply(multiply(sF0,multiply(a1,multiply(multiply(a1,sF0),inverse(multiply(X0,sF1))))),multiply(X0,X1)),
inference(superposition,[],[f1261,f18]) ).
fof(f2137,plain,
multiply(a1,sF0) = multiply(inverse(multiply(sF0,multiply(a1,multiply(a1,sF0)))),sF1),
inference(superposition,[],[f734,f1095]) ).
fof(f3496,plain,
! [X0,X1] : multiply(X0,X1) = inverse(inverse(multiply(X0,multiply(X1,multiply(a1,sF0))))),
inference(superposition,[],[f18,f1098]) ).
fof(f3551,plain,
! [X0] : multiply(X0,multiply(sF0,multiply(a1,multiply(multiply(a1,sF0),inverse(multiply(a1,sF1)))))) = inverse(inverse(multiply(X0,multiply(a1,multiply(sF0,sF0))))),
inference(superposition,[],[f3496,f1307]) ).
fof(f3554,plain,
! [X0] : multiply(X0,multiply(multiply(a1,sF0),inverse(multiply(a1,multiply(sF0,X0))))) = inverse(inverse(inverse(multiply(inverse(multiply(sF0,multiply(a1,multiply(a1,sF0)))),sF1)))),
inference(superposition,[],[f3496,f1172]) ).
fof(f3579,plain,
! [X0] : multiply(X0,multiply(multiply(a1,sF0),inverse(multiply(a1,multiply(sF0,X0))))) = inverse(inverse(inverse(multiply(a1,sF0)))),
inference(forward_demodulation,[],[f3554,f2137]) ).
fof(f3586,plain,
! [X0] : multiply(sF0,multiply(a1,multiply(multiply(a1,sF0),inverse(multiply(X0,sF1))))) = multiply(inverse(X0),inverse(inverse(inverse(multiply(a1,sF0))))),
inference(backward_demodulation,[],[f1198,f3579]) ).
fof(f3633,plain,
! [X1] : multiply(inverse(inverse(X1)),inverse(inverse(inverse(multiply(a1,sF0))))) = X1,
inference(backward_demodulation,[],[f1220,f3586]) ).
fof(f3641,plain,
! [X0] : inverse(inverse(multiply(X0,multiply(a1,multiply(sF0,sF0))))) = multiply(X0,multiply(inverse(a1),inverse(inverse(inverse(multiply(a1,sF0)))))),
inference(backward_demodulation,[],[f3551,f3586]) ).
fof(f3654,plain,
! [X0] : inverse(inverse(multiply(X0,multiply(a1,multiply(sF0,sF0))))) = multiply(X0,multiply(sF0,inverse(inverse(inverse(multiply(a1,sF0)))))),
inference(forward_demodulation,[],[f3641,f4]) ).
fof(f3679,plain,
! [X0] : multiply(a1,multiply(sF0,inverse(inverse(inverse(multiply(a1,sF0)))))) = multiply(inverse(X0),X0),
inference(superposition,[],[f1261,f3633]) ).
fof(f3685,plain,
! [X0] : multiply(inverse(X0),X0) = inverse(inverse(multiply(a1,multiply(a1,multiply(sF0,sF0))))),
inference(forward_demodulation,[],[f3679,f3654]) ).
fof(f3702,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1),
inference(superposition,[],[f3685,f3685]) ).
fof(f3769,plain,
! [X0] : multiply(sF0,a1) = multiply(inverse(X0),X0),
inference(superposition,[],[f3702,f4]) ).
fof(f3770,plain,
! [X0] : multiply(sF2,b1) = multiply(inverse(X0),X0),
inference(superposition,[],[f3702,f8]) ).
fof(f3918,plain,
! [X0] : sF3 = multiply(inverse(X0),X0),
inference(forward_demodulation,[],[f3770,f10]) ).
fof(f3919,plain,
! [X0] : sF1 = multiply(inverse(X0),X0),
inference(forward_demodulation,[],[f3769,f6]) ).
fof(f3955,plain,
sF1 = sF3,
inference(backward_demodulation,[],[f3918,f3919]) ).
fof(f4413,plain,
$false,
inference(forward_subsumption_resolution,[],[f3955,f11]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP442-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n019.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 10:04:49 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 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
% 8.32/1.98 % (2854297)Detected a unit-equality problem, will run specialized UEQ schedule.
% 8.32/1.98 % (2854307)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3614860896:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 8.32/1.98 % (2854303)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=161230223:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 8.32/1.98 % (2854302)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=3629646009:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 8.32/1.98 % (2854305)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2148928965:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 8.32/1.98 % (2854304)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=1017213104:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 8.32/1.98 % (2854306)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=3814769489:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 8.32/1.98 % (2854308)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1209092125:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 8.32/1.98 % (2854305)Instruction limit reached!
% 8.32/1.98 % (2854305)------------------------------
% 8.32/1.98 % (2854305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.32/1.98 % (2854305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.32/1.98 % (2854305)CaDiCaL version: 2.1.3
% 8.32/1.98 % (2854305)Termination reason: Instruction limit
% 8.32/1.98 % (2854305)Termination phase: Saturation
% 8.32/1.98 % (2854305)Time elapsed: 0.077 s
% 8.32/1.98 % (2854305)Peak memory usage: 88 MB
% 8.32/1.98 % (2854305)Instructions burned: 137 (million)
% 8.32/1.98 % (2854307)Instruction limit reached!
% 8.32/1.98 % (2854307)------------------------------
% 8.32/1.98 % (2854307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.32/1.98 % (2854307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.32/1.98 % (2854307)CaDiCaL version: 2.1.3
% 8.32/1.98 % (2854307)Termination reason: Instruction limit
% 8.32/1.98 % (2854307)Termination phase: Saturation
% 8.32/1.98 % (2854307)Time elapsed: 0.082 s
% 8.32/1.98 % (2854307)Peak memory usage: 90 MB
% 8.32/1.98 % (2854307)Instructions burned: 257 (million)
% 8.32/1.98 % (2854306)Instruction limit reached!
% 8.32/1.98 % (2854306)------------------------------
% 8.32/1.98 % (2854306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.32/1.98 % (2854306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.32/1.98 % (2854306)CaDiCaL version: 2.1.3
% 8.32/1.98 % (2854306)Termination reason: Instruction limit
% 8.32/1.98 % (2854306)Termination phase: Saturation
% 8.32/1.98 % (2854306)Time elapsed: 0.091 s
% 8.32/1.98 % (2854306)Peak memory usage: 89 MB
% 8.32/1.98 % (2854306)Instructions burned: 182 (million)
% 8.32/1.98 % (2854317)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2458922370:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 8.32/1.98 % (2854316)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=234185257:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 8.32/1.98 % (2854318)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=686904117:i=215:ep=RSTC_2997 on theBenchmark for (2997ds/215Mi)
% 8.32/1.98 % (2854318)Instruction limit reached!
% 8.32/1.98 % (2854318)------------------------------
% 8.32/1.98 % (2854318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.32/1.98 % (2854318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.32/1.98 % (2854318)CaDiCaL version: 2.1.3
% 8.32/1.98 % (2854318)Termination reason: Instruction limit
% 8.32/1.98 % (2854318)Termination phase: Saturation
% 8.32/1.98 % (2854318)Time elapsed: 0.128 s
% 8.32/1.98 % (2854318)Peak memory usage: 91 MB
% 8.32/1.98 % (2854318)Instructions burned: 216 (million)
% 8.32/1.98 % (2854322)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=453800197:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2994 on theBenchmark for (2994ds/317Mi)
% 8.32/1.98 % (2854308)Instruction limit reached!
% 8.32/1.98 % (2854308)------------------------------
% 8.32/1.98 % (2854308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.32/1.98 % (2854308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.32/1.98 % (2854308)CaDiCaL version: 2.1.3
% 8.32/1.98 % (2854308)Termination reason: Instruction limit
% 8.32/1.98 % (2854308)Termination phase: Saturation
% 8.32/1.98 % (2854308)Time elapsed: 0.615 s
% 8.32/1.98 % (2854308)Peak memory usage: 98 MB
% 8.32/1.98 % (2854308)Instructions burned: 1189 (million)
% 8.32/1.98 % (2854322)Instruction limit reached!
% 8.32/1.98 % (2854322)------------------------------
% 8.32/1.98 % (2854322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.32/1.98 % (2854322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.32/1.98 % (2854322)CaDiCaL version: 2.1.3
% 8.32/1.98 % (2854322)Termination reason: Instruction limit
% 8.32/1.98 % (2854322)Termination phase: Saturation
% 8.32/1.98 % (2854322)Time elapsed: 0.155 s
% 8.32/1.98 % (2854322)Peak memory usage: 91 MB
% 8.32/1.98 % (2854322)Instructions burned: 317 (million)
% 8.32/1.98 % (2854324)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=3364715743:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2992 on theBenchmark for (2992ds/12125Mi)
% 8.32/1.98 % (2854325)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=1768030031:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2991 on theBenchmark for (2991ds/2836Mi)
% 8.32/1.98 % (2854304)First to succeed.
% 8.32/1.98 % (2854304)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2854297"
% 8.32/1.98 % (2854304)Refutation found. Thanks to Tanya!
% 8.32/1.98 % SZS status Unsatisfiable for theBenchmark
% 8.32/1.98 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/2.20 % (2854304)------------------------------
% 0.16/2.20 % (2854304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/2.20 % (2854304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/2.20 % (2854304)CaDiCaL version: 2.1.3
% 0.16/2.20 % (2854304)Termination reason: Refutation
% 0.16/2.20 % (2854304)Time elapsed: 1.016 s
% 0.16/2.20 % (2854304)Peak memory usage: 139 MB
% 0.16/2.20 % (2854304)Instructions burned: 2381 (million)
% 0.16/2.20 % (2854304)------------------------------
% 0.16/2.20 % (2854304)------------------------------
% 0.16/2.20 % (2854297)Success in time 1.36 s
% 0.16/2.20 % Vampire exiting
%------------------------------------------------------------------------------