%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MED007+1 : TPTP v8.2.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n032.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 181.28s 181.41s
% Output : CNFRefutation 181.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.18 % Problem : MED007+1 : TPTP v8.2.0. Released v3.2.0.
% 0.08/0.18 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.08/0.38 % Computer : n032.cluster.edu
% 0.08/0.38 % Model : x86_64 x86_64
% 0.08/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.38 % Memory : 8042.1875MB
% 0.08/0.38 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.38 % CPULimit : 300
% 0.08/0.38 % WCLimit : 300
% 0.08/0.38 % DateTime : Sat Jun 22 18:52:54 EDT 2024
% 0.08/0.39 % CPUTime :
% 0.31/0.62 start to proof:theBenchmark
% 181.21/181.39 %-------------------------------------------
% 181.21/181.39 % File :CSE---1.7
% 181.21/181.39 % Problem :theBenchmark
% 181.21/181.39 % Transform :cnf
% 181.21/181.39 % Format :tptp:raw
% 181.21/181.39 % Command :java -jar mcs_scs.jar %d %s
% 181.21/181.39
% 181.21/181.39 % Result :Theorem 180.680000s
% 181.21/181.39 % Output :CNFRefutation 180.680000s
% 181.21/181.39 %-------------------------------------------
% 181.28/181.41 %------------------------------------------------------------------------------
% 181.28/181.41 % File : MED007+1 : TPTP v8.2.0. Released v3.2.0.
% 181.28/181.41 % Domain : Medicine
% 181.28/181.41 % Problem : Unsuccessful s1-qilt27 treatment next step
% 181.28/181.41 % Version : [HLB05] axioms : Especial.
% 181.28/181.41 % English : After unsuccessful treatment with single oral anti-diabetic for
% 181.28/181.41 % patients with QI less than 27 medical management moves to next
% 181.28/181.41 % step.
% 181.28/181.41
% 181.28/181.41 % Refs : [HLB05] Hommersom et al. (2005), Automated Theorem Proving for
% 181.28/181.41 % : [Hom06] Hommersom (2006), Email to G. Sutcliffe
% 181.28/181.41 % Source : [Hom06]
% 181.28/181.41 % Names :
% 181.28/181.41
% 181.28/181.41 % Status : Theorem
% 181.28/181.41 % Rating : 0.00 v8.1.0, 0.07 v7.5.0, 0.24 v7.4.0, 0.06 v7.3.0, 0.14 v7.2.0, 0.17 v7.1.0, 0.00 v7.0.0, 0.07 v6.3.0, 0.00 v6.2.0, 0.18 v6.1.0, 0.32 v6.0.0, 0.25 v5.5.0, 0.50 v5.4.0, 0.48 v5.3.0, 0.52 v5.2.0, 0.29 v5.0.0, 0.35 v4.1.0, 0.44 v4.0.1, 0.42 v4.0.0, 0.45 v3.7.0, 0.33 v3.5.0, 0.25 v3.4.0, 0.33 v3.3.0, 0.67 v3.2.0
% 181.28/181.41 % Syntax : Number of formulae : 41 ( 1 unt; 0 def)
% 181.28/181.41 % Number of atoms : 201 ( 0 equ)
% 181.28/181.41 % Maximal formula atoms : 30 ( 4 avg)
% 181.28/181.41 % Number of connectives : 244 ( 84 ~; 34 |; 51 &)
% 181.28/181.41 % ( 0 <=>; 75 =>; 0 <=; 0 <~>)
% 181.28/181.41 % Maximal formula depth : 12 ( 6 avg)
% 181.28/181.41 % Maximal term depth : 1 ( 1 avg)
% 181.28/181.41 % Number of predicates : 20 ( 20 usr; 0 prp; 1-2 aty)
% 181.28/181.41 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% 181.28/181.41 % Number of variables : 96 ( 92 !; 4 ?)
% 181.28/181.41 % SPC : FOF_THM_RFO_NEQ
% 181.28/181.41
% 181.28/181.41 % Comments :
% 181.28/181.41 %------------------------------------------------------------------------------
% 181.28/181.41 include('Axioms/MED001+0.ax').
% 181.28/181.41 include('Axioms/MED001+1.ax').
% 181.28/181.41 %------------------------------------------------------------------------------
% 181.28/181.41 fof(transs1s2_qilt27,conjecture,
% 181.28/181.41 ( ( s1(n0)
% 181.28/181.41 & ! [X0] :
% 181.28/181.41 ( gt(n0,X0)
% 181.28/181.41 => conditionhyper(X0) )
% 181.28/181.41 & ~ bcapacitysn(n0)
% 181.28/181.41 & qilt27(n0) )
% 181.28/181.41 => ? [X0] :
% 181.28/181.41 ( ~ gt(n0,X0)
% 181.28/181.41 & s2(X0)
% 181.28/181.41 & ! [X1] :
% 181.28/181.41 ( gt(X0,X1)
% 181.28/181.41 => conditionhyper(X1) )
% 181.28/181.41 & ( bcapacityne(X0)
% 181.28/181.41 | bcapacityex(X0) ) ) ) ).
% 181.28/181.41
% 181.28/181.41 %------------------------------------------------------------------------------
% 181.28/181.41 %-------------------------------------------
% 181.28/181.41 % Proof found
% 181.28/181.41 % SZS status Theorem for theBenchmark
% 181.28/181.41 % SZS output start Proof
% 181.28/181.42 %ClaNum:167(EqnAxiom:0)
% 181.28/181.42 %VarNum:684(SingletonVarNum:221)
% 181.28/181.42 %MaxLitNum:8
% 181.28/181.42 %MaxfuncDepth:1
% 181.28/181.42 %SharedTerms:4
% 181.28/181.42 %goalClause: 1 2 3 36 67 68 72 73
% 181.28/181.42 %singleGoalClaCount:3
% 181.28/181.42 [1]P1(a1)
% 181.28/181.42 [2]P15(a1)
% 181.28/181.42 [3]~P2(a1)
% 181.28/181.42 [4]~P5(x41,x41)
% 181.28/181.42 [5]~P18(x51)+P6(x51)
% 181.28/181.42 [6]~P19(x61)+P12(x61)
% 181.28/181.42 [7]~P19(x71)+P7(x71)
% 181.28/181.42 [8]~P6(x81)+P18(x81)
% 181.28/181.42 [11]~P4(x111)+~P3(x111)
% 181.28/181.42 [12]~P2(x121)+~P3(x121)
% 181.28/181.42 [13]~P2(x131)+~P4(x131)
% 181.28/181.42 [14]~P10(x141)+~P8(x141)
% 181.28/181.42 [15]~P11(x151)+~P8(x151)
% 181.28/181.42 [16]~P11(x161)+~P10(x161)
% 181.28/181.42 [17]~P15(x171)+~P16(x171)
% 181.28/181.42 [18]~P19(x181)+~P16(x181)
% 181.28/181.42 [19]~P18(x191)+~P16(x191)
% 181.28/181.42 [20]~P19(x201)+~P15(x201)
% 181.28/181.42 [21]~P18(x211)+~P15(x211)
% 181.28/181.42 [22]~P18(x221)+~P19(x221)
% 181.28/181.42 [36]P8(x361)+~P5(a1,x361)
% 181.28/181.42 [35]~P4(x351)+~P9(f2(x351))
% 181.28/181.42 [58]~P4(x581)+~P5(x581,f2(x581))
% 181.28/181.42 [9]P4(x91)+P2(x91)+P3(x91)
% 181.28/181.42 [10]P10(x101)+P11(x101)+P8(x101)
% 181.28/181.42 [23]P2(x231)+~P13(x231)+P3(x231)
% 181.28/181.42 [24]P1(x241)+~P15(x241)+P7(x241)
% 181.28/181.42 [26]~P1(x261)+~P15(x261)+P12(x261)
% 181.28/181.42 [37]P13(x371)+P4(x371)+~P11(f3(x371))
% 181.28/181.42 [62]P13(x621)+P4(x621)+~P5(x621,f3(x621))
% 181.28/181.42 [34]P17(x341)+P20(x341)+P5(x342,x341)
% 181.28/181.42 [38]~P20(x382)+~P17(x382)+P5(x381,x382)
% 181.28/181.42 [39]P7(x391)+P5(x392,x391)+P17(f11(x392))
% 181.28/181.42 [43]P6(x431)+P5(x432,x431)+~P20(f9(x432))
% 181.28/181.42 [44]P6(x441)+P5(x442,x441)+~P21(f10(x442))
% 181.28/181.42 [45]P20(x451)+P5(x452,x451)+~P6(f12(x452))
% 181.28/181.42 [46]P21(x461)+P5(x462,x461)+~P6(f12(x462))
% 181.28/181.42 [47]P12(x471)+P5(x472,x471)+~P9(f2(x472))
% 181.28/181.42 [56]~P17(x562)+P5(x561,x562)+~P7(f16(x561))
% 181.28/181.42 [76]P6(x761)+P5(x762,x761)+~P5(x762,f9(x762))
% 181.28/181.42 [77]P6(x771)+P5(x772,x771)+~P5(x772,f10(x772))
% 181.28/181.42 [78]P20(x781)+P5(x782,x781)+~P5(x782,f12(x782))
% 181.28/181.43 [79]P21(x791)+P5(x792,x791)+~P5(x792,f12(x792))
% 181.28/181.43 [80]P12(x801)+P5(x802,x801)+~P5(x802,f2(x802))
% 181.28/181.43 [81]P7(x811)+P5(x812,x811)+~P5(x812,f11(x812))
% 181.28/181.43 [87]~P17(x872)+P5(x871,x872)+~P5(x871,f16(x871))
% 181.28/181.43 [102]~P5(x1021,x1023)+P5(x1021,x1022)+~P5(x1023,x1022)
% 181.28/181.43 [25]P15(x251)+P19(x251)+P18(x251)+P16(x251)
% 181.28/181.43 [29]P19(x291)+P18(x291)+~P12(x291)+P15(x291)
% 181.28/181.43 [30]P19(x301)+P18(x301)+~P7(x301)+P15(x301)
% 181.28/181.43 [31]P18(x311)+P14(x311)+~P12(x311)+P19(x311)
% 181.28/181.43 [33]P18(x331)+~P7(x331)+~P1(x331)+P19(x331)
% 181.28/181.43 [67]~P3(x671)+~P19(x671)+P5(a1,x671)+~P8(f18(x671))
% 181.28/181.43 [68]~P4(x681)+~P19(x681)+P5(a1,x681)+~P8(f18(x681))
% 181.28/181.43 [72]~P3(x721)+~P19(x721)+P5(x721,f18(x721))+P5(a1,x721)
% 181.28/181.43 [73]~P4(x731)+~P19(x731)+P5(x731,f18(x731))+P5(a1,x731)
% 181.28/181.43 [40]P5(x401,x402)+~P13(x401)+P2(x401)+P9(x402)
% 181.28/181.43 [57]~P13(x571)+~P5(x571,x572)+P2(x571)+P8(x572)
% 181.28/181.43 [48]~P19(x482)+P11(x481)+P5(x482,x481)+P4(f13(x482))
% 181.28/181.43 [49]~P16(x492)+P11(x491)+P5(x492,x491)+P15(f14(x492))
% 181.28/181.43 [50]~P15(x502)+P11(x501)+P5(x502,x501)+P19(f15(x502))
% 181.28/181.43 [51]~P19(x512)+P11(x511)+P5(x512,x511)+P18(f13(x512))
% 181.28/181.43 [59]P5(x591,x592)+P4(x591)+P9(x592)+~P12(f17(x591))
% 181.28/181.43 [60]P5(x602,x601)+P20(x601)+P13(x602)+~P11(f3(x602))
% 181.28/181.43 [61]P5(x612,x611)+P21(x611)+P13(x612)+~P11(f3(x612))
% 181.28/181.43 [74]~P5(x742,x741)+P8(x741)+P13(x742)+~P11(f3(x742))
% 181.28/181.43 [88]P5(x881,x882)+P4(x881)+P9(x882)+~P5(x881,f17(x881))
% 181.28/181.43 [89]P5(x892,x891)+P20(x891)+P13(x892)+~P5(x892,f3(x892))
% 181.28/181.43 [90]P5(x902,x901)+P21(x901)+P13(x902)+~P5(x902,f3(x902))
% 181.28/181.43 [98]~P16(x982)+P11(x981)+P5(x982,x981)+~P5(x982,f14(x982))
% 181.28/181.43 [99]~P15(x992)+P11(x991)+P5(x992,x991)+~P5(x992,f15(x992))
% 181.28/181.43 [100]~P19(x1002)+P11(x1001)+P5(x1002,x1001)+~P5(x1002,f13(x1002))
% 181.28/181.43 [112]~P5(x1122,x1121)+P8(x1121)+P13(x1122)+~P5(x1122,f3(x1122))
% 181.28/181.43 [53]P5(x531,x532)+~P1(x531)+~P13(x531)+P3(x531)+P9(x532)
% 181.28/181.43 [54]P1(x541)+~P17(x542)+~P13(x541)+P3(x541)+P5(x541,x542)
% 181.28/181.43 [65]P1(x651)+~P13(x651)+~P5(x651,x652)+P3(x651)+P8(x652)
% 181.28/181.43 [69]~P1(x691)+~P13(x691)+~P5(x691,x692)+P3(x691)+P8(x692)
% 181.28/181.43 [71]~P15(x712)+P11(x711)+P5(x712,x711)+P3(f15(x712))+P4(f15(x712))
% 181.28/181.43 [109]~P16(x1093)+P8(x1091)+P5(x1093,x1092)+P11(x1092)+~P5(f14(x1093),x1091)
% 181.28/181.43 [110]~P15(x1103)+P8(x1101)+P5(x1103,x1102)+P11(x1102)+~P5(f15(x1103),x1101)
% 181.28/181.43 [111]~P19(x1113)+P8(x1111)+P5(x1113,x1112)+P11(x1112)+~P5(f13(x1113),x1111)
% 181.28/181.43 [97]P5(x972,x971)+~P2(x972)+P11(x971)+P1(x972)+P17(f19(x972))+~P8(f22(x972))
% 181.28/181.43 [108]P5(x1082,x1081)+~P2(x1082)+P11(x1081)+P1(x1082)+P5(x1082,f22(x1082))+P17(f19(x1082))
% 181.28/181.43 [118]~P2(x1182)+~P1(x1182)+P11(x1181)+P5(x1182,x1181)+~P8(f20(x1182))+~P9(f21(x1182))
% 181.28/181.43 [120]~P3(x1202)+P11(x1201)+P5(x1202,x1201)+P17(f23(x1202))+~P8(f4(x1202))+~P9(f5(x1202))
% 181.28/181.43 [121]~P2(x1212)+~P1(x1212)+P11(x1211)+P5(x1212,x1211)+P5(x1212,f20(x1212))+~P9(f21(x1212))
% 181.28/181.43 [127]~P3(x1272)+P11(x1271)+P5(x1272,x1271)+P5(x1272,f4(x1272))+P17(f23(x1272))+~P9(f5(x1272))
% 181.28/181.43 [130]~P3(x1302)+P11(x1301)+P5(x1302,x1301)+~P8(f4(x1302))+~P21(f24(x1302))+~P9(f5(x1302))
% 181.28/181.43 [134]P5(x1342,x1341)+~P2(x1342)+P11(x1341)+P1(x1342)+~P5(x1342,f19(x1342))+~P8(f22(x1342))
% 181.28/181.43 [135]~P3(x1352)+P11(x1351)+P5(x1352,x1351)+P5(x1352,f4(x1352))+~P21(f24(x1352))+~P9(f5(x1352))
% 181.28/181.43 [140]~P2(x1402)+~P1(x1402)+P11(x1401)+P5(x1402,x1401)+~P5(x1402,f21(x1402))+~P8(f20(x1402))
% 181.28/181.43 [142]P5(x1422,x1421)+~P2(x1422)+P11(x1421)+P1(x1422)+P5(x1422,f22(x1422))+~P5(x1422,f19(x1422))
% 181.28/181.43 [144]~P3(x1442)+P11(x1441)+P5(x1442,x1441)+~P5(x1442,f5(x1442))+P17(f23(x1442))+~P8(f4(x1442))
% 181.28/181.43 [145]~P2(x1452)+~P1(x1452)+P11(x1451)+P5(x1452,x1451)+P5(x1452,f20(x1452))+~P5(x1452,f21(x1452))
% 181.28/181.43 [148]~P3(x1482)+P11(x1481)+P5(x1482,x1481)+P5(x1482,f4(x1482))+~P5(x1482,f5(x1482))+P17(f23(x1482))
% 181.28/181.43 [149]~P3(x1492)+P11(x1491)+P5(x1492,x1491)+~P5(x1492,f5(x1492))+~P8(f4(x1492))+~P21(f24(x1492))
% 181.28/181.43 [150]~P3(x1502)+P11(x1501)+P5(x1502,x1501)+~P5(x1502,f23(x1502))+~P8(f4(x1502))+~P9(f5(x1502))
% 181.28/181.43 [151]~P3(x1512)+P11(x1511)+P5(x1512,x1511)+~P5(x1512,f24(x1512))+~P8(f4(x1512))+~P9(f5(x1512))
% 181.28/181.43 [153]~P3(x1532)+P11(x1531)+P5(x1532,x1531)+P5(x1532,f4(x1532))+~P5(x1532,f5(x1532))+~P21(f24(x1532))
% 181.28/181.43 [154]~P3(x1542)+P11(x1541)+P5(x1542,x1541)+P5(x1542,f4(x1542))+~P5(x1542,f23(x1542))+~P9(f5(x1542))
% 181.28/181.43 [155]~P3(x1552)+P11(x1551)+P5(x1552,x1551)+P5(x1552,f4(x1552))+~P5(x1552,f24(x1552))+~P9(f5(x1552))
% 181.28/181.43 [162]~P3(x1622)+P11(x1621)+P5(x1622,x1621)+~P5(x1622,f23(x1622))+~P5(x1622,f5(x1622))+~P8(f4(x1622))
% 181.28/181.43 [163]~P3(x1632)+P11(x1631)+P5(x1632,x1631)+~P5(x1632,f24(x1632))+~P5(x1632,f5(x1632))+~P8(f4(x1632))
% 181.28/181.43 [164]~P3(x1642)+P11(x1641)+P5(x1642,x1641)+P5(x1642,f4(x1642))+~P5(x1642,f23(x1642))+~P5(x1642,f5(x1642))
% 181.28/181.43 [165]~P3(x1652)+P11(x1651)+P5(x1652,x1651)+P5(x1652,f4(x1652))+~P5(x1652,f24(x1652))+~P5(x1652,f5(x1652))
% 181.28/181.43 [82]P5(x821,x822)+~P17(x823)+~P13(x821)+P3(x821)+P5(x821,x823)+P9(x822)
% 181.28/181.43 [83]P5(x831,x832)+~P17(x833)+~P13(x831)+P2(x831)+P5(x831,x833)+P21(x832)
% 181.28/181.43 [85]P5(x853,x852)+~P1(x853)+~P13(x853)+P9(x851)+P5(x853,x851)+P9(x852)
% 181.28/181.43 [86]P5(x862,x861)+~P17(x863)+~P13(x862)+P9(x861)+P5(x862,x863)+P1(x862)
% 181.28/181.43 [113]~P13(x1131)+~P5(x1131,x1132)+~P5(x1131,x1133)+P3(x1131)+P8(x1132)+P8(x1133)
% 181.28/181.43 [116]~P13(x1163)+~P5(x1163,x1161)+~P5(x1163,x1162)+P8(x1161)+P8(x1162)+P1(x1163)
% 181.28/181.43 [119]~P13(x1193)+~P5(x1193,x1191)+~P5(x1193,x1192)+P8(x1191)+P8(x1192)+~P1(x1193)
% 181.28/181.43 [138]P11(x1381)+~P4(x1382)+P10(x1381)+P5(x1382,x1381)+~P8(f6(x1382))+~P20(f7(x1382))+~P21(f8(x1382))
% 181.28/181.43 [143]P11(x1431)+~P4(x1432)+P10(x1431)+P5(x1432,x1431)+P5(x1432,f6(x1432))+~P20(f7(x1432))+~P21(f8(x1432))
% 181.28/181.43 [156]P11(x1561)+~P4(x1562)+P10(x1561)+P5(x1562,x1561)+~P5(x1562,f8(x1562))+~P8(f6(x1562))+~P20(f7(x1562))
% 181.28/181.43 [157]P11(x1571)+~P4(x1572)+P10(x1571)+P5(x1572,x1571)+~P5(x1572,f7(x1572))+~P8(f6(x1572))+~P21(f8(x1572))
% 181.28/181.43 [159]P11(x1591)+~P4(x1592)+P10(x1591)+P5(x1592,x1591)+P5(x1592,f6(x1592))+~P5(x1592,f8(x1592))+~P20(f7(x1592))
% 181.28/181.43 [160]P11(x1601)+~P4(x1602)+P10(x1601)+P5(x1602,x1601)+P5(x1602,f6(x1602))+~P5(x1602,f7(x1602))+~P21(f8(x1602))
% 181.28/181.43 [166]P11(x1661)+~P4(x1662)+P10(x1661)+P5(x1662,x1661)+~P5(x1662,f7(x1662))+~P5(x1662,f8(x1662))+~P8(f6(x1662))
% 181.28/181.43 [167]P11(x1671)+~P4(x1672)+P10(x1671)+P5(x1672,x1671)+P5(x1672,f6(x1672))+~P5(x1672,f7(x1672))+~P5(x1672,f8(x1672))
% 181.28/181.43 [117]P5(x1173,x1172)+~P17(x1174)+~P13(x1173)+P9(x1171)+P5(x1173,x1171)+P9(x1172)+P5(x1173,x1174)
% 181.28/181.43 [147]~P5(x1474,x1471)+~P5(x1474,x1472)+~P5(x1474,x1473)+P8(x1471)+P8(x1472)+P8(x1473)+~P13(x1474)
% 181.28/181.43 [126]P5(x1262,x1261)+~P17(x1263)+~P17(x1264)+~P13(x1262)+P21(x1261)+P5(x1262,x1263)+P1(x1262)+P5(x1262,x1264)
% 181.28/181.43 %EqnAxiom
% 181.28/181.43
% 181.28/181.43 %-------------------------------------------
% 181.28/181.45 cnf(168,plain,
% 181.28/181.45 (~P19(a1)),
% 181.28/181.45 inference(scs_inference,[],[2,20])).
% 181.28/181.45 cnf(170,plain,
% 181.28/181.45 (~P18(a1)),
% 181.28/181.45 inference(scs_inference,[],[2,20,21])).
% 181.28/181.45 cnf(172,plain,
% 181.28/181.45 (~P6(a1)),
% 181.28/181.45 inference(scs_inference,[],[2,20,21,8])).
% 181.28/181.45 cnf(235,plain,
% 181.28/181.45 (~P18(f12(x2351))+P20(x2351)),
% 181.28/181.45 inference(scs_inference,[],[4,5,45])).
% 181.28/181.45 cnf(1195,plain,
% 181.28/181.45 (~P18(f12(f9(a1)))),
% 181.28/181.45 inference(scs_inference,[],[172,4,235,43])).
% 181.28/181.45 cnf(1196,plain,
% 181.28/181.45 (~P6(f12(f9(a1)))),
% 181.28/181.45 inference(scs_inference,[],[1195,8])).
% 181.28/181.45 cnf(1561,plain,
% 181.28/181.45 (P17(f11(a1))),
% 181.28/181.45 inference(scs_inference,[],[4,168,1,170,39,33])).
% 181.28/181.45 cnf(1562,plain,
% 181.28/181.45 (~P20(f11(a1))),
% 181.28/181.45 inference(scs_inference,[],[1561,4,38])).
% 181.28/181.45 cnf(1567,plain,
% 181.28/181.45 (~P6(f12(f11(a1)))),
% 181.28/181.45 inference(scs_inference,[],[1561,4,38,235,8])).
% 181.28/181.45 cnf(1632,plain,
% 181.28/181.45 (~P7(f16(f11(a1)))),
% 181.28/181.45 inference(scs_inference,[],[4,1562,56,34])).
% 181.28/181.45 cnf(1806,plain,
% 181.28/181.45 (~P5(f11(a1),f12(f11(a1)))),
% 181.28/181.45 inference(scs_inference,[],[4,1561,78,38])).
% 181.28/181.45 cnf(1822,plain,
% 181.28/181.45 (~P5(f10(f11(a1)),f12(f10(f11(a1))))),
% 181.28/181.45 inference(scs_inference,[],[4,1806,1567,79,44])).
% 181.28/181.45 cnf(1854,plain,
% 181.28/181.45 (P5(x18541,f11(a1))+~P5(f16(x18541),f11(f16(x18541)))),
% 181.28/181.45 inference(scs_inference,[],[4,1561,81,56])).
% 181.28/181.45 cnf(2727,plain,
% 181.28/181.45 (~P7(a1)),
% 181.28/181.45 inference(scs_inference,[],[172,168,1,5,33])).
% 181.28/181.45 cnf(3615,plain,
% 181.28/181.45 (~P20(f9(a1))),
% 181.28/181.45 inference(scs_inference,[],[170,4,8,43])).
% 181.28/181.45 cnf(3616,plain,
% 181.28/181.45 (P17(f9(a1))),
% 181.28/181.45 inference(scs_inference,[],[3615,4,34])).
% 181.28/181.45 cnf(3634,plain,
% 181.28/181.45 (~P21(f10(a1))),
% 181.28/181.45 inference(scs_inference,[],[170,4,8,44])).
% 181.28/181.45 cnf(3650,plain,
% 181.28/181.45 (~P5(a1,f9(a1))),
% 181.28/181.45 inference(scs_inference,[],[170,4,8,76])).
% 181.28/181.45 cnf(3666,plain,
% 181.28/181.45 (~P5(a1,f10(a1))),
% 181.28/181.45 inference(scs_inference,[],[170,4,8,77])).
% 181.28/181.45 cnf(24332,plain,
% 181.28/181.45 (~P6(f12(a1))),
% 181.28/181.45 inference(scs_inference,[],[3615,3650,45])).
% 181.28/181.45 cnf(24334,plain,
% 181.28/181.45 (~P7(f16(a1))),
% 181.28/181.45 inference(scs_inference,[],[3615,3616,3650,45,56])).
% 181.28/181.45 cnf(24336,plain,
% 181.28/181.45 (~P5(a1,f12(a1))),
% 181.28/181.45 inference(scs_inference,[],[3615,3616,3650,45,56,78])).
% 181.28/181.45 cnf(24338,plain,
% 181.28/181.45 (~P5(a1,f11(a1))),
% 181.28/181.45 inference(scs_inference,[],[2727,3615,3616,3650,4,45,56,78,81])).
% 181.28/181.45 cnf(24356,plain,
% 181.28/181.45 (~P11(f3(a1))),
% 181.28/181.45 inference(scs_inference,[],[24338,3634,1561,3666,3,83,62,61])).
% 181.28/181.45 cnf(24358,plain,
% 181.28/181.45 (~P5(a1,f3(a1))),
% 181.28/181.45 inference(scs_inference,[],[24338,3634,1562,1561,3666,3,83,62,61,89])).
% 181.28/181.45 cnf(24363,plain,
% 181.28/181.45 (P19(f15(a1))),
% 181.28/181.45 inference(scs_inference,[],[24358,24356,2,50])).
% 181.28/181.45 cnf(24365,plain,
% 181.28/181.45 (~P5(a1,f15(a1))),
% 181.28/181.45 inference(scs_inference,[],[24358,24356,2,50,99])).
% 181.28/181.45 cnf(24385,plain,
% 181.28/181.45 (P8(x243851)+~P5(f15(a1),x243851)),
% 181.28/181.45 inference(scs_inference,[],[24336,24356,24358,2,38,110])).
% 181.28/181.45 cnf(24387,plain,
% 181.28/181.45 (P4(f15(a1))+P3(f15(a1))),
% 181.28/181.45 inference(scs_inference,[],[24356,24358,2,71])).
% 181.28/181.45 cnf(27181,plain,
% 181.28/181.45 (~P18(f15(a1))),
% 181.28/181.45 inference(scs_inference,[],[24363,22])).
% 181.28/181.45 cnf(27202,plain,
% 181.28/181.45 (~P6(f15(a1))),
% 181.28/181.45 inference(scs_inference,[],[27181,8])).
% 181.28/181.45 cnf(35912,plain,
% 181.28/181.45 (~P5(f16(a1),f11(f16(a1)))),
% 181.28/181.45 inference(scs_inference,[],[24338,1854])).
% 181.28/181.45 cnf(35914,plain,
% 181.28/181.45 (~P5(f15(a1),f9(f15(a1)))),
% 181.28/181.45 inference(scs_inference,[],[27202,24338,4,1854,76])).
% 181.28/181.45 cnf(35915,plain,
% 181.28/181.45 (~P5(x359151,x359151)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(35917,plain,
% 181.28/181.45 (~P5(f15(a1),f10(f15(a1)))),
% 181.28/181.45 inference(scs_inference,[],[27202,24338,4,35915,1854,76,77])).
% 181.28/181.45 cnf(35918,plain,
% 181.28/181.45 (~P5(x359181,x359181)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(35920,plain,
% 181.28/181.45 (~P21(f10(f15(a1)))),
% 181.28/181.45 inference(scs_inference,[],[27202,24338,4,35915,35918,1854,76,77,44])).
% 181.28/181.45 cnf(35921,plain,
% 181.28/181.45 (~P5(x359211,x359211)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(35923,plain,
% 181.28/181.45 (P17(f11(f16(f11(a1))))),
% 181.28/181.45 inference(scs_inference,[],[27202,1632,24338,4,35915,35918,35921,1854,76,77,44,39])).
% 181.28/181.45 cnf(35924,plain,
% 181.28/181.45 (~P5(x359241,x359241)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(35926,plain,
% 181.28/181.45 (~P7(f16(f9(a1)))),
% 181.28/181.45 inference(scs_inference,[],[27202,1632,24338,4,35915,35918,35921,35924,3616,1854,76,77,44,39,56])).
% 181.28/181.45 cnf(35927,plain,
% 181.28/181.45 (~P5(x359271,x359271)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(35929,plain,
% 181.28/181.45 (~P6(f12(f10(f15(a1))))),
% 181.28/181.45 inference(scs_inference,[],[27202,1632,24338,4,35915,35918,35921,35924,35927,3616,1854,76,77,44,39,56,46])).
% 181.28/181.45 cnf(35930,plain,
% 181.28/181.45 (~P5(x359301,x359301)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(35932,plain,
% 181.28/181.45 (~P5(f9(a1),f12(f9(a1)))),
% 181.28/181.45 inference(scs_inference,[],[3615,27202,1632,24338,4,35915,35918,35921,35924,35927,35930,3616,1854,76,77,44,39,56,46,78])).
% 181.28/181.45 cnf(35933,plain,
% 181.28/181.45 (~P5(x359331,x359331)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(35935,plain,
% 181.28/181.45 (~P5(f16(f11(a1)),f11(f16(f11(a1))))),
% 181.28/181.45 inference(scs_inference,[],[3615,27202,1632,24338,4,35915,35918,35921,35924,35927,35930,35933,3616,1854,76,77,44,39,56,46,78,81])).
% 181.28/181.45 cnf(35936,plain,
% 181.28/181.45 (~P5(x359361,x359361)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(35938,plain,
% 181.28/181.45 (~P20(f11(f16(f11(a1))))),
% 181.28/181.45 inference(scs_inference,[],[3615,27202,1632,24338,4,35915,35918,35921,35924,35927,35930,35933,35936,3616,1854,76,77,44,39,56,46,78,81,38])).
% 181.28/181.45 cnf(35939,plain,
% 181.28/181.45 (~P5(x359391,x359391)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(35951,plain,
% 181.28/181.45 (~P5(f9(a1),f16(f9(a1)))),
% 181.28/181.45 inference(scs_inference,[],[3615,1822,27202,1632,24338,4,35915,35918,35921,35924,35927,35930,35933,35936,35939,3616,1854,76,77,44,39,56,46,78,81,38,5,235,7,8,43,87])).
% 181.28/181.45 cnf(35952,plain,
% 181.28/181.45 (~P5(x359521,x359521)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(35954,plain,
% 181.28/181.45 (~P5(f10(a1),f12(f10(a1)))),
% 181.28/181.45 inference(scs_inference,[],[3615,1822,27202,1632,3634,24338,4,35915,35918,35921,35924,35927,35930,35933,35936,35939,35952,3616,1854,76,77,44,39,56,46,78,81,38,5,235,7,8,43,87,79])).
% 181.28/181.45 cnf(35960,plain,
% 181.28/181.45 (~P20(f9(f12(f10(f15(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[35929,4,43])).
% 181.28/181.45 cnf(35961,plain,
% 181.28/181.45 (~P5(x359611,x359611)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(35964,plain,
% 181.28/181.45 (~P5(x359641,x359641)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(35966,plain,
% 181.28/181.45 (~P5(f12(f10(f15(a1))),f9(f12(f10(f15(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[35929,4,35961,35964,43,77,76])).
% 181.28/181.45 cnf(35967,plain,
% 181.28/181.45 (~P5(x359671,x359671)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(35969,plain,
% 181.28/181.45 (~P6(f12(f16(f11(a1))))),
% 181.28/181.45 inference(scs_inference,[],[35929,35938,35935,4,35961,35964,43,77,76,45])).
% 181.28/181.45 cnf(35973,plain,
% 181.28/181.45 (~P5(f15(a1),f12(f15(a1)))),
% 181.28/181.45 inference(scs_inference,[],[35917,35920,35923,35929,35938,35935,4,35961,35964,43,77,76,45,87,79])).
% 181.28/181.45 cnf(35981,plain,
% 181.28/181.45 (P17(f11(f9(a1)))),
% 181.28/181.45 inference(scs_inference,[],[35917,35951,35920,35926,35923,35929,35938,35935,4,35961,35964,43,77,76,45,87,79,5,235,8,39])).
% 181.28/181.45 cnf(35988,plain,
% 181.28/181.45 (~P7(f16(f16(f11(a1))))),
% 181.28/181.45 inference(scs_inference,[],[35912,35917,35951,35920,35926,35923,35929,35938,35935,4,35961,35964,35967,43,77,76,45,87,79,5,235,8,39,44,46,56])).
% 181.28/181.45 cnf(35990,plain,
% 181.28/181.45 (~P5(f16(f11(a1)),f12(f16(f11(a1))))),
% 181.28/181.45 inference(scs_inference,[],[35912,35917,35951,35920,35926,35923,35929,35938,35935,4,35961,35964,35967,43,77,76,45,87,79,5,235,8,39,44,46,56,78])).
% 181.28/181.45 cnf(35992,plain,
% 181.28/181.45 (~P5(f9(a1),f11(f9(a1)))),
% 181.28/181.45 inference(scs_inference,[],[35912,35917,35951,35920,35926,35923,35929,35938,35935,4,35961,35964,35967,43,77,76,45,87,79,5,235,8,39,44,46,56,78,81])).
% 181.28/181.45 cnf(35994,plain,
% 181.28/181.45 (P17(f9(f12(f10(f15(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[35912,35917,35951,35920,35926,35923,35929,35938,35935,4,35961,35964,35967,43,77,76,45,87,79,5,235,8,39,44,46,56,78,81,34])).
% 181.28/181.45 cnf(36000,plain,
% 181.28/181.45 (~P6(f12(f12(f10(f15(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[35960,35966,45])).
% 181.28/181.45 cnf(36010,plain,
% 181.28/181.45 (~P6(f12(f11(f9(a1))))),
% 181.28/181.45 inference(scs_inference,[],[35914,35992,35981,35960,35966,45,102,38,5,235,8])).
% 181.28/181.45 cnf(36024,plain,
% 181.28/181.45 (~P21(f10(f16(f11(a1))))),
% 181.28/181.45 inference(scs_inference,[],[35973,35990,35969,39,44])).
% 181.28/181.45 cnf(36026,plain,
% 181.28/181.45 (~P6(f12(f15(a1)))),
% 181.28/181.45 inference(scs_inference,[],[35973,35990,35969,35917,35920,39,44,46])).
% 181.28/181.45 cnf(36028,plain,
% 181.28/181.45 (~P7(f16(f12(f10(f15(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[35973,35990,35994,35969,35917,35920,35966,39,44,46,56])).
% 181.28/181.45 cnf(36034,plain,
% 181.28/181.45 (~P20(f9(f12(f11(f9(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[35973,35990,35994,36010,35969,35917,35920,35966,4,39,44,46,56,5,7,43])).
% 181.28/181.45 cnf(36035,plain,
% 181.28/181.45 (~P5(x360351,x360351)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(36037,plain,
% 181.28/181.45 (~P5(f12(f11(f9(a1))),f9(f12(f11(f9(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[35973,35990,35994,36010,35969,35917,35920,35966,4,36035,39,44,46,56,5,7,43,76])).
% 181.28/181.45 cnf(36038,plain,
% 181.28/181.45 (~P5(x360381,x360381)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(36043,plain,
% 181.28/181.45 (~P5(f12(f10(f15(a1))),f16(f12(f10(f15(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[35973,35990,35994,36010,35969,35917,35920,35966,4,36035,36038,39,44,46,56,5,7,43,76,77,87])).
% 181.28/181.45 cnf(36045,plain,
% 181.28/181.45 (P20(f11(f16(a1)))+~P5(f16(a1),f12(f16(a1)))),
% 181.28/181.45 inference(scs_inference,[],[35973,35990,35994,36010,35969,35912,35917,35920,35966,4,36035,36038,39,44,46,56,5,7,43,76,77,87,78])).
% 181.28/181.45 cnf(36051,plain,
% 181.28/181.45 (~P20(f9(f9(a1)))),
% 181.28/181.45 inference(scs_inference,[],[36034,35932,1196,235,8,43])).
% 181.28/181.45 cnf(36057,plain,
% 181.28/181.45 (~P5(f10(f16(f11(a1))),f12(f10(f16(f11(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[36024,36034,35932,1196,4,235,8,43,77,76,79])).
% 181.28/181.45 cnf(36058,plain,
% 181.28/181.45 (~P5(x360581,x360581)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(36064,plain,
% 181.28/181.45 (~P6(f12(f12(f11(f9(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[36024,36028,36034,36037,36043,35932,1196,4,235,8,43,77,76,79,81,39,45])).
% 181.28/181.45 cnf(36067,plain,
% 181.28/181.45 (~P5(x360671,x360671)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(36072,plain,
% 181.28/181.45 (~P5(x360721,x360721)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(36074,plain,
% 181.28/181.45 (~P5(f12(f11(f9(a1))),f12(f12(f11(f9(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[36024,36028,36034,36037,36043,36000,35932,35954,1196,4,36058,36067,235,8,43,77,76,79,81,39,45,44,46,56,78])).
% 181.28/181.45 cnf(36076,plain,
% 181.28/181.45 (P17(f9(f12(f11(f9(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[36024,36028,36034,36037,36043,36000,35932,35954,1196,4,36058,36067,235,8,43,77,76,79,81,39,45,44,46,56,78,34])).
% 181.28/181.45 cnf(36085,plain,
% 181.28/181.45 (~P5(f12(f11(f9(a1))),f16(f12(f11(f9(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[36024,36028,36034,36037,36043,36000,35932,35954,1196,4,36058,36067,36072,235,8,43,77,76,79,81,39,45,44,46,56,78,34,38,5,7,87])).
% 181.28/181.45 cnf(36092,plain,
% 181.28/181.45 (~P6(f12(f9(f9(a1))))),
% 181.28/181.45 inference(scs_inference,[],[36051,235,8])).
% 181.28/181.45 cnf(36114,plain,
% 181.28/181.45 (P7(f16(f12(f11(f9(a1)))))+P17(f11(f12(f11(f9(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[36085,39])).
% 181.28/181.45 cnf(36118,plain,
% 181.28/181.45 (~P6(f12(f10(f16(f11(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[36085,36064,36074,36024,4,39,44,46])).
% 181.28/181.45 cnf(36121,plain,
% 181.28/181.45 (~P7(f16(f12(f11(f9(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[36076,36085,36064,36074,36024,36037,4,39,44,46,56])).
% 181.28/181.45 cnf(36129,plain,
% 181.28/181.45 (P17(f11(f12(f11(f9(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[36121,36114])).
% 181.28/181.45 cnf(36130,plain,
% 181.28/181.45 (~P20(f9(f10(f16(f11(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[36118,36121,36057,36114,43])).
% 181.28/181.45 cnf(36132,plain,
% 181.28/181.45 (~P5(f10(f16(f11(a1))),f9(f10(f16(f11(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[36118,36121,36057,36114,43,76])).
% 181.28/181.45 cnf(36140,plain,
% 181.28/181.45 (P17(f11(f16(a1)))),
% 181.28/181.45 inference(scs_inference,[],[36118,36121,36057,24334,4,36114,43,76,77,235,8,39])).
% 181.28/181.45 cnf(36141,plain,
% 181.28/181.45 (~P5(x361411,x361411)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(36145,plain,
% 181.28/181.45 (~P5(f16(a1),f16(f16(a1)))),
% 181.28/181.45 inference(scs_inference,[],[36118,36121,36057,35912,24334,4,36114,43,76,77,235,8,39,44,87])).
% 181.28/181.45 cnf(36149,plain,
% 181.28/181.45 (~P7(f16(f11(f12(f11(f9(a1))))))),
% 181.28/181.45 inference(scs_inference,[],[36118,36121,1822,36057,35912,24334,4,36141,36114,43,76,77,235,8,39,44,87,46,56])).
% 181.28/181.45 cnf(36158,plain,
% 181.28/181.45 (~P5(f12(f9(f9(a1))),f9(f12(f9(f9(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[36149,36092,4,7,76])).
% 181.28/181.45 cnf(36159,plain,
% 181.28/181.45 (~P5(x361591,x361591)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(36164,plain,
% 181.28/181.45 (~P5(f12(f11(f9(a1))),f11(f12(f11(f9(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[36149,36092,36121,36085,4,36159,7,76,77,81])).
% 181.28/181.45 cnf(36168,plain,
% 181.28/181.45 (P17(f9(f10(f16(f11(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[36145,36130,36132,36149,36092,36121,36085,4,36159,7,76,77,81,79,34])).
% 181.28/181.45 cnf(36170,plain,
% 181.28/181.45 (~P5(f10(f16(f11(a1))),f16(f10(f16(f11(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[36145,36130,36132,36149,36092,36121,36085,4,36159,7,76,77,81,79,34,87])).
% 181.28/181.45 cnf(36176,plain,
% 181.28/181.45 (~P5(f16(a1),f12(f16(a1)))),
% 181.28/181.45 inference(scs_inference,[],[36140,35912,38,36045])).
% 181.28/181.45 cnf(36181,plain,
% 181.28/181.45 (~P6(f12(f16(a1)))),
% 181.28/181.45 inference(scs_inference,[],[36140,35912,38,36045,235,8,45])).
% 181.28/181.45 cnf(36185,plain,
% 181.28/181.45 (~P5(f16(f16(f11(a1))),f11(f16(f16(f11(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[36140,36158,35988,35912,4,38,36045,235,8,45,78,81])).
% 181.28/181.45 cnf(36190,plain,
% 181.28/181.45 (~P4(f15(a1))+~P8(f18(f15(a1)))),
% 181.28/181.45 inference(scs_inference,[],[36140,36158,35988,35912,4,24363,24365,38,36045,235,8,45,78,81,5,68])).
% 181.28/181.45 cnf(36199,plain,
% 181.28/181.45 (~P6(f12(f10(f16(a1))))),
% 181.28/181.45 inference(scs_inference,[],[36181,36176,4,44,46])).
% 181.28/181.45 cnf(36200,plain,
% 181.28/181.45 (~P5(x362001,x362001)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(36204,plain,
% 181.28/181.45 (~P5(f10(f16(a1)),f12(f10(f16(a1))))),
% 181.28/181.45 inference(scs_inference,[],[36168,36181,36176,36132,4,36200,44,46,56,79])).
% 181.28/181.45 cnf(36215,plain,
% 181.28/181.45 (~P20(f11(f12(f11(f9(a1)))))),
% 181.28/181.45 inference(scs_inference,[],[36129,36168,36170,36181,36164,36176,36132,4,36200,44,46,56,79,5,7,43,102,38])).
% 181.28/181.45 cnf(36232,plain,
% 181.28/181.45 (~P20(f9(f10(f16(a1))))),
% 181.28/181.45 inference(scs_inference,[],[36199,36204,36215,235,8,43])).
% 181.28/181.45 cnf(36289,plain,
% 181.28/181.45 (~P6(f12(f10(a1)))),
% 181.28/181.45 inference(scs_inference,[],[4,3634,46])).
% 181.28/181.45 cnf(36290,plain,
% 181.28/181.45 (~P5(x362901,x362901)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.45 cnf(36293,plain,
% 181.28/181.45 (~P5(x362931,x362931)),
% 181.28/181.45 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(36295,plain,
% 181.28/181.46 (~P5(f11(a1),f9(f11(a1)))),
% 181.28/181.46 inference(scs_inference,[],[1561,4,36290,1806,3634,1567,46,87,76])).
% 181.28/181.46 cnf(36298,plain,
% 181.28/181.46 (~P5(x362981,x362981)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(36306,plain,
% 181.28/181.46 (~P20(f11(f11(a1)))),
% 181.28/181.46 inference(scs_inference,[],[1561,4,36290,36293,36298,1806,3634,1632,1567,24332,46,87,76,44,77,39,5,38])).
% 181.28/181.46 cnf(36319,plain,
% 181.28/181.46 (~P5(x363191,x363191)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(36322,plain,
% 181.28/181.46 (~P5(x363221,x363221)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(36325,plain,
% 181.28/181.46 (~P5(x363251,x363251)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(36328,plain,
% 181.28/181.46 (~P5(x363281,x363281)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(36331,plain,
% 181.28/181.46 (~P5(x363311,x363311)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(36334,plain,
% 181.28/181.46 (~P5(x363341,x363341)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(36342,plain,
% 181.28/181.46 (~P20(f11(f11(f16(f11(a1)))))),
% 181.28/181.46 inference(scs_inference,[],[4,36319,36322,36325,36328,36331,36334,1196,35923,36232,36306,235,34,56,87,76,44,77,39,8,7,38])).
% 181.28/181.46 cnf(36365,plain,
% 181.28/181.46 (~P7(f16(f9(f12(f10(f15(a1))))))),
% 181.28/181.46 inference(scs_inference,[],[4,35994,36342,235,56])).
% 181.28/181.46 cnf(36366,plain,
% 181.28/181.46 (~P5(x363661,x363661)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(36368,plain,
% 181.28/181.46 (~P5(f11(f16(a1)),f16(f11(f16(a1))))),
% 181.28/181.46 inference(scs_inference,[],[4,36366,35994,36140,36342,235,56,87])).
% 181.28/181.46 cnf(36390,plain,
% 181.28/181.46 (~P7(f16(f11(f16(a1))))),
% 181.28/181.46 inference(scs_inference,[],[4,36140,36365,7,56])).
% 181.28/181.46 cnf(36391,plain,
% 181.28/181.46 (~P5(x363911,x363911)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(36394,plain,
% 181.28/181.46 (~P5(x363941,x363941)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(36396,plain,
% 181.28/181.46 (~P5(f10(a1),f9(f10(a1)))),
% 181.28/181.46 inference(scs_inference,[],[4,36391,35954,36140,35981,36365,36289,7,56,87,76])).
% 181.28/181.46 cnf(36399,plain,
% 181.28/181.46 (~P5(x363991,x363991)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(36403,plain,
% 181.28/181.46 (P17(f11(f11(f16(a1))))),
% 181.28/181.46 inference(scs_inference,[],[4,36391,36394,36199,35954,36140,35981,36368,36365,36289,7,56,87,76,44,77,39])).
% 181.28/181.46 cnf(36414,plain,
% 181.28/181.46 (~P18(f12(f11(f11(f16(a1)))))),
% 181.28/181.46 inference(scs_inference,[],[4,36391,36394,36399,36176,36199,35954,36140,35981,36368,36365,36289,7,56,87,76,44,77,39,38,80,81,78,235])).
% 181.28/181.46 cnf(36427,plain,
% 181.28/181.46 (~P5(x364271,x364271)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(36432,plain,
% 181.28/181.46 (~P5(f16(f11(a1)),f9(f16(f11(a1))))),
% 181.28/181.46 inference(scs_inference,[],[4,36427,35981,35990,35969,36403,36414,36390,8,7,56,87,76])).
% 181.28/181.46 cnf(37212,plain,
% 181.28/181.46 (~P5(f15(a1),f18(f15(a1)))+~P4(f15(a1))),
% 181.28/181.46 inference(scs_inference,[],[36190,24385])).
% 181.28/181.46 cnf(37983,plain,
% 181.28/181.46 (~P5(x379831,x379831)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(37985,plain,
% 181.28/181.46 (~P17(f9(f10(a1)))+~P7(f16(f9(f10(a1))))),
% 181.28/181.46 inference(scs_inference,[],[4,37983,36396,38,34,56])).
% 181.28/181.46 cnf(37986,plain,
% 181.28/181.46 (~P5(x379861,x379861)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(37988,plain,
% 181.28/181.46 (~P17(f9(f10(a1)))+~P5(f9(f10(a1)),f16(f9(f10(a1))))),
% 181.28/181.46 inference(scs_inference,[],[4,37983,37986,36396,38,34,56,87])).
% 181.28/181.46 cnf(37995,plain,
% 181.28/181.46 (~P17(f9(f10(a1)))+~P19(f16(f9(f10(a1))))),
% 181.28/181.46 inference(scs_inference,[],[4,37983,37986,36396,38,34,56,87,235,8,7])).
% 181.28/181.46 cnf(39808,plain,
% 181.28/181.46 (~P5(x398081,x398081)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(39810,plain,
% 181.28/181.46 (~P17(f9(f16(f11(a1))))+~P7(f16(f9(f16(f11(a1)))))),
% 181.28/181.46 inference(scs_inference,[],[4,39808,36432,38,34,56])).
% 181.28/181.46 cnf(39811,plain,
% 181.28/181.46 (~P5(x398111,x398111)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(39813,plain,
% 181.28/181.46 (~P17(f9(f16(f11(a1))))+~P5(f9(f16(f11(a1))),f16(f9(f16(f11(a1)))))),
% 181.28/181.46 inference(scs_inference,[],[4,39808,39811,36432,38,34,56,87])).
% 181.28/181.46 cnf(39962,plain,
% 181.28/181.46 (~P5(x399621,x399621)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(39964,plain,
% 181.28/181.46 (~P17(f9(f11(a1)))+~P7(f16(f9(f11(a1))))),
% 181.28/181.46 inference(scs_inference,[],[4,39962,36295,38,34,56])).
% 181.28/181.46 cnf(39965,plain,
% 181.28/181.46 (~P5(x399651,x399651)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(39967,plain,
% 181.28/181.46 (~P17(f9(f11(a1)))+~P5(f16(f9(f11(a1))),f11(f16(f9(f11(a1)))))),
% 181.28/181.46 inference(scs_inference,[],[4,39962,39965,36295,38,34,56,81])).
% 181.28/181.46 cnf(39968,plain,
% 181.28/181.46 (~P5(x399681,x399681)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(39977,plain,
% 181.28/181.46 (~P17(f9(f11(a1)))+~P19(f16(f9(f11(a1))))),
% 181.28/181.46 inference(scs_inference,[],[4,39962,39965,39968,36295,38,34,56,81,87,235,8,7])).
% 181.28/181.46 cnf(40912,plain,
% 181.28/181.46 (~P20(f9(f12(f9(a1))))),
% 181.28/181.46 inference(scs_inference,[],[4,36185,1196,46,43])).
% 181.28/181.46 cnf(40915,plain,
% 181.28/181.46 (~P18(f12(f9(f12(f9(a1)))))),
% 181.28/181.46 inference(scs_inference,[],[4,36185,1196,46,43,235])).
% 181.28/181.46 cnf(40925,plain,
% 181.28/181.46 (~P5(x409251,x409251)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(40928,plain,
% 181.28/181.46 (~P5(x409281,x409281)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(40933,plain,
% 181.28/181.46 (~P20(f9(f11(a1)))),
% 181.28/181.46 inference(scs_inference,[],[4,40925,40928,1806,1567,40912,40915,8,34,56,87,43])).
% 181.28/181.46 cnf(40935,plain,
% 181.28/181.46 (~P18(f12(f9(f11(a1))))),
% 181.28/181.46 inference(scs_inference,[],[4,40925,40928,1806,1567,40912,40915,8,34,56,87,43,235])).
% 181.28/181.46 cnf(40941,plain,
% 181.28/181.46 (P17(f11(f9(f12(f9(a1)))))),
% 181.28/181.46 inference(scs_inference,[],[4,40925,40928,1806,1567,40912,40915,8,34,56,87,43,235,7,24,39])).
% 181.28/181.46 cnf(40952,plain,
% 181.28/181.46 (~P5(x409521,x409521)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(40954,plain,
% 181.28/181.46 (~P7(f16(f11(f9(f12(f9(a1))))))),
% 181.28/181.46 inference(scs_inference,[],[4,40952,40941,40933,40935,8,34,56])).
% 181.28/181.46 cnf(40955,plain,
% 181.28/181.46 (~P5(x409551,x409551)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(40958,plain,
% 181.28/181.46 (~P5(x409581,x409581)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(40963,plain,
% 181.28/181.46 (~P20(f9(f10(a1)))),
% 181.28/181.46 inference(scs_inference,[],[4,40952,40955,40958,35954,36289,40941,40933,40935,8,34,56,87,77,43])).
% 181.28/181.46 cnf(40965,plain,
% 181.28/181.46 (~P18(f12(f9(f10(a1))))),
% 181.28/181.46 inference(scs_inference,[],[4,40952,40955,40958,35954,36289,40941,40933,40935,8,34,56,87,77,43,235])).
% 181.28/181.46 cnf(40972,plain,
% 181.28/181.46 (P17(f11(f9(f11(a1))))),
% 181.28/181.46 inference(scs_inference,[],[4,40952,40955,40958,35954,36289,40941,40933,40935,8,34,56,87,77,43,235,39964,39967,39977,24,39])).
% 181.28/181.46 cnf(40985,plain,
% 181.28/181.46 (~P5(x409851,x409851)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(40987,plain,
% 181.28/181.46 (~P7(f16(f11(f9(f11(a1)))))),
% 181.28/181.46 inference(scs_inference,[],[4,40985,40972,40954,40963,40965,8,7,34,56])).
% 181.28/181.46 cnf(40988,plain,
% 181.28/181.46 (~P5(x409881,x409881)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(40991,plain,
% 181.28/181.46 (~P5(x409911,x409911)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(40996,plain,
% 181.28/181.46 (~P20(f9(f16(f11(a1))))),
% 181.28/181.46 inference(scs_inference,[],[4,40985,40988,40991,35990,35969,40972,40954,40963,40965,8,7,34,56,87,77,43])).
% 181.28/181.46 cnf(40998,plain,
% 181.28/181.46 (~P18(f12(f9(f16(f11(a1)))))),
% 181.28/181.46 inference(scs_inference,[],[4,40985,40988,40991,35990,35969,40972,40954,40963,40965,8,7,34,56,87,77,43,235])).
% 181.28/181.46 cnf(41000,plain,
% 181.28/181.46 (~P5(f9(f10(a1)),f16(f9(f10(a1))))),
% 181.28/181.46 inference(scs_inference,[],[4,40985,40988,40991,35990,35969,40972,40954,40963,40965,8,7,34,56,87,77,43,235,37988])).
% 181.28/181.46 cnf(41001,plain,
% 181.28/181.46 (~P7(f16(f9(f10(a1))))),
% 181.28/181.46 inference(scs_inference,[],[4,40985,40988,40991,35990,35969,40972,40954,40963,40965,8,7,34,56,87,77,43,235,37988,37985])).
% 181.28/181.46 cnf(41005,plain,
% 181.28/181.46 (P17(f11(f11(f9(f11(a1)))))),
% 181.28/181.46 inference(scs_inference,[],[4,40985,40988,40991,35990,35969,40972,40954,40963,40965,8,7,34,56,87,77,43,235,37988,37985,37995,24,39])).
% 181.28/181.46 cnf(41020,plain,
% 181.28/181.46 (~P5(x410201,x410201)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(41022,plain,
% 181.28/181.46 (~P7(f16(f11(f11(f9(f11(a1))))))),
% 181.28/181.46 inference(scs_inference,[],[4,41020,41005,41001,40987,41000,40996,40998,8,7,39,34,56])).
% 181.28/181.46 cnf(41023,plain,
% 181.28/181.46 (~P5(x410231,x410231)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(41028,plain,
% 181.28/181.46 (~P20(f9(f15(a1)))),
% 181.28/181.46 inference(scs_inference,[],[4,41020,41023,35973,36026,41005,41001,40987,41000,40996,40998,8,7,39,34,56,87,43])).
% 181.28/181.46 cnf(41030,plain,
% 181.28/181.46 (~P18(f12(f9(f15(a1))))),
% 181.28/181.46 inference(scs_inference,[],[4,41020,41023,35973,36026,41005,41001,40987,41000,40996,40998,8,7,39,34,56,87,43,235])).
% 181.28/181.46 cnf(41032,plain,
% 181.28/181.46 (~P7(f16(f9(f16(f11(a1)))))),
% 181.28/181.46 inference(scs_inference,[],[4,41020,41023,35973,36026,41005,41001,40987,41000,40996,40998,8,7,39,34,56,87,43,235,39810])).
% 181.28/181.46 cnf(41033,plain,
% 181.28/181.46 (~P5(f9(f16(f11(a1))),f16(f9(f16(f11(a1)))))),
% 181.28/181.46 inference(scs_inference,[],[4,41020,41023,35973,36026,41005,41001,40987,41000,40996,40998,8,7,39,34,56,87,43,235,39810,39813])).
% 181.28/181.46 cnf(41050,plain,
% 181.28/181.46 (P17(f9(f15(a1)))),
% 181.28/181.46 inference(scs_inference,[],[4,41032,41022,41033,41028,41030,8,7,39,34])).
% 181.28/181.46 cnf(44138,plain,
% 181.28/181.46 (~P5(f15(a1),f16(f15(a1)))),
% 181.28/181.46 inference(scs_inference,[],[41050,35914,87])).
% 181.28/181.46 cnf(44140,plain,
% 181.28/181.46 (~P7(f16(f15(a1)))),
% 181.28/181.46 inference(scs_inference,[],[41050,35914,87,56])).
% 181.28/181.46 cnf(44171,plain,
% 181.28/181.46 (P3(f15(a1))+P5(f15(a1),f18(f15(a1)))),
% 181.28/181.46 inference(scs_inference,[],[24363,24365,73,24387])).
% 181.28/181.46 cnf(44239,plain,
% 181.28/181.46 (~P5(x442391,x442391)),
% 181.28/181.46 inference(rename_variables,[],[4])).
% 181.28/181.46 cnf(44246,plain,
% 181.28/181.46 (~P8(f18(f15(a1)))),
% 181.28/181.46 inference(scs_inference,[],[4,44239,2,44138,44140,1567,24356,1806,24363,24365,24358,44,81,67,71,73,102,37212,58,35,97,68])).
% 181.28/181.46 cnf(44250,plain,
% 181.28/181.46 (~P5(f15(a1),f18(f15(a1)))),
% 181.28/181.46 inference(scs_inference,[],[44246,24385])).
% 181.28/181.46 cnf(44256,plain,
% 181.28/181.46 (P3(f15(a1))),
% 181.28/181.46 inference(scs_inference,[],[44246,24363,24365,24385,36,73,44171])).
% 181.28/181.46 cnf(44266,plain,
% 181.28/181.46 ($false),
% 181.28/181.46 inference(scs_inference,[],[44250,44256,24363,24365,72]),
% 181.28/181.46 ['proof']).
% 181.28/181.47 % SZS output end Proof
% 181.28/181.47 % Total time :180.680000s
%------------------------------------------------------------------------------