%------------------------------------------------------------------------------ % File : CSE-F---1.0 % Problem : TOP027+1 : TPTP v7.5.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n025.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:15 EDT 2022 % Result : Theorem 0.65s 0.86s % Output : CNFRefutation 0.65s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : TOP027+1 : TPTP v7.5.0. Released v3.4.0. % 0.06/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n025.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % RAMPerCPU : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Wed Mar 16 07:41:20 EDT 2022 % 0.13/0.33 % CPUTime : % 0.19/0.43 openjdk version "1.8.0_171" % 0.19/0.43 OpenJDK Runtime Environment (build 1.8.0_171-b10) % 0.19/0.43 OpenJDK 64-Bit Server VM (build 25.171-b10, mixed mode) % 0.19/0.44 file=/export/starexec/sandbox2/benchmark/theBenchmark.p % 0.57/0.66 start to proof:theBenchmark % 0.65/0.86 % Version : CSE-F---1.0 % 0.65/0.86 % Problem : theBenchmark.p % 0.65/0.86 % Proof found % 0.65/0.86 % SZS status Theorem for theBenchmark.p % 0.65/0.86 % SZS output start Proof % 0.65/0.86 [57]P1(a1) % 0.65/0.86 [58]P2(a1) % 0.65/0.86 [59]P2(a2) % 0.65/0.86 [60]P3(a11) % 0.65/0.86 [61]P3(a12) % 0.65/0.86 [62]P9(a11) % 0.65/0.86 [63]P9(a12) % 0.65/0.86 [64]P15(a11) % 0.65/0.86 [65]P15(a12) % 0.65/0.86 [66]P17(a11) % 0.65/0.86 [67]P17(a12) % 0.65/0.86 [68]P21(a11) % 0.65/0.86 [69]P21(a12) % 0.65/0.86 [70]P10(a11) % 0.65/0.86 [71]P4(a3) % 0.65/0.86 [72]P4(a5) % 0.65/0.86 [74]P11(a13,a1) % 0.65/0.86 [83]~P18(a1) % 0.65/0.86 [84]~P18(a5) % 0.65/0.86 [85]~P10(a12) % 0.65/0.86 [79]P6(a13,f22(f24(a1))) % 0.65/0.86 [80]P6(a14,f22(f24(a1))) % 0.65/0.86 [87]~E(f23(a1,f25(f24(a1),a13,f15(a1,a14))),f15(a1,a14)) % 0.65/0.86 [76]P5(x761,x761) % 0.65/0.86 [73]P10(f6(x731)) % 0.65/0.86 [75]E(f21(x751,a11),a11) % 0.65/0.86 [77]E(f21(x771,x771),x771) % 0.65/0.86 [78]P6(f9(x781),x781) % 0.65/0.86 [81]P6(f6(x811),f22(x811)) % 0.65/0.86 [86]~P10(f22(x861)) % 0.65/0.86 [82]E(f21(x821,x822),f21(x822,x821)) % 0.65/0.86 [88]~P10(x881)+E(x881,a11) % 0.65/0.86 [89]~P9(x891)+P3(x891) % 0.65/0.86 [90]~P10(x901)+P3(x901) % 0.65/0.86 [91]~P15(x911)+P9(x911) % 0.65/0.86 [92]~P10(x921)+P9(x921) % 0.65/0.86 [93]~P17(x931)+P15(x931) % 0.65/0.86 [94]~P10(x941)+P15(x941) % 0.65/0.86 [95]~P21(x951)+P17(x951) % 0.65/0.86 [96]~P10(x961)+P17(x961) % 0.65/0.86 [97]~P10(x971)+P21(x971) % 0.65/0.86 [98]~P2(x981)+P4(x981) % 0.65/0.86 [100]~P2(x1001)+P3(f16(x1001)) % 0.65/0.86 [101]~P2(x1011)+P9(f16(x1011)) % 0.65/0.86 [102]~P2(x1021)+P15(f16(x1021)) % 0.65/0.86 [103]~P2(x1031)+P17(f16(x1031)) % 0.65/0.86 [104]~P2(x1041)+P21(f16(x1041)) % 0.65/0.86 [105]~P2(x1051)+P10(f16(x1051)) % 0.65/0.86 [106]P10(x1061)+~P10(f7(x1061)) % 0.65/0.86 [113]~P2(x1131)+P16(f16(x1131),x1131) % 0.65/0.86 [117]P10(x1171)+P6(f7(x1171),f22(x1171)) % 0.65/0.86 [195]~P2(x1951)+P6(f16(x1951),f22(f24(x1951))) % 0.65/0.86 [116]~P10(x1161)+~P7(x1162,x1161) % 0.65/0.86 [143]~P7(x1431,x1432)+P6(x1431,x1432) % 0.65/0.86 [194]~P7(x1942,x1941)+~P7(x1941,x1942) % 0.65/0.86 [144]~P3(x1442)+P3(f21(x1441,x1442)) % 0.65/0.86 [145]~P3(x1451)+P3(f21(x1451,x1452)) % 0.65/0.86 [146]~P9(x1462)+P3(f21(x1461,x1462)) % 0.65/0.86 [147]~P9(x1471)+P3(f21(x1471,x1472)) % 0.65/0.86 [148]~P15(x1482)+P3(f21(x1481,x1482)) % 0.65/0.86 [149]~P15(x1491)+P3(f21(x1491,x1492)) % 0.65/0.86 [150]~P17(x1502)+P3(f21(x1501,x1502)) % 0.65/0.86 [151]~P17(x1511)+P3(f21(x1511,x1512)) % 0.65/0.86 [152]~P21(x1522)+P3(f21(x1521,x1522)) % 0.65/0.86 [153]~P21(x1531)+P3(f21(x1531,x1532)) % 0.65/0.86 [154]~P9(x1542)+P9(f21(x1541,x1542)) % 0.65/0.86 [155]~P9(x1551)+P9(f21(x1551,x1552)) % 0.65/0.86 [156]~P15(x1562)+P9(f21(x1561,x1562)) % 0.65/0.86 [157]~P15(x1571)+P9(f21(x1571,x1572)) % 0.65/0.86 [158]~P17(x1582)+P9(f21(x1581,x1582)) % 0.65/0.86 [159]~P17(x1591)+P9(f21(x1591,x1592)) % 0.65/0.86 [160]~P21(x1602)+P9(f21(x1601,x1602)) % 0.65/0.86 [161]~P21(x1611)+P9(f21(x1611,x1612)) % 0.65/0.86 [162]~P15(x1622)+P15(f21(x1621,x1622)) % 0.65/0.86 [163]~P15(x1631)+P15(f21(x1631,x1632)) % 0.65/0.86 [164]~P17(x1642)+P15(f21(x1641,x1642)) % 0.65/0.86 [165]~P17(x1651)+P15(f21(x1651,x1652)) % 0.65/0.86 [166]~P21(x1662)+P15(f21(x1661,x1662)) % 0.65/0.86 [167]~P21(x1671)+P15(f21(x1671,x1672)) % 0.65/0.86 [168]~P17(x1682)+P17(f21(x1681,x1682)) % 0.65/0.86 [169]~P17(x1691)+P17(f21(x1691,x1692)) % 0.65/0.86 [170]~P21(x1702)+P17(f21(x1701,x1702)) % 0.65/0.86 [171]~P21(x1711)+P17(f21(x1711,x1712)) % 0.65/0.86 [172]~P21(x1722)+P21(f21(x1721,x1722)) % 0.65/0.86 [173]~P21(x1731)+P21(f21(x1731,x1732)) % 0.65/0.86 [178]~P5(x1781,x1782)+P6(x1781,f22(x1782)) % 0.65/0.86 [196]P5(x1961,x1962)+~P6(x1961,f22(x1962)) % 0.65/0.86 [107]~P1(x1071)+~P2(x1071)+P3(f19(x1071)) % 0.65/0.86 [108]~P1(x1081)+~P2(x1081)+P9(f19(x1081)) % 0.65/0.86 [109]~P1(x1091)+~P2(x1091)+P15(f19(x1091)) % 0.65/0.86 [110]~P1(x1101)+~P2(x1101)+P17(f19(x1101)) % 0.65/0.86 [111]~P1(x1111)+~P2(x1111)+P21(f19(x1111)) % 0.65/0.86 [112]~P1(x1121)+~P2(x1121)+P10(f19(x1121)) % 0.65/0.86 [114]~P4(x1141)+P18(x1141)+~P10(f24(x1141)) % 0.65/0.86 [115]~P4(x1151)+P18(x1151)+~P10(f8(x1151)) % 0.65/0.86 [133]~P1(x1331)+~P2(x1331)+P20(f19(x1331),x1331) % 0.65/0.86 [134]~P1(x1341)+~P2(x1341)+P16(f19(x1341),x1341) % 0.65/0.86 [135]~P1(x1351)+~P2(x1351)+P23(f17(x1351),x1351) % 0.65/0.86 [136]~P1(x1361)+~P2(x1361)+P23(f19(x1361),x1361) % 0.65/0.86 [137]~P1(x1371)+~P2(x1371)+P23(f20(x1371),x1371) % 0.65/0.86 [138]~P1(x1381)+~P2(x1381)+P19(f17(x1381),x1381) % 0.65/0.86 [139]~P1(x1391)+~P2(x1391)+P19(f19(x1391),x1391) % 0.65/0.86 [140]~P1(x1401)+~P2(x1401)+P19(f10(x1401),x1401) % 0.65/0.86 [197]~P4(x1971)+P18(x1971)+P6(f8(x1971),f22(f24(x1971))) % 0.65/0.86 [198]~P1(x1981)+~P2(x1981)+P6(f17(x1981),f22(f24(x1981))) % 0.65/0.86 [199]~P1(x1991)+~P2(x1991)+P6(f19(x1991),f22(f24(x1991))) % 0.65/0.86 [200]~P1(x2001)+~P2(x2001)+P6(f20(x2001),f22(f24(x2001))) % 0.65/0.86 [201]~P1(x2011)+~P2(x2011)+P6(f10(x2011),f22(f24(x2011))) % 0.65/0.86 [99]~P10(x992)+~P10(x991)+E(x991,x992) % 0.65/0.86 [118]~P6(x1181,x1182)+P13(x1181)+~P3(x1182) % 0.65/0.86 [119]~P6(x1191,x1192)+P13(x1191)+~P9(x1192) % 0.65/0.86 [120]~P6(x1201,x1202)+P13(x1201)+~P15(x1202) % 0.65/0.86 [121]~P6(x1211,x1212)+P13(x1211)+~P17(x1212) % 0.65/0.86 [122]~P6(x1221,x1222)+P13(x1221)+~P21(x1222) % 0.65/0.86 [123]~P6(x1231,x1232)+P14(x1231)+~P9(x1232) % 0.65/0.86 [124]~P6(x1241,x1242)+P14(x1241)+~P15(x1242) % 0.65/0.86 [125]~P6(x1251,x1252)+P14(x1251)+~P17(x1252) % 0.65/0.86 [126]~P6(x1261,x1262)+P14(x1261)+~P21(x1262) % 0.65/0.86 [127]~P6(x1271,x1272)+P12(x1271)+~P15(x1272) % 0.65/0.86 [128]~P6(x1281,x1282)+P12(x1281)+~P17(x1282) % 0.65/0.87 [129]~P6(x1291,x1292)+P12(x1291)+~P21(x1292) % 0.65/0.87 [130]~P6(x1301,x1302)+P8(x1301)+~P17(x1302) % 0.65/0.87 [131]~P6(x1311,x1312)+P8(x1311)+~P21(x1312) % 0.65/0.87 [132]~P6(x1321,x1322)+P22(x1321)+~P21(x1322) % 0.65/0.87 [177]~P6(x1772,x1771)+P10(x1771)+P7(x1772,x1771) % 0.65/0.87 [179]P3(x1791)+~P3(x1792)+~P6(x1791,f22(x1792)) % 0.65/0.87 [180]P3(x1801)+~P9(x1802)+~P6(x1801,f22(x1802)) % 0.65/0.87 [181]P3(x1811)+~P15(x1812)+~P6(x1811,f22(x1812)) % 0.65/0.87 [182]P3(x1821)+~P17(x1822)+~P6(x1821,f22(x1822)) % 0.65/0.87 [183]P3(x1831)+~P21(x1832)+~P6(x1831,f22(x1832)) % 0.65/0.87 [184]P9(x1841)+~P9(x1842)+~P6(x1841,f22(x1842)) % 0.65/0.87 [185]P9(x1851)+~P15(x1852)+~P6(x1851,f22(x1852)) % 0.65/0.87 [186]P9(x1861)+~P17(x1862)+~P6(x1861,f22(x1862)) % 0.65/0.87 [187]P9(x1871)+~P21(x1872)+~P6(x1871,f22(x1872)) % 0.65/0.87 [188]P15(x1881)+~P15(x1882)+~P6(x1881,f22(x1882)) % 0.65/0.87 [189]P15(x1891)+~P17(x1892)+~P6(x1891,f22(x1892)) % 0.65/0.87 [190]P15(x1901)+~P21(x1902)+~P6(x1901,f22(x1902)) % 0.65/0.87 [191]P17(x1911)+~P17(x1912)+~P6(x1911,f22(x1912)) % 0.65/0.87 [192]P17(x1921)+~P21(x1922)+~P6(x1921,f22(x1922)) % 0.65/0.87 [193]P21(x1931)+~P21(x1932)+~P6(x1931,f22(x1932)) % 0.65/0.87 [224]~P2(x2241)+~P6(x2242,f22(f24(x2241)))+P6(f15(x2241,x2242),f22(f24(x2241))) % 0.65/0.87 [204]~P10(x2041)+~P7(x2042,x2043)+~P6(x2043,f22(x2041)) % 0.65/0.87 [205]P6(x2051,x2052)+~P7(x2051,x2053)+~P6(x2053,f22(x2052)) % 0.65/0.87 [225]~P6(x2252,f22(x2251))+E(f25(x2251,x2252,x2252),x2252)+~P6(x2253,f22(x2251)) % 0.65/0.87 [231]~P6(x2313,f22(x2311))+~P6(x2312,f22(x2311))+E(f25(x2311,x2312,x2313),f21(x2312,x2313)) % 0.65/0.87 [232]~P6(x2323,f22(x2321))+~P6(x2322,f22(x2321))+E(f25(x2321,x2322,x2323),f25(x2321,x2323,x2322)) % 0.65/0.87 [233]~P6(x2333,f22(x2331))+~P6(x2332,f22(x2331))+P6(f25(x2331,x2332,x2333),f22(x2331)) % 0.65/0.87 [141]~P1(x1411)+~P2(x1411)+P18(x1411)+~P10(f18(x1411)) % 0.65/0.87 [142]~P1(x1421)+~P2(x1421)+P18(x1421)+~P10(f4(x1421)) % 0.65/0.87 [174]~P1(x1741)+~P2(x1741)+P18(x1741)+P23(f18(x1741),x1741) % 0.65/0.87 [175]~P1(x1751)+~P2(x1751)+P18(x1751)+P23(f4(x1751),x1751) % 0.65/0.87 [176]~P1(x1761)+~P2(x1761)+P18(x1761)+P19(f18(x1761),x1761) % 0.65/0.87 [202]~P1(x2021)+~P2(x2021)+P18(x2021)+P6(f18(x2021),f22(f24(x2021))) % 0.65/0.87 [203]~P1(x2031)+~P2(x2031)+P18(x2031)+P6(f4(x2031),f22(f24(x2031))) % 0.65/0.87 [206]~P2(x2062)+~P10(x2061)+P16(x2061,x2062)+~P6(x2061,f22(f24(x2062))) % 0.65/0.87 [211]~P1(x2111)+~P2(x2111)+P19(f15(x2111,x2112),x2111)+~P6(x2112,f22(f24(x2111))) % 0.65/0.87 [212]~P2(x2121)+~P16(x2122,x2121)+~P6(x2122,f22(f24(x2121)))+P3(f15(x2121,x2122)) % 0.65/0.87 [213]~P2(x2131)+~P16(x2132,x2131)+~P6(x2132,f22(f24(x2131)))+P9(f15(x2131,x2132)) % 0.65/0.87 [214]~P2(x2141)+~P16(x2142,x2141)+~P6(x2142,f22(f24(x2141)))+P15(f15(x2141,x2142)) % 0.65/0.87 [215]~P2(x2151)+~P16(x2152,x2151)+~P6(x2152,f22(f24(x2151)))+P17(f15(x2151,x2152)) % 0.65/0.87 [216]~P2(x2161)+~P16(x2162,x2161)+~P6(x2162,f22(f24(x2161)))+P21(f15(x2161,x2162)) % 0.65/0.87 [217]~P2(x2171)+~P16(x2172,x2171)+~P6(x2172,f22(f24(x2171)))+P10(f15(x2171,x2172)) % 0.65/0.87 [226]~P2(x2261)+~P16(x2262,x2261)+P16(f15(x2261,x2262),x2261)+~P6(x2262,f22(f24(x2261))) % 0.65/0.87 [227]~P2(x2271)+P18(x2271)+~P6(x2272,f22(f24(x2271)))+P6(f23(x2271,x2272),f22(f24(x2271))) % 0.65/0.87 [207]~P1(x2072)+~P2(x2072)+~P10(x2071)+P20(x2071,x2072)+~P6(x2071,f22(f24(x2072))) % 0.65/0.87 [208]~P1(x2082)+~P2(x2082)+~P10(x2081)+P23(x2081,x2082)+~P6(x2081,f22(f24(x2082))) % 0.65/0.87 [209]~P1(x2092)+~P2(x2092)+~P10(x2091)+P19(x2091,x2092)+~P6(x2091,f22(f24(x2092))) % 0.65/0.87 [210]~P1(x2102)+~P2(x2102)+~P20(x2101,x2102)+P16(x2101,x2102)+~P6(x2101,f22(f24(x2102))) % 0.65/0.87 [218]~P2(x2182)+~P20(x2181,x2182)+~P19(x2181,x2182)+P3(x2181)+~P1(x2182)+~P6(x2181,f22(f24(x2182))) % 0.65/0.87 [219]~P2(x2192)+~P20(x2191,x2192)+~P19(x2191,x2192)+P9(x2191)+~P1(x2192)+~P6(x2191,f22(f24(x2192))) % 0.65/0.87 [220]~P2(x2202)+~P20(x2201,x2202)+~P19(x2201,x2202)+P15(x2201)+~P1(x2202)+~P6(x2201,f22(f24(x2202))) % 0.65/0.87 [221]~P2(x2212)+~P20(x2211,x2212)+~P19(x2211,x2212)+P17(x2211)+~P1(x2212)+~P6(x2211,f22(f24(x2212))) % 0.65/0.87 [222]~P2(x2222)+~P20(x2221,x2222)+~P19(x2221,x2222)+P21(x2221)+~P1(x2222)+~P6(x2221,f22(f24(x2222))) % 0.65/0.87 [223]~P2(x2232)+~P20(x2231,x2232)+~P19(x2231,x2232)+P10(x2231)+~P1(x2232)+~P6(x2231,f22(f24(x2232))) % 0.65/0.87 [228]~P1(x2282)+~P2(x2282)+~P16(x2281,x2282)+~P23(x2281,x2282)+P20(x2281,x2282)+~P6(x2281,f22(f24(x2282))) % 0.65/0.87 [230]~P1(x2302)+~P2(x2302)+~P20(x2301,x2302)+~P19(x2301,x2302)+P23(x2301,x2302)+~P6(x2301,f22(f24(x2302))) % 0.65/0.87 [234]P18(x2341)+~P1(x2341)+~P2(x2341)+~P11(x2342,x2341)+~P19(x2343,x2341)+~P6(x2343,f22(f24(x2341)))+~P6(x2342,f22(f24(x2341)))+E(f23(x2341,f25(f24(x2341),x2342,x2343)),x2343) % 0.65/0.87 [1]E(x11,x11) % 0.65/0.87 [2]E(x22,x21)+~E(x21,x22) % 0.65/0.87 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.65/0.87 [4]~E(x41,x42)+E(f6(x41),f6(x42)) % 0.65/0.87 [5]~E(x51,x52)+E(f21(x51,x53),f21(x52,x53)) % 0.65/0.87 [6]~E(x61,x62)+E(f21(x63,x61),f21(x63,x62)) % 0.65/0.87 [7]~E(x71,x72)+E(f24(x71),f24(x72)) % 0.65/0.87 [8]~E(x81,x82)+E(f9(x81),f9(x82)) % 0.65/0.87 [9]~E(x91,x92)+E(f25(x91,x93,x94),f25(x92,x93,x94)) % 0.65/0.87 [10]~E(x101,x102)+E(f25(x103,x101,x104),f25(x103,x102,x104)) % 0.65/0.87 [11]~E(x111,x112)+E(f25(x113,x114,x111),f25(x113,x114,x112)) % 0.65/0.87 [12]~E(x121,x122)+E(f22(x121),f22(x122)) % 0.65/0.87 [13]~E(x131,x132)+E(f15(x131,x133),f15(x132,x133)) % 0.65/0.87 [14]~E(x141,x142)+E(f15(x143,x141),f15(x143,x142)) % 0.65/0.87 [15]~E(x151,x152)+E(f23(x151,x153),f23(x152,x153)) % 0.65/0.87 [16]~E(x161,x162)+E(f23(x163,x161),f23(x163,x162)) % 0.65/0.87 [17]~E(x171,x172)+E(f4(x171),f4(x172)) % 0.65/0.87 [18]~E(x181,x182)+E(f18(x181),f18(x182)) % 0.65/0.87 [19]~E(x191,x192)+E(f19(x191),f19(x192)) % 0.65/0.87 [20]~E(x201,x202)+E(f10(x201),f10(x202)) % 0.65/0.87 [21]~E(x211,x212)+E(f20(x211),f20(x212)) % 0.65/0.87 [22]~E(x221,x222)+E(f17(x221),f17(x222)) % 0.65/0.87 [23]~E(x231,x232)+E(f8(x231),f8(x232)) % 0.65/0.87 [24]~E(x241,x242)+E(f16(x241),f16(x242)) % 0.65/0.87 [25]~E(x251,x252)+E(f7(x251),f7(x252)) % 0.65/0.87 [26]~P1(x261)+P1(x262)+~E(x261,x262) % 0.65/0.87 [27]~P2(x271)+P2(x272)+~E(x271,x272) % 0.65/0.87 [28]P6(x282,x283)+~E(x281,x282)+~P6(x281,x283) % 0.65/0.87 [29]P6(x293,x292)+~E(x291,x292)+~P6(x293,x291) % 0.65/0.87 [30]~P3(x301)+P3(x302)+~E(x301,x302) % 0.65/0.87 [31]~P15(x311)+P15(x312)+~E(x311,x312) % 0.65/0.87 [32]~P9(x321)+P9(x322)+~E(x321,x322) % 0.65/0.87 [33]~P17(x331)+P17(x332)+~E(x331,x332) % 0.65/0.87 [34]~P21(x341)+P21(x342)+~E(x341,x342) % 0.65/0.87 [35]P5(x352,x353)+~E(x351,x352)+~P5(x351,x353) % 0.65/0.87 [36]P5(x363,x362)+~E(x361,x362)+~P5(x363,x361) % 0.65/0.87 [37]~P18(x371)+P18(x372)+~E(x371,x372) % 0.65/0.87 [38]P20(x382,x383)+~E(x381,x382)+~P20(x381,x383) % 0.65/0.87 [39]P20(x393,x392)+~E(x391,x392)+~P20(x393,x391) % 0.65/0.87 [40]~P8(x401)+P8(x402)+~E(x401,x402) % 0.65/0.87 [41]P19(x412,x413)+~E(x411,x412)+~P19(x411,x413) % 0.65/0.87 [42]P19(x423,x422)+~E(x421,x422)+~P19(x423,x421) % 0.65/0.87 [43]~P10(x431)+P10(x432)+~E(x431,x432) % 0.65/0.87 [44]~P4(x441)+P4(x442)+~E(x441,x442) % 0.65/0.87 [45]P16(x452,x453)+~E(x451,x452)+~P16(x451,x453) % 0.65/0.87 [46]P16(x463,x462)+~E(x461,x462)+~P16(x463,x461) % 0.65/0.87 [47]P7(x472,x473)+~E(x471,x472)+~P7(x471,x473) % 0.65/0.87 [48]P7(x483,x482)+~E(x481,x482)+~P7(x483,x481) % 0.65/0.87 [49]P11(x492,x493)+~E(x491,x492)+~P11(x491,x493) % 0.65/0.87 [50]P11(x503,x502)+~E(x501,x502)+~P11(x503,x501) % 0.65/0.87 [51]~P12(x511)+P12(x512)+~E(x511,x512) % 0.65/0.87 [52]~P13(x521)+P13(x522)+~E(x521,x522) % 0.65/0.87 [53]P23(x532,x533)+~E(x531,x532)+~P23(x531,x533) % 0.65/0.87 [54]P23(x543,x542)+~E(x541,x542)+~P23(x543,x541) % 0.65/0.87 [55]~P14(x551)+P14(x552)+~E(x551,x552) % 0.65/0.87 [56]~P22(x561)+P22(x562)+~E(x561,x562) % 0.65/0.87 cnf(235,plain, % 0.65/0.87 (P5(a13,f24(a1))), % 0.65/0.87 inference(scs_inference,[],[79,196])). % 0.65/0.87 cnf(237,plain, % 0.65/0.87 (E(x2371,f21(x2371,x2371))), % 0.65/0.87 inference(scs_inference,[],[79,77,196,2])). % 0.65/0.87 cnf(240,plain, % 0.65/0.87 (P7(f9(a12),a12)), % 0.65/0.87 inference(scs_inference,[],[79,78,77,70,85,196,2,116,177])). % 0.65/0.87 cnf(241,plain, % 0.65/0.87 (P6(f9(x2411),x2411)), % 0.65/0.87 inference(rename_variables,[],[78])). % 0.65/0.87 cnf(243,plain, % 0.65/0.87 (P3(f9(f22(a11)))), % 0.65/0.87 inference(scs_inference,[],[79,78,241,77,60,70,85,196,2,116,177,179])). % 0.65/0.87 cnf(244,plain, % 0.65/0.87 (P6(f9(x2441),x2441)), % 0.65/0.87 inference(rename_variables,[],[78])). % 0.65/0.87 cnf(247,plain, % 0.65/0.87 (P6(f6(x2471),f22(x2471))), % 0.65/0.87 inference(rename_variables,[],[81])). % 0.65/0.87 cnf(250,plain, % 0.65/0.87 (P6(f9(x2501),x2501)), % 0.65/0.87 inference(rename_variables,[],[78])). % 0.65/0.87 cnf(253,plain, % 0.65/0.87 (P6(f6(x2531),f22(x2531))), % 0.65/0.87 inference(rename_variables,[],[81])). % 0.65/0.87 cnf(256,plain, % 0.65/0.87 (P6(f9(x2561),x2561)), % 0.65/0.87 inference(rename_variables,[],[78])). % 0.65/0.87 cnf(259,plain, % 0.65/0.87 (P6(f6(x2591),f22(x2591))), % 0.65/0.87 inference(rename_variables,[],[81])). % 0.65/0.87 cnf(262,plain, % 0.65/0.87 (P6(f9(x2621),x2621)), % 0.65/0.87 inference(rename_variables,[],[78])). % 0.65/0.87 cnf(265,plain, % 0.65/0.87 (P6(f6(x2651),f22(x2651))), % 0.65/0.87 inference(rename_variables,[],[81])). % 0.65/0.87 cnf(268,plain, % 0.65/0.87 (P6(f9(x2681),x2681)), % 0.65/0.87 inference(rename_variables,[],[78])). % 0.65/0.87 cnf(270,plain, % 0.65/0.87 (~P7(x2701,f9(f22(a11)))), % 0.65/0.87 inference(scs_inference,[],[79,78,241,244,250,256,262,268,81,247,253,259,77,60,62,64,66,68,70,85,196,2,116,177,179,180,184,185,188,189,191,192,193,204])). % 0.65/0.87 cnf(271,plain, % 0.65/0.87 (P6(f9(x2711),x2711)), % 0.65/0.87 inference(rename_variables,[],[78])). % 0.65/0.87 cnf(274,plain, % 0.65/0.87 (E(f21(x2741,x2741),x2741)), % 0.65/0.87 inference(rename_variables,[],[77])). % 0.65/0.87 cnf(275,plain, % 0.65/0.87 (P6(f9(f21(x2751,x2751)),x2751)), % 0.65/0.87 inference(scs_inference,[],[79,87,78,241,244,250,256,262,268,271,81,247,253,259,77,274,60,62,64,66,68,70,85,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29])). % 0.65/0.87 cnf(278,plain, % 0.65/0.87 (E(f21(x2781,x2781),x2781)), % 0.65/0.87 inference(rename_variables,[],[77])). % 0.65/0.87 cnf(279,plain, % 0.65/0.87 (~P10(f21(a12,a12))), % 0.65/0.87 inference(scs_inference,[],[83,79,87,78,241,244,250,256,262,268,271,81,247,253,259,77,274,278,60,62,64,66,68,70,85,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,37,43])). % 0.65/0.87 cnf(280,plain, % 0.65/0.87 (E(f21(x2801,x2801),x2801)), % 0.65/0.87 inference(rename_variables,[],[77])). % 0.65/0.87 cnf(282,plain, % 0.65/0.87 (P5(x2821,x2821)), % 0.65/0.87 inference(rename_variables,[],[76])). % 0.65/0.87 cnf(285,plain, % 0.65/0.87 (~E(a12,a11)), % 0.65/0.87 inference(scs_inference,[],[83,79,87,78,241,244,250,256,262,268,271,81,247,253,259,76,282,77,274,278,280,60,62,64,66,68,70,85,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,37,43,35,36,48])). % 0.65/0.87 cnf(286,plain, % 0.65/0.87 (P16(f6(f24(a1)),a1)), % 0.65/0.87 inference(scs_inference,[],[58,83,79,87,78,241,244,250,256,262,268,271,81,247,253,259,265,76,282,77,274,278,280,60,62,64,66,68,70,85,73,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,37,43,35,36,48,206])). % 0.65/0.87 cnf(287,plain, % 0.65/0.87 (P6(f6(x2871),f22(x2871))), % 0.65/0.87 inference(rename_variables,[],[81])). % 0.65/0.87 cnf(288,plain, % 0.65/0.87 (P10(f6(x2881))), % 0.65/0.87 inference(rename_variables,[],[73])). % 0.65/0.87 cnf(293,plain, % 0.65/0.87 (P6(f6(x2931),f22(x2931))), % 0.65/0.87 inference(rename_variables,[],[81])). % 0.65/0.87 cnf(295,plain, % 0.65/0.87 (P9(f15(a1,f6(f24(a1))))), % 0.65/0.87 inference(scs_inference,[],[57,58,83,79,87,78,241,244,250,256,262,268,271,81,247,253,259,265,287,293,76,282,77,274,278,280,60,62,64,66,68,70,85,73,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,37,43,35,36,48,206,211,212,213])). % 0.65/0.87 cnf(296,plain, % 0.65/0.87 (P6(f6(x2961),f22(x2961))), % 0.65/0.87 inference(rename_variables,[],[81])). % 0.65/0.87 cnf(299,plain, % 0.65/0.87 (P6(f6(x2991),f22(x2991))), % 0.65/0.87 inference(rename_variables,[],[81])). % 0.65/0.87 cnf(301,plain, % 0.65/0.87 (P17(f15(a1,f6(f24(a1))))), % 0.65/0.87 inference(scs_inference,[],[57,58,83,79,87,78,241,244,250,256,262,268,271,81,247,253,259,265,287,293,296,299,76,282,77,274,278,280,60,62,64,66,68,70,85,73,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,37,43,35,36,48,206,211,212,213,214,215])). % 0.65/0.87 cnf(302,plain, % 0.65/0.87 (P6(f6(x3021),f22(x3021))), % 0.65/0.87 inference(rename_variables,[],[81])). % 0.65/0.87 cnf(304,plain, % 0.65/0.87 (P21(f15(a1,f6(f24(a1))))), % 0.65/0.87 inference(scs_inference,[],[57,58,83,79,87,78,241,244,250,256,262,268,271,81,247,253,259,265,287,293,296,299,302,76,282,77,274,278,280,60,62,64,66,68,70,85,73,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,37,43,35,36,48,206,211,212,213,214,215,216])). % 0.65/0.87 cnf(305,plain, % 0.65/0.87 (P6(f6(x3051),f22(x3051))), % 0.65/0.87 inference(rename_variables,[],[81])). % 0.65/0.87 cnf(307,plain, % 0.65/0.87 (P10(f15(a1,f6(f24(a1))))), % 0.65/0.87 inference(scs_inference,[],[57,58,83,79,87,78,241,244,250,256,262,268,271,81,247,253,259,265,287,293,296,299,302,305,76,282,77,274,278,280,60,62,64,66,68,70,85,73,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,37,43,35,36,48,206,211,212,213,214,215,216,217])). % 0.65/0.87 cnf(308,plain, % 0.65/0.87 (P6(f6(x3081),f22(x3081))), % 0.65/0.87 inference(rename_variables,[],[81])). % 0.65/0.87 cnf(311,plain, % 0.65/0.87 (P6(f6(x3111),f22(x3111))), % 0.65/0.87 inference(rename_variables,[],[81])). % 0.65/0.87 cnf(313,plain, % 0.65/0.87 (P20(f6(f24(a1)),a1)), % 0.65/0.87 inference(scs_inference,[],[57,58,83,79,87,78,241,244,250,256,262,268,271,81,247,253,259,265,287,293,296,299,302,305,308,311,76,282,77,274,278,280,60,62,64,66,68,70,85,73,288,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,37,43,35,36,48,206,211,212,213,214,215,216,217,226,207])). % 0.65/0.87 cnf(314,plain, % 0.65/0.87 (P6(f6(x3141),f22(x3141))), % 0.65/0.87 inference(rename_variables,[],[81])). % 0.65/0.87 cnf(315,plain, % 0.65/0.87 (P10(f6(x3151))), % 0.65/0.87 inference(rename_variables,[],[73])). % 0.65/0.87 cnf(317,plain, % 0.65/0.87 (P23(f6(f24(a1)),a1)), % 0.65/0.87 inference(scs_inference,[],[57,58,83,79,87,78,241,244,250,256,262,268,271,81,247,253,259,265,287,293,296,299,302,305,308,311,314,76,282,77,274,278,280,60,62,64,66,68,70,85,73,288,315,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,37,43,35,36,48,206,211,212,213,214,215,216,217,226,207,208])). % 0.65/0.87 cnf(318,plain, % 0.65/0.87 (P6(f6(x3181),f22(x3181))), % 0.65/0.87 inference(rename_variables,[],[81])). % 0.65/0.87 cnf(319,plain, % 0.65/0.87 (P10(f6(x3191))), % 0.65/0.87 inference(rename_variables,[],[73])). % 0.65/0.87 cnf(321,plain, % 0.65/0.87 (P19(f6(f24(a1)),a1)), % 0.65/0.87 inference(scs_inference,[],[57,58,83,79,87,78,241,244,250,256,262,268,271,81,247,253,259,265,287,293,296,299,302,305,308,311,314,318,76,282,77,274,278,280,60,62,64,66,68,70,85,73,288,315,319,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,37,43,35,36,48,206,211,212,213,214,215,216,217,226,207,208,209])). % 0.65/0.87 cnf(360,plain, % 0.65/0.87 (E(x3601,f21(x3601,x3601))), % 0.65/0.87 inference(rename_variables,[],[237])). % 0.65/0.88 cnf(362,plain, % 0.65/0.88 (E(x3621,f21(x3621,x3621))), % 0.65/0.88 inference(rename_variables,[],[237])). % 0.65/0.88 cnf(363,plain, % 0.65/0.88 (P6(f21(a14,a14),f22(f24(a1)))), % 0.65/0.88 inference(scs_inference,[],[57,80,58,237,360,362,307,75,196,116,2,26,27,28])). % 0.65/0.88 cnf(364,plain, % 0.65/0.88 (E(x3641,f21(x3641,x3641))), % 0.65/0.88 inference(rename_variables,[],[237])). % 0.65/0.88 cnf(366,plain, % 0.65/0.88 (E(x3661,f21(x3661,x3661))), % 0.65/0.88 inference(rename_variables,[],[237])). % 0.65/0.88 cnf(368,plain, % 0.65/0.88 (E(x3681,f21(x3681,x3681))), % 0.65/0.88 inference(rename_variables,[],[237])). % 0.65/0.88 cnf(370,plain, % 0.65/0.88 (E(x3701,f21(x3701,x3701))), % 0.65/0.88 inference(rename_variables,[],[237])). % 0.65/0.88 cnf(376,plain, % 0.65/0.88 (E(x3761,f21(x3761,x3761))), % 0.65/0.88 inference(rename_variables,[],[237])). % 0.65/0.88 cnf(378,plain, % 0.65/0.88 (E(x3781,f21(x3781,x3781))), % 0.65/0.88 inference(rename_variables,[],[237])). % 0.65/0.88 cnf(380,plain, % 0.65/0.88 (E(x3801,f21(x3801,x3801))), % 0.65/0.88 inference(rename_variables,[],[237])). % 0.65/0.88 cnf(382,plain, % 0.65/0.88 (E(x3821,f21(x3821,x3821))), % 0.65/0.88 inference(rename_variables,[],[237])). % 0.65/0.88 cnf(384,plain, % 0.65/0.88 (E(x3841,f21(x3841,x3841))), % 0.65/0.88 inference(rename_variables,[],[237])). % 0.65/0.88 cnf(386,plain, % 0.65/0.88 (E(x3861,f21(x3861,x3861))), % 0.65/0.88 inference(rename_variables,[],[237])). % 0.65/0.88 cnf(388,plain, % 0.65/0.88 (E(x3881,f21(x3881,x3881))), % 0.65/0.88 inference(rename_variables,[],[237])). % 0.65/0.88 cnf(390,plain, % 0.65/0.88 (E(x3901,f21(x3901,x3901))), % 0.65/0.88 inference(rename_variables,[],[237])). % 0.65/0.88 cnf(392,plain, % 0.65/0.88 (E(x3921,f21(x3921,x3921))), % 0.65/0.88 inference(rename_variables,[],[237])). % 0.65/0.88 cnf(394,plain, % 0.65/0.88 (E(x3941,f21(x3941,x3941))), % 0.65/0.88 inference(rename_variables,[],[237])). % 0.65/0.88 cnf(396,plain, % 0.65/0.88 (P6(f6(x3961),f22(x3961))), % 0.65/0.88 inference(rename_variables,[],[81])). % 0.65/0.88 cnf(398,plain, % 0.65/0.88 (P7(f9(f21(f21(a12,a12),f21(a12,a12))),f21(a12,a12))), % 0.65/0.88 inference(scs_inference,[],[57,74,80,58,237,360,362,364,366,368,370,376,378,380,382,384,386,388,390,392,275,307,304,286,313,317,243,321,240,279,81,71,75,62,64,66,68,196,116,2,26,27,28,49,50,30,31,32,33,34,38,39,41,42,45,46,53,54,44,47,190,177])). % 0.65/0.88 cnf(405,plain, % 0.65/0.88 (P6(f6(x4051),f22(x4051))), % 0.65/0.88 inference(rename_variables,[],[81])). % 0.65/0.88 cnf(408,plain, % 0.65/0.88 (P6(f6(x4081),f22(x4081))), % 0.65/0.88 inference(rename_variables,[],[81])). % 0.65/0.88 cnf(411,plain, % 0.65/0.88 (P6(f6(x4111),f22(x4111))), % 0.65/0.88 inference(rename_variables,[],[81])). % 0.65/0.88 cnf(414,plain, % 0.65/0.88 (P6(f6(x4141),f22(x4141))), % 0.65/0.88 inference(rename_variables,[],[81])). % 0.65/0.88 cnf(421,plain, % 0.65/0.88 (E(x4211,f21(x4211,x4211))), % 0.65/0.88 inference(rename_variables,[],[237])). % 0.65/0.88 cnf(425,plain, % 0.65/0.88 (E(x4251,f21(x4251,x4251))), % 0.65/0.88 inference(rename_variables,[],[237])). % 0.65/0.88 cnf(432,plain, % 0.65/0.88 (~P6(f15(a1,a14),f22(f24(a1)))), % 0.65/0.88 inference(scs_inference,[],[57,74,80,83,87,79,58,237,360,362,364,366,368,370,376,378,380,382,384,386,388,390,392,394,421,425,275,307,304,301,270,286,313,317,295,243,321,235,240,279,78,81,396,405,408,411,414,71,285,75,77,62,64,66,68,196,116,2,26,27,28,49,50,30,31,32,33,34,38,39,41,42,45,46,53,54,44,47,190,177,179,184,191,193,204,180,3,29,43,35,36,48,211,234])). % 0.65/0.88 cnf(456,plain, % 0.65/0.88 ($false), % 0.65/0.88 inference(scs_inference,[],[80,58,432,398,363,78,73,196,116,194,205,224]), % 0.65/0.88 ['proof']). % 0.65/0.88 % SZS output end Proof % 0.65/0.88 % Total time : 0.120000 s %------------------------------------------------------------------------------