%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : HWV079+1 : TPTP v9.3.1. Bugfixed v5.5.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:38:43 AM UTC 2026
% Result : Satisfiable 63.64s 11.24s
% Output : Saturation 74.48s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u684,axiom,
~ p(sK45) ).
cnf(u689,axiom,
p(sK40) ).
cnf(u693,axiom,
p(sK46) ).
cnf(u697,axiom,
p(sK39) ).
cnf(u701,axiom,
p(sK38) ).
cnf(u705,axiom,
p(sK44) ).
cnf(u710,axiom,
~ p(sK35) ).
cnf(u713,axiom,
~ p(sK36) ).
cnf(u717,axiom,
p(sK37) ).
cnf(u722,axiom,
~ p(sK33) ).
cnf(u730,axiom,
p(sK32) ).
cnf(u733,axiom,
~ p(sK34) ).
cnf(u738,axiom,
~ p(sK41) ).
cnf(u746,axiom,
~ p(sK43) ).
cnf(u750,axiom,
~ p(sK42) ).
cnf(u755,axiom,
~ p(sK53) ).
cnf(u758,axiom,
p(sK54) ).
cnf(u763,axiom,
~ p(sK55) ).
cnf(u772,axiom,
p(sK50) ).
cnf(u780,axiom,
~ p(sK52) ).
cnf(u784,axiom,
p(sK51) ).
cnf(u788,axiom,
~ p(sK12) ).
cnf(u792,axiom,
( ~ p(sK64(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK58(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK57(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK56(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK59(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u801,axiom,
~ p(sK47) ).
cnf(u804,axiom,
p(sK49) ).
cnf(u808,axiom,
p(sK48) ).
cnf(u815,axiom,
p(sK2) ).
cnf(u819,axiom,
( ~ p(sK57(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK64(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK59(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK58(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK56(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u841,axiom,
( p(sK60(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X56) ) ).
cnf(u847,axiom,
p(sK23) ).
cnf(u851,axiom,
( ~ p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK60(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK61(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u855,axiom,
p(sK31) ).
cnf(u859,axiom,
( ~ p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK60(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK61(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u876,axiom,
( p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X57) ) ).
cnf(u882,axiom,
~ p(sK18) ).
cnf(u902,axiom,
~ p(sK3) ).
cnf(u930,axiom,
( ~ p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X60) ) ).
cnf(u945,axiom,
( p(sK56(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X58) ) ).
cnf(u972,axiom,
p(sK21) ).
cnf(u1009,axiom,
~ p(sK25) ).
cnf(u1020,axiom,
~ p(sK22) ).
cnf(u1038,axiom,
~ p(sK5) ).
cnf(u1046,axiom,
p(sK14) ).
cnf(u1053,axiom,
~ p(sK10) ).
cnf(u1057,axiom,
( ~ p(sK64(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK56(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK59(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK57(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK58(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1089,axiom,
( ~ p(sK57(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X59) ) ).
cnf(u1128,axiom,
( p(sK57(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X59) ) ).
cnf(u1152,axiom,
~ p(sK19) ).
cnf(u1170,axiom,
p(sK13) ).
cnf(u1174,axiom,
( ~ p(sK59(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK56(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK57(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK58(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK64(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1182,axiom,
( p(sK59(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X61) ) ).
cnf(u1193,axiom,
~ p(sK9) ).
cnf(u1200,axiom,
( ~ p(sK64(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK57(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK59(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK56(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK58(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1209,axiom,
~ p(sK0) ).
cnf(u1216,axiom,
~ p(sK20) ).
cnf(u1220,axiom,
( ~ p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK60(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK61(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK63(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1224,axiom,
( p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK60(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK61(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1233,axiom,
p(sK26) ).
cnf(u1237,axiom,
( ~ p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK61(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK60(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1241,axiom,
( ~ p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK61(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK60(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1256,axiom,
~ p(sK17) ).
cnf(u1275,axiom,
( ~ p(sK58(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X62) ) ).
cnf(u1302,axiom,
~ p(sK6) ).
cnf(u1316,axiom,
p(sK27) ).
cnf(u1327,axiom,
( ~ p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK61(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK60(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK62(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1341,axiom,
~ p(sK28) ).
cnf(u1368,axiom,
p(sK11) ).
cnf(u1372,axiom,
( ~ p(sK59(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK64(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK57(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK58(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK56(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1376,axiom,
( ~ p(sK61(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X63) ) ).
cnf(u1400,axiom,
p(sK8) ).
cnf(u1404,axiom,
( ~ p(sK59(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK56(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK64(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK58(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK57(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1408,axiom,
( p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK60(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK61(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1415,axiom,
~ p(sK16) ).
cnf(u1423,axiom,
p(sK29) ).
cnf(u1427,axiom,
( p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK61(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK60(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK62(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1441,axiom,
~ p(sK15) ).
cnf(u1454,axiom,
( ~ p(sK60(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X56) ) ).
cnf(u1458,axiom,
( ~ p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK61(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK60(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1464,axiom,
( p(sK60(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK61(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1477,axiom,
p(sK7) ).
cnf(u1481,axiom,
( ~ p(sK58(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK64(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK56(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK57(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK59(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1511,axiom,
( ~ p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X57) ) ).
cnf(u1541,axiom,
( ~ p(sK59(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK64(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK56(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK58(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK57(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1556,axiom,
( ~ p(sK60(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK61(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK62(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1561,axiom,
( ~ p(sK64(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK56(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK57(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK58(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK59(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1569,axiom,
( p(sK61(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X63) ) ).
cnf(u1582,axiom,
( p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK61(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK60(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1599,axiom,
~ p(sK24) ).
cnf(u1608,axiom,
( ~ p(sK56(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X58) ) ).
cnf(u1617,axiom,
( ~ p(sK61(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK60(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK65(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1636,axiom,
( ~ p(sK59(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X61) ) ).
cnf(u1651,axiom,
( p(sK60(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK61(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK65(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1660,axiom,
( ~ p(sK64(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK56(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK59(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK57(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK58(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1680,axiom,
( ~ p(sK64(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK57(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK56(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK58(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK59(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1702,axiom,
p(sK30) ).
cnf(u1713,axiom,
( ~ p(sK64(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK57(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK58(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK56(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK59(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1722,axiom,
( ~ p(sK64(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK59(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK57(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK58(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK56(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1734,axiom,
p(sK4) ).
cnf(u1738,axiom,
( ~ p(sK58(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK56(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK59(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK57(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK64(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1782,axiom,
( p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X60) ) ).
cnf(u1797,axiom,
( ~ p(sK56(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK57(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK59(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK64(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK58(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u1800,axiom,
p(sK1) ).
cnf(u1838,axiom,
( p(sK58(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X62) ) ).
cnf(u1847,axiom,
( ~ p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK61(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK60(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK63(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u14234,axiom,
( p(sK65(X7,X2,X6,X0,X1,X5,X4,X3))
| p(X1)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| p(X5)
| p(X6)
| p(X0) ) ).
cnf(u13834,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X58)
| ~ p(X60)
| ~ p(X59)
| p(X61)
| ~ p(X62) ) ).
cnf(u17875,axiom,
( p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X58)
| ~ p(X59)
| p(X62)
| p(X56)
| ~ p(X61)
| ~ p(X63)
| ~ p(X57) ) ).
cnf(u7468,axiom,
( p(sK65(X6,X1,X0,X2,X7,X3,X4,X5))
| ~ p(X1)
| ~ p(X2)
| p(X3)
| p(X4)
| ~ p(X5)
| p(X0) ) ).
cnf(u46538,axiom,
( p(sK62(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X3)
| ~ p(X2)
| p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK60(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X7) ) ).
cnf(u2066,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X61)
| p(X59)
| ~ p(X56)
| p(X58)
| ~ p(X63)
| ~ p(X62) ) ).
cnf(u2203,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X58)
| ~ p(X59)
| ~ p(X57)
| ~ p(X61)
| p(X62)
| ~ p(X63)
| p(X56) ) ).
cnf(u50552,axiom,
( p(sK65(X2,X3,X4,X1,X5,X6,X0,X7))
| ~ p(X1)
| p(sK56(X2,X3,X4,X1,X5,X6,X0,X7))
| ~ p(X3)
| ~ p(X6)
| ~ p(X0)
| ~ p(X7) ) ).
cnf(u24619,axiom,
( p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| p(X5)
| ~ p(X3)
| ~ p(X2)
| ~ p(X0)
| ~ p(X6) ) ).
cnf(u43858,axiom,
( p(sK65(X6,X1,X2,X3,X7,X4,X5,X0))
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| p(X5)
| ~ p(X0) ) ).
cnf(u28578,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X57)
| ~ p(X61)
| ~ p(X62)
| p(X56)
| p(X60) ) ).
cnf(u13576,axiom,
( p(sK64(X1,X6,X0,X3,X5,X4,X2,X7))
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| ~ p(X5)
| p(X0) ) ).
cnf(u49238,axiom,
( p(sK56(X1,X2,X3,X4,X0,X5,X6,X7))
| ~ p(X0)
| ~ p(X1)
| p(sK66(X1,X2,X3,X4,X0,X5,X6,X7))
| ~ p(X5)
| p(X6)
| p(X4) ) ).
cnf(u51081,axiom,
( p(sK59(X1,X2,X3,X4,X5,X6,X0,X7))
| ~ p(X0)
| ~ p(X2)
| p(sK57(X1,X2,X3,X4,X5,X6,X0,X7))
| p(sK56(X1,X2,X3,X4,X5,X6,X0,X7))
| ~ p(X7)
| p(sK66(X1,X2,X3,X4,X5,X6,X0,X7)) ) ).
cnf(u16411,axiom,
( p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X59)
| ~ p(X63)
| ~ p(X57)
| ~ p(X62)
| p(X58)
| p(X61)
| p(X56) ) ).
cnf(u49492,axiom,
( ~ p(sK61(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK65(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| ~ p(X4) ) ).
cnf(u50390,axiom,
( p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X2)
| ~ p(X4)
| ~ p(X7)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(X5)
| p(X6) ) ).
cnf(u28556,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X60)
| ~ p(X61)
| p(X62)
| p(X57)
| ~ p(X59)
| p(X58) ) ).
cnf(u28472,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X57)
| ~ p(X59)
| p(X63)
| p(X60)
| p(X61) ) ).
cnf(u47870,axiom,
( p(sK59(X1,X2,X3,X4,X0,X5,X6,X7))
| ~ p(X1)
| p(sK66(X1,X2,X3,X4,X0,X5,X6,X7))
| ~ p(X2)
| ~ p(X0)
| p(sK58(X1,X2,X3,X4,X0,X5,X6,X7))
| p(sK56(X1,X2,X3,X4,X0,X5,X6,X7))
| ~ p(X4) ) ).
cnf(u45424,axiom,
( ~ p(sK64(X2,X3,X4,X5,X0,X6,X7,X1))
| ~ p(X1)
| ~ p(X2)
| p(sK66(X2,X3,X4,X5,X0,X6,X7,X1))
| ~ p(X0) ) ).
cnf(u47839,axiom,
( ~ p(sK60(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK65(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| ~ p(X4) ) ).
cnf(u46561,axiom,
( p(sK62(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK60(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X7) ) ).
cnf(u46078,axiom,
( p(sK64(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X6)
| ~ p(X2) ) ).
cnf(u48519,axiom,
( p(sK64(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X6)
| ~ p(X3)
| ~ p(X2) ) ).
cnf(u27419,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X63)
| p(X62)
| p(X59)
| p(X60)
| ~ p(X57) ) ).
cnf(u50975,axiom,
( ~ p(sK61(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X3)
| ~ p(X1)
| p(sK65(X0,X1,X2,X3,X4,X5,X6,X7)) ) ).
cnf(u32716,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X58)
| p(X62)
| p(X61)
| ~ p(X63)
| p(X59)
| ~ p(X60) ) ).
cnf(u15949,axiom,
( p(sK64(X5,X4,X0,X1,X7,X6,X3,X2))
| p(X1)
| ~ p(X2)
| p(X3)
| ~ p(X4)
| p(X5)
| ~ p(X6)
| p(X0) ) ).
cnf(u49140,axiom,
( p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| ~ p(X0)
| ~ p(X5)
| ~ p(X3)
| ~ p(X2) ) ).
cnf(u43555,axiom,
( p(sK65(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| ~ p(X1)
| ~ p(X7)
| ~ p(X0) ) ).
cnf(u49133,axiom,
( p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| ~ p(X0)
| p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X3) ) ).
cnf(u49640,axiom,
( p(sK58(X1,X2,X3,X4,X5,X6,X7,X0))
| p(sK66(X1,X2,X3,X4,X5,X6,X7,X0))
| ~ p(X2)
| ~ p(X5)
| ~ p(X0)
| p(sK56(X1,X2,X3,X4,X5,X6,X7,X0))
| ~ p(X4)
| p(X6) ) ).
cnf(u45943,axiom,
( p(sK59(X1,X2,X3,X4,X5,X6,X7,X0))
| ~ p(X1)
| p(sK66(X1,X2,X3,X4,X5,X6,X7,X0))
| ~ p(X2)
| ~ p(X0)
| p(sK58(X1,X2,X3,X4,X5,X6,X7,X0))
| p(sK56(X1,X2,X3,X4,X5,X6,X7,X0))
| ~ p(X4) ) ).
cnf(u49534,axiom,
( p(sK58(X2,X3,X4,X5,X0,X6,X7,X1))
| ~ p(X1)
| p(sK66(X2,X3,X4,X5,X0,X6,X7,X1))
| ~ p(X3)
| p(sK56(X2,X3,X4,X5,X0,X6,X7,X1))
| ~ p(X0)
| p(sK57(X2,X3,X4,X5,X0,X6,X7,X1))
| ~ p(X6) ) ).
cnf(u28660,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X62)
| ~ p(X63)
| p(X58)
| p(X59)
| p(X57)
| p(X60) ) ).
cnf(u50522,axiom,
( p(sK65(X2,X3,X1,X0,X4,X5,X6,X7))
| ~ p(X1)
| p(sK59(X2,X3,X1,X0,X4,X5,X6,X7))
| ~ p(X3)
| ~ p(X6)
| ~ p(X0)
| ~ p(X7) ) ).
cnf(u33145,axiom,
( ~ p(sK62(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK65(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(sK60(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(sK61(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1) ) ).
cnf(u45564,axiom,
( p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| ~ p(X7)
| ~ p(X0)
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X3)
| p(X5) ) ).
cnf(u49648,axiom,
( p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| ~ p(X4)
| ~ p(X7)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X3)
| p(X5)
| p(X6) ) ).
cnf(u13020,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X57)
| ~ p(X58)
| ~ p(X62)
| p(X63)
| p(X61)
| p(X59) ) ).
cnf(u29027,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X61)
| ~ p(X59)
| ~ p(X56)
| p(X58)
| p(X57)
| p(X62) ) ).
cnf(u50314,axiom,
( p(sK62(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X2)
| p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK60(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X7) ) ).
cnf(u24567,axiom,
( p(sK65(X6,X2,X4,X1,X0,X5,X7,X3))
| p(X1)
| p(X4)
| ~ p(X5)
| ~ p(X6)
| p(X7)
| ~ p(X0) ) ).
cnf(u44348,axiom,
( p(sK65(X6,X1,X5,X2,X7,X4,X3,X0))
| ~ p(X1)
| p(X2)
| ~ p(X3)
| ~ p(X4)
| ~ p(X5)
| ~ p(X0) ) ).
cnf(u13547,axiom,
( p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X58)
| ~ p(X56)
| ~ p(X62)
| ~ p(X59)
| ~ p(X61)
| ~ p(X60) ) ).
cnf(u49096,axiom,
( ~ p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK60(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u51046,axiom,
( p(sK56(X2,X0,X3,X4,X5,X1,X6,X7))
| ~ p(X1)
| ~ p(X0)
| ~ p(X7)
| p(sK66(X2,X0,X3,X4,X5,X1,X6,X7))
| p(X6)
| p(X4) ) ).
cnf(u24571,axiom,
( p(sK65(X6,X7,X5,X4,X3,X0,X1,X2))
| p(X1)
| ~ p(X3)
| p(X4)
| ~ p(X5)
| ~ p(X6)
| p(X0) ) ).
cnf(u19585,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X58)
| ~ p(X60)
| p(X63)
| p(X56)
| ~ p(X62)
| ~ p(X59) ) ).
cnf(u49263,axiom,
( ~ p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK61(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u50976,axiom,
( p(sK65(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X3)
| ~ p(X1)
| p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X7) ) ).
cnf(u49231,axiom,
( p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| p(X6) ) ).
cnf(u16811,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X58)
| p(X60)
| ~ p(X62)
| p(X57)
| ~ p(X61)
| ~ p(X63) ) ).
cnf(u23990,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X58)
| p(X62)
| ~ p(X61)
| p(X60)
| p(X59) ) ).
cnf(u13945,axiom,
( p(sK65(X7,X2,X4,X1,X0,X5,X6,X3))
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| p(X4)
| ~ p(X5)
| ~ p(X6)
| p(X0) ) ).
cnf(u23554,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X57)
| ~ p(X62)
| p(X63)
| p(X58)
| p(X56) ) ).
cnf(u49532,axiom,
( p(sK57(X2,X3,X4,X5,X0,X6,X7,X1))
| ~ p(X1)
| p(sK66(X2,X3,X4,X5,X0,X6,X7,X1))
| ~ p(X3)
| ~ p(X0)
| ~ p(X6)
| ~ p(X7)
| ~ p(X4) ) ).
cnf(u47838,axiom,
( ~ p(sK62(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(sK60(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK65(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1) ) ).
cnf(u45914,axiom,
( ~ p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK60(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK61(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u32241,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X60)
| ~ p(X58)
| ~ p(X61)
| p(X59)
| p(X63)
| ~ p(X56) ) ).
cnf(u19377,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X58)
| ~ p(X59)
| ~ p(X62)
| ~ p(X63)
| ~ p(X57)
| ~ p(X61) ) ).
cnf(u49533,axiom,
( p(sK58(X2,X3,X4,X5,X0,X6,X7,X1))
| ~ p(X1)
| p(sK66(X2,X3,X4,X5,X0,X6,X7,X1))
| ~ p(X3)
| ~ p(X0)
| ~ p(X6)
| ~ p(X5)
| ~ p(X4) ) ).
cnf(u29616,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X61)
| p(X63)
| ~ p(X59)
| ~ p(X56)
| p(X60)
| p(X58) ) ).
cnf(u22285,axiom,
( p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X59)
| ~ p(X63)
| ~ p(X57)
| p(X60)
| p(X62)
| p(X58)
| ~ p(X61) ) ).
cnf(u14497,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X63)
| p(X57)
| ~ p(X61)
| p(X56)
| p(X60)
| p(X59) ) ).
cnf(u24617,axiom,
( p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| p(X3)
| p(X2)
| ~ p(X5)
| ~ p(X0)
| p(X6)
| ~ p(X4) ) ).
cnf(u20906,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X60)
| ~ p(X56)
| p(X59)
| p(X62)
| p(X63)
| p(X58) ) ).
cnf(u16718,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X56)
| p(X57)
| ~ p(X63)
| p(X62)
| p(X60)
| ~ p(X59) ) ).
cnf(u13206,axiom,
( p(sK65(X1,X5,X6,X4,X7,X3,X0,X2))
| p(X1)
| ~ p(X2)
| p(X3)
| p(X4)
| ~ p(X5)
| ~ p(X6)
| p(X0) ) ).
cnf(u50467,axiom,
( p(sK57(X1,X2,X0,X3,X4,X5,X6,X7))
| ~ p(X0)
| ~ p(X2)
| ~ p(X5)
| ~ p(X6)
| ~ p(X7)
| p(sK66(X1,X2,X0,X3,X4,X5,X6,X7)) ) ).
cnf(u46086,axiom,
( p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X6)
| ~ p(X2)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1) ) ).
cnf(u47984,axiom,
( p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| ~ p(X0)
| ~ p(X5)
| p(X6) ) ).
cnf(u18734,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X57)
| ~ p(X61)
| ~ p(X62)
| p(X58)
| p(X59)
| p(X63) ) ).
cnf(u27308,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X62)
| p(X63)
| ~ p(X59)
| p(X61)
| p(X56) ) ).
cnf(u15440,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X62)
| p(X59)
| ~ p(X58)
| p(X61)
| ~ p(X60)
| p(X63) ) ).
cnf(u50458,axiom,
( p(sK65(X2,X3,X1,X4,X5,X6,X0,X7))
| ~ p(X1)
| p(sK57(X2,X3,X1,X4,X5,X6,X0,X7))
| ~ p(X3)
| ~ p(X6)
| ~ p(X0)
| ~ p(X7) ) ).
cnf(u31864,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X62)
| p(X56)
| ~ p(X59)
| p(X58)
| p(X61) ) ).
cnf(u17104,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X58)
| p(X60)
| ~ p(X61)
| p(X56)
| ~ p(X62)
| p(X57) ) ).
cnf(u15168,axiom,
( p(sK65(X7,X2,X4,X3,X5,X6,X1,X0))
| p(X1)
| ~ p(X2)
| p(X3)
| ~ p(X4)
| p(X5)
| p(X6)
| ~ p(X0) ) ).
cnf(u29874,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X57)
| p(X56)
| ~ p(X62)
| ~ p(X60)
| p(X63)
| ~ p(X58) ) ).
cnf(u51038,axiom,
( p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| ~ p(X5)
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X7)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| p(X6) ) ).
cnf(u16439,axiom,
( p(sK65(X6,X2,X4,X0,X7,X5,X3,X1))
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| p(X4)
| p(X5)
| p(X6)
| p(X0) ) ).
cnf(u2240,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X63)
| p(X60)
| p(X57)
| ~ p(X58)
| p(X59)
| ~ p(X56)
| p(X61) ) ).
cnf(u8011,axiom,
( p(sK65(X2,X1,X0,X6,X7,X5,X3,X4))
| ~ p(X1)
| p(X2)
| ~ p(X3)
| ~ p(X4)
| ~ p(X5)
| p(X6)
| ~ p(X0) ) ).
cnf(u18534,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X59)
| ~ p(X60)
| p(X58)
| p(X62)
| p(X56)
| p(X63) ) ).
cnf(u43554,axiom,
( ~ p(sK60(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK65(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| ~ p(X1)
| ~ p(X7) ) ).
cnf(u7469,axiom,
( p(sK64(X6,X1,X0,X2,X7,X3,X4,X5))
| ~ p(X1)
| ~ p(X2)
| p(X3)
| p(X4)
| ~ p(X5)
| p(X0) ) ).
cnf(u24563,axiom,
( p(sK65(X0,X1,X3,X2,X5,X4,X7,X6))
| ~ p(X2)
| p(X3)
| p(X4)
| ~ p(X5)
| p(X7)
| ~ p(X0) ) ).
cnf(u51120,axiom,
( ~ p(sK61(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X2)
| p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK65(X0,X1,X2,X3,X4,X5,X6,X7)) ) ).
cnf(u14606,axiom,
( p(sK65(X3,X5,X0,X6,X7,X1,X2,X4))
| ~ p(X1)
| ~ p(X2)
| p(X3)
| ~ p(X4)
| ~ p(X5)
| ~ p(X6)
| p(X0) ) ).
cnf(u40764,axiom,
( ~ p(sK61(X1,X2,X3,X4,X0,X5,X6,X7))
| p(sK65(X1,X2,X3,X4,X0,X5,X6,X7))
| ~ p(sK60(X1,X2,X3,X4,X0,X5,X6,X7))
| ~ p(X0) ) ).
cnf(u26755,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X61)
| p(X59)
| p(X63)
| p(X62)
| p(X60) ) ).
cnf(u7440,axiom,
( p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X58)
| ~ p(X57)
| ~ p(X59)
| p(X61)
| p(X62)
| ~ p(X63) ) ).
cnf(u27650,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X61)
| ~ p(X58)
| p(X62)
| p(X59)
| p(X57) ) ).
cnf(u49490,axiom,
( ~ p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK61(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK62(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u11518,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X59)
| ~ p(X61)
| p(X57)
| p(X60)
| p(X56)
| p(X58) ) ).
cnf(u49212,axiom,
( p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X3)
| p(X5) ) ).
cnf(u26756,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X57)
| p(X63)
| p(X56)
| p(X61)
| p(X62) ) ).
cnf(u31254,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X59)
| ~ p(X56)
| ~ p(X61)
| ~ p(X60)
| p(X62)
| p(X58) ) ).
cnf(u43612,axiom,
( p(sK66(X2,X0,X3,X4,X5,X6,X7,X1))
| ~ p(X1)
| ~ p(X0)
| p(X4)
| p(X3)
| ~ p(X6)
| p(X7) ) ).
cnf(u22313,axiom,
( p(sK65(X7,X2,X5,X0,X3,X6,X4,X1))
| ~ p(X1)
| ~ p(X2)
| p(X3)
| p(X4)
| p(X5)
| ~ p(X6)
| p(X0) ) ).
cnf(u44102,axiom,
( p(sK65(X6,X1,X5,X3,X7,X4,X2,X0))
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| p(X5)
| ~ p(X0) ) ).
cnf(u34501,axiom,
( ~ p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK64(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5) ) ).
cnf(u49097,axiom,
( ~ p(sK60(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK65(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4) ) ).
cnf(u50356,axiom,
( p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X2)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(X5) ) ).
cnf(u50145,axiom,
( p(sK64(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X6) ) ).
cnf(u48490,axiom,
( ~ p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK64(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X6) ) ).
cnf(u32670,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X59)
| p(X57)
| p(X60)
| p(X61)
| ~ p(X63) ) ).
cnf(u552,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK64(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u50190,axiom,
( p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X6)
| ~ p(X4)
| ~ p(X7)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1) ) ).
cnf(u17585,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X62)
| ~ p(X61)
| ~ p(X58)
| ~ p(X59)
| p(X57)
| p(X63) ) ).
cnf(u13207,axiom,
( p(sK64(X1,X5,X6,X4,X7,X3,X0,X2))
| p(X1)
| ~ p(X2)
| p(X3)
| p(X4)
| ~ p(X5)
| ~ p(X6)
| p(X0) ) ).
cnf(u51131,axiom,
( p(sK59(X1,X2,X0,X3,X4,X5,X6,X7))
| ~ p(X0)
| ~ p(X2)
| p(sK57(X1,X2,X0,X3,X4,X5,X6,X7))
| p(sK58(X1,X2,X0,X3,X4,X5,X6,X7))
| ~ p(X7)
| p(sK66(X1,X2,X0,X3,X4,X5,X6,X7)) ) ).
cnf(u49491,axiom,
( ~ p(sK62(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(sK61(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK65(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1) ) ).
cnf(u5174,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X60)
| p(X57)
| ~ p(X58)
| ~ p(X63)
| ~ p(X62)
| ~ p(X56)
| ~ p(X59) ) ).
cnf(u680,axiom,
p(true) ).
cnf(u4257,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X58)
| ~ p(X57)
| ~ p(X59)
| p(X60)
| p(X62)
| ~ p(X61)
| p(X56) ) ).
cnf(u12459,axiom,
( p(sK65(X7,X4,X3,X0,X1,X6,X2,X5))
| p(X1)
| p(X2)
| ~ p(X3)
| ~ p(X4)
| ~ p(X5)
| ~ p(X6)
| ~ p(X0) ) ).
cnf(u43859,axiom,
( p(sK64(X6,X1,X2,X3,X7,X4,X5,X0))
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| p(X5)
| ~ p(X0) ) ).
cnf(u2481,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X56)
| ~ p(X62)
| ~ p(X57)
| p(X59)
| p(X58)
| ~ p(X61) ) ).
cnf(u45208,axiom,
( p(sK62(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK60(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X7)
| p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X3) ) ).
cnf(u49141,axiom,
( p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X0)
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5) ) ).
cnf(u46562,axiom,
( p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4) ) ).
cnf(u5038,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X62)
| ~ p(X59)
| ~ p(X63)
| p(X58)
| ~ p(X61)
| p(X56)
| p(X60) ) ).
cnf(u18206,axiom,
( p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X62)
| ~ p(X56)
| ~ p(X60)
| ~ p(X58)
| ~ p(X59)
| ~ p(X61) ) ).
cnf(u7983,axiom,
( p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X58)
| ~ p(X57)
| p(X56)
| ~ p(X62)
| ~ p(X63)
| ~ p(X61)
| p(X59) ) ).
cnf(u12431,axiom,
( p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X59)
| p(X60)
| p(X62)
| ~ p(X58)
| ~ p(X57)
| ~ p(X63)
| ~ p(X61) ) ).
cnf(u19481,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X62)
| p(X60)
| p(X58)
| p(X59)
| ~ p(X56)
| p(X61) ) ).
cnf(u11961,axiom,
( p(sK64(X4,X6,X0,X2,X1,X5,X3,X7))
| ~ p(X1)
| p(X2)
| ~ p(X3)
| ~ p(X4)
| ~ p(X5)
| ~ p(X0) ) ).
cnf(u9284,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X57)
| p(X63)
| p(X62)
| p(X58)
| ~ p(X59)
| ~ p(X61) ) ).
cnf(u43615,axiom,
( p(sK66(X2,X0,X3,X4,X5,X6,X7,X1))
| ~ p(X1)
| ~ p(X0)
| p(X4)
| ~ p(X7)
| ~ p(X6)
| ~ p(X3) ) ).
cnf(u50202,axiom,
( p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X6)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| p(X5) ) ).
cnf(u49526,axiom,
( p(sK59(X2,X3,X4,X5,X0,X6,X7,X1))
| ~ p(X1)
| p(sK66(X2,X3,X4,X5,X0,X6,X7,X1))
| ~ p(X3)
| ~ p(X0)
| p(sK58(X2,X3,X4,X5,X0,X6,X7,X1))
| p(sK56(X2,X3,X4,X5,X0,X6,X7,X1))
| ~ p(X5) ) ).
cnf(u47978,axiom,
( p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| ~ p(X4)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X3)
| p(X5)
| p(X6) ) ).
cnf(u51033,axiom,
( p(sK58(X1,X2,X3,X4,X5,X0,X6,X7))
| p(sK56(X1,X2,X3,X4,X5,X0,X6,X7))
| ~ p(X2)
| ~ p(X0)
| p(sK57(X1,X2,X3,X4,X5,X0,X6,X7))
| ~ p(X7)
| p(sK66(X1,X2,X3,X4,X5,X0,X6,X7)) ) ).
cnf(u15948,axiom,
( p(sK65(X5,X4,X0,X1,X7,X6,X3,X2))
| p(X1)
| ~ p(X2)
| p(X3)
| ~ p(X4)
| p(X5)
| ~ p(X6)
| p(X0) ) ).
cnf(u23439,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X62)
| ~ p(X56)
| ~ p(X60)
| ~ p(X58)
| p(X61)
| p(X59) ) ).
cnf(u31910,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X63)
| ~ p(X56)
| p(X57)
| ~ p(X62)
| p(X60)
| ~ p(X58) ) ).
cnf(u45422,axiom,
( p(sK65(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| ~ p(X7)
| ~ p(X0) ) ).
cnf(u17391,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X58)
| p(X59)
| p(X63)
| p(X62)
| p(X56)
| ~ p(X61)
| ~ p(X57) ) ).
cnf(u49666,axiom,
( p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| ~ p(X7)
| ~ p(X5)
| p(X6)
| p(X3) ) ).
cnf(u50986,axiom,
( p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X3)
| ~ p(X1)
| p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X7)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7)) ) ).
cnf(u45993,axiom,
( p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| ~ p(X7)
| ~ p(X0)
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X3)
| p(X5) ) ).
cnf(u30521,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X63)
| p(X59)
| ~ p(X60)
| p(X56)
| ~ p(X58)
| ~ p(X57) ) ).
cnf(u46585,axiom,
( p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(X6)
| p(X3) ) ).
cnf(u24573,axiom,
( p(sK64(X6,X7,X5,X4,X3,X0,X1,X2))
| p(X1)
| ~ p(X3)
| p(X4)
| ~ p(X5)
| ~ p(X6)
| p(X0) ) ).
cnf(u24559,axiom,
( p(sK65(X7,X2,X6,X5,X1,X3,X0,X4))
| ~ p(X1)
| p(X3)
| ~ p(X5)
| ~ p(X6)
| ~ p(X7)
| ~ p(X0) ) ).
cnf(u14962,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X59)
| p(X61)
| p(X63)
| ~ p(X58)
| p(X62) ) ).
cnf(u45448,axiom,
( p(sK59(X1,X2,X3,X4,X5,X6,X7,X0))
| ~ p(X1)
| p(sK66(X1,X2,X3,X4,X5,X6,X7,X0))
| ~ p(X5)
| ~ p(X0)
| p(sK58(X1,X2,X3,X4,X5,X6,X7,X0))
| p(sK56(X1,X2,X3,X4,X5,X6,X7,X0))
| ~ p(X4) ) ).
cnf(u48946,axiom,
( p(sK62(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X6)
| ~ p(X3)
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK60(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X7) ) ).
cnf(u51121,axiom,
( p(sK65(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X2)
| p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X7) ) ).
cnf(u24616,axiom,
( p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| p(X6)
| ~ p(X4)
| p(X3)
| ~ p(X2)
| ~ p(X0)
| p(X5) ) ).
cnf(u11617,axiom,
( p(sK65(X2,X6,X0,X5,X1,X4,X3,X7))
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| p(X4)
| p(X5)
| p(X0) ) ).
cnf(u11371,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X62)
| ~ p(X57)
| ~ p(X58)
| p(X63)
| ~ p(X56)
| p(X60) ) ).
cnf(u31816,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X57)
| p(X63)
| p(X60)
| ~ p(X58)
| ~ p(X56) ) ).
cnf(u39606,axiom,
( ~ p(sK61(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK65(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK62(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK60(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1) ) ).
cnf(u6632,axiom,
( p(sK65(X7,X2,X6,X1,X5,X4,X3,X0))
| p(X1)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| p(X5)
| ~ p(X6)
| ~ p(X0) ) ).
cnf(u14578,axiom,
( p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X58)
| ~ p(X61)
| ~ p(X62)
| p(X56)
| ~ p(X63)
| ~ p(X57)
| ~ p(X59) ) ).
cnf(u44592,axiom,
( p(sK64(X6,X1,X5,X4,X7,X3,X2,X0))
| ~ p(X1)
| ~ p(X2)
| p(X3)
| p(X4)
| p(X5)
| ~ p(X0) ) ).
cnf(u18632,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X58)
| ~ p(X60)
| p(X56)
| p(X63)
| ~ p(X59)
| p(X61) ) ).
cnf(u46539,axiom,
( p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X3)
| ~ p(X2)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4) ) ).
cnf(u14607,axiom,
( p(sK64(X3,X5,X0,X6,X7,X1,X2,X4))
| ~ p(X1)
| ~ p(X2)
| p(X3)
| ~ p(X4)
| ~ p(X5)
| ~ p(X6)
| p(X0) ) ).
cnf(u49098,axiom,
( p(sK65(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| ~ p(X0) ) ).
cnf(u50521,axiom,
( ~ p(sK61(X3,X4,X2,X1,X5,X6,X0,X7))
| ~ p(X1)
| ~ p(X2)
| p(sK59(X3,X4,X2,X1,X5,X6,X0,X7))
| ~ p(X4)
| ~ p(X0)
| p(sK65(X3,X4,X2,X1,X5,X6,X0,X7)) ) ).
cnf(u50866,axiom,
( ~ p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK61(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK63(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u50551,axiom,
( ~ p(sK61(X3,X4,X5,X2,X6,X0,X1,X7))
| ~ p(X1)
| ~ p(X2)
| p(sK56(X3,X4,X5,X2,X6,X0,X1,X7))
| ~ p(X4)
| ~ p(X0)
| p(sK65(X3,X4,X5,X2,X6,X0,X1,X7)) ) ).
cnf(u43614,axiom,
( p(sK66(X2,X0,X3,X4,X5,X6,X7,X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(X7)
| ~ p(X4)
| ~ p(X6)
| p(X3) ) ).
cnf(u17904,axiom,
( p(sK64(X3,X6,X0,X1,X7,X4,X2,X5))
| ~ p(X1)
| p(X2)
| p(X3)
| ~ p(X4)
| ~ p(X5)
| ~ p(X6)
| ~ p(X0) ) ).
cnf(u48533,axiom,
( p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X6)
| ~ p(X3)
| ~ p(X2)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4) ) ).
cnf(u32286,axiom,
( p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X62)
| p(X61)
| p(X59)
| ~ p(X58)
| ~ p(X63)
| ~ p(X57) ) ).
cnf(u11932,axiom,
( p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X58)
| ~ p(X60)
| p(X59)
| ~ p(X62)
| ~ p(X56)
| ~ p(X61) ) ).
cnf(u44881,axiom,
( ~ p(sK64(X1,X2,X3,X4,X5,X6,X7,X0))
| p(sK62(X1,X2,X3,X4,X5,X6,X7,X0))
| p(sK60(X1,X2,X3,X4,X5,X6,X7,X0))
| ~ p(X2)
| p(sK66(X1,X2,X3,X4,X5,X6,X7,X0))
| ~ p(X0) ) ).
cnf(u28802,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X59)
| ~ p(X60)
| ~ p(X58)
| p(X57)
| ~ p(X61)
| p(X56) ) ).
cnf(u50499,axiom,
( p(sK58(X1,X2,X0,X3,X4,X5,X6,X7))
| ~ p(X0)
| ~ p(X2)
| ~ p(X5)
| ~ p(X3)
| ~ p(X7)
| p(sK66(X1,X2,X0,X3,X4,X5,X6,X7)) ) ).
cnf(u50253,axiom,
( p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X6)
| ~ p(X4)
| ~ p(X7)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(X5) ) ).
cnf(u49659,axiom,
( p(sK57(X1,X2,X3,X4,X5,X6,X7,X0))
| p(sK66(X1,X2,X3,X4,X5,X6,X7,X0))
| ~ p(X2)
| p(sK56(X1,X2,X3,X4,X5,X6,X7,X0))
| ~ p(X5)
| ~ p(X0)
| ~ p(X6)
| p(X7) ) ).
cnf(u46540,axiom,
( p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X3)
| ~ p(X2)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1) ) ).
cnf(u46581,axiom,
( p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(X6) ) ).
cnf(u28618,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X57)
| p(X60)
| ~ p(X56)
| p(X61)
| ~ p(X58)
| ~ p(X59) ) ).
cnf(u51136,axiom,
( p(sK58(X2,X1,X0,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(sK57(X2,X1,X0,X3,X4,X5,X6,X7))
| ~ p(X0)
| ~ p(X7)
| p(sK66(X2,X1,X0,X3,X4,X5,X6,X7))
| p(X5) ) ).
cnf(u51206,axiom,
( ~ p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK61(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK60(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u50262,axiom,
( p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X6)
| ~ p(X4)
| ~ p(X7)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(X5)
| p(X3) ) ).
cnf(u45421,axiom,
( ~ p(sK60(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK65(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| ~ p(X7) ) ).
cnf(u45915,axiom,
( ~ p(sK61(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK65(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(sK60(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1) ) ).
cnf(u29075,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X56)
| p(X58)
| p(X57)
| ~ p(X60)
| ~ p(X59)
| ~ p(X62) ) ).
cnf(u12354,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X56)
| p(X58)
| p(X61)
| ~ p(X63)
| p(X62)
| p(X59) ) ).
cnf(u5307,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X59)
| p(X62)
| p(X58)
| ~ p(X56)
| p(X63)
| ~ p(X60)
| ~ p(X61) ) ).
cnf(u50340,axiom,
( p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X2)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| p(X5)
| p(X6) ) ).
cnf(u32056,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X60)
| ~ p(X59)
| ~ p(X58)
| p(X62)
| p(X61) ) ).
cnf(u32571,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X62)
| ~ p(X61)
| ~ p(X63)
| ~ p(X59)
| ~ p(X58)
| ~ p(X60) ) ).
cnf(u17296,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X56)
| ~ p(X62)
| p(X57)
| ~ p(X58)
| ~ p(X63)
| ~ p(X61) ) ).
cnf(u6222,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X60)
| p(X62)
| p(X56)
| ~ p(X59)
| p(X61)
| ~ p(X58) ) ).
cnf(u51144,axiom,
( p(sK57(X1,X0,X2,X3,X4,X5,X6,X7))
| ~ p(X0)
| ~ p(X2)
| ~ p(X7)
| p(sK66(X1,X0,X2,X3,X4,X5,X6,X7))
| p(X5)
| p(X6) ) ).
cnf(u6604,axiom,
( p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X63)
| p(X59)
| ~ p(X57)
| ~ p(X62)
| ~ p(X61)
| p(X60)
| ~ p(X58) ) ).
cnf(u48947,axiom,
( p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X6)
| ~ p(X3)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4) ) ).
cnf(u51070,axiom,
( ~ p(sK61(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X6)
| p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK65(X0,X1,X2,X3,X4,X5,X6,X7)) ) ).
cnf(u46555,axiom,
( p(sK64(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5) ) ).
cnf(u32786,axiom,
( p(sK64(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X3) ) ).
cnf(u31957,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X60)
| p(X58)
| p(X63)
| ~ p(X56)
| ~ p(X59) ) ).
cnf(u51071,axiom,
( p(sK65(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X6)
| p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X7) ) ).
cnf(u11223,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X62)
| ~ p(X56)
| p(X59)
| ~ p(X57)
| ~ p(X58)
| p(X61) ) ).
cnf(u47876,axiom,
( p(sK57(X1,X2,X3,X4,X0,X5,X6,X7))
| ~ p(X1)
| p(sK66(X1,X2,X3,X4,X0,X5,X6,X7))
| ~ p(X2)
| ~ p(X0)
| ~ p(X5)
| ~ p(X6)
| ~ p(X3) ) ).
cnf(u29341,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X61)
| p(X63)
| ~ p(X57)
| ~ p(X56)
| ~ p(X58)
| p(X60) ) ).
cnf(u37277,axiom,
( ~ p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK60(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u28596,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X57)
| p(X58)
| p(X61)
| p(X63)
| ~ p(X62)
| ~ p(X59) ) ).
cnf(u10085,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X63)
| ~ p(X62)
| ~ p(X59)
| p(X58)
| ~ p(X56)
| p(X61) ) ).
cnf(u32009,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X56)
| p(X58)
| ~ p(X59)
| ~ p(X63)
| p(X57)
| ~ p(X60) ) ).
cnf(u3060,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X60)
| ~ p(X62)
| p(X63)
| ~ p(X59)
| ~ p(X56)
| p(X61) ) ).
cnf(u46926,axiom,
( ~ p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK60(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK61(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u48948,axiom,
( p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X6)
| ~ p(X3)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1) ) ).
cnf(u32835,axiom,
( ~ p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK60(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK61(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u49099,axiom,
( ~ p(sK64(X1,X2,X3,X4,X0,X5,X6,X7))
| ~ p(X1)
| p(sK66(X1,X2,X3,X4,X0,X5,X6,X7))
| ~ p(X0) ) ).
cnf(u5129,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X59)
| p(X61)
| ~ p(X62)
| ~ p(X63)
| p(X56)
| p(X57) ) ).
cnf(u21591,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X58)
| ~ p(X56)
| p(X60)
| ~ p(X62)
| p(X63)
| ~ p(X59) ) ).
cnf(u50991,axiom,
( p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X3)
| ~ p(X1)
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X7)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| p(X5) ) ).
cnf(u22655,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X59)
| ~ p(X56)
| p(X62)
| ~ p(X58)
| ~ p(X61) ) ).
cnf(u50236,axiom,
( p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X6)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(X5)
| p(X3) ) ).
cnf(u45916,axiom,
( ~ p(sK60(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK65(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| ~ p(X7) ) ).
cnf(u23211,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X59)
| p(X60)
| ~ p(X56)
| ~ p(X62)
| p(X61)
| p(X57) ) ).
cnf(u32574,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X59)
| p(X62)
| p(X61)
| p(X56)
| ~ p(X58) ) ).
cnf(u9223,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X59)
| ~ p(X61)
| p(X57)
| p(X60)
| ~ p(X62) ) ).
cnf(u47973,axiom,
( p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| ~ p(X4)
| ~ p(X0)
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X3)
| p(X5) ) ).
cnf(u29315,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X63)
| ~ p(X59)
| ~ p(X62)
| p(X60)
| ~ p(X56)
| ~ p(X57) ) ).
cnf(u50489,axiom,
( ~ p(sK61(X3,X4,X2,X1,X5,X0,X6,X7))
| ~ p(X1)
| ~ p(X2)
| p(sK58(X3,X4,X2,X1,X5,X0,X6,X7))
| ~ p(X4)
| ~ p(X0)
| p(sK65(X3,X4,X2,X1,X5,X0,X6,X7)) ) ).
cnf(u9351,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X60)
| ~ p(X59)
| p(X57)
| p(X56)
| p(X61)
| ~ p(X63) ) ).
cnf(u51022,axiom,
( ~ p(sK61(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK65(X0,X1,X2,X3,X4,X5,X6,X7)) ) ).
cnf(u29098,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X60)
| ~ p(X59)
| ~ p(X56)
| p(X57)
| ~ p(X63)
| ~ p(X58) ) ).
cnf(u27230,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X58)
| p(X60)
| p(X63)
| ~ p(X59)
| p(X62) ) ).
cnf(u6551,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X60)
| p(X62)
| p(X58)
| p(X59)
| p(X56)
| p(X61) ) ).
cnf(u10294,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X62)
| p(X57)
| p(X56)
| p(X61)
| ~ p(X60)
| p(X59) ) ).
cnf(u46567,axiom,
( p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| p(X6) ) ).
cnf(u50331,axiom,
( p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X2)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| p(X5) ) ).
cnf(u49536,axiom,
( p(sK56(X2,X3,X4,X5,X0,X6,X7,X1))
| ~ p(X1)
| p(sK66(X2,X3,X4,X5,X0,X6,X7,X1))
| ~ p(X3)
| ~ p(X0)
| ~ p(X6)
| ~ p(X7)
| ~ p(X5) ) ).
cnf(u29392,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X58)
| ~ p(X62)
| ~ p(X57)
| p(X59)
| p(X61) ) ).
cnf(u24569,axiom,
( p(sK64(X6,X2,X4,X1,X0,X5,X7,X3))
| p(X1)
| p(X4)
| ~ p(X5)
| ~ p(X6)
| p(X7)
| ~ p(X0) ) ).
cnf(u47877,axiom,
( p(sK58(X1,X2,X3,X4,X0,X5,X6,X7))
| ~ p(X1)
| p(sK66(X1,X2,X3,X4,X0,X5,X6,X7))
| ~ p(X2)
| ~ p(X0)
| ~ p(X5)
| ~ p(X4)
| ~ p(X3) ) ).
cnf(u47878,axiom,
( p(sK58(X1,X2,X3,X4,X0,X5,X6,X7))
| ~ p(X1)
| p(sK66(X1,X2,X3,X4,X0,X5,X6,X7))
| ~ p(X2)
| p(sK56(X1,X2,X3,X4,X0,X5,X6,X7))
| ~ p(X0)
| p(sK57(X1,X2,X3,X4,X0,X5,X6,X7))
| ~ p(X5) ) ).
cnf(u50319,axiom,
( p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X2)
| ~ p(X4)
| ~ p(X7)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1) ) ).
cnf(u51023,axiom,
( p(sK65(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X7) ) ).
cnf(u22174,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X61)
| p(X60)
| ~ p(X57)
| ~ p(X56)
| p(X62)
| p(X63) ) ).
cnf(u48910,axiom,
( ~ p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK64(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X6) ) ).
cnf(u49142,axiom,
( p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| ~ p(X0)
| ~ p(X6)
| ~ p(X3)
| ~ p(X2) ) ).
cnf(u16440,axiom,
( p(sK64(X6,X2,X4,X0,X7,X5,X3,X1))
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| p(X4)
| p(X5)
| p(X6)
| p(X0) ) ).
cnf(u50531,axiom,
( p(sK59(X1,X2,X0,X3,X4,X5,X6,X7))
| ~ p(X0)
| ~ p(X2)
| ~ p(X6)
| ~ p(X3)
| ~ p(X7)
| p(sK66(X1,X2,X0,X3,X4,X5,X6,X7)) ) ).
cnf(u17006,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X56)
| p(X58)
| ~ p(X62)
| ~ p(X61)
| p(X57)
| p(X59) ) ).
cnf(u27827,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X63)
| p(X60)
| p(X62)
| p(X61)
| ~ p(X57) ) ).
cnf(u14235,axiom,
( p(sK64(X7,X2,X6,X0,X1,X5,X4,X3))
| p(X1)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| p(X5)
| p(X6)
| p(X0) ) ).
cnf(u46571,axiom,
( p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| p(X6)
| p(X3) ) ).
cnf(u337,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK65(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u29642,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X62)
| ~ p(X60)
| p(X61)
| p(X56)
| ~ p(X58)
| p(X63) ) ).
cnf(u10923,axiom,
( p(sK64(X6,X2,X4,X5,X7,X3,X1,X0))
| ~ p(X1)
| ~ p(X2)
| p(X3)
| ~ p(X4)
| ~ p(X5)
| ~ p(X0) ) ).
cnf(u24565,axiom,
( p(sK64(X0,X1,X3,X2,X5,X4,X7,X6))
| ~ p(X2)
| p(X3)
| p(X4)
| ~ p(X5)
| p(X7)
| ~ p(X0) ) ).
cnf(u7641,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X62)
| p(X58)
| p(X59)
| p(X60)
| ~ p(X61) ) ).
cnf(u23100,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X60)
| p(X56)
| ~ p(X62)
| p(X59)
| p(X63)
| p(X58) ) ).
cnf(u46527,axiom,
( ~ p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK64(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X3) ) ).
cnf(u29052,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X58)
| p(X61)
| ~ p(X62)
| ~ p(X59)
| ~ p(X57) ) ).
cnf(u22770,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X56)
| p(X61)
| p(X57)
| p(X63)
| p(X58) ) ).
cnf(u40766,axiom,
( ~ p(sK61(X1,X2,X3,X4,X0,X5,X6,X7))
| p(sK65(X1,X2,X3,X4,X0,X5,X6,X7))
| ~ p(sK60(X1,X2,X3,X4,X0,X5,X6,X7))
| ~ p(X0)
| ~ p(X2) ) ).
cnf(u50381,axiom,
( p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X2)
| ~ p(X4)
| ~ p(X7)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(X5) ) ).
cnf(u24444,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X57)
| p(X56)
| ~ p(X62)
| ~ p(X61)
| p(X63)
| ~ p(X58) ) ).
cnf(u44349,axiom,
( p(sK64(X6,X1,X5,X2,X7,X4,X3,X0))
| ~ p(X1)
| p(X2)
| ~ p(X3)
| ~ p(X4)
| ~ p(X5)
| ~ p(X0) ) ).
cnf(u254,axiom,
( ~ p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK64(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u21120,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X57)
| p(X61)
| p(X62)
| ~ p(X58)
| ~ p(X59) ) ).
cnf(u45917,axiom,
( p(sK65(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| ~ p(X7)
| ~ p(X0) ) ).
cnf(u46532,axiom,
( p(sK64(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X3)
| ~ p(X2) ) ).
cnf(u32195,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X62)
| p(X58)
| ~ p(X57)
| p(X59)
| p(X61)
| p(X60) ) ).
cnf(u11618,axiom,
( p(sK64(X2,X6,X0,X5,X1,X4,X3,X7))
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| p(X4)
| p(X5)
| p(X0) ) ).
cnf(u10894,axiom,
( p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X63)
| ~ p(X62)
| ~ p(X57)
| p(X61)
| ~ p(X58)
| ~ p(X59) ) ).
cnf(u28450,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X63)
| ~ p(X58)
| p(X62)
| p(X59)
| ~ p(X61) ) ).
cnf(u48983,axiom,
( ~ p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK60(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK62(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u50999,axiom,
( p(sK56(X2,X1,X3,X0,X4,X5,X6,X7))
| ~ p(X1)
| ~ p(X0)
| ~ p(X7)
| p(sK66(X2,X1,X3,X0,X4,X5,X6,X7))
| p(X5)
| p(X6) ) ).
cnf(u50189,axiom,
( p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X6)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4) ) ).
cnf(u31295,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X56)
| p(X58)
| p(X63)
| ~ p(X57)
| p(X60)
| p(X61) ) ).
cnf(u50185,axiom,
( p(sK62(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X6)
| p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK60(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X7) ) ).
cnf(u47840,axiom,
( p(sK65(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| ~ p(X4)
| ~ p(X0) ) ).
cnf(u12460,axiom,
( p(sK64(X7,X4,X3,X0,X1,X6,X2,X5))
| p(X1)
| p(X2)
| ~ p(X3)
| ~ p(X4)
| ~ p(X5)
| ~ p(X6)
| ~ p(X0) ) ).
cnf(u23661,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X62)
| p(X60)
| p(X57)
| p(X56)
| p(X59) ) ).
cnf(u47845,axiom,
( ~ p(sK64(X2,X0,X3,X4,X1,X5,X6,X7))
| ~ p(X1)
| ~ p(X2)
| p(sK66(X2,X0,X3,X4,X1,X5,X6,X7))
| ~ p(X0) ) ).
cnf(u10224,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X56)
| p(X63)
| p(X59)
| ~ p(X57)
| p(X60)
| p(X62) ) ).
cnf(u29005,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X61)
| p(X57)
| ~ p(X59)
| p(X60)
| p(X63)
| p(X62) ) ).
cnf(u19689,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X63)
| ~ p(X58)
| p(X62)
| p(X56)
| ~ p(X59) ) ).
cnf(u50211,axiom,
( p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X6)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| p(X5)
| p(X3) ) ).
cnf(u32103,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X60)
| ~ p(X58)
| ~ p(X59)
| p(X63)
| p(X56) ) ).
cnf(u29366,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X61)
| p(X59)
| ~ p(X62)
| ~ p(X57)
| ~ p(X60)
| ~ p(X58) ) ).
cnf(u16908,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X61)
| ~ p(X57)
| p(X59)
| p(X58)
| ~ p(X60)
| p(X62)
| ~ p(X63) ) ).
cnf(u43618,axiom,
( p(sK64(X6,X1,X3,X2,X7,X4,X5,X0))
| ~ p(X1)
| p(X2)
| p(X3)
| ~ p(X4)
| p(X5)
| ~ p(X0) ) ).
cnf(u48534,axiom,
( p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X6)
| ~ p(X3)
| ~ p(X2)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1) ) ).
cnf(u28781,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X57)
| p(X56)
| p(X63)
| ~ p(X61)
| ~ p(X59)
| ~ p(X58) ) ).
cnf(u11960,axiom,
( p(sK65(X4,X6,X0,X2,X1,X5,X3,X7))
| ~ p(X1)
| p(X2)
| ~ p(X3)
| ~ p(X4)
| ~ p(X5)
| ~ p(X0) ) ).
cnf(u50365,axiom,
( p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X2)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(X5)
| p(X6) ) ).
cnf(u46082,axiom,
( p(sK62(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X6)
| ~ p(X2)
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK60(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X7) ) ).
cnf(u11297,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X57)
| p(X61)
| ~ p(X62)
| p(X63)
| p(X60)
| ~ p(X59) ) ).
cnf(u43557,axiom,
( ~ p(sK64(X3,X1,X4,X5,X0,X6,X7,X2))
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| p(sK66(X3,X1,X4,X5,X0,X6,X7,X2))
| ~ p(X0) ) ).
cnf(u51094,axiom,
( p(sK56(X2,X0,X3,X4,X5,X6,X1,X7))
| ~ p(X1)
| ~ p(X0)
| ~ p(X7)
| p(sK66(X2,X0,X3,X4,X5,X6,X1,X7))
| p(X6)
| p(X4) ) ).
cnf(u15140,axiom,
( p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X63)
| p(X62)
| ~ p(X57)
| p(X59)
| ~ p(X58)
| p(X60)
| p(X61) ) ).
cnf(u50318,axiom,
( p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X2)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4) ) ).
cnf(u32522,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X63)
| p(X61)
| ~ p(X60)
| p(X57)
| p(X59)
| p(X56) ) ).
cnf(u16317,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X58)
| p(X60)
| p(X59)
| ~ p(X61)
| ~ p(X63)
| p(X57) ) ).
cnf(u49494,axiom,
( ~ p(sK64(X3,X0,X4,X5,X1,X6,X7,X2))
| ~ p(X1)
| ~ p(X2)
| p(sK66(X3,X0,X4,X5,X1,X6,X7,X2))
| ~ p(X0) ) ).
cnf(u48900,axiom,
( ~ p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK64(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5) ) ).
cnf(u46075,axiom,
( ~ p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK64(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X6) ) ).
cnf(u10922,axiom,
( p(sK65(X6,X2,X4,X5,X7,X3,X1,X0))
| ~ p(X1)
| ~ p(X2)
| p(X3)
| ~ p(X4)
| ~ p(X5)
| ~ p(X0) ) ).
cnf(u5808,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X60)
| ~ p(X57)
| p(X58)
| p(X62)
| ~ p(X59)
| ~ p(X63)
| ~ p(X61) ) ).
cnf(u681,axiom,
true != false ).
cnf(u13917,axiom,
( p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X60)
| ~ p(X59)
| ~ p(X57)
| ~ p(X63)
| p(X58)
| ~ p(X61)
| ~ p(X62) ) ).
cnf(u32149,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X60)
| p(X56)
| p(X63)
| ~ p(X57)
| ~ p(X62) ) ).
cnf(u47785,axiom,
( ~ p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK60(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK62(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK61(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u8012,axiom,
( p(sK64(X2,X1,X0,X6,X7,X5,X3,X4))
| ~ p(X1)
| p(X2)
| ~ p(X3)
| ~ p(X4)
| ~ p(X5)
| p(X6)
| ~ p(X0) ) ).
cnf(u48506,axiom,
( ~ p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK64(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X6)
| ~ p(X3) ) ).
cnf(u49535,axiom,
( p(sK59(X2,X3,X4,X5,X0,X6,X7,X1))
| ~ p(X1)
| p(sK66(X2,X3,X4,X5,X0,X6,X7,X1))
| ~ p(X3)
| ~ p(X0)
| ~ p(X7)
| ~ p(X5)
| ~ p(X4) ) ).
cnf(u28512,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X58)
| ~ p(X59)
| ~ p(X56)
| ~ p(X60)
| p(X61)
| p(X62) ) ).
cnf(u47988,axiom,
( p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| ~ p(X0)
| ~ p(X5)
| p(X6)
| p(X3) ) ).
cnf(u3848,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X61)
| ~ p(X63)
| p(X59)
| p(X58)
| ~ p(X57)
| ~ p(X62) ) ).
cnf(u48949,axiom,
( p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X6)
| ~ p(X3)
| ~ p(X4)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1) ) ).
cnf(u18234,axiom,
( p(sK65(X1,X6,X3,X4,X2,X5,X0,X7))
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| ~ p(X5)
| p(X0) ) ).
cnf(u49493,axiom,
( p(sK65(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| ~ p(X4)
| ~ p(X7) ) ).
cnf(u17903,axiom,
( p(sK65(X3,X6,X0,X1,X7,X4,X2,X5))
| ~ p(X1)
| p(X2)
| p(X3)
| ~ p(X4)
| ~ p(X5)
| ~ p(X6)
| ~ p(X0) ) ).
cnf(u6633,axiom,
( p(sK64(X7,X2,X6,X1,X5,X4,X3,X0))
| p(X1)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| p(X5)
| ~ p(X6)
| ~ p(X0) ) ).
cnf(u43550,axiom,
( p(sK65(X1,X2,X3,X4,X5,X6,X7,X0))
| ~ p(X0)
| p(sK62(X1,X2,X3,X4,X5,X6,X7,X0))
| p(sK60(X1,X2,X3,X4,X5,X6,X7,X0))
| ~ p(X2) ) ).
cnf(u8411,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X61)
| p(X57)
| ~ p(X58)
| p(X60)
| ~ p(X62)
| p(X63) ) ).
cnf(u22990,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X62)
| p(X59)
| ~ p(X60)
| p(X56)
| p(X58)
| p(X57) ) ).
cnf(u50275,axiom,
( p(sK64(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X2) ) ).
cnf(u50187,axiom,
( p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X6)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1) ) ).
cnf(u23325,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X63)
| ~ p(X57)
| p(X56)
| ~ p(X60)
| ~ p(X61) ) ).
cnf(u49139,axiom,
( p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| ~ p(X0)
| ~ p(X5)
| ~ p(X6)
| ~ p(X2) ) ).
cnf(u32287,axiom,
( p(sK65(X6,X5,X3,X2,X7,X1,X0,X4))
| p(X1)
| p(X2)
| ~ p(X3)
| ~ p(X4)
| ~ p(X5)
| p(X0) ) ).
cnf(u23880,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X60)
| p(X62)
| p(X61)
| p(X63)
| p(X56) ) ).
cnf(u43613,axiom,
( p(sK66(X2,X0,X3,X4,X5,X6,X7,X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(X3)
| ~ p(X4)
| ~ p(X6)
| p(X7) ) ).
cnf(u24218,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X61)
| ~ p(X58)
| p(X60)
| ~ p(X56)
| ~ p(X62)
| p(X63) ) ).
cnf(u50227,axiom,
( p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X6)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(X5) ) ).
cnf(u13575,axiom,
( p(sK65(X1,X6,X0,X3,X5,X4,X2,X7))
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| ~ p(X5)
| p(X0) ) ).
cnf(u10364,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X62)
| ~ p(X56)
| ~ p(X57)
| ~ p(X59)
| ~ p(X58)
| ~ p(X61) ) ).
cnf(u24618,axiom,
( p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X3)
| p(X2)
| p(X5)
| ~ p(X4)
| p(X6)
| ~ p(X0) ) ).
cnf(u46522,axiom,
( ~ p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK64(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5) ) ).
cnf(u13946,axiom,
( p(sK64(X7,X2,X4,X1,X0,X5,X6,X3))
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| p(X4)
| ~ p(X5)
| ~ p(X6)
| p(X0) ) ).
cnf(u45919,axiom,
( ~ p(sK64(X2,X0,X3,X4,X5,X6,X7,X1))
| ~ p(X1)
| ~ p(X2)
| p(sK66(X2,X0,X3,X4,X5,X6,X7,X1))
| ~ p(X0) ) ).
cnf(u24561,axiom,
( p(sK64(X7,X2,X6,X5,X1,X3,X0,X4))
| ~ p(X1)
| p(X3)
| ~ p(X5)
| ~ p(X6)
| ~ p(X7)
| ~ p(X0) ) ).
cnf(u46563,axiom,
( p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1) ) ).
cnf(u17683,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X56)
| p(X60)
| ~ p(X59)
| p(X61)
| p(X63)
| ~ p(X57) ) ).
cnf(u28491,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X60)
| ~ p(X58)
| p(X62)
| p(X61)
| p(X57)
| ~ p(X63) ) ).
cnf(u50490,axiom,
( p(sK65(X2,X3,X1,X0,X4,X5,X6,X7))
| ~ p(X1)
| p(sK58(X2,X3,X1,X0,X4,X5,X6,X7))
| ~ p(X3)
| ~ p(X5)
| ~ p(X0)
| ~ p(X7) ) ).
cnf(u48532,axiom,
( p(sK62(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X6)
| ~ p(X3)
| ~ p(X2)
| p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK60(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X7) ) ).
cnf(u43617,axiom,
( p(sK65(X6,X1,X3,X2,X7,X4,X5,X0))
| ~ p(X1)
| p(X2)
| p(X3)
| ~ p(X4)
| p(X5)
| ~ p(X0) ) ).
cnf(u13101,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X60)
| p(X61)
| p(X58)
| p(X57)
| p(X56) ) ).
cnf(u50561,axiom,
( p(sK56(X1,X2,X3,X0,X4,X5,X6,X7))
| ~ p(X0)
| ~ p(X2)
| ~ p(X5)
| ~ p(X6)
| ~ p(X7)
| p(sK66(X1,X2,X3,X0,X4,X5,X6,X7)) ) ).
cnf(u31553,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X63)
| ~ p(X57)
| ~ p(X62)
| p(X56)
| ~ p(X60)
| p(X59) ) ).
cnf(u15169,axiom,
( p(sK64(X7,X2,X4,X3,X5,X6,X1,X0))
| p(X1)
| ~ p(X2)
| p(X3)
| ~ p(X4)
| p(X5)
| p(X6)
| ~ p(X0) ) ).
cnf(u679,axiom,
~ p(false) ).
cnf(u11589,axiom,
( p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X58)
| ~ p(X60)
| ~ p(X56)
| ~ p(X62)
| p(X61)
| p(X59) ) ).
cnf(u51086,axiom,
( p(sK57(X2,X1,X3,X4,X5,X6,X0,X7))
| ~ p(X1)
| ~ p(X0)
| p(sK56(X2,X1,X3,X4,X5,X6,X0,X7))
| ~ p(X7)
| p(sK66(X2,X1,X3,X4,X5,X6,X0,X7))
| p(X6) ) ).
cnf(u22062,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X61)
| ~ p(X57)
| ~ p(X59)
| p(X58)
| ~ p(X62)
| p(X56) ) ).
cnf(u22314,axiom,
( p(sK64(X7,X2,X5,X0,X3,X6,X4,X1))
| ~ p(X1)
| ~ p(X2)
| p(X3)
| p(X4)
| p(X5)
| ~ p(X6)
| p(X0) ) ).
cnf(u18235,axiom,
( p(sK64(X1,X6,X3,X4,X2,X5,X0,X7))
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| ~ p(X5)
| p(X0) ) ).
cnf(u15920,axiom,
( p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X58)
| p(X59)
| ~ p(X63)
| p(X62)
| ~ p(X57)
| p(X56)
| ~ p(X61) ) ).
cnf(u28536,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X60)
| ~ p(X59)
| p(X57)
| ~ p(X62)
| p(X61) ) ).
cnf(u32288,axiom,
( p(sK64(X6,X5,X3,X2,X7,X1,X0,X4))
| p(X1)
| p(X2)
| ~ p(X3)
| ~ p(X4)
| ~ p(X5)
| p(X0) ) ).
cnf(u43616,axiom,
( p(sK66(X2,X0,X3,X4,X5,X6,X7,X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(X7)
| p(X6)
| p(X4)
| p(X3) ) ).
cnf(u49143,axiom,
( p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| ~ p(X0)
| ~ p(X5)
| ~ p(X6)
| ~ p(X3) ) ).
cnf(u45565,axiom,
( p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X3)
| p(X5)
| p(X6) ) ).
cnf(u48535,axiom,
( p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X6)
| ~ p(X3)
| ~ p(X2)
| ~ p(X4)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1) ) ).
cnf(u50316,axiom,
( p(sK59(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK58(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X2)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1) ) ).
cnf(u44591,axiom,
( p(sK65(X6,X1,X5,X4,X7,X3,X2,X0))
| ~ p(X1)
| ~ p(X2)
| p(X3)
| p(X4)
| p(X5)
| ~ p(X0) ) ).
cnf(u48929,axiom,
( p(sK64(X0,X1,X2,X3,X4,X5,X6,X7))
| p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X6)
| ~ p(X3) ) ).
cnf(u49220,axiom,
( p(sK56(X1,X2,X3,X4,X0,X5,X6,X7))
| ~ p(X1)
| p(sK66(X1,X2,X3,X4,X0,X5,X6,X7))
| ~ p(X0)
| ~ p(X4)
| p(X5)
| p(X6) ) ).
cnf(u44103,axiom,
( p(sK64(X6,X1,X5,X3,X7,X4,X2,X0))
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| p(X5)
| ~ p(X0) ) ).
cnf(u47784,axiom,
( ~ p(sK63(X56,X57,X58,X59,X60,X61,X62,X63))
| p(sK65(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK60(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(sK62(X56,X57,X58,X59,X60,X61,X62,X63)) ) ).
cnf(u7699,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X61)
| p(X57)
| p(X60)
| ~ p(X62)
| p(X63)
| p(X58) ) ).
cnf(u50457,axiom,
( ~ p(sK61(X3,X4,X2,X5,X6,X0,X1,X7))
| ~ p(X1)
| ~ p(X2)
| p(sK57(X3,X4,X2,X5,X6,X0,X1,X7))
| ~ p(X4)
| ~ p(X0)
| p(sK65(X3,X4,X2,X5,X6,X0,X1,X7)) ) ).
cnf(u22877,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X63)
| p(X58)
| ~ p(X61)
| ~ p(X62)
| ~ p(X57)
| p(X60) ) ).
cnf(u14206,axiom,
( p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X59)
| p(X60)
| ~ p(X57)
| ~ p(X63)
| ~ p(X62)
| p(X61)
| p(X58) ) ).
cnf(u46085,axiom,
( p(sK57(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X5)
| ~ p(X6)
| ~ p(X2)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X4) ) ).
cnf(u24104,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X63)
| p(X58)
| ~ p(X56)
| p(X59)
| p(X61)
| p(X62) ) ).
cnf(u5397,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| ~ p(X62)
| ~ p(X63)
| ~ p(X59)
| ~ p(X61)
| ~ p(X58)
| ~ p(X60)
| p(X56) ) ).
cnf(u45994,axiom,
( p(sK56(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X1)
| ~ p(X7)
| ~ p(X0)
| p(sK66(X0,X1,X2,X3,X4,X5,X6,X7))
| ~ p(X3)
| p(X5)
| p(X6) ) ).
cnf(u23766,axiom,
( ~ p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X56)
| ~ p(X62)
| p(X63)
| ~ p(X60)
| ~ p(X58)
| p(X59) ) ).
cnf(u13178,axiom,
( p(sK66(X56,X57,X58,X59,X60,X61,X62,X63))
| p(X62)
| p(X56)
| ~ p(X63)
| p(X61)
| p(X59)
| ~ p(X57)
| ~ p(X58) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV079+1 : TPTP v9.3.1. Bugfixed v5.5.1.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n006.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 11:21:55 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.16/0.42 Running first-order theorem proving
% 0.16/0.42 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
% 12.54/2.73 % (2820052)Detected formulas, will run a generic FOF schedule.
% 12.54/2.73 % (2820121)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2385210337:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.54/2.73 % (2820118)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=6099578:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.54/2.73 % (2820123)dis-21_1_sil=8000:lcm=predicate:random_seed=3252716582: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)
% 12.54/2.73 % (2820122)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2565418694:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.54/2.73 % (2820119)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=1205063262:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.54/2.73 % (2820121)Refutation not found, incomplete strategy
% 12.54/2.73 % (2820121)------------------------------
% 12.54/2.73 % (2820121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.54/2.73 % (2820121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.73 % (2820121)CaDiCaL version: 2.1.3
% 12.54/2.73 % (2820121)Termination reason: Refutation not found, incomplete strategy
% 12.54/2.73 % (2820121)Time elapsed: 0.001 s
% 12.54/2.73 % (2820121)Peak memory usage: 86 MB
% 12.54/2.73 % (2820121)Instructions burned: 1 (million)
% 12.54/2.73 % (2820120)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=283195036:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.54/2.73 % (2820120)Refutation not found, incomplete strategy
% 12.54/2.73 % (2820120)------------------------------
% 12.54/2.73 % (2820120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.54/2.73 % (2820120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.73 % (2820120)CaDiCaL version: 2.1.3
% 12.54/2.73 % (2820120)Termination reason: Refutation not found, incomplete strategy
% 12.54/2.73 % (2820120)Time elapsed: 0.001 s
% 12.54/2.73 % (2820120)Peak memory usage: 87 MB
% 12.54/2.73 % (2820120)Instructions burned: 1 (million)
% 12.54/2.73 % (2820117)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=2224901024:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.54/2.73 % (2820123)Instruction limit reached!
% 12.54/2.73 % (2820123)------------------------------
% 12.54/2.73 % (2820123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.54/2.73 % (2820123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.73 % (2820123)CaDiCaL version: 2.1.3
% 12.54/2.73 % (2820123)Termination reason: Instruction limit
% 12.54/2.73 % (2820123)Termination phase: Saturation
% 12.54/2.73 % (2820123)Time elapsed: 0.065 s
% 12.54/2.73 % (2820123)Peak memory usage: 90 MB
% 12.54/2.73 % (2820123)Instructions burned: 130 (million)
% 12.54/2.73 % (2820122)Instruction limit reached!
% 12.54/2.73 % (2820122)------------------------------
% 12.54/2.73 % (2820122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.54/2.73 % (2820122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.73 % (2820122)CaDiCaL version: 2.1.3
% 12.54/2.73 % (2820122)Termination reason: Instruction limit
% 12.54/2.73 % (2820122)Termination phase: Saturation
% 12.54/2.73 % (2820122)Time elapsed: 0.069 s
% 12.54/2.73 % (2820122)Peak memory usage: 90 MB
% 12.54/2.73 % (2820122)Instructions burned: 139 (million)
% 12.54/2.73 % (2820120)------------------------------
% 12.54/2.73 % (2820120)------------------------------
% 12.54/2.73 % (2820172)lrs+10_1_sil=8000:sp=occurrence:random_seed=4229271905:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 12.54/2.73 % (2820172)Refutation not found, incomplete strategy
% 12.54/2.73 % (2820172)------------------------------
% 12.54/2.73 % (2820172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.54/2.73 % (2820172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.73 % (2820172)CaDiCaL version: 2.1.3
% 12.54/2.73 % (2820172)Termination reason: Refutation not found, incomplete strategy
% 12.54/2.73 % (2820172)Time elapsed: 0.001 s
% 12.54/2.73 % (2820172)Peak memory usage: 87 MB
% 13.55/2.87 % (2820172)Instructions burned: 1 (million)
% 13.55/2.87 % (2820121)------------------------------
% 13.55/2.87 % (2820121)------------------------------
% 13.55/2.87 % (2820173)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2499632176:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 13.55/2.87 % (2820173)Refutation not found, incomplete strategy
% 13.55/2.87 % (2820173)------------------------------
% 13.55/2.87 % (2820173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.55/2.87 % (2820173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.55/2.87 % (2820173)CaDiCaL version: 2.1.3
% 13.55/2.87 % (2820173)Termination reason: Refutation not found, incomplete strategy
% 13.55/2.87 % (2820173)Time elapsed: 0.003 s
% 13.55/2.87 % (2820173)Peak memory usage: 87 MB
% 13.55/2.87 % (2820173)Instructions burned: 5 (million)
% 13.55/2.87 % (2820174)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1555237330:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 13.55/2.87 % (2820174)Refutation not found, incomplete strategy
% 13.55/2.87 % (2820174)------------------------------
% 13.55/2.87 % (2820174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.55/2.87 % (2820174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.55/2.87 % (2820174)CaDiCaL version: 2.1.3
% 13.55/2.87 % (2820174)Termination reason: Refutation not found, incomplete strategy
% 13.55/2.87 % (2820174)Time elapsed: 0.001 s
% 13.55/2.87 % (2820174)Peak memory usage: 87 MB
% 13.55/2.87 % (2820174)Instructions burned: 1 (million)
% 13.55/2.87 % (2820174)------------------------------
% 13.55/2.87 % (2820174)------------------------------
% 13.55/2.87 % (2820183)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=1433649946:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 13.55/2.87 % (2820172)------------------------------
% 13.55/2.87 % (2820172)------------------------------
% 13.55/2.87 % (2820173)------------------------------
% 13.55/2.87 % (2820173)------------------------------
% 13.55/2.87 % (2820215)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1675755484:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi)
% 13.55/2.87 % (2820215)Refutation not found, incomplete strategy
% 13.55/2.87 % (2820215)------------------------------
% 13.55/2.87 % (2820215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.55/2.87 % (2820215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.55/2.87 % (2820215)CaDiCaL version: 2.1.3
% 13.55/2.87 % (2820215)Termination reason: Refutation not found, incomplete strategy
% 13.55/2.87 % (2820215)Time elapsed: 0.001 s
% 13.55/2.87 % (2820215)Peak memory usage: 86 MB
% 13.55/2.87 % (2820215)Instructions burned: 2 (million)
% 13.55/2.87 % (2820183)Instruction limit reached!
% 13.55/2.87 % (2820183)------------------------------
% 13.55/2.87 % (2820183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.55/2.87 % (2820183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.55/2.87 % (2820183)CaDiCaL version: 2.1.3
% 13.55/2.87 % (2820183)Termination reason: Instruction limit
% 13.55/2.87 % (2820183)Termination phase: Saturation
% 13.55/2.87 % (2820183)Time elapsed: 0.213 s
% 13.55/2.87 % (2820183)Peak memory usage: 100 MB
% 13.55/2.87 % (2820183)Instructions burned: 248 (million)
% 13.55/2.87 % (2820119)Refutation not found, incomplete strategy
% 13.55/2.87 % (2820119)------------------------------
% 13.55/2.87 % (2820119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.55/2.87 % (2820119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.55/2.87 % (2820119)CaDiCaL version: 2.1.3
% 13.55/2.87 % (2820119)Termination reason: Refutation not found, incomplete strategy
% 13.55/2.87 % (2820119)Time elapsed: 0.835 s
% 13.55/2.87 % (2820119)Peak memory usage: 138 MB
% 13.55/2.87 % (2820119)Instructions burned: 990 (million)
% 13.55/2.87 % (2820217)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=443709908:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 13.55/2.87 % (2820219)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=641645932:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 13.55/2.87 % (2820219)Refutation not found, incomplete strategy
% 13.55/2.87 % (2820219)------------------------------
% 13.55/2.87 % (2820219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.31/3.69 % (2820219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.31/3.69 % (2820219)CaDiCaL version: 2.1.3
% 20.31/3.69 % (2820219)Termination reason: Refutation not found, incomplete strategy
% 20.31/3.69 % (2820219)Time elapsed: 0.040 s
% 20.31/3.69 % (2820219)Peak memory usage: 89 MB
% 20.31/3.69 % (2820219)Instructions burned: 47 (million)
% 20.31/3.69 % (2820215)------------------------------
% 20.31/3.69 % (2820215)------------------------------
% 20.31/3.69 % (2820225)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1884139234:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 20.31/3.69 % (2820225)Refutation not found, incomplete strategy
% 20.31/3.69 % (2820225)------------------------------
% 20.31/3.69 % (2820225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.31/3.69 % (2820225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.31/3.69 % (2820225)CaDiCaL version: 2.1.3
% 20.31/3.69 % (2820225)Termination reason: Refutation not found, incomplete strategy
% 20.31/3.69 % (2820225)Time elapsed: 0.092 s
% 20.31/3.69 % (2820225)Peak memory usage: 89 MB
% 20.31/3.69 % (2820225)Instructions burned: 110 (million)
% 20.31/3.69 % (2820228)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1764349644:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2988 on theBenchmark for (2988ds/114Mi)
% 20.31/3.69 % (2820228)Refutation not found, incomplete strategy
% 20.31/3.69 % (2820228)------------------------------
% 20.31/3.69 % (2820228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.31/3.69 % (2820228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.31/3.69 % (2820228)CaDiCaL version: 2.1.3
% 20.31/3.69 % (2820228)Termination reason: Refutation not found, incomplete strategy
% 20.31/3.69 % (2820228)Time elapsed: 0.003 s
% 20.31/3.69 % (2820228)Peak memory usage: 88 MB
% 20.31/3.69 % (2820228)Instructions burned: 7 (million)
% 20.31/3.69 % (2820119)------------------------------
% 20.31/3.69 % (2820119)------------------------------
% 20.31/3.69 % (2820219)------------------------------
% 20.31/3.69 % (2820219)------------------------------
% 20.31/3.69 % (2820228)------------------------------
% 20.31/3.69 % (2820228)------------------------------
% 20.31/3.69 % (2820225)------------------------------
% 20.31/3.69 % (2820225)------------------------------
% 20.31/3.69 % (2820239)lrs+10_1_sil=8000:sp=occurrence:random_seed=4114639624:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 20.31/3.69 % (2820239)Refutation not found, incomplete strategy
% 20.31/3.69 % (2820239)------------------------------
% 20.31/3.69 % (2820239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.31/3.69 % (2820239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.31/3.69 % (2820239)CaDiCaL version: 2.1.3
% 20.31/3.69 % (2820239)Termination reason: Refutation not found, incomplete strategy
% 20.31/3.69 % (2820239)Time elapsed: 0.002 s
% 20.31/3.69 % (2820239)Peak memory usage: 86 MB
% 20.31/3.69 % (2820239)Instructions burned: 1 (million)
% 20.31/3.69 % (2820241)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3638581304:i=5202:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/5202Mi)
% 20.31/3.69 % (2820240)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2968819285:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 20.31/3.69 % (2820240)Refutation not found, incomplete strategy
% 20.31/3.69 % (2820240)------------------------------
% 20.31/3.69 % (2820240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.31/3.69 % (2820240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.31/3.69 % (2820240)CaDiCaL version: 2.1.3
% 20.31/3.69 % (2820240)Termination reason: Refutation not found, incomplete strategy
% 20.31/3.69 % (2820240)Time elapsed: 0.043 s
% 20.31/3.69 % (2820240)Peak memory usage: 89 MB
% 20.31/3.69 % (2820240)Instructions burned: 49 (million)
% 20.31/3.69 % (2820244)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4011112419:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2983 on theBenchmark for (2983ds/134Mi)
% 20.31/3.69 [W927 11:21:57.453814999 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.
% 20.31/3.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.72/3.73 [W927 11:21:57.453843320 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.
% 20.72/3.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.72/3.73 [W927 11:21:57.453865259 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.
% 20.72/3.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.72/3.73 [W927 11:21:57.453871395 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.
% 20.72/3.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.72/3.73 [W927 11:21:57.453884937 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.
% 20.72/3.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.72/3.73 [W927 11:21:57.453890300 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.
% 20.72/3.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.72/3.73 [W927 11:21:57.453904403 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.
% 20.72/3.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.72/3.73 [W927 11:21:57.453910202 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.
% 20.72/3.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.72/3.73 [W927 11:21:57.453922982 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.
% 20.72/3.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.72/3.73 [W927 11:21:57.453928610 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.
% 20.72/3.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.72/3.73 [W927 11:21:57.453941412 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.
% 20.72/3.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.72/3.73 [W927 11:21:57.453946768 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.
% 20.72/3.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.72/3.73 % (2820239)------------------------------
% 20.72/3.73 % (2820239)------------------------------
% 20.72/3.73 % (2820244)Instruction limit reached!
% 20.72/3.73 % (2820244)------------------------------
% 20.72/3.73 % (2820244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.72/3.73 % (2820244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.72/3.73 % (2820244)CaDiCaL version: 2.1.3
% 20.72/3.73 % (2820244)Termination reason: Instruction limit
% 20.72/3.73 % (2820244)Termination phase: Saturation
% 20.72/3.73 % (2820244)Time elapsed: 0.114 s
% 20.72/3.73 % (2820244)Peak memory usage: 93 MB
% 20.72/3.73 % (2820244)Instructions burned: 135 (million)
% 20.72/3.73 % (2820241)Refutation not found, incomplete strategy
% 26.53/4.69 % (2820241)------------------------------
% 26.53/4.69 % (2820241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/4.69 % (2820241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/4.69 % (2820241)CaDiCaL version: 2.1.3
% 26.53/4.69 % (2820241)Termination reason: Refutation not found, incomplete strategy
% 26.53/4.69 % (2820241)Time elapsed: 0.435 s
% 26.53/4.69 % (2820241)Peak memory usage: 126 MB
% 26.53/4.69 % (2820241)Instructions burned: 825 (million)
% 26.53/4.69 % (2820240)------------------------------
% 26.53/4.69 % (2820240)------------------------------
% 26.53/4.69 % (2820257)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1496703886:st=8:i=592:sd=3:ep=RST:ss=axioms_2979 on theBenchmark for (2979ds/592Mi)
% 26.53/4.69 % (2820257)Refutation not found, incomplete strategy
% 26.53/4.69 % (2820257)------------------------------
% 26.53/4.69 % (2820257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/4.69 % (2820257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/4.69 % (2820257)CaDiCaL version: 2.1.3
% 26.53/4.69 % (2820257)Termination reason: Refutation not found, incomplete strategy
% 26.53/4.69 % (2820257)Time elapsed: 0.003 s
% 26.53/4.69 % (2820257)Peak memory usage: 87 MB
% 26.53/4.69 % (2820257)Instructions burned: 2 (million)
% 26.53/4.69 % (2820258)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=149304991:st=3:i=13193:sd=3:ss=axioms_2978 on theBenchmark for (2978ds/13193Mi)
% 26.53/4.69 % (2820241)------------------------------
% 26.53/4.69 % (2820241)------------------------------
% 26.53/4.69 % (2820261)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=2224701756:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/125Mi)
% 26.53/4.69 % (2820261)Refutation not found, incomplete strategy
% 26.53/4.69 % (2820261)------------------------------
% 26.53/4.69 % (2820261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/4.69 % (2820261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/4.69 % (2820261)CaDiCaL version: 2.1.3
% 26.53/4.69 % (2820261)Termination reason: Refutation not found, incomplete strategy
% 26.53/4.69 % (2820261)Time elapsed: 0.004 s
% 26.53/4.69 % (2820261)Peak memory usage: 88 MB
% 26.53/4.69 % (2820261)Instructions burned: 7 (million)
% 26.53/4.69 % (2820267)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1653311162:i=134:gtgl=5:slsql=off:gtg=exists_sym_2975 on theBenchmark for (2975ds/134Mi)
% 26.53/4.69 % (2820257)------------------------------
% 26.53/4.69 % (2820257)------------------------------
% 26.53/4.69 % (2820267)Instruction limit reached!
% 26.53/4.69 % (2820267)------------------------------
% 26.53/4.69 % (2820267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/4.69 % (2820267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/4.69 % (2820267)CaDiCaL version: 2.1.3
% 26.53/4.69 % (2820267)Termination reason: Instruction limit
% 26.53/4.69 % (2820267)Termination phase: Saturation
% 26.53/4.69 % (2820267)Time elapsed: 0.057 s
% 26.53/4.69 % (2820267)Peak memory usage: 89 MB
% 26.53/4.69 % (2820267)Instructions burned: 134 (million)
% 26.53/4.69 % (2820261)------------------------------
% 26.53/4.69 % (2820261)------------------------------
% 26.53/4.69 % (2820270)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=169426819:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2972 on theBenchmark for (2972ds/431Mi)
% 26.53/4.69 % (2820270)Refutation not found, incomplete strategy
% 26.53/4.69 % (2820270)------------------------------
% 26.53/4.69 % (2820270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/4.69 % (2820270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/4.69 % (2820270)CaDiCaL version: 2.1.3
% 26.53/4.69 % (2820270)Termination reason: Refutation not found, incomplete strategy
% 26.53/4.69 % (2820270)Time elapsed: 0.001 s
% 26.53/4.69 % (2820270)Peak memory usage: 86 MB
% 26.53/4.69 % (2820270)Instructions burned: 1 (million)
% 26.53/4.69 % (2820269)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1173605186:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/141Mi)
% 26.53/4.69 % (2820269)Refutation not found, incomplete strategy
% 26.53/4.69 % (2820269)------------------------------
% 26.53/4.69 % (2820269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.47/6.71 % (2820269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.47/6.71 % (2820269)CaDiCaL version: 2.1.3
% 42.47/6.71 % (2820269)Termination reason: Refutation not found, incomplete strategy
% 42.47/6.71 % (2820269)Time elapsed: 0.002 s
% 42.47/6.71 % (2820269)Peak memory usage: 87 MB
% 42.47/6.71 % (2820269)Instructions burned: 1 (million)
% 42.47/6.71 [W927 11:21:59.462452428 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.
% 42.47/6.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 42.47/6.71 [W927 11:21:59.462497018 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.
% 42.47/6.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 42.47/6.71 [W927 11:21:59.462550965 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.
% 42.47/6.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 42.47/6.71 [W927 11:21:59.462569702 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.
% 42.47/6.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 42.47/6.71 [W927 11:21:59.462610515 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.
% 42.47/6.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 42.47/6.71 [W927 11:21:59.462628658 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.
% 42.47/6.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 42.47/6.71 [W927 11:21:59.462669898 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.
% 42.47/6.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 42.47/6.71 [W927 11:21:59.462687692 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.
% 42.47/6.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 42.47/6.71 [W927 11:21:59.462727752 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.
% 42.47/6.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 42.47/6.71 [W927 11:21:59.462745422 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.
% 42.47/6.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 42.47/6.71 [W927 11:21:59.462786265 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.
% 42.47/6.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 42.47/6.71 [W927 11:21:59.462803959 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.
% 42.47/6.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 49.07/7.61 % (2820271)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=3957742316:i=6060:aac=none:ins=25_2971 on theBenchmark for (2971ds/6060Mi)
% 49.07/7.61 % (2820270)------------------------------
% 49.07/7.61 % (2820270)------------------------------
% 49.07/7.61 % (2820258)Refutation not found, incomplete strategy
% 49.07/7.61 % (2820258)------------------------------
% 49.07/7.61 % (2820258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.07/7.61 % (2820258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.07/7.61 % (2820258)CaDiCaL version: 2.1.3
% 49.07/7.61 % (2820258)Termination reason: Refutation not found, incomplete strategy
% 49.07/7.61 % (2820258)Time elapsed: 0.900 s
% 49.07/7.61 % (2820258)Peak memory usage: 125 MB
% 49.07/7.61 % (2820258)Instructions burned: 828 (million)
% 49.07/7.61 % (2820269)------------------------------
% 49.07/7.61 % (2820269)------------------------------
% 49.07/7.61 % (2820217)Instruction limit reached!
% 49.07/7.61 % (2820217)------------------------------
% 49.07/7.61 % (2820217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.07/7.61 % (2820217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.07/7.61 % (2820217)CaDiCaL version: 2.1.3
% 49.07/7.61 % (2820217)Termination reason: Instruction limit
% 49.07/7.61 % (2820217)Termination phase: Saturation
% 49.07/7.61 % (2820217)Time elapsed: 2.375 s
% 49.07/7.61 % (2820217)Peak memory usage: 142 MB
% 49.07/7.61 % (2820217)Instructions burned: 2351 (million)
% 49.07/7.61 % (2820275)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=1760676348:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2968 on theBenchmark for (2968ds/150Mi)
% 49.07/7.61 % (2820275)Instruction limit reached!
% 49.07/7.61 % (2820275)------------------------------
% 49.07/7.61 % (2820275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.07/7.61 % (2820275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.07/7.61 % (2820275)CaDiCaL version: 2.1.3
% 49.07/7.61 % (2820275)Termination reason: Instruction limit
% 49.07/7.61 % (2820275)Termination phase: Saturation
% 49.07/7.61 % (2820275)Time elapsed: 0.059 s
% 49.07/7.61 % (2820275)Peak memory usage: 89 MB
% 49.07/7.61 % (2820275)Instructions burned: 151 (million)
% 49.07/7.61 % (2820280)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2343853476:i=14155:bd=all_2965 on theBenchmark for (2965ds/14155Mi)
% 49.07/7.61 % (2820282)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=636203540:i=667:av=off:fsr=off_2965 on theBenchmark for (2965ds/667Mi)
% 49.07/7.61 % (2820283)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=3454640977:s2a=on:i=185:s2at=1.8:fdi=4_2965 on theBenchmark for (2965ds/185Mi)
% 49.07/7.61 % (2820282)Refutation not found, incomplete strategy
% 49.07/7.61 % (2820282)------------------------------
% 49.07/7.61 % (2820282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.07/7.61 % (2820282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.07/7.61 % (2820282)CaDiCaL version: 2.1.3
% 49.07/7.61 % (2820282)Termination reason: Refutation not found, incomplete strategy
% 49.07/7.61 % (2820282)Time elapsed: 0.039 s
% 49.07/7.61 % (2820282)Peak memory usage: 89 MB
% 49.07/7.61 % (2820282)Instructions burned: 43 (million)
% 49.07/7.61 % (2820258)------------------------------
% 49.07/7.61 % (2820258)------------------------------
% 49.07/7.61 % (2820283)Instruction limit reached!
% 49.07/7.61 % (2820283)------------------------------
% 49.07/7.61 % (2820283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.07/7.61 % (2820283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.07/7.61 % (2820283)CaDiCaL version: 2.1.3
% 49.07/7.61 % (2820283)Termination reason: Instruction limit
% 49.07/7.61 % (2820283)Termination phase: Saturation
% 49.07/7.61 % (2820283)Time elapsed: 0.080 s
% 49.07/7.61 % (2820283)Peak memory usage: 92 MB
% 49.07/7.61 % (2820283)Instructions burned: 187 (million)
% 49.07/7.61 % (2820288)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1614303268:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2962 on theBenchmark for (2962ds/4850Mi)
% 60.24/9.26 % (2820287)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1159345055:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2962 on theBenchmark for (2962ds/193Mi)
% 60.24/9.26 % (2820287)Refutation not found, incomplete strategy
% 60.24/9.26 % (2820287)------------------------------
% 60.24/9.26 % (2820287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.24/9.26 % (2820287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.24/9.26 % (2820287)CaDiCaL version: 2.1.3
% 60.24/9.26 % (2820287)Termination reason: Refutation not found, incomplete strategy
% 60.24/9.26 % (2820287)Time elapsed: 0.003 s
% 60.24/9.26 % (2820287)Peak memory usage: 86 MB
% 60.24/9.26 % (2820288)Refutation not found, incomplete strategy
% 60.24/9.26 % (2820288)------------------------------
% 60.24/9.26 % (2820288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.24/9.26 % (2820287)Instructions burned: 3 (million)
% 60.24/9.26 % (2820288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.24/9.26 % (2820288)CaDiCaL version: 2.1.3
% 60.24/9.26 % (2820288)Termination reason: Refutation not found, incomplete strategy
% 60.24/9.26 % (2820288)Time elapsed: 0.014 s
% 60.24/9.26 % (2820288)Peak memory usage: 89 MB
% 60.24/9.26 % (2820288)Instructions burned: 52 (million)
% 60.24/9.26 % (2820282)------------------------------
% 60.24/9.26 % (2820282)------------------------------
% 60.24/9.26 % (2820288)------------------------------
% 60.24/9.26 % (2820288)------------------------------
% 60.24/9.26 % (2820293)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1490956626:i=12111:sd=1:ss=included_2958 on theBenchmark for (2958ds/12111Mi)
% 60.24/9.26 % (2820287)------------------------------
% 60.24/9.26 % (2820287)------------------------------
% 60.24/9.26 % (2820294)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1228123115:i=319:kws=precedence:fsr=off_2957 on theBenchmark for (2957ds/319Mi)
% 60.24/9.26 % (2820294)Instruction limit reached!
% 60.24/9.26 % (2820294)------------------------------
% 60.24/9.26 % (2820294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.24/9.26 % (2820294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.24/9.26 % (2820294)CaDiCaL version: 2.1.3
% 60.24/9.26 % (2820294)Termination reason: Instruction limit
% 60.24/9.26 % (2820294)Termination phase: Saturation
% 60.24/9.26 % (2820294)Time elapsed: 0.130 s
% 60.24/9.26 % (2820294)Peak memory usage: 90 MB
% 60.24/9.26 % (2820294)Instructions burned: 320 (million)
% 60.24/9.26 % (2820296)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3128798937:i=2064:ep=RST_2955 on theBenchmark for (2955ds/2064Mi)
% 60.24/9.26 % (2820296)Refutation not found, incomplete strategy
% 60.24/9.26 % (2820296)------------------------------
% 60.24/9.26 % (2820296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.24/9.26 % (2820296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.24/9.26 % (2820296)CaDiCaL version: 2.1.3
% 60.24/9.26 % (2820296)Termination reason: Refutation not found, incomplete strategy
% 60.24/9.26 % (2820296)Time elapsed: 0.048 s
% 60.24/9.26 % (2820296)Peak memory usage: 89 MB
% 60.24/9.26 % (2820296)Instructions burned: 56 (million)
% 60.24/9.26 % (2820298)dis-1011_128_sil=32000:random_seed=2482037444:i=3706:ep=RST:av=off_2953 on theBenchmark for (2953ds/3706Mi)
% 60.24/9.26 % (2820296)------------------------------
% 60.24/9.26 % (2820296)------------------------------
% 60.24/9.26 % (2820301)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3059120282:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2948 on theBenchmark for (2948ds/757Mi)
% 60.24/9.26 % (2820301)Refutation not found, incomplete strategy
% 60.24/9.26 % (2820301)------------------------------
% 60.24/9.26 % (2820301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.24/9.26 % (2820301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.24/9.26 % (2820301)CaDiCaL version: 2.1.3
% 60.24/9.26 % (2820301)Termination reason: Refutation not found, incomplete strategy
% 60.24/9.26 % (2820301)Time elapsed: 0.002 s
% 60.24/9.26 % (2820301)Peak memory usage: 87 MB
% 60.24/9.26 % (2820301)Instructions burned: 1 (million)
% 60.24/9.26 % (2820301)------------------------------
% 60.24/9.26 % (2820301)------------------------------
% 60.24/9.26 % (2820305)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2099796394:i=13913:ss=axioms:sgt=8_2942 on theBenchmark for (2942ds/13913Mi)
% 60.84/9.40 [W927 11:22:02.072857772 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.
% 60.84/9.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.84/9.40 [W927 11:22:02.072984418 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.
% 60.84/9.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.84/9.40 [W927 11:22:02.073095279 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.
% 60.84/9.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.84/9.40 [W927 11:22:02.073149472 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.
% 60.84/9.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.84/9.40 [W927 11:22:02.073224232 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.
% 60.84/9.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.84/9.40 [W927 11:22:02.073272965 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.
% 60.84/9.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.84/9.40 [W927 11:22:02.073357742 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.
% 60.84/9.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.84/9.40 [W927 11:22:02.073405249 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.
% 60.84/9.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.84/9.40 [W927 11:22:02.073475842 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.
% 60.84/9.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.84/9.40 [W927 11:22:02.073523532 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.
% 60.84/9.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.84/9.40 [W927 11:22:02.073593956 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.
% 60.84/9.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.84/9.40 [W927 11:22:02.073641262 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.
% 60.84/9.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.84/9.40 % (2820305)Refutation not found, incomplete strategy
% 60.84/9.40 % (2820305)------------------------------
% 60.84/9.40 % (2820305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.74/10.71 % (2820305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.74/10.71 % (2820305)CaDiCaL version: 2.1.3
% 70.74/10.71 % (2820305)Termination reason: Refutation not found, incomplete strategy
% 70.74/10.71 % (2820305)Time elapsed: 0.901 s
% 70.74/10.71 % (2820305)Peak memory usage: 125 MB
% 70.74/10.71 % (2820305)Instructions burned: 824 (million)
% 70.74/10.71 % (2820305)------------------------------
% 70.74/10.71 % (2820305)------------------------------
% 70.74/10.71 % (2820298)Instruction limit reached!
% 70.74/10.71 % (2820298)------------------------------
% 70.74/10.71 % (2820298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.74/10.71 % (2820298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.74/10.71 % (2820298)CaDiCaL version: 2.1.3
% 70.74/10.71 % (2820298)Termination reason: Instruction limit
% 70.74/10.71 % (2820298)Termination phase: Saturation
% 70.74/10.71 % (2820298)Time elapsed: 2.444 s
% 70.74/10.71 % (2820298)Peak memory usage: 91 MB
% 70.74/10.71 % (2820298)Instructions burned: 3707 (million)
% 70.74/10.71 % (2820308)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1464385985:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2926 on theBenchmark for (2926ds/2479Mi)
% 70.74/10.71 % (2820307)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=311177121:i=9925:aac=none_2926 on theBenchmark for (2926ds/9925Mi)
% 70.74/10.71 % (2820308)Refutation not found, incomplete strategy
% 70.74/10.71 % (2820308)------------------------------
% 70.74/10.71 % (2820308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.74/10.71 % (2820308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.74/10.71 % (2820308)CaDiCaL version: 2.1.3
% 70.74/10.71 % (2820308)Termination reason: Refutation not found, incomplete strategy
% 70.74/10.71 % (2820308)Time elapsed: 0.003 s
% 70.74/10.71 % (2820308)Peak memory usage: 87 MB
% 70.74/10.71 % (2820308)Instructions burned: 3 (million)
% 70.74/10.71 % (2820271)Instruction limit reached!
% 70.74/10.71 % (2820271)------------------------------
% 70.74/10.71 % (2820271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.74/10.71 % (2820271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.74/10.71 % (2820271)CaDiCaL version: 2.1.3
% 70.74/10.71 % (2820271)Termination reason: Instruction limit
% 70.74/10.71 % (2820271)Termination phase: Saturation
% 70.74/10.71 % (2820271)Time elapsed: 4.732 s
% 70.74/10.71 % (2820271)Peak memory usage: 141 MB
% 70.74/10.71 % (2820271)Instructions burned: 6060 (million)
% 70.74/10.71 % (2820308)------------------------------
% 70.74/10.71 % (2820308)------------------------------
% 70.74/10.71 % (2820317)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=65354973:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2921 on theBenchmark for (2921ds/440Mi)
% 70.74/10.71 % (2820319)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2833366367:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2919 on theBenchmark for (2919ds/11145Mi)
% 70.74/10.71 % (2820317)Instruction limit reached!
% 70.74/10.71 % (2820317)------------------------------
% 70.74/10.71 % (2820317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.74/10.71 % (2820317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.74/10.71 % (2820317)CaDiCaL version: 2.1.3
% 70.74/10.71 % (2820317)Termination reason: Instruction limit
% 70.74/10.71 % (2820317)Termination phase: Saturation
% 70.74/10.71 % (2820317)Time elapsed: 0.305 s
% 70.74/10.71 % (2820317)Peak memory usage: 90 MB
% 70.74/10.71 % (2820317)Instructions burned: 442 (million)
% 70.74/10.71 % (2820322)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=3606516038:cts=off:i=3034:av=off:er=known:fsd=on_2916 on theBenchmark for (2916ds/3034Mi)
% 70.74/10.71 % (2820307)Refutation not found, incomplete strategy
% 70.74/10.71 % (2820307)------------------------------
% 70.74/10.71 % (2820307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.74/10.71 % (2820307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.74/10.71 % (2820307)CaDiCaL version: 2.1.3
% 70.74/10.71 % (2820307)Termination reason: Refutation not found, incomplete strategy
% 70.74/10.71 % (2820307)Time elapsed: 0.908 s
% 70.74/10.71 % (2820307)Peak memory usage: 137 MB
% 70.74/10.71 % (2820307)Instructions burned: 967 (million)
% 70.74/10.71 % (2820117)Refutation not found, incomplete strategy
% 63.64/11.23 % (2820117)------------------------------
% 63.64/11.23 % (2820117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.64/11.23 % (2820117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.64/11.23 % (2820117)CaDiCaL version: 2.1.3
% 63.64/11.23 % (2820117)Termination reason: Refutation not found, incomplete strategy
% 63.64/11.23 % (2820117)Time elapsed: 8.383 s
% 63.64/11.23 % (2820117)Peak memory usage: 188 MB
% 63.64/11.23 % (2820117)Instructions burned: 8896 (million)
% 63.64/11.23 [W927 11:22:04.124611937 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.
% 63.64/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.64/11.23 [W927 11:22:04.124657187 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.
% 63.64/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.64/11.23 [W927 11:22:04.124695064 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.
% 63.64/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.64/11.23 [W927 11:22:04.124711591 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.
% 63.64/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.64/11.23 [W927 11:22:04.124736971 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.
% 63.64/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.64/11.23 [W927 11:22:04.124748624 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.
% 63.64/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.64/11.23 [W927 11:22:04.124775404 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.
% 63.64/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.64/11.23 [W927 11:22:04.124787811 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.
% 63.64/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.64/11.23 [W927 11:22:04.124812444 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.
% 63.64/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.64/11.23 [W927 11:22:04.124824221 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.
% 63.64/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.64/11.23 [W927 11:22:04.124849154 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.
% 63.64/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.64/11.23 [W927 11:22:04.124860598 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.
% 63.64/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.64/11.23 % (2820307)------------------------------
% 63.64/11.23 % (2820307)------------------------------
% 63.64/11.23 % (2820117)------------------------------
% 63.64/11.23 % (2820117)------------------------------
% 63.64/11.23 % (2820319)Refutation not found, incomplete strategy
% 63.64/11.23 % (2820319)------------------------------
% 63.64/11.23 % (2820319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.64/11.23 % (2820319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.64/11.23 % (2820319)CaDiCaL version: 2.1.3
% 63.64/11.23 % (2820319)Termination reason: Refutation not found, incomplete strategy
% 63.64/11.23 % (2820319)Time elapsed: 0.556 s
% 63.64/11.23 % (2820319)Peak memory usage: 126 MB
% 63.64/11.23 % (2820319)Instructions burned: 826 (million)
% 63.64/11.23 % (2820429)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3502963677:st=2:s2a=on:i=524:s2at=2:ss=axioms_2912 on theBenchmark for (2912ds/524Mi)
% 63.64/11.23 % (2820429)Refutation not found, incomplete strategy
% 63.64/11.24 % (2820429)------------------------------
% 63.64/11.24 % (2820429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.64/11.24 % (2820429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.64/11.24 % (2820429)CaDiCaL version: 2.1.3
% 63.64/11.24 % (2820429)Termination reason: Refutation not found, incomplete strategy
% 63.64/11.24 % (2820429)Time elapsed: 0.002 s
% 63.64/11.24 % (2820429)Peak memory usage: 87 MB
% 63.64/11.24 % (2820429)Instructions burned: 5 (million)
% 63.64/11.24 % (2820430)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1529326009:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2911 on theBenchmark for (2911ds/1016Mi)
% 63.64/11.24 % (2820430)Refutation not found, incomplete strategy
% 63.64/11.24 % (2820430)------------------------------
% 63.64/11.24 % (2820430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.64/11.24 % (2820430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.64/11.24 % (2820430)CaDiCaL version: 2.1.3
% 63.64/11.24 % (2820430)Termination reason: Refutation not found, incomplete strategy
% 63.64/11.24 % (2820430)Time elapsed: 0.001 s
% 63.64/11.24 % (2820430)Peak memory usage: 87 MB
% 63.64/11.24 % (2820430)Instructions burned: 1 (million)
% 63.64/11.24 % (2820319)------------------------------
% 63.64/11.24 % (2820319)------------------------------
% 63.64/11.24 % (2820429)------------------------------
% 63.64/11.24 % (2820429)------------------------------
% 63.64/11.24 % (2820430)------------------------------
% 63.64/11.24 % (2820430)------------------------------
% 63.64/11.24 % (2820480)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2813846181:i=14123:bd=preordered:ins=4_2908 on theBenchmark for (2908ds/14123Mi)
% 63.64/11.24 % (2820481)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=7662051:i=5781:kws=precedence:bd=all:rawr=on_2908 on theBenchmark for (2908ds/5781Mi)
% 63.64/11.24 % (2820482)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=3976409568:i=2448:gtgl=5:bd=preordered:gtg=all_2907 on theBenchmark for (2907ds/2448Mi)
% 63.64/11.24 % (2820280)Instruction limit reached!
% 63.64/11.24 % (2820280)------------------------------
% 63.64/11.24 % (2820280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.64/11.24 % (2820280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.64/11.24 % (2820280)CaDiCaL version: 2.1.3
% 63.64/11.24 % (2820280)Termination reason: Instruction limit
% 63.64/11.24 % (2820280)Termination phase: Saturation
% 63.64/11.24 % (2820280)Time elapsed: 6.036 s
% 63.64/11.24 % (2820280)Peak memory usage: 471 MB
% 63.64/11.24 % (2820280)Instructions burned: 14159 (million)
% 63.64/11.24 % (2820486)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3900922456:i=3223:kws=precedence:fgj=on:av=off_2902 on theBenchmark for (2902ds/3223Mi)
% 63.64/11.24 % (2820322)Instruction limit reached!
% 63.64/11.24 % (2820322)------------------------------
% 63.64/11.24 % (2820322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.64/11.24 % (2820322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.64/11.24 % (2820322)CaDiCaL version: 2.1.3
% 63.64/11.24 % (2820322)Termination reason: Instruction limit
% 63.64/11.24 % (2820322)Termination phase: Saturation
% 63.64/11.24 % (2820322)Time elapsed: 1.521 s
% 63.64/11.24 % (2820322)Peak memory usage: 140 MB
% 63.64/11.24 % (2820322)Instructions burned: 3035 (million)
% 63.64/11.24 % (2820481)First to succeed.
% 63.64/11.24 % (2820488)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=1225133513:st=5.6:i=2033:sd=3:ss=axioms_2899 on theBenchmark for (2899ds/2033Mi)
% 63.64/11.24 % (2820481)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2820052"
% 63.64/11.24 % SZS status Satisfiable for theBenchmark
% 63.64/11.24 % SZS output start Saturation.
% See solution above
% 74.48/11.44 % SZS output start Definitions and Model Updates.
% 74.48/11.44 % SZS output end Definitions and Model Updates.
% 74.48/11.44 % (2820481)------------------------------
% 74.48/11.44 % (2820481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.48/11.44 % (2820481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.48/11.44 % (2820481)CaDiCaL version: 2.1.3
% 74.48/11.44 % (2820481)Termination reason: Satisfiable
% 74.48/11.44 % (2820481)Time elapsed: 0.854 s
% 74.48/11.44 % (2820481)Peak memory usage: 97 MB
% 74.48/11.44 % (2820481)Instructions burned: 1612 (million)
% 74.48/11.44 % (2820481)------------------------------
% 74.48/11.44 % (2820481)------------------------------
% 74.48/11.44 % (2820052)Success in time 10.55 s
% 74.48/11.44 % Vampire exiting
%------------------------------------------------------------------------------