%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP654+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n012.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 180.38s 39.04s
% Output : Refutation 267.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 6
% Syntax : Number of formulae : 109 ( 101 unt; 0 def)
% Number of atoms : 117 ( 116 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 25 ( 17 ~; 6 |; 2 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 0 con; 1-2 aty)
% Number of variables : 240 ( 237 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : mult(X1,ld(X1,X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f01) ).
fof(f2,axiom,
! [X0,X1] : ld(X1,mult(X1,X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f02) ).
fof(f3,axiom,
! [X0,X1] : mult(rd(X1,X0),X0) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f03) ).
fof(f4,axiom,
! [X0,X1] : rd(mult(X1,X0),X0) = X1,
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',f05) ).
fof(f6,conjecture,
? [X0] :
! [X1] :
( mult(X1,X0) = X1
& mult(X0,X1) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f7,negated_conjecture,
~ ? [X0] :
! [X1] :
( mult(X1,X0) = X1
& mult(X0,X1) = X1 ),
inference(negated_conjecture,[status(cth)],[f6]) ).
fof(f8,plain,
! [X0] :
? [X1] :
( mult(X1,X0) != X1
| mult(X0,X1) != X1 ),
inference(ennf_transformation,[],[f7]) ).
fof(f9,plain,
! [X0] :
( sK0(X0) != mult(sK0(X0),X0)
| sK0(X0) != mult(X0,sK0(X0)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X1,sK0(X0))],[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,
! [X0] :
( sK0(X0) != mult(sK0(X0),X0)
| sK0(X0) != mult(X0,sK0(X0)) ),
inference(cnf_transformation,[],[f9]) ).
fof(f16,plain,
! [X2,X0,X1] : mult(X1,mult(ld(X1,X0),mult(X1,X2))) = mult(mult(X0,X1),X2),
inference(superposition,[],[f14,f10]) ).
fof(f46,plain,
! [X0,X1] : rd(X0,ld(X1,X0)) = X1,
inference(superposition,[],[f13,f10]) ).
fof(f47,plain,
! [X0,X1] : ld(rd(X1,X0),X1) = X0,
inference(superposition,[],[f11,f12]) ).
fof(f78,plain,
! [X2,X0,X1] : mult(X1,X2) = mult(X0,mult(ld(X0,rd(X1,X0)),mult(X0,X2))),
inference(superposition,[],[f16,f12]) ).
fof(f81,plain,
! [X2,X0,X1] : mult(X1,X2) = rd(mult(X2,mult(ld(X2,X1),mult(X2,X0))),X0),
inference(superposition,[],[f13,f16]) ).
fof(f107,plain,
! [X2,X0,X1] : mult(X2,X1) = rd(mult(X1,mult(ld(X1,X2),X0)),ld(X1,X0)),
inference(superposition,[],[f81,f10]) ).
fof(f151,plain,
! [X2,X0,X1] : mult(X2,X1) = rd(mult(X1,X0),ld(X1,ld(ld(X1,X2),X0))),
inference(superposition,[],[f107,f10]) ).
fof(f164,plain,
! [X2,X0,X1] : mult(X2,ld(X1,X0)) = mult(X1,mult(ld(X1,rd(X2,X1)),X0)),
inference(superposition,[],[f78,f10]) ).
fof(f186,plain,
! [X2,X0,X1] : mult(X1,X0) = mult(X2,ld(X1,ld(ld(X1,rd(X2,X1)),X0))),
inference(superposition,[],[f164,f10]) ).
fof(f209,plain,
! [X2,X0,X1] : mult(X2,X1) = rd(X0,ld(X1,ld(ld(X1,X2),ld(X1,X0)))),
inference(superposition,[],[f151,f10]) ).
fof(f210,plain,
! [X2,X0,X1] : mult(X2,rd(X1,X0)) = rd(X1,ld(rd(X1,X0),ld(ld(rd(X1,X0),X2),X0))),
inference(superposition,[],[f151,f12]) ).
fof(f235,plain,
! [X2,X0,X1] : ld(X2,ld(ld(X2,X0),ld(X2,X1))) = ld(mult(X0,X2),X1),
inference(superposition,[],[f47,f209]) ).
fof(f422,plain,
! [X2,X0,X1] : ld(X0,X2) = ld(ld(X1,X0),ld(ld(ld(X1,X0),X1),ld(ld(X1,X0),X2))),
inference(superposition,[],[f235,f10]) ).
fof(f450,plain,
! [X2,X0,X1] : mult(ld(X1,X0),X2) = mult(X0,ld(ld(X1,X0),ld(ld(ld(X1,X0),X1),X2))),
inference(superposition,[],[f186,f46]) ).
fof(f461,plain,
! [X0,X1] : mult(X0,X1) = ld(ld(X0,rd(X0,X0)),X1),
inference(superposition,[],[f10,f186]) ).
fof(f465,plain,
! [X2,X0,X1] : ld(X0,mult(X2,X1)) = ld(X2,ld(ld(X2,rd(X0,X2)),X1)),
inference(superposition,[],[f11,f186]) ).
fof(f691,plain,
! [X0,X1] : ld(ld(X0,rd(X0,X0)),ld(X0,X1)) = X1,
inference(superposition,[],[f10,f461]) ).
fof(f694,plain,
! [X2,X0,X1] : ld(X1,ld(ld(X1,X0),ld(X1,X2))) = ld(ld(ld(X0,rd(X0,X0)),X1),X2),
inference(superposition,[],[f235,f461]) ).
fof(f696,plain,
! [X0,X1] : ld(X0,ld(ld(X0,rd(X0,X0)),X1)) = X1,
inference(superposition,[],[f11,f461]) ).
fof(f698,plain,
! [X0,X1] : ld(X0,rd(X0,X0)) = rd(X1,mult(X0,X1)),
inference(superposition,[],[f46,f461]) ).
fof(f783,plain,
! [X2,X0,X1] : ld(X0,ld(rd(X1,mult(X0,X1)),X2)) = X2,
inference(superposition,[],[f696,f698]) ).
fof(f784,plain,
! [X2,X0,X1] : ld(rd(X1,mult(X0,X1)),ld(X0,X2)) = X2,
inference(superposition,[],[f691,f698]) ).
fof(f785,plain,
! [X2,X0,X1] : mult(X0,X2) = ld(rd(X1,mult(X0,X1)),X2),
inference(superposition,[],[f461,f698]) ).
fof(f788,plain,
! [X0,X1] : rd(X0,X0) = mult(X0,rd(X1,mult(X0,X1))),
inference(superposition,[],[f10,f698]) ).
fof(f817,plain,
! [X2,X0,X1] : mult(rd(X1,X0),X2) = ld(rd(X0,X1),X2),
inference(superposition,[],[f785,f12]) ).
fof(f825,plain,
! [X2,X3,X0,X1] : ld(X0,ld(ld(X0,X1),ld(X0,X3))) = ld(ld(rd(X2,mult(X1,X2)),X0),X3),
inference(superposition,[],[f235,f785]) ).
fof(f967,plain,
! [X2,X0,X1] : ld(rd(X2,X1),ld(rd(X1,X2),X0)) = X0,
inference(superposition,[],[f11,f817]) ).
fof(f1014,plain,
! [X0,X1] : ld(mult(X0,rd(X1,mult(X0,X1))),X0) = X0,
inference(superposition,[],[f47,f788]) ).
fof(f1032,plain,
! [X0,X1] : ld(rd(X1,mult(X0,X1)),ld(ld(rd(X1,mult(X0,X1)),X0),ld(rd(X1,mult(X0,X1)),X0))) = X0,
inference(forward_demodulation,[],[f1014,f235]) ).
fof(f1051,plain,
! [X0,X1] : ld(rd(X1,mult(X0,X1)),ld(X0,ld(ld(X0,X0),ld(X0,ld(rd(X1,mult(X0,X1)),X0))))) = X0,
inference(forward_demodulation,[],[f1032,f825]) ).
fof(f1064,plain,
! [X0,X1] : ld(ld(X0,X0),ld(X0,ld(rd(X1,mult(X0,X1)),X0))) = X0,
inference(forward_demodulation,[],[f1051,f784]) ).
fof(f1071,plain,
! [X0] : ld(ld(X0,X0),X0) = X0,
inference(forward_demodulation,[],[f1064,f783]) ).
fof(f1099,plain,
! [X0] : ld(X0,X0) = rd(X0,X0),
inference(superposition,[],[f46,f1071]) ).
fof(f1102,plain,
! [X0,X1] : mult(X0,X1) = ld(ld(X0,ld(X0,X0)),X1),
inference(backward_demodulation,[],[f461,f1099]) ).
fof(f1103,plain,
! [X0,X1] : ld(ld(X0,ld(X0,X0)),ld(X0,X1)) = X1,
inference(backward_demodulation,[],[f691,f1099]) ).
fof(f1106,plain,
! [X2,X0,X1] : ld(X1,ld(ld(X1,X0),ld(X1,X2))) = ld(ld(ld(X0,ld(X0,X0)),X1),X2),
inference(backward_demodulation,[],[f694,f1099]) ).
fof(f1107,plain,
! [X0,X1] : ld(X0,ld(ld(X0,ld(X0,X0)),X1)) = X1,
inference(backward_demodulation,[],[f696,f1099]) ).
fof(f1208,plain,
! [X2,X0,X1] : ld(X2,ld(ld(X2,rd(X0,X2)),X1)) = ld(X0,ld(ld(X2,ld(X2,X2)),X1)),
inference(backward_demodulation,[],[f465,f1102]) ).
fof(f1226,plain,
! [X2,X0,X1] : mult(ld(X1,X0),X2) = ld(ld(X0,ld(X0,X0)),ld(ld(X1,X0),ld(ld(ld(X1,X0),X1),X2))),
inference(backward_demodulation,[],[f450,f1102]) ).
fof(f1231,plain,
! [X2,X0,X1] : rd(X1,ld(rd(X1,X0),ld(ld(rd(X1,X0),X2),X0))) = ld(ld(X2,ld(X2,X2)),rd(X1,X0)),
inference(backward_demodulation,[],[f210,f1102]) ).
fof(f1232,plain,
! [X0] :
( sK0(X0) != ld(ld(X0,ld(X0,X0)),sK0(X0))
| sK0(X0) != mult(sK0(X0),X0) ),
inference(backward_demodulation,[],[f15,f1102]) ).
fof(f1233,plain,
! [X0,X1] : ld(ld(rd(X1,X0),ld(rd(X1,X0),rd(X1,X0))),X0) = X1,
inference(backward_demodulation,[],[f12,f1102]) ).
fof(f1285,plain,
! [X0] :
( sK0(X0) != ld(ld(sK0(X0),ld(sK0(X0),sK0(X0))),X0)
| sK0(X0) != ld(ld(X0,ld(X0,X0)),sK0(X0)) ),
inference(forward_demodulation,[],[f1232,f1102]) ).
fof(f1290,plain,
! [X2,X0,X1] : ld(ld(X0,ld(X0,X0)),ld(ld(X1,X0),ld(ld(ld(X1,X0),X1),X2))) = ld(ld(ld(X1,X0),ld(ld(X1,X0),ld(X1,X0))),X2),
inference(forward_demodulation,[],[f1226,f1102]) ).
fof(f1589,plain,
! [X0,X1] : ld(ld(X0,X0),ld(ld(X0,X0),X1)) = X1,
inference(superposition,[],[f967,f1099]) ).
fof(f1649,plain,
! [X0,X1] : ld(X0,X1) = ld(ld(X0,X0),ld(X0,ld(ld(X0,X0),X1))),
inference(superposition,[],[f422,f1071]) ).
fof(f1654,plain,
! [X2,X0,X1] : ld(ld(ld(X0,X0),X1),X2) = ld(X1,ld(ld(X1,ld(X0,X0)),ld(X1,X2))),
inference(superposition,[],[f422,f1589]) ).
fof(f1690,plain,
! [X0,X1] : ld(ld(X0,X0),ld(X0,X1)) = ld(X0,ld(ld(X0,X0),X1)),
inference(superposition,[],[f1589,f1649]) ).
fof(f1884,plain,
! [X2,X0,X1] : ld(ld(X0,rd(X1,X0)),X2) = ld(ld(X0,ld(X0,X0)),ld(X1,ld(ld(X0,ld(X0,X0)),X2))),
inference(superposition,[],[f1103,f1208]) ).
fof(f2159,plain,
! [X0,X1] : ld(ld(X0,X0),ld(ld(X0,ld(X0,X0)),X1)) = ld(ld(X0,ld(X0,X0)),ld(ld(X0,X0),X1)),
inference(superposition,[],[f1690,f1103]) ).
fof(f2244,plain,
! [X0,X1] : ld(ld(X0,ld(X0,X0)),ld(X1,X1)) = rd(X1,ld(ld(X1,X1),ld(ld(ld(X1,X1),X0),X1))),
inference(superposition,[],[f1231,f1099]) ).
fof(f2259,plain,
! [X2,X0,X1] : ld(ld(ld(ld(X0,ld(X0,X0)),rd(X2,X1)),ld(ld(ld(X0,ld(X0,X0)),rd(X2,X1)),ld(ld(X0,ld(X0,X0)),rd(X2,X1)))),ld(rd(X2,X1),ld(ld(rd(X2,X1),X0),X1))) = X2,
inference(superposition,[],[f1233,f1231]) ).
fof(f2272,plain,
! [X2,X0,X1] : ld(ld(rd(X2,X1),ld(rd(X2,X1),rd(X2,X1))),ld(ld(ld(X0,ld(X0,X0)),rd(X2,X1)),ld(ld(ld(ld(X0,ld(X0,X0)),rd(X2,X1)),ld(X0,ld(X0,X0))),ld(rd(X2,X1),ld(ld(rd(X2,X1),X0),X1))))) = X2,
inference(forward_demodulation,[],[f2259,f1290]) ).
fof(f2534,plain,
! [X0,X1] : ld(ld(rd(X1,X0),ld(rd(X1,X0),rd(X1,X0))),ld(ld(ld(X1,ld(X1,X1)),rd(X1,X0)),ld(ld(ld(ld(X1,ld(X1,X1)),rd(X1,X0)),ld(X1,ld(X1,X1))),ld(rd(X1,X0),ld(X0,X0))))) = X1,
inference(superposition,[],[f2272,f47]) ).
fof(f2597,plain,
! [X2,X0,X1] : ld(rd(X1,X0),ld(X0,ld(rd(X1,X0),X2))) = ld(ld(ld(X1,ld(X1,X1)),rd(X1,X0)),X2),
inference(superposition,[],[f1106,f47]) ).
fof(f2629,plain,
! [X2,X0,X1] : ld(ld(X2,X1),ld(X2,X0)) = ld(ld(X2,ld(X2,X2)),ld(ld(ld(X1,ld(X1,X1)),X2),X0)),
inference(superposition,[],[f1103,f1106]) ).
fof(f2668,plain,
! [X0,X1] : ld(ld(rd(X1,X0),ld(rd(X1,X0),rd(X1,X0))),ld(ld(ld(X1,ld(X1,X1)),rd(X1,X0)),ld(ld(rd(X1,X0),ld(X0,ld(rd(X1,X0),ld(X1,ld(X1,X1))))),ld(rd(X1,X0),ld(X0,X0))))) = X1,
inference(backward_demodulation,[],[f2534,f2597]) ).
fof(f2683,plain,
! [X0,X1] : ld(ld(rd(X1,X0),X1),ld(rd(X1,X0),ld(ld(rd(X1,X0),ld(X0,ld(rd(X1,X0),ld(X1,ld(X1,X1))))),ld(rd(X1,X0),ld(X0,X0))))) = X1,
inference(forward_demodulation,[],[f2668,f2629]) ).
fof(f2690,plain,
! [X0,X1] : ld(X0,ld(rd(X1,X0),ld(ld(rd(X1,X0),ld(X0,ld(rd(X1,X0),ld(X1,ld(X1,X1))))),ld(rd(X1,X0),ld(X0,X0))))) = X1,
inference(forward_demodulation,[],[f2683,f47]) ).
fof(f2695,plain,
! [X0,X1] : ld(X0,X0) = ld(X1,ld(rd(ld(X0,X0),X1),ld(ld(rd(ld(X0,X0),X1),ld(X1,ld(rd(ld(X0,X0),X1),ld(ld(X0,X0),ld(X0,ld(ld(X0,X0),X0)))))),ld(rd(ld(X0,X0),X1),ld(X1,X1))))),
inference(superposition,[],[f2690,f1690]) ).
fof(f2733,plain,
! [X0,X1] : ld(X0,X0) = ld(X1,ld(rd(ld(X0,X0),X1),ld(ld(rd(ld(X0,X0),X1),ld(X1,ld(rd(ld(X0,X0),X1),ld(X0,ld(ld(X0,X0),ld(ld(X0,X0),X0)))))),ld(rd(ld(X0,X0),X1),ld(X1,X1))))),
inference(forward_demodulation,[],[f2695,f1690]) ).
fof(f2740,plain,
! [X0,X1] : ld(X0,X0) = ld(X1,ld(rd(ld(X0,X0),X1),ld(ld(rd(ld(X0,X0),X1),ld(X1,ld(rd(ld(X0,X0),X1),ld(X0,X0)))),ld(rd(ld(X0,X0),X1),ld(X1,X1))))),
inference(forward_demodulation,[],[f2733,f1589]) ).
fof(f2746,plain,
! [X0,X1] : ld(X0,X0) = ld(X1,ld(rd(ld(X0,X0),X1),ld(ld(rd(ld(X0,X0),X1),ld(X1,X1)),ld(rd(ld(X0,X0),X1),ld(X1,X1))))),
inference(forward_demodulation,[],[f2740,f47]) ).
fof(f2749,plain,
! [X0,X1] : ld(X0,X0) = ld(X1,ld(ld(ld(ld(X1,X1),ld(ld(X1,X1),ld(X1,X1))),rd(ld(X0,X0),X1)),ld(X1,X1))),
inference(forward_demodulation,[],[f2746,f1106]) ).
fof(f2750,plain,
! [X0,X1] : ld(X0,X0) = ld(X1,ld(ld(ld(X1,ld(X1,X1)),ld(ld(X1,X1),ld(ld(ld(X1,X1),X1),rd(ld(X0,X0),X1)))),ld(X1,X1))),
inference(forward_demodulation,[],[f2749,f1290]) ).
fof(f2751,plain,
! [X0,X1] : ld(X0,X0) = ld(X1,ld(ld(ld(X1,X1),ld(ld(X1,ld(X1,X1)),ld(ld(ld(X1,X1),X1),rd(ld(X0,X0),X1)))),ld(X1,X1))),
inference(forward_demodulation,[],[f2750,f2159]) ).
fof(f2752,plain,
! [X0,X1] : ld(X0,X0) = ld(X1,ld(ld(ld(X1,X1),ld(ld(X1,ld(X1,X1)),ld(X1,ld(ld(X1,ld(X1,X1)),ld(X1,rd(ld(X0,X0),X1)))))),ld(X1,X1))),
inference(forward_demodulation,[],[f2751,f1654]) ).
fof(f2753,plain,
! [X0,X1] : ld(X0,X0) = ld(X1,ld(ld(ld(X1,X1),ld(ld(X1,ld(X1,X1)),ld(X1,rd(ld(X0,X0),X1)))),ld(X1,X1))),
inference(forward_demodulation,[],[f2752,f1103]) ).
fof(f2754,plain,
! [X0,X1] : ld(X0,X0) = ld(X1,ld(ld(ld(X1,X1),rd(ld(X0,X0),X1)),ld(X1,X1))),
inference(forward_demodulation,[],[f2753,f1103]) ).
fof(f2826,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X0,X0),ld(ld(ld(X0,ld(ld(X0,X0),X0)),rd(ld(X1,X1),ld(X0,X0))),ld(X0,ld(ld(X0,X0),X0)))),
inference(superposition,[],[f2754,f1690]) ).
fof(f2846,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X0,X0),ld(ld(ld(X0,X0),rd(ld(X1,X1),ld(X0,X0))),ld(X0,X0))),
inference(forward_demodulation,[],[f2826,f1071]) ).
fof(f2857,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X0,X0),ld(ld(ld(X0,X0),ld(ld(X0,X0),ld(X0,X0))),ld(ld(X1,X1),ld(ld(ld(X0,X0),ld(ld(X0,X0),ld(X0,X0))),ld(X0,X0))))),
inference(forward_demodulation,[],[f2846,f1884]) ).
fof(f2863,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X1,X1),ld(ld(ld(X0,X0),ld(ld(X0,X0),ld(X0,X0))),ld(X0,X0))),
inference(forward_demodulation,[],[f2857,f1107]) ).
fof(f2865,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X1,X1),ld(ld(X0,ld(X0,X0)),ld(ld(X0,X0),ld(ld(ld(X0,X0),X0),ld(X0,X0))))),
inference(forward_demodulation,[],[f2863,f1290]) ).
fof(f2866,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X1,X1),ld(ld(X0,X0),ld(ld(X0,ld(X0,X0)),ld(ld(ld(X0,X0),X0),ld(X0,X0))))),
inference(forward_demodulation,[],[f2865,f2159]) ).
fof(f2867,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X1,X1),ld(ld(X0,X0),ld(ld(X0,ld(X0,X0)),ld(X0,ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))))))),
inference(forward_demodulation,[],[f2866,f1654]) ).
fof(f2868,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X1,X1),ld(ld(X0,X0),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))))),
inference(forward_demodulation,[],[f2867,f1103]) ).
fof(f2869,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X1,X1),ld(ld(X0,X0),ld(X0,X0))),
inference(forward_demodulation,[],[f2868,f1103]) ).
fof(f2870,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X1,X1),ld(X0,ld(ld(X0,X0),X0))),
inference(forward_demodulation,[],[f2869,f1690]) ).
fof(f2871,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X1,X1),ld(X0,X0)),
inference(forward_demodulation,[],[f2870,f1071]) ).
fof(f2890,plain,
! [X0,X1] : ld(X0,X0) = ld(ld(X1,X1),ld(X1,X1)),
inference(superposition,[],[f1589,f2871]) ).
fof(f2896,plain,
! [X0,X1] : ld(X0,X0) = ld(X1,ld(ld(X1,X1),X1)),
inference(forward_demodulation,[],[f2890,f1690]) ).
fof(f2899,plain,
! [X0,X1] : ld(X1,X1) = ld(X0,X0),
inference(forward_demodulation,[],[f2896,f1071]) ).
fof(f2940,plain,
! [X0,X1] : ld(ld(X1,X1),X0) = X0,
inference(superposition,[],[f1071,f2899]) ).
fof(f2941,plain,
! [X2,X0,X1] : ld(ld(X0,ld(X2,X2)),ld(X0,X1)) = X1,
inference(superposition,[],[f1103,f2899]) ).
fof(f2999,plain,
! [X0,X1] : ld(ld(X0,ld(X0,X0)),ld(X1,X1)) = rd(X1,ld(ld(X1,X1),ld(X0,X1))),
inference(backward_demodulation,[],[f2244,f2940]) ).
fof(f3076,plain,
! [X0,X1] : rd(X1,ld(X0,X1)) = ld(ld(X0,ld(X0,X0)),ld(X1,X1)),
inference(forward_demodulation,[],[f2999,f2940]) ).
fof(f3109,plain,
! [X0,X1] : ld(ld(X0,ld(X0,X0)),ld(X1,X1)) = X0,
inference(forward_demodulation,[],[f3076,f46]) ).
fof(f3345,plain,
! [X0] :
( sK0(ld(X0,X0)) != sK0(ld(X0,X0))
| sK0(ld(X0,X0)) != ld(ld(ld(X0,X0),ld(ld(X0,X0),ld(X0,X0))),sK0(ld(X0,X0))) ),
inference(superposition,[],[f1285,f3109]) ).
fof(f3349,plain,
! [X0] : sK0(ld(X0,X0)) != ld(ld(ld(X0,X0),ld(ld(X0,X0),ld(X0,X0))),sK0(ld(X0,X0))),
inference(trivial_inequality_removal,[],[f3345]) ).
fof(f3352,plain,
! [X0] : sK0(ld(X0,X0)) != ld(ld(X0,ld(X0,X0)),ld(ld(X0,X0),ld(ld(ld(X0,X0),X0),sK0(ld(X0,X0))))),
inference(forward_demodulation,[],[f3349,f1290]) ).
fof(f3360,plain,
! [X0] : sK0(ld(X0,X0)) != ld(ld(X0,ld(X0,X0)),ld(ld(ld(X0,X0),X0),sK0(ld(X0,X0)))),
inference(forward_demodulation,[],[f3352,f2940]) ).
fof(f3361,plain,
! [X0] : sK0(ld(X0,X0)) != ld(ld(X0,ld(X0,X0)),ld(X0,sK0(ld(X0,X0)))),
inference(forward_demodulation,[],[f3360,f2940]) ).
fof(f3362,plain,
$false,
inference(forward_subsumption_resolution,[],[f3361,f2941]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP654+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.36 % Computer : n012.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 10:31:05 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 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
% 10.54/2.30 % (2175108)Detected formulas, will run a generic FOF schedule.
% 10.54/2.30 % (2175115)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=893638825:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.54/2.30 % (2175116)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=240243866:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.54/2.30 % (2175114)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=2432756947:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.54/2.30 % (2175118)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1888322515:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.54/2.30 % (2175117)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1902664697:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.54/2.30 % (2175117)Refutation not found, incomplete strategy
% 10.54/2.30 % (2175117)------------------------------
% 10.54/2.30 % (2175117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.54/2.30 % (2175117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.54/2.30 % (2175117)CaDiCaL version: 2.1.3
% 10.54/2.30 % (2175117)Termination reason: Refutation not found, incomplete strategy
% 10.54/2.30 % (2175117)Time elapsed: 0.001 s
% 10.54/2.30 % (2175117)Peak memory usage: 88 MB
% 10.54/2.30 % (2175120)dis-21_1_sil=8000:lcm=predicate:random_seed=195300024: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)
% 10.54/2.30 % (2175119)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=844205544:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.54/2.30 % (2175120)Refutation not found, incomplete strategy
% 10.54/2.30 % (2175120)------------------------------
% 10.54/2.30 % (2175120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.54/2.30 % (2175120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.54/2.30 % (2175120)CaDiCaL version: 2.1.3
% 10.54/2.30 % (2175120)Termination reason: Refutation not found, incomplete strategy
% 10.54/2.30 % (2175120)Time elapsed: 0.001 s
% 10.54/2.30 % (2175120)Peak memory usage: 88 MB
% 10.54/2.30 % (2175118)Instruction limit reached!
% 10.54/2.30 % (2175118)------------------------------
% 10.54/2.30 % (2175118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.54/2.30 % (2175118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.54/2.30 % (2175118)CaDiCaL version: 2.1.3
% 10.54/2.30 % (2175118)Termination reason: Instruction limit
% 10.54/2.30 % (2175118)Termination phase: Saturation
% 10.54/2.30 % (2175118)Time elapsed: 0.050 s
% 10.54/2.30 % (2175118)Peak memory usage: 88 MB
% 10.54/2.30 % (2175118)Instructions burned: 119 (million)
% 10.54/2.30 % (2175119)Instruction limit reached!
% 10.54/2.30 % (2175119)------------------------------
% 10.54/2.30 % (2175119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.54/2.30 % (2175119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.54/2.30 % (2175119)CaDiCaL version: 2.1.3
% 10.54/2.30 % (2175119)Termination reason: Instruction limit
% 10.54/2.30 % (2175119)Termination phase: Saturation
% 10.54/2.30 % (2175119)Time elapsed: 0.088 s
% 10.54/2.30 % (2175119)Peak memory usage: 89 MB
% 10.54/2.30 % (2175119)Instructions burned: 140 (million)
% 10.54/2.30 % (2175128)lrs+10_1_sil=8000:sp=occurrence:random_seed=4073408587:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 10.54/2.30 % (2175117)------------------------------
% 10.54/2.30 % (2175117)------------------------------
% 10.54/2.30 % (2175120)------------------------------
% 10.54/2.30 % (2175120)------------------------------
% 10.54/2.30 % (2175129)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4093296360:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 10.54/2.30 % (2175129)Instruction limit reached!
% 10.54/2.30 % (2175129)------------------------------
% 10.54/2.30 % (2175129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.54/2.30 % (2175129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.54/2.30 % (2175129)CaDiCaL version: 2.1.3
% 12.52/2.67 % (2175129)Termination reason: Instruction limit
% 12.52/2.67 % (2175129)Termination phase: Saturation
% 12.52/2.67 % (2175129)Time elapsed: 0.085 s
% 12.52/2.67 % (2175129)Peak memory usage: 90 MB
% 12.52/2.67 % (2175129)Instructions burned: 160 (million)
% 12.52/2.67 % (2175128)Instruction limit reached!
% 12.52/2.67 % (2175128)------------------------------
% 12.52/2.67 % (2175128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.67 % (2175128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.67 % (2175128)CaDiCaL version: 2.1.3
% 12.52/2.67 % (2175128)Termination reason: Instruction limit
% 12.52/2.67 % (2175128)Termination phase: Saturation
% 12.52/2.67 % (2175128)Time elapsed: 0.152 s
% 12.52/2.67 % (2175128)Peak memory usage: 92 MB
% 12.52/2.67 % (2175128)Instructions burned: 285 (million)
% 12.52/2.67 % (2175131)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1154013913:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 12.52/2.67 % (2175132)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=254770745:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 12.52/2.67 % (2175116)Refutation not found, incomplete strategy
% 12.52/2.67 % (2175116)------------------------------
% 12.52/2.67 % (2175116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.67 % (2175116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.67 % (2175116)CaDiCaL version: 2.1.3
% 12.52/2.67 % (2175116)Termination reason: Refutation not found, incomplete strategy
% 12.52/2.67 % (2175116)Time elapsed: 0.525 s
% 12.52/2.67 % (2175116)Peak memory usage: 125 MB
% 12.52/2.67 % (2175116)Instructions burned: 884 (million)
% 12.52/2.67 % (2175134)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3520213874:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 12.52/2.67 % (2175134)Refutation not found, incomplete strategy
% 12.52/2.67 % (2175134)------------------------------
% 12.52/2.67 % (2175134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.67 % (2175134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.67 % (2175134)CaDiCaL version: 2.1.3
% 12.52/2.67 % (2175134)Termination reason: Refutation not found, incomplete strategy
% 12.52/2.67 % (2175134)Time elapsed: 0.001 s
% 12.52/2.67 % (2175134)Peak memory usage: 88 MB
% 12.52/2.67 % (2175135)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1053980799:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 12.52/2.67 % (2175132)Instruction limit reached!
% 12.52/2.67 % (2175132)------------------------------
% 12.52/2.67 % (2175132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.67 % (2175132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.67 % (2175132)CaDiCaL version: 2.1.3
% 12.52/2.67 % (2175132)Termination reason: Instruction limit
% 12.52/2.67 % (2175132)Termination phase: Saturation
% 12.52/2.67 % (2175132)Time elapsed: 0.130 s
% 12.52/2.67 % (2175132)Peak memory usage: 92 MB
% 12.52/2.67 % (2175132)Instructions burned: 249 (million)
% 12.52/2.67 % (2175131)Instruction limit reached!
% 12.52/2.67 % (2175131)------------------------------
% 12.52/2.67 % (2175131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.67 % (2175131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.67 % (2175131)CaDiCaL version: 2.1.3
% 12.52/2.67 % (2175131)Termination reason: Instruction limit
% 12.52/2.67 % (2175131)Termination phase: Saturation
% 12.52/2.67 % (2175131)Time elapsed: 0.171 s
% 12.52/2.67 % (2175131)Peak memory usage: 92 MB
% 12.52/2.67 % (2175131)Instructions burned: 325 (million)
% 12.52/2.67 % (2175140)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=540182665:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 12.52/2.67 % (2175140)Refutation not found, incomplete strategy
% 12.52/2.67 % (2175140)------------------------------
% 12.52/2.67 % (2175140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.67 % (2175140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.67 % (2175140)CaDiCaL version: 2.1.3
% 12.52/2.67 % (2175140)Termination reason: Refutation not found, incomplete strategy
% 12.52/2.67 % (2175140)Time elapsed: 0.001 s
% 12.52/2.67 % (2175140)Peak memory usage: 88 MB
% 12.52/2.67 % (2175141)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=913349881:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 19.91/3.63 % (2175141)Refutation not found, incomplete strategy
% 19.91/3.63 % (2175141)------------------------------
% 19.91/3.63 % (2175141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/3.63 % (2175141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/3.63 % (2175141)CaDiCaL version: 2.1.3
% 19.91/3.63 % (2175141)Termination reason: Refutation not found, incomplete strategy
% 19.91/3.63 % (2175141)Time elapsed: 0.001 s
% 19.91/3.63 % (2175141)Peak memory usage: 87 MB
% 19.91/3.63 % (2175134)------------------------------
% 19.91/3.63 % (2175134)------------------------------
% 19.91/3.63 % (2175116)------------------------------
% 19.91/3.63 % (2175116)------------------------------
% 19.91/3.63 % (2175153)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1540509955:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 19.91/3.63 % (2175153)Refutation not found, incomplete strategy
% 19.91/3.63 % (2175153)------------------------------
% 19.91/3.63 % (2175153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/3.63 % (2175153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/3.63 % (2175153)CaDiCaL version: 2.1.3
% 19.91/3.63 % (2175153)Termination reason: Refutation not found, incomplete strategy
% 19.91/3.63 % (2175153)Time elapsed: 0.001 s
% 19.91/3.63 % (2175153)Peak memory usage: 88 MB
% 19.91/3.63 % (2175154)lrs+10_1_sil=8000:sp=occurrence:random_seed=3382135845:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 19.91/3.63 % (2175140)------------------------------
% 19.91/3.63 % (2175140)------------------------------
% 19.91/3.63 % (2175141)------------------------------
% 19.91/3.63 % (2175141)------------------------------
% 19.91/3.63 % (2175157)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2331410575:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 19.91/3.63 % (2175157)Refutation not found, incomplete strategy
% 19.91/3.63 % (2175157)------------------------------
% 19.91/3.63 % (2175157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/3.63 % (2175157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/3.63 % (2175157)CaDiCaL version: 2.1.3
% 19.91/3.63 % (2175157)Termination reason: Refutation not found, incomplete strategy
% 19.91/3.63 % (2175157)Time elapsed: 0.0000 s
% 19.91/3.63 % (2175157)Peak memory usage: 88 MB
% 19.91/3.63 % (2175158)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1562152007:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 19.91/3.63 % (2175153)------------------------------
% 19.91/3.63 % (2175153)------------------------------
% 19.91/3.63 % (2175157)------------------------------
% 19.91/3.63 % (2175157)------------------------------
% 19.91/3.63 % (2175161)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=177902635:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 19.91/3.63 % (2175161)Refutation not found, incomplete strategy
% 19.91/3.63 % (2175161)------------------------------
% 19.91/3.63 % (2175161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/3.63 % (2175161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/3.63 % (2175161)CaDiCaL version: 2.1.3
% 19.91/3.63 % (2175161)Termination reason: Refutation not found, incomplete strategy
% 19.91/3.63 % (2175161)Time elapsed: 0.0000 s
% 19.91/3.63 % (2175161)Peak memory usage: 88 MB
% 19.91/3.63 % (2175154)Instruction limit reached!
% 19.91/3.63 % (2175154)------------------------------
% 19.91/3.63 % (2175154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.91/3.63 % (2175154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.91/3.63 % (2175154)CaDiCaL version: 2.1.3
% 19.91/3.63 % (2175154)Termination reason: Instruction limit
% 19.91/3.63 % (2175154)Termination phase: Saturation
% 19.91/3.63 % (2175154)Time elapsed: 0.307 s
% 19.91/3.63 % (2175154)Peak memory usage: 99 MB
% 19.91/3.63 % (2175154)Instructions burned: 907 (million)
% 19.91/3.63 % (2175165)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1348185593:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 19.91/3.63 % (2175167)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3200175115:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 35.60/5.86 % (2175161)------------------------------
% 35.60/5.86 % (2175161)------------------------------
% 35.60/5.86 % (2175209)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=1549526701:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi)
% 35.60/5.86 % (2175209)Refutation not found, incomplete strategy
% 35.60/5.86 % (2175209)------------------------------
% 35.60/5.86 % (2175209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.60/5.86 % (2175209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.60/5.86 % (2175209)CaDiCaL version: 2.1.3
% 35.60/5.86 % (2175209)Termination reason: Refutation not found, incomplete strategy
% 35.60/5.86 % (2175209)Time elapsed: 0.001 s
% 35.60/5.86 % (2175209)Peak memory usage: 88 MB
% 35.60/5.86 % (2175165)Instruction limit reached!
% 35.60/5.86 % (2175165)------------------------------
% 35.60/5.86 % (2175165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.60/5.86 % (2175165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.60/5.86 % (2175165)CaDiCaL version: 2.1.3
% 35.60/5.86 % (2175165)Termination reason: Instruction limit
% 35.60/5.86 % (2175165)Termination phase: Saturation
% 35.60/5.86 % (2175165)Time elapsed: 0.182 s
% 35.60/5.86 % (2175165)Peak memory usage: 92 MB
% 35.60/5.86 % (2175165)Instructions burned: 593 (million)
% 35.60/5.86 % (2175135)Instruction limit reached!
% 35.60/5.86 % (2175135)------------------------------
% 35.60/5.86 % (2175135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.60/5.86 % (2175135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.60/5.86 % (2175135)CaDiCaL version: 2.1.3
% 35.60/5.86 % (2175135)Termination reason: Instruction limit
% 35.60/5.86 % (2175135)Termination phase: Saturation
% 35.60/5.86 % (2175135)Time elapsed: 0.972 s
% 35.60/5.86 % (2175135)Peak memory usage: 142 MB
% 35.60/5.86 % (2175135)Instructions burned: 2350 (million)
% 35.60/5.86 % (2175245)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3512161507:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 35.60/5.86 % (2175245)Instruction limit reached!
% 35.60/5.86 % (2175245)------------------------------
% 35.60/5.86 % (2175245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.60/5.86 % (2175245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.60/5.86 % (2175245)CaDiCaL version: 2.1.3
% 35.60/5.86 % (2175245)Termination reason: Instruction limit
% 35.60/5.86 % (2175245)Termination phase: Saturation
% 35.60/5.86 % (2175245)Time elapsed: 0.035 s
% 35.60/5.86 % (2175245)Peak memory usage: 90 MB
% 35.60/5.86 % (2175245)Instructions burned: 137 (million)
% 35.60/5.86 % (2175263)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1972937146:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/141Mi)
% 35.60/5.86 % (2175209)------------------------------
% 35.60/5.86 % (2175209)------------------------------
% 35.60/5.86 % (2175263)Refutation not found, incomplete strategy
% 35.60/5.86 % (2175263)------------------------------
% 35.60/5.86 % (2175263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.60/5.86 % (2175263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.60/5.86 % (2175263)CaDiCaL version: 2.1.3
% 35.60/5.86 % (2175263)Termination reason: Refutation not found, incomplete strategy
% 35.60/5.86 % (2175263)Time elapsed: 0.019 s
% 35.60/5.86 % (2175263)Peak memory usage: 88 MB
% 35.60/5.86 % (2175288)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4224614955:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2982 on theBenchmark for (2982ds/431Mi)
% 35.60/5.86 % (2175288)Refutation not found, incomplete strategy
% 35.60/5.86 % (2175288)------------------------------
% 35.60/5.86 % (2175288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.60/5.86 % (2175288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.60/5.86 % (2175288)CaDiCaL version: 2.1.3
% 35.60/5.86 % (2175288)Termination reason: Refutation not found, incomplete strategy
% 35.60/5.86 % (2175288)Time elapsed: 0.0000 s
% 35.60/5.86 % (2175288)Peak memory usage: 88 MB
% 35.60/5.86 % (2175305)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=1693760204:i=6060:aac=none:ins=25_2982 on theBenchmark for (2982ds/6060Mi)
% 50.39/7.97 % (2175263)------------------------------
% 50.39/7.97 % (2175263)------------------------------
% 50.39/7.97 % (2175288)------------------------------
% 50.39/7.97 % (2175288)------------------------------
% 50.39/7.97 % (2175332)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=339599177:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2980 on theBenchmark for (2980ds/150Mi)
% 50.39/7.97 % (2175332)Instruction limit reached!
% 50.39/7.97 % (2175332)------------------------------
% 50.39/7.97 % (2175332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.39/7.97 % (2175332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.39/7.97 % (2175332)CaDiCaL version: 2.1.3
% 50.39/7.97 % (2175332)Termination reason: Instruction limit
% 50.39/7.97 % (2175332)Termination phase: Saturation
% 50.39/7.97 % (2175332)Time elapsed: 0.042 s
% 50.39/7.97 % (2175332)Peak memory usage: 90 MB
% 50.39/7.97 % (2175332)Instructions burned: 150 (million)
% 50.39/7.97 % (2175333)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=4042441149:i=14155:bd=all_2979 on theBenchmark for (2979ds/14155Mi)
% 50.39/7.97 % (2175335)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=367629487:i=667:av=off:fsr=off_2979 on theBenchmark for (2979ds/667Mi)
% 50.39/7.97 % (2175335)Refutation not found, incomplete strategy
% 50.39/7.97 % (2175335)------------------------------
% 50.39/7.97 % (2175335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.39/7.97 % (2175335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.39/7.97 % (2175335)CaDiCaL version: 2.1.3
% 50.39/7.97 % (2175335)Termination reason: Refutation not found, incomplete strategy
% 50.39/7.97 % (2175335)Time elapsed: 0.001 s
% 50.39/7.97 % (2175335)Peak memory usage: 88 MB
% 50.39/7.97 % (2175335)------------------------------
% 50.39/7.97 % (2175335)------------------------------
% 50.39/7.97 % (2175338)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=2711778330:s2a=on:i=185:s2at=1.8:fdi=4_2976 on theBenchmark for (2976ds/185Mi)
% 50.39/7.97 % (2175338)Instruction limit reached!
% 50.39/7.97 % (2175338)------------------------------
% 50.39/7.97 % (2175338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.39/7.97 % (2175338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.39/7.97 % (2175338)CaDiCaL version: 2.1.3
% 50.39/7.97 % (2175338)Termination reason: Instruction limit
% 50.39/7.97 % (2175338)Termination phase: Saturation
% 50.39/7.97 % (2175338)Time elapsed: 0.059 s
% 50.39/7.97 % (2175338)Peak memory usage: 91 MB
% 50.39/7.97 % (2175338)Instructions burned: 186 (million)
% 50.39/7.97 % (2175340)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=917249428:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2975 on theBenchmark for (2975ds/193Mi)
% 50.39/7.97 % (2175340)Instruction limit reached!
% 50.39/7.97 % (2175340)------------------------------
% 50.39/7.97 % (2175340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.39/7.97 % (2175340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.39/7.97 % (2175340)CaDiCaL version: 2.1.3
% 50.39/7.97 % (2175340)Termination reason: Instruction limit
% 50.39/7.97 % (2175340)Termination phase: Saturation
% 50.39/7.97 % (2175340)Time elapsed: 0.050 s
% 50.39/7.97 % (2175340)Peak memory usage: 89 MB
% 50.39/7.97 % (2175340)Instructions burned: 194 (million)
% 50.39/7.97 % (2175342)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2895371658:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2973 on theBenchmark for (2973ds/4850Mi)
% 50.39/7.97 % (2175342)Refutation not found, incomplete strategy
% 50.39/7.97 % (2175342)------------------------------
% 50.39/7.97 % (2175342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.39/7.97 % (2175342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.39/7.97 % (2175342)CaDiCaL version: 2.1.3
% 50.39/7.97 % (2175342)Termination reason: Refutation not found, incomplete strategy
% 50.39/7.97 % (2175342)Time elapsed: 0.0000 s
% 50.39/7.97 % (2175342)Peak memory usage: 87 MB
% 50.39/7.97 % (2175342)------------------------------
% 63.76/9.99 % (2175342)------------------------------
% 63.76/9.99 % (2175344)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1392277917:i=12111:sd=1:ss=included_2971 on theBenchmark for (2971ds/12111Mi)
% 63.76/9.99 % (2175158)Instruction limit reached!
% 63.76/9.99 % (2175158)------------------------------
% 63.76/9.99 % (2175158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.76/9.99 % (2175158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.76/9.99 % (2175158)CaDiCaL version: 2.1.3
% 63.76/9.99 % (2175158)Termination reason: Instruction limit
% 63.76/9.99 % (2175158)Termination phase: Saturation
% 63.76/9.99 % (2175158)Time elapsed: 1.765 s
% 63.76/9.99 % (2175158)Peak memory usage: 167 MB
% 63.76/9.99 % (2175158)Instructions burned: 5203 (million)
% 63.76/9.99 % (2175346)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1226504819:i=319:kws=precedence:fsr=off_2970 on theBenchmark for (2970ds/319Mi)
% 63.76/9.99 % (2175346)Instruction limit reached!
% 63.76/9.99 % (2175346)------------------------------
% 63.76/9.99 % (2175346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.76/9.99 % (2175346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.76/9.99 % (2175346)CaDiCaL version: 2.1.3
% 63.76/9.99 % (2175346)Termination reason: Instruction limit
% 63.76/9.99 % (2175346)Termination phase: Saturation
% 63.76/9.99 % (2175346)Time elapsed: 0.113 s
% 63.76/9.99 % (2175346)Peak memory usage: 94 MB
% 63.76/9.99 % (2175346)Instructions burned: 322 (million)
% 63.76/9.99 % (2175348)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=577464851:i=2064:ep=RST_2968 on theBenchmark for (2968ds/2064Mi)
% 63.76/9.99 % (2175348)Instruction limit reached!
% 63.76/9.99 % (2175348)------------------------------
% 63.76/9.99 % (2175348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.76/9.99 % (2175348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.76/9.99 % (2175348)CaDiCaL version: 2.1.3
% 63.76/9.99 % (2175348)Termination reason: Instruction limit
% 63.76/9.99 % (2175348)Termination phase: Saturation
% 63.76/9.99 % (2175348)Time elapsed: 0.568 s
% 63.76/9.99 % (2175348)Peak memory usage: 99 MB
% 63.76/9.99 % (2175348)Instructions burned: 2066 (million)
% 63.76/9.99 % (2175351)dis-1011_128_sil=32000:random_seed=1261164138:i=3706:ep=RST:av=off_2961 on theBenchmark for (2961ds/3706Mi)
% 63.76/9.99 % (2175305)Instruction limit reached!
% 63.76/9.99 % (2175305)------------------------------
% 63.76/9.99 % (2175305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.76/9.99 % (2175305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.76/9.99 % (2175305)CaDiCaL version: 2.1.3
% 63.76/9.99 % (2175305)Termination reason: Instruction limit
% 63.76/9.99 % (2175305)Termination phase: Saturation
% 63.76/9.99 % (2175305)Time elapsed: 2.062 s
% 63.76/9.99 % (2175305)Peak memory usage: 187 MB
% 63.76/9.99 % (2175305)Instructions burned: 6063 (million)
% 63.76/9.99 % (2175353)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=739277900:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2960 on theBenchmark for (2960ds/757Mi)
% 63.76/9.99 % (2175353)Refutation not found, incomplete strategy
% 63.76/9.99 % (2175353)------------------------------
% 63.76/9.99 % (2175353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.76/9.99 % (2175353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.76/9.99 % (2175353)CaDiCaL version: 2.1.3
% 63.76/9.99 % (2175353)Termination reason: Refutation not found, incomplete strategy
% 63.76/9.99 % (2175353)Time elapsed: 0.0000 s
% 63.76/9.99 % (2175353)Peak memory usage: 88 MB
% 63.76/9.99 % (2175353)------------------------------
% 63.76/9.99 % (2175353)------------------------------
% 63.76/9.99 % (2175355)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=948539546:i=13913:ss=axioms:sgt=8_2957 on theBenchmark for (2957ds/13913Mi)
% 63.76/9.99 % (2175351)Instruction limit reached!
% 63.76/9.99 % (2175351)------------------------------
% 63.76/9.99 % (2175351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.76/9.99 % (2175351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.76/9.99 % (2175351)CaDiCaL version: 2.1.3
% 63.76/9.99 % (2175351)Termination reason: Instruction limit
% 63.76/9.99 % (2175351)Termination phase: Saturation
% 63.76/9.99 % (2175351)Time elapsed: 1.142 s
% 71.27/11.23 % (2175351)Peak memory usage: 99 MB
% 71.27/11.23 % (2175351)Instructions burned: 3706 (million)
% 71.27/11.23 % (2175357)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2492871689:i=9925:aac=none_2949 on theBenchmark for (2949ds/9925Mi)
% 71.27/11.23 % (2175357)Refutation not found, incomplete strategy
% 71.27/11.23 % (2175357)------------------------------
% 71.27/11.23 % (2175357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.27/11.23 % (2175357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.27/11.23 % (2175357)CaDiCaL version: 2.1.3
% 71.27/11.23 % (2175357)Termination reason: Refutation not found, incomplete strategy
% 71.27/11.23 % (2175357)Time elapsed: 0.315 s
% 71.27/11.23 % (2175357)Peak memory usage: 127 MB
% 71.27/11.23 % (2175357)Instructions burned: 855 (million)
% 71.27/11.23 % (2175357)------------------------------
% 71.27/11.23 % (2175357)------------------------------
% 71.27/11.23 % (2175359)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=4181637802:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2943 on theBenchmark for (2943ds/2479Mi)
% 71.27/11.23 % (2175359)Refutation not found, incomplete strategy
% 71.27/11.23 % (2175359)------------------------------
% 71.27/11.23 % (2175359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.27/11.23 % (2175359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.27/11.23 % (2175359)CaDiCaL version: 2.1.3
% 71.27/11.23 % (2175359)Termination reason: Refutation not found, incomplete strategy
% 71.27/11.23 % (2175359)Time elapsed: 0.0000 s
% 71.27/11.23 % (2175359)Peak memory usage: 88 MB
% 71.27/11.23 % (2175359)------------------------------
% 71.27/11.23 % (2175359)------------------------------
% 71.27/11.23 % (2175361)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3371562703:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2940 on theBenchmark for (2940ds/440Mi)
% 71.27/11.23 % (2175167)Instruction limit reached!
% 71.27/11.23 % (2175167)------------------------------
% 71.27/11.23 % (2175167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.27/11.23 % (2175167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.27/11.23 % (2175167)CaDiCaL version: 2.1.3
% 71.27/11.23 % (2175167)Termination reason: Instruction limit
% 71.27/11.23 % (2175167)Termination phase: Saturation
% 71.27/11.23 % (2175167)Time elapsed: 4.562 s
% 71.27/11.23 % (2175167)Peak memory usage: 239 MB
% 71.27/11.23 % (2175167)Instructions burned: 13195 (million)
% 71.27/11.23 % (2175361)Instruction limit reached!
% 71.27/11.23 % (2175361)------------------------------
% 71.27/11.23 % (2175361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.27/11.23 % (2175361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.27/11.23 % (2175361)CaDiCaL version: 2.1.3
% 71.27/11.23 % (2175361)Termination reason: Instruction limit
% 71.27/11.23 % (2175361)Termination phase: Saturation
% 71.27/11.23 % (2175361)Time elapsed: 0.128 s
% 71.27/11.23 % (2175361)Peak memory usage: 94 MB
% 71.27/11.23 % (2175361)Instructions burned: 441 (million)
% 71.27/11.23 % (2175363)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2891534093:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2938 on theBenchmark for (2938ds/11145Mi)
% 71.27/11.23 % (2175364)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=4050877695:cts=off:i=3034:av=off:er=known:fsd=on_2938 on theBenchmark for (2938ds/3034Mi)
% 71.27/11.23 % (2175333)Instruction limit reached!
% 71.27/11.23 % (2175333)------------------------------
% 71.27/11.23 % (2175333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.27/11.23 % (2175333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.27/11.23 % (2175333)CaDiCaL version: 2.1.3
% 71.27/11.23 % (2175333)Termination reason: Instruction limit
% 71.27/11.23 % (2175333)Termination phase: Saturation
% 71.27/11.23 % (2175333)Time elapsed: 4.975 s
% 71.27/11.23 % (2175333)Peak memory usage: 233 MB
% 71.27/11.23 % (2175333)Instructions burned: 14158 (million)
% 71.27/11.23 % (2175344)Instruction limit reached!
% 71.27/11.23 % (2175344)------------------------------
% 71.27/11.23 % (2175344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.27/11.23 % (2175344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.27/11.23 % (2175344)CaDiCaL version: 2.1.3
% 78.31/12.27 % (2175344)Termination reason: Instruction limit
% 78.31/12.27 % (2175344)Termination phase: Saturation
% 78.31/12.27 % (2175344)Time elapsed: 4.226 s
% 78.31/12.27 % (2175344)Peak memory usage: 221 MB
% 78.31/12.27 % (2175344)Instructions burned: 12114 (million)
% 78.31/12.27 % (2175367)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1985282045:st=2:s2a=on:i=524:s2at=2:ss=axioms_2928 on theBenchmark for (2928ds/524Mi)
% 78.31/12.27 % (2175364)Instruction limit reached!
% 78.31/12.27 % (2175364)------------------------------
% 78.31/12.27 % (2175364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.31/12.27 % (2175364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.31/12.27 % (2175364)CaDiCaL version: 2.1.3
% 78.31/12.27 % (2175364)Termination reason: Instruction limit
% 78.31/12.27 % (2175364)Termination phase: Saturation
% 78.31/12.27 % (2175364)Time elapsed: 1.006 s
% 78.31/12.27 % (2175364)Peak memory usage: 142 MB
% 78.31/12.27 % (2175364)Instructions burned: 3037 (million)
% 78.31/12.27 % (2175369)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2106199005:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2927 on theBenchmark for (2927ds/1016Mi)
% 78.31/12.27 % (2175370)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3648283831:i=14123:bd=preordered:ins=4_2927 on theBenchmark for (2927ds/14123Mi)
% 78.31/12.27 % (2175367)Instruction limit reached!
% 78.31/12.27 % (2175367)------------------------------
% 78.31/12.27 % (2175367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.31/12.27 % (2175367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.31/12.27 % (2175367)CaDiCaL version: 2.1.3
% 78.31/12.27 % (2175367)Termination reason: Instruction limit
% 78.31/12.27 % (2175367)Termination phase: Saturation
% 78.31/12.27 % (2175367)Time elapsed: 0.140 s
% 78.31/12.27 % (2175367)Peak memory usage: 93 MB
% 78.31/12.27 % (2175367)Instructions burned: 527 (million)
% 78.31/12.27 % (2175373)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2420331304:i=5781:kws=precedence:bd=all:rawr=on_2926 on theBenchmark for (2926ds/5781Mi)
% 78.31/12.27 % (2175369)Instruction limit reached!
% 78.31/12.27 % (2175369)------------------------------
% 78.31/12.27 % (2175369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.31/12.27 % (2175369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.31/12.27 % (2175369)CaDiCaL version: 2.1.3
% 78.31/12.27 % (2175369)Termination reason: Instruction limit
% 78.31/12.27 % (2175369)Termination phase: Saturation
% 78.31/12.27 % (2175369)Time elapsed: 0.262 s
% 78.31/12.27 % (2175369)Peak memory usage: 97 MB
% 78.31/12.27 % (2175369)Instructions burned: 1016 (million)
% 78.31/12.27 % (2175375)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=3446029218:i=2448:gtgl=5:bd=preordered:gtg=all_2924 on theBenchmark for (2924ds/2448Mi)
% 78.31/12.27 % (2175375)Instruction limit reached!
% 78.31/12.27 % (2175375)------------------------------
% 78.31/12.27 % (2175375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.31/12.27 % (2175375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.31/12.27 % (2175375)CaDiCaL version: 2.1.3
% 78.31/12.27 % (2175375)Termination reason: Instruction limit
% 78.31/12.27 % (2175375)Termination phase: Saturation
% 78.31/12.27 % (2175375)Time elapsed: 0.722 s
% 78.31/12.27 % (2175375)Peak memory usage: 160 MB
% 78.31/12.27 % (2175375)Instructions burned: 2451 (million)
% 78.31/12.27 % (2175377)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2530610895:i=3223:kws=precedence:fgj=on:av=off_2916 on theBenchmark for (2916ds/3223Mi)
% 78.31/12.27 % (2175355)Instruction limit reached!
% 78.31/12.27 % (2175355)------------------------------
% 78.31/12.27 % (2175355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.31/12.27 % (2175355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.31/12.27 % (2175355)CaDiCaL version: 2.1.3
% 78.31/12.27 % (2175355)Termination reason: Instruction limit
% 78.31/12.27 % (2175355)Termination phase: Saturation
% 78.31/12.27 % (2175355)Time elapsed: 4.882 s
% 78.31/12.27 % (2175355)Peak memory usage: 234 MB
% 78.31/12.27 % (2175355)Instructions burned: 13915 (million)
% 78.31/12.27 % (2175373)Instruction limit reached!
% 78.31/12.27 % (2175373)------------------------------
% 78.31/12.27 % (2175373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.43/14.79 % (2175373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.43/14.79 % (2175373)CaDiCaL version: 2.1.3
% 95.43/14.79 % (2175373)Termination reason: Instruction limit
% 95.43/14.79 % (2175373)Termination phase: Saturation
% 95.43/14.79 % (2175373)Time elapsed: 1.779 s
% 95.43/14.79 % (2175373)Peak memory usage: 137 MB
% 95.43/14.79 % (2175373)Instructions burned: 5782 (million)
% 95.43/14.79 % (2175363)Instruction limit reached!
% 95.43/14.79 % (2175363)------------------------------
% 95.43/14.79 % (2175363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.43/14.79 % (2175363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.43/14.79 % (2175363)CaDiCaL version: 2.1.3
% 95.43/14.79 % (2175363)Termination reason: Instruction limit
% 95.43/14.79 % (2175363)Termination phase: Saturation
% 95.43/14.79 % (2175363)Time elapsed: 3.064 s
% 95.43/14.79 % (2175363)Peak memory usage: 212 MB
% 95.43/14.79 % (2175363)Instructions burned: 11147 (million)
% 95.43/14.79 % (2175377)Instruction limit reached!
% 95.43/14.79 % (2175377)------------------------------
% 95.43/14.79 % (2175377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.43/14.79 % (2175377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.43/14.79 % (2175377)CaDiCaL version: 2.1.3
% 95.43/14.79 % (2175377)Termination reason: Instruction limit
% 95.43/14.79 % (2175377)Termination phase: Saturation
% 95.43/14.79 % (2175377)Time elapsed: 1.128 s
% 95.43/14.79 % (2175377)Peak memory usage: 151 MB
% 95.43/14.79 % (2175377)Instructions burned: 3225 (million)
% 95.43/14.79 % (2175379)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3512820452:st=5.6:i=2033:sd=3:ss=axioms_2908 on theBenchmark for (2908ds/2033Mi)
% 95.43/14.79 % (2175381)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=210864238:i=21611:sd=3:ss=axioms_2907 on theBenchmark for (2907ds/21611Mi)
% 95.43/14.79 % (2175382)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=898474631:i=4835:sd=13:ss=axioms:sgt=23_2903 on theBenchmark for (2903ds/4835Mi)
% 95.43/14.79 % (2175380)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=125834040:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2907 on theBenchmark for (2907ds/2055Mi)
% 95.43/14.79 % (2175382)Refutation not found, incomplete strategy
% 95.43/14.79 % (2175382)------------------------------
% 95.43/14.79 % (2175382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.43/14.79 % (2175382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.43/14.79 % (2175382)CaDiCaL version: 2.1.3
% 95.43/14.79 % (2175382)Termination reason: Refutation not found, incomplete strategy
% 95.43/14.79 % (2175382)Time elapsed: 0.001 s
% 95.43/14.79 % (2175382)Peak memory usage: 88 MB
% 95.43/14.79 % (2175382)------------------------------
% 95.43/14.79 % (2175382)------------------------------
% 95.43/14.79 % (2175387)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=2812073565:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2898 on theBenchmark for (2898ds/797Mi)
% 95.43/14.79 % (2175387)Refutation not found, incomplete strategy
% 95.43/14.79 % (2175387)------------------------------
% 95.43/14.79 % (2175387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.43/14.79 % (2175387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.43/14.79 % (2175387)CaDiCaL version: 2.1.3
% 95.43/14.79 % (2175387)Termination reason: Refutation not found, incomplete strategy
% 95.43/14.79 % (2175387)Time elapsed: 0.002 s
% 95.43/14.79 % (2175387)Peak memory usage: 87 MB
% 95.43/14.79 % (2175379)Refutation not found, incomplete strategy
% 95.43/14.79 % (2175379)------------------------------
% 95.43/14.79 % (2175379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.43/14.79 % (2175379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.43/14.79 % (2175379)CaDiCaL version: 2.1.3
% 95.43/14.79 % (2175379)Termination reason: Refutation not found, incomplete strategy
% 95.43/14.79 % (2175379)Time elapsed: 0.319 s
% 95.43/14.79 % (2175379)Peak memory usage: 126 MB
% 95.43/14.79 % (2175379)Instructions burned: 855 (million)
% 95.43/14.79 % (2175387)------------------------------
% 95.43/14.79 % (2175387)------------------------------
% 95.43/14.79 % (2175379)------------------------------
% 95.43/14.79 % (2175379)------------------------------
% 114.94/17.42 % (2175389)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1006669860:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2896 on theBenchmark for (2896ds/2326Mi)
% 114.94/17.42 % (2175389)Refutation not found, incomplete strategy
% 114.94/17.42 % (2175389)------------------------------
% 114.94/17.42 % (2175389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.94/17.42 % (2175389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.94/17.42 % (2175389)CaDiCaL version: 2.1.3
% 114.94/17.42 % (2175389)Termination reason: Refutation not found, incomplete strategy
% 114.94/17.42 % (2175389)Time elapsed: 0.0000 s
% 114.94/17.42 % (2175389)Peak memory usage: 88 MB
% 114.94/17.42 % (2175390)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3826128183:i=6038:nm=6_2895 on theBenchmark for (2895ds/6038Mi)
% 114.94/17.42 % (2175389)------------------------------
% 114.94/17.42 % (2175389)------------------------------
% 114.94/17.42 % (2175380)Instruction limit reached!
% 114.94/17.42 % (2175380)------------------------------
% 114.94/17.42 % (2175380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.94/17.42 % (2175380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.94/17.42 % (2175380)CaDiCaL version: 2.1.3
% 114.94/17.42 % (2175380)Termination reason: Instruction limit
% 114.94/17.42 % (2175380)Termination phase: Saturation
% 114.94/17.42 % (2175380)Time elapsed: 0.655 s
% 114.94/17.42 % (2175380)Peak memory usage: 138 MB
% 114.94/17.42 % (2175380)Instructions burned: 2056 (million)
% 114.94/17.42 % (2175393)lrs+10_1_sil=32000:sp=occurrence:random_seed=4194736289:st=2:i=33334:sd=3:ss=included:sgt=32_2893 on theBenchmark for (2893ds/33334Mi)
% 114.94/17.42 % (2175394)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=17954073:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2893 on theBenchmark for (2893ds/1008Mi)
% 114.94/17.42 % (2175394)Refutation not found, incomplete strategy
% 114.94/17.42 % (2175394)------------------------------
% 114.94/17.42 % (2175394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.94/17.42 % (2175394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.94/17.42 % (2175394)CaDiCaL version: 2.1.3
% 114.94/17.42 % (2175394)Termination reason: Refutation not found, incomplete strategy
% 114.94/17.42 % (2175394)Time elapsed: 0.001 s
% 114.94/17.42 % (2175394)Peak memory usage: 88 MB
% 114.94/17.42 % (2175394)Instructions burned: 1 (million)
% 114.94/17.42 % (2175390)Refutation not found, incomplete strategy
% 114.94/17.42 % (2175390)------------------------------
% 114.94/17.42 % (2175390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.94/17.42 % (2175390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.94/17.42 % (2175390)CaDiCaL version: 2.1.3
% 114.94/17.42 % (2175390)Termination reason: Refutation not found, incomplete strategy
% 114.94/17.42 % (2175390)Time elapsed: 0.318 s
% 114.94/17.42 % (2175390)Peak memory usage: 127 MB
% 114.94/17.42 % (2175390)Instructions burned: 854 (million)
% 114.94/17.42 % (2175394)------------------------------
% 114.94/17.42 % (2175394)------------------------------
% 114.94/17.42 % (2175397)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=3292523285:i=8327:s2at=5:bd=preordered_2891 on theBenchmark for (2891ds/8327Mi)
% 114.94/17.42 % (2175390)------------------------------
% 114.94/17.42 % (2175390)------------------------------
% 114.94/17.42 % (2175399)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=1848066314:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2889 on theBenchmark for (2889ds/1083Mi)
% 114.94/17.42 % (2175399)Instruction limit reached!
% 114.94/17.42 % (2175399)------------------------------
% 114.94/17.42 % (2175399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.94/17.42 % (2175399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.94/17.42 % (2175399)CaDiCaL version: 2.1.3
% 114.94/17.42 % (2175399)Termination reason: Instruction limit
% 114.94/17.42 % (2175399)Termination phase: Saturation
% 114.94/17.42 % (2175399)Time elapsed: 0.279 s
% 114.94/17.42 % (2175399)Peak memory usage: 98 MB
% 114.94/17.42 % (2175399)Instructions burned: 1085 (million)
% 114.94/17.42 % (2175401)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=1635342647:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2885 on theBenchmark for (2885ds/1084Mi)
% 138.30/20.82 % (2175401)Instruction limit reached!
% 138.30/20.82 % (2175401)------------------------------
% 138.30/20.82 % (2175401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.30/20.82 % (2175401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.30/20.82 % (2175401)CaDiCaL version: 2.1.3
% 138.30/20.82 % (2175401)Termination reason: Instruction limit
% 138.30/20.82 % (2175401)Termination phase: Saturation
% 138.30/20.82 % (2175401)Time elapsed: 0.239 s
% 138.30/20.82 % (2175401)Peak memory usage: 98 MB
% 138.30/20.82 % (2175401)Instructions burned: 1088 (million)
% 138.30/20.82 % (2175403)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3971717321:i=6995:s2at=5:gtg=all_2882 on theBenchmark for (2882ds/6995Mi)
% 138.30/20.82 % (2175370)Instruction limit reached!
% 138.30/20.82 % (2175370)------------------------------
% 138.30/20.82 % (2175370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.30/20.82 % (2175370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.30/20.82 % (2175370)CaDiCaL version: 2.1.3
% 138.30/20.82 % (2175370)Termination reason: Instruction limit
% 138.30/20.82 % (2175370)Termination phase: Saturation
% 138.30/20.82 % (2175370)Time elapsed: 4.925 s
% 138.30/20.82 % (2175370)Peak memory usage: 247 MB
% 138.30/20.82 % (2175370)Instructions burned: 14125 (million)
% 138.30/20.82 % (2175405)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=2991335625:st=2:i=6225:sd=15:ss=axioms_2877 on theBenchmark for (2877ds/6225Mi)
% 138.30/20.82 % (2175405)Refutation not found, incomplete strategy
% 138.30/20.82 % (2175405)------------------------------
% 138.30/20.82 % (2175405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.30/20.82 % (2175405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.30/20.82 % (2175405)CaDiCaL version: 2.1.3
% 138.30/20.82 % (2175405)Termination reason: Refutation not found, incomplete strategy
% 138.30/20.82 % (2175405)Time elapsed: 0.0000 s
% 138.30/20.82 % (2175405)Peak memory usage: 88 MB
% 138.30/20.82 % (2175405)------------------------------
% 138.30/20.82 % (2175405)------------------------------
% 138.30/20.82 % (2175407)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3783418312:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2874 on theBenchmark for (2874ds/3372Mi)
% 138.30/20.82 % (2175407)Instruction limit reached!
% 138.30/20.82 % (2175407)------------------------------
% 138.30/20.82 % (2175407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.30/20.82 % (2175407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.30/20.82 % (2175407)CaDiCaL version: 2.1.3
% 138.30/20.82 % (2175407)Termination reason: Instruction limit
% 138.30/20.82 % (2175407)Termination phase: Saturation
% 138.30/20.82 % (2175407)Time elapsed: 0.973 s
% 138.30/20.82 % (2175407)Peak memory usage: 150 MB
% 138.30/20.82 % (2175407)Instructions burned: 3375 (million)
% 138.30/20.82 % (2175542)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=2121909435:st=2.3:i=26457:sd=10:ss=included:sgt=8_2864 on theBenchmark for (2864ds/26457Mi)
% 138.30/20.82 % (2175397)Instruction limit reached!
% 138.30/20.82 % (2175397)------------------------------
% 138.30/20.82 % (2175397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.30/20.82 % (2175397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.30/20.82 % (2175397)CaDiCaL version: 2.1.3
% 138.30/20.82 % (2175397)Termination reason: Instruction limit
% 138.30/20.82 % (2175397)Termination phase: Saturation
% 138.30/20.82 % (2175397)Time elapsed: 2.728 s
% 138.30/20.82 % (2175397)Peak memory usage: 172 MB
% 138.30/20.82 % (2175397)Instructions burned: 8329 (million)
% 138.30/20.82 % (2175596)lrs+10_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:foolp=on:s2agt=20:sac=on:random_seed=1274375293:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2862 on theBenchmark for (2862ds/13494Mi)
% 138.30/20.82 % (2175542)Refutation not found, incomplete strategy
% 138.30/20.82 % (2175542)------------------------------
% 138.30/20.82 % (2175542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.30/20.82 % (2175542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.76/23.22 % (2175542)CaDiCaL version: 2.1.3
% 155.76/23.22 % (2175542)Termination reason: Refutation not found, incomplete strategy
% 155.76/23.22 % (2175542)Time elapsed: 0.315 s
% 155.76/23.22 % (2175542)Peak memory usage: 127 MB
% 155.76/23.22 % (2175542)Instructions burned: 851 (million)
% 155.76/23.22 % (2175542)------------------------------
% 155.76/23.22 % (2175542)------------------------------
% 155.76/23.22 % (2175403)Instruction limit reached!
% 155.76/23.22 % (2175403)------------------------------
% 155.76/23.22 % (2175403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.76/23.22 % (2175403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.76/23.22 % (2175403)CaDiCaL version: 2.1.3
% 155.76/23.22 % (2175403)Termination reason: Instruction limit
% 155.76/23.22 % (2175403)Termination phase: Saturation
% 155.76/23.22 % (2175403)Time elapsed: 2.499 s
% 155.76/23.22 % (2175403)Peak memory usage: 187 MB
% 155.76/23.22 % (2175403)Instructions burned: 6995 (million)
% 155.76/23.22 % (2175656)dis-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:fde=unused:sp=const_min:spb=goal_then_units:lcm=predicate:acc=on:flr=on:random_seed=1855035991:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2857 on theBenchmark for (2857ds/2503Mi)
% 155.76/23.22 % (2175657)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=1474645467:i=2559:sd=1:ep=RSTC:ss=axioms_2856 on theBenchmark for (2856ds/2559Mi)
% 155.76/23.22 % (2175657)Refutation not found, incomplete strategy
% 155.76/23.22 % (2175657)------------------------------
% 155.76/23.22 % (2175657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.76/23.22 % (2175657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.76/23.22 % (2175657)CaDiCaL version: 2.1.3
% 155.76/23.22 % (2175657)Termination reason: Refutation not found, incomplete strategy
% 155.76/23.22 % (2175657)Time elapsed: 0.335 s
% 155.76/23.22 % (2175657)Peak memory usage: 127 MB
% 155.76/23.22 % (2175657)Instructions burned: 850 (million)
% 155.76/23.22 % (2175657)------------------------------
% 155.76/23.22 % (2175657)------------------------------
% 155.76/23.22 % (2175808)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=940073599:i=30753:av=off:ss=included_2849 on theBenchmark for (2849ds/30753Mi)
% 155.76/23.22 % (2175656)Instruction limit reached!
% 155.76/23.22 % (2175656)------------------------------
% 155.76/23.22 % (2175656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.76/23.22 % (2175656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.76/23.22 % (2175656)CaDiCaL version: 2.1.3
% 155.76/23.22 % (2175656)Termination reason: Instruction limit
% 155.76/23.22 % (2175656)Termination phase: Saturation
% 155.76/23.22 % (2175656)Time elapsed: 0.874 s
% 155.76/23.22 % (2175656)Peak memory usage: 143 MB
% 155.76/23.22 % (2175656)Instructions burned: 2503 (million)
% 155.76/23.22 % (2175814)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=3087898123:i=26473:ep=RSTC_2846 on theBenchmark for (2846ds/26473Mi)
% 155.76/23.22 % (2175381)Instruction limit reached!
% 155.76/23.22 % (2175381)------------------------------
% 155.76/23.22 % (2175381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.76/23.22 % (2175381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.76/23.22 % (2175381)CaDiCaL version: 2.1.3
% 155.76/23.22 % (2175381)Termination reason: Instruction limit
% 155.76/23.22 % (2175381)Termination phase: Saturation
% 155.76/23.22 % (2175381)Time elapsed: 6.090 s
% 155.76/23.22 % (2175381)Peak memory usage: 309 MB
% 155.76/23.22 % (2175381)Instructions burned: 21615 (million)
% 155.76/23.22 % (2175816)dis-1011_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:tgt=ground:npcc=on:sp=arity:sos=on:erd=off:rp=on:gs=on:kmz=on:random_seed=3252959892:cts=off:i=2759:kws=inv_arity:fgj=on_2839 on theBenchmark for (2839ds/2759Mi)
% 155.76/23.22 % (2175816)Refutation not found, incomplete strategy
% 155.76/23.22 % (2175816)------------------------------
% 155.76/23.22 % (2175816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.76/23.22 % (2175816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.76/23.22 % (2175816)CaDiCaL version: 2.1.3
% 155.76/23.22 % (2175816)Termination reason: Refutation not found, incomplete strategy
% 155.76/23.22 % (2175816)Time elapsed: 0.315 s
% 155.76/23.22 % (2175816)Peak memory usage: 127 MB
% 155.76/23.22 % (2175816)Instructions burned: 856 (million)
% 155.76/23.22 % (2175816)------------------------------
% 155.76/23.22 % (2175816)------------------------------
% 166.82/24.97 % (2175818)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:sos=all:spb=goal_then_units:urr=ec_only:sac=on:random_seed=3990027086:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2833 on theBenchmark for (2833ds/5665Mi)
% 166.82/24.97 % (2175818)Instruction limit reached!
% 166.82/24.97 % (2175818)------------------------------
% 166.82/24.97 % (2175818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.82/24.97 % (2175818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.82/24.97 % (2175818)CaDiCaL version: 2.1.3
% 166.82/24.97 % (2175818)Termination reason: Instruction limit
% 166.82/24.97 % (2175818)Termination phase: Saturation
% 166.82/24.97 % (2175818)Time elapsed: 1.808 s
% 166.82/24.97 % (2175818)Peak memory usage: 138 MB
% 166.82/24.97 % (2175818)Instructions burned: 5667 (million)
% 166.82/24.97 % (2175820)dis+1011_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:npcc=on:sos=on:lsd=20:urr=full:alpa=true:sac=on:random_seed=1739767493:i=1532:ep=RS:ss=axioms_2814 on theBenchmark for (2814ds/1532Mi)
% 166.82/24.97 % (2175596)Instruction limit reached!
% 166.82/24.97 % (2175596)------------------------------
% 166.82/24.97 % (2175596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.82/24.97 % (2175596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.82/24.97 % (2175596)CaDiCaL version: 2.1.3
% 166.82/24.97 % (2175596)Termination reason: Instruction limit
% 166.82/24.97 % (2175596)Termination phase: Saturation
% 166.82/24.97 % (2175596)Time elapsed: 5.149 s
% 166.82/24.97 % (2175596)Peak memory usage: 261 MB
% 166.82/24.97 % (2175596)Instructions burned: 13494 (million)
% 166.82/24.97 % (2175820)Refutation not found, incomplete strategy
% 166.82/24.97 % (2175820)------------------------------
% 166.82/24.97 % (2175820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.82/24.97 % (2175820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.82/24.97 % (2175820)CaDiCaL version: 2.1.3
% 166.82/24.97 % (2175820)Termination reason: Refutation not found, incomplete strategy
% 166.82/24.97 % (2175820)Time elapsed: 0.313 s
% 166.82/24.97 % (2175820)Peak memory usage: 127 MB
% 166.82/24.97 % (2175820)Instructions burned: 851 (million)
% 166.82/24.97 % (2175822)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=60557261:i=1565:sd=2:ss=axioms:sgt=32_2810 on theBenchmark for (2810ds/1565Mi)
% 166.82/24.97 % (2175820)------------------------------
% 166.82/24.97 % (2175820)------------------------------
% 166.82/24.97 % (2175824)lrs-1011_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:sims=off:bsd=on:sp=unary_first:erd=off:spb=goal:lcm=reverse:gs=on:s2agt=8:random_seed=431176076:i=1572:fgj=on:gsp=on_2808 on theBenchmark for (2808ds/1572Mi)
% 166.82/24.97 % (2175822)Instruction limit reached!
% 166.82/24.97 % (2175822)------------------------------
% 166.82/24.97 % (2175822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.82/24.97 % (2175822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.82/24.97 % (2175822)CaDiCaL version: 2.1.3
% 166.82/24.97 % (2175822)Termination reason: Instruction limit
% 166.82/24.97 % (2175822)Termination phase: Saturation
% 166.82/24.97 % (2175822)Time elapsed: 0.553 s
% 166.82/24.97 % (2175822)Peak memory usage: 135 MB
% 166.82/24.97 % (2175822)Instructions burned: 1568 (million)
% 166.82/24.97 % (2175826)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=2312786692:i=6052:sd=4:ss=axioms:sgt=24_2803 on theBenchmark for (2803ds/6052Mi)
% 166.82/24.97 % (2175824)Instruction limit reached!
% 166.82/24.97 % (2175824)------------------------------
% 166.82/24.97 % (2175824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.82/24.97 % (2175824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.82/24.97 % (2175824)CaDiCaL version: 2.1.3
% 166.82/24.97 % (2175824)Termination reason: Instruction limit
% 166.82/24.97 % (2175824)Termination phase: Saturation
% 166.82/24.97 % (2175824)Time elapsed: 0.538 s
% 166.82/24.97 % (2175824)Peak memory usage: 135 MB
% 166.82/24.97 % (2175824)Instructions burned: 1572 (million)
% 166.82/24.97 % (2175828)lrs+21_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:sos=on:erd=off:lcm=predicate:alpa=false:sac=on:random_seed=2874448319:i=3500:sd=1:bd=preordered:sup=off:ss=included_2802 on theBenchmark for (2802ds/3500Mi)
% 166.82/24.97 % (2175826)Refutation not found, incomplete strategy
% 193.09/28.55 % (2175826)------------------------------
% 193.09/28.55 % (2175826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 193.09/28.55 % (2175826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 193.09/28.55 % (2175826)CaDiCaL version: 2.1.3
% 193.09/28.55 % (2175826)Termination reason: Refutation not found, incomplete strategy
% 193.09/28.55 % (2175826)Time elapsed: 0.318 s
% 193.09/28.55 % (2175826)Peak memory usage: 127 MB
% 193.09/28.55 % (2175826)Instructions burned: 856 (million)
% 193.09/28.55 % (2175828)Refutation not found, incomplete strategy
% 193.09/28.55 % (2175828)------------------------------
% 193.09/28.55 % (2175828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 193.09/28.55 % (2175828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 193.09/28.55 % (2175828)CaDiCaL version: 2.1.3
% 193.09/28.55 % (2175828)Termination reason: Refutation not found, incomplete strategy
% 193.09/28.55 % (2175828)Time elapsed: 0.316 s
% 193.09/28.55 % (2175828)Peak memory usage: 127 MB
% 193.09/28.55 % (2175828)Instructions burned: 855 (million)
% 193.09/28.55 % (2175826)------------------------------
% 193.09/28.55 % (2175826)------------------------------
% 193.09/28.55 % (2175830)lrs+35_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:npcc=on:fde=none:sp=weighted_frequency:erd=off:spb=non_intro:updr=off:newcnf=on:random_seed=3853613640:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2797 on theBenchmark for (2797ds/1842Mi)
% 193.09/28.55 % (2175828)------------------------------
% 193.09/28.55 % (2175828)------------------------------
% 193.09/28.55 % (2175832)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1071291789:i=66096:add=on_2796 on theBenchmark for (2796ds/66096Mi)
% 193.09/28.55 % (2175830)Instruction limit reached!
% 193.09/28.55 % (2175830)------------------------------
% 193.09/28.55 % (2175830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 193.09/28.55 % (2175830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 193.09/28.55 % (2175830)CaDiCaL version: 2.1.3
% 193.09/28.55 % (2175830)Termination reason: Instruction limit
% 193.09/28.55 % (2175830)Termination phase: Saturation
% 193.09/28.55 % (2175830)Time elapsed: 0.630 s
% 193.09/28.55 % (2175830)Peak memory usage: 137 MB
% 193.09/28.55 % (2175830)Instructions burned: 1842 (million)
% 193.09/28.55 % (2175834)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=2931111515:i=1884:sd=1:nm=60:ss=axioms_2790 on theBenchmark for (2790ds/1884Mi)
% 193.09/28.55 % (2175393)Instruction limit reached!
% 193.09/28.55 % (2175393)------------------------------
% 193.09/28.55 % (2175393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 193.09/28.55 % (2175393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 193.09/28.55 % (2175393)CaDiCaL version: 2.1.3
% 193.09/28.55 % (2175393)Termination reason: Instruction limit
% 193.09/28.55 % (2175393)Termination phase: Saturation
% 193.09/28.55 % (2175393)Time elapsed: 10.450 s
% 193.09/28.55 % (2175393)Peak memory usage: 271 MB
% 193.09/28.55 % (2175393)Instructions burned: 33335 (million)
% 193.09/28.55 % (2175836)lrs-1011_4:1_sil=16000:bsr=on:random_seed=3758124045:cts=off:i=5469:bs=on:fsr=off_2788 on theBenchmark for (2788ds/5469Mi)
% 193.09/28.55 % (2175834)Instruction limit reached!
% 193.09/28.55 % (2175834)------------------------------
% 193.09/28.55 % (2175834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 193.09/28.55 % (2175834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 193.09/28.55 % (2175834)CaDiCaL version: 2.1.3
% 193.09/28.55 % (2175834)Termination reason: Instruction limit
% 193.09/28.55 % (2175834)Termination phase: Saturation
% 193.09/28.55 % (2175834)Time elapsed: 0.592 s
% 193.09/28.55 % (2175834)Peak memory usage: 138 MB
% 193.09/28.55 % (2175834)Instructions burned: 1888 (million)
% 193.09/28.55 % (2175838)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=unary_frequency:urr=on:bce=on:alpa=false:sac=on:random_seed=264584961:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2783 on theBenchmark for (2783ds/2037Mi)
% 193.09/28.55 % (2175838)Instruction limit reached!
% 193.09/28.55 % (2175838)------------------------------
% 193.09/28.55 % (2175838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 193.09/28.55 % (2175838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 193.09/28.55 % (2175838)CaDiCaL version: 2.1.3
% 193.09/28.55 % (2175838)Termination reason: Instruction limit
% 198.72/29.37 % (2175838)Termination phase: Saturation
% 198.72/29.37 % (2175838)Time elapsed: 0.708 s
% 198.72/29.37 % (2175838)Peak memory usage: 138 MB
% 198.72/29.37 % (2175838)Instructions burned: 2037 (million)
% 198.72/29.37 % (2175840)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=4040765685:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2775 on theBenchmark for (2775ds/2110Mi)
% 198.72/29.37 % (2175836)Instruction limit reached!
% 198.72/29.37 % (2175836)------------------------------
% 198.72/29.37 % (2175836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 198.72/29.37 % (2175836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.72/29.37 % (2175836)CaDiCaL version: 2.1.3
% 198.72/29.37 % (2175836)Termination reason: Instruction limit
% 198.72/29.37 % (2175836)Termination phase: Saturation
% 198.72/29.37 % (2175836)Time elapsed: 1.851 s
% 198.72/29.37 % (2175836)Peak memory usage: 131 MB
% 198.72/29.37 % (2175836)Instructions burned: 5472 (million)
% 198.72/29.37 % (2175842)dis-1010_1_anc=all_dependent:ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:lcm=reverse:fd=off:flr=on:random_seed=794952234:i=2430:add=off:aac=none:nm=16_2768 on theBenchmark for (2768ds/2430Mi)
% 198.72/29.37 % (2175840)Instruction limit reached!
% 198.72/29.37 % (2175840)------------------------------
% 198.72/29.37 % (2175840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 198.72/29.37 % (2175840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.72/29.37 % (2175840)CaDiCaL version: 2.1.3
% 198.72/29.37 % (2175840)Termination reason: Instruction limit
% 198.72/29.37 % (2175840)Termination phase: Saturation
% 198.72/29.37 % (2175840)Time elapsed: 0.721 s
% 198.72/29.37 % (2175840)Peak memory usage: 140 MB
% 198.72/29.37 % (2175840)Instructions burned: 2113 (million)
% 198.72/29.37 % (2175844)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:spb=units:acc=on:bsr=unit_only:gs=on:sac=on:random_seed=671276319:cond=fast:i=4891_2767 on theBenchmark for (2767ds/4891Mi)
% 198.72/29.37 % (2175814)Instruction limit reached!
% 198.72/29.37 % (2175814)------------------------------
% 198.72/29.37 % (2175814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 198.72/29.37 % (2175814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.72/29.37 % (2175814)CaDiCaL version: 2.1.3
% 198.72/29.37 % (2175814)Termination reason: Instruction limit
% 198.72/29.37 % (2175814)Termination phase: Saturation
% 198.72/29.37 % (2175814)Time elapsed: 8.084 s
% 198.72/29.37 % (2175814)Peak memory usage: 560 MB
% 198.72/29.37 % (2175814)Instructions burned: 26476 (million)
% 198.72/29.37 % (2175846)lrs+4_1_anc=all:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sos=on:spb=goal_then_units:lcm=reverse:gs=on:s2agt=16:sac=on:newcnf=on:random_seed=3736872191:st=2:i=14845:sd=2:ss=included:fsd=on_2764 on theBenchmark for (2764ds/14845Mi)
% 198.72/29.37 % (2175846)Refutation not found, incomplete strategy
% 198.72/29.37 % (2175846)------------------------------
% 198.72/29.37 % (2175846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 198.72/29.37 % (2175846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.72/29.37 % (2175846)CaDiCaL version: 2.1.3
% 198.72/29.37 % (2175846)Termination reason: Refutation not found, incomplete strategy
% 198.72/29.37 % (2175846)Time elapsed: 0.324 s
% 198.72/29.37 % (2175846)Peak memory usage: 128 MB
% 198.72/29.37 % (2175846)Instructions burned: 887 (million)
% 198.72/29.37 % (2175842)Instruction limit reached!
% 198.72/29.37 % (2175842)------------------------------
% 198.72/29.37 % (2175842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 198.72/29.37 % (2175842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.72/29.37 % (2175842)CaDiCaL version: 2.1.3
% 198.72/29.37 % (2175842)Termination reason: Instruction limit
% 198.72/29.37 % (2175842)Termination phase: Saturation
% 198.72/29.37 % (2175842)Time elapsed: 0.788 s
% 198.72/29.37 % (2175842)Peak memory usage: 143 MB
% 198.72/29.37 % (2175842)Instructions burned: 2430 (million)
% 198.72/29.37 % (2175846)------------------------------
% 198.72/29.37 % (2175846)------------------------------
% 198.72/29.37 % (2175848)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=2872737045:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2759 on theBenchmark for (2759ds/7534Mi)
% 198.72/29.37 % (2175849)lrs-1002_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=ground:npcc=on:prc=on:fde=none:sims=off:spb=goal:bsr=unit_only:s2agt=32:random_seed=2452982728:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2759 on theBenchmark for (2759ds/10353Mi)
% 228.23/33.50 % (2175844)Instruction limit reached!
% 228.23/33.50 % (2175844)------------------------------
% 228.23/33.50 % (2175844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 228.23/33.50 % (2175844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.23/33.50 % (2175844)CaDiCaL version: 2.1.3
% 228.23/33.50 % (2175844)Termination reason: Instruction limit
% 228.23/33.50 % (2175844)Termination phase: Saturation
% 228.23/33.50 % (2175844)Time elapsed: 1.651 s
% 228.23/33.50 % (2175844)Peak memory usage: 166 MB
% 228.23/33.50 % (2175844)Instructions burned: 4893 (million)
% 228.23/33.50 % (2175852)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1812896836:i=7860_2749 on theBenchmark for (2749ds/7860Mi)
% 228.23/33.50 % (2175852)Refutation not found, incomplete strategy
% 228.23/33.50 % (2175852)------------------------------
% 228.23/33.50 % (2175852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 228.23/33.50 % (2175852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.23/33.50 % (2175852)CaDiCaL version: 2.1.3
% 228.23/33.50 % (2175852)Termination reason: Refutation not found, incomplete strategy
% 228.23/33.50 % (2175852)Time elapsed: 0.001 s
% 228.23/33.50 % (2175852)Peak memory usage: 88 MB
% 228.23/33.50 % (2175852)------------------------------
% 228.23/33.50 % (2175852)------------------------------
% 228.23/33.50 % (2175854)ott+1011_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:fde=unused:spb=goal:lsd=30:lcm=predicate:fd=off:gs=on:sac=on:random_seed=4129040767:i=7896:sd=2:bs=on:ss=included:sgt=20_2747 on theBenchmark for (2747ds/7896Mi)
% 228.23/33.50 % (2175808)Instruction limit reached!
% 228.23/33.50 % (2175808)------------------------------
% 228.23/33.50 % (2175808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 228.23/33.50 % (2175808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.23/33.50 % (2175808)CaDiCaL version: 2.1.3
% 228.23/33.50 % (2175808)Termination reason: Instruction limit
% 228.23/33.50 % (2175808)Termination phase: Saturation
% 228.23/33.50 % (2175808)Time elapsed: 10.943 s
% 228.23/33.50 % (2175808)Peak memory usage: 368 MB
% 228.23/33.50 % (2175808)Instructions burned: 30754 (million)
% 228.23/33.50 % (2175856)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=2455766296:i=5812:gtgl=2:gtg=all_2739 on theBenchmark for (2739ds/5812Mi)
% 228.23/33.50 % (2175848)Instruction limit reached!
% 228.23/33.50 % (2175848)------------------------------
% 228.23/33.50 % (2175848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 228.23/33.50 % (2175848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.23/33.50 % (2175848)CaDiCaL version: 2.1.3
% 228.23/33.50 % (2175848)Termination reason: Instruction limit
% 228.23/33.50 % (2175848)Termination phase: Saturation
% 228.23/33.50 % (2175848)Time elapsed: 2.104 s
% 228.23/33.50 % (2175848)Peak memory usage: 149 MB
% 228.23/33.50 % (2175848)Instructions burned: 7535 (million)
% 228.23/33.50 % (2175858)ott-1011_1_anc=none:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:sp=const_frequency:sos=on:lsd=100:random_seed=2948304232:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2737 on theBenchmark for (2737ds/2965Mi)
% 228.23/33.50 % (2175858)Refutation not found, incomplete strategy
% 228.23/33.50 % (2175858)------------------------------
% 228.23/33.50 % (2175858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 228.23/33.50 % (2175858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.23/33.50 % (2175858)CaDiCaL version: 2.1.3
% 228.23/33.50 % (2175858)Termination reason: Refutation not found, incomplete strategy
% 228.23/33.50 % (2175858)Time elapsed: 0.316 s
% 228.23/33.50 % (2175858)Peak memory usage: 127 MB
% 228.23/33.50 % (2175858)Instructions burned: 856 (million)
% 228.23/33.50 % (2175858)------------------------------
% 228.23/33.50 % (2175858)------------------------------
% 228.23/33.50 % (2175860)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=4271034782:i=2967:kws=precedence:bd=preordered:av=off_2731 on theBenchmark for (2731ds/2967Mi)
% 228.23/33.50 % (2175849)Instruction limit reached!
% 228.23/33.50 % (2175849)------------------------------
% 228.23/33.50 % (2175849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 180.38/39.04 % (2175849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.38/39.04 % (2175849)CaDiCaL version: 2.1.3
% 180.38/39.04 % (2175849)Termination reason: Instruction limit
% 180.38/39.04 % (2175849)Termination phase: Saturation
% 180.38/39.04 % (2175849)Time elapsed: 3.583 s
% 180.38/39.04 % (2175849)Peak memory usage: 224 MB
% 180.38/39.04 % (2175849)Instructions burned: 10356 (million)
% 180.38/39.04 % (2175862)ott+1002_1_anc=all:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:sos=on:spb=goal_then_units:alpa=false:sac=on:random_seed=503088567:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2722 on theBenchmark for (2722ds/3022Mi)
% 180.38/39.04 % (2175854)Instruction limit reached!
% 180.38/39.04 % (2175854)------------------------------
% 180.38/39.04 % (2175854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 180.38/39.04 % (2175854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.38/39.04 % (2175854)CaDiCaL version: 2.1.3
% 180.38/39.04 % (2175854)Termination reason: Instruction limit
% 180.38/39.04 % (2175854)Termination phase: Saturation
% 180.38/39.04 % (2175854)Time elapsed: 2.534 s
% 180.38/39.04 % (2175854)Peak memory usage: 180 MB
% 180.38/39.04 % (2175854)Instructions burned: 7898 (million)
% 180.38/39.04 % (2175860)Instruction limit reached!
% 180.38/39.04 % (2175860)------------------------------
% 180.38/39.04 % (2175860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 180.38/39.04 % (2175860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.38/39.04 % (2175860)CaDiCaL version: 2.1.3
% 180.38/39.04 % (2175860)Termination reason: Instruction limit
% 180.38/39.04 % (2175860)Termination phase: Saturation
% 180.38/39.04 % (2175860)Time elapsed: 1.026 s
% 180.38/39.04 % (2175860)Peak memory usage: 148 MB
% 180.38/39.04 % (2175860)Instructions burned: 2967 (million)
% 180.38/39.04 % (2175864)lrs-1010_1_ncem=casc2026/models/loop4.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=const_frequency:sos=all:lcm=predicate:acc=on:bsr=unit_only:gs=on:sac=on:newcnf=on:random_seed=699711226:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2720 on theBenchmark for (2720ds/3207Mi)
% 180.38/39.04 % (2175865)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=3625030160:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2720 on theBenchmark for (2720ds/3289Mi)
% 180.38/39.04 % (2175856)Instruction limit reached!
% 180.38/39.04 % (2175856)------------------------------
% 180.38/39.04 % (2175856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 180.38/39.04 % (2175856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.38/39.04 % (2175856)CaDiCaL version: 2.1.3
% 180.38/39.04 % (2175856)Termination reason: Instruction limit
% 180.38/39.04 % (2175856)Termination phase: Saturation
% 180.38/39.04 % (2175856)Time elapsed: 1.986 s
% 180.38/39.04 % (2175856)Peak memory usage: 183 MB
% 180.38/39.04 % (2175856)Instructions burned: 5813 (million)
% 180.38/39.04 % (2175868)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=2895950978:i=38569:sd=3:ss=axioms:sgt=32_2718 on theBenchmark for (2718ds/38569Mi)
% 180.38/39.04 % (2175864)Refutation not found, incomplete strategy
% 180.38/39.04 % (2175864)------------------------------
% 180.38/39.04 % (2175864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 180.38/39.04 % (2175864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.38/39.04 % (2175864)CaDiCaL version: 2.1.3
% 180.38/39.04 % (2175864)Termination reason: Refutation not found, incomplete strategy
% 180.38/39.04 % (2175864)Time elapsed: 0.316 s
% 180.38/39.04 % (2175864)Peak memory usage: 127 MB
% 180.38/39.04 % (2175864)Instructions burned: 851 (million)
% 180.38/39.04 % (2175865)Refutation not found, incomplete strategy
% 180.38/39.04 % (2175865)------------------------------
% 180.38/39.04 % (2175865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 180.38/39.04 % (2175865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.38/39.04 % (2175865)CaDiCaL version: 2.1.3
% 180.38/39.04 % (2175865)Termination reason: Refutation not found, incomplete strategy
% 180.38/39.04 % (2175865)Time elapsed: 0.322 s
% 180.38/39.04 % (2175865)Peak memory usage: 128 MB
% 180.38/39.04 % (2175865)Instructions burned: 859 (million)
% 180.38/39.04 % (2175864)------------------------------
% 180.38/39.04 % (2175864)------------------------------
% 180.38/39.04 % (2175865)------------------------------
% 180.38/39.04 % (2175865)------------------------------
% 180.38/39.04 % (2175873)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=arity:spb=intro:lcm=reverse:urr=ec_only:fd=preordered:gs=on:sac=on:random_seed=146836875:i=33824:bd=preordered_2714 on theBenchmark for (2714ds/33824Mi)
% 180.38/39.04 % (2175872)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=2747261260:cts=off:i=3394_2715 on theBenchmark for (2715ds/3394Mi)
% 180.38/39.04 % (2175862)Instruction limit reached!
% 180.38/39.04 % (2175862)------------------------------
% 180.38/39.04 % (2175862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 180.38/39.04 % (2175862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.38/39.04 % (2175862)CaDiCaL version: 2.1.3
% 180.38/39.04 % (2175862)Termination reason: Instruction limit
% 180.38/39.04 % (2175862)Termination phase: Saturation
% 180.38/39.04 % (2175862)Time elapsed: 0.913 s
% 180.38/39.04 % (2175862)Peak memory usage: 133 MB
% 180.38/39.04 % (2175862)Instructions burned: 3024 (million)
% 180.38/39.04 % (2175893)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=1313230588:i=20684:bd=all:gtg=exists_sym_2711 on theBenchmark for (2711ds/20684Mi)
% 180.38/39.04 % (2175872)Instruction limit reached!
% 180.38/39.04 % (2175872)------------------------------
% 180.38/39.04 % (2175872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 180.38/39.04 % (2175872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.38/39.04 % (2175872)CaDiCaL version: 2.1.3
% 180.38/39.04 % (2175872)Termination reason: Instruction limit
% 180.38/39.04 % (2175872)Termination phase: Saturation
% 180.38/39.04 % (2175872)Time elapsed: 1.123 s
% 180.38/39.04 % (2175872)Peak memory usage: 150 MB
% 180.38/39.04 % (2175872)Instructions burned: 3395 (million)
% 180.38/39.04 % (2175947)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:irw=on:npcc=on:prc=on:bsd=on:sp=reverse_frequency:sos=on:erd=off:spb=goal:lcm=reverse:urr=full:bsr=on:s2agt=32:alpa=random:kmz=on:random_seed=802952680:st=3:prac=on:i=7222:kws=arity_squared:add=on:fgj=on:bd=preordered:gtg=exists_top:gsp=on:ss=axioms:er=known:sgt=8:proc=on_2702 on theBenchmark for (2702ds/7222Mi)
% 180.38/39.04 % (2175947)Refutation not found, incomplete strategy
% 180.38/39.04 % (2175947)------------------------------
% 180.38/39.04 % (2175947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 180.38/39.04 % (2175947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.38/39.04 % (2175947)CaDiCaL version: 2.1.3
% 180.38/39.04 % (2175947)Termination reason: Refutation not found, incomplete strategy
% 180.38/39.04 % (2175947)Time elapsed: 0.315 s
% 180.38/39.04 % (2175947)Peak memory usage: 128 MB
% 180.38/39.04 % (2175947)Instructions burned: 856 (million)
% 180.38/39.04 % (2175947)------------------------------
% 180.38/39.04 % (2175947)------------------------------
% 180.38/39.04 % (2175957)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=1372441469:st=4:i=7295:sd=4:ep=R:ss=axioms_2696 on theBenchmark for (2696ds/7295Mi)
% 180.38/39.04 % (2175957)Refutation not found, incomplete strategy
% 180.38/39.04 % (2175957)------------------------------
% 180.38/39.04 % (2175957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 180.38/39.04 % (2175957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.38/39.04 % (2175957)CaDiCaL version: 2.1.3
% 180.38/39.04 % (2175957)Termination reason: Refutation not found, incomplete strategy
% 180.38/39.04 % (2175957)Time elapsed: 0.319 s
% 180.38/39.04 % (2175957)Peak memory usage: 127 MB
% 180.38/39.04 % (2175957)Instructions burned: 857 (million)
% 180.38/39.04 % (2175957)------------------------------
% 180.38/39.04 % (2175957)------------------------------
% 180.38/39.04 % (2176001)lrs+32_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:fde=none:sp=occurrence:urr=ec_only:fd=preordered:random_seed=3056223077:i=4036:ins=10_2691 on theBenchmark for (2691ds/4036Mi)
% 180.38/39.04 % (2176001)Instruction limit reached!
% 180.38/39.04 % (2176001)------------------------------
% 180.38/39.04 % (2176001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 180.38/39.04 % (2176001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.38/39.04 % (2176001)CaDiCaL version: 2.1.3
% 180.38/39.04 % (2176001)Termination reason: Instruction limit
% 180.38/39.04 % (2176001)Termination phase: Saturation
% 180.38/39.04 % (2176001)Time elapsed: 1.645 s
% 180.38/39.04 % (2176001)Peak memory usage: 185 MB
% 180.38/39.04 % (2176001)Instructions burned: 4036 (million)
% 180.38/39.04 % (2176007)lrs+10_1_sil=128000:lcm=predicate:random_seed=4053951035:st=3:i=43697:sd=5:ss=axioms_2673 on theBenchmark for (2673ds/43697Mi)
% 180.38/39.04 % (2175893)Instruction limit reached!
% 180.38/39.04 % (2175893)------------------------------
% 180.38/39.04 % (2175893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 180.38/39.04 % (2175893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.38/39.04 % (2175893)CaDiCaL version: 2.1.3
% 180.38/39.04 % (2175893)Termination reason: Instruction limit
% 180.38/39.04 % (2175893)Termination phase: Saturation
% 180.38/39.04 % (2175893)Time elapsed: 7.404 s
% 180.38/39.04 % (2175893)Peak memory usage: 281 MB
% 180.38/39.04 % (2175893)Instructions burned: 20684 (million)
% 180.38/39.04 % (2176095)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:sp=const_frequency:sos=all:lcm=predicate:urr=on:s2agt=20:sac=on:random_seed=4018870535:i=17599:gtg=all:ss=axioms:fsd=on_2636 on theBenchmark for (2636ds/17599Mi)
% 180.38/39.04 % (2176095)Refutation not found, incomplete strategy
% 180.38/39.04 % (2176095)------------------------------
% 180.38/39.04 % (2176095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 180.38/39.04 % (2176095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.38/39.04 % (2176095)CaDiCaL version: 2.1.3
% 180.38/39.04 % (2176095)Termination reason: Refutation not found, incomplete strategy
% 180.38/39.04 % (2176095)Time elapsed: 0.320 s
% 180.38/39.04 % (2176095)Peak memory usage: 128 MB
% 180.38/39.04 % (2176095)Instructions burned: 854 (million)
% 180.38/39.04 % (2176095)------------------------------
% 180.38/39.04 % (2176095)------------------------------
% 180.38/39.04 % (2176097)lrs+1011_1_to=lpo:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:sp=occurrence:lcm=reverse:urr=ec_only:gs=on:random_seed=3358154669:i=4547:bd=preordered_2630 on theBenchmark for (2630ds/4547Mi)
% 180.38/39.04 % (2176097)First to succeed.
% 180.38/39.04 % (2176097)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2175108"
% 180.38/39.04 % (2176097)Refutation found. Thanks to Tanya!
% 180.38/39.04 % SZS status Theorem for theBenchmark
% 180.38/39.04 % SZS output start Proof for theBenchmark
% See solution above
% 267.23/39.13 % (2176097)------------------------------
% 267.23/39.13 % (2176097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 267.23/39.13 % (2176097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 267.23/39.13 % (2176097)CaDiCaL version: 2.1.3
% 267.23/39.13 % (2176097)Termination reason: Refutation
% 267.23/39.13 % (2176097)Time elapsed: 1.013 s
% 267.23/39.13 % (2176097)Peak memory usage: 143 MB
% 267.23/39.13 % (2176097)Instructions burned: 3539 (million)
% 267.23/39.13 % (2176097)------------------------------
% 267.23/39.13 % (2176097)------------------------------
% 267.23/39.13 % (2175108)Success in time 38.269 s
% 267.23/39.13 % Vampire exiting
%------------------------------------------------------------------------------