%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : KLE176+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:40:33 AM UTC 2026
% Result : Satisfiable 14.67s 3.31s
% Output : Saturation 17.94s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u192,axiom,
zero = c(zero) ).
cnf(u196,axiom,
one = sK0(zero) ).
cnf(u205,axiom,
test(zero) ).
cnf(u210,axiom,
complement(one,zero) ).
cnf(u404,axiom,
multiplication(X0,addition(one,multiplication(star(zero),star(star(zero))))) = X0 ).
cnf(u181,axiom,
( one = addition(X0,sK0(X0))
| zero = c(X0) ) ).
cnf(u984,axiom,
( zero != X0
| complement(zero,X0) ) ).
cnf(u988,axiom,
( leq(multiplication(X0,star(X1)),X0)
| ~ leq(multiplication(X0,X1),X0) ) ).
cnf(u578,axiom,
( leq(multiplication(X0,multiplication(X1,multiplication(X2,star(X1)))),X0)
| ~ leq(multiplication(X0,multiplication(X1,addition(one,X2))),X0) ) ).
cnf(u58,axiom,
( ~ complement(X1,X0)
| test(X0) ) ).
cnf(u1486,axiom,
test(X0) ).
cnf(u766,axiom,
( ~ leq(multiplication(addition(X0,X1),multiplication(X2,X3)),multiplication(X0,X2))
| leq(multiplication(X1,multiplication(X2,multiplication(X3,star(X3)))),multiplication(X0,X2)) ) ).
cnf(u66,axiom,
( ~ test(X1)
| ~ test(X0)
| c(addition(X0,X1)) = multiplication(c(X0),c(X1)) ) ).
cnf(u94,axiom,
( ~ leq(multiplication(X0,X1),X0)
| addition(X0,multiplication(X0,multiplication(X1,star(X1)))) = X0 ) ).
cnf(u549,axiom,
( ~ leq(multiplication(X0,addition(one,X1)),X0)
| leq(multiplication(X0,star(X1)),X0) ) ).
cnf(u986,axiom,
multiplication(X0,multiplication(star(star(zero)),star(zero))) = X0 ).
cnf(u430,axiom,
multiplication(X0,addition(one,X1)) = multiplication(X0,addition(one,addition(multiplication(star(zero),star(star(zero))),X1))) ).
cnf(u442,axiom,
zero = c(one) ).
cnf(u257,axiom,
multiplication(X0,addition(one,X1)) = multiplication(X0,addition(one,addition(multiplication(star(one),star(one)),X1))) ).
cnf(u49,axiom,
zero = multiplication(X0,zero) ).
cnf(u653,axiom,
( one != addition(X0,c(X0))
| complement(c(X0),X0)
| zero = c(X0) ) ).
cnf(u81,axiom,
( ~ leq(addition(X0,X1),X0)
| leq(multiplication(X1,star(one)),X0) ) ).
cnf(u489,axiom,
( zero = multiplication(X0,multiplication(c(X0),X1))
| zero = c(X0) ) ).
cnf(u153,axiom,
( multiplication(X0,X1) != multiplication(X0,addition(X1,X2))
| leq(multiplication(X0,X2),multiplication(X0,X1)) ) ).
cnf(u40,axiom,
addition(X0,X1) = addition(X1,X0) ).
cnf(u213,axiom,
( test(c(X0))
| ~ test(X0) ) ).
cnf(u172,axiom,
( ~ leq(multiplication(X1,X0),X1)
| multiplication(X1,addition(one,multiplication(X0,star(X0)))) = X1 ) ).
cnf(u797,axiom,
( ~ leq(X0,X1)
| addition(X1,multiplication(c(X1),multiplication(X0,star(X0)))) = X1
| zero = c(X1) ) ).
cnf(u283,axiom,
( leq(multiplication(X3,multiplication(X0,multiplication(X1,star(X2)))),X3)
| ~ leq(multiplication(X3,addition(X2,multiplication(X0,X1))),X3) ) ).
cnf(u216,axiom,
leq(star(one),one) ).
cnf(u947,axiom,
( leq(multiplication(X0,star(X1)),zero)
| ~ leq(X0,zero) ) ).
cnf(u459,axiom,
leq(one,star(one)) ).
cnf(u1181,axiom,
( complement(X0,zero)
| ~ test(X0) ) ).
cnf(u302,axiom,
( leq(multiplication(X0,star(one)),sK0(X0))
| ~ leq(one,sK0(X0))
| zero = c(X0) ) ).
cnf(u70,axiom,
( addition(X0,X1) != X0
| leq(X1,X0) ) ).
cnf(u779,axiom,
( leq(multiplication(c(multiplication(X0,X1)),star(X1)),X0)
| ~ leq(one,X0)
| zero = c(multiplication(X0,X1)) ) ).
cnf(u142,axiom,
multiplication(X0,addition(one,X1)) = addition(X0,multiplication(X0,X1)) ).
cnf(u597,axiom,
leq(multiplication(X0,star(multiplication(star(one),star(star(one))))),X0) ).
cnf(u977,axiom,
( zero != X0
| complement(X0,zero) ) ).
cnf(u490,axiom,
( multiplication(X0,addition(one,multiplication(c(X0),star(c(X0))))) = X0
| zero = c(X0) ) ).
cnf(u55,axiom,
( ~ leq(addition(multiplication(X0,X1),X2),X1)
| leq(multiplication(star(X0),X2),X1) ) ).
cnf(u493,axiom,
multiplication(X0,addition(one,multiplication(star(one),multiplication(star(star(one)),star(multiplication(star(one),star(star(one)))))))) = X0 ).
cnf(u157,axiom,
( ~ leq(multiplication(X0,addition(X1,X2)),multiplication(X0,X1))
| leq(multiplication(X0,multiplication(X2,star(one))),multiplication(X0,X1)) ) ).
cnf(u44,axiom,
multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2) ).
cnf(u88,axiom,
( leq(multiplication(X0,multiplication(X1,star(X1))),X0)
| ~ leq(multiplication(X0,X1),X0) ) ).
cnf(u116,axiom,
( ~ test(X0)
| one = addition(X0,sK0(X0)) ) ).
cnf(u324,axiom,
( ~ leq(multiplication(X0,multiplication(X1,X2)),multiplication(X0,X1))
| multiplication(X0,X1) = multiplication(X0,multiplication(X1,addition(one,multiplication(X2,star(X2))))) ) ).
cnf(u259,axiom,
multiplication(X0,addition(one,multiplication(star(one),multiplication(star(one),star(one))))) = X0 ).
cnf(u51,axiom,
( ~ leq(X0,X1)
| addition(X0,X1) = X1 ) ).
cnf(u239,axiom,
( one != addition(one,addition(star(one),X0))
| complement(X0,one)
| zero != X0 ) ).
cnf(u700,axiom,
( ~ leq(multiplication(X3,multiplication(addition(X0,X1),X2)),X3)
| multiplication(X3,addition(one,multiplication(X1,multiplication(X2,star(multiplication(X0,X2)))))) = X3 ) ).
cnf(u732,axiom,
( ~ leq(addition(X1,X0),X1)
| leq(multiplication(X0,multiplication(star(zero),star(star(zero)))),X1) ) ).
cnf(u908,axiom,
multiplication(X0,addition(one,X1)) = multiplication(X0,addition(one,addition(multiplication(star(star(one)),star(one)),X1))) ).
cnf(u767,axiom,
( ~ leq(multiplication(X0,multiplication(addition(X1,X2),X3)),multiplication(X0,X1))
| leq(multiplication(X0,multiplication(X2,multiplication(X3,star(X3)))),multiplication(X0,X1)) ) ).
cnf(u802,axiom,
leq(multiplication(X0,multiplication(X1,star(star(one)))),multiplication(X0,X1)) ).
cnf(u227,axiom,
one = addition(one,star(one)) ).
cnf(u695,axiom,
( multiplication(X1,X2) != multiplication(addition(X0,X1),X2)
| leq(multiplication(X0,X2),multiplication(X1,X2)) ) ).
cnf(u730,axiom,
multiplication(X0,multiplication(addition(one,X1),X1)) = multiplication(X0,multiplication(X1,addition(one,X1))) ).
cnf(u758,axiom,
( leq(multiplication(sK0(X0),multiplication(X1,star(X1))),X0)
| ~ leq(X1,X0)
| zero = c(X0) ) ).
cnf(u186,axiom,
( one != sK0(X0)
| leq(X0,sK0(X0))
| zero = c(X0) ) ).
cnf(u513,axiom,
multiplication(X0,addition(one,multiplication(star(zero),multiplication(star(star(zero)),star(multiplication(star(zero),star(star(zero)))))))) = X0 ).
cnf(u305,axiom,
( ~ leq(multiplication(X0,addition(X1,X2)),multiplication(X0,X2))
| leq(multiplication(X0,multiplication(X1,star(one))),multiplication(X0,X2)) ) ).
cnf(u909,axiom,
multiplication(X0,addition(one,multiplication(star(star(one)),multiplication(star(one),star(one))))) = X0 ).
cnf(u701,axiom,
( ~ leq(multiplication(addition(X0,X1),X2),multiplication(X1,X2))
| leq(multiplication(X0,multiplication(X2,star(one))),multiplication(X1,X2)) ) ).
cnf(u365,axiom,
multiplication(X0,addition(one,multiplication(star(one),multiplication(star(star(one)),star(one))))) = X0 ).
cnf(u981,axiom,
leq(multiplication(X0,star(star(zero))),X0) ).
cnf(u559,axiom,
( ~ leq(multiplication(X2,multiplication(X0,addition(one,X1))),X2)
| multiplication(X2,addition(one,multiplication(X0,multiplication(X1,star(X0))))) = X2 ) ).
cnf(u705,axiom,
( ~ leq(multiplication(addition(X0,X1),X2),X0)
| leq(multiplication(X1,multiplication(X2,star(X2))),X0) ) ).
cnf(u719,axiom,
( multiplication(addition(X0,X1),c(X0)) = multiplication(X1,c(X0))
| zero = c(X0) ) ).
cnf(u657,axiom,
( zero = multiplication(c(X0),multiplication(X0,X1))
| zero = c(X0) ) ).
cnf(u385,axiom,
( leq(multiplication(X0,star(zero)),X1)
| ~ leq(X0,X1) ) ).
cnf(u92,axiom,
( leq(multiplication(X0,star(X0)),one)
| ~ leq(X0,one) ) ).
cnf(u435,axiom,
( one != addition(one,addition(multiplication(star(zero),star(star(zero))),X0))
| complement(X0,one)
| zero != X0 ) ).
cnf(u478,axiom,
( zero = multiplication(X0,multiplication(X1,c(multiplication(X0,X1))))
| zero = c(multiplication(X0,X1)) ) ).
cnf(u159,axiom,
( leq(multiplication(X0,multiplication(X2,star(X1))),X0)
| ~ leq(multiplication(X0,addition(X1,X2)),X0) ) ).
cnf(u171,axiom,
( ~ leq(multiplication(X2,addition(X0,X1)),X2)
| multiplication(X2,addition(one,multiplication(X0,star(X1)))) = X2 ) ).
cnf(u82,axiom,
( leq(multiplication(X1,star(X0)),one)
| ~ leq(addition(X0,X1),one) ) ).
cnf(u118,axiom,
( ~ test(X0)
| one = addition(X0,c(X0)) ) ).
cnf(u793,axiom,
( leq(multiplication(c(X2),multiplication(X0,multiplication(X1,star(multiplication(X0,X1))))),X2)
| ~ leq(multiplication(X0,X1),X2)
| zero = c(X2) ) ).
cnf(u853,axiom,
multiplication(X0,addition(one,X1)) = multiplication(X0,addition(one,addition(star(star(one)),X1))) ).
cnf(u969,axiom,
multiplication(X0,zero) = X0 ).
cnf(u177,axiom,
( ~ leq(addition(X0,X1),one)
| one = addition(one,multiplication(X1,star(X0))) ) ).
cnf(u1218,axiom,
complement(X0,zero) ).
cnf(u882,axiom,
one = addition(one,multiplication(star(star(one)),star(one))) ).
cnf(u885,axiom,
zero = c(addition(one,multiplication(star(star(one)),star(one)))) ).
cnf(u68,axiom,
( complement(X0,c(X0))
| ~ test(X0) ) ).
cnf(u80,axiom,
( ~ test(X0)
| zero = multiplication(X0,sK0(X0)) ) ).
cnf(u200,axiom,
( multiplication(X0,addition(one,multiplication(sK0(X1),star(X1)))) = X0
| zero = c(X1) ) ).
cnf(u768,axiom,
( leq(multiplication(X0,multiplication(X1,multiplication(X2,star(X2)))),X0)
| ~ leq(multiplication(X0,multiplication(addition(one,X1),X2)),X0) ) ).
cnf(u43,axiom,
addition(X0,X0) = X0 ).
cnf(u488,axiom,
( multiplication(X0,X1) = multiplication(X0,addition(c(X0),X1))
| zero = c(X0) ) ).
cnf(u791,axiom,
complement(zero,zero) ).
cnf(u1000,axiom,
zero = X0 ).
cnf(u900,axiom,
leq(multiplication(X0,star(multiplication(star(star(one)),star(one)))),X0) ).
cnf(u62,axiom,
( zero != multiplication(X1,X0)
| zero != multiplication(X0,X1)
| complement(X1,X0)
| addition(X0,X1) != one ) ).
cnf(u650,axiom,
( c(X0) = multiplication(c(X0),addition(one,X0))
| zero = c(X0) ) ).
cnf(u282,axiom,
( leq(multiplication(X2,multiplication(X0,multiplication(X1,star(multiplication(X0,X1))))),X2)
| ~ leq(multiplication(X2,multiplication(X0,X1)),X2) ) ).
cnf(u41,axiom,
addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0) ).
cnf(u285,axiom,
( leq(multiplication(X0,multiplication(X1,multiplication(X2,star(X3)))),multiplication(X0,X1))
| ~ leq(multiplication(X0,multiplication(X1,addition(X3,X2))),multiplication(X0,X1)) ) ).
cnf(u273,axiom,
( one != addition(X2,multiplication(X0,X1))
| zero != multiplication(X2,multiplication(X0,X1))
| complement(multiplication(X0,X1),X2)
| zero != multiplication(X0,multiplication(X1,X2)) ) ).
cnf(u401,axiom,
( leq(star(zero),X0)
| ~ leq(one,X0) ) ).
cnf(u680,axiom,
multiplication(addition(X3,multiplication(X0,X1)),X2) = addition(multiplication(X3,X2),multiplication(X0,multiplication(X1,X2))) ).
cnf(u184,axiom,
( leq(multiplication(sK0(X0),star(one)),X0)
| ~ leq(one,X0)
| zero = c(X0) ) ).
cnf(u84,axiom,
( ~ leq(addition(X0,multiplication(X1,X2)),X1)
| leq(multiplication(X0,star(X2)),X1) ) ).
cnf(u828,axiom,
leq(addition(one,star(addition(one,star(star(one))))),star(addition(one,star(star(one))))) ).
cnf(u643,axiom,
( leq(multiplication(c(addition(one,X0)),star(X0)),c(addition(one,X0)))
| zero = c(addition(one,X0)) ) ).
cnf(u596,axiom,
leq(multiplication(X0,star(multiplication(star(zero),star(star(zero))))),X0) ).
cnf(u1048,axiom,
leq(X1,X0) ).
cnf(u860,axiom,
( one != addition(one,addition(star(star(one)),X0))
| complement(X0,one)
| zero != X0 ) ).
cnf(u79,axiom,
( ~ test(X0)
| zero = multiplication(sK0(X0),X0) ) ).
cnf(u522,axiom,
( ~ leq(multiplication(X0,addition(X2,X1)),X0)
| multiplication(X0,addition(one,multiplication(X1,multiplication(star(X2),multiplication(star(multiplication(X1,star(X2))),star(multiplication(X1,multiplication(star(X2),star(multiplication(X1,star(X2))))))))))) = X0 ) ).
cnf(u550,axiom,
( multiplication(X0,X1) != multiplication(X0,addition(one,X1))
| leq(X0,multiplication(X0,X1)) ) ).
cnf(u487,axiom,
( multiplication(X0,X1) = multiplication(X0,addition(X1,c(X0)))
| zero = c(X0) ) ).
cnf(u60,axiom,
( ~ complement(X1,X0)
| zero = multiplication(X1,X0) ) ).
cnf(u603,axiom,
( zero = multiplication(c(X0),X0)
| zero = c(X0) ) ).
cnf(u770,axiom,
( one = addition(X0,c(X0))
| zero = c(X0) ) ).
cnf(u553,axiom,
( ~ leq(multiplication(X0,addition(one,X1)),multiplication(X0,X1))
| leq(multiplication(X0,star(one)),multiplication(X0,X1)) ) ).
cnf(u958,axiom,
( one != X0
| complement(zero,X0) ) ).
cnf(u773,axiom,
( one != X0
| leq(c(X0),X0)
| zero = c(X0) ) ).
cnf(u154,axiom,
( multiplication(X0,addition(X1,X2)) != multiplication(X0,X2)
| leq(multiplication(X0,X1),multiplication(X0,X2)) ) ).
cnf(u330,axiom,
( ~ leq(multiplication(X0,X1),X0)
| multiplication(X0,addition(one,multiplication(X1,multiplication(star(X1),star(multiplication(X1,star(X1))))))) = X0 ) ).
cnf(u53,axiom,
leq(addition(one,multiplication(X0,star(X0))),star(X0)) ).
cnf(u97,axiom,
( ~ test(X0)
| zero = multiplication(X0,c(X0)) ) ).
cnf(u125,axiom,
( ~ test(sK0(X0))
| c(sK0(X0)) = X0
| ~ test(X0) ) ).
cnf(u505,axiom,
( ~ leq(X0,one)
| one = addition(one,multiplication(X0,multiplication(star(X0),star(multiplication(X0,star(X0)))))) ) ).
cnf(u169,axiom,
( ~ leq(multiplication(X0,addition(X1,X2)),X0)
| multiplication(X0,addition(one,multiplication(X2,star(X1)))) = X0 ) ).
cnf(u56,axiom,
( ~ leq(addition(multiplication(X0,X1),X2),X0)
| leq(multiplication(X2,star(X1)),X0) ) ).
cnf(u364,axiom,
multiplication(X0,addition(one,X1)) = multiplication(X0,addition(one,addition(multiplication(star(one),star(star(one))),X1))) ).
cnf(u287,axiom,
( ~ leq(multiplication(X0,multiplication(X1,addition(X2,X3))),multiplication(X0,X1))
| multiplication(X0,X1) = multiplication(X0,multiplication(X1,addition(one,multiplication(X3,star(X2))))) ) ).
cnf(u67,axiom,
( ~ test(X1)
| ~ test(X0)
| c(multiplication(X0,X1)) = addition(c(X0),c(X1)) ) ).
cnf(u830,axiom,
zero = c(addition(one,star(star(one)))) ).
cnf(u992,axiom,
multiplication(X0,star(zero)) = X0 ).
cnf(u598,axiom,
leq(multiplication(X0,star(multiplication(star(one),star(one)))),X0) ).
cnf(u987,axiom,
multiplication(X0,star(star(zero))) = X0 ).
cnf(u711,axiom,
( multiplication(addition(X0,X1),c(X1)) = multiplication(X0,c(X1))
| zero = c(X1) ) ).
cnf(u158,axiom,
( leq(multiplication(X0,multiplication(X1,star(X2))),X0)
| ~ leq(multiplication(X0,addition(X1,X2)),X0) ) ).
cnf(u1067,axiom,
X0 = X1 ).
cnf(u993,axiom,
leq(multiplication(star(X0),X0),star(X0)) ).
cnf(u506,axiom,
( multiplication(X0,addition(one,multiplication(c(X0),multiplication(star(c(X0)),star(multiplication(c(X0),star(c(X0)))))))) = X0
| zero = c(X0) ) ).
cnf(u321,axiom,
multiplication(X0,addition(one,multiplication(star(one),star(star(one))))) = X0 ).
cnf(u1220,axiom,
complement(zero,X0) ).
cnf(u523,axiom,
( ~ leq(multiplication(X0,X1),X0)
| multiplication(X0,addition(one,multiplication(X1,multiplication(star(X1),multiplication(star(multiplication(X1,star(X1))),star(multiplication(X1,multiplication(star(X1),star(multiplication(X1,star(X1))))))))))) = X0 ) ).
cnf(u1227,axiom,
complement(X0,X1) ).
cnf(u236,axiom,
multiplication(X0,addition(one,X1)) = multiplication(X0,addition(one,addition(star(one),X1))) ).
cnf(u806,axiom,
multiplication(X0,addition(one,multiplication(star(star(one)),star(star(star(one)))))) = X0 ).
cnf(u968,axiom,
zero = one ).
cnf(u702,axiom,
( ~ leq(multiplication(addition(X0,X1),X2),multiplication(X0,X2))
| leq(multiplication(X1,multiplication(X2,star(one))),multiplication(X0,X2)) ) ).
cnf(u595,axiom,
( ~ leq(multiplication(X0,multiplication(X1,addition(one,X2))),multiplication(X0,X1))
| leq(multiplication(X0,multiplication(X1,star(X2))),multiplication(X0,X1)) ) ).
cnf(u991,axiom,
multiplication(X0,multiplication(star(zero),star(zero))) = X0 ).
cnf(u655,axiom,
( multiplication(c(X0),X1) = multiplication(c(X0),addition(X1,X0))
| zero = c(X0) ) ).
cnf(u798,axiom,
multiplication(X0,addition(one,multiplication(star(star(one)),multiplication(star(star(star(one))),star(multiplication(star(star(one)),star(star(star(one))))))))) = X0 ).
cnf(u45,axiom,
multiplication(X0,one) = X0 ).
cnf(u485,axiom,
( one != addition(X0,c(X0))
| zero != multiplication(c(X0),X0)
| complement(X0,c(X0))
| zero = c(X0) ) ).
cnf(u48,axiom,
multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)) ).
cnf(u284,axiom,
leq(multiplication(X0,multiplication(X1,star(one))),multiplication(X0,X1)) ).
cnf(u115,axiom,
( one != addition(one,X0)
| complement(X0,one)
| zero != X0 ) ).
cnf(u803,axiom,
leq(star(star(one)),one) ).
cnf(u431,axiom,
multiplication(X0,addition(one,multiplication(star(zero),multiplication(star(star(zero)),star(one))))) = X0 ).
cnf(u187,axiom,
( leq(multiplication(sK0(multiplication(X0,X1)),star(X1)),X0)
| ~ leq(one,X0)
| zero = c(multiplication(X0,X1)) ) ).
cnf(u972,axiom,
leq(multiplication(X0,star(zero)),X0) ).
cnf(u710,axiom,
addition(X0,multiplication(X1,X0)) = multiplication(addition(X1,one),X0) ).
cnf(u178,axiom,
( ~ leq(multiplication(X3,multiplication(X0,addition(X1,X2))),X3)
| multiplication(X3,addition(one,multiplication(X0,multiplication(X2,star(multiplication(X0,X1)))))) = X3 ) ).
cnf(u78,axiom,
addition(zero,X0) = X0 ).
cnf(u662,axiom,
( c(X0) = multiplication(c(X0),addition(one,multiplication(X0,star(X0))))
| zero = c(X0) ) ).
cnf(u970,axiom,
multiplication(zero,X0) = X0 ).
cnf(u369,axiom,
( one != addition(one,addition(multiplication(star(one),star(star(one))),X0))
| complement(X0,one)
| zero != X0 ) ).
cnf(u648,axiom,
( c(addition(X0,X1)) = multiplication(c(addition(X0,X1)),addition(one,multiplication(X1,star(X0))))
| zero = c(addition(X0,X1)) ) ).
cnf(u65,axiom,
( test(X0)
| zero = c(X0) ) ).
cnf(u709,axiom,
( multiplication(X0,X1) = multiplication(addition(X0,c(X1)),X1)
| zero = c(X1) ) ).
cnf(u52,axiom,
( addition(X0,X1) != X1
| leq(X0,X1) ) ).
cnf(u96,axiom,
( ~ test(X0)
| zero = multiplication(c(X0),X0) ) ).
cnf(u272,axiom,
( ~ leq(addition(multiplication(X0,multiplication(X1,X2)),X3),multiplication(X0,X1))
| leq(multiplication(X3,star(X2)),multiplication(X0,X1)) ) ).
cnf(u156,axiom,
multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X2),multiplication(X0,X1)) ).
cnf(u47,axiom,
multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)) ).
cnf(u59,axiom,
( ~ complement(X1,X0)
| addition(X0,X1) = one ) ).
cnf(u504,axiom,
( ~ leq(multiplication(X0,multiplication(X1,X2)),multiplication(X0,X1))
| multiplication(X0,X1) = multiplication(X0,multiplication(X1,addition(one,multiplication(X2,multiplication(star(X2),star(multiplication(X2,star(X2)))))))) ) ).
cnf(u844,axiom,
multiplication(X0,addition(one,multiplication(star(star(one)),star(one)))) = X0 ).
cnf(u786,axiom,
( leq(multiplication(c(X0),multiplication(X1,star(X1))),X0)
| ~ leq(X1,X0)
| zero = c(X0) ) ).
cnf(u807,axiom,
multiplication(X0,addition(one,star(star(one)))) = X0 ).
cnf(u329,axiom,
( ~ leq(multiplication(X0,addition(X2,X1)),X0)
| multiplication(X0,addition(one,multiplication(X1,multiplication(star(X2),star(multiplication(X1,star(X2))))))) = X0 ) ).
cnf(u916,axiom,
( one != addition(one,addition(multiplication(star(star(one)),star(one)),X0))
| complement(X0,one)
| zero != X0 ) ).
cnf(u50,axiom,
zero = multiplication(zero,X0) ).
cnf(u696,axiom,
( multiplication(X0,X2) != multiplication(addition(X0,X1),X2)
| leq(multiplication(X1,X2),multiplication(X0,X2)) ) ).
cnf(u694,axiom,
multiplication(addition(X0,X1),X2) = addition(multiplication(X1,X2),multiplication(X0,X2)) ).
cnf(u286,axiom,
( leq(multiplication(X0,multiplication(X1,multiplication(X2,star(X2)))),multiplication(X0,X1))
| ~ leq(multiplication(X0,multiplication(X1,X2)),multiplication(X0,X1)) ) ).
cnf(u274,axiom,
( ~ leq(addition(X3,multiplication(X0,multiplication(X1,X2))),multiplication(X0,X1))
| leq(multiplication(X3,star(X2)),multiplication(X0,X1)) ) ).
cnf(u460,axiom,
star(X0) = addition(star(X0),addition(one,multiplication(star(X0),X0))) ).
cnf(u845,axiom,
leq(multiplication(X0,star(star(star(one)))),X0) ).
cnf(u402,axiom,
( leq(multiplication(X0,multiplication(X1,star(zero))),X2)
| ~ leq(multiplication(X0,X1),X2) ) ).
cnf(u961,axiom,
complement(zero,one) ).
cnf(u883,axiom,
leq(addition(one,star(addition(one,multiplication(star(star(one)),star(one))))),star(addition(one,multiplication(star(star(one)),star(one))))) ).
cnf(u417,axiom,
one = addition(one,multiplication(star(zero),star(star(zero)))) ).
cnf(u141,axiom,
( zero = multiplication(X0,sK0(X0))
| zero = c(X0) ) ).
cnf(u652,axiom,
( leq(multiplication(X0,star(X1)),c(X1))
| ~ leq(X0,c(X1))
| zero = c(X1) ) ).
cnf(u563,axiom,
( multiplication(X0,addition(one,c(X0))) = X0
| zero = c(X0) ) ).
cnf(u72,axiom,
leq(X0,X0) ).
cnf(u656,axiom,
( multiplication(c(X0),X1) = multiplication(c(X0),addition(X0,X1))
| zero = c(X0) ) ).
cnf(u95,axiom,
leq(multiplication(X0,star(one)),X0) ).
cnf(u774,axiom,
( leq(multiplication(c(X0),star(one)),X0)
| ~ leq(one,X0)
| zero = c(X0) ) ).
cnf(u54,axiom,
leq(addition(one,multiplication(star(X0),X0)),star(X0)) ).
cnf(u670,axiom,
multiplication(addition(multiplication(X0,X1),X3),X2) = addition(multiplication(X0,multiplication(X1,X2)),multiplication(X3,X2)) ).
cnf(u789,axiom,
( multiplication(X0,addition(one,multiplication(c(X1),star(X1)))) = X0
| zero = c(X1) ) ).
cnf(u749,axiom,
( leq(multiplication(X1,multiplication(c(addition(X0,X1)),star(c(addition(X0,X1))))),X0)
| zero = c(addition(X0,X1)) ) ).
cnf(u962,axiom,
test(one) ).
cnf(u113,axiom,
( one != addition(X0,one)
| complement(one,X0)
| zero != X0 ) ).
cnf(u393,axiom,
( one != X0
| complement(X0,zero) ) ).
cnf(u185,axiom,
( one != X0
| leq(sK0(X0),X0)
| zero = c(X0) ) ).
cnf(u76,axiom,
( zero != X0
| leq(X0,zero) ) ).
cnf(u248,axiom,
one = addition(one,multiplication(star(one),star(one))) ).
cnf(u827,axiom,
one = addition(one,star(star(one))) ).
cnf(u484,axiom,
( leq(multiplication(X0,star(c(X1))),X1)
| ~ leq(X0,X1)
| zero = c(X1) ) ).
cnf(u551,axiom,
( multiplication(X0,addition(one,X1)) != X0
| leq(multiplication(X0,X1),X0) ) ).
cnf(u704,axiom,
( ~ leq(multiplication(addition(X0,X1),X2),X1)
| leq(multiplication(X0,multiplication(X2,star(X2))),X1) ) ).
cnf(u42,axiom,
addition(X0,zero) = X0 ).
cnf(u772,axiom,
( one != c(X0)
| leq(X0,c(X0))
| zero = c(X0) ) ).
cnf(u102,axiom,
leq(zero,X0) ).
cnf(u718,axiom,
( multiplication(X1,X0) = multiplication(addition(c(X0),X1),X0)
| zero = c(X0) ) ).
cnf(u739,axiom,
( leq(multiplication(X0,multiplication(X1,star(X1))),zero)
| ~ leq(multiplication(X0,X1),zero) ) ).
cnf(u174,axiom,
( ~ leq(multiplication(X1,X0),X1)
| multiplication(X1,addition(one,multiplication(X0,star(zero)))) = X1 ) ).
cnf(u57,axiom,
( complement(sK0(X0),X0)
| ~ test(X0) ) ).
cnf(u218,axiom,
multiplication(X0,addition(one,star(one))) = X0 ).
cnf(u325,axiom,
( ~ leq(X0,one)
| one = addition(one,multiplication(X0,star(X0))) ) ).
cnf(u454,axiom,
leq(one,star(zero)) ).
cnf(u161,axiom,
addition(X0,multiplication(X0,X1)) = multiplication(X0,addition(X1,one)) ).
cnf(u233,axiom,
multiplication(X0,addition(one,multiplication(star(one),star(one)))) = X0 ).
cnf(u261,axiom,
( one != addition(one,addition(multiplication(star(one),star(one)),X0))
| complement(X0,one)
| zero != X0 ) ).
cnf(u104,axiom,
( ~ leq(addition(X1,X0),X0)
| leq(multiplication(X1,star(one)),X0) ) ).
cnf(u64,axiom,
( ~ complement(X0,X1)
| c(X0) = X1
| ~ test(X0) ) ).
cnf(u400,axiom,
( ~ leq(X0,X1)
| addition(multiplication(X0,star(zero)),X1) = X1 ) ).
cnf(u351,axiom,
one = addition(one,multiplication(star(one),star(star(one)))) ).
cnf(u87,axiom,
( ~ leq(multiplication(X0,X1),X0)
| leq(zero,X0) ) ).
cnf(u775,axiom,
( leq(multiplication(X0,star(one)),c(X0))
| ~ leq(one,c(X0))
| zero = c(X0) ) ).
cnf(u467,axiom,
( zero = multiplication(X0,c(X0))
| zero = c(X0) ) ).
cnf(u599,axiom,
leq(multiplication(X0,star(star(one))),X0) ).
cnf(u46,axiom,
multiplication(one,X0) = X0 ).
cnf(u133,axiom,
( leq(multiplication(X0,star(one)),zero)
| ~ leq(X0,zero) ) ).
cnf(u671,axiom,
multiplication(addition(one,X1),X0) = addition(X0,multiplication(X1,X0)) ).
cnf(u1183,axiom,
( complement(zero,X0)
| ~ test(X0) ) ).
cnf(u61,axiom,
( ~ complement(X1,X0)
| zero = multiplication(X0,X1) ) ).
cnf(u649,axiom,
( c(X0) = multiplication(c(X0),addition(one,multiplication(X0,multiplication(star(X0),star(multiplication(X0,star(X0)))))))
| zero = c(X0) ) ).
cnf(u105,axiom,
( leq(multiplication(X1,star(X0)),one)
| ~ leq(addition(X1,X0),one) ) ).
cnf(u165,axiom,
( ~ leq(multiplication(X1,addition(X0,one)),X1)
| leq(multiplication(X1,star(X0)),X1) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE176+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n011.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 13:15:10 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/0.41 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
% 4.89/1.68 % (2399445)Detected formulas, will run a generic FOF schedule.
% 4.89/1.68 % (2399492)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1786962471:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.89/1.68 % (2399492)Refutation not found, incomplete strategy
% 4.89/1.68 % (2399492)------------------------------
% 4.89/1.68 % (2399492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.89/1.68 % (2399492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.89/1.68 % (2399492)CaDiCaL version: 2.1.3
% 4.89/1.68 % (2399492)Termination reason: Refutation not found, incomplete strategy
% 4.89/1.68 % (2399492)Time elapsed: 0.0000 s
% 4.89/1.68 % (2399492)Peak memory usage: 86 MB
% 4.89/1.68 % (2399491)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=3342630846:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.89/1.68 % (2399494)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1617807607:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.89/1.68 % (2399493)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3898093042:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.89/1.68 % (2399495)dis-21_1_sil=8000:lcm=predicate:random_seed=3708553617: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)
% 4.89/1.68 % (2399489)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=2391446237:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.89/1.68 % (2399493)Refutation not found, incomplete strategy
% 4.89/1.68 % (2399493)------------------------------
% 4.89/1.68 % (2399493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.89/1.68 % (2399493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.89/1.68 % (2399493)CaDiCaL version: 2.1.3
% 4.89/1.68 % (2399493)Termination reason: Refutation not found, incomplete strategy
% 4.89/1.68 % (2399493)Time elapsed: 0.0000 s
% 4.89/1.68 % (2399493)Peak memory usage: 86 MB
% 4.89/1.68 % (2399495)Refutation not found, incomplete strategy
% 4.89/1.68 % (2399495)------------------------------
% 4.89/1.68 % (2399495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.89/1.68 % (2399495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.89/1.68 % (2399495)CaDiCaL version: 2.1.3
% 4.89/1.68 % (2399495)Termination reason: Refutation not found, incomplete strategy
% 4.89/1.68 % (2399495)Time elapsed: 0.0000 s
% 4.89/1.68 % (2399495)Peak memory usage: 87 MB
% 4.89/1.68 % (2399494)Instruction limit reached!
% 4.89/1.68 % (2399494)------------------------------
% 4.89/1.68 % (2399494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.89/1.68 % (2399494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.89/1.68 % (2399494)CaDiCaL version: 2.1.3
% 4.89/1.68 % (2399494)Termination reason: Instruction limit
% 4.89/1.68 % (2399494)Termination phase: Saturation
% 4.89/1.68 % (2399494)Time elapsed: 0.083 s
% 4.89/1.68 % (2399494)Peak memory usage: 89 MB
% 4.89/1.68 % (2399494)Instructions burned: 140 (million)
% 4.89/1.68 % (2399490)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=2715741565:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.89/1.68 % (2399492)------------------------------
% 4.89/1.68 % (2399492)------------------------------
% 4.89/1.68 % (2399504)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3755126367:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 4.89/1.68 % (2399504)Refutation not found, incomplete strategy
% 4.89/1.68 % (2399504)------------------------------
% 4.89/1.68 % (2399504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.89/1.68 % (2399504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.89/1.68 % (2399504)CaDiCaL version: 2.1.3
% 4.89/1.68 % (2399504)Termination reason: Refutation not found, incomplete strategy
% 4.89/1.68 % (2399504)Time elapsed: 0.0000 s
% 4.89/1.68 % (2399504)Peak memory usage: 87 MB
% 4.89/1.68 % (2399502)lrs+10_1_sil=8000:sp=occurrence:random_seed=785494101:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 7.22/1.96 % (2399502)Refutation not found, incomplete strategy
% 7.22/1.96 % (2399502)------------------------------
% 7.22/1.96 % (2399502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.22/1.96 % (2399502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.96 % (2399502)CaDiCaL version: 2.1.3
% 7.22/1.96 % (2399502)Termination reason: Refutation not found, incomplete strategy
% 7.22/1.96 % (2399502)Time elapsed: 0.0000 s
% 7.22/1.96 % (2399502)Peak memory usage: 86 MB
% 7.22/1.96 % (2399495)------------------------------
% 7.22/1.96 % (2399495)------------------------------
% 7.22/1.96 % (2399493)------------------------------
% 7.22/1.96 % (2399493)------------------------------
% 7.22/1.96 [W927 13:15:11.435758777 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.22/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.22/1.96 [W927 13:15:11.435792274 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.22/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.22/1.96 [W927 13:15:11.435829401 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.22/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.22/1.96 [W927 13:15:11.435898344 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.22/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.22/1.96 [W927 13:15:11.435950631 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.22/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.22/1.96 [W927 13:15:11.435983211 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.22/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.22/1.96 [W927 13:15:11.436037311 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.22/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.22/1.96 [W927 13:15:11.436070578 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.22/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.22/1.96 [W927 13:15:11.436115411 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.22/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.22/1.96 [W927 13:15:11.436145448 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.22/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.22/1.96 [W927 13:15:11.436188988 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.22/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.21/2.61 [W927 13:15:11.436243275 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.21/2.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.21/2.61 % (2399504)------------------------------
% 11.21/2.61 % (2399504)------------------------------
% 11.21/2.61 % (2399507)lrs+1011_1_sil=32000:sp=occurrence:random_seed=457687983:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 11.21/2.61 % (2399508)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=3325944739:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 11.21/2.61 % (2399507)Refutation not found, incomplete strategy
% 11.21/2.61 % (2399507)------------------------------
% 11.21/2.61 % (2399507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/2.61 % (2399507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/2.61 % (2399507)CaDiCaL version: 2.1.3
% 11.21/2.61 % (2399507)Termination reason: Refutation not found, incomplete strategy
% 11.21/2.61 % (2399507)Time elapsed: 0.001 s
% 11.21/2.61 % (2399507)Peak memory usage: 86 MB
% 11.21/2.61 % (2399502)------------------------------
% 11.21/2.61 % (2399502)------------------------------
% 11.21/2.61 % (2399517)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1573453907:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 11.21/2.61 % (2399517)Refutation not found, incomplete strategy
% 11.21/2.61 % (2399517)------------------------------
% 11.21/2.61 % (2399517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/2.61 % (2399517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/2.61 % (2399517)CaDiCaL version: 2.1.3
% 11.21/2.61 % (2399517)Termination reason: Refutation not found, incomplete strategy
% 11.21/2.61 % (2399517)Time elapsed: 0.001 s
% 11.21/2.61 % (2399517)Peak memory usage: 86 MB
% 11.21/2.61 % (2399491)Refutation not found, incomplete strategy
% 11.21/2.61 % (2399491)------------------------------
% 11.21/2.61 % (2399491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/2.61 % (2399491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/2.61 % (2399491)CaDiCaL version: 2.1.3
% 11.21/2.61 % (2399491)Termination reason: Refutation not found, incomplete strategy
% 11.21/2.61 % (2399491)Time elapsed: 0.657 s
% 11.21/2.61 % (2399491)Peak memory usage: 123 MB
% 11.21/2.61 % (2399491)Instructions burned: 825 (million)
% 11.21/2.61 % (2399508)Instruction limit reached!
% 11.21/2.61 % (2399508)------------------------------
% 11.21/2.61 % (2399508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/2.61 % (2399508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/2.61 % (2399508)CaDiCaL version: 2.1.3
% 11.21/2.61 % (2399508)Termination reason: Instruction limit
% 11.21/2.61 % (2399508)Termination phase: Saturation
% 11.21/2.61 % (2399508)Time elapsed: 0.237 s
% 11.21/2.61 % (2399508)Peak memory usage: 91 MB
% 11.21/2.61 % (2399508)Instructions burned: 248 (million)
% 11.21/2.61 [W927 13:15:12.714676790 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.21/2.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.21/2.61 [W927 13:15:12.714718704 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.21/2.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.21/2.61 [W927 13:15:12.714784697 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.21/2.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.21/2.61 [W927 13:15:12.714805660 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 15.97/3.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.97/3.09 [W927 13:15:12.714854424 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 15.97/3.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.97/3.09 [W927 13:15:12.714873444 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 15.97/3.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.97/3.09 [W927 13:15:12.714920077 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 15.97/3.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.97/3.09 [W927 13:15:12.714937957 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 15.97/3.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.97/3.09 [W927 13:15:12.714980884 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 15.97/3.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.97/3.09 [W927 13:15:12.714998567 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 15.97/3.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.97/3.09 [W927 13:15:12.715060237 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 15.97/3.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.97/3.09 [W927 13:15:12.715079061 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 15.97/3.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.97/3.09 % (2399507)------------------------------
% 15.97/3.09 % (2399507)------------------------------
% 15.97/3.09 % (2399517)------------------------------
% 15.97/3.09 % (2399517)------------------------------
% 15.97/3.09 % (2399521)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=851325883:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 15.97/3.09 % (2399490)Refutation not found, incomplete strategy
% 15.97/3.09 % (2399490)------------------------------
% 15.97/3.09 % (2399490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.97/3.09 % (2399490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.97/3.09 % (2399490)CaDiCaL version: 2.1.3
% 15.97/3.09 % (2399490)Termination reason: Refutation not found, incomplete strategy
% 15.97/3.09 % (2399490)Time elapsed: 0.781 s
% 15.97/3.09 % (2399490)Peak memory usage: 125 MB
% 15.97/3.09 % (2399490)Instructions burned: 825 (million)
% 15.97/3.09 % (2399529)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4130836084:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 15.97/3.09 % (2399529)Refutation not found, incomplete strategy
% 15.97/3.09 % (2399529)------------------------------
% 15.97/3.09 % (2399529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.97/3.09 % (2399529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.97/3.09 % (2399529)CaDiCaL version: 2.1.3
% 15.97/3.09 % (2399529)Termination reason: Refutation not found, incomplete strategy
% 15.97/3.09 % (2399529)Time elapsed: 0.001 s
% 15.97/3.09 % (2399529)Peak memory usage: 86 MB
% 14.67/3.31 % (2399489)Refutation not found, incomplete strategy
% 14.67/3.31 % (2399489)------------------------------
% 14.67/3.31 % (2399489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.67/3.31 % (2399489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.67/3.31 % (2399489)CaDiCaL version: 2.1.3
% 14.67/3.31 % (2399489)Termination reason: Refutation not found, incomplete strategy
% 14.67/3.31 % (2399489)Time elapsed: 0.983 s
% 14.67/3.31 % (2399489)Peak memory usage: 130 MB
% 14.67/3.31 % (2399489)Instructions burned: 1206 (million)
% 14.67/3.31 % (2399532)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2058100246:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 14.67/3.31 % (2399532)Refutation not found, incomplete strategy
% 14.67/3.31 % (2399532)------------------------------
% 14.67/3.31 % (2399532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.67/3.31 % (2399532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.67/3.31 % (2399532)CaDiCaL version: 2.1.3
% 14.67/3.31 % (2399532)Termination reason: Refutation not found, incomplete strategy
% 14.67/3.31 % (2399532)Time elapsed: 0.001 s
% 14.67/3.31 % (2399532)Peak memory usage: 87 MB
% 14.67/3.31 % (2399491)------------------------------
% 14.67/3.31 % (2399491)------------------------------
% 14.67/3.31 % (2399531)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=427729886:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 14.67/3.31 % (2399531)Refutation not found, incomplete strategy
% 14.67/3.31 % (2399531)------------------------------
% 14.67/3.31 % (2399531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.67/3.31 % (2399531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.67/3.31 % (2399531)CaDiCaL version: 2.1.3
% 14.67/3.31 % (2399531)Termination reason: Refutation not found, incomplete strategy
% 14.67/3.31 % (2399531)Time elapsed: 0.002 s
% 14.67/3.31 % (2399531)Peak memory usage: 88 MB
% 14.67/3.31 % (2399531)Instructions burned: 1 (million)
% 14.67/3.31 % (2399490)------------------------------
% 14.67/3.31 % (2399490)------------------------------
% 14.67/3.31 % (2399532)------------------------------
% 14.67/3.31 % (2399532)------------------------------
% 14.67/3.31 % (2399529)------------------------------
% 14.67/3.31 % (2399529)------------------------------
% 14.67/3.31 % (2399489)------------------------------
% 14.67/3.31 % (2399489)------------------------------
% 14.67/3.31 % (2399540)lrs+10_1_sil=8000:sp=occurrence:random_seed=756217852:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2987 on theBenchmark for (2987ds/907Mi)
% 14.67/3.31 % (2399540)Refutation not found, incomplete strategy
% 14.67/3.31 % (2399540)------------------------------
% 14.67/3.31 % (2399540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.67/3.31 % (2399540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.67/3.31 % (2399540)CaDiCaL version: 2.1.3
% 14.67/3.31 % (2399540)Termination reason: Refutation not found, incomplete strategy
% 14.67/3.31 % (2399540)Time elapsed: 0.001 s
% 14.67/3.31 % (2399540)Peak memory usage: 86 MB
% 14.67/3.31 % (2399546)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3548344113:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi)
% 14.67/3.31 % (2399546)Refutation not found, incomplete strategy
% 14.67/3.31 % (2399546)------------------------------
% 14.67/3.31 % (2399546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.67/3.31 % (2399546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.67/3.31 % (2399546)CaDiCaL version: 2.1.3
% 14.67/3.31 % (2399546)Termination reason: Refutation not found, incomplete strategy
% 14.67/3.31 % (2399546)Time elapsed: 0.0000 s
% 14.67/3.31 % (2399546)Peak memory usage: 86 MB
% 14.67/3.31 % (2399531)------------------------------
% 14.67/3.31 % (2399531)------------------------------
% 14.67/3.31 % (2399547)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3222479762:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi)
% 14.67/3.31 % (2399549)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=414203525:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2984 on theBenchmark for (2984ds/134Mi)
% 14.67/3.31 % (2399549)Refutation not found, incomplete strategy
% 14.67/3.31 % (2399549)------------------------------
% 14.67/3.31 % (2399549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.67/3.31 % (2399549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.67/3.31 % (2399549)CaDiCaL version: 2.1.3
% 14.67/3.31 % (2399549)Termination reason: Refutation not found, incomplete strategy
% 14.67/3.31 % (2399549)Time elapsed: 0.001 s
% 14.67/3.31 % (2399549)Peak memory usage: 86 MB
% 14.67/3.31 % (2399550)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=896153881:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 14.67/3.31 % (2399550)Refutation not found, incomplete strategy
% 14.67/3.31 % (2399550)------------------------------
% 14.67/3.31 % (2399550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.67/3.31 % (2399550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.67/3.31 % (2399550)CaDiCaL version: 2.1.3
% 14.67/3.31 % (2399550)Termination reason: Refutation not found, incomplete strategy
% 14.67/3.31 % (2399550)Time elapsed: 0.001 s
% 14.67/3.31 % (2399550)Peak memory usage: 86 MB
% 14.67/3.31 % (2399540)------------------------------
% 14.67/3.31 % (2399540)------------------------------
% 14.67/3.31 % (2399546)------------------------------
% 14.67/3.31 % (2399546)------------------------------
% 14.67/3.31 % (2399555)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2616106192:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 14.67/3.31 % (2399549)------------------------------
% 14.67/3.31 % (2399549)------------------------------
% 14.67/3.31 % (2399563)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1007404758:i=134:gtgl=5:slsql=off:gtg=exists_sym_2980 on theBenchmark for (2980ds/134Mi)
% 14.67/3.31 % (2399562)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=1020772757:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/125Mi)
% 14.67/3.31 % (2399562)Refutation not found, incomplete strategy
% 14.67/3.31 % (2399562)------------------------------
% 14.67/3.31 % (2399562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.67/3.31 % (2399562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.67/3.31 % (2399562)CaDiCaL version: 2.1.3
% 14.67/3.31 % (2399562)Termination reason: Refutation not found, incomplete strategy
% 14.67/3.31 % (2399562)Time elapsed: 0.001 s
% 14.67/3.31 % (2399562)Peak memory usage: 87 MB
% 14.67/3.31 % (2399521)First to succeed.
% 14.67/3.31 % (2399521)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2399445"
% 14.67/3.31 % (2399550)------------------------------
% 14.67/3.31 % (2399550)------------------------------
% 14.67/3.31 [W927 13:15:13.125076415 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 14.67/3.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 14.67/3.31 [W927 13:15:13.125189662 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 14.67/3.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 14.67/3.31 [W927 13:15:13.125281232 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 14.67/3.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 14.67/3.31 [W927 13:15:13.125337372 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 14.67/3.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 14.67/3.31 [W927 13:15:13.125414199 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 14.67/3.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 14.67/3.31 [W927 13:15:13.125461912 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 14.67/3.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 14.67/3.31 [W927 13:15:13.125563246 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 14.67/3.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 14.67/3.31 [W927 13:15:13.125613206 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 14.67/3.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 14.67/3.31 [W927 13:15:13.125687929 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 14.67/3.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 14.67/3.31 [W927 13:15:13.125736109 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 14.67/3.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 14.67/3.31 [W927 13:15:13.125810059 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 14.67/3.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 14.67/3.31 [W927 13:15:13.125857912 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 14.67/3.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 14.67/3.31 % (2399563)Instruction limit reached!
% 14.67/3.31 % (2399563)------------------------------
% 14.67/3.31 % (2399563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.67/3.31 % (2399563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.67/3.31 % (2399563)CaDiCaL version: 2.1.3
% 14.67/3.31 % (2399563)Termination reason: Instruction limit
% 14.67/3.31 % (2399563)Termination phase: Saturation
% 14.67/3.31 % (2399563)Time elapsed: 0.099 s
% 14.67/3.31 % (2399563)Peak memory usage: 89 MB
% 14.67/3.31 % (2399563)Instructions burned: 134 (million)
% 14.67/3.31 % (2399569)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3918384418:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/141Mi)
% 14.67/3.31 % (2399569)Refutation not found, incomplete strategy
% 14.67/3.31 % (2399569)------------------------------
% 14.67/3.31 % (2399569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.67/3.31 % (2399569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.67/3.31 % (2399569)CaDiCaL version: 2.1.3
% 14.67/3.31 % (2399569)Termination reason: Refutation not found, incomplete strategy
% 14.67/3.31 % (2399569)Time elapsed: 0.001 s
% 14.67/3.31 % (2399569)Peak memory usage: 86 MB
% 14.67/3.31 % (2399575)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=484647392:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2977 on theBenchmark for (2977ds/431Mi)
% 14.67/3.31 % (2399575)Refutation not found, incomplete strategy
% 14.67/3.31 % (2399575)------------------------------
% 14.67/3.31 % (2399575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.67/3.31 % (2399575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.67/3.31 % (2399575)CaDiCaL version: 2.1.3
% 14.67/3.31 % (2399575)Termination reason: Refutation not found, incomplete strategy
% 14.67/3.31 % (2399575)Time elapsed: 0.001 s
% 14.67/3.31 % (2399575)Peak memory usage: 86 MB
% 14.67/3.31 % SZS status Satisfiable for theBenchmark
% 14.67/3.31 % SZS output start Saturation.
% See solution above
% 17.94/3.56 % SZS output start Definitions and Model Updates.
% 17.94/3.56 for all inputs,
% 17.94/3.56 define ismeet(X2,X0,X1) := leq(X2,X0) & leq(X2,X1) & ! [X3] : ((leq(X3,X0) & leq(X3,X1)) => leq(X3,X2))
% 17.94/3.56 for all inputs,
% 17.94/3.56 define ismeetu(X2,X0,X1) := ! [X3] : ((leq(X3,X0) & leq(X3,X1)) <=> leq(X3,X2))
% 17.94/3.56 % SZS output end Definitions and Model Updates.
% 17.94/3.56 % (2399521)------------------------------
% 17.94/3.56 % (2399521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.94/3.56 % (2399521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.94/3.56 % (2399521)CaDiCaL version: 2.1.3
% 17.94/3.56 % (2399521)Termination reason: Satisfiable
% 17.94/3.56 % (2399521)Time elapsed: 1.200 s
% 17.94/3.56 % (2399521)Peak memory usage: 134 MB
% 17.94/3.56 % (2399521)Instructions burned: 1353 (million)
% 17.94/3.56 % (2399521)------------------------------
% 17.94/3.56 % (2399521)------------------------------
% 17.94/3.56 % (2399445)Success in time 2.466 s
% 17.94/3.56 % Vampire exiting
%------------------------------------------------------------------------------