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