%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL645+1.020 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:59:11 AM UTC 2026
% Result : CounterSatisfiable 0.07s 0.41s
% Output : Saturation 0.07s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1668,axiom,
~ p77(sK76(X0)) ).
cnf(u1671,axiom,
~ sP74(X0) ).
cnf(u1674,axiom,
~ p76(sK78(X0)) ).
cnf(u1677,axiom,
~ sP73(X0) ).
cnf(u1680,axiom,
~ p75(sK80(X0)) ).
cnf(u1683,axiom,
~ sP72(X0) ).
cnf(u1686,axiom,
~ p74(sK82(X0)) ).
cnf(u1689,axiom,
~ sP71(X0) ).
cnf(u1692,axiom,
~ p73(sK84(X0)) ).
cnf(u1695,axiom,
~ sP70(X0) ).
cnf(u1698,axiom,
~ p72(sK86(X0)) ).
cnf(u1701,axiom,
~ sP69(X0) ).
cnf(u1704,axiom,
~ p71(sK88(X0)) ).
cnf(u1707,axiom,
~ sP68(X0) ).
cnf(u1710,axiom,
~ p70(sK90(X0)) ).
cnf(u1713,axiom,
~ sP67(X0) ).
cnf(u1716,axiom,
~ p69(sK92(X0)) ).
cnf(u1719,axiom,
~ sP66(X0) ).
cnf(u1722,axiom,
~ p68(sK94(X0)) ).
cnf(u1725,axiom,
~ sP65(X0) ).
cnf(u1728,axiom,
~ p67(sK96(X0)) ).
cnf(u1731,axiom,
~ sP64(X0) ).
cnf(u1734,axiom,
~ p66(sK98(X0)) ).
cnf(u1737,axiom,
~ sP63(X0) ).
cnf(u1740,axiom,
~ p65(sK100(X0)) ).
cnf(u1743,axiom,
~ sP62(X0) ).
cnf(u1746,axiom,
~ p64(sK102(X0)) ).
cnf(u1749,axiom,
~ sP61(X0) ).
cnf(u1752,axiom,
~ p63(sK104(X0)) ).
cnf(u1755,axiom,
~ sP60(X0) ).
cnf(u1758,axiom,
~ p62(sK106(X0)) ).
cnf(u1761,axiom,
~ sP59(X0) ).
cnf(u1764,axiom,
~ p61(sK108(X0)) ).
cnf(u1767,axiom,
~ sP58(X0) ).
cnf(u1770,axiom,
~ p60(sK110(X0)) ).
cnf(u1773,axiom,
~ sP57(X0) ).
cnf(u1776,axiom,
~ p59(sK112(X0)) ).
cnf(u1779,axiom,
~ sP56(X0) ).
cnf(u1782,axiom,
~ p58(sK114(X0)) ).
cnf(u1785,axiom,
~ sP55(X0) ).
cnf(u1788,axiom,
~ p57(sK116(X0)) ).
cnf(u1791,axiom,
~ sP54(X0) ).
cnf(u1794,axiom,
~ p56(sK118(X0)) ).
cnf(u1797,axiom,
~ sP53(X0) ).
cnf(u1800,axiom,
~ p55(sK120(X0)) ).
cnf(u1803,axiom,
~ sP52(X0) ).
cnf(u1806,axiom,
~ p54(sK122(X0)) ).
cnf(u1809,axiom,
~ sP51(X0) ).
cnf(u1812,axiom,
~ p53(sK124(X0)) ).
cnf(u1815,axiom,
~ sP50(X0) ).
cnf(u1818,axiom,
~ p52(sK126(X0)) ).
cnf(u1821,axiom,
~ sP49(X0) ).
cnf(u1824,axiom,
~ p51(sK128(X0)) ).
cnf(u1827,axiom,
~ sP48(X0) ).
cnf(u1830,axiom,
~ p50(sK130(X0)) ).
cnf(u1833,axiom,
~ sP47(X0) ).
cnf(u1836,axiom,
~ p49(sK132(X0)) ).
cnf(u1839,axiom,
~ sP46(X0) ).
cnf(u1842,axiom,
~ p48(sK134(X0)) ).
cnf(u1845,axiom,
~ sP45(X0) ).
cnf(u1848,axiom,
~ p47(sK136(X0)) ).
cnf(u1851,axiom,
~ sP44(X0) ).
cnf(u1854,axiom,
~ p46(sK138(X0)) ).
cnf(u1857,axiom,
~ sP43(X0) ).
cnf(u1860,axiom,
~ p45(sK140(X0)) ).
cnf(u1863,axiom,
~ sP42(X0) ).
cnf(u1866,axiom,
~ p44(sK142(X0)) ).
cnf(u1869,axiom,
~ sP41(X0) ).
cnf(u1872,axiom,
~ p43(sK144(X0)) ).
cnf(u1875,axiom,
~ sP40(X0) ).
cnf(u1878,axiom,
~ p42(sK146(X0)) ).
cnf(u1881,axiom,
~ sP39(X0) ).
cnf(u1884,axiom,
~ p41(sK148(X0)) ).
cnf(u1887,axiom,
~ sP38(X0) ).
cnf(u1890,axiom,
~ p39(sK150(X0)) ).
cnf(u1893,axiom,
~ sP37(X0) ).
cnf(u1896,axiom,
~ p38(sK152(X0)) ).
cnf(u1899,axiom,
~ sP36(X0) ).
cnf(u1902,axiom,
~ p37(sK154(X0)) ).
cnf(u1905,axiom,
~ sP35(X0) ).
cnf(u1908,axiom,
~ p36(sK156(X0)) ).
cnf(u1911,axiom,
~ sP34(X0) ).
cnf(u1914,axiom,
~ p35(sK158(X0)) ).
cnf(u1917,axiom,
~ sP33(X0) ).
cnf(u1920,axiom,
~ p34(sK160(X0)) ).
cnf(u1923,axiom,
~ sP32(X0) ).
cnf(u1926,axiom,
~ p33(sK162(X0)) ).
cnf(u1929,axiom,
~ sP31(X0) ).
cnf(u1932,axiom,
~ p32(sK164(X0)) ).
cnf(u1935,axiom,
~ sP30(X0) ).
cnf(u1938,axiom,
~ p31(sK166(X0)) ).
cnf(u1941,axiom,
~ sP29(X0) ).
cnf(u1944,axiom,
~ p30(sK168(X0)) ).
cnf(u1947,axiom,
~ sP28(X0) ).
cnf(u1950,axiom,
~ p29(sK170(X0)) ).
cnf(u1953,axiom,
~ sP27(X0) ).
cnf(u1956,axiom,
~ p28(sK172(X0)) ).
cnf(u1959,axiom,
~ sP26(X0) ).
cnf(u1962,axiom,
~ p27(sK174(X0)) ).
cnf(u1965,axiom,
~ sP25(X0) ).
cnf(u1968,axiom,
~ p26(sK176(X0)) ).
cnf(u1971,axiom,
~ sP24(X0) ).
cnf(u1974,negated_conjecture,
~ r1(sK412,X448) ).
cnf(u1980,axiom,
~ p25(sK178(X0)) ).
cnf(u1983,axiom,
~ sP23(X0) ).
cnf(u1986,axiom,
~ p24(sK180(X0)) ).
cnf(u1989,axiom,
~ sP22(X0) ).
cnf(u1992,axiom,
~ p23(sK182(X0)) ).
cnf(u1995,axiom,
~ sP21(X0) ).
cnf(u1998,axiom,
~ p22(sK184(X0)) ).
cnf(u2001,axiom,
~ sP20(X0) ).
cnf(u2004,axiom,
~ p21(sK186(X0)) ).
cnf(u2007,axiom,
~ sP19(X0) ).
cnf(u2010,axiom,
~ p20(sK188(X0)) ).
cnf(u2013,axiom,
~ sP18(X0) ).
cnf(u2016,axiom,
~ p19(sK190(X0)) ).
cnf(u2019,axiom,
~ sP17(X0) ).
cnf(u2022,axiom,
~ p18(sK192(X0)) ).
cnf(u2025,axiom,
~ sP16(X0) ).
cnf(u2028,axiom,
~ p17(sK194(X0)) ).
cnf(u2031,axiom,
~ sP15(X0) ).
cnf(u2034,axiom,
~ p16(sK196(X0)) ).
cnf(u2037,axiom,
~ sP14(X0) ).
cnf(u2040,axiom,
~ p15(sK198(X0)) ).
cnf(u2043,axiom,
~ sP13(X0) ).
cnf(u2046,axiom,
~ p14(sK200(X0)) ).
cnf(u2049,axiom,
~ sP12(X0) ).
cnf(u2052,axiom,
~ p13(sK202(X0)) ).
cnf(u2055,axiom,
~ sP11(X0) ).
cnf(u2058,axiom,
~ p12(sK204(X0)) ).
cnf(u2061,axiom,
~ sP10(X0) ).
cnf(u2064,axiom,
~ p11(sK206(X0)) ).
cnf(u2067,axiom,
~ sP9(X0) ).
cnf(u2070,axiom,
~ p10(sK208(X0)) ).
cnf(u2073,axiom,
~ sP8(X0) ).
cnf(u2076,axiom,
~ p9(sK210(X0)) ).
cnf(u2079,axiom,
~ sP7(X0) ).
cnf(u2082,axiom,
~ p8(sK212(X0)) ).
cnf(u2085,axiom,
~ sP6(X0) ).
cnf(u2095,axiom,
~ p7(sK214(X0)) ).
cnf(u2098,axiom,
~ sP5(X0) ).
cnf(u2101,axiom,
~ p6(sK216(X0)) ).
cnf(u2104,axiom,
~ sP4(X0) ).
cnf(u2107,axiom,
~ p5(sK218(X0)) ).
cnf(u2110,axiom,
~ sP3(X0) ).
cnf(u2113,axiom,
~ p4(sK220(X0)) ).
cnf(u2116,axiom,
~ sP2(X0) ).
cnf(u2119,axiom,
~ p3(sK222(X0)) ).
cnf(u2122,axiom,
~ sP1(X0) ).
cnf(u2125,axiom,
~ p2(sK224(X0)) ).
cnf(u2128,axiom,
~ sP0(X0) ).
cnf(u2131,negated_conjecture,
~ r1(sK411,X446) ).
cnf(u2150,negated_conjecture,
~ p1(X893) ).
cnf(u2153,negated_conjecture,
~ p2(sK598(X893)) ).
cnf(u2156,negated_conjecture,
~ p2(X893) ).
cnf(u2159,negated_conjecture,
( ~ r1(sK225,X893)
| ~ p2(X893)
| ~ p2(sK598(X893))
| ~ p1(X893)
| p2(X894)
| ~ r1(X893,X894) ) ).
cnf(u2188,negated_conjecture,
~ p3(X869) ).
cnf(u2191,negated_conjecture,
~ p4(sK588(X869)) ).
cnf(u2194,negated_conjecture,
~ p4(X869) ).
cnf(u2197,negated_conjecture,
( ~ r1(sK225,X869)
| ~ p4(X869)
| ~ p4(sK588(X869))
| ~ p3(X869)
| p4(X870)
| ~ r1(X869,X870) ) ).
cnf(u2218,negated_conjecture,
~ p5(X845) ).
cnf(u2221,negated_conjecture,
~ p6(sK578(X845)) ).
cnf(u2224,negated_conjecture,
~ p6(X845) ).
cnf(u2227,negated_conjecture,
( ~ r1(sK225,X845)
| ~ p6(X845)
| ~ p6(sK578(X845))
| ~ p5(X845)
| p6(X846)
| ~ r1(X845,X846) ) ).
cnf(u2248,negated_conjecture,
~ p7(X821) ).
cnf(u2251,negated_conjecture,
~ p8(sK568(X821)) ).
cnf(u2254,negated_conjecture,
~ p8(X821) ).
cnf(u2257,negated_conjecture,
( ~ r1(sK225,X821)
| ~ p8(X821)
| ~ p8(sK568(X821))
| ~ p7(X821)
| p8(X822)
| ~ r1(X821,X822) ) ).
cnf(u2278,negated_conjecture,
~ p9(X797) ).
cnf(u2281,negated_conjecture,
~ p10(sK558(X797)) ).
cnf(u2284,negated_conjecture,
~ p10(X797) ).
cnf(u2287,negated_conjecture,
( ~ r1(sK225,X797)
| ~ p10(X797)
| ~ p10(sK558(X797))
| ~ p9(X797)
| p10(X798)
| ~ r1(X797,X798) ) ).
cnf(u2308,negated_conjecture,
~ p11(X773) ).
cnf(u2311,negated_conjecture,
~ p12(sK548(X773)) ).
cnf(u2314,negated_conjecture,
~ p12(X773) ).
cnf(u2317,negated_conjecture,
( ~ r1(sK225,X773)
| ~ p12(X773)
| ~ p12(sK548(X773))
| ~ p11(X773)
| p12(X774)
| ~ r1(X773,X774) ) ).
cnf(u2338,negated_conjecture,
~ p13(X749) ).
cnf(u2341,negated_conjecture,
~ p14(sK538(X749)) ).
cnf(u2344,negated_conjecture,
~ p14(X749) ).
cnf(u2347,negated_conjecture,
( ~ r1(sK225,X749)
| ~ p14(X749)
| ~ p14(sK538(X749))
| ~ p13(X749)
| p14(X750)
| ~ r1(X749,X750) ) ).
cnf(u2368,negated_conjecture,
~ p15(X725) ).
cnf(u2371,negated_conjecture,
~ p16(sK528(X725)) ).
cnf(u2374,negated_conjecture,
~ p16(X725) ).
cnf(u2377,negated_conjecture,
( ~ r1(sK225,X725)
| ~ p16(X725)
| ~ p16(sK528(X725))
| ~ p15(X725)
| p16(X726)
| ~ r1(X725,X726) ) ).
cnf(u2398,negated_conjecture,
~ p17(X701) ).
cnf(u2401,negated_conjecture,
~ p18(sK518(X701)) ).
cnf(u2404,negated_conjecture,
~ p18(X701) ).
cnf(u2407,negated_conjecture,
( ~ r1(sK225,X701)
| ~ p18(X701)
| ~ p18(sK518(X701))
| ~ p17(X701)
| p18(X702)
| ~ r1(X701,X702) ) ).
cnf(u2425,negated_conjecture,
~ p19(X677) ).
cnf(u2428,negated_conjecture,
~ p20(sK508(X677)) ).
cnf(u2431,negated_conjecture,
~ p20(X677) ).
cnf(u2434,negated_conjecture,
( ~ r1(sK225,X677)
| ~ p20(X677)
| ~ p20(sK508(X677))
| ~ p19(X677)
| p20(X678)
| ~ r1(X677,X678) ) ).
cnf(u2453,negated_conjecture,
~ p21(X653) ).
cnf(u2456,negated_conjecture,
~ p22(sK498(X653)) ).
cnf(u2459,negated_conjecture,
~ p22(X653) ).
cnf(u2462,negated_conjecture,
( ~ r1(sK225,X653)
| ~ p22(X653)
| ~ p22(sK498(X653))
| ~ p21(X653)
| p22(X654)
| ~ r1(X653,X654) ) ).
cnf(u2483,negated_conjecture,
~ p23(X629) ).
cnf(u2486,negated_conjecture,
~ p24(sK488(X629)) ).
cnf(u2489,negated_conjecture,
~ p24(X629) ).
cnf(u2492,negated_conjecture,
( ~ r1(sK225,X629)
| ~ p24(X629)
| ~ p24(sK488(X629))
| ~ p23(X629)
| p24(X630)
| ~ r1(X629,X630) ) ).
cnf(u2513,negated_conjecture,
~ p25(X605) ).
cnf(u2516,negated_conjecture,
~ p26(sK478(X605)) ).
cnf(u2519,negated_conjecture,
~ p26(X605) ).
cnf(u2522,negated_conjecture,
( ~ r1(sK225,X605)
| ~ p26(X605)
| ~ p26(sK478(X605))
| ~ p25(X605)
| p26(X606)
| ~ r1(X605,X606) ) ).
cnf(u2543,negated_conjecture,
~ p27(X581) ).
cnf(u2546,negated_conjecture,
~ p28(sK468(X581)) ).
cnf(u2549,negated_conjecture,
~ p28(X581) ).
cnf(u2552,negated_conjecture,
( ~ r1(sK225,X581)
| ~ p28(X581)
| ~ p28(sK468(X581))
| ~ p27(X581)
| p28(X582)
| ~ r1(X581,X582) ) ).
cnf(u2573,negated_conjecture,
~ p29(X557) ).
cnf(u2576,negated_conjecture,
~ p30(sK458(X557)) ).
cnf(u2579,negated_conjecture,
~ p30(X557) ).
cnf(u2582,negated_conjecture,
( ~ r1(sK225,X557)
| ~ p30(X557)
| ~ p30(sK458(X557))
| ~ p29(X557)
| p30(X558)
| ~ r1(X557,X558) ) ).
cnf(u2603,negated_conjecture,
~ p31(X533) ).
cnf(u2606,negated_conjecture,
~ p32(sK448(X533)) ).
cnf(u2609,negated_conjecture,
~ p32(X533) ).
cnf(u2612,negated_conjecture,
( ~ r1(sK225,X533)
| ~ p32(X533)
| ~ p32(sK448(X533))
| ~ p31(X533)
| p32(X534)
| ~ r1(X533,X534) ) ).
cnf(u2633,negated_conjecture,
~ p33(X509) ).
cnf(u2636,negated_conjecture,
~ p34(sK438(X509)) ).
cnf(u2639,negated_conjecture,
~ p34(X509) ).
cnf(u2642,negated_conjecture,
( ~ r1(sK225,X509)
| ~ p34(X509)
| ~ p34(sK438(X509))
| ~ p33(X509)
| p34(X510)
| ~ r1(X509,X510) ) ).
cnf(u2663,negated_conjecture,
~ p35(X485) ).
cnf(u2666,negated_conjecture,
~ p36(sK428(X485)) ).
cnf(u2669,negated_conjecture,
~ p36(X485) ).
cnf(u2672,negated_conjecture,
( ~ r1(sK225,X485)
| ~ p36(X485)
| ~ p36(sK428(X485))
| ~ p35(X485)
| p36(X486)
| ~ r1(X485,X486) ) ).
cnf(u2693,negated_conjecture,
~ p37(X461) ).
cnf(u2696,negated_conjecture,
~ p38(sK418(X461)) ).
cnf(u2699,negated_conjecture,
~ p38(X461) ).
cnf(u2702,negated_conjecture,
( ~ r1(sK225,X461)
| ~ p38(X461)
| ~ p38(sK418(X461))
| ~ p37(X461)
| p38(X462)
| ~ r1(X461,X462) ) ).
cnf(u2723,negated_conjecture,
~ p40(X433) ).
cnf(u2726,negated_conjecture,
~ p41(sK406(X433)) ).
cnf(u2729,negated_conjecture,
~ p41(X433) ).
cnf(u2732,negated_conjecture,
( ~ r1(sK225,X433)
| ~ p41(X433)
| ~ p41(sK406(X433))
| ~ p40(X433)
| p41(X434)
| ~ r1(X433,X434) ) ).
cnf(u2753,negated_conjecture,
~ p42(X409) ).
cnf(u2756,negated_conjecture,
~ p43(sK396(X409)) ).
cnf(u2759,negated_conjecture,
~ p43(X409) ).
cnf(u2762,negated_conjecture,
( ~ r1(sK225,X409)
| ~ p43(X409)
| ~ p43(sK396(X409))
| ~ p42(X409)
| p43(X410)
| ~ r1(X409,X410) ) ).
cnf(u2783,negated_conjecture,
~ p44(X385) ).
cnf(u2786,negated_conjecture,
~ p45(sK386(X385)) ).
cnf(u2789,negated_conjecture,
~ p45(X385) ).
cnf(u2792,negated_conjecture,
( ~ r1(sK225,X385)
| ~ p45(X385)
| ~ p45(sK386(X385))
| ~ p44(X385)
| p45(X386)
| ~ r1(X385,X386) ) ).
cnf(u2813,negated_conjecture,
~ p46(X361) ).
cnf(u2816,negated_conjecture,
~ p47(sK376(X361)) ).
cnf(u2819,negated_conjecture,
~ p47(X361) ).
cnf(u2822,negated_conjecture,
( ~ r1(sK225,X361)
| ~ p47(X361)
| ~ p47(sK376(X361))
| ~ p46(X361)
| p47(X362)
| ~ r1(X361,X362) ) ).
cnf(u2843,negated_conjecture,
~ p48(X337) ).
cnf(u2846,negated_conjecture,
~ p49(sK366(X337)) ).
cnf(u2849,negated_conjecture,
~ p49(X337) ).
cnf(u2852,negated_conjecture,
( ~ r1(sK225,X337)
| ~ p49(X337)
| ~ p49(sK366(X337))
| ~ p48(X337)
| p49(X338)
| ~ r1(X337,X338) ) ).
cnf(u2873,negated_conjecture,
~ p50(X313) ).
cnf(u2876,negated_conjecture,
~ p51(sK356(X313)) ).
cnf(u2879,negated_conjecture,
~ p51(X313) ).
cnf(u2882,negated_conjecture,
( ~ r1(sK225,X313)
| ~ p51(X313)
| ~ p51(sK356(X313))
| ~ p50(X313)
| p51(X314)
| ~ r1(X313,X314) ) ).
cnf(u2903,negated_conjecture,
~ p52(X289) ).
cnf(u2906,negated_conjecture,
~ p53(sK346(X289)) ).
cnf(u2909,negated_conjecture,
~ p53(X289) ).
cnf(u2912,negated_conjecture,
( ~ r1(sK225,X289)
| ~ p53(X289)
| ~ p53(sK346(X289))
| ~ p52(X289)
| p53(X290)
| ~ r1(X289,X290) ) ).
cnf(u2933,negated_conjecture,
~ p54(X265) ).
cnf(u2936,negated_conjecture,
~ p55(sK336(X265)) ).
cnf(u2939,negated_conjecture,
~ p55(X265) ).
cnf(u2942,negated_conjecture,
( ~ r1(sK225,X265)
| ~ p55(X265)
| ~ p55(sK336(X265))
| ~ p54(X265)
| p55(X266)
| ~ r1(X265,X266) ) ).
cnf(u2963,negated_conjecture,
~ p56(X241) ).
cnf(u2966,negated_conjecture,
~ p57(sK326(X241)) ).
cnf(u2969,negated_conjecture,
~ p57(X241) ).
cnf(u2972,negated_conjecture,
( ~ r1(sK225,X241)
| ~ p57(X241)
| ~ p57(sK326(X241))
| ~ p56(X241)
| p57(X242)
| ~ r1(X241,X242) ) ).
cnf(u2993,negated_conjecture,
~ p58(X217) ).
cnf(u2996,negated_conjecture,
~ p59(sK316(X217)) ).
cnf(u2999,negated_conjecture,
~ p59(X217) ).
cnf(u3002,negated_conjecture,
( ~ r1(sK225,X217)
| ~ p59(X217)
| ~ p59(sK316(X217))
| ~ p58(X217)
| p59(X218)
| ~ r1(X217,X218) ) ).
cnf(u3023,negated_conjecture,
~ p60(X193) ).
cnf(u3026,negated_conjecture,
~ p61(sK306(X193)) ).
cnf(u3029,negated_conjecture,
~ p61(X193) ).
cnf(u3032,negated_conjecture,
( ~ r1(sK225,X193)
| ~ p61(X193)
| ~ p61(sK306(X193))
| ~ p60(X193)
| p61(X194)
| ~ r1(X193,X194) ) ).
cnf(u3053,negated_conjecture,
~ p62(X169) ).
cnf(u3056,negated_conjecture,
~ p63(sK296(X169)) ).
cnf(u3059,negated_conjecture,
~ p63(X169) ).
cnf(u3062,negated_conjecture,
( ~ r1(sK225,X169)
| ~ p63(X169)
| ~ p63(sK296(X169))
| ~ p62(X169)
| p63(X170)
| ~ r1(X169,X170) ) ).
cnf(u3083,negated_conjecture,
~ p64(X145) ).
cnf(u3086,negated_conjecture,
~ p65(sK286(X145)) ).
cnf(u3089,negated_conjecture,
~ p65(X145) ).
cnf(u3092,negated_conjecture,
( ~ r1(sK225,X145)
| ~ p65(X145)
| ~ p65(sK286(X145))
| ~ p64(X145)
| p65(X146)
| ~ r1(X145,X146) ) ).
cnf(u3113,negated_conjecture,
~ p66(X121) ).
cnf(u3116,negated_conjecture,
~ p67(sK276(X121)) ).
cnf(u3119,negated_conjecture,
~ p67(X121) ).
cnf(u3122,negated_conjecture,
( ~ r1(sK225,X121)
| ~ p67(X121)
| ~ p67(sK276(X121))
| ~ p66(X121)
| p67(X122)
| ~ r1(X121,X122) ) ).
cnf(u3143,negated_conjecture,
~ p68(X97) ).
cnf(u3146,negated_conjecture,
~ p69(sK266(X97)) ).
cnf(u3149,negated_conjecture,
~ p69(X97) ).
cnf(u3152,negated_conjecture,
( ~ r1(sK225,X97)
| ~ p69(X97)
| ~ p69(sK266(X97))
| ~ p68(X97)
| p69(X98)
| ~ r1(X97,X98) ) ).
cnf(u3173,negated_conjecture,
~ p70(X73) ).
cnf(u3176,negated_conjecture,
~ p71(sK256(X73)) ).
cnf(u3179,negated_conjecture,
~ p71(X73) ).
cnf(u3182,negated_conjecture,
( ~ r1(sK225,X73)
| ~ p71(X73)
| ~ p71(sK256(X73))
| ~ p70(X73)
| p71(X74)
| ~ r1(X73,X74) ) ).
cnf(u3203,negated_conjecture,
~ p72(X49) ).
cnf(u3206,negated_conjecture,
~ p73(sK246(X49)) ).
cnf(u3209,negated_conjecture,
~ p73(X49) ).
cnf(u3212,negated_conjecture,
( ~ r1(sK225,X49)
| ~ p73(X49)
| ~ p73(sK246(X49))
| ~ p72(X49)
| p73(X50)
| ~ r1(X49,X50) ) ).
cnf(u3233,negated_conjecture,
~ p74(X25) ).
cnf(u3236,negated_conjecture,
~ p75(sK236(X25)) ).
cnf(u3239,negated_conjecture,
~ p75(X25) ).
cnf(u3242,negated_conjecture,
( ~ r1(sK225,X25)
| ~ p75(X25)
| ~ p75(sK236(X25))
| ~ p74(X25)
| p75(X26)
| ~ r1(X25,X26) ) ).
cnf(u3263,negated_conjecture,
~ p76(X1) ).
cnf(u3266,negated_conjecture,
~ p77(sK226(X1)) ).
cnf(u3269,negated_conjecture,
~ p77(X1) ).
cnf(u3272,negated_conjecture,
( ~ r1(sK225,X1)
| ~ p77(X1)
| ~ p77(sK226(X1))
| ~ p76(X1)
| p77(X2)
| ~ r1(X1,X2) ) ).
cnf(u339,axiom,
( ~ p70(sK90(X0))
| ~ sP67(X0) ) ).
cnf(u367,axiom,
( ~ p63(sK104(X0))
| ~ sP60(X0) ) ).
cnf(u543,axiom,
( ~ p18(sK192(X0))
| ~ sP16(X0) ) ).
cnf(u471,axiom,
( ~ p36(sK156(X0))
| ~ sP34(X0) ) ).
cnf(u587,axiom,
( ~ p7(sK214(X0))
| ~ sP5(X0) ) ).
cnf(u1145,negated_conjecture,
( ~ r1(sK411,X446)
| p20(X446) ) ).
cnf(u343,axiom,
( ~ p69(sK92(X0))
| ~ sP66(X0) ) ).
cnf(u387,axiom,
( ~ p58(sK114(X0))
| ~ sP55(X0) ) ).
cnf(u415,axiom,
( ~ p51(sK128(X0))
| ~ sP48(X0) ) ).
cnf(u519,axiom,
( ~ p24(sK180(X0))
| ~ sP22(X0) ) ).
cnf(u531,axiom,
( ~ p21(sK186(X0))
| ~ sP19(X0) ) ).
cnf(u459,axiom,
( ~ p39(sK150(X0))
| ~ sP37(X0) ) ).
cnf(u591,axiom,
( ~ p6(sK216(X0))
| ~ sP4(X0) ) ).
cnf(u331,axiom,
( ~ p72(sK86(X0))
| ~ sP69(X0) ) ).
cnf(u579,axiom,
( ~ p9(sK210(X0))
| ~ sP7(X0) ) ).
cnf(u1146,negated_conjecture,
~ p20(sK411) ).
cnf(u411,axiom,
( ~ p52(sK126(X0))
| ~ sP49(X0) ) ).
cnf(u335,axiom,
( ~ p71(sK88(X0))
| ~ sP68(X0) ) ).
cnf(u567,axiom,
( ~ p12(sK204(X0))
| ~ sP10(X0) ) ).
cnf(u495,axiom,
( ~ p30(sK168(X0))
| ~ sP28(X0) ) ).
cnf(u507,axiom,
( ~ p27(sK174(X0))
| ~ sP25(X0) ) ).
cnf(u423,axiom,
( ~ p49(sK132(X0))
| ~ sP46(X0) ) ).
cnf(u559,axiom,
( ~ p14(sK200(X0))
| ~ sP12(X0) ) ).
cnf(u379,axiom,
( ~ p60(sK110(X0))
| ~ sP57(X0) ) ).
cnf(u439,axiom,
( ~ p45(sK140(X0))
| ~ sP42(X0) ) ).
cnf(u555,axiom,
( ~ p15(sK198(X0))
| ~ sP13(X0) ) ).
cnf(u511,axiom,
( ~ p26(sK176(X0))
| ~ sP24(X0) ) ).
cnf(u483,axiom,
( ~ p33(sK162(X0))
| ~ sP31(X0) ) ).
cnf(u311,axiom,
( ~ p77(sK76(X0))
| ~ sP74(X0) ) ).
cnf(u435,axiom,
( ~ p46(sK138(X0))
| ~ sP43(X0) ) ).
cnf(u355,axiom,
( ~ p66(sK98(X0))
| ~ sP63(X0) ) ).
cnf(u383,axiom,
( ~ p59(sK112(X0))
| ~ sP56(X0) ) ).
cnf(u427,axiom,
( ~ p48(sK134(X0))
| ~ sP45(X0) ) ).
cnf(u391,axiom,
( ~ p57(sK116(X0))
| ~ sP54(X0) ) ).
cnf(u487,axiom,
( ~ p32(sK164(X0))
| ~ sP30(X0) ) ).
cnf(u547,axiom,
( ~ p17(sK194(X0))
| ~ sP15(X0) ) ).
cnf(u603,axiom,
( ~ p3(sK222(X0))
| ~ sP1(X0) ) ).
cnf(u1143,negated_conjecture,
~ p20(sK412) ).
cnf(u1147,negated_conjecture,
r1(sK225,sK411) ).
cnf(u359,axiom,
( ~ p65(sK100(X0))
| ~ sP62(X0) ) ).
cnf(u403,axiom,
( ~ p54(sK122(X0))
| ~ sP51(X0) ) ).
cnf(u431,axiom,
( ~ p47(sK136(X0))
| ~ sP44(X0) ) ).
cnf(u535,axiom,
( ~ p20(sK188(X0))
| ~ sP18(X0) ) ).
cnf(u463,axiom,
( ~ p38(sK152(X0))
| ~ sP36(X0) ) ).
cnf(u475,axiom,
( ~ p35(sK158(X0))
| ~ sP33(X0) ) ).
cnf(u607,axiom,
( ~ p2(sK224(X0))
| ~ sP0(X0) ) ).
cnf(u1142,negated_conjecture,
( ~ r1(sK412,X448)
| p20(X448) ) ).
cnf(u407,axiom,
( ~ p53(sK124(X0))
| ~ sP50(X0) ) ).
cnf(u523,axiom,
( ~ p23(sK182(X0))
| ~ sP21(X0) ) ).
cnf(u451,axiom,
( ~ p42(sK146(X0))
| ~ sP39(X0) ) ).
cnf(u583,axiom,
( ~ p8(sK212(X0))
| ~ sP6(X0) ) ).
cnf(u595,axiom,
( ~ p5(sK218(X0))
| ~ sP3(X0) ) ).
cnf(u571,axiom,
( ~ p11(sK206(X0))
| ~ sP9(X0) ) ).
cnf(u323,axiom,
( ~ p74(sK82(X0))
| ~ sP71(X0) ) ).
cnf(u1144,negated_conjecture,
r1(sK225,sK412) ).
cnf(u527,axiom,
( ~ p22(sK184(X0))
| ~ sP20(X0) ) ).
cnf(u455,axiom,
( ~ p41(sK148(X0))
| ~ sP38(X0) ) ).
cnf(u563,axiom,
( ~ p13(sK202(X0))
| ~ sP11(X0) ) ).
cnf(u327,axiom,
( ~ p73(sK84(X0))
| ~ sP70(X0) ) ).
cnf(u499,axiom,
( ~ p29(sK170(X0))
| ~ sP27(X0) ) ).
cnf(u399,axiom,
( ~ p55(sK120(X0))
| ~ sP52(X0) ) ).
cnf(u515,axiom,
( ~ p25(sK178(X0))
| ~ sP23(X0) ) ).
cnf(u371,axiom,
( ~ p62(sK106(X0))
| ~ sP59(X0) ) ).
cnf(u443,axiom,
( ~ p44(sK142(X0))
| ~ sP41(X0) ) ).
cnf(u575,axiom,
( ~ p10(sK208(X0))
| ~ sP8(X0) ) ).
cnf(u503,axiom,
( ~ p28(sK172(X0))
| ~ sP26(X0) ) ).
cnf(u315,axiom,
( ~ p76(sK78(X0))
| ~ sP73(X0) ) ).
cnf(u375,axiom,
( ~ p61(sK108(X0))
| ~ sP58(X0) ) ).
cnf(u395,axiom,
( ~ p56(sK118(X0))
| ~ sP53(X0) ) ).
cnf(u419,axiom,
( ~ p50(sK130(X0))
| ~ sP47(X0) ) ).
cnf(u447,axiom,
( ~ p43(sK144(X0))
| ~ sP40(X0) ) ).
cnf(u551,axiom,
( ~ p16(sK196(X0))
| ~ sP14(X0) ) ).
cnf(u479,axiom,
( ~ p34(sK160(X0))
| ~ sP32(X0) ) ).
cnf(u347,axiom,
( ~ p68(sK94(X0))
| ~ sP65(X0) ) ).
cnf(u491,axiom,
( ~ p31(sK166(X0))
| ~ sP29(X0) ) ).
cnf(u319,axiom,
( ~ p75(sK80(X0))
| ~ sP72(X0) ) ).
cnf(u363,axiom,
( ~ p64(sK102(X0))
| ~ sP61(X0) ) ).
cnf(u351,axiom,
( ~ p67(sK96(X0))
| ~ sP64(X0) ) ).
cnf(u539,axiom,
( ~ p19(sK190(X0))
| ~ sP17(X0) ) ).
cnf(u467,axiom,
( ~ p37(sK154(X0))
| ~ sP35(X0) ) ).
cnf(u599,axiom,
( ~ p4(sK220(X0))
| ~ sP2(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LCL645+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.03/0.31 % Computer : n012.cluster.edu
% 0.03/0.31 % Model : x86_64 x86_64
% 0.03/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.31 % Memory : 8046.5625MB
% 0.03/0.31 % OS : Linux 6.8.0-71-generic
% 0.03/0.31 % CPULimit : 300
% 0.03/0.31 % WCLimit : 300
% 0.03/0.31 % DateTime : Sun Sep 27 16:12:20 UTC 2026
% 0.03/0.32 % CPUTime :
% 0.03/0.32 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.33 Running first-order model finding
% 0.07/0.33 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.41 % (2559340)Will run a generic schedule for satisfiability detection.
% 0.07/0.41 % (2559346)% WARNING: option uhcvi not known.
% 0.07/0.41 % (2559345)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3982634200_2999 on theBenchmark for (2999ds/0Mi)
% 0.07/0.41 % (2559346)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2422324422:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.07/0.41 % (2559347)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=857442871:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.07/0.41 % (2559348)dis+10_1_sil=32000:sp=arity:random_seed=83922412:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.07/0.41 % (2559349)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3385204409:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.07/0.41 % (2559350)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3968164705:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.07/0.41 % (2559351)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2569265279:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.07/0.41 % (2559348)Instruction limit reached!
% 0.07/0.41 % (2559348)------------------------------
% 0.07/0.41 % (2559348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.07/0.41 % (2559348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.07/0.41 % (2559348)CaDiCaL version: 2.1.3
% 0.07/0.41 % (2559348)Termination reason: Instruction limit
% 0.07/0.41 % (2559348)Termination phase: Saturation
% 0.07/0.41 % (2559348)Time elapsed: 0.030 s
% 0.07/0.41 % (2559348)Peak memory usage: 16 MB
% 0.07/0.41 % (2559348)Instructions burned: 107 (million)
% 0.07/0.41 % (2559349)Instruction limit reached!
% 0.07/0.41 % (2559349)------------------------------
% 0.07/0.41 % (2559349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.07/0.41 % (2559349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.07/0.41 % (2559349)CaDiCaL version: 2.1.3
% 0.07/0.41 % (2559349)Termination reason: Instruction limit
% 0.07/0.41 % (2559349)Termination phase: Blocked clause elimination
% 0.07/0.41 % (2559349)Time elapsed: 0.034 s
% 0.07/0.41 % (2559349)Peak memory usage: 16 MB
% 0.07/0.41 % (2559349)Instructions burned: 119 (million)
% 0.07/0.41 % (2559350)Instruction limit reached!
% 0.07/0.41 % (2559350)------------------------------
% 0.07/0.41 % (2559350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.07/0.41 % (2559350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.07/0.41 % (2559350)CaDiCaL version: 2.1.3
% 0.07/0.41 % (2559350)Termination reason: Instruction limit
% 0.07/0.41 % (2559350)Termination phase: Saturation
% 0.07/0.41 % (2559350)Time elapsed: 0.037 s
% 0.07/0.41 % (2559350)Peak memory usage: 17 MB
% 0.07/0.41 % (2559350)Instructions burned: 135 (million)
% 0.07/0.41 % (2559347) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2559340-2559347"...
% 0.07/0.41 % (2559347)...printing done.
% 0.07/0.41 % SZS status CounterSatisfiable for theBenchmark
% 0.07/0.41 % SZS output start Saturation.
% See solution above
% 0.07/0.41 % SZS output start Definitions and Model Updates.
% 0.07/0.41 % SZS output end Definitions and Model Updates.
% 0.07/0.41 % (2559347)------------------------------
% 0.07/0.41 % (2559347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.07/0.41 % (2559347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.07/0.41 % (2559347)CaDiCaL version: 2.1.3
% 0.07/0.41 % (2559347)Termination reason: Satisfiable
% 0.07/0.41 % (2559347)Time elapsed: 0.040 s
% 0.07/0.41 % (2559347)Peak memory usage: 16 MB
% 0.07/0.41 % (2559347)Instructions burned: 139 (million)
% 0.07/0.41 % (2559340)Success in time 0.069 s
% 0.07/0.41 % Vampire exiting
%------------------------------------------------------------------------------