%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET084-7 : 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 : n032.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:36 EDT 2024
% Result : Unsatisfiable 59.27s 59.40s
% Output : CNFRefutation 59.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.08 % Problem : SET084-7 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.02/0.08 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.06/0.26 % Computer : n032.cluster.edu
% 0.06/0.26 % Model : x86_64 x86_64
% 0.06/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.26 % Memory : 8042.1875MB
% 0.06/0.26 % OS : Linux 3.10.0-693.el7.x86_64
% 0.06/0.26 % CPULimit : 300
% 0.06/0.26 % WCLimit : 300
% 0.06/0.26 % DateTime : Sun Jun 23 14:05:23 EDT 2024
% 0.06/0.26 % CPUTime :
% 0.11/0.43 start to proof:theBenchmark
% 59.27/59.39 %-------------------------------------------
% 59.27/59.39 % File :CSE---1.7
% 59.27/59.39 % Problem :theBenchmark
% 59.27/59.39 % Transform :cnf
% 59.27/59.39 % Format :tptp:raw
% 59.27/59.39 % Command :java -jar mcs_scs.jar %d %s
% 59.27/59.39
% 59.27/59.39 % Result :Theorem 58.900000s
% 59.27/59.39 % Output :CNFRefutation 58.900000s
% 59.27/59.39 %-------------------------------------------
% 59.27/59.40 %--------------------------------------------------------------------------
% 59.27/59.40 % File : SET084-7 : TPTP v8.2.0. Bugfixed v2.1.0.
% 59.27/59.40 % Domain : Set Theory
% 59.27/59.40 % Problem : A singleton set depends on its element, part 2
% 59.27/59.40 % Version : [Qua92] axioms : Augmented.
% 59.27/59.40 % English :
% 59.27/59.40
% 59.27/59.40 % Refs : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 59.27/59.40 % Source : [Quaife]
% 59.27/59.40 % Names : SS5.2 [Qua92]
% 59.27/59.40
% 59.27/59.40 % Status : Unsatisfiable
% 59.27/59.40 % 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.3.0, 0.09 v6.2.0, 0.10 v6.1.0, 0.07 v6.0.0, 0.00 v5.5.0, 0.10 v5.4.0, 0.15 v5.3.0, 0.11 v5.2.0, 0.06 v5.0.0, 0.07 v4.1.0, 0.08 v4.0.1, 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.15 v3.1.0, 0.09 v2.7.0, 0.08 v2.6.0, 0.00 v2.5.0, 0.18 v2.4.0, 0.12 v2.2.1, 0.00 v2.1.0
% 59.27/59.40 % Syntax : Number of clauses : 129 ( 43 unt; 16 nHn; 87 RR)
% 59.27/59.40 % Number of literals : 252 ( 61 equ; 114 neg)
% 59.27/59.40 % Maximal clause size : 5 ( 1 avg)
% 59.27/59.40 % Maximal term depth : 6 ( 1 avg)
% 59.27/59.40 % Number of predicates : 10 ( 9 usr; 0 prp; 1-3 aty)
% 59.27/59.40 % Number of functors : 40 ( 40 usr; 10 con; 0-3 aty)
% 59.27/59.40 % Number of variables : 247 ( 46 sgn)
% 59.27/59.40 % SPC : CNF_UNS_RFO_SEQ_NHN
% 59.27/59.40
% 59.27/59.40 % Comments : Preceding lemmas are added.
% 59.27/59.40 % Bugfixes : v2.1.0 - Bugfix in SET004-0.ax.
% 59.27/59.40 %--------------------------------------------------------------------------
% 59.27/59.40 %----Include von Neuman-Bernays-Godel set theory axioms
% 59.27/59.40 include('Axioms/SET004-0.ax').
% 59.27/59.40 %--------------------------------------------------------------------------
% 59.27/59.40 %----Corollaries to Unordered pair axiom. Not in paper, but in email.
% 59.27/59.40 cnf(corollary_1_to_unordered_pair,axiom,
% 59.27/59.40 ( ~ member(ordered_pair(X,Y),cross_product(U,V))
% 59.27/59.40 | member(X,unordered_pair(X,Y)) ) ).
% 59.27/59.40
% 59.27/59.40 cnf(corollary_2_to_unordered_pair,axiom,
% 59.27/59.40 ( ~ member(ordered_pair(X,Y),cross_product(U,V))
% 59.27/59.40 | member(Y,unordered_pair(X,Y)) ) ).
% 59.27/59.40
% 59.27/59.40 %----Corollaries to Cartesian product axiom.
% 59.27/59.40 cnf(corollary_1_to_cartesian_product,axiom,
% 59.27/59.40 ( ~ member(ordered_pair(U,V),cross_product(X,Y))
% 59.27/59.40 | member(U,universal_class) ) ).
% 59.27/59.40
% 59.27/59.40 cnf(corollary_2_to_cartesian_product,axiom,
% 59.27/59.40 ( ~ member(ordered_pair(U,V),cross_product(X,Y))
% 59.27/59.40 | member(V,universal_class) ) ).
% 59.27/59.40
% 59.27/59.40 %---- PARTIAL ORDER.
% 59.27/59.40 %----(PO1): reflexive.
% 59.27/59.40 cnf(subclass_is_reflexive,axiom,
% 59.27/59.40 subclass(X,X) ).
% 59.27/59.40
% 59.27/59.40 %----(PO2): antisymmetry is part of A-3.
% 59.27/59.40 %----(x < y), (y < x) --> (x = y).
% 59.27/59.40
% 59.27/59.40 %----(PO3): transitivity.
% 59.27/59.40 cnf(transitivity_of_subclass,axiom,
% 59.27/59.40 ( ~ subclass(X,Y)
% 59.27/59.40 | ~ subclass(Y,Z)
% 59.27/59.40 | subclass(X,Z) ) ).
% 59.27/59.40
% 59.27/59.40 %---- EQUALITY.
% 59.27/59.40 %----(EQ1): equality axiom.
% 59.27/59.40 %----a:x:(x = x).
% 59.27/59.40 %----This is always an axiom in the TPTP presentation.
% 59.27/59.40
% 59.27/59.40 %----(EQ2): expanded equality definition.
% 59.27/59.40 cnf(equality1,axiom,
% 59.27/59.40 ( X = Y
% 59.27/59.40 | member(not_subclass_element(X,Y),X)
% 59.27/59.40 | member(not_subclass_element(Y,X),Y) ) ).
% 59.27/59.40
% 59.27/59.40 cnf(equality2,axiom,
% 59.27/59.40 ( ~ member(not_subclass_element(X,Y),Y)
% 59.27/59.40 | X = Y
% 59.27/59.40 | member(not_subclass_element(Y,X),Y) ) ).
% 59.27/59.40
% 59.27/59.40 cnf(equality3,axiom,
% 59.27/59.40 ( ~ member(not_subclass_element(Y,X),X)
% 59.27/59.40 | X = Y
% 59.27/59.40 | member(not_subclass_element(X,Y),X) ) ).
% 59.27/59.40
% 59.27/59.40 cnf(equality4,axiom,
% 59.27/59.40 ( ~ member(not_subclass_element(X,Y),Y)
% 59.27/59.40 | ~ member(not_subclass_element(Y,X),X)
% 59.27/59.40 | X = Y ) ).
% 59.27/59.40
% 59.27/59.40 %---- SPECIAL CLASSES.
% 59.27/59.40 %----(SP1): lemma.
% 59.27/59.40 cnf(special_classes_lemma,axiom,
% 59.27/59.40 ~ member(Y,intersection(complement(X),X)) ).
% 59.27/59.40
% 59.27/59.40 %----(SP2): Existence of O (null class).
% 59.27/59.40 %----e:x:a:z:(-(z e x)).
% 59.27/59.40 cnf(existence_of_null_class,axiom,
% 59.27/59.40 ~ member(Z,null_class) ).
% 59.27/59.40
% 59.27/59.40 %----(SP3): O is a subclass of every class.
% 59.27/59.40 cnf(null_class_is_subclass,axiom,
% 59.27/59.40 subclass(null_class,X) ).
% 59.27/59.40
% 59.27/59.40 %----corollary.
% 59.27/59.40 cnf(corollary_of_null_class_is_subclass,axiom,
% 59.27/59.40 ( ~ subclass(X,null_class)
% 59.27/59.40 | X = null_class ) ).
% 59.27/59.40
% 59.27/59.40 %----(SP4): uniqueness of null class.
% 59.27/59.40 cnf(null_class_is_unique,axiom,
% 59.27/59.40 ( Z = null_class
% 59.27/59.40 | member(not_subclass_element(Z,null_class),Z) ) ).
% 59.27/59.40
% 59.27/59.40 %----(SP5): O is a set (follows from axiom of infinity).
% 59.27/59.40 cnf(null_class_is_a_set,axiom,
% 59.27/59.40 member(null_class,universal_class) ).
% 59.27/59.40
% 59.27/59.40 %---- UNORDERED PAIRS.
% 59.27/59.40 %----(UP1): unordered pair is commutative.
% 59.27/59.40 cnf(commutativity_of_unordered_pair,axiom,
% 59.27/59.40 unordered_pair(X,Y) = unordered_pair(Y,X) ).
% 59.27/59.40
% 59.27/59.40 %----(UP2): if one argument is a proper class, pair contains only the
% 59.27/59.40 %----other. In a slightly different form to the paper
% 59.27/59.40 cnf(singleton_in_unordered_pair1,axiom,
% 59.27/59.40 subclass(singleton(X),unordered_pair(X,Y)) ).
% 59.27/59.40
% 59.27/59.40 cnf(singleton_in_unordered_pair2,axiom,
% 59.27/59.40 subclass(singleton(Y),unordered_pair(X,Y)) ).
% 59.27/59.40
% 59.27/59.40 cnf(unordered_pair_equals_singleton1,axiom,
% 59.27/59.40 ( member(Y,universal_class)
% 59.27/59.40 | unordered_pair(X,Y) = singleton(X) ) ).
% 59.27/59.40
% 59.27/59.40 cnf(unordered_pair_equals_singleton2,axiom,
% 59.27/59.40 ( member(X,universal_class)
% 59.27/59.40 | unordered_pair(X,Y) = singleton(Y) ) ).
% 59.27/59.40
% 59.27/59.40 %----(UP3): if both arguments are proper classes, pair is null.
% 59.27/59.40 cnf(null_unordered_pair,axiom,
% 59.27/59.40 ( unordered_pair(X,Y) = null_class
% 59.27/59.40 | member(X,universal_class)
% 59.27/59.40 | member(Y,universal_class) ) ).
% 59.27/59.40
% 59.27/59.40 %----(UP4): left cancellation for unordered pairs.
% 59.27/59.40 cnf(left_cancellation,axiom,
% 59.27/59.40 ( unordered_pair(X,Y) != unordered_pair(X,Z)
% 59.27/59.40 | ~ member(ordered_pair(Y,Z),cross_product(universal_class,universal_class))
% 59.27/59.40 | Y = Z ) ).
% 59.27/59.40
% 59.27/59.40 %----(UP5): right cancellation for unordered pairs.
% 59.27/59.40 cnf(right_cancellation,axiom,
% 59.27/59.40 ( unordered_pair(X,Z) != unordered_pair(Y,Z)
% 59.27/59.40 | ~ member(ordered_pair(X,Y),cross_product(universal_class,universal_class))
% 59.27/59.40 | X = Y ) ).
% 59.27/59.40
% 59.27/59.40 %----(UP6): corollary to (A-4).
% 59.27/59.40 cnf(corollary_to_unordered_pair_axiom1,axiom,
% 59.27/59.40 ( ~ member(X,universal_class)
% 59.27/59.40 | unordered_pair(X,Y) != null_class ) ).
% 59.27/59.40
% 59.27/59.40 cnf(corollary_to_unordered_pair_axiom2,axiom,
% 59.27/59.40 ( ~ member(Y,universal_class)
% 59.27/59.40 | unordered_pair(X,Y) != null_class ) ).
% 59.27/59.40
% 59.27/59.40 %----corollary to instantiate variables.
% 59.27/59.40 %----Not in the paper
% 59.27/59.40 cnf(corollary_to_unordered_pair_axiom3,axiom,
% 59.27/59.40 ( ~ member(ordered_pair(X,Y),cross_product(U,V))
% 59.27/59.40 | unordered_pair(X,Y) != null_class ) ).
% 59.27/59.40
% 59.27/59.40 %----(UP7): if both members of a pair belong to a set, the pair
% 59.27/59.40 %----is a subset.
% 59.27/59.40 cnf(unordered_pair_is_subset,axiom,
% 59.27/59.40 ( ~ member(X,Z)
% 59.27/59.40 | ~ member(Y,Z)
% 59.27/59.40 | subclass(unordered_pair(X,Y),Z) ) ).
% 59.27/59.40
% 59.27/59.40 %---- SINGLETONS.
% 59.27/59.40 %----(SS1): every singleton is a set.
% 59.27/59.40 cnf(singletons_are_sets,axiom,
% 59.27/59.40 member(singleton(X),universal_class) ).
% 59.27/59.40
% 59.27/59.40 %----corollary, not in the paper.
% 59.27/59.40 cnf(corollary_1_to_singletons_are_sets,axiom,
% 59.27/59.40 member(singleton(Y),unordered_pair(X,singleton(Y))) ).
% 59.27/59.40
% 59.27/59.40 %----(SS2): a set belongs to its singleton.
% 59.27/59.40 %----(u = x), (u e universal_class) --> (u e {x}).
% 59.27/59.40 cnf(set_in_its_singleton,axiom,
% 59.27/59.40 ( ~ member(X,universal_class)
% 59.27/59.40 | member(X,singleton(X)) ) ).
% 59.27/59.40
% 59.27/59.40 %----corollary
% 59.27/59.40 cnf(corollary_to_set_in_its_singleton,axiom,
% 59.27/59.40 ( ~ member(X,universal_class)
% 59.27/59.40 | singleton(X) != null_class ) ).
% 59.27/59.40
% 59.27/59.40 %----Not in the paper
% 59.27/59.40 cnf(null_class_in_its_singleton,axiom,
% 59.27/59.40 member(null_class,singleton(null_class)) ).
% 59.27/59.40
% 59.27/59.40 %----(SS3): only x can belong to {x}.
% 59.27/59.40 cnf(only_member_in_singleton,axiom,
% 59.27/59.40 ( ~ member(Y,singleton(X))
% 59.27/59.40 | Y = X ) ).
% 59.27/59.40
% 59.27/59.40 %----(SS4): if x is not a set, {x} = O.
% 59.27/59.40 cnf(singleton_is_null_class,axiom,
% 59.27/59.40 ( member(X,universal_class)
% 59.27/59.40 | singleton(X) = null_class ) ).
% 59.27/59.40
% 59.27/59.40 cnf(prove_singleton_identified_by_element2_1,negated_conjecture,
% 59.27/59.40 singleton(x) = singleton(y) ).
% 59.27/59.40
% 59.27/59.40 cnf(prove_singleton_identified_by_element2_2,negated_conjecture,
% 59.27/59.40 member(y,universal_class) ).
% 59.27/59.40
% 59.27/59.40 cnf(prove_singleton_identified_by_element2_3,negated_conjecture,
% 59.27/59.40 x != y ).
% 59.27/59.40
% 59.27/59.40 %--------------------------------------------------------------------------
% 59.27/59.40 %-------------------------------------------
% 59.27/59.40 % Proof found
% 59.27/59.40 % SZS status Theorem for theBenchmark
% 59.27/59.40 % SZS output start Proof
% 59.27/59.41 %ClaNum:156(EqnAxiom:42)
% 59.27/59.41 %VarNum:879(SingletonVarNum:216)
% 59.27/59.41 %MaxLitNum:5
% 59.27/59.41 %MaxfuncDepth:24
% 59.27/59.41 %SharedTerms:39
% 59.27/59.41 %goalClause: 47 51 68
% 59.27/59.41 %singleGoalClaCount:3
% 59.27/59.41 [43]P1(a1)
% 59.27/59.41 [44]P2(a2)
% 59.27/59.41 [45]P5(a4,a17)
% 59.27/59.41 [46]P5(a1,a17)
% 59.27/59.41 [47]P5(a23,a17)
% 59.27/59.41 [68]~E(a24,a23)
% 59.27/59.41 [51]E(f25(a24,a24),f25(a23,a23))
% 59.27/59.41 [53]P6(a5,f6(a17,a17))
% 59.27/59.41 [54]P6(a18,f6(a17,a17))
% 59.27/59.41 [55]P5(a4,f25(a4,a4))
% 59.27/59.41 [64]E(f10(f9(f11(f6(a21,a17))),a21),a13)
% 59.27/59.41 [66]E(f10(f6(a17,a17),f10(f6(a17,a17),f8(f7(f8(a5),f9(f11(f6(a5,a17))))))),a21)
% 59.27/59.41 [48]P6(x481,a17)
% 59.27/59.41 [49]P6(a4,x491)
% 59.27/59.41 [50]P6(x501,x501)
% 59.27/59.41 [69]~P5(x691,a4)
% 59.27/59.41 [62]P6(f19(x621),f6(f6(a17,a17),a17))
% 59.27/59.41 [63]P6(f11(x631),f6(f6(a17,a17),a17))
% 59.27/59.41 [67]E(f10(f9(x671),f8(f9(f10(f7(f9(f11(f6(a5,a17))),x671),a13)))),f3(x671))
% 59.27/59.41 [52]E(f25(x521,x522),f25(x522,x521))
% 59.27/59.41 [56]P5(f25(x561,x562),a17)
% 59.27/59.41 [58]P6(f7(x581,x582),f6(a17,a17))
% 59.27/59.41 [59]P6(f25(x591,x591),f25(x592,x591))
% 59.27/59.41 [60]P6(f25(x601,x601),f25(x601,x602))
% 59.27/59.41 [65]P5(f25(x651,x651),f25(x652,f25(x651,x651)))
% 59.27/59.41 [70]~P5(x701,f10(f8(x702),x702))
% 59.27/59.41 [61]E(f10(f6(x611,x612),x613),f10(x613,f6(x611,x612)))
% 59.27/59.41 [71]~P7(x711)+P2(x711)
% 59.27/59.41 [72]~P8(x721)+P2(x721)
% 59.27/59.41 [75]~P1(x751)+P6(a1,x751)
% 59.27/59.41 [76]~P1(x761)+P5(a4,x761)
% 59.27/59.41 [77]~P6(x771,a4)+E(x771,a4)
% 59.27/59.41 [79]P5(f20(x791),x791)+E(x791,a4)
% 59.27/59.41 [80]P5(x801,a17)+E(f25(x801,x801),a4)
% 59.27/59.41 [81]E(x811,a4)+P5(f14(x811,a4),x811)
% 59.27/59.41 [85]~P2(x851)+P6(x851,f6(a17,a17))
% 59.27/59.41 [78]E(x781,a4)+E(f10(x781,f20(x781)),a4)
% 59.27/59.41 [98]~P8(x981)+E(f6(f9(f9(x981)),f9(f9(x981))),f9(x981))
% 59.27/59.41 [113]~P7(x1131)+P2(f9(f11(f6(x1131,a17))))
% 59.27/59.41 [118]~P5(x1181,a17)+P5(f9(f10(a5,f6(a17,x1181))),a17)
% 59.27/59.41 [120]~P9(x1201)+P6(f7(x1201,f9(f11(f6(x1201,a17)))),a13)
% 59.27/59.41 [121]~P2(x1211)+P6(f7(x1211,f9(f11(f6(x1211,a17)))),a13)
% 59.27/59.41 [122]~P8(x1221)+P6(f9(f9(f11(f6(x1221,a17)))),f9(f9(x1221)))
% 59.27/59.41 [127]P9(x1271)+~P6(f7(x1271,f9(f11(f6(x1271,a17)))),a13)
% 59.27/59.41 [143]~P1(x1431)+P6(f9(f9(f11(f6(f10(a18,f6(x1431,a17)),a17)))),x1431)
% 59.27/59.41 [147]~P5(x1471,a17)+P5(f8(f9(f9(f11(f6(f10(a5,f6(f8(x1471),a17)),a17))))),a17)
% 59.27/59.41 [73]~E(x732,x731)+P6(x731,x732)
% 59.27/59.41 [74]~E(x741,x742)+P6(x741,x742)
% 59.27/59.41 [83]P5(x832,a17)+E(f25(x831,x832),f25(x831,x831))
% 59.27/59.41 [84]P5(x841,a17)+E(f25(x841,x842),f25(x842,x842))
% 59.27/59.41 [86]~P5(x862,a17)+~E(f25(x861,x862),a4)
% 59.27/59.41 [87]~P5(x871,a17)+~E(f25(x871,x872),a4)
% 59.27/59.41 [90]P6(x901,x902)+P5(f14(x901,x902),x901)
% 59.27/59.41 [91]~P5(x911,x912)+~P5(x911,f8(x912))
% 59.27/59.41 [95]~P5(x951,a17)+P5(x951,f25(x952,x951))
% 59.27/59.41 [96]~P5(x961,a17)+P5(x961,f25(x961,x962))
% 59.27/59.41 [99]E(x991,x992)+~P5(x991,f25(x992,x992))
% 59.27/59.41 [103]P6(x1031,x1032)+~P5(f14(x1031,x1032),x1032)
% 59.27/59.41 [117]~P5(x1172,f9(x1171))+~E(f10(x1171,f6(f25(x1172,x1172),a17)),a4)
% 59.27/59.41 [126]P5(x1261,x1262)+~P5(f25(f25(x1261,x1261),f25(x1261,f25(x1262,x1262))),a5)
% 59.27/59.41 [140]~P5(f25(f25(x1401,x1401),f25(x1401,f25(x1402,x1402))),a18)+E(f8(f10(f8(x1401),f8(f25(x1401,x1401)))),x1402)
% 59.27/59.41 [107]P2(x1071)+~P3(x1071,x1072,x1073)
% 59.27/59.41 [108]P8(x1081)+~P4(x1082,x1083,x1081)
% 59.27/59.41 [109]P8(x1091)+~P4(x1092,x1091,x1093)
% 59.27/59.41 [116]~P4(x1161,x1162,x1163)+P3(x1161,x1162,x1163)
% 59.27/59.41 [101]P5(x1011,x1012)+~P5(x1011,f10(x1013,x1012))
% 59.27/59.41 [102]P5(x1021,x1022)+~P5(x1021,f10(x1022,x1023))
% 59.27/59.41 [110]~P3(x1102,x1101,x1103)+E(f9(f9(x1101)),f9(x1102))
% 59.27/59.41 [123]~P5(x1231,f6(x1232,x1233))+E(f25(f25(f12(x1231),f12(x1231)),f25(f12(x1231),f25(f22(x1231),f22(x1231)))),x1231)
% 59.27/59.41 [125]~P3(x1251,x1253,x1252)+P6(f9(f9(f11(f6(x1251,a17)))),f9(f9(x1252)))
% 59.27/59.41 [128]P5(x1281,a17)+~P5(f25(f25(x1282,x1282),f25(x1282,f25(x1281,x1281))),f6(x1283,x1284))
% 59.27/59.41 [129]P5(x1291,a17)+~P5(f25(f25(x1291,x1291),f25(x1291,f25(x1292,x1292))),f6(x1293,x1294))
% 59.27/59.41 [130]P5(x1301,x1302)+~P5(f25(f25(x1303,x1303),f25(x1303,f25(x1301,x1301))),f6(x1304,x1302))
% 59.27/59.41 [131]P5(x1311,x1312)+~P5(f25(f25(x1311,x1311),f25(x1311,f25(x1313,x1313))),f6(x1312,x1314))
% 59.27/59.41 [132]~E(f25(x1321,x1322),a4)+~P5(f25(f25(x1321,x1321),f25(x1321,f25(x1322,x1322))),f6(x1323,x1324))
% 59.27/59.41 [136]P5(x1361,f25(x1362,x1361))+~P5(f25(f25(x1362,x1362),f25(x1362,f25(x1361,x1361))),f6(x1363,x1364))
% 59.27/59.41 [137]P5(x1371,f25(x1371,x1372))+~P5(f25(f25(x1371,x1371),f25(x1371,f25(x1372,x1372))),f6(x1373,x1374))
% 59.27/59.41 [148]~P5(f25(f25(f25(f25(x1483,x1483),f25(x1483,f25(x1481,x1481))),f25(f25(x1483,x1483),f25(x1483,f25(x1481,x1481)))),f25(f25(f25(x1483,x1483),f25(x1483,f25(x1481,x1481))),f25(x1482,x1482))),f19(x1484))+P5(f25(f25(f25(f25(x1481,x1481),f25(x1481,f25(x1482,x1482))),f25(f25(x1481,x1481),f25(x1481,f25(x1482,x1482)))),f25(f25(f25(x1481,x1481),f25(x1481,f25(x1482,x1482))),f25(x1483,x1483))),x1484)
% 59.27/59.41 [149]~P5(f25(f25(f25(f25(x1492,x1492),f25(x1492,f25(x1491,x1491))),f25(f25(x1492,x1492),f25(x1492,f25(x1491,x1491)))),f25(f25(f25(x1492,x1492),f25(x1492,f25(x1491,x1491))),f25(x1493,x1493))),f11(x1494))+P5(f25(f25(f25(f25(x1491,x1491),f25(x1491,f25(x1492,x1492))),f25(f25(x1491,x1491),f25(x1491,f25(x1492,x1492)))),f25(f25(f25(x1491,x1491),f25(x1491,f25(x1492,x1492))),f25(x1493,x1493))),x1494)
% 59.27/59.41 [153]~P5(f25(f25(x1534,x1534),f25(x1534,f25(x1531,x1531))),f7(x1532,x1533))+P5(x1531,f9(f9(f11(f6(f10(x1532,f6(f9(f9(f11(f6(f10(x1533,f6(f25(x1534,x1534),a17)),a17)))),a17)),a17)))))
% 59.27/59.41 [119]~P2(x1191)+P7(x1191)+~P2(f9(f11(f6(x1191,a17))))
% 59.27/59.41 [133]P2(x1331)+~P6(x1331,f6(a17,a17))+~P6(f7(x1331,f9(f11(f6(x1331,a17)))),a13)
% 59.27/59.41 [145]P1(x1451)+~P5(a4,x1451)+~P6(f9(f9(f11(f6(f10(a18,f6(x1451,a17)),a17)))),x1451)
% 59.27/59.41 [152]~P5(x1521,a17)+E(x1521,a4)+P5(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(a2,f6(f25(x1521,x1521),a17)),a17))))))),x1521)
% 59.27/59.41 [89]~P6(x892,x891)+~P6(x891,x892)+E(x891,x892)
% 59.27/59.41 [82]P5(x822,a17)+P5(x821,a17)+E(f25(x821,x822),a4)
% 59.27/59.41 [92]P5(x921,x922)+P5(x921,f8(x922))+~P5(x921,a17)
% 59.27/59.41 [104]E(x1041,x1042)+P5(f14(x1042,x1041),x1042)+P5(f14(x1041,x1042),x1041)
% 59.27/59.41 [112]E(x1121,x1122)+P5(f14(x1122,x1121),x1122)+~P5(f14(x1121,x1122),x1122)
% 59.27/59.41 [114]E(x1141,x1142)+~P5(f14(x1142,x1141),x1141)+~P5(f14(x1141,x1142),x1142)
% 59.27/59.41 [115]P5(x1152,f9(x1151))+~P5(x1152,a17)+E(f10(x1151,f6(f25(x1152,x1152),a17)),a4)
% 59.27/59.41 [141]~P5(x1411,x1412)+~P5(f25(f25(x1411,x1411),f25(x1411,f25(x1412,x1412))),f6(a17,a17))+P5(f25(f25(x1411,x1411),f25(x1411,f25(x1412,x1412))),a5)
% 59.27/59.41 [142]~P5(f25(f25(x1421,x1421),f25(x1421,f25(x1422,x1422))),f6(a17,a17))+~E(f8(f10(f8(x1421),f8(f25(x1421,x1421)))),x1422)+P5(f25(f25(x1421,x1421),f25(x1421,f25(x1422,x1422))),a18)
% 59.27/59.41 [144]~P2(x1441)+~P5(x1442,a17)+P5(f9(f9(f11(f6(f10(x1441,f6(x1442,a17)),a17)))),a17)
% 59.27/59.41 [93]~P6(x931,x933)+P6(x931,x932)+~P6(x933,x932)
% 59.27/59.41 [94]~P5(x941,x943)+P5(x941,x942)+~P6(x943,x942)
% 59.27/59.41 [100]E(x1001,x1002)+E(x1001,x1003)+~P5(x1001,f25(x1003,x1002))
% 59.27/59.41 [105]~P5(x1051,x1053)+~P5(x1051,x1052)+P5(x1051,f10(x1052,x1053))
% 59.27/59.41 [106]~P5(x1062,x1063)+~P5(x1061,x1063)+P6(f25(x1061,x1062),x1063)
% 59.27/59.41 [134]E(x1341,x1342)+~E(f25(x1343,x1341),f25(x1343,x1342))+~P5(f25(f25(x1341,x1341),f25(x1341,f25(x1342,x1342))),f6(a17,a17))
% 59.27/59.41 [135]E(x1351,x1352)+~E(f25(x1351,x1353),f25(x1352,x1353))+~P5(f25(f25(x1351,x1351),f25(x1351,f25(x1352,x1352))),f6(a17,a17))
% 59.27/59.41 [124]~P5(x1242,x1244)+~P5(x1241,x1243)+P5(f25(f25(x1241,x1241),f25(x1241,f25(x1242,x1242))),f6(x1243,x1244))
% 59.27/59.41 [150]~P5(f25(f25(f25(f25(x1502,x1502),f25(x1502,f25(x1503,x1503))),f25(f25(x1502,x1502),f25(x1502,f25(x1503,x1503)))),f25(f25(f25(x1502,x1502),f25(x1502,f25(x1503,x1503))),f25(x1501,x1501))),x1504)+P5(f25(f25(f25(f25(x1501,x1501),f25(x1501,f25(x1502,x1502))),f25(f25(x1501,x1501),f25(x1501,f25(x1502,x1502)))),f25(f25(f25(x1501,x1501),f25(x1501,f25(x1502,x1502))),f25(x1503,x1503))),f19(x1504))+~P5(f25(f25(f25(f25(x1501,x1501),f25(x1501,f25(x1502,x1502))),f25(f25(x1501,x1501),f25(x1501,f25(x1502,x1502)))),f25(f25(f25(x1501,x1501),f25(x1501,f25(x1502,x1502))),f25(x1503,x1503))),f6(f6(a17,a17),a17))
% 59.27/59.41 [151]~P5(f25(f25(f25(f25(x1512,x1512),f25(x1512,f25(x1511,x1511))),f25(f25(x1512,x1512),f25(x1512,f25(x1511,x1511)))),f25(f25(f25(x1512,x1512),f25(x1512,f25(x1511,x1511))),f25(x1513,x1513))),x1514)+P5(f25(f25(f25(f25(x1511,x1511),f25(x1511,f25(x1512,x1512))),f25(f25(x1511,x1511),f25(x1511,f25(x1512,x1512)))),f25(f25(f25(x1511,x1511),f25(x1511,f25(x1512,x1512))),f25(x1513,x1513))),f11(x1514))+~P5(f25(f25(f25(f25(x1511,x1511),f25(x1511,f25(x1512,x1512))),f25(f25(x1511,x1511),f25(x1511,f25(x1512,x1512)))),f25(f25(f25(x1511,x1511),f25(x1511,f25(x1512,x1512))),f25(x1513,x1513))),f6(f6(a17,a17),a17))
% 59.27/59.41 [154]P5(f25(f25(x1541,x1541),f25(x1541,f25(x1542,x1542))),f7(x1543,x1544))+~P5(f25(f25(x1541,x1541),f25(x1541,f25(x1542,x1542))),f6(a17,a17))+~P5(x1542,f9(f9(f11(f6(f10(x1543,f6(f9(f9(f11(f6(f10(x1544,f6(f25(x1541,x1541),a17)),a17)))),a17)),a17)))))
% 59.27/59.41 [155]~P4(x1552,x1555,x1551)+~P5(f25(f25(x1553,x1553),f25(x1553,f25(x1554,x1554))),f9(x1555))+E(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1551,f6(f25(f25(f25(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1552,f6(f25(x1553,x1553),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1552,f6(f25(x1553,x1553),a17)),a17)))))))),f25(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1552,f6(f25(x1553,x1553),a17)),a17))))))),f25(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1552,f6(f25(x1554,x1554),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1552,f6(f25(x1554,x1554),a17)),a17)))))))))),f25(f25(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1552,f6(f25(x1553,x1553),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1552,f6(f25(x1553,x1553),a17)),a17)))))))),f25(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1552,f6(f25(x1553,x1553),a17)),a17))))))),f25(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1552,f6(f25(x1554,x1554),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1552,f6(f25(x1554,x1554),a17)),a17))))))))))),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1552,f6(f25(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1555,f6(f25(f25(f25(x1553,x1553),f25(x1553,f25(x1554,x1554))),f25(f25(x1553,x1553),f25(x1553,f25(x1554,x1554)))),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1555,f6(f25(f25(f25(x1553,x1553),f25(x1553,f25(x1554,x1554))),f25(f25(x1553,x1553),f25(x1553,f25(x1554,x1554)))),a17)),a17)))))))),a17)),a17))))))))
% 59.27/59.41 [139]~P2(x1391)+P8(x1391)+~E(f6(f9(f9(x1391)),f9(f9(x1391))),f9(x1391))+~P6(f9(f9(f11(f6(x1391,a17)))),f9(f9(x1391)))
% 59.27/59.41 [138]~P2(x1381)+P3(x1381,x1382,x1383)+~E(f9(f9(x1382)),f9(x1381))+~P6(f9(f9(f11(f6(x1381,a17)))),f9(f9(x1383)))
% 59.27/59.41 [146]~P8(x1463)+~P8(x1462)+~P3(x1461,x1462,x1463)+P4(x1461,x1462,x1463)+P5(f25(f25(f15(x1461,x1462,x1463),f15(x1461,x1462,x1463)),f25(f15(x1461,x1462,x1463),f25(f16(x1461,x1462,x1463),f16(x1461,x1462,x1463)))),f9(x1462))
% 59.27/59.41 [156]~P8(x1563)+~P8(x1562)+~P3(x1561,x1562,x1563)+P4(x1561,x1562,x1563)+~E(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1563,f6(f25(f25(f25(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1561,f6(f25(f15(x1561,x1562,x1563),f15(x1561,x1562,x1563)),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1561,f6(f25(f15(x1561,x1562,x1563),f15(x1561,x1562,x1563)),a17)),a17)))))))),f25(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1561,f6(f25(f15(x1561,x1562,x1563),f15(x1561,x1562,x1563)),a17)),a17))))))),f25(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1561,f6(f25(f16(x1561,x1562,x1563),f16(x1561,x1562,x1563)),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1561,f6(f25(f16(x1561,x1562,x1563),f16(x1561,x1562,x1563)),a17)),a17)))))))))),f25(f25(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1561,f6(f25(f15(x1561,x1562,x1563),f15(x1561,x1562,x1563)),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1561,f6(f25(f15(x1561,x1562,x1563),f15(x1561,x1562,x1563)),a17)),a17)))))))),f25(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1561,f6(f25(f15(x1561,x1562,x1563),f15(x1561,x1562,x1563)),a17)),a17))))))),f25(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1561,f6(f25(f16(x1561,x1562,x1563),f16(x1561,x1562,x1563)),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1561,f6(f25(f16(x1561,x1562,x1563),f16(x1561,x1562,x1563)),a17)),a17))))))))))),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1561,f6(f25(f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1562,f6(f25(f25(f25(f15(x1561,x1562,x1563),f15(x1561,x1562,x1563)),f25(f15(x1561,x1562,x1563),f25(f16(x1561,x1562,x1563),f16(x1561,x1562,x1563)))),f25(f25(f15(x1561,x1562,x1563),f15(x1561,x1562,x1563)),f25(f15(x1561,x1562,x1563),f25(f16(x1561,x1562,x1563),f16(x1561,x1562,x1563))))),a17)),a17))))))),f9(f10(a5,f6(a17,f9(f9(f11(f6(f10(x1562,f6(f25(f25(f25(f15(x1561,x1562,x1563),f15(x1561,x1562,x1563)),f25(f15(x1561,x1562,x1563),f25(f16(x1561,x1562,x1563),f16(x1561,x1562,x1563)))),f25(f25(f15(x1561,x1562,x1563),f15(x1561,x1562,x1563)),f25(f15(x1561,x1562,x1563),f25(f16(x1561,x1562,x1563),f16(x1561,x1562,x1563))))),a17)),a17)))))))),a17)),a17))))))))
% 59.27/59.41 %EqnAxiom
% 59.27/59.41 [1]E(x11,x11)
% 59.27/59.41 [2]E(x22,x21)+~E(x21,x22)
% 59.27/59.41 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.27/59.41 [4]~E(x41,x42)+E(f25(x41,x43),f25(x42,x43))
% 59.27/59.41 [5]~E(x51,x52)+E(f25(x53,x51),f25(x53,x52))
% 59.27/59.41 [6]~E(x61,x62)+E(f9(x61),f9(x62))
% 59.27/59.41 [7]~E(x71,x72)+E(f10(x71,x73),f10(x72,x73))
% 59.27/59.41 [8]~E(x81,x82)+E(f10(x83,x81),f10(x83,x82))
% 59.27/59.41 [9]~E(x91,x92)+E(f6(x91,x93),f6(x92,x93))
% 59.27/59.41 [10]~E(x101,x102)+E(f6(x103,x101),f6(x103,x102))
% 59.27/59.41 [11]~E(x111,x112)+E(f8(x111),f8(x112))
% 59.27/59.41 [12]~E(x121,x122)+E(f15(x121,x123,x124),f15(x122,x123,x124))
% 59.27/59.41 [13]~E(x131,x132)+E(f15(x133,x131,x134),f15(x133,x132,x134))
% 59.27/59.41 [14]~E(x141,x142)+E(f15(x143,x144,x141),f15(x143,x144,x142))
% 59.27/59.41 [15]~E(x151,x152)+E(f11(x151),f11(x152))
% 59.27/59.41 [16]~E(x161,x162)+E(f22(x161),f22(x162))
% 59.27/59.41 [17]~E(x171,x172)+E(f7(x171,x173),f7(x172,x173))
% 59.27/59.41 [18]~E(x181,x182)+E(f7(x183,x181),f7(x183,x182))
% 59.27/59.41 [19]~E(x191,x192)+E(f20(x191),f20(x192))
% 59.27/59.41 [20]~E(x201,x202)+E(f16(x201,x203,x204),f16(x202,x203,x204))
% 59.27/59.41 [21]~E(x211,x212)+E(f16(x213,x211,x214),f16(x213,x212,x214))
% 59.27/59.41 [22]~E(x221,x222)+E(f16(x223,x224,x221),f16(x223,x224,x222))
% 59.27/59.41 [23]~E(x231,x232)+E(f19(x231),f19(x232))
% 59.27/59.41 [24]~E(x241,x242)+E(f12(x241),f12(x242))
% 59.27/59.41 [25]~E(x251,x252)+E(f14(x251,x253),f14(x252,x253))
% 59.27/59.41 [26]~E(x261,x262)+E(f14(x263,x261),f14(x263,x262))
% 59.27/59.41 [27]~E(x271,x272)+E(f3(x271),f3(x272))
% 59.27/59.41 [28]~P1(x281)+P1(x282)+~E(x281,x282)
% 59.27/59.41 [29]~P2(x291)+P2(x292)+~E(x291,x292)
% 59.27/59.41 [30]P5(x302,x303)+~E(x301,x302)+~P5(x301,x303)
% 59.27/59.41 [31]P5(x313,x312)+~E(x311,x312)+~P5(x313,x311)
% 59.27/59.41 [32]P3(x322,x323,x324)+~E(x321,x322)+~P3(x321,x323,x324)
% 59.27/59.41 [33]P3(x333,x332,x334)+~E(x331,x332)+~P3(x333,x331,x334)
% 59.27/59.41 [34]P3(x343,x344,x342)+~E(x341,x342)+~P3(x343,x344,x341)
% 59.27/59.41 [35]~P8(x351)+P8(x352)+~E(x351,x352)
% 59.27/59.41 [36]P6(x362,x363)+~E(x361,x362)+~P6(x361,x363)
% 59.27/59.41 [37]P6(x373,x372)+~E(x371,x372)+~P6(x373,x371)
% 59.27/59.41 [38]P4(x382,x383,x384)+~E(x381,x382)+~P4(x381,x383,x384)
% 59.27/59.41 [39]P4(x393,x392,x394)+~E(x391,x392)+~P4(x393,x391,x394)
% 59.27/59.41 [40]P4(x403,x404,x402)+~E(x401,x402)+~P4(x403,x404,x401)
% 59.27/59.41 [41]~P7(x411)+P7(x412)+~E(x411,x412)
% 59.27/59.41 [42]~P9(x421)+P9(x422)+~E(x421,x422)
% 59.27/59.41
% 59.27/59.41 %-------------------------------------------
% 59.38/59.42 cnf(163,plain,
% 59.38/59.42 (E(f25(a23,a23),f25(a24,a24))),
% 59.38/59.42 inference(scs_inference,[],[51,2])).
% 59.38/59.42 cnf(164,plain,
% 59.38/59.42 (~P1(a4)),
% 59.38/59.42 inference(scs_inference,[],[51,69,2,76])).
% 59.38/59.42 cnf(165,plain,
% 59.38/59.42 (~P5(x1651,a4)),
% 59.38/59.42 inference(rename_variables,[],[69])).
% 59.38/59.42 cnf(167,plain,
% 59.38/59.42 (E(f10(f8(x1671),x1671),a4)),
% 59.38/59.42 inference(scs_inference,[],[51,69,70,2,76,81])).
% 59.38/59.42 cnf(168,plain,
% 59.38/59.42 (~P5(x1681,f10(f8(x1682),x1682))),
% 59.38/59.42 inference(rename_variables,[],[70])).
% 59.38/59.42 cnf(170,plain,
% 59.38/59.42 (P6(f10(f8(x1701),x1701),x1702)),
% 59.38/59.42 inference(scs_inference,[],[51,69,70,168,2,76,81,90])).
% 59.38/59.42 cnf(171,plain,
% 59.38/59.42 (~P5(x1711,f10(f8(x1712),x1712))),
% 59.38/59.42 inference(rename_variables,[],[70])).
% 59.38/59.42 cnf(173,plain,
% 59.38/59.42 (~P5(x1731,f9(f8(f6(f25(x1731,x1731),a17))))),
% 59.38/59.42 inference(scs_inference,[],[51,69,70,168,2,76,81,90,117])).
% 59.38/59.42 cnf(175,plain,
% 59.38/59.42 (~P5(f25(f25(f25(f25(x1751,x1751),f25(x1751,f25(x1752,x1752))),f25(f25(x1751,x1751),f25(x1751,f25(x1752,x1752)))),f25(f25(f25(x1751,x1751),f25(x1751,f25(x1752,x1752))),f25(x1753,x1753))),f19(a4))),
% 59.38/59.42 inference(scs_inference,[],[51,69,165,70,168,2,76,81,90,117,148])).
% 59.38/59.42 cnf(176,plain,
% 59.38/59.42 (~P5(x1761,a4)),
% 59.38/59.42 inference(rename_variables,[],[69])).
% 59.38/59.42 cnf(179,plain,
% 59.38/59.42 (~P5(x1791,a4)),
% 59.38/59.42 inference(rename_variables,[],[69])).
% 59.38/59.42 cnf(181,plain,
% 59.38/59.42 (P5(f25(x1811,x1811),f25(f25(x1811,x1811),x1812))),
% 59.38/59.42 inference(scs_inference,[],[51,69,165,176,60,65,70,168,2,76,81,90,117,148,149,94])).
% 59.38/59.42 cnf(183,plain,
% 59.38/59.42 (P5(f25(x1831,x1831),f25(x1832,f25(x1831,x1831)))),
% 59.38/59.42 inference(rename_variables,[],[65])).
% 59.38/59.42 cnf(185,plain,
% 59.38/59.42 (~P5(a23,f8(a17))),
% 59.38/59.42 inference(scs_inference,[],[47,51,69,165,176,60,65,70,168,171,2,76,81,90,117,148,149,94,105])).
% 59.38/59.42 cnf(186,plain,
% 59.38/59.42 (~P5(x1861,f10(f8(x1862),x1862))),
% 59.38/59.42 inference(rename_variables,[],[70])).
% 59.38/59.42 cnf(188,plain,
% 59.38/59.42 (E(f10(f6(f25(x1881,x1881),a17),f8(f6(f25(x1881,x1881),a17))),a4)),
% 59.38/59.42 inference(scs_inference,[],[47,51,69,165,176,60,65,61,70,168,171,2,76,81,90,117,148,149,94,105,3])).
% 59.38/59.42 cnf(191,plain,
% 59.38/59.42 (P5(f25(a23,a23),f25(x1911,f25(a24,a24)))),
% 59.38/59.42 inference(scs_inference,[],[47,51,69,165,176,60,65,183,61,70,168,171,2,76,81,90,117,148,149,94,105,3,28,30])).
% 59.38/59.42 cnf(193,plain,
% 59.38/59.42 (~E(a17,a4)),
% 59.38/59.42 inference(scs_inference,[],[47,51,69,165,176,179,60,65,183,61,70,168,171,2,76,81,90,117,148,149,94,105,3,28,30,31])).
% 59.38/59.42 cnf(194,plain,
% 59.38/59.42 (~P5(x1941,a4)),
% 59.38/59.42 inference(rename_variables,[],[69])).
% 59.38/59.42 cnf(195,plain,
% 59.38/59.42 (E(a4,f10(f8(x1951),x1951))),
% 59.38/59.42 inference(scs_inference,[],[47,51,69,165,176,179,194,60,65,183,61,70,168,171,186,2,76,81,90,117,148,149,94,105,3,28,30,31,104])).
% 59.38/59.42 cnf(199,plain,
% 59.38/59.42 (P1(a17)),
% 59.38/59.42 inference(scs_inference,[],[47,51,48,69,165,176,179,194,60,45,65,183,61,70,168,171,186,2,76,81,90,117,148,149,94,105,3,28,30,31,104,145])).
% 59.38/59.42 cnf(203,plain,
% 59.38/59.42 (P6(x2031,x2031)),
% 59.38/59.42 inference(rename_variables,[],[50])).
% 59.38/59.42 cnf(204,plain,
% 59.38/59.42 (P6(f25(a24,a24),f25(a23,a23))),
% 59.38/59.42 inference(scs_inference,[],[47,51,50,203,48,69,165,176,179,194,60,45,65,183,61,70,168,171,186,2,76,81,90,117,148,149,94,105,3,28,30,31,104,145,36,37])).
% 59.38/59.42 cnf(206,plain,
% 59.38/59.42 (~P6(a17,a4)),
% 59.38/59.42 inference(scs_inference,[],[47,51,50,203,48,69,165,176,179,194,60,45,65,183,61,70,168,171,186,2,76,81,90,117,148,149,94,105,3,28,30,31,104,145,36,37,77])).
% 59.38/59.42 cnf(233,plain,
% 59.38/59.42 (~P5(f25(f25(f25(f25(x2331,x2331),f25(x2331,f25(x2332,x2332))),f25(f25(x2331,x2331),f25(x2331,f25(x2332,x2332)))),f25(f25(f25(x2331,x2331),f25(x2331,f25(x2332,x2332))),f25(x2333,x2333))),f11(f19(a4)))),
% 59.38/59.42 inference(scs_inference,[],[173,175,76,149])).
% 59.38/59.42 cnf(235,plain,
% 59.38/59.42 (~P5(f25(f25(f25(f25(x2351,x2351),f25(x2351,f25(x2352,x2352))),f25(f25(x2351,x2351),f25(x2351,f25(x2352,x2352)))),f25(f25(f25(x2351,x2351),f25(x2351,f25(x2352,x2352))),f25(x2353,x2353))),f19(f19(a4)))),
% 59.38/59.42 inference(scs_inference,[],[173,175,76,149,148])).
% 59.38/59.42 cnf(237,plain,
% 59.38/59.42 (E(a4,f10(f6(f25(x2371,x2371),a17),f8(f6(f25(x2371,x2371),a17))))),
% 59.38/59.42 inference(scs_inference,[],[188,173,175,76,149,148,2])).
% 59.38/59.42 cnf(239,plain,
% 59.38/59.42 (P5(f25(a23,a23),f25(f25(a24,a24),x2391))),
% 59.38/59.42 inference(scs_inference,[],[51,181,193,188,173,175,76,149,148,2,3,30])).
% 59.38/59.42 cnf(242,plain,
% 59.38/59.42 (~E(f10(f8(x2421),x2421),a17)),
% 59.38/59.42 inference(scs_inference,[],[47,51,181,193,188,185,170,173,175,206,76,149,148,2,3,30,31,36])).
% 59.38/59.42 cnf(243,plain,
% 59.38/59.42 (P6(f10(f8(x2431),x2431),x2432)),
% 59.38/59.42 inference(rename_variables,[],[170])).
% 59.38/59.42 cnf(249,plain,
% 59.38/59.42 (~E(a17,f10(f8(x2491),x2491))),
% 59.38/59.42 inference(scs_inference,[],[47,51,181,193,188,185,170,243,173,175,164,206,76,149,148,2,3,30,31,36,28,42,89,74])).
% 59.38/59.42 cnf(261,plain,
% 59.38/59.42 (~P5(f25(f25(f25(f25(x2611,x2611),f25(x2611,f25(x2612,x2612))),f25(f25(x2611,x2611),f25(x2611,f25(x2612,x2612)))),f25(f25(f25(x2611,x2611),f25(x2611,f25(x2612,x2612))),f25(x2613,x2613))),f11(f10(f8(x2614),x2614)))),
% 59.38/59.42 inference(scs_inference,[],[70,149])).
% 59.38/59.42 cnf(262,plain,
% 59.38/59.42 (~P5(x2621,f10(f8(x2622),x2622))),
% 59.38/59.42 inference(rename_variables,[],[70])).
% 59.38/59.42 cnf(264,plain,
% 59.38/59.42 (~P1(f10(f8(x2641),x2641))),
% 59.38/59.42 inference(scs_inference,[],[70,262,149,76])).
% 59.38/59.42 cnf(265,plain,
% 59.38/59.42 (~P5(x2651,f10(f8(x2652),x2652))),
% 59.38/59.42 inference(rename_variables,[],[70])).
% 59.38/59.42 cnf(267,plain,
% 59.38/59.42 (~P5(f25(f25(f25(f25(x2671,x2671),f25(x2671,f25(x2672,x2672))),f25(f25(x2671,x2671),f25(x2671,f25(x2672,x2672)))),f25(f25(f25(x2671,x2671),f25(x2671,f25(x2672,x2672))),f25(x2673,x2673))),f19(f10(f8(x2674),x2674)))),
% 59.38/59.42 inference(scs_inference,[],[70,262,265,149,76,148])).
% 59.38/59.42 cnf(268,plain,
% 59.38/59.42 (~P5(x2681,f10(f8(x2682),x2682))),
% 59.38/59.42 inference(rename_variables,[],[70])).
% 59.38/59.42 cnf(274,plain,
% 59.38/59.42 (~E(f25(x2741,f25(a24,a24)),f10(f8(x2742),x2742))),
% 59.38/59.42 inference(scs_inference,[],[191,249,70,262,265,268,64,61,149,76,148,2,3,31])).
% 59.38/59.42 cnf(276,plain,
% 59.38/59.42 (P6(f25(a23,a23),f25(x2761,a24))),
% 59.38/59.42 inference(scs_inference,[],[51,191,249,70,262,265,268,59,64,61,149,76,148,2,3,31,36])).
% 59.38/59.42 cnf(278,plain,
% 59.38/59.42 (P5(f10(f6(f25(x2781,x2781),a17),f8(f6(f25(x2781,x2781),a17))),f25(a4,a4))),
% 59.38/59.42 inference(scs_inference,[],[51,191,249,237,70,262,265,268,59,55,64,61,149,76,148,2,3,31,36,30])).
% 59.38/59.42 cnf(285,plain,
% 59.38/59.42 (~P5(f25(f25(f25(f25(x2851,x2851),f25(x2851,f25(x2852,x2852))),f25(f25(x2851,x2851),f25(x2851,f25(x2852,x2852)))),f25(f25(f25(x2851,x2851),f25(x2851,f25(x2852,x2852))),f25(x2853,x2853))),f11(f11(f10(f8(x2854),x2854))))),
% 59.38/59.42 inference(scs_inference,[],[261,149])).
% 59.38/59.42 cnf(287,plain,
% 59.38/59.42 (~P5(f25(f25(f25(f25(x2871,x2871),f25(x2871,f25(x2872,x2872))),f25(f25(x2871,x2871),f25(x2871,f25(x2872,x2872)))),f25(f25(f25(x2871,x2871),f25(x2871,f25(x2872,x2872))),f25(x2873,x2873))),f19(f11(f10(f8(x2874),x2874))))),
% 59.38/59.42 inference(scs_inference,[],[261,149,148])).
% 59.38/59.42 cnf(298,plain,
% 59.38/59.42 (~E(f25(f25(a24,a24),x2981),a4)),
% 59.38/59.42 inference(scs_inference,[],[51,239,237,274,69,60,195,264,261,66,45,61,149,148,2,3,28,30,36,31])).
% 59.38/59.42 cnf(300,plain,
% 59.38/59.42 (P5(f20(f25(x3001,f25(a24,a24))),f25(x3001,f25(a24,a24)))),
% 59.38/59.42 inference(scs_inference,[],[51,239,237,274,69,60,195,264,261,66,45,61,149,148,2,3,28,30,36,31,79])).
% 59.38/59.42 cnf(302,plain,
% 59.38/59.42 (~P6(f25(x3021,f25(a24,a24)),a4)),
% 59.38/59.42 inference(scs_inference,[],[51,239,237,274,69,60,195,264,261,66,45,61,149,148,2,3,28,30,36,31,79,77])).
% 59.38/59.42 cnf(306,plain,
% 59.38/59.42 (E(f20(f25(f25(a24,a24),f25(a24,a24))),f25(a24,a24))),
% 59.38/59.42 inference(scs_inference,[],[51,239,237,274,69,60,195,54,264,261,66,45,61,149,148,2,3,28,30,36,31,79,77,89,99])).
% 59.38/59.42 cnf(311,plain,
% 59.38/59.42 (~P5(x3111,f25(a24,a24))+P5(x3111,f25(a23,a23))),
% 59.38/59.42 inference(scs_inference,[],[51,239,237,274,204,69,60,195,54,264,261,66,45,61,149,148,2,3,28,30,36,31,79,77,89,99,73,37,94])).
% 59.38/59.42 cnf(317,plain,
% 59.38/59.42 (~P6(f25(f25(a24,a24),x3171),a4)),
% 59.38/59.42 inference(scs_inference,[],[298,77])).
% 59.38/59.42 cnf(323,plain,
% 59.38/59.42 (~P5(f25(f25(f25(f25(x3231,x3231),f25(x3231,f25(x3232,x3232))),f25(f25(x3231,x3231),f25(x3231,f25(x3232,x3232)))),f25(f25(f25(x3231,x3231),f25(x3231,f25(x3232,x3232))),f25(x3233,x3233))),f11(f19(f10(f8(x3234),x3234))))),
% 59.38/59.42 inference(scs_inference,[],[298,267,302,77,73,79,149])).
% 59.38/59.42 cnf(325,plain,
% 59.38/59.42 (~P5(f25(f25(f25(f25(x3251,x3251),f25(x3251,f25(x3252,x3252))),f25(f25(x3251,x3251),f25(x3251,f25(x3252,x3252)))),f25(f25(f25(x3251,x3251),f25(x3251,f25(x3252,x3252))),f25(x3253,x3253))),f19(f19(f10(f8(x3254),x3254))))),
% 59.38/59.42 inference(scs_inference,[],[298,267,302,77,73,79,149,148])).
% 59.38/59.42 cnf(327,plain,
% 59.38/59.42 (E(f25(a24,a24),f20(f25(f25(a24,a24),f25(a24,a24))))),
% 59.38/59.42 inference(scs_inference,[],[298,267,306,302,77,73,79,149,148,2])).
% 59.38/59.42 cnf(328,plain,
% 59.38/59.42 (~E(f25(x3281,f25(a24,a24)),f10(f6(x3282,x3283),f8(f6(x3282,x3283))))),
% 59.38/59.43 inference(scs_inference,[],[298,274,267,306,302,61,77,73,79,149,148,2,3])).
% 59.38/59.43 cnf(331,plain,
% 59.38/59.43 (~E(f25(a4,a4),f10(f8(x3311),x3311))),
% 59.38/59.43 inference(scs_inference,[],[278,298,274,70,267,306,302,61,77,73,79,149,148,2,3,31])).
% 59.38/59.43 cnf(338,plain,
% 59.38/59.43 (~P5(x3381,f25(a23,a23))+P5(x3381,f25(x3382,a24))),
% 59.38/59.43 inference(scs_inference,[],[51,278,298,274,70,276,62,267,300,306,302,61,77,73,79,149,148,2,3,31,100,89,35,94])).
% 59.38/59.43 cnf(345,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x3451,x3451),f25(x3451,f25(x3452,x3452))),f25(f25(x3451,x3451),f25(x3451,f25(x3452,x3452)))),f25(f25(f25(x3451,x3451),f25(x3451,f25(x3452,x3452))),f25(x3453,x3453))),f11(f11(f11(f10(f8(x3454),x3454)))))),
% 59.38/59.43 inference(scs_inference,[],[285,317,73,149])).
% 59.38/59.43 cnf(347,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x3471,x3471),f25(x3471,f25(x3472,x3472))),f25(f25(x3471,x3471),f25(x3471,f25(x3472,x3472)))),f25(f25(f25(x3471,x3471),f25(x3471,f25(x3472,x3472))),f25(x3473,x3473))),f19(f11(f11(f10(f8(x3474),x3474)))))),
% 59.38/59.43 inference(scs_inference,[],[285,317,73,149,148])).
% 59.38/59.43 cnf(349,plain,
% 59.38/59.43 (E(f10(x3491,f6(x3492,x3493)),f10(f6(x3492,x3493),x3491))),
% 59.38/59.43 inference(scs_inference,[],[285,317,61,73,149,148,2])).
% 59.38/59.43 cnf(350,plain,
% 59.38/59.43 (E(f25(a23,a23),f20(f25(f25(a24,a24),f25(a24,a24))))),
% 59.38/59.43 inference(scs_inference,[],[327,163,285,317,61,73,149,148,2,3])).
% 59.38/59.43 cnf(351,plain,
% 59.38/59.43 (~E(f25(f25(a24,a24),x3511),f10(f8(x3512),x3512))),
% 59.38/59.43 inference(scs_inference,[],[239,327,163,70,285,317,61,73,149,148,2,3,31])).
% 59.38/59.43 cnf(362,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x3621,x3621),f25(x3621,f25(x3622,x3622))),f25(f25(x3621,x3621),f25(x3621,f25(x3622,x3622)))),f25(f25(f25(x3621,x3621),f25(x3621,f25(x3622,x3622))),f25(x3623,x3623))),f11(f19(f11(f10(f8(x3624),x3624)))))),
% 59.38/59.43 inference(scs_inference,[],[287,149])).
% 59.38/59.43 cnf(364,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x3641,x3641),f25(x3641,f25(x3642,x3642))),f25(f25(x3641,x3641),f25(x3641,f25(x3642,x3642)))),f25(f25(f25(x3641,x3641),f25(x3641,f25(x3642,x3642))),f25(x3643,x3643))),f19(f19(f11(f10(f8(x3644),x3644)))))),
% 59.38/59.43 inference(scs_inference,[],[287,149,148])).
% 59.38/59.43 cnf(367,plain,
% 59.38/59.43 (P6(f20(f25(f25(a24,a24),f25(a24,a24))),f25(x3671,a24))),
% 59.38/59.43 inference(scs_inference,[],[350,276,287,149,148,2,36])).
% 59.38/59.43 cnf(368,plain,
% 59.38/59.43 (P6(f25(a24,a24),f20(f25(f25(a24,a24),f25(a24,a24))))),
% 59.38/59.43 inference(scs_inference,[],[350,204,276,287,149,148,2,36,37])).
% 59.38/59.43 cnf(369,plain,
% 59.38/59.43 (~E(f25(f25(a24,a24),x3691),f10(f6(x3692,x3693),f8(f6(x3692,x3693))))),
% 59.38/59.43 inference(scs_inference,[],[351,350,204,276,61,287,149,148,2,36,37,3])).
% 59.38/59.43 cnf(379,plain,
% 59.38/59.43 (~E(a4,f25(a4,a4))),
% 59.38/59.43 inference(scs_inference,[],[191,278,351,350,204,69,276,61,287,149,148,2,36,37,3,30,31,77,79,73])).
% 59.38/59.43 cnf(381,plain,
% 59.38/59.43 (E(f20(f25(a4,a4)),a4)),
% 59.38/59.43 inference(scs_inference,[],[191,278,351,350,204,69,276,61,287,149,148,2,36,37,3,30,31,77,79,73,100])).
% 59.38/59.43 cnf(386,plain,
% 59.38/59.43 (~P5(x3861,a5)+P5(x3861,f6(a17,a17))),
% 59.38/59.43 inference(scs_inference,[],[191,278,351,350,204,69,276,53,58,61,287,164,149,148,2,36,37,3,30,31,77,79,73,100,89,28,94])).
% 59.38/59.43 cnf(392,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x3921,x3921),f25(x3921,f25(x3922,x3922))),f25(f25(x3921,x3921),f25(x3921,f25(x3922,x3922)))),f25(f25(f25(x3921,x3921),f25(x3921,f25(x3922,x3922))),f25(x3923,x3923))),f11(f11(f19(f10(f8(x3924),x3924)))))),
% 59.38/59.43 inference(scs_inference,[],[323,149])).
% 59.38/59.43 cnf(396,plain,
% 59.38/59.43 (E(a4,f20(f25(a4,a4)))),
% 59.38/59.43 inference(scs_inference,[],[323,381,149,148,2])).
% 59.38/59.43 cnf(398,plain,
% 59.38/59.43 (P6(f20(f25(f25(a24,a24),f25(a24,a24))),f25(a23,a23))),
% 59.38/59.43 inference(scs_inference,[],[51,323,368,367,381,149,148,2,36,37])).
% 59.38/59.43 cnf(405,plain,
% 59.38/59.43 (~P5(f10(f8(x4051),x4051),f6(x4052,x4053))),
% 59.38/59.43 inference(scs_inference,[],[51,181,331,70,61,323,368,367,381,149,148,2,36,37,3,31,123])).
% 59.38/59.43 cnf(417,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x4171,x4171),f25(x4171,f25(x4172,x4172))),f25(f25(x4171,x4171),f25(x4171,f25(x4172,x4172)))),f25(f25(f25(x4171,x4171),f25(x4171,f25(x4172,x4172))),f25(x4173,x4173))),f19(f19(f19(f10(f8(x4174),x4174)))))),
% 59.38/59.43 inference(scs_inference,[],[325,148])).
% 59.38/59.43 cnf(419,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x4191,x4191),f25(x4191,f25(x4192,x4192))),f25(f25(x4191,x4191),f25(x4191,f25(x4192,x4192)))),f25(f25(f25(x4191,x4191),f25(x4191,f25(x4192,x4192))),f25(x4193,x4193))),f11(f19(f19(f10(f8(x4194),x4194)))))),
% 59.38/59.43 inference(scs_inference,[],[325,148,149])).
% 59.38/59.43 cnf(427,plain,
% 59.38/59.43 (E(f20(f25(a4,a4)),f10(f6(f25(x4271,x4271),a17),f8(f6(f25(x4271,x4271),a17))))),
% 59.38/59.43 inference(scs_inference,[],[188,396,70,65,58,405,325,148,149,94,3,31,2])).
% 59.38/59.43 cnf(440,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x4401,x4401),f25(x4401,f25(x4402,x4402))),f25(f25(x4401,x4401),f25(x4401,f25(x4402,x4402)))),f25(f25(f25(x4401,x4401),f25(x4401,f25(x4402,x4402))),f25(x4403,x4403))),f11(f11(f11(f11(f10(f8(x4404),x4404))))))),
% 59.38/59.43 inference(scs_inference,[],[345,149])).
% 59.38/59.43 cnf(442,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x4421,x4421),f25(x4421,f25(x4422,x4422))),f25(f25(x4421,x4421),f25(x4421,f25(x4422,x4422)))),f25(f25(f25(x4421,x4421),f25(x4421,f25(x4422,x4422))),f25(x4423,x4423))),f19(f11(f11(f11(f10(f8(x4424),x4424))))))),
% 59.38/59.43 inference(scs_inference,[],[345,149,148])).
% 59.38/59.43 cnf(449,plain,
% 59.38/59.43 (~E(f25(f25(x4491,x4491),x4492),a4)),
% 59.38/59.43 inference(scs_inference,[],[181,369,427,69,54,345,405,149,148,94,3,31])).
% 59.38/59.43 cnf(451,plain,
% 59.38/59.43 (~P5(a4,f6(x4511,x4512))),
% 59.38/59.43 inference(scs_inference,[],[181,369,427,69,54,345,405,149,148,94,3,31,123])).
% 59.38/59.43 cnf(468,plain,
% 59.38/59.43 (~P6(f25(f25(x4681,x4681),x4682),a4)),
% 59.38/59.43 inference(scs_inference,[],[449,77])).
% 59.38/59.43 cnf(470,plain,
% 59.38/59.43 (~E(a4,f25(f25(x4701,x4701),x4702))),
% 59.38/59.43 inference(scs_inference,[],[449,77,73])).
% 59.38/59.43 cnf(472,plain,
% 59.38/59.43 (P5(f20(f25(f25(x4721,x4721),x4722)),f25(f25(x4721,x4721),x4722))),
% 59.38/59.43 inference(scs_inference,[],[449,77,73,79])).
% 59.38/59.43 cnf(474,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x4741,x4741),f25(x4741,f25(x4742,x4742))),f25(f25(x4741,x4741),f25(x4741,f25(x4742,x4742)))),f25(f25(f25(x4741,x4741),f25(x4741,f25(x4742,x4742))),f25(x4743,x4743))),f19(f19(f11(f11(f10(f8(x4744),x4744))))))),
% 59.38/59.43 inference(scs_inference,[],[449,347,77,73,79,148])).
% 59.38/59.43 cnf(476,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x4761,x4761),f25(x4761,f25(x4762,x4762))),f25(f25(x4761,x4761),f25(x4761,f25(x4762,x4762)))),f25(f25(f25(x4761,x4761),f25(x4761,f25(x4762,x4762))),f25(x4763,x4763))),f11(f19(f11(f11(f10(f8(x4764),x4764))))))),
% 59.38/59.43 inference(scs_inference,[],[449,347,77,73,79,148,149])).
% 59.38/59.43 cnf(478,plain,
% 59.38/59.43 (~P5(a4,a5)),
% 59.38/59.43 inference(scs_inference,[],[449,53,347,451,77,73,79,148,149,94])).
% 59.38/59.43 cnf(483,plain,
% 59.38/59.43 (E(f20(f25(f25(x4831,x4831),f25(x4831,x4831))),f25(x4831,x4831))),
% 59.38/59.43 inference(scs_inference,[],[427,328,449,53,347,451,77,73,79,148,149,94,3,99])).
% 59.38/59.43 cnf(485,plain,
% 59.38/59.43 (~P1(a5)),
% 59.38/59.43 inference(scs_inference,[],[427,328,449,53,347,451,77,73,79,148,149,94,3,99,76])).
% 59.38/59.43 cnf(487,plain,
% 59.38/59.43 (E(f25(x4871,x4871),f20(f25(f25(x4871,x4871),f25(x4871,x4871))))),
% 59.38/59.43 inference(scs_inference,[],[427,328,449,53,347,451,77,73,79,148,149,94,3,99,76,2])).
% 59.38/59.43 cnf(500,plain,
% 59.38/59.43 (~P5(a4,f19(x5001))),
% 59.38/59.43 inference(scs_inference,[],[62,362,451,148,149,94])).
% 59.38/59.43 cnf(524,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x5241,x5241),f25(x5241,f25(x5242,x5242))),f25(f25(x5241,x5241),f25(x5241,f25(x5242,x5242)))),f25(f25(f25(x5241,x5241),f25(x5241,f25(x5242,x5242))),f25(x5243,x5243))),f19(f19(f19(f11(f10(f8(x5244),x5244))))))),
% 59.38/59.43 inference(scs_inference,[],[364,148])).
% 59.38/59.43 cnf(551,plain,
% 59.38/59.43 (~E(a17,a5)),
% 59.38/59.43 inference(scs_inference,[],[51,487,478,45,54,451,392,149,148,94,3,31])).
% 59.38/59.43 cnf(554,plain,
% 59.38/59.43 (E(f20(f25(f25(a23,a23),f25(a23,a23))),f25(a24,a24))),
% 59.38/59.43 inference(scs_inference,[],[51,487,478,45,54,451,392,149,148,94,3,31,76,2])).
% 59.38/59.43 cnf(599,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x5991,x5991),f25(x5991,f25(x5992,x5992))),f25(f25(x5991,x5991),f25(x5991,f25(x5992,x5992)))),f25(f25(f25(x5991,x5991),f25(x5991,f25(x5992,x5992))),f25(x5993,x5993))),f11(f19(f19(f19(f10(f8(x5994),x5994))))))),
% 59.38/59.43 inference(scs_inference,[],[417,149])).
% 59.38/59.43 cnf(628,plain,
% 59.38/59.43 (~P5(x6281,f20(f25(f25(a24,a24),f25(a24,a24))))+P5(x6281,f25(a23,a23))),
% 59.38/59.43 inference(scs_inference,[],[349,398,66,419,148,149,3,2,94])).
% 59.38/59.43 cnf(644,plain,
% 59.38/59.43 (~E(a4,f20(f25(f25(a4,a4),f25(a4,a4))))),
% 59.38/59.43 inference(scs_inference,[],[379,483,440,149,148,3])).
% 59.38/59.43 cnf(661,plain,
% 59.38/59.43 (~E(a4,f25(x6611,f25(x6612,x6612)))),
% 59.38/59.43 inference(scs_inference,[],[470,52,442,148,149,3])).
% 59.38/59.43 cnf(663,plain,
% 59.38/59.43 (~P5(x6631,f25(a24,a24))+P5(x6631,f20(f25(f25(a24,a24),f25(a24,a24))))),
% 59.38/59.43 inference(scs_inference,[],[470,368,52,442,148,149,3,94])).
% 59.38/59.43 cnf(679,plain,
% 59.38/59.43 (~E(f25(x6791,f25(x6792,x6792)),a4)),
% 59.38/59.43 inference(scs_inference,[],[661,49,59,468,474,149,148,89,37])).
% 59.38/59.43 cnf(712,plain,
% 59.38/59.43 (E(f25(a24,a24),a24)+~P5(f25(a24,a24),f20(f25(f25(a24,a24),f25(a24,a24))))),
% 59.38/59.43 inference(scs_inference,[],[51,644,70,49,367,476,148,149,89,74,79,94,30,31,99])).
% 59.38/59.43 cnf(766,plain,
% 59.38/59.43 (P5(f25(a24,a24),f25(f25(a23,a23),f25(a23,a23)))),
% 59.38/59.43 inference(scs_inference,[],[554,472,524,149,148,30])).
% 59.38/59.43 cnf(865,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x8651,x8651),f25(x8651,f25(x8652,x8652))),f25(f25(x8651,x8651),f25(x8651,f25(x8652,x8652)))),f25(f25(f25(x8651,x8651),f25(x8651,f25(x8652,x8652))),f25(x8653,x8653))),f19(f11(f19(f19(f19(f10(f8(x8654),x8654)))))))),
% 59.38/59.43 inference(scs_inference,[],[599,149,148])).
% 59.38/59.43 cnf(920,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x9201,x9201),f25(x9201,f25(x9202,x9202))),f25(f25(x9201,x9201),f25(x9201,f25(x9202,x9202)))),f25(f25(f25(x9201,x9201),f25(x9201,f25(x9202,x9202))),f25(x9203,x9203))),f11(f11(f19(a4))))),
% 59.38/59.43 inference(scs_inference,[],[233,149])).
% 59.38/59.43 cnf(922,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x9221,x9221),f25(x9221,f25(x9222,x9222))),f25(f25(x9221,x9221),f25(x9221,f25(x9222,x9222)))),f25(f25(f25(x9221,x9221),f25(x9221,f25(x9222,x9222))),f25(x9223,x9223))),f19(f11(f19(a4))))),
% 59.38/59.43 inference(scs_inference,[],[233,149,148])).
% 59.38/59.43 cnf(932,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x9321,x9321),f25(x9321,f25(x9322,x9322))),f25(f25(x9321,x9321),f25(x9321,f25(x9322,x9322)))),f25(f25(f25(x9321,x9321),f25(x9321,f25(x9322,x9322))),f25(x9323,x9323))),f19(f11(f11(f19(a4)))))),
% 59.38/59.43 inference(scs_inference,[],[920,148])).
% 59.38/59.43 cnf(934,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x9341,x9341),f25(x9341,f25(x9342,x9342))),f25(f25(x9341,x9341),f25(x9341,f25(x9342,x9342)))),f25(f25(f25(x9341,x9341),f25(x9341,f25(x9342,x9342))),f25(x9343,x9343))),f11(f11(f11(f19(a4)))))),
% 59.38/59.43 inference(scs_inference,[],[920,148,149])).
% 59.38/59.43 cnf(943,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x9431,x9431),f25(x9431,f25(x9432,x9432))),f25(f25(x9431,x9431),f25(x9431,f25(x9432,x9432)))),f25(f25(f25(x9431,x9431),f25(x9431,f25(x9432,x9432))),f25(x9433,x9433))),f19(f19(f11(f11(f19(a4))))))),
% 59.38/59.43 inference(scs_inference,[],[932,149,148])).
% 59.38/59.43 cnf(1003,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x10031,x10031),f25(x10031,f25(x10032,x10032))),f25(f25(x10031,x10031),f25(x10031,f25(x10032,x10032)))),f25(f25(f25(x10031,x10031),f25(x10031,f25(x10032,x10032))),f25(x10033,x10033))),f19(f19(f19(f11(f11(f19(a4)))))))),
% 59.38/59.43 inference(scs_inference,[],[943,149,148])).
% 59.38/59.43 cnf(1021,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x10211,x10211),f25(x10211,f25(x10212,x10212))),f25(f25(x10211,x10211),f25(x10211,f25(x10212,x10212)))),f25(f25(f25(x10211,x10211),f25(x10211,f25(x10212,x10212))),f25(x10213,x10213))),f19(f19(f19(f19(f11(f11(f19(a4))))))))),
% 59.38/59.43 inference(scs_inference,[],[1003,149,148])).
% 59.38/59.43 cnf(1039,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x10391,x10391),f25(x10391,f25(x10392,x10392))),f25(f25(x10391,x10391),f25(x10391,f25(x10392,x10392)))),f25(f25(f25(x10391,x10391),f25(x10391,f25(x10392,x10392))),f25(x10393,x10393))),f19(f11(f11(f11(f19(a4))))))),
% 59.38/59.43 inference(scs_inference,[],[934,149,148])).
% 59.38/59.43 cnf(1103,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x11031,x11031),f25(x11031,f25(x11032,x11032))),f25(f25(x11031,x11031),f25(x11031,f25(x11032,x11032)))),f25(f25(f25(x11031,x11031),f25(x11031,f25(x11032,x11032))),f25(x11033,x11033))),f19(f19(f11(f11(f11(f19(a4)))))))),
% 59.38/59.43 inference(scs_inference,[],[1039,149,148])).
% 59.38/59.43 cnf(1117,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x11171,x11171),f25(x11171,f25(x11172,x11172))),f25(f25(x11171,x11171),f25(x11171,f25(x11172,x11172)))),f25(f25(f25(x11171,x11171),f25(x11171,f25(x11172,x11172))),f25(x11173,x11173))),f11(f19(f19(f11(f11(f11(f19(a4))))))))),
% 59.38/59.43 inference(scs_inference,[],[1103,149])).
% 59.38/59.43 cnf(1119,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x11191,x11191),f25(x11191,f25(x11192,x11192))),f25(f25(x11191,x11191),f25(x11191,f25(x11192,x11192)))),f25(f25(f25(x11191,x11191),f25(x11191,f25(x11192,x11192))),f25(x11193,x11193))),f19(f19(f19(f11(f11(f11(f19(a4))))))))),
% 59.38/59.43 inference(scs_inference,[],[1103,149,148])).
% 59.38/59.43 cnf(1124,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x11241,x11241),f25(x11241,f25(x11242,x11242))),f25(f25(x11241,x11241),f25(x11241,f25(x11242,x11242)))),f25(f25(f25(x11241,x11241),f25(x11241,f25(x11242,x11242))),f25(x11243,x11243))),f11(f19(f11(f19(a4)))))),
% 59.38/59.43 inference(scs_inference,[],[922,149])).
% 59.38/59.43 cnf(1126,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x11261,x11261),f25(x11261,f25(x11262,x11262))),f25(f25(x11261,x11261),f25(x11261,f25(x11262,x11262)))),f25(f25(f25(x11261,x11261),f25(x11261,f25(x11262,x11262))),f25(x11263,x11263))),f19(f19(f11(f19(a4)))))),
% 59.38/59.43 inference(scs_inference,[],[922,149,148])).
% 59.38/59.43 cnf(1131,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x11311,x11311),f25(x11311,f25(x11312,x11312))),f25(f25(x11311,x11311),f25(x11311,f25(x11312,x11312)))),f25(f25(f25(x11311,x11311),f25(x11311,f25(x11312,x11312))),f25(x11313,x11313))),f11(f11(f19(f11(f19(a4))))))),
% 59.38/59.43 inference(scs_inference,[],[1124,149])).
% 59.38/59.43 cnf(1135,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x11351,x11351),f25(x11351,f25(x11352,x11352))),f25(f25(x11351,x11351),f25(x11351,f25(x11352,x11352)))),f25(f25(f25(x11351,x11351),f25(x11351,f25(x11352,x11352))),f25(x11353,x11353))),f11(f11(f11(f19(f11(f19(a4)))))))),
% 59.38/59.43 inference(scs_inference,[],[1131,149])).
% 59.38/59.43 cnf(1137,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x11371,x11371),f25(x11371,f25(x11372,x11372))),f25(f25(x11371,x11371),f25(x11371,f25(x11372,x11372)))),f25(f25(f25(x11371,x11371),f25(x11371,f25(x11372,x11372))),f25(x11373,x11373))),f19(f11(f11(f19(f11(f19(a4)))))))),
% 59.38/59.43 inference(scs_inference,[],[1131,149,148])).
% 59.38/59.43 cnf(1141,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x11411,x11411),f25(x11411,f25(x11412,x11412))),f25(f25(x11411,x11411),f25(x11411,f25(x11412,x11412)))),f25(f25(f25(x11411,x11411),f25(x11411,f25(x11412,x11412))),f25(x11413,x11413))),f19(f11(f11(f11(f19(f11(f19(a4))))))))),
% 59.38/59.43 inference(scs_inference,[],[1135,149,148])).
% 59.38/59.43 cnf(1143,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x11431,x11431),f25(x11431,f25(x11432,x11432))),f25(f25(x11431,x11431),f25(x11431,f25(x11432,x11432)))),f25(f25(f25(x11431,x11431),f25(x11431,f25(x11432,x11432))),f25(x11433,x11433))),f11(f19(f11(f11(f19(f11(f19(a4))))))))),
% 59.38/59.43 inference(scs_inference,[],[1137,149])).
% 59.38/59.43 cnf(1161,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x11611,x11611),f25(x11611,f25(x11612,x11612))),f25(f25(x11611,x11611),f25(x11611,f25(x11612,x11612)))),f25(f25(f25(x11611,x11611),f25(x11611,f25(x11612,x11612))),f25(x11613,x11613))),f19(f19(f19(f11(f19(a4))))))),
% 59.38/59.43 inference(scs_inference,[],[1126,149,148])).
% 59.38/59.43 cnf(1175,plain,
% 59.38/59.43 (~P5(a4,f8(a17))),
% 59.38/59.43 inference(scs_inference,[],[199,91,76])).
% 59.38/59.43 cnf(1180,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x11801,x11801),f25(x11801,f25(x11802,x11802))),f25(f25(x11801,x11801),f25(x11801,f25(x11802,x11802)))),f25(f25(f25(x11801,x11801),f25(x11801,f25(x11802,x11802))),f25(x11803,x11803))),f19(f19(f19(f19(f11(f19(a4)))))))),
% 59.38/59.43 inference(scs_inference,[],[1175,1161,76,149,148])).
% 59.38/59.43 cnf(1188,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x11881,x11881),f25(x11881,f25(x11882,x11882))),f25(f25(x11881,x11881),f25(x11881,f25(x11882,x11882)))),f25(f25(f25(x11881,x11881),f25(x11881,f25(x11882,x11882))),f25(x11883,x11883))),f19(f19(f19(f19(f19(f11(f19(a4))))))))),
% 59.38/59.43 inference(scs_inference,[],[1180,149,148])).
% 59.38/59.43 cnf(1190,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x11901,x11901),f25(x11901,f25(x11902,x11902))),f25(f25(x11901,x11901),f25(x11901,f25(x11902,x11902)))),f25(f25(f25(x11901,x11901),f25(x11901,f25(x11902,x11902))),f25(x11903,x11903))),f11(f19(f19(a4))))),
% 59.38/59.43 inference(scs_inference,[],[235,149])).
% 59.38/59.43 cnf(1194,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x11941,x11941),f25(x11941,f25(x11942,x11942))),f25(f25(x11941,x11941),f25(x11941,f25(x11942,x11942)))),f25(f25(f25(x11941,x11941),f25(x11941,f25(x11942,x11942))),f25(x11943,x11943))),f11(f11(f19(f19(a4)))))),
% 59.38/59.43 inference(scs_inference,[],[1190,149])).
% 59.38/59.43 cnf(1198,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x11981,x11981),f25(x11981,f25(x11982,x11982))),f25(f25(x11981,x11981),f25(x11981,f25(x11982,x11982)))),f25(f25(f25(x11981,x11981),f25(x11981,f25(x11982,x11982))),f25(x11983,x11983))),f11(f11(f11(f19(f19(a4))))))),
% 59.38/59.43 inference(scs_inference,[],[1194,149])).
% 59.38/59.43 cnf(1202,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x12021,x12021),f25(x12021,f25(x12022,x12022))),f25(f25(x12021,x12021),f25(x12021,f25(x12022,x12022)))),f25(f25(f25(x12021,x12021),f25(x12021,f25(x12022,x12022))),f25(x12023,x12023))),f11(f11(f11(f11(f19(f19(a4)))))))),
% 59.38/59.43 inference(scs_inference,[],[1198,149])).
% 59.38/59.43 cnf(1204,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x12041,x12041),f25(x12041,f25(x12042,x12042))),f25(f25(x12041,x12041),f25(x12041,f25(x12042,x12042)))),f25(f25(f25(x12041,x12041),f25(x12041,f25(x12042,x12042))),f25(x12043,x12043))),f19(f11(f11(f11(f19(f19(a4)))))))),
% 59.38/59.43 inference(scs_inference,[],[1198,149,148])).
% 59.38/59.43 cnf(1208,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x12081,x12081),f25(x12081,f25(x12082,x12082))),f25(f25(x12081,x12081),f25(x12081,f25(x12082,x12082)))),f25(f25(f25(x12081,x12081),f25(x12081,f25(x12082,x12082))),f25(x12083,x12083))),f19(f11(f11(f11(f11(f19(f19(a4))))))))),
% 59.38/59.43 inference(scs_inference,[],[1202,149,148])).
% 59.38/59.43 cnf(1210,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x12101,x12101),f25(x12101,f25(x12102,x12102))),f25(f25(x12101,x12101),f25(x12101,f25(x12102,x12102)))),f25(f25(f25(x12101,x12101),f25(x12101,f25(x12102,x12102))),f25(x12103,x12103))),f11(f19(f11(f11(f11(f19(f19(a4))))))))),
% 59.38/59.43 inference(scs_inference,[],[1204,149])).
% 59.38/59.43 cnf(1212,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x12121,x12121),f25(x12121,f25(x12122,x12122))),f25(f25(x12121,x12121),f25(x12121,f25(x12122,x12122)))),f25(f25(f25(x12121,x12121),f25(x12121,f25(x12122,x12122))),f25(x12123,x12123))),f19(f19(f11(f11(f11(f19(f19(a4))))))))),
% 59.38/59.43 inference(scs_inference,[],[1204,149,148])).
% 59.38/59.43 cnf(1694,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x16941,x16941),f25(x16941,f25(x16942,x16942))),f25(f25(x16941,x16941),f25(x16941,f25(x16942,x16942)))),f25(f25(f25(x16941,x16941),f25(x16941,f25(x16942,x16942))),f25(x16943,x16943))),f19(f19(f11(f19(f19(f19(f10(f8(x16944),x16944))))))))),
% 59.38/59.43 inference(scs_inference,[],[865,149,148])).
% 59.38/59.43 cnf(1749,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x17491,x17491),f25(x17491,f25(x17492,x17492))),f25(f25(x17491,x17491),f25(x17491,f25(x17492,x17492)))),f25(f25(f25(x17491,x17491),f25(x17491,f25(x17492,x17492))),f25(x17493,x17493))),f19(f19(f19(f19(f19(f11(f11(f19(a4)))))))))),
% 59.38/59.43 inference(scs_inference,[],[1021,148])).
% 59.38/59.43 cnf(1779,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x17791,x17791),f25(x17791,f25(x17792,x17792))),f25(f25(x17791,x17791),f25(x17791,f25(x17792,x17792)))),f25(f25(f25(x17791,x17791),f25(x17791,f25(x17792,x17792))),f25(x17793,x17793))),f11(f11(f19(f19(f11(f11(f11(f19(a4)))))))))),
% 59.38/59.43 inference(scs_inference,[],[1117,148,149])).
% 59.38/59.43 cnf(1781,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x17811,x17811),f25(x17811,f25(x17812,x17812))),f25(f25(x17811,x17811),f25(x17811,f25(x17812,x17812)))),f25(f25(f25(x17811,x17811),f25(x17811,f25(x17812,x17812))),f25(x17813,x17813))),f19(f19(f19(f19(f11(f11(f11(f19(a4)))))))))),
% 59.38/59.43 inference(scs_inference,[],[1119,148])).
% 59.38/59.43 cnf(1791,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x17911,x17911),f25(x17911,f25(x17912,x17912))),f25(f25(x17911,x17911),f25(x17911,f25(x17912,x17912)))),f25(f25(f25(x17911,x17911),f25(x17911,f25(x17912,x17912))),f25(x17913,x17913))),f11(f19(f11(f11(f11(f19(f11(f19(a4)))))))))),
% 59.38/59.43 inference(scs_inference,[],[1141,148,149])).
% 59.38/59.43 cnf(1793,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x17931,x17931),f25(x17931,f25(x17932,x17932))),f25(f25(x17931,x17931),f25(x17931,f25(x17932,x17932)))),f25(f25(f25(x17931,x17931),f25(x17931,f25(x17932,x17932))),f25(x17933,x17933))),f19(f11(f19(f11(f11(f19(f11(f19(a4)))))))))),
% 59.38/59.43 inference(scs_inference,[],[1143,148])).
% 59.38/59.43 cnf(1795,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x17951,x17951),f25(x17951,f25(x17952,x17952))),f25(f25(x17951,x17951),f25(x17951,f25(x17952,x17952)))),f25(f25(f25(x17951,x17951),f25(x17951,f25(x17952,x17952))),f25(x17953,x17953))),f11(f11(f19(f11(f11(f19(f11(f19(a4)))))))))),
% 59.38/59.43 inference(scs_inference,[],[1143,148,149])).
% 59.38/59.43 cnf(1848,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x18481,x18481),f25(x18481,f25(x18482,x18482))),f25(f25(x18481,x18481),f25(x18481,f25(x18482,x18482)))),f25(f25(f25(x18481,x18481),f25(x18481,f25(x18482,x18482))),f25(x18483,x18483))),f11(f19(f19(f19(f19(f19(f11(f19(a4)))))))))),
% 59.38/59.43 inference(scs_inference,[],[1188,148,149])).
% 59.38/59.43 cnf(1863,plain,
% 59.38/59.43 (P5(a4,f25(x18631,a4))),
% 59.38/59.43 inference(scs_inference,[],[278,188,69,59,1208,148,149,94,31,30])).
% 59.38/59.43 cnf(1866,plain,
% 59.38/59.43 (~P6(f25(x18661,a4),a4)),
% 59.38/59.43 inference(scs_inference,[],[278,188,69,59,1208,148,149,94,31,30,79,77])).
% 59.38/59.43 cnf(1871,plain,
% 59.38/59.43 (~E(a4,f25(x18711,a4))),
% 59.38/59.43 inference(scs_inference,[],[1866,73])).
% 59.38/59.43 cnf(1878,plain,
% 59.38/59.43 (P5(f25(a24,a24),f25(f25(a23,a23),x18781))),
% 59.38/59.43 inference(scs_inference,[],[766,478,1863,60,1210,1866,73,148,149,31,94])).
% 59.38/59.43 cnf(1887,plain,
% 59.38/59.43 (~E(f25(x18871,a4),f19(x18872))),
% 59.38/59.43 inference(scs_inference,[],[500,1871,1863,52,1212,148,149,3,31])).
% 59.38/59.43 cnf(2877,plain,
% 59.38/59.43 (~P5(f25(x28771,x28771),f8(a17))),
% 59.38/59.43 inference(scs_inference,[],[449,80,91])).
% 59.38/59.43 cnf(2879,plain,
% 59.38/59.43 (~P5(f25(x28791,x28791),f8(a17))),
% 59.38/59.43 inference(rename_variables,[],[2877])).
% 59.38/59.43 cnf(2881,plain,
% 59.38/59.43 (~P5(f25(f25(f25(f25(x28811,x28811),f25(x28811,f25(f25(x28811,x28811),f25(x28811,x28811)))),f25(f25(x28811,x28811),f25(x28811,f25(f25(x28811,x28811),f25(x28811,x28811))))),f25(f25(f25(x28811,x28811),f25(x28811,f25(f25(x28811,x28811),f25(x28811,x28811)))),f25(f25(f25(x28811,x28811),f25(x28811,x28811)),f25(f25(x28811,x28811),f25(x28811,x28811))))),f11(f8(a17)))),
% 59.38/59.43 inference(scs_inference,[],[2877,2879,148,149])).
% 59.38/59.43 cnf(2932,plain,
% 59.38/59.43 (~P5(f8(a17),f6(x29321,x29322))),
% 59.38/59.43 inference(scs_inference,[],[181,2877,1694,148,149,31,123])).
% 59.38/59.43 cnf(3165,plain,
% 59.38/59.43 (~E(f25(f14(a17,a4),x31651),a4)),
% 59.38/59.43 inference(scs_inference,[],[193,87,81])).
% 59.38/59.43 cnf(3166,plain,
% 59.38/59.43 (P5(f14(a17,a4),a17)),
% 59.38/59.43 inference(scs_inference,[],[3165,80])).
% 59.38/59.43 cnf(3167,plain,
% 59.38/59.43 (~E(f25(f14(a17,a4),x31671),a4)),
% 59.38/59.43 inference(rename_variables,[],[3165])).
% 59.38/59.43 cnf(3171,plain,
% 59.38/59.43 (~P6(f25(f14(a17,a4),x31711),a4)),
% 59.38/59.43 inference(scs_inference,[],[3165,3167,80,79,77])).
% 59.38/59.43 cnf(3181,plain,
% 59.38/59.43 (E(f20(f25(f14(a17,a4),f14(a17,a4))),f14(a17,a4))),
% 59.38/59.43 inference(scs_inference,[],[3165,3167,70,1749,80,79,77,148,149,31,73,99])).
% 59.38/59.43 cnf(3321,plain,
% 59.38/59.43 (~P5(a24,f10(x33211,f25(a23,a23)))),
% 59.38/59.43 inference(scs_inference,[],[68,101,99])).
% 59.38/59.43 cnf(3328,plain,
% 59.38/59.43 (~P5(a24,f25(a23,a23))),
% 59.38/59.43 inference(scs_inference,[],[276,1779,3321,148,149,105,94])).
% 59.38/59.43 cnf(3337,plain,
% 59.38/59.43 (~P5(a24,a17)),
% 59.38/59.43 inference(scs_inference,[],[3328,628,311,96])).
% 59.38/59.43 cnf(3343,plain,
% 59.38/59.43 (~E(a23,a24)),
% 59.38/59.43 inference(scs_inference,[],[47,3328,1781,628,311,96,148,149,30])).
% 59.38/59.43 cnf(3369,plain,
% 59.38/59.43 (~E(f25(x33691,x33692),a24)),
% 59.38/59.43 inference(scs_inference,[],[3337,56,1791,148,149,30])).
% 59.38/59.43 cnf(3370,plain,
% 59.38/59.43 (~P5(f25(a24,a24),f20(f25(f25(a24,a24),f25(a24,a24))))),
% 59.38/59.43 inference(scs_inference,[],[3337,56,1791,148,149,30,712])).
% 59.38/59.43 cnf(3371,plain,
% 59.38/59.43 (~P5(f25(a24,a24),f25(a24,a24))),
% 59.38/59.43 inference(scs_inference,[],[3337,56,1791,148,149,30,712,663])).
% 59.38/59.43 cnf(3383,plain,
% 59.38/59.43 (~E(a4,a24)),
% 59.38/59.43 inference(scs_inference,[],[3371,3369,3337,276,45,1793,123,148,149,94,30])).
% 59.38/59.43 cnf(3388,plain,
% 59.38/59.43 (~P6(a24,a4)),
% 59.38/59.43 inference(scs_inference,[],[3383,49,1795,148,149,89])).
% 59.38/59.43 cnf(3392,plain,
% 59.38/59.43 (~E(a24,a4)),
% 59.38/59.43 inference(scs_inference,[],[3383,3337,49,3166,1795,148,149,89,30,74])).
% 59.38/59.43 cnf(3512,plain,
% 59.38/59.43 (P5(f25(a24,a24),f25(x35121,f25(a23,a23)))),
% 59.38/59.43 inference(scs_inference,[],[1878,59,1848,148,149,94])).
% 59.38/59.43 cnf(3594,plain,
% 59.38/59.43 (~P5(f8(a17),f6(x35941,x35942))),
% 59.38/59.43 inference(rename_variables,[],[2932])).
% 59.38/59.43 cnf(3658,plain,
% 59.38/59.43 (~P5(x36581,f9(f8(f6(f25(x36581,x36581),a17))))),
% 59.38/59.43 inference(rename_variables,[],[173])).
% 59.38/59.43 cnf(3689,plain,
% 59.38/59.43 ($false),
% 59.38/59.43 inference(scs_inference,[],[47,551,3343,485,1887,2932,3594,3512,242,2881,3370,3388,3392,679,3171,43,44,173,3658,56,3181,170,167,59,163,487,3337,48,70,91,101,102,85,6,11,15,16,19,23,24,27,86,87,386,4,5,7,8,9,10,17,18,25,26,78,83,84,12,13,14,20,21,22,121,118,126,130,131,128,129,143,95,80,90,81,96,73,76,74,99,2,124,144,92,106,100,3,28,37,36,94,30,31,104,93,105,89,338]),
% 59.38/59.43 ['proof']).
% 59.38/59.43 % SZS output end Proof
% 59.38/59.43 % Total time :58.900000s
%------------------------------------------------------------------------------