%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET057-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 : n017.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:21 EDT 2024
% Result : Unsatisfiable 0.52s 0.62s
% Output : CNFRefutation 0.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SET057-7 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n017.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 16:05:08 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.48/0.56 start to proof:theBenchmark
% 0.52/0.62 %-------------------------------------------
% 0.52/0.62 % File :CSE---1.7
% 0.52/0.62 % Problem :theBenchmark
% 0.52/0.62 % Transform :cnf
% 0.52/0.62 % Format :tptp:raw
% 0.52/0.62 % Command :java -jar mcs_scs.jar %d %s
% 0.52/0.62
% 0.52/0.62 % Result :Theorem 0.010000s
% 0.52/0.62 % Output :CNFRefutation 0.010000s
% 0.52/0.62 %-------------------------------------------
% 0.52/0.62 %--------------------------------------------------------------------------
% 0.52/0.62 % File : SET057-7 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.52/0.62 % Domain : Set Theory
% 0.52/0.62 % Problem : Expanded equality definition
% 0.52/0.62 % Version : [Qua92] axioms : Augmented.
% 0.52/0.62 % English :
% 0.52/0.62
% 0.52/0.62 % Refs : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 0.52/0.62 % Source : [Quaife]
% 0.52/0.62 % Names : EQ2.2 [Qua92]
% 0.52/0.62
% 0.52/0.62 % Status : Unsatisfiable
% 0.52/0.62 % 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.3.0, 0.00 v6.2.0, 0.10 v6.1.0, 0.00 v5.5.0, 0.15 v5.4.0, 0.20 v5.3.0, 0.11 v5.2.0, 0.12 v5.0.0, 0.07 v4.1.0, 0.08 v4.0.1, 0.09 v4.0.0, 0.18 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.08 v2.6.0, 0.00 v2.1.0
% 0.52/0.62 % Syntax : Number of clauses : 100 ( 33 unt; 8 nHn; 70 RR)
% 0.52/0.62 % Number of literals : 196 ( 40 equ; 92 neg)
% 0.52/0.62 % Maximal clause size : 5 ( 1 avg)
% 0.52/0.62 % Maximal term depth : 6 ( 1 avg)
% 0.52/0.62 % Number of predicates : 10 ( 9 usr; 0 prp; 1-3 aty)
% 0.52/0.62 % Number of functors : 40 ( 40 usr; 10 con; 0-3 aty)
% 0.52/0.62 % Number of variables : 196 ( 35 sgn)
% 0.52/0.62 % SPC : CNF_UNS_RFO_SEQ_NHN
% 0.52/0.62
% 0.52/0.62 % Comments : Preceding lemmas are added.
% 0.52/0.62 % Bugfixes : v2.1.0 - Bugfix in SET004-0.ax.
% 0.52/0.62 %--------------------------------------------------------------------------
% 0.52/0.62 %----Include von Neuman-Bernays-Godel set theory axioms
% 0.52/0.62 include('Axioms/SET004-0.ax').
% 0.52/0.62 %--------------------------------------------------------------------------
% 0.52/0.62 %----Corollaries to Unordered pair axiom. Not in paper, but in email.
% 0.52/0.62 cnf(corollary_1_to_unordered_pair,axiom,
% 0.52/0.62 ( ~ member(ordered_pair(X,Y),cross_product(U,V))
% 0.52/0.62 | member(X,unordered_pair(X,Y)) ) ).
% 0.52/0.62
% 0.52/0.62 cnf(corollary_2_to_unordered_pair,axiom,
% 0.52/0.62 ( ~ member(ordered_pair(X,Y),cross_product(U,V))
% 0.52/0.62 | member(Y,unordered_pair(X,Y)) ) ).
% 0.52/0.62
% 0.52/0.62 %----Corollaries to Cartesian product axiom.
% 0.52/0.62 cnf(corollary_1_to_cartesian_product,axiom,
% 0.52/0.62 ( ~ member(ordered_pair(U,V),cross_product(X,Y))
% 0.52/0.62 | member(U,universal_class) ) ).
% 0.52/0.62
% 0.52/0.62 cnf(corollary_2_to_cartesian_product,axiom,
% 0.52/0.62 ( ~ member(ordered_pair(U,V),cross_product(X,Y))
% 0.52/0.62 | member(V,universal_class) ) ).
% 0.52/0.62
% 0.52/0.62 %---- PARTIAL ORDER.
% 0.52/0.62 %----(PO1): reflexive.
% 0.52/0.62 cnf(subclass_is_reflexive,axiom,
% 0.52/0.62 subclass(X,X) ).
% 0.52/0.62
% 0.52/0.62 %----(PO2): antisymmetry is part of A-3.
% 0.52/0.62 %----(x < y), (y < x) --> (x = y).
% 0.52/0.62
% 0.52/0.62 %----(PO3): transitivity.
% 0.52/0.62 cnf(transitivity_of_subclass,axiom,
% 0.52/0.62 ( ~ subclass(X,Y)
% 0.52/0.62 | ~ subclass(Y,Z)
% 0.52/0.62 | subclass(X,Z) ) ).
% 0.52/0.62
% 0.52/0.62 %---- EQUALITY.
% 0.52/0.62 %----(EQ1): equality axiom.
% 0.52/0.62 %----a:x:(x = x).
% 0.52/0.62 %----This is always an axiom in the TPTP presentation.
% 0.52/0.62
% 0.52/0.62 cnf(prove_equality2_1,negated_conjecture,
% 0.52/0.62 member(not_subclass_element(x,y),y) ).
% 0.52/0.62
% 0.52/0.62 cnf(prove_equality2_2,negated_conjecture,
% 0.52/0.62 x != y ).
% 0.52/0.62
% 0.52/0.62 cnf(prove_equality2_3,negated_conjecture,
% 0.52/0.62 ~ member(not_subclass_element(y,x),y) ).
% 0.52/0.62
% 0.52/0.62 %--------------------------------------------------------------------------
% 0.52/0.62 %-------------------------------------------
% 0.52/0.62 % Proof found
% 0.52/0.62 % SZS status Theorem for theBenchmark
% 0.52/0.62 % SZS output start Proof
% 0.52/0.62 %ClaNum:127(EqnAxiom:42)
% 0.52/0.62 %VarNum:762(SingletonVarNum:170)
% 0.52/0.62 %MaxLitNum:5
% 0.52/0.62 %MaxfuncDepth:24
% 0.52/0.62 %SharedTerms:36
% 0.52/0.62 %goalClause: 50 59 60
% 0.52/0.62 %singleGoalClaCount:3
% 0.52/0.62 [43]P1(a1)
% 0.52/0.62 [44]P2(a2)
% 0.52/0.62 [45]P5(a1,a17)
% 0.52/0.62 [59]~E(a25,a23)
% 0.52/0.62 [48]P6(a4,f5(a17,a17))
% 0.52/0.62 [49]P6(a18,f5(a17,a17))
% 0.52/0.62 [50]P5(f9(a23,a25),a25)
% 0.52/0.62 [60]~P5(f9(a25,a23),a25)
% 0.52/0.62 [56]E(f10(f8(f11(f5(a21,a17))),a21),a13)
% 0.52/0.62 [57]E(f10(f5(a17,a17),f10(f5(a17,a17),f7(f6(f7(a4),f8(f11(f5(a4,a17))))))),a21)
% 0.52/0.62 [46]P6(x461,a17)
% 0.52/0.62 [47]P6(x471,x471)
% 0.52/0.62 [54]P6(f19(x541),f5(f5(a17,a17),a17))
% 0.52/0.62 [55]P6(f11(x551),f5(f5(a17,a17),a17))
% 0.52/0.62 [58]E(f10(f8(x581),f7(f8(f10(f6(f8(f11(f5(a4,a17))),x581),a13)))),f3(x581))
% 0.52/0.62 [51]P5(f24(x511,x512),a17)
% 0.52/0.62 [52]P6(f6(x521,x522),f5(a17,a17))
% 0.52/0.62 [53]E(f10(f5(x531,x532),x533),f10(x533,f5(x531,x532)))
% 0.52/0.62 [61]~P7(x611)+P2(x611)
% 0.52/0.62 [62]~P8(x621)+P2(x621)
% 0.52/0.62 [65]~P1(x651)+P6(a1,x651)
% 0.52/0.62 [66]~P1(x661)+P5(a16,x661)
% 0.52/0.62 [68]P5(f20(x681),x681)+E(x681,a16)
% 0.52/0.62 [69]~P2(x691)+P6(x691,f5(a17,a17))
% 0.52/0.62 [67]E(x671,a16)+E(f10(x671,f20(x671)),a16)
% 0.52/0.62 [78]~P8(x781)+E(f5(f8(f8(x781)),f8(f8(x781))),f8(x781))
% 0.52/0.62 [88]~P7(x881)+P2(f8(f11(f5(x881,a17))))
% 0.52/0.62 [92]~P5(x921,a17)+P5(f8(f10(a4,f5(a17,x921))),a17)
% 0.52/0.62 [94]~P9(x941)+P6(f6(x941,f8(f11(f5(x941,a17)))),a13)
% 0.52/0.62 [95]~P2(x951)+P6(f6(x951,f8(f11(f5(x951,a17)))),a13)
% 0.52/0.62 [96]~P8(x961)+P6(f8(f8(f11(f5(x961,a17)))),f8(f8(x961)))
% 0.52/0.62 [101]P9(x1011)+~P6(f6(x1011,f8(f11(f5(x1011,a17)))),a13)
% 0.52/0.62 [114]~P1(x1141)+P6(f8(f8(f11(f5(f10(a18,f5(x1141,a17)),a17)))),x1141)
% 0.52/0.62 [118]~P5(x1181,a17)+P5(f7(f8(f8(f11(f5(f10(a4,f5(f7(x1181),a17)),a17))))),a17)
% 0.52/0.62 [63]~E(x632,x631)+P6(x631,x632)
% 0.52/0.62 [64]~E(x641,x642)+P6(x641,x642)
% 0.52/0.62 [71]P6(x711,x712)+P5(f9(x711,x712),x711)
% 0.52/0.62 [72]~P5(x721,x722)+~P5(x721,f7(x722))
% 0.52/0.62 [76]~P5(x761,a17)+P5(x761,f24(x762,x761))
% 0.52/0.62 [77]~P5(x771,a17)+P5(x771,f24(x771,x772))
% 0.52/0.62 [82]P6(x821,x822)+~P5(f9(x821,x822),x822)
% 0.52/0.62 [91]~P5(x912,f8(x911))+~E(f10(x911,f5(f24(x912,x912),a17)),a16)
% 0.52/0.62 [100]P5(x1001,x1002)+~P5(f24(f24(x1001,x1001),f24(x1001,f24(x1002,x1002))),a4)
% 0.52/0.62 [111]~P5(f24(f24(x1111,x1111),f24(x1111,f24(x1112,x1112))),a18)+E(f7(f10(f7(x1111),f7(f24(x1111,x1111)))),x1112)
% 0.52/0.62 [84]P2(x841)+~P3(x841,x842,x843)
% 0.52/0.62 [85]P8(x851)+~P4(x852,x853,x851)
% 0.52/0.62 [86]P8(x861)+~P4(x862,x861,x863)
% 0.52/0.62 [90]~P4(x901,x902,x903)+P3(x901,x902,x903)
% 0.52/0.62 [80]P5(x801,x802)+~P5(x801,f10(x803,x802))
% 0.52/0.62 [81]P5(x811,x812)+~P5(x811,f10(x812,x813))
% 0.52/0.62 [87]~P3(x872,x871,x873)+E(f8(f8(x871)),f8(x872))
% 0.52/0.62 [97]~P5(x971,f5(x972,x973))+E(f24(f24(f12(x971),f12(x971)),f24(f12(x971),f24(f22(x971),f22(x971)))),x971)
% 0.52/0.62 [99]~P3(x991,x993,x992)+P6(f8(f8(f11(f5(x991,a17)))),f8(f8(x992)))
% 0.52/0.62 [102]P5(x1021,a17)+~P5(f24(f24(x1022,x1022),f24(x1022,f24(x1021,x1021))),f5(x1023,x1024))
% 0.52/0.62 [103]P5(x1031,a17)+~P5(f24(f24(x1031,x1031),f24(x1031,f24(x1032,x1032))),f5(x1033,x1034))
% 0.52/0.62 [104]P5(x1041,x1042)+~P5(f24(f24(x1043,x1043),f24(x1043,f24(x1041,x1041))),f5(x1044,x1042))
% 0.52/0.62 [105]P5(x1051,x1052)+~P5(f24(f24(x1051,x1051),f24(x1051,f24(x1053,x1053))),f5(x1052,x1054))
% 0.52/0.62 [107]P5(x1071,f24(x1072,x1071))+~P5(f24(f24(x1072,x1072),f24(x1072,f24(x1071,x1071))),f5(x1073,x1074))
% 0.52/0.62 [108]P5(x1081,f24(x1081,x1082))+~P5(f24(f24(x1081,x1081),f24(x1081,f24(x1082,x1082))),f5(x1083,x1084))
% 0.52/0.62 [119]~P5(f24(f24(f24(f24(x1193,x1193),f24(x1193,f24(x1191,x1191))),f24(f24(x1193,x1193),f24(x1193,f24(x1191,x1191)))),f24(f24(f24(x1193,x1193),f24(x1193,f24(x1191,x1191))),f24(x1192,x1192))),f19(x1194))+P5(f24(f24(f24(f24(x1191,x1191),f24(x1191,f24(x1192,x1192))),f24(f24(x1191,x1191),f24(x1191,f24(x1192,x1192)))),f24(f24(f24(x1191,x1191),f24(x1191,f24(x1192,x1192))),f24(x1193,x1193))),x1194)
% 0.52/0.62 [120]~P5(f24(f24(f24(f24(x1202,x1202),f24(x1202,f24(x1201,x1201))),f24(f24(x1202,x1202),f24(x1202,f24(x1201,x1201)))),f24(f24(f24(x1202,x1202),f24(x1202,f24(x1201,x1201))),f24(x1203,x1203))),f11(x1204))+P5(f24(f24(f24(f24(x1201,x1201),f24(x1201,f24(x1202,x1202))),f24(f24(x1201,x1201),f24(x1201,f24(x1202,x1202)))),f24(f24(f24(x1201,x1201),f24(x1201,f24(x1202,x1202))),f24(x1203,x1203))),x1204)
% 0.52/0.62 [124]~P5(f24(f24(x1244,x1244),f24(x1244,f24(x1241,x1241))),f6(x1242,x1243))+P5(x1241,f8(f8(f11(f5(f10(x1242,f5(f8(f8(f11(f5(f10(x1243,f5(f24(x1244,x1244),a17)),a17)))),a17)),a17)))))
% 0.52/0.62 [93]~P2(x931)+P7(x931)+~P2(f8(f11(f5(x931,a17))))
% 0.52/0.62 [106]P2(x1061)+~P6(x1061,f5(a17,a17))+~P6(f6(x1061,f8(f11(f5(x1061,a17)))),a13)
% 0.52/0.62 [116]P1(x1161)+~P5(a16,x1161)+~P6(f8(f8(f11(f5(f10(a18,f5(x1161,a17)),a17)))),x1161)
% 0.52/0.62 [123]~P5(x1231,a17)+E(x1231,a16)+P5(f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(a2,f5(f24(x1231,x1231),a17)),a17))))))),x1231)
% 0.52/0.62 [70]~P6(x702,x701)+~P6(x701,x702)+E(x701,x702)
% 0.52/0.62 [73]P5(x731,x732)+P5(x731,f7(x732))+~P5(x731,a17)
% 0.52/0.62 [89]P5(x892,f8(x891))+~P5(x892,a17)+E(f10(x891,f5(f24(x892,x892),a17)),a16)
% 0.52/0.62 [112]~P5(x1121,x1122)+~P5(f24(f24(x1121,x1121),f24(x1121,f24(x1122,x1122))),f5(a17,a17))+P5(f24(f24(x1121,x1121),f24(x1121,f24(x1122,x1122))),a4)
% 0.52/0.62 [113]~P5(f24(f24(x1131,x1131),f24(x1131,f24(x1132,x1132))),f5(a17,a17))+~E(f7(f10(f7(x1131),f7(f24(x1131,x1131)))),x1132)+P5(f24(f24(x1131,x1131),f24(x1131,f24(x1132,x1132))),a18)
% 0.52/0.62 [115]~P2(x1151)+~P5(x1152,a17)+P5(f8(f8(f11(f5(f10(x1151,f5(x1152,a17)),a17)))),a17)
% 0.52/0.62 [74]~P6(x741,x743)+P6(x741,x742)+~P6(x743,x742)
% 0.52/0.62 [75]~P5(x751,x753)+P5(x751,x752)+~P6(x753,x752)
% 0.52/0.62 [79]E(x791,x792)+E(x791,x793)+~P5(x791,f24(x793,x792))
% 0.52/0.62 [83]~P5(x831,x833)+~P5(x831,x832)+P5(x831,f10(x832,x833))
% 0.52/0.62 [98]~P5(x982,x984)+~P5(x981,x983)+P5(f24(f24(x981,x981),f24(x981,f24(x982,x982))),f5(x983,x984))
% 0.52/0.63 [121]~P5(f24(f24(f24(f24(x1212,x1212),f24(x1212,f24(x1213,x1213))),f24(f24(x1212,x1212),f24(x1212,f24(x1213,x1213)))),f24(f24(f24(x1212,x1212),f24(x1212,f24(x1213,x1213))),f24(x1211,x1211))),x1214)+P5(f24(f24(f24(f24(x1211,x1211),f24(x1211,f24(x1212,x1212))),f24(f24(x1211,x1211),f24(x1211,f24(x1212,x1212)))),f24(f24(f24(x1211,x1211),f24(x1211,f24(x1212,x1212))),f24(x1213,x1213))),f19(x1214))+~P5(f24(f24(f24(f24(x1211,x1211),f24(x1211,f24(x1212,x1212))),f24(f24(x1211,x1211),f24(x1211,f24(x1212,x1212)))),f24(f24(f24(x1211,x1211),f24(x1211,f24(x1212,x1212))),f24(x1213,x1213))),f5(f5(a17,a17),a17))
% 0.52/0.63 [122]~P5(f24(f24(f24(f24(x1222,x1222),f24(x1222,f24(x1221,x1221))),f24(f24(x1222,x1222),f24(x1222,f24(x1221,x1221)))),f24(f24(f24(x1222,x1222),f24(x1222,f24(x1221,x1221))),f24(x1223,x1223))),x1224)+P5(f24(f24(f24(f24(x1221,x1221),f24(x1221,f24(x1222,x1222))),f24(f24(x1221,x1221),f24(x1221,f24(x1222,x1222)))),f24(f24(f24(x1221,x1221),f24(x1221,f24(x1222,x1222))),f24(x1223,x1223))),f11(x1224))+~P5(f24(f24(f24(f24(x1221,x1221),f24(x1221,f24(x1222,x1222))),f24(f24(x1221,x1221),f24(x1221,f24(x1222,x1222)))),f24(f24(f24(x1221,x1221),f24(x1221,f24(x1222,x1222))),f24(x1223,x1223))),f5(f5(a17,a17),a17))
% 0.52/0.63 [125]P5(f24(f24(x1251,x1251),f24(x1251,f24(x1252,x1252))),f6(x1253,x1254))+~P5(f24(f24(x1251,x1251),f24(x1251,f24(x1252,x1252))),f5(a17,a17))+~P5(x1252,f8(f8(f11(f5(f10(x1253,f5(f8(f8(f11(f5(f10(x1254,f5(f24(x1251,x1251),a17)),a17)))),a17)),a17)))))
% 0.52/0.63 [126]~P4(x1262,x1265,x1261)+~P5(f24(f24(x1263,x1263),f24(x1263,f24(x1264,x1264))),f8(x1265))+E(f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1261,f5(f24(f24(f24(f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1262,f5(f24(x1263,x1263),a17)),a17))))))),f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1262,f5(f24(x1263,x1263),a17)),a17)))))))),f24(f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1262,f5(f24(x1263,x1263),a17)),a17))))))),f24(f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1262,f5(f24(x1264,x1264),a17)),a17))))))),f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1262,f5(f24(x1264,x1264),a17)),a17)))))))))),f24(f24(f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1262,f5(f24(x1263,x1263),a17)),a17))))))),f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1262,f5(f24(x1263,x1263),a17)),a17)))))))),f24(f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1262,f5(f24(x1263,x1263),a17)),a17))))))),f24(f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1262,f5(f24(x1264,x1264),a17)),a17))))))),f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1262,f5(f24(x1264,x1264),a17)),a17))))))))))),a17)),a17))))))),f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1262,f5(f24(f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1265,f5(f24(f24(f24(x1263,x1263),f24(x1263,f24(x1264,x1264))),f24(f24(x1263,x1263),f24(x1263,f24(x1264,x1264)))),a17)),a17))))))),f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1265,f5(f24(f24(f24(x1263,x1263),f24(x1263,f24(x1264,x1264))),f24(f24(x1263,x1263),f24(x1263,f24(x1264,x1264)))),a17)),a17)))))))),a17)),a17))))))))
% 0.52/0.63 [110]~P2(x1101)+P8(x1101)+~E(f5(f8(f8(x1101)),f8(f8(x1101))),f8(x1101))+~P6(f8(f8(f11(f5(x1101,a17)))),f8(f8(x1101)))
% 0.52/0.63 [109]~P2(x1091)+P3(x1091,x1092,x1093)+~E(f8(f8(x1092)),f8(x1091))+~P6(f8(f8(f11(f5(x1091,a17)))),f8(f8(x1093)))
% 0.52/0.63 [117]~P8(x1173)+~P8(x1172)+~P3(x1171,x1172,x1173)+P4(x1171,x1172,x1173)+P5(f24(f24(f14(x1171,x1172,x1173),f14(x1171,x1172,x1173)),f24(f14(x1171,x1172,x1173),f24(f15(x1171,x1172,x1173),f15(x1171,x1172,x1173)))),f8(x1172))
% 0.52/0.63 [127]~P8(x1273)+~P8(x1272)+~P3(x1271,x1272,x1273)+P4(x1271,x1272,x1273)+~E(f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1273,f5(f24(f24(f24(f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1271,f5(f24(f14(x1271,x1272,x1273),f14(x1271,x1272,x1273)),a17)),a17))))))),f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1271,f5(f24(f14(x1271,x1272,x1273),f14(x1271,x1272,x1273)),a17)),a17)))))))),f24(f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1271,f5(f24(f14(x1271,x1272,x1273),f14(x1271,x1272,x1273)),a17)),a17))))))),f24(f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1271,f5(f24(f15(x1271,x1272,x1273),f15(x1271,x1272,x1273)),a17)),a17))))))),f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1271,f5(f24(f15(x1271,x1272,x1273),f15(x1271,x1272,x1273)),a17)),a17)))))))))),f24(f24(f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1271,f5(f24(f14(x1271,x1272,x1273),f14(x1271,x1272,x1273)),a17)),a17))))))),f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1271,f5(f24(f14(x1271,x1272,x1273),f14(x1271,x1272,x1273)),a17)),a17)))))))),f24(f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1271,f5(f24(f14(x1271,x1272,x1273),f14(x1271,x1272,x1273)),a17)),a17))))))),f24(f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1271,f5(f24(f15(x1271,x1272,x1273),f15(x1271,x1272,x1273)),a17)),a17))))))),f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1271,f5(f24(f15(x1271,x1272,x1273),f15(x1271,x1272,x1273)),a17)),a17))))))))))),a17)),a17))))))),f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1271,f5(f24(f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1272,f5(f24(f24(f24(f14(x1271,x1272,x1273),f14(x1271,x1272,x1273)),f24(f14(x1271,x1272,x1273),f24(f15(x1271,x1272,x1273),f15(x1271,x1272,x1273)))),f24(f24(f14(x1271,x1272,x1273),f14(x1271,x1272,x1273)),f24(f14(x1271,x1272,x1273),f24(f15(x1271,x1272,x1273),f15(x1271,x1272,x1273))))),a17)),a17))))))),f8(f10(a4,f5(a17,f8(f8(f11(f5(f10(x1272,f5(f24(f24(f24(f14(x1271,x1272,x1273),f14(x1271,x1272,x1273)),f24(f14(x1271,x1272,x1273),f24(f15(x1271,x1272,x1273),f15(x1271,x1272,x1273)))),f24(f24(f14(x1271,x1272,x1273),f14(x1271,x1272,x1273)),f24(f14(x1271,x1272,x1273),f24(f15(x1271,x1272,x1273),f15(x1271,x1272,x1273))))),a17)),a17)))))))),a17)),a17))))))))
% 0.52/0.63 %EqnAxiom
% 0.52/0.63 [1]E(x11,x11)
% 0.52/0.63 [2]E(x22,x21)+~E(x21,x22)
% 0.52/0.63 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.52/0.63 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43))
% 0.52/0.63 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52))
% 0.52/0.63 [6]~E(x61,x62)+E(f8(x61),f8(x62))
% 0.52/0.63 [7]~E(x71,x72)+E(f9(x71,x73),f9(x72,x73))
% 0.52/0.63 [8]~E(x81,x82)+E(f9(x83,x81),f9(x83,x82))
% 0.52/0.63 [9]~E(x91,x92)+E(f24(x91,x93),f24(x92,x93))
% 0.52/0.63 [10]~E(x101,x102)+E(f24(x103,x101),f24(x103,x102))
% 0.52/0.63 [11]~E(x111,x112)+E(f6(x111,x113),f6(x112,x113))
% 0.52/0.63 [12]~E(x121,x122)+E(f6(x123,x121),f6(x123,x122))
% 0.52/0.63 [13]~E(x131,x132)+E(f10(x131,x133),f10(x132,x133))
% 0.52/0.63 [14]~E(x141,x142)+E(f10(x143,x141),f10(x143,x142))
% 0.52/0.63 [15]~E(x151,x152)+E(f11(x151),f11(x152))
% 0.52/0.63 [16]~E(x161,x162)+E(f7(x161),f7(x162))
% 0.52/0.63 [17]~E(x171,x172)+E(f15(x171,x173,x174),f15(x172,x173,x174))
% 0.52/0.63 [18]~E(x181,x182)+E(f15(x183,x181,x184),f15(x183,x182,x184))
% 0.52/0.63 [19]~E(x191,x192)+E(f15(x193,x194,x191),f15(x193,x194,x192))
% 0.52/0.63 [20]~E(x201,x202)+E(f14(x201,x203,x204),f14(x202,x203,x204))
% 0.52/0.63 [21]~E(x211,x212)+E(f14(x213,x211,x214),f14(x213,x212,x214))
% 0.52/0.63 [22]~E(x221,x222)+E(f14(x223,x224,x221),f14(x223,x224,x222))
% 0.52/0.63 [23]~E(x231,x232)+E(f19(x231),f19(x232))
% 0.52/0.63 [24]~E(x241,x242)+E(f22(x241),f22(x242))
% 0.52/0.63 [25]~E(x251,x252)+E(f20(x251),f20(x252))
% 0.52/0.63 [26]~E(x261,x262)+E(f12(x261),f12(x262))
% 0.52/0.63 [27]~E(x271,x272)+E(f3(x271),f3(x272))
% 0.52/0.63 [28]~P1(x281)+P1(x282)+~E(x281,x282)
% 0.52/0.63 [29]~P2(x291)+P2(x292)+~E(x291,x292)
% 0.52/0.63 [30]P5(x302,x303)+~E(x301,x302)+~P5(x301,x303)
% 0.52/0.63 [31]P5(x313,x312)+~E(x311,x312)+~P5(x313,x311)
% 0.52/0.63 [32]P6(x322,x323)+~E(x321,x322)+~P6(x321,x323)
% 0.52/0.63 [33]P6(x333,x332)+~E(x331,x332)+~P6(x333,x331)
% 0.52/0.63 [34]~P8(x341)+P8(x342)+~E(x341,x342)
% 0.52/0.63 [35]P4(x352,x353,x354)+~E(x351,x352)+~P4(x351,x353,x354)
% 0.52/0.63 [36]P4(x363,x362,x364)+~E(x361,x362)+~P4(x363,x361,x364)
% 0.52/0.63 [37]P4(x373,x374,x372)+~E(x371,x372)+~P4(x373,x374,x371)
% 0.52/0.63 [38]P3(x382,x383,x384)+~E(x381,x382)+~P3(x381,x383,x384)
% 0.52/0.63 [39]P3(x393,x392,x394)+~E(x391,x392)+~P3(x393,x391,x394)
% 0.52/0.63 [40]P3(x403,x404,x402)+~E(x401,x402)+~P3(x403,x404,x401)
% 0.52/0.63 [41]~P7(x411)+P7(x412)+~E(x411,x412)
% 0.52/0.63 [42]~P9(x421)+P9(x422)+~E(x421,x422)
% 0.52/0.63
% 0.52/0.63 %-------------------------------------------
% 0.52/0.63 cnf(137,plain,
% 0.52/0.63 ($false),
% 0.52/0.63 inference(scs_inference,[],[50,59,60,53,71,82,2,70]),
% 0.52/0.63 ['proof']).
% 0.52/0.63 % SZS output end Proof
% 0.52/0.63 % Total time :0.010000s
%------------------------------------------------------------------------------