%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL659+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:54:23 AM UTC 2026
% Result : CounterSatisfiable 10.55s 2.37s
% Output : Saturation 11.19s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u70,negated_conjecture,
( ~ r1(sK8,X0)
| r1(X0,sK11(X0)) ) ).
cnf(u81,negated_conjecture,
( ~ r1(sK14,X0)
| r1(X0,sK11(X0)) ) ).
cnf(u86,negated_conjecture,
r1(sK12(sK14),sK15(sK12(sK14))) ).
cnf(u96,negated_conjecture,
r1(sK11(sK14),sK15(sK11(sK14))) ).
cnf(u105,negated_conjecture,
r1(sK14,sK4(sK14)) ).
cnf(u108,negated_conjecture,
( ~ r1(sK14,X0)
| ~ r1(X0,X1)
| r1(X1,sK2(X1))
| p1(X1) ) ).
cnf(u113,negated_conjecture,
r1(sK4(sK14),sK15(sK4(sK14))) ).
cnf(u116,negated_conjecture,
p1(sK4(sK14)) ).
cnf(u123,negated_conjecture,
( ~ r1(sK14,X0)
| ~ r1(X0,X1)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u134,negated_conjecture,
p1(sK15(sK14)) ).
cnf(u140,negated_conjecture,
r1(sK8,sK4(sK8)) ).
cnf(u154,negated_conjecture,
r1(sK4(sK8),sK12(sK4(sK8))) ).
cnf(u172,negated_conjecture,
r1(sK14,sK13(sK14)) ).
cnf(u179,negated_conjecture,
r1(sK15(sK14),sK13(sK15(sK14))) ).
cnf(u186,negated_conjecture,
r1(sK4(sK14),sK13(sK4(sK14))) ).
cnf(u193,negated_conjecture,
r1(sK12(sK14),sK13(sK12(sK14))) ).
cnf(u206,negated_conjecture,
r1(sK11(sK14),sK13(sK11(sK14))) ).
cnf(u222,negated_conjecture,
( ~ r1(sK14,X0)
| ~ r1(X0,X1)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u246,negated_conjecture,
r1(sK12(sK14),sK2(sK12(sK14))) ).
cnf(u253,negated_conjecture,
r1(sK13(sK12(sK14)),sK2(sK13(sK12(sK14)))) ).
cnf(u262,negated_conjecture,
r1(sK4(sK14),sK2(sK4(sK14))) ).
cnf(u267,negated_conjecture,
r1(sK15(sK14),sK2(sK15(sK14))) ).
cnf(u284,negated_conjecture,
~ r1(sK8,sK4(sK14)) ).
cnf(u291,negated_conjecture,
( ~ r1(sK12(X0),sK4(sK14))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u344,negated_conjecture,
~ r1(sK8,sK15(sK14)) ).
cnf(u351,negated_conjecture,
( ~ r1(sK12(X0),sK15(sK14))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u364,negated_conjecture,
r1(sK4(sK8),sK4(sK4(sK8))) ).
cnf(u386,negated_conjecture,
r1(sK2(sK14),sK15(sK2(sK14))) ).
cnf(u389,negated_conjecture,
p1(sK2(sK14)) ).
cnf(u393,negated_conjecture,
r1(sK2(sK14),sK13(sK2(sK14))) ).
cnf(u420,negated_conjecture,
r1(sK8,sK13(sK8)) ).
cnf(u427,negated_conjecture,
r1(sK4(sK8),sK13(sK4(sK8))) ).
cnf(u448,negated_conjecture,
r1(sK2(sK14),sK2(sK2(sK14))) ).
cnf(u455,negated_conjecture,
r1(sK11(sK2(sK14)),sK2(sK11(sK2(sK14)))) ).
cnf(u462,negated_conjecture,
r1(sK13(sK2(sK14)),sK2(sK13(sK2(sK14)))) ).
cnf(u492,negated_conjecture,
~ r1(sK8,sK2(sK14)) ).
cnf(u499,negated_conjecture,
( ~ r1(sK12(X0),sK2(sK14))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u511,negated_conjecture,
( ~ p1(X2)
| ~ r1(sK4(sK8),X2)
| p1(X3)
| ~ r1(X2,X3) ) ).
cnf(u599,negated_conjecture,
( ~ r1(sK4(sK4(sK8)),X2)
| ~ p1(X2)
| p1(X3)
| ~ r1(X2,X3) ) ).
cnf(u607,negated_conjecture,
~ p1(sK4(sK4(sK8))) ).
cnf(u2066,negated_conjecture,
~ p1(sK15(sK4(sK14))) ).
cnf(u653,negated_conjecture,
r1(sK15(sK4(sK14)),sK2(sK15(sK4(sK14)))) ).
cnf(u2053,negated_conjecture,
~ p1(sK13(sK4(sK14))) ).
cnf(u660,negated_conjecture,
r1(sK13(sK4(sK14)),sK2(sK13(sK4(sK14)))) ).
cnf(u2056,negated_conjecture,
~ p1(sK11(sK4(sK14))) ).
cnf(u667,negated_conjecture,
r1(sK11(sK4(sK14)),sK2(sK11(sK4(sK14)))) ).
cnf(u671,negated_conjecture,
p1(sK2(sK4(sK14))) ).
cnf(u687,negated_conjecture,
r1(sK13(sK15(sK14)),sK2(sK13(sK15(sK14)))) ).
cnf(u774,negated_conjecture,
p1(sK2(sK2(sK14))) ).
cnf(u778,negated_conjecture,
p1(sK2(sK11(sK2(sK14)))) ).
cnf(u782,negated_conjecture,
p1(sK2(sK13(sK2(sK14)))) ).
cnf(u852,negated_conjecture,
( ~ r1(sK2(sK2(sK14)),X0)
| p1(X0) ) ).
cnf(u884,negated_conjecture,
r1(sK13(sK4(sK8)),sK13(sK13(sK4(sK8)))) ).
cnf(u891,negated_conjecture,
r1(sK12(sK4(sK8)),sK13(sK12(sK4(sK8)))) ).
cnf(u898,negated_conjecture,
r1(sK4(sK4(sK8)),sK13(sK4(sK4(sK8)))) ).
cnf(u909,negated_conjecture,
~ p1(sK13(sK4(sK4(sK8)))) ).
cnf(u921,negated_conjecture,
r1(sK11(sK15(sK14)),sK2(sK11(sK15(sK14)))) ).
cnf(u992,negated_conjecture,
~ r1(sK4(sK8),sK2(sK13(sK2(sK14)))) ).
cnf(u1002,negated_conjecture,
~ r1(sK8,sK2(sK13(sK2(sK14)))) ).
cnf(u1014,negated_conjecture,
( ~ r1(sK12(X0),sK2(sK13(sK2(sK14))))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u1018,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK13(sK2(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u1022,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK13(sK2(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u1036,negated_conjecture,
r1(sK13(sK14),sK15(sK13(sK14))) ).
cnf(u1043,negated_conjecture,
r1(sK13(sK14),sK13(sK13(sK14))) ).
cnf(u1051,negated_conjecture,
r1(sK11(sK14),sK2(sK11(sK14))) ).
cnf(u1115,negated_conjecture,
r1(sK11(sK4(sK8)),sK13(sK11(sK4(sK8)))) ).
cnf(u1126,negated_conjecture,
p1(sK2(sK15(sK14))) ).
cnf(u1130,negated_conjecture,
p1(sK2(sK11(sK15(sK14)))) ).
cnf(u1134,negated_conjecture,
p1(sK2(sK13(sK15(sK14)))) ).
cnf(u1151,negated_conjecture,
~ r1(sK4(sK8),sK2(sK16(sK14))) ).
cnf(u1161,negated_conjecture,
~ r1(sK8,sK2(sK16(sK14))) ).
cnf(u1173,negated_conjecture,
( ~ r1(sK12(X0),sK2(sK16(sK14)))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u1177,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK16(sK14)))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u1181,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK16(sK14)))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u1195,negated_conjecture,
~ r1(sK4(sK8),sK2(sK13(sK15(sK14)))) ).
cnf(u1205,negated_conjecture,
~ r1(sK8,sK2(sK13(sK15(sK14)))) ).
cnf(u1217,negated_conjecture,
( ~ r1(sK12(X0),sK2(sK13(sK15(sK14))))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u1221,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK13(sK15(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u1225,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK13(sK15(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u1240,negated_conjecture,
~ r1(sK4(sK8),sK2(sK11(sK15(sK14)))) ).
cnf(u1250,negated_conjecture,
~ r1(sK8,sK2(sK11(sK15(sK14)))) ).
cnf(u1262,negated_conjecture,
( ~ r1(sK12(X0),sK2(sK11(sK15(sK14))))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u1266,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK11(sK15(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u1270,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK11(sK15(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u1282,negated_conjecture,
( ~ r1(sK2(sK15(sK14)),X0)
| p1(X0) ) ).
cnf(u1327,negated_conjecture,
r1(sK11(sK11(sK14)),sK2(sK11(sK11(sK14)))) ).
cnf(u1336,negated_conjecture,
r1(sK2(sK15(sK14)),sK3(sK15(sK14))) ).
cnf(u1341,negated_conjecture,
r1(sK2(sK13(sK15(sK14))),sK3(sK13(sK15(sK14)))) ).
cnf(u1345,negated_conjecture,
r1(sK2(sK11(sK15(sK14))),sK3(sK11(sK15(sK14)))) ).
cnf(u1364,negated_conjecture,
~ r1(sK4(sK8),sK3(sK16(sK14))) ).
cnf(u1374,negated_conjecture,
~ r1(sK8,sK3(sK16(sK14))) ).
cnf(u1386,negated_conjecture,
( ~ r1(sK12(X0),sK3(sK16(sK14)))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u1390,negated_conjecture,
( ~ r1(sK4(X2),sK3(sK16(sK14)))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u1394,negated_conjecture,
( ~ r1(sK4(X2),sK3(sK16(sK14)))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u1521,negated_conjecture,
( ~ r1(sK2(sK4(sK14)),X0)
| p1(X0) ) ).
cnf(u1607,negated_conjecture,
r1(sK2(sK13(sK14)),sK3(sK13(sK14))) ).
cnf(u1611,negated_conjecture,
r1(sK2(sK11(sK14)),sK3(sK11(sK14))) ).
cnf(u1626,negated_conjecture,
p1(sK2(sK4(sK8))) ).
cnf(u1633,negated_conjecture,
p1(sK2(sK13(sK4(sK8)))) ).
cnf(u1640,negated_conjecture,
p1(sK2(sK12(sK4(sK8)))) ).
cnf(u1647,negated_conjecture,
p1(sK2(sK11(sK4(sK8)))) ).
cnf(u1762,negated_conjecture,
( ~ r1(sK2(sK12(sK4(sK8))),X0)
| p1(X0) ) ).
cnf(u1806,negated_conjecture,
( ~ r1(sK2(sK4(sK4(sK8))),X0)
| p1(X0) ) ).
cnf(u1850,negated_conjecture,
( ~ r1(sK2(sK11(sK4(sK8))),X0)
| p1(X0) ) ).
cnf(u1894,negated_conjecture,
( ~ r1(sK2(sK13(sK4(sK8))),X0)
| p1(X0) ) ).
cnf(u1940,negated_conjecture,
( ~ r1(sK2(sK4(sK8)),X0)
| p1(X0) ) ).
cnf(u1985,negated_conjecture,
r1(sK13(sK14),sK2(sK13(sK14))) ).
cnf(u2007,negated_conjecture,
~ r1(sK4(sK8),sK15(sK4(sK14))) ).
cnf(u2017,negated_conjecture,
~ r1(sK8,sK15(sK4(sK14))) ).
cnf(u2029,negated_conjecture,
( ~ r1(sK12(X0),sK15(sK4(sK14)))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u2033,negated_conjecture,
( ~ r1(sK4(X2),sK15(sK4(sK14)))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u2037,negated_conjecture,
( ~ r1(sK4(X2),sK15(sK4(sK14)))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u2088,negated_conjecture,
~ r1(sK4(sK8),sK2(sK11(sK4(sK14)))) ).
cnf(u2098,negated_conjecture,
~ r1(sK8,sK2(sK11(sK4(sK14)))) ).
cnf(u2110,negated_conjecture,
( ~ r1(sK12(X0),sK2(sK11(sK4(sK14))))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u2114,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK11(sK4(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u2118,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK11(sK4(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u2132,negated_conjecture,
~ r1(sK4(sK8),sK2(sK13(sK4(sK14)))) ).
cnf(u2142,negated_conjecture,
~ r1(sK8,sK2(sK13(sK4(sK14)))) ).
cnf(u2154,negated_conjecture,
( ~ r1(sK12(X0),sK2(sK13(sK4(sK14))))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u2158,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK13(sK4(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u2162,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK13(sK4(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u2178,negated_conjecture,
~ r1(sK4(sK8),sK2(sK15(sK4(sK14)))) ).
cnf(u2188,negated_conjecture,
~ r1(sK8,sK2(sK15(sK4(sK14)))) ).
cnf(u2200,negated_conjecture,
( ~ r1(sK12(X0),sK2(sK15(sK4(sK14))))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u2204,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK15(sK4(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u2208,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK15(sK4(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u2221,negated_conjecture,
~ r1(sK4(sK8),sK4(sK14)) ).
cnf(u2246,negated_conjecture,
( ~ r1(sK4(X2),sK4(sK14))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u2250,negated_conjecture,
( ~ r1(sK4(X2),sK4(sK14))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u2330,negated_conjecture,
p1(sK15(sK2(sK14))) ).
cnf(u2333,negated_conjecture,
r1(sK15(sK2(sK14)),sK2(sK15(sK2(sK14)))) ).
cnf(u2363,negated_conjecture,
~ r1(sK4(sK8),sK2(sK11(sK2(sK14)))) ).
cnf(u2373,negated_conjecture,
~ r1(sK8,sK2(sK11(sK2(sK14)))) ).
cnf(u2385,negated_conjecture,
( ~ r1(sK12(X0),sK2(sK11(sK2(sK14))))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u2389,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK11(sK2(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u2393,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK11(sK2(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u2542,negated_conjecture,
r1(sK2(sK2(sK14)),sK3(sK2(sK14))) ).
cnf(u2546,negated_conjecture,
r1(sK2(sK11(sK2(sK14))),sK3(sK11(sK2(sK14)))) ).
cnf(u2550,negated_conjecture,
r1(sK2(sK13(sK2(sK14))),sK3(sK13(sK2(sK14)))) ).
cnf(u2584,negated_conjecture,
r1(sK13(sK8),sK13(sK13(sK8))) ).
cnf(u2594,negated_conjecture,
( ~ r1(sK13(sK8),X0)
| r1(X0,sK11(X0)) ) ).
cnf(u2605,negated_conjecture,
r1(sK13(sK11(sK14)),sK2(sK13(sK11(sK14)))) ).
cnf(u2719,negated_conjecture,
( ~ r1(X0,sK13(sK15(sK14)))
| ~ sP1(X1)
| r1(X1,sK4(X1))
| ~ r1(X1,X0) ) ).
cnf(u2742,negated_conjecture,
~ r1(sK4(sK8),sK15(sK2(sK14))) ).
cnf(u2752,negated_conjecture,
~ r1(sK8,sK15(sK2(sK14))) ).
cnf(u2764,negated_conjecture,
( ~ r1(sK12(X0),sK15(sK2(sK14)))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u2768,negated_conjecture,
( ~ r1(sK4(X2),sK15(sK2(sK14)))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u2772,negated_conjecture,
( ~ r1(sK4(X2),sK15(sK2(sK14)))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u2782,negated_conjecture,
p1(sK15(sK11(sK14))) ).
cnf(u2794,negated_conjecture,
p1(sK2(sK11(sK14))) ).
cnf(u2798,negated_conjecture,
p1(sK2(sK13(sK11(sK14)))) ).
cnf(u2802,negated_conjecture,
p1(sK2(sK11(sK11(sK14)))) ).
cnf(u2816,negated_conjecture,
~ r1(sK4(sK8),sK2(sK11(sK11(sK14)))) ).
cnf(u2826,negated_conjecture,
~ r1(sK8,sK2(sK11(sK11(sK14)))) ).
cnf(u2838,negated_conjecture,
( ~ r1(sK12(X0),sK2(sK11(sK11(sK14))))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u2842,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK11(sK11(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u2846,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK11(sK11(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u2860,negated_conjecture,
~ r1(sK4(sK8),sK2(sK13(sK11(sK14)))) ).
cnf(u2870,negated_conjecture,
~ r1(sK8,sK2(sK13(sK11(sK14)))) ).
cnf(u2882,negated_conjecture,
( ~ r1(sK12(X0),sK2(sK13(sK11(sK14))))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u2886,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK13(sK11(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u2890,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK13(sK11(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u2899,negated_conjecture,
r1(sK2(sK13(sK11(sK14))),sK3(sK13(sK11(sK14)))) ).
cnf(u2903,negated_conjecture,
r1(sK2(sK11(sK11(sK14))),sK3(sK11(sK11(sK14)))) ).
cnf(u2919,negated_conjecture,
~ r1(sK4(sK8),sK2(sK11(sK14))) ).
cnf(u2929,negated_conjecture,
~ r1(sK8,sK2(sK11(sK14))) ).
cnf(u2941,negated_conjecture,
( ~ r1(sK12(X0),sK2(sK11(sK14)))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u2945,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK11(sK14)))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u2949,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK11(sK14)))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u3023,negated_conjecture,
( ~ r1(X0,sK11(sK14))
| ~ sP1(X1)
| r1(X1,sK4(X1))
| ~ r1(X1,X0) ) ).
cnf(u3060,negated_conjecture,
~ r1(sK4(sK8),sK15(sK11(sK14))) ).
cnf(u3070,negated_conjecture,
~ r1(sK8,sK15(sK11(sK14))) ).
cnf(u3082,negated_conjecture,
( ~ r1(sK12(X0),sK15(sK11(sK14)))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u3086,negated_conjecture,
( ~ r1(sK4(X2),sK15(sK11(sK14)))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u3090,negated_conjecture,
( ~ r1(sK4(X2),sK15(sK11(sK14)))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u3099,negated_conjecture,
r1(sK11(sK8),sK13(sK11(sK8))) ).
cnf(u3106,negated_conjecture,
r1(sK11(sK8),sK12(sK11(sK8))) ).
cnf(u3120,negated_conjecture,
r1(sK13(sK8),sK4(sK13(sK8))) ).
cnf(u3135,negated_conjecture,
( ~ r1(sK4(sK13(sK8)),X2)
| ~ p1(X2)
| p1(X3)
| ~ r1(X2,X3) ) ).
cnf(u3144,negated_conjecture,
~ p1(sK4(sK13(sK8))) ).
cnf(u3155,negated_conjecture,
p1(sK2(sK13(sK14))) ).
cnf(u3167,negated_conjecture,
~ r1(sK4(sK8),sK2(sK14)) ).
cnf(u3171,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK14))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u3175,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK14))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u3218,negated_conjecture,
( ~ r1(sK3(sK15(sK14)),X0)
| p1(X0) ) ).
cnf(u3255,negated_conjecture,
( ~ r1(X0,sK15(sK14))
| ~ sP1(X1)
| r1(X1,sK4(X1))
| ~ r1(X1,X0) ) ).
cnf(u3285,negated_conjecture,
r1(sK3(sK14),sK2(sK3(sK14))) ).
cnf(u3289,negated_conjecture,
p1(sK2(sK3(sK14))) ).
cnf(u3293,negated_conjecture,
r1(sK2(sK3(sK14)),sK3(sK3(sK14))) ).
cnf(u3367,negated_conjecture,
~ r1(sK4(sK8),sK2(sK3(sK14))) ).
cnf(u3377,negated_conjecture,
~ r1(sK8,sK2(sK3(sK14))) ).
cnf(u3389,negated_conjecture,
( ~ r1(sK12(X0),sK2(sK3(sK14)))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u3393,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK3(sK14)))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u3397,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK3(sK14)))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u3466,negated_conjecture,
~ sP1(sK15(sK14)) ).
cnf(u3479,negated_conjecture,
r1(sK11(sK13(sK14)),sK2(sK11(sK13(sK14)))) ).
cnf(u3483,negated_conjecture,
p1(sK2(sK11(sK13(sK14)))) ).
cnf(u3498,negated_conjecture,
~ r1(sK4(sK8),sK2(sK11(sK13(sK14)))) ).
cnf(u3508,negated_conjecture,
~ r1(sK8,sK2(sK11(sK13(sK14)))) ).
cnf(u3520,negated_conjecture,
( ~ r1(sK12(X0),sK2(sK11(sK13(sK14))))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u3524,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK11(sK13(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u3528,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK11(sK13(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u3550,negated_conjecture,
~ r1(sK4(sK8),sK15(sK14)) ).
cnf(u3554,negated_conjecture,
( ~ r1(sK4(X2),sK15(sK14))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u3558,negated_conjecture,
( ~ r1(sK4(X2),sK15(sK14))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u3592,negated_conjecture,
r1(sK11(sK8),sK4(sK11(sK8))) ).
cnf(u3607,negated_conjecture,
( ~ r1(sK4(sK11(sK8)),X2)
| ~ p1(X2)
| p1(X3)
| ~ r1(X2,X3) ) ).
cnf(u3657,negated_conjecture,
( ~ r1(sK3(sK2(sK14)),X0)
| p1(X0) ) ).
cnf(u3743,negated_conjecture,
( ~ r1(X0,sK11(sK15(sK14)))
| ~ sP1(X1)
| r1(X1,sK4(X1))
| ~ r1(X1,X0) ) ).
cnf(u3821,negated_conjecture,
~ p1(sK4(sK11(sK8))) ).
cnf(u3849,negated_conjecture,
~ r1(sK4(sK8),sK2(sK13(sK14))) ).
cnf(u3859,negated_conjecture,
~ r1(sK8,sK2(sK13(sK14))) ).
cnf(u3871,negated_conjecture,
( ~ r1(sK12(X0),sK2(sK13(sK14)))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u3875,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK13(sK14)))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u3879,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK13(sK14)))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u3932,negated_conjecture,
( ~ r1(X0,sK11(sK2(sK14)))
| ~ sP1(X1)
| r1(X1,sK4(X1))
| ~ r1(X1,X0) ) ).
cnf(u3966,negated_conjecture,
~ sP1(sK2(sK14)) ).
cnf(u3975,negated_conjecture,
r1(sK2(sK11(sK13(sK14))),sK3(sK11(sK13(sK14)))) ).
cnf(u4030,negated_conjecture,
r1(sK13(sK13(sK14)),sK2(sK13(sK13(sK14)))) ).
cnf(u4034,negated_conjecture,
p1(sK2(sK13(sK13(sK14)))) ).
cnf(u4038,negated_conjecture,
r1(sK2(sK13(sK13(sK14))),sK3(sK13(sK13(sK14)))) ).
cnf(u4117,negated_conjecture,
~ r1(sK4(sK8),sK2(sK13(sK13(sK14)))) ).
cnf(u4127,negated_conjecture,
~ r1(sK8,sK2(sK13(sK13(sK14)))) ).
cnf(u4139,negated_conjecture,
( ~ r1(sK12(X0),sK2(sK13(sK13(sK14))))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u4143,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK13(sK13(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u4147,negated_conjecture,
( ~ r1(sK4(X2),sK2(sK13(sK13(sK14))))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u4156,negated_conjecture,
~ p1(sK11(sK4(sK13(sK8)))) ).
cnf(u4210,negated_conjecture,
( ~ r1(X0,sK13(sK2(sK14)))
| ~ sP1(X1)
| r1(X1,sK4(X1))
| ~ r1(X1,X0) ) ).
cnf(u4307,negated_conjecture,
( ~ r1(X0,sK13(sK11(sK14)))
| ~ sP1(X1)
| r1(X1,sK4(X1))
| ~ r1(X1,X0) ) ).
cnf(u4384,negated_conjecture,
( ~ r1(X0,sK13(sK14))
| ~ sP1(X1)
| r1(X1,sK4(X1))
| ~ r1(X1,X0) ) ).
cnf(u4545,negated_conjecture,
~ sP1(sK11(sK14)) ).
cnf(u4600,negated_conjecture,
( ~ r1(X0,sK11(sK11(sK14)))
| ~ sP1(X1)
| r1(X1,sK4(X1))
| ~ r1(X1,X0) ) ).
cnf(u4717,negated_conjecture,
p1(sK15(sK13(sK14))) ).
cnf(u4720,negated_conjecture,
r1(sK15(sK13(sK14)),sK2(sK15(sK13(sK14)))) ).
cnf(u4724,negated_conjecture,
p1(sK2(sK15(sK13(sK14)))) ).
cnf(u4728,negated_conjecture,
r1(sK2(sK15(sK13(sK14))),sK3(sK15(sK13(sK14)))) ).
cnf(u4742,negated_conjecture,
~ r1(sK4(sK8),sK15(sK13(sK14))) ).
cnf(u4752,negated_conjecture,
~ r1(sK8,sK15(sK13(sK14))) ).
cnf(u4764,negated_conjecture,
( ~ r1(sK12(X0),sK15(sK13(sK14)))
| ~ r1(sK8,X0)
| p1(X0)
| r1(X1,sK11(X1))
| ~ r1(X0,X1) ) ).
cnf(u4768,negated_conjecture,
( ~ r1(sK4(X2),sK15(sK13(sK14)))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u4772,negated_conjecture,
( ~ r1(sK4(X2),sK15(sK13(sK14)))
| ~ sP1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u4788,negated_conjecture,
( ~ r1(sK2(sK15(sK13(sK14))),X0)
| p1(X0) ) ).
cnf(u4828,negated_conjecture,
~ sP1(sK13(sK14)) ).
cnf(u4837,negated_conjecture,
~ sP1(sK13(sK2(sK14))) ).
cnf(u4846,negated_conjecture,
~ sP1(sK11(sK2(sK14))) ).
cnf(u4902,negated_conjecture,
( ~ r1(X0,sK11(sK13(sK14)))
| ~ sP1(X1)
| r1(X1,sK4(X1))
| ~ r1(X1,X0) ) ).
cnf(u5002,negated_conjecture,
~ sP1(sK13(sK15(sK14))) ).
cnf(u5011,negated_conjecture,
~ sP1(sK13(sK11(sK14))) ).
cnf(u5021,negated_conjecture,
r1(sK13(sK13(sK8)),sK13(sK13(sK13(sK8)))) ).
cnf(u5028,negated_conjecture,
r1(sK4(sK13(sK8)),sK13(sK4(sK13(sK8)))) ).
cnf(u5039,negated_conjecture,
~ p1(sK13(sK4(sK13(sK8)))) ).
cnf(u5045,negated_conjecture,
~ sP1(sK11(sK11(sK14))) ).
cnf(u5056,negated_conjecture,
r1(sK13(sK11(sK8)),sK13(sK13(sK11(sK8)))) ).
cnf(u5063,negated_conjecture,
r1(sK12(sK11(sK8)),sK13(sK12(sK11(sK8)))) ).
cnf(u5070,negated_conjecture,
r1(sK4(sK11(sK8)),sK13(sK4(sK11(sK8)))) ).
cnf(u5086,negated_conjecture,
~ p1(sK13(sK4(sK11(sK8)))) ).
cnf(u5120,negated_conjecture,
~ sP1(sK11(sK15(sK14))) ).
cnf(u5175,negated_conjecture,
( ~ r1(X0,sK13(sK13(sK14)))
| ~ sP1(X1)
| r1(X1,sK4(X1))
| ~ r1(X1,X0) ) ).
cnf(u5218,negated_conjecture,
~ sP1(sK11(sK13(sK14))) ).
cnf(u5227,negated_conjecture,
~ sP1(sK13(sK13(sK14))) ).
cnf(u5235,negated_conjecture,
r1(sK11(sK11(sK8)),sK13(sK11(sK11(sK8)))) ).
cnf(u5253,negated_conjecture,
( ~ r1(sK3(sK15(sK13(sK14))),X0)
| p1(X0) ) ).
cnf(u5290,negated_conjecture,
( ~ r1(X0,sK15(sK13(sK14)))
| ~ sP1(X1)
| r1(X1,sK4(X1))
| ~ r1(X1,X0) ) ).
cnf(u5328,negated_conjecture,
r1(sK11(sK13(sK8)),sK13(sK11(sK13(sK8)))) ).
cnf(u5337,negated_conjecture,
~ sP1(sK15(sK13(sK14))) ).
cnf(u56,negated_conjecture,
( ~ p1(X1)
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(sK8,X1)
| ~ r1(X1,X3)
| r1(X3,sK9(X3))
| sP0(X1) ) ).
cnf(u530,negated_conjecture,
( ~ r1(sK4(sK8),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK13(X0)) ) ).
cnf(u2403,negated_conjecture,
r1(sK2(sK11(sK4(sK14))),sK3(sK11(sK4(sK14)))) ).
cnf(u50,negated_conjecture,
( ~ p1(X9)
| p1(X1)
| ~ r1(X1,X6)
| r1(X6,sK11(X6))
| ~ r1(sK12(X1),X9)
| ~ r1(X9,X10)
| p1(X10)
| ~ r1(sK8,X1) ) ).
cnf(u1994,negated_conjecture,
( ~ r1(sK2(sK14),X0)
| p1(sK2(X0))
| p1(X0) ) ).
cnf(u1348,negated_conjecture,
r1(sK2(sK16(sK14)),sK3(sK16(sK14))) ).
cnf(u1110,negated_conjecture,
r1(sK4(sK8),sK11(sK4(sK8))) ).
cnf(u3096,negated_conjecture,
r1(sK11(sK8),sK11(sK11(sK8))) ).
cnf(u91,negated_conjecture,
r1(sK14,sK11(sK14)) ).
cnf(u25,axiom,
( ~ p1(X6)
| ~ r1(X1,X2)
| p1(X2)
| r1(sK2(X2),sK3(X2))
| ~ r1(sK4(X0),X6)
| ~ r1(X6,X7)
| p1(X7)
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u914,negated_conjecture,
( ~ r1(sK4(sK8),sK15(X0))
| p1(X1)
| ~ r1(sK15(X0),X1)
| p1(X0)
| ~ r1(sK14,X0) ) ).
cnf(u4851,negated_conjecture,
r1(sK13(sK13(sK8)),sK11(sK13(sK13(sK8)))) ).
cnf(u49,negated_conjecture,
( ~ p1(sK11(X6))
| p1(X1)
| ~ r1(X1,X6)
| ~ r1(sK8,X1)
| r1(X1,sK12(X1)) ) ).
cnf(u52,negated_conjecture,
( ~ r1(sK8,X1)
| p1(X1)
| ~ r1(X1,X6)
| r1(X6,sK11(X6))
| r1(X1,sK12(X1)) ) ).
cnf(u43,negated_conjecture,
r1(sK8,sK14) ).
cnf(u46,negated_conjecture,
( ~ r1(sK8,X1)
| ~ r1(X1,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| p1(X13)
| r1(X11,sK13(X11)) ) ).
cnf(u45,negated_conjecture,
( ~ p1(sK13(X11))
| ~ r1(X1,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| p1(X13)
| ~ r1(sK8,X1) ) ).
cnf(u32,axiom,
( ~ p1(sK7(X3))
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| ~ r1(sK5(X0),X3)
| ~ sP0(X0) ) ).
cnf(u39,negated_conjecture,
( ~ p1(sK16(X16))
| p1(X16)
| ~ r1(sK14,X16) ) ).
cnf(u26,axiom,
( ~ p1(sK4(X0))
| ~ r1(X1,X2)
| p1(X2)
| r1(sK2(X2),sK3(X2))
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u28,axiom,
( ~ sP1(X0)
| ~ r1(X1,X2)
| p1(X2)
| r1(X2,sK2(X2))
| ~ r1(sK4(X0),X6)
| ~ r1(X6,X7)
| p1(X7)
| ~ p1(X6)
| ~ r1(X0,X1) ) ).
cnf(u19,axiom,
( ~ p1(X6)
| ~ r1(X1,X2)
| p1(X2)
| p1(sK2(X2))
| ~ r1(sK4(X0),X6)
| ~ r1(X6,X7)
| p1(X7)
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u22,axiom,
( ~ p1(sK3(X2))
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X0,X1)
| ~ r1(sK4(X0),X6)
| ~ r1(X6,X7)
| p1(X7)
| ~ p1(X6)
| ~ sP1(X0) ) ).
cnf(u21,axiom,
( ~ sP1(X0)
| ~ r1(X1,X2)
| p1(X2)
| p1(sK2(X2))
| r1(X0,sK4(X0))
| ~ r1(X0,X1) ) ).
cnf(u2669,negated_conjecture,
r1(sK13(sK8),sK11(sK13(sK8))) ).
cnf(u3460,negated_conjecture,
( ~ r1(X0,sK13(sK15(sK14)))
| r1(X0,sK4(X0))
| ~ sP1(X0) ) ).
cnf(u1991,negated_conjecture,
r1(sK2(sK14),sK11(sK2(sK14))) ).
cnf(u1982,negated_conjecture,
r1(sK14,sK2(sK14)) ).
cnf(u5192,negated_conjecture,
( ~ r1(X0,sK13(sK13(sK14)))
| r1(X0,sK4(X0))
| ~ sP1(X0) ) ).
cnf(u410,negated_conjecture,
( ~ r1(sK11(sK14),X0)
| r1(sK2(X0),sK3(X0))
| p1(X0) ) ).
cnf(u3636,negated_conjecture,
( ~ r1(sK11(sK8),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK13(X0)) ) ).
cnf(u236,negated_conjecture,
( ~ r1(sK12(X0),sK15(X2))
| ~ r1(X0,X1)
| r1(X1,sK11(X1))
| p1(X0)
| ~ r1(sK15(X2),X3)
| p1(X3)
| ~ r1(sK8,X0)
| p1(X2)
| ~ r1(sK14,X2) ) ).
cnf(u406,negated_conjecture,
( ~ r1(sK11(sK14),X0)
| p1(sK2(X0))
| p1(X0) ) ).
cnf(u202,negated_conjecture,
( ~ r1(sK11(sK14),X0)
| r1(X0,sK2(X0))
| p1(X0) ) ).
cnf(u1138,negated_conjecture,
p1(sK2(sK16(sK14))) ).
cnf(u198,negated_conjecture,
r1(sK15(sK14),sK11(sK15(sK14))) ).
cnf(u358,negated_conjecture,
( ~ r1(sK8,sK15(X0))
| p1(X1)
| ~ r1(sK15(X0),X1)
| ~ r1(sK15(X0),X2)
| r1(sK9(X2),sK10(X2))
| sP0(sK15(X0))
| p1(X0)
| ~ r1(sK14,X0) ) ).
cnf(u125,negated_conjecture,
( ~ r1(sK4(sK14),X0)
| r1(X0,sK2(X0))
| p1(X0) ) ).
cnf(u5325,negated_conjecture,
r1(sK11(sK13(sK8)),sK11(sK11(sK13(sK8)))) ).
cnf(u119,negated_conjecture,
( ~ r1(sK14,X0)
| r1(X0,sK2(X0))
| p1(X0) ) ).
cnf(u3275,negated_conjecture,
r1(sK2(sK14),sK3(sK14)) ).
cnf(u2577,negated_conjecture,
( ~ r1(sK13(sK8),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK13(X0)) ) ).
cnf(u58,negated_conjecture,
( ~ r1(sK14,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK13(X0)) ) ).
cnf(u1992,negated_conjecture,
( ~ r1(sK2(sK14),X0)
| r1(X0,sK2(X0))
| p1(X0) ) ).
cnf(u57,negated_conjecture,
sP1(sK14) ).
cnf(u60,negated_conjecture,
sP1(sK8) ).
cnf(u3045,negated_conjecture,
( ~ r1(X0,sK14)
| r1(X0,sK4(X0))
| ~ sP1(X0) ) ).
cnf(u51,negated_conjecture,
( ~ p1(sK12(X1))
| p1(X1)
| ~ r1(X1,X6)
| r1(X6,sK11(X6))
| ~ r1(sK8,X1) ) ).
cnf(u54,negated_conjecture,
( ~ p1(sK10(X3))
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(X1)
| ~ r1(X1,X3)
| ~ r1(sK8,X1)
| sP0(X1) ) ).
cnf(u53,negated_conjecture,
( ~ p1(X1)
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(sK8,X1)
| ~ r1(X1,X3)
| p1(sK9(X3))
| sP0(X1) ) ).
cnf(u40,negated_conjecture,
( r1(sK15(X16),sK16(X16))
| p1(X16)
| ~ r1(sK14,X16) ) ).
cnf(u47,negated_conjecture,
( ~ p1(sK11(X6))
| p1(X1)
| ~ r1(X1,X6)
| ~ r1(sK8,X1)
| ~ r1(sK12(X1),X9)
| ~ r1(X9,X10)
| p1(X10)
| ~ p1(X9) ) ).
cnf(u34,axiom,
( p1(sK5(X0))
| ~ sP0(X0) ) ).
cnf(u4976,negated_conjecture,
( ~ r1(X0,sK11(sK13(sK14)))
| r1(X0,sK4(X0))
| ~ sP1(X0) ) ).
cnf(u357,negated_conjecture,
( ~ r1(sK8,sK5(X0))
| p1(X1)
| ~ r1(sK5(X0),X1)
| ~ r1(sK5(X0),X2)
| r1(sK9(X2),sK10(X2))
| sP0(sK5(X0))
| ~ sP0(X0) ) ).
cnf(u691,negated_conjecture,
r1(sK16(sK14),sK2(sK16(sK14))) ).
cnf(u5301,negated_conjecture,
( ~ r1(X0,sK15(sK13(sK14)))
| r1(X0,sK4(X0))
| ~ sP1(X0) ) ).
cnf(u1930,negated_conjecture,
p1(sK2(sK4(sK4(sK8)))) ).
cnf(u5240,negated_conjecture,
p1(sK3(sK15(sK13(sK14)))) ).
cnf(u36,axiom,
( r1(sK5(X0),sK6(X0))
| ~ sP0(X0) ) ).
cnf(u4502,negated_conjecture,
( ~ r1(X0,sK13(sK14))
| r1(X0,sK4(X0))
| ~ sP1(X0) ) ).
cnf(u234,negated_conjecture,
( ~ r1(sK14,X0)
| p1(sK2(X0))
| p1(X0) ) ).
cnf(u30,axiom,
( ~ sP1(X0)
| ~ r1(X1,X2)
| p1(X2)
| r1(X2,sK2(X2))
| r1(X0,sK4(X0))
| ~ r1(X0,X1) ) ).
cnf(u233,negated_conjecture,
( ~ r1(sK4(sK14),X0)
| p1(sK2(X0))
| p1(X0) ) ).
cnf(u33,axiom,
( ~ sP0(X0)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| r1(X3,sK7(X3))
| ~ r1(sK5(X0),X3) ) ).
cnf(u23,axiom,
( ~ p1(sK4(X0))
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(sK3(X2))
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u27,axiom,
( ~ sP1(X0)
| ~ r1(X1,X2)
| p1(X2)
| r1(sK2(X2),sK3(X2))
| r1(X0,sK4(X0))
| ~ r1(X0,X1) ) ).
cnf(u29,axiom,
( ~ p1(sK4(X0))
| ~ r1(X1,X2)
| p1(X2)
| r1(X2,sK2(X2))
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u2402,negated_conjecture,
r1(sK2(sK13(sK4(sK14))),sK3(sK13(sK4(sK14)))) ).
cnf(u2401,negated_conjecture,
r1(sK2(sK15(sK4(sK14))),sK3(sK15(sK4(sK14)))) ).
cnf(u2074,negated_conjecture,
p1(sK2(sK13(sK4(sK14)))) ).
cnf(u151,negated_conjecture,
sP1(sK4(sK8)) ).
cnf(u3949,negated_conjecture,
( ~ r1(X0,sK11(sK2(sK14)))
| r1(X0,sK4(X0))
| ~ sP1(X0) ) ).
cnf(u164,negated_conjecture,
( ~ r1(sK8,sK5(X0))
| p1(X1)
| ~ r1(sK5(X0),X1)
| ~ r1(sK5(X0),X2)
| r1(X2,sK9(X2))
| sP0(sK5(X0))
| ~ sP0(X0) ) ).
cnf(u766,negated_conjecture,
( ~ r1(sK4(X2),sK15(X3))
| p1(X1)
| r1(sK2(X1),sK3(X1))
| ~ r1(X0,X1)
| ~ r1(sK15(X3),X4)
| p1(X4)
| ~ r1(X2,X0)
| ~ sP1(X2)
| p1(X3)
| ~ r1(sK14,X3) ) ).
cnf(u765,axiom,
( ~ r1(sK4(X2),sK5(X3))
| p1(X1)
| r1(sK2(X1),sK3(X1))
| ~ r1(X0,X1)
| ~ r1(sK5(X3),X4)
| p1(X4)
| ~ r1(X2,X0)
| ~ sP1(X2)
| ~ sP0(X3) ) ).
cnf(u127,negated_conjecture,
( ~ r1(sK15(sK14),X0)
| r1(X0,sK2(X0))
| p1(X0) ) ).
cnf(u3044,negated_conjecture,
( ~ r1(X0,sK11(sK14))
| r1(X0,sK4(X0))
| ~ sP1(X0) ) ).
cnf(u1028,negated_conjecture,
r1(sK13(sK14),sK11(sK13(sK14))) ).
cnf(u3205,negated_conjecture,
p1(sK3(sK15(sK14))) ).
cnf(u1031,negated_conjecture,
( ~ r1(sK13(sK14),X0)
| p1(sK2(X0))
| p1(X0) ) ).
cnf(u767,axiom,
( ~ r1(sK4(X2),sK5(X3))
| p1(X1)
| p1(sK2(X1))
| ~ r1(X0,X1)
| ~ r1(sK5(X3),X4)
| p1(X4)
| ~ r1(X2,X0)
| ~ sP1(X2)
| ~ sP0(X3) ) ).
cnf(u912,negated_conjecture,
( ~ r1(sK4(sK8),sK5(X0))
| p1(X1)
| ~ r1(sK5(X0),X1)
| ~ sP0(X0) ) ).
cnf(u584,negated_conjecture,
r1(sK4(sK14),sK11(sK4(sK14))) ).
cnf(u3950,negated_conjecture,
( ~ r1(X0,sK2(sK14))
| r1(X0,sK4(X0))
| ~ sP1(X0) ) ).
cnf(u59,negated_conjecture,
( ~ r1(sK8,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK13(X0)) ) ).
cnf(u768,negated_conjecture,
( ~ r1(sK4(X2),sK15(X3))
| p1(X1)
| p1(sK2(X1))
| ~ r1(X0,X1)
| ~ r1(sK15(X3),X4)
| p1(X4)
| ~ r1(X2,X0)
| ~ sP1(X2)
| p1(X3)
| ~ r1(sK14,X3) ) ).
cnf(u3461,negated_conjecture,
( ~ r1(X0,sK15(sK14))
| r1(X0,sK4(X0))
| ~ sP1(X0) ) ).
cnf(u2252,negated_conjecture,
( ~ p1(sK3(X1))
| p1(X1)
| ~ r1(X0,X1)
| ~ r1(sK14,X0) ) ).
cnf(u411,negated_conjecture,
( ~ r1(sK14,X0)
| r1(sK2(X0),sK3(X0))
| p1(X0) ) ).
cnf(u2576,negated_conjecture,
sP1(sK13(sK8)) ).
cnf(u62,negated_conjecture,
r1(sK14,sK15(sK14)) ).
cnf(u92,negated_conjecture,
r1(sK11(sK14),sK11(sK11(sK14))) ).
cnf(u48,negated_conjecture,
( ~ p1(sK12(X1))
| p1(X1)
| ~ r1(X1,X6)
| ~ p1(sK11(X6))
| ~ r1(sK8,X1) ) ).
cnf(u55,negated_conjecture,
( ~ p1(X1)
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(sK8,X1)
| ~ r1(X1,X3)
| r1(sK9(X3),sK10(X3))
| sP0(X1) ) ).
cnf(u42,negated_conjecture,
~ p1(sK14) ).
cnf(u2073,negated_conjecture,
p1(sK2(sK15(sK4(sK14)))) ).
cnf(u41,negated_conjecture,
( ~ r1(sK14,X16)
| p1(X16)
| r1(X16,sK15(X16)) ) ).
cnf(u44,negated_conjecture,
( ~ r1(sK8,X1)
| sP1(X1) ) ).
cnf(u35,axiom,
( ~ p1(sK6(X0))
| ~ sP0(X0) ) ).
cnf(u38,negated_conjecture,
( p1(sK15(X16))
| p1(X16)
| ~ r1(sK14,X16) ) ).
cnf(u37,axiom,
( ~ sP0(X0)
| r1(X0,sK5(X0)) ) ).
cnf(u24,axiom,
( ~ p1(sK3(X2))
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X0,X1)
| r1(X0,sK4(X0))
| ~ sP1(X0) ) ).
cnf(u31,axiom,
( ~ sP0(X0)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| p1(X3)
| ~ r1(sK5(X0),X3) ) ).
cnf(u18,axiom,
r1(X0,X0) ).
cnf(u1995,negated_conjecture,
( ~ r1(sK2(sK14),X0)
| r1(sK2(X0),sK3(X0))
| p1(X0) ) ).
cnf(u4324,negated_conjecture,
( ~ r1(X0,sK13(sK11(sK14)))
| r1(X0,sK4(X0))
| ~ sP1(X0) ) ).
cnf(u3092,negated_conjecture,
sP1(sK11(sK8)) ).
cnf(u1111,negated_conjecture,
r1(sK8,sK11(sK8)) ).
cnf(u4675,negated_conjecture,
( ~ r1(X0,sK11(sK11(sK14)))
| r1(X0,sK4(X0))
| ~ sP1(X0) ) ).
cnf(u476,negated_conjecture,
( ~ r1(sK4(sK14),X0)
| r1(sK2(X0),sK3(X0))
| p1(X0) ) ).
cnf(u235,negated_conjecture,
( ~ r1(sK12(X0),sK5(X2))
| ~ r1(X0,X1)
| r1(X1,sK11(X1))
| p1(X0)
| ~ r1(sK5(X2),X3)
| p1(X3)
| ~ r1(sK8,X0)
| ~ sP0(X2) ) ).
cnf(u1030,negated_conjecture,
( ~ r1(sK13(sK14),X0)
| r1(sK2(X0),sK3(X0))
| p1(X0) ) ).
cnf(u238,negated_conjecture,
( ~ r1(sK8,sK15(X0))
| p1(X1)
| ~ r1(sK15(X0),X1)
| ~ r1(sK15(X0),X2)
| p1(sK9(X2))
| sP0(sK15(X0))
| p1(X0)
| ~ r1(sK14,X0) ) ).
cnf(u3137,negated_conjecture,
r1(sK4(sK13(sK8)),sK11(sK4(sK13(sK8)))) ).
cnf(u1029,negated_conjecture,
( ~ r1(sK13(sK14),X0)
| r1(X0,sK2(X0))
| p1(X0) ) ).
cnf(u237,negated_conjecture,
( ~ r1(sK8,sK5(X0))
| p1(X1)
| ~ r1(sK5(X0),X1)
| ~ r1(sK5(X0),X2)
| p1(sK9(X2))
| sP0(sK5(X0))
| ~ sP0(X0) ) ).
cnf(u231,negated_conjecture,
( ~ r1(sK15(sK14),X0)
| p1(sK2(X0))
| p1(X0) ) ).
cnf(u20,axiom,
( ~ p1(sK4(X0))
| ~ r1(X1,X2)
| p1(X2)
| p1(sK2(X2))
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u2075,negated_conjecture,
p1(sK2(sK11(sK4(sK14)))) ).
cnf(u4236,negated_conjecture,
( ~ r1(X0,sK13(sK2(sK14)))
| r1(X0,sK4(X0))
| ~ sP1(X0) ) ).
cnf(u165,negated_conjecture,
( ~ r1(sK8,sK15(X0))
| p1(X1)
| ~ r1(sK15(X0),X1)
| ~ r1(sK15(X0),X2)
| r1(X2,sK9(X2))
| sP0(sK15(X0))
| p1(X0)
| ~ r1(sK14,X0) ) ).
cnf(u4158,negated_conjecture,
( ~ r1(X0,sK11(sK15(sK14)))
| r1(X0,sK4(X0))
| ~ sP1(X0) ) ).
cnf(u409,negated_conjecture,
( ~ r1(sK15(sK14),X0)
| r1(sK2(X0),sK3(X0))
| p1(X0) ) ).
cnf(u3644,negated_conjecture,
p1(sK3(sK2(sK14))) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL659+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.37 % Computer : n003.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 16:23:41 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.55/2.37 % (760390)Detected formulas, will run a generic FOF schedule.
% 10.55/2.37 % (760496)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=2222770129:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.55/2.37 % (760497)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=393155865:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.55/2.37 % (760499)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3255994331:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.55/2.37 % (760501)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3075718600:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.55/2.37 % (760498)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=1812093928:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.55/2.37 % (760502)dis-21_1_sil=8000:lcm=predicate:random_seed=3876277275: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)
% 10.55/2.37 % (760500)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3384742590:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.55/2.37 % (760501)Refutation not found, incomplete strategy
% 10.55/2.37 % (760501)------------------------------
% 10.55/2.37 % (760501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.37 % (760501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.37 % (760501)CaDiCaL version: 2.1.3
% 10.55/2.37 % (760501)Termination reason: Refutation not found, incomplete strategy
% 10.55/2.37 % (760501)Time elapsed: 0.003 s
% 10.55/2.37 % (760501)Peak memory usage: 88 MB
% 10.55/2.37 % (760501)Instructions burned: 3 (million)
% 10.55/2.37 % (760502)Instruction limit reached!
% 10.55/2.37 % (760502)------------------------------
% 10.55/2.37 % (760502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.37 % (760502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.37 % (760502)CaDiCaL version: 2.1.3
% 10.55/2.37 % (760502)Termination reason: Instruction limit
% 10.55/2.37 % (760502)Termination phase: Saturation
% 10.55/2.37 % (760502)Time elapsed: 0.068 s
% 10.55/2.37 % (760502)Peak memory usage: 88 MB
% 10.55/2.37 % (760502)Instructions burned: 131 (million)
% 10.55/2.37 % (760499)Instruction limit reached!
% 10.55/2.37 % (760499)------------------------------
% 10.55/2.37 % (760499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.37 % (760499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.37 % (760499)CaDiCaL version: 2.1.3
% 10.55/2.37 % (760499)Termination reason: Instruction limit
% 10.55/2.37 % (760499)Termination phase: Saturation
% 10.55/2.37 % (760499)Time elapsed: 0.071 s
% 10.55/2.37 % (760499)Peak memory usage: 89 MB
% 10.55/2.37 % (760499)Instructions burned: 110 (million)
% 10.55/2.37 % (760500)Instruction limit reached!
% 10.55/2.37 % (760500)------------------------------
% 10.55/2.37 % (760500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.37 % (760500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.37 % (760500)CaDiCaL version: 2.1.3
% 10.55/2.37 % (760500)Termination reason: Instruction limit
% 10.55/2.37 % (760500)Termination phase: Saturation
% 10.55/2.37 % (760500)Time elapsed: 0.077 s
% 10.55/2.37 % (760500)Peak memory usage: 88 MB
% 10.55/2.37 % (760500)Instructions burned: 119 (million)
% 10.55/2.37 % (760533)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1884880602:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 10.55/2.37 % (760532)lrs+10_1_sil=8000:sp=occurrence:random_seed=2517496790:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 10.55/2.37 % (760534)lrs+1011_1_sil=32000:sp=occurrence:random_seed=427868583:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 10.55/2.37 % (760534)Refutation not found, incomplete strategy
% 10.55/2.37 % (760534)------------------------------
% 10.55/2.37 % (760534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.37 % (760534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.37 % (760534)CaDiCaL version: 2.1.3
% 10.55/2.37 % (760534)Termination reason: Refutation not found, incomplete strategy
% 10.55/2.37 % (760534)Time elapsed: 0.003 s
% 10.55/2.37 % (760534)Peak memory usage: 88 MB
% 10.55/2.37 % (760534)Instructions burned: 3 (million)
% 10.55/2.37 % (760533)Refutation not found, incomplete strategy
% 10.55/2.37 % (760533)------------------------------
% 10.55/2.37 % (760533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.37 % (760533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.37 % (760533)CaDiCaL version: 2.1.3
% 10.55/2.37 % (760533)Termination reason: Refutation not found, incomplete strategy
% 10.55/2.37 % (760533)Time elapsed: 0.011 s
% 10.55/2.37 % (760533)Peak memory usage: 88 MB
% 10.55/2.37 % (760533)Instructions burned: 20 (million)
% 10.55/2.37 % (760501)------------------------------
% 10.55/2.37 % (760501)------------------------------
% 10.55/2.37 % (760532)Instruction limit reached!
% 10.55/2.37 % (760532)------------------------------
% 10.55/2.37 % (760532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.37 % (760532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.37 % (760532)CaDiCaL version: 2.1.3
% 10.55/2.37 % (760532)Termination reason: Instruction limit
% 10.55/2.37 % (760532)Termination phase: Saturation
% 10.55/2.37 % (760532)Time elapsed: 0.171 s
% 10.55/2.37 % (760532)Peak memory usage: 92 MB
% 10.55/2.37 % (760532)Instructions burned: 285 (million)
% 10.55/2.37 % (760560)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=671962159:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 10.55/2.37 % (760560)Refutation not found, incomplete strategy
% 10.55/2.37 % (760560)------------------------------
% 10.55/2.37 % (760560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.37 % (760560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.37 % (760560)CaDiCaL version: 2.1.3
% 10.55/2.37 % (760560)Termination reason: Refutation not found, incomplete strategy
% 10.55/2.37 % (760560)Time elapsed: 0.009 s
% 10.55/2.37 % (760560)Peak memory usage: 88 MB
% 10.55/2.37 % (760560)Instructions burned: 16 (million)
% 10.55/2.37 % (760534)------------------------------
% 10.55/2.37 % (760534)------------------------------
% 10.55/2.37 % (760533)------------------------------
% 10.55/2.37 % (760533)------------------------------
% 10.55/2.37 % (760612)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1627719580:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 10.55/2.37 % (760635)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=190625313:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 10.55/2.37 % (760636)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=791033449:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 10.55/2.37 % (760560)------------------------------
% 10.55/2.37 % (760560)------------------------------
% 10.55/2.37 % (760636)Instruction limit reached!
% 10.55/2.37 % (760636)------------------------------
% 10.55/2.37 % (760636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.37 % (760636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.37 % (760636)CaDiCaL version: 2.1.3
% 10.55/2.37 % (760636)Termination reason: Instruction limit
% 10.55/2.37 % (760636)Termination phase: Saturation
% 10.55/2.37 % (760636)Time elapsed: 0.069 s
% 10.55/2.37 % (760636)Peak memory usage: 91 MB
% 10.55/2.37 % (760636)Instructions burned: 114 (million)
% 10.55/2.37 % (760612)Instruction limit reached!
% 10.55/2.37 % (760612)------------------------------
% 10.55/2.37 % (760612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.37 % (760612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.37 % (760612)CaDiCaL version: 2.1.3
% 10.55/2.37 % (760612)Termination reason: Instruction limit
% 10.55/2.37 % (760612)Termination phase: Saturation
% 10.55/2.37 % (760612)Time elapsed: 0.155 s
% 10.55/2.37 % (760612)Peak memory usage: 88 MB
% 10.55/2.37 % (760612)Instructions burned: 296 (million)
% 10.55/2.37 % (760659)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2153587468:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 10.55/2.37 % (760668)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3359783515:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 10.55/2.37 % (760675)lrs+10_1_sil=8000:sp=occurrence:random_seed=2463155545:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 10.55/2.37 % (760668)Instruction limit reached!
% 10.55/2.37 % (760668)------------------------------
% 10.55/2.37 % (760668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.37 % (760668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.37 % (760668)CaDiCaL version: 2.1.3
% 10.55/2.37 % (760668)Termination reason: Instruction limit
% 10.55/2.37 % (760668)Termination phase: Saturation
% 10.55/2.37 % (760668)Time elapsed: 0.059 s
% 10.55/2.37 % (760668)Peak memory usage: 88 MB
% 10.55/2.37 % (760668)Instructions burned: 115 (million)
% 10.55/2.37 % (760659)Instruction limit reached!
% 10.55/2.37 % (760659)------------------------------
% 10.55/2.37 % (760659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.37 % (760659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.37 % (760659)CaDiCaL version: 2.1.3
% 10.55/2.37 % (760659)Termination reason: Instruction limit
% 10.55/2.37 % (760659)Termination phase: Saturation
% 10.55/2.37 % (760659)Time elapsed: 0.072 s
% 10.55/2.37 % (760659)Peak memory usage: 89 MB
% 10.55/2.37 % (760659)Instructions burned: 128 (million)
% 10.55/2.37 % (760704)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2972110716:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 10.55/2.37 % (760705)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=86111564:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 10.55/2.37 % (760497)First to succeed.
% 10.55/2.37 % (760497)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-760390"
% 10.55/2.37 % (760704)Instruction limit reached!
% 10.55/2.37 % (760704)------------------------------
% 10.55/2.37 % (760704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.37 % (760704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.37 % (760704)CaDiCaL version: 2.1.3
% 10.55/2.37 % (760704)Termination reason: Instruction limit
% 10.55/2.37 % (760704)Termination phase: Saturation
% 10.55/2.37 % (760704)Time elapsed: 0.241 s
% 10.55/2.37 % (760704)Peak memory usage: 89 MB
% 10.55/2.37 % (760704)Instructions burned: 437 (million)
% 10.55/2.37 % SZS status CounterSatisfiable for theBenchmark
% 10.55/2.37 % SZS output start Saturation.
% See solution above
% 11.19/2.56 % SZS output start Definitions and Model Updates.
% 11.19/2.56 % SZS output end Definitions and Model Updates.
% 11.19/2.56 % (760497)------------------------------
% 11.19/2.56 % (760497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.19/2.56 % (760497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.19/2.56 % (760497)CaDiCaL version: 2.1.3
% 11.19/2.56 % (760497)Termination reason: Satisfiable
% 11.19/2.56 % (760497)Time elapsed: 1.071 s
% 11.19/2.56 % (760497)Peak memory usage: 133 MB
% 11.19/2.56 % (760497)Instructions burned: 1587 (million)
% 11.19/2.56 % (760497)------------------------------
% 11.19/2.56 % (760497)------------------------------
% 11.19/2.56 % (760390)Success in time 1.506 s
% 11.19/2.56 % Vampire exiting
%------------------------------------------------------------------------------