%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT085+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n029.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:04:24 AM UTC 2026
% Result : Theorem 2.04s 2.24s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT085+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 0.00/0.02 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.07/0.33 % Computer : n029.cluster.edu
% 0.07/0.33 % Model : x86_64 x86_64
% 0.07/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.33 % Memory : 8046.5625MB
% 0.07/0.33 % OS : Linux 6.8.0-71-generic
% 0.07/0.33 % CPULimit : 300
% 0.07/0.33 % WCLimit : 300
% 0.07/0.33 % DateTime : Mon Sep 7 14:21:11 UTC 2026
% 0.07/0.33 % CPUTime :
% 0.25/0.49 start to proof:theBenchmark
% 2.04/2.23 %-------------------------------------------
% 2.04/2.23 % File :CSE---1.7
% 2.04/2.23 % Problem :theBenchmark
% 2.04/2.23 % Transform :cnf
% 2.04/2.23 % Format :tptp:raw
% 2.04/2.23 % Command :java -jar mcs_scs.jar %d %s
% 2.04/2.23
% 2.04/2.23 % Result :Theorem 1.745840s
% 2.04/2.23 % Output :CNFRefutation 1.745840s
% 2.04/2.23 %-------------------------------------------
% 2.04/2.23 %--------------------------------------------------------------------------
% 2.04/2.23 % File : MGT085+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 2.04/2.23 % Domain : Management
% 2.04/2.23 % Problem : 3-branch or: all branch pairs conflict => Conflict
% 2.04/2.23 % Version : Especial.
% 2.04/2.23 % English : PolicyA: width lteq 200 OR height lteq 100 OR depth lteq 50
% 2.04/2.23 % PolicyB: width gteq 400 AND height gteq 200 AND depth gteq 100
% 2.04/2.23 % All 3 branch pairs Conflict => verdictOr=Conflict
% 2.04/2.23
% 2.04/2.23 % Refs : [MC+26] Mustafa et al. (2026), Axis Decomposition for ODRL
% 2.04/2.23 % Source : [MC+26]
% 2.04/2.23 % Names : ODRL445-1.p [MC+26]
% 2.04/2.23
% 2.04/2.23 % Status : Theorem
% 2.04/2.23 % Rating : ? v9.3.1
% 2.04/2.23 % Syntax : Number of formulae : 44 ( 22 unt; 0 def)
% 2.04/2.23 % Number of atoms : 108 ( 33 equ)
% 2.04/2.23 % Maximal formula atoms : 10 ( 2 avg)
% 2.04/2.23 % Number of connectives : 82 ( 18 ~; 11 |; 33 &)
% 2.04/2.23 % ( 8 <=>; 12 =>; 0 <=; 0 <~>)
% 2.04/2.23 % Maximal formula depth : 11 ( 4 avg)
% 2.04/2.23 % Maximal term depth : 2 ( 1 avg)
% 2.04/2.23 % Number of predicates : 12 ( 11 usr; 0 prp; 1-4 aty)
% 2.04/2.23 % Number of functors : 9 ( 9 usr; 8 con; 0-2 aty)
% 2.04/2.23 % Number of variables : 60 ( 55 !; 5 ?)
% 2.04/2.23 % SPC : FOF_THM_RFO_SEQ
% 2.04/2.23
% 2.04/2.23 % Comments : Requires MGT002+0.ax + MGT002+2.ax.
% 2.04/2.23 % Bugfixes : v9.3.1 - $distinct expanded to inequalities.
% 2.04/2.23 %--------------------------------------------------------------------------
% 2.04/2.23 include('Axioms/MGT002+0.ax').
% 2.04/2.23 include('Axioms/MGT002+2.ax').
% 2.04/2.23 %--------------------------------------------------------------------------
% 2.04/2.23 %----Named constants and ordering
% 2.04/2.23 fof(val_v0,axiom,
% 2.04/2.23 val(v0) ).
% 2.04/2.23
% 2.04/2.23 fof(val_v50,axiom,
% 2.04/2.23 val(v50) ).
% 2.04/2.23
% 2.04/2.23 fof(val_v100,axiom,
% 2.04/2.23 val(v100) ).
% 2.04/2.23
% 2.04/2.23 fof(val_v200,axiom,
% 2.04/2.23 val(v200) ).
% 2.04/2.23
% 2.04/2.23 fof(val_v400,axiom,
% 2.04/2.23 val(v400) ).
% 2.04/2.23
% 2.04/2.23 fof(ord_v0_v50,axiom,
% 2.04/2.23 less(v0,v50) ).
% 2.04/2.23
% 2.04/2.23 fof(ord_v0_v100,axiom,
% 2.04/2.23 less(v0,v100) ).
% 2.04/2.23
% 2.04/2.23 fof(ord_v0_v200,axiom,
% 2.04/2.23 less(v0,v200) ).
% 2.04/2.23
% 2.04/2.23 fof(ord_v0_v400,axiom,
% 2.04/2.23 less(v0,v400) ).
% 2.04/2.23
% 2.04/2.23 fof(ord_v50_v100,axiom,
% 2.04/2.23 less(v50,v100) ).
% 2.04/2.23
% 2.04/2.23 fof(ord_v50_v200,axiom,
% 2.04/2.23 less(v50,v200) ).
% 2.04/2.23
% 2.04/2.23 fof(ord_v50_v400,axiom,
% 2.04/2.23 less(v50,v400) ).
% 2.04/2.23
% 2.04/2.23 fof(ord_v100_v200,axiom,
% 2.04/2.23 less(v100,v200) ).
% 2.04/2.23
% 2.04/2.23 fof(ord_v100_v400,axiom,
% 2.04/2.23 less(v100,v400) ).
% 2.04/2.23
% 2.04/2.23 fof(ord_v200_v400,axiom,
% 2.04/2.23 less(v200,v400) ).
% 2.04/2.23
% 2.04/2.23 fof(distinct,axiom,
% 2.04/2.23 ( v0 != v50
% 2.04/2.23 & v0 != v100
% 2.04/2.23 & v0 != v200
% 2.04/2.23 & v0 != v400
% 2.04/2.23 & v50 != v100
% 2.04/2.23 & v50 != v200
% 2.04/2.23 & v50 != v400
% 2.04/2.23 & v100 != v200
% 2.04/2.23 & v100 != v400
% 2.04/2.23 & v200 != v400 ) ).
% 2.04/2.23
% 2.04/2.23 fof(odrl445,conjecture,
% 2.04/2.23 ~ ? [X,Y,Z] :
% 2.04/2.23 ( ( in_lopen(X,v0,v200)
% 2.04/2.23 | in_lopen(Y,v0,v100)
% 2.04/2.24 | in_lopen(Z,v0,v50) )
% 2.04/2.24 & leq(v400,X)
% 2.04/2.24 & leq(v200,Y)
% 2.04/2.24 & leq(v100,Z) ) ).
% 2.04/2.24
% 2.04/2.24 %--------------------------------------------------------------------------
% 2.04/2.24 %-------------------------------------------
% 2.04/2.24 % Proof found
% 2.04/2.24 % SZS status Theorem for theBenchmark
% 2.04/2.24 % SZS output start Proof
% 2.04/2.24 %ClaNum:121(EqnAxiom:47)
% 2.04/2.24 %VarNum:252(SingletonVarNum:111)
% 2.04/2.24 %MaxLitNum:6
% 2.04/2.24 %MaxfuncDepth:1
% 2.04/2.24 %SharedTerms:48
% 2.04/2.24 %goalClause: 66 67 68 112
% 2.04/2.24 %singleGoalClaCount:3
% 2.04/2.24 [48]P1(a1)
% 2.04/2.24 [49]P1(a2)
% 2.04/2.24 [50]P1(a4)
% 2.04/2.24 [51]P9(a11)
% 2.04/2.24 [52]P9(a12)
% 2.04/2.24 [53]P9(a13)
% 2.04/2.24 [54]P9(a14)
% 2.04/2.24 [55]P9(a15)
% 2.04/2.24 [56]P10(a11,a12)
% 2.04/2.24 [57]P10(a11,a13)
% 2.04/2.24 [58]P10(a11,a14)
% 2.04/2.24 [59]P10(a11,a15)
% 2.04/2.24 [60]P10(a12,a13)
% 2.04/2.24 [61]P10(a12,a14)
% 2.04/2.24 [62]P10(a12,a15)
% 2.04/2.24 [63]P10(a13,a14)
% 2.04/2.24 [64]P10(a13,a15)
% 2.04/2.24 [65]P10(a14,a15)
% 2.04/2.24 [66]P11(a13,a5)
% 2.04/2.24 [67]P11(a14,a6)
% 2.04/2.24 [68]P11(a15,a7)
% 2.04/2.24 [69]~E(a1,a2)
% 2.04/2.24 [70]~E(a1,a4)
% 2.04/2.24 [71]~E(a4,a2)
% 2.04/2.24 [72]~E(a12,a11)
% 2.04/2.24 [73]~E(a13,a11)
% 2.04/2.24 [74]~E(a13,a12)
% 2.04/2.24 [75]~E(a14,a11)
% 2.04/2.24 [76]~E(a14,a12)
% 2.04/2.24 [77]~E(a14,a13)
% 2.04/2.24 [78]~E(a15,a11)
% 2.04/2.24 [79]~E(a15,a12)
% 2.04/2.24 [80]~E(a15,a13)
% 2.04/2.24 [81]~E(a15,a14)
% 2.04/2.24 [82]~P10(x821,x821)
% 2.04/2.24 [84]~E(x841,x842)+P11(x841,x842)
% 2.04/2.24 [92]~P10(x921,x922)+P11(x921,x922)
% 2.04/2.24 [104]P10(x1041,x1042)+~P6(x1042,x1041,x1043)
% 2.04/2.24 [105]P10(x1051,x1052)+~P7(x1051,x1053,x1052)
% 2.04/2.24 [106]P10(x1061,x1062)+~P8(x1062,x1061,x1063)
% 2.04/2.24 [107]P10(x1071,x1072)+~P8(x1071,x1073,x1072)
% 2.04/2.24 [108]P11(x1081,x1082)+~P2(x1082,x1081,x1083)
% 2.04/2.24 [109]P11(x1091,x1092)+~P2(x1091,x1093,x1092)
% 2.04/2.24 [110]P11(x1101,x1102)+~P6(x1101,x1103,x1102)
% 2.04/2.24 [111]P11(x1111,x1112)+~P7(x1112,x1111,x1113)
% 2.04/2.24 [116]P5(x1161,x1162,x1163,x1164)+P2(f8(x1161,x1162,x1163,x1164),x1163,x1164)
% 2.04/2.24 [117]P5(x1171,x1172,x1173,x1174)+P2(f8(x1171,x1172,x1173,x1174),x1171,x1172)
% 2.04/2.24 [118]P4(x1181,x1182,x1183,x1184)+P2(f9(x1181,x1182,x1183,x1184),x1181,x1182)
% 2.04/2.24 [119]~P3(x1191,x1192,x1193,x1194)+P2(f10(x1191,x1192,x1193,x1194),x1193,x1194)
% 2.04/2.24 [120]~P3(x1201,x1202,x1203,x1204)+P2(f10(x1201,x1202,x1203,x1204),x1201,x1202)
% 2.04/2.24 [121]P4(x1211,x1212,x1213,x1214)+~P2(f9(x1211,x1212,x1213,x1214),x1213,x1214)
% 2.04/2.24 [112]P6(a7,a11,a14)+P6(a6,a11,a13)+P6(a5,a11,a12)
% 2.04/2.24 [85]P10(x852,x851)+P10(x851,x852)+E(x851,x852)
% 2.04/2.24 [93]P10(x931,x932)+~P11(x931,x932)+E(x931,x932)
% 2.04/2.24 [94]~P11(x942,x941)+~P11(x941,x942)+E(x941,x942)
% 2.04/2.24 [96]~P10(x961,x963)+P10(x961,x962)+~P10(x963,x962)
% 2.04/2.24 [97]~P11(x971,x973)+P10(x971,x972)+~P10(x973,x972)
% 2.04/2.24 [98]~P11(x983,x982)+P10(x981,x982)+~P10(x981,x983)
% 2.04/2.24 [99]~P11(x991,x993)+P11(x991,x992)+~P11(x993,x992)
% 2.04/2.24 [100]~P11(x1001,x1003)+~P11(x1002,x1001)+P2(x1001,x1002,x1003)
% 2.04/2.24 [101]~P10(x1012,x1011)+~P11(x1011,x1013)+P6(x1011,x1012,x1013)
% 2.04/2.24 [102]~P10(x1021,x1023)+~P11(x1022,x1021)+P7(x1021,x1022,x1023)
% 2.04/2.24 [103]~P10(x1031,x1033)+~P10(x1032,x1031)+P8(x1031,x1032,x1033)
% 2.04/2.24 [113]~P2(x1135,x1131,x1132)+P3(x1131,x1132,x1133,x1134)+~P2(x1135,x1133,x1134)
% 2.04/2.24 [114]~P4(x1144,x1145,x1142,x1143)+P2(x1141,x1142,x1143)+~P2(x1141,x1144,x1145)
% 2.04/2.24 [115]~P5(x1154,x1155,x1152,x1153)+~P2(x1151,x1152,x1153)+~P2(x1151,x1154,x1155)
% 2.04/2.24 [83]~P1(x831)+E(x831,a2)+E(x831,a4)+E(x831,a1)
% 2.04/2.24 [86]~P1(x861)+~P1(x862)+~E(x862,a1)+E(f3(x861,x862),a1)
% 2.04/2.24 [87]~P1(x872)+~P1(x871)+~E(x871,a1)+E(f3(x871,x872),a1)
% 2.04/2.24 [88]~P1(x882)+~P1(x881)+~E(x882,a2)+~E(x881,a2)+E(f3(x881,x882),a2)
% 2.04/2.24 [95]~P1(x952)+~P1(x951)+E(f3(x951,x952),a1)+E(f3(x951,x952),a2)+E(f3(x951,x952),a4)
% 2.04/2.24 [89]~P1(x891)+~P1(x892)+~E(x892,a4)+E(x891,a1)+E(x892,a1)+E(f3(x891,x892),a4)
% 2.04/2.24 [90]~P1(x901)+~P1(x902)+~E(x902,a4)+E(x901,a1)+E(x902,a1)+E(f3(x902,x901),a4)
% 2.04/2.24 %EqnAxiom
% 2.04/2.24 [1]E(x11,x11)
% 2.04/2.24 [2]E(x22,x21)+~E(x21,x22)
% 2.04/2.24 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 2.04/2.24 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 2.04/2.24 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 2.04/2.24 [6]~E(x61,x62)+E(f9(x61,x63,x64,x65),f9(x62,x63,x64,x65))
% 2.04/2.24 [7]~E(x71,x72)+E(f9(x73,x71,x74,x75),f9(x73,x72,x74,x75))
% 2.04/2.24 [8]~E(x81,x82)+E(f9(x83,x84,x81,x85),f9(x83,x84,x82,x85))
% 2.04/2.24 [9]~E(x91,x92)+E(f9(x93,x94,x95,x91),f9(x93,x94,x95,x92))
% 2.04/2.24 [10]~E(x101,x102)+E(f10(x101,x103,x104,x105),f10(x102,x103,x104,x105))
% 2.04/2.24 [11]~E(x111,x112)+E(f10(x113,x111,x114,x115),f10(x113,x112,x114,x115))
% 2.04/2.24 [12]~E(x121,x122)+E(f10(x123,x124,x121,x125),f10(x123,x124,x122,x125))
% 2.04/2.24 [13]~E(x131,x132)+E(f10(x133,x134,x135,x131),f10(x133,x134,x135,x132))
% 2.04/2.24 [14]~E(x141,x142)+E(f8(x141,x143,x144,x145),f8(x142,x143,x144,x145))
% 2.04/2.24 [15]~E(x151,x152)+E(f8(x153,x151,x154,x155),f8(x153,x152,x154,x155))
% 2.04/2.24 [16]~E(x161,x162)+E(f8(x163,x164,x161,x165),f8(x163,x164,x162,x165))
% 2.04/2.24 [17]~E(x171,x172)+E(f8(x173,x174,x175,x171),f8(x173,x174,x175,x172))
% 2.04/2.24 [18]~P1(x181)+P1(x182)+~E(x181,x182)
% 2.04/2.24 [19]P2(x192,x193,x194)+~E(x191,x192)+~P2(x191,x193,x194)
% 2.04/2.24 [20]P2(x203,x202,x204)+~E(x201,x202)+~P2(x203,x201,x204)
% 2.04/2.24 [21]P2(x213,x214,x212)+~E(x211,x212)+~P2(x213,x214,x211)
% 2.04/2.24 [22]P4(x222,x223,x224,x225)+~E(x221,x222)+~P4(x221,x223,x224,x225)
% 2.04/2.24 [23]P4(x233,x232,x234,x235)+~E(x231,x232)+~P4(x233,x231,x234,x235)
% 2.04/2.24 [24]P4(x243,x244,x242,x245)+~E(x241,x242)+~P4(x243,x244,x241,x245)
% 2.04/2.24 [25]P4(x253,x254,x255,x252)+~E(x251,x252)+~P4(x253,x254,x255,x251)
% 2.04/2.24 [26]~P9(x261)+P9(x262)+~E(x261,x262)
% 2.04/2.24 [27]P11(x272,x273)+~E(x271,x272)+~P11(x271,x273)
% 2.04/2.24 [28]P11(x283,x282)+~E(x281,x282)+~P11(x283,x281)
% 2.04/2.24 [29]P8(x292,x293,x294)+~E(x291,x292)+~P8(x291,x293,x294)
% 2.04/2.24 [30]P8(x303,x302,x304)+~E(x301,x302)+~P8(x303,x301,x304)
% 2.04/2.24 [31]P8(x313,x314,x312)+~E(x311,x312)+~P8(x313,x314,x311)
% 2.04/2.24 [32]P10(x322,x323)+~E(x321,x322)+~P10(x321,x323)
% 2.04/2.24 [33]P10(x333,x332)+~E(x331,x332)+~P10(x333,x331)
% 2.04/2.24 [34]P6(x342,x343,x344)+~E(x341,x342)+~P6(x341,x343,x344)
% 2.04/2.24 [35]P6(x353,x352,x354)+~E(x351,x352)+~P6(x353,x351,x354)
% 2.04/2.24 [36]P6(x363,x364,x362)+~E(x361,x362)+~P6(x363,x364,x361)
% 2.04/2.24 [37]P3(x372,x373,x374,x375)+~E(x371,x372)+~P3(x371,x373,x374,x375)
% 2.04/2.24 [38]P3(x383,x382,x384,x385)+~E(x381,x382)+~P3(x383,x381,x384,x385)
% 2.04/2.24 [39]P3(x393,x394,x392,x395)+~E(x391,x392)+~P3(x393,x394,x391,x395)
% 2.04/2.24 [40]P3(x403,x404,x405,x402)+~E(x401,x402)+~P3(x403,x404,x405,x401)
% 2.04/2.24 [41]P7(x412,x413,x414)+~E(x411,x412)+~P7(x411,x413,x414)
% 2.04/2.24 [42]P7(x423,x422,x424)+~E(x421,x422)+~P7(x423,x421,x424)
% 2.04/2.24 [43]P7(x433,x434,x432)+~E(x431,x432)+~P7(x433,x434,x431)
% 2.04/2.24 [44]P5(x442,x443,x444,x445)+~E(x441,x442)+~P5(x441,x443,x444,x445)
% 2.04/2.24 [45]P5(x453,x452,x454,x455)+~E(x451,x452)+~P5(x453,x451,x454,x455)
% 2.04/2.24 [46]P5(x463,x464,x462,x465)+~E(x461,x462)+~P5(x463,x464,x461,x465)
% 2.04/2.24 [47]P5(x473,x474,x475,x472)+~E(x471,x472)+~P5(x473,x474,x475,x471)
% 2.04/2.24
% 2.04/2.24 %-------------------------------------------
% 2.04/2.24 cnf(139,plain,
% 2.04/2.24 (P10(a11,a5)),
% 2.04/2.24 inference(scs_inference,[],[66,82,57,104,105,106,107,98])).
% 2.04/2.24 cnf(141,plain,
% 2.04/2.24 (~P10(a12,a11)),
% 2.04/2.24 inference(scs_inference,[],[66,82,56,57,104,105,106,107,98,96])).
% 2.04/2.24 cnf(165,plain,
% 2.04/2.24 (P10(a11,a6)),
% 2.04/2.24 inference(scs_inference,[],[67,141,58,104,106,107,105,98])).
% 2.04/2.24 cnf(168,plain,
% 2.04/2.24 (~P10(x1681,x1681)),
% 2.04/2.24 inference(rename_variables,[],[82])).
% 2.04/2.24 cnf(169,plain,
% 2.04/2.24 (~P10(a5,a11)),
% 2.04/2.24 inference(scs_inference,[],[67,139,82,168,141,58,104,106,107,105,98,32,96])).
% 2.04/2.24 cnf(190,plain,
% 2.04/2.24 (~P10(a6,a11)),
% 2.04/2.24 inference(scs_inference,[],[165,82,169,104,107,106,105,96])).
% 2.04/2.24 cnf(193,plain,
% 2.04/2.24 (P10(a11,a7)),
% 2.04/2.24 inference(scs_inference,[],[68,165,82,169,59,104,107,106,105,96,98])).
% 2.04/2.24 cnf(216,plain,
% 2.04/2.24 (~P10(a7,a11)),
% 2.04/2.24 inference(scs_inference,[],[193,82,190,104,106,107,105,96])).
% 2.04/2.24 cnf(219,plain,
% 2.04/2.24 (P10(a12,a5)),
% 2.04/2.24 inference(scs_inference,[],[66,193,82,190,60,104,106,107,105,96,98])).
% 2.04/2.24 cnf(242,plain,
% 2.04/2.24 (~P10(a13,a11)),
% 2.04/2.24 inference(scs_inference,[],[82,216,57,104,107,106,105,96])).
% 2.04/2.24 cnf(268,plain,
% 2.04/2.24 (~P10(a14,a11)),
% 2.04/2.24 inference(scs_inference,[],[82,242,58,104,106,107,105,96])).
% 2.04/2.24 cnf(295,plain,
% 2.04/2.24 (~P10(a15,a11)),
% 2.04/2.24 inference(scs_inference,[],[82,268,59,104,107,106,105,96])).
% 2.04/2.24 cnf(316,plain,
% 2.04/2.24 (P10(a13,a6)),
% 2.04/2.24 inference(scs_inference,[],[67,295,63,104,106,107,105,98])).
% 2.04/2.24 cnf(327,plain,
% 2.04/2.24 (P10(a14,a7)),
% 2.04/2.24 inference(scs_inference,[],[68,65,98])).
% 2.04/2.24 cnf(330,plain,
% 2.04/2.24 (~P10(x3301,x3301)),
% 2.04/2.24 inference(rename_variables,[],[82])).
% 2.04/2.24 cnf(331,plain,
% 2.04/2.24 (~E(a7,a14)),
% 2.04/2.24 inference(scs_inference,[],[68,316,82,330,65,98,32,33])).
% 2.04/2.24 cnf(672,plain,
% 2.04/2.24 (~P10(a7,a14)),
% 2.04/2.24 inference(scs_inference,[],[327,82,96])).
% 2.04/2.24 cnf(801,plain,
% 2.04/2.24 (~P6(a5,x8011,a12)),
% 2.04/2.24 inference(scs_inference,[],[219,82,97,108,109,111,110])).
% 2.04/2.24 cnf(803,plain,
% 2.04/2.24 (P6(a7,a11,a14)+P6(a6,a11,a13)),
% 2.04/2.24 inference(scs_inference,[],[801,112])).
% 2.04/2.24 cnf(804,plain,
% 2.04/2.24 (P11(a7,a14)+P6(a6,a11,a13)),
% 2.04/2.24 inference(scs_inference,[],[803,110])).
% 2.04/2.24 cnf(816,plain,
% 2.04/2.24 (P6(a6,a11,a13)),
% 2.04/2.24 inference(scs_inference,[],[331,672,804,93])).
% 2.04/2.24 cnf(838,plain,
% 2.04/2.24 ($false),
% 2.04/2.24 inference(scs_inference,[],[816,316,82,97,108,109,111,110]),
% 2.04/2.24 ['proof']).
% 2.04/2.24 % SZS output end Proof
% 2.04/2.24 % Total time :1.745840s
%------------------------------------------------------------------------------