%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT073+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n016.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 4.23s 4.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT073+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.07/0.34 % Computer : n016.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 7 14:01:47 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.24/0.50 start to proof:theBenchmark
% 4.23/4.49 %-------------------------------------------
% 4.23/4.49 % File :CSE---1.7
% 4.23/4.49 % Problem :theBenchmark
% 4.23/4.49 % Transform :cnf
% 4.23/4.49 % Format :tptp:raw
% 4.23/4.49 % Command :java -jar mcs_scs.jar %d %s
% 4.23/4.49
% 4.23/4.49 % Result :Theorem 3.983981s
% 4.23/4.49 % Output :CNFRefutation 3.983981s
% 4.23/4.49 %-------------------------------------------
% 4.23/4.49 %--------------------------------------------------------------------------
% 4.23/4.49 % File : MGT073+1 : TPTP v9.3.0. Released v9.3.0.
% 4.23/4.49 % Domain : Management
% 4.23/4.49 % Problem : Compatible verdict implies joint witness exists
% 4.23/4.49 % Version : Especial.
% 4.23/4.49 % English : If axis_compatible holds for two closed intervals then some
% 4.23/4.49 % value belongs to both. Establishes Compatible is never a
% 4.23/4.49 % false positive (prop:no-false-verdict, Compatible direction).
% 4.23/4.49
% 4.23/4.49 % Refs : [MC+26] Mustafa et al. (2026), Axis Decomposition for ODRL
% 4.23/4.49 % Source : [MC+26]
% 4.23/4.49 % Names : NFV002+1.p [MC+26]
% 4.23/4.49
% 4.23/4.49 % Status : Theorem
% 4.23/4.49 % Rating : 0.04 v9.3.0
% 4.23/4.49 % Syntax : Number of formulae : 40 ( 10 unt; 0 def)
% 4.23/4.49 % Number of atoms : 109 ( 24 equ)
% 4.23/4.49 % Maximal formula atoms : 7 ( 2 avg)
% 4.23/4.49 % Number of connectives : 76 ( 7 ~; 10 |; 30 &)
% 4.23/4.49 % ( 17 <=>; 12 =>; 0 <=; 0 <~>)
% 4.23/4.49 % Maximal formula depth : 13 ( 5 avg)
% 4.23/4.49 % Maximal term depth : 2 ( 1 avg)
% 4.23/4.49 % Number of predicates : 15 ( 14 usr; 0 prp; 1-9 aty)
% 4.23/4.49 % Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% 4.23/4.49 % Number of variables : 103 ( 100 !; 3 ?)
% 4.23/4.49 % SPC : FOF_THM_RFO_SEQ
% 4.23/4.49
% 4.23/4.49 % Comments : Hard tier - prop:no-false-verdict Compatible direction.
% 4.23/4.49 % : axis_compatible given as hypothesis; prover finds witness.
% 4.23/4.49 %--------------------------------------------------------------------------
% 4.23/4.49 include('Axioms/MGT002+0.ax').
% 4.23/4.49 include('Axioms/MGT002+2.ax').
% 4.23/4.49 include('Axioms/MGT002+6.ax').
% 4.23/4.49 %--------------------------------------------------------------------------
% 4.23/4.49 %----Domain constants: n0 < n5 < n10
% 4.23/4.49 fof(order_0_5,hypothesis,
% 4.23/4.49 less(n0,n5) ).
% 4.23/4.49
% 4.23/4.49 fof(order_5_10,hypothesis,
% 4.23/4.49 less(n5,n10) ).
% 4.23/4.49
% 4.23/4.49 %----The two intervals [n0,n10] and [n5,n10] overlap (n5 is in both).
% 4.23/4.49 %----axis_compatible is defined in AXIS000 Section B as the existence of a
% 4.23/4.49 %----shared witness; we assert it here directly as a ground hypothesis to
% 4.23/4.49 %----exercise the no-false-verdict claim independently of the criterion
% 4.23/4.49 %----proof.
% 4.23/4.49 fof(compatible_hyp,hypothesis,
% 4.23/4.49 axis_compatible(n0,n10,n5,n10) ).
% 4.23/4.49
% 4.23/4.49 %----Conjecture: some value lies in both intervals.
% 4.23/4.49 %----Compatible => every axis was examined and admits overlap.
% 4.23/4.49 fof(no_false_compatible,conjecture,
% 4.23/4.49 ? [X] :
% 4.23/4.49 ( in_closed(X,n0,n10)
% 4.23/4.49 & in_closed(X,n5,n10) ) ).
% 4.23/4.49
% 4.23/4.49 %--------------------------------------------------------------------------
% 4.23/4.49 %-------------------------------------------
% 4.23/4.49 % Proof found
% 4.23/4.49 % SZS status Theorem for theBenchmark
% 4.23/4.49 % SZS output start Proof
% 4.23/4.49 %ClaNum:153(EqnAxiom:77)
% 4.23/4.49 %VarNum:428(SingletonVarNum:218)
% 4.23/4.49 %MaxLitNum:6
% 4.23/4.49 %MaxfuncDepth:1
% 4.23/4.49 %SharedTerms:15
% 4.23/4.49 %goalClause: 131
% 4.23/4.49 [78]P1(a1)
% 4.23/4.49 [79]P1(a2)
% 4.23/4.49 [80]P1(a4)
% 4.23/4.49 [81]P13(a5,a9)
% 4.23/4.49 [82]P13(a9,a10)
% 4.23/4.49 [83]P2(a5,a10,a9,a10)
% 4.23/4.49 [84]~E(a1,a2)
% 4.23/4.49 [85]~E(a1,a4)
% 4.23/4.50 [86]~E(a4,a2)
% 4.23/4.50 [87]~P13(x871,x871)
% 4.23/4.50 [131]~P3(x1311,a9,a10)+~P3(x1311,a5,a10)
% 4.23/4.50 [89]~E(x891,x892)+P14(x891,x892)
% 4.23/4.50 [97]~P13(x971,x972)+P14(x971,x972)
% 4.23/4.50 [101]~E(x1011,x1012)+P3(x1011,x1012,x1012)
% 4.23/4.50 [106]~P3(x1061,x1062,x1062)+E(x1061,x1062)
% 4.23/4.50 [116]P13(x1161,x1162)+~P10(x1162,x1161,x1163)
% 4.23/4.50 [118]P13(x1181,x1182)+~P11(x1181,x1183,x1182)
% 4.23/4.50 [120]P13(x1201,x1202)+~P12(x1202,x1201,x1203)
% 4.23/4.50 [122]P13(x1221,x1222)+~P12(x1221,x1223,x1222)
% 4.23/4.50 [124]P14(x1241,x1242)+~P3(x1242,x1241,x1243)
% 4.23/4.50 [126]P14(x1261,x1262)+~P3(x1261,x1263,x1262)
% 4.23/4.50 [128]P14(x1281,x1282)+~P10(x1281,x1283,x1282)
% 4.23/4.50 [130]P14(x1301,x1302)+~P11(x1302,x1301,x1303)
% 4.23/4.50 [135]P5(x1351,x1352,x1353,x1354)+P3(f6(x1351,x1352,x1353,x1354),x1353,x1354)
% 4.23/4.50 [136]P5(x1361,x1362,x1363,x1364)+P3(f6(x1361,x1362,x1363,x1364),x1361,x1362)
% 4.23/4.50 [137]P4(x1371,x1372,x1373,x1374)+P3(f7(x1371,x1372,x1373,x1374),x1371,x1372)
% 4.23/4.50 [138]~P2(x1381,x1382,x1383,x1384)+P3(f8(x1381,x1382,x1383,x1384),x1383,x1384)
% 4.23/4.50 [139]~P2(x1391,x1392,x1393,x1394)+P3(f8(x1391,x1392,x1393,x1394),x1391,x1392)
% 4.23/4.50 [140]P4(x1401,x1402,x1403,x1404)+~P3(f7(x1401,x1402,x1403,x1404),x1403,x1404)
% 4.23/4.50 [142]P3(x1421,x1422,x1423)+~P6(x1424,x1421,x1425,x1426,x1422,x1423)
% 4.23/4.50 [143]P3(x1431,x1432,x1433)+~P6(x1431,x1434,x1432,x1433,x1435,x1436)
% 4.23/4.50 [144]~P5(x1443,x1444,x1447,x1448)+P7(x1441,x1442,x1443,x1444,x1445,x1446,x1447,x1448)
% 4.23/4.50 [145]~P5(x1451,x1452,x1455,x1456)+P7(x1451,x1452,x1453,x1454,x1455,x1456,x1457,x1458)
% 4.23/4.50 [147]P2(x1471,x1472,x1473,x1474)+~P8(x1475,x1476,x1471,x1472,x1477,x1478,x1473,x1474)
% 4.23/4.50 [148]P2(x1481,x1482,x1483,x1484)+~P8(x1481,x1482,x1485,x1486,x1483,x1484,x1487,x1488)
% 4.23/4.50 [151]P3(x1511,x1512,x1513)+~P9(x1514,x1515,x1511,x1516,x1517,x1518,x1519,x1512,x1513)
% 4.23/4.50 [152]P3(x1521,x1522,x1523)+~P9(x1524,x1521,x1525,x1526,x1527,x1522,x1523,x1528,x1529)
% 4.23/4.50 [153]P3(x1531,x1532,x1533)+~P9(x1531,x1534,x1535,x1532,x1533,x1536,x1537,x1538,x1539)
% 4.23/4.50 [90]P13(x902,x901)+P13(x901,x902)+E(x901,x902)
% 4.23/4.50 [98]P13(x981,x982)+~P14(x981,x982)+E(x981,x982)
% 4.23/4.50 [99]~P14(x992,x991)+~P14(x991,x992)+E(x991,x992)
% 4.34/4.50 [102]~P13(x1021,x1023)+P13(x1021,x1022)+~P13(x1023,x1022)
% 4.34/4.50 [103]~P14(x1031,x1033)+P13(x1031,x1032)+~P13(x1033,x1032)
% 4.34/4.50 [104]~P14(x1043,x1042)+P13(x1041,x1042)+~P13(x1041,x1043)
% 4.34/4.50 [105]~P14(x1051,x1053)+P14(x1051,x1052)+~P14(x1053,x1052)
% 4.34/4.50 [108]~P14(x1081,x1083)+~P14(x1082,x1081)+P3(x1081,x1082,x1083)
% 4.34/4.50 [110]~P13(x1102,x1101)+~P14(x1101,x1103)+P10(x1101,x1102,x1103)
% 4.34/4.50 [112]~P13(x1121,x1123)+~P14(x1122,x1121)+P11(x1121,x1122,x1123)
% 4.34/4.50 [114]~P13(x1141,x1143)+~P13(x1142,x1141)+P12(x1141,x1142,x1143)
% 4.34/4.50 [132]~P3(x1325,x1321,x1322)+P2(x1321,x1322,x1323,x1324)+~P3(x1325,x1323,x1324)
% 4.34/4.50 [133]~P4(x1334,x1335,x1332,x1333)+P3(x1331,x1332,x1333)+~P3(x1331,x1334,x1335)
% 4.34/4.50 [134]~P5(x1344,x1345,x1342,x1343)+~P3(x1341,x1342,x1343)+~P3(x1341,x1344,x1345)
% 4.34/4.50 [141]~P3(x1412,x1415,x1416)+~P3(x1411,x1413,x1414)+P6(x1411,x1412,x1413,x1414,x1415,x1416)
% 4.34/4.50 [146]~P2(x1463,x1464,x1467,x1468)+~P2(x1461,x1462,x1465,x1466)+P8(x1461,x1462,x1463,x1464,x1465,x1466,x1467,x1468)
% 4.34/4.50 [149]~P7(x1495,x1496,x1491,x1492,x1497,x1498,x1493,x1494)+P5(x1491,x1492,x1493,x1494)+P5(x1495,x1496,x1497,x1498)
% 4.34/4.50 [88]~P1(x881)+E(x881,a2)+E(x881,a4)+E(x881,a1)
% 4.34/4.50 [91]~P1(x911)+~P1(x912)+~E(x912,a1)+E(f3(x911,x912),a1)
% 4.34/4.50 [92]~P1(x922)+~P1(x921)+~E(x921,a1)+E(f3(x921,x922),a1)
% 4.34/4.50 [150]~P3(x1503,x1508,x1509)+~P3(x1502,x1506,x1507)+~P3(x1501,x1504,x1505)+P9(x1501,x1502,x1503,x1504,x1505,x1506,x1507,x1508,x1509)
% 4.34/4.50 [93]~P1(x932)+~P1(x931)+~E(x932,a2)+~E(x931,a2)+E(f3(x931,x932),a2)
% 4.34/4.50 [100]~P1(x1002)+~P1(x1001)+E(f3(x1001,x1002),a1)+E(f3(x1001,x1002),a2)+E(f3(x1001,x1002),a4)
% 4.34/4.50 [94]~P1(x941)+~P1(x942)+~E(x942,a4)+E(x941,a1)+E(x942,a1)+E(f3(x941,x942),a4)
% 4.34/4.50 [95]~P1(x951)+~P1(x952)+~E(x952,a4)+E(x951,a1)+E(x952,a1)+E(f3(x952,x951),a4)
% 4.34/4.50 %EqnAxiom
% 4.34/4.50 [1]E(x11,x11)
% 4.34/4.50 [2]E(x22,x21)+~E(x21,x22)
% 4.34/4.50 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 4.34/4.50 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 4.34/4.50 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 4.34/4.50 [6]~E(x61,x62)+E(f7(x61,x63,x64,x65),f7(x62,x63,x64,x65))
% 4.34/4.50 [7]~E(x71,x72)+E(f7(x73,x71,x74,x75),f7(x73,x72,x74,x75))
% 4.34/4.50 [8]~E(x81,x82)+E(f7(x83,x84,x81,x85),f7(x83,x84,x82,x85))
% 4.34/4.50 [9]~E(x91,x92)+E(f7(x93,x94,x95,x91),f7(x93,x94,x95,x92))
% 4.34/4.50 [10]~E(x101,x102)+E(f8(x101,x103,x104,x105),f8(x102,x103,x104,x105))
% 4.34/4.50 [11]~E(x111,x112)+E(f8(x113,x111,x114,x115),f8(x113,x112,x114,x115))
% 4.34/4.50 [12]~E(x121,x122)+E(f8(x123,x124,x121,x125),f8(x123,x124,x122,x125))
% 4.34/4.50 [13]~E(x131,x132)+E(f8(x133,x134,x135,x131),f8(x133,x134,x135,x132))
% 4.34/4.50 [14]~E(x141,x142)+E(f6(x141,x143,x144,x145),f6(x142,x143,x144,x145))
% 4.34/4.50 [15]~E(x151,x152)+E(f6(x153,x151,x154,x155),f6(x153,x152,x154,x155))
% 4.34/4.50 [16]~E(x161,x162)+E(f6(x163,x164,x161,x165),f6(x163,x164,x162,x165))
% 4.34/4.50 [17]~E(x171,x172)+E(f6(x173,x174,x175,x171),f6(x173,x174,x175,x172))
% 4.34/4.50 [18]~P1(x181)+P1(x182)+~E(x181,x182)
% 4.34/4.50 [19]P9(x192,x193,x194,x195,x196,x197,x198,x199,x1910)+~E(x191,x192)+~P9(x191,x193,x194,x195,x196,x197,x198,x199,x1910)
% 4.34/4.50 [20]P9(x203,x202,x204,x205,x206,x207,x208,x209,x2010)+~E(x201,x202)+~P9(x203,x201,x204,x205,x206,x207,x208,x209,x2010)
% 4.34/4.50 [21]P9(x213,x214,x212,x215,x216,x217,x218,x219,x2110)+~E(x211,x212)+~P9(x213,x214,x211,x215,x216,x217,x218,x219,x2110)
% 4.34/4.50 [22]P9(x223,x224,x225,x222,x226,x227,x228,x229,x2210)+~E(x221,x222)+~P9(x223,x224,x225,x221,x226,x227,x228,x229,x2210)
% 4.34/4.50 [23]P9(x233,x234,x235,x236,x232,x237,x238,x239,x2310)+~E(x231,x232)+~P9(x233,x234,x235,x236,x231,x237,x238,x239,x2310)
% 4.34/4.50 [24]P9(x243,x244,x245,x246,x247,x242,x248,x249,x2410)+~E(x241,x242)+~P9(x243,x244,x245,x246,x247,x241,x248,x249,x2410)
% 4.34/4.50 [25]P9(x253,x254,x255,x256,x257,x258,x252,x259,x2510)+~E(x251,x252)+~P9(x253,x254,x255,x256,x257,x258,x251,x259,x2510)
% 4.34/4.50 [26]P9(x263,x264,x265,x266,x267,x268,x269,x262,x2610)+~E(x261,x262)+~P9(x263,x264,x265,x266,x267,x268,x269,x261,x2610)
% 4.34/4.50 [27]P9(x273,x274,x275,x276,x277,x278,x279,x2710,x272)+~E(x271,x272)+~P9(x273,x274,x275,x276,x277,x278,x279,x2710,x271)
% 4.34/4.50 [28]P3(x282,x283,x284)+~E(x281,x282)+~P3(x281,x283,x284)
% 4.34/4.50 [29]P3(x293,x292,x294)+~E(x291,x292)+~P3(x293,x291,x294)
% 4.34/4.50 [30]P3(x303,x304,x302)+~E(x301,x302)+~P3(x303,x304,x301)
% 4.34/4.50 [31]P13(x312,x313)+~E(x311,x312)+~P13(x311,x313)
% 4.34/4.50 [32]P13(x323,x322)+~E(x321,x322)+~P13(x323,x321)
% 4.34/4.50 [33]P4(x332,x333,x334,x335)+~E(x331,x332)+~P4(x331,x333,x334,x335)
% 4.34/4.50 [34]P4(x343,x342,x344,x345)+~E(x341,x342)+~P4(x343,x341,x344,x345)
% 4.34/4.50 [35]P4(x353,x354,x352,x355)+~E(x351,x352)+~P4(x353,x354,x351,x355)
% 4.34/4.50 [36]P4(x363,x364,x365,x362)+~E(x361,x362)+~P4(x363,x364,x365,x361)
% 4.34/4.50 [37]P2(x372,x373,x374,x375)+~E(x371,x372)+~P2(x371,x373,x374,x375)
% 4.34/4.50 [38]P2(x383,x382,x384,x385)+~E(x381,x382)+~P2(x383,x381,x384,x385)
% 4.34/4.50 [39]P2(x393,x394,x392,x395)+~E(x391,x392)+~P2(x393,x394,x391,x395)
% 4.34/4.50 [40]P2(x403,x404,x405,x402)+~E(x401,x402)+~P2(x403,x404,x405,x401)
% 4.34/4.50 [41]P5(x412,x413,x414,x415)+~E(x411,x412)+~P5(x411,x413,x414,x415)
% 4.34/4.50 [42]P5(x423,x422,x424,x425)+~E(x421,x422)+~P5(x423,x421,x424,x425)
% 4.34/4.50 [43]P5(x433,x434,x432,x435)+~E(x431,x432)+~P5(x433,x434,x431,x435)
% 4.34/4.50 [44]P5(x443,x444,x445,x442)+~E(x441,x442)+~P5(x443,x444,x445,x441)
% 4.34/4.50 [45]P8(x452,x453,x454,x455,x456,x457,x458,x459)+~E(x451,x452)+~P8(x451,x453,x454,x455,x456,x457,x458,x459)
% 4.34/4.50 [46]P8(x463,x462,x464,x465,x466,x467,x468,x469)+~E(x461,x462)+~P8(x463,x461,x464,x465,x466,x467,x468,x469)
% 4.34/4.50 [47]P8(x473,x474,x472,x475,x476,x477,x478,x479)+~E(x471,x472)+~P8(x473,x474,x471,x475,x476,x477,x478,x479)
% 4.34/4.50 [48]P8(x483,x484,x485,x482,x486,x487,x488,x489)+~E(x481,x482)+~P8(x483,x484,x485,x481,x486,x487,x488,x489)
% 4.34/4.50 [49]P8(x493,x494,x495,x496,x492,x497,x498,x499)+~E(x491,x492)+~P8(x493,x494,x495,x496,x491,x497,x498,x499)
% 4.34/4.50 [50]P8(x503,x504,x505,x506,x507,x502,x508,x509)+~E(x501,x502)+~P8(x503,x504,x505,x506,x507,x501,x508,x509)
% 4.34/4.50 [51]P8(x513,x514,x515,x516,x517,x518,x512,x519)+~E(x511,x512)+~P8(x513,x514,x515,x516,x517,x518,x511,x519)
% 4.34/4.50 [52]P8(x523,x524,x525,x526,x527,x528,x529,x522)+~E(x521,x522)+~P8(x523,x524,x525,x526,x527,x528,x529,x521)
% 4.34/4.50 [53]P14(x532,x533)+~E(x531,x532)+~P14(x531,x533)
% 4.34/4.50 [54]P14(x543,x542)+~E(x541,x542)+~P14(x543,x541)
% 4.34/4.50 [55]P12(x552,x553,x554)+~E(x551,x552)+~P12(x551,x553,x554)
% 4.34/4.50 [56]P12(x563,x562,x564)+~E(x561,x562)+~P12(x563,x561,x564)
% 4.34/4.50 [57]P12(x573,x574,x572)+~E(x571,x572)+~P12(x573,x574,x571)
% 4.34/4.50 [58]P11(x582,x583,x584)+~E(x581,x582)+~P11(x581,x583,x584)
% 4.34/4.50 [59]P11(x593,x592,x594)+~E(x591,x592)+~P11(x593,x591,x594)
% 4.34/4.50 [60]P11(x603,x604,x602)+~E(x601,x602)+~P11(x603,x604,x601)
% 4.34/4.50 [61]P10(x612,x613,x614)+~E(x611,x612)+~P10(x611,x613,x614)
% 4.34/4.50 [62]P10(x623,x622,x624)+~E(x621,x622)+~P10(x623,x621,x624)
% 4.34/4.50 [63]P10(x633,x634,x632)+~E(x631,x632)+~P10(x633,x634,x631)
% 4.34/4.50 [64]P7(x642,x643,x644,x645,x646,x647,x648,x649)+~E(x641,x642)+~P7(x641,x643,x644,x645,x646,x647,x648,x649)
% 4.34/4.50 [65]P7(x653,x652,x654,x655,x656,x657,x658,x659)+~E(x651,x652)+~P7(x653,x651,x654,x655,x656,x657,x658,x659)
% 4.34/4.50 [66]P7(x663,x664,x662,x665,x666,x667,x668,x669)+~E(x661,x662)+~P7(x663,x664,x661,x665,x666,x667,x668,x669)
% 4.34/4.50 [67]P7(x673,x674,x675,x672,x676,x677,x678,x679)+~E(x671,x672)+~P7(x673,x674,x675,x671,x676,x677,x678,x679)
% 4.34/4.50 [68]P7(x683,x684,x685,x686,x682,x687,x688,x689)+~E(x681,x682)+~P7(x683,x684,x685,x686,x681,x687,x688,x689)
% 4.34/4.50 [69]P7(x693,x694,x695,x696,x697,x692,x698,x699)+~E(x691,x692)+~P7(x693,x694,x695,x696,x697,x691,x698,x699)
% 4.34/4.50 [70]P7(x703,x704,x705,x706,x707,x708,x702,x709)+~E(x701,x702)+~P7(x703,x704,x705,x706,x707,x708,x701,x709)
% 4.34/4.50 [71]P7(x713,x714,x715,x716,x717,x718,x719,x712)+~E(x711,x712)+~P7(x713,x714,x715,x716,x717,x718,x719,x711)
% 4.34/4.50 [72]P6(x722,x723,x724,x725,x726,x727)+~E(x721,x722)+~P6(x721,x723,x724,x725,x726,x727)
% 4.34/4.50 [73]P6(x733,x732,x734,x735,x736,x737)+~E(x731,x732)+~P6(x733,x731,x734,x735,x736,x737)
% 4.34/4.50 [74]P6(x743,x744,x742,x745,x746,x747)+~E(x741,x742)+~P6(x743,x744,x741,x745,x746,x747)
% 4.34/4.50 [75]P6(x753,x754,x755,x752,x756,x757)+~E(x751,x752)+~P6(x753,x754,x755,x751,x756,x757)
% 4.34/4.50 [76]P6(x763,x764,x765,x766,x762,x767)+~E(x761,x762)+~P6(x763,x764,x765,x766,x761,x767)
% 4.34/4.50 [77]P6(x773,x774,x775,x776,x777,x772)+~E(x771,x772)+~P6(x773,x774,x775,x776,x777,x771)
% 4.34/4.50
% 4.34/4.50 %-------------------------------------------
% 4.34/4.50 cnf(912,plain,
% 4.34/4.50 (~P3(f8(a5,a10,a9,a10),a9,a10)),
% 4.34/4.50 inference(scs_inference,[],[83,131,139])).
% 4.34/4.50 cnf(913,plain,
% 4.34/4.50 ($false),
% 4.34/4.50 inference(scs_inference,[],[912,83,138]),
% 4.34/4.50 ['proof']).
% 4.34/4.50 % SZS output end Proof
% 4.34/4.50 % Total time :3.983981s
%------------------------------------------------------------------------------