%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MED010+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 : 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.22s 116.45s
% Output : CNFRefutation 116.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : MED010+1 : TPTP v8.2.0. Released v3.2.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n025.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % 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:52:39 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.20/0.56 start to proof:theBenchmark
% 116.22/116.43 %-------------------------------------------
% 116.22/116.43 % File :CSE---1.7
% 116.22/116.43 % Problem :theBenchmark
% 116.22/116.43 % Transform :cnf
% 116.22/116.43 % Format :tptp:raw
% 116.22/116.43 % Command :java -jar mcs_scs.jar %d %s
% 116.22/116.43
% 116.22/116.43 % Result :Theorem 115.600000s
% 116.22/116.43 % Output :CNFRefutation 115.600000s
% 116.22/116.43 %-------------------------------------------
% 116.22/116.44 %------------------------------------------------------------------------------
% 116.22/116.44 % File : MED010+1 : TPTP v8.2.0. Released v3.2.0.
% 116.22/116.44 % Domain : Medicine
% 116.22/116.44 % Problem : Unsuccessful s1-qilt27 treatment - two oral anti-diabetic
% 116.22/116.44 % Version : [HLB05] axioms : Especial.
% 116.22/116.44 % English : After unsuccessful treatment with two oral anti-diabetic medical
% 116.22/116.44 % management moves to next step.
% 116.22/116.44
% 116.22/116.44 % Refs : [HLB05] Hommersom et al. (2005), Automated Theorem Proving for
% 116.22/116.44 % : [Hom06] Hommersom (2006), Email to G. Sutcliffe
% 116.22/116.44 % Source : [Hom06]
% 116.22/116.44 % Names :
% 116.22/116.44
% 116.22/116.44 % Status : Theorem
% 116.22/116.44 % Rating : 0.12 v8.2.0, 0.07 v7.5.0, 0.19 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.00 v6.2.0, 0.18 v6.1.0, 0.28 v6.0.0, 0.25 v5.5.0, 0.46 v5.4.0, 0.43 v5.3.0, 0.48 v5.2.0, 0.29 v5.0.0, 0.35 v4.1.0, 0.39 v4.0.1, 0.42 v4.0.0, 0.45 v3.7.0, 0.00 v3.5.0, 0.12 v3.4.0, 0.33 v3.3.0, 0.44 v3.2.0
% 116.22/116.44 % Syntax : Number of formulae : 41 ( 1 unt; 0 def)
% 116.22/116.44 % Number of atoms : 199 ( 0 equ)
% 116.22/116.44 % Maximal formula atoms : 30 ( 4 avg)
% 116.22/116.44 % Number of connectives : 241 ( 83 ~; 33 |; 50 &)
% 116.22/116.44 % ( 0 <=>; 75 =>; 0 <=; 0 <~>)
% 116.22/116.44 % Maximal formula depth : 12 ( 6 avg)
% 116.22/116.44 % Maximal term depth : 1 ( 1 avg)
% 116.22/116.44 % Number of predicates : 20 ( 20 usr; 0 prp; 1-2 aty)
% 116.22/116.44 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% 116.22/116.44 % Number of variables : 96 ( 92 !; 4 ?)
% 116.22/116.44 % SPC : FOF_THM_RFO_NEQ
% 116.22/116.44
% 116.22/116.44 % Comments :
% 116.22/116.44 %------------------------------------------------------------------------------
% 116.22/116.44 include('Axioms/MED001+0.ax').
% 116.22/116.44 include('Axioms/MED001+1.ax').
% 116.22/116.44 %------------------------------------------------------------------------------
% 116.22/116.44 fof(unsuccesfuls2,conjecture,
% 116.22/116.44 ( ( s2(n0)
% 116.22/116.44 & ! [X0] :
% 116.22/116.44 ( gt(n0,X0)
% 116.22/116.44 => conditionhyper(X0) )
% 116.22/116.44 & bcapacityex(n0) )
% 116.22/116.44 => ? [X0] :
% 116.22/116.44 ( ~ gt(n0,X0)
% 116.22/116.44 & s3(X0)
% 116.22/116.44 & ! [X1] :
% 116.22/116.44 ( gt(X0,X1)
% 116.22/116.44 => conditionhyper(X1) )
% 116.22/116.44 & bcapacityex(X0) ) ) ).
% 116.22/116.44
% 116.22/116.44 %------------------------------------------------------------------------------
% 116.22/116.44 %-------------------------------------------
% 116.22/116.45 % Proof found
% 116.22/116.45 % SZS status Theorem for theBenchmark
% 116.22/116.45 % SZS output start Proof
% 116.22/116.45 %ClaNum:164(EqnAxiom:0)
% 116.22/116.45 %VarNum:675(SingletonVarNum:219)
% 116.22/116.45 %MaxLitNum:8
% 116.22/116.45 %MaxfuncDepth:1
% 116.22/116.45 %SharedTerms:3
% 116.22/116.45 %goalClause: 1 2 35 66 70
% 116.22/116.45 %singleGoalClaCount:2
% 116.22/116.45 [1]P1(a1)
% 116.22/116.45 [2]P2(a1)
% 116.22/116.45 [3]~P3(x31,x31)
% 116.22/116.45 [4]~P19(x41)+P4(x41)
% 116.22/116.45 [5]~P2(x51)+P12(x51)
% 116.22/116.45 [6]~P2(x61)+P5(x61)
% 116.22/116.45 [7]~P4(x71)+P19(x71)
% 116.22/116.45 [10]~P1(x101)+~P6(x101)
% 116.22/116.45 [11]~P7(x111)+~P6(x111)
% 116.22/116.45 [12]~P7(x121)+~P1(x121)
% 116.22/116.45 [13]~P10(x131)+~P8(x131)
% 116.22/116.45 [14]~P11(x141)+~P8(x141)
% 116.22/116.45 [15]~P11(x151)+~P10(x151)
% 116.22/116.45 [16]~P18(x161)+~P14(x161)
% 116.22/116.45 [17]~P2(x171)+~P14(x171)
% 116.22/116.45 [18]~P19(x181)+~P14(x181)
% 116.22/116.45 [19]~P2(x191)+~P18(x191)
% 116.22/116.45 [20]~P19(x201)+~P18(x201)
% 116.22/116.45 [21]~P19(x211)+~P2(x211)
% 116.22/116.45 [35]P8(x351)+~P3(a1,x351)
% 116.22/116.45 [34]~P1(x341)+~P9(f2(x341))
% 116.22/116.45 [57]~P1(x571)+~P3(x571,f2(x571))
% 116.22/116.45 [8]P1(x81)+P7(x81)+P6(x81)
% 116.22/116.45 [9]P10(x91)+P11(x91)+P8(x91)
% 116.22/116.45 [22]P7(x221)+~P13(x221)+P6(x221)
% 116.22/116.45 [23]P15(x231)+~P18(x231)+P5(x231)
% 116.22/116.45 [25]~P15(x251)+~P18(x251)+P12(x251)
% 116.22/116.45 [36]P13(x361)+P1(x361)+~P11(f3(x361))
% 116.22/116.45 [61]P13(x611)+P1(x611)+~P3(x611,f3(x611))
% 116.22/116.45 [33]P17(x331)+P20(x331)+P3(x332,x331)
% 116.22/116.45 [37]~P20(x372)+~P17(x372)+P3(x371,x372)
% 116.22/116.45 [38]P5(x381)+P3(x382,x381)+P17(f11(x382))
% 116.22/116.45 [42]P4(x421)+P3(x422,x421)+~P20(f9(x422))
% 116.22/116.45 [43]P4(x431)+P3(x432,x431)+~P21(f10(x432))
% 116.22/116.45 [44]P20(x441)+P3(x442,x441)+~P4(f12(x442))
% 116.22/116.45 [45]P21(x451)+P3(x452,x451)+~P4(f12(x452))
% 116.22/116.46 [46]P12(x461)+P3(x462,x461)+~P9(f2(x462))
% 116.22/116.46 [55]~P17(x552)+P3(x551,x552)+~P5(f16(x551))
% 116.22/116.46 [73]P4(x731)+P3(x732,x731)+~P3(x732,f9(x732))
% 116.22/116.46 [74]P4(x741)+P3(x742,x741)+~P3(x742,f10(x742))
% 116.22/116.46 [75]P20(x751)+P3(x752,x751)+~P3(x752,f12(x752))
% 116.22/116.46 [76]P21(x761)+P3(x762,x761)+~P3(x762,f12(x762))
% 116.22/116.46 [77]P12(x771)+P3(x772,x771)+~P3(x772,f2(x772))
% 116.22/116.46 [78]P5(x781)+P3(x782,x781)+~P3(x782,f11(x782))
% 116.22/116.46 [84]~P17(x842)+P3(x841,x842)+~P3(x841,f16(x841))
% 116.22/116.46 [99]~P3(x991,x993)+P3(x991,x992)+~P3(x993,x992)
% 116.22/116.46 [24]P18(x241)+P2(x241)+P19(x241)+P14(x241)
% 116.22/116.46 [28]P2(x281)+P19(x281)+~P12(x281)+P18(x281)
% 116.22/116.46 [29]P2(x291)+P19(x291)+~P5(x291)+P18(x291)
% 116.22/116.46 [30]P19(x301)+P16(x301)+~P12(x301)+P2(x301)
% 116.22/116.46 [32]P19(x321)+~P5(x321)+~P15(x321)+P2(x321)
% 116.22/116.46 [66]~P1(x661)+~P19(x661)+P3(a1,x661)+~P8(f18(x661))
% 116.22/116.46 [70]~P1(x701)+~P19(x701)+P3(x701,f18(x701))+P3(a1,x701)
% 116.22/116.46 [39]P3(x391,x392)+~P13(x391)+P7(x391)+P9(x392)
% 116.22/116.46 [56]~P13(x561)+~P3(x561,x562)+P7(x561)+P8(x562)
% 116.22/116.46 [47]~P2(x472)+P11(x471)+P3(x472,x471)+P1(f13(x472))
% 116.22/116.46 [48]~P14(x482)+P11(x481)+P3(x482,x481)+P18(f14(x482))
% 116.22/116.46 [49]~P18(x492)+P11(x491)+P3(x492,x491)+P2(f15(x492))
% 116.22/116.46 [50]~P2(x502)+P11(x501)+P3(x502,x501)+P19(f13(x502))
% 116.22/116.46 [58]P3(x581,x582)+P1(x581)+P9(x582)+~P12(f17(x581))
% 116.22/116.46 [59]P3(x592,x591)+P20(x591)+P13(x592)+~P11(f3(x592))
% 116.22/116.46 [60]P3(x602,x601)+P21(x601)+P13(x602)+~P11(f3(x602))
% 116.22/116.46 [71]~P3(x712,x711)+P8(x711)+P13(x712)+~P11(f3(x712))
% 116.22/116.46 [85]P3(x851,x852)+P1(x851)+P9(x852)+~P3(x851,f17(x851))
% 116.22/116.46 [86]P3(x862,x861)+P20(x861)+P13(x862)+~P3(x862,f3(x862))
% 116.22/116.46 [87]P3(x872,x871)+P21(x871)+P13(x872)+~P3(x872,f3(x872))
% 116.22/116.46 [95]~P14(x952)+P11(x951)+P3(x952,x951)+~P3(x952,f14(x952))
% 116.22/116.46 [96]~P18(x962)+P11(x961)+P3(x962,x961)+~P3(x962,f15(x962))
% 116.22/116.46 [97]~P2(x972)+P11(x971)+P3(x972,x971)+~P3(x972,f13(x972))
% 116.22/116.46 [109]~P3(x1092,x1091)+P8(x1091)+P13(x1092)+~P3(x1092,f3(x1092))
% 116.22/116.46 [52]P3(x521,x522)+~P15(x521)+~P13(x521)+P6(x521)+P9(x522)
% 116.22/116.46 [53]P15(x531)+~P17(x532)+~P13(x531)+P6(x531)+P3(x531,x532)
% 116.22/116.46 [64]P15(x641)+~P13(x641)+~P3(x641,x642)+P6(x641)+P8(x642)
% 116.22/116.46 [67]~P15(x671)+~P13(x671)+~P3(x671,x672)+P6(x671)+P8(x672)
% 116.22/116.46 [69]~P18(x692)+P11(x691)+P3(x692,x691)+P6(f15(x692))+P1(f15(x692))
% 116.22/116.46 [106]~P14(x1063)+P8(x1061)+P3(x1063,x1062)+P11(x1062)+~P3(f14(x1063),x1061)
% 116.22/116.46 [107]~P18(x1073)+P8(x1071)+P3(x1073,x1072)+P11(x1072)+~P3(f15(x1073),x1071)
% 116.22/116.46 [108]~P2(x1083)+P8(x1081)+P3(x1083,x1082)+P11(x1082)+~P3(f13(x1083),x1081)
% 116.22/116.46 [94]P3(x942,x941)+~P7(x942)+P11(x941)+P15(x942)+P17(f19(x942))+~P8(f22(x942))
% 116.22/116.46 [105]P3(x1052,x1051)+~P7(x1052)+P11(x1051)+P15(x1052)+P3(x1052,f22(x1052))+P17(f19(x1052))
% 116.22/116.46 [115]~P7(x1152)+~P15(x1152)+P11(x1151)+P3(x1152,x1151)+~P8(f20(x1152))+~P9(f21(x1152))
% 116.22/116.46 [117]~P6(x1172)+P11(x1171)+P3(x1172,x1171)+P17(f23(x1172))+~P8(f4(x1172))+~P9(f5(x1172))
% 116.22/116.46 [118]~P7(x1182)+~P15(x1182)+P11(x1181)+P3(x1182,x1181)+P3(x1182,f20(x1182))+~P9(f21(x1182))
% 116.22/116.46 [124]~P6(x1242)+P11(x1241)+P3(x1242,x1241)+P3(x1242,f4(x1242))+P17(f23(x1242))+~P9(f5(x1242))
% 116.22/116.46 [127]~P6(x1272)+P11(x1271)+P3(x1272,x1271)+~P8(f4(x1272))+~P21(f24(x1272))+~P9(f5(x1272))
% 116.22/116.46 [131]P3(x1312,x1311)+~P7(x1312)+P11(x1311)+P15(x1312)+~P3(x1312,f19(x1312))+~P8(f22(x1312))
% 116.22/116.46 [132]~P6(x1322)+P11(x1321)+P3(x1322,x1321)+P3(x1322,f4(x1322))+~P21(f24(x1322))+~P9(f5(x1322))
% 116.22/116.46 [137]~P7(x1372)+~P15(x1372)+P11(x1371)+P3(x1372,x1371)+~P3(x1372,f21(x1372))+~P8(f20(x1372))
% 116.22/116.46 [139]P3(x1392,x1391)+~P7(x1392)+P11(x1391)+P15(x1392)+P3(x1392,f22(x1392))+~P3(x1392,f19(x1392))
% 116.22/116.46 [141]~P6(x1412)+P11(x1411)+P3(x1412,x1411)+~P3(x1412,f5(x1412))+P17(f23(x1412))+~P8(f4(x1412))
% 116.22/116.46 [142]~P7(x1422)+~P15(x1422)+P11(x1421)+P3(x1422,x1421)+P3(x1422,f20(x1422))+~P3(x1422,f21(x1422))
% 116.22/116.46 [145]~P6(x1452)+P11(x1451)+P3(x1452,x1451)+P3(x1452,f4(x1452))+~P3(x1452,f5(x1452))+P17(f23(x1452))
% 116.22/116.46 [146]~P6(x1462)+P11(x1461)+P3(x1462,x1461)+~P3(x1462,f5(x1462))+~P8(f4(x1462))+~P21(f24(x1462))
% 116.22/116.46 [147]~P6(x1472)+P11(x1471)+P3(x1472,x1471)+~P3(x1472,f23(x1472))+~P8(f4(x1472))+~P9(f5(x1472))
% 116.22/116.46 [148]~P6(x1482)+P11(x1481)+P3(x1482,x1481)+~P3(x1482,f24(x1482))+~P8(f4(x1482))+~P9(f5(x1482))
% 116.22/116.46 [150]~P6(x1502)+P11(x1501)+P3(x1502,x1501)+P3(x1502,f4(x1502))+~P3(x1502,f5(x1502))+~P21(f24(x1502))
% 116.22/116.46 [151]~P6(x1512)+P11(x1511)+P3(x1512,x1511)+P3(x1512,f4(x1512))+~P3(x1512,f23(x1512))+~P9(f5(x1512))
% 116.22/116.46 [152]~P6(x1522)+P11(x1521)+P3(x1522,x1521)+P3(x1522,f4(x1522))+~P3(x1522,f24(x1522))+~P9(f5(x1522))
% 116.22/116.46 [159]~P6(x1592)+P11(x1591)+P3(x1592,x1591)+~P3(x1592,f23(x1592))+~P3(x1592,f5(x1592))+~P8(f4(x1592))
% 116.22/116.46 [160]~P6(x1602)+P11(x1601)+P3(x1602,x1601)+~P3(x1602,f24(x1602))+~P3(x1602,f5(x1602))+~P8(f4(x1602))
% 116.22/116.46 [161]~P6(x1612)+P11(x1611)+P3(x1612,x1611)+P3(x1612,f4(x1612))+~P3(x1612,f23(x1612))+~P3(x1612,f5(x1612))
% 116.22/116.46 [162]~P6(x1622)+P11(x1621)+P3(x1622,x1621)+P3(x1622,f4(x1622))+~P3(x1622,f24(x1622))+~P3(x1622,f5(x1622))
% 116.22/116.46 [79]P3(x791,x792)+~P17(x793)+~P13(x791)+P6(x791)+P3(x791,x793)+P9(x792)
% 116.22/116.46 [80]P3(x801,x802)+~P17(x803)+~P13(x801)+P7(x801)+P3(x801,x803)+P21(x802)
% 116.22/116.46 [82]P3(x823,x822)+~P15(x823)+~P13(x823)+P9(x821)+P3(x823,x821)+P9(x822)
% 116.22/116.46 [83]P3(x832,x831)+~P17(x833)+~P13(x832)+P9(x831)+P3(x832,x833)+P15(x832)
% 116.22/116.46 [110]~P13(x1101)+~P3(x1101,x1102)+~P3(x1101,x1103)+P6(x1101)+P8(x1102)+P8(x1103)
% 116.22/116.46 [113]~P13(x1133)+~P3(x1133,x1131)+~P3(x1133,x1132)+P8(x1131)+P8(x1132)+P15(x1133)
% 116.22/116.46 [116]~P13(x1163)+~P3(x1163,x1161)+~P3(x1163,x1162)+P8(x1161)+P8(x1162)+~P15(x1163)
% 116.22/116.46 [135]P11(x1351)+~P1(x1352)+P10(x1351)+P3(x1352,x1351)+~P8(f6(x1352))+~P20(f7(x1352))+~P21(f8(x1352))
% 116.22/116.46 [140]P11(x1401)+~P1(x1402)+P10(x1401)+P3(x1402,x1401)+P3(x1402,f6(x1402))+~P20(f7(x1402))+~P21(f8(x1402))
% 116.22/116.46 [153]P11(x1531)+~P1(x1532)+P10(x1531)+P3(x1532,x1531)+~P3(x1532,f8(x1532))+~P8(f6(x1532))+~P20(f7(x1532))
% 116.22/116.46 [154]P11(x1541)+~P1(x1542)+P10(x1541)+P3(x1542,x1541)+~P3(x1542,f7(x1542))+~P8(f6(x1542))+~P21(f8(x1542))
% 116.22/116.46 [156]P11(x1561)+~P1(x1562)+P10(x1561)+P3(x1562,x1561)+P3(x1562,f6(x1562))+~P3(x1562,f8(x1562))+~P20(f7(x1562))
% 116.22/116.46 [157]P11(x1571)+~P1(x1572)+P10(x1571)+P3(x1572,x1571)+P3(x1572,f6(x1572))+~P3(x1572,f7(x1572))+~P21(f8(x1572))
% 116.22/116.46 [163]P11(x1631)+~P1(x1632)+P10(x1631)+P3(x1632,x1631)+~P3(x1632,f7(x1632))+~P3(x1632,f8(x1632))+~P8(f6(x1632))
% 116.22/116.46 [164]P11(x1641)+~P1(x1642)+P10(x1641)+P3(x1642,x1641)+P3(x1642,f6(x1642))+~P3(x1642,f7(x1642))+~P3(x1642,f8(x1642))
% 116.22/116.46 [114]P3(x1143,x1142)+~P17(x1144)+~P13(x1143)+P9(x1141)+P3(x1143,x1141)+P9(x1142)+P3(x1143,x1144)
% 116.22/116.46 [144]~P3(x1444,x1441)+~P3(x1444,x1442)+~P3(x1444,x1443)+P8(x1441)+P8(x1442)+P8(x1443)+~P13(x1444)
% 116.22/116.46 [123]P3(x1232,x1231)+~P17(x1233)+~P17(x1234)+~P13(x1232)+P21(x1231)+P3(x1232,x1233)+P15(x1232)+P3(x1232,x1234)
% 116.22/116.46 %EqnAxiom
% 116.22/116.46
% 116.22/116.46 %-------------------------------------------
% 116.22/116.46 cnf(165,plain,
% 116.22/116.46 (~P7(a1)),
% 116.22/116.46 inference(scs_inference,[],[1,12])).
% 116.22/116.46 cnf(167,plain,
% 116.22/116.46 (~P19(a1)),
% 116.22/116.46 inference(scs_inference,[],[1,2,12,21])).
% 116.22/116.47 cnf(169,plain,
% 116.22/116.47 (~P4(a1)),
% 116.22/116.47 inference(scs_inference,[],[1,2,12,21,7])).
% 116.22/116.47 cnf(187,plain,
% 116.22/116.47 (~P19(f12(x1871))+P20(x1871)),
% 116.22/116.47 inference(scs_inference,[],[3,4,44])).
% 116.22/116.47 cnf(235,plain,
% 116.22/116.47 (~P13(a1)),
% 116.22/116.47 inference(scs_inference,[],[1,165,10,22])).
% 116.22/116.47 cnf(410,plain,
% 116.22/116.47 (~P19(f12(f9(a1)))),
% 116.22/116.47 inference(scs_inference,[],[169,3,187,42])).
% 116.22/116.47 cnf(411,plain,
% 116.22/116.47 (~P4(f12(f9(a1)))),
% 116.22/116.47 inference(scs_inference,[],[410,7])).
% 116.22/116.47 cnf(757,plain,
% 116.22/116.47 (~P17(x7571)+P3(x7572,x7571)+P17(f11(f16(x7572)))),
% 116.22/116.47 inference(scs_inference,[],[3,38,55])).
% 116.22/116.47 cnf(961,plain,
% 116.22/116.47 (~P3(a1,f9(a1))),
% 116.22/116.47 inference(scs_inference,[],[3,167,73,7])).
% 116.22/116.47 cnf(1008,plain,
% 116.22/116.47 (~P3(a1,f12(a1))),
% 116.22/116.47 inference(scs_inference,[],[961,169,3,75,42])).
% 116.22/116.47 cnf(1072,plain,
% 116.22/116.47 (~P17(f9(a1))+~P3(f16(a1),f11(f16(a1)))),
% 116.22/116.47 inference(scs_inference,[],[3,961,78,55])).
% 116.22/116.47 cnf(1817,plain,
% 116.22/116.47 (~P19(f12(a1))+P20(f9(a1))),
% 116.22/116.47 inference(scs_inference,[],[961,4,44])).
% 116.22/116.47 cnf(1833,plain,
% 116.22/116.47 (~P4(f12(a1))+P20(f9(a1))),
% 116.22/116.47 inference(scs_inference,[],[1817,7])).
% 116.22/116.47 cnf(1849,plain,
% 116.22/116.47 (P20(f9(a1))+~P21(f10(a1))),
% 116.22/116.47 inference(scs_inference,[],[1008,1833,43])).
% 116.22/116.47 cnf(1865,plain,
% 116.22/116.47 (~P17(f9(a1))+~P21(f10(a1))),
% 116.22/116.47 inference(scs_inference,[],[961,1849,37])).
% 116.22/116.47 cnf(1881,plain,
% 116.22/116.47 (~P17(f9(a1))+~P4(f12(f10(a1)))),
% 116.22/116.47 inference(scs_inference,[],[3,1865,45])).
% 116.22/116.47 cnf(1897,plain,
% 116.22/116.47 (~P19(f12(f10(a1)))+~P17(f9(a1))),
% 116.22/116.47 inference(scs_inference,[],[1881,4])).
% 116.22/116.47 cnf(1913,plain,
% 116.22/116.47 (P20(f9(a1))+~P19(f12(f10(a1)))),
% 116.22/116.47 inference(scs_inference,[],[961,1897,33])).
% 116.22/116.47 cnf(1929,plain,
% 116.22/116.47 (~P4(f12(f10(a1)))+P20(f9(a1))),
% 116.22/116.47 inference(scs_inference,[],[1913,7])).
% 116.22/116.47 cnf(1945,plain,
% 116.22/116.47 (P20(f9(a1))+~P20(f9(f12(f10(a1))))),
% 116.22/116.47 inference(scs_inference,[],[3,1929,42])).
% 116.22/116.47 cnf(3014,plain,
% 116.22/116.47 (~P19(f12(x30141))+P21(x30141)),
% 116.22/116.47 inference(scs_inference,[],[3,4,45])).
% 116.22/116.47 cnf(3030,plain,
% 116.22/116.47 (~P19(f12(f10(f12(f9(a1)))))),
% 116.22/116.47 inference(scs_inference,[],[3,411,3014,43])).
% 116.22/116.47 cnf(3468,plain,
% 116.22/116.47 (P20(x34681)+~P4(f12(x34681))),
% 116.22/116.47 inference(scs_inference,[],[7,187])).
% 116.22/116.47 cnf(3594,plain,
% 116.22/116.47 (~P20(f9(f12(f9(a1))))),
% 116.22/116.47 inference(scs_inference,[],[410,3,7,42])).
% 116.22/116.47 cnf(3610,plain,
% 116.22/116.47 (P21(x36101)+~P4(f12(x36101))),
% 116.22/116.47 inference(scs_inference,[],[7,3014])).
% 116.22/116.47 cnf(3642,plain,
% 116.22/116.47 (~P3(f12(f9(a1)),f9(f12(f9(a1))))),
% 116.22/116.47 inference(scs_inference,[],[410,3,7,73])).
% 116.22/116.47 cnf(3694,plain,
% 116.22/116.47 (~P3(f12(f9(a1)),f10(f12(f9(a1))))),
% 116.22/116.47 inference(scs_inference,[],[410,3,7,74])).
% 116.22/116.47 cnf(3741,plain,
% 116.22/116.47 (~P20(f9(a1))),
% 116.22/116.47 inference(scs_inference,[],[167,3,7,42])).
% 116.22/116.47 cnf(3747,plain,
% 116.22/116.47 (~P20(f9(f12(f10(a1))))),
% 116.22/116.47 inference(scs_inference,[],[3741,1945])).
% 116.22/116.47 cnf(4073,plain,
% 116.22/116.47 (~P3(a1,f10(a1))),
% 116.22/116.47 inference(scs_inference,[],[167,3,7,74])).
% 116.22/116.47 cnf(7175,plain,
% 116.22/116.47 (P17(f9(a1))),
% 116.22/116.47 inference(scs_inference,[],[3741,4073,961,37,33])).
% 116.22/116.47 cnf(7181,plain,
% 116.22/116.47 (~P3(f16(a1),f11(f16(a1)))),
% 116.22/116.47 inference(scs_inference,[],[7175,1072])).
% 116.22/116.47 cnf(7182,plain,
% 116.22/116.47 (~P21(f10(a1))),
% 116.22/116.47 inference(scs_inference,[],[7175,1865])).
% 116.22/116.47 cnf(7183,plain,
% 116.22/116.47 (~P4(f12(f10(a1)))),
% 116.22/116.47 inference(scs_inference,[],[7175,1881])).
% 116.22/116.47 cnf(10282,plain,
% 116.22/116.47 (~P4(f12(f9(f12(f10(a1)))))),
% 116.22/116.47 inference(scs_inference,[],[7183,3,3468,42])).
% 116.22/116.47 cnf(10298,plain,
% 116.22/116.47 (~P21(f10(f12(f9(a1))))),
% 116.22/116.47 inference(scs_inference,[],[3741,3,3468,43])).
% 116.22/116.47 cnf(10345,plain,
% 116.22/116.47 (~P3(f12(f10(a1)),f9(f12(f10(a1))))),
% 116.22/116.47 inference(scs_inference,[],[7182,3,3610,73])).
% 116.22/116.47 cnf(21551,plain,
% 116.22/116.47 (P17(f11(a1))),
% 116.22/116.47 inference(scs_inference,[],[7175,2,961,19,55,84,38])).
% 116.22/116.47 cnf(21553,plain,
% 116.22/116.47 (~P11(f3(a1))),
% 116.22/116.47 inference(scs_inference,[],[7175,3741,2,961,235,19,55,84,38,59])).
% 116.22/116.47 cnf(21555,plain,
% 116.22/116.47 (~P3(a1,f3(a1))),
% 116.22/116.47 inference(scs_inference,[],[7175,3741,2,961,235,19,55,84,38,59,86])).
% 116.22/116.47 cnf(21559,plain,
% 116.22/116.47 (~P3(a1,f11(a1))),
% 116.22/116.47 inference(scs_inference,[],[7175,3741,2,961,3,235,19,55,84,38,59,86,46,78])).
% 116.22/116.47 cnf(21563,plain,
% 116.22/116.47 (P19(f13(a1))),
% 116.22/116.47 inference(scs_inference,[],[7175,3741,2,961,3,235,19,55,84,38,59,86,46,78,37,50])).
% 116.22/116.47 cnf(21575,plain,
% 116.22/116.47 (P1(f13(a1))),
% 116.22/116.47 inference(scs_inference,[],[21555,21553,2,47])).
% 116.22/116.47 cnf(21577,plain,
% 116.22/116.47 (~P3(a1,f13(a1))),
% 116.22/116.47 inference(scs_inference,[],[21555,21553,2,47,97])).
% 116.22/116.47 cnf(21593,plain,
% 116.22/116.47 (P8(x215931)+~P3(f13(a1),x215931)),
% 116.22/116.47 inference(scs_inference,[],[21553,21555,2,108])).
% 116.22/116.47 cnf(24374,plain,
% 116.22/116.47 (P8(f18(f13(a1)))),
% 116.22/116.47 inference(scs_inference,[],[21575,21577,21563,21593,70])).
% 116.22/116.47 cnf(28887,plain,
% 116.22/116.47 (~P3(x288871,x288871)),
% 116.22/116.47 inference(rename_variables,[],[3])).
% 116.22/116.47 cnf(28898,plain,
% 116.22/116.47 ($false),
% 116.22/116.47 inference(scs_inference,[],[24374,3594,3747,10298,3642,3694,10345,3030,10282,7181,21559,21577,21551,3,28887,21563,21575,13,14,187,7,45,75,44,42,43,757,84,33,66]),
% 116.22/116.47 ['proof']).
% 116.22/116.47 % SZS output end Proof
% 116.22/116.47 % Total time :115.600000s
%------------------------------------------------------------------------------