%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MED006+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 28.21s 28.38s
% Output : CNFRefutation 28.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.10 % Problem : MED006+1 : TPTP v8.2.0. Released v3.2.0.
% 0.03/0.10 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.09/0.30 % Computer : n032.cluster.edu
% 0.09/0.30 % Model : x86_64 x86_64
% 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.30 % Memory : 8042.1875MB
% 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.30 % CPULimit : 300
% 0.09/0.30 % WCLimit : 300
% 0.09/0.30 % DateTime : Sat Jun 22 18:51:08 EDT 2024
% 0.09/0.30 % CPUTime :
% 0.16/0.50 start to proof:theBenchmark
% 28.21/28.38 %-------------------------------------------
% 28.21/28.38 % File :CSE---1.7
% 28.21/28.38 % Problem :theBenchmark
% 28.21/28.38 % Transform :cnf
% 28.21/28.38 % Format :tptp:raw
% 28.21/28.38 % Command :java -jar mcs_scs.jar %d %s
% 28.21/28.38
% 28.21/28.38 % Result :Theorem 27.790000s
% 28.21/28.38 % Output :CNFRefutation 27.790000s
% 28.21/28.38 %-------------------------------------------
% 28.21/28.38 %------------------------------------------------------------------------------
% 28.21/28.38 % File : MED006+1 : TPTP v8.2.0. Released v3.2.0.
% 28.21/28.38 % Domain : Medicine
% 28.21/28.38 % Problem : Unsuccessful s1-qilt27 treatment - single oral anti-diabetic
% 28.21/28.38 % Version : [HLB05] axioms : Especial.
% 28.21/28.38 % English : Unsuccessful treatment with single oral anti-diabetic for patients
% 28.21/28.38 % with QI less than 27 deductively follows in completed theory.
% 28.21/28.38
% 28.21/28.38 % Refs : [HLB05] Hommersom et al. (2005), Automated Theorem Proving for
% 28.21/28.38 % : [Hom06] Hommersom (2006), Email to G. Sutcliffe
% 28.21/28.38 % Source : [Hom06]
% 28.21/28.38 % Names :
% 28.21/28.38
% 28.21/28.38 % Status : Theorem
% 28.21/28.38 % Rating : 0.00 v7.5.0, 0.14 v7.4.0, 0.00 v7.0.0, 0.14 v6.4.0, 0.00 v6.2.0, 0.18 v6.1.0, 0.24 v6.0.0, 0.25 v5.5.0, 0.42 v5.4.0, 0.39 v5.3.0, 0.43 v5.2.0, 0.29 v5.0.0, 0.25 v4.1.0, 0.22 v4.0.1, 0.32 v4.0.0, 0.30 v3.7.0, 0.33 v3.5.0, 0.12 v3.4.0, 0.25 v3.3.0, 0.33 v3.2.0
% 28.21/28.38 % Syntax : Number of formulae : 41 ( 1 unt; 0 def)
% 28.21/28.38 % Number of atoms : 197 ( 0 equ)
% 28.21/28.38 % Maximal formula atoms : 30 ( 4 avg)
% 28.21/28.38 % Number of connectives : 241 ( 85 ~; 33 |; 48 &)
% 28.21/28.38 % ( 0 <=>; 75 =>; 0 <=; 0 <~>)
% 28.21/28.38 % Maximal formula depth : 12 ( 6 avg)
% 28.21/28.38 % Maximal term depth : 1 ( 1 avg)
% 28.21/28.38 % Number of predicates : 20 ( 20 usr; 0 prp; 1-2 aty)
% 28.21/28.38 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% 28.21/28.38 % Number of variables : 95 ( 92 !; 3 ?)
% 28.21/28.38 % SPC : FOF_THM_RFO_NEQ
% 28.21/28.38
% 28.21/28.38 % Comments :
% 28.21/28.38 %------------------------------------------------------------------------------
% 28.21/28.38 include('Axioms/MED001+0.ax').
% 28.21/28.38 include('Axioms/MED001+1.ax').
% 28.21/28.38 %------------------------------------------------------------------------------
% 28.21/28.38 fof(unsuccessfuls1_qilt27,conjecture,
% 28.21/28.38 ( ( s1(n0)
% 28.21/28.38 & ! [X0] :
% 28.21/28.38 ( gt(n0,X0)
% 28.21/28.38 => conditionhyper(X0) )
% 28.21/28.38 & ~ bcapacitysn(n0)
% 28.21/28.38 & qilt27(n0) )
% 28.21/28.38 => ~ ! [X0] :
% 28.21/28.38 ( ~ gt(n0,X0)
% 28.21/28.38 => conditionnormo(X0) ) ) ).
% 28.21/28.38
% 28.21/28.38 %------------------------------------------------------------------------------
% 28.21/28.38 %-------------------------------------------
% 28.21/28.38 % Proof found
% 28.21/28.38 % SZS status Theorem for theBenchmark
% 28.21/28.38 % SZS output start Proof
% 28.21/28.39 %ClaNum:164(EqnAxiom:0)
% 28.28/28.39 %VarNum:668(SingletonVarNum:218)
% 28.28/28.39 %MaxLitNum:8
% 28.28/28.39 %MaxfuncDepth:1
% 28.28/28.39 %SharedTerms:4
% 28.28/28.39 %goalClause: 1 2 3 25 37
% 28.28/28.39 %singleGoalClaCount:3
% 28.28/28.39 [1]P1(a1)
% 28.28/28.39 [2]P15(a1)
% 28.28/28.39 [3]~P2(a1)
% 28.28/28.39 [4]~P5(x41,x41)
% 28.28/28.39 [5]~P18(x51)+P6(x51)
% 28.28/28.39 [6]~P19(x61)+P12(x61)
% 28.28/28.39 [7]~P19(x71)+P7(x71)
% 28.28/28.39 [8]~P6(x81)+P18(x81)
% 28.28/28.39 [11]~P4(x111)+~P3(x111)
% 28.28/28.39 [12]~P2(x121)+~P3(x121)
% 28.28/28.39 [13]~P2(x131)+~P4(x131)
% 28.28/28.39 [14]~P10(x141)+~P8(x141)
% 28.28/28.39 [15]~P11(x151)+~P8(x151)
% 28.28/28.39 [16]~P11(x161)+~P10(x161)
% 28.28/28.39 [17]~P15(x171)+~P16(x171)
% 28.28/28.39 [18]~P19(x181)+~P16(x181)
% 28.28/28.39 [19]~P18(x191)+~P16(x191)
% 28.28/28.39 [20]~P19(x201)+~P15(x201)
% 28.28/28.39 [21]~P18(x211)+~P15(x211)
% 28.28/28.39 [22]~P18(x221)+~P19(x221)
% 28.28/28.39 [25]P11(x251)+P5(a1,x251)
% 28.28/28.39 [37]P8(x371)+~P5(a1,x371)
% 28.28/28.39 [36]~P4(x361)+~P9(f2(x361))
% 28.28/28.39 [59]~P4(x591)+~P5(x591,f2(x591))
% 28.28/28.39 [9]P4(x91)+P2(x91)+P3(x91)
% 28.28/28.39 [10]P10(x101)+P11(x101)+P8(x101)
% 28.28/28.39 [23]P2(x231)+~P13(x231)+P3(x231)
% 28.28/28.39 [24]P1(x241)+~P15(x241)+P7(x241)
% 28.28/28.39 [27]~P1(x271)+~P15(x271)+P12(x271)
% 28.28/28.39 [38]P13(x381)+P4(x381)+~P11(f3(x381))
% 28.28/28.39 [63]P13(x631)+P4(x631)+~P5(x631,f3(x631))
% 28.28/28.39 [35]P17(x351)+P20(x351)+P5(x352,x351)
% 28.28/28.39 [39]~P20(x392)+~P17(x392)+P5(x391,x392)
% 28.28/28.39 [40]P7(x401)+P5(x402,x401)+P17(f11(x402))
% 28.28/28.39 [44]P6(x441)+P5(x442,x441)+~P20(f9(x442))
% 28.28/28.39 [45]P6(x451)+P5(x452,x451)+~P21(f10(x452))
% 28.28/28.39 [46]P20(x461)+P5(x462,x461)+~P6(f12(x462))
% 28.28/28.39 [47]P21(x471)+P5(x472,x471)+~P6(f12(x472))
% 28.28/28.39 [48]P12(x481)+P5(x482,x481)+~P9(f2(x482))
% 28.28/28.39 [57]~P17(x572)+P5(x571,x572)+~P7(f16(x571))
% 28.28/28.39 [73]P6(x731)+P5(x732,x731)+~P5(x732,f9(x732))
% 28.28/28.39 [74]P6(x741)+P5(x742,x741)+~P5(x742,f10(x742))
% 28.28/28.39 [75]P20(x751)+P5(x752,x751)+~P5(x752,f12(x752))
% 28.28/28.39 [76]P21(x761)+P5(x762,x761)+~P5(x762,f12(x762))
% 28.28/28.39 [77]P12(x771)+P5(x772,x771)+~P5(x772,f2(x772))
% 28.28/28.39 [78]P7(x781)+P5(x782,x781)+~P5(x782,f11(x782))
% 28.28/28.39 [84]~P17(x842)+P5(x841,x842)+~P5(x841,f16(x841))
% 28.28/28.39 [99]~P5(x991,x993)+P5(x991,x992)+~P5(x993,x992)
% 28.28/28.39 [26]P15(x261)+P19(x261)+P18(x261)+P16(x261)
% 28.28/28.39 [30]P19(x301)+P18(x301)+~P12(x301)+P15(x301)
% 28.28/28.39 [31]P19(x311)+P18(x311)+~P7(x311)+P15(x311)
% 28.28/28.39 [32]P18(x321)+P14(x321)+~P12(x321)+P19(x321)
% 28.28/28.39 [34]P18(x341)+~P7(x341)+~P1(x341)+P19(x341)
% 28.28/28.39 [41]P5(x411,x412)+~P13(x411)+P2(x411)+P9(x412)
% 28.28/28.39 [58]~P13(x581)+~P5(x581,x582)+P2(x581)+P8(x582)
% 28.28/28.39 [49]~P19(x492)+P11(x491)+P5(x492,x491)+P4(f13(x492))
% 28.28/28.39 [50]~P16(x502)+P11(x501)+P5(x502,x501)+P15(f14(x502))
% 28.28/28.39 [51]~P15(x512)+P11(x511)+P5(x512,x511)+P19(f15(x512))
% 28.28/28.39 [52]~P19(x522)+P11(x521)+P5(x522,x521)+P18(f13(x522))
% 28.28/28.39 [60]P5(x601,x602)+P4(x601)+P9(x602)+~P12(f17(x601))
% 28.28/28.39 [61]P5(x612,x611)+P20(x611)+P13(x612)+~P11(f3(x612))
% 28.28/28.39 [62]P5(x622,x621)+P21(x621)+P13(x622)+~P11(f3(x622))
% 28.28/28.39 [71]~P5(x712,x711)+P8(x711)+P13(x712)+~P11(f3(x712))
% 28.28/28.39 [85]P5(x851,x852)+P4(x851)+P9(x852)+~P5(x851,f17(x851))
% 28.28/28.39 [86]P5(x862,x861)+P20(x861)+P13(x862)+~P5(x862,f3(x862))
% 28.28/28.39 [87]P5(x872,x871)+P21(x871)+P13(x872)+~P5(x872,f3(x872))
% 28.28/28.39 [95]~P16(x952)+P11(x951)+P5(x952,x951)+~P5(x952,f14(x952))
% 28.28/28.39 [96]~P15(x962)+P11(x961)+P5(x962,x961)+~P5(x962,f15(x962))
% 28.28/28.39 [97]~P19(x972)+P11(x971)+P5(x972,x971)+~P5(x972,f13(x972))
% 28.28/28.39 [109]~P5(x1092,x1091)+P8(x1091)+P13(x1092)+~P5(x1092,f3(x1092))
% 28.28/28.39 [54]P5(x541,x542)+~P1(x541)+~P13(x541)+P3(x541)+P9(x542)
% 28.28/28.39 [55]P1(x551)+~P17(x552)+~P13(x551)+P3(x551)+P5(x551,x552)
% 28.28/28.39 [66]P1(x661)+~P13(x661)+~P5(x661,x662)+P3(x661)+P8(x662)
% 28.28/28.39 [68]~P1(x681)+~P13(x681)+~P5(x681,x682)+P3(x681)+P8(x682)
% 28.28/28.39 [70]~P15(x702)+P11(x701)+P5(x702,x701)+P3(f15(x702))+P4(f15(x702))
% 28.28/28.39 [106]~P16(x1063)+P8(x1061)+P5(x1063,x1062)+P11(x1062)+~P5(f14(x1063),x1061)
% 28.28/28.39 [107]~P15(x1073)+P8(x1071)+P5(x1073,x1072)+P11(x1072)+~P5(f15(x1073),x1071)
% 28.28/28.39 [108]~P19(x1083)+P8(x1081)+P5(x1083,x1082)+P11(x1082)+~P5(f13(x1083),x1081)
% 28.28/28.39 [94]P5(x942,x941)+~P2(x942)+P11(x941)+P1(x942)+P17(f18(x942))+~P8(f21(x942))
% 28.28/28.39 [105]P5(x1052,x1051)+~P2(x1052)+P11(x1051)+P1(x1052)+P5(x1052,f21(x1052))+P17(f18(x1052))
% 28.28/28.39 [115]~P2(x1152)+~P1(x1152)+P11(x1151)+P5(x1152,x1151)+~P8(f19(x1152))+~P9(f20(x1152))
% 28.28/28.39 [117]~P3(x1172)+P11(x1171)+P5(x1172,x1171)+P17(f22(x1172))+~P8(f4(x1172))+~P9(f5(x1172))
% 28.28/28.39 [118]~P2(x1182)+~P1(x1182)+P11(x1181)+P5(x1182,x1181)+P5(x1182,f19(x1182))+~P9(f20(x1182))
% 28.28/28.39 [124]~P3(x1242)+P11(x1241)+P5(x1242,x1241)+P5(x1242,f4(x1242))+P17(f22(x1242))+~P9(f5(x1242))
% 28.28/28.39 [127]~P3(x1272)+P11(x1271)+P5(x1272,x1271)+~P8(f4(x1272))+~P21(f23(x1272))+~P9(f5(x1272))
% 28.28/28.39 [131]P5(x1312,x1311)+~P2(x1312)+P11(x1311)+P1(x1312)+~P5(x1312,f18(x1312))+~P8(f21(x1312))
% 28.28/28.39 [132]~P3(x1322)+P11(x1321)+P5(x1322,x1321)+P5(x1322,f4(x1322))+~P21(f23(x1322))+~P9(f5(x1322))
% 28.28/28.39 [137]~P2(x1372)+~P1(x1372)+P11(x1371)+P5(x1372,x1371)+~P5(x1372,f20(x1372))+~P8(f19(x1372))
% 28.28/28.39 [139]P5(x1392,x1391)+~P2(x1392)+P11(x1391)+P1(x1392)+P5(x1392,f21(x1392))+~P5(x1392,f18(x1392))
% 28.28/28.39 [141]~P3(x1412)+P11(x1411)+P5(x1412,x1411)+~P5(x1412,f5(x1412))+P17(f22(x1412))+~P8(f4(x1412))
% 28.28/28.39 [142]~P2(x1422)+~P1(x1422)+P11(x1421)+P5(x1422,x1421)+P5(x1422,f19(x1422))+~P5(x1422,f20(x1422))
% 28.28/28.39 [145]~P3(x1452)+P11(x1451)+P5(x1452,x1451)+P5(x1452,f4(x1452))+~P5(x1452,f5(x1452))+P17(f22(x1452))
% 28.28/28.39 [146]~P3(x1462)+P11(x1461)+P5(x1462,x1461)+~P5(x1462,f5(x1462))+~P8(f4(x1462))+~P21(f23(x1462))
% 28.28/28.39 [147]~P3(x1472)+P11(x1471)+P5(x1472,x1471)+~P5(x1472,f22(x1472))+~P8(f4(x1472))+~P9(f5(x1472))
% 28.28/28.39 [148]~P3(x1482)+P11(x1481)+P5(x1482,x1481)+~P5(x1482,f23(x1482))+~P8(f4(x1482))+~P9(f5(x1482))
% 28.28/28.39 [150]~P3(x1502)+P11(x1501)+P5(x1502,x1501)+P5(x1502,f4(x1502))+~P5(x1502,f5(x1502))+~P21(f23(x1502))
% 28.28/28.39 [151]~P3(x1512)+P11(x1511)+P5(x1512,x1511)+P5(x1512,f4(x1512))+~P5(x1512,f22(x1512))+~P9(f5(x1512))
% 28.28/28.39 [152]~P3(x1522)+P11(x1521)+P5(x1522,x1521)+P5(x1522,f4(x1522))+~P5(x1522,f23(x1522))+~P9(f5(x1522))
% 28.28/28.39 [159]~P3(x1592)+P11(x1591)+P5(x1592,x1591)+~P5(x1592,f22(x1592))+~P5(x1592,f5(x1592))+~P8(f4(x1592))
% 28.28/28.39 [160]~P3(x1602)+P11(x1601)+P5(x1602,x1601)+~P5(x1602,f23(x1602))+~P5(x1602,f5(x1602))+~P8(f4(x1602))
% 28.28/28.39 [161]~P3(x1612)+P11(x1611)+P5(x1612,x1611)+P5(x1612,f4(x1612))+~P5(x1612,f22(x1612))+~P5(x1612,f5(x1612))
% 28.28/28.39 [162]~P3(x1622)+P11(x1621)+P5(x1622,x1621)+P5(x1622,f4(x1622))+~P5(x1622,f23(x1622))+~P5(x1622,f5(x1622))
% 28.28/28.39 [79]P5(x791,x792)+~P17(x793)+~P13(x791)+P3(x791)+P5(x791,x793)+P9(x792)
% 28.28/28.39 [80]P5(x801,x802)+~P17(x803)+~P13(x801)+P2(x801)+P5(x801,x803)+P21(x802)
% 28.28/28.39 [82]P5(x823,x822)+~P1(x823)+~P13(x823)+P9(x821)+P5(x823,x821)+P9(x822)
% 28.28/28.39 [83]P5(x832,x831)+~P17(x833)+~P13(x832)+P9(x831)+P5(x832,x833)+P1(x832)
% 28.28/28.39 [110]~P13(x1101)+~P5(x1101,x1102)+~P5(x1101,x1103)+P3(x1101)+P8(x1102)+P8(x1103)
% 28.28/28.39 [113]~P13(x1133)+~P5(x1133,x1131)+~P5(x1133,x1132)+P8(x1131)+P8(x1132)+P1(x1133)
% 28.28/28.39 [116]~P13(x1163)+~P5(x1163,x1161)+~P5(x1163,x1162)+P8(x1161)+P8(x1162)+~P1(x1163)
% 28.28/28.39 [135]P11(x1351)+~P4(x1352)+P10(x1351)+P5(x1352,x1351)+~P8(f6(x1352))+~P20(f7(x1352))+~P21(f8(x1352))
% 28.28/28.39 [140]P11(x1401)+~P4(x1402)+P10(x1401)+P5(x1402,x1401)+P5(x1402,f6(x1402))+~P20(f7(x1402))+~P21(f8(x1402))
% 28.28/28.39 [153]P11(x1531)+~P4(x1532)+P10(x1531)+P5(x1532,x1531)+~P5(x1532,f8(x1532))+~P8(f6(x1532))+~P20(f7(x1532))
% 28.28/28.39 [154]P11(x1541)+~P4(x1542)+P10(x1541)+P5(x1542,x1541)+~P5(x1542,f7(x1542))+~P8(f6(x1542))+~P21(f8(x1542))
% 28.28/28.39 [156]P11(x1561)+~P4(x1562)+P10(x1561)+P5(x1562,x1561)+P5(x1562,f6(x1562))+~P5(x1562,f8(x1562))+~P20(f7(x1562))
% 28.28/28.39 [157]P11(x1571)+~P4(x1572)+P10(x1571)+P5(x1572,x1571)+P5(x1572,f6(x1572))+~P5(x1572,f7(x1572))+~P21(f8(x1572))
% 28.28/28.39 [163]P11(x1631)+~P4(x1632)+P10(x1631)+P5(x1632,x1631)+~P5(x1632,f7(x1632))+~P5(x1632,f8(x1632))+~P8(f6(x1632))
% 28.28/28.39 [164]P11(x1641)+~P4(x1642)+P10(x1641)+P5(x1642,x1641)+P5(x1642,f6(x1642))+~P5(x1642,f7(x1642))+~P5(x1642,f8(x1642))
% 28.28/28.39 [114]P5(x1143,x1142)+~P17(x1144)+~P13(x1143)+P9(x1141)+P5(x1143,x1141)+P9(x1142)+P5(x1143,x1144)
% 28.28/28.39 [144]~P5(x1444,x1441)+~P5(x1444,x1442)+~P5(x1444,x1443)+P8(x1441)+P8(x1442)+P8(x1443)+~P13(x1444)
% 28.28/28.39 [123]P5(x1232,x1231)+~P17(x1233)+~P17(x1234)+~P13(x1232)+P21(x1231)+P5(x1232,x1233)+P1(x1232)+P5(x1232,x1234)
% 28.28/28.39 %EqnAxiom
% 28.28/28.39
% 28.28/28.39 %-------------------------------------------
% 28.28/28.41 cnf(170,plain,
% 28.28/28.41 (~P18(a1)),
% 28.28/28.41 inference(scs_inference,[],[2,4,25,20,21])).
% 28.28/28.41 cnf(172,plain,
% 28.28/28.41 (~P6(a1)),
% 28.28/28.41 inference(scs_inference,[],[2,4,25,20,21,8])).
% 28.28/28.41 cnf(176,plain,
% 28.28/28.41 (P3(a1)+P4(a1)),
% 28.28/28.41 inference(scs_inference,[],[1,2,3,4,25,20,21,8,27,9])).
% 28.28/28.41 cnf(1359,plain,
% 28.28/28.41 (~P5(a1,f2(a1))+P3(a1)),
% 28.28/28.41 inference(scs_inference,[],[59,176])).
% 28.28/28.41 cnf(1407,plain,
% 28.28/28.41 (P11(f2(a1))+P3(a1)),
% 28.28/28.41 inference(scs_inference,[],[1359,25])).
% 28.28/28.41 cnf(1823,plain,
% 28.28/28.41 (~P5(a1,f10(a1))),
% 28.28/28.41 inference(scs_inference,[],[4,170,74,8])).
% 28.28/28.41 cnf(1872,plain,
% 28.28/28.41 (~P5(a1,f12(a1))),
% 28.28/28.41 inference(scs_inference,[],[1823,172,4,76,45])).
% 28.28/28.41 cnf(2001,plain,
% 28.28/28.41 (~P5(x20011,f10(a1))+P11(x20011)),
% 28.28/28.41 inference(scs_inference,[],[1823,99,25])).
% 28.28/28.41 cnf(3943,plain,
% 28.28/28.41 (~P20(f9(a1))),
% 28.28/28.41 inference(scs_inference,[],[170,4,8,44])).
% 28.28/28.41 cnf(3944,plain,
% 28.28/28.41 (P17(f9(a1))),
% 28.28/28.41 inference(scs_inference,[],[3943,4,35])).
% 28.28/28.41 cnf(3962,plain,
% 28.28/28.41 (~P21(f10(a1))),
% 28.28/28.41 inference(scs_inference,[],[170,4,8,45])).
% 28.28/28.41 cnf(4152,plain,
% 28.28/28.41 (~P5(a1,f9(a1))),
% 28.28/28.41 inference(scs_inference,[],[170,4,8,73])).
% 28.28/28.41 cnf(4185,plain,
% 28.28/28.41 (~P4(a1)+P11(f2(a1))),
% 28.28/28.41 inference(scs_inference,[],[11,1407])).
% 28.28/28.41 cnf(4201,plain,
% 28.28/28.41 (~P8(f2(a1))+~P4(a1)),
% 28.28/28.41 inference(scs_inference,[],[4185,15])).
% 28.28/28.41 cnf(4217,plain,
% 28.28/28.41 (~P13(x42171)+~P5(x42171,f2(a1))+~P4(a1)),
% 28.28/28.41 inference(scs_inference,[],[4201,144])).
% 28.28/28.41 cnf(4233,plain,
% 28.28/28.41 (~P13(a1)+P9(f2(a1))+~P4(a1)),
% 28.28/28.41 inference(scs_inference,[],[3,4217,41])).
% 28.28/28.41 cnf(4249,plain,
% 28.28/28.41 (~P4(a1)+~P13(a1)),
% 28.28/28.41 inference(scs_inference,[],[4233,36])).
% 28.28/28.41 cnf(4265,plain,
% 28.28/28.41 (~P13(a1)+P3(a1)),
% 28.28/28.41 inference(scs_inference,[],[4249,176])).
% 28.28/28.41 cnf(4281,plain,
% 28.28/28.41 (~P5(a1,f3(a1))+P3(a1)),
% 28.28/28.41 inference(scs_inference,[],[3962,1823,4265,87])).
% 28.28/28.41 cnf(4297,plain,
% 28.28/28.41 (P11(f3(a1))+P3(a1)),
% 28.28/28.41 inference(scs_inference,[],[4281,25])).
% 28.28/28.41 cnf(4313,plain,
% 28.28/28.41 (P13(a1)+P3(a1)),
% 28.28/28.41 inference(scs_inference,[],[3943,4152,4297,61])).
% 28.28/28.41 cnf(4329,plain,
% 28.28/28.41 (P3(a1)),
% 28.28/28.41 inference(scs_inference,[],[3,4152,3962,1823,3944,4313,80])).
% 28.28/28.41 cnf(4347,plain,
% 28.28/28.41 (P13(a1)+~P11(f3(a1))),
% 28.28/28.41 inference(scs_inference,[],[4329,11,38])).
% 28.28/28.41 cnf(4363,plain,
% 28.28/28.41 (~P5(f3(a1),f10(a1))+P13(a1)),
% 28.28/28.41 inference(scs_inference,[],[4347,2001])).
% 28.28/28.41 cnf(4379,plain,
% 28.28/28.41 (P13(a1)+~P6(f12(f3(a1)))),
% 28.28/28.41 inference(scs_inference,[],[3962,4363,47])).
% 28.28/28.41 cnf(4426,plain,
% 28.28/28.41 (P13(a1)+~P5(a1,f3(a1))),
% 28.28/28.41 inference(scs_inference,[],[4329,11,63])).
% 28.28/28.41 cnf(4442,plain,
% 28.28/28.41 (P11(f3(a1))+P13(a1)),
% 28.28/28.41 inference(scs_inference,[],[4426,25])).
% 28.28/28.41 cnf(4461,plain,
% 28.28/28.41 (~P17(f12(a1))+~P20(f12(a1))),
% 28.28/28.41 inference(scs_inference,[],[1872,39])).
% 28.28/28.41 cnf(27354,plain,
% 28.28/28.41 (P20(f12(a1))+P17(f12(a1))),
% 28.28/28.41 inference(scs_inference,[],[1872,35])).
% 28.28/28.41 cnf(27382,plain,
% 28.28/28.41 (~P13(a1)+P20(f12(a1))),
% 28.28/28.41 inference(scs_inference,[],[3,1872,3962,1823,27354,80])).
% 28.28/28.41 cnf(27428,plain,
% 28.28/28.41 (~P17(f12(a1))+~P13(a1)),
% 28.28/28.41 inference(scs_inference,[],[27382,4461])).
% 28.28/28.41 cnf(27474,plain,
% 28.28/28.41 (~P17(f12(a1))+~P11(f3(a1))),
% 28.28/28.41 inference(scs_inference,[],[27428,4347])).
% 28.28/28.41 cnf(27658,plain,
% 28.28/28.41 (~P11(f3(a1))+P20(f12(a1))),
% 28.28/28.41 inference(scs_inference,[],[27474,27354])).
% 28.28/28.41 cnf(27704,plain,
% 28.28/28.41 (P20(f12(a1))+P5(a1,f3(a1))),
% 28.28/28.41 inference(scs_inference,[],[27658,25])).
% 28.28/28.41 cnf(27750,plain,
% 28.28/28.41 (P13(a1)+P20(f12(a1))),
% 28.28/28.41 inference(scs_inference,[],[3943,4152,27704,86])).
% 28.28/28.41 cnf(27796,plain,
% 28.28/28.41 (~P17(f12(a1))+P13(a1)),
% 28.28/28.41 inference(scs_inference,[],[27750,4461])).
% 28.28/28.41 cnf(33454,plain,
% 28.28/28.41 ($false),
% 28.28/28.41 inference(scs_inference,[],[3,1823,4152,3944,3962,80,27750,27796,4379,4442,4347]),
% 28.28/28.41 ['proof']).
% 28.28/28.42 % SZS output end Proof
% 28.28/28.42 % Total time :27.790000s
%------------------------------------------------------------------------------