%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL653+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.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:19 AM UTC 2026
% Result : CounterSatisfiable 6.61s 1.77s
% Output : Saturation 8.49s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u87,negated_conjecture,
( ~ p2(X0)
| ~ r1(sK4(sK21),X0) ) ).
cnf(u94,negated_conjecture,
r1(sK21,sK4(sK21)) ).
cnf(u117,negated_conjecture,
( ~ p2(X0)
| ~ r1(sK4(sK18),X0) ) ).
cnf(u124,negated_conjecture,
r1(sK18,sK4(sK18)) ).
cnf(u145,negated_conjecture,
( ~ r1(sK2(sK18),X1)
| p2(X1) ) ).
cnf(u157,negated_conjecture,
r1(sK19,sK6(sK19)) ).
cnf(u164,negated_conjecture,
r1(sK20,sK6(sK20)) ).
cnf(u174,negated_conjecture,
( ~ r1(sK21,X0)
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u178,negated_conjecture,
r1(sK18,sK17(sK18)) ).
cnf(u195,negated_conjecture,
r1(sK4(sK21),sK5(sK4(sK21))) ).
cnf(u234,negated_conjecture,
r1(sK4(sK18),sK5(sK4(sK18))) ).
cnf(u267,negated_conjecture,
r1(sK21,sK16(sK21)) ).
cnf(u270,negated_conjecture,
( ~ r1(sK21,X0)
| p2(sK14(X1))
| ~ r1(X0,X1) ) ).
cnf(u274,negated_conjecture,
r1(sK18,sK16(sK18)) ).
cnf(u284,negated_conjecture,
r1(sK16(sK21),sK5(sK16(sK21))) ).
cnf(u303,negated_conjecture,
~ p2(sK22(sK16(sK21))) ).
cnf(u310,negated_conjecture,
~ p2(sK5(sK16(sK21))) ).
cnf(u329,negated_conjecture,
( ~ r1(sK21,X0)
| r1(X1,sK10(X1))
| ~ r1(X0,X1) ) ).
cnf(u333,negated_conjecture,
r1(sK18,sK11(sK18)) ).
cnf(u358,negated_conjecture,
r1(sK16(sK18),sK5(sK16(sK18))) ).
cnf(u372,negated_conjecture,
~ p2(sK5(sK16(sK18))) ).
cnf(u441,negated_conjecture,
r1(sK23(sK18),sK5(sK23(sK18))) ).
cnf(u465,negated_conjecture,
( ~ r1(sK21,X0)
| p1(sK10(X1))
| ~ r1(X0,X1) ) ).
cnf(u494,negated_conjecture,
( ~ r1(X0,sK14(sK5(sK4(sK21))))
| ~ r1(sK9,X0) ) ).
cnf(u509,negated_conjecture,
r1(sK17(sK18),sK5(sK17(sK18))) ).
cnf(u519,negated_conjecture,
r1(sK11(sK18),sK5(sK11(sK18))) ).
cnf(u530,negated_conjecture,
~ p1(sK5(sK11(sK18))) ).
cnf(u557,negated_conjecture,
( ~ r1(X0,sK14(sK5(sK16(sK21))))
| ~ r1(sK9,X0) ) ).
cnf(u575,negated_conjecture,
~ r1(sK9,sK9) ).
cnf(u596,negated_conjecture,
( ~ r1(X0,sK14(sK22(sK16(sK21))))
| ~ r1(sK9,X0) ) ).
cnf(u621,negated_conjecture,
( ~ r1(X0,sK14(sK22(sK4(sK21))))
| ~ r1(sK9,X0) ) ).
cnf(u654,negated_conjecture,
r1(sK23(sK21),sK5(sK23(sK21))) ).
cnf(u686,negated_conjecture,
( ~ r1(X0,sK14(sK5(sK23(sK21))))
| ~ r1(sK9,X0) ) ).
cnf(u713,negated_conjecture,
( ~ r1(X0,sK14(sK22(sK23(sK21))))
| ~ r1(sK9,X0) ) ).
cnf(u753,negated_conjecture,
~ r1(sK9,sK16(sK21)) ).
cnf(u762,negated_conjecture,
~ r1(sK9,sK23(sK21)) ).
cnf(u771,negated_conjecture,
~ r1(sK9,sK4(sK21)) ).
cnf(u404,negated_conjecture,
p1(sK6(sK19)) ).
cnf(u580,negated_conjecture,
( ~ r1(sK16(X0),sK14(sK22(sK16(sK21))))
| ~ r1(X1,X2)
| r1(sK14(X2),sK15(X2))
| ~ r1(X0,X1)
| ~ r1(sK9,X0) ) ).
cnf(u476,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK5(sK4(sK21))))
| ~ r1(X1,X0)
| ~ r1(sK6(X0),X2)
| r1(sK7(X2),sK8(X2))
| ~ sP0(X1) ) ).
cnf(u75,negated_conjecture,
( ~ p2(X1)
| ~ r1(sK5(X0),X1)
| r1(X0,sK6(X0))
| ~ r1(sK21,X0) ) ).
cnf(u471,negated_conjecture,
( ~ r1(X1,sK5(sK16(sK21)))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u578,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK22(sK16(sK21))))
| ~ r1(X1,X0)
| ~ r1(sK6(X0),X2)
| r1(sK7(X2),sK8(X2))
| ~ sP0(X1) ) ).
cnf(u647,negated_conjecture,
( ~ r1(sK23(sK21),X0)
| p1(sK10(X0)) ) ).
cnf(u659,negated_conjecture,
p1(sK5(sK23(sK21))) ).
cnf(u313,negated_conjecture,
( ~ r1(sK16(sK21),X0)
| p2(sK14(X0)) ) ).
cnf(u719,negated_conjecture,
( ~ r1(X0,sK4(sK21))
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u37,negated_conjecture,
( ~ p1(X34)
| ~ r1(X32,X33)
| ~ r1(X33,X34)
| ~ r1(sK9,X32)
| r1(X32,sK23(X32)) ) ).
cnf(u49,negated_conjecture,
( ~ r1(sK9,X8)
| sP0(X8) ) ).
cnf(u502,negated_conjecture,
( ~ r1(sK4(sK21),X0)
| r1(X0,sK10(X0)) ) ).
cnf(u662,negated_conjecture,
( ~ r1(X1,sK5(sK23(sK21)))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u725,negated_conjecture,
( ~ r1(X1,sK10(sK5(sK23(sK21))))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u724,negated_conjecture,
p1(sK10(sK22(sK23(sK21)))) ).
cnf(u40,negated_conjecture,
r1(sK9,sK21) ).
cnf(u279,negated_conjecture,
( ~ r1(sK16(sK21),X0)
| p1(X0) ) ).
cnf(u63,negated_conjecture,
( ~ p2(X9)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| r1(X10,sK12(X10))
| ~ r1(sK9,X8)
| ~ r1(X9,X12)
| r1(X12,sK13(X12)) ) ).
cnf(u696,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK22(sK23(sK21))))
| ~ r1(X1,X0)
| ~ r1(sK6(X0),X2)
| r1(X2,sK7(X2))
| ~ sP0(X1) ) ).
cnf(u704,negated_conjecture,
~ r1(sK4(sK18),sK14(sK22(sK23(sK21)))) ).
cnf(u70,negated_conjecture,
sP1(sK21) ).
cnf(u697,negated_conjecture,
( ~ r1(sK16(X0),sK14(sK22(sK23(sK21))))
| ~ r1(X1,X2)
| r1(sK14(X2),sK15(X2))
| ~ r1(X0,X1)
| ~ r1(sK9,X0) ) ).
cnf(u25,axiom,
( ~ sP1(X0)
| r1(X0,sK4(X0))
| r1(X0,sK2(X0)) ) ).
cnf(u478,negated_conjecture,
( ~ r1(sK16(X0),sK14(sK5(sK4(sK21))))
| ~ r1(X1,X2)
| r1(sK14(X2),sK15(X2))
| ~ r1(X0,X1)
| ~ r1(sK9,X0) ) ).
cnf(u641,negated_conjecture,
( ~ r1(X1,sK10(sK22(sK4(sK21))))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u44,negated_conjecture,
r1(sK18,sK19) ).
cnf(u568,negated_conjecture,
( ~ r1(X0,sK18)
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u787,negated_conjecture,
( ~ r1(X0,sK22(sK23(sK21)))
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u628,negated_conjecture,
p1(sK10(sK22(sK4(sK21)))) ).
cnf(u51,negated_conjecture,
( ~ r1(sK9,X8)
| ~ r1(X8,X15)
| ~ r1(X15,X16)
| p2(sK14(X16))
| r1(X8,sK16(X8)) ) ).
cnf(u633,negated_conjecture,
( ~ r1(X1,sK10(sK5(sK16(sK21))))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u732,negated_conjecture,
( ~ r1(X1,sK23(sK21))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u744,negated_conjecture,
( ~ r1(X1,sK10(sK22(sK23(sK21))))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u635,negated_conjecture,
r1(sK22(sK16(sK21)),sK10(sK22(sK16(sK21)))) ).
cnf(u579,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK22(sK16(sK21))))
| ~ r1(X1,X0)
| ~ r1(sK6(X0),X2)
| r1(X2,sK7(X2))
| ~ sP0(X1) ) ).
cnf(u350,negated_conjecture,
p1(sK22(sK4(sK21))) ).
cnf(u636,negated_conjecture,
r1(sK5(sK16(sK21)),sK10(sK5(sK16(sK21)))) ).
cnf(u29,axiom,
( ~ p2(X3)
| ~ r1(sK5(X1),X3)
| ~ r1(X0,X1)
| ~ r1(sK6(X1),X5)
| r1(X5,sK7(X5))
| ~ sP0(X0) ) ).
cnf(u663,negated_conjecture,
( ~ r1(X1,sK22(sK23(sK21)))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u645,negated_conjecture,
r1(sK21,sK23(sK21)) ).
cnf(u73,negated_conjecture,
( ~ r1(sK6(X0),X1)
| r1(X0,sK5(X0))
| p2(sK7(X1))
| ~ r1(sK21,X0) ) ).
cnf(u469,negated_conjecture,
( ~ r1(X1,sK22(sK16(sK21)))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u642,negated_conjecture,
( ~ r1(X1,sK10(sK22(sK4(sK21))))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u780,negated_conjecture,
( ~ r1(X0,sK5(sK4(sK21)))
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u55,negated_conjecture,
( ~ r1(sK9,X8)
| ~ r1(X8,X15)
| ~ r1(X15,X16)
| r1(sK14(X16),sK15(X16))
| r1(X8,sK16(X8)) ) ).
cnf(u500,negated_conjecture,
( ~ r1(sK4(sK21),X0)
| p1(sK10(X0)) ) ).
cnf(u676,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK5(sK23(sK21))))
| r1(X0,sK6(X0))
| ~ r1(sK18,X0) ) ).
cnf(u567,negated_conjecture,
( ~ r1(X1,sK23(sK18))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u602,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK22(sK4(sK21))))
| ~ r1(X1,X0)
| ~ r1(sK6(X0),X2)
| p2(sK7(X2))
| ~ sP0(X1) ) ).
cnf(u630,negated_conjecture,
( ~ r1(X1,sK10(sK5(sK4(sK21))))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u58,negated_conjecture,
( ~ p2(X14)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p2(X10)
| ~ p2(X9)
| ~ r1(X9,X12)
| ~ r1(sK13(X12),X14)
| ~ r1(sK9,X8) ) ).
cnf(u674,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK5(sK23(sK21))))
| r1(X0,sK6(X0))
| ~ r1(sK21,X0) ) ).
cnf(u34,axiom,
( ~ sP0(X0)
| r1(X1,sK5(X1))
| ~ r1(sK6(X1),X5)
| r1(X5,sK7(X5))
| ~ r1(X0,X1) ) ).
cnf(u755,negated_conjecture,
( ~ r1(X0,sK5(sK23(sK21)))
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u774,negated_conjecture,
( ~ r1(X0,sK5(sK16(sK21)))
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u353,negated_conjecture,
( ~ r1(X1,sK5(sK4(sK21)))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u470,negated_conjecture,
( ~ r1(X1,sK22(sK16(sK21)))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u36,negated_conjecture,
( ~ p1(X34)
| ~ r1(X32,X33)
| ~ r1(X33,X34)
| ~ r1(sK9,X32)
| p1(sK23(X32)) ) ).
cnf(u548,negated_conjecture,
~ r1(sK4(sK18),sK14(sK5(sK16(sK21)))) ).
cnf(u31,axiom,
( ~ sP0(X0)
| r1(X1,sK5(X1))
| ~ r1(sK6(X1),X5)
| p2(sK7(X5))
| ~ r1(X0,X1) ) ).
cnf(u43,negated_conjecture,
( ~ r1(sK19,X27)
| p1(X27) ) ).
cnf(u664,negated_conjecture,
( ~ r1(X1,sK22(sK23(sK21)))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u103,negated_conjecture,
( ~ r1(sK6(X0),X1)
| r1(X0,sK5(X0))
| p2(sK7(X1))
| ~ r1(sK18,X0) ) ).
cnf(u546,negated_conjecture,
~ r1(sK4(sK21),sK14(sK5(sK16(sK21)))) ).
cnf(u483,negated_conjecture,
~ r1(sK4(sK21),sK14(sK5(sK4(sK21)))) ).
cnf(u606,negated_conjecture,
( ~ r1(sK13(X3),sK14(sK22(sK4(sK21))))
| ~ r1(X1,X2)
| p2(X2)
| ~ p2(X1)
| ~ r1(X1,X3)
| ~ r1(X0,X1)
| ~ r1(sK9,X0) ) ).
cnf(u627,negated_conjecture,
p1(sK10(sK5(sK4(sK21)))) ).
cnf(u62,negated_conjecture,
( ~ r1(sK13(X12),X14)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| r1(X10,sK12(X10))
| ~ p2(X9)
| ~ r1(X9,X12)
| ~ r1(sK9,X8)
| ~ p2(X14) ) ).
cnf(u106,negated_conjecture,
( ~ r1(sK18,X0)
| r1(X0,sK6(X0))
| r1(X0,sK5(X0)) ) ).
cnf(u731,negated_conjecture,
p1(sK23(sK21)) ).
cnf(u665,negated_conjecture,
p2(sK14(sK5(sK23(sK21)))) ).
cnf(u694,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK22(sK23(sK21))))
| ~ r1(X1,X0)
| ~ r1(sK6(X0),X2)
| p2(sK7(X2))
| ~ sP0(X1) ) ).
cnf(u458,negated_conjecture,
( ~ r1(X0,sK19)
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u536,negated_conjecture,
p2(sK14(sK22(sK16(sK21)))) ).
cnf(u643,negated_conjecture,
( ~ r1(X0,sK16(sK21))
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u668,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK5(sK23(sK21))))
| ~ r1(X1,X0)
| ~ r1(sK6(X0),X2)
| r1(sK7(X2),sK8(X2))
| ~ sP0(X1) ) ).
cnf(u19,axiom,
( ~ sP1(X0)
| r1(X0,sK4(X0))
| p2(sK2(X0)) ) ).
cnf(u640,negated_conjecture,
( ~ r1(X1,sK10(sK22(sK16(sK21))))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u603,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK22(sK4(sK21))))
| ~ r1(X1,X0)
| ~ r1(sK6(X0),X2)
| r1(sK7(X2),sK8(X2))
| ~ sP0(X1) ) ).
cnf(u38,negated_conjecture,
( ~ p2(sK22(X30))
| ~ r1(sK21,X30) ) ).
cnf(u675,negated_conjecture,
~ r1(sK4(sK21),sK14(sK5(sK23(sK21)))) ).
cnf(u537,negated_conjecture,
p2(sK14(sK5(sK16(sK21)))) ).
cnf(u565,negated_conjecture,
p1(sK23(sK18)) ).
cnf(u726,negated_conjecture,
( ~ r1(X1,sK10(sK5(sK23(sK21))))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u609,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK22(sK4(sK21))))
| r1(X0,sK6(X0))
| ~ r1(sK21,X0) ) ).
cnf(u669,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK5(sK23(sK21))))
| ~ r1(X1,X0)
| ~ r1(sK6(X0),X2)
| r1(X2,sK7(X2))
| ~ sP0(X1) ) ).
cnf(u505,negated_conjecture,
r1(sK22(sK4(sK21)),sK10(sK22(sK4(sK21)))) ).
cnf(u56,negated_conjecture,
( ~ r1(sK16(X8),X20)
| ~ r1(X8,X15)
| ~ r1(X15,X16)
| r1(X16,sK14(X16))
| ~ r1(sK9,X8)
| ~ p2(X20) ) ).
cnf(u229,negated_conjecture,
r1(sK4(sK21),sK22(sK4(sK21))) ).
cnf(u733,negated_conjecture,
( ~ r1(X1,sK23(sK21))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u540,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK5(sK16(sK21))))
| ~ r1(X1,X0)
| ~ r1(sK6(X0),X2)
| r1(X2,sK7(X2))
| ~ sP0(X1) ) ).
cnf(u584,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK22(sK16(sK21))))
| r1(X0,sK6(X0))
| ~ r1(sK21,X0) ) ).
cnf(u23,axiom,
( r1(sK2(X0),sK3(X0))
| r1(X0,sK4(X0))
| ~ sP1(X0) ) ).
cnf(u468,negated_conjecture,
p1(sK5(sK16(sK21))) ).
cnf(u67,negated_conjecture,
( ~ r1(sK9,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| r1(X4,sK10(X4))
| r1(X2,sK11(X2)) ) ).
cnf(u547,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK5(sK16(sK21))))
| r1(X0,sK6(X0))
| ~ r1(sK18,X0) ) ).
cnf(u475,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK5(sK4(sK21))))
| ~ r1(X1,X0)
| ~ r1(sK6(X0),X2)
| p2(sK7(X2))
| ~ sP0(X1) ) ).
cnf(u698,negated_conjecture,
( ~ r1(sK13(X3),sK14(sK22(sK23(sK21))))
| ~ r1(X1,X2)
| p2(X2)
| ~ p2(X1)
| ~ r1(X1,X3)
| ~ r1(X0,X1)
| ~ r1(sK9,X0) ) ).
cnf(u26,axiom,
( ~ p2(X3)
| ~ r1(sK5(X1),X3)
| ~ r1(X0,X1)
| ~ r1(sK6(X1),X5)
| p2(sK7(X5))
| ~ sP0(X0) ) ).
cnf(u651,negated_conjecture,
r1(sK23(sK21),sK22(sK23(sK21))) ).
cnf(u541,negated_conjecture,
( ~ r1(sK16(X0),sK14(sK5(sK16(sK21))))
| ~ r1(X1,X2)
| r1(sK14(X2),sK15(X2))
| ~ r1(X0,X1)
| ~ r1(sK9,X0) ) ).
cnf(u585,negated_conjecture,
~ r1(sK4(sK21),sK14(sK22(sK16(sK21)))) ).
cnf(u41,negated_conjecture,
~ p1(sK20) ).
cnf(u634,negated_conjecture,
( ~ r1(X1,sK10(sK5(sK16(sK21))))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u104,negated_conjecture,
( ~ r1(sK6(X0),X1)
| r1(X0,sK5(X0))
| r1(X1,sK7(X1))
| ~ r1(sK18,X0) ) ).
cnf(u352,negated_conjecture,
( ~ r1(X1,sK22(sK4(sK21)))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u456,negated_conjecture,
( ~ r1(X1,sK6(sK19))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u71,negated_conjecture,
sP0(sK18) ).
cnf(u721,negated_conjecture,
( ~ r1(X0,sK23(sK21))
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u702,negated_conjecture,
~ r1(sK4(sK21),sK14(sK22(sK23(sK21)))) ).
cnf(u30,axiom,
( ~ sP0(X0)
| ~ r1(sK5(X1),X3)
| ~ p2(X3)
| r1(X1,sK6(X1))
| ~ r1(X0,X1) ) ).
cnf(u746,negated_conjecture,
( ~ r1(X0,sK5(sK16(sK21)))
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u646,negated_conjecture,
( ~ r1(sK23(sK21),X0)
| r1(X0,sK10(X0)) ) ).
cnf(u74,negated_conjecture,
( ~ r1(sK6(X0),X1)
| r1(X0,sK5(X0))
| r1(X1,sK7(X1))
| ~ r1(sK21,X0) ) ).
cnf(u45,negated_conjecture,
r1(sK9,sK18) ).
cnf(u482,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK5(sK4(sK21))))
| r1(X0,sK6(X0))
| ~ r1(sK21,X0) ) ).
cnf(u661,negated_conjecture,
( ~ r1(X1,sK5(sK23(sK21)))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u485,negated_conjecture,
~ r1(sK4(sK18),sK14(sK5(sK4(sK21)))) ).
cnf(u789,negated_conjecture,
( ~ r1(X0,sK22(sK4(sK21)))
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u48,negated_conjecture,
( ~ r1(sK9,X8)
| sP1(X8) ) ).
cnf(u47,negated_conjecture,
( ~ r1(sK9,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| p1(X23)
| r1(X21,sK17(X21)) ) ).
cnf(u632,negated_conjecture,
p1(sK10(sK5(sK16(sK21)))) ).
cnf(u692,negated_conjecture,
r1(sK5(sK23(sK21)),sK10(sK5(sK23(sK21)))) ).
cnf(u351,negated_conjecture,
( ~ r1(X1,sK22(sK4(sK21)))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u736,negated_conjecture,
( ~ r1(X0,sK21)
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u455,negated_conjecture,
( ~ r1(X1,sK6(sK19))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u677,negated_conjecture,
~ r1(sK4(sK18),sK14(sK5(sK23(sK21)))) ).
cnf(u354,negated_conjecture,
( ~ r1(X1,sK5(sK4(sK21)))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u297,negated_conjecture,
r1(sK16(sK21),sK22(sK16(sK21))) ).
cnf(u577,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK22(sK16(sK21))))
| ~ r1(X1,X0)
| ~ r1(sK6(X0),X2)
| p2(sK7(X2))
| ~ sP0(X1) ) ).
cnf(u33,axiom,
( ~ r1(sK6(X1),X5)
| r1(X1,sK5(X1))
| ~ r1(X0,X1)
| r1(sK7(X5),sK8(X5))
| ~ sP0(X0) ) ).
cnf(u65,negated_conjecture,
( ~ r1(sK9,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(sK10(X4))
| r1(X2,sK11(X2)) ) ).
cnf(u473,negated_conjecture,
p2(sK14(sK5(sK4(sK21)))) ).
cnf(u24,axiom,
( ~ sP1(X0)
| ~ r1(sK4(X0),X4)
| ~ p2(X4)
| r1(X0,sK2(X0)) ) ).
cnf(u312,negated_conjecture,
( ~ r1(sK4(sK21),X0)
| p2(sK14(X0)) ) ).
cnf(u59,negated_conjecture,
( ~ p2(X9)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p2(X10)
| ~ r1(sK9,X8)
| ~ r1(X9,X12)
| r1(X12,sK13(X12)) ) ).
cnf(u504,negated_conjecture,
r1(sK5(sK4(sK21)),sK10(sK5(sK4(sK21)))) ).
cnf(u740,negated_conjecture,
( ~ r1(X0,sK23(sK21))
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u631,negated_conjecture,
p1(sK10(sK22(sK16(sK21)))) ).
cnf(u50,negated_conjecture,
( ~ r1(sK16(X8),X20)
| ~ r1(X8,X15)
| ~ r1(X15,X16)
| p2(sK14(X16))
| ~ r1(sK9,X8)
| ~ p2(X20) ) ).
cnf(u666,negated_conjecture,
p2(sK14(sK22(sK23(sK21)))) ).
cnf(u703,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK22(sK23(sK21))))
| r1(X0,sK6(X0))
| ~ r1(sK18,X0) ) ).
cnf(u785,negated_conjecture,
( ~ r1(X0,sK22(sK16(sK21)))
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u778,negated_conjecture,
( ~ r1(X0,sK5(sK23(sK21)))
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u738,negated_conjecture,
( ~ r1(X0,sK4(sK21))
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u637,negated_conjecture,
( ~ r1(X0,sK18)
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u581,negated_conjecture,
( ~ r1(sK13(X3),sK14(sK22(sK16(sK21))))
| ~ r1(X1,X2)
| p2(X2)
| ~ p2(X1)
| ~ r1(X1,X3)
| ~ r1(X0,X1)
| ~ r1(sK9,X0) ) ).
cnf(u745,negated_conjecture,
( ~ r1(X1,sK10(sK22(sK23(sK21))))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u474,negated_conjecture,
p2(sK14(sK22(sK4(sK21)))) ).
cnf(u69,negated_conjecture,
sP1(sK18) ).
cnf(u477,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK5(sK4(sK21))))
| ~ r1(X1,X0)
| ~ r1(sK6(X0),X2)
| r1(X2,sK7(X2))
| ~ sP0(X1) ) ).
cnf(u28,axiom,
( ~ p2(X3)
| ~ r1(sK5(X1),X3)
| ~ r1(X0,X1)
| ~ r1(sK6(X1),X5)
| r1(sK7(X5),sK8(X5))
| ~ sP0(X0) ) ).
cnf(u72,negated_conjecture,
sP0(sK21) ).
cnf(u791,negated_conjecture,
( ~ r1(X0,sK22(sK23(sK21)))
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u436,negated_conjecture,
r1(sK18,sK23(sK18)) ).
cnf(u612,negated_conjecture,
~ r1(sK4(sK18),sK14(sK22(sK4(sK21)))) ).
cnf(u35,axiom,
( ~ sP0(X0)
| r1(X1,sK5(X1))
| r1(X1,sK6(X1))
| ~ r1(X0,X1) ) ).
cnf(u538,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK5(sK16(sK21))))
| ~ r1(X1,X0)
| ~ r1(sK6(X0),X2)
| p2(sK7(X2))
| ~ sP0(X1) ) ).
cnf(u566,negated_conjecture,
( ~ r1(X1,sK23(sK18))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u503,negated_conjecture,
( ~ r1(sK16(sK21),X0)
| r1(X0,sK10(X0)) ) ).
cnf(u42,negated_conjecture,
r1(sK18,sK20) ).
cnf(u610,negated_conjecture,
~ r1(sK4(sK21),sK14(sK22(sK4(sK21)))) ).
cnf(u54,negated_conjecture,
( ~ p2(X20)
| ~ r1(X8,X15)
| ~ r1(X15,X16)
| r1(sK14(X16),sK15(X16))
| ~ r1(sK16(X8),X20)
| ~ r1(sK9,X8) ) ).
cnf(u782,negated_conjecture,
( ~ r1(X0,sK22(sK4(sK21)))
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u670,negated_conjecture,
( ~ r1(sK16(X0),sK14(sK5(sK23(sK21))))
| ~ r1(X1,X2)
| r1(sK14(X2),sK15(X2))
| ~ r1(X0,X1)
| ~ r1(sK9,X0) ) ).
cnf(u723,negated_conjecture,
p1(sK10(sK5(sK23(sK21)))) ).
cnf(u776,negated_conjecture,
( ~ r1(X0,sK22(sK16(sK21)))
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u230,negated_conjecture,
( ~ r1(sK4(sK21),X0)
| p1(X0) ) ).
cnf(u695,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK22(sK23(sK21))))
| ~ r1(X1,X0)
| ~ r1(sK6(X0),X2)
| r1(sK7(X2),sK8(X2))
| ~ sP0(X1) ) ).
cnf(u349,negated_conjecture,
p1(sK5(sK4(sK21))) ).
cnf(u701,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK22(sK23(sK21))))
| r1(X0,sK6(X0))
| ~ r1(sK21,X0) ) ).
cnf(u734,negated_conjecture,
( ~ r1(X0,sK21)
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u76,negated_conjecture,
( ~ r1(sK21,X0)
| r1(X0,sK6(X0))
| r1(X0,sK5(X0)) ) ).
cnf(u39,negated_conjecture,
( ~ r1(sK21,X30)
| r1(X30,sK22(X30)) ) ).
cnf(u484,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK5(sK4(sK21))))
| r1(X0,sK6(X0))
| ~ r1(sK18,X0) ) ).
cnf(u660,negated_conjecture,
p1(sK22(sK23(sK21))) ).
cnf(u542,negated_conjecture,
( ~ r1(sK13(X3),sK14(sK5(sK16(sK21))))
| ~ r1(X1,X2)
| p2(X2)
| ~ p2(X1)
| ~ r1(X1,X3)
| ~ r1(X0,X1)
| ~ r1(sK9,X0) ) ).
cnf(u563,negated_conjecture,
( ~ r1(X0,sK19)
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u586,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK22(sK16(sK21))))
| r1(X0,sK6(X0))
| ~ r1(sK18,X0) ) ).
cnf(u587,negated_conjecture,
~ r1(sK4(sK18),sK14(sK22(sK16(sK21)))) ).
cnf(u667,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK5(sK23(sK21))))
| ~ r1(X1,X0)
| ~ r1(sK6(X0),X2)
| p2(sK7(X2))
| ~ sP0(X1) ) ).
cnf(u629,negated_conjecture,
( ~ r1(X1,sK10(sK5(sK4(sK21))))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u57,negated_conjecture,
( ~ r1(sK9,X8)
| ~ r1(X8,X15)
| ~ r1(X15,X16)
| r1(X16,sK14(X16))
| r1(X8,sK16(X8)) ) ).
cnf(u66,negated_conjecture,
( ~ r1(sK11(X2),X7)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| r1(X4,sK10(X4))
| ~ r1(sK9,X2)
| ~ p1(X7) ) ).
cnf(u18,axiom,
( ~ sP1(X0)
| ~ r1(sK4(X0),X4)
| ~ p2(X4)
| p2(sK2(X0)) ) ).
cnf(u64,negated_conjecture,
( ~ r1(sK11(X2),X7)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(sK10(X4))
| ~ r1(sK9,X2)
| ~ p1(X7) ) ).
cnf(u479,negated_conjecture,
( ~ r1(sK13(X3),sK14(sK5(sK4(sK21))))
| ~ r1(X1,X2)
| p2(X2)
| ~ p2(X1)
| ~ r1(X1,X3)
| ~ r1(X0,X1)
| ~ r1(sK9,X0) ) ).
cnf(u604,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK22(sK4(sK21))))
| ~ r1(X1,X0)
| ~ r1(sK6(X0),X2)
| r1(X2,sK7(X2))
| ~ sP0(X1) ) ).
cnf(u764,negated_conjecture,
( ~ r1(X0,sK5(sK4(sK21)))
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u472,negated_conjecture,
( ~ r1(X1,sK5(sK16(sK21)))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| r1(X0,sK23(X0)) ) ).
cnf(u648,negated_conjecture,
( ~ r1(sK23(sK21),X0)
| p2(sK14(X0)) ) ).
cnf(u539,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK5(sK16(sK21))))
| ~ r1(X1,X0)
| ~ r1(sK6(X0),X2)
| r1(sK7(X2),sK8(X2))
| ~ sP0(X1) ) ).
cnf(u467,negated_conjecture,
p1(sK22(sK16(sK21))) ).
cnf(u611,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK22(sK4(sK21))))
| r1(X0,sK6(X0))
| ~ r1(sK18,X0) ) ).
cnf(u46,negated_conjecture,
( ~ p1(sK17(X21))
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| p1(X23)
| ~ r1(sK9,X21) ) ).
cnf(u671,negated_conjecture,
( ~ r1(sK13(X3),sK14(sK5(sK23(sK21))))
| ~ r1(X1,X2)
| p2(X2)
| ~ p2(X1)
| ~ r1(X1,X3)
| ~ r1(X0,X1)
| ~ r1(sK9,X0) ) ).
cnf(u729,negated_conjecture,
( ~ r1(X0,sK16(sK21))
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
cnf(u545,negated_conjecture,
( ~ r1(sK5(X0),sK14(sK5(sK16(sK21))))
| r1(X0,sK6(X0))
| ~ r1(sK21,X0) ) ).
cnf(u605,negated_conjecture,
( ~ r1(sK16(X0),sK14(sK22(sK4(sK21))))
| ~ r1(X1,X2)
| r1(sK14(X2),sK15(X2))
| ~ r1(X0,X1)
| ~ r1(sK9,X0) ) ).
cnf(u649,negated_conjecture,
( ~ r1(sK23(sK21),X0)
| p1(X0) ) ).
cnf(u105,negated_conjecture,
( ~ p2(X1)
| ~ r1(sK5(X0),X1)
| r1(X0,sK6(X0))
| ~ r1(sK18,X0) ) ).
cnf(u501,negated_conjecture,
( ~ r1(sK16(sK21),X0)
| p1(sK10(X0)) ) ).
cnf(u22,axiom,
( ~ sP1(X0)
| ~ r1(sK4(X0),X4)
| ~ p2(X4)
| r1(sK2(X0),sK3(X0)) ) ).
cnf(u693,negated_conjecture,
r1(sK22(sK23(sK21)),sK10(sK22(sK23(sK21)))) ).
cnf(u639,negated_conjecture,
( ~ r1(X1,sK10(sK22(sK16(sK21))))
| ~ r1(X0,X1)
| ~ r1(sK9,X0)
| p1(sK23(X0)) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL653+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n001.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 16:23:01 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.61/1.77 % (3763223)Detected formulas, will run a generic FOF schedule.
% 6.61/1.77 % (3763233)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4045246044:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 6.61/1.77 % (3763232)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=313868444:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 6.61/1.77 % (3763229)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=2880888100:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 6.61/1.77 % (3763231)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=518720627:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 6.61/1.77 % (3763228)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=1040628410:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 6.61/1.77 % (3763234)dis-21_1_sil=8000:lcm=predicate:random_seed=3213839016: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)
% 6.61/1.77 % (3763230)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=2912786994:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 6.61/1.77 % (3763231)Instruction limit reached!
% 6.61/1.77 % (3763231)------------------------------
% 6.61/1.77 % (3763231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.77 % (3763231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.77 % (3763231)CaDiCaL version: 2.1.3
% 6.61/1.77 % (3763231)Termination reason: Instruction limit
% 6.61/1.77 % (3763231)Termination phase: Saturation
% 6.61/1.77 % (3763231)Time elapsed: 0.060 s
% 6.61/1.77 % (3763231)Peak memory usage: 90 MB
% 6.61/1.77 % (3763231)Instructions burned: 111 (million)
% 6.61/1.77 % (3763232)Instruction limit reached!
% 6.61/1.77 % (3763232)------------------------------
% 6.61/1.77 % (3763232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.77 % (3763232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.77 % (3763232)CaDiCaL version: 2.1.3
% 6.61/1.77 % (3763232)Termination reason: Instruction limit
% 6.61/1.77 % (3763232)Termination phase: Saturation
% 6.61/1.77 % (3763232)Time elapsed: 0.062 s
% 6.61/1.77 % (3763232)Peak memory usage: 88 MB
% 6.61/1.77 % (3763232)Instructions burned: 120 (million)
% 6.61/1.77 % (3763234)Instruction limit reached!
% 6.61/1.77 % (3763234)------------------------------
% 6.61/1.77 % (3763234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.77 % (3763234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.77 % (3763234)CaDiCaL version: 2.1.3
% 6.61/1.77 % (3763234)Termination reason: Instruction limit
% 6.61/1.77 % (3763234)Termination phase: Saturation
% 6.61/1.77 % (3763234)Time elapsed: 0.066 s
% 6.61/1.77 % (3763234)Peak memory usage: 88 MB
% 6.61/1.77 % (3763234)Instructions burned: 129 (million)
% 6.61/1.77 % (3763233)Instruction limit reached!
% 6.61/1.77 % (3763233)------------------------------
% 6.61/1.77 % (3763233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.77 % (3763233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.77 % (3763233)CaDiCaL version: 2.1.3
% 6.61/1.77 % (3763233)Termination reason: Instruction limit
% 6.61/1.77 % (3763233)Termination phase: Saturation
% 6.61/1.77 % (3763233)Time elapsed: 0.071 s
% 6.61/1.77 % (3763233)Peak memory usage: 88 MB
% 6.61/1.77 % (3763233)Instructions burned: 139 (million)
% 6.61/1.77 % (3763242)lrs+10_1_sil=8000:sp=occurrence:random_seed=1459437104:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 6.61/1.77 % (3763244)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3538805474:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 6.61/1.77 % (3763243)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2291733686:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 6.61/1.77 % (3763243)Refutation not found, incomplete strategy
% 6.61/1.77 % (3763243)------------------------------
% 6.61/1.77 % (3763243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.77 % (3763243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.77 % (3763243)CaDiCaL version: 2.1.3
% 6.61/1.77 % (3763243)Termination reason: Refutation not found, incomplete strategy
% 6.61/1.77 % (3763243)Time elapsed: 0.003 s
% 6.61/1.77 % (3763243)Peak memory usage: 88 MB
% 6.61/1.77 % (3763243)Instructions burned: 4 (million)
% 6.61/1.77 % (3763245)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=3708957977:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 6.61/1.77 % (3763245)Refutation not found, incomplete strategy
% 6.61/1.77 % (3763245)------------------------------
% 6.61/1.77 % (3763245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.77 % (3763245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.77 % (3763245)CaDiCaL version: 2.1.3
% 6.61/1.77 % (3763245)Termination reason: Refutation not found, incomplete strategy
% 6.61/1.77 % (3763245)Time elapsed: 0.003 s
% 6.61/1.77 % (3763245)Peak memory usage: 88 MB
% 6.61/1.77 % (3763245)Instructions burned: 4 (million)
% 6.61/1.77 % (3763244)Instruction limit reached!
% 6.61/1.77 % (3763244)------------------------------
% 6.61/1.77 % (3763244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.77 % (3763244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.77 % (3763244)CaDiCaL version: 2.1.3
% 6.61/1.77 % (3763244)Termination reason: Instruction limit
% 6.61/1.77 % (3763244)Termination phase: Saturation
% 6.61/1.77 % (3763244)Time elapsed: 0.073 s
% 6.61/1.77 % (3763244)Peak memory usage: 88 MB
% 6.61/1.77 % (3763244)Instructions burned: 332 (million)
% 6.61/1.77 % (3763242)Instruction limit reached!
% 6.61/1.77 % (3763242)------------------------------
% 6.61/1.77 % (3763242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.77 % (3763242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.77 % (3763242)CaDiCaL version: 2.1.3
% 6.61/1.77 % (3763242)Termination reason: Instruction limit
% 6.61/1.77 % (3763242)Termination phase: Saturation
% 6.61/1.77 % (3763242)Time elapsed: 0.158 s
% 6.61/1.77 % (3763242)Peak memory usage: 92 MB
% 6.61/1.77 % (3763242)Instructions burned: 286 (million)
% 6.61/1.77 % (3763250)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1474048387:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 6.61/1.77 % (3763243)------------------------------
% 6.61/1.77 % (3763243)------------------------------
% 6.61/1.77 % (3763245)------------------------------
% 6.61/1.77 % (3763245)------------------------------
% 6.61/1.77 % (3763250)Instruction limit reached!
% 6.61/1.77 % (3763250)------------------------------
% 6.61/1.77 % (3763250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.77 % (3763250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.77 % (3763250)CaDiCaL version: 2.1.3
% 6.61/1.77 % (3763250)Termination reason: Instruction limit
% 6.61/1.77 % (3763250)Termination phase: Saturation
% 6.61/1.77 % (3763250)Time elapsed: 0.079 s
% 6.61/1.77 % (3763250)Peak memory usage: 89 MB
% 6.61/1.77 % (3763250)Instructions burned: 295 (million)
% 6.61/1.77 % (3763251)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3382389622:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 6.61/1.77 % (3763255)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1063200473:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 6.61/1.77 % (3763253)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2832040444:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 6.61/1.77 % (3763255)Instruction limit reached!
% 6.61/1.77 % (3763255)------------------------------
% 6.61/1.77 % (3763255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.77 % (3763255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.77 % (3763255)CaDiCaL version: 2.1.3
% 6.61/1.77 % (3763255)Termination reason: Instruction limit
% 6.61/1.77 % (3763255)Termination phase: Saturation
% 6.61/1.77 % (3763255)Time elapsed: 0.034 s
% 6.61/1.77 % (3763255)Peak memory usage: 88 MB
% 6.61/1.77 % (3763255)Instructions burned: 118 (million)
% 6.61/1.77 % (3763254)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1842102701:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 6.61/1.77 % (3763253)Instruction limit reached!
% 6.61/1.77 % (3763253)------------------------------
% 6.61/1.77 % (3763253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.77 % (3763253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.77 % (3763253)CaDiCaL version: 2.1.3
% 6.61/1.77 % (3763253)Termination reason: Instruction limit
% 6.61/1.77 % (3763253)Termination phase: Saturation
% 6.61/1.77 % (3763253)Time elapsed: 0.066 s
% 6.61/1.77 % (3763253)Peak memory usage: 90 MB
% 6.61/1.77 % (3763253)Instructions burned: 114 (million)
% 6.61/1.77 % (3763254)Instruction limit reached!
% 6.61/1.77 % (3763254)------------------------------
% 6.61/1.77 % (3763254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.77 % (3763254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.77 % (3763254)CaDiCaL version: 2.1.3
% 6.61/1.77 % (3763254)Termination reason: Instruction limit
% 6.61/1.77 % (3763254)Termination phase: Saturation
% 6.61/1.77 % (3763254)Time elapsed: 0.071 s
% 6.61/1.77 % (3763254)Peak memory usage: 89 MB
% 6.61/1.77 % (3763254)Instructions burned: 127 (million)
% 6.61/1.77 % (3763229)First to succeed.
% 6.61/1.77 % (3763229)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3763223"
% 6.61/1.77 % (3763260)lrs+10_1_sil=8000:sp=occurrence:random_seed=956599832:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 6.61/1.77 % (3763261)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=322459368:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 6.61/1.77 % (3763262)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2283663435:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 6.61/1.77 % SZS status CounterSatisfiable for theBenchmark
% 6.61/1.77 % SZS output start Saturation.
% See solution above
% 8.49/1.97 % SZS output start Definitions and Model Updates.
% 8.49/1.97 for all groundings,
% 8.49/1.97 whenever ~r1(sK9,X8) | ~r1(X8,X15) | ~r1(X15,X16) | ~p3(sK15(X16)) | ~r1(sK16(X8),X20) | ~p2(X20) is false, set ~p3(sK15(X16)) to true
% 8.49/1.97 for all groundings,
% 8.49/1.97 whenever ~r1(sK9,X8) | ~r1(X8,X15) | ~r1(X15,X16) | ~p3(sK15(X16)) | r1(X8,sK16(X8)) is false, set ~p3(sK15(X16)) to true
% 8.49/1.97 for all groundings,
% 8.49/1.97 whenever ~r1(sK9,X8) | ~r1(X8,X9) | ~r1(X9,X10) | ~p3(sK12(X10)) | ~p2(X9) | ~r1(X9,X12) | ~r1(sK13(X12),X14) | ~p2(X14) is false, set ~p3(sK12(X10)) to true
% 8.49/1.97 for all groundings,
% 8.49/1.97 whenever ~r1(sK9,X8) | ~r1(X8,X9) | ~r1(X9,X10) | ~p3(sK12(X10)) | ~p2(X9) | ~r1(X9,X12) | r1(X12,sK13(X12)) is false, set ~p3(sK12(X10)) to true
% 8.49/1.97 for all groundings,
% 8.49/1.97 whenever ~r1(X0,X1) | ~r1(sK5(X1),X3) | ~p2(X3) | ~r1(sK6(X1),X5) | ~p3(sK8(X5)) | ~sP0(X0) is false, set ~p3(sK8(X5)) to true
% 8.49/1.97 for all groundings,
% 8.49/1.97 whenever ~r1(X0,X1) | r1(X1,sK5(X1)) | ~r1(sK6(X1),X5) | ~p3(sK8(X5)) | ~sP0(X0) is false, set ~p3(sK8(X5)) to true
% 8.49/1.97 for all groundings,
% 8.49/1.97 whenever ~p3(sK3(X0)) | ~r1(sK4(X0),X4) | ~p2(X4) | ~sP1(X0) is false, set ~p3(sK3(X0)) to true
% 8.49/1.97 for all groundings,
% 8.49/1.97 whenever ~p3(sK3(X0)) | r1(X0,sK4(X0)) | ~sP1(X0) is false, set ~p3(sK3(X0)) to true
% 8.49/1.97 for all groundings,
% 8.49/1.97 whenever ~r1(sK9,X1) | ~p4(X1) is false, set ~p4(X1) to true
% 8.49/1.97 % SZS output end Definitions and Model Updates.
% 8.49/1.97 % (3763229)------------------------------
% 8.49/1.97 % (3763229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.49/1.97 % (3763229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.49/1.97 % (3763229)CaDiCaL version: 2.1.3
% 8.49/1.97 % (3763229)Termination reason: Satisfiable
% 8.49/1.97 % (3763229)Time elapsed: 0.726 s
% 8.49/1.97 % (3763229)Peak memory usage: 127 MB
% 8.49/1.97 % (3763229)Instructions burned: 1065 (million)
% 8.49/1.97 % (3763229)------------------------------
% 8.49/1.97 % (3763229)------------------------------
% 8.49/1.97 % (3763223)Success in time 1.155 s
% 8.49/1.97 % Vampire exiting
%------------------------------------------------------------------------------