%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT094+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 0.25s 0.54s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT094+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 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 14:27:11 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.25/0.53 start to proof:theBenchmark
% 0.25/0.53 %-------------------------------------------
% 0.25/0.53 % File :CSE---1.7
% 0.25/0.53 % Problem :theBenchmark
% 0.25/0.53 % Transform :cnf
% 0.25/0.53 % Format :tptp:raw
% 0.25/0.53 % Command :java -jar mcs_scs.jar %d %s
% 0.25/0.53
% 0.25/0.53 % Result :Theorem 0.006270s
% 0.25/0.53 % Output :CNFRefutation 0.006270s
% 0.25/0.53 %-------------------------------------------
% 0.25/0.53 %--------------------------------------------------------------------------
% 0.25/0.53 % File : MGT094+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 0.25/0.53 % Domain : Management
% 0.25/0.53 % Problem : 4-axis box containment: width axis escapes => Conflict
% 0.25/0.53 % Version : Especial.
% 0.25/0.53 % English : Width: (0,800] not_subset (0,600] Conflict <= escape axis
% 0.25/0.53 % Height: (0,400] subseteq (0,800] Compatible
% 0.25/0.53 % Depth: (0,16] subseteq (0,32] Compatible
% 0.25/0.53 % Alt: (0,150] subseteq (0,300] Compatible
% 0.25/0.53 % box_subs chained: one Conflict => overall Conflict
% 0.25/0.53
% 0.25/0.53 % Refs : [MC+26] Mustafa et al. (2026), Axis Decomposition for ODRL
% 0.25/0.53 % Source : [MC+26]
% 0.25/0.53 % Names : ODRL653-1.p [MC+26]
% 0.25/0.53
% 0.25/0.53 % Status : Theorem
% 0.25/0.53 % Rating : ? v9.3.1
% 0.25/0.53 % Syntax : Number of formulae : 80 ( 51 unt; 0 def)
% 0.25/0.53 % Number of atoms : 183 ( 77 equ)
% 0.25/0.53 % Maximal formula atoms : 28 ( 2 avg)
% 0.25/0.54 % Number of connectives : 144 ( 41 ~; 15 |; 60 &)
% 0.25/0.54 % ( 8 <=>; 20 =>; 0 <=; 0 <~>)
% 0.25/0.54 % Maximal formula depth : 29 ( 4 avg)
% 0.25/0.54 % Maximal term depth : 2 ( 1 avg)
% 0.25/0.54 % Number of predicates : 13 ( 12 usr; 0 prp; 1-4 aty)
% 0.25/0.54 % Number of functors : 16 ( 16 usr; 13 con; 0-6 aty)
% 0.25/0.54 % Number of variables : 92 ( 90 !; 2 ?)
% 0.25/0.54 % SPC : FOF_THM_RFO_SEQ
% 0.25/0.54
% 0.25/0.54 % Comments : Requires MGT002+0.ax + MGT002+2.ax.
% 0.25/0.54 % Bugfixes : v9.3.1 - $distinct expanded to inequalities.
% 0.25/0.54 %--------------------------------------------------------------------------
% 0.25/0.54 include('Axioms/MGT002+0.ax').
% 0.25/0.54 include('Axioms/MGT002+2.ax').
% 0.25/0.54 include('Axioms/MGT002+7.ax').
% 0.25/0.54 %--------------------------------------------------------------------------
% 0.25/0.54 %----Named constants and ordering
% 0.25/0.54 fof(val_v0,axiom,
% 0.25/0.54 val(v0) ).
% 0.25/0.54
% 0.25/0.54 fof(val_v16,axiom,
% 0.25/0.54 val(v16) ).
% 0.25/0.54
% 0.25/0.54 fof(val_v32,axiom,
% 0.25/0.54 val(v32) ).
% 0.25/0.54
% 0.25/0.54 fof(val_v150,axiom,
% 0.25/0.54 val(v150) ).
% 0.25/0.54
% 0.25/0.54 fof(val_v300,axiom,
% 0.25/0.54 val(v300) ).
% 0.25/0.54
% 0.25/0.54 fof(val_v400,axiom,
% 0.25/0.54 val(v400) ).
% 0.25/0.54
% 0.25/0.54 fof(val_v600,axiom,
% 0.25/0.54 val(v600) ).
% 0.25/0.54
% 0.25/0.54 fof(val_v800,axiom,
% 0.25/0.54 val(v800) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v0_v16,axiom,
% 0.25/0.54 less(v0,v16) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v0_v32,axiom,
% 0.25/0.54 less(v0,v32) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v0_v150,axiom,
% 0.25/0.54 less(v0,v150) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v0_v300,axiom,
% 0.25/0.54 less(v0,v300) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v0_v400,axiom,
% 0.25/0.54 less(v0,v400) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v0_v600,axiom,
% 0.25/0.54 less(v0,v600) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v0_v800,axiom,
% 0.25/0.54 less(v0,v800) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v16_v32,axiom,
% 0.25/0.54 less(v16,v32) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v16_v150,axiom,
% 0.25/0.54 less(v16,v150) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v16_v300,axiom,
% 0.25/0.54 less(v16,v300) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v16_v400,axiom,
% 0.25/0.54 less(v16,v400) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v16_v600,axiom,
% 0.25/0.54 less(v16,v600) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v16_v800,axiom,
% 0.25/0.54 less(v16,v800) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v32_v150,axiom,
% 0.25/0.54 less(v32,v150) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v32_v300,axiom,
% 0.25/0.54 less(v32,v300) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v32_v400,axiom,
% 0.25/0.54 less(v32,v400) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v32_v600,axiom,
% 0.25/0.54 less(v32,v600) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v32_v800,axiom,
% 0.25/0.54 less(v32,v800) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v150_v300,axiom,
% 0.25/0.54 less(v150,v300) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v150_v400,axiom,
% 0.25/0.54 less(v150,v400) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v150_v600,axiom,
% 0.25/0.54 less(v150,v600) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v150_v800,axiom,
% 0.25/0.54 less(v150,v800) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v300_v400,axiom,
% 0.25/0.54 less(v300,v400) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v300_v600,axiom,
% 0.25/0.54 less(v300,v600) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v300_v800,axiom,
% 0.25/0.54 less(v300,v800) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v400_v600,axiom,
% 0.25/0.54 less(v400,v600) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v400_v800,axiom,
% 0.25/0.54 less(v400,v800) ).
% 0.25/0.54
% 0.25/0.54 fof(ord_v600_v800,axiom,
% 0.25/0.54 less(v600,v800) ).
% 0.25/0.54
% 0.25/0.54 fof(distinct,axiom,
% 0.25/0.54 ( v0 != v16
% 0.25/0.54 & v0 != v32
% 0.25/0.54 & v0 != v150
% 0.25/0.54 & v0 != v300
% 0.25/0.54 & v0 != v400
% 0.25/0.54 & v0 != v600
% 0.25/0.54 & v0 != v800
% 0.25/0.54 & v16 != v32
% 0.25/0.54 & v16 != v150
% 0.25/0.54 & v16 != v300
% 0.25/0.54 & v16 != v400
% 0.25/0.54 & v16 != v600
% 0.25/0.54 & v16 != v800
% 0.25/0.54 & v32 != v150
% 0.25/0.54 & v32 != v300
% 0.25/0.54 & v32 != v400
% 0.25/0.54 & v32 != v600
% 0.25/0.54 & v32 != v800
% 0.25/0.54 & v150 != v300
% 0.25/0.54 & v150 != v400
% 0.25/0.54 & v150 != v600
% 0.25/0.54 & v150 != v800
% 0.25/0.54 & v300 != v400
% 0.25/0.54 & v300 != v600
% 0.25/0.54 & v300 != v800
% 0.25/0.54 & v400 != v600
% 0.25/0.54 & v400 != v800
% 0.25/0.54 & v600 != v800 ) ).
% 0.25/0.54
% 0.25/0.54 fof(no_subs_hint,axiom,
% 0.25/0.54 ~ axis_subsumes(v0,v800,v0,v600) ).
% 0.25/0.54
% 0.25/0.54 fof(odrl653,conjecture,
% 0.25/0.54 subs_verdict(v0,v800,present,v0,v600,present) = conflict ).
% 0.25/0.54
% 0.25/0.54 %--------------------------------------------------------------------------
% 0.25/0.54 %-------------------------------------------
% 0.25/0.54 % Proof found
% 0.25/0.54 % SZS status Theorem for theBenchmark
% 0.25/0.54 % SZS output start Proof
% 0.25/0.54 %ClaNum:183(EqnAxiom:56)
% 0.25/0.54 %VarNum:341(SingletonVarNum:150)
% 0.25/0.54 %MaxLitNum:6
% 0.25/0.54 %MaxfuncDepth:1
% 0.25/0.54 %SharedTerms:89
% 0.25/0.54 %goalClause: 135
% 0.25/0.54 %singleGoalClaCount:1
% 0.25/0.54 [57]P1(a1)
% 0.25/0.54 [58]P1(a2)
% 0.25/0.54 [59]P1(a6)
% 0.25/0.54 [60]P2(a7)
% 0.25/0.54 [61]P2(a3)
% 0.25/0.54 [62]P10(a12)
% 0.25/0.55 [63]P10(a13)
% 0.25/0.55 [64]P10(a15)
% 0.25/0.55 [65]P10(a14)
% 0.25/0.55 [66]P10(a16)
% 0.25/0.55 [67]P10(a17)
% 0.25/0.55 [68]P10(a18)
% 0.25/0.55 [69]P10(a19)
% 0.25/0.55 [70]P11(a12,a13)
% 0.25/0.55 [71]P11(a12,a15)
% 0.25/0.55 [72]P11(a12,a14)
% 0.25/0.55 [73]P11(a12,a16)
% 0.25/0.55 [74]P11(a12,a17)
% 0.25/0.55 [75]P11(a12,a18)
% 0.25/0.55 [76]P11(a12,a19)
% 0.25/0.55 [77]P11(a13,a15)
% 0.25/0.55 [78]P11(a13,a14)
% 0.25/0.55 [79]P11(a13,a16)
% 0.25/0.55 [80]P11(a13,a17)
% 0.25/0.55 [81]P11(a13,a18)
% 0.25/0.55 [82]P11(a13,a19)
% 0.25/0.55 [83]P11(a15,a14)
% 0.25/0.55 [84]P11(a15,a16)
% 0.25/0.55 [85]P11(a15,a17)
% 0.25/0.55 [86]P11(a15,a18)
% 0.25/0.55 [87]P11(a15,a19)
% 0.25/0.55 [88]P11(a14,a16)
% 0.25/0.55 [89]P11(a14,a17)
% 0.25/0.55 [90]P11(a14,a18)
% 0.25/0.55 [91]P11(a14,a19)
% 0.25/0.55 [92]P11(a16,a17)
% 0.25/0.55 [93]P11(a16,a18)
% 0.25/0.55 [94]P11(a16,a19)
% 0.25/0.55 [95]P11(a17,a18)
% 0.25/0.55 [96]P11(a17,a19)
% 0.25/0.55 [97]P11(a18,a19)
% 0.25/0.55 [101]~E(a1,a2)
% 0.25/0.55 [102]~E(a1,a6)
% 0.25/0.55 [103]~E(a6,a2)
% 0.25/0.55 [104]~E(a3,a7)
% 0.25/0.55 [105]~E(a13,a12)
% 0.25/0.55 [106]~E(a15,a12)
% 0.25/0.55 [107]~E(a15,a13)
% 0.25/0.55 [108]~E(a14,a12)
% 0.25/0.55 [109]~E(a14,a13)
% 0.25/0.55 [110]~E(a14,a15)
% 0.25/0.55 [111]~E(a16,a12)
% 0.25/0.55 [112]~E(a16,a13)
% 0.25/0.55 [113]~E(a16,a15)
% 0.25/0.55 [114]~E(a16,a14)
% 0.25/0.55 [115]~E(a17,a12)
% 0.25/0.55 [116]~E(a17,a13)
% 0.25/0.55 [117]~E(a17,a15)
% 0.25/0.55 [118]~E(a17,a14)
% 0.25/0.55 [119]~E(a17,a16)
% 0.25/0.55 [120]~E(a18,a12)
% 0.25/0.55 [121]~E(a18,a13)
% 0.25/0.55 [122]~E(a18,a15)
% 0.25/0.55 [123]~E(a18,a14)
% 0.25/0.55 [124]~E(a18,a16)
% 0.25/0.55 [125]~E(a18,a17)
% 0.25/0.55 [126]~E(a19,a12)
% 0.25/0.55 [127]~E(a19,a13)
% 0.25/0.55 [128]~E(a19,a15)
% 0.25/0.55 [129]~E(a19,a14)
% 0.25/0.55 [130]~E(a19,a16)
% 0.25/0.55 [131]~E(a19,a17)
% 0.25/0.55 [132]~E(a19,a18)
% 0.25/0.55 [134]~P3(a12,a19,a12,a18)
% 0.25/0.55 [135]~E(f11(a12,a19,a7,a12,a18,a7),a1)
% 0.25/0.55 [133]~P11(x1331,x1331)
% 0.25/0.55 [98]E(f11(x981,x982,a7,x983,x984,a3),a6)
% 0.25/0.55 [99]E(f11(x991,x992,a3,x993,x994,a7),a6)
% 0.25/0.55 [100]E(f11(x1001,x1002,a3,x1003,x1004,a3),a6)
% 0.25/0.55 [138]~E(x1381,x1382)+P12(x1381,x1382)
% 0.25/0.55 [151]~P11(x1511,x1512)+P12(x1511,x1512)
% 0.25/0.55 [164]P11(x1641,x1642)+~P7(x1642,x1641,x1643)
% 0.25/0.55 [165]P11(x1651,x1652)+~P8(x1651,x1653,x1652)
% 0.25/0.55 [166]P11(x1661,x1662)+~P9(x1662,x1661,x1663)
% 0.25/0.55 [167]P11(x1671,x1672)+~P9(x1671,x1673,x1672)
% 0.25/0.55 [168]P12(x1681,x1682)+~P6(x1682,x1681,x1683)
% 0.25/0.55 [169]P12(x1691,x1692)+~P6(x1691,x1693,x1692)
% 0.25/0.55 [170]P12(x1701,x1702)+~P7(x1701,x1703,x1702)
% 0.25/0.55 [171]P12(x1711,x1712)+~P8(x1712,x1711,x1713)
% 0.25/0.55 [175]P5(x1751,x1752,x1753,x1754)+P6(f8(x1751,x1752,x1753,x1754),x1753,x1754)
% 0.25/0.55 [176]P5(x1761,x1762,x1763,x1764)+P6(f8(x1761,x1762,x1763,x1764),x1761,x1762)
% 0.25/0.55 [177]P3(x1771,x1772,x1773,x1774)+P6(f9(x1771,x1772,x1773,x1774),x1771,x1772)
% 0.25/0.55 [178]~P4(x1781,x1782,x1783,x1784)+P6(f10(x1781,x1782,x1783,x1784),x1783,x1784)
% 0.25/0.55 [179]~P4(x1791,x1792,x1793,x1794)+P6(f10(x1791,x1792,x1793,x1794),x1791,x1792)
% 0.25/0.55 [180]P3(x1801,x1802,x1803,x1804)+~P6(f9(x1801,x1802,x1803,x1804),x1803,x1804)
% 0.25/0.55 [181]P3(x1811,x1812,x1813,x1814)+E(f11(x1811,x1812,a7,x1813,x1814,a7),a1)
% 0.25/0.55 [182]~P3(x1821,x1822,x1823,x1824)+E(f11(x1821,x1822,a7,x1823,x1824,a7),a2)
% 0.25/0.55 [136]~P2(x1361)+E(x1361,a3)+E(x1361,a7)
% 0.25/0.55 [139]P11(x1392,x1391)+P11(x1391,x1392)+E(x1391,x1392)
% 0.25/0.55 [152]P11(x1521,x1522)+~P12(x1521,x1522)+E(x1521,x1522)
% 0.25/0.55 [153]~P12(x1532,x1531)+~P12(x1531,x1532)+E(x1531,x1532)
% 0.25/0.55 [156]~P11(x1561,x1563)+P11(x1561,x1562)+~P11(x1563,x1562)
% 0.25/0.55 [157]~P12(x1571,x1573)+P11(x1571,x1572)+~P11(x1573,x1572)
% 0.25/0.55 [158]~P12(x1583,x1582)+P11(x1581,x1582)+~P11(x1581,x1583)
% 0.25/0.55 [159]~P12(x1591,x1593)+P12(x1591,x1592)+~P12(x1593,x1592)
% 0.25/0.55 [160]~P12(x1601,x1603)+~P12(x1602,x1601)+P6(x1601,x1602,x1603)
% 0.25/0.55 [161]~P11(x1612,x1611)+~P12(x1611,x1613)+P7(x1611,x1612,x1613)
% 0.25/0.55 [162]~P11(x1621,x1623)+~P12(x1622,x1621)+P8(x1621,x1622,x1623)
% 0.25/0.55 [163]~P11(x1631,x1633)+~P11(x1632,x1631)+P9(x1631,x1632,x1633)
% 0.25/0.55 [172]~P6(x1725,x1721,x1722)+P4(x1721,x1722,x1723,x1724)+~P6(x1725,x1723,x1724)
% 0.25/0.55 [173]~P3(x1734,x1735,x1732,x1733)+P6(x1731,x1732,x1733)+~P6(x1731,x1734,x1735)
% 0.25/0.55 [174]~P5(x1744,x1745,x1742,x1743)+~P6(x1741,x1742,x1743)+~P6(x1741,x1744,x1745)
% 0.25/0.55 [137]~P1(x1371)+E(x1371,a2)+E(x1371,a6)+E(x1371,a1)
% 0.25/0.55 [140]~P1(x1401)+~P1(x1402)+~E(x1402,a1)+E(f4(x1401,x1402),a1)
% 0.25/0.55 [141]~P1(x1412)+~P1(x1411)+~E(x1411,a1)+E(f4(x1411,x1412),a1)
% 0.25/0.55 [142]~P1(x1421)+~P1(x1422)+~E(x1422,a1)+E(f5(x1421,x1422),a1)
% 0.25/0.55 [143]~P1(x1432)+~P1(x1431)+~E(x1431,a1)+E(f5(x1431,x1432),a1)
% 0.25/0.55 [146]~P1(x1462)+~P1(x1461)+~E(x1462,a2)+~E(x1461,a2)+E(f4(x1461,x1462),a2)
% 0.25/0.55 [147]~P1(x1472)+~P1(x1471)+~E(x1472,a2)+~E(x1471,a2)+E(f5(x1471,x1472),a2)
% 0.25/0.55 [154]~P1(x1542)+~P1(x1541)+E(f4(x1541,x1542),a1)+E(f4(x1541,x1542),a2)+E(f4(x1541,x1542),a6)
% 0.25/0.55 [155]~P1(x1552)+~P1(x1551)+E(f5(x1551,x1552),a1)+E(f5(x1551,x1552),a2)+E(f5(x1551,x1552),a6)
% 0.25/0.55 [183]~P2(x1836)+~P2(x1833)+E(f11(x1831,x1832,x1833,x1834,x1835,x1836),a1)+E(f11(x1831,x1832,x1833,x1834,x1835,x1836),a2)+E(f11(x1831,x1832,x1833,x1834,x1835,x1836),a6)
% 0.25/0.55 [144]~P1(x1441)+~P1(x1442)+E(x1442,a2)+E(x1441,a1)+E(x1442,a1)+E(f5(x1441,x1442),a6)
% 0.25/0.55 [145]~P1(x1451)+~P1(x1452)+E(x1452,a2)+E(x1451,a1)+E(x1452,a1)+E(f5(x1452,x1451),a6)
% 0.25/0.55 [148]~P1(x1481)+~P1(x1482)+~E(x1482,a6)+E(x1481,a1)+E(x1482,a1)+E(f4(x1481,x1482),a6)
% 0.25/0.55 [149]~P1(x1491)+~P1(x1492)+~E(x1492,a6)+E(x1491,a1)+E(x1492,a1)+E(f4(x1492,x1491),a6)
% 0.25/0.55 %EqnAxiom
% 0.25/0.55 [1]E(x11,x11)
% 0.25/0.55 [2]E(x22,x21)+~E(x21,x22)
% 0.25/0.55 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.25/0.55 [4]~E(x41,x42)+E(f11(x41,x43,x44,x45,x46,x47),f11(x42,x43,x44,x45,x46,x47))
% 0.25/0.55 [5]~E(x51,x52)+E(f11(x53,x51,x54,x55,x56,x57),f11(x53,x52,x54,x55,x56,x57))
% 0.25/0.55 [6]~E(x61,x62)+E(f11(x63,x64,x61,x65,x66,x67),f11(x63,x64,x62,x65,x66,x67))
% 0.25/0.55 [7]~E(x71,x72)+E(f11(x73,x74,x75,x71,x76,x77),f11(x73,x74,x75,x72,x76,x77))
% 0.25/0.55 [8]~E(x81,x82)+E(f11(x83,x84,x85,x86,x81,x87),f11(x83,x84,x85,x86,x82,x87))
% 0.25/0.55 [9]~E(x91,x92)+E(f11(x93,x94,x95,x96,x97,x91),f11(x93,x94,x95,x96,x97,x92))
% 0.25/0.55 [10]~E(x101,x102)+E(f9(x101,x103,x104,x105),f9(x102,x103,x104,x105))
% 0.25/0.55 [11]~E(x111,x112)+E(f9(x113,x111,x114,x115),f9(x113,x112,x114,x115))
% 0.25/0.55 [12]~E(x121,x122)+E(f9(x123,x124,x121,x125),f9(x123,x124,x122,x125))
% 0.25/0.55 [13]~E(x131,x132)+E(f9(x133,x134,x135,x131),f9(x133,x134,x135,x132))
% 0.25/0.55 [14]~E(x141,x142)+E(f10(x141,x143,x144,x145),f10(x142,x143,x144,x145))
% 0.25/0.55 [15]~E(x151,x152)+E(f10(x153,x151,x154,x155),f10(x153,x152,x154,x155))
% 0.25/0.55 [16]~E(x161,x162)+E(f10(x163,x164,x161,x165),f10(x163,x164,x162,x165))
% 0.25/0.55 [17]~E(x171,x172)+E(f10(x173,x174,x175,x171),f10(x173,x174,x175,x172))
% 0.25/0.55 [18]~E(x181,x182)+E(f8(x181,x183,x184,x185),f8(x182,x183,x184,x185))
% 0.25/0.55 [19]~E(x191,x192)+E(f8(x193,x191,x194,x195),f8(x193,x192,x194,x195))
% 0.25/0.55 [20]~E(x201,x202)+E(f8(x203,x204,x201,x205),f8(x203,x204,x202,x205))
% 0.25/0.55 [21]~E(x211,x212)+E(f8(x213,x214,x215,x211),f8(x213,x214,x215,x212))
% 0.25/0.55 [22]~E(x221,x222)+E(f4(x221,x223),f4(x222,x223))
% 0.25/0.55 [23]~E(x231,x232)+E(f4(x233,x231),f4(x233,x232))
% 0.25/0.55 [24]~E(x241,x242)+E(f5(x241,x243),f5(x242,x243))
% 0.25/0.55 [25]~E(x251,x252)+E(f5(x253,x251),f5(x253,x252))
% 0.25/0.55 [26]~P1(x261)+P1(x262)+~E(x261,x262)
% 0.25/0.55 [27]~P2(x271)+P2(x272)+~E(x271,x272)
% 0.25/0.55 [28]P7(x282,x283,x284)+~E(x281,x282)+~P7(x281,x283,x284)
% 0.25/0.55 [29]P7(x293,x292,x294)+~E(x291,x292)+~P7(x293,x291,x294)
% 0.25/0.55 [30]P7(x303,x304,x302)+~E(x301,x302)+~P7(x303,x304,x301)
% 0.25/0.55 [31]P12(x312,x313)+~E(x311,x312)+~P12(x311,x313)
% 0.25/0.55 [32]P12(x323,x322)+~E(x321,x322)+~P12(x323,x321)
% 0.25/0.55 [33]P6(x332,x333,x334)+~E(x331,x332)+~P6(x331,x333,x334)
% 0.25/0.55 [34]P6(x343,x342,x344)+~E(x341,x342)+~P6(x343,x341,x344)
% 0.25/0.55 [35]P6(x353,x354,x352)+~E(x351,x352)+~P6(x353,x354,x351)
% 0.25/0.55 [36]~P10(x361)+P10(x362)+~E(x361,x362)
% 0.25/0.55 [37]P11(x372,x373)+~E(x371,x372)+~P11(x371,x373)
% 0.25/0.55 [38]P11(x383,x382)+~E(x381,x382)+~P11(x383,x381)
% 0.25/0.55 [39]P8(x392,x393,x394)+~E(x391,x392)+~P8(x391,x393,x394)
% 0.25/0.55 [40]P8(x403,x402,x404)+~E(x401,x402)+~P8(x403,x401,x404)
% 0.25/0.55 [41]P8(x413,x414,x412)+~E(x411,x412)+~P8(x413,x414,x411)
% 0.25/0.55 [42]P4(x422,x423,x424,x425)+~E(x421,x422)+~P4(x421,x423,x424,x425)
% 0.25/0.55 [43]P4(x433,x432,x434,x435)+~E(x431,x432)+~P4(x433,x431,x434,x435)
% 0.25/0.55 [44]P4(x443,x444,x442,x445)+~E(x441,x442)+~P4(x443,x444,x441,x445)
% 0.25/0.55 [45]P4(x453,x454,x455,x452)+~E(x451,x452)+~P4(x453,x454,x455,x451)
% 0.25/0.55 [46]P9(x462,x463,x464)+~E(x461,x462)+~P9(x461,x463,x464)
% 0.25/0.55 [47]P9(x473,x472,x474)+~E(x471,x472)+~P9(x473,x471,x474)
% 0.25/0.55 [48]P9(x483,x484,x482)+~E(x481,x482)+~P9(x483,x484,x481)
% 0.25/0.55 [49]P3(x492,x493,x494,x495)+~E(x491,x492)+~P3(x491,x493,x494,x495)
% 0.25/0.55 [50]P3(x503,x502,x504,x505)+~E(x501,x502)+~P3(x503,x501,x504,x505)
% 0.25/0.55 [51]P3(x513,x514,x512,x515)+~E(x511,x512)+~P3(x513,x514,x511,x515)
% 0.25/0.55 [52]P3(x523,x524,x525,x522)+~E(x521,x522)+~P3(x523,x524,x525,x521)
% 0.25/0.55 [53]P5(x532,x533,x534,x535)+~E(x531,x532)+~P5(x531,x533,x534,x535)
% 0.25/0.55 [54]P5(x543,x542,x544,x545)+~E(x541,x542)+~P5(x543,x541,x544,x545)
% 0.25/0.55 [55]P5(x553,x554,x552,x555)+~E(x551,x552)+~P5(x553,x554,x551,x555)
% 0.25/0.55 [56]P5(x563,x564,x565,x562)+~E(x561,x562)+~P5(x563,x564,x565,x561)
% 0.25/0.55
% 0.25/0.55 %-------------------------------------------
% 0.25/0.55 cnf(191,plain,
% 0.25/0.55 ($false),
% 0.25/0.55 inference(scs_inference,[],[134,135,181]),
% 0.25/0.55 ['proof']).
% 0.25/0.55 % SZS output end Proof
% 0.25/0.55 % Total time :0.006270s
%------------------------------------------------------------------------------