%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : KLE179+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 : 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 11:40:34 AM UTC 2026
% Result : Satisfiable 39.55s 6.22s
% Output : Saturation 39.96s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u296,axiom,
zero = c(one) ).
cnf(u300,axiom,
zero = sK0(one) ).
cnf(u313,axiom,
test(one) ).
cnf(u318,axiom,
complement(zero,one) ).
cnf(u1248,axiom,
zero = c(zero) ).
cnf(u2564,axiom,
( ~ leq(multiplication(X2,multiplication(X0,X1)),multiplication(X0,X1))
| leq(multiplication(star(X2),multiplication(X2,X0)),multiplication(X0,X1)) ) ).
cnf(u2772,axiom,
omega(multiplication(X0,addition(X1,X2))) = addition(multiplication(X0,X1),addition(multiplication(X0,X2),omega(multiplication(X0,addition(X1,X2))))) ).
cnf(u1032,axiom,
( addition(X0,addition(X1,X2)) != X2
| leq(addition(X0,addition(X1,X2)),X2) ) ).
cnf(u75,axiom,
( addition(X0,X1) != X0
| leq(X1,X0) ) ).
cnf(u1774,axiom,
( ~ leq(multiplication(X3,addition(X0,addition(X1,X2))),X2)
| leq(multiplication(star(X3),multiplication(X3,addition(X1,X0))),X2) ) ).
cnf(u995,axiom,
leq(multiplication(X1,X2),multiplication(addition(X0,X1),X2)) ).
cnf(u66,axiom,
( ~ complement(X1,X0)
| zero = multiplication(X0,X1) ) ).
cnf(u2156,axiom,
( zero != multiplication(X1,X0)
| addition(X0,X1) != zero
| zero != multiplication(X0,X1)
| complement(X1,X0) ) ).
cnf(u1080,axiom,
addition(X0,addition(X1,X2)) = addition(X1,addition(X0,addition(X1,X2))) ).
cnf(u1501,axiom,
( ~ leq(multiplication(X0,addition(X1,X2)),X1)
| leq(multiplication(star(X0),multiplication(X0,X2)),X1) ) ).
cnf(u2632,axiom,
omega(addition(X0,X1)) = multiplication(X0,omega(addition(X0,X1))) ).
cnf(u1424,axiom,
addition(X0,addition(X1,addition(X2,X3))) = addition(X3,addition(X2,addition(X0,X1))) ).
cnf(u2516,axiom,
( ~ leq(addition(X0,addition(multiplication(X1,X0),X2)),X0)
| leq(multiplication(star(X1),X2),X0) ) ).
cnf(u2586,axiom,
( leq(multiplication(X2,star(addition(X0,X1))),X2)
| ~ leq(multiplication(X2,addition(X0,X1)),X2) ) ).
cnf(u2583,axiom,
( ~ leq(addition(X0,X1),zero)
| leq(multiplication(star(X0),X1),zero) ) ).
cnf(u44,axiom,
addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0) ).
cnf(u3136,axiom,
( leq(multiplication(addition(X0,X1),star(X2)),X0)
| ~ leq(multiplication(addition(X0,X1),X2),X0) ) ).
cnf(u3087,axiom,
omega(multiplication(X0,X1)) = multiplication(X0,omega(multiplication(X0,X1))) ).
cnf(u1740,axiom,
( ~ leq(multiplication(X3,addition(X0,addition(X1,X2))),addition(X0,X1))
| leq(multiplication(star(X3),multiplication(X3,X2)),addition(X0,X1)) ) ).
cnf(u1425,axiom,
addition(X0,addition(X1,addition(X2,X3))) = addition(X2,addition(X3,addition(X0,X1))) ).
cnf(u63,axiom,
( ~ complement(X1,X0)
| test(X0) ) ).
cnf(u3533,axiom,
test(X0) ).
cnf(u2815,axiom,
( omega(X0) != addition(X1,omega(X0))
| leq(addition(X1,X0),omega(X0)) ) ).
cnf(u1753,axiom,
( ~ leq(multiplication(X0,multiplication(X1,addition(X2,X3))),X2)
| leq(multiplication(star(multiplication(X0,X1)),multiplication(X0,multiplication(X1,X3))),X2) ) ).
cnf(u387,axiom,
( ~ leq(multiplication(X3,multiplication(addition(X0,X1),X2)),X3)
| leq(multiplication(X3,multiplication(X1,multiplication(X2,star(multiplication(X0,X2))))),X3) ) ).
cnf(u179,axiom,
( ~ leq(multiplication(X0,addition(X1,X2)),X0)
| leq(multiplication(X0,multiplication(X2,star(X1))),X0) ) ).
cnf(u1119,axiom,
addition(X2,addition(X1,X0)) = addition(X0,addition(X1,X2)) ).
cnf(u2152,axiom,
multiplication(zero,X0) = X0 ).
cnf(u971,axiom,
leq(X1,addition(X0,X1)) ).
cnf(u999,axiom,
( addition(X0,X1) != addition(X2,addition(X0,X1))
| leq(addition(X2,X0),addition(X0,X1)) ) ).
cnf(u930,axiom,
addition(X0,X1) = addition(X1,addition(X0,X1)) ).
cnf(u1577,axiom,
addition(multiplication(X3,multiplication(X0,X1)),addition(multiplication(X3,multiplication(X0,X2)),X4)) = addition(multiplication(X3,multiplication(X0,addition(X1,X2))),X4) ).
cnf(u1175,axiom,
addition(X0,addition(X1,addition(X2,X3))) = addition(X2,addition(X0,addition(X1,X3))) ).
cnf(u1863,axiom,
( ~ leq(addition(multiplication(X0,X1),addition(multiplication(X0,X2),omega(X3))),X3)
| leq(multiplication(X0,multiplication(addition(X1,X2),star(omega(X3)))),X3) ) ).
cnf(u1332,axiom,
addition(X3,multiplication(addition(X0,X1),X2)) = addition(multiplication(X1,X2),addition(X3,multiplication(X0,X2))) ).
cnf(u55,axiom,
( addition(X0,X1) != X1
| leq(X0,X1) ) ).
cnf(u2619,axiom,
multiplication(addition(X0,addition(X1,X2)),omega(X2)) = multiplication(addition(X1,X0),omega(X2)) ).
cnf(u3150,axiom,
( ~ leq(X0,zero)
| zero = star(X0) ) ).
cnf(u2631,axiom,
leq(X0,multiplication(X0,X1)) ).
cnf(u2643,axiom,
multiplication(addition(X0,X1),addition(X2,omega(X1))) = addition(multiplication(X0,X2),addition(multiplication(X1,X2),multiplication(X0,omega(X1)))) ).
cnf(u3111,axiom,
multiplication(X0,omega(multiplication(X1,X2))) = multiplication(addition(X0,X1),omega(multiplication(X1,X2))) ).
cnf(u201,axiom,
( ~ leq(multiplication(X3,multiplication(X0,addition(X1,X2))),X3)
| leq(multiplication(X3,multiplication(X0,multiplication(X2,star(multiplication(X0,X1))))),X3) ) ).
cnf(u1121,axiom,
( addition(X0,addition(X1,X2)) != X2
| leq(addition(X1,X0),X2) ) ).
cnf(u1529,axiom,
( leq(multiplication(star(X0),X1),zero)
| ~ leq(X1,zero) ) ).
cnf(u2795,axiom,
( ~ test(sK0(X0))
| zero = X0
| ~ test(X0) ) ).
cnf(u1536,axiom,
( ~ leq(addition(omega(X1),addition(multiplication(X0,omega(X1)),X2)),omega(X1))
| leq(multiplication(star(addition(X0,X1)),X2),omega(X1)) ) ).
cnf(u51,axiom,
multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)) ).
cnf(u2530,axiom,
leq(multiplication(X2,X1),multiplication(X2,multiplication(X0,X1))) ).
cnf(u3140,axiom,
( ~ leq(multiplication(addition(X0,addition(X1,X2)),X3),X2)
| leq(multiplication(addition(X0,X1),star(X3)),X2) ) ).
cnf(u1126,axiom,
( ~ leq(multiplication(X3,addition(X0,addition(X1,X2))),X3)
| leq(multiplication(X3,multiplication(X2,star(addition(X1,X0)))),X3) ) ).
cnf(u2533,axiom,
multiplication(X0,X1) = addition(X1,multiplication(X0,X1)) ).
cnf(u2522,axiom,
multiplication(X0,multiplication(X1,addition(X2,X3))) = addition(multiplication(X1,X2),addition(multiplication(X1,X3),multiplication(X0,multiplication(X1,addition(X2,X3))))) ).
cnf(u1293,axiom,
leq(multiplication(X3,addition(X0,X1)),multiplication(X3,addition(X0,addition(X1,X2)))) ).
cnf(u2682,axiom,
multiplication(addition(X0,X1),multiplication(omega(X0),X2)) = multiplication(X1,multiplication(omega(X0),X2)) ).
cnf(u1508,axiom,
( ~ leq(addition(X0,addition(X1,multiplication(X2,X3))),X3)
| leq(multiplication(star(X2),addition(X0,X1)),X3) ) ).
cnf(u862,axiom,
addition(multiplication(X0,X1),addition(multiplication(X0,X2),X3)) = addition(multiplication(X0,addition(X1,X2)),X3) ).
cnf(u3134,axiom,
( ~ leq(multiplication(X0,multiplication(addition(X1,X2),X3)),multiplication(X0,X1))
| leq(multiplication(X0,multiplication(X2,star(X3))),multiplication(X0,X1)) ) ).
cnf(u978,axiom,
leq(addition(X0,X1),addition(X0,addition(X1,X2))) ).
cnf(u2740,axiom,
( ~ leq(addition(X0,X1),zero)
| leq(multiplication(X1,star(X0)),zero) ) ).
cnf(u2622,axiom,
multiplication(X1,X0) = addition(X1,multiplication(X1,X0)) ).
cnf(u981,axiom,
leq(multiplication(X0,X2),multiplication(addition(X0,X1),X2)) ).
cnf(u2704,axiom,
( ~ leq(addition(X2,multiplication(X0,omega(X1))),addition(X0,X1))
| leq(multiplication(X2,star(omega(X1))),addition(X0,X1)) ) ).
cnf(u2816,axiom,
leq(X0,omega(X0)) ).
cnf(u2155,axiom,
( ~ complement(X1,X0)
| addition(X0,X1) = zero ) ).
cnf(u2623,axiom,
multiplication(addition(X1,X0),omega(X1)) = multiplication(X0,omega(X1)) ).
cnf(u2738,axiom,
( ~ leq(addition(X1,X0),zero)
| leq(multiplication(X1,star(X0)),zero) ) ).
cnf(u1387,axiom,
( addition(X2,X0) != addition(X3,addition(X0,addition(X1,X2)))
| leq(addition(X3,X1),addition(X2,X0)) ) ).
cnf(u875,axiom,
( addition(X0,addition(X1,X2)) != X2
| leq(addition(X0,X1),X2) ) ).
cnf(u1788,axiom,
( ~ leq(multiplication(X0,multiplication(X1,addition(X2,X3))),X3)
| leq(multiplication(star(multiplication(X0,X1)),multiplication(X0,multiplication(X1,X2))),X3) ) ).
cnf(u1621,axiom,
addition(X4,addition(multiplication(X0,X1),addition(multiplication(X0,X2),X3))) = addition(X3,addition(X4,multiplication(X0,addition(X1,X2)))) ).
cnf(u92,axiom,
( zero != X0
| leq(X0,zero) ) ).
cnf(u1601,axiom,
( ~ leq(addition(multiplication(X0,X1),addition(multiplication(X0,X2),X3)),addition(X1,X2))
| leq(multiplication(star(X0),X3),addition(X1,X2)) ) ).
cnf(u1732,axiom,
( ~ leq(multiplication(X3,addition(X0,addition(X1,X2))),X1)
| leq(multiplication(star(X3),multiplication(X3,addition(X2,X0))),X1) ) ).
cnf(u136,axiom,
multiplication(omega(X0),X1) = multiplication(X0,multiplication(omega(X0),X1)) ).
cnf(u1614,axiom,
( ~ leq(multiplication(X4,addition(multiplication(X0,X1),addition(multiplication(X0,X2),X3))),X4)
| leq(multiplication(X4,multiplication(X3,star(multiplication(X0,addition(X1,X2))))),X4) ) ).
cnf(u3132,axiom,
( leq(multiplication(X0,star(X1)),zero)
| ~ leq(multiplication(X0,X1),zero) ) ).
cnf(u852,axiom,
addition(X0,X1) = addition(X0,addition(X0,X1)) ).
cnf(u720,axiom,
test(zero) ).
cnf(u1418,axiom,
( addition(X0,X1) != addition(X3,addition(X0,addition(X1,X2)))
| leq(addition(X3,X2),addition(X0,X1)) ) ).
cnf(u1629,axiom,
addition(X3,addition(X4,multiplication(X0,addition(X1,X2)))) = addition(multiplication(X0,X1),addition(multiplication(X0,X2),addition(X3,X4))) ).
cnf(u1376,axiom,
( addition(X0,addition(X1,X2)) != addition(X2,X0)
| leq(X1,addition(X2,X0)) ) ).
cnf(u58,axiom,
( ~ leq(addition(multiplication(X0,X1),X2),X1)
| leq(multiplication(star(X0),X2),X1) ) ).
cnf(u3131,axiom,
( ~ leq(multiplication(addition(X0,X1),X2),X0)
| leq(multiplication(X1,star(X2)),X0) ) ).
cnf(u3141,axiom,
( ~ leq(multiplication(addition(multiplication(X0,X1),addition(multiplication(X0,X2),X3)),X4),multiplication(X0,addition(X1,X2)))
| leq(multiplication(X3,star(X4)),multiplication(X0,addition(X1,X2))) ) ).
cnf(u910,axiom,
multiplication(addition(X1,X0),addition(omega(X1),X2)) = addition(omega(X1),addition(multiplication(X0,omega(X1)),multiplication(addition(X1,X0),X2))) ).
cnf(u2528,axiom,
( leq(multiplication(star(X2),multiplication(X2,multiplication(X0,X1))),X1)
| ~ leq(multiplication(X2,multiplication(X0,X1)),X1) ) ).
cnf(u1503,axiom,
( leq(multiplication(star(X0),multiplication(X0,X1)),X1)
| ~ leq(multiplication(X0,X1),X1) ) ).
cnf(u341,axiom,
( leq(multiplication(X0,star(X1)),zero)
| ~ leq(X0,zero) ) ).
cnf(u3016,axiom,
( zero != multiplication(omega(X1),addition(X1,X0))
| zero != multiplication(X0,omega(X1))
| zero != addition(X1,addition(omega(X1),X0))
| complement(addition(X1,X0),omega(X1)) ) ).
cnf(u177,axiom,
multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X2),multiplication(X0,X1)) ).
cnf(u77,axiom,
leq(X0,X0) ).
cnf(u1553,axiom,
( leq(multiplication(star(multiplication(X0,X1)),multiplication(X0,multiplication(X1,X2))),X2)
| ~ leq(multiplication(X0,multiplication(X1,X2)),X2) ) ).
cnf(u879,axiom,
( multiplication(X3,X2) != multiplication(X3,addition(X0,addition(X1,X2)))
| leq(multiplication(X3,addition(X0,X1)),multiplication(X3,X2)) ) ).
cnf(u1604,axiom,
addition(multiplication(X0,X1),addition(multiplication(X0,X2),multiplication(X3,addition(X1,X2)))) = multiplication(addition(X0,X3),addition(X1,X2)) ).
cnf(u885,axiom,
( ~ leq(addition(X0,addition(X1,multiplication(X2,X3))),X2)
| leq(multiplication(addition(X0,X1),star(X3)),X2) ) ).
cnf(u1506,axiom,
( leq(multiplication(star(X0),addition(multiplication(X0,X1),X2)),X1)
| ~ leq(addition(multiplication(X0,X1),X2),X1) ) ).
cnf(u2962,axiom,
omega(multiplication(X0,X1)) = multiplication(X1,omega(multiplication(X0,X1))) ).
cnf(u2150,axiom,
zero = one ).
cnf(u1729,axiom,
( leq(multiplication(star(X2),multiplication(X2,addition(X0,X1))),X0)
| ~ leq(multiplication(X2,addition(X0,X1)),X0) ) ).
cnf(u2779,axiom,
( leq(multiplication(star(X0),omega(multiplication(X0,X1))),X1)
| ~ leq(omega(multiplication(X0,X1)),X1) ) ).
cnf(u43,axiom,
addition(X0,X1) = addition(X1,X0) ).
cnf(u2266,axiom,
( zero != X0
| complement(zero,X0) ) ).
cnf(u3138,axiom,
( ~ leq(multiplication(addition(X0,addition(X1,X2)),X3),addition(X1,X0))
| leq(multiplication(X2,star(X3)),addition(X1,X0)) ) ).
cnf(u53,axiom,
zero = multiplication(zero,X0) ).
cnf(u2781,axiom,
leq(multiplication(X1,X0),multiplication(X1,omega(X0))) ).
cnf(u1176,axiom,
addition(X0,addition(X1,addition(X2,X3))) = addition(X2,addition(X1,addition(X0,X3))) ).
cnf(u2599,axiom,
leq(multiplication(X0,omega(X1)),multiplication(addition(X1,X0),addition(omega(X1),X2))) ).
cnf(u1061,axiom,
( leq(multiplication(X2,multiplication(addition(X0,X1),star(X1))),X2)
| ~ leq(multiplication(X2,addition(X0,X1)),X2) ) ).
cnf(u62,axiom,
( complement(sK0(X0),X0)
| ~ test(X0) ) ).
cnf(u3139,axiom,
( ~ leq(multiplication(addition(X0,addition(X1,X2)),X3),X1)
| leq(multiplication(addition(X2,X0),star(X3)),X1) ) ).
cnf(u1133,axiom,
leq(addition(X1,X0),addition(X0,addition(X1,X2))) ).
cnf(u1328,axiom,
addition(X3,addition(X0,addition(X1,X2))) = addition(X2,addition(X3,addition(X1,X0))) ).
cnf(u1778,axiom,
( ~ leq(multiplication(X3,multiplication(addition(X0,X1),X2)),multiplication(X1,X2))
| leq(multiplication(star(X3),multiplication(X3,multiplication(X0,X2))),multiplication(X1,X2)) ) ).
cnf(u957,axiom,
leq(multiplication(X2,X0),multiplication(X2,addition(X0,X1))) ).
cnf(u2590,axiom,
multiplication(addition(X0,addition(X1,X2)),omega(addition(X2,X0))) = multiplication(X1,omega(addition(X2,X0))) ).
cnf(u3112,axiom,
multiplication(X1,omega(multiplication(X0,X2))) = multiplication(addition(X0,X1),omega(multiplication(X0,X2))) ).
cnf(u386,axiom,
multiplication(addition(X0,X1),X2) = addition(multiplication(X1,X2),multiplication(X0,X2)) ).
cnf(u2652,axiom,
( leq(multiplication(X0,multiplication(X1,star(X2))),multiplication(X0,X1))
| ~ leq(multiplication(X0,multiplication(X1,X2)),multiplication(X0,X1)) ) ).
cnf(u1412,axiom,
( ~ leq(multiplication(X3,addition(X0,addition(X1,X2))),X3)
| leq(multiplication(X3,multiplication(addition(X0,X1),star(X2))),X3) ) ).
cnf(u2727,axiom,
( leq(multiplication(X2,multiplication(X0,multiplication(X1,star(X0)))),X2)
| ~ leq(multiplication(X2,multiplication(X0,X1)),X2) ) ).
cnf(u1450,axiom,
addition(X2,addition(X0,X1)) = addition(X1,addition(X0,addition(X1,X2))) ).
cnf(u2771,axiom,
( leq(multiplication(star(X1),multiplication(X1,omega(X0))),X0)
| ~ leq(multiplication(X1,omega(X0)),X0) ) ).
cnf(u1411,axiom,
( multiplication(X3,addition(X0,addition(X1,X2))) != multiplication(X3,addition(X0,X1))
| leq(multiplication(X3,X2),multiplication(X3,addition(X0,X1))) ) ).
cnf(u2929,axiom,
multiplication(X0,multiplication(addition(X1,X2),omega(multiplication(X0,X2)))) = multiplication(X0,multiplication(X1,omega(multiplication(X0,X2)))) ).
cnf(u2653,axiom,
( leq(multiplication(X1,star(X0)),X1)
| ~ leq(multiplication(X1,X0),X1) ) ).
cnf(u383,axiom,
( multiplication(X0,X2) != multiplication(addition(X0,X1),X2)
| leq(multiplication(X1,X2),multiplication(X0,X2)) ) ).
cnf(u3130,axiom,
( ~ leq(multiplication(addition(X0,X1),X2),X1)
| leq(multiplication(X0,star(X2)),X1) ) ).
cnf(u1066,axiom,
( addition(X0,X1) != addition(X2,addition(X0,X1))
| leq(addition(X2,X1),addition(X0,X1)) ) ).
cnf(u944,axiom,
( addition(X0,X1) != X0
| leq(addition(X0,X1),X0) ) ).
cnf(u2687,axiom,
( ~ leq(addition(X2,multiplication(X0,omega(X1))),addition(X1,X0))
| leq(multiplication(X2,star(omega(X1))),addition(X1,X0)) ) ).
cnf(u1296,axiom,
leq(multiplication(X3,multiplication(X0,X2)),multiplication(X3,multiplication(addition(X0,X1),X2))) ).
cnf(u1131,axiom,
( addition(X3,addition(X0,addition(X1,X2))) != X2
| leq(addition(X3,addition(X1,X0)),X2) ) ).
cnf(u60,axiom,
omega(X0) = multiplication(X0,omega(X0)) ).
cnf(u2726,axiom,
( ~ leq(addition(X0,addition(multiplication(X0,X1),X2)),X0)
| leq(multiplication(X2,star(X1)),X0) ) ).
cnf(u1071,axiom,
( leq(multiplication(addition(X0,multiplication(X1,X2)),star(X2)),X1)
| ~ leq(addition(X0,multiplication(X1,X2)),X1) ) ).
cnf(u1502,axiom,
( ~ leq(multiplication(addition(X0,X1),X2),X2)
| leq(multiplication(star(X0),multiplication(X1,X2)),X2) ) ).
cnf(u958,axiom,
leq(X0,addition(X0,X1)) ).
cnf(u2651,axiom,
leq(multiplication(X0,multiplication(X1,star(multiplication(X0,X1)))),star(multiplication(X0,X1))) ).
cnf(u2823,axiom,
multiplication(addition(X1,X0),addition(X2,omega(X1))) = addition(multiplication(X1,X2),multiplication(X0,addition(X2,omega(X1)))) ).
cnf(u1423,axiom,
( addition(X0,X1) != addition(X0,addition(X1,X2))
| leq(addition(X0,addition(X1,X2)),addition(X0,X1)) ) ).
cnf(u1358,axiom,
addition(multiplication(X0,X1),addition(multiplication(X0,X2),X3)) = addition(X3,multiplication(X0,addition(X1,X2))) ).
cnf(u3102,axiom,
( zero != multiplication(omega(X0),X0)
| zero != omega(X0)
| complement(X0,omega(X0)) ) ).
cnf(u1005,axiom,
( addition(X3,addition(X0,addition(X1,X2))) != X2
| leq(addition(X3,addition(X0,X1)),X2) ) ).
cnf(u1017,axiom,
( addition(X0,addition(X1,X2)) != X1
| leq(addition(X2,X0),X1) ) ).
cnf(u125,axiom,
( ~ leq(addition(X1,omega(X0)),X0)
| leq(multiplication(X1,star(omega(X0))),X0) ) ).
cnf(u2700,axiom,
multiplication(addition(X0,X1),multiplication(omega(X1),X2)) = multiplication(X0,multiplication(omega(X1),X2)) ).
cnf(u3152,axiom,
( ~ leq(omega(X0),X0)
| addition(X0,star(omega(X0))) = X0 ) ).
cnf(u2591,axiom,
multiplication(addition(X0,addition(X1,X2)),omega(X1)) = multiplication(addition(X2,X0),omega(X1)) ).
cnf(u1420,axiom,
leq(multiplication(X3,X2),multiplication(X3,addition(X0,addition(X1,X2)))) ).
cnf(u1644,axiom,
( ~ leq(addition(multiplication(X0,X1),addition(multiplication(X0,X2),multiplication(X3,X4))),X3)
| leq(multiplication(X0,multiplication(addition(X1,X2),star(X4))),X3) ) ).
cnf(u1147,axiom,
( addition(X0,addition(X1,addition(X2,X3))) != X3
| leq(addition(X1,addition(X0,X2)),X3) ) ).
cnf(u2766,axiom,
multiplication(X0,multiplication(X1,X2)) = addition(X2,multiplication(X0,multiplication(X1,X2))) ).
cnf(u1498,axiom,
( ~ leq(addition(multiplication(X0,multiplication(X1,X2)),X3),X2)
| leq(multiplication(star(multiplication(X0,X1)),X3),X2) ) ).
cnf(u2767,axiom,
multiplication(addition(X0,X1),X2) = multiplication(addition(X1,X0),X2) ).
cnf(u876,axiom,
( addition(X0,X1) != addition(X0,addition(X1,X2))
| leq(X2,addition(X0,X1)) ) ).
cnf(u2770,axiom,
( ~ leq(multiplication(X1,omega(X0)),omega(X0))
| leq(multiplication(star(X1),multiplication(X1,X0)),omega(X0)) ) ).
cnf(u1374,axiom,
addition(X0,addition(X1,X2)) = addition(addition(X2,X0),X1) ).
cnf(u1400,axiom,
addition(X0,X1) = addition(X0,addition(X1,X0)) ).
cnf(u2532,axiom,
addition(X2,multiplication(X0,X1)) = addition(X1,addition(multiplication(X0,X1),X2)) ).
cnf(u1270,axiom,
leq(omega(X0),multiplication(X0,addition(omega(X0),X1))) ).
cnf(u874,axiom,
addition(X0,addition(X1,X2)) = addition(X2,addition(X0,X1)) ).
cnf(u1295,axiom,
leq(multiplication(X3,multiplication(X0,X1)),multiplication(X3,multiplication(X0,addition(X1,X2)))) ).
cnf(u199,axiom,
( ~ leq(multiplication(X0,multiplication(X1,addition(X2,X3))),multiplication(X0,X1))
| leq(multiplication(X0,multiplication(X1,multiplication(X3,star(X2)))),multiplication(X0,X1)) ) ).
cnf(u1860,axiom,
( ~ leq(addition(X0,addition(X1,omega(X2))),X2)
| leq(multiplication(addition(X0,X1),star(omega(X2))),X2) ) ).
cnf(u3145,axiom,
( ~ leq(multiplication(X0,multiplication(X1,X2)),multiplication(X0,X1))
| multiplication(X0,X1) = multiplication(X0,multiplication(X1,star(X2))) ) ).
cnf(u1380,axiom,
( multiplication(X3,addition(X0,addition(X1,X2))) != multiplication(X3,addition(X2,X0))
| leq(multiplication(X3,X1),multiplication(X3,addition(X2,X0))) ) ).
cnf(u158,axiom,
multiplication(X0,addition(omega(X0),X1)) = addition(omega(X0),multiplication(X0,X1)) ).
cnf(u1767,axiom,
( ~ leq(multiplication(X3,addition(X0,addition(X1,X2))),addition(X2,X0))
| leq(multiplication(star(X3),multiplication(X3,X1)),addition(X2,X0)) ) ).
cnf(u2620,axiom,
multiplication(addition(X0,addition(X1,X2)),omega(addition(X1,X0))) = multiplication(X2,omega(addition(X1,X0))) ).
cnf(u1116,axiom,
addition(X0,addition(X1,X2)) = addition(X1,addition(X0,X2)) ).
cnf(u2578,axiom,
( leq(multiplication(star(X0),multiplication(X0,multiplication(X1,X2))),X1)
| ~ leq(multiplication(X0,multiplication(X1,X2)),X1) ) ).
cnf(u2647,axiom,
multiplication(addition(X0,addition(X1,X2)),omega(addition(X0,X1))) = multiplication(X2,omega(addition(X0,X1))) ).
cnf(u3093,axiom,
multiplication(addition(X1,X0),X2) = addition(X0,multiplication(addition(X1,X0),X2)) ).
cnf(u2938,axiom,
multiplication(addition(X0,X2),X1) = addition(X0,multiplication(addition(X0,X2),X1)) ).
cnf(u3133,axiom,
( ~ leq(multiplication(addition(X0,X1),multiplication(X2,X3)),multiplication(X0,X2))
| leq(multiplication(X1,multiplication(X2,star(X3))),multiplication(X0,X2)) ) ).
cnf(u2730,axiom,
( multiplication(X0,X1) != X0
| leq(multiplication(X0,X1),X0) ) ).
cnf(u917,axiom,
( ~ leq(addition(omega(X1),addition(multiplication(X0,omega(X1)),X2)),addition(X1,X0))
| leq(multiplication(X2,star(omega(X1))),addition(X1,X0)) ) ).
cnf(u280,axiom,
( ~ test(X0)
| zero = multiplication(sK0(X0),X0) ) ).
cnf(u992,axiom,
leq(X2,addition(X0,addition(X1,X2))) ).
cnf(u3151,axiom,
( leq(multiplication(omega(X0),star(X1)),X0)
| ~ leq(multiplication(omega(X0),X1),X0) ) ).
cnf(u65,axiom,
( ~ complement(X1,X0)
| zero = multiplication(X1,X0) ) ).
cnf(u3269,axiom,
complement(X1,X0) ).
cnf(u384,axiom,
( multiplication(X1,X2) != multiplication(addition(X0,X1),X2)
| leq(multiplication(X0,X2),multiplication(X1,X2)) ) ).
cnf(u1744,axiom,
( ~ leq(multiplication(X4,addition(multiplication(X0,X1),addition(multiplication(X0,X2),X3))),multiplication(X0,addition(X1,X2)))
| leq(multiplication(star(X4),multiplication(X4,X3)),multiplication(X0,addition(X1,X2))) ) ).
cnf(u1779,axiom,
( ~ leq(multiplication(X4,addition(multiplication(X0,X1),addition(multiplication(X0,X2),X3))),X3)
| leq(multiplication(star(X4),multiplication(X4,multiplication(X0,addition(X1,X2)))),X3) ) ).
cnf(u3148,axiom,
( ~ leq(multiplication(X0,X1),X0)
| multiplication(X0,star(X1)) = X0 ) ).
cnf(u911,axiom,
multiplication(addition(X0,X1),addition(omega(X1),X2)) = addition(omega(X1),addition(multiplication(X0,omega(X1)),multiplication(addition(X0,X1),X2))) ).
cnf(u996,axiom,
( addition(X1,X0) != X0
| leq(addition(X1,X0),X0) ) ).
cnf(u1624,axiom,
leq(multiplication(X4,multiplication(X0,addition(X1,X2))),multiplication(X4,addition(multiplication(X0,X1),addition(multiplication(X0,X2),X3)))) ).
cnf(u1437,axiom,
addition(X0,addition(X1,addition(X2,X3))) = addition(X2,addition(X1,addition(X3,X0))) ).
cnf(u2568,axiom,
multiplication(addition(multiplication(X0,X1),addition(multiplication(X0,X2),X3)),omega(multiplication(X0,addition(X1,X2)))) = multiplication(X3,omega(multiplication(X0,addition(X1,X2)))) ).
cnf(u1728,axiom,
( ~ leq(multiplication(X2,addition(X0,X1)),X1)
| leq(multiplication(star(X2),multiplication(X2,X0)),X1) ) ).
cnf(u2979,axiom,
( ~ test(X0)
| zero = X0 ) ).
cnf(u2628,axiom,
( multiplication(X0,X1) != addition(X2,multiplication(X0,X1))
| leq(addition(X2,X0),multiplication(X0,X1)) ) ).
cnf(u59,axiom,
( ~ leq(addition(multiplication(X0,X1),X2),X0)
| leq(multiplication(X2,star(X1)),X0) ) ).
cnf(u45,axiom,
addition(X0,zero) = X0 ).
cnf(u1396,axiom,
( ~ leq(addition(X0,addition(multiplication(X1,X2),X3)),X1)
| leq(multiplication(addition(X3,X0),star(X2)),X1) ) ).
cnf(u2602,axiom,
leq(multiplication(X0,omega(X1)),multiplication(addition(X0,X1),addition(omega(X1),X2))) ).
cnf(u2780,axiom,
addition(X1,omega(X0)) = addition(X0,addition(omega(X0),X1)) ).
cnf(u581,axiom,
( multiplication(X3,multiplication(X0,addition(X1,X2))) != multiplication(X3,multiplication(X0,X2))
| leq(multiplication(X3,multiplication(X0,X1)),multiplication(X3,multiplication(X0,X2))) ) ).
cnf(u1625,axiom,
leq(multiplication(X0,addition(X1,X2)),addition(multiplication(X0,X1),addition(multiplication(X0,X2),X3))) ).
cnf(u2683,axiom,
multiplication(addition(X2,addition(X0,X1)),omega(X0)) = multiplication(addition(X2,X1),omega(X0)) ).
cnf(u3019,axiom,
( zero != multiplication(omega(X1),addition(X0,X1))
| zero != multiplication(X0,omega(X1))
| zero != addition(X1,addition(omega(X1),X0))
| complement(addition(X0,X1),omega(X1)) ) ).
cnf(u2665,axiom,
zero = star(zero) ).
cnf(u1449,axiom,
addition(X3,addition(X0,addition(X1,X2))) = addition(X2,addition(X0,addition(X1,X3))) ).
cnf(u1507,axiom,
( leq(multiplication(star(X1),addition(X0,multiplication(X1,X2))),X2)
| ~ leq(addition(X0,multiplication(X1,X2)),X2) ) ).
cnf(u948,axiom,
( leq(multiplication(X2,multiplication(addition(X0,X1),star(X0))),X2)
| ~ leq(multiplication(X2,addition(X0,X1)),X2) ) ).
cnf(u1859,axiom,
( ~ leq(addition(X0,addition(X1,omega(X2))),X2)
| leq(multiplication(addition(X1,X0),star(omega(X2))),X2) ) ).
cnf(u279,axiom,
( ~ test(X0)
| zero = multiplication(X0,sK0(X0)) ) ).
cnf(u2957,axiom,
multiplication(X0,addition(X1,X2)) = addition(X2,multiplication(X0,addition(X1,X2))) ).
cnf(u994,axiom,
leq(multiplication(X0,X2),multiplication(X0,addition(X1,X2))) ).
cnf(u2537,axiom,
( multiplication(X0,X1) != X1
| leq(multiplication(X0,X1),X1) ) ).
cnf(u175,axiom,
( multiplication(X0,addition(X1,X2)) != multiplication(X0,X2)
| leq(multiplication(X0,X1),multiplication(X0,X2)) ) ).
cnf(u863,axiom,
addition(multiplication(X0,X2),addition(multiplication(X1,X2),X3)) = addition(multiplication(addition(X0,X1),X2),X3) ).
cnf(u1392,axiom,
( addition(X0,addition(X1,X2)) != addition(X2,X0)
| leq(addition(X0,addition(X1,X2)),addition(X2,X0)) ) ).
cnf(u2529,axiom,
leq(X1,multiplication(X0,X1)) ).
cnf(u854,axiom,
addition(addition(X0,X1),X2) = addition(X1,addition(X0,X2)) ).
cnf(u178,axiom,
( ~ leq(multiplication(X0,addition(X1,X2)),X0)
| leq(multiplication(X0,multiplication(X1,star(X2))),X0) ) ).
cnf(u3283,axiom,
leq(X0,X1) ).
cnf(u369,axiom,
multiplication(addition(X3,multiplication(X0,X1)),X2) = addition(multiplication(X3,X2),multiplication(X0,multiplication(X1,X2))) ).
cnf(u1390,axiom,
leq(X1,addition(X0,addition(X1,X2))) ).
cnf(u2151,axiom,
multiplication(X0,zero) = X0 ).
cnf(u1730,axiom,
( leq(multiplication(star(X2),multiplication(X2,addition(X0,X1))),X1)
| ~ leq(multiplication(X2,addition(X0,X1)),X1) ) ).
cnf(u2944,axiom,
( omega(X0) != X0
| leq(omega(X0),X0) ) ).
cnf(u1104,axiom,
addition(multiplication(addition(X0,X1),X2),X3) = addition(multiplication(X1,X2),addition(multiplication(X0,X2),X3)) ).
cnf(u52,axiom,
zero = multiplication(X0,zero) ).
cnf(u2802,axiom,
multiplication(X2,addition(X1,X0)) = multiplication(X2,addition(X0,X1)) ).
cnf(u96,axiom,
( ~ leq(multiplication(X0,X1),X0)
| leq(zero,X0) ) ).
cnf(u2621,axiom,
omega(addition(X0,X1)) = multiplication(X1,omega(addition(X0,X1))) ).
cnf(u2190,axiom,
zero = sK0(zero) ).
cnf(u1122,axiom,
( addition(X1,X0) != addition(X0,addition(X1,X2))
| leq(X2,addition(X1,X0)) ) ).
cnf(u47,axiom,
multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2) ).
cnf(u2606,axiom,
zero = c(X0) ).
cnf(u2945,axiom,
( leq(multiplication(X1,multiplication(omega(X0),star(X0))),X1)
| ~ leq(multiplication(X1,omega(X0)),X1) ) ).
cnf(u3154,axiom,
( leq(multiplication(X0,star(omega(X1))),X1)
| ~ leq(multiplication(X0,omega(X1)),X1) ) ).
cnf(u1731,axiom,
( ~ leq(multiplication(X3,addition(X0,addition(X1,X2))),X2)
| leq(multiplication(star(X3),multiplication(X3,addition(X0,X1))),X2) ) ).
cnf(u2797,axiom,
omega(addition(X1,X0)) = addition(X0,addition(X1,omega(addition(X1,X0)))) ).
cnf(u163,axiom,
multiplication(X0,addition(X1,omega(X0))) = addition(multiplication(X0,X1),omega(X0)) ).
cnf(u3146,axiom,
( leq(multiplication(X0,multiplication(X1,star(X2))),X0)
| ~ leq(multiplication(X0,multiplication(X1,X2)),X0) ) ).
cnf(u50,axiom,
multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)) ).
cnf(u1140,axiom,
( ~ leq(addition(X0,addition(X1,multiplication(X2,X3))),X2)
| leq(multiplication(addition(X1,X0),star(X3)),X2) ) ).
cnf(u1264,axiom,
complement(zero,zero) ).
cnf(u3155,axiom,
( leq(multiplication(X1,star(omega(addition(X0,X1)))),X0)
| ~ leq(omega(addition(X0,X1)),X0) ) ).
cnf(u1391,axiom,
leq(addition(X2,X0),addition(X0,addition(X1,X2))) ).
cnf(u1765,axiom,
( ~ leq(multiplication(X2,addition(X0,X1)),addition(X0,X1))
| leq(multiplication(star(X2),multiplication(X2,X1)),addition(X0,X1)) ) ).
cnf(u2750,axiom,
multiplication(X1,addition(X0,X2)) = addition(X0,multiplication(X1,addition(X0,X2))) ).
cnf(u2188,axiom,
( ~ test(X0)
| zero = addition(X0,sK0(X0)) ) ).
cnf(u1602,axiom,
( ~ leq(addition(multiplication(X0,X1),addition(multiplication(X0,X2),X3)),X0)
| leq(multiplication(X3,star(addition(X1,X2))),X0) ) ).
cnf(u3094,axiom,
multiplication(X1,omega(X0)) = addition(X0,multiplication(X1,omega(X0))) ).
cnf(u2942,axiom,
( leq(multiplication(omega(multiplication(X0,X1)),star(X1)),X0)
| ~ leq(omega(multiplication(X0,X1)),X0) ) ).
cnf(u1742,axiom,
( ~ leq(multiplication(X3,multiplication(X0,addition(X1,X2))),multiplication(X0,X1))
| leq(multiplication(star(X3),multiplication(X3,multiplication(X0,X2))),multiplication(X0,X1)) ) ).
cnf(u2976,axiom,
( ~ leq(addition(X0,addition(omega(X0),X1)),omega(X0))
| leq(multiplication(star(X0),X1),omega(X0)) ) ).
cnf(u1743,axiom,
( ~ leq(multiplication(X3,multiplication(addition(X0,X1),X2)),multiplication(X0,X2))
| leq(multiplication(star(X3),multiplication(X3,multiplication(X1,X2))),multiplication(X0,X2)) ) ).
cnf(u2260,axiom,
( zero != multiplication(X2,multiplication(X0,X1))
| zero != multiplication(X0,multiplication(X1,X2))
| zero != addition(X2,multiplication(X0,X1))
| complement(multiplication(X0,X1),X2) ) ).
cnf(u3189,axiom,
zero = X0 ).
cnf(u1389,axiom,
leq(multiplication(X3,X1),multiplication(X3,addition(X0,addition(X1,X2)))) ).
cnf(u2267,axiom,
( zero != X0
| complement(X0,zero) ) ).
cnf(u3002,axiom,
star(X0) = multiplication(X0,star(X0)) ).
cnf(u1610,axiom,
( multiplication(X0,addition(X1,X2)) != addition(multiplication(X0,X1),addition(multiplication(X0,X2),X3))
| leq(X3,multiplication(X0,addition(X1,X2))) ) ).
cnf(u1035,axiom,
( multiplication(X1,X2) != multiplication(addition(X0,X1),X2)
| leq(multiplication(addition(X0,X1),X2),multiplication(X1,X2)) ) ).
cnf(u144,axiom,
( ~ leq(addition(X3,multiplication(X0,multiplication(X1,X2))),multiplication(X0,X1))
| leq(multiplication(X3,star(X2)),multiplication(X0,X1)) ) ).
cnf(u1622,axiom,
( addition(X4,addition(multiplication(X0,X1),addition(multiplication(X0,X2),X3))) != X3
| leq(addition(X4,multiplication(X0,addition(X1,X2))),X3) ) ).
cnf(u2971,axiom,
( leq(multiplication(star(addition(X1,X0)),multiplication(X0,omega(X1))),omega(X1))
| ~ leq(multiplication(X0,omega(X1)),omega(X1)) ) ).
cnf(u1578,axiom,
addition(multiplication(X3,multiplication(X0,X2)),addition(multiplication(X3,multiplication(X1,X2)),X4)) = addition(multiplication(X3,multiplication(addition(X0,X1),X2)),X4) ).
cnf(u2785,axiom,
( complement(X0,zero)
| ~ test(X0) ) ).
cnf(u1632,axiom,
addition(X3,multiplication(X0,addition(X1,X2))) = addition(multiplication(X0,X1),addition(multiplication(X0,X2),addition(X3,multiplication(X0,addition(X1,X2))))) ).
cnf(u54,axiom,
( ~ leq(X0,X1)
| addition(X0,X1) = X1 ) ).
cnf(u1125,axiom,
( multiplication(X3,X2) != multiplication(X3,addition(X0,addition(X1,X2)))
| leq(multiplication(X3,addition(X1,X0)),multiplication(X3,X2)) ) ).
cnf(u3105,axiom,
zero = addition(X0,omega(X0)) ).
cnf(u1533,axiom,
( ~ leq(addition(omega(X1),addition(multiplication(X0,omega(X1)),X2)),omega(X1))
| leq(multiplication(star(addition(X1,X0)),X2),omega(X1)) ) ).
cnf(u3137,axiom,
( leq(multiplication(addition(X0,X1),star(X2)),X1)
| ~ leq(multiplication(addition(X0,X1),X2),X1) ) ).
cnf(u582,axiom,
( multiplication(X3,multiplication(addition(X0,X1),X2)) != multiplication(X3,multiplication(X1,X2))
| leq(multiplication(X3,multiplication(X0,X2)),multiplication(X3,multiplication(X1,X2))) ) ).
cnf(u1034,axiom,
( multiplication(X0,addition(X1,X2)) != multiplication(X0,X2)
| leq(multiplication(X0,addition(X1,X2)),multiplication(X0,X2)) ) ).
cnf(u1485,axiom,
addition(X0,addition(X1,X2)) = addition(X0,addition(X2,addition(X0,X1))) ).
cnf(u3301,axiom,
leq(X0,zero) ).
cnf(u3142,axiom,
( leq(multiplication(X0,multiplication(X1,star(X2))),X1)
| ~ leq(multiplication(X0,multiplication(X1,X2)),X1) ) ).
cnf(u2598,axiom,
leq(multiplication(X2,X0),multiplication(X2,multiplication(X0,X1))) ).
cnf(u1739,axiom,
( ~ leq(multiplication(X3,addition(X0,addition(X1,X2))),addition(X1,X0))
| leq(multiplication(star(X3),multiplication(X3,X2)),addition(X1,X0)) ) ).
cnf(u1371,axiom,
addition(X1,X0) = addition(X0,addition(X0,X1)) ).
cnf(u1049,axiom,
addition(X0,addition(X1,X2)) = addition(X2,addition(X0,addition(X1,X2))) ).
cnf(u2782,axiom,
( ~ complement(X0,X1)
| zero = X1
| ~ test(X0) ) ).
cnf(u2958,axiom,
( ~ leq(addition(X0,addition(multiplication(X1,X0),X2)),X1)
| leq(multiplication(X2,star(X0)),X1) ) ).
cnf(u3143,axiom,
( ~ leq(multiplication(X0,X1),X0)
| leq(star(X1),X0) ) ).
cnf(u61,axiom,
( ~ leq(X0,addition(multiplication(X1,X0),X2))
| leq(X0,addition(omega(X1),multiplication(star(X1),X2))) ) ).
cnf(u94,axiom,
addition(zero,X0) = X0 ).
cnf(u1054,axiom,
( addition(X0,X1) != X1
| leq(addition(X1,X0),X1) ) ).
cnf(u2717,axiom,
( ~ leq(addition(X0,addition(omega(X0),X1)),X0)
| leq(multiplication(X1,star(omega(X0))),X0) ) ).
cnf(u83,axiom,
( ~ leq(addition(omega(X0),X1),X0)
| leq(multiplication(X1,star(omega(X0))),X0) ) ).
cnf(u1008,axiom,
( multiplication(X1,X2) != addition(X3,multiplication(addition(X0,X1),X2))
| leq(addition(X3,multiplication(X0,X2)),multiplication(X1,X2)) ) ).
cnf(u1613,axiom,
( multiplication(X4,X3) != multiplication(X4,addition(multiplication(X0,X1),addition(multiplication(X0,X2),X3)))
| leq(multiplication(X4,multiplication(X0,addition(X1,X2))),multiplication(X4,X3)) ) ).
cnf(u102,axiom,
leq(zero,X0) ).
cnf(u2824,axiom,
omega(addition(X0,X1)) = addition(X0,addition(X1,omega(addition(X0,X1)))) ).
cnf(u1509,axiom,
( ~ leq(addition(X0,addition(multiplication(X1,X2),X3)),X2)
| leq(multiplication(star(X1),addition(X3,X0)),X2) ) ).
cnf(u146,axiom,
( ~ leq(addition(multiplication(X0,multiplication(X1,X2)),X3),multiplication(X0,X1))
| leq(multiplication(X3,star(X2)),multiplication(X0,X1)) ) ).
cnf(u174,axiom,
( multiplication(X0,X1) != multiplication(X0,addition(X1,X2))
| leq(multiplication(X0,X2),multiplication(X0,X1)) ) ).
cnf(u3153,axiom,
( leq(star(omega(X0)),X0)
| ~ leq(omega(X0),X0) ) ).
cnf(u1609,axiom,
( addition(multiplication(X0,X1),addition(multiplication(X0,X2),X3)) != X3
| leq(multiplication(X0,addition(X1,X2)),X3) ) ).
cnf(u337,axiom,
zero = omega(zero) ).
cnf(u2594,axiom,
addition(X2,multiplication(X0,X1)) = addition(X0,addition(multiplication(X0,X1),X2)) ).
cnf(u2531,axiom,
( multiplication(X0,X1) != addition(X2,multiplication(X0,X1))
| leq(addition(X2,X1),multiplication(X0,X1)) ) ).
cnf(u3135,axiom,
( ~ leq(multiplication(addition(X0,addition(X1,X2)),X3),addition(X0,X1))
| leq(multiplication(X2,star(X3)),addition(X0,X1)) ) ).
cnf(u1329,axiom,
addition(X3,addition(X0,addition(X1,X2))) = addition(X2,addition(X3,addition(X0,X1))) ).
cnf(u2523,axiom,
( leq(multiplication(star(X1),multiplication(X0,multiplication(X1,X2))),X2)
| ~ leq(multiplication(X0,multiplication(X1,X2)),X2) ) ).
cnf(u916,axiom,
( ~ leq(addition(omega(X1),addition(multiplication(X0,omega(X1)),X2)),addition(X0,X1))
| leq(multiplication(X2,star(omega(X1))),addition(X0,X1)) ) ).
cnf(u2646,axiom,
multiplication(addition(X0,addition(X1,X2)),omega(X2)) = multiplication(addition(X0,X1),omega(X2)) ).
cnf(u1490,axiom,
( ~ leq(addition(omega(X0),X1),omega(X0))
| leq(multiplication(star(X0),X1),omega(X0)) ) ).
cnf(u2589,axiom,
( leq(multiplication(X2,star(addition(X1,X0))),X2)
| ~ leq(multiplication(X2,addition(X0,X1)),X2) ) ).
cnf(u1505,axiom,
( ~ leq(addition(X0,multiplication(X1,X2)),X2)
| leq(multiplication(star(X1),X0),X2) ) ).
cnf(u2741,axiom,
leq(multiplication(star(X0),X0),star(X0)) ).
cnf(u880,axiom,
( ~ leq(multiplication(X3,addition(X0,addition(X1,X2))),X3)
| leq(multiplication(X3,multiplication(X2,star(addition(X0,X1)))),X3) ) ).
cnf(u3277,axiom,
X0 = X1 ).
cnf(u2705,axiom,
multiplication(addition(X0,X1),omega(X1)) = multiplication(X0,omega(X1)) ).
cnf(u87,axiom,
( ~ leq(addition(X0,multiplication(X1,X2)),X1)
| leq(multiplication(X0,star(X2)),X1) ) ).
cnf(u1557,axiom,
leq(multiplication(star(X0),omega(X0)),omega(X0)) ).
cnf(u1103,axiom,
addition(multiplication(X0,addition(X1,X2)),X3) = addition(multiplication(X0,X2),addition(multiplication(X0,X1),X3)) ).
cnf(u1381,axiom,
( ~ leq(multiplication(X3,addition(X0,addition(X1,X2))),X3)
| leq(multiplication(X3,multiplication(addition(X2,X0),star(X1))),X3) ) ).
cnf(u2921,axiom,
multiplication(X0,multiplication(addition(X1,X2),omega(multiplication(X0,X1)))) = multiplication(X0,multiplication(X2,omega(multiplication(X0,X1)))) ).
cnf(u46,axiom,
addition(X0,X0) = X0 ).
cnf(u1007,axiom,
( multiplication(X0,X2) != addition(X3,multiplication(X0,addition(X1,X2)))
| leq(addition(X3,multiplication(X0,X1)),multiplication(X0,X2)) ) ).
cnf(u1359,axiom,
addition(multiplication(X0,X2),addition(multiplication(X1,X2),X3)) = addition(X3,multiplication(addition(X0,X1),X2)) ).
cnf(u998,axiom,
( addition(X2,addition(X0,X1)) != X0
| leq(addition(X2,X1),X0) ) ).
cnf(u150,axiom,
( leq(multiplication(X2,multiplication(X0,multiplication(X1,star(multiplication(X0,X1))))),X2)
| ~ leq(multiplication(X2,multiplication(X0,X1)),X2) ) ).
cnf(u953,axiom,
( leq(multiplication(addition(multiplication(X0,X1),X2),star(X1)),X0)
| ~ leq(addition(multiplication(X0,X1),X2),X0) ) ).
cnf(u1777,axiom,
( ~ leq(multiplication(X3,multiplication(X0,addition(X1,X2))),multiplication(X0,X2))
| leq(multiplication(star(X3),multiplication(X3,multiplication(X0,X1))),multiplication(X0,X2)) ) ).
cnf(u360,axiom,
multiplication(addition(multiplication(X0,X1),X3),X2) = addition(multiplication(X0,multiplication(X1,X2)),multiplication(X3,X2)) ).
cnf(u1292,axiom,
leq(multiplication(X3,addition(X1,X0)),multiplication(X3,addition(X0,addition(X1,X2)))) ).
cnf(u1331,axiom,
addition(X3,multiplication(X0,addition(X1,X2))) = addition(multiplication(X0,X2),addition(X3,multiplication(X0,X1))) ).
cnf(u2972,axiom,
( leq(multiplication(star(addition(X0,X1)),multiplication(X0,omega(X1))),omega(X1))
| ~ leq(multiplication(X0,omega(X1)),omega(X1)) ) ).
cnf(u2527,axiom,
( ~ leq(multiplication(X2,multiplication(X0,X1)),multiplication(X0,X1))
| leq(multiplication(star(X2),multiplication(X2,X1)),multiplication(X0,X1)) ) ).
cnf(u2975,axiom,
( ~ leq(addition(X0,addition(multiplication(X0,X1),X2)),X1)
| leq(multiplication(star(X0),X2),X1) ) ).
cnf(u1764,axiom,
( ~ leq(multiplication(X2,addition(X0,X1)),addition(X0,X1))
| leq(multiplication(star(X2),multiplication(X2,X0)),addition(X0,X1)) ) ).
cnf(u2970,axiom,
( ~ leq(multiplication(X0,X1),X1)
| multiplication(star(X0),multiplication(X0,X1)) = X1 ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : KLE179+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.04/0.31 % Computer : n012.cluster.edu
% 0.04/0.31 % Model : x86_64 x86_64
% 0.04/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.31 % Memory : 8046.5625MB
% 0.04/0.31 % OS : Linux 6.8.0-71-generic
% 0.04/0.31 % CPULimit : 300
% 0.04/0.31 % WCLimit : 300
% 0.04/0.31 % DateTime : Sun Sep 27 13:14:20 UTC 2026
% 0.04/0.31 % CPUTime :
% 0.04/0.31 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.33 Running first-order theorem proving
% 0.09/0.33 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
% 1.29/0.95 % (2383811)Detected formulas, will run a generic FOF schedule.
% 1.29/0.95 % (2383858)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=771833363:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 1.29/0.95 % (2383856)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=1005282394:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 1.29/0.95 % (2383861)dis-21_1_sil=8000:lcm=predicate:random_seed=2726905718: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)
% 1.29/0.95 % (2383857)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=4206661710:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 1.29/0.95 % (2383860)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1365651954:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 1.29/0.95 % (2383859)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1658055515:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 1.29/0.95 % (2383855)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=746661989:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 1.29/0.95 % (2383859)Refutation not found, incomplete strategy
% 1.29/0.95 % (2383859)------------------------------
% 1.29/0.95 % (2383859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.29/0.95 % (2383859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.29/0.95 % (2383861)Refutation not found, incomplete strategy
% 1.29/0.95 % (2383861)------------------------------
% 1.29/0.95 % (2383861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.29/0.95 % (2383858)Refutation not found, incomplete strategy
% 1.29/0.95 % (2383858)------------------------------
% 1.29/0.95 % (2383858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.29/0.95 % (2383861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.29/0.95 % (2383859)CaDiCaL version: 2.1.3
% 1.29/0.95 % (2383858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.29/0.95 % (2383859)Termination reason: Refutation not found, incomplete strategy
% 1.29/0.95 % (2383859)Time elapsed: 0.0000 s
% 1.29/0.95 % (2383861)CaDiCaL version: 2.1.3
% 1.29/0.95 % (2383859)Peak memory usage: 86 MB
% 1.29/0.95 % (2383861)Termination reason: Refutation not found, incomplete strategy
% 1.29/0.95 % (2383861)Time elapsed: 0.0000 s
% 1.29/0.95 % (2383858)CaDiCaL version: 2.1.3
% 1.29/0.95 % (2383861)Peak memory usage: 86 MB
% 1.29/0.95 % (2383858)Termination reason: Refutation not found, incomplete strategy
% 1.29/0.95 % (2383858)Time elapsed: 0.0000 s
% 1.29/0.95 % (2383858)Peak memory usage: 86 MB
% 1.29/0.95 % (2383860)Instruction limit reached!
% 1.29/0.95 % (2383860)------------------------------
% 1.29/0.95 % (2383860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.29/0.95 % (2383860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.29/0.95 % (2383860)CaDiCaL version: 2.1.3
% 1.29/0.95 % (2383860)Termination reason: Instruction limit
% 1.29/0.95 % (2383860)Termination phase: Saturation
% 1.29/0.95 % (2383860)Time elapsed: 0.045 s
% 1.29/0.95 % (2383860)Peak memory usage: 90 MB
% 1.29/0.95 % (2383860)Instructions burned: 139 (million)
% 1.29/0.95 % (2383861)------------------------------
% 1.29/0.95 % (2383861)------------------------------
% 1.29/0.95 % (2383859)------------------------------
% 1.29/0.95 % (2383859)------------------------------
% 1.29/0.95 % (2383858)------------------------------
% 1.29/0.95 % (2383858)------------------------------
% 1.29/0.95 % (2383869)lrs+10_1_sil=8000:sp=occurrence:random_seed=2990234186:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 1.29/0.95 % (2383869)Refutation not found, incomplete strategy
% 1.29/0.95 % (2383869)------------------------------
% 1.29/0.95 % (2383869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.29/0.95 % (2383869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.29/0.95 % (2383869)CaDiCaL version: 2.1.3
% 1.29/0.95 % (2383869)Termination reason: Refutation not found, incomplete strategy
% 1.29/0.95 % (2383869)Time elapsed: 0.0000 s
% 4.23/1.23 % (2383869)Peak memory usage: 86 MB
% 4.23/1.23 [W927 13:14:20.227143192 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.
% 4.23/1.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.23/1.23 [W927 13:14:20.227167289 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.
% 4.23/1.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.23/1.23 [W927 13:14:20.227169545 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.
% 4.23/1.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.23/1.23 [W927 13:14:20.227183194 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.
% 4.23/1.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.23/1.23 [W927 13:14:20.227188664 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.
% 4.23/1.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.23/1.23 [W927 13:14:20.227195195 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.
% 4.23/1.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.23/1.23 [W927 13:14:20.227205864 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.
% 4.23/1.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.23/1.23 [W927 13:14:20.227209948 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.
% 4.23/1.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.23/1.23 [W927 13:14:20.227213235 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.
% 4.23/1.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.23/1.23 [W927 13:14:20.227216748 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.
% 4.23/1.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.23/1.23 [W927 13:14:20.227227491 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.
% 4.23/1.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.23/1.23 [W927 13:14:20.227230311 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.
% 4.23/1.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.23/1.23 [W927 13:14:20.227234281 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.
% 4.23/1.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.84/1.50 [W927 13:14:20.227236107 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.
% 5.84/1.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.84/1.50 [W927 13:14:20.227248209 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.
% 5.84/1.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.84/1.50 [W927 13:14:20.227248761 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.
% 5.84/1.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.84/1.50 [W927 13:14:20.227253761 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.
% 5.84/1.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.84/1.50 [W927 13:14:20.227254352 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.
% 5.84/1.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.84/1.50 [W927 13:14:20.227266625 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.
% 5.84/1.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.84/1.50 [W927 13:14:20.227266869 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.
% 5.84/1.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.84/1.50 [W927 13:14:20.227272525 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.
% 5.84/1.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.84/1.50 [W927 13:14:20.227279875 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.
% 5.84/1.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.84/1.50 [W927 13:14:20.227294672 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.
% 5.84/1.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.84/1.50 [W927 13:14:20.227299948 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.
% 5.84/1.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.84/1.50 % (2383872)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=4253713709:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 5.84/1.50 % (2383870)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2508490354:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.84/1.50 % (2383871)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3817277314:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 5.84/1.50 % (2383871)Refutation not found, incomplete strategy
% 5.84/1.50 % (2383871)------------------------------
% 5.84/1.50 % (2383871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.71 % (2383871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.71 % (2383870)Refutation not found, incomplete strategy
% 6.96/1.71 % (2383870)------------------------------
% 6.96/1.71 % (2383870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.71 % (2383871)CaDiCaL version: 2.1.3
% 6.96/1.71 % (2383870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.71 % (2383870)CaDiCaL version: 2.1.3
% 6.96/1.71 % (2383870)Termination reason: Refutation not found, incomplete strategy
% 6.96/1.71 % (2383870)Time elapsed: 0.0000 s
% 6.96/1.71 % (2383871)Termination reason: Refutation not found, incomplete strategy
% 6.96/1.71 % (2383871)Time elapsed: 0.0000 s
% 6.96/1.71 % (2383871)Peak memory usage: 86 MB
% 6.96/1.71 % (2383870)Peak memory usage: 87 MB
% 6.96/1.71 % (2383857)Refutation not found, incomplete strategy
% 6.96/1.71 % (2383857)------------------------------
% 6.96/1.71 % (2383857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.71 % (2383857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.71 % (2383857)CaDiCaL version: 2.1.3
% 6.96/1.71 % (2383857)Termination reason: Refutation not found, incomplete strategy
% 6.96/1.71 % (2383857)Time elapsed: 0.305 s
% 6.96/1.71 % (2383857)Peak memory usage: 123 MB
% 6.96/1.71 % (2383857)Instructions burned: 826 (million)
% 6.96/1.71 % (2383856)Refutation not found, incomplete strategy
% 6.96/1.71 % (2383856)------------------------------
% 6.96/1.71 % (2383856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.71 % (2383856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.71 % (2383856)CaDiCaL version: 2.1.3
% 6.96/1.71 % (2383856)Termination reason: Refutation not found, incomplete strategy
% 6.96/1.71 % (2383856)Time elapsed: 0.306 s
% 6.96/1.71 % (2383856)Peak memory usage: 122 MB
% 6.96/1.71 % (2383856)Instructions burned: 826 (million)
% 6.96/1.71 % (2383869)------------------------------
% 6.96/1.71 % (2383869)------------------------------
% 6.96/1.71 % (2383872)Instruction limit reached!
% 6.96/1.71 % (2383872)------------------------------
% 6.96/1.71 % (2383872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.71 % (2383872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.71 % (2383872)CaDiCaL version: 2.1.3
% 6.96/1.71 % (2383872)Termination reason: Instruction limit
% 6.96/1.71 % (2383872)Termination phase: Saturation
% 6.96/1.71 % (2383872)Time elapsed: 0.088 s
% 6.96/1.71 % (2383872)Peak memory usage: 91 MB
% 6.96/1.71 % (2383872)Instructions burned: 249 (million)
% 6.96/1.71 % (2383870)------------------------------
% 6.96/1.71 % (2383870)------------------------------
% 6.96/1.71 % (2383871)------------------------------
% 6.96/1.71 % (2383871)------------------------------
% 6.96/1.71 % (2383856)------------------------------
% 6.96/1.71 % (2383856)------------------------------
% 6.96/1.71 % (2383857)------------------------------
% 6.96/1.71 % (2383857)------------------------------
% 6.96/1.71 % (2383877)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4125063157:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 6.96/1.71 % (2383877)Refutation not found, incomplete strategy
% 6.96/1.71 % (2383877)------------------------------
% 6.96/1.71 % (2383877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.71 % (2383877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.71 % (2383877)CaDiCaL version: 2.1.3
% 6.96/1.71 % (2383877)Termination reason: Refutation not found, incomplete strategy
% 6.96/1.71 % (2383877)Time elapsed: 0.0000 s
% 6.96/1.71 % (2383877)Peak memory usage: 86 MB
% 6.96/1.71 % (2383878)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1529937877:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 6.96/1.71 % (2383879)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3528082371:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 6.96/1.71 % (2383880)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2889302571:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 6.96/1.71 % (2383879)Refutation not found, incomplete strategy
% 6.96/1.71 % (2383879)------------------------------
% 6.96/1.71 % (2383879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.71 % (2383879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.73 % (2383879)CaDiCaL version: 2.1.3
% 6.96/1.73 % (2383879)Termination reason: Refutation not found, incomplete strategy
% 6.96/1.73 % (2383879)Time elapsed: 0.0000 s
% 6.96/1.73 % (2383879)Peak memory usage: 86 MB
% 6.96/1.73 % (2383880)Refutation not found, incomplete strategy
% 6.96/1.73 % (2383880)------------------------------
% 6.96/1.73 % (2383880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.73 % (2383880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.73 % (2383880)CaDiCaL version: 2.1.3
% 6.96/1.73 % (2383880)Termination reason: Refutation not found, incomplete strategy
% 6.96/1.73 % (2383880)Time elapsed: 0.001 s
% 6.96/1.73 % (2383880)Peak memory usage: 87 MB
% 6.96/1.73 % (2383855)Refutation not found, incomplete strategy
% 6.96/1.73 % (2383855)------------------------------
% 6.96/1.73 % (2383855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.73 % (2383855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.73 % (2383855)CaDiCaL version: 2.1.3
% 6.96/1.73 % (2383855)Termination reason: Refutation not found, incomplete strategy
% 6.96/1.73 % (2383855)Time elapsed: 0.584 s
% 6.96/1.73 % (2383855)Peak memory usage: 135 MB
% 6.96/1.73 % (2383855)Instructions burned: 1628 (million)
% 6.96/1.73 % (2383882)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3328630817:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 6.96/1.73 % (2383883)lrs+10_1_sil=8000:sp=occurrence:random_seed=24408196:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi)
% 6.96/1.73 % (2383882)Refutation not found, incomplete strategy
% 6.96/1.73 % (2383882)------------------------------
% 6.96/1.73 % (2383882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.73 % (2383883)Refutation not found, incomplete strategy
% 6.96/1.73 % (2383883)------------------------------
% 6.96/1.73 % (2383883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.73 % (2383883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.73 % (2383882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.73 % (2383883)CaDiCaL version: 2.1.3
% 6.96/1.73 % (2383883)Termination reason: Refutation not found, incomplete strategy
% 6.96/1.73 % (2383883)Time elapsed: 0.0000 s
% 6.96/1.73 % (2383882)CaDiCaL version: 2.1.3
% 6.96/1.73 % (2383883)Peak memory usage: 86 MB
% 6.96/1.73 % (2383882)Termination reason: Refutation not found, incomplete strategy
% 6.96/1.73 % (2383882)Time elapsed: 0.0000 s
% 6.96/1.73 % (2383882)Peak memory usage: 87 MB
% 6.96/1.73 % (2383877)------------------------------
% 6.96/1.73 % (2383877)------------------------------
% 6.96/1.73 % (2383880)------------------------------
% 6.96/1.73 % (2383880)------------------------------
% 6.96/1.73 % (2383879)------------------------------
% 6.96/1.73 % (2383879)------------------------------
% 6.96/1.73 % (2383883)------------------------------
% 6.96/1.73 % (2383883)------------------------------
% 6.96/1.73 % (2383882)------------------------------
% 6.96/1.73 % (2383882)------------------------------
% 6.96/1.73 % (2383855)------------------------------
% 6.96/1.73 % (2383855)------------------------------
% 6.96/1.73 % (2383889)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=289688719:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 6.96/1.73 % (2383889)Refutation not found, incomplete strategy
% 6.96/1.73 % (2383889)------------------------------
% 6.96/1.73 % (2383889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.73 % (2383889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.73 % (2383889)CaDiCaL version: 2.1.3
% 6.96/1.73 % (2383889)Termination reason: Refutation not found, incomplete strategy
% 6.96/1.73 % (2383889)Time elapsed: 0.0000 s
% 6.96/1.73 % (2383889)Peak memory usage: 86 MB
% 6.96/1.73 % (2383890)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2517025342:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 6.96/1.73 % (2383891)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=738971849:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2991 on theBenchmark for (2991ds/134Mi)
% 6.96/1.73 % (2383891)Refutation not found, incomplete strategy
% 6.96/1.73 % (2383891)------------------------------
% 6.96/1.73 % (2383891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.14/1.82 % (2383891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.82 % (2383891)CaDiCaL version: 2.1.3
% 7.14/1.82 % (2383891)Termination reason: Refutation not found, incomplete strategy
% 7.14/1.82 % (2383891)Time elapsed: 0.0000 s
% 7.14/1.82 % (2383891)Peak memory usage: 86 MB
% 7.14/1.82 % (2383893)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2789558696:st=3:i=13193:sd=3:ss=axioms_2991 on theBenchmark for (2991ds/13193Mi)
% 7.14/1.82 % (2383892)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=795801081:st=8:i=592:sd=3:ep=RST:ss=axioms_2991 on theBenchmark for (2991ds/592Mi)
% 7.14/1.82 % (2383892)Refutation not found, incomplete strategy
% 7.14/1.82 % (2383892)------------------------------
% 7.14/1.82 % (2383892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.14/1.82 % (2383892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.82 % (2383892)CaDiCaL version: 2.1.3
% 7.14/1.82 % (2383892)Termination reason: Refutation not found, incomplete strategy
% 7.14/1.82 % (2383892)Time elapsed: 0.0000 s
% 7.14/1.82 % (2383892)Peak memory usage: 86 MB
% 7.14/1.82 % (2383894)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=423353055:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/125Mi)
% 7.14/1.82 % (2383894)Refutation not found, incomplete strategy
% 7.14/1.82 % (2383894)------------------------------
% 7.14/1.82 % (2383894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.14/1.82 % (2383894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.82 % (2383894)CaDiCaL version: 2.1.3
% 7.14/1.82 % (2383894)Termination reason: Refutation not found, incomplete strategy
% 7.14/1.82 % (2383894)Time elapsed: 0.0000 s
% 7.14/1.82 % (2383894)Peak memory usage: 87 MB
% 7.14/1.82 % (2383889)------------------------------
% 7.14/1.82 % (2383889)------------------------------
% 7.14/1.82 % (2383891)------------------------------
% 7.14/1.82 % (2383891)------------------------------
% 7.14/1.82 % (2383892)------------------------------
% 7.14/1.82 % (2383892)------------------------------
% 7.14/1.82 % (2383894)------------------------------
% 7.14/1.82 % (2383894)------------------------------
% 7.14/1.82 [W927 13:14:21.067981961 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.14/1.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.14/1.82 [W927 13:14:21.068029224 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.14/1.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.14/1.82 [W927 13:14:21.068051346 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.14/1.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.14/1.82 [W927 13:14:21.068057731 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.14/1.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.14/1.82 [W927 13:14:21.068072554 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.14/1.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.14/1.82 [W927 13:14:21.068079040 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.14/1.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.14/1.82 [W927 13:14:21.068093880 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.06/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.06/2.12 [W927 13:14:21.068100133 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.06/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.06/2.12 [W927 13:14:21.068118620 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.06/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.06/2.12 [W927 13:14:21.068133719 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.06/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.06/2.12 [W927 13:14:21.068148560 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.06/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.06/2.12 [W927 13:14:21.068154142 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.06/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.06/2.12 % (2383901)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1669670428:i=134:gtgl=5:slsql=off:gtg=exists_sym_2989 on theBenchmark for (2989ds/134Mi)
% 11.06/2.12 [W927 13:14:21.082763460 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.06/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.06/2.12 [W927 13:14:21.082780899 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.06/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.06/2.12 [W927 13:14:21.082801984 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.06/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.06/2.12 [W927 13:14:21.082808679 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.06/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.06/2.12 [W927 13:14:21.082823083 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.06/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.06/2.12 [W927 13:14:21.082829279 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.06/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.06/2.12 [W927 13:14:21.082843279 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.
% 12.01/2.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.01/2.38 [W927 13:14:21.082849297 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.
% 12.01/2.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.01/2.38 [W927 13:14:21.082868100 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.
% 12.01/2.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.01/2.38 [W927 13:14:21.082882359 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.
% 12.01/2.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.01/2.38 [W927 13:14:21.082897145 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.
% 12.01/2.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.01/2.38 [W927 13:14:21.082902602 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.
% 12.01/2.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.01/2.38 % (2383901)Instruction limit reached!
% 12.01/2.38 % (2383901)------------------------------
% 12.01/2.38 % (2383901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.01/2.38 % (2383901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.01/2.38 % (2383901)CaDiCaL version: 2.1.3
% 12.01/2.38 % (2383901)Termination reason: Instruction limit
% 12.01/2.38 % (2383901)Termination phase: Saturation
% 12.01/2.38 % (2383901)Time elapsed: 0.046 s
% 12.01/2.38 % (2383901)Peak memory usage: 89 MB
% 12.01/2.38 % (2383901)Instructions burned: 134 (million)
% 12.01/2.38 % (2383902)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3992543352:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/141Mi)
% 12.01/2.38 % (2383902)Refutation not found, incomplete strategy
% 12.01/2.38 % (2383902)------------------------------
% 12.01/2.38 % (2383902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.01/2.38 % (2383902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.01/2.38 % (2383902)CaDiCaL version: 2.1.3
% 12.01/2.38 % (2383902)Termination reason: Refutation not found, incomplete strategy
% 12.01/2.38 % (2383902)Time elapsed: 0.0000 s
% 12.01/2.38 % (2383902)Peak memory usage: 86 MB
% 12.01/2.38 % (2383903)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1148809277:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2988 on theBenchmark for (2988ds/431Mi)
% 12.01/2.38 % (2383903)Refutation not found, incomplete strategy
% 12.01/2.38 % (2383903)------------------------------
% 12.01/2.38 % (2383903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.01/2.38 % (2383903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.01/2.38 % (2383903)CaDiCaL version: 2.1.3
% 12.01/2.38 % (2383903)Termination reason: Refutation not found, incomplete strategy
% 12.01/2.38 % (2383903)Time elapsed: 0.0000 s
% 12.01/2.38 % (2383903)Peak memory usage: 86 MB
% 12.01/2.38 % (2383890)Refutation not found, incomplete strategy
% 12.01/2.38 % (2383890)------------------------------
% 12.01/2.38 % (2383890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.01/2.38 % (2383890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.01/2.38 % (2383890)CaDiCaL version: 2.1.3
% 12.01/2.38 % (2383890)Termination reason: Refutation not found, incomplete strategy
% 12.01/2.38 % (2383890)Time elapsed: 0.318 s
% 12.01/2.38 % (2383890)Peak memory usage: 125 MB
% 12.01/2.38 % (2383890)Instructions burned: 825 (million)
% 12.01/2.38 % (2383904)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=3870103829:i=6060:aac=none:ins=25_2988 on theBenchmark for (2988ds/6060Mi)
% 12.45/2.48 % (2383893)Refutation not found, incomplete strategy
% 12.45/2.48 % (2383893)------------------------------
% 12.45/2.48 % (2383893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.45/2.48 % (2383893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.45/2.48 % (2383893)CaDiCaL version: 2.1.3
% 12.45/2.48 % (2383893)Termination reason: Refutation not found, incomplete strategy
% 12.45/2.48 % (2383893)Time elapsed: 0.313 s
% 12.45/2.48 % (2383893)Peak memory usage: 125 MB
% 12.45/2.48 % (2383893)Instructions burned: 820 (million)
% 12.45/2.48 % (2383907)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=1771422338:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2987 on theBenchmark for (2987ds/150Mi)
% 12.45/2.48 % (2383902)------------------------------
% 12.45/2.48 % (2383902)------------------------------
% 12.45/2.48 % (2383903)------------------------------
% 12.45/2.48 % (2383903)------------------------------
% 12.45/2.48 % (2383907)Instruction limit reached!
% 12.45/2.48 % (2383907)------------------------------
% 12.45/2.48 % (2383907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.45/2.48 % (2383907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.45/2.48 % (2383907)CaDiCaL version: 2.1.3
% 12.45/2.48 % (2383907)Termination reason: Instruction limit
% 12.45/2.48 % (2383907)Termination phase: Saturation
% 12.45/2.48 % (2383907)Time elapsed: 0.043 s
% 12.45/2.48 % (2383907)Peak memory usage: 90 MB
% 12.45/2.48 % (2383907)Instructions burned: 151 (million)
% 12.45/2.48 % (2383890)------------------------------
% 12.45/2.48 % (2383890)------------------------------
% 12.45/2.48 % (2383893)------------------------------
% 12.45/2.48 % (2383893)------------------------------
% 12.45/2.48 % (2383878)Instruction limit reached!
% 12.45/2.48 % (2383878)------------------------------
% 12.45/2.48 % (2383878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.45/2.48 % (2383878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.45/2.48 % (2383878)CaDiCaL version: 2.1.3
% 12.45/2.48 % (2383878)Termination reason: Instruction limit
% 12.45/2.48 % (2383878)Termination phase: Saturation
% 12.45/2.48 % (2383878)Time elapsed: 0.858 s
% 12.45/2.48 % (2383878)Peak memory usage: 141 MB
% 12.45/2.48 % (2383878)Instructions burned: 2351 (million)
% 12.45/2.48 % (2383912)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1955915235:i=667:av=off:fsr=off_2985 on theBenchmark for (2985ds/667Mi)
% 12.45/2.48 % (2383911)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3200236449:i=14155:bd=all_2985 on theBenchmark for (2985ds/14155Mi)
% 12.45/2.48 % (2383912)Refutation not found, incomplete strategy
% 12.45/2.48 % (2383912)------------------------------
% 12.45/2.48 % (2383912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.45/2.48 % (2383912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.45/2.48 % (2383912)CaDiCaL version: 2.1.3
% 12.45/2.48 % (2383912)Termination reason: Refutation not found, incomplete strategy
% 12.45/2.48 % (2383912)Time elapsed: 0.001 s
% 12.45/2.48 % (2383912)Peak memory usage: 88 MB
% 12.45/2.48 % (2383912)Instructions burned: 1 (million)
% 12.45/2.48 % (2383913)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=298002689:s2a=on:i=185:s2at=1.8:fdi=4_2985 on theBenchmark for (2985ds/185Mi)
% 12.45/2.48 % (2383914)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3789179947:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2985 on theBenchmark for (2985ds/193Mi)
% 12.45/2.48 % (2383914)Refutation not found, incomplete strategy
% 12.45/2.48 % (2383914)------------------------------
% 12.45/2.48 % (2383914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.45/2.48 % (2383914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.45/2.48 % (2383914)CaDiCaL version: 2.1.3
% 12.45/2.48 % (2383914)Termination reason: Refutation not found, incomplete strategy
% 12.45/2.48 % (2383914)Time elapsed: 0.0000 s
% 12.45/2.48 % (2383914)Peak memory usage: 86 MB
% 12.45/2.48 % (2383915)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=102337710:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2985 on theBenchmark for (2985ds/4850Mi)
% 14.52/2.73 % (2383915)Refutation not found, incomplete strategy
% 14.52/2.73 % (2383915)------------------------------
% 14.52/2.73 % (2383915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.52/2.73 % (2383915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.52/2.73 % (2383915)CaDiCaL version: 2.1.3
% 14.52/2.73 % (2383915)Termination reason: Refutation not found, incomplete strategy
% 14.52/2.73 % (2383915)Time elapsed: 0.0000 s
% 14.52/2.73 % (2383915)Peak memory usage: 86 MB
% 14.52/2.73 % (2383913)Instruction limit reached!
% 14.52/2.73 % (2383913)------------------------------
% 14.52/2.73 % (2383913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.52/2.73 % (2383913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.52/2.73 % (2383913)CaDiCaL version: 2.1.3
% 14.52/2.73 % (2383913)Termination reason: Instruction limit
% 14.52/2.73 % (2383913)Termination phase: Saturation
% 14.52/2.73 % (2383913)Time elapsed: 0.064 s
% 14.52/2.73 % (2383913)Peak memory usage: 91 MB
% 14.52/2.73 % (2383913)Instructions burned: 187 (million)
% 14.52/2.73 % (2383916)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3785257952:i=12111:sd=1:ss=included_2984 on theBenchmark for (2984ds/12111Mi)
% 14.52/2.73 % (2383912)------------------------------
% 14.52/2.73 % (2383912)------------------------------
% 14.52/2.73 % (2383914)------------------------------
% 14.52/2.73 % (2383914)------------------------------
% 14.52/2.73 % (2383922)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=300937791:i=319:kws=precedence:fsr=off_2983 on theBenchmark for (2983ds/319Mi)
% 14.52/2.73 % (2383915)------------------------------
% 14.52/2.73 % (2383915)------------------------------
% 14.52/2.73 % (2383924)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=459734896:i=2064:ep=RST_2983 on theBenchmark for (2983ds/2064Mi)
% 14.52/2.73 % (2383924)Refutation not found, incomplete strategy
% 14.52/2.73 % (2383924)------------------------------
% 14.52/2.73 % (2383924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.52/2.73 % (2383924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.52/2.73 % (2383924)CaDiCaL version: 2.1.3
% 14.52/2.73 % (2383924)Termination reason: Refutation not found, incomplete strategy
% 14.52/2.73 % (2383924)Time elapsed: 0.001 s
% 14.52/2.73 % (2383924)Peak memory usage: 88 MB
% 14.52/2.73 % (2383924)Instructions burned: 1 (million)
% 14.52/2.73 [W927 13:14:22.733912173 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.52/2.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 14.52/2.73 [W927 13:14:22.733934699 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.52/2.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 14.52/2.73 [W927 13:14:22.733973472 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.52/2.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 14.52/2.73 [W927 13:14:22.733979740 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.52/2.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 14.52/2.73 [W927 13:14:22.733992517 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.52/2.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 14.52/2.73 [W927 13:14:22.733998975 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.48/2.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.48/2.97 [W927 13:14:22.734021392 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.48/2.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.48/2.97 [W927 13:14:22.734027299 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.48/2.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.48/2.97 [W927 13:14:22.734039489 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.48/2.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.48/2.97 [W927 13:14:22.734045136 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.48/2.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.48/2.97 [W927 13:14:22.734058443 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.48/2.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.48/2.97 [W927 13:14:22.734063713 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.48/2.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.48/2.97 % (2383925)dis-1011_128_sil=32000:random_seed=3146804466:i=3706:ep=RST:av=off_2982 on theBenchmark for (2982ds/3706Mi)
% 15.48/2.97 % (2383925)Refutation not found, incomplete strategy
% 15.48/2.97 % (2383925)------------------------------
% 15.48/2.97 % (2383925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.48/2.97 % (2383925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/2.97 % (2383925)CaDiCaL version: 2.1.3
% 15.48/2.97 % (2383925)Termination reason: Refutation not found, incomplete strategy
% 15.48/2.97 % (2383925)Time elapsed: 0.001 s
% 15.48/2.97 % (2383925)Peak memory usage: 88 MB
% 15.48/2.97 % (2383925)Instructions burned: 2 (million)
% 15.48/2.97 % (2383922)Instruction limit reached!
% 15.48/2.97 % (2383922)------------------------------
% 15.48/2.97 % (2383922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.48/2.97 % (2383922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/2.97 % (2383922)CaDiCaL version: 2.1.3
% 15.48/2.97 % (2383922)Termination reason: Instruction limit
% 15.48/2.97 % (2383922)Termination phase: Saturation
% 15.48/2.97 % (2383922)Time elapsed: 0.110 s
% 15.48/2.97 % (2383922)Peak memory usage: 93 MB
% 15.48/2.97 % (2383922)Instructions burned: 321 (million)
% 15.48/2.97 % (2383927)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=149391497:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2982 on theBenchmark for (2982ds/757Mi)
% 15.48/2.97 % (2383927)Refutation not found, incomplete strategy
% 15.48/2.97 % (2383927)------------------------------
% 15.48/2.97 % (2383927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.48/2.97 % (2383927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/2.97 % (2383927)CaDiCaL version: 2.1.3
% 15.48/2.97 % (2383927)Termination reason: Refutation not found, incomplete strategy
% 15.48/2.97 % (2383927)Time elapsed: 0.0000 s
% 15.48/2.97 % (2383927)Peak memory usage: 86 MB
% 15.48/2.97 % (2383916)Refutation not found, incomplete strategy
% 15.48/2.97 % (2383916)------------------------------
% 15.48/2.97 % (2383916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.48/2.97 % (2383916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.53/3.08 % (2383916)CaDiCaL version: 2.1.3
% 17.53/3.08 % (2383916)Termination reason: Refutation not found, incomplete strategy
% 17.53/3.08 % (2383916)Time elapsed: 0.310 s
% 17.53/3.08 % (2383916)Peak memory usage: 125 MB
% 17.53/3.08 % (2383916)Instructions burned: 821 (million)
% 17.53/3.08 % (2383924)------------------------------
% 17.53/3.08 % (2383924)------------------------------
% 17.53/3.08 % (2383930)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2529056826:i=13913:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/13913Mi)
% 17.53/3.08 % (2383925)------------------------------
% 17.53/3.08 % (2383925)------------------------------
% 17.53/3.08 % (2383927)------------------------------
% 17.53/3.08 % (2383927)------------------------------
% 17.53/3.08 % (2383932)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=4245259594:i=9925:aac=none_2980 on theBenchmark for (2980ds/9925Mi)
% 17.53/3.08 % (2383916)------------------------------
% 17.53/3.08 % (2383916)------------------------------
% 17.53/3.08 % (2383934)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=51422891:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2979 on theBenchmark for (2979ds/2479Mi)
% 17.53/3.08 % (2383934)Refutation not found, incomplete strategy
% 17.53/3.08 % (2383934)------------------------------
% 17.53/3.08 % (2383934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.53/3.08 % (2383934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.53/3.08 % (2383934)CaDiCaL version: 2.1.3
% 17.53/3.08 % (2383934)Termination reason: Refutation not found, incomplete strategy
% 17.53/3.08 % (2383934)Time elapsed: 0.0000 s
% 17.53/3.08 % (2383934)Peak memory usage: 86 MB
% 17.53/3.08 % (2383935)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=4161833640:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2979 on theBenchmark for (2979ds/440Mi)
% 17.53/3.08 [W927 13:14:22.085300646 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.
% 17.53/3.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.53/3.08 [W927 13:14:22.085322631 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.
% 17.53/3.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.53/3.08 [W927 13:14:22.085343349 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.
% 17.53/3.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.53/3.08 [W927 13:14:22.085350105 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.
% 17.53/3.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.53/3.08 [W927 13:14:22.085364837 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.
% 17.53/3.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.53/3.08 [W927 13:14:22.085371132 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.
% 17.53/3.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.53/3.08 [W927 13:14:22.085384865 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.
% 17.53/3.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.53/3.08 [W927 13:14:22.085391087 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.
% 24.53/4.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.53/4.11 [W927 13:14:22.085404412 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.
% 24.53/4.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.53/4.11 [W927 13:14:22.085409862 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.
% 24.53/4.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.53/4.11 [W927 13:14:22.085422961 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.
% 24.53/4.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.53/4.11 [W927 13:14:22.085428412 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.
% 24.53/4.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.53/4.11 % (2383937)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2256099906:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2978 on theBenchmark for (2978ds/11145Mi)
% 24.53/4.11 % (2383934)------------------------------
% 24.53/4.11 % (2383934)------------------------------
% 24.53/4.11 % (2383930)Refutation not found, incomplete strategy
% 24.53/4.11 % (2383930)------------------------------
% 24.53/4.11 % (2383930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.53/4.11 % (2383930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.11 % (2383930)CaDiCaL version: 2.1.3
% 24.53/4.11 % (2383930)Termination reason: Refutation not found, incomplete strategy
% 24.53/4.11 % (2383930)Time elapsed: 0.313 s
% 24.53/4.11 % (2383930)Peak memory usage: 125 MB
% 24.53/4.11 % (2383930)Instructions burned: 824 (million)
% 24.53/4.11 % (2383935)Instruction limit reached!
% 24.53/4.11 % (2383935)------------------------------
% 24.53/4.11 % (2383935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.53/4.11 % (2383935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.11 % (2383935)CaDiCaL version: 2.1.3
% 24.53/4.11 % (2383935)Termination reason: Instruction limit
% 24.53/4.11 % (2383935)Termination phase: Saturation
% 24.53/4.11 % (2383935)Time elapsed: 0.129 s
% 24.53/4.11 % (2383935)Peak memory usage: 93 MB
% 24.53/4.11 % (2383935)Instructions burned: 441 (million)
% 24.53/4.11 % (2383932)Refutation not found, incomplete strategy
% 24.53/4.11 % (2383932)------------------------------
% 24.53/4.11 % (2383932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.53/4.11 % (2383932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.11 % (2383932)CaDiCaL version: 2.1.3
% 24.53/4.11 % (2383932)Termination reason: Refutation not found, incomplete strategy
% 24.53/4.11 % (2383932)Time elapsed: 0.316 s
% 24.53/4.11 % (2383932)Peak memory usage: 127 MB
% 24.53/4.11 % (2383932)Instructions burned: 832 (million)
% 24.53/4.11 % (2383941)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=4233771019:cts=off:i=3034:av=off:er=known:fsd=on_2977 on theBenchmark for (2977ds/3034Mi)
% 24.53/4.11 % (2383942)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3515922431:st=2:s2a=on:i=524:s2at=2:ss=axioms_2977 on theBenchmark for (2977ds/524Mi)
% 24.53/4.11 % (2383942)Refutation not found, incomplete strategy
% 24.53/4.11 % (2383942)------------------------------
% 24.53/4.11 % (2383942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.53/4.11 % (2383942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.11 % (2383942)CaDiCaL version: 2.1.3
% 24.53/4.11 % (2383942)Termination reason: Refutation not found, incomplete strategy
% 26.37/4.31 % (2383942)Time elapsed: 0.0000 s
% 26.37/4.31 % (2383942)Peak memory usage: 87 MB
% 26.37/4.31 [W927 13:14:22.335330458 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.
% 26.37/4.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.37/4.31 [W927 13:14:22.335352110 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.
% 26.37/4.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.37/4.31 [W927 13:14:22.335372984 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.
% 26.37/4.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.37/4.31 [W927 13:14:22.335379930 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.
% 26.37/4.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.37/4.31 [W927 13:14:22.335394154 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.
% 26.37/4.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.37/4.31 [W927 13:14:22.335400259 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.
% 26.37/4.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.37/4.31 [W927 13:14:22.335414464 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.
% 26.37/4.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.37/4.31 [W927 13:14:22.335420587 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.
% 26.37/4.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.37/4.31 [W927 13:14:22.335433610 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.
% 26.37/4.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.37/4.31 [W927 13:14:22.335439759 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.
% 26.37/4.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.37/4.31 [W927 13:14:22.335453100 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.
% 26.37/4.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.37/4.31 [W927 13:14:22.335459129 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.
% 26.37/4.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.37/4.31 % (2383930)------------------------------
% 26.37/4.31 % (2383930)------------------------------
% 26.37/4.31 % (2383937)Refutation not found, incomplete strategy
% 26.37/4.31 % (2383937)------------------------------
% 26.37/4.31 % (2383937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.98/4.41 % (2383937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.98/4.41 % (2383937)CaDiCaL version: 2.1.3
% 26.98/4.41 % (2383937)Termination reason: Refutation not found, incomplete strategy
% 26.98/4.41 % (2383937)Time elapsed: 0.308 s
% 26.98/4.41 % (2383937)Peak memory usage: 125 MB
% 26.98/4.41 % (2383937)Instructions burned: 825 (million)
% 26.98/4.41 % (2383932)------------------------------
% 26.98/4.41 % (2383932)------------------------------
% 26.98/4.41 % (2383942)------------------------------
% 26.98/4.41 % (2383942)------------------------------
% 26.98/4.41 % (2383945)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=963822340:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2975 on theBenchmark for (2975ds/1016Mi)
% 26.98/4.41 % (2383945)Refutation not found, incomplete strategy
% 26.98/4.41 % (2383945)------------------------------
% 26.98/4.41 % (2383945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.98/4.41 % (2383945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.98/4.41 % (2383945)CaDiCaL version: 2.1.3
% 26.98/4.41 % (2383945)Termination reason: Refutation not found, incomplete strategy
% 26.98/4.41 % (2383945)Time elapsed: 0.0000 s
% 26.98/4.41 % (2383945)Peak memory usage: 87 MB
% 26.98/4.41 % (2383946)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1177576591:i=14123:bd=preordered:ins=4_2974 on theBenchmark for (2974ds/14123Mi)
% 26.98/4.41 % (2383937)------------------------------
% 26.98/4.41 % (2383937)------------------------------
% 26.98/4.41 % (2383948)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=431129007:i=5781:kws=precedence:bd=all:rawr=on_2974 on theBenchmark for (2974ds/5781Mi)
% 26.98/4.41 % (2383945)------------------------------
% 26.98/4.41 % (2383945)------------------------------
% 26.98/4.41 % (2383950)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=3735493327:i=2448:gtgl=5:bd=preordered:gtg=all_2972 on theBenchmark for (2972ds/2448Mi)
% 26.98/4.41 % (2383952)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=4231577022:i=3223:kws=precedence:fgj=on:av=off_2972 on theBenchmark for (2972ds/3223Mi)
% 26.98/4.41 % (2383904)Refutation not found, incomplete strategy
% 26.98/4.41 % (2383904)------------------------------
% 26.98/4.41 % (2383904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.98/4.41 % (2383904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.98/4.41 % (2383904)CaDiCaL version: 2.1.3
% 26.98/4.41 % (2383904)Termination reason: Refutation not found, incomplete strategy
% 26.98/4.41 % (2383904)Time elapsed: 1.762 s
% 26.98/4.41 % (2383904)Peak memory usage: 179 MB
% 26.98/4.41 % (2383904)Instructions burned: 4981 (million)
% 26.98/4.41 % (2383904)------------------------------
% 26.98/4.41 % (2383904)------------------------------
% 26.98/4.41 % (2383955)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3504082618:st=5.6:i=2033:sd=3:ss=axioms_2967 on theBenchmark for (2967ds/2033Mi)
% 26.98/4.41 % (2383941)Instruction limit reached!
% 26.98/4.41 % (2383941)------------------------------
% 26.98/4.41 % (2383941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.98/4.41 % (2383941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.98/4.41 % (2383941)CaDiCaL version: 2.1.3
% 26.98/4.41 % (2383941)Termination reason: Instruction limit
% 26.98/4.41 % (2383941)Termination phase: Saturation
% 26.98/4.41 % (2383941)Time elapsed: 0.959 s
% 26.98/4.41 % (2383941)Peak memory usage: 134 MB
% 26.98/4.41 % (2383941)Instructions burned: 3036 (million)
% 26.98/4.41 % (2383957)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1925825903:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2966 on theBenchmark for (2966ds/2055Mi)
% 26.98/4.41 [W927 13:14:23.463348704 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.
% 26.98/4.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.98/4.41 [W927 13:14:23.463370057 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.
% 27.97/4.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.97/4.66 [W927 13:14:23.463406607 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.
% 27.97/4.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.97/4.66 [W927 13:14:23.463412493 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.
% 27.97/4.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.97/4.66 [W927 13:14:23.463425329 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.
% 27.97/4.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.97/4.66 [W927 13:14:23.463430687 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.
% 27.97/4.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.97/4.66 [W927 13:14:23.463446159 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.
% 27.97/4.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.97/4.66 [W927 13:14:23.463451708 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.
% 27.97/4.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.97/4.66 [W927 13:14:23.463473249 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.
% 27.97/4.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.97/4.66 [W927 13:14:23.463478573 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.
% 27.97/4.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.97/4.66 [W927 13:14:23.463491319 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.
% 27.97/4.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.97/4.66 [W927 13:14:23.463496485 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.
% 27.97/4.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.97/4.66 % (2383950)Instruction limit reached!
% 27.97/4.66 % (2383950)------------------------------
% 27.97/4.66 % (2383950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.97/4.66 % (2383950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.97/4.66 % (2383950)CaDiCaL version: 2.1.3
% 27.97/4.66 % (2383950)Termination reason: Instruction limit
% 27.97/4.66 % (2383950)Termination phase: Saturation
% 27.97/4.66 % (2383950)Time elapsed: 0.935 s
% 27.97/4.66 % (2383950)Peak memory usage: 147 MB
% 27.97/4.66 % (2383950)Instructions burned: 2702 (million)
% 27.97/4.66 % (2383955)Refutation not found, incomplete strategy
% 27.97/4.66 % (2383955)------------------------------
% 27.97/4.66 % (2383955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.97/4.66 % (2383955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.13/4.89 % (2383955)CaDiCaL version: 2.1.3
% 29.13/4.89 % (2383955)Termination reason: Refutation not found, incomplete strategy
% 29.13/4.89 % (2383955)Time elapsed: 0.407 s
% 29.13/4.89 % (2383955)Peak memory usage: 125 MB
% 29.13/4.89 % (2383955)Instructions burned: 825 (million)
% 29.13/4.89 [W927 13:14:24.668780788 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.
% 29.13/4.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 29.13/4.89 [W927 13:14:24.668801056 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.
% 29.13/4.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 29.13/4.89 [W927 13:14:24.668839647 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.
% 29.13/4.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 29.13/4.89 [W927 13:14:24.668845895 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.
% 29.13/4.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 29.13/4.89 [W927 13:14:24.668859504 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.
% 29.13/4.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 29.13/4.89 [W927 13:14:24.668865769 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.
% 29.13/4.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 29.13/4.89 [W927 13:14:24.668879692 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.
% 29.13/4.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 29.13/4.89 [W927 13:14:24.668885718 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.
% 29.13/4.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 29.13/4.89 [W927 13:14:24.668899807 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.
% 29.13/4.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 29.13/4.89 [W927 13:14:24.668905901 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.
% 29.13/4.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 29.13/4.89 [W927 13:14:24.668919708 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.
% 29.13/4.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 29.13/4.89 [W927 13:14:24.668925798 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.
% 29.13/4.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 29.13/4.89 % (2383957)Refutation not found, incomplete strategy
% 29.13/4.89 % (2383957)------------------------------
% 29.13/4.89 % (2383957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.42/5.47 % (2383957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.42/5.47 % (2383957)CaDiCaL version: 2.1.3
% 33.42/5.47 % (2383957)Termination reason: Refutation not found, incomplete strategy
% 33.42/5.47 % (2383957)Time elapsed: 0.373 s
% 33.42/5.47 % (2383957)Peak memory usage: 126 MB
% 33.42/5.47 % (2383957)Instructions burned: 824 (million)
% 33.42/5.47 % (2383959)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=3319719586:i=21611:sd=3:ss=axioms_2962 on theBenchmark for (2962ds/21611Mi)
% 33.42/5.47 % (2383955)------------------------------
% 33.42/5.47 % (2383955)------------------------------
% 33.42/5.47 % (2383952)Instruction limit reached!
% 33.42/5.47 % (2383952)------------------------------
% 33.42/5.47 % (2383952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.42/5.47 % (2383952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.42/5.47 % (2383952)CaDiCaL version: 2.1.3
% 33.42/5.47 % (2383952)Termination reason: Instruction limit
% 33.42/5.47 % (2383952)Termination phase: Saturation
% 33.42/5.47 % (2383952)Time elapsed: 1.060 s
% 33.42/5.47 % (2383952)Peak memory usage: 151 MB
% 33.42/5.47 % (2383952)Instructions burned: 3223 (million)
% 33.42/5.47 % (2383957)------------------------------
% 33.42/5.47 % (2383957)------------------------------
% 33.42/5.47 % (2383961)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=761407603:i=4835:sd=13:ss=axioms:sgt=23_2960 on theBenchmark for (2960ds/4835Mi)
% 33.42/5.47 % (2383961)Refutation not found, incomplete strategy
% 33.42/5.47 % (2383961)------------------------------
% 33.42/5.47 % (2383961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.42/5.47 % (2383961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.42/5.47 % (2383961)CaDiCaL version: 2.1.3
% 33.42/5.47 % (2383961)Termination reason: Refutation not found, incomplete strategy
% 33.42/5.47 % (2383961)Time elapsed: 0.0000 s
% 33.42/5.47 % (2383961)Peak memory usage: 86 MB
% 33.42/5.47 % (2383962)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=3056139580:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2960 on theBenchmark for (2960ds/797Mi)
% 33.42/5.47 % (2383962)Refutation not found, incomplete strategy
% 33.42/5.47 % (2383962)------------------------------
% 33.42/5.47 % (2383962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.42/5.47 % (2383962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.42/5.47 % (2383962)CaDiCaL version: 2.1.3
% 33.42/5.47 % (2383962)Termination reason: Refutation not found, incomplete strategy
% 33.42/5.47 % (2383962)Time elapsed: 0.0000 s
% 33.42/5.47 % (2383962)Peak memory usage: 86 MB
% 33.42/5.47 [W927 13:14:24.015234307 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.
% 33.42/5.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 33.42/5.47 [W927 13:14:24.015259208 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.
% 33.42/5.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 33.42/5.47 [W927 13:14:24.015279810 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.
% 33.42/5.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 33.42/5.47 [W927 13:14:24.015286912 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.
% 33.42/5.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 33.42/5.47 [W927 13:14:24.015299953 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.
% 35.07/5.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 35.07/5.70 [W927 13:14:24.015306639 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.
% 35.07/5.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 35.07/5.70 [W927 13:14:24.015326211 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.
% 35.07/5.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 35.07/5.70 [W927 13:14:24.015332049 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.
% 35.07/5.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 35.07/5.70 [W927 13:14:24.015344636 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.
% 35.07/5.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 35.07/5.70 [W927 13:14:24.015350235 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.
% 35.07/5.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 35.07/5.70 [W927 13:14:24.015363375 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.
% 35.07/5.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 35.07/5.70 [W927 13:14:24.015369122 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.
% 35.07/5.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 35.07/5.70 % (2383963)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2083493404:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2959 on theBenchmark for (2959ds/2326Mi)
% 35.07/5.70 % (2383963)Refutation not found, incomplete strategy
% 35.07/5.70 % (2383963)------------------------------
% 35.07/5.70 % (2383963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.07/5.70 % (2383963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.07/5.70 % (2383963)CaDiCaL version: 2.1.3
% 35.07/5.70 % (2383963)Termination reason: Refutation not found, incomplete strategy
% 35.07/5.70 % (2383963)Time elapsed: 0.001 s
% 35.07/5.70 % (2383963)Peak memory usage: 88 MB
% 35.07/5.70 % (2383963)Instructions burned: 1 (million)
% 35.07/5.70 % (2383961)------------------------------
% 35.07/5.70 % (2383961)------------------------------
% 35.07/5.70 % (2383959)Refutation not found, incomplete strategy
% 35.07/5.70 % (2383959)------------------------------
% 35.07/5.70 % (2383959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.07/5.70 % (2383959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.07/5.70 % (2383959)CaDiCaL version: 2.1.3
% 35.07/5.70 % (2383959)Termination reason: Refutation not found, incomplete strategy
% 35.07/5.70 % (2383959)Time elapsed: 0.307 s
% 35.07/5.70 % (2383959)Peak memory usage: 125 MB
% 35.07/5.70 % (2383959)Instructions burned: 821 (million)
% 35.07/5.70 % (2383962)------------------------------
% 35.07/5.70 % (2383962)------------------------------
% 35.07/5.70 % (2383963)------------------------------
% 35.07/5.70 % (2383963)------------------------------
% 35.07/5.70 % (2383967)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2455602822:i=6038:nm=6_2957 on theBenchmark for (2957ds/6038Mi)
% 35.07/5.70 % (2383968)lrs+10_1_sil=32000:sp=occurrence:random_seed=2818671049:st=2:i=33334:sd=3:ss=included:sgt=32_2957 on theBenchmark for (2957ds/33334Mi)
% 35.37/5.81 % (2383968)Refutation not found, incomplete strategy
% 35.37/5.81 % (2383968)------------------------------
% 35.37/5.81 % (2383968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.37/5.81 % (2383968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.37/5.81 % (2383968)CaDiCaL version: 2.1.3
% 35.37/5.81 % (2383968)Termination reason: Refutation not found, incomplete strategy
% 35.37/5.81 % (2383968)Time elapsed: 0.0000 s
% 35.37/5.81 % (2383968)Peak memory usage: 86 MB
% 35.37/5.81 % (2383959)------------------------------
% 35.37/5.81 % (2383959)------------------------------
% 35.37/5.81 % (2383969)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3105131721:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2956 on theBenchmark for (2956ds/1008Mi)
% 35.37/5.81 % (2383969)Refutation not found, incomplete strategy
% 35.37/5.81 % (2383969)------------------------------
% 35.37/5.81 % (2383969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.37/5.81 % (2383969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.37/5.81 % (2383969)CaDiCaL version: 2.1.3
% 35.37/5.81 % (2383969)Termination reason: Refutation not found, incomplete strategy
% 35.37/5.81 % (2383969)Time elapsed: 0.0000 s
% 35.37/5.81 % (2383969)Peak memory usage: 86 MB
% 35.37/5.81 % (2383968)------------------------------
% 35.37/5.81 % (2383968)------------------------------
% 35.37/5.81 % (2383972)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=99210575:i=8327:s2at=5:bd=preordered_2956 on theBenchmark for (2956ds/8327Mi)
% 35.37/5.81 % (2383948)Instruction limit reached!
% 35.37/5.81 % (2383948)------------------------------
% 35.37/5.81 % (2383948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.37/5.81 % (2383948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.37/5.81 % (2383948)CaDiCaL version: 2.1.3
% 35.37/5.81 % (2383948)Termination reason: Instruction limit
% 35.37/5.81 % (2383948)Termination phase: Saturation
% 35.37/5.81 % (2383948)Time elapsed: 1.800 s
% 35.37/5.81 % (2383948)Peak memory usage: 134 MB
% 35.37/5.81 % (2383948)Instructions burned: 5781 (million)
% 35.37/5.81 % (2383969)------------------------------
% 35.37/5.81 % (2383969)------------------------------
% 35.37/5.81 % (2383974)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=3743904262:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2954 on theBenchmark for (2954ds/1083Mi)
% 35.37/5.81 % (2383967)Refutation not found, incomplete strategy
% 35.37/5.81 % (2383967)------------------------------
% 35.37/5.81 % (2383967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.37/5.81 % (2383967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.37/5.81 % (2383967)CaDiCaL version: 2.1.3
% 35.37/5.81 % (2383967)Termination reason: Refutation not found, incomplete strategy
% 35.37/5.81 % (2383967)Time elapsed: 0.315 s
% 35.37/5.81 % (2383967)Peak memory usage: 127 MB
% 35.37/5.81 % (2383967)Instructions burned: 832 (million)
% 35.37/5.81 % (2383976)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=1832729068:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2954 on theBenchmark for (2954ds/1084Mi)
% 35.37/5.81 % (2383976)Refutation not found, incomplete strategy
% 35.37/5.81 % (2383976)------------------------------
% 35.37/5.81 % (2383976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.37/5.81 % (2383976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.37/5.81 % (2383976)CaDiCaL version: 2.1.3
% 35.37/5.81 % (2383976)Termination reason: Refutation not found, incomplete strategy
% 35.37/5.81 % (2383976)Time elapsed: 0.0000 s
% 35.37/5.81 % (2383976)Peak memory usage: 86 MB
% 35.37/5.81 % (2383977)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3935346493:i=6995:s2at=5:gtg=all_2954 on theBenchmark for (2954ds/6995Mi)
% 35.37/5.81 % (2383967)------------------------------
% 35.37/5.81 % (2383967)------------------------------
% 35.37/5.81 % (2383976)------------------------------
% 35.37/5.81 % (2383976)------------------------------
% 35.37/5.81 % (2383974)Instruction limit reached!
% 35.37/5.81 % (2383974)------------------------------
% 39.55/6.22 % (2383974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.55/6.22 % (2383974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.55/6.22 % (2383974)CaDiCaL version: 2.1.3
% 39.55/6.22 % (2383974)Termination reason: Instruction limit
% 39.55/6.22 % (2383974)Termination phase: Saturation
% 39.55/6.22 % (2383974)Time elapsed: 0.309 s
% 39.55/6.22 % (2383974)Peak memory usage: 102 MB
% 39.55/6.22 % (2383974)Instructions burned: 1086 (million)
% 39.55/6.22 % (2383982)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=4119650534:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2951 on theBenchmark for (2951ds/3372Mi)
% 39.55/6.22 % (2383981)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=3374225009:st=2:i=6225:sd=15:ss=axioms_2951 on theBenchmark for (2951ds/6225Mi)
% 39.55/6.22 % (2383981)Refutation not found, incomplete strategy
% 39.55/6.22 % (2383981)------------------------------
% 39.55/6.22 % (2383981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.55/6.22 % (2383981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.55/6.22 % (2383981)CaDiCaL version: 2.1.3
% 39.55/6.22 % (2383981)Termination reason: Refutation not found, incomplete strategy
% 39.55/6.22 % (2383981)Time elapsed: 0.0000 s
% 39.55/6.22 % (2383981)Peak memory usage: 86 MB
% 39.55/6.22 % (2383983)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=236100834:st=2.3:i=26457:sd=10:ss=included:sgt=8_2950 on theBenchmark for (2950ds/26457Mi)
% 39.55/6.22 % (2383981)------------------------------
% 39.55/6.22 % (2383981)------------------------------
% 39.55/6.22 [W927 13:14:25.053829413 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.053868191 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.053890399 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.053896751 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.053914919 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.053921656 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.053936017 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.053942569 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.053956607 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.053963132 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.053982459 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.053997516 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 % (2383987)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=1029904880:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2948 on theBenchmark for (2948ds/13494Mi)
% 39.55/6.22 % (2383982)Refutation not found, incomplete strategy
% 39.55/6.22 % (2383982)------------------------------
% 39.55/6.22 % (2383982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.55/6.22 % (2383982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.55/6.22 % (2383982)CaDiCaL version: 2.1.3
% 39.55/6.22 % (2383982)Termination reason: Refutation not found, incomplete strategy
% 39.55/6.22 % (2383982)Time elapsed: 0.313 s
% 39.55/6.22 % (2383982)Peak memory usage: 126 MB
% 39.55/6.22 % (2383982)Instructions burned: 824 (million)
% 39.55/6.22 [W927 13:14:25.167774140 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.167794771 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.167832156 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.167838103 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.167850621 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.167857127 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.167870363 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.167876409 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.167894423 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.167909930 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.167924844 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 [W927 13:14:25.167930214 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.
% 39.55/6.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.55/6.22 % (2383983)Refutation not found, incomplete strategy
% 39.55/6.22 % (2383983)------------------------------
% 39.55/6.22 % (2383983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.55/6.22 % (2383983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.55/6.22 % (2383983)CaDiCaL version: 2.1.3
% 39.55/6.22 % (2383983)Termination reason: Refutation not found, incomplete strategy
% 39.55/6.22 % (2383983)Time elapsed: 0.302 s
% 39.55/6.22 % (2383983)Peak memory usage: 125 MB
% 39.55/6.22 % (2383983)Instructions burned: 824 (million)
% 39.55/6.22 % (2383982)------------------------------
% 39.55/6.22 % (2383982)------------------------------
% 39.55/6.22 % (2383972)First to succeed.
% 39.55/6.22 % (2383972)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2383811"
% 39.55/6.22 % (2383983)------------------------------
% 39.55/6.22 % (2383983)------------------------------
% 39.55/6.22 % (2383989)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=1730625358:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2945 on theBenchmark for (2945ds/2503Mi)
% 39.55/6.22 % (2383911)Instruction limit reached!
% 39.55/6.22 % (2383911)------------------------------
% 39.55/6.22 % (2383911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.55/6.22 % (2383911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.55/6.22 % (2383911)CaDiCaL version: 2.1.3
% 39.55/6.22 % (2383911)Termination reason: Instruction limit
% 39.55/6.22 % (2383911)Termination phase: Saturation
% 39.55/6.22 % (2383911)Time elapsed: 4.083 s
% 39.55/6.22 % (2383911)Peak memory usage: 305 MB
% 39.55/6.22 % (2383911)Instructions burned: 14159 (million)
% 39.55/6.22 % (2383990)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=1702003245:i=2559:sd=1:ep=RSTC:ss=axioms_2944 on theBenchmark for (2944ds/2559Mi)
% 39.55/6.22 % SZS status Satisfiable for theBenchmark
% 39.55/6.22 % SZS output start Saturation.
% See solution above
% 39.96/6.31 % SZS output start Definitions and Model Updates.
% 39.96/6.31 for all inputs,
% 39.96/6.31 define ismeet(X2,X0,X1) := leq(X2,X0) & leq(X2,X1) & ! [X3] : ((leq(X3,X0) & leq(X3,X1)) => leq(X3,X2))
% 39.96/6.31 for all inputs,
% 39.96/6.31 define ismeetu(X2,X0,X1) := ! [X3] : ((leq(X3,X0) & leq(X3,X1)) <=> leq(X3,X2))
% 39.96/6.31 % SZS output end Definitions and Model Updates.
% 39.96/6.31 % (2383972)------------------------------
% 39.96/6.31 % (2383972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.96/6.31 % (2383972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.96/6.31 % (2383972)CaDiCaL version: 2.1.3
% 39.96/6.31 % (2383972)Termination reason: Satisfiable
% 39.96/6.31 % (2383972)Time elapsed: 0.988 s
% 39.96/6.31 % (2383972)Peak memory usage: 156 MB
% 39.96/6.31 % (2383972)Instructions burned: 2851 (million)
% 39.96/6.31 % (2383972)------------------------------
% 39.96/6.31 % (2383972)------------------------------
% 39.96/6.31 % (2383811)Success in time 5.682 s
% 39.96/6.31 % Vampire exiting
%------------------------------------------------------------------------------