%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET062-7 : 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 14:20:25 EDT 2024
% Result : Unsatisfiable 0.57s 0.64s
% Output : CNFRefutation 0.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SET062-7 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.32 % Computer : n026.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Sun Jun 23 11:31:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.56 start to proof:theBenchmark
% 0.57/0.63 %-------------------------------------------
% 0.57/0.63 % File :CSE---1.7
% 0.57/0.63 % Problem :theBenchmark
% 0.57/0.63 % Transform :cnf
% 0.57/0.63 % Format :tptp:raw
% 0.57/0.63 % Command :java -jar mcs_scs.jar %d %s
% 0.57/0.63
% 0.57/0.63 % Result :Theorem 0.000000s
% 0.57/0.63 % Output :CNFRefutation 0.000000s
% 0.57/0.63 %-------------------------------------------
% 0.57/0.63 %--------------------------------------------------------------------------
% 0.57/0.64 % File : SET062-7 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.57/0.64 % Domain : Set Theory
% 0.57/0.64 % Problem : The empty set is a subset of X
% 0.57/0.64 % Version : [Qua92] axioms : Augmented.
% 0.57/0.64 % English :
% 0.57/0.64
% 0.57/0.64 % Refs : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 0.57/0.64 % Source : [Quaife]
% 0.57/0.64 % Names : SP3 [Qua92]
% 0.57/0.64
% 0.57/0.64 % Status : Unsatisfiable
% 0.57/0.64 % Rating : 0.10 v8.2.0, 0.14 v8.1.0, 0.11 v7.4.0, 0.12 v7.3.0, 0.00 v7.0.0, 0.13 v6.4.0, 0.07 v6.3.0, 0.00 v6.2.0, 0.10 v6.1.0, 0.00 v5.5.0, 0.10 v5.3.0, 0.06 v5.1.0, 0.12 v5.0.0, 0.14 v4.1.0, 0.15 v4.0.1, 0.18 v4.0.0, 0.27 v3.7.0, 0.20 v3.5.0, 0.18 v3.4.0, 0.08 v3.3.0, 0.07 v3.2.0, 0.08 v3.1.0, 0.09 v2.7.0, 0.17 v2.6.0, 0.11 v2.5.0, 0.09 v2.4.0, 0.00 v2.1.0
% 0.57/0.64 % Syntax : Number of clauses : 104 ( 33 unt; 11 nHn; 73 RR)
% 0.57/0.64 % Number of literals : 208 ( 43 equ; 97 neg)
% 0.57/0.64 % Maximal clause size : 5 ( 2 avg)
% 0.57/0.64 % Maximal term depth : 6 ( 1 avg)
% 0.57/0.64 % Number of predicates : 10 ( 9 usr; 0 prp; 1-3 aty)
% 0.57/0.64 % Number of functors : 39 ( 39 usr; 9 con; 0-3 aty)
% 0.57/0.64 % Number of variables : 207 ( 37 sgn)
% 0.57/0.64 % SPC : CNF_UNS_RFO_SEQ_NHN
% 0.57/0.64
% 0.57/0.64 % Comments : Preceding lemmas are added.
% 0.57/0.64 % Bugfixes : v2.1.0 - Bugfix in SET004-0.ax.
% 0.57/0.64 %--------------------------------------------------------------------------
% 0.57/0.64 %----Include von Neuman-Bernays-Godel set theory axioms
% 0.57/0.64 include('Axioms/SET004-0.ax').
% 0.57/0.64 %--------------------------------------------------------------------------
% 0.57/0.64 %----Corollaries to Unordered pair axiom. Not in paper, but in email.
% 0.57/0.64 cnf(corollary_1_to_unordered_pair,axiom,
% 0.57/0.64 ( ~ member(ordered_pair(X,Y),cross_product(U,V))
% 0.57/0.64 | member(X,unordered_pair(X,Y)) ) ).
% 0.57/0.64
% 0.57/0.64 cnf(corollary_2_to_unordered_pair,axiom,
% 0.57/0.64 ( ~ member(ordered_pair(X,Y),cross_product(U,V))
% 0.57/0.64 | member(Y,unordered_pair(X,Y)) ) ).
% 0.57/0.64
% 0.57/0.64 %----Corollaries to Cartesian product axiom.
% 0.57/0.64 cnf(corollary_1_to_cartesian_product,axiom,
% 0.57/0.64 ( ~ member(ordered_pair(U,V),cross_product(X,Y))
% 0.57/0.64 | member(U,universal_class) ) ).
% 0.57/0.64
% 0.57/0.64 cnf(corollary_2_to_cartesian_product,axiom,
% 0.57/0.64 ( ~ member(ordered_pair(U,V),cross_product(X,Y))
% 0.57/0.64 | member(V,universal_class) ) ).
% 0.57/0.64
% 0.57/0.64 %---- PARTIAL ORDER.
% 0.57/0.64 %----(PO1): reflexive.
% 0.57/0.64 cnf(subclass_is_reflexive,axiom,
% 0.57/0.64 subclass(X,X) ).
% 0.57/0.64
% 0.57/0.64 %----(PO2): antisymmetry is part of A-3.
% 0.57/0.64 %----(x < y), (y < x) --> (x = y).
% 0.57/0.64
% 0.57/0.64 %----(PO3): transitivity.
% 0.57/0.64 cnf(transitivity_of_subclass,axiom,
% 0.57/0.64 ( ~ subclass(X,Y)
% 0.57/0.64 | ~ subclass(Y,Z)
% 0.57/0.64 | subclass(X,Z) ) ).
% 0.57/0.64
% 0.57/0.64 %---- EQUALITY.
% 0.57/0.64 %----(EQ1): equality axiom.
% 0.57/0.64 %----a:x:(x = x).
% 0.57/0.64 %----This is always an axiom in the TPTP presentation.
% 0.57/0.64
% 0.57/0.64 %----(EQ2): expanded equality definition.
% 0.57/0.64 cnf(equality1,axiom,
% 0.57/0.64 ( X = Y
% 0.57/0.64 | member(not_subclass_element(X,Y),X)
% 0.57/0.64 | member(not_subclass_element(Y,X),Y) ) ).
% 0.57/0.64
% 0.57/0.64 cnf(equality2,axiom,
% 0.57/0.64 ( ~ member(not_subclass_element(X,Y),Y)
% 0.57/0.64 | X = Y
% 0.57/0.64 | member(not_subclass_element(Y,X),Y) ) ).
% 0.57/0.64
% 0.57/0.64 cnf(equality3,axiom,
% 0.57/0.64 ( ~ member(not_subclass_element(Y,X),X)
% 0.57/0.64 | X = Y
% 0.57/0.64 | member(not_subclass_element(X,Y),X) ) ).
% 0.57/0.64
% 0.57/0.64 cnf(equality4,axiom,
% 0.57/0.64 ( ~ member(not_subclass_element(X,Y),Y)
% 0.57/0.64 | ~ member(not_subclass_element(Y,X),X)
% 0.57/0.64 | X = Y ) ).
% 0.57/0.64
% 0.57/0.64 %---- SPECIAL CLASSES.
% 0.57/0.64 %----(SP1): lemma.
% 0.57/0.64 cnf(special_classes_lemma,axiom,
% 0.57/0.64 ~ member(Y,intersection(complement(X),X)) ).
% 0.57/0.64
% 0.57/0.64 %----(SP2): Existence of O (null class).
% 0.57/0.64 %----e:x:a:z:(-(z e x)).
% 0.57/0.64 cnf(existence_of_null_class,axiom,
% 0.57/0.64 ~ member(Z,null_class) ).
% 0.57/0.64
% 0.57/0.64 cnf(prove_null_class_is_subclass_1,negated_conjecture,
% 0.57/0.64 ~ subclass(null_class,x) ).
% 0.57/0.64
% 0.57/0.64 %--------------------------------------------------------------------------
% 0.57/0.64 %-------------------------------------------
% 0.57/0.64 % Proof found
% 0.57/0.64 % SZS status Theorem for theBenchmark
% 0.57/0.64 % SZS output start Proof
% 0.57/0.64 %ClaNum:131(EqnAxiom:42)
% 0.57/0.64 %VarNum:790(SingletonVarNum:179)
% 0.57/0.64 %MaxLitNum:5
% 0.57/0.64 %MaxfuncDepth:24
% 0.57/0.64 %SharedTerms:31
% 0.57/0.64 %goalClause: 58
% 0.57/0.64 %singleGoalClaCount:1
% 0.57/0.64 [43]P1(a1)
% 0.57/0.64 [44]P2(a2)
% 0.57/0.64 [45]P5(a1,a17)
% 0.57/0.64 [58]~P6(a13,a24)
% 0.57/0.64 [48]P6(a4,f5(a17,a17))
% 0.57/0.64 [49]P6(a18,f5(a17,a17))
% 0.57/0.64 [55]E(f9(f8(f10(f5(a21,a17))),a21),a12)
% 0.57/0.64 [56]E(f9(f5(a17,a17),f9(f5(a17,a17),f7(f6(f7(a4),f8(f10(f5(a4,a17))))))),a21)
% 0.57/0.64 [46]P6(x461,a17)
% 0.57/0.64 [47]P6(x471,x471)
% 0.57/0.64 [59]~P5(x591,a13)
% 0.57/0.64 [53]P6(f19(x531),f5(f5(a17,a17),a17))
% 0.57/0.64 [54]P6(f10(x541),f5(f5(a17,a17),a17))
% 0.57/0.64 [57]E(f9(f8(x571),f7(f8(f9(f6(f8(f10(f5(a4,a17))),x571),a12)))),f3(x571))
% 0.57/0.64 [50]P5(f23(x501,x502),a17)
% 0.57/0.64 [51]P6(f6(x511,x512),f5(a17,a17))
% 0.57/0.64 [60]~P5(x601,f9(f7(x602),x602))
% 0.57/0.64 [52]E(f9(f5(x521,x522),x523),f9(x523,f5(x521,x522)))
% 0.57/0.64 [61]~P7(x611)+P2(x611)
% 0.57/0.64 [62]~P8(x621)+P2(x621)
% 0.57/0.64 [65]~P1(x651)+P6(a1,x651)
% 0.57/0.64 [66]~P1(x661)+P5(a13,x661)
% 0.57/0.64 [68]P5(f20(x681),x681)+E(x681,a13)
% 0.57/0.64 [69]~P2(x691)+P6(x691,f5(a17,a17))
% 0.57/0.64 [67]E(x671,a13)+E(f9(x671,f20(x671)),a13)
% 0.57/0.64 [78]~P8(x781)+E(f5(f8(f8(x781)),f8(f8(x781))),f8(x781))
% 0.57/0.64 [91]~P7(x911)+P2(f8(f10(f5(x911,a17))))
% 0.57/0.64 [96]~P5(x961,a17)+P5(f8(f9(a4,f5(a17,x961))),a17)
% 0.57/0.64 [98]~P9(x981)+P6(f6(x981,f8(f10(f5(x981,a17)))),a12)
% 0.57/0.64 [99]~P2(x991)+P6(f6(x991,f8(f10(f5(x991,a17)))),a12)
% 0.57/0.64 [100]~P8(x1001)+P6(f8(f8(f10(f5(x1001,a17)))),f8(f8(x1001)))
% 0.57/0.64 [105]P9(x1051)+~P6(f6(x1051,f8(f10(f5(x1051,a17)))),a12)
% 0.57/0.64 [118]~P1(x1181)+P6(f8(f8(f10(f5(f9(a18,f5(x1181,a17)),a17)))),x1181)
% 0.57/0.64 [122]~P5(x1221,a17)+P5(f7(f8(f8(f10(f5(f9(a4,f5(f7(x1221),a17)),a17))))),a17)
% 0.57/0.64 [63]~E(x632,x631)+P6(x631,x632)
% 0.57/0.64 [64]~E(x641,x642)+P6(x641,x642)
% 0.57/0.64 [71]P6(x711,x712)+P5(f14(x711,x712),x711)
% 0.57/0.64 [72]~P5(x721,x722)+~P5(x721,f7(x722))
% 0.57/0.64 [76]~P5(x761,a17)+P5(x761,f23(x762,x761))
% 0.57/0.64 [77]~P5(x771,a17)+P5(x771,f23(x771,x772))
% 0.57/0.64 [82]P6(x821,x822)+~P5(f14(x821,x822),x822)
% 0.57/0.64 [95]~P5(x952,f8(x951))+~E(f9(x951,f5(f23(x952,x952),a17)),a13)
% 0.57/0.64 [104]P5(x1041,x1042)+~P5(f23(f23(x1041,x1041),f23(x1041,f23(x1042,x1042))),a4)
% 0.57/0.64 [115]~P5(f23(f23(x1151,x1151),f23(x1151,f23(x1152,x1152))),a18)+E(f7(f9(f7(x1151),f7(f23(x1151,x1151)))),x1152)
% 0.57/0.64 [85]P2(x851)+~P3(x851,x852,x853)
% 0.57/0.64 [86]P8(x861)+~P4(x862,x863,x861)
% 0.57/0.64 [87]P8(x871)+~P4(x872,x871,x873)
% 0.57/0.64 [94]~P4(x941,x942,x943)+P3(x941,x942,x943)
% 0.57/0.64 [80]P5(x801,x802)+~P5(x801,f9(x803,x802))
% 0.57/0.64 [81]P5(x811,x812)+~P5(x811,f9(x812,x813))
% 0.57/0.64 [88]~P3(x882,x881,x883)+E(f8(f8(x881)),f8(x882))
% 0.57/0.64 [101]~P5(x1011,f5(x1012,x1013))+E(f23(f23(f11(x1011),f11(x1011)),f23(f11(x1011),f23(f22(x1011),f22(x1011)))),x1011)
% 0.57/0.64 [103]~P3(x1031,x1033,x1032)+P6(f8(f8(f10(f5(x1031,a17)))),f8(f8(x1032)))
% 0.57/0.64 [106]P5(x1061,a17)+~P5(f23(f23(x1062,x1062),f23(x1062,f23(x1061,x1061))),f5(x1063,x1064))
% 0.57/0.64 [107]P5(x1071,a17)+~P5(f23(f23(x1071,x1071),f23(x1071,f23(x1072,x1072))),f5(x1073,x1074))
% 0.57/0.64 [108]P5(x1081,x1082)+~P5(f23(f23(x1083,x1083),f23(x1083,f23(x1081,x1081))),f5(x1084,x1082))
% 0.57/0.64 [109]P5(x1091,x1092)+~P5(f23(f23(x1091,x1091),f23(x1091,f23(x1093,x1093))),f5(x1092,x1094))
% 0.57/0.64 [111]P5(x1111,f23(x1112,x1111))+~P5(f23(f23(x1112,x1112),f23(x1112,f23(x1111,x1111))),f5(x1113,x1114))
% 0.57/0.64 [112]P5(x1121,f23(x1121,x1122))+~P5(f23(f23(x1121,x1121),f23(x1121,f23(x1122,x1122))),f5(x1123,x1124))
% 0.57/0.64 [123]~P5(f23(f23(f23(f23(x1233,x1233),f23(x1233,f23(x1231,x1231))),f23(f23(x1233,x1233),f23(x1233,f23(x1231,x1231)))),f23(f23(f23(x1233,x1233),f23(x1233,f23(x1231,x1231))),f23(x1232,x1232))),f19(x1234))+P5(f23(f23(f23(f23(x1231,x1231),f23(x1231,f23(x1232,x1232))),f23(f23(x1231,x1231),f23(x1231,f23(x1232,x1232)))),f23(f23(f23(x1231,x1231),f23(x1231,f23(x1232,x1232))),f23(x1233,x1233))),x1234)
% 0.57/0.64 [124]~P5(f23(f23(f23(f23(x1242,x1242),f23(x1242,f23(x1241,x1241))),f23(f23(x1242,x1242),f23(x1242,f23(x1241,x1241)))),f23(f23(f23(x1242,x1242),f23(x1242,f23(x1241,x1241))),f23(x1243,x1243))),f10(x1244))+P5(f23(f23(f23(f23(x1241,x1241),f23(x1241,f23(x1242,x1242))),f23(f23(x1241,x1241),f23(x1241,f23(x1242,x1242)))),f23(f23(f23(x1241,x1241),f23(x1241,f23(x1242,x1242))),f23(x1243,x1243))),x1244)
% 0.57/0.64 [128]~P5(f23(f23(x1284,x1284),f23(x1284,f23(x1281,x1281))),f6(x1282,x1283))+P5(x1281,f8(f8(f10(f5(f9(x1282,f5(f8(f8(f10(f5(f9(x1283,f5(f23(x1284,x1284),a17)),a17)))),a17)),a17)))))
% 0.57/0.64 [97]~P2(x971)+P7(x971)+~P2(f8(f10(f5(x971,a17))))
% 0.57/0.64 [110]P2(x1101)+~P6(x1101,f5(a17,a17))+~P6(f6(x1101,f8(f10(f5(x1101,a17)))),a12)
% 0.57/0.64 [120]P1(x1201)+~P5(a13,x1201)+~P6(f8(f8(f10(f5(f9(a18,f5(x1201,a17)),a17)))),x1201)
% 0.57/0.64 [127]~P5(x1271,a17)+E(x1271,a13)+P5(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(a2,f5(f23(x1271,x1271),a17)),a17))))))),x1271)
% 0.57/0.64 [70]~P6(x702,x701)+~P6(x701,x702)+E(x701,x702)
% 0.57/0.64 [73]P5(x731,x732)+P5(x731,f7(x732))+~P5(x731,a17)
% 0.57/0.64 [83]E(x831,x832)+P5(f14(x832,x831),x832)+P5(f14(x831,x832),x831)
% 0.57/0.64 [90]E(x901,x902)+P5(f14(x902,x901),x902)+~P5(f14(x901,x902),x902)
% 0.57/0.64 [92]E(x921,x922)+~P5(f14(x922,x921),x921)+~P5(f14(x921,x922),x922)
% 0.57/0.64 [93]P5(x932,f8(x931))+~P5(x932,a17)+E(f9(x931,f5(f23(x932,x932),a17)),a13)
% 0.57/0.64 [116]~P5(x1161,x1162)+~P5(f23(f23(x1161,x1161),f23(x1161,f23(x1162,x1162))),f5(a17,a17))+P5(f23(f23(x1161,x1161),f23(x1161,f23(x1162,x1162))),a4)
% 0.57/0.64 [117]~P5(f23(f23(x1171,x1171),f23(x1171,f23(x1172,x1172))),f5(a17,a17))+~E(f7(f9(f7(x1171),f7(f23(x1171,x1171)))),x1172)+P5(f23(f23(x1171,x1171),f23(x1171,f23(x1172,x1172))),a18)
% 0.57/0.64 [119]~P2(x1191)+~P5(x1192,a17)+P5(f8(f8(f10(f5(f9(x1191,f5(x1192,a17)),a17)))),a17)
% 0.57/0.64 [74]~P6(x741,x743)+P6(x741,x742)+~P6(x743,x742)
% 0.57/0.64 [75]~P5(x751,x753)+P5(x751,x752)+~P6(x753,x752)
% 0.57/0.64 [79]E(x791,x792)+E(x791,x793)+~P5(x791,f23(x793,x792))
% 0.57/0.64 [84]~P5(x841,x843)+~P5(x841,x842)+P5(x841,f9(x842,x843))
% 0.57/0.64 [102]~P5(x1022,x1024)+~P5(x1021,x1023)+P5(f23(f23(x1021,x1021),f23(x1021,f23(x1022,x1022))),f5(x1023,x1024))
% 0.57/0.64 [125]~P5(f23(f23(f23(f23(x1252,x1252),f23(x1252,f23(x1253,x1253))),f23(f23(x1252,x1252),f23(x1252,f23(x1253,x1253)))),f23(f23(f23(x1252,x1252),f23(x1252,f23(x1253,x1253))),f23(x1251,x1251))),x1254)+P5(f23(f23(f23(f23(x1251,x1251),f23(x1251,f23(x1252,x1252))),f23(f23(x1251,x1251),f23(x1251,f23(x1252,x1252)))),f23(f23(f23(x1251,x1251),f23(x1251,f23(x1252,x1252))),f23(x1253,x1253))),f19(x1254))+~P5(f23(f23(f23(f23(x1251,x1251),f23(x1251,f23(x1252,x1252))),f23(f23(x1251,x1251),f23(x1251,f23(x1252,x1252)))),f23(f23(f23(x1251,x1251),f23(x1251,f23(x1252,x1252))),f23(x1253,x1253))),f5(f5(a17,a17),a17))
% 0.57/0.64 [126]~P5(f23(f23(f23(f23(x1262,x1262),f23(x1262,f23(x1261,x1261))),f23(f23(x1262,x1262),f23(x1262,f23(x1261,x1261)))),f23(f23(f23(x1262,x1262),f23(x1262,f23(x1261,x1261))),f23(x1263,x1263))),x1264)+P5(f23(f23(f23(f23(x1261,x1261),f23(x1261,f23(x1262,x1262))),f23(f23(x1261,x1261),f23(x1261,f23(x1262,x1262)))),f23(f23(f23(x1261,x1261),f23(x1261,f23(x1262,x1262))),f23(x1263,x1263))),f10(x1264))+~P5(f23(f23(f23(f23(x1261,x1261),f23(x1261,f23(x1262,x1262))),f23(f23(x1261,x1261),f23(x1261,f23(x1262,x1262)))),f23(f23(f23(x1261,x1261),f23(x1261,f23(x1262,x1262))),f23(x1263,x1263))),f5(f5(a17,a17),a17))
% 0.57/0.64 [129]P5(f23(f23(x1291,x1291),f23(x1291,f23(x1292,x1292))),f6(x1293,x1294))+~P5(f23(f23(x1291,x1291),f23(x1291,f23(x1292,x1292))),f5(a17,a17))+~P5(x1292,f8(f8(f10(f5(f9(x1293,f5(f8(f8(f10(f5(f9(x1294,f5(f23(x1291,x1291),a17)),a17)))),a17)),a17)))))
% 0.57/0.64 [130]~P4(x1302,x1305,x1301)+~P5(f23(f23(x1303,x1303),f23(x1303,f23(x1304,x1304))),f8(x1305))+E(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1301,f5(f23(f23(f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1302,f5(f23(x1303,x1303),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1302,f5(f23(x1303,x1303),a17)),a17)))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1302,f5(f23(x1303,x1303),a17)),a17))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1302,f5(f23(x1304,x1304),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1302,f5(f23(x1304,x1304),a17)),a17)))))))))),f23(f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1302,f5(f23(x1303,x1303),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1302,f5(f23(x1303,x1303),a17)),a17)))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1302,f5(f23(x1303,x1303),a17)),a17))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1302,f5(f23(x1304,x1304),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1302,f5(f23(x1304,x1304),a17)),a17))))))))))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1302,f5(f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1305,f5(f23(f23(f23(x1303,x1303),f23(x1303,f23(x1304,x1304))),f23(f23(x1303,x1303),f23(x1303,f23(x1304,x1304)))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1305,f5(f23(f23(f23(x1303,x1303),f23(x1303,f23(x1304,x1304))),f23(f23(x1303,x1303),f23(x1303,f23(x1304,x1304)))),a17)),a17)))))))),a17)),a17))))))))
% 0.57/0.64 [114]~P2(x1141)+P8(x1141)+~E(f5(f8(f8(x1141)),f8(f8(x1141))),f8(x1141))+~P6(f8(f8(f10(f5(x1141,a17)))),f8(f8(x1141)))
% 0.57/0.64 [113]~P2(x1131)+P3(x1131,x1132,x1133)+~E(f8(f8(x1132)),f8(x1131))+~P6(f8(f8(f10(f5(x1131,a17)))),f8(f8(x1133)))
% 0.57/0.64 [121]~P8(x1213)+~P8(x1212)+~P3(x1211,x1212,x1213)+P4(x1211,x1212,x1213)+P5(f23(f23(f15(x1211,x1212,x1213),f15(x1211,x1212,x1213)),f23(f15(x1211,x1212,x1213),f23(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)))),f8(x1212))
% 0.57/0.64 [131]~P8(x1313)+~P8(x1312)+~P3(x1311,x1312,x1313)+P4(x1311,x1312,x1313)+~E(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1313,f5(f23(f23(f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1311,f5(f23(f15(x1311,x1312,x1313),f15(x1311,x1312,x1313)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1311,f5(f23(f15(x1311,x1312,x1313),f15(x1311,x1312,x1313)),a17)),a17)))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1311,f5(f23(f15(x1311,x1312,x1313),f15(x1311,x1312,x1313)),a17)),a17))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1311,f5(f23(f16(x1311,x1312,x1313),f16(x1311,x1312,x1313)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1311,f5(f23(f16(x1311,x1312,x1313),f16(x1311,x1312,x1313)),a17)),a17)))))))))),f23(f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1311,f5(f23(f15(x1311,x1312,x1313),f15(x1311,x1312,x1313)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1311,f5(f23(f15(x1311,x1312,x1313),f15(x1311,x1312,x1313)),a17)),a17)))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1311,f5(f23(f15(x1311,x1312,x1313),f15(x1311,x1312,x1313)),a17)),a17))))))),f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1311,f5(f23(f16(x1311,x1312,x1313),f16(x1311,x1312,x1313)),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1311,f5(f23(f16(x1311,x1312,x1313),f16(x1311,x1312,x1313)),a17)),a17))))))))))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1311,f5(f23(f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1312,f5(f23(f23(f23(f15(x1311,x1312,x1313),f15(x1311,x1312,x1313)),f23(f15(x1311,x1312,x1313),f23(f16(x1311,x1312,x1313),f16(x1311,x1312,x1313)))),f23(f23(f15(x1311,x1312,x1313),f15(x1311,x1312,x1313)),f23(f15(x1311,x1312,x1313),f23(f16(x1311,x1312,x1313),f16(x1311,x1312,x1313))))),a17)),a17))))))),f8(f9(a4,f5(a17,f8(f8(f10(f5(f9(x1312,f5(f23(f23(f23(f15(x1311,x1312,x1313),f15(x1311,x1312,x1313)),f23(f15(x1311,x1312,x1313),f23(f16(x1311,x1312,x1313),f16(x1311,x1312,x1313)))),f23(f23(f15(x1311,x1312,x1313),f15(x1311,x1312,x1313)),f23(f15(x1311,x1312,x1313),f23(f16(x1311,x1312,x1313),f16(x1311,x1312,x1313))))),a17)),a17)))))))),a17)),a17))))))))
% 0.57/0.64 %EqnAxiom
% 0.57/0.64 [1]E(x11,x11)
% 0.57/0.64 [2]E(x22,x21)+~E(x21,x22)
% 0.57/0.64 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.57/0.64 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43))
% 0.57/0.64 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52))
% 0.57/0.64 [6]~E(x61,x62)+E(f8(x61),f8(x62))
% 0.57/0.64 [7]~E(x71,x72)+E(f23(x71,x73),f23(x72,x73))
% 0.57/0.64 [8]~E(x81,x82)+E(f23(x83,x81),f23(x83,x82))
% 0.57/0.64 [9]~E(x91,x92)+E(f6(x91,x93),f6(x92,x93))
% 0.57/0.64 [10]~E(x101,x102)+E(f6(x103,x101),f6(x103,x102))
% 0.57/0.64 [11]~E(x111,x112)+E(f9(x111,x113),f9(x112,x113))
% 0.57/0.64 [12]~E(x121,x122)+E(f9(x123,x121),f9(x123,x122))
% 0.57/0.64 [13]~E(x131,x132)+E(f10(x131),f10(x132))
% 0.57/0.64 [14]~E(x141,x142)+E(f16(x141,x143,x144),f16(x142,x143,x144))
% 0.57/0.64 [15]~E(x151,x152)+E(f16(x153,x151,x154),f16(x153,x152,x154))
% 0.57/0.64 [16]~E(x161,x162)+E(f16(x163,x164,x161),f16(x163,x164,x162))
% 0.57/0.64 [17]~E(x171,x172)+E(f15(x171,x173,x174),f15(x172,x173,x174))
% 0.57/0.64 [18]~E(x181,x182)+E(f15(x183,x181,x184),f15(x183,x182,x184))
% 0.57/0.64 [19]~E(x191,x192)+E(f15(x193,x194,x191),f15(x193,x194,x192))
% 0.57/0.64 [20]~E(x201,x202)+E(f7(x201),f7(x202))
% 0.57/0.64 [21]~E(x211,x212)+E(f19(x211),f19(x212))
% 0.57/0.64 [22]~E(x221,x222)+E(f14(x221,x223),f14(x222,x223))
% 0.57/0.64 [23]~E(x231,x232)+E(f14(x233,x231),f14(x233,x232))
% 0.57/0.64 [24]~E(x241,x242)+E(f22(x241),f22(x242))
% 0.57/0.64 [25]~E(x251,x252)+E(f11(x251),f11(x252))
% 0.57/0.64 [26]~E(x261,x262)+E(f3(x261),f3(x262))
% 0.57/0.64 [27]~E(x271,x272)+E(f20(x271),f20(x272))
% 0.57/0.64 [28]~P1(x281)+P1(x282)+~E(x281,x282)
% 0.57/0.64 [29]~P2(x291)+P2(x292)+~E(x291,x292)
% 0.57/0.64 [30]P5(x302,x303)+~E(x301,x302)+~P5(x301,x303)
% 0.57/0.64 [31]P5(x313,x312)+~E(x311,x312)+~P5(x313,x311)
% 0.57/0.64 [32]P6(x322,x323)+~E(x321,x322)+~P6(x321,x323)
% 0.57/0.64 [33]P6(x333,x332)+~E(x331,x332)+~P6(x333,x331)
% 0.57/0.64 [34]~P8(x341)+P8(x342)+~E(x341,x342)
% 0.57/0.64 [35]P3(x352,x353,x354)+~E(x351,x352)+~P3(x351,x353,x354)
% 0.57/0.64 [36]P3(x363,x362,x364)+~E(x361,x362)+~P3(x363,x361,x364)
% 0.57/0.64 [37]P3(x373,x374,x372)+~E(x371,x372)+~P3(x373,x374,x371)
% 0.57/0.64 [38]P4(x382,x383,x384)+~E(x381,x382)+~P4(x381,x383,x384)
% 0.57/0.64 [39]P4(x393,x392,x394)+~E(x391,x392)+~P4(x393,x391,x394)
% 0.57/0.64 [40]P4(x403,x404,x402)+~E(x401,x402)+~P4(x403,x404,x401)
% 0.57/0.64 [41]~P9(x411)+P9(x412)+~E(x411,x412)
% 0.57/0.64 [42]~P7(x421)+P7(x422)+~E(x421,x422)
% 0.57/0.64
% 0.57/0.64 %-------------------------------------------
% 0.57/0.64 cnf(136,plain,
% 0.57/0.64 ($false),
% 0.57/0.64 inference(scs_inference,[],[58,59,71]),
% 0.57/0.64 ['proof']).
% 0.57/0.64 % SZS output end Proof
% 0.57/0.64 % Total time :0.000000s
%------------------------------------------------------------------------------