%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL149-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.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:51:20 AM UTC 2026
% Result : Unsatisfiable 100.78s 17.68s
% Output : Refutation 117.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 13
% Syntax : Number of formulae : 207 ( 207 unt; 7 def)
% Number of atoms : 207 ( 206 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 11 con; 0-2 aty)
% Number of variables : 330 ( 330 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : implies(truth,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wajsberg_1) ).
fof(f2,axiom,
! [X2,X0,X1] : implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))) = truth,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wajsberg_2) ).
fof(f3,plain,
! [X2,X0,X1] : truth = implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X0,X1] : implies(implies(X0,X1),X1) = implies(implies(X1,X0),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wajsberg_3) ).
fof(f5,axiom,
! [X0,X1] : implies(implies(not(X0),not(X1)),implies(X1,X0)) = truth,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wajsberg_4) ).
fof(f6,plain,
! [X0,X1] : truth = implies(implies(not(X0),not(X1)),implies(X1,X0)),
inference(reorient_equations,[],[f5]) ).
fof(f7,axiom,
! [X0,X1] : big_V(X0,X1) = implies(implies(X0,X1),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',big_V_definition) ).
fof(f8,plain,
! [X0,X1] : implies(implies(X0,X1),X1) = big_V(X0,X1),
inference(reorient_equations,[],[f7]) ).
fof(f14,negated_conjecture,
implies(x,big_V(y,z)) != big_V(implies(x,y),implies(x,z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_wajsberg_theorem) ).
fof(f16,plain,
implies(x,implies(implies(y,z),z)) != implies(implies(implies(x,y),implies(x,z)),implies(x,z)),
inference(definition_unfolding,[],[f14,f8,f8]) ).
fof(f17,definition,
sF0 = implies(y,z),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f18,plain,
implies(y,z) = sF0,
inference(reorient_equations,[],[f17]) ).
fof(f19,definition,
sF1 = implies(sF0,z),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f20,plain,
implies(sF0,z) = sF1,
inference(reorient_equations,[],[f19]) ).
fof(f21,definition,
sF2 = implies(x,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f22,plain,
implies(x,sF1) = sF2,
inference(reorient_equations,[],[f21]) ).
fof(f23,definition,
sF3 = implies(x,y),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f24,plain,
implies(x,y) = sF3,
inference(reorient_equations,[],[f23]) ).
fof(f25,definition,
sF4 = implies(x,z),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f26,plain,
implies(x,z) = sF4,
inference(reorient_equations,[],[f25]) ).
fof(f27,definition,
sF5 = implies(sF3,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f28,plain,
implies(sF3,sF4) = sF5,
inference(reorient_equations,[],[f27]) ).
fof(f29,definition,
sF6 = implies(sF5,sF4),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f30,plain,
implies(sF5,sF4) = sF6,
inference(reorient_equations,[],[f29]) ).
fof(f31,plain,
sF2 != sF6,
inference(definition_folding,[],[f16,f30,f26,f28,f26,f24,f22,f20,f18]) ).
fof(f35,plain,
implies(sF0,z) = implies(implies(z,y),y),
inference(superposition,[],[f4,f18]) ).
fof(f36,plain,
sF1 = implies(implies(z,y),y),
inference(forward_demodulation,[],[f35,f20]) ).
fof(f41,plain,
! [X2,X3,X0,X1] : truth = implies(truth,implies(implies(implies(implies(X1,X2),implies(X0,X2)),X3),implies(implies(X0,X1),X3))),
inference(superposition,[],[f3,f3]) ).
fof(f52,plain,
! [X0,X1] : truth = implies(implies(truth,X1),implies(implies(X1,X0),X0)),
inference(superposition,[],[f3,f1]) ).
fof(f61,plain,
! [X2,X0,X1] : implies(implies(implies(implies(X1,X2),implies(X0,X2)),implies(X0,X1)),implies(X0,X1)) = implies(truth,implies(implies(X1,X2),implies(X0,X2))),
inference(superposition,[],[f4,f3]) ).
fof(f62,plain,
! [X2,X0,X1] : implies(implies(X1,X2),implies(X0,X2)) = implies(implies(implies(implies(X1,X2),implies(X0,X2)),implies(X0,X1)),implies(X0,X1)),
inference(forward_demodulation,[],[f61,f1]) ).
fof(f64,plain,
! [X0,X1] : truth = implies(X1,implies(implies(X1,X0),X0)),
inference(forward_demodulation,[],[f52,f1]) ).
fof(f66,plain,
! [X2,X3,X0,X1] : truth = implies(implies(implies(implies(X1,X2),implies(X0,X2)),X3),implies(implies(X0,X1),X3)),
inference(forward_demodulation,[],[f41,f1]) ).
fof(f77,plain,
implies(sF5,sF4) = implies(implies(sF4,sF3),sF3),
inference(superposition,[],[f4,f28]) ).
fof(f78,plain,
sF6 = implies(implies(sF4,sF3),sF3),
inference(forward_demodulation,[],[f77,f30]) ).
fof(f90,plain,
! [X2,X0,X1] : implies(implies(implies(X0,X1),X1),implies(X2,X0)) = implies(implies(implies(implies(implies(X0,X1),X1),implies(X2,X0)),implies(X2,implies(X1,X0))),implies(X2,implies(X1,X0))),
inference(superposition,[],[f62,f4]) ).
fof(f91,plain,
! [X2,X3,X0,X1] : implies(truth,implies(X3,implies(implies(X1,X2),implies(X0,X2)))) = implies(implies(implies(truth,implies(X3,implies(implies(X1,X2),implies(X0,X2)))),implies(X3,implies(X0,X1))),implies(X3,implies(X0,X1))),
inference(superposition,[],[f62,f3]) ).
fof(f115,plain,
! [X0,X1] : implies(implies(X0,X1),implies(truth,X1)) = implies(implies(implies(implies(X0,X1),implies(truth,X1)),X0),X0),
inference(superposition,[],[f62,f1]) ).
fof(f117,plain,
! [X2,X0,X1] : implies(implies(X0,X2),implies(implies(X1,X0),X2)) = implies(implies(implies(implies(X0,X2),implies(implies(X1,X0),X2)),implies(implies(X0,X1),X1)),implies(implies(X0,X1),X1)),
inference(superposition,[],[f62,f4]) ).
fof(f131,plain,
! [X0,X1] : implies(implies(X0,X1),X1) = implies(implies(implies(implies(X0,X1),X1),X0),X0),
inference(forward_demodulation,[],[f115,f1]) ).
fof(f134,plain,
! [X2,X3,X0,X1] : implies(X3,implies(implies(X1,X2),implies(X0,X2))) = implies(implies(implies(X3,implies(implies(X1,X2),implies(X0,X2))),implies(X3,implies(X0,X1))),implies(X3,implies(X0,X1))),
inference(forward_demodulation,[],[f91,f1]) ).
fof(f184,plain,
! [X0] : truth = implies(implies(truth,X0),X0),
inference(superposition,[],[f1,f64]) ).
fof(f185,plain,
! [X2,X0,X1] : truth = implies(truth,implies(implies(implies(implies(X0,X1),X1),X2),implies(X0,X2))),
inference(superposition,[],[f3,f64]) ).
fof(f199,plain,
! [X2,X0,X1] : truth = implies(implies(implies(implies(X0,X1),X1),X2),implies(X0,X2)),
inference(forward_demodulation,[],[f185,f1]) ).
fof(f200,plain,
! [X0] : truth = implies(X0,X0),
inference(forward_demodulation,[],[f184,f1]) ).
fof(f245,plain,
! [X2,X0,X1] : truth = implies(implies(implies(implies(X0,X1),X1),X2),implies(X1,X2)),
inference(superposition,[],[f199,f4]) ).
fof(f273,plain,
! [X0,X1] : implies(implies(implies(X0,X1),X1),X1) = implies(truth,implies(X0,X1)),
inference(superposition,[],[f131,f199]) ).
fof(f287,plain,
! [X0,X1] : implies(X0,X1) = implies(implies(implies(X0,X1),X1),X1),
inference(forward_demodulation,[],[f273,f1]) ).
fof(f323,plain,
sF5 = implies(implies(sF5,sF4),sF4),
inference(superposition,[],[f287,f28]) ).
fof(f326,plain,
! [X0,X1] : implies(X1,X0) = implies(implies(implies(X0,X1),X1),X0),
inference(superposition,[],[f287,f4]) ).
fof(f342,plain,
sF5 = implies(sF6,sF4),
inference(forward_demodulation,[],[f323,f30]) ).
fof(f365,plain,
implies(z,y) = implies(sF1,y),
inference(superposition,[],[f287,f36]) ).
fof(f367,plain,
truth = implies(z,sF1),
inference(superposition,[],[f64,f36]) ).
fof(f423,plain,
! [X2,X0,X1] : truth = implies(implies(truth,X2),implies(implies(implies(implies(X0,X1),X1),X0),X2)),
inference(superposition,[],[f66,f64]) ).
fof(f426,plain,
! [X2,X0,X1] : truth = implies(truth,implies(implies(X2,implies(X0,X1)),implies(X0,implies(X2,X1)))),
inference(superposition,[],[f66,f199]) ).
fof(f455,plain,
! [X2,X0,X1] : truth = implies(implies(implies(implies(X0,X2),implies(X1,X2)),X0),implies(implies(X0,X1),X1)),
inference(superposition,[],[f66,f4]) ).
fof(f502,plain,
! [X2,X0,X1] : truth = implies(implies(X2,implies(X0,X1)),implies(X0,implies(X2,X1))),
inference(forward_demodulation,[],[f426,f1]) ).
fof(f505,plain,
! [X2,X0,X1] : truth = implies(implies(truth,X2),implies(implies(X1,X0),X2)),
inference(forward_demodulation,[],[f423,f326]) ).
fof(f527,plain,
! [X2,X0,X1] : truth = implies(X2,implies(implies(X1,X0),X2)),
inference(forward_demodulation,[],[f505,f1]) ).
fof(f615,plain,
! [X2,X0,X1] : implies(truth,implies(X1,implies(X0,X2))) = implies(implies(implies(truth,implies(X1,implies(X0,X2))),implies(X0,implies(X1,X2))),implies(X0,implies(X1,X2))),
inference(superposition,[],[f131,f502]) ).
fof(f626,plain,
! [X2,X0,X1] : implies(X1,implies(X0,X2)) = implies(implies(implies(X1,implies(X0,X2)),implies(X0,implies(X1,X2))),implies(X0,implies(X1,X2))),
inference(forward_demodulation,[],[f615,f1]) ).
fof(f658,plain,
! [X2,X0,X1] : implies(X1,implies(X0,X2)) = implies(truth,implies(X0,implies(X1,X2))),
inference(forward_demodulation,[],[f626,f502]) ).
fof(f663,plain,
! [X2,X0,X1] : implies(X0,implies(X1,X2)) = implies(X1,implies(X0,X2)),
inference(forward_demodulation,[],[f658,f1]) ).
fof(f704,plain,
! [X0,X1] : implies(X0,implies(X1,X0)) = implies(X1,truth),
inference(superposition,[],[f663,f200]) ).
fof(f707,plain,
! [X2,X0,X1] : implies(X2,implies(implies(X0,X1),X1)) = implies(implies(X1,X0),implies(X2,X0)),
inference(superposition,[],[f663,f4]) ).
fof(f714,plain,
! [X2,X0,X1] : implies(implies(implies(X0,X1),X1),implies(X2,X1)) = implies(X2,implies(X0,X1)),
inference(superposition,[],[f663,f287]) ).
fof(f716,plain,
! [X0] : implies(X0,sF4) = implies(x,implies(X0,z)),
inference(superposition,[],[f663,f26]) ).
fof(f717,plain,
! [X0] : implies(X0,sF3) = implies(x,implies(X0,y)),
inference(superposition,[],[f663,f24]) ).
fof(f719,plain,
! [X0] : implies(X0,sF0) = implies(y,implies(X0,z)),
inference(superposition,[],[f663,f18]) ).
fof(f797,plain,
! [X2,X0,X1] : implies(implies(X0,implies(X1,X2)),implies(X0,X2)) = implies(implies(implies(X0,X2),X1),X1),
inference(superposition,[],[f4,f663]) ).
fof(f836,plain,
implies(x,sF1) = implies(sF0,sF4),
inference(superposition,[],[f716,f20]) ).
fof(f873,plain,
sF2 = implies(sF0,sF4),
inference(forward_demodulation,[],[f836,f22]) ).
fof(f927,plain,
implies(x,sF1) = implies(implies(z,y),sF3),
inference(superposition,[],[f717,f36]) ).
fof(f963,plain,
implies(x,sF1) = implies(implies(sF1,y),sF3),
inference(forward_demodulation,[],[f927,f365]) ).
fof(f967,plain,
sF2 = implies(implies(sF1,y),sF3),
inference(forward_demodulation,[],[f963,f22]) ).
fof(f1023,plain,
! [X0,X1] : implies(X0,implies(implies(X0,X1),X1)) = implies(implies(X1,X0),truth),
inference(superposition,[],[f704,f4]) ).
fof(f1040,plain,
implies(z,sF1) = implies(sF0,truth),
inference(superposition,[],[f704,f20]) ).
fof(f1041,plain,
implies(sF0,truth) = implies(sF4,sF2),
inference(superposition,[],[f704,f873]) ).
fof(f1089,plain,
implies(z,sF1) = implies(sF4,sF2),
inference(forward_demodulation,[],[f1040,f1041]) ).
fof(f1098,plain,
! [X0,X1] : truth = implies(implies(X1,X0),truth),
inference(forward_demodulation,[],[f1023,f64]) ).
fof(f1101,plain,
truth = implies(sF4,sF2),
inference(forward_demodulation,[],[f1089,f367]) ).
fof(f1122,plain,
! [X0] : implies(X0,sF2) = implies(implies(sF1,y),implies(X0,sF3)),
inference(superposition,[],[f663,f967]) ).
fof(f1345,plain,
! [X0] : truth = implies(X0,truth),
inference(superposition,[],[f287,f1098]) ).
fof(f1363,plain,
! [X2,X0,X1] : implies(X2,truth) = implies(implies(X0,X1),implies(X2,truth)),
inference(superposition,[],[f663,f1098]) ).
fof(f1501,plain,
! [X0] : truth = implies(implies(not(X0),not(truth)),X0),
inference(superposition,[],[f6,f1]) ).
fof(f1542,plain,
! [X2,X0,X1] : truth = implies(implies(X0,implies(not(X1),not(X2))),implies(truth,implies(X0,implies(X2,X1)))),
inference(superposition,[],[f3,f6]) ).
fof(f1545,plain,
! [X2,X0,X1] : implies(truth,implies(X2,implies(X1,X0))) = implies(implies(implies(truth,implies(X2,implies(X1,X0))),implies(X2,implies(not(X0),not(X1)))),implies(X2,implies(not(X0),not(X1)))),
inference(superposition,[],[f62,f6]) ).
fof(f1551,plain,
! [X0,X1] : implies(truth,implies(X1,X0)) = implies(implies(implies(truth,implies(X1,X0)),implies(not(X0),not(X1))),implies(not(X0),not(X1))),
inference(superposition,[],[f131,f6]) ).
fof(f1569,plain,
! [X0,X1] : implies(X1,X0) = implies(implies(implies(X1,X0),implies(not(X0),not(X1))),implies(not(X0),not(X1))),
inference(forward_demodulation,[],[f1551,f1]) ).
fof(f1575,plain,
! [X2,X0,X1] : implies(X2,implies(X1,X0)) = implies(implies(implies(X2,implies(X1,X0)),implies(X2,implies(not(X0),not(X1)))),implies(X2,implies(not(X0),not(X1)))),
inference(forward_demodulation,[],[f1545,f1]) ).
fof(f1578,plain,
! [X2,X0,X1] : truth = implies(implies(X0,implies(not(X1),not(X2))),implies(X0,implies(X2,X1))),
inference(forward_demodulation,[],[f1542,f1]) ).
fof(f1722,plain,
! [X0] : implies(X0,sF6) = implies(implies(sF4,sF3),implies(X0,sF3)),
inference(superposition,[],[f663,f78]) ).
fof(f1957,plain,
! [X2,X3,X0,X1] : truth = implies(implies(implies(truth,implies(implies(X1,X2),X0)),X3),implies(X0,X3)),
inference(superposition,[],[f199,f527]) ).
fof(f1979,plain,
! [X2,X3,X0,X1] : truth = implies(implies(implies(implies(X1,X2),X0),X3),implies(X0,X3)),
inference(forward_demodulation,[],[f1957,f1]) ).
fof(f2600,plain,
! [X0] : implies(implies(sF4,sF3),implies(X0,sF3)) = implies(implies(implies(X0,sF3),sF3),sF6),
inference(superposition,[],[f714,f78]) ).
fof(f2703,plain,
! [X0] : implies(X0,sF6) = implies(implies(implies(X0,sF3),sF3),sF6),
inference(forward_demodulation,[],[f2600,f1722]) ).
fof(f2948,plain,
! [X2,X0,X1] : implies(implies(X0,X1),implies(X2,X1)) = implies(implies(X1,X0),implies(X2,X0)),
inference(superposition,[],[f663,f707]) ).
fof(f5160,plain,
implies(sF4,sF5) = implies(implies(sF6,sF4),sF5),
inference(superposition,[],[f326,f30]) ).
fof(f5302,plain,
implies(sF4,sF5) = implies(sF5,sF5),
inference(forward_demodulation,[],[f5160,f342]) ).
fof(f5350,plain,
truth = implies(sF4,sF5),
inference(forward_demodulation,[],[f5302,f200]) ).
fof(f7601,plain,
! [X2,X0,X1] : implies(X1,implies(implies(X1,X2),implies(X0,X2))) = implies(implies(implies(X1,implies(implies(X1,X2),implies(X0,X2))),implies(X0,truth)),implies(X0,truth)),
inference(superposition,[],[f134,f704]) ).
fof(f7733,plain,
! [X2,X0,X1] : implies(X0,truth) = implies(X1,implies(implies(X1,X2),implies(X0,X2))),
inference(forward_demodulation,[],[f7601,f1363]) ).
fof(f7875,plain,
! [X2,X0,X1] : truth = implies(X1,implies(implies(X1,X2),implies(X0,X2))),
inference(forward_demodulation,[],[f7733,f1345]) ).
fof(f8429,plain,
! [X0,X1] : implies(not(X1),implies(X1,X0)) = implies(implies(implies(not(X1),implies(X1,X0)),implies(not(X0),truth)),implies(not(X0),truth)),
inference(superposition,[],[f1575,f704]) ).
fof(f8552,plain,
! [X0,X1] : implies(not(X0),truth) = implies(not(X1),implies(X1,X0)),
inference(forward_demodulation,[],[f8429,f1363]) ).
fof(f8595,plain,
! [X0,X1] : truth = implies(not(X1),implies(X1,X0)),
inference(forward_demodulation,[],[f8552,f1345]) ).
fof(f8615,plain,
! [X0] : truth = implies(not(truth),X0),
inference(superposition,[],[f8595,f1]) ).
fof(f8697,plain,
! [X0,X1] : truth = implies(X0,implies(not(X0),X1)),
inference(superposition,[],[f663,f8595]) ).
fof(f8725,plain,
! [X0,X1] : implies(truth,implies(X0,X1)) = implies(implies(implies(truth,implies(X0,X1)),not(X0)),not(X0)),
inference(superposition,[],[f131,f8595]) ).
fof(f8742,plain,
! [X2,X0,X1] : implies(implies(implies(X1,X2),not(X1)),implies(X0,not(X1))) = implies(X0,implies(truth,implies(X1,X2))),
inference(superposition,[],[f707,f8595]) ).
fof(f8758,plain,
! [X2,X0,X1] : implies(X0,implies(X1,X2)) = implies(implies(implies(X1,X2),not(X1)),implies(X0,not(X1))),
inference(forward_demodulation,[],[f8742,f1]) ).
fof(f8772,plain,
! [X0,X1] : implies(X0,X1) = implies(implies(implies(X0,X1),not(X0)),not(X0)),
inference(forward_demodulation,[],[f8725,f1]) ).
fof(f11919,plain,
implies(not(truth),not(not(truth))) = implies(truth,not(not(truth))),
inference(superposition,[],[f326,f1501]) ).
fof(f12067,plain,
not(not(truth)) = implies(not(truth),not(not(truth))),
inference(forward_demodulation,[],[f11919,f1]) ).
fof(f12099,plain,
truth = not(not(truth)),
inference(forward_demodulation,[],[f12067,f8615]) ).
fof(f12805,plain,
! [X0] : implies(implies(implies(sF3,X0),X0),sF2) = implies(implies(implies(implies(implies(sF3,X0),X0),sF2),implies(implies(sF1,y),implies(X0,sF3))),implies(implies(sF1,y),implies(X0,sF3))),
inference(superposition,[],[f90,f967]) ).
fof(f13378,plain,
! [X0] : implies(implies(implies(sF3,X0),X0),sF2) = implies(implies(implies(implies(implies(sF3,X0),X0),sF2),implies(X0,sF2)),implies(X0,sF2)),
inference(forward_demodulation,[],[f12805,f1122]) ).
fof(f13691,plain,
! [X0] : implies(truth,implies(X0,sF2)) = implies(implies(implies(sF3,X0),X0),sF2),
inference(forward_demodulation,[],[f13378,f245]) ).
fof(f13882,plain,
! [X0] : implies(X0,sF2) = implies(implies(implies(sF3,X0),X0),sF2),
inference(forward_demodulation,[],[f13691,f1]) ).
fof(f14399,plain,
implies(sF4,sF2) = implies(implies(sF5,sF4),sF2),
inference(superposition,[],[f13882,f28]) ).
fof(f14529,plain,
implies(sF4,sF2) = implies(sF6,sF2),
inference(forward_demodulation,[],[f14399,f30]) ).
fof(f14544,plain,
truth = implies(sF6,sF2),
inference(forward_demodulation,[],[f14529,f1101]) ).
fof(f14599,plain,
implies(truth,sF2) = implies(implies(implies(truth,sF2),sF6),sF6),
inference(superposition,[],[f131,f14544]) ).
fof(f14659,plain,
sF2 = implies(implies(sF2,sF6),sF6),
inference(forward_demodulation,[],[f14599,f1]) ).
fof(f22761,plain,
! [X2,X0,X1] : implies(implies(implies(not(X0),X2),X2),implies(X0,X1)) = implies(implies(implies(implies(implies(not(X0),X2),X2),implies(X0,X1)),implies(implies(implies(X0,X1),not(X0)),implies(X2,not(X0)))),implies(implies(implies(X0,X1),not(X0)),implies(X2,not(X0)))),
inference(superposition,[],[f90,f8772]) ).
fof(f22826,plain,
! [X2,X0,X1] : implies(implies(implies(not(X0),X2),X2),implies(X0,X1)) = implies(implies(implies(implies(implies(not(X0),X2),X2),implies(X0,X1)),implies(X2,implies(X0,X1))),implies(X2,implies(X0,X1))),
inference(forward_demodulation,[],[f22761,f8758]) ).
fof(f22913,plain,
! [X2,X0,X1] : implies(truth,implies(X2,implies(X0,X1))) = implies(implies(implies(not(X0),X2),X2),implies(X0,X1)),
inference(forward_demodulation,[],[f22826,f245]) ).
fof(f22926,plain,
! [X2,X0,X1] : implies(X2,implies(X0,X1)) = implies(implies(implies(not(X0),X2),X2),implies(X0,X1)),
inference(forward_demodulation,[],[f22913,f1]) ).
fof(f28349,plain,
! [X0] : implies(implies(X0,sF4),sF6) = implies(implies(sF4,X0),implies(sF5,X0)),
inference(superposition,[],[f2948,f30]) ).
fof(f34723,plain,
! [X2,X0,X1] : implies(implies(implies(implies(implies(implies(X0,X1),implies(X2,X1)),X0),X2),implies(X0,X2)),implies(X0,X2)) = implies(truth,implies(implies(implies(implies(X0,X1),implies(X2,X1)),X0),X2)),
inference(superposition,[],[f797,f455]) ).
fof(f34903,plain,
! [X2,X0,X1] : implies(implies(implies(implies(X0,X1),implies(X2,X1)),X0),X2) = implies(implies(implies(implies(implies(implies(X0,X1),implies(X2,X1)),X0),X2),implies(X0,X2)),implies(X0,X2)),
inference(forward_demodulation,[],[f34723,f1]) ).
fof(f35313,plain,
! [X2,X0,X1] : implies(truth,implies(X0,X2)) = implies(implies(implies(implies(X0,X1),implies(X2,X1)),X0),X2),
inference(forward_demodulation,[],[f34903,f1979]) ).
fof(f35515,plain,
! [X2,X0,X1] : implies(X0,X2) = implies(implies(implies(implies(X0,X1),implies(X2,X1)),X0),X2),
inference(forward_demodulation,[],[f35313,f1]) ).
fof(f37256,plain,
! [X0] : implies(implies(X0,implies(not(X0),not(truth))),implies(not(X0),not(truth))) = X0,
inference(superposition,[],[f1569,f1]) ).
fof(f37680,plain,
! [X0] : implies(truth,implies(not(X0),not(truth))) = X0,
inference(forward_demodulation,[],[f37256,f8697]) ).
fof(f37725,plain,
! [X0] : implies(not(X0),not(truth)) = X0,
inference(forward_demodulation,[],[f37680,f1]) ).
fof(f37754,plain,
! [X0] : implies(X0,not(truth)) = implies(implies(not(truth),not(X0)),not(X0)),
inference(superposition,[],[f4,f37725]) ).
fof(f37779,plain,
! [X0,X1] : implies(implies(not(X0),X1),implies(implies(not(truth),not(X0)),X1)) = implies(implies(implies(implies(not(X0),X1),implies(implies(not(truth),not(X0)),X1)),implies(X0,not(truth))),implies(X0,not(truth))),
inference(superposition,[],[f117,f37725]) ).
fof(f37812,plain,
! [X0,X1] : implies(X1,implies(X0,not(truth))) = implies(implies(not(truth),not(X0)),implies(X1,not(X0))),
inference(superposition,[],[f707,f37725]) ).
fof(f37823,plain,
! [X0,X1] : truth = implies(implies(X1,implies(not(not(truth)),not(not(X0)))),implies(X1,X0)),
inference(superposition,[],[f1578,f37725]) ).
fof(f37825,plain,
! [X0,X1] : implies(X0,implies(X1,not(truth))) = implies(implies(not(truth),not(X0)),implies(X1,not(X0))),
inference(superposition,[],[f2948,f37725]) ).
fof(f37848,plain,
! [X0,X1] : implies(X0,implies(X1,not(truth))) = implies(truth,implies(X1,not(X0))),
inference(forward_demodulation,[],[f37825,f8615]) ).
fof(f37850,plain,
! [X0,X1] : truth = implies(implies(X1,implies(truth,not(not(X0)))),implies(X1,X0)),
inference(forward_demodulation,[],[f37823,f12099]) ).
fof(f37857,plain,
! [X0,X1] : implies(X1,implies(X0,not(truth))) = implies(truth,implies(X1,not(X0))),
inference(forward_demodulation,[],[f37812,f8615]) ).
fof(f37868,plain,
! [X0,X1] : implies(implies(not(X0),X1),implies(truth,X1)) = implies(implies(implies(implies(not(X0),X1),implies(truth,X1)),implies(X0,not(truth))),implies(X0,not(truth))),
inference(forward_demodulation,[],[f37779,f8615]) ).
fof(f37882,plain,
! [X0] : implies(X0,not(truth)) = implies(truth,not(X0)),
inference(forward_demodulation,[],[f37754,f8615]) ).
fof(f37891,plain,
! [X0,X1] : implies(X1,not(X0)) = implies(X0,implies(X1,not(truth))),
inference(forward_demodulation,[],[f37848,f1]) ).
fof(f37893,plain,
! [X0,X1] : truth = implies(implies(X1,not(not(X0))),implies(X1,X0)),
inference(forward_demodulation,[],[f37850,f1]) ).
fof(f37898,plain,
! [X0,X1] : implies(X1,not(X0)) = implies(X1,implies(X0,not(truth))),
inference(forward_demodulation,[],[f37857,f1]) ).
fof(f37901,plain,
! [X0,X1] : implies(implies(not(X0),X1),X1) = implies(implies(implies(implies(not(X0),X1),X1),implies(X0,not(truth))),implies(X0,not(truth))),
inference(forward_demodulation,[],[f37868,f1]) ).
fof(f37912,plain,
! [X0] : not(X0) = implies(X0,not(truth)),
inference(forward_demodulation,[],[f37882,f1]) ).
fof(f37914,plain,
! [X0,X1] : implies(X0,not(X1)) = implies(X1,not(X0)),
inference(forward_demodulation,[],[f37898,f37891]) ).
fof(f37915,plain,
! [X0,X1] : implies(implies(not(X0),X1),X1) = implies(X0,not(implies(implies(implies(not(X0),X1),X1),implies(X0,not(truth))))),
inference(forward_demodulation,[],[f37901,f37891]) ).
fof(f37923,plain,
! [X0,X1] : implies(implies(not(X0),X1),X1) = implies(X0,not(implies(X1,implies(X0,not(truth))))),
inference(forward_demodulation,[],[f37915,f22926]) ).
fof(f37927,plain,
! [X0,X1] : implies(implies(not(X0),X1),X1) = implies(X0,not(implies(X0,not(X1)))),
inference(forward_demodulation,[],[f37923,f37891]) ).
fof(f38141,plain,
! [X0] : implies(truth,not(not(X0))) = X0,
inference(superposition,[],[f37725,f37914]) ).
fof(f38328,plain,
! [X0] : not(not(X0)) = X0,
inference(forward_demodulation,[],[f38141,f1]) ).
fof(f38379,plain,
! [X0,X1] : implies(X1,X0) = implies(not(X0),not(X1)),
inference(superposition,[],[f37914,f38328]) ).
fof(f39371,plain,
! [X0,X1] : implies(X1,not(implies(X1,not(not(X0))))) = implies(implies(X0,not(not(X1))),not(X0)),
inference(superposition,[],[f37927,f37914]) ).
fof(f39373,plain,
! [X0,X1] : implies(X0,not(implies(X0,not(not(implies(not(X0),not(X1))))))) = implies(implies(implies(not(not(X0)),X1),X1),not(implies(not(X0),not(X1)))),
inference(superposition,[],[f37927,f37927]) ).
fof(f39788,plain,
! [X0,X1] : implies(X0,not(implies(X0,not(not(implies(X1,X0)))))) = implies(implies(implies(not(not(X0)),X1),X1),not(implies(X1,X0))),
inference(forward_demodulation,[],[f39373,f38379]) ).
fof(f39790,plain,
! [X0,X1] : implies(implies(X0,X1),not(X0)) = implies(X1,not(implies(X1,not(not(X0))))),
inference(forward_demodulation,[],[f39371,f38328]) ).
fof(f39877,plain,
! [X0,X1] : implies(implies(implies(X0,X1),X1),not(implies(X1,X0))) = implies(X0,not(implies(X0,not(not(implies(X1,X0)))))),
inference(forward_demodulation,[],[f39788,f38328]) ).
fof(f39879,plain,
! [X0,X1] : implies(implies(X0,X1),not(X0)) = implies(X1,not(implies(X1,X0))),
inference(forward_demodulation,[],[f39790,f38328]) ).
fof(f39918,plain,
! [X0,X1] : implies(implies(implies(X0,X1),X1),not(implies(X1,X0))) = implies(X0,not(implies(X0,implies(X1,X0)))),
inference(forward_demodulation,[],[f39877,f38328]) ).
fof(f39940,plain,
! [X0,X1] : implies(implies(implies(X0,X1),X1),not(implies(X1,X0))) = implies(X0,not(implies(X1,truth))),
inference(forward_demodulation,[],[f39918,f704]) ).
fof(f39947,plain,
! [X0,X1] : implies(X0,not(truth)) = implies(implies(implies(X0,X1),X1),not(implies(X1,X0))),
inference(forward_demodulation,[],[f39940,f1345]) ).
fof(f39949,plain,
! [X0,X1] : not(X0) = implies(implies(implies(X0,X1),X1),not(implies(X1,X0))),
inference(forward_demodulation,[],[f39947,f37912]) ).
fof(f40041,plain,
! [X2,X0,X1] : implies(X2,implies(X0,X1)) = implies(not(X1),implies(X2,not(X0))),
inference(superposition,[],[f663,f38379]) ).
fof(f57960,plain,
! [X2,X0,X1] : implies(implies(X1,X0),implies(X1,X2)) = implies(not(X2),implies(X0,not(implies(X0,X1)))),
inference(superposition,[],[f40041,f39879]) ).
fof(f57964,plain,
! [X2,X0,X1] : implies(not(X2),not(X0)) = implies(implies(implies(X0,X1),X1),implies(implies(X1,X0),X2)),
inference(superposition,[],[f40041,f39949]) ).
fof(f58248,plain,
! [X2,X0,X1] : implies(X0,X2) = implies(implies(implies(X0,X1),X1),implies(implies(X1,X0),X2)),
inference(forward_demodulation,[],[f57964,f38379]) ).
fof(f58249,plain,
! [X2,X0,X1] : implies(implies(X1,X0),implies(X1,X2)) = implies(X0,implies(implies(X0,X1),X2)),
inference(forward_demodulation,[],[f57960,f40041]) ).
fof(f58473,plain,
! [X0] : implies(sF4,implies(implies(sF4,sF5),X0)) = implies(sF6,implies(sF5,X0)),
inference(superposition,[],[f58249,f30]) ).
fof(f58639,plain,
! [X0] : implies(implies(x,X0),sF4) = implies(X0,implies(implies(X0,x),z)),
inference(superposition,[],[f58249,f26]) ).
fof(f58879,plain,
! [X2,X0,X1] : implies(implies(X0,implies(implies(X0,X2),implies(X1,X2))),implies(X0,X1)) = implies(implies(implies(X0,X2),implies(X1,X2)),implies(X0,X1)),
inference(superposition,[],[f58249,f35515]) ).
fof(f59419,plain,
! [X2,X0,X1] : implies(truth,implies(X0,X1)) = implies(implies(implies(X0,X2),implies(X1,X2)),implies(X0,X1)),
inference(forward_demodulation,[],[f58879,f7875]) ).
fof(f59660,plain,
! [X0] : implies(sF6,implies(sF5,X0)) = implies(sF4,implies(truth,X0)),
inference(forward_demodulation,[],[f58473,f5350]) ).
fof(f59842,plain,
! [X2,X0,X1] : implies(X0,X1) = implies(implies(implies(X0,X2),implies(X1,X2)),implies(X0,X1)),
inference(forward_demodulation,[],[f59419,f1]) ).
fof(f59968,plain,
! [X0] : implies(sF4,X0) = implies(sF6,implies(sF5,X0)),
inference(forward_demodulation,[],[f59660,f1]) ).
fof(f64316,plain,
implies(implies(y,x),sF0) = implies(implies(x,y),sF4),
inference(superposition,[],[f719,f58639]) ).
fof(f64495,plain,
implies(sF3,sF4) = implies(implies(y,x),sF0),
inference(forward_demodulation,[],[f64316,f24]) ).
fof(f64570,plain,
sF5 = implies(implies(y,x),sF0),
inference(forward_demodulation,[],[f64495,f28]) ).
fof(f70265,plain,
! [X0] : implies(implies(sF4,X0),implies(sF5,X0)) = implies(implies(implies(sF5,X0),sF6),sF6),
inference(superposition,[],[f4,f59968]) ).
fof(f70399,plain,
! [X0] : implies(implies(X0,sF4),sF6) = implies(implies(implies(sF5,X0),sF6),sF6),
inference(forward_demodulation,[],[f70265,f28349]) ).
fof(f73625,plain,
! [X2,X0,X1] : implies(implies(implies(X1,X0),X0),X2) = implies(implies(implies(X0,X1),X1),implies(implies(X1,implies(implies(X1,X0),X0)),X2)),
inference(superposition,[],[f58248,f326]) ).
fof(f75083,plain,
! [X2,X0,X1] : implies(implies(implies(X1,X0),X0),X2) = implies(implies(implies(X0,X1),X1),implies(truth,X2)),
inference(forward_demodulation,[],[f73625,f64]) ).
fof(f75466,plain,
! [X2,X0,X1] : implies(implies(implies(X0,X1),X1),X2) = implies(implies(implies(X1,X0),X0),X2),
inference(forward_demodulation,[],[f75083,f1]) ).
fof(f81410,plain,
! [X2,X0,X1] : implies(X1,X2) = implies(implies(implies(X0,truth),implies(X2,implies(X0,X1))),implies(X1,X2)),
inference(superposition,[],[f59842,f704]) ).
fof(f82870,plain,
! [X2,X0,X1] : implies(X1,X2) = implies(implies(truth,implies(X2,implies(X0,X1))),implies(X1,X2)),
inference(forward_demodulation,[],[f81410,f1345]) ).
fof(f83013,plain,
! [X2,X0,X1] : implies(X1,X2) = implies(implies(X2,implies(X0,X1)),implies(X1,X2)),
inference(forward_demodulation,[],[f82870,f1]) ).
fof(f83370,plain,
! [X2,X0,X1] : implies(X2,X1) = implies(implies(X0,implies(X1,X2)),implies(X2,X1)),
inference(superposition,[],[f83013,f663]) ).
fof(f85272,plain,
! [X2,X0,X1] : implies(X0,X1) = implies(X0,implies(implies(X2,implies(X1,X0)),X1)),
inference(superposition,[],[f663,f83370]) ).
fof(f152011,plain,
! [X2,X0,X1] : implies(X1,X0) = implies(X1,implies(implies(implies(implies(X0,X1),X2),X2),X0)),
inference(superposition,[],[f85272,f75466]) ).
fof(f153495,plain,
implies(x,y) = implies(x,implies(implies(sF5,sF0),y)),
inference(superposition,[],[f152011,f64570]) ).
fof(f154219,plain,
implies(x,y) = implies(implies(sF5,sF0),sF3),
inference(forward_demodulation,[],[f153495,f717]) ).
fof(f154627,plain,
sF3 = implies(implies(sF5,sF0),sF3),
inference(forward_demodulation,[],[f154219,f24]) ).
fof(f155077,plain,
implies(implies(sF3,sF3),sF6) = implies(implies(sF5,sF0),sF6),
inference(superposition,[],[f2703,f154627]) ).
fof(f155335,plain,
implies(truth,sF6) = implies(implies(sF5,sF0),sF6),
inference(forward_demodulation,[],[f155077,f200]) ).
fof(f155377,plain,
sF6 = implies(implies(sF5,sF0),sF6),
inference(forward_demodulation,[],[f155335,f1]) ).
fof(f155486,plain,
truth = implies(implies(implies(sF5,sF0),not(not(sF6))),sF6),
inference(superposition,[],[f37893,f155377]) ).
fof(f155625,plain,
truth = implies(implies(implies(sF5,sF0),sF6),sF6),
inference(forward_demodulation,[],[f155486,f38328]) ).
fof(f155708,plain,
truth = implies(implies(sF0,sF4),sF6),
inference(forward_demodulation,[],[f155625,f70399]) ).
fof(f155746,plain,
truth = implies(sF2,sF6),
inference(forward_demodulation,[],[f155708,f873]) ).
fof(f155780,plain,
sF2 = implies(truth,sF6),
inference(superposition,[],[f14659,f155746]) ).
fof(f156052,plain,
sF2 = sF6,
inference(forward_demodulation,[],[f155780,f1]) ).
fof(f156102,plain,
$false,
inference(forward_subsumption_resolution,[],[f156052,f31]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LCL149-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.18/0.45 % Computer : n010.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Sun Sep 27 15:23:32 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.50 Running first-order theorem proving
% 0.22/0.50 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
% 16.99/3.57 % (1088388)Input is clausal, will run a generic CNF schedule.
% 16.99/3.57 % (1088403)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2561103751:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 16.99/3.57 % (1088399)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=2859020717:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 16.99/3.57 % (1088405)dis-21_1_sil=8000:lcm=predicate:random_seed=1054711470:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 16.99/3.57 % (1088405)Refutation not found, incomplete strategy
% 16.99/3.57 % (1088405)------------------------------
% 16.99/3.57 % (1088405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.99/3.57 % (1088405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.99/3.57 % (1088405)CaDiCaL version: 2.1.3
% 16.99/3.57 % (1088405)Termination reason: Refutation not found, incomplete strategy
% 16.99/3.57 % (1088405)Time elapsed: 0.002 s
% 16.99/3.57 % (1088405)Peak memory usage: 88 MB
% 16.99/3.57 % (1088400)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=199648555:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 16.99/3.57 % (1088401)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=412432117:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 16.99/3.57 % (1088402)lrs+10_1_sil=8000:sp=occurrence:random_seed=2342678776:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 16.99/3.57 % (1088404)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3830323797:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 16.99/3.57 % (1088403)Instruction limit reached!
% 16.99/3.57 % (1088403)------------------------------
% 16.99/3.57 % (1088403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.99/3.57 % (1088403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.99/3.57 % (1088403)CaDiCaL version: 2.1.3
% 16.99/3.57 % (1088403)Termination reason: Instruction limit
% 16.99/3.57 % (1088403)Termination phase: Saturation
% 16.99/3.57 % (1088403)Time elapsed: 0.088 s
% 16.99/3.57 % (1088403)Peak memory usage: 88 MB
% 16.99/3.57 % (1088403)Instructions burned: 114 (million)
% 16.99/3.57 % (1088402)Instruction limit reached!
% 16.99/3.57 % (1088402)------------------------------
% 16.99/3.57 % (1088402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.99/3.57 % (1088402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.99/3.57 % (1088402)CaDiCaL version: 2.1.3
% 16.99/3.57 % (1088402)Termination reason: Instruction limit
% 16.99/3.57 % (1088402)Termination phase: Saturation
% 16.99/3.57 % (1088402)Time elapsed: 0.103 s
% 16.99/3.57 % (1088402)Peak memory usage: 89 MB
% 16.99/3.57 % (1088402)Instructions burned: 108 (million)
% 16.99/3.57 % (1088404)Instruction limit reached!
% 16.99/3.57 % (1088404)------------------------------
% 16.99/3.57 % (1088404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.99/3.57 % (1088404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.99/3.57 % (1088404)CaDiCaL version: 2.1.3
% 16.99/3.57 % (1088404)Termination reason: Instruction limit
% 16.99/3.57 % (1088404)Termination phase: Saturation
% 16.99/3.57 % (1088404)Time elapsed: 0.168 s
% 16.99/3.57 % (1088404)Peak memory usage: 89 MB
% 16.99/3.57 % (1088404)Instructions burned: 181 (million)
% 16.99/3.57 % (1088416)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=95191116:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 16.99/3.57 % (1088416)Refutation not found, incomplete strategy
% 16.99/3.57 % (1088416)------------------------------
% 16.99/3.57 % (1088416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.99/3.57 % (1088416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.99/3.57 % (1088416)CaDiCaL version: 2.1.3
% 16.99/3.57 % (1088416)Termination reason: Refutation not found, incomplete strategy
% 16.99/3.57 % (1088416)Time elapsed: 0.002 s
% 16.99/3.57 % (1088416)Peak memory usage: 88 MB
% 16.99/3.57 % (1088416)Instructions burned: 1 (million)
% 16.99/3.57 % (1088418)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1221001353:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 37.84/6.43 % (1088418)Refutation not found, incomplete strategy
% 37.84/6.43 % (1088418)------------------------------
% 37.84/6.43 % (1088418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.84/6.43 % (1088418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.84/6.43 % (1088418)CaDiCaL version: 2.1.3
% 37.84/6.43 % (1088418)Termination reason: Refutation not found, incomplete strategy
% 37.84/6.43 % (1088418)Time elapsed: 0.002 s
% 37.84/6.43 % (1088418)Peak memory usage: 88 MB
% 37.84/6.43 % (1088418)Instructions burned: 1 (million)
% 37.84/6.43 % (1088405)------------------------------
% 37.84/6.43 % (1088405)------------------------------
% 37.84/6.43 % (1088420)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3948020430:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 37.84/6.43 % (1088416)------------------------------
% 37.84/6.43 % (1088416)------------------------------
% 37.84/6.43 % (1088422)lrs+10_64_to=lpo:sil=8000:random_seed=524539202:i=126:bd=preordered_2994 on theBenchmark for (2994ds/126Mi)
% 37.84/6.43 % (1088420)Instruction limit reached!
% 37.84/6.43 % (1088420)------------------------------
% 37.84/6.43 % (1088420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.84/6.43 % (1088420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.84/6.43 % (1088420)CaDiCaL version: 2.1.3
% 37.84/6.43 % (1088420)Termination reason: Instruction limit
% 37.84/6.43 % (1088420)Termination phase: Saturation
% 37.84/6.43 % (1088420)Time elapsed: 0.235 s
% 37.84/6.43 % (1088420)Peak memory usage: 90 MB
% 37.84/6.43 % (1088420)Instructions burned: 219 (million)
% 37.84/6.43 % (1088418)------------------------------
% 37.84/6.43 % (1088418)------------------------------
% 37.84/6.43 % (1088422)Instruction limit reached!
% 37.84/6.43 % (1088422)------------------------------
% 37.84/6.43 % (1088422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.84/6.43 % (1088422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.84/6.43 % (1088422)CaDiCaL version: 2.1.3
% 37.84/6.43 % (1088422)Termination reason: Instruction limit
% 37.84/6.43 % (1088422)Termination phase: Saturation
% 37.84/6.43 % (1088422)Time elapsed: 0.128 s
% 37.84/6.43 % (1088422)Peak memory usage: 89 MB
% 37.84/6.43 % (1088422)Instructions burned: 126 (million)
% 37.84/6.43 % (1088424)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=727990508:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 37.84/6.43 % (1088424)Instruction limit reached!
% 37.84/6.43 % (1088424)------------------------------
% 37.84/6.43 % (1088424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.84/6.43 % (1088424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.84/6.43 % (1088424)CaDiCaL version: 2.1.3
% 37.84/6.43 % (1088424)Termination reason: Instruction limit
% 37.84/6.43 % (1088424)Termination phase: Saturation
% 37.84/6.43 % (1088424)Time elapsed: 0.108 s
% 37.84/6.43 % (1088424)Peak memory usage: 90 MB
% 37.84/6.43 % (1088424)Instructions burned: 194 (million)
% 37.84/6.43 % (1088426)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2160419996:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 37.84/6.43 % (1088428)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1608455057:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2990 on theBenchmark for (2990ds/106Mi)
% 37.84/6.43 % (1088427)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3462326000:i=3394:sd=4:ss=included:sgt=64_2990 on theBenchmark for (2990ds/3394Mi)
% 37.84/6.43 % (1088426)Instruction limit reached!
% 37.84/6.43 % (1088426)------------------------------
% 37.84/6.43 % (1088426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.84/6.43 % (1088426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.84/6.43 % (1088426)CaDiCaL version: 2.1.3
% 37.84/6.43 % (1088426)Termination reason: Instruction limit
% 37.84/6.43 % (1088426)Termination phase: Saturation
% 37.84/6.43 % (1088426)Time elapsed: 0.131 s
% 37.84/6.43 % (1088426)Peak memory usage: 91 MB
% 37.84/6.43 % (1088426)Instructions burned: 157 (million)
% 37.84/6.43 % (1088428)Instruction limit reached!
% 37.84/6.43 % (1088428)------------------------------
% 37.84/6.43 % (1088428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.33/8.91 % (1088428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.33/8.91 % (1088428)CaDiCaL version: 2.1.3
% 54.33/8.91 % (1088428)Termination reason: Instruction limit
% 54.33/8.91 % (1088428)Termination phase: Saturation
% 54.33/8.91 % (1088428)Time elapsed: 0.105 s
% 54.33/8.91 % (1088428)Peak memory usage: 88 MB
% 54.33/8.91 % (1088428)Instructions burned: 106 (million)
% 54.33/8.91 % (1088430)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1578263569:i=107_2989 on theBenchmark for (2989ds/107Mi)
% 54.33/8.91 % (1088430)Refutation not found, incomplete strategy
% 54.33/8.91 % (1088430)------------------------------
% 54.33/8.91 % (1088430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.33/8.91 % (1088430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.33/8.91 % (1088430)CaDiCaL version: 2.1.3
% 54.33/8.91 % (1088430)Termination reason: Refutation not found, incomplete strategy
% 54.33/8.91 % (1088430)Time elapsed: 0.002 s
% 54.33/8.91 % (1088430)Peak memory usage: 88 MB
% 54.33/8.91 % (1088434)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1801637640:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2987 on theBenchmark for (2987ds/242Mi)
% 54.33/8.91 % (1088435)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1092104933:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi)
% 54.33/8.91 % (1088434)Instruction limit reached!
% 54.33/8.91 % (1088434)------------------------------
% 54.33/8.91 % (1088434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.33/8.91 % (1088434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.33/8.91 % (1088434)CaDiCaL version: 2.1.3
% 54.33/8.91 % (1088434)Termination reason: Instruction limit
% 54.33/8.91 % (1088434)Termination phase: Saturation
% 54.33/8.91 % (1088434)Time elapsed: 0.235 s
% 54.33/8.91 % (1088434)Peak memory usage: 91 MB
% 54.33/8.91 % (1088434)Instructions burned: 243 (million)
% 54.33/8.91 % (1088430)------------------------------
% 54.33/8.91 % (1088430)------------------------------
% 54.33/8.91 % (1088441)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2510156544:i=134:sd=2:doe=on:ss=axioms:sgt=14_2983 on theBenchmark for (2983ds/134Mi)
% 54.33/8.91 % (1088442)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2473340043:i=499:bd=all_2983 on theBenchmark for (2983ds/499Mi)
% 54.33/8.91 % (1088441)Instruction limit reached!
% 54.33/8.91 % (1088441)------------------------------
% 54.33/8.91 % (1088441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.33/8.91 % (1088441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.33/8.91 % (1088441)CaDiCaL version: 2.1.3
% 54.33/8.91 % (1088441)Termination reason: Instruction limit
% 54.33/8.91 % (1088441)Termination phase: Saturation
% 54.33/8.91 % (1088441)Time elapsed: 0.132 s
% 54.33/8.91 % (1088441)Peak memory usage: 89 MB
% 54.33/8.91 % (1088441)Instructions burned: 134 (million)
% 54.33/8.91 % (1088445)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2551462896:i=191:fgj=on:bd=all_2980 on theBenchmark for (2980ds/191Mi)
% 54.33/8.91 % (1088445)Instruction limit reached!
% 54.33/8.91 % (1088445)------------------------------
% 54.33/8.91 % (1088445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.33/8.91 % (1088445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.33/8.91 % (1088445)CaDiCaL version: 2.1.3
% 54.33/8.91 % (1088445)Termination reason: Instruction limit
% 54.33/8.91 % (1088445)Termination phase: Saturation
% 54.33/8.91 % (1088445)Time elapsed: 0.205 s
% 54.33/8.91 % (1088445)Peak memory usage: 91 MB
% 54.33/8.91 % (1088445)Instructions burned: 191 (million)
% 54.33/8.91 % (1088442)Instruction limit reached!
% 54.33/8.91 % (1088442)------------------------------
% 54.33/8.91 % (1088442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.33/8.91 % (1088442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.33/8.91 % (1088442)CaDiCaL version: 2.1.3
% 54.33/8.91 % (1088442)Termination reason: Instruction limit
% 54.33/8.91 % (1088442)Termination phase: Saturation
% 54.33/8.91 % (1088442)Time elapsed: 0.518 s
% 54.33/8.91 % (1088442)Peak memory usage: 94 MB
% 54.33/8.91 % (1088442)Instructions burned: 499 (million)
% 103.30/15.70 % (1088447)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=679110516:i=264:kws=precedence:fsr=off_2975 on theBenchmark for (2975ds/264Mi)
% 103.30/15.70 % (1088448)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1984507688:cond=on:i=156:bs=on:gtg=exists_all:er=known_2975 on theBenchmark for (2975ds/156Mi)
% 103.30/15.70 % (1088448)Instruction limit reached!
% 103.30/15.70 % (1088448)------------------------------
% 103.30/15.70 % (1088448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.30/15.70 % (1088448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.30/15.70 % (1088448)CaDiCaL version: 2.1.3
% 103.30/15.70 % (1088448)Termination reason: Instruction limit
% 103.30/15.70 % (1088448)Termination phase: Saturation
% 103.30/15.70 % (1088448)Time elapsed: 0.159 s
% 103.30/15.70 % (1088448)Peak memory usage: 89 MB
% 103.30/15.70 % (1088448)Instructions burned: 156 (million)
% 103.30/15.70 % (1088447)Instruction limit reached!
% 103.30/15.70 % (1088447)------------------------------
% 103.30/15.70 % (1088447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.30/15.70 % (1088447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.30/15.70 % (1088447)CaDiCaL version: 2.1.3
% 103.30/15.70 % (1088447)Termination reason: Instruction limit
% 103.30/15.70 % (1088447)Termination phase: Saturation
% 103.30/15.70 % (1088447)Time elapsed: 0.266 s
% 103.30/15.70 % (1088447)Peak memory usage: 93 MB
% 103.30/15.70 % (1088447)Instructions burned: 264 (million)
% 103.30/15.70 % (1088452)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2086353441:i=537:av=off:ss=included_2971 on theBenchmark for (2971ds/537Mi)
% 103.30/15.70 % (1088451)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1015640536:i=3256:kws=precedence:bd=preordered:av=off_2971 on theBenchmark for (2971ds/3256Mi)
% 103.30/15.70 % (1088452)Refutation not found, incomplete strategy
% 103.30/15.70 % (1088452)------------------------------
% 103.30/15.70 % (1088452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.30/15.70 % (1088452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.30/15.70 % (1088452)CaDiCaL version: 2.1.3
% 103.30/15.70 % (1088452)Termination reason: Refutation not found, incomplete strategy
% 103.30/15.70 % (1088452)Time elapsed: 0.002 s
% 103.30/15.70 % (1088452)Peak memory usage: 87 MB
% 103.30/15.70 % (1088452)Instructions burned: 1 (million)
% 103.30/15.70 % (1088452)------------------------------
% 103.30/15.70 % (1088452)------------------------------
% 103.30/15.70 % (1088455)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2523846977:i=180:bd=preordered:av=off_2965 on theBenchmark for (2965ds/180Mi)
% 103.30/15.70 % (1088455)Instruction limit reached!
% 103.30/15.70 % (1088455)------------------------------
% 103.30/15.70 % (1088455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.30/15.70 % (1088455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.30/15.70 % (1088455)CaDiCaL version: 2.1.3
% 103.30/15.70 % (1088455)Termination reason: Instruction limit
% 103.30/15.70 % (1088455)Termination phase: Saturation
% 103.30/15.70 % (1088455)Time elapsed: 0.175 s
% 103.30/15.70 % (1088455)Peak memory usage: 89 MB
% 103.30/15.70 % (1088455)Instructions burned: 180 (million)
% 103.30/15.70 % (1088457)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=1944992933:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2961 on theBenchmark for (2961ds/10307Mi)
% 103.30/15.70 % (1088427)Instruction limit reached!
% 103.30/15.70 % (1088427)------------------------------
% 103.30/15.70 % (1088427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.30/15.70 % (1088427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.30/15.70 % (1088427)CaDiCaL version: 2.1.3
% 103.30/15.70 % (1088427)Termination reason: Instruction limit
% 103.30/15.70 % (1088427)Termination phase: Saturation
% 103.30/15.70 % (1088427)Time elapsed: 3.522 s
% 103.30/15.70 % (1088427)Peak memory usage: 151 MB
% 103.30/15.70 % (1088427)Instructions burned: 3394 (million)
% 103.30/15.70 % (1088459)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=4169494979:i=412:gtgl=4:gtg=exists_all_2953 on theBenchmark for (2953ds/412Mi)
% 103.30/15.70 % (1088459)Instruction limit reached!
% 103.30/15.70 % (1088459)------------------------------
% 100.78/17.68 % (1088459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.78/17.68 % (1088459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.78/17.68 % (1088459)CaDiCaL version: 2.1.3
% 100.78/17.68 % (1088459)Termination reason: Instruction limit
% 100.78/17.68 % (1088459)Termination phase: Saturation
% 100.78/17.68 % (1088459)Time elapsed: 0.408 s
% 100.78/17.68 % (1088459)Peak memory usage: 96 MB
% 100.78/17.68 % (1088459)Instructions burned: 413 (million)
% 100.78/17.68 % (1088463)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=2115615308:s2pl=no:i=8478:s2at=4:nm=6_2946 on theBenchmark for (2946ds/8478Mi)
% 100.78/17.68 % (1088451)Instruction limit reached!
% 100.78/17.68 % (1088451)------------------------------
% 100.78/17.68 % (1088451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.78/17.68 % (1088451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.78/17.68 % (1088451)CaDiCaL version: 2.1.3
% 100.78/17.68 % (1088451)Termination reason: Instruction limit
% 100.78/17.68 % (1088451)Termination phase: Saturation
% 100.78/17.68 % (1088451)Time elapsed: 3.403 s
% 100.78/17.68 % (1088451)Peak memory usage: 148 MB
% 100.78/17.68 % (1088451)Instructions burned: 3256 (million)
% 100.78/17.68 % (1088470)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=267706083:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2935 on theBenchmark for (2935ds/303Mi)
% 100.78/17.68 % (1088470)Refutation not found, incomplete strategy
% 100.78/17.68 % (1088470)------------------------------
% 100.78/17.68 % (1088470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.78/17.68 % (1088470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.78/17.68 % (1088470)CaDiCaL version: 2.1.3
% 100.78/17.68 % (1088470)Termination reason: Refutation not found, incomplete strategy
% 100.78/17.68 % (1088470)Time elapsed: 0.002 s
% 100.78/17.68 % (1088470)Peak memory usage: 88 MB
% 100.78/17.68 % (1088435)Instruction limit reached!
% 100.78/17.68 % (1088435)------------------------------
% 100.78/17.68 % (1088435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.78/17.68 % (1088435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.78/17.68 % (1088435)CaDiCaL version: 2.1.3
% 100.78/17.68 % (1088435)Termination reason: Instruction limit
% 100.78/17.68 % (1088435)Termination phase: Saturation
% 100.78/17.68 % (1088435)Time elapsed: 5.215 s
% 100.78/17.68 % (1088435)Peak memory usage: 170 MB
% 100.78/17.68 % (1088435)Instructions burned: 5208 (million)
% 100.78/17.68 % (1088473)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2479992312:st=4:i=720:sd=3:fsr=off:ss=axioms_2932 on theBenchmark for (2932ds/720Mi)
% 100.78/17.68 % (1088473)Refutation not found, incomplete strategy
% 100.78/17.68 % (1088473)------------------------------
% 100.78/17.68 % (1088473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.78/17.68 % (1088473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.78/17.68 % (1088473)CaDiCaL version: 2.1.3
% 100.78/17.68 % (1088473)Termination reason: Refutation not found, incomplete strategy
% 100.78/17.68 % (1088473)Time elapsed: 0.001 s
% 100.78/17.68 % (1088473)Peak memory usage: 88 MB
% 100.78/17.68 % (1088470)------------------------------
% 100.78/17.68 % (1088470)------------------------------
% 100.78/17.68 % (1088473)------------------------------
% 100.78/17.68 % (1088473)------------------------------
% 100.78/17.68 % (1088477)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=74712049:i=598:bs=on:bd=preordered:av=off:ss=axioms_2929 on theBenchmark for (2929ds/598Mi)
% 100.78/17.68 % (1088478)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=939971696:i=2989:sd=3:ss=axioms:sgt=60_2928 on theBenchmark for (2928ds/2989Mi)
% 100.78/17.68 % (1088477)Instruction limit reached!
% 100.78/17.68 % (1088477)------------------------------
% 100.78/17.68 % (1088477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.78/17.68 % (1088477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.78/17.68 % (1088477)CaDiCaL version: 2.1.3
% 100.78/17.68 % (1088477)Termination reason: Instruction limit
% 100.78/17.68 % (1088477)Termination phase: Saturation
% 100.78/17.68 % (1088477)Time elapsed: 0.511 s
% 100.78/17.68 % (1088477)Peak memory usage: 98 MB
% 100.78/17.68 % (1088477)Instructions burned: 599 (million)
% 100.78/17.68 % (1088481)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=1513480597:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2922 on theBenchmark for (2922ds/1997Mi)
% 100.78/17.68 % (1088481)Instruction limit reached!
% 100.78/17.68 % (1088481)------------------------------
% 100.78/17.68 % (1088481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.78/17.68 % (1088481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.78/17.68 % (1088481)CaDiCaL version: 2.1.3
% 100.78/17.68 % (1088481)Termination reason: Instruction limit
% 100.78/17.68 % (1088481)Termination phase: Saturation
% 100.78/17.68 % (1088481)Time elapsed: 2.074 s
% 100.78/17.68 % (1088481)Peak memory usage: 140 MB
% 100.78/17.68 % (1088481)Instructions burned: 1997 (million)
% 100.78/17.68 % (1088487)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=581419465:i=2088:bd=preordered:av=off_2899 on theBenchmark for (2899ds/2088Mi)
% 100.78/17.68 % (1088478)Instruction limit reached!
% 100.78/17.68 % (1088478)------------------------------
% 100.78/17.68 % (1088478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.78/17.68 % (1088478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.78/17.68 % (1088478)CaDiCaL version: 2.1.3
% 100.78/17.68 % (1088478)Termination reason: Instruction limit
% 100.78/17.68 % (1088478)Termination phase: Saturation
% 100.78/17.68 % (1088478)Time elapsed: 2.958 s
% 100.78/17.68 % (1088478)Peak memory usage: 148 MB
% 100.78/17.68 % (1088478)Instructions burned: 2989 (million)
% 100.78/17.68 % (1088489)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2156978825:i=1098:nicw=on_2896 on theBenchmark for (2896ds/1098Mi)
% 100.78/17.68 % (1088489)Instruction limit reached!
% 100.78/17.68 % (1088489)------------------------------
% 100.78/17.68 % (1088489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.78/17.68 % (1088489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.78/17.68 % (1088489)CaDiCaL version: 2.1.3
% 100.78/17.68 % (1088489)Termination reason: Instruction limit
% 100.78/17.68 % (1088489)Termination phase: Saturation
% 100.78/17.68 % (1088489)Time elapsed: 1.129 s
% 100.78/17.68 % (1088489)Peak memory usage: 101 MB
% 100.78/17.68 % (1088489)Instructions burned: 1098 (million)
% 100.78/17.68 % (1088495)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=4183009259:i=433:bd=preordered_2882 on theBenchmark for (2882ds/433Mi)
% 100.78/17.68 % (1088495)Refutation not found, incomplete strategy
% 100.78/17.68 % (1088495)------------------------------
% 100.78/17.68 % (1088495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.78/17.68 % (1088495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.78/17.68 % (1088495)CaDiCaL version: 2.1.3
% 100.78/17.68 % (1088495)Termination reason: Refutation not found, incomplete strategy
% 100.78/17.68 % (1088495)Time elapsed: 0.002 s
% 100.78/17.68 % (1088495)Peak memory usage: 88 MB
% 100.78/17.68 % (1088495)Instructions burned: 1 (million)
% 100.78/17.68 % (1088495)------------------------------
% 100.78/17.68 % (1088495)------------------------------
% 100.78/17.68 % (1088487)Instruction limit reached!
% 100.78/17.68 % (1088487)------------------------------
% 100.78/17.68 % (1088487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.78/17.68 % (1088487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.78/17.68 % (1088487)CaDiCaL version: 2.1.3
% 100.78/17.68 % (1088487)Termination reason: Instruction limit
% 100.78/17.68 % (1088487)Termination phase: Saturation
% 100.78/17.68 % (1088487)Time elapsed: 2.121 s
% 100.78/17.68 % (1088487)Peak memory usage: 138 MB
% 100.78/17.68 % (1088487)Instructions burned: 2088 (million)
% 100.78/17.68 % (1088499)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=595068603:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2876 on theBenchmark for (2876ds/2942Mi)
% 100.78/17.68 % (1088500)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=4022981261:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2875 on theBenchmark for (2875ds/6922Mi)
% 100.78/17.68 % (1088463)Instruction limit reached!
% 100.78/17.68 % (1088463)------------------------------
% 100.78/17.68 % (1088463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.78/17.68 % (1088463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.78/17.68 % (1088463)CaDiCaL version: 2.1.3
% 100.78/17.68 % (1088463)Termination reason: Instruction limit
% 100.78/17.68 % (1088463)Termination phase: Saturation
% 100.78/17.68 % (1088463)Time elapsed: 9.041 s
% 100.78/17.68 % (1088463)Peak memory usage: 202 MB
% 100.78/17.68 % (1088463)Instructions burned: 8478 (million)
% 100.78/17.68 % (1088503)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=1824566267:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2854 on theBenchmark for (2854ds/596Mi)
% 100.78/17.68 % (1088503)Refutation not found, incomplete strategy
% 100.78/17.68 % (1088503)------------------------------
% 100.78/17.68 % (1088503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.78/17.68 % (1088503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.78/17.68 % (1088503)CaDiCaL version: 2.1.3
% 100.78/17.68 % (1088503)Termination reason: Refutation not found, incomplete strategy
% 100.78/17.68 % (1088503)Time elapsed: 0.003 s
% 100.78/17.68 % (1088503)Peak memory usage: 88 MB
% 100.78/17.68 % (1088503)Instructions burned: 1 (million)
% 100.78/17.68 % (1088457)Instruction limit reached!
% 100.78/17.68 % (1088457)------------------------------
% 100.78/17.68 % (1088457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.78/17.68 % (1088457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.78/17.68 % (1088457)CaDiCaL version: 2.1.3
% 100.78/17.68 % (1088457)Termination reason: Instruction limit
% 100.78/17.68 % (1088457)Termination phase: Saturation
% 100.78/17.68 % (1088457)Time elapsed: 11.060 s
% 100.78/17.68 % (1088457)Peak memory usage: 200 MB
% 100.78/17.68 % (1088457)Instructions burned: 10307 (million)
% 100.78/17.68 % (1088503)------------------------------
% 100.78/17.68 % (1088503)------------------------------
% 100.78/17.68 % (1088505)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=3424356990:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2848 on theBenchmark for (2848ds/4123Mi)
% 100.78/17.68 % (1088506)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2436442974:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2847 on theBenchmark for (2847ds/16411Mi)
% 100.78/17.68 % (1088499)Instruction limit reached!
% 100.78/17.68 % (1088499)------------------------------
% 100.78/17.68 % (1088499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.78/17.68 % (1088499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.78/17.68 % (1088499)CaDiCaL version: 2.1.3
% 100.78/17.68 % (1088499)Termination reason: Instruction limit
% 100.78/17.68 % (1088499)Termination phase: Saturation
% 100.78/17.68 % (1088499)Time elapsed: 3.272 s
% 100.78/17.68 % (1088499)Peak memory usage: 143 MB
% 100.78/17.68 % (1088499)Instructions burned: 2942 (million)
% 100.78/17.68 % (1088399)First to succeed.
% 100.78/17.68 % (1088399)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1088388"
% 100.78/17.68 % (1088511)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1741225612:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2841 on theBenchmark for (2841ds/1670Mi)
% 100.78/17.68 % (1088399)Refutation found. Thanks to Tanya!
% 100.78/17.68 % SZS status Unsatisfiable for theBenchmark
% 100.78/17.68 % SZS output start Proof for theBenchmark
% See solution above
% 117.98/17.92 % (1088399)------------------------------
% 117.98/17.92 % (1088399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.98/17.92 % (1088399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.98/17.92 % (1088399)CaDiCaL version: 2.1.3
% 117.98/17.92 % (1088399)Termination reason: Refutation
% 117.98/17.92 % (1088399)Time elapsed: 15.883 s
% 117.98/17.92 % (1088399)Peak memory usage: 272 MB
% 117.98/17.92 % (1088399)Instructions burned: 15759 (million)
% 117.98/17.92 % (1088399)------------------------------
% 117.98/17.92 % (1088399)------------------------------
% 117.98/17.92 % (1088388)Success in time 16.544 s
% 117.98/17.92 % Vampire exiting
%------------------------------------------------------------------------------