%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL641+1.010 : 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 : n007.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:53:44 AM UTC 2026
% Result : CounterSatisfiable 6.22s 2.14s
% Output : Saturation 11.23s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u150,negated_conjecture,
( ~ r1(sK33,X0)
| ~ r1(X0,X1)
| r1(X1,sK2(X1))
| p1(X1) ) ).
cnf(u154,negated_conjecture,
( ~ r1(sK33,X0)
| ~ r1(X0,X1)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u161,negated_conjecture,
r1(sK34,sK35(sK34)) ).
cnf(u164,negated_conjecture,
p1(sK34) ).
cnf(u170,negated_conjecture,
( ~ r1(sK33,X0)
| ~ r1(X0,X1)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u199,negated_conjecture,
r1(sK34,sK22(sK34)) ).
cnf(u202,negated_conjecture,
( ~ r1(sK34,X0)
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u232,negated_conjecture,
( ~ r1(sK32,X0)
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u247,negated_conjecture,
r1(sK31,sK14(sK31)) ).
cnf(u257,negated_conjecture,
r1(sK14(sK31),sK11(sK14(sK31))) ).
cnf(u272,negated_conjecture,
r1(sK30,sK17(sK30)) ).
cnf(u285,negated_conjecture,
r1(sK28,sK39(sK28)) ).
cnf(u288,negated_conjecture,
( ~ r1(sK28,X0)
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u297,negated_conjecture,
r1(sK17(sK30),sK14(sK17(sK30))) ).
cnf(u307,negated_conjecture,
r1(sK26,sK45(sK26)) ).
cnf(u310,negated_conjecture,
( ~ r1(sK26,X0)
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u316,negated_conjecture,
r1(sK25,sK48(sK25)) ).
cnf(u319,negated_conjecture,
( ~ r1(sK25,X0)
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u330,negated_conjecture,
r1(sK48(sK25),sK45(sK48(sK25))) ).
cnf(u333,negated_conjecture,
( ~ r1(sK48(sK25),X0)
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u342,negated_conjecture,
r1(sK27,sK42(sK27)) ).
cnf(u345,negated_conjecture,
( ~ r1(sK27,X0)
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u353,negated_conjecture,
( ~ r1(sK24,X0)
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u366,negated_conjecture,
r1(sK51(sK24),sK48(sK51(sK24))) ).
cnf(u380,negated_conjecture,
p1(sK23) ).
cnf(u397,negated_conjecture,
( ~ r1(sK45(sK26),X0)
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u433,negated_conjecture,
r1(sK42(sK27),sK39(sK42(sK27))) ).
cnf(u436,negated_conjecture,
( ~ r1(sK42(sK27),X0)
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u507,negated_conjecture,
p1(sK24) ).
cnf(u528,negated_conjecture,
r1(sK17(sK30),sK10(sK17(sK30))) ).
cnf(u547,negated_conjecture,
p1(sK31) ).
cnf(u600,negated_conjecture,
p1(sK30) ).
cnf(u629,negated_conjecture,
p1(sK25) ).
cnf(u632,negated_conjecture,
( ~ r1(sK25,X0)
| p1(X0) ) ).
cnf(u728,negated_conjecture,
( ~ r1(sK11(sK14(sK31)),X0)
| ~ r1(X0,X1)
| r1(X1,sK2(X1))
| p1(X1) ) ).
cnf(u732,negated_conjecture,
( ~ r1(sK11(sK14(sK31)),X0)
| ~ r1(X0,X1)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u736,negated_conjecture,
( ~ r1(sK11(sK14(sK31)),X0)
| ~ r1(X0,X1)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u762,negated_conjecture,
r1(sK14(sK17(sK30)),sK11(sK14(sK17(sK30)))) ).
cnf(u772,negated_conjecture,
( ~ r1(sK10(sK17(sK30)),X0)
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u796,negated_conjecture,
( ~ r1(sK11(sK14(sK17(sK30))),X0)
| ~ r1(X0,X1)
| r1(X1,sK2(X1))
| p1(X1) ) ).
cnf(u800,negated_conjecture,
( ~ r1(sK11(sK14(sK17(sK30))),X0)
| ~ r1(X0,X1)
| p1(sK2(X1))
| p1(X1) ) ).
cnf(u804,negated_conjecture,
( ~ r1(sK11(sK14(sK17(sK30))),X0)
| ~ r1(X0,X1)
| r1(sK2(X1),sK3(X1))
| p1(X1) ) ).
cnf(u818,negated_conjecture,
( ~ r1(sK45(sK48(sK25)),X0)
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u841,negated_conjecture,
( ~ r1(sK11(sK14(sK31)),X1)
| r1(X1,sK20(X1)) ) ).
cnf(u892,negated_conjecture,
~ p1(sK11(sK14(sK31))) ).
cnf(u858,negated_conjecture,
r1(sK42(sK45(sK26)),sK39(sK42(sK45(sK26)))) ).
cnf(u911,negated_conjecture,
( ~ r1(sK11(sK14(sK17(sK30))),X1)
| r1(X1,sK20(X1)) ) ).
cnf(u944,negated_conjecture,
~ p1(sK11(sK14(sK17(sK30)))) ).
cnf(u98,negated_conjecture,
( ~ p1(sK20(X73))
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| ~ r1(X57,X58)
| ~ r1(X58,X59)
| ~ r1(X59,X60)
| ~ r1(X60,X61)
| ~ r1(X61,X62)
| ~ r1(X62,X63)
| ~ r1(X63,X64)
| ~ r1(X64,X65)
| ~ r1(X65,X72)
| p1(X72)
| p1(X65)
| ~ r1(X65,X73)
| ~ r1(sK8,X55)
| ~ r1(sK21(X65),X76)
| ~ r1(X76,X77)
| p1(X77)
| ~ p1(X76) ) ).
cnf(u901,negated_conjecture,
( ~ r1(sK39(sK42(sK27)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| ~ r1(X3,X6)
| p1(X6)
| ~ p1(X3)
| ~ r1(X3,X7)
| p1(sK18(X7))
| sP0(X3) ) ).
cnf(u934,negated_conjecture,
( ~ r1(sK45(sK48(sK25)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| p1(X2)
| ~ r1(X2,X4)
| r1(X4,sK12(X4))
| r1(X2,sK13(X2)) ) ).
cnf(u97,negated_conjecture,
( ~ r1(sK8,X55)
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| ~ r1(X57,X58)
| ~ r1(X58,X59)
| ~ r1(X59,X60)
| ~ r1(X60,X61)
| ~ r1(X61,X62)
| ~ r1(X62,X63)
| ~ r1(X63,X64)
| ~ r1(X64,X65)
| ~ r1(X65,X78)
| ~ r1(X78,X79)
| ~ r1(X79,X80)
| p1(X80)
| r1(X78,sK22(X78)) ) ).
cnf(u56,negated_conjecture,
( ~ p1(sK44(X129))
| ~ r1(X127,X128)
| ~ r1(X128,X129)
| ~ r1(X129,X130)
| p1(X130)
| p1(X129)
| ~ r1(X129,X131)
| ~ p1(sK43(X131))
| ~ r1(sK8,X127) ) ).
cnf(u701,negated_conjecture,
( ~ r1(sK48(sK25),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| p1(X2)
| ~ r1(X2,X4)
| r1(X4,sK15(X4))
| r1(X2,sK16(X2)) ) ).
cnf(u63,negated_conjecture,
( ~ p1(sK40(X118))
| ~ r1(X113,X114)
| ~ r1(X114,X115)
| ~ r1(X115,X116)
| ~ r1(X116,X117)
| p1(X117)
| p1(X116)
| ~ r1(X116,X118)
| ~ r1(sK8,X113)
| ~ r1(sK41(X116),X121)
| ~ r1(X121,X122)
| p1(X122)
| ~ p1(X121) ) ).
cnf(u50,negated_conjecture,
( ~ r1(sK47(X141),X146)
| ~ r1(X140,X141)
| ~ r1(X141,X142)
| p1(X142)
| p1(X141)
| ~ r1(X141,X143)
| r1(X143,sK46(X143))
| ~ r1(sK8,X140)
| ~ r1(X146,X147)
| p1(X147)
| ~ p1(X146) ) ).
cnf(u682,negated_conjecture,
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p1(X10)
| ~ p1(X9)
| ~ r1(X8,X11)
| p1(X11)
| ~ p1(X8)
| ~ r1(X8,X12)
| r1(sK18(X12),sK19(X12))
| sP0(X8) ) ).
cnf(u94,negated_conjecture,
r1(sK8,sK23) ).
cnf(u809,negated_conjecture,
( ~ r1(sK11(sK14(sK17(sK30))),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK22(X0)) ) ).
cnf(u689,negated_conjecture,
( ~ r1(sK42(sK27),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| ~ p1(X5)
| ~ r1(X4,X7)
| p1(X7)
| ~ p1(X4)
| ~ r1(X4,X8)
| r1(sK18(X8),sK19(X8))
| sP0(X4) ) ).
cnf(u776,negated_conjecture,
( ~ r1(sK10(sK17(sK30)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK22(X1)) ) ).
cnf(u588,negated_conjecture,
( ~ r1(sK42(sK27),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| p1(X1)
| ~ r1(X1,X3)
| r1(X3,sK12(X3))
| r1(X1,sK13(X1)) ) ).
cnf(u279,negated_conjecture,
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| r1(X2,sK39(X2)) ) ).
cnf(u740,negated_conjecture,
( ~ r1(sK45(sK48(sK25)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| r1(X4,sK11(X4)) ) ).
cnf(u684,negated_conjecture,
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p1(X8)
| ~ p1(X7)
| ~ r1(X6,X9)
| p1(X9)
| ~ p1(X6)
| ~ r1(X6,X10)
| r1(sK18(X10),sK19(X10))
| sP0(X6) ) ).
cnf(u74,negated_conjecture,
( ~ r1(sK38(X102),X107)
| ~ r1(X98,X99)
| ~ r1(X99,X100)
| ~ r1(X100,X101)
| ~ r1(X101,X102)
| ~ r1(X102,X103)
| p1(X103)
| p1(X102)
| ~ r1(X102,X104)
| r1(X104,sK37(X104))
| ~ r1(sK8,X98)
| ~ r1(X107,X108)
| p1(X108)
| ~ p1(X107) ) ).
cnf(u696,negated_conjecture,
( ~ r1(sK14(sK31),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(X1)
| ~ r1(X0,X3)
| p1(X3)
| ~ p1(X0)
| ~ r1(X0,X4)
| r1(sK18(X4),sK19(X4))
| sP0(X0) ) ).
cnf(u703,negated_conjecture,
( ~ r1(sK45(sK26),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| p1(X1)
| ~ r1(X1,X3)
| r1(X3,sK15(X3))
| r1(X1,sK16(X1)) ) ).
cnf(u694,negated_conjecture,
( ~ r1(sK17(sK30),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| ~ p1(X2)
| ~ r1(X1,X4)
| p1(X4)
| ~ p1(X1)
| ~ r1(X1,X5)
| r1(sK18(X5),sK19(X5))
| sP0(X1) ) ).
cnf(u336,negated_conjecture,
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK42(X1)) ) ).
cnf(u693,negated_conjecture,
( ~ r1(sK31,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| ~ p1(X2)
| ~ r1(X1,X4)
| p1(X4)
| ~ p1(X1)
| ~ r1(X1,X5)
| r1(sK18(X5),sK19(X5))
| sP0(X1) ) ).
cnf(u52,negated_conjecture,
( ~ r1(sK8,X140)
| ~ r1(X140,X141)
| ~ r1(X141,X142)
| p1(X142)
| p1(X141)
| ~ r1(X141,X143)
| r1(X143,sK46(X143))
| r1(X141,sK47(X141)) ) ).
cnf(u139,negated_conjecture,
( ~ r1(sK30,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP1(X2) ) ).
cnf(u692,negated_conjecture,
( ~ r1(sK30,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| ~ p1(X3)
| ~ r1(X2,X5)
| p1(X5)
| ~ p1(X2)
| ~ r1(X2,X6)
| r1(sK18(X6),sK19(X6))
| sP0(X2) ) ).
cnf(u142,negated_conjecture,
sP1(sK33) ).
cnf(u683,negated_conjecture,
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p1(X9)
| ~ p1(X8)
| ~ r1(X7,X10)
| p1(X10)
| ~ p1(X7)
| ~ r1(X7,X11)
| r1(sK18(X11),sK19(X11))
| sP0(X7) ) ).
cnf(u520,negated_conjecture,
( ~ r1(sK42(sK27),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| p1(X2)
| ~ r1(X2,X4)
| r1(X4,sK9(X4))
| r1(X2,sK10(X2)) ) ).
cnf(u141,negated_conjecture,
( ~ r1(sK32,X0)
| sP1(X0) ) ).
cnf(u904,negated_conjecture,
( ~ r1(sK14(sK17(sK30)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(X1)
| ~ r1(X0,X3)
| p1(X3)
| ~ p1(X0)
| ~ r1(X0,X4)
| r1(sK18(X4),sK19(X4))
| sP0(X0) ) ).
cnf(u449,negated_conjecture,
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| ~ p1(X6)
| ~ r1(X5,X8)
| p1(X8)
| ~ p1(X5)
| ~ r1(X5,X9)
| p1(sK18(X9))
| sP0(X5) ) ).
cnf(u482,negated_conjecture,
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p1(X9)
| p1(X8)
| ~ r1(X8,X10)
| r1(X10,sK20(X10))
| r1(X8,sK21(X8)) ) ).
cnf(u485,negated_conjecture,
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| p1(X6)
| ~ r1(X6,X8)
| r1(X8,sK20(X8))
| r1(X6,sK21(X6)) ) ).
cnf(u707,negated_conjecture,
( ~ r1(sK10(sK17(sK30)),X0)
| sP1(X0) ) ).
cnf(u100,negated_conjecture,
( ~ p1(sK20(X73))
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| ~ r1(X57,X58)
| ~ r1(X58,X59)
| ~ r1(X59,X60)
| ~ r1(X60,X61)
| ~ r1(X61,X62)
| ~ r1(X62,X63)
| ~ r1(X63,X64)
| ~ r1(X64,X65)
| ~ r1(X65,X72)
| p1(X72)
| p1(X65)
| ~ r1(X65,X73)
| ~ r1(sK8,X55)
| r1(X65,sK21(X65)) ) ).
cnf(u264,negated_conjecture,
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| r1(X4,sK17(X4)) ) ).
cnf(u91,negated_conjecture,
r1(sK25,sK26) ).
cnf(u516,negated_conjecture,
( ~ r1(sK48(sK25),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| p1(X4)
| ~ r1(X4,X6)
| r1(X6,sK9(X6))
| r1(X4,sK10(X4)) ) ).
cnf(u440,negated_conjecture,
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| p1(X1)
| ~ r1(X1,X3)
| r1(X3,sK43(X3))
| r1(X1,sK44(X1)) ) ).
cnf(u25,axiom,
( ~ p1(sK4(X0))
| ~ r1(X1,X2)
| p1(X2)
| r1(sK2(X2),sK3(X2))
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u93,negated_conjecture,
r1(sK23,sK24) ).
cnf(u243,negated_conjecture,
( ~ r1(sK30,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK14(X0)) ) ).
cnf(u80,negated_conjecture,
( ~ r1(sK33,X95)
| p1(X95)
| r1(X95,sK35(X95)) ) ).
cnf(u787,negated_conjecture,
sP1(sK11(sK14(sK17(sK30)))) ).
cnf(u464,negated_conjecture,
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| p1(X11)
| ~ p1(X10)
| ~ r1(X9,X12)
| p1(X12)
| ~ p1(X9)
| ~ r1(X9,X13)
| r1(sK18(X13),sK19(X13))
| sP0(X9) ) ).
cnf(u87,negated_conjecture,
r1(sK29,sK30) ).
cnf(u278,negated_conjecture,
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| r1(X3,sK39(X3)) ) ).
cnf(u43,negated_conjecture,
( ~ p1(sK50(X152))
| ~ r1(X152,X153)
| p1(X153)
| p1(X152)
| ~ r1(X152,X154)
| r1(X154,sK49(X154))
| ~ r1(sK8,X152) ) ).
cnf(u73,negated_conjecture,
( ~ p1(sK37(X104))
| ~ r1(X98,X99)
| ~ r1(X99,X100)
| ~ r1(X100,X101)
| ~ r1(X101,X102)
| ~ r1(X102,X103)
| p1(X103)
| p1(X102)
| ~ r1(X102,X104)
| ~ r1(sK8,X98)
| r1(X102,sK38(X102)) ) ).
cnf(u46,negated_conjecture,
( ~ r1(sK8,X140)
| ~ r1(X140,X141)
| ~ r1(X141,X148)
| ~ r1(X148,X149)
| ~ r1(X149,X150)
| p1(X150)
| r1(X148,sK48(X148)) ) ).
cnf(u76,negated_conjecture,
( ~ r1(sK8,X98)
| ~ r1(X98,X99)
| ~ r1(X99,X100)
| ~ r1(X100,X101)
| ~ r1(X101,X102)
| ~ r1(X102,X103)
| p1(X103)
| p1(X102)
| ~ r1(X102,X104)
| r1(X104,sK37(X104))
| r1(X102,sK38(X102)) ) ).
cnf(u705,negated_conjecture,
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| p1(X2)
| ~ r1(X2,X4)
| r1(X4,sK37(X4))
| r1(X2,sK38(X2)) ) ).
cnf(u45,negated_conjecture,
( ~ p1(sK48(X148))
| ~ r1(X140,X141)
| ~ r1(X141,X148)
| ~ r1(X148,X149)
| ~ r1(X149,X150)
| p1(X150)
| ~ r1(sK8,X140) ) ).
cnf(u67,negated_conjecture,
( ~ p1(sK41(X116))
| ~ r1(X113,X114)
| ~ r1(X114,X115)
| ~ r1(X115,X116)
| ~ r1(X116,X117)
| p1(X117)
| p1(X116)
| ~ r1(X116,X118)
| r1(X118,sK40(X118))
| ~ r1(sK8,X113) ) ).
cnf(u32,axiom,
( ~ sP0(X0)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| r1(X3,sK7(X3))
| ~ r1(sK5(X0),X3) ) ).
cnf(u225,negated_conjecture,
( ~ r1(sK31,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK11(X0)) ) ).
cnf(u70,negated_conjecture,
( ~ r1(sK8,X98)
| ~ r1(X98,X99)
| ~ r1(X99,X100)
| ~ r1(X100,X101)
| ~ r1(X101,X102)
| ~ r1(X102,X109)
| ~ r1(X109,X110)
| ~ r1(X110,X111)
| p1(X111)
| r1(X109,sK39(X109)) ) ).
cnf(u39,negated_conjecture,
( ~ p1(sK49(X154))
| ~ r1(X152,X153)
| p1(X153)
| p1(X152)
| ~ r1(X152,X154)
| ~ r1(sK8,X152)
| ~ r1(sK50(X152),X157)
| ~ r1(X157,X158)
| p1(X158)
| ~ p1(X157) ) ).
cnf(u400,negated_conjecture,
( ~ r1(sK39(sK28),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK14(X1)) ) ).
cnf(u69,negated_conjecture,
( ~ p1(sK39(X109))
| ~ r1(X98,X99)
| ~ r1(X99,X100)
| ~ r1(X100,X101)
| ~ r1(X101,X102)
| ~ r1(X102,X109)
| ~ r1(X109,X110)
| ~ r1(X110,X111)
| p1(X111)
| ~ r1(sK8,X98) ) ).
cnf(u26,axiom,
( ~ sP1(X0)
| ~ r1(X1,X2)
| p1(X2)
| r1(sK2(X2),sK3(X2))
| r1(X0,sK4(X0))
| ~ r1(X0,X1) ) ).
cnf(u219,negated_conjecture,
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p1(X8)
| r1(X6,sK11(X6)) ) ).
cnf(u184,negated_conjecture,
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p1(X9)
| r1(X7,sK14(X7)) ) ).
cnf(u658,negated_conjecture,
( ~ r1(sK27,X0)
| p1(X0) ) ).
cnf(u191,negated_conjecture,
( ~ r1(sK29,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| r1(X4,sK22(X4)) ) ).
cnf(u28,axiom,
( ~ p1(sK4(X0))
| ~ r1(X1,X2)
| p1(X2)
| r1(X2,sK2(X2))
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u19,axiom,
( ~ p1(sK4(X0))
| ~ r1(X1,X2)
| p1(X2)
| p1(sK2(X2))
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u22,axiom,
( ~ p1(sK4(X0))
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(sK3(X2))
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u756,negated_conjecture,
( ~ r1(sK39(sK42(sK27)),X0)
| p1(X0) ) ).
cnf(u21,axiom,
( ~ p1(sK3(X2))
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X0,X1)
| ~ r1(sK4(X0),X6)
| ~ r1(X6,X7)
| p1(X7)
| ~ p1(X6)
| ~ sP1(X0) ) ).
cnf(u323,negated_conjecture,
( ~ r1(sK48(sK25),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| r1(X5,sK11(X5)) ) ).
cnf(u123,negated_conjecture,
( ~ r1(sK8,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ r1(X23,X24)
| ~ r1(X24,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(X27,X28)
| p1(X28)
| p1(X27)
| ~ r1(X27,X29)
| r1(X29,sK12(X29))
| r1(X27,sK13(X27)) ) ).
cnf(u933,negated_conjecture,
( ~ r1(sK45(sK48(sK25)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| p1(X3)
| ~ r1(X3,X5)
| r1(X5,sK9(X5))
| r1(X3,sK10(X3)) ) ).
cnf(u325,negated_conjecture,
( ~ r1(sK48(sK25),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| r1(X3,sK17(X3)) ) ).
cnf(u281,negated_conjecture,
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK39(X0)) ) ).
cnf(u605,negated_conjecture,
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| p1(X1)
| p1(X0)
| ~ r1(X0,X2)
| r1(X2,sK43(X2))
| r1(X0,sK44(X0)) ) ).
cnf(u112,negated_conjecture,
( ~ p1(sK15(X46))
| ~ r1(X38,X39)
| ~ r1(X39,X40)
| ~ r1(X40,X41)
| ~ r1(X41,X42)
| ~ r1(X42,X43)
| ~ r1(X43,X44)
| ~ r1(X44,X45)
| p1(X45)
| p1(X44)
| ~ r1(X44,X46)
| ~ r1(sK8,X38)
| r1(X44,sK16(X44)) ) ).
cnf(u586,negated_conjecture,
( ~ r1(sK45(sK26),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| p1(X2)
| ~ r1(X2,X4)
| r1(X4,sK12(X4))
| r1(X2,sK13(X2)) ) ).
cnf(u519,negated_conjecture,
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| p1(X2)
| ~ r1(X2,X4)
| r1(X4,sK9(X4))
| r1(X2,sK10(X2)) ) ).
cnf(u277,negated_conjecture,
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| r1(X3,sK42(X3)) ) ).
cnf(u659,negated_conjecture,
( ~ r1(sK45(sK26),X0)
| p1(X0) ) ).
cnf(u129,negated_conjecture,
( ~ r1(sK10(X9),X14)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p1(X10)
| p1(X9)
| ~ r1(X9,X11)
| r1(X11,sK9(X11))
| ~ r1(sK8,X1)
| ~ r1(X14,X15)
| p1(X15)
| ~ p1(X14) ) ).
cnf(u585,negated_conjecture,
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| p1(X2)
| ~ r1(X2,X4)
| r1(X4,sK12(X4))
| r1(X2,sK13(X2)) ) ).
cnf(u450,negated_conjecture,
( ~ r1(sK45(sK26),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| ~ p1(X6)
| ~ r1(X5,X8)
| p1(X8)
| ~ p1(X5)
| ~ r1(X5,X9)
| p1(sK18(X9))
| sP0(X5) ) ).
cnf(u648,negated_conjecture,
p1(sK27) ).
cnf(u808,negated_conjecture,
( ~ r1(sK45(sK48(sK25)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK39(X0)) ) ).
cnf(u240,negated_conjecture,
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| r1(X3,sK14(X3)) ) ).
cnf(u114,negated_conjecture,
( ~ p1(sK16(X44))
| ~ r1(X38,X39)
| ~ r1(X39,X40)
| ~ r1(X40,X41)
| ~ r1(X41,X42)
| ~ r1(X42,X43)
| ~ r1(X43,X44)
| ~ r1(X44,X45)
| p1(X45)
| p1(X44)
| ~ r1(X44,X46)
| r1(X46,sK15(X46))
| ~ r1(sK8,X38) ) ).
cnf(u99,negated_conjecture,
( ~ p1(sK21(X65))
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| ~ r1(X57,X58)
| ~ r1(X58,X59)
| ~ r1(X59,X60)
| ~ r1(X60,X61)
| ~ r1(X61,X62)
| ~ r1(X62,X63)
| ~ r1(X63,X64)
| ~ r1(X64,X65)
| ~ r1(X65,X72)
| p1(X72)
| p1(X65)
| ~ r1(X65,X73)
| ~ p1(sK20(X73))
| ~ r1(sK8,X55) ) ).
cnf(u517,negated_conjecture,
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| p1(X3)
| ~ r1(X3,X5)
| r1(X5,sK9(X5))
| r1(X3,sK10(X3)) ) ).
cnf(u647,negated_conjecture,
( ~ r1(sK48(sK25),X0)
| p1(X0) ) ).
cnf(u518,negated_conjecture,
( ~ r1(sK45(sK26),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| p1(X3)
| ~ r1(X3,X5)
| r1(X5,sK9(X5))
| r1(X3,sK10(X3)) ) ).
cnf(u222,negated_conjecture,
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| r1(X3,sK11(X3)) ) ).
cnf(u221,negated_conjecture,
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| r1(X4,sK11(X4)) ) ).
cnf(u236,negated_conjecture,
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| r1(X2,sK45(X2)) ) ).
cnf(u572,negated_conjecture,
( ~ r1(sK17(sK30),X0)
| ~ r1(X0,X1)
| sP1(X1) ) ).
cnf(u866,negated_conjecture,
( ~ r1(sK39(sK42(sK27)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| p1(X1)
| ~ r1(X1,X3)
| r1(X3,sK9(X3))
| r1(X1,sK10(X1)) ) ).
cnf(u587,negated_conjecture,
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| p1(X1)
| ~ r1(X1,X3)
| r1(X3,sK12(X3))
| r1(X1,sK13(X1)) ) ).
cnf(u204,negated_conjecture,
p1(sK22(sK34)) ).
cnf(u82,negated_conjecture,
r1(sK33,sK34) ).
cnf(u936,negated_conjecture,
( ~ r1(sK39(sK42(sK27)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| ~ r1(X3,X6)
| p1(X6)
| ~ p1(X3)
| ~ r1(X3,X7)
| r1(sK18(X7),sK19(X7))
| sP0(X3) ) ).
cnf(u195,negated_conjecture,
( ~ r1(sK33,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK22(X0)) ) ).
cnf(u386,negated_conjecture,
( ~ r1(sK45(sK26),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p1(X8)
| r1(X6,sK22(X6)) ) ).
cnf(u576,negated_conjecture,
( ~ r1(sK17(sK30),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| ~ p1(X2)
| ~ r1(X1,X4)
| p1(X4)
| ~ p1(X1)
| ~ r1(X1,X5)
| p1(sK18(X5))
| sP0(X1) ) ).
cnf(u475,negated_conjecture,
( ~ r1(sK39(sK28),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| ~ r1(X3,X6)
| p1(X6)
| ~ p1(X3)
| ~ r1(X3,X7)
| r1(X7,sK18(X7))
| sP0(X3) ) ).
cnf(u583,negated_conjecture,
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| p1(X3)
| ~ r1(X3,X5)
| r1(X5,sK12(X5))
| r1(X3,sK13(X3)) ) ).
cnf(u447,negated_conjecture,
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p1(X8)
| ~ p1(X7)
| ~ r1(X6,X9)
| p1(X9)
| ~ p1(X6)
| ~ r1(X6,X10)
| p1(sK18(X10))
| sP0(X6) ) ).
cnf(u126,negated_conjecture,
( ~ p1(sK9(X11))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p1(X10)
| p1(X9)
| ~ r1(X9,X11)
| ~ r1(sK8,X1)
| ~ r1(sK10(X9),X14)
| ~ r1(X14,X15)
| p1(X15)
| ~ p1(X14) ) ).
cnf(u477,negated_conjecture,
( ~ r1(sK31,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| ~ p1(X2)
| ~ r1(X1,X4)
| p1(X4)
| ~ p1(X1)
| ~ r1(X1,X5)
| r1(X5,sK18(X5))
| sP0(X1) ) ).
cnf(u125,negated_conjecture,
( ~ r1(sK8,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X16)
| ~ r1(X16,X17)
| ~ r1(X17,X18)
| p1(X18)
| r1(X16,sK11(X16)) ) ).
cnf(u338,negated_conjecture,
( ~ r1(sK48(sK25),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK42(X0)) ) ).
cnf(u757,negated_conjecture,
( ~ r1(sK45(sK48(sK25)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| r1(X3,sK14(X3)) ) ).
cnf(u401,negated_conjecture,
( ~ r1(sK39(sK28),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| r1(X2,sK11(X2)) ) ).
cnf(u119,negated_conjecture,
( ~ p1(sK13(X27))
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ r1(X23,X24)
| ~ r1(X24,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(X27,X28)
| p1(X28)
| p1(X27)
| ~ r1(X27,X29)
| ~ p1(sK12(X29))
| ~ r1(sK8,X20) ) ).
cnf(u427,negated_conjecture,
( ~ r1(sK42(sK27),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| r1(X2,sK14(X2)) ) ).
cnf(u106,negated_conjecture,
( ~ r1(sK8,X55)
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| ~ r1(X57,X58)
| ~ r1(X58,X59)
| ~ r1(X59,X60)
| ~ r1(X60,X61)
| ~ r1(X61,X62)
| ~ r1(X62,X63)
| ~ r1(X63,X64)
| ~ r1(X64,X65)
| ~ r1(X65,X66)
| ~ r1(X66,X67)
| p1(X67)
| ~ p1(X66)
| ~ r1(X65,X68)
| p1(X68)
| ~ p1(X65)
| ~ r1(X65,X69)
| r1(sK18(X69),sK19(X69))
| sP0(X65) ) ).
cnf(u136,negated_conjecture,
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| sP1(X5) ) ).
cnf(u105,negated_conjecture,
( ~ p1(sK19(X69))
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| ~ r1(X57,X58)
| ~ r1(X58,X59)
| ~ r1(X59,X60)
| ~ r1(X60,X61)
| ~ r1(X61,X62)
| ~ r1(X62,X63)
| ~ r1(X63,X64)
| ~ r1(X64,X65)
| ~ r1(X65,X66)
| ~ r1(X66,X67)
| p1(X67)
| ~ p1(X66)
| ~ r1(X65,X68)
| p1(X68)
| ~ p1(X65)
| ~ r1(X65,X69)
| ~ r1(sK8,X55)
| sP0(X65) ) ).
cnf(u738,negated_conjecture,
( ~ r1(sK14(sK17(sK30)),X0)
| sP1(X0) ) ).
cnf(u429,negated_conjecture,
( ~ r1(sK42(sK27),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| r1(X5,sK22(X5)) ) ).
cnf(u108,negated_conjecture,
( ~ p1(sK17(X51))
| ~ r1(X38,X39)
| ~ r1(X39,X40)
| ~ r1(X40,X41)
| ~ r1(X41,X42)
| ~ r1(X42,X43)
| ~ r1(X43,X44)
| ~ r1(X44,X51)
| ~ r1(X51,X52)
| ~ r1(X52,X53)
| p1(X53)
| ~ r1(sK8,X38) ) ).
cnf(u451,negated_conjecture,
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| ~ p1(X5)
| ~ r1(X4,X7)
| p1(X7)
| ~ p1(X4)
| ~ r1(X4,X8)
| p1(sK18(X8))
| sP0(X4) ) ).
cnf(u130,negated_conjecture,
( ~ p1(sK10(X9))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p1(X10)
| p1(X9)
| ~ r1(X9,X11)
| r1(X11,sK9(X11))
| ~ r1(sK8,X1) ) ).
cnf(u290,negated_conjecture,
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK51(X0)) ) ).
cnf(u423,negated_conjecture,
( ~ r1(sK33,X0)
| p1(X0) ) ).
cnf(u102,negated_conjecture,
( ~ p1(sK21(X65))
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| ~ r1(X57,X58)
| ~ r1(X58,X59)
| ~ r1(X59,X60)
| ~ r1(X60,X61)
| ~ r1(X61,X62)
| ~ r1(X62,X63)
| ~ r1(X63,X64)
| ~ r1(X64,X65)
| ~ r1(X65,X72)
| p1(X72)
| p1(X65)
| ~ r1(X65,X73)
| r1(X73,sK20(X73))
| ~ r1(sK8,X55) ) ).
cnf(u453,negated_conjecture,
( ~ r1(sK29,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| ~ r1(X3,X6)
| p1(X6)
| ~ p1(X3)
| ~ r1(X3,X7)
| p1(sK18(X7))
| sP0(X3) ) ).
cnf(u132,negated_conjecture,
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| sP1(X9) ) ).
cnf(u101,negated_conjecture,
( ~ r1(sK21(X65),X76)
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| ~ r1(X57,X58)
| ~ r1(X58,X59)
| ~ r1(X59,X60)
| ~ r1(X60,X61)
| ~ r1(X61,X62)
| ~ r1(X62,X63)
| ~ r1(X63,X64)
| ~ r1(X64,X65)
| ~ r1(X65,X72)
| p1(X72)
| p1(X65)
| ~ r1(X65,X73)
| r1(X73,sK20(X73))
| ~ r1(sK8,X55)
| ~ r1(X76,X77)
| p1(X77)
| ~ p1(X76) ) ).
cnf(u58,negated_conjecture,
( ~ r1(sK44(X129),X134)
| ~ r1(X127,X128)
| ~ r1(X128,X129)
| ~ r1(X129,X130)
| p1(X130)
| p1(X129)
| ~ r1(X129,X131)
| r1(X131,sK43(X131))
| ~ r1(sK8,X127)
| ~ r1(X134,X135)
| p1(X135)
| ~ p1(X134) ) ).
cnf(u88,negated_conjecture,
r1(sK28,sK29) ).
cnf(u57,negated_conjecture,
( ~ p1(sK43(X131))
| ~ r1(X127,X128)
| ~ r1(X128,X129)
| ~ r1(X129,X130)
| p1(X130)
| p1(X129)
| ~ r1(X129,X131)
| ~ r1(sK8,X127)
| r1(X129,sK44(X129)) ) ).
cnf(u690,negated_conjecture,
( ~ r1(sK29,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| ~ r1(X3,X6)
| p1(X6)
| ~ p1(X3)
| ~ r1(X3,X7)
| r1(sK18(X7),sK19(X7))
| sP0(X3) ) ).
cnf(u95,negated_conjecture,
( ~ r1(sK8,X55)
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| ~ r1(X57,X58)
| ~ r1(X58,X59)
| ~ r1(X59,X60)
| ~ r1(X60,X61)
| ~ r1(X61,X62)
| ~ r1(X62,X63)
| ~ r1(X63,X64)
| ~ r1(X64,X65)
| sP1(X65) ) ).
cnf(u60,negated_conjecture,
( ~ r1(sK8,X127)
| ~ r1(X127,X128)
| ~ r1(X128,X129)
| ~ r1(X129,X130)
| p1(X130)
| p1(X129)
| ~ r1(X129,X131)
| r1(X131,sK43(X131))
| r1(X129,sK44(X129)) ) ).
cnf(u403,negated_conjecture,
( ~ r1(sK39(sK28),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP1(X3) ) ).
cnf(u474,negated_conjecture,
( ~ r1(sK29,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| ~ r1(X3,X6)
| p1(X6)
| ~ p1(X3)
| ~ r1(X3,X7)
| r1(X7,sK18(X7))
| sP0(X3) ) ).
cnf(u51,negated_conjecture,
( ~ p1(sK47(X141))
| ~ r1(X140,X141)
| ~ r1(X141,X142)
| p1(X142)
| p1(X141)
| ~ r1(X141,X143)
| r1(X143,sK46(X143))
| ~ r1(sK8,X140) ) ).
cnf(u81,negated_conjecture,
( ~ r1(sK34,X94)
| p1(X94) ) ).
cnf(u54,negated_conjecture,
( ~ r1(sK8,X127)
| ~ r1(X127,X128)
| ~ r1(X128,X129)
| ~ r1(X129,X136)
| ~ r1(X136,X137)
| ~ r1(X137,X138)
| p1(X138)
| r1(X136,sK45(X136)) ) ).
cnf(u53,negated_conjecture,
( ~ p1(sK45(X136))
| ~ r1(X127,X128)
| ~ r1(X128,X129)
| ~ r1(X129,X136)
| ~ r1(X136,X137)
| ~ r1(X137,X138)
| p1(X138)
| ~ r1(sK8,X127) ) ).
cnf(u686,negated_conjecture,
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| ~ p1(X6)
| ~ r1(X5,X8)
| p1(X8)
| ~ p1(X5)
| ~ r1(X5,X9)
| r1(sK18(X9),sK19(X9))
| sP0(X5) ) ).
cnf(u387,negated_conjecture,
( ~ r1(sK45(sK26),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| r1(X4,sK11(X4)) ) ).
cnf(u40,negated_conjecture,
( ~ p1(sK50(X152))
| ~ r1(X152,X153)
| p1(X153)
| p1(X152)
| ~ r1(X152,X154)
| ~ p1(sK49(X154))
| ~ r1(sK8,X152) ) ).
cnf(u685,negated_conjecture,
( ~ r1(sK48(sK25),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p1(X8)
| ~ p1(X7)
| ~ r1(X6,X9)
| p1(X9)
| ~ p1(X6)
| ~ r1(X6,X10)
| r1(sK18(X10),sK19(X10))
| sP0(X6) ) ).
cnf(u47,negated_conjecture,
( ~ p1(sK46(X143))
| ~ r1(X140,X141)
| ~ r1(X141,X142)
| p1(X142)
| p1(X141)
| ~ r1(X141,X143)
| ~ r1(sK8,X140)
| ~ r1(sK47(X141),X146)
| ~ r1(X146,X147)
| p1(X147)
| ~ p1(X146) ) ).
cnf(u513,negated_conjecture,
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| p1(X5)
| ~ r1(X5,X7)
| r1(X7,sK9(X7))
| r1(X5,sK10(X5)) ) ).
cnf(u34,axiom,
( ~ p1(sK6(X0))
| ~ sP0(X0) ) ).
cnf(u471,negated_conjecture,
( ~ r1(sK45(sK26),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| ~ p1(X6)
| ~ r1(X5,X8)
| p1(X8)
| ~ p1(X5)
| ~ r1(X5,X9)
| r1(X9,sK18(X9))
| sP0(X5) ) ).
cnf(u578,negated_conjecture,
( ~ r1(sK17(sK30),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| p1(X1)
| ~ r1(X1,X3)
| r1(X3,sK20(X3))
| r1(X1,sK21(X1)) ) ).
cnf(u84,negated_conjecture,
r1(sK32,sK33) ).
cnf(u739,negated_conjecture,
( ~ r1(sK45(sK48(sK25)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p1(X8)
| r1(X6,sK22(X6)) ) ).
cnf(u324,negated_conjecture,
( ~ r1(sK48(sK25),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| r1(X4,sK14(X4)) ) ).
cnf(u637,negated_conjecture,
p1(sK48(sK25)) ).
cnf(u932,negated_conjecture,
( ~ r1(sK45(sK48(sK25)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| ~ p1(X6)
| ~ r1(X5,X8)
| p1(X8)
| ~ p1(X5)
| ~ r1(X5,X9)
| r1(X9,sK18(X9))
| sP0(X5) ) ).
cnf(u700,negated_conjecture,
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| p1(X2)
| ~ r1(X2,X4)
| r1(X4,sK15(X4))
| r1(X2,sK16(X2)) ) ).
cnf(u138,negated_conjecture,
( ~ r1(sK29,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP1(X3) ) ).
cnf(u679,negated_conjecture,
( ~ r1(sK29,X0)
| p1(X0) ) ).
cnf(u691,negated_conjecture,
( ~ r1(sK39(sK28),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| ~ r1(X3,X6)
| p1(X6)
| ~ p1(X3)
| ~ r1(X3,X7)
| r1(sK18(X7),sK19(X7))
| sP0(X3) ) ).
cnf(u672,negated_conjecture,
p1(sK29) ).
cnf(u490,negated_conjecture,
( ~ r1(sK42(sK27),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| p1(X4)
| ~ r1(X4,X6)
| r1(X6,sK20(X6))
| r1(X4,sK21(X4)) ) ).
cnf(u452,negated_conjecture,
( ~ r1(sK42(sK27),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| ~ p1(X5)
| ~ r1(X4,X7)
| p1(X7)
| ~ p1(X4)
| ~ r1(X4,X8)
| p1(sK18(X8))
| sP0(X4) ) ).
cnf(u426,negated_conjecture,
( ~ r1(sK42(sK27),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK17(X1)) ) ).
cnf(u680,negated_conjecture,
( ~ r1(sK39(sK28),X0)
| p1(X0) ) ).
cnf(u492,negated_conjecture,
( ~ r1(sK39(sK28),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| p1(X3)
| ~ r1(X3,X5)
| r1(X5,sK20(X5))
| r1(X3,sK21(X3)) ) ).
cnf(u687,negated_conjecture,
( ~ r1(sK45(sK26),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| ~ p1(X6)
| ~ r1(X5,X8)
| p1(X8)
| ~ p1(X5)
| ~ r1(X5,X9)
| r1(sK18(X9),sK19(X9))
| sP0(X5) ) ).
cnf(u570,negated_conjecture,
( ~ r1(sK14(sK31),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(X1)
| ~ r1(X0,X3)
| p1(X3)
| ~ p1(X0)
| ~ r1(X0,X4)
| r1(X4,sK18(X4))
| sP0(X0) ) ).
cnf(u515,negated_conjecture,
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| p1(X4)
| ~ r1(X4,X6)
| r1(X6,sK9(X6))
| r1(X4,sK10(X4)) ) ).
cnf(u486,negated_conjecture,
( ~ r1(sK48(sK25),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| p1(X6)
| ~ r1(X6,X8)
| r1(X8,sK20(X8))
| r1(X6,sK21(X6)) ) ).
cnf(u864,negated_conjecture,
( ~ r1(sK39(sK42(sK27)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| p1(X3)
| ~ r1(X3,X5)
| r1(X5,sK20(X5))
| r1(X3,sK21(X3)) ) ).
cnf(u263,negated_conjecture,
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| r1(X5,sK17(X5)) ) ).
cnf(u442,negated_conjecture,
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| p1(X2)
| ~ r1(X2,X4)
| r1(X4,sK40(X4))
| r1(X2,sK41(X2)) ) ).
cnf(u472,negated_conjecture,
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| ~ p1(X5)
| ~ r1(X4,X7)
| p1(X7)
| ~ p1(X4)
| ~ r1(X4,X8)
| r1(X8,sK18(X8))
| sP0(X4) ) ).
cnf(u863,negated_conjecture,
( ~ r1(sK39(sK42(sK27)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK17(X0)) ) ).
cnf(u444,negated_conjecture,
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p1(X10)
| ~ p1(X9)
| ~ r1(X8,X11)
| p1(X11)
| ~ p1(X8)
| ~ r1(X8,X12)
| p1(sK18(X12))
| sP0(X8) ) ).
cnf(u36,axiom,
( ~ sP0(X0)
| r1(X0,sK5(X0)) ) ).
cnf(u466,negated_conjecture,
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p1(X9)
| ~ p1(X8)
| ~ r1(X7,X10)
| p1(X10)
| ~ p1(X7)
| ~ r1(X7,X11)
| r1(X11,sK18(X11))
| sP0(X7) ) ).
cnf(u438,negated_conjecture,
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| p1(X11)
| ~ p1(X10)
| ~ r1(X9,X12)
| p1(X12)
| ~ p1(X9)
| ~ r1(X9,X13)
| p1(sK18(X13))
| sP0(X9) ) ).
cnf(u468,negated_conjecture,
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p1(X8)
| ~ p1(X7)
| ~ r1(X6,X9)
| p1(X9)
| ~ p1(X6)
| ~ r1(X6,X10)
| r1(X10,sK18(X10))
| sP0(X6) ) ).
cnf(u75,negated_conjecture,
( ~ p1(sK38(X102))
| ~ r1(X98,X99)
| ~ r1(X99,X100)
| ~ r1(X100,X101)
| ~ r1(X101,X102)
| ~ r1(X102,X103)
| p1(X103)
| p1(X102)
| ~ r1(X102,X104)
| r1(X104,sK37(X104))
| ~ r1(sK8,X98) ) ).
cnf(u266,negated_conjecture,
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| r1(X2,sK17(X2)) ) ).
cnf(u399,negated_conjecture,
( ~ r1(sK39(sK28),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK17(X0)) ) ).
cnf(u78,negated_conjecture,
( ~ p1(sK36(X95))
| p1(X95)
| ~ r1(sK33,X95) ) ).
cnf(u469,negated_conjecture,
( ~ r1(sK48(sK25),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p1(X8)
| ~ p1(X7)
| ~ r1(X6,X9)
| p1(X9)
| ~ p1(X6)
| ~ r1(X6,X10)
| r1(X10,sK18(X10))
| sP0(X6) ) ).
cnf(u462,negated_conjecture,
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| p1(X5)
| ~ r1(X5,X7)
| r1(X7,sK15(X7))
| r1(X5,sK16(X5)) ) ).
cnf(u77,negated_conjecture,
( p1(sK35(X95))
| p1(X95)
| ~ r1(sK33,X95) ) ).
cnf(u242,negated_conjecture,
( ~ r1(sK29,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK14(X1)) ) ).
cnf(u268,negated_conjecture,
( ~ r1(sK29,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK17(X0)) ) ).
cnf(u385,negated_conjecture,
( ~ r1(sK45(sK26),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| sP1(X5) ) ).
cnf(u64,negated_conjecture,
( ~ p1(sK41(X116))
| ~ r1(X113,X114)
| ~ r1(X114,X115)
| ~ r1(X115,X116)
| ~ r1(X116,X117)
| p1(X117)
| p1(X116)
| ~ r1(X116,X118)
| ~ p1(sK40(X118))
| ~ r1(sK8,X113) ) ).
cnf(u709,negated_conjecture,
p1(sK45(sK48(sK25))) ).
cnf(u33,axiom,
( p1(sK5(X0))
| ~ sP0(X0) ) ).
cnf(u448,negated_conjecture,
( ~ r1(sK48(sK25),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p1(X8)
| ~ p1(X7)
| ~ r1(X6,X9)
| p1(X9)
| ~ p1(X6)
| ~ r1(X6,X10)
| p1(sK18(X10))
| sP0(X6) ) ).
cnf(u71,negated_conjecture,
( ~ p1(sK37(X104))
| ~ r1(X98,X99)
| ~ r1(X99,X100)
| ~ r1(X100,X101)
| ~ r1(X101,X102)
| ~ r1(X102,X103)
| p1(X103)
| p1(X102)
| ~ r1(X102,X104)
| ~ r1(sK8,X98)
| ~ r1(sK38(X102),X107)
| ~ r1(X107,X108)
| p1(X108)
| ~ p1(X107) ) ).
cnf(u262,negated_conjecture,
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK48(X1)) ) ).
cnf(u463,negated_conjecture,
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| p1(X3)
| ~ r1(X3,X5)
| r1(X5,sK37(X5))
| r1(X3,sK38(X3)) ) ).
cnf(u404,negated_conjecture,
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| p1(X1)
| p1(X0)
| ~ r1(X0,X2)
| r1(X2,sK46(X2))
| r1(X0,sK47(X0)) ) ).
cnf(u186,negated_conjecture,
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| p1(X11)
| r1(X9,sK22(X9)) ) ).
cnf(u27,axiom,
( ~ r1(sK4(X0),X6)
| ~ r1(X1,X2)
| p1(X2)
| r1(X2,sK2(X2))
| ~ r1(X0,X1)
| ~ r1(X6,X7)
| p1(X7)
| ~ p1(X6)
| ~ sP1(X0) ) ).
cnf(u216,negated_conjecture,
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| r1(X4,sK39(X4)) ) ).
cnf(u185,negated_conjecture,
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p1(X8)
| r1(X6,sK17(X6)) ) ).
cnf(u30,axiom,
( ~ sP0(X0)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| p1(X3)
| ~ r1(sK5(X0),X3) ) ).
cnf(u223,negated_conjecture,
( ~ r1(sK29,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| r1(X2,sK11(X2)) ) ).
cnf(u571,negated_conjecture,
( ~ r1(sK14(sK31),X0)
| ~ r1(X0,X1)
| p1(X1)
| p1(X0)
| ~ r1(X0,X2)
| r1(X2,sK20(X2))
| r1(X0,sK21(X0)) ) ).
cnf(u188,negated_conjecture,
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p1(X9)
| r1(X7,sK22(X7)) ) ).
cnf(u29,axiom,
( ~ sP1(X0)
| ~ r1(X1,X2)
| p1(X2)
| r1(X2,sK2(X2))
| r1(X0,sK4(X0))
| ~ r1(X0,X1) ) ).
cnf(u210,negated_conjecture,
( ~ r1(sK35(sK34),X0)
| p1(X0) ) ).
cnf(u337,negated_conjecture,
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK42(X0)) ) ).
cnf(u661,negated_conjecture,
p1(sK42(sK27)) ).
cnf(u182,negated_conjecture,
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| p1(X12)
| r1(X10,sK22(X10)) ) ).
cnf(u23,axiom,
( ~ p1(sK3(X2))
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X0,X1)
| r1(X0,sK4(X0))
| ~ sP1(X0) ) ).
cnf(u489,negated_conjecture,
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| p1(X4)
| ~ r1(X4,X6)
| r1(X6,sK20(X6))
| r1(X4,sK21(X4)) ) ).
cnf(u567,negated_conjecture,
( ~ r1(sK14(sK31),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK22(X1)) ) ).
cnf(u388,negated_conjecture,
( ~ r1(sK45(sK26),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| r1(X3,sK14(X3)) ) ).
cnf(u303,negated_conjecture,
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK45(X0)) ) ).
cnf(u483,negated_conjecture,
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p1(X8)
| p1(X7)
| ~ r1(X7,X9)
| r1(X9,sK20(X9))
| r1(X7,sK21(X7)) ) ).
cnf(u569,negated_conjecture,
( ~ r1(sK14(sK31),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(X1)
| ~ r1(X0,X3)
| p1(X3)
| ~ p1(X0)
| ~ r1(X0,X4)
| p1(sK18(X4))
| sP0(X0) ) ).
cnf(u441,negated_conjecture,
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p1(X10)
| p1(X9)
| ~ r1(X9,X11)
| r1(X11,sK20(X11))
| r1(X9,sK21(X9)) ) ).
cnf(u120,negated_conjecture,
( ~ p1(sK12(X29))
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ r1(X23,X24)
| ~ r1(X24,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(X27,X28)
| p1(X28)
| p1(X27)
| ~ r1(X27,X29)
| ~ r1(sK8,X20)
| r1(X27,sK13(X27)) ) ).
cnf(u140,negated_conjecture,
( ~ r1(sK31,X0)
| ~ r1(X0,X1)
| sP1(X1) ) ).
cnf(u127,negated_conjecture,
( ~ p1(sK10(X9))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p1(X10)
| p1(X9)
| ~ r1(X9,X11)
| ~ p1(sK9(X11))
| ~ r1(sK8,X1) ) ).
cnf(u884,negated_conjecture,
( ~ r1(sK14(sK17(sK30)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(X1)
| ~ r1(X0,X3)
| p1(X3)
| ~ p1(X0)
| ~ r1(X0,X4)
| p1(sK18(X4))
| sP0(X0) ) ).
cnf(u566,negated_conjecture,
( ~ r1(sK14(sK31),X0)
| sP1(X0) ) ).
cnf(u116,negated_conjecture,
( ~ p1(sK14(X34))
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ r1(X23,X24)
| ~ r1(X24,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(X27,X34)
| ~ r1(X34,X35)
| ~ r1(X35,X36)
| p1(X36)
| ~ r1(sK8,X20) ) ).
cnf(u950,negated_conjecture,
( ~ r1(sK45(sK48(sK25)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| ~ p1(X6)
| ~ r1(X5,X8)
| p1(X8)
| ~ p1(X5)
| ~ r1(X5,X9)
| r1(sK18(X9),sK19(X9))
| sP0(X5) ) ).
cnf(u113,negated_conjecture,
( ~ r1(sK16(X44),X49)
| ~ r1(X38,X39)
| ~ r1(X39,X40)
| ~ r1(X40,X41)
| ~ r1(X41,X42)
| ~ r1(X42,X43)
| ~ r1(X43,X44)
| ~ r1(X44,X45)
| p1(X45)
| p1(X44)
| ~ r1(X44,X46)
| r1(X46,sK15(X46))
| ~ r1(sK8,X38)
| ~ r1(X49,X50)
| p1(X50)
| ~ p1(X49) ) ).
cnf(u778,negated_conjecture,
( ~ r1(sK45(sK48(sK25)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| r1(X2,sK17(X2)) ) ).
cnf(u590,negated_conjecture,
( ~ r1(sK39(sK28),X0)
| ~ r1(X0,X1)
| p1(X1)
| p1(X0)
| ~ r1(X0,X2)
| r1(X2,sK12(X2))
| r1(X0,sK13(X0)) ) ).
cnf(u265,negated_conjecture,
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| r1(X3,sK17(X3)) ) ).
cnf(u488,negated_conjecture,
( ~ r1(sK45(sK26),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| p1(X5)
| ~ r1(X5,X7)
| r1(X7,sK20(X7))
| r1(X5,sK21(X5)) ) ).
cnf(u589,negated_conjecture,
( ~ r1(sK29,X0)
| ~ r1(X0,X1)
| p1(X1)
| p1(X0)
| ~ r1(X0,X2)
| r1(X2,sK12(X2))
| r1(X0,sK13(X0)) ) ).
cnf(u774,negated_conjecture,
( ~ r1(sK11(sK14(sK31)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK22(X0)) ) ).
cnf(u698,negated_conjecture,
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| p1(X4)
| ~ r1(X4,X6)
| r1(X6,sK15(X6))
| r1(X4,sK16(X4)) ) ).
cnf(u898,negated_conjecture,
( ~ r1(sK14(sK17(sK30)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(X1)
| ~ r1(X0,X3)
| p1(X3)
| ~ p1(X0)
| ~ r1(X0,X4)
| r1(X4,sK18(X4))
| sP0(X0) ) ).
cnf(u96,negated_conjecture,
( ~ p1(sK22(X78))
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| ~ r1(X57,X58)
| ~ r1(X58,X59)
| ~ r1(X59,X60)
| ~ r1(X60,X61)
| ~ r1(X61,X62)
| ~ r1(X62,X63)
| ~ r1(X63,X64)
| ~ r1(X64,X65)
| ~ r1(X65,X78)
| ~ r1(X78,X79)
| ~ r1(X79,X80)
| p1(X80)
| ~ r1(sK8,X55) ) ).
cnf(u238,negated_conjecture,
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| r1(X5,sK14(X5)) ) ).
cnf(u280,negated_conjecture,
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK39(X1)) ) ).
cnf(u522,negated_conjecture,
( ~ r1(sK39(sK28),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| p1(X1)
| ~ r1(X1,X3)
| r1(X3,sK9(X3))
| r1(X1,sK10(X1)) ) ).
cnf(u521,negated_conjecture,
( ~ r1(sK29,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| p1(X1)
| ~ r1(X1,X3)
| r1(X3,sK9(X3))
| r1(X1,sK10(X1)) ) ).
cnf(u584,negated_conjecture,
( ~ r1(sK48(sK25),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| p1(X3)
| ~ r1(X3,X5)
| r1(X5,sK12(X5))
| r1(X3,sK13(X3)) ) ).
cnf(u192,negated_conjecture,
( ~ r1(sK30,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| r1(X3,sK22(X3)) ) ).
cnf(u62,negated_conjecture,
( ~ r1(sK8,X113)
| ~ r1(X113,X114)
| ~ r1(X114,X115)
| ~ r1(X115,X116)
| ~ r1(X116,X123)
| ~ r1(X123,X124)
| ~ r1(X124,X125)
| p1(X125)
| r1(X123,sK42(X123)) ) ).
cnf(u580,negated_conjecture,
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| p1(X5)
| ~ r1(X5,X7)
| r1(X7,sK12(X7))
| r1(X5,sK13(X5)) ) ).
cnf(u699,negated_conjecture,
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| p1(X3)
| ~ r1(X3,X5)
| r1(X5,sK15(X5))
| r1(X3,sK16(X3)) ) ).
cnf(u465,negated_conjecture,
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p1(X10)
| ~ p1(X9)
| ~ r1(X8,X11)
| p1(X11)
| ~ p1(X8)
| ~ r1(X8,X12)
| r1(X12,sK18(X12))
| sP0(X8) ) ).
cnf(u688,negated_conjecture,
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| ~ p1(X5)
| ~ r1(X4,X7)
| p1(X7)
| ~ p1(X4)
| ~ r1(X4,X8)
| r1(sK18(X8),sK19(X8))
| sP0(X4) ) ).
cnf(u267,negated_conjecture,
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK17(X1)) ) ).
cnf(u107,negated_conjecture,
( ~ r1(sK8,X55)
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| ~ r1(X57,X58)
| ~ r1(X58,X59)
| ~ r1(X59,X60)
| ~ r1(X60,X61)
| ~ r1(X61,X62)
| ~ r1(X62,X63)
| ~ r1(X63,X64)
| ~ r1(X64,X65)
| ~ r1(X65,X66)
| ~ r1(X66,X67)
| p1(X67)
| ~ p1(X66)
| ~ r1(X65,X68)
| p1(X68)
| ~ p1(X65)
| ~ r1(X65,X69)
| r1(X69,sK18(X69))
| sP0(X65) ) ).
cnf(u137,negated_conjecture,
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| sP1(X4) ) ).
cnf(u110,negated_conjecture,
( ~ p1(sK15(X46))
| ~ r1(X38,X39)
| ~ r1(X39,X40)
| ~ r1(X40,X41)
| ~ r1(X41,X42)
| ~ r1(X42,X43)
| ~ r1(X43,X44)
| ~ r1(X44,X45)
| p1(X45)
| p1(X44)
| ~ r1(X44,X46)
| ~ r1(sK8,X38)
| ~ r1(sK16(X44),X49)
| ~ r1(X49,X50)
| p1(X50)
| ~ p1(X49) ) ).
cnf(u461,negated_conjecture,
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| p1(X6)
| ~ r1(X6,X8)
| r1(X8,sK12(X8))
| r1(X6,sK13(X6)) ) ).
cnf(u523,negated_conjecture,
( ~ r1(sK30,X0)
| ~ r1(X0,X1)
| p1(X1)
| p1(X0)
| ~ r1(X0,X2)
| r1(X2,sK9(X2))
| r1(X0,sK10(X0)) ) ).
cnf(u494,negated_conjecture,
( ~ r1(sK31,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| p1(X1)
| ~ r1(X1,X3)
| r1(X3,sK20(X3))
| r1(X1,sK21(X1)) ) ).
cnf(u109,negated_conjecture,
( ~ r1(sK8,X38)
| ~ r1(X38,X39)
| ~ r1(X39,X40)
| ~ r1(X40,X41)
| ~ r1(X41,X42)
| ~ r1(X42,X43)
| ~ r1(X43,X44)
| ~ r1(X44,X51)
| ~ r1(X51,X52)
| ~ r1(X52,X53)
| p1(X53)
| r1(X51,sK17(X51)) ) ).
cnf(u131,negated_conjecture,
( ~ r1(sK8,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p1(X10)
| p1(X9)
| ~ r1(X9,X11)
| r1(X11,sK9(X11))
| r1(X9,sK10(X9)) ) ).
cnf(u322,negated_conjecture,
( ~ r1(sK48(sK25),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p1(X9)
| r1(X7,sK22(X7)) ) ).
cnf(u455,negated_conjecture,
( ~ r1(sK30,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| ~ p1(X3)
| ~ r1(X2,X5)
| p1(X5)
| ~ p1(X2)
| ~ r1(X2,X6)
| p1(sK18(X6))
| sP0(X2) ) ).
cnf(u134,negated_conjecture,
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| sP1(X7) ) ).
cnf(u103,negated_conjecture,
( ~ r1(sK8,X55)
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| ~ r1(X57,X58)
| ~ r1(X58,X59)
| ~ r1(X59,X60)
| ~ r1(X60,X61)
| ~ r1(X61,X62)
| ~ r1(X62,X63)
| ~ r1(X63,X64)
| ~ r1(X64,X65)
| ~ r1(X65,X72)
| p1(X72)
| p1(X65)
| ~ r1(X65,X73)
| r1(X73,sK20(X73))
| r1(X65,sK21(X65)) ) ).
cnf(u512,negated_conjecture,
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| p1(X6)
| ~ r1(X6,X8)
| r1(X8,sK9(X8))
| r1(X6,sK10(X6)) ) ).
cnf(u133,negated_conjecture,
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| sP1(X8) ) ).
cnf(u90,negated_conjecture,
r1(sK26,sK27) ).
cnf(u59,negated_conjecture,
( ~ p1(sK44(X129))
| ~ r1(X127,X128)
| ~ r1(X128,X129)
| ~ r1(X129,X130)
| p1(X130)
| p1(X129)
| ~ r1(X129,X131)
| r1(X131,sK43(X131))
| ~ r1(sK8,X127) ) ).
cnf(u89,negated_conjecture,
r1(sK27,sK28) ).
cnf(u194,negated_conjecture,
( ~ r1(sK32,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK22(X1)) ) ).
cnf(u38,negated_conjecture,
( ~ r1(sK8,X152)
| ~ r1(X152,X159)
| ~ r1(X159,X160)
| ~ r1(X160,X161)
| p1(X161)
| r1(X159,sK51(X159)) ) ).
cnf(u92,negated_conjecture,
r1(sK24,sK25) ).
cnf(u61,negated_conjecture,
( ~ p1(sK42(X123))
| ~ r1(X113,X114)
| ~ r1(X114,X115)
| ~ r1(X115,X116)
| ~ r1(X116,X123)
| ~ r1(X123,X124)
| ~ r1(X124,X125)
| p1(X125)
| ~ r1(sK8,X113) ) ).
cnf(u193,negated_conjecture,
( ~ r1(sK31,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| r1(X2,sK22(X2)) ) ).
cnf(u83,negated_conjecture,
~ p1(sK33) ).
cnf(u48,negated_conjecture,
( ~ p1(sK47(X141))
| ~ r1(X140,X141)
| ~ r1(X141,X142)
| p1(X142)
| p1(X141)
| ~ r1(X141,X143)
| ~ p1(sK46(X143))
| ~ r1(sK8,X140) ) ).
cnf(u241,negated_conjecture,
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| r1(X2,sK14(X2)) ) ).
cnf(u86,negated_conjecture,
r1(sK30,sK31) ).
cnf(u55,negated_conjecture,
( ~ p1(sK43(X131))
| ~ r1(X127,X128)
| ~ r1(X128,X129)
| ~ r1(X129,X130)
| p1(X130)
| p1(X129)
| ~ r1(X129,X131)
| ~ r1(sK8,X127)
| ~ r1(sK44(X129),X134)
| ~ r1(X134,X135)
| p1(X135)
| ~ p1(X134) ) ).
cnf(u85,negated_conjecture,
r1(sK31,sK32) ).
cnf(u718,negated_conjecture,
( ~ r1(sK45(sK48(sK25)),X0)
| p1(X0) ) ).
cnf(u42,negated_conjecture,
( ~ r1(sK50(X152),X157)
| ~ r1(X152,X153)
| p1(X153)
| p1(X152)
| ~ r1(X152,X154)
| r1(X154,sK49(X154))
| ~ r1(sK8,X152)
| ~ r1(X157,X158)
| p1(X158)
| ~ p1(X157) ) ).
cnf(u72,negated_conjecture,
( ~ p1(sK38(X102))
| ~ r1(X98,X99)
| ~ r1(X99,X100)
| ~ r1(X100,X101)
| ~ r1(X101,X102)
| ~ r1(X102,X103)
| p1(X103)
| p1(X102)
| ~ r1(X102,X104)
| ~ p1(sK37(X104))
| ~ r1(sK8,X98) ) ).
cnf(u41,negated_conjecture,
( ~ p1(sK49(X154))
| ~ r1(X152,X153)
| p1(X153)
| p1(X152)
| ~ r1(X152,X154)
| ~ r1(sK8,X152)
| r1(X152,sK50(X152)) ) ).
cnf(u79,negated_conjecture,
( r1(sK35(X95),sK36(X95))
| p1(X95)
| ~ r1(sK33,X95) ) ).
cnf(u44,negated_conjecture,
( ~ r1(sK8,X152)
| ~ r1(X152,X153)
| p1(X153)
| p1(X152)
| ~ r1(X152,X154)
| r1(X154,sK49(X154))
| r1(X152,sK50(X152)) ) ).
cnf(u673,negated_conjecture,
p1(sK39(sK28)) ).
cnf(u66,negated_conjecture,
( ~ r1(sK41(X116),X121)
| ~ r1(X113,X114)
| ~ r1(X114,X115)
| ~ r1(X115,X116)
| ~ r1(X116,X117)
| p1(X117)
| p1(X116)
| ~ r1(X116,X118)
| r1(X118,sK40(X118))
| ~ r1(sK8,X113)
| ~ r1(X121,X122)
| p1(X122)
| ~ p1(X121) ) ).
cnf(u35,axiom,
( r1(sK5(X0),sK6(X0))
| ~ sP0(X0) ) ).
cnf(u902,negated_conjecture,
( ~ r1(sK39(sK42(sK27)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| ~ r1(X3,X6)
| p1(X6)
| ~ p1(X3)
| ~ r1(X3,X7)
| r1(X7,sK18(X7))
| sP0(X3) ) ).
cnf(u65,negated_conjecture,
( ~ p1(sK40(X118))
| ~ r1(X113,X114)
| ~ r1(X114,X115)
| ~ r1(X115,X116)
| ~ r1(X116,X117)
| p1(X117)
| p1(X116)
| ~ r1(X116,X118)
| ~ r1(sK8,X113)
| r1(X116,sK41(X116)) ) ).
cnf(u326,negated_conjecture,
( ~ r1(sK48(sK25),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK39(X1)) ) ).
cnf(u389,negated_conjecture,
( ~ r1(sK45(sK26),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| r1(X2,sK17(X2)) ) ).
cnf(u68,negated_conjecture,
( ~ r1(sK8,X113)
| ~ r1(X113,X114)
| ~ r1(X114,X115)
| ~ r1(X115,X116)
| ~ r1(X116,X117)
| p1(X117)
| p1(X116)
| ~ r1(X116,X118)
| r1(X118,sK40(X118))
| r1(X116,sK41(X116)) ) ).
cnf(u37,negated_conjecture,
( ~ p1(sK51(X159))
| ~ r1(X152,X159)
| ~ r1(X159,X160)
| ~ r1(X160,X161)
| p1(X161)
| ~ r1(sK8,X152) ) ).
cnf(u670,negated_conjecture,
( ~ r1(sK28,X0)
| p1(X0) ) ).
cnf(u581,negated_conjecture,
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| p1(X4)
| ~ r1(X4,X6)
| r1(X6,sK12(X6))
| r1(X4,sK13(X4)) ) ).
cnf(u24,axiom,
( ~ r1(sK4(X0),X6)
| ~ r1(X1,X2)
| p1(X2)
| r1(sK2(X2),sK3(X2))
| ~ r1(X0,X1)
| ~ r1(X6,X7)
| p1(X7)
| ~ p1(X6)
| ~ sP1(X0) ) ).
cnf(u31,axiom,
( ~ p1(sK7(X3))
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| ~ r1(sK5(X0),X3)
| ~ sP0(X0) ) ).
cnf(u18,axiom,
( ~ r1(sK4(X0),X6)
| ~ r1(X1,X2)
| p1(X2)
| p1(sK2(X2))
| ~ r1(X0,X1)
| ~ r1(X6,X7)
| p1(X7)
| ~ p1(X6)
| ~ sP1(X0) ) ).
cnf(u854,negated_conjecture,
( ~ r1(sK39(sK42(sK27)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK14(X1)) ) ).
cnf(u930,negated_conjecture,
( ~ r1(sK45(sK48(sK25)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| p1(X5)
| ~ r1(X5,X7)
| r1(X7,sK20(X7))
| r1(X5,sK21(X5)) ) ).
cnf(u777,negated_conjecture,
( ~ r1(sK14(sK17(sK30)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK22(X1)) ) ).
cnf(u649,negated_conjecture,
p1(sK45(sK26)) ).
cnf(u454,negated_conjecture,
( ~ r1(sK39(sK28),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| ~ r1(X3,X6)
| p1(X6)
| ~ p1(X3)
| ~ r1(X3,X7)
| p1(sK18(X7))
| sP0(X3) ) ).
cnf(u719,negated_conjecture,
sP1(sK11(sK14(sK31))) ).
cnf(u806,negated_conjecture,
( ~ r1(sK39(sK42(sK27)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| r1(X4,sK22(X4)) ) ).
cnf(u574,negated_conjecture,
( ~ r1(sK17(sK30),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK11(X0)) ) ).
cnf(u708,negated_conjecture,
( ~ r1(sK45(sK48(sK25)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| sP1(X5) ) ).
cnf(u573,negated_conjecture,
( ~ r1(sK17(sK30),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| r1(X2,sK22(X2)) ) ).
cnf(u476,negated_conjecture,
( ~ r1(sK30,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| ~ p1(X3)
| ~ r1(X2,X5)
| p1(X5)
| ~ p1(X2)
| ~ r1(X2,X6)
| r1(X6,sK18(X6))
| sP0(X2) ) ).
cnf(u671,negated_conjecture,
( ~ r1(sK42(sK27),X0)
| p1(X0) ) ).
cnf(u636,negated_conjecture,
p1(sK26) ).
cnf(u470,negated_conjecture,
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| ~ p1(X6)
| ~ r1(X5,X8)
| p1(X8)
| ~ p1(X5)
| ~ r1(X5,X9)
| r1(X9,sK18(X9))
| sP0(X5) ) ).
cnf(u660,negated_conjecture,
p1(sK28) ).
cnf(u456,negated_conjecture,
( ~ r1(sK31,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| ~ p1(X2)
| ~ r1(X1,X4)
| p1(X4)
| ~ p1(X1)
| ~ r1(X1,X5)
| p1(sK18(X5))
| sP0(X1) ) ).
cnf(u430,negated_conjecture,
( ~ r1(sK42(sK27),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| sP1(X4) ) ).
cnf(u237,negated_conjecture,
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p1(X8)
| r1(X6,sK14(X6)) ) ).
cnf(u428,negated_conjecture,
( ~ r1(sK42(sK27),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| r1(X3,sK11(X3)) ) ).
cnf(u882,negated_conjecture,
( ~ r1(sK14(sK17(sK30)),X0)
| ~ r1(X0,X1)
| p1(X1)
| p1(X0)
| ~ r1(X0,X2)
| r1(X2,sK20(X2))
| r1(X0,sK21(X0)) ) ).
cnf(u224,negated_conjecture,
( ~ r1(sK30,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK11(X1)) ) ).
cnf(u931,negated_conjecture,
( ~ r1(sK45(sK48(sK25)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| ~ p1(X6)
| ~ r1(X5,X8)
| p1(X8)
| ~ p1(X5)
| ~ r1(X5,X9)
| p1(sK18(X9))
| sP0(X5) ) ).
cnf(u218,negated_conjecture,
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p1(X9)
| r1(X7,sK11(X7)) ) ).
cnf(u187,negated_conjecture,
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p1(X10)
| r1(X8,sK22(X8)) ) ).
cnf(u190,negated_conjecture,
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| r1(X5,sK22(X5)) ) ).
cnf(u220,negated_conjecture,
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| r1(X5,sK11(X5)) ) ).
cnf(u239,negated_conjecture,
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| r1(X4,sK14(X4)) ) ).
cnf(u189,negated_conjecture,
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p1(X8)
| r1(X6,sK22(X6)) ) ).
cnf(u211,negated_conjecture,
( ~ r1(sK22(sK34),X0)
| p1(X0) ) ).
cnf(u402,negated_conjecture,
( ~ r1(sK39(sK28),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| r1(X4,sK22(X4)) ) ).
cnf(u183,negated_conjecture,
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p1(X10)
| r1(X8,sK11(X8)) ) ).
cnf(u390,negated_conjecture,
( ~ r1(sK45(sK26),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK39(X0)) ) ).
cnf(u20,axiom,
( ~ sP1(X0)
| ~ r1(X1,X2)
| p1(X2)
| p1(sK2(X2))
| r1(X0,sK4(X0))
| ~ r1(X0,X1) ) ).
cnf(u491,negated_conjecture,
( ~ r1(sK29,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| p1(X3)
| ~ r1(X3,X5)
| r1(X5,sK20(X5))
| r1(X3,sK21(X3)) ) ).
cnf(u335,negated_conjecture,
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| r1(X2,sK42(X2)) ) ).
cnf(u493,negated_conjecture,
( ~ r1(sK30,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| p1(X2)
| ~ r1(X2,X4)
| r1(X4,sK20(X4))
| r1(X2,sK21(X2)) ) ).
cnf(u646,negated_conjecture,
( ~ r1(sK26,X0)
| p1(X0) ) ).
cnf(u321,negated_conjecture,
( ~ r1(sK48(sK25),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| sP1(X6) ) ).
cnf(u487,negated_conjecture,
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| p1(X5)
| ~ r1(X5,X7)
| r1(X7,sK20(X7))
| r1(X5,sK21(X5)) ) ).
cnf(u166,negated_conjecture,
p1(sK35(sK34)) ).
cnf(u443,negated_conjecture,
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p1(X8)
| p1(X7)
| ~ r1(X7,X9)
| r1(X9,sK9(X9))
| r1(X7,sK10(X7)) ) ).
cnf(u122,negated_conjecture,
( ~ p1(sK13(X27))
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ r1(X23,X24)
| ~ r1(X24,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(X27,X28)
| p1(X28)
| p1(X27)
| ~ r1(X27,X29)
| r1(X29,sK12(X29))
| ~ r1(sK8,X20) ) ).
cnf(u473,negated_conjecture,
( ~ r1(sK42(sK27),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| ~ p1(X5)
| ~ r1(X4,X7)
| p1(X7)
| ~ p1(X4)
| ~ r1(X4,X8)
| r1(X8,sK18(X8))
| sP0(X4) ) ).
cnf(u121,negated_conjecture,
( ~ r1(sK13(X27),X32)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ r1(X23,X24)
| ~ r1(X24,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(X27,X28)
| p1(X28)
| p1(X27)
| ~ r1(X27,X29)
| r1(X29,sK12(X29))
| ~ r1(sK8,X20)
| ~ r1(X32,X33)
| p1(X33)
| ~ p1(X32) ) ).
cnf(u312,negated_conjecture,
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK48(X0)) ) ).
cnf(u445,negated_conjecture,
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p1(X9)
| ~ p1(X8)
| ~ r1(X7,X10)
| p1(X10)
| ~ p1(X7)
| ~ r1(X7,X11)
| p1(sK18(X11))
| sP0(X7) ) ).
cnf(u124,negated_conjecture,
( ~ p1(sK11(X16))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X16)
| ~ r1(X16,X17)
| ~ r1(X17,X18)
| p1(X18)
| ~ r1(sK8,X1) ) ).
cnf(u115,negated_conjecture,
( ~ r1(sK8,X38)
| ~ r1(X38,X39)
| ~ r1(X39,X40)
| ~ r1(X40,X41)
| ~ r1(X41,X42)
| ~ r1(X42,X43)
| ~ r1(X43,X44)
| ~ r1(X44,X45)
| p1(X45)
| p1(X44)
| ~ r1(X44,X46)
| r1(X46,sK15(X46))
| r1(X44,sK16(X44)) ) ).
cnf(u439,negated_conjecture,
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| p1(X11)
| ~ p1(X10)
| ~ r1(X9,X12)
| p1(X12)
| ~ p1(X9)
| ~ r1(X9,X13)
| r1(X13,sK18(X13))
| sP0(X9) ) ).
cnf(u118,negated_conjecture,
( ~ p1(sK12(X29))
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ r1(X23,X24)
| ~ r1(X24,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(X27,X28)
| p1(X28)
| p1(X27)
| ~ r1(X27,X29)
| ~ r1(sK8,X20)
| ~ r1(sK13(X27),X32)
| ~ r1(X32,X33)
| p1(X33)
| ~ p1(X32) ) ).
cnf(u135,negated_conjecture,
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| sP1(X6) ) ).
cnf(u128,negated_conjecture,
( ~ p1(sK9(X11))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p1(X10)
| p1(X9)
| ~ r1(X9,X11)
| ~ r1(sK8,X1)
| r1(X9,sK10(X9)) ) ).
cnf(u117,negated_conjecture,
( ~ r1(sK8,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ r1(X23,X24)
| ~ r1(X24,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(X27,X34)
| ~ r1(X34,X35)
| ~ r1(X35,X36)
| p1(X36)
| r1(X34,sK14(X34)) ) ).
cnf(u750,negated_conjecture,
p1(sK39(sK42(sK27))) ).
cnf(u104,negated_conjecture,
( ~ r1(sK8,X55)
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| ~ r1(X57,X58)
| ~ r1(X58,X59)
| ~ r1(X59,X60)
| ~ r1(X60,X61)
| ~ r1(X61,X62)
| ~ r1(X62,X63)
| ~ r1(X63,X64)
| ~ r1(X64,X65)
| ~ r1(X65,X66)
| ~ r1(X66,X67)
| p1(X67)
| ~ p1(X66)
| ~ r1(X65,X68)
| p1(X68)
| ~ p1(X65)
| ~ r1(X65,X69)
| p1(sK18(X69))
| sP0(X65) ) ).
cnf(u749,negated_conjecture,
( ~ r1(sK39(sK42(sK27)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP1(X3) ) ).
cnf(u811,negated_conjecture,
( ~ r1(sK39(sK42(sK27)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| r1(X2,sK11(X2)) ) ).
cnf(u49,negated_conjecture,
( ~ p1(sK46(X143))
| ~ r1(X140,X141)
| ~ r1(X141,X142)
| p1(X142)
| p1(X141)
| ~ r1(X141,X143)
| ~ r1(sK8,X140)
| r1(X141,sK47(X141)) ) ).
cnf(u111,negated_conjecture,
( ~ p1(sK16(X44))
| ~ r1(X38,X39)
| ~ r1(X39,X40)
| ~ r1(X40,X41)
| ~ r1(X41,X42)
| ~ r1(X42,X43)
| ~ r1(X43,X44)
| ~ r1(X44,X45)
| p1(X45)
| p1(X44)
| ~ r1(X44,X46)
| ~ p1(sK15(X46))
| ~ r1(sK8,X38) ) ).
cnf(u302,negated_conjecture,
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK45(X1)) ) ).
cnf(u577,negated_conjecture,
( ~ r1(sK17(sK30),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| ~ p1(X2)
| ~ r1(X1,X4)
| p1(X4)
| ~ p1(X1)
| ~ r1(X1,X5)
| r1(X5,sK18(X5))
| sP0(X1) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL641+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n007.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 16:07:40 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 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.22/2.14 % (1624442)Detected formulas, will run a generic FOF schedule.
% 6.22/2.14 % (1624452)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=542089161:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 6.22/2.14 % (1624447)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=3859180418:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 6.22/2.14 % (1624451)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=269281707:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 6.22/2.14 % (1624450)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1562287812:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 6.22/2.14 % (1624453)dis-21_1_sil=8000:lcm=predicate:random_seed=2497330652: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.22/2.14 % (1624448)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=1737701199:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 6.22/2.14 % (1624449)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=1409041155:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 6.22/2.14 % (1624450)Instruction limit reached!
% 6.22/2.14 % (1624450)------------------------------
% 6.22/2.14 % (1624450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/2.14 % (1624450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/2.14 % (1624450)CaDiCaL version: 2.1.3
% 6.22/2.14 % (1624450)Termination reason: Instruction limit
% 6.22/2.14 % (1624450)Termination phase: Saturation
% 6.22/2.14 % (1624450)Time elapsed: 0.058 s
% 6.22/2.14 % (1624450)Peak memory usage: 91 MB
% 6.22/2.14 % (1624450)Instructions burned: 109 (million)
% 6.22/2.14 % (1624451)Instruction limit reached!
% 6.22/2.14 % (1624451)------------------------------
% 6.22/2.14 % (1624451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/2.14 % (1624451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/2.14 % (1624451)CaDiCaL version: 2.1.3
% 6.22/2.14 % (1624451)Termination reason: Instruction limit
% 6.22/2.14 % (1624451)Termination phase: Saturation
% 6.22/2.14 % (1624451)Time elapsed: 0.061 s
% 6.22/2.14 % (1624451)Peak memory usage: 88 MB
% 6.22/2.14 % (1624451)Instructions burned: 120 (million)
% 6.22/2.14 % (1624452)Instruction limit reached!
% 6.22/2.14 % (1624452)------------------------------
% 6.22/2.14 % (1624452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/2.14 % (1624452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/2.14 % (1624452)CaDiCaL version: 2.1.3
% 6.22/2.14 % (1624452)Termination reason: Instruction limit
% 6.22/2.14 % (1624452)Termination phase: Saturation
% 6.22/2.14 % (1624453)Instruction limit reached!
% 6.22/2.14 % (1624453)------------------------------
% 6.22/2.14 % (1624453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/2.14 % (1624452)Time elapsed: 0.065 s
% 6.22/2.14 % (1624452)Peak memory usage: 89 MB
% 6.22/2.14 % (1624453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/2.14 % (1624452)Instructions burned: 141 (million)
% 6.22/2.14 % (1624453)CaDiCaL version: 2.1.3
% 6.22/2.14 % (1624453)Termination reason: Instruction limit
% 6.22/2.14 % (1624453)Termination phase: Saturation
% 6.22/2.14 % (1624453)Time elapsed: 0.065 s
% 6.22/2.14 % (1624453)Peak memory usage: 88 MB
% 6.22/2.14 % (1624453)Instructions burned: 131 (million)
% 6.22/2.14 % (1624461)lrs+10_1_sil=8000:sp=occurrence:random_seed=465293167:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 6.22/2.14 % (1624462)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2639270896:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi)
% 6.22/2.14 % (1624464)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=423280766:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 6.22/2.14 % (1624463)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2446280605:i=325:sd=1:ss=axioms:sgt=32_2998 on theBenchmark for (2998ds/325Mi)
% 6.22/2.14 % (1624462)Refutation not found, incomplete strategy
% 6.22/2.14 % (1624462)------------------------------
% 6.22/2.14 % (1624462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/2.14 % (1624462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/2.14 % (1624462)CaDiCaL version: 2.1.3
% 6.22/2.14 % (1624462)Termination reason: Refutation not found, incomplete strategy
% 6.22/2.14 % (1624462)Time elapsed: 0.040 s
% 6.22/2.14 % (1624462)Peak memory usage: 89 MB
% 6.22/2.14 % (1624462)Instructions burned: 88 (million)
% 6.22/2.14 % (1624464)Refutation not found, incomplete strategy
% 6.22/2.14 % (1624464)------------------------------
% 6.22/2.14 % (1624464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/2.14 % (1624464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/2.14 % (1624464)CaDiCaL version: 2.1.3
% 6.22/2.14 % (1624464)Termination reason: Refutation not found, incomplete strategy
% 6.22/2.14 % (1624464)Time elapsed: 0.044 s
% 6.22/2.14 % (1624464)Peak memory usage: 89 MB
% 6.22/2.14 % (1624464)Instructions burned: 94 (million)
% 6.22/2.14 % (1624463)Refutation not found, incomplete strategy
% 6.22/2.14 % (1624463)------------------------------
% 6.22/2.14 % (1624463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/2.14 % (1624463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/2.14 % (1624463)CaDiCaL version: 2.1.3
% 6.22/2.14 % (1624463)Termination reason: Refutation not found, incomplete strategy
% 6.22/2.14 % (1624463)Time elapsed: 0.109 s
% 6.22/2.14 % (1624463)Peak memory usage: 89 MB
% 6.22/2.14 % (1624463)Instructions burned: 250 (million)
% 6.22/2.14 % (1624461)Instruction limit reached!
% 6.22/2.14 % (1624461)------------------------------
% 6.22/2.14 % (1624461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/2.14 % (1624461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/2.14 % (1624461)CaDiCaL version: 2.1.3
% 6.22/2.14 % (1624461)Termination reason: Instruction limit
% 6.22/2.14 % (1624461)Termination phase: Saturation
% 6.22/2.14 % (1624461)Time elapsed: 0.133 s
% 6.22/2.14 % (1624461)Peak memory usage: 90 MB
% 6.22/2.14 % (1624461)Instructions burned: 286 (million)
% 6.22/2.14 % (1624464)------------------------------
% 6.22/2.14 % (1624464)------------------------------
% 6.22/2.14 % (1624469)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=95766506:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 6.22/2.14 % (1624462)------------------------------
% 6.22/2.14 % (1624462)------------------------------
% 6.22/2.14 % (1624470)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1736577166:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 6.22/2.14 % (1624463)------------------------------
% 6.22/2.14 % (1624463)------------------------------
% 6.22/2.14 % (1624469)Instruction limit reached!
% 6.22/2.14 % (1624469)------------------------------
% 6.22/2.14 % (1624469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/2.14 % (1624469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/2.14 % (1624469)CaDiCaL version: 2.1.3
% 6.22/2.14 % (1624469)Termination reason: Instruction limit
% 6.22/2.14 % (1624469)Termination phase: Saturation
% 6.22/2.14 % (1624469)Time elapsed: 0.142 s
% 6.22/2.14 % (1624469)Peak memory usage: 89 MB
% 6.22/2.14 % (1624469)Instructions burned: 295 (million)
% 6.22/2.14 % (1624472)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3859428157:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 6.22/2.14 % (1624472)Instruction limit reached!
% 6.22/2.14 % (1624472)------------------------------
% 6.22/2.14 % (1624472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/2.14 % (1624472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/2.14 % (1624472)CaDiCaL version: 2.1.3
% 6.22/2.14 % (1624472)Termination reason: Instruction limit
% 6.22/2.14 % (1624472)Termination phase: Saturation
% 6.22/2.14 % (1624472)Time elapsed: 0.065 s
% 6.22/2.14 % (1624472)Peak memory usage: 90 MB
% 6.22/2.14 % (1624472)Instructions burned: 113 (million)
% 6.22/2.14 % (1624474)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3205877105:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 6.22/2.14 % (1624475)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2608196866:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 6.22/2.14 % (1624474)Instruction limit reached!
% 6.22/2.14 % (1624474)------------------------------
% 6.22/2.14 % (1624474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/2.14 % (1624474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/2.14 % (1624474)CaDiCaL version: 2.1.3
% 6.22/2.14 % (1624474)Termination reason: Instruction limit
% 6.22/2.14 % (1624474)Termination phase: Saturation
% 6.22/2.14 % (1624474)Time elapsed: 0.071 s
% 6.22/2.14 % (1624474)Peak memory usage: 89 MB
% 6.22/2.14 % (1624474)Instructions burned: 128 (million)
% 6.22/2.14 % (1624475)Instruction limit reached!
% 6.22/2.14 % (1624475)------------------------------
% 6.22/2.14 % (1624475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/2.14 % (1624475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/2.14 % (1624475)CaDiCaL version: 2.1.3
% 6.22/2.14 % (1624475)Termination reason: Instruction limit
% 6.22/2.14 % (1624475)Termination phase: Saturation
% 6.22/2.14 % (1624475)Time elapsed: 0.058 s
% 6.22/2.14 % (1624475)Peak memory usage: 89 MB
% 6.22/2.14 % (1624475)Instructions burned: 114 (million)
% 6.22/2.14 % (1624477)lrs+10_1_sil=8000:sp=occurrence:random_seed=1797907772:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 6.22/2.14 % (1624480)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3278799163:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 6.22/2.14 % (1624481)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2889386701:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 6.22/2.14 % (1624480)Instruction limit reached!
% 6.22/2.14 % (1624480)------------------------------
% 6.22/2.14 % (1624480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/2.14 % (1624480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/2.14 % (1624480)CaDiCaL version: 2.1.3
% 6.22/2.14 % (1624480)Termination reason: Instruction limit
% 6.22/2.14 % (1624480)Termination phase: Saturation
% 6.22/2.14 % (1624480)Time elapsed: 0.101 s
% 6.22/2.14 % (1624480)Peak memory usage: 89 MB
% 6.22/2.14 % (1624480)Instructions burned: 442 (million)
% 6.22/2.14 % (1624485)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1497468789:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 6.22/2.14 % (1624485)Refutation not found, incomplete strategy
% 6.22/2.14 % (1624485)------------------------------
% 6.22/2.14 % (1624485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/2.14 % (1624485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/2.14 % (1624485)CaDiCaL version: 2.1.3
% 6.22/2.14 % (1624485)Termination reason: Refutation not found, incomplete strategy
% 6.22/2.14 % (1624485)Time elapsed: 0.026 s
% 6.22/2.14 % (1624485)Peak memory usage: 89 MB
% 6.22/2.14 % (1624485)Instructions burned: 110 (million)
% 6.22/2.14 % (1624448)First to succeed.
% 6.22/2.14 % (1624448)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1624442"
% 6.22/2.14 % (1624485)------------------------------
% 6.22/2.14 % (1624485)------------------------------
% 6.22/2.14 % (1624477)Instruction limit reached!
% 6.22/2.14 % (1624477)------------------------------
% 6.22/2.14 % (1624477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.22/2.14 % (1624477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.22/2.14 % (1624477)CaDiCaL version: 2.1.3
% 6.22/2.14 % (1624477)Termination reason: Instruction limit
% 6.22/2.14 % (1624477)Termination phase: Saturation
% 6.22/2.14 % (1624477)Time elapsed: 0.429 s
% 6.22/2.14 % (1624477)Peak memory usage: 94 MB
% 6.22/2.14 % (1624477)Instructions burned: 908 (million)
% 6.22/2.14 % (1624487)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3514654744:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 6.22/2.14 % (1624488)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1853361364:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi)
% 6.22/2.14 % SZS status CounterSatisfiable for theBenchmark
% 6.22/2.14 % SZS output start Saturation.
% See solution above
% 11.23/2.33 % SZS output start Definitions and Model Updates.
% 11.23/2.33 % SZS output end Definitions and Model Updates.
% 11.23/2.33 % (1624448)------------------------------
% 11.23/2.33 % (1624448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.23/2.33 % (1624448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.23/2.33 % (1624448)CaDiCaL version: 2.1.3
% 11.23/2.33 % (1624448)Termination reason: Satisfiable
% 11.23/2.33 % (1624448)Time elapsed: 1.138 s
% 11.23/2.33 % (1624448)Peak memory usage: 133 MB
% 11.23/2.33 % (1624448)Instructions burned: 1815 (million)
% 11.23/2.33 % (1624448)------------------------------
% 11.23/2.33 % (1624448)------------------------------
% 11.23/2.33 % (1624442)Success in time 1.535 s
% 11.23/2.33 % Vampire exiting
%------------------------------------------------------------------------------