%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP654+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n009.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:15:21 AM UTC 2026
% Result : Theorem 20.65s 5.61s
% Output : Refutation 34.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 64
% Number of leaves : 11
% Syntax : Number of formulae : 211 ( 199 unt; 5 def)
% Number of atoms : 223 ( 208 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 26 ( 14 ~; 8 |; 2 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 3 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 331 ( 0 sgn 329 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : mult(X1,ld(X1,X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f01) ).
fof(f2,axiom,
! [X0,X1] : ld(X1,mult(X1,X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f02) ).
fof(f3,axiom,
! [X0,X1] : mult(rd(X1,X0),X0) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f03) ).
fof(f4,axiom,
! [X0,X1] : rd(mult(X1,X0),X0) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f04) ).
fof(f5,axiom,
! [X0,X1,X2] : mult(X2,mult(X1,mult(X2,X0))) = mult(mult(mult(X2,X1),X2),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f05) ).
fof(f6,conjecture,
! [X0,X1] :
( mult(X0,rd(X1,X1)) = X0
& mult(rd(X1,X1),X0) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f7,negated_conjecture,
~ ! [X0,X1] :
( mult(X0,rd(X1,X1)) = X0
& mult(rd(X1,X1),X0) = X0 ),
inference(negated_conjecture,[status(cth)],[f6]) ).
fof(f8,plain,
? [X0,X1] :
( mult(X0,rd(X1,X1)) != X0
| mult(rd(X1,X1),X0) != X0 ),
inference(ennf_transformation,[],[f7]) ).
fof(f9,plain,
( sK0 != mult(sK0,rd(sK1,sK1))
| sK0 != mult(rd(sK1,sK1),sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f8]) ).
fof(f10,plain,
! [X0,X1] : mult(X1,ld(X1,X0)) = X0,
inference(cnf_transformation,[],[f1]) ).
fof(f11,plain,
! [X0,X1] : ld(X1,mult(X1,X0)) = X0,
inference(cnf_transformation,[],[f2]) ).
fof(f12,plain,
! [X0,X1] : mult(rd(X1,X0),X0) = X1,
inference(cnf_transformation,[],[f3]) ).
fof(f13,plain,
! [X0,X1] : rd(mult(X1,X0),X0) = X1,
inference(cnf_transformation,[],[f4]) ).
fof(f14,plain,
! [X2,X0,X1] : mult(X2,mult(X1,mult(X2,X0))) = mult(mult(mult(X2,X1),X2),X0),
inference(cnf_transformation,[],[f5]) ).
fof(f15,plain,
( sK0 != mult(sK0,rd(sK1,sK1))
| sK0 != mult(rd(sK1,sK1),sK0) ),
inference(cnf_transformation,[],[f9]) ).
fof(f16,definition,
sF2 = rd(sK1,sK1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f17,plain,
rd(sK1,sK1) = sF2,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF3 = mult(sK0,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f19,plain,
mult(sK0,sF2) = sF3,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF4 = mult(sF2,sK0),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f21,plain,
mult(sF2,sK0) = sF4,
inference(reorient_equations,[],[f20]) ).
fof(f22,plain,
( sK0 != sF3
| sK0 != sF4 ),
inference(definition_folding,[],[f15,f21,f17,f19,f17]) ).
fof(f24,definition,
( spl5_1
<=> sK0 = sF4 ),
introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition]) ).
fof(f26,plain,
( sK0 != sF4
| spl5_1 ),
inference(avatar_component_clause,[],[f24]) ).
fof(f28,definition,
( spl5_2
<=> sK0 = sF3 ),
introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition]) ).
fof(f31,plain,
( ~ spl5_1
| ~ spl5_2 ),
inference(avatar_split_clause,[],[f22,f28,f24]) ).
fof(f32,plain,
sK1 = mult(sF2,sK1),
inference(superposition,[],[f12,f17]) ).
fof(f35,plain,
! [X0,X1] : rd(X0,ld(X1,X0)) = X1,
inference(superposition,[],[f13,f10]) ).
fof(f36,plain,
! [X2,X0,X1] : mult(X1,mult(ld(X1,X0),mult(X1,X2))) = mult(mult(X0,X1),X2),
inference(superposition,[],[f14,f10]) ).
fof(f38,plain,
! [X2,X0,X1] : mult(rd(X0,X1),mult(X1,mult(rd(X0,X1),X2))) = mult(mult(X0,rd(X0,X1)),X2),
inference(superposition,[],[f14,f12]) ).
fof(f43,plain,
! [X2,X0,X1] : mult(mult(X0,X1),X0) = rd(mult(X0,mult(X1,mult(X0,X2))),X2),
inference(superposition,[],[f13,f14]) ).
fof(f44,plain,
! [X2,X0,X1] : mult(X0,mult(X1,mult(X0,ld(mult(mult(X0,X1),X0),X2)))) = X2,
inference(superposition,[],[f10,f14]) ).
fof(f48,plain,
! [X2,X0,X1] : ld(mult(mult(X0,X1),X0),mult(X0,mult(X1,mult(X0,X2)))) = X2,
inference(superposition,[],[f11,f14]) ).
fof(f49,plain,
! [X0,X1] : ld(rd(X0,X1),X0) = X1,
inference(superposition,[],[f11,f12]) ).
fof(f51,plain,
sK0 = ld(sF2,sF4),
inference(superposition,[],[f11,f21]) ).
fof(f53,plain,
! [X2,X0,X1] : mult(mult(X1,X2),X1) = rd(mult(X1,mult(X2,X0)),ld(X1,X0)),
inference(superposition,[],[f43,f10]) ).
fof(f59,plain,
! [X2,X0,X1] : mult(mult(X1,rd(X0,mult(X1,X2))),X1) = rd(mult(X1,X0),X2),
inference(superposition,[],[f43,f12]) ).
fof(f74,plain,
! [X0,X1] : mult(mult(X0,rd(X0,X1)),X1) = mult(rd(X0,X1),mult(X1,X0)),
inference(superposition,[],[f38,f12]) ).
fof(f81,plain,
! [X2,X0,X1] : mult(X1,mult(rd(X0,X1),X2)) = ld(rd(X0,X1),mult(mult(X0,rd(X0,X1)),X2)),
inference(superposition,[],[f11,f38]) ).
fof(f103,plain,
! [X2,X0,X1] : mult(mult(X1,rd(X0,X2)),X1) = rd(mult(X1,X0),ld(X1,X2)),
inference(superposition,[],[f53,f12]) ).
fof(f133,plain,
! [X2,X0,X1] : mult(mult(rd(X0,X1),rd(X1,X2)),rd(X0,X1)) = rd(X0,ld(rd(X0,X1),X2)),
inference(superposition,[],[f103,f12]) ).
fof(f172,plain,
! [X2,X0,X1] : mult(mult(X2,X1),ld(X1,X0)) = mult(X1,mult(ld(X1,X2),X0)),
inference(superposition,[],[f36,f10]) ).
fof(f185,plain,
! [X2,X0,X1] : mult(ld(X1,X0),mult(X1,X2)) = ld(X1,mult(mult(X0,X1),X2)),
inference(superposition,[],[f11,f36]) ).
fof(f218,plain,
! [X2,X0,X1] : ld(X0,X1) = rd(ld(X0,mult(mult(X1,X0),X2)),mult(X0,X2)),
inference(superposition,[],[f13,f185]) ).
fof(f321,plain,
! [X2,X0,X1] : ld(X1,rd(X0,X1)) = rd(ld(X1,mult(X0,X2)),mult(X1,X2)),
inference(superposition,[],[f218,f12]) ).
fof(f546,plain,
! [X2,X0,X1] : mult(X0,rd(X1,mult(X0,X2))) = rd(rd(mult(X0,X1),X2),X0),
inference(superposition,[],[f13,f59]) ).
fof(f594,plain,
! [X2,X0,X1] : mult(X1,mult(rd(X2,X1),ld(mult(X2,rd(X2,X1)),X0))) = ld(rd(X2,X1),X0),
inference(superposition,[],[f81,f10]) ).
fof(f698,plain,
! [X0,X1] : ld(X1,rd(X1,X1)) = rd(X0,mult(X1,X0)),
inference(superposition,[],[f321,f11]) ).
fof(f759,plain,
! [X0,X1] : ld(X1,rd(X1,X1)) = rd(ld(X1,X0),X0),
inference(superposition,[],[f698,f10]) ).
fof(f767,plain,
ld(sF2,rd(sF2,sF2)) = rd(sK0,sF4),
inference(superposition,[],[f698,f21]) ).
fof(f768,plain,
rd(sK1,sK1) = ld(sF2,rd(sF2,sF2)),
inference(superposition,[],[f698,f32]) ).
fof(f770,plain,
! [X0,X1] : rd(X1,X1) = mult(X1,rd(X0,mult(X1,X0))),
inference(superposition,[],[f10,f698]) ).
fof(f776,plain,
! [X2,X0,X1] : mult(rd(X0,mult(X1,X0)),mult(X1,X2)) = ld(X1,mult(mult(rd(X1,X1),X1),X2)),
inference(superposition,[],[f185,f698]) ).
fof(f782,plain,
! [X0,X1] : mult(X0,X1) = ld(ld(X0,rd(X0,X0)),X1),
inference(superposition,[],[f49,f698]) ).
fof(f792,plain,
! [X2,X0,X1] : ld(X1,mult(X1,X2)) = mult(rd(X0,mult(X1,X0)),mult(X1,X2)),
inference(forward_demodulation,[],[f776,f12]) ).
fof(f794,plain,
sF2 = ld(sF2,rd(sF2,sF2)),
inference(forward_demodulation,[],[f768,f17]) ).
fof(f804,plain,
! [X2,X0,X1] : mult(rd(X0,mult(X1,X0)),mult(X1,X2)) = X2,
inference(forward_demodulation,[],[f792,f11]) ).
fof(f806,plain,
sF2 = rd(sK0,sF4),
inference(forward_demodulation,[],[f794,f767]) ).
fof(f819,plain,
sF4 = ld(sF2,sK0),
inference(superposition,[],[f49,f806]) ).
fof(f838,plain,
! [X2,X0,X1] : rd(ld(X0,X1),X1) = rd(ld(X0,X2),X2),
inference(superposition,[],[f759,f759]) ).
fof(f852,plain,
! [X0,X1] : rd(X0,X0) = mult(X0,rd(ld(X0,X1),X1)),
inference(superposition,[],[f10,f759]) ).
fof(f861,plain,
! [X0,X1] : ld(X0,X1) = mult(ld(X0,rd(X0,X0)),X1),
inference(superposition,[],[f12,f759]) ).
fof(f909,plain,
! [X0] : mult(rd(sK1,sK1),mult(sF2,X0)) = X0,
inference(superposition,[],[f804,f32]) ).
fof(f912,plain,
! [X2,X0,X1] : ld(X2,X0) = mult(rd(X1,mult(X2,X1)),X0),
inference(superposition,[],[f804,f10]) ).
fof(f933,plain,
! [X2,X0,X1] : mult(X2,X0) = ld(rd(X1,mult(X2,X1)),X0),
inference(superposition,[],[f11,f804]) ).
fof(f965,plain,
! [X0] : mult(sF2,mult(sF2,X0)) = X0,
inference(forward_demodulation,[],[f909,f17]) ).
fof(f999,plain,
! [X0] : ld(mult(mult(sF2,sF2),sF2),mult(sF2,X0)) = X0,
inference(superposition,[],[f48,f965]) ).
fof(f1000,plain,
! [X0] : mult(mult(sF2,sF2),sF2) = rd(mult(sF2,X0),X0),
inference(superposition,[],[f43,f965]) ).
fof(f1001,plain,
! [X0] : mult(sF2,X0) = ld(sF2,X0),
inference(superposition,[],[f11,f965]) ).
fof(f1029,plain,
sF2 = mult(mult(sF2,sF2),sF2),
inference(forward_demodulation,[],[f1000,f13]) ).
fof(f1030,plain,
! [X0] : ld(mult(mult(sF2,sF2),sF2),ld(sF2,X0)) = X0,
inference(forward_demodulation,[],[f999,f1001]) ).
fof(f1037,plain,
sF2 = mult(ld(sF2,sF2),sF2),
inference(forward_demodulation,[],[f1029,f1001]) ).
fof(f1038,plain,
! [X0] : ld(mult(ld(sF2,sF2),sF2),ld(sF2,X0)) = X0,
inference(forward_demodulation,[],[f1030,f1001]) ).
fof(f1043,plain,
! [X0] : ld(sF2,ld(sF2,X0)) = X0,
inference(forward_demodulation,[],[f1038,f1037]) ).
fof(f1055,plain,
! [X0] : sF2 = rd(ld(sF2,X0),X0),
inference(superposition,[],[f13,f1001]) ).
fof(f1065,plain,
! [X0,X1] : mult(ld(sF2,X1),ld(sF2,X0)) = ld(sF2,mult(mult(X1,sF2),X0)),
inference(superposition,[],[f185,f1001]) ).
fof(f1130,plain,
! [X2,X0,X1] : mult(rd(X1,X0),X2) = ld(rd(X0,X1),X2),
inference(superposition,[],[f912,f12]) ).
fof(f1166,plain,
! [X2,X3,X0,X1] : ld(rd(X2,mult(X0,X2)),rd(X3,rd(X2,mult(X0,X2)))) = rd(ld(rd(X2,mult(X0,X2)),mult(X3,X1)),ld(X0,X1)),
inference(superposition,[],[f321,f912]) ).
fof(f1190,plain,
! [X2,X3,X0,X1] : ld(rd(X2,mult(X0,X2)),rd(X3,rd(X2,mult(X0,X2)))) = rd(mult(X0,mult(X3,X1)),ld(X0,X1)),
inference(forward_demodulation,[],[f1166,f933]) ).
fof(f1234,plain,
! [X2,X3,X0,X1] : ld(rd(X2,mult(X0,X2)),rd(X3,rd(X2,mult(X0,X2)))) = mult(mult(X0,rd(mult(X3,X1),X1)),X0),
inference(forward_demodulation,[],[f1190,f103]) ).
fof(f1249,plain,
! [X2,X3,X0] : ld(rd(X2,mult(X0,X2)),rd(X3,rd(X2,mult(X0,X2)))) = mult(mult(X0,X3),X0),
inference(forward_demodulation,[],[f1234,f13]) ).
fof(f1258,plain,
! [X2,X3,X0] : mult(mult(X0,X3),X0) = mult(X0,rd(X3,rd(X2,mult(X0,X2)))),
inference(forward_demodulation,[],[f1249,f933]) ).
fof(f1290,plain,
! [X2,X0,X1] : rd(X1,X0) = rd(ld(rd(X0,X1),X2),X2),
inference(superposition,[],[f13,f1130]) ).
fof(f1304,plain,
! [X2,X3,X0,X1] : ld(rd(X1,X0),rd(X3,rd(X1,X0))) = rd(ld(rd(X1,X0),mult(X3,X2)),ld(rd(X0,X1),X2)),
inference(superposition,[],[f321,f1130]) ).
fof(f1309,plain,
! [X2,X0,X1] : ld(rd(X0,X1),ld(rd(X1,X0),X2)) = X2,
inference(superposition,[],[f10,f1130]) ).
fof(f1311,plain,
! [X2,X3,X0,X1] : mult(mult(rd(X1,X0),X2),rd(X1,X0)) = rd(ld(rd(X0,X1),mult(X2,X3)),ld(rd(X1,X0),X3)),
inference(superposition,[],[f53,f1130]) ).
fof(f1327,plain,
! [X2,X3,X0,X1] : mult(ld(rd(X0,X1),X2),rd(X1,X0)) = rd(ld(rd(X0,X1),mult(X2,X3)),ld(rd(X1,X0),X3)),
inference(forward_demodulation,[],[f1311,f1130]) ).
fof(f1363,plain,
! [X2,X0,X1] : ld(rd(X0,X1),rd(X2,rd(X0,X1))) = mult(ld(rd(X0,X1),X2),rd(X1,X0)),
inference(forward_demodulation,[],[f1327,f1304]) ).
fof(f1585,plain,
! [X0,X1] : rd(rd(X0,X1),rd(X0,X1)) = mult(rd(X0,X1),rd(X1,X0)),
inference(superposition,[],[f770,f12]) ).
fof(f1603,plain,
! [X0,X1] : mult(mult(X0,X0),mult(rd(X0,mult(X0,X0)),X1)) = ld(rd(X0,mult(X0,X0)),mult(rd(X0,X0),X1)),
inference(superposition,[],[f81,f770]) ).
fof(f1604,plain,
! [X0] : mult(rd(X0,X0),mult(X0,X0)) = mult(rd(X0,mult(X0,X0)),mult(mult(X0,X0),X0)),
inference(superposition,[],[f74,f770]) ).
fof(f1618,plain,
! [X2,X0,X1] : ld(rd(X1,mult(X0,X1)),X0) = rd(ld(rd(X1,mult(X0,X1)),mult(rd(X0,X0),X2)),mult(rd(X1,mult(X0,X1)),X2)),
inference(superposition,[],[f218,f770]) ).
fof(f1656,plain,
! [X0,X1] : ld(rd(X1,mult(X0,X1)),X0) = ld(rd(X1,mult(X0,X1)),rd(rd(X0,X0),rd(X1,mult(X0,X1)))),
inference(forward_demodulation,[],[f1618,f321]) ).
fof(f1663,plain,
! [X0] : mult(rd(X0,X0),mult(X0,X0)) = ld(rd(mult(X0,X0),X0),mult(mult(X0,X0),X0)),
inference(forward_demodulation,[],[f1604,f1130]) ).
fof(f1664,plain,
! [X0,X1] : mult(mult(X0,X0),mult(rd(X0,mult(X0,X0)),X1)) = mult(X0,mult(rd(X0,X0),X1)),
inference(forward_demodulation,[],[f1603,f933]) ).
fof(f1680,plain,
! [X0,X1] : rd(rd(X0,X1),rd(X0,X1)) = ld(rd(X1,X0),rd(X1,X0)),
inference(forward_demodulation,[],[f1585,f1130]) ).
fof(f1696,plain,
! [X0,X1] : ld(rd(X1,mult(X0,X1)),X0) = mult(X0,rd(rd(X0,X0),rd(X1,mult(X0,X1)))),
inference(forward_demodulation,[],[f1656,f933]) ).
fof(f1700,plain,
! [X0] : mult(rd(X0,X0),mult(X0,X0)) = ld(X0,mult(mult(X0,X0),X0)),
inference(forward_demodulation,[],[f1663,f13]) ).
fof(f1701,plain,
! [X0,X1] : mult(mult(X0,X0),mult(rd(X0,mult(X0,X0)),X1)) = mult(X0,ld(rd(X0,X0),X1)),
inference(forward_demodulation,[],[f1664,f1130]) ).
fof(f1718,plain,
! [X0,X1] : mult(mult(X0,rd(X0,X0)),X0) = ld(rd(X1,mult(X0,X1)),X0),
inference(forward_demodulation,[],[f1696,f1258]) ).
fof(f1722,plain,
! [X0] : ld(X0,mult(mult(X0,X0),X0)) = ld(rd(X0,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f1700,f1130]) ).
fof(f1723,plain,
! [X0,X1] : mult(X0,ld(rd(X0,X0),X1)) = mult(mult(X0,X0),ld(rd(mult(X0,X0),X0),X1)),
inference(forward_demodulation,[],[f1701,f1130]) ).
fof(f1729,plain,
! [X0] : mult(X0,X0) = mult(mult(X0,rd(X0,X0)),X0),
inference(forward_demodulation,[],[f1718,f933]) ).
fof(f1732,plain,
! [X0,X1] : mult(X0,ld(rd(X0,X0),X1)) = mult(mult(X0,X0),ld(X0,X1)),
inference(forward_demodulation,[],[f1723,f13]) ).
fof(f1736,plain,
! [X0] : mult(X0,X0) = mult(rd(X0,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f1729,f74]) ).
fof(f1738,plain,
! [X0,X1] : mult(X0,ld(rd(X0,X0),X1)) = mult(X0,mult(ld(X0,X0),X1)),
inference(forward_demodulation,[],[f1732,f172]) ).
fof(f1739,plain,
! [X0] : mult(X0,X0) = ld(rd(X0,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f1736,f1130]) ).
fof(f1740,plain,
! [X0] : mult(X0,X0) = ld(X0,mult(mult(X0,X0),X0)),
inference(forward_demodulation,[],[f1739,f1722]) ).
fof(f2520,plain,
! [X2,X0,X1] : ld(ld(X0,rd(X0,X0)),rd(X2,ld(X0,rd(X0,X0)))) = rd(ld(ld(X0,rd(X0,X0)),mult(X2,X1)),ld(X0,X1)),
inference(superposition,[],[f321,f861]) ).
fof(f2559,plain,
! [X2,X0,X1] : ld(ld(X0,rd(X0,X0)),rd(X2,ld(X0,rd(X0,X0)))) = rd(mult(X0,mult(X2,X1)),ld(X0,X1)),
inference(forward_demodulation,[],[f2520,f782]) ).
fof(f2595,plain,
! [X2,X0,X1] : ld(ld(X0,rd(X0,X0)),rd(X2,ld(X0,rd(X0,X0)))) = mult(mult(X0,rd(mult(X2,X1),X1)),X0),
inference(forward_demodulation,[],[f2559,f103]) ).
fof(f2614,plain,
! [X2,X0] : mult(mult(X0,X2),X0) = ld(ld(X0,rd(X0,X0)),rd(X2,ld(X0,rd(X0,X0)))),
inference(forward_demodulation,[],[f2595,f13]) ).
fof(f2621,plain,
! [X2,X0] : mult(mult(X0,X2),X0) = mult(X0,rd(X2,ld(X0,rd(X0,X0)))),
inference(forward_demodulation,[],[f2614,f782]) ).
fof(f2643,plain,
! [X0] : rd(X0,X0) = mult(mult(X0,ld(X0,ld(X0,rd(X0,X0)))),X0),
inference(superposition,[],[f852,f2621]) ).
fof(f2711,plain,
! [X0] : rd(X0,X0) = mult(ld(X0,rd(X0,X0)),X0),
inference(forward_demodulation,[],[f2643,f10]) ).
fof(f2742,plain,
! [X0] : rd(X0,X0) = ld(X0,X0),
inference(forward_demodulation,[],[f2711,f861]) ).
fof(f2806,plain,
! [X0] : ld(ld(X0,X0),X0) = X0,
inference(superposition,[],[f49,f2742]) ).
fof(f2808,plain,
! [X0,X1] : mult(X0,mult(ld(X0,X0),X1)) = ld(ld(X0,X0),mult(mult(X0,ld(X0,X0)),X1)),
inference(superposition,[],[f81,f2742]) ).
fof(f2814,plain,
! [X0,X1] : mult(ld(X0,X0),X1) = ld(ld(X0,X0),X1),
inference(superposition,[],[f1130,f2742]) ).
fof(f2819,plain,
sF2 = ld(sK1,sK1),
inference(superposition,[],[f17,f2742]) ).
fof(f2826,plain,
! [X0,X1] : mult(X0,mult(ld(X0,X0),X1)) = ld(ld(X0,X0),mult(X0,X1)),
inference(forward_demodulation,[],[f2808,f10]) ).
fof(f2833,plain,
! [X0,X1] : mult(X0,ld(rd(X0,X0),X1)) = ld(ld(X0,X0),mult(X0,X1)),
inference(forward_demodulation,[],[f2826,f1738]) ).
fof(f2837,plain,
! [X0,X1] : ld(ld(X0,X0),mult(X0,X1)) = mult(X0,ld(ld(X0,X0),X1)),
inference(forward_demodulation,[],[f2833,f2742]) ).
fof(f2841,plain,
sK1 = mult(sK1,sF2),
inference(superposition,[],[f10,f2819]) ).
fof(f2842,plain,
sK1 = rd(sK1,sF2),
inference(superposition,[],[f35,f2819]) ).
fof(f2861,plain,
! [X0] : rd(X0,ld(rd(X0,sK1),sF2)) = mult(mult(rd(X0,sK1),sK1),rd(X0,sK1)),
inference(superposition,[],[f133,f2842]) ).
fof(f2872,plain,
! [X0] : rd(X0,ld(rd(X0,sK1),sF2)) = mult(X0,rd(X0,sK1)),
inference(forward_demodulation,[],[f2861,f12]) ).
fof(f2960,plain,
! [X0] : ld(X0,X0) = rd(mult(X0,X0),mult(X0,X0)),
inference(superposition,[],[f218,f1740]) ).
fof(f2962,plain,
! [X0] : mult(mult(X0,X0),X0) = mult(X0,mult(X0,X0)),
inference(superposition,[],[f10,f1740]) ).
fof(f2979,plain,
! [X0] : ld(X0,X0) = ld(mult(X0,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f2960,f2742]) ).
fof(f3019,plain,
! [X0] : mult(X0,X0) = rd(mult(X0,mult(X0,X0)),X0),
inference(superposition,[],[f13,f2962]) ).
fof(f4447,plain,
! [X0,X1] : mult(mult(X1,mult(rd(X0,mult(X1,X0)),mult(rd(X0,mult(X1,X0)),rd(X0,mult(X1,X0))))),X1) = mult(X1,mult(rd(X0,mult(X1,X0)),rd(X0,mult(X1,X0)))),
inference(superposition,[],[f1258,f3019]) ).
fof(f4448,plain,
! [X0,X1] : mult(mult(X1,mult(rd(X0,mult(X1,X0)),ld(rd(mult(X1,X0),X0),rd(X0,mult(X1,X0))))),X1) = mult(X1,ld(rd(mult(X1,X0),X0),rd(X0,mult(X1,X0)))),
inference(forward_demodulation,[],[f4447,f1130]) ).
fof(f4471,plain,
! [X0,X1] : mult(mult(X1,mult(rd(X0,mult(X1,X0)),ld(X1,rd(X0,mult(X1,X0))))),X1) = mult(X1,ld(X1,rd(X0,mult(X1,X0)))),
inference(forward_demodulation,[],[f4448,f13]) ).
fof(f4484,plain,
! [X0,X1] : rd(X0,mult(X1,X0)) = mult(mult(X1,mult(rd(X0,mult(X1,X0)),ld(X1,rd(X0,mult(X1,X0))))),X1),
inference(forward_demodulation,[],[f4471,f10]) ).
fof(f4489,plain,
! [X0,X1] : rd(X0,mult(X1,X0)) = mult(mult(X1,ld(rd(mult(X1,X0),X0),ld(X1,rd(X0,mult(X1,X0))))),X1),
inference(forward_demodulation,[],[f4484,f1130]) ).
fof(f4493,plain,
! [X0,X1] : rd(X0,mult(X1,X0)) = mult(mult(X1,ld(X1,ld(X1,rd(X0,mult(X1,X0))))),X1),
inference(forward_demodulation,[],[f4489,f13]) ).
fof(f4496,plain,
! [X0,X1] : rd(X0,mult(X1,X0)) = mult(ld(X1,rd(X0,mult(X1,X0))),X1),
inference(forward_demodulation,[],[f4493,f10]) ).
fof(f4550,plain,
! [X0,X1] : ld(X1,rd(X0,mult(X1,X0))) = rd(rd(X0,mult(X1,X0)),X1),
inference(superposition,[],[f13,f4496]) ).
fof(f4930,plain,
! [X2,X0,X1] : ld(rd(X2,mult(X0,X2)),rd(X1,ld(X0,X1))) = rd(rd(X1,ld(X0,X1)),rd(X2,mult(X0,X2))),
inference(superposition,[],[f4550,f912]) ).
fof(f4987,plain,
! [X2,X0] : ld(rd(X2,mult(X0,X2)),X0) = rd(X0,rd(X2,mult(X0,X2))),
inference(forward_demodulation,[],[f4930,f35]) ).
fof(f5016,plain,
! [X2,X0] : mult(X0,X0) = rd(X0,rd(X2,mult(X0,X2))),
inference(forward_demodulation,[],[f4987,f933]) ).
fof(f5098,plain,
! [X2,X0,X1] : mult(mult(X0,X0),X2) = ld(rd(rd(X1,mult(X0,X1)),X0),X2),
inference(superposition,[],[f1130,f5016]) ).
fof(f5100,plain,
! [X0,X1] : rd(mult(X0,X0),mult(X0,X0)) = ld(rd(rd(X1,mult(X0,X1)),X0),rd(rd(X1,mult(X0,X1)),X0)),
inference(superposition,[],[f1680,f5016]) ).
fof(f5105,plain,
! [X0,X1] : rd(mult(X0,X0),mult(X0,X0)) = ld(ld(X0,rd(X1,mult(X0,X1))),ld(X0,rd(X1,mult(X0,X1)))),
inference(forward_demodulation,[],[f5100,f4550]) ).
fof(f5107,plain,
! [X2,X0,X1] : mult(mult(X0,X0),X2) = ld(ld(X0,rd(X1,mult(X0,X1))),X2),
inference(forward_demodulation,[],[f5098,f4550]) ).
fof(f5147,plain,
! [X0,X1] : ld(mult(X0,X0),mult(X0,X0)) = ld(ld(X0,rd(X1,mult(X0,X1))),ld(X0,rd(X1,mult(X0,X1)))),
inference(forward_demodulation,[],[f5105,f2742]) ).
fof(f5172,plain,
! [X0,X1] : ld(mult(X0,X0),mult(X0,X0)) = mult(mult(X0,X0),ld(X0,rd(X1,mult(X0,X1)))),
inference(forward_demodulation,[],[f5147,f5107]) ).
fof(f5180,plain,
! [X0,X1] : ld(mult(X0,X0),mult(X0,X0)) = mult(X0,mult(ld(X0,X0),rd(X1,mult(X0,X1)))),
inference(forward_demodulation,[],[f5172,f172]) ).
fof(f5186,plain,
! [X0,X1] : ld(mult(X0,X0),mult(X0,X0)) = mult(X0,ld(rd(X0,X0),rd(X1,mult(X0,X1)))),
inference(forward_demodulation,[],[f5180,f1738]) ).
fof(f5191,plain,
! [X0,X1] : ld(mult(X0,X0),mult(X0,X0)) = mult(X0,ld(ld(X0,X0),rd(X1,mult(X0,X1)))),
inference(forward_demodulation,[],[f5186,f2742]) ).
fof(f5193,plain,
! [X0,X1] : ld(mult(X0,X0),mult(X0,X0)) = ld(ld(X0,X0),mult(X0,rd(X1,mult(X0,X1)))),
inference(forward_demodulation,[],[f5191,f2837]) ).
fof(f5195,plain,
! [X0] : ld(ld(X0,X0),rd(X0,X0)) = ld(mult(X0,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f5193,f770]) ).
fof(f5197,plain,
! [X0] : ld(X0,X0) = ld(ld(X0,X0),rd(X0,X0)),
inference(forward_demodulation,[],[f5195,f2979]) ).
fof(f5198,plain,
! [X0] : ld(X0,X0) = ld(ld(X0,X0),ld(X0,X0)),
inference(forward_demodulation,[],[f5197,f2742]) ).
fof(f5691,plain,
mult(sK1,sF2) = rd(sK1,ld(sF2,sF2)),
inference(superposition,[],[f2872,f17]) ).
fof(f5721,plain,
sK1 = rd(sK1,ld(sF2,sF2)),
inference(forward_demodulation,[],[f5691,f2841]) ).
fof(f5757,plain,
ld(sF2,sF2) = ld(sK1,sK1),
inference(superposition,[],[f49,f5721]) ).
fof(f5778,plain,
sF2 = ld(sF2,sF2),
inference(forward_demodulation,[],[f5757,f2819]) ).
fof(f20171,plain,
! [X2,X0,X1] : ld(X1,X0) = mult(X2,mult(X1,ld(mult(mult(X1,X2),X1),X0))),
inference(superposition,[],[f11,f44]) ).
fof(f20815,plain,
! [X2,X0,X1] : ld(X2,ld(X0,X1)) = mult(X0,ld(mult(mult(X0,X2),X0),X1)),
inference(superposition,[],[f11,f20171]) ).
fof(f21373,plain,
! [X2,X3,X0,X1] : ld(X0,ld(rd(X1,mult(X2,X1)),X3)) = ld(X2,ld(mult(mult(rd(X1,mult(X2,X1)),X0),rd(X1,mult(X2,X1))),X3)),
inference(superposition,[],[f912,f20815]) ).
fof(f21388,plain,
! [X2,X3,X0,X1] : ld(X0,ld(rd(X1,mult(X2,X1)),X3)) = ld(X2,ld(mult(ld(rd(mult(X2,X1),X1),X0),rd(X1,mult(X2,X1))),X3)),
inference(forward_demodulation,[],[f21373,f1130]) ).
fof(f21514,plain,
! [X2,X3,X0,X1] : ld(X0,ld(rd(X1,mult(X2,X1)),X3)) = ld(X2,ld(ld(rd(mult(X2,X1),X1),rd(X0,rd(mult(X2,X1),X1))),X3)),
inference(forward_demodulation,[],[f21388,f1363]) ).
fof(f21593,plain,
! [X2,X3,X0,X1] : ld(X0,ld(rd(X1,mult(X2,X1)),X3)) = ld(X2,ld(ld(X2,rd(X0,X2)),X3)),
inference(forward_demodulation,[],[f21514,f13]) ).
fof(f21633,plain,
! [X2,X3,X0] : ld(X0,mult(X2,X3)) = ld(X2,ld(ld(X2,rd(X0,X2)),X3)),
inference(forward_demodulation,[],[f21593,f933]) ).
fof(f27004,plain,
! [X0] : rd(rd(sF4,X0),sF2) = mult(sF2,rd(sK0,mult(sF2,X0))),
inference(superposition,[],[f546,f21]) ).
fof(f27134,plain,
! [X0] : rd(rd(sF4,X0),sF2) = ld(sF2,rd(sK0,mult(sF2,X0))),
inference(forward_demodulation,[],[f27004,f1001]) ).
fof(f27210,plain,
! [X0] : rd(rd(sF4,X0),sF2) = ld(sF2,rd(sK0,ld(sF2,X0))),
inference(forward_demodulation,[],[f27134,f1001]) ).
fof(f65865,plain,
ld(sF2,rd(sK0,sK0)) = rd(rd(sF4,sF4),sF2),
inference(superposition,[],[f27210,f51]) ).
fof(f65973,plain,
rd(ld(sF4,sF4),sF2) = ld(sF2,rd(sK0,sK0)),
inference(forward_demodulation,[],[f65865,f2742]) ).
fof(f66016,plain,
rd(ld(sF4,sF4),sF2) = ld(sF2,ld(sK0,sK0)),
inference(forward_demodulation,[],[f65973,f2742]) ).
fof(f66101,plain,
! [X0] : ld(ld(sF2,ld(sK0,sK0)),X0) = mult(sF2,mult(ld(sF2,ld(sK0,sK0)),ld(mult(ld(sF4,sF4),ld(sF2,ld(sK0,sK0))),X0))),
inference(superposition,[],[f594,f66016]) ).
fof(f66107,plain,
! [X0] : mult(ld(sF2,ld(sK0,sK0)),X0) = ld(rd(sF2,ld(sF4,sF4)),X0),
inference(superposition,[],[f1130,f66016]) ).
fof(f66108,plain,
! [X0] : rd(sF2,ld(sF4,sF4)) = rd(ld(ld(sF2,ld(sK0,sK0)),X0),X0),
inference(superposition,[],[f1290,f66016]) ).
fof(f66109,plain,
! [X0] : ld(rd(sF2,ld(sF4,sF4)),ld(ld(sF2,ld(sK0,sK0)),X0)) = X0,
inference(superposition,[],[f1309,f66016]) ).
fof(f66128,plain,
! [X0] : ld(ld(sF4,sF4),mult(sF2,X0)) = ld(sF2,ld(ld(sF2,ld(sF2,ld(sK0,sK0))),X0)),
inference(superposition,[],[f21633,f66016]) ).
fof(f66147,plain,
! [X0] : ld(ld(sF4,sF4),mult(sF2,X0)) = ld(sF2,ld(ld(sK0,sK0),X0)),
inference(forward_demodulation,[],[f66128,f1043]) ).
fof(f66161,plain,
! [X0] : ld(ld(sF2,ld(sK0,sK0)),X0) = ld(sF2,mult(ld(sF2,ld(sK0,sK0)),ld(mult(ld(sF4,sF4),ld(sF2,ld(sK0,sK0))),X0))),
inference(forward_demodulation,[],[f66101,f1001]) ).
fof(f66182,plain,
! [X0] : ld(ld(sF4,sF4),ld(sF2,X0)) = ld(sF2,ld(ld(sK0,sK0),X0)),
inference(forward_demodulation,[],[f66147,f1001]) ).
fof(f66190,plain,
! [X0] : ld(ld(sF2,ld(sK0,sK0)),X0) = ld(sF2,ld(rd(sF2,ld(sF4,sF4)),ld(mult(ld(sF4,sF4),ld(sF2,ld(sK0,sK0))),X0))),
inference(forward_demodulation,[],[f66161,f66107]) ).
fof(f66212,plain,
! [X0] : ld(ld(sF2,ld(sK0,sK0)),X0) = ld(sF2,ld(rd(sF2,ld(sF4,sF4)),ld(ld(ld(sF4,sF4),ld(sF2,ld(sK0,sK0))),X0))),
inference(forward_demodulation,[],[f66190,f2814]) ).
fof(f66231,plain,
! [X0] : ld(ld(sF2,ld(sK0,sK0)),X0) = ld(sF2,ld(rd(sF2,ld(sF4,sF4)),ld(ld(sF2,ld(ld(sK0,sK0),ld(sK0,sK0))),X0))),
inference(forward_demodulation,[],[f66212,f66182]) ).
fof(f66243,plain,
! [X0] : ld(ld(sF2,ld(sK0,sK0)),X0) = ld(sF2,ld(rd(sF2,ld(sF4,sF4)),ld(ld(sF2,ld(sK0,sK0)),X0))),
inference(forward_demodulation,[],[f66231,f5198]) ).
fof(f66249,plain,
! [X0] : ld(sF2,X0) = ld(ld(sF2,ld(sK0,sK0)),X0),
inference(forward_demodulation,[],[f66243,f66109]) ).
fof(f81156,plain,
! [X0,X1] : rd(ld(sF2,X0),X0) = rd(ld(ld(sF2,ld(sK0,sK0)),X1),X1),
inference(superposition,[],[f838,f66249]) ).
fof(f81216,plain,
! [X0] : rd(X0,mult(ld(sF2,ld(sK0,sK0)),X0)) = mult(ld(sF2,rd(X0,mult(ld(sF2,ld(sK0,sK0)),X0))),ld(sF2,ld(sK0,sK0))),
inference(superposition,[],[f4496,f66249]) ).
fof(f81238,plain,
! [X0] : rd(X0,mult(ld(sF2,ld(sK0,sK0)),X0)) = ld(sF2,mult(mult(rd(X0,mult(ld(sF2,ld(sK0,sK0)),X0)),sF2),ld(sK0,sK0))),
inference(forward_demodulation,[],[f81216,f1065]) ).
fof(f81298,plain,
! [X0] : rd(ld(sF2,X0),X0) = rd(sF2,ld(sF4,sF4)),
inference(forward_demodulation,[],[f81156,f66108]) ).
fof(f81364,plain,
! [X0] : rd(X0,mult(ld(sF2,ld(sK0,sK0)),X0)) = ld(sF2,mult(ld(rd(mult(ld(sF2,ld(sK0,sK0)),X0),X0),sF2),ld(sK0,sK0))),
inference(forward_demodulation,[],[f81238,f1130]) ).
fof(f81421,plain,
sF2 = rd(sF2,ld(sF4,sF4)),
inference(forward_demodulation,[],[f81298,f1055]) ).
fof(f81478,plain,
! [X0] : rd(X0,mult(ld(sF2,ld(sK0,sK0)),X0)) = ld(sF2,mult(ld(ld(sF2,ld(sK0,sK0)),sF2),ld(sK0,sK0))),
inference(forward_demodulation,[],[f81364,f13]) ).
fof(f81584,plain,
! [X0] : rd(X0,mult(ld(sF2,ld(sK0,sK0)),X0)) = ld(sF2,mult(ld(sF2,sF2),ld(sK0,sK0))),
inference(forward_demodulation,[],[f81478,f66249]) ).
fof(f81674,plain,
! [X0] : rd(X0,mult(ld(sF2,ld(sK0,sK0)),X0)) = ld(sF2,ld(ld(sF2,sF2),ld(sK0,sK0))),
inference(forward_demodulation,[],[f81584,f2814]) ).
fof(f81750,plain,
! [X0] : ld(sF2,ld(sF2,ld(sK0,sK0))) = rd(X0,mult(ld(sF2,ld(sK0,sK0)),X0)),
inference(forward_demodulation,[],[f81674,f5778]) ).
fof(f81807,plain,
! [X0] : ld(sF2,ld(sF2,ld(sK0,sK0))) = rd(X0,ld(rd(sF2,ld(sF4,sF4)),X0)),
inference(forward_demodulation,[],[f81750,f66107]) ).
fof(f81855,plain,
rd(sF2,ld(sF4,sF4)) = ld(sF2,ld(sF2,ld(sK0,sK0))),
inference(forward_demodulation,[],[f81807,f35]) ).
fof(f81897,plain,
ld(sK0,sK0) = rd(sF2,ld(sF4,sF4)),
inference(forward_demodulation,[],[f81855,f1043]) ).
fof(f81926,plain,
sF2 = ld(sK0,sK0),
inference(forward_demodulation,[],[f81897,f81421]) ).
fof(f81999,plain,
sK0 = ld(sF2,sK0),
inference(superposition,[],[f2806,f81926]) ).
fof(f82016,plain,
sK0 = mult(sK0,sF2),
inference(superposition,[],[f10,f81926]) ).
fof(f82076,plain,
sK0 = sF3,
inference(forward_demodulation,[],[f82016,f19]) ).
fof(f82082,plain,
sK0 = sF4,
inference(forward_demodulation,[],[f81999,f819]) ).
fof(f82102,plain,
spl5_2,
inference(avatar_split_clause,[],[f82076,f28]) ).
fof(f82106,plain,
( $false
| spl5_1 ),
inference(forward_subsumption_resolution,[],[f82082,f26]) ).
fof(f82107,plain,
spl5_1,
inference(avatar_contradiction_clause,[],[f82106]) ).
cnf(s1,plain,
( ~ spl5_1
| ~ spl5_2 ),
inference(sat_conversion,[],[f31]) ).
cnf(s2,plain,
spl5_2,
inference(sat_conversion,[],[f82102]) ).
cnf(s3,plain,
spl5_1,
inference(sat_conversion,[],[f82107]) ).
cnf(s5,plain,
$false,
inference(rat,[],[s1,s2,s3]) ).
fof(f82122,plain,
$false,
inference(avatar_sat_refutation,[],[s5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP654+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n009.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 10:31:14 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.35/2.73 % (1833349)Detected formulas, will run a generic FOF schedule.
% 12.35/2.73 % (1833355)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=1506622126:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.35/2.73 % (1833354)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=1373160237:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.35/2.73 % (1833356)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=2085769031:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.35/2.73 % (1833360)dis-21_1_sil=8000:lcm=predicate:random_seed=528764477: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.35/2.73 % (1833357)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4002645520:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.35/2.73 % (1833358)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1150292951:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.35/2.73 % (1833357)Refutation not found, incomplete strategy
% 12.35/2.73 % (1833357)------------------------------
% 12.35/2.73 % (1833357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.35/2.73 % (1833357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.73 % (1833360)Refutation not found, incomplete strategy
% 12.35/2.73 % (1833360)------------------------------
% 12.35/2.73 % (1833360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.35/2.73 % (1833360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.73 % (1833357)CaDiCaL version: 2.1.3
% 12.35/2.73 % (1833357)Termination reason: Refutation not found, incomplete strategy
% 12.35/2.73 % (1833357)Time elapsed: 0.001 s
% 12.35/2.73 % (1833360)CaDiCaL version: 2.1.3
% 12.35/2.73 % (1833357)Peak memory usage: 88 MB
% 12.35/2.73 % (1833360)Termination reason: Refutation not found, incomplete strategy
% 12.35/2.73 % (1833360)Time elapsed: 0.001 s
% 12.35/2.73 % (1833360)Peak memory usage: 88 MB
% 12.35/2.73 % (1833359)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3111014451:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.35/2.73 % (1833358)Instruction limit reached!
% 12.35/2.73 % (1833358)------------------------------
% 12.35/2.73 % (1833358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.35/2.73 % (1833358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.73 % (1833358)CaDiCaL version: 2.1.3
% 12.35/2.73 % (1833358)Termination reason: Instruction limit
% 12.35/2.73 % (1833358)Termination phase: Saturation
% 12.35/2.73 % (1833358)Time elapsed: 0.066 s
% 12.35/2.73 % (1833358)Peak memory usage: 88 MB
% 12.35/2.73 % (1833358)Instructions burned: 120 (million)
% 12.35/2.73 % (1833359)Instruction limit reached!
% 12.35/2.73 % (1833359)------------------------------
% 12.35/2.73 % (1833359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.35/2.73 % (1833359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.73 % (1833359)CaDiCaL version: 2.1.3
% 12.35/2.73 % (1833359)Termination reason: Instruction limit
% 12.35/2.73 % (1833359)Termination phase: Saturation
% 12.35/2.73 % (1833359)Time elapsed: 0.081 s
% 12.35/2.73 % (1833359)Peak memory usage: 90 MB
% 12.35/2.73 % (1833359)Instructions burned: 140 (million)
% 12.35/2.73 % (1833368)lrs+10_1_sil=8000:sp=occurrence:random_seed=876265915:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 12.35/2.73 % (1833369)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1131780815:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 12.35/2.73 % (1833360)------------------------------
% 12.35/2.73 % (1833360)------------------------------
% 12.35/2.73 % (1833357)------------------------------
% 12.35/2.73 % (1833357)------------------------------
% 12.35/2.73 % (1833369)Instruction limit reached!
% 12.35/2.73 % (1833369)------------------------------
% 12.35/2.73 % (1833369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.35/2.73 % (1833369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.73 % (1833369)CaDiCaL version: 2.1.3
% 16.74/3.23 % (1833369)Termination reason: Instruction limit
% 16.74/3.23 % (1833369)Termination phase: Saturation
% 16.74/3.23 % (1833369)Time elapsed: 0.098 s
% 16.74/3.23 % (1833369)Peak memory usage: 90 MB
% 16.74/3.23 % (1833369)Instructions burned: 158 (million)
% 16.74/3.23 % (1833368)Instruction limit reached!
% 16.74/3.23 % (1833368)------------------------------
% 16.74/3.23 % (1833368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.74/3.23 % (1833368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.74/3.23 % (1833368)CaDiCaL version: 2.1.3
% 16.74/3.23 % (1833368)Termination reason: Instruction limit
% 16.74/3.23 % (1833368)Termination phase: Saturation
% 16.74/3.23 % (1833368)Time elapsed: 0.175 s
% 16.74/3.23 % (1833368)Peak memory usage: 92 MB
% 16.74/3.23 % (1833368)Instructions burned: 286 (million)
% 16.74/3.23 % (1833373)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=3905665110:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 16.74/3.23 % (1833372)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2314318877:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 16.74/3.23 % (1833374)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=972823558:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 16.74/3.23 % (1833374)Refutation not found, incomplete strategy
% 16.74/3.23 % (1833374)------------------------------
% 16.74/3.23 % (1833374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.74/3.23 % (1833374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.74/3.23 % (1833374)CaDiCaL version: 2.1.3
% 16.74/3.23 % (1833374)Termination reason: Refutation not found, incomplete strategy
% 16.74/3.23 % (1833374)Time elapsed: 0.001 s
% 16.74/3.23 % (1833374)Peak memory usage: 88 MB
% 16.74/3.23 % (1833375)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1845712832:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 16.74/3.23 % (1833373)Instruction limit reached!
% 16.74/3.23 % (1833373)------------------------------
% 16.74/3.23 % (1833373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.74/3.23 % (1833373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.74/3.23 % (1833373)CaDiCaL version: 2.1.3
% 16.74/3.23 % (1833373)Termination reason: Instruction limit
% 16.74/3.23 % (1833373)Termination phase: Saturation
% 16.74/3.23 % (1833373)Time elapsed: 0.158 s
% 16.74/3.23 % (1833373)Peak memory usage: 91 MB
% 16.74/3.23 % (1833373)Instructions burned: 249 (million)
% 16.74/3.23 % (1833356)Refutation not found, incomplete strategy
% 16.74/3.23 % (1833356)------------------------------
% 16.74/3.23 % (1833356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.74/3.23 % (1833356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.74/3.23 % (1833356)CaDiCaL version: 2.1.3
% 16.74/3.23 % (1833356)Termination reason: Refutation not found, incomplete strategy
% 16.74/3.23 % (1833356)Time elapsed: 0.591 s
% 16.74/3.23 % (1833356)Peak memory usage: 126 MB
% 16.74/3.23 % (1833356)Instructions burned: 883 (million)
% 16.74/3.23 % (1833372)Instruction limit reached!
% 16.74/3.23 % (1833372)------------------------------
% 16.74/3.23 % (1833372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.74/3.23 % (1833372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.74/3.23 % (1833372)CaDiCaL version: 2.1.3
% 16.74/3.23 % (1833372)Termination reason: Instruction limit
% 16.74/3.23 % (1833372)Termination phase: Saturation
% 16.74/3.23 % (1833372)Time elapsed: 0.199 s
% 16.74/3.23 % (1833372)Peak memory usage: 92 MB
% 16.74/3.23 % (1833372)Instructions burned: 326 (million)
% 16.74/3.23 % (1833374)------------------------------
% 16.74/3.23 % (1833374)------------------------------
% 16.74/3.23 % (1833380)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1708120685:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 16.74/3.23 % (1833380)Refutation not found, incomplete strategy
% 16.74/3.23 % (1833380)------------------------------
% 16.74/3.23 % (1833380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.74/3.23 % (1833380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.74/3.23 % (1833380)CaDiCaL version: 2.1.3
% 16.74/3.23 % (1833380)Termination reason: Refutation not found, incomplete strategy
% 16.74/3.23 % (1833380)Time elapsed: 0.001 s
% 28.60/4.91 % (1833380)Peak memory usage: 88 MB
% 28.60/4.91 % (1833381)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=465035184:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 28.60/4.91 % (1833381)Refutation not found, incomplete strategy
% 28.60/4.91 % (1833381)------------------------------
% 28.60/4.91 % (1833381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.60/4.91 % (1833381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.60/4.91 % (1833381)CaDiCaL version: 2.1.3
% 28.60/4.91 % (1833381)Termination reason: Refutation not found, incomplete strategy
% 28.60/4.91 % (1833381)Time elapsed: 0.001 s
% 28.60/4.91 % (1833381)Peak memory usage: 87 MB
% 28.60/4.91 % (1833356)------------------------------
% 28.60/4.91 % (1833356)------------------------------
% 28.60/4.91 % (1833383)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2122235251:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 28.60/4.91 % (1833383)Refutation not found, incomplete strategy
% 28.60/4.91 % (1833383)------------------------------
% 28.60/4.91 % (1833383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.60/4.91 % (1833383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.60/4.91 % (1833383)CaDiCaL version: 2.1.3
% 28.60/4.91 % (1833383)Termination reason: Refutation not found, incomplete strategy
% 28.60/4.91 % (1833383)Time elapsed: 0.001 s
% 28.60/4.91 % (1833383)Peak memory usage: 88 MB
% 28.60/4.91 % (1833380)------------------------------
% 28.60/4.91 % (1833380)------------------------------
% 28.60/4.91 % (1833385)lrs+10_1_sil=8000:sp=occurrence:random_seed=627680738:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 28.60/4.91 % (1833381)------------------------------
% 28.60/4.91 % (1833381)------------------------------
% 28.60/4.91 % (1833387)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1023163802:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 28.60/4.91 % (1833387)Refutation not found, incomplete strategy
% 28.60/4.91 % (1833387)------------------------------
% 28.60/4.91 % (1833387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.60/4.91 % (1833387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.60/4.91 % (1833387)CaDiCaL version: 2.1.3
% 28.60/4.91 % (1833387)Termination reason: Refutation not found, incomplete strategy
% 28.60/4.91 % (1833387)Time elapsed: 0.001 s
% 28.60/4.91 % (1833387)Peak memory usage: 88 MB
% 28.60/4.91 % (1833383)------------------------------
% 28.60/4.91 % (1833383)------------------------------
% 28.60/4.91 % (1833389)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1215875742:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 28.60/4.91 % (1833391)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1759449493:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 28.60/4.91 % (1833391)Refutation not found, incomplete strategy
% 28.60/4.91 % (1833391)------------------------------
% 28.60/4.91 % (1833391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.60/4.91 % (1833391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.60/4.91 % (1833391)CaDiCaL version: 2.1.3
% 28.60/4.91 % (1833391)Termination reason: Refutation not found, incomplete strategy
% 28.60/4.91 % (1833391)Time elapsed: 0.001 s
% 28.60/4.91 % (1833391)Peak memory usage: 88 MB
% 28.60/4.91 % (1833387)------------------------------
% 28.60/4.91 % (1833387)------------------------------
% 28.60/4.91 % (1833391)------------------------------
% 28.60/4.91 % (1833391)------------------------------
% 28.60/4.91 % (1833394)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2642372947:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 28.60/4.91 % (1833385)Instruction limit reached!
% 28.60/4.91 % (1833385)------------------------------
% 28.60/4.91 % (1833385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.60/4.91 % (1833385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.60/4.91 % (1833385)CaDiCaL version: 2.1.3
% 28.60/4.91 % (1833385)Termination reason: Instruction limit
% 28.60/4.91 % (1833385)Termination phase: Saturation
% 28.60/4.91 % (1833385)Time elapsed: 0.558 s
% 28.60/4.91 % (1833385)Peak memory usage: 99 MB
% 28.60/4.91 % (1833385)Instructions burned: 907 (million)
% 28.60/4.91 % (1833395)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2870365547:st=3:i=13193:sd=3:ss=axioms_2982 on theBenchmark for (2982ds/13193Mi)
% 20.65/5.60 % (1833397)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=199078550:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/125Mi)
% 20.65/5.60 % (1833397)Instruction limit reached!
% 20.65/5.60 % (1833397)------------------------------
% 20.65/5.60 % (1833397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.65/5.60 % (1833397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.65/5.60 % (1833397)CaDiCaL version: 2.1.3
% 20.65/5.60 % (1833397)Termination reason: Instruction limit
% 20.65/5.60 % (1833397)Termination phase: Saturation
% 20.65/5.60 % (1833397)Time elapsed: 0.080 s
% 20.65/5.60 % (1833397)Peak memory usage: 90 MB
% 20.65/5.60 % (1833397)Instructions burned: 125 (million)
% 20.65/5.60 % (1833394)Instruction limit reached!
% 20.65/5.60 % (1833394)------------------------------
% 20.65/5.60 % (1833394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.65/5.60 % (1833394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.65/5.60 % (1833394)CaDiCaL version: 2.1.3
% 20.65/5.60 % (1833394)Termination reason: Instruction limit
% 20.65/5.60 % (1833394)Termination phase: Saturation
% 20.65/5.60 % (1833394)Time elapsed: 0.320 s
% 20.65/5.60 % (1833394)Peak memory usage: 93 MB
% 20.65/5.60 % (1833394)Instructions burned: 594 (million)
% 20.65/5.60 % (1833400)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=130627517:i=134:gtgl=5:slsql=off:gtg=exists_sym_2979 on theBenchmark for (2979ds/134Mi)
% 20.65/5.60 % (1833401)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4257353308:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/141Mi)
% 20.65/5.60 % (1833401)Refutation not found, incomplete strategy
% 20.65/5.60 % (1833401)------------------------------
% 20.65/5.60 % (1833401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.65/5.60 % (1833401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.65/5.60 % (1833401)CaDiCaL version: 2.1.3
% 20.65/5.60 % (1833401)Termination reason: Refutation not found, incomplete strategy
% 20.65/5.60 % (1833401)Time elapsed: 0.001 s
% 20.65/5.60 % (1833401)Peak memory usage: 88 MB
% 20.65/5.60 % (1833375)Instruction limit reached!
% 20.65/5.60 % (1833375)------------------------------
% 20.65/5.60 % (1833375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.65/5.60 % (1833375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.65/5.60 % (1833375)CaDiCaL version: 2.1.3
% 20.65/5.60 % (1833375)Termination reason: Instruction limit
% 20.65/5.60 % (1833375)Termination phase: Saturation
% 20.65/5.60 % (1833375)Time elapsed: 1.464 s
% 20.65/5.60 % (1833375)Peak memory usage: 143 MB
% 20.65/5.60 % (1833375)Instructions burned: 2350 (million)
% 20.65/5.60 % (1833400)Instruction limit reached!
% 20.65/5.60 % (1833400)------------------------------
% 20.65/5.60 % (1833400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.65/5.60 % (1833400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.65/5.60 % (1833400)CaDiCaL version: 2.1.3
% 20.65/5.60 % (1833400)Termination reason: Instruction limit
% 20.65/5.60 % (1833400)Termination phase: Saturation
% 20.65/5.60 % (1833400)Time elapsed: 0.062 s
% 20.65/5.60 % (1833400)Peak memory usage: 90 MB
% 20.65/5.60 % (1833400)Instructions burned: 136 (million)
% 20.65/5.60 % (1833404)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2054024296:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2977 on theBenchmark for (2977ds/431Mi)
% 20.65/5.60 % (1833405)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=96793818:i=6060:aac=none:ins=25_2977 on theBenchmark for (2977ds/6060Mi)
% 20.65/5.60 % (1833404)Refutation not found, incomplete strategy
% 20.65/5.60 % (1833404)------------------------------
% 20.65/5.60 % (1833404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.65/5.60 % (1833404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.65/5.60 % (1833404)CaDiCaL version: 2.1.3
% 20.65/5.60 % (1833404)Termination reason: Refutation not found, incomplete strategy
% 20.65/5.60 % (1833404)Time elapsed: 0.001 s
% 20.65/5.60 % (1833404)Peak memory usage: 88 MB
% 20.65/5.60 % (1833401)------------------------------
% 20.65/5.60 % (1833401)------------------------------
% 20.65/5.60 % (1833404)------------------------------
% 20.65/5.60 % (1833404)------------------------------
% 20.65/5.60 % (1833408)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=3161046207:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2975 on theBenchmark for (2975ds/150Mi)
% 20.65/5.60 % (1833408)Instruction limit reached!
% 20.65/5.60 % (1833408)------------------------------
% 20.65/5.60 % (1833408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.65/5.60 % (1833408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.65/5.60 % (1833408)CaDiCaL version: 2.1.3
% 20.65/5.60 % (1833408)Termination reason: Instruction limit
% 20.65/5.60 % (1833408)Termination phase: Saturation
% 20.65/5.60 % (1833408)Time elapsed: 0.092 s
% 20.65/5.60 % (1833408)Peak memory usage: 91 MB
% 20.65/5.60 % (1833408)Instructions burned: 151 (million)
% 20.65/5.60 % (1833409)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3826787374:i=14155:bd=all_2973 on theBenchmark for (2973ds/14155Mi)
% 20.65/5.60 % (1833411)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1751715561:i=667:av=off:fsr=off_2972 on theBenchmark for (2972ds/667Mi)
% 20.65/5.60 % (1833411)Refutation not found, incomplete strategy
% 20.65/5.60 % (1833411)------------------------------
% 20.65/5.60 % (1833411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.65/5.60 % (1833411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.65/5.60 % (1833411)CaDiCaL version: 2.1.3
% 20.65/5.60 % (1833411)Termination reason: Refutation not found, incomplete strategy
% 20.65/5.60 % (1833411)Time elapsed: 0.001 s
% 20.65/5.60 % (1833411)Peak memory usage: 88 MB
% 20.65/5.60 % (1833411)------------------------------
% 20.65/5.60 % (1833411)------------------------------
% 20.65/5.60 % (1833414)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2214791185:s2a=on:i=185:s2at=1.8:fdi=4_2968 on theBenchmark for (2968ds/185Mi)
% 20.65/5.60 % (1833414)Instruction limit reached!
% 20.65/5.60 % (1833414)------------------------------
% 20.65/5.60 % (1833414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.65/5.60 % (1833414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.65/5.60 % (1833414)CaDiCaL version: 2.1.3
% 20.65/5.60 % (1833414)Termination reason: Instruction limit
% 20.65/5.60 % (1833414)Termination phase: Saturation
% 20.65/5.60 % (1833414)Time elapsed: 0.100 s
% 20.65/5.60 % (1833414)Peak memory usage: 91 MB
% 20.65/5.60 % (1833414)Instructions burned: 185 (million)
% 20.65/5.60 % (1833416)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=706679001:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2966 on theBenchmark for (2966ds/193Mi)
% 20.65/5.60 % (1833416)Instruction limit reached!
% 20.65/5.60 % (1833416)------------------------------
% 20.65/5.60 % (1833416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.65/5.60 % (1833416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.65/5.61 % (1833416)CaDiCaL version: 2.1.3
% 20.65/5.61 % (1833416)Termination reason: Instruction limit
% 20.65/5.61 % (1833416)Termination phase: Saturation
% 20.65/5.61 % (1833416)Time elapsed: 0.107 s
% 20.65/5.61 % (1833416)Peak memory usage: 91 MB
% 20.65/5.61 % (1833416)Instructions burned: 194 (million)
% 20.65/5.61 % (1833418)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=398546713:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2963 on theBenchmark for (2963ds/4850Mi)
% 20.65/5.61 % (1833418)Refutation not found, incomplete strategy
% 20.65/5.61 % (1833418)------------------------------
% 20.65/5.61 % (1833418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.65/5.61 % (1833418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.65/5.61 % (1833418)CaDiCaL version: 2.1.3
% 20.65/5.61 % (1833418)Termination reason: Refutation not found, incomplete strategy
% 20.65/5.61 % (1833418)Time elapsed: 0.001 s
% 20.65/5.61 % (1833418)Peak memory usage: 87 MB
% 20.65/5.61 % (1833418)------------------------------
% 20.65/5.61 % (1833418)------------------------------
% 20.65/5.61 % (1833420)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1507474695:i=12111:sd=1:ss=included_2959 on theBenchmark for (2959ds/12111Mi)
% 20.65/5.61 % (1833354)First to succeed.
% 20.65/5.61 % (1833354)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1833349"
% 20.65/5.61 % (1833389)Instruction limit reached!
% 20.65/5.61 % (1833389)------------------------------
% 20.65/5.61 % (1833389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.65/5.61 % (1833389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.65/5.61 % (1833389)CaDiCaL version: 2.1.3
% 20.65/5.61 % (1833389)Termination reason: Instruction limit
% 20.65/5.61 % (1833389)Termination phase: Saturation
% 20.65/5.61 % (1833389)Time elapsed: 3.182 s
% 20.65/5.61 % (1833389)Peak memory usage: 168 MB
% 20.65/5.61 % (1833389)Instructions burned: 5203 (million)
% 20.65/5.61 % (1833354)Refutation found. Thanks to Tanya!
% 20.65/5.61 % SZS status Theorem for theBenchmark
% 20.65/5.61 % SZS output start Proof for theBenchmark
% See solution above
% 34.24/5.80 % (1833354)------------------------------
% 34.24/5.80 % (1833354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.24/5.80 % (1833354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.24/5.80 % (1833354)CaDiCaL version: 2.1.3
% 34.24/5.80 % (1833354)Termination reason: Refutation
% 34.24/5.80 % (1833354)Time elapsed: 4.297 s
% 34.24/5.80 % (1833354)Peak memory usage: 187 MB
% 34.24/5.80 % (1833354)Instructions burned: 6873 (million)
% 34.24/5.80 % (1833354)------------------------------
% 34.24/5.80 % (1833354)------------------------------
% 34.24/5.80 % (1833349)Success in time 4.743 s
% 34.24/5.80 % Vampire exiting
%------------------------------------------------------------------------------