%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET093-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 : 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:39 EDT 2024
% Result : Unsatisfiable 0.62s 0.68s
% Output : CNFRefutation 0.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SET093-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.07/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n019.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Sun Jun 23 14:59:54 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.22/0.59 start to proof:theBenchmark
% 0.62/0.67 %-------------------------------------------
% 0.62/0.67 % File :CSE---1.7
% 0.62/0.67 % Problem :theBenchmark
% 0.62/0.67 % Transform :cnf
% 0.62/0.67 % Format :tptp:raw
% 0.62/0.67 % Command :java -jar mcs_scs.jar %d %s
% 0.62/0.67
% 0.62/0.67 % Result :Theorem 0.010000s
% 0.62/0.67 % Output :CNFRefutation 0.010000s
% 0.62/0.67 %-------------------------------------------
% 0.62/0.68 %--------------------------------------------------------------------------
% 0.62/0.68 % File : SET093-6 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.62/0.68 % Domain : Set Theory
% 0.62/0.68 % Problem : Corollary to every singleton is a set
% 0.62/0.68 % Version : [Qua92] axioms.
% 0.62/0.68 % English :
% 0.62/0.68
% 0.62/0.68 % Refs : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 0.62/0.68 % Source : [Quaife]
% 0.62/0.68 % Names :
% 0.62/0.68
% 0.62/0.68 % Status : Unsatisfiable
% 0.62/0.68 % Rating : 0.10 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.13 v6.4.0, 0.07 v6.3.0, 0.09 v6.2.0, 0.10 v6.1.0, 0.14 v6.0.0, 0.00 v5.5.0, 0.10 v5.4.0, 0.15 v5.3.0, 0.17 v5.2.0, 0.12 v5.0.0, 0.14 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.62/0.68 % Syntax : Number of clauses : 93 ( 31 unt; 8 nHn; 64 RR)
% 0.62/0.68 % Number of literals : 183 ( 40 equ; 85 neg)
% 0.62/0.68 % Maximal clause size : 5 ( 1 avg)
% 0.62/0.68 % Maximal term depth : 6 ( 1 avg)
% 0.62/0.68 % Number of predicates : 10 ( 9 usr; 0 prp; 1-3 aty)
% 0.62/0.68 % Number of functors : 40 ( 40 usr; 9 con; 0-3 aty)
% 0.62/0.68 % Number of variables : 176 ( 25 sgn)
% 0.62/0.68 % SPC : CNF_UNS_RFO_SEQ_NHN
% 0.62/0.68
% 0.62/0.68 % Comments :
% 0.62/0.68 % Bugfixes : v2.1.0 - Bugfix in SET004-0.ax.
% 0.62/0.68 %--------------------------------------------------------------------------
% 0.62/0.68 %----Include von Neuman-Bernays-Godel set theory axioms
% 0.62/0.68 include('Axioms/SET004-0.ax').
% 0.62/0.68 %--------------------------------------------------------------------------
% 0.62/0.68 cnf(prove_corollary_2_to_singletons_are_sets_1,negated_conjecture,
% 0.62/0.68 singleton(member_of(x)) = x ).
% 0.62/0.68
% 0.62/0.68 cnf(prove_corollary_2_to_singletons_are_sets_2,negated_conjecture,
% 0.62/0.68 ~ member(x,universal_class) ).
% 0.62/0.68
% 0.62/0.68 %--------------------------------------------------------------------------
% 0.62/0.68 %-------------------------------------------
% 0.62/0.68 % Proof found
% 0.62/0.68 % SZS status Theorem for theBenchmark
% 0.62/0.68 % SZS output start Proof
% 0.62/0.68 %ClaNum:121(EqnAxiom:43)
% 0.62/0.68 %VarNum:718(SingletonVarNum:150)
% 0.62/0.68 %MaxLitNum:5
% 0.62/0.68 %MaxfuncDepth:24
% 0.62/0.68 %SharedTerms:34
% 0.62/0.68 %goalClause: 48 59
% 0.62/0.68 %singleGoalClaCount:2
% 0.62/0.68 [44]P1(a1)
% 0.62/0.68 [45]P2(a2)
% 0.62/0.68 [46]P5(a1,a18)
% 0.62/0.68 [59]~P5(a24,a18)
% 0.62/0.68 [49]P6(a5,f6(a18,a18))
% 0.62/0.68 [50]P6(a19,f6(a18,a18))
% 0.62/0.68 [48]E(f25(f4(a24),f4(a24)),a24)
% 0.62/0.68 [56]E(f10(f9(f11(f6(a22,a18))),a22),a13)
% 0.62/0.68 [57]E(f10(f6(a18,a18),f10(f6(a18,a18),f8(f7(f8(a5),f9(f11(f6(a5,a18))))))),a22)
% 0.62/0.68 [47]P6(x471,a18)
% 0.62/0.68 [54]P6(f20(x541),f6(f6(a18,a18),a18))
% 0.62/0.68 [55]P6(f11(x551),f6(f6(a18,a18),a18))
% 0.62/0.68 [58]E(f10(f9(x581),f8(f9(f10(f7(f9(f11(f6(a5,a18))),x581),a13)))),f3(x581))
% 0.62/0.68 [51]P5(f25(x511,x512),a18)
% 0.62/0.68 [52]P6(f7(x521,x522),f6(a18,a18))
% 0.62/0.68 [53]E(f10(f6(x531,x532),x533),f10(x533,f6(x531,x532)))
% 0.62/0.68 [60]~P7(x601)+P2(x601)
% 0.62/0.68 [61]~P8(x611)+P2(x611)
% 0.62/0.68 [64]~P1(x641)+P6(a1,x641)
% 0.62/0.68 [65]~P1(x651)+P5(a14,x651)
% 0.62/0.68 [67]P5(f21(x671),x671)+E(x671,a14)
% 0.62/0.68 [68]~P2(x681)+P6(x681,f6(a18,a18))
% 0.62/0.68 [66]E(x661,a14)+E(f10(x661,f21(x661)),a14)
% 0.62/0.68 [76]~P8(x761)+E(f6(f9(f9(x761)),f9(f9(x761))),f9(x761))
% 0.62/0.68 [86]~P7(x861)+P2(f9(f11(f6(x861,a18))))
% 0.62/0.68 [90]~P5(x901,a18)+P5(f9(f10(a5,f6(a18,x901))),a18)
% 0.62/0.68 [92]~P9(x921)+P6(f7(x921,f9(f11(f6(x921,a18)))),a13)
% 0.62/0.68 [93]~P2(x931)+P6(f7(x931,f9(f11(f6(x931,a18)))),a13)
% 0.62/0.68 [94]~P8(x941)+P6(f9(f9(f11(f6(x941,a18)))),f9(f9(x941)))
% 0.62/0.68 [99]P9(x991)+~P6(f7(x991,f9(f11(f6(x991,a18)))),a13)
% 0.62/0.68 [108]~P1(x1081)+P6(f9(f9(f11(f6(f10(a19,f6(x1081,a18)),a18)))),x1081)
% 0.62/0.68 [112]~P5(x1121,a18)+P5(f8(f9(f9(f11(f6(f10(a5,f6(f8(x1121),a18)),a18))))),a18)
% 0.62/0.68 [62]~E(x622,x621)+P6(x621,x622)
% 0.62/0.68 [63]~E(x631,x632)+P6(x631,x632)
% 0.62/0.68 [70]P6(x701,x702)+P5(f15(x701,x702),x701)
% 0.62/0.68 [71]~P5(x711,x712)+~P5(x711,f8(x712))
% 0.62/0.68 [74]~P5(x741,a18)+P5(x741,f25(x742,x741))
% 0.62/0.68 [75]~P5(x751,a18)+P5(x751,f25(x751,x752))
% 0.62/0.68 [80]P6(x801,x802)+~P5(f15(x801,x802),x802)
% 0.62/0.68 [89]~P5(x892,f9(x891))+~E(f10(x891,f6(f25(x892,x892),a18)),a14)
% 0.62/0.68 [98]P5(x981,x982)+~P5(f25(f25(x981,x981),f25(x981,f25(x982,x982))),a5)
% 0.62/0.68 [105]~P5(f25(f25(x1051,x1051),f25(x1051,f25(x1052,x1052))),a19)+E(f8(f10(f8(x1051),f8(f25(x1051,x1051)))),x1052)
% 0.62/0.68 [82]P2(x821)+~P3(x821,x822,x823)
% 0.62/0.68 [83]P8(x831)+~P4(x832,x833,x831)
% 0.62/0.68 [84]P8(x841)+~P4(x842,x841,x843)
% 0.62/0.68 [88]~P4(x881,x882,x883)+P3(x881,x882,x883)
% 0.62/0.68 [78]P5(x781,x782)+~P5(x781,f10(x783,x782))
% 0.62/0.68 [79]P5(x791,x792)+~P5(x791,f10(x792,x793))
% 0.62/0.68 [85]~P3(x852,x851,x853)+E(f9(f9(x851)),f9(x852))
% 0.62/0.68 [95]~P5(x951,f6(x952,x953))+E(f25(f25(f12(x951),f12(x951)),f25(f12(x951),f25(f23(x951),f23(x951)))),x951)
% 0.62/0.68 [97]~P3(x971,x973,x972)+P6(f9(f9(f11(f6(x971,a18)))),f9(f9(x972)))
% 0.62/0.68 [100]P5(x1001,x1002)+~P5(f25(f25(x1003,x1003),f25(x1003,f25(x1001,x1001))),f6(x1004,x1002))
% 0.62/0.68 [101]P5(x1011,x1012)+~P5(f25(f25(x1011,x1011),f25(x1011,f25(x1013,x1013))),f6(x1012,x1014))
% 0.62/0.68 [113]~P5(f25(f25(f25(f25(x1133,x1133),f25(x1133,f25(x1131,x1131))),f25(f25(x1133,x1133),f25(x1133,f25(x1131,x1131)))),f25(f25(f25(x1133,x1133),f25(x1133,f25(x1131,x1131))),f25(x1132,x1132))),f20(x1134))+P5(f25(f25(f25(f25(x1131,x1131),f25(x1131,f25(x1132,x1132))),f25(f25(x1131,x1131),f25(x1131,f25(x1132,x1132)))),f25(f25(f25(x1131,x1131),f25(x1131,f25(x1132,x1132))),f25(x1133,x1133))),x1134)
% 0.62/0.68 [114]~P5(f25(f25(f25(f25(x1142,x1142),f25(x1142,f25(x1141,x1141))),f25(f25(x1142,x1142),f25(x1142,f25(x1141,x1141)))),f25(f25(f25(x1142,x1142),f25(x1142,f25(x1141,x1141))),f25(x1143,x1143))),f11(x1144))+P5(f25(f25(f25(f25(x1141,x1141),f25(x1141,f25(x1142,x1142))),f25(f25(x1141,x1141),f25(x1141,f25(x1142,x1142)))),f25(f25(f25(x1141,x1141),f25(x1141,f25(x1142,x1142))),f25(x1143,x1143))),x1144)
% 0.62/0.68 [118]~P5(f25(f25(x1184,x1184),f25(x1184,f25(x1181,x1181))),f7(x1182,x1183))+P5(x1181,f9(f9(f11(f6(f10(x1182,f6(f9(f9(f11(f6(f10(x1183,f6(f25(x1184,x1184),a18)),a18)))),a18)),a18)))))
% 0.62/0.68 [91]~P2(x911)+P7(x911)+~P2(f9(f11(f6(x911,a18))))
% 0.62/0.68 [102]P2(x1021)+~P6(x1021,f6(a18,a18))+~P6(f7(x1021,f9(f11(f6(x1021,a18)))),a13)
% 0.62/0.68 [110]P1(x1101)+~P5(a14,x1101)+~P6(f9(f9(f11(f6(f10(a19,f6(x1101,a18)),a18)))),x1101)
% 0.62/0.68 [117]~P5(x1171,a18)+E(x1171,a14)+P5(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(a2,f6(f25(x1171,x1171),a18)),a18))))))),x1171)
% 0.62/0.68 [69]~P6(x692,x691)+~P6(x691,x692)+E(x691,x692)
% 0.62/0.68 [72]P5(x721,x722)+P5(x721,f8(x722))+~P5(x721,a18)
% 0.62/0.68 [87]P5(x872,f9(x871))+~P5(x872,a18)+E(f10(x871,f6(f25(x872,x872),a18)),a14)
% 0.62/0.68 [106]~P5(x1061,x1062)+~P5(f25(f25(x1061,x1061),f25(x1061,f25(x1062,x1062))),f6(a18,a18))+P5(f25(f25(x1061,x1061),f25(x1061,f25(x1062,x1062))),a5)
% 0.62/0.68 [107]~P5(f25(f25(x1071,x1071),f25(x1071,f25(x1072,x1072))),f6(a18,a18))+~E(f8(f10(f8(x1071),f8(f25(x1071,x1071)))),x1072)+P5(f25(f25(x1071,x1071),f25(x1071,f25(x1072,x1072))),a19)
% 0.62/0.68 [109]~P2(x1091)+~P5(x1092,a18)+P5(f9(f9(f11(f6(f10(x1091,f6(x1092,a18)),a18)))),a18)
% 0.62/0.68 [73]~P5(x731,x733)+P5(x731,x732)+~P6(x733,x732)
% 0.62/0.68 [77]E(x771,x772)+E(x771,x773)+~P5(x771,f25(x773,x772))
% 0.62/0.68 [81]~P5(x811,x813)+~P5(x811,x812)+P5(x811,f10(x812,x813))
% 0.62/0.68 [96]~P5(x962,x964)+~P5(x961,x963)+P5(f25(f25(x961,x961),f25(x961,f25(x962,x962))),f6(x963,x964))
% 0.62/0.68 [115]~P5(f25(f25(f25(f25(x1152,x1152),f25(x1152,f25(x1153,x1153))),f25(f25(x1152,x1152),f25(x1152,f25(x1153,x1153)))),f25(f25(f25(x1152,x1152),f25(x1152,f25(x1153,x1153))),f25(x1151,x1151))),x1154)+P5(f25(f25(f25(f25(x1151,x1151),f25(x1151,f25(x1152,x1152))),f25(f25(x1151,x1151),f25(x1151,f25(x1152,x1152)))),f25(f25(f25(x1151,x1151),f25(x1151,f25(x1152,x1152))),f25(x1153,x1153))),f20(x1154))+~P5(f25(f25(f25(f25(x1151,x1151),f25(x1151,f25(x1152,x1152))),f25(f25(x1151,x1151),f25(x1151,f25(x1152,x1152)))),f25(f25(f25(x1151,x1151),f25(x1151,f25(x1152,x1152))),f25(x1153,x1153))),f6(f6(a18,a18),a18))
% 0.62/0.68 [116]~P5(f25(f25(f25(f25(x1162,x1162),f25(x1162,f25(x1161,x1161))),f25(f25(x1162,x1162),f25(x1162,f25(x1161,x1161)))),f25(f25(f25(x1162,x1162),f25(x1162,f25(x1161,x1161))),f25(x1163,x1163))),x1164)+P5(f25(f25(f25(f25(x1161,x1161),f25(x1161,f25(x1162,x1162))),f25(f25(x1161,x1161),f25(x1161,f25(x1162,x1162)))),f25(f25(f25(x1161,x1161),f25(x1161,f25(x1162,x1162))),f25(x1163,x1163))),f11(x1164))+~P5(f25(f25(f25(f25(x1161,x1161),f25(x1161,f25(x1162,x1162))),f25(f25(x1161,x1161),f25(x1161,f25(x1162,x1162)))),f25(f25(f25(x1161,x1161),f25(x1161,f25(x1162,x1162))),f25(x1163,x1163))),f6(f6(a18,a18),a18))
% 0.62/0.68 [119]P5(f25(f25(x1191,x1191),f25(x1191,f25(x1192,x1192))),f7(x1193,x1194))+~P5(f25(f25(x1191,x1191),f25(x1191,f25(x1192,x1192))),f6(a18,a18))+~P5(x1192,f9(f9(f11(f6(f10(x1193,f6(f9(f9(f11(f6(f10(x1194,f6(f25(x1191,x1191),a18)),a18)))),a18)),a18)))))
% 0.62/0.68 [120]~P4(x1202,x1205,x1201)+~P5(f25(f25(x1203,x1203),f25(x1203,f25(x1204,x1204))),f9(x1205))+E(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1201,f6(f25(f25(f25(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1202,f6(f25(x1203,x1203),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1202,f6(f25(x1203,x1203),a18)),a18)))))))),f25(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1202,f6(f25(x1203,x1203),a18)),a18))))))),f25(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1202,f6(f25(x1204,x1204),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1202,f6(f25(x1204,x1204),a18)),a18)))))))))),f25(f25(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1202,f6(f25(x1203,x1203),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1202,f6(f25(x1203,x1203),a18)),a18)))))))),f25(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1202,f6(f25(x1203,x1203),a18)),a18))))))),f25(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1202,f6(f25(x1204,x1204),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1202,f6(f25(x1204,x1204),a18)),a18))))))))))),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1202,f6(f25(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1205,f6(f25(f25(f25(x1203,x1203),f25(x1203,f25(x1204,x1204))),f25(f25(x1203,x1203),f25(x1203,f25(x1204,x1204)))),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1205,f6(f25(f25(f25(x1203,x1203),f25(x1203,f25(x1204,x1204))),f25(f25(x1203,x1203),f25(x1203,f25(x1204,x1204)))),a18)),a18)))))))),a18)),a18))))))))
% 0.62/0.68 [104]~P2(x1041)+P8(x1041)+~E(f6(f9(f9(x1041)),f9(f9(x1041))),f9(x1041))+~P6(f9(f9(f11(f6(x1041,a18)))),f9(f9(x1041)))
% 0.62/0.68 [103]~P2(x1031)+P3(x1031,x1032,x1033)+~E(f9(f9(x1032)),f9(x1031))+~P6(f9(f9(f11(f6(x1031,a18)))),f9(f9(x1033)))
% 0.62/0.68 [111]~P8(x1113)+~P8(x1112)+~P3(x1111,x1112,x1113)+P4(x1111,x1112,x1113)+P5(f25(f25(f16(x1111,x1112,x1113),f16(x1111,x1112,x1113)),f25(f16(x1111,x1112,x1113),f25(f17(x1111,x1112,x1113),f17(x1111,x1112,x1113)))),f9(x1112))
% 0.62/0.68 [121]~P8(x1213)+~P8(x1212)+~P3(x1211,x1212,x1213)+P4(x1211,x1212,x1213)+~E(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1213,f6(f25(f25(f25(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1211,f6(f25(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1211,f6(f25(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)),a18)),a18)))))))),f25(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1211,f6(f25(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)),a18)),a18))))))),f25(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1211,f6(f25(f17(x1211,x1212,x1213),f17(x1211,x1212,x1213)),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1211,f6(f25(f17(x1211,x1212,x1213),f17(x1211,x1212,x1213)),a18)),a18)))))))))),f25(f25(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1211,f6(f25(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1211,f6(f25(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)),a18)),a18)))))))),f25(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1211,f6(f25(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)),a18)),a18))))))),f25(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1211,f6(f25(f17(x1211,x1212,x1213),f17(x1211,x1212,x1213)),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1211,f6(f25(f17(x1211,x1212,x1213),f17(x1211,x1212,x1213)),a18)),a18))))))))))),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1211,f6(f25(f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1212,f6(f25(f25(f25(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)),f25(f16(x1211,x1212,x1213),f25(f17(x1211,x1212,x1213),f17(x1211,x1212,x1213)))),f25(f25(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)),f25(f16(x1211,x1212,x1213),f25(f17(x1211,x1212,x1213),f17(x1211,x1212,x1213))))),a18)),a18))))))),f9(f10(a5,f6(a18,f9(f9(f11(f6(f10(x1212,f6(f25(f25(f25(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)),f25(f16(x1211,x1212,x1213),f25(f17(x1211,x1212,x1213),f17(x1211,x1212,x1213)))),f25(f25(f16(x1211,x1212,x1213),f16(x1211,x1212,x1213)),f25(f16(x1211,x1212,x1213),f25(f17(x1211,x1212,x1213),f17(x1211,x1212,x1213))))),a18)),a18)))))))),a18)),a18))))))))
% 0.62/0.68 %EqnAxiom
% 0.62/0.69 [1]E(x11,x11)
% 0.62/0.69 [2]E(x22,x21)+~E(x21,x22)
% 0.62/0.69 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.62/0.69 [4]~E(x41,x42)+E(f4(x41),f4(x42))
% 0.62/0.69 [5]~E(x51,x52)+E(f9(x51),f9(x52))
% 0.62/0.69 [6]~E(x61,x62)+E(f25(x61,x63),f25(x62,x63))
% 0.62/0.69 [7]~E(x71,x72)+E(f25(x73,x71),f25(x73,x72))
% 0.62/0.69 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83))
% 0.62/0.69 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92))
% 0.62/0.69 [10]~E(x101,x102)+E(f11(x101),f11(x102))
% 0.62/0.69 [11]~E(x111,x112)+E(f10(x111,x113),f10(x112,x113))
% 0.62/0.69 [12]~E(x121,x122)+E(f10(x123,x121),f10(x123,x122))
% 0.62/0.69 [13]~E(x131,x132)+E(f7(x131,x133),f7(x132,x133))
% 0.62/0.69 [14]~E(x141,x142)+E(f7(x143,x141),f7(x143,x142))
% 0.62/0.69 [15]~E(x151,x152)+E(f16(x151,x153,x154),f16(x152,x153,x154))
% 0.62/0.69 [16]~E(x161,x162)+E(f16(x163,x161,x164),f16(x163,x162,x164))
% 0.62/0.69 [17]~E(x171,x172)+E(f16(x173,x174,x171),f16(x173,x174,x172))
% 0.62/0.69 [18]~E(x181,x182)+E(f17(x181,x183,x184),f17(x182,x183,x184))
% 0.62/0.69 [19]~E(x191,x192)+E(f17(x193,x191,x194),f17(x193,x192,x194))
% 0.62/0.69 [20]~E(x201,x202)+E(f17(x203,x204,x201),f17(x203,x204,x202))
% 0.62/0.69 [21]~E(x211,x212)+E(f8(x211),f8(x212))
% 0.62/0.69 [22]~E(x221,x222)+E(f12(x221),f12(x222))
% 0.62/0.69 [23]~E(x231,x232)+E(f15(x231,x233),f15(x232,x233))
% 0.62/0.69 [24]~E(x241,x242)+E(f15(x243,x241),f15(x243,x242))
% 0.62/0.69 [25]~E(x251,x252)+E(f20(x251),f20(x252))
% 0.62/0.69 [26]~E(x261,x262)+E(f21(x261),f21(x262))
% 0.62/0.69 [27]~E(x271,x272)+E(f3(x271),f3(x272))
% 0.62/0.69 [28]~E(x281,x282)+E(f23(x281),f23(x282))
% 0.62/0.69 [29]~P1(x291)+P1(x292)+~E(x291,x292)
% 0.62/0.69 [30]~P2(x301)+P2(x302)+~E(x301,x302)
% 0.62/0.69 [31]P5(x312,x313)+~E(x311,x312)+~P5(x311,x313)
% 0.62/0.69 [32]P5(x323,x322)+~E(x321,x322)+~P5(x323,x321)
% 0.62/0.69 [33]P6(x332,x333)+~E(x331,x332)+~P6(x331,x333)
% 0.62/0.69 [34]P6(x343,x342)+~E(x341,x342)+~P6(x343,x341)
% 0.62/0.69 [35]P4(x352,x353,x354)+~E(x351,x352)+~P4(x351,x353,x354)
% 0.62/0.69 [36]P4(x363,x362,x364)+~E(x361,x362)+~P4(x363,x361,x364)
% 0.62/0.69 [37]P4(x373,x374,x372)+~E(x371,x372)+~P4(x373,x374,x371)
% 0.62/0.69 [38]~P8(x381)+P8(x382)+~E(x381,x382)
% 0.62/0.69 [39]P3(x392,x393,x394)+~E(x391,x392)+~P3(x391,x393,x394)
% 0.62/0.69 [40]P3(x403,x402,x404)+~E(x401,x402)+~P3(x403,x401,x404)
% 0.62/0.69 [41]P3(x413,x414,x412)+~E(x411,x412)+~P3(x413,x414,x411)
% 0.62/0.69 [42]~P7(x421)+P7(x422)+~E(x421,x422)
% 0.62/0.69 [43]~P9(x431)+P9(x432)+~E(x431,x432)
% 0.62/0.69
% 0.62/0.69 %-------------------------------------------
% 0.62/0.69 cnf(146,plain,
% 0.62/0.69 ($false),
% 0.62/0.69 inference(scs_inference,[],[48,59,51,53,57,2,3,31]),
% 0.62/0.69 ['proof']).
% 0.62/0.69 % SZS output end Proof
% 0.62/0.69 % Total time :0.010000s
%------------------------------------------------------------------------------