%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL657+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 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:59:29 AM UTC 2026
% Result : CounterSatisfiable 0.16s 0.54s
% Output : Saturation 0.16s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u130,negated_conjecture,
sP11(X5) ).
cnf(u150,negated_conjecture,
p100(X0) ).
cnf(u249,axiom,
sP5(X0) ).
cnf(u277,axiom,
sP6(X0) ).
cnf(u281,axiom,
sP7(X0) ).
cnf(u285,axiom,
sP8(X0) ).
cnf(u289,axiom,
sP9(X0) ).
cnf(u293,axiom,
sP10(X0) ).
cnf(u297,axiom,
sP0(X0) ).
cnf(u306,axiom,
sP1(X0) ).
cnf(u313,axiom,
sP2(X0) ).
cnf(u317,axiom,
sP3(X0) ).
cnf(u321,axiom,
sP4(X0) ).
cnf(u350,negated_conjecture,
~ p2(sK20(X0)) ).
cnf(u355,negated_conjecture,
r1(X0,sK21(X0)) ).
cnf(u731,axiom,
p104(sK15(X0)) ).
cnf(u735,negated_conjecture,
p103(sK15(X0)) ).
cnf(u743,axiom,
p5(sK15(X0)) ).
cnf(u758,axiom,
~ p5(sK14(X0)) ).
cnf(u764,axiom,
~ p105(sK14(X0)) ).
cnf(u818,axiom,
p105(sK13(X0)) ).
cnf(u825,negated_conjecture,
p104(sK13(X0)) ).
cnf(u842,axiom,
p6(sK13(X0)) ).
cnf(u865,negated_conjecture,
p103(sK13(X0)) ).
cnf(u887,axiom,
~ p6(sK12(X0)) ).
cnf(u913,axiom,
p4(sK17(X0)) ).
cnf(u929,axiom,
~ p104(sK16(X0)) ).
cnf(u933,axiom,
~ p4(sK16(X0)) ).
cnf(u948,axiom,
~ p103(sK19(X0)) ).
cnf(u952,axiom,
p3(sK19(X0)) ).
cnf(u967,axiom,
~ p103(sK18(X0)) ).
cnf(u971,axiom,
~ p3(sK18(X0)) ).
cnf(u976,negated_conjecture,
~ p102(sK21(X0)) ).
cnf(u981,negated_conjecture,
~ p102(sK20(X0)) ).
cnf(u1037,axiom,
r1(X0,sK17(X0)) ).
cnf(u1063,axiom,
r1(X0,sK16(X0)) ).
cnf(u1089,axiom,
r1(X0,sK19(X0)) ).
cnf(u1115,axiom,
r1(X0,sK18(X0)) ).
cnf(u1142,negated_conjecture,
r1(X0,sK20(X0)) ).
cnf(u1264,negated_conjecture,
~ p105(sK20(X0)) ).
cnf(u1270,negated_conjecture,
~ p105(sK21(X0)) ).
cnf(u1323,axiom,
~ p105(sK16(X0)) ).
cnf(u1335,axiom,
~ p105(sK18(X0)) ).
cnf(u1341,axiom,
~ p105(sK19(X0)) ).
cnf(u1758,negated_conjecture,
p5(sK20(X0)) ).
cnf(u1761,negated_conjecture,
~ p104(sK20(X0)) ).
cnf(u1764,negated_conjecture,
p5(sK21(X0)) ).
cnf(u1767,negated_conjecture,
~ p104(sK21(X0)) ).
cnf(u1818,axiom,
~ p6(sK14(X0)) ).
cnf(u1821,axiom,
~ p6(sK15(X0)) ).
cnf(u1824,axiom,
~ p6(sK16(X0)) ).
cnf(u1876,axiom,
p5(sK16(X0)) ).
cnf(u1879,axiom,
p5(sK17(X0)) ).
cnf(u1882,axiom,
p5(sK18(X0)) ).
cnf(u1885,axiom,
~ p104(sK18(X0)) ).
cnf(u1888,axiom,
p5(sK19(X0)) ).
cnf(u1891,axiom,
~ p104(sK19(X0)) ).
cnf(u2195,negated_conjecture,
~ p103(sK20(X0)) ).
cnf(u2201,negated_conjecture,
~ p103(sK21(X0)) ).
cnf(u2692,negated_conjecture,
p101(sK14(X0)) ).
cnf(u4776,negated_conjecture,
p102(sK13(X0)) ).
cnf(u4967,negated_conjecture,
p102(sK15(X0)) ).
cnf(u5112,axiom,
~ p6(sK17(X0)) ).
cnf(u5433,negated_conjecture,
p1(X2) ).
cnf(u5717,negated_conjecture,
p101(sK12(X0)) ).
cnf(u5859,axiom,
~ p6(sK19(X0)) ).
cnf(u4489,axiom,
( ~ p2(sK18(X0))
| ~ p101(sK18(X0))
| p2(X0)
| ~ p101(X0) ) ).
cnf(u5955,negated_conjecture,
( ~ p2(sK15(X0))
| p2(X0)
| p104(X0)
| ~ p103(X0) ) ).
cnf(u906,axiom,
( ~ p104(sK17(X0))
| p103(X0)
| ~ p102(X0) ) ).
cnf(u3353,axiom,
( ~ p102(sK17(X0))
| p3(sK17(X0))
| ~ p3(X0)
| ~ p102(X0) ) ).
cnf(u1572,axiom,
( p5(sK15(X0))
| p104(X0)
| ~ p103(X0) ) ).
cnf(u61,axiom,
( ~ sP11(X0)
| sP8(X0) ) ).
cnf(u5032,negated_conjecture,
( ~ p2(sK13(X0))
| p2(X0)
| p105(X0)
| ~ p104(X0) ) ).
cnf(u5951,negated_conjecture,
( ~ p3(sK12(X0))
| p3(X0)
| p105(X0)
| ~ p104(X0) ) ).
cnf(u4501,negated_conjecture,
( ~ p2(sK19(X0))
| p2(X0)
| ~ p101(X0)
| p102(X0) ) ).
cnf(u1953,axiom,
( ~ p104(sK17(X0))
| p5(X0)
| ~ p104(X0) ) ).
cnf(u822,negated_conjecture,
( p104(sK13(X0))
| ~ p104(X0)
| p105(X0) ) ).
cnf(u5146,negated_conjecture,
( p4(sK12(X0))
| ~ p4(X0)
| p105(X0)
| ~ p104(X0) ) ).
cnf(u1034,axiom,
( r1(X0,sK17(X0))
| p103(X0)
| ~ p102(X0) ) ).
cnf(u3399,negated_conjecture,
( ~ p3(sK17(X0))
| p3(X0)
| ~ p102(X0)
| p103(X0) ) ).
cnf(u578,negated_conjecture,
sP7(sK21(sK21(sK21(sK22)))) ).
cnf(u584,negated_conjecture,
sP2(sK21(sK21(sK21(sK22)))) ).
cnf(u5557,negated_conjecture,
( ~ p3(sK13(X0))
| p3(X0)
| p105(X0)
| ~ p104(X0) ) ).
cnf(u4046,negated_conjecture,
( ~ p2(sK20(X0))
| p101(X0) ) ).
cnf(u4426,negated_conjecture,
( p2(sK19(X0))
| ~ p2(X0)
| ~ p101(X0)
| p102(X0) ) ).
cnf(u5561,negated_conjecture,
( p2(sK15(X0))
| ~ p2(X0)
| p104(X0)
| ~ p103(X0) ) ).
cnf(u66,axiom,
( ~ sP11(X0)
| sP2(X0) ) ).
cnf(u4430,negated_conjecture,
( p2(sK17(X0))
| ~ p2(X0)
| p103(X0)
| ~ p102(X0) ) ).
cnf(u5131,axiom,
( ~ p103(sK19(X0))
| p4(sK19(X0))
| ~ p4(X0)
| ~ p103(X0) ) ).
cnf(u517,negated_conjecture,
sP1(sK21(sK22)) ).
cnf(u645,negated_conjecture,
( ~ r1(sK21(sK21(sK21(sK22))),X0)
| sP11(X0) ) ).
cnf(u1800,axiom,
( ~ r1(X0,X2)
| p5(X2)
| ~ p104(X2)
| ~ p5(X0)
| ~ p104(X0) ) ).
cnf(u890,axiom,
( p104(sK14(X0))
| p104(X0)
| ~ p103(X0) ) ).
cnf(u534,negated_conjecture,
sP11(sK21(sK21(sK22))) ).
cnf(u540,negated_conjecture,
sP6(sK21(sK21(sK22))) ).
cnf(u3344,axiom,
( ~ r1(X0,X2)
| p3(X2)
| ~ p102(X2)
| ~ p3(X0)
| ~ p102(X0) ) ).
cnf(u519,negated_conjecture,
sP3(sK21(sK22)) ).
cnf(u4502,negated_conjecture,
( ~ p2(sK18(X0))
| p2(X0)
| ~ p101(X0)
| p102(X0) ) ).
cnf(u896,negated_conjecture,
( p102(sK17(X0))
| ~ p102(X0)
| p103(X0) ) ).
cnf(u3357,axiom,
( ~ p102(sK19(X0))
| p3(sK19(X0))
| ~ p3(X0)
| ~ p102(X0) ) ).
cnf(u5141,negated_conjecture,
( p4(sK15(X0))
| ~ p4(X0)
| ~ p103(X0)
| p104(X0) ) ).
cnf(u5430,negated_conjecture,
( ~ r1(X0,X2)
| p1(X2)
| ~ p1(X0) ) ).
cnf(u3485,negated_conjecture,
( p3(sK14(X0))
| ~ p3(X0)
| p104(X0)
| ~ p103(X0) ) ).
cnf(u930,axiom,
( ~ p4(sK16(X0))
| p103(X0)
| ~ p102(X0) ) ).
cnf(u5145,negated_conjecture,
( p4(sK13(X0))
| ~ p4(X0)
| p105(X0)
| ~ p104(X0) ) ).
cnf(u4650,negated_conjecture,
( p2(sK14(X0))
| ~ p2(X0)
| p104(X0)
| ~ p103(X0) ) ).
cnf(u5798,negated_conjecture,
( ~ p2(sK12(X0))
| p2(X0)
| p105(X0)
| ~ p104(X0) ) ).
cnf(u290,negated_conjecture,
sP9(sK22) ).
cnf(u62,axiom,
( ~ sP11(X0)
| sP9(X0) ) ).
cnf(u1189,negated_conjecture,
( ~ p105(sK21(X0))
| p6(sK21(X0))
| ~ p6(X0)
| ~ p105(X0) ) ).
cnf(u4648,negated_conjecture,
( ~ p2(sK14(X0))
| p2(X0)
| p104(X0)
| ~ p103(X0) ) ).
cnf(u3383,axiom,
( ~ p3(sK16(X0))
| ~ p102(sK16(X0))
| p3(X0)
| ~ p102(X0) ) ).
cnf(u5031,negated_conjecture,
( p2(sK13(X0))
| ~ p2(X0)
| p105(X0)
| ~ p104(X0) ) ).
cnf(u60,axiom,
( ~ sP11(X0)
| sP7(X0) ) ).
cnf(u3387,axiom,
( ~ p3(sK18(X0))
| ~ p102(sK18(X0))
| p3(X0)
| ~ p102(X0) ) ).
cnf(u934,axiom,
( p102(sK19(X0))
| p102(X0)
| ~ p101(X0) ) ).
cnf(u307,negated_conjecture,
sP1(sK22) ).
cnf(u945,axiom,
( ~ p103(sK19(X0))
| p102(X0)
| ~ p101(X0) ) ).
cnf(u1356,axiom,
( ~ p105(sK19(X0))
| ~ p6(sK19(X0))
| p6(X0)
| ~ p105(X0) ) ).
cnf(u1258,axiom,
( ~ p105(sK14(X0))
| p104(X0)
| ~ p103(X0) ) ).
cnf(u4969,negated_conjecture,
p101(sK15(X0)) ).
cnf(u717,negated_conjecture,
( ~ p102(X0)
| p101(X0) ) ).
cnf(u3389,axiom,
( ~ p3(sK19(X0))
| ~ p102(sK19(X0))
| p3(X0)
| ~ p102(X0) ) ).
cnf(u119,negated_conjecture,
p100(sK22) ).
cnf(u968,axiom,
( ~ p3(sK18(X0))
| p102(X0)
| ~ p101(X0) ) ).
cnf(u1350,axiom,
( ~ p105(sK16(X0))
| ~ p6(sK16(X0))
| p6(X0)
| ~ p105(X0) ) ).
cnf(u874,negated_conjecture,
( p104(sK12(X0))
| ~ p104(X0)
| p105(X0) ) ).
cnf(u518,negated_conjecture,
sP2(sK21(sK22)) ).
cnf(u245,negated_conjecture,
sP11(sK22) ).
cnf(u1008,axiom,
( r1(X0,sK12(X0))
| p105(X0)
| ~ p104(X0) ) ).
cnf(u1915,negated_conjecture,
( ~ p5(sK12(X0))
| p5(X0)
| ~ p104(X0)
| p105(X0) ) ).
cnf(u512,negated_conjecture,
sP7(sK21(sK22)) ).
cnf(u1179,axiom,
( ~ p105(sK16(X0))
| p6(sK16(X0))
| ~ p6(X0)
| ~ p105(X0) ) ).
cnf(u5797,negated_conjecture,
( p2(sK12(X0))
| ~ p2(X0)
| p105(X0)
| ~ p104(X0) ) ).
cnf(u134,negated_conjecture,
( ~ r1(sK22,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP11(X3) ) ).
cnf(u543,negated_conjecture,
sP9(sK21(sK21(sK22))) ).
cnf(u914,axiom,
( p103(sK16(X0))
| p103(X0)
| ~ p102(X0) ) ).
cnf(u546,negated_conjecture,
sP1(sK21(sK21(sK22))) ).
cnf(u5285,negated_conjecture,
( ~ p4(sK12(X0))
| p4(X0)
| p105(X0)
| ~ p104(X0) ) ).
cnf(u1847,negated_conjecture,
( p5(sK12(X0))
| ~ p5(X0)
| ~ p104(X0)
| p105(X0) ) ).
cnf(u4129,axiom,
( ~ p102(sK19(X0))
| p3(X0)
| ~ p102(X0) ) ).
cnf(u918,negated_conjecture,
( p102(sK16(X0))
| ~ p102(X0)
| p103(X0) ) ).
cnf(u815,axiom,
( p105(sK13(X0))
| p105(X0)
| ~ p104(X0) ) ).
cnf(u59,axiom,
( ~ sP11(X0)
| sP6(X0) ) ).
cnf(u680,negated_conjecture,
( ~ p104(X0)
| p103(X0) ) ).
cnf(u314,negated_conjecture,
sP2(sK22) ).
cnf(u1183,axiom,
( ~ p105(sK18(X0))
| p6(sK18(X0))
| ~ p6(X0)
| ~ p105(X0) ) ).
cnf(u3583,negated_conjecture,
( p3(sK15(X0))
| ~ p3(X0)
| p104(X0)
| ~ p103(X0) ) ).
cnf(u1846,negated_conjecture,
( p5(sK13(X0))
| ~ p5(X0)
| ~ p104(X0)
| p105(X0) ) ).
cnf(u63,axiom,
( ~ sP11(X0)
| sP10(X0) ) ).
cnf(u318,negated_conjecture,
sP3(sK22) ).
cnf(u964,axiom,
( ~ p103(sK18(X0))
| p102(X0)
| ~ p101(X0) ) ).
cnf(u1892,axiom,
( ~ r1(X0,X1)
| ~ p5(X1)
| ~ p104(X1)
| p5(X0)
| ~ p104(X0) ) ).
cnf(u973,negated_conjecture,
( ~ p102(sK21(X0))
| p101(X0) ) ).
cnf(u2911,axiom,
( r1(X0,sK14(X0))
| p104(X0)
| ~ p103(X0) ) ).
cnf(u513,negated_conjecture,
sP8(sK21(sK22)) ).
cnf(u4487,axiom,
( ~ p2(sK17(X0))
| ~ p101(sK17(X0))
| p2(X0)
| ~ p101(X0) ) ).
cnf(u1564,axiom,
( ~ p5(sK14(X0))
| p104(X0)
| ~ p103(X0) ) ).
cnf(u244,negated_conjecture,
( ~ r1(sK22,X0)
| sP11(X0) ) ).
cnf(u4485,axiom,
( ~ p2(sK16(X0))
| ~ p101(sK16(X0))
| p2(X0)
| ~ p101(X0) ) ).
cnf(u4495,negated_conjecture,
( ~ p2(sK21(X0))
| ~ p101(sK21(X0))
| p2(X0)
| ~ p101(X0) ) ).
cnf(u2087,axiom,
( r1(X0,sK15(X0))
| p104(X0)
| ~ p103(X0) ) ).
cnf(u3584,negated_conjecture,
( ~ p3(sK15(X0))
| p3(X0)
| p104(X0)
| ~ p103(X0) ) ).
cnf(u3355,axiom,
( ~ p102(sK18(X0))
| p3(sK18(X0))
| ~ p3(X0)
| ~ p102(X0) ) ).
cnf(u658,negated_conjecture,
( ~ p101(X0)
| p100(X0) ) ).
cnf(u298,negated_conjecture,
sP0(sK22) ).
cnf(u4410,axiom,
( ~ p101(sK16(X0))
| p2(sK16(X0))
| ~ p2(X0)
| ~ p101(X0) ) ).
cnf(u5279,negated_conjecture,
( ~ p4(sK15(X0))
| p4(X0)
| ~ p103(X0)
| p104(X0) ) ).
cnf(u286,negated_conjecture,
sP8(sK22) ).
cnf(u1830,axiom,
( ~ p104(sK16(X0))
| p5(sK16(X0))
| ~ p5(X0)
| ~ p104(X0) ) ).
cnf(u1836,axiom,
( ~ p104(sK19(X0))
| p5(sK19(X0))
| ~ p5(X0)
| ~ p104(X0) ) ).
cnf(u555,negated_conjecture,
( ~ r1(sK21(sK21(sK22)),X0)
| sP11(X0) ) ).
cnf(u1834,axiom,
( ~ p104(sK18(X0))
| p5(sK18(X0))
| ~ p5(X0)
| ~ p104(X0) ) ).
cnf(u58,axiom,
( ~ sP11(X0)
| sP5(X0) ) ).
cnf(u953,axiom,
( p102(sK18(X0))
| p102(X0)
| ~ p101(X0) ) ).
cnf(u4414,axiom,
( ~ p101(sK18(X0))
| p2(sK18(X0))
| ~ p2(X0)
| ~ p101(X0) ) ).
cnf(u839,axiom,
( p6(sK13(X0))
| p105(X0)
| ~ p104(X0) ) ).
cnf(u4427,negated_conjecture,
( p2(sK18(X0))
| ~ p2(X0)
| ~ p101(X0)
| p102(X0) ) ).
cnf(u4416,axiom,
( ~ p101(sK19(X0))
| p2(sK19(X0))
| ~ p2(X0)
| ~ p101(X0) ) ).
cnf(u580,negated_conjecture,
sP9(sK21(sK21(sK21(sK22)))) ).
cnf(u957,negated_conjecture,
( p101(sK18(X0))
| ~ p101(X0)
| p102(X0) ) ).
cnf(u4425,negated_conjecture,
( ~ p101(sK20(X0))
| ~ p2(X0)
| ~ p101(X0) ) ).
cnf(u3400,negated_conjecture,
( ~ p3(sK16(X0))
| p3(X0)
| ~ p102(X0)
| p103(X0) ) ).
cnf(u585,negated_conjecture,
sP3(sK21(sK21(sK21(sK22)))) ).
cnf(u5911,axiom,
( ~ p103(sK17(X0))
| p4(X0)
| ~ p103(X0) ) ).
cnf(u888,axiom,
( p104(sK15(X0))
| p104(X0)
| ~ p103(X0) ) ).
cnf(u508,negated_conjecture,
sP11(sK21(sK22)) ).
cnf(u514,negated_conjecture,
sP9(sK21(sK22)) ).
cnf(u2579,negated_conjecture,
( p101(sK14(X0))
| ~ p103(X0)
| p104(X0) ) ).
cnf(u892,axiom,
( p103(sK17(X0))
| p103(X0)
| ~ p102(X0) ) ).
cnf(u243,negated_conjecture,
( ~ r1(sK22,X0)
| ~ r1(X0,X1)
| sP11(X1) ) ).
cnf(u520,negated_conjecture,
sP4(sK21(sK22)) ).
cnf(u5142,negated_conjecture,
( p4(sK14(X0))
| ~ p4(X0)
| ~ p103(X0)
| p104(X0) ) ).
cnf(u642,negated_conjecture,
( ~ r1(sK21(sK21(sK22)),X0)
| ~ r1(X0,X1)
| sP11(X1) ) ).
cnf(u5257,axiom,
( ~ r1(X0,X1)
| ~ p4(X1)
| ~ p103(X1)
| p4(X0)
| ~ p103(X0) ) ).
cnf(u282,negated_conjecture,
sP7(sK22) ).
cnf(u5140,axiom,
( ~ p103(sK16(X0))
| ~ p4(X0)
| ~ p103(X0) ) ).
cnf(u4509,negated_conjecture,
( ~ p2(sK17(X0))
| p2(X0)
| p103(X0)
| ~ p102(X0) ) ).
cnf(u541,negated_conjecture,
sP7(sK21(sK21(sK22))) ).
cnf(u52,axiom,
r1(X0,X0) ).
cnf(u926,axiom,
( ~ p104(sK16(X0))
| p103(X0)
| ~ p102(X0) ) ).
cnf(u4544,negated_conjecture,
( ~ p101(sK21(X0))
| p2(sK21(X0))
| ~ p2(X0) ) ).
cnf(u5280,negated_conjecture,
( ~ p4(sK14(X0))
| p4(X0)
| ~ p103(X0)
| p104(X0) ) ).
cnf(u826,negated_conjecture,
( p103(sK13(X0))
| p105(X0)
| ~ p104(X0) ) ).
cnf(u579,negated_conjecture,
sP8(sK21(sK21(sK21(sK22)))) ).
cnf(u1342,axiom,
( ~ r1(X0,X1)
| ~ p6(X1)
| ~ p105(X1)
| p6(X0)
| ~ p105(X0) ) ).
cnf(u583,negated_conjecture,
sP1(sK21(sK21(sK21(sK22)))) ).
cnf(u866,negated_conjecture,
( p102(sK13(X0))
| ~ p104(X0)
| p105(X0) ) ).
cnf(u586,negated_conjecture,
sP4(sK21(sK21(sK21(sK22)))) ).
cnf(u4956,negated_conjecture,
p101(sK13(X0)) ).
cnf(u870,axiom,
( p105(sK12(X0))
| p105(X0)
| ~ p104(X0) ) ).
cnf(u511,negated_conjecture,
sP6(sK21(sK22)) ).
cnf(u1243,axiom,
( ~ p105(sK15(X0))
| p104(X0)
| ~ p103(X0) ) ).
cnf(u114,axiom,
( r1(X0,sK21(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u1165,axiom,
( ~ r1(X0,X2)
| p6(X2)
| ~ p105(X2)
| ~ p6(X0)
| ~ p105(X0) ) ).
cnf(u242,negated_conjecture,
( ~ r1(sK22,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP11(X2) ) ).
cnf(u910,axiom,
( p4(sK17(X0))
| p103(X0)
| ~ p102(X0) ) ).
cnf(u542,negated_conjecture,
sP8(sK21(sK21(sK22))) ).
cnf(u548,negated_conjecture,
sP3(sK21(sK21(sK22))) ).
cnf(u563,negated_conjecture,
sP11(sK21(sK21(sK21(sK22)))) ).
cnf(u4510,negated_conjecture,
( ~ p2(sK16(X0))
| p2(X0)
| p103(X0)
| ~ p102(X0) ) ).
cnf(u1562,negated_conjecture,
( p101(sK20(X0))
| p101(X0) ) ).
cnf(u1568,negated_conjecture,
( p102(sK15(X0))
| p104(X0)
| ~ p103(X0) ) ).
cnf(u53,axiom,
( ~ sP11(X0)
| ~ p101(X0)
| p100(X0) ) ).
cnf(u5680,axiom,
( ~ p104(sK19(X0))
| p5(X0)
| ~ p104(X0) ) ).
cnf(u938,negated_conjecture,
( p101(sK19(X0))
| ~ p101(X0)
| p102(X0) ) ).
cnf(u3385,axiom,
( ~ p3(sK17(X0))
| ~ p102(sK17(X0))
| p3(X0)
| ~ p102(X0) ) ).
cnf(u582,negated_conjecture,
sP0(sK21(sK21(sK21(sK22)))) ).
cnf(u64,axiom,
( ~ sP11(X0)
| sP0(X0) ) ).
cnf(u3351,axiom,
( ~ p102(sK16(X0))
| p3(sK16(X0))
| ~ p3(X0)
| ~ p102(X0) ) ).
cnf(u698,negated_conjecture,
( ~ p105(X0)
| p104(X0) ) ).
cnf(u3409,negated_conjecture,
( ~ p3(sK14(X0))
| p3(X0)
| p104(X0)
| ~ p103(X0) ) ).
cnf(u68,axiom,
( ~ sP11(X0)
| sP4(X0) ) ).
cnf(u978,negated_conjecture,
( ~ p102(sK20(X0))
| p101(X0) ) ).
cnf(u4479,axiom,
( ~ r1(X0,X1)
| ~ p2(X1)
| ~ p101(X1)
| p2(X0)
| ~ p101(X0) ) ).
cnf(u982,axiom,
( r1(X0,sK13(X0))
| p105(X0)
| ~ p104(X0) ) ).
cnf(u2025,negated_conjecture,
( p102(sK14(X0))
| p104(X0)
| ~ p103(X0) ) ).
cnf(u1139,negated_conjecture,
( r1(X0,sK20(X0))
| p101(X0) ) ).
cnf(u3442,negated_conjecture,
( p3(sK16(X0))
| ~ p3(X0)
| ~ p102(X0)
| p103(X0) ) ).
cnf(u121,negated_conjecture,
( ~ r1(sK22,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| sP11(X5) ) ).
cnf(u5119,axiom,
( ~ r1(X0,X2)
| p4(X2)
| ~ p103(X2)
| ~ p4(X0)
| ~ p103(X0) ) ).
cnf(u506,negated_conjecture,
( ~ r1(sK21(sK22),X0)
| ~ r1(X0,X1)
| sP11(X1) ) ).
cnf(u1914,negated_conjecture,
( ~ p5(sK13(X0))
| p5(X0)
| ~ p104(X0)
| p105(X0) ) ).
cnf(u900,negated_conjecture,
( p101(sK17(X0))
| p103(X0)
| ~ p102(X0) ) ).
cnf(u549,negated_conjecture,
sP4(sK21(sK21(sK22))) ).
cnf(u547,negated_conjecture,
sP2(sK21(sK21(sK22))) ).
cnf(u294,negated_conjecture,
sP10(sK22) ).
cnf(u1832,axiom,
( ~ p104(sK17(X0))
| p5(sK17(X0))
| ~ p5(X0)
| ~ p104(X0) ) ).
cnf(u5284,negated_conjecture,
( ~ p4(sK13(X0))
| p4(X0)
| p105(X0)
| ~ p104(X0) ) ).
cnf(u1187,negated_conjecture,
( ~ p105(sK20(X0))
| p6(sK20(X0))
| ~ p6(X0)
| ~ p105(X0) ) ).
cnf(u3376,axiom,
( ~ r1(X0,X1)
| ~ p3(X1)
| ~ p102(X1)
| p3(X0)
| ~ p102(X0) ) ).
cnf(u922,negated_conjecture,
( p101(sK16(X0))
| p103(X0)
| ~ p102(X0) ) ).
cnf(u4404,axiom,
( ~ r1(X0,X2)
| p2(X2)
| ~ p101(X2)
| ~ p2(X0)
| ~ p101(X0) ) ).
cnf(u545,negated_conjecture,
sP0(sK21(sK21(sK22))) ).
cnf(u5551,negated_conjecture,
( p3(sK13(X0))
| ~ p3(X0)
| p105(X0)
| ~ p104(X0) ) ).
cnf(u949,axiom,
( p3(sK19(X0))
| p102(X0)
| ~ p101(X0) ) ).
cnf(u4412,axiom,
( ~ p101(sK17(X0))
| p2(sK17(X0))
| ~ p2(X0)
| ~ p101(X0) ) ).
cnf(u5265,axiom,
( ~ p4(sK17(X0))
| ~ p103(sK17(X0))
| p4(X0)
| ~ p103(X0) ) ).
cnf(u1185,axiom,
( ~ p105(sK19(X0))
| p6(sK19(X0))
| ~ p6(X0)
| ~ p105(X0) ) ).
cnf(u4012,negated_conjecture,
( p2(sK21(X0))
| p101(X0) ) ).
cnf(u5702,negated_conjecture,
( p101(sK12(X0))
| p105(X0)
| ~ p104(X0) ) ).
cnf(u577,negated_conjecture,
sP6(sK21(sK21(sK21(sK22)))) ).
cnf(u4431,negated_conjecture,
( p2(sK16(X0))
| ~ p2(X0)
| p103(X0)
| ~ p102(X0) ) ).
cnf(u1086,axiom,
( r1(X0,sK19(X0))
| p102(X0)
| ~ p101(X0) ) ).
cnf(u67,axiom,
( ~ sP11(X0)
| sP3(X0) ) ).
cnf(u322,negated_conjecture,
sP4(sK22) ).
cnf(u1352,axiom,
( ~ p105(sK17(X0))
| ~ p6(sK17(X0))
| p6(X0)
| ~ p105(X0) ) ).
cnf(u65,axiom,
( ~ sP11(X0)
| sP1(X0) ) ).
cnf(u3366,negated_conjecture,
( p3(sK17(X0))
| ~ p3(X0)
| ~ p102(X0)
| p103(X0) ) ).
cnf(u722,negated_conjecture,
( ~ p103(X0)
| p102(X0) ) ).
cnf(u4961,negated_conjecture,
( p102(sK12(X0))
| ~ p104(X0)
| p105(X0) ) ).
cnf(u878,negated_conjecture,
( p103(sK12(X0))
| p105(X0)
| ~ p104(X0) ) ).
cnf(u1112,axiom,
( r1(X0,sK18(X0))
| p102(X0)
| ~ p101(X0) ) ).
cnf(u884,axiom,
( ~ p6(sK12(X0))
| p105(X0)
| ~ p104(X0) ) ).
cnf(u889,negated_conjecture,
( p103(sK15(X0))
| ~ p103(X0)
| p104(X0) ) ).
cnf(u5127,axiom,
( ~ p103(sK17(X0))
| p4(sK17(X0))
| ~ p4(X0)
| ~ p103(X0) ) ).
cnf(u111,axiom,
( p101(sK21(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u5949,negated_conjecture,
( p3(sK12(X0))
| ~ p3(X0)
| p105(X0)
| ~ p104(X0) ) ).
cnf(u516,negated_conjecture,
sP0(sK21(sK22)) ).
cnf(u507,negated_conjecture,
( ~ r1(sK21(sK22),X0)
| sP11(X0) ) ).
cnf(u120,negated_conjecture,
~ p101(sK22) ).
cnf(u250,negated_conjecture,
sP5(sK22) ).
cnf(u4491,axiom,
( ~ p2(sK19(X0))
| ~ p101(sK19(X0))
| p2(X0)
| ~ p101(X0) ) ).
cnf(u891,negated_conjecture,
( p103(sK14(X0))
| ~ p103(X0)
| p104(X0) ) ).
cnf(u1060,axiom,
( r1(X0,sK16(X0))
| p103(X0)
| ~ p102(X0) ) ).
cnf(u505,negated_conjecture,
( ~ r1(sK21(sK22),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP11(X2) ) ).
cnf(u1181,axiom,
( ~ p105(sK17(X0))
| p6(sK17(X0))
| ~ p6(X0)
| ~ p105(X0) ) ).
cnf(u278,negated_conjecture,
sP6(sK22) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL657+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n003.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.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 16:22:12 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42 Running first-order model finding
% 0.12/0.42 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.54 % (758401)Will run a generic schedule for satisfiability detection.
% 0.16/0.54 % (758408)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=431158401:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.16/0.54 % (758407)% WARNING: option uhcvi not known.
% 0.16/0.54 % (758410)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2948427342:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.16/0.54 % (758406)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1451406414_2999 on theBenchmark for (2999ds/0Mi)
% 0.16/0.54 % (758407)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1298462410:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.16/0.54 % (758411)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1186489611:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.16/0.54 % (758409)dis+10_1_sil=32000:sp=arity:random_seed=183390285:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.16/0.54 % (758412)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1484208648:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.16/0.54 % TRYING [1]
% 0.16/0.54 % TRYING [2]
% 0.16/0.54 % TRYING [3]
% 0.16/0.54 % TRYING [4]
% 0.16/0.54 % TRYING [5]
% 0.16/0.54 % TRYING [6]
% 0.16/0.54 % (758410)Instruction limit reached!
% 0.16/0.54 % (758410)------------------------------
% 0.16/0.54 % (758410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.16/0.54 % (758410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/0.54 % (758410)CaDiCaL version: 2.1.3
% 0.16/0.54 % (758410)Termination reason: Instruction limit
% 0.16/0.54 % (758410)Termination phase: Saturation
% 0.16/0.54 % (758410)Time elapsed: 0.048 s
% 0.16/0.54 % (758410)Peak memory usage: 12 MB
% 0.16/0.54 % (758410)Instructions burned: 116 (million)
% 0.16/0.54 % TRYING [7]
% 0.16/0.54 % (758409)Instruction limit reached!
% 0.16/0.54 % (758409)------------------------------
% 0.16/0.54 % (758409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.16/0.54 % (758409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/0.54 % (758409)CaDiCaL version: 2.1.3
% 0.16/0.54 % (758409)Termination reason: Instruction limit
% 0.16/0.54 % (758409)Termination phase: Saturation
% 0.16/0.54 % (758409)Time elapsed: 0.057 s
% 0.16/0.54 % (758409)Peak memory usage: 14 MB
% 0.16/0.54 % (758409)Instructions burned: 104 (million)
% 0.16/0.54 % (758420)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2195854959:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.16/0.54 % TRYING [1]
% 0.16/0.54 % TRYING [2]
% 0.16/0.54 % TRYING [3]
% 0.16/0.54 % TRYING [4]
% 0.16/0.54 % TRYING [5]
% 0.16/0.54 % (758411)Instruction limit reached!
% 0.16/0.54 % (758411)------------------------------
% 0.16/0.54 % (758411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.16/0.54 % (758411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/0.54 % (758411)CaDiCaL version: 2.1.3
% 0.16/0.54 % (758411)Termination reason: Instruction limit
% 0.16/0.54 % (758411)Termination phase: Saturation
% 0.16/0.54 % (758411)Time elapsed: 0.074 s
% 0.16/0.54 % (758411)Peak memory usage: 14 MB
% 0.16/0.54 % (758411)Instructions burned: 131 (million)
% 0.16/0.54 % (758408) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-758401-758408"...
% 0.16/0.54 % (758408)...printing done.
% 0.16/0.54 % SZS status CounterSatisfiable for theBenchmark
% 0.16/0.54 % SZS output start Saturation.
% See solution above
% 0.16/0.55 % SZS output start Definitions and Model Updates.
% 0.16/0.55 for all inputs,
% 0.16/0.55 define p106(X0) := $false
% 0.16/0.55 % SZS output end Definitions and Model Updates.
% 0.16/0.55 % (758408)------------------------------
% 0.16/0.55 % (758408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.16/0.55 % (758408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/0.55 % (758408)CaDiCaL version: 2.1.3
% 0.16/0.55 % (758408)Termination reason: Satisfiable
% 0.16/0.55 % (758408)Time elapsed: 0.083 s
% 0.16/0.55 % (758408)Peak memory usage: 14 MB
% 0.16/0.55 % (758408)Instructions burned: 244 (million)
% 0.16/0.55 % (758401)Success in time 0.112 s
% 0.16/0.55 % Vampire exiting
%------------------------------------------------------------------------------