%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN513-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:17:25 PM UTC 2026
% Result : Satisfiable 0.21s 0.31s
% Output : Saturation 0.21s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u396,negated_conjecture,
~ c4_0 ).
cnf(u406,negated_conjecture,
ndr1_0 ).
cnf(u414,negated_conjecture,
~ c2_0 ).
cnf(u418,negated_conjecture,
ndr1_1(a827) ).
cnf(u422,negated_conjecture,
( ~ c2_2(a827,X3)
| c5_2(a827,X3)
| c1_2(a827,X3) ) ).
cnf(u429,negated_conjecture,
( ~ c1_2(X3,a785)
| c2_1(X3) ) ).
cnf(u436,negated_conjecture,
~ ssSkC2 ).
cnf(u440,negated_conjecture,
( ~ c2_2(X3,a785)
| c2_1(X3) ) ).
cnf(u448,negated_conjecture,
( ndr1_1(X3)
| c2_1(X3) ) ).
cnf(u452,negated_conjecture,
( ~ c2_2(X1,X2)
| ~ c3_1(X1)
| ~ c5_2(X1,a803)
| ~ ndr1_1(X1)
| ~ c3_2(X1,X2)
| ~ c4_2(X1,X2) ) ).
cnf(u455,negated_conjecture,
( ~ c4_1(X0)
| c2_1(X0) ) ).
cnf(u458,negated_conjecture,
ssSkC6 ).
cnf(u469,negated_conjecture,
~ c5_1(a827) ).
cnf(u481,negated_conjecture,
( ~ ndr1_1(X0)
| c5_2(X0,X2)
| c3_2(X0,X1)
| ~ c1_2(X0,a832)
| ~ c4_2(X0,X2)
| ~ c5_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u485,negated_conjecture,
~ ssSkC13 ).
cnf(u489,negated_conjecture,
( ~ ndr1_1(X0)
| c5_2(X0,X2)
| c3_2(X0,X1)
| ~ c2_2(X0,a832)
| ~ c4_2(X0,X2)
| ~ c5_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u493,negated_conjecture,
~ c3_0 ).
cnf(u500,negated_conjecture,
( ~ ndr1_1(X0)
| c4_2(X0,X2)
| c5_2(X0,X2)
| c3_2(X0,X2)
| ~ c1_1(X0)
| ~ c3_1(X0) ) ).
cnf(u512,negated_conjecture,
~ c1_0 ).
cnf(u516,negated_conjecture,
( ~ c4_1(X1)
| c3_1(X1)
| c4_2(X1,X2)
| c1_2(X1,X2)
| ~ c5_2(X1,X2)
| ~ ndr1_1(X1) ) ).
cnf(u541,negated_conjecture,
( ~ c2_1(X0)
| c1_1(X0)
| c4_1(X0) ) ).
cnf(u554,negated_conjecture,
~ c5_2(a796,a797) ).
cnf(u562,negated_conjecture,
~ c3_2(a796,a798) ).
cnf(u567,negated_conjecture,
~ c2_2(a796,a798) ).
cnf(u579,negated_conjecture,
ndr1_1(a855) ).
cnf(u583,negated_conjecture,
( ~ c5_2(a855,X1)
| c2_2(a855,X1)
| ~ c1_2(a855,X1) ) ).
cnf(u598,negated_conjecture,
( ~ ndr1_1(X0)
| c5_1(X0)
| c2_2(X0,X1)
| c5_2(X0,X1)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1) ) ).
cnf(u603,negated_conjecture,
~ c2_1(a796) ).
cnf(u608,negated_conjecture,
c1_2(a796,a797) ).
cnf(u613,negated_conjecture,
c2_2(a796,a797) ).
cnf(u624,negated_conjecture,
( ~ c1_1(X0)
| c2_1(X0)
| ~ c5_1(X0) ) ).
cnf(u641,negated_conjecture,
ndr1_1(a796) ).
cnf(u649,negated_conjecture,
c5_0 ).
cnf(u653,negated_conjecture,
( ~ ndr1_1(X0)
| c1_1(X0)
| c4_2(X0,X1)
| c5_2(X0,X1)
| ~ c2_2(X0,a826)
| ~ c2_2(X0,X1) ) ).
cnf(u656,negated_conjecture,
ssSkC12 ).
cnf(u661,negated_conjecture,
( ~ ndr1_1(X0)
| c1_1(X0)
| c4_2(X0,X1)
| c5_2(X0,X1)
| ~ c1_2(X0,a826)
| ~ c2_2(X0,X1) ) ).
cnf(u665,negated_conjecture,
( c4_2(a863,X2)
| c3_2(a863,X2) ) ).
cnf(u668,negated_conjecture,
ndr1_1(a863) ).
cnf(u679,negated_conjecture,
( ~ c5_1(X0)
| c1_2(X0,X1)
| c2_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c2_2(X0,a866)
| ~ ndr1_1(X0) ) ).
cnf(u683,negated_conjecture,
( ~ ndr1_1(X0)
| c1_1(X0)
| c5_2(X0,a826)
| c4_2(X0,X1)
| c5_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u687,negated_conjecture,
( ~ ssSkP3(X0)
| c1_2(X0,X1)
| ~ c5_2(X0,a834)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u691,negated_conjecture,
( ~ ssSkP3(X0)
| c1_2(X0,X1)
| ~ c2_2(X0,a834)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u695,negated_conjecture,
( ~ c5_1(X0)
| c3_2(X0,a866)
| c1_2(X0,X1)
| c2_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u706,negated_conjecture,
ssSkC0 ).
cnf(u731,negated_conjecture,
ndr1_1(a824) ).
cnf(u735,negated_conjecture,
( ~ c4_2(a824,X1)
| ~ c1_2(a824,X1) ) ).
cnf(u746,negated_conjecture,
ndr1_1(a795) ).
cnf(u753,negated_conjecture,
ssSkC5 ).
cnf(u766,negated_conjecture,
ndr1_1(a852) ).
cnf(u770,negated_conjecture,
( ~ c4_2(a852,X0)
| c1_2(a852,X0)
| ~ c5_2(a852,X0) ) ).
cnf(u773,negated_conjecture,
ssSkC16 ).
cnf(u778,negated_conjecture,
ndr1_1(a867) ).
cnf(u782,negated_conjecture,
( ~ c4_2(a867,X0)
| c3_2(a867,X0)
| c5_2(a867,X0) ) ).
cnf(u794,negated_conjecture,
ndr1_1(a891) ).
cnf(u798,negated_conjecture,
( ~ c4_2(a891,X0)
| ~ c1_2(a891,X0)
| ~ c5_2(a891,X0) ) ).
cnf(u801,negated_conjecture,
ssSkC20 ).
cnf(u805,negated_conjecture,
ssSkC19 ).
cnf(u811,negated_conjecture,
ssSkC17 ).
cnf(u834,negated_conjecture,
( ~ c1_2(a795,X0)
| c3_2(a795,X0)
| c5_2(a795,X0) ) ).
cnf(u838,negated_conjecture,
ndr1_1(a800) ).
cnf(u842,negated_conjecture,
( ~ c4_2(a800,X0)
| ~ c5_2(a800,X0)
| ~ c1_2(a800,X0) ) ).
cnf(u847,negated_conjecture,
~ c1_1(a863) ).
cnf(u859,negated_conjecture,
( ~ ndr1_1(X0)
| c5_2(X0,a886)
| c5_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u863,negated_conjecture,
( ~ ndr1_1(X0)
| c4_2(X0,a886)
| c5_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u877,negated_conjecture,
ndr1_1(a830) ).
cnf(u881,negated_conjecture,
( ~ c1_2(a830,X0)
| c2_2(a830,X0)
| ~ c3_2(a830,X0) ) ).
cnf(u892,negated_conjecture,
ssSkC14 ).
cnf(u897,negated_conjecture,
ndr1_1(a853) ).
cnf(u901,negated_conjecture,
( ~ c1_2(a853,X0)
| c5_2(a853,X0)
| c3_2(a853,X0) ) ).
cnf(u906,negated_conjecture,
c5_1(a863) ).
cnf(u913,negated_conjecture,
ssSkC18 ).
cnf(u918,negated_conjecture,
~ ssSkC1 ).
cnf(u922,negated_conjecture,
ndr1_1(a779) ).
cnf(u926,negated_conjecture,
( ~ c1_2(a779,X0)
| c3_2(a779,X0)
| c2_2(a779,X0) ) ).
cnf(u930,negated_conjecture,
~ ssSkC3 ).
cnf(u934,negated_conjecture,
ndr1_1(a786) ).
cnf(u938,negated_conjecture,
( ~ c2_2(a786,X0)
| c4_2(a786,X0)
| c5_2(a786,X0) ) ).
cnf(u942,negated_conjecture,
( ~ c1_2(a786,X0)
| c5_2(a786,X0)
| c3_2(a786,X0) ) ).
cnf(u947,negated_conjecture,
ssSkC11 ).
cnf(u958,negated_conjecture,
~ ssSkC21 ).
cnf(u962,negated_conjecture,
ndr1_1(a892) ).
cnf(u966,negated_conjecture,
( ~ c2_2(a892,X0)
| c3_2(a892,X0)
| c1_2(a892,X0) ) ).
cnf(u999,negated_conjecture,
~ c1_1(a855) ).
cnf(u1004,negated_conjecture,
c2_2(a855,a856) ).
cnf(u1009,negated_conjecture,
c5_2(a855,a856) ).
cnf(u1014,negated_conjecture,
c1_2(a855,a856) ).
cnf(u1043,negated_conjecture,
ssSkC7 ).
cnf(u1054,negated_conjecture,
( ~ c3_1(X0)
| c1_2(X0,a809)
| ~ c2_1(X0) ) ).
cnf(u1057,negated_conjecture,
ssSkC8 ).
cnf(u1062,negated_conjecture,
( ~ c3_1(X0)
| c3_2(X0,a809)
| ~ c2_1(X0) ) ).
cnf(u1066,negated_conjecture,
( ~ c3_1(X0)
| c5_2(X0,a809)
| ~ c2_1(X0) ) ).
cnf(u1093,negated_conjecture,
ssSkC9 ).
cnf(u1096,negated_conjecture,
( ~ c3_1(X0)
| c1_1(X0)
| ~ c2_2(X0,a811) ) ).
cnf(u1116,negated_conjecture,
ndr1_1(a839) ).
cnf(u1120,negated_conjecture,
( ~ c5_2(a839,X0)
| c4_2(a839,X0) ) ).
cnf(u1124,negated_conjecture,
( ~ c1_2(a853,X0)
| c2_2(a853,X0) ) ).
cnf(u1128,negated_conjecture,
ndr1_1(a875) ).
cnf(u1132,negated_conjecture,
( ~ c4_2(a875,X0)
| ~ c1_2(a875,X0) ) ).
cnf(u1136,negated_conjecture,
( ~ c5_2(a891,X0)
| c3_2(a891,X0) ) ).
cnf(u1149,negated_conjecture,
ssSkC22 ).
cnf(u1152,negated_conjecture,
ndr1_1(a893) ).
cnf(u1160,negated_conjecture,
( ~ c4_1(X0)
| c3_1(X0)
| ~ c5_1(X0) ) ).
cnf(u1168,negated_conjecture,
( ~ c3_1(X0)
| ndr1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u1193,negated_conjecture,
ssSkC4 ).
cnf(u1228,negated_conjecture,
( ~ c4_1(X0)
| c4_2(X0,a805) ) ).
cnf(u1237,negated_conjecture,
~ c4_1(a824) ).
cnf(u1242,negated_conjecture,
~ c2_1(a824) ).
cnf(u1250,negated_conjecture,
( ~ ssSkP5(X0)
| ~ c4_2(X0,a872) ) ).
cnf(u1254,negated_conjecture,
( ~ ssSkP5(X0)
| ~ c5_2(X0,a872) ) ).
cnf(u1258,negated_conjecture,
( ~ c4_1(X0)
| ~ c1_2(X0,a784) ) ).
cnf(u1266,negated_conjecture,
( ~ c4_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ) ).
cnf(u1290,negated_conjecture,
( ~ c3_1(X0)
| c1_1(X0)
| ndr1_1(X0) ) ).
cnf(u1314,negated_conjecture,
( c5_2(a800,X0)
| c2_2(a800,X0) ) ).
cnf(u1318,negated_conjecture,
( ~ c4_1(X0)
| ndr1_1(X0) ) ).
cnf(u1322,negated_conjecture,
( c5_2(a830,X0)
| c1_2(a830,X0) ) ).
cnf(u1330,negated_conjecture,
( ~ ssSkP5(X0)
| c3_2(X0,a872) ) ).
cnf(u1334,negated_conjecture,
( ~ c4_1(X0)
| c2_2(X0,a784) ) ).
cnf(u1338,negated_conjecture,
( ~ c4_1(X0)
| c3_2(X0,a784) ) ).
cnf(u1358,negated_conjecture,
( ~ c4_1(X0)
| ~ c5_1(X0) ) ).
cnf(u1363,negated_conjecture,
~ c3_2(a867,a868) ).
cnf(u1368,negated_conjecture,
~ c4_2(a867,a869) ).
cnf(u1372,negated_conjecture,
( ~ ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(u1382,negated_conjecture,
c5_2(a867,a868) ).
cnf(u1387,negated_conjecture,
c3_2(a867,a869) ).
cnf(u1392,negated_conjecture,
c2_2(a867,a869) ).
cnf(u1406,negated_conjecture,
( c3_1(X0)
| c1_1(X0) ) ).
cnf(u1416,negated_conjecture,
~ c1_1(a795) ).
cnf(u1426,negated_conjecture,
~ c5_2(a820,a821) ).
cnf(u1429,negated_conjecture,
ssSkC10 ).
cnf(u1435,negated_conjecture,
~ c3_2(a820,a821) ).
cnf(u1440,negated_conjecture,
~ c2_2(a820,a822) ).
cnf(u1445,negated_conjecture,
~ c5_2(a820,a822) ).
cnf(u1450,negated_conjecture,
~ c5_2(a839,a840) ).
cnf(u1455,negated_conjecture,
~ c4_2(a839,a841) ).
cnf(u1460,negated_conjecture,
~ c2_2(a839,a841) ).
cnf(u1465,negated_conjecture,
~ c1_1(a843) ).
cnf(u1520,negated_conjecture,
~ c1_2(a894,a895) ).
cnf(u1524,negated_conjecture,
c5_2(a894,a895) ).
cnf(u1642,negated_conjecture,
c1_2(a820,a821) ).
cnf(u1657,negated_conjecture,
c2_2(a839,a840) ).
cnf(u1662,negated_conjecture,
c4_2(a839,a840) ).
cnf(u1667,negated_conjecture,
c5_1(a843) ).
cnf(u1672,negated_conjecture,
c1_1(a852) ).
cnf(u1677,negated_conjecture,
c2_2(a853,a854) ).
cnf(u1682,negated_conjecture,
c3_2(a853,a854) ).
cnf(u1687,negated_conjecture,
~ c1_2(a858,a859) ).
cnf(u1728,negated_conjecture,
~ c3_1(a891) ).
cnf(u1732,negated_conjecture,
c2_1(a894) ).
cnf(u1738,negated_conjecture,
c3_2(a894,a895) ).
cnf(u1753,negated_conjecture,
~ c3_1(a779) ).
cnf(u1758,negated_conjecture,
~ c4_1(a786) ).
cnf(u1788,negated_conjecture,
~ c4_1(a831) ).
cnf(u1798,negated_conjecture,
~ c3_1(a844) ).
cnf(u1828,negated_conjecture,
~ c4_1(a892) ).
cnf(u1832,negated_conjecture,
c5_1(a893) ).
cnf(u1862,negated_conjecture,
~ c3_1(a812) ).
cnf(u1867,negated_conjecture,
c2_2(a812,a813) ).
cnf(u1872,negated_conjecture,
c1_2(a812,a813) ).
cnf(u1877,negated_conjecture,
c3_2(a812,a813) ).
cnf(u1892,negated_conjecture,
ndr1_1(a820) ).
cnf(u1902,negated_conjecture,
c2_2(a858,a859) ).
cnf(u1907,negated_conjecture,
c3_2(a858,a859) ).
cnf(u1927,negated_conjecture,
~ c4_1(a875) ).
cnf(u1932,negated_conjecture,
c4_1(a894) ).
cnf(u1937,negated_conjecture,
ndr1_1(a894) ).
cnf(u1964,negated_conjecture,
c2_1(a817) ).
cnf(u1968,negated_conjecture,
~ c4_1(a817) ).
cnf(u1980,negated_conjecture,
c3_1(a831) ).
cnf(u2020,negated_conjecture,
c5_1(a892) ).
cnf(u2030,negated_conjecture,
c2_1(a800) ).
cnf(u2035,negated_conjecture,
ndr1_1(a812) ).
cnf(u2041,negated_conjecture,
c2_1(a830) ).
cnf(u2048,negated_conjecture,
c5_1(a858) ).
cnf(u2053,negated_conjecture,
ndr1_1(a858) ).
cnf(u2059,negated_conjecture,
c2_1(a875) ).
cnf(u2118,negated_conjecture,
~ c4_1(a830) ).
cnf(u2123,negated_conjecture,
c1_1(a830) ).
cnf(u2128,negated_conjecture,
c4_1(a800) ).
cnf(u2187,negated_conjecture,
~ ssSkP3(a800) ).
cnf(u2192,negated_conjecture,
c2_2(a800,a833) ).
cnf(u2199,negated_conjecture,
ssSkP7(a830) ).
cnf(u2210,negated_conjecture,
~ c2_1(a858) ).
cnf(u2219,negated_conjecture,
~ c2_1(a843) ).
cnf(u2234,negated_conjecture,
~ c2_2(a858,a811) ).
cnf(u2246,negated_conjecture,
c3_2(a858,a811) ).
cnf(u2266,negated_conjecture,
c1_2(a830,a872) ).
cnf(u2274,negated_conjecture,
~ c2_2(a800,a872) ).
cnf(u2279,negated_conjecture,
c5_2(a800,a871) ).
cnf(u2287,negated_conjecture,
~ c3_2(a830,a872) ).
cnf(u2300,negated_conjecture,
~ c2_2(a795,a871) ).
cnf(u2322,negated_conjecture,
c4_2(a839,a871) ).
cnf(u2336,negated_conjecture,
( ~ c2_2(a867,X0)
| c5_2(a867,X0) ) ).
cnf(u2344,negated_conjecture,
( ~ c2_2(a820,X0)
| c5_2(a820,X0) ) ).
cnf(u2356,negated_conjecture,
c5_2(a839,a886) ).
cnf(u2360,negated_conjecture,
( ~ c2_2(a853,X0)
| c5_2(a853,X0) ) ).
cnf(u2368,negated_conjecture,
( ~ c2_2(a858,X0)
| c5_2(a858,X0) ) ).
cnf(u2395,negated_conjecture,
~ c5_1(a817) ).
cnf(u2423,negated_conjecture,
c5_1(a779) ).
cnf(u2428,negated_conjecture,
c2_1(a779) ).
cnf(u2432,negated_conjecture,
c5_1(a844) ).
cnf(u2437,negated_conjecture,
c2_1(a844) ).
cnf(u2441,negated_conjecture,
c5_1(a852) ).
cnf(u2446,negated_conjecture,
c2_1(a852) ).
cnf(u2451,negated_conjecture,
c5_1(a891) ).
cnf(u2456,negated_conjecture,
c2_1(a891) ).
cnf(u2484,negated_conjecture,
c5_1(a867) ).
cnf(u2491,negated_conjecture,
~ c1_2(a800,a791) ).
cnf(u2495,negated_conjecture,
~ c5_1(a800) ).
cnf(u2507,negated_conjecture,
~ c5_1(a830) ).
cnf(u2523,negated_conjecture,
c3_1(a830) ).
cnf(u2551,negated_conjecture,
c3_2(a867,a791) ).
cnf(u2558,negated_conjecture,
c3_2(a800,a791) ).
cnf(u2563,negated_conjecture,
c3_2(a830,a791) ).
cnf(u2573,negated_conjecture,
c4_2(a867,a791) ).
cnf(u2580,negated_conjecture,
c4_2(a800,a791) ).
cnf(u2585,negated_conjecture,
c4_2(a830,a791) ).
cnf(u2597,negated_conjecture,
c5_2(a800,a834) ).
cnf(u2610,negated_conjecture,
~ c2_2(a800,a834) ).
cnf(u2623,negated_conjecture,
( ~ c5_2(a817,X0)
| c4_2(a817,X0)
| c1_2(a817,X0) ) ).
cnf(u2627,negated_conjecture,
( ~ c5_2(a800,X0)
| c4_2(a800,X0)
| c1_2(a800,X0) ) ).
cnf(u2641,negated_conjecture,
~ c2_1(a839) ).
cnf(u2654,negated_conjecture,
~ c2_1(a853) ).
cnf(u2680,negated_conjecture,
~ c2_2(a863,a866) ).
cnf(u2688,negated_conjecture,
~ c2_2(a858,a866) ).
cnf(u2696,negated_conjecture,
~ c2_2(a843,a866) ).
cnf(u2699,negated_conjecture,
( ~ c3_2(a843,X0)
| c1_2(a843,X0)
| c2_2(a843,X0) ) ).
cnf(u2721,negated_conjecture,
c3_2(a863,a866) ).
cnf(u2726,negated_conjecture,
c3_2(a858,a866) ).
cnf(u2780,negated_conjecture,
~ c1_2(a839,a832) ).
cnf(u2791,negated_conjecture,
~ c1_2(a853,a832) ).
cnf(u2802,negated_conjecture,
~ c1_2(a858,a832) ).
cnf(u2820,negated_conjecture,
~ c2_2(a839,a832) ).
cnf(u2825,negated_conjecture,
~ c2_2(a853,a832) ).
cnf(u2830,negated_conjecture,
~ c2_2(a858,a832) ).
cnf(u2842,negated_conjecture,
~ c2_2(a894,a785) ).
cnf(u2864,negated_conjecture,
c3_2(a839,a832) ).
cnf(u2869,negated_conjecture,
c3_2(a853,a832) ).
cnf(u2874,negated_conjecture,
c3_2(a858,a832) ).
cnf(u2893,negated_conjecture,
c5_1(a824) ).
cnf(u2917,negated_conjecture,
c5_2(a867,a791) ).
cnf(u2926,negated_conjecture,
c2_2(a894,a895) ).
cnf(u2938,negated_conjecture,
( ~ c3_2(a824,X0)
| c1_2(a824,X0)
| c2_2(a824,X0) ) ).
cnf(u2950,negated_conjecture,
c5_2(a839,a832) ).
cnf(u2958,negated_conjecture,
c5_2(a853,a832) ).
cnf(u2981,negated_conjecture,
c4_2(a839,a886) ).
cnf(u2984,negated_conjecture,
~ c2_2(a839,a886) ).
cnf(u3029,negated_conjecture,
~ c1_2(a855,a871) ).
cnf(u3043,negated_conjecture,
c1_1(a817) ).
cnf(u3047,negated_conjecture,
c1_2(a817,a809) ).
cnf(u3052,negated_conjecture,
c1_2(a800,a809) ).
cnf(u3057,negated_conjecture,
c1_2(a830,a809) ).
cnf(u3064,negated_conjecture,
c4_2(a853,a785) ).
cnf(u3067,negated_conjecture,
~ c2_2(a853,a785) ).
cnf(u3087,negated_conjecture,
c3_2(a817,a809) ).
cnf(u3092,negated_conjecture,
c3_2(a800,a809) ).
cnf(u3097,negated_conjecture,
c3_2(a830,a809) ).
cnf(u3105,negated_conjecture,
c4_2(a839,a785) ).
cnf(u3121,negated_conjecture,
c5_2(a817,a809) ).
cnf(u3126,negated_conjecture,
c5_2(a800,a809) ).
cnf(u3131,negated_conjecture,
c5_2(a830,a809) ).
cnf(u3141,negated_conjecture,
~ c5_1(a894) ).
cnf(u3151,negated_conjecture,
( ~ c5_2(a894,X0)
| c4_2(a894,X0)
| c1_2(a894,X0) ) ).
cnf(u3164,negated_conjecture,
c1_2(a894,a809) ).
cnf(u3169,negated_conjecture,
c3_2(a894,a809) ).
cnf(u3174,negated_conjecture,
c5_2(a894,a809) ).
cnf(u3186,negated_conjecture,
( ~ c3_2(a892,X0)
| c1_2(a892,X0)
| c2_2(a892,X0) ) ).
cnf(u3212,negated_conjecture,
c1_1(a786) ).
cnf(u3217,negated_conjecture,
c5_2(a892,a785) ).
cnf(u3228,negated_conjecture,
~ c5_1(a786) ).
cnf(u3250,negated_conjecture,
c5_2(a894,a886) ).
cnf(u3262,negated_conjecture,
c5_2(a800,a886) ).
cnf(u3265,negated_conjecture,
~ c5_2(a800,a833) ).
cnf(u3272,negated_conjecture,
c5_2(a800,a872) ).
cnf(u3281,negated_conjecture,
~ c1_2(a800,a805) ).
cnf(u3284,negated_conjecture,
c5_2(a800,a805) ).
cnf(u3323,negated_conjecture,
c4_2(a800,a886) ).
cnf(u3333,negated_conjecture,
c3_2(a817,a872) ).
cnf(u3352,negated_conjecture,
c3_2(a843,a871) ).
cnf(u3369,negated_conjecture,
c4_2(a853,a832) ).
cnf(u3385,negated_conjecture,
c4_2(a894,a871) ).
cnf(u3392,negated_conjecture,
~ c2_2(a843,a811) ).
cnf(u3411,negated_conjecture,
c1_2(a892,a872) ).
cnf(u3425,negated_conjecture,
c5_2(a795,a811) ).
cnf(u3428,negated_conjecture,
~ c2_2(a795,a811) ).
cnf(u3468,negated_conjecture,
~ c2_2(a839,a871) ).
cnf(u3476,negated_conjecture,
~ c5_2(a839,a803) ).
cnf(u3482,negated_conjecture,
~ c2_2(a894,a805) ).
cnf(u3490,negated_conjecture,
~ c5_2(a894,a803) ).
cnf(u3499,negated_conjecture,
~ c3_2(a817,a805) ).
cnf(u3512,negated_conjecture,
~ c3_2(a800,a805) ).
cnf(u3516,negated_conjecture,
~ c5_2(a800,a803) ).
cnf(u3522,negated_conjecture,
~ c2_2(a830,a805) ).
cnf(u3530,negated_conjecture,
~ c5_2(a830,a803) ).
cnf(u3540,negated_conjecture,
~ c2_2(a867,a791) ).
cnf(u3549,negated_conjecture,
~ c3_2(a839,a840) ).
cnf(u3554,negated_conjecture,
~ c2_2(a800,a791) ).
cnf(u3559,negated_conjecture,
~ c2_2(a830,a791) ).
cnf(u3582,negated_conjecture,
c4_2(a800,a803) ).
cnf(u3632,negated_conjecture,
c1_2(a830,a834) ).
cnf(u3747,negated_conjecture,
c1_1(a796) ).
cnf(u3769,negated_conjecture,
~ c2_2(a796,a785) ).
cnf(u3774,negated_conjecture,
c3_2(a796,a791) ).
cnf(u3779,negated_conjecture,
c4_2(a796,a791) ).
cnf(u3798,negated_conjecture,
~ c1_2(a863,a832) ).
cnf(u3807,negated_conjecture,
~ c1_2(a894,a832) ).
cnf(u3815,negated_conjecture,
~ c1_2(a817,a832) ).
cnf(u3824,negated_conjecture,
~ c1_2(a800,a832) ).
cnf(u3832,negated_conjecture,
~ c1_2(a830,a832) ).
cnf(u3857,negated_conjecture,
~ c2_2(a863,a832) ).
cnf(u3863,negated_conjecture,
~ c2_2(a894,a832) ).
cnf(u3868,negated_conjecture,
~ c2_2(a817,a832) ).
cnf(u3874,negated_conjecture,
~ c2_2(a800,a832) ).
cnf(u3879,negated_conjecture,
~ c2_2(a830,a832) ).
cnf(u3930,negated_conjecture,
c5_2(a831,a785) ).
cnf(u3933,negated_conjecture,
~ c1_1(a831) ).
cnf(u3967,negated_conjecture,
~ c5_2(a831,a803) ).
cnf(u3972,negated_conjecture,
~ c2_1(a831) ).
cnf(u4010,negated_conjecture,
c2_2(a817,a809) ).
cnf(u4034,negated_conjecture,
c4_2(a894,a809) ).
cnf(u4054,negated_conjecture,
c4_2(a800,a833) ).
cnf(u4070,negated_conjecture,
( c5_2(a817,X0)
| c1_2(a817,X0)
| c3_2(a817,X0) ) ).
cnf(u4085,negated_conjecture,
c2_2(a843,a871) ).
cnf(u4100,negated_conjecture,
c3_2(a894,a871) ).
cnf(u4110,negated_conjecture,
~ c3_2(a830,a834) ).
cnf(u4133,negated_conjecture,
( c5_2(a796,X0)
| c1_2(a796,X0)
| c3_2(a796,X0) ) ).
cnf(u4141,negated_conjecture,
c2_2(a796,a791) ).
cnf(u4149,negated_conjecture,
~ c1_2(a796,a832) ).
cnf(u4157,negated_conjecture,
~ c2_2(a796,a832) ).
cnf(u4176,negated_conjecture,
c5_1(a831) ).
cnf(u4197,negated_conjecture,
( ~ c3_2(a831,X0)
| c1_2(a831,X0)
| c2_2(a831,X0) ) ).
cnf(u4250,negated_conjecture,
( c4_2(a830,X0)
| c5_2(a830,X0)
| c3_2(a830,X0) ) ).
cnf(u4264,negated_conjecture,
c3_2(a892,a811) ).
cnf(u4296,negated_conjecture,
c1_2(a855,a809) ).
cnf(u4301,negated_conjecture,
c5_2(a795,a785) ).
cnf(u4319,negated_conjecture,
c3_2(a855,a809) ).
cnf(u4338,negated_conjecture,
c5_2(a855,a809) ).
cnf(u4353,negated_conjecture,
c4_2(a855,a805) ).
cnf(u4367,negated_conjecture,
c1_2(a800,a871) ).
cnf(u4376,negated_conjecture,
c1_2(a800,a834) ).
cnf(u4451,negated_conjecture,
c3_2(a779,a872) ).
cnf(u4518,negated_conjecture,
c1_2(a800,a872) ).
cnf(u4599,negated_conjecture,
c3_2(a827,a871) ).
cnf(u4680,negated_conjecture,
c3_2(a786,a871) ).
cnf(u4683,negated_conjecture,
( c5_2(a786,X0)
| c3_2(a786,X0) ) ).
cnf(u4720,negated_conjecture,
( ~ c3_2(a827,X0)
| c1_2(a827,X0)
| c2_2(a827,X0) ) ).
cnf(u4737,negated_conjecture,
( ~ c3_2(a893,X0)
| c1_2(a893,X0)
| c2_2(a893,X0) ) ).
cnf(u4755,negated_conjecture,
c5_2(a812,a813) ).
cnf(u4772,negated_conjecture,
( ~ c3_2(a852,X0)
| c1_2(a852,X0)
| c2_2(a852,X0) ) ).
cnf(u4788,negated_conjecture,
~ c5_1(a812) ).
cnf(u4808,negated_conjecture,
( ~ c3_2(a779,X0)
| c1_2(a779,X0)
| c2_2(a779,X0) ) ).
cnf(u4834,negated_conjecture,
~ c2_2(a844,a866) ).
cnf(u4842,negated_conjecture,
c3_2(a844,a866) ).
cnf(u4909,negated_conjecture,
~ c2_2(a891,a866) ).
cnf(u4917,negated_conjecture,
c3_2(a891,a866) ).
cnf(u4958,negated_conjecture,
c4_2(a894,a886) ).
cnf(u4963,negated_conjecture,
c4_2(a894,a784) ).
cnf(u4975,negated_conjecture,
c3_2(a812,a871) ).
cnf(u4989,negated_conjecture,
c1_2(a893,a872) ).
cnf(u5021,negated_conjecture,
c5_2(a800,a784) ).
cnf(u5025,negated_conjecture,
c4_2(a800,a784) ).
cnf(u5039,negated_conjecture,
c1_2(a852,a872) ).
cnf(u5103,negated_conjecture,
c5_2(a843,a871) ).
cnf(u5117,negated_conjecture,
c5_2(a894,a871) ).
cnf(u5123,negated_conjecture,
~ c2_2(a892,a811) ).
cnf(u5128,negated_conjecture,
c1_2(a892,a811) ).
cnf(u5134,negated_conjecture,
~ c2_2(a795,a785) ).
cnf(u5154,negated_conjecture,
~ c1_2(a855,a832) ).
cnf(u5162,negated_conjecture,
~ c2_2(a855,a832) ).
cnf(u5175,negated_conjecture,
~ c5_2(a855,a803) ).
cnf(u5183,negated_conjecture,
c1_2(a827,a871) ).
cnf(u5188,negated_conjecture,
c5_2(a827,a871) ).
cnf(u5195,negated_conjecture,
c5_2(a812,a871) ).
cnf(u5220,negated_conjecture,
c1_2(a824,a872) ).
cnf(u5244,negated_conjecture,
c1_2(a855,a834) ).
cnf(u5254,negated_conjecture,
ssSkP7(a855) ).
cnf(u5286,negated_conjecture,
c1_2(a817,a834) ).
cnf(u5304,negated_conjecture,
c1_2(a817,a881) ).
cnf(u5344,negated_conjecture,
c1_2(a796,a834) ).
cnf(u5362,negated_conjecture,
c1_2(a796,a881) ).
cnf(u5414,negated_conjecture,
ssSkP0(a800) ).
cnf(u5427,negated_conjecture,
ssSkP4(a800) ).
cnf(u5441,negated_conjecture,
c1_2(a779,a872) ).
cnf(u5463,negated_conjecture,
~ c3_2(a830,a803) ).
cnf(u5520,negated_conjecture,
~ c2_2(a867,a872) ).
cnf(u5525,negated_conjecture,
c3_2(a867,a866) ).
cnf(u5529,negated_conjecture,
c3_2(a867,a871) ).
cnf(u5537,negated_conjecture,
c2_2(a839,a872) ).
cnf(u5551,negated_conjecture,
c3_2(a853,a866) ).
cnf(u5614,negated_conjecture,
c3_2(a855,a803) ).
cnf(u5665,negated_conjecture,
~ c2_2(a867,a866) ).
cnf(u5680,negated_conjecture,
~ c4_2(a839,a872) ).
cnf(u5685,negated_conjecture,
c5_2(a839,a826) ).
cnf(u5695,negated_conjecture,
c5_2(a853,a866) ).
cnf(u5709,negated_conjecture,
( ~ c2_2(a786,X0)
| ~ c3_2(a786,X0)
| c1_2(a786,X0) ) ).
cnf(u5727,negated_conjecture,
c3_2(a786,a881) ).
cnf(u5748,negated_conjecture,
c1_2(a831,a872) ).
cnf(u5766,negated_conjecture,
c1_2(a817,a787) ).
cnf(u5852,negated_conjecture,
c3_2(a820,a871) ).
cnf(u5868,negated_conjecture,
c2_2(a855,a803) ).
cnf(u5886,negated_conjecture,
c5_2(a820,a871) ).
cnf(u5901,negated_conjecture,
c4_2(a855,a803) ).
cnf(u5933,negated_conjecture,
~ c1_2(a855,a886) ).
cnf(clause98,negated_conjecture,
( ssSkP9(X0)
| c2_2(X0,a889) ) ).
cnf(u2998,negated_conjecture,
c5_2(a858,a859) ).
cnf(clause177,negated_conjecture,
( ~ c3_2(X0,a807)
| ssSkP2(X0) ) ).
cnf(u2403,negated_conjecture,
( ~ c2_1(X0)
| c1_2(X0,a809)
| c1_1(X0) ) ).
cnf(u2405,negated_conjecture,
( ~ c2_1(X0)
| c5_2(X0,a809)
| c1_1(X0) ) ).
cnf(u5271,negated_conjecture,
( c4_2(a817,X0)
| c3_2(a817,X0)
| c1_2(a817,X0) ) ).
cnf(u2328,negated_conjecture,
( ~ c2_2(X0,X1)
| c5_2(X0,X1)
| c5_2(X0,a886) ) ).
cnf(u2604,negated_conjecture,
( ~ c2_2(X0,a834)
| c1_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1)
| c1_2(X0,a833) ) ).
cnf(u5768,negated_conjecture,
c4_2(a839,a826) ).
cnf(u2591,negated_conjecture,
( ~ c5_2(X0,a834)
| c1_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1)
| c3_2(X0,a833) ) ).
cnf(clause49,negated_conjecture,
( ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(u2084,negated_conjecture,
ndr1_1(X0) ).
cnf(u2459,negated_conjecture,
( ~ c2_2(X0,X1)
| c5_2(X0,X1)
| c4_2(X0,a886) ) ).
cnf(clause43,negated_conjecture,
( ssSkP8(X0)
| ndr1_1(X0) ) ).
cnf(clause46,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(clause45,negated_conjecture,
( ssSkP6(X0)
| ndr1_1(X0) ) ).
cnf(u2109,negated_conjecture,
( ~ c5_2(X0,a872)
| c3_2(X0,a871) ) ).
cnf(u2411,negated_conjecture,
c1_1(a844) ).
cnf(u2413,negated_conjecture,
c1_1(a891) ).
cnf(clause178,negated_conjecture,
( ~ c2_2(X0,a807)
| ssSkP2(X0) ) ).
cnf(u2375,negated_conjecture,
( ~ c3_2(X0,X1)
| c2_2(X0,X1)
| c5_2(X0,X1)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| c5_1(X0) ) ).
cnf(u2969,negated_conjecture,
c5_2(a867,a869) ).
cnf(u3003,negated_conjecture,
c1_2(a800,a833) ).
cnf(u4826,negated_conjecture,
c3_2(a894,a784) ).
cnf(clause99,negated_conjecture,
( ssSkP9(X0)
| c3_2(X0,a889) ) ).
cnf(u5513,negated_conjecture,
( c5_2(X0,X1)
| c3_2(X0,X1)
| c1_2(X0,X1)
| c3_2(X0,a871)
| c3_2(X0,a866)
| c1_2(X0,a872)
| c2_2(X0,a872) ) ).
cnf(u4816,negated_conjecture,
c2_2(a800,a784) ).
cnf(u5773,negated_conjecture,
( ~ c2_2(X0,X1)
| c1_2(X0,a834)
| c3_2(X0,a871)
| c3_2(X0,a866)
| c1_2(X0,a872)
| c2_2(X0,a872)
| c1_2(X0,X1)
| c3_2(X0,a834)
| ~ c3_2(X0,X1)
| c1_2(X0,a833) ) ).
cnf(u3758,negated_conjecture,
~ c5_1(a796) ).
cnf(clause173,negated_conjecture,
( ~ c5_2(X0,a833)
| ssSkP3(X0) ) ).
cnf(u2376,negated_conjecture,
( ~ ssSkP3(X0)
| c1_2(X0,X1)
| ~ c5_2(X0,a834)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(clause126,negated_conjecture,
( ssSkP0(X0)
| c5_2(X0,a787) ) ).
cnf(u2603,negated_conjecture,
( ~ c2_2(X0,a834)
| c1_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1)
| c3_2(X0,a833) ) ).
cnf(clause112,negated_conjecture,
( ssSkP4(X0)
| c3_2(X0,a847) ) ).
cnf(clause119,negated_conjecture,
( ssSkP1(X0)
| c2_2(X0,a806) ) ).
cnf(u2592,negated_conjecture,
( ~ c5_2(X0,a834)
| c1_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1)
| c1_2(X0,a833) ) ).
cnf(clause106,negated_conjecture,
( ssSkP6(X0)
| c3_2(X0,a876) ) ).
cnf(u2170,negated_conjecture,
c4_2(a894,a805) ).
cnf(u2770,negated_conjecture,
( ~ c4_2(X0,X1)
| c3_2(X0,X2)
| ~ c1_2(X0,a832)
| c5_2(X0,X1)
| ~ c5_2(X0,X2)
| ~ c2_2(X0,X2) ) ).
cnf(clause105,negated_conjecture,
( ssSkP6(X0)
| c5_2(X0,a876) ) ).
cnf(u4663,negated_conjecture,
( ~ c2_2(X0,a866)
| c1_2(X0,X1)
| c3_2(X0,X1)
| c5_2(X0,X1)
| c3_2(X0,a871)
| c1_2(X0,X2)
| c2_2(X0,X2)
| ~ c3_2(X0,X2)
| c2_2(X0,a872) ) ).
cnf(clause108,negated_conjecture,
( ssSkP5(X0)
| c5_2(X0,a871) ) ).
cnf(u2967,negated_conjecture,
c3_2(a830,a871) ).
cnf(u2176,negated_conjecture,
( ~ c3_1(X1)
| ~ c2_2(X1,X2)
| ~ c5_2(X1,a803)
| ~ c3_2(X1,X2)
| ~ c4_2(X1,X2) ) ).
cnf(clause102,negated_conjecture,
( ssSkP8(X0)
| c1_2(X0,a883) ) ).
cnf(clause60,negated_conjecture,
( ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(clause53,negated_conjecture,
( ssSkP3(X0)
| ndr1_1(X0) ) ).
cnf(u2968,negated_conjecture,
( c5_1(X0)
| c2_2(X0,a872)
| c1_2(X0,X1)
| c3_2(X0,X1)
| c5_2(X0,X1)
| c3_2(X0,a871) ) ).
cnf(clause40,negated_conjecture,
( ssSkP9(X0)
| ndr1_1(X0) ) ).
cnf(u2111,negated_conjecture,
( c5_2(X0,a871)
| c3_2(X0,a872) ) ).
cnf(u2997,negated_conjecture,
c5_2(a853,a854) ).
cnf(u4355,negated_conjecture,
( c4_2(a800,X0)
| c1_2(a800,X0)
| c2_2(a800,X0) ) ).
cnf(u3343,negated_conjecture,
c4_2(a839,a832) ).
cnf(u3387,negated_conjecture,
c4_2(a894,a895) ).
cnf(u2374,negated_conjecture,
( ~ c3_1(X0)
| c5_2(X0,X2)
| c3_2(X0,X2)
| ~ c1_1(X0)
| c4_2(X0,X2) ) ).
cnf(u4797,negated_conjecture,
~ c1_2(a894,a784) ).
cnf(u4065,negated_conjecture,
~ c1_2(a800,a886) ).
cnf(u5086,negated_conjecture,
c2_2(a800,a803) ).
cnf(clause182,negated_conjecture,
( ~ c4_2(X0,a787)
| ssSkP0(X0) ) ).
cnf(u2404,negated_conjecture,
( ~ c2_1(X0)
| c3_2(X0,a809)
| c1_1(X0) ) ).
cnf(clause162,negated_conjecture,
( ~ c4_2(X0,a889)
| ssSkP9(X0) ) ).
cnf(clause164,negated_conjecture,
( ~ c2_2(X0,a883)
| ssSkP8(X0) ) ).
cnf(clause120,negated_conjecture,
( ssSkP1(X0)
| c4_2(X0,a806) ) ).
cnf(u2810,negated_conjecture,
( ~ c4_2(X0,X1)
| c3_2(X0,X2)
| ~ c2_2(X0,a832)
| c5_2(X0,X1)
| ~ c5_2(X0,X2)
| ~ c2_2(X0,X2) ) ).
cnf(u3884,negated_conjecture,
c2_2(a830,a809) ).
cnf(u5774,negated_conjecture,
( ~ c2_2(X0,X1)
| c1_2(X0,a834)
| c3_2(X0,a871)
| c3_2(X0,a866)
| c1_2(X0,a872)
| c2_2(X0,a872)
| c1_2(X0,X1)
| c3_2(X0,a834)
| ~ c3_2(X0,X1)
| c3_2(X0,a833) ) ).
cnf(u4824,negated_conjecture,
c3_2(a800,a784) ).
cnf(u2256,negated_conjecture,
ssSkP0(a863) ).
cnf(u2416,negated_conjecture,
( ~ c2_2(X0,a811)
| c1_1(X0) ) ).
cnf(u5142,negated_conjecture,
c2_2(a855,a809) ).
cnf(u5087,negated_conjecture,
c1_2(a830,a803) ).
cnf(u3742,negated_conjecture,
c4_2(a796,a886) ).
cnf(u2663,negated_conjecture,
( ~ c2_2(X0,a826)
| c4_2(X0,X1)
| c5_2(X0,X1)
| c1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u2412,negated_conjecture,
c1_1(a779) ).
cnf(u2529,negated_conjecture,
c1_1(a875) ).
cnf(clause116,negated_conjecture,
( ssSkP3(X0)
| c3_2(X0,a833) ) ).
cnf(u2532,negated_conjecture,
c4_2(a800,a805) ).
cnf(u2108,negated_conjecture,
( ~ c5_2(X0,a872)
| c5_2(X0,a871) ) ).
cnf(clause107,negated_conjecture,
( ssSkP5(X0)
| c3_2(X0,a871) ) ).
cnf(u5894,negated_conjecture,
c5_2(a855,a886) ).
cnf(u2587,negated_conjecture,
( ~ c4_2(X0,X1)
| ~ c5_2(X0,a803)
| ~ c3_2(X0,X1)
| ~ c2_2(X0,X1)
| c1_1(X0) ) ).
cnf(clause103,negated_conjecture,
( ssSkP8(X0)
| c3_2(X0,a883) ) ).
cnf(clause115,negated_conjecture,
( ssSkP3(X0)
| c1_2(X0,a833) ) ).
cnf(clause59,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(u4744,negated_conjecture,
c1_1(a812) ).
cnf(u2106,negated_conjecture,
( ~ c4_2(X0,a872)
| c3_2(X0,a871) ) ).
cnf(u5769,negated_conjecture,
( ssSkP7(X0)
| c1_2(X0,a881)
| c3_2(X0,a871)
| c3_2(X0,a866)
| c1_2(X0,a872)
| c2_2(X0,a872)
| c3_2(X0,a881) ) ).
cnf(clause44,negated_conjecture,
( ssSkP7(X0)
| ndr1_1(X0) ) ).
cnf(clause66,negated_conjecture,
( ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(u2702,negated_conjecture,
( ~ c2_2(X0,X1)
| c5_2(X0,a826)
| c4_2(X0,X1)
| c5_2(X0,X1)
| c1_1(X0) ) ).
cnf(u2377,negated_conjecture,
( ~ ssSkP3(X0)
| c1_2(X0,X1)
| ~ c2_2(X0,a834)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u4795,negated_conjecture,
~ c1_2(a800,a784) ).
cnf(u5895,negated_conjecture,
c4_2(a855,a886) ).
cnf(u4818,negated_conjecture,
c2_2(a894,a784) ).
cnf(u3741,negated_conjecture,
c5_2(a796,a886) ).
cnf(u5313,negated_conjecture,
c3_2(a800,a871) ).
cnf(u2667,negated_conjecture,
( ~ c1_2(X0,a826)
| c4_2(X0,X1)
| c5_2(X0,X1)
| c1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u2112,negated_conjecture,
( c3_2(X0,a872)
| c3_2(X0,a871) ) ).
cnf(u2105,negated_conjecture,
( ~ c4_2(X0,a872)
| c5_2(X0,a871) ) ).
cnf(clause183,negated_conjecture,
( ~ c3_2(X0,a787)
| ssSkP0(X0) ) ).
cnf(clause170,negated_conjecture,
( ~ c4_2(X0,a847)
| ssSkP4(X0) ) ).
cnf(clause166,negated_conjecture,
( ~ c2_2(X0,a876)
| ssSkP6(X0) ) ).
cnf(clause165,negated_conjecture,
( ~ c5_2(X0,a881)
| ssSkP7(X0) ) ).
cnf(clause118,negated_conjecture,
( ssSkP1(X0)
| c5_2(X0,a806) ) ).
cnf(u3002,negated_conjecture,
c3_2(a800,a833) ).
cnf(u4664,negated_conjecture,
( ~ c3_2(X0,X2)
| c1_2(X0,X1)
| c3_2(X0,X1)
| c5_2(X0,X1)
| c3_2(X0,a871)
| c3_2(X0,a866)
| c1_2(X0,X2)
| c2_2(X0,X2)
| c2_2(X0,a872) ) ).
cnf(clause104,negated_conjecture,
( ssSkP7(X0)
| c2_2(X0,a881) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN513-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n003.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 16:22:58 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.31 % (1732691)Will run a generic schedule for satisfiability detection.
% 0.21/0.31 % (1732701)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2819397626:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.21/0.31 % (1732697)% WARNING: option uhcvi not known.
% 0.21/0.31 % (1732696)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1411925142_2999 on theBenchmark for (2999ds/0Mi)
% 0.21/0.31 % (1732697)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2576118680:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.21/0.31 % (1732698)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=480681993:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.21/0.31 % (1732699)dis+10_1_sil=32000:sp=arity:random_seed=484066899:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.21/0.31 % (1732700)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4008180713:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.21/0.31 % (1732702)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3765580744:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.21/0.31 % Detected minimum model sizes of [1]
% 0.21/0.31 % Detected maximum model sizes of [118]
% 0.21/0.31 % TRYING [1]
% 0.21/0.31 % TRYING [2]
% 0.21/0.31 % TRYING [3]
% 0.21/0.31 % (1732702) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1732691-1732702"...
% 0.21/0.31 % (1732701) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1732691-1732701"...
% 0.21/0.31 % Finite Model Found!
% 0.21/0.31 % SZS status Satisfiable for theBenchmark
% 0.21/0.31 % (1732696) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1732691-1732696"...
% 0.21/0.31 % (1732701)...printing done.
% 0.21/0.31 % (1732696)...printing done.
% 0.21/0.31 % (1732702)...printing done.
% 0.21/0.31 % SZS status Satisfiable for theBenchmark
% 0.21/0.31 % SZS output start Saturation.
% See solution above
% 0.21/0.32 % SZS output start Definitions and Model Updates.
% 0.21/0.32 % SZS output end Definitions and Model Updates.
% 0.21/0.32 % (1732701)------------------------------
% 0.21/0.32 % (1732701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.32 % (1732701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.32 % (1732701)CaDiCaL version: 2.1.3
% 0.21/0.32 % (1732701)Termination reason: Satisfiable
% 0.21/0.32 % (1732701)Time elapsed: 0.039 s
% 0.21/0.32 % (1732701)Peak memory usage: 14 MB
% 0.21/0.32 % (1732701)Instructions burned: 114 (million)
% 0.21/0.32 % (1732691)Success in time 0.08 s
% 0.21/0.32 % Vampire exiting
%------------------------------------------------------------------------------