%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SYN138-1 : TPTP v8.2.0. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n024.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 : 300s
% DateTime : Mon Jun 24 19:04:39 EDT 2024
% Result : Unsatisfiable 58.70s 58.79s
% Output : CNFRefutation 58.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SYN138-1 : TPTP v8.2.0. Released v1.1.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n024.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sun Jun 23 23:08:24 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.60 start to proof:theBenchmark
% 58.70/58.78 %-------------------------------------------
% 58.70/58.78 % File :CSE---1.7
% 58.70/58.78 % Problem :theBenchmark
% 58.70/58.78 % Transform :cnf
% 58.70/58.78 % Format :tptp:raw
% 58.70/58.78 % Command :java -jar mcs_scs.jar %d %s
% 58.70/58.78
% 58.70/58.78 % Result :Theorem 58.080000s
% 58.70/58.78 % Output :CNFRefutation 58.080000s
% 58.70/58.78 %-------------------------------------------
% 58.70/58.79 %--------------------------------------------------------------------------
% 58.70/58.79 % File : SYN138-1 : TPTP v8.2.0. Released v1.1.0.
% 58.70/58.79 % Domain : Syntactic (Random Prolog Theory)
% 58.70/58.79 % Problem : RPT63 synthetic problem 36 (quasi-uniform distribution)
% 58.70/58.79 % Version : [SE94] axioms : Especial.
% 58.70/58.79 % English :
% 58.70/58.79
% 58.70/58.79 % Refs : [SE94] Segre & Elkan (1994), A High-Performance Explanation-B
% 58.70/58.79 % Source : [SE94]
% 58.70/58.79 % Names : - [SE94]
% 58.70/58.79
% 58.70/58.79 % Status : Unsatisfiable
% 58.70/58.79 % Rating : 0.00 v7.3.0, 0.10 v7.2.0, 0.11 v7.1.0, 0.14 v7.0.0, 0.00 v6.2.0, 0.12 v6.1.0, 0.00 v2.0.0
% 58.70/58.79 % Syntax : Number of clauses : 369 ( 39 unt; 0 nHn; 362 RR)
% 58.70/58.79 % Number of literals : 1060 ( 0 equ; 692 neg)
% 58.70/58.79 % Maximal clause size : 5 ( 2 avg)
% 58.70/58.79 % Maximal term depth : 1 ( 1 avg)
% 58.70/58.79 % Number of predicates : 48 ( 48 usr; 0 prp; 1-3 aty)
% 58.70/58.79 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% 58.70/58.79 % Number of variables : 626 ( 160 sgn)
% 58.70/58.79 % SPC : CNF_UNS_EPR_NEQ_HRN
% 58.70/58.79
% 58.70/58.79 % Comments : This theory has a finite deductive closure.
% 58.70/58.79 %--------------------------------------------------------------------------
% 58.70/58.79 %----Include Synthetic domain theory for EBL
% 58.70/58.79 include('Axioms/SYN001-0.ax').
% 58.70/58.79 %--------------------------------------------------------------------------
% 58.70/58.79 cnf(prove_this,negated_conjecture,
% 58.70/58.79 ~ m3(c,e,c) ).
% 58.70/58.79
% 58.70/58.79 %--------------------------------------------------------------------------
% 58.70/58.79 %-------------------------------------------
% 58.70/58.79 % Proof found
% 58.70/58.79 % SZS status Theorem for theBenchmark
% 58.70/58.79 % SZS output start Proof
% 58.78/58.80 %ClaNum:362(EqnAxiom:0)
% 58.78/58.80 %VarNum:1493(SingletonVarNum:573)
% 58.78/58.80 %MaxLitNum:5
% 58.78/58.80 %MaxfuncDepth:0
% 58.78/58.80 %SharedTerms:201
% 58.78/58.80 %goalClause: 39
% 58.78/58.80 %singleGoalClaCount:1
% 58.78/58.80 [1]P1(a1)
% 58.78/58.80 [2]P1(a2)
% 58.78/58.80 [3]P2(a5)
% 58.78/58.80 [4]P2(a2)
% 58.78/58.80 [5]P3(a3)
% 58.78/58.80 [6]P3(a4)
% 58.78/58.80 [7]P4(a5)
% 58.78/58.80 [8]P4(a2)
% 58.78/58.80 [10]P10(a1,a2)
% 58.78/58.80 [11]P10(a1,a4)
% 58.78/58.80 [13]P10(a3,a2)
% 58.78/58.80 [14]P10(a2,a5)
% 58.78/58.80 [15]P10(a2,a2)
% 58.78/58.80 [16]P11(a1,a5)
% 58.78/58.80 [17]P11(a1,a2)
% 58.78/58.80 [18]P11(a1,a4)
% 58.78/58.80 [19]P11(a5,a5)
% 58.78/58.80 [20]P11(a5,a2)
% 58.78/58.80 [21]P11(a3,a2)
% 58.78/58.80 [22]P11(a2,a3)
% 58.78/58.80 [23]P11(a4,a1)
% 58.78/58.80 [26]P23(a4,a2)
% 58.78/58.80 [29]P12(a1,a5,a4)
% 58.78/58.80 [32]P12(a5,a2,a4)
% 58.78/58.80 [33]P12(a3,a5,a5)
% 58.78/58.80 [34]P12(a2,a3,a3)
% 58.78/58.80 [35]P12(a2,a2,a5)
% 58.78/58.80 [36]P12(a4,a2,a3)
% 58.78/58.80 [39]~P18(a4,a5,a4)
% 58.78/58.80 [27]P10(x271,a1)
% 58.78/58.80 [28]P23(a2,x281)
% 58.78/58.80 [37]P12(a3,x371,a3)
% 58.78/58.80 [38]P12(x381,a1,x382)
% 58.78/58.80 [40]P19(a2)+~P5(a2)
% 58.78/58.80 [43]P34(a3,a3)+~P40(a3)
% 58.78/58.80 [58]P7(a5,a5)+~P15(a5,a5)
% 58.78/58.80 [59]P14(a1,a1)+~P7(a3,a1)
% 58.78/58.80 [60]P14(a4,a4)+~P7(a2,a4)
% 58.78/58.80 [79]P20(a5,a5,a5)+~P2(a5)
% 58.78/58.80 [80]P20(a2,a2,a2)+~P3(a2)
% 58.78/58.80 [81]P20(a4,a4,a4)+~P3(a4)
% 58.78/58.80 [82]P26(a4,a4,a4)+~P3(a4)
% 58.78/58.80 [83]P29(a3,a3,a3)+~P3(a3)
% 58.78/58.80 [85]P37(a2,a2,a2)+~P3(a2)
% 58.78/58.80 [86]P8(a3,a3,a3)+~P41(a3)
% 58.78/58.80 [87]P8(a4,a4,a4)+~P41(a4)
% 58.78/58.80 [116]P26(a1,a1,a1)+~P10(a1,a1)
% 58.78/58.80 [119]P18(a2,a2,a2)+~P16(a3,a2)
% 58.78/58.80 [120]P31(a2,a4,a2)+~P7(a4,a2)
% 58.78/58.80 [171]P24(a1,a1)+~P32(a4,a1,a4)
% 58.78/58.80 [213]P29(a4,a5,a2)+~P12(a2,a4,a5)
% 58.78/58.80 [214]P30(a1,a2,a2)+~P29(a1,a2,a5)
% 58.78/58.80 [215]P30(a3,a3,a3)+~P29(a5,a5,a3)
% 58.78/58.80 [216]P18(a2,a2,a2)+~P38(a3,a2,a3)
% 58.78/58.80 [46]~P41(x461)+P14(x461,x461)
% 58.78/58.80 [47]~P6(x471)+P21(x471,x471)
% 58.78/58.80 [48]~P40(x481)+P24(x481,x481)
% 58.78/58.80 [49]~P13(x491)+P34(x491,x491)
% 58.78/58.80 [50]~P6(x501)+P43(x501,x501)
% 58.78/58.80 [54]~P23(x541,x541)+P45(x541)
% 58.78/58.80 [68]~P22(x681,x681)+P34(x681,x681)
% 58.78/58.80 [69]~P35(x691,x691)+P34(x691,x691)
% 58.78/58.80 [96]~P1(x961)+P20(x961,x961,x961)
% 58.78/58.80 [97]~P2(x971)+P26(x971,x971,x971)
% 58.78/58.80 [98]~P4(x981)+P29(x981,x981,x981)
% 58.78/58.80 [100]~P1(x1001)+P37(x1001,x1001,x1001)
% 58.78/58.80 [101]~P2(x1011)+P37(x1011,x1011,x1011)
% 58.78/58.80 [102]~P5(x1021)+P30(x1021,x1021,x1021)
% 58.78/58.80 [103]~P19(x1031)+P8(x1031,x1031,x1031)
% 58.78/58.80 [104]~P25(x1041)+P8(x1041,x1041,x1041)
% 58.78/58.80 [105]~P25(x1051)+P18(x1051,x1051,x1051)
% 58.78/58.80 [106]~P25(x1061)+P31(x1061,x1061,x1061)
% 58.78/58.80 [107]~P41(x1071)+P42(x1071,x1071,x1071)
% 58.78/58.80 [108]~P44(x1081)+P42(x1081,x1081,x1081)
% 58.78/58.80 [134]P30(x1341,x1341,x1341)+~P15(x1341,a1)
% 58.78/58.80 [146]~P16(x1461,x1461)+P31(x1461,x1461,x1461)
% 58.78/58.80 [223]P30(x2231,a5,x2231)+~P26(x2231,a5,a5)
% 58.78/58.80 [224]P37(x2241,x2241,x2241)+~P12(x2241,a4,a2)
% 58.78/58.80 [225]P30(x2251,x2251,x2251)+~P26(a1,a1,x2251)
% 58.78/58.80 [227]~P37(x2271,a3,x2271)+P30(x2271,a3,x2271)
% 58.78/58.80 [243]~P37(x2431,x2431,x2431)+P30(x2431,x2431,x2431)
% 58.78/58.80 [244]~P29(x2441,x2441,x2441)+P38(x2441,x2441,x2441)
% 58.78/58.80 [247]~P30(x2471,x2471,x2471)+P18(x2471,x2471,x2471)
% 58.78/58.80 [53]P5(x531)+~P11(x532,x531)
% 58.78/58.80 [65]P15(x651,x651)+~P11(x652,x651)
% 58.78/58.80 [66]P24(x661,x661)+~P28(x662,x661)
% 58.78/58.80 [67]P24(x671,x671)+~P35(x672,x671)
% 58.78/58.80 [135]P20(x1351,x1351,x1351)+~P10(x1352,x1351)
% 58.78/58.80 [136]~P23(x1362,x1361)+P29(x1361,x1361,x1362)
% 58.78/58.80 [137]P29(x1371,x1371,x1371)+~P10(x1372,x1371)
% 58.78/58.80 [138]P29(x1381,x1381,x1381)+~P11(x1382,x1381)
% 58.78/58.80 [139]P29(x1391,x1391,x1391)+~P23(x1392,x1391)
% 58.78/58.80 [140]~P23(x1402,x1401)+P37(x1401,x1402,x1402)
% 58.78/58.80 [141]P37(x1411,x1411,x1411)+~P10(x1412,x1411)
% 58.78/58.80 [142]P37(x1421,x1421,x1421)+~P11(x1422,x1421)
% 58.78/58.80 [143]P30(x1431,x1431,x1431)+~P15(x1432,x1431)
% 58.78/58.80 [144]~P15(x1442,x1441)+P38(x1441,x1441,x1442)
% 58.78/58.80 [145]~P7(x1452,x1451)+P8(x1451,x1451,x1452)
% 58.78/58.80 [147]P42(x1471,x1471,x1471)+~P16(x1472,x1471)
% 58.78/58.80 [190]P7(x1901,x1901)+~P37(x1902,x1901,x1901)
% 58.78/58.80 [226]P26(x2261,a4,x2261)+~P12(x2262,x2261,a4)
% 58.78/58.80 [231]P38(x2311,x2311,x2311)+~P37(x2312,a4,x2311)
% 58.78/58.80 [232]P26(x2321,x2321,x2322)+~P12(a2,x2322,x2321)
% 58.78/58.80 [234]~P12(x2342,x2342,x2341)+P20(x2341,x2342,x2341)
% 58.78/58.80 [241]~P20(x2412,x2411,x2412)+P30(x2411,x2412,x2411)
% 58.78/58.80 [242]P30(x2421,x2421,x2421)+~P20(x2422,x2422,x2421)
% 58.78/58.80 [245]~P30(x2452,x2451,x2451)+P8(x2451,x2452,x2451)
% 58.78/58.80 [246]P8(x2461,x2461,x2461)+~P30(x2462,x2461,x2461)
% 58.78/58.80 [249]~P8(x2491,x2491,x2492)+P32(x2491,x2492,x2491)
% 58.78/58.80 [250]P32(x2501,x2501,x2501)+~P31(x2502,x2502,x2501)
% 58.78/58.80 [172]P25(x1721)+~P29(x1722,x1723,x1721)
% 58.78/58.80 [173]P27(x1731)+~P30(x1732,x1733,x1731)
% 58.78/58.80 [174]P13(x1741)+~P31(x1742,x1743,x1741)
% 58.78/58.80 [236]P20(x2361,x2361,x2361)+~P12(x2362,x2363,x2361)
% 58.78/58.80 [239]P37(x2391,x2391,x2391)+~P12(x2392,x2393,x2391)
% 58.78/58.80 [248]P42(x2481,x2482,x2481)+~P30(x2481,x2483,x2482)
% 58.78/58.80 [41]P44(a1)+~P1(a1)+~P45(a3)
% 58.78/58.80 [42]P44(a1)+~P39(a1)+~P45(a1)
% 58.78/58.80 [51]P25(a4)+~P4(a2)+~P15(a5,a4)
% 58.78/58.80 [90]P20(a3,a3,a3)+~P1(a1)+~P3(a3)
% 58.78/58.80 [132]~P15(a5,a4)+P30(a5,a4,a4)+~P39(a1)
% 58.78/58.80 [133]P8(a4,a4,a4)+~P44(a5)+~P7(a4,a5)
% 58.78/58.80 [164]P20(a2,a2,a2)+~P10(a4,a1)+~P15(a3,a2)
% 58.78/58.80 [165]P9(a2)+~P47(a5)+~P26(a2,a2,a2)
% 58.78/58.80 [197]P28(a5,a5)+~P14(a2,a3)+~P31(a2,a5,a3)
% 58.78/58.80 [198]P35(a2,a2)+~P15(a2,a4)+~P8(a4,a5,a2)
% 58.78/58.80 [199]P24(a2,a5)+~P28(a2,a5)+~P42(a1,a2,a4)
% 58.78/58.80 [222]P29(a3,a2,a3)+~P2(a2)+~P29(a3,a3,a3)
% 58.78/58.80 [260]P29(a1,a1,a2)+~P23(a1,a2)+~P12(a5,a3,a3)
% 58.78/58.80 [261]P30(a4,a5,a5)+~P15(a4,a2)+~P37(a5,a5,a5)
% 58.78/58.80 [300]P28(a1,a1)+~P37(a1,a1,a1)+~P8(a4,a4,a5)
% 58.78/58.80 [324]P37(a1,a1,a4)+~P12(a4,a2,a3)+~P20(a4,a1,a3)
% 58.78/58.80 [44]~P3(x441)+~P39(x441)+P41(x441)
% 58.78/58.80 [52]~P25(x521)+P14(x521,x521)+~P19(a2)
% 58.78/58.80 [56]~P45(x561)+~P6(x561)+P24(x561,x561)
% 58.78/58.80 [70]~P47(x701)+P21(x701,x701)+~P22(a5,a5)
% 58.78/58.80 [109]~P1(x1091)+P37(x1091,a2,a2)+~P1(a2)
% 58.78/58.80 [113]~P5(x1131)+P37(x1131,x1131,x1131)+~P1(a2)
% 58.78/58.80 [114]~P25(x1141)+P30(x1141,x1141,x1141)+~P5(a5)
% 58.78/58.80 [123]~P1(x1231)+~P4(x1231)+P26(x1231,x1231,x1231)
% 58.78/58.80 [148]P8(x1481,x1481,x1481)+~P15(a2,x1481)+~P41(a4)
% 58.78/58.80 [170]~P23(x1701,a1)+P26(a3,x1701,a2)+~P23(a3,a2)
% 58.78/58.80 [175]P44(x1751)+~P38(a2,x1751,a2)+~P45(a2)
% 58.78/58.81 [182]~P11(x1821,x1821)+P26(x1821,x1821,x1821)+~P10(a3,x1821)
% 58.78/58.81 [203]~P28(x2031,a1)+P24(a1,x2031)+~P8(a1,x2031,a3)
% 58.78/58.81 [228]~P30(x2281,a5,a5)+P18(x2281,a5,a5)+~P25(a5)
% 58.78/58.81 [229]~P18(x2291,a4,a3)+P32(a4,a4,x2291)+~P27(a3)
% 58.78/58.81 [230]~P20(a2,x2301,a5)+P26(a5,a5,x2301)+~P1(a2)
% 58.78/58.81 [233]P18(x2331,a4,x2331)+~P38(x2331,a4,a4)+~P44(a4)
% 58.78/58.81 [283]~P11(x2831,a1)+~P20(a3,x2831,a1)+P30(a3,x2831,a1)
% 58.78/58.81 [326]~P38(x3261,x3261,a2)+~P18(a5,x3261,a5)+P31(a5,a2,a5)
% 58.78/58.81 [328]~P12(x3281,a1,x3281)+P37(a5,x3281,x3281)+~P12(a5,a1,x3281)
% 58.78/58.81 [45]~P13(x451)+P46(x451)+~P40(x452)
% 58.78/58.81 [55]~P2(x551)+P21(x551,x551)+~P47(x552)
% 58.78/58.81 [57]~P19(x572)+~P47(x571)+P34(x571,x572)
% 58.78/58.81 [64]~P5(x641)+P17(x641)+~P35(x642,x642)
% 58.78/58.81 [72]~P15(x721,x721)+P14(x721,x721)+~P44(x722)
% 58.78/58.81 [121]~P2(x1211)+~P3(x1212)+P20(x1211,x1212,x1211)
% 58.78/58.81 [122]~P3(x1221)+~P4(x1222)+P20(x1221,x1222,x1221)
% 58.78/58.81 [124]~P1(x1241)+P29(x1241,x1241,x1241)+~P1(x1242)
% 58.78/58.81 [125]~P4(x1251)+P37(x1251,x1251,x1251)+~P3(x1252)
% 58.78/58.81 [126]~P2(x1261)+P30(x1261,x1261,x1261)+~P39(x1262)
% 58.78/58.81 [150]~P1(x1501)+P37(x1501,x1501,x1502)+~P23(x1502,a1)
% 58.78/58.81 [151]~P5(x1511)+P8(x1511,x1511,x1511)+~P16(x1512,a2)
% 58.78/58.81 [152]~P4(x1522)+P29(x1521,x1521,x1522)+~P11(a1,x1521)
% 58.78/58.81 [153]~P41(x1531)+P18(x1531,x1532,x1531)+~P7(a4,x1532)
% 58.78/58.81 [154]~P44(x1542)+P42(x1541,x1542,x1542)+~P16(a4,x1541)
% 58.78/58.81 [155]~P1(x1551)+~P23(x1551,x1552)+P20(x1551,x1552,x1551)
% 58.78/58.81 [157]~P4(x1571)+~P11(x1572,x1572)+P20(x1571,x1571,x1572)
% 58.78/58.81 [163]~P47(x1632)+~P16(x1631,x1631)+P33(x1631,x1631,x1632)
% 58.78/58.81 [180]~P12(x1802,x1801,x1801)+P13(x1801)+~P13(x1802)
% 58.78/58.81 [187]~P15(x1872,x1871)+P26(x1871,x1871,x1871)+~P11(x1872,x1871)
% 58.78/58.81 [194]~P2(x1941)+~P30(x1941,x1942,x1941)+P14(x1941,x1942)
% 58.78/58.81 [195]~P18(x1951,x1951,x1951)+P28(x1951,x1951)+~P6(x1952)
% 58.78/58.81 [210]~P30(x2102,x2101,x2101)+P36(x2101,x2101)+~P36(x2102,x2101)
% 58.78/58.81 [211]~P28(x2111,x2111)+~P31(x2111,x2112,x2112)+P28(x2111,x2112)
% 58.78/58.81 [212]~P12(x2122,x2121,x2122)+P24(x2121,x2121)+~P24(x2122,x2121)
% 58.78/58.81 [251]~P32(x2511,x2511,x2512)+P33(a2,a2,a2)+~P9(a2)
% 58.78/58.81 [252]P30(x2521,x2521,a1)+~P12(x2522,x2521,a1)+~P39(a3)
% 58.78/58.81 [253]~P29(x2531,x2532,a5)+P30(a5,x2531,x2532)+~P2(a5)
% 58.78/58.81 [254]~P5(x2541)+~P12(x2541,x2542,a5)+P26(x2541,a5,a5)
% 58.78/58.81 [255]~P4(x2552)+~P20(x2551,x2552,a2)+P29(x2551,a2,x2552)
% 58.78/58.81 [267]~P12(x2671,x2671,x2672)+P37(x2671,x2671,x2671)+~P4(x2672)
% 58.78/58.81 [268]~P4(x2682)+~P29(x2681,x2681,x2681)+P38(x2681,x2682,x2682)
% 58.78/58.81 [269]~P26(x2691,x2691,x2692)+P38(x2691,x2691,x2691)+~P5(x2692)
% 58.78/58.81 [271]~P41(x2712)+~P8(x2711,x2712,x2711)+P18(x2711,x2711,x2712)
% 58.78/58.81 [274]~P27(x2741)+P31(x2741,x2741,x2741)+~P30(x2742,x2741,x2741)
% 58.78/58.81 [275]~P2(x2751)+~P42(x2752,x2751,x2752)+P32(x2751,x2751,x2752)
% 58.78/58.81 [289]P29(x2891,x2891,x2891)+~P15(x2891,a2)+~P12(a2,x2892,a2)
% 58.78/58.81 [290]P30(x2901,x2901,x2901)+~P37(x2902,a4,x2902)+~P7(x2901,a4)
% 58.78/58.81 [294]~P23(x2941,x2941)+P30(x2941,x2941,x2941)+~P26(x2942,x2942,x2942)
% 58.78/58.81 [327]~P37(a3,x3272,x3271)+P30(x3271,a5,x3272)+~P26(a5,x3271,a3)
% 58.78/58.81 [330]P42(x3301,x3301,x3301)+~P42(x3301,x3301,x3302)+~P12(a1,x3302,x3301)
% 58.78/58.81 [62]P45(x621)+~P10(x621,x623)+~P45(x622)
% 58.78/58.81 [63]~P1(x631)+P19(x631)+~P15(x632,x633)
% 58.78/58.81 [89]P22(x891,x892)+~P16(x893,x892)+~P48(a3,x891)
% 58.78/58.81 [156]~P2(x1561)+P20(x1561,x1562,x1561)+~P23(x1563,x1562)
% 58.78/58.81 [161]~P27(x1611)+P32(x1611,x1611,x1611)+~P36(x1612,x1613)
% 58.78/58.81 [162]~P45(x1621)+P33(x1621,x1622,x1621)+~P35(x1622,x1623)
% 58.78/58.81 [181]P9(x1811)+~P42(x1813,x1811,x1811)+~P47(x1812)
% 58.78/58.81 [186]~P23(x1861,x1861)+P26(x1861,x1862,x1861)+~P23(x1862,x1863)
% 58.78/58.81 [189]P31(x1891,x1891,x1891)+~P10(x1892,x1891)+~P7(x1893,x1893)
% 58.78/58.81 [196]~P2(x1961)+P21(x1961,x1962)+~P32(x1961,x1963,x1962)
% 58.78/58.81 [208]P14(x2081,x2081)+~P16(x2082,x2082)+~P8(x2083,x2081,x2081)
% 58.78/58.81 [209]~P38(x2093,x2091,x2092)+P36(x2091,x2092)+~P11(x2093,x2091)
% 58.78/58.81 [256]~P3(x2561)+P29(x2561,x2561,x2561)+~P12(x2562,x2563,a2)
% 58.78/58.81 [258]P30(x2581,x2582,x2582)+~P5(x2583)+~P30(a5,x2581,x2582)
% 58.78/58.81 [262]~P12(x2622,x2622,x2621)+P20(x2621,x2622,x2622)+~P3(x2623)
% 58.78/58.81 [263]P26(x2631,x2631,x2631)+~P20(x2632,x2633,x2631)+~P4(x2632)
% 58.78/58.81 [264]~P3(x2641)+P29(x2641,x2641,x2641)+~P12(x2642,x2643,x2641)
% 58.78/58.81 [265]~P20(x2651,x2652,x2652)+P37(x2651,x2651,x2652)+~P2(x2653)
% 58.78/58.81 [270]~P39(x2701)+P8(x2701,x2701,x2701)+~P30(x2702,x2703,x2703)
% 58.78/58.81 [272]~P41(x2722)+~P8(x2722,x2723,x2721)+P31(x2721,x2722,x2723)
% 58.78/58.81 [273]~P5(x2731)+P31(x2731,x2731,x2731)+~P38(x2732,x2733,x2731)
% 58.78/58.81 [293]P20(x2931,x2931,x2931)+~P10(x2932,x2932)+~P20(x2933,x2932,x2931)
% 58.78/58.81 [295]P38(x2951,x2951,x2951)+~P10(x2952,x2951)+~P26(x2952,x2951,x2953)
% 58.78/58.81 [319]P14(x3191,x3191)+~P29(x3191,x3191,x3192)+~P30(x3192,x3193,x3191)
% 58.78/58.81 [329]P30(x3291,x3291,x3291)+~P30(a3,x3292,x3291)+~P20(a3,a3,x3293)
% 58.78/58.81 [333]~P26(x3332,x3331,x3332)+P26(x3331,x3331,x3331)+~P12(x3332,x3332,x3333)
% 58.78/58.81 [335]~P30(x3352,x3351,x3352)+P30(x3351,x3351,x3351)+~P20(x3352,x3353,x3351)
% 58.78/58.81 [336]P30(x3361,x3361,x3361)+~P29(x3361,x3362,x3361)+~P37(x3363,x3363,x3363)
% 58.78/58.81 [337]~P30(x3372,x3372,x3373)+P30(x3371,x3371,x3371)+~P37(x3372,x3373,x3372)
% 58.78/58.81 [338]P8(x3381,x3381,x3381)+~P20(x3381,x3381,x3382)+~P30(x3383,x3382,x3383)
% 58.78/58.81 [340]~P42(x3402,x3402,x3402)+P42(x3401,x3401,x3401)+~P31(x3402,x3401,x3403)
% 58.78/58.81 [342]~P32(x3421,x3423,x3421)+P32(x3421,x3421,x3421)+~P18(x3422,x3423,x3421)
% 58.78/58.81 [188]P37(x1881,x1882,x1881)+~P11(x1883,x1882)+~P23(x1884,x1881)
% 58.78/58.81 [201]P47(x2011)+~P15(x2011,x2012)+~P31(x2013,x2012,x2014)
% 58.78/58.81 [291]~P7(x2912,x2913)+P31(x2911,x2912,x2913)+~P38(x2914,a1,x2911)
% 58.78/58.81 [331]~P20(x3313,x3312,x3311)+P20(x3311,x3312,x3312)+~P20(x3313,x3314,x3312)
% 58.78/58.81 [332]~P12(x3322,x3323,x3321)+P26(x3321,x3321,x3322)+~P12(x3323,x3324,x3324)
% 58.78/58.81 [334]~P29(x3343,x3341,x3344)+P29(x3341,x3342,x3343)+~P12(x3343,x3341,x3344)
% 58.78/58.81 [339]P31(x3391,x3392,x3392)+~P30(x3391,x3392,x3393)+~P18(x3392,x3394,x3393)
% 58.78/58.81 [341]~P42(x3412,x3412,x3411)+P32(x3411,x3412,x3412)+~P32(x3413,x3413,x3414)
% 58.78/58.81 [71]P6(a4)+~P27(a5)+~P11(a4,a1)+~P36(a5,a2)
% 58.78/58.81 [110]P37(a2,a5,a5)+~P1(a5)+~P3(a4)+~P4(a2)
% 58.78/58.81 [184]P14(a1,a4)+~P2(a2)+~P44(a1)+~P8(a3,a4,a3)
% 58.78/58.81 [277]P26(a1,a1,a2)+~P4(a2)+~P10(a2,a5)+~P20(a1,a5,a5)
% 58.78/58.81 [278]P26(a1,a5,a5)+~P2(a2)+~P23(a1,a1)+~P26(a5,a5,a5)
% 58.78/58.81 [279]P38(a1,a3,a3)+~P45(a4)+~P10(a5,a4)+~P38(a1,a4,a3)
% 58.78/58.81 [280]P8(a1,a1,a1)+~P41(a3)+~P16(a5,a2)+~P29(a3,a1,a2)
% 58.78/58.81 [281]P18(a4,a2,a1)+~P19(a1)+~P15(a1,a2)+~P38(a2,a4,a1)
% 58.78/58.81 [130]~P5(x1301)+P29(x1301,x1301,x1301)+~P3(a4)+~P4(a5)
% 58.78/58.81 [131]~P3(x1311)+P8(x1311,x1311,x1311)+~P2(a5)+~P41(a5)
% 58.78/58.81 [296]~P5(x2961)+P37(x2961,x2961,x2961)+~P10(x2961,a2)+~P29(a2,a2,x2961)
% 58.78/58.81 [297]~P2(x2971)+~P16(x2971,x2971)+P42(x2971,a2,x2971)+~P30(a2,x2971,a2)
% 58.78/58.81 [357]P7(x3571,x3571)+~P37(x3571,x3571,a1)+~P20(x3571,a5,x3571)+~P26(a5,a1,x3571)
% 58.78/58.81 [359]~P26(a5,a5,x3591)+~P37(a5,a4,x3591)+~P29(x3591,a2,a2)+P30(a2,a4,a4)
% 58.78/58.81 [61]~P27(x612)+~P47(x611)+P43(x611,x612)+~P4(a2)
% 58.78/58.81 [74]~P5(x741)+~P15(x742,x742)+P15(x741,x741)+~P3(x742)
% 58.78/58.81 [111]~P45(x1111)+~P16(x1112,x1112)+P16(x1111,x1112)+~P11(a5,x1112)
% 58.78/58.81 [166]~P3(x1661)+P26(x1661,x1662,x1661)+~P23(a2,x1662)+~P1(a2)
% 58.78/58.81 [167]~P5(x1672)+~P16(x1672,x1671)+P38(x1671,a4,x1672)+~P3(a4)
% 58.78/58.81 [168]~P3(x1681)+P20(x1681,x1681,x1681)+~P3(x1682)+~P23(x1682,a1)
% 58.78/58.81 [169]~P5(x1692)+~P10(x1691,x1691)+P20(x1691,x1692,x1692)+~P5(a3)
% 58.78/58.81 [179]~P29(a2,x1791,x1792)+P25(a5)+~P2(a5)+~P39(a2)
% 58.78/58.81 [191]~P2(x1911)+~P23(x1912,x1912)+P26(x1911,a1,x1912)+~P15(x1912,a1)
% 58.78/58.81 [202]P39(x2021)+~P10(x2021,x2022)+~P37(a1,x2022,a1)+~P1(a1)
% 58.78/58.81 [205]~P23(x2052,x2051)+~P11(x2052,x2052)+P20(x2051,x2051,a4)+~P15(a4,a4)
% 58.78/58.81 [206]~P23(x2061,x2062)+~P15(x2062,x2062)+P29(x2061,x2061,x2061)+~P11(x2062,x2062)
% 58.78/58.81 [276]~P45(x2761)+P8(x2761,x2761,x2761)+~P44(x2762)+~P38(a1,x2762,a1)
% 58.78/58.81 [292]P37(x2921,x2921,x2921)+~P26(x2922,a1,x2921)+~P1(a2)+~P23(a2,a1)
% 58.78/58.81 [321]~P36(x3211,x3211)+~P42(x3211,a5,x3212)+~P37(a3,a3,x3212)+P6(a5)
% 58.78/58.81 [360]P26(x3601,x3601,x3601)+~P26(x3602,x3601,x3602)+~P20(a4,x3601,x3602)+~P12(a2,x3602,a4)
% 58.78/58.81 [75]~P41(x751)+P36(x751,x751)+~P16(x753,x753)+~P45(x752)
% 58.78/58.81 [76]~P39(x761)+P35(x761,x761)+~P35(x762,x763)+~P13(x762)
% 58.78/58.81 [112]P24(x1121,x1121)+~P23(x1121,x1122)+~P22(x1123,x1123)+~P9(a1)
% 58.78/58.81 [115]~P14(x1153,x1153)+P14(x1151,x1151)+~P15(x1153,x1151)+~P25(x1152)
% 58.78/58.81 [177]~P2(x1771)+~P3(x1772)+P26(x1771,x1772,x1771)+~P23(x1773,x1771)
% 58.78/58.81 [193]~P5(x1931)+~P10(x1932,x1931)+P37(x1931,x1931,x1932)+~P23(x1933,x1933)
% 58.78/58.81 [207]~P28(x2073,x2071)+P32(x2071,x2071,x2071)+~P14(x2072,x2072)+~P36(x2072,x2073)
% 58.78/58.81 [220]~P44(x2201)+~P36(x2202,x2201)+P36(x2201,x2202)+~P26(x2203,x2201,x2202)
% 58.78/58.81 [285]~P3(x2851)+~P37(x2852,x2852,x2853)+P37(x2851,x2852,x2852)+~P4(x2853)
% 58.78/58.81 [287]~P19(x2872)+~P25(x2871)+P18(x2871,x2872,x2872)+~P18(x2873,x2871,x2873)
% 58.78/58.81 [302]~P15(x3023,x3021)+~P26(x3021,x3022,x3021)+P26(x3021,x3022,x3022)+~P3(x3023)
% 58.78/58.81 [307]~P23(x3071,x3071)+P30(x3071,x3071,x3071)+~P30(x3073,x3072,x3071)+~P39(x3072)
% 58.78/58.81 [309]~P41(x3093)+~P7(x3092,x3093)+~P42(x3093,x3091,x3091)+P42(x3091,x3092,x3093)
% 58.78/58.81 [312]P37(x3121,x3121,x3121)+~P23(x3122,x3123)+~P29(x3121,a2,a2)+~P10(a2,a2)
% 58.78/58.81 [317]~P14(x3172,x3171)+P31(x3171,x3171,x3171)+~P15(x3172,x3172)+~P31(x3173,x3173,x3172)
% 58.78/58.81 [318]~P22(x3183,x3182)+~P33(x3181,x3183,x3181)+P33(x3181,x3182,x3182)+~P16(x3181,x3183)
% 58.78/58.81 [320]~P45(x3201)+P24(x3201,x3201)+~P32(x3202,x3201,x3201)+~P32(a2,a2,x3203)
% 58.78/58.81 [325]~P20(x3253,x3252,x3252)+P16(x3251,x3251)+~P23(x3252,x3251)+~P12(x3252,x3251,x3253)
% 58.78/58.81 [343]~P8(x3431,x3432,x3432)+P8(x3431,x3431,x3431)+~P45(x3432)+~P30(x3432,x3433,a5)
% 58.78/58.81 [344]~P5(x3441)+P38(x3441,x3441,x3441)+~P38(x3442,x3442,x3443)+~P26(x3443,a1,x3442)
% 58.78/58.81 [349]~P10(x3491,x3492)+~P20(x3492,a4,x3492)+P20(x3491,a3,x3492)+~P12(a3,x3493,a3)
% 58.78/58.81 [352]~P23(x3521,x3522)+~P30(x3521,x3522,x3521)+P30(x3521,x3522,x3522)+~P26(x3523,x3522,x3523)
% 58.78/58.81 [354]~P29(x3543,x3542,x3541)+~P42(x3541,x3543,x3541)+P42(x3541,x3541,x3541)+~P16(x3542,x3543)
% 58.78/58.81 [355]~P8(x3553,x3552,x3552)+P32(x3551,x3551,x3551)+~P28(x3551,x3552)+~P29(x3552,x3553,x3551)
% 58.78/58.81 [361]~P29(x3611,x3611,x3613)+~P38(x3612,x3613,x3611)+P38(x3611,x3612,x3611)+~P26(x3612,x3611,x3613)
% 58.78/58.81 [88]~P27(x881)+P40(x881)+~P23(x882,x881)+~P36(x883,x884)
% 58.78/58.81 [217]~P12(x2172,x2171,x2174)+P15(x2171,x2172)+~P23(x2174,x2171)+~P2(x2173)
% 58.78/58.81 [218]~P7(x2183,x2182)+P7(x2181,x2182)+~P20(x2184,x2182,x2181)+~P5(x2183)
% 58.78/58.81 [219]P16(x2191,x2191)+~P12(x2194,x2192,x2191)+~P23(x2193,x2193)+~P45(x2192)
% 58.78/58.81 [282]P29(x2821,x2822,x2821)+~P29(x2822,x2824,x2821)+~P3(x2823)+~P1(a2)
% 58.78/58.81 [286]~P29(x2862,x2864,x2861)+P8(x2861,x2861,x2862)+~P19(x2863)+~P19(x2864)
% 58.78/58.81 [303]~P4(x3031)+P26(x3031,x3031,x3031)+~P12(x3034,x3033,x3034)+~P10(x3032,x3033)
% 58.78/58.81 [305]P29(x3051,x3051,x3051)+~P26(x3053,x3054,x3051)+~P11(x3053,x3053)+~P3(x3052)
% 58.78/58.81 [308]~P45(x3082)+P8(x3081,x3082,x3081)+~P30(x3084,x3082,x3083)+~P11(x3081,x3083)
% 58.78/58.81 [311]~P13(x3111)+P32(x3111,x3111,x3111)+~P11(x3111,x3112)+~P32(x3113,x3114,x3113)
% 58.78/58.81 [322]~P44(x3221)+~P38(x3223,x3221,x3223)+P48(x3221,x3222)+~P12(x3223,x3224,x3222)
% 58.78/58.81 [345]~P19(x3452)+P42(x3451,x3451,x3452)+~P42(x3452,x3453,x3453)+~P18(x3454,a2,x3451)
% 58.78/58.81 [353]~P29(x3531,x3533,x3534)+~P30(x3531,x3532,x3531)+P30(x3531,x3532,x3532)+~P15(x3533,x3534)
% 58.78/58.81 [304]P29(x3041,x3041,x3041)+~P20(x3045,x3043,x3041)+~P3(x3042)+~P10(x3043,x3044)
% 58.78/58.81 [306]P29(x3061,x3061,x3061)+~P26(x3063,x3061,x3065)+~P5(x3062)+~P10(x3063,x3064)
% 58.78/58.81 [316]P8(x3161,x3161,x3162)+~P10(x3163,x3162)+~P8(x3162,x3165,x3164)+~P7(x3161,x3164)
% 58.78/58.81 [358]P35(x3581,x3582)+~P38(x3583,x3582,x3581)+~P8(x3584,x3584,x3581)+~P18(x3583,x3585,x3583)
% 58.78/58.81 [301]~P15(a5,a4)+~P16(a5,a2)+P30(a3,a4,a2)+~P39(a5)+~P20(a1,a3,a4)
% 58.78/58.81 [351]P25(a3)+~P5(a4)+~P20(a2,a3,a5)+~P26(a5,a3,a5)+~P37(a4,a3,a1)
% 58.78/58.81 [259]~P2(x2591)+P20(a4,a3,a4)+~P2(a5)+~P4(a5)+~P12(a3,a5,a4)
% 58.78/58.81 [298]~P1(x2981)+~P11(a4,x2981)+~P26(a4,a1,x2981)+P29(a1,a1,x2981)+~P2(a1)
% 58.78/58.81 [313]~P26(a4,x3131,x3131)+~P23(a2,x3131)+P30(a2,a4,a3)+~P2(a5)+~P7(a4,a3)
% 58.78/58.81 [347]~P27(x3471)+~P38(x3471,a1,x3471)+P31(x3471,a1,a5)+~P14(a2,a5)+~P30(a1,a2,a4)
% 58.78/58.81 [348]~P18(a3,x3481,x3481)+~P38(x3481,a5,x3481)+P42(a3,a3,a5)+~P19(a2)+~P7(a3,a3)
% 58.78/58.81 [192]~P23(x1921,x1922)+P20(x1921,x1922,a4)+~P10(x1922,a1)+~P1(a1)+~P2(a4)
% 58.78/58.81 [200]~P5(x2002)+P30(x2001,x2001,x2001)+~P4(x2002)+~P7(x2001,a3)+~P16(a3,x2002)
% 58.78/58.81 [221]~P5(x2211)+P36(x2211,x2211)+~P36(x2212,x2211)+~P12(x2212,a1,x2212)+~P41(a1)
% 58.78/58.81 [73]~P6(x731)+~P46(x732)+P46(x731)+~P48(x731,x733)+~P17(x732)
% 58.78/58.81 [314]~P1(x3141)+~P5(x3141)+~P12(x3143,x3143,x3143)+P26(x3141,x3141,x3141)+~P23(x3142,x3143)
% 58.78/58.81 [323]~P18(x3231,x3233,x3231)+P18(x3231,x3231,x3231)+~P7(x3232,x3233)+~P11(x3233,a3)+~P16(a3,a3)
% 58.78/58.81 [346]P30(x3461,x3461,x3462)+~P30(x3461,x3463,x3461)+~P37(a4,x3461,x3463)+~P1(a5)+~P45(a4)
% 58.78/58.81 [183]~P41(x1831)+P18(x1831,x1831,x1831)+~P1(x1832)+~P10(x1834,x1833)+~P44(x1833)
% 58.78/58.81 [204]~P3(x2041)+~P10(x2042,x2042)+P37(x2041,x2042,x2041)+~P23(x2044,x2041)+~P2(x2043)
% 58.78/58.81 [315]~P44(x3151)+~P8(x3153,x3154,x3153)+P8(x3151,x3151,x3151)+~P19(x3152)+~P15(x3153,x3154)
% 58.78/58.81 [350]~P4(x3502)+~P39(x3502)+~P38(x3502,x3502,x3502)+P38(x3501,x3502,x3501)+~P12(x3503,x3504,x3501)
% 58.78/58.81 [356]~P12(x3563,x3563,x3562)+~P12(x3561,x3564,x3564)+P18(x3561,x3562,x3561)+~P16(x3564,x3561)+~P44(x3563)
% 58.78/58.81 [362]~P26(x3622,x3624,x3624)+~P37(x3623,x3622,x3624)+P37(x3621,x3621,x3621)+~P20(x3621,x3624,x3622)+~P23(x3622,x3623)
% 58.78/58.81 [299]~P32(x2995,x2995,x2992)+P24(x2991,x2992)+~P28(x2991,x2993)+~P35(x2994,x2993)+~P24(x2995,x2992)
% 58.78/58.81 %EqnAxiom
% 58.78/58.81
% 58.78/58.81 %-------------------------------------------
% 58.78/58.88 cnf(363,plain,
% 58.78/58.88 (P26(x3631,x3631,a1)),
% 58.78/58.88 inference(scs_inference,[],[38,232])).
% 58.78/58.88 cnf(364,plain,
% 58.78/58.88 (P12(x3641,a1,x3642)),
% 58.78/58.88 inference(rename_variables,[],[38])).
% 58.78/58.88 cnf(371,plain,
% 58.78/58.88 (P23(a2,x3711)),
% 58.78/58.88 inference(rename_variables,[],[28])).
% 58.78/58.88 cnf(373,plain,
% 58.78/58.88 (P29(a5,a5,a5)),
% 58.78/58.88 inference(scs_inference,[],[38,28,1,2,7,8,16,232,109,123,150,152])).
% 58.78/58.88 cnf(378,plain,
% 58.78/58.88 (P12(x3781,a1,x3782)),
% 58.78/58.88 inference(rename_variables,[],[38])).
% 58.78/58.88 cnf(384,plain,
% 58.78/58.88 (P29(a3,x3841,a3)),
% 58.78/58.88 inference(scs_inference,[],[38,364,378,37,5,28,1,2,3,7,8,16,232,109,123,150,152,253,256,328,334])).
% 58.78/58.88 cnf(387,plain,
% 58.78/58.88 (P30(x3871,x3871,x3871)),
% 58.78/58.88 inference(scs_inference,[],[38,364,378,37,5,28,1,2,3,7,8,16,232,109,123,150,152,253,256,328,334,337])).
% 58.78/58.88 cnf(389,plain,
% 58.78/58.88 (P26(a3,x3891,a3)),
% 58.78/58.88 inference(scs_inference,[],[38,364,378,37,5,28,371,1,2,3,7,8,16,232,109,123,150,152,253,256,328,334,337,166])).
% 58.78/58.88 cnf(394,plain,
% 58.78/58.88 (P37(x3941,x3941,x3941)+~P5(x3941)),
% 58.78/58.88 inference(scs_inference,[],[38,364,378,37,5,28,371,1,2,3,7,8,16,232,109,123,150,152,253,256,328,334,337,166,292,113])).
% 58.78/58.88 cnf(395,plain,
% 58.78/58.88 (P39(x3951)),
% 58.78/58.88 inference(scs_inference,[],[38,364,378,37,5,27,28,371,1,2,3,7,8,16,232,109,123,150,152,253,256,328,334,337,166,292,113,202])).
% 58.78/58.88 cnf(406,plain,
% 58.78/58.88 (P44(a1)+~P45(a3)),
% 58.78/58.88 inference(scs_inference,[],[1,41])).
% 58.78/58.88 cnf(407,plain,
% 58.78/58.88 (P44(a1)+~P45(a1)),
% 58.78/58.88 inference(scs_inference,[],[395,42])).
% 58.78/58.88 cnf(409,plain,
% 58.78/58.88 (P6(a4)+~P27(a5)+~P36(a5,a2)),
% 58.78/58.88 inference(scs_inference,[],[23,71])).
% 58.78/58.88 cnf(410,plain,
% 58.78/58.88 (P20(a5,a5,a5)),
% 58.78/58.88 inference(scs_inference,[],[3,79])).
% 58.78/58.88 cnf(411,plain,
% 58.78/58.88 (P20(a4,a4,a4)),
% 58.78/58.88 inference(scs_inference,[],[6,81])).
% 58.78/58.88 cnf(415,plain,
% 58.78/58.88 (P29(x4151,x4151,x4151)+~P1(x4151)),
% 58.78/58.88 inference(scs_inference,[],[2,124])).
% 58.78/58.88 cnf(422,plain,
% 58.78/58.88 (P26(x4221,x4222,x4221)+~P3(x4221)+~P23(a2,x4222)),
% 58.78/58.88 inference(scs_inference,[],[2,166])).
% 58.78/58.88 cnf(423,plain,
% 58.78/58.88 (~P5(x4231)+~P16(x4231,x4232)+P38(x4232,a4,x4231)),
% 58.78/58.88 inference(scs_inference,[],[6,167])).
% 58.78/58.88 cnf(424,plain,
% 58.78/58.88 (~P29(a2,x4241,x4242)+P25(a5)),
% 58.78/58.88 inference(scs_inference,[],[3,395,179])).
% 58.78/58.88 cnf(427,plain,
% 58.78/58.88 (P37(x4271,x4272,x4271)+~P3(x4271)+~P10(x4272,x4272)+~P23(x4273,x4271)),
% 58.78/58.88 inference(scs_inference,[],[4,204])).
% 58.78/58.88 cnf(428,plain,
% 58.78/58.88 (P15(x4281,x4282)+~P23(x4283,x4281)+~P12(x4282,x4281,x4283)),
% 58.78/58.88 inference(scs_inference,[],[4,217])).
% 58.78/58.88 cnf(430,plain,
% 58.78/58.88 (P30(x4301,x4301,a1)+~P12(x4302,x4301,a1)),
% 58.78/58.88 inference(scs_inference,[],[395,252])).
% 58.78/58.88 cnf(431,plain,
% 58.78/58.88 (P30(a5,x4311,x4312)+~P29(x4311,x4312,a5)),
% 58.78/58.88 inference(scs_inference,[],[3,253])).
% 58.78/58.88 cnf(432,plain,
% 58.78/58.88 (P29(x4321,x4321,x4321)+~P3(x4321)),
% 58.78/58.88 inference(scs_inference,[],[38,256])).
% 58.78/58.88 cnf(434,plain,
% 58.78/58.88 (P20(x4341,x4342,x4342)+~P12(x4342,x4342,x4341)),
% 58.78/58.88 inference(scs_inference,[],[5,262])).
% 58.78/58.88 cnf(435,plain,
% 58.78/58.88 (P37(x4351,x4351,x4352)+~P20(x4351,x4352,x4352)),
% 58.78/58.88 inference(scs_inference,[],[4,265])).
% 58.78/58.88 cnf(437,plain,
% 58.78/58.88 (P29(x4371,x4372,x4371)+~P29(x4372,x4373,x4371)),
% 58.78/58.88 inference(scs_inference,[],[2,5,282])).
% 58.78/58.88 cnf(439,plain,
% 58.78/58.88 (P37(x4391,x4391,x4391)+~P26(x4392,a1,x4391)),
% 58.78/58.88 inference(scs_inference,[],[2,28,292])).
% 58.78/58.88 cnf(443,plain,
% 58.78/58.88 (~P11(x4431,x4431)+P29(x4432,x4432,x4432)+~P26(x4431,x4433,x4432)),
% 58.78/58.88 inference(scs_inference,[],[5,305])).
% 58.78/58.88 cnf(446,plain,
% 58.78/58.88 (~P10(x4461,x4462)+~P20(x4462,a4,x4462)+P20(x4461,a3,x4462)),
% 58.78/58.88 inference(scs_inference,[],[38,349])).
% 58.78/58.88 cnf(447,plain,
% 58.78/58.88 (P29(a2,a2,a2)),
% 58.78/58.88 inference(scs_inference,[],[2,415])).
% 58.78/58.88 cnf(449,plain,
% 58.78/58.88 (P29(a4,a4,a4)),
% 58.78/58.88 inference(scs_inference,[],[6,2,415,432])).
% 58.78/58.88 cnf(451,plain,
% 58.78/58.88 (P20(a5,a2,a2)),
% 58.78/58.88 inference(scs_inference,[],[35,6,2,415,432,434])).
% 58.78/58.88 cnf(453,plain,
% 58.78/58.88 (P37(a5,a5,a2)),
% 58.78/58.88 inference(scs_inference,[],[35,6,2,415,432,434,435])).
% 58.78/58.88 cnf(460,plain,
% 58.78/58.88 (P15(a1,x4601)),
% 58.78/58.88 inference(scs_inference,[],[35,38,6,2,389,28,415,432,434,435,439,232,428])).
% 58.78/58.88 cnf(461,plain,
% 58.78/58.88 (P12(x4611,a1,x4612)),
% 58.78/58.88 inference(rename_variables,[],[38])).
% 58.78/58.88 cnf(464,plain,
% 58.78/58.88 (P29(a1,a1,a1)),
% 58.78/58.88 inference(scs_inference,[],[35,38,6,2,363,389,19,28,415,432,434,435,439,232,428,443])).
% 58.78/58.88 cnf(473,plain,
% 58.78/58.88 (P41(a3)),
% 58.78/58.88 inference(scs_inference,[],[5,35,38,461,395,6,2,363,384,389,18,19,28,8,415,432,434,435,439,232,428,443,152,334,44])).
% 58.78/58.88 cnf(483,plain,
% 58.78/58.88 (P19(x4831)+~P1(x4831)),
% 58.78/58.88 inference(scs_inference,[],[460,63])).
% 58.78/58.88 cnf(487,plain,
% 58.78/58.88 (P19(a2)),
% 58.78/58.88 inference(scs_inference,[],[2,483])).
% 58.78/58.88 cnf(491,plain,
% 58.78/58.88 (P20(x4911,a1,a1)),
% 58.78/58.88 inference(scs_inference,[],[38,2,411,483,435,434])).
% 58.78/58.88 cnf(492,plain,
% 58.78/58.88 (P12(x4921,a1,x4922)),
% 58.78/58.88 inference(rename_variables,[],[38])).
% 58.78/58.88 cnf(496,plain,
% 58.78/58.88 (P20(a1,a3,a4)),
% 58.78/58.88 inference(scs_inference,[],[38,2,11,411,483,435,434,231,446])).
% 58.78/58.88 cnf(500,plain,
% 58.78/58.88 (P12(a3,x5001,a3)),
% 58.78/58.88 inference(rename_variables,[],[37])).
% 58.78/58.88 cnf(502,plain,
% 58.78/58.88 (P26(a5,a5,a5)),
% 58.78/58.88 inference(scs_inference,[],[37,38,492,7,2,11,410,411,483,435,434,231,446,328,263])).
% 58.78/58.88 cnf(504,plain,
% 58.78/58.88 (P15(a2,a5)),
% 58.78/58.88 inference(scs_inference,[],[37,38,492,7,2,11,26,32,410,411,483,435,434,231,446,328,263,428])).
% 58.78/58.88 cnf(508,plain,
% 58.78/58.88 (P29(x5081,x5082,a3)),
% 58.78/58.88 inference(scs_inference,[],[37,500,38,492,8,7,2,11,26,32,410,411,384,16,483,435,434,231,446,328,263,428,152,334])).
% 58.78/58.88 cnf(514,plain,
% 58.78/58.88 (P14(x5141,x5141)+~P25(x5141)),
% 58.78/58.88 inference(scs_inference,[],[37,500,38,492,6,8,7,2,11,26,32,410,411,384,15,16,28,483,435,434,231,446,328,263,428,152,334,427,52])).
% 58.78/58.88 cnf(520,plain,
% 58.78/58.88 (P8(x5201,x5201,x5202)+~P19(x5203)+~P29(x5202,x5203,x5201)),
% 58.78/58.88 inference(scs_inference,[],[487,286])).
% 58.78/58.88 cnf(523,plain,
% 58.78/58.88 (P25(a5)),
% 58.78/58.88 inference(scs_inference,[],[447,424])).
% 58.78/58.88 cnf(526,plain,
% 58.78/58.88 (~P15(x5261,x5262)+~P14(x5261,x5261)+P14(x5262,x5262)),
% 58.78/58.88 inference(scs_inference,[],[523,115])).
% 58.78/58.88 cnf(527,plain,
% 58.78/58.88 (P18(x5271,a5,a5)+~P30(x5271,a5,a5)),
% 58.78/58.88 inference(scs_inference,[],[523,228])).
% 58.78/58.88 cnf(528,plain,
% 58.78/58.88 (P18(a5,a5,a5)),
% 58.78/58.88 inference(scs_inference,[],[387,527])).
% 58.78/58.88 cnf(529,plain,
% 58.78/58.88 (P30(x5291,x5291,x5291)),
% 58.78/58.88 inference(rename_variables,[],[387])).
% 58.78/58.88 cnf(533,plain,
% 58.78/58.88 (P37(x5331,x5331,a1)),
% 58.78/58.88 inference(scs_inference,[],[387,491,523,527,514,435])).
% 58.78/58.88 cnf(535,plain,
% 58.78/58.88 (P19(a1)),
% 58.78/58.88 inference(scs_inference,[],[1,387,491,523,527,514,435,483])).
% 58.78/58.88 cnf(537,plain,
% 58.78/58.88 (P38(a1,a1,a1)),
% 58.78/58.88 inference(scs_inference,[],[1,387,491,523,527,514,435,483,231])).
% 58.78/58.88 cnf(541,plain,
% 58.78/58.88 (P29(a3,x5411,a2)),
% 58.78/58.88 inference(scs_inference,[],[34,447,1,387,508,491,487,523,527,514,435,483,231,520,334])).
% 58.78/58.88 cnf(544,plain,
% 58.78/58.88 (P16(a2,a2)),
% 58.78/58.88 inference(scs_inference,[],[35,34,447,451,1,387,508,491,487,523,28,527,514,435,483,231,520,334,325])).
% 58.78/58.88 cnf(545,plain,
% 58.78/58.88 (P23(a2,x5451)),
% 58.78/58.88 inference(rename_variables,[],[28])).
% 58.78/58.88 cnf(547,plain,
% 58.78/58.88 (P42(a2,a2,a2)),
% 58.78/58.88 inference(scs_inference,[],[35,34,447,451,1,387,529,508,491,4,487,523,28,527,514,435,483,231,520,334,325,297])).
% 58.78/58.88 cnf(556,plain,
% 58.78/58.88 (~P7(x5561,x5562)+P31(a1,x5561,x5562)),
% 58.78/58.88 inference(scs_inference,[],[35,5,34,447,451,1,387,529,508,491,4,487,523,27,28,545,527,514,435,483,231,520,334,325,297,427,151,291])).
% 58.78/58.88 cnf(560,plain,
% 58.78/58.88 (P42(x5601,x5601,x5601)+~P31(a2,x5601,x5602)),
% 58.78/58.88 inference(scs_inference,[],[35,5,34,447,451,1,387,529,508,491,4,487,523,27,28,545,527,514,435,483,231,520,334,325,297,427,151,291,526,340])).
% 58.78/58.88 cnf(570,plain,
% 58.78/58.88 (P29(a1,x5701,a1)),
% 58.78/58.88 inference(scs_inference,[],[38,464,535,520,334])).
% 58.78/58.88 cnf(571,plain,
% 58.78/58.88 (P12(x5711,a1,x5712)),
% 58.78/58.88 inference(rename_variables,[],[38])).
% 58.78/58.88 cnf(573,plain,
% 58.78/58.88 (P16(a1,a1)),
% 58.78/58.88 inference(scs_inference,[],[38,571,451,464,535,28,520,334,325])).
% 58.78/58.88 cnf(584,plain,
% 58.78/58.88 (P8(a2,a2,a3)),
% 58.78/58.88 inference(scs_inference,[],[541,487,520])).
% 58.78/58.88 cnf(587,plain,
% 58.78/58.88 (P29(a2,x5871,a4)),
% 58.78/58.88 inference(scs_inference,[],[541,36,508,487,520,334])).
% 58.78/58.88 cnf(606,plain,
% 58.78/58.88 (P8(a4,a4,a2)),
% 58.78/58.88 inference(scs_inference,[],[587,535,520])).
% 58.78/58.88 cnf(619,plain,
% 58.78/58.88 (P8(a3,a3,x6191)),
% 58.78/58.88 inference(scs_inference,[],[508,487,520])).
% 58.78/58.88 cnf(627,plain,
% 58.78/58.88 (~P29(a1,a5,a4)+P29(a5,x6271,a1)),
% 58.78/58.88 inference(scs_inference,[],[35,29,508,487,491,520,283,428,334])).
% 58.78/58.88 cnf(630,plain,
% 58.78/58.88 (P16(x6301,a2)+~P45(x6301)),
% 58.78/58.88 inference(scs_inference,[],[35,544,387,29,20,508,487,491,520,283,428,334,343,111])).
% 58.78/58.88 cnf(674,plain,
% 58.78/58.88 (P8(a1,a2,a1)+~P45(a2)),
% 58.78/58.88 inference(scs_inference,[],[35,537,17,387,491,283,428,276,308])).
% 58.78/58.88 cnf(677,plain,
% 58.78/58.88 (P38(x6771,x6771,x6771)+~P5(x6771)),
% 58.78/58.88 inference(scs_inference,[],[35,537,17,387,363,491,283,428,276,308,344])).
% 58.78/58.88 cnf(691,plain,
% 58.78/58.88 (P16(x6911,a5)+~P16(a5,a5)+~P45(x6911)),
% 58.78/58.88 inference(scs_inference,[],[35,18,387,19,460,4,491,111])).
% 58.78/58.88 cnf(739,plain,
% 58.78/58.88 (P30(x7391,x7391,x7391)),
% 58.78/58.88 inference(rename_variables,[],[387])).
% 58.78/58.88 cnf(743,plain,
% 58.78/58.88 (P8(a5,a2,a5)+~P45(a2)),
% 58.78/58.88 inference(scs_inference,[],[35,387,739,460,20,4,491,283,428,343,191,308])).
% 58.78/58.88 cnf(762,plain,
% 58.78/58.88 (P29(a2,a2,a5)),
% 58.78/58.88 inference(scs_inference,[],[7,17,152])).
% 58.78/58.88 cnf(764,plain,
% 58.78/58.88 (P29(a2,x7641,a2)),
% 58.78/58.88 inference(scs_inference,[],[35,7,17,152,334])).
% 58.78/58.88 cnf(766,plain,
% 58.78/58.88 (P30(a5,a2,a2)),
% 58.78/58.88 inference(scs_inference,[],[35,7,17,152,334,431])).
% 58.78/58.88 cnf(777,plain,
% 58.78/58.88 (P29(a4,a4,a5)),
% 58.78/58.88 inference(scs_inference,[],[7,18,152])).
% 58.78/58.88 cnf(779,plain,
% 58.78/58.88 (P30(a5,a4,a4)),
% 58.78/58.88 inference(scs_inference,[],[7,18,152,431])).
% 58.78/58.88 cnf(821,plain,
% 58.78/58.88 (P8(a2,a3,a2)+~P45(a3)),
% 58.78/58.88 inference(scs_inference,[],[35,387,19,460,491,22,4,428,283,111,191,308])).
% 58.78/58.88 cnf(845,plain,
% 58.78/58.88 (P30(x8451,x8451,x8451)),
% 58.78/58.88 inference(rename_variables,[],[387])).
% 58.78/58.88 cnf(846,plain,
% 58.78/58.88 (P8(a4,a1,a4)+~P45(a1)),
% 58.78/58.88 inference(scs_inference,[],[35,387,845,491,23,283,428,343,308])).
% 58.78/58.88 cnf(1192,plain,
% 58.78/58.88 (P38(a2,a2,a2)),
% 58.78/58.88 inference(scs_inference,[],[17,53,677])).
% 58.78/58.88 cnf(1311,plain,
% 58.78/58.88 (P8(a1,a2,a1)),
% 58.78/58.88 inference(scs_inference,[],[28,54,674])).
% 58.78/58.88 cnf(1552,plain,
% 58.78/58.88 (~P45(x15521)+P16(a3,a2)),
% 58.78/58.88 inference(scs_inference,[],[13,630,62])).
% 58.78/58.88 cnf(2063,plain,
% 58.78/58.88 (P16(a3,a2)),
% 58.78/58.88 inference(scs_inference,[],[28,1552,54])).
% 58.78/58.88 cnf(2064,plain,
% 58.78/58.88 (P18(a2,a2,a2)),
% 58.78/58.88 inference(scs_inference,[],[2063,119])).
% 58.78/58.88 cnf(2081,plain,
% 58.78/58.88 (P42(a2,a2,a1)+~P42(a1,x20811,x20811)),
% 58.78/58.88 inference(scs_inference,[],[35,2064,491,535,283,428,345])).
% 58.78/58.88 cnf(2518,plain,
% 58.78/58.88 (~P20(a3,a2,a2)+P16(a3,a3)),
% 58.78/58.88 inference(scs_inference,[],[37,34,28,387,491,283,428,343,325])).
% 58.78/58.88 cnf(3440,plain,
% 58.78/58.88 (P38(a5,a5,a5)),
% 58.78/58.88 inference(scs_inference,[],[7,98,244])).
% 58.78/58.88 cnf(3692,plain,
% 58.78/58.88 (P7(a2,a2)),
% 58.78/58.88 inference(scs_inference,[],[2,100,190])).
% 58.78/58.88 cnf(3809,plain,
% 58.78/58.88 (P7(a5,a5)),
% 58.78/58.88 inference(scs_inference,[],[3,101,190])).
% 58.78/58.88 cnf(3934,plain,
% 58.78/58.88 (P32(a1,a1,a1)),
% 58.78/58.88 inference(scs_inference,[],[535,103,249])).
% 58.78/58.88 cnf(4455,plain,
% 58.78/58.88 (P32(a3,a3,a3)),
% 58.78/58.88 inference(scs_inference,[],[473,3934,107,341])).
% 58.78/58.88 cnf(4741,plain,
% 58.78/58.88 (P31(x47411,x47411,x47411)),
% 58.78/58.88 inference(scs_inference,[],[387,173,274])).
% 58.78/58.88 cnf(4878,plain,
% 58.78/58.88 (~P5(x48781)+P7(x48781,x48781)),
% 58.78/58.88 inference(scs_inference,[],[394,190])).
% 58.78/58.88 cnf(5007,plain,
% 58.78/58.88 (~P5(x50071)+P31(a1,x50071,x50071)),
% 58.78/58.88 inference(scs_inference,[],[4878,556])).
% 58.78/58.88 cnf(6331,plain,
% 58.78/58.88 (P26(a4,x63311,a4)),
% 58.78/58.88 inference(scs_inference,[],[6,28,422])).
% 58.78/58.88 cnf(6333,plain,
% 58.78/58.88 (P41(a4)),
% 58.78/58.88 inference(scs_inference,[],[6,395,28,422,44])).
% 58.78/58.88 cnf(6334,plain,
% 58.78/58.88 (P39(x63341)),
% 58.78/58.88 inference(rename_variables,[],[395])).
% 58.78/58.88 cnf(6338,plain,
% 58.78/58.88 (P38(a3,a2,a3)),
% 58.78/58.88 inference(scs_inference,[],[6,37,3809,1192,537,395,6334,28,8,422,44,291,350])).
% 58.78/58.88 cnf(6355,plain,
% 58.78/58.88 (P8(x63551,x63551,x63551)+~P15(a2,x63551)),
% 58.78/58.88 inference(scs_inference,[],[6333,148])).
% 58.78/58.88 cnf(6356,plain,
% 58.78/58.88 (P18(a2,a2,a2)),
% 58.78/58.88 inference(scs_inference,[],[6338,216])).
% 58.78/58.88 cnf(6391,plain,
% 58.78/58.88 (P8(a5,a2,a5)),
% 58.78/58.88 inference(scs_inference,[],[28,743,54])).
% 58.78/58.88 cnf(6785,plain,
% 58.78/58.88 (P18(a2,a2,a3)+~P45(a3)),
% 58.78/58.88 inference(scs_inference,[],[473,821,271])).
% 58.78/58.88 cnf(6916,plain,
% 58.78/58.88 (P31(a4,a4,a1)+~P45(a1)),
% 58.78/58.88 inference(scs_inference,[],[6333,846,272])).
% 58.78/58.88 cnf(7047,plain,
% 58.78/58.88 (~P5(x70471)+P13(x70471)),
% 58.78/58.88 inference(scs_inference,[],[5007,174])).
% 58.78/58.88 cnf(7178,plain,
% 58.78/58.88 (P13(a2)),
% 58.78/58.88 inference(scs_inference,[],[17,7047,53])).
% 58.78/58.88 cnf(7231,plain,
% 58.78/58.88 (P38(x72311,a2,x72311)),
% 58.78/58.88 inference(scs_inference,[],[38,1192,395,8,350])).
% 58.78/58.88 cnf(9108,plain,
% 58.78/58.88 (P42(a3,a3,a2)+~P45(a3)),
% 58.78/58.88 inference(scs_inference,[],[547,487,6785,345])).
% 58.78/58.88 cnf(10094,plain,
% 58.78/58.88 (P32(a2,a3,a3)+~P45(a3)),
% 58.78/58.88 inference(scs_inference,[],[4455,9108,341])).
% 58.78/58.88 cnf(10402,plain,
% 58.78/58.88 (P8(a2,a2,a4)),
% 58.78/58.88 inference(scs_inference,[],[11,3692,606,316])).
% 58.78/58.88 cnf(10415,plain,
% 58.78/58.88 (P8(x104151,x104151,x104151)+~P45(x104151)+~P44(a2)),
% 58.78/58.88 inference(scs_inference,[],[11,33,6333,3692,7231,460,491,606,4,316,276])).
% 58.78/58.88 cnf(10479,plain,
% 58.78/58.88 (P38(x104791,a5,x104791)),
% 58.78/58.88 inference(scs_inference,[],[38,395,3440,7,350])).
% 58.78/58.88 cnf(11125,plain,
% 58.78/58.88 (P25(a2)),
% 58.78/58.88 inference(scs_inference,[],[28,136,172])).
% 58.78/58.88 cnf(11355,plain,
% 58.78/58.88 (P38(a5,a2,a2)),
% 58.78/58.88 inference(scs_inference,[],[19,8,138,268])).
% 58.78/58.88 cnf(11364,plain,
% 58.78/58.88 (~P16(a1,a4)+~P44(a2)),
% 58.78/58.88 inference(scs_inference,[],[39,34,35,38,19,491,460,4,283,428,111,191,356])).
% 58.78/58.88 cnf(11486,plain,
% 58.78/58.88 (~P16(a1,a4)+~P45(a2)),
% 58.78/58.88 inference(scs_inference,[],[7231,11364,175])).
% 58.78/58.88 cnf(11610,plain,
% 58.78/58.88 (~P16(a1,a4)),
% 58.78/58.88 inference(scs_inference,[],[28,11486,54])).
% 58.78/58.88 cnf(11735,plain,
% 58.78/58.88 (P38(x117351,x117351,x117351)),
% 58.78/58.88 inference(scs_inference,[],[28,139,244])).
% 58.78/58.88 cnf(11741,plain,
% 58.78/58.88 (~P44(x117411)+P48(x117411,x117412)),
% 58.78/58.88 inference(scs_inference,[],[38,35,11735,491,428,283,322])).
% 58.78/58.88 cnf(12502,plain,
% 58.78/58.88 (P36(a5,a2)),
% 58.78/58.88 inference(scs_inference,[],[504,19,144,209])).
% 58.78/58.88 cnf(12503,plain,
% 58.78/58.88 (P40(x125031)+~P27(x125031)+~P23(x125032,x125031)),
% 58.78/58.88 inference(scs_inference,[],[12502,88])).
% 58.78/58.88 cnf(12504,plain,
% 58.78/58.88 (P32(x125041,x125041,x125041)+~P27(x125041)),
% 58.78/58.88 inference(scs_inference,[],[12502,161])).
% 58.78/58.88 cnf(12505,plain,
% 58.78/58.88 (P6(a4)+~P27(a5)),
% 58.78/58.88 inference(scs_inference,[],[12502,409])).
% 58.78/58.88 cnf(12608,plain,
% 58.78/58.88 (P28(a2,a2)+~P27(a5)),
% 58.78/58.89 inference(scs_inference,[],[6356,12505,195])).
% 58.78/58.89 cnf(12865,plain,
% 58.78/58.89 (P32(x128651,x128651,x128651)),
% 58.78/58.89 inference(scs_inference,[],[387,12504,173])).
% 58.78/58.89 cnf(13745,plain,
% 58.78/58.89 (P42(a2,a2,a1)),
% 58.78/58.89 inference(scs_inference,[],[573,147,2081])).
% 58.78/58.89 cnf(14813,plain,
% 58.78/58.89 (P35(a5,x148131)+~P38(a2,x148131,a5)),
% 58.78/58.89 inference(scs_inference,[],[504,6356,6355,358])).
% 58.78/58.89 cnf(16288,plain,
% 58.78/58.89 (P42(a5,a5,a5)),
% 58.78/58.89 inference(scs_inference,[],[502,223,248])).
% 58.78/58.89 cnf(16896,plain,
% 58.78/58.89 (P30(a1,x168961,a1)),
% 58.78/58.89 inference(scs_inference,[],[38,234,241])).
% 58.78/58.89 cnf(17069,plain,
% 58.78/58.89 (P37(x170691,x170691,x170691)),
% 58.78/58.89 inference(scs_inference,[],[38,236,435])).
% 58.78/58.89 cnf(17560,plain,
% 58.78/58.89 (P27(a1)),
% 58.78/58.89 inference(scs_inference,[],[38,430,173])).
% 58.78/58.89 cnf(17561,plain,
% 58.78/58.89 (P40(a1)),
% 58.78/58.89 inference(scs_inference,[],[17560,28,12503])).
% 58.78/58.89 cnf(17575,plain,
% 58.78/58.89 (P46(x175751)+~P13(x175751)),
% 58.78/58.89 inference(scs_inference,[],[17561,45])).
% 58.78/58.89 cnf(17877,plain,
% 58.78/58.89 (P30(a5,a5,a2)),
% 58.78/58.89 inference(scs_inference,[],[762,437,431])).
% 58.78/58.89 cnf(18481,plain,
% 58.78/58.89 (~P29(a1,a5,a4)+P8(a1,a1,a5)),
% 58.78/58.89 inference(scs_inference,[],[535,627,520])).
% 58.78/58.89 cnf(19859,plain,
% 58.78/58.89 (P29(a1,x198591,a2)),
% 58.78/58.89 inference(scs_inference,[],[38,587,334])).
% 58.78/58.89 cnf(19863,plain,
% 58.78/58.89 (P8(a2,a2,a1)),
% 58.78/58.89 inference(scs_inference,[],[38,587,487,334,520])).
% 58.78/58.89 cnf(20551,plain,
% 58.78/58.89 (P8(a1,a1,a5)),
% 58.78/58.89 inference(scs_inference,[],[38,508,18481,334])).
% 58.78/58.89 cnf(22012,plain,
% 58.78/58.89 (P30(a5,a3,a5)),
% 58.78/58.89 inference(scs_inference,[],[5,7,122,241])).
% 58.78/58.89 cnf(22013,plain,
% 58.78/58.89 (P30(a3,a5,a5)+~P5(x220131)),
% 58.78/58.89 inference(scs_inference,[],[22012,258])).
% 58.78/58.89 cnf(22168,plain,
% 58.78/58.89 (P30(a3,a5,a5)),
% 58.78/58.89 inference(scs_inference,[],[22,22013,53])).
% 58.78/58.89 cnf(22687,plain,
% 58.78/58.89 (P8(a1,a3,a1)+~P45(a3)),
% 58.78/58.89 inference(scs_inference,[],[37,491,16,19,22012,16288,181,283,428,111,308])).
% 58.78/58.89 cnf(22831,plain,
% 58.78/58.89 (P18(a1,a1,a3)+~P45(a3)),
% 58.78/58.89 inference(scs_inference,[],[473,22687,271])).
% 58.78/58.89 cnf(24324,plain,
% 58.78/58.89 (~P45(x243241)+~P45(a1)+P16(x243241,a5)),
% 58.78/58.89 inference(scs_inference,[],[38,28,691,219])).
% 58.78/58.89 cnf(24487,plain,
% 58.78/58.89 (P16(a2,a5)+~P45(a1)),
% 58.78/58.89 inference(scs_inference,[],[28,24324,54])).
% 58.78/58.89 cnf(25140,plain,
% 58.78/58.89 (P8(a5,a5,a1)),
% 58.78/58.89 inference(scs_inference,[],[27,3809,20551,316])).
% 58.78/58.89 cnf(25313,plain,
% 58.78/58.89 (P8(x253131,x253131,x253131)+~P45(x253132)+~P44(a2)),
% 58.78/58.89 inference(scs_inference,[],[27,10415,62])).
% 58.78/58.89 cnf(26680,plain,
% 58.78/58.89 (P35(a2,a2)+~P45(x266801)+~P44(a2)),
% 58.78/58.89 inference(scs_inference,[],[6356,11735,25313,358])).
% 58.78/58.89 cnf(26845,plain,
% 58.78/58.89 (P35(a2,a2)+~P44(a2)),
% 58.78/58.89 inference(scs_inference,[],[28,26680,54])).
% 58.78/58.89 cnf(27011,plain,
% 58.78/58.89 (P35(x270111,x270111)+~P44(a2)),
% 58.78/58.89 inference(scs_inference,[],[7178,395,26845,76])).
% 58.78/58.89 cnf(27177,plain,
% 58.78/58.89 (P24(x271771,x271771)+~P44(a2)),
% 58.78/58.89 inference(scs_inference,[],[27011,67])).
% 58.78/58.89 cnf(27331,plain,
% 58.78/58.89 (P24(x273311,x273311)+~P45(a2)),
% 58.78/58.89 inference(scs_inference,[],[11735,27177,175])).
% 58.78/58.89 cnf(27485,plain,
% 58.78/58.89 (P24(x274851,x274851)),
% 58.78/58.89 inference(scs_inference,[],[28,27331,54])).
% 58.78/58.89 cnf(27652,plain,
% 58.78/58.89 (P22(x276521,a2)+~P45(x276522)+~P48(a3,x276521)),
% 58.78/58.89 inference(scs_inference,[],[20,544,89,111])).
% 58.78/58.89 cnf(27820,plain,
% 58.78/58.89 (~P48(a3,x278201)+P22(x278201,a2)),
% 58.78/58.89 inference(scs_inference,[],[28,27652,54])).
% 58.78/58.89 cnf(27978,plain,
% 58.78/58.89 (~P44(a3)+P22(x279781,a2)),
% 58.78/58.89 inference(scs_inference,[],[27820,11741])).
% 58.78/58.89 cnf(28137,plain,
% 58.78/58.89 (P22(x281371,a2)+~P38(a2,a3,a2)+~P45(a2)),
% 58.78/58.89 inference(scs_inference,[],[27978,175])).
% 58.78/58.89 cnf(28612,plain,
% 58.78/58.89 (P42(x286121,a1,a1)+~P16(a4,x286121)+~P45(a3)),
% 58.78/58.89 inference(scs_inference,[],[154,406])).
% 58.78/58.89 cnf(28771,plain,
% 58.78/58.89 (P30(x287711,a2,x287711)),
% 58.78/58.89 inference(scs_inference,[],[2,28,155,241])).
% 58.78/58.89 cnf(28772,plain,
% 58.78/58.89 (P30(a2,a5,a5)+~P5(x287721)),
% 58.78/58.89 inference(scs_inference,[],[17560,28771,258])).
% 58.78/58.89 cnf(28830,plain,
% 58.78/58.89 (P30(a4,a2,a2)),
% 58.78/58.89 inference(scs_inference,[],[17560,26,389,28771,352])).
% 58.78/58.89 cnf(28929,plain,
% 58.78/58.89 (P30(a2,a5,a5)),
% 58.78/58.89 inference(scs_inference,[],[17,28772,53])).
% 58.78/58.89 cnf(28930,plain,
% 58.78/58.89 (P18(a2,a5,a5)),
% 58.78/58.89 inference(scs_inference,[],[28929,527])).
% 58.78/58.89 cnf(29089,plain,
% 58.78/58.89 (P20(a3,a3,a2)),
% 58.78/58.89 inference(scs_inference,[],[4,28,13,156,446])).
% 58.78/58.89 cnf(29251,plain,
% 58.78/58.89 (~P5(a2)+P7(a5,a2)),
% 58.78/58.89 inference(scs_inference,[],[8,19,3692,157,218])).
% 58.78/58.89 cnf(29421,plain,
% 58.78/58.89 (P7(a5,a2)),
% 58.78/58.89 inference(scs_inference,[],[17,29251,53])).
% 58.78/58.89 cnf(29758,plain,
% 58.78/58.89 (P38(a2,a4,a3)),
% 58.78/58.89 inference(scs_inference,[],[2063,22,423,53])).
% 58.78/58.89 cnf(32068,plain,
% 58.78/58.89 (P30(x320681,a3,x320681)),
% 58.78/58.89 inference(scs_inference,[],[22,28,188,227])).
% 58.78/58.89 cnf(32070,plain,
% 58.78/58.89 (P30(a2,a3,a3)),
% 58.78/58.89 inference(scs_inference,[],[17560,28,389,32068,352])).
% 58.78/58.89 cnf(33436,plain,
% 58.78/58.89 (P27(x334361)),
% 58.78/58.89 inference(scs_inference,[],[28771,173])).
% 58.78/58.89 cnf(33440,plain,
% 58.78/58.89 (P25(a3)),
% 58.78/58.89 inference(scs_inference,[],[28771,508,10402,173,249,172])).
% 58.78/58.89 cnf(33442,plain,
% 58.78/58.89 (P47(a1)),
% 58.78/58.89 inference(scs_inference,[],[28771,508,460,4741,10402,173,249,172,201])).
% 58.78/58.89 cnf(33443,plain,
% 58.78/58.89 (P31(x334431,x334431,x334431)),
% 58.78/58.89 inference(rename_variables,[],[4741])).
% 58.78/58.89 cnf(33445,plain,
% 58.78/58.89 (P38(a1,a5,a5)),
% 58.78/58.89 inference(scs_inference,[],[7,28771,570,508,460,4741,10402,173,249,172,201,268])).
% 58.78/58.89 cnf(33454,plain,
% 58.78/58.89 (P18(x334541,x334541,x334541)),
% 58.78/58.89 inference(scs_inference,[],[17560,7,28771,570,508,547,460,4741,33443,387,533,10402,173,249,172,201,268,190,12608,174,247])).
% 58.78/58.89 cnf(33456,plain,
% 58.78/58.89 (P8(a5,a3,a5)),
% 58.78/58.89 inference(scs_inference,[],[17560,7,28771,570,508,22168,547,460,4741,33443,387,533,10402,173,249,172,201,268,190,12608,174,247,245])).
% 58.78/58.89 cnf(33458,plain,
% 58.78/58.89 (P42(a3,a5,a3)),
% 58.78/58.89 inference(scs_inference,[],[17560,7,28771,570,508,22168,547,460,4741,33443,387,533,10402,173,249,172,201,268,190,12608,174,247,245,248])).
% 58.78/58.89 cnf(33462,plain,
% 58.78/58.89 (P31(a3,a5,a5)),
% 58.78/58.89 inference(scs_inference,[],[17560,528,7,28771,570,508,22168,547,460,4741,33443,387,533,10402,173,249,172,201,268,190,12608,174,247,245,248,17575,339])).
% 58.78/58.89 cnf(33470,plain,
% 58.78/58.89 (P33(a1,a1,a1)),
% 58.78/58.89 inference(scs_inference,[],[6333,13745,573,17560,528,7,28771,570,508,22168,547,460,4741,33443,387,533,1311,10402,606,12865,173,249,172,201,268,190,12608,174,247,245,248,17575,339,271,272,341,163])).
% 58.78/58.89 cnf(33475,plain,
% 58.78/58.89 (P8(a1,a1,a2)),
% 58.78/58.89 inference(scs_inference,[],[6333,13745,573,11735,17560,528,7,28771,19,570,508,22168,547,460,4741,33443,387,13,533,1311,10402,19863,606,12865,173,249,172,201,268,190,12608,174,247,245,248,17575,339,271,272,341,163,209,316])).
% 58.78/58.89 cnf(33489,plain,
% 58.78/58.89 (P8(a4,a3,a4)+~P45(a3)),
% 58.78/58.89 inference(scs_inference,[],[35,6333,13745,573,11735,17560,528,7,28771,19,570,508,22168,32068,547,460,4741,33443,387,13,491,533,23,496,1311,10402,19863,606,12865,173,249,172,201,268,190,12608,174,247,245,248,17575,339,271,272,341,163,209,316,560,331,428,283,354,308])).
% 58.78/58.89 cnf(33493,plain,
% 58.78/58.89 (P32(a4,a4,x334931)+~P18(x334931,a4,a3)),
% 58.78/58.89 inference(scs_inference,[],[33436,229])).
% 58.78/58.89 cnf(33495,plain,
% 58.78/58.89 (P6(a4)),
% 58.78/58.89 inference(scs_inference,[],[33436,12505])).
% 58.78/58.89 cnf(33496,plain,
% 58.78/58.89 (P8(x334961,x334961,x334961)),
% 58.78/58.89 inference(scs_inference,[],[387,245])).
% 58.78/58.89 cnf(33498,plain,
% 58.78/58.89 (P42(x334981,x334981,x334981)),
% 58.78/58.89 inference(scs_inference,[],[28771,387,245,248])).
% 58.78/58.89 cnf(33500,plain,
% 58.78/58.89 (P7(x335001,x335001)),
% 58.78/58.89 inference(scs_inference,[],[28771,387,17069,245,248,190])).
% 58.78/58.89 cnf(33509,plain,
% 58.78/58.89 (P18(a5,a5,a3)),
% 58.78/58.89 inference(scs_inference,[],[13745,473,7231,28771,17,387,17069,25140,33456,12865,245,248,190,249,341,209,271])).
% 58.78/58.89 cnf(33513,plain,
% 58.78/58.89 (P38(a3,a5,a5)),
% 58.78/58.89 inference(scs_inference,[],[13745,473,7231,7,28771,508,17,387,17069,25140,33456,619,12865,245,248,190,249,341,209,271,272,268])).
% 58.78/58.89 cnf(33519,plain,
% 58.78/58.89 (P20(x335191,a2,a2)+~P20(a3,a2,x335191)),
% 58.78/58.89 inference(scs_inference,[],[13745,473,7231,28930,33436,7,28771,508,17,387,17069,25140,33456,29089,619,12865,245,248,190,249,341,209,271,272,268,339,331])).
% 58.78/58.89 cnf(33535,plain,
% 58.78/58.89 (P28(x335351,x335351)+~P18(x335351,x335351,x335351)),
% 58.78/58.89 inference(scs_inference,[],[33495,195])).
% 58.78/58.89 cnf(33537,plain,
% 58.78/58.89 (P28(x335371,x335371)),
% 58.78/58.89 inference(scs_inference,[],[33454,33535])).
% 58.78/58.89 cnf(33541,plain,
% 58.78/58.89 (P42(a5,a2,a5)),
% 58.78/58.89 inference(scs_inference,[],[33454,17877,779,33535,245,248])).
% 58.78/58.89 cnf(33545,plain,
% 58.78/58.89 (P31(a1,a5,a2)),
% 58.78/58.89 inference(scs_inference,[],[29421,11735,33454,17877,779,33475,33535,245,248,249,291])).
% 58.78/58.89 cnf(33550,plain,
% 58.78/58.89 (P36(a2,a2)),
% 58.78/58.89 inference(scs_inference,[],[13745,29421,11735,11355,33454,17877,20,779,33475,12865,33535,245,248,249,291,341,209])).
% 58.78/58.89 cnf(33563,plain,
% 58.78/58.89 (P31(x335631,a5,a5)+~P30(x335631,a5,a3)),
% 58.78/58.89 inference(scs_inference,[],[6333,13745,29421,11735,33509,11355,33454,33436,7,764,17877,20,779,6391,33475,12865,33535,245,248,249,291,341,209,268,272,14813,162,271,339])).
% 58.78/58.89 cnf(33578,plain,
% 58.78/58.89 (P32(a3,x335781,a3)),
% 58.78/58.89 inference(scs_inference,[],[28929,619,28830,245,248,249])).
% 58.78/58.89 cnf(33586,plain,
% 58.78/58.89 (P42(a4,a4,a2)),
% 58.78/58.89 inference(scs_inference,[],[6333,13745,33436,7,449,28929,619,28830,33498,12865,487,245,248,249,341,271,268,345])).
% 58.78/58.89 cnf(33640,plain,
% 58.78/58.89 (P35(x336401,x336401)),
% 58.78/58.89 inference(scs_inference,[],[13745,11735,33454,33578,33436,33496,606,766,779,245,248,249,341,358])).
% 58.78/58.89 cnf(33644,plain,
% 58.78/58.89 (P33(x336441,x336442,x336441)+~P45(x336441)),
% 58.78/58.89 inference(scs_inference,[],[13745,11735,33454,33578,33436,33496,606,766,779,245,248,249,341,358,162])).
% 58.78/58.89 cnf(33663,plain,
% 58.78/58.89 (P42(a4,a2,a4)),
% 58.78/58.89 inference(scs_inference,[],[606,28830,249,248])).
% 58.78/58.89 cnf(33688,plain,
% 58.78/58.89 (P32(a3,x336881,a3)),
% 58.78/58.89 inference(rename_variables,[],[33578])).
% 58.78/58.89 cnf(33709,plain,
% 58.78/58.89 (P26(a3,x337091,x337091)+~P15(a3,a3)),
% 58.78/58.89 inference(scs_inference,[],[35,5,13745,33500,33640,33537,33578,33688,29758,33436,8,389,491,29089,606,27485,453,584,249,341,285,299,209,272,428,283,218,302])).
% 58.78/58.89 cnf(33748,plain,
% 58.78/58.89 (P33(a1,x337481,x337481)+~P22(a1,x337481)),
% 58.78/58.89 inference(scs_inference,[],[35,13745,33500,573,33578,29758,33436,491,496,606,6391,33470,249,341,209,272,428,283,218,318])).
% 58.78/58.89 cnf(34018,plain,
% 58.78/58.89 (P36(a5,a1)),
% 58.78/58.89 inference(scs_inference,[],[13745,10479,33578,16,606,249,341,209])).
% 58.78/58.89 cnf(34023,plain,
% 58.78/58.89 (P35(x340231,a2)),
% 58.78/58.89 inference(scs_inference,[],[13745,7231,10479,33454,33578,33436,449,8,16,619,606,249,341,209,268,358])).
% 58.78/58.89 cnf(34040,plain,
% 58.78/58.89 (P38(a3,a2,a2)),
% 58.78/58.89 inference(scs_inference,[],[13745,33578,8,508,606,249,341,268])).
% 58.78/58.89 cnf(34938,plain,
% 58.78/58.89 (P18(a4,a4,a3)+~P45(a3)),
% 58.78/58.89 inference(scs_inference,[],[473,33489,271])).
% 58.78/58.89 cnf(36041,plain,
% 58.78/58.89 (P33(a2,x360411,a2)),
% 58.78/58.89 inference(scs_inference,[],[28,33644,54])).
% 58.78/58.89 cnf(37116,plain,
% 58.78/58.89 (P31(a1,x371161,x371161)),
% 58.78/58.89 inference(scs_inference,[],[33500,11735,19863,249,291])).
% 58.78/58.89 cnf(37307,plain,
% 58.78/58.89 (P47(a2)),
% 58.78/58.89 inference(scs_inference,[],[33462,25140,504,249,201])).
% 58.78/58.89 cnf(37309,plain,
% 58.78/58.89 (P36(a2,a3)),
% 58.78/58.89 inference(scs_inference,[],[33462,7231,33436,25140,21,504,249,201,209])).
% 58.78/58.89 cnf(40941,plain,
% 58.78/58.89 (P26(a3,x409411,x409411)),
% 58.78/58.89 inference(scs_inference,[],[22,33709,65])).
% 58.78/58.89 cnf(40942,plain,
% 58.78/58.89 (P30(a3,a5,a3)),
% 58.78/58.89 inference(scs_inference,[],[40941,223])).
% 58.78/58.89 cnf(40943,plain,
% 58.78/58.89 (P26(a3,x409431,x409431)),
% 58.78/58.89 inference(rename_variables,[],[40941])).
% 58.78/58.89 cnf(40952,plain,
% 58.78/58.89 (P38(a2,a3,a2)),
% 58.78/58.89 inference(scs_inference,[],[13745,573,34040,37307,33436,33578,606,764,40941,40943,223,249,163,341,361])).
% 58.78/58.89 cnf(40957,plain,
% 58.78/58.89 (~P45(x409571)+P22(x409572,a2)),
% 58.78/58.89 inference(scs_inference,[],[13745,573,34040,37307,33436,33578,27,606,764,40941,40943,223,249,163,341,361,28137,62])).
% 58.78/58.89 cnf(41227,plain,
% 58.78/58.89 (P22(x412271,a2)),
% 58.78/58.89 inference(scs_inference,[],[28,40957,54])).
% 58.78/58.89 cnf(42496,plain,
% 58.78/58.89 (P32(a4,a4,a3)),
% 58.78/58.89 inference(scs_inference,[],[33500,473,33493,153])).
% 58.78/58.89 cnf(42777,plain,
% 58.78/58.89 (P20(a3,a2,a2)),
% 58.78/58.89 inference(scs_inference,[],[5,8,33519,122])).
% 58.78/58.89 cnf(42778,plain,
% 58.78/58.89 (P16(a3,a3)),
% 58.78/58.89 inference(scs_inference,[],[42777,2518])).
% 58.78/58.89 cnf(43059,plain,
% 58.78/58.89 (P28(a3,a5)),
% 58.78/58.89 inference(scs_inference,[],[40942,33537,33563,211])).
% 58.78/58.89 cnf(44832,plain,
% 58.78/58.89 (P26(a2,a5,a5)),
% 58.78/58.89 inference(scs_inference,[],[35,17,254,53])).
% 58.78/58.89 cnf(44833,plain,
% 58.78/58.89 (P30(a2,a5,a2)),
% 58.78/58.89 inference(scs_inference,[],[44832,223])).
% 58.78/58.89 cnf(45346,plain,
% 58.78/58.89 (P38(a5,a3,a5)),
% 58.78/58.89 inference(scs_inference,[],[373,13745,42496,42778,33513,33442,33436,19863,40941,41227,249,33748,163,341,361])).
% 58.78/58.89 cnf(49845,plain,
% 58.78/58.89 (P8(a4,x498451,a4)+~P45(x498451)),
% 58.78/58.89 inference(scs_inference,[],[37,13745,42496,544,33442,45346,33436,16896,19863,491,23,41227,249,33748,163,341,428,209,283,308])).
% 58.78/58.89 cnf(52202,plain,
% 58.78/58.89 (P20(x522021,x522021,x522021)),
% 58.78/58.89 inference(scs_inference,[],[27,38,293,234])).
% 58.78/58.89 cnf(58834,plain,
% 58.78/58.89 (P35(x588341,a5)),
% 58.78/58.89 inference(scs_inference,[],[13745,573,42496,10479,33454,37307,33436,619,606,41227,33748,249,163,341,358])).
% 58.78/58.89 cnf(63651,plain,
% 58.78/58.89 (P20(a2,a3,a3)),
% 58.78/58.89 inference(scs_inference,[],[13745,42496,544,33442,33436,606,29089,52202,41227,33748,249,341,163,331])).
% 58.78/58.89 cnf(70940,plain,
% 58.78/58.89 (P35(a2,a3)),
% 58.78/58.89 inference(scs_inference,[],[13745,544,42496,40952,33454,33442,33436,606,41227,249,33748,341,163,358])).
% 58.78/58.89 cnf(98745,plain,
% 58.78/58.89 (P37(a3,a3,a2)),
% 58.78/58.89 inference(scs_inference,[],[42777,435])).
% 58.78/58.89 cnf(98985,plain,
% 58.78/58.89 (P28(a1,x989851)),
% 58.78/58.89 inference(scs_inference,[],[33537,584,37116,41227,33748,249,211])).
% 58.78/58.89 cnf(100134,plain,
% 58.78/58.89 (P5(a1)),
% 58.78/58.89 inference(scs_inference,[],[23,53])).
% 58.78/58.89 cnf(100140,plain,
% 58.78/58.89 (P29(x1001401,x1001401,x1001401)),
% 58.78/58.89 inference(scs_inference,[],[23,16,28,53,65,136,139])).
% 58.78/58.89 cnf(100146,plain,
% 58.78/58.89 (P20(x1001461,a1,x1001461)),
% 58.78/58.89 inference(scs_inference,[],[23,16,504,28,38,53,65,136,139,140,144,234])).
% 58.78/58.89 cnf(100147,plain,
% 58.78/58.89 (P12(x1001471,a1,x1001472)),
% 58.78/58.89 inference(rename_variables,[],[38])).
% 58.78/58.89 cnf(100153,plain,
% 58.78/58.89 (P45(a2)),
% 58.78/58.89 inference(scs_inference,[],[32,587,23,16,504,28,38,53,65,136,139,140,144,234,437,226,54])).
% 58.78/58.89 cnf(100154,plain,
% 58.78/58.89 (P23(a2,x1001541)),
% 58.78/58.89 inference(rename_variables,[],[28])).
% 58.78/58.89 cnf(100158,plain,
% 58.78/58.89 (P20(a4,a2,a4)),
% 58.78/58.89 inference(scs_inference,[],[32,587,23,16,6,504,8,28,3,38,53,65,136,139,140,144,234,437,226,54,121,122])).
% 58.78/58.89 cnf(100160,plain,
% 58.78/58.89 (P20(a2,x1001601,a2)),
% 58.78/58.89 inference(scs_inference,[],[32,587,23,16,6,504,2,8,28,100154,3,38,53,65,136,139,140,144,234,437,226,54,121,122,155])).
% 58.78/58.89 cnf(100162,plain,
% 58.78/58.89 (P20(a5,x1001621,a5)),
% 58.78/58.89 inference(scs_inference,[],[32,587,23,16,6,504,2,8,28,100154,3,38,53,65,136,139,140,144,234,437,226,54,121,122,155,156])).
% 58.78/58.89 cnf(100164,plain,
% 58.78/58.89 (P20(a2,a2,a5)),
% 58.78/58.89 inference(scs_inference,[],[32,587,23,16,6,504,2,8,28,100154,3,38,19,53,65,136,139,140,144,234,437,226,54,121,122,155,156,157])).
% 58.78/58.89 cnf(100170,plain,
% 58.78/58.89 (P32(a2,a2,a5)),
% 58.78/58.89 inference(scs_inference,[],[33541,37309,32,32070,587,23,16,6,504,2,8,28,100154,3,4,44833,38,19,53,65,136,139,140,144,234,437,226,54,121,122,155,156,157,188,210,275])).
% 58.78/58.89 cnf(100181,plain,
% 58.78/58.89 (P12(a3,x1001811,a3)),
% 58.78/58.89 inference(rename_variables,[],[37])).
% 58.78/58.89 cnf(100183,plain,
% 58.78/58.89 (P26(a1,a5,a5)),
% 58.78/58.89 inference(scs_inference,[],[33541,37309,40952,32,32070,587,451,23,16,6,504,2,8,28,100154,34,3,4,44833,38,100147,389,19,573,37,53,65,136,139,140,144,234,437,226,54,121,122,155,156,157,188,210,275,423,175,255,332,333,254])).
% 58.78/58.89 cnf(100186,plain,
% 58.78/58.89 (P45(a1)),
% 58.78/58.89 inference(scs_inference,[],[33541,37309,10,40952,32,32070,587,451,23,16,6,504,2,8,28,100154,34,3,4,44833,38,100147,389,19,573,37,53,65,136,139,140,144,234,437,226,54,121,122,155,156,157,188,210,275,423,175,255,332,333,254,62])).
% 58.78/58.89 cnf(100192,plain,
% 58.78/58.89 (~P7(a4,a5)),
% 58.78/58.89 inference(scs_inference,[],[39,33541,37309,10,33545,40952,32,32070,587,451,23,16,6,504,2,8,6333,14,28,100154,34,3,4,44833,38,100147,389,19,573,37,53,65,136,139,140,144,234,437,226,54,121,122,155,156,157,188,210,275,423,175,255,332,333,254,62,446,201,153])).
% 58.78/58.89 cnf(100199,plain,
% 58.78/58.89 (P23(a2,x1001991)),
% 58.78/58.89 inference(rename_variables,[],[28])).
% 58.78/58.89 cnf(100202,plain,
% 58.78/58.89 (P23(a2,x1002021)),
% 58.78/58.89 inference(rename_variables,[],[28])).
% 58.78/58.89 cnf(100204,plain,
% 58.78/58.89 (P16(a4,a4)),
% 58.78/58.89 inference(scs_inference,[],[39,33541,37309,10,33545,63651,40952,32,32070,587,451,23,16,6,504,2,27,8,6333,42778,14,28,100154,100199,100202,34,3,4,44833,38,100147,389,19,573,37,53,65,136,139,140,144,234,437,226,54,121,122,155,156,157,188,210,275,423,175,255,332,333,254,62,446,201,153,331,75,177,193,219])).
% 58.78/58.89 cnf(100205,plain,
% 58.78/58.89 (P23(a2,x1002051)),
% 58.78/58.89 inference(rename_variables,[],[28])).
% 58.78/58.89 cnf(100207,plain,
% 58.78/58.89 (P18(a2,a3,a2)),
% 58.78/58.89 inference(scs_inference,[],[39,33541,37309,10,98745,33545,63651,2063,40952,32,32070,587,451,23,16,6,504,2,27,8,6333,42778,14,28,100154,100199,100202,34,3,4,44833,38,100147,389,19,573,37,100181,53,65,136,139,140,144,234,437,226,54,121,122,155,156,157,188,210,275,423,175,255,332,333,254,62,446,201,153,331,75,177,193,219,356])).
% 58.78/58.89 cnf(100210,plain,
% 58.78/58.89 (P24(a1,x1002101)),
% 58.78/58.89 inference(scs_inference,[],[39,33541,37309,70940,98985,10,98745,33545,63651,2063,40952,32,32070,587,27485,451,23,16,6,12865,504,2,27,8,6333,42778,14,28,100154,100199,100202,34,3,4,44833,38,100147,389,19,573,37,100181,53,65,136,139,140,144,234,437,226,54,121,122,155,156,157,188,210,275,423,175,255,332,333,254,62,446,201,153,331,75,177,193,219,356,299])).
% 58.78/58.89 cnf(100216,plain,
% 58.78/58.89 (P44(a1)),
% 58.78/58.89 inference(scs_inference,[],[39,33541,37309,70940,98985,10,98745,33545,63651,2063,40952,32,32070,587,27485,451,23,16,6,12865,504,2,27,8,6333,42778,14,28,100154,100199,100202,34,3,4,44833,38,100147,389,19,573,37,100181,53,65,136,139,140,144,234,437,226,54,121,122,155,156,157,188,210,275,423,175,255,332,333,254,62,446,201,153,331,75,177,193,219,356,299,11741,407])).
% 58.78/58.89 cnf(100219,plain,
% 58.78/58.89 (P16(a2,a5)),
% 58.78/58.89 inference(scs_inference,[],[39,33541,37309,70940,98985,10,98745,33545,63651,2063,40952,32,32070,587,27485,451,23,16,6,12865,504,2,27,8,6333,42778,14,28,100154,100199,100202,34,3,4,44833,38,100147,389,19,573,37,100181,53,65,136,139,140,144,234,437,226,54,121,122,155,156,157,188,210,275,423,175,255,332,333,254,62,446,201,153,331,75,177,193,219,356,299,11741,407,630,24487])).
% 58.78/58.89 cnf(100227,plain,
% 58.78/58.89 (P42(a4,a3,a3)),
% 58.78/58.89 inference(scs_inference,[],[39,33541,37309,70940,98985,10,98745,33545,63651,2063,40952,32,32070,587,27485,451,23,16,6,12865,504,2,27,8,6333,42778,14,28,100154,100199,100202,34,3,4,44833,38,100147,389,19,573,37,100181,53,65,136,139,140,144,234,437,226,54,121,122,155,156,157,188,210,275,423,175,255,332,333,254,62,446,201,153,331,75,177,193,219,356,299,11741,407,630,24487,49845,6916,241,24324,154])).
% 58.78/58.89 cnf(100251,plain,
% 58.78/58.89 (P22(x1002511,a3)),
% 58.78/58.89 inference(scs_inference,[],[39,33541,37309,70940,11610,98985,10,11125,98745,33545,63651,2063,40952,32,32070,33470,587,27485,451,23,16,18,6,12865,504,2,33454,27,535,8,6333,42778,14,28,100154,100199,100202,100205,34,3,4,44833,38,100147,389,33442,6331,33436,41227,19,573,37,100181,53,65,136,139,140,144,234,437,226,54,121,122,155,156,157,188,210,275,423,175,255,332,333,254,62,446,201,153,331,75,177,193,219,356,299,11741,407,630,24487,49845,6916,241,24324,154,28612,163,12503,209,220,318,111,287,285,89])).
% 58.78/58.89 cnf(100255,plain,
% 58.78/58.89 (~P10(x1002551,x1002552)+P45(x1002551)),
% 58.78/58.89 inference(scs_inference,[],[100153,62])).
% 58.78/58.89 cnf(100257,plain,
% 58.78/58.89 (P44(x1002571)+~P38(a2,x1002571,a2)),
% 58.78/58.89 inference(scs_inference,[],[100153,175])).
% 58.78/58.89 cnf(100261,plain,
% 58.78/58.89 (~P45(x1002611)+P16(x1002611,a5)),
% 58.78/58.89 inference(scs_inference,[],[100186,24324])).
% 58.78/58.89 cnf(100262,plain,
% 58.78/58.89 (P44(a5)),
% 58.78/58.89 inference(scs_inference,[],[10479,100257])).
% 58.78/58.89 cnf(100265,plain,
% 58.78/58.89 (P15(a2,a2)),
% 58.78/58.89 inference(scs_inference,[],[10479,21,100257,65])).
% 58.78/58.89 cnf(100273,plain,
% 58.78/58.89 (P38(x1002731,x1002731,a1)),
% 58.78/58.89 inference(scs_inference,[],[10479,21,762,26,460,100257,65,140,11741,437,144])).
% 58.78/58.89 cnf(100276,plain,
% 58.78/58.89 (P12(x1002761,a1,x1002762)),
% 58.78/58.89 inference(rename_variables,[],[38])).
% 58.78/58.89 cnf(100278,plain,
% 58.78/58.89 (P5(a2)),
% 58.78/58.89 inference(scs_inference,[],[10479,21,762,26,460,38,100257,65,140,11741,437,144,226,53])).
% 58.78/58.89 cnf(100280,plain,
% 58.78/58.89 (P30(x1002801,a5,x1002801)),
% 58.78/58.89 inference(scs_inference,[],[100162,10479,21,762,26,460,38,100257,65,140,11741,437,144,226,53,241])).
% 58.78/58.89 cnf(100288,plain,
% 58.78/58.89 (P20(a4,a5,a4)),
% 58.78/58.89 inference(scs_inference,[],[33663,100219,100162,10479,21,6,762,28,4,26,460,38,7,100257,65,140,11741,437,144,226,53,241,423,188,275,122])).
% 58.78/58.89 cnf(100295,plain,
% 58.78/58.89 (P20(a2,x1002951,a2)),
% 58.78/58.89 inference(rename_variables,[],[100160])).
% 58.78/58.89 cnf(100304,plain,
% 58.78/58.89 (P29(x1003041,x1003041,x1003041)),
% 58.78/58.89 inference(rename_variables,[],[100140])).
% 58.78/58.89 cnf(100307,plain,
% 58.78/58.89 (P16(x1003071,x1003071)),
% 58.78/58.89 inference(scs_inference,[],[33586,33663,100140,100219,58834,100160,100295,100162,100164,100170,100186,33458,10,10479,21,6,762,8,28,34,4,26,460,38,100276,28771,33,7,100257,65,140,11741,437,144,226,53,241,423,188,275,122,332,268,446,331,341,353,219])).
% 58.78/58.89 cnf(100314,plain,
% 58.78/58.89 (P38(a5,a1,a5)),
% 58.78/58.89 inference(scs_inference,[],[33586,33663,100140,100304,100219,100183,58834,100251,100160,100295,100162,100164,100170,100186,33458,36041,33445,10,10479,21,6,762,8,28,34,4,26,460,38,100276,28771,33,7,100257,65,140,11741,437,144,226,53,241,423,188,275,122,332,268,446,331,341,353,219,318,361])).
% 58.78/58.89 cnf(100319,plain,
% 58.78/58.89 (P7(x1003191,a1)),
% 58.78/58.89 inference(scs_inference,[],[33586,33663,100140,100304,100219,100146,100183,58834,100251,100160,100295,100162,100134,100164,100170,100186,33458,36041,33445,10,10479,21,11,29421,6,762,33500,8,28,34,4,26,460,38,100276,28771,606,33,7,100257,65,140,11741,437,144,226,53,241,423,188,275,122,332,268,446,331,341,353,219,318,361,316,218])).
% 58.78/58.89 cnf(100320,plain,
% 58.78/58.89 (P7(x1003201,x1003201)),
% 58.78/58.89 inference(rename_variables,[],[33500])).
% 58.78/58.89 cnf(100347,plain,
% 58.78/58.89 (P8(a1,a1,x1003471)),
% 58.78/58.89 inference(scs_inference,[],[33586,33663,43059,100140,100304,100219,100146,100183,58834,100210,100251,100160,100295,100162,33440,100134,100164,100170,100186,100204,100207,100216,100227,33458,36041,33445,11610,10,2063,10479,21,11,29421,12865,6,762,13,33500,100320,535,8,6333,28,34,4,26,460,38,100276,28771,606,33,7,100257,65,140,11741,437,144,226,53,241,423,188,275,122,332,268,446,331,341,353,219,318,361,316,218,309,287,111,356,299,100255,100261,6785,9108,10094,22831,34938,556,145])).
% 58.78/58.89 cnf(100349,plain,
% 58.78/58.89 (P42(a1,a2,a1)),
% 58.78/58.89 inference(scs_inference,[],[33586,33663,43059,100140,100304,100219,100146,100183,58834,100210,100251,100160,100295,100162,33440,100134,100164,100170,100186,100204,100207,100216,100227,33458,36041,33445,11610,10,2063,10479,21,11,29421,12865,6,762,13,33500,100320,535,8,6333,28,34,4,26,460,38,100276,28771,606,33,7,100257,65,140,11741,437,144,226,53,241,423,188,275,122,332,268,446,331,341,353,219,318,361,316,218,309,287,111,356,299,100255,100261,6785,9108,10094,22831,34938,556,145,248])).
% 58.78/58.89 cnf(100381,plain,
% 58.78/58.89 (P15(a4,a4)),
% 58.78/58.89 inference(scs_inference,[],[18,26,140,65])).
% 58.78/58.89 cnf(100387,plain,
% 58.78/58.89 (P5(a5)),
% 58.78/58.89 inference(scs_inference,[],[100262,16,18,26,777,140,65,11741,437,53])).
% 58.78/58.89 cnf(100392,plain,
% 58.78/58.89 (P16(x1003921,x1003921)),
% 58.78/58.89 inference(rename_variables,[],[100307])).
% 58.78/58.89 cnf(100407,plain,
% 58.78/58.89 (P8(a1,a1,x1004071)),
% 58.78/58.89 inference(rename_variables,[],[100347])).
% 58.78/58.89 cnf(100415,plain,
% 58.78/58.89 (P31(a2,a4,a2)),
% 58.78/58.89 inference(scs_inference,[],[100265,100307,100392,100158,100280,100314,100347,100262,100278,100349,19859,33550,34023,11610,100186,16,18,29421,33454,8,28,34,4,26,36,777,5,140,65,11741,437,53,241,423,275,122,188,332,353,358,218,111,120])).
% 58.78/58.89 cnf(100418,plain,
% 58.78/58.89 (P42(a1,a5,a1)),
% 58.78/58.89 inference(scs_inference,[],[100265,100307,100392,100158,100280,100314,100347,100262,100278,100349,19859,33550,34023,11610,100186,16,18,29421,33454,8,28,34,4,26,36,777,5,140,65,11741,437,53,241,423,275,122,188,332,353,358,218,111,120,556,248])).
% 58.78/58.89 cnf(100426,plain,
% 58.78/58.89 (P38(a1,a3,a1)),
% 58.78/58.89 inference(scs_inference,[],[34018,100265,100307,100392,100158,100273,100280,100314,100347,100262,100278,100349,19859,33550,34023,11610,100186,16,18,29421,6,33454,508,8,28,34,4,26,36,777,389,6331,5,140,65,11741,437,53,241,423,275,122,188,332,353,358,218,111,120,556,248,431,210,302,361])).
% 58.78/58.89 cnf(100431,plain,
% 58.78/58.89 (P8(x1004311,x1004311,a1)),
% 58.78/58.89 inference(scs_inference,[],[34018,100265,100307,100392,100158,100273,100280,100314,100319,100347,100407,100262,100278,100349,19859,33550,34023,11610,100186,16,18,29421,6,33454,27,508,8,28,34,4,26,36,777,389,6331,5,140,65,11741,437,53,241,423,275,122,188,332,353,358,218,111,120,556,248,431,210,302,361,316])).
% 58.78/58.89 cnf(100463,plain,
% 58.78/58.89 ($false),
% 58.78/58.89 inference(scs_inference,[],[100426,100192,100431,100381,100387,100415,100418,100288,100307,100216,100280,100140,98745,18,22,33454,33500,3,26,65,11741,140,53,241,275,201,423,353,358,218]),
% 58.78/58.89 ['proof']).
% 58.99/58.94 % SZS output end Proof
% 58.99/58.94 % Total time :58.080000s
%------------------------------------------------------------------------------