%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET061-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 : n001.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 59.55s 59.67s
% Output : CNFRefutation 59.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SET061-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.13/0.34 % Computer : n001.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 15:08:39 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.21/0.57 start to proof:theBenchmark
% 59.52/59.66 %-------------------------------------------
% 59.52/59.66 % File :CSE---1.7
% 59.52/59.66 % Problem :theBenchmark
% 59.52/59.66 % Transform :cnf
% 59.52/59.66 % Format :tptp:raw
% 59.52/59.66 % Command :java -jar mcs_scs.jar %d %s
% 59.52/59.66
% 59.52/59.66 % Result :Theorem 58.930000s
% 59.52/59.66 % Output :CNFRefutation 58.930000s
% 59.52/59.66 %-------------------------------------------
% 59.52/59.66 %--------------------------------------------------------------------------
% 59.52/59.66 % File : SET061-7 : TPTP v8.2.0. Bugfixed v2.1.0.
% 59.52/59.67 % Domain : Set Theory
% 59.52/59.67 % Problem : Existence of the null class
% 59.52/59.67 % Version : [Qua92] axioms : Augmented.
% 59.52/59.67 % English :
% 59.52/59.67
% 59.52/59.67 % Refs : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 59.52/59.67 % Source : [Quaife]
% 59.52/59.67 % Names : SP2 [Qua92]
% 59.52/59.67
% 59.52/59.67 % Status : Unsatisfiable
% 59.52/59.67 % Rating : 0.20 v8.2.0, 0.24 v8.1.0, 0.16 v7.5.0, 0.21 v7.4.0, 0.24 v7.3.0, 0.17 v7.1.0, 0.08 v7.0.0, 0.20 v6.4.0, 0.27 v6.3.0, 0.18 v6.2.0, 0.10 v6.1.0, 0.07 v6.0.0, 0.00 v5.5.0, 0.20 v5.3.0, 0.22 v5.2.0, 0.19 v5.1.0, 0.18 v5.0.0, 0.21 v4.1.0, 0.31 v4.0.1, 0.27 v4.0.0, 0.36 v3.7.0, 0.30 v3.5.0, 0.36 v3.4.0, 0.25 v3.3.0, 0.21 v3.2.0, 0.08 v3.1.0, 0.09 v2.7.0, 0.08 v2.6.0, 0.00 v2.5.0, 0.09 v2.4.0, 0.00 v2.1.0
% 59.52/59.67 % Syntax : Number of clauses : 103 ( 32 unt; 11 nHn; 72 RR)
% 59.52/59.67 % Number of literals : 207 ( 43 equ; 95 neg)
% 59.52/59.67 % Maximal clause size : 5 ( 2 avg)
% 59.52/59.67 % Maximal term depth : 6 ( 1 avg)
% 59.52/59.67 % Number of predicates : 10 ( 9 usr; 0 prp; 1-3 aty)
% 59.52/59.67 % Number of functors : 39 ( 39 usr; 9 con; 0-3 aty)
% 59.52/59.67 % Number of variables : 206 ( 36 sgn)
% 59.52/59.67 % SPC : CNF_UNS_RFO_SEQ_NHN
% 59.52/59.67
% 59.52/59.67 % Comments : Preceding lemmas are added.
% 59.52/59.67 % Bugfixes : v2.1.0 - Bugfix in SET004-0.ax.
% 59.52/59.67 %--------------------------------------------------------------------------
% 59.52/59.67 %----Include von Neuman-Bernays-Godel set theory axioms
% 59.52/59.67 include('Axioms/SET004-0.ax').
% 59.52/59.67 %--------------------------------------------------------------------------
% 59.52/59.67 %----Corollaries to Unordered pair axiom. Not in paper, but in email.
% 59.52/59.67 cnf(corollary_1_to_unordered_pair,axiom,
% 59.52/59.67 ( ~ member(ordered_pair(X,Y),cross_product(U,V))
% 59.52/59.67 | member(X,unordered_pair(X,Y)) ) ).
% 59.55/59.67
% 59.55/59.67 cnf(corollary_2_to_unordered_pair,axiom,
% 59.55/59.67 ( ~ member(ordered_pair(X,Y),cross_product(U,V))
% 59.55/59.67 | member(Y,unordered_pair(X,Y)) ) ).
% 59.55/59.67
% 59.55/59.67 %----Corollaries to Cartesian product axiom.
% 59.55/59.67 cnf(corollary_1_to_cartesian_product,axiom,
% 59.55/59.67 ( ~ member(ordered_pair(U,V),cross_product(X,Y))
% 59.55/59.67 | member(U,universal_class) ) ).
% 59.55/59.67
% 59.55/59.67 cnf(corollary_2_to_cartesian_product,axiom,
% 59.55/59.67 ( ~ member(ordered_pair(U,V),cross_product(X,Y))
% 59.55/59.67 | member(V,universal_class) ) ).
% 59.55/59.67
% 59.55/59.67 %---- PARTIAL ORDER.
% 59.55/59.67 %----(PO1): reflexive.
% 59.55/59.67 cnf(subclass_is_reflexive,axiom,
% 59.55/59.67 subclass(X,X) ).
% 59.55/59.67
% 59.55/59.67 %----(PO2): antisymmetry is part of A-3.
% 59.55/59.67 %----(x < y), (y < x) --> (x = y).
% 59.55/59.67
% 59.55/59.67 %----(PO3): transitivity.
% 59.55/59.67 cnf(transitivity_of_subclass,axiom,
% 59.55/59.67 ( ~ subclass(X,Y)
% 59.55/59.67 | ~ subclass(Y,Z)
% 59.55/59.67 | subclass(X,Z) ) ).
% 59.55/59.67
% 59.55/59.67 %---- EQUALITY.
% 59.55/59.67 %----(EQ1): equality axiom.
% 59.55/59.67 %----a:x:(x = x).
% 59.55/59.67 %----This is always an axiom in the TPTP presentation.
% 59.55/59.67
% 59.55/59.67 %----(EQ2): expanded equality definition.
% 59.55/59.67 cnf(equality1,axiom,
% 59.55/59.67 ( X = Y
% 59.55/59.67 | member(not_subclass_element(X,Y),X)
% 59.55/59.67 | member(not_subclass_element(Y,X),Y) ) ).
% 59.55/59.67
% 59.55/59.67 cnf(equality2,axiom,
% 59.55/59.67 ( ~ member(not_subclass_element(X,Y),Y)
% 59.55/59.67 | X = Y
% 59.55/59.67 | member(not_subclass_element(Y,X),Y) ) ).
% 59.55/59.67
% 59.55/59.67 cnf(equality3,axiom,
% 59.55/59.67 ( ~ member(not_subclass_element(Y,X),X)
% 59.55/59.67 | X = Y
% 59.55/59.67 | member(not_subclass_element(X,Y),X) ) ).
% 59.55/59.67
% 59.55/59.67 cnf(equality4,axiom,
% 59.55/59.67 ( ~ member(not_subclass_element(X,Y),Y)
% 59.55/59.67 | ~ member(not_subclass_element(Y,X),X)
% 59.55/59.67 | X = Y ) ).
% 59.55/59.67
% 59.55/59.67 %---- SPECIAL CLASSES.
% 59.55/59.67 %----(SP1): lemma.
% 59.55/59.67 cnf(special_classes_lemma,axiom,
% 59.55/59.67 ~ member(Y,intersection(complement(X),X)) ).
% 59.55/59.67
% 59.55/59.67 cnf(prove_existence_of_null_class_1,negated_conjecture,
% 59.55/59.67 member(z,null_class) ).
% 59.55/59.67
% 59.55/59.67 %--------------------------------------------------------------------------
% 59.55/59.67 %-------------------------------------------
% 59.55/59.67 % Proof found
% 59.55/59.67 % SZS status Theorem for theBenchmark
% 59.55/59.67 % SZS output start Proof
% 59.55/59.67 %ClaNum:130(EqnAxiom:42)
% 59.55/59.67 %VarNum:789(SingletonVarNum:178)
% 59.55/59.67 %MaxLitNum:5
% 59.55/59.67 %MaxfuncDepth:24
% 59.55/59.67 %SharedTerms:31
% 59.55/59.67 %goalClause: 46
% 59.55/59.67 %singleGoalClaCount:1
% 59.55/59.67 [43]P1(a1)
% 59.55/59.67 [44]P2(a2)
% 59.55/59.67 [45]P5(a1,a17)
% 59.55/59.67 [46]P5(a23,a4)
% 59.55/59.67 [49]P6(a5,f6(a17,a17))
% 59.55/59.67 [50]P6(a18,f6(a17,a17))
% 59.55/59.67 [56]E(f10(f9(f11(f6(a21,a17))),a21),a13)
% 59.55/59.67 [57]E(f10(f6(a17,a17),f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17))))))),a21)
% 59.55/59.67 [47]P6(x471,a17)
% 59.55/59.67 [48]P6(x481,x481)
% 59.55/59.67 [54]P6(f19(x541),f6(f6(a17,a17),a17))
% 59.55/59.67 [55]P6(f11(x551),f6(f6(a17,a17),a17))
% 59.55/59.67 [58]E(f10(f9(x581),f8(f9(f10(f7(f9(f11(f6(a5,a17))),x581),a13)))),f3(x581))
% 59.55/59.67 [51]P5(f24(x511,x512),a17)
% 59.55/59.67 [52]P6(f7(x521,x522),f6(a17,a17))
% 59.55/59.67 [59]~P5(x591,f10(f8(x592),x592))
% 59.55/59.67 [53]E(f10(f6(x531,x532),x533),f10(x533,f6(x531,x532)))
% 59.55/59.67 [60]~P7(x601)+P2(x601)
% 59.55/59.67 [61]~P8(x611)+P2(x611)
% 59.55/59.67 [64]~P1(x641)+P6(a1,x641)
% 59.55/59.67 [65]~P1(x651)+P5(a4,x651)
% 59.55/59.67 [67]P5(f20(x671),x671)+E(x671,a4)
% 59.55/59.67 [68]~P2(x681)+P6(x681,f6(a17,a17))
% 59.55/59.67 [66]E(x661,a4)+E(f10(x661,f20(x661)),a4)
% 59.55/59.67 [77]~P8(x771)+E(f6(f9(f9(x771)),f9(f9(x771))),f9(x771))
% 59.55/59.67 [90]~P7(x901)+P2(f9(f11(f6(x901,a17))))
% 59.55/59.67 [95]~P5(x951,a17)+P5(f9(f10(a5,f6(a17,x951))),a17)
% 59.55/59.67 [97]~P9(x971)+P6(f7(x971,f9(f11(f6(x971,a17)))),a13)
% 59.55/59.67 [98]~P2(x981)+P6(f7(x981,f9(f11(f6(x981,a17)))),a13)
% 59.55/59.67 [99]~P8(x991)+P6(f9(f9(f11(f6(x991,a17)))),f9(f9(x991)))
% 59.55/59.67 [104]P9(x1041)+~P6(f7(x1041,f9(f11(f6(x1041,a17)))),a13)
% 59.55/59.67 [117]~P1(x1171)+P6(f9(f9(f11(f6(f10(a18,f6(x1171,a17)),a17)))),x1171)
% 59.55/59.67 [121]~P5(x1211,a17)+P5(f8(f9(f9(f11(f6(f10(a5,f6(f8(x1211),a17)),a17))))),a17)
% 59.55/59.67 [62]~E(x622,x621)+P6(x621,x622)
% 59.55/59.67 [63]~E(x631,x632)+P6(x631,x632)
% 59.55/59.67 [70]P6(x701,x702)+P5(f14(x701,x702),x701)
% 59.55/59.67 [71]~P5(x711,x712)+~P5(x711,f8(x712))
% 59.55/59.67 [75]~P5(x751,a17)+P5(x751,f24(x752,x751))
% 59.55/59.67 [76]~P5(x761,a17)+P5(x761,f24(x761,x762))
% 59.55/59.67 [81]P6(x811,x812)+~P5(f14(x811,x812),x812)
% 59.55/59.67 [94]~P5(x942,f9(x941))+~E(f10(x941,f6(f24(x942,x942),a17)),a4)
% 59.55/59.67 [103]P5(x1031,x1032)+~P5(f24(f24(x1031,x1031),f24(x1031,f24(x1032,x1032))),a5)
% 59.55/59.67 [114]~P5(f24(f24(x1141,x1141),f24(x1141,f24(x1142,x1142))),a18)+E(f8(f10(f8(x1141),f8(f24(x1141,x1141)))),x1142)
% 59.55/59.67 [84]P2(x841)+~P3(x841,x842,x843)
% 59.55/59.67 [85]P8(x851)+~P4(x852,x853,x851)
% 59.55/59.67 [86]P8(x861)+~P4(x862,x861,x863)
% 59.55/59.67 [93]~P4(x931,x932,x933)+P3(x931,x932,x933)
% 59.55/59.67 [79]P5(x791,x792)+~P5(x791,f10(x793,x792))
% 59.55/59.67 [80]P5(x801,x802)+~P5(x801,f10(x802,x803))
% 59.55/59.67 [87]~P3(x872,x871,x873)+E(f9(f9(x871)),f9(x872))
% 59.55/59.67 [100]~P5(x1001,f6(x1002,x1003))+E(f24(f24(f12(x1001),f12(x1001)),f24(f12(x1001),f24(f22(x1001),f22(x1001)))),x1001)
% 59.55/59.67 [102]~P3(x1021,x1023,x1022)+P6(f9(f9(f11(f6(x1021,a17)))),f9(f9(x1022)))
% 59.55/59.67 [105]P5(x1051,a17)+~P5(f24(f24(x1052,x1052),f24(x1052,f24(x1051,x1051))),f6(x1053,x1054))
% 59.55/59.67 [106]P5(x1061,a17)+~P5(f24(f24(x1061,x1061),f24(x1061,f24(x1062,x1062))),f6(x1063,x1064))
% 59.55/59.67 [107]P5(x1071,x1072)+~P5(f24(f24(x1073,x1073),f24(x1073,f24(x1071,x1071))),f6(x1074,x1072))
% 59.55/59.67 [108]P5(x1081,x1082)+~P5(f24(f24(x1081,x1081),f24(x1081,f24(x1083,x1083))),f6(x1082,x1084))
% 59.55/59.67 [110]P5(x1101,f24(x1102,x1101))+~P5(f24(f24(x1102,x1102),f24(x1102,f24(x1101,x1101))),f6(x1103,x1104))
% 59.55/59.67 [111]P5(x1111,f24(x1111,x1112))+~P5(f24(f24(x1111,x1111),f24(x1111,f24(x1112,x1112))),f6(x1113,x1114))
% 59.55/59.67 [122]~P5(f24(f24(f24(f24(x1223,x1223),f24(x1223,f24(x1221,x1221))),f24(f24(x1223,x1223),f24(x1223,f24(x1221,x1221)))),f24(f24(f24(x1223,x1223),f24(x1223,f24(x1221,x1221))),f24(x1222,x1222))),f19(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))),x1224)
% 59.55/59.67 [123]~P5(f24(f24(f24(f24(x1232,x1232),f24(x1232,f24(x1231,x1231))),f24(f24(x1232,x1232),f24(x1232,f24(x1231,x1231)))),f24(f24(f24(x1232,x1232),f24(x1232,f24(x1231,x1231))),f24(x1233,x1233))),f11(x1234))+P5(f24(f24(f24(f24(x1231,x1231),f24(x1231,f24(x1232,x1232))),f24(f24(x1231,x1231),f24(x1231,f24(x1232,x1232)))),f24(f24(f24(x1231,x1231),f24(x1231,f24(x1232,x1232))),f24(x1233,x1233))),x1234)
% 59.55/59.67 [127]~P5(f24(f24(x1274,x1274),f24(x1274,f24(x1271,x1271))),f7(x1272,x1273))+P5(x1271,f9(f9(f11(f6(f10(x1272,f6(f9(f9(f11(f6(f10(x1273,f6(f24(x1274,x1274),a17)),a17)))),a17)),a17)))))
% 59.55/59.67 [96]~P2(x961)+P7(x961)+~P2(f9(f11(f6(x961,a17))))
% 59.55/59.67 [109]P2(x1091)+~P6(x1091,f6(a17,a17))+~P6(f7(x1091,f9(f11(f6(x1091,a17)))),a13)
% 59.55/59.67 [119]P1(x1191)+~P5(a4,x1191)+~P6(f9(f9(f11(f6(f10(a18,f6(x1191,a17)),a17)))),x1191)
% 59.55/59.67 [126]~P5(x1261,a17)+E(x1261,a4)+P5(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(a2,f6(f24(x1261,x1261),a17)),a17))))))),x1261)
% 59.55/59.67 [69]~P6(x692,x691)+~P6(x691,x692)+E(x691,x692)
% 59.55/59.67 [72]P5(x721,x722)+P5(x721,f8(x722))+~P5(x721,a17)
% 59.55/59.67 [82]E(x821,x822)+P5(f14(x822,x821),x822)+P5(f14(x821,x822),x821)
% 59.55/59.67 [89]E(x891,x892)+P5(f14(x892,x891),x892)+~P5(f14(x891,x892),x892)
% 59.55/59.67 [91]E(x911,x912)+~P5(f14(x912,x911),x911)+~P5(f14(x911,x912),x912)
% 59.55/59.67 [92]P5(x922,f9(x921))+~P5(x922,a17)+E(f10(x921,f6(f24(x922,x922),a17)),a4)
% 59.55/59.67 [115]~P5(x1151,x1152)+~P5(f24(f24(x1151,x1151),f24(x1151,f24(x1152,x1152))),f6(a17,a17))+P5(f24(f24(x1151,x1151),f24(x1151,f24(x1152,x1152))),a5)
% 59.55/59.67 [116]~P5(f24(f24(x1161,x1161),f24(x1161,f24(x1162,x1162))),f6(a17,a17))+~E(f8(f10(f8(x1161),f8(f24(x1161,x1161)))),x1162)+P5(f24(f24(x1161,x1161),f24(x1161,f24(x1162,x1162))),a18)
% 59.55/59.67 [118]~P2(x1181)+~P5(x1182,a17)+P5(f9(f9(f11(f6(f10(x1181,f6(x1182,a17)),a17)))),a17)
% 59.55/59.67 [73]~P6(x731,x733)+P6(x731,x732)+~P6(x733,x732)
% 59.55/59.67 [74]~P5(x741,x743)+P5(x741,x742)+~P6(x743,x742)
% 59.55/59.67 [78]E(x781,x782)+E(x781,x783)+~P5(x781,f24(x783,x782))
% 59.55/59.67 [83]~P5(x831,x833)+~P5(x831,x832)+P5(x831,f10(x832,x833))
% 59.55/59.67 [101]~P5(x1012,x1014)+~P5(x1011,x1013)+P5(f24(f24(x1011,x1011),f24(x1011,f24(x1012,x1012))),f6(x1013,x1014))
% 59.55/59.67 [124]~P5(f24(f24(f24(f24(x1242,x1242),f24(x1242,f24(x1243,x1243))),f24(f24(x1242,x1242),f24(x1242,f24(x1243,x1243)))),f24(f24(f24(x1242,x1242),f24(x1242,f24(x1243,x1243))),f24(x1241,x1241))),x1244)+P5(f24(f24(f24(f24(x1241,x1241),f24(x1241,f24(x1242,x1242))),f24(f24(x1241,x1241),f24(x1241,f24(x1242,x1242)))),f24(f24(f24(x1241,x1241),f24(x1241,f24(x1242,x1242))),f24(x1243,x1243))),f19(x1244))+~P5(f24(f24(f24(f24(x1241,x1241),f24(x1241,f24(x1242,x1242))),f24(f24(x1241,x1241),f24(x1241,f24(x1242,x1242)))),f24(f24(f24(x1241,x1241),f24(x1241,f24(x1242,x1242))),f24(x1243,x1243))),f6(f6(a17,a17),a17))
% 59.55/59.68 [125]~P5(f24(f24(f24(f24(x1252,x1252),f24(x1252,f24(x1251,x1251))),f24(f24(x1252,x1252),f24(x1252,f24(x1251,x1251)))),f24(f24(f24(x1252,x1252),f24(x1252,f24(x1251,x1251))),f24(x1253,x1253))),x1254)+P5(f24(f24(f24(f24(x1251,x1251),f24(x1251,f24(x1252,x1252))),f24(f24(x1251,x1251),f24(x1251,f24(x1252,x1252)))),f24(f24(f24(x1251,x1251),f24(x1251,f24(x1252,x1252))),f24(x1253,x1253))),f11(x1254))+~P5(f24(f24(f24(f24(x1251,x1251),f24(x1251,f24(x1252,x1252))),f24(f24(x1251,x1251),f24(x1251,f24(x1252,x1252)))),f24(f24(f24(x1251,x1251),f24(x1251,f24(x1252,x1252))),f24(x1253,x1253))),f6(f6(a17,a17),a17))
% 59.55/59.68 [128]P5(f24(f24(x1281,x1281),f24(x1281,f24(x1282,x1282))),f7(x1283,x1284))+~P5(f24(f24(x1281,x1281),f24(x1281,f24(x1282,x1282))),f6(a17,a17))+~P5(x1282,f9(f9(f11(f6(f10(x1283,f6(f9(f9(f11(f6(f10(x1284,f6(f24(x1281,x1281),a17)),a17)))),a17)),a17)))))
% 59.55/59.68 [129]~P4(x1292,x1295,x1291)+~P5(f24(f24(x1293,x1293),f24(x1293,f24(x1294,x1294))),f9(x1295))+E(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1291,f6(f24(f24(f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1292,f6(f24(x1293,x1293),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1292,f6(f24(x1293,x1293),a17)),a17)))))))),f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1292,f6(f24(x1293,x1293),a17)),a17))))))),f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1292,f6(f24(x1294,x1294),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1292,f6(f24(x1294,x1294),a17)),a17)))))))))),f24(f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1292,f6(f24(x1293,x1293),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1292,f6(f24(x1293,x1293),a17)),a17)))))))),f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1292,f6(f24(x1293,x1293),a17)),a17))))))),f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1292,f6(f24(x1294,x1294),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1292,f6(f24(x1294,x1294),a17)),a17))))))))))),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1292,f6(f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1295,f6(f24(f24(f24(x1293,x1293),f24(x1293,f24(x1294,x1294))),f24(f24(x1293,x1293),f24(x1293,f24(x1294,x1294)))),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1295,f6(f24(f24(f24(x1293,x1293),f24(x1293,f24(x1294,x1294))),f24(f24(x1293,x1293),f24(x1293,f24(x1294,x1294)))),a17)),a17)))))))),a17)),a17))))))))
% 59.55/59.68 [113]~P2(x1131)+P8(x1131)+~E(f6(f9(f9(x1131)),f9(f9(x1131))),f9(x1131))+~P6(f9(f9(f11(f6(x1131,a17)))),f9(f9(x1131)))
% 59.55/59.68 [112]~P2(x1121)+P3(x1121,x1122,x1123)+~E(f9(f9(x1122)),f9(x1121))+~P6(f9(f9(f11(f6(x1121,a17)))),f9(f9(x1123)))
% 59.55/59.68 [120]~P8(x1203)+~P8(x1202)+~P3(x1201,x1202,x1203)+P4(x1201,x1202,x1203)+P5(f24(f24(f15(x1201,x1202,x1203),f15(x1201,x1202,x1203)),f24(f15(x1201,x1202,x1203),f24(f16(x1201,x1202,x1203),f16(x1201,x1202,x1203)))),f9(x1202))
% 59.55/59.68 [130]~P8(x1303)+~P8(x1302)+~P3(x1301,x1302,x1303)+P4(x1301,x1302,x1303)+~E(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1303,f6(f24(f24(f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1301,f6(f24(f15(x1301,x1302,x1303),f15(x1301,x1302,x1303)),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1301,f6(f24(f15(x1301,x1302,x1303),f15(x1301,x1302,x1303)),a17)),a17)))))))),f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1301,f6(f24(f15(x1301,x1302,x1303),f15(x1301,x1302,x1303)),a17)),a17))))))),f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1301,f6(f24(f16(x1301,x1302,x1303),f16(x1301,x1302,x1303)),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1301,f6(f24(f16(x1301,x1302,x1303),f16(x1301,x1302,x1303)),a17)),a17)))))))))),f24(f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1301,f6(f24(f15(x1301,x1302,x1303),f15(x1301,x1302,x1303)),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1301,f6(f24(f15(x1301,x1302,x1303),f15(x1301,x1302,x1303)),a17)),a17)))))))),f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1301,f6(f24(f15(x1301,x1302,x1303),f15(x1301,x1302,x1303)),a17)),a17))))))),f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1301,f6(f24(f16(x1301,x1302,x1303),f16(x1301,x1302,x1303)),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1301,f6(f24(f16(x1301,x1302,x1303),f16(x1301,x1302,x1303)),a17)),a17))))))))))),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1301,f6(f24(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1302,f6(f24(f24(f24(f15(x1301,x1302,x1303),f15(x1301,x1302,x1303)),f24(f15(x1301,x1302,x1303),f24(f16(x1301,x1302,x1303),f16(x1301,x1302,x1303)))),f24(f24(f15(x1301,x1302,x1303),f15(x1301,x1302,x1303)),f24(f15(x1301,x1302,x1303),f24(f16(x1301,x1302,x1303),f16(x1301,x1302,x1303))))),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1302,f6(f24(f24(f24(f15(x1301,x1302,x1303),f15(x1301,x1302,x1303)),f24(f15(x1301,x1302,x1303),f24(f16(x1301,x1302,x1303),f16(x1301,x1302,x1303)))),f24(f24(f15(x1301,x1302,x1303),f15(x1301,x1302,x1303)),f24(f15(x1301,x1302,x1303),f24(f16(x1301,x1302,x1303),f16(x1301,x1302,x1303))))),a17)),a17)))))))),a17)),a17))))))))
% 59.55/59.68 %EqnAxiom
% 59.55/59.68 [1]E(x11,x11)
% 59.55/59.68 [2]E(x22,x21)+~E(x21,x22)
% 59.55/59.68 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.55/59.68 [4]~E(x41,x42)+E(f6(x41,x43),f6(x42,x43))
% 59.55/59.68 [5]~E(x51,x52)+E(f6(x53,x51),f6(x53,x52))
% 59.55/59.68 [6]~E(x61,x62)+E(f9(x61),f9(x62))
% 59.55/59.68 [7]~E(x71,x72)+E(f24(x71,x73),f24(x72,x73))
% 59.55/59.68 [8]~E(x81,x82)+E(f24(x83,x81),f24(x83,x82))
% 59.55/59.68 [9]~E(x91,x92)+E(f7(x91,x93),f7(x92,x93))
% 59.55/59.68 [10]~E(x101,x102)+E(f7(x103,x101),f7(x103,x102))
% 59.55/59.68 [11]~E(x111,x112)+E(f10(x111,x113),f10(x112,x113))
% 59.55/59.68 [12]~E(x121,x122)+E(f10(x123,x121),f10(x123,x122))
% 59.55/59.68 [13]~E(x131,x132)+E(f11(x131),f11(x132))
% 59.55/59.68 [14]~E(x141,x142)+E(f16(x141,x143,x144),f16(x142,x143,x144))
% 59.55/59.68 [15]~E(x151,x152)+E(f16(x153,x151,x154),f16(x153,x152,x154))
% 59.55/59.68 [16]~E(x161,x162)+E(f16(x163,x164,x161),f16(x163,x164,x162))
% 59.55/59.68 [17]~E(x171,x172)+E(f15(x171,x173,x174),f15(x172,x173,x174))
% 59.55/59.68 [18]~E(x181,x182)+E(f15(x183,x181,x184),f15(x183,x182,x184))
% 59.55/59.68 [19]~E(x191,x192)+E(f15(x193,x194,x191),f15(x193,x194,x192))
% 59.55/59.68 [20]~E(x201,x202)+E(f8(x201),f8(x202))
% 59.55/59.68 [21]~E(x211,x212)+E(f19(x211),f19(x212))
% 59.55/59.68 [22]~E(x221,x222)+E(f14(x221,x223),f14(x222,x223))
% 59.55/59.68 [23]~E(x231,x232)+E(f14(x233,x231),f14(x233,x232))
% 59.55/59.68 [24]~E(x241,x242)+E(f22(x241),f22(x242))
% 59.55/59.68 [25]~E(x251,x252)+E(f12(x251),f12(x252))
% 59.55/59.68 [26]~E(x261,x262)+E(f3(x261),f3(x262))
% 59.55/59.68 [27]~E(x271,x272)+E(f20(x271),f20(x272))
% 59.55/59.68 [28]~P1(x281)+P1(x282)+~E(x281,x282)
% 59.55/59.68 [29]~P2(x291)+P2(x292)+~E(x291,x292)
% 59.55/59.68 [30]P5(x302,x303)+~E(x301,x302)+~P5(x301,x303)
% 59.55/59.68 [31]P5(x313,x312)+~E(x311,x312)+~P5(x313,x311)
% 59.55/59.68 [32]P3(x322,x323,x324)+~E(x321,x322)+~P3(x321,x323,x324)
% 59.55/59.68 [33]P3(x333,x332,x334)+~E(x331,x332)+~P3(x333,x331,x334)
% 59.55/59.68 [34]P3(x343,x344,x342)+~E(x341,x342)+~P3(x343,x344,x341)
% 59.55/59.68 [35]P6(x352,x353)+~E(x351,x352)+~P6(x351,x353)
% 59.55/59.68 [36]P6(x363,x362)+~E(x361,x362)+~P6(x363,x361)
% 59.55/59.68 [37]~P7(x371)+P7(x372)+~E(x371,x372)
% 59.55/59.68 [38]P4(x382,x383,x384)+~E(x381,x382)+~P4(x381,x383,x384)
% 59.55/59.68 [39]P4(x393,x392,x394)+~E(x391,x392)+~P4(x393,x391,x394)
% 59.55/59.68 [40]P4(x403,x404,x402)+~E(x401,x402)+~P4(x403,x404,x401)
% 59.55/59.68 [41]~P8(x411)+P8(x412)+~E(x411,x412)
% 59.55/59.68 [42]~P9(x421)+P9(x422)+~E(x421,x422)
% 59.55/59.68
% 59.55/59.68 %-------------------------------------------
% 59.55/59.68 cnf(136,plain,
% 59.55/59.68 (~P5(x1361,f10(f8(x1362),x1362))),
% 59.55/59.68 inference(rename_variables,[],[59])).
% 59.55/59.68 cnf(138,plain,
% 59.55/59.68 (P6(f10(f8(x1381),x1381),x1382)),
% 59.55/59.68 inference(scs_inference,[],[59,136,65,70])).
% 59.55/59.68 cnf(139,plain,
% 59.55/59.68 (~P5(x1391,f10(f8(x1392),x1392))),
% 59.55/59.68 inference(rename_variables,[],[59])).
% 59.55/59.68 cnf(141,plain,
% 59.55/59.68 (~P5(f24(f24(f24(f24(x1411,x1411),f24(x1411,f24(x1412,x1412))),f24(f24(x1411,x1411),f24(x1411,f24(x1412,x1412)))),f24(f24(f24(x1411,x1411),f24(x1411,f24(x1412,x1412))),f24(x1413,x1413))),f19(f10(f8(x1414),x1414)))),
% 59.55/59.68 inference(scs_inference,[],[59,136,139,65,70,122])).
% 59.55/59.68 cnf(142,plain,
% 59.55/59.68 (~P5(x1421,f10(f8(x1422),x1422))),
% 59.55/59.68 inference(rename_variables,[],[59])).
% 59.55/59.68 cnf(144,plain,
% 59.55/59.68 (~P5(f24(f24(f24(f24(x1441,x1441),f24(x1441,f24(x1442,x1442))),f24(f24(x1441,x1441),f24(x1441,f24(x1442,x1442)))),f24(f24(f24(x1441,x1441),f24(x1441,f24(x1442,x1442))),f24(x1443,x1443))),f11(f10(f8(x1444),x1444)))),
% 59.55/59.68 inference(scs_inference,[],[59,136,139,142,65,70,122,123])).
% 59.55/59.68 cnf(145,plain,
% 59.55/59.68 (~P5(x1451,f10(f8(x1452),x1452))),
% 59.55/59.68 inference(rename_variables,[],[59])).
% 59.55/59.68 cnf(147,plain,
% 59.55/59.68 (E(f10(x1471,f6(x1472,x1473)),f10(f6(x1472,x1473),x1471))),
% 59.55/59.68 inference(scs_inference,[],[53,59,136,139,142,65,70,122,123,2])).
% 59.55/59.68 cnf(148,plain,
% 59.55/59.68 (P5(a23,a17)),
% 59.55/59.68 inference(scs_inference,[],[46,47,53,59,136,139,142,65,70,122,123,2,74])).
% 59.55/59.68 cnf(151,plain,
% 59.55/59.68 (~P5(a23,f8(a4))),
% 59.55/59.68 inference(scs_inference,[],[46,47,53,59,136,139,142,145,65,70,122,123,2,74,83])).
% 59.55/59.68 cnf(152,plain,
% 59.55/59.68 (~P5(x1521,f10(f8(x1522),x1522))),
% 59.55/59.68 inference(rename_variables,[],[59])).
% 59.55/59.68 cnf(157,plain,
% 59.55/59.68 (E(f10(f6(x1571,x1572),x1573),f10(x1573,f6(x1571,x1572)))),
% 59.55/59.68 inference(rename_variables,[],[53])).
% 59.55/59.68 cnf(159,plain,
% 59.55/59.68 (P6(x1591,x1591)),
% 59.55/59.68 inference(rename_variables,[],[48])).
% 59.55/59.68 cnf(160,plain,
% 59.55/59.68 (P6(f10(f6(x1601,x1602),x1603),f10(x1603,f6(x1601,x1602)))),
% 59.55/59.68 inference(scs_inference,[],[46,48,159,47,53,157,59,136,139,142,145,152,65,70,122,123,2,74,83,31,3,35,36])).
% 59.55/59.68 cnf(162,plain,
% 59.55/59.68 (~P1(f10(f6(x1621,x1622),f8(f6(x1621,x1622))))),
% 59.55/59.68 inference(scs_inference,[],[46,48,159,47,53,157,59,136,139,142,145,152,65,70,122,123,2,74,83,31,3,35,36,28])).
% 59.55/59.68 cnf(174,plain,
% 59.55/59.68 (~P5(f24(f24(f24(f24(x1741,x1741),f24(x1741,f24(x1742,x1742))),f24(f24(x1741,x1741),f24(x1741,f24(x1742,x1742)))),f24(f24(f24(x1741,x1741),f24(x1741,f24(x1742,x1742))),f24(x1743,x1743))),f19(f19(f10(f8(x1744),x1744))))),
% 59.55/59.68 inference(scs_inference,[],[141,123,122])).
% 59.55/59.68 cnf(176,plain,
% 59.55/59.68 (E(a13,f10(f9(f11(f6(a21,a17))),a21))),
% 59.55/59.68 inference(scs_inference,[],[141,56,123,122,2])).
% 59.55/59.68 cnf(179,plain,
% 59.55/59.68 (P6(f10(f6(x1791,x1792),x1793),f10(x1793,f6(x1791,x1792)))),
% 59.55/59.68 inference(rename_variables,[],[160])).
% 59.55/59.68 cnf(181,plain,
% 59.55/59.68 (~P5(x1811,f10(f6(x1812,x1813),f8(f6(x1812,x1813))))),
% 59.55/59.68 inference(scs_inference,[],[160,179,138,141,56,59,123,122,2,73,74])).
% 59.55/59.68 cnf(183,plain,
% 59.55/59.68 (~P5(x1831,f10(f8(x1832),x1832))),
% 59.55/59.68 inference(rename_variables,[],[59])).
% 59.55/59.68 cnf(185,plain,
% 59.55/59.68 (E(f10(f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17)))))),f6(a17,a17)),a21)),
% 59.55/59.68 inference(scs_inference,[],[147,160,179,138,141,56,57,59,123,122,2,73,74,3])).
% 59.55/59.68 cnf(187,plain,
% 59.55/59.68 (~E(a4,f8(a4))),
% 59.55/59.68 inference(scs_inference,[],[46,151,147,160,179,138,141,56,57,59,123,122,2,73,74,3,31])).
% 59.55/59.68 cnf(188,plain,
% 59.55/59.68 (E(f10(f8(x1881),x1881),f10(f6(x1882,x1883),f8(f6(x1882,x1883))))),
% 59.55/59.68 inference(scs_inference,[],[46,151,147,160,179,138,141,56,57,59,183,123,122,2,73,74,3,31,82])).
% 59.55/59.68 cnf(202,plain,
% 59.55/59.68 (~P5(f24(f24(f24(f24(x2021,x2021),f24(x2021,f24(x2022,x2022))),f24(f24(x2021,x2021),f24(x2021,f24(x2022,x2022)))),f24(f24(f24(x2021,x2021),f24(x2021,f24(x2022,x2022))),f24(x2023,x2023))),f11(f10(f6(x2024,x2025),f8(f6(x2024,x2025)))))),
% 59.55/59.68 inference(scs_inference,[],[181,123])).
% 59.55/59.68 cnf(203,plain,
% 59.55/59.68 (~P5(x2031,f10(f6(x2032,x2033),f8(f6(x2032,x2033))))),
% 59.55/59.68 inference(rename_variables,[],[181])).
% 59.55/59.68 cnf(205,plain,
% 59.55/59.68 (~P5(f24(f24(f24(f24(x2051,x2051),f24(x2051,f24(x2052,x2052))),f24(f24(x2051,x2051),f24(x2051,f24(x2052,x2052)))),f24(f24(f24(x2051,x2051),f24(x2051,f24(x2052,x2052))),f24(x2053,x2053))),f19(f10(f6(x2054,x2055),f8(f6(x2054,x2055)))))),
% 59.55/59.68 inference(scs_inference,[],[181,203,123,122])).
% 59.55/59.68 cnf(206,plain,
% 59.55/59.68 (~P5(x2061,f10(f6(x2062,x2063),f8(f6(x2062,x2063))))),
% 59.55/59.68 inference(rename_variables,[],[181])).
% 59.55/59.68 cnf(209,plain,
% 59.55/59.68 (~E(a17,f10(f6(x2091,x2092),f8(f6(x2091,x2092))))),
% 59.55/59.68 inference(scs_inference,[],[181,203,206,45,188,123,122,2,31])).
% 59.55/59.68 cnf(230,plain,
% 59.55/59.68 (~E(a17,f8(a4))),
% 59.55/59.68 inference(scs_inference,[],[151,148,209,188,185,144,123,122,2,3,31])).
% 59.55/59.68 cnf(253,plain,
% 59.55/59.68 (~P5(f24(f24(f24(f24(x2531,x2531),f24(x2531,f24(x2532,x2532))),f24(f24(x2531,x2531),f24(x2531,f24(x2532,x2532)))),f24(f24(f24(x2531,x2531),f24(x2531,f24(x2532,x2532))),f24(x2533,x2533))),f19(f19(f19(f10(f8(x2534),x2534)))))),
% 59.55/59.68 inference(scs_inference,[],[174,123,122])).
% 59.55/59.68 cnf(290,plain,
% 59.55/59.68 (~P5(f24(f24(f24(f24(x2901,x2901),f24(x2901,f24(x2902,x2902))),f24(f24(x2901,x2901),f24(x2901,f24(x2902,x2902)))),f24(f24(f24(x2901,x2901),f24(x2901,f24(x2902,x2902))),f24(x2903,x2903))),f11(f11(f10(f6(x2904,x2905),f8(f6(x2904,x2905))))))),
% 59.55/59.68 inference(scs_inference,[],[202,123])).
% 59.55/59.68 cnf(305,plain,
% 59.55/59.68 (P6(x3051,x3052)+~E(a17,x3052)),
% 59.55/59.68 inference(scs_inference,[],[47,205,123,122,36])).
% 59.55/59.68 cnf(348,plain,
% 59.55/59.68 (~P5(f24(f24(f24(f24(x3481,x3481),f24(x3481,f24(x3482,x3482))),f24(f24(x3481,x3481),f24(x3481,f24(x3482,x3482)))),f24(f24(f24(x3481,x3481),f24(x3481,f24(x3482,x3482))),f24(x3483,x3483))),f11(f19(f19(f19(f10(f8(x3484),x3484))))))),
% 59.55/59.68 inference(scs_inference,[],[253,123])).
% 59.55/59.68 cnf(432,plain,
% 59.55/59.68 (~P5(f24(f24(f24(f24(x4321,x4321),f24(x4321,f24(x4322,x4322))),f24(f24(x4321,x4321),f24(x4321,f24(x4322,x4322)))),f24(f24(f24(x4321,x4321),f24(x4321,f24(x4322,x4322))),f24(x4323,x4323))),f19(f11(f11(f10(f6(x4324,x4325),f8(f6(x4324,x4325)))))))),
% 59.55/59.68 inference(scs_inference,[],[290,123,122])).
% 59.55/59.68 cnf(587,plain,
% 59.55/59.68 (~P5(f24(f24(f24(f24(x5871,x5871),f24(x5871,f24(x5872,x5872))),f24(f24(x5871,x5871),f24(x5871,f24(x5872,x5872)))),f24(f24(f24(x5871,x5871),f24(x5871,f24(x5872,x5872))),f24(x5873,x5873))),f19(f11(f19(f19(f19(f10(f8(x5874),x5874)))))))),
% 59.55/59.68 inference(scs_inference,[],[348,123,122])).
% 59.55/59.68 cnf(736,plain,
% 59.55/59.68 (~P5(f24(f24(f24(f24(x7361,x7361),f24(x7361,f24(x7362,x7362))),f24(f24(x7361,x7361),f24(x7361,f24(x7362,x7362)))),f24(f24(f24(x7361,x7361),f24(x7361,f24(x7362,x7362))),f24(x7363,x7363))),f11(f19(f11(f11(f10(f6(x7364,x7365),f8(f6(x7364,x7365))))))))),
% 59.55/59.68 inference(scs_inference,[],[432,123])).
% 59.55/59.68 cnf(738,plain,
% 59.55/59.68 (~P5(f24(f24(f24(f24(x7381,x7381),f24(x7381,f24(x7382,x7382))),f24(f24(x7381,x7381),f24(x7381,f24(x7382,x7382)))),f24(f24(f24(x7381,x7381),f24(x7381,f24(x7382,x7382))),f24(x7383,x7383))),f19(f19(f11(f11(f10(f6(x7384,x7385),f8(f6(x7384,x7385))))))))),
% 59.55/59.68 inference(scs_inference,[],[432,123,122])).
% 59.55/59.68 cnf(832,plain,
% 59.55/59.68 (~P5(f24(f24(f24(f24(x8321,x8321),f24(x8321,f24(x8322,x8322))),f24(f24(x8321,x8321),f24(x8321,f24(x8322,x8322)))),f24(f24(f24(x8321,x8321),f24(x8321,f24(x8322,x8322))),f24(x8323,x8323))),f11(f19(f11(f19(f19(f19(f10(f8(x8324),x8324))))))))),
% 59.55/59.69 inference(scs_inference,[],[587,123])).
% 59.55/59.69 cnf(973,plain,
% 59.55/59.69 (E(f3(x9731),f10(f9(x9731),f8(f9(f10(f7(f9(f11(f6(a5,a17))),x9731),a13)))))),
% 59.55/59.69 inference(scs_inference,[],[58,2])).
% 59.55/59.69 cnf(986,plain,
% 59.55/59.69 (E(f6(f10(f6(x9861,x9862),f8(f6(x9861,x9862))),x9863),f6(a4,x9863))),
% 59.55/59.69 inference(scs_inference,[],[181,67,4])).
% 59.55/59.69 cnf(987,plain,
% 59.55/59.69 (E(f6(a4,x9871),f6(f10(f6(x9872,x9873),f8(f6(x9872,x9873))),x9871))),
% 59.55/59.69 inference(scs_inference,[],[986,2])).
% 59.55/59.69 cnf(1001,plain,
% 59.55/59.69 (E(f6(f10(f6(x10011,x10012),f8(f6(x10011,x10012))),x10013),f6(f10(f6(x10014,x10015),f8(f6(x10014,x10015))),x10013))),
% 59.55/59.69 inference(scs_inference,[],[736,987,986,122,123,3])).
% 59.55/59.69 cnf(1013,plain,
% 59.55/59.69 (~P5(f24(f24(f24(f24(x10131,x10131),f24(x10131,f24(x10132,x10132))),f24(f24(x10131,x10131),f24(x10131,f24(x10132,x10132)))),f24(f24(f24(x10131,x10131),f24(x10131,f24(x10132,x10132))),f24(x10133,x10133))),f19(f19(f19(f11(f11(f10(f6(x10134,x10135),f8(f6(x10134,x10135)))))))))),
% 59.55/59.69 inference(scs_inference,[],[738,122])).
% 59.55/59.69 cnf(1075,plain,
% 59.55/59.69 (~P5(a4,f8(a1))),
% 59.55/59.69 inference(scs_inference,[],[43,71,65])).
% 59.55/59.69 cnf(1076,plain,
% 59.55/59.69 (~P1(f8(a1))),
% 59.55/59.69 inference(scs_inference,[],[1075,65])).
% 59.55/59.69 cnf(1265,plain,
% 59.55/59.69 (~P5(f24(f24(f24(f24(x12651,x12651),f24(x12651,f24(x12652,x12652))),f24(f24(x12651,x12651),f24(x12651,f24(x12652,x12652)))),f24(f24(f24(x12651,x12651),f24(x12651,f24(x12652,x12652))),f24(x12653,x12653))),f19(f11(f19(f11(f19(f19(f19(f10(f8(x12654),x12654)))))))))),
% 59.55/59.69 inference(scs_inference,[],[832,123,122])).
% 59.55/59.69 cnf(1446,plain,
% 59.55/59.69 (E(f9(f6(x14461,f3(x14462))),f9(f6(x14461,f10(f9(x14462),f8(f9(f10(f7(f9(f11(f6(a5,a17))),x14462),a13)))))))),
% 59.55/59.69 inference(scs_inference,[],[973,6,5])).
% 59.55/59.69 cnf(1450,plain,
% 59.55/59.69 (~P5(f24(f24(f24(f24(x14501,x14501),f24(x14501,f24(x14502,x14502))),f24(f24(x14501,x14501),f24(x14501,f24(x14502,x14502)))),f24(f24(f24(x14501,x14501),f24(x14501,f24(x14502,x14502))),f24(x14503,x14503))),f11(f19(f19(f19(f11(f11(f10(f6(x14504,x14505),f8(f6(x14504,x14505))))))))))),
% 59.55/59.69 inference(scs_inference,[],[1013,1446,2,122,123])).
% 59.55/59.69 cnf(1992,plain,
% 59.55/59.69 (E(f20(f16(f10(f6(x19921,x19922),x19923),x19924,x19925)),f20(f16(f10(x19923,f6(x19921,x19922)),x19924,x19925)))),
% 59.55/59.69 inference(scs_inference,[],[53,27,14])).
% 59.55/59.69 cnf(1993,plain,
% 59.55/59.69 (E(f20(f16(f10(x19931,f6(x19932,x19933)),x19934,x19935)),f20(f16(f10(f6(x19932,x19933),x19931),x19934,x19935)))),
% 59.55/59.69 inference(scs_inference,[],[1992,2])).
% 59.55/59.69 cnf(2106,plain,
% 59.55/59.69 (~P5(a1,f8(f24(x21061,a1)))),
% 59.55/59.69 inference(scs_inference,[],[45,75,71])).
% 59.55/59.69 cnf(2111,plain,
% 59.55/59.69 (P5(a1,f24(x21111,a1))),
% 59.55/59.69 inference(scs_inference,[],[45,2106,1265,122,123,72])).
% 59.55/59.69 cnf(2184,plain,
% 59.55/59.69 (~P5(a23,f8(f24(a23,x21841)))),
% 59.55/59.69 inference(scs_inference,[],[148,76,71])).
% 59.55/59.69 cnf(2565,plain,
% 59.55/59.69 (~P5(a1,f8(a17))),
% 59.55/59.69 inference(scs_inference,[],[45,1993,48,59,1450,122,123,35,83])).
% 59.55/59.69 cnf(2941,plain,
% 59.55/59.69 (P6(a13,f10(f9(f11(f6(a21,a17))),a21))),
% 59.55/59.69 inference(scs_inference,[],[176,62,63])).
% 59.55/59.69 cnf(2943,plain,
% 59.55/59.69 (~P5(f24(x29431,x29432),f8(a17))),
% 59.55/59.69 inference(scs_inference,[],[51,176,62,63,71])).
% 59.55/59.69 cnf(2951,plain,
% 59.55/59.69 (P5(f24(x29511,x29512),f24(x29513,f24(x29511,x29512)))),
% 59.55/59.69 inference(scs_inference,[],[2565,44,51,176,62,63,71,79,80,68,75])).
% 59.55/59.69 cnf(2979,plain,
% 59.55/59.69 (P6(f7(a2,f9(f11(f6(a2,a17)))),a13)),
% 59.55/59.69 inference(scs_inference,[],[2565,1001,44,51,176,62,63,71,79,80,68,75,76,6,13,20,21,24,25,26,27,4,5,7,8,9,10,11,12,22,23,14,15,16,17,18,19,98])).
% 59.55/59.69 cnf(2981,plain,
% 59.55/59.69 (P5(f9(f10(a5,f6(a17,f24(x29811,x29812)))),a17)),
% 59.55/59.69 inference(scs_inference,[],[2565,1001,44,51,176,62,63,71,79,80,68,75,76,6,13,20,21,24,25,26,27,4,5,7,8,9,10,11,12,22,23,14,15,16,17,18,19,98,95])).
% 59.55/59.69 cnf(2991,plain,
% 59.55/59.69 (E(f10(f8(x29911),x29911),a4)),
% 59.55/59.69 inference(scs_inference,[],[2565,1001,44,51,43,176,59,62,63,71,79,80,68,75,76,6,13,20,21,24,25,26,27,4,5,7,8,9,10,11,12,22,23,14,15,16,17,18,19,98,95,103,107,108,117,67])).
% 59.55/59.69 cnf(2994,plain,
% 59.55/59.69 (P5(a4,a1)),
% 59.55/59.69 inference(scs_inference,[],[2565,1001,44,51,43,176,59,62,63,71,79,80,68,75,76,6,13,20,21,24,25,26,27,4,5,7,8,9,10,11,12,22,23,14,15,16,17,18,19,98,95,103,107,108,117,67,65])).
% 59.55/59.69 cnf(3001,plain,
% 59.55/59.69 (~P5(a4,f24(f8(a4),f8(a4)))),
% 59.55/59.69 inference(scs_inference,[],[46,187,2565,1001,44,51,43,176,59,62,63,71,79,80,68,75,76,6,13,20,21,24,25,26,27,4,5,7,8,9,10,11,12,22,23,14,15,16,17,18,19,98,95,103,107,108,117,67,65,2,101,118,78])).
% 59.55/59.69 cnf(3003,plain,
% 59.55/59.69 (~E(f24(x30031,a1),f8(a17))),
% 59.55/59.69 inference(scs_inference,[],[46,187,2565,2111,1001,44,51,43,176,59,62,63,71,79,80,68,75,76,6,13,20,21,24,25,26,27,4,5,7,8,9,10,11,12,22,23,14,15,16,17,18,19,98,95,103,107,108,117,67,65,2,101,118,78,31])).
% 59.55/59.69 cnf(3004,plain,
% 59.55/59.69 (~P6(a4,f8(f24(a23,x30041)))),
% 59.55/59.69 inference(scs_inference,[],[46,187,2565,2111,1001,44,2184,51,43,176,59,62,63,71,79,80,68,75,76,6,13,20,21,24,25,26,27,4,5,7,8,9,10,11,12,22,23,14,15,16,17,18,19,98,95,103,107,108,117,67,65,2,101,118,78,31,74])).
% 59.55/59.69 cnf(3006,plain,
% 59.55/59.69 (~P6(a17,f8(a4))),
% 59.55/59.69 inference(scs_inference,[],[46,187,230,2565,2111,1001,44,2184,51,43,176,59,47,62,63,71,79,80,68,75,76,6,13,20,21,24,25,26,27,4,5,7,8,9,10,11,12,22,23,14,15,16,17,18,19,98,95,103,107,108,117,67,65,2,101,118,78,31,74,69])).
% 59.55/59.69 cnf(3009,plain,
% 59.55/59.69 (~E(f8(a4),f10(f8(x30091),x30091))),
% 59.55/59.69 inference(scs_inference,[],[46,187,230,2565,2111,1001,44,2184,51,43,176,59,47,62,63,71,79,80,68,75,76,6,13,20,21,24,25,26,27,4,5,7,8,9,10,11,12,22,23,14,15,16,17,18,19,98,95,103,107,108,117,67,65,2,101,118,78,31,74,69,3])).
% 59.55/59.69 cnf(3010,plain,
% 59.55/59.69 (P5(a23,f10(a4,a4))),
% 59.55/59.69 inference(scs_inference,[],[46,187,230,2565,2111,1001,44,2184,51,43,176,59,47,62,63,71,79,80,68,75,76,6,13,20,21,24,25,26,27,4,5,7,8,9,10,11,12,22,23,14,15,16,17,18,19,98,95,103,107,108,117,67,65,2,101,118,78,31,74,69,3,83])).
% 59.55/59.69 cnf(3012,plain,
% 59.55/59.69 (~P5(f10(f8(x30121),x30121),f8(a1))),
% 59.55/59.69 inference(scs_inference,[],[46,187,230,2565,2111,1001,44,2184,51,43,176,59,1075,47,62,63,71,79,80,68,75,76,6,13,20,21,24,25,26,27,4,5,7,8,9,10,11,12,22,23,14,15,16,17,18,19,98,95,103,107,108,117,67,65,2,101,118,78,31,74,69,3,83,30])).
% 59.55/59.69 cnf(3017,plain,
% 59.55/59.69 (E(f10(f8(a4),f20(f8(a4))),a4)),
% 59.55/59.69 inference(scs_inference,[],[46,187,230,1076,2565,2111,1001,44,2184,51,43,148,176,59,1075,47,62,63,71,79,80,68,75,76,6,13,20,21,24,25,26,27,4,5,7,8,9,10,11,12,22,23,14,15,16,17,18,19,98,95,103,107,108,117,67,65,2,101,118,78,31,74,69,3,83,30,72,28,305,66])).
% 59.55/59.69 cnf(3047,plain,
% 59.55/59.69 (P6(a4,f10(f8(x30471),x30471))),
% 59.55/59.69 inference(scs_inference,[],[2943,3010,2991,71,107,103,80,62])).
% 59.55/59.69 cnf(3059,plain,
% 59.55/59.69 (E(f16(x30591,f10(f8(x30592),x30592),x30593),f16(x30591,a4,x30593))),
% 59.55/59.69 inference(scs_inference,[],[2943,3010,2991,3017,2981,71,107,103,80,62,75,63,108,95,79,15])).
% 59.55/59.69 cnf(3090,plain,
% 59.55/59.69 (P5(f14(a17,f8(a4)),a17)),
% 59.55/59.69 inference(scs_inference,[],[2943,3010,3006,2991,3017,2981,181,71,107,103,80,62,75,63,108,95,79,15,7,11,22,76,25,12,23,27,24,21,6,26,10,18,16,67,19,14,17,20,8,9,5,13,4,81,70])).
% 59.55/59.69 cnf(3100,plain,
% 59.55/59.69 (P6(f10(f8(x31001),x31001),x31002)),
% 59.55/59.69 inference(rename_variables,[],[138])).
% 59.55/59.69 cnf(3101,plain,
% 59.55/59.69 (~P6(f24(x31011,f24(x31012,x31013)),f8(a17))),
% 59.55/59.69 inference(scs_inference,[],[2994,2943,3003,3010,3006,2951,2991,3017,2981,2941,2979,138,181,71,107,103,80,62,75,63,108,95,79,15,7,11,22,76,25,12,23,27,24,21,6,26,10,18,16,67,19,14,17,20,8,9,5,13,4,81,70,2,101,78,73,35,74])).
% 59.55/59.69 cnf(3102,plain,
% 59.55/59.69 (~P5(f24(x31021,x31022),f8(a17))),
% 59.55/59.69 inference(rename_variables,[],[2943])).
% 59.55/59.69 cnf(3108,plain,
% 59.55/59.69 (P5(a4,f10(a1,a1))),
% 59.55/59.69 inference(scs_inference,[],[2994,2943,3102,3003,3010,3006,2951,2991,3017,2981,2941,2979,138,151,51,181,71,107,103,80,62,75,63,108,95,79,15,7,11,22,76,25,12,23,27,24,21,6,26,10,18,16,67,19,14,17,20,8,9,5,13,4,81,70,2,101,78,73,35,74,72,31,83])).
% 59.55/59.69 cnf(3113,plain,
% 59.55/59.69 (~E(a4,a17)),
% 59.55/59.69 inference(scs_inference,[],[2994,2943,3102,3003,3010,3006,2951,3009,2991,3017,2981,2941,2979,138,3100,151,51,181,71,107,103,80,62,75,63,108,95,79,15,7,11,22,76,25,12,23,27,24,21,6,26,10,18,16,67,19,14,17,20,8,9,5,13,4,81,70,2,101,78,73,35,74,72,31,83,69,3])).
% 59.55/59.69 cnf(3114,plain,
% 59.55/59.69 (E(f10(f8(x31141),x31141),a4)),
% 59.55/59.69 inference(rename_variables,[],[2991])).
% 59.55/59.69 cnf(3117,plain,
% 59.55/59.69 (~P6(a17,f8(f10(f8(x31171),x31171)))),
% 59.55/59.69 inference(scs_inference,[],[2994,2943,3102,3003,3010,3006,2951,3009,2991,3114,3001,162,3017,2981,2941,2979,138,3100,151,43,51,181,71,107,103,80,62,75,63,108,95,79,15,7,11,22,76,25,12,23,27,24,21,6,26,10,18,16,67,19,14,17,20,8,9,5,13,4,81,70,2,101,78,73,35,74,72,31,83,69,3,28,30,36])).
% 59.55/59.69 cnf(3186,plain,
% 59.55/59.69 ($false),
% 59.55/59.69 inference(scs_inference,[],[3113,3108,3012,3101,3047,3004,3090,3059,3117,138,103,71,62,107,75,63,80,95,108,76,27,22,79,11,7,25,26,18,19,15,10,305,9,16,6,4,13,24,12,14,20,23,21,17,8,5,81,70,2,101,78,73]),
% 59.55/59.69 ['proof']).
% 59.55/59.69 % SZS output end Proof
% 59.55/59.69 % Total time :58.930000s
%------------------------------------------------------------------------------