%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL909+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n015.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:56:59 AM UTC 2026
% Result : Satisfiable 19.41s 3.77s
% Output : Saturation 21.16s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u85,axiom,
op_implies_or ).
cnf(u90,axiom,
op_and ).
cnf(u95,axiom,
op_equiv ).
cnf(u100,axiom,
modus_ponens ).
cnf(u105,axiom,
r1 ).
cnf(u110,axiom,
r2 ).
cnf(u115,axiom,
r3 ).
cnf(u120,axiom,
r4 ).
cnf(u125,axiom,
r5 ).
cnf(u130,axiom,
substitution_of_equivalents ).
cnf(u134,axiom,
is_a_theorem(implies(or(X0,X0),X0)) ).
cnf(u138,axiom,
is_a_theorem(implies(X1,or(X0,X1))) ).
cnf(u142,axiom,
( ~ is_a_theorem(equiv(X0,X1))
| X0 = X1 ) ).
cnf(u146,axiom,
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(implies(X0,X1)) ) ).
cnf(u151,axiom,
is_a_theorem(implies(or(X0,X1),or(X1,X0))) ).
cnf(u155,axiom,
implies(X0,X1) = or(not(X0),X1) ).
cnf(u163,axiom,
is_a_theorem(implies(X1,implies(X0,X1))) ).
cnf(u167,axiom,
and(X0,X1) = not(or(not(X0),not(X1))) ).
cnf(u172,axiom,
is_a_theorem(implies(implies(X0,not(X0)),not(X0))) ).
cnf(u176,axiom,
and(X0,X1) = not(implies(X0,not(X1))) ).
cnf(u184,axiom,
is_a_theorem(implies(or(X1,not(X0)),implies(X0,X1))) ).
cnf(u188,axiom,
is_a_theorem(implies(implies(X0,X1),or(X1,not(X0)))) ).
cnf(u200,axiom,
is_a_theorem(or(and(X0,X1),implies(X1,not(X0)))) ).
cnf(u205,axiom,
( ~ is_a_theorem(implies(X0,equiv(X1,X2)))
| ~ is_a_theorem(X0)
| X1 = X2 ) ).
cnf(u211,axiom,
( ~ is_a_theorem(or(equiv(X0,X1),equiv(X0,X1)))
| X0 = X1 ) ).
cnf(u216,axiom,
equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0)) ).
cnf(u221,axiom,
implies(implies(X0,not(X1)),X2) = or(and(X0,X1),X2) ).
cnf(u247,axiom,
is_a_theorem(or(and(X0,X0),not(X0))) ).
cnf(u256,axiom,
is_a_theorem(or(equiv(X0,X0),not(implies(X0,X0)))) ).
cnf(u262,axiom,
is_a_theorem(or(and(X0,X1),implies(X2,implies(X0,not(X1))))) ).
cnf(u266,axiom,
is_a_theorem(or(and(X0,X1),or(X2,implies(X0,not(X1))))) ).
cnf(u282,axiom,
is_a_theorem(or(equiv(not(X0),not(X0)),and(not(X0),X0))) ).
cnf(u288,axiom,
is_a_theorem(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))) ).
cnf(u300,axiom,
is_a_theorem(implies(or(X1,implies(X0,X2)),implies(X0,or(X1,X2)))) ).
cnf(u304,axiom,
is_a_theorem(implies(implies(X0,or(X2,X1)),or(X2,implies(X0,X1)))) ).
cnf(u308,axiom,
is_a_theorem(implies(implies(X1,X2),implies(or(X0,X1),or(X0,X2)))) ).
cnf(u334,axiom,
is_a_theorem(implies(implies(X2,X1),implies(implies(X0,X2),implies(X0,X1)))) ).
cnf(u345,axiom,
is_a_theorem(implies(implies(X0,implies(X2,X1)),implies(X2,implies(X0,X1)))) ).
cnf(u357,axiom,
and(X2,implies(X0,not(X1))) = not(implies(X2,and(X0,X1))) ).
cnf(u381,axiom,
is_a_theorem(or(and(X0,X1),implies(or(X2,X0),or(X2,not(X1))))) ).
cnf(u385,axiom,
is_a_theorem(implies(implies(not(X1),X2),or(and(X0,X1),implies(X0,X2)))) ).
cnf(u389,axiom,
is_a_theorem(or(and(X0,X1),implies(implies(X2,X0),implies(X2,not(X1))))) ).
cnf(u425,axiom,
is_a_theorem(or(and(implies(X0,not(X1)),X2),implies(X2,and(X0,X1)))) ).
cnf(u429,axiom,
is_a_theorem(or(equiv(X0,X1),implies(implies(X1,X0),not(implies(X0,X1))))) ).
cnf(u452,axiom,
and(implies(X0,not(X1)),X2) = not(or(and(X0,X1),not(X2))) ).
cnf(u456,axiom,
equiv(not(X0),X1) = not(implies(implies(not(X0),X1),and(X1,X0))) ).
cnf(u516,axiom,
is_a_theorem(or(and(not(X0),X1),or(and(X2,X0),implies(X2,not(X1))))) ).
cnf(u542,axiom,
is_a_theorem(or(equiv(X0,not(X1)),implies(implies(not(X1),X0),and(X0,X1)))) ).
cnf(u555,axiom,
( ~ is_a_theorem(implies(X3,implies(X0,equiv(X1,X2))))
| X1 = X2
| ~ is_a_theorem(X3)
| ~ is_a_theorem(X0) ) ).
cnf(u565,axiom,
( ~ is_a_theorem(or(equiv(X0,X1),not(X2)))
| X0 = X1
| ~ is_a_theorem(X2) ) ).
cnf(u574,axiom,
( ~ is_a_theorem(implies(X2,or(equiv(X0,X1),equiv(X0,X1))))
| ~ is_a_theorem(X2)
| X0 = X1 ) ).
cnf(u578,axiom,
( ~ is_a_theorem(or(and(X0,X1),equiv(X2,X3)))
| ~ is_a_theorem(implies(X0,not(X1)))
| X2 = X3 ) ).
cnf(u582,axiom,
is_a_theorem(or(equiv(X0,X1),implies(X2,implies(implies(X0,X1),not(implies(X1,X0)))))) ).
cnf(u586,axiom,
is_a_theorem(or(equiv(X0,X1),or(X2,implies(implies(X0,X1),not(implies(X1,X0)))))) ).
cnf(u607,axiom,
is_a_theorem(or(equiv(not(X1),X0),or(and(X0,X1),not(implies(not(X1),X0))))) ).
cnf(u628,axiom,
is_a_theorem(or(and(implies(X0,not(X1)),X2),implies(X3,or(and(X0,X1),not(X2))))) ).
cnf(u632,axiom,
is_a_theorem(or(and(implies(X0,not(X1)),X2),or(X3,or(and(X0,X1),not(X2))))) ).
cnf(u636,axiom,
equiv(not(X0),not(X1)) = not(or(and(not(X0),X1),and(not(X1),X0))) ).
cnf(u752,axiom,
( ~ is_a_theorem(implies(X3,or(equiv(X0,X1),not(X2))))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(X3)
| X0 = X1 ) ).
cnf(u756,axiom,
( ~ is_a_theorem(or(equiv(X2,X3),and(X0,X1)))
| X2 = X3
| ~ is_a_theorem(implies(X0,not(X1))) ) ).
cnf(u760,axiom,
is_a_theorem(or(equiv(not(X1),X0),implies(X2,implies(implies(not(X1),X0),and(X0,X1))))) ).
cnf(u764,axiom,
is_a_theorem(or(equiv(not(X1),X0),or(X2,implies(implies(not(X1),X0),and(X0,X1))))) ).
cnf(u779,axiom,
X1 = X2 ).
cnf(u1222,axiom,
is_a_theorem(X0) ).
cnf(u1277,axiom,
or(and(implies(X0,not(X1)),X2),X3) = implies(or(and(X0,X1),not(X2)),X3) ).
cnf(u1303,axiom,
is_a_theorem(or(equiv(not(X1),not(X0)),or(and(not(X0),X1),and(not(X1),X0)))) ).
cnf(u1307,axiom,
is_a_theorem(implies(or(and(X0,X1),X2),implies(or(X3,implies(X0,not(X1))),or(X3,X2)))) ).
cnf(u1311,axiom,
is_a_theorem(implies(or(and(X0,X1),X2),implies(implies(X3,implies(X0,not(X1))),implies(X3,X2)))) ).
cnf(u1315,axiom,
is_a_theorem(or(equiv(X0,X1),implies(or(X2,implies(X0,X1)),or(X2,not(implies(X1,X0)))))) ).
cnf(u1319,axiom,
is_a_theorem(implies(implies(not(implies(X1,X0)),X2),or(equiv(X0,X1),implies(implies(X0,X1),X2)))) ).
cnf(u1323,axiom,
is_a_theorem(or(equiv(X0,X1),implies(implies(X2,implies(X0,X1)),implies(X2,not(implies(X1,X0)))))) ).
cnf(u1327,axiom,
implies(implies(implies(not(X0),X1),and(X1,X0)),X2) = or(equiv(not(X0),X1),X2) ).
cnf(u1331,axiom,
( X0 = X1
| ~ is_a_theorem(or(implies(X2,equiv(X0,X1)),implies(X2,equiv(X0,X1))))
| ~ is_a_theorem(X2) ) ).
cnf(u1335,axiom,
is_a_theorem(or(and(implies(implies(X0,X1),not(implies(X1,X0))),X2),implies(X2,equiv(X0,X1)))) ).
cnf(u1339,axiom,
is_a_theorem(or(equiv(X0,not(X1)),implies(X2,or(and(X0,X1),not(implies(not(X1),X0)))))) ).
cnf(u1343,axiom,
is_a_theorem(or(equiv(X0,not(X1)),or(X2,or(and(X0,X1),not(implies(not(X1),X0)))))) ).
cnf(u1347,axiom,
not(implies(X3,and(implies(X0,not(X1)),X2))) = and(X3,or(and(X0,X1),not(X2))) ).
cnf(u1351,axiom,
is_a_theorem(implies(implies(not(X3),X2),or(and(implies(X0,not(X1)),X3),or(and(X0,X1),X2)))) ).
cnf(u1355,axiom,
and(implies(implies(X0,X1),not(implies(X1,X0))),X2) = not(or(equiv(X0,X1),not(X2))) ).
cnf(u1359,axiom,
and(X2,implies(implies(not(X0),X1),and(X1,X0))) = not(implies(X2,equiv(not(X0),X1))) ).
cnf(u1363,axiom,
is_a_theorem(implies(or(X2,equiv(not(X0),X1)),implies(implies(implies(not(X0),X1),and(X1,X0)),X2))) ).
cnf(u1367,axiom,
is_a_theorem(implies(implies(implies(implies(not(X0),X1),and(X1,X0)),X2),or(X2,equiv(not(X0),X1)))) ).
cnf(u1371,axiom,
is_a_theorem(or(and(implies(implies(not(X0),X1),and(X1,X0)),X2),implies(X2,equiv(not(X0),X1)))) ).
cnf(u1375,axiom,
is_a_theorem(or(and(or(and(X0,X1),not(X2)),X3),implies(X3,and(implies(X0,not(X1)),X2)))) ).
cnf(u1379,axiom,
is_a_theorem(or(and(not(implies(X1,X0)),X2),or(equiv(X0,X1),implies(implies(X0,X1),not(X2))))) ).
cnf(u1383,axiom,
equiv(X2,implies(X0,not(X1))) = and(implies(X2,implies(X0,not(X1))),or(and(X0,X1),X2)) ).
cnf(u1387,axiom,
equiv(implies(X0,not(X1)),X2) = and(or(and(X0,X1),X2),implies(X2,implies(X0,not(X1)))) ).
cnf(u1391,axiom,
is_a_theorem(implies(implies(implies(implies(not(X0),X1),and(X1,X0)),equiv(not(X0),X1)),equiv(not(X0),X1))) ).
cnf(u1395,axiom,
( X0 = X1
| ~ is_a_theorem(X2)
| ~ is_a_theorem(X3)
| ~ is_a_theorem(X4)
| ~ is_a_theorem(implies(X4,implies(X2,implies(X3,equiv(X0,X1))))) ) ).
cnf(u1399,axiom,
is_a_theorem(or(and(not(X3),X2),or(and(implies(X0,not(X1)),X3),or(and(X0,X1),not(X2))))) ).
cnf(u1403,axiom,
( ~ is_a_theorem(or(or(equiv(X0,X1),equiv(X0,X1)),or(equiv(X0,X1),equiv(X0,X1))))
| X0 = X1 ) ).
cnf(u1407,axiom,
( ~ is_a_theorem(X0)
| X1 = X2
| ~ is_a_theorem(X3)
| ~ is_a_theorem(implies(X3,implies(X0,or(equiv(X1,X2),equiv(X1,X2))))) ) ).
cnf(u1411,axiom,
implies(or(and(not(X0),X1),and(not(X1),X0)),X2) = or(equiv(not(X0),not(X1)),X2) ).
cnf(u1415,axiom,
( ~ is_a_theorem(X0)
| ~ is_a_theorem(or(or(equiv(X1,X2),not(X0)),or(equiv(X1,X2),not(X0))))
| X1 = X2 ) ).
cnf(u1419,axiom,
is_a_theorem(or(and(X3,or(and(X0,X1),not(X2))),implies(X4,implies(X3,and(implies(X0,not(X1)),X2))))) ).
cnf(u1423,axiom,
is_a_theorem(or(and(X3,or(and(X0,X1),not(X2))),or(X4,implies(X3,and(implies(X0,not(X1)),X2))))) ).
cnf(u1427,axiom,
is_a_theorem(or(and(X2,implies(implies(not(X0),X1),and(X1,X0))),implies(X3,implies(X2,equiv(not(X0),X1))))) ).
cnf(u1431,axiom,
is_a_theorem(or(and(X2,implies(implies(not(X0),X1),and(X1,X0))),or(X3,implies(X2,equiv(not(X0),X1))))) ).
cnf(u1435,axiom,
( ~ is_a_theorem(implies(X4,or(and(X0,X1),equiv(X2,X3))))
| X2 = X3
| ~ is_a_theorem(X4)
| ~ is_a_theorem(implies(X0,not(X1))) ) ).
cnf(u1439,axiom,
( ~ is_a_theorem(or(and(X0,X1),implies(X2,equiv(X3,X4))))
| X3 = X4
| ~ is_a_theorem(implies(X0,not(X1)))
| ~ is_a_theorem(X2) ) ).
cnf(u1443,axiom,
( ~ is_a_theorem(or(equiv(X0,X1),equiv(X2,X3)))
| ~ is_a_theorem(implies(implies(X0,X1),not(implies(X1,X0))))
| X2 = X3 ) ).
cnf(u1447,axiom,
is_a_theorem(or(equiv(implies(X0,not(X1)),implies(X0,not(X1))),not(or(and(X0,X1),implies(X0,not(X1)))))) ).
cnf(u1451,axiom,
( ~ is_a_theorem(or(and(X0,X1),or(equiv(X2,X3),equiv(X2,X3))))
| ~ is_a_theorem(implies(X0,not(X1)))
| X2 = X3 ) ).
cnf(u1455,axiom,
and(X2,or(and(not(X0),X1),and(not(X1),X0))) = not(implies(X2,equiv(not(X0),not(X1)))) ).
cnf(u1459,axiom,
is_a_theorem(implies(or(X2,equiv(not(X0),not(X1))),implies(or(and(not(X0),X1),and(not(X1),X0)),X2))) ).
cnf(u1463,axiom,
is_a_theorem(implies(implies(or(and(not(X0),X1),and(not(X1),X0)),X2),or(X2,equiv(not(X0),not(X1))))) ).
cnf(u1467,axiom,
is_a_theorem(or(and(or(and(not(X0),X1),and(not(X1),X0)),X2),implies(X2,equiv(not(X0),not(X1))))) ).
cnf(u1471,axiom,
( ~ is_a_theorem(X0)
| ~ is_a_theorem(X1)
| X2 = X3
| ~ is_a_theorem(X4)
| ~ is_a_theorem(implies(X4,implies(X1,or(equiv(X2,X3),not(X0))))) ) ).
cnf(u1475,axiom,
( ~ is_a_theorem(implies(X2,or(equiv(X3,X4),and(X0,X1))))
| ~ is_a_theorem(implies(X0,not(X1)))
| ~ is_a_theorem(X2)
| X3 = X4 ) ).
cnf(u1479,axiom,
or(and(X3,or(and(X0,X1),not(X2))),X4) = implies(implies(X3,and(implies(X0,not(X1)),X2)),X4) ).
cnf(u1483,axiom,
is_a_theorem(or(and(or(and(X0,X1),not(X2)),or(and(X0,X1),not(X2))),and(implies(X0,not(X1)),X2))) ).
cnf(u1487,axiom,
or(and(X2,implies(implies(not(X0),X1),and(X1,X0))),X3) = implies(implies(X2,equiv(not(X0),X1)),X3) ).
cnf(u1491,axiom,
is_a_theorem(or(equiv(X2,implies(X0,not(X1))),implies(or(and(X0,X1),X2),not(implies(X2,implies(X0,not(X1))))))) ).
cnf(u1495,axiom,
is_a_theorem(or(equiv(implies(X0,not(X1)),X2),implies(implies(X2,implies(X0,not(X1))),not(or(and(X0,X1),X2))))) ).
cnf(u1499,axiom,
( ~ is_a_theorem(or(equiv(X2,X3),equiv(not(X0),X1)))
| X2 = X3
| ~ is_a_theorem(implies(implies(not(X0),X1),and(X1,X0))) ) ).
cnf(u1503,axiom,
( ~ is_a_theorem(or(equiv(X3,X4),and(implies(X0,not(X1)),X2)))
| X3 = X4
| ~ is_a_theorem(or(and(X0,X1),not(X2))) ) ).
cnf(u1507,axiom,
is_a_theorem(or(and(or(and(X0,X1),not(X2)),X3),implies(X4,or(and(implies(X0,not(X1)),X2),not(X3))))) ).
cnf(u1511,axiom,
is_a_theorem(or(and(or(and(X0,X1),not(X2)),X3),or(X4,or(and(implies(X0,not(X1)),X2),not(X3))))) ).
cnf(u1515,axiom,
( ~ is_a_theorem(or(and(X0,X1),or(equiv(X2,X3),not(X4))))
| ~ is_a_theorem(X4)
| ~ is_a_theorem(implies(X0,not(X1)))
| X2 = X3 ) ).
cnf(u1519,axiom,
not(implies(X3,and(X4,or(and(X0,X1),not(X2))))) = and(X3,implies(X4,and(implies(X0,not(X1)),X2))) ).
cnf(u1523,axiom,
is_a_theorem(or(and(X3,or(and(X0,X1),not(X2))),implies(or(X4,X3),or(X4,and(implies(X0,not(X1)),X2))))) ).
cnf(u1527,axiom,
is_a_theorem(implies(implies(and(implies(X0,not(X1)),X2),X3),or(and(X4,or(and(X0,X1),not(X2))),implies(X4,X3)))) ).
cnf(u1531,axiom,
is_a_theorem(or(and(X3,or(and(X0,X1),not(X2))),implies(implies(X4,X3),implies(X4,and(implies(X0,not(X1)),X2))))) ).
cnf(u1535,axiom,
equiv(not(implies(X1,X0)),implies(X0,X1)) = not(implies(implies(not(implies(X1,X0)),implies(X0,X1)),equiv(X0,X1))) ).
cnf(u1539,axiom,
not(implies(X2,and(X3,implies(implies(not(X0),X1),and(X1,X0))))) = and(X2,implies(X3,equiv(not(X0),X1))) ).
cnf(u1543,axiom,
is_a_theorem(or(and(X2,implies(implies(not(X0),X1),and(X1,X0))),implies(or(X3,X2),or(X3,equiv(not(X0),X1))))) ).
cnf(u1547,axiom,
is_a_theorem(implies(implies(equiv(not(X0),X1),X2),or(and(X3,implies(implies(not(X0),X1),and(X1,X0))),implies(X3,X2)))) ).
cnf(u1551,axiom,
is_a_theorem(or(and(X2,implies(implies(not(X0),X1),and(X1,X0))),implies(implies(X3,X2),implies(X3,equiv(not(X0),X1))))) ).
cnf(u1555,axiom,
is_a_theorem(or(and(implies(X3,and(implies(X0,not(X1)),X2)),X4),implies(X4,and(X3,or(and(X0,X1),not(X2)))))) ).
cnf(u1559,axiom,
and(implies(X3,not(X4)),or(and(X0,X1),not(X2))) = not(or(and(X3,X4),and(implies(X0,not(X1)),X2))) ).
cnf(u1563,axiom,
is_a_theorem(or(and(implies(X2,equiv(not(X0),X1)),X3),implies(X3,and(X2,implies(implies(not(X0),X1),and(X1,X0)))))) ).
cnf(u1567,axiom,
is_a_theorem(implies(implies(or(and(not(X0),X1),and(not(X1),X0)),equiv(not(X0),not(X1))),equiv(not(X0),not(X1)))) ).
cnf(u1571,axiom,
is_a_theorem(or(and(X2,or(and(not(X0),X1),and(not(X1),X0))),implies(X3,implies(X2,equiv(not(X0),not(X1)))))) ).
cnf(u1575,axiom,
is_a_theorem(or(and(X2,or(and(not(X0),X1),and(not(X1),X0))),or(X3,implies(X2,equiv(not(X0),not(X1)))))) ).
cnf(u1579,axiom,
is_a_theorem(or(equiv(implies(X0,X1),not(implies(X1,X0))),implies(implies(not(implies(X1,X0)),implies(X0,X1)),equiv(X0,X1)))) ).
cnf(u1583,axiom,
is_a_theorem(or(and(implies(implies(not(X0),X1),and(X1,X0)),implies(implies(not(X0),X1),and(X1,X0))),equiv(not(X0),X1))) ).
cnf(u1587,axiom,
and(implies(X2,not(X3)),implies(implies(not(X0),X1),and(X1,X0))) = not(or(and(X2,X3),equiv(not(X0),X1))) ).
cnf(u1591,axiom,
is_a_theorem(or(equiv(implies(not(X0),X1),and(X1,X0)),implies(implies(and(X1,X0),implies(not(X0),X1)),equiv(not(X0),X1)))) ).
cnf(u1595,axiom,
is_a_theorem(or(equiv(implies(X0,not(X1)),X2),implies(X3,implies(or(and(X0,X1),X2),not(implies(X2,implies(X0,not(X1)))))))) ).
cnf(u1599,axiom,
is_a_theorem(or(equiv(X2,implies(X0,not(X1))),implies(X3,implies(implies(X2,implies(X0,not(X1))),not(or(and(X0,X1),X2)))))) ).
cnf(u1603,axiom,
is_a_theorem(or(equiv(implies(X0,not(X1)),X2),or(X3,implies(or(and(X0,X1),X2),not(implies(X2,implies(X0,not(X1)))))))) ).
cnf(u1607,axiom,
is_a_theorem(or(equiv(X2,implies(X0,not(X1))),or(X3,implies(implies(X2,implies(X0,not(X1))),not(or(and(X0,X1),X2)))))) ).
cnf(u1611,axiom,
or(and(X2,or(and(not(X0),X1),and(not(X1),X0))),X3) = implies(implies(X2,equiv(not(X0),not(X1))),X3) ).
cnf(u1615,axiom,
( ~ is_a_theorem(or(equiv(X2,X3),equiv(not(X0),not(X1))))
| X2 = X3
| ~ is_a_theorem(or(and(not(X0),X1),and(not(X1),X0))) ) ).
cnf(u1619,axiom,
is_a_theorem(or(equiv(not(implies(X1,X0)),implies(X0,X1)),or(equiv(X0,X1),not(implies(not(implies(X1,X0)),implies(X0,X1)))))) ).
cnf(u1623,axiom,
not(implies(X2,and(X3,or(and(not(X0),X1),and(not(X1),X0))))) = and(X2,implies(X3,equiv(not(X0),not(X1)))) ).
cnf(u1627,axiom,
is_a_theorem(or(and(X2,or(and(not(X0),X1),and(not(X1),X0))),implies(or(X3,X2),or(X3,equiv(not(X0),not(X1)))))) ).
cnf(u1631,axiom,
is_a_theorem(implies(implies(equiv(not(X0),not(X1)),X2),or(and(X3,or(and(not(X0),X1),and(not(X1),X0))),implies(X3,X2)))) ).
cnf(u1635,axiom,
is_a_theorem(or(and(X2,or(and(not(X0),X1),and(not(X1),X0))),implies(implies(X3,X2),implies(X3,equiv(not(X0),not(X1)))))) ).
cnf(u1639,axiom,
is_a_theorem(or(and(implies(X2,equiv(not(X0),not(X1))),X3),implies(X3,and(X2,or(and(not(X0),X1),and(not(X1),X0)))))) ).
cnf(u1643,axiom,
is_a_theorem(or(equiv(equiv(not(X0),X1),equiv(not(X0),X1)),and(equiv(not(X0),X1),implies(implies(not(X0),X1),and(X1,X0))))) ).
cnf(u1647,axiom,
is_a_theorem(or(equiv(and(X1,X0),implies(not(X0),X1)),implies(X2,implies(implies(and(X1,X0),implies(not(X0),X1)),equiv(not(X0),X1))))) ).
cnf(u1651,axiom,
is_a_theorem(or(equiv(and(X1,X0),implies(not(X0),X1)),or(X2,implies(implies(and(X1,X0),implies(not(X0),X1)),equiv(not(X0),X1))))) ).
cnf(u1655,axiom,
and(implies(X2,not(X3)),or(and(not(X0),X1),and(not(X1),X0))) = not(or(and(X2,X3),equiv(not(X0),not(X1)))) ).
cnf(u1659,axiom,
is_a_theorem(or(and(not(X2),or(and(not(X0),X1),and(not(X1),X0))),or(and(X3,X2),implies(X3,equiv(not(X0),not(X1)))))) ).
cnf(u1663,axiom,
is_a_theorem(or(and(equiv(not(X0),not(X1)),X2),or(and(X3,or(and(not(X0),X1),and(not(X1),X0))),implies(X3,not(X2))))) ).
cnf(u1667,axiom,
( ~ is_a_theorem(implies(X2,or(equiv(X3,X4),equiv(not(X0),X1))))
| ~ is_a_theorem(implies(implies(not(X0),X1),and(X1,X0)))
| ~ is_a_theorem(X2)
| X3 = X4 ) ).
cnf(u1671,axiom,
( ~ is_a_theorem(implies(X3,or(equiv(X4,X5),and(implies(X0,not(X1)),X2))))
| ~ is_a_theorem(or(and(X0,X1),not(X2)))
| ~ is_a_theorem(X3)
| X4 = X5 ) ).
cnf(u1675,axiom,
is_a_theorem(or(and(or(and(not(X0),X1),and(not(X1),X0)),or(and(not(X0),X1),and(not(X1),X0))),equiv(not(X0),not(X1)))) ).
cnf(u1679,axiom,
is_a_theorem(or(and(implies(X2,equiv(not(X0),not(X1))),X3),implies(X4,or(and(X2,or(and(not(X0),X1),and(not(X1),X0))),not(X3))))) ).
cnf(u1683,axiom,
is_a_theorem(or(and(implies(X2,not(X3)),or(and(not(X0),X1),and(not(X1),X0))),implies(X4,or(and(X2,X3),equiv(not(X0),not(X1)))))) ).
cnf(u1687,axiom,
is_a_theorem(or(and(implies(X2,equiv(not(X0),not(X1))),X3),or(X4,or(and(X2,or(and(not(X0),X1),and(not(X1),X0))),not(X3))))) ).
cnf(u1691,axiom,
is_a_theorem(or(and(implies(X2,not(X3)),or(and(not(X0),X1),and(not(X1),X0))),or(X4,or(and(X2,X3),equiv(not(X0),not(X1)))))) ).
cnf(u1695,axiom,
is_a_theorem(or(equiv(X3,and(implies(X0,not(X1)),X2)),implies(implies(and(implies(X0,not(X1)),X2),X3),and(X3,or(and(X0,X1),not(X2)))))) ).
cnf(u1699,axiom,
( ~ is_a_theorem(implies(X2,or(equiv(X3,X4),equiv(not(X0),not(X1)))))
| ~ is_a_theorem(or(and(not(X0),X1),and(not(X1),X0)))
| ~ is_a_theorem(X2)
| X3 = X4 ) ).
cnf(u1703,axiom,
equiv(equiv(not(X0),not(X1)),X2) = not(implies(implies(equiv(not(X0),not(X1)),X2),and(X2,or(and(not(X0),X1),and(not(X1),X0))))) ).
cnf(u1707,axiom,
is_a_theorem(or(equiv(and(implies(X0,not(X1)),X2),and(implies(X0,not(X1)),X2)),and(and(implies(X0,not(X1)),X2),or(and(X0,X1),not(X2))))) ).
cnf(u1711,axiom,
is_a_theorem(or(equiv(equiv(not(X0),not(X1)),equiv(not(X0),not(X1))),and(equiv(not(X0),not(X1)),or(and(not(X0),X1),and(not(X1),X0))))) ).
cnf(u1715,axiom,
is_a_theorem(or(equiv(X2,equiv(not(X0),not(X1))),implies(implies(equiv(not(X0),not(X1)),X2),and(X2,or(and(not(X0),X1),and(not(X1),X0)))))) ).
cnf(u1719,axiom,
equiv(and(implies(X0,not(X1)),X2),not(X3)) = not(or(and(and(implies(X0,not(X1)),X2),X3),and(not(X3),or(and(X0,X1),not(X2))))) ).
cnf(u1723,axiom,
is_a_theorem(or(equiv(equiv(not(X0),not(X1)),X2),or(and(X2,or(and(not(X0),X1),and(not(X1),X0))),not(implies(equiv(not(X0),not(X1)),X2))))) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL909+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.38 % Computer : n015.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Sun Sep 27 17:09:16 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.27/1.37 % (1864780)Detected formulas, will run a generic FOF schedule.
% 3.27/1.37 % (1864828)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=1016782803:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.27/1.37 % (1864834)dis-21_1_sil=8000:lcm=predicate:random_seed=592288732: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)
% 3.27/1.37 % (1864826)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=393028073:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.27/1.37 % (1864830)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=139723628:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.27/1.37 % (1864829)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=869622046:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.27/1.37 % (1864830)Refutation not found, incomplete strategy
% 3.27/1.37 % (1864830)------------------------------
% 3.27/1.37 % (1864830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.27/1.37 % (1864834)Refutation not found, incomplete strategy
% 3.27/1.37 % (1864834)------------------------------
% 3.27/1.37 % (1864834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.27/1.37 % (1864830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.27/1.37 % (1864834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.27/1.37 % (1864830)CaDiCaL version: 2.1.3
% 3.27/1.37 % (1864830)Termination reason: Refutation not found, incomplete strategy
% 3.27/1.37 % (1864830)Time elapsed: 0.001 s
% 3.27/1.37 % (1864830)Peak memory usage: 86 MB
% 3.27/1.37 % (1864834)CaDiCaL version: 2.1.3
% 3.27/1.37 % (1864834)Termination reason: Refutation not found, incomplete strategy
% 3.27/1.37 % (1864834)Time elapsed: 0.001 s
% 3.27/1.37 % (1864834)Peak memory usage: 86 MB
% 3.27/1.37 % (1864831)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2891700727:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.27/1.37 % (1864833)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=924804723:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.27/1.37 % (1864831)Refutation not found, incomplete strategy
% 3.27/1.37 % (1864831)------------------------------
% 3.27/1.37 % (1864831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.27/1.37 % (1864831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.27/1.37 % (1864831)CaDiCaL version: 2.1.3
% 3.27/1.37 % (1864831)Termination reason: Refutation not found, incomplete strategy
% 3.27/1.37 % (1864831)Time elapsed: 0.0000 s
% 3.27/1.37 % (1864831)Peak memory usage: 86 MB
% 3.27/1.37 % (1864833)Instruction limit reached!
% 3.27/1.37 % (1864833)------------------------------
% 3.27/1.37 % (1864833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.27/1.37 % (1864833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.27/1.37 % (1864833)CaDiCaL version: 2.1.3
% 3.27/1.37 % (1864833)Termination reason: Instruction limit
% 3.27/1.37 % (1864833)Termination phase: Saturation
% 3.27/1.37 % (1864833)Time elapsed: 0.095 s
% 3.27/1.37 % (1864833)Peak memory usage: 90 MB
% 3.27/1.37 % (1864833)Instructions burned: 140 (million)
% 3.27/1.37 [W927 17:09:17.352529535 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.
% 3.27/1.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.27/1.37 [W927 17:09:17.352549934 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.
% 3.27/1.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.27/1.37 [W927 17:09:17.352571956 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.70/1.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.68 [W927 17:09:17.352587266 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.70/1.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.68 [W927 17:09:17.352612664 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.70/1.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.68 [W927 17:09:17.352618537 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.70/1.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.68 [W927 17:09:17.352631616 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.70/1.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.68 [W927 17:09:17.352644883 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.70/1.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.68 [W927 17:09:17.352658475 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.70/1.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.68 [W927 17:09:17.352664259 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.70/1.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.68 [W927 17:09:17.352677348 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.70/1.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.68 [W927 17:09:17.352683019 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.70/1.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.70/1.68 % (1864893)lrs+10_1_sil=8000:sp=occurrence:random_seed=561358184:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 4.70/1.68 % (1864893)Refutation not found, incomplete strategy
% 4.70/1.68 % (1864893)------------------------------
% 4.70/1.68 % (1864893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.68 % (1864893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.68 % (1864893)CaDiCaL version: 2.1.3
% 4.70/1.68 % (1864893)Termination reason: Refutation not found, incomplete strategy
% 4.70/1.68 % (1864893)Time elapsed: 0.001 s
% 4.70/1.68 % (1864893)Peak memory usage: 86 MB
% 4.70/1.68 % (1864830)------------------------------
% 4.70/1.68 % (1864830)------------------------------
% 4.70/1.68 % (1864834)------------------------------
% 4.70/1.68 % (1864834)------------------------------
% 4.70/1.68 % (1864831)------------------------------
% 4.70/1.68 % (1864831)------------------------------
% 4.70/1.68 % (1864828)Refutation not found, incomplete strategy
% 4.70/1.68 % (1864828)------------------------------
% 4.70/1.68 % (1864828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.68 % (1864828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.74/2.12 % (1864828)CaDiCaL version: 2.1.3
% 8.74/2.12 % (1864828)Termination reason: Refutation not found, incomplete strategy
% 8.74/2.12 % (1864828)Time elapsed: 0.319 s
% 8.74/2.12 % (1864828)Peak memory usage: 125 MB
% 8.74/2.12 % (1864828)Instructions burned: 822 (million)
% 8.74/2.12 % (1864919)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2496019321:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 8.74/2.12 % (1864917)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2338811570:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 8.74/2.12 % (1864919)Refutation not found, incomplete strategy
% 8.74/2.12 % (1864919)------------------------------
% 8.74/2.12 % (1864919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.74/2.12 % (1864919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.74/2.12 % (1864919)CaDiCaL version: 2.1.3
% 8.74/2.12 % (1864919)Termination reason: Refutation not found, incomplete strategy
% 8.74/2.12 % (1864919)Time elapsed: 0.001 s
% 8.74/2.12 % (1864919)Peak memory usage: 86 MB
% 8.74/2.12 % (1864917)Refutation not found, incomplete strategy
% 8.74/2.12 % (1864917)------------------------------
% 8.74/2.12 % (1864917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.74/2.12 % (1864917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.74/2.12 % (1864917)CaDiCaL version: 2.1.3
% 8.74/2.12 % (1864917)Termination reason: Refutation not found, incomplete strategy
% 8.74/2.12 % (1864917)Time elapsed: 0.001 s
% 8.74/2.12 % (1864917)Peak memory usage: 87 MB
% 8.74/2.12 [W927 17:09:17.556526049 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.
% 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.74/2.12 [W927 17:09:17.556566466 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.
% 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.74/2.12 [W927 17:09:17.556603300 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.
% 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.74/2.12 [W927 17:09:17.556616710 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.
% 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.74/2.12 [W927 17:09:17.556641783 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.
% 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.74/2.12 [W927 17:09:17.556706164 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.
% 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.74/2.12 [W927 17:09:17.556739034 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.
% 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.74/2.12 [W927 17:09:17.556751607 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.
% 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.74/2.12 [W927 17:09:17.556776284 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.
% 10.93/2.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.93/2.43 [W927 17:09:17.556786728 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.
% 10.93/2.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.93/2.43 [W927 17:09:17.556818311 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.
% 10.93/2.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.93/2.43 [W927 17:09:17.556838331 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.
% 10.93/2.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.93/2.43 % (1864921)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=3200793630:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 10.93/2.43 % (1864828)------------------------------
% 10.93/2.43 % (1864828)------------------------------
% 10.93/2.43 % (1864893)------------------------------
% 10.93/2.43 % (1864893)------------------------------
% 10.93/2.43 % (1864921)Instruction limit reached!
% 10.93/2.43 % (1864921)------------------------------
% 10.93/2.43 % (1864921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.43 % (1864921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.43 % (1864921)CaDiCaL version: 2.1.3
% 10.93/2.43 % (1864921)Termination reason: Instruction limit
% 10.93/2.43 % (1864921)Termination phase: Saturation
% 10.93/2.43 % (1864921)Time elapsed: 0.156 s
% 10.93/2.43 % (1864921)Peak memory usage: 92 MB
% 10.93/2.43 % (1864921)Instructions burned: 249 (million)
% 10.93/2.43 % (1864829)Refutation not found, incomplete strategy
% 10.93/2.43 % (1864829)------------------------------
% 10.93/2.43 % (1864829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.43 % (1864829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.43 % (1864829)CaDiCaL version: 2.1.3
% 10.93/2.43 % (1864829)Termination reason: Refutation not found, incomplete strategy
% 10.93/2.43 % (1864829)Time elapsed: 0.560 s
% 10.93/2.43 % (1864829)Peak memory usage: 125 MB
% 10.93/2.43 % (1864829)Instructions burned: 822 (million)
% 10.93/2.43 % (1864934)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2019663957:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 10.93/2.43 % (1864934)Refutation not found, incomplete strategy
% 10.93/2.43 % (1864934)------------------------------
% 10.93/2.43 % (1864934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.43 % (1864934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.43 % (1864934)CaDiCaL version: 2.1.3
% 10.93/2.43 % (1864934)Termination reason: Refutation not found, incomplete strategy
% 10.93/2.43 % (1864934)Time elapsed: 0.001 s
% 10.93/2.43 % (1864934)Peak memory usage: 86 MB
% 10.93/2.43 % (1864935)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2972006129:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 10.93/2.43 % (1864917)------------------------------
% 10.93/2.43 % (1864917)------------------------------
% 10.93/2.43 % (1864919)------------------------------
% 10.93/2.43 % (1864919)------------------------------
% 10.93/2.43 % (1864941)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=53801407:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 10.93/2.43 % (1864941)Refutation not found, incomplete strategy
% 10.93/2.43 % (1864941)------------------------------
% 10.93/2.43 % (1864941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.43 % (1864941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.43 % (1864941)CaDiCaL version: 2.1.3
% 10.93/2.43 % (1864941)Termination reason: Refutation not found, incomplete strategy
% 10.93/2.43 % (1864941)Time elapsed: 0.001 s
% 10.93/2.43 % (1864941)Peak memory usage: 87 MB
% 12.48/2.70 % (1864959)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=816896690:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 12.48/2.70 % (1864960)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2283956324:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 12.48/2.70 % (1864960)Refutation not found, incomplete strategy
% 12.48/2.70 % (1864960)------------------------------
% 12.48/2.70 % (1864960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.48/2.70 % (1864960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.70 % (1864960)CaDiCaL version: 2.1.3
% 12.48/2.70 % (1864960)Termination reason: Refutation not found, incomplete strategy
% 12.48/2.70 % (1864960)Time elapsed: 0.001 s
% 12.48/2.70 % (1864960)Peak memory usage: 87 MB
% 12.48/2.70 % (1864959)Refutation not found, incomplete strategy
% 12.48/2.70 % (1864959)------------------------------
% 12.48/2.70 % (1864959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.48/2.70 % (1864959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.70 % (1864959)CaDiCaL version: 2.1.3
% 12.48/2.70 % (1864959)Termination reason: Refutation not found, incomplete strategy
% 12.48/2.70 % (1864959)Time elapsed: 0.001 s
% 12.48/2.70 % (1864959)Peak memory usage: 87 MB
% 12.48/2.70 % (1864829)------------------------------
% 12.48/2.70 % (1864829)------------------------------
% 12.48/2.70 % (1864934)------------------------------
% 12.48/2.70 % (1864934)------------------------------
% 12.48/2.70 % (1864941)------------------------------
% 12.48/2.70 % (1864941)------------------------------
% 12.48/2.70 % (1864991)lrs+10_1_sil=8000:sp=occurrence:random_seed=2567640735:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 12.48/2.70 % (1864991)Refutation not found, incomplete strategy
% 12.48/2.70 % (1864991)------------------------------
% 12.48/2.70 % (1864991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.48/2.70 % (1864991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.70 % (1864991)CaDiCaL version: 2.1.3
% 12.48/2.70 % (1864991)Termination reason: Refutation not found, incomplete strategy
% 12.48/2.70 % (1864991)Time elapsed: 0.001 s
% 12.48/2.70 % (1864991)Peak memory usage: 86 MB
% 12.48/2.70 % (1864992)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3776033573:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 12.48/2.70 % (1864992)Refutation not found, incomplete strategy
% 12.48/2.70 % (1864992)------------------------------
% 12.48/2.70 % (1864992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.48/2.70 % (1864992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.70 % (1864992)CaDiCaL version: 2.1.3
% 12.48/2.70 % (1864992)Termination reason: Refutation not found, incomplete strategy
% 12.48/2.70 % (1864992)Time elapsed: 0.001 s
% 12.48/2.70 % (1864992)Peak memory usage: 86 MB
% 12.48/2.70 % (1864959)------------------------------
% 12.48/2.70 % (1864959)------------------------------
% 12.48/2.70 % (1864960)------------------------------
% 12.48/2.70 % (1864960)------------------------------
% 12.48/2.70 % (1864993)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1739054363:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 12.48/2.70 % (1864996)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1056535837:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 12.48/2.70 % (1864996)Refutation not found, incomplete strategy
% 12.48/2.70 % (1864996)------------------------------
% 12.48/2.70 % (1864996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.48/2.70 % (1864996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.70 % (1864996)CaDiCaL version: 2.1.3
% 12.48/2.70 % (1864996)Termination reason: Refutation not found, incomplete strategy
% 12.48/2.70 % (1864996)Time elapsed: 0.001 s
% 12.48/2.70 % (1864996)Peak memory usage: 87 MB
% 12.48/2.70 % (1864997)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1167247639:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi)
% 12.48/2.70 % (1864997)Refutation not found, incomplete strategy
% 12.48/2.70 % (1864997)------------------------------
% 12.48/2.70 % (1864997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.16/2.87 % (1864997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.16/2.87 % (1864997)CaDiCaL version: 2.1.3
% 13.16/2.87 % (1864997)Termination reason: Refutation not found, incomplete strategy
% 13.16/2.87 % (1864997)Time elapsed: 0.001 s
% 13.16/2.87 % (1864997)Peak memory usage: 86 MB
% 13.16/2.87 % (1864991)------------------------------
% 13.16/2.87 % (1864991)------------------------------
% 13.16/2.87 % (1864992)------------------------------
% 13.16/2.87 % (1864992)------------------------------
% 13.16/2.87 % (1865001)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2354595168:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi)
% 13.16/2.87 % (1865002)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=2873507483:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/125Mi)
% 13.16/2.87 % (1864996)------------------------------
% 13.16/2.87 % (1864996)------------------------------
% 13.16/2.87 % (1865002)Refutation not found, incomplete strategy
% 13.16/2.87 % (1865002)------------------------------
% 13.16/2.87 % (1865002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.16/2.87 % (1865002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.16/2.87 % (1865002)CaDiCaL version: 2.1.3
% 13.16/2.87 % (1865002)Termination reason: Refutation not found, incomplete strategy
% 13.16/2.87 % (1865002)Time elapsed: 0.001 s
% 13.16/2.87 % (1865002)Peak memory usage: 87 MB
% 13.16/2.87 % (1864997)------------------------------
% 13.16/2.87 % (1864997)------------------------------
% 13.16/2.87 [W927 17:09:18.621763286 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.
% 13.16/2.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 13.16/2.87 [W927 17:09:18.621855986 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.
% 13.16/2.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 13.16/2.87 [W927 17:09:18.621900877 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.
% 13.16/2.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 13.16/2.87 [W927 17:09:18.621913877 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.
% 13.16/2.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 13.16/2.87 [W927 17:09:18.621940144 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.
% 13.16/2.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 13.16/2.87 [W927 17:09:18.621951620 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.
% 13.16/2.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 13.16/2.88 [W927 17:09:18.621978411 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.
% 13.16/2.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 13.16/2.88 [W927 17:09:18.621990084 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.
% 13.16/2.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 13.16/2.88 [W927 17:09:18.622027481 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.
% 16.91/3.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 16.91/3.26 [W927 17:09:18.622040331 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.
% 16.91/3.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 16.91/3.26 [W927 17:09:18.622072248 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.
% 16.91/3.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 16.91/3.26 [W927 17:09:18.622090835 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.
% 16.91/3.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 16.91/3.26 % (1865005)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3746632296:i=134:gtgl=5:slsql=off:gtg=exists_sym_2984 on theBenchmark for (2984ds/134Mi)
% 16.91/3.26 % (1865006)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2488411451:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/141Mi)
% 16.91/3.26 % (1865006)Refutation not found, incomplete strategy
% 16.91/3.26 % (1865006)------------------------------
% 16.91/3.26 % (1865006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.91/3.26 % (1865006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.91/3.26 % (1865006)CaDiCaL version: 2.1.3
% 16.91/3.26 % (1865006)Termination reason: Refutation not found, incomplete strategy
% 16.91/3.26 % (1865006)Time elapsed: 0.0000 s
% 16.91/3.26 % (1865006)Peak memory usage: 86 MB
% 16.91/3.26 % (1865005)Instruction limit reached!
% 16.91/3.26 % (1865005)------------------------------
% 16.91/3.26 % (1865005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.91/3.26 % (1865005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.91/3.26 % (1865005)CaDiCaL version: 2.1.3
% 16.91/3.26 % (1865005)Termination reason: Instruction limit
% 16.91/3.26 % (1865005)Termination phase: Saturation
% 16.91/3.26 % (1865005)Time elapsed: 0.087 s
% 16.91/3.26 % (1865005)Peak memory usage: 90 MB
% 16.91/3.26 % (1865005)Instructions burned: 135 (million)
% 16.91/3.26 % (1865002)------------------------------
% 16.91/3.26 % (1865002)------------------------------
% 16.91/3.26 % (1864993)Refutation not found, incomplete strategy
% 16.91/3.26 % (1864993)------------------------------
% 16.91/3.26 % (1864993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.91/3.26 % (1864993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.91/3.26 % (1864993)CaDiCaL version: 2.1.3
% 16.91/3.26 % (1864993)Termination reason: Refutation not found, incomplete strategy
% 16.91/3.26 % (1864993)Time elapsed: 0.551 s
% 16.91/3.26 % (1864993)Peak memory usage: 125 MB
% 16.91/3.26 % (1864993)Instructions burned: 826 (million)
% 16.91/3.26 [W927 17:09:18.889397539 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.
% 16.91/3.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 16.91/3.26 [W927 17:09:18.889436466 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.
% 16.91/3.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 16.91/3.26 [W927 17:09:18.889473229 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.
% 16.91/3.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 16.91/3.26 [W927 17:09:18.889485663 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.
% 19.41/3.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.41/3.77 [W927 17:09:18.889510453 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.
% 19.41/3.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.41/3.77 [W927 17:09:18.889521416 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.
% 19.41/3.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.41/3.77 [W927 17:09:18.889546130 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.
% 19.41/3.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.41/3.77 [W927 17:09:18.889556876 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.
% 19.41/3.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.41/3.77 [W927 17:09:18.889581887 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.
% 19.41/3.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.41/3.77 [W927 17:09:18.889592577 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.
% 19.41/3.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.41/3.77 [W927 17:09:18.889616410 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.
% 19.41/3.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.41/3.77 [W927 17:09:18.889627204 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.
% 19.41/3.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.41/3.77 % (1865009)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1367144120:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2982 on theBenchmark for (2982ds/431Mi)
% 19.41/3.77 % (1865009)Refutation not found, incomplete strategy
% 19.41/3.77 % (1865009)------------------------------
% 19.41/3.77 % (1865009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.77 % (1865009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.77 % (1865009)CaDiCaL version: 2.1.3
% 19.41/3.77 % (1865009)Termination reason: Refutation not found, incomplete strategy
% 19.41/3.77 % (1865009)Time elapsed: 0.001 s
% 19.41/3.77 % (1865009)Peak memory usage: 86 MB
% 19.41/3.77 % (1865010)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=2782639887:i=6060:aac=none:ins=25_2982 on theBenchmark for (2982ds/6060Mi)
% 19.41/3.77 % (1865006)------------------------------
% 19.41/3.77 % (1865006)------------------------------
% 19.41/3.77 % (1864993)------------------------------
% 19.41/3.77 % (1864993)------------------------------
% 19.41/3.77 % (1865001)Refutation not found, incomplete strategy
% 19.41/3.77 % (1865001)------------------------------
% 19.41/3.77 % (1865001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.77 % (1865001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.77 % (1865001)CaDiCaL version: 2.1.3
% 19.41/3.77 % (1865001)Termination reason: Refutation not found, incomplete strategy
% 19.41/3.77 % (1865001)Time elapsed: 0.555 s
% 19.41/3.77 % (1865001)Peak memory usage: 125 MB
% 19.41/3.77 % (1865001)Instructions burned: 826 (million)
% 19.41/3.77 % (1865013)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=811039687:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2981 on theBenchmark for (2981ds/150Mi)
% 19.41/3.77 % (1865009)------------------------------
% 19.41/3.77 % (1865009)------------------------------
% 19.41/3.77 % (1865013)Instruction limit reached!
% 19.41/3.77 % (1865013)------------------------------
% 19.41/3.77 % (1865013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.77 % (1865013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.77 % (1865013)CaDiCaL version: 2.1.3
% 19.41/3.77 % (1865013)Termination reason: Instruction limit
% 19.41/3.77 % (1865013)Termination phase: Saturation
% 19.41/3.77 % (1865013)Time elapsed: 0.098 s
% 19.41/3.77 % (1865013)Peak memory usage: 91 MB
% 19.41/3.77 % (1865013)Instructions burned: 151 (million)
% 19.41/3.77 % (1865014)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2452336567:i=14155:bd=all_2979 on theBenchmark for (2979ds/14155Mi)
% 19.41/3.77 % (1865016)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1640217433:i=667:av=off:fsr=off_2978 on theBenchmark for (2978ds/667Mi)
% 19.41/3.77 % (1865016)Refutation not found, incomplete strategy
% 19.41/3.77 % (1865016)------------------------------
% 19.41/3.77 % (1865016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.77 % (1865016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.77 % (1865016)CaDiCaL version: 2.1.3
% 19.41/3.77 % (1865016)Termination reason: Refutation not found, incomplete strategy
% 19.41/3.77 % (1865016)Time elapsed: 0.001 s
% 19.41/3.77 % (1865016)Peak memory usage: 87 MB
% 19.41/3.77 % (1865001)------------------------------
% 19.41/3.77 % (1865001)------------------------------
% 19.41/3.77 % (1864935)Instruction limit reached!
% 19.41/3.77 % (1864935)------------------------------
% 19.41/3.77 % (1864935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.77 % (1864935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.77 % (1864935)CaDiCaL version: 2.1.3
% 19.41/3.77 % (1864935)Termination reason: Instruction limit
% 19.41/3.77 % (1864935)Termination phase: Saturation
% 19.41/3.77 % (1864935)Time elapsed: 1.531 s
% 19.41/3.77 % (1864935)Peak memory usage: 141 MB
% 19.41/3.77 % (1864935)Instructions burned: 2351 (million)
% 19.41/3.77 % (1865017)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=3810392972:s2a=on:i=185:s2at=1.8:fdi=4_2978 on theBenchmark for (2978ds/185Mi)
% 19.41/3.77 % (1865017)Instruction limit reached!
% 19.41/3.77 % (1865017)------------------------------
% 19.41/3.77 % (1865017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.77 % (1865017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.77 % (1865017)CaDiCaL version: 2.1.3
% 19.41/3.77 % (1865017)Termination reason: Instruction limit
% 19.41/3.77 % (1865017)Termination phase: Saturation
% 19.41/3.77 % (1865017)Time elapsed: 0.114 s
% 19.41/3.77 % (1865017)Peak memory usage: 91 MB
% 19.41/3.77 % (1865017)Instructions burned: 185 (million)
% 19.41/3.77 % (1865022)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1382500192:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2977 on theBenchmark for (2977ds/4850Mi)
% 19.41/3.77 % (1865021)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2280538625:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2977 on theBenchmark for (2977ds/193Mi)
% 19.41/3.77 % (1865022)Refutation not found, incomplete strategy
% 19.41/3.77 % (1865022)------------------------------
% 19.41/3.77 % (1865022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.77 % (1865022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.77 % (1865022)CaDiCaL version: 2.1.3
% 19.41/3.77 % (1865022)Termination reason: Refutation not found, incomplete strategy
% 19.41/3.77 % (1865022)Time elapsed: 0.0000 s
% 19.41/3.77 % (1865022)Peak memory usage: 86 MB
% 19.41/3.77 % (1865021)Refutation not found, incomplete strategy
% 19.41/3.77 % (1865021)------------------------------
% 19.41/3.77 % (1865021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.77 % (1865021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.77 % (1865021)CaDiCaL version: 2.1.3
% 19.41/3.77 % (1865021)Termination reason: Refutation not found, incomplete strategy
% 19.41/3.77 % (1865021)Time elapsed: 0.001 s
% 19.41/3.77 % (1865021)Peak memory usage: 86 MB
% 19.41/3.77 % (1865016)------------------------------
% 19.41/3.77 % (1865016)------------------------------
% 19.41/3.77 % (1865023)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3939950118:i=12111:sd=1:ss=included_2976 on theBenchmark for (2976ds/12111Mi)
% 19.41/3.77 % (1865026)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2530517184:i=319:kws=precedence:fsr=off_2975 on theBenchmark for (2975ds/319Mi)
% 19.41/3.77 % (1865026)First to succeed.
% 19.41/3.77 % (1865021)------------------------------
% 19.41/3.77 % (1865021)------------------------------
% 19.41/3.77 % (1865022)------------------------------
% 19.41/3.77 % (1865022)------------------------------
% 19.41/3.77 % (1865026)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1864780"
% 19.41/3.77 % (1865030)dis-1011_128_sil=32000:random_seed=1732146133:i=3706:ep=RST:av=off_2973 on theBenchmark for (2973ds/3706Mi)
% 19.41/3.77 % (1865029)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1089983973:i=2064:ep=RST_2973 on theBenchmark for (2973ds/2064Mi)
% 19.41/3.77 % (1865029)Refutation not found, incomplete strategy
% 19.41/3.77 % (1865029)------------------------------
% 19.41/3.77 % (1865029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.77 % (1865029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.77 % (1865029)CaDiCaL version: 2.1.3
% 19.41/3.77 % (1865029)Termination reason: Refutation not found, incomplete strategy
% 19.41/3.77 % (1865029)Time elapsed: 0.001 s
% 19.41/3.77 % (1865029)Peak memory usage: 88 MB
% 19.41/3.77 % (1865029)Instructions burned: 1 (million)
% 19.41/3.77 % (1865030)Refutation not found, incomplete strategy
% 19.41/3.77 % (1865030)------------------------------
% 19.41/3.77 % (1865030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.77 % (1865030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.77 % (1865030)CaDiCaL version: 2.1.3
% 19.41/3.77 % (1865030)Termination reason: Refutation not found, incomplete strategy
% 19.41/3.77 % (1865030)Time elapsed: 0.001 s
% 19.41/3.77 % (1865030)Peak memory usage: 88 MB
% 19.41/3.77 % (1865030)Instructions burned: 1 (million)
% 19.41/3.77 % SZS status Satisfiable for theBenchmark
% 19.41/3.77 % SZS output start Saturation.
% See solution above
% 21.16/3.96 % SZS output start Definitions and Model Updates.
% 21.16/3.96 for all inputs,
% 21.16/3.96 define op_or := $false
% 21.16/3.96 for all inputs,
% 21.16/3.96 define op_implies_and := $false
% 21.16/3.96 for all groundings,
% 21.16/3.96 whenever ! [X0,X1] : ((is_a_theorem(X0) & is_a_theorem(implies(X0,X1))) => is_a_theorem(X1)) is true, set modus_ponens to true
% 21.16/3.96 for all groundings,
% 21.16/3.96 whenever ! [X0,X1] : (is_a_theorem(equiv(X0,X1)) => X0 = X1) is true, set substitution_of_equivalents to true
% 21.16/3.96 for all inputs,
% 21.16/3.96 define modus_tollens := ! [X0,X1] : is_a_theorem(implies(implies(not(X1),not(X0)),implies(X0,X1)))
% 21.16/3.96 for all inputs,
% 21.16/3.96 define implies_1 := ! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X0)))
% 21.16/3.96 for all inputs,
% 21.16/3.96 define implies_2 := ! [X0,X1] : is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1)))
% 21.16/3.96 for all inputs,
% 21.16/3.96 define implies_3 := ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))))
% 21.16/3.96 for all inputs,
% 21.16/3.96 define and_1 := ! [X0,X1] : is_a_theorem(implies(and(X0,X1),X0))
% 21.16/3.96 for all inputs,
% 21.16/3.96 define and_2 := ! [X0,X1] : is_a_theorem(implies(and(X0,X1),X1))
% 21.16/3.96 for all inputs,
% 21.16/3.96 define and_3 := ! [X0,X1] : is_a_theorem(implies(X0,implies(X1,and(X0,X1))))
% 21.16/3.96 for all inputs,
% 21.16/3.96 define or_1 := ! [X0,X1] : is_a_theorem(implies(X0,or(X0,X1)))
% 21.16/3.96 for all inputs,
% 21.16/3.96 define or_2 := ! [X0,X1] : is_a_theorem(implies(X1,or(X0,X1)))
% 21.16/3.96 for all inputs,
% 21.16/3.96 define or_3 := ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X2),implies(implies(X1,X2),implies(or(X0,X1),X2))))
% 21.16/3.96 for all inputs,
% 21.16/3.96 define equivalence_1 := ! [X0,X1] : is_a_theorem(implies(equiv(X0,X1),implies(X0,X1)))
% 21.16/3.96 for all inputs,
% 21.16/3.96 define equivalence_2 := ! [X0,X1] : is_a_theorem(implies(equiv(X0,X1),implies(X1,X0)))
% 21.16/3.96 for all inputs,
% 21.16/3.96 define equivalence_3 := ! [X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X0),equiv(X0,X1))))
% 21.16/3.96 for all inputs,
% 21.16/3.96 define kn1 := ! [X0] : is_a_theorem(implies(X0,and(X0,X0)))
% 21.16/3.96 for all inputs,
% 21.16/3.96 define kn2 := ! [X0,X1] : is_a_theorem(implies(and(X0,X1),X0))
% 21.16/3.96 for all inputs,
% 21.16/3.96 define kn3 := ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0)))))
% 21.16/3.96 for all inputs,
% 21.16/3.96 define cn1 := ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))))
% 21.16/3.96 for all inputs,
% 21.16/3.96 define cn2 := ! [X0,X1] : is_a_theorem(implies(X0,implies(not(X0),X1)))
% 21.16/3.96 for all inputs,
% 21.16/3.96 define cn3 := ! [X0] : is_a_theorem(implies(implies(not(X0),X0),X0))
% 21.16/3.96 for all groundings,
% 21.16/3.96 whenever ! [X0] : is_a_theorem(implies(or(X0,X0),X0)) is true, set r1 to true
% 21.16/3.96 for all groundings,
% 21.16/3.96 whenever ! [X0,X1] : is_a_theorem(implies(X1,or(X0,X1))) is true, set r2 to true
% 21.16/3.96 for all groundings,
% 21.16/3.96 whenever ! [X0,X1] : is_a_theorem(implies(or(X0,X1),or(X1,X0))) is true, set r3 to true
% 21.16/3.96 for all groundings,
% 21.16/3.96 whenever ! [X0,X1,X2] : is_a_theorem(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))) is true, set r4 to true
% 21.16/3.96 for all groundings,
% 21.16/3.96 whenever ! [X0,X1,X2] : is_a_theorem(implies(implies(X1,X2),implies(or(X0,X1),or(X0,X2)))) is true, set r5 to true
% 21.16/3.96 % SZS output end Definitions and Model Updates.
% 21.16/3.96 % (1865026)------------------------------
% 21.16/3.96 % (1865026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.16/3.96 % (1865026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.16/3.96 % (1865026)CaDiCaL version: 2.1.3
% 21.16/3.96 % (1865026)Termination reason: Satisfiable
% 21.16/3.96 % (1865026)Time elapsed: 0.028 s
% 21.16/3.96 % (1865026)Peak memory usage: 89 MB
% 21.16/3.96 % (1865026)Instructions burned: 41 (million)
% 21.16/3.96 % (1865026)------------------------------
% 21.16/3.96 % (1865026)------------------------------
% 21.16/3.96 % (1864780)Success in time 2.917 s
% 21.16/3.96 % Vampire exiting
%------------------------------------------------------------------------------