%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MED005+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 : 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 11:44:43 EDT 2024
% Result : Theorem 116.23s 116.26s
% Output : CNFRefutation 116.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : MED005+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.11/0.33 % Computer : n019.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Sat Jun 22 18:51:09 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.51/0.55 start to proof:theBenchmark
% 116.19/116.24 %-------------------------------------------
% 116.19/116.24 % File :CSE---1.7
% 116.19/116.24 % Problem :theBenchmark
% 116.19/116.24 % Transform :cnf
% 116.19/116.25 % Format :tptp:raw
% 116.19/116.25 % Command :java -jar mcs_scs.jar %d %s
% 116.19/116.25
% 116.19/116.25 % Result :Theorem 115.600000s
% 116.19/116.25 % Output :CNFRefutation 115.600000s
% 116.19/116.25 %-------------------------------------------
% 116.23/116.26 %------------------------------------------------------------------------------
% 116.23/116.26 % File : MED005+1 : TPTP v8.2.0. Released v3.2.0.
% 116.23/116.26 % Domain : Medicine
% 116.23/116.26 % Problem : Unsuccessful diet treatment
% 116.23/116.26 % Version : [HLB05] axioms : Especial.
% 116.23/116.26 % English : Unsuccessful treatment of diet requires that medical management
% 116.23/116.26 % moves to at least oral diabetics.
% 116.23/116.26
% 116.23/116.26 % Refs : [HLB05] Hommersom et al. (2005), Automated Theorem Proving for
% 116.23/116.26 % : [Hom06] Hommersom (2006), Email to G. Sutcliffe
% 116.23/116.26 % Source : [Hom06]
% 116.23/116.26 % Names :
% 116.23/116.26
% 116.23/116.26 % Status : Theorem
% 116.23/116.26 % Rating : 0.06 v8.2.0, 0.00 v8.1.0, 0.07 v7.5.0, 0.14 v7.4.0, 0.06 v7.3.0, 0.00 v7.0.0, 0.07 v6.3.0, 0.00 v6.2.0, 0.09 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.43 v5.0.0, 0.40 v4.1.0, 0.44 v4.0.1, 0.47 v4.0.0, 0.45 v3.7.0, 0.33 v3.5.0, 0.25 v3.4.0, 0.33 v3.3.0, 0.44 v3.2.0
% 116.23/116.26 % Syntax : Number of formulae : 41 ( 1 unt; 0 def)
% 116.23/116.26 % Number of atoms : 197 ( 0 equ)
% 116.23/116.26 % Maximal formula atoms : 30 ( 4 avg)
% 116.23/116.26 % Number of connectives : 239 ( 83 ~; 33 |; 48 &)
% 116.23/116.26 % ( 0 <=>; 75 =>; 0 <=; 0 <~>)
% 116.23/116.26 % Maximal formula depth : 12 ( 6 avg)
% 116.23/116.26 % Maximal term depth : 1 ( 1 avg)
% 116.23/116.26 % Number of predicates : 20 ( 20 usr; 0 prp; 1-2 aty)
% 116.23/116.26 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% 116.23/116.26 % Number of variables : 96 ( 92 !; 4 ?)
% 116.23/116.26 % SPC : FOF_THM_RFO_NEQ
% 116.23/116.26
% 116.23/116.26 % Comments :
% 116.23/116.26 %------------------------------------------------------------------------------
% 116.23/116.26 include('Axioms/MED001+0.ax').
% 116.23/116.26 include('Axioms/MED001+1.ax').
% 116.23/116.26 %------------------------------------------------------------------------------
% 116.23/116.26 fof(transs0s1,conjecture,
% 116.23/116.26 ( ( s0(n0)
% 116.23/116.26 & ! [X0] :
% 116.23/116.26 ( gt(n0,X0)
% 116.23/116.26 => conditionhyper(X0) ) )
% 116.23/116.26 => ? [X0] :
% 116.23/116.26 ( ~ gt(n0,X0)
% 116.23/116.26 & s1(X0)
% 116.23/116.26 & ! [X1] :
% 116.23/116.26 ( gt(X0,X1)
% 116.23/116.26 => conditionhyper(X1) ) ) ) ).
% 116.23/116.26
% 116.23/116.26 %------------------------------------------------------------------------------
% 116.23/116.26 %-------------------------------------------
% 116.23/116.26 % Proof found
% 116.23/116.26 % SZS status Theorem for theBenchmark
% 116.23/116.26 % SZS output start Proof
% 116.23/116.27 %ClaNum:163(EqnAxiom:0)
% 116.23/116.27 %VarNum:673(SingletonVarNum:219)
% 116.23/116.27 %MaxLitNum:8
% 116.23/116.27 %MaxfuncDepth:1
% 116.23/116.27 %SharedTerms:2
% 116.23/116.27 %goalClause: 1 34 50 61
% 116.23/116.27 %singleGoalClaCount:1
% 116.23/116.27 [1]P1(a1)
% 116.23/116.27 [2]~P2(x21,x21)
% 116.23/116.27 [3]~P17(x31)+P3(x31)
% 116.23/116.27 [4]~P18(x41)+P12(x41)
% 116.23/116.27 [5]~P18(x51)+P4(x51)
% 116.23/116.27 [6]~P3(x61)+P17(x61)
% 116.23/116.27 [9]~P6(x91)+~P5(x91)
% 116.23/116.27 [10]~P7(x101)+~P5(x101)
% 116.23/116.27 [11]~P7(x111)+~P6(x111)
% 116.23/116.27 [12]~P10(x121)+~P8(x121)
% 116.23/116.27 [13]~P11(x131)+~P8(x131)
% 116.23/116.27 [14]~P11(x141)+~P10(x141)
% 116.23/116.27 [15]~P19(x151)+~P1(x151)
% 116.23/116.27 [16]~P18(x161)+~P1(x161)
% 116.23/116.27 [17]~P17(x171)+~P1(x171)
% 116.23/116.27 [18]~P18(x181)+~P19(x181)
% 116.23/116.27 [19]~P17(x191)+~P19(x191)
% 116.23/116.27 [20]~P17(x201)+~P18(x201)
% 116.23/116.27 [34]P8(x341)+~P2(a1,x341)
% 116.23/116.27 [33]~P6(x331)+~P9(f2(x331))
% 116.23/116.27 [57]~P6(x571)+~P2(x571,f2(x571))
% 116.23/116.27 [7]P6(x71)+P7(x71)+P5(x71)
% 116.23/116.27 [8]P10(x81)+P11(x81)+P8(x81)
% 116.23/116.27 [21]P7(x211)+~P13(x211)+P5(x211)
% 116.23/116.27 [22]P14(x221)+~P19(x221)+P4(x221)
% 116.23/116.27 [24]~P14(x241)+~P19(x241)+P12(x241)
% 116.23/116.27 [35]P13(x351)+P6(x351)+~P11(f3(x351))
% 116.23/116.27 [50]~P19(x501)+P2(a1,x501)+~P8(f16(x501))
% 116.23/116.27 [61]~P19(x611)+P2(x611,f16(x611))+P2(a1,x611)
% 116.23/116.27 [62]P13(x621)+P6(x621)+~P2(x621,f3(x621))
% 116.23/116.27 [32]P16(x321)+P20(x321)+P2(x322,x321)
% 116.23/116.27 [36]~P20(x362)+~P16(x362)+P2(x361,x362)
% 116.23/116.27 [37]P4(x371)+P2(x372,x371)+P16(f11(x372))
% 116.23/116.27 [41]P3(x411)+P2(x412,x411)+~P20(f9(x412))
% 116.23/116.27 [42]P3(x421)+P2(x422,x421)+~P21(f10(x422))
% 116.23/116.27 [43]P20(x431)+P2(x432,x431)+~P3(f12(x432))
% 116.23/116.27 [44]P21(x441)+P2(x442,x441)+~P3(f12(x442))
% 116.23/116.27 [45]P12(x451)+P2(x452,x451)+~P9(f2(x452))
% 116.23/116.27 [55]~P16(x552)+P2(x551,x552)+~P4(f17(x551))
% 116.23/116.27 [72]P3(x721)+P2(x722,x721)+~P2(x722,f9(x722))
% 116.23/116.27 [73]P3(x731)+P2(x732,x731)+~P2(x732,f10(x732))
% 116.23/116.27 [74]P20(x741)+P2(x742,x741)+~P2(x742,f12(x742))
% 116.23/116.27 [75]P21(x751)+P2(x752,x751)+~P2(x752,f12(x752))
% 116.23/116.27 [76]P12(x761)+P2(x762,x761)+~P2(x762,f2(x762))
% 116.23/116.27 [77]P4(x771)+P2(x772,x771)+~P2(x772,f11(x772))
% 116.23/116.27 [83]~P16(x832)+P2(x831,x832)+~P2(x831,f17(x831))
% 116.23/116.27 [98]~P2(x981,x983)+P2(x981,x982)+~P2(x983,x982)
% 116.23/116.27 [23]P19(x231)+P18(x231)+P17(x231)+P1(x231)
% 116.23/116.27 [27]P18(x271)+P17(x271)+~P12(x271)+P19(x271)
% 116.23/116.27 [28]P18(x281)+P17(x281)+~P4(x281)+P19(x281)
% 116.23/116.27 [29]P17(x291)+P15(x291)+~P12(x291)+P18(x291)
% 116.23/116.27 [31]P17(x311)+~P4(x311)+~P14(x311)+P18(x311)
% 116.23/116.27 [38]P2(x381,x382)+~P13(x381)+P7(x381)+P9(x382)
% 116.23/116.27 [56]~P13(x561)+~P2(x561,x562)+P7(x561)+P8(x562)
% 116.23/116.27 [46]~P18(x462)+P11(x461)+P2(x462,x461)+P6(f13(x462))
% 116.23/116.27 [47]~P1(x472)+P11(x471)+P2(x472,x471)+P19(f14(x472))
% 116.23/116.28 [48]~P19(x482)+P11(x481)+P2(x482,x481)+P18(f15(x482))
% 116.23/116.28 [49]~P18(x492)+P11(x491)+P2(x492,x491)+P17(f13(x492))
% 116.23/116.28 [58]P2(x581,x582)+P6(x581)+P9(x582)+~P12(f18(x581))
% 116.23/116.28 [59]P2(x592,x591)+P20(x591)+P13(x592)+~P11(f3(x592))
% 116.23/116.28 [60]P2(x602,x601)+P21(x601)+P13(x602)+~P11(f3(x602))
% 116.23/116.28 [70]~P2(x702,x701)+P8(x701)+P13(x702)+~P11(f3(x702))
% 116.23/116.28 [84]P2(x841,x842)+P6(x841)+P9(x842)+~P2(x841,f18(x841))
% 116.23/116.28 [85]P2(x852,x851)+P20(x851)+P13(x852)+~P2(x852,f3(x852))
% 116.23/116.28 [86]P2(x862,x861)+P21(x861)+P13(x862)+~P2(x862,f3(x862))
% 116.23/116.28 [94]~P1(x942)+P11(x941)+P2(x942,x941)+~P2(x942,f14(x942))
% 116.23/116.28 [95]~P19(x952)+P11(x951)+P2(x952,x951)+~P2(x952,f15(x952))
% 116.23/116.28 [96]~P18(x962)+P11(x961)+P2(x962,x961)+~P2(x962,f13(x962))
% 116.23/116.28 [108]~P2(x1082,x1081)+P8(x1081)+P13(x1082)+~P2(x1082,f3(x1082))
% 116.23/116.28 [52]P2(x521,x522)+~P14(x521)+~P13(x521)+P5(x521)+P9(x522)
% 116.23/116.28 [53]P14(x531)+~P16(x532)+~P13(x531)+P5(x531)+P2(x531,x532)
% 116.23/116.28 [65]P14(x651)+~P13(x651)+~P2(x651,x652)+P5(x651)+P8(x652)
% 116.23/116.28 [67]~P14(x671)+~P13(x671)+~P2(x671,x672)+P5(x671)+P8(x672)
% 116.23/116.28 [69]~P19(x692)+P11(x691)+P2(x692,x691)+P5(f15(x692))+P6(f15(x692))
% 116.23/116.28 [105]~P1(x1053)+P8(x1051)+P2(x1053,x1052)+P11(x1052)+~P2(f14(x1053),x1051)
% 116.23/116.28 [106]~P19(x1063)+P8(x1061)+P2(x1063,x1062)+P11(x1062)+~P2(f15(x1063),x1061)
% 116.23/116.28 [107]~P18(x1073)+P8(x1071)+P2(x1073,x1072)+P11(x1072)+~P2(f13(x1073),x1071)
% 116.23/116.28 [93]P2(x932,x931)+~P7(x932)+P11(x931)+P14(x932)+P16(f19(x932))+~P8(f22(x932))
% 116.23/116.28 [104]P2(x1042,x1041)+~P7(x1042)+P11(x1041)+P14(x1042)+P2(x1042,f22(x1042))+P16(f19(x1042))
% 116.23/116.28 [114]~P7(x1142)+~P14(x1142)+P11(x1141)+P2(x1142,x1141)+~P8(f20(x1142))+~P9(f21(x1142))
% 116.23/116.28 [116]~P5(x1162)+P11(x1161)+P2(x1162,x1161)+P16(f23(x1162))+~P8(f4(x1162))+~P9(f5(x1162))
% 116.23/116.28 [117]~P7(x1172)+~P14(x1172)+P11(x1171)+P2(x1172,x1171)+P2(x1172,f20(x1172))+~P9(f21(x1172))
% 116.23/116.28 [123]~P5(x1232)+P11(x1231)+P2(x1232,x1231)+P2(x1232,f4(x1232))+P16(f23(x1232))+~P9(f5(x1232))
% 116.23/116.28 [126]~P5(x1262)+P11(x1261)+P2(x1262,x1261)+~P8(f4(x1262))+~P21(f24(x1262))+~P9(f5(x1262))
% 116.23/116.28 [130]P2(x1302,x1301)+~P7(x1302)+P11(x1301)+P14(x1302)+~P2(x1302,f19(x1302))+~P8(f22(x1302))
% 116.23/116.28 [131]~P5(x1312)+P11(x1311)+P2(x1312,x1311)+P2(x1312,f4(x1312))+~P21(f24(x1312))+~P9(f5(x1312))
% 116.23/116.28 [136]~P7(x1362)+~P14(x1362)+P11(x1361)+P2(x1362,x1361)+~P2(x1362,f21(x1362))+~P8(f20(x1362))
% 116.23/116.28 [138]P2(x1382,x1381)+~P7(x1382)+P11(x1381)+P14(x1382)+P2(x1382,f22(x1382))+~P2(x1382,f19(x1382))
% 116.23/116.28 [140]~P5(x1402)+P11(x1401)+P2(x1402,x1401)+~P2(x1402,f5(x1402))+P16(f23(x1402))+~P8(f4(x1402))
% 116.23/116.28 [141]~P7(x1412)+~P14(x1412)+P11(x1411)+P2(x1412,x1411)+P2(x1412,f20(x1412))+~P2(x1412,f21(x1412))
% 116.23/116.28 [144]~P5(x1442)+P11(x1441)+P2(x1442,x1441)+P2(x1442,f4(x1442))+~P2(x1442,f5(x1442))+P16(f23(x1442))
% 116.23/116.28 [145]~P5(x1452)+P11(x1451)+P2(x1452,x1451)+~P2(x1452,f5(x1452))+~P8(f4(x1452))+~P21(f24(x1452))
% 116.23/116.28 [146]~P5(x1462)+P11(x1461)+P2(x1462,x1461)+~P2(x1462,f23(x1462))+~P8(f4(x1462))+~P9(f5(x1462))
% 116.23/116.28 [147]~P5(x1472)+P11(x1471)+P2(x1472,x1471)+~P2(x1472,f24(x1472))+~P8(f4(x1472))+~P9(f5(x1472))
% 116.23/116.28 [149]~P5(x1492)+P11(x1491)+P2(x1492,x1491)+P2(x1492,f4(x1492))+~P2(x1492,f5(x1492))+~P21(f24(x1492))
% 116.23/116.28 [150]~P5(x1502)+P11(x1501)+P2(x1502,x1501)+P2(x1502,f4(x1502))+~P2(x1502,f23(x1502))+~P9(f5(x1502))
% 116.23/116.28 [151]~P5(x1512)+P11(x1511)+P2(x1512,x1511)+P2(x1512,f4(x1512))+~P2(x1512,f24(x1512))+~P9(f5(x1512))
% 116.23/116.28 [158]~P5(x1582)+P11(x1581)+P2(x1582,x1581)+~P2(x1582,f23(x1582))+~P2(x1582,f5(x1582))+~P8(f4(x1582))
% 116.23/116.28 [159]~P5(x1592)+P11(x1591)+P2(x1592,x1591)+~P2(x1592,f24(x1592))+~P2(x1592,f5(x1592))+~P8(f4(x1592))
% 116.23/116.28 [160]~P5(x1602)+P11(x1601)+P2(x1602,x1601)+P2(x1602,f4(x1602))+~P2(x1602,f23(x1602))+~P2(x1602,f5(x1602))
% 116.23/116.28 [161]~P5(x1612)+P11(x1611)+P2(x1612,x1611)+P2(x1612,f4(x1612))+~P2(x1612,f24(x1612))+~P2(x1612,f5(x1612))
% 116.23/116.28 [78]P2(x781,x782)+~P16(x783)+~P13(x781)+P5(x781)+P2(x781,x783)+P9(x782)
% 116.23/116.28 [79]P2(x791,x792)+~P16(x793)+~P13(x791)+P7(x791)+P2(x791,x793)+P21(x792)
% 116.23/116.28 [81]P2(x813,x812)+~P14(x813)+~P13(x813)+P9(x811)+P2(x813,x811)+P9(x812)
% 116.23/116.28 [82]P2(x822,x821)+~P16(x823)+~P13(x822)+P9(x821)+P2(x822,x823)+P14(x822)
% 116.23/116.28 [109]~P13(x1091)+~P2(x1091,x1092)+~P2(x1091,x1093)+P5(x1091)+P8(x1092)+P8(x1093)
% 116.23/116.28 [112]~P13(x1123)+~P2(x1123,x1121)+~P2(x1123,x1122)+P8(x1121)+P8(x1122)+P14(x1123)
% 116.23/116.28 [115]~P13(x1153)+~P2(x1153,x1151)+~P2(x1153,x1152)+P8(x1151)+P8(x1152)+~P14(x1153)
% 116.23/116.28 [134]P11(x1341)+~P6(x1342)+P10(x1341)+P2(x1342,x1341)+~P8(f6(x1342))+~P20(f7(x1342))+~P21(f8(x1342))
% 116.23/116.28 [139]P11(x1391)+~P6(x1392)+P10(x1391)+P2(x1392,x1391)+P2(x1392,f6(x1392))+~P20(f7(x1392))+~P21(f8(x1392))
% 116.23/116.28 [152]P11(x1521)+~P6(x1522)+P10(x1521)+P2(x1522,x1521)+~P2(x1522,f8(x1522))+~P8(f6(x1522))+~P20(f7(x1522))
% 116.23/116.28 [153]P11(x1531)+~P6(x1532)+P10(x1531)+P2(x1532,x1531)+~P2(x1532,f7(x1532))+~P8(f6(x1532))+~P21(f8(x1532))
% 116.23/116.28 [155]P11(x1551)+~P6(x1552)+P10(x1551)+P2(x1552,x1551)+P2(x1552,f6(x1552))+~P2(x1552,f8(x1552))+~P20(f7(x1552))
% 116.23/116.28 [156]P11(x1561)+~P6(x1562)+P10(x1561)+P2(x1562,x1561)+P2(x1562,f6(x1562))+~P2(x1562,f7(x1562))+~P21(f8(x1562))
% 116.23/116.28 [162]P11(x1621)+~P6(x1622)+P10(x1621)+P2(x1622,x1621)+~P2(x1622,f7(x1622))+~P2(x1622,f8(x1622))+~P8(f6(x1622))
% 116.23/116.28 [163]P11(x1631)+~P6(x1632)+P10(x1631)+P2(x1632,x1631)+P2(x1632,f6(x1632))+~P2(x1632,f7(x1632))+~P2(x1632,f8(x1632))
% 116.23/116.28 [113]P2(x1133,x1132)+~P16(x1134)+~P13(x1133)+P9(x1131)+P2(x1133,x1131)+P9(x1132)+P2(x1133,x1134)
% 116.23/116.28 [143]~P2(x1434,x1431)+~P2(x1434,x1432)+~P2(x1434,x1433)+P8(x1431)+P8(x1432)+P8(x1433)+~P13(x1434)
% 116.23/116.28 [122]P2(x1222,x1221)+~P16(x1223)+~P16(x1224)+~P13(x1222)+P21(x1221)+P2(x1222,x1223)+P14(x1222)+P2(x1222,x1224)
% 116.23/116.28 %EqnAxiom
% 116.23/116.28
% 116.23/116.28 %-------------------------------------------
% 116.23/116.29 cnf(164,plain,
% 116.23/116.29 (~P19(a1)),
% 116.23/116.29 inference(scs_inference,[],[1,15])).
% 116.23/116.29 cnf(166,plain,
% 116.23/116.29 (~P18(a1)),
% 116.23/116.29 inference(scs_inference,[],[1,15,16])).
% 116.23/116.29 cnf(168,plain,
% 116.23/116.29 (~P17(a1)),
% 116.23/116.29 inference(scs_inference,[],[1,15,16,17])).
% 116.23/116.29 cnf(172,plain,
% 116.23/116.29 (~P12(a1)),
% 116.23/116.29 inference(scs_inference,[],[1,15,16,17,6,27])).
% 116.23/116.29 cnf(174,plain,
% 116.23/116.29 (~P4(a1)),
% 116.23/116.29 inference(scs_inference,[],[1,15,16,17,6,27,28])).
% 116.23/116.29 cnf(176,plain,
% 116.23/116.29 (~P17(f12(x1761))+P20(x1761)),
% 116.23/116.29 inference(scs_inference,[],[2,3,43])).
% 116.23/116.29 cnf(571,plain,
% 116.23/116.29 (~P9(f2(a1))),
% 116.23/116.29 inference(scs_inference,[],[2,168,164,166,45,27])).
% 116.23/116.29 cnf(809,plain,
% 116.23/116.29 (~P2(a1,f10(a1))),
% 116.23/116.29 inference(scs_inference,[],[2,168,73,6])).
% 116.23/116.29 cnf(904,plain,
% 116.23/116.29 (~P2(a1,f11(a1))),
% 116.23/116.29 inference(scs_inference,[],[2,168,164,166,77,28])).
% 116.23/116.29 cnf(1932,plain,
% 116.23/116.29 (~P19(x19321)+~P3(x19321)),
% 116.23/116.29 inference(scs_inference,[],[6,19])).
% 116.23/116.29 cnf(2093,plain,
% 116.23/116.29 (~P21(f10(a1))),
% 116.23/116.29 inference(scs_inference,[],[168,2,6,42])).
% 116.23/116.29 cnf(24932,plain,
% 116.23/116.29 (P16(f11(a1))),
% 116.23/116.29 inference(scs_inference,[],[174,2,37])).
% 116.23/116.29 cnf(24933,plain,
% 116.23/116.29 (~P2(x249331,x249331)),
% 116.23/116.29 inference(rename_variables,[],[2])).
% 116.23/116.29 cnf(24937,plain,
% 116.23/116.29 (~P2(a1,f2(a1))),
% 116.23/116.29 inference(scs_inference,[],[174,172,2,24933,904,37,55,76])).
% 116.23/116.29 cnf(24940,plain,
% 116.23/116.29 (~P20(f11(a1))),
% 116.23/116.29 inference(scs_inference,[],[174,172,2,24933,904,37,55,76,36])).
% 116.23/116.29 cnf(24961,plain,
% 116.23/116.29 (~P13(a1)),
% 116.23/116.29 inference(scs_inference,[],[24932,24937,2093,571,809,904,75,32,113])).
% 116.23/116.29 cnf(24966,plain,
% 116.23/116.29 (~P11(f3(a1))),
% 116.23/116.29 inference(scs_inference,[],[24961,24940,904,59])).
% 116.23/116.29 cnf(24968,plain,
% 116.23/116.29 (~P2(a1,f3(a1))),
% 116.23/116.29 inference(scs_inference,[],[24961,24940,904,59,85])).
% 116.23/116.29 cnf(24970,plain,
% 116.23/116.29 (P19(f14(a1))),
% 116.23/116.29 inference(scs_inference,[],[1,24961,24940,904,59,85,47])).
% 116.23/116.29 cnf(24974,plain,
% 116.23/116.29 (~P2(a1,f14(a1))),
% 116.23/116.29 inference(scs_inference,[],[1,24961,24940,24937,571,904,59,85,47,84,94])).
% 116.23/116.29 cnf(24991,plain,
% 116.23/116.29 (P8(x249911)+~P2(f14(a1),x249911)),
% 116.23/116.29 inference(scs_inference,[],[1,24968,24966,24970,1932,15,105])).
% 116.23/116.29 cnf(27066,plain,
% 116.23/116.29 (~P3(f12(f11(a1)))),
% 116.23/116.29 inference(scs_inference,[],[24940,176,6])).
% 116.23/116.29 cnf(30879,plain,
% 116.23/116.29 (P8(f16(f14(a1)))),
% 116.23/116.29 inference(scs_inference,[],[24970,24974,24991,61])).
% 116.23/116.29 cnf(34050,plain,
% 116.23/116.29 ($false),
% 116.23/116.29 inference(scs_inference,[],[27066,30879,24970,24974,3,50]),
% 116.23/116.29 ['proof']).
% 116.23/116.30 % SZS output end Proof
% 116.23/116.30 % Total time :115.600000s
%------------------------------------------------------------------------------