%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SYN142-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 : n019.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:40 EDT 2024
% Result : Unsatisfiable 70.59s 70.65s
% Output : CNFRefutation 70.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYN142-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.34 % Computer : n019.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Sun Jun 23 18:45:09 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.53/0.58 start to proof:theBenchmark
% 70.59/70.63 %-------------------------------------------
% 70.59/70.63 % File :CSE---1.7
% 70.59/70.63 % Problem :theBenchmark
% 70.59/70.63 % Transform :cnf
% 70.59/70.63 % Format :tptp:raw
% 70.59/70.63 % Command :java -jar mcs_scs.jar %d %s
% 70.59/70.63
% 70.59/70.63 % Result :Theorem 69.970000s
% 70.59/70.63 % Output :CNFRefutation 69.970000s
% 70.59/70.63 %-------------------------------------------
% 70.59/70.64 %--------------------------------------------------------------------------
% 70.59/70.64 % File : SYN142-1 : TPTP v8.2.0. Released v1.1.0.
% 70.59/70.64 % Domain : Syntactic (Random Prolog Theory)
% 70.59/70.64 % Problem : RPT63 synthetic problem 40 (quasi-uniform distribution)
% 70.59/70.64 % Version : [SE94] axioms : Especial.
% 70.59/70.64 % English :
% 70.59/70.64
% 70.59/70.64 % Refs : [SE94] Segre & Elkan (1994), A High-Performance Explanation-B
% 70.59/70.64 % Source : [SE94]
% 70.59/70.64 % Names : - [SE94]
% 70.59/70.64
% 70.59/70.64 % Status : Unsatisfiable
% 70.59/70.64 % 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.2.0, 0.33 v2.1.0, 0.00 v2.0.0
% 70.59/70.64 % Syntax : Number of clauses : 369 ( 39 unt; 0 nHn; 362 RR)
% 70.59/70.64 % Number of literals : 1060 ( 0 equ; 692 neg)
% 70.59/70.64 % Maximal clause size : 5 ( 2 avg)
% 70.59/70.64 % Maximal term depth : 1 ( 1 avg)
% 70.59/70.65 % Number of predicates : 48 ( 48 usr; 0 prp; 1-3 aty)
% 70.59/70.65 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% 70.59/70.65 % Number of variables : 627 ( 161 sgn)
% 70.59/70.65 % SPC : CNF_UNS_EPR_NEQ_HRN
% 70.59/70.65
% 70.59/70.65 % Comments : This theory has a finite deductive closure.
% 70.59/70.65 %--------------------------------------------------------------------------
% 70.59/70.65 %----Include Synthetic domain theory for EBL
% 70.59/70.65 include('Axioms/SYN001-0.ax').
% 70.59/70.65 %--------------------------------------------------------------------------
% 70.59/70.65 cnf(prove_this,negated_conjecture,
% 70.59/70.65 ~ m5(d,X) ).
% 70.59/70.65
% 70.59/70.65 %--------------------------------------------------------------------------
% 70.59/70.65 %-------------------------------------------
% 70.59/70.65 % Proof found
% 70.59/70.65 % SZS status Theorem for theBenchmark
% 70.59/70.65 % SZS output start Proof
% 70.59/70.65 %ClaNum:362(EqnAxiom:0)
% 70.59/70.65 %VarNum:1494(SingletonVarNum:574)
% 70.59/70.65 %MaxLitNum:5
% 70.59/70.65 %MaxfuncDepth:0
% 70.59/70.65 %SharedTerms:200
% 70.59/70.65 %goalClause: 39
% 70.59/70.65 %singleGoalClaCount:1
% 70.59/70.65 [1]P1(a1)
% 70.59/70.65 [2]P1(a2)
% 70.59/70.65 [3]P2(a5)
% 70.59/70.65 [4]P2(a2)
% 70.59/70.65 [5]P3(a3)
% 70.59/70.65 [6]P3(a4)
% 70.59/70.65 [7]P4(a5)
% 70.59/70.65 [8]P4(a2)
% 70.59/70.65 [10]P10(a1,a2)
% 70.59/70.65 [11]P10(a1,a4)
% 70.59/70.65 [13]P10(a3,a2)
% 70.59/70.65 [14]P10(a2,a5)
% 70.59/70.65 [15]P10(a2,a2)
% 70.59/70.65 [16]P11(a1,a5)
% 70.59/70.65 [17]P11(a1,a2)
% 70.59/70.65 [18]P11(a1,a4)
% 70.59/70.65 [19]P11(a5,a5)
% 70.59/70.65 [20]P11(a5,a2)
% 70.59/70.65 [21]P11(a3,a2)
% 70.59/70.65 [22]P11(a2,a3)
% 70.59/70.65 [23]P11(a4,a1)
% 70.59/70.66 [26]P23(a4,a2)
% 70.59/70.66 [29]P12(a1,a5,a4)
% 70.59/70.66 [32]P12(a5,a2,a4)
% 70.59/70.66 [33]P12(a3,a5,a5)
% 70.59/70.66 [34]P12(a2,a3,a3)
% 70.59/70.66 [35]P12(a2,a2,a5)
% 70.59/70.66 [36]P12(a4,a2,a3)
% 70.59/70.66 [27]P10(x271,a1)
% 70.59/70.66 [28]P23(a2,x281)
% 70.59/70.66 [37]P12(a3,x371,a3)
% 70.59/70.66 [39]~P18(a1,x391)
% 70.59/70.66 [38]P12(x381,a1,x382)
% 70.59/70.66 [40]P19(a2)+~P5(a2)
% 70.59/70.66 [43]P34(a3,a3)+~P40(a3)
% 70.59/70.66 [58]P7(a5,a5)+~P15(a5,a5)
% 70.59/70.66 [59]P14(a1,a1)+~P7(a3,a1)
% 70.59/70.66 [60]P14(a4,a4)+~P7(a2,a4)
% 70.59/70.66 [79]P20(a5,a5,a5)+~P2(a5)
% 70.59/70.66 [80]P20(a2,a2,a2)+~P3(a2)
% 70.59/70.66 [81]P20(a4,a4,a4)+~P3(a4)
% 70.59/70.66 [82]P26(a4,a4,a4)+~P3(a4)
% 70.59/70.66 [83]P29(a3,a3,a3)+~P3(a3)
% 70.59/70.66 [85]P37(a2,a2,a2)+~P3(a2)
% 70.59/70.66 [86]P8(a3,a3,a3)+~P41(a3)
% 70.59/70.66 [87]P8(a4,a4,a4)+~P41(a4)
% 70.59/70.66 [116]P26(a1,a1,a1)+~P10(a1,a1)
% 70.59/70.66 [119]P22(a2,a2,a2)+~P16(a3,a2)
% 70.59/70.66 [120]P31(a2,a4,a2)+~P7(a4,a2)
% 70.59/70.66 [171]P24(a1,a1)+~P32(a4,a1,a4)
% 70.59/70.66 [213]P29(a4,a5,a2)+~P12(a2,a4,a5)
% 70.59/70.66 [214]P30(a1,a2,a2)+~P29(a1,a2,a5)
% 70.59/70.66 [215]P30(a3,a3,a3)+~P29(a5,a5,a3)
% 70.59/70.66 [216]P22(a2,a2,a2)+~P38(a3,a2,a3)
% 70.59/70.66 [46]~P41(x461)+P14(x461,x461)
% 70.59/70.66 [47]~P6(x471)+P18(x471,x471)
% 70.59/70.66 [48]~P40(x481)+P24(x481,x481)
% 70.59/70.66 [49]~P13(x491)+P34(x491,x491)
% 70.59/70.66 [50]~P6(x501)+P43(x501,x501)
% 70.59/70.66 [54]~P23(x541,x541)+P45(x541)
% 70.59/70.66 [68]~P21(x681,x681)+P34(x681,x681)
% 70.59/70.66 [69]~P35(x691,x691)+P34(x691,x691)
% 70.59/70.66 [96]~P1(x961)+P20(x961,x961,x961)
% 70.59/70.66 [97]~P2(x971)+P26(x971,x971,x971)
% 70.59/70.66 [98]~P4(x981)+P29(x981,x981,x981)
% 70.59/70.66 [100]~P1(x1001)+P37(x1001,x1001,x1001)
% 70.59/70.66 [101]~P2(x1011)+P37(x1011,x1011,x1011)
% 70.59/70.66 [102]~P5(x1021)+P30(x1021,x1021,x1021)
% 70.59/70.66 [103]~P19(x1031)+P8(x1031,x1031,x1031)
% 70.59/70.66 [104]~P25(x1041)+P8(x1041,x1041,x1041)
% 70.59/70.66 [105]~P25(x1051)+P22(x1051,x1051,x1051)
% 70.59/70.66 [106]~P25(x1061)+P31(x1061,x1061,x1061)
% 70.59/70.66 [107]~P41(x1071)+P42(x1071,x1071,x1071)
% 70.59/70.66 [108]~P44(x1081)+P42(x1081,x1081,x1081)
% 70.59/70.66 [134]P30(x1341,x1341,x1341)+~P15(x1341,a1)
% 70.59/70.66 [146]~P16(x1461,x1461)+P31(x1461,x1461,x1461)
% 70.59/70.66 [223]P30(x2231,a5,x2231)+~P26(x2231,a5,a5)
% 70.59/70.66 [224]P37(x2241,x2241,x2241)+~P12(x2241,a4,a2)
% 70.59/70.66 [225]P30(x2251,x2251,x2251)+~P26(a1,a1,x2251)
% 70.59/70.66 [227]~P37(x2271,a3,x2271)+P30(x2271,a3,x2271)
% 70.59/70.66 [243]~P37(x2431,x2431,x2431)+P30(x2431,x2431,x2431)
% 70.59/70.66 [244]~P29(x2441,x2441,x2441)+P38(x2441,x2441,x2441)
% 70.59/70.66 [247]~P30(x2471,x2471,x2471)+P22(x2471,x2471,x2471)
% 70.59/70.66 [53]P5(x531)+~P11(x532,x531)
% 70.59/70.66 [65]P15(x651,x651)+~P11(x652,x651)
% 70.59/70.66 [66]P24(x661,x661)+~P28(x662,x661)
% 70.59/70.66 [67]P24(x671,x671)+~P35(x672,x671)
% 70.59/70.66 [135]P20(x1351,x1351,x1351)+~P10(x1352,x1351)
% 70.59/70.66 [136]~P23(x1362,x1361)+P29(x1361,x1361,x1362)
% 70.59/70.66 [137]P29(x1371,x1371,x1371)+~P10(x1372,x1371)
% 70.59/70.66 [138]P29(x1381,x1381,x1381)+~P11(x1382,x1381)
% 70.59/70.66 [139]P29(x1391,x1391,x1391)+~P23(x1392,x1391)
% 70.59/70.66 [140]~P23(x1402,x1401)+P37(x1401,x1402,x1402)
% 70.59/70.66 [141]P37(x1411,x1411,x1411)+~P10(x1412,x1411)
% 70.59/70.66 [142]P37(x1421,x1421,x1421)+~P11(x1422,x1421)
% 70.59/70.66 [143]P30(x1431,x1431,x1431)+~P15(x1432,x1431)
% 70.59/70.66 [144]~P15(x1442,x1441)+P38(x1441,x1441,x1442)
% 70.59/70.66 [145]~P7(x1452,x1451)+P8(x1451,x1451,x1452)
% 70.59/70.66 [147]P42(x1471,x1471,x1471)+~P16(x1472,x1471)
% 70.59/70.66 [190]P7(x1901,x1901)+~P37(x1902,x1901,x1901)
% 70.59/70.66 [226]P26(x2261,a4,x2261)+~P12(x2262,x2261,a4)
% 70.59/70.66 [231]P38(x2311,x2311,x2311)+~P37(x2312,a4,x2311)
% 70.59/70.66 [232]P26(x2321,x2321,x2322)+~P12(a2,x2322,x2321)
% 70.59/70.66 [234]~P12(x2342,x2342,x2341)+P20(x2341,x2342,x2341)
% 70.59/70.66 [241]~P20(x2412,x2411,x2412)+P30(x2411,x2412,x2411)
% 70.59/70.66 [242]P30(x2421,x2421,x2421)+~P20(x2422,x2422,x2421)
% 70.59/70.66 [245]~P30(x2452,x2451,x2451)+P8(x2451,x2452,x2451)
% 70.59/70.66 [246]P8(x2461,x2461,x2461)+~P30(x2462,x2461,x2461)
% 70.59/70.66 [249]~P8(x2491,x2491,x2492)+P32(x2491,x2492,x2491)
% 70.59/70.66 [250]P32(x2501,x2501,x2501)+~P31(x2502,x2502,x2501)
% 70.59/70.66 [172]P25(x1721)+~P29(x1722,x1723,x1721)
% 70.59/70.66 [173]P27(x1731)+~P30(x1732,x1733,x1731)
% 70.59/70.66 [174]P13(x1741)+~P31(x1742,x1743,x1741)
% 70.59/70.66 [236]P20(x2361,x2361,x2361)+~P12(x2362,x2363,x2361)
% 70.59/70.66 [239]P37(x2391,x2391,x2391)+~P12(x2392,x2393,x2391)
% 70.59/70.66 [248]P42(x2481,x2482,x2481)+~P30(x2481,x2483,x2482)
% 70.59/70.66 [41]P44(a1)+~P1(a1)+~P45(a3)
% 70.59/70.66 [42]P44(a1)+~P39(a1)+~P45(a1)
% 70.59/70.66 [51]P25(a4)+~P4(a2)+~P15(a5,a4)
% 70.59/70.66 [90]P20(a3,a3,a3)+~P1(a1)+~P3(a3)
% 70.59/70.66 [132]~P15(a5,a4)+P30(a5,a4,a4)+~P39(a1)
% 70.59/70.66 [133]P8(a4,a4,a4)+~P44(a5)+~P7(a4,a5)
% 70.59/70.66 [164]P20(a2,a2,a2)+~P10(a4,a1)+~P15(a3,a2)
% 70.59/70.66 [165]P9(a2)+~P47(a5)+~P26(a2,a2,a2)
% 70.59/70.66 [197]P28(a5,a5)+~P14(a2,a3)+~P31(a2,a5,a3)
% 70.59/70.66 [198]P35(a2,a2)+~P15(a2,a4)+~P8(a4,a5,a2)
% 70.59/70.66 [199]P24(a2,a5)+~P28(a2,a5)+~P42(a1,a2,a4)
% 70.59/70.66 [222]P29(a3,a2,a3)+~P2(a2)+~P29(a3,a3,a3)
% 70.59/70.66 [260]P29(a1,a1,a2)+~P23(a1,a2)+~P12(a5,a3,a3)
% 70.59/70.66 [261]P30(a4,a5,a5)+~P15(a4,a2)+~P37(a5,a5,a5)
% 70.59/70.66 [300]P28(a1,a1)+~P37(a1,a1,a1)+~P8(a4,a4,a5)
% 70.59/70.66 [324]P37(a1,a1,a4)+~P12(a4,a2,a3)+~P20(a4,a1,a3)
% 70.59/70.66 [44]~P3(x441)+~P39(x441)+P41(x441)
% 70.59/70.66 [52]~P25(x521)+P14(x521,x521)+~P19(a2)
% 70.59/70.66 [56]~P45(x561)+~P6(x561)+P24(x561,x561)
% 70.59/70.66 [70]~P47(x701)+P18(x701,x701)+~P21(a5,a5)
% 70.59/70.66 [109]~P1(x1091)+P37(x1091,a2,a2)+~P1(a2)
% 70.59/70.66 [113]~P5(x1131)+P37(x1131,x1131,x1131)+~P1(a2)
% 70.59/70.66 [114]~P25(x1141)+P30(x1141,x1141,x1141)+~P5(a5)
% 70.59/70.66 [123]~P1(x1231)+~P4(x1231)+P26(x1231,x1231,x1231)
% 70.59/70.66 [148]P8(x1481,x1481,x1481)+~P15(a2,x1481)+~P41(a4)
% 70.59/70.66 [170]~P23(x1701,a1)+P26(a3,x1701,a2)+~P23(a3,a2)
% 70.59/70.66 [175]P44(x1751)+~P38(a2,x1751,a2)+~P45(a2)
% 70.59/70.66 [182]~P11(x1821,x1821)+P26(x1821,x1821,x1821)+~P10(a3,x1821)
% 70.59/70.66 [203]~P28(x2031,a1)+P24(a1,x2031)+~P8(a1,x2031,a3)
% 70.59/70.66 [228]~P30(x2281,a5,a5)+P22(x2281,a5,a5)+~P25(a5)
% 70.59/70.66 [229]~P22(x2291,a4,a3)+P32(a4,a4,x2291)+~P27(a3)
% 70.59/70.66 [230]~P20(a2,x2301,a5)+P26(a5,a5,x2301)+~P1(a2)
% 70.59/70.66 [233]P22(x2331,a4,x2331)+~P38(x2331,a4,a4)+~P44(a4)
% 70.59/70.66 [283]~P11(x2831,a1)+~P20(a3,x2831,a1)+P30(a3,x2831,a1)
% 70.59/70.66 [326]~P38(x3261,x3261,a2)+~P22(a5,x3261,a5)+P31(a5,a2,a5)
% 70.59/70.66 [328]~P12(x3281,a1,x3281)+P37(a5,x3281,x3281)+~P12(a5,a1,x3281)
% 70.59/70.66 [45]~P13(x451)+P46(x451)+~P40(x452)
% 70.59/70.66 [55]~P2(x551)+P18(x551,x551)+~P47(x552)
% 70.59/70.66 [57]~P19(x572)+~P47(x571)+P34(x571,x572)
% 70.59/70.66 [64]~P5(x641)+P17(x641)+~P35(x642,x642)
% 70.59/70.66 [72]~P15(x721,x721)+P14(x721,x721)+~P44(x722)
% 70.59/70.66 [121]~P2(x1211)+~P3(x1212)+P20(x1211,x1212,x1211)
% 70.59/70.66 [122]~P3(x1221)+~P4(x1222)+P20(x1221,x1222,x1221)
% 70.59/70.66 [124]~P1(x1241)+P29(x1241,x1241,x1241)+~P1(x1242)
% 70.59/70.66 [125]~P4(x1251)+P37(x1251,x1251,x1251)+~P3(x1252)
% 70.59/70.66 [126]~P2(x1261)+P30(x1261,x1261,x1261)+~P39(x1262)
% 70.59/70.66 [150]~P1(x1501)+P37(x1501,x1501,x1502)+~P23(x1502,a1)
% 70.59/70.66 [151]~P5(x1511)+P8(x1511,x1511,x1511)+~P16(x1512,a2)
% 70.59/70.66 [152]~P4(x1522)+P29(x1521,x1521,x1522)+~P11(a1,x1521)
% 70.59/70.66 [153]~P41(x1531)+P22(x1531,x1532,x1531)+~P7(a4,x1532)
% 70.59/70.66 [154]~P44(x1542)+P42(x1541,x1542,x1542)+~P16(a4,x1541)
% 70.59/70.66 [155]~P1(x1551)+~P23(x1551,x1552)+P20(x1551,x1552,x1551)
% 70.59/70.66 [157]~P4(x1571)+~P11(x1572,x1572)+P20(x1571,x1571,x1572)
% 70.59/70.66 [163]~P47(x1632)+~P16(x1631,x1631)+P33(x1631,x1631,x1632)
% 70.59/70.66 [180]~P12(x1802,x1801,x1801)+P13(x1801)+~P13(x1802)
% 70.59/70.66 [187]~P15(x1872,x1871)+P26(x1871,x1871,x1871)+~P11(x1872,x1871)
% 70.59/70.66 [194]~P2(x1941)+~P30(x1941,x1942,x1941)+P14(x1941,x1942)
% 70.59/70.66 [195]~P22(x1951,x1951,x1951)+P28(x1951,x1951)+~P6(x1952)
% 70.59/70.66 [210]~P30(x2102,x2101,x2101)+P36(x2101,x2101)+~P36(x2102,x2101)
% 70.59/70.66 [211]~P28(x2111,x2111)+~P31(x2111,x2112,x2112)+P28(x2111,x2112)
% 70.59/70.66 [212]~P12(x2122,x2121,x2122)+P24(x2121,x2121)+~P24(x2122,x2121)
% 70.59/70.66 [251]~P32(x2511,x2511,x2512)+P33(a2,a2,a2)+~P9(a2)
% 70.59/70.66 [252]P30(x2521,x2521,a1)+~P12(x2522,x2521,a1)+~P39(a3)
% 70.59/70.66 [253]~P29(x2531,x2532,a5)+P30(a5,x2531,x2532)+~P2(a5)
% 70.59/70.66 [254]~P5(x2541)+~P12(x2541,x2542,a5)+P26(x2541,a5,a5)
% 70.59/70.66 [255]~P4(x2552)+~P20(x2551,x2552,a2)+P29(x2551,a2,x2552)
% 70.59/70.66 [267]~P12(x2671,x2671,x2672)+P37(x2671,x2671,x2671)+~P4(x2672)
% 70.59/70.66 [268]~P4(x2682)+~P29(x2681,x2681,x2681)+P38(x2681,x2682,x2682)
% 70.59/70.66 [269]~P26(x2691,x2691,x2692)+P38(x2691,x2691,x2691)+~P5(x2692)
% 70.59/70.66 [271]~P41(x2712)+~P8(x2711,x2712,x2711)+P22(x2711,x2711,x2712)
% 70.59/70.66 [274]~P27(x2741)+P31(x2741,x2741,x2741)+~P30(x2742,x2741,x2741)
% 70.59/70.66 [275]~P2(x2751)+~P42(x2752,x2751,x2752)+P32(x2751,x2751,x2752)
% 70.59/70.66 [289]P29(x2891,x2891,x2891)+~P15(x2891,a2)+~P12(a2,x2892,a2)
% 70.59/70.66 [290]P30(x2901,x2901,x2901)+~P37(x2902,a4,x2902)+~P7(x2901,a4)
% 70.59/70.66 [294]~P23(x2941,x2941)+P30(x2941,x2941,x2941)+~P26(x2942,x2942,x2942)
% 70.59/70.66 [327]~P37(a3,x3272,x3271)+P30(x3271,a5,x3272)+~P26(a5,x3271,a3)
% 70.59/70.66 [330]P42(x3301,x3301,x3301)+~P42(x3301,x3301,x3302)+~P12(a1,x3302,x3301)
% 70.59/70.66 [62]P45(x621)+~P10(x621,x623)+~P45(x622)
% 70.59/70.66 [63]~P1(x631)+P19(x631)+~P15(x632,x633)
% 70.59/70.66 [89]P21(x891,x892)+~P16(x893,x892)+~P48(a3,x891)
% 70.59/70.66 [156]~P2(x1561)+P20(x1561,x1562,x1561)+~P23(x1563,x1562)
% 70.59/70.66 [161]~P27(x1611)+P32(x1611,x1611,x1611)+~P36(x1612,x1613)
% 70.59/70.66 [162]~P45(x1621)+P33(x1621,x1622,x1621)+~P35(x1622,x1623)
% 70.59/70.66 [181]P9(x1811)+~P42(x1813,x1811,x1811)+~P47(x1812)
% 70.59/70.66 [186]~P23(x1861,x1861)+P26(x1861,x1862,x1861)+~P23(x1862,x1863)
% 70.59/70.66 [189]P31(x1891,x1891,x1891)+~P10(x1892,x1891)+~P7(x1893,x1893)
% 70.59/70.66 [196]~P2(x1961)+P18(x1961,x1962)+~P32(x1961,x1963,x1962)
% 70.59/70.66 [208]P14(x2081,x2081)+~P16(x2082,x2082)+~P8(x2083,x2081,x2081)
% 70.59/70.66 [209]~P38(x2093,x2091,x2092)+P36(x2091,x2092)+~P11(x2093,x2091)
% 70.59/70.66 [256]~P3(x2561)+P29(x2561,x2561,x2561)+~P12(x2562,x2563,a2)
% 70.59/70.66 [258]P30(x2581,x2582,x2582)+~P5(x2583)+~P30(a5,x2581,x2582)
% 70.59/70.66 [262]~P12(x2622,x2622,x2621)+P20(x2621,x2622,x2622)+~P3(x2623)
% 70.59/70.66 [263]P26(x2631,x2631,x2631)+~P20(x2632,x2633,x2631)+~P4(x2632)
% 70.59/70.66 [264]~P3(x2641)+P29(x2641,x2641,x2641)+~P12(x2642,x2643,x2641)
% 70.59/70.66 [265]~P20(x2651,x2652,x2652)+P37(x2651,x2651,x2652)+~P2(x2653)
% 70.59/70.66 [270]~P39(x2701)+P8(x2701,x2701,x2701)+~P30(x2702,x2703,x2703)
% 70.59/70.66 [272]~P41(x2722)+~P8(x2722,x2723,x2721)+P31(x2721,x2722,x2723)
% 70.59/70.66 [273]~P5(x2731)+P31(x2731,x2731,x2731)+~P38(x2732,x2733,x2731)
% 70.59/70.66 [293]P20(x2931,x2931,x2931)+~P10(x2932,x2932)+~P20(x2933,x2932,x2931)
% 70.59/70.66 [295]P38(x2951,x2951,x2951)+~P10(x2952,x2951)+~P26(x2952,x2951,x2953)
% 70.59/70.66 [319]P14(x3191,x3191)+~P29(x3191,x3191,x3192)+~P30(x3192,x3193,x3191)
% 70.59/70.66 [329]P30(x3291,x3291,x3291)+~P30(a3,x3292,x3291)+~P20(a3,a3,x3293)
% 70.59/70.66 [333]~P26(x3332,x3331,x3332)+P26(x3331,x3331,x3331)+~P12(x3332,x3332,x3333)
% 70.59/70.66 [335]~P30(x3352,x3351,x3352)+P30(x3351,x3351,x3351)+~P20(x3352,x3353,x3351)
% 70.59/70.66 [336]P30(x3361,x3361,x3361)+~P29(x3361,x3362,x3361)+~P37(x3363,x3363,x3363)
% 70.59/70.66 [337]~P30(x3372,x3372,x3373)+P30(x3371,x3371,x3371)+~P37(x3372,x3373,x3372)
% 70.59/70.66 [338]P8(x3381,x3381,x3381)+~P20(x3381,x3381,x3382)+~P30(x3383,x3382,x3383)
% 70.59/70.66 [340]~P42(x3402,x3402,x3402)+P42(x3401,x3401,x3401)+~P31(x3402,x3401,x3403)
% 70.59/70.66 [342]~P32(x3421,x3423,x3421)+P32(x3421,x3421,x3421)+~P22(x3422,x3423,x3421)
% 70.59/70.66 [188]P37(x1881,x1882,x1881)+~P11(x1883,x1882)+~P23(x1884,x1881)
% 70.59/70.66 [201]P47(x2011)+~P15(x2011,x2012)+~P31(x2013,x2012,x2014)
% 70.59/70.66 [291]~P7(x2912,x2913)+P31(x2911,x2912,x2913)+~P38(x2914,a1,x2911)
% 70.59/70.66 [331]~P20(x3313,x3312,x3311)+P20(x3311,x3312,x3312)+~P20(x3313,x3314,x3312)
% 70.59/70.66 [332]~P12(x3322,x3323,x3321)+P26(x3321,x3321,x3322)+~P12(x3323,x3324,x3324)
% 70.59/70.66 [334]~P29(x3343,x3341,x3344)+P29(x3341,x3342,x3343)+~P12(x3343,x3341,x3344)
% 70.59/70.66 [339]P31(x3391,x3392,x3392)+~P30(x3391,x3392,x3393)+~P22(x3392,x3394,x3393)
% 70.59/70.66 [341]~P42(x3412,x3412,x3411)+P32(x3411,x3412,x3412)+~P32(x3413,x3413,x3414)
% 70.59/70.66 [71]P6(a4)+~P27(a5)+~P11(a4,a1)+~P36(a5,a2)
% 70.59/70.66 [110]P37(a2,a5,a5)+~P1(a5)+~P3(a4)+~P4(a2)
% 70.59/70.66 [184]P14(a1,a4)+~P2(a2)+~P44(a1)+~P8(a3,a4,a3)
% 70.59/70.66 [277]P26(a1,a1,a2)+~P4(a2)+~P10(a2,a5)+~P20(a1,a5,a5)
% 70.59/70.66 [278]P26(a1,a5,a5)+~P2(a2)+~P23(a1,a1)+~P26(a5,a5,a5)
% 70.59/70.66 [279]P38(a1,a3,a3)+~P45(a4)+~P10(a5,a4)+~P38(a1,a4,a3)
% 70.59/70.66 [280]P8(a1,a1,a1)+~P41(a3)+~P16(a5,a2)+~P29(a3,a1,a2)
% 70.59/70.66 [281]P22(a4,a2,a1)+~P19(a1)+~P15(a1,a2)+~P38(a2,a4,a1)
% 70.59/70.66 [130]~P5(x1301)+P29(x1301,x1301,x1301)+~P3(a4)+~P4(a5)
% 70.59/70.66 [131]~P3(x1311)+P8(x1311,x1311,x1311)+~P2(a5)+~P41(a5)
% 70.59/70.66 [296]~P5(x2961)+P37(x2961,x2961,x2961)+~P10(x2961,a2)+~P29(a2,a2,x2961)
% 70.59/70.66 [297]~P2(x2971)+~P16(x2971,x2971)+P42(x2971,a2,x2971)+~P30(a2,x2971,a2)
% 70.59/70.66 [357]P7(x3571,x3571)+~P37(x3571,x3571,a1)+~P20(x3571,a5,x3571)+~P26(a5,a1,x3571)
% 70.59/70.66 [359]~P26(a5,a5,x3591)+~P37(a5,a4,x3591)+~P29(x3591,a2,a2)+P30(a2,a4,a4)
% 70.59/70.66 [61]~P27(x612)+~P47(x611)+P43(x611,x612)+~P4(a2)
% 70.59/70.66 [74]~P5(x741)+~P15(x742,x742)+P15(x741,x741)+~P3(x742)
% 70.59/70.66 [111]~P45(x1111)+~P16(x1112,x1112)+P16(x1111,x1112)+~P11(a5,x1112)
% 70.59/70.66 [166]~P3(x1661)+P26(x1661,x1662,x1661)+~P23(a2,x1662)+~P1(a2)
% 70.59/70.66 [167]~P5(x1672)+~P16(x1672,x1671)+P38(x1671,a4,x1672)+~P3(a4)
% 70.59/70.66 [168]~P3(x1681)+P20(x1681,x1681,x1681)+~P3(x1682)+~P23(x1682,a1)
% 70.59/70.66 [169]~P5(x1692)+~P10(x1691,x1691)+P20(x1691,x1692,x1692)+~P5(a3)
% 70.59/70.66 [179]~P29(a2,x1791,x1792)+P25(a5)+~P2(a5)+~P39(a2)
% 70.59/70.66 [191]~P2(x1911)+~P23(x1912,x1912)+P26(x1911,a1,x1912)+~P15(x1912,a1)
% 70.59/70.67 [202]P39(x2021)+~P10(x2021,x2022)+~P37(a1,x2022,a1)+~P1(a1)
% 70.59/70.67 [205]~P23(x2052,x2051)+~P11(x2052,x2052)+P20(x2051,x2051,a4)+~P15(a4,a4)
% 70.59/70.67 [206]~P23(x2061,x2062)+~P15(x2062,x2062)+P29(x2061,x2061,x2061)+~P11(x2062,x2062)
% 70.59/70.67 [276]~P45(x2761)+P8(x2761,x2761,x2761)+~P44(x2762)+~P38(a1,x2762,a1)
% 70.59/70.67 [292]P37(x2921,x2921,x2921)+~P26(x2922,a1,x2921)+~P1(a2)+~P23(a2,a1)
% 70.59/70.67 [321]~P36(x3211,x3211)+~P42(x3211,a5,x3212)+~P37(a3,a3,x3212)+P6(a5)
% 70.59/70.67 [360]P26(x3601,x3601,x3601)+~P26(x3602,x3601,x3602)+~P20(a4,x3601,x3602)+~P12(a2,x3602,a4)
% 70.59/70.67 [75]~P41(x751)+P36(x751,x751)+~P16(x753,x753)+~P45(x752)
% 70.59/70.67 [76]~P39(x761)+P35(x761,x761)+~P35(x762,x763)+~P13(x762)
% 70.59/70.67 [112]P24(x1121,x1121)+~P23(x1121,x1122)+~P21(x1123,x1123)+~P9(a1)
% 70.59/70.67 [115]~P14(x1153,x1153)+P14(x1151,x1151)+~P15(x1153,x1151)+~P25(x1152)
% 70.59/70.67 [177]~P2(x1771)+~P3(x1772)+P26(x1771,x1772,x1771)+~P23(x1773,x1771)
% 70.59/70.67 [193]~P5(x1931)+~P10(x1932,x1931)+P37(x1931,x1931,x1932)+~P23(x1933,x1933)
% 70.59/70.67 [207]~P28(x2073,x2071)+P32(x2071,x2071,x2071)+~P14(x2072,x2072)+~P36(x2072,x2073)
% 70.59/70.67 [220]~P44(x2201)+~P36(x2202,x2201)+P36(x2201,x2202)+~P26(x2203,x2201,x2202)
% 70.59/70.67 [285]~P3(x2851)+~P37(x2852,x2852,x2853)+P37(x2851,x2852,x2852)+~P4(x2853)
% 70.59/70.67 [287]~P19(x2872)+~P25(x2871)+P22(x2871,x2872,x2872)+~P22(x2873,x2871,x2873)
% 70.59/70.67 [302]~P15(x3023,x3021)+~P26(x3021,x3022,x3021)+P26(x3021,x3022,x3022)+~P3(x3023)
% 70.59/70.67 [307]~P23(x3071,x3071)+P30(x3071,x3071,x3071)+~P30(x3073,x3072,x3071)+~P39(x3072)
% 70.59/70.67 [309]~P41(x3093)+~P7(x3092,x3093)+~P42(x3093,x3091,x3091)+P42(x3091,x3092,x3093)
% 70.59/70.67 [312]P37(x3121,x3121,x3121)+~P23(x3122,x3123)+~P29(x3121,a2,a2)+~P10(a2,a2)
% 70.59/70.67 [317]~P14(x3172,x3171)+P31(x3171,x3171,x3171)+~P15(x3172,x3172)+~P31(x3173,x3173,x3172)
% 70.59/70.67 [318]~P21(x3183,x3182)+~P33(x3181,x3183,x3181)+P33(x3181,x3182,x3182)+~P16(x3181,x3183)
% 70.59/70.67 [320]~P45(x3201)+P24(x3201,x3201)+~P32(x3202,x3201,x3201)+~P32(a2,a2,x3203)
% 70.59/70.67 [325]~P20(x3253,x3252,x3252)+P16(x3251,x3251)+~P23(x3252,x3251)+~P12(x3252,x3251,x3253)
% 70.59/70.67 [343]~P8(x3431,x3432,x3432)+P8(x3431,x3431,x3431)+~P45(x3432)+~P30(x3432,x3433,a5)
% 70.59/70.67 [344]~P5(x3441)+P38(x3441,x3441,x3441)+~P38(x3442,x3442,x3443)+~P26(x3443,a1,x3442)
% 70.59/70.67 [349]~P10(x3491,x3492)+~P20(x3492,a4,x3492)+P20(x3491,a3,x3492)+~P12(a3,x3493,a3)
% 70.59/70.67 [352]~P23(x3521,x3522)+~P30(x3521,x3522,x3521)+P30(x3521,x3522,x3522)+~P26(x3523,x3522,x3523)
% 70.59/70.67 [354]~P29(x3543,x3542,x3541)+~P42(x3541,x3543,x3541)+P42(x3541,x3541,x3541)+~P16(x3542,x3543)
% 70.59/70.67 [355]~P8(x3553,x3552,x3552)+P32(x3551,x3551,x3551)+~P28(x3551,x3552)+~P29(x3552,x3553,x3551)
% 70.59/70.67 [361]~P29(x3611,x3611,x3613)+~P38(x3612,x3613,x3611)+P38(x3611,x3612,x3611)+~P26(x3612,x3611,x3613)
% 70.59/70.67 [88]~P27(x881)+P40(x881)+~P23(x882,x881)+~P36(x883,x884)
% 70.59/70.67 [217]~P12(x2172,x2171,x2174)+P15(x2171,x2172)+~P23(x2174,x2171)+~P2(x2173)
% 70.59/70.67 [218]~P7(x2183,x2182)+P7(x2181,x2182)+~P20(x2184,x2182,x2181)+~P5(x2183)
% 70.59/70.67 [219]P16(x2191,x2191)+~P12(x2194,x2192,x2191)+~P23(x2193,x2193)+~P45(x2192)
% 70.59/70.67 [282]P29(x2821,x2822,x2821)+~P29(x2822,x2824,x2821)+~P3(x2823)+~P1(a2)
% 70.59/70.67 [286]~P29(x2862,x2864,x2861)+P8(x2861,x2861,x2862)+~P19(x2863)+~P19(x2864)
% 70.59/70.67 [303]~P4(x3031)+P26(x3031,x3031,x3031)+~P12(x3034,x3033,x3034)+~P10(x3032,x3033)
% 70.59/70.67 [305]P29(x3051,x3051,x3051)+~P26(x3053,x3054,x3051)+~P11(x3053,x3053)+~P3(x3052)
% 70.59/70.67 [308]~P45(x3082)+P8(x3081,x3082,x3081)+~P30(x3084,x3082,x3083)+~P11(x3081,x3083)
% 70.59/70.67 [311]~P13(x3111)+P32(x3111,x3111,x3111)+~P11(x3111,x3112)+~P32(x3113,x3114,x3113)
% 70.59/70.67 [322]~P44(x3221)+~P38(x3223,x3221,x3223)+P48(x3221,x3222)+~P12(x3223,x3224,x3222)
% 70.59/70.67 [345]~P19(x3452)+P42(x3451,x3451,x3452)+~P42(x3452,x3453,x3453)+~P22(x3454,a2,x3451)
% 70.59/70.67 [353]~P29(x3531,x3533,x3534)+~P30(x3531,x3532,x3531)+P30(x3531,x3532,x3532)+~P15(x3533,x3534)
% 70.59/70.67 [304]P29(x3041,x3041,x3041)+~P20(x3045,x3043,x3041)+~P3(x3042)+~P10(x3043,x3044)
% 70.59/70.67 [306]P29(x3061,x3061,x3061)+~P26(x3063,x3061,x3065)+~P5(x3062)+~P10(x3063,x3064)
% 70.59/70.67 [316]P8(x3161,x3161,x3162)+~P10(x3163,x3162)+~P8(x3162,x3165,x3164)+~P7(x3161,x3164)
% 70.59/70.67 [358]P35(x3581,x3582)+~P38(x3583,x3582,x3581)+~P8(x3584,x3584,x3581)+~P22(x3583,x3585,x3583)
% 70.59/70.67 [301]~P15(a5,a4)+~P16(a5,a2)+P30(a3,a4,a2)+~P39(a5)+~P20(a1,a3,a4)
% 70.59/70.67 [351]P25(a3)+~P5(a4)+~P20(a2,a3,a5)+~P26(a5,a3,a5)+~P37(a4,a3,a1)
% 70.59/70.67 [259]~P2(x2591)+P20(a4,a3,a4)+~P2(a5)+~P4(a5)+~P12(a3,a5,a4)
% 70.59/70.67 [298]~P1(x2981)+~P11(a4,x2981)+~P26(a4,a1,x2981)+P29(a1,a1,x2981)+~P2(a1)
% 70.59/70.67 [313]~P26(a4,x3131,x3131)+~P23(a2,x3131)+P30(a2,a4,a3)+~P2(a5)+~P7(a4,a3)
% 70.59/70.67 [347]~P27(x3471)+~P38(x3471,a1,x3471)+P31(x3471,a1,a5)+~P14(a2,a5)+~P30(a1,a2,a4)
% 70.59/70.67 [348]~P22(a3,x3481,x3481)+~P38(x3481,a5,x3481)+P42(a3,a3,a5)+~P19(a2)+~P7(a3,a3)
% 70.59/70.67 [192]~P23(x1921,x1922)+P20(x1921,x1922,a4)+~P10(x1922,a1)+~P1(a1)+~P2(a4)
% 70.59/70.67 [200]~P5(x2002)+P30(x2001,x2001,x2001)+~P4(x2002)+~P7(x2001,a3)+~P16(a3,x2002)
% 70.59/70.67 [221]~P5(x2211)+P36(x2211,x2211)+~P36(x2212,x2211)+~P12(x2212,a1,x2212)+~P41(a1)
% 70.59/70.67 [73]~P6(x731)+~P46(x732)+P46(x731)+~P48(x731,x733)+~P17(x732)
% 70.59/70.67 [314]~P1(x3141)+~P5(x3141)+~P12(x3143,x3143,x3143)+P26(x3141,x3141,x3141)+~P23(x3142,x3143)
% 70.59/70.67 [323]~P22(x3231,x3233,x3231)+P22(x3231,x3231,x3231)+~P7(x3232,x3233)+~P11(x3233,a3)+~P16(a3,a3)
% 70.59/70.67 [346]P30(x3461,x3461,x3462)+~P30(x3461,x3463,x3461)+~P37(a4,x3461,x3463)+~P1(a5)+~P45(a4)
% 70.59/70.67 [183]~P41(x1831)+P22(x1831,x1831,x1831)+~P1(x1832)+~P10(x1834,x1833)+~P44(x1833)
% 70.59/70.67 [204]~P3(x2041)+~P10(x2042,x2042)+P37(x2041,x2042,x2041)+~P23(x2044,x2041)+~P2(x2043)
% 70.59/70.67 [315]~P44(x3151)+~P8(x3153,x3154,x3153)+P8(x3151,x3151,x3151)+~P19(x3152)+~P15(x3153,x3154)
% 70.59/70.67 [350]~P4(x3502)+~P39(x3502)+~P38(x3502,x3502,x3502)+P38(x3501,x3502,x3501)+~P12(x3503,x3504,x3501)
% 70.59/70.67 [356]~P12(x3563,x3563,x3562)+~P12(x3561,x3564,x3564)+P22(x3561,x3562,x3561)+~P16(x3564,x3561)+~P44(x3563)
% 70.59/70.67 [362]~P26(x3622,x3624,x3624)+~P37(x3623,x3622,x3624)+P37(x3621,x3621,x3621)+~P20(x3621,x3624,x3622)+~P23(x3622,x3623)
% 70.59/70.67 [299]~P32(x2995,x2995,x2992)+P24(x2991,x2992)+~P28(x2991,x2993)+~P35(x2994,x2993)+~P24(x2995,x2992)
% 70.59/70.67 %EqnAxiom
% 70.59/70.67
% 70.59/70.67 %-------------------------------------------
% 70.74/70.74 cnf(364,plain,
% 70.74/70.74 (~P18(a1,x3641)),
% 70.74/70.74 inference(rename_variables,[],[39])).
% 70.74/70.74 cnf(366,plain,
% 70.74/70.74 (P26(x3661,x3661,a1)),
% 70.74/70.74 inference(scs_inference,[],[39,38,47,232])).
% 70.74/70.74 cnf(367,plain,
% 70.74/70.74 (P12(x3671,a1,x3672)),
% 70.74/70.74 inference(rename_variables,[],[38])).
% 70.74/70.74 cnf(370,plain,
% 70.74/70.74 (P23(a2,x3701)),
% 70.74/70.74 inference(rename_variables,[],[28])).
% 70.74/70.74 cnf(376,plain,
% 70.74/70.74 (P29(a5,a5,a5)),
% 70.74/70.74 inference(scs_inference,[],[39,38,28,1,2,7,8,16,47,232,150,109,123,152])).
% 70.74/70.74 cnf(379,plain,
% 70.74/70.74 (P12(x3791,a1,x3792)),
% 70.74/70.74 inference(rename_variables,[],[38])).
% 70.74/70.74 cnf(385,plain,
% 70.74/70.74 (P29(a3,x3851,a3)),
% 70.74/70.74 inference(scs_inference,[],[39,38,367,379,28,37,1,2,5,7,8,16,47,232,150,109,123,152,256,328,334])).
% 70.74/70.74 cnf(389,plain,
% 70.74/70.74 (P23(a2,x3891)),
% 70.74/70.74 inference(rename_variables,[],[28])).
% 70.74/70.74 cnf(391,plain,
% 70.74/70.74 (P26(a3,x3911,a3)),
% 70.74/70.74 inference(scs_inference,[],[39,38,367,379,28,370,389,37,1,2,5,7,8,16,47,232,150,109,123,152,256,328,334,292,166])).
% 70.74/70.74 cnf(393,plain,
% 70.74/70.74 (P39(x3931)),
% 70.74/70.74 inference(scs_inference,[],[39,38,367,379,27,28,370,389,37,1,2,5,7,8,16,47,232,150,109,123,152,256,328,334,292,166,202])).
% 70.74/70.74 cnf(402,plain,
% 70.74/70.74 (P41(a3)),
% 70.74/70.74 inference(scs_inference,[],[39,364,3,38,367,379,27,28,370,389,37,1,2,5,7,8,16,47,232,150,109,123,152,256,328,334,292,166,202,225,55,253,44])).
% 70.74/70.74 cnf(404,plain,
% 70.74/70.74 (P30(x4041,x4041,x4041)),
% 70.74/70.74 inference(scs_inference,[],[39,364,3,38,367,379,27,28,370,389,37,1,2,5,7,8,16,47,232,150,109,123,152,256,328,334,292,166,202,225,55,253,44,337])).
% 70.74/70.74 cnf(414,plain,
% 70.74/70.74 (P44(a1)+~P45(a3)),
% 70.74/70.74 inference(scs_inference,[],[1,41])).
% 70.74/70.74 cnf(415,plain,
% 70.74/70.74 (P44(a1)+~P45(a1)),
% 70.74/70.74 inference(scs_inference,[],[393,42])).
% 70.74/70.74 cnf(417,plain,
% 70.74/70.74 (P6(a4)+~P27(a5)+~P36(a5,a2)),
% 70.74/70.74 inference(scs_inference,[],[23,71])).
% 70.74/70.74 cnf(418,plain,
% 70.74/70.74 (P20(a5,a5,a5)),
% 70.74/70.74 inference(scs_inference,[],[3,79])).
% 70.74/70.74 cnf(419,plain,
% 70.74/70.74 (P20(a4,a4,a4)),
% 70.74/70.74 inference(scs_inference,[],[6,81])).
% 70.74/70.74 cnf(423,plain,
% 70.74/70.74 (~P1(x4231)+P37(x4231,a2,a2)),
% 70.74/70.74 inference(scs_inference,[],[2,109])).
% 70.74/70.74 cnf(424,plain,
% 70.74/70.74 (P29(x4241,x4241,x4241)+~P1(x4241)),
% 70.74/70.74 inference(scs_inference,[],[2,124])).
% 70.74/70.74 cnf(426,plain,
% 70.74/70.74 (P29(x4261,x4261,x4261)+~P5(x4261)),
% 70.74/70.74 inference(scs_inference,[],[6,7,130])).
% 70.74/70.74 cnf(431,plain,
% 70.74/70.74 (P26(x4311,x4312,x4311)+~P3(x4311)+~P23(a2,x4312)),
% 70.74/70.74 inference(scs_inference,[],[2,166])).
% 70.74/70.74 cnf(432,plain,
% 70.74/70.74 (~P5(x4321)+~P16(x4321,x4322)+P38(x4322,a4,x4321)),
% 70.74/70.74 inference(scs_inference,[],[6,167])).
% 70.74/70.74 cnf(433,plain,
% 70.74/70.74 (~P29(a2,x4331,x4332)+P25(a5)),
% 70.74/70.74 inference(scs_inference,[],[3,393,179])).
% 70.74/70.74 cnf(434,plain,
% 70.74/70.74 (P22(x4341,x4341,x4341)+~P44(x4342)+~P41(x4341)+~P10(x4343,x4342)),
% 70.74/70.74 inference(scs_inference,[],[2,183])).
% 70.74/70.74 cnf(435,plain,
% 70.74/70.74 (P14(a1,a4)+~P44(a1)+~P8(a3,a4,a3)),
% 70.74/70.74 inference(scs_inference,[],[4,184])).
% 70.74/70.74 cnf(436,plain,
% 70.74/70.74 (P37(x4361,x4362,x4361)+~P3(x4361)+~P10(x4362,x4362)+~P23(x4363,x4361)),
% 70.74/70.74 inference(scs_inference,[],[4,204])).
% 70.74/70.74 cnf(437,plain,
% 70.74/70.74 (P15(x4371,x4372)+~P23(x4373,x4371)+~P12(x4372,x4371,x4373)),
% 70.74/70.74 inference(scs_inference,[],[4,217])).
% 70.74/70.74 cnf(440,plain,
% 70.74/70.74 (P30(a5,x4401,x4402)+~P29(x4401,x4402,a5)),
% 70.74/70.74 inference(scs_inference,[],[3,253])).
% 70.74/70.74 cnf(441,plain,
% 70.74/70.74 (P29(x4411,x4411,x4411)+~P3(x4411)),
% 70.74/70.74 inference(scs_inference,[],[38,256])).
% 70.74/70.74 cnf(443,plain,
% 70.74/70.74 (P20(x4431,x4432,x4432)+~P12(x4432,x4432,x4431)),
% 70.74/70.74 inference(scs_inference,[],[5,262])).
% 70.74/70.74 cnf(444,plain,
% 70.74/70.74 (P37(x4441,x4441,x4442)+~P20(x4441,x4442,x4442)),
% 70.74/70.74 inference(scs_inference,[],[4,265])).
% 70.74/70.74 cnf(447,plain,
% 70.74/70.74 (P29(x4471,x4472,x4471)+~P29(x4472,x4473,x4471)),
% 70.74/70.74 inference(scs_inference,[],[2,5,282])).
% 70.74/70.74 cnf(449,plain,
% 70.74/70.74 (P37(x4491,x4491,x4491)+~P26(x4492,a1,x4491)),
% 70.74/70.74 inference(scs_inference,[],[2,28,292])).
% 70.74/70.74 cnf(453,plain,
% 70.74/70.74 (~P11(x4531,x4531)+P29(x4532,x4532,x4532)+~P26(x4531,x4533,x4532)),
% 70.74/70.74 inference(scs_inference,[],[5,305])).
% 70.74/70.74 cnf(456,plain,
% 70.74/70.74 (~P10(x4561,x4562)+~P20(x4562,a4,x4562)+P20(x4561,a3,x4562)),
% 70.74/70.74 inference(scs_inference,[],[38,349])).
% 70.74/70.74 cnf(457,plain,
% 70.74/70.74 (P37(a3,a3,a3)),
% 70.74/70.74 inference(scs_inference,[],[391,449])).
% 70.74/70.74 cnf(460,plain,
% 70.74/70.74 (P29(a2,a2,a2)),
% 70.74/70.74 inference(scs_inference,[],[2,391,449,424])).
% 70.74/70.74 cnf(462,plain,
% 70.74/70.74 (P29(a4,a4,a4)),
% 70.74/70.74 inference(scs_inference,[],[2,391,6,449,424,441])).
% 70.74/70.74 cnf(464,plain,
% 70.74/70.74 (P20(a5,a2,a2)),
% 70.74/70.74 inference(scs_inference,[],[2,391,6,35,449,424,441,443])).
% 70.74/70.74 cnf(466,plain,
% 70.74/70.74 (P26(a5,a5,a2)),
% 70.74/70.74 inference(scs_inference,[],[2,391,6,35,449,424,441,443,232])).
% 70.74/70.74 cnf(471,plain,
% 70.74/70.74 (P15(a2,a5)),
% 70.74/70.74 inference(scs_inference,[],[39,2,391,6,26,32,35,449,424,441,443,232,47,437])).
% 70.74/70.74 cnf(473,plain,
% 70.74/70.74 (P29(a1,a1,a1)),
% 70.74/70.74 inference(scs_inference,[],[39,2,366,391,6,19,26,32,35,449,424,441,443,232,47,437,453])).
% 70.74/70.74 cnf(480,plain,
% 70.74/70.74 (P29(a2,a2,a5)),
% 70.74/70.74 inference(scs_inference,[],[39,2,366,385,391,6,17,19,26,32,35,38,7,449,424,441,443,232,47,437,453,334,152])).
% 70.74/70.74 cnf(485,plain,
% 70.74/70.74 (P30(a5,a2,a2)),
% 70.74/70.74 inference(scs_inference,[],[39,5,2,366,385,391,6,15,17,19,26,32,35,38,28,7,449,424,441,443,232,47,437,453,334,152,436,440])).
% 70.74/70.74 cnf(499,plain,
% 70.74/70.74 (P19(x4991)+~P1(x4991)),
% 70.74/70.74 inference(scs_inference,[],[471,63])).
% 70.74/70.74 cnf(500,plain,
% 70.74/70.74 (P19(a2)),
% 70.74/70.74 inference(scs_inference,[],[2,499])).
% 70.74/70.74 cnf(502,plain,
% 70.74/70.74 (P20(x5021,a1,a1)),
% 70.74/70.74 inference(scs_inference,[],[2,38,499,443])).
% 70.74/70.74 cnf(503,plain,
% 70.74/70.74 (P12(x5031,a1,x5032)),
% 70.74/70.74 inference(rename_variables,[],[38])).
% 70.74/70.74 cnf(508,plain,
% 70.74/70.74 (~P18(a1,x5081)),
% 70.74/70.74 inference(rename_variables,[],[39])).
% 70.74/70.74 cnf(513,plain,
% 70.74/70.74 (P12(x5131,a1,x5132)),
% 70.74/70.74 inference(rename_variables,[],[38])).
% 70.74/70.74 cnf(514,plain,
% 70.74/70.74 (P12(a3,x5141,a3)),
% 70.74/70.74 inference(rename_variables,[],[37])).
% 70.74/70.74 cnf(516,plain,
% 70.74/70.74 (P15(a1,x5161)),
% 70.74/70.74 inference(scs_inference,[],[39,2,11,419,37,38,503,513,28,499,443,444,47,456,328,437])).
% 70.74/70.74 cnf(518,plain,
% 70.74/70.74 (P23(a2,x5181)),
% 70.74/70.74 inference(rename_variables,[],[28])).
% 70.74/70.74 cnf(522,plain,
% 70.74/70.74 (P29(x5221,x5222,a3)),
% 70.74/70.74 inference(scs_inference,[],[39,418,7,2,11,419,37,514,385,38,503,513,28,499,443,444,47,456,328,437,263,334])).
% 70.74/70.74 cnf(531,plain,
% 70.74/70.74 (P38(a4,a4,a4)),
% 70.74/70.74 inference(scs_inference,[],[39,418,8,27,7,5,2,11,18,419,37,514,385,38,503,513,28,518,499,443,444,47,456,328,437,263,334,152,436,231])).
% 70.74/70.74 cnf(533,plain,
% 70.74/70.74 (P14(x5331,x5331)+~P25(x5331)),
% 70.74/70.74 inference(scs_inference,[],[39,418,8,27,7,5,2,11,18,419,37,514,385,38,503,513,28,518,499,443,444,47,456,328,437,263,334,152,436,231,52])).
% 70.74/70.74 cnf(541,plain,
% 70.74/70.74 (P16(x5411,a2)+~P16(a2,a2)+~P45(x5411)),
% 70.74/70.74 inference(scs_inference,[],[39,508,4,418,8,27,7,5,2,11,18,20,419,37,514,385,38,503,513,28,518,499,443,444,47,456,328,437,263,334,152,436,231,111])).
% 70.74/70.74 cnf(543,plain,
% 70.74/70.74 (P8(x5431,x5431,x5432)+~P19(x5433)+~P29(x5432,x5433,x5431)),
% 70.74/70.74 inference(scs_inference,[],[500,286])).
% 70.74/70.74 cnf(546,plain,
% 70.74/70.74 (P25(a5)),
% 70.74/70.74 inference(scs_inference,[],[460,433])).
% 70.74/70.74 cnf(548,plain,
% 70.74/70.74 (P19(a1)),
% 70.74/70.74 inference(scs_inference,[],[1,499])).
% 70.74/70.74 cnf(553,plain,
% 70.74/70.74 (P37(x5531,x5531,a1)),
% 70.74/70.74 inference(scs_inference,[],[39,1,502,499,47,444])).
% 70.74/70.74 cnf(559,plain,
% 70.74/70.74 (P41(a4)),
% 70.74/70.74 inference(scs_inference,[],[39,393,460,6,1,502,500,28,499,47,444,543,431,44])).
% 70.74/70.74 cnf(562,plain,
% 70.74/70.74 (P29(a5,a5,a2)),
% 70.74/70.74 inference(scs_inference,[],[39,8,393,460,6,1,502,500,16,28,499,47,444,543,431,44,152])).
% 70.74/70.74 cnf(564,plain,
% 70.74/70.74 (P29(a2,x5641,a2)),
% 70.74/70.74 inference(scs_inference,[],[39,8,393,460,480,6,1,35,502,500,16,28,499,47,444,543,431,44,152,334])).
% 70.74/70.74 cnf(566,plain,
% 70.74/70.74 (P16(a2,a2)),
% 70.74/70.74 inference(scs_inference,[],[39,8,393,460,464,480,6,1,35,502,500,16,28,499,47,444,543,431,44,152,334,325])).
% 70.74/70.74 cnf(567,plain,
% 70.74/70.74 (P23(a2,x5671)),
% 70.74/70.74 inference(rename_variables,[],[28])).
% 70.74/70.74 cnf(573,plain,
% 70.74/70.74 (P8(a4,a4,a4)),
% 70.74/70.74 inference(scs_inference,[],[39,8,393,460,464,480,6,1,35,27,502,500,16,28,567,499,47,444,543,431,44,152,334,325,436,87])).
% 70.74/70.74 cnf(574,plain,
% 70.74/70.74 (P38(a1,a1,a1)),
% 70.74/70.74 inference(scs_inference,[],[39,8,393,460,464,480,6,1,35,27,502,500,16,28,567,499,47,444,543,431,44,152,334,325,436,87,231])).
% 70.74/70.74 cnf(580,plain,
% 70.74/70.74 (P42(a2,a2,a2)),
% 70.74/70.74 inference(scs_inference,[],[39,4,471,8,393,460,464,480,6,1,35,27,404,502,500,16,28,567,499,47,444,543,431,44,152,334,325,436,87,231,148,151,297])).
% 70.74/70.74 cnf(585,plain,
% 70.74/70.74 (~P7(x5851,x5852)+P31(a1,x5851,x5852)),
% 70.74/70.74 inference(scs_inference,[],[39,4,471,8,393,460,464,480,6,1,35,27,404,502,500,16,28,567,499,47,444,543,431,44,152,334,325,436,87,231,148,151,297,181,291])).
% 70.74/70.74 cnf(587,plain,
% 70.74/70.74 (~P45(x5871)+P16(x5871,a2)),
% 70.74/70.74 inference(scs_inference,[],[39,4,471,8,393,460,464,480,6,1,35,27,404,502,500,16,28,567,499,47,444,543,431,44,152,334,325,436,87,231,148,151,297,181,291,541])).
% 70.74/70.74 cnf(590,plain,
% 70.74/70.74 (P42(x5901,x5901,x5901)+~P31(a2,x5901,x5902)),
% 70.74/70.74 inference(scs_inference,[],[39,4,471,8,393,460,464,480,6,29,1,35,27,404,502,500,16,28,567,499,47,444,543,431,44,152,334,325,436,87,231,148,151,297,181,291,541,437,340])).
% 70.74/70.74 cnf(594,plain,
% 70.74/70.74 (P22(x5941,a5,a5)+~P30(x5941,a5,a5)),
% 70.74/70.74 inference(scs_inference,[],[546,228])).
% 70.74/70.74 cnf(603,plain,
% 70.74/70.74 (P8(a5,a5,a2)),
% 70.74/70.74 inference(scs_inference,[],[39,546,480,404,500,533,594,47,543])).
% 70.74/70.74 cnf(605,plain,
% 70.74/70.74 (P29(a1,x6051,a1)),
% 70.74/70.74 inference(scs_inference,[],[39,546,38,480,473,404,500,533,594,47,543,334])).
% 70.74/70.74 cnf(631,plain,
% 70.74/70.74 (P8(a3,a3,x6311)),
% 70.74/70.74 inference(scs_inference,[],[39,522,548,47,543])).
% 70.74/70.74 cnf(634,plain,
% 70.74/70.74 (P29(a1,x6341,a2)),
% 70.74/70.74 inference(scs_inference,[],[39,38,564,522,548,47,543,334])).
% 70.74/70.74 cnf(655,plain,
% 70.74/70.74 (P29(a3,x6551,a2)),
% 70.74/70.74 inference(scs_inference,[],[39,605,34,522,548,47,543,334])).
% 70.74/70.74 cnf(677,plain,
% 70.74/70.74 (P8(a2,a2,a1)),
% 70.74/70.74 inference(scs_inference,[],[39,634,500,47,543])).
% 70.74/70.74 cnf(680,plain,
% 70.74/70.74 (P29(a2,x6801,a4)),
% 70.74/70.74 inference(scs_inference,[],[39,634,36,522,500,47,543,334])).
% 70.74/70.74 cnf(697,plain,
% 70.74/70.74 (~P18(a1,x6971)),
% 70.74/70.74 inference(rename_variables,[],[39])).
% 70.74/70.74 cnf(699,plain,
% 70.74/70.74 (P8(a2,a2,a3)),
% 70.74/70.74 inference(scs_inference,[],[39,655,548,47,543])).
% 70.74/70.74 cnf(712,plain,
% 70.74/70.74 (~P29(a1,a5,a4)+P29(a5,x7121,a1)),
% 70.74/70.74 inference(scs_inference,[],[39,697,3,35,29,655,502,548,47,543,283,196,55,437,334])).
% 70.74/70.74 cnf(719,plain,
% 70.74/70.74 (P8(a4,a4,a2)),
% 70.74/70.74 inference(scs_inference,[],[39,680,500,47,543])).
% 70.74/70.74 cnf(755,plain,
% 70.74/70.74 (~P18(a1,x7551)),
% 70.74/70.74 inference(rename_variables,[],[39])).
% 70.74/70.74 cnf(769,plain,
% 70.74/70.74 (P22(a4,a4,a4)+~P44(a2)),
% 70.74/70.74 inference(scs_inference,[],[39,755,4,35,13,502,562,559,47,543,283,196,55,437,434])).
% 70.74/70.74 cnf(805,plain,
% 70.74/70.74 (~P18(a1,x8051)),
% 70.74/70.74 inference(rename_variables,[],[39])).
% 70.74/70.74 cnf(817,plain,
% 70.74/70.74 (P16(x8171,a5)+~P16(a5,a5)+~P45(x8171)),
% 70.74/70.74 inference(scs_inference,[],[39,805,3,35,19,502,47,111])).
% 70.74/70.74 cnf(870,plain,
% 70.74/70.74 (P29(a4,a4,a5)),
% 70.74/70.74 inference(scs_inference,[],[39,7,18,47,152])).
% 70.74/70.74 cnf(872,plain,
% 70.74/70.74 (P30(a5,a4,a4)),
% 70.74/70.74 inference(scs_inference,[],[39,7,18,47,152,440])).
% 70.74/70.74 cnf(1015,plain,
% 70.74/70.74 (~P18(a1,x10151)),
% 70.74/70.74 inference(rename_variables,[],[39])).
% 70.74/70.74 cnf(1027,plain,
% 70.74/70.74 (P8(a3,a2,a3)+~P45(a2)),
% 70.74/70.74 inference(scs_inference,[],[39,1015,4,485,35,502,21,47,196,283,55,437,308])).
% 70.74/70.74 cnf(1109,plain,
% 70.74/70.74 (~P18(a1,x11091)),
% 70.74/70.74 inference(rename_variables,[],[39])).
% 70.74/70.74 cnf(1121,plain,
% 70.74/70.74 (P8(a2,a3,a2)+~P45(a3)),
% 70.74/70.74 inference(scs_inference,[],[39,1109,3,404,35,502,22,47,196,283,55,437,308])).
% 70.74/70.74 cnf(1936,plain,
% 70.74/70.74 (P26(a1,a5,a5)),
% 70.74/70.74 inference(scs_inference,[],[23,38,53,254])).
% 70.74/70.74 cnf(2736,plain,
% 70.74/70.74 (~P45(x27361)+P16(a3,a2)),
% 70.74/70.74 inference(scs_inference,[],[13,587,62])).
% 70.74/70.74 cnf(3443,plain,
% 70.74/70.74 (P16(a3,a2)),
% 70.74/70.74 inference(scs_inference,[],[28,2736,54])).
% 70.74/70.74 cnf(4361,plain,
% 70.74/70.74 (P7(a5,a5)),
% 70.74/70.74 inference(scs_inference,[],[16,65,58])).
% 70.74/70.74 cnf(4365,plain,
% 70.74/70.74 (P31(a1,a5,a5)),
% 70.74/70.74 inference(scs_inference,[],[39,574,4361,47,291])).
% 70.74/70.74 cnf(4804,plain,
% 70.74/70.74 (P24(a4,a4)+~P22(a4,x48041,a4)),
% 70.74/70.74 inference(scs_inference,[],[531,573,67,358])).
% 70.74/70.74 cnf(5272,plain,
% 70.74/70.74 (P38(a2,a2,a2)),
% 70.74/70.74 inference(scs_inference,[],[4,15,97,295])).
% 70.74/70.74 cnf(5977,plain,
% 70.74/70.74 (P38(a5,a5,a5)),
% 70.74/70.74 inference(scs_inference,[],[7,98,244])).
% 70.74/70.74 cnf(6447,plain,
% 70.74/70.74 (P7(a1,a1)),
% 70.74/70.74 inference(scs_inference,[],[1,100,190])).
% 70.74/70.74 cnf(6451,plain,
% 70.74/70.74 (P8(a1,a1,a2)),
% 70.74/70.74 inference(scs_inference,[],[39,677,13,6447,47,316])).
% 70.74/70.74 cnf(6916,plain,
% 70.74/70.74 (P32(a2,a2,a2)),
% 70.74/70.74 inference(scs_inference,[],[500,103,249])).
% 70.74/70.74 cnf(7167,plain,
% 70.74/70.74 (P32(a5,a5,a5)),
% 70.74/70.74 inference(scs_inference,[],[546,104,249])).
% 70.74/70.74 cnf(7408,plain,
% 70.74/70.74 (P31(a5,a5,a5)),
% 70.74/70.74 inference(scs_inference,[],[546,404,105,339])).
% 70.74/70.74 cnf(8169,plain,
% 70.74/70.74 (P32(a3,a3,a3)),
% 70.74/70.74 inference(scs_inference,[],[402,6916,107,341])).
% 70.74/70.74 cnf(8417,plain,
% 70.74/70.74 (P22(a1,a1,a1)),
% 70.74/70.74 inference(scs_inference,[],[605,172,105])).
% 70.74/70.74 cnf(8670,plain,
% 70.74/70.74 (P31(a1,a1,a1)),
% 70.74/70.74 inference(scs_inference,[],[39,6447,574,47,291])).
% 70.74/70.74 cnf(9142,plain,
% 70.74/70.74 (P7(a2,a2)),
% 70.74/70.74 inference(scs_inference,[],[1,423,190])).
% 70.74/70.74 cnf(9634,plain,
% 70.74/70.74 (~P5(x96341)+P38(x96341,a5,a5)),
% 70.74/70.74 inference(scs_inference,[],[7,426,268])).
% 70.74/70.74 cnf(11319,plain,
% 70.74/70.74 (~P44(a2)+P24(a4,a4)),
% 70.74/70.74 inference(scs_inference,[],[769,4804])).
% 70.74/70.74 cnf(11543,plain,
% 70.74/70.74 (P24(a4,a4)+~P45(a2)),
% 70.74/70.74 inference(scs_inference,[],[5272,11319,175])).
% 70.74/70.74 cnf(11777,plain,
% 70.74/70.74 (P24(a4,a4)),
% 70.74/70.74 inference(scs_inference,[],[28,11543,54])).
% 70.74/70.74 cnf(11861,plain,
% 70.74/70.74 (P38(x118611,a2,x118611)),
% 70.74/70.74 inference(scs_inference,[],[39,3,7167,38,5272,393,8,47,196,350])).
% 70.74/70.74 cnf(11880,plain,
% 70.74/70.74 (P38(x118801,a5,x118801)),
% 70.74/70.74 inference(scs_inference,[],[39,3,7167,38,5977,7,393,47,196,350])).
% 70.74/70.74 cnf(13199,plain,
% 70.74/70.74 (P31(a1,a2,a2)),
% 70.74/70.74 inference(scs_inference,[],[39,9142,574,47,291])).
% 70.74/70.74 cnf(13212,plain,
% 70.74/70.74 (P31(a3,a3,a2)+~P45(a2)),
% 70.74/70.74 inference(scs_inference,[],[402,1027,272])).
% 70.74/70.74 cnf(13455,plain,
% 70.74/70.74 (P22(a2,a2,a3)+~P45(a3)),
% 70.74/70.74 inference(scs_inference,[],[402,1121,271])).
% 70.74/70.74 cnf(14435,plain,
% 70.74/70.74 (P38(a1,a5,a5)),
% 70.74/70.74 inference(scs_inference,[],[23,9634,53])).
% 70.74/70.74 cnf(16242,plain,
% 70.74/70.74 (P29(a1,x162421,x162422)),
% 70.74/70.74 inference(scs_inference,[],[39,38,522,47,334])).
% 70.74/70.74 cnf(16248,plain,
% 70.74/70.74 (P30(a5,a1,x162481)),
% 70.74/70.74 inference(scs_inference,[],[39,3,7167,38,522,47,334,196,440])).
% 70.74/70.74 cnf(16250,plain,
% 70.74/70.74 (P30(a1,x162501,x162501)+~P5(x162502)),
% 70.74/70.74 inference(scs_inference,[],[39,3,7167,38,522,47,334,196,440,258])).
% 70.74/70.74 cnf(16267,plain,
% 70.74/70.74 (P29(a5,x162671,a1)),
% 70.74/70.74 inference(scs_inference,[],[16242,712])).
% 70.74/70.74 cnf(16271,plain,
% 70.74/70.74 (P8(x162711,x162711,a1)),
% 70.74/70.74 inference(scs_inference,[],[39,16242,548,47,543])).
% 70.74/70.74 cnf(16296,plain,
% 70.74/70.74 (P8(a1,a1,a5)),
% 70.74/70.74 inference(scs_inference,[],[39,16267,500,47,543])).
% 70.74/70.74 cnf(18288,plain,
% 70.74/70.74 (P42(a3,a3,a2)+~P45(a3)),
% 70.74/70.74 inference(scs_inference,[],[580,500,13455,345])).
% 70.74/70.74 cnf(18649,plain,
% 70.74/70.74 (P8(a1,a1,a4)),
% 70.74/70.74 inference(scs_inference,[],[11,39,3,7167,16271,6447,47,196,316])).
% 70.74/70.74 cnf(18673,plain,
% 70.74/70.74 (P8(a2,a2,a4)),
% 70.74/70.74 inference(scs_inference,[],[11,39,3,7167,719,9142,47,196,316])).
% 70.74/70.74 cnf(19291,plain,
% 70.74/70.74 (P30(a1,x192911,x192911)),
% 70.74/70.74 inference(scs_inference,[],[23,16250,53])).
% 70.74/70.74 cnf(20961,plain,
% 70.74/70.74 (P32(a2,a3,a3)+~P45(a3)),
% 70.74/70.74 inference(scs_inference,[],[8169,18288,341])).
% 70.74/70.74 cnf(22312,plain,
% 70.74/70.74 (P8(a2,a2,a5)),
% 70.74/70.74 inference(scs_inference,[],[14,39,3,7167,603,9142,47,196,316])).
% 70.74/70.74 cnf(24408,plain,
% 70.74/70.74 (P42(a4,a4,a4)+~P7(a4,a2)),
% 70.74/70.74 inference(scs_inference,[],[120,590])).
% 70.74/70.74 cnf(25588,plain,
% 70.74/70.74 (P38(x255881,x255881,x255881)),
% 70.74/70.74 inference(scs_inference,[],[28,139,244])).
% 70.74/70.74 cnf(25590,plain,
% 70.74/70.74 (~P18(a1,x255901)),
% 70.74/70.74 inference(rename_variables,[],[39])).
% 70.74/70.74 cnf(25602,plain,
% 70.74/70.74 (~P44(x256021)+P48(x256021,x256022)),
% 70.74/70.74 inference(scs_inference,[],[39,25590,3,7167,38,35,502,25588,47,196,283,55,437,322])).
% 70.74/70.74 cnf(27088,plain,
% 70.74/70.74 (P36(a5,a1)),
% 70.74/70.74 inference(scs_inference,[],[516,19,144,209])).
% 70.74/70.74 cnf(27089,plain,
% 70.74/70.74 (P40(x270891)+~P27(x270891)+~P23(x270892,x270891)),
% 70.74/70.74 inference(scs_inference,[],[27088,88])).
% 70.74/70.74 cnf(27090,plain,
% 70.74/70.74 (P32(x270901,x270901,x270901)+~P27(x270901)),
% 70.74/70.74 inference(scs_inference,[],[27088,161])).
% 70.74/70.74 cnf(27306,plain,
% 70.74/70.74 (P32(x273061,x273061,x273061)),
% 70.74/70.74 inference(scs_inference,[],[16248,27090,173])).
% 70.74/70.74 cnf(29818,plain,
% 70.74/70.74 (P42(a4,x298181,a4)+~P7(x298181,a4)+~P7(a4,a2)),
% 70.74/70.74 inference(scs_inference,[],[559,24408,309])).
% 70.74/70.74 cnf(31092,plain,
% 70.74/70.74 (P27(a3)),
% 70.74/70.74 inference(scs_inference,[],[457,227,173])).
% 70.74/70.74 cnf(31097,plain,
% 70.74/70.74 (P40(a3)),
% 70.74/70.74 inference(scs_inference,[],[39,31092,28,47,27089])).
% 70.74/70.74 cnf(31114,plain,
% 70.74/70.74 (P46(x311141)+~P13(x311141)),
% 70.74/70.74 inference(scs_inference,[],[31097,45])).
% 70.74/70.74 cnf(31329,plain,
% 70.74/70.74 (P30(a1,x313291,a1)),
% 70.74/70.74 inference(scs_inference,[],[38,234,241])).
% 70.74/70.74 cnf(31853,plain,
% 70.74/70.74 (P7(a4,a4)),
% 70.74/70.74 inference(scs_inference,[],[29,239,190])).
% 70.74/70.74 cnf(31857,plain,
% 70.74/70.75 (P22(a3,a4,a3)),
% 70.74/70.75 inference(scs_inference,[],[39,402,31853,47,153])).
% 70.74/70.75 cnf(32123,plain,
% 70.74/70.75 (P35(a1,a2)),
% 70.74/70.75 inference(scs_inference,[],[16248,11861,8417,246,358])).
% 70.74/70.75 cnf(32387,plain,
% 70.74/70.75 (P31(a5,a1,a1)),
% 70.74/70.75 inference(scs_inference,[],[19291,16248,247,339])).
% 70.74/70.75 cnf(32650,plain,
% 70.74/70.75 (P42(a1,a1,a1)),
% 70.74/70.75 inference(scs_inference,[],[16248,32387,248,340])).
% 70.74/70.75 cnf(34048,plain,
% 70.74/70.75 (P31(a1,a4,a4)),
% 70.74/70.75 inference(scs_inference,[],[39,25588,31853,47,291])).
% 70.74/70.75 cnf(34073,plain,
% 70.74/70.75 (P42(a4,a4,a4)),
% 70.74/70.75 inference(scs_inference,[],[39,32650,34048,47,340])).
% 70.74/70.75 cnf(38423,plain,
% 70.74/70.75 (~P21(a5,a5)),
% 70.74/70.75 inference(scs_inference,[],[39,8670,516,70,201])).
% 70.74/70.75 cnf(38698,plain,
% 70.74/70.75 (P30(a5,a4,a5)),
% 70.74/70.75 inference(scs_inference,[],[6,7,122,241])).
% 70.74/70.75 cnf(38705,plain,
% 70.74/70.75 (P30(a4,a5,a5)+~P5(x387051)),
% 70.74/70.75 inference(scs_inference,[],[39,3,27306,38698,47,196,258])).
% 70.74/70.75 cnf(38974,plain,
% 70.74/70.75 (P30(a4,a5,a5)),
% 70.74/70.75 inference(scs_inference,[],[22,38705,53])).
% 70.74/70.75 cnf(38995,plain,
% 70.74/70.75 (~P18(a1,x389951)),
% 70.74/70.75 inference(rename_variables,[],[39])).
% 70.74/70.75 cnf(38998,plain,
% 70.74/70.75 (P32(x389981,x389981,x389981)),
% 70.74/70.75 inference(rename_variables,[],[27306])).
% 70.74/70.75 cnf(39013,plain,
% 70.74/70.75 (P24(x390131,a4)+~P28(x390131,a2)),
% 70.74/70.75 inference(scs_inference,[],[39,38995,3,27306,38998,34073,516,29,502,11777,32123,47,196,181,283,437,55,191,299])).
% 70.74/70.75 cnf(42935,plain,
% 70.74/70.75 (~P45(x429351)+~P45(a2)+P16(x429351,a5)),
% 70.74/70.75 inference(scs_inference,[],[35,28,817,219])).
% 70.74/70.75 cnf(43226,plain,
% 70.74/70.75 (P16(a2,a5)+~P45(a2)),
% 70.74/70.75 inference(scs_inference,[],[28,42935,54])).
% 70.74/70.75 cnf(43517,plain,
% 70.74/70.75 (~P48(a3,a5)+~P45(a2)),
% 70.74/70.75 inference(scs_inference,[],[38423,43226,89])).
% 70.74/70.75 cnf(43808,plain,
% 70.74/70.75 (~P44(a3)+~P45(a2)),
% 70.74/70.75 inference(scs_inference,[],[43517,25602])).
% 70.74/70.75 cnf(44097,plain,
% 70.74/70.75 (~P38(a2,a3,a2)+~P45(a2)),
% 70.74/70.75 inference(scs_inference,[],[43808,175])).
% 70.74/70.75 cnf(44142,plain,
% 70.74/70.75 (P47(a1)),
% 70.74/70.75 inference(scs_inference,[],[39,516,7408,47,201])).
% 70.74/70.75 cnf(44163,plain,
% 70.74/70.75 (P18(x441631,x441631)+~P2(x441631)),
% 70.74/70.75 inference(scs_inference,[],[44142,55])).
% 70.74/70.75 cnf(44609,plain,
% 70.74/70.75 (~P38(a3,a3,a2)+~P45(a2)),
% 70.74/70.75 inference(scs_inference,[],[391,522,44097,361])).
% 70.74/70.75 cnf(46014,plain,
% 70.74/70.75 (~P15(a2,a3)+~P45(a2)),
% 70.74/70.75 inference(scs_inference,[],[44609,144])).
% 70.74/70.75 cnf(46150,plain,
% 70.74/70.75 (P47(a2)),
% 70.74/70.75 inference(scs_inference,[],[39,3,4,27306,471,4365,47,44163,196,201])).
% 70.74/70.75 cnf(50351,plain,
% 70.74/70.75 (P42(x503511,a1,a1)+~P16(a4,x503511)+~P45(a3)),
% 70.74/70.75 inference(scs_inference,[],[154,414])).
% 70.74/70.75 cnf(50913,plain,
% 70.74/70.75 (P30(x509131,a5,x509131)),
% 70.74/70.75 inference(scs_inference,[],[3,28,156,241])).
% 70.74/70.75 cnf(50922,plain,
% 70.74/70.75 (P30(a2,a5,a5)),
% 70.74/70.75 inference(scs_inference,[],[39,3,4,27306,28,391,50913,44163,47,196,352])).
% 70.74/70.75 cnf(50927,plain,
% 70.74/70.75 (P22(a2,a5,a5)),
% 70.74/70.75 inference(scs_inference,[],[39,3,4,27306,28,391,50913,44163,47,196,352,594])).
% 70.74/70.75 cnf(52661,plain,
% 70.74/70.75 (P38(a2,a4,a3)),
% 70.74/70.75 inference(scs_inference,[],[3443,22,432,53])).
% 70.74/70.75 cnf(52890,plain,
% 70.74/70.75 (P14(a1,a4)+~P8(a3,a4,a3)+~P45(a3)),
% 70.74/70.75 inference(scs_inference,[],[435,414])).
% 70.74/70.75 cnf(54021,plain,
% 70.74/70.75 (~P45(a5)+P42(a4,a1,a1)+~P45(a3)),
% 70.74/70.75 inference(scs_inference,[],[29,28,50351,219])).
% 70.74/70.75 cnf(54493,plain,
% 70.74/70.75 (~P30(a4,a3,a3)+P14(a1,a4)+~P45(a3)),
% 70.74/70.75 inference(scs_inference,[],[52890,245])).
% 70.74/70.75 cnf(54965,plain,
% 70.74/70.75 (~P30(a4,a3,a4)+P14(a1,a4)+~P45(a3)),
% 70.74/70.75 inference(scs_inference,[],[516,522,54493,353])).
% 70.74/70.75 cnf(55436,plain,
% 70.74/70.75 (~P37(a4,a3,a4)+P14(a1,a4)+~P45(a3)),
% 70.74/70.75 inference(scs_inference,[],[54965,227])).
% 70.74/70.75 cnf(55666,plain,
% 70.74/70.75 (P14(a1,a4)+~P45(a3)),
% 70.74/70.75 inference(scs_inference,[],[22,28,55436,188])).
% 70.74/70.75 cnf(56823,plain,
% 70.74/70.75 (P27(x568231)),
% 70.74/70.75 inference(scs_inference,[],[35,3,4,27306,16248,44163,196,437,173])).
% 70.74/70.75 cnf(56835,plain,
% 70.74/70.75 (P6(a4)+~P36(a5,a2)),
% 70.74/70.75 inference(scs_inference,[],[56823,417])).
% 70.74/70.75 cnf(56836,plain,
% 70.74/70.75 (P8(a1,a5,a1)),
% 70.74/70.75 inference(scs_inference,[],[16248,245])).
% 70.74/70.75 cnf(56837,plain,
% 70.74/70.75 (P30(a5,a1,x568371)),
% 70.74/70.75 inference(rename_variables,[],[16248])).
% 70.74/70.75 cnf(56841,plain,
% 70.74/70.75 (P36(a2,a5)),
% 70.74/70.75 inference(scs_inference,[],[3,16248,11861,20,245,44163,209])).
% 70.74/70.75 cnf(56847,plain,
% 70.74/70.75 (P32(a2,a3,a2)),
% 70.74/70.75 inference(scs_inference,[],[3,4,27306,16248,699,11861,20,245,44163,209,196,249])).
% 70.74/70.75 cnf(56849,plain,
% 70.74/70.75 (P42(a5,x568491,a5)),
% 70.74/70.75 inference(scs_inference,[],[3,4,27306,16248,56837,699,11861,20,245,44163,209,196,249,248])).
% 70.74/70.75 cnf(56885,plain,
% 70.74/70.75 (P25(x568851)),
% 70.74/70.75 inference(scs_inference,[],[16242,172])).
% 70.74/70.75 cnf(56887,plain,
% 70.74/70.75 (P8(a4,a5,a4)),
% 70.74/70.75 inference(scs_inference,[],[872,16242,172,245])).
% 70.74/70.75 cnf(56891,plain,
% 70.74/70.75 (P22(x568911,x568911,x568911)),
% 70.74/70.75 inference(scs_inference,[],[6451,872,16242,172,245,249,105])).
% 70.74/70.75 cnf(56895,plain,
% 70.74/70.75 (P42(x568951,x568951,x568951)),
% 70.74/70.75 inference(scs_inference,[],[13199,6451,872,50913,16242,172,245,249,105,174,248])).
% 70.74/70.75 cnf(56899,plain,
% 70.74/70.75 (P31(x568991,a3,a3)),
% 70.74/70.75 inference(scs_inference,[],[3,13199,6451,631,872,50913,402,16242,172,245,249,105,174,248,44163,272])).
% 70.74/70.75 cnf(56924,plain,
% 70.74/70.75 (P32(a1,a5,a1)),
% 70.74/70.75 inference(scs_inference,[],[16296,485,245,249])).
% 70.74/70.75 cnf(56928,plain,
% 70.74/70.75 (P42(a1,x569281,a1)),
% 70.74/70.75 inference(scs_inference,[],[16296,56899,485,19291,245,249,174,248])).
% 70.74/70.75 cnf(56932,plain,
% 70.74/70.75 (P32(a5,a5,a1)),
% 70.74/70.75 inference(scs_inference,[],[3,16296,56899,485,19291,245,249,174,248,44163,275])).
% 70.74/70.75 cnf(56936,plain,
% 70.74/70.75 (P38(a3,a5,a5)),
% 70.74/70.75 inference(scs_inference,[],[3,16296,56899,56887,485,7,19291,559,522,245,249,174,248,44163,275,272,268])).
% 70.74/70.75 cnf(56945,plain,
% 70.74/70.75 (P31(x569451,a2,a2)+~P30(x569451,a2,a5)),
% 70.74/70.75 inference(scs_inference,[],[3,4,56847,16296,56836,56899,56887,485,7,19291,559,522,50927,245,249,174,248,44163,275,272,268,196,31114,271,339])).
% 70.74/70.75 cnf(56957,plain,
% 70.74/70.75 (P8(x569571,x569571,x569571)),
% 70.74/70.75 inference(scs_inference,[],[404,245])).
% 70.74/70.75 cnf(56959,plain,
% 70.74/70.75 (P32(a1,a4,a1)),
% 70.74/70.75 inference(scs_inference,[],[18649,404,245,249])).
% 70.74/70.75 cnf(56965,plain,
% 70.74/70.75 (P32(a5,a5,a4)),
% 70.74/70.75 inference(scs_inference,[],[3,18649,404,38974,245,249,248,44163,275])).
% 70.74/70.75 cnf(56978,plain,
% 70.74/70.75 (P32(a2,a4,a2)),
% 70.74/70.75 inference(scs_inference,[],[18673,19291,245,249])).
% 70.74/70.75 cnf(57002,plain,
% 70.74/70.75 (P32(a2,a5,a2)),
% 70.74/70.75 inference(scs_inference,[],[22312,38974,245,249])).
% 70.74/70.75 cnf(57008,plain,
% 70.74/70.75 (P31(a4,a5,a5)),
% 70.74/70.75 inference(scs_inference,[],[3,22312,50913,38974,559,245,249,44163,271,339])).
% 70.74/70.75 cnf(57024,plain,
% 70.74/70.75 (P32(a5,a2,a5)),
% 70.74/70.75 inference(scs_inference,[],[603,249])).
% 70.74/70.75 cnf(57924,plain,
% 70.74/70.75 (P35(a3,a2)),
% 70.74/70.75 inference(scs_inference,[],[3,4,56978,56957,31857,11861,44163,196,358])).
% 70.74/70.75 cnf(57935,plain,
% 70.74/70.75 (P26(a3,x579351,x579351)+~P15(a3,a3)),
% 70.74/70.75 inference(scs_inference,[],[36,3,4,56978,56957,31857,11861,5,391,502,52661,44163,196,358,209,283,437,302])).
% 70.74/70.75 cnf(57946,plain,
% 70.74/70.75 (P35(a4,a2)),
% 70.74/70.75 inference(scs_inference,[],[3,4,57002,18649,11861,56891,44163,196,358])).
% 70.74/70.75 cnf(58967,plain,
% 70.74/70.75 (P35(x589671,x589671)),
% 70.74/70.75 inference(scs_inference,[],[3,4,57002,56957,25588,462,8,56891,44163,268,196,358])).
% 70.74/70.75 cnf(58971,plain,
% 70.74/70.75 (P24(x589711,x589711)),
% 70.74/70.75 inference(scs_inference,[],[3,4,57002,56957,25588,462,8,56891,44163,268,196,358,67])).
% 70.74/70.75 cnf(59019,plain,
% 70.74/70.75 (P38(a3,a2,a2)),
% 70.74/70.75 inference(scs_inference,[],[3,8,522,44163,268])).
% 70.74/70.75 cnf(62951,plain,
% 70.74/70.75 (P26(a3,x629511,x629511)),
% 70.74/70.75 inference(scs_inference,[],[22,57935,65])).
% 70.74/70.75 cnf(64220,plain,
% 70.74/70.75 (P28(x642201,a2)+~P28(x642201,x642201)+~P30(x642201,a2,a5)),
% 70.74/70.75 inference(scs_inference,[],[56945,211])).
% 70.74/70.75 cnf(65636,plain,
% 70.74/70.75 (P35(x656361,a5)),
% 70.74/70.75 inference(scs_inference,[],[3,4,56978,631,11880,56891,44163,196,358])).
% 70.74/70.75 cnf(71523,plain,
% 70.74/70.75 (P6(a5)),
% 70.74/70.75 inference(scs_inference,[],[27088,16248,553,56928,210,321])).
% 70.74/70.75 cnf(71524,plain,
% 70.74/70.75 (P28(x715241,x715241)+~P22(x715241,x715241,x715241)),
% 70.74/70.75 inference(scs_inference,[],[71523,195])).
% 70.74/70.75 cnf(71532,plain,
% 70.74/70.75 (P28(x715321,x715321)),
% 70.74/70.75 inference(scs_inference,[],[56891,71524])).
% 70.74/70.75 cnf(76925,plain,
% 70.74/70.75 (P24(x769251,a4)+~P30(x769251,a2,a5)),
% 70.74/70.75 inference(scs_inference,[],[71532,64220,39013])).
% 70.74/70.75 cnf(77096,plain,
% 70.74/70.75 (~P20(a2,a5,a2)+P24(a5,a4)),
% 70.74/70.75 inference(scs_inference,[],[76925,241])).
% 70.74/70.75 cnf(77184,plain,
% 70.74/70.75 (P32(a2,a2,a5)),
% 70.74/70.75 inference(scs_inference,[],[4,71523,56849,47,44163,275])).
% 70.74/70.75 cnf(77306,plain,
% 70.74/70.75 (P24(a5,a4)),
% 70.74/70.75 inference(scs_inference,[],[2,28,77096,155])).
% 70.74/70.75 cnf(78631,plain,
% 70.74/70.75 (P20(x786311,x786311,x786311)),
% 70.74/70.75 inference(scs_inference,[],[27,38,293,234])).
% 70.74/70.75 cnf(78640,plain,
% 70.74/70.75 (P7(x786401,x786401)),
% 70.74/70.75 inference(scs_inference,[],[4,71523,77184,78631,444,47,44163,196,190])).
% 70.74/70.75 cnf(81537,plain,
% 70.74/70.75 (~P44(a5)+P6(a4)),
% 70.74/70.75 inference(scs_inference,[],[56841,466,220,56835])).
% 70.74/70.75 cnf(81764,plain,
% 70.74/70.75 (P6(a4)+~P45(a2)),
% 70.74/70.75 inference(scs_inference,[],[11880,81537,175])).
% 70.74/70.75 cnf(83330,plain,
% 70.74/70.75 (P22(a2,x833301,a2)+~P45(a3)),
% 70.74/70.75 inference(scs_inference,[],[3443,38,34,414,356])).
% 70.74/70.75 cnf(90812,plain,
% 70.74/70.75 (P36(a1,a5)+~P26(x908121,a1,a5)+~P45(a3)),
% 70.74/70.75 inference(scs_inference,[],[27088,414,220])).
% 70.74/70.75 cnf(91029,plain,
% 70.74/70.75 (~P12(a1,x910291,x910291)+P36(a1,a5)+~P45(a3)),
% 70.74/70.75 inference(scs_inference,[],[38,90812,332])).
% 70.74/70.75 cnf(93184,plain,
% 70.74/70.75 (P5(a2)),
% 70.74/70.75 inference(scs_inference,[],[21,53])).
% 70.74/70.75 cnf(93186,plain,
% 70.74/70.75 (P15(a2,a2)),
% 70.74/70.75 inference(scs_inference,[],[21,53,65])).
% 70.74/70.75 cnf(93188,plain,
% 70.74/70.75 (P29(x931881,x931881,a2)),
% 70.74/70.75 inference(scs_inference,[],[21,28,53,65,136])).
% 70.74/70.75 cnf(93190,plain,
% 70.74/70.75 (P29(x931901,x931901,x931901)),
% 70.74/70.75 inference(scs_inference,[],[21,28,53,65,136,139])).
% 70.74/70.75 cnf(93196,plain,
% 70.74/70.75 (P20(a5,a2,a5)),
% 70.74/70.75 inference(scs_inference,[],[21,471,35,26,28,53,65,136,139,140,144,234])).
% 70.74/70.75 cnf(93205,plain,
% 70.74/70.75 (P45(a2)),
% 70.74/70.75 inference(scs_inference,[],[680,21,1,471,35,38,26,28,53,65,136,139,140,144,234,423,447,226,54])).
% 70.74/70.75 cnf(93206,plain,
% 70.74/70.75 (P23(a2,x932061)),
% 70.74/70.75 inference(rename_variables,[],[28])).
% 70.74/70.75 cnf(93208,plain,
% 70.74/70.75 (~P15(a2,a3)),
% 70.74/70.75 inference(scs_inference,[],[680,21,1,471,35,38,26,28,53,65,136,139,140,144,234,423,447,226,54,46014])).
% 70.74/70.75 cnf(93210,plain,
% 70.74/70.75 (~P18(a1,x932101)),
% 70.74/70.75 inference(rename_variables,[],[39])).
% 70.74/70.75 cnf(93215,plain,
% 70.74/70.75 (P20(a5,a3,a5)),
% 70.74/70.75 inference(scs_inference,[],[39,93210,680,21,1,471,35,3,5,38,26,28,53,65,136,139,140,144,234,423,447,226,54,46014,47,44163,121])).
% 70.74/70.75 cnf(93217,plain,
% 70.74/70.75 (P20(a3,a2,a3)),
% 70.74/70.75 inference(scs_inference,[],[39,93210,680,21,1,8,471,35,3,5,38,26,28,53,65,136,139,140,144,234,423,447,226,54,46014,47,44163,121,122])).
% 70.74/70.75 cnf(93219,plain,
% 70.74/70.75 (P20(a2,x932191,a2)),
% 70.74/70.75 inference(scs_inference,[],[39,93210,680,21,1,2,8,471,35,3,5,38,26,28,93206,53,65,136,139,140,144,234,423,447,226,54,46014,47,44163,121,122,155])).
% 70.74/70.75 cnf(93229,plain,
% 70.74/70.75 (P16(a2,a5)),
% 70.74/70.75 inference(scs_inference,[],[39,93210,566,57946,44142,38698,680,21,1,2,8,471,35,3,5,38,26,19,28,93206,53,65,136,139,140,144,234,423,447,226,54,46014,47,44163,121,122,155,157,162,163,194,42935])).
% 70.74/70.75 cnf(93238,plain,
% 70.74/70.75 (P38(a2,a4,a2)),
% 70.74/70.75 inference(scs_inference,[],[39,93210,566,57946,38423,44142,38698,27088,680,21,16,1,2,8,471,35,3,5,38,26,19,16248,28,93206,53,65,136,139,140,144,234,423,447,226,54,46014,47,44163,121,122,155,157,162,163,194,42935,89,188,210,432])).
% 70.74/70.75 cnf(93240,plain,
% 70.74/70.75 (P44(a5)),
% 70.74/70.75 inference(scs_inference,[],[39,93210,566,57946,38423,44142,38698,27088,680,21,16,1,2,8,471,35,3,5,38,11880,26,19,16248,28,93206,53,65,136,139,140,144,234,423,447,226,54,46014,47,44163,121,122,155,157,162,163,194,42935,89,188,210,432,175])).
% 70.74/70.75 cnf(93252,plain,
% 70.74/70.75 (P45(a1)),
% 70.74/70.75 inference(scs_inference,[],[39,93210,566,57946,10,38423,44142,38698,27088,680,464,21,16,1,2,8,471,33,391,35,3,5,38,11880,34,26,37,19,16248,28,93206,53,65,136,139,140,144,234,423,447,226,54,46014,47,44163,121,122,155,157,162,163,194,42935,89,188,210,432,175,255,332,333,254,62])).
% 70.74/70.75 cnf(93254,plain,
% 70.74/70.75 (P20(a1,a3,a2)),
% 70.74/70.75 inference(scs_inference,[],[39,93210,566,57946,10,38423,44142,38698,27088,680,464,21,16,1,2,8,471,33,391,35,3,5,38,11880,34,26,37,19,16248,28,93206,53,65,136,139,140,144,234,423,447,226,54,46014,47,44163,121,122,155,157,162,163,194,42935,89,188,210,432,175,255,332,333,254,62,456])).
% 70.74/70.75 cnf(93272,plain,
% 70.74/70.75 (P44(a1)),
% 70.74/70.75 inference(scs_inference,[],[39,93210,566,62951,57946,56936,466,56841,10,38423,44142,376,38698,27088,56885,680,464,21,31857,16,1,2,500,402,8,471,33,391,35,3,5,38,11880,34,26,37,19,16248,28,93206,4,53,65,136,139,140,144,234,423,447,226,54,46014,47,44163,121,122,155,157,162,163,194,42935,89,188,210,432,175,255,332,333,254,62,456,437,75,177,220,287,361,25602,415])).
% 70.74/70.75 cnf(93277,plain,
% 70.74/70.75 (P31(a3,a3,a2)),
% 70.74/70.75 inference(scs_inference,[],[39,93210,566,62951,57946,56936,466,56841,10,38423,44142,376,38698,27088,56885,680,464,21,31857,16,1,2,500,402,8,471,33,391,35,3,5,38,11880,34,26,37,19,16248,28,93206,4,53,65,136,139,140,144,234,423,447,226,54,46014,47,44163,121,122,155,157,162,163,194,42935,89,188,210,432,175,255,332,333,254,62,456,437,75,177,220,287,361,25602,415,587,43808,81764,13212])).
% 70.74/70.75 cnf(93278,plain,
% 70.74/70.75 (~P38(a2,a3,a2)),
% 70.74/70.75 inference(scs_inference,[],[39,93210,566,62951,57946,56936,466,56841,10,38423,44142,376,38698,27088,56885,680,464,21,31857,16,1,2,500,402,8,471,33,391,35,3,5,38,11880,34,26,37,19,16248,28,93206,4,53,65,136,139,140,144,234,423,447,226,54,46014,47,44163,121,122,155,157,162,163,194,42935,89,188,210,432,175,255,332,333,254,62,456,437,75,177,220,287,361,25602,415,587,43808,81764,13212,44097])).
% 70.74/70.75 cnf(93280,plain,
% 70.74/70.75 (P20(a5,a4,a5)),
% 70.74/70.75 inference(scs_inference,[],[39,93210,566,62951,57946,56936,466,56841,10,38423,44142,376,38698,27088,56885,680,464,21,31857,16,1,2,500,402,8,471,33,391,35,3,5,38,11880,34,26,37,19,16248,28,93206,4,53,65,136,139,140,144,234,423,447,226,54,46014,47,44163,121,122,155,157,162,163,194,42935,89,188,210,432,175,255,332,333,254,62,456,437,75,177,220,287,361,25602,415,587,43808,81764,13212,44097,44609,156])).
% 70.74/70.75 cnf(93281,plain,
% 70.74/70.75 (P23(a2,x932811)),
% 70.74/70.75 inference(rename_variables,[],[28])).
% 70.74/70.75 cnf(93283,plain,
% 70.74/70.75 (P42(x932831,a5,a5)+~P16(a4,x932831)),
% 70.74/70.75 inference(scs_inference,[],[39,93210,566,62951,57946,56936,466,56841,10,38423,44142,376,38698,27088,56885,680,464,21,31857,16,1,2,500,402,8,471,33,391,35,3,5,38,11880,34,26,37,19,16248,28,93206,4,53,65,136,139,140,144,234,423,447,226,54,46014,47,44163,121,122,155,157,162,163,194,42935,89,188,210,432,175,255,332,333,254,62,456,437,75,177,220,287,361,25602,415,587,43808,81764,13212,44097,44609,156,154])).
% 70.74/70.75 cnf(93286,plain,
% 70.74/70.75 (P23(a2,x932861)),
% 70.74/70.75 inference(rename_variables,[],[28])).
% 70.74/70.75 cnf(93288,plain,
% 70.74/70.75 (P31(a2,a5,a5)),
% 70.74/70.75 inference(scs_inference,[],[39,93210,566,62951,57946,56936,466,56841,10,38423,44142,376,38698,50922,27088,56885,680,464,21,31857,16,1,2,500,402,56891,8,471,33,391,35,3,5,38,11880,34,26,37,19,16248,28,93206,93281,4,53,65,136,139,140,144,234,423,447,226,54,46014,47,44163,121,122,155,157,162,163,194,42935,89,188,210,432,175,255,332,333,254,62,456,437,75,177,220,287,361,25602,415,587,43808,81764,13212,44097,44609,156,154,186,339])).
% 70.74/70.75 cnf(93289,plain,
% 70.74/70.75 (P22(x932891,x932891,x932891)),
% 70.74/70.75 inference(rename_variables,[],[56891])).
% 70.74/70.75 cnf(93292,plain,
% 70.74/70.75 (P23(a2,x932921)),
% 70.74/70.75 inference(rename_variables,[],[28])).
% 70.74/70.75 cnf(93294,plain,
% 70.74/70.75 (P16(a5,a5)),
% 70.74/70.75 inference(scs_inference,[],[39,93210,566,62951,57946,56936,466,56841,10,38423,44142,376,38698,50922,27088,56885,680,464,21,31857,16,1,2,500,402,56891,8,471,33,391,35,3,5,38,11880,34,26,37,13,19,16248,28,93206,93281,93286,93292,4,53,65,136,139,140,144,234,423,447,226,54,46014,47,44163,121,122,155,157,162,163,194,42935,89,188,210,432,175,255,332,333,254,62,456,437,75,177,220,287,361,25602,415,587,43808,81764,13212,44097,44609,156,154,186,339,193,219])).
% 70.74/70.75 cnf(93297,plain,
% 70.74/70.75 (P35(a3,a4)),
% 70.74/70.75 inference(scs_inference,[],[39,93210,566,62951,57946,56936,466,56841,10,38423,44142,376,38698,50922,27088,56885,56957,680,464,21,31857,16,1,2,500,402,56891,93289,8,471,33,391,35,3,5,38,11880,34,26,37,52661,13,19,16248,28,93206,93281,93286,93292,4,53,65,136,139,140,144,234,423,447,226,54,46014,47,44163,121,122,155,157,162,163,194,42935,89,188,210,432,175,255,332,333,254,62,456,437,75,177,220,287,361,25602,415,587,43808,81764,13212,44097,44609,156,154,186,339,193,219,358])).
% 70.74/70.75 cnf(93301,plain,
% 70.74/70.75 (P24(a2,x933011)),
% 70.74/70.75 inference(scs_inference,[],[39,93210,566,62951,57946,56936,466,56841,10,38423,44142,376,38698,50922,27088,56885,56957,71532,680,464,21,31857,58971,16,1,2,500,402,56891,93289,8,471,33,391,35,3,5,38,11880,34,26,37,27306,52661,13,19,16248,28,93206,93281,93286,93292,4,53,65,136,139,140,144,234,423,447,226,54,46014,47,44163,121,122,155,157,162,163,194,42935,89,188,210,432,175,255,332,333,254,62,456,437,75,177,220,287,361,25602,415,587,43808,81764,13212,44097,44609,156,154,186,339,193,219,358,299])).
% 70.74/70.75 cnf(93308,plain,
% 70.74/70.75 (~P10(x933081,x933082)+P45(x933081)),
% 70.74/70.75 inference(scs_inference,[],[93205,62])).
% 70.74/70.75 cnf(93310,plain,
% 70.74/70.75 (P44(x933101)+~P38(a2,x933101,a2)),
% 70.74/70.75 inference(scs_inference,[],[93205,175])).
% 70.74/70.75 cnf(93313,plain,
% 70.74/70.75 (~P45(x933131)+P16(x933131,a5)),
% 70.74/70.75 inference(scs_inference,[],[93294,817])).
% 70.74/70.75 cnf(93322,plain,
% 70.74/70.75 (P44(a4)),
% 70.74/70.75 inference(scs_inference,[],[93238,93310])).
% 70.74/70.75 cnf(93326,plain,
% 70.74/70.75 (P38(x933261,x933261,a1)),
% 70.74/70.75 inference(scs_inference,[],[93238,26,516,93310,140,144])).
% 70.74/70.75 cnf(93334,plain,
% 70.74/70.75 (P15(a3,a3)),
% 70.74/70.75 inference(scs_inference,[],[93238,93240,16242,22,26,29,516,93310,140,144,25602,226,447,65])).
% 70.74/70.75 cnf(93336,plain,
% 70.74/70.75 (P20(x933361,a1,x933361)),
% 70.74/70.75 inference(scs_inference,[],[93238,93240,16242,22,38,26,29,516,93310,140,144,25602,226,447,65,234])).
% 70.74/70.75 cnf(93337,plain,
% 70.74/70.75 (P12(x933371,a1,x933372)),
% 70.74/70.75 inference(rename_variables,[],[38])).
% 70.74/70.75 cnf(93341,plain,
% 70.74/70.75 (P5(a3)),
% 70.74/70.75 inference(scs_inference,[],[93238,93240,16242,22,1,38,26,29,516,93310,140,144,25602,226,447,65,234,423,53])).
% 70.74/70.75 cnf(93344,plain,
% 70.74/70.75 (~P18(a1,x933441)),
% 70.74/70.75 inference(rename_variables,[],[39])).
% 70.74/70.75 cnf(93350,plain,
% 70.74/70.75 (P28(x933501,x933501)),
% 70.74/70.75 inference(rename_variables,[],[71532])).
% 70.74/70.75 cnf(93352,plain,
% 70.74/70.75 (P20(a3,a5,a3)),
% 70.74/70.75 inference(scs_inference,[],[39,93344,93288,93238,93240,71532,16242,22,1,5,38,26,29,7,516,93310,140,144,25602,226,447,65,234,423,53,47,44163,211,122])).
% 70.74/70.75 cnf(93356,plain,
% 70.74/70.75 (P38(a5,a4,a2)),
% 70.74/70.75 inference(scs_inference,[],[39,93344,93288,93229,93184,93238,93240,65636,71532,16242,21,22,1,5,38,26,29,7,516,28,93310,140,144,25602,226,447,65,234,423,53,47,44163,211,122,188,432])).
% 70.74/70.75 cnf(93366,plain,
% 70.74/70.75 (P47(a3)),
% 70.74/70.75 inference(scs_inference,[],[39,93344,93288,93229,46150,93184,93205,93238,93240,93277,93280,93294,93297,65636,38698,71532,16242,21,22,1,14,3,5,38,26,29,7,516,28,93310,140,144,25602,226,447,65,234,423,53,47,44163,211,122,188,432,194,163,162,456,201])).
% 70.74/70.75 cnf(93370,plain,
% 70.74/70.75 (P7(a5,a2)),
% 70.74/70.75 inference(scs_inference,[],[39,93344,93288,93196,93229,93208,46150,93184,93205,93238,93240,93277,93280,93294,93297,78640,65636,38698,71532,16242,21,22,1,14,3,5,38,26,29,7,516,28,93310,140,144,25602,226,447,65,234,423,53,47,44163,211,122,188,432,194,163,162,456,201,437,218])).
% 70.74/70.75 cnf(93374,plain,
% 70.74/70.75 (P23(a2,x933741)),
% 70.74/70.75 inference(rename_variables,[],[28])).
% 70.74/70.75 cnf(93376,plain,
% 70.74/70.75 (P45(x933761)),
% 70.74/70.75 inference(scs_inference,[],[39,93344,93288,93196,93229,93208,46150,93184,93205,93238,93240,93277,93280,93294,93297,78640,65636,38698,71532,16242,21,22,1,14,3,5,38,27,26,29,7,516,28,93310,140,144,25602,226,447,65,234,423,53,47,44163,211,122,188,432,194,163,162,456,201,437,218,177,93308])).
% 70.74/70.75 cnf(93378,plain,
% 70.74/70.75 (P16(x933781,a5)),
% 70.74/70.75 inference(scs_inference,[],[39,93344,93288,93196,93229,93208,46150,93184,93205,93238,93240,93277,93280,93294,93297,78640,65636,38698,71532,16242,21,22,1,14,3,5,38,27,26,29,7,516,28,93310,140,144,25602,226,447,65,234,423,53,47,44163,211,122,188,432,194,163,162,456,201,437,218,177,93308,93313])).
% 70.74/70.75 cnf(93381,plain,
% 70.74/70.75 (P22(a2,a2,a3)),
% 70.74/70.75 inference(scs_inference,[],[39,93344,93288,93196,93229,93208,46150,93184,93205,93238,93240,93277,93280,93294,93297,78640,65636,38698,71532,16242,21,22,1,14,3,5,38,27,26,29,7,516,28,93310,140,144,25602,226,447,65,234,423,53,47,44163,211,122,188,432,194,163,162,456,201,437,218,177,93308,93313,55666,13455])).
% 70.74/70.75 cnf(93387,plain,
% 70.74/70.75 (P12(x933871,a1,x933872)),
% 70.74/70.75 inference(rename_variables,[],[38])).
% 70.74/70.75 cnf(93391,plain,
% 70.74/70.75 (P38(x933911,a2,a2)),
% 70.74/70.75 inference(scs_inference,[],[39,93344,93190,93288,93196,93229,93208,46150,93184,93205,93238,93240,93277,93280,93294,93297,78640,65636,38698,71532,16242,21,22,1,14,8,3,5,38,93337,27,26,29,7,516,28,93310,140,144,25602,226,447,65,234,423,53,47,44163,211,122,188,432,194,163,162,456,201,437,218,177,93308,93313,55666,13455,18288,20961,585,91029,155,268])).
% 70.74/70.75 cnf(93393,plain,
% 70.74/70.75 (P16(x933931,x933931)),
% 70.74/70.75 inference(scs_inference,[],[39,93344,93190,93288,93196,93229,93208,46150,93184,93205,93238,93240,93252,93277,93280,93294,93297,78640,65636,38698,71532,16242,21,22,1,14,8,3,5,38,93337,93387,27,26,29,7,516,28,93374,93310,140,144,25602,226,447,65,234,423,53,47,44163,211,122,188,432,194,163,162,456,201,437,218,177,93308,93313,55666,13455,18288,20961,585,91029,155,268,219])).
% 70.74/70.75 cnf(93407,plain,
% 70.74/70.75 (P42(a4,a1,a1)+~P45(a5)),
% 70.74/70.75 inference(scs_inference,[],[39,93344,93190,93288,93196,93229,93208,93301,46150,93184,93205,93238,93240,93252,93277,93278,93280,93294,93297,59019,62951,78640,65636,38698,71532,93350,16242,21,22,1,14,8,393,3,5,38,93337,93387,27,26,77184,25588,29,7,516,28,93374,93310,140,144,25602,226,447,65,234,423,53,47,44163,211,122,188,432,194,163,162,456,201,437,218,177,93308,93313,55666,13455,18288,20961,585,91029,155,268,219,361,299,350,54021])).
% 70.74/70.75 cnf(93408,plain,
% 70.74/70.75 (P20(x934081,x934082,x934082)+~P10(x934081,x934081)+~P5(x934082)),
% 70.74/70.75 inference(scs_inference,[],[93341,169])).
% 70.74/70.75 cnf(93409,plain,
% 70.74/70.75 (P22(x934091,a4,x934091)+~P38(x934091,a4,a4)),
% 70.74/70.75 inference(scs_inference,[],[93322,233])).
% 70.74/70.75 cnf(93414,plain,
% 70.74/70.75 (~P16(a4,x934141)+P42(x934141,a1,a1)),
% 70.74/70.75 inference(scs_inference,[],[93376,50351])).
% 70.74/70.75 cnf(93415,plain,
% 70.74/70.75 (P22(a2,x934151,a2)),
% 70.74/70.75 inference(scs_inference,[],[93376,83330])).
% 70.74/70.75 cnf(93419,plain,
% 70.74/70.75 (P16(x934191,x934191)),
% 70.74/70.75 inference(rename_variables,[],[93393])).
% 70.74/70.75 cnf(93421,plain,
% 70.74/70.75 (P16(x934211,a2)),
% 70.74/70.75 inference(scs_inference,[],[93393,93376,93283,587])).
% 70.74/70.75 cnf(93427,plain,
% 70.74/70.75 (P5(a5)),
% 70.74/70.75 inference(scs_inference,[],[93393,93376,480,16,26,93283,587,447,140,53])).
% 70.74/70.75 cnf(93431,plain,
% 70.74/70.75 (P15(a5,a5)),
% 70.74/70.75 inference(scs_inference,[],[93393,93376,93322,480,16,26,93283,587,447,140,53,25602,65])).
% 70.74/70.75 cnf(93436,plain,
% 70.74/70.75 (~P18(a1,x934361)),
% 70.74/70.75 inference(rename_variables,[],[39])).
% 70.74/70.75 cnf(93446,plain,
% 70.74/70.75 (P16(x934461,x934461)),
% 70.74/70.75 inference(rename_variables,[],[93393])).
% 70.74/70.75 cnf(93450,plain,
% 70.74/70.75 (P20(a4,a2,a4)),
% 70.74/70.75 inference(scs_inference,[],[39,93436,93393,93419,93376,93322,93341,58967,38698,15,480,16,1,8,3,26,6,93283,587,447,140,53,25602,65,423,47,44163,93408,188,432,194,122])).
% 70.74/70.75 cnf(93461,plain,
% 70.74/70.75 (P8(a4,x934611,a4)),
% 70.74/70.75 inference(scs_inference,[],[39,93436,93393,93419,93446,93376,93322,93341,93366,57924,31329,57008,93208,58967,38698,15,71532,480,16,1,23,8,3,26,6,93283,587,447,140,53,25602,65,423,47,44163,93408,188,432,194,122,211,163,162,437,308])).
% 70.74/70.75 cnf(93462,plain,
% 70.74/70.75 (P45(x934621)),
% 70.74/70.75 inference(rename_variables,[],[93376])).
% 70.74/70.75 cnf(93464,plain,
% 70.74/70.75 (P35(a1,a3)),
% 70.74/70.75 inference(scs_inference,[],[39,93436,93393,93419,93446,93376,93326,93322,93341,93366,57924,31329,57008,93208,58967,38698,56957,15,71532,31857,480,16,1,23,8,3,26,6,93283,587,447,140,53,25602,65,423,47,44163,93408,188,432,194,122,211,163,162,437,308,358])).
% 70.74/70.75 cnf(93468,plain,
% 70.74/70.75 (P7(a5,a3)),
% 70.74/70.75 inference(scs_inference,[],[39,93436,93393,93419,93446,93376,93215,93326,93322,93341,93366,57924,31329,57008,93208,78640,58967,38698,56957,15,71532,31857,480,16,1,23,8,3,26,6,93283,587,447,140,53,25602,65,423,47,44163,93408,188,432,194,122,211,163,162,437,308,358,218])).
% 70.74/70.75 cnf(93481,plain,
% 70.74/70.75 (P31(a1,a5,a3)),
% 70.74/70.75 inference(scs_inference,[],[39,93436,93393,93419,93446,93376,93462,93215,93326,93378,93322,93341,93366,57924,31329,57008,93208,93278,78640,58967,38698,56957,15,71532,31857,480,16,1,23,8,393,3,38,26,25588,6,93283,587,447,140,53,25602,65,423,47,44163,93408,188,432,194,122,211,163,162,437,308,358,218,350,93407,93414,585])).
% 70.74/70.75 cnf(93503,plain,
% 70.74/70.75 (P5(a4)),
% 70.74/70.75 inference(scs_inference,[],[18,870,447,53])).
% 70.74/70.75 cnf(93509,plain,
% 70.74/70.75 (P15(a4,a4)),
% 70.74/70.75 inference(scs_inference,[],[93272,18,870,26,447,53,25602,140,65])).
% 70.74/70.75 cnf(93514,plain,
% 70.74/70.75 (~P18(a1,x935141)),
% 70.74/70.75 inference(rename_variables,[],[39])).
% 70.74/70.75 cnf(93521,plain,
% 70.74/70.75 (P38(a2,a4,a5)),
% 70.74/70.75 inference(scs_inference,[],[39,93514,93421,93427,93272,15,1,18,870,26,447,53,25602,140,65,423,47,44163,93408,432])).
% 70.74/70.75 cnf(93522,plain,
% 70.74/70.75 (P16(x935221,a2)),
% 70.74/70.75 inference(rename_variables,[],[93421])).
% 70.74/70.75 cnf(93531,plain,
% 70.74/70.75 (P31(a4,a4,x935311)),
% 70.74/70.75 inference(scs_inference,[],[39,93514,93421,93522,93461,93427,93464,93272,44142,93376,38698,15,1,559,18,3,870,26,447,53,25602,140,65,423,47,44163,93408,432,194,163,162,272])).
% 70.74/70.75 cnf(93533,plain,
% 70.74/70.75 (P47(a5)),
% 70.74/70.75 inference(scs_inference,[],[39,93514,93421,93522,93431,93461,93427,93464,93481,93272,44142,93376,38698,15,1,559,18,3,870,26,447,53,25602,140,65,423,47,44163,93408,432,194,163,162,272,201])).
% 70.74/70.75 cnf(93537,plain,
% 70.74/70.75 (P7(a2,a3)),
% 70.74/70.75 inference(scs_inference,[],[39,93514,93254,93421,93522,93431,93461,93427,93464,93468,93481,93272,93208,44142,93376,38698,15,1,559,18,3,870,26,447,53,25602,140,65,423,47,44163,93408,432,194,163,162,272,201,437,218])).
% 70.74/70.75 cnf(93551,plain,
% 70.74/70.75 (P42(a3,a5,a3)),
% 70.74/70.75 inference(scs_inference,[],[39,93514,93254,93421,93522,93431,93461,77306,93356,93427,93464,93468,93481,93272,93393,93208,44142,93376,56965,38698,15,71532,56895,1,402,559,18,3,38,870,26,37,447,53,25602,140,65,423,47,44163,93408,432,194,163,162,272,201,437,218,356,299,585,209,309])).
% 70.74/70.75 cnf(93556,plain,
% 70.74/70.75 (~P11(x935561,x935561)+~P23(x935561,x935562)+P20(x935562,x935562,a4)),
% 70.74/70.75 inference(scs_inference,[],[93509,205])).
% 70.74/70.75 cnf(93559,plain,
% 70.74/70.75 (P5(a1)),
% 70.74/70.75 inference(scs_inference,[],[93322,23,25602,53])).
% 70.74/70.75 cnf(93566,plain,
% 70.74/70.75 (~P18(a1,x935661)),
% 70.74/70.75 inference(rename_variables,[],[39])).
% 70.74/70.75 cnf(93572,plain,
% 70.74/70.75 (P16(x935721,a2)),
% 70.74/70.75 inference(rename_variables,[],[93421])).
% 70.74/70.75 cnf(93579,plain,
% 70.74/70.75 (P47(a4)),
% 70.74/70.75 inference(scs_inference,[],[39,93566,93531,93503,93509,93533,93421,93572,93322,38698,1,23,3,26,25602,53,423,140,47,44163,163,194,432,201])).
% 70.74/70.75 cnf(93583,plain,
% 70.74/70.75 (P42(a3,a2,a3)),
% 70.74/70.75 inference(scs_inference,[],[39,93566,93531,93503,93509,93533,93537,93421,93572,93322,93208,38698,56895,1,402,23,3,26,25602,53,423,140,47,44163,163,194,432,201,437,309])).
% 70.74/70.75 cnf(93586,plain,
% 70.74/70.75 (P7(a2,a4)),
% 70.74/70.75 inference(scs_inference,[],[39,93566,93531,93503,93509,93533,93537,93219,93421,93572,93322,93208,78640,38698,56895,1,402,23,3,26,25602,53,423,140,47,44163,163,194,432,201,437,309,218])).
% 70.74/70.75 cnf(93604,plain,
% 70.74/70.75 (P42(a4,a2,a4)+~P7(a4,a2)),
% 70.74/70.75 inference(scs_inference,[],[39,93566,93381,93551,93531,93503,93509,93533,93537,93219,93421,93572,93322,57946,56928,93208,78640,93376,38698,56895,548,1,402,23,3,27,26,19,28,25602,53,423,140,47,44163,163,194,432,201,437,309,218,585,93556,162,275,193,345,29818])).
% 70.74/70.75 cnf(93613,plain,
% 70.74/70.75 (~P18(a1,x936131)),
% 70.74/70.75 inference(rename_variables,[],[39])).
% 70.74/70.75 cnf(93619,plain,
% 70.74/70.75 (P16(x936191,a5)),
% 70.74/70.75 inference(rename_variables,[],[93378])).
% 70.74/70.75 cnf(93628,plain,
% 70.74/70.75 (P7(x936281,a1)),
% 70.74/70.75 inference(scs_inference,[],[39,93613,93559,93579,93336,93378,93619,93240,65636,93208,78640,38698,1,3,26,25602,423,140,47,44163,432,194,163,437,218])).
% 70.74/70.75 cnf(93631,plain,
% 70.74/70.75 (P8(a1,a1,x936311)),
% 70.74/70.75 inference(scs_inference,[],[39,93613,93559,93579,93336,93378,93619,93240,65636,93208,78640,38698,1,3,26,25602,423,140,47,44163,432,194,163,437,218,145])).
% 70.74/70.75 cnf(93633,plain,
% 70.74/70.75 (P44(a2)),
% 70.74/70.75 inference(scs_inference,[],[39,93613,93559,93579,93336,93391,93378,93619,93240,65636,93208,78640,38698,1,3,26,25602,423,140,47,44163,432,194,163,437,218,145,93310])).
% 70.74/70.75 cnf(93652,plain,
% 70.74/70.75 (~P18(a1,x936521)),
% 70.74/70.75 inference(rename_variables,[],[39])).
% 70.74/70.75 cnf(93658,plain,
% 70.74/70.75 (P12(x936581,a1,x936582)),
% 70.74/70.75 inference(rename_variables,[],[38])).
% 70.74/70.75 cnf(93661,plain,
% 70.74/70.75 (P16(x936611,x936611)),
% 70.74/70.75 inference(rename_variables,[],[93393])).
% 70.74/70.75 cnf(93666,plain,
% 70.74/70.75 (P16(x936661,x936661)),
% 70.74/70.75 inference(rename_variables,[],[93393])).
% 70.74/70.75 cnf(93676,plain,
% 70.74/70.75 (P7(a5,a4)),
% 70.74/70.75 inference(scs_inference,[],[39,93652,93586,93633,46150,93280,93393,93661,93666,93322,93559,93184,58967,93208,38698,1,18,3,38,32,26,28,423,25602,140,44163,47,332,154,156,432,163,194,209,437,218])).
% 70.74/70.75 cnf(93685,plain,
% 70.74/70.75 (P16(x936851,a2)),
% 70.74/70.75 inference(rename_variables,[],[93421])).
% 70.74/70.75 cnf(93697,plain,
% 70.74/70.75 (P38(a5,a1,a5)),
% 70.74/70.75 inference(scs_inference,[],[39,93652,93628,93586,93633,14435,46150,93280,1936,93393,93661,93666,93421,93685,93322,93559,93190,93184,58967,93208,38698,1,559,18,23,35,3,38,93658,32,26,28,423,25602,140,44163,47,332,154,156,432,163,194,209,437,218,356,145,93414,93283,585,153,283,361])).
% 70.74/70.75 cnf(93715,plain,
% 70.74/70.75 (~P18(a1,x937151)),
% 70.74/70.75 inference(rename_variables,[],[39])).
% 70.74/70.75 cnf(93721,plain,
% 70.74/70.75 (P16(x937211,a5)),
% 70.74/70.75 inference(rename_variables,[],[93378])).
% 70.74/70.75 cnf(93736,plain,
% 70.74/70.75 (P35(a5,a4)),
% 70.74/70.75 inference(scs_inference,[],[39,93715,93415,93631,93521,93676,93697,93533,93378,93721,93240,93503,93208,38698,1,23,3,26,140,25602,423,47,44163,432,194,163,437,93409,291,209,358])).
% 70.74/70.75 cnf(93752,plain,
% 70.74/70.75 (~P18(a1,x937521)),
% 70.74/70.75 inference(rename_variables,[],[39])).
% 70.74/70.75 cnf(93765,plain,
% 70.74/70.75 (P16(x937651,a5)),
% 70.74/70.75 inference(rename_variables,[],[93378])).
% 70.74/70.75 cnf(93780,plain,
% 70.74/70.75 (P30(a2,a3,a2)),
% 70.74/70.75 inference(scs_inference,[],[39,93752,57024,93217,93736,93579,93219,93370,93272,93378,93765,93341,93427,93376,93208,38698,22,1,3,26,13,423,25602,140,44163,47,188,162,456,432,331,163,194,196,437,218,227])).
% 70.74/70.75 cnf(93799,plain,
% 70.74/70.75 (~P18(a1,x937991)),
% 70.74/70.75 inference(rename_variables,[],[39])).
% 70.74/70.75 cnf(93826,plain,
% 70.74/70.75 (P42(a4,a2,a4)),
% 70.74/70.75 inference(scs_inference,[],[39,93799,93450,93780,93186,93188,93322,93184,93503,78640,65636,93376,15,17,93208,38698,1,3,26,19,140,423,25602,47,44163,93408,162,194,437,308,218,120,585,93556,353,93604])).
% 70.74/70.75 cnf(93839,plain,
% 70.74/70.75 (~P18(a1,x938391)),
% 70.74/70.75 inference(rename_variables,[],[39])).
% 70.74/70.75 cnf(93851,plain,
% 70.74/70.75 (P32(a2,a2,a4)),
% 70.74/70.75 inference(scs_inference,[],[39,93839,93826,93780,93240,93421,93559,58967,93208,1,26,4,25602,423,140,44163,47,432,194,437,275])).
% 70.74/70.75 cnf(93990,plain,
% 70.74/70.75 (~P18(a1,x939901)),
% 70.74/70.75 inference(rename_variables,[],[39])).
% 70.74/70.75 cnf(94009,plain,
% 70.74/70.75 (P32(a2,a2,a3)),
% 70.74/70.75 inference(scs_inference,[],[93352,93583,93240,28,78640,93503,93427,93208,39,93990,4,47,44163,25602,140,437,218,145,585,275])).
% 70.74/70.75 cnf(100540,plain,
% 70.74/70.75 (~P18(a1,x1005401)),
% 70.74/70.75 inference(rename_variables,[],[39])).
% 70.74/70.75 cnf(100553,plain,
% 70.74/70.75 (P22(a5,x1005531,a5)+~P12(a5,x1005532,x1005532)),
% 70.74/70.75 inference(scs_inference,[],[38,94009,93378,93503,404,93272,26,4,93208,39,100540,19,47,44163,140,196,437,93556,356])).
% 70.74/70.75 cnf(100557,plain,
% 70.74/70.75 (~P18(a1,x1005571)),
% 70.74/70.75 inference(rename_variables,[],[39])).
% 70.74/70.75 cnf(100568,plain,
% 70.74/70.75 (P22(a5,x1005681,a5)),
% 70.74/70.75 inference(scs_inference,[],[38,56959,58967,26,3,93208,39,100557,47,44163,140,196,437,100553])).
% 70.74/70.75 cnf(103973,plain,
% 70.74/70.75 (~P18(a1,x1039731)),
% 70.74/70.75 inference(rename_variables,[],[39])).
% 70.74/70.75 cnf(103987,plain,
% 70.74/70.75 (P30(x1039871,a5,a5)),
% 70.74/70.75 inference(scs_inference,[],[522,93334,93851,93208,39,103973,93559,1,50913,28,26,4,47,140,44163,437,196,155,353])).
% 70.74/70.75 cnf(104016,plain,
% 70.74/70.75 (~P18(a1,x1040161)),
% 70.74/70.75 inference(rename_variables,[],[39])).
% 70.74/70.75 cnf(104028,plain,
% 70.74/70.75 (P31(x1040281,a5,a5)),
% 70.74/70.75 inference(scs_inference,[],[103987,100568,56932,93208,39,104016,28,26,3,44163,47,140,196,437,339])).
% 70.74/70.75 cnf(104039,plain,
% 70.74/70.75 (~P18(a1,x1040391)),
% 70.74/70.75 inference(rename_variables,[],[39])).
% 70.74/70.75 cnf(104049,plain,
% 70.74/70.75 (P28(x1040491,a5)),
% 70.74/70.75 inference(scs_inference,[],[104028,71532,56924,93208,39,104039,28,26,4,44163,47,140,196,437,211])).
% 70.74/70.75 cnf(104061,plain,
% 70.74/70.75 (~P18(a1,x1040611)),
% 70.74/70.75 inference(rename_variables,[],[39])).
% 70.74/70.75 cnf(104079,plain,
% 70.74/70.75 (P42(x1040791,a5,x1040791)),
% 70.74/70.75 inference(scs_inference,[],[104049,56899,103987,56965,93208,39,104061,93559,28,26,3,44163,47,140,196,437,211,245,248])).
% 70.74/70.75 cnf(104090,plain,
% 70.74/70.75 (P32(a5,a5,x1040901)),
% 70.74/70.75 inference(scs_inference,[],[104079,39,26,4,3,44163,47,140,275])).
% 70.74/70.75 cnf(104189,plain,
% 70.74/70.75 (~P18(a1,x1041891)),
% 70.74/70.75 inference(rename_variables,[],[39])).
% 70.74/70.75 cnf(104201,plain,
% 70.74/70.75 ($false),
% 70.74/70.75 inference(scs_inference,[],[104090,93188,93391,62951,103987,93208,39,104189,93278,65636,28,26,3,44163,47,140,196,437,361]),
% 70.74/70.75 ['proof']).
% 70.91/70.81 % SZS output end Proof
% 70.91/70.81 % Total time :69.970000s
%------------------------------------------------------------------------------