%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MED009+1 : TPTP v8.2.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n025.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 11:44:44 EDT 2024
% Result : Theorem 116.55s 116.57s
% Output : CNFRefutation 116.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : MED009+1 : TPTP v8.2.0. Released v3.2.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.32 % Computer : n025.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 : Sat Jun 22 18:53:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.55 start to proof:theBenchmark
% 116.55/116.55 %-------------------------------------------
% 116.55/116.55 % File :CSE---1.7
% 116.55/116.55 % Problem :theBenchmark
% 116.55/116.55 % Transform :cnf
% 116.55/116.55 % Format :tptp:raw
% 116.55/116.55 % Command :java -jar mcs_scs.jar %d %s
% 116.55/116.55
% 116.55/116.55 % Result :Theorem 115.920000s
% 116.55/116.55 % Output :CNFRefutation 115.920000s
% 116.55/116.55 %-------------------------------------------
% 116.55/116.57 %------------------------------------------------------------------------------
% 116.55/116.57 % File : MED009+1 : TPTP v8.2.0. Released v3.2.0.
% 116.55/116.57 % Domain : Medicine
% 116.55/116.57 % Problem : Unsuccessful s1-qige27 treatment - next step
% 116.55/116.57 % Version : [HLB05] axioms : Especial.
% 116.55/116.57 % English : After unsuccessful treatment with single oral anti-diabetic for
% 116.55/116.57 % patients with QI greater equal than 27 medical management moves
% 116.55/116.57 % to next step.
% 116.55/116.57
% 116.55/116.57 % Refs : [HLB05] Hommersom et al. (2005), Automated Theorem Proving for
% 116.55/116.57 % : [Hom06] Hommersom (2006), Email to G. Sutcliffe
% 116.55/116.57 % Source : [Hom06]
% 116.55/116.57 % Names :
% 116.55/116.57
% 116.55/116.57 % Status : Theorem
% 116.55/116.57 % Rating : 0.00 v8.2.0, 0.07 v8.1.0, 0.14 v7.5.0, 0.29 v7.4.0, 0.12 v7.3.0, 0.14 v7.2.0, 0.17 v7.1.0, 0.00 v7.0.0, 0.07 v6.3.0, 0.08 v6.2.0, 0.18 v6.1.0, 0.36 v6.0.0, 0.25 v5.5.0, 0.54 v5.4.0, 0.52 v5.3.0, 0.57 v5.2.0, 0.36 v5.0.0, 0.35 v4.1.0, 0.44 v4.0.1, 0.47 v4.0.0, 0.50 v3.7.0, 0.33 v3.5.0, 0.25 v3.4.0, 0.33 v3.3.0, 0.67 v3.2.0
% 116.55/116.57 % Syntax : Number of formulae : 41 ( 1 unt; 0 def)
% 116.55/116.57 % Number of atoms : 201 ( 0 equ)
% 116.55/116.57 % Maximal formula atoms : 30 ( 4 avg)
% 116.55/116.57 % Number of connectives : 245 ( 85 ~; 34 |; 51 &)
% 116.55/116.57 % ( 0 <=>; 75 =>; 0 <=; 0 <~>)
% 116.55/116.57 % Maximal formula depth : 12 ( 6 avg)
% 116.55/116.57 % Maximal term depth : 1 ( 1 avg)
% 116.55/116.57 % Number of predicates : 20 ( 20 usr; 0 prp; 1-2 aty)
% 116.55/116.57 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% 116.55/116.57 % Number of variables : 96 ( 92 !; 4 ?)
% 116.55/116.57 % SPC : FOF_THM_RFO_NEQ
% 116.55/116.57
% 116.55/116.57 % Comments :
% 116.55/116.57 %------------------------------------------------------------------------------
% 116.55/116.57 include('Axioms/MED001+0.ax').
% 116.55/116.57 include('Axioms/MED001+1.ax').
% 116.55/116.57 %------------------------------------------------------------------------------
% 116.55/116.57 fof(transs1s2_qige27,conjecture,
% 116.55/116.57 ( ( s1(n0)
% 116.55/116.57 & ! [X0] :
% 116.55/116.57 ( gt(n0,X0)
% 116.55/116.57 => conditionhyper(X0) )
% 116.55/116.57 & ~ bcapacitysn(n0)
% 116.55/116.57 & ~ qilt27(n0) )
% 116.55/116.57 => ? [X0] :
% 116.55/116.57 ( ~ gt(n0,X0)
% 116.55/116.57 & s2(X0)
% 116.55/116.57 & ! [X1] :
% 116.55/116.57 ( gt(X0,X1)
% 116.55/116.57 => conditionhyper(X1) )
% 116.55/116.57 & ( bcapacityne(X0)
% 116.55/116.57 | bcapacityex(X0) ) ) ) ).
% 116.55/116.57
% 116.55/116.57 %------------------------------------------------------------------------------
% 116.55/116.57 %-------------------------------------------
% 116.55/116.57 % Proof found
% 116.55/116.57 % SZS status Theorem for theBenchmark
% 116.55/116.57 % SZS output start Proof
% 116.55/116.58 %ClaNum:167(EqnAxiom:0)
% 116.55/116.58 %VarNum:684(SingletonVarNum:221)
% 116.55/116.58 %MaxLitNum:8
% 116.55/116.58 %MaxfuncDepth:1
% 116.55/116.58 %SharedTerms:4
% 116.55/116.58 %goalClause: 1 2 3 36 67 68 72 73
% 116.55/116.58 %singleGoalClaCount:3
% 116.55/116.58 [1]P1(a1)
% 116.55/116.58 [2]~P2(a1)
% 116.55/116.58 [3]~P5(a1)
% 116.55/116.58 [4]~P6(x41,x41)
% 116.55/116.58 [5]~P18(x51)+P7(x51)
% 116.55/116.58 [6]~P19(x61)+P13(x61)
% 116.55/116.58 [7]~P19(x71)+P8(x71)
% 116.55/116.58 [8]~P7(x81)+P18(x81)
% 116.55/116.58 [11]~P4(x111)+~P3(x111)
% 116.55/116.58 [12]~P2(x121)+~P3(x121)
% 116.55/116.58 [13]~P2(x131)+~P4(x131)
% 116.55/116.58 [14]~P11(x141)+~P9(x141)
% 116.55/116.58 [15]~P12(x151)+~P9(x151)
% 116.55/116.58 [16]~P12(x161)+~P11(x161)
% 116.55/116.58 [17]~P1(x171)+~P16(x171)
% 116.55/116.58 [18]~P19(x181)+~P16(x181)
% 116.55/116.58 [19]~P18(x191)+~P16(x191)
% 116.55/116.58 [20]~P19(x201)+~P1(x201)
% 116.55/116.58 [21]~P18(x211)+~P1(x211)
% 116.55/116.58 [22]~P18(x221)+~P19(x221)
% 116.55/116.58 [36]P9(x361)+~P6(a1,x361)
% 116.55/116.58 [35]~P4(x351)+~P10(f2(x351))
% 116.55/116.58 [58]~P4(x581)+~P6(x581,f2(x581))
% 116.55/116.58 [9]P4(x91)+P2(x91)+P3(x91)
% 116.55/116.58 [10]P11(x101)+P12(x101)+P9(x101)
% 116.55/116.58 [23]P2(x231)+~P14(x231)+P3(x231)
% 116.55/116.58 [24]P5(x241)+~P1(x241)+P8(x241)
% 116.55/116.58 [26]~P5(x261)+~P1(x261)+P13(x261)
% 116.55/116.58 [37]P14(x371)+P4(x371)+~P12(f3(x371))
% 116.55/116.58 [62]P14(x621)+P4(x621)+~P6(x621,f3(x621))
% 116.55/116.58 [34]P17(x341)+P20(x341)+P6(x342,x341)
% 116.55/116.58 [38]~P20(x382)+~P17(x382)+P6(x381,x382)
% 116.55/116.58 [39]P8(x391)+P6(x392,x391)+P17(f11(x392))
% 116.55/116.58 [43]P7(x431)+P6(x432,x431)+~P20(f9(x432))
% 116.55/116.58 [44]P7(x441)+P6(x442,x441)+~P21(f10(x442))
% 116.55/116.58 [45]P20(x451)+P6(x452,x451)+~P7(f12(x452))
% 116.55/116.58 [46]P21(x461)+P6(x462,x461)+~P7(f12(x462))
% 116.55/116.58 [47]P13(x471)+P6(x472,x471)+~P10(f2(x472))
% 116.55/116.58 [56]~P17(x562)+P6(x561,x562)+~P8(f16(x561))
% 116.55/116.58 [76]P7(x761)+P6(x762,x761)+~P6(x762,f9(x762))
% 116.55/116.58 [77]P7(x771)+P6(x772,x771)+~P6(x772,f10(x772))
% 116.55/116.58 [78]P20(x781)+P6(x782,x781)+~P6(x782,f12(x782))
% 116.55/116.58 [79]P21(x791)+P6(x792,x791)+~P6(x792,f12(x792))
% 116.55/116.58 [80]P13(x801)+P6(x802,x801)+~P6(x802,f2(x802))
% 116.55/116.58 [81]P8(x811)+P6(x812,x811)+~P6(x812,f11(x812))
% 116.55/116.58 [87]~P17(x872)+P6(x871,x872)+~P6(x871,f16(x871))
% 116.55/116.58 [102]~P6(x1021,x1023)+P6(x1021,x1022)+~P6(x1023,x1022)
% 116.55/116.58 [25]P1(x251)+P19(x251)+P18(x251)+P16(x251)
% 116.55/116.58 [29]P19(x291)+P18(x291)+~P13(x291)+P1(x291)
% 116.55/116.58 [30]P19(x301)+P18(x301)+~P8(x301)+P1(x301)
% 116.55/116.58 [31]P18(x311)+P15(x311)+~P13(x311)+P19(x311)
% 116.55/116.58 [33]P18(x331)+~P8(x331)+~P5(x331)+P19(x331)
% 116.55/116.58 [67]~P3(x671)+~P19(x671)+P6(a1,x671)+~P9(f18(x671))
% 116.55/116.58 [68]~P4(x681)+~P19(x681)+P6(a1,x681)+~P9(f18(x681))
% 116.55/116.58 [72]~P3(x721)+~P19(x721)+P6(x721,f18(x721))+P6(a1,x721)
% 116.55/116.58 [73]~P4(x731)+~P19(x731)+P6(x731,f18(x731))+P6(a1,x731)
% 116.55/116.58 [40]P6(x401,x402)+~P14(x401)+P2(x401)+P10(x402)
% 116.55/116.58 [57]~P14(x571)+~P6(x571,x572)+P2(x571)+P9(x572)
% 116.55/116.58 [48]~P19(x482)+P12(x481)+P6(x482,x481)+P4(f13(x482))
% 116.55/116.58 [49]~P16(x492)+P12(x491)+P6(x492,x491)+P1(f14(x492))
% 116.55/116.58 [50]~P1(x502)+P12(x501)+P6(x502,x501)+P19(f15(x502))
% 116.55/116.58 [51]~P19(x512)+P12(x511)+P6(x512,x511)+P18(f13(x512))
% 116.55/116.58 [59]P6(x591,x592)+P4(x591)+P10(x592)+~P13(f17(x591))
% 116.55/116.58 [60]P6(x602,x601)+P20(x601)+P14(x602)+~P12(f3(x602))
% 116.55/116.58 [61]P6(x612,x611)+P21(x611)+P14(x612)+~P12(f3(x612))
% 116.55/116.58 [74]~P6(x742,x741)+P9(x741)+P14(x742)+~P12(f3(x742))
% 116.55/116.58 [88]P6(x881,x882)+P4(x881)+P10(x882)+~P6(x881,f17(x881))
% 116.55/116.58 [89]P6(x892,x891)+P20(x891)+P14(x892)+~P6(x892,f3(x892))
% 116.55/116.58 [90]P6(x902,x901)+P21(x901)+P14(x902)+~P6(x902,f3(x902))
% 116.55/116.58 [98]~P16(x982)+P12(x981)+P6(x982,x981)+~P6(x982,f14(x982))
% 116.55/116.58 [99]~P1(x992)+P12(x991)+P6(x992,x991)+~P6(x992,f15(x992))
% 116.55/116.58 [100]~P19(x1002)+P12(x1001)+P6(x1002,x1001)+~P6(x1002,f13(x1002))
% 116.55/116.58 [112]~P6(x1122,x1121)+P9(x1121)+P14(x1122)+~P6(x1122,f3(x1122))
% 116.55/116.58 [53]P6(x531,x532)+~P5(x531)+~P14(x531)+P3(x531)+P10(x532)
% 116.55/116.58 [54]P5(x541)+~P17(x542)+~P14(x541)+P3(x541)+P6(x541,x542)
% 116.55/116.58 [65]P5(x651)+~P14(x651)+~P6(x651,x652)+P3(x651)+P9(x652)
% 116.55/116.58 [69]~P5(x691)+~P14(x691)+~P6(x691,x692)+P3(x691)+P9(x692)
% 116.55/116.58 [71]~P1(x712)+P12(x711)+P6(x712,x711)+P3(f15(x712))+P4(f15(x712))
% 116.55/116.58 [109]~P16(x1093)+P9(x1091)+P6(x1093,x1092)+P12(x1092)+~P6(f14(x1093),x1091)
% 116.55/116.58 [110]~P1(x1103)+P9(x1101)+P6(x1103,x1102)+P12(x1102)+~P6(f15(x1103),x1101)
% 116.55/116.58 [111]~P19(x1113)+P9(x1111)+P6(x1113,x1112)+P12(x1112)+~P6(f13(x1113),x1111)
% 116.55/116.58 [97]P6(x972,x971)+~P2(x972)+P12(x971)+P5(x972)+P17(f19(x972))+~P9(f22(x972))
% 116.55/116.58 [108]P6(x1082,x1081)+~P2(x1082)+P12(x1081)+P5(x1082)+P6(x1082,f22(x1082))+P17(f19(x1082))
% 116.55/116.58 [118]~P2(x1182)+~P5(x1182)+P12(x1181)+P6(x1182,x1181)+~P9(f20(x1182))+~P10(f21(x1182))
% 116.55/116.58 [120]~P3(x1202)+P12(x1201)+P6(x1202,x1201)+P17(f23(x1202))+~P9(f4(x1202))+~P10(f5(x1202))
% 116.55/116.58 [121]~P2(x1212)+~P5(x1212)+P12(x1211)+P6(x1212,x1211)+P6(x1212,f20(x1212))+~P10(f21(x1212))
% 116.55/116.58 [127]~P3(x1272)+P12(x1271)+P6(x1272,x1271)+P6(x1272,f4(x1272))+P17(f23(x1272))+~P10(f5(x1272))
% 116.55/116.58 [130]~P3(x1302)+P12(x1301)+P6(x1302,x1301)+~P9(f4(x1302))+~P21(f24(x1302))+~P10(f5(x1302))
% 116.55/116.58 [134]P6(x1342,x1341)+~P2(x1342)+P12(x1341)+P5(x1342)+~P6(x1342,f19(x1342))+~P9(f22(x1342))
% 116.55/116.58 [135]~P3(x1352)+P12(x1351)+P6(x1352,x1351)+P6(x1352,f4(x1352))+~P21(f24(x1352))+~P10(f5(x1352))
% 116.55/116.58 [140]~P2(x1402)+~P5(x1402)+P12(x1401)+P6(x1402,x1401)+~P6(x1402,f21(x1402))+~P9(f20(x1402))
% 116.55/116.58 [142]P6(x1422,x1421)+~P2(x1422)+P12(x1421)+P5(x1422)+P6(x1422,f22(x1422))+~P6(x1422,f19(x1422))
% 116.55/116.58 [144]~P3(x1442)+P12(x1441)+P6(x1442,x1441)+~P6(x1442,f5(x1442))+P17(f23(x1442))+~P9(f4(x1442))
% 116.55/116.58 [145]~P2(x1452)+~P5(x1452)+P12(x1451)+P6(x1452,x1451)+P6(x1452,f20(x1452))+~P6(x1452,f21(x1452))
% 116.55/116.58 [148]~P3(x1482)+P12(x1481)+P6(x1482,x1481)+P6(x1482,f4(x1482))+~P6(x1482,f5(x1482))+P17(f23(x1482))
% 116.55/116.58 [149]~P3(x1492)+P12(x1491)+P6(x1492,x1491)+~P6(x1492,f5(x1492))+~P9(f4(x1492))+~P21(f24(x1492))
% 116.55/116.58 [150]~P3(x1502)+P12(x1501)+P6(x1502,x1501)+~P6(x1502,f23(x1502))+~P9(f4(x1502))+~P10(f5(x1502))
% 116.55/116.58 [151]~P3(x1512)+P12(x1511)+P6(x1512,x1511)+~P6(x1512,f24(x1512))+~P9(f4(x1512))+~P10(f5(x1512))
% 116.55/116.58 [153]~P3(x1532)+P12(x1531)+P6(x1532,x1531)+P6(x1532,f4(x1532))+~P6(x1532,f5(x1532))+~P21(f24(x1532))
% 116.55/116.58 [154]~P3(x1542)+P12(x1541)+P6(x1542,x1541)+P6(x1542,f4(x1542))+~P6(x1542,f23(x1542))+~P10(f5(x1542))
% 116.55/116.58 [155]~P3(x1552)+P12(x1551)+P6(x1552,x1551)+P6(x1552,f4(x1552))+~P6(x1552,f24(x1552))+~P10(f5(x1552))
% 116.55/116.59 [162]~P3(x1622)+P12(x1621)+P6(x1622,x1621)+~P6(x1622,f23(x1622))+~P6(x1622,f5(x1622))+~P9(f4(x1622))
% 116.55/116.59 [163]~P3(x1632)+P12(x1631)+P6(x1632,x1631)+~P6(x1632,f24(x1632))+~P6(x1632,f5(x1632))+~P9(f4(x1632))
% 116.55/116.59 [164]~P3(x1642)+P12(x1641)+P6(x1642,x1641)+P6(x1642,f4(x1642))+~P6(x1642,f23(x1642))+~P6(x1642,f5(x1642))
% 116.55/116.59 [165]~P3(x1652)+P12(x1651)+P6(x1652,x1651)+P6(x1652,f4(x1652))+~P6(x1652,f24(x1652))+~P6(x1652,f5(x1652))
% 116.55/116.59 [82]P6(x821,x822)+~P17(x823)+~P14(x821)+P3(x821)+P6(x821,x823)+P10(x822)
% 116.55/116.59 [83]P6(x831,x832)+~P17(x833)+~P14(x831)+P2(x831)+P6(x831,x833)+P21(x832)
% 116.55/116.59 [85]P6(x853,x852)+~P5(x853)+~P14(x853)+P10(x851)+P6(x853,x851)+P10(x852)
% 116.55/116.59 [86]P6(x862,x861)+~P17(x863)+~P14(x862)+P10(x861)+P6(x862,x863)+P5(x862)
% 116.55/116.59 [113]~P14(x1131)+~P6(x1131,x1132)+~P6(x1131,x1133)+P3(x1131)+P9(x1132)+P9(x1133)
% 116.55/116.59 [116]~P14(x1163)+~P6(x1163,x1161)+~P6(x1163,x1162)+P9(x1161)+P9(x1162)+P5(x1163)
% 116.55/116.59 [119]~P14(x1193)+~P6(x1193,x1191)+~P6(x1193,x1192)+P9(x1191)+P9(x1192)+~P5(x1193)
% 116.55/116.59 [138]P12(x1381)+~P4(x1382)+P11(x1381)+P6(x1382,x1381)+~P9(f6(x1382))+~P20(f7(x1382))+~P21(f8(x1382))
% 116.55/116.59 [143]P12(x1431)+~P4(x1432)+P11(x1431)+P6(x1432,x1431)+P6(x1432,f6(x1432))+~P20(f7(x1432))+~P21(f8(x1432))
% 116.55/116.59 [156]P12(x1561)+~P4(x1562)+P11(x1561)+P6(x1562,x1561)+~P6(x1562,f8(x1562))+~P9(f6(x1562))+~P20(f7(x1562))
% 116.55/116.59 [157]P12(x1571)+~P4(x1572)+P11(x1571)+P6(x1572,x1571)+~P6(x1572,f7(x1572))+~P9(f6(x1572))+~P21(f8(x1572))
% 116.55/116.59 [159]P12(x1591)+~P4(x1592)+P11(x1591)+P6(x1592,x1591)+P6(x1592,f6(x1592))+~P6(x1592,f8(x1592))+~P20(f7(x1592))
% 116.55/116.59 [160]P12(x1601)+~P4(x1602)+P11(x1601)+P6(x1602,x1601)+P6(x1602,f6(x1602))+~P6(x1602,f7(x1602))+~P21(f8(x1602))
% 116.55/116.59 [166]P12(x1661)+~P4(x1662)+P11(x1661)+P6(x1662,x1661)+~P6(x1662,f7(x1662))+~P6(x1662,f8(x1662))+~P9(f6(x1662))
% 116.55/116.59 [167]P12(x1671)+~P4(x1672)+P11(x1671)+P6(x1672,x1671)+P6(x1672,f6(x1672))+~P6(x1672,f7(x1672))+~P6(x1672,f8(x1672))
% 116.55/116.59 [117]P6(x1173,x1172)+~P17(x1174)+~P14(x1173)+P10(x1171)+P6(x1173,x1171)+P10(x1172)+P6(x1173,x1174)
% 116.55/116.59 [147]~P6(x1474,x1471)+~P6(x1474,x1472)+~P6(x1474,x1473)+P9(x1471)+P9(x1472)+P9(x1473)+~P14(x1474)
% 116.55/116.59 [126]P6(x1262,x1261)+~P17(x1263)+~P17(x1264)+~P14(x1262)+P21(x1261)+P6(x1262,x1263)+P5(x1262)+P6(x1262,x1264)
% 116.55/116.59 %EqnAxiom
% 116.55/116.59
% 116.55/116.59 %-------------------------------------------
% 116.55/116.60 cnf(170,plain,
% 116.55/116.60 (~P18(a1)),
% 116.55/116.60 inference(scs_inference,[],[1,20,21])).
% 116.55/116.60 cnf(196,plain,
% 116.55/116.60 (~P18(f12(x1961))+P20(x1961)),
% 116.55/116.60 inference(scs_inference,[],[4,5,45])).
% 116.55/116.60 cnf(228,plain,
% 116.55/116.60 (~P19(f16(x2281))+~P17(x2281)),
% 116.55/116.60 inference(scs_inference,[],[4,7,56])).
% 116.55/116.60 cnf(1065,plain,
% 116.55/116.60 (~P6(a1,f10(a1))),
% 116.55/116.60 inference(scs_inference,[],[4,170,77,8])).
% 116.55/116.60 cnf(1860,plain,
% 116.55/116.60 (~P18(f12(a1))+P21(f10(a1))),
% 116.55/116.60 inference(scs_inference,[],[1065,5,46])).
% 116.55/116.60 cnf(1876,plain,
% 116.55/116.60 (~P7(f12(a1))+P21(f10(a1))),
% 116.55/116.60 inference(scs_inference,[],[1860,8])).
% 116.55/116.60 cnf(1892,plain,
% 116.55/116.60 (P21(f10(a1))+~P20(f9(f12(a1)))),
% 116.55/116.60 inference(scs_inference,[],[4,1876,43])).
% 116.55/116.60 cnf(1939,plain,
% 116.55/116.60 (P7(f13(x19391))+~P19(x19391)+P12(x19391)),
% 116.55/116.60 inference(scs_inference,[],[4,5,51])).
% 116.55/116.60 cnf(2018,plain,
% 116.55/116.60 (~P18(f12(x20181))+P21(x20181)),
% 116.55/116.60 inference(scs_inference,[],[4,5,46])).
% 116.55/116.60 cnf(3876,plain,
% 116.55/116.60 (~P19(x38761)+~P7(x38761)),
% 116.55/116.60 inference(scs_inference,[],[8,22])).
% 116.55/116.60 cnf(3939,plain,
% 116.55/116.60 (~P20(f9(a1))),
% 116.55/116.60 inference(scs_inference,[],[170,4,8,43])).
% 116.55/116.60 cnf(3955,plain,
% 116.55/116.60 (P21(x39551)+~P7(f12(x39551))),
% 116.55/116.60 inference(scs_inference,[],[8,2018])).
% 116.55/116.60 cnf(4020,plain,
% 116.55/116.60 (~P21(f10(a1))),
% 116.55/116.60 inference(scs_inference,[],[170,4,8,44])).
% 116.55/116.60 cnf(4022,plain,
% 116.55/116.60 (~P7(f12(a1))),
% 116.55/116.60 inference(scs_inference,[],[4020,1876])).
% 116.55/116.60 cnf(4023,plain,
% 116.55/116.60 (~P20(f9(f12(a1)))),
% 116.55/116.60 inference(scs_inference,[],[4020,1892])).
% 116.55/116.60 cnf(4240,plain,
% 116.55/116.60 (~P7(f12(f9(f12(a1))))),
% 116.55/116.60 inference(scs_inference,[],[4023,8,196])).
% 116.55/116.60 cnf(4256,plain,
% 116.55/116.60 (~P6(a1,f9(a1))),
% 116.55/116.60 inference(scs_inference,[],[170,4,8,76])).
% 116.55/116.60 cnf(6107,plain,
% 116.55/116.60 (~P3(f13(x61071))+~P19(x61071)+P12(x61071)),
% 116.55/116.60 inference(scs_inference,[],[4,11,48])).
% 116.55/116.60 cnf(7234,plain,
% 116.55/116.60 (P17(f9(a1))),
% 116.55/116.60 inference(scs_inference,[],[3939,4256,34])).
% 116.55/116.60 cnf(7237,plain,
% 116.55/116.60 (P17(f9(f12(a1)))),
% 116.55/116.60 inference(scs_inference,[],[4023,4,34])).
% 116.55/116.60 cnf(10654,plain,
% 116.55/116.60 (~P14(a1)),
% 116.55/116.60 inference(scs_inference,[],[2,1065,7234,4256,4020,83])).
% 116.55/116.60 cnf(33040,plain,
% 116.55/116.60 (~P12(f3(a1))),
% 116.55/116.60 inference(scs_inference,[],[10654,3939,4256,78,60])).
% 116.55/116.60 cnf(33042,plain,
% 116.55/116.60 (~P6(a1,f3(a1))),
% 116.55/116.60 inference(scs_inference,[],[10654,4020,3939,1065,4256,78,60,90])).
% 116.55/116.60 cnf(33044,plain,
% 116.55/116.60 (~P6(a1,f15(a1))),
% 116.55/116.60 inference(scs_inference,[],[1,10654,4020,3939,1065,4256,78,60,90,99])).
% 116.55/116.60 cnf(33048,plain,
% 116.55/116.60 (~P8(f16(a1))),
% 116.55/116.60 inference(scs_inference,[],[1,10654,4020,3939,7234,1065,4256,78,60,90,99,39,56])).
% 116.55/116.60 cnf(33050,plain,
% 116.55/116.60 (~P6(a1,f16(a1))),
% 116.55/116.60 inference(scs_inference,[],[1,10654,4020,3939,7234,1065,4256,78,60,90,99,39,56,87])).
% 116.55/116.60 cnf(33052,plain,
% 116.55/116.60 (P19(f15(a1))),
% 116.55/116.60 inference(scs_inference,[],[1,10654,4020,3939,7234,1065,4256,78,60,90,99,39,56,87,50])).
% 116.55/116.60 cnf(33060,plain,
% 116.55/116.60 (~P7(f15(a1))),
% 116.55/116.60 inference(scs_inference,[],[1,10654,4020,3939,7234,1065,4256,78,60,90,99,39,56,87,50,6,7,18,3876])).
% 116.55/116.60 cnf(33066,plain,
% 116.55/116.60 (~P6(a1,f11(a1))),
% 116.55/116.60 inference(scs_inference,[],[33048,33050,81])).
% 116.55/116.60 cnf(33068,plain,
% 116.55/116.60 (P17(f11(a1))),
% 116.55/116.60 inference(scs_inference,[],[33048,33050,81,39])).
% 116.55/116.60 cnf(33076,plain,
% 116.55/116.60 (~P20(f11(a1))),
% 116.55/116.60 inference(scs_inference,[],[33068,33066,80,38])).
% 116.55/116.60 cnf(33078,plain,
% 116.55/116.60 (P9(x330781)+~P6(f15(a1),x330781)),
% 116.55/116.60 inference(scs_inference,[],[1,33068,33066,33040,33042,80,38,110])).
% 116.55/116.60 cnf(33093,plain,
% 116.55/116.60 (P4(f15(a1))+P3(f15(a1))),
% 116.55/116.60 inference(scs_inference,[],[1,33040,33042,71])).
% 116.55/116.60 cnf(33146,plain,
% 116.55/116.60 (~P6(x331461,x331462)+~P6(x331462,x331461)),
% 116.55/116.60 inference(scs_inference,[],[4,102])).
% 116.55/116.60 cnf(33179,plain,
% 116.55/116.60 (~P11(x331791)+~P6(f15(a1),x331791)),
% 116.55/116.60 inference(scs_inference,[],[33078,14])).
% 116.55/116.60 cnf(34632,plain,
% 116.55/116.60 (~P2(f15(a1))+P4(f15(a1))),
% 116.55/116.60 inference(scs_inference,[],[12,33093])).
% 116.55/116.60 cnf(34714,plain,
% 116.55/116.60 (~P2(f15(a1))),
% 116.55/116.60 inference(scs_inference,[],[13,34632])).
% 116.55/116.60 cnf(35281,plain,
% 116.55/116.60 (~P12(x352811)+~P6(f15(a1),x352811)),
% 116.55/116.60 inference(scs_inference,[],[33040,1,33042,15,110])).
% 116.55/116.60 cnf(36435,plain,
% 116.55/116.60 (~P20(f9(f15(a1)))),
% 116.55/116.60 inference(scs_inference,[],[33052,4,3876,43])).
% 116.55/116.60 cnf(36465,plain,
% 116.55/116.60 (~P21(f10(f15(a1)))),
% 116.55/116.60 inference(scs_inference,[],[33052,4,3876,44])).
% 116.55/116.60 cnf(36490,plain,
% 116.55/116.60 (~P6(f15(a1),f9(f15(a1)))),
% 116.55/116.60 inference(scs_inference,[],[33052,4,3876,76])).
% 116.55/116.60 cnf(36585,plain,
% 116.55/116.60 (~P6(f15(a1),f10(f15(a1)))),
% 116.55/116.60 inference(scs_inference,[],[33052,4,3876,77])).
% 116.55/116.60 cnf(37271,plain,
% 116.55/116.60 (~P7(f12(f11(a1)))),
% 116.55/116.60 inference(scs_inference,[],[33076,196,8])).
% 116.55/116.60 cnf(37295,plain,
% 116.55/116.60 (~P18(f12(f9(f15(a1))))),
% 116.55/116.60 inference(scs_inference,[],[4,33060,196,43])).
% 116.55/116.60 cnf(37870,plain,
% 116.55/116.60 (~P20(f9(f12(f10(a1))))),
% 116.55/116.60 inference(scs_inference,[],[4020,4,3955,43])).
% 116.55/116.60 cnf(37966,plain,
% 116.55/116.60 (~P21(f10(f12(f10(a1))))),
% 116.55/116.60 inference(scs_inference,[],[4020,4,3955,44])).
% 116.55/116.60 cnf(37985,plain,
% 116.55/116.60 (~P6(f12(f10(a1)),f9(f12(f10(a1))))),
% 116.55/116.60 inference(scs_inference,[],[4020,4,3955,76])).
% 116.55/116.60 cnf(38011,plain,
% 116.55/116.60 (~P7(f12(f10(f12(a1))))),
% 116.55/116.60 inference(scs_inference,[],[4022,4,3955,44])).
% 116.55/116.60 cnf(42053,plain,
% 116.55/116.60 (P4(f15(a1))+P6(f15(a1),f18(f15(a1)))),
% 116.55/116.60 inference(scs_inference,[],[33052,33044,33093,72])).
% 116.55/116.60 cnf(42181,plain,
% 116.55/116.60 (P4(f15(a1))+~P9(f18(f15(a1)))),
% 116.55/116.60 inference(scs_inference,[],[33052,33044,33093,67])).
% 116.55/116.60 cnf(45506,plain,
% 116.55/116.60 (~P18(f12(f10(f15(a1))))),
% 116.55/116.60 inference(scs_inference,[],[36465,38011,7237,228,5,2018])).
% 116.55/116.60 cnf(45508,plain,
% 116.55/116.60 (~P18(f12(f9(f12(f10(a1)))))),
% 116.55/116.60 inference(scs_inference,[],[36465,37870,38011,7237,228,5,2018,196])).
% 116.55/116.60 cnf(45510,plain,
% 116.55/116.60 (~P7(f12(f9(f15(a1))))),
% 116.55/116.60 inference(scs_inference,[],[36465,37295,37870,38011,7237,228,5,2018,196,8])).
% 116.55/116.60 cnf(45512,plain,
% 116.55/116.60 (~P6(f12(f11(a1)),f9(f12(f11(a1))))),
% 116.55/116.60 inference(scs_inference,[],[36465,37271,37295,37870,38011,7237,4,228,5,2018,196,8,76])).
% 116.55/116.60 cnf(45513,plain,
% 116.55/116.60 (~P6(x455131,x455131)),
% 116.55/116.60 inference(rename_variables,[],[4])).
% 116.55/116.60 cnf(45515,plain,
% 116.55/116.60 (~P21(f10(f12(f11(a1))))),
% 116.55/116.60 inference(scs_inference,[],[36465,37271,37295,37870,38011,7237,4,45513,228,5,2018,196,8,76,44])).
% 116.55/116.60 cnf(45516,plain,
% 116.55/116.60 (~P6(x455161,x455161)),
% 116.55/116.60 inference(rename_variables,[],[4])).
% 116.55/116.60 cnf(45520,plain,
% 116.55/116.60 (~P7(f12(f15(a1)))),
% 116.55/116.60 inference(scs_inference,[],[36585,36465,37271,37295,37870,38011,7237,4,45513,228,5,2018,196,8,76,44,79,46])).
% 116.55/116.60 cnf(45522,plain,
% 116.55/116.60 (~P6(f9(f12(a1)),f16(f9(f12(a1))))),
% 116.55/116.60 inference(scs_inference,[],[36585,36465,37271,37295,37870,38011,7237,4,45513,45516,228,5,2018,196,8,76,44,79,46,87])).
% 116.55/116.60 cnf(45523,plain,
% 116.55/116.60 (~P6(x455231,x455231)),
% 116.55/116.60 inference(rename_variables,[],[4])).
% 116.55/116.60 cnf(45525,plain,
% 116.55/116.60 (P17(f9(f15(a1)))),
% 116.55/116.60 inference(scs_inference,[],[36490,36585,36435,36465,37271,37295,37870,38011,7237,4,45513,45516,228,5,2018,196,8,76,44,79,46,87,34])).
% 116.55/116.60 cnf(45529,plain,
% 116.55/116.60 (~P20(f9(f12(f11(a1))))),
% 116.55/116.60 inference(scs_inference,[],[36490,36585,36435,36465,37271,37295,37870,38011,7237,33052,4,45513,45516,45523,228,5,2018,196,8,76,44,79,46,87,34,6107,43])).
% 116.55/116.60 cnf(45530,plain,
% 116.55/116.60 (~P6(x455301,x455301)),
% 116.55/116.60 inference(rename_variables,[],[4])).
% 116.55/116.60 cnf(45532,plain,
% 116.55/116.60 (~P7(f12(f12(f10(a1))))),
% 116.55/116.60 inference(scs_inference,[],[36490,36585,36435,36465,37271,37295,37870,38011,37985,7237,33052,4,45513,45516,45523,228,5,2018,196,8,76,44,79,46,87,34,6107,43,45])).
% 116.55/116.60 cnf(45534,plain,
% 116.55/116.60 (~P6(f12(f11(a1)),f10(f12(f11(a1))))),
% 116.55/116.60 inference(scs_inference,[],[36490,36585,36435,36465,37271,37295,37870,38011,37985,7237,33052,4,45513,45516,45523,45530,228,5,2018,196,8,76,44,79,46,87,34,6107,43,45,77])).
% 116.55/116.60 cnf(45535,plain,
% 116.55/116.60 (~P6(x455351,x455351)),
% 116.55/116.60 inference(rename_variables,[],[4])).
% 116.55/116.60 cnf(45539,plain,
% 116.55/116.60 (~P8(f16(f15(a1)))),
% 116.55/116.60 inference(scs_inference,[],[36490,36585,36435,36465,37271,37295,37870,38011,37985,7237,33052,4,45513,45516,45523,45530,228,5,2018,196,8,76,44,79,46,87,34,6107,43,45,77,78,56])).
% 116.55/116.60 cnf(45541,plain,
% 116.55/116.60 (~P14(f15(a1))),
% 116.55/116.60 inference(scs_inference,[],[36490,36585,36435,36465,37271,37295,37870,38011,37985,7237,33052,4,45513,45516,45523,45530,34714,228,5,2018,196,8,76,44,79,46,87,34,6107,43,45,77,78,56,83])).
% 116.55/116.60 cnf(45547,plain,
% 116.55/116.60 (~P6(f16(f15(a1)),f11(f16(f15(a1))))),
% 116.55/116.60 inference(scs_inference,[],[36490,36585,36435,36465,37271,37295,37870,38011,37985,7237,33052,4,45513,45516,45523,45530,45535,34714,228,5,2018,196,8,76,44,79,46,87,34,6107,43,45,77,78,56,83,7,1939,81])).
% 116.55/116.60 cnf(45548,plain,
% 116.55/116.60 (~P6(x455481,x455481)),
% 116.55/116.60 inference(rename_variables,[],[4])).
% 116.55/116.60 cnf(45550,plain,
% 116.55/116.60 (P17(f11(f16(f15(a1))))),
% 116.55/116.60 inference(scs_inference,[],[36490,36585,36435,36465,37271,37295,37870,38011,37985,7237,33052,4,45513,45516,45523,45530,45535,45548,34714,228,5,2018,196,8,76,44,79,46,87,34,6107,43,45,77,78,56,83,7,1939,81,39])).
% 116.55/116.60 cnf(45560,plain,
% 116.55/116.61 (~P18(f12(f10(f12(f10(a1)))))),
% 116.55/116.61 inference(scs_inference,[],[45525,37966,45529,196,228,2018])).
% 116.55/116.61 cnf(45566,plain,
% 116.55/116.61 (~P20(f9(f12(f9(f12(a1)))))),
% 116.55/116.61 inference(scs_inference,[],[45520,45525,4240,37966,45506,45529,4,196,228,2018,5,8,43])).
% 116.55/116.61 cnf(45567,plain,
% 116.55/116.61 (~P6(x455671,x455671)),
% 116.55/116.61 inference(rename_variables,[],[4])).
% 116.55/116.61 cnf(45571,plain,
% 116.55/116.61 (~P7(f12(f12(f11(a1))))),
% 116.55/116.61 inference(scs_inference,[],[45520,45525,4240,37966,45506,45515,45529,45512,45534,4,196,228,2018,5,8,43,79,45])).
% 116.55/116.61 cnf(45573,plain,
% 116.55/116.61 (~P6(f12(f9(f12(a1))),f10(f12(f9(f12(a1)))))),
% 116.55/116.61 inference(scs_inference,[],[45520,45525,4240,37966,45506,45515,45529,45512,45534,4,45567,196,228,2018,5,8,43,79,45,77])).
% 116.55/116.61 cnf(45574,plain,
% 116.55/116.61 (~P6(x455741,x455741)),
% 116.55/116.61 inference(rename_variables,[],[4])).
% 116.55/116.61 cnf(45576,plain,
% 116.55/116.61 (~P6(f9(f12(a1)),f12(f9(f12(a1))))),
% 116.55/116.61 inference(scs_inference,[],[45520,45525,4240,37966,45506,45515,45529,45512,45534,4023,4,45567,45574,196,228,2018,5,8,43,79,45,77,78])).
% 116.55/116.61 cnf(45577,plain,
% 116.55/116.61 (~P6(x455771,x455771)),
% 116.55/116.61 inference(rename_variables,[],[4])).
% 116.55/116.61 cnf(45579,plain,
% 116.55/116.61 (~P6(f15(a1),f16(f15(a1)))),
% 116.55/116.61 inference(scs_inference,[],[45520,45525,4240,37966,45506,45515,45529,45512,45534,4023,36490,4,45567,45574,196,228,2018,5,8,43,79,45,77,78,87])).
% 116.55/116.61 cnf(45581,plain,
% 116.55/116.61 (~P8(f16(f16(f15(a1))))),
% 116.55/116.61 inference(scs_inference,[],[45520,45525,4240,37966,45506,45515,45529,45550,45512,45534,45547,4023,36490,4,45567,45574,196,228,2018,5,8,43,79,45,77,78,87,56])).
% 116.55/116.61 cnf(45583,plain,
% 116.55/116.61 (P17(f11(f15(a1)))),
% 116.55/116.61 inference(scs_inference,[],[45520,45525,45539,4240,37966,45506,45515,45529,45550,45512,45534,45547,4023,36490,4,45567,45574,196,228,2018,5,8,43,79,45,77,78,87,56,39])).
% 116.55/116.61 cnf(45585,plain,
% 116.55/116.61 (~P20(f11(f16(f15(a1))))),
% 116.55/116.61 inference(scs_inference,[],[45520,45525,45539,4240,37966,45506,45515,45529,45550,45512,45534,45547,4023,36490,4,45567,45574,196,228,2018,5,8,43,79,45,77,78,87,56,39,38])).
% 116.55/116.61 cnf(45587,plain,
% 116.55/116.61 (~P6(f15(a1),f3(f15(a1)))),
% 116.55/116.61 inference(scs_inference,[],[45541,45520,45525,45539,4240,37966,45506,45515,45529,45550,45512,45534,45547,4023,36585,36465,36490,4,45567,45574,196,228,2018,5,8,43,79,45,77,78,87,56,39,38,90])).
% 116.55/116.61 cnf(45591,plain,
% 116.55/116.61 (~P21(f10(f12(f9(f12(a1)))))),
% 116.55/116.61 inference(scs_inference,[],[45541,45520,45525,45539,4240,37966,45506,45515,45529,45550,45512,45534,45547,4023,36585,36465,36490,4,45567,45574,45577,196,228,2018,5,8,43,79,45,77,78,87,56,39,38,90,7,44])).
% 116.55/116.61 cnf(45596,plain,
% 116.55/116.61 (P17(f9(f12(f11(a1))))),
% 116.55/116.61 inference(scs_inference,[],[45541,45520,45525,45539,4240,37966,45506,45515,45529,45550,45512,45522,45534,45547,4023,36585,36465,36490,4,45567,45574,45577,196,228,2018,5,8,43,79,45,77,78,87,56,39,38,90,7,44,76,34])).
% 116.55/116.61 cnf(45598,plain,
% 116.55/116.61 (~P12(f3(f15(a1)))),
% 116.55/116.61 inference(scs_inference,[],[45541,45520,45525,45539,4240,37966,45506,45515,45529,45550,45512,45522,45534,45547,36435,4023,36585,36465,36490,4,45567,45574,45577,196,228,2018,5,8,43,79,45,77,78,87,56,39,38,90,7,44,76,34,60])).
% 116.55/116.61 cnf(45607,plain,
% 116.55/116.61 (~P18(f12(f11(f16(f15(a1)))))),
% 116.55/116.61 inference(scs_inference,[],[45585,196])).
% 116.55/116.61 cnf(45617,plain,
% 116.55/116.61 (~P20(f11(f15(a1)))),
% 116.55/116.61 inference(scs_inference,[],[45583,45532,45585,45508,45591,4,196,5,228,2018,8,38])).
% 116.55/116.61 cnf(45626,plain,
% 116.55/116.61 (~P2(f13(f15(a1)))),
% 116.55/116.61 inference(scs_inference,[],[45587,45583,45598,45532,45585,45508,45591,33052,4,196,5,228,2018,8,38,51,48,100,13])).
% 116.55/116.61 cnf(45636,plain,
% 116.55/116.61 (~P18(f12(f10(f12(f11(a1)))))),
% 116.55/116.61 inference(scs_inference,[],[45571,45515,5,2018])).
% 116.55/116.61 cnf(45640,plain,
% 116.55/116.61 (~P18(f12(f11(f15(a1))))),
% 116.55/116.61 inference(scs_inference,[],[45617,45571,45596,45515,5,2018,228,196])).
% 116.55/116.61 cnf(45653,plain,
% 116.55/116.61 (~P7(f12(f11(f15(a1))))),
% 116.55/116.61 inference(scs_inference,[],[45640,45566,45550,228,196,8])).
% 116.55/116.61 cnf(45660,plain,
% 116.55/116.61 (~P7(f12(f10(f12(f10(a1)))))),
% 116.55/116.61 inference(scs_inference,[],[45560,8])).
% 116.55/116.61 cnf(45664,plain,
% 116.55/116.61 (~P21(f10(f9(f12(a1))))),
% 116.55/116.61 inference(scs_inference,[],[45576,45560,45581,4240,8,24,44])).
% 116.55/116.61 cnf(45667,plain,
% 116.55/116.61 (~P6(x456671,x456671)),
% 116.55/116.61 inference(rename_variables,[],[4])).
% 116.55/116.61 cnf(45669,plain,
% 116.55/116.61 (~P7(f12(f12(f9(f12(a1)))))),
% 116.55/116.61 inference(scs_inference,[],[45653,45576,45560,45573,45581,45591,4240,4,8,24,44,76,46])).
% 116.55/116.61 cnf(45671,plain,
% 116.55/116.61 (~P6(f16(f16(f15(a1))),f11(f16(f16(f15(a1)))))),
% 116.55/116.61 inference(scs_inference,[],[45653,45576,45560,45573,45581,45591,4240,4,45667,8,24,44,76,46,81])).
% 116.55/116.61 cnf(45686,plain,
% 116.55/116.61 (~P6(f10(f9(f12(a1))),f12(f10(f9(f12(a1)))))),
% 116.55/116.61 inference(scs_inference,[],[45664,45607,45669,4,2018,5,8,79])).
% 116.55/116.61 cnf(45687,plain,
% 116.55/116.61 (~P6(x456871,x456871)),
% 116.55/116.61 inference(rename_variables,[],[4])).
% 116.55/116.61 cnf(45690,plain,
% 116.55/116.61 (~P6(x456901,x456901)),
% 116.55/116.61 inference(rename_variables,[],[4])).
% 116.55/116.61 cnf(45692,plain,
% 116.55/116.61 (~P7(f12(f16(f15(a1))))),
% 116.55/116.61 inference(scs_inference,[],[45664,45607,45660,45669,45585,45547,4,45687,2018,5,8,79,43,45])).
% 116.55/116.61 cnf(45695,plain,
% 116.55/116.61 (~P6(x456951,x456951)),
% 116.55/116.61 inference(rename_variables,[],[4])).
% 116.55/116.61 cnf(45697,plain,
% 116.55/116.61 (~P6(f11(f15(a1)),f12(f11(f15(a1))))),
% 116.55/116.61 inference(scs_inference,[],[45664,45607,45660,45669,45510,45617,45585,45547,4,45687,45690,45695,2018,5,8,79,43,45,77,78])).
% 116.55/116.61 cnf(45698,plain,
% 116.55/116.61 (~P6(x456981,x456981)),
% 116.55/116.61 inference(rename_variables,[],[4])).
% 116.55/116.61 cnf(45711,plain,
% 116.55/116.61 (~P6(x457111,x457111)),
% 116.55/116.61 inference(rename_variables,[],[4])).
% 116.55/116.61 cnf(45715,plain,
% 116.55/116.61 (~P7(f12(f10(f9(f12(a1)))))),
% 116.55/116.61 inference(scs_inference,[],[45664,45607,45660,45669,45671,45510,45596,45617,45585,45547,45512,4,45687,45690,45695,45698,45711,2018,5,8,79,43,45,77,78,87,56,39,228,7,44,76,46])).
% 116.55/116.61 cnf(45716,plain,
% 116.55/116.61 (~P6(x457161,x457161)),
% 116.55/116.61 inference(rename_variables,[],[4])).
% 116.55/116.61 cnf(45718,plain,
% 116.55/116.61 (~P6(f15(a1),f11(f15(a1)))),
% 116.55/116.61 inference(scs_inference,[],[45664,45607,45660,45669,45671,45579,45510,45596,45617,45585,45539,45547,45512,4,45687,45690,45695,45698,45711,2018,5,8,79,43,45,77,78,87,56,39,228,7,44,76,46,81])).
% 116.55/116.61 cnf(45720,plain,
% 116.55/116.61 (P17(f9(f12(f10(a1))))),
% 116.55/116.61 inference(scs_inference,[],[45664,45607,45660,45669,45671,45579,45510,45596,45617,45585,45539,37985,45547,45512,37870,4,45687,45690,45695,45698,45711,2018,5,8,79,43,45,77,78,87,56,39,228,7,44,76,46,81,34])).
% 116.55/116.61 cnf(45722,plain,
% 116.55/116.61 (~P20(f11(f12(f11(a1))))),
% 116.55/116.61 inference(scs_inference,[],[45664,45607,45660,45669,45671,45579,45510,45596,45617,45585,45539,37985,45547,45512,37870,4,45687,45690,45695,45698,45711,45716,2018,5,8,79,43,45,77,78,87,56,39,228,7,44,76,46,81,34,38])).
% 116.55/116.61 cnf(45737,plain,
% 116.55/116.61 (~P6(x457371,x457371)),
% 116.55/116.61 inference(rename_variables,[],[4])).
% 116.55/116.61 cnf(45739,plain,
% 116.55/116.61 (~P20(f9(f11(f15(a1))))),
% 116.55/116.61 inference(scs_inference,[],[45692,45720,45722,45697,45636,45573,45653,45591,4,196,5,228,8,79,45,43])).
% 116.55/116.61 cnf(45741,plain,
% 116.55/116.61 (~P6(f11(f15(a1)),f10(f11(f15(a1))))),
% 116.55/116.61 inference(scs_inference,[],[45692,45720,45722,45697,45636,45573,45653,45591,4,196,5,228,8,79,45,43,77])).
% 116.55/116.61 cnf(45743,plain,
% 116.55/116.61 (~P6(f16(f15(a1)),f12(f16(f15(a1))))),
% 116.55/116.61 inference(scs_inference,[],[45692,45720,45722,45697,45636,45573,45653,45591,45585,45547,4,196,5,228,8,79,45,43,77,78])).
% 116.55/116.61 cnf(45745,plain,
% 116.55/116.61 (~P6(f12(f10(a1)),f16(f12(f10(a1))))),
% 116.55/116.61 inference(scs_inference,[],[45692,45720,45722,45697,45636,45573,45653,45591,45585,37985,45547,4,196,5,228,8,79,45,43,77,78,87])).
% 116.55/116.61 cnf(45747,plain,
% 116.55/116.61 (~P8(f16(f12(f10(a1))))),
% 116.55/116.61 inference(scs_inference,[],[45692,45720,45722,45697,45636,45573,45653,45591,45585,37985,45547,4,196,5,228,8,79,45,43,77,78,87,56])).
% 116.55/116.61 cnf(45749,plain,
% 116.55/116.61 (P17(f11(f16(f16(f15(a1)))))),
% 116.55/116.61 inference(scs_inference,[],[45692,45720,45722,45697,45636,45573,45653,45591,45585,45581,37985,45547,4,45737,196,5,228,8,79,45,43,77,78,87,56,39])).
% 116.55/116.61 cnf(45756,plain,
% 116.55/116.61 (~P20(f11(f16(f16(f15(a1)))))),
% 116.55/116.61 inference(scs_inference,[],[45718,45692,45720,45722,45697,45636,45573,45671,45653,45591,45585,45581,37985,45547,4,45737,196,5,228,8,79,45,43,77,78,87,56,39,7,47,38])).
% 116.55/116.61 cnf(45759,plain,
% 116.55/116.61 (~P18(f12(f9(f11(f15(a1)))))),
% 116.55/116.61 inference(scs_inference,[],[45739,196])).
% 116.55/116.61 cnf(45768,plain,
% 116.55/116.61 (~P18(f12(f11(f16(f16(f15(a1))))))),
% 116.55/116.61 inference(scs_inference,[],[45756,196])).
% 116.55/116.61 cnf(45770,plain,
% 116.55/116.61 (~P7(f12(f9(f11(f15(a1)))))),
% 116.55/116.61 inference(scs_inference,[],[45756,45759,196,8])).
% 116.55/116.61 cnf(45782,plain,
% 116.55/116.61 (~P6(f10(f9(f12(a1))),f9(f10(f9(f12(a1)))))),
% 116.55/116.61 inference(scs_inference,[],[45741,45686,45768,45715,8,44,76])).
% 116.55/116.61 cnf(45799,plain,
% 116.55/116.61 (~P6(f12(f10(a1)),f11(f12(f10(a1))))),
% 116.55/116.61 inference(scs_inference,[],[45743,45745,45770,45626,45747,45692,4,23,44,76,81])).
% 116.55/116.61 cnf(45806,plain,
% 116.55/116.61 (~P7(f12(f16(f16(f15(a1)))))),
% 116.55/116.61 inference(scs_inference,[],[45756,45671,45])).
% 116.55/116.61 cnf(45812,plain,
% 116.55/116.61 (~P6(f16(f16(f15(a1))),f12(f16(f16(f15(a1)))))),
% 116.55/116.61 inference(scs_inference,[],[45686,45715,45756,45671,45,43,77,78])).
% 116.55/116.61 cnf(45814,plain,
% 116.55/116.61 (~P8(f16(f16(f16(f15(a1)))))),
% 116.55/116.61 inference(scs_inference,[],[45686,45715,45749,45756,45671,45,43,77,78,56])).
% 116.55/116.61 cnf(45818,plain,
% 116.55/116.61 (P17(f11(f12(f10(a1))))),
% 116.55/116.61 inference(scs_inference,[],[45686,45745,45747,45715,45749,45756,45671,45,43,77,78,56,87,39])).
% 116.55/116.61 cnf(45820,plain,
% 116.55/116.61 (P17(f9(f10(f9(f12(a1)))))),
% 116.55/116.61 inference(scs_inference,[],[45782,45686,45745,45747,45715,45749,45756,45671,45,43,77,78,56,87,39,34])).
% 116.55/116.61 cnf(45846,plain,
% 116.55/116.61 (~P6(x458461,x458461)),
% 116.55/116.61 inference(rename_variables,[],[4])).
% 116.55/116.61 cnf(45855,plain,
% 116.55/116.61 (~P20(f11(f12(f10(a1))))),
% 116.55/116.61 inference(scs_inference,[],[45818,45799,45806,45814,45820,45812,45782,45739,4,45846,228,43,77,78,56,87,39,38])).
% 116.55/116.61 cnf(45866,plain,
% 116.55/116.61 (P6(f15(a1),f18(f15(a1)))),
% 116.55/116.61 inference(scs_inference,[],[45818,45799,45806,45814,45820,45812,45782,45739,33044,33052,4,45846,228,43,77,78,56,87,39,38,196,7,8,73,42181,42053])).
% 116.55/116.61 cnf(45884,plain,
% 116.55/116.61 ($false),
% 116.55/116.61 inference(scs_inference,[],[45866,45855,33044,33052,33146,33078,33179,35281,42181,196,8,68]),
% 116.55/116.61 ['proof']).
% 116.55/116.61 % SZS output end Proof
% 116.55/116.61 % Total time :115.920000s
%------------------------------------------------------------------------------