%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUM228-1 : TPTP v8.2.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n020.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 12:23:31 EDT 2024
% Result : Unsatisfiable 0.11s 0.52s
% Output : CNFRefutation 0.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.07 % Problem : NUM228-1 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.00/0.07 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.06/0.26 % Computer : n020.cluster.edu
% 0.06/0.26 % Model : x86_64 x86_64
% 0.06/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.26 % Memory : 8042.1875MB
% 0.06/0.26 % OS : Linux 3.10.0-693.el7.x86_64
% 0.06/0.26 % CPULimit : 300
% 0.06/0.26 % WCLimit : 300
% 0.06/0.26 % DateTime : Sun Jun 23 01:43:54 EDT 2024
% 0.06/0.26 % CPUTime :
% 0.11/0.43 start to proof:theBenchmark
% 0.11/0.52 %-------------------------------------------
% 0.11/0.52 % File :CSE---1.7
% 0.11/0.52 % Problem :theBenchmark
% 0.11/0.52 % Transform :cnf
% 0.11/0.52 % Format :tptp:raw
% 0.11/0.52 % Command :java -jar mcs_scs.jar %d %s
% 0.11/0.52
% 0.11/0.52 % Result :Theorem 0.010000s
% 0.11/0.52 % Output :CNFRefutation 0.010000s
% 0.11/0.52 %-------------------------------------------
% 0.11/0.52 %--------------------------------------------------------------------------
% 0.11/0.52 % File : NUM228-1 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.11/0.52 % Domain : Number Theory (Ordinals)
% 0.11/0.52 % Problem : Corollary to recursion equation functions definition
% 0.11/0.52 % Version : [Qua92] axioms.
% 0.11/0.52 % English :
% 0.11/0.52
% 0.11/0.52 % Refs : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 0.11/0.52 % Source : [Quaife]
% 0.11/0.52 % Names : TRECDEF4 cor. [Quaife]
% 0.11/0.52
% 0.11/0.52 % Status : Unsatisfiable
% 0.11/0.52 % Rating : 0.20 v8.2.0, 0.24 v8.1.0, 0.21 v7.4.0, 0.24 v7.3.0, 0.17 v7.0.0, 0.27 v6.3.0, 0.09 v6.2.0, 0.10 v6.1.0, 0.07 v6.0.0, 0.10 v5.5.0, 0.20 v5.3.0, 0.17 v5.2.0, 0.19 v5.1.0, 0.24 v5.0.0, 0.21 v4.1.0, 0.31 v4.0.1, 0.36 v3.7.0, 0.40 v3.5.0, 0.36 v3.4.0, 0.25 v3.3.0, 0.21 v3.2.0, 0.08 v3.1.0, 0.18 v2.7.0, 0.17 v2.6.0, 0.00 v2.5.0, 0.09 v2.4.0, 0.00 v2.1.0
% 0.11/0.52 % Syntax : Number of clauses : 160 ( 48 unt; 12 nHn; 121 RR)
% 0.11/0.52 % Number of literals : 324 ( 72 equ; 157 neg)
% 0.11/0.52 % Maximal clause size : 5 ( 2 avg)
% 0.11/0.52 % Maximal term depth : 6 ( 1 avg)
% 0.11/0.52 % Number of predicates : 17 ( 16 usr; 0 prp; 1-3 aty)
% 0.11/0.52 % Number of functors : 63 ( 63 usr; 19 con; 0-3 aty)
% 0.11/0.52 % Number of variables : 303 ( 40 sgn)
% 0.11/0.52 % SPC : CNF_UNS_RFO_SEQ_NHN
% 0.11/0.52
% 0.11/0.52 % Comments : Not in [Qua92]. Theorem TRECDEF4 cor. in [Quaife].
% 0.11/0.52 % : Quaife proves all these problems by augmenting the axioms with
% 0.11/0.52 % all previously proved theorems. The user may create an augmented
% 0.11/0.52 % version of this problem by adding all previously proved theorems.
% 0.11/0.52 % These include all of [Qua92]'s set theory and Boolean algebra
% 0.11/0.52 % theorems, available from the SET domain.
% 0.11/0.52 % Bugfixes : v1.0.1 - Bugfix in SET004-1.ax.
% 0.11/0.52 % : v2.1.0 - Bugfix in SET004-0.ax.
% 0.11/0.52 %--------------------------------------------------------------------------
% 0.11/0.52 %----Include von Neuman-Bernays-Godel set theory axioms
% 0.11/0.52 include('Axioms/SET004-0.ax').
% 0.11/0.52 %----Include Set theory (Boolean algebra) axioms based on NBG set theory
% 0.11/0.52 include('Axioms/SET004-1.ax').
% 0.11/0.52 %----Include ordinal number theory axioms.
% 0.11/0.52 include('Axioms/NUM004-0.ax').
% 0.11/0.52 %--------------------------------------------------------------------------
% 0.11/0.52 cnf(prove_corollary_1,negated_conjecture,
% 0.11/0.52 ~ function(z) ).
% 0.11/0.52
% 0.11/0.52 cnf(prove_corollary_2,negated_conjecture,
% 0.11/0.52 recursion_equation_functions(z) != null_class ).
% 0.11/0.52
% 0.11/0.52 %--------------------------------------------------------------------------
% 0.11/0.52 %-------------------------------------------
% 0.11/0.52 % Proof found
% 0.11/0.52 % SZS status Theorem for theBenchmark
% 0.11/0.52 % SZS output start Proof
% 0.11/0.52 %ClaNum:215(EqnAxiom:74)
% 0.11/0.52 %VarNum:1151(SingletonVarNum:271)
% 0.11/0.52 %MaxLitNum:5
% 0.11/0.52 %MaxfuncDepth:24
% 0.11/0.53 %SharedTerms:69
% 0.11/0.53 %goalClause: 102 103
% 0.11/0.53 %singleGoalClaCount:2
% 0.11/0.53 [75]P1(a1)
% 0.11/0.53 [76]P2(a2)
% 0.11/0.53 [77]P7(a1,a27)
% 0.11/0.53 [103]~P2(a44)
% 0.11/0.53 [80]P10(a9,f10(a27,a27))
% 0.11/0.53 [81]P10(a31,f10(a27,a27))
% 0.11/0.53 [82]P10(a14,f10(a27,a27))
% 0.11/0.53 [83]P10(a32,f10(a27,a27))
% 0.11/0.53 [84]P10(a42,f10(a27,a27))
% 0.11/0.53 [102]~E(f35(a44),a22)
% 0.11/0.53 [79]E(f8(f7(a6),a28),a20)
% 0.11/0.53 [89]P10(a13,f10(a27,f10(a27,a27)))
% 0.11/0.53 [90]P10(a3,f10(a27,f10(a27,a27)))
% 0.11/0.53 [91]E(f8(f7(f12(a9,f7(a16))),a9),a37)
% 0.11/0.53 [95]E(f8(f15(f17(f10(a41,a27))),a41),a16)
% 0.11/0.53 [96]E(f8(f10(a27,a27),f8(f10(a27,a27),f7(f12(f7(a9),f15(f17(f10(a9,a27))))))),a41)
% 0.11/0.53 [98]E(f7(f8(f7(f43(a22,a22)),f7(f15(f15(f17(f10(f8(a31,f10(a28,a27)),a27))))))),a6)
% 0.11/0.53 [78]P10(x781,a27)
% 0.11/0.53 [86]P10(f11(x861),f10(a27,a27))
% 0.11/0.53 [87]P10(f33(x871),f10(a27,a27))
% 0.11/0.53 [93]P10(f38(x931),f10(f10(a27,a27),a27))
% 0.11/0.53 [94]P10(f17(x941),f10(f10(a27,a27),a27))
% 0.11/0.53 [97]E(f8(f15(x971),f7(f15(f8(f12(f15(f17(f10(a9,a27))),x971),a16)))),f5(x971))
% 0.11/0.53 [101]E(f18(f23(f8(x1011,f10(f15(f15(f17(f10(f8(f15(f17(f10(x1011,a27))),f10(f43(f18(f23(f12(x1011,f15(f17(f10(x1011,a27)))),a16)),f18(f23(f12(x1011,f15(f17(f10(x1011,a27)))),a16))),a27)),a27)))),f43(f39(f23(f12(x1011,f15(f17(f10(x1011,a27)))),a16)),f39(f23(f12(x1011,f15(f17(f10(x1011,a27)))),a16))))),a22)),f40(x1011))
% 0.11/0.53 [85]P7(f43(x851,x852),a27)
% 0.11/0.53 [88]P10(f12(x881,x882),f10(a27,a27))
% 0.11/0.53 [100]E(f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(f34(x1001,a31,a42),f10(f43(x1002,x1002),a27)),a27))))))),f30(x1001,x1002))
% 0.11/0.53 [99]E(f34(a22,f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(a4,f10(f43(x991,x991),a27)),a27))))))),a42),f29(x991,x992))
% 0.11/0.53 [92]E(f8(f10(x921,x922),x923),f8(x923,f10(x921,x922)))
% 0.11/0.53 [104]~P11(x1041)+P2(x1041)
% 0.11/0.53 [105]~P12(x1051)+P2(x1051)
% 0.11/0.53 [109]~P1(x1091)+P10(a1,x1091)
% 0.11/0.53 [110]~P1(x1101)+P7(a22,x1101)
% 0.11/0.53 [114]~P7(x1141,a28)+P15(a9,x1141)
% 0.11/0.53 [106]P7(x1061,a1)+E(f19(x1061),a22)
% 0.11/0.53 [112]P7(f36(x1121),x1121)+E(x1121,a22)
% 0.11/0.53 [113]~P7(x1131,a1)+E(f19(x1131),x1131)
% 0.11/0.53 [118]~P2(x1181)+P10(x1181,f10(a27,a27))
% 0.11/0.53 [111]E(x1111,a22)+E(f8(x1111,f36(x1111)),a22)
% 0.11/0.53 [129]~P12(x1291)+E(f10(f15(f15(x1291)),f15(f15(x1291))),f15(x1291))
% 0.11/0.53 [147]~P11(x1471)+P2(f15(f17(f10(x1471,a27))))
% 0.11/0.53 [152]~P7(x1521,a27)+P7(f15(f8(a9,f10(a27,x1521))),a27)
% 0.11/0.53 [153]~P7(x1531,a28)+P10(f15(f8(a9,f10(a27,x1531))),x1531)
% 0.11/0.53 [156]~P14(x1561)+P10(f12(x1561,f15(f17(f10(x1561,a27)))),a16)
% 0.11/0.53 [157]~P2(x1571)+P10(f12(x1571,f15(f17(f10(x1571,a27)))),a16)
% 0.11/0.53 [158]~P12(x1581)+P10(f15(f15(f17(f10(x1581,a27)))),f15(f15(x1581)))
% 0.11/0.53 [168]~P7(x1681,a27)+P7(f43(f43(x1681,x1681),f43(x1681,f43(f15(x1681),f15(x1681)))),a14)
% 0.11/0.53 [169]~P7(x1691,a27)+P7(f43(f43(x1691,x1691),f43(x1691,f43(f33(x1691),f33(x1691)))),a32)
% 0.11/0.53 [173]P14(x1731)+~P10(f12(x1731,f15(f17(f10(x1731,a27)))),a16)
% 0.11/0.53 [193]~P1(x1931)+P10(f15(f15(f17(f10(f8(a31,f10(x1931,a27)),a27)))),x1931)
% 0.11/0.53 [199]~P7(x1991,a27)+P7(f7(f15(f15(f17(f10(f8(a9,f10(f7(x1991),a27)),a27))))),a27)
% 0.11/0.53 [107]~E(x1072,x1071)+P10(x1071,x1072)
% 0.11/0.53 [108]~E(x1081,x1082)+P10(x1081,x1082)
% 0.11/0.53 [117]~P15(x1171,x1172)+P3(x1171,x1172)
% 0.11/0.53 [115]P2(x1151)+~P7(x1152,f35(x1151))
% 0.11/0.53 [116]P2(x1161)+~P7(x1161,f35(x1162))
% 0.11/0.53 [120]~P7(x1201,f35(x1202))+P7(f15(x1201),a28)
% 0.11/0.53 [122]P10(x1221,x1222)+P7(f23(x1221,x1222),x1221)
% 0.11/0.53 [123]~P7(x1231,x1232)+~P7(x1231,f7(x1232))
% 0.11/0.53 [127]~P7(x1271,a27)+P7(x1271,f43(x1272,x1271))
% 0.11/0.53 [128]~P7(x1281,a27)+P7(x1281,f43(x1281,x1282))
% 0.11/0.53 [134]P10(x1341,x1342)+~P7(f23(x1341,x1342),x1342)
% 0.11/0.53 [121]~P7(x1212,f35(x1211))+E(f12(x1211,f33(x1212)),x1212)
% 0.11/0.53 [146]~P9(x1461,x1462)+P10(f8(x1461,f10(x1462,x1462)),f7(a16))
% 0.11/0.53 [150]P9(x1501,x1502)+~P10(f8(x1501,f10(x1502,x1502)),f7(a16))
% 0.11/0.53 [162]~P5(x1621,x1622)+E(f8(f8(x1621,f15(f17(f10(x1621,a27)))),f10(x1622,x1622)),a22)
% 0.11/0.53 [181]P5(x1811,x1812)+~E(f8(f8(x1811,f15(f17(f10(x1811,a27)))),f10(x1812,x1812)),a22)
% 0.11/0.53 [151]~P7(x1512,f15(x1511))+~E(f8(x1511,f10(f43(x1512,x1512),a27)),a22)
% 0.11/0.53 [170]E(f15(x1701),x1702)+~P7(f43(f43(x1701,x1701),f43(x1701,f43(x1702,x1702))),a14)
% 0.11/0.53 [171]E(f33(x1711),x1712)+~P7(f43(f43(x1711,x1711),f43(x1711,f43(x1712,x1712))),a32)
% 0.11/0.53 [172]P7(x1721,x1722)+~P7(f43(f43(x1721,x1721),f43(x1721,f43(x1722,x1722))),a9)
% 0.11/0.53 [180]~P16(x1801,x1802)+P10(f12(f8(x1801,f10(x1802,x1802)),f8(x1801,f10(x1802,x1802))),f8(x1801,f10(x1802,x1802)))
% 0.11/0.53 [188]P16(x1881,x1882)+~P10(f12(f8(x1881,f10(x1882,x1882)),f8(x1881,f10(x1882,x1882))),f8(x1881,f10(x1882,x1882)))
% 0.11/0.53 [185]~P7(f43(f43(x1851,x1851),f43(x1851,f43(x1852,x1852))),a31)+E(f7(f8(f7(x1851),f7(f43(x1851,x1851)))),x1852)
% 0.11/0.53 [194]~P7(f43(f43(x1941,x1941),f43(x1941,f43(x1942,x1942))),a42)+E(f15(f8(a9,f10(a27,f15(f15(f17(f10(x1941,a27))))))),x1942)
% 0.11/0.53 [205]~P7(f43(f43(x2051,x2051),f43(x2051,f43(x2052,x2052))),f10(a27,a27))+P7(f43(f43(x2051,x2051),f43(x2051,f43(f43(f43(x2052,x2052),f43(x2052,f43(f12(x2051,x2052),f12(x2051,x2052)))),f43(f43(x2052,x2052),f43(x2052,f43(f12(x2051,x2052),f12(x2051,x2052))))))),a13)
% 0.11/0.53 [204]~P3(x2042,x2041)+P10(f10(x2041,x2041),f7(f8(f7(a16),f7(f7(f8(f7(x2042),f7(f15(f17(f10(x2042,a27))))))))))
% 0.11/0.53 [206]P3(x2061,x2062)+~P10(f10(x2062,x2062),f7(f8(f7(a16),f7(f7(f8(f7(x2061),f7(f15(f17(f10(x2061,a27))))))))))
% 0.11/0.53 [137]P2(x1371)+~P4(x1371,x1372,x1373)
% 0.11/0.53 [138]P2(x1381)+~P8(x1381,x1382,x1383)
% 0.11/0.53 [139]P12(x1391)+~P6(x1392,x1393,x1391)
% 0.11/0.53 [140]P12(x1401)+~P6(x1402,x1401,x1403)
% 0.11/0.53 [143]P10(x1431,x1432)+~P13(x1433,x1431,x1432)
% 0.11/0.53 [149]~P6(x1491,x1492,x1493)+P4(x1491,x1492,x1493)
% 0.11/0.53 [132]P7(x1321,x1322)+~P7(x1321,f8(x1323,x1322))
% 0.11/0.53 [133]P7(x1331,x1332)+~P7(x1331,f8(x1332,x1333))
% 0.11/0.53 [141]~P8(x1411,x1412,x1413)+E(f15(x1411),x1412)
% 0.11/0.53 [144]~P4(x1442,x1441,x1443)+E(f15(f15(x1441)),f15(x1442))
% 0.11/0.53 [155]~P13(x1551,x1553,x1552)+P10(f15(f8(x1551,f10(x1552,x1553))),x1553)
% 0.11/0.53 [174]E(f12(x1741,x1742),x1743)+~P7(f43(f43(x1742,x1742),f43(x1742,f43(x1743,x1743))),f11(x1741))
% 0.11/0.53 [175]P7(x1751,f15(x1752))+~P7(f43(f43(x1751,x1751),f43(x1751,f43(x1753,x1753))),f33(x1752))
% 0.11/0.53 [176]E(f8(x1761,f10(x1762,a27)),x1763)+~P7(f43(f43(x1762,x1762),f43(x1762,f43(x1763,x1763))),f33(x1761))
% 0.11/0.53 [159]~P7(x1591,f10(x1592,x1593))+E(f43(f43(f18(x1591),f18(x1591)),f43(f18(x1591),f43(f39(x1591),f39(x1591)))),x1591)
% 0.11/0.53 [164]~P8(x1641,x1643,x1642)+P10(f15(f15(f17(f10(x1641,a27)))),x1642)
% 0.11/0.53 [165]~P4(x1651,x1653,x1652)+P10(f15(f15(f17(f10(x1651,a27)))),f15(f15(x1652)))
% 0.11/0.53 [200]E(f12(x2001,x2002),x2003)+~P7(f43(f43(x2001,x2001),f43(x2001,f43(f43(f43(x2002,x2002),f43(x2002,f43(x2003,x2003))),f43(f43(x2002,x2002),f43(x2002,f43(x2003,x2003)))))),a13)
% 0.11/0.53 [201]P7(x2011,f15(x2012))+~P7(f43(f43(x2012,x2012),f43(x2012,f43(f43(f43(x2011,x2011),f43(x2011,f43(x2013,x2013))),f43(f43(x2011,x2011),f43(x2011,f43(x2013,x2013)))))),a3)
% 0.11/0.53 [209]~P7(f43(f43(x2091,x2091),f43(x2091,f43(f43(f43(x2092,x2092),f43(x2092,f43(x2093,x2093))),f43(f43(x2092,x2092),f43(x2092,f43(x2093,x2093)))))),a3)+E(f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2091,f10(f43(x2092,x2092),a27)),a27))))))),x2093)
% 0.11/0.53 [177]P7(x1771,x1772)+~P7(f43(f43(x1773,x1773),f43(x1773,f43(x1771,x1771))),f10(x1774,x1772))
% 0.11/0.53 [178]P7(x1781,x1782)+~P7(f43(f43(x1781,x1781),f43(x1781,f43(x1783,x1783))),f10(x1782,x1784))
% 0.11/0.53 [202]~P7(f43(f43(f43(f43(x2023,x2023),f43(x2023,f43(x2021,x2021))),f43(f43(x2023,x2023),f43(x2023,f43(x2021,x2021)))),f43(f43(f43(x2023,x2023),f43(x2023,f43(x2021,x2021))),f43(x2022,x2022))),f38(x2024))+P7(f43(f43(f43(f43(x2021,x2021),f43(x2021,f43(x2022,x2022))),f43(f43(x2021,x2021),f43(x2021,f43(x2022,x2022)))),f43(f43(f43(x2021,x2021),f43(x2021,f43(x2022,x2022))),f43(x2023,x2023))),x2024)
% 0.11/0.53 [203]~P7(f43(f43(f43(f43(x2032,x2032),f43(x2032,f43(x2031,x2031))),f43(f43(x2032,x2032),f43(x2032,f43(x2031,x2031)))),f43(f43(f43(x2032,x2032),f43(x2032,f43(x2031,x2031))),f43(x2033,x2033))),f17(x2034))+P7(f43(f43(f43(f43(x2031,x2031),f43(x2031,f43(x2032,x2032))),f43(f43(x2031,x2031),f43(x2031,f43(x2032,x2032)))),f43(f43(f43(x2031,x2031),f43(x2031,f43(x2032,x2032))),f43(x2033,x2033))),x2034)
% 0.11/0.53 [211]~P7(f43(f43(x2114,x2114),f43(x2114,f43(x2111,x2111))),f12(x2112,x2113))+P7(x2111,f15(f15(f17(f10(f8(x2112,f10(f15(f15(f17(f10(f8(x2113,f10(f43(x2114,x2114),a27)),a27)))),a27)),a27)))))
% 0.11/0.53 [154]~P2(x1541)+P11(x1541)+~P2(f15(f17(f10(x1541,a27))))
% 0.11/0.53 [182]P2(x1821)+~P10(x1821,f10(a27,a27))+~P10(f12(x1821,f15(f17(f10(x1821,a27)))),a16)
% 0.11/0.53 [196]P1(x1961)+~P7(a22,x1961)+~P10(f15(f15(f17(f10(f8(a31,f10(x1961,a27)),a27)))),x1961)
% 0.11/0.53 [210]~P7(x2101,a27)+E(x2101,a22)+P7(f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(a2,f10(f43(x2101,x2101),a27)),a27))))))),x2101)
% 0.11/0.53 [119]~P10(x1192,x1191)+~P10(x1191,x1192)+E(x1191,x1192)
% 0.11/0.53 [124]P7(x1241,x1242)+P7(x1241,f7(x1242))+~P7(x1241,a27)
% 0.11/0.53 [125]~P3(x1251,x1252)+P15(x1251,x1252)+~E(f26(x1251,x1252),a22)
% 0.11/0.53 [131]~P3(x1311,x1312)+P15(x1311,x1312)+P10(f26(x1311,x1312),x1312)
% 0.11/0.53 [148]P7(x1482,f15(x1481))+~P7(x1482,a27)+E(f8(x1481,f10(f43(x1482,x1482),a27)),a22)
% 0.11/0.53 [189]~P7(x1891,x1892)+~P7(f43(f43(x1891,x1891),f43(x1891,f43(x1892,x1892))),f10(a27,a27))+P7(f43(f43(x1891,x1891),f43(x1891,f43(x1892,x1892))),a9)
% 0.11/0.53 [179]~P2(x1791)+P8(x1791,f15(x1791),x1792)+~P10(f15(f15(f17(f10(x1791,a27)))),x1792)
% 0.11/0.53 [191]~P7(f43(f43(x1911,x1911),f43(x1911,f43(x1912,x1912))),f10(a27,a27))+~E(f7(f8(f7(x1911),f7(f43(x1911,x1911)))),x1912)+P7(f43(f43(x1911,x1911),f43(x1911,f43(x1912,x1912))),a31)
% 0.11/0.53 [195]~P2(x1951)+~P7(x1952,a27)+P7(f15(f15(f17(f10(f8(x1951,f10(x1952,a27)),a27)))),a27)
% 0.11/0.53 [197]~P7(f43(f43(x1971,x1971),f43(x1971,f43(x1972,x1972))),f10(a27,a27))+P7(f43(f43(x1971,x1971),f43(x1971,f43(x1972,x1972))),a42)+~E(f15(f8(a9,f10(a27,f15(f15(f17(f10(x1971,a27))))))),x1972)
% 0.11/0.53 [126]~P7(x1261,x1263)+P7(x1261,x1262)+~P10(x1263,x1262)
% 0.11/0.53 [130]E(x1301,x1302)+E(x1301,x1303)+~P7(x1301,f43(x1303,x1302))
% 0.11/0.53 [135]~P7(x1351,x1353)+~P7(x1351,x1352)+P7(x1351,f8(x1352,x1353))
% 0.11/0.53 [166]~P7(x1661,f15(x1663))+~E(f8(x1663,f10(x1661,a27)),x1662)+P7(f43(f43(x1661,x1661),f43(x1661,f43(x1662,x1662))),f33(x1663))
% 0.11/0.53 [167]~P10(x1672,x1673)+P13(x1671,x1672,x1673)+~P10(f15(f8(x1671,f10(x1673,x1672))),x1672)
% 0.11/0.53 [190]~E(f12(x1903,x1901),x1902)+P7(f43(f43(x1901,x1901),f43(x1901,f43(x1902,x1902))),f11(x1903))+~P7(f43(f43(x1901,x1901),f43(x1901,f43(x1902,x1902))),f10(a27,a27))
% 0.11/0.53 [187]~P15(x1871,x1873)+~P10(x1872,x1873)+E(f15(f8(x1871,f10(x1872,f43(f21(x1871,x1872),f21(x1871,x1872))))),a22)
% 0.11/0.53 [213]~P7(x2132,f15(x2131))+~P7(f43(f43(x2131,x2131),f43(x2131,f43(f43(f43(x2132,x2132),f43(x2132,f43(x2133,x2133))),f43(f43(x2132,x2132),f43(x2132,f43(x2133,x2133)))))),f10(a27,f10(a27,a27)))+P7(f43(f43(x2131,x2131),f43(x2131,f43(f43(f43(x2132,x2132),f43(x2132,f43(f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2131,f10(f43(x2132,x2132),a27)),a27))))))),f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2131,f10(f43(x2132,x2132),a27)),a27)))))))))),f43(f43(x2132,x2132),f43(x2132,f43(f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2131,f10(f43(x2132,x2132),a27)),a27))))))),f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2131,f10(f43(x2132,x2132),a27)),a27))))))))))))),a3)
% 0.11/0.53 [163]~P7(x1632,x1634)+~P7(x1631,x1633)+P7(f43(f43(x1631,x1631),f43(x1631,f43(x1632,x1632))),f10(x1633,x1634))
% 0.11/0.53 [207]~P7(f43(f43(f43(f43(x2072,x2072),f43(x2072,f43(x2073,x2073))),f43(f43(x2072,x2072),f43(x2072,f43(x2073,x2073)))),f43(f43(f43(x2072,x2072),f43(x2072,f43(x2073,x2073))),f43(x2071,x2071))),x2074)+P7(f43(f43(f43(f43(x2071,x2071),f43(x2071,f43(x2072,x2072))),f43(f43(x2071,x2071),f43(x2071,f43(x2072,x2072)))),f43(f43(f43(x2071,x2071),f43(x2071,f43(x2072,x2072))),f43(x2073,x2073))),f38(x2074))+~P7(f43(f43(f43(f43(x2071,x2071),f43(x2071,f43(x2072,x2072))),f43(f43(x2071,x2071),f43(x2071,f43(x2072,x2072)))),f43(f43(f43(x2071,x2071),f43(x2071,f43(x2072,x2072))),f43(x2073,x2073))),f10(f10(a27,a27),a27))
% 0.11/0.53 [208]~P7(f43(f43(f43(f43(x2082,x2082),f43(x2082,f43(x2081,x2081))),f43(f43(x2082,x2082),f43(x2082,f43(x2081,x2081)))),f43(f43(f43(x2082,x2082),f43(x2082,f43(x2081,x2081))),f43(x2083,x2083))),x2084)+P7(f43(f43(f43(f43(x2081,x2081),f43(x2081,f43(x2082,x2082))),f43(f43(x2081,x2081),f43(x2081,f43(x2082,x2082)))),f43(f43(f43(x2081,x2081),f43(x2081,f43(x2082,x2082))),f43(x2083,x2083))),f17(x2084))+~P7(f43(f43(f43(f43(x2081,x2081),f43(x2081,f43(x2082,x2082))),f43(f43(x2081,x2081),f43(x2081,f43(x2082,x2082)))),f43(f43(f43(x2081,x2081),f43(x2081,f43(x2082,x2082))),f43(x2083,x2083))),f10(f10(a27,a27),a27))
% 0.11/0.53 [212]~P7(f43(f43(x2121,x2121),f43(x2121,f43(x2122,x2122))),f10(a27,a27))+P7(f43(f43(x2121,x2121),f43(x2121,f43(x2122,x2122))),f12(x2123,x2124))+~P7(x2122,f15(f15(f17(f10(f8(x2123,f10(f15(f15(f17(f10(f8(x2124,f10(f43(x2121,x2121),a27)),a27)))),a27)),a27)))))
% 0.11/0.53 [214]~P6(x2142,x2145,x2141)+~P7(f43(f43(x2143,x2143),f43(x2143,f43(x2144,x2144))),f15(x2145))+E(f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2141,f10(f43(f43(f43(f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2142,f10(f43(x2143,x2143),a27)),a27))))))),f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2142,f10(f43(x2143,x2143),a27)),a27)))))))),f43(f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2142,f10(f43(x2143,x2143),a27)),a27))))))),f43(f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2142,f10(f43(x2144,x2144),a27)),a27))))))),f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2142,f10(f43(x2144,x2144),a27)),a27)))))))))),f43(f43(f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2142,f10(f43(x2143,x2143),a27)),a27))))))),f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2142,f10(f43(x2143,x2143),a27)),a27)))))))),f43(f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2142,f10(f43(x2143,x2143),a27)),a27))))))),f43(f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2142,f10(f43(x2144,x2144),a27)),a27))))))),f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2142,f10(f43(x2144,x2144),a27)),a27))))))))))),a27)),a27))))))),f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2142,f10(f43(f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2145,f10(f43(f43(f43(x2143,x2143),f43(x2143,f43(x2144,x2144))),f43(f43(x2143,x2143),f43(x2143,f43(x2144,x2144)))),a27)),a27))))))),f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2145,f10(f43(f43(f43(x2143,x2143),f43(x2143,f43(x2144,x2144))),f43(f43(x2143,x2143),f43(x2143,f43(x2144,x2144)))),a27)),a27)))))))),a27)),a27))))))))
% 0.11/0.53 [160]P7(x1601,a28)+~P15(a9,x1601)+E(x1601,a28)+~P10(f15(f8(a9,f10(a27,x1601))),x1601)
% 0.11/0.53 [161]~P7(x1611,a27)+~P15(a9,x1611)+P7(x1611,a28)+~P10(f15(f8(a9,f10(a27,x1611))),x1611)
% 0.11/0.53 [184]~P2(x1841)+P12(x1841)+~E(f10(f15(f15(x1841)),f15(f15(x1841))),f15(x1841))+~P10(f15(f15(f17(f10(x1841,a27)))),f15(f15(x1841)))
% 0.11/0.53 [136]~P15(x1362,x1363)+~P10(x1361,x1363)+P7(f21(x1362,x1361),x1361)+E(x1361,a22)
% 0.11/0.53 [183]~P2(x1831)+P4(x1831,x1832,x1833)+~E(f15(f15(x1832)),f15(x1831))+~P10(f15(f15(f17(f10(x1831,a27)))),f15(f15(x1833)))
% 0.11/0.53 [186]~P3(x1861,x1862)+P15(x1861,x1862)+~P7(x1863,f26(x1861,x1862))+~E(f15(f8(x1861,f10(f26(x1861,x1862),f43(x1863,x1863)))),a22)
% 0.11/0.53 [145]~P15(x1451,x1453)+~P10(x1452,x1453)+~P7(x1454,x1452)+P7(f21(x1451,x1452),x1452)
% 0.11/0.53 [192]~P10(x1921,x1922)+~P7(x1923,x1921)+~P15(x1924,x1922)+~P7(f43(f43(x1923,x1923),f43(x1923,f43(f21(x1924,x1921),f21(x1924,x1921)))),x1924)
% 0.11/0.53 [142]~P2(x1421)+~P2(x1422)+P7(x1421,f35(x1422))+~E(f12(x1422,f33(x1421)),x1421)+~P7(f15(x1421),a28)
% 0.11/0.53 [198]~P12(x1983)+~P12(x1982)+~P4(x1981,x1982,x1983)+P6(x1981,x1982,x1983)+P7(f43(f43(f24(x1981,x1982,x1983),f24(x1981,x1982,x1983)),f43(f24(x1981,x1982,x1983),f43(f25(x1981,x1982,x1983),f25(x1981,x1982,x1983)))),f15(x1982))
% 0.11/0.53 [215]~P12(x2153)+~P12(x2152)+~P4(x2151,x2152,x2153)+P6(x2151,x2152,x2153)+~E(f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2153,f10(f43(f43(f43(f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2151,f10(f43(f24(x2151,x2152,x2153),f24(x2151,x2152,x2153)),a27)),a27))))))),f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2151,f10(f43(f24(x2151,x2152,x2153),f24(x2151,x2152,x2153)),a27)),a27)))))))),f43(f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2151,f10(f43(f24(x2151,x2152,x2153),f24(x2151,x2152,x2153)),a27)),a27))))))),f43(f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2151,f10(f43(f25(x2151,x2152,x2153),f25(x2151,x2152,x2153)),a27)),a27))))))),f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2151,f10(f43(f25(x2151,x2152,x2153),f25(x2151,x2152,x2153)),a27)),a27)))))))))),f43(f43(f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2151,f10(f43(f24(x2151,x2152,x2153),f24(x2151,x2152,x2153)),a27)),a27))))))),f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2151,f10(f43(f24(x2151,x2152,x2153),f24(x2151,x2152,x2153)),a27)),a27)))))))),f43(f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2151,f10(f43(f24(x2151,x2152,x2153),f24(x2151,x2152,x2153)),a27)),a27))))))),f43(f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2151,f10(f43(f25(x2151,x2152,x2153),f25(x2151,x2152,x2153)),a27)),a27))))))),f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2151,f10(f43(f25(x2151,x2152,x2153),f25(x2151,x2152,x2153)),a27)),a27))))))))))),a27)),a27))))))),f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2151,f10(f43(f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2152,f10(f43(f43(f43(f24(x2151,x2152,x2153),f24(x2151,x2152,x2153)),f43(f24(x2151,x2152,x2153),f43(f25(x2151,x2152,x2153),f25(x2151,x2152,x2153)))),f43(f43(f24(x2151,x2152,x2153),f24(x2151,x2152,x2153)),f43(f24(x2151,x2152,x2153),f43(f25(x2151,x2152,x2153),f25(x2151,x2152,x2153))))),a27)),a27))))))),f15(f8(a9,f10(a27,f15(f15(f17(f10(f8(x2152,f10(f43(f43(f43(f24(x2151,x2152,x2153),f24(x2151,x2152,x2153)),f43(f24(x2151,x2152,x2153),f43(f25(x2151,x2152,x2153),f25(x2151,x2152,x2153)))),f43(f43(f24(x2151,x2152,x2153),f24(x2151,x2152,x2153)),f43(f24(x2151,x2152,x2153),f43(f25(x2151,x2152,x2153),f25(x2151,x2152,x2153))))),a27)),a27)))))))),a27)),a27))))))))
% 0.11/0.53 %EqnAxiom
% 0.11/0.53 [1]E(x11,x11)
% 0.11/0.53 [2]E(x22,x21)+~E(x21,x22)
% 0.11/0.53 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.11/0.53 [4]~E(x41,x42)+E(f7(x41),f7(x42))
% 0.11/0.53 [5]~E(x51,x52)+E(f8(x51,x53),f8(x52,x53))
% 0.11/0.53 [6]~E(x61,x62)+E(f8(x63,x61),f8(x63,x62))
% 0.11/0.53 [7]~E(x71,x72)+E(f10(x71,x73),f10(x72,x73))
% 0.11/0.53 [8]~E(x81,x82)+E(f10(x83,x81),f10(x83,x82))
% 0.11/0.53 [9]~E(x91,x92)+E(f17(x91),f17(x92))
% 0.11/0.53 [10]~E(x101,x102)+E(f15(x101),f15(x102))
% 0.11/0.53 [11]~E(x111,x112)+E(f43(x111,x113),f43(x112,x113))
% 0.11/0.53 [12]~E(x121,x122)+E(f43(x123,x121),f43(x123,x122))
% 0.11/0.53 [13]~E(x131,x132)+E(f25(x131,x133,x134),f25(x132,x133,x134))
% 0.11/0.53 [14]~E(x141,x142)+E(f25(x143,x141,x144),f25(x143,x142,x144))
% 0.11/0.53 [15]~E(x151,x152)+E(f25(x153,x154,x151),f25(x153,x154,x152))
% 0.46/0.53 [16]~E(x161,x162)+E(f38(x161),f38(x162))
% 0.46/0.53 [17]~E(x171,x172)+E(f11(x171),f11(x172))
% 0.46/0.53 [18]~E(x181,x182)+E(f36(x181),f36(x182))
% 0.46/0.53 [19]~E(x191,x192)+E(f33(x191),f33(x192))
% 0.46/0.53 [20]~E(x201,x202)+E(f12(x201,x203),f12(x202,x203))
% 0.46/0.53 [21]~E(x211,x212)+E(f12(x213,x211),f12(x213,x212))
% 0.46/0.53 [22]~E(x221,x222)+E(f24(x221,x223,x224),f24(x222,x223,x224))
% 0.46/0.53 [23]~E(x231,x232)+E(f24(x233,x231,x234),f24(x233,x232,x234))
% 0.46/0.53 [24]~E(x241,x242)+E(f24(x243,x244,x241),f24(x243,x244,x242))
% 0.46/0.53 [25]~E(x251,x252)+E(f19(x251),f19(x252))
% 0.46/0.53 [26]~E(x261,x262)+E(f35(x261),f35(x262))
% 0.46/0.53 [27]~E(x271,x272)+E(f34(x271,x273,x274),f34(x272,x273,x274))
% 0.46/0.53 [28]~E(x281,x282)+E(f34(x283,x281,x284),f34(x283,x282,x284))
% 0.46/0.53 [29]~E(x291,x292)+E(f34(x293,x294,x291),f34(x293,x294,x292))
% 0.46/0.53 [30]~E(x301,x302)+E(f29(x301,x303),f29(x302,x303))
% 0.46/0.53 [31]~E(x311,x312)+E(f29(x313,x311),f29(x313,x312))
% 0.46/0.53 [32]~E(x321,x322)+E(f21(x321,x323),f21(x322,x323))
% 0.46/0.53 [33]~E(x331,x332)+E(f21(x333,x331),f21(x333,x332))
% 0.46/0.53 [34]~E(x341,x342)+E(f23(x341,x343),f23(x342,x343))
% 0.46/0.53 [35]~E(x351,x352)+E(f23(x353,x351),f23(x353,x352))
% 0.46/0.53 [36]~E(x361,x362)+E(f26(x361,x363),f26(x362,x363))
% 0.46/0.53 [37]~E(x371,x372)+E(f26(x373,x371),f26(x373,x372))
% 0.46/0.53 [38]~E(x381,x382)+E(f40(x381),f40(x382))
% 0.46/0.53 [39]~E(x391,x392)+E(f18(x391),f18(x392))
% 0.46/0.53 [40]~E(x401,x402)+E(f39(x401),f39(x402))
% 0.46/0.53 [41]~E(x411,x412)+E(f30(x411,x413),f30(x412,x413))
% 0.46/0.53 [42]~E(x421,x422)+E(f30(x423,x421),f30(x423,x422))
% 0.46/0.54 [43]~E(x431,x432)+E(f5(x431),f5(x432))
% 0.46/0.54 [44]~P1(x441)+P1(x442)+~E(x441,x442)
% 0.46/0.54 [45]~P2(x451)+P2(x452)+~E(x451,x452)
% 0.46/0.54 [46]P7(x462,x463)+~E(x461,x462)+~P7(x461,x463)
% 0.46/0.54 [47]P7(x473,x472)+~E(x471,x472)+~P7(x473,x471)
% 0.46/0.54 [48]P10(x482,x483)+~E(x481,x482)+~P10(x481,x483)
% 0.46/0.54 [49]P10(x493,x492)+~E(x491,x492)+~P10(x493,x491)
% 0.46/0.54 [50]~P11(x501)+P11(x502)+~E(x501,x502)
% 0.46/0.54 [51]P13(x512,x513,x514)+~E(x511,x512)+~P13(x511,x513,x514)
% 0.46/0.54 [52]P13(x523,x522,x524)+~E(x521,x522)+~P13(x523,x521,x524)
% 0.46/0.54 [53]P13(x533,x534,x532)+~E(x531,x532)+~P13(x533,x534,x531)
% 0.46/0.54 [54]P9(x542,x543)+~E(x541,x542)+~P9(x541,x543)
% 0.46/0.54 [55]P9(x553,x552)+~E(x551,x552)+~P9(x553,x551)
% 0.46/0.54 [56]P6(x562,x563,x564)+~E(x561,x562)+~P6(x561,x563,x564)
% 0.46/0.54 [57]P6(x573,x572,x574)+~E(x571,x572)+~P6(x573,x571,x574)
% 0.46/0.54 [58]P6(x583,x584,x582)+~E(x581,x582)+~P6(x583,x584,x581)
% 0.46/0.54 [59]P4(x592,x593,x594)+~E(x591,x592)+~P4(x591,x593,x594)
% 0.46/0.54 [60]P4(x603,x602,x604)+~E(x601,x602)+~P4(x603,x601,x604)
% 0.46/0.54 [61]P4(x613,x614,x612)+~E(x611,x612)+~P4(x613,x614,x611)
% 0.46/0.54 [62]~P14(x621)+P14(x622)+~E(x621,x622)
% 0.46/0.54 [63]P16(x632,x633)+~E(x631,x632)+~P16(x631,x633)
% 0.46/0.54 [64]P16(x643,x642)+~E(x641,x642)+~P16(x643,x641)
% 0.46/0.54 [65]P15(x652,x653)+~E(x651,x652)+~P15(x651,x653)
% 0.46/0.54 [66]P15(x663,x662)+~E(x661,x662)+~P15(x663,x661)
% 0.46/0.54 [67]P8(x672,x673,x674)+~E(x671,x672)+~P8(x671,x673,x674)
% 0.46/0.54 [68]P8(x683,x682,x684)+~E(x681,x682)+~P8(x683,x681,x684)
% 0.46/0.54 [69]P8(x693,x694,x692)+~E(x691,x692)+~P8(x693,x694,x691)
% 0.46/0.54 [70]~P12(x701)+P12(x702)+~E(x701,x702)
% 0.46/0.54 [71]P3(x712,x713)+~E(x711,x712)+~P3(x711,x713)
% 0.46/0.54 [72]P3(x723,x722)+~E(x721,x722)+~P3(x723,x721)
% 0.46/0.54 [73]P5(x732,x733)+~E(x731,x732)+~P5(x731,x733)
% 0.46/0.54 [74]P5(x743,x742)+~E(x741,x742)+~P5(x743,x741)
% 0.46/0.54
% 0.46/0.54 %-------------------------------------------
% 0.46/0.54 cnf(229,plain,
% 0.46/0.54 ($false),
% 0.46/0.54 inference(scs_inference,[],[102,103,112,104,105,115]),
% 0.46/0.54 ['proof']).
% 0.46/0.54 % SZS output end Proof
% 0.46/0.54 % Total time :0.010000s
%------------------------------------------------------------------------------