%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET074-6 : 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 : 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:31 EDT 2024
% Result : Unsatisfiable 21.19s 21.22s
% Output : CNFRefutation 21.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SET074-6 : 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.33 % Computer : n020.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 11:20:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.20/0.56 start to proof:theBenchmark
% 21.09/21.21 %-------------------------------------------
% 21.09/21.21 % File :CSE---1.7
% 21.09/21.21 % Problem :theBenchmark
% 21.09/21.21 % Transform :cnf
% 21.09/21.21 % Format :tptp:raw
% 21.09/21.21 % Command :java -jar mcs_scs.jar %d %s
% 21.09/21.21
% 21.09/21.21 % Result :Theorem 20.610000s
% 21.09/21.21 % Output :CNFRefutation 20.610000s
% 21.09/21.21 %-------------------------------------------
% 21.19/21.22 %--------------------------------------------------------------------------
% 21.19/21.22 % File : SET074-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 21.19/21.22 % Domain : Set Theory
% 21.19/21.22 % Problem : Corollary to unordered pair axiom
% 21.19/21.22 % Version : [Qua92] axioms.
% 21.19/21.22 % English :
% 21.19/21.22
% 21.19/21.22 % Refs : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 21.19/21.22 % Source : [Quaife]
% 21.19/21.22 % Names :
% 21.19/21.22
% 21.19/21.22 % Status : Unsatisfiable
% 21.19/21.22 % Rating : 0.20 v8.2.0, 0.24 v8.1.0, 0.11 v7.5.0, 0.21 v7.4.0, 0.24 v7.3.0, 0.25 v7.1.0, 0.17 v7.0.0, 0.27 v6.4.0, 0.33 v6.3.0, 0.18 v6.2.0, 0.30 v6.1.0, 0.29 v6.0.0, 0.20 v5.5.0, 0.50 v5.3.0, 0.39 v5.2.0, 0.38 v5.1.0, 0.35 v5.0.0, 0.36 v4.1.0, 0.38 v4.0.1, 0.55 v3.7.0, 0.40 v3.5.0, 0.45 v3.4.0, 0.33 v3.3.0, 0.29 v3.2.0, 0.15 v3.1.0, 0.27 v2.7.0, 0.25 v2.6.0, 0.11 v2.5.0, 0.18 v2.4.0, 0.12 v2.2.1, 0.17 v2.2.0, 0.33 v2.1.0
% 21.19/21.22 % Syntax : Number of clauses : 93 ( 31 unt; 8 nHn; 64 RR)
% 21.19/21.22 % Number of literals : 183 ( 40 equ; 84 neg)
% 21.19/21.22 % Maximal clause size : 5 ( 1 avg)
% 21.19/21.22 % Maximal term depth : 6 ( 1 avg)
% 21.19/21.22 % Number of predicates : 10 ( 9 usr; 0 prp; 1-3 aty)
% 21.19/21.22 % Number of functors : 40 ( 40 usr; 10 con; 0-3 aty)
% 21.19/21.22 % Number of variables : 176 ( 25 sgn)
% 21.19/21.22 % SPC : CNF_UNS_RFO_SEQ_NHN
% 21.19/21.22
% 21.19/21.22 % Comments :
% 21.19/21.22 % Bugfixes : v2.1.0 - Bugfix in SET004-0.ax.
% 21.19/21.22 %--------------------------------------------------------------------------
% 21.19/21.22 %----Include von Neuman-Bernays-Godel set theory axioms
% 21.19/21.22 include('Axioms/SET004-0.ax').
% 21.19/21.22 %--------------------------------------------------------------------------
% 21.19/21.22 cnf(prove_corollary_to_unordered_pair_axiom2_1,negated_conjecture,
% 21.19/21.22 member(y,universal_class) ).
% 21.19/21.22
% 21.19/21.22 cnf(prove_corollary_to_unordered_pair_axiom2_2,negated_conjecture,
% 21.19/21.22 unordered_pair(x,y) = null_class ).
% 21.19/21.22
% 21.19/21.22 %--------------------------------------------------------------------------
% 21.19/21.22 %-------------------------------------------
% 21.19/21.22 % Proof found
% 21.19/21.22 % SZS status Theorem for theBenchmark
% 21.19/21.22 % SZS output start Proof
% 21.19/21.22 %ClaNum:120(EqnAxiom:42)
% 21.19/21.22 %VarNum:718(SingletonVarNum:150)
% 21.19/21.22 %MaxLitNum:5
% 21.19/21.22 %MaxfuncDepth:24
% 21.19/21.22 %SharedTerms:34
% 21.19/21.22 %goalClause: 45 47
% 21.19/21.22 %singleGoalClaCount:2
% 21.19/21.22 [43]P1(a1)
% 21.19/21.22 [44]P2(a2)
% 21.19/21.22 [46]P5(a1,a19)
% 21.19/21.22 [47]P5(a25,a19)
% 21.19/21.22 [45]E(f18(a17,a25),a4)
% 21.19/21.22 [49]P6(a5,f6(a19,a19))
% 21.19/21.22 [50]P6(a20,f6(a19,a19))
% 21.19/21.22 [56]E(f10(f9(f11(f6(a23,a19))),a23),a13)
% 21.19/21.22 [57]E(f10(f6(a19,a19),f10(f6(a19,a19),f8(f7(f8(a5),f9(f11(f6(a5,a19))))))),a23)
% 21.19/21.22 [48]P6(x481,a19)
% 21.19/21.22 [54]P6(f21(x541),f6(f6(a19,a19),a19))
% 21.19/21.22 [55]P6(f11(x551),f6(f6(a19,a19),a19))
% 21.19/21.22 [58]E(f10(f9(x581),f8(f9(f10(f7(f9(f11(f6(a5,a19))),x581),a13)))),f3(x581))
% 21.19/21.22 [51]P5(f18(x511,x512),a19)
% 21.19/21.22 [52]P6(f7(x521,x522),f6(a19,a19))
% 21.19/21.22 [53]E(f10(f6(x531,x532),x533),f10(x533,f6(x531,x532)))
% 21.19/21.22 [59]~P7(x591)+P2(x591)
% 21.19/21.22 [60]~P8(x601)+P2(x601)
% 21.19/21.22 [63]~P1(x631)+P6(a1,x631)
% 21.19/21.22 [64]~P1(x641)+P5(a4,x641)
% 21.19/21.22 [66]P5(f22(x661),x661)+E(x661,a4)
% 21.19/21.22 [67]~P2(x671)+P6(x671,f6(a19,a19))
% 21.19/21.22 [65]E(x651,a4)+E(f10(x651,f22(x651)),a4)
% 21.19/21.22 [75]~P8(x751)+E(f6(f9(f9(x751)),f9(f9(x751))),f9(x751))
% 21.19/21.22 [85]~P7(x851)+P2(f9(f11(f6(x851,a19))))
% 21.19/21.22 [89]~P5(x891,a19)+P5(f9(f10(a5,f6(a19,x891))),a19)
% 21.19/21.22 [91]~P9(x911)+P6(f7(x911,f9(f11(f6(x911,a19)))),a13)
% 21.19/21.22 [92]~P2(x921)+P6(f7(x921,f9(f11(f6(x921,a19)))),a13)
% 21.19/21.22 [93]~P8(x931)+P6(f9(f9(f11(f6(x931,a19)))),f9(f9(x931)))
% 21.19/21.22 [98]P9(x981)+~P6(f7(x981,f9(f11(f6(x981,a19)))),a13)
% 21.19/21.22 [107]~P1(x1071)+P6(f9(f9(f11(f6(f10(a20,f6(x1071,a19)),a19)))),x1071)
% 21.19/21.22 [111]~P5(x1111,a19)+P5(f8(f9(f9(f11(f6(f10(a5,f6(f8(x1111),a19)),a19))))),a19)
% 21.19/21.22 [61]~E(x612,x611)+P6(x611,x612)
% 21.19/21.22 [62]~E(x621,x622)+P6(x621,x622)
% 21.19/21.22 [69]P6(x691,x692)+P5(f14(x691,x692),x691)
% 21.19/21.22 [70]~P5(x701,x702)+~P5(x701,f8(x702))
% 21.19/21.22 [73]~P5(x731,a19)+P5(x731,f18(x732,x731))
% 21.19/21.22 [74]~P5(x741,a19)+P5(x741,f18(x741,x742))
% 21.19/21.22 [79]P6(x791,x792)+~P5(f14(x791,x792),x792)
% 21.19/21.22 [88]~P5(x882,f9(x881))+~E(f10(x881,f6(f18(x882,x882),a19)),a4)
% 21.19/21.22 [97]P5(x971,x972)+~P5(f18(f18(x971,x971),f18(x971,f18(x972,x972))),a5)
% 21.19/21.22 [104]~P5(f18(f18(x1041,x1041),f18(x1041,f18(x1042,x1042))),a20)+E(f8(f10(f8(x1041),f8(f18(x1041,x1041)))),x1042)
% 21.19/21.22 [81]P2(x811)+~P3(x811,x812,x813)
% 21.19/21.22 [82]P8(x821)+~P4(x822,x823,x821)
% 21.19/21.22 [83]P8(x831)+~P4(x832,x831,x833)
% 21.19/21.22 [87]~P4(x871,x872,x873)+P3(x871,x872,x873)
% 21.19/21.22 [77]P5(x771,x772)+~P5(x771,f10(x773,x772))
% 21.19/21.22 [78]P5(x781,x782)+~P5(x781,f10(x782,x783))
% 21.19/21.22 [84]~P3(x842,x841,x843)+E(f9(f9(x841)),f9(x842))
% 21.19/21.22 [94]~P5(x941,f6(x942,x943))+E(f18(f18(f12(x941),f12(x941)),f18(f12(x941),f18(f24(x941),f24(x941)))),x941)
% 21.19/21.22 [96]~P3(x961,x963,x962)+P6(f9(f9(f11(f6(x961,a19)))),f9(f9(x962)))
% 21.19/21.22 [99]P5(x991,x992)+~P5(f18(f18(x993,x993),f18(x993,f18(x991,x991))),f6(x994,x992))
% 21.19/21.22 [100]P5(x1001,x1002)+~P5(f18(f18(x1001,x1001),f18(x1001,f18(x1003,x1003))),f6(x1002,x1004))
% 21.19/21.22 [112]~P5(f18(f18(f18(f18(x1123,x1123),f18(x1123,f18(x1121,x1121))),f18(f18(x1123,x1123),f18(x1123,f18(x1121,x1121)))),f18(f18(f18(x1123,x1123),f18(x1123,f18(x1121,x1121))),f18(x1122,x1122))),f21(x1124))+P5(f18(f18(f18(f18(x1121,x1121),f18(x1121,f18(x1122,x1122))),f18(f18(x1121,x1121),f18(x1121,f18(x1122,x1122)))),f18(f18(f18(x1121,x1121),f18(x1121,f18(x1122,x1122))),f18(x1123,x1123))),x1124)
% 21.19/21.22 [113]~P5(f18(f18(f18(f18(x1132,x1132),f18(x1132,f18(x1131,x1131))),f18(f18(x1132,x1132),f18(x1132,f18(x1131,x1131)))),f18(f18(f18(x1132,x1132),f18(x1132,f18(x1131,x1131))),f18(x1133,x1133))),f11(x1134))+P5(f18(f18(f18(f18(x1131,x1131),f18(x1131,f18(x1132,x1132))),f18(f18(x1131,x1131),f18(x1131,f18(x1132,x1132)))),f18(f18(f18(x1131,x1131),f18(x1131,f18(x1132,x1132))),f18(x1133,x1133))),x1134)
% 21.19/21.22 [117]~P5(f18(f18(x1174,x1174),f18(x1174,f18(x1171,x1171))),f7(x1172,x1173))+P5(x1171,f9(f9(f11(f6(f10(x1172,f6(f9(f9(f11(f6(f10(x1173,f6(f18(x1174,x1174),a19)),a19)))),a19)),a19)))))
% 21.19/21.22 [90]~P2(x901)+P7(x901)+~P2(f9(f11(f6(x901,a19))))
% 21.19/21.22 [101]P2(x1011)+~P6(x1011,f6(a19,a19))+~P6(f7(x1011,f9(f11(f6(x1011,a19)))),a13)
% 21.19/21.22 [109]P1(x1091)+~P5(a4,x1091)+~P6(f9(f9(f11(f6(f10(a20,f6(x1091,a19)),a19)))),x1091)
% 21.19/21.22 [116]~P5(x1161,a19)+E(x1161,a4)+P5(f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(a2,f6(f18(x1161,x1161),a19)),a19))))))),x1161)
% 21.19/21.22 [68]~P6(x682,x681)+~P6(x681,x682)+E(x681,x682)
% 21.19/21.22 [71]P5(x711,x712)+P5(x711,f8(x712))+~P5(x711,a19)
% 21.19/21.22 [86]P5(x862,f9(x861))+~P5(x862,a19)+E(f10(x861,f6(f18(x862,x862),a19)),a4)
% 21.19/21.22 [105]~P5(x1051,x1052)+~P5(f18(f18(x1051,x1051),f18(x1051,f18(x1052,x1052))),f6(a19,a19))+P5(f18(f18(x1051,x1051),f18(x1051,f18(x1052,x1052))),a5)
% 21.19/21.22 [106]~P5(f18(f18(x1061,x1061),f18(x1061,f18(x1062,x1062))),f6(a19,a19))+~E(f8(f10(f8(x1061),f8(f18(x1061,x1061)))),x1062)+P5(f18(f18(x1061,x1061),f18(x1061,f18(x1062,x1062))),a20)
% 21.19/21.22 [108]~P2(x1081)+~P5(x1082,a19)+P5(f9(f9(f11(f6(f10(x1081,f6(x1082,a19)),a19)))),a19)
% 21.19/21.23 [72]~P5(x721,x723)+P5(x721,x722)+~P6(x723,x722)
% 21.19/21.23 [76]E(x761,x762)+E(x761,x763)+~P5(x761,f18(x763,x762))
% 21.19/21.23 [80]~P5(x801,x803)+~P5(x801,x802)+P5(x801,f10(x802,x803))
% 21.19/21.23 [95]~P5(x952,x954)+~P5(x951,x953)+P5(f18(f18(x951,x951),f18(x951,f18(x952,x952))),f6(x953,x954))
% 21.19/21.23 [114]~P5(f18(f18(f18(f18(x1142,x1142),f18(x1142,f18(x1143,x1143))),f18(f18(x1142,x1142),f18(x1142,f18(x1143,x1143)))),f18(f18(f18(x1142,x1142),f18(x1142,f18(x1143,x1143))),f18(x1141,x1141))),x1144)+P5(f18(f18(f18(f18(x1141,x1141),f18(x1141,f18(x1142,x1142))),f18(f18(x1141,x1141),f18(x1141,f18(x1142,x1142)))),f18(f18(f18(x1141,x1141),f18(x1141,f18(x1142,x1142))),f18(x1143,x1143))),f21(x1144))+~P5(f18(f18(f18(f18(x1141,x1141),f18(x1141,f18(x1142,x1142))),f18(f18(x1141,x1141),f18(x1141,f18(x1142,x1142)))),f18(f18(f18(x1141,x1141),f18(x1141,f18(x1142,x1142))),f18(x1143,x1143))),f6(f6(a19,a19),a19))
% 21.19/21.23 [115]~P5(f18(f18(f18(f18(x1152,x1152),f18(x1152,f18(x1151,x1151))),f18(f18(x1152,x1152),f18(x1152,f18(x1151,x1151)))),f18(f18(f18(x1152,x1152),f18(x1152,f18(x1151,x1151))),f18(x1153,x1153))),x1154)+P5(f18(f18(f18(f18(x1151,x1151),f18(x1151,f18(x1152,x1152))),f18(f18(x1151,x1151),f18(x1151,f18(x1152,x1152)))),f18(f18(f18(x1151,x1151),f18(x1151,f18(x1152,x1152))),f18(x1153,x1153))),f11(x1154))+~P5(f18(f18(f18(f18(x1151,x1151),f18(x1151,f18(x1152,x1152))),f18(f18(x1151,x1151),f18(x1151,f18(x1152,x1152)))),f18(f18(f18(x1151,x1151),f18(x1151,f18(x1152,x1152))),f18(x1153,x1153))),f6(f6(a19,a19),a19))
% 21.19/21.23 [118]P5(f18(f18(x1181,x1181),f18(x1181,f18(x1182,x1182))),f7(x1183,x1184))+~P5(f18(f18(x1181,x1181),f18(x1181,f18(x1182,x1182))),f6(a19,a19))+~P5(x1182,f9(f9(f11(f6(f10(x1183,f6(f9(f9(f11(f6(f10(x1184,f6(f18(x1181,x1181),a19)),a19)))),a19)),a19)))))
% 21.19/21.23 [119]~P4(x1192,x1195,x1191)+~P5(f18(f18(x1193,x1193),f18(x1193,f18(x1194,x1194))),f9(x1195))+E(f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1191,f6(f18(f18(f18(f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1192,f6(f18(x1193,x1193),a19)),a19))))))),f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1192,f6(f18(x1193,x1193),a19)),a19)))))))),f18(f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1192,f6(f18(x1193,x1193),a19)),a19))))))),f18(f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1192,f6(f18(x1194,x1194),a19)),a19))))))),f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1192,f6(f18(x1194,x1194),a19)),a19)))))))))),f18(f18(f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1192,f6(f18(x1193,x1193),a19)),a19))))))),f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1192,f6(f18(x1193,x1193),a19)),a19)))))))),f18(f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1192,f6(f18(x1193,x1193),a19)),a19))))))),f18(f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1192,f6(f18(x1194,x1194),a19)),a19))))))),f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1192,f6(f18(x1194,x1194),a19)),a19))))))))))),a19)),a19))))))),f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1192,f6(f18(f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1195,f6(f18(f18(f18(x1193,x1193),f18(x1193,f18(x1194,x1194))),f18(f18(x1193,x1193),f18(x1193,f18(x1194,x1194)))),a19)),a19))))))),f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1195,f6(f18(f18(f18(x1193,x1193),f18(x1193,f18(x1194,x1194))),f18(f18(x1193,x1193),f18(x1193,f18(x1194,x1194)))),a19)),a19)))))))),a19)),a19))))))))
% 21.19/21.23 [103]~P2(x1031)+P8(x1031)+~E(f6(f9(f9(x1031)),f9(f9(x1031))),f9(x1031))+~P6(f9(f9(f11(f6(x1031,a19)))),f9(f9(x1031)))
% 21.19/21.23 [102]~P2(x1021)+P3(x1021,x1022,x1023)+~E(f9(f9(x1022)),f9(x1021))+~P6(f9(f9(f11(f6(x1021,a19)))),f9(f9(x1023)))
% 21.19/21.23 [110]~P8(x1103)+~P8(x1102)+~P3(x1101,x1102,x1103)+P4(x1101,x1102,x1103)+P5(f18(f18(f15(x1101,x1102,x1103),f15(x1101,x1102,x1103)),f18(f15(x1101,x1102,x1103),f18(f16(x1101,x1102,x1103),f16(x1101,x1102,x1103)))),f9(x1102))
% 21.19/21.23 [120]~P8(x1203)+~P8(x1202)+~P3(x1201,x1202,x1203)+P4(x1201,x1202,x1203)+~E(f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1203,f6(f18(f18(f18(f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1201,f6(f18(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a19)),a19))))))),f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1201,f6(f18(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a19)),a19)))))))),f18(f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1201,f6(f18(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a19)),a19))))))),f18(f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1201,f6(f18(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)),a19)),a19))))))),f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1201,f6(f18(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)),a19)),a19)))))))))),f18(f18(f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1201,f6(f18(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a19)),a19))))))),f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1201,f6(f18(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a19)),a19)))))))),f18(f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1201,f6(f18(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),a19)),a19))))))),f18(f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1201,f6(f18(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)),a19)),a19))))))),f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1201,f6(f18(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)),a19)),a19))))))))))),a19)),a19))))))),f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1201,f6(f18(f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1202,f6(f18(f18(f18(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),f18(f15(x1201,x1202,x1203),f18(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)))),f18(f18(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),f18(f15(x1201,x1202,x1203),f18(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203))))),a19)),a19))))))),f9(f10(a5,f6(a19,f9(f9(f11(f6(f10(x1202,f6(f18(f18(f18(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),f18(f15(x1201,x1202,x1203),f18(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)))),f18(f18(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),f18(f15(x1201,x1202,x1203),f18(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203))))),a19)),a19)))))))),a19)),a19))))))))
% 21.19/21.23 %EqnAxiom
% 21.19/21.23 [1]E(x11,x11)
% 21.19/21.23 [2]E(x22,x21)+~E(x21,x22)
% 21.19/21.23 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 21.19/21.23 [4]~E(x41,x42)+E(f18(x41,x43),f18(x42,x43))
% 21.19/21.23 [5]~E(x51,x52)+E(f18(x53,x51),f18(x53,x52))
% 21.19/21.23 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63))
% 21.19/21.23 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72))
% 21.19/21.23 [8]~E(x81,x82)+E(f10(x81,x83),f10(x82,x83))
% 21.19/21.23 [9]~E(x91,x92)+E(f10(x93,x91),f10(x93,x92))
% 21.19/21.23 [10]~E(x101,x102)+E(f9(x101),f9(x102))
% 21.19/21.23 [11]~E(x111,x112)+E(f7(x111,x113),f7(x112,x113))
% 21.19/21.23 [12]~E(x121,x122)+E(f7(x123,x121),f7(x123,x122))
% 21.19/21.23 [13]~E(x131,x132)+E(f15(x131,x133,x134),f15(x132,x133,x134))
% 21.19/21.23 [14]~E(x141,x142)+E(f15(x143,x141,x144),f15(x143,x142,x144))
% 21.19/21.23 [15]~E(x151,x152)+E(f15(x153,x154,x151),f15(x153,x154,x152))
% 21.19/21.23 [16]~E(x161,x162)+E(f11(x161),f11(x162))
% 21.19/21.23 [17]~E(x171,x172)+E(f16(x171,x173,x174),f16(x172,x173,x174))
% 21.19/21.23 [18]~E(x181,x182)+E(f16(x183,x181,x184),f16(x183,x182,x184))
% 21.19/21.23 [19]~E(x191,x192)+E(f16(x193,x194,x191),f16(x193,x194,x192))
% 21.19/21.23 [20]~E(x201,x202)+E(f8(x201),f8(x202))
% 21.19/21.23 [21]~E(x211,x212)+E(f21(x211),f21(x212))
% 21.19/21.23 [22]~E(x221,x222)+E(f14(x221,x223),f14(x222,x223))
% 21.19/21.23 [23]~E(x231,x232)+E(f14(x233,x231),f14(x233,x232))
% 21.19/21.23 [24]~E(x241,x242)+E(f3(x241),f3(x242))
% 21.19/21.23 [25]~E(x251,x252)+E(f24(x251),f24(x252))
% 21.19/21.23 [26]~E(x261,x262)+E(f22(x261),f22(x262))
% 21.19/21.23 [27]~E(x271,x272)+E(f12(x271),f12(x272))
% 21.19/21.23 [28]~P1(x281)+P1(x282)+~E(x281,x282)
% 21.19/21.23 [29]~P2(x291)+P2(x292)+~E(x291,x292)
% 21.19/21.23 [30]P5(x302,x303)+~E(x301,x302)+~P5(x301,x303)
% 21.19/21.23 [31]P5(x313,x312)+~E(x311,x312)+~P5(x313,x311)
% 21.19/21.23 [32]P3(x322,x323,x324)+~E(x321,x322)+~P3(x321,x323,x324)
% 21.19/21.23 [33]P3(x333,x332,x334)+~E(x331,x332)+~P3(x333,x331,x334)
% 21.19/21.23 [34]P3(x343,x344,x342)+~E(x341,x342)+~P3(x343,x344,x341)
% 21.19/21.23 [35]P6(x352,x353)+~E(x351,x352)+~P6(x351,x353)
% 21.19/21.23 [36]P6(x363,x362)+~E(x361,x362)+~P6(x363,x361)
% 21.19/21.23 [37]~P7(x371)+P7(x372)+~E(x371,x372)
% 21.19/21.23 [38]~P8(x381)+P8(x382)+~E(x381,x382)
% 21.19/21.23 [39]P4(x392,x393,x394)+~E(x391,x392)+~P4(x391,x393,x394)
% 21.19/21.23 [40]P4(x403,x402,x404)+~E(x401,x402)+~P4(x403,x401,x404)
% 21.19/21.23 [41]P4(x413,x414,x412)+~E(x411,x412)+~P4(x413,x414,x411)
% 21.19/21.23 [42]~P9(x421)+P9(x422)+~E(x421,x422)
% 21.19/21.23
% 21.19/21.23 %-------------------------------------------
% 21.19/21.23 cnf(121,plain,
% 21.19/21.23 (P6(x1211,x1211)),
% 21.19/21.23 inference(equality_inference,[],[61])).
% 21.19/21.23 cnf(126,plain,
% 21.19/21.23 (P5(a4,a19)),
% 21.19/21.23 inference(scs_inference,[],[45,51,2,30])).
% 21.19/21.23 cnf(128,plain,
% 21.19/21.23 (P6(a4,f18(a17,a25))),
% 21.19/21.23 inference(scs_inference,[],[45,121,51,2,30,35])).
% 21.19/21.23 cnf(129,plain,
% 21.19/21.23 (P6(x1291,x1291)),
% 21.19/21.23 inference(rename_variables,[],[121])).
% 21.19/21.23 cnf(130,plain,
% 21.19/21.23 (P6(f18(a17,a25),a4)),
% 21.19/21.23 inference(scs_inference,[],[45,121,129,51,2,30,35,36])).
% 21.19/21.23 cnf(158,plain,
% 21.19/21.23 (~P5(x1581,f18(a17,a25))+P5(x1581,a4)),
% 21.19/21.23 inference(scs_inference,[],[130,57,2,72])).
% 21.19/21.23 cnf(167,plain,
% 21.19/21.23 (~P5(x1671,a4)+P5(x1671,f18(a17,a25))),
% 21.19/21.23 inference(scs_inference,[],[128,50,54,56,2,68,36,72])).
% 21.19/21.23 cnf(375,plain,
% 21.19/21.23 (~P5(a4,f8(a1))),
% 21.19/21.23 inference(scs_inference,[],[43,64,70])).
% 21.19/21.23 cnf(401,plain,
% 21.19/21.23 (P6(f10(x4011,f6(x4012,x4013)),f10(f6(x4012,x4013),x4011))),
% 21.19/21.23 inference(scs_inference,[],[53,121,35])).
% 21.19/21.23 cnf(770,plain,
% 21.19/21.23 (~P5(a25,f8(f18(a25,x7701)))),
% 21.19/21.23 inference(scs_inference,[],[47,74,70])).
% 21.19/21.23 cnf(789,plain,
% 21.19/21.23 (~P5(a4,f10(x7891,f10(f8(a1),x7892)))),
% 21.19/21.23 inference(scs_inference,[],[375,77,78])).
% 21.19/21.23 cnf(793,plain,
% 21.19/21.23 (~P5(a4,f10(x7931,f10(f8(a1),x7932)))),
% 21.19/21.23 inference(rename_variables,[],[789])).
% 21.19/21.23 cnf(795,plain,
% 21.19/21.23 (~P5(a4,f10(f10(f8(a1),x7951),f6(x7952,x7953)))),
% 21.19/21.23 inference(scs_inference,[],[401,126,789,793,64,80,72])).
% 21.19/21.23 cnf(805,plain,
% 21.19/21.23 (P5(a25,a4)),
% 21.19/21.23 inference(scs_inference,[],[47,158,73])).
% 21.19/21.23 cnf(810,plain,
% 21.19/21.23 (~E(a4,f8(f18(a25,x8101)))),
% 21.19/21.23 inference(scs_inference,[],[770,805,795,167,64,31])).
% 21.19/21.23 cnf(978,plain,
% 21.19/21.23 (E(f10(f8(f18(a25,x9781)),f22(f8(f18(a25,x9781)))),a4)),
% 21.19/21.23 inference(scs_inference,[],[810,65,2])).
% 21.19/21.23 cnf(979,plain,
% 21.19/21.23 (E(a4,f10(f8(f18(a25,x9791)),f22(f8(f18(a25,x9791)))))),
% 21.19/21.23 inference(scs_inference,[],[978,2])).
% 21.19/21.23 cnf(3188,plain,
% 21.19/21.23 (P6(x31881,x31881)),
% 21.19/21.23 inference(rename_variables,[],[121])).
% 21.19/21.23 cnf(3192,plain,
% 21.19/21.23 (P5(a25,f10(f8(f18(a25,x31921)),f22(f8(f18(a25,x31921)))))),
% 21.19/21.23 inference(scs_inference,[],[978,979,121,3188,805,35,36,3,72])).
% 21.19/21.23 cnf(3214,plain,
% 21.19/21.23 ($false),
% 21.19/21.23 inference(scs_inference,[],[770,3192,78]),
% 21.19/21.23 ['proof']).
% 21.19/21.24 % SZS output end Proof
% 21.19/21.24 % Total time :20.610000s
%------------------------------------------------------------------------------