%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT071+1 : TPTP v9.3.0. Released v9.3.0.
% 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:23 AM UTC 2026
% Result : Theorem 0.26s 0.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT071+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.09/0.35 % Computer : n029.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 7 13:56:41 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.26/0.52 start to proof:theBenchmark
% 0.26/0.52 %-------------------------------------------
% 0.26/0.52 % File :CSE---1.7
% 0.26/0.52 % Problem :theBenchmark
% 0.26/0.52 % Transform :cnf
% 0.26/0.52 % Format :tptp:raw
% 0.26/0.52 % Command :java -jar mcs_scs.jar %d %s
% 0.26/0.52
% 0.26/0.52 % Result :Theorem 0.005273s
% 0.26/0.52 % Output :CNFRefutation 0.005273s
% 0.26/0.52 %-------------------------------------------
% 0.26/0.52 %--------------------------------------------------------------------------
% 0.26/0.52 % File : MGT071+1 : TPTP v9.3.0. Released v9.3.0.
% 0.26/0.52 % Domain : Management
% 0.26/0.52 % Problem : Conflict verdict implies no joint witness
% 0.26/0.52 % Version : Especial.
% 0.26/0.52 % English : If axis_conflict holds for two closed intervals then no
% 0.26/0.52 % value belongs to both. Establishes Conflict is never a false
% 0.26/0.52 % positive (prop:no-false-verdict, Conflict direction).
% 0.26/0.52
% 0.26/0.52 % Refs : [MC+26] Mustafa et al. (2026), Axis Decomposition for ODRL
% 0.26/0.52 % Source : [MC+26]
% 0.26/0.52 % Names : NFV001+1.p [MC+26]
% 0.26/0.52
% 0.26/0.52 % Status : Theorem
% 0.26/0.52 % Rating : 0.04 v9.3.0
% 0.26/0.52 % Syntax : Number of formulae : 41 ( 11 unt; 0 def)
% 0.26/0.52 % Number of atoms : 110 ( 24 equ)
% 0.26/0.52 % Maximal formula atoms : 7 ( 2 avg)
% 0.26/0.52 % Number of connectives : 77 ( 8 ~; 10 |; 30 &)
% 0.26/0.52 % ( 17 <=>; 12 =>; 0 <=; 0 <~>)
% 0.26/0.52 % Maximal formula depth : 13 ( 5 avg)
% 0.26/0.52 % Maximal term depth : 2 ( 1 avg)
% 0.26/0.52 % Number of predicates : 15 ( 14 usr; 0 prp; 1-9 aty)
% 0.26/0.52 % Number of functors : 8 ( 8 usr; 7 con; 0-2 aty)
% 0.26/0.52 % Number of variables : 103 ( 100 !; 3 ?)
% 0.26/0.52 % SPC : FOF_THM_RFO_SEQ
% 0.26/0.52
% 0.26/0.52 % Comments : Hard tier - prop:no-false-verdict Conflict direction.
% 0.26/0.52 % : axis_conflict given as hypothesis; prover derives emptiness.
% 0.26/0.52 %--------------------------------------------------------------------------
% 0.26/0.52 include('Axioms/MGT002+0.ax').
% 0.26/0.52 include('Axioms/MGT002+2.ax').
% 0.26/0.52 include('Axioms/MGT002+6.ax').
% 0.26/0.52 %--------------------------------------------------------------------------
% 0.26/0.52 %----Domain constants: n0 < n5 < n10 < n15
% 0.26/0.53 fof(order_0_5,hypothesis,
% 0.26/0.53 less(n0,n5) ).
% 0.26/0.53
% 0.26/0.53 fof(order_5_10,hypothesis,
% 0.26/0.53 less(n5,n10) ).
% 0.26/0.53
% 0.26/0.53 fof(order_10_15,hypothesis,
% 0.26/0.53 less(n10,n15) ).
% 0.26/0.53
% 0.26/0.53 %----The two intervals [n0,n5] and [n10,n15] are disjoint on this axis.
% 0.26/0.53 %----axis_conflict is defined in AXIS000 Section B as the absence of a
% 0.26/0.53 %----shared witness; we assert it here directly as a ground hypothesis to
% 0.26/0.53 %----exercise the no-false-verdict claim independently of the criterion
% 0.26/0.53 %---- proof.
% 0.26/0.53 fof(conflict_hyp,hypothesis,
% 0.26/0.53 axis_conflict(n0,n5,n10,n15) ).
% 0.26/0.53
% 0.26/0.53 %----Conjecture: no value lies in both intervals.
% 0.26/0.53 %----Conflict => no request simultaneously satisfies both constraint sets.
% 0.26/0.53 fof(no_false_conflict,conjecture,
% 0.26/0.53 ~ ? [X] :
% 0.26/0.53 ( in_closed(X,n0,n5)
% 0.26/0.53 & in_closed(X,n10,n15) ) ).
% 0.26/0.53
% 0.26/0.53 %--------------------------------------------------------------------------
% 0.26/0.53 %-------------------------------------------
% 0.26/0.53 % Proof found
% 0.26/0.53 % SZS status Theorem for theBenchmark
% 0.26/0.53 % SZS output start Proof
% 0.26/0.53 %ClaNum:155(EqnAxiom:77)
% 0.26/0.53 %VarNum:426(SingletonVarNum:217)
% 0.26/0.53 %MaxLitNum:6
% 0.26/0.53 %MaxfuncDepth:1
% 0.26/0.53 %SharedTerms:20
% 0.26/0.53 %goalClause: 84 85
% 0.26/0.53 %singleGoalClaCount:2
% 0.26/0.53 [78]P1(a1)
% 0.26/0.53 [79]P1(a2)
% 0.26/0.53 [80]P1(a4)
% 0.26/0.53 [81]P13(a5,a10)
% 0.26/0.53 [82]P13(a10,a11)
% 0.26/0.53 [83]P13(a11,a12)
% 0.26/0.53 [84]P2(a6,a5,a10)
% 0.26/0.53 [85]P2(a6,a11,a12)
% 0.26/0.53 [86]P3(a5,a10,a11,a12)
% 0.26/0.53 [87]~E(a1,a2)
% 0.26/0.53 [88]~E(a1,a4)
% 0.26/0.53 [89]~E(a4,a2)
% 0.26/0.53 [90]~P13(x901,x901)
% 0.26/0.53 [92]~E(x921,x922)+P14(x921,x922)
% 0.26/0.53 [100]~P13(x1001,x1002)+P14(x1001,x1002)
% 0.26/0.53 [104]~E(x1041,x1042)+P2(x1041,x1042,x1042)
% 0.26/0.53 [109]~P2(x1091,x1092,x1092)+E(x1091,x1092)
% 0.26/0.53 [119]P13(x1191,x1192)+~P10(x1192,x1191,x1193)
% 0.26/0.53 [121]P13(x1211,x1212)+~P11(x1211,x1213,x1212)
% 0.26/0.53 [123]P13(x1231,x1232)+~P12(x1232,x1231,x1233)
% 0.26/0.53 [125]P13(x1251,x1252)+~P12(x1251,x1253,x1252)
% 0.26/0.53 [127]P14(x1271,x1272)+~P2(x1272,x1271,x1273)
% 0.26/0.53 [129]P14(x1291,x1292)+~P2(x1291,x1293,x1292)
% 0.26/0.53 [131]P14(x1311,x1312)+~P10(x1311,x1313,x1312)
% 0.26/0.53 [133]P14(x1331,x1332)+~P11(x1332,x1331,x1333)
% 0.26/0.53 [137]P3(x1371,x1372,x1373,x1374)+P2(f7(x1371,x1372,x1373,x1374),x1373,x1374)
% 0.26/0.53 [138]P3(x1381,x1382,x1383,x1384)+P2(f7(x1381,x1382,x1383,x1384),x1381,x1382)
% 0.26/0.53 [139]P5(x1391,x1392,x1393,x1394)+P2(f8(x1391,x1392,x1393,x1394),x1391,x1392)
% 0.26/0.53 [140]~P4(x1401,x1402,x1403,x1404)+P2(f9(x1401,x1402,x1403,x1404),x1403,x1404)
% 0.26/0.53 [141]~P4(x1411,x1412,x1413,x1414)+P2(f9(x1411,x1412,x1413,x1414),x1411,x1412)
% 0.26/0.53 [142]P5(x1421,x1422,x1423,x1424)+~P2(f8(x1421,x1422,x1423,x1424),x1423,x1424)
% 0.26/0.53 [144]P2(x1441,x1442,x1443)+~P6(x1444,x1441,x1445,x1446,x1442,x1443)
% 0.26/0.53 [145]P2(x1451,x1452,x1453)+~P6(x1451,x1454,x1452,x1453,x1455,x1456)
% 0.26/0.53 [146]~P3(x1463,x1464,x1467,x1468)+P7(x1461,x1462,x1463,x1464,x1465,x1466,x1467,x1468)
% 0.26/0.53 [147]~P3(x1471,x1472,x1475,x1476)+P7(x1471,x1472,x1473,x1474,x1475,x1476,x1477,x1478)
% 0.26/0.53 [149]P4(x1491,x1492,x1493,x1494)+~P8(x1495,x1496,x1491,x1492,x1497,x1498,x1493,x1494)
% 0.26/0.53 [150]P4(x1501,x1502,x1503,x1504)+~P8(x1501,x1502,x1505,x1506,x1503,x1504,x1507,x1508)
% 0.26/0.53 [153]P2(x1531,x1532,x1533)+~P9(x1534,x1535,x1531,x1536,x1537,x1538,x1539,x1532,x1533)
% 0.26/0.53 [154]P2(x1541,x1542,x1543)+~P9(x1544,x1541,x1545,x1546,x1547,x1542,x1543,x1548,x1549)
% 0.26/0.53 [155]P2(x1551,x1552,x1553)+~P9(x1551,x1554,x1555,x1552,x1553,x1556,x1557,x1558,x1559)
% 0.26/0.53 [93]P13(x932,x931)+P13(x931,x932)+E(x931,x932)
% 0.26/0.53 [101]P13(x1011,x1012)+~P14(x1011,x1012)+E(x1011,x1012)
% 0.26/0.53 [102]~P14(x1022,x1021)+~P14(x1021,x1022)+E(x1021,x1022)
% 0.26/0.53 [105]~P13(x1051,x1053)+P13(x1051,x1052)+~P13(x1053,x1052)
% 0.26/0.53 [106]~P14(x1061,x1063)+P13(x1061,x1062)+~P13(x1063,x1062)
% 0.26/0.53 [107]~P14(x1073,x1072)+P13(x1071,x1072)+~P13(x1071,x1073)
% 0.26/0.53 [108]~P14(x1081,x1083)+P14(x1081,x1082)+~P14(x1083,x1082)
% 0.26/0.53 [111]~P14(x1111,x1113)+~P14(x1112,x1111)+P2(x1111,x1112,x1113)
% 0.26/0.53 [113]~P13(x1132,x1131)+~P14(x1131,x1133)+P10(x1131,x1132,x1133)
% 0.26/0.53 [115]~P13(x1151,x1153)+~P14(x1152,x1151)+P11(x1151,x1152,x1153)
% 0.26/0.53 [117]~P13(x1171,x1173)+~P13(x1172,x1171)+P12(x1171,x1172,x1173)
% 0.26/0.53 [134]~P2(x1345,x1341,x1342)+P4(x1341,x1342,x1343,x1344)+~P2(x1345,x1343,x1344)
% 0.26/0.53 [135]~P5(x1354,x1355,x1352,x1353)+P2(x1351,x1352,x1353)+~P2(x1351,x1354,x1355)
% 0.26/0.53 [136]~P3(x1364,x1365,x1362,x1363)+~P2(x1361,x1362,x1363)+~P2(x1361,x1364,x1365)
% 0.26/0.53 [143]~P2(x1432,x1435,x1436)+~P2(x1431,x1433,x1434)+P6(x1431,x1432,x1433,x1434,x1435,x1436)
% 0.26/0.53 [148]~P4(x1483,x1484,x1487,x1488)+~P4(x1481,x1482,x1485,x1486)+P8(x1481,x1482,x1483,x1484,x1485,x1486,x1487,x1488)
% 0.26/0.53 [151]~P7(x1515,x1516,x1511,x1512,x1517,x1518,x1513,x1514)+P3(x1511,x1512,x1513,x1514)+P3(x1515,x1516,x1517,x1518)
% 0.26/0.53 [91]~P1(x911)+E(x911,a2)+E(x911,a4)+E(x911,a1)
% 0.26/0.53 [94]~P1(x941)+~P1(x942)+~E(x942,a1)+E(f3(x941,x942),a1)
% 0.26/0.53 [95]~P1(x952)+~P1(x951)+~E(x951,a1)+E(f3(x951,x952),a1)
% 0.26/0.53 [152]~P2(x1523,x1528,x1529)+~P2(x1522,x1526,x1527)+~P2(x1521,x1524,x1525)+P9(x1521,x1522,x1523,x1524,x1525,x1526,x1527,x1528,x1529)
% 0.26/0.53 [96]~P1(x962)+~P1(x961)+~E(x962,a2)+~E(x961,a2)+E(f3(x961,x962),a2)
% 0.26/0.53 [103]~P1(x1032)+~P1(x1031)+E(f3(x1031,x1032),a1)+E(f3(x1031,x1032),a2)+E(f3(x1031,x1032),a4)
% 0.26/0.53 [97]~P1(x971)+~P1(x972)+~E(x972,a4)+E(x971,a1)+E(x972,a1)+E(f3(x971,x972),a4)
% 0.26/0.53 [98]~P1(x981)+~P1(x982)+~E(x982,a4)+E(x981,a1)+E(x982,a1)+E(f3(x982,x981),a4)
% 0.26/0.53 %EqnAxiom
% 0.26/0.53 [1]E(x11,x11)
% 0.26/0.53 [2]E(x22,x21)+~E(x21,x22)
% 0.26/0.53 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.26/0.53 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 0.26/0.53 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 0.26/0.53 [6]~E(x61,x62)+E(f8(x61,x63,x64,x65),f8(x62,x63,x64,x65))
% 0.26/0.53 [7]~E(x71,x72)+E(f8(x73,x71,x74,x75),f8(x73,x72,x74,x75))
% 0.26/0.53 [8]~E(x81,x82)+E(f8(x83,x84,x81,x85),f8(x83,x84,x82,x85))
% 0.26/0.53 [9]~E(x91,x92)+E(f8(x93,x94,x95,x91),f8(x93,x94,x95,x92))
% 0.26/0.53 [10]~E(x101,x102)+E(f9(x101,x103,x104,x105),f9(x102,x103,x104,x105))
% 0.26/0.53 [11]~E(x111,x112)+E(f9(x113,x111,x114,x115),f9(x113,x112,x114,x115))
% 0.26/0.53 [12]~E(x121,x122)+E(f9(x123,x124,x121,x125),f9(x123,x124,x122,x125))
% 0.26/0.53 [13]~E(x131,x132)+E(f9(x133,x134,x135,x131),f9(x133,x134,x135,x132))
% 0.26/0.53 [14]~E(x141,x142)+E(f7(x141,x143,x144,x145),f7(x142,x143,x144,x145))
% 0.26/0.53 [15]~E(x151,x152)+E(f7(x153,x151,x154,x155),f7(x153,x152,x154,x155))
% 0.26/0.53 [16]~E(x161,x162)+E(f7(x163,x164,x161,x165),f7(x163,x164,x162,x165))
% 0.26/0.53 [17]~E(x171,x172)+E(f7(x173,x174,x175,x171),f7(x173,x174,x175,x172))
% 0.26/0.53 [18]~P1(x181)+P1(x182)+~E(x181,x182)
% 0.26/0.53 [19]P9(x192,x193,x194,x195,x196,x197,x198,x199,x1910)+~E(x191,x192)+~P9(x191,x193,x194,x195,x196,x197,x198,x199,x1910)
% 0.26/0.53 [20]P9(x203,x202,x204,x205,x206,x207,x208,x209,x2010)+~E(x201,x202)+~P9(x203,x201,x204,x205,x206,x207,x208,x209,x2010)
% 0.26/0.53 [21]P9(x213,x214,x212,x215,x216,x217,x218,x219,x2110)+~E(x211,x212)+~P9(x213,x214,x211,x215,x216,x217,x218,x219,x2110)
% 0.26/0.53 [22]P9(x223,x224,x225,x222,x226,x227,x228,x229,x2210)+~E(x221,x222)+~P9(x223,x224,x225,x221,x226,x227,x228,x229,x2210)
% 0.26/0.53 [23]P9(x233,x234,x235,x236,x232,x237,x238,x239,x2310)+~E(x231,x232)+~P9(x233,x234,x235,x236,x231,x237,x238,x239,x2310)
% 0.26/0.53 [24]P9(x243,x244,x245,x246,x247,x242,x248,x249,x2410)+~E(x241,x242)+~P9(x243,x244,x245,x246,x247,x241,x248,x249,x2410)
% 0.26/0.53 [25]P9(x253,x254,x255,x256,x257,x258,x252,x259,x2510)+~E(x251,x252)+~P9(x253,x254,x255,x256,x257,x258,x251,x259,x2510)
% 0.26/0.53 [26]P9(x263,x264,x265,x266,x267,x268,x269,x262,x2610)+~E(x261,x262)+~P9(x263,x264,x265,x266,x267,x268,x269,x261,x2610)
% 0.26/0.53 [27]P9(x273,x274,x275,x276,x277,x278,x279,x2710,x272)+~E(x271,x272)+~P9(x273,x274,x275,x276,x277,x278,x279,x2710,x271)
% 0.26/0.53 [28]P2(x282,x283,x284)+~E(x281,x282)+~P2(x281,x283,x284)
% 0.26/0.53 [29]P2(x293,x292,x294)+~E(x291,x292)+~P2(x293,x291,x294)
% 0.26/0.53 [30]P2(x303,x304,x302)+~E(x301,x302)+~P2(x303,x304,x301)
% 0.26/0.53 [31]P13(x312,x313)+~E(x311,x312)+~P13(x311,x313)
% 0.26/0.53 [32]P13(x323,x322)+~E(x321,x322)+~P13(x323,x321)
% 0.26/0.53 [33]P5(x332,x333,x334,x335)+~E(x331,x332)+~P5(x331,x333,x334,x335)
% 0.26/0.53 [34]P5(x343,x342,x344,x345)+~E(x341,x342)+~P5(x343,x341,x344,x345)
% 0.26/0.53 [35]P5(x353,x354,x352,x355)+~E(x351,x352)+~P5(x353,x354,x351,x355)
% 0.26/0.53 [36]P5(x363,x364,x365,x362)+~E(x361,x362)+~P5(x363,x364,x365,x361)
% 0.26/0.53 [37]P3(x372,x373,x374,x375)+~E(x371,x372)+~P3(x371,x373,x374,x375)
% 0.26/0.53 [38]P3(x383,x382,x384,x385)+~E(x381,x382)+~P3(x383,x381,x384,x385)
% 0.26/0.53 [39]P3(x393,x394,x392,x395)+~E(x391,x392)+~P3(x393,x394,x391,x395)
% 0.26/0.53 [40]P3(x403,x404,x405,x402)+~E(x401,x402)+~P3(x403,x404,x405,x401)
% 0.26/0.53 [41]P4(x412,x413,x414,x415)+~E(x411,x412)+~P4(x411,x413,x414,x415)
% 0.26/0.53 [42]P4(x423,x422,x424,x425)+~E(x421,x422)+~P4(x423,x421,x424,x425)
% 0.26/0.53 [43]P4(x433,x434,x432,x435)+~E(x431,x432)+~P4(x433,x434,x431,x435)
% 0.26/0.53 [44]P4(x443,x444,x445,x442)+~E(x441,x442)+~P4(x443,x444,x445,x441)
% 0.26/0.53 [45]P8(x452,x453,x454,x455,x456,x457,x458,x459)+~E(x451,x452)+~P8(x451,x453,x454,x455,x456,x457,x458,x459)
% 0.26/0.53 [46]P8(x463,x462,x464,x465,x466,x467,x468,x469)+~E(x461,x462)+~P8(x463,x461,x464,x465,x466,x467,x468,x469)
% 0.26/0.53 [47]P8(x473,x474,x472,x475,x476,x477,x478,x479)+~E(x471,x472)+~P8(x473,x474,x471,x475,x476,x477,x478,x479)
% 0.26/0.53 [48]P8(x483,x484,x485,x482,x486,x487,x488,x489)+~E(x481,x482)+~P8(x483,x484,x485,x481,x486,x487,x488,x489)
% 0.26/0.53 [49]P8(x493,x494,x495,x496,x492,x497,x498,x499)+~E(x491,x492)+~P8(x493,x494,x495,x496,x491,x497,x498,x499)
% 0.26/0.53 [50]P8(x503,x504,x505,x506,x507,x502,x508,x509)+~E(x501,x502)+~P8(x503,x504,x505,x506,x507,x501,x508,x509)
% 0.26/0.53 [51]P8(x513,x514,x515,x516,x517,x518,x512,x519)+~E(x511,x512)+~P8(x513,x514,x515,x516,x517,x518,x511,x519)
% 0.26/0.53 [52]P8(x523,x524,x525,x526,x527,x528,x529,x522)+~E(x521,x522)+~P8(x523,x524,x525,x526,x527,x528,x529,x521)
% 0.26/0.53 [53]P10(x532,x533,x534)+~E(x531,x532)+~P10(x531,x533,x534)
% 0.26/0.53 [54]P10(x543,x542,x544)+~E(x541,x542)+~P10(x543,x541,x544)
% 0.26/0.53 [55]P10(x553,x554,x552)+~E(x551,x552)+~P10(x553,x554,x551)
% 0.26/0.53 [56]P12(x562,x563,x564)+~E(x561,x562)+~P12(x561,x563,x564)
% 0.26/0.53 [57]P12(x573,x572,x574)+~E(x571,x572)+~P12(x573,x571,x574)
% 0.26/0.53 [58]P12(x583,x584,x582)+~E(x581,x582)+~P12(x583,x584,x581)
% 0.26/0.53 [59]P11(x592,x593,x594)+~E(x591,x592)+~P11(x591,x593,x594)
% 0.26/0.53 [60]P11(x603,x602,x604)+~E(x601,x602)+~P11(x603,x601,x604)
% 0.26/0.53 [61]P11(x613,x614,x612)+~E(x611,x612)+~P11(x613,x614,x611)
% 0.26/0.53 [62]P14(x622,x623)+~E(x621,x622)+~P14(x621,x623)
% 0.26/0.53 [63]P14(x633,x632)+~E(x631,x632)+~P14(x633,x631)
% 0.26/0.54 [64]P6(x642,x643,x644,x645,x646,x647)+~E(x641,x642)+~P6(x641,x643,x644,x645,x646,x647)
% 0.26/0.54 [65]P6(x653,x652,x654,x655,x656,x657)+~E(x651,x652)+~P6(x653,x651,x654,x655,x656,x657)
% 0.26/0.54 [66]P6(x663,x664,x662,x665,x666,x667)+~E(x661,x662)+~P6(x663,x664,x661,x665,x666,x667)
% 0.26/0.54 [67]P6(x673,x674,x675,x672,x676,x677)+~E(x671,x672)+~P6(x673,x674,x675,x671,x676,x677)
% 0.26/0.54 [68]P6(x683,x684,x685,x686,x682,x687)+~E(x681,x682)+~P6(x683,x684,x685,x686,x681,x687)
% 0.26/0.54 [69]P6(x693,x694,x695,x696,x697,x692)+~E(x691,x692)+~P6(x693,x694,x695,x696,x697,x691)
% 0.26/0.54 [70]P7(x702,x703,x704,x705,x706,x707,x708,x709)+~E(x701,x702)+~P7(x701,x703,x704,x705,x706,x707,x708,x709)
% 0.26/0.54 [71]P7(x713,x712,x714,x715,x716,x717,x718,x719)+~E(x711,x712)+~P7(x713,x711,x714,x715,x716,x717,x718,x719)
% 0.26/0.54 [72]P7(x723,x724,x722,x725,x726,x727,x728,x729)+~E(x721,x722)+~P7(x723,x724,x721,x725,x726,x727,x728,x729)
% 0.26/0.54 [73]P7(x733,x734,x735,x732,x736,x737,x738,x739)+~E(x731,x732)+~P7(x733,x734,x735,x731,x736,x737,x738,x739)
% 0.26/0.54 [74]P7(x743,x744,x745,x746,x742,x747,x748,x749)+~E(x741,x742)+~P7(x743,x744,x745,x746,x741,x747,x748,x749)
% 0.26/0.54 [75]P7(x753,x754,x755,x756,x757,x752,x758,x759)+~E(x751,x752)+~P7(x753,x754,x755,x756,x757,x751,x758,x759)
% 0.26/0.54 [76]P7(x763,x764,x765,x766,x767,x768,x762,x769)+~E(x761,x762)+~P7(x763,x764,x765,x766,x767,x768,x761,x769)
% 0.26/0.54 [77]P7(x773,x774,x775,x776,x777,x778,x779,x772)+~E(x771,x772)+~P7(x773,x774,x775,x776,x777,x778,x779,x771)
% 0.26/0.54
% 0.26/0.54 %-------------------------------------------
% 0.26/0.54 cnf(162,plain,
% 0.26/0.54 ($false),
% 0.26/0.54 inference(scs_inference,[],[86,85,84,136]),
% 0.26/0.54 ['proof']).
% 0.26/0.54 % SZS output end Proof
% 0.26/0.54 % Total time :0.005273s
%------------------------------------------------------------------------------