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