%------------------------------------------------------------------------------
% 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 : n019.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 : CounterSatisfiable 4.02s 1.35s
% Output : Saturation 5.20s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u589,negated_conjecture,
ndr1_0 ).
cnf(u597,negated_conjecture,
c5_0 ).
cnf(u609,negated_conjecture,
~ sP0 ).
cnf(u613,negated_conjecture,
~ sP1 ).
cnf(u618,negated_conjecture,
~ c4_1(a892) ).
cnf(u623,negated_conjecture,
c5_1(a892) ).
cnf(u627,negated_conjecture,
ndr1_1(a892) ).
cnf(u631,negated_conjecture,
( ~ c2_2(a892,X96)
| c1_2(a892,X96)
| c3_2(a892,X96) ) ).
cnf(u640,negated_conjecture,
~ sP4 ).
cnf(u648,negated_conjecture,
sP3 ).
cnf(u664,negated_conjecture,
( ~ c2_2(X92,X93)
| c5_2(X92,a886)
| ~ ndr1_1(X92)
| c5_2(X92,X93) ) ).
cnf(u668,negated_conjecture,
( ~ c2_2(X92,X93)
| c4_2(X92,a886)
| ~ ndr1_1(X92)
| c5_2(X92,X93) ) ).
cnf(u676,negated_conjecture,
~ c3_0 ).
cnf(u681,negated_conjecture,
~ c1_0 ).
cnf(u694,negated_conjecture,
( ~ c5_2(X89,X90)
| c3_1(X89)
| ~ ndr1_1(X89)
| c4_2(X89,X90)
| c1_2(X89,X90)
| ~ c4_1(X89) ) ).
cnf(u713,negated_conjecture,
~ c4_0 ).
cnf(u717,negated_conjecture,
( ~ c3_2(X85,X86)
| c1_2(X85,X87)
| c3_2(X85,X87)
| c5_2(X85,X87)
| c5_1(X85)
| ~ ndr1_1(X85)
| c2_2(X85,X86)
| c5_2(X85,X86) ) ).
cnf(u733,negated_conjecture,
( ~ c4_1(X83)
| ~ c3_1(X83)
| c2_1(X83) ) ).
cnf(u763,negated_conjecture,
~ c2_0 ).
cnf(u768,negated_conjecture,
~ sP8 ).
cnf(u789,negated_conjecture,
ndr1_1(a875) ).
cnf(u793,negated_conjecture,
( ~ c4_2(a875,X80)
| ~ c1_2(a875,X80) ) ).
cnf(u798,negated_conjecture,
c2_1(a875) ).
cnf(u803,negated_conjecture,
~ c4_1(a875) ).
cnf(u834,negated_conjecture,
( c5_2(X79,a871)
| sP9(X79) ) ).
cnf(u838,negated_conjecture,
( c3_2(X79,a871)
| sP9(X79) ) ).
cnf(u842,negated_conjecture,
( ndr1_1(X79)
| sP9(X79) ) ).
cnf(u862,negated_conjecture,
~ sP10 ).
cnf(u868,negated_conjecture,
( ~ c2_2(X76,a866)
| ~ ndr1_1(X76)
| c1_2(X76,X77)
| c2_2(X76,X77)
| ~ c3_2(X76,X77)
| ~ c5_1(X76) ) ).
cnf(u872,negated_conjecture,
( ~ c3_2(X76,X77)
| ~ ndr1_1(X76)
| c1_2(X76,X77)
| c2_2(X76,X77)
| ~ c5_1(X76)
| c3_2(X76,a866) ) ).
cnf(u902,negated_conjecture,
( c3_1(X75)
| c2_1(X75)
| ~ c4_1(X75) ) ).
cnf(u926,negated_conjecture,
~ sP11 ).
cnf(u945,negated_conjecture,
c2_2(a858,a859) ).
cnf(u950,negated_conjecture,
c3_2(a858,a859) ).
cnf(u955,negated_conjecture,
~ c1_2(a858,a859) ).
cnf(u960,negated_conjecture,
ndr1_1(a858) ).
cnf(u965,negated_conjecture,
c5_1(a858) ).
cnf(u993,negated_conjecture,
( ~ c2_1(X69)
| ~ c3_1(X69)
| c5_1(X69) ) ).
cnf(u1018,negated_conjecture,
ndr1_1(a853) ).
cnf(u1022,negated_conjecture,
( ~ c1_2(a853,X68)
| c5_2(a853,X68)
| c3_2(a853,X68) ) ).
cnf(u1027,negated_conjecture,
c2_2(a853,a854) ).
cnf(u1032,negated_conjecture,
c3_2(a853,a854) ).
cnf(u1037,negated_conjecture,
( ~ c1_2(a853,X67)
| c2_2(a853,X67) ) ).
cnf(u1043,negated_conjecture,
c1_1(a852) ).
cnf(u1046,negated_conjecture,
~ sP12 ).
cnf(u1051,negated_conjecture,
ndr1_1(a852) ).
cnf(u1055,negated_conjecture,
( ~ c4_2(a852,X66)
| ~ c5_2(a852,X66)
| c1_2(a852,X66) ) ).
cnf(u1078,negated_conjecture,
( c4_2(X60,X61)
| ~ ndr1_1(X60)
| ~ c3_1(X60)
| c5_2(X60,X61)
| c3_2(X60,X61)
| ~ c1_1(X60) ) ).
cnf(u1132,negated_conjecture,
( c1_1(X59)
| c3_1(X59) ) ).
cnf(u1153,negated_conjecture,
sP14 ).
cnf(u1161,negated_conjecture,
~ sP15 ).
cnf(u1191,negated_conjecture,
( ~ c5_2(X54,a834)
| ~ ndr1_1(X54)
| ~ c2_2(X54,X55)
| ~ c3_2(X54,X55)
| c1_2(X54,X55)
| sP16(X54) ) ).
cnf(u1195,negated_conjecture,
( ~ c2_2(X54,a834)
| ~ ndr1_1(X54)
| ~ c2_2(X54,X55)
| ~ c3_2(X54,X55)
| c1_2(X54,X55)
| sP16(X54) ) ).
cnf(u1199,negated_conjecture,
~ sP17 ).
cnf(u1204,negated_conjecture,
~ c4_1(a831) ).
cnf(u1209,negated_conjecture,
c3_1(a831) ).
cnf(u1218,negated_conjecture,
ndr1_1(a830) ).
cnf(u1222,negated_conjecture,
( c5_2(a830,X50)
| c1_2(a830,X50) ) ).
cnf(u1226,negated_conjecture,
( ~ c1_2(a830,X49)
| ~ c3_2(a830,X49)
| c2_2(a830,X49) ) ).
cnf(u1231,negated_conjecture,
c2_1(a830) ).
cnf(u1243,negated_conjecture,
( ~ c1_1(X46)
| ~ c5_1(X46)
| c2_1(X46) ) ).
cnf(u1270,negated_conjecture,
ndr1_1(a827) ).
cnf(u1274,negated_conjecture,
( ~ c2_2(a827,X40)
| c5_2(a827,X40)
| c1_2(a827,X40) ) ).
cnf(u1279,negated_conjecture,
~ c5_1(a827) ).
cnf(u1284,negated_conjecture,
~ sP18 ).
cnf(u1288,negated_conjecture,
( c1_2(X39,a825)
| ~ c2_1(X39)
| c1_1(X39) ) ).
cnf(u1292,negated_conjecture,
( ~ c2_2(X39,a825)
| ~ c2_1(X39)
| c1_1(X39) ) ).
cnf(u1296,negated_conjecture,
( c3_2(X39,a825)
| ~ c2_1(X39)
| c1_1(X39) ) ).
cnf(u1300,negated_conjecture,
( ~ c2_1(X39)
| ndr1_1(X39)
| c1_1(X39) ) ).
cnf(u1305,negated_conjecture,
~ c4_1(a824) ).
cnf(u1312,negated_conjecture,
ndr1_1(a824) ).
cnf(u1316,negated_conjecture,
( ~ c4_2(a824,X38)
| ~ c1_2(a824,X38) ) ).
cnf(u1321,negated_conjecture,
~ c2_1(a824) ).
cnf(u1339,negated_conjecture,
~ sP19 ).
cnf(u1343,negated_conjecture,
~ sP20 ).
cnf(u1348,negated_conjecture,
c2_1(a817) ).
cnf(u1353,negated_conjecture,
c4_1(a817) ).
cnf(u1400,negated_conjecture,
( ~ c4_1(X35)
| ~ c5_1(X35) ) ).
cnf(u1404,negated_conjecture,
~ sP21 ).
cnf(u1408,negated_conjecture,
( ~ c3_1(X34)
| c3_2(X34,a811)
| c1_1(X34) ) ).
cnf(u1412,negated_conjecture,
( ~ c3_1(X34)
| ~ c2_2(X34,a811)
| c1_1(X34) ) ).
cnf(u1416,negated_conjecture,
( ~ c3_1(X34)
| ndr1_1(X34)
| c1_1(X34) ) ).
cnf(u1431,negated_conjecture,
( ~ c5_1(X33)
| ~ c4_1(X33)
| c3_1(X33) ) ).
cnf(u1435,negated_conjecture,
~ sP24 ).
cnf(u1439,negated_conjecture,
( ~ c2_2(X32,a807)
| sP22(X32)
| sP23(X32) ) ).
cnf(u1443,negated_conjecture,
( ~ c3_2(X32,a807)
| sP22(X32)
| sP23(X32) ) ).
cnf(u1447,negated_conjecture,
( sP23(X32)
| sP22(X32)
| ndr1_1(X32) ) ).
cnf(u1451,negated_conjecture,
~ sP25 ).
cnf(u1472,negated_conjecture,
( ~ c4_1(X28)
| c2_1(X28) ) ).
cnf(u1475,negated_conjecture,
~ sP26 ).
cnf(u1488,negated_conjecture,
ndr1_1(a800) ).
cnf(u1492,negated_conjecture,
( c5_2(a800,X27)
| c2_2(a800,X27) ) ).
cnf(u1496,negated_conjecture,
( ~ c4_2(a800,X26)
| ~ c5_2(a800,X26)
| ~ c1_2(a800,X26) ) ).
cnf(u1501,negated_conjecture,
c2_1(a800) ).
cnf(u1522,negated_conjecture,
~ sP27 ).
cnf(u1526,negated_conjecture,
( ~ c5_2(X22,X23)
| ~ c3_1(X22)
| c2_2(X22,X24)
| c3_2(X22,X24)
| ~ ndr1_1(X22)
| c3_2(X22,X23)
| c4_2(X22,X23) ) ).
cnf(u1535,negated_conjecture,
~ sP28 ).
cnf(u1554,negated_conjecture,
( ~ c2_1(X19)
| c1_1(X19)
| c4_1(X19) ) ).
cnf(u1573,negated_conjecture,
~ sP30 ).
cnf(u1577,negated_conjecture,
~ sP31 ).
cnf(u1582,negated_conjecture,
~ c4_1(a786) ).
cnf(u1586,negated_conjecture,
ndr1_1(a786) ).
cnf(u1590,negated_conjecture,
( ~ c2_2(a786,X14)
| c5_2(a786,X14)
| c4_2(a786,X14) ) ).
cnf(u1594,negated_conjecture,
( ~ c1_2(a786,X13)
| c5_2(a786,X13)
| c3_2(a786,X13) ) ).
cnf(u1599,negated_conjecture,
~ sP32 ).
cnf(u1606,negated_conjecture,
( ~ c4_2(X9,X10)
| ~ c1_2(X9,X11)
| ~ c5_2(X9,X11)
| ~ c5_1(X9)
| ~ ndr1_1(X9)
| ~ c5_2(X9,X10)
| c3_2(X9,X10) ) ).
cnf(u1671,negated_conjecture,
~ sP33 ).
cnf(u1675,negated_conjecture,
ndr1_1(a779) ).
cnf(u1679,negated_conjecture,
( ~ c1_2(a779,X2)
| c3_2(a779,X2)
| c2_2(a779,X2) ) ).
cnf(u1684,negated_conjecture,
~ c3_1(a779) ).
cnf(u1692,negated_conjecture,
~ sP34 ).
cnf(u1752,axiom,
ndr1_1(a893) ).
cnf(u1761,axiom,
~ c5_1(a893) ).
cnf(u1771,axiom,
c5_1(a887) ).
cnf(u1776,axiom,
c3_2(a887,a888) ).
cnf(u1781,axiom,
c1_2(a887,a888) ).
cnf(u1786,axiom,
~ c4_2(a887,a888) ).
cnf(u1791,axiom,
ndr1_1(a887) ).
cnf(u1796,axiom,
ndr1_1(a891) ).
cnf(u1805,axiom,
~ c3_1(a891) ).
cnf(u1929,axiom,
ndr1_1(a839) ).
cnf(u1933,axiom,
( ~ c5_2(a839,X0)
| c4_2(a839,X0) ) ).
cnf(u1938,axiom,
~ c4_2(a839,a841) ).
cnf(u1943,axiom,
~ c2_2(a839,a841) ).
cnf(u1949,axiom,
c2_2(a839,a840) ).
cnf(u1954,axiom,
~ c5_2(a839,a840) ).
cnf(u1959,axiom,
c4_2(a839,a840) ).
cnf(u2386,negated_conjecture,
~ c3_1(a875) ).
cnf(u2390,negated_conjecture,
~ c5_1(a830) ).
cnf(u2395,negated_conjecture,
~ c3_1(a830) ).
cnf(u2400,negated_conjecture,
~ c5_1(a800) ).
cnf(u2405,negated_conjecture,
~ c3_1(a800) ).
cnf(u2416,negated_conjecture,
~ c5_1(a852) ).
cnf(u2429,negated_conjecture,
~ c4_1(a830) ).
cnf(u2434,negated_conjecture,
c1_1(a830) ).
cnf(u2439,negated_conjecture,
c4_1(a800) ).
cnf(u2455,negated_conjecture,
~ c2_1(a853) ).
cnf(u2466,negated_conjecture,
c3_1(a858) ).
cnf(u2489,negated_conjecture,
c5_2(a853,a886) ).
cnf(u2494,negated_conjecture,
c5_2(a858,a859) ).
cnf(u2506,negated_conjecture,
c4_2(a853,a886) ).
cnf(u2531,negated_conjecture,
~ c1_1(a824) ).
cnf(u2537,negated_conjecture,
c3_1(a824) ).
cnf(u2561,negated_conjecture,
~ sP16(a830) ).
cnf(u2565,negated_conjecture,
( ~ c2_2(a830,X0)
| c1_2(a830,X0)
| ~ c3_2(a830,X0) ) ).
cnf(u2570,negated_conjecture,
~ sP16(a800) ).
cnf(u2574,negated_conjecture,
( ~ c2_2(a800,X0)
| c1_2(a800,X0)
| ~ c3_2(a800,X0) ) ).
cnf(u2595,negated_conjecture,
~ c5_1(a853) ).
cnf(u2608,negated_conjecture,
c3_1(a892) ).
cnf(u2627,negated_conjecture,
c3_1(a887) ).
cnf(u2647,negated_conjecture,
~ c4_1(a852) ).
cnf(u2654,negated_conjecture,
~ c3_1(a852) ).
cnf(u2677,negated_conjecture,
~ sP9(a830) ).
cnf(u2720,negated_conjecture,
~ c1_1(a839) ).
cnf(u2731,negated_conjecture,
c3_1(a839) ).
cnf(u2754,negated_conjecture,
~ c5_1(a839) ).
cnf(u2763,negated_conjecture,
c5_2(a839,a811) ).
cnf(u2768,negated_conjecture,
~ c2_1(a839) ).
cnf(u2793,negated_conjecture,
c4_2(a839,a811) ).
cnf(u2797,negated_conjecture,
c3_2(a839,a811) ).
cnf(u2840,negated_conjecture,
c1_1(a786) ).
cnf(u2843,negated_conjecture,
~ c5_1(a786) ).
cnf(u2866,negated_conjecture,
~ sP16(a853) ).
cnf(u2875,negated_conjecture,
c5_2(a853,a811) ).
cnf(u2892,negated_conjecture,
~ c4_1(a853) ).
cnf(u2903,negated_conjecture,
~ c3_1(a853) ).
cnf(u2935,negated_conjecture,
~ c1_2(a875,a806) ).
cnf(u2949,negated_conjecture,
~ sP23(a824) ).
cnf(u2960,negated_conjecture,
~ sP23(a852) ).
cnf(u2969,negated_conjecture,
~ sP23(a800) ).
cnf(u2989,negated_conjecture,
~ sP23(a892) ).
cnf(u3002,negated_conjecture,
~ sP23(a830) ).
cnf(u3015,negated_conjecture,
~ c1_2(a875,a808) ).
cnf(u3029,negated_conjecture,
~ sP22(a824) ).
cnf(u3040,negated_conjecture,
~ sP22(a852) ).
cnf(u3049,negated_conjecture,
~ sP22(a800) ).
cnf(u3093,negated_conjecture,
~ sP13(a800) ).
cnf(u3111,negated_conjecture,
~ sP13(a830) ).
cnf(u3133,negated_conjecture,
~ sP9(a800) ).
cnf(u3160,negated_conjecture,
~ sP7(a853) ).
cnf(u3173,negated_conjecture,
~ sP7(a786) ).
cnf(u3186,negated_conjecture,
c5_2(a800,a877) ).
cnf(u3191,negated_conjecture,
~ sP7(a800) ).
cnf(u3257,negated_conjecture,
c1_2(a800,a877) ).
cnf(u3278,negated_conjecture,
~ c1_2(a875,a884) ).
cnf(u3295,negated_conjecture,
~ sP5(a852) ).
cnf(u3300,negated_conjecture,
~ c1_2(a824,a884) ).
cnf(u3317,negated_conjecture,
~ sP5(a800) ).
cnf(u3341,negated_conjecture,
~ sP2(a827) ).
cnf(u3353,negated_conjecture,
~ sP2(a830) ).
cnf(u3363,negated_conjecture,
~ c1_2(a875,a890) ).
cnf(u3367,negated_conjecture,
~ sP2(a875) ).
cnf(u3380,negated_conjecture,
~ sP2(a852) ).
cnf(u3385,negated_conjecture,
~ c1_2(a824,a890) ).
cnf(u3389,negated_conjecture,
~ sP2(a824) ).
cnf(u3402,negated_conjecture,
~ sP2(a800) ).
cnf(u3417,axiom,
~ sP6(a839) ).
cnf(u3426,negated_conjecture,
sP9(a839) ).
cnf(u3473,negated_conjecture,
~ sP7(a852) ).
cnf(u3496,negated_conjecture,
~ c1_2(a824,a886) ).
cnf(u3588,negated_conjecture,
~ sP6(a827) ).
cnf(u3604,negated_conjecture,
~ sP6(a786) ).
cnf(u3608,negated_conjecture,
~ c3_1(a786) ).
cnf(u3622,negated_conjecture,
~ sP6(a892) ).
cnf(u3651,negated_conjecture,
~ sP6(a824) ).
cnf(u3689,negated_conjecture,
~ sP29(a839) ).
cnf(u3730,negated_conjecture,
~ sP16(a839) ).
cnf(u3760,negated_conjecture,
~ sP13(a839) ).
cnf(u3789,negated_conjecture,
c2_2(a839,a872) ).
cnf(u4087,negated_conjecture,
~ sP13(a853) ).
cnf(u4146,negated_conjecture,
~ sP9(a853) ).
cnf(u4587,negated_conjecture,
~ c1_2(a800,a886) ).
cnf(u263,axiom,
( ~ c3_2(X0,a882)
| ~ sP6(X0) ) ).
cnf(u3999,negated_conjecture,
( c5_2(X0,a788)
| c1_2(X0,a834)
| c5_1(X0)
| ~ sP29(X0)
| c3_2(X0,a834)
| c1_2(X0,a890)
| sP16(X0)
| ~ sP2(X0) ) ).
cnf(u3569,negated_conjecture,
( c2_2(X0,a871)
| ~ c5_1(X0)
| c3_2(X0,a806)
| sP9(X0)
| ~ sP23(X0)
| c3_2(X0,a866) ) ).
cnf(u3852,negated_conjecture,
( ~ c1_2(X0,a806)
| c5_2(X0,a890)
| ~ sP2(X0)
| ~ c5_1(X0)
| c3_2(X0,a886)
| ~ sP23(X0) ) ).
cnf(u4905,negated_conjecture,
( ~ c1_2(X0,a882)
| c3_2(X0,a886)
| sP9(X0)
| c2_2(X0,a871)
| c3_2(X0,a866)
| ~ c5_1(X0)
| ~ sP7(X0)
| c3_2(X0,a877)
| ~ sP6(X0) ) ).
cnf(u2971,negated_conjecture,
( ~ c3_2(X0,a806)
| c3_2(X0,a834)
| c5_1(X0)
| c1_2(X0,a834)
| c1_1(X0)
| c5_2(X0,a811)
| ~ sP23(X0)
| c1_2(X0,a806)
| sP16(X0) ) ).
cnf(u3502,negated_conjecture,
( ~ c5_2(X0,X1)
| c5_2(X0,a890)
| ~ c1_2(X0,X1)
| ~ sP2(X0)
| ~ c5_1(X0)
| c3_2(X0,a886) ) ).
cnf(u2665,negated_conjecture,
( c5_2(X0,a811)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c5_1(X0)
| c1_2(X0,X1)
| c1_1(X0) ) ).
cnf(u3180,negated_conjecture,
( ~ c5_2(X0,a877)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c5_1(X0)
| ~ sP7(X0)
| c3_2(X0,a877) ) ).
cnf(u3345,negated_conjecture,
( c5_2(X0,a811)
| c3_2(X0,a834)
| c5_1(X0)
| c1_2(X0,a834)
| c1_1(X0)
| ~ sP2(X0)
| c1_2(X0,a890)
| sP16(X0) ) ).
cnf(u2849,negated_conjecture,
( c4_2(X0,X2)
| c5_2(X0,X1)
| c1_2(X0,X2)
| c1_1(X0)
| c3_2(X0,X2)
| c3_2(X0,X1)
| c5_2(X0,a811)
| c5_2(X0,a886)
| c5_1(X0) ) ).
cnf(u4058,negated_conjecture,
( c4_2(X0,X2)
| c5_2(X0,X1)
| c5_1(X0)
| c2_2(X0,a833)
| ~ c3_1(X0)
| c3_2(X0,X2)
| c3_2(X0,X1)
| c1_2(X0,X2)
| c5_2(X0,a886)
| ~ sP16(X0) ) ).
cnf(u3934,negated_conjecture,
( ~ c1_2(X0,a882)
| c3_2(X0,X1)
| ~ sP6(X0)
| ~ c3_1(X0)
| c2_2(X0,X1)
| ~ c5_1(X0) ) ).
cnf(u4025,negated_conjecture,
( c4_2(X0,a886)
| c4_2(X0,X2)
| c5_2(X0,X1)
| ~ sP29(X0)
| ~ c3_1(X0)
| c3_2(X0,X2)
| c3_2(X0,X1)
| c5_2(X0,a788)
| c5_1(X0)
| c1_2(X0,X2) ) ).
cnf(u4458,negated_conjecture,
( c4_2(X0,a886)
| ~ sP6(X0)
| ~ c3_1(X0)
| c4_2(X0,a882)
| c3_2(X0,a877)
| ~ sP23(X0)
| ~ c5_1(X0)
| c3_2(X0,a806)
| ~ sP7(X0) ) ).
cnf(u3886,negated_conjecture,
( ~ c1_2(X0,X1)
| c3_2(X0,X1)
| ~ sP6(X0)
| c5_2(X0,a886)
| ~ c3_1(X0)
| c4_2(X0,a882)
| ~ sP23(X0)
| ~ c5_1(X0)
| c3_2(X0,a806) ) ).
cnf(u3885,negated_conjecture,
( ~ c1_2(X0,X1)
| c3_2(X0,X1)
| ~ sP6(X0)
| c5_2(X0,a886)
| ~ c3_1(X0)
| c4_2(X0,a882)
| ~ sP22(X0)
| ~ c5_1(X0)
| c3_2(X0,a808) ) ).
cnf(u128,axiom,
( c3_2(X0,a788)
| ~ sP29(X0) ) ).
cnf(u4327,negated_conjecture,
( c2_2(X0,a871)
| ~ c3_1(X0)
| ~ sP6(X0)
| ~ c5_1(X0)
| sP9(X0)
| c3_2(X0,a866)
| ~ sP5(X0) ) ).
cnf(u201,axiom,
( c3_2(X0,a833)
| ~ sP16(X0) ) ).
cnf(u4818,negated_conjecture,
( c4_2(X0,a886)
| c5_2(X0,X1)
| c2_2(X0,a848)
| ~ c3_1(X0)
| c3_2(X0,a886)
| c3_2(X0,X1)
| c1_2(X0,a886)
| c5_1(X0)
| ~ sP13(X0) ) ).
cnf(u4925,negated_conjecture,
( c2_2(X0,a871)
| c3_2(X0,a886)
| sP9(X0)
| ~ c5_1(X0)
| c3_2(X0,a866)
| ~ sP7(X0)
| c3_2(X0,a877) ) ).
cnf(u250,axiom,
( ~ c4_2(X0,a872)
| ~ sP9(X0) ) ).
cnf(u282,axiom,
( ~ sP2(X0)
| ndr1_1(X0) ) ).
cnf(u249,axiom,
( c3_2(X0,a872)
| ~ sP9(X0) ) ).
cnf(u252,axiom,
( ~ sP9(X0)
| ndr1_1(X0) ) ).
cnf(u3204,negated_conjecture,
( c4_2(X0,a882)
| c3_1(X0)
| ~ sP6(X0)
| c1_2(X0,a882)
| ~ c4_1(X0) ) ).
cnf(u264,axiom,
( ~ sP6(X0)
| ndr1_1(X0) ) ).
cnf(u258,axiom,
( c4_2(X0,a877)
| ~ sP7(X0) ) ).
cnf(u3924,negated_conjecture,
( ~ c1_2(X0,a886)
| c3_2(X0,X1)
| ~ sP6(X0)
| ~ c3_1(X0)
| c2_2(X0,X1)
| ~ c5_1(X0)
| ~ sP7(X0)
| c5_2(X0,a877) ) ).
cnf(u4198,negated_conjecture,
( c5_2(X0,a825)
| c5_1(X0)
| c1_2(X0,a834)
| ~ c2_1(X0)
| c1_1(X0)
| c3_2(X0,a834)
| c1_2(X0,a890)
| sP16(X0)
| ~ sP2(X0) ) ).
cnf(u260,axiom,
( ~ sP7(X0)
| ndr1_1(X0) ) ).
cnf(u2850,negated_conjecture,
( c4_2(X0,a886)
| c4_2(X0,X2)
| c5_2(X0,X1)
| c1_1(X0)
| c3_2(X0,X2)
| c3_2(X0,X1)
| c5_2(X0,a811)
| c1_2(X0,X2)
| c5_1(X0) ) ).
cnf(u4898,negated_conjecture,
( ~ c1_2(X0,a808)
| c3_2(X0,a886)
| sP9(X0)
| c2_2(X0,a871)
| c3_2(X0,a866)
| ~ c5_1(X0)
| ~ sP7(X0)
| c3_2(X0,a877)
| ~ sP22(X0) ) ).
cnf(u4440,negated_conjecture,
( c4_2(X0,a886)
| ~ sP6(X0)
| ~ c3_1(X0)
| c4_2(X0,a882)
| c3_2(X0,a877)
| ~ sP22(X0)
| ~ c5_1(X0)
| c3_2(X0,a808)
| ~ sP7(X0) ) ).
cnf(u4501,negated_conjecture,
( ~ c1_2(X0,a806)
| ~ sP6(X0)
| ~ c3_1(X0)
| c4_2(X0,a882)
| c3_2(X0,X1)
| c5_2(X0,X1)
| ~ c5_1(X0)
| c3_2(X0,a886)
| ~ sP23(X0) ) ).
cnf(u3522,negated_conjecture,
( ~ c1_2(X0,a886)
| ~ sP23(X0)
| ~ c5_1(X0)
| c3_2(X0,a806)
| ~ sP7(X0)
| c5_2(X0,a877) ) ).
cnf(u3521,negated_conjecture,
( ~ c1_2(X0,a882)
| ~ sP23(X0)
| ~ c5_1(X0)
| c3_2(X0,a806)
| ~ sP6(X0) ) ).
cnf(u3200,negated_conjecture,
( c5_2(X0,a886)
| ~ sP7(X0)
| c5_2(X0,a877) ) ).
cnf(u4136,negated_conjecture,
( c1_2(X0,a890)
| ~ sP9(X0)
| c5_1(X0)
| c2_2(X0,a872)
| c1_2(X0,a834)
| c3_2(X0,a834)
| sP16(X0)
| ~ sP2(X0) ) ).
cnf(u4177,negated_conjecture,
( c4_2(X0,a886)
| c4_2(X0,X2)
| c5_2(X0,X1)
| c2_2(X0,a872)
| ~ c3_1(X0)
| c3_2(X0,X2)
| c3_2(X0,X1)
| c1_2(X0,X2)
| c5_1(X0)
| ~ sP9(X0) ) ).
cnf(u2921,negated_conjecture,
~ sP29(a830) ).
cnf(u2698,negated_conjecture,
( ~ c2_2(X0,X1)
| c3_2(X0,a834)
| c5_1(X0)
| c1_2(X0,a834)
| c1_1(X0)
| c5_2(X0,a811)
| ~ c3_2(X0,X1)
| c1_2(X0,X1)
| sP16(X0) ) ).
cnf(u3517,negated_conjecture,
( ~ c1_2(X0,a808)
| ~ sP23(X0)
| ~ c5_1(X0)
| c3_2(X0,a806)
| ~ sP22(X0) ) ).
cnf(u4024,negated_conjecture,
( c4_2(X0,X2)
| c5_2(X0,X1)
| c5_1(X0)
| ~ sP29(X0)
| ~ c3_1(X0)
| c3_2(X0,X2)
| c3_2(X0,X1)
| c5_2(X0,a788)
| c5_2(X0,a886)
| c1_2(X0,X2) ) ).
cnf(u3782,negated_conjecture,
( c4_2(X0,X1)
| c2_2(X0,X2)
| ~ sP9(X0)
| c5_1(X0)
| c2_2(X0,a872)
| ~ c3_1(X0)
| c3_2(X0,X1)
| c3_2(X0,X2)
| c1_2(X0,X1) ) ).
cnf(u281,axiom,
( c4_2(X0,a890)
| ~ sP2(X0) ) ).
cnf(u3811,negated_conjecture,
( c2_2(X0,a871)
| ~ c5_1(X0)
| c3_2(X0,a808)
| sP9(X0)
| ~ sP22(X0)
| c3_2(X0,a866) ) ).
cnf(u3099,negated_conjecture,
( c5_2(X0,X1)
| c1_2(X0,X1)
| c3_2(X0,X1)
| ~ sP13(X0)
| c5_1(X0)
| c2_2(X0,a848) ) ).
cnf(u130,axiom,
( ~ sP29(X0)
| ndr1_1(X0) ) ).
cnf(u3829,negated_conjecture,
( ~ c1_2(X0,a808)
| c5_2(X0,a877)
| ~ sP7(X0)
| ~ c5_1(X0)
| c3_2(X0,a886)
| ~ sP22(X0) ) ).
cnf(u2522,negated_conjecture,
( c4_2(a800,X0)
| c1_2(a800,X0)
| c2_2(a800,X0) ) ).
cnf(u268,axiom,
( ~ sP5(X0)
| ndr1_1(X0) ) ).
cnf(u3523,negated_conjecture,
( ~ c1_2(X0,a890)
| ~ sP23(X0)
| ~ c5_1(X0)
| c3_2(X0,a806)
| c5_2(X0,a886)
| ~ sP2(X0) ) ).
cnf(u2925,negated_conjecture,
( c5_2(X0,a788)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c1_2(X0,X1)
| c5_1(X0)
| ~ sP29(X0) ) ).
cnf(u222,axiom,
( c3_2(X0,a848)
| ~ sP13(X0) ) ).
cnf(u221,axiom,
( ~ c4_2(X0,a848)
| ~ sP13(X0) ) ).
cnf(u2919,negated_conjecture,
~ sP29(a853) ).
cnf(u2349,negated_conjecture,
( c3_2(X34,a811)
| c1_1(X34) ) ).
cnf(u202,axiom,
( ~ c5_2(X0,a833)
| ~ sP16(X0) ) ).
cnf(u171,axiom,
( ~ sP22(X0)
| ndr1_1(X0) ) ).
cnf(u2426,negated_conjecture,
c1_1(a875) ).
cnf(u4362,negated_conjecture,
( ~ c1_2(X0,a882)
| ~ sP6(X0)
| c5_2(X0,a886)
| ~ c3_1(X0)
| c3_2(X0,X1)
| c5_2(X0,X1)
| ~ c5_1(X0) ) ).
cnf(u204,axiom,
( ~ sP16(X0)
| ndr1_1(X0) ) ).
cnf(u167,axiom,
( ~ sP23(X0)
| ndr1_1(X0) ) ).
cnf(u4346,negated_conjecture,
( ~ c1_2(X0,a871)
| ~ sP6(X0)
| c5_2(X0,a886)
| ~ c3_1(X0)
| c3_2(X0,X1)
| c5_2(X0,X1)
| ~ c5_1(X0)
| sP9(X0) ) ).
cnf(u2548,negated_conjecture,
( c1_2(X0,a871)
| c2_2(X0,a871)
| ~ c5_1(X0)
| c3_2(X0,a866)
| sP9(X0) ) ).
cnf(u4176,negated_conjecture,
( c4_2(X0,X2)
| c5_2(X0,X1)
| c5_1(X0)
| c2_2(X0,a872)
| ~ c3_1(X0)
| c3_2(X0,X2)
| c3_2(X0,X1)
| c1_2(X0,X2)
| c5_2(X0,a886)
| ~ sP9(X0) ) ).
cnf(u4342,negated_conjecture,
( ~ c1_2(X0,a808)
| ~ sP6(X0)
| c5_2(X0,a886)
| ~ c3_1(X0)
| c3_2(X0,X1)
| c5_2(X0,X1)
| ~ c5_1(X0)
| ~ sP22(X0) ) ).
cnf(u2372,negated_conjecture,
~ c5_1(a817) ).
cnf(u3763,negated_conjecture,
( c4_2(X0,X1)
| c3_2(X0,X1)
| ~ sP13(X0)
| c2_2(X0,a848)
| c3_1(X0)
| c1_2(X0,X1)
| ~ c4_1(X0) ) ).
cnf(u257,axiom,
( c1_2(X0,a877)
| ~ sP7(X0) ) ).
cnf(u2741,negated_conjecture,
c4_2(a839,a886) ).
cnf(u129,axiom,
( ~ c2_2(X0,a788)
| ~ sP29(X0) ) ).
cnf(u4122,negated_conjecture,
( ~ c3_2(X0,a806)
| ~ sP9(X0)
| c5_1(X0)
| c2_2(X0,a872)
| c1_2(X0,a834)
| c3_2(X0,a834)
| c1_2(X0,a806)
| sP16(X0)
| ~ sP23(X0) ) ).
cnf(u4718,negated_conjecture,
( c4_2(X0,a886)
| c5_2(X0,X1)
| c2_2(X0,a833)
| ~ c3_1(X0)
| c3_2(X0,a886)
| c3_2(X0,X1)
| c1_2(X0,a886)
| c5_1(X0)
| ~ sP16(X0) ) ).
cnf(u3857,negated_conjecture,
( ~ c1_2(X0,a882)
| c5_2(X0,a890)
| ~ sP2(X0)
| ~ c5_1(X0)
| c3_2(X0,a886)
| ~ sP6(X0) ) ).
cnf(u4115,negated_conjecture,
( c4_2(X0,X2)
| c5_2(X0,X1)
| c5_1(X0)
| c2_2(X0,a848)
| ~ c3_1(X0)
| c3_2(X0,X2)
| c3_2(X0,X1)
| c1_2(X0,X2)
| c5_2(X0,a886)
| ~ sP13(X0) ) ).
cnf(u3856,negated_conjecture,
( ~ c1_2(X0,a871)
| c5_2(X0,a890)
| ~ sP2(X0)
| ~ c5_1(X0)
| c3_2(X0,a886)
| sP9(X0) ) ).
cnf(u3540,negated_conjecture,
( ~ c1_2(X0,a882)
| ~ sP22(X0)
| ~ c5_1(X0)
| c3_2(X0,a808)
| ~ sP6(X0) ) ).
cnf(u3986,negated_conjecture,
( c5_2(X0,a890)
| ~ sP2(X0)
| ~ c5_1(X0)
| c3_2(X0,a886)
| sP9(X0)
| c2_2(X0,a871)
| c3_2(X0,a866) ) ).
cnf(u3181,negated_conjecture,
~ sP7(a875) ).
cnf(u3206,negated_conjecture,
( c4_2(X0,a882)
| c2_2(X0,X1)
| ~ c3_1(X0)
| c3_2(X0,X1)
| ~ sP6(X0) ) ).
cnf(u4917,negated_conjecture,
( ~ c1_2(X0,a890)
| c3_2(X0,a886)
| sP9(X0)
| c2_2(X0,a871)
| c3_2(X0,a866)
| ~ c5_1(X0)
| ~ sP7(X0)
| c3_2(X0,a877)
| ~ sP2(X0) ) ).
cnf(u3343,negated_conjecture,
( c5_2(X0,a890)
| c5_2(X0,a886)
| ~ sP2(X0) ) ).
cnf(u3938,negated_conjecture,
( c5_2(X0,a877)
| ~ sP7(X0)
| ~ c5_1(X0)
| c3_2(X0,a886)
| sP9(X0)
| c2_2(X0,a871)
| c3_2(X0,a866) ) ).
cnf(u3733,negated_conjecture,
( c4_2(X0,X1)
| c3_2(X0,X1)
| ~ sP16(X0)
| c2_2(X0,a833)
| c3_1(X0)
| c1_2(X0,X1)
| ~ c4_1(X0) ) ).
cnf(u3201,negated_conjecture,
( c4_2(X0,a886)
| ~ sP7(X0)
| c5_2(X0,a877) ) ).
cnf(u3918,negated_conjecture,
( ~ c1_2(X0,a806)
| c3_2(X0,X1)
| ~ sP6(X0)
| ~ c3_1(X0)
| c2_2(X0,X1)
| ~ c5_1(X0)
| ~ sP23(X0) ) ).
cnf(u3097,negated_conjecture,
( c1_2(X0,a848)
| ~ sP13(X0)
| c2_2(X0,a848)
| ~ c5_1(X0)
| c3_2(X0,a866) ) ).
cnf(u251,axiom,
( ~ c5_2(X0,a872)
| ~ sP9(X0) ) ).
cnf(u2664,negated_conjecture,
( c5_2(X0,a825)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c5_1(X0)
| c1_2(X0,X1)
| ~ c2_1(X0)
| c1_1(X0) ) ).
cnf(u3682,negated_conjecture,
( ~ c2_2(X0,X1)
| c3_2(X0,a834)
| c1_2(X0,a834)
| c5_1(X0)
| ~ sP29(X0)
| c5_2(X0,a788)
| ~ c3_2(X0,X1)
| c1_2(X0,X1)
| sP16(X0) ) ).
cnf(u4502,negated_conjecture,
( ~ c1_2(X0,a808)
| ~ sP6(X0)
| ~ c3_1(X0)
| c4_2(X0,a882)
| c3_2(X0,X1)
| c5_2(X0,X1)
| ~ c5_1(X0)
| c3_2(X0,a886)
| ~ sP22(X0) ) ).
cnf(u3989,negated_conjecture,
( ~ c3_2(X0,a806)
| c1_2(X0,a834)
| c5_1(X0)
| ~ sP29(X0)
| c5_2(X0,a788)
| c3_2(X0,a834)
| c1_2(X0,a806)
| sP16(X0)
| ~ sP23(X0) ) ).
cnf(u266,axiom,
( ~ c2_2(X0,a884)
| ~ sP5(X0) ) ).
cnf(u3833,negated_conjecture,
( ~ c1_2(X0,a882)
| c5_2(X0,a877)
| ~ sP7(X0)
| ~ c5_1(X0)
| c3_2(X0,a886)
| ~ sP6(X0) ) ).
cnf(u4577,negated_conjecture,
( c4_2(X0,a886)
| c5_2(X0,X1)
| c1_1(X0)
| c3_2(X0,a886)
| c3_2(X0,X1)
| c5_2(X0,a811)
| c1_2(X0,a886)
| c5_1(X0) ) ).
cnf(u4424,negated_conjecture,
( c4_2(X0,a882)
| ~ sP6(X0)
| c5_2(X0,a886)
| ~ c3_1(X0)
| c3_2(X0,a877)
| ~ sP23(X0)
| ~ c5_1(X0)
| c3_2(X0,a806)
| ~ sP7(X0) ) ).
cnf(u262,axiom,
( ~ c2_2(X0,a882)
| ~ sP6(X0) ) ).
cnf(u4507,negated_conjecture,
( ~ c1_2(X0,a871)
| ~ sP6(X0)
| ~ c3_1(X0)
| c4_2(X0,a882)
| c3_2(X0,X1)
| c5_2(X0,X1)
| ~ c5_1(X0)
| c3_2(X0,a886)
| sP9(X0) ) ).
cnf(u2408,negated_conjecture,
( ~ c5_1(X0)
| c2_1(X0)
| c3_1(X0) ) ).
cnf(u223,axiom,
( ~ c5_2(X0,a848)
| ~ sP13(X0) ) ).
cnf(u3614,negated_conjecture,
( c4_2(X0,a882)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ sP6(X0)
| c5_2(X0,a886)
| ~ c3_1(X0) ) ).
cnf(u3908,negated_conjecture,
( ~ c5_2(X0,X2)
| c3_2(X0,X1)
| ~ sP6(X0)
| ~ c3_1(X0)
| c4_2(X0,a882)
| ~ c1_2(X0,X2)
| c5_2(X0,X1)
| ~ c5_1(X0)
| c3_2(X0,a886) ) ).
cnf(u3893,negated_conjecture,
( ~ c5_2(X0,X2)
| c3_2(X0,X1)
| ~ sP6(X0)
| c5_2(X0,a886)
| ~ c3_1(X0)
| ~ c1_2(X0,X2)
| c5_2(X0,X1)
| ~ c5_1(X0) ) ).
cnf(u203,axiom,
( c1_2(X0,a833)
| ~ sP16(X0) ) ).
cnf(u168,axiom,
( c4_2(X0,a808)
| ~ sP22(X0) ) ).
cnf(u2515,negated_conjecture,
( c4_2(X0,a871)
| c3_1(X0)
| c1_2(X0,a871)
| ~ c4_1(X0)
| sP9(X0) ) ).
cnf(u2397,negated_conjecture,
~ c3_1(a817) ).
cnf(u3542,negated_conjecture,
( ~ c1_2(X0,a890)
| ~ sP22(X0)
| ~ c5_1(X0)
| c3_2(X0,a808)
| c5_2(X0,a886)
| ~ sP2(X0) ) ).
cnf(u3828,negated_conjecture,
( ~ c1_2(X0,a806)
| c5_2(X0,a877)
| ~ sP7(X0)
| ~ c5_1(X0)
| c3_2(X0,a886)
| ~ sP23(X0) ) ).
cnf(u164,axiom,
( c4_2(X0,a806)
| ~ sP23(X0) ) ).
cnf(u4184,negated_conjecture,
( ~ c3_2(X0,a806)
| c5_1(X0)
| c1_2(X0,a834)
| ~ c2_1(X0)
| c1_1(X0)
| c5_2(X0,a825)
| c3_2(X0,a834)
| c1_2(X0,a806)
| sP16(X0)
| ~ sP23(X0) ) ).
cnf(u2347,negated_conjecture,
ndr1_1(X79) ).
cnf(u127,axiom,
( c1_2(X0,a788)
| ~ sP29(X0) ) ).
cnf(u3344,negated_conjecture,
( c4_2(X0,a886)
| ~ sP2(X0)
| c5_2(X0,a890) ) ).
cnf(u279,axiom,
( c3_2(X0,a890)
| ~ sP2(X0) ) ).
cnf(u265,axiom,
( ~ c3_2(X0,a884)
| ~ sP5(X0) ) ).
cnf(u3520,negated_conjecture,
( ~ c1_2(X0,a871)
| ~ sP23(X0)
| ~ c5_1(X0)
| c3_2(X0,a806)
| sP9(X0) ) ).
cnf(u259,axiom,
( c2_2(X0,a877)
| ~ sP7(X0) ) ).
cnf(u3182,negated_conjecture,
~ sP7(a824) ).
cnf(u261,axiom,
( c5_2(X0,a882)
| ~ sP6(X0) ) ).
cnf(u3056,negated_conjecture,
( c5_2(X0,X1)
| c1_2(X0,X1)
| c3_2(X0,X1)
| ~ sP16(X0)
| c5_1(X0)
| c2_2(X0,a833) ) ).
cnf(u4522,negated_conjecture,
( ~ c1_2(X0,a882)
| ~ sP6(X0)
| ~ c3_1(X0)
| c4_2(X0,a882)
| c3_2(X0,X1)
| c5_2(X0,X1)
| ~ c5_1(X0)
| c3_2(X0,a886) ) ).
cnf(u2740,negated_conjecture,
c5_2(a839,a886) ).
cnf(u3461,negated_conjecture,
( ~ c5_2(X0,X1)
| c5_2(X0,a877)
| ~ c1_2(X0,X1)
| ~ sP7(X0)
| ~ c5_1(X0)
| c3_2(X0,a886) ) ).
cnf(u3785,negated_conjecture,
( c4_2(X0,X1)
| c3_2(X0,X1)
| ~ sP9(X0)
| c2_2(X0,a872)
| c3_1(X0)
| c1_2(X0,X1)
| ~ c4_1(X0) ) ).
cnf(u2952,negated_conjecture,
( ~ c5_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ sP23(X0)
| ~ c5_1(X0)
| c3_2(X0,a806) ) ).
cnf(u3902,negated_conjecture,
( ~ c1_2(X0,X1)
| c3_2(X0,X1)
| ~ sP6(X0)
| ~ c3_1(X0)
| c4_2(X0,a882)
| c4_2(X0,a886)
| ~ sP23(X0)
| ~ c5_1(X0)
| c3_2(X0,a806) ) ).
cnf(u3901,negated_conjecture,
( ~ c1_2(X0,X1)
| c3_2(X0,X1)
| ~ sP6(X0)
| ~ c3_1(X0)
| c4_2(X0,a882)
| c4_2(X0,a886)
| ~ sP22(X0)
| ~ c5_1(X0)
| c3_2(X0,a808) ) ).
cnf(u267,axiom,
( c4_2(X0,a884)
| ~ sP5(X0) ) ).
cnf(u3535,negated_conjecture,
( ~ c1_2(X0,a806)
| ~ sP22(X0)
| ~ c5_1(X0)
| c3_2(X0,a808)
| ~ sP23(X0) ) ).
cnf(u4077,negated_conjecture,
( c1_2(X0,a890)
| ~ sP13(X0)
| c5_1(X0)
| c2_2(X0,a848)
| c1_2(X0,a834)
| c3_2(X0,a834)
| sP16(X0)
| ~ sP2(X0) ) ).
cnf(u4064,negated_conjecture,
( ~ c3_2(X0,a806)
| ~ sP13(X0)
| c5_1(X0)
| c2_2(X0,a848)
| c1_2(X0,a834)
| c3_2(X0,a834)
| c1_2(X0,a806)
| sP16(X0)
| ~ sP23(X0) ) ).
cnf(u2700,negated_conjecture,
( c4_2(X0,X1)
| c2_2(X0,X2)
| c5_1(X0)
| c1_2(X0,X1)
| c1_1(X0)
| c3_2(X0,X1)
| c3_2(X0,X2)
| c5_2(X0,a811) ) ).
cnf(u280,axiom,
( c2_2(X0,a890)
| ~ sP2(X0) ) ).
cnf(u3780,negated_conjecture,
( ~ c2_2(X0,X1)
| c3_2(X0,a834)
| ~ sP9(X0)
| c5_1(X0)
| c2_2(X0,a872)
| c1_2(X0,a834)
| ~ c3_2(X0,X1)
| c1_2(X0,X1)
| sP16(X0) ) ).
cnf(u3752,negated_conjecture,
( c4_2(X0,X1)
| c2_2(X0,X2)
| ~ sP13(X0)
| c5_1(X0)
| c2_2(X0,a848)
| ~ c3_1(X0)
| c3_2(X0,X1)
| c3_2(X0,X2)
| c1_2(X0,X1) ) ).
cnf(u3699,negated_conjecture,
( c4_2(X0,X1)
| c3_2(X0,X1)
| c1_2(X0,X1)
| ~ sP29(X0)
| c3_1(X0)
| c5_2(X0,a788)
| ~ c4_1(X0) ) ).
cnf(u4200,negated_conjecture,
( c2_2(X0,a871)
| c2_2(X0,X1)
| ~ c3_1(X0)
| ~ sP6(X0)
| ~ c5_1(X0)
| sP9(X0)
| c3_2(X0,X1)
| c3_2(X0,a866) ) ).
cnf(u3853,negated_conjecture,
( ~ c1_2(X0,a808)
| c5_2(X0,a890)
| ~ sP2(X0)
| ~ c5_1(X0)
| c3_2(X0,a886)
| ~ sP22(X0) ) ).
cnf(u4663,negated_conjecture,
( c4_2(X0,a886)
| c5_2(X0,X1)
| ~ sP29(X0)
| ~ c3_1(X0)
| c3_2(X0,a886)
| c3_2(X0,X1)
| c5_2(X0,a788)
| c5_1(X0)
| c1_2(X0,a886) ) ).
cnf(u2549,negated_conjecture,
( c1_2(X0,a811)
| ~ c5_1(X0)
| c3_2(X0,a866)
| c1_1(X0) ) ).
cnf(u3551,negated_conjecture,
( ~ c1_2(X0,a808)
| ~ sP22(X0)
| ~ c5_1(X0)
| c3_2(X0,a808) ) ).
cnf(u3615,negated_conjecture,
( c4_2(X0,a886)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ sP6(X0)
| ~ c3_1(X0)
| c4_2(X0,a882) ) ).
cnf(u3319,negated_conjecture,
( ~ c5_2(X0,a884)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c5_1(X0)
| ~ sP5(X0) ) ).
cnf(u4949,negated_conjecture,
( c4_2(X0,a886)
| c5_2(X0,X1)
| c2_2(X0,a872)
| ~ c3_1(X0)
| c3_2(X0,a886)
| c3_2(X0,X1)
| c1_2(X0,a886)
| c5_1(X0)
| ~ sP9(X0) ) ).
cnf(u2714,negated_conjecture,
( c4_2(X0,X1)
| c3_2(X0,X1)
| c5_1(X0)
| c1_2(X0,X1)
| ~ c2_1(X0)
| c1_1(X0)
| c5_2(X0,a825) ) ).
cnf(u3919,negated_conjecture,
( ~ c1_2(X0,a808)
| c3_2(X0,X1)
| ~ sP6(X0)
| ~ c3_1(X0)
| c2_2(X0,X1)
| ~ c5_1(X0)
| ~ sP22(X0) ) ).
cnf(u3115,negated_conjecture,
( c1_2(X0,a872)
| ~ sP9(X0)
| c2_2(X0,a872)
| ~ c5_1(X0)
| c3_2(X0,a866) ) ).
cnf(u3922,negated_conjecture,
( ~ c1_2(X0,a871)
| c3_2(X0,X1)
| ~ sP6(X0)
| ~ c3_1(X0)
| c2_2(X0,X1)
| ~ c5_1(X0)
| sP9(X0) ) ).
cnf(u3117,negated_conjecture,
( c5_2(X0,X1)
| c1_2(X0,X1)
| c3_2(X0,X1)
| ~ sP9(X0)
| c5_1(X0)
| c2_2(X0,a872) ) ).
cnf(u3750,negated_conjecture,
( ~ c2_2(X0,X1)
| c3_2(X0,a834)
| ~ sP13(X0)
| c5_1(X0)
| c2_2(X0,a848)
| c1_2(X0,a834)
| ~ c3_2(X0,X1)
| c1_2(X0,X1)
| sP16(X0) ) ).
cnf(u4408,negated_conjecture,
( c4_2(X0,a882)
| ~ sP6(X0)
| c5_2(X0,a886)
| ~ c3_1(X0)
| c3_2(X0,a877)
| ~ sP22(X0)
| ~ c5_1(X0)
| c3_2(X0,a808)
| ~ sP7(X0) ) ).
cnf(u4059,negated_conjecture,
( c4_2(X0,a886)
| c4_2(X0,X2)
| c5_2(X0,X1)
| c2_2(X0,a833)
| ~ c3_1(X0)
| c3_2(X0,X2)
| c3_2(X0,X1)
| c1_2(X0,X2)
| c5_1(X0)
| ~ sP16(X0) ) ).
cnf(u3539,negated_conjecture,
( ~ c1_2(X0,a871)
| ~ sP22(X0)
| ~ c5_1(X0)
| c3_2(X0,a808)
| sP9(X0) ) ).
cnf(u4897,negated_conjecture,
( ~ c1_2(X0,a806)
| c3_2(X0,a886)
| sP9(X0)
| c2_2(X0,a871)
| c3_2(X0,a866)
| ~ c5_1(X0)
| ~ sP7(X0)
| c3_2(X0,a877)
| ~ sP23(X0) ) ).
cnf(u3032,negated_conjecture,
( ~ c5_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ sP22(X0)
| ~ c5_1(X0)
| c3_2(X0,a808) ) ).
cnf(u224,axiom,
( ~ sP13(X0)
| ndr1_1(X0) ) ).
cnf(u4224,negated_conjecture,
( ~ c5_2(X0,X1)
| ~ c5_1(X0)
| c3_2(X0,a886)
| sP9(X0)
| c2_2(X0,a871)
| c3_2(X0,a866)
| ~ c1_2(X0,X1)
| ~ sP7(X0)
| c3_2(X0,a877) ) ).
cnf(u3722,negated_conjecture,
( c4_2(X0,X1)
| c2_2(X0,X2)
| ~ sP16(X0)
| c5_1(X0)
| c2_2(X0,a833)
| ~ c3_1(X0)
| c3_2(X0,X1)
| c3_2(X0,X2)
| c1_2(X0,X1) ) ).
cnf(u3925,negated_conjecture,
( ~ c1_2(X0,a890)
| c3_2(X0,X1)
| ~ sP6(X0)
| ~ c3_1(X0)
| c2_2(X0,X1)
| ~ c5_1(X0)
| c5_2(X0,a886)
| ~ sP2(X0) ) ).
cnf(u4908,negated_conjecture,
( ~ c1_2(X0,a890)
| c3_2(X0,a886)
| sP9(X0)
| c2_2(X0,a871)
| c3_2(X0,a866)
| ~ c5_1(X0)
| ~ sP7(X0)
| c3_2(X0,a877)
| c5_2(X0,a886)
| ~ sP2(X0) ) ).
cnf(u170,axiom,
( c5_2(X0,a808)
| ~ sP22(X0) ) ).
cnf(u4341,negated_conjecture,
( ~ c1_2(X0,a806)
| ~ sP6(X0)
| c5_2(X0,a886)
| ~ c3_1(X0)
| c3_2(X0,X1)
| c5_2(X0,X1)
| ~ c5_1(X0)
| ~ sP23(X0) ) ).
cnf(u169,axiom,
( ~ c2_2(X0,a808)
| ~ sP22(X0) ) ).
cnf(u4328,negated_conjecture,
( c2_2(X0,a871)
| ~ c3_1(X0)
| ~ sP6(X0)
| ~ c5_1(X0)
| sP9(X0)
| c3_2(X0,a866) ) ).
cnf(u4360,negated_conjecture,
( ~ c1_2(X0,a890)
| ~ sP6(X0)
| c5_2(X0,a886)
| ~ c3_1(X0)
| c3_2(X0,X1)
| c5_2(X0,X1)
| ~ c5_1(X0)
| ~ sP2(X0) ) ).
cnf(u2710,negated_conjecture,
( ~ c2_2(X0,X1)
| c3_2(X0,a834)
| c5_1(X0)
| c1_2(X0,a834)
| ~ c2_1(X0)
| c1_1(X0)
| c5_2(X0,a825)
| ~ c3_2(X0,X1)
| c1_2(X0,X1)
| sP16(X0) ) ).
cnf(u3541,negated_conjecture,
( ~ c1_2(X0,a886)
| ~ sP22(X0)
| ~ c5_1(X0)
| c3_2(X0,a808)
| ~ sP7(X0)
| c5_2(X0,a877) ) ).
cnf(u166,axiom,
( c5_2(X0,a806)
| ~ sP23(X0) ) ).
cnf(u3832,negated_conjecture,
( ~ c1_2(X0,a871)
| c5_2(X0,a877)
| ~ sP7(X0)
| ~ c5_1(X0)
| c3_2(X0,a886)
| sP9(X0) ) ).
cnf(u165,axiom,
( c2_2(X0,a806)
| ~ sP23(X0) ) ).
cnf(u3532,negated_conjecture,
( ~ c1_2(X0,a806)
| ~ sP23(X0)
| ~ c5_1(X0)
| c3_2(X0,a806) ) ).
cnf(u4116,negated_conjecture,
( c4_2(X0,a886)
| c4_2(X0,X2)
| c5_2(X0,X1)
| c2_2(X0,a848)
| ~ c3_1(X0)
| c3_2(X0,X2)
| c3_2(X0,X1)
| c1_2(X0,X2)
| c5_1(X0)
| ~ sP13(X0) ) ).
cnf(u3844,negated_conjecture,
( ~ c1_2(X0,a886)
| c5_2(X0,a877)
| ~ sP7(X0)
| ~ c5_1(X0)
| c3_2(X0,a886) ) ).
cnf(u3656,negated_conjecture,
( ~ c5_2(X0,X2)
| ~ c3_1(X0)
| c3_2(X0,X1)
| ~ sP6(X0)
| ~ c1_2(X0,X2)
| c2_2(X0,X1)
| ~ c5_1(X0) ) ).
cnf(u3684,negated_conjecture,
( c4_2(X0,X1)
| c2_2(X0,X2)
| c1_2(X0,X1)
| c5_1(X0)
| ~ sP29(X0)
| ~ c3_1(X0)
| c3_2(X0,X1)
| c3_2(X0,X2)
| c5_2(X0,a788) ) ).
cnf(u2350,negated_conjecture,
( ~ c2_2(X34,a811)
| c1_1(X34) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN513+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.24 % Computer : n019.cluster.edu
% 0.12/0.24 % Model : x86_64 x86_64
% 0.12/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.24 % Memory : 8046.5625MB
% 0.12/0.24 % OS : Linux 6.8.0-71-generic
% 0.12/0.24 % CPULimit : 300
% 0.12/0.24 % WCLimit : 300
% 0.12/0.24 % DateTime : Mon Sep 28 16:21:19 UTC 2026
% 0.12/0.24 % CPUTime :
% 0.12/0.24 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.25/0.30 Running first-order theorem proving
% 0.25/0.30 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
% 4.02/1.35 % (4132458)Detected formulas, will run a generic FOF schedule.
% 4.02/1.35 % (4132471)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=1429161523:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.02/1.35 % (4132473)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=3004167337:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.02/1.35 % (4132474)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2997212521:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.02/1.35 % (4132472)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=2903031298:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.02/1.35 % (4132475)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=29532254:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.02/1.35 % (4132476)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=428870420:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.02/1.35 % (4132477)dis-21_1_sil=8000:lcm=predicate:random_seed=2295626844: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)
% 4.02/1.35 % (4132476)Refutation not found, incomplete strategy
% 4.02/1.35 % (4132476)------------------------------
% 4.02/1.35 % (4132476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.02/1.35 % (4132476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/1.35 % (4132476)CaDiCaL version: 2.1.3
% 4.02/1.35 % (4132476)Termination reason: Refutation not found, incomplete strategy
% 4.02/1.35 % (4132476)Time elapsed: 0.045 s
% 4.02/1.35 % (4132476)Peak memory usage: 90 MB
% 4.02/1.35 % (4132476)Instructions burned: 43 (million)
% 4.02/1.35 % (4132475)Instruction limit reached!
% 4.02/1.35 % (4132475)------------------------------
% 4.02/1.35 % (4132475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.02/1.35 % (4132475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/1.35 % (4132475)CaDiCaL version: 2.1.3
% 4.02/1.35 % (4132475)Termination reason: Instruction limit
% 4.02/1.35 % (4132475)Termination phase: Saturation
% 4.02/1.35 % (4132475)Time elapsed: 0.093 s
% 4.02/1.35 % (4132475)Peak memory usage: 89 MB
% 4.02/1.35 % (4132475)Instructions burned: 123 (million)
% 4.02/1.35 % (4132474)Instruction limit reached!
% 4.02/1.35 % (4132474)------------------------------
% 4.02/1.35 % (4132474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.02/1.35 % (4132474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/1.35 % (4132474)CaDiCaL version: 2.1.3
% 4.02/1.35 % (4132474)Termination reason: Instruction limit
% 4.02/1.35 % (4132474)Termination phase: Saturation
% 4.02/1.35 % (4132474)Time elapsed: 0.103 s
% 4.02/1.35 % (4132474)Peak memory usage: 90 MB
% 4.02/1.35 % (4132474)Instructions burned: 109 (million)
% 4.02/1.35 % (4132477)Instruction limit reached!
% 4.02/1.35 % (4132477)------------------------------
% 4.02/1.35 % (4132477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.02/1.35 % (4132477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/1.35 % (4132477)CaDiCaL version: 2.1.3
% 4.02/1.35 % (4132477)Termination reason: Instruction limit
% 4.02/1.35 % (4132477)Termination phase: Saturation
% 4.02/1.35 % (4132477)Time elapsed: 0.124 s
% 4.02/1.35 % (4132477)Peak memory usage: 91 MB
% 4.02/1.35 % (4132477)Instructions burned: 129 (million)
% 4.02/1.35 % (4132489)lrs+10_1_sil=8000:sp=occurrence:random_seed=478992928:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 4.02/1.35 % (4132489)First to succeed.
% 4.02/1.35 % (4132489)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4132458"
% 4.02/1.35 % (4132490)lrs+10_1_sil=32000:urr=on:br=off:random_seed=396641350:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 4.02/1.35 % (4132490)Refutation not found, incomplete strategy
% 4.02/1.35 % (4132490)------------------------------
% 4.02/1.35 % (4132490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.02/1.35 % (4132490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/1.35 % (4132490)CaDiCaL version: 2.1.3
% 4.02/1.35 % (4132490)Termination reason: Refutation not found, incomplete strategy
% 4.02/1.35 % (4132490)Time elapsed: 0.027 s
% 4.02/1.35 % (4132490)Peak memory usage: 90 MB
% 4.02/1.35 % (4132490)Instructions burned: 27 (million)
% 4.02/1.35 % (4132491)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1618411573:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 4.02/1.35 % (4132491)Refutation not found, incomplete strategy
% 4.02/1.35 % (4132491)------------------------------
% 4.02/1.35 % (4132491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.02/1.35 % (4132491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/1.35 % (4132491)CaDiCaL version: 2.1.3
% 4.02/1.35 % (4132491)Termination reason: Refutation not found, incomplete strategy
% 4.02/1.35 % (4132491)Time elapsed: 0.041 s
% 4.02/1.35 % (4132491)Peak memory usage: 90 MB
% 4.02/1.35 % (4132491)Instructions burned: 40 (million)
% 4.02/1.35 % SZS status CounterSatisfiable for theBenchmark
% 4.02/1.35 % SZS output start Saturation.
% See solution above
% 5.20/1.45 % SZS output start Definitions and Model Updates.
% 5.20/1.45 % SZS output end Definitions and Model Updates.
% 5.20/1.45 % (4132489)------------------------------
% 5.20/1.45 % (4132489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.20/1.45 % (4132489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.20/1.45 % (4132489)CaDiCaL version: 2.1.3
% 5.20/1.45 % (4132489)Termination reason: Satisfiable
% 5.20/1.45 % (4132489)Time elapsed: 0.046 s
% 5.20/1.45 % (4132489)Peak memory usage: 91 MB
% 5.20/1.45 % (4132489)Instructions burned: 86 (million)
% 5.20/1.45 % (4132489)------------------------------
% 5.20/1.45 % (4132489)------------------------------
% 5.20/1.45 % (4132458)Success in time 0.661 s
% 5.20/1.45 % Vampire exiting
%------------------------------------------------------------------------------