%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET024-3 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/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 14:20:07 EDT 2024
% Result : Unsatisfiable 0.58s 0.69s
% Output : CNFRefutation 0.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SET024-3 : TPTP v8.2.0. Released v1.0.0.
% 0.07/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.35 % Computer : n020.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Sun Jun 23 15:48:24 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.21/0.59 start to proof:theBenchmark
% 0.58/0.69 %-------------------------------------------
% 0.58/0.69 % File :CSE---1.7
% 0.58/0.69 % Problem :theBenchmark
% 0.58/0.69 % Transform :cnf
% 0.58/0.69 % Format :tptp:raw
% 0.58/0.69 % Command :java -jar mcs_scs.jar %d %s
% 0.58/0.69
% 0.58/0.69 % Result :Theorem 0.020000s
% 0.58/0.69 % Output :CNFRefutation 0.020000s
% 0.58/0.69 %-------------------------------------------
% 0.58/0.69 %--------------------------------------------------------------------------
% 0.58/0.69 % File : SET024-3 : TPTP v8.2.0. Released v1.0.0.
% 0.58/0.69 % Domain : Set Theory
% 0.58/0.69 % Problem : A set belongs to its singleton
% 0.58/0.69 % Version : [BL+86] axioms : Augmented.
% 0.58/0.69 % English :
% 0.58/0.69
% 0.58/0.69 % Refs : [BL+86] Boyer et al. (1986), Set Theory in First-Order Logic:
% 0.58/0.69 % Source : [BL+86]
% 0.58/0.69 % Names : Lemma 9 [BL+86]
% 0.58/0.69
% 0.58/0.69 % Status : Unsatisfiable
% 0.58/0.69 % Rating : 0.10 v8.2.0, 0.05 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.08 v7.2.0, 0.17 v7.1.0, 0.00 v7.0.0, 0.20 v6.3.0, 0.18 v6.2.0, 0.10 v6.1.0, 0.14 v6.0.0, 0.00 v5.5.0, 0.10 v5.3.0, 0.17 v5.2.0, 0.19 v5.1.0, 0.24 v5.0.0, 0.07 v4.1.0, 0.00 v4.0.1, 0.09 v4.0.0, 0.00 v3.3.0, 0.07 v3.2.0, 0.08 v3.1.0, 0.18 v2.7.0, 0.08 v2.6.0, 0.00 v2.5.0, 0.17 v2.4.0, 0.00 v2.2.1, 0.22 v2.2.0, 0.33 v2.1.0, 0.33 v2.0.0
% 0.58/0.69 % Syntax : Number of clauses : 151 ( 13 unt; 20 nHn; 128 RR)
% 0.58/0.69 % Number of literals : 384 ( 56 equ; 217 neg)
% 0.58/0.69 % Maximal clause size : 8 ( 2 avg)
% 0.58/0.69 % Maximal term depth : 4 ( 1 avg)
% 0.58/0.69 % Number of predicates : 14 ( 13 usr; 0 prp; 1-5 aty)
% 0.58/0.69 % Number of functors : 60 ( 60 usr; 7 con; 0-5 aty)
% 0.58/0.69 % Number of variables : 339 ( 30 sgn)
% 0.58/0.69 % SPC : CNF_UNS_RFO_SEQ_NHN
% 0.58/0.69
% 0.58/0.69 % Comments :
% 0.58/0.69 %--------------------------------------------------------------------------
% 0.58/0.69 %----Include Godel's set axioms
% 0.58/0.69 include('Axioms/SET003-0.ax').
% 0.58/0.69 %--------------------------------------------------------------------------
% 0.58/0.69 %----Previously proved lemmas are added at each step
% 0.58/0.69 cnf(first_components_are_equal,axiom,
% 0.58/0.69 ( ~ little_set(X)
% 0.58/0.69 | ~ little_set(U)
% 0.58/0.69 | ordered_pair(X,Y) != ordered_pair(U,V)
% 0.58/0.69 | X = U ) ).
% 0.58/0.69
% 0.58/0.69 cnf(left_cancellation,axiom,
% 0.58/0.69 ( ~ little_set(X)
% 0.58/0.69 | ~ little_set(Y)
% 0.58/0.69 | non_ordered_pair(Z,X) != non_ordered_pair(Z,Y)
% 0.58/0.69 | X = Y ) ).
% 0.58/0.69
% 0.58/0.69 cnf(second_components_are_equal,axiom,
% 0.58/0.69 ( ~ little_set(X)
% 0.58/0.69 | ~ little_set(Y)
% 0.58/0.69 | ~ little_set(U)
% 0.58/0.69 | ~ little_set(V)
% 0.58/0.69 | ordered_pair(X,Y) != ordered_pair(U,V)
% 0.58/0.69 | Y = V ) ).
% 0.58/0.69
% 0.58/0.69 cnf(two_sets_equal,axiom,
% 0.58/0.69 ( ~ subset(X,Y)
% 0.58/0.69 | ~ subset(Y,X)
% 0.58/0.69 | X = Y ) ).
% 0.58/0.69
% 0.58/0.69 cnf(property_of_first,axiom,
% 0.58/0.69 ( ~ little_set(X)
% 0.58/0.69 | ~ little_set(Y)
% 0.58/0.69 | first(ordered_pair(X,Y)) = X ) ).
% 0.58/0.69
% 0.58/0.69 cnf(property_of_second,axiom,
% 0.58/0.69 ( ~ little_set(X)
% 0.58/0.69 | ~ little_set(Y)
% 0.58/0.69 | second(ordered_pair(X,Y)) = Y ) ).
% 0.58/0.69
% 0.58/0.69 cnf(first_component_is_small,axiom,
% 0.58/0.69 ( ~ ordered_pair_predicate(X)
% 0.58/0.69 | little_set(first(X)) ) ).
% 0.58/0.69
% 0.58/0.69 cnf(second_component_is_small,axiom,
% 0.58/0.69 ( ~ ordered_pair_predicate(X)
% 0.58/0.69 | little_set(second(X)) ) ).
% 0.58/0.69
% 0.58/0.69 cnf(a_little_set,hypothesis,
% 0.58/0.69 little_set(a) ).
% 0.58/0.69
% 0.58/0.69 cnf(prove_membership_of_singleton_set,negated_conjecture,
% 0.58/0.69 ~ member(a,singleton_set(a)) ).
% 0.58/0.69
% 0.58/0.69 %--------------------------------------------------------------------------
% 0.58/0.69 %-------------------------------------------
% 0.58/0.69 % Proof found
% 0.58/0.69 % SZS status Theorem for theBenchmark
% 0.58/0.69 % SZS output start Proof
% 0.58/0.70 %ClaNum:259(EqnAxiom:114)
% 0.58/0.70 %VarNum:966(SingletonVarNum:328)
% 0.58/0.70 %MaxLitNum:8
% 0.58/0.70 %MaxfuncDepth:5
% 0.58/0.70 %SharedTerms:13
% 0.58/0.70 %goalClause: 121
% 0.58/0.70 %singleGoalClaCount:1
% 0.58/0.70 [115]P1(a1)
% 0.58/0.70 [116]P1(a2)
% 0.58/0.70 [117]P2(a3)
% 0.58/0.70 [118]P6(a4,a1)
% 0.58/0.70 [121]~P6(a2,f47(a2,a2))
% 0.58/0.70 [120]~P6(x1201,a4)
% 0.58/0.70 [119]P1(f47(x1191,x1192))
% 0.58/0.70 [122]~P2(x1221)+P8(x1221)
% 0.58/0.70 [123]~P2(x1231)+P12(x1231)
% 0.58/0.70 [124]~P9(x1241)+P2(x1241)
% 0.58/0.70 [137]~P1(x1371)+P6(x1371,a54)
% 0.58/0.70 [141]P10(x1411)+~P6(x1411,a13)
% 0.58/0.70 [142]P10(x1421)+~P6(x1421,a44)
% 0.58/0.70 [125]P12(x1251)+P1(f11(x1251))
% 0.58/0.70 [126]P12(x1261)+P1(f22(x1261))
% 0.58/0.70 [127]P12(x1271)+P1(f24(x1271))
% 0.58/0.70 [128]P12(x1281)+~E(f24(x1281),f22(x1281))
% 0.58/0.70 [129]~P10(x1291)+P1(f23(x1291))
% 0.58/0.70 [130]~P10(x1301)+P1(f28(x1301))
% 0.58/0.70 [131]~P10(x1311)+P1(f33(x1311))
% 0.58/0.70 [132]~P10(x1321)+P1(f49(x1321))
% 0.58/0.70 [133]~P1(x1331)+P1(f53(x1331))
% 0.58/0.70 [134]~P1(x1341)+P1(f50(x1341))
% 0.58/0.70 [135]~P9(x1351)+P2(f5(x1351))
% 0.58/0.70 [138]P8(x1381)+~P10(f12(x1381))
% 0.58/0.70 [139]P6(f25(x1391),x1391)+E(x1391,a4)
% 0.58/0.70 [140]P3(f25(x1401),x1401)+E(x1401,a4)
% 0.58/0.70 [143]P8(x1431)+P6(f12(x1431),x1431)
% 0.58/0.70 [149]~P6(x1491,a44)+E(f49(x1491),f33(x1491))
% 0.58/0.70 [160]~P6(x1601,a13)+P6(f33(x1601),f49(x1601))
% 0.58/0.70 [213]~P10(x2131)+E(f47(f47(f23(x2131),f23(x2131)),f47(f23(x2131),f28(x2131))),x2131)
% 0.58/0.70 [233]P12(x2331)+P6(f47(f47(f11(x2331),f11(x2331)),f47(f11(x2331),f22(x2331))),x2331)
% 0.58/0.70 [234]P12(x2341)+P6(f47(f47(f11(x2341),f11(x2341)),f47(f11(x2341),f24(x2341))),x2341)
% 0.58/0.70 [240]~P6(x2401,a1)+P6(f6(f48(f6(x2401),f6(f47(x2401,x2401)))),a1)
% 0.58/0.70 [144]~P11(x1441,x1442)+~E(x1441,x1442)
% 0.58/0.70 [145]P1(x1451)+~P4(x1452,x1451)
% 0.58/0.70 [146]P1(x1461)+~P6(x1461,x1462)
% 0.58/0.70 [147]P1(x1471)+~P4(x1471,x1472)
% 0.58/0.70 [154]~P11(x1541,x1542)+P13(x1541,x1542)
% 0.58/0.70 [151]E(x1511,x1512)+P1(f14(x1511,x1512))
% 0.58/0.70 [153]P10(x1531)+~P6(x1531,f5(x1532))
% 0.58/0.70 [159]P13(x1591,x1592)+~P6(x1591,f50(x1592))
% 0.58/0.70 [165]P13(x1651,x1652)+P6(f15(x1651,x1652),x1651)
% 0.58/0.70 [166]P3(x1661,x1662)+P6(f26(x1661,x1662),x1662)
% 0.58/0.70 [167]P3(x1671,x1672)+P6(f26(x1671,x1672),x1671)
% 0.58/0.70 [168]~P6(x1681,x1682)+~P6(x1681,f6(x1682))
% 0.58/0.70 [171]~P6(x1711,f33(x1712))+P1(f34(x1711,x1712))
% 0.58/0.70 [172]~P6(x1721,f33(x1722))+P1(f39(x1721,x1722))
% 0.58/0.70 [173]~P6(x1731,f49(x1732))+P1(f40(x1731,x1732))
% 0.58/0.70 [174]~P6(x1741,f49(x1742))+P1(f41(x1741,x1742))
% 0.58/0.70 [175]~P6(x1751,f51(x1752))+P1(f42(x1751,x1752))
% 0.58/0.70 [176]~P6(x1761,f51(x1762))+P1(f16(x1761,x1762))
% 0.58/0.70 [177]~P6(x1771,f51(x1772))+P1(f17(x1771,x1772))
% 0.58/0.70 [178]~P6(x1781,f45(x1782))+P1(f18(x1781,x1782))
% 0.58/0.70 [179]~P6(x1791,f45(x1792))+P1(f19(x1791,x1792))
% 0.58/0.70 [180]~P6(x1801,f45(x1802))+P1(f20(x1801,x1802))
% 0.58/0.70 [181]~P6(x1811,f9(x1812))+P10(f43(x1811,x1812))
% 0.58/0.70 [182]~P6(x1821,f52(x1822))+P10(f30(x1821,x1822))
% 0.58/0.70 [192]~P6(x1921,f33(x1922))+P6(x1921,f34(x1921,x1922))
% 0.58/0.70 [193]~P6(x1931,f49(x1932))+P6(x1931,f41(x1931,x1932))
% 0.58/0.70 [194]~P6(x1941,f53(x1942))+P6(x1941,f21(x1941,x1942))
% 0.58/0.70 [195]~P6(x1951,f9(x1952))+P6(f43(x1951,x1952),x1952)
% 0.58/0.70 [196]~P6(x1961,f53(x1962))+P6(f21(x1961,x1962),x1962)
% 0.58/0.70 [197]~P6(x1971,f52(x1972))+P6(f30(x1971,x1972),x1972)
% 0.58/0.70 [200]P13(x2001,x2002)+~P6(f15(x2001,x2002),x2002)
% 0.58/0.70 [208]~P4(x2082,x2081)+P7(x2081,f10(x2082,x2082),x2082)
% 0.58/0.70 [183]~P6(x1831,f9(x1832))+E(f33(f43(x1831,x1832)),x1831)
% 0.58/0.70 [184]~P6(x1841,f52(x1842))+E(f49(f30(x1841,x1842)),x1841)
% 0.58/0.70 [235]~P6(x2351,f5(x2352))+P6(f47(f47(f49(x2351),f49(x2351)),f47(f49(x2351),f33(x2351))),x2352)
% 0.58/0.70 [238]~P6(x2381,f33(x2382))+E(f47(f47(f34(x2381,x2382),f34(x2381,x2382)),f47(f34(x2381,x2382),f39(x2381,x2382))),x2382)
% 0.58/0.70 [239]~P6(x2391,f49(x2392))+E(f47(f47(f40(x2391,x2392),f40(x2391,x2392)),f47(f40(x2391,x2392),f41(x2391,x2392))),x2392)
% 0.58/0.70 [245]~P6(x2451,f51(x2452))+E(f47(f47(f42(x2451,x2452),f42(x2451,x2452)),f47(f42(x2451,x2452),f47(f47(f16(x2451,x2452),f16(x2451,x2452)),f47(f16(x2451,x2452),f17(x2451,x2452))))),x2451)
% 0.58/0.70 [246]~P6(x2461,f45(x2462))+E(f47(f47(f18(x2461,x2462),f18(x2461,x2462)),f47(f18(x2461,x2462),f47(f47(f19(x2461,x2462),f19(x2461,x2462)),f47(f19(x2461,x2462),f20(x2461,x2462))))),x2461)
% 0.58/0.70 [254]~P6(x2541,f51(x2542))+P6(f47(f47(f16(x2541,x2542),f16(x2541,x2542)),f47(f16(x2541,x2542),f47(f47(f17(x2541,x2542),f17(x2541,x2542)),f47(f17(x2541,x2542),f42(x2541,x2542))))),x2542)
% 0.58/0.70 [255]~P6(x2551,f45(x2552))+P6(f47(f47(f18(x2551,x2552),f18(x2551,x2552)),f47(f18(x2551,x2552),f47(f47(f20(x2551,x2552),f20(x2551,x2552)),f47(f20(x2551,x2552),f19(x2551,x2552))))),x2552)
% 0.58/0.70 [205]P2(x2051)+~P7(x2051,x2052,x2053)
% 0.58/0.70 [188]P10(x1881)+~P6(x1881,f10(x1882,x1883))
% 0.58/0.70 [198]P6(x1981,x1982)+~P6(x1981,f48(x1983,x1982))
% 0.58/0.70 [199]P6(x1991,x1992)+~P6(x1991,f48(x1992,x1993))
% 0.58/0.70 [202]P6(f33(x2021),x2022)+~P6(x2021,f10(x2022,x2023))
% 0.58/0.70 [203]P6(f49(x2031),x2032)+~P6(x2031,f10(x2033,x2032))
% 0.58/0.70 [206]~P7(x2061,x2062,x2063)+E(f9(x2061),x2062)
% 0.58/0.70 [209]~P7(x2091,x2093,x2092)+P13(f52(x2091),x2092)
% 0.58/0.70 [221]~P6(x2211,f8(x2212,x2213))+P1(f31(x2211,x2212,x2213))
% 0.58/0.70 [222]~P6(x2221,f8(x2222,x2223))+P1(f35(x2221,x2222,x2223))
% 0.58/0.70 [223]~P6(x2231,f8(x2232,x2233))+P1(f36(x2231,x2232,x2233))
% 0.58/0.70 [224]~P6(x2241,f46(x2242,x2243))+P10(f27(x2241,x2242,x2243))
% 0.58/0.70 [225]~P6(x2251,f7(x2252,x2253))+P10(f32(x2251,x2252,x2253))
% 0.58/0.70 [229]~P6(x2291,f46(x2292,x2293))+P6(f27(x2291,x2292,x2293),x2293)
% 0.58/0.70 [230]~P6(x2301,f7(x2302,x2303))+P6(f32(x2301,x2302,x2303),x2302)
% 0.58/0.70 [226]~P6(x2261,f7(x2262,x2263))+E(f33(f32(x2261,x2262,x2263)),x2263)
% 0.58/0.70 [227]~P6(x2271,f46(x2272,x2273))+E(f49(f27(x2271,x2272,x2273)),x2271)
% 0.58/0.70 [236]~P6(x2361,f7(x2362,x2363))+P6(x2361,f49(f32(x2361,x2362,x2363)))
% 0.58/0.70 [237]~P6(x2371,f46(x2372,x2373))+P6(f33(f27(x2371,x2372,x2373)),x2372)
% 0.58/0.70 [244]~P6(x2441,f8(x2442,x2443))+E(f47(f47(f31(x2441,x2442,x2443),f31(x2441,x2442,x2443)),f47(f31(x2441,x2442,x2443),f35(x2441,x2442,x2443))),x2441)
% 0.58/0.70 [251]~P6(x2511,f8(x2512,x2513))+P6(f47(f47(f31(x2511,x2512,x2513),f31(x2511,x2512,x2513)),f47(f31(x2511,x2512,x2513),f36(x2511,x2512,x2513))),x2512)
% 0.58/0.70 [252]~P6(x2521,f8(x2522,x2523))+P6(f47(f47(f36(x2521,x2522,x2523),f36(x2521,x2522,x2523)),f47(f36(x2521,x2522,x2523),f35(x2521,x2522,x2523))),x2523)
% 0.58/0.70 [249]P4(x2491,x2492)+~P5(x2493,x2494,x2495,x2491,x2492)
% 0.58/0.70 [250]P4(x2501,x2502)+~P5(x2503,x2501,x2502,x2504,x2505)
% 0.58/0.70 [253]P7(x2531,x2532,x2533)+~P5(x2531,x2532,x2534,x2533,x2535)
% 0.58/0.70 [136]~P8(x1361)+~P12(x1361)+P2(x1361)
% 0.58/0.70 [148]~P2(x1481)+P9(x1481)+~P2(f5(x1481))
% 0.58/0.70 [150]~P1(x1501)+P6(f29(x1501),x1501)+E(x1501,a4)
% 0.58/0.70 [228]~P1(x2281)+E(x2281,a4)+P6(f47(f47(x2281,x2281),f47(x2281,f29(x2281))),a3)
% 0.58/0.70 [152]~P6(x1521,x1522)+P10(x1521)+~P8(x1522)
% 0.58/0.70 [155]P11(x1551,x1552)+~P13(x1551,x1552)+E(x1551,x1552)
% 0.58/0.70 [161]~P13(x1612,x1611)+~P13(x1611,x1612)+E(x1611,x1612)
% 0.58/0.70 [157]~P1(x1571)+P6(x1571,x1572)+P6(x1571,f6(x1572))
% 0.58/0.70 [158]~P1(x1581)+~P2(x1582)+P1(f46(x1581,x1582))
% 0.58/0.70 [162]~P1(x1621)+~P13(x1621,x1622)+P6(x1621,f50(x1622))
% 0.58/0.70 [201]E(x2011,x2012)+P6(f14(x2011,x2012),x2012)+P6(f14(x2011,x2012),x2011)
% 0.58/0.70 [215]E(x2151,x2152)+~P6(f14(x2151,x2152),x2152)+~P6(f14(x2151,x2152),x2151)
% 0.58/0.70 [216]~P1(x2162)+~P1(x2161)+E(f33(f47(f47(x2161,x2161),f47(x2161,x2162))),x2161)
% 0.58/0.70 [217]~P1(x2172)+~P1(x2171)+E(f49(f47(f47(x2171,x2171),f47(x2171,x2172))),x2172)
% 0.58/0.70 [169]~P13(x1693,x1692)+P6(x1691,x1692)+~P6(x1691,x1693)
% 0.58/0.70 [190]~P3(x1903,x1902)+~P6(x1901,x1902)+~P6(x1901,x1903)
% 0.58/0.70 [163]~E(x1631,x1633)+~P1(x1631)+P6(x1631,f47(x1632,x1633))
% 0.58/0.70 [164]~E(x1641,x1642)+~P1(x1641)+P6(x1641,f47(x1642,x1643))
% 0.58/0.70 [185]~P6(x1851,x1853)+~P6(x1853,x1852)+P6(x1851,f53(x1852))
% 0.58/0.70 [189]E(x1891,x1892)+E(x1891,x1893)+~P6(x1891,f47(x1893,x1892))
% 0.58/0.70 [204]~P6(x2041,x2043)+~P6(x2041,x2042)+P6(x2041,f48(x2042,x2043))
% 0.58/0.70 [156]~P1(x1561)+~P10(x1561)+~E(f49(x1561),f33(x1561))+P6(x1561,a44)
% 0.58/0.70 [191]~P1(x1911)+~P10(x1911)+~P6(f33(x1911),f49(x1911))+P6(x1911,a13)
% 0.58/0.70 [218]~P1(x2182)+~P1(x2181)+P4(x2181,x2182)+~P7(x2182,f10(x2181,x2181),x2181)
% 0.58/0.70 [241]~P1(x2411)+~P10(x2411)+P6(x2411,f5(x2412))+~P6(f47(f47(f49(x2411),f49(x2411)),f47(f49(x2411),f33(x2411))),x2412)
% 0.58/0.70 [170]~P1(x1702)+~P1(x1701)+E(x1701,x1702)+~E(f47(x1703,x1701),f47(x1703,x1702))
% 0.58/0.70 [207]~P2(x2071)+P7(x2071,x2072,x2073)+~E(f9(x2071),x2072)+~P13(f52(x2071),x2073)
% 0.58/0.70 [214]~P1(x2143)+~P1(x2142)+P10(x2141)+~E(x2141,f47(f47(x2142,x2142),f47(x2142,x2143)))
% 0.58/0.70 [231]~P1(x2312)+~P1(x2311)+E(x2311,x2312)+~E(f47(f47(x2311,x2311),f47(x2311,x2313)),f47(f47(x2312,x2312),f47(x2312,x2314)))
% 0.58/0.70 [256]~P6(x2563,x2566)+~P5(x2561,x2566,x2562,x2567,x2565)+~P6(x2564,x2566)+E(f7(x2561,f7(x2562,f47(f47(x2563,x2563),f47(x2563,x2564)))),f7(x2565,f47(f47(f7(x2561,x2563),f7(x2561,x2563)),f47(f7(x2561,x2563),f7(x2561,x2564)))))
% 0.58/0.70 [186]~P1(x1861)+~P10(x1863)+~P6(x1863,x1862)+P6(x1861,f9(x1862))+~E(x1861,f33(x1863))
% 0.58/0.70 [187]~P1(x1871)+~P10(x1873)+~P6(x1873,x1872)+P6(x1871,f52(x1872))+~E(x1871,f49(x1873))
% 0.58/0.70 [212]~P1(x2121)+~P10(x2121)+~P6(f33(x2121),x2122)+~P6(f49(x2121),x2123)+P6(x2121,f10(x2122,x2123))
% 0.58/0.70 [210]~P10(x2104)+~P6(x2104,x2102)+~P6(x2101,f49(x2104))+P6(x2101,f7(x2102,x2103))+~E(f33(x2104),x2103)
% 0.58/0.70 [219]~P1(x2194)+~P1(x2193)+~P6(x2191,x2193)+P6(x2191,f33(x2192))+~E(x2192,f47(f47(x2193,x2193),f47(x2193,x2194)))
% 0.58/0.70 [220]~P1(x2204)+~P1(x2203)+~P6(x2201,x2204)+P6(x2201,f49(x2202))+~E(x2202,f47(f47(x2203,x2203),f47(x2203,x2204)))
% 0.58/0.70 [257]~P4(x2574,x2575)+~P4(x2572,x2573)+~P7(x2571,x2572,x2574)+P5(x2571,x2572,x2573,x2574,x2575)+P6(f37(x2571,x2572,x2573,x2574,x2575),x2572)
% 0.58/0.70 [258]~P4(x2584,x2585)+~P4(x2582,x2583)+~P7(x2581,x2582,x2584)+P5(x2581,x2582,x2583,x2584,x2585)+P6(f38(x2581,x2582,x2583,x2584,x2585),x2582)
% 0.58/0.70 [259]~P4(x2594,x2595)+~P4(x2592,x2593)+~P7(x2591,x2592,x2594)+P5(x2591,x2592,x2593,x2594,x2595)+~E(f7(x2591,f7(x2593,f47(f47(f37(x2591,x2592,x2593,x2594,x2595),f37(x2591,x2592,x2593,x2594,x2595)),f47(f37(x2591,x2592,x2593,x2594,x2595),f38(x2591,x2592,x2593,x2594,x2595))))),f7(x2595,f47(f47(f7(x2591,f37(x2591,x2592,x2593,x2594,x2595)),f7(x2591,f37(x2591,x2592,x2593,x2594,x2595))),f47(f7(x2591,f37(x2591,x2592,x2593,x2594,x2595)),f7(x2591,f38(x2591,x2592,x2593,x2594,x2595))))))
% 0.58/0.70 [211]~P1(x2111)+~P10(x2114)+~P6(x2114,x2113)+~P6(f33(x2114),x2112)+P6(x2111,f46(x2112,x2113))+~E(f49(x2114),x2111)
% 0.58/0.70 [232]~P1(x2322)+~P1(x2324)+~P1(x2321)+~P1(x2323)+E(x2321,x2322)+~E(f47(f47(x2323,x2323),f47(x2323,x2321)),f47(f47(x2324,x2324),f47(x2324,x2322)))
% 0.58/0.70 [242]~P1(x2422)+~P1(x2421)+E(x2421,x2422)+~P1(x2423)+~P12(x2424)+~P6(f47(f47(x2423,x2423),f47(x2423,x2422)),x2424)+~P6(f47(f47(x2423,x2423),f47(x2423,x2421)),x2424)
% 0.58/0.70 [247]~P1(x2475)+~P1(x2474)+~P1(x2473)+~P1(x2471)+P6(x2471,f51(x2472))+~P6(f47(f47(x2474,x2474),f47(x2474,f47(f47(x2475,x2475),f47(x2475,x2473)))),x2472)+~E(x2471,f47(f47(x2473,x2473),f47(x2473,f47(f47(x2474,x2474),f47(x2474,x2475)))))
% 0.58/0.70 [248]~P1(x2485)+~P1(x2484)+~P1(x2483)+~P1(x2481)+P6(x2481,f45(x2482))+~P6(f47(f47(x2483,x2483),f47(x2483,f47(f47(x2485,x2485),f47(x2485,x2484)))),x2482)+~E(x2481,f47(f47(x2483,x2483),f47(x2483,f47(f47(x2484,x2484),f47(x2484,x2485)))))
% 0.58/0.70 [243]~P1(x2435)+~P1(x2434)+~P1(x2431)+~P1(x2436)+P6(x2431,f8(x2432,x2433))+~P6(f47(f47(x2436,x2436),f47(x2436,x2435)),x2433)+~P6(f47(f47(x2434,x2434),f47(x2434,x2436)),x2432)+~E(x2431,f47(f47(x2434,x2434),f47(x2434,x2435)))
% 0.58/0.70 %EqnAxiom
% 0.58/0.70 [1]E(x11,x11)
% 0.58/0.70 [2]E(x22,x21)+~E(x21,x22)
% 0.58/0.70 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.58/0.70 [4]~E(x41,x42)+E(f47(x41,x43),f47(x42,x43))
% 0.58/0.70 [5]~E(x51,x52)+E(f47(x53,x51),f47(x53,x52))
% 0.58/0.70 [6]~E(x61,x62)+E(f7(x61,x63),f7(x62,x63))
% 0.58/0.70 [7]~E(x71,x72)+E(f7(x73,x71),f7(x73,x72))
% 0.58/0.70 [8]~E(x81,x82)+E(f11(x81),f11(x82))
% 0.58/0.70 [9]~E(x91,x92)+E(f22(x91),f22(x92))
% 0.58/0.70 [10]~E(x101,x102)+E(f24(x101),f24(x102))
% 0.58/0.70 [11]~E(x111,x112)+E(f6(x111),f6(x112))
% 0.58/0.70 [12]~E(x121,x122)+E(f49(x121),f49(x122))
% 0.58/0.70 [13]~E(x131,x132)+E(f23(x131),f23(x132))
% 0.58/0.70 [14]~E(x141,x142)+E(f28(x141),f28(x142))
% 0.58/0.70 [15]~E(x151,x152)+E(f33(x151),f33(x152))
% 0.58/0.70 [16]~E(x161,x162)+E(f41(x161,x163),f41(x162,x163))
% 0.58/0.70 [17]~E(x171,x172)+E(f41(x173,x171),f41(x173,x172))
% 0.58/0.70 [18]~E(x181,x182)+E(f53(x181),f53(x182))
% 0.58/0.70 [19]~E(x191,x192)+E(f50(x191),f50(x192))
% 0.58/0.70 [20]~E(x201,x202)+E(f5(x201),f5(x202))
% 0.58/0.70 [21]~E(x211,x212)+E(f12(x211),f12(x212))
% 0.58/0.70 [22]~E(x221,x222)+E(f25(x221),f25(x222))
% 0.58/0.70 [23]~E(x231,x232)+E(f45(x231),f45(x232))
% 0.58/0.70 [24]~E(x241,x242)+E(f29(x241),f29(x242))
% 0.58/0.70 [25]~E(x251,x252)+E(f46(x251,x253),f46(x252,x253))
% 0.58/0.70 [26]~E(x261,x262)+E(f46(x263,x261),f46(x263,x262))
% 0.58/0.70 [27]~E(x271,x272)+E(f40(x271,x273),f40(x272,x273))
% 0.58/0.70 [28]~E(x281,x282)+E(f40(x283,x281),f40(x283,x282))
% 0.58/0.70 [29]~E(x291,x292)+E(f36(x291,x293,x294),f36(x292,x293,x294))
% 0.58/0.70 [30]~E(x301,x302)+E(f36(x303,x301,x304),f36(x303,x302,x304))
% 0.58/0.70 [31]~E(x311,x312)+E(f36(x313,x314,x311),f36(x313,x314,x312))
% 0.58/0.70 [32]~E(x321,x322)+E(f32(x321,x323,x324),f32(x322,x323,x324))
% 0.58/0.70 [33]~E(x331,x332)+E(f32(x333,x331,x334),f32(x333,x332,x334))
% 0.58/0.70 [34]~E(x341,x342)+E(f32(x343,x344,x341),f32(x343,x344,x342))
% 0.58/0.70 [35]~E(x351,x352)+E(f14(x351,x353),f14(x352,x353))
% 0.58/0.70 [36]~E(x361,x362)+E(f14(x363,x361),f14(x363,x362))
% 0.58/0.70 [37]~E(x371,x372)+E(f27(x371,x373,x374),f27(x372,x373,x374))
% 0.58/0.70 [38]~E(x381,x382)+E(f27(x383,x381,x384),f27(x383,x382,x384))
% 0.58/0.70 [39]~E(x391,x392)+E(f27(x393,x394,x391),f27(x393,x394,x392))
% 0.58/0.70 [40]~E(x401,x402)+E(f51(x401),f51(x402))
% 0.58/0.70 [41]~E(x411,x412)+E(f19(x411,x413),f19(x412,x413))
% 0.58/0.70 [42]~E(x421,x422)+E(f19(x423,x421),f19(x423,x422))
% 0.58/0.70 [43]~E(x431,x432)+E(f20(x431,x433),f20(x432,x433))
% 0.58/0.70 [44]~E(x441,x442)+E(f20(x443,x441),f20(x443,x442))
% 0.58/0.70 [45]~E(x451,x452)+E(f18(x451,x453),f18(x452,x453))
% 0.58/0.70 [46]~E(x461,x462)+E(f18(x463,x461),f18(x463,x462))
% 0.58/0.70 [47]~E(x471,x472)+E(f37(x471,x473,x474,x475,x476),f37(x472,x473,x474,x475,x476))
% 0.58/0.70 [48]~E(x481,x482)+E(f37(x483,x481,x484,x485,x486),f37(x483,x482,x484,x485,x486))
% 0.58/0.70 [49]~E(x491,x492)+E(f37(x493,x494,x491,x495,x496),f37(x493,x494,x492,x495,x496))
% 0.58/0.70 [50]~E(x501,x502)+E(f37(x503,x504,x505,x501,x506),f37(x503,x504,x505,x502,x506))
% 0.58/0.70 [51]~E(x511,x512)+E(f37(x513,x514,x515,x516,x511),f37(x513,x514,x515,x516,x512))
% 0.58/0.70 [52]~E(x521,x522)+E(f42(x521,x523),f42(x522,x523))
% 0.58/0.70 [53]~E(x531,x532)+E(f42(x533,x531),f42(x533,x532))
% 0.58/0.70 [54]~E(x541,x542)+E(f8(x541,x543),f8(x542,x543))
% 0.58/0.70 [55]~E(x551,x552)+E(f8(x553,x551),f8(x553,x552))
% 0.58/0.70 [56]~E(x561,x562)+E(f16(x561,x563),f16(x562,x563))
% 0.58/0.70 [57]~E(x571,x572)+E(f16(x573,x571),f16(x573,x572))
% 0.58/0.70 [58]~E(x581,x582)+E(f31(x581,x583,x584),f31(x582,x583,x584))
% 0.58/0.70 [59]~E(x591,x592)+E(f31(x593,x591,x594),f31(x593,x592,x594))
% 0.58/0.70 [60]~E(x601,x602)+E(f31(x603,x604,x601),f31(x603,x604,x602))
% 0.58/0.70 [61]~E(x611,x612)+E(f38(x611,x613,x614,x615,x616),f38(x612,x613,x614,x615,x616))
% 0.58/0.70 [62]~E(x621,x622)+E(f38(x623,x621,x624,x625,x626),f38(x623,x622,x624,x625,x626))
% 0.58/0.70 [63]~E(x631,x632)+E(f38(x633,x634,x631,x635,x636),f38(x633,x634,x632,x635,x636))
% 0.58/0.71 [64]~E(x641,x642)+E(f38(x643,x644,x645,x641,x646),f38(x643,x644,x645,x642,x646))
% 0.58/0.71 [65]~E(x651,x652)+E(f38(x653,x654,x655,x656,x651),f38(x653,x654,x655,x656,x652))
% 0.58/0.71 [66]~E(x661,x662)+E(f15(x661,x663),f15(x662,x663))
% 0.58/0.71 [67]~E(x671,x672)+E(f15(x673,x671),f15(x673,x672))
% 0.58/0.71 [68]~E(x681,x682)+E(f26(x681,x683),f26(x682,x683))
% 0.58/0.71 [69]~E(x691,x692)+E(f26(x693,x691),f26(x693,x692))
% 0.58/0.71 [70]~E(x701,x702)+E(f48(x701,x703),f48(x702,x703))
% 0.58/0.71 [71]~E(x711,x712)+E(f48(x713,x711),f48(x713,x712))
% 0.58/0.71 [72]~E(x721,x722)+E(f17(x721,x723),f17(x722,x723))
% 0.58/0.71 [73]~E(x731,x732)+E(f17(x733,x731),f17(x733,x732))
% 0.58/0.71 [74]~E(x741,x742)+E(f52(x741),f52(x742))
% 0.58/0.71 [75]~E(x751,x752)+E(f10(x751,x753),f10(x752,x753))
% 0.58/0.71 [76]~E(x761,x762)+E(f10(x763,x761),f10(x763,x762))
% 0.58/0.71 [77]~E(x771,x772)+E(f34(x771,x773),f34(x772,x773))
% 0.58/0.71 [78]~E(x781,x782)+E(f34(x783,x781),f34(x783,x782))
% 0.58/0.71 [79]~E(x791,x792)+E(f30(x791,x793),f30(x792,x793))
% 0.58/0.71 [80]~E(x801,x802)+E(f30(x803,x801),f30(x803,x802))
% 0.58/0.71 [81]~E(x811,x812)+E(f39(x811,x813),f39(x812,x813))
% 0.58/0.71 [82]~E(x821,x822)+E(f39(x823,x821),f39(x823,x822))
% 0.58/0.71 [83]~E(x831,x832)+E(f43(x831,x833),f43(x832,x833))
% 0.58/0.71 [84]~E(x841,x842)+E(f43(x843,x841),f43(x843,x842))
% 0.58/0.71 [85]~E(x851,x852)+E(f9(x851),f9(x852))
% 0.58/0.71 [86]~E(x861,x862)+E(f35(x861,x863,x864),f35(x862,x863,x864))
% 0.58/0.71 [87]~E(x871,x872)+E(f35(x873,x871,x874),f35(x873,x872,x874))
% 0.58/0.71 [88]~E(x881,x882)+E(f35(x883,x884,x881),f35(x883,x884,x882))
% 0.58/0.71 [89]~E(x891,x892)+E(f21(x891,x893),f21(x892,x893))
% 0.58/0.71 [90]~E(x901,x902)+E(f21(x903,x901),f21(x903,x902))
% 0.58/0.71 [91]~P1(x911)+P1(x912)+~E(x911,x912)
% 0.58/0.71 [92]P7(x922,x923,x924)+~E(x921,x922)+~P7(x921,x923,x924)
% 0.58/0.71 [93]P7(x933,x932,x934)+~E(x931,x932)+~P7(x933,x931,x934)
% 0.58/0.71 [94]P7(x943,x944,x942)+~E(x941,x942)+~P7(x943,x944,x941)
% 0.58/0.71 [95]~P2(x951)+P2(x952)+~E(x951,x952)
% 0.58/0.71 [96]P6(x962,x963)+~E(x961,x962)+~P6(x961,x963)
% 0.58/0.71 [97]P6(x973,x972)+~E(x971,x972)+~P6(x973,x971)
% 0.58/0.71 [98]P4(x982,x983)+~E(x981,x982)+~P4(x981,x983)
% 0.58/0.71 [99]P4(x993,x992)+~E(x991,x992)+~P4(x993,x991)
% 0.58/0.71 [100]P13(x1002,x1003)+~E(x1001,x1002)+~P13(x1001,x1003)
% 0.58/0.71 [101]P13(x1013,x1012)+~E(x1011,x1012)+~P13(x1013,x1011)
% 0.58/0.71 [102]~P10(x1021)+P10(x1022)+~E(x1021,x1022)
% 0.58/0.71 [103]~P8(x1031)+P8(x1032)+~E(x1031,x1032)
% 0.58/0.71 [104]~P12(x1041)+P12(x1042)+~E(x1041,x1042)
% 0.58/0.71 [105]~P9(x1051)+P9(x1052)+~E(x1051,x1052)
% 0.58/0.71 [106]P5(x1062,x1063,x1064,x1065,x1066)+~E(x1061,x1062)+~P5(x1061,x1063,x1064,x1065,x1066)
% 0.58/0.71 [107]P5(x1073,x1072,x1074,x1075,x1076)+~E(x1071,x1072)+~P5(x1073,x1071,x1074,x1075,x1076)
% 0.58/0.71 [108]P5(x1083,x1084,x1082,x1085,x1086)+~E(x1081,x1082)+~P5(x1083,x1084,x1081,x1085,x1086)
% 0.58/0.71 [109]P5(x1093,x1094,x1095,x1092,x1096)+~E(x1091,x1092)+~P5(x1093,x1094,x1095,x1091,x1096)
% 0.58/0.71 [110]P5(x1103,x1104,x1105,x1106,x1102)+~E(x1101,x1102)+~P5(x1103,x1104,x1105,x1106,x1101)
% 0.58/0.71 [111]P3(x1112,x1113)+~E(x1111,x1112)+~P3(x1111,x1113)
% 0.58/0.71 [112]P3(x1123,x1122)+~E(x1121,x1122)+~P3(x1123,x1121)
% 0.58/0.71 [113]P11(x1132,x1133)+~E(x1131,x1132)+~P11(x1131,x1133)
% 0.58/0.71 [114]P11(x1143,x1142)+~E(x1141,x1142)+~P11(x1143,x1141)
% 0.58/0.71
% 0.58/0.71 %-------------------------------------------
% 0.58/0.71 cnf(261,plain,
% 0.58/0.71 (~P1(x2611)+P6(x2611,f47(x2612,x2611))),
% 0.58/0.71 inference(equality_inference,[],[163])).
% 0.58/0.71 cnf(277,plain,
% 0.58/0.71 ($false),
% 0.58/0.71 inference(scs_inference,[],[121,116,261]),
% 0.58/0.71 ['proof']).
% 0.58/0.71 % SZS output end Proof
% 0.58/0.71 % Total time :0.020000s
%------------------------------------------------------------------------------