%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL655+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 : n019.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:20 AM UTC 2026
% Result : CounterSatisfiable 3.04s 1.91s
% Output : Saturation 6.51s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u38,negated_conjecture,
~ r1(sK0,sK10) ).
cnf(u42,negated_conjecture,
p1(sK10) ).
cnf(u50,negated_conjecture,
r1(sK9,sK8(sK9)) ).
cnf(u58,negated_conjecture,
p1(sK0) ).
cnf(u71,negated_conjecture,
~ r1(sK9,sK7(sK9)) ).
cnf(u75,negated_conjecture,
( ~ r1(sK9,X0)
| p1(sK6(X1))
| ~ r1(X0,X1) ) ).
cnf(u86,negated_conjecture,
p1(sK4(sK9)) ).
cnf(u95,negated_conjecture,
~ r1(sK9,sK2(sK9)) ).
cnf(u99,negated_conjecture,
( ~ r1(sK9,X0)
| r1(X1,sK1(X1))
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u106,negated_conjecture,
r1(sK9,sK3(sK9)) ).
cnf(u118,negated_conjecture,
p1(sK9) ).
cnf(u130,negated_conjecture,
r1(sK3(sK9),sK4(sK9)) ).
cnf(u141,negated_conjecture,
~ r1(sK0,sK11) ).
cnf(u165,negated_conjecture,
~ r1(sK0,sK2(sK0)) ).
cnf(u169,negated_conjecture,
( ~ r1(sK0,X0)
| r1(X1,sK1(X1))
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u174,negated_conjecture,
r1(sK0,sK3(sK0)) ).
cnf(u182,negated_conjecture,
r1(sK3(sK0),sK4(sK0)) ).
cnf(u187,negated_conjecture,
p1(sK4(sK0)) ).
cnf(u192,negated_conjecture,
r1(sK0,sK7(sK0)) ).
cnf(u199,negated_conjecture,
( ~ r1(sK0,X0)
| p1(sK6(X1))
| ~ r1(X0,X1) ) ).
cnf(u204,negated_conjecture,
r1(sK0,sK8(sK0)) ).
cnf(u218,negated_conjecture,
~ r1(sK2(sK0),sK2(sK2(sK0))) ).
cnf(u230,negated_conjecture,
( ~ r1(sK2(sK0),X0)
| ~ p1(X2)
| ~ r1(X1,X2)
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u245,negated_conjecture,
r1(sK2(sK0),sK7(sK2(sK0))) ).
cnf(u256,negated_conjecture,
~ r1(sK2(sK0),sK8(sK2(sK0))) ).
cnf(u272,negated_conjecture,
r1(sK7(sK0),sK2(sK7(sK0))) ).
cnf(u275,negated_conjecture,
( ~ r1(sK7(sK0),X0)
| r1(X1,sK1(X1))
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u280,negated_conjecture,
r1(sK7(sK0),sK3(sK7(sK0))) ).
cnf(u288,negated_conjecture,
r1(sK3(sK7(sK0)),sK4(sK7(sK0))) ).
cnf(u293,negated_conjecture,
p1(sK4(sK7(sK0))) ).
cnf(u298,negated_conjecture,
r1(sK7(sK0),sK7(sK7(sK0))) ).
cnf(u310,negated_conjecture,
r1(sK7(sK0),sK8(sK7(sK0))) ).
cnf(u324,negated_conjecture,
~ r1(sK8(sK0),sK2(sK8(sK0))) ).
cnf(u328,negated_conjecture,
( ~ r1(sK8(sK0),X0)
| r1(X1,sK1(X1))
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u336,negated_conjecture,
( ~ r1(sK8(sK0),X0)
| ~ p1(X2)
| ~ r1(X1,X2)
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u351,negated_conjecture,
r1(sK8(sK0),sK7(sK8(sK0))) ).
cnf(u363,negated_conjecture,
r1(sK8(sK0),sK8(sK8(sK0))) ).
cnf(u449,negated_conjecture,
~ p1(sK8(sK0)) ).
cnf(u454,negated_conjecture,
p1(sK6(sK5(sK8(sK0)))) ).
cnf(u474,negated_conjecture,
~ p1(sK2(sK7(sK0))) ).
cnf(u482,negated_conjecture,
~ p1(sK7(sK7(sK0))) ).
cnf(u490,negated_conjecture,
~ p1(sK8(sK7(sK0))) ).
cnf(u523,negated_conjecture,
~ r1(sK9,sK0) ).
cnf(u527,negated_conjecture,
( ~ r1(sK6(sK0),X1)
| ~ p1(X0)
| p1(X1)
| ~ r1(X1,X0) ) ).
cnf(u548,negated_conjecture,
( ~ r1(sK6(sK0),X0)
| ~ p1(X2)
| ~ r1(X1,X2)
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u562,negated_conjecture,
~ r1(sK6(sK0),sK7(sK6(sK0))) ).
cnf(u574,negated_conjecture,
~ r1(sK6(sK0),sK8(sK6(sK0))) ).
cnf(u583,negated_conjecture,
p1(sK6(sK11)) ).
cnf(u693,negated_conjecture,
~ r1(sK9,sK8(sK0)) ).
cnf(u697,negated_conjecture,
r1(sK1(sK8(sK0)),sK1(sK1(sK8(sK0)))) ).
cnf(u700,negated_conjecture,
~ p1(sK1(sK8(sK0))) ).
cnf(u707,negated_conjecture,
~ r1(sK11,sK8(sK0)) ).
cnf(u712,negated_conjecture,
r1(sK8(sK0),sK1(sK8(sK0))) ).
cnf(u718,negated_conjecture,
r1(sK8(sK8(sK0)),sK1(sK8(sK8(sK0)))) ).
cnf(u721,negated_conjecture,
~ p1(sK8(sK8(sK0))) ).
cnf(u727,negated_conjecture,
r1(sK7(sK8(sK0)),sK1(sK7(sK8(sK0)))) ).
cnf(u730,negated_conjecture,
~ p1(sK7(sK8(sK0))) ).
cnf(u747,negated_conjecture,
r1(sK5(sK8(sK0)),sK1(sK5(sK8(sK0)))) ).
cnf(u874,negated_conjecture,
~ p1(sK8(sK9)) ).
cnf(u882,negated_conjecture,
~ p1(sK7(sK9)) ).
cnf(u890,negated_conjecture,
~ p1(sK3(sK9)) ).
cnf(u916,negated_conjecture,
r1(sK3(sK0),sK3(sK3(sK0))) ).
cnf(u924,negated_conjecture,
r1(sK3(sK3(sK0)),sK4(sK3(sK0))) ).
cnf(u929,negated_conjecture,
p1(sK4(sK3(sK0))) ).
cnf(u934,negated_conjecture,
r1(sK3(sK0),sK7(sK3(sK0))) ).
cnf(u946,negated_conjecture,
r1(sK3(sK0),sK8(sK3(sK0))) ).
cnf(u1034,negated_conjecture,
~ r1(sK11,sK10) ).
cnf(u1042,negated_conjecture,
~ r1(sK11,sK9) ).
cnf(u1054,negated_conjecture,
~ r1(sK11,sK0) ).
cnf(u1144,negated_conjecture,
~ p1(sK7(sK0)) ).
cnf(u1148,negated_conjecture,
( ~ r1(sK7(sK0),X0)
| ~ p1(X0) ) ).
cnf(u1305,negated_conjecture,
~ r1(sK11,sK3(sK0)) ).
cnf(u1308,negated_conjecture,
~ p1(sK3(sK0)) ).
cnf(u1313,negated_conjecture,
p1(sK6(sK1(sK3(sK0)))) ).
cnf(u1319,negated_conjecture,
~ r1(sK9,sK3(sK0)) ).
cnf(u1324,negated_conjecture,
p1(sK6(sK5(sK3(sK0)))) ).
cnf(u1339,negated_conjecture,
~ r1(sK11,sK7(sK0)) ).
cnf(u1343,negated_conjecture,
p1(sK6(sK1(sK7(sK0)))) ).
cnf(u1349,negated_conjecture,
~ r1(sK9,sK7(sK0)) ).
cnf(u1354,negated_conjecture,
p1(sK6(sK5(sK7(sK0)))) ).
cnf(u1372,negated_conjecture,
~ r1(sK11,sK3(sK9)) ).
cnf(u1376,negated_conjecture,
r1(sK1(sK3(sK9)),sK1(sK1(sK3(sK9)))) ).
cnf(u1379,negated_conjecture,
~ p1(sK1(sK3(sK9))) ).
cnf(u1385,negated_conjecture,
~ r1(sK0,sK3(sK9)) ).
cnf(u1420,negated_conjecture,
p1(sK1(sK7(sK9))) ).
cnf(u1425,negated_conjecture,
~ r1(sK0,sK7(sK9)) ).
cnf(u1448,negated_conjecture,
~ r1(sK11,sK8(sK9)) ).
cnf(u1452,negated_conjecture,
r1(sK1(sK8(sK9)),sK1(sK1(sK8(sK9)))) ).
cnf(u1455,negated_conjecture,
~ p1(sK1(sK8(sK9))) ).
cnf(u1461,negated_conjecture,
~ r1(sK0,sK8(sK9)) ).
cnf(u1486,negated_conjecture,
r1(sK1(sK7(sK0)),sK1(sK1(sK7(sK0)))) ).
cnf(u1489,negated_conjecture,
~ p1(sK1(sK7(sK0))) ).
cnf(u1497,negated_conjecture,
r1(sK7(sK0),sK1(sK7(sK0))) ).
cnf(u1507,negated_conjecture,
r1(sK5(sK7(sK0)),sK1(sK5(sK7(sK0)))) ).
cnf(u1521,negated_conjecture,
r1(sK1(sK3(sK0)),sK1(sK1(sK3(sK0)))) ).
cnf(u1524,negated_conjecture,
~ p1(sK1(sK3(sK0))) ).
cnf(u1532,negated_conjecture,
r1(sK3(sK0),sK1(sK3(sK0))) ).
cnf(u1537,negated_conjecture,
r1(sK8(sK3(sK0)),sK1(sK8(sK3(sK0)))) ).
cnf(u1540,negated_conjecture,
~ p1(sK8(sK3(sK0))) ).
cnf(u1546,negated_conjecture,
r1(sK7(sK3(sK0)),sK1(sK7(sK3(sK0)))) ).
cnf(u1549,negated_conjecture,
~ p1(sK7(sK3(sK0))) ).
cnf(u1557,negated_conjecture,
r1(sK5(sK3(sK0)),sK1(sK5(sK3(sK0)))) ).
cnf(u1605,negated_conjecture,
( ~ r1(sK1(sK7(sK0)),X0)
| ~ p1(X0) ) ).
cnf(u1692,negated_conjecture,
( ~ r1(sK1(sK7(sK0)),X0)
| r1(X0,sK1(X0)) ) ).
cnf(u1725,negated_conjecture,
~ r1(sK9,sK2(sK0)) ).
cnf(u1728,negated_conjecture,
~ p1(sK2(sK0)) ).
cnf(u1737,negated_conjecture,
~ r1(sK11,sK2(sK0)) ).
cnf(u1762,negated_conjecture,
( ~ r1(sK1(sK7(sK0)),X1)
| ~ p1(X0)
| ~ r1(X1,X0) ) ).
cnf(u2034,negated_conjecture,
~ r1(sK11,sK1(sK7(sK0))) ).
cnf(u2038,negated_conjecture,
~ p1(sK1(sK1(sK7(sK0)))) ).
cnf(u2043,negated_conjecture,
~ r1(sK0,sK1(sK7(sK0))) ).
cnf(u2048,negated_conjecture,
~ r1(sK9,sK1(sK7(sK0))) ).
cnf(u2064,negated_conjecture,
~ p1(sK1(sK7(sK8(sK0)))) ).
cnf(u2074,negated_conjecture,
~ p1(sK1(sK7(sK7(sK0)))) ).
cnf(u2086,negated_conjecture,
~ p1(sK1(sK7(sK3(sK0)))) ).
cnf(u2109,negated_conjecture,
~ r1(sK0,sK8(sK8(sK0))) ).
cnf(u2118,negated_conjecture,
~ r1(sK11,sK8(sK8(sK0))) ).
cnf(u2122,negated_conjecture,
r1(sK1(sK8(sK8(sK0))),sK6(sK1(sK8(sK8(sK0))))) ).
cnf(u2128,negated_conjecture,
~ r1(sK9,sK8(sK8(sK0))) ).
cnf(u2140,negated_conjecture,
~ r1(sK0,sK7(sK8(sK0))) ).
cnf(u2149,negated_conjecture,
~ r1(sK11,sK7(sK8(sK0))) ).
cnf(u2159,negated_conjecture,
~ r1(sK9,sK7(sK8(sK0))) ).
cnf(u2167,negated_conjecture,
~ p1(sK6(sK7(sK6(sK0)))) ).
cnf(u2200,negated_conjecture,
p1(sK6(sK6(sK0))) ).
cnf(u2248,negated_conjecture,
~ r1(sK11,sK1(sK1(sK7(sK0)))) ).
cnf(u2252,negated_conjecture,
~ p1(sK1(sK1(sK1(sK7(sK0))))) ).
cnf(u2262,negated_conjecture,
~ r1(sK9,sK1(sK1(sK7(sK0)))) ).
cnf(u2297,negated_conjecture,
r1(sK1(sK2(sK7(sK0))),sK1(sK1(sK2(sK7(sK0))))) ).
cnf(u2300,negated_conjecture,
~ p1(sK1(sK2(sK7(sK0)))) ).
cnf(u2312,negated_conjecture,
~ r1(sK0,sK2(sK7(sK0))) ).
cnf(u2342,negated_conjecture,
~ r1(sK0,sK7(sK7(sK0))) ).
cnf(u2361,negated_conjecture,
r1(sK1(sK8(sK7(sK0))),sK1(sK1(sK8(sK7(sK0))))) ).
cnf(u2364,negated_conjecture,
~ p1(sK1(sK8(sK7(sK0)))) ).
cnf(u2376,negated_conjecture,
~ r1(sK0,sK8(sK7(sK0))) ).
cnf(u2402,negated_conjecture,
r1(sK1(sK8(sK8(sK0))),sK1(sK1(sK8(sK8(sK0))))) ).
cnf(u2405,negated_conjecture,
~ p1(sK1(sK8(sK8(sK0)))) ).
cnf(u2429,negated_conjecture,
r1(sK1(sK7(sK8(sK0))),sK1(sK1(sK7(sK8(sK0))))) ).
cnf(u2454,negated_conjecture,
( ~ r1(sK2(sK0),X0)
| ~ p1(X0) ) ).
cnf(u2459,negated_conjecture,
p1(sK8(sK2(sK0))) ).
cnf(u2466,negated_conjecture,
~ p1(sK7(sK2(sK0))) ).
cnf(u2470,negated_conjecture,
( ~ r1(sK7(sK2(sK0)),X0)
| ~ p1(X0) ) ).
cnf(u2544,negated_conjecture,
( ~ r1(sK1(sK8(sK0)),X0)
| ~ p1(X0) ) ).
cnf(u2548,negated_conjecture,
( ~ r1(sK8(sK8(sK0)),X0)
| ~ p1(X0) ) ).
cnf(u2586,negated_conjecture,
( ~ r1(sK8(sK3(sK0)),X0)
| ~ p1(X0) ) ).
cnf(u2590,negated_conjecture,
( ~ r1(sK7(sK3(sK0)),X0)
| ~ p1(X0) ) ).
cnf(u2606,negated_conjecture,
r1(sK3(sK3(sK0)),sK1(sK3(sK3(sK0)))) ).
cnf(u2609,negated_conjecture,
~ p1(sK3(sK3(sK0))) ).
cnf(u2654,negated_conjecture,
~ r1(sK11,sK7(sK2(sK0))) ).
cnf(u2658,negated_conjecture,
~ p1(sK1(sK7(sK2(sK0)))) ).
cnf(u2663,negated_conjecture,
~ r1(sK0,sK7(sK2(sK0))) ).
cnf(u2668,negated_conjecture,
~ r1(sK9,sK7(sK2(sK0))) ).
cnf(u2688,negated_conjecture,
r1(sK1(sK5(sK7(sK0))),sK1(sK1(sK5(sK7(sK0))))) ).
cnf(u2691,negated_conjecture,
~ p1(sK1(sK5(sK7(sK0)))) ).
cnf(u2697,negated_conjecture,
~ r1(sK0,sK5(sK7(sK0))) ).
cnf(u2720,negated_conjecture,
~ r1(sK11,sK5(sK8(sK0))) ).
cnf(u2723,negated_conjecture,
~ p1(sK5(sK8(sK0))) ).
cnf(u2728,negated_conjecture,
r1(sK1(sK5(sK8(sK0))),sK1(sK1(sK5(sK8(sK0))))) ).
cnf(u2731,negated_conjecture,
~ p1(sK1(sK5(sK8(sK0)))) ).
cnf(u2737,negated_conjecture,
~ r1(sK0,sK5(sK8(sK0))) ).
cnf(u2742,negated_conjecture,
~ r1(sK9,sK5(sK8(sK0))) ).
cnf(u2764,negated_conjecture,
~ r1(sK0,sK7(sK3(sK0))) ).
cnf(u2773,negated_conjecture,
~ r1(sK11,sK7(sK3(sK0))) ).
cnf(u2777,negated_conjecture,
r1(sK1(sK7(sK3(sK0))),sK1(sK1(sK7(sK3(sK0))))) ).
cnf(u2783,negated_conjecture,
~ r1(sK9,sK7(sK3(sK0))) ).
cnf(u2796,negated_conjecture,
~ r1(sK11,sK8(sK3(sK0))) ).
cnf(u2799,negated_conjecture,
~ p1(sK1(sK8(sK3(sK0)))) ).
cnf(u2804,negated_conjecture,
r1(sK1(sK8(sK3(sK0))),sK1(sK1(sK8(sK3(sK0))))) ).
cnf(u2809,negated_conjecture,
~ r1(sK0,sK8(sK3(sK0))) ).
cnf(u2814,negated_conjecture,
~ r1(sK9,sK8(sK3(sK0))) ).
cnf(u2844,negated_conjecture,
r1(sK1(sK5(sK3(sK0))),sK1(sK1(sK5(sK3(sK0))))) ).
cnf(u2849,negated_conjecture,
~ r1(sK0,sK5(sK3(sK0))) ).
cnf(u2875,negated_conjecture,
~ p1(sK1(sK1(sK3(sK0)))) ).
cnf(u2880,negated_conjecture,
r1(sK1(sK1(sK3(sK0))),sK1(sK1(sK1(sK3(sK0))))) ).
cnf(u2885,negated_conjecture,
~ r1(sK0,sK1(sK3(sK0))) ).
cnf(u2921,negated_conjecture,
~ p1(sK1(sK3(sK3(sK0)))) ).
cnf(u2926,negated_conjecture,
r1(sK1(sK3(sK3(sK0))),sK1(sK1(sK3(sK3(sK0))))) ).
cnf(u2937,negated_conjecture,
~ r1(sK0,sK3(sK3(sK0))) ).
cnf(u3037,negated_conjecture,
( ~ r1(sK1(sK8(sK8(sK0))),X0)
| ~ p1(X0) ) ).
cnf(u3085,negated_conjecture,
( ~ r1(sK1(sK5(sK7(sK0))),X0)
| ~ p1(X0) ) ).
cnf(u3098,negated_conjecture,
( ~ r1(sK1(sK5(sK8(sK0))),X0)
| ~ p1(X0) ) ).
cnf(u3246,negated_conjecture,
r1(sK1(sK3(sK7(sK0))),sK1(sK1(sK3(sK7(sK0))))) ).
cnf(u3261,negated_conjecture,
~ r1(sK0,sK3(sK7(sK0))) ).
cnf(u3350,negated_conjecture,
~ r1(sK11,sK1(sK8(sK8(sK0)))) ).
cnf(u3354,negated_conjecture,
~ p1(sK1(sK1(sK8(sK8(sK0))))) ).
cnf(u3364,negated_conjecture,
~ r1(sK9,sK1(sK8(sK8(sK0)))) ).
cnf(u3377,negated_conjecture,
~ r1(sK11,sK1(sK7(sK8(sK0)))) ).
cnf(u3381,negated_conjecture,
~ p1(sK1(sK1(sK7(sK8(sK0))))) ).
cnf(u3391,negated_conjecture,
~ r1(sK9,sK1(sK7(sK8(sK0)))) ).
cnf(u3401,negated_conjecture,
~ r1(sK11,sK1(sK5(sK7(sK0)))) ).
cnf(u3405,negated_conjecture,
~ p1(sK1(sK1(sK5(sK7(sK0))))) ).
cnf(u3415,negated_conjecture,
~ r1(sK9,sK1(sK5(sK7(sK0)))) ).
cnf(u3429,negated_conjecture,
~ r1(sK11,sK1(sK5(sK8(sK0)))) ).
cnf(u3433,negated_conjecture,
~ p1(sK1(sK1(sK5(sK8(sK0))))) ).
cnf(u3443,negated_conjecture,
~ r1(sK9,sK1(sK5(sK8(sK0)))) ).
cnf(u3611,negated_conjecture,
p1(sK6(sK6(sK11))) ).
cnf(u3615,negated_conjecture,
~ r1(sK10,sK11) ).
cnf(u3620,negated_conjecture,
( ~ r1(sK6(sK9),X0)
| r1(X0,sK1(X0))
| p1(X0) ) ).
cnf(u3624,negated_conjecture,
~ r1(sK10,sK9) ).
cnf(u3629,negated_conjecture,
p1(sK6(sK6(sK9))) ).
cnf(u3633,negated_conjecture,
( ~ r1(sK6(sK9),X0)
| p1(sK6(X0)) ) ).
cnf(u3637,negated_conjecture,
( ~ r1(sK6(sK9),X0)
| r1(X0,sK6(X0)) ) ).
cnf(u3642,negated_conjecture,
p1(sK6(sK6(sK8(sK9)))) ).
cnf(u3646,negated_conjecture,
~ r1(sK10,sK8(sK9)) ).
cnf(u3654,negated_conjecture,
~ r1(sK10,sK8(sK0)) ).
cnf(u3674,negated_conjecture,
~ r1(sK10,sK7(sK0)) ).
cnf(u3687,negated_conjecture,
p1(sK6(sK6(sK3(sK9)))) ).
cnf(u3691,negated_conjecture,
~ r1(sK10,sK3(sK9)) ).
cnf(u3700,negated_conjecture,
~ r1(sK10,sK3(sK0)) ).
cnf(u3712,negated_conjecture,
~ r1(sK10,sK2(sK0)) ).
cnf(u3726,negated_conjecture,
~ r1(sK10,sK1(sK7(sK0))) ).
cnf(u3741,negated_conjecture,
~ r1(sK10,sK0) ).
cnf(u4034,negated_conjecture,
~ r1(sK10,sK6(sK9)) ).
cnf(u4038,negated_conjecture,
p1(sK6(sK6(sK6(sK9)))) ).
cnf(u4043,negated_conjecture,
~ r1(sK11,sK6(sK9)) ).
cnf(u4047,negated_conjecture,
r1(sK9,sK6(sK9)) ).
cnf(u4104,negated_conjecture,
~ r1(sK0,sK1(sK8(sK0))) ).
cnf(u4157,negated_conjecture,
~ r1(sK0,sK1(sK1(sK8(sK0)))) ).
cnf(u4161,negated_conjecture,
~ p1(sK1(sK1(sK1(sK8(sK0))))) ).
cnf(u4194,negated_conjecture,
~ r1(sK10,sK6(sK0)) ).
cnf(u4199,negated_conjecture,
~ r1(sK11,sK6(sK0)) ).
cnf(u4204,negated_conjecture,
~ r1(sK9,sK6(sK0)) ).
cnf(u4050,negated_conjecture,
r1(sK6(sK9),sK6(sK6(sK9))) ).
cnf(u829,negated_conjecture,
( ~ p1(sK1(sK7(X0)))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| r1(X2,sK6(X2))
| ~ r1(sK0,X0)
| ~ r1(sK9,sK7(X0)) ) ).
cnf(u1768,negated_conjecture,
( ~ r1(sK1(sK8(sK0)),X1)
| ~ r1(X1,X0)
| p1(X1)
| ~ p1(X0) ) ).
cnf(u1916,negated_conjecture,
( ~ r1(sK4(sK0),X0)
| r1(X0,sK1(X0))
| p1(X0) ) ).
cnf(u1293,negated_conjecture,
p1(sK6(sK4(sK0))) ).
cnf(u681,negated_conjecture,
( ~ p1(sK1(sK7(X0)))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| r1(X2,sK6(X2))
| ~ r1(sK0,X0)
| ~ r1(sK11,sK7(X0)) ) ).
cnf(u1295,negated_conjecture,
p1(sK6(sK8(sK3(sK0)))) ).
cnf(u1839,negated_conjecture,
( ~ r1(sK5(sK8(sK0)),X1)
| ~ r1(X1,X0)
| p1(X1)
| ~ p1(X0) ) ).
cnf(u1281,negated_conjecture,
p1(sK6(sK3(sK0))) ).
cnf(u1259,negated_conjecture,
p1(sK6(sK1(sK8(sK0)))) ).
cnf(u1714,negated_conjecture,
( ~ r1(sK7(sK2(sK0)),X1)
| ~ r1(X1,X0)
| p1(X1)
| ~ p1(X0) ) ).
cnf(u1294,negated_conjecture,
p1(sK6(sK7(sK3(sK0)))) ).
cnf(u3649,negated_conjecture,
~ r1(sK10,sK8(sK3(sK0))) ).
cnf(u440,negated_conjecture,
p1(sK6(sK0)) ).
cnf(u1984,negated_conjecture,
p1(sK6(sK4(sK9))) ).
cnf(u4149,negated_conjecture,
~ r1(sK11,sK1(sK1(sK8(sK0)))) ).
cnf(u828,negated_conjecture,
( ~ p1(sK1(sK7(X0)))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(sK6(X2))
| ~ r1(sK0,X0)
| ~ r1(sK9,sK7(X0)) ) ).
cnf(u1699,negated_conjecture,
( ~ r1(sK7(sK8(sK0)),X0)
| p1(X0)
| r1(X0,sK1(X0)) ) ).
cnf(u32,axiom,
r1(X0,X0) ).
cnf(u391,negated_conjecture,
( ~ r1(sK8(sK0),X0)
| p1(sK6(X0)) ) ).
cnf(u1500,negated_conjecture,
r1(sK7(sK7(sK0)),sK1(sK7(sK7(sK0)))) ).
cnf(u26,negated_conjecture,
( ~ r1(sK2(X1),X6)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| ~ p1(sK1(X3))
| ~ r1(sK0,X1)
| p1(X6) ) ).
cnf(u25,negated_conjecture,
( ~ r1(sK0,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p1(X9)
| ~ r1(X9,X10)
| ~ p1(X10)
| r1(X7,sK3(X7)) ) ).
cnf(u3683,negated_conjecture,
~ r1(sK10,sK5(sK8(sK0))) ).
cnf(u28,negated_conjecture,
( ~ p1(sK1(X3))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| ~ r1(sK0,X1)
| r1(X1,sK2(X1)) ) ).
cnf(u3716,negated_conjecture,
~ r1(sK10,sK1(sK8(sK0))) ).
cnf(u19,negated_conjecture,
( ~ r1(sK0,X15)
| ~ r1(X15,X16)
| ~ r1(X16,X17)
| r1(X17,sK6(X17))
| r1(X15,sK7(X15)) ) ).
cnf(u22,negated_conjecture,
( ~ r1(sK0,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p1(X9)
| ~ r1(X9,X10)
| ~ p1(X10)
| p1(sK4(X7)) ) ).
cnf(u21,negated_conjecture,
( r1(X13,sK5(X13))
| p1(X13)
| ~ r1(sK0,X13) ) ).
cnf(u4079,negated_conjecture,
~ p1(sK6(sK1(sK8(sK8(sK0))))) ).
cnf(u3522,negated_conjecture,
( r1(X0,sK6(X0))
| ~ r1(sK10,X0) ) ).
cnf(u3521,negated_conjecture,
( ~ r1(sK8(sK9),X0)
| r1(X0,sK6(X0)) ) ).
cnf(u15,negated_conjecture,
( ~ r1(sK0,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| p1(X23)
| r1(X21,sK8(X21)) ) ).
cnf(u464,negated_conjecture,
( ~ r1(sK7(sK0),X0)
| p1(X0)
| r1(X0,sK1(X0)) ) ).
cnf(u1472,negated_conjecture,
( ~ r1(X1,sK7(sK9))
| ~ r1(X0,X1)
| ~ r1(sK0,X0)
| r1(X0,sK2(X0)) ) ).
cnf(u3995,negated_conjecture,
r1(sK4(sK9),sK6(sK4(sK9))) ).
cnf(u1670,negated_conjecture,
( ~ r1(sK2(sK7(sK0)),X0)
| p1(X0)
| r1(X0,sK1(X0)) ) ).
cnf(u3734,negated_conjecture,
~ r1(sK10,sK1(sK1(sK7(sK0)))) ).
cnf(u1327,negated_conjecture,
p1(sK6(sK2(sK7(sK0)))) ).
cnf(u3523,negated_conjecture,
( r1(X0,sK6(X0))
| ~ r1(sK11,X0) ) ).
cnf(u3648,negated_conjecture,
~ r1(sK10,sK8(sK8(sK0))) ).
cnf(u2006,negated_conjecture,
p1(sK6(sK1(sK8(sK9)))) ).
cnf(u1291,negated_conjecture,
( ~ r1(sK7(sK0),X0)
| p1(sK6(X0)) ) ).
cnf(u406,negated_conjecture,
p1(sK6(sK10)) ).
cnf(u3681,negated_conjecture,
( ~ r1(sK10,sK7(X0))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(sK6(X2))
| ~ r1(sK0,X0) ) ).
cnf(u2552,negated_conjecture,
( ~ r1(sK5(sK8(sK0)),X0)
| ~ p1(X0) ) ).
cnf(u1769,negated_conjecture,
( ~ r1(sK7(sK8(sK0)),X1)
| ~ r1(X1,X0)
| p1(X1)
| ~ p1(X0) ) ).
cnf(u2224,negated_conjecture,
( ~ r1(sK1(sK1(sK7(sK0))),X0)
| ~ p1(X0) ) ).
cnf(u2640,negated_conjecture,
( ~ r1(sK3(sK3(sK0)),X0)
| r1(X0,sK1(X0))
| p1(X0) ) ).
cnf(u156,negated_conjecture,
( ~ p1(sK7(X0))
| ~ r1(X1,X2)
| p1(sK6(X2))
| ~ r1(sK0,X0)
| ~ r1(X0,X1) ) ).
cnf(u433,negated_conjecture,
( r1(X0,sK1(X0))
| p1(X0)
| ~ r1(sK11,X0) ) ).
cnf(u4004,negated_conjecture,
r1(sK6(sK3(sK9)),sK6(sK6(sK3(sK9)))) ).
cnf(u4148,negated_conjecture,
~ r1(sK10,sK1(sK1(sK8(sK0)))) ).
cnf(u429,negated_conjecture,
( ~ r1(sK3(sK9),X0)
| p1(X0)
| r1(X0,sK1(X0)) ) ).
cnf(u1981,negated_conjecture,
p1(sK6(sK1(sK11))) ).
cnf(u409,negated_conjecture,
p1(sK6(sK9)) ).
cnf(u403,negated_conjecture,
p1(sK6(sK3(sK9))) ).
cnf(u1716,negated_conjecture,
( ~ r1(sK2(sK0),X1)
| ~ r1(X1,X0)
| p1(X1)
| ~ p1(X0) ) ).
cnf(u405,negated_conjecture,
p1(sK6(sK8(sK9))) ).
cnf(u1328,negated_conjecture,
p1(sK6(sK7(sK7(sK0)))) ).
cnf(u4098,negated_conjecture,
r1(sK1(sK1(sK8(sK0))),sK1(sK1(sK1(sK8(sK0))))) ).
cnf(u1847,negated_conjecture,
( ~ r1(sK3(sK0),X0)
| p1(X1)
| r1(X1,sK1(X1))
| ~ r1(X0,X1) ) ).
cnf(u1926,negated_conjecture,
( ~ r1(sK5(sK3(sK0)),X0)
| r1(X0,sK1(X0))
| p1(X0) ) ).
cnf(u3664,negated_conjecture,
~ r1(sK10,sK7(sK8(sK0))) ).
cnf(u3715,negated_conjecture,
~ r1(sK10,sK1(sK8(sK8(sK0)))) ).
cnf(u3159,negated_conjecture,
r1(sK3(sK7(sK0)),sK1(sK3(sK7(sK0)))) ).
cnf(u1963,negated_conjecture,
( ~ r1(sK11,X0)
| p1(sK6(X0)) ) ).
cnf(u912,negated_conjecture,
( ~ r1(sK3(sK0),X0)
| p1(X0)
| r1(X0,sK1(X0)) ) ).
cnf(u3733,negated_conjecture,
~ r1(sK10,sK1(sK5(sK7(sK0)))) ).
cnf(u3158,negated_conjecture,
p1(sK6(sK3(sK7(sK0)))) ).
cnf(u680,negated_conjecture,
( ~ p1(sK1(sK7(X0)))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(sK6(X2))
| ~ r1(sK0,X0)
| ~ r1(sK11,sK7(X0)) ) ).
cnf(u808,negated_conjecture,
( ~ p1(sK1(sK7(X0)))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| r1(X2,sK6(X2))
| ~ r1(sK0,X0)
| ~ r1(sK0,sK7(X0)) ) ).
cnf(u1698,negated_conjecture,
( ~ r1(sK1(sK8(sK0)),X0)
| p1(X0)
| r1(X0,sK1(X0)) ) ).
cnf(u1697,negated_conjecture,
( ~ r1(sK8(sK8(sK0)),X0)
| p1(X0)
| r1(X0,sK1(X0)) ) ).
cnf(u442,negated_conjecture,
p1(sK6(sK7(sK8(sK0)))) ).
cnf(u438,negated_conjecture,
p1(sK6(sK8(sK0))) ).
cnf(u399,negated_conjecture,
( ~ r1(sK8(sK0),X0)
| p1(X0)
| r1(X0,sK1(X0)) ) ).
cnf(u443,negated_conjecture,
p1(sK6(sK8(sK8(sK0)))) ).
cnf(u3964,negated_conjecture,
( ~ r1(sK9,sK7(X0))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| r1(X2,sK6(X2))
| ~ r1(sK0,X0) ) ).
cnf(u23,negated_conjecture,
( ~ r1(sK0,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p1(X9)
| ~ r1(X9,X10)
| ~ p1(X10)
| r1(sK3(X7),sK4(X7)) ) ).
cnf(u27,negated_conjecture,
( ~ p1(sK2(X1))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| ~ p1(sK1(X3))
| ~ r1(sK0,X1) ) ).
cnf(u4150,negated_conjecture,
~ r1(sK9,sK1(sK1(sK8(sK0)))) ).
cnf(u30,negated_conjecture,
( ~ p1(sK2(X1))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X3,sK1(X3))
| ~ r1(sK0,X1) ) ).
cnf(u29,negated_conjecture,
( ~ r1(sK2(X1),X6)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X3,sK1(X3))
| ~ r1(sK0,X1)
| p1(X6) ) ).
cnf(u16,negated_conjecture,
( ~ r1(sK7(X15),X20)
| ~ r1(X15,X16)
| ~ r1(X16,X17)
| p1(sK6(X17))
| ~ r1(sK0,X15)
| ~ p1(X20) ) ).
cnf(u1292,negated_conjecture,
p1(sK6(sK7(sK0))) ).
cnf(u10,negated_conjecture,
r1(sK9,sK11) ).
cnf(u9,negated_conjecture,
~ p1(sK11) ).
cnf(u12,negated_conjecture,
r1(sK9,sK10) ).
cnf(u4007,negated_conjecture,
r1(sK8(sK9),sK6(sK8(sK9))) ).
cnf(u162,negated_conjecture,
( ~ r1(sK0,X0)
| ~ r1(X1,X2)
| p1(X2)
| r1(X2,sK1(X2))
| ~ r1(X0,X1) ) ).
cnf(u161,negated_conjecture,
( ~ p1(sK1(X2))
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X0,X1)
| ~ r1(sK0,X0) ) ).
cnf(u3849,negated_conjecture,
~ r1(sK11,sK1(sK8(sK0))) ).
cnf(u4063,negated_conjecture,
r1(sK6(sK6(sK9)),sK6(sK6(sK6(sK9)))) ).
cnf(u1280,negated_conjecture,
( ~ r1(sK3(sK0),X0)
| p1(sK6(X0)) ) ).
cnf(u435,negated_conjecture,
( r1(X0,sK1(X0))
| p1(X0)
| ~ r1(sK9,X0) ) ).
cnf(u1837,negated_conjecture,
( ~ r1(sK5(sK8(sK0)),X0)
| p1(X0)
| r1(X0,sK1(X0)) ) ).
cnf(u1671,negated_conjecture,
( ~ r1(sK7(sK7(sK0)),X0)
| p1(X0)
| r1(X0,sK1(X0)) ) ).
cnf(u4015,negated_conjecture,
r1(sK6(sK8(sK9)),sK6(sK6(sK8(sK9)))) ).
cnf(u3520,negated_conjecture,
( ~ r1(sK3(sK9),X0)
| r1(X0,sK6(X0)) ) ).
cnf(u1499,negated_conjecture,
r1(sK8(sK7(sK0)),sK1(sK8(sK7(sK0)))) ).
cnf(u1501,negated_conjecture,
r1(sK2(sK7(sK0)),sK1(sK2(sK7(sK0)))) ).
cnf(u3994,negated_conjecture,
r1(sK1(sK3(sK9)),sK6(sK1(sK3(sK9)))) ).
cnf(u1767,negated_conjecture,
( ~ r1(sK8(sK8(sK0)),X1)
| ~ r1(X1,X0)
| p1(X1)
| ~ p1(X0) ) ).
cnf(u3155,negated_conjecture,
( ~ r1(sK3(sK7(sK0)),X0)
| p1(X0)
| r1(X0,sK1(X0)) ) ).
cnf(u3157,negated_conjecture,
~ p1(sK3(sK7(sK0))) ).
cnf(u1962,negated_conjecture,
( ~ r1(sK10,X0)
| p1(sK6(X0)) ) ).
cnf(u1672,negated_conjecture,
( ~ r1(sK8(sK7(sK0)),X0)
| p1(X0)
| r1(X0,sK1(X0)) ) ).
cnf(u1918,negated_conjecture,
( ~ r1(sK8(sK3(sK0)),X0)
| r1(X0,sK1(X0))
| p1(X0) ) ).
cnf(u390,negated_conjecture,
( ~ r1(sK9,X0)
| p1(sK6(X0)) ) ).
cnf(u3665,negated_conjecture,
~ r1(sK10,sK7(sK3(sK0))) ).
cnf(u155,negated_conjecture,
( ~ p1(sK7(X0))
| ~ r1(X1,X2)
| r1(X2,sK6(X2))
| ~ r1(sK0,X0)
| ~ r1(X0,X1) ) ).
cnf(u2602,negated_conjecture,
p1(sK6(sK3(sK3(sK0)))) ).
cnf(u3617,negated_conjecture,
p1(sK6(sK6(sK10))) ).
cnf(u431,negated_conjecture,
( ~ r1(sK8(sK9),X0)
| p1(X0)
| r1(X0,sK1(X0)) ) ).
cnf(u401,negated_conjecture,
( r1(X0,sK1(X0))
| p1(X0)
| ~ r1(sK0,X0) ) ).
cnf(u134,negated_conjecture,
( ~ r1(sK0,sK2(X0))
| ~ r1(X1,X2)
| p1(X2)
| r1(X2,sK1(X2))
| ~ r1(sK0,X0)
| p1(sK5(sK2(X0)))
| ~ r1(X0,X1) ) ).
cnf(u807,negated_conjecture,
( ~ p1(sK1(sK7(X0)))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(sK6(X2))
| ~ r1(sK0,X0)
| ~ r1(sK0,sK7(X0)) ) ).
cnf(u3845,negated_conjecture,
( ~ r1(sK11,sK7(X0))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| r1(X2,sK6(X2))
| ~ r1(sK0,X0) ) ).
cnf(u1927,negated_conjecture,
( ~ r1(sK1(sK3(sK0)),X0)
| r1(X0,sK1(X0))
| p1(X0) ) ).
cnf(u393,negated_conjecture,
( ~ r1(sK0,X0)
| p1(sK6(X0)) ) ).
cnf(u3996,negated_conjecture,
r1(sK3(sK9),sK6(sK3(sK9))) ).
cnf(u3732,negated_conjecture,
~ r1(sK10,sK1(sK5(sK8(sK0)))) ).
cnf(u1473,negated_conjecture,
( ~ r1(X0,sK7(sK9))
| ~ r1(X1,X0)
| ~ r1(sK0,X1) ) ).
cnf(u24,negated_conjecture,
( ~ p1(sK3(X7))
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p1(X9)
| ~ r1(X9,X10)
| ~ p1(X10)
| ~ r1(sK0,X7) ) ).
cnf(u3216,negated_conjecture,
~ p1(sK1(sK1(sK8(sK0)))) ).
cnf(u2174,negated_conjecture,
r1(sK1(sK1(sK7(sK0))),sK1(sK1(sK1(sK7(sK0))))) ).
cnf(u31,negated_conjecture,
( ~ r1(sK0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X3,sK1(X3))
| r1(X1,sK2(X1)) ) ).
cnf(u3524,negated_conjecture,
( r1(X0,sK6(X0))
| ~ r1(sK9,X0) ) ).
cnf(u18,negated_conjecture,
( ~ r1(sK7(X15),X20)
| ~ r1(X15,X16)
| ~ r1(X16,X17)
| r1(X17,sK6(X17))
| ~ r1(sK0,X15)
| ~ p1(X20) ) ).
cnf(u17,negated_conjecture,
( ~ r1(sK0,X15)
| ~ r1(X15,X16)
| ~ r1(X16,X17)
| p1(sK6(X17))
| r1(X15,sK7(X15)) ) ).
cnf(u1983,negated_conjecture,
p1(sK6(sK1(sK3(sK9)))) ).
cnf(u1836,negated_conjecture,
( ~ r1(sK5(sK7(sK0)),X0)
| p1(X0)
| r1(X0,sK1(X0)) ) ).
cnf(u1770,negated_conjecture,
( ~ r1(sK8(sK0),X1)
| ~ r1(X1,X0)
| p1(X1)
| ~ p1(X0) ) ).
cnf(u124,negated_conjecture,
( ~ r1(sK0,sK2(X0))
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(sK1(X2))
| ~ r1(sK0,X0)
| p1(sK5(sK2(X0)))
| ~ r1(X0,X1) ) ).
cnf(u2541,negated_conjecture,
( ~ r1(sK7(sK8(sK0)),X0)
| ~ p1(X0) ) ).
cnf(u4006,negated_conjecture,
r1(sK1(sK8(sK9)),sK6(sK1(sK8(sK9)))) ).
cnf(u3717,negated_conjecture,
~ r1(sK10,sK1(sK7(sK8(sK0)))) ).
cnf(u2540,negated_conjecture,
( ~ r1(sK8(sK0),X0)
| ~ p1(X0) ) ).
cnf(u1329,negated_conjecture,
p1(sK6(sK8(sK7(sK0)))) ).
cnf(u1443,negated_conjecture,
r1(sK8(sK9),sK1(sK8(sK9))) ).
cnf(u1367,negated_conjecture,
r1(sK3(sK9),sK1(sK3(sK9))) ).
cnf(u1961,negated_conjecture,
( ~ r1(sK8(sK9),X0)
| p1(sK6(X0)) ) ).
cnf(u3682,negated_conjecture,
( ~ r1(sK10,sK7(X0))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| r1(X2,sK6(X2))
| ~ r1(sK0,X0) ) ).
cnf(u3666,negated_conjecture,
~ r1(sK10,sK7(sK2(sK0))) ).
cnf(u1917,negated_conjecture,
( ~ r1(sK7(sK3(sK0)),X0)
| r1(X0,sK1(X0))
| p1(X0) ) ).
cnf(u20,negated_conjecture,
( ~ p1(sK5(X13))
| p1(X13)
| ~ r1(sK0,X13) ) ).
cnf(u11,negated_conjecture,
( ~ r1(sK10,X27)
| p1(X27) ) ).
cnf(u14,negated_conjecture,
( ~ p1(sK8(X21))
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| p1(X23)
| ~ r1(sK0,X21) ) ).
cnf(u13,negated_conjecture,
r1(sK0,sK9) ).
cnf(u3447,negated_conjecture,
( ~ r1(X0,sK7(sK9))
| ~ r1(sK0,X0) ) ).
cnf(u3968,negated_conjecture,
~ r1(sK9,sK1(sK8(sK0))) ).
cnf(u3504,negated_conjecture,
( ~ r1(sK9,X0)
| ~ r1(X0,X1)
| r1(X1,sK6(X1)) ) ).
cnf(u3050,negated_conjecture,
( ~ r1(sK1(sK7(sK8(sK0))),X0)
| ~ p1(X0) ) ).
cnf(u1959,negated_conjecture,
( ~ r1(sK3(sK9),X0)
| p1(sK6(X0)) ) ).
cnf(u4120,negated_conjecture,
( ~ r1(sK1(sK1(sK8(sK0))),X0)
| ~ p1(X0) ) ).
cnf(u3844,negated_conjecture,
( ~ r1(sK11,sK7(X0))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(sK6(X2))
| ~ r1(sK0,X0) ) ).
cnf(u3963,negated_conjecture,
( ~ r1(sK9,sK7(X0))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(sK6(X2))
| ~ r1(sK0,X0) ) ).
cnf(u2334,negated_conjecture,
r1(sK1(sK7(sK7(sK0))),sK1(sK1(sK7(sK7(sK0))))) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL655+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.40 % Computer : n019.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Sun Sep 27 16:19:19 UTC 2026
% 0.12/0.41 % CPUTime :
% 0.12/0.41 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.44 Running first-order theorem proving
% 0.12/0.44 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.04/1.91 % (3244714)Detected formulas, will run a generic FOF schedule.
% 3.04/1.91 % (3244754)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1036833143:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.04/1.91 % (3244750)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=2108703866:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.04/1.91 % (3244751)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=2437988582:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.04/1.91 % (3244754)Instruction limit reached!
% 3.04/1.91 % (3244754)------------------------------
% 3.04/1.91 % (3244754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.04/1.91 % (3244754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/1.91 % (3244754)CaDiCaL version: 2.1.3
% 3.04/1.91 % (3244754)Termination reason: Instruction limit
% 3.04/1.91 % (3244754)Termination phase: Saturation
% 3.04/1.91 % (3244754)Time elapsed: 0.049 s
% 3.04/1.91 % (3244754)Peak memory usage: 88 MB
% 3.04/1.91 % (3244754)Instructions burned: 119 (million)
% 3.04/1.91 % (3244752)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=2770238837:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.04/1.91 % (3244753)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3660542686:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.04/1.91 % (3244755)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=126390332:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.04/1.91 % (3244756)dis-21_1_sil=8000:lcm=predicate:random_seed=3919399271:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 3.04/1.91 % (3244755)Refutation not found, incomplete strategy
% 3.04/1.91 % (3244755)------------------------------
% 3.04/1.91 % (3244755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.04/1.91 % (3244755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/1.91 % (3244755)CaDiCaL version: 2.1.3
% 3.04/1.91 % (3244755)Termination reason: Refutation not found, incomplete strategy
% 3.04/1.91 % (3244755)Time elapsed: 0.005 s
% 3.04/1.91 % (3244755)Peak memory usage: 88 MB
% 3.04/1.91 % (3244755)Instructions burned: 3 (million)
% 3.04/1.91 % (3244753)Instruction limit reached!
% 3.04/1.91 % (3244753)------------------------------
% 3.04/1.91 % (3244753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.04/1.91 % (3244753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/1.91 % (3244753)CaDiCaL version: 2.1.3
% 3.04/1.91 % (3244753)Termination reason: Instruction limit
% 3.04/1.91 % (3244753)Termination phase: Saturation
% 3.04/1.91 % (3244753)Time elapsed: 0.095 s
% 3.04/1.91 % (3244753)Peak memory usage: 89 MB
% 3.04/1.91 % (3244753)Instructions burned: 110 (million)
% 3.04/1.91 % (3244756)Instruction limit reached!
% 3.04/1.91 % (3244756)------------------------------
% 3.04/1.91 % (3244756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.04/1.91 % (3244756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/1.91 % (3244756)CaDiCaL version: 2.1.3
% 3.04/1.91 % (3244756)Termination reason: Instruction limit
% 3.04/1.91 % (3244756)Termination phase: Saturation
% 3.04/1.91 % (3244756)Time elapsed: 0.109 s
% 3.04/1.91 % (3244756)Peak memory usage: 88 MB
% 3.04/1.91 % (3244756)Instructions burned: 129 (million)
% 3.04/1.91 % (3244760)lrs+10_1_sil=8000:sp=occurrence:random_seed=172028940:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 3.04/1.91 % (3244760)First to succeed.
% 3.04/1.91 % (3244760)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3244714"
% 3.04/1.91 % (3244765)lrs+10_1_sil=32000:urr=on:br=off:random_seed=72678517:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 3.04/1.91 % (3244755)------------------------------
% 3.04/1.91 % (3244755)------------------------------
% 3.04/1.91 % (3244765)Refutation not found, incomplete strategy
% 3.04/1.91 % (3244765)------------------------------
% 3.04/1.91 % (3244765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.04/1.91 % (3244765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/1.91 % (3244765)CaDiCaL version: 2.1.3
% 3.04/1.91 % (3244765)Termination reason: Refutation not found, incomplete strategy
% 3.04/1.91 % (3244765)Time elapsed: 0.014 s
% 3.04/1.91 % (3244765)Peak memory usage: 88 MB
% 3.04/1.91 % (3244765)Instructions burned: 15 (million)
% 3.04/1.91 % (3244766)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3218945534:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 3.04/1.91 % (3244766)Refutation not found, incomplete strategy
% 3.04/1.91 % (3244766)------------------------------
% 3.04/1.91 % (3244766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.04/1.91 % (3244766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/1.91 % (3244766)CaDiCaL version: 2.1.3
% 3.04/1.91 % (3244766)Termination reason: Refutation not found, incomplete strategy
% 3.04/1.91 % (3244766)Time elapsed: 0.005 s
% 3.04/1.91 % (3244766)Peak memory usage: 88 MB
% 3.04/1.91 % (3244766)Instructions burned: 3 (million)
% 3.04/1.91 % SZS status CounterSatisfiable for theBenchmark
% 3.04/1.91 % SZS output start Saturation.
% See solution above
% 6.51/2.12 % SZS output start Definitions and Model Updates.
% 6.51/2.12 % SZS output end Definitions and Model Updates.
% 6.51/2.12 % (3244760)------------------------------
% 6.51/2.12 % (3244760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.51/2.12 % (3244760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.51/2.12 % (3244760)CaDiCaL version: 2.1.3
% 6.51/2.12 % (3244760)Termination reason: Satisfiable
% 6.51/2.12 % (3244760)Time elapsed: 0.052 s
% 6.51/2.12 % (3244760)Peak memory usage: 90 MB
% 6.51/2.12 % (3244760)Instructions burned: 91 (million)
% 6.51/2.12 % (3244760)------------------------------
% 6.51/2.12 % (3244760)------------------------------
% 6.51/2.12 % (3244714)Success in time 0.838 s
% 6.51/2.12 % Vampire exiting
%------------------------------------------------------------------------------