%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN513-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:00:46 PM UTC 2026
% Result : Satisfiable 2.98s 1.11s
% Output : Saturation 3.67s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u395,negated_conjecture,
~ c4_0 ).
cnf(u1718,negated_conjecture,
ndr1_0 ).
cnf(u513,negated_conjecture,
~ c2_0 ).
cnf(u417,negated_conjecture,
( c1_2(a827,X3)
| c5_2(a827,X3)
| ~ c2_2(a827,X3) ) ).
cnf(u427,negated_conjecture,
( ~ c5_1(X0)
| c3_2(X0,X2)
| ~ c5_2(X0,X1)
| ~ c4_2(X0,X2)
| ~ c5_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u1196,negated_conjecture,
ssSkC2 ).
cnf(u449,negated_conjecture,
( ~ c4_1(X0)
| c2_1(X0) ) ).
cnf(u814,negated_conjecture,
ssSkC6 ).
cnf(u460,negated_conjecture,
~ c5_1(a827) ).
cnf(u472,negated_conjecture,
( ~ c1_2(X0,a832)
| c5_2(X0,X2)
| c3_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c4_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u1657,negated_conjecture,
ssSkC13 ).
cnf(u479,negated_conjecture,
( c3_2(X0,X1)
| c5_2(X0,X2)
| ~ c5_2(X0,X1)
| ~ c2_2(X0,a832)
| ~ c4_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u676,negated_conjecture,
~ c3_0 ).
cnf(u489,negated_conjecture,
( ~ c1_1(X0)
| c4_2(X0,X2)
| c5_2(X0,X2)
| c3_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c3_1(X0) ) ).
cnf(u616,negated_conjecture,
~ c1_0 ).
cnf(u504,negated_conjecture,
( ~ c4_1(X1)
| c3_1(X1)
| c4_2(X1,X2)
| c1_2(X1,X2)
| ~ c5_2(X1,X2)
| ~ ndr1_1(X1) ) ).
cnf(u530,negated_conjecture,
( c4_1(X0)
| c1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u545,negated_conjecture,
( ~ c3_1(X0)
| c3_2(X0,X1)
| c4_2(X0,X1)
| c2_2(X0,X2)
| c3_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u557,negated_conjecture,
( ~ c2_2(X0,X1)
| c3_2(X0,a832)
| c5_2(X0,X2)
| c3_2(X0,X1)
| ~ c4_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u571,negated_conjecture,
( c5_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) ) ).
cnf(u584,negated_conjecture,
( c5_1(X0)
| ~ ndr1_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(u606,negated_conjecture,
( ~ c5_1(X0)
| c2_1(X0)
| ~ c1_1(X0) ) ).
cnf(u681,negated_conjecture,
c5_0 ).
cnf(u634,negated_conjecture,
( c1_1(X0)
| ~ c2_2(X0,X1)
| c4_2(X0,X1)
| c5_2(X0,X1)
| ~ c2_2(X0,a826)
| ~ ndr1_1(X0) ) ).
cnf(u1041,negated_conjecture,
ssSkC12 ).
cnf(u641,negated_conjecture,
( c1_1(X0)
| ~ c2_2(X0,X1)
| c4_2(X0,X1)
| c5_2(X0,X1)
| ~ c1_2(X0,a826)
| ~ ndr1_1(X0) ) ).
cnf(u654,negated_conjecture,
( ~ c4_1(X0)
| c2_1(X0)
| c3_1(X0) ) ).
cnf(u658,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(u662,negated_conjecture,
( c1_1(X0)
| ~ c2_2(X0,X1)
| c5_2(X0,a826)
| c4_2(X0,X1)
| c5_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u666,negated_conjecture,
( ~ ssSkP3(X0)
| c1_2(X0,X1)
| ~ c5_2(X0,a834)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u670,negated_conjecture,
( ~ ssSkP3(X0)
| c1_2(X0,X1)
| ~ c2_2(X0,a834)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u674,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(u679,negated_conjecture,
( c5_1(X0)
| ~ ndr1_1(X0)
| c3_2(X0,X1)
| c5_2(X0,X1)
| c1_2(X0,X1)
| ~ c2_1(X0) ) ).
cnf(u1081,negated_conjecture,
ssSkC0 ).
cnf(u714,negated_conjecture,
( ~ c1_2(a824,X1)
| ~ c4_2(a824,X1) ) ).
cnf(u728,negated_conjecture,
( c1_2(a795,X0)
| ~ c2_2(a795,X0)
| ~ c5_2(a795,X0) ) ).
cnf(u1453,negated_conjecture,
ssSkC5 ).
cnf(u745,negated_conjecture,
( c1_2(a852,X0)
| ~ c4_2(a852,X0)
| ~ c5_2(a852,X0) ) ).
cnf(u1487,negated_conjecture,
ssSkC16 ).
cnf(u1425,negated_conjecture,
ndr1_1(a867) ).
cnf(u755,negated_conjecture,
( ~ c4_2(a867,X0)
| c3_2(a867,X0)
| c5_2(a867,X0) ) ).
cnf(u769,negated_conjecture,
( ~ c1_2(a891,X0)
| ~ c4_2(a891,X0)
| ~ c5_2(a891,X0) ) ).
cnf(u1155,negated_conjecture,
ssSkC20 ).
cnf(u1500,negated_conjecture,
ssSkC19 ).
cnf(u779,negated_conjecture,
ssSkC17 ).
cnf(u801,negated_conjecture,
( ~ c1_2(a795,X0)
| c3_2(a795,X0)
| c5_2(a795,X0) ) ).
cnf(u808,negated_conjecture,
( ~ c1_2(a800,X0)
| ~ c5_2(a800,X0)
| ~ c4_2(a800,X0) ) ).
cnf(u824,negated_conjecture,
( ~ c2_2(X0,X1)
| c5_2(X0,a886)
| c5_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u828,negated_conjecture,
( ~ c2_2(X0,X1)
| c4_2(X0,a886)
| c5_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u843,negated_conjecture,
( ~ c1_2(a830,X0)
| c2_2(a830,X0)
| ~ c3_2(a830,X0) ) ).
cnf(u1478,negated_conjecture,
ssSkC14 ).
cnf(u1754,negated_conjecture,
ndr1_1(a853) ).
cnf(u860,negated_conjecture,
( ~ c1_2(a853,X0)
| c5_2(a853,X0)
| c3_2(a853,X0) ) ).
cnf(u1237,negated_conjecture,
ssSkC18 ).
cnf(u923,negated_conjecture,
~ ssSkC1 ).
cnf(u881,negated_conjecture,
( ~ c1_2(a779,X0)
| c3_2(a779,X0)
| c2_2(a779,X0) ) ).
cnf(u1347,negated_conjecture,
~ ssSkC3 ).
cnf(u891,negated_conjecture,
( ~ c2_2(a786,X0)
| c4_2(a786,X0)
| c5_2(a786,X0) ) ).
cnf(u895,negated_conjecture,
( ~ c1_2(a786,X0)
| c5_2(a786,X0)
| c3_2(a786,X0) ) ).
cnf(u899,negated_conjecture,
ssSkC11 ).
cnf(u909,negated_conjecture,
ssSkC21 ).
cnf(u987,negated_conjecture,
ssSkC7 ).
cnf(u997,negated_conjecture,
( ~ c2_1(X0)
| c1_2(X0,a809)
| ~ c3_1(X0) ) ).
cnf(u1138,negated_conjecture,
ssSkC8 ).
cnf(u1004,negated_conjecture,
( ~ c2_1(X0)
| c3_2(X0,a809)
| ~ c3_1(X0) ) ).
cnf(u1008,negated_conjecture,
( ~ c2_1(X0)
| c5_2(X0,a809)
| ~ c3_1(X0) ) ).
cnf(u1723,negated_conjecture,
~ ssSkC9 ).
cnf(u1039,negated_conjecture,
( c1_1(X0)
| ~ c2_2(X0,a811)
| ~ c3_1(X0) ) ).
cnf(u1048,negated_conjecture,
( ~ c4_1(X0)
| ~ c5_2(X0,a805) ) ).
cnf(u1750,negated_conjecture,
ndr1_1(a839) ).
cnf(u1064,negated_conjecture,
( c4_2(a839,X0)
| ~ c5_2(a839,X0) ) ).
cnf(u1068,negated_conjecture,
( ~ c1_2(a853,X0)
| c2_2(a853,X0) ) ).
cnf(u1075,negated_conjecture,
( ~ c1_2(a875,X0)
| ~ c4_2(a875,X0) ) ).
cnf(u1079,negated_conjecture,
( c3_2(a891,X0)
| ~ c5_2(a891,X0) ) ).
cnf(u1438,negated_conjecture,
~ ssSkC22 ).
cnf(u1097,negated_conjecture,
( c4_2(a893,X0)
| ~ c5_2(a893,X0) ) ).
cnf(u1101,negated_conjecture,
( ~ c4_1(X0)
| c3_1(X0)
| ~ c5_1(X0) ) ).
cnf(u1109,negated_conjecture,
( ~ c2_1(X0)
| ndr1_1(X0)
| ~ c3_1(X0) ) ).
cnf(u1133,negated_conjecture,
ssSkC4 ).
cnf(u1145,negated_conjecture,
( c1_1(X0)
| ~ c3_1(X0)
| c3_2(X0,a811) ) ).
cnf(u1170,negated_conjecture,
( ~ c4_1(X0)
| c4_2(X0,a805) ) ).
cnf(u1174,negated_conjecture,
( ~ c4_1(X0)
| c2_2(X0,a805) ) ).
cnf(u1178,negated_conjecture,
~ c4_1(a824) ).
cnf(u1182,negated_conjecture,
~ c2_1(a824) ).
cnf(u1190,negated_conjecture,
( ~ ssSkP5(X0)
| ~ c4_2(X0,a872) ) ).
cnf(u1194,negated_conjecture,
( ~ ssSkP5(X0)
| ~ c5_2(X0,a872) ) ).
cnf(u1203,negated_conjecture,
( c1_2(a893,X0)
| c4_2(a893,X0) ) ).
cnf(u1207,negated_conjecture,
( ~ c4_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ) ).
cnf(u1231,negated_conjecture,
( ~ c3_1(X0)
| c1_1(X0)
| ndr1_1(X0) ) ).
cnf(u1256,negated_conjecture,
( c2_2(a800,X0)
| c5_2(a800,X0) ) ).
cnf(u1260,negated_conjecture,
( ~ c4_1(X0)
| ndr1_1(X0) ) ).
cnf(u1264,negated_conjecture,
( c1_2(a830,X0)
| c5_2(a830,X0) ) ).
cnf(u1272,negated_conjecture,
( ~ ssSkP5(X0)
| c3_2(X0,a872) ) ).
cnf(u1300,negated_conjecture,
( ~ c4_1(X0)
| ~ c5_1(X0) ) ).
cnf(u1304,negated_conjecture,
~ c3_2(a867,a868) ).
cnf(u1308,negated_conjecture,
~ c4_2(a867,a869) ).
cnf(u1312,negated_conjecture,
( ~ ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(u1321,negated_conjecture,
c5_2(a867,a868) ).
cnf(u1325,negated_conjecture,
c3_2(a867,a869) ).
cnf(u1341,negated_conjecture,
( c1_1(X0)
| c3_1(X0) ) ).
cnf(u1359,negated_conjecture,
~ c5_2(a820,a821) ).
cnf(u1808,negated_conjecture,
ssSkC10 ).
cnf(u1367,negated_conjecture,
~ c3_2(a820,a821) ).
cnf(u1371,negated_conjecture,
~ c2_2(a820,a822) ).
cnf(u1375,negated_conjecture,
~ c5_2(a820,a822) ).
cnf(u1379,negated_conjecture,
~ c5_2(a839,a840) ).
cnf(u1383,negated_conjecture,
~ c4_2(a839,a841) ).
cnf(u1387,negated_conjecture,
~ c2_2(a839,a841) ).
cnf(u1391,negated_conjecture,
~ c1_1(a843) ).
cnf(u1541,negated_conjecture,
c1_2(a820,a821) ).
cnf(u1553,negated_conjecture,
c2_2(a839,a840) ).
cnf(u1557,negated_conjecture,
c4_2(a839,a840) ).
cnf(u1561,negated_conjecture,
c5_1(a843) ).
cnf(u1565,negated_conjecture,
c1_1(a852) ).
cnf(u1569,negated_conjecture,
c2_2(a853,a854) ).
cnf(u1573,negated_conjecture,
c3_2(a853,a854) ).
cnf(u1577,negated_conjecture,
~ c1_2(a858,a859) ).
cnf(u1611,negated_conjecture,
~ c3_1(a891) ).
cnf(u1631,negated_conjecture,
~ c3_1(a779) ).
cnf(u1635,negated_conjecture,
~ c4_1(a786) ).
cnf(u1669,negated_conjecture,
~ c3_1(a844) ).
cnf(u1697,negated_conjecture,
~ c5_1(a893) ).
cnf(u1747,negated_conjecture,
ndr1_1(a820) ).
cnf(u1758,negated_conjecture,
c2_2(a858,a859) ).
cnf(u1762,negated_conjecture,
c3_2(a858,a859) ).
cnf(u1778,negated_conjecture,
~ c4_1(a875) ).
cnf(u1866,negated_conjecture,
c2_1(a800) ).
cnf(u1875,negated_conjecture,
c2_1(a830) ).
cnf(u1881,negated_conjecture,
c5_1(a858) ).
cnf(u1885,negated_conjecture,
ndr1_1(a858) ).
cnf(u1890,negated_conjecture,
c2_1(a875) ).
cnf(u1948,negated_conjecture,
~ c2_1(a786) ).
cnf(u1958,negated_conjecture,
~ c3_1(a830) ).
cnf(u1965,negated_conjecture,
~ c3_1(a800) ).
cnf(u1993,negated_conjecture,
~ c2_2(a843,a811) ).
cnf(u2882,negated_conjecture,
c3_1(a795) ).
cnf(u2000,negated_conjecture,
~ c2_2(a795,a811) ).
cnf(u2687,negated_conjecture,
~ c3_2(a795,a811) ).
cnf(u2018,negated_conjecture,
~ c2_1(a843) ).
cnf(u2151,negated_conjecture,
c2_1(a858) ).
cnf(u2039,negated_conjecture,
c1_1(a858) ).
cnf(u2159,negated_conjecture,
~ c3_1(a858) ).
cnf(u2061,negated_conjecture,
c5_2(a839,a886) ).
cnf(u2065,negated_conjecture,
c5_2(a853,a854) ).
cnf(u2072,negated_conjecture,
c5_2(a800,X0) ).
cnf(u2080,negated_conjecture,
c5_2(a858,a859) ).
cnf(u2098,negated_conjecture,
c1_1(a875) ).
cnf(u2105,negated_conjecture,
~ c3_1(a875) ).
cnf(u2129,negated_conjecture,
~ c3_1(a893) ).
cnf(u2132,negated_conjecture,
~ c2_1(a893) ).
cnf(u2139,negated_conjecture,
~ c2_1(a827) ).
cnf(u2145,negated_conjecture,
c3_2(a843,a811) ).
cnf(u2191,negated_conjecture,
c4_2(a839,a886) ).
cnf(u2218,negated_conjecture,
~ c3_1(a852) ).
cnf(u2245,negated_conjecture,
~ c2_2(a843,a826) ).
cnf(u2257,negated_conjecture,
~ c1_2(a843,a826) ).
cnf(u2266,negated_conjecture,
~ c2_2(a858,a866) ).
cnf(u2269,negated_conjecture,
( c1_2(a858,X0)
| ~ c3_2(a858,X0)
| c2_2(a858,X0) ) ).
cnf(u2273,negated_conjecture,
~ c2_2(a843,a866) ).
cnf(u2276,negated_conjecture,
( c1_2(a843,X0)
| ~ c3_2(a843,X0)
| c2_2(a843,X0) ) ).
cnf(u2283,negated_conjecture,
c5_2(a843,a826) ).
cnf(u2638,negated_conjecture,
~ c3_2(a843,a866) ).
cnf(u2308,negated_conjecture,
( ~ c4_2(a858,X0)
| ~ c5_2(a858,X0)
| c3_2(a858,X0) ) ).
cnf(u2312,negated_conjecture,
( ~ c1_2(a843,X1)
| ~ c5_2(a843,X1) ) ).
cnf(u2323,negated_conjecture,
( c4_2(a843,X0)
| ~ c5_2(a843,X0)
| c3_2(a843,X0) ) ).
cnf(u2332,negated_conjecture,
~ c2_2(a827,a832) ).
cnf(u2345,negated_conjecture,
~ c5_2(a795,a832) ).
cnf(u2361,negated_conjecture,
~ c4_2(a852,a832) ).
cnf(u2371,negated_conjecture,
c4_2(a893,a832) ).
cnf(u2381,negated_conjecture,
c5_2(a830,a832) ).
cnf(u2393,negated_conjecture,
~ c2_2(a867,a868) ).
cnf(u2418,negated_conjecture,
( c2_2(a893,X0)
| ~ c3_2(a893,X0)
| c5_2(a893,X0) ) ).
cnf(u2425,negated_conjecture,
( c2_2(a827,X0)
| ~ c3_2(a827,X0)
| c5_2(a827,X0) ) ).
cnf(u2441,negated_conjecture,
c5_2(a830,a886) ).
cnf(u2448,negated_conjecture,
c4_2(a830,a886) ).
cnf(u2488,negated_conjecture,
~ c2_2(a858,a832) ).
cnf(u2463,negated_conjecture,
~ c3_2(a858,a832) ).
cnf(u2495,negated_conjecture,
~ c2_2(a843,a832) ).
cnf(u2479,negated_conjecture,
~ c3_2(a843,a832) ).
cnf(u2484,negated_conjecture,
~ c3_2(a843,a826) ).
cnf(u2491,negated_conjecture,
~ c5_2(a858,a832) ).
cnf(u2507,negated_conjecture,
c5_2(a893,a886) ).
cnf(u2514,negated_conjecture,
c4_2(a893,a886) ).
cnf(u2528,negated_conjecture,
( ~ c3_2(a827,X0)
| c5_2(a827,X0) ) ).
cnf(u2536,negated_conjecture,
~ c3_2(a827,a832) ).
cnf(u2600,negated_conjecture,
( c1_2(a852,X1)
| c5_2(a852,X1)
| c3_2(a852,X1) ) ).
cnf(u2618,negated_conjecture,
( c1_2(a875,X1)
| c3_2(a875,X1)
| c5_2(a875,X1) ) ).
cnf(u2621,negated_conjecture,
~ c2_2(a875,a866) ).
cnf(u2642,negated_conjecture,
~ c5_2(a843,a811) ).
cnf(u2686,negated_conjecture,
~ c2_2(a795,a866) ).
cnf(u2700,negated_conjecture,
~ c2_2(a786,a866) ).
cnf(u2713,negated_conjecture,
~ c2_2(a820,a866) ).
cnf(u2716,negated_conjecture,
~ c3_2(a820,a822) ).
cnf(u2733,negated_conjecture,
~ c3_2(a839,a841) ).
cnf(u2766,negated_conjecture,
c1_2(a843,a811) ).
cnf(u2776,negated_conjecture,
c3_2(a786,a866) ).
cnf(u2799,negated_conjecture,
~ c5_2(a795,a811) ).
cnf(u2809,negated_conjecture,
~ c4_2(a867,a868) ).
cnf(u2953,negated_conjecture,
~ c3_1(a824) ).
cnf(u2877,negated_conjecture,
( c1_2(a824,X1)
| c5_2(a824,X1)
| c3_2(a824,X1) ) ).
cnf(u2886,negated_conjecture,
c3_1(a786) ).
cnf(u2958,negated_conjecture,
~ c2_2(a786,a811) ).
cnf(u2971,negated_conjecture,
( c4_2(a795,X0)
| ~ c5_2(a795,X0)
| c3_2(a795,X0) ) ).
cnf(u2975,negated_conjecture,
( c4_2(a795,X0)
| c5_2(a795,X0)
| c3_2(a795,X0) ) ).
cnf(u3022,negated_conjecture,
c3_2(a786,a811) ).
cnf(u3032,negated_conjecture,
( c2_2(a786,X1)
| c3_2(a786,X1) ) ).
cnf(u3039,negated_conjecture,
( c5_2(a786,X0)
| c4_2(a786,X0)
| c3_2(a786,X0) ) ).
cnf(u3126,negated_conjecture,
~ c3_2(a795,a832) ).
cnf(u3183,negated_conjecture,
c5_2(a827,a871) ).
cnf(u3212,negated_conjecture,
( c3_2(a786,X0)
| c5_2(a786,X0) ) ).
cnf(u3220,negated_conjecture,
( ~ c4_2(a786,X1)
| c5_2(a786,X1) ) ).
cnf(u3257,negated_conjecture,
c5_2(a795,a809) ).
cnf(u3264,negated_conjecture,
c3_2(a795,a809) ).
cnf(u3271,negated_conjecture,
c1_2(a795,a809) ).
cnf(u3324,negated_conjecture,
~ c2_2(a824,a834) ).
cnf(u3334,negated_conjecture,
~ c2_2(a843,a834) ).
cnf(u3344,negated_conjecture,
~ c2_2(a891,a834) ).
cnf(u3351,negated_conjecture,
( ~ c2_2(a800,X0)
| ~ c4_2(a800,X0)
| ~ c5_2(a800,X0)
| ~ c3_2(a800,X0) ) ).
cnf(u3354,negated_conjecture,
~ c2_2(a800,a834) ).
cnf(u3357,negated_conjecture,
c1_2(a800,a833) ).
cnf(u3363,negated_conjecture,
~ c2_2(a858,a834) ).
cnf(u3373,negated_conjecture,
~ c2_2(a875,a834) ).
cnf(u3396,negated_conjecture,
~ c5_2(a824,a834) ).
cnf(u3400,negated_conjecture,
~ c5_2(a843,a834) ).
cnf(u3404,negated_conjecture,
~ c5_2(a891,a834) ).
cnf(u3412,negated_conjecture,
~ c5_2(a858,a834) ).
cnf(u3416,negated_conjecture,
~ c5_2(a875,a834) ).
cnf(u3425,negated_conjecture,
~ c3_2(a843,a834) ).
cnf(u3438,negated_conjecture,
~ c3_2(a891,a834) ).
cnf(u3460,negated_conjecture,
~ c3_2(a858,a834) ).
cnf(u3533,negated_conjecture,
c3_2(a800,a833) ).
cnf(u3546,negated_conjecture,
~ c4_2(a800,a833) ).
cnf(u2263,negated_conjecture,
( ~ c2_1(X0)
| c2_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c2_2(X0,a866)
| ~ ndr1_1(X0)
| c3_2(X0,X2)
| c5_2(X0,X2)
| c1_2(X0,X2)
| c1_2(X0,X1) ) ).
cnf(u3065,negated_conjecture,
( ~ c3_1(X0)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X3)
| c4_2(X0,X3)
| c5_2(X0,X3)
| ~ c1_2(X0,a826)
| c1_2(X0,a809)
| c5_2(X0,X1) ) ).
cnf(u2215,negated_conjecture,
( ~ c3_1(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ ndr1_1(X0)
| c4_2(X0,X1)
| c3_2(X0,a811) ) ).
cnf(u2280,negated_conjecture,
( ~ c3_1(X0)
| c5_2(X0,a826)
| c4_2(X0,X1)
| c5_2(X0,X1)
| ~ ndr1_1(X0)
| c4_2(X0,X2)
| c5_2(X0,X2)
| c3_2(X0,X2)
| ~ c2_2(X0,X1) ) ).
cnf(clause166,negated_conjecture,
( ssSkP6(X0)
| ~ c2_2(X0,a876) ) ).
cnf(u2239,negated_conjecture,
( ~ c3_1(X0)
| c4_2(X0,X1)
| c5_2(X0,X1)
| ~ c2_2(X0,a826)
| ~ ndr1_1(X0)
| c4_2(X0,X2)
| c5_2(X0,X2)
| c3_2(X0,X2)
| ~ c2_2(X0,X1) ) ).
cnf(clause49,negated_conjecture,
( ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(u2583,negated_conjecture,
( c2_1(X0)
| c5_2(X0,X1)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,a811)
| ~ c3_1(X0) ) ).
cnf(clause40,negated_conjecture,
( ssSkP9(X0)
| ndr1_1(X0) ) ).
cnf(u3302,negated_conjecture,
( c1_2(X0,X1)
| c1_2(X0,a833)
| ~ c5_2(X0,a834)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u3066,negated_conjecture,
( ~ c3_1(X0)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X3)
| c4_2(X0,X3)
| c5_2(X0,X3)
| ~ c1_2(X0,a826)
| c3_2(X0,a809)
| c5_2(X0,X1) ) ).
cnf(u2044,negated_conjecture,
( c2_2(a830,X0)
| ~ c3_2(a830,X0)
| c5_2(a830,X0) ) ).
cnf(u3092,negated_conjecture,
( ~ c3_1(X0)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X3)
| c4_2(X0,X3)
| c5_2(X0,X3)
| ~ c2_2(X0,a826)
| c5_2(X0,a809)
| c5_2(X0,X1) ) ).
cnf(u3091,negated_conjecture,
( ~ c3_1(X0)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X3)
| c4_2(X0,X3)
| c5_2(X0,X3)
| ~ c2_2(X0,a826)
| c3_2(X0,a809)
| c5_2(X0,X1) ) ).
cnf(clause103,negated_conjecture,
( ssSkP8(X0)
| c3_2(X0,a883) ) ).
cnf(clause106,negated_conjecture,
( ssSkP6(X0)
| c3_2(X0,a876) ) ).
cnf(u3016,negated_conjecture,
( ~ c3_1(X0)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| c5_2(X0,X1)
| c3_2(X0,a811)
| c3_2(X0,a809) ) ).
cnf(u3044,negated_conjecture,
( ~ c3_1(X0)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X3)
| c5_2(X0,a826)
| c4_2(X0,X3)
| c5_2(X0,X3)
| c5_2(X0,a809)
| c5_2(X0,X1) ) ).
cnf(clause44,negated_conjecture,
( ssSkP7(X0)
| ndr1_1(X0) ) ).
cnf(u3491,negated_conjecture,
( c1_2(X0,X1)
| c3_2(X0,a833)
| ~ c2_2(X0,a834)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u2414,negated_conjecture,
( c2_2(X0,X3)
| c2_2(X0,X1)
| c5_2(X0,X1)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c3_2(X0,a866)
| c1_2(X0,X3)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X3) ) ).
cnf(clause116,negated_conjecture,
( ssSkP3(X0)
| c3_2(X0,a833) ) ).
cnf(clause107,negated_conjecture,
( ssSkP5(X0)
| c3_2(X0,a871) ) ).
cnf(u2254,negated_conjecture,
( ~ c3_1(X0)
| c4_2(X0,X1)
| c5_2(X0,X1)
| ~ c1_2(X0,a826)
| ~ ndr1_1(X0)
| c4_2(X0,X2)
| c5_2(X0,X2)
| c3_2(X0,X2)
| ~ c2_2(X0,X1) ) ).
cnf(u2761,negated_conjecture,
( c5_2(X0,X3)
| c5_2(X0,X1)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c3_2(X0,a866)
| c1_2(X0,X3)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X3)
| c5_2(X0,a886)
| c2_2(X0,X1) ) ).
cnf(u3090,negated_conjecture,
( ~ c3_1(X0)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X3)
| c4_2(X0,X3)
| c5_2(X0,X3)
| ~ c2_2(X0,a826)
| c1_2(X0,a809)
| c5_2(X0,X1) ) ).
cnf(u2682,negated_conjecture,
( c5_2(X0,X3)
| c5_2(X0,X1)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c1_2(X0,X3)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X3)
| ~ c2_2(X0,a866)
| c4_2(X0,a886)
| c2_2(X0,X1) ) ).
cnf(u3042,negated_conjecture,
( ~ c3_1(X0)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X3)
| c5_2(X0,a826)
| c4_2(X0,X3)
| c5_2(X0,X3)
| c1_2(X0,a809)
| c5_2(X0,X1) ) ).
cnf(u2289,negated_conjecture,
( ~ c2_1(X0)
| c1_2(X0,X1)
| c2_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0)
| c3_2(X0,X2)
| c5_2(X0,X2)
| c1_2(X0,X2)
| c3_2(X0,a866) ) ).
cnf(clause112,negated_conjecture,
( ssSkP4(X0)
| c3_2(X0,a847) ) ).
cnf(u1941,negated_conjecture,
( c1_1(X0)
| ~ c2_1(X0)
| c2_2(X0,a805) ) ).
cnf(clause164,negated_conjecture,
( ssSkP8(X0)
| ~ c2_2(X0,a883) ) ).
cnf(u3015,negated_conjecture,
( ~ c3_1(X0)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| c5_2(X0,X1)
| c3_2(X0,a811)
| c5_2(X0,a809) ) ).
cnf(u2681,negated_conjecture,
( c5_2(X0,X3)
| c5_2(X0,X1)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c1_2(X0,X3)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X3)
| ~ c2_2(X0,a866)
| c5_2(X0,a886)
| c2_2(X0,X1) ) ).
cnf(u2762,negated_conjecture,
( c5_2(X0,X3)
| c5_2(X0,X1)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c3_2(X0,a866)
| c1_2(X0,X3)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X3)
| c4_2(X0,a886)
| c2_2(X0,X1) ) ).
cnf(clause99,negated_conjecture,
( ssSkP9(X0)
| c3_2(X0,a889) ) ).
cnf(u2301,negated_conjecture,
( ~ c2_1(X0)
| ~ c5_2(X0,X2)
| ~ c4_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X2)
| c3_2(X0,X1)
| ~ c3_1(X0) ) ).
cnf(clause177,negated_conjecture,
( ssSkP2(X0)
| ~ c3_2(X0,a807) ) ).
cnf(u2593,negated_conjecture,
( c2_1(X0)
| c5_2(X0,X1)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X3)
| c4_2(X0,X3)
| c5_2(X0,X3)
| ~ c1_2(X0,a826) ) ).
cnf(u2302,negated_conjecture,
( ~ c2_1(X0)
| ~ c5_2(X0,X2)
| ~ c4_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X2)
| c3_2(X0,X3)
| c5_2(X0,X3)
| c1_2(X0,X3)
| c3_2(X0,X1) ) ).
cnf(clause43,negated_conjecture,
( ssSkP8(X0)
| ndr1_1(X0) ) ).
cnf(u2120,negated_conjecture,
c3_1(a843) ).
cnf(u3174,negated_conjecture,
( c3_2(X0,a871)
| ~ c5_2(X0,a872) ) ).
cnf(u3175,negated_conjecture,
( ~ c4_2(X0,a872)
| c3_2(X0,a871) ) ).
cnf(u3173,negated_conjecture,
( c3_2(X0,a871)
| c3_2(X0,a872) ) ).
cnf(u2592,negated_conjecture,
( c2_1(X0)
| c5_2(X0,X1)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X3)
| c5_2(X0,a826)
| c4_2(X0,X3)
| c5_2(X0,X3) ) ).
cnf(u1942,negated_conjecture,
( c1_1(X0)
| ~ c2_1(X0)
| c4_2(X0,a805) ) ).
cnf(u2433,negated_conjecture,
( c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_1(X0)
| c3_2(X0,X1)
| c5_2(X0,X1)
| c1_2(X0,X1) ) ).
cnf(clause98,negated_conjecture,
( ssSkP9(X0)
| c2_2(X0,a889) ) ).
cnf(u3244,negated_conjecture,
( ~ c4_2(X0,a872)
| c5_2(X0,a871) ) ).
cnf(u2288,negated_conjecture,
( ~ c2_1(X0)
| c1_2(X0,X1)
| c2_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0)
| c3_2(X0,a866)
| ~ c3_1(X0) ) ).
cnf(u2415,negated_conjecture,
( c3_2(X0,X3)
| c2_2(X0,X1)
| c5_2(X0,X1)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X4)
| ~ c4_2(X0,X3)
| ~ c5_2(X0,X3)
| ~ c1_2(X0,X4) ) ).
cnf(u3017,negated_conjecture,
( ~ c3_1(X0)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| c5_2(X0,X1)
| c3_2(X0,a811)
| c1_2(X0,a809) ) ).
cnf(u2838,negated_conjecture,
( ~ c4_2(a875,X0)
| c5_2(a875,X0)
| c3_2(a875,X0) ) ).
cnf(clause183,negated_conjecture,
( ssSkP0(X0)
| ~ c3_2(X0,a787) ) ).
cnf(u2004,negated_conjecture,
( ~ c5_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u1918,negated_conjecture,
ndr1_1(X0) ).
cnf(clause119,negated_conjecture,
( ssSkP1(X0)
| c2_2(X0,a806) ) ).
cnf(clause170,negated_conjecture,
( ssSkP4(X0)
| ~ c4_2(X0,a847) ) ).
cnf(clause173,negated_conjecture,
( ssSkP3(X0)
| ~ c5_2(X0,a833) ) ).
cnf(clause104,negated_conjecture,
( ssSkP7(X0)
| c2_2(X0,a881) ) ).
cnf(u2118,negated_conjecture,
( ~ c5_1(X0)
| c1_1(X0)
| ~ c2_1(X0) ) ).
cnf(clause126,negated_conjecture,
( ssSkP0(X0)
| c5_2(X0,a787) ) ).
cnf(clause118,negated_conjecture,
( ssSkP1(X0)
| c5_2(X0,a806) ) ).
cnf(clause45,negated_conjecture,
( ssSkP6(X0)
| ndr1_1(X0) ) ).
cnf(u3043,negated_conjecture,
( ~ c3_1(X0)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X3)
| c5_2(X0,a826)
| c4_2(X0,X3)
| c5_2(X0,X3)
| c3_2(X0,a809)
| c5_2(X0,X1) ) ).
cnf(u2413,negated_conjecture,
( c2_2(X0,X3)
| c2_2(X0,X1)
| c5_2(X0,X1)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c1_2(X0,X3)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X3)
| ~ c2_2(X0,a866) ) ).
cnf(clause178,negated_conjecture,
( ssSkP2(X0)
| ~ c2_2(X0,a807) ) ).
cnf(clause165,negated_conjecture,
( ssSkP7(X0)
| ~ c5_2(X0,a881) ) ).
cnf(u2952,negated_conjecture,
( ~ c3_1(X0)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,a811)
| c5_2(X0,X1)
| c1_2(X0,a809) ) ).
cnf(u3492,negated_conjecture,
( c1_2(X0,X1)
| c3_2(X0,a833)
| ~ c5_2(X0,a834)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(clause162,negated_conjecture,
( ssSkP9(X0)
| ~ c4_2(X0,a889) ) ).
cnf(u3067,negated_conjecture,
( ~ c3_1(X0)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X3)
| c4_2(X0,X3)
| c5_2(X0,X3)
| ~ c1_2(X0,a826)
| c5_2(X0,a809)
| c5_2(X0,X1) ) ).
cnf(u2466,negated_conjecture,
( c2_2(a843,X0)
| ~ c3_2(a843,X0)
| ~ c5_2(a843,X0) ) ).
cnf(u3569,negated_conjecture,
( c1_2(X0,X1)
| ~ c5_2(X0,a833)
| ~ c5_2(X0,a834)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(clause182,negated_conjecture,
( ssSkP0(X0)
| ~ c4_2(X0,a787) ) ).
cnf(clause120,negated_conjecture,
( ssSkP1(X0)
| c4_2(X0,a806) ) ).
cnf(u2951,negated_conjecture,
( ~ c3_1(X0)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,a811)
| c5_2(X0,X1)
| c3_2(X0,a809) ) ).
cnf(u1953,negated_conjecture,
~ c5_2(a839,a841) ).
cnf(clause108,negated_conjecture,
( ssSkP5(X0)
| c5_2(X0,a871) ) ).
cnf(u2950,negated_conjecture,
( ~ c3_1(X0)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,a811)
| c5_2(X0,X1)
| c5_2(X0,a809) ) ).
cnf(u2214,negated_conjecture,
( ~ c3_1(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ ndr1_1(X0)
| c4_2(X0,X1)
| ~ c2_2(X0,a811) ) ).
cnf(u2594,negated_conjecture,
( c2_1(X0)
| c5_2(X0,X1)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X3)
| c4_2(X0,X3)
| c5_2(X0,X3)
| ~ c2_2(X0,a826) ) ).
cnf(u2584,negated_conjecture,
( c2_1(X0)
| c5_2(X0,X1)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_1(X0)
| c3_2(X0,a811) ) ).
cnf(u3229,negated_conjecture,
( ~ c4_2(a824,X0)
| c3_2(a824,X0)
| c5_2(a824,X0) ) ).
cnf(u3301,negated_conjecture,
( c1_2(X0,X1)
| c1_2(X0,a833)
| ~ c2_2(X0,a834)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(clause102,negated_conjecture,
( ssSkP8(X0)
| c1_2(X0,a883) ) ).
cnf(u2411,negated_conjecture,
( ~ c1_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)
| c2_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u2608,negated_conjecture,
( ~ c2_1(X0)
| ~ c3_1(X0)
| c4_2(X0,X1)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u3242,negated_conjecture,
( c3_2(X0,a872)
| c5_2(X0,a871) ) ).
cnf(clause115,negated_conjecture,
( ssSkP3(X0)
| c1_2(X0,a833) ) ).
cnf(clause46,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(u3243,negated_conjecture,
( c5_2(X0,a871)
| ~ c5_2(X0,a872) ) ).
cnf(u2262,negated_conjecture,
( ~ c2_1(X0)
| c2_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c2_2(X0,a866)
| ~ ndr1_1(X0)
| c1_2(X0,X1)
| ~ c3_1(X0) ) ).
cnf(u2432,negated_conjecture,
( c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) ) ).
cnf(u1943,negated_conjecture,
( c1_1(X0)
| ~ c2_1(X0)
| ~ c5_2(X0,a805) ) ).
cnf(clause105,negated_conjecture,
( ssSkP6(X0)
| c5_2(X0,a876) ) ).
cnf(u2585,negated_conjecture,
( c2_1(X0)
| c5_2(X0,X1)
| c1_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| c3_1(X0) ) ).
cnf(u3568,negated_conjecture,
( c1_2(X0,X1)
| ~ c5_2(X0,a833)
| ~ c2_2(X0,a834)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN513-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n026.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 16:23:57 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 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
% 2.98/1.11 % (3990122)Input is clausal, will run a generic CNF schedule.
% 2.98/1.11 % (3990131)lrs+10_1_sil=8000:sp=occurrence:random_seed=903398424:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 2.98/1.11 % (3990131)Instruction limit reached!
% 2.98/1.11 % (3990131)------------------------------
% 2.98/1.11 % (3990131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.98/1.11 % (3990131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.98/1.11 % (3990131)CaDiCaL version: 2.1.3
% 2.98/1.11 % (3990131)Termination reason: Instruction limit
% 2.98/1.11 % (3990131)Termination phase: Saturation
% 2.98/1.11 % (3990131)Time elapsed: 0.036 s
% 2.98/1.11 % (3990131)Peak memory usage: 91 MB
% 2.98/1.11 % (3990131)Instructions burned: 108 (million)
% 2.98/1.11 % (3990129)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3138596526:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 2.98/1.11 % (3990132)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3572314858:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 2.98/1.11 % (3990134)dis-21_1_sil=8000:lcm=predicate:random_seed=4234346302:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 2.98/1.11 % (3990128)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=3739781337:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 2.98/1.11 % (3990130)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=96290814:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 2.98/1.11 % (3990133)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1942197112:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 2.98/1.11 % (3990133)Refutation not found, incomplete strategy
% 2.98/1.11 % (3990133)------------------------------
% 2.98/1.11 % (3990133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.98/1.11 % (3990133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.98/1.11 % (3990133)CaDiCaL version: 2.1.3
% 2.98/1.11 % (3990133)Termination reason: Refutation not found, incomplete strategy
% 2.98/1.11 % (3990133)Time elapsed: 0.023 s
% 2.98/1.11 % (3990133)Peak memory usage: 90 MB
% 2.98/1.11 % (3990133)Instructions burned: 36 (million)
% 2.98/1.11 % (3990134)First to succeed.
% 2.98/1.11 % (3990134)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3990122"
% 2.98/1.11 % (3990132)Instruction limit reached!
% 2.98/1.11 % (3990132)------------------------------
% 2.98/1.11 % (3990132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.98/1.11 % (3990132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.98/1.11 % (3990132)CaDiCaL version: 2.1.3
% 2.98/1.11 % (3990132)Termination reason: Instruction limit
% 2.98/1.11 % (3990132)Termination phase: Saturation
% 2.98/1.11 % (3990132)Time elapsed: 0.066 s
% 2.98/1.11 % (3990132)Peak memory usage: 90 MB
% 2.98/1.11 % (3990132)Instructions burned: 114 (million)
% 2.98/1.11 % (3990141)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=4116334216:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 2.98/1.11 % (3990141)Instruction limit reached!
% 2.98/1.11 % (3990141)------------------------------
% 2.98/1.11 % (3990141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.98/1.11 % (3990141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.98/1.11 % (3990141)CaDiCaL version: 2.1.3
% 2.98/1.11 % (3990141)Termination reason: Instruction limit
% 2.98/1.11 % (3990141)Termination phase: Saturation
% 2.98/1.11 % (3990141)Time elapsed: 0.046 s
% 2.98/1.11 % (3990141)Peak memory usage: 91 MB
% 2.98/1.11 % (3990141)Instructions burned: 144 (million)
% 2.98/1.11 % (3990143)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=267012442:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 2.98/1.11 % (3990143)Refutation not found, incomplete strategy
% 2.98/1.11 % (3990143)------------------------------
% 2.98/1.11 % (3990143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.98/1.11 % (3990143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.98/1.11 % (3990143)CaDiCaL version: 2.1.3
% 2.98/1.11 % (3990143)Termination reason: Refutation not found, incomplete strategy
% 2.98/1.11 % (3990143)Time elapsed: 0.026 s
% 2.98/1.11 % (3990143)Peak memory usage: 89 MB
% 2.98/1.11 % (3990143)Instructions burned: 45 (million)
% 2.98/1.11 % (3990145)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2457863063:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 2.98/1.11 % (3990133)------------------------------
% 2.98/1.11 % (3990133)------------------------------
% 2.98/1.11 % (3990145)Instruction limit reached!
% 2.98/1.11 % (3990145)------------------------------
% 2.98/1.11 % (3990145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.98/1.11 % (3990145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.98/1.11 % (3990145)CaDiCaL version: 2.1.3
% 2.98/1.11 % (3990145)Termination reason: Instruction limit
% 2.98/1.11 % (3990145)Termination phase: Saturation
% 2.98/1.11 % (3990145)Time elapsed: 0.063 s
% 2.98/1.11 % (3990145)Peak memory usage: 91 MB
% 2.98/1.11 % (3990145)Instructions burned: 220 (million)
% 2.98/1.11 % SZS status Satisfiable for theBenchmark
% 2.98/1.11 % SZS output start Saturation.
% See solution above
% 3.67/1.21 % SZS output start Definitions and Model Updates.
% 3.67/1.21 % SZS output end Definitions and Model Updates.
% 3.67/1.21 % (3990134)------------------------------
% 3.67/1.21 % (3990134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.67/1.21 % (3990134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/1.21 % (3990134)CaDiCaL version: 2.1.3
% 3.67/1.21 % (3990134)Termination reason: Satisfiable
% 3.67/1.21 % (3990134)Time elapsed: 0.042 s
% 3.67/1.21 % (3990134)Peak memory usage: 90 MB
% 3.67/1.21 % (3990134)Instructions burned: 68 (million)
% 3.67/1.21 % (3990134)------------------------------
% 3.67/1.21 % (3990134)------------------------------
% 3.67/1.21 % (3990122)Success in time 0.441 s
% 3.67/1.21 % Vampire exiting
%------------------------------------------------------------------------------