%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN423-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/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 01:50:35 PM UTC 2026
% Result : Satisfiable 29.79s 4.78s
% Output : Saturation 31.41s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u635,negated_conjecture,
ndr1_0 ).
cnf(u639,negated_conjecture,
( ~ c4_1(X2)
| c8_2(X2,X3)
| ~ c6_2(X2,X4)
| ~ c8_2(X2,X4)
| ~ c5_2(X2,X4)
| ~ ndr1_1(X2)
| ~ c4_2(X2,X3)
| ~ c10_2(X2,X3) ) ).
cnf(u665,negated_conjecture,
( ~ c6_2(X0,X3)
| c10_2(X0,X3)
| c9_2(X0,X2)
| ~ c5_2(X0,X1)
| ~ c3_2(X0,X3)
| ~ c8_2(X0,X2)
| ~ c4_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1)
| ~ c8_2(X0,X1) ) ).
cnf(u668,negated_conjecture,
ssSkC33 ).
cnf(u673,negated_conjecture,
c4_0 ).
cnf(u677,negated_conjecture,
( ~ c3_1(X3)
| c5_2(X3,X4)
| c1_2(X3,X4)
| ~ ndr1_1(X3)
| ~ c10_1(X3) ) ).
cnf(u685,negated_conjecture,
~ c5_0 ).
cnf(u695,negated_conjecture,
( ~ c5_1(X0)
| c10_2(X0,X2)
| c5_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ c6_2(X0,X2)
| ~ c5_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u704,negated_conjecture,
( ~ c8_2(X1,a577)
| c9_2(X1,X3)
| ~ c4_2(X1,X2)
| ~ c3_2(X1,X3)
| ~ c1_2(X1,X3)
| ~ ndr1_1(X1)
| ~ c9_2(X1,X2)
| ~ c8_2(X1,X2) ) ).
cnf(u710,negated_conjecture,
ssSkC26 ).
cnf(u715,negated_conjecture,
( ~ c4_2(X1,X2)
| c9_2(X1,a577)
| c9_2(X1,X3)
| ~ c3_2(X1,X3)
| ~ c1_2(X1,X3)
| ~ ndr1_1(X1)
| ~ c9_2(X1,X2)
| ~ c8_2(X1,X2) ) ).
cnf(u719,negated_conjecture,
( ~ c4_2(X1,X2)
| c3_2(X1,a577)
| c9_2(X1,X3)
| ~ c3_2(X1,X3)
| ~ c1_2(X1,X3)
| ~ ndr1_1(X1)
| ~ c9_2(X1,X2)
| ~ c8_2(X1,X2) ) ).
cnf(u724,negated_conjecture,
~ ndr1_1(a562) ).
cnf(u734,negated_conjecture,
c10_0 ).
cnf(u738,negated_conjecture,
( ~ c8_1(X2)
| c10_1(X2)
| ~ c2_1(X2) ) ).
cnf(u750,negated_conjecture,
ndr1_1(a584) ).
cnf(u754,negated_conjecture,
( ~ c7_2(a584,X1)
| c9_2(a584,X1)
| c2_2(a584,X1) ) ).
cnf(u760,negated_conjecture,
ssSkC28 ).
cnf(u774,negated_conjecture,
~ ndr1_1(a595) ).
cnf(u780,negated_conjecture,
ssSkC31 ).
cnf(u785,negated_conjecture,
( ~ c8_2(X0,a506)
| c3_2(X0,X2)
| c1_2(X0,X2)
| c3_2(X0,X1)
| c2_2(X0,X1)
| ~ c6_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u789,negated_conjecture,
~ ssSkC9 ).
cnf(u793,negated_conjecture,
( ~ c1_2(X0,a506)
| c3_2(X0,X2)
| c1_2(X0,X2)
| c3_2(X0,X1)
| c2_2(X0,X1)
| ~ c6_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u797,negated_conjecture,
~ c7_0 ).
cnf(u801,negated_conjecture,
( ~ c10_1(X1)
| ~ c1_1(X1) ) ).
cnf(u824,negated_conjecture,
( ~ c8_1(X0)
| c7_2(X0,X2)
| c2_2(X0,X2)
| c10_2(X0,X2)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u835,negated_conjecture,
( ~ c5_1(X0)
| c10_1(X0)
| ~ c3_1(X0) ) ).
cnf(u838,negated_conjecture,
ssSkC27 ).
cnf(u844,negated_conjecture,
~ c3_0 ).
cnf(u854,negated_conjecture,
~ ssSkC11 ).
cnf(u858,negated_conjecture,
( ~ c4_2(X0,a512)
| ~ c2_1(X0)
| ~ c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1)
| ~ c7_2(X0,X1) ) ).
cnf(u862,negated_conjecture,
( ~ c3_2(X0,a512)
| ~ c2_1(X0)
| ~ c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1)
| ~ c7_2(X0,X1) ) ).
cnf(u872,negated_conjecture,
~ c9_0 ).
cnf(u879,negated_conjecture,
( ~ c6_2(X0,a464)
| c6_1(X0)
| c8_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1) ) ).
cnf(u883,negated_conjecture,
( ~ c2_1(X0)
| c1_2(X0,a512)
| ~ c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1)
| ~ c7_2(X0,X1) ) ).
cnf(u887,negated_conjecture,
( ~ c4_2(X0,X1)
| c6_1(X0)
| c9_2(X0,X2)
| c5_2(X0,X2)
| c4_2(X0,X2)
| c8_2(X0,X1)
| c6_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u891,negated_conjecture,
( ~ c5_2(X0,a463)
| c4_1(X0)
| c9_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u895,negated_conjecture,
( ~ c2_2(X0,a463)
| c4_1(X0)
| c9_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u899,negated_conjecture,
( ~ c6_2(X0,X1)
| c6_1(X0)
| c7_2(X0,a464)
| c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u903,negated_conjecture,
( ~ c6_2(X0,X1)
| c6_1(X0)
| c3_2(X0,a464)
| c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u911,negated_conjecture,
( ~ c8_1(X0)
| c4_2(X0,X1)
| c3_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c2_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u915,negated_conjecture,
( ~ c7_2(X0,a550)
| c3_1(X0)
| c5_2(X0,X1)
| ~ c10_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1) ) ).
cnf(u919,negated_conjecture,
( ~ c5_2(X0,a550)
| c3_1(X0)
| c5_2(X0,X1)
| ~ c10_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1) ) ).
cnf(u923,negated_conjecture,
( ~ c10_2(X0,a550)
| c3_1(X0)
| c5_2(X0,X1)
| ~ c10_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1) ) ).
cnf(u928,negated_conjecture,
~ c10_1(a562) ).
cnf(u932,negated_conjecture,
( ~ c3_2(X0,a505)
| c1_1(X0)
| c2_2(X0,X1)
| ~ c10_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1) ) ).
cnf(u936,negated_conjecture,
~ ssSkC13 ).
cnf(u940,negated_conjecture,
( ~ c2_2(X0,a520)
| c4_2(X0,X1)
| c1_2(X0,X1)
| ~ c1_1(X0)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u944,negated_conjecture,
( ~ c6_2(X0,a583)
| c6_2(X0,X1)
| c5_2(X0,X1)
| ~ c3_1(X0)
| ~ c7_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u948,negated_conjecture,
~ ssSkC30 ).
cnf(u952,negated_conjecture,
( ~ c9_2(X0,a590)
| c3_1(X0)
| c3_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1) ) ).
cnf(u956,negated_conjecture,
( ~ c10_2(X0,a590)
| c3_1(X0)
| c3_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1) ) ).
cnf(u961,negated_conjecture,
ssSkC19 ).
cnf(u964,negated_conjecture,
( ~ c8_2(X0,a545)
| ~ c10_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u969,negated_conjecture,
~ c1_0 ).
cnf(u976,negated_conjecture,
( ~ c1_2(X0,X1)
| c4_1(X0)
| c7_2(X0,a463)
| c9_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u984,negated_conjecture,
( ~ c7_1(X0)
| c5_2(X0,X1)
| ~ c8_1(X0)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u998,negated_conjecture,
( ~ c8_2(X0,a511)
| c8_2(X0,X1)
| ~ c2_1(X0)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1) ) ).
cnf(u1002,negated_conjecture,
( ~ c9_2(X0,a535)
| c5_2(X0,X1)
| ~ ssSkP6(X0)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u1006,negated_conjecture,
( ~ c8_2(X0,a535)
| c5_2(X0,X1)
| ~ ssSkP6(X0)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u1010,negated_conjecture,
( ~ c4_2(X0,a535)
| c5_2(X0,X1)
| ~ ssSkP6(X0)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u1014,negated_conjecture,
( ~ c4_2(X0,a552)
| c9_2(X0,X1)
| c5_2(X0,X1)
| ~ ssSkP7(X0)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u1018,negated_conjecture,
( ~ c10_2(X0,a552)
| c9_2(X0,X1)
| c5_2(X0,X1)
| ~ ssSkP7(X0)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u1023,negated_conjecture,
c7_1(a562) ).
cnf(u1028,negated_conjecture,
~ c9_1(a595) ).
cnf(u1033,negated_conjecture,
~ c3_1(a595) ).
cnf(u1037,negated_conjecture,
( ~ c10_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a505)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1) ) ).
cnf(u1041,negated_conjecture,
( ~ ndr1_1(X0)
| c8_2(X0,a520)
| c4_2(X0,X1)
| c1_2(X0,X1)
| ~ c1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u1054,negated_conjecture,
ssSkC36 ).
cnf(u1069,negated_conjecture,
c2_0 ).
cnf(u1081,negated_conjecture,
( ~ c10_2(X0,X1)
| c6_2(X0,a545)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u1099,negated_conjecture,
( ~ c2_1(X0)
| c4_2(X0,a511)
| c8_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1) ) ).
cnf(u1103,negated_conjecture,
( ~ c2_1(X0)
| c1_2(X0,a511)
| c8_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1) ) ).
cnf(u1111,negated_conjecture,
~ ndr1_1(a542) ).
cnf(u1118,negated_conjecture,
( ~ ssSkP7(X0)
| c3_2(X0,a552)
| c9_2(X0,X1)
| c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u1123,negated_conjecture,
~ c4_2(a584,a585) ).
cnf(u1128,negated_conjecture,
~ c2_2(a584,a585) ).
cnf(u1149,negated_conjecture,
ssSkC23 ).
cnf(u1152,negated_conjecture,
( ~ c2_2(X0,a559)
| c7_1(X0)
| c10_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1161,negated_conjecture,
~ c8_1(a584) ).
cnf(u1166,negated_conjecture,
c7_2(a584,a585) ).
cnf(u1175,negated_conjecture,
~ ndr1_1(a556) ).
cnf(u1181,negated_conjecture,
ssSkC21 ).
cnf(u1195,negated_conjecture,
ssSkC24 ).
cnf(u1207,negated_conjecture,
ssSkC41 ).
cnf(u1226,negated_conjecture,
ssSkC1 ).
cnf(u1239,negated_conjecture,
ndr1_1(a493) ).
cnf(u1263,negated_conjecture,
~ ssSkC20 ).
cnf(u1278,negated_conjecture,
ssSkC22 ).
cnf(u1292,negated_conjecture,
~ ndr1_1(a615) ).
cnf(u1298,negated_conjecture,
ssSkC39 ).
cnf(u1304,negated_conjecture,
~ ndr1_1(a619) ).
cnf(u1307,negated_conjecture,
( ~ c7_2(a619,X0)
| c3_2(a619,X0)
| ~ c4_2(a619,X0) ) ).
cnf(u1310,negated_conjecture,
ssSkC40 ).
cnf(u1316,negated_conjecture,
ssSkC0 ).
cnf(u1328,negated_conjecture,
ssSkC37 ).
cnf(u1339,negated_conjecture,
( ~ c6_2(X0,a433)
| ~ c7_1(X0)
| ~ c6_1(X0) ) ).
cnf(u1343,negated_conjecture,
( ~ c4_2(X0,a433)
| ~ c7_1(X0)
| ~ c6_1(X0) ) ).
cnf(u1359,negated_conjecture,
ndr1_1(a465) ).
cnf(u1363,negated_conjecture,
( ~ c3_2(a465,X0)
| c8_2(a465,X0)
| ~ c4_2(a465,X0) ) ).
cnf(u1383,negated_conjecture,
~ ssSkC3 ).
cnf(u1395,negated_conjecture,
~ ssSkC5 ).
cnf(u1399,negated_conjecture,
ndr1_1(a501) ).
cnf(u1403,negated_conjecture,
( ~ c6_2(a501,X0)
| c3_2(a501,X0)
| ~ c1_2(a501,X0) ) ).
cnf(u1408,negated_conjecture,
~ ndr1_1(a503) ).
cnf(u1427,negated_conjecture,
( ~ c8_2(X0,a518)
| ~ c9_1(X0)
| ~ c1_1(X0) ) ).
cnf(u1443,negated_conjecture,
( c1_2(a541,X0)
| c9_2(a541,X0)
| c3_2(a541,X0) ) ).
cnf(u1446,negated_conjecture,
ndr1_1(a541) ).
cnf(u1450,negated_conjecture,
ssSkC17 ).
cnf(u1458,negated_conjecture,
ndr1_1(a546) ).
cnf(u1467,negated_conjecture,
ndr1_1(a572) ).
cnf(u1471,negated_conjecture,
( ~ c7_2(a572,X0)
| c9_2(a572,X0)
| ~ c2_2(a572,X0) ) ).
cnf(u1474,negated_conjecture,
ssSkC25 ).
cnf(u1488,negated_conjecture,
( ~ c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ).
cnf(u1491,negated_conjecture,
ssSkC29 ).
cnf(u1509,negated_conjecture,
~ ssSkC38 ).
cnf(u1514,negated_conjecture,
~ ndr1_1(a540) ).
cnf(u1521,negated_conjecture,
~ ssSkC18 ).
cnf(u1526,negated_conjecture,
~ ndr1_1(a543) ).
cnf(u1549,negated_conjecture,
( c5_2(X0,a433)
| ~ c6_1(X0)
| ~ c7_1(X0) ) ).
cnf(u1565,negated_conjecture,
ndr1_1(a470) ).
cnf(u1569,negated_conjecture,
( c7_2(a470,X0)
| ~ c4_2(a470,X0)
| c3_2(a470,X0) ) ).
cnf(u1573,negated_conjecture,
( ~ c7_2(a501,X0)
| c9_2(a501,X0)
| c6_2(a501,X0) ) ).
cnf(u1577,negated_conjecture,
( ~ c9_1(X0)
| c4_2(X0,a518)
| ~ c1_1(X0) ) ).
cnf(u1581,negated_conjecture,
( c1_2(X0,a518)
| ~ c1_1(X0)
| ~ c9_1(X0) ) ).
cnf(u1585,negated_conjecture,
( ~ c3_2(X0,a519)
| c9_1(X0)
| ~ c1_1(X0) ) ).
cnf(u1589,negated_conjecture,
( ~ c1_2(X0,a519)
| c9_1(X0)
| ~ c1_1(X0) ) ).
cnf(u1593,negated_conjecture,
( ~ c9_2(X0,a561)
| ~ c5_1(X0)
| ~ ssSkP8(X0) ) ).
cnf(u1597,negated_conjecture,
( ~ c8_2(X0,a561)
| ~ c5_1(X0)
| ~ ssSkP8(X0) ) ).
cnf(u1601,negated_conjecture,
( ~ c1_2(X0,a561)
| ~ c5_1(X0)
| ~ ssSkP8(X0) ) ).
cnf(u1638,negated_conjecture,
~ ndr1_1(a609) ).
cnf(u1643,negated_conjecture,
ssSkC15 ).
cnf(u1658,negated_conjecture,
( ~ c6_1(X0)
| ndr1_1(X0)
| ~ c7_1(X0) ) ).
cnf(u1682,negated_conjecture,
( ~ c9_1(X0)
| ndr1_1(X0)
| ~ c1_1(X0) ) ).
cnf(u1686,negated_conjecture,
( c2_2(X0,a519)
| c9_1(X0)
| ~ c1_1(X0) ) ).
cnf(u1691,negated_conjecture,
~ c10_1(a542) ).
cnf(u1701,negated_conjecture,
( c5_2(X0,a488)
| ~ c3_1(X0)
| ~ c7_1(X0) ) ).
cnf(u1705,negated_conjecture,
( c4_2(X0,a488)
| ~ c3_1(X0)
| ~ c7_1(X0) ) ).
cnf(u1709,negated_conjecture,
( c1_2(X0,a488)
| ~ c3_1(X0)
| ~ c7_1(X0) ) ).
cnf(u1714,negated_conjecture,
ssSkC7 ).
cnf(u1726,negated_conjecture,
ssSkC10 ).
cnf(u1742,negated_conjecture,
ssSkC16 ).
cnf(u1745,negated_conjecture,
( ~ c1_2(X0,a538)
| c3_1(X0)
| ~ c8_1(X0) ) ).
cnf(u1757,negated_conjecture,
( ~ c4_2(X0,a557)
| c2_1(X0)
| ~ c8_1(X0) ) ).
cnf(u1785,negated_conjecture,
( c5_2(X0,a432)
| ~ ssSkP0(X0)
| ~ c2_1(X0) ) ).
cnf(u1789,negated_conjecture,
( ~ ssSkP0(X0)
| c4_2(X0,a432)
| ~ c2_1(X0) ) ).
cnf(u1793,negated_conjecture,
( ~ ssSkP0(X0)
| c10_2(X0,a432)
| ~ c2_1(X0) ) ).
cnf(u1797,negated_conjecture,
( ~ c4_2(X0,a476)
| ~ c2_1(X0)
| ~ ssSkP3(X0) ) ).
cnf(u1801,negated_conjecture,
( ~ c10_2(X0,a476)
| ~ c2_1(X0)
| ~ ssSkP3(X0) ) ).
cnf(u1813,negated_conjecture,
( ~ ssSkP8(X0)
| ndr1_1(X0)
| ~ c5_1(X0) ) ).
cnf(u1829,negated_conjecture,
( c9_2(X0,a473)
| ~ ssSkP2(X0)
| ~ c5_1(X0) ) ).
cnf(u1833,negated_conjecture,
( c8_2(X0,a473)
| ~ ssSkP2(X0)
| ~ c5_1(X0) ) ).
cnf(u1837,negated_conjecture,
( c5_2(X0,a473)
| ~ ssSkP2(X0)
| ~ c5_1(X0) ) ).
cnf(u1841,negated_conjecture,
( ~ c7_1(X0)
| ndr1_1(X0)
| ~ c3_1(X0) ) ).
cnf(u1857,negated_conjecture,
( c5_2(X0,a538)
| c3_1(X0)
| ~ c8_1(X0) ) ).
cnf(u1861,negated_conjecture,
( c2_2(X0,a538)
| c3_1(X0)
| ~ c8_1(X0) ) ).
cnf(u1869,negated_conjecture,
( c5_2(X0,a557)
| c2_1(X0)
| ~ c8_1(X0) ) ).
cnf(u1873,negated_conjecture,
( c10_2(X0,a557)
| c2_1(X0)
| ~ c8_1(X0) ) ).
cnf(u1885,negated_conjecture,
~ ssSkC32 ).
cnf(u1889,negated_conjecture,
( ~ c5_2(X0,a596)
| c8_1(X0)
| c5_1(X0) ) ).
cnf(u1893,negated_conjecture,
( ~ c2_2(X0,a596)
| c8_1(X0)
| c5_1(X0) ) ).
cnf(u1902,negated_conjecture,
ssSkC34 ).
cnf(u1925,negated_conjecture,
ndr1_1(a508) ).
cnf(u1929,negated_conjecture,
( ~ c6_2(a508,X0)
| c8_2(a508,X0) ) ).
cnf(u1933,negated_conjecture,
( c8_2(X0,a533)
| c7_1(X0) ) ).
cnf(u1937,negated_conjecture,
( c5_2(X0,a533)
| c7_1(X0) ) ).
cnf(u1941,negated_conjecture,
( c10_2(X0,a533)
| c7_1(X0) ) ).
cnf(u1946,negated_conjecture,
ssSkC2 ).
cnf(u1958,negated_conjecture,
ssSkC14 ).
cnf(u1961,negated_conjecture,
( ~ c2_2(X0,a523)
| ~ c10_1(X0) ) ).
cnf(u1965,negated_conjecture,
( ~ c10_2(X0,a523)
| ~ c10_1(X0) ) ).
cnf(u1969,negated_conjecture,
( ~ ssSkP0(X0)
| ndr1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u1977,negated_conjecture,
( c2_2(X0,a476)
| ~ ssSkP3(X0)
| ~ c2_1(X0) ) ).
cnf(u1985,negated_conjecture,
( ~ ssSkP2(X0)
| ndr1_1(X0)
| ~ c5_1(X0) ) ).
cnf(u2029,negated_conjecture,
( ~ c5_1(X0)
| ndr1_1(X0) ) ).
cnf(u2033,negated_conjecture,
( c7_1(X0)
| ndr1_1(X0) ) ).
cnf(u2045,negated_conjecture,
( c9_2(X0,a523)
| ~ c10_1(X0) ) ).
cnf(u2053,negated_conjecture,
( ~ ssSkP3(X0)
| ndr1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u2057,negated_conjecture,
( c3_2(X0,a504)
| c2_1(X0)
| ~ c3_1(X0) ) ).
cnf(u2061,negated_conjecture,
( c2_2(X0,a504)
| c2_1(X0)
| ~ c3_1(X0) ) ).
cnf(u2073,negated_conjecture,
( c5_1(X0)
| c8_1(X0)
| ndr1_1(X0) ) ).
cnf(u2083,negated_conjecture,
~ c7_2(a536,a537) ).
cnf(u2097,negated_conjecture,
ssSkC4 ).
cnf(u2100,negated_conjecture,
( c9_2(X0,a484)
| c2_1(X0) ) ).
cnf(u2104,negated_conjecture,
( c5_2(X0,a484)
| c2_1(X0) ) ).
cnf(u2116,negated_conjecture,
( ~ c3_1(X0)
| c2_1(X0)
| ndr1_1(X0) ) ).
cnf(u2120,negated_conjecture,
( ~ c3_1(X0)
| ~ c9_1(X0) ) ).
cnf(u2170,negated_conjecture,
~ c6_1(a536) ).
cnf(u2175,negated_conjecture,
c2_2(a536,a537) ).
cnf(u2180,negated_conjecture,
c1_2(a536,a537) ).
cnf(u2200,negated_conjecture,
~ c7_2(a568,a570) ).
cnf(u2278,negated_conjecture,
~ c6_2(a485,a486) ).
cnf(u2283,negated_conjecture,
~ c8_2(a485,a487) ).
cnf(u2288,negated_conjecture,
~ c3_2(a485,a487) ).
cnf(u2293,negated_conjecture,
~ c2_2(a485,a487) ).
cnf(u2298,negated_conjecture,
~ c4_2(a491,a492) ).
cnf(u2301,negated_conjecture,
ssSkC6 ).
cnf(u2307,negated_conjecture,
~ c1_2(a491,a492) ).
cnf(u2312,negated_conjecture,
~ c4_2(a524,a525) ).
cnf(u2328,negated_conjecture,
c10_1(a536) ).
cnf(u2333,negated_conjecture,
ndr1_1(a536) ).
cnf(u2338,negated_conjecture,
~ c9_1(a539) ).
cnf(u2343,negated_conjecture,
~ c8_1(a541) ).
cnf(u2348,negated_conjecture,
~ c5_1(a541) ).
cnf(u2353,negated_conjecture,
~ c1_1(a544) ).
cnf(u2388,negated_conjecture,
~ c7_1(a568) ).
cnf(u2393,negated_conjecture,
c9_2(a568,a569) ).
cnf(u2398,negated_conjecture,
c3_2(a568,a569) ).
cnf(u2403,negated_conjecture,
c10_2(a568,a569) ).
cnf(u2408,negated_conjecture,
c8_2(a568,a570) ).
cnf(u2413,negated_conjecture,
c5_2(a568,a570) ).
cnf(u2422,negated_conjecture,
~ ssSkC35 ).
cnf(u2492,negated_conjecture,
~ c7_2(a613,a614) ).
cnf(u2497,negated_conjecture,
~ c4_2(a613,a614) ).
cnf(u2502,negated_conjecture,
~ c2_2(a613,a614) ).
cnf(u2519,negated_conjecture,
~ c9_1(a436) ).
cnf(u2524,negated_conjecture,
~ c3_1(a436) ).
cnf(u2609,negated_conjecture,
~ c1_2(a465,a466) ).
cnf(u2639,negated_conjecture,
~ c4_2(a479,a481) ).
cnf(u2654,negated_conjecture,
c7_2(a485,a486) ).
cnf(u2659,negated_conjecture,
c5_2(a485,a486) ).
cnf(u2669,negated_conjecture,
~ c4_1(a491) ).
cnf(u2674,negated_conjecture,
c3_2(a491,a492) ).
cnf(u2679,negated_conjecture,
c2_1(a493) ).
cnf(u2684,negated_conjecture,
~ c6_1(a498) ).
cnf(u2689,negated_conjecture,
~ c2_1(a498) ).
cnf(u2694,negated_conjecture,
~ c2_2(a501,a502) ).
cnf(u2699,negated_conjecture,
~ c6_1(a503) ).
cnf(u2704,negated_conjecture,
~ c9_2(a508,a509) ).
cnf(u2709,negated_conjecture,
~ c5_2(a508,a509) ).
cnf(u2714,negated_conjecture,
~ c2_2(a508,a509) ).
cnf(u2739,negated_conjecture,
c7_2(a524,a525) ).
cnf(u2744,negated_conjecture,
c3_2(a524,a525) ).
cnf(u2774,negated_conjecture,
c3_1(a539) ).
cnf(u2778,negated_conjecture,
~ c6_1(a544) ).
cnf(u2783,negated_conjecture,
~ c2_1(a544) ).
cnf(u2789,negated_conjecture,
c3_1(a546) ).
cnf(u2800,negated_conjecture,
~ c1_1(a564) ).
cnf(u2805,negated_conjecture,
c4_2(a564,a565) ).
cnf(u2810,negated_conjecture,
c10_2(a564,a565) ).
cnf(u2815,negated_conjecture,
ndr1_1(a568) ).
cnf(u2820,negated_conjecture,
~ c10_2(a572,a573) ).
cnf(u2825,negated_conjecture,
~ c1_2(a572,a573) ).
cnf(u2865,negated_conjecture,
~ c3_1(a609) ).
cnf(u2880,negated_conjecture,
~ c3_1(a619) ).
cnf(u2900,negated_conjecture,
ssSkC8 ).
cnf(u2908,negated_conjecture,
~ ssSkC12 ).
cnf(u2913,negated_conjecture,
~ c7_1(a515) ).
cnf(u2917,negated_conjecture,
c8_1(a540) ).
cnf(u2923,negated_conjecture,
~ c2_1(a540) ).
cnf(u2928,negated_conjecture,
~ c8_1(a547) ).
cnf(u2933,negated_conjecture,
~ c1_1(a547) ).
cnf(u2958,negated_conjecture,
~ c8_1(a603) ).
cnf(u2963,negated_conjecture,
~ c6_1(a603) ).
cnf(u2968,negated_conjecture,
~ c10_1(a603) ).
cnf(u2987,negated_conjecture,
c7_1(a436) ).
cnf(u3028,negated_conjecture,
~ c10_1(a465) ).
cnf(u3033,negated_conjecture,
c6_2(a465,a466) ).
cnf(u3038,negated_conjecture,
c2_2(a465,a466) ).
cnf(u3044,negated_conjecture,
c8_2(a470,a471) ).
cnf(u3049,negated_conjecture,
c7_2(a470,a471) ).
cnf(u3059,negated_conjecture,
c9_2(a479,a480) ).
cnf(u3064,negated_conjecture,
c10_2(a479,a480) ).
cnf(u3069,negated_conjecture,
c8_2(a479,a481) ).
cnf(u3074,negated_conjecture,
c5_2(a479,a481) ).
cnf(u3079,negated_conjecture,
c1_1(a485) ).
cnf(u3084,negated_conjecture,
ndr1_1(a485) ).
cnf(u3094,negated_conjecture,
c8_1(a491) ).
cnf(u3099,negated_conjecture,
ndr1_1(a491) ).
cnf(u3104,negated_conjecture,
c4_1(a500) ).
cnf(u3109,negated_conjecture,
c10_1(a500) ).
cnf(u3114,negated_conjecture,
c9_2(a501,a502) ).
cnf(u3119,negated_conjecture,
c3_2(a501,a502) ).
cnf(u3130,negated_conjecture,
c3_1(a524) ).
cnf(u3135,negated_conjecture,
ndr1_1(a524) ).
cnf(u3158,negated_conjecture,
c10_1(a564) ).
cnf(u3163,negated_conjecture,
ndr1_1(a564) ).
cnf(u3168,negated_conjecture,
~ c1_1(a572) ).
cnf(u3173,negated_conjecture,
c8_2(a572,a573) ).
cnf(u3198,negated_conjecture,
~ c1_1(a615) ).
cnf(u3203,negated_conjecture,
c8_1(a619) ).
cnf(u3235,negated_conjecture,
c8_1(a515) ).
cnf(u3240,negated_conjecture,
c1_1(a515) ).
cnf(u3245,negated_conjecture,
c1_1(a543) ).
cnf(u3296,negated_conjecture,
c1_1(a610) ).
cnf(u3300,negated_conjecture,
~ c8_1(a613) ).
cnf(u3306,negated_conjecture,
c3_1(a613) ).
cnf(u3311,negated_conjecture,
ndr1_1(a613) ).
cnf(u3342,negated_conjecture,
~ c8_1(a470) ).
cnf(u3349,negated_conjecture,
ndr1_1(a479) ).
cnf(u3407,negated_conjecture,
c7_1(a615) ).
cnf(u3453,negated_conjecture,
~ c2_1(a515) ).
cnf(u3456,negated_conjecture,
~ c3_1(a515) ).
cnf(u3465,negated_conjecture,
~ c2_1(a610) ).
cnf(u3489,negated_conjecture,
~ c2_1(a470) ).
cnf(u3507,negated_conjecture,
~ c2_1(a613) ).
cnf(u3510,negated_conjecture,
~ c10_1(a613) ).
cnf(u3536,negated_conjecture,
~ c1_1(a613) ).
cnf(u3562,negated_conjecture,
~ c7_1(a613) ).
cnf(u3612,negated_conjecture,
~ c2_1(a619) ).
cnf(u3642,negated_conjecture,
~ c1_1(a568) ).
cnf(u3659,negated_conjecture,
~ ndr1_1(a436) ).
cnf(u3673,negated_conjecture,
~ c3_2(a465,a466) ).
cnf(u3692,negated_conjecture,
~ c3_2(a536,a537) ).
cnf(u3711,negated_conjecture,
~ c3_1(a465) ).
cnf(u3752,negated_conjecture,
~ c1_1(a536) ).
cnf(u3770,negated_conjecture,
~ ndr1_1(a544) ).
cnf(u3798,negated_conjecture,
~ c8_2(a564,a565) ).
cnf(u3802,negated_conjecture,
~ c9_2(a564,a565) ).
cnf(u3815,negated_conjecture,
~ c1_1(a501) ).
cnf(u3836,negated_conjecture,
~ ndr1_1(a500) ).
cnf(u3854,negated_conjecture,
~ c1_1(a524) ).
cnf(u3887,negated_conjecture,
~ c1_1(a470) ).
cnf(u3904,negated_conjecture,
~ c2_2(a568,a569) ).
cnf(u3921,negated_conjecture,
~ c1_1(a584) ).
cnf(u3934,negated_conjecture,
~ c1_1(a465) ).
cnf(u3951,negated_conjecture,
~ c1_1(a619) ).
cnf(u3989,negated_conjecture,
( c3_2(a515,X1)
| c9_2(a515,X1)
| c8_2(a515,X1) ) ).
cnf(u4013,negated_conjecture,
ndr1_1(a515) ).
cnf(u4025,negated_conjecture,
~ c2_2(a479,a480) ).
cnf(u4051,negated_conjecture,
~ c10_1(a524) ).
cnf(u4079,negated_conjecture,
~ c1_1(a479) ).
cnf(u4094,negated_conjecture,
~ c2_1(a491) ).
cnf(u4108,negated_conjecture,
( c3_2(a491,X1)
| c9_2(a491,X1)
| c8_2(a491,X1) ) ).
cnf(u4122,negated_conjecture,
~ c4_2(a470,a550) ).
cnf(u4135,negated_conjecture,
~ c1_1(a491) ).
cnf(u4166,negated_conjecture,
c7_2(a515,a463) ).
cnf(u4174,negated_conjecture,
c8_2(a515,a475) ).
cnf(u4183,negated_conjecture,
ssSkP11(a515) ).
cnf(u4196,negated_conjecture,
c9_1(a515) ).
cnf(u4209,negated_conjecture,
ssSkP1(a515) ).
cnf(u4222,negated_conjecture,
~ c10_1(a539) ).
cnf(u4246,negated_conjecture,
c7_2(a491,a463) ).
cnf(u4276,negated_conjecture,
c8_2(a491,a446) ).
cnf(u4297,negated_conjecture,
( ~ c9_2(a493,X0)
| c8_2(a493,X0)
| ~ c2_2(a493,X0) ) ).
cnf(u4310,negated_conjecture,
( ~ c7_2(a493,X0)
| ~ c4_2(a493,X0)
| ~ c9_2(a493,X0) ) ).
cnf(u4320,negated_conjecture,
~ c2_1(a485) ).
cnf(u4323,negated_conjecture,
~ c3_1(a485) ).
cnf(u4330,negated_conjecture,
( ~ c3_2(a485,X0)
| c4_2(a485,X0)
| c1_2(a485,X0) ) ).
cnf(u4340,negated_conjecture,
~ c2_1(a543) ).
cnf(u4364,negated_conjecture,
~ c1_1(a493) ).
cnf(u4381,negated_conjecture,
c8_2(a515,a520) ).
cnf(u4404,negated_conjecture,
c8_2(a515,a431) ).
cnf(u4419,negated_conjecture,
c3_2(a470,a496) ).
cnf(u4433,negated_conjecture,
~ c4_2(a470,a593) ).
cnf(u4449,negated_conjecture,
~ c4_2(a470,a551) ).
cnf(u4470,negated_conjecture,
~ ssSkP7(a515) ).
cnf(u4489,negated_conjecture,
~ c10_1(a546) ).
cnf(u4498,negated_conjecture,
~ c1_1(a546) ).
cnf(u4515,negated_conjecture,
~ c4_2(a470,a475) ).
cnf(u4552,negated_conjecture,
ssSkP8(a515) ).
cnf(u4584,negated_conjecture,
~ c1_1(a508) ).
cnf(u4604,negated_conjecture,
~ c1_2(a501,a560) ).
cnf(u4617,negated_conjecture,
c8_2(a508,a560) ).
cnf(u4633,negated_conjecture,
c9_2(a491,a560) ).
cnf(u4666,negated_conjecture,
c6_1(a515) ).
cnf(u4681,negated_conjecture,
~ c3_2(a485,a560) ).
cnf(u4698,negated_conjecture,
~ c4_2(a465,a464) ).
cnf(u4706,negated_conjecture,
~ c3_2(a465,a560) ).
cnf(u4741,negated_conjecture,
c6_2(a564,a565) ).
cnf(u4765,negated_conjecture,
~ c3_2(a564,a565) ).
cnf(u4773,negated_conjecture,
c6_2(a564,a506) ).
cnf(u4795,negated_conjecture,
~ c3_2(a564,a506) ).
cnf(u4830,negated_conjecture,
~ c1_2(a501,a496) ).
cnf(u4841,negated_conjecture,
~ c8_2(a501,a496) ).
cnf(u4846,negated_conjecture,
c6_1(a501) ).
cnf(u4854,negated_conjecture,
ssSkP5(a508) ).
cnf(u4895,negated_conjecture,
ssSkP0(a508) ).
cnf(u4904,negated_conjecture,
c3_2(a501,a431) ).
cnf(u4918,negated_conjecture,
~ c7_2(a501,a463) ).
cnf(u4923,negated_conjecture,
c4_1(a501) ).
cnf(u4945,negated_conjecture,
c9_2(a491,a431) ).
cnf(u4959,negated_conjecture,
( ~ c9_2(a501,X1)
| ~ c8_2(a501,X1)
| ~ c5_2(a501,X1) ) ).
cnf(u4973,negated_conjecture,
~ c10_1(a501) ).
cnf(u4986,negated_conjecture,
~ c5_2(a501,a502) ).
cnf(u4999,negated_conjecture,
~ c8_2(a501,a484) ).
cnf(u5009,negated_conjecture,
~ ssSkP2(a501) ).
cnf(u5018,negated_conjecture,
~ c8_2(a501,a431) ).
cnf(u5030,negated_conjecture,
~ c3_2(a485,a431) ).
cnf(u5160,negated_conjecture,
c8_2(a491,a505) ).
cnf(u5199,negated_conjecture,
~ c3_2(a479,a505) ).
cnf(u5237,negated_conjecture,
~ c2_1(a508) ).
cnf(u5253,negated_conjecture,
( ~ c6_2(a501,X1)
| ~ c5_2(a501,X1)
| ~ c8_2(a501,X1) ) ).
cnf(u5270,negated_conjecture,
~ c8_2(a501,a560) ).
cnf(u5302,negated_conjecture,
~ c8_2(a515,a518) ).
cnf(u5305,negated_conjecture,
c9_2(a515,a518) ).
cnf(u5323,negated_conjecture,
c6_2(a515,a518) ).
cnf(u5341,negated_conjecture,
~ c3_2(a515,a518) ).
cnf(u5366,negated_conjecture,
~ c2_2(a493,a496) ).
cnf(u5392,negated_conjecture,
c8_2(a493,a472) ).
cnf(u5405,negated_conjecture,
~ c8_2(a501,a472) ).
cnf(u5437,negated_conjecture,
~ c3_2(a568,a505) ).
cnf(u5471,negated_conjecture,
~ c1_1(a539) ).
cnf(u5485,negated_conjecture,
~ c1_1(a603) ).
cnf(u5510,negated_conjecture,
~ c8_2(a470,a496) ).
cnf(u5514,negated_conjecture,
( c5_2(a470,X0)
| c4_2(a470,X0)
| c9_2(a470,X0) ) ).
cnf(u5546,negated_conjecture,
~ c4_1(a470) ).
cnf(u5551,negated_conjecture,
c9_2(a470,a463) ).
cnf(u5564,negated_conjecture,
c9_2(a470,a596) ).
cnf(u5577,negated_conjecture,
c9_2(a470,a534) ).
cnf(u5582,negated_conjecture,
c9_2(a470,a550) ).
cnf(u5608,negated_conjecture,
~ c3_2(a485,a496) ).
cnf(u5660,negated_conjecture,
c9_2(a568,a550) ).
cnf(u5689,negated_conjecture,
c9_2(a479,a550) ).
cnf(u5736,negated_conjecture,
~ c7_1(a539) ).
cnf(u5756,negated_conjecture,
~ c7_1(a546) ).
cnf(u5776,negated_conjecture,
~ c7_1(a524) ).
cnf(u5838,negated_conjecture,
( ~ c7_2(a541,X0)
| c3_2(a541,X0)
| c1_2(a541,X0) ) ).
cnf(u5851,negated_conjecture,
~ c1_1(a541) ).
cnf(u5931,negated_conjecture,
~ c6_2(a491,a496) ).
cnf(u5936,negated_conjecture,
ssSkP5(a491) ).
cnf(u5958,negated_conjecture,
c3_2(a491,a496) ).
cnf(u6023,negated_conjecture,
c6_2(a515,a496) ).
cnf(u6034,negated_conjecture,
~ c8_2(a515,a496) ).
cnf(u6049,negated_conjecture,
c3_2(a515,a496) ).
cnf(u6054,negated_conjecture,
c10_2(a515,a496) ).
cnf(u5188,negated_conjecture,
c6_2(a568,a505) ).
cnf(u4734,negated_conjecture,
( c5_2(X0,X1)
| c6_2(X0,a496)
| c6_1(X0)
| c4_2(X0,X1)
| c8_2(X0,a496)
| c9_2(X0,X1)
| ssSkP5(X0) ) ).
cnf(u3762,negated_conjecture,
~ c1_1(a500) ).
cnf(u4040,negated_conjecture,
( ~ c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u4873,negated_conjecture,
( ~ c1_2(X0,X1)
| c6_1(X0)
| c4_2(X0,a463)
| c8_2(X0,a496)
| c9_2(X0,a463)
| ssSkP5(X0)
| c4_1(X0)
| c9_2(X0,X1)
| c6_2(X0,a496)
| ~ c3_2(X0,X1) ) ).
cnf(u4869,negated_conjecture,
( ~ c3_2(X0,a496)
| c6_1(X0)
| c4_2(X0,X1)
| c8_2(X0,a496)
| c9_2(X0,X1)
| ssSkP5(X0)
| c3_2(X0,a464)
| c5_2(X0,X1) ) ).
cnf(u3915,negated_conjecture,
c9_2(a584,a585) ).
cnf(u5714,negated_conjecture,
( ~ c3_2(X0,a475)
| c4_2(X0,a463)
| c8_2(X0,a496)
| c9_2(X0,a463)
| ssSkP5(X0)
| c4_1(X0)
| c9_2(X0,a475)
| c6_2(X0,a496)
| c6_1(X0)
| ssSkP3(X0) ) ).
cnf(u5713,negated_conjecture,
( ~ c3_2(X0,a551)
| c4_2(X0,a463)
| c8_2(X0,a496)
| c9_2(X0,a463)
| ssSkP5(X0)
| c4_1(X0)
| c9_2(X0,a551)
| c6_2(X0,a496)
| c6_1(X0)
| ssSkP7(X0) ) ).
cnf(clause100,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(clause91,negated_conjecture,
( ssSkP6(X0)
| ndr1_1(X0) ) ).
cnf(clause282,negated_conjecture,
( ~ c6_2(X0,a598)
| ssSkP10(X0) ) ).
cnf(u4285,negated_conjecture,
ndr1_1(a539) ).
cnf(clause284,negated_conjecture,
( ~ c7_2(X0,a593)
| ssSkP9(X0) ) ).
cnf(u4284,negated_conjecture,
( ~ c3_2(X0,a488)
| ~ c7_1(X0)
| c4_1(X0)
| c7_2(X0,a463)
| c9_2(X0,a488)
| ~ c3_1(X0) ) ).
cnf(clause76,negated_conjecture,
( ssSkP11(X0)
| ndr1_1(X0) ) ).
cnf(clause184,negated_conjecture,
( c4_2(X0,a496)
| ssSkP5(X0) ) ).
cnf(clause191,negated_conjecture,
( c2_2(X0,a472)
| ssSkP2(X0) ) ).
cnf(u3965,negated_conjecture,
( ~ c3_2(X0,a475)
| c4_1(X0)
| c7_2(X0,a463)
| c9_2(X0,a475)
| ssSkP3(X0) ) ).
cnf(u5720,negated_conjecture,
( ~ c3_2(X0,a446)
| c4_2(X0,a463)
| c8_2(X0,a496)
| c9_2(X0,a463)
| ssSkP5(X0)
| c4_1(X0)
| c6_2(X0,a496)
| c6_1(X0)
| ssSkP1(X0) ) ).
cnf(clause299,negated_conjecture,
( ~ c9_2(X0,a446)
| ssSkP1(X0) ) ).
cnf(clause295,negated_conjecture,
( ~ c7_2(X0,a475)
| ssSkP3(X0) ) ).
cnf(u5418,negated_conjecture,
( c3_2(X0,a464)
| c4_2(X0,a596)
| c8_2(X0,a496)
| c9_2(X0,a596)
| ssSkP5(X0)
| c8_1(X0)
| c5_1(X0)
| c6_1(X0)
| ~ c3_2(X0,a496) ) ).
cnf(u4062,negated_conjecture,
( ~ c2_2(X0,a533)
| c6_2(X0,a545)
| c7_1(X0) ) ).
cnf(u5712,negated_conjecture,
( ~ c3_2(X0,a601)
| c4_2(X0,a463)
| c8_2(X0,a496)
| c9_2(X0,a463)
| ssSkP5(X0)
| c4_1(X0)
| c9_2(X0,a601)
| c6_2(X0,a496)
| c6_1(X0)
| ssSkP11(X0) ) ).
cnf(u5416,negated_conjecture,
( ~ c4_2(X0,X1)
| c4_2(X0,a596)
| c8_2(X0,a496)
| c9_2(X0,a596)
| ssSkP5(X0)
| c8_1(X0)
| c5_1(X0)
| c10_2(X0,a496)
| c9_2(X0,X1)
| ~ c5_2(X0,X2)
| ~ c3_2(X0,a496)
| ~ c8_2(X0,X1)
| c6_1(X0)
| ~ c9_2(X0,X2)
| ~ c8_2(X0,X2) ) ).
cnf(clause106,negated_conjecture,
( ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(clause88,negated_conjecture,
( ssSkP8(X0)
| ndr1_1(X0) ) ).
cnf(u3477,negated_conjecture,
( c8_1(X0)
| ndr1_1(X0) ) ).
cnf(clause174,negated_conjecture,
( c6_2(X0,a560)
| ssSkP8(X0) ) ).
cnf(clause192,negated_conjecture,
( c9_2(X0,a472)
| ssSkP2(X0) ) ).
cnf(clause173,negated_conjecture,
( c5_2(X0,a560)
| ssSkP8(X0) ) ).
cnf(clause195,negated_conjecture,
( c1_2(X0,a446)
| ssSkP1(X0) ) ).
cnf(clause167,negated_conjecture,
( c5_2(X0,a593)
| ssSkP9(X0) ) ).
cnf(u4867,negated_conjecture,
( ~ c3_2(X0,a496)
| c6_1(X0)
| c4_2(X0,X1)
| c8_2(X0,a496)
| c9_2(X0,X1)
| ssSkP5(X0)
| c10_2(X0,a496)
| c9_2(X0,X2)
| ~ c5_2(X0,X3)
| c5_2(X0,X1)
| ~ c8_2(X0,X2)
| ~ c4_2(X0,X2)
| ~ c9_2(X0,X3)
| ~ c8_2(X0,X3) ) ).
cnf(clause197,negated_conjecture,
( c6_2(X0,a431)
| ssSkP0(X0) ) ).
cnf(u4281,negated_conjecture,
~ c3_1(a562) ).
cnf(u3963,negated_conjecture,
( ~ c3_2(X0,a446)
| c4_1(X0)
| c7_2(X0,a463)
| ssSkP1(X0) ) ).
cnf(u4725,negated_conjecture,
ndr1_1(a603) ).
cnf(u4282,negated_conjecture,
( ~ c9_2(X0,a488)
| ~ c7_1(X0)
| c3_2(X0,a577)
| c9_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c3_1(X0)
| ~ c8_2(X0,a488) ) ).
cnf(clause296,negated_conjecture,
( ~ c3_2(X0,a472)
| ssSkP2(X0) ) ).
cnf(clause185,negated_conjecture,
( c9_2(X0,a496)
| ssSkP5(X0) ) ).
cnf(clause99,negated_conjecture,
( ssSkP3(X0)
| ndr1_1(X0) ) ).
cnf(clause292,negated_conjecture,
( ~ c4_2(X0,a534)
| ssSkP6(X0) ) ).
cnf(clause95,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(u4874,negated_conjecture,
( c6_2(X0,a496)
| c6_1(X0)
| c8_2(X0,a496)
| c9_2(X0,a534)
| ssSkP5(X0)
| ssSkP6(X0) ) ).
cnf(u3473,negated_conjecture,
~ c9_1(a613) ).
cnf(u5417,negated_conjecture,
( ~ c3_2(X0,a496)
| c4_2(X0,a596)
| c8_2(X0,a496)
| c9_2(X0,a596)
| ssSkP5(X0)
| c8_1(X0)
| c5_1(X0)
| c7_2(X0,a464)
| c6_1(X0) ) ).
cnf(u5717,negated_conjecture,
( ~ c3_2(X0,a488)
| c4_2(X0,a463)
| c8_2(X0,a496)
| c9_2(X0,a463)
| ssSkP5(X0)
| c4_1(X0)
| c9_2(X0,a488)
| c6_2(X0,a496)
| c6_1(X0)
| ~ c3_1(X0)
| ~ c7_1(X0) ) ).
cnf(u5718,negated_conjecture,
( ~ c9_1(X0)
| c4_2(X0,a463)
| c8_2(X0,a496)
| c9_2(X0,a463)
| ssSkP5(X0)
| c4_1(X0)
| c9_2(X0,a518)
| c6_2(X0,a496)
| ~ c3_2(X0,a518)
| ~ c1_1(X0)
| c6_1(X0) ) ).
cnf(u3946,negated_conjecture,
( ~ c3_2(X0,a601)
| c4_1(X0)
| c7_2(X0,a463)
| c9_2(X0,a601)
| ssSkP11(X0) ) ).
cnf(clause78,negated_conjecture,
( ssSkP9(X0)
| ndr1_1(X0) ) ).
cnf(clause77,negated_conjecture,
( ssSkP10(X0)
| ndr1_1(X0) ) ).
cnf(u3898,negated_conjecture,
( ~ c2_2(X0,a557)
| ~ ndr1_1(X0)
| ~ c8_2(X0,a557)
| c6_2(X0,a545)
| c2_1(X0)
| ~ c8_1(X0) ) ).
cnf(u6358,negated_conjecture,
( ~ c8_2(X0,a488)
| c8_2(X0,a496)
| c9_2(X0,a596)
| ssSkP5(X0)
| c8_1(X0)
| c5_1(X0)
| c10_2(X0,a496)
| c9_2(X0,a488)
| ~ c5_2(X0,X1)
| ~ c3_2(X0,a496)
| c4_2(X0,a596)
| c6_1(X0)
| ~ c9_2(X0,X1)
| ~ c8_2(X0,X1)
| ~ c3_1(X0)
| ~ c7_1(X0) ) ).
cnf(u5709,negated_conjecture,
( ~ c4_2(X0,X1)
| c8_2(X0,a496)
| c9_2(X0,a534)
| ssSkP5(X0)
| ssSkP6(X0)
| c10_2(X0,a496)
| c9_2(X0,X1)
| ~ c5_2(X0,X2)
| ~ c3_2(X0,a496)
| ~ c8_2(X0,X1)
| c6_1(X0)
| ~ c9_2(X0,X2)
| ~ c8_2(X0,X2) ) ).
cnf(u4899,negated_conjecture,
( c3_2(X0,a464)
| c6_1(X0)
| ssSkP0(X0)
| c8_2(X0,a431)
| ~ c3_2(X0,a431) ) ).
cnf(clause186,negated_conjecture,
( c2_2(X0,a494)
| ssSkP4(X0) ) ).
cnf(clause188,negated_conjecture,
( c8_2(X0,a494)
| ssSkP4(X0) ) ).
cnf(u4624,negated_conjecture,
( ~ c3_2(X0,a560)
| c6_1(X0)
| c7_2(X0,a464)
| c8_2(X0,a560)
| ssSkP8(X0) ) ).
cnf(clause181,negated_conjecture,
( c8_2(X0,a534)
| ssSkP6(X0) ) ).
cnf(u4814,negated_conjecture,
( c6_2(X0,a496)
| c6_1(X0)
| c4_2(X0,a596)
| c8_2(X0,a496)
| c9_2(X0,a596)
| ssSkP5(X0)
| c8_1(X0)
| c5_1(X0) ) ).
cnf(clause303,negated_conjecture,
( ~ c10_2(X0,a431)
| ssSkP0(X0) ) ).
cnf(clause175,negated_conjecture,
( c1_2(X0,a551)
| ssSkP7(X0) ) ).
cnf(clause283,negated_conjecture,
( ~ c6_2(X0,a593)
| ssSkP9(X0) ) ).
cnf(u3971,negated_conjecture,
( ~ c8_2(X0,a496)
| c9_2(X0,a577)
| c9_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c1_2(X0,X1)
| ssSkP5(X0) ) ).
cnf(clause279,negated_conjecture,
( ~ c2_2(X0,a601)
| ssSkP11(X0) ) ).
cnf(u4459,negated_conjecture,
( ~ c3_2(X0,a551)
| c4_1(X0)
| c7_2(X0,a463)
| c9_2(X0,a551)
| ssSkP7(X0) ) ).
cnf(u4008,negated_conjecture,
( ~ c2_1(X0)
| ndr1_1(X0) ) ).
cnf(u5169,negated_conjecture,
( ~ c9_2(X0,a557)
| c6_2(X0,a505)
| c2_2(X0,a557)
| ~ ndr1_1(X0)
| c1_1(X0)
| c2_1(X0)
| ~ c8_1(X0) ) ).
cnf(clause103,negated_conjecture,
( ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(u4733,negated_conjecture,
( ~ c3_1(X0)
| c9_2(X0,X1)
| c5_2(X0,X1)
| c4_2(X0,X1)
| c8_2(X0,a488)
| c6_2(X0,a488)
| c6_1(X0)
| ~ c7_1(X0) ) ).
cnf(clause89,negated_conjecture,
( ssSkP7(X0)
| ndr1_1(X0) ) ).
cnf(clause281,negated_conjecture,
( ~ c10_2(X0,a598)
| ssSkP10(X0) ) ).
cnf(u5189,negated_conjecture,
c6_2(a479,a505) ).
cnf(u4283,negated_conjecture,
( ~ c9_2(X0,a488)
| ~ c7_1(X0)
| c9_2(X0,a577)
| c9_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c3_1(X0)
| ~ c8_2(X0,a488) ) ).
cnf(u5291,negated_conjecture,
( ~ c9_1(X0)
| ~ c1_1(X0)
| c4_1(X0)
| c7_2(X0,a463)
| c9_2(X0,a518)
| ~ c3_2(X0,a518) ) ).
cnf(u5710,negated_conjecture,
( ~ c3_2(X0,a496)
| c8_2(X0,a496)
| c9_2(X0,a534)
| ssSkP5(X0)
| ssSkP6(X0)
| c7_2(X0,a464)
| c6_1(X0) ) ).
cnf(clause298,negated_conjecture,
( ~ c6_2(X0,a446)
| ssSkP1(X0) ) ).
cnf(u3602,negated_conjecture,
~ c9_1(a546) ).
cnf(clause96,negated_conjecture,
( ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(clause294,negated_conjecture,
( ~ c7_2(X0,a496)
| ssSkP5(X0) ) ).
cnf(clause280,negated_conjecture,
( ~ c4_2(X0,a601)
| ssSkP11(X0) ) ).
cnf(u4726,negated_conjecture,
ndr1_1(a547) ).
cnf(u6363,negated_conjecture,
( ~ c8_2(X0,a488)
| c9_2(X0,a534)
| ssSkP5(X0)
| ssSkP6(X0)
| c10_2(X0,a496)
| c9_2(X0,a488)
| ~ c5_2(X0,X1)
| ~ c3_2(X0,a496)
| c8_2(X0,a496)
| c6_1(X0)
| ~ c9_2(X0,X1)
| ~ c8_2(X0,X1)
| ~ c3_1(X0)
| ~ c7_1(X0) ) ).
cnf(clause172,negated_conjecture,
( c2_2(X0,a560)
| ssSkP8(X0) ) ).
cnf(u3840,negated_conjecture,
~ c9_1(a524) ).
cnf(u5716,negated_conjecture,
( ~ c3_2(X0,a431)
| c4_2(X0,a463)
| c8_2(X0,a496)
| c9_2(X0,a463)
| ssSkP5(X0)
| c4_1(X0)
| c9_2(X0,a431)
| c6_2(X0,a496)
| c6_1(X0)
| ssSkP0(X0) ) ).
cnf(u4625,negated_conjecture,
( c3_2(X0,a464)
| c6_1(X0)
| ssSkP8(X0)
| c8_2(X0,a560)
| ~ c3_2(X0,a560) ) ).
cnf(u3970,negated_conjecture,
( ~ c8_2(X0,a496)
| c3_2(X0,a577)
| c9_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c1_2(X0,X1)
| ssSkP5(X0) ) ).
cnf(clause291,negated_conjecture,
( ~ c7_2(X0,a551)
| ssSkP7(X0) ) ).
cnf(u5289,negated_conjecture,
c4_2(a515,a518) ).
cnf(u4872,negated_conjecture,
( ~ c10_2(X0,X1)
| c6_1(X0)
| c4_2(X0,a550)
| c8_2(X0,a496)
| c9_2(X0,a550)
| ssSkP5(X0)
| c3_1(X0)
| c5_2(X0,X1)
| c6_2(X0,a496)
| ~ c9_2(X0,X1) ) ).
cnf(clause293,negated_conjecture,
( ~ c5_2(X0,a534)
| ssSkP6(X0) ) ).
cnf(u4868,negated_conjecture,
( ~ c3_2(X0,a496)
| c6_1(X0)
| c4_2(X0,X1)
| c8_2(X0,a496)
| c9_2(X0,X1)
| ssSkP5(X0)
| c7_2(X0,a464)
| c5_2(X0,X1) ) ).
cnf(u5177,negated_conjecture,
( ~ c9_2(X0,a533)
| c6_2(X0,a505)
| c2_2(X0,a533)
| c1_1(X0)
| c7_1(X0) ) ).
cnf(u4623,negated_conjecture,
( ~ c3_2(X0,a560)
| c10_2(X0,a560)
| c9_2(X0,X1)
| ~ c5_2(X0,X2)
| ssSkP8(X0)
| ~ c8_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ c9_2(X0,X2)
| ~ c8_2(X0,X2) ) ).
cnf(clause187,negated_conjecture,
( c5_2(X0,a494)
| ssSkP4(X0) ) ).
cnf(clause190,negated_conjecture,
( c1_2(X0,a475)
| ssSkP3(X0) ) ).
cnf(clause176,negated_conjecture,
( c2_2(X0,a551)
| ssSkP7(X0) ) ).
cnf(u4396,negated_conjecture,
( ~ c3_2(X0,a431)
| c4_1(X0)
| c7_2(X0,a463)
| c9_2(X0,a431)
| ssSkP0(X0) ) ).
cnf(clause166,negated_conjecture,
( c2_2(X0,a598)
| ssSkP10(X0) ) ).
cnf(clause196,negated_conjecture,
( c1_2(X0,a431)
| ssSkP0(X0) ) ).
cnf(clause165,negated_conjecture,
( c1_2(X0,a601)
| ssSkP11(X0) ) ).
cnf(u4898,negated_conjecture,
( ~ c3_2(X0,a431)
| c6_1(X0)
| c7_2(X0,a464)
| c8_2(X0,a431)
| ssSkP0(X0) ) ).
cnf(u5711,negated_conjecture,
( c3_2(X0,a464)
| c8_2(X0,a496)
| c9_2(X0,a534)
| ssSkP5(X0)
| ssSkP6(X0)
| c6_1(X0)
| ~ c3_2(X0,a496) ) ).
cnf(u4910,negated_conjecture,
( ~ c3_2(X0,a431)
| c9_2(X0,X1)
| ~ c5_2(X0,X2)
| ssSkP0(X0)
| ~ c8_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ c9_2(X0,X2)
| ~ c8_2(X0,X2) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYN423-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Mon Sep 28 15:55:34 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.12 Running first-order theorem proving
% 0.08/0.12 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
% 6.85/1.41 % (3482818)Input is clausal, will run a generic CNF schedule.
% 6.85/1.41 % (3482826)lrs+10_1_sil=8000:sp=occurrence:random_seed=3310249918:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.85/1.41 % (3482829)dis-21_1_sil=8000:lcm=predicate:random_seed=1818303405:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 6.85/1.41 % (3482824)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2044367400:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.85/1.41 % (3482827)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4159593701:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.85/1.41 % (3482828)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=175576184:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.85/1.41 % (3482825)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2571548145:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.85/1.41 % (3482823)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=340215500:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.85/1.41 % (3482828)Refutation not found, incomplete strategy
% 6.85/1.41 % (3482828)------------------------------
% 6.85/1.41 % (3482828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/1.41 % (3482828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.41 % (3482828)CaDiCaL version: 2.1.3
% 6.85/1.41 % (3482828)Termination reason: Refutation not found, incomplete strategy
% 6.85/1.41 % (3482828)Time elapsed: 0.020 s
% 6.85/1.41 % (3482828)Peak memory usage: 91 MB
% 6.85/1.41 % (3482828)Instructions burned: 58 (million)
% 6.85/1.41 % (3482826)Instruction limit reached!
% 6.85/1.41 % (3482826)------------------------------
% 6.85/1.41 % (3482826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/1.41 % (3482826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.41 % (3482826)CaDiCaL version: 2.1.3
% 6.85/1.41 % (3482826)Termination reason: Instruction limit
% 6.85/1.41 % (3482826)Termination phase: Saturation
% 6.85/1.41 % (3482826)Time elapsed: 0.032 s
% 6.85/1.41 % (3482826)Peak memory usage: 90 MB
% 6.85/1.41 % (3482826)Instructions burned: 107 (million)
% 6.85/1.41 % (3482827)Instruction limit reached!
% 6.85/1.41 % (3482827)------------------------------
% 6.85/1.41 % (3482827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/1.41 % (3482827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.41 % (3482827)CaDiCaL version: 2.1.3
% 6.85/1.41 % (3482827)Termination reason: Instruction limit
% 6.85/1.41 % (3482827)Termination phase: Saturation
% 6.85/1.41 % (3482827)Time elapsed: 0.036 s
% 6.85/1.41 % (3482827)Peak memory usage: 90 MB
% 6.85/1.41 % (3482827)Instructions burned: 118 (million)
% 6.85/1.41 % (3482829)Instruction limit reached!
% 6.85/1.41 % (3482829)------------------------------
% 6.85/1.41 % (3482829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/1.41 % (3482829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.41 % (3482829)CaDiCaL version: 2.1.3
% 6.85/1.41 % (3482829)Termination reason: Instruction limit
% 6.85/1.41 % (3482829)Termination phase: Saturation
% 6.85/1.41 % (3482829)Time elapsed: 0.037 s
% 6.85/1.41 % (3482829)Peak memory usage: 90 MB
% 6.85/1.41 % (3482829)Instructions burned: 118 (million)
% 6.85/1.41 % (3482837)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=53308214:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 6.85/1.41 % (3482839)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=537150509:st=4:i=219:sd=3:ss=axioms_2998 on theBenchmark for (2998ds/219Mi)
% 6.85/1.41 % (3482838)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2669586969:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2998 on theBenchmark for (2998ds/189Mi)
% 6.85/1.41 % (3482828)------------------------------
% 6.85/1.41 % (3482828)------------------------------
% 6.85/1.41 % (3482838)Refutation not found, incomplete strategy
% 6.85/1.41 % (3482838)------------------------------
% 9.66/1.90 % (3482838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.66/1.90 % (3482838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.66/1.90 % (3482838)CaDiCaL version: 2.1.3
% 9.66/1.90 % (3482838)Termination reason: Refutation not found, incomplete strategy
% 9.66/1.90 % (3482838)Time elapsed: 0.023 s
% 9.66/1.90 % (3482838)Peak memory usage: 90 MB
% 9.66/1.90 % (3482838)Instructions burned: 75 (million)
% 9.66/1.90 % (3482837)Instruction limit reached!
% 9.66/1.90 % (3482837)------------------------------
% 9.66/1.90 % (3482837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.66/1.90 % (3482837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.66/1.90 % (3482837)CaDiCaL version: 2.1.3
% 9.66/1.90 % (3482837)Termination reason: Instruction limit
% 9.66/1.90 % (3482837)Termination phase: Saturation
% 9.66/1.90 % (3482837)Time elapsed: 0.045 s
% 9.66/1.90 % (3482837)Peak memory usage: 91 MB
% 9.66/1.90 % (3482837)Instructions burned: 146 (million)
% 9.66/1.90 % (3482839)Instruction limit reached!
% 9.66/1.90 % (3482839)------------------------------
% 9.66/1.90 % (3482839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.66/1.90 % (3482839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.66/1.90 % (3482839)CaDiCaL version: 2.1.3
% 9.66/1.90 % (3482839)Termination reason: Instruction limit
% 9.66/1.90 % (3482839)Termination phase: Saturation
% 9.66/1.90 % (3482839)Time elapsed: 0.062 s
% 9.66/1.90 % (3482839)Peak memory usage: 91 MB
% 9.66/1.90 % (3482839)Instructions burned: 221 (million)
% 9.66/1.90 % (3482844)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=4018749745:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 9.66/1.90 % (3482843)lrs+10_64_to=lpo:sil=8000:random_seed=2264833929:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 9.66/1.90 % (3482844)Refutation not found, incomplete strategy
% 9.66/1.90 % (3482844)------------------------------
% 9.66/1.90 % (3482844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.66/1.90 % (3482844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.66/1.90 % (3482844)CaDiCaL version: 2.1.3
% 9.66/1.90 % (3482844)Termination reason: Refutation not found, incomplete strategy
% 9.66/1.90 % (3482844)Time elapsed: 0.019 s
% 9.66/1.90 % (3482844)Peak memory usage: 89 MB
% 9.66/1.90 % (3482844)Instructions burned: 53 (million)
% 9.66/1.90 % (3482838)------------------------------
% 9.66/1.90 % (3482838)------------------------------
% 9.66/1.90 % (3482843)Instruction limit reached!
% 9.66/1.90 % (3482843)------------------------------
% 9.66/1.90 % (3482843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.66/1.90 % (3482843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.66/1.90 % (3482843)CaDiCaL version: 2.1.3
% 9.66/1.90 % (3482843)Termination reason: Instruction limit
% 9.66/1.90 % (3482843)Termination phase: Saturation
% 9.66/1.90 % (3482843)Time elapsed: 0.041 s
% 9.66/1.90 % (3482843)Peak memory usage: 91 MB
% 9.66/1.90 % (3482843)Instructions burned: 126 (million)
% 9.66/1.90 % (3482845)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=892295010:i=157:gtg=all_2996 on theBenchmark for (2996ds/157Mi)
% 9.66/1.90 % (3482824)Refutation not found, incomplete strategy
% 9.66/1.90 % (3482824)------------------------------
% 9.66/1.90 % (3482824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.66/1.90 % (3482824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.66/1.90 % (3482824)CaDiCaL version: 2.1.3
% 9.66/1.90 % (3482824)Termination reason: Refutation not found, incomplete strategy
% 9.66/1.90 % (3482824)Time elapsed: 0.383 s
% 9.66/1.90 % (3482824)Peak memory usage: 131 MB
% 9.66/1.90 % (3482824)Instructions burned: 1044 (million)
% 9.66/1.90 % (3482845)Instruction limit reached!
% 9.66/1.90 % (3482845)------------------------------
% 9.66/1.90 % (3482845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.66/1.90 % (3482845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.66/1.90 % (3482845)CaDiCaL version: 2.1.3
% 9.66/1.90 % (3482845)Termination reason: Instruction limit
% 9.66/1.90 % (3482845)Termination phase: Saturation
% 9.66/1.90 % (3482845)Time elapsed: 0.051 s
% 9.66/1.90 % (3482845)Peak memory usage: 92 MB
% 9.66/1.90 % (3482845)Instructions burned: 159 (million)
% 9.66/1.90 % (3482844)------------------------------
% 9.66/1.90 % (3482844)------------------------------
% 15.78/2.73 % (3482849)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3892176692:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 15.78/2.73 % (3482850)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3994238023:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 15.78/2.73 % (3482850)Refutation not found, incomplete strategy
% 15.78/2.73 % (3482850)------------------------------
% 15.78/2.73 % (3482850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.78/2.73 % (3482850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.78/2.73 % (3482850)CaDiCaL version: 2.1.3
% 15.78/2.73 % (3482850)Termination reason: Refutation not found, incomplete strategy
% 15.78/2.73 % (3482850)Time elapsed: 0.014 s
% 15.78/2.73 % (3482850)Peak memory usage: 90 MB
% 15.78/2.73 % (3482850)Instructions burned: 44 (million)
% 15.78/2.73 % (3482851)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3864781031:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 15.78/2.73 % (3482824)------------------------------
% 15.78/2.73 % (3482824)------------------------------
% 15.78/2.73 % (3482851)Instruction limit reached!
% 15.78/2.73 % (3482851)------------------------------
% 15.78/2.73 % (3482851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.78/2.73 % (3482851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.78/2.73 % (3482851)CaDiCaL version: 2.1.3
% 15.78/2.73 % (3482851)Termination reason: Instruction limit
% 15.78/2.73 % (3482851)Termination phase: Saturation
% 15.78/2.73 % (3482851)Time elapsed: 0.034 s
% 15.78/2.73 % (3482851)Peak memory usage: 91 MB
% 15.78/2.73 % (3482851)Instructions burned: 108 (million)
% 15.78/2.73 % (3482854)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3266332456:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 15.78/2.73 % (3482850)------------------------------
% 15.78/2.73 % (3482850)------------------------------
% 15.78/2.73 % (3482856)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2153091871:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 15.78/2.73 % (3482854)Refutation not found, incomplete strategy
% 15.78/2.73 % (3482854)------------------------------
% 15.78/2.73 % (3482854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.78/2.73 % (3482854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.78/2.73 % (3482854)CaDiCaL version: 2.1.3
% 15.78/2.73 % (3482854)Termination reason: Refutation not found, incomplete strategy
% 15.78/2.73 % (3482854)Time elapsed: 0.048 s
% 15.78/2.73 % (3482854)Peak memory usage: 89 MB
% 15.78/2.73 % (3482854)Instructions burned: 167 (million)
% 15.78/2.73 % (3482857)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4217472372:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi)
% 15.78/2.73 % (3482857)Refutation not found, incomplete strategy
% 15.78/2.73 % (3482857)------------------------------
% 15.78/2.73 % (3482857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.78/2.73 % (3482857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.78/2.73 % (3482857)CaDiCaL version: 2.1.3
% 15.78/2.73 % (3482857)Termination reason: Refutation not found, incomplete strategy
% 15.78/2.73 % (3482857)Time elapsed: 0.030 s
% 15.78/2.73 % (3482857)Peak memory usage: 91 MB
% 15.78/2.73 % (3482857)Instructions burned: 95 (million)
% 15.78/2.73 % (3482860)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=269030493:i=499:bd=all_2991 on theBenchmark for (2991ds/499Mi)
% 15.78/2.73 % (3482854)------------------------------
% 15.78/2.73 % (3482854)------------------------------
% 15.78/2.73 % (3482857)------------------------------
% 15.78/2.73 % (3482857)------------------------------
% 15.78/2.73 % (3482860)Instruction limit reached!
% 15.78/2.73 % (3482860)------------------------------
% 15.78/2.73 % (3482860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.78/2.73 % (3482860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.78/2.73 % (3482860)CaDiCaL version: 2.1.3
% 15.78/2.73 % (3482860)Termination reason: Instruction limit
% 22.03/3.67 % (3482860)Termination phase: Saturation
% 22.03/3.67 % (3482860)Time elapsed: 0.153 s
% 22.03/3.67 % (3482860)Peak memory usage: 95 MB
% 22.03/3.67 % (3482860)Instructions burned: 503 (million)
% 22.03/3.67 % (3482863)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2882629278:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi)
% 22.03/3.67 % (3482864)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2211645612:i=264:kws=precedence:fsr=off_2989 on theBenchmark for (2989ds/264Mi)
% 22.03/3.67 % (3482863)Instruction limit reached!
% 22.03/3.67 % (3482863)------------------------------
% 22.03/3.67 % (3482863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.03/3.67 % (3482863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.03/3.67 % (3482863)CaDiCaL version: 2.1.3
% 22.03/3.67 % (3482863)Termination reason: Instruction limit
% 22.03/3.67 % (3482863)Termination phase: Saturation
% 22.03/3.67 % (3482863)Time elapsed: 0.060 s
% 22.03/3.67 % (3482863)Peak memory usage: 93 MB
% 22.03/3.67 % (3482863)Instructions burned: 192 (million)
% 22.03/3.67 % (3482864)Instruction limit reached!
% 22.03/3.67 % (3482864)------------------------------
% 22.03/3.67 % (3482864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.03/3.67 % (3482864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.03/3.67 % (3482864)CaDiCaL version: 2.1.3
% 22.03/3.67 % (3482864)Termination reason: Instruction limit
% 22.03/3.67 % (3482864)Termination phase: Saturation
% 22.03/3.67 % (3482864)Time elapsed: 0.067 s
% 22.03/3.67 % (3482864)Peak memory usage: 91 MB
% 22.03/3.67 % (3482864)Instructions burned: 264 (million)
% 22.03/3.67 % (3482865)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3571893586:cond=on:i=156:bs=on:gtg=exists_all:er=known_2989 on theBenchmark for (2989ds/156Mi)
% 22.03/3.67 % (3482865)Instruction limit reached!
% 22.03/3.67 % (3482865)------------------------------
% 22.03/3.67 % (3482865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.03/3.67 % (3482865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.03/3.67 % (3482865)CaDiCaL version: 2.1.3
% 22.03/3.67 % (3482865)Termination reason: Instruction limit
% 22.03/3.67 % (3482865)Termination phase: Saturation
% 22.03/3.67 % (3482865)Time elapsed: 0.050 s
% 22.03/3.67 % (3482865)Peak memory usage: 92 MB
% 22.03/3.67 % (3482865)Instructions burned: 156 (million)
% 22.03/3.67 % (3482868)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3497638151:i=3256:kws=precedence:bd=preordered:av=off_2988 on theBenchmark for (2988ds/3256Mi)
% 22.03/3.67 % (3482869)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3657488292:i=537:av=off:ss=included_2987 on theBenchmark for (2987ds/537Mi)
% 22.03/3.67 % (3482871)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2510021314:i=180:bd=preordered:av=off_2987 on theBenchmark for (2987ds/180Mi)
% 22.03/3.67 % (3482871)Instruction limit reached!
% 22.03/3.67 % (3482871)------------------------------
% 22.03/3.67 % (3482871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.03/3.67 % (3482871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.03/3.67 % (3482871)CaDiCaL version: 2.1.3
% 22.03/3.67 % (3482871)Termination reason: Instruction limit
% 22.03/3.67 % (3482871)Termination phase: Saturation
% 22.03/3.67 % (3482871)Time elapsed: 0.049 s
% 22.03/3.67 % (3482871)Peak memory usage: 89 MB
% 22.03/3.67 % (3482871)Instructions burned: 181 (million)
% 22.03/3.67 % (3482869)Instruction limit reached!
% 22.03/3.67 % (3482869)------------------------------
% 22.03/3.67 % (3482869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.03/3.67 % (3482869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.03/3.67 % (3482869)CaDiCaL version: 2.1.3
% 22.03/3.67 % (3482869)Termination reason: Instruction limit
% 22.03/3.67 % (3482869)Termination phase: Saturation
% 22.03/3.67 % (3482869)Time elapsed: 0.131 s
% 22.03/3.67 % (3482869)Peak memory usage: 90 MB
% 22.03/3.67 % (3482869)Instructions burned: 542 (million)
% 22.03/3.67 % (3482875)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=1968564982:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2985 on theBenchmark for (2985ds/10307Mi)
% 22.03/3.67 % (3482876)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=4017937888:i=412:gtgl=4:gtg=exists_all_2985 on theBenchmark for (2985ds/412Mi)
% 29.79/4.73 % (3482876)Instruction limit reached!
% 29.79/4.73 % (3482876)------------------------------
% 29.79/4.73 % (3482876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/4.73 % (3482876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/4.73 % (3482876)CaDiCaL version: 2.1.3
% 29.79/4.73 % (3482876)Termination reason: Instruction limit
% 29.79/4.73 % (3482876)Termination phase: Saturation
% 29.79/4.73 % (3482876)Time elapsed: 0.108 s
% 29.79/4.73 % (3482876)Peak memory usage: 93 MB
% 29.79/4.73 % (3482876)Instructions burned: 413 (million)
% 29.79/4.73 % (3482849)Instruction limit reached!
% 29.79/4.73 % (3482849)------------------------------
% 29.79/4.73 % (3482849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/4.73 % (3482849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/4.73 % (3482849)CaDiCaL version: 2.1.3
% 29.79/4.73 % (3482849)Termination reason: Instruction limit
% 29.79/4.73 % (3482849)Termination phase: Saturation
% 29.79/4.73 % (3482849)Time elapsed: 1.119 s
% 29.79/4.73 % (3482849)Peak memory usage: 151 MB
% 29.79/4.73 % (3482849)Instructions burned: 3396 (million)
% 29.79/4.73 % (3482879)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=3837274573:s2pl=no:i=8478:s2at=4:nm=6_2983 on theBenchmark for (2983ds/8478Mi)
% 29.79/4.73 % (3482880)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=2014022108:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2982 on theBenchmark for (2982ds/303Mi)
% 29.79/4.73 % (3482880)Refutation not found, incomplete strategy
% 29.79/4.73 % (3482880)------------------------------
% 29.79/4.73 % (3482880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/4.73 % (3482880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/4.73 % (3482880)CaDiCaL version: 2.1.3
% 29.79/4.73 % (3482880)Termination reason: Refutation not found, incomplete strategy
% 29.79/4.73 % (3482880)Time elapsed: 0.046 s
% 29.79/4.73 % (3482880)Peak memory usage: 92 MB
% 29.79/4.73 % (3482880)Instructions burned: 132 (million)
% 29.79/4.73 % (3482880)------------------------------
% 29.79/4.73 % (3482880)------------------------------
% 29.79/4.73 % (3482883)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=246806911:st=4:i=720:sd=3:fsr=off:ss=axioms_2979 on theBenchmark for (2979ds/720Mi)
% 29.79/4.73 % (3482879)Refutation not found, incomplete strategy
% 29.79/4.73 % (3482879)------------------------------
% 29.79/4.73 % (3482879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/4.73 % (3482879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/4.73 % (3482879)CaDiCaL version: 2.1.3
% 29.79/4.73 % (3482879)Termination reason: Refutation not found, incomplete strategy
% 29.79/4.73 % (3482879)Time elapsed: 0.399 s
% 29.79/4.73 % (3482879)Peak memory usage: 133 MB
% 29.79/4.73 % (3482879)Instructions burned: 1087 (million)
% 29.79/4.73 % (3482883)Refutation not found, incomplete strategy
% 29.79/4.73 % (3482883)------------------------------
% 29.79/4.73 % (3482883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/4.73 % (3482883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/4.73 % (3482883)CaDiCaL version: 2.1.3
% 29.79/4.73 % (3482883)Termination reason: Refutation not found, incomplete strategy
% 29.79/4.73 % (3482883)Time elapsed: 0.114 s
% 29.79/4.73 % (3482883)Peak memory usage: 95 MB
% 29.79/4.73 % (3482883)Instructions burned: 364 (million)
% 29.79/4.73 % (3482879)------------------------------
% 29.79/4.73 % (3482879)------------------------------
% 29.79/4.73 % (3482868)Instruction limit reached!
% 29.79/4.73 % (3482868)------------------------------
% 29.79/4.73 % (3482868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/4.73 % (3482868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/4.73 % (3482868)CaDiCaL version: 2.1.3
% 29.79/4.73 % (3482868)Termination reason: Instruction limit
% 29.79/4.73 % (3482868)Termination phase: Saturation
% 29.79/4.73 % (3482868)Time elapsed: 1.104 s
% 29.79/4.73 % (3482868)Peak memory usage: 149 MB
% 29.79/4.73 % (3482868)Instructions burned: 3257 (million)
% 29.79/4.78 % (3482856)Instruction limit reached!
% 29.79/4.78 % (3482856)------------------------------
% 29.79/4.78 % (3482856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/4.78 % (3482856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/4.78 % (3482856)CaDiCaL version: 2.1.3
% 29.79/4.78 % (3482856)Termination reason: Instruction limit
% 29.79/4.78 % (3482856)Termination phase: Saturation
% 29.79/4.78 % (3482856)Time elapsed: 1.610 s
% 29.79/4.78 % (3482856)Peak memory usage: 157 MB
% 29.79/4.78 % (3482856)Instructions burned: 5209 (million)
% 29.79/4.78 % (3482883)------------------------------
% 29.79/4.78 % (3482883)------------------------------
% 29.79/4.78 % (3482885)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2028429333:i=598:bs=on:bd=preordered:av=off:ss=axioms_2976 on theBenchmark for (2976ds/598Mi)
% 29.79/4.78 % (3482886)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2809666371:i=2989:sd=3:ss=axioms:sgt=60_2975 on theBenchmark for (2975ds/2989Mi)
% 29.79/4.78 % (3482887)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=2694684613:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2975 on theBenchmark for (2975ds/1997Mi)
% 29.79/4.78 % (3482888)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=1405130551:i=2088:bd=preordered:av=off_2975 on theBenchmark for (2975ds/2088Mi)
% 29.79/4.78 % (3482885)Instruction limit reached!
% 29.79/4.78 % (3482885)------------------------------
% 29.79/4.78 % (3482885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/4.78 % (3482885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/4.78 % (3482885)CaDiCaL version: 2.1.3
% 29.79/4.78 % (3482885)Termination reason: Instruction limit
% 29.79/4.78 % (3482885)Termination phase: Saturation
% 29.79/4.78 % (3482885)Time elapsed: 0.167 s
% 29.79/4.78 % (3482885)Peak memory usage: 92 MB
% 29.79/4.78 % (3482885)Instructions burned: 598 (million)
% 29.79/4.78 % (3482893)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3685894335:i=1098:nicw=on_2973 on theBenchmark for (2973ds/1098Mi)
% 29.79/4.78 % (3482893)Instruction limit reached!
% 29.79/4.78 % (3482893)------------------------------
% 29.79/4.78 % (3482893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/4.78 % (3482893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/4.78 % (3482893)CaDiCaL version: 2.1.3
% 29.79/4.78 % (3482893)Termination reason: Instruction limit
% 29.79/4.78 % (3482893)Termination phase: Saturation
% 29.79/4.78 % (3482893)Time elapsed: 0.275 s
% 29.79/4.78 % (3482893)Peak memory usage: 95 MB
% 29.79/4.78 % (3482893)Instructions burned: 1102 (million)
% 29.79/4.78 % (3482887)Refutation not found, incomplete strategy
% 29.79/4.78 % (3482887)------------------------------
% 29.79/4.78 % (3482887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/4.78 % (3482887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/4.78 % (3482887)CaDiCaL version: 2.1.3
% 29.79/4.78 % (3482887)Termination reason: Refutation not found, incomplete strategy
% 29.79/4.78 % (3482887)Time elapsed: 0.564 s
% 29.79/4.78 % (3482887)Peak memory usage: 135 MB
% 29.79/4.78 % (3482887)Instructions burned: 1594 (million)
% 29.79/4.78 % (3482895)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1207180903:i=433:bd=preordered_2969 on theBenchmark for (2969ds/433Mi)
% 29.79/4.78 % (3482895)Refutation not found, incomplete strategy
% 29.79/4.78 % (3482895)------------------------------
% 29.79/4.78 % (3482895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/4.78 % (3482895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/4.78 % (3482895)CaDiCaL version: 2.1.3
% 29.79/4.78 % (3482895)Termination reason: Refutation not found, incomplete strategy
% 29.79/4.78 % (3482895)Time elapsed: 0.045 s
% 29.79/4.78 % (3482895)Peak memory usage: 92 MB
% 29.79/4.78 % (3482895)Instructions burned: 135 (million)
% 29.79/4.78 % (3482887)------------------------------
% 29.79/4.78 % (3482887)------------------------------
% 29.79/4.78 % (3482888)Instruction limit reached!
% 29.79/4.78 % (3482888)------------------------------
% 29.79/4.78 % (3482888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/4.78 % (3482888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/4.78 % (3482888)CaDiCaL version: 2.1.3
% 29.79/4.78 % (3482888)Termination reason: Instruction limit
% 29.79/4.78 % (3482888)Termination phase: Saturation
% 29.79/4.78 % (3482888)Time elapsed: 0.732 s
% 29.79/4.78 % (3482888)Peak memory usage: 139 MB
% 29.79/4.78 % (3482888)Instructions burned: 2090 (million)
% 29.79/4.78 % (3482895)------------------------------
% 29.79/4.78 % (3482895)------------------------------
% 29.79/4.78 % (3482897)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=4132988417:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2967 on theBenchmark for (2967ds/2942Mi)
% 29.79/4.78 % (3482898)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2239370046:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2966 on theBenchmark for (2966ds/6922Mi)
% 29.79/4.78 % (3482899)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=2549579002:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2965 on theBenchmark for (2965ds/596Mi)
% 29.79/4.78 % (3482899)Refutation not found, incomplete strategy
% 29.79/4.78 % (3482899)------------------------------
% 29.79/4.78 % (3482899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/4.78 % (3482899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/4.78 % (3482899)CaDiCaL version: 2.1.3
% 29.79/4.78 % (3482899)Termination reason: Refutation not found, incomplete strategy
% 29.79/4.78 % (3482899)Time elapsed: 0.015 s
% 29.79/4.78 % (3482899)Peak memory usage: 90 MB
% 29.79/4.78 % (3482899)Instructions burned: 43 (million)
% 29.79/4.78 % (3482886)Instruction limit reached!
% 29.79/4.78 % (3482886)------------------------------
% 29.79/4.78 % (3482886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/4.78 % (3482886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/4.78 % (3482886)CaDiCaL version: 2.1.3
% 29.79/4.78 % (3482886)Termination reason: Instruction limit
% 29.79/4.78 % (3482886)Termination phase: Saturation
% 29.79/4.78 % (3482886)Time elapsed: 1.079 s
% 29.79/4.78 % (3482886)Peak memory usage: 149 MB
% 29.79/4.78 % (3482886)Instructions burned: 2989 (million)
% 29.79/4.78 % (3482899)------------------------------
% 29.79/4.78 % (3482899)------------------------------
% 29.79/4.78 % (3482903)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=2310479813:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2963 on theBenchmark for (2963ds/4123Mi)
% 29.79/4.78 % (3482904)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2386569874:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2963 on theBenchmark for (2963ds/16411Mi)
% 29.79/4.78 % (3482898)Refutation not found, incomplete strategy
% 29.79/4.78 % (3482898)------------------------------
% 29.79/4.78 % (3482898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/4.78 % (3482898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/4.78 % (3482898)CaDiCaL version: 2.1.3
% 29.79/4.78 % (3482898)Termination reason: Refutation not found, incomplete strategy
% 29.79/4.78 % (3482898)Time elapsed: 0.392 s
% 29.79/4.78 % (3482898)Peak memory usage: 132 MB
% 29.79/4.78 % (3482898)Instructions burned: 1080 (million)
% 29.79/4.78 % (3482898)------------------------------
% 29.79/4.78 % (3482898)------------------------------
% 29.79/4.78 % (3482907)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1578704570:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2959 on theBenchmark for (2959ds/1670Mi)
% 29.79/4.78 % (3482904)First to succeed.
% 29.79/4.78 % (3482904)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3482818"
% 29.79/4.78 % (3482897)Instruction limit reached!
% 29.79/4.78 % (3482897)------------------------------
% 29.79/4.78 % (3482897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/4.78 % (3482897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/4.78 % (3482897)CaDiCaL version: 2.1.3
% 29.79/4.78 % (3482897)Termination reason: Instruction limit
% 29.79/4.78 % (3482897)Termination phase: Saturation
% 29.79/4.78 % (3482897)Time elapsed: 0.987 s
% 29.79/4.78 % (3482897)Peak memory usage: 144 MB
% 29.79/4.78 % (3482897)Instructions burned: 2944 (million)
% 29.79/4.78 % SZS status Satisfiable for theBenchmark
% 29.79/4.78 % SZS output start Saturation.
% See solution above
% 31.41/4.88 % SZS output start Definitions and Model Updates.
% 31.41/4.88 for all inputs,
% 31.41/4.88 define c6_0 := $true
% 31.41/4.88 for all inputs,
% 31.41/4.88 define c8_0 := $false
% 31.41/4.88 % SZS output end Definitions and Model Updates.
% 31.41/4.88 % (3482904)------------------------------
% 31.41/4.88 % (3482904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.41/4.88 % (3482904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.41/4.88 % (3482904)CaDiCaL version: 2.1.3
% 31.41/4.88 % (3482904)Termination reason: Satisfiable
% 31.41/4.88 % (3482904)Time elapsed: 0.468 s
% 31.41/4.88 % (3482904)Peak memory usage: 134 MB
% 31.41/4.88 % (3482904)Instructions burned: 1261 (million)
% 31.41/4.88 % (3482904)------------------------------
% 31.41/4.88 % (3482904)------------------------------
% 31.41/4.88 % (3482818)Success in time 4.461 s
% 31.41/4.88 % Vampire exiting
%------------------------------------------------------------------------------