%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET071-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 : n021.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:29 EDT 2024
% Result : Unsatisfiable 0.56s 0.79s
% Output : CNFRefutation 0.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SET071-7 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.14/0.34 % Computer : n021.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Sun Jun 23 12:23:24 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.54/0.58 start to proof:theBenchmark
% 0.56/0.78 %-------------------------------------------
% 0.56/0.78 % File :CSE---1.7
% 0.56/0.78 % Problem :theBenchmark
% 0.56/0.78 % Transform :cnf
% 0.56/0.78 % Format :tptp:raw
% 0.56/0.78 % Command :java -jar mcs_scs.jar %d %s
% 0.56/0.78
% 0.56/0.78 % Result :Theorem 0.140000s
% 0.56/0.78 % Output :CNFRefutation 0.140000s
% 0.56/0.78 %-------------------------------------------
% 0.56/0.78 %--------------------------------------------------------------------------
% 0.56/0.78 % File : SET071-7 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.56/0.78 % Domain : Set Theory
% 0.56/0.78 % Problem : Null unordered pair
% 0.56/0.78 % Version : [Qua92] axioms : Augmented.
% 0.56/0.78 % English : If both arguments of an unordered pair are proper classes,
% 0.56/0.78 % the pair is null.
% 0.56/0.78
% 0.56/0.78 % Refs : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 0.56/0.78 % Source : [Quaife]
% 0.56/0.78 % Names : UP3 [Qua92]
% 0.56/0.78
% 0.56/0.78 % Status : Unsatisfiable
% 0.56/0.78 % Rating : 0.15 v8.2.0, 0.14 v8.1.0, 0.05 v7.5.0, 0.11 v7.4.0, 0.12 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.33 v6.4.0, 0.27 v6.3.0, 0.09 v6.2.0, 0.30 v6.1.0, 0.29 v6.0.0, 0.40 v5.5.0, 0.60 v5.4.0, 0.65 v5.3.0, 0.67 v5.2.0, 0.56 v5.1.0, 0.59 v5.0.0, 0.50 v4.1.0, 0.46 v4.0.1, 0.64 v4.0.0, 0.55 v3.7.0, 0.20 v3.5.0, 0.36 v3.4.0, 0.42 v3.3.0, 0.36 v3.2.0, 0.23 v3.1.0, 0.18 v2.7.0, 0.33 v2.5.0, 0.27 v2.4.0, 0.25 v2.2.1, 0.17 v2.2.0, 0.33 v2.1.0
% 0.56/0.78 % Syntax : Number of clauses : 115 ( 40 unt; 14 nHn; 77 RR)
% 0.56/0.78 % Number of literals : 223 ( 49 equ; 100 neg)
% 0.56/0.78 % Maximal clause size : 5 ( 1 avg)
% 0.56/0.78 % Maximal term depth : 6 ( 1 avg)
% 0.56/0.78 % Number of predicates : 10 ( 9 usr; 0 prp; 1-3 aty)
% 0.56/0.78 % Number of functors : 40 ( 40 usr; 10 con; 0-3 aty)
% 0.56/0.78 % Number of variables : 220 ( 40 sgn)
% 0.56/0.78 % SPC : CNF_UNS_RFO_SEQ_NHN
% 0.56/0.78
% 0.56/0.78 % Comments : Preceding lemmas are added.
% 0.56/0.78 % Bugfixes : v2.1.0 - Bugfix in SET004-0.ax.
% 0.56/0.78 %--------------------------------------------------------------------------
% 0.56/0.78 %----Include von Neuman-Bernays-Godel set theory axioms
% 0.56/0.78 include('Axioms/SET004-0.ax').
% 0.56/0.78 %--------------------------------------------------------------------------
% 0.56/0.78 %----Corollaries to Unordered pair axiom. Not in paper, but in email.
% 0.56/0.78 cnf(corollary_1_to_unordered_pair,axiom,
% 0.56/0.78 ( ~ member(ordered_pair(X,Y),cross_product(U,V))
% 0.56/0.78 | member(X,unordered_pair(X,Y)) ) ).
% 0.56/0.78
% 0.56/0.78 cnf(corollary_2_to_unordered_pair,axiom,
% 0.56/0.78 ( ~ member(ordered_pair(X,Y),cross_product(U,V))
% 0.56/0.78 | member(Y,unordered_pair(X,Y)) ) ).
% 0.56/0.78
% 0.56/0.78 %----Corollaries to Cartesian product axiom.
% 0.56/0.78 cnf(corollary_1_to_cartesian_product,axiom,
% 0.56/0.78 ( ~ member(ordered_pair(U,V),cross_product(X,Y))
% 0.56/0.78 | member(U,universal_class) ) ).
% 0.56/0.78
% 0.56/0.78 cnf(corollary_2_to_cartesian_product,axiom,
% 0.56/0.78 ( ~ member(ordered_pair(U,V),cross_product(X,Y))
% 0.56/0.78 | member(V,universal_class) ) ).
% 0.56/0.78
% 0.56/0.78 %---- PARTIAL ORDER.
% 0.56/0.78 %----(PO1): reflexive.
% 0.56/0.78 cnf(subclass_is_reflexive,axiom,
% 0.56/0.78 subclass(X,X) ).
% 0.56/0.78
% 0.56/0.78 %----(PO2): antisymmetry is part of A-3.
% 0.56/0.78 %----(x < y), (y < x) --> (x = y).
% 0.56/0.78
% 0.56/0.78 %----(PO3): transitivity.
% 0.56/0.78 cnf(transitivity_of_subclass,axiom,
% 0.56/0.78 ( ~ subclass(X,Y)
% 0.56/0.78 | ~ subclass(Y,Z)
% 0.56/0.78 | subclass(X,Z) ) ).
% 0.56/0.78
% 0.56/0.78 %---- EQUALITY.
% 0.56/0.78 %----(EQ1): equality axiom.
% 0.56/0.78 %----a:x:(x = x).
% 0.56/0.78 %----This is always an axiom in the TPTP presentation.
% 0.56/0.78
% 0.56/0.78 %----(EQ2): expanded equality definition.
% 0.56/0.78 cnf(equality1,axiom,
% 0.56/0.78 ( X = Y
% 0.56/0.78 | member(not_subclass_element(X,Y),X)
% 0.56/0.79 | member(not_subclass_element(Y,X),Y) ) ).
% 0.56/0.79
% 0.56/0.79 cnf(equality2,axiom,
% 0.56/0.79 ( ~ member(not_subclass_element(X,Y),Y)
% 0.56/0.79 | X = Y
% 0.56/0.79 | member(not_subclass_element(Y,X),Y) ) ).
% 0.56/0.79
% 0.56/0.79 cnf(equality3,axiom,
% 0.56/0.79 ( ~ member(not_subclass_element(Y,X),X)
% 0.56/0.79 | X = Y
% 0.56/0.79 | member(not_subclass_element(X,Y),X) ) ).
% 0.56/0.79
% 0.56/0.79 cnf(equality4,axiom,
% 0.56/0.79 ( ~ member(not_subclass_element(X,Y),Y)
% 0.56/0.79 | ~ member(not_subclass_element(Y,X),X)
% 0.56/0.79 | X = Y ) ).
% 0.56/0.79
% 0.56/0.79 %---- SPECIAL CLASSES.
% 0.56/0.79 %----(SP1): lemma.
% 0.56/0.79 cnf(special_classes_lemma,axiom,
% 0.56/0.79 ~ member(Y,intersection(complement(X),X)) ).
% 0.56/0.79
% 0.56/0.79 %----(SP2): Existence of O (null class).
% 0.56/0.79 %----e:x:a:z:(-(z e x)).
% 0.56/0.79 cnf(existence_of_null_class,axiom,
% 0.56/0.79 ~ member(Z,null_class) ).
% 0.56/0.79
% 0.56/0.79 %----(SP3): O is a subclass of every class.
% 0.56/0.79 cnf(null_class_is_subclass,axiom,
% 0.56/0.79 subclass(null_class,X) ).
% 0.56/0.79
% 0.56/0.79 %----corollary.
% 0.56/0.79 cnf(corollary_of_null_class_is_subclass,axiom,
% 0.56/0.79 ( ~ subclass(X,null_class)
% 0.56/0.79 | X = null_class ) ).
% 0.56/0.79
% 0.56/0.79 %----(SP4): uniqueness of null class.
% 0.56/0.79 cnf(null_class_is_unique,axiom,
% 0.56/0.79 ( Z = null_class
% 0.56/0.79 | member(not_subclass_element(Z,null_class),Z) ) ).
% 0.56/0.79
% 0.56/0.79 %----(SP5): O is a set (follows from axiom of infinity).
% 0.56/0.79 cnf(null_class_is_a_set,axiom,
% 0.56/0.79 member(null_class,universal_class) ).
% 0.56/0.79
% 0.56/0.79 %---- UNORDERED PAIRS.
% 0.56/0.79 %----(UP1): unordered pair is commutative.
% 0.56/0.79 cnf(commutativity_of_unordered_pair,axiom,
% 0.56/0.79 unordered_pair(X,Y) = unordered_pair(Y,X) ).
% 0.56/0.79
% 0.56/0.79 %----(UP2): if one argument is a proper class, pair contains only the
% 0.56/0.79 %----other. In a slightly different form to the paper
% 0.56/0.79 cnf(singleton_in_unordered_pair1,axiom,
% 0.56/0.79 subclass(singleton(X),unordered_pair(X,Y)) ).
% 0.56/0.79
% 0.56/0.79 cnf(singleton_in_unordered_pair2,axiom,
% 0.56/0.79 subclass(singleton(Y),unordered_pair(X,Y)) ).
% 0.56/0.79
% 0.56/0.79 cnf(unordered_pair_equals_singleton1,axiom,
% 0.56/0.79 ( member(Y,universal_class)
% 0.56/0.79 | unordered_pair(X,Y) = singleton(X) ) ).
% 0.56/0.79
% 0.56/0.79 cnf(unordered_pair_equals_singleton2,axiom,
% 0.56/0.79 ( member(X,universal_class)
% 0.56/0.79 | unordered_pair(X,Y) = singleton(Y) ) ).
% 0.56/0.79
% 0.56/0.79 cnf(prove_null_unordered_pair_1,negated_conjecture,
% 0.56/0.79 unordered_pair(x,y) != null_class ).
% 0.56/0.79
% 0.56/0.79 cnf(prove_null_unordered_pair_2,negated_conjecture,
% 0.56/0.79 ~ member(x,universal_class) ).
% 0.56/0.79
% 0.56/0.79 cnf(prove_null_unordered_pair_3,negated_conjecture,
% 0.56/0.79 ~ member(y,universal_class) ).
% 0.56/0.79
% 0.56/0.79 %--------------------------------------------------------------------------
% 0.56/0.79 %-------------------------------------------
% 0.56/0.79 % Proof found
% 0.56/0.79 % SZS status Theorem for theBenchmark
% 0.56/0.79 % SZS output start Proof
% 0.56/0.79 %ClaNum:142(EqnAxiom:42)
% 0.56/0.79 %VarNum:818(SingletonVarNum:192)
% 0.56/0.79 %MaxLitNum:5
% 0.56/0.79 %MaxfuncDepth:24
% 0.56/0.79 %SharedTerms:36
% 0.56/0.79 %goalClause: 63 64 65
% 0.56/0.79 %singleGoalClaCount:3
% 0.56/0.79 [43]P1(a1)
% 0.56/0.79 [44]P2(a2)
% 0.56/0.79 [45]P5(a4,a17)
% 0.56/0.79 [46]P5(a1,a17)
% 0.56/0.79 [64]~P5(a24,a17)
% 0.56/0.79 [65]~P5(a25,a17)
% 0.56/0.79 [51]P6(a5,f6(a17,a17))
% 0.56/0.79 [52]P6(a18,f6(a17,a17))
% 0.56/0.79 [63]~E(f23(a24,a25),a4)
% 0.56/0.79 [60]E(f10(f9(f11(f6(a21,a17))),a21),a13)
% 0.56/0.79 [61]E(f10(f6(a17,a17),f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17))))))),a21)
% 0.56/0.79 [47]P6(x471,a17)
% 0.56/0.79 [48]P6(a4,x481)
% 0.56/0.79 [49]P6(x491,x491)
% 0.56/0.79 [66]~P5(x661,a4)
% 0.56/0.79 [58]P6(f19(x581),f6(f6(a17,a17),a17))
% 0.56/0.79 [59]P6(f11(x591),f6(f6(a17,a17),a17))
% 0.56/0.79 [62]E(f10(f9(x621),f8(f9(f10(f7(f9(f11(f6(a5,a17))),x621),a13)))),f3(x621))
% 0.56/0.79 [50]E(f23(x501,x502),f23(x502,x501))
% 0.56/0.79 [53]P5(f23(x531,x532),a17)
% 0.56/0.79 [54]P6(f7(x541,x542),f6(a17,a17))
% 0.56/0.79 [55]P6(f23(x551,x551),f23(x552,x551))
% 0.56/0.79 [56]P6(f23(x561,x561),f23(x561,x562))
% 0.56/0.79 [67]~P5(x671,f10(f8(x672),x672))
% 0.56/0.79 [57]E(f10(f6(x571,x572),x573),f10(x573,f6(x571,x572)))
% 0.56/0.79 [68]~P7(x681)+P2(x681)
% 0.56/0.79 [69]~P8(x691)+P2(x691)
% 0.56/0.79 [72]~P1(x721)+P6(a1,x721)
% 0.56/0.79 [73]~P1(x731)+P5(a4,x731)
% 0.56/0.79 [74]~P6(x741,a4)+E(x741,a4)
% 0.56/0.79 [76]P5(f20(x761),x761)+E(x761,a4)
% 0.56/0.79 [77]E(x771,a4)+P5(f14(x771,a4),x771)
% 0.56/0.79 [80]~P2(x801)+P6(x801,f6(a17,a17))
% 0.56/0.79 [75]E(x751,a4)+E(f10(x751,f20(x751)),a4)
% 0.56/0.79 [89]~P8(x891)+E(f6(f9(f9(x891)),f9(f9(x891))),f9(x891))
% 0.56/0.79 [102]~P7(x1021)+P2(f9(f11(f6(x1021,a17))))
% 0.56/0.79 [107]~P5(x1071,a17)+P5(f9(f10(a5,f6(a17,x1071))),a17)
% 0.56/0.79 [109]~P9(x1091)+P6(f7(x1091,f9(f11(f6(x1091,a17)))),a13)
% 0.56/0.79 [110]~P2(x1101)+P6(f7(x1101,f9(f11(f6(x1101,a17)))),a13)
% 0.56/0.79 [111]~P8(x1111)+P6(f9(f9(f11(f6(x1111,a17)))),f9(f9(x1111)))
% 0.56/0.79 [116]P9(x1161)+~P6(f7(x1161,f9(f11(f6(x1161,a17)))),a13)
% 0.56/0.79 [129]~P1(x1291)+P6(f9(f9(f11(f6(f10(a18,f6(x1291,a17)),a17)))),x1291)
% 0.56/0.79 [133]~P5(x1331,a17)+P5(f8(f9(f9(f11(f6(f10(a5,f6(f8(x1331),a17)),a17))))),a17)
% 0.56/0.79 [70]~E(x702,x701)+P6(x701,x702)
% 0.56/0.79 [71]~E(x711,x712)+P6(x711,x712)
% 0.56/0.79 [78]P5(x782,a17)+E(f23(x781,x782),f23(x781,x781))
% 0.56/0.79 [79]P5(x791,a17)+E(f23(x791,x792),f23(x792,x792))
% 0.56/0.79 [82]P6(x821,x822)+P5(f14(x821,x822),x821)
% 0.56/0.79 [83]~P5(x831,x832)+~P5(x831,f8(x832))
% 0.56/0.79 [87]~P5(x871,a17)+P5(x871,f23(x872,x871))
% 0.56/0.79 [88]~P5(x881,a17)+P5(x881,f23(x881,x882))
% 0.56/0.79 [93]P6(x931,x932)+~P5(f14(x931,x932),x932)
% 0.56/0.79 [106]~P5(x1062,f9(x1061))+~E(f10(x1061,f6(f23(x1062,x1062),a17)),a4)
% 0.56/0.79 [115]P5(x1151,x1152)+~P5(f23(f23(x1151,x1151),f23(x1151,f23(x1152,x1152))),a5)
% 0.56/0.79 [126]~P5(f23(f23(x1261,x1261),f23(x1261,f23(x1262,x1262))),a18)+E(f8(f10(f8(x1261),f8(f23(x1261,x1261)))),x1262)
% 0.56/0.79 [96]P2(x961)+~P3(x961,x962,x963)
% 0.56/0.79 [97]P8(x971)+~P4(x972,x973,x971)
% 0.56/0.79 [98]P8(x981)+~P4(x982,x981,x983)
% 0.56/0.79 [105]~P4(x1051,x1052,x1053)+P3(x1051,x1052,x1053)
% 0.56/0.79 [91]P5(x911,x912)+~P5(x911,f10(x913,x912))
% 0.56/0.79 [92]P5(x921,x922)+~P5(x921,f10(x922,x923))
% 0.56/0.79 [99]~P3(x992,x991,x993)+E(f9(f9(x991)),f9(x992))
% 0.56/0.79 [112]~P5(x1121,f6(x1122,x1123))+E(f23(f23(f12(x1121),f12(x1121)),f23(f12(x1121),f23(f22(x1121),f22(x1121)))),x1121)
% 0.56/0.79 [114]~P3(x1141,x1143,x1142)+P6(f9(f9(f11(f6(x1141,a17)))),f9(f9(x1142)))
% 0.56/0.79 [117]P5(x1171,a17)+~P5(f23(f23(x1172,x1172),f23(x1172,f23(x1171,x1171))),f6(x1173,x1174))
% 0.56/0.79 [118]P5(x1181,a17)+~P5(f23(f23(x1181,x1181),f23(x1181,f23(x1182,x1182))),f6(x1183,x1184))
% 0.56/0.79 [119]P5(x1191,x1192)+~P5(f23(f23(x1193,x1193),f23(x1193,f23(x1191,x1191))),f6(x1194,x1192))
% 0.56/0.79 [120]P5(x1201,x1202)+~P5(f23(f23(x1201,x1201),f23(x1201,f23(x1203,x1203))),f6(x1202,x1204))
% 0.56/0.79 [122]P5(x1221,f23(x1222,x1221))+~P5(f23(f23(x1222,x1222),f23(x1222,f23(x1221,x1221))),f6(x1223,x1224))
% 0.56/0.79 [123]P5(x1231,f23(x1231,x1232))+~P5(f23(f23(x1231,x1231),f23(x1231,f23(x1232,x1232))),f6(x1233,x1234))
% 0.56/0.79 [134]~P5(f23(f23(f23(f23(x1343,x1343),f23(x1343,f23(x1341,x1341))),f23(f23(x1343,x1343),f23(x1343,f23(x1341,x1341)))),f23(f23(f23(x1343,x1343),f23(x1343,f23(x1341,x1341))),f23(x1342,x1342))),f19(x1344))+P5(f23(f23(f23(f23(x1341,x1341),f23(x1341,f23(x1342,x1342))),f23(f23(x1341,x1341),f23(x1341,f23(x1342,x1342)))),f23(f23(f23(x1341,x1341),f23(x1341,f23(x1342,x1342))),f23(x1343,x1343))),x1344)
% 0.56/0.79 [135]~P5(f23(f23(f23(f23(x1352,x1352),f23(x1352,f23(x1351,x1351))),f23(f23(x1352,x1352),f23(x1352,f23(x1351,x1351)))),f23(f23(f23(x1352,x1352),f23(x1352,f23(x1351,x1351))),f23(x1353,x1353))),f11(x1354))+P5(f23(f23(f23(f23(x1351,x1351),f23(x1351,f23(x1352,x1352))),f23(f23(x1351,x1351),f23(x1351,f23(x1352,x1352)))),f23(f23(f23(x1351,x1351),f23(x1351,f23(x1352,x1352))),f23(x1353,x1353))),x1354)
% 0.56/0.79 [139]~P5(f23(f23(x1394,x1394),f23(x1394,f23(x1391,x1391))),f7(x1392,x1393))+P5(x1391,f9(f9(f11(f6(f10(x1392,f6(f9(f9(f11(f6(f10(x1393,f6(f23(x1394,x1394),a17)),a17)))),a17)),a17)))))
% 0.56/0.79 [108]~P2(x1081)+P7(x1081)+~P2(f9(f11(f6(x1081,a17))))
% 0.56/0.79 [121]P2(x1211)+~P6(x1211,f6(a17,a17))+~P6(f7(x1211,f9(f11(f6(x1211,a17)))),a13)
% 0.56/0.79 [131]P1(x1311)+~P5(a4,x1311)+~P6(f9(f9(f11(f6(f10(a18,f6(x1311,a17)),a17)))),x1311)
% 0.56/0.79 [138]~P5(x1381,a17)+E(x1381,a4)+P5(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(a2,f6(f23(x1381,x1381),a17)),a17))))))),x1381)
% 0.56/0.79 [81]~P6(x812,x811)+~P6(x811,x812)+E(x811,x812)
% 0.56/0.79 [84]P5(x841,x842)+P5(x841,f8(x842))+~P5(x841,a17)
% 0.56/0.79 [94]E(x941,x942)+P5(f14(x942,x941),x942)+P5(f14(x941,x942),x941)
% 0.56/0.79 [101]E(x1011,x1012)+P5(f14(x1012,x1011),x1012)+~P5(f14(x1011,x1012),x1012)
% 0.56/0.79 [103]E(x1031,x1032)+~P5(f14(x1032,x1031),x1031)+~P5(f14(x1031,x1032),x1032)
% 0.56/0.79 [104]P5(x1042,f9(x1041))+~P5(x1042,a17)+E(f10(x1041,f6(f23(x1042,x1042),a17)),a4)
% 0.56/0.79 [127]~P5(x1271,x1272)+~P5(f23(f23(x1271,x1271),f23(x1271,f23(x1272,x1272))),f6(a17,a17))+P5(f23(f23(x1271,x1271),f23(x1271,f23(x1272,x1272))),a5)
% 0.56/0.79 [128]~P5(f23(f23(x1281,x1281),f23(x1281,f23(x1282,x1282))),f6(a17,a17))+~E(f8(f10(f8(x1281),f8(f23(x1281,x1281)))),x1282)+P5(f23(f23(x1281,x1281),f23(x1281,f23(x1282,x1282))),a18)
% 0.56/0.79 [130]~P2(x1301)+~P5(x1302,a17)+P5(f9(f9(f11(f6(f10(x1301,f6(x1302,a17)),a17)))),a17)
% 0.56/0.79 [85]~P6(x851,x853)+P6(x851,x852)+~P6(x853,x852)
% 0.56/0.79 [86]~P5(x861,x863)+P5(x861,x862)+~P6(x863,x862)
% 0.56/0.79 [90]E(x901,x902)+E(x901,x903)+~P5(x901,f23(x903,x902))
% 0.56/0.79 [95]~P5(x951,x953)+~P5(x951,x952)+P5(x951,f10(x952,x953))
% 0.56/0.79 [113]~P5(x1132,x1134)+~P5(x1131,x1133)+P5(f23(f23(x1131,x1131),f23(x1131,f23(x1132,x1132))),f6(x1133,x1134))
% 0.56/0.79 [136]~P5(f23(f23(f23(f23(x1362,x1362),f23(x1362,f23(x1363,x1363))),f23(f23(x1362,x1362),f23(x1362,f23(x1363,x1363)))),f23(f23(f23(x1362,x1362),f23(x1362,f23(x1363,x1363))),f23(x1361,x1361))),x1364)+P5(f23(f23(f23(f23(x1361,x1361),f23(x1361,f23(x1362,x1362))),f23(f23(x1361,x1361),f23(x1361,f23(x1362,x1362)))),f23(f23(f23(x1361,x1361),f23(x1361,f23(x1362,x1362))),f23(x1363,x1363))),f19(x1364))+~P5(f23(f23(f23(f23(x1361,x1361),f23(x1361,f23(x1362,x1362))),f23(f23(x1361,x1361),f23(x1361,f23(x1362,x1362)))),f23(f23(f23(x1361,x1361),f23(x1361,f23(x1362,x1362))),f23(x1363,x1363))),f6(f6(a17,a17),a17))
% 0.56/0.79 [137]~P5(f23(f23(f23(f23(x1372,x1372),f23(x1372,f23(x1371,x1371))),f23(f23(x1372,x1372),f23(x1372,f23(x1371,x1371)))),f23(f23(f23(x1372,x1372),f23(x1372,f23(x1371,x1371))),f23(x1373,x1373))),x1374)+P5(f23(f23(f23(f23(x1371,x1371),f23(x1371,f23(x1372,x1372))),f23(f23(x1371,x1371),f23(x1371,f23(x1372,x1372)))),f23(f23(f23(x1371,x1371),f23(x1371,f23(x1372,x1372))),f23(x1373,x1373))),f11(x1374))+~P5(f23(f23(f23(f23(x1371,x1371),f23(x1371,f23(x1372,x1372))),f23(f23(x1371,x1371),f23(x1371,f23(x1372,x1372)))),f23(f23(f23(x1371,x1371),f23(x1371,f23(x1372,x1372))),f23(x1373,x1373))),f6(f6(a17,a17),a17))
% 0.56/0.79 [140]P5(f23(f23(x1401,x1401),f23(x1401,f23(x1402,x1402))),f7(x1403,x1404))+~P5(f23(f23(x1401,x1401),f23(x1401,f23(x1402,x1402))),f6(a17,a17))+~P5(x1402,f9(f9(f11(f6(f10(x1403,f6(f9(f9(f11(f6(f10(x1404,f6(f23(x1401,x1401),a17)),a17)))),a17)),a17)))))
% 0.56/0.79 [141]~P4(x1412,x1415,x1411)+~P5(f23(f23(x1413,x1413),f23(x1413,f23(x1414,x1414))),f9(x1415))+E(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1411,f6(f23(f23(f23(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1412,f6(f23(x1413,x1413),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1412,f6(f23(x1413,x1413),a17)),a17)))))))),f23(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1412,f6(f23(x1413,x1413),a17)),a17))))))),f23(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1412,f6(f23(x1414,x1414),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1412,f6(f23(x1414,x1414),a17)),a17)))))))))),f23(f23(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1412,f6(f23(x1413,x1413),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1412,f6(f23(x1413,x1413),a17)),a17)))))))),f23(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1412,f6(f23(x1413,x1413),a17)),a17))))))),f23(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1412,f6(f23(x1414,x1414),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1412,f6(f23(x1414,x1414),a17)),a17))))))))))),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1412,f6(f23(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1415,f6(f23(f23(f23(x1413,x1413),f23(x1413,f23(x1414,x1414))),f23(f23(x1413,x1413),f23(x1413,f23(x1414,x1414)))),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1415,f6(f23(f23(f23(x1413,x1413),f23(x1413,f23(x1414,x1414))),f23(f23(x1413,x1413),f23(x1413,f23(x1414,x1414)))),a17)),a17)))))))),a17)),a17))))))))
% 0.56/0.79 [125]~P2(x1251)+P8(x1251)+~E(f6(f9(f9(x1251)),f9(f9(x1251))),f9(x1251))+~P6(f9(f9(f11(f6(x1251,a17)))),f9(f9(x1251)))
% 0.56/0.79 [124]~P2(x1241)+P3(x1241,x1242,x1243)+~E(f9(f9(x1242)),f9(x1241))+~P6(f9(f9(f11(f6(x1241,a17)))),f9(f9(x1243)))
% 0.56/0.79 [132]~P8(x1323)+~P8(x1322)+~P3(x1321,x1322,x1323)+P4(x1321,x1322,x1323)+P5(f23(f23(f15(x1321,x1322,x1323),f15(x1321,x1322,x1323)),f23(f15(x1321,x1322,x1323),f23(f16(x1321,x1322,x1323),f16(x1321,x1322,x1323)))),f9(x1322))
% 0.56/0.79 [142]~P8(x1423)+~P8(x1422)+~P3(x1421,x1422,x1423)+P4(x1421,x1422,x1423)+~E(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1423,f6(f23(f23(f23(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1421,f6(f23(f15(x1421,x1422,x1423),f15(x1421,x1422,x1423)),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1421,f6(f23(f15(x1421,x1422,x1423),f15(x1421,x1422,x1423)),a17)),a17)))))))),f23(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1421,f6(f23(f15(x1421,x1422,x1423),f15(x1421,x1422,x1423)),a17)),a17))))))),f23(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1421,f6(f23(f16(x1421,x1422,x1423),f16(x1421,x1422,x1423)),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1421,f6(f23(f16(x1421,x1422,x1423),f16(x1421,x1422,x1423)),a17)),a17)))))))))),f23(f23(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1421,f6(f23(f15(x1421,x1422,x1423),f15(x1421,x1422,x1423)),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1421,f6(f23(f15(x1421,x1422,x1423),f15(x1421,x1422,x1423)),a17)),a17)))))))),f23(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1421,f6(f23(f15(x1421,x1422,x1423),f15(x1421,x1422,x1423)),a17)),a17))))))),f23(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1421,f6(f23(f16(x1421,x1422,x1423),f16(x1421,x1422,x1423)),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1421,f6(f23(f16(x1421,x1422,x1423),f16(x1421,x1422,x1423)),a17)),a17))))))))))),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1421,f6(f23(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1422,f6(f23(f23(f23(f15(x1421,x1422,x1423),f15(x1421,x1422,x1423)),f23(f15(x1421,x1422,x1423),f23(f16(x1421,x1422,x1423),f16(x1421,x1422,x1423)))),f23(f23(f15(x1421,x1422,x1423),f15(x1421,x1422,x1423)),f23(f15(x1421,x1422,x1423),f23(f16(x1421,x1422,x1423),f16(x1421,x1422,x1423))))),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1422,f6(f23(f23(f23(f15(x1421,x1422,x1423),f15(x1421,x1422,x1423)),f23(f15(x1421,x1422,x1423),f23(f16(x1421,x1422,x1423),f16(x1421,x1422,x1423)))),f23(f23(f15(x1421,x1422,x1423),f15(x1421,x1422,x1423)),f23(f15(x1421,x1422,x1423),f23(f16(x1421,x1422,x1423),f16(x1421,x1422,x1423))))),a17)),a17)))))))),a17)),a17))))))))
% 0.56/0.79 %EqnAxiom
% 0.56/0.79 [1]E(x11,x11)
% 0.56/0.79 [2]E(x22,x21)+~E(x21,x22)
% 0.56/0.79 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.56/0.79 [4]~E(x41,x42)+E(f23(x41,x43),f23(x42,x43))
% 0.56/0.79 [5]~E(x51,x52)+E(f23(x53,x51),f23(x53,x52))
% 0.56/0.79 [6]~E(x61,x62)+E(f9(x61),f9(x62))
% 0.56/0.79 [7]~E(x71,x72)+E(f6(x71,x73),f6(x72,x73))
% 0.56/0.79 [8]~E(x81,x82)+E(f6(x83,x81),f6(x83,x82))
% 0.56/0.79 [9]~E(x91,x92)+E(f10(x91,x93),f10(x92,x93))
% 0.56/0.79 [10]~E(x101,x102)+E(f10(x103,x101),f10(x103,x102))
% 0.56/0.79 [11]~E(x111,x112)+E(f8(x111),f8(x112))
% 0.56/0.79 [12]~E(x121,x122)+E(f7(x121,x123),f7(x122,x123))
% 0.56/0.79 [13]~E(x131,x132)+E(f7(x133,x131),f7(x133,x132))
% 0.56/0.79 [14]~E(x141,x142)+E(f11(x141),f11(x142))
% 0.56/0.79 [15]~E(x151,x152)+E(f15(x151,x153,x154),f15(x152,x153,x154))
% 0.56/0.79 [16]~E(x161,x162)+E(f15(x163,x161,x164),f15(x163,x162,x164))
% 0.56/0.79 [17]~E(x171,x172)+E(f15(x173,x174,x171),f15(x173,x174,x172))
% 0.56/0.79 [18]~E(x181,x182)+E(f14(x181,x183),f14(x182,x183))
% 0.56/0.79 [19]~E(x191,x192)+E(f14(x193,x191),f14(x193,x192))
% 0.56/0.79 [20]~E(x201,x202)+E(f19(x201),f19(x202))
% 0.56/0.79 [21]~E(x211,x212)+E(f16(x211,x213,x214),f16(x212,x213,x214))
% 0.56/0.79 [22]~E(x221,x222)+E(f16(x223,x221,x224),f16(x223,x222,x224))
% 0.56/0.79 [23]~E(x231,x232)+E(f16(x233,x234,x231),f16(x233,x234,x232))
% 0.56/0.79 [24]~E(x241,x242)+E(f20(x241),f20(x242))
% 0.56/0.79 [25]~E(x251,x252)+E(f22(x251),f22(x252))
% 0.56/0.79 [26]~E(x261,x262)+E(f12(x261),f12(x262))
% 0.56/0.79 [27]~E(x271,x272)+E(f3(x271),f3(x272))
% 0.56/0.79 [28]~P1(x281)+P1(x282)+~E(x281,x282)
% 0.56/0.79 [29]~P2(x291)+P2(x292)+~E(x291,x292)
% 0.56/0.79 [30]P5(x302,x303)+~E(x301,x302)+~P5(x301,x303)
% 0.56/0.79 [31]P5(x313,x312)+~E(x311,x312)+~P5(x313,x311)
% 0.56/0.80 [32]P3(x322,x323,x324)+~E(x321,x322)+~P3(x321,x323,x324)
% 0.56/0.80 [33]P3(x333,x332,x334)+~E(x331,x332)+~P3(x333,x331,x334)
% 0.56/0.80 [34]P3(x343,x344,x342)+~E(x341,x342)+~P3(x343,x344,x341)
% 0.56/0.80 [35]P6(x352,x353)+~E(x351,x352)+~P6(x351,x353)
% 0.56/0.80 [36]P6(x363,x362)+~E(x361,x362)+~P6(x363,x361)
% 0.56/0.80 [37]P4(x372,x373,x374)+~E(x371,x372)+~P4(x371,x373,x374)
% 0.56/0.80 [38]P4(x383,x382,x384)+~E(x381,x382)+~P4(x383,x381,x384)
% 0.56/0.80 [39]P4(x393,x394,x392)+~E(x391,x392)+~P4(x393,x394,x391)
% 0.56/0.80 [40]~P7(x401)+P7(x402)+~E(x401,x402)
% 0.56/0.80 [41]~P8(x411)+P8(x412)+~E(x411,x412)
% 0.56/0.80 [42]~P9(x421)+P9(x422)+~E(x421,x422)
% 0.56/0.80
% 0.56/0.80 %-------------------------------------------
% 0.56/0.80 cnf(149,plain,
% 0.56/0.80 (P5(f20(f23(a24,a25)),f23(a24,a25))),
% 0.56/0.80 inference(scs_inference,[],[63,74,76])).
% 0.56/0.80 cnf(151,plain,
% 0.56/0.80 (E(f10(f8(x1511),x1511),a4)),
% 0.56/0.80 inference(scs_inference,[],[63,67,74,76,77])).
% 0.56/0.80 cnf(152,plain,
% 0.56/0.80 (~P5(x1521,f10(f8(x1522),x1522))),
% 0.56/0.80 inference(rename_variables,[],[67])).
% 0.56/0.80 cnf(154,plain,
% 0.56/0.80 (E(f10(x1541,f6(x1542,x1543)),f10(f6(x1542,x1543),x1541))),
% 0.56/0.80 inference(scs_inference,[],[63,57,67,74,76,77,2])).
% 0.56/0.80 cnf(157,plain,
% 0.56/0.80 (P6(f10(f8(x1571),x1571),x1572)),
% 0.56/0.80 inference(scs_inference,[],[63,57,67,152,74,76,77,2,70,82])).
% 0.56/0.80 cnf(158,plain,
% 0.56/0.80 (~P5(x1581,f10(f8(x1582),x1582))),
% 0.56/0.80 inference(rename_variables,[],[67])).
% 0.56/0.80 cnf(160,plain,
% 0.56/0.80 (~P5(x1601,f9(f8(f6(f23(x1601,x1601),a17))))),
% 0.56/0.80 inference(scs_inference,[],[63,57,67,152,74,76,77,2,70,82,106])).
% 0.56/0.80 cnf(162,plain,
% 0.56/0.80 (~P1(a4)),
% 0.56/0.80 inference(scs_inference,[],[63,66,57,67,152,74,76,77,2,70,82,106,73])).
% 0.56/0.80 cnf(163,plain,
% 0.56/0.80 (~P5(x1631,a4)),
% 0.56/0.80 inference(rename_variables,[],[66])).
% 0.56/0.80 cnf(165,plain,
% 0.56/0.80 (~P5(f23(f23(f23(f23(x1651,x1651),f23(x1651,f23(x1652,x1652))),f23(f23(x1651,x1651),f23(x1651,f23(x1652,x1652)))),f23(f23(f23(x1651,x1651),f23(x1651,f23(x1652,x1652))),f23(x1653,x1653))),f19(a4))),
% 0.56/0.80 inference(scs_inference,[],[63,66,163,57,67,152,74,76,77,2,70,82,106,73,134])).
% 0.56/0.80 cnf(166,plain,
% 0.56/0.80 (~P5(x1661,a4)),
% 0.56/0.80 inference(rename_variables,[],[66])).
% 0.56/0.80 cnf(169,plain,
% 0.56/0.80 (~P5(x1691,a4)),
% 0.56/0.80 inference(rename_variables,[],[66])).
% 0.56/0.80 cnf(172,plain,
% 0.56/0.80 (~P5(x1721,f10(f8(x1722),x1722))),
% 0.56/0.80 inference(rename_variables,[],[67])).
% 0.56/0.80 cnf(173,plain,
% 0.56/0.80 (~P5(x1731,a4)),
% 0.56/0.80 inference(rename_variables,[],[66])).
% 0.56/0.80 cnf(175,plain,
% 0.56/0.80 (~E(a4,f23(a25,a24))),
% 0.56/0.80 inference(scs_inference,[],[63,66,163,166,169,50,57,67,152,158,74,76,77,2,70,82,106,73,134,135,94,3])).
% 0.56/0.80 cnf(177,plain,
% 0.56/0.80 (~E(a4,a24)),
% 0.56/0.80 inference(scs_inference,[],[63,64,66,163,166,169,50,45,57,67,152,158,74,76,77,2,70,82,106,73,134,135,94,3,30])).
% 0.56/0.80 cnf(178,plain,
% 0.56/0.80 (~E(a17,a4)),
% 0.56/0.80 inference(scs_inference,[],[63,64,66,163,166,169,173,50,45,57,67,152,158,74,76,77,2,70,82,106,73,134,135,94,3,30,31])).
% 0.56/0.80 cnf(181,plain,
% 0.56/0.80 (~E(f10(f8(x1811),x1811),f23(a24,a25))),
% 0.56/0.80 inference(scs_inference,[],[63,64,66,163,166,169,173,50,45,57,67,152,158,74,76,77,2,70,82,106,73,134,135,94,3,30,31,28,35])).
% 0.56/0.80 cnf(182,plain,
% 0.56/0.80 (~P5(a4,f8(a17))),
% 0.56/0.80 inference(scs_inference,[],[63,64,66,163,166,169,173,50,45,57,67,152,158,172,74,76,77,2,70,82,106,73,134,135,94,3,30,31,28,35,95])).
% 0.56/0.80 cnf(204,plain,
% 0.56/0.80 (~P5(f23(f23(f23(f23(x2041,x2041),f23(x2041,f23(x2042,x2042))),f23(f23(x2041,x2041),f23(x2041,f23(x2042,x2042)))),f23(f23(f23(x2041,x2041),f23(x2041,f23(x2042,x2042))),f23(x2043,x2043))),f11(f19(a4)))),
% 0.56/0.80 inference(scs_inference,[],[178,165,74,135])).
% 0.56/0.80 cnf(206,plain,
% 0.56/0.80 (P5(f20(a17),a17)),
% 0.56/0.80 inference(scs_inference,[],[178,165,74,135,76])).
% 0.56/0.80 cnf(211,plain,
% 0.56/0.80 (~P5(x2111,f9(f8(f6(f23(x2111,x2111),a17))))),
% 0.56/0.80 inference(rename_variables,[],[160])).
% 0.56/0.80 cnf(216,plain,
% 0.56/0.80 (P5(f20(f23(a24,a25)),a17)),
% 0.56/0.80 inference(scs_inference,[],[149,178,160,165,60,47,74,135,76,134,73,70,2,86])).
% 0.56/0.80 cnf(229,plain,
% 0.56/0.80 (~P1(f10(f8(x2291),x2291))),
% 0.56/0.80 inference(scs_inference,[],[63,65,48,149,178,151,175,160,211,165,46,162,60,47,67,74,135,76,134,73,70,2,86,30,3,81,95,31,28])).
% 0.56/0.80 cnf(230,plain,
% 0.56/0.80 (~E(f23(a25,a24),a4)),
% 0.56/0.80 inference(scs_inference,[],[63,65,48,149,178,151,175,160,211,165,46,162,60,47,67,74,135,76,134,73,70,2,86,30,3,81,95,31,28,71])).
% 0.56/0.80 cnf(261,plain,
% 0.56/0.80 (~E(a24,a4)),
% 0.56/0.80 inference(scs_inference,[],[64,48,216,177,154,229,230,160,182,204,61,57,135,76,134,73,2,81,31,3,30,28,71])).
% 0.56/0.80 cnf(264,plain,
% 0.56/0.80 (E(f20(f23(a24,a25)),a25)),
% 0.56/0.80 inference(scs_inference,[],[64,48,151,149,216,177,154,229,230,160,182,204,61,57,135,76,134,73,2,81,31,3,30,28,71,42,90])).
% 0.56/0.80 cnf(273,plain,
% 0.56/0.80 (~P5(f23(f23(f23(f23(x2731,x2731),f23(x2731,f23(x2732,x2732))),f23(f23(x2731,x2731),f23(x2731,f23(x2732,x2732)))),f23(f23(f23(x2731,x2731),f23(x2731,f23(x2732,x2732))),f23(x2733,x2733))),f11(f10(f8(x2734),x2734)))),
% 0.56/0.80 inference(scs_inference,[],[67,135])).
% 0.56/0.80 cnf(274,plain,
% 0.56/0.80 (~P5(x2741,f10(f8(x2742),x2742))),
% 0.56/0.80 inference(rename_variables,[],[67])).
% 0.56/0.80 cnf(287,plain,
% 0.56/0.80 (P5(a25,f23(a24,a25))),
% 0.56/0.80 inference(scs_inference,[],[149,264,206,157,181,261,160,67,274,135,76,134,2,81,31,30])).
% 0.56/0.80 cnf(298,plain,
% 0.56/0.80 (~P5(f23(f23(f23(f23(x2981,x2981),f23(x2981,f23(x2982,x2982))),f23(f23(x2981,x2981),f23(x2981,f23(x2982,x2982)))),f23(f23(f23(x2981,x2981),f23(x2981,f23(x2982,x2982))),f23(x2983,x2983))),f11(f11(f10(f8(x2984),x2984))))),
% 0.56/0.80 inference(scs_inference,[],[273,135])).
% 0.56/0.80 cnf(346,plain,
% 0.56/0.80 ($false),
% 0.56/0.80 inference(scs_inference,[],[65,264,287,216,298,135,134,31,30]),
% 0.56/0.80 ['proof']).
% 0.56/0.80 % SZS output end Proof
% 0.56/0.80 % Total time :0.140000s
%------------------------------------------------------------------------------