%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SYN204-1 : TPTP v8.2.0. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/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:50 EDT 2024
% Result : Unsatisfiable 58.72s 58.74s
% Output : CNFRefutation 58.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYN204-1 : TPTP v8.2.0. Released v1.1.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.32 % Computer : n024.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % 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 21:16:53 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.49/0.56 start to proof:theBenchmark
% 58.72/58.73 %-------------------------------------------
% 58.72/58.73 % File :CSE---1.7
% 58.72/58.73 % Problem :theBenchmark
% 58.72/58.73 % Transform :cnf
% 58.72/58.73 % Format :tptp:raw
% 58.72/58.73 % Command :java -jar mcs_scs.jar %d %s
% 58.72/58.73
% 58.72/58.73 % Result :Theorem 58.100000s
% 58.72/58.73 % Output :CNFRefutation 58.100000s
% 58.72/58.73 %-------------------------------------------
% 58.72/58.74 %--------------------------------------------------------------------------
% 58.72/58.74 % File : SYN204-1 : TPTP v8.2.0. Released v1.1.0.
% 58.72/58.74 % Domain : Syntactic (Random Prolog Theory)
% 58.72/58.74 % Problem : RPT63 synthetic problem 102 (quasi-uniform distribution)
% 58.72/58.74 % Version : [SE94] axioms : Especial.
% 58.72/58.74 % English :
% 58.72/58.74
% 58.72/58.74 % Refs : [SE94] Segre & Elkan (1994), A High-Performance Explanation-B
% 58.72/58.74 % Source : [SE94]
% 58.72/58.74 % Names : - [SE94]
% 58.72/58.74
% 58.72/58.74 % Status : Unsatisfiable
% 58.72/58.74 % 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.72/58.74 % Syntax : Number of clauses : 369 ( 39 unt; 0 nHn; 362 RR)
% 58.72/58.74 % Number of literals : 1060 ( 0 equ; 692 neg)
% 58.72/58.74 % Maximal clause size : 5 ( 2 avg)
% 58.72/58.74 % Maximal term depth : 1 ( 1 avg)
% 58.72/58.74 % Number of predicates : 48 ( 48 usr; 0 prp; 1-3 aty)
% 58.72/58.74 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% 58.72/58.74 % Number of variables : 626 ( 160 sgn)
% 58.72/58.74 % SPC : CNF_UNS_EPR_NEQ_HRN
% 58.72/58.74
% 58.72/58.74 % Comments : This theory has a finite deductive closure.
% 58.72/58.74 %--------------------------------------------------------------------------
% 58.72/58.74 %----Include Synthetic domain theory for EBL
% 58.72/58.74 include('Axioms/SYN001-0.ax').
% 58.72/58.74 %--------------------------------------------------------------------------
% 58.72/58.74 cnf(prove_this,negated_conjecture,
% 58.72/58.74 ~ s3(a,c) ).
% 58.72/58.74
% 58.72/58.74 %--------------------------------------------------------------------------
% 58.72/58.74 %-------------------------------------------
% 58.72/58.74 % Proof found
% 58.72/58.74 % SZS status Theorem for theBenchmark
% 58.72/58.74 % SZS output start Proof
% 58.72/58.75 %ClaNum:362(EqnAxiom:0)
% 58.72/58.75 %VarNum:1493(SingletonVarNum:573)
% 58.72/58.75 %MaxLitNum:5
% 58.72/58.75 %MaxfuncDepth:0
% 58.72/58.75 %SharedTerms:201
% 58.72/58.75 %goalClause: 39
% 58.72/58.75 %singleGoalClaCount:1
% 58.72/58.75 [1]P1(a1)
% 58.72/58.75 [2]P1(a2)
% 58.72/58.75 [3]P2(a5)
% 58.72/58.75 [4]P2(a2)
% 58.72/58.75 [5]P3(a3)
% 58.72/58.75 [6]P3(a4)
% 58.72/58.75 [7]P4(a5)
% 58.72/58.75 [8]P4(a2)
% 58.72/58.75 [10]P10(a1,a2)
% 58.72/58.75 [11]P10(a1,a4)
% 58.72/58.75 [13]P10(a3,a2)
% 58.72/58.75 [14]P10(a2,a5)
% 58.72/58.75 [15]P10(a2,a2)
% 58.72/58.75 [16]P11(a1,a5)
% 58.72/58.75 [17]P11(a1,a2)
% 58.72/58.75 [18]P11(a1,a4)
% 58.72/58.75 [19]P11(a5,a5)
% 58.72/58.75 [20]P11(a5,a2)
% 58.72/58.75 [21]P11(a3,a2)
% 58.72/58.75 [22]P11(a2,a3)
% 58.72/58.75 [23]P11(a4,a1)
% 58.72/58.75 [26]P23(a4,a2)
% 58.72/58.75 [29]P12(a1,a5,a4)
% 58.72/58.75 [32]P12(a5,a2,a4)
% 58.72/58.75 [33]P12(a3,a5,a5)
% 58.72/58.75 [34]P12(a2,a3,a3)
% 58.72/58.75 [35]P12(a2,a2,a5)
% 58.72/58.75 [36]P12(a4,a2,a3)
% 58.72/58.75 [39]~P44(a3,a4)
% 58.72/58.75 [27]P10(x271,a1)
% 58.72/58.75 [28]P23(a2,x281)
% 58.72/58.75 [37]P12(a3,x371,a3)
% 58.72/58.75 [38]P12(x381,a1,x382)
% 58.72/58.75 [40]P18(a2)+~P5(a2)
% 58.72/58.75 [43]P34(a3,a3)+~P40(a3)
% 58.72/58.75 [58]P7(a5,a5)+~P15(a5,a5)
% 58.72/58.75 [59]P14(a1,a1)+~P7(a3,a1)
% 58.72/58.75 [60]P14(a4,a4)+~P7(a2,a4)
% 58.72/58.75 [79]P19(a5,a5,a5)+~P2(a5)
% 58.72/58.75 [80]P19(a2,a2,a2)+~P3(a2)
% 58.72/58.75 [81]P19(a4,a4,a4)+~P3(a4)
% 58.72/58.75 [82]P26(a4,a4,a4)+~P3(a4)
% 58.72/58.75 [83]P29(a3,a3,a3)+~P3(a3)
% 58.72/58.75 [85]P37(a2,a2,a2)+~P3(a2)
% 58.72/58.75 [86]P8(a3,a3,a3)+~P41(a3)
% 58.72/58.75 [87]P8(a4,a4,a4)+~P41(a4)
% 58.72/58.75 [116]P26(a1,a1,a1)+~P10(a1,a1)
% 58.72/58.75 [119]P22(a2,a2,a2)+~P16(a3,a2)
% 58.72/58.75 [120]P31(a2,a4,a2)+~P7(a4,a2)
% 58.72/58.75 [171]P24(a1,a1)+~P32(a4,a1,a4)
% 58.72/58.75 [213]P29(a4,a5,a2)+~P12(a2,a4,a5)
% 58.72/58.75 [214]P30(a1,a2,a2)+~P29(a1,a2,a5)
% 58.72/58.75 [215]P30(a3,a3,a3)+~P29(a5,a5,a3)
% 58.72/58.75 [216]P22(a2,a2,a2)+~P38(a3,a2,a3)
% 58.72/58.75 [46]~P41(x461)+P14(x461,x461)
% 58.72/58.75 [47]~P6(x471)+P20(x471,x471)
% 58.72/58.75 [48]~P40(x481)+P24(x481,x481)
% 58.72/58.75 [49]~P13(x491)+P34(x491,x491)
% 58.72/58.75 [50]~P6(x501)+P43(x501,x501)
% 58.72/58.75 [54]~P23(x541,x541)+P46(x541)
% 58.72/58.75 [68]~P21(x681,x681)+P34(x681,x681)
% 58.72/58.75 [69]~P35(x691,x691)+P34(x691,x691)
% 58.72/58.75 [96]~P1(x961)+P19(x961,x961,x961)
% 58.72/58.75 [97]~P2(x971)+P26(x971,x971,x971)
% 58.72/58.75 [98]~P4(x981)+P29(x981,x981,x981)
% 58.72/58.75 [100]~P1(x1001)+P37(x1001,x1001,x1001)
% 58.72/58.75 [101]~P2(x1011)+P37(x1011,x1011,x1011)
% 58.72/58.75 [102]~P5(x1021)+P30(x1021,x1021,x1021)
% 58.72/58.75 [103]~P18(x1031)+P8(x1031,x1031,x1031)
% 58.72/58.75 [104]~P25(x1041)+P8(x1041,x1041,x1041)
% 58.72/58.75 [105]~P25(x1051)+P22(x1051,x1051,x1051)
% 58.72/58.75 [106]~P25(x1061)+P31(x1061,x1061,x1061)
% 58.72/58.75 [107]~P41(x1071)+P42(x1071,x1071,x1071)
% 58.72/58.75 [108]~P45(x1081)+P42(x1081,x1081,x1081)
% 58.72/58.75 [134]P30(x1341,x1341,x1341)+~P15(x1341,a1)
% 58.72/58.75 [146]~P16(x1461,x1461)+P31(x1461,x1461,x1461)
% 58.72/58.75 [223]P30(x2231,a5,x2231)+~P26(x2231,a5,a5)
% 58.72/58.75 [224]P37(x2241,x2241,x2241)+~P12(x2241,a4,a2)
% 58.72/58.75 [225]P30(x2251,x2251,x2251)+~P26(a1,a1,x2251)
% 58.72/58.75 [227]~P37(x2271,a3,x2271)+P30(x2271,a3,x2271)
% 58.72/58.75 [243]~P37(x2431,x2431,x2431)+P30(x2431,x2431,x2431)
% 58.72/58.75 [244]~P29(x2441,x2441,x2441)+P38(x2441,x2441,x2441)
% 58.72/58.75 [247]~P30(x2471,x2471,x2471)+P22(x2471,x2471,x2471)
% 58.72/58.75 [53]P5(x531)+~P11(x532,x531)
% 58.72/58.75 [65]P15(x651,x651)+~P11(x652,x651)
% 58.72/58.75 [66]P24(x661,x661)+~P28(x662,x661)
% 58.72/58.75 [67]P24(x671,x671)+~P35(x672,x671)
% 58.72/58.75 [135]P19(x1351,x1351,x1351)+~P10(x1352,x1351)
% 58.72/58.75 [136]~P23(x1362,x1361)+P29(x1361,x1361,x1362)
% 58.72/58.75 [137]P29(x1371,x1371,x1371)+~P10(x1372,x1371)
% 58.72/58.75 [138]P29(x1381,x1381,x1381)+~P11(x1382,x1381)
% 58.72/58.75 [139]P29(x1391,x1391,x1391)+~P23(x1392,x1391)
% 58.72/58.75 [140]~P23(x1402,x1401)+P37(x1401,x1402,x1402)
% 58.72/58.75 [141]P37(x1411,x1411,x1411)+~P10(x1412,x1411)
% 58.72/58.75 [142]P37(x1421,x1421,x1421)+~P11(x1422,x1421)
% 58.72/58.75 [143]P30(x1431,x1431,x1431)+~P15(x1432,x1431)
% 58.72/58.76 [144]~P15(x1442,x1441)+P38(x1441,x1441,x1442)
% 58.72/58.76 [145]~P7(x1452,x1451)+P8(x1451,x1451,x1452)
% 58.72/58.76 [147]P42(x1471,x1471,x1471)+~P16(x1472,x1471)
% 58.72/58.76 [190]P7(x1901,x1901)+~P37(x1902,x1901,x1901)
% 58.72/58.76 [226]P26(x2261,a4,x2261)+~P12(x2262,x2261,a4)
% 58.72/58.76 [231]P38(x2311,x2311,x2311)+~P37(x2312,a4,x2311)
% 58.72/58.76 [232]P26(x2321,x2321,x2322)+~P12(a2,x2322,x2321)
% 58.72/58.76 [234]~P12(x2342,x2342,x2341)+P19(x2341,x2342,x2341)
% 58.72/58.76 [241]~P19(x2412,x2411,x2412)+P30(x2411,x2412,x2411)
% 58.72/58.76 [242]P30(x2421,x2421,x2421)+~P19(x2422,x2422,x2421)
% 58.72/58.76 [245]~P30(x2452,x2451,x2451)+P8(x2451,x2452,x2451)
% 58.72/58.76 [246]P8(x2461,x2461,x2461)+~P30(x2462,x2461,x2461)
% 58.72/58.76 [249]~P8(x2491,x2491,x2492)+P32(x2491,x2492,x2491)
% 58.72/58.76 [250]P32(x2501,x2501,x2501)+~P31(x2502,x2502,x2501)
% 58.72/58.76 [172]P25(x1721)+~P29(x1722,x1723,x1721)
% 58.72/58.76 [173]P27(x1731)+~P30(x1732,x1733,x1731)
% 58.72/58.76 [174]P13(x1741)+~P31(x1742,x1743,x1741)
% 58.72/58.76 [236]P19(x2361,x2361,x2361)+~P12(x2362,x2363,x2361)
% 58.72/58.76 [239]P37(x2391,x2391,x2391)+~P12(x2392,x2393,x2391)
% 58.72/58.76 [248]P42(x2481,x2482,x2481)+~P30(x2481,x2483,x2482)
% 58.72/58.76 [41]P45(a1)+~P1(a1)+~P46(a3)
% 58.72/58.76 [42]P45(a1)+~P39(a1)+~P46(a1)
% 58.72/58.76 [51]P25(a4)+~P4(a2)+~P15(a5,a4)
% 58.72/58.76 [90]P19(a3,a3,a3)+~P1(a1)+~P3(a3)
% 58.72/58.76 [132]~P15(a5,a4)+P30(a5,a4,a4)+~P39(a1)
% 58.72/58.76 [133]P8(a4,a4,a4)+~P45(a5)+~P7(a4,a5)
% 58.72/58.76 [164]P19(a2,a2,a2)+~P10(a4,a1)+~P15(a3,a2)
% 58.72/58.76 [165]P9(a2)+~P48(a5)+~P26(a2,a2,a2)
% 58.72/58.76 [197]P28(a5,a5)+~P14(a2,a3)+~P31(a2,a5,a3)
% 58.72/58.76 [198]P35(a2,a2)+~P15(a2,a4)+~P8(a4,a5,a2)
% 58.72/58.76 [199]P24(a2,a5)+~P28(a2,a5)+~P42(a1,a2,a4)
% 58.72/58.76 [222]P29(a3,a2,a3)+~P2(a2)+~P29(a3,a3,a3)
% 58.72/58.76 [260]P29(a1,a1,a2)+~P23(a1,a2)+~P12(a5,a3,a3)
% 58.72/58.76 [261]P30(a4,a5,a5)+~P15(a4,a2)+~P37(a5,a5,a5)
% 58.72/58.76 [300]P28(a1,a1)+~P37(a1,a1,a1)+~P8(a4,a4,a5)
% 58.72/58.76 [324]P37(a1,a1,a4)+~P12(a4,a2,a3)+~P19(a4,a1,a3)
% 58.72/58.76 [44]~P3(x441)+~P39(x441)+P41(x441)
% 58.72/58.76 [52]~P25(x521)+P14(x521,x521)+~P18(a2)
% 58.72/58.76 [56]~P46(x561)+~P6(x561)+P24(x561,x561)
% 58.72/58.76 [70]~P48(x701)+P20(x701,x701)+~P21(a5,a5)
% 58.72/58.76 [109]~P1(x1091)+P37(x1091,a2,a2)+~P1(a2)
% 58.72/58.76 [113]~P5(x1131)+P37(x1131,x1131,x1131)+~P1(a2)
% 58.72/58.76 [114]~P25(x1141)+P30(x1141,x1141,x1141)+~P5(a5)
% 58.72/58.76 [123]~P1(x1231)+~P4(x1231)+P26(x1231,x1231,x1231)
% 58.72/58.76 [148]P8(x1481,x1481,x1481)+~P15(a2,x1481)+~P41(a4)
% 58.72/58.76 [170]~P23(x1701,a1)+P26(a3,x1701,a2)+~P23(a3,a2)
% 58.72/58.76 [175]P45(x1751)+~P38(a2,x1751,a2)+~P46(a2)
% 58.72/58.76 [182]~P11(x1821,x1821)+P26(x1821,x1821,x1821)+~P10(a3,x1821)
% 58.72/58.76 [203]~P28(x2031,a1)+P24(a1,x2031)+~P8(a1,x2031,a3)
% 58.72/58.76 [228]~P30(x2281,a5,a5)+P22(x2281,a5,a5)+~P25(a5)
% 58.72/58.76 [229]~P22(x2291,a4,a3)+P32(a4,a4,x2291)+~P27(a3)
% 58.72/58.76 [230]~P19(a2,x2301,a5)+P26(a5,a5,x2301)+~P1(a2)
% 58.72/58.76 [233]P22(x2331,a4,x2331)+~P38(x2331,a4,a4)+~P45(a4)
% 58.72/58.76 [283]~P11(x2831,a1)+~P19(a3,x2831,a1)+P30(a3,x2831,a1)
% 58.72/58.76 [326]~P38(x3261,x3261,a2)+~P22(a5,x3261,a5)+P31(a5,a2,a5)
% 58.72/58.76 [328]~P12(x3281,a1,x3281)+P37(a5,x3281,x3281)+~P12(a5,a1,x3281)
% 58.72/58.76 [45]~P13(x451)+P47(x451)+~P40(x452)
% 58.72/58.76 [55]~P2(x551)+P20(x551,x551)+~P48(x552)
% 58.72/58.76 [57]~P18(x572)+~P48(x571)+P34(x571,x572)
% 58.72/58.76 [64]~P5(x641)+P17(x641)+~P35(x642,x642)
% 58.72/58.76 [72]~P15(x721,x721)+P14(x721,x721)+~P45(x722)
% 58.72/58.76 [121]~P2(x1211)+~P3(x1212)+P19(x1211,x1212,x1211)
% 58.72/58.76 [122]~P3(x1221)+~P4(x1222)+P19(x1221,x1222,x1221)
% 58.72/58.76 [124]~P1(x1241)+P29(x1241,x1241,x1241)+~P1(x1242)
% 58.72/58.76 [125]~P4(x1251)+P37(x1251,x1251,x1251)+~P3(x1252)
% 58.72/58.76 [126]~P2(x1261)+P30(x1261,x1261,x1261)+~P39(x1262)
% 58.72/58.76 [150]~P1(x1501)+P37(x1501,x1501,x1502)+~P23(x1502,a1)
% 58.72/58.76 [151]~P5(x1511)+P8(x1511,x1511,x1511)+~P16(x1512,a2)
% 58.72/58.76 [152]~P4(x1522)+P29(x1521,x1521,x1522)+~P11(a1,x1521)
% 58.72/58.76 [153]~P41(x1531)+P22(x1531,x1532,x1531)+~P7(a4,x1532)
% 58.72/58.76 [154]~P45(x1542)+P42(x1541,x1542,x1542)+~P16(a4,x1541)
% 58.72/58.76 [155]~P1(x1551)+~P23(x1551,x1552)+P19(x1551,x1552,x1551)
% 58.72/58.76 [157]~P4(x1571)+~P11(x1572,x1572)+P19(x1571,x1571,x1572)
% 58.72/58.76 [163]~P48(x1632)+~P16(x1631,x1631)+P33(x1631,x1631,x1632)
% 58.72/58.76 [180]~P12(x1802,x1801,x1801)+P13(x1801)+~P13(x1802)
% 58.72/58.76 [187]~P15(x1872,x1871)+P26(x1871,x1871,x1871)+~P11(x1872,x1871)
% 58.72/58.76 [194]~P2(x1941)+~P30(x1941,x1942,x1941)+P14(x1941,x1942)
% 58.72/58.76 [195]~P22(x1951,x1951,x1951)+P28(x1951,x1951)+~P6(x1952)
% 58.72/58.76 [210]~P30(x2102,x2101,x2101)+P36(x2101,x2101)+~P36(x2102,x2101)
% 58.72/58.76 [211]~P28(x2111,x2111)+~P31(x2111,x2112,x2112)+P28(x2111,x2112)
% 58.72/58.76 [212]~P12(x2122,x2121,x2122)+P24(x2121,x2121)+~P24(x2122,x2121)
% 58.72/58.76 [251]~P32(x2511,x2511,x2512)+P33(a2,a2,a2)+~P9(a2)
% 58.72/58.76 [252]P30(x2521,x2521,a1)+~P12(x2522,x2521,a1)+~P39(a3)
% 58.72/58.76 [253]~P29(x2531,x2532,a5)+P30(a5,x2531,x2532)+~P2(a5)
% 58.72/58.76 [254]~P5(x2541)+~P12(x2541,x2542,a5)+P26(x2541,a5,a5)
% 58.72/58.76 [255]~P4(x2552)+~P19(x2551,x2552,a2)+P29(x2551,a2,x2552)
% 58.72/58.76 [267]~P12(x2671,x2671,x2672)+P37(x2671,x2671,x2671)+~P4(x2672)
% 58.72/58.76 [268]~P4(x2682)+~P29(x2681,x2681,x2681)+P38(x2681,x2682,x2682)
% 58.72/58.76 [269]~P26(x2691,x2691,x2692)+P38(x2691,x2691,x2691)+~P5(x2692)
% 58.72/58.76 [271]~P41(x2712)+~P8(x2711,x2712,x2711)+P22(x2711,x2711,x2712)
% 58.72/58.76 [274]~P27(x2741)+P31(x2741,x2741,x2741)+~P30(x2742,x2741,x2741)
% 58.72/58.76 [275]~P2(x2751)+~P42(x2752,x2751,x2752)+P32(x2751,x2751,x2752)
% 58.72/58.76 [289]P29(x2891,x2891,x2891)+~P15(x2891,a2)+~P12(a2,x2892,a2)
% 58.72/58.76 [290]P30(x2901,x2901,x2901)+~P37(x2902,a4,x2902)+~P7(x2901,a4)
% 58.72/58.76 [294]~P23(x2941,x2941)+P30(x2941,x2941,x2941)+~P26(x2942,x2942,x2942)
% 58.72/58.76 [327]~P37(a3,x3272,x3271)+P30(x3271,a5,x3272)+~P26(a5,x3271,a3)
% 58.72/58.76 [330]P42(x3301,x3301,x3301)+~P42(x3301,x3301,x3302)+~P12(a1,x3302,x3301)
% 58.72/58.76 [62]P46(x621)+~P10(x621,x623)+~P46(x622)
% 58.72/58.76 [63]~P1(x631)+P18(x631)+~P15(x632,x633)
% 58.72/58.76 [89]P21(x891,x892)+~P16(x893,x892)+~P44(a3,x891)
% 58.72/58.76 [156]~P2(x1561)+P19(x1561,x1562,x1561)+~P23(x1563,x1562)
% 58.72/58.76 [161]~P27(x1611)+P32(x1611,x1611,x1611)+~P36(x1612,x1613)
% 58.72/58.76 [162]~P46(x1621)+P33(x1621,x1622,x1621)+~P35(x1622,x1623)
% 58.72/58.76 [181]P9(x1811)+~P42(x1813,x1811,x1811)+~P48(x1812)
% 58.72/58.76 [186]~P23(x1861,x1861)+P26(x1861,x1862,x1861)+~P23(x1862,x1863)
% 58.72/58.76 [189]P31(x1891,x1891,x1891)+~P10(x1892,x1891)+~P7(x1893,x1893)
% 58.72/58.76 [196]~P2(x1961)+P20(x1961,x1962)+~P32(x1961,x1963,x1962)
% 58.72/58.76 [208]P14(x2081,x2081)+~P16(x2082,x2082)+~P8(x2083,x2081,x2081)
% 58.72/58.76 [209]~P38(x2093,x2091,x2092)+P36(x2091,x2092)+~P11(x2093,x2091)
% 58.72/58.76 [256]~P3(x2561)+P29(x2561,x2561,x2561)+~P12(x2562,x2563,a2)
% 58.72/58.76 [258]P30(x2581,x2582,x2582)+~P5(x2583)+~P30(a5,x2581,x2582)
% 58.72/58.76 [262]~P12(x2622,x2622,x2621)+P19(x2621,x2622,x2622)+~P3(x2623)
% 58.72/58.76 [263]P26(x2631,x2631,x2631)+~P19(x2632,x2633,x2631)+~P4(x2632)
% 58.72/58.76 [264]~P3(x2641)+P29(x2641,x2641,x2641)+~P12(x2642,x2643,x2641)
% 58.72/58.76 [265]~P19(x2651,x2652,x2652)+P37(x2651,x2651,x2652)+~P2(x2653)
% 58.72/58.76 [270]~P39(x2701)+P8(x2701,x2701,x2701)+~P30(x2702,x2703,x2703)
% 58.72/58.76 [272]~P41(x2722)+~P8(x2722,x2723,x2721)+P31(x2721,x2722,x2723)
% 58.72/58.76 [273]~P5(x2731)+P31(x2731,x2731,x2731)+~P38(x2732,x2733,x2731)
% 58.72/58.76 [293]P19(x2931,x2931,x2931)+~P10(x2932,x2932)+~P19(x2933,x2932,x2931)
% 58.72/58.76 [295]P38(x2951,x2951,x2951)+~P10(x2952,x2951)+~P26(x2952,x2951,x2953)
% 58.72/58.76 [319]P14(x3191,x3191)+~P29(x3191,x3191,x3192)+~P30(x3192,x3193,x3191)
% 58.72/58.76 [329]P30(x3291,x3291,x3291)+~P30(a3,x3292,x3291)+~P19(a3,a3,x3293)
% 58.72/58.76 [333]~P26(x3332,x3331,x3332)+P26(x3331,x3331,x3331)+~P12(x3332,x3332,x3333)
% 58.72/58.76 [335]~P30(x3352,x3351,x3352)+P30(x3351,x3351,x3351)+~P19(x3352,x3353,x3351)
% 58.72/58.76 [336]P30(x3361,x3361,x3361)+~P29(x3361,x3362,x3361)+~P37(x3363,x3363,x3363)
% 58.72/58.76 [337]~P30(x3372,x3372,x3373)+P30(x3371,x3371,x3371)+~P37(x3372,x3373,x3372)
% 58.72/58.76 [338]P8(x3381,x3381,x3381)+~P19(x3381,x3381,x3382)+~P30(x3383,x3382,x3383)
% 58.72/58.76 [340]~P42(x3402,x3402,x3402)+P42(x3401,x3401,x3401)+~P31(x3402,x3401,x3403)
% 58.72/58.76 [342]~P32(x3421,x3423,x3421)+P32(x3421,x3421,x3421)+~P22(x3422,x3423,x3421)
% 58.72/58.76 [188]P37(x1881,x1882,x1881)+~P11(x1883,x1882)+~P23(x1884,x1881)
% 58.72/58.76 [201]P48(x2011)+~P15(x2011,x2012)+~P31(x2013,x2012,x2014)
% 58.72/58.76 [291]~P7(x2912,x2913)+P31(x2911,x2912,x2913)+~P38(x2914,a1,x2911)
% 58.72/58.76 [331]~P19(x3313,x3312,x3311)+P19(x3311,x3312,x3312)+~P19(x3313,x3314,x3312)
% 58.72/58.76 [332]~P12(x3322,x3323,x3321)+P26(x3321,x3321,x3322)+~P12(x3323,x3324,x3324)
% 58.72/58.76 [334]~P29(x3343,x3341,x3344)+P29(x3341,x3342,x3343)+~P12(x3343,x3341,x3344)
% 58.72/58.76 [339]P31(x3391,x3392,x3392)+~P30(x3391,x3392,x3393)+~P22(x3392,x3394,x3393)
% 58.72/58.76 [341]~P42(x3412,x3412,x3411)+P32(x3411,x3412,x3412)+~P32(x3413,x3413,x3414)
% 58.72/58.76 [71]P6(a4)+~P27(a5)+~P11(a4,a1)+~P36(a5,a2)
% 58.72/58.76 [110]P37(a2,a5,a5)+~P1(a5)+~P3(a4)+~P4(a2)
% 58.72/58.76 [184]P14(a1,a4)+~P2(a2)+~P45(a1)+~P8(a3,a4,a3)
% 58.72/58.76 [277]P26(a1,a1,a2)+~P4(a2)+~P10(a2,a5)+~P19(a1,a5,a5)
% 58.72/58.76 [278]P26(a1,a5,a5)+~P2(a2)+~P23(a1,a1)+~P26(a5,a5,a5)
% 58.72/58.76 [279]P38(a1,a3,a3)+~P46(a4)+~P10(a5,a4)+~P38(a1,a4,a3)
% 58.72/58.76 [280]P8(a1,a1,a1)+~P41(a3)+~P16(a5,a2)+~P29(a3,a1,a2)
% 58.72/58.76 [281]P22(a4,a2,a1)+~P18(a1)+~P15(a1,a2)+~P38(a2,a4,a1)
% 58.72/58.76 [130]~P5(x1301)+P29(x1301,x1301,x1301)+~P3(a4)+~P4(a5)
% 58.72/58.76 [131]~P3(x1311)+P8(x1311,x1311,x1311)+~P2(a5)+~P41(a5)
% 58.72/58.76 [296]~P5(x2961)+P37(x2961,x2961,x2961)+~P10(x2961,a2)+~P29(a2,a2,x2961)
% 58.72/58.76 [297]~P2(x2971)+~P16(x2971,x2971)+P42(x2971,a2,x2971)+~P30(a2,x2971,a2)
% 58.72/58.76 [357]P7(x3571,x3571)+~P37(x3571,x3571,a1)+~P19(x3571,a5,x3571)+~P26(a5,a1,x3571)
% 58.72/58.76 [359]~P26(a5,a5,x3591)+~P37(a5,a4,x3591)+~P29(x3591,a2,a2)+P30(a2,a4,a4)
% 58.72/58.76 [61]~P27(x612)+~P48(x611)+P43(x611,x612)+~P4(a2)
% 58.72/58.76 [74]~P5(x741)+~P15(x742,x742)+P15(x741,x741)+~P3(x742)
% 58.72/58.76 [111]~P46(x1111)+~P16(x1112,x1112)+P16(x1111,x1112)+~P11(a5,x1112)
% 58.72/58.76 [166]~P3(x1661)+P26(x1661,x1662,x1661)+~P23(a2,x1662)+~P1(a2)
% 58.72/58.76 [167]~P5(x1672)+~P16(x1672,x1671)+P38(x1671,a4,x1672)+~P3(a4)
% 58.72/58.76 [168]~P3(x1681)+P19(x1681,x1681,x1681)+~P3(x1682)+~P23(x1682,a1)
% 58.72/58.76 [169]~P5(x1692)+~P10(x1691,x1691)+P19(x1691,x1692,x1692)+~P5(a3)
% 58.72/58.76 [179]~P29(a2,x1791,x1792)+P25(a5)+~P2(a5)+~P39(a2)
% 58.72/58.76 [191]~P2(x1911)+~P23(x1912,x1912)+P26(x1911,a1,x1912)+~P15(x1912,a1)
% 58.72/58.76 [202]P39(x2021)+~P10(x2021,x2022)+~P37(a1,x2022,a1)+~P1(a1)
% 58.72/58.76 [205]~P23(x2052,x2051)+~P11(x2052,x2052)+P19(x2051,x2051,a4)+~P15(a4,a4)
% 58.72/58.76 [206]~P23(x2061,x2062)+~P15(x2062,x2062)+P29(x2061,x2061,x2061)+~P11(x2062,x2062)
% 58.72/58.76 [276]~P46(x2761)+P8(x2761,x2761,x2761)+~P45(x2762)+~P38(a1,x2762,a1)
% 58.72/58.76 [292]P37(x2921,x2921,x2921)+~P26(x2922,a1,x2921)+~P1(a2)+~P23(a2,a1)
% 58.72/58.76 [321]~P36(x3211,x3211)+~P42(x3211,a5,x3212)+~P37(a3,a3,x3212)+P6(a5)
% 58.72/58.76 [360]P26(x3601,x3601,x3601)+~P26(x3602,x3601,x3602)+~P19(a4,x3601,x3602)+~P12(a2,x3602,a4)
% 58.72/58.76 [75]~P41(x751)+P36(x751,x751)+~P16(x753,x753)+~P46(x752)
% 58.72/58.76 [76]~P39(x761)+P35(x761,x761)+~P35(x762,x763)+~P13(x762)
% 58.72/58.76 [112]P24(x1121,x1121)+~P23(x1121,x1122)+~P21(x1123,x1123)+~P9(a1)
% 58.72/58.76 [115]~P14(x1153,x1153)+P14(x1151,x1151)+~P15(x1153,x1151)+~P25(x1152)
% 58.72/58.76 [177]~P2(x1771)+~P3(x1772)+P26(x1771,x1772,x1771)+~P23(x1773,x1771)
% 58.72/58.76 [193]~P5(x1931)+~P10(x1932,x1931)+P37(x1931,x1931,x1932)+~P23(x1933,x1933)
% 58.72/58.76 [207]~P28(x2073,x2071)+P32(x2071,x2071,x2071)+~P14(x2072,x2072)+~P36(x2072,x2073)
% 58.72/58.76 [220]~P45(x2201)+~P36(x2202,x2201)+P36(x2201,x2202)+~P26(x2203,x2201,x2202)
% 58.72/58.76 [285]~P3(x2851)+~P37(x2852,x2852,x2853)+P37(x2851,x2852,x2852)+~P4(x2853)
% 58.72/58.76 [287]~P18(x2872)+~P25(x2871)+P22(x2871,x2872,x2872)+~P22(x2873,x2871,x2873)
% 58.72/58.76 [302]~P15(x3023,x3021)+~P26(x3021,x3022,x3021)+P26(x3021,x3022,x3022)+~P3(x3023)
% 58.72/58.76 [307]~P23(x3071,x3071)+P30(x3071,x3071,x3071)+~P30(x3073,x3072,x3071)+~P39(x3072)
% 58.72/58.76 [309]~P41(x3093)+~P7(x3092,x3093)+~P42(x3093,x3091,x3091)+P42(x3091,x3092,x3093)
% 58.72/58.76 [312]P37(x3121,x3121,x3121)+~P23(x3122,x3123)+~P29(x3121,a2,a2)+~P10(a2,a2)
% 58.72/58.76 [317]~P14(x3172,x3171)+P31(x3171,x3171,x3171)+~P15(x3172,x3172)+~P31(x3173,x3173,x3172)
% 58.72/58.76 [318]~P21(x3183,x3182)+~P33(x3181,x3183,x3181)+P33(x3181,x3182,x3182)+~P16(x3181,x3183)
% 58.72/58.76 [320]~P46(x3201)+P24(x3201,x3201)+~P32(x3202,x3201,x3201)+~P32(a2,a2,x3203)
% 58.72/58.76 [325]~P19(x3253,x3252,x3252)+P16(x3251,x3251)+~P23(x3252,x3251)+~P12(x3252,x3251,x3253)
% 58.72/58.76 [343]~P8(x3431,x3432,x3432)+P8(x3431,x3431,x3431)+~P46(x3432)+~P30(x3432,x3433,a5)
% 58.72/58.76 [344]~P5(x3441)+P38(x3441,x3441,x3441)+~P38(x3442,x3442,x3443)+~P26(x3443,a1,x3442)
% 58.72/58.76 [349]~P10(x3491,x3492)+~P19(x3492,a4,x3492)+P19(x3491,a3,x3492)+~P12(a3,x3493,a3)
% 58.72/58.76 [352]~P23(x3521,x3522)+~P30(x3521,x3522,x3521)+P30(x3521,x3522,x3522)+~P26(x3523,x3522,x3523)
% 58.72/58.76 [354]~P29(x3543,x3542,x3541)+~P42(x3541,x3543,x3541)+P42(x3541,x3541,x3541)+~P16(x3542,x3543)
% 58.72/58.76 [355]~P8(x3553,x3552,x3552)+P32(x3551,x3551,x3551)+~P28(x3551,x3552)+~P29(x3552,x3553,x3551)
% 58.72/58.76 [361]~P29(x3611,x3611,x3613)+~P38(x3612,x3613,x3611)+P38(x3611,x3612,x3611)+~P26(x3612,x3611,x3613)
% 58.72/58.76 [88]~P27(x881)+P40(x881)+~P23(x882,x881)+~P36(x883,x884)
% 58.72/58.76 [217]~P12(x2172,x2171,x2174)+P15(x2171,x2172)+~P23(x2174,x2171)+~P2(x2173)
% 58.72/58.76 [218]~P7(x2183,x2182)+P7(x2181,x2182)+~P19(x2184,x2182,x2181)+~P5(x2183)
% 58.72/58.76 [219]P16(x2191,x2191)+~P12(x2194,x2192,x2191)+~P23(x2193,x2193)+~P46(x2192)
% 58.72/58.76 [282]P29(x2821,x2822,x2821)+~P29(x2822,x2824,x2821)+~P3(x2823)+~P1(a2)
% 58.72/58.76 [286]~P29(x2862,x2864,x2861)+P8(x2861,x2861,x2862)+~P18(x2863)+~P18(x2864)
% 58.72/58.76 [303]~P4(x3031)+P26(x3031,x3031,x3031)+~P12(x3034,x3033,x3034)+~P10(x3032,x3033)
% 58.72/58.76 [305]P29(x3051,x3051,x3051)+~P26(x3053,x3054,x3051)+~P11(x3053,x3053)+~P3(x3052)
% 58.72/58.76 [308]~P46(x3082)+P8(x3081,x3082,x3081)+~P30(x3084,x3082,x3083)+~P11(x3081,x3083)
% 58.72/58.76 [311]~P13(x3111)+P32(x3111,x3111,x3111)+~P11(x3111,x3112)+~P32(x3113,x3114,x3113)
% 58.72/58.76 [322]~P45(x3221)+~P38(x3223,x3221,x3223)+P44(x3221,x3222)+~P12(x3223,x3224,x3222)
% 58.72/58.76 [345]~P18(x3452)+P42(x3451,x3451,x3452)+~P42(x3452,x3453,x3453)+~P22(x3454,a2,x3451)
% 58.72/58.76 [353]~P29(x3531,x3533,x3534)+~P30(x3531,x3532,x3531)+P30(x3531,x3532,x3532)+~P15(x3533,x3534)
% 58.72/58.76 [304]P29(x3041,x3041,x3041)+~P19(x3045,x3043,x3041)+~P3(x3042)+~P10(x3043,x3044)
% 58.72/58.76 [306]P29(x3061,x3061,x3061)+~P26(x3063,x3061,x3065)+~P5(x3062)+~P10(x3063,x3064)
% 58.72/58.76 [316]P8(x3161,x3161,x3162)+~P10(x3163,x3162)+~P8(x3162,x3165,x3164)+~P7(x3161,x3164)
% 58.72/58.76 [358]P35(x3581,x3582)+~P38(x3583,x3582,x3581)+~P8(x3584,x3584,x3581)+~P22(x3583,x3585,x3583)
% 58.72/58.76 [301]~P15(a5,a4)+~P16(a5,a2)+P30(a3,a4,a2)+~P39(a5)+~P19(a1,a3,a4)
% 58.72/58.76 [351]P25(a3)+~P5(a4)+~P19(a2,a3,a5)+~P26(a5,a3,a5)+~P37(a4,a3,a1)
% 58.72/58.76 [259]~P2(x2591)+P19(a4,a3,a4)+~P2(a5)+~P4(a5)+~P12(a3,a5,a4)
% 58.72/58.76 [298]~P1(x2981)+~P11(a4,x2981)+~P26(a4,a1,x2981)+P29(a1,a1,x2981)+~P2(a1)
% 58.72/58.76 [313]~P26(a4,x3131,x3131)+~P23(a2,x3131)+P30(a2,a4,a3)+~P2(a5)+~P7(a4,a3)
% 58.72/58.76 [347]~P27(x3471)+~P38(x3471,a1,x3471)+P31(x3471,a1,a5)+~P14(a2,a5)+~P30(a1,a2,a4)
% 58.72/58.76 [348]~P22(a3,x3481,x3481)+~P38(x3481,a5,x3481)+P42(a3,a3,a5)+~P18(a2)+~P7(a3,a3)
% 58.72/58.76 [192]~P23(x1921,x1922)+P19(x1921,x1922,a4)+~P10(x1922,a1)+~P1(a1)+~P2(a4)
% 58.72/58.76 [200]~P5(x2002)+P30(x2001,x2001,x2001)+~P4(x2002)+~P7(x2001,a3)+~P16(a3,x2002)
% 58.72/58.76 [221]~P5(x2211)+P36(x2211,x2211)+~P36(x2212,x2211)+~P12(x2212,a1,x2212)+~P41(a1)
% 58.72/58.76 [73]~P6(x731)+~P47(x732)+P47(x731)+~P44(x731,x733)+~P17(x732)
% 58.72/58.76 [314]~P1(x3141)+~P5(x3141)+~P12(x3143,x3143,x3143)+P26(x3141,x3141,x3141)+~P23(x3142,x3143)
% 58.72/58.76 [323]~P22(x3231,x3233,x3231)+P22(x3231,x3231,x3231)+~P7(x3232,x3233)+~P11(x3233,a3)+~P16(a3,a3)
% 58.72/58.76 [346]P30(x3461,x3461,x3462)+~P30(x3461,x3463,x3461)+~P37(a4,x3461,x3463)+~P1(a5)+~P46(a4)
% 58.72/58.76 [183]~P41(x1831)+P22(x1831,x1831,x1831)+~P1(x1832)+~P10(x1834,x1833)+~P45(x1833)
% 58.72/58.76 [204]~P3(x2041)+~P10(x2042,x2042)+P37(x2041,x2042,x2041)+~P23(x2044,x2041)+~P2(x2043)
% 58.72/58.76 [315]~P45(x3151)+~P8(x3153,x3154,x3153)+P8(x3151,x3151,x3151)+~P18(x3152)+~P15(x3153,x3154)
% 58.72/58.76 [350]~P4(x3502)+~P39(x3502)+~P38(x3502,x3502,x3502)+P38(x3501,x3502,x3501)+~P12(x3503,x3504,x3501)
% 58.72/58.76 [356]~P12(x3563,x3563,x3562)+~P12(x3561,x3564,x3564)+P22(x3561,x3562,x3561)+~P16(x3564,x3561)+~P45(x3563)
% 58.72/58.76 [362]~P26(x3622,x3624,x3624)+~P37(x3623,x3622,x3624)+P37(x3621,x3621,x3621)+~P19(x3621,x3624,x3622)+~P23(x3622,x3623)
% 58.72/58.76 [299]~P32(x2995,x2995,x2992)+P24(x2991,x2992)+~P28(x2991,x2993)+~P35(x2994,x2993)+~P24(x2995,x2992)
% 58.72/58.76 %EqnAxiom
% 58.72/58.76
% 58.72/58.76 %-------------------------------------------
% 58.85/58.84 cnf(364,plain,
% 58.85/58.84 (P12(x3641,a1,x3642)),
% 58.85/58.84 inference(rename_variables,[],[38])).
% 58.85/58.84 cnf(370,plain,
% 58.85/58.84 (P37(a1,a1,a2)),
% 58.85/58.84 inference(scs_inference,[],[38,1,8,28,2,232,225,123,150])).
% 58.85/58.84 cnf(371,plain,
% 58.85/58.84 (P23(a2,x3711)),
% 58.85/58.84 inference(rename_variables,[],[28])).
% 58.85/58.84 cnf(375,plain,
% 58.85/58.84 (P29(a4,a4,a4)),
% 58.85/58.84 inference(scs_inference,[],[38,364,1,6,7,8,28,2,16,232,225,123,150,152,256])).
% 58.85/58.84 cnf(376,plain,
% 58.85/58.84 (P12(x3761,a1,x3762)),
% 58.85/58.84 inference(rename_variables,[],[38])).
% 58.85/58.84 cnf(378,plain,
% 58.85/58.84 (P37(a5,a5,a5)),
% 58.85/58.84 inference(scs_inference,[],[38,364,376,1,6,7,8,28,2,16,232,225,123,150,152,256,328])).
% 58.85/58.84 cnf(386,plain,
% 58.85/58.84 (P30(x3861,x3861,x3861)),
% 58.85/58.84 inference(scs_inference,[],[38,364,376,1,6,7,8,28,2,3,16,232,225,123,150,152,256,328,109,253,337])).
% 58.85/58.84 cnf(388,plain,
% 58.85/58.84 (P26(a4,x3881,a4)),
% 58.85/58.84 inference(scs_inference,[],[38,364,376,1,6,7,8,28,371,2,3,16,232,225,123,150,152,256,328,109,253,337,166])).
% 58.85/58.84 cnf(390,plain,
% 58.85/58.84 (P37(a1,a1,a1)),
% 58.85/58.84 inference(scs_inference,[],[38,364,376,1,6,7,8,28,371,2,3,16,232,225,123,150,152,256,328,109,253,337,166,292])).
% 58.85/58.84 cnf(394,plain,
% 58.85/58.84 (P39(x3941)),
% 58.85/58.84 inference(scs_inference,[],[38,364,376,27,1,6,7,8,28,371,2,3,16,232,225,123,150,152,256,328,109,253,337,166,292,113,202])).
% 58.85/58.84 cnf(404,plain,
% 58.85/58.84 (P45(a1)+~P46(a3)),
% 58.85/58.84 inference(scs_inference,[],[1,41])).
% 58.85/58.84 cnf(405,plain,
% 58.85/58.84 (P45(a1)+~P46(a1)),
% 58.85/58.84 inference(scs_inference,[],[394,42])).
% 58.85/58.84 cnf(409,plain,
% 58.85/58.84 (P19(a4,a4,a4)),
% 58.85/58.84 inference(scs_inference,[],[6,81])).
% 58.85/58.84 cnf(410,plain,
% 58.85/58.84 (P29(a3,a3,a3)),
% 58.85/58.84 inference(scs_inference,[],[5,83])).
% 58.85/58.84 cnf(411,plain,
% 58.85/58.84 (P19(a3,a3,a3)),
% 58.85/58.84 inference(scs_inference,[],[1,5,90])).
% 58.85/58.84 cnf(413,plain,
% 58.85/58.84 (P29(x4131,x4131,x4131)+~P1(x4131)),
% 58.85/58.84 inference(scs_inference,[],[1,124])).
% 58.85/58.84 cnf(420,plain,
% 58.85/58.84 (P26(x4201,x4202,x4201)+~P3(x4201)+~P23(a2,x4202)),
% 58.85/58.84 inference(scs_inference,[],[2,166])).
% 58.85/58.84 cnf(421,plain,
% 58.85/58.84 (~P5(x4211)+~P16(x4211,x4212)+P38(x4212,a4,x4211)),
% 58.85/58.84 inference(scs_inference,[],[6,167])).
% 58.85/58.84 cnf(422,plain,
% 58.85/58.84 (~P29(a2,x4221,x4222)+P25(a5)),
% 58.85/58.84 inference(scs_inference,[],[3,394,179])).
% 58.85/58.84 cnf(423,plain,
% 58.85/58.84 (P22(x4231,x4231,x4231)+~P45(x4232)+~P41(x4231)+~P10(x4233,x4232)),
% 58.85/58.84 inference(scs_inference,[],[1,183])).
% 58.85/58.84 cnf(425,plain,
% 58.85/58.84 (P37(x4251,x4252,x4251)+~P3(x4251)+~P10(x4252,x4252)+~P23(x4253,x4251)),
% 58.85/58.84 inference(scs_inference,[],[4,204])).
% 58.85/58.84 cnf(426,plain,
% 58.85/58.84 (P15(x4261,x4262)+~P23(x4263,x4261)+~P12(x4262,x4261,x4263)),
% 58.85/58.84 inference(scs_inference,[],[4,217])).
% 58.85/58.84 cnf(430,plain,
% 58.85/58.84 (P30(a5,x4301,x4302)+~P29(x4301,x4302,a5)),
% 58.85/58.84 inference(scs_inference,[],[3,253])).
% 58.85/58.84 cnf(432,plain,
% 58.85/58.84 (P30(a4,a5,a5)+~P15(a4,a2)),
% 58.85/58.84 inference(scs_inference,[],[378,261])).
% 58.85/58.84 cnf(433,plain,
% 58.85/58.84 (P19(x4331,x4332,x4332)+~P12(x4332,x4332,x4331)),
% 58.85/58.84 inference(scs_inference,[],[6,262])).
% 58.85/58.84 cnf(434,plain,
% 58.85/58.84 (P37(x4341,x4341,x4342)+~P19(x4341,x4342,x4342)),
% 58.85/58.84 inference(scs_inference,[],[4,265])).
% 58.85/58.84 cnf(436,plain,
% 58.85/58.84 (P29(x4361,x4362,x4361)+~P29(x4362,x4363,x4361)),
% 58.85/58.84 inference(scs_inference,[],[2,6,282])).
% 58.85/58.84 cnf(438,plain,
% 58.85/58.84 (P37(x4381,x4381,x4381)+~P26(x4382,a1,x4381)),
% 58.85/58.84 inference(scs_inference,[],[2,28,292])).
% 58.85/58.84 cnf(439,plain,
% 58.85/58.84 (P28(a1,a1)+~P8(a4,a4,a5)),
% 58.85/58.84 inference(scs_inference,[],[390,300])).
% 58.85/58.84 cnf(445,plain,
% 58.85/58.84 (~P10(x4451,x4452)+~P19(x4452,a4,x4452)+P19(x4451,a3,x4452)),
% 58.85/58.84 inference(scs_inference,[],[37,349])).
% 58.85/58.84 cnf(448,plain,
% 58.85/58.84 (P19(a5,a2,a2)),
% 58.85/58.84 inference(scs_inference,[],[35,1,413,433])).
% 58.85/58.84 cnf(455,plain,
% 58.85/58.84 (P38(a4,a4,a4)),
% 58.85/58.84 inference(scs_inference,[],[35,388,1,413,433,434,438,231])).
% 58.85/58.84 cnf(460,plain,
% 58.85/58.84 (P12(x4601,a1,x4602)),
% 58.85/58.84 inference(rename_variables,[],[38])).
% 58.85/58.84 cnf(462,plain,
% 58.85/58.84 (P15(a2,a5)),
% 58.85/58.84 inference(scs_inference,[],[32,34,35,38,388,1,26,413,433,434,438,231,232,334,426])).
% 58.85/58.84 cnf(464,plain,
% 58.85/58.84 (P41(a4)),
% 58.85/58.84 inference(scs_inference,[],[32,34,35,38,394,388,1,6,26,413,433,434,438,231,232,334,426,44])).
% 58.85/58.84 cnf(467,plain,
% 58.85/58.84 (P8(a5,a5,a5)),
% 58.85/58.84 inference(scs_inference,[],[32,34,35,38,394,388,1,6,26,413,433,434,438,231,232,334,426,44,148])).
% 58.85/58.84 cnf(473,plain,
% 58.85/58.84 (P29(a2,a2,a2)),
% 58.85/58.84 inference(scs_inference,[],[37,32,34,35,38,460,394,388,8,1,6,17,26,413,433,434,438,231,232,334,426,44,148,328,152])).
% 58.85/58.84 cnf(478,plain,
% 58.85/58.84 (P8(a4,a4,a4)),
% 58.85/58.84 inference(scs_inference,[],[37,32,34,35,38,460,394,388,15,8,1,6,17,26,28,413,433,434,438,231,232,334,426,44,148,328,152,425,87])).
% 58.85/58.84 cnf(482,plain,
% 58.85/58.84 (P18(x4821)+~P1(x4821)),
% 58.85/58.84 inference(scs_inference,[],[462,63])).
% 58.85/58.84 cnf(484,plain,
% 58.85/58.84 (P18(a1)),
% 58.85/58.84 inference(scs_inference,[],[1,482])).
% 58.85/58.84 cnf(486,plain,
% 58.85/58.84 (P19(x4861,a1,a1)),
% 58.85/58.84 inference(scs_inference,[],[38,1,482,433])).
% 58.85/58.84 cnf(487,plain,
% 58.85/58.84 (P12(x4871,a1,x4872)),
% 58.85/58.84 inference(rename_variables,[],[38])).
% 58.85/58.84 cnf(489,plain,
% 58.85/58.84 (P37(a3,a3,a3)),
% 58.85/58.84 inference(scs_inference,[],[38,1,411,482,433,434])).
% 58.85/58.84 cnf(493,plain,
% 58.85/58.84 (P19(a1,a3,a4)),
% 58.85/58.84 inference(scs_inference,[],[35,38,11,1,411,409,482,433,434,232,445])).
% 58.85/58.84 cnf(495,plain,
% 58.85/58.84 (P29(a3,x4951,a3)),
% 58.85/58.84 inference(scs_inference,[],[37,35,38,410,11,1,411,409,482,433,434,232,445,334])).
% 58.85/58.84 cnf(498,plain,
% 58.85/58.84 (P15(a1,x4981)),
% 58.85/58.84 inference(scs_inference,[],[37,35,38,487,410,11,1,411,409,28,482,433,434,232,445,334,426])).
% 58.85/58.84 cnf(502,plain,
% 58.85/58.84 (P29(a4,a4,a2)),
% 58.85/58.84 inference(scs_inference,[],[37,35,38,487,8,410,11,1,411,18,409,28,482,433,434,232,445,334,426,152])).
% 58.85/58.84 cnf(514,plain,
% 58.85/58.84 (P8(x5141,x5141,x5142)+~P18(x5143)+~P29(x5142,x5143,x5141)),
% 58.85/58.84 inference(scs_inference,[],[484,286])).
% 58.85/58.84 cnf(516,plain,
% 58.85/58.84 (P25(a5)),
% 58.85/58.84 inference(scs_inference,[],[473,422])).
% 58.85/58.84 cnf(518,plain,
% 58.85/58.84 (P18(a2)),
% 58.85/58.84 inference(scs_inference,[],[2,482])).
% 58.85/58.84 cnf(520,plain,
% 58.85/58.84 (P37(x5201,x5201,a1)),
% 58.85/58.84 inference(scs_inference,[],[486,2,482,434])).
% 58.85/58.84 cnf(522,plain,
% 58.85/58.84 (P8(a2,a2,a2)),
% 58.85/58.84 inference(scs_inference,[],[473,486,2,482,434,514])).
% 58.85/58.84 cnf(524,plain,
% 58.85/58.84 (P29(x5241,x5242,a3)),
% 58.85/58.84 inference(scs_inference,[],[37,473,486,495,2,482,434,514,334])).
% 58.85/58.84 cnf(533,plain,
% 58.85/58.84 (P38(a1,a1,a1)),
% 58.85/58.84 inference(scs_inference,[],[37,8,6,473,486,495,27,2,16,28,482,434,514,334,152,425,231])).
% 58.85/58.84 cnf(535,plain,
% 58.85/58.84 (~P7(x5351,x5352)+P31(a1,x5351,x5352)),
% 58.85/58.84 inference(scs_inference,[],[37,8,6,473,486,495,27,2,16,28,482,434,514,334,152,425,231,291])).
% 58.85/58.84 cnf(540,plain,
% 58.85/58.84 (P14(x5401,x5401)+~P25(x5401)),
% 58.85/58.84 inference(scs_inference,[],[518,52])).
% 58.85/58.84 cnf(541,plain,
% 58.85/58.84 (~P15(x5411,x5412)+~P14(x5411,x5411)+P14(x5412,x5412)),
% 58.85/58.84 inference(scs_inference,[],[516,115])).
% 58.85/58.84 cnf(542,plain,
% 58.85/58.84 (P22(x5421,a5,a5)+~P30(x5421,a5,a5)),
% 58.85/58.84 inference(scs_inference,[],[516,228])).
% 58.85/58.84 cnf(543,plain,
% 58.85/58.84 (~P38(x5431,a5,x5431)+~P22(a3,x5431,x5431)+P42(a3,a3,a5)+~P7(a3,a3)),
% 58.85/58.84 inference(scs_inference,[],[518,348])).
% 58.85/58.84 cnf(546,plain,
% 58.85/58.84 (P22(a5,a5,a5)),
% 58.85/58.84 inference(scs_inference,[],[386,516,540,542])).
% 58.85/58.84 cnf(549,plain,
% 58.85/58.84 (P8(a3,a3,x5491)),
% 58.85/58.84 inference(scs_inference,[],[524,386,484,516,540,542,514])).
% 58.85/58.84 cnf(550,plain,
% 58.85/58.84 (P29(x5501,x5502,a3)),
% 58.85/58.84 inference(rename_variables,[],[524])).
% 58.85/58.84 cnf(552,plain,
% 58.85/58.84 (P29(a1,x5521,x5522)),
% 58.85/58.84 inference(scs_inference,[],[38,524,550,386,484,516,540,542,514,334])).
% 58.85/58.84 cnf(553,plain,
% 58.85/58.84 (P12(x5531,a1,x5532)),
% 58.85/58.84 inference(rename_variables,[],[38])).
% 58.85/58.84 cnf(556,plain,
% 58.85/58.84 (P16(a1,a1)),
% 58.85/58.84 inference(scs_inference,[],[38,553,448,524,550,386,484,516,28,540,542,514,334,325])).
% 58.85/58.84 cnf(560,plain,
% 58.85/58.84 (P30(a5,a1,x5601)),
% 58.85/58.84 inference(scs_inference,[],[38,553,448,524,550,386,484,516,28,540,542,514,334,325,430])).
% 58.85/58.84 cnf(564,plain,
% 58.85/58.84 (P30(a1,x5641,x5641)+~P5(x5642)),
% 58.85/58.84 inference(scs_inference,[],[38,553,448,524,550,386,484,516,28,540,542,514,334,325,430,541,258])).
% 58.85/58.84 cnf(577,plain,
% 58.85/58.84 (P8(x5771,x5771,a1)),
% 58.85/58.84 inference(scs_inference,[],[552,518,514])).
% 58.85/58.84 cnf(580,plain,
% 58.85/58.84 (P29(a3,x5801,a2)),
% 58.85/58.84 inference(scs_inference,[],[34,552,524,518,514,334])).
% 58.85/58.84 cnf(594,plain,
% 58.85/58.84 (P38(x5941,x5941,x5941)+~P5(x5941)),
% 58.85/58.84 inference(scs_inference,[],[35,34,455,7,388,486,27,552,524,5,518,28,514,334,425,283,123,426,344])).
% 58.85/58.84 cnf(597,plain,
% 58.85/58.84 (P16(x5971,a5)+~P16(a5,a5)+~P46(x5971)),
% 58.85/58.84 inference(scs_inference,[],[35,34,455,7,388,486,27,552,524,19,5,518,28,514,334,425,111])).
% 58.85/58.84 cnf(598,plain,
% 58.85/58.84 (P8(a2,a2,a3)),
% 58.85/58.84 inference(scs_inference,[],[580,484,514])).
% 58.85/58.84 cnf(601,plain,
% 58.85/58.84 (P29(a5,x6011,a1)),
% 58.85/58.84 inference(scs_inference,[],[29,580,552,484,514,334])).
% 58.85/58.84 cnf(615,plain,
% 58.85/58.84 (P8(a1,a1,a5)),
% 58.85/58.84 inference(scs_inference,[],[601,518,514])).
% 58.85/58.84 cnf(618,plain,
% 58.85/58.84 (P29(a2,x6181,a4)),
% 58.85/58.84 inference(scs_inference,[],[36,601,524,518,514,334])).
% 58.85/58.84 cnf(631,plain,
% 58.85/58.84 (P8(a4,a4,a2)),
% 58.85/58.84 inference(scs_inference,[],[618,484,514])).
% 58.85/58.84 cnf(653,plain,
% 58.85/58.84 (P22(a1,a1,a1)+~P46(a3)),
% 58.85/58.84 inference(scs_inference,[],[556,38,404,356])).
% 58.85/58.84 cnf(663,plain,
% 58.85/58.84 (P8(x6631,x6631,x6631)+~P46(x6631)+~P45(a1)),
% 58.85/58.84 inference(scs_inference,[],[35,533,7,486,502,276])).
% 58.85/58.84 cnf(693,plain,
% 58.85/58.84 (P22(a4,a4,a4)+~P45(a2)),
% 58.85/58.84 inference(scs_inference,[],[35,7,13,486,464,283,123,426,423])).
% 58.85/58.84 cnf(698,plain,
% 58.85/58.84 (P8(a3,a1,a3)+~P46(a1)),
% 58.85/58.84 inference(scs_inference,[],[35,7,13,486,498,560,21,4,464,283,123,426,423,191,308])).
% 58.85/58.84 cnf(1383,plain,
% 58.85/58.84 (P30(a1,x13831,x13831)),
% 58.85/58.84 inference(scs_inference,[],[19,53,564])).
% 58.85/58.84 cnf(1530,plain,
% 58.85/58.84 (P46(a3)),
% 58.85/58.84 inference(scs_inference,[],[28,13,54,62])).
% 58.85/58.84 cnf(1531,plain,
% 58.85/58.84 (P46(x15311)+~P10(x15311,x15312)),
% 58.85/58.84 inference(scs_inference,[],[1530,62])).
% 58.85/58.84 cnf(1532,plain,
% 58.85/58.84 (P36(x15321,x15321)+~P41(x15321)+~P16(x15322,x15322)),
% 58.85/58.84 inference(scs_inference,[],[1530,75])).
% 58.85/58.84 cnf(1533,plain,
% 58.85/58.84 (P45(a1)),
% 58.85/58.84 inference(scs_inference,[],[1530,404])).
% 58.85/58.84 cnf(1534,plain,
% 58.85/58.84 (P22(a1,a1,a1)),
% 58.85/58.84 inference(scs_inference,[],[1530,653])).
% 58.85/58.84 cnf(1535,plain,
% 58.85/58.84 (P36(a4,a4)),
% 58.85/58.84 inference(scs_inference,[],[556,464,1532])).
% 58.85/58.84 cnf(1537,plain,
% 58.85/58.84 (P16(a3,a3)),
% 58.85/58.84 inference(scs_inference,[],[34,1530,556,28,464,1532,219])).
% 58.85/58.84 cnf(1540,plain,
% 58.85/58.84 (P8(a2,a3,a2)),
% 58.85/58.84 inference(scs_inference,[],[34,1530,556,28,386,464,22,1532,219,308])).
% 58.85/58.84 cnf(1550,plain,
% 58.85/58.84 (P16(a3,a5)+~P16(a5,a5)),
% 58.85/58.84 inference(scs_inference,[],[35,34,7,486,1530,556,28,386,19,464,22,1532,219,308,123,283,426,111])).
% 58.85/58.84 cnf(1557,plain,
% 58.85/58.84 (P14(x15571,x15571)+~P15(x15571,x15571)),
% 58.85/58.84 inference(scs_inference,[],[1533,72])).
% 58.85/58.84 cnf(1558,plain,
% 58.85/58.84 (P40(x15581)+~P27(x15581)+~P23(x15582,x15581)),
% 58.85/58.84 inference(scs_inference,[],[1535,88])).
% 58.85/58.84 cnf(1559,plain,
% 58.85/58.84 (P32(x15591,x15591,x15591)+~P27(x15591)),
% 58.85/58.84 inference(scs_inference,[],[1535,161])).
% 58.85/58.84 cnf(1560,plain,
% 58.85/58.84 (P22(x15601,x15601,x15601)+~P22(x15601,x15602,x15601)+~P7(x15603,x15602)+~P11(x15602,a3)),
% 58.85/58.84 inference(scs_inference,[],[1537,323])).
% 58.85/58.84 cnf(1563,plain,
% 58.85/58.84 (~P46(x15631)+P8(x15631,x15631,x15631)),
% 58.85/58.84 inference(scs_inference,[],[1533,663])).
% 58.85/58.84 cnf(1565,plain,
% 58.85/58.84 (P15(a1,x15651)),
% 58.85/58.84 inference(rename_variables,[],[498])).
% 58.85/58.84 cnf(1576,plain,
% 58.85/58.84 (P8(a5,a3,a5)+~P30(x15761,a3,a5)),
% 58.85/58.84 inference(scs_inference,[],[35,7,486,498,1565,1530,19,22,1557,541,123,283,426,1560,308])).
% 58.85/58.84 cnf(1671,plain,
% 58.85/58.84 (P16(a2,a2)),
% 58.85/58.84 inference(scs_inference,[],[35,448,28,325])).
% 58.85/58.84 cnf(1679,plain,
% 58.85/58.84 (P16(a3,a2)),
% 58.85/58.84 inference(scs_inference,[],[35,448,1530,386,28,20,4,325,151,297,111])).
% 58.85/58.84 cnf(1681,plain,
% 58.85/58.84 (P22(a2,a2,a2)),
% 58.85/58.84 inference(scs_inference,[],[35,448,1530,386,28,20,4,325,151,297,111,119])).
% 58.85/58.84 cnf(2932,plain,
% 58.85/58.84 (P29(a2,a2,a5)),
% 58.85/58.84 inference(scs_inference,[],[7,17,152])).
% 58.85/58.84 cnf(2934,plain,
% 58.85/58.84 (P29(a2,x29341,a2)),
% 58.85/58.84 inference(scs_inference,[],[35,7,17,152,334])).
% 58.85/58.84 cnf(2936,plain,
% 58.85/58.84 (P8(a5,a5,a2)),
% 58.85/58.84 inference(scs_inference,[],[35,7,17,518,152,334,514])).
% 58.85/58.84 cnf(2938,plain,
% 58.85/58.84 (P30(a5,a2,a2)),
% 58.85/58.84 inference(scs_inference,[],[35,7,17,518,152,334,514,430])).
% 58.85/58.84 cnf(2945,plain,
% 58.85/58.84 (P29(a4,a4,a5)),
% 58.85/58.84 inference(scs_inference,[],[7,18,152])).
% 58.85/58.84 cnf(2947,plain,
% 58.85/58.84 (P30(a5,a4,a4)),
% 58.85/58.84 inference(scs_inference,[],[7,18,152,430])).
% 58.85/58.84 cnf(3010,plain,
% 58.85/58.84 (P42(a2,a2,a1)+~P42(a1,x30101,x30101)),
% 58.85/58.84 inference(scs_inference,[],[34,7,486,2945,1681,484,514,426,283,123,345])).
% 58.85/58.84 cnf(3032,plain,
% 58.85/58.84 (P38(a5,a5,a5)),
% 58.85/58.84 inference(scs_inference,[],[7,98,244])).
% 58.85/58.84 cnf(3543,plain,
% 58.85/58.84 (P7(a2,a2)),
% 58.85/58.84 inference(scs_inference,[],[2,100,190])).
% 58.85/58.84 cnf(5130,plain,
% 58.85/58.84 (P42(a2,a2,a1)),
% 58.85/58.84 inference(scs_inference,[],[1533,108,3010])).
% 58.85/58.84 cnf(5642,plain,
% 58.85/58.84 (P32(x56421,x56421,x56421)),
% 58.85/58.84 inference(scs_inference,[],[1383,173,1559])).
% 58.85/58.84 cnf(6846,plain,
% 58.85/58.84 (~P5(a5)+P35(a5,a5)),
% 58.85/58.84 inference(scs_inference,[],[467,546,594,358])).
% 58.85/58.84 cnf(7067,plain,
% 58.85/58.84 (P35(a5,a5)),
% 58.85/58.84 inference(scs_inference,[],[16,6846,53])).
% 58.85/58.84 cnf(7835,plain,
% 58.85/58.84 (P35(a4,a4)+~P45(a2)),
% 58.85/58.84 inference(scs_inference,[],[455,478,693,358])).
% 58.85/58.84 cnf(8006,plain,
% 58.85/58.84 (P26(a3,x80061,a3)),
% 58.85/58.84 inference(scs_inference,[],[5,28,420])).
% 58.85/58.84 cnf(8008,plain,
% 58.85/58.84 (P41(a3)),
% 58.85/58.84 inference(scs_inference,[],[5,394,28,420,44])).
% 58.85/58.84 cnf(8067,plain,
% 58.85/58.84 (P24(a4,a4)+~P45(a2)),
% 58.85/58.84 inference(scs_inference,[],[7835,67])).
% 58.85/58.84 cnf(8218,plain,
% 58.85/58.84 (P24(x82181,a4)+~P28(x82181,a5)+~P45(a2)),
% 58.85/58.84 inference(scs_inference,[],[5642,7067,8067,299])).
% 58.85/58.84 cnf(8369,plain,
% 58.85/58.84 (P31(a3,a3,a1)+~P46(a1)),
% 58.85/58.84 inference(scs_inference,[],[8008,698,272])).
% 58.85/58.84 cnf(9390,plain,
% 58.85/58.84 (P22(a3,a3,a3)),
% 58.85/58.84 inference(scs_inference,[],[1530,8008,1563,271])).
% 58.85/58.84 cnf(11613,plain,
% 58.85/58.84 (P13(a1)+~P46(a1)),
% 58.85/58.84 inference(scs_inference,[],[8369,174])).
% 58.85/58.84 cnf(11869,plain,
% 58.85/58.84 (P35(x118691,x118691)+~P35(a1,x118692)+~P46(a1)),
% 58.85/58.84 inference(scs_inference,[],[394,11613,76])).
% 58.85/58.84 cnf(13742,plain,
% 58.85/58.84 (P38(a2,a2,a2)),
% 58.85/58.84 inference(scs_inference,[],[28,136,244])).
% 58.85/58.84 cnf(14475,plain,
% 58.85/58.84 (P38(a3,a3,a3)),
% 58.85/58.84 inference(scs_inference,[],[22,138,244])).
% 58.85/58.84 cnf(14476,plain,
% 58.85/58.84 (~P45(a3)),
% 58.85/58.84 inference(scs_inference,[],[39,38,14475,322])).
% 58.85/58.84 cnf(14983,plain,
% 58.85/58.84 (P7(a4,a4)),
% 58.85/58.84 inference(scs_inference,[],[26,140,190])).
% 58.85/58.84 cnf(14984,plain,
% 58.85/58.84 (P22(a3,a4,a3)),
% 58.85/58.84 inference(scs_inference,[],[8008,14983,153])).
% 58.85/58.84 cnf(15496,plain,
% 58.85/58.84 (P7(a3,a3)),
% 58.85/58.84 inference(scs_inference,[],[22,142,190])).
% 58.85/58.84 cnf(15497,plain,
% 58.85/58.84 (~P22(a3,x154971,x154971)+~P38(x154971,a5,x154971)+P42(a3,a3,a5)),
% 58.85/58.84 inference(scs_inference,[],[15496,543])).
% 58.85/58.84 cnf(15736,plain,
% 58.85/58.84 (P36(a5,a1)),
% 58.85/58.84 inference(scs_inference,[],[498,19,144,209])).
% 58.85/58.84 cnf(15992,plain,
% 58.85/58.84 (~P7(a5,a4)+P28(a1,a1)),
% 58.85/58.84 inference(scs_inference,[],[145,439])).
% 58.85/58.84 cnf(16248,plain,
% 58.85/58.84 (~P5(a4)+~P19(x162481,a4,a5)+P28(a1,a1)),
% 58.85/58.84 inference(scs_inference,[],[14983,15992,218])).
% 58.85/58.84 cnf(16266,plain,
% 58.85/58.84 (P8(a2,a2,a4)),
% 58.85/58.84 inference(scs_inference,[],[11,3543,631,316])).
% 58.85/58.84 cnf(18009,plain,
% 58.85/58.84 (P27(a5)+~P15(a4,a2)),
% 58.85/58.84 inference(scs_inference,[],[432,173])).
% 58.85/58.84 cnf(18220,plain,
% 58.85/58.84 (P40(a5)+~P15(a4,a2)),
% 58.85/58.84 inference(scs_inference,[],[28,18009,1558])).
% 58.85/58.84 cnf(18299,plain,
% 58.85/58.84 (P38(x182991,a5,x182991)),
% 58.85/58.84 inference(scs_inference,[],[38,3032,394,7,350])).
% 58.85/58.84 cnf(18422,plain,
% 58.85/58.84 (P24(a5,a5)+~P15(a4,a2)),
% 58.85/58.84 inference(scs_inference,[],[18220,48])).
% 58.85/58.84 cnf(18617,plain,
% 58.85/58.84 (P24(x186171,a5)+~P28(x186171,a5)+~P15(a4,a2)),
% 58.85/58.84 inference(scs_inference,[],[5642,7067,18422,299])).
% 58.85/58.84 cnf(19442,plain,
% 58.85/58.84 (P38(x194421,a2,x194421)),
% 58.85/58.84 inference(scs_inference,[],[38,13742,8,394,350])).
% 58.85/58.84 cnf(21232,plain,
% 58.85/58.84 (P27(x212321)+~P26(x212321,a5,a5)),
% 58.85/58.84 inference(scs_inference,[],[223,173])).
% 58.85/58.84 cnf(22086,plain,
% 58.85/58.84 (P27(a3)),
% 58.85/58.84 inference(scs_inference,[],[489,227,173])).
% 58.85/58.84 cnf(22087,plain,
% 58.85/58.84 (P32(a4,a4,x220871)+~P22(x220871,a4,a3)),
% 58.85/58.84 inference(scs_inference,[],[22086,229])).
% 58.85/58.84 cnf(22088,plain,
% 58.85/58.84 (P32(a4,a4,a3)),
% 58.85/58.84 inference(scs_inference,[],[14984,22087])).
% 58.85/58.84 cnf(22090,plain,
% 58.85/58.84 (P40(a3)),
% 58.85/58.84 inference(scs_inference,[],[28,22086,14984,22087,1558])).
% 58.85/58.84 cnf(22107,plain,
% 58.85/58.84 (P47(x221071)+~P13(x221071)),
% 58.85/58.84 inference(scs_inference,[],[22090,45])).
% 58.85/58.84 cnf(22677,plain,
% 58.85/58.84 (P37(x226771,x226771,x226771)),
% 58.85/58.84 inference(scs_inference,[],[38,236,434])).
% 58.85/58.84 cnf(22870,plain,
% 58.85/58.84 (P35(a1,a1)),
% 58.85/58.84 inference(scs_inference,[],[386,1534,533,245,358])).
% 58.85/58.84 cnf(22871,plain,
% 58.85/58.84 (P35(x228711,x228711)+~P46(a1)),
% 58.85/58.84 inference(scs_inference,[],[22870,11869])).
% 58.85/58.84 cnf(23050,plain,
% 58.85/58.84 (P24(x230501,x230501)+~P46(a1)),
% 58.85/58.84 inference(scs_inference,[],[22871,67])).
% 58.85/58.84 cnf(23237,plain,
% 58.85/58.84 (P24(x232371,x232372)+~P28(x232371,a1)+~P46(a1)),
% 58.85/58.84 inference(scs_inference,[],[5642,22870,23050,299])).
% 58.85/58.84 cnf(23430,plain,
% 58.85/58.84 (P31(a3,a3,a3)),
% 58.85/58.84 inference(scs_inference,[],[1383,8008,246,272])).
% 58.85/58.84 cnf(23810,plain,
% 58.85/58.84 (P32(a2,a2,a1)),
% 58.85/58.84 inference(scs_inference,[],[1383,4,248,275])).
% 58.85/58.84 cnf(27138,plain,
% 58.85/58.84 (P22(a5,a5,a3)+~P30(x271381,a3,a5)),
% 58.85/58.84 inference(scs_inference,[],[8008,1576,271])).
% 58.85/58.84 cnf(29738,plain,
% 58.85/58.84 (P31(x297381,a5,a5)+~P30(x297381,a5,a3)+~P30(x297382,a3,a5)),
% 58.85/58.84 inference(scs_inference,[],[27138,339])).
% 58.85/58.84 cnf(34968,plain,
% 58.85/58.84 (P30(a4,a2,a4)),
% 58.85/58.84 inference(scs_inference,[],[4,6,121,241])).
% 58.85/58.84 cnf(34969,plain,
% 58.85/58.84 (P30(a4,a2,a2)),
% 58.85/58.84 inference(scs_inference,[],[8006,26,34968,352])).
% 58.85/58.84 cnf(36986,plain,
% 58.85/58.84 (P24(x369861,x369862)+~P28(x369861,a1)),
% 58.85/58.84 inference(scs_inference,[],[27,23237,1531])).
% 58.85/58.84 cnf(37544,plain,
% 58.85/58.84 (P22(a4,a4,a4)),
% 58.85/58.84 inference(scs_inference,[],[27,1533,464,423])).
% 58.85/58.84 cnf(38569,plain,
% 58.85/58.84 (P42(x385691,a1,a1)+~P16(a4,x385691)+~P46(a1)),
% 58.85/58.84 inference(scs_inference,[],[154,405])).
% 58.85/58.84 cnf(39021,plain,
% 58.85/58.84 (P30(x390211,a5,x390211)),
% 58.85/58.84 inference(scs_inference,[],[3,28,156,241])).
% 58.85/58.84 cnf(39023,plain,
% 58.85/58.84 (P30(x390231,a5,x390231)),
% 58.85/58.84 inference(rename_variables,[],[39021])).
% 58.85/58.84 cnf(39029,plain,
% 58.85/58.84 (P31(a3,a5,a5)+~P30(x390291,a3,a5)),
% 58.85/58.84 inference(scs_inference,[],[8006,28,39021,39023,352,542,29738])).
% 58.85/58.84 cnf(39468,plain,
% 58.85/58.84 (P48(a2)+~P30(x394681,a3,a5)),
% 58.85/58.84 inference(scs_inference,[],[462,39029,201])).
% 58.85/58.84 cnf(39685,plain,
% 58.85/58.84 (~P37(a5,a3,a5)+P48(a2)),
% 58.85/58.84 inference(scs_inference,[],[39468,227])).
% 58.85/58.84 cnf(39911,plain,
% 58.85/58.84 (P48(a2)),
% 58.85/58.84 inference(scs_inference,[],[22,28,39685,188])).
% 58.85/58.84 cnf(43228,plain,
% 58.85/58.84 (~P5(a4)+P28(a1,a1)),
% 58.85/58.84 inference(scs_inference,[],[3,28,16248,156])).
% 58.85/58.84 cnf(43393,plain,
% 58.85/58.84 (P28(a1,a1)),
% 58.85/58.84 inference(scs_inference,[],[18,43228,53])).
% 58.85/58.84 cnf(43394,plain,
% 58.85/58.84 (P24(a1,x433941)),
% 58.85/58.84 inference(scs_inference,[],[43393,36986])).
% 58.85/58.84 cnf(45731,plain,
% 58.85/58.84 (~P42(a1,a5,a1)+P6(a5)),
% 58.85/58.84 inference(scs_inference,[],[15736,560,520,210,321])).
% 58.85/58.84 cnf(45927,plain,
% 58.85/58.84 (P6(a5)),
% 58.85/58.84 inference(scs_inference,[],[1383,45731,248])).
% 58.85/58.84 cnf(45928,plain,
% 58.85/58.84 (P28(x459281,x459281)+~P22(x459281,x459281,x459281)),
% 58.85/58.84 inference(scs_inference,[],[45927,195])).
% 58.85/58.84 cnf(45949,plain,
% 58.85/58.84 (P28(a2,a2)),
% 58.85/58.84 inference(scs_inference,[],[1681,45928])).
% 58.85/58.84 cnf(45964,plain,
% 58.85/58.84 (P28(a3,a3)),
% 58.85/58.84 inference(scs_inference,[],[9390,45928])).
% 58.85/58.84 cnf(45979,plain,
% 58.85/58.84 (P28(a5,a5)),
% 58.85/58.84 inference(scs_inference,[],[546,45928])).
% 58.85/58.84 cnf(47215,plain,
% 58.85/58.84 (P26(a2,a5,a5)),
% 58.85/58.84 inference(scs_inference,[],[35,20,254,53])).
% 58.85/58.84 cnf(47218,plain,
% 58.85/58.84 (P40(a2)),
% 58.85/58.84 inference(scs_inference,[],[47215,28,21232,1558])).
% 58.85/58.84 cnf(47456,plain,
% 58.85/58.84 (P8(a1,a1,a2)),
% 58.85/58.84 inference(scs_inference,[],[35,13,520,577,190,426,316])).
% 58.85/58.84 cnf(47471,plain,
% 58.85/58.84 (P7(x474711,x474711)),
% 58.85/58.84 inference(scs_inference,[],[22677,190])).
% 58.85/58.84 cnf(47486,plain,
% 58.85/58.84 (P31(a1,x474861,x474861)),
% 58.85/58.84 inference(scs_inference,[],[533,47471,291])).
% 58.85/58.84 cnf(47509,plain,
% 58.85/58.84 (P40(x475091)),
% 58.85/58.84 inference(scs_inference,[],[18299,39021,28,19,598,173,249,209,1558])).
% 58.85/58.84 cnf(47515,plain,
% 58.85/58.84 (P13(x475151)),
% 58.85/58.84 inference(scs_inference,[],[18299,524,47486,39021,28,19,598,47218,173,249,209,1558,48,172,174])).
% 58.85/58.84 cnf(47522,plain,
% 58.85/58.84 (P48(a1)),
% 58.85/58.84 inference(scs_inference,[],[18299,7,2934,524,498,47486,39021,28,19,23430,598,47218,173,249,209,1558,48,172,174,22107,268,201])).
% 58.85/58.84 cnf(47543,plain,
% 58.85/58.84 (P25(x475431)),
% 58.85/58.84 inference(scs_inference,[],[552,172])).
% 58.85/58.84 cnf(47545,plain,
% 58.85/58.84 (P24(x475451,x475451)),
% 58.85/58.84 inference(scs_inference,[],[552,47509,172,48])).
% 58.85/58.84 cnf(47584,plain,
% 58.85/58.84 (P31(a2,a4,a4)),
% 58.85/58.84 inference(scs_inference,[],[464,16266,631,249,272])).
% 58.85/58.84 cnf(47594,plain,
% 58.85/58.84 (P22(a2,a2,a3)),
% 58.85/58.84 inference(scs_inference,[],[7,552,5130,23810,386,8008,464,1681,16266,631,1540,249,272,339,268,341,271])).
% 58.85/58.84 cnf(47676,plain,
% 58.85/58.84 (P32(x476761,a1,x476761)),
% 58.85/58.84 inference(scs_inference,[],[577,249])).
% 58.85/58.84 cnf(48004,plain,
% 58.85/58.84 (P35(x480041,x480041)),
% 58.85/58.84 inference(scs_inference,[],[35,533,7,486,394,37544,22870,1537,5130,23810,522,615,47515,39911,249,341,163,209,426,283,123,358,76])).
% 58.85/58.84 cnf(48066,plain,
% 58.85/58.84 (P26(a4,x480661,x480661)+~P15(a4,a4)),
% 58.85/58.84 inference(scs_inference,[],[35,533,7,486,6,8,1534,388,1537,370,5130,23810,43394,615,45964,47543,47676,48004,518,39911,249,163,341,285,287,299,209,123,426,283,302])).
% 58.85/58.84 cnf(48182,plain,
% 58.85/58.84 (P38(a4,a2,a2)),
% 58.85/58.84 inference(scs_inference,[],[8,375,615,249,268])).
% 58.85/58.84 cnf(49746,plain,
% 58.85/58.84 (P38(a1,a4,a1)+~P38(a4,a4,a1)),
% 58.85/58.84 inference(scs_inference,[],[36,533,6,486,552,8,388,1537,7,370,5130,23810,16266,39911,249,163,341,285,209,123,283,426,361])).
% 58.85/58.84 cnf(50917,plain,
% 58.85/58.84 (P22(a5,a2,a2)),
% 58.85/58.84 inference(scs_inference,[],[1671,5130,23810,16266,546,47543,518,47522,249,163,341,287])).
% 58.85/58.84 cnf(51746,plain,
% 58.85/58.84 (P31(a2,a5,a5)),
% 58.85/58.84 inference(scs_inference,[],[16266,39021,50917,249,339])).
% 58.85/58.84 cnf(53444,plain,
% 58.85/58.84 (P42(x534441,x534441,x534441)+~P42(x534441,a1,x534441)),
% 58.85/58.84 inference(scs_inference,[],[35,18299,19442,1537,552,486,7,8,556,6,1534,370,5130,23810,615,21,549,39911,249,209,341,163,358,285,426,283,123,354])).
% 58.85/58.84 cnf(53445,plain,
% 58.85/58.84 (P29(a1,x534451,x534452)),
% 58.85/58.84 inference(rename_variables,[],[552])).
% 58.85/58.84 cnf(53450,plain,
% 58.85/58.84 (P38(a1,a3,a1)+~P38(a3,a3,a1)),
% 58.85/58.84 inference(scs_inference,[],[35,18299,19442,1537,552,53445,486,7,498,8,556,6,8006,1534,370,5130,23810,615,21,549,39911,3,249,209,341,163,358,285,426,283,123,354,191,361])).
% 58.85/58.84 cnf(55766,plain,
% 58.85/58.84 (P22(a2,x557661,a2)),
% 58.85/58.84 inference(scs_inference,[],[38,1533,533,34,1679,1537,8,6,370,5130,23810,615,39911,249,341,163,285,209,356])).
% 58.85/58.84 cnf(55789,plain,
% 58.85/58.84 (P35(a4,a5)),
% 58.85/58.84 inference(scs_inference,[],[18299,1671,37544,5130,23810,549,615,47522,249,341,163,358])).
% 58.85/58.84 cnf(55793,plain,
% 58.85/58.84 (P22(x557931,a2,a2)),
% 58.85/58.84 inference(scs_inference,[],[18299,1671,37544,55766,5130,23810,549,615,47543,518,47522,249,341,163,358,287])).
% 58.85/58.84 cnf(55948,plain,
% 58.85/58.84 (P42(a3,a3,a5)),
% 58.85/58.84 inference(scs_inference,[],[18299,16266,9390,249,15497])).
% 58.85/58.84 cnf(56341,plain,
% 58.85/58.84 (P26(a4,x563411,x563411)),
% 58.85/58.84 inference(scs_inference,[],[18,48066,65])).
% 58.85/58.84 cnf(58448,plain,
% 58.85/58.84 (P38(a2,a4,a2)),
% 58.85/58.84 inference(scs_inference,[],[48182,556,2934,6,8,56341,55948,370,23810,631,39911,249,341,163,285,361])).
% 58.85/58.84 cnf(61184,plain,
% 58.85/58.84 (~P38(a4,a4,a1)+P36(a4,a1)),
% 58.85/58.84 inference(scs_inference,[],[18,49746,209])).
% 58.85/58.84 cnf(61530,plain,
% 58.85/58.84 (P36(a4,a1)),
% 58.85/58.84 inference(scs_inference,[],[498,61184,144])).
% 58.85/58.84 cnf(61876,plain,
% 58.85/58.84 (P42(x618761,x618761,x618761)+~P42(a1,a1,a1)),
% 58.85/58.84 inference(scs_inference,[],[47486,53444,340])).
% 58.85/58.84 cnf(63666,plain,
% 58.85/58.84 (P35(a3,a2)),
% 58.85/58.84 inference(scs_inference,[],[19442,1537,55948,23810,2936,9390,598,39911,249,341,163,358])).
% 58.85/58.84 cnf(65482,plain,
% 58.85/58.84 (P42(x654821,x654821,x654821)),
% 58.85/58.84 inference(scs_inference,[],[1533,61876,108])).
% 58.85/58.84 cnf(65489,plain,
% 58.85/58.84 (P42(a3,a3,a1)),
% 58.85/58.84 inference(scs_inference,[],[1537,55948,65482,23810,615,47594,484,39911,249,341,163,345])).
% 58.85/58.84 cnf(73385,plain,
% 58.85/58.84 (P8(a5,x733851,a5)),
% 58.85/58.84 inference(scs_inference,[],[498,524,39021,353,245])).
% 58.85/58.84 cnf(73389,plain,
% 58.85/58.84 (P8(a5,x733891,a5)),
% 58.85/58.84 inference(rename_variables,[],[73385])).
% 58.85/58.84 cnf(73399,plain,
% 58.85/58.84 (P31(a3,a5,a5)),
% 58.85/58.84 inference(scs_inference,[],[6,8,556,370,55948,23810,39021,615,8008,73385,73389,39911,249,271,341,163,285,272,339])).
% 58.85/58.84 cnf(74064,plain,
% 58.85/58.84 (~P29(a5,a2,a2)+~P26(a5,a5,a5)+P30(a2,a4,a4)),
% 58.85/58.84 inference(scs_inference,[],[18,28,359,188])).
% 58.85/58.84 cnf(74395,plain,
% 58.85/58.84 (~P15(a5,a5)+~P29(a5,a2,a2)+P30(a2,a4,a4)),
% 58.85/58.84 inference(scs_inference,[],[19,74064,187])).
% 58.85/58.84 cnf(74724,plain,
% 58.85/58.84 (~P29(a5,a2,a2)+P30(a2,a4,a4)),
% 58.85/58.84 inference(scs_inference,[],[19,74395,65])).
% 58.85/58.84 cnf(75025,plain,
% 58.85/58.84 (P30(a2,a4,a4)),
% 58.85/58.84 inference(scs_inference,[],[448,8,74724,255])).
% 58.85/58.84 cnf(85975,plain,
% 58.85/58.84 (P19(a1,a3,a3)),
% 58.85/58.84 inference(scs_inference,[],[22,27,53,169])).
% 58.85/58.84 cnf(86301,plain,
% 58.85/58.84 (P7(a4,a3)),
% 58.85/58.84 inference(scs_inference,[],[22,47471,493,53,218])).
% 58.85/58.84 cnf(95785,plain,
% 58.85/58.84 (P29(x957851,x957851,x957851)),
% 58.85/58.84 inference(scs_inference,[],[22,56341,27,53,306])).
% 58.85/58.84 cnf(95786,plain,
% 58.85/58.84 (P38(x957861,x957861,x957861)),
% 58.85/58.84 inference(scs_inference,[],[95785,244])).
% 58.85/58.84 cnf(98242,plain,
% 58.85/58.84 (P45(a2)),
% 58.85/58.84 inference(scs_inference,[],[28,95786,54,175])).
% 58.85/58.84 cnf(98243,plain,
% 58.85/58.84 (~P28(x982431,a5)+P24(x982431,a4)),
% 58.85/58.84 inference(scs_inference,[],[98242,8218])).
% 58.85/58.84 cnf(100295,plain,
% 58.85/58.84 (P38(x1002951,a2,a2)),
% 58.85/58.84 inference(scs_inference,[],[95785,8,55948,23810,47456,249,341,268])).
% 58.85/58.84 cnf(105499,plain,
% 58.85/58.84 (P5(a1)),
% 58.85/58.84 inference(scs_inference,[],[23,53])).
% 58.85/58.84 cnf(105501,plain,
% 58.85/58.84 (P46(a2)),
% 58.85/58.84 inference(scs_inference,[],[28,23,53,54])).
% 58.85/58.84 cnf(105502,plain,
% 58.85/58.84 (P23(a2,x1055021)),
% 58.85/58.84 inference(rename_variables,[],[28])).
% 58.85/58.84 cnf(105504,plain,
% 58.85/58.84 (P46(a1)),
% 58.85/58.84 inference(scs_inference,[],[10,28,23,53,54,1531])).
% 58.85/58.84 cnf(105510,plain,
% 58.85/58.84 (P31(x1055101,x1055101,x1055101)),
% 58.85/58.84 inference(scs_inference,[],[10,28,23,17,47543,53,54,1531,65,105,106])).
% 58.85/58.84 cnf(105516,plain,
% 58.85/58.84 (P38(a5,a5,a2)),
% 58.85/58.84 inference(scs_inference,[],[10,28,105502,462,23,65482,17,47543,53,54,1531,65,105,106,136,140,144])).
% 58.85/58.84 cnf(105519,plain,
% 58.85/58.84 (P12(x1055191,a1,x1055192)),
% 58.85/58.84 inference(rename_variables,[],[38])).
% 58.85/58.84 cnf(105523,plain,
% 58.85/58.84 (P42(a5,a2,a5)),
% 58.85/58.84 inference(scs_inference,[],[2938,10,28,105502,462,23,65482,1383,17,47543,38,53,54,1531,65,105,106,136,140,144,234,245,248])).
% 58.85/58.84 cnf(105528,plain,
% 58.85/58.84 (P12(x1055281,a1,x1055282)),
% 58.85/58.84 inference(rename_variables,[],[38])).
% 58.85/58.84 cnf(105534,plain,
% 58.85/58.84 (P19(a2,x1055341,a2)),
% 58.85/58.84 inference(scs_inference,[],[2938,10,28,105502,2932,462,23,5,65482,1383,17,47543,2,48004,7,38,105519,3,53,54,1531,65,105,106,136,140,144,234,245,248,436,226,121,122,155])).
% 58.85/58.84 cnf(105541,plain,
% 58.85/58.84 (P30(a5,a1,x1055411)),
% 58.85/58.85 inference(rename_variables,[],[560])).
% 58.85/58.85 cnf(105552,plain,
% 58.85/58.85 (P45(a5)),
% 58.85/58.85 inference(scs_inference,[],[2938,10,28,105502,15736,2932,43393,47486,462,23,5,65482,1383,17,47543,2,48004,18299,560,105541,7,8,19,38,105519,3,556,53,54,1531,65,105,106,136,140,144,234,245,248,436,226,121,122,155,156,157,194,188,210,211,421,175])).
% 58.85/58.85 cnf(105553,plain,
% 58.85/58.85 (P38(x1055531,a5,x1055531)),
% 58.85/58.85 inference(rename_variables,[],[18299])).
% 58.85/58.85 cnf(105556,plain,
% 58.85/58.85 (P12(x1055561,a1,x1055562)),
% 58.85/58.85 inference(rename_variables,[],[38])).
% 58.85/58.85 cnf(105559,plain,
% 58.85/58.85 (P12(a3,x1055591,a3)),
% 58.85/58.85 inference(rename_variables,[],[37])).
% 58.85/58.85 cnf(105562,plain,
% 58.85/58.85 (P12(x1055621,a1,x1055622)),
% 58.85/58.85 inference(rename_variables,[],[38])).
% 58.85/58.85 cnf(105567,plain,
% 58.85/58.85 (P23(a2,x1055671)),
% 58.85/58.85 inference(rename_variables,[],[28])).
% 58.85/58.85 cnf(105569,plain,
% 58.85/58.85 (P37(a1,a1,x1055691)),
% 58.85/58.85 inference(scs_inference,[],[2938,10,28,105502,105567,15736,2932,43393,47486,462,23,448,5,65482,1383,17,47543,2,37,27,48004,18299,560,105541,7,8006,8,19,38,105519,105528,105556,32,3,556,53,54,1531,65,105,106,136,140,144,234,245,248,436,226,121,122,155,156,157,194,188,210,211,421,175,332,333,254,255,177,193])).
% 58.85/58.85 cnf(105570,plain,
% 58.85/58.85 (P23(a2,x1055701)),
% 58.85/58.85 inference(rename_variables,[],[28])).
% 58.85/58.85 cnf(105586,plain,
% 58.85/58.85 (P23(a2,x1055861)),
% 58.85/58.85 inference(rename_variables,[],[28])).
% 58.85/58.85 cnf(105592,plain,
% 58.85/58.85 (P7(x1055921,a1)),
% 58.85/58.85 inference(scs_inference,[],[2938,22088,65489,10,28,105502,105567,105570,55793,15736,85975,2932,43393,47486,86301,1679,462,23,448,5,47471,65482,1383,17,47543,2,37,105559,493,27,48004,18299,105553,560,105541,8008,7,8006,8,19,26,39911,38,105519,105528,105556,32,1537,3,556,53,54,1531,65,105,106,136,140,144,234,245,248,436,226,121,122,155,156,157,194,188,210,211,421,175,332,333,254,255,177,193,309,322,89,331,339,186,163,341,218])).
% 58.85/58.85 cnf(105598,plain,
% 58.85/58.85 (P16(x1055981,x1055981)),
% 58.85/58.85 inference(scs_inference,[],[2938,22088,65489,10,61530,28,105502,105567,105570,105586,55793,15736,85975,2932,43393,47486,86301,1679,462,23,1533,448,5,47471,65482,1383,17,47543,2,37,105559,493,27,388,48004,18299,105553,560,105541,8008,7,8006,8,19,26,39911,38,105519,105528,105556,105562,32,1537,3,556,53,54,1531,65,105,106,136,140,144,234,245,248,436,226,121,122,155,156,157,194,188,210,211,421,175,332,333,254,255,177,193,309,322,89,331,339,186,163,341,218,220,219])).
% 58.85/58.85 cnf(105611,plain,
% 58.85/58.85 (P16(a3,a5)),
% 58.85/58.85 inference(scs_inference,[],[2938,22088,47545,65489,10,61530,28,105502,105567,105570,105586,55789,55793,15736,85975,2932,43393,47486,86301,22677,1679,45979,462,23,1533,448,5,47471,65482,1383,17,47543,2,37,105559,493,27,388,48004,18299,105553,560,105541,8008,7,8006,8,19,5642,26,39911,38,105519,105528,105556,105562,32,1537,3,556,53,54,1531,65,105,106,136,140,144,234,245,248,436,226,121,122,155,156,157,194,188,210,211,421,175,332,333,254,255,177,193,309,322,89,331,339,186,163,341,218,220,219,285,299,145,535,1550])).
% 58.85/58.85 cnf(105612,plain,
% 58.85/58.85 (P16(a2,a5)),
% 58.85/58.85 inference(scs_inference,[],[2938,22088,47545,65489,10,61530,28,105502,105567,105570,105586,55789,55793,15736,85975,2932,43393,47486,86301,22677,1679,45979,462,23,1533,448,5,47471,65482,1383,17,47543,2,37,105559,493,27,388,48004,18299,105553,560,105541,8008,7,8006,8,19,5642,26,39911,38,105519,105528,105556,105562,32,1537,3,556,53,54,1531,65,105,106,136,140,144,234,245,248,436,226,121,122,155,156,157,194,188,210,211,421,175,332,333,254,255,177,193,309,322,89,331,339,186,163,341,218,220,219,285,299,145,535,1550,597])).
% 58.85/58.85 cnf(105616,plain,
% 58.85/58.85 (P45(x1056161)+~P38(a2,x1056161,a2)),
% 58.85/58.85 inference(scs_inference,[],[105501,175])).
% 58.85/58.85 cnf(105619,plain,
% 58.85/58.85 (~P46(x1056191)+P16(x1056191,a5)),
% 58.85/58.85 inference(scs_inference,[],[105598,597])).
% 58.85/58.85 cnf(105621,plain,
% 58.85/58.85 (~P16(a4,x1056211)+P42(x1056211,a1,a1)),
% 58.85/58.85 inference(scs_inference,[],[105504,38569])).
% 58.85/58.85 cnf(105640,plain,
% 58.85/58.85 (P42(a4,a5,a5)),
% 58.85/58.85 inference(scs_inference,[],[105598,105552,2947,618,65482,16,27,26,29,498,58448,105616,226,53,248,436,1531,140,144,65,154])).
% 58.85/58.85 cnf(105641,plain,
% 58.85/58.85 (P16(x1056411,x1056411)),
% 58.85/58.85 inference(rename_variables,[],[105598])).
% 58.85/58.85 cnf(105646,plain,
% 58.85/58.85 (P19(a3,a2,a3)),
% 58.85/58.85 inference(scs_inference,[],[105510,105598,105552,2947,618,65482,16,5,27,8,26,29,498,58448,105616,226,53,248,436,1531,140,144,65,154,201,122])).
% 58.85/58.85 cnf(105666,plain,
% 58.85/58.85 (P16(x1056661,x1056661)),
% 58.85/58.85 inference(rename_variables,[],[105598])).
% 58.85/58.85 cnf(105670,plain,
% 58.85/58.85 (P42(a4,a1,a1)),
% 58.85/58.85 inference(scs_inference,[],[105510,105598,105641,105666,105592,105569,105501,105504,105516,105552,2947,51746,63666,10,28,618,1533,577,65482,16,5,37,45949,27,48004,7,8,19,26,38,29,498,4,58448,105616,226,53,248,436,1531,140,144,65,154,201,122,211,162,209,177,316,285,356,105619,105621])).
% 58.85/58.85 cnf(105688,plain,
% 58.85/58.85 (P42(a5,a4,a4)),
% 58.85/58.85 inference(scs_inference,[],[105510,105523,105598,105641,105666,105592,105534,105569,105499,105501,105504,105516,105552,2947,51746,63666,10,28,618,1533,577,47471,65482,16,5,37,45949,27,48004,464,7,8,19,26,38,29,498,4,58448,105616,226,53,248,436,1531,140,144,65,154,201,122,211,162,209,177,316,285,356,105619,105621,53450,98243,18617,421,445,153,275,309])).
% 58.85/58.85 cnf(105708,plain,
% 58.85/58.85 (P5(a2)),
% 58.85/58.85 inference(scs_inference,[],[14476,17,2945,105616,436,53])).
% 58.85/58.85 cnf(105724,plain,
% 58.85/58.85 (~P26(a3,a2,a2)),
% 58.85/58.85 inference(scs_inference,[],[105670,105612,14476,34969,100295,73399,2934,17,18,386,45964,2945,48004,7,26,6,105616,436,53,248,140,65,430,122,421,211,361])).
% 58.85/58.85 cnf(105761,plain,
% 58.85/58.85 (P5(a4)),
% 58.85/58.85 inference(scs_inference,[],[18,53])).
% 58.85/58.85 cnf(105769,plain,
% 58.85/58.85 (P15(a3,a3)),
% 58.85/58.85 inference(scs_inference,[],[105640,75025,18,22,26,552,53,140,248,436,65])).
% 58.85/58.85 cnf(105771,plain,
% 58.85/58.85 (P30(a5,a5,a1)),
% 58.85/58.85 inference(scs_inference,[],[105640,75025,18,22,26,552,53,140,248,436,65,430])).
% 58.85/58.85 cnf(105810,plain,
% 58.85/58.85 ($false),
% 58.85/58.85 inference(scs_inference,[],[105611,105646,105688,105761,105769,105771,47584,105724,105708,47471,524,5,386,45949,22,39021,8006,26,53,248,140,421,211,353,218,302]),
% 58.85/58.85 ['proof']).
% 58.96/58.90 % SZS output end Proof
% 58.96/58.90 % Total time :58.100000s
%------------------------------------------------------------------------------