%------------------------------------------------------------------------------ % File : CSE-F---1.0 % Problem : TOP034+1 : TPTP v7.5.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n008.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Tue Mar 29 15:48:17 EDT 2022 % Result : Theorem 51.83s 51.84s % Output : CNFRefutation 51.83s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : TOP034+1 : TPTP v7.5.0. Released v3.4.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.35 % Computer : n008.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % RAMPerCPU : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Wed Mar 16 10:24:32 EDT 2022 % 0.13/0.35 % CPUTime : % 0.20/0.45 openjdk version "1.8.0_171" % 0.20/0.45 OpenJDK Runtime Environment (build 1.8.0_171-b10) % 0.20/0.46 OpenJDK 64-Bit Server VM (build 25.171-b10, mixed mode) % 0.20/0.46 file=/export/starexec/sandbox/benchmark/theBenchmark.p % 0.61/0.69 start to proof:theBenchmark % 51.83/51.84 % Version : CSE-F---1.0 % 51.83/51.84 % Problem : theBenchmark.p % 51.83/51.84 % Proof found % 51.83/51.84 % SZS status Theorem for theBenchmark.p % 51.83/51.85 % SZS output start Proof % 51.83/51.85 [98]P1(a1) % 51.83/51.85 [99]P2(a1) % 51.83/51.85 [100]P2(a12) % 51.83/51.85 [101]P3(a19) % 51.83/51.85 [102]P3(a2) % 51.83/51.85 [103]P17(a19) % 51.83/51.85 [104]P17(a2) % 51.83/51.85 [105]P26(a19) % 51.83/51.85 [106]P26(a2) % 51.83/51.85 [107]P33(a19) % 51.83/51.85 [108]P33(a2) % 51.83/51.85 [109]P39(a19) % 51.83/51.85 [110]P39(a2) % 51.83/51.85 [111]P18(a19) % 51.83/51.85 [112]P4(a20) % 51.83/51.85 [113]P4(a4) % 51.83/51.85 [115]P27(a13,a1) % 51.83/51.85 [116]P5(a13,a1) % 51.83/51.85 [122]~P34(a1) % 51.83/51.85 [123]~P34(a13) % 51.83/51.85 [124]~P34(a4) % 51.83/51.85 [125]~P18(a2) % 51.83/51.85 [127]~P11(a1,a13) % 51.83/51.85 [117]P10(x1171,x1171) % 51.83/51.85 [114]P18(f5(x1141)) % 51.83/51.85 [118]P6(f21(x1181),x1181) % 51.83/51.85 [119]P6(f5(x1191),f25(x1191)) % 51.83/51.85 [126]~P18(f25(x1261)) % 51.83/51.85 [120]P9(f24(x1201,x1202),x1201,x1202) % 51.83/51.85 [121]P7(f22(x1211,x1212),x1211,x1212) % 51.83/51.85 [128]~P18(x1281)+E(x1281,a19) % 51.83/51.85 [129]~P17(x1291)+P3(x1291) % 51.83/51.85 [130]~P18(x1301)+P3(x1301) % 51.83/51.85 [131]~P26(x1311)+P17(x1311) % 51.83/51.85 [132]~P18(x1321)+P17(x1321) % 51.83/51.85 [133]~P33(x1331)+P26(x1331) % 51.83/51.85 [134]~P18(x1341)+P26(x1341) % 51.83/51.85 [135]~P39(x1351)+P33(x1351) % 51.83/51.85 [136]~P18(x1361)+P33(x1361) % 51.83/51.85 [137]~P18(x1371)+P39(x1371) % 51.83/51.85 [138]~P2(x1381)+P4(x1381) % 51.83/51.85 [140]~P2(x1401)+P3(f9(x1401)) % 51.83/51.85 [141]~P2(x1411)+P17(f9(x1411)) % 51.83/51.85 [142]~P2(x1421)+P26(f9(x1421)) % 51.83/51.85 [143]~P2(x1431)+P33(f9(x1431)) % 51.83/51.85 [144]~P2(x1441)+P39(f9(x1441)) % 51.83/51.85 [145]~P2(x1451)+P18(f9(x1451)) % 51.83/51.85 [146]P18(x1461)+~P18(f6(x1461)) % 51.83/51.85 [155]~P2(x1551)+P5(f3(x1551),x1551) % 51.83/51.85 [156]~P2(x1561)+P8(f23(x1561),x1561) % 51.83/51.85 [157]~P2(x1571)+P29(f9(x1571),x1571) % 51.83/51.85 [164]P18(x1641)+P6(f6(x1641),f25(x1641)) % 51.83/51.85 [232]~P2(x2321)+P6(f9(x2321),f25(f26(x2321))) % 51.83/51.85 [160]~P18(x1601)+~P12(x1602,x1601) % 51.83/51.85 [192]~P12(x1921,x1922)+P6(x1921,x1922) % 51.83/51.85 [231]~P12(x2312,x2311)+~P12(x2311,x2312) % 51.83/51.85 [213]~P10(x2131,x2132)+P6(x2131,f25(x2132)) % 51.83/51.85 [233]P10(x2331,x2332)+~P6(x2331,f25(x2332)) % 51.83/51.85 [283]~P7(x2831,x2832,x2833)+P9(x2831,x2832,x2833) % 51.83/51.85 [284]~P9(x2841,x2842,x2843)+P7(x2841,x2842,x2843) % 51.83/51.85 [279]P21(x2791)+~P6(x2791,f25(f27(x2792,x2793))) % 51.83/51.85 [289]~P9(x2891,x2892,x2893)+P6(x2891,f25(f27(x2892,x2893))) % 51.83/51.85 [149]~P1(x1491)+~P2(x1491)+P3(f14(x1491)) % 51.83/51.85 [150]~P1(x1501)+~P2(x1501)+P17(f14(x1501)) % 51.83/51.85 [151]~P1(x1511)+~P2(x1511)+P26(f14(x1511)) % 51.83/51.85 [152]~P1(x1521)+~P2(x1521)+P33(f14(x1521)) % 51.83/51.85 [153]~P1(x1531)+~P2(x1531)+P39(f14(x1531)) % 51.83/51.85 [154]~P1(x1541)+~P2(x1541)+P18(f14(x1541)) % 51.83/51.85 [158]~P4(x1581)+P34(x1581)+~P18(f26(x1581)) % 51.83/51.85 [159]~P4(x1591)+P34(x1591)+~P18(f11(x1591)) % 51.83/51.85 [182]~P1(x1821)+~P2(x1821)+P36(f7(x1821),x1821) % 51.83/51.85 [183]~P1(x1831)+~P2(x1831)+P36(f8(x1831),x1831) % 51.83/51.85 [184]~P1(x1841)+~P2(x1841)+P36(f14(x1841),x1841) % 51.83/51.85 [185]~P1(x1851)+~P2(x1851)+P41(f8(x1851),x1851) % 51.83/51.85 [186]~P1(x1861)+~P2(x1861)+P41(f14(x1861),x1861) % 51.83/51.85 [187]~P1(x1871)+~P2(x1871)+P41(f15(x1871),x1871) % 51.83/51.85 [188]~P1(x1881)+~P2(x1881)+P29(f14(x1881),x1881) % 51.83/51.85 [189]~P1(x1891)+~P2(x1891)+P37(f14(x1891),x1891) % 51.83/51.85 [234]~P4(x2341)+P34(x2341)+P6(f11(x2341),f25(f26(x2341))) % 51.83/51.85 [235]~P1(x2351)+~P2(x2351)+P6(f7(x2351),f25(f26(x2351))) % 51.83/51.85 [236]~P1(x2361)+~P2(x2361)+P6(f8(x2361),f25(f26(x2361))) % 51.83/51.85 [237]~P1(x2371)+~P2(x2371)+P6(f14(x2371),f25(f26(x2371))) % 51.83/51.85 [238]~P1(x2381)+~P2(x2381)+P6(f15(x2381),f25(f26(x2381))) % 51.83/51.85 [139]~P18(x1392)+~P18(x1391)+E(x1391,x1392) % 51.83/51.85 [165]~P5(x1651,x1652)+P2(x1651)+~P2(x1652) % 51.83/51.85 [166]~P8(x1661,x1662)+P2(x1661)+~P2(x1662) % 51.83/51.85 [167]~P6(x1671,x1672)+P24(x1671)+~P3(x1672) % 51.83/51.85 [168]~P6(x1681,x1682)+P24(x1681)+~P17(x1682) % 51.83/51.85 [169]~P6(x1691,x1692)+P24(x1691)+~P26(x1692) % 51.83/51.85 [170]~P6(x1701,x1702)+P24(x1701)+~P33(x1702) % 51.83/51.85 [171]~P6(x1711,x1712)+P24(x1711)+~P39(x1712) % 51.83/51.85 [172]~P6(x1721,x1722)+P25(x1721)+~P17(x1722) % 51.83/51.85 [173]~P6(x1731,x1732)+P25(x1731)+~P26(x1732) % 51.83/51.85 [174]~P6(x1741,x1742)+P25(x1741)+~P33(x1742) % 51.83/51.85 [175]~P6(x1751,x1752)+P25(x1751)+~P39(x1752) % 51.83/51.85 [176]~P6(x1761,x1762)+P20(x1761)+~P26(x1762) % 51.83/51.85 [177]~P6(x1771,x1772)+P20(x1771)+~P33(x1772) % 51.83/51.85 [178]~P6(x1781,x1782)+P20(x1781)+~P39(x1782) % 51.83/51.85 [179]~P6(x1791,x1792)+P13(x1791)+~P33(x1792) % 51.83/51.85 [180]~P6(x1801,x1802)+P13(x1801)+~P39(x1802) % 51.83/51.85 [181]~P6(x1811,x1812)+P40(x1811)+~P39(x1812) % 51.83/51.85 [212]~P6(x2122,x2121)+P18(x2121)+P12(x2122,x2121) % 51.83/51.85 [229]~P2(x2292)+~P8(x2291,x2292)+P5(x2291,x2292) % 51.83/51.85 [230]~P2(x2302)+~P5(x2301,x2302)+P8(x2301,x2302) % 51.83/51.85 [214]P3(x2141)+~P3(x2142)+~P6(x2141,f25(x2142)) % 51.83/51.85 [215]P3(x2151)+~P17(x2152)+~P6(x2151,f25(x2152)) % 51.83/51.85 [216]P3(x2161)+~P26(x2162)+~P6(x2161,f25(x2162)) % 51.83/51.85 [217]P3(x2171)+~P33(x2172)+~P6(x2171,f25(x2172)) % 51.83/51.85 [218]P3(x2181)+~P39(x2182)+~P6(x2181,f25(x2182)) % 51.83/51.85 [219]P17(x2191)+~P17(x2192)+~P6(x2191,f25(x2192)) % 51.83/51.85 [220]P17(x2201)+~P26(x2202)+~P6(x2201,f25(x2202)) % 51.83/51.85 [221]P17(x2211)+~P33(x2212)+~P6(x2211,f25(x2212)) % 51.83/51.85 [222]P17(x2221)+~P39(x2222)+~P6(x2221,f25(x2222)) % 51.83/51.85 [223]P26(x2231)+~P26(x2232)+~P6(x2231,f25(x2232)) % 51.83/51.85 [224]P26(x2241)+~P33(x2242)+~P6(x2241,f25(x2242)) % 51.83/51.85 [225]P26(x2251)+~P39(x2252)+~P6(x2251,f25(x2252)) % 51.83/51.85 [226]P33(x2261)+~P33(x2262)+~P6(x2261,f25(x2262)) % 51.83/51.85 [227]P33(x2271)+~P39(x2272)+~P6(x2271,f25(x2272)) % 51.83/51.85 [228]P39(x2281)+~P39(x2282)+~P6(x2281,f25(x2282)) % 51.83/51.85 [239]P18(x2391)+P18(x2392)+~P18(f27(x2392,x2391)) % 51.83/51.85 [244]~P18(x2441)+~P12(x2442,x2443)+~P6(x2443,f25(x2441)) % 51.83/51.85 [248]P6(x2481,x2482)+~P12(x2481,x2483)+~P6(x2483,f25(x2482)) % 51.83/51.85 [148]P28(x1481)+~P2(x1481)+~P35(x1481)+P34(x1481) % 51.83/51.85 [190]~P1(x1901)+~P2(x1901)+P34(x1901)+~P18(f10(x1901)) % 51.83/51.85 [191]~P1(x1911)+~P2(x1911)+P34(x1911)+~P18(f16(x1911)) % 51.83/51.85 [208]~P1(x2081)+~P2(x2081)+P34(x2081)+P36(f10(x2081),x2081) % 51.83/51.85 [209]~P1(x2091)+~P2(x2091)+P34(x2091)+P41(f10(x2091),x2091) % 51.83/51.85 [210]~P1(x2101)+~P2(x2101)+P34(x2101)+P41(f16(x2101),x2101) % 51.83/51.85 [240]~P1(x2401)+~P2(x2401)+P34(x2401)+P6(f10(x2401),f25(f26(x2401))) % 51.83/51.85 [241]~P1(x2411)+~P2(x2411)+P34(x2411)+P6(f16(x2411),f25(f26(x2411))) % 51.83/51.85 [211]~P2(x2112)+~P8(x2111,x2112)+P1(x2111)+~P1(x2112) % 51.83/51.85 [254]~P2(x2542)+~P18(x2541)+P29(x2541,x2542)+~P6(x2541,f25(f26(x2542))) % 51.83/51.85 [162]P28(x1621)+~P1(x1621)+~P2(x1621)+~P19(x1621)+P34(x1621) % 51.83/51.85 [255]~P1(x2552)+~P2(x2552)+~P18(x2551)+P36(x2551,x2552)+~P6(x2551,f25(f26(x2552))) % 51.83/51.85 [256]~P1(x2562)+~P2(x2562)+~P18(x2561)+P41(x2561,x2562)+~P6(x2561,f25(f26(x2562))) % 51.83/51.85 [257]~P1(x2572)+~P2(x2572)+~P18(x2571)+P37(x2571,x2572)+~P6(x2571,f25(f26(x2572))) % 51.83/51.85 [266]~P1(x2662)+~P2(x2662)+~P37(x2661,x2662)+P29(x2661,x2662)+~P6(x2661,f25(f26(x2662))) % 51.83/51.85 [193]P19(x1931)+~P1(x1931)+~P2(x1931)+~P28(x1931)+~P35(x1931)+P34(x1931) % 51.83/51.85 [195]P19(x1951)+~P1(x1951)+~P2(x1951)+~P28(x1951)+~P30(x1951)+P34(x1951) % 51.83/51.85 [198]P19(x1981)+~P1(x1981)+~P2(x1981)+~P28(x1981)+~P38(x1981)+P34(x1981) % 51.83/51.85 [199]P19(x1991)+~P1(x1991)+~P2(x1991)+~P35(x1991)+~P38(x1991)+P34(x1991) % 51.83/51.85 [202]P35(x2021)+~P1(x2021)+~P2(x2021)+~P28(x2021)+~P30(x2021)+P34(x2021) % 51.83/51.85 [203]P38(x2031)+~P1(x2031)+~P2(x2031)+~P28(x2031)+~P30(x2031)+P34(x2031) % 51.83/51.85 [204]P42(x2041)+~P1(x2041)+~P2(x2041)+~P28(x2041)+~P30(x2041)+P34(x2041) % 51.83/51.85 [205]P42(x2051)+~P1(x2051)+~P2(x2051)+~P28(x2051)+~P38(x2051)+P34(x2051) % 51.83/51.85 [206]P43(x2061)+~P1(x2061)+~P2(x2061)+~P28(x2061)+~P30(x2061)+P34(x2061) % 51.83/51.85 [207]P43(x2071)+~P1(x2071)+~P2(x2071)+~P28(x2071)+~P38(x2071)+P34(x2071) % 51.83/51.85 [246]P28(x2462)+~P2(x2461)+~P27(x2462,x2461)+~P8(x2462,x2461)+P34(x2461)+P34(x2462) % 51.83/51.85 [253]~P1(x2531)+~P2(x2531)+~P27(x2532,x2531)+~P8(x2532,x2531)+P34(x2531)+P22(x2532,x2531) % 51.83/51.85 [273]~P2(x2732)+~P36(x2731,x2732)+~P37(x2731,x2732)+P3(x2731)+~P1(x2732)+~P6(x2731,f25(f26(x2732))) % 51.83/51.85 [274]~P2(x2742)+~P36(x2741,x2742)+~P37(x2741,x2742)+P17(x2741)+~P1(x2742)+~P6(x2741,f25(f26(x2742))) % 51.83/51.85 [275]~P2(x2752)+~P36(x2751,x2752)+~P37(x2751,x2752)+P26(x2751)+~P1(x2752)+~P6(x2751,f25(f26(x2752))) % 51.83/51.85 [276]~P2(x2762)+~P36(x2761,x2762)+~P37(x2761,x2762)+P33(x2761)+~P1(x2762)+~P6(x2761,f25(f26(x2762))) % 51.83/51.85 [277]~P2(x2772)+~P36(x2771,x2772)+~P37(x2771,x2772)+P39(x2771)+~P1(x2772)+~P6(x2771,f25(f26(x2772))) % 51.83/51.85 [278]~P2(x2782)+~P36(x2781,x2782)+~P37(x2781,x2782)+P18(x2781)+~P1(x2782)+~P6(x2781,f25(f26(x2782))) % 51.83/51.85 [280]~P1(x2802)+~P2(x2802)+~P36(x2801,x2802)+~P37(x2801,x2802)+P41(x2801,x2802)+~P6(x2801,f25(f26(x2802))) % 51.83/51.85 [282]~P1(x2822)+~P2(x2822)+~P41(x2821,x2822)+~P29(x2821,x2822)+P37(x2821,x2822)+~P6(x2821,f25(f26(x2822))) % 51.83/51.85 [242]P28(x2422)+~P1(x2421)+~P2(x2421)+~P28(x2421)+~P8(x2422,x2421)+P34(x2421)+P34(x2422) % 51.83/51.85 [269]~P1(x2691)+~P2(x2691)+~P8(x2692,x2691)+~P31(x2692,x2691)+~P14(x2692,x2691)+P34(x2691)+~P27(x2692,x2691) % 51.83/51.85 [272]~P1(x2721)+~P2(x2721)+~P8(x2722,x2721)+~P31(x2722,x2721)+~P23(x2722,x2721)+P34(x2721)+~P27(x2722,x2721) % 51.83/51.85 [264]~P1(x2642)+~P2(x2642)+~P11(x2642,x2641)+~P8(x2641,x2642)+P34(x2641)+P34(x2642)+P15(f18(x2642,x2641)) % 51.83/51.85 [265]~P1(x2652)+~P2(x2652)+~P27(x2651,x2652)+~P5(x2651,x2652)+P34(x2651)+P34(x2652)+P15(f17(x2652,x2651)) % 51.83/51.85 [285]~P1(x2852)+~P2(x2852)+~P11(x2852,x2851)+~P8(x2851,x2852)+P34(x2851)+P34(x2852)+P44(f18(x2852,x2851),x2852,x2851) % 51.83/51.85 [286]~P1(x2862)+~P2(x2862)+~P27(x2861,x2862)+~P5(x2861,x2862)+P34(x2861)+P34(x2862)+P44(f17(x2862,x2861),x2862,x2861) % 51.83/51.85 [287]~P1(x2872)+~P2(x2872)+~P11(x2872,x2871)+~P8(x2871,x2872)+P34(x2871)+P34(x2872)+P32(f18(x2872,x2871),x2872,x2871) % 51.83/51.85 [288]~P1(x2882)+~P2(x2882)+~P27(x2881,x2882)+~P5(x2881,x2882)+P34(x2881)+P34(x2882)+P32(f17(x2882,x2881),x2882,x2881) % 51.83/51.85 [290]~P1(x2902)+~P2(x2902)+~P11(x2902,x2901)+~P8(x2901,x2902)+P34(x2901)+P34(x2902)+P16(f18(x2902,x2901),f26(x2902),f26(x2901)) % 51.83/51.85 [291]~P1(x2912)+~P2(x2912)+~P27(x2911,x2912)+~P5(x2911,x2912)+P34(x2911)+P34(x2912)+P16(f17(x2912,x2911),f26(x2912),f26(x2911)) % 51.83/51.85 [292]~P1(x2922)+~P2(x2922)+~P11(x2922,x2921)+~P8(x2921,x2922)+P34(x2921)+P34(x2922)+P9(f18(x2922,x2921),f26(x2922),f26(x2921)) % 51.83/51.85 [293]~P1(x2932)+~P2(x2932)+~P27(x2931,x2932)+~P5(x2931,x2932)+P34(x2931)+P34(x2932)+P9(f17(x2932,x2931),f26(x2932),f26(x2931)) % 51.83/51.85 [250]P28(x2501)+P31(x2502,x2501)+~P1(x2501)+~P2(x2501)+~P28(x2502)+~P8(x2502,x2501)+P34(x2501)+P34(x2502) % 51.83/51.85 [251]P28(x2511)+P31(x2512,x2511)+~P1(x2511)+~P2(x2511)+~P35(x2512)+~P8(x2512,x2511)+P34(x2511)+P34(x2512) % 51.83/51.85 [294]P11(x2942,x2941)+~P1(x2942)+~P2(x2942)+~P8(x2941,x2942)+~P44(x2943,x2942,x2941)+~P32(x2943,x2942,x2941)+P34(x2941)+P34(x2942)+~P15(x2943)+~P16(x2943,f26(x2942),f26(x2941))+~P9(x2943,f26(x2942),f26(x2941)) % 51.83/51.85 [1]E(x11,x11) % 51.83/51.85 [2]E(x22,x21)+~E(x21,x22) % 51.83/51.85 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 51.83/51.85 [4]~E(x41,x42)+E(f5(x41),f5(x42)) % 51.83/51.85 [5]~E(x51,x52)+E(f21(x51),f21(x52)) % 51.83/51.85 [6]~E(x61,x62)+E(f26(x61),f26(x62)) % 51.83/51.85 [7]~E(x71,x72)+E(f25(x71),f25(x72)) % 51.83/51.85 [8]~E(x81,x82)+E(f24(x81,x83),f24(x82,x83)) % 51.83/51.85 [9]~E(x91,x92)+E(f24(x93,x91),f24(x93,x92)) % 51.83/51.85 [10]~E(x101,x102)+E(f22(x101,x103),f22(x102,x103)) % 51.83/51.85 [11]~E(x111,x112)+E(f22(x113,x111),f22(x113,x112)) % 51.83/51.85 [12]~E(x121,x122)+E(f27(x121,x123),f27(x122,x123)) % 51.83/51.85 [13]~E(x131,x132)+E(f27(x133,x131),f27(x133,x132)) % 51.83/51.85 [14]~E(x141,x142)+E(f9(x141),f9(x142)) % 51.83/51.85 [15]~E(x151,x152)+E(f11(x151),f11(x152)) % 51.83/51.85 [16]~E(x161,x162)+E(f17(x161,x163),f17(x162,x163)) % 51.83/51.85 [17]~E(x171,x172)+E(f17(x173,x171),f17(x173,x172)) % 51.83/51.85 [18]~E(x181,x182)+E(f7(x181),f7(x182)) % 51.83/51.85 [19]~E(x191,x192)+E(f18(x191,x193),f18(x192,x193)) % 51.83/51.85 [20]~E(x201,x202)+E(f18(x203,x201),f18(x203,x202)) % 51.83/51.85 [21]~E(x211,x212)+E(f8(x211),f8(x212)) % 51.83/51.86 [22]~E(x221,x222)+E(f6(x221),f6(x222)) % 51.83/51.86 [23]~E(x231,x232)+E(f14(x231),f14(x232)) % 51.83/51.86 [24]~E(x241,x242)+E(f10(x241),f10(x242)) % 51.83/51.86 [25]~E(x251,x252)+E(f15(x251),f15(x252)) % 51.83/51.86 [26]~E(x261,x262)+E(f16(x261),f16(x262)) % 51.83/51.86 [27]~E(x271,x272)+E(f23(x271),f23(x272)) % 51.83/51.86 [28]~E(x281,x282)+E(f3(x281),f3(x282)) % 51.83/51.86 [29]~P1(x291)+P1(x292)+~E(x291,x292) % 51.83/51.86 [30]~P2(x301)+P2(x302)+~E(x301,x302) % 51.83/51.86 [31]~P18(x311)+P18(x312)+~E(x311,x312) % 51.83/51.86 [32]~P3(x321)+P3(x322)+~E(x321,x322) % 51.83/51.86 [33]P41(x332,x333)+~E(x331,x332)+~P41(x331,x333) % 51.83/51.86 [34]P41(x343,x342)+~E(x341,x342)+~P41(x343,x341) % 51.83/51.86 [35]~P17(x351)+P17(x352)+~E(x351,x352) % 51.83/51.86 [36]P37(x362,x363)+~E(x361,x362)+~P37(x361,x363) % 51.83/51.86 [37]P37(x373,x372)+~E(x371,x372)+~P37(x373,x371) % 51.83/51.86 [38]~P26(x381)+P26(x382)+~E(x381,x382) % 51.83/51.86 [39]~P34(x391)+P34(x392)+~E(x391,x392) % 51.83/51.86 [40]~P33(x401)+P33(x402)+~E(x401,x402) % 51.83/51.86 [41]P6(x412,x413)+~E(x411,x412)+~P6(x411,x413) % 51.83/51.86 [42]P6(x423,x422)+~E(x421,x422)+~P6(x423,x421) % 51.83/51.86 [43]~P39(x431)+P39(x432)+~E(x431,x432) % 51.83/51.86 [44]~P30(x441)+P30(x442)+~E(x441,x442) % 51.83/51.86 [45]P29(x452,x453)+~E(x451,x452)+~P29(x451,x453) % 51.83/51.86 [46]P29(x463,x462)+~E(x461,x462)+~P29(x463,x461) % 51.83/51.86 [47]~P4(x471)+P4(x472)+~E(x471,x472) % 51.83/51.86 [48]~P19(x481)+P19(x482)+~E(x481,x482) % 51.83/51.86 [49]P14(x492,x493)+~E(x491,x492)+~P14(x491,x493) % 51.83/51.86 [50]P14(x503,x502)+~E(x501,x502)+~P14(x503,x501) % 51.83/51.86 [51]P27(x512,x513)+~E(x511,x512)+~P27(x511,x513) % 51.83/51.86 [52]P27(x523,x522)+~E(x521,x522)+~P27(x523,x521) % 51.83/51.86 [53]P5(x532,x533)+~E(x531,x532)+~P5(x531,x533) % 51.83/51.86 [54]P5(x543,x542)+~E(x541,x542)+~P5(x543,x541) % 51.83/51.86 [55]P10(x552,x553)+~E(x551,x552)+~P10(x551,x553) % 51.83/51.86 [56]P10(x563,x562)+~E(x561,x562)+~P10(x563,x561) % 51.83/51.86 [57]~P28(x571)+P28(x572)+~E(x571,x572) % 51.83/51.86 [58]P23(x582,x583)+~E(x581,x582)+~P23(x581,x583) % 51.83/51.86 [59]P23(x593,x592)+~E(x591,x592)+~P23(x593,x591) % 51.83/51.86 [60]P9(x602,x603,x604)+~E(x601,x602)+~P9(x601,x603,x604) % 51.83/51.86 [61]P9(x613,x612,x614)+~E(x611,x612)+~P9(x613,x611,x614) % 51.83/51.86 [62]P9(x623,x624,x622)+~E(x621,x622)+~P9(x623,x624,x621) % 51.83/51.86 [63]P7(x632,x633,x634)+~E(x631,x632)+~P7(x631,x633,x634) % 51.83/51.86 [64]P7(x643,x642,x644)+~E(x641,x642)+~P7(x643,x641,x644) % 51.83/51.86 [65]P7(x653,x654,x652)+~E(x651,x652)+~P7(x653,x654,x651) % 51.83/51.86 [66]P8(x662,x663)+~E(x661,x662)+~P8(x661,x663) % 51.83/51.86 [67]P8(x673,x672)+~E(x671,x672)+~P8(x673,x671) % 51.83/51.86 [68]~P35(x681)+P35(x682)+~E(x681,x682) % 51.83/51.86 [69]~P15(x691)+P15(x692)+~E(x691,x692) % 51.83/51.86 [70]P36(x702,x703)+~E(x701,x702)+~P36(x701,x703) % 51.83/51.86 [71]P36(x713,x712)+~E(x711,x712)+~P36(x713,x711) % 51.83/51.86 [72]~P43(x721)+P43(x722)+~E(x721,x722) % 51.83/51.86 [73]P11(x732,x733)+~E(x731,x732)+~P11(x731,x733) % 51.83/51.86 [74]P11(x743,x742)+~E(x741,x742)+~P11(x743,x741) % 51.83/51.86 [75]P31(x752,x753)+~E(x751,x752)+~P31(x751,x753) % 51.83/51.86 [76]P31(x763,x762)+~E(x761,x762)+~P31(x763,x761) % 51.83/51.86 [77]~P25(x771)+P25(x772)+~E(x771,x772) % 51.83/51.86 [78]~P21(x781)+P21(x782)+~E(x781,x782) % 51.83/51.86 [79]~P38(x791)+P38(x792)+~E(x791,x792) % 51.83/51.86 [80]P12(x802,x803)+~E(x801,x802)+~P12(x801,x803) % 51.83/51.86 [81]P12(x813,x812)+~E(x811,x812)+~P12(x813,x811) % 51.83/51.86 [82]P22(x822,x823)+~E(x821,x822)+~P22(x821,x823) % 51.83/51.86 [83]P22(x833,x832)+~E(x831,x832)+~P22(x833,x831) % 51.83/51.86 [84]P16(x842,x843,x844)+~E(x841,x842)+~P16(x841,x843,x844) % 51.83/51.86 [85]P16(x853,x852,x854)+~E(x851,x852)+~P16(x853,x851,x854) % 51.83/51.86 [86]P16(x863,x864,x862)+~E(x861,x862)+~P16(x863,x864,x861) % 51.83/51.86 [87]P44(x872,x873,x874)+~E(x871,x872)+~P44(x871,x873,x874) % 51.83/51.86 [88]P44(x883,x882,x884)+~E(x881,x882)+~P44(x883,x881,x884) % 51.83/51.86 [89]P44(x893,x894,x892)+~E(x891,x892)+~P44(x893,x894,x891) % 51.83/51.86 [90]~P20(x901)+P20(x902)+~E(x901,x902) % 51.83/51.86 [91]P32(x912,x913,x914)+~E(x911,x912)+~P32(x911,x913,x914) % 51.83/51.86 [92]P32(x923,x922,x924)+~E(x921,x922)+~P32(x923,x921,x924) % 51.83/51.86 [93]P32(x933,x934,x932)+~E(x931,x932)+~P32(x933,x934,x931) % 51.83/51.86 [94]~P13(x941)+P13(x942)+~E(x941,x942) % 51.83/51.86 [95]~P24(x951)+P24(x952)+~E(x951,x952) % 51.83/51.86 [96]~P40(x961)+P40(x962)+~E(x961,x962) % 51.83/51.86 [97]~P42(x971)+P42(x972)+~E(x971,x972) % 51.83/51.86 cnf(297,plain, % 51.83/51.86 (P10(f21(f25(x2971)),x2971)), % 51.83/51.86 inference(scs_inference,[],[118,111,160,233])). % 51.83/51.86 cnf(298,plain, % 51.83/51.86 (P6(f21(x2981),x2981)), % 51.83/51.86 inference(rename_variables,[],[118])). % 51.83/51.86 cnf(301,plain, % 51.83/51.86 (P6(f21(x3011),x3011)), % 51.83/51.86 inference(rename_variables,[],[118])). % 51.83/51.86 cnf(303,plain, % 51.83/51.86 (P12(f21(a2),a2)), % 51.83/51.86 inference(scs_inference,[],[118,298,301,111,125,160,233,279,212])). % 51.83/51.86 cnf(304,plain, % 51.83/51.86 (P6(f21(x3041),x3041)), % 51.83/51.86 inference(rename_variables,[],[118])). % 51.83/51.86 cnf(307,plain, % 51.83/51.86 (P6(f21(x3071),x3071)), % 51.83/51.86 inference(rename_variables,[],[118])). % 51.83/51.86 cnf(310,plain, % 51.83/51.86 (P6(f5(x3101),f25(x3101))), % 51.83/51.86 inference(rename_variables,[],[119])). % 51.83/51.86 cnf(313,plain, % 51.83/51.86 (P6(f21(x3131),x3131)), % 51.83/51.86 inference(rename_variables,[],[118])). % 51.83/51.86 cnf(316,plain, % 51.83/51.86 (P6(f5(x3161),f25(x3161))), % 51.83/51.86 inference(rename_variables,[],[119])). % 51.83/51.86 cnf(319,plain, % 51.83/51.86 (P6(f21(x3191),x3191)), % 51.83/51.86 inference(rename_variables,[],[118])). % 51.83/51.86 cnf(322,plain, % 51.83/51.86 (P6(f5(x3221),f25(x3221))), % 51.83/51.86 inference(rename_variables,[],[119])). % 51.83/51.86 cnf(325,plain, % 51.83/51.86 (P6(f21(x3251),x3251)), % 51.83/51.86 inference(rename_variables,[],[118])). % 51.83/51.86 cnf(328,plain, % 51.83/51.86 (P6(f5(x3281),f25(x3281))), % 51.83/51.86 inference(rename_variables,[],[119])). % 51.83/51.86 cnf(331,plain, % 51.83/51.86 (P6(f21(x3311),x3311)), % 51.83/51.86 inference(rename_variables,[],[118])). % 51.83/51.86 cnf(333,plain, % 51.83/51.86 (~P12(x3331,f21(f25(a19)))), % 51.83/51.86 inference(scs_inference,[],[118,298,301,304,307,313,319,325,331,119,310,316,322,111,125,101,103,105,107,109,160,233,279,212,214,215,219,220,223,224,226,227,228,244])). % 51.83/51.86 cnf(337,plain, % 51.83/51.86 (P29(f5(f26(a1)),a1)), % 51.83/51.86 inference(scs_inference,[],[99,118,298,301,304,307,313,319,325,331,119,310,316,322,328,111,125,114,101,103,105,107,109,160,233,279,212,214,215,219,220,223,224,226,227,228,244,81,254])). % 51.83/51.86 cnf(338,plain, % 51.83/51.86 (P6(f5(x3381),f25(x3381))), % 51.83/51.86 inference(rename_variables,[],[119])). % 51.83/51.86 cnf(339,plain, % 51.83/51.86 (P18(f5(x3391))), % 51.83/51.86 inference(rename_variables,[],[114])). % 51.83/51.86 cnf(342,plain, % 51.83/51.86 (P6(f5(x3421),f25(x3421))), % 51.83/51.86 inference(rename_variables,[],[119])). % 51.83/51.86 cnf(343,plain, % 51.83/51.86 (P18(f5(x3431))), % 51.83/51.86 inference(rename_variables,[],[114])). % 51.83/51.86 cnf(345,plain, % 51.83/51.86 (P41(f5(f26(a1)),a1)), % 51.83/51.86 inference(scs_inference,[],[98,99,118,298,301,304,307,313,319,325,331,119,310,316,322,328,338,342,111,125,114,339,343,101,103,105,107,109,160,233,279,212,214,215,219,220,223,224,226,227,228,244,81,254,255,256])). % 51.83/51.86 cnf(346,plain, % 51.83/51.86 (P6(f5(x3461),f25(x3461))), % 51.83/51.86 inference(rename_variables,[],[119])). % 51.83/51.86 cnf(347,plain, % 51.83/51.86 (P18(f5(x3471))), % 51.83/51.86 inference(rename_variables,[],[114])). % 51.83/51.86 cnf(349,plain, % 51.83/51.86 (P37(f5(f26(a1)),a1)), % 51.83/51.86 inference(scs_inference,[],[98,99,118,298,301,304,307,313,319,325,331,119,310,316,322,328,338,342,346,111,125,114,339,343,347,101,103,105,107,109,160,233,279,212,214,215,219,220,223,224,226,227,228,244,81,254,255,256,257])). % 51.83/51.86 cnf(350,plain, % 51.83/51.86 (P6(f5(x3501),f25(x3501))), % 51.83/51.86 inference(rename_variables,[],[119])). % 51.83/51.86 cnf(354,plain, % 51.83/51.86 (P6(f5(x3541),f25(x3541))), % 51.83/51.86 inference(rename_variables,[],[119])). % 51.83/51.86 cnf(357,plain, % 51.83/51.86 (P6(f5(x3571),f25(x3571))), % 51.83/51.86 inference(rename_variables,[],[119])). % 51.83/51.86 cnf(359,plain, % 51.83/51.86 (P26(f5(f26(a1)))), % 51.83/51.86 inference(scs_inference,[],[98,99,118,298,301,304,307,313,319,325,331,119,310,316,322,328,338,342,346,350,354,357,111,125,114,339,343,347,101,103,105,107,109,160,233,279,212,214,215,219,220,223,224,226,227,228,244,81,254,255,256,257,273,274,275])). % 51.83/51.86 cnf(360,plain, % 51.83/51.86 (P6(f5(x3601),f25(x3601))), % 51.83/51.86 inference(rename_variables,[],[119])). % 51.83/51.86 cnf(362,plain, % 51.83/51.86 (P33(f5(f26(a1)))), % 51.83/51.86 inference(scs_inference,[],[98,99,118,298,301,304,307,313,319,325,331,119,310,316,322,328,338,342,346,350,354,357,360,111,125,114,339,343,347,101,103,105,107,109,160,233,279,212,214,215,219,220,223,224,226,227,228,244,81,254,255,256,257,273,274,275,276])). % 51.83/51.86 cnf(363,plain, % 51.83/51.86 (P6(f5(x3631),f25(x3631))), % 51.83/51.86 inference(rename_variables,[],[119])). % 51.83/51.86 cnf(365,plain, % 51.83/51.86 (P39(f5(f26(a1)))), % 51.83/51.86 inference(scs_inference,[],[98,99,118,298,301,304,307,313,319,325,331,119,310,316,322,328,338,342,346,350,354,357,360,363,111,125,114,339,343,347,101,103,105,107,109,160,233,279,212,214,215,219,220,223,224,226,227,228,244,81,254,255,256,257,273,274,275,276,277])). % 51.83/51.86 cnf(383,plain, % 51.83/51.86 (~P12(x3831,f5(x3832))), % 51.83/51.86 inference(scs_inference,[],[114,160])). % 51.83/51.86 cnf(385,plain, % 51.83/51.86 (P10(f5(x3851),x3851)), % 51.83/51.86 inference(scs_inference,[],[119,114,160,233])). % 51.83/51.86 cnf(387,plain, % 51.83/51.86 (P21(f5(f27(x3871,x3872)))), % 51.83/51.86 inference(scs_inference,[],[119,114,160,233,279])). % 51.83/51.86 cnf(388,plain, % 51.83/51.86 (P6(f5(x3881),f25(x3881))), % 51.83/51.86 inference(rename_variables,[],[119])). % 51.83/51.86 cnf(391,plain, % 51.83/51.86 (P6(f5(x3911),f25(x3911))), % 51.83/51.86 inference(rename_variables,[],[119])). % 51.83/51.86 cnf(394,plain, % 51.83/51.86 (P6(f5(x3941),f25(x3941))), % 51.83/51.86 inference(rename_variables,[],[119])). % 51.83/51.86 cnf(397,plain, % 51.83/51.86 (P6(f5(x3971),f25(x3971))), % 51.83/51.86 inference(rename_variables,[],[119])). % 51.83/51.86 cnf(399,plain, % 51.83/51.86 (P12(f21(f25(x3991)),f25(x3991))), % 51.83/51.86 inference(scs_inference,[],[359,362,365,126,118,119,388,391,394,114,160,233,279,216,221,225,212])). % 51.83/51.86 cnf(400,plain, % 51.83/51.86 (P6(f21(x4001),x4001)), % 51.83/51.86 inference(rename_variables,[],[118])). % 51.83/51.86 cnf(403,plain, % 51.83/51.86 (P6(f5(x4031),f25(x4031))), % 51.83/51.86 inference(rename_variables,[],[119])). % 51.83/51.86 cnf(408,plain, % 51.83/51.86 (~P12(x4081,f21(f25(f5(x4082))))), % 51.83/51.86 inference(scs_inference,[],[359,362,365,126,118,400,119,388,391,394,397,403,114,160,233,279,216,221,225,212,226,228,244])). % 51.83/51.86 cnf(409,plain, % 51.83/51.86 (P6(f21(x4091),x4091)), % 51.83/51.86 inference(rename_variables,[],[118])). % 51.83/51.86 cnf(413,plain, % 51.83/51.86 (~P12(f25(x4131),f21(f25(x4131)))), % 51.83/51.86 inference(scs_inference,[],[359,362,365,333,303,126,118,400,119,388,391,394,397,403,114,160,233,279,216,221,225,212,226,228,244,81,231])). % 51.83/51.86 cnf(419,plain, % 51.83/51.86 (P6(f21(x4191),x4192)+~E(x4191,x4192)), % 51.83/51.86 inference(scs_inference,[],[345,349,359,362,365,333,303,126,118,400,409,119,388,391,394,397,403,114,160,233,279,216,221,225,212,226,228,244,81,231,34,36,37,41,42])). % 51.83/51.86 cnf(431,plain, % 51.83/51.86 (P9(f24(x4311,x4312),x4313,x4312)+~E(x4311,x4313)), % 51.83/51.86 inference(scs_inference,[],[337,399,383,120,81,46,60,61])). % 51.83/51.86 cnf(432,plain, % 51.83/51.86 (P9(f24(x4321,x4322),x4321,x4323)+~E(x4322,x4323)), % 51.83/51.86 inference(scs_inference,[],[337,399,383,120,81,46,60,61,62])). % 51.83/51.86 cnf(447,plain, % 51.83/51.86 (P10(f5(x4471),x4472)+~E(x4471,x4472)), % 51.83/51.86 inference(scs_inference,[],[119,399,126,385,408,212,81,55,56])). % 51.83/51.86 cnf(449,plain, % 51.83/51.86 (P7(f22(x4491,x4492),x4493,x4492)+~E(x4491,x4493)), % 51.83/51.86 inference(scs_inference,[],[119,399,126,385,408,121,212,81,55,56,63,64])). % 51.83/51.86 cnf(450,plain, % 51.83/51.86 (P7(f22(x4501,x4502),x4501,x4503)+~E(x4502,x4503)), % 51.83/51.86 inference(scs_inference,[],[119,399,126,385,408,121,212,81,55,56,63,64,65])). % 51.83/51.86 cnf(491,plain, % 51.83/51.86 (P10(f21(f25(x4911)),x4912)+~E(x4911,x4912)), % 51.83/51.86 inference(scs_inference,[],[303,297,408,81,55,56])). % 51.83/51.86 cnf(505,plain, % 51.83/51.86 (P10(x5051,x5052)+~E(x5052,x5051)), % 51.83/51.86 inference(scs_inference,[],[399,333,117,81,55])). % 51.83/51.86 cnf(506,plain, % 51.83/51.86 (P10(x5061,x5062)+~E(x5061,x5062)), % 51.83/51.86 inference(scs_inference,[],[399,333,117,81,55,56])). % 51.83/51.86 cnf(903,plain, % 51.83/51.86 (E(f9(a1),a19)), % 51.83/51.86 inference(scs_inference,[],[99,128,145])). % 51.83/51.86 cnf(913,plain, % 51.83/51.86 (E(a19,f9(a1))), % 51.83/51.86 inference(scs_inference,[],[903,419,431,432,447,449,450,491,505,506,2])). % 51.83/51.86 cnf(914,plain, % 51.83/51.86 (P18(f9(a1))), % 51.83/51.86 inference(scs_inference,[],[111,903,419,431,432,447,449,450,491,505,506,2,31])). % 51.83/51.86 cnf(930,plain, % 51.83/51.86 (P9(f24(a19,x9301),f9(a1),x9301)), % 51.83/51.86 inference(scs_inference,[],[913,419,431])). % 51.83/51.86 cnf(1236,plain, % 51.83/51.86 (~P18(f6(a2))), % 51.83/51.86 inference(scs_inference,[],[303,146,160])). % 51.83/51.86 cnf(4199,plain, % 51.83/51.86 (P6(f5(f9(a1)),f25(a19))), % 51.83/51.86 inference(scs_inference,[],[903,213,447])). % 51.83/51.86 cnf(4550,plain, % 51.83/51.86 (P12(f5(f9(a1)),f25(a19))), % 51.83/51.86 inference(scs_inference,[],[108,4199,118,126,226,212])). % 51.83/51.86 cnf(4709,plain, % 51.83/51.86 (E(f9(a19),f9(f9(a1)))), % 51.83/51.86 inference(scs_inference,[],[903,14,2])). % 51.83/51.86 cnf(4710,plain, % 51.83/51.86 (P10(f9(f9(a1)),f9(a19))), % 51.83/51.86 inference(scs_inference,[],[4709,505])). % 51.83/51.86 cnf(4717,plain, % 51.83/51.86 (E(f9(f9(a1)),f9(a19))), % 51.83/51.86 inference(scs_inference,[],[4709,505,506,431,432,449,450,419,2])). % 51.83/51.86 cnf(4750,plain, % 51.83/51.86 (P7(f22(f9(f9(a1)),x47501),f9(a19),x47501)), % 51.83/51.86 inference(scs_inference,[],[4717,431,432,449])). % 51.83/51.86 cnf(4755,plain, % 51.83/51.86 (P9(f24(f9(a1),f9(f9(a1))),a19,f9(a19))), % 51.83/51.86 inference(scs_inference,[],[903,4717,431,432,449,450,419,62,65,61])). % 51.83/51.86 cnf(6675,plain, % 51.83/51.86 (P6(f21(x66751),x66751)), % 51.83/51.86 inference(rename_variables,[],[118])). % 51.83/51.86 cnf(6687,plain, % 51.83/51.86 (P6(f21(x66871),x66871)), % 51.83/51.86 inference(rename_variables,[],[118])). % 51.83/51.86 cnf(6728,plain, % 51.83/51.86 ($false), % 51.83/51.86 inference(scs_inference,[],[98,127,113,124,413,387,4710,4550,1236,4750,4755,930,914,333,114,123,116,913,118,6675,6687,99,115,122,100,146,155,156,157,213,283,284,164,15,18,21,23,24,25,26,27,28,232,289,8,9,10,11,12,13,16,17,19,20,132,134,136,137,145,130,140,143,141,142,144,128,6,22,4,5,7,149,150,151,152,153,154,158,159,229,182,183,184,185,186,187,188,189,239,234,235,236,237,238,175,165,166,244,230,212,80,78,41,42,31,190,191,208,209,210,240,241,211,256,257,255,265,286,288,291,293,294]), % 51.83/51.86 ['proof']). % 51.83/51.86 % SZS output end Proof % 51.83/51.86 % Total time : 51.080000 s %------------------------------------------------------------------------------