%------------------------------------------------------------------------------ % File : CSE-F---1.0 % Problem : TOP023+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 : n026.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:13 EDT 2022 % Result : Theorem 52.58s 52.65s % Output : CNFRefutation 52.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : TOP023+1 : TPTP v7.5.0. Released v3.4.0. % 0.06/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n026.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:19:24 EDT 2022 % 0.13/0.34 % CPUTime : % 0.19/0.44 openjdk version "1.8.0_171" % 0.19/0.44 OpenJDK Runtime Environment (build 1.8.0_171-b10) % 0.19/0.44 OpenJDK 64-Bit Server VM (build 25.171-b10, mixed mode) % 0.19/0.45 file=/export/starexec/sandbox2/benchmark/theBenchmark.p % 0.53/0.68 start to proof:theBenchmark % 52.58/52.65 % Version : CSE-F---1.0 % 52.58/52.65 % Problem : theBenchmark.p % 52.58/52.65 % Proof found % 52.58/52.65 % SZS status Theorem for theBenchmark.p % 52.58/52.65 % SZS output start Proof % 52.58/52.65 [41]E(a1,a2) % 52.58/52.65 [42]P1(a3) % 52.58/52.65 [43]P1(a8) % 52.58/52.66 [44]P1(a9) % 52.58/52.66 [45]P1(a4) % 52.58/52.66 [46]P2(a4) % 52.58/52.66 [47]P3(a11) % 52.58/52.66 [48]P3(a12) % 52.58/52.66 [49]P9(a11) % 52.58/52.66 [50]P9(a12) % 52.58/52.66 [51]P16(a11) % 52.58/52.66 [52]P16(a12) % 52.58/52.66 [53]P18(a11) % 52.58/52.66 [54]P18(a12) % 52.58/52.66 [55]P19(a11) % 52.58/52.66 [56]P19(a12) % 52.58/52.66 [57]P10(a11) % 52.58/52.66 [58]P4(a13) % 52.58/52.66 [60]P11(a2,a3) % 52.58/52.66 [67]~P10(a12) % 52.58/52.66 [69]~P11(a1,a8) % 52.58/52.66 [63]P6(a2,f17(f16(a3))) % 52.58/52.66 [64]P6(a1,f17(f16(a8))) % 52.58/52.66 [66]E(f15(f16(a8),f18(a8)),f15(f16(a3),f18(a3))) % 52.58/52.66 [61]P5(x611,x611) % 52.58/52.66 [59]P10(f5(x591)) % 52.58/52.66 [62]P6(f14(x621),x621) % 52.58/52.66 [65]P6(f5(x651),f17(x651)) % 52.58/52.66 [68]~P10(f17(x681)) % 52.58/52.66 [70]~P10(x701)+E(x701,a11) % 52.58/52.66 [71]~P9(x711)+P3(x711) % 52.58/52.66 [72]~P10(x721)+P3(x721) % 52.58/52.66 [73]~P16(x731)+P9(x731) % 52.58/52.66 [74]~P10(x741)+P9(x741) % 52.58/52.66 [75]~P18(x751)+P16(x751) % 52.58/52.66 [76]~P10(x761)+P16(x761) % 52.58/52.66 [77]~P19(x771)+P18(x771) % 52.58/52.66 [78]~P10(x781)+P18(x781) % 52.58/52.66 [79]~P10(x791)+P19(x791) % 52.58/52.66 [80]~P1(x801)+P4(x801) % 52.58/52.66 [82]~P1(x821)+P3(f7(x821)) % 52.58/52.66 [83]~P1(x831)+P9(f7(x831)) % 52.58/52.66 [84]~P1(x841)+P16(f7(x841)) % 52.58/52.66 [85]~P1(x851)+P18(f7(x851)) % 52.58/52.66 [86]~P1(x861)+P19(f7(x861)) % 52.58/52.66 [87]~P1(x871)+P10(f7(x871)) % 52.58/52.66 [88]P10(x881)+~P10(f6(x881)) % 52.58/52.66 [89]~P1(x891)+P17(f7(x891),x891) % 52.58/52.66 [91]P10(x911)+P6(f6(x911),f17(x911)) % 52.58/52.66 [127]~P1(x1271)+P6(f7(x1271),f17(f16(x1271))) % 52.58/52.66 [131]~P1(x1311)+P6(f18(x1311),f17(f17(f16(x1311)))) % 52.58/52.66 [90]~P10(x901)+~P7(x902,x901) % 52.58/52.66 [107]~P7(x1071,x1072)+P6(x1071,x1072) % 52.58/52.66 [126]~P7(x1262,x1261)+~P7(x1261,x1262) % 52.58/52.66 [110]~P5(x1101,x1102)+P6(x1101,f17(x1102)) % 52.58/52.66 [128]P5(x1281,x1282)+~P6(x1281,f17(x1282)) % 52.58/52.66 [133]~P6(x1332,f17(f17(x1331)))+P1(f15(x1331,x1332)) % 52.58/52.66 [134]~P6(x1342,f17(f17(x1341)))+P2(f15(x1341,x1342)) % 52.58/52.66 [109]~P1(x1091)+~P2(x1091)+E(f15(f16(x1091),f18(x1091)),x1091) % 52.58/52.66 [81]~P10(x812)+~P10(x811)+E(x811,x812) % 52.58/52.66 [92]~P6(x921,x922)+P14(x921)+~P3(x922) % 52.58/52.66 [93]~P6(x931,x932)+P14(x931)+~P9(x932) % 52.58/52.66 [94]~P6(x941,x942)+P14(x941)+~P16(x942) % 52.58/52.66 [95]~P6(x951,x952)+P14(x951)+~P18(x952) % 52.58/52.66 [96]~P6(x961,x962)+P14(x961)+~P19(x962) % 52.58/52.66 [97]~P6(x971,x972)+P15(x971)+~P9(x972) % 52.58/52.66 [98]~P6(x981,x982)+P15(x981)+~P16(x982) % 52.58/52.66 [99]~P6(x991,x992)+P15(x991)+~P18(x992) % 52.58/52.66 [100]~P6(x1001,x1002)+P15(x1001)+~P19(x1002) % 52.58/52.66 [101]~P6(x1011,x1012)+P12(x1011)+~P16(x1012) % 52.58/52.66 [102]~P6(x1021,x1022)+P12(x1021)+~P18(x1022) % 52.58/52.66 [103]~P6(x1031,x1032)+P12(x1031)+~P19(x1032) % 52.58/52.66 [104]~P6(x1041,x1042)+P8(x1041)+~P18(x1042) % 52.58/52.66 [105]~P6(x1051,x1052)+P8(x1051)+~P19(x1052) % 52.58/52.66 [106]~P6(x1061,x1062)+P20(x1061)+~P19(x1062) % 52.58/52.66 [108]~P6(x1082,x1081)+P10(x1081)+P7(x1082,x1081) % 52.58/52.66 [111]P3(x1111)+~P3(x1112)+~P6(x1111,f17(x1112)) % 52.58/52.66 [112]P3(x1121)+~P9(x1122)+~P6(x1121,f17(x1122)) % 52.58/52.66 [113]P3(x1131)+~P16(x1132)+~P6(x1131,f17(x1132)) % 52.58/52.66 [114]P3(x1141)+~P18(x1142)+~P6(x1141,f17(x1142)) % 52.58/52.66 [115]P3(x1151)+~P19(x1152)+~P6(x1151,f17(x1152)) % 52.58/52.66 [116]P9(x1161)+~P9(x1162)+~P6(x1161,f17(x1162)) % 52.58/52.66 [117]P9(x1171)+~P16(x1172)+~P6(x1171,f17(x1172)) % 52.58/52.66 [118]P9(x1181)+~P18(x1182)+~P6(x1181,f17(x1182)) % 52.58/52.66 [119]P9(x1191)+~P19(x1192)+~P6(x1191,f17(x1192)) % 52.58/52.66 [120]P16(x1201)+~P16(x1202)+~P6(x1201,f17(x1202)) % 52.58/52.66 [121]P16(x1211)+~P18(x1212)+~P6(x1211,f17(x1212)) % 52.58/52.66 [122]P16(x1221)+~P19(x1222)+~P6(x1221,f17(x1222)) % 52.58/52.66 [123]P18(x1231)+~P18(x1232)+~P6(x1231,f17(x1232)) % 52.58/52.66 [124]P18(x1241)+~P19(x1242)+~P6(x1241,f17(x1242)) % 52.58/52.66 [125]P19(x1251)+~P19(x1252)+~P6(x1251,f17(x1252)) % 52.58/52.66 [129]~P10(x1291)+~P7(x1292,x1293)+~P6(x1293,f17(x1291)) % 52.58/52.66 [130]P6(x1301,x1302)+~P7(x1301,x1303)+~P6(x1303,f17(x1302)) % 52.58/52.66 [136]E(x1361,x1362)+~E(f15(x1363,x1361),f15(x1364,x1362))+~P6(x1361,f17(f17(x1363))) % 52.58/52.66 [137]E(x1371,x1372)+~E(f15(x1371,x1373),f15(x1372,x1374))+~P6(x1373,f17(f17(x1371))) % 52.58/52.66 [132]~P1(x1322)+~P10(x1321)+P17(x1321,x1322)+~P6(x1321,f17(f16(x1322))) % 52.58/52.66 [135]~P1(x1352)+~P11(x1351,x1352)+P13(x1351,x1352)+~P6(x1351,f17(f16(x1352))) % 52.58/52.66 [138]~P1(x1382)+~P13(x1381,x1382)+P11(x1381,x1382)+~E(f10(x1382,x1381),x1381)+~P6(x1381,f17(f16(x1382))) % 52.58/52.66 [139]~P1(x1392)+~P13(x1391,x1392)+P11(x1391,x1392)+P5(x1391,f10(x1392,x1391))+~P6(x1391,f17(f16(x1392))) % 52.58/52.66 [140]~P1(x1402)+~P13(x1401,x1402)+P11(x1401,x1402)+P13(f10(x1402,x1401),x1402)+~P6(x1401,f17(f16(x1402))) % 52.58/52.66 [141]~P1(x1412)+~P13(x1411,x1412)+P11(x1411,x1412)+P6(f10(x1412,x1411),f17(f16(x1412)))+~P6(x1411,f17(f16(x1412))) % 52.58/52.66 [142]~P11(x1422,x1423)+~P13(x1421,x1423)+~P5(x1422,x1421)+E(x1421,x1422)+~P1(x1423)+~P6(x1422,f17(f16(x1423)))+~P6(x1421,f17(f16(x1423))) % 52.58/52.66 [143]~P1(x1432)+~P1(x1434)+~P13(x1433,x1434)+P13(x1431,x1432)+~E(x1433,x1431)+~P6(x1431,f17(f16(x1432)))+~E(f15(f16(x1434),f18(x1434)),f15(f16(x1432),f18(x1432)))+~P6(x1433,f17(f16(x1434))) % 52.58/52.66 [1]E(x11,x11) % 52.58/52.66 [2]E(x22,x21)+~E(x21,x22) % 52.58/52.66 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 52.58/52.66 [4]~E(x41,x42)+E(f5(x41),f5(x42)) % 52.58/52.66 [5]~E(x51,x52)+E(f14(x51),f14(x52)) % 52.58/52.66 [6]~E(x61,x62)+E(f16(x61),f16(x62)) % 52.58/52.66 [7]~E(x71,x72)+E(f17(x71),f17(x72)) % 52.58/52.66 [8]~E(x81,x82)+E(f10(x81,x83),f10(x82,x83)) % 52.58/52.66 [9]~E(x91,x92)+E(f10(x93,x91),f10(x93,x92)) % 52.58/52.66 [10]~E(x101,x102)+E(f7(x101),f7(x102)) % 52.58/52.66 [11]~E(x111,x112)+E(f18(x111),f18(x112)) % 52.58/52.66 [12]~E(x121,x122)+E(f15(x121,x123),f15(x122,x123)) % 52.58/52.66 [13]~E(x131,x132)+E(f15(x133,x131),f15(x133,x132)) % 52.58/52.66 [14]~E(x141,x142)+E(f6(x141),f6(x142)) % 52.58/52.66 [15]~P1(x151)+P1(x152)+~E(x151,x152) % 52.58/52.66 [16]P6(x162,x163)+~E(x161,x162)+~P6(x161,x163) % 52.58/52.66 [17]P6(x173,x172)+~E(x171,x172)+~P6(x173,x171) % 52.58/52.66 [18]P13(x182,x183)+~E(x181,x182)+~P13(x181,x183) % 52.58/52.66 [19]P13(x193,x192)+~E(x191,x192)+~P13(x193,x191) % 52.58/52.66 [20]~P9(x201)+P9(x202)+~E(x201,x202) % 52.58/52.66 [21]~P2(x211)+P2(x212)+~E(x211,x212) % 52.58/52.66 [22]~P3(x221)+P3(x222)+~E(x221,x222) % 52.58/52.66 [23]~P16(x231)+P16(x232)+~E(x231,x232) % 52.58/52.66 [24]~P19(x241)+P19(x242)+~E(x241,x242) % 52.58/52.66 [25]P5(x252,x253)+~E(x251,x252)+~P5(x251,x253) % 52.58/52.66 [26]P5(x263,x262)+~E(x261,x262)+~P5(x263,x261) % 52.58/52.66 [27]~P12(x271)+P12(x272)+~E(x271,x272) % 52.58/52.66 [28]P11(x282,x283)+~E(x281,x282)+~P11(x281,x283) % 52.58/52.66 [29]P11(x293,x292)+~E(x291,x292)+~P11(x293,x291) % 52.58/52.66 [30]~P18(x301)+P18(x302)+~E(x301,x302) % 52.58/52.66 [31]~P10(x311)+P10(x312)+~E(x311,x312) % 52.58/52.66 [32]~P15(x321)+P15(x322)+~E(x321,x322) % 52.58/52.66 [33]~P14(x331)+P14(x332)+~E(x331,x332) % 52.58/52.66 [34]P7(x342,x343)+~E(x341,x342)+~P7(x341,x343) % 52.58/52.66 [35]P7(x353,x352)+~E(x351,x352)+~P7(x353,x351) % 52.58/52.66 [36]~P4(x361)+P4(x362)+~E(x361,x362) % 52.58/52.66 [37]~P8(x371)+P8(x372)+~E(x371,x372) % 52.58/52.66 [38]P17(x382,x383)+~E(x381,x382)+~P17(x381,x383) % 52.58/52.66 [39]P17(x393,x392)+~E(x391,x392)+~P17(x393,x391) % 52.58/52.66 [40]~P20(x401)+P20(x402)+~E(x401,x402) % 52.66/52.67 cnf(146,plain, % 52.66/52.67 (E(a2,a1)), % 52.66/52.67 inference(scs_inference,[],[41,2])). % 52.66/52.67 cnf(147,plain, % 52.66/52.67 (~P7(x1471,a11)), % 52.66/52.67 inference(scs_inference,[],[41,57,2,90])). % 52.66/52.67 cnf(149,plain, % 52.66/52.67 (P5(a2,f16(a3))), % 52.66/52.67 inference(scs_inference,[],[41,63,57,2,90,128])). % 52.66/52.67 cnf(151,plain, % 52.66/52.67 (P6(a1,f17(f16(a3)))), % 52.66/52.67 inference(scs_inference,[],[41,63,57,2,90,128,16])). % 52.66/52.67 cnf(153,plain, % 52.66/52.67 (P6(f14(x1531),x1531)), % 52.66/52.67 inference(rename_variables,[],[62])). % 52.66/52.67 cnf(154,plain, % 52.66/52.67 (P5(a2,a1)), % 52.66/52.67 inference(scs_inference,[],[41,63,61,62,57,2,90,128,16,17,25])). % 52.66/52.67 cnf(155,plain, % 52.66/52.67 (P5(x1551,x1551)), % 52.66/52.67 inference(rename_variables,[],[61])). % 52.66/52.68 cnf(156,plain, % 52.66/52.68 (P5(a1,a2)), % 52.66/52.68 inference(scs_inference,[],[41,63,61,155,62,57,2,90,128,16,17,25,26])). % 52.66/52.68 cnf(158,plain, % 52.66/52.68 (P11(a1,a3)), % 52.66/52.68 inference(scs_inference,[],[41,60,63,61,155,62,57,2,90,128,16,17,25,26,28])). % 52.66/52.68 cnf(159,plain, % 52.66/52.68 (~E(a3,a8)), % 52.66/52.68 inference(scs_inference,[],[41,60,69,63,61,155,62,57,2,90,128,16,17,25,26,28,29])). % 52.66/52.68 cnf(160,plain, % 52.66/52.68 (P7(f14(a12),a12)), % 52.66/52.68 inference(scs_inference,[],[41,60,69,63,61,155,62,153,57,67,2,90,128,16,17,25,26,28,29,108])). % 52.66/52.68 cnf(161,plain, % 52.66/52.68 (P6(f14(x1611),x1611)), % 52.66/52.68 inference(rename_variables,[],[62])). % 52.66/52.68 cnf(164,plain, % 52.66/52.68 (P6(f14(x1641),x1641)), % 52.66/52.68 inference(rename_variables,[],[62])). % 52.66/52.68 cnf(167,plain, % 52.66/52.68 (P6(f5(x1671),f17(x1671))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(170,plain, % 52.66/52.68 (P6(f14(x1701),x1701)), % 52.66/52.68 inference(rename_variables,[],[62])). % 52.66/52.68 cnf(173,plain, % 52.66/52.68 (P6(f5(x1731),f17(x1731))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(175,plain, % 52.66/52.68 (P16(f14(f17(a11)))), % 52.66/52.68 inference(scs_inference,[],[41,60,69,63,61,155,62,153,161,164,170,65,167,47,49,51,57,67,2,90,128,16,17,25,26,28,29,108,111,112,116,117,120])). % 52.66/52.68 cnf(176,plain, % 52.66/52.68 (P6(f14(x1761),x1761)), % 52.66/52.68 inference(rename_variables,[],[62])). % 52.66/52.68 cnf(179,plain, % 52.66/52.68 (P6(f5(x1791),f17(x1791))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(181,plain, % 52.66/52.68 (P18(f14(f17(a11)))), % 52.66/52.68 inference(scs_inference,[],[41,60,69,63,61,155,62,153,161,164,170,176,65,167,173,47,49,51,53,57,67,2,90,128,16,17,25,26,28,29,108,111,112,116,117,120,121,123])). % 52.66/52.68 cnf(182,plain, % 52.66/52.68 (P6(f14(x1821),x1821)), % 52.66/52.68 inference(rename_variables,[],[62])). % 52.66/52.68 cnf(184,plain, % 52.66/52.68 (P18(f5(a11))), % 52.66/52.68 inference(scs_inference,[],[41,60,69,63,61,155,62,153,161,164,170,176,65,167,173,179,47,49,51,53,55,57,67,2,90,128,16,17,25,26,28,29,108,111,112,116,117,120,121,123,124])). % 52.66/52.68 cnf(185,plain, % 52.66/52.68 (P6(f5(x1851),f17(x1851))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(187,plain, % 52.66/52.68 (P19(f14(f17(a11)))), % 52.66/52.68 inference(scs_inference,[],[41,60,69,63,61,155,62,153,161,164,170,176,182,65,167,173,179,47,49,51,53,55,57,67,2,90,128,16,17,25,26,28,29,108,111,112,116,117,120,121,123,124,125])). % 52.66/52.68 cnf(188,plain, % 52.66/52.68 (P6(f14(x1881),x1881)), % 52.66/52.68 inference(rename_variables,[],[62])). % 52.66/52.68 cnf(190,plain, % 52.66/52.68 (~P7(x1901,f14(f17(a11)))), % 52.66/52.68 inference(scs_inference,[],[41,60,69,63,61,155,62,153,161,164,170,176,182,188,65,167,173,179,47,49,51,53,55,57,67,2,90,128,16,17,25,26,28,29,108,111,112,116,117,120,121,123,124,125,129])). % 52.66/52.68 cnf(191,plain, % 52.66/52.68 (P6(f14(x1911),x1911)), % 52.66/52.68 inference(rename_variables,[],[62])). % 52.66/52.68 cnf(196,plain, % 52.66/52.68 (P17(f5(f16(a3)),a3)), % 52.66/52.68 inference(scs_inference,[],[41,42,60,69,63,61,155,62,153,161,164,170,176,182,188,191,65,167,173,179,185,47,49,51,53,55,57,67,59,2,90,128,16,17,25,26,28,29,108,111,112,116,117,120,121,123,124,125,129,137,132])). % 52.66/52.68 cnf(200,plain, % 52.66/52.68 (P13(a2,a3)), % 52.66/52.68 inference(scs_inference,[],[41,42,60,69,63,61,155,62,153,161,164,170,176,182,188,191,65,167,173,179,185,47,49,51,53,55,57,67,59,2,90,128,16,17,25,26,28,29,108,111,112,116,117,120,121,123,124,125,129,137,132,135])). % 52.66/52.68 cnf(205,plain, % 52.66/52.68 (~E(a3,f15(f16(a8),f18(a8)))+P1(f15(f16(a3),f18(a3)))), % 52.66/52.68 inference(scs_inference,[],[41,42,60,69,66,63,61,155,62,153,161,164,170,176,182,188,191,65,167,173,179,185,47,49,51,53,55,57,67,59,2,90,128,16,17,25,26,28,29,108,111,112,116,117,120,121,123,124,125,129,137,132,135,126,3,15])). % 52.66/52.68 cnf(212,plain, % 52.66/52.68 (~P7(x2121,f5(x2122))), % 52.66/52.68 inference(scs_inference,[],[59,90])). % 52.66/52.68 cnf(216,plain, % 52.66/52.68 (E(f15(f16(a3),f18(a3)),f15(f16(a8),f18(a8)))), % 52.66/52.68 inference(scs_inference,[],[64,66,59,90,128,2])). % 52.66/52.68 cnf(218,plain, % 52.66/52.68 (P6(f14(x2181),x2181)), % 52.66/52.68 inference(rename_variables,[],[62])). % 52.66/52.68 cnf(221,plain, % 52.66/52.68 (P6(f5(x2211),f17(x2211))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(224,plain, % 52.66/52.68 (P6(f14(x2241),x2241)), % 52.66/52.68 inference(rename_variables,[],[62])). % 52.66/52.68 cnf(227,plain, % 52.66/52.68 (P6(f5(x2271),f17(x2271))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(230,plain, % 52.66/52.68 (P6(f14(x2301),x2301)), % 52.66/52.68 inference(rename_variables,[],[62])). % 52.66/52.68 cnf(232,plain, % 52.66/52.68 (P7(a1,f17(f16(a8)))), % 52.66/52.68 inference(scs_inference,[],[64,66,175,181,187,68,62,218,224,65,221,59,90,128,2,113,114,118,119,122,108])). % 52.66/52.68 cnf(236,plain, % 52.66/52.68 (P6(f5(x2361),f17(x2361))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(238,plain, % 52.66/52.68 (P18(f14(f17(f14(f17(a11)))))), % 52.66/52.68 inference(scs_inference,[],[64,66,175,181,187,68,62,218,224,230,65,221,227,59,90,128,2,113,114,118,119,122,108,120,123])). % 52.66/52.68 cnf(239,plain, % 52.66/52.68 (P6(f14(x2391),x2391)), % 52.66/52.68 inference(rename_variables,[],[62])). % 52.66/52.68 cnf(242,plain, % 52.66/52.68 (P6(f14(x2421),x2421)), % 52.66/52.68 inference(rename_variables,[],[62])). % 52.66/52.68 cnf(244,plain, % 52.66/52.68 (~P7(x2441,f14(f17(f5(x2442))))), % 52.66/52.68 inference(scs_inference,[],[64,66,175,181,187,68,62,218,224,230,239,242,65,221,227,59,90,128,2,113,114,118,119,122,108,120,123,125,129])). % 52.66/52.68 cnf(247,plain, % 52.66/52.68 (P18(f5(f14(f17(a11))))), % 52.66/52.68 inference(scs_inference,[],[64,66,175,181,187,68,62,218,224,230,239,242,65,221,227,236,59,90,128,2,113,114,118,119,122,108,120,123,125,129,124])). % 52.66/52.68 cnf(248,plain, % 52.66/52.68 (P6(f5(x2481),f17(x2481))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(251,plain, % 52.66/52.68 (P6(f5(x2511),f17(x2511))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(253,plain, % 52.66/52.68 (P6(a2,f17(f16(a8)))), % 52.66/52.68 inference(scs_inference,[],[41,64,66,159,175,181,187,68,62,218,224,230,239,242,65,221,227,236,248,59,90,128,2,113,114,118,119,122,108,120,123,125,129,124,137,16])). % 52.66/52.68 cnf(256,plain, % 52.66/52.68 (~E(a12,f14(f17(a11)))), % 52.66/52.68 inference(scs_inference,[],[41,64,66,159,146,190,175,181,187,149,160,200,68,62,218,224,230,239,242,65,221,227,236,248,59,90,128,2,113,114,118,119,122,108,120,123,125,129,124,137,16,18,25,35])). % 52.66/52.68 cnf(258,plain, % 52.66/52.68 (P17(f5(f16(a8)),a8)), % 52.66/52.68 inference(scs_inference,[],[41,43,64,66,159,146,190,175,181,187,149,160,200,68,62,218,224,230,239,242,65,221,227,236,248,251,59,90,128,2,113,114,118,119,122,108,120,123,125,129,124,137,16,18,25,35,132])). % 52.66/52.68 cnf(262,plain, % 52.66/52.68 (P13(a1,a8)), % 52.66/52.68 inference(scs_inference,[],[41,43,64,66,42,63,159,146,190,175,181,187,149,160,200,68,62,218,224,230,239,242,65,221,227,236,248,251,59,90,128,2,113,114,118,119,122,108,120,123,125,129,124,137,16,18,25,35,132,143])). % 52.66/52.68 cnf(267,plain, % 52.66/52.68 (P7(a2,f17(f16(a8)))), % 52.66/52.68 inference(scs_inference,[],[41,43,64,66,42,63,159,146,190,175,181,187,149,160,200,68,62,218,224,230,239,242,65,221,227,236,248,251,59,90,128,2,113,114,118,119,122,108,120,123,125,129,124,137,16,18,25,35,132,143,126,27,34])). % 52.66/52.68 cnf(285,plain, % 52.66/52.68 (P7(a2,f17(f16(a3)))), % 52.66/52.68 inference(scs_inference,[],[63,253,267,68,128,126,108])). % 52.66/52.68 cnf(291,plain, % 52.66/52.68 (P7(a1,f17(f16(a3)))), % 52.66/52.68 inference(scs_inference,[],[63,253,256,267,146,68,65,128,126,108,137,34])). % 52.66/52.68 cnf(292,plain, % 52.66/52.68 (P13(a2,a8)), % 52.66/52.68 inference(scs_inference,[],[41,63,253,256,267,262,146,68,65,128,126,108,137,34,18])). % 52.66/52.68 cnf(293,plain, % 52.66/52.68 (~E(f17(f16(a8)),f5(x2931))), % 52.66/52.68 inference(scs_inference,[],[41,63,253,256,267,262,146,212,68,65,128,126,108,137,34,18,35])). % 52.66/52.68 cnf(295,plain, % 52.66/52.68 (~E(f10(a8,a1),a1)), % 52.66/52.68 inference(scs_inference,[],[41,63,69,43,64,253,256,267,262,146,212,68,65,128,126,108,137,34,18,35,138])). % 52.66/52.68 cnf(297,plain, % 52.66/52.68 (P5(a1,f10(a8,a1))), % 52.66/52.68 inference(scs_inference,[],[41,63,69,43,64,253,256,267,262,146,212,68,65,128,126,108,137,34,18,35,138,139])). % 52.66/52.68 cnf(299,plain, % 52.66/52.68 (P13(f10(a8,a1),a8)), % 52.66/52.68 inference(scs_inference,[],[41,63,69,43,64,253,256,267,262,146,212,68,65,128,126,108,137,34,18,35,138,139,140])). % 52.66/52.68 cnf(304,plain, % 52.66/52.68 (P5(a2,f10(a8,a1))), % 52.66/52.68 inference(scs_inference,[],[41,63,69,43,64,253,256,267,262,159,146,212,68,65,128,126,108,137,34,18,35,138,139,140,81,3,25])). % 52.66/52.68 cnf(309,plain, % 52.66/52.68 (P17(x3091,a3)+~E(f5(f16(a3)),x3091)), % 52.66/52.68 inference(scs_inference,[],[41,63,69,43,64,253,256,267,262,159,146,212,196,68,62,65,128,126,108,137,34,18,35,138,139,140,81,3,25,136,37,38])). % 52.66/52.68 cnf(317,plain, % 52.66/52.68 (P5(f14(f17(x3171)),x3171)), % 52.66/52.68 inference(scs_inference,[],[291,62,126,128])). % 52.66/52.68 cnf(334,plain, % 52.66/52.68 (P5(f5(x3341),x3341)), % 52.66/52.68 inference(scs_inference,[],[65,285,126,128])). % 52.66/52.68 cnf(336,plain, % 52.66/52.68 (P5(f5(a1),a2)), % 52.66/52.68 inference(scs_inference,[],[41,65,285,126,128,26])). % 52.66/52.68 cnf(381,plain, % 52.66/52.68 (~E(a12,f5(x3811))), % 52.66/52.68 inference(scs_inference,[],[160,212,35])). % 52.66/52.68 cnf(421,plain, % 52.66/52.68 (P6(f5(x4211),f17(x4211))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(424,plain, % 52.66/52.68 (P6(f5(x4241),f17(x4241))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(427,plain, % 52.66/52.68 (P6(f5(x4271),f17(x4271))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(430,plain, % 52.66/52.68 (P6(f5(x4301),f17(x4301))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(435,plain, % 52.66/52.68 (~E(a12,a11)), % 52.66/52.68 inference(scs_inference,[],[381,65,421,424,427,430,160,247,147,118,121,137,123,114,35])). % 52.66/52.68 cnf(525,plain, % 52.66/52.68 (P6(f5(x5251),f17(x5251))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(528,plain, % 52.66/52.68 (P6(f5(x5281),f17(x5281))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(531,plain, % 52.66/52.68 (P6(f5(x5311),f17(x5311))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(534,plain, % 52.66/52.68 (P6(f5(x5341),f17(x5341))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(537,plain, % 52.66/52.68 (P6(f5(x5371),f17(x5371))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(540,plain, % 52.66/52.68 (P6(f5(x5401),f17(x5401))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(542,plain, % 52.66/52.68 (P9(f5(f5(a11)))), % 52.66/52.68 inference(scs_inference,[],[65,525,528,531,534,537,540,184,56,119,121,114,115,123,125,118])). % 52.66/52.68 cnf(543,plain, % 52.66/52.68 (P6(f5(x5431),f17(x5431))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(546,plain, % 52.66/52.68 (P6(f5(x5461),f17(x5461))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(548,plain, % 52.66/52.68 (P18(f5(a12))), % 52.66/52.68 inference(scs_inference,[],[65,525,528,531,534,537,540,543,546,184,56,119,121,114,115,123,125,118,122,124])). % 52.66/52.68 cnf(632,plain, % 52.66/52.68 (~P1(f15(f16(a8),f18(a8)))+P4(f15(f16(a3),f18(a3)))), % 52.66/52.68 inference(scs_inference,[],[66,36,80])). % 52.66/52.68 cnf(641,plain, % 52.66/52.68 (P16(f5(x6411))), % 52.66/52.68 inference(scs_inference,[],[59,78,75])). % 52.66/52.68 cnf(643,plain, % 52.66/52.68 (P6(f14(x6431),x6431)), % 52.66/52.68 inference(rename_variables,[],[62])). % 52.66/52.68 cnf(646,plain, % 52.66/52.68 (P6(f14(x6461),x6461)), % 52.66/52.68 inference(rename_variables,[],[62])). % 52.66/52.68 cnf(648,plain, % 52.66/52.68 (P16(f14(f17(f5(x6481))))), % 52.66/52.68 inference(scs_inference,[],[62,643,646,641,113,117,120])). % 52.66/52.68 cnf(720,plain, % 52.66/52.68 (P17(x7201,a8)+~E(f5(f16(a8)),x7201)), % 52.66/52.68 inference(scs_inference,[],[151,258,123,38])). % 52.66/52.68 cnf(767,plain, % 52.66/52.68 (P6(f5(x7671),f17(x7671))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(769,plain, % 52.66/52.68 (P18(f5(f5(a12)))), % 52.66/52.68 inference(scs_inference,[],[65,767,548,114,123])). % 52.66/52.68 cnf(770,plain, % 52.66/52.68 (P6(f5(x7701),f17(x7701))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(775,plain, % 52.66/52.68 (P13(x7751,a8)+~E(f10(a8,a1),x7751)), % 52.66/52.68 inference(scs_inference,[],[65,767,770,299,548,114,123,118,18])). % 52.66/52.68 cnf(777,plain, % 52.66/52.68 (P5(x7771,a2)+~E(f5(a1),x7771)), % 52.66/52.68 inference(scs_inference,[],[336,65,767,770,160,299,548,114,123,118,18,34,25])). % 52.66/52.68 cnf(778,plain, % 52.66/52.68 (P6(x7781,x7782)+~P7(x7781,f14(f17(x7782)))), % 52.66/52.68 inference(scs_inference,[],[336,65,767,770,62,160,299,548,114,123,118,18,34,25,130])). % 52.66/52.68 cnf(842,plain, % 52.66/52.68 (~P2(f15(f16(a3),f18(a3)))+P2(f15(f16(a8),f18(a8)))), % 52.66/52.68 inference(scs_inference,[],[253,146,216,123,15,21])). % 52.66/52.68 cnf(883,plain, % 52.66/52.68 (P6(f14(x8831),x8831)), % 52.66/52.68 inference(rename_variables,[],[62])). % 52.66/52.68 cnf(886,plain, % 52.66/52.68 (P6(f14(x8861),x8861)), % 52.66/52.68 inference(rename_variables,[],[62])). % 52.66/52.68 cnf(888,plain, % 52.66/52.68 (P9(f14(f17(a12)))), % 52.66/52.68 inference(scs_inference,[],[62,883,886,54,114,121,118])). % 52.66/52.68 cnf(889,plain, % 52.66/52.68 (P6(f14(x8891),x8891)), % 52.66/52.68 inference(rename_variables,[],[62])). % 52.66/52.68 cnf(891,plain, % 52.66/52.68 (P18(f14(f17(a12)))), % 52.66/52.68 inference(scs_inference,[],[62,883,886,889,54,114,121,118,123])). % 52.66/52.68 cnf(905,plain, % 52.66/52.68 (P6(f5(x9051),f17(x9051))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(907,plain, % 52.66/52.68 (P16(f14(f17(f14(f17(a12)))))), % 52.66/52.68 inference(scs_inference,[],[65,62,891,114,121])). % 52.66/52.68 cnf(911,plain, % 52.66/52.68 (P6(f5(x9111),f17(x9111))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(913,plain, % 52.66/52.68 (P18(f5(f14(f17(a12))))), % 52.66/52.68 inference(scs_inference,[],[65,905,911,62,891,114,121,118,123])). % 52.66/52.68 cnf(925,plain, % 52.66/52.68 (P6(f5(x9251),f17(x9251))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(928,plain, % 52.66/52.68 (P6(f5(x9281),f17(x9281))), % 52.66/52.68 inference(rename_variables,[],[65])). % 52.66/52.68 cnf(933,plain, % 52.66/52.68 (P5(a2,x9331)+~E(f10(a8,a1),x9331)), % 52.66/52.68 inference(scs_inference,[],[304,65,925,928,913,114,118,123,26])). % 52.66/52.68 cnf(934,plain, % 52.66/52.68 (P5(a1,x9341)+~E(f10(a8,a1),x9341)), % 52.66/52.68 inference(scs_inference,[],[146,304,65,925,928,913,114,118,123,26,25])). % 52.66/52.68 cnf(939,plain, % 52.66/52.68 (~P1(f15(f16(a3),f18(a3)))+P1(f15(f16(a8),f18(a8)))), % 52.66/52.68 inference(scs_inference,[],[216,15])). % 52.66/52.68 cnf(941,plain, % 52.66/52.68 (P1(f15(f16(a8),f18(a8)))+~P6(f18(a3),f17(f17(f16(a3))))), % 52.66/52.68 inference(scs_inference,[],[216,15,205,133])). % 52.66/52.68 cnf(984,plain, % 52.66/52.68 (P5(f5(x9841),f16(a3))+~E(f17(x9841),f17(f16(a3)))), % 52.66/52.68 inference(scs_inference,[],[42,65,59,17,132,128])). % 52.66/52.68 cnf(1032,plain, % 52.66/52.68 (P6(x10321,f17(x10322))+~E(f5(x10322),x10321)), % 52.66/52.68 inference(scs_inference,[],[65,16])). % 52.66/52.68 cnf(1044,plain, % 52.66/52.68 (P6(x10441,x10442)+~E(f14(x10442),x10441)), % 52.66/52.68 inference(scs_inference,[],[66,216,62,334,25,20,23,16])). % 52.66/52.68 cnf(1059,plain, % 52.66/52.68 (P11(a2,a8)+~E(f10(a8,a2),a2)), % 52.66/52.68 inference(scs_inference,[],[63,42,43,253,146,292,62,317,25,20,135,132,138])). % 52.66/52.68 cnf(1693,plain, % 52.66/52.68 (P5(f5(f15(f16(a8),f18(a8))),f15(f16(a3),f18(a3)))), % 52.66/52.68 inference(scs_inference,[],[66,62,334,17,26])). % 52.66/52.68 cnf(1695,plain, % 52.66/52.68 (P5(f15(f16(a3),f18(a3)),f15(f16(a8),f18(a8)))), % 52.66/52.68 inference(scs_inference,[],[66,62,334,61,17,26,25])). % 52.66/52.68 cnf(1705,plain, % 52.66/52.68 (P5(x17051,f15(f16(a3),f18(a3)))+~E(f5(f15(f16(a8),f18(a8))),x17051)), % 52.66/52.68 inference(scs_inference,[],[66,1693,317,26,25])). % 52.66/52.68 cnf(1712,plain, % 52.66/52.68 (P5(f15(f16(a8),f18(a8)),f15(f16(a3),f18(a3)))), % 52.66/52.68 inference(scs_inference,[],[66,61,26])). % 52.66/52.68 cnf(4353,plain, % 52.66/52.68 (E(f7(a3),a11)), % 52.66/52.68 inference(scs_inference,[],[42,70,87])). % 52.66/52.68 cnf(4356,plain, % 52.66/52.68 (P10(f7(a3))), % 52.66/52.68 inference(scs_inference,[],[435,57,4353,2,3,31])). % 52.66/52.68 cnf(4357,plain, % 52.66/52.68 (P19(f7(a3))), % 52.66/52.68 inference(scs_inference,[],[435,57,4353,55,2,3,31,24])). % 52.66/52.68 cnf(4358,plain, % 52.66/52.68 (P18(f7(a3))), % 52.66/52.68 inference(scs_inference,[],[435,57,4353,53,55,2,3,31,24,30])). % 52.66/52.68 cnf(4359,plain, % 52.66/52.68 (P16(f7(a3))), % 52.66/52.68 inference(scs_inference,[],[435,57,4353,51,53,55,2,3,31,24,30,23])). % 52.66/52.68 cnf(4361,plain, % 52.66/52.68 (P9(f7(a3))), % 52.66/52.68 inference(scs_inference,[],[435,57,4353,47,49,51,53,55,2,3,31,24,30,23,22,20])). % 52.66/52.69 cnf(4362,plain, % 52.66/52.69 (~P7(x43621,f7(a3))), % 52.66/52.69 inference(scs_inference,[],[435,57,4353,47,49,51,53,55,2,3,31,24,30,23,22,20,90])). % 52.66/52.69 cnf(4375,plain, % 52.66/52.69 (P6(f5(x43751),f17(x43751))), % 52.66/52.69 inference(rename_variables,[],[65])). % 52.66/52.69 cnf(4377,plain, % 52.66/52.69 (P16(f14(f17(f7(a3))))), % 52.66/52.69 inference(scs_inference,[],[4358,4359,65,62,113,121])). % 52.66/52.69 cnf(4378,plain, % 52.66/52.69 (P6(f14(x43781),x43781)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(4381,plain, % 52.66/52.69 (P6(f5(x43811),f17(x43811))), % 52.66/52.69 inference(rename_variables,[],[65])). % 52.66/52.69 cnf(4383,plain, % 52.66/52.69 (P18(f5(f7(a3)))), % 52.66/52.69 inference(scs_inference,[],[4357,4358,4359,65,4375,4381,62,113,121,117,124])). % 52.66/52.69 cnf(4384,plain, % 52.66/52.69 (P6(f5(x43841),f17(x43841))), % 52.66/52.69 inference(rename_variables,[],[65])). % 52.66/52.69 cnf(4387,plain, % 52.66/52.69 (P6(f14(x43871),x43871)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(4389,plain, % 52.66/52.69 (P3(f14(f17(f7(a3))))), % 52.66/52.69 inference(scs_inference,[],[4357,4358,4359,4361,65,4375,4381,62,4378,4387,113,121,117,124,116,115])). % 52.66/52.69 cnf(4390,plain, % 52.66/52.69 (P6(f14(x43901),x43901)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(4396,plain, % 52.66/52.69 (P6(f14(x43961),x43961)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(4398,plain, % 52.66/52.69 (~P7(x43981,f14(f17(f7(a3))))), % 52.66/52.69 inference(scs_inference,[],[4356,4357,4358,4359,4361,65,4375,4381,4384,62,4378,4387,4390,4396,113,121,117,124,116,115,125,123,129])). % 52.66/52.69 cnf(4401,plain, % 52.66/52.69 (~E(f17(f16(a3)),f7(a3))), % 52.66/52.69 inference(scs_inference,[],[291,4356,4357,4358,4359,4361,65,4375,4381,4384,62,4378,4387,4390,4396,4362,113,121,117,124,116,115,125,123,129,35])). % 52.66/52.69 cnf(4435,plain, % 52.66/52.69 (~E(f17(f16(a8)),f7(a3))), % 52.66/52.69 inference(scs_inference,[],[267,4362,35])). % 52.66/52.69 cnf(4531,plain, % 52.66/52.69 (P17(x45311,a9)+~E(f5(f16(a9)),x45311)), % 52.66/52.69 inference(scs_inference,[],[44,65,59,132,38])). % 52.66/52.69 cnf(4617,plain, % 52.66/52.69 (P16(f7(f15(x46171,f5(f17(x46171)))))), % 52.66/52.69 inference(scs_inference,[],[65,84,133])). % 52.66/52.69 cnf(4996,plain, % 52.66/52.69 (P17(x49961,a4)+~E(f5(f16(a4)),x49961)), % 52.66/52.69 inference(scs_inference,[],[45,65,59,132,38])). % 52.66/52.69 cnf(9556,plain, % 52.66/52.69 (P19(f5(a11))), % 52.66/52.69 inference(scs_inference,[],[55,65,125])). % 52.66/52.69 cnf(10014,plain, % 52.66/52.69 (P19(f14(f17(a12)))), % 52.66/52.69 inference(scs_inference,[],[56,62,125])). % 52.66/52.69 cnf(11754,plain, % 52.66/52.69 (P16(f7(a9))), % 52.66/52.69 inference(scs_inference,[],[44,82,83,84])). % 52.66/52.69 cnf(11758,plain, % 52.66/52.69 (P19(f7(a9))), % 52.66/52.69 inference(scs_inference,[],[44,82,83,84,85,86])). % 52.66/52.69 cnf(11760,plain, % 52.66/52.69 (P10(f7(a9))), % 52.66/52.69 inference(scs_inference,[],[44,82,83,84,85,86,87])). % 52.66/52.69 cnf(11762,plain, % 52.66/52.69 (~P10(f6(a12))), % 52.66/52.69 inference(scs_inference,[],[67,44,82,83,84,85,86,87,88])). % 52.66/52.69 cnf(11766,plain, % 52.66/52.69 (P6(f15(f16(a3),f18(a3)),f17(f15(f16(a8),f18(a8))))), % 52.66/52.69 inference(scs_inference,[],[1695,67,44,82,83,84,85,86,87,88,89,110])). % 52.66/52.69 cnf(11768,plain, % 52.66/52.69 (P6(f6(a12),f17(a12))), % 52.66/52.69 inference(scs_inference,[],[1695,67,44,82,83,84,85,86,87,88,89,110,91])). % 52.66/52.69 cnf(11770,plain, % 52.66/52.69 (E(f5(a1),f5(a2))), % 52.66/52.69 inference(scs_inference,[],[41,1695,67,44,82,83,84,85,86,87,88,89,110,91,4])). % 52.66/52.69 cnf(11773,plain, % 52.66/52.69 (E(f17(a1),f17(a2))), % 52.66/52.69 inference(scs_inference,[],[41,1695,67,44,82,83,84,85,86,87,88,89,110,91,4,5,6,7])). % 52.66/52.69 cnf(11777,plain, % 52.66/52.69 (P6(f7(a9),f17(f16(a9)))), % 52.66/52.69 inference(scs_inference,[],[41,1695,67,44,82,83,84,85,86,87,88,89,110,91,4,5,6,7,10,11,14,127])). % 52.66/52.69 cnf(11780,plain, % 52.66/52.69 (P6(f14(x117801),x117801)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11782,plain, % 52.66/52.69 (E(f10(a1,x117821),f10(a2,x117821))), % 52.66/52.69 inference(scs_inference,[],[41,1695,67,62,44,82,83,84,85,86,87,88,89,110,91,4,5,6,7,10,11,14,127,134,8])). % 52.66/52.69 cnf(11783,plain, % 52.66/52.69 (E(f10(x117831,a1),f10(x117831,a2))), % 52.66/52.69 inference(scs_inference,[],[41,1695,67,62,44,82,83,84,85,86,87,88,89,110,91,4,5,6,7,10,11,14,127,134,8,9])). % 52.66/52.69 cnf(11784,plain, % 52.66/52.69 (P6(f18(a9),f17(f17(f16(a9))))), % 52.66/52.69 inference(scs_inference,[],[41,1695,67,62,44,82,83,84,85,86,87,88,89,110,91,4,5,6,7,10,11,14,127,134,8,9,131])). % 52.66/52.69 cnf(11786,plain, % 52.66/52.69 (E(f5(x117861),a11)), % 52.66/52.69 inference(scs_inference,[],[41,1695,67,59,62,44,82,83,84,85,86,87,88,89,110,91,4,5,6,7,10,11,14,127,134,8,9,131,70])). % 52.66/52.69 cnf(11789,plain, % 52.66/52.69 (P1(f15(x117891,f14(f17(f17(x117891)))))), % 52.66/52.69 inference(scs_inference,[],[41,1695,67,59,62,11780,44,82,83,84,85,86,87,88,89,110,91,4,5,6,7,10,11,14,127,134,8,9,131,70,12,133])). % 52.66/52.69 cnf(11790,plain, % 52.66/52.69 (P6(f14(x117901),x117901)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11794,plain, % 52.66/52.69 (P19(f5(x117941))), % 52.66/52.69 inference(scs_inference,[],[41,1695,67,59,62,11780,44,82,83,84,85,86,87,88,89,110,91,4,5,6,7,10,11,14,127,134,8,9,131,70,12,133,72,79])). % 52.66/52.69 cnf(11798,plain, % 52.66/52.69 (P18(f5(x117981))), % 52.66/52.69 inference(scs_inference,[],[41,1695,67,59,62,11780,44,82,83,84,85,86,87,88,89,110,91,4,5,6,7,10,11,14,127,134,8,9,131,70,12,133,72,79,74,78])). % 52.66/52.69 cnf(11807,plain, % 52.66/52.69 (P6(f14(x118071),x118071)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11812,plain, % 52.66/52.69 (P6(f14(x118121),x118121)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11815,plain, % 52.66/52.69 (P6(f14(x118151),x118151)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11818,plain, % 52.66/52.69 (P6(f14(x118181),x118181)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11821,plain, % 52.66/52.69 (P6(f14(x118211),x118211)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11824,plain, % 52.66/52.69 (P6(f14(x118241),x118241)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11827,plain, % 52.66/52.69 (P6(f14(x118271),x118271)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11830,plain, % 52.66/52.69 (P6(f14(x118301),x118301)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11833,plain, % 52.66/52.69 (P6(f14(x118331),x118331)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11836,plain, % 52.66/52.69 (P6(f14(x118361),x118361)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11839,plain, % 52.66/52.69 (~E(f10(a8,a2),a1)), % 52.66/52.69 inference(scs_inference,[],[41,46,4401,4383,542,9556,4377,1695,295,907,648,67,769,69,59,146,62,11780,11790,11807,11812,11815,11818,11821,11824,11827,11830,11833,44,45,82,83,84,85,86,87,88,89,110,91,4,5,6,7,10,11,14,127,134,8,9,131,70,12,133,72,79,74,78,13,73,80,2,93,109,98,99,97,101,102,103,105,104,106,28,3])). % 52.66/52.69 cnf(11840,plain, % 52.66/52.69 (P10(f14(f17(a11)))), % 52.66/52.69 inference(scs_inference,[],[41,46,4401,4383,542,9556,4377,1695,295,907,648,67,190,769,69,59,146,62,11780,11790,11807,11812,11815,11818,11821,11824,11827,11830,11833,11836,44,45,82,83,84,85,86,87,88,89,110,91,4,5,6,7,10,11,14,127,134,8,9,131,70,12,133,72,79,74,78,13,73,80,2,93,109,98,99,97,101,102,103,105,104,106,28,3,108])). % 52.66/52.69 cnf(11842,plain, % 52.66/52.69 (P6(f14(x118421),x118421)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11845,plain, % 52.66/52.69 (P6(f14(x118451),x118451)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11847,plain, % 52.66/52.69 (P9(f14(f17(f7(a9))))), % 52.66/52.69 inference(scs_inference,[],[41,46,4401,4383,542,888,9556,4377,1695,295,907,648,67,190,769,69,59,146,62,11780,11790,11807,11812,11815,11818,11821,11824,11827,11830,11833,11836,11842,11845,44,45,82,83,84,85,86,87,88,89,110,91,4,5,6,7,10,11,14,127,134,8,9,131,70,12,133,72,79,74,78,13,73,80,2,93,109,98,99,97,101,102,103,105,104,106,28,3,108,112,117])). % 52.66/52.69 cnf(11848,plain, % 52.66/52.69 (P6(f14(x118481),x118481)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11850,plain, % 52.66/52.69 (~P6(f17(f16(a8)),f17(f7(a3)))), % 52.66/52.69 inference(scs_inference,[],[41,46,4401,4383,542,888,9556,4377,1695,295,232,907,4356,648,67,190,769,69,59,146,62,11780,11790,11807,11812,11815,11818,11821,11824,11827,11830,11833,11836,11842,11845,44,45,82,83,84,85,86,87,88,89,110,91,4,5,6,7,10,11,14,127,134,8,9,131,70,12,133,72,79,74,78,13,73,80,2,93,109,98,99,97,101,102,103,105,104,106,28,3,108,112,117,129])). % 52.66/52.69 cnf(11853,plain, % 52.66/52.69 (P6(f14(x118531),x118531)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11855,plain, % 52.66/52.69 (P18(f14(f17(f5(a11))))), % 52.66/52.69 inference(scs_inference,[],[41,46,4401,4383,542,888,9556,4377,1695,295,232,907,4356,648,67,190,769,69,59,146,62,11780,11790,11807,11812,11815,11818,11821,11824,11827,11830,11833,11836,11842,11845,11848,11853,44,45,82,83,84,85,86,87,88,89,110,91,4,5,6,7,10,11,14,127,134,8,9,131,70,12,133,72,79,74,78,13,73,80,2,93,109,98,99,97,101,102,103,105,104,106,28,3,108,112,117,129,125,124])). % 52.66/52.69 cnf(11856,plain, % 52.66/52.69 (P6(f14(x118561),x118561)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11859,plain, % 52.66/52.69 (~E(f7(a3),a12)), % 52.66/52.69 inference(scs_inference,[],[41,46,4401,4383,542,888,9556,4377,1695,295,232,907,4356,648,67,190,769,69,59,146,62,11780,11790,11807,11812,11815,11818,11821,11824,11827,11830,11833,11836,11842,11845,11848,11853,44,45,82,83,84,85,86,87,88,89,110,91,4,5,6,7,10,11,14,127,134,8,9,131,70,12,133,72,79,74,78,13,73,80,2,93,109,98,99,97,101,102,103,105,104,106,28,3,108,112,117,129,125,124,36,31])). % 52.66/52.69 cnf(11863,plain, % 52.66/52.69 (P1(f15(a2,f14(f17(f17(a1)))))), % 52.66/52.69 inference(scs_inference,[],[41,46,4401,4383,542,888,9556,4377,1695,295,232,907,4356,648,67,190,769,69,59,146,62,11780,11790,11807,11812,11815,11818,11821,11824,11827,11830,11833,11836,11842,11845,11848,11853,11856,44,45,82,83,84,85,86,87,88,89,110,91,4,5,6,7,10,11,14,127,134,8,9,131,70,12,133,72,79,74,78,13,73,80,2,93,109,98,99,97,101,102,103,105,104,106,28,3,108,112,117,129,125,124,36,31,21,16,15])). % 52.66/52.69 cnf(11864,plain, % 52.66/52.69 (P6(f10(a8,a2),f17(f16(a8)))), % 52.66/52.69 inference(scs_inference,[],[41,46,4401,4383,542,888,9556,4377,1695,295,232,907,4356,648,67,190,769,69,292,59,253,146,62,11780,11790,11807,11812,11815,11818,11821,11824,11827,11830,11833,11836,11842,11845,11848,11853,11856,44,45,43,82,83,84,85,86,87,88,89,110,91,4,5,6,7,10,11,14,127,134,8,9,131,70,12,133,72,79,74,78,13,73,80,2,93,109,98,99,97,101,102,103,105,104,106,28,3,108,112,117,129,125,124,36,31,21,16,15,141])). % 52.66/52.69 cnf(11866,plain, % 52.66/52.69 (P5(a11,a2)), % 52.66/52.69 inference(scs_inference,[],[41,46,4401,4383,542,888,9556,4377,1695,295,232,907,4356,648,67,190,769,69,292,59,253,146,62,11780,11790,11807,11812,11815,11818,11821,11824,11827,11830,11833,11836,11842,11845,11848,11853,11856,44,45,43,82,83,84,85,86,87,88,89,110,91,4,5,6,7,10,11,14,127,134,8,9,131,70,12,133,72,79,74,78,13,73,80,2,93,109,98,99,97,101,102,103,105,104,106,28,3,108,112,117,129,125,124,36,31,21,16,15,141,777])). % 52.66/52.69 cnf(11868,plain, % 52.66/52.69 (P13(f10(a8,a2),a8)), % 52.66/52.69 inference(scs_inference,[],[41,46,4401,4383,542,888,9556,4377,1695,295,232,907,4356,648,67,190,769,69,292,59,253,146,62,11780,11790,11807,11812,11815,11818,11821,11824,11827,11830,11833,11836,11842,11845,11848,11853,11856,44,45,43,82,83,84,85,86,87,88,89,110,91,4,5,6,7,10,11,14,127,134,8,9,131,70,12,133,72,79,74,78,13,73,80,2,93,109,98,99,97,101,102,103,105,104,106,28,3,108,112,117,129,125,124,36,31,21,16,15,141,777,1032,775])). % 52.66/52.69 cnf(11869,plain, % 52.66/52.69 (P5(a2,f10(a8,a2))), % 52.66/52.69 inference(scs_inference,[],[41,46,4401,4383,542,888,9556,4377,1695,295,232,907,4356,648,67,190,769,69,292,59,253,146,62,11780,11790,11807,11812,11815,11818,11821,11824,11827,11830,11833,11836,11842,11845,11848,11853,11856,44,45,43,82,83,84,85,86,87,88,89,110,91,4,5,6,7,10,11,14,127,134,8,9,131,70,12,133,72,79,74,78,13,73,80,2,93,109,98,99,97,101,102,103,105,104,106,28,3,108,112,117,129,125,124,36,31,21,16,15,141,777,1032,775,933])). % 52.66/52.69 cnf(11870,plain, % 52.66/52.69 (P5(a1,f10(a8,a2))), % 52.66/52.69 inference(scs_inference,[],[41,46,4401,4383,542,888,9556,4377,1695,295,232,907,4356,648,67,190,769,69,292,59,253,146,62,11780,11790,11807,11812,11815,11818,11821,11824,11827,11830,11833,11836,11842,11845,11848,11853,11856,44,45,43,82,83,84,85,86,87,88,89,110,91,4,5,6,7,10,11,14,127,134,8,9,131,70,12,133,72,79,74,78,13,73,80,2,93,109,98,99,97,101,102,103,105,104,106,28,3,108,112,117,129,125,124,36,31,21,16,15,141,777,1032,775,933,934])). % 52.66/52.69 cnf(11871,plain, % 52.66/52.69 (~E(f10(a8,a2),a2)), % 52.66/52.69 inference(scs_inference,[],[41,46,4401,4383,542,888,9556,4377,1695,295,232,907,4356,648,67,190,769,69,292,59,253,146,62,11780,11790,11807,11812,11815,11818,11821,11824,11827,11830,11833,11836,11842,11845,11848,11853,11856,44,45,43,82,83,84,85,86,87,88,89,110,91,4,5,6,7,10,11,14,127,134,8,9,131,70,12,133,72,79,74,78,13,73,80,2,93,109,98,99,97,101,102,103,105,104,106,28,3,108,112,117,129,125,124,36,31,21,16,15,141,777,1032,775,933,934,1059])). % 52.66/52.69 cnf(11897,plain, % 52.66/52.69 (~P7(f17(f16(a8)),f14(f17(f17(f7(a3)))))), % 52.66/52.69 inference(scs_inference,[],[11850,778])). % 52.66/52.69 cnf(11900,plain, % 52.66/52.69 (E(f5(x119001),a11)), % 52.66/52.69 inference(rename_variables,[],[11786])). % 52.66/52.69 cnf(11902,plain, % 52.66/52.69 (E(f5(x119021),a11)), % 52.66/52.69 inference(rename_variables,[],[11786])). % 52.66/52.69 cnf(11904,plain, % 52.66/52.69 (E(f5(x119041),a11)), % 52.66/52.69 inference(rename_variables,[],[11786])). % 52.66/52.69 cnf(11906,plain, % 52.66/52.69 (E(f5(x119061),a11)), % 52.66/52.69 inference(rename_variables,[],[11786])). % 52.66/52.69 cnf(11907,plain, % 52.66/52.69 (P5(a11,f15(f16(a3),f18(a3)))), % 52.66/52.69 inference(scs_inference,[],[11850,11786,11900,11902,11904,11906,778,309,720,4531,4996,1705])). % 52.66/52.69 cnf(11913,plain, % 52.66/52.69 (~P10(f6(f6(a12)))), % 52.66/52.69 inference(scs_inference,[],[11762,11850,11789,11786,11900,11902,11904,11906,778,309,720,4531,4996,1705,82,83,88])). % 52.66/52.69 cnf(11917,plain, % 52.66/52.69 (P6(a11,f17(a2))), % 52.66/52.69 inference(scs_inference,[],[11866,11762,11850,11789,11786,11900,11902,11904,11906,45,778,309,720,4531,4996,1705,82,83,88,89,110])). % 52.66/52.69 cnf(11919,plain, % 52.66/52.69 (P6(f6(f6(a12)),f17(f6(a12)))), % 52.66/52.69 inference(scs_inference,[],[11866,11762,11850,11789,11786,11900,11902,11904,11906,45,778,309,720,4531,4996,1705,82,83,88,89,110,91])). % 52.66/52.69 cnf(11921,plain, % 52.66/52.69 (P6(f7(a4),f17(f16(a4)))), % 52.66/52.69 inference(scs_inference,[],[11866,11762,11850,11789,11786,11900,11902,11904,11906,45,778,309,720,4531,4996,1705,82,83,88,89,110,91,127])). % 52.66/52.69 cnf(11925,plain, % 52.66/52.69 (P6(f18(a4),f17(f17(f16(a4))))), % 52.66/52.69 inference(scs_inference,[],[11866,11762,11850,11784,11789,11786,11900,11902,11904,11906,45,778,309,720,4531,4996,1705,82,83,88,89,110,91,127,134,131])). % 52.66/52.69 cnf(11929,plain, % 52.66/52.69 (P10(f7(f15(x119291,f14(f17(f17(x119291))))))), % 52.66/52.69 inference(scs_inference,[],[11866,11762,11850,11784,11789,11786,11900,11902,11904,11906,45,778,309,720,4531,4996,1705,82,83,88,89,110,91,127,134,131,84,87])). % 52.66/52.69 cnf(11935,plain, % 52.66/52.69 (E(f7(a9),a11)), % 52.66/52.69 inference(scs_inference,[],[11866,11760,11762,11850,11784,11789,11786,11900,11902,11904,11906,45,778,309,720,4531,4996,1705,82,83,88,89,110,91,127,134,131,84,87,85,86,70])). % 52.66/52.69 cnf(11937,plain, % 52.66/52.69 (P1(f15(f16(a9),f18(a9)))), % 52.66/52.69 inference(scs_inference,[],[11866,11760,11762,11850,11784,11789,11786,11900,11902,11904,11906,45,778,309,720,4531,4996,1705,82,83,88,89,110,91,127,134,131,84,87,85,86,70,133])). % 52.66/52.69 cnf(11952,plain, % 52.66/52.69 (~E(a2,f10(a8,a2))), % 52.66/52.69 inference(scs_inference,[],[11866,11871,11782,11760,11762,11850,11784,11789,11786,11900,11902,11904,11906,45,778,309,720,4531,4996,1705,82,83,88,89,110,91,127,134,131,84,87,85,86,70,133,5,6,7,10,11,14,8,4,9,12,13,80,2])). % 52.66/52.69 cnf(11956,plain, % 52.66/52.69 (P6(f14(x119561),x119561)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11959,plain, % 52.66/52.69 (P6(f14(x119591),x119591)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11962,plain, % 52.66/52.69 (P6(f14(x119621),x119621)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11965,plain, % 52.66/52.69 (P6(f14(x119651),x119651)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11968,plain, % 52.66/52.69 (P6(f14(x119681),x119681)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11971,plain, % 52.66/52.69 (P6(f14(x119711),x119711)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(11973,plain, % 52.66/52.69 (E(f10(a1,a1),f10(a2,a2))), % 52.66/52.69 inference(scs_inference,[],[11866,11794,11798,11871,11782,11783,11754,11760,11762,11850,11784,11789,11786,11900,11902,11904,11906,62,11956,11959,11962,11965,11968,45,778,309,720,4531,4996,1705,82,83,88,89,110,91,127,134,131,84,87,85,86,70,133,5,6,7,10,11,14,8,4,9,12,13,80,2,109,98,99,101,102,105,106,3])). % 52.66/52.69 cnf(11976,plain, % 52.66/52.69 (P7(f6(a12),f17(a12))), % 52.66/52.69 inference(scs_inference,[],[11866,11794,11798,11871,11782,11783,11754,11760,11762,11768,11850,11784,11789,11786,11900,11902,11904,11906,68,62,11956,11959,11962,11965,11968,45,778,309,720,4531,4996,1705,82,83,88,89,110,91,127,134,131,84,87,85,86,70,133,5,6,7,10,11,14,8,4,9,12,13,80,2,109,98,99,101,102,105,106,3,108])). % 52.66/52.69 cnf(11982,plain, % 52.66/52.69 (~P6(f17(f16(a8)),f17(f7(a9)))), % 52.66/52.69 inference(scs_inference,[],[11866,11794,11798,11871,11782,11783,11754,11760,11762,11768,11850,11847,11784,11789,11786,11900,11902,11904,11906,232,68,62,11956,11959,11962,11965,11968,11971,45,778,309,720,4531,4996,1705,82,83,88,89,110,91,127,134,131,84,87,85,86,70,133,5,6,7,10,11,14,8,4,9,12,13,80,2,109,98,99,101,102,105,106,3,108,116,129])). % 52.66/52.69 cnf(11984,plain, % 52.66/52.69 (~E(f7(a9),f6(a12))), % 52.66/52.69 inference(scs_inference,[],[11866,11794,11798,11871,11782,11783,11754,11760,11762,11768,11850,11847,11784,11789,11786,11900,11902,11904,11906,232,68,62,11956,11959,11962,11965,11968,11971,45,778,309,720,4531,4996,1705,82,83,88,89,110,91,127,134,131,84,87,85,86,70,133,5,6,7,10,11,14,8,4,9,12,13,80,2,109,98,99,101,102,105,106,3,108,116,129,31])). % 52.66/52.69 cnf(11987,plain, % 52.66/52.69 (P6(f10(a8,a1),f17(f16(a8)))), % 52.66/52.69 inference(scs_inference,[],[11866,11794,11798,11871,11782,11783,11754,11760,11762,11768,11770,11850,11847,11784,11789,11786,11900,11902,11904,11906,232,68,262,69,62,11956,11959,11962,11965,11968,11971,64,45,43,65,778,309,720,4531,4996,1705,82,83,88,89,110,91,127,134,131,84,87,85,86,70,133,5,6,7,10,11,14,8,4,9,12,13,80,2,109,98,99,101,102,105,106,3,108,116,129,31,16,141])). % 52.66/52.69 cnf(11993,plain, % 52.66/52.69 (~P7(f17(a12),f6(a12))), % 52.66/52.69 inference(scs_inference,[],[11866,11794,11798,11871,11782,11783,11754,11760,11762,11768,11770,11850,11847,11784,11789,11786,11900,11902,11904,11906,232,68,262,69,62,11956,11959,11962,11965,11968,11971,64,45,43,65,778,309,720,4531,4996,1705,82,83,88,89,110,91,127,134,131,84,87,85,86,70,133,5,6,7,10,11,14,8,4,9,12,13,80,2,109,98,99,101,102,105,106,3,108,116,129,31,16,141,1044,1032,71,126])). % 52.66/52.69 cnf(12031,plain, % 52.66/52.69 (~P7(f17(f16(a8)),f14(f17(f17(f7(a9)))))), % 52.66/52.69 inference(scs_inference,[],[11982,778])). % 52.66/52.69 cnf(12035,plain, % 52.66/52.69 (P9(f7(f15(f16(a9),f18(a9))))), % 52.66/52.69 inference(scs_inference,[],[11937,11982,778,82,83])). % 52.66/52.69 cnf(12037,plain, % 52.66/52.69 (~P10(f6(f6(f6(a12))))), % 52.66/52.69 inference(scs_inference,[],[11937,11913,11982,778,82,83,88])). % 52.66/52.69 cnf(12049,plain, % 52.66/52.69 (P6(f18(a3),f17(f17(f16(a3))))), % 52.66/52.69 inference(scs_inference,[],[11869,11937,11913,11982,11925,42,778,82,83,88,89,110,91,127,134,131])). % 52.66/52.69 cnf(12051,plain, % 52.66/52.69 (P16(f7(f15(f16(a9),f18(a9))))), % 52.66/52.69 inference(scs_inference,[],[11869,11937,11913,11982,11925,42,778,82,83,88,89,110,91,127,134,131,84])). % 52.66/52.69 cnf(12053,plain, % 52.66/52.69 (P18(f7(f15(f16(a9),f18(a9))))), % 52.66/52.69 inference(scs_inference,[],[11869,11937,11913,11982,11925,42,778,82,83,88,89,110,91,127,134,131,84,85])). % 52.66/52.69 cnf(12055,plain, % 52.66/52.69 (P19(f7(f15(f16(a9),f18(a9))))), % 52.66/52.69 inference(scs_inference,[],[11869,11937,11913,11982,11925,42,778,82,83,88,89,110,91,127,134,131,84,85,86])). % 52.66/52.69 cnf(12057,plain, % 52.66/52.69 (P10(f7(f15(f16(a9),f18(a9))))), % 52.66/52.69 inference(scs_inference,[],[11869,11937,11913,11982,11925,42,778,82,83,88,89,110,91,127,134,131,84,85,86,87])). % 52.66/52.69 cnf(12061,plain, % 52.66/52.69 (P1(f15(f16(a4),f18(a4)))), % 52.66/52.69 inference(scs_inference,[],[11869,11937,11913,11982,11925,11929,42,778,82,83,88,89,110,91,127,134,131,84,85,86,87,70,133])). % 52.66/52.69 cnf(12069,plain, % 52.66/52.69 (E(f10(f10(a1,a1),x120691),f10(f10(a2,a2),x120691))), % 52.66/52.69 inference(scs_inference,[],[11869,11973,11937,11913,11982,11925,11929,42,778,82,83,88,89,110,91,127,134,131,84,85,86,87,70,133,5,6,7,10,11,14,8])). % 52.66/52.69 cnf(12071,plain, % 52.66/52.69 (E(f10(x120711,f10(a1,a1)),f10(x120711,f10(a2,a2)))), % 52.66/52.69 inference(scs_inference,[],[11869,11973,11937,11913,11982,11925,11929,42,778,82,83,88,89,110,91,127,134,131,84,85,86,87,70,133,5,6,7,10,11,14,8,4,9])). % 52.66/52.69 cnf(12072,plain, % 52.66/52.69 (E(f15(f10(a1,a1),x120721),f15(f10(a2,a2),x120721))), % 52.66/52.69 inference(scs_inference,[],[11869,11973,11937,11913,11982,11925,11929,42,778,82,83,88,89,110,91,127,134,131,84,85,86,87,70,133,5,6,7,10,11,14,8,4,9,12])). % 52.66/52.69 cnf(12073,plain, % 52.66/52.69 (E(f15(x120731,f10(a1,a1)),f15(x120731,f10(a2,a2)))), % 52.66/52.69 inference(scs_inference,[],[11869,11973,11937,11913,11982,11925,11929,42,778,82,83,88,89,110,91,127,134,131,84,85,86,87,70,133,5,6,7,10,11,14,8,4,9,12,13])). % 52.66/52.69 cnf(12076,plain, % 52.66/52.69 (~E(a1,f10(a8,a2))), % 52.66/52.69 inference(scs_inference,[],[11869,11839,11973,11937,11913,11982,11925,11929,42,778,82,83,88,89,110,91,127,134,131,84,85,86,87,70,133,5,6,7,10,11,14,8,4,9,12,13,80,2])). % 52.66/52.69 cnf(12078,plain, % 52.66/52.69 (P6(f14(x120781),x120781)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12083,plain, % 52.66/52.69 (P6(f14(x120831),x120831)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12086,plain, % 52.66/52.69 (P6(f14(x120861),x120861)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12089,plain, % 52.66/52.69 (P6(f14(x120891),x120891)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12091,plain, % 52.66/52.69 (P12(f14(f7(f15(x120911,f5(f17(x120911))))))), % 52.66/52.69 inference(scs_inference,[],[11869,11839,11973,11937,11913,11982,11925,11929,4617,11847,907,62,12078,12083,12086,12089,42,778,82,83,88,89,110,91,127,134,131,84,85,86,87,70,133,5,6,7,10,11,14,8,4,9,12,13,80,2,95,109,93,98,99,101])). % 52.66/52.69 cnf(12092,plain, % 52.66/52.69 (P6(f14(x120921),x120921)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12095,plain, % 52.66/52.69 (P6(f14(x120951),x120951)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12098,plain, % 52.66/52.69 (P6(f14(x120981),x120981)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12101,plain, % 52.66/52.69 (P6(f14(x121011),x121011)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12103,plain, % 52.66/52.69 (E(f16(a3),f16(a8))), % 52.66/52.69 inference(scs_inference,[],[11869,11839,11973,11937,11913,11982,11925,11929,11758,4617,11847,11855,907,216,62,12078,12083,12086,12089,12092,12095,12098,42,778,82,83,88,89,110,91,127,134,131,84,85,86,87,70,133,5,6,7,10,11,14,8,4,9,12,13,80,2,95,109,93,98,99,101,102,105,106,137])). % 52.66/52.69 cnf(12105,plain, % 52.66/52.69 (~P6(f17(a12),f6(a12))), % 52.66/52.69 inference(scs_inference,[],[11869,11839,11973,11993,11937,11913,11982,11925,11929,11758,4617,11847,11855,907,11762,216,62,12078,12083,12086,12089,12092,12095,12098,42,778,82,83,88,89,110,91,127,134,131,84,85,86,87,70,133,5,6,7,10,11,14,8,4,9,12,13,80,2,95,109,93,98,99,101,102,105,106,137,108])). % 52.66/52.69 cnf(12107,plain, % 52.66/52.69 (~E(a11,f6(a12))), % 52.66/52.69 inference(scs_inference,[],[11869,11839,11973,11984,11993,11935,11937,11913,11982,11925,11929,11758,4617,11847,11855,907,11762,216,62,12078,12083,12086,12089,12092,12095,12098,42,778,82,83,88,89,110,91,127,134,131,84,85,86,87,70,133,5,6,7,10,11,14,8,4,9,12,13,80,2,95,109,93,98,99,101,102,105,106,137,108,3])). % 52.66/52.69 cnf(12108,plain, % 52.66/52.69 (E(f18(a3),f18(a8))), % 52.66/52.69 inference(scs_inference,[],[11869,11839,11973,11984,11993,11935,11937,11913,11982,11925,11929,11758,4617,11847,11855,907,11762,216,62,12078,12083,12086,12089,12092,12095,12098,42,778,82,83,88,89,110,91,127,134,131,84,85,86,87,70,133,5,6,7,10,11,14,8,4,9,12,13,80,2,95,109,93,98,99,101,102,105,106,137,108,3,136])). % 52.66/52.69 cnf(12110,plain, % 52.66/52.69 (~P7(f17(a12),f6(f6(a12)))), % 52.66/52.69 inference(scs_inference,[],[11869,11839,11973,11984,11993,11935,11937,11913,11919,11982,11925,11929,11758,4617,11847,11855,907,11762,216,62,12078,12083,12086,12089,12092,12095,12098,42,778,82,83,88,89,110,91,127,134,131,84,85,86,87,70,133,5,6,7,10,11,14,8,4,9,12,13,80,2,95,109,93,98,99,101,102,105,106,137,108,3,136,130])). % 52.66/52.69 cnf(12112,plain, % 52.66/52.69 (~P6(f17(a12),f17(f14(f17(a11))))), % 52.66/52.69 inference(scs_inference,[],[11869,11839,11973,11976,11984,11993,11935,11937,11913,11919,11982,11925,11929,11758,4617,11840,11847,11855,907,11762,216,62,12078,12083,12086,12089,12092,12095,12098,42,778,82,83,88,89,110,91,127,134,131,84,85,86,87,70,133,5,6,7,10,11,14,8,4,9,12,13,80,2,95,109,93,98,99,101,102,105,106,137,108,3,136,130,129])). % 52.66/52.69 cnf(12115,plain, % 52.66/52.69 (~E(f14(f6(a12)),f17(a12))), % 52.66/52.69 inference(scs_inference,[],[11869,11839,11973,11976,11984,11993,11935,11937,11913,11919,11982,11925,11929,11758,4617,11840,11847,11855,907,11762,216,62,12078,12083,12086,12089,12092,12095,12098,12101,42,778,82,83,88,89,110,91,127,134,131,84,85,86,87,70,133,5,6,7,10,11,14,8,4,9,12,13,80,2,95,109,93,98,99,101,102,105,106,137,108,3,136,130,129,31,16])). % 52.66/52.69 cnf(12117,plain, % 52.66/52.69 (~E(f17(a12),f7(a3))), % 52.66/52.69 inference(scs_inference,[],[11869,11839,11973,11976,11984,11993,11935,11937,11913,11919,11982,11925,11929,11758,4617,11840,11847,11855,4362,907,11762,216,62,12078,12083,12086,12089,12092,12095,12098,12101,42,778,82,83,88,89,110,91,127,134,131,84,85,86,87,70,133,5,6,7,10,11,14,8,4,9,12,13,80,2,95,109,93,98,99,101,102,105,106,137,108,3,136,130,129,31,16,35])). % 52.66/52.69 cnf(12129,plain, % 52.66/52.69 (P1(f15(f16(a8),f18(a8)))), % 52.66/52.69 inference(scs_inference,[],[12049,941])). % 52.66/52.69 cnf(12134,plain, % 52.66/52.69 (~P10(f6(f6(f6(f6(a12)))))), % 52.66/52.69 inference(scs_inference,[],[12105,12061,12037,778,82,88])). % 52.66/52.69 cnf(12140,plain, % 52.66/52.69 (P6(f6(f17(x121401)),f17(f17(x121401)))), % 52.66/52.69 inference(scs_inference,[],[11870,12105,12061,12037,68,778,82,88,89,110,91])). % 52.66/52.69 cnf(12144,plain, % 52.66/52.69 (P2(f15(f16(a3),f18(a3)))), % 52.66/52.69 inference(scs_inference,[],[11870,12105,12061,12037,12049,68,778,82,88,89,110,91,127,134])). % 52.66/52.69 cnf(12146,plain, % 52.66/52.69 (P9(f7(f15(f16(a4),f18(a4))))), % 52.66/52.69 inference(scs_inference,[],[11870,12105,12061,12037,12049,68,778,82,88,89,110,91,127,134,83])). % 52.66/52.69 cnf(12148,plain, % 52.66/52.69 (P16(f7(f15(f16(a4),f18(a4))))), % 52.66/52.69 inference(scs_inference,[],[11870,12105,12061,12037,12049,68,778,82,88,89,110,91,127,134,83,84])). % 52.66/52.69 cnf(12150,plain, % 52.66/52.69 (P6(f18(a8),f17(f17(f16(a8))))), % 52.66/52.69 inference(scs_inference,[],[11870,12105,12061,12037,12049,68,43,778,82,88,89,110,91,127,134,83,84,131])). % 52.66/52.69 cnf(12152,plain, % 52.66/52.69 (P18(f7(f15(f16(a4),f18(a4))))), % 52.66/52.69 inference(scs_inference,[],[11870,12105,12061,12037,12049,68,43,778,82,88,89,110,91,127,134,83,84,131,85])). % 52.66/52.69 cnf(12154,plain, % 52.66/52.69 (P19(f7(f15(f16(a4),f18(a4))))), % 52.66/52.69 inference(scs_inference,[],[11870,12105,12061,12037,12049,68,43,778,82,88,89,110,91,127,134,83,84,131,85,86])). % 52.66/52.69 cnf(12156,plain, % 52.66/52.69 (P10(f7(f15(f16(a4),f18(a4))))), % 52.66/52.69 inference(scs_inference,[],[11870,12105,12061,12037,12049,68,43,778,82,88,89,110,91,127,134,83,84,131,85,86,87])). % 52.66/52.69 cnf(12158,plain, % 52.66/52.69 (E(f7(f15(f16(a9),f18(a9))),a11)), % 52.66/52.69 inference(scs_inference,[],[11870,12105,12061,12057,12037,12049,68,43,778,82,88,89,110,91,127,134,83,84,131,85,86,87,70])). % 52.66/52.69 cnf(12160,plain, % 52.66/52.69 (P1(f15(f16(a3),f18(a3)))), % 52.66/52.69 inference(scs_inference,[],[11870,12105,12061,12057,12037,12049,68,43,778,82,88,89,110,91,127,134,83,84,131,85,86,87,70,133])). % 52.66/52.69 cnf(12164,plain, % 52.66/52.69 (E(f17(f16(a3)),f17(f16(a8)))), % 52.66/52.69 inference(scs_inference,[],[11870,12103,12105,12061,12057,12037,12049,68,43,778,82,88,89,110,91,127,134,83,84,131,85,86,87,70,133,5,6,7])). % 52.66/52.69 cnf(12168,plain, % 52.66/52.69 (E(f10(f16(a3),x121681),f10(f16(a8),x121681))), % 52.66/52.69 inference(scs_inference,[],[11870,12103,12105,12061,12057,12037,12049,68,43,778,82,88,89,110,91,127,134,83,84,131,85,86,87,70,133,5,6,7,10,11,14,8])). % 52.66/52.69 cnf(12170,plain, % 52.66/52.69 (E(f10(x121701,f16(a3)),f10(x121701,f16(a8)))), % 52.66/52.69 inference(scs_inference,[],[11870,12103,12105,12061,12057,12037,12049,68,43,778,82,88,89,110,91,127,134,83,84,131,85,86,87,70,133,5,6,7,10,11,14,8,4,9])). % 52.66/52.69 cnf(12171,plain, % 52.66/52.69 (E(f15(f16(a3),x121711),f15(f16(a8),x121711))), % 52.66/52.69 inference(scs_inference,[],[11870,12103,12105,12061,12057,12037,12049,68,43,778,82,88,89,110,91,127,134,83,84,131,85,86,87,70,133,5,6,7,10,11,14,8,4,9,12])). % 52.66/52.69 cnf(12173,plain, % 52.66/52.69 (~E(f7(a3),f17(a12))), % 52.66/52.69 inference(scs_inference,[],[11870,12103,12105,12117,12061,12057,12037,12049,68,43,778,82,88,89,110,91,127,134,83,84,131,85,86,87,70,133,5,6,7,10,11,14,8,4,9,12,13,2])). % 52.66/52.69 cnf(12175,plain, % 52.66/52.69 (P6(f14(x121751),x121751)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12178,plain, % 52.66/52.69 (P6(f14(x121781),x121781)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12183,plain, % 52.66/52.69 (P6(f14(x121831),x121831)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12186,plain, % 52.66/52.69 (P6(f14(x121861),x121861)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12191,plain, % 52.66/52.69 (P7(a11,f17(a2))), % 52.66/52.69 inference(scs_inference,[],[11870,12076,12103,12105,12117,11917,12061,12053,12055,12057,12037,12049,68,62,12175,12178,12183,12186,43,778,82,88,89,110,91,127,134,83,84,131,85,86,87,70,133,5,6,7,10,11,14,8,4,9,12,13,2,96,103,109,104,106,137,108])). % 52.66/52.69 cnf(12204,plain, % 52.66/52.69 (P6(f18(a8),f17(f17(f16(a3))))), % 52.66/52.69 inference(scs_inference,[],[11870,12076,12103,12105,12108,12117,11917,12061,12069,12071,12072,12053,12055,12057,12037,12049,11897,285,68,11789,62,12175,12178,12183,12186,43,778,82,88,89,110,91,127,134,83,84,131,85,86,87,70,133,5,6,7,10,11,14,8,4,9,12,13,2,96,103,109,104,106,137,108,3,129,31,34,15,16])). % 52.66/52.69 cnf(12205,plain, % 52.66/52.69 (~E(f17(a12),f5(x122051))), % 52.66/52.69 inference(scs_inference,[],[11870,12076,12103,12105,12108,12117,11917,12061,12069,12071,12072,12053,12055,12057,12037,12049,11897,285,11976,212,68,11789,62,12175,12178,12183,12186,43,778,82,88,89,110,91,127,134,83,84,131,85,86,87,70,133,5,6,7,10,11,14,8,4,9,12,13,2,96,103,109,104,106,137,108,3,129,31,34,15,16,35])). % 52.66/52.69 cnf(12219,plain, % 52.66/52.69 (P4(f15(f16(a3),f18(a3)))), % 52.66/52.69 inference(scs_inference,[],[12129,632])). % 52.66/52.69 cnf(12220,plain, % 52.66/52.69 (P2(f15(f16(a8),f18(a8)))), % 52.66/52.69 inference(scs_inference,[],[12144,842])). % 52.66/52.69 cnf(12221,plain, % 52.66/52.69 (P1(f15(f16(a8),f18(a8)))), % 52.66/52.69 inference(scs_inference,[],[12160,939])). % 52.66/52.69 cnf(12228,plain, % 52.66/52.69 (P17(f7(f15(f16(a8),f18(a8))),f15(f16(a8),f18(a8)))), % 52.66/52.69 inference(scs_inference,[],[12129,12112,12134,778,82,88,89])). % 52.66/52.69 cnf(12238,plain, % 52.66/52.69 (P16(f7(f15(f16(a8),f18(a8))))), % 52.66/52.69 inference(scs_inference,[],[11907,12129,12140,12112,12134,778,82,88,89,110,127,134,83,84])). % 52.66/52.69 cnf(12240,plain, % 52.66/52.69 (P19(f7(f15(f16(a8),f18(a8))))), % 52.66/52.69 inference(scs_inference,[],[11907,12129,12140,12112,12134,778,82,88,89,110,127,134,83,84,86])). % 52.66/52.69 cnf(12244,plain, % 52.66/52.69 (P10(f7(f15(f16(a8),f18(a8))))), % 52.66/52.69 inference(scs_inference,[],[11907,12129,12140,12112,12134,778,82,88,89,110,127,134,83,84,86,85,87])). % 52.66/52.69 cnf(12248,plain, % 52.66/52.69 (P1(f15(x122481,f6(f17(x122481))))), % 52.66/52.69 inference(scs_inference,[],[11907,12129,12140,12156,12112,12134,778,82,88,89,110,127,134,83,84,86,85,87,70,133])). % 52.66/52.69 cnf(12263,plain, % 52.66/52.69 (P6(f14(x122631),x122631)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12266,plain, % 52.66/52.69 (P6(f14(x122661),x122661)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12269,plain, % 52.66/52.69 (P6(f14(x122691),x122691)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12272,plain, % 52.66/52.69 (P6(f14(x122721),x122721)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12275,plain, % 52.66/52.69 (P6(f14(x122751),x122751)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12277,plain, % 52.66/52.69 (E(f16(a8),f16(a3))), % 52.66/52.69 inference(scs_inference,[],[12205,11907,12129,12140,12073,12146,12152,12154,12156,12112,12150,12134,66,62,12263,12266,12269,12272,778,82,88,89,110,127,134,83,84,86,85,87,70,133,5,6,10,11,14,8,4,9,7,12,13,2,95,103,97,104,106,137])). % 52.66/52.69 cnf(12279,plain, % 52.66/52.69 (~P6(f17(a12),f6(f6(a12)))), % 52.66/52.69 inference(scs_inference,[],[12205,11907,12129,12110,12140,12073,12146,12152,12154,12156,12112,12150,12134,11913,66,62,12263,12266,12269,12272,778,82,88,89,110,127,134,83,84,86,85,87,70,133,5,6,10,11,14,8,4,9,7,12,13,2,95,103,97,104,106,137,108])). % 52.66/52.69 cnf(12287,plain, % 52.66/52.69 (~P6(f17(a2),f17(f7(f15(f16(a4),f18(a4)))))), % 52.66/52.69 inference(scs_inference,[],[12205,12191,11907,12129,12110,12140,12073,12146,12152,12154,12156,12112,12150,12134,11913,66,62,12263,12266,12269,12272,12275,65,778,82,88,89,110,127,134,83,84,86,85,87,70,133,5,6,10,11,14,8,4,9,7,12,13,2,95,103,97,104,106,137,108,136,123,129])). % 52.66/52.69 cnf(12289,plain, % 52.66/52.69 (~E(a11,f17(a12))), % 52.66/52.69 inference(scs_inference,[],[12205,12173,12191,11907,12129,12110,12140,12073,12146,12152,12154,12156,12112,12150,12134,11913,4353,66,62,12263,12266,12269,12272,12275,65,778,82,88,89,110,127,134,83,84,86,85,87,70,133,5,6,10,11,14,8,4,9,7,12,13,2,95,103,97,104,106,137,108,136,123,129,3])). % 52.66/52.69 cnf(12292,plain, % 52.66/52.69 (~P6(f17(f16(a3)),f17(f7(a3)))), % 52.66/52.69 inference(scs_inference,[],[12205,12173,12191,11907,12129,12110,12140,12073,12164,12146,12152,12154,12156,12112,12150,12134,12031,11850,11913,4353,66,62,12263,12266,12269,12272,12275,65,778,82,88,89,110,127,134,83,84,86,85,87,70,133,5,6,10,11,14,8,4,9,7,12,13,2,95,103,97,104,106,137,108,136,123,129,3,31,34,16])). % 52.66/52.69 cnf(12293,plain, % 52.66/52.69 (~P7(x122931,f7(f15(f16(a9),f18(a9))))), % 52.66/52.69 inference(scs_inference,[],[12205,12173,12191,11907,12129,12110,12140,12073,12164,12146,12152,12154,12156,12112,12150,12158,12134,12031,11850,11913,147,4353,66,62,12263,12266,12269,12272,12275,65,778,82,88,89,110,127,134,83,84,86,85,87,70,133,5,6,10,11,14,8,4,9,7,12,13,2,95,103,97,104,106,137,108,136,123,129,3,31,34,16,35])). % 52.66/52.69 cnf(12316,plain, % 52.66/52.69 (~P10(f6(f17(x123161)))), % 52.66/52.69 inference(scs_inference,[],[12279,12248,68,778,82,88])). % 52.66/52.69 cnf(12324,plain, % 52.66/52.69 (P2(f15(f16(a3),f18(a8)))), % 52.66/52.69 inference(scs_inference,[],[12279,12248,12204,12160,1712,68,778,82,88,89,110,127,134])). % 52.66/52.69 cnf(12326,plain, % 52.66/52.69 (P9(f7(f15(x123261,f6(f17(x123261)))))), % 52.66/52.69 inference(scs_inference,[],[12279,12248,12204,12160,1712,68,778,82,88,89,110,127,134,83])). % 52.66/52.69 cnf(12328,plain, % 52.66/52.69 (P16(f7(f15(x123281,f6(f17(x123281)))))), % 52.66/52.69 inference(scs_inference,[],[12279,12248,12204,12160,1712,68,778,82,88,89,110,127,134,83,84])). % 52.66/52.69 cnf(12330,plain, % 52.66/52.69 (P18(f7(f15(x123301,f6(f17(x123301)))))), % 52.66/52.69 inference(scs_inference,[],[12279,12248,12204,12160,1712,68,778,82,88,89,110,127,134,83,84,85])). % 52.66/52.69 cnf(12332,plain, % 52.66/52.69 (P19(f7(f15(x123321,f6(f17(x123321)))))), % 52.66/52.69 inference(scs_inference,[],[12279,12248,12204,12160,1712,68,778,82,88,89,110,127,134,83,84,85,86])). % 52.66/52.69 cnf(12334,plain, % 52.66/52.69 (P10(f7(f15(x123341,f6(f17(x123341)))))), % 52.66/52.69 inference(scs_inference,[],[12279,12248,12204,12160,1712,68,778,82,88,89,110,127,134,83,84,85,86,87])). % 52.66/52.69 cnf(12336,plain, % 52.66/52.69 (E(f7(f15(f16(a8),f18(a8))),a11)), % 52.66/52.69 inference(scs_inference,[],[12279,12248,12244,12204,12160,1712,68,778,82,88,89,110,127,134,83,84,85,86,87,70])). % 52.66/52.69 cnf(12338,plain, % 52.66/52.69 (P1(f15(f16(a3),f18(a8)))), % 52.66/52.69 inference(scs_inference,[],[12279,12248,12244,12204,12160,1712,68,778,82,88,89,110,127,134,83,84,85,86,87,70,133])). % 52.66/52.69 cnf(12346,plain, % 52.66/52.69 (E(f10(f16(a8),x123461),f10(f16(a3),x123461))), % 52.66/52.69 inference(scs_inference,[],[12277,12279,12292,12248,12244,12204,12160,1712,68,778,82,88,89,110,127,134,83,84,85,86,87,70,133,1044,5,6,10,11,14,8])). % 52.66/52.69 cnf(12348,plain, % 52.66/52.69 (E(f10(x123481,f16(a8)),f10(x123481,f16(a3)))), % 52.66/52.69 inference(scs_inference,[],[12277,12279,12292,12248,12244,12204,12160,1712,68,778,82,88,89,110,127,134,83,84,85,86,87,70,133,1044,5,6,10,11,14,8,4,9])). % 52.66/52.69 cnf(12349,plain, % 52.66/52.69 (E(f17(f16(a8)),f17(f16(a3)))), % 52.66/52.69 inference(scs_inference,[],[12277,12279,12292,12248,12244,12204,12160,1712,68,778,82,88,89,110,127,134,83,84,85,86,87,70,133,1044,5,6,10,11,14,8,4,9,7])). % 52.66/52.69 cnf(12351,plain, % 52.66/52.69 (E(f15(f16(a8),x123511),f15(f16(a3),x123511))), % 52.66/52.69 inference(scs_inference,[],[12277,12279,12292,12248,12244,12204,12160,1712,68,778,82,88,89,110,127,134,83,84,85,86,87,70,133,1044,5,6,10,11,14,8,4,9,7,1032,12])). % 52.66/52.69 cnf(12353,plain, % 52.66/52.69 (~E(f6(a12),a11)), % 52.66/52.69 inference(scs_inference,[],[12277,12107,12279,12292,12248,12244,12204,12160,1712,68,778,82,88,89,110,127,134,83,84,85,86,87,70,133,1044,5,6,10,11,14,8,4,9,7,1032,12,13,2])). % 52.66/52.69 cnf(12355,plain, % 52.66/52.69 (P6(f14(x123551),x123551)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12358,plain, % 52.66/52.69 (P6(f14(x123581),x123581)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12363,plain, % 52.66/52.69 (P6(f14(x123631),x123631)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12366,plain, % 52.66/52.69 (P6(f14(x123661),x123661)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12369,plain, % 52.66/52.69 (P6(f14(x123691),x123691)), % 52.66/52.69 inference(rename_variables,[],[62])). % 52.66/52.69 cnf(12377,plain, % 52.66/52.69 (P7(f10(a8,a1),f17(f16(a8)))), % 52.66/52.69 inference(scs_inference,[],[11952,12277,12107,11987,12220,12221,12279,12292,12248,12238,12240,12244,12204,12160,1712,12140,68,62,12355,12358,12363,12366,12369,778,82,88,89,110,127,134,83,84,85,86,87,70,133,1044,5,6,10,11,14,8,4,9,7,1032,12,13,2,96,98,109,103,105,106,137,119,108])). % 52.66/52.69 cnf(12380,plain, % 52.66/52.69 (E(f18(a8),f18(a3))), % 52.66/52.70 inference(scs_inference,[],[11952,12277,12107,11987,12220,12221,12279,12292,12248,12238,12240,12244,12204,12160,1712,12150,12140,68,66,62,12355,12358,12363,12366,12369,778,82,88,89,110,127,134,83,84,85,86,87,70,133,1044,5,6,10,11,14,8,4,9,7,1032,12,13,2,96,98,109,103,105,106,137,119,108,136])). % 52.66/52.70 cnf(12382,plain, % 52.66/52.70 (~P6(f17(a2),f17(f7(f15(f16(a8),f18(a8)))))), % 52.66/52.70 inference(scs_inference,[],[11952,12277,12107,11987,12220,12221,12279,12292,12248,12238,12240,12244,12204,12160,1712,12150,12191,12140,68,66,62,12355,12358,12363,12366,12369,778,82,88,89,110,127,134,83,84,85,86,87,70,133,1044,5,6,10,11,14,8,4,9,7,1032,12,13,2,96,98,109,103,105,106,137,119,108,136,129])). % 52.66/52.70 cnf(12392,plain, % 52.66/52.70 (P5(f5(f16(a8)),f16(a3))), % 52.66/52.70 inference(scs_inference,[],[11952,12277,12107,11987,12220,12221,12279,12168,12170,12171,12292,12248,12293,12238,12240,12244,12204,11766,12160,1712,12150,12191,12140,12037,68,66,62,12355,12358,12363,12366,12369,778,82,88,89,110,127,134,83,84,85,86,87,70,133,1044,5,6,10,11,14,8,4,9,7,1032,12,13,2,96,98,109,103,105,106,137,119,108,136,129,3,31,16,35,984])). % 52.66/52.70 cnf(12397,plain, % 52.66/52.70 (~P7(f17(f16(a8)),f10(a8,a1))), % 52.66/52.70 inference(scs_inference,[],[11952,12277,12107,11987,12220,12221,12279,12168,12170,12171,12292,12248,12293,12238,12240,12244,12204,11766,12160,1712,12150,12191,12140,12037,68,66,62,12355,12358,12363,12366,12369,778,82,88,89,110,127,134,83,84,85,86,87,70,133,1044,5,6,10,11,14,8,4,9,7,1032,12,13,2,96,98,109,103,105,106,137,119,108,136,129,3,31,16,35,984,720,71,126])). % 52.66/52.70 cnf(12412,plain, % 52.66/52.70 (P6(f5(x124121),f17(x124121))), % 52.66/52.70 inference(rename_variables,[],[65])). % 52.66/52.70 cnf(12420,plain, % 52.66/52.70 (P16(f7(f15(f16(a3),f18(a8))))), % 52.66/52.70 inference(scs_inference,[],[12392,12316,12338,65,91,110,134,82,89,127,84])). % 52.66/52.70 cnf(12422,plain, % 52.66/52.70 (P9(f7(f15(f16(a3),f18(a8))))), % 52.66/52.70 inference(scs_inference,[],[12392,12316,12338,65,91,110,134,82,89,127,84,83])). % 52.66/52.70 cnf(12424,plain, % 52.66/52.70 (~P10(f6(f6(f17(x124241))))), % 52.66/52.70 inference(scs_inference,[],[12392,12316,12338,65,91,110,134,82,89,127,84,83,88])). % 52.66/52.70 cnf(12428,plain, % 52.66/52.70 (P19(f7(f15(f16(a3),f18(a8))))), % 52.66/52.70 inference(scs_inference,[],[12392,12316,12338,65,91,110,134,82,89,127,84,83,88,85,86])). % 52.66/52.70 cnf(12430,plain, % 52.66/52.70 (P10(f7(f15(f16(a3),f18(a8))))), % 52.66/52.70 inference(scs_inference,[],[12392,12316,12338,65,91,110,134,82,89,127,84,83,88,85,86,87])). % 52.66/52.70 cnf(12434,plain, % 52.66/52.70 (P1(f15(x124341,f5(f17(x124341))))), % 52.66/52.70 inference(scs_inference,[],[12392,12316,12338,12334,65,12412,91,110,134,82,89,127,84,83,88,85,86,87,70,133])). % 52.66/52.70 cnf(12454,plain, % 52.66/52.70 (P6(f14(x124541),x124541)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12457,plain, % 52.66/52.70 (P6(f14(x124571),x124571)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12460,plain, % 52.66/52.70 (P6(f14(x124601),x124601)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12463,plain, % 52.66/52.70 (P6(f14(x124631),x124631)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12468,plain, % 52.66/52.70 (P6(f14(x124681),x124681)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12471,plain, % 52.66/52.70 (P6(f14(x124711),x124711)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12474,plain, % 52.66/52.70 (P6(f14(x124741),x124741)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12477,plain, % 52.66/52.70 (P6(f14(x124771),x124771)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12480,plain, % 52.66/52.70 (P6(f14(x124801),x124801)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12483,plain, % 52.66/52.70 (P6(f14(x124831),x124831)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12486,plain, % 52.66/52.70 (P6(f14(x124861),x124861)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12488,plain, % 52.66/52.70 (P10(f14(f17(f5(x124881))))), % 52.66/52.70 inference(scs_inference,[],[12380,12289,12392,12316,12338,12324,12326,12328,12330,12332,12334,12287,12382,12148,12051,12035,10014,244,62,12454,12457,12460,12463,12468,12471,12474,12477,12480,12483,12486,65,12412,91,110,134,82,89,127,84,83,88,85,86,87,70,133,80,1044,5,6,10,11,14,8,4,9,7,1032,12,13,2,93,101,97,98,109,103,104,105,106,112,120,117,108])). % 52.66/52.70 cnf(12490,plain, % 52.66/52.70 (P6(f14(x124901),x124901)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12493,plain, % 52.66/52.70 (E(f15(f16(a3),x124931),f15(f16(a8),x124931))), % 52.66/52.70 inference(rename_variables,[],[12171])). % 52.66/52.70 cnf(12502,plain, % 52.66/52.70 (P5(f14(f17(f18(a8))),f18(a3))), % 52.66/52.70 inference(scs_inference,[],[12380,11859,12289,12397,12392,12316,12338,12377,12144,12219,12324,12326,12328,12330,12332,12334,12287,12382,12148,12051,12035,10014,12171,12493,12164,317,244,4353,62,12454,12457,12460,12463,12468,12471,12474,12477,12480,12483,12486,12490,65,12412,91,110,134,82,89,127,84,83,88,85,86,87,70,133,80,1044,5,6,10,11,14,8,4,9,7,1032,12,13,2,93,101,97,98,109,103,104,105,106,112,120,117,108,36,129,21,17,3,34,26])). % 52.66/52.70 cnf(12504,plain, % 52.66/52.70 (P5(f18(a3),f18(a8))), % 52.66/52.70 inference(scs_inference,[],[12380,11859,12289,12397,12392,12316,12338,12377,12144,12219,12324,12326,12328,12330,12332,12334,12287,12382,12148,12051,12035,10014,12171,12493,12164,317,244,61,4353,62,12454,12457,12460,12463,12468,12471,12474,12477,12480,12483,12486,12490,65,12412,91,110,134,82,89,127,84,83,88,85,86,87,70,133,80,1044,5,6,10,11,14,8,4,9,7,1032,12,13,2,93,101,97,98,109,103,104,105,106,112,120,117,108,36,129,21,17,3,34,26,25])). % 52.66/52.70 cnf(12507,plain, % 52.66/52.70 (~P6(f17(a1),f17(f7(f15(f16(a4),f18(a4)))))), % 52.66/52.70 inference(scs_inference,[],[12380,11859,12289,12397,12392,12316,12338,12377,12144,12219,12324,12326,12328,12330,12332,12334,12287,12382,12148,12051,11773,12035,10014,12171,12493,12164,317,244,61,4353,62,12454,12457,12460,12463,12468,12471,12474,12477,12480,12483,12486,12490,65,12412,91,110,134,82,89,127,84,83,88,85,86,87,70,133,80,1044,5,6,10,11,14,8,4,9,7,1032,12,13,2,93,101,97,98,109,103,104,105,106,112,120,117,108,36,129,21,17,3,34,26,25,31,16])). % 52.66/52.70 cnf(12508,plain, % 52.66/52.70 (P7(f10(a8,a1),f17(f16(a3)))), % 52.66/52.70 inference(scs_inference,[],[12380,11859,12289,12397,12392,12316,12338,12377,12144,12219,12324,12349,12326,12328,12330,12332,12334,12287,12382,12148,12051,11773,12035,10014,12171,12493,12164,317,244,61,4353,62,12454,12457,12460,12463,12468,12471,12474,12477,12480,12483,12486,12490,65,12412,91,110,134,82,89,127,84,83,88,85,86,87,70,133,80,1044,5,6,10,11,14,8,4,9,7,1032,12,13,2,93,101,97,98,109,103,104,105,106,112,120,117,108,36,129,21,17,3,34,26,25,31,16,35])). % 52.66/52.70 cnf(12509,plain, % 52.66/52.70 (P6(f10(a8,a1),f17(f16(a3)))), % 52.66/52.70 inference(scs_inference,[],[12380,11859,12289,12397,12392,12316,12338,12377,12144,12219,12324,12349,12326,12328,12330,12332,12334,12287,12382,12148,12051,11773,12035,10014,12171,12493,12164,317,244,61,4353,62,12454,12457,12460,12463,12468,12471,12474,12477,12480,12483,12486,12490,65,12412,91,110,134,82,89,127,84,83,88,85,86,87,70,133,80,1044,5,6,10,11,14,8,4,9,7,1032,12,13,2,93,101,97,98,109,103,104,105,106,112,120,117,108,36,129,21,17,3,34,26,25,31,16,35,107])). % 52.66/52.70 cnf(12511,plain, % 52.66/52.70 (P19(f14(f17(f5(x125111))))), % 52.66/52.70 inference(scs_inference,[],[12380,11859,12289,12397,12392,12316,12338,12377,12144,12219,12324,12349,12326,12328,12330,12332,12334,12287,12382,12148,12051,11773,12035,10014,12171,12493,12164,317,244,61,4353,62,12454,12457,12460,12463,12468,12471,12474,12477,12480,12483,12486,12490,65,12412,91,110,134,82,89,127,84,83,88,85,86,87,70,133,80,1044,5,6,10,11,14,8,4,9,7,1032,12,13,2,93,101,97,98,109,103,104,105,106,112,120,117,108,36,129,21,17,3,34,26,25,31,16,35,107,79])). % 52.66/52.70 cnf(12513,plain, % 52.66/52.70 (P18(f14(f17(f5(x125131))))), % 52.66/52.70 inference(scs_inference,[],[12380,11859,12289,12397,12392,12316,12338,12377,12144,12219,12324,12349,12326,12328,12330,12332,12334,12287,12382,12148,12051,11773,12035,10014,12171,12493,12164,317,244,61,4353,62,12454,12457,12460,12463,12468,12471,12474,12477,12480,12483,12486,12490,65,12412,91,110,134,82,89,127,84,83,88,85,86,87,70,133,80,1044,5,6,10,11,14,8,4,9,7,1032,12,13,2,93,101,97,98,109,103,104,105,106,112,120,117,108,36,129,21,17,3,34,26,25,31,16,35,107,79,78])). % 52.66/52.70 cnf(12537,plain, % 52.66/52.70 (~P10(f6(f6(f6(f17(x125371)))))), % 52.66/52.70 inference(scs_inference,[],[12504,12434,12424,11863,42,110,82,89,127,84,83,88])). % 52.66/52.70 cnf(12543,plain, % 52.66/52.70 (P10(f7(f15(x125431,f5(f17(x125431)))))), % 52.66/52.70 inference(scs_inference,[],[12504,12434,12424,11863,42,110,82,89,127,84,83,88,86,85,87])). % 52.66/52.70 cnf(12545,plain, % 52.66/52.70 (E(f14(f17(f5(x125451))),a11)), % 52.66/52.70 inference(scs_inference,[],[12504,12434,12424,12488,11863,42,110,82,89,127,84,83,88,86,85,87,70])). % 52.66/52.70 cnf(12562,plain, % 52.66/52.70 (P6(f14(x125621),x125621)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12565,plain, % 52.66/52.70 (P6(f14(x125651),x125651)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12568,plain, % 52.66/52.70 (P6(f14(x125681),x125681)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12571,plain, % 52.66/52.70 (P6(f14(x125711),x125711)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12574,plain, % 52.66/52.70 (P6(f14(x125741),x125741)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12577,plain, % 52.66/52.70 (P6(f14(x125771),x125771)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12580,plain, % 52.66/52.70 (P6(f14(x125801),x125801)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12583,plain, % 52.66/52.70 (P6(f14(x125831),x125831)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12586,plain, % 52.66/52.70 (P6(f14(x125861),x125861)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12589,plain, % 52.66/52.70 (P6(f14(x125891),x125891)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12594,plain, % 52.66/52.70 (P6(f14(x125941),x125941)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12599,plain, % 52.66/52.70 (P7(f7(a9),f17(f16(a9)))), % 52.66/52.70 inference(scs_inference,[],[12504,4435,11777,12346,12434,12424,12488,12511,12513,12420,12422,12428,11863,12507,4389,11847,11768,56,68,62,12562,12565,12568,12571,12574,12577,12580,12583,12586,12589,12594,42,110,82,89,127,84,83,88,86,85,87,70,1044,5,6,10,11,14,8,4,9,7,1032,12,13,2,102,101,97,104,106,118,114,113,121,111,115,122,116,108])). % 52.66/52.70 cnf(12602,plain, % 52.66/52.70 (~P6(f17(f16(a3)),f17(f14(f17(f5(x126021)))))), % 52.66/52.70 inference(scs_inference,[],[12504,4435,12508,11777,12346,12434,12424,12488,12511,12513,12420,12422,12428,11863,12507,4389,11847,11768,56,68,62,12562,12565,12568,12571,12574,12577,12580,12583,12586,12589,12594,42,110,82,89,127,84,83,88,86,85,87,70,1044,5,6,10,11,14,8,4,9,7,1032,12,13,2,102,101,97,104,106,118,114,113,121,111,115,122,116,108,129])). % 52.66/52.70 cnf(12604,plain, % 52.66/52.70 (E(f10(f16(a8),f16(a8)),f10(f16(a3),f16(a3)))), % 52.66/52.70 inference(scs_inference,[],[12504,4435,12508,11777,12346,12348,12434,12424,12488,12511,12513,12420,12422,12428,11863,12507,4389,11847,11768,56,68,62,12562,12565,12568,12571,12574,12577,12580,12583,12586,12589,12594,42,110,82,89,127,84,83,88,86,85,87,70,1044,5,6,10,11,14,8,4,9,7,1032,12,13,2,102,101,97,104,106,118,114,113,121,111,115,122,116,108,129,3])). % 52.66/52.70 cnf(12607,plain, % 52.66/52.70 (P17(a11,f15(f16(a8),f18(a8)))), % 52.66/52.70 inference(scs_inference,[],[12504,4435,12508,11777,12346,12348,12434,12424,12488,12511,12513,12420,12422,12428,12336,12228,11863,12507,4389,11847,11768,56,68,62,12562,12565,12568,12571,12574,12577,12580,12583,12586,12589,12594,42,110,82,89,127,84,83,88,86,85,87,70,1044,5,6,10,11,14,8,4,9,7,1032,12,13,2,102,101,97,104,106,118,114,113,121,111,115,122,116,108,129,3,38])). % 52.66/52.70 cnf(12627,plain, % 52.66/52.70 (P16(f7(f15(f16(a3),f18(a3))))), % 52.66/52.70 inference(scs_inference,[],[12502,12160,110,89,82,84])). % 52.66/52.70 cnf(12637,plain, % 52.66/52.70 (P19(f7(f15(f16(a3),f18(a3))))), % 52.66/52.70 inference(scs_inference,[],[12502,12537,12160,43,110,89,82,84,88,83,127,85,86])). % 52.66/52.70 cnf(12639,plain, % 52.66/52.70 (P10(f7(f15(f16(a3),f18(a3))))), % 52.66/52.70 inference(scs_inference,[],[12502,12537,12160,43,110,89,82,84,88,83,127,85,86,87])). % 52.66/52.70 cnf(12641,plain, % 52.66/52.70 (E(f7(f15(x126411,f5(f17(x126411)))),a11)), % 52.66/52.70 inference(scs_inference,[],[12502,12543,12537,12160,43,110,89,82,84,88,83,127,85,86,87,70])). % 52.66/52.70 cnf(12649,plain, % 52.66/52.70 (E(f10(f10(f16(a8),f16(a8)),x126491),f10(f10(f16(a3),f16(a3)),x126491))), % 52.66/52.70 inference(scs_inference,[],[12604,12502,12543,12537,12602,12160,43,110,89,82,84,88,83,127,85,86,87,70,1044,5,6,10,11,14,8])). % 52.66/52.70 cnf(12650,plain, % 52.66/52.70 (E(f5(f10(f16(a8),f16(a8))),f5(f10(f16(a3),f16(a3))))), % 52.66/52.70 inference(scs_inference,[],[12604,12502,12543,12537,12602,12160,43,110,89,82,84,88,83,127,85,86,87,70,1044,5,6,10,11,14,8,4])). % 52.66/52.70 cnf(12651,plain, % 52.66/52.70 (E(f10(x126511,f10(f16(a8),f16(a8))),f10(x126511,f10(f16(a3),f16(a3))))), % 52.66/52.70 inference(scs_inference,[],[12604,12502,12543,12537,12602,12160,43,110,89,82,84,88,83,127,85,86,87,70,1044,5,6,10,11,14,8,4,9])). % 52.66/52.70 cnf(12658,plain, % 52.66/52.70 (P6(f14(x126581),x126581)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12661,plain, % 52.66/52.70 (P6(f14(x126611),x126611)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12664,plain, % 52.66/52.70 (P6(f14(x126641),x126641)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12667,plain, % 52.66/52.70 (P6(f14(x126671),x126671)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12680,plain, % 52.66/52.70 (~P6(f17(f16(a8)),f17(f14(f17(f5(x126801)))))), % 52.66/52.70 inference(scs_inference,[],[12353,12115,12599,12604,12502,12545,12543,12537,12602,12430,12428,12349,238,12160,4398,12140,62,12658,12661,12664,12667,43,110,89,82,84,88,83,127,85,86,87,70,1044,5,6,10,11,14,8,4,9,7,1032,12,13,2,99,95,102,106,130,108,129,3,31,16])). % 52.66/52.70 cnf(12704,plain, % 52.66/52.70 (P10(f7(f15(a2,f14(f17(f17(a1))))))), % 52.66/52.70 inference(scs_inference,[],[154,11863,45,42,110,89,82,84,83,85,86,87])). % 52.66/52.70 cnf(12706,plain, % 52.66/52.70 (E(f7(f15(f16(a3),f18(a3))),a11)), % 52.66/52.70 inference(scs_inference,[],[12639,154,11863,45,42,110,89,82,84,83,85,86,87,70])). % 52.66/52.70 cnf(12723,plain, % 52.66/52.70 (P6(f14(x127231),x127231)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12726,plain, % 52.66/52.70 (P6(f14(x127261),x127261)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12729,plain, % 52.66/52.70 (P6(f14(x127291),x127291)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12732,plain, % 52.66/52.70 (P6(f14(x127321),x127321)), % 52.66/52.70 inference(rename_variables,[],[62])). % 52.66/52.70 cnf(12740,plain, % 52.66/52.70 (P6(f5(x127401),f17(x127401))), % 52.66/52.70 inference(rename_variables,[],[65])). % 52.66/52.70 cnf(12745,plain, % 52.66/52.70 (~P6(f17(f16(a3)),f17(f7(f15(f16(a3),f18(a3)))))), % 52.66/52.70 inference(scs_inference,[],[293,11921,12627,12637,12639,12641,12680,12091,154,12508,11863,68,62,12723,12726,12729,12732,45,42,65,110,89,82,84,83,85,86,87,70,1044,5,6,10,11,14,8,4,9,7,1032,12,13,2,96,101,105,97,106,27,136,108,129])). % 52.66/52.70 cnf(12759,plain, % 52.66/52.70 (~E(f10(a8,a2),f10(a8,a1))), % 52.66/52.70 inference(scs_inference,[],[293,11921,12607,12627,12637,12639,12649,12651,12650,12641,12680,12091,11868,12351,154,158,297,12509,12293,12508,295,11864,12424,12599,11863,68,151,66,62,12723,12726,12729,12732,45,42,43,65,12740,110,89,82,84,83,85,86,87,70,1044,5,6,10,11,14,8,4,9,7,1032,12,13,2,96,101,105,97,106,27,136,108,129,3,39,31,16,35,142,143])). % 52.66/52.70 cnf(12803,plain, % 52.66/52.70 ($false), % 52.66/52.70 inference(scs_inference,[],[12759,12706,12745,12704,156,11783,45,43,110,89,82,84,83,85,86,87,70,1044,6,10,11,14,8,4,5,9,1032,7,12,13,2]), % 52.66/52.70 ['proof']). % 52.66/52.70 % SZS output end Proof % 52.66/52.70 % Total time : 51.910000 s %------------------------------------------------------------------------------