%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU303+3 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n027.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 15:02:21 EDT 2024 % Result : Theorem 117.24s 117.56s % Output : CNFRefutation 117.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU303+3 : TPTP v8.2.0. Released v3.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.33 % Computer : n027.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Fri Jun 21 12:44:09 EDT 2024 % 0.11/0.33 % CPUTime : % 0.49/0.60 start to proof:theBenchmark % 117.18/117.54 %------------------------------------------- % 117.18/117.54 % File :CSE---1.7 % 117.18/117.54 % Problem :theBenchmark % 117.18/117.54 % Transform :cnf % 117.18/117.54 % Format :tptp:raw % 117.18/117.54 % Command :java -jar mcs_scs.jar %d %s % 117.18/117.54 % 117.18/117.54 % Result :Theorem 116.580000s % 117.18/117.54 % Output :CNFRefutation 116.580000s % 117.18/117.54 %------------------------------------------- % 117.24/117.55 %------------------------------------------------------------------------------ % 117.24/117.55 % File : SEU303+3 : TPTP v8.2.0. Released v3.2.0. % 117.24/117.55 % Domain : Set theory % 117.24/117.55 % Problem : Finite sets, theorem 26 % 117.24/117.55 % Version : [Urb06] axioms : Especial. % 117.24/117.55 % English : % 117.24/117.55 % 117.24/117.55 % Refs : [Dar90] Darmochwal (1990), Finite Sets % 117.24/117.55 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 117.24/117.55 % Source : [Urb06] % 117.24/117.55 % Names : finset_1__t26_finset_1 [Urb06] % 117.24/117.55 % 117.24/117.55 % Status : Theorem % 117.24/117.55 % Rating : 0.14 v8.1.0, 0.08 v7.5.0, 0.09 v7.4.0, 0.03 v7.3.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.17 v6.2.0, 0.16 v6.1.0, 0.20 v6.0.0, 0.09 v5.5.0, 0.19 v5.4.0, 0.21 v5.3.0, 0.26 v5.2.0, 0.10 v5.1.0, 0.14 v5.0.0, 0.17 v4.1.0, 0.22 v4.0.0, 0.25 v3.7.0, 0.10 v3.5.0, 0.11 v3.3.0, 0.07 v3.2.0 % 117.24/117.55 % Syntax : Number of formulae : 63 ( 7 unt; 0 def) % 117.24/117.55 % Number of atoms : 205 ( 3 equ) % 117.24/117.55 % Maximal formula atoms : 10 ( 3 avg) % 117.24/117.55 % Number of connectives : 163 ( 21 ~; 1 |; 107 &) % 117.24/117.55 % ( 1 <=>; 33 =>; 0 <=; 0 <~>) % 117.24/117.55 % Maximal formula depth : 12 ( 5 avg) % 117.24/117.55 % Maximal term depth : 3 ( 1 avg) % 117.24/117.55 % Number of predicates : 20 ( 19 usr; 0 prp; 1-2 aty) % 117.24/117.55 % Number of functors : 6 ( 6 usr; 2 con; 0-2 aty) % 117.24/117.55 % Number of variables : 78 ( 52 !; 26 ?) % 117.24/117.55 % SPC : FOF_THM_RFO_SEQ % 117.24/117.55 % 117.24/117.55 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 117.24/117.55 % library, www.mizar.org % 117.24/117.55 %------------------------------------------------------------------------------ % 117.24/117.55 fof(antisymmetry_r2_hidden,axiom, % 117.24/117.55 ! [A,B] : % 117.24/117.55 ( in(A,B) % 117.24/117.55 => ~ in(B,A) ) ). % 117.24/117.55 % 117.24/117.55 fof(cc1_arytm_3,axiom, % 117.24/117.55 ! [A] : % 117.24/117.55 ( ordinal(A) % 117.24/117.55 => ! [B] : % 117.24/117.55 ( element(B,A) % 117.24/117.55 => ( epsilon_transitive(B) % 117.24/117.55 & epsilon_connected(B) % 117.24/117.55 & ordinal(B) ) ) ) ). % 117.24/117.55 % 117.24/117.55 fof(cc1_finset_1,axiom, % 117.24/117.55 ! [A] : % 117.24/117.55 ( empty(A) % 117.24/117.55 => finite(A) ) ). % 117.24/117.55 % 117.24/117.55 fof(cc1_funct_1,axiom, % 117.24/117.55 ! [A] : % 117.24/117.55 ( empty(A) % 117.24/117.55 => function(A) ) ). % 117.24/117.55 % 117.24/117.55 fof(cc1_ordinal1,axiom, % 117.24/117.55 ! [A] : % 117.24/117.55 ( ordinal(A) % 117.24/117.55 => ( epsilon_transitive(A) % 117.24/117.55 & epsilon_connected(A) ) ) ). % 117.24/117.55 % 117.24/117.55 fof(cc1_relat_1,axiom, % 117.24/117.55 ! [A] : % 117.24/117.55 ( empty(A) % 117.24/117.55 => relation(A) ) ). % 117.24/117.55 % 117.24/117.55 fof(cc2_arytm_3,axiom, % 117.24/117.55 ! [A] : % 117.24/117.55 ( ( empty(A) % 117.24/117.55 & ordinal(A) ) % 117.24/117.55 => ( epsilon_transitive(A) % 117.24/117.55 & epsilon_connected(A) % 117.24/117.55 & ordinal(A) % 117.24/117.55 & natural(A) ) ) ). % 117.24/117.55 % 117.24/117.55 fof(cc2_finset_1,axiom, % 117.24/117.55 ! [A] : % 117.24/117.55 ( finite(A) % 117.24/117.55 => ! [B] : % 117.24/117.55 ( element(B,powerset(A)) % 117.24/117.55 => finite(B) ) ) ). % 117.24/117.55 % 117.24/117.55 fof(cc2_funct_1,axiom, % 117.24/117.55 ! [A] : % 117.24/117.55 ( ( relation(A) % 117.24/117.55 & empty(A) % 117.24/117.55 & function(A) ) % 117.24/117.55 => ( relation(A) % 117.24/117.55 & function(A) % 117.24/117.55 & one_to_one(A) ) ) ). % 117.24/117.55 % 117.24/117.55 fof(cc2_ordinal1,axiom, % 117.24/117.55 ! [A] : % 117.24/117.55 ( ( epsilon_transitive(A) % 117.24/117.55 & epsilon_connected(A) ) % 117.24/117.55 => ordinal(A) ) ). % 117.24/117.55 % 117.24/117.55 fof(cc3_ordinal1,axiom, % 117.24/117.55 ! [A] : % 117.24/117.55 ( empty(A) % 117.24/117.55 => ( epsilon_transitive(A) % 117.24/117.55 & epsilon_connected(A) % 117.24/117.55 & ordinal(A) ) ) ). % 117.24/117.55 % 117.24/117.55 fof(cc4_arytm_3,axiom, % 117.24/117.55 ! [A] : % 117.24/117.55 ( element(A,positive_rationals) % 117.24/117.55 => ( ordinal(A) % 117.24/117.55 => ( epsilon_transitive(A) % 117.24/117.55 & epsilon_connected(A) % 117.24/117.55 & ordinal(A) % 117.24/117.55 & natural(A) ) ) ) ). % 117.24/117.55 % 117.24/117.55 fof(existence_m1_subset_1,axiom, % 117.24/117.55 ! [A] : % 117.24/117.55 ? [B] : element(B,A) ). % 117.24/117.55 % 117.24/117.55 fof(fc12_relat_1,axiom, % 117.24/117.55 ( empty(empty_set) % 117.24/117.55 & relation(empty_set) % 117.24/117.55 & relation_empty_yielding(empty_set) ) ). % 117.24/117.55 % 117.24/117.55 fof(fc13_finset_1,axiom, % 117.24/117.55 ! [A,B] : % 117.24/117.55 ( ( relation(A) % 117.24/117.55 & function(A) % 117.24/117.55 & finite(B) ) % 117.24/117.55 => finite(relation_image(A,B)) ) ). % 117.24/117.55 % 117.24/117.55 fof(fc1_subset_1,axiom, % 117.24/117.55 ! [A] : ~ empty(powerset(A)) ). % 117.24/117.55 % 117.24/117.55 fof(fc1_xboole_0,axiom, % 117.24/117.55 empty(empty_set) ). % 117.24/117.55 % 117.24/117.55 fof(fc2_ordinal1,axiom, % 117.24/117.55 ( relation(empty_set) % 117.24/117.55 & relation_empty_yielding(empty_set) % 117.24/117.55 & function(empty_set) % 117.24/117.55 & one_to_one(empty_set) % 117.24/117.55 & empty(empty_set) % 117.24/117.55 & epsilon_transitive(empty_set) % 117.24/117.55 & epsilon_connected(empty_set) % 117.24/117.55 & ordinal(empty_set) ) ). % 117.24/117.55 % 117.24/117.55 fof(fc4_relat_1,axiom, % 117.24/117.55 ( empty(empty_set) % 117.24/117.55 & relation(empty_set) ) ). % 117.24/117.55 % 117.24/117.55 fof(fc5_ordinal1,axiom, % 117.24/117.55 ! [A] : % 117.24/117.55 ( ( relation(A) % 117.24/117.55 & function(A) % 117.24/117.55 & transfinite_sequence(A) ) % 117.24/117.55 => ( epsilon_transitive(relation_dom(A)) % 117.24/117.55 & epsilon_connected(relation_dom(A)) % 117.24/117.55 & ordinal(relation_dom(A)) ) ) ). % 117.24/117.55 % 117.24/117.55 fof(fc5_relat_1,axiom, % 117.24/117.55 ! [A] : % 117.24/117.55 ( ( ~ empty(A) % 117.24/117.55 & relation(A) ) % 117.24/117.55 => ~ empty(relation_dom(A)) ) ). % 117.24/117.55 % 117.24/117.55 fof(fc6_funct_1,axiom, % 117.24/117.55 ! [A] : % 117.24/117.55 ( ( relation(A) % 117.24/117.55 & relation_non_empty(A) % 117.24/117.55 & function(A) ) % 117.24/117.55 => with_non_empty_elements(relation_rng(A)) ) ). % 117.24/117.55 % 117.24/117.55 fof(fc6_relat_1,axiom, % 117.24/117.55 ! [A] : % 117.24/117.55 ( ( ~ empty(A) % 117.24/117.55 & relation(A) ) % 117.24/117.55 => ~ empty(relation_rng(A)) ) ). % 117.24/117.55 % 117.24/117.55 fof(fc7_relat_1,axiom, % 117.24/117.55 ! [A] : % 117.24/117.55 ( empty(A) % 117.24/117.55 => ( empty(relation_dom(A)) % 117.24/117.55 & relation(relation_dom(A)) ) ) ). % 117.24/117.55 % 117.24/117.55 fof(fc8_arytm_3,axiom, % 117.24/117.55 ~ empty(positive_rationals) ). % 117.24/117.55 % 117.24/117.55 fof(fc8_relat_1,axiom, % 117.24/117.55 ! [A] : % 117.24/117.55 ( empty(A) % 117.24/117.55 => ( empty(relation_rng(A)) % 117.24/117.55 & relation(relation_rng(A)) ) ) ). % 117.24/117.55 % 117.24/117.55 fof(rc1_arytm_3,axiom, % 117.24/117.55 ? [A] : % 117.24/117.55 ( ~ empty(A) % 117.24/117.55 & epsilon_transitive(A) % 117.24/117.55 & epsilon_connected(A) % 117.24/117.55 & ordinal(A) % 117.24/117.55 & natural(A) ) ). % 117.24/117.55 % 117.24/117.55 fof(rc1_finset_1,axiom, % 117.24/117.55 ? [A] : % 117.24/117.55 ( ~ empty(A) % 117.24/117.56 & finite(A) ) ). % 117.24/117.56 % 117.24/117.56 fof(rc1_funcop_1,axiom, % 117.24/117.56 ? [A] : % 117.24/117.56 ( relation(A) % 117.24/117.56 & function(A) % 117.24/117.56 & function_yielding(A) ) ). % 117.24/117.56 % 117.24/117.56 fof(rc1_funct_1,axiom, % 117.24/117.56 ? [A] : % 117.24/117.56 ( relation(A) % 117.24/117.56 & function(A) ) ). % 117.24/117.56 % 117.24/117.56 fof(rc1_ordinal1,axiom, % 117.24/117.56 ? [A] : % 117.24/117.56 ( epsilon_transitive(A) % 117.24/117.56 & epsilon_connected(A) % 117.24/117.56 & ordinal(A) ) ). % 117.24/117.56 % 117.24/117.56 fof(rc1_ordinal2,axiom, % 117.24/117.56 ? [A] : % 117.24/117.56 ( epsilon_transitive(A) % 117.24/117.56 & epsilon_connected(A) % 117.24/117.56 & ordinal(A) % 117.24/117.56 & being_limit_ordinal(A) ) ). % 117.24/117.56 % 117.24/117.56 fof(rc1_relat_1,axiom, % 117.24/117.56 ? [A] : % 117.24/117.56 ( empty(A) % 117.24/117.56 & relation(A) ) ). % 117.24/117.56 % 117.24/117.56 fof(rc1_subset_1,axiom, % 117.24/117.56 ! [A] : % 117.24/117.56 ( ~ empty(A) % 117.24/117.56 => ? [B] : % 117.24/117.56 ( element(B,powerset(A)) % 117.24/117.56 & ~ empty(B) ) ) ). % 117.24/117.56 % 117.24/117.56 fof(rc1_xboole_0,axiom, % 117.24/117.56 ? [A] : empty(A) ). % 117.24/117.56 % 117.24/117.56 fof(rc2_arytm_3,axiom, % 117.24/117.56 ? [A] : % 117.24/117.56 ( element(A,positive_rationals) % 117.24/117.56 & ~ empty(A) % 117.24/117.56 & epsilon_transitive(A) % 117.24/117.56 & epsilon_connected(A) % 117.24/117.56 & ordinal(A) ) ). % 117.24/117.56 % 117.24/117.56 fof(rc2_finset_1,axiom, % 117.24/117.56 ! [A] : % 117.24/117.56 ? [B] : % 117.24/117.56 ( element(B,powerset(A)) % 117.24/117.56 & empty(B) % 117.24/117.56 & relation(B) % 117.24/117.56 & function(B) % 117.24/117.56 & one_to_one(B) % 117.24/117.56 & epsilon_transitive(B) % 117.24/117.56 & epsilon_connected(B) % 117.24/117.56 & ordinal(B) % 117.24/117.56 & natural(B) % 117.24/117.56 & finite(B) ) ). % 117.24/117.56 % 117.24/117.56 fof(rc2_funct_1,axiom, % 117.24/117.56 ? [A] : % 117.24/117.56 ( relation(A) % 117.24/117.56 & empty(A) % 117.24/117.56 & function(A) ) ). % 117.24/117.56 % 117.24/117.56 fof(rc2_ordinal1,axiom, % 117.24/117.56 ? [A] : % 117.24/117.56 ( relation(A) % 117.24/117.56 & function(A) % 117.24/117.56 & one_to_one(A) % 117.24/117.56 & empty(A) % 117.24/117.56 & epsilon_transitive(A) % 117.24/117.56 & epsilon_connected(A) % 117.24/117.56 & ordinal(A) ) ). % 117.24/117.56 % 117.24/117.56 fof(rc2_ordinal2,axiom, % 117.24/117.56 ? [A] : % 117.24/117.56 ( relation(A) % 117.24/117.56 & function(A) % 117.24/117.56 & transfinite_sequence(A) % 117.24/117.56 & ordinal_yielding(A) ) ). % 117.24/117.56 % 117.24/117.56 fof(rc2_relat_1,axiom, % 117.24/117.56 ? [A] : % 117.24/117.56 ( ~ empty(A) % 117.24/117.56 & relation(A) ) ). % 117.24/117.56 % 117.24/117.56 fof(rc2_subset_1,axiom, % 117.24/117.56 ! [A] : % 117.24/117.56 ? [B] : % 117.24/117.56 ( element(B,powerset(A)) % 117.24/117.56 & empty(B) ) ). % 117.24/117.56 % 117.24/117.56 fof(rc2_xboole_0,axiom, % 117.24/117.56 ? [A] : ~ empty(A) ). % 117.24/117.56 % 117.24/117.56 fof(rc3_arytm_3,axiom, % 117.24/117.56 ? [A] : % 117.24/117.56 ( element(A,positive_rationals) % 117.24/117.56 & empty(A) % 117.24/117.56 & epsilon_transitive(A) % 117.24/117.56 & epsilon_connected(A) % 117.24/117.56 & ordinal(A) % 117.24/117.56 & natural(A) ) ). % 117.24/117.56 % 117.24/117.56 fof(rc3_finset_1,axiom, % 117.24/117.56 ! [A] : % 117.24/117.56 ( ~ empty(A) % 117.24/117.56 => ? [B] : % 117.24/117.56 ( element(B,powerset(A)) % 117.24/117.56 & ~ empty(B) % 117.24/117.56 & finite(B) ) ) ). % 117.24/117.56 % 117.24/117.56 fof(rc3_funct_1,axiom, % 117.24/117.56 ? [A] : % 117.24/117.56 ( relation(A) % 117.24/117.56 & function(A) % 117.24/117.56 & one_to_one(A) ) ). % 117.24/117.56 % 117.24/117.56 fof(rc3_ordinal1,axiom, % 117.24/117.56 ? [A] : % 117.24/117.56 ( ~ empty(A) % 117.24/117.56 & epsilon_transitive(A) % 117.24/117.56 & epsilon_connected(A) % 117.24/117.56 & ordinal(A) ) ). % 117.24/117.56 % 117.24/117.56 fof(rc3_relat_1,axiom, % 117.24/117.56 ? [A] : % 117.24/117.56 ( relation(A) % 117.24/117.56 & relation_empty_yielding(A) ) ). % 117.24/117.56 % 117.24/117.56 fof(rc4_funct_1,axiom, % 117.24/117.56 ? [A] : % 117.24/117.56 ( relation(A) % 117.24/117.56 & relation_empty_yielding(A) % 117.24/117.56 & function(A) ) ). % 117.24/117.56 % 117.24/117.56 fof(rc4_ordinal1,axiom, % 117.24/117.56 ? [A] : % 117.24/117.56 ( relation(A) % 117.24/117.56 & function(A) % 117.24/117.56 & transfinite_sequence(A) ) ). % 117.24/117.56 % 117.24/117.56 fof(rc5_funct_1,axiom, % 117.24/117.56 ? [A] : % 117.24/117.56 ( relation(A) % 117.24/117.56 & relation_non_empty(A) % 117.24/117.56 & function(A) ) ). % 117.24/117.56 % 117.24/117.56 fof(reflexivity_r1_tarski,axiom, % 117.24/117.56 ! [A,B] : subset(A,A) ). % 117.24/117.56 % 117.24/117.56 fof(t146_relat_1,axiom, % 117.24/117.56 ! [A] : % 117.24/117.56 ( relation(A) % 117.24/117.56 => relation_image(A,relation_dom(A)) = relation_rng(A) ) ). % 117.24/117.56 % 117.24/117.56 fof(t17_finset_1,axiom, % 117.24/117.56 ! [A,B] : % 117.24/117.56 ( ( relation(B) % 117.24/117.56 & function(B) ) % 117.24/117.56 => ( finite(A) % 117.24/117.56 => finite(relation_image(B,A)) ) ) ). % 117.24/117.56 % 117.24/117.56 fof(t1_subset,axiom, % 117.24/117.56 ! [A,B] : % 117.24/117.56 ( in(A,B) % 117.24/117.56 => element(A,B) ) ). % 117.24/117.56 % 117.24/117.56 fof(t26_finset_1,conjecture, % 117.24/117.56 ! [A] : % 117.24/117.56 ( ( relation(A) % 117.24/117.56 & function(A) ) % 117.24/117.56 => ( finite(relation_dom(A)) % 117.24/117.56 => finite(relation_rng(A)) ) ) ). % 117.24/117.56 % 117.24/117.56 fof(t2_subset,axiom, % 117.24/117.56 ! [A,B] : % 117.24/117.56 ( element(A,B) % 117.24/117.56 => ( empty(B) % 117.24/117.56 | in(A,B) ) ) ). % 117.24/117.56 % 117.24/117.56 fof(t3_subset,axiom, % 117.24/117.56 ! [A,B] : % 117.24/117.56 ( element(A,powerset(B)) % 117.24/117.56 <=> subset(A,B) ) ). % 117.24/117.56 % 117.24/117.56 fof(t4_subset,axiom, % 117.24/117.56 ! [A,B,C] : % 117.24/117.56 ( ( in(A,B) % 117.24/117.56 & element(B,powerset(C)) ) % 117.24/117.56 => element(A,C) ) ). % 117.24/117.56 % 117.24/117.56 fof(t5_subset,axiom, % 117.24/117.56 ! [A,B,C] : % 117.24/117.56 ~ ( in(A,B) % 117.24/117.56 & element(B,powerset(C)) % 117.24/117.56 & empty(C) ) ). % 117.24/117.56 % 117.24/117.56 fof(t6_boole,axiom, % 117.24/117.56 ! [A] : % 117.24/117.56 ( empty(A) % 117.24/117.56 => A = empty_set ) ). % 117.24/117.56 % 117.24/117.56 fof(t7_boole,axiom, % 117.24/117.56 ! [A,B] : % 117.24/117.56 ~ ( in(A,B) % 117.24/117.56 & empty(B) ) ). % 117.24/117.56 % 117.24/117.56 fof(t8_boole,axiom, % 117.24/117.56 ! [A,B] : % 117.24/117.56 ~ ( empty(A) % 117.24/117.56 & A != B % 117.24/117.56 & empty(B) ) ). % 117.24/117.56 % 117.24/117.56 %------------------------------------------------------------------------------ % 117.24/117.56 %------------------------------------------- % 117.24/117.56 % Proof found % 117.24/117.56 % SZS status Theorem for theBenchmark % 117.24/117.56 % SZS output start Proof % 117.24/117.56 %ClaNum:185(EqnAxiom:35) % 117.24/117.56 %VarNum:156(SingletonVarNum:74) % 117.24/117.56 %MaxLitNum:4 % 117.24/117.56 %MaxfuncDepth:2 % 117.24/117.56 %SharedTerms:107 % 117.24/117.56 %goalClause: 80 96 112 136 % 117.24/117.56 %singleGoalClaCount:4 % 117.24/117.56 [36]P1(a1) % 117.24/117.56 [37]P1(a2) % 117.24/117.56 [38]P1(a22) % 117.24/117.56 [39]P1(a26) % 117.24/117.56 [40]P1(a3) % 117.24/117.56 [41]P1(a5) % 117.24/117.56 [42]P1(a8) % 117.24/117.56 [43]P1(a13) % 117.24/117.56 [44]P2(a1) % 117.24/117.56 [45]P2(a2) % 117.24/117.56 [46]P2(a22) % 117.24/117.56 [47]P2(a26) % 117.24/117.56 [48]P2(a3) % 117.24/117.56 [49]P2(a5) % 117.24/117.56 [50]P2(a8) % 117.24/117.56 [51]P2(a13) % 117.24/117.56 [52]P3(a1) % 117.24/117.56 [53]P3(a2) % 117.24/117.56 [54]P3(a22) % 117.24/117.56 [55]P3(a26) % 117.24/117.56 [56]P3(a3) % 117.24/117.56 [57]P3(a5) % 117.24/117.56 [58]P3(a8) % 117.24/117.56 [59]P3(a13) % 117.24/117.56 [63]P4(a1) % 117.24/117.56 [64]P4(a27) % 117.24/117.56 [65]P4(a4) % 117.24/117.56 [66]P4(a6) % 117.24/117.56 [67]P4(a5) % 117.24/117.56 [68]P4(a8) % 117.24/117.56 [69]P7(a23) % 117.24/117.56 [70]P8(a1) % 117.24/117.56 [71]P8(a24) % 117.24/117.56 [72]P8(a25) % 117.24/117.56 [73]P8(a6) % 117.24/117.56 [74]P8(a5) % 117.24/117.56 [75]P8(a9) % 117.24/117.56 [76]P8(a14) % 117.24/117.56 [77]P8(a17) % 117.24/117.56 [78]P8(a19) % 117.24/117.56 [79]P8(a20) % 117.24/117.56 [80]P8(a21) % 117.24/117.56 [83]P13(a1) % 117.24/117.56 [84]P13(a24) % 117.24/117.56 [85]P13(a25) % 117.24/117.56 [86]P13(a27) % 117.24/117.56 [87]P13(a6) % 117.24/117.56 [88]P13(a5) % 117.24/117.56 [89]P13(a9) % 117.24/117.56 [90]P13(a10) % 117.24/117.56 [91]P13(a14) % 117.24/117.56 [92]P13(a18) % 117.24/117.56 [93]P13(a17) % 117.24/117.56 [94]P13(a19) % 117.24/117.56 [95]P13(a20) % 117.24/117.56 [96]P13(a21) % 117.24/117.56 [97]P9(a2) % 117.24/117.56 [98]P9(a8) % 117.24/117.56 [99]P12(a1) % 117.24/117.56 [100]P12(a5) % 117.24/117.56 [101]P12(a14) % 117.24/117.56 [103]P15(a1) % 117.24/117.56 [104]P15(a18) % 117.24/117.56 [105]P15(a17) % 117.24/117.56 [106]P16(a9) % 117.24/117.56 [107]P16(a19) % 117.24/117.56 [108]P17(a20) % 117.24/117.56 [109]P10(a24) % 117.24/117.56 [110]P5(a26) % 117.24/117.56 [111]P14(a9) % 117.24/117.56 [123]P6(a3,a29) % 117.24/117.56 [124]P6(a8,a29) % 117.24/117.56 [129]~P4(a29) % 117.24/117.56 [130]~P4(a2) % 117.24/117.56 [131]~P4(a23) % 117.24/117.56 [132]~P4(a3) % 117.24/117.56 [133]~P4(a10) % 117.24/117.56 [134]~P4(a12) % 117.24/117.56 [135]~P4(a13) % 117.24/117.57 [112]P7(f28(a21)) % 117.24/117.57 [136]~P7(f32(a21)) % 117.24/117.57 [125]P18(x1251,x1251) % 117.24/117.57 [113]P1(f7(x1131)) % 117.24/117.57 [114]P2(f7(x1141)) % 117.24/117.57 [115]P3(f7(x1151)) % 117.24/117.57 [116]P4(f7(x1161)) % 117.24/117.57 [117]P4(f11(x1171)) % 117.24/117.57 [118]P7(f7(x1181)) % 117.24/117.57 [119]P8(f7(x1191)) % 117.24/117.57 [120]P13(f7(x1201)) % 117.24/117.57 [121]P9(f7(x1211)) % 117.24/117.57 [122]P12(f7(x1221)) % 117.24/117.57 [126]P6(f15(x1261),x1261) % 117.24/117.57 [127]P6(f7(x1271),f31(x1271)) % 117.24/117.57 [128]P6(f11(x1281),f31(x1281)) % 117.24/117.57 [137]~P4(f31(x1371)) % 117.24/117.57 [138]~P4(x1381)+E(x1381,a1) % 117.24/117.57 [139]~P4(x1391)+P1(x1391) % 117.24/117.57 [140]~P1(x1401)+P2(x1401) % 117.24/117.57 [141]~P4(x1411)+P2(x1411) % 117.24/117.57 [142]~P1(x1421)+P3(x1421) % 117.24/117.57 [143]~P4(x1431)+P3(x1431) % 117.24/117.57 [144]~P4(x1441)+P7(x1441) % 117.24/117.57 [145]~P4(x1451)+P8(x1451) % 117.24/117.57 [146]~P4(x1461)+P13(x1461) % 117.24/117.57 [147]P4(x1471)+P7(f16(x1471)) % 117.24/117.57 [149]~P4(x1491)+P4(f28(x1491)) % 117.24/117.57 [150]~P4(x1501)+P4(f32(x1501)) % 117.24/117.57 [151]~P4(x1511)+P13(f28(x1511)) % 117.24/117.57 [152]~P4(x1521)+P13(f32(x1521)) % 117.24/117.57 [157]P4(x1571)+~P4(f30(x1571)) % 117.24/117.57 [158]P4(x1581)+~P4(f16(x1581)) % 117.24/117.57 [163]P4(x1631)+P6(f30(x1631),f31(x1631)) % 117.24/117.57 [164]P4(x1641)+P6(f16(x1641),f31(x1641)) % 117.24/117.57 [165]~P13(x1651)+E(f33(x1651,f28(x1651)),f32(x1651)) % 117.24/117.57 [162]~P4(x1621)+~P11(x1622,x1621) % 117.24/117.57 [176]~P11(x1761,x1762)+P6(x1761,x1762) % 117.24/117.57 [180]~P11(x1802,x1801)+~P11(x1801,x1802) % 117.24/117.57 [178]~P18(x1781,x1782)+P6(x1781,f31(x1782)) % 117.24/117.57 [181]P18(x1811,x1812)+~P6(x1811,f31(x1812)) % 117.24/117.57 [153]~P2(x1531)+~P3(x1531)+P1(x1531) % 117.24/117.57 [156]~P1(x1561)+~P4(x1561)+P9(x1561) % 117.24/117.57 [168]~P1(x1681)+P9(x1681)+~P6(x1681,a29) % 117.24/117.57 [160]~P13(x1601)+P4(x1601)+~P4(f28(x1601)) % 117.24/117.57 [161]~P13(x1611)+P4(x1611)+~P4(f32(x1611)) % 117.24/117.57 [148]~P4(x1482)+~P4(x1481)+E(x1481,x1482) % 117.24/117.57 [173]~P6(x1731,x1732)+P1(x1731)+~P1(x1732) % 117.24/117.57 [174]~P6(x1741,x1742)+P2(x1741)+~P1(x1742) % 117.24/117.57 [175]~P6(x1751,x1752)+P3(x1751)+~P1(x1752) % 117.24/117.57 [177]~P6(x1772,x1771)+P4(x1771)+P11(x1772,x1771) % 117.24/117.57 [179]P7(x1791)+~P7(x1792)+~P6(x1791,f31(x1792)) % 117.24/117.57 [184]~P4(x1841)+~P11(x1842,x1843)+~P6(x1843,f31(x1841)) % 117.24/117.57 [185]P6(x1851,x1852)+~P11(x1851,x1853)+~P6(x1853,f31(x1852)) % 117.24/117.57 [159]~P4(x1591)+~P8(x1591)+~P13(x1591)+P12(x1591) % 117.24/117.57 [169]~P8(x1691)+~P13(x1691)+~P16(x1691)+P1(f28(x1691)) % 117.24/117.57 [170]~P8(x1701)+~P13(x1701)+~P16(x1701)+P2(f28(x1701)) % 117.24/117.57 [171]~P8(x1711)+~P13(x1711)+~P16(x1711)+P3(f28(x1711)) % 117.24/117.57 [172]~P8(x1721)+~P13(x1721)+~P17(x1721)+P19(f32(x1721)) % 117.24/117.57 [183]~P7(x1832)+~P8(x1831)+~P13(x1831)+P7(f33(x1831,x1832)) % 117.24/117.57 %EqnAxiom % 117.24/117.57 [1]E(x11,x11) % 117.24/117.57 [2]E(x22,x21)+~E(x21,x22) % 117.24/117.57 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 117.24/117.57 [4]~E(x41,x42)+E(f28(x41),f28(x42)) % 117.24/117.57 [5]~E(x51,x52)+E(f7(x51),f7(x52)) % 117.24/117.57 [6]~E(x61,x62)+E(f32(x61),f32(x62)) % 117.24/117.57 [7]~E(x71,x72)+E(f31(x71),f31(x72)) % 117.24/117.57 [8]~E(x81,x82)+E(f30(x81),f30(x82)) % 117.24/117.57 [9]~E(x91,x92)+E(f11(x91),f11(x92)) % 117.24/117.57 [10]~E(x101,x102)+E(f16(x101),f16(x102)) % 117.24/117.57 [11]~E(x111,x112)+E(f33(x111,x113),f33(x112,x113)) % 117.24/117.57 [12]~E(x121,x122)+E(f33(x123,x121),f33(x123,x122)) % 117.24/117.57 [13]~E(x131,x132)+E(f15(x131),f15(x132)) % 117.24/117.57 [14]~P1(x141)+P1(x142)+~E(x141,x142) % 117.24/117.57 [15]P6(x152,x153)+~E(x151,x152)+~P6(x151,x153) % 117.24/117.57 [16]P6(x163,x162)+~E(x161,x162)+~P6(x163,x161) % 117.24/117.57 [17]P11(x172,x173)+~E(x171,x172)+~P11(x171,x173) % 117.24/117.57 [18]P11(x183,x182)+~E(x181,x182)+~P11(x183,x181) % 117.24/117.57 [19]~P8(x191)+P8(x192)+~E(x191,x192) % 117.24/117.57 [20]~P4(x201)+P4(x202)+~E(x201,x202) % 117.24/117.57 [21]~P3(x211)+P3(x212)+~E(x211,x212) % 117.24/117.57 [22]~P13(x221)+P13(x222)+~E(x221,x222) % 117.24/117.57 [23]~P2(x231)+P2(x232)+~E(x231,x232) % 117.24/117.57 [24]~P9(x241)+P9(x242)+~E(x241,x242) % 117.24/117.57 [25]~P7(x251)+P7(x252)+~E(x251,x252) % 117.24/117.57 [26]~P12(x261)+P12(x262)+~E(x261,x262) % 117.24/117.57 [27]~P16(x271)+P16(x272)+~E(x271,x272) % 117.24/117.57 [28]~P5(x281)+P5(x282)+~E(x281,x282) % 117.24/117.57 [29]~P15(x291)+P15(x292)+~E(x291,x292) % 117.24/117.57 [30]P18(x302,x303)+~E(x301,x302)+~P18(x301,x303) % 117.24/117.57 [31]P18(x313,x312)+~E(x311,x312)+~P18(x313,x311) % 117.24/117.57 [32]~P17(x321)+P17(x322)+~E(x321,x322) % 117.24/117.57 [33]~P10(x331)+P10(x332)+~E(x331,x332) % 117.24/117.57 [34]~P19(x341)+P19(x342)+~E(x341,x342) % 117.24/117.57 [35]~P14(x351)+P14(x352)+~E(x351,x352) % 117.24/117.57 % 117.24/117.57 %------------------------------------------- % 117.24/117.57 cnf(186,plain, % 117.24/117.57 (~P4(f32(a21))), % 117.24/117.57 inference(scs_inference,[],[136,144])). % 117.24/117.57 cnf(188,plain, % 117.24/117.57 (~P4(a21)), % 117.24/117.57 inference(scs_inference,[],[136,144,150])). % 117.24/117.57 cnf(190,plain, % 117.24/117.57 (~P11(x1901,a1)), % 117.24/117.57 inference(scs_inference,[],[136,63,144,150,162])). % 117.24/117.57 cnf(192,plain, % 117.24/117.57 (P18(f15(f31(x1921)),x1921)), % 117.24/117.57 inference(scs_inference,[],[136,63,126,144,150,162,181])). % 117.24/117.57 cnf(193,plain, % 117.24/117.57 (P6(f15(x1931),x1931)), % 117.24/117.57 inference(rename_variables,[],[126])). % 117.24/117.57 cnf(198,plain, % 117.24/117.57 (P9(a1)), % 117.24/117.57 inference(scs_inference,[],[112,136,63,126,128,36,144,150,162,181,179,156])). % 117.24/117.57 cnf(202,plain, % 117.24/117.57 (P11(f15(a29),a29)), % 117.24/117.57 inference(scs_inference,[],[112,136,63,126,193,128,36,40,123,129,144,150,162,181,179,156,168,177])). % 117.24/117.57 cnf(203,plain, % 117.24/117.57 (P6(f15(x2031),x2031)), % 117.24/117.57 inference(rename_variables,[],[126])). % 117.24/117.57 cnf(205,plain, % 117.24/117.57 (~E(a29,a1)), % 117.24/117.57 inference(scs_inference,[],[112,136,63,126,193,128,36,40,123,129,144,150,162,181,179,156,168,177,18])). % 117.24/117.57 cnf(206,plain, % 117.24/117.57 (~P11(x2061,f15(f31(a1)))), % 117.24/117.57 inference(scs_inference,[],[112,136,63,126,193,203,128,36,40,123,129,144,150,162,181,179,156,168,177,18,184])). % 117.24/117.57 cnf(207,plain, % 117.24/117.57 (P6(f15(x2071),x2071)), % 117.24/117.57 inference(rename_variables,[],[126])). % 117.24/117.57 cnf(213,plain, % 117.24/117.57 (P6(x2131,x2132)+~E(f15(x2132),x2131)), % 117.24/117.57 inference(scs_inference,[],[112,136,63,66,73,87,126,193,203,207,128,36,40,123,129,144,150,162,181,179,156,168,177,18,184,159,180,15])). % 117.24/117.57 cnf(219,plain, % 117.24/117.57 (~P11(x2191,a27)), % 117.24/117.57 inference(scs_inference,[],[64,162])). % 117.24/117.57 cnf(221,plain, % 117.24/117.57 (P18(f7(x2211),x2211)), % 117.24/117.57 inference(scs_inference,[],[64,127,162,181])). % 117.24/117.57 cnf(228,plain, % 117.24/117.57 (P11(f15(f32(a21)),f32(a21))), % 117.24/117.57 inference(scs_inference,[],[186,63,64,67,127,41,126,162,181,184,156,177])). % 117.24/117.57 cnf(241,plain, % 117.24/117.57 (~P11(x2411,a4)), % 117.24/117.57 inference(scs_inference,[],[65,162])). % 117.24/117.57 cnf(243,plain, % 117.24/117.57 (P18(f11(x2431),x2431)), % 117.24/117.57 inference(scs_inference,[],[65,128,162,181])). % 117.24/117.57 cnf(245,plain, % 117.24/117.57 (P11(f15(a21),a21)), % 117.24/117.57 inference(scs_inference,[],[65,188,128,126,162,181,177])). % 117.24/117.57 cnf(261,plain, % 117.24/117.57 (~P11(x2611,a8)), % 117.24/117.57 inference(scs_inference,[],[68,162])). % 117.24/117.57 cnf(263,plain, % 117.24/117.57 (P11(f15(a2),a2)), % 117.24/117.57 inference(scs_inference,[],[68,130,126,162,177])). % 117.24/117.57 cnf(276,plain, % 117.24/117.57 (~P11(x2761,f7(x2762))), % 117.24/117.57 inference(scs_inference,[],[116,162])). % 117.24/117.57 cnf(278,plain, % 117.24/117.57 (P11(f15(a23),a23)), % 117.24/117.57 inference(scs_inference,[],[116,131,126,162,177])). % 117.24/117.57 cnf(279,plain, % 117.24/117.57 (P6(f15(x2791),x2791)), % 117.24/117.57 inference(rename_variables,[],[126])). % 117.24/117.57 cnf(290,plain, % 117.24/117.57 (P18(f11(x2901),x2902)+~E(x2901,x2902)), % 117.24/117.57 inference(scs_inference,[],[116,263,64,243,190,131,126,279,162,177,18,180,168,156,31])). % 117.24/117.57 cnf(291,plain, % 117.24/117.57 (P6(f7(x2911),x2912)+~E(f31(x2911),x2912)), % 117.24/117.57 inference(scs_inference,[],[116,263,64,127,243,190,131,126,279,162,177,18,180,168,156,31,16])). % 117.24/117.57 cnf(292,plain, % 117.24/117.57 (P6(x2921,f31(x2922))+~E(f7(x2922),x2921)), % 117.24/117.57 inference(scs_inference,[],[116,263,64,127,243,190,131,126,279,162,177,18,180,168,156,31,16,15])). % 117.24/117.57 cnf(298,plain, % 117.24/117.57 (~P11(x2981,a5)), % 117.24/117.57 inference(scs_inference,[],[67,162])). % 117.24/117.57 cnf(300,plain, % 117.24/117.57 (P11(f15(a3),a3)), % 117.24/117.57 inference(scs_inference,[],[67,132,126,162,177])). % 117.24/117.57 cnf(309,plain, % 117.24/117.57 (P18(x3091,x3092)+~E(f7(x3092),x3091)), % 117.24/117.57 inference(scs_inference,[],[67,278,66,276,132,221,126,162,177,18,180,156,30])). % 117.24/117.57 cnf(310,plain, % 117.24/117.57 (P18(f7(x3101),x3102)+~E(x3101,x3102)), % 117.24/117.57 inference(scs_inference,[],[67,278,66,276,132,221,126,162,177,18,180,156,30,31])). % 117.24/117.57 cnf(311,plain, % 117.24/117.57 (P6(f11(x3111),x3112)+~E(f31(x3111),x3112)), % 117.24/117.57 inference(scs_inference,[],[67,278,66,128,276,132,221,126,162,177,18,180,156,30,31,16])). % 117.24/117.57 cnf(312,plain, % 117.24/117.57 (P6(x3121,f31(x3122))+~E(f11(x3122),x3121)), % 117.24/117.57 inference(scs_inference,[],[67,278,66,128,276,132,221,126,162,177,18,180,156,30,31,16,15])). % 117.24/117.57 cnf(319,plain, % 117.24/117.57 (~P11(x3191,f11(x3192))), % 117.24/117.57 inference(scs_inference,[],[117,162])). % 117.24/117.57 cnf(321,plain, % 117.24/117.57 (P11(f15(a10),a10)), % 117.24/117.57 inference(scs_inference,[],[117,133,126,162,177])). % 117.24/117.57 cnf(330,plain, % 117.24/117.57 (P18(x3301,x3302)+~E(f11(x3302),x3301)), % 117.24/117.57 inference(scs_inference,[],[300,117,219,133,243,126,162,177,18,180,156,30])). % 117.24/117.57 cnf(332,plain, % 117.24/117.57 (P6(x3321,a29)+~E(a8,x3321)), % 117.24/117.57 inference(scs_inference,[],[300,117,124,219,133,243,126,162,177,18,180,156,30,17,15])). % 117.24/117.57 cnf(334,plain, % 117.24/117.57 (P18(x3341,x3342)+~E(x3341,x3342)), % 117.24/117.57 inference(scs_inference,[],[300,117,124,219,133,243,125,126,162,177,18,180,156,30,17,15,16,31])). % 117.24/117.57 cnf(340,plain, % 117.24/117.57 (~P11(x3401,a6)), % 117.24/117.57 inference(scs_inference,[],[66,162])). % 117.24/117.57 cnf(342,plain, % 117.24/117.57 (P11(f15(a12),a12)), % 117.24/117.57 inference(scs_inference,[],[66,134,126,162,177])). % 117.24/117.57 cnf(353,plain, % 117.24/117.57 (P18(f15(f31(x3531)),x3532)+~E(x3531,x3532)), % 117.24/117.57 inference(scs_inference,[],[321,65,66,123,319,134,192,126,162,177,18,180,156,30,16,31])). % 117.24/117.57 cnf(361,plain, % 117.24/117.57 (P11(f15(a13),a13)), % 117.24/117.57 inference(scs_inference,[],[135,126,177])). % 117.24/117.57 cnf(368,plain, % 117.24/117.57 (P18(x3681,x3682)+~E(x3682,x3681)), % 117.24/117.57 inference(scs_inference,[],[342,241,135,125,126,177,18,180,30])). % 117.24/117.57 cnf(374,plain, % 117.24/117.57 (P11(f7(x3741),f31(x3741))), % 117.24/117.57 inference(scs_inference,[],[127,137,177])). % 117.24/117.57 cnf(389,plain, % 117.24/117.57 (P6(f15(x3891),x3892)+~E(x3891,x3892)), % 117.24/117.57 inference(scs_inference,[],[202,124,126,298,129,177,18,16])). % 117.24/117.57 cnf(397,plain, % 117.24/117.57 (P11(f11(x3971),f31(x3971))), % 117.24/117.57 inference(scs_inference,[],[128,137,177])). % 117.24/117.57 cnf(412,plain, % 117.24/117.57 (~P11(a29,a3)), % 117.24/117.57 inference(scs_inference,[],[245,123,276,129,177,18,180])). % 117.24/117.57 cnf(419,plain, % 117.24/117.57 (~P6(a29,a3)), % 117.24/117.57 inference(scs_inference,[],[412,132,177])). % 117.24/117.57 cnf(433,plain, % 117.24/117.57 (P11(x4331,f31(x4332))+~E(f7(x4332),x4331)), % 117.24/117.57 inference(scs_inference,[],[278,374,206,18,17])). % 117.24/117.57 cnf(441,plain, % 117.24/117.57 (P11(x4411,f31(x4412))+~E(f11(x4412),x4411)), % 117.24/117.57 inference(scs_inference,[],[321,397,190,18,17])). % 117.24/117.57 cnf(523,plain, % 117.24/117.57 (~E(a21,a1)), % 117.24/117.57 inference(scs_inference,[],[245,190,18])). % 117.24/117.57 cnf(595,plain, % 117.24/117.57 (P3(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[63,143,150])). % 117.24/117.57 cnf(598,plain, % 117.24/117.57 (P1(f32(a1))+~P2(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[374,595,319,18,153])). % 117.24/117.57 cnf(622,plain, % 117.24/117.57 (E(f33(a1,f28(a1)),f32(a1))), % 117.24/117.57 inference(scs_inference,[],[63,146,165])). % 117.24/117.57 cnf(625,plain, % 117.24/117.57 (E(f32(a1),f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[622,334,368,2])). % 117.24/117.57 cnf(626,plain, % 117.24/117.57 (P3(f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[622,595,334,368,2,21])). % 117.24/117.57 cnf(627,plain, % 117.24/117.57 (P18(f11(f32(a1)),f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[622,595,334,368,2,21,290])). % 117.24/117.57 cnf(628,plain, % 117.24/117.57 (P18(f7(f32(a1)),f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[622,595,334,368,2,21,290,310])). % 117.24/117.57 cnf(629,plain, % 117.24/117.57 (P6(f15(f32(a1)),f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[622,595,334,368,2,21,290,310,389])). % 117.24/117.57 cnf(630,plain, % 117.24/117.57 (~P8(f33(a1,f28(a1)))+P8(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[622,595,334,368,2,21,290,310,389,19])). % 117.24/117.57 cnf(631,plain, % 117.24/117.57 (~P4(f33(a1,f28(a1)))+P8(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[622,595,334,368,2,21,290,310,389,19,145])). % 117.24/117.57 cnf(637,plain, % 117.24/117.57 (~P15(f33(a1,f28(a1)))+P15(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[622,28,29])). % 117.24/117.57 cnf(642,plain, % 117.24/117.57 (~P12(f33(a1,f28(a1)))+P12(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[622,28,29,32,33,34,35,26])). % 117.24/117.57 cnf(643,plain, % 117.24/117.57 (~P8(f32(a1))+P8(f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[622,625,28,29,32,33,34,35,26,19])). % 117.24/117.57 cnf(669,plain, % 117.24/117.57 (~P2(f33(a1,f28(a1)))+P1(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[622,626,153,14])). % 117.24/117.57 cnf(690,plain, % 117.24/117.57 (~P4(f33(a1,f28(a1)))+P4(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[622,20])). % 117.24/117.57 cnf(691,plain, % 117.24/117.57 (P11(f15(f32(a1)),f33(a1,f28(a1)))+P4(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[622,629,20,177])). % 117.24/117.57 cnf(693,plain, % 117.24/117.57 (~E(f33(a1,f28(a1)),a1)+P4(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[622,629,190,20,177,18])). % 117.24/117.57 cnf(702,plain, % 117.24/117.57 (~P4(f33(a1,f28(a1)))+P13(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[622,374,219,18,22,146])). % 117.24/117.57 cnf(710,plain, % 117.24/117.57 (~P7(f28(a1))+P7(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[622,300,70,83,241,18,25,183])). % 117.24/117.57 cnf(718,plain, % 117.24/117.57 (~P15(f32(a1))+P15(f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[625,300,261,18,29])). % 117.24/117.57 cnf(734,plain, % 117.24/117.57 (~P4(f32(a1))+P4(f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[625,300,340,18,20])). % 117.24/117.57 cnf(742,plain, % 117.24/117.57 (~P9(f33(a1,f28(a1)))+P9(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[622,24])). % 117.24/117.57 cnf(744,plain, % 117.24/117.57 (~P7(f32(a1))+P7(f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[622,625,24,14,25])). % 117.24/117.57 cnf(773,plain, % 117.24/117.57 (P7(f16(a29))), % 117.24/117.57 inference(scs_inference,[],[205,138,147])). % 117.24/117.57 cnf(777,plain, % 117.24/117.57 (~P4(f16(a2))), % 117.24/117.57 inference(scs_inference,[],[263,158,162])). % 117.24/117.57 cnf(778,plain, % 117.24/117.57 (P11(f15(f16(a2)),f16(a2))), % 117.24/117.57 inference(scs_inference,[],[777,126,177])). % 117.24/117.57 cnf(783,plain, % 117.24/117.57 (~P11(f16(a2),f15(f16(a2)))), % 117.24/117.57 inference(scs_inference,[],[777,126,276,177,18,180])). % 117.24/117.57 cnf(811,plain, % 117.24/117.57 (~P4(f28(a1))+P7(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[710,144])). % 117.24/117.57 cnf(814,plain, % 117.24/117.57 (P7(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[63,811,149])). % 117.24/117.57 cnf(815,plain, % 117.24/117.57 (P7(f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[814,744])). % 117.24/117.57 cnf(816,plain, % 117.24/117.57 (P6(f30(a29),f31(a29))), % 117.24/117.57 inference(scs_inference,[],[205,163,138])). % 117.24/117.57 cnf(819,plain, % 117.24/117.57 (P11(f30(a29),f31(a29))), % 117.24/117.57 inference(scs_inference,[],[816,137,181,177])). % 117.24/117.57 cnf(822,plain, % 117.24/117.57 (~P11(f31(a29),f30(a29))), % 117.24/117.57 inference(scs_inference,[],[816,137,181,177,180])). % 117.24/117.57 cnf(875,plain, % 117.24/117.57 (~P11(x8751,f15(f31(a27)))), % 117.24/117.57 inference(scs_inference,[],[64,126,184])). % 117.24/117.57 cnf(878,plain, % 117.24/117.57 (P8(f32(a1))+~P8(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[630,643])). % 117.24/117.57 cnf(909,plain, % 117.24/117.57 (~P11(x9091,f15(f31(a4)))), % 117.24/117.57 inference(scs_inference,[],[65,126,184])). % 117.24/117.57 cnf(938,plain, % 117.24/117.57 (~P15(f32(a1))+P15(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[718,637])). % 117.24/117.57 cnf(942,plain, % 117.24/117.57 (~P11(x9421,f15(f31(a6)))), % 117.24/117.57 inference(scs_inference,[],[66,126,184])). % 117.24/117.57 cnf(947,plain, % 117.24/117.57 (~P4(f32(a1))+E(f33(a1,f28(a1)),a1)), % 117.24/117.57 inference(scs_inference,[],[734,138])). % 117.24/117.57 cnf(1013,plain, % 117.24/117.57 (P2(f32(a1))+~E(f33(a1,f28(a1)),a1)), % 117.24/117.57 inference(scs_inference,[],[693,141])). % 117.24/117.57 cnf(1017,plain, % 117.24/117.57 (~P11(x10171,f15(f31(a8)))), % 117.24/117.57 inference(scs_inference,[],[68,126,184])). % 117.24/117.57 cnf(1032,plain, % 117.24/117.57 (E(f33(a1,f28(a1)),a1)), % 117.24/117.57 inference(scs_inference,[],[63,947,150])). % 117.24/117.57 cnf(1033,plain, % 117.24/117.57 (P4(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[1032,693])). % 117.24/117.57 cnf(1034,plain, % 117.24/117.57 (P2(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[1032,1013])). % 117.24/117.57 cnf(1037,plain, % 117.24/117.57 (E(a1,f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[1032,368,334,2])). % 117.24/117.57 cnf(1038,plain, % 117.24/117.57 (P6(f15(a1),f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[1032,368,334,2,389])). % 117.24/117.57 cnf(1040,plain, % 117.24/117.57 (P15(f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[205,1032,103,368,334,2,389,3,29])). % 117.24/117.57 cnf(1041,plain, % 117.24/117.57 (P12(f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[205,1032,99,103,368,334,2,389,3,29,26])). % 117.24/117.57 cnf(1042,plain, % 117.24/117.57 (P2(f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[205,1032,44,99,103,368,334,2,389,3,29,26,23])). % 117.24/117.57 cnf(1043,plain, % 117.24/117.57 (P1(f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[205,1032,44,99,103,36,368,334,2,389,3,29,26,23,14])). % 117.24/117.57 cnf(1045,plain, % 117.24/117.57 (P4(f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[622,63,205,1032,44,99,103,36,368,334,2,389,3,29,26,23,14,31,20])). % 117.24/117.57 cnf(1046,plain, % 117.24/117.57 (P7(a1)), % 117.24/117.57 inference(scs_inference,[],[622,63,815,205,1032,44,99,103,36,368,334,2,389,3,29,26,23,14,31,20,25])). % 117.24/117.57 cnf(1047,plain, % 117.24/117.57 (P8(f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[622,63,815,205,70,1032,44,99,103,36,368,334,2,389,3,29,26,23,14,31,20,25,19])). % 117.24/117.57 cnf(1049,plain, % 117.24/117.57 (P9(f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[622,63,815,205,70,1032,198,44,99,103,36,368,334,2,389,3,29,26,23,14,31,20,25,19,16,24])). % 117.24/117.57 cnf(1050,plain, % 117.24/117.57 (P13(f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[622,63,815,205,70,1032,198,83,44,99,103,36,368,334,2,389,3,29,26,23,14,31,20,25,19,16,24,22])). % 117.24/117.57 cnf(1055,plain, % 117.24/117.57 (P18(f11(a1),f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[622,63,815,361,205,70,1032,198,83,44,99,103,1017,36,368,334,2,389,3,29,26,23,14,31,20,25,19,16,24,22,30,18,353,290])). % 117.24/117.57 cnf(1056,plain, % 117.24/117.57 (P18(f7(a1),f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[622,63,815,361,205,70,1032,198,83,44,99,103,1017,36,368,334,2,389,3,29,26,23,14,31,20,25,19,16,24,22,30,18,353,290,310])). % 117.24/117.57 cnf(1057,plain, % 117.24/117.57 (~P11(x10571,f33(a1,f28(a1)))), % 117.24/117.57 inference(scs_inference,[],[622,63,815,361,205,70,1032,198,83,44,99,103,1017,36,368,334,2,389,3,29,26,23,14,31,20,25,19,16,24,22,30,18,353,290,310,162])). % 117.24/117.57 cnf(1067,plain, % 117.24/117.57 (P1(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[1034,598])). % 117.24/117.57 cnf(1068,plain, % 117.24/117.57 (P8(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[1047,630])). % 117.24/117.57 cnf(1069,plain, % 117.24/117.57 (P8(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[1045,631])). % 117.24/117.57 cnf(1070,plain, % 117.24/117.57 (P15(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[1040,637])). % 117.24/117.57 cnf(1071,plain, % 117.24/117.57 (P12(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[1041,642])). % 117.24/117.57 cnf(1075,plain, % 117.24/117.57 (P1(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[1042,669])). % 117.24/117.57 cnf(1078,plain, % 117.24/117.57 (P4(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[1045,690])). % 117.24/117.57 cnf(1079,plain, % 117.24/117.57 (P4(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[1057,691])). % 117.24/117.57 cnf(1081,plain, % 117.24/117.57 (P13(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[1045,702])). % 117.24/117.57 cnf(1082,plain, % 117.24/117.57 (P9(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[1049,742])). % 117.24/117.57 cnf(1093,plain, % 117.24/117.57 (P8(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[1068,878])). % 117.24/117.57 cnf(1097,plain, % 117.24/117.57 (P15(f32(a1))), % 117.24/117.57 inference(scs_inference,[],[1070,938])). % 117.24/117.57 cnf(1099,plain, % 117.24/117.57 (~P11(x10991,f32(a1))), % 117.24/117.57 inference(scs_inference,[],[1033,162])). % 117.24/117.57 cnf(1116,plain, % 117.24/117.57 (P18(f11(a1),f32(a1))), % 117.24/117.57 inference(scs_inference,[],[622,1055,31])). % 117.24/117.57 cnf(1122,plain, % 117.24/117.57 (P18(f7(a1),f32(a1))), % 117.24/117.57 inference(scs_inference,[],[622,1056,31])). % 117.24/117.57 cnf(1195,plain, % 117.24/117.57 (P7(f11(a23))), % 117.24/117.57 inference(scs_inference,[],[69,128,179])). % 117.24/117.57 cnf(1226,plain, % 117.24/117.58 (~P4(f28(a21))), % 117.24/117.58 inference(scs_inference,[],[96,523,160,138])). % 117.24/117.58 cnf(1266,plain, % 117.24/117.58 (P7(f11(f7(x12661)))), % 117.24/117.58 inference(scs_inference,[],[118,128,179])). % 117.24/117.58 cnf(1278,plain, % 117.24/117.58 (P11(f15(f31(x12781)),f31(x12781))), % 117.24/117.58 inference(scs_inference,[],[126,137,177])). % 117.24/117.58 cnf(1350,plain, % 117.24/117.58 (P1(f28(a1))), % 117.24/117.58 inference(scs_inference,[],[63,139,149])). % 117.24/117.58 cnf(1364,plain, % 117.24/117.58 (P1(f15(a1))), % 117.24/117.58 inference(scs_inference,[],[63,126,139,173])). % 117.24/117.58 cnf(1377,plain, % 117.24/117.58 (P7(f33(a21,a1))), % 117.24/117.58 inference(scs_inference,[],[63,80,96,144,183])). % 117.24/117.58 cnf(1379,plain, % 117.24/117.58 (P7(f28(a1))), % 117.24/117.58 inference(scs_inference,[],[63,144,149])). % 117.24/117.58 cnf(1420,plain, % 117.24/117.58 (P8(f28(a1))), % 117.24/117.58 inference(scs_inference,[],[63,145,149])). % 117.24/117.58 cnf(1421,plain, % 117.24/117.58 (P12(f28(a1))+~P13(f28(a1))+~P4(f28(a1))), % 117.24/117.58 inference(scs_inference,[],[1420,159])). % 117.24/117.58 cnf(1422,plain, % 117.24/117.58 (~P4(f28(a1))+P12(f28(a1))), % 117.24/117.58 inference(scs_inference,[],[1421,146])). % 117.24/117.58 cnf(1429,plain, % 117.24/117.58 (P12(f28(a1))), % 117.24/117.58 inference(scs_inference,[],[63,1422,149])). % 117.24/117.58 cnf(1546,plain, % 117.24/117.58 (P7(f11(f32(a1)))), % 117.24/117.58 inference(scs_inference,[],[814,128,179])). % 117.24/117.58 cnf(1621,plain, % 117.24/117.58 (P6(f15(f32(a1)),a1)), % 117.24/117.58 inference(scs_inference,[],[1032,629,16])). % 117.24/117.58 cnf(1622,plain, % 117.24/117.58 (P18(f11(f32(a1)),a1)), % 117.24/117.58 inference(scs_inference,[],[1032,629,627,16,31])). % 117.24/117.58 cnf(1627,plain, % 117.24/117.58 (P18(f7(f32(a1)),a1)), % 117.24/117.58 inference(scs_inference,[],[1032,628,31])). % 117.24/117.58 cnf(1644,plain, % 117.24/117.58 (P7(f11(a1))), % 117.24/117.58 inference(scs_inference,[],[1046,128,179])). % 117.24/117.58 cnf(1751,plain, % 117.24/117.58 (P7(f11(f33(a21,a1)))), % 117.24/117.58 inference(scs_inference,[],[1377,128,179])). % 117.24/117.58 cnf(1793,plain, % 117.24/117.58 (P7(f11(f11(a1)))), % 117.24/117.58 inference(scs_inference,[],[1644,128,179])). % 117.24/117.58 cnf(1810,plain, % 117.24/117.58 (P6(a1,f31(x18101))), % 117.24/117.58 inference(scs_inference,[],[116,138,292])). % 117.24/117.58 cnf(1811,plain, % 117.24/117.58 (P18(a1,x18111)), % 117.24/117.58 inference(scs_inference,[],[1810,181])). % 117.24/117.58 cnf(1813,plain, % 117.24/117.58 (P6(f33(a1,f28(a1)),f31(x18131))), % 117.24/117.58 inference(scs_inference,[],[1037,1810,181,15])). % 117.24/117.58 cnf(1817,plain, % 117.24/117.58 (~P4(f30(a29))), % 117.24/117.58 inference(scs_inference,[],[205,138,157])). % 117.24/117.58 cnf(1818,plain, % 117.24/117.58 (~P6(f31(a29),f30(a29))), % 117.24/117.58 inference(scs_inference,[],[1817,822,177])). % 117.24/117.58 cnf(1820,plain, % 117.24/117.58 (P6(f32(a1),f31(x18201))), % 117.24/117.58 inference(scs_inference,[],[622,1813,1817,822,177,15])). % 117.24/117.58 cnf(1828,plain, % 117.24/117.58 (P6(a1,a29)), % 117.24/117.58 inference(scs_inference,[],[68,138,332])). % 117.24/117.58 cnf(1829,plain, % 117.24/117.58 (P11(a1,a29)), % 117.24/117.58 inference(scs_inference,[],[1828,129,177])). % 117.24/117.58 cnf(1831,plain, % 117.24/117.58 (P6(f33(a1,f28(a1)),a29)), % 117.24/117.58 inference(scs_inference,[],[1037,1828,129,177,15])). % 117.24/117.58 cnf(1832,plain, % 117.24/117.58 (P11(f33(a1,f28(a1)),a29)), % 117.24/117.58 inference(scs_inference,[],[1037,1828,129,177,15,17])). % 117.24/117.58 cnf(1835,plain, % 117.24/117.58 (P6(f32(a1),a29)), % 117.24/117.58 inference(scs_inference,[],[622,1831,15])). % 117.24/117.58 cnf(1836,plain, % 117.24/117.58 (P11(f32(a1),a29)), % 117.24/117.58 inference(scs_inference,[],[622,1831,1832,15,17])). % 117.24/117.58 cnf(1864,plain, % 117.24/117.58 (~P4(f16(a29))), % 117.24/117.58 inference(scs_inference,[],[205,138,158])). % 117.24/117.58 cnf(1865,plain, % 117.24/117.58 (P11(f15(f16(a29)),f16(a29))), % 117.24/117.58 inference(scs_inference,[],[1864,126,177])). % 117.24/117.58 cnf(1914,plain, % 117.24/117.58 (P11(a1,f31(x19141))), % 117.24/117.58 inference(scs_inference,[],[116,138,433])). % 117.24/117.58 cnf(1915,plain, % 117.24/117.58 (P11(f33(a1,f28(a1)),f31(x19151))), % 117.24/117.58 inference(scs_inference,[],[1037,1914,17])). % 117.24/117.58 cnf(1916,plain, % 117.24/117.58 (P6(f16(a29),f31(a29))), % 117.24/117.58 inference(scs_inference,[],[205,138,164])). % 117.24/117.58 cnf(1921,plain, % 117.24/117.58 (P11(f32(a1),f31(x19211))), % 117.24/117.58 inference(scs_inference,[],[622,1865,1915,1916,181,185,17])). % 117.24/117.58 cnf(1962,plain, % 117.24/117.58 (P7(f16(a21))), % 117.24/117.58 inference(scs_inference,[],[1226,147,149])). % 117.24/117.58 cnf(1967,plain, % 117.24/117.58 (P7(f16(a10))), % 117.24/117.58 inference(scs_inference,[],[321,147,162])). % 117.24/117.58 cnf(1968,plain, % 117.24/117.58 (P7(f16(a12))), % 117.24/117.58 inference(scs_inference,[],[342,147,162])). % 117.24/117.58 cnf(1969,plain, % 117.24/117.58 (P7(f16(a2))), % 117.24/117.58 inference(scs_inference,[],[263,147,162])). % 117.24/117.58 cnf(1970,plain, % 117.24/117.58 (P7(f16(a23))), % 117.24/117.58 inference(scs_inference,[],[278,147,162])). % 117.24/117.58 cnf(1973,plain, % 117.24/117.58 (P4(f28(f32(a1)))), % 117.24/117.58 inference(scs_inference,[],[63,149,150])). % 117.24/117.58 cnf(1974,plain, % 117.24/117.58 (~P11(x19741,f28(f32(a1)))), % 117.24/117.58 inference(scs_inference,[],[1973,162])). % 117.24/117.58 cnf(1982,plain, % 117.24/117.58 (E(f28(a1),a1)), % 117.24/117.58 inference(scs_inference,[],[63,149,138])). % 117.24/117.58 cnf(1983,plain, % 117.24/117.58 (P18(f7(f28(a1)),a1)), % 117.24/117.58 inference(scs_inference,[],[1982,310])). % 117.24/117.58 cnf(1985,plain, % 117.24/117.58 (P18(f11(f28(a1)),a1)), % 117.24/117.58 inference(scs_inference,[],[1982,310,389,290])). % 117.24/117.58 cnf(1986,plain, % 117.24/117.58 (E(a1,f28(a1))), % 117.24/117.58 inference(scs_inference,[],[1982,310,389,290,2])). % 117.24/117.58 cnf(1987,plain, % 117.24/117.58 (P18(f28(a1),a1)), % 117.24/117.58 inference(scs_inference,[],[1982,310,389,290,2,334])). % 117.24/117.58 cnf(1989,plain, % 117.24/117.58 (P15(f28(a1))), % 117.24/117.58 inference(scs_inference,[],[205,1982,103,310,389,290,2,334,3,29])). % 117.24/117.58 cnf(1990,plain, % 117.24/117.58 (P4(f28(a1))), % 117.24/117.58 inference(scs_inference,[],[63,205,1982,103,310,389,290,2,334,3,29,20])). % 117.24/117.58 cnf(1992,plain, % 117.24/117.58 (P6(f15(f28(a1)),f33(a1,f28(a1)))), % 117.24/117.58 inference(scs_inference,[],[63,1037,205,1982,198,103,310,389,290,2,334,3,29,20,24,16])). % 117.24/117.58 cnf(1997,plain, % 117.24/117.58 (~P11(x19971,f28(a1))), % 117.24/117.58 inference(scs_inference,[],[63,1037,342,205,1982,198,1974,103,310,389,290,2,334,3,29,20,24,16,31,18,353,162])). % 117.24/117.58 cnf(2009,plain, % 117.24/117.58 (P6(f15(a1),f28(a1))), % 117.24/117.58 inference(scs_inference,[],[1986,389])). % 117.24/117.58 cnf(2010,plain, % 117.24/117.58 (P18(f11(a1),f28(a1))), % 117.24/117.58 inference(scs_inference,[],[1986,389,290])). % 117.24/117.58 cnf(2011,plain, % 117.24/117.58 (P18(f7(a1),f28(a1))), % 117.24/117.58 inference(scs_inference,[],[1986,389,290,310])). % 117.24/117.58 cnf(2012,plain, % 117.24/117.58 (P6(f15(f28(a1)),f32(a1))), % 117.24/117.58 inference(scs_inference,[],[622,1992,1986,389,290,310,16])). % 117.24/117.58 cnf(2013,plain, % 117.24/117.58 (P18(f28(a1),f33(a1,f28(a1)))), % 117.24/117.58 inference(scs_inference,[],[622,1037,1987,1992,1986,389,290,310,16,31])). % 117.24/117.58 cnf(2040,plain, % 117.24/117.58 (P18(f28(a1),f32(a1))), % 117.24/117.58 inference(scs_inference,[],[622,2013,31])). % 117.24/117.58 cnf(2090,plain, % 117.24/117.58 (~E(f28(a1),a3)+~E(f15(a1),a29)), % 117.24/117.58 inference(scs_inference,[],[361,419,2009,1997,18,15,16])). % 117.24/117.58 cnf(2113,plain, % 117.24/117.58 (P18(x21131,f28(a1))+~E(f11(a1),x21131)), % 117.24/117.58 inference(scs_inference,[],[245,2010,1997,18,30])). % 117.24/117.58 cnf(2117,plain, % 117.24/117.58 (P18(x21171,f28(a1))+~E(f7(a1),x21171)), % 117.24/117.58 inference(scs_inference,[],[228,2011,1974,18,30])). % 117.24/117.58 cnf(2172,plain, % 117.24/117.58 (~E(a29,f15(a1))+~E(f28(a1),a3)), % 117.24/117.58 inference(scs_inference,[],[2090,2])). % 117.24/117.58 cnf(2177,plain, % 117.24/117.58 (~E(x21771,f15(a1))+~E(a29,x21771)+~E(f28(a1),a3)), % 117.24/117.58 inference(scs_inference,[],[2172,3])). % 117.24/117.58 cnf(2275,plain, % 117.24/117.58 (~P4(f30(a21))), % 117.24/117.58 inference(scs_inference,[],[1226,149,157])). % 117.24/117.58 cnf(2329,plain, % 117.24/117.58 (P4(f32(f28(a1)))), % 117.24/117.58 inference(scs_inference,[],[63,149,150])). % 117.24/117.58 cnf(2332,plain, % 117.24/117.58 (P9(f32(f28(a1)))+~P1(f32(f28(a1)))), % 117.24/117.58 inference(scs_inference,[],[2329,162,156])). % 117.24/117.58 cnf(2338,plain, % 117.24/117.58 (~P4(f16(a21))), % 117.24/117.58 inference(scs_inference,[],[1226,149,158])). % 117.24/117.58 cnf(2339,plain, % 117.24/117.58 (P11(f15(f16(a21)),f16(a21))), % 117.24/117.58 inference(scs_inference,[],[2338,126,177])). % 117.24/117.58 cnf(2422,plain, % 117.24/117.58 (P13(f32(f28(a1)))), % 117.24/117.58 inference(scs_inference,[],[63,149,152])). % 117.24/117.58 cnf(2466,plain, % 117.24/117.58 (P6(f16(a21),f31(a21))), % 117.24/117.58 inference(scs_inference,[],[1226,149,164])). % 117.24/117.58 cnf(2469,plain, % 117.24/117.58 (P6(f15(f16(a21)),a21)), % 117.24/117.58 inference(scs_inference,[],[2339,2466,181,185])). % 117.24/117.58 cnf(2517,plain, % 117.24/117.58 (~E(a1,a21)), % 117.24/117.58 inference(scs_inference,[],[1226,63,149,20])). % 117.24/117.58 cnf(2518,plain, % 117.24/117.58 (E(f32(a1),a1)), % 117.24/117.58 inference(scs_inference,[],[63,150,138])). % 117.24/117.58 cnf(2519,plain, % 117.24/117.58 (E(a1,f32(a1))), % 117.24/117.58 inference(scs_inference,[],[2518,2])). % 117.24/117.58 cnf(2533,plain, % 117.24/117.58 (P7(f33(f28(a1),f28(a21)))), % 117.24/117.58 inference(scs_inference,[],[63,112,1420,151,183])). % 117.24/117.58 cnf(2535,plain, % 117.24/117.58 (P7(f33(f32(a1),f28(a21)))), % 117.24/117.58 inference(scs_inference,[],[63,112,1069,152,183])). % 117.24/117.58 cnf(2537,plain, % 117.24/117.58 (~P4(f30(a10))), % 117.24/117.58 inference(scs_inference,[],[321,157,162])). % 117.24/117.58 cnf(2538,plain, % 117.24/117.58 (P11(f15(f30(a10)),f30(a10))), % 117.24/117.58 inference(scs_inference,[],[2537,126,177])). % 117.24/117.58 cnf(2566,plain, % 117.24/117.58 (~E(f30(a10),f32(a1))), % 117.24/117.58 inference(scs_inference,[],[2538,1099,18])). % 117.24/117.58 cnf(2568,plain, % 117.24/117.58 (~E(f30(a10),f28(a1))), % 117.24/117.58 inference(scs_inference,[],[2538,1997,18])). % 117.24/117.58 cnf(2572,plain, % 117.24/117.58 (~E(f30(a10),a27)), % 117.24/117.58 inference(scs_inference,[],[2538,219,18])). % 117.24/117.58 cnf(2575,plain, % 117.24/117.58 (~E(f16(a21),a4)), % 117.24/117.58 inference(scs_inference,[],[2339,241,18])). % 117.24/117.58 cnf(2577,plain, % 117.24/117.58 (~E(f30(a10),a8)), % 117.24/117.58 inference(scs_inference,[],[2538,261,18])). % 117.24/117.58 cnf(2579,plain, % 117.24/117.58 (~E(f30(a10),a5)), % 117.24/117.58 inference(scs_inference,[],[2538,298,18])). % 117.24/117.58 cnf(2581,plain, % 117.24/117.58 (~E(f30(a10),a6)), % 117.24/117.58 inference(scs_inference,[],[2538,340,18])). % 117.24/117.58 cnf(2583,plain, % 117.24/117.58 (~E(f30(a10),f7(x25831))), % 117.24/117.58 inference(scs_inference,[],[2538,276,18])). % 117.24/117.58 cnf(2585,plain, % 117.24/117.58 (~E(f30(a10),f11(x25851))), % 117.24/117.58 inference(scs_inference,[],[2538,319,18])). % 117.24/117.58 cnf(2598,plain, % 117.24/117.58 (~P4(f30(a12))), % 117.24/117.58 inference(scs_inference,[],[342,157,162])). % 117.24/117.58 cnf(2599,plain, % 117.24/117.58 (P11(f15(f30(a12)),f30(a12))), % 117.24/117.58 inference(scs_inference,[],[2598,126,177])). % 117.24/117.58 cnf(2627,plain, % 117.24/117.58 (~E(f30(a12),f32(a1))), % 117.24/117.58 inference(scs_inference,[],[2599,1099,18])). % 117.24/117.58 cnf(2629,plain, % 117.24/117.58 (~E(f30(a12),f28(a1))), % 117.24/117.58 inference(scs_inference,[],[2599,1997,18])). % 117.24/117.58 cnf(2633,plain, % 117.24/117.58 (~E(f30(a12),a27)), % 117.24/117.58 inference(scs_inference,[],[2599,219,18])). % 117.24/117.58 cnf(2635,plain, % 117.24/117.58 (~E(f30(a10),a4)), % 117.24/117.58 inference(scs_inference,[],[2538,241,18])). % 117.24/117.58 cnf(2637,plain, % 117.24/117.58 (~E(f30(a12),a8)), % 117.24/117.58 inference(scs_inference,[],[2599,261,18])). % 117.24/117.58 cnf(2639,plain, % 117.24/117.58 (~E(f30(a12),a5)), % 117.24/117.58 inference(scs_inference,[],[2599,298,18])). % 117.24/117.58 cnf(2641,plain, % 117.24/117.58 (~E(f30(a12),a6)), % 117.24/117.58 inference(scs_inference,[],[2599,340,18])). % 117.24/117.58 cnf(2644,plain, % 117.24/117.58 (~E(f30(a12),f7(x26441))), % 117.24/117.58 inference(scs_inference,[],[2599,276,18])). % 117.24/117.58 cnf(2646,plain, % 117.24/117.58 (~E(f30(a12),f11(x26461))), % 117.24/117.58 inference(scs_inference,[],[2599,319,18])). % 117.24/117.58 cnf(2657,plain, % 117.24/117.58 (~P4(f30(a2))), % 117.24/117.58 inference(scs_inference,[],[263,157,162])). % 117.24/117.58 cnf(2658,plain, % 117.24/117.58 (P11(f15(f30(a2)),f30(a2))), % 117.24/117.58 inference(scs_inference,[],[2657,126,177])). % 117.24/117.58 cnf(2663,plain, % 117.24/117.58 (~P11(f30(a2),f15(f30(a2)))), % 117.24/117.58 inference(scs_inference,[],[2657,126,875,177,18,180])). % 117.24/117.58 cnf(2690,plain, % 117.24/117.58 (~P4(f30(f30(a10)))), % 117.24/117.58 inference(scs_inference,[],[2537,2329,67,141,143,147,151,152,157])). % 117.24/117.58 cnf(2692,plain, % 117.24/117.58 (~P4(f16(f30(a10)))), % 117.24/117.58 inference(scs_inference,[],[2537,2329,67,141,143,147,151,152,157,158])). % 117.24/117.58 cnf(2701,plain, % 117.24/117.58 (E(f7(a1),f7(f32(a1)))), % 117.24/117.58 inference(scs_inference,[],[1818,2040,2519,2537,2329,67,141,143,147,151,152,157,158,178,213,163,164,5])). % 117.24/117.58 cnf(2702,plain, % 117.24/117.58 (E(f31(a1),f31(f32(a1)))), % 117.24/117.58 inference(scs_inference,[],[1818,2040,2519,2537,2329,67,141,143,147,151,152,157,158,178,213,163,164,5,7])). % 117.24/117.58 cnf(2704,plain, % 117.24/117.58 (E(f11(a1),f11(f32(a1)))), % 117.24/117.58 inference(scs_inference,[],[1818,2040,2519,2537,2329,67,141,143,147,151,152,157,158,178,213,163,164,5,7,8,9])). % 117.24/117.58 cnf(2709,plain, % 117.24/117.58 (E(f33(a1,x27091),f33(f32(a1),x27091))), % 117.24/117.58 inference(scs_inference,[],[86,1818,2040,2519,2537,2329,67,141,143,147,151,152,157,158,178,213,163,164,5,7,8,9,10,13,165,11])). % 117.24/117.58 cnf(2710,plain, % 117.24/117.58 (E(f33(x27101,a1),f33(x27101,f32(a1)))), % 117.24/117.58 inference(scs_inference,[],[86,1818,2040,2519,2537,2329,67,141,143,147,151,152,157,158,178,213,163,164,5,7,8,9,10,13,165,11,12])). % 117.24/117.58 cnf(2711,plain, % 117.24/117.58 (E(f28(a1),f28(f32(a1)))), % 117.24/117.58 inference(scs_inference,[],[86,1818,2040,2519,2537,2329,67,141,143,147,151,152,157,158,178,213,163,164,5,7,8,9,10,13,165,11,12,4])). % 117.24/117.58 cnf(2712,plain, % 117.24/117.58 (P4(f28(f28(a1)))), % 117.24/117.58 inference(scs_inference,[],[86,1818,2040,1990,2519,2537,2329,67,141,143,147,151,152,157,158,178,213,163,164,5,7,8,9,10,13,165,11,12,4,149])). % 117.24/117.58 cnf(2714,plain, % 117.24/117.58 (E(f32(a1),f32(f32(a1)))), % 117.24/117.58 inference(scs_inference,[],[86,1818,2040,1990,2519,2537,2329,67,141,143,147,151,152,157,158,178,213,163,164,5,7,8,9,10,13,165,11,12,4,149,6])). % 117.24/117.58 cnf(2721,plain, % 117.24/117.58 (P13(a8)), % 117.24/117.58 inference(scs_inference,[],[86,1818,2040,1990,2519,2537,2329,67,68,141,143,147,151,152,157,158,178,213,163,164,5,7,8,9,10,13,165,11,12,4,149,6,138,144,145,146])). % 117.24/117.58 cnf(2723,plain, % 117.24/117.58 (P4(f32(f32(a1)))), % 117.24/117.58 inference(scs_inference,[],[86,1818,2040,1990,2519,2537,1033,2329,67,68,141,143,147,151,152,157,158,178,213,163,164,5,7,8,9,10,13,165,11,12,4,149,6,138,144,145,146,150])). % 117.24/117.58 cnf(2727,plain, % 117.24/117.58 (~E(f32(a1),f30(a10))), % 117.24/117.58 inference(scs_inference,[],[86,2566,1818,2040,1990,2519,2537,1033,2329,67,68,141,143,147,151,152,157,158,178,213,163,164,5,7,8,9,10,13,165,11,12,4,149,6,138,144,145,146,150,139,2])). % 117.24/117.58 cnf(2732,plain, % 117.24/117.58 (~P4(f28(a10))), % 117.24/117.58 inference(scs_inference,[],[86,90,2566,1067,1818,2040,1990,2519,2537,133,1033,2012,2329,67,68,141,143,147,151,152,157,158,178,213,163,164,5,7,8,9,10,13,165,11,12,4,149,6,138,144,145,146,150,139,2,174,175,160])). % 117.24/117.58 cnf(2734,plain, % 117.24/117.58 (~P4(f32(a10))), % 117.24/117.58 inference(scs_inference,[],[86,90,2566,1067,1818,2040,1990,2519,2537,133,1033,2012,2329,67,68,141,143,147,151,152,157,158,178,213,163,164,5,7,8,9,10,13,165,11,12,4,149,6,138,144,145,146,150,139,2,174,175,160,161])). % 117.24/117.58 cnf(2738,plain, % 117.24/117.58 (~E(f32(a1),a21)), % 117.24/117.58 inference(scs_inference,[],[2517,86,90,2566,1067,1818,2040,1990,2519,2537,133,1033,2012,2329,67,68,141,143,147,151,152,157,158,178,213,163,164,5,7,8,9,10,13,165,11,12,4,149,6,138,144,145,146,150,139,2,174,175,160,161,173,3])). % 117.24/117.58 cnf(2739,plain, % 117.24/117.58 (~E(f16(a21),f32(a21))), % 117.24/117.58 inference(scs_inference,[],[2517,86,90,2566,1067,1962,1818,2040,1990,2519,2537,133,1033,2012,2329,67,68,136,141,143,147,151,152,157,158,178,213,163,164,5,7,8,9,10,13,165,11,12,4,149,6,138,144,145,146,150,139,2,174,175,160,161,173,3,25])). % 117.24/117.58 cnf(2740,plain, % 117.24/117.58 (~E(f28(a1),f30(a10))), % 117.24/117.58 inference(scs_inference,[],[2517,86,90,2566,1067,1962,1818,2040,1990,2519,2537,133,1033,2012,2329,67,68,136,141,143,147,151,152,157,158,178,213,163,164,5,7,8,9,10,13,165,11,12,4,149,6,138,144,145,146,150,139,2,174,175,160,161,173,3,25,20])). % 117.24/117.58 cnf(2741,plain, % 117.24/117.58 (P11(f15(f16(a21)),a21)), % 117.24/117.58 inference(scs_inference,[],[2517,86,90,2566,1067,1962,1818,2040,1990,2519,2537,133,188,1033,2012,2329,2469,67,68,136,141,143,147,151,152,157,158,178,213,163,164,5,7,8,9,10,13,165,11,12,4,149,6,138,144,145,146,150,139,2,174,175,160,161,173,3,25,20,177])). % 117.24/117.58 cnf(2743,plain, % 117.24/117.58 (~P6(a29,f31(f28(a1)))), % 117.24/117.58 inference(scs_inference,[],[2517,86,90,2566,1067,1962,1818,2040,1836,1990,2519,2537,133,188,1033,2012,2329,2469,67,68,136,141,143,147,151,152,157,158,178,213,163,164,5,7,8,9,10,13,165,11,12,4,149,6,138,144,145,146,150,139,2,174,175,160,161,173,3,25,20,177,184])). % 117.24/117.58 cnf(2745,plain, % 117.24/117.58 (~P6(f32(a21),f31(f16(a21)))), % 117.24/117.58 inference(scs_inference,[],[2517,86,90,2566,1067,1962,1818,2040,1836,1990,2519,2537,133,188,1033,2012,2329,2469,67,68,136,141,143,147,151,152,157,158,178,213,163,164,5,7,8,9,10,13,165,11,12,4,149,6,138,144,145,146,150,139,2,174,175,160,161,173,3,25,20,177,184,179])). % 117.24/117.58 cnf(2747,plain, % 117.24/117.58 (~E(f32(a1),a29)), % 117.24/117.58 inference(scs_inference,[],[2517,86,90,2566,1067,1962,1818,2040,1836,1990,2519,2537,133,188,1033,2012,1820,2329,2469,67,68,136,141,143,147,151,152,157,158,178,213,163,164,5,7,8,9,10,13,165,11,12,4,149,6,138,144,145,146,150,139,2,174,175,160,161,173,3,25,20,177,184,179,15])). % 117.24/117.58 cnf(2763,plain, % 117.24/117.58 (P18(f28(a1),x27631)), % 117.24/117.58 inference(scs_inference,[],[80,2517,86,90,2566,1067,1962,2422,1818,2040,1836,1990,1811,2519,1621,108,2537,133,188,1033,2012,1820,79,2329,2469,67,68,95,1986,136,96,141,143,147,151,152,157,158,178,213,163,164,5,7,8,9,10,13,165,11,12,4,149,6,138,144,145,146,150,139,2,174,175,160,161,173,3,25,20,177,184,179,15,183,172,159,292,312,2332,180,22,16,31,30])). % 117.24/117.58 cnf(2769,plain, % 117.24/117.58 (P13(f32(f7(x27691)))), % 117.24/117.58 inference(scs_inference,[],[2732,116,147,152])). % 117.24/117.58 cnf(2771,plain, % 117.24/117.58 (P13(f28(f7(x27711)))), % 117.24/117.58 inference(scs_inference,[],[2732,116,147,152,151])). % 117.24/117.58 cnf(2773,plain, % 117.24/117.58 (P6(f30(a2),f31(a2))), % 117.24/117.58 inference(scs_inference,[],[2732,130,116,147,152,151,163])). % 117.24/117.58 cnf(2775,plain, % 117.24/117.58 (P4(f28(f7(x27751)))), % 117.24/117.58 inference(scs_inference,[],[2732,130,116,147,152,151,163,149])). % 117.24/117.58 cnf(2777,plain, % 117.24/117.58 (~P4(f30(f28(a10)))), % 117.24/117.58 inference(scs_inference,[],[2732,130,116,147,152,151,163,149,157])). % 117.24/117.58 cnf(2783,plain, % 117.24/117.58 (~P4(f16(f28(a10)))), % 117.24/117.58 inference(scs_inference,[],[88,2732,2712,130,116,147,152,151,163,149,157,165,143,158])). % 117.24/117.58 cnf(2787,plain, % 117.24/117.58 (P6(f16(a2),f31(a2))), % 117.24/117.58 inference(scs_inference,[],[88,2732,2712,130,116,147,152,151,163,149,157,165,143,158,141,164])). % 117.24/117.58 cnf(2792,plain, % 117.24/117.58 (P6(f28(a1),f31(x27921))), % 117.24/117.58 inference(scs_inference,[],[88,2763,2732,2712,2745,130,2518,116,147,152,151,163,149,157,165,143,158,141,164,13,292,8,178])). % 117.24/117.58 cnf(2804,plain, % 117.24/117.58 (E(f31(f32(a1)),f31(a1))), % 117.24/117.58 inference(scs_inference,[],[88,2763,2732,2712,2745,130,2518,116,117,147,152,151,163,149,157,165,143,158,141,164,13,292,8,178,138,6,146,9,312,145,10,7])). % 117.24/117.58 cnf(2805,plain, % 117.24/117.58 (E(f33(f32(a1),x28051),f33(a1,x28051))), % 117.24/117.58 inference(scs_inference,[],[88,2763,2732,2712,2745,130,2518,116,117,147,152,151,163,149,157,165,143,158,141,164,13,292,8,178,138,6,146,9,312,145,10,7,11])). % 117.24/117.58 cnf(2810,plain, % 117.24/117.58 (E(f33(x28101,f32(a1)),f33(x28101,a1))), % 117.24/117.58 inference(scs_inference,[],[88,2763,2732,2712,2745,130,2518,116,117,147,152,151,163,149,157,165,143,158,141,164,13,292,8,178,138,6,146,9,312,145,10,7,11,4,5,144,12])). % 117.24/117.58 cnf(2813,plain, % 117.24/117.58 (P4(f32(f7(x28131)))), % 117.24/117.58 inference(scs_inference,[],[88,2763,2732,2712,2745,130,2518,116,117,147,152,151,163,149,157,165,143,158,141,164,13,292,8,178,138,6,146,9,312,145,10,7,11,4,5,144,12,139,150])). % 117.24/117.58 cnf(2817,plain, % 117.24/117.58 (P6(f15(x28171),x28171)), % 117.24/117.58 inference(rename_variables,[],[126])). % 117.24/117.58 cnf(2820,plain, % 117.24/117.58 (P6(f15(x28201),x28201)), % 117.24/117.58 inference(rename_variables,[],[126])). % 117.24/117.58 cnf(2823,plain, % 117.24/117.58 (P6(f15(x28231),x28231)), % 117.24/117.58 inference(rename_variables,[],[126])). % 117.24/117.58 cnf(2825,plain, % 117.24/117.58 (E(f33(a1,a1),f33(f32(a1),f32(a1)))), % 117.24/117.58 inference(scs_inference,[],[88,2572,2763,2732,2709,2710,2712,2745,1364,130,2518,116,117,126,2817,2820,147,152,151,163,149,157,165,143,158,141,164,13,292,8,178,138,6,146,9,312,145,10,7,11,4,5,144,12,139,150,2,174,175,173,3])). % 117.24/117.58 cnf(2826,plain, % 117.24/117.58 (E(f33(a1,x28261),f33(f32(a1),x28261))), % 117.24/117.58 inference(rename_variables,[],[2709])). % 117.24/117.58 cnf(2832,plain, % 117.24/117.58 (~E(f28(f28(a1)),f28(a10))), % 117.24/117.58 inference(scs_inference,[],[88,2572,2763,1070,1967,2732,2709,2710,2712,2711,2714,2745,1364,1350,1093,130,2518,116,117,136,126,2817,2820,147,152,151,163,149,157,165,143,158,141,164,13,292,8,178,138,6,146,9,312,145,10,7,11,4,5,144,12,139,150,2,174,175,173,3,29,14,19,25,20])). % 117.24/117.58 cnf(2833,plain, % 117.24/117.58 (P4(f15(f31(a1)))), % 117.24/117.58 inference(scs_inference,[],[88,2572,2763,1070,1967,2732,2709,2710,2712,2711,2714,2745,1364,1350,1093,130,2518,116,117,206,136,126,2817,2820,2823,147,152,151,163,149,157,165,143,158,141,164,13,292,8,178,138,6,146,9,312,145,10,7,11,4,5,144,12,139,150,2,174,175,173,3,29,14,19,25,20,177])). % 117.24/117.58 cnf(2837,plain, % 117.24/117.58 (~P6(f32(a21),f31(f16(a10)))), % 117.24/117.58 inference(scs_inference,[],[88,2572,2763,1070,1967,2732,2709,2710,2712,2711,2714,2745,1364,1350,1093,130,2518,116,117,206,136,126,2817,2820,2823,147,152,151,163,149,157,165,143,158,141,164,13,292,8,178,138,6,146,9,312,145,10,7,11,4,5,144,12,139,150,2,174,175,173,3,29,14,19,25,20,177,179])). % 117.24/117.58 cnf(2839,plain, % 117.24/117.58 (P6(f33(f32(a1),f28(a1)),a29)), % 117.24/117.58 inference(scs_inference,[],[88,2572,2763,1070,1967,2732,2709,2826,2710,2712,2711,2714,2745,1364,1350,1093,130,1831,2518,116,117,206,136,126,2817,2820,2823,147,152,151,163,149,157,165,143,158,141,164,13,292,8,178,138,6,146,9,312,145,10,7,11,4,5,144,12,139,150,2,174,175,173,3,29,14,19,25,20,177,179,15])). % 117.24/117.58 cnf(2865,plain, % 117.24/117.58 (P6(f30(a23),f31(a23))), % 117.24/117.58 inference(scs_inference,[],[131,68,151,163])). % 117.24/117.58 cnf(2867,plain, % 117.24/117.58 (P4(f28(a8))), % 117.24/117.58 inference(scs_inference,[],[131,68,151,163,149])). % 117.24/117.58 cnf(2869,plain, % 117.24/117.58 (P13(f32(a8))), % 117.24/117.58 inference(scs_inference,[],[131,68,151,163,149,152])). % 117.24/117.58 cnf(2871,plain, % 117.24/117.58 (~P4(f16(f32(a10)))), % 117.24/117.58 inference(scs_inference,[],[2734,131,68,151,163,149,152,158])). % 117.24/117.58 cnf(2877,plain, % 117.24/117.58 (~P4(f30(f32(a10)))), % 117.24/117.58 inference(scs_inference,[],[2734,2775,131,68,151,163,149,152,158,147,141,157])). % 117.24/117.58 cnf(2881,plain, % 117.24/117.58 (P6(f16(a23),f31(a23))), % 117.24/117.58 inference(scs_inference,[],[91,2734,2775,131,68,151,163,149,152,158,147,141,157,165,164])). % 117.24/117.58 cnf(2887,plain, % 117.24/117.58 (P6(f7(f32(a1)),f31(a1))), % 117.24/117.58 inference(scs_inference,[],[91,2734,2775,2833,1627,131,68,151,163,149,152,158,147,141,157,165,164,143,146,178])). % 117.24/117.58 cnf(2891,plain, % 117.24/117.58 (P7(f28(f7(x28911)))), % 117.24/117.58 inference(scs_inference,[],[91,2734,2775,2833,1627,131,68,151,163,149,152,158,147,141,157,165,164,143,146,178,139,144])). % 117.24/117.58 cnf(2895,plain, % 117.24/117.58 (E(f32(a1),f32(f28(a1)))), % 117.24/117.58 inference(scs_inference,[],[91,2734,2775,2833,1627,131,68,1986,151,163,149,152,158,147,141,157,165,164,143,146,178,139,144,138,6])). % 117.24/117.58 cnf(2897,plain, % 117.24/117.58 (P4(f32(a8))), % 117.24/117.58 inference(scs_inference,[],[91,2734,2775,2833,1627,131,68,1986,151,163,149,152,158,147,141,157,165,164,143,146,178,139,144,138,6,8,150])). % 117.24/117.58 cnf(2900,plain, % 117.24/117.58 (E(f15(a1),f15(f28(a1)))), % 117.24/117.58 inference(scs_inference,[],[91,2734,2775,2833,1627,131,68,1986,151,163,149,152,158,147,141,157,165,164,143,146,178,139,144,138,6,8,150,10,13])). % 117.24/117.58 cnf(2901,plain, % 117.24/117.58 (P8(f28(f7(x29011)))), % 117.24/117.58 inference(scs_inference,[],[91,2734,2775,2833,1627,131,68,1986,151,163,149,152,158,147,141,157,165,164,143,146,178,139,144,138,6,8,150,10,13,145])). % 117.24/117.58 cnf(2905,plain, % 117.24/117.58 (E(f31(a1),f31(f28(a1)))), % 117.24/117.58 inference(scs_inference,[],[91,2734,2775,2833,2837,1627,131,68,1986,151,163,149,152,158,147,141,157,165,164,143,146,178,139,144,138,6,8,150,10,13,145,292,5,7])). % 117.24/117.58 cnf(2906,plain, % 117.24/117.58 (E(f11(a1),f11(f28(a1)))), % 117.24/117.58 inference(scs_inference,[],[91,2734,2775,2833,2837,1627,131,68,1986,151,163,149,152,158,147,141,157,165,164,143,146,178,139,144,138,6,8,150,10,13,145,292,5,7,9])). % 117.24/117.58 cnf(2908,plain, % 117.24/117.58 (E(f33(x29081,a1),f33(x29081,f28(a1)))), % 117.24/117.58 inference(scs_inference,[],[91,2734,2775,2833,2837,1627,131,68,1986,151,163,149,152,158,147,141,157,165,164,143,146,178,139,144,138,6,8,150,10,13,145,292,5,7,9,312,12])). % 117.24/117.58 cnf(2909,plain, % 117.24/117.58 (E(f33(a1,x29091),f33(f28(a1),x29091))), % 117.24/117.58 inference(scs_inference,[],[91,2734,2775,2833,2837,1627,131,68,1986,151,163,149,152,158,147,141,157,165,164,143,146,178,139,144,138,6,8,150,10,13,145,292,5,7,9,312,12,11])). % 117.24/117.58 cnf(2910,plain, % 117.24/117.58 (E(f28(a1),f28(f28(a1)))), % 117.24/117.58 inference(scs_inference,[],[91,2734,2775,2833,2837,1627,131,68,1986,151,163,149,152,158,147,141,157,165,164,143,146,178,139,144,138,6,8,150,10,13,145,292,5,7,9,312,12,11,4])). % 117.24/117.58 cnf(2912,plain, % 117.24/117.58 (P3(f33(f32(a1),f28(a1)))), % 117.24/117.58 inference(scs_inference,[],[91,2575,2734,2775,2833,2837,1627,2709,131,626,68,1986,151,163,149,152,158,147,141,157,165,164,143,146,178,139,144,138,6,8,150,10,13,145,292,5,7,9,312,12,11,4,2,21])). % 117.24/117.58 cnf(2913,plain, % 117.24/117.58 (E(f33(a1,x29131),f33(f32(a1),x29131))), % 117.24/117.58 inference(rename_variables,[],[2709])). % 117.24/117.58 cnf(2914,plain, % 117.24/117.58 (E(f33(f32(a1),f32(a1)),f33(a1,a1))), % 117.24/117.58 inference(scs_inference,[],[91,2575,2734,2805,2810,2775,2833,2837,1627,2709,131,626,68,1986,151,163,149,152,158,147,141,157,165,164,143,146,178,139,144,138,6,8,150,10,13,145,292,5,7,9,312,12,11,4,2,21,3])). % 117.24/117.58 cnf(2917,plain, % 117.24/117.58 (~E(f16(a12),f32(a21))), % 117.24/117.58 inference(scs_inference,[],[91,2575,1968,2734,2805,2810,2775,2833,2837,1627,2709,131,626,68,1986,136,151,163,149,152,158,147,141,157,165,164,143,146,178,139,144,138,6,8,150,10,13,145,292,5,7,9,312,12,11,4,2,21,3,25])). % 117.24/117.58 cnf(2919,plain, % 117.24/117.58 (P13(f33(f32(a1),f28(a1)))), % 117.24/117.58 inference(scs_inference,[],[91,2575,1968,2734,2805,2810,2775,2833,2837,1627,2709,2913,1050,131,626,68,1986,136,151,163,149,152,158,147,141,157,165,164,143,146,178,139,144,138,6,8,150,10,13,145,292,5,7,9,312,12,11,4,2,21,3,25,20,22])). % 117.24/117.58 cnf(2921,plain, % 117.24/117.58 (P11(f28(a1),f31(x29211))), % 117.24/117.58 inference(scs_inference,[],[91,2575,2792,1968,2734,2805,2810,2775,2833,2837,1627,2709,2913,1050,131,626,68,137,1986,136,151,163,149,152,158,147,141,157,165,164,143,146,178,139,144,138,6,8,150,10,13,145,292,5,7,9,312,12,11,4,2,21,3,25,20,22,177])). % 117.24/117.58 cnf(2922,plain, % 117.24/117.58 (P6(f28(a1),f31(x29221))), % 117.24/117.58 inference(rename_variables,[],[2792])). % 117.24/117.58 cnf(2924,plain, % 117.24/117.58 (~P6(f32(a21),f31(f16(a12)))), % 117.24/117.58 inference(scs_inference,[],[91,2575,2792,1968,2734,2805,2810,2775,2833,2837,1627,2709,2913,1050,131,626,68,137,1986,136,151,163,149,152,158,147,141,157,165,164,143,146,178,139,144,138,6,8,150,10,13,145,292,5,7,9,312,12,11,4,2,21,3,25,20,22,177,179])). % 117.24/117.58 cnf(2926,plain, % 117.24/117.58 (~E(f28(a1),f32(a21))), % 117.24/117.58 inference(scs_inference,[],[91,2575,2792,2922,1968,2734,2805,2810,2775,2833,2837,1627,2709,2913,1050,131,626,68,137,1986,136,151,163,149,152,158,147,141,157,165,164,143,146,178,139,144,138,6,8,150,10,13,145,292,5,7,9,312,12,11,4,2,21,3,25,20,22,177,179,15])). % 117.24/117.58 cnf(2928,plain, % 117.24/117.58 (~P6(a29,f31(a1))), % 117.24/117.58 inference(scs_inference,[],[91,2575,2792,2922,1968,2734,2805,2810,2775,2833,2837,2743,1627,2709,2913,1050,131,626,68,137,1986,136,151,163,149,152,158,147,141,157,165,164,143,146,178,139,144,138,6,8,150,10,13,145,292,5,7,9,312,12,11,4,2,21,3,25,20,22,177,179,15,16])). % 117.24/117.58 cnf(2946,plain, % 117.24/117.58 (P4(f28(f28(a8)))), % 117.24/117.58 inference(scs_inference,[],[2867,149])). % 117.24/117.58 cnf(2948,plain, % 117.24/117.58 (~P4(f16(f30(a12)))), % 117.24/117.58 inference(scs_inference,[],[2867,2598,149,158])). % 117.24/117.58 cnf(2952,plain, % 117.24/117.58 (P6(f30(a12),f31(a12))), % 117.24/117.58 inference(scs_inference,[],[2867,2598,134,149,158,152,163])). % 117.24/117.58 cnf(2962,plain, % 117.24/117.58 (P6(f16(a12),f31(a12))), % 117.24/117.58 inference(scs_inference,[],[92,2867,2598,134,149,158,152,163,151,147,165,141,164])). % 117.24/117.58 cnf(2964,plain, % 117.24/117.58 (~P4(f30(f30(a12)))), % 117.24/117.58 inference(scs_inference,[],[92,2867,2598,134,149,158,152,163,151,147,165,141,164,157])). % 117.24/117.58 cnf(2966,plain, % 117.24/117.58 (P1(f28(a8))), % 117.24/117.58 inference(scs_inference,[],[92,2867,2598,134,149,158,152,163,151,147,165,141,164,157,139])). % 117.24/117.58 cnf(2970,plain, % 117.24/117.58 (P7(f28(a8))), % 117.24/117.58 inference(scs_inference,[],[92,2867,2598,134,149,158,152,163,151,147,165,141,164,157,139,143,144])). % 117.24/117.58 cnf(2972,plain, % 117.24/117.58 (P6(f11(f32(a1)),f31(a1))), % 117.24/117.58 inference(scs_inference,[],[92,2867,1622,2598,134,149,158,152,163,151,147,165,141,164,157,139,143,144,178])). % 117.24/117.58 cnf(2974,plain, % 117.24/117.58 (P13(a4)), % 117.24/117.58 inference(scs_inference,[],[92,2867,1622,2598,134,65,149,158,152,163,151,147,165,141,164,157,139,143,144,178,146])). % 117.24/117.58 cnf(2978,plain, % 117.24/117.58 (E(f28(a8),a1)), % 117.24/117.58 inference(scs_inference,[],[92,2867,1622,2598,134,65,149,158,152,163,151,147,165,141,164,157,139,143,144,178,146,145,138])). % 117.24/117.58 cnf(2982,plain, % 117.24/117.58 (P4(f32(f28(a8)))), % 117.24/117.58 inference(scs_inference,[],[92,2867,1622,2598,134,65,1982,149,158,152,163,151,147,165,141,164,157,139,143,144,178,146,145,138,6,8,150])). % 117.24/117.58 cnf(2987,plain, % 117.24/117.58 (E(f33(f28(a1),x29871),f33(a1,x29871))), % 117.24/117.58 inference(scs_inference,[],[92,2867,2928,1622,2598,134,65,1982,149,158,152,163,151,147,165,141,164,157,139,143,144,178,146,145,138,6,8,150,292,312,9,11])). % 117.24/117.58 cnf(2992,plain, % 117.24/117.58 (E(f31(f28(a1)),f31(a1))), % 117.24/117.58 inference(scs_inference,[],[92,2867,2928,1622,2598,134,65,1982,149,158,152,163,151,147,165,141,164,157,139,143,144,178,146,145,138,6,8,150,292,312,9,11,13,10,4,5,7])). % 117.24/117.58 cnf(2993,plain, % 117.24/117.58 (E(f33(x29931,f28(a1)),f33(x29931,a1))), % 117.24/117.58 inference(scs_inference,[],[92,2867,2928,1622,2598,134,65,1982,149,158,152,163,151,147,165,141,164,157,139,143,144,178,146,145,138,6,8,150,292,312,9,11,13,10,4,5,7,12])). % 117.24/117.58 cnf(2995,plain, % 117.24/117.58 (E(f33(a1,a1),f33(f28(a1),f28(a1)))), % 117.24/117.58 inference(scs_inference,[],[92,2577,2867,2928,2908,2909,1622,2598,134,65,1982,149,158,152,163,151,147,165,141,164,157,139,143,144,178,146,145,138,6,8,150,292,312,9,11,13,10,4,5,7,12,2,3])). % 117.24/117.58 cnf(2996,plain, % 117.24/117.58 (E(f33(x29961,a1),f33(x29961,f28(a1)))), % 117.24/117.58 inference(rename_variables,[],[2908])). % 117.24/117.58 cnf(2997,plain, % 117.24/117.58 (E(f33(a1,x29971),f33(f28(a1),x29971))), % 117.24/117.58 inference(rename_variables,[],[2909])). % 117.24/117.58 cnf(2998,plain, % 117.24/117.58 (P2(f33(f28(a1),f28(a1)))), % 117.24/117.58 inference(scs_inference,[],[92,2577,2867,2928,2908,2909,2997,1042,1622,2598,134,65,1982,149,158,152,163,151,147,165,141,164,157,139,143,144,178,146,145,138,6,8,150,292,312,9,11,13,10,4,5,7,12,2,3,23])). % 117.24/117.58 cnf(2999,plain, % 117.24/117.58 (E(f33(a1,x29991),f33(f28(a1),x29991))), % 117.24/117.58 inference(rename_variables,[],[2909])). % 117.24/117.58 cnf(3000,plain, % 117.24/117.58 (~E(f16(a2),f32(a21))), % 117.24/117.58 inference(scs_inference,[],[92,2577,1969,2867,2928,2908,2909,2997,1042,1622,2598,134,65,1982,136,149,158,152,163,151,147,165,141,164,157,139,143,144,178,146,145,138,6,8,150,292,312,9,11,13,10,4,5,7,12,2,3,23,25])). % 117.24/117.58 cnf(3001,plain, % 117.24/117.58 (~E(f28(a8),f30(f30(a10)))), % 117.24/117.58 inference(scs_inference,[],[92,2577,1969,2867,2928,2908,2909,2997,2690,1042,1622,2598,134,65,1982,136,149,158,152,163,151,147,165,141,164,157,139,143,144,178,146,145,138,6,8,150,292,312,9,11,13,10,4,5,7,12,2,3,23,25,20])). % 117.24/117.58 cnf(3002,plain, % 117.24/117.58 (P4(f15(f31(a27)))), % 117.24/117.58 inference(scs_inference,[],[92,2577,1969,2867,2928,2908,2909,2997,2690,1042,1622,2598,134,65,1982,875,136,126,149,158,152,163,151,147,165,141,164,157,139,143,144,178,146,145,138,6,8,150,292,312,9,11,13,10,4,5,7,12,2,3,23,25,20,177])). % 117.24/117.58 cnf(3006,plain, % 117.24/117.58 (~P6(f31(x30061),f31(f28(a8)))), % 117.24/117.58 inference(scs_inference,[],[92,2577,2921,1969,2867,2928,2908,2909,2997,2690,1042,1622,2598,134,65,1982,875,136,126,149,158,152,163,151,147,165,141,164,157,139,143,144,178,146,145,138,6,8,150,292,312,9,11,13,10,4,5,7,12,2,3,23,25,20,177,184])). % 117.24/117.58 cnf(3008,plain, % 117.24/117.58 (~P6(f32(a21),f31(f16(a2)))), % 117.24/117.58 inference(scs_inference,[],[92,2577,2921,1969,2867,2928,2908,2909,2997,2690,1042,1622,2598,134,65,1982,875,136,126,149,158,152,163,151,147,165,141,164,157,139,143,144,178,146,145,138,6,8,150,292,312,9,11,13,10,4,5,7,12,2,3,23,25,20,177,184,179])). % 117.24/117.58 cnf(3010,plain, % 117.24/117.58 (P6(f33(f28(a1),f28(a1)),f31(x30101))), % 117.24/117.58 inference(scs_inference,[],[92,2577,2921,1969,2867,2928,2908,2909,2997,2999,2690,1042,1622,2598,134,1813,65,1982,875,136,126,149,158,152,163,151,147,165,141,164,157,139,143,144,178,146,145,138,6,8,150,292,312,9,11,13,10,4,5,7,12,2,3,23,25,20,177,184,179,15])). % 117.24/117.58 cnf(3012,plain, % 117.24/117.58 (~P6(a29,f31(f32(a1)))), % 117.24/117.58 inference(scs_inference,[],[92,2577,2921,1969,2867,2928,2804,2908,2909,2997,2999,2690,1042,1622,2598,134,1813,65,1982,875,136,126,149,158,152,163,151,147,165,141,164,157,139,143,144,178,146,145,138,6,8,150,292,312,9,11,13,10,4,5,7,12,2,3,23,25,20,177,184,179,15,16])). % 117.24/117.58 cnf(3013,plain, % 117.24/117.58 (~P11(x30131,f33(a1,a1))), % 117.24/117.58 inference(scs_inference,[],[92,2577,2921,1969,2867,2928,2804,2908,2996,2909,2997,2999,2690,1042,1622,2598,134,1813,65,1982,1057,875,136,126,149,158,152,163,151,147,165,141,164,157,139,143,144,178,146,145,138,6,8,150,292,312,9,11,13,10,4,5,7,12,2,3,23,25,20,177,184,179,15,16,18])). % 117.24/117.58 cnf(3032,plain, % 117.24/117.58 (P6(f30(a13),f31(a13))), % 117.24/117.58 inference(scs_inference,[],[2897,135,152,151,163])). % 117.24/117.58 cnf(3036,plain, % 117.24/117.58 (~P4(f16(f30(a2)))), % 117.24/117.58 inference(scs_inference,[],[2897,2657,135,152,151,163,149,158])). % 117.24/117.58 cnf(3042,plain, % 117.24/117.58 (P6(f16(a13),f31(a13))), % 117.24/117.58 inference(scs_inference,[],[2974,2897,2657,135,152,151,163,149,158,147,165,164])). % 117.24/117.58 cnf(3048,plain, % 117.24/117.58 (P1(f32(a8))), % 117.24/117.58 inference(scs_inference,[],[2974,2897,2657,135,152,151,163,149,158,147,165,164,157,141,139])). % 117.24/117.58 cnf(3050,plain, % 117.24/117.58 (P6(f11(a1),f31(f28(a1)))), % 117.24/117.58 inference(scs_inference,[],[2974,2897,2657,135,2010,152,151,163,149,158,147,165,164,157,141,139,178])). % 117.24/117.58 cnf(3052,plain, % 117.24/117.58 (E(f32(a8),a1)), % 117.24/117.58 inference(scs_inference,[],[2974,2897,2657,135,2010,152,151,163,149,158,147,165,164,157,141,139,178,138])). % 117.24/117.58 cnf(3058,plain, % 117.24/117.58 (P7(f32(a8))), % 117.24/117.58 inference(scs_inference,[],[2974,2897,3002,2657,135,2010,152,151,163,149,158,147,165,164,157,141,139,178,138,143,146,144])). % 117.24/117.58 cnf(3060,plain, % 117.24/117.58 (P8(f32(a8))), % 117.24/117.58 inference(scs_inference,[],[2974,2897,3002,2657,135,2010,152,151,163,149,158,147,165,164,157,141,139,178,138,143,146,144,145])). % 117.24/117.58 cnf(3063,plain, % 117.24/117.58 (P4(f32(f32(a8)))), % 117.24/117.58 inference(scs_inference,[],[2974,2897,2978,3002,2657,135,2010,152,151,163,149,158,147,165,164,157,141,139,178,138,143,146,144,145,6,150])). % 117.24/117.58 cnf(3068,plain, % 117.24/117.58 (E(f11(f28(a8)),f11(a1))), % 117.24/117.58 inference(scs_inference,[],[2974,2897,2978,3006,3002,2657,135,2010,152,151,163,149,158,147,165,164,157,141,139,178,138,143,146,144,145,6,150,312,8,4,9])). % 117.24/117.58 cnf(3069,plain, % 117.24/117.58 (E(f31(f28(a8)),f31(a1))), % 117.24/117.58 inference(scs_inference,[],[2974,2897,2978,3006,3002,2657,135,2010,152,151,163,149,158,147,165,164,157,141,139,178,138,143,146,144,145,6,150,312,8,4,9,7])). % 117.24/117.58 cnf(3072,plain, % 117.24/117.58 (E(f33(x30721,f28(a8)),f33(x30721,a1))), % 117.24/117.58 inference(scs_inference,[],[2974,2897,2978,3006,3002,2657,135,2010,152,151,163,149,158,147,165,164,157,141,139,178,138,143,146,144,145,6,150,312,8,4,9,7,10,292,12])). % 117.24/117.58 cnf(3073,plain, % 117.24/117.58 (E(f33(f28(a8),x30731),f33(a1,x30731))), % 117.24/117.58 inference(scs_inference,[],[2974,2897,2978,3006,3002,2657,135,2010,152,151,163,149,158,147,165,164,157,141,139,178,138,143,146,144,145,6,150,312,8,4,9,7,10,292,12,11])). % 117.24/117.58 cnf(3074,plain, % 117.24/117.58 (E(f7(f28(a8)),f7(a1))), % 117.24/117.58 inference(scs_inference,[],[2974,2897,2978,3006,3002,2657,135,2010,152,151,163,149,158,147,165,164,157,141,139,178,138,143,146,144,145,6,150,312,8,4,9,7,10,292,12,11,5])). % 117.24/117.58 cnf(3075,plain, % 117.24/117.58 (E(f15(f28(a8)),f15(a1))), % 117.24/117.58 inference(scs_inference,[],[2974,2897,2978,3006,3002,2657,135,2010,152,151,163,149,158,147,165,164,157,141,139,178,138,143,146,144,145,6,150,312,8,4,9,7,10,292,12,11,5,13])). % 117.24/117.58 cnf(3078,plain, % 117.24/117.58 (P6(f15(x30781),x30781)), % 117.24/117.58 inference(rename_variables,[],[126])). % 117.24/117.58 cnf(3081,plain, % 117.24/117.58 (P6(f15(x30811),x30811)), % 117.24/117.58 inference(rename_variables,[],[126])). % 117.24/117.58 cnf(3088,plain, % 117.24/117.58 (P6(f33(f28(a1),f28(a1)),f31(x30881))), % 117.24/117.58 inference(rename_variables,[],[3010])). % 117.24/117.58 cnf(3090,plain, % 117.24/117.58 (~E(f16(a23),f32(a21))), % 117.24/117.58 inference(scs_inference,[],[2974,2579,1970,2897,2966,2978,3010,3006,3002,3001,2657,135,2010,136,126,3078,3081,152,151,163,149,158,147,165,164,157,141,139,178,138,143,146,144,145,6,150,312,8,4,9,7,10,292,12,11,5,13,2,174,175,173,3,185,25])). % 117.24/117.58 cnf(3091,plain, % 117.24/117.58 (~E(f32(a8),f16(f30(a10)))), % 117.24/117.58 inference(scs_inference,[],[2974,2579,1970,2897,2966,2978,3010,3006,2692,3002,3001,2657,135,2010,136,126,3078,3081,152,151,163,149,158,147,165,164,157,141,139,178,138,143,146,144,145,6,150,312,8,4,9,7,10,292,12,11,5,13,2,174,175,173,3,185,25,20])). % 117.24/117.58 cnf(3092,plain, % 117.24/117.58 (P11(f30(a2),f31(a2))), % 117.24/117.58 inference(scs_inference,[],[2974,2579,1970,2773,2897,2966,2978,3010,3006,2692,3002,3001,2657,135,2010,137,136,126,3078,3081,152,151,163,149,158,147,165,164,157,141,139,178,138,143,146,144,145,6,150,312,8,4,9,7,10,292,12,11,5,13,2,174,175,173,3,185,25,20,177])). % 117.24/117.58 cnf(3095,plain, % 117.24/117.58 (~P6(a21,f31(f32(a8)))), % 117.24/117.58 inference(scs_inference,[],[2974,2579,1970,2773,2897,2966,2978,3010,3006,2692,3002,3001,2741,2657,135,2010,137,136,126,3078,3081,152,151,163,149,158,147,165,164,157,141,139,178,138,143,146,144,145,6,150,312,8,4,9,7,10,292,12,11,5,13,2,174,175,173,3,185,25,20,177,184])). % 117.24/117.58 cnf(3097,plain, % 117.24/117.58 (~P6(f32(a21),f31(f16(a23)))), % 117.24/117.58 inference(scs_inference,[],[2974,2579,1970,2773,2897,2966,2978,3010,3006,2692,3002,3001,2741,2657,135,2010,137,136,126,3078,3081,152,151,163,149,158,147,165,164,157,141,139,178,138,143,146,144,145,6,150,312,8,4,9,7,10,292,12,11,5,13,2,174,175,173,3,185,25,20,177,184,179])). % 117.24/117.58 cnf(3101,plain, % 117.24/117.58 (~P11(x31011,f33(f32(a1),f32(a1)))), % 117.24/117.58 inference(scs_inference,[],[2974,3013,2579,1970,2773,2897,2966,2978,3010,3088,2914,3006,2692,3002,3001,3008,2741,2657,135,2010,137,136,126,3078,3081,152,151,163,149,158,147,165,164,157,141,139,178,138,143,146,144,145,6,150,312,8,4,9,7,10,292,12,11,5,13,2,174,175,173,3,185,25,20,177,184,179,15,18])). % 117.24/117.58 cnf(3104,plain, % 117.24/117.58 (~P11(f31(a2),f30(a2))), % 117.24/117.58 inference(scs_inference,[],[80,2974,3013,2579,1970,2773,2897,2966,2978,3010,3088,2914,3006,2692,3002,3001,3008,2741,2657,135,2010,137,136,96,126,3078,3081,152,151,163,149,158,147,165,164,157,141,139,178,138,143,146,144,145,6,150,312,8,4,9,7,10,292,12,11,5,13,2,174,175,173,3,185,25,20,177,184,179,15,18,183,180])). % 117.24/117.58 cnf(3110,plain, % 117.24/117.58 (P13(f28(a6))), % 117.24/117.58 inference(scs_inference,[],[66,151])). % 117.24/117.58 cnf(3114,plain, % 117.24/117.58 (P6(f30(a3),f31(a3))), % 117.24/117.58 inference(scs_inference,[],[132,66,151,152,163])). % 117.24/117.58 cnf(3118,plain, % 117.24/117.58 (P4(f28(a5))), % 117.24/117.58 inference(scs_inference,[],[2338,132,67,66,151,152,163,158,149])). % 117.24/117.58 cnf(3124,plain, % 117.24/117.58 (E(f33(a8,f28(a8)),f32(a8))), % 117.24/117.58 inference(scs_inference,[],[2721,2338,132,67,66,151,152,163,158,149,147,157,165])). % 117.24/117.58 cnf(3126,plain, % 117.24/117.58 (P6(f16(a3),f31(a3))), % 117.24/117.58 inference(scs_inference,[],[2721,2338,132,67,66,151,152,163,158,149,147,157,165,164])). % 117.24/117.58 cnf(3134,plain, % 117.24/117.58 (P7(f32(f7(x31341)))), % 117.24/117.58 inference(scs_inference,[],[2813,2721,2338,132,67,66,151,152,163,158,149,147,157,165,164,141,139,143,144])). % 117.24/117.58 cnf(3138,plain, % 117.24/117.58 (P6(f7(a1),f31(f28(a1)))), % 117.24/117.58 inference(scs_inference,[],[2813,2721,2338,2011,132,67,66,151,152,163,158,149,147,157,165,164,141,139,143,144,138,178])). % 117.24/117.58 cnf(3140,plain, % 117.24/117.58 (P8(f32(f7(x31401)))), % 117.24/117.58 inference(scs_inference,[],[2813,2721,2338,2011,132,67,66,151,152,163,158,149,147,157,165,164,141,139,143,144,138,178,145])). % 117.24/117.58 cnf(3143,plain, % 117.24/117.58 (P4(f32(a5))), % 117.24/117.58 inference(scs_inference,[],[3052,2813,2721,2338,2011,132,67,66,151,152,163,158,149,147,157,165,164,141,139,143,144,138,178,145,6,150])). % 117.24/117.58 cnf(3151,plain, % 117.24/117.58 (E(f31(f32(a8)),f31(a1))), % 117.24/117.58 inference(scs_inference,[],[3052,2813,3097,2721,2338,2011,132,67,66,151,152,163,158,149,147,157,165,164,141,139,143,144,138,178,145,6,150,4,312,8,12,11,9,7])). % 117.24/117.58 cnf(3158,plain, % 117.24/117.58 (P6(f15(x31581),x31581)), % 117.24/117.58 inference(rename_variables,[],[126])). % 117.24/117.58 cnf(3161,plain, % 117.24/117.58 (P6(f15(x31611),x31611)), % 117.24/117.58 inference(rename_variables,[],[126])). % 117.24/117.58 cnf(3167,plain, % 117.24/117.58 (P6(f15(f30(a2)),a2)), % 117.24/117.58 inference(scs_inference,[],[2581,3048,3052,2813,3091,3097,2721,2773,2338,2011,132,2658,67,66,126,3158,3161,151,152,163,158,149,147,157,165,164,141,139,143,144,138,178,145,6,150,4,312,8,12,11,9,7,292,10,13,5,2,175,174,173,3,185])). % 117.24/117.58 cnf(3169,plain, % 117.24/117.58 (~E(f28(a8),f32(a21))), % 117.24/117.58 inference(scs_inference,[],[2581,2970,3048,3052,2813,3091,3097,2721,2773,2338,2011,132,2658,67,66,136,126,3158,3161,151,152,163,158,149,147,157,165,164,141,139,143,144,138,178,145,6,150,4,312,8,12,11,9,7,292,10,13,5,2,175,174,173,3,185,25])). % 117.24/117.58 cnf(3173,plain, % 117.24/117.58 (~P6(f32(a21),f31(f28(a8)))), % 117.24/117.58 inference(scs_inference,[],[2581,2970,3048,3104,3052,2813,2777,3091,3097,2721,2773,2338,1078,2011,132,2657,2658,67,66,136,126,3158,3161,151,152,163,158,149,147,157,165,164,141,139,143,144,138,178,145,6,150,4,312,8,12,11,9,7,292,10,13,5,2,175,174,173,3,185,25,20,177,179])). % 117.24/117.58 cnf(3175,plain, % 117.24/117.58 (~P6(a29,f31(f28(a8)))), % 117.24/117.58 inference(scs_inference,[],[2581,2970,3048,3104,3052,3069,2813,2777,3091,3097,2721,2773,2338,1078,2011,132,2928,2657,2658,67,66,136,126,3158,3161,151,152,163,158,149,147,157,165,164,141,139,143,144,138,178,145,6,150,4,312,8,12,11,9,7,292,10,13,5,2,175,174,173,3,185,25,20,177,179,16])). % 117.24/117.58 cnf(3176,plain, % 117.24/117.58 (P6(f11(a1),f31(f28(a8)))), % 117.24/117.58 inference(scs_inference,[],[2581,2970,3048,3104,3052,3068,3069,2813,2777,3091,3097,2721,2773,2338,1078,2011,132,2928,2657,2658,67,66,128,136,126,3158,3161,151,152,163,158,149,147,157,165,164,141,139,143,144,138,178,145,6,150,4,312,8,12,11,9,7,292,10,13,5,2,175,174,173,3,185,25,20,177,179,16,15])). % 117.24/117.58 cnf(3178,plain, % 117.24/117.58 (~P11(x31781,f32(a8))), % 117.24/117.58 inference(scs_inference,[],[2581,2970,3048,3104,3052,3068,3069,2813,2777,3091,3097,2721,2773,2338,1078,2011,132,2928,2657,2658,67,66,190,128,136,126,3158,3161,151,152,163,158,149,147,157,165,164,141,139,143,144,138,178,145,6,150,4,312,8,12,11,9,7,292,10,13,5,2,175,174,173,3,185,25,20,177,179,16,15,18])). % 117.24/117.58 cnf(3190,plain, % 117.24/117.58 (P6(f30(a10),f31(a10))), % 117.24/117.58 inference(scs_inference,[],[3118,133,152,151,163])). % 117.24/117.58 cnf(3194,plain, % 117.24/117.58 (P4(f28(f28(a5)))), % 117.24/117.58 inference(scs_inference,[],[3118,2275,133,152,151,163,147,149])). % 117.24/117.58 cnf(3198,plain, % 117.24/117.58 (P6(f16(a10),f31(a10))), % 117.24/117.58 inference(scs_inference,[],[3118,2275,133,152,151,163,147,149,158,164])). % 117.24/117.58 cnf(3200,plain, % 117.24/117.58 (~P4(f30(f30(a21)))), % 117.24/117.58 inference(scs_inference,[],[3118,2275,133,152,151,163,147,149,158,164,157])). % 117.24/117.58 cnf(3206,plain, % 117.24/117.58 (P1(f28(a5))), % 117.24/117.58 inference(scs_inference,[],[3118,87,2275,133,152,151,163,147,149,158,164,157,165,141,139])). % 117.24/117.58 cnf(3208,plain, % 117.24/117.58 (E(f28(a5),a1)), % 117.24/117.58 inference(scs_inference,[],[3118,87,2275,133,152,151,163,147,149,158,164,157,165,141,139,138])). % 117.24/117.58 cnf(3210,plain, % 117.24/117.58 (P7(f28(a5))), % 117.24/117.58 inference(scs_inference,[],[3118,87,2275,133,152,151,163,147,149,158,164,157,165,141,139,138,144])). % 117.24/117.58 cnf(3216,plain, % 117.24/117.58 (P6(f7(f28(a1)),f31(a1))), % 117.24/117.58 inference(scs_inference,[],[3118,87,2275,1983,133,152,151,163,147,149,158,164,157,165,141,139,138,144,143,145,178])). % 117.24/117.58 cnf(3218,plain, % 117.24/117.58 (P4(f32(f28(a5)))), % 117.24/117.58 inference(scs_inference,[],[3118,87,2275,1983,133,152,151,163,147,149,158,164,157,165,141,139,138,144,143,145,178,150])). % 117.24/117.58 cnf(3221,plain, % 117.24/117.58 (E(f28(f28(a5)),f28(a1))), % 117.24/117.58 inference(scs_inference,[],[3118,87,2275,1983,133,152,151,163,147,149,158,164,157,165,141,139,138,144,143,145,178,150,6,4])). % 117.24/117.58 cnf(3222,plain, % 117.24/117.58 (E(f33(x32221,f28(a5)),f33(x32221,a1))), % 117.24/117.58 inference(scs_inference,[],[3118,87,2275,1983,133,152,151,163,147,149,158,164,157,165,141,139,138,144,143,145,178,150,6,4,12])). % 117.24/117.58 cnf(3226,plain, % 117.24/117.58 (E(f15(f28(a5)),f15(a1))), % 117.24/117.58 inference(scs_inference,[],[3118,3173,87,2275,1983,133,152,151,163,147,149,158,164,157,165,141,139,138,144,143,145,178,150,6,4,12,312,8,10,13])). % 117.24/117.58 cnf(3227,plain, % 117.24/117.58 (E(f33(f28(a5),x32271),f33(a1,x32271))), % 117.24/117.58 inference(scs_inference,[],[3118,3173,87,2275,1983,133,152,151,163,147,149,158,164,157,165,141,139,138,144,143,145,178,150,6,4,12,312,8,10,13,11])). % 117.24/117.58 cnf(3230,plain, % 117.24/117.58 (E(f31(f28(a5)),f31(a1))), % 117.24/117.58 inference(scs_inference,[],[3118,3173,87,2275,1983,133,152,151,163,147,149,158,164,157,165,141,139,138,144,143,145,178,150,6,4,12,312,8,10,13,11,9,292,7])). % 117.24/117.58 cnf(3231,plain, % 117.24/117.58 (E(f7(f28(a5)),f7(a1))), % 117.24/117.58 inference(scs_inference,[],[3118,3173,87,2275,1983,133,152,151,163,147,149,158,164,157,165,141,139,138,144,143,145,178,150,6,4,12,312,8,10,13,11,9,292,7,5])). % 117.24/117.58 cnf(3239,plain, % 117.24/117.58 (E(f33(f28(a8),f28(a8)),f33(a1,a1))), % 117.24/117.58 inference(scs_inference,[],[2583,3118,3072,3073,3167,3173,87,2275,1983,37,133,152,151,163,147,149,158,164,157,165,141,139,138,144,143,145,178,150,6,4,12,312,8,10,13,11,9,292,7,5,2,175,174,173,3])). % 117.24/117.58 cnf(3240,plain, % 117.24/117.58 (E(f33(x32401,f28(a8)),f33(x32401,a1))), % 117.24/117.58 inference(rename_variables,[],[3072])). % 117.24/117.58 cnf(3243,plain, % 117.24/117.58 (P13(f33(f32(a1),a1))), % 117.24/117.58 inference(scs_inference,[],[2583,1429,3118,3072,3073,2919,3167,3173,2993,87,2910,2275,1983,37,133,152,151,163,147,149,158,164,157,165,141,139,138,144,143,145,178,150,6,4,12,312,8,10,13,11,9,292,7,5,2,175,174,173,3,26,22])). % 117.24/117.58 cnf(3245,plain, % 117.24/117.58 (~P11(a29,f30(a3))), % 117.24/117.58 inference(scs_inference,[],[2583,1429,3114,3118,3072,3073,2919,3167,3173,2993,87,2910,2275,1983,37,133,419,152,151,163,147,149,158,164,157,165,141,139,138,144,143,145,178,150,6,4,12,312,8,10,13,11,9,292,7,5,2,175,174,173,3,26,22,185])). % 117.24/117.58 cnf(3247,plain, % 117.24/117.58 (~E(f32(a8),f32(a21))), % 117.24/117.58 inference(scs_inference,[],[2583,1429,3058,3114,3118,3072,3073,2919,3167,3173,2993,87,2910,2275,1983,37,133,419,136,152,151,163,147,149,158,164,157,165,141,139,138,144,143,145,178,150,6,4,12,312,8,10,13,11,9,292,7,5,2,175,174,173,3,26,22,185,25])). % 117.24/117.58 cnf(3248,plain, % 117.24/117.58 (~E(f28(a5),f16(f28(a10)))), % 117.24/117.58 inference(scs_inference,[],[2583,1429,3058,3114,3118,3072,3073,2919,2783,3167,3173,2993,87,2910,2275,1983,37,133,419,136,152,151,163,147,149,158,164,157,165,141,139,138,144,143,145,178,150,6,4,12,312,8,10,13,11,9,292,7,5,2,175,174,173,3,26,22,185,25,20])). % 117.24/117.58 cnf(3249,plain, % 117.24/117.58 (P11(f16(a2),f31(a2))), % 117.24/117.58 inference(scs_inference,[],[2583,1429,2787,3058,3114,3118,3072,3073,2919,2783,3167,3173,2993,87,2910,2275,1983,37,133,137,419,136,152,151,163,147,149,158,164,157,165,141,139,138,144,143,145,178,150,6,4,12,312,8,10,13,11,9,292,7,5,2,175,174,173,3,26,22,185,25,20,177])). % 117.24/117.58 cnf(3252,plain, % 117.24/117.58 (~P6(f31(a2),f31(f28(a5)))), % 117.24/117.58 inference(scs_inference,[],[2583,1429,2787,3058,3114,3118,3072,3073,2919,2783,3167,3173,2993,3092,87,2910,2275,1983,37,133,137,419,136,152,151,163,147,149,158,164,157,165,141,139,138,144,143,145,178,150,6,4,12,312,8,10,13,11,9,292,7,5,2,175,174,173,3,26,22,185,25,20,177,184])). % 117.24/117.58 cnf(3254,plain, % 117.24/117.58 (~P6(f32(a21),f31(f32(a8)))), % 117.24/117.58 inference(scs_inference,[],[2583,1429,2787,3058,3114,3118,3072,3073,2919,2783,3167,3173,2993,3092,87,2910,2275,1983,37,133,137,419,136,152,151,163,147,149,158,164,157,165,141,139,138,144,143,145,178,150,6,4,12,312,8,10,13,11,9,292,7,5,2,175,174,173,3,26,22,185,25,20,177,184,179])). % 117.24/117.58 cnf(3256,plain, % 117.24/117.58 (~P6(a29,f31(f32(a8)))), % 117.24/117.58 inference(scs_inference,[],[2583,1429,2787,3058,3114,3118,3072,3073,3151,2919,2783,3167,3173,2993,3092,87,2910,2275,1983,37,133,2928,137,419,136,152,151,163,147,149,158,164,157,165,141,139,138,144,143,145,178,150,6,4,12,312,8,10,13,11,9,292,7,5,2,175,174,173,3,26,22,185,25,20,177,184,179,16])). % 117.24/117.58 cnf(3257,plain, % 117.24/117.58 (~E(f11(a1),f32(a21))), % 117.24/117.58 inference(scs_inference,[],[2583,1429,2787,3058,3114,3118,3072,3073,3151,2919,2783,3167,3173,3176,2993,3092,87,2910,2275,1983,37,133,2928,137,419,136,152,151,163,147,149,158,164,157,165,141,139,138,144,143,145,178,150,6,4,12,312,8,10,13,11,9,292,7,5,2,175,174,173,3,26,22,185,25,20,177,184,179,16,15])). % 117.24/117.58 cnf(3258,plain, % 117.24/117.58 (P18(f33(x32581,a1),f33(x32581,f28(a8)))), % 117.24/117.58 inference(scs_inference,[],[2583,1429,2787,3058,3114,3118,3072,3240,3073,3151,2919,2783,3167,3173,3176,2993,3092,87,2910,2275,1983,37,133,2928,125,137,419,136,152,151,163,147,149,158,164,157,165,141,139,138,144,143,145,178,150,6,4,12,312,8,10,13,11,9,292,7,5,2,175,174,173,3,26,22,185,25,20,177,184,179,16,15,30])). % 117.24/117.58 cnf(3260,plain, % 117.24/117.58 (~P11(x32601,f33(a8,f28(a8)))), % 117.24/117.58 inference(scs_inference,[],[2583,3178,1429,2787,3058,3114,3118,3072,3240,3073,3151,3124,2919,2783,3167,3173,3176,2993,3092,87,2910,2275,1983,37,133,2928,125,137,419,136,152,151,163,147,149,158,164,157,165,141,139,138,144,143,145,178,150,6,4,12,312,8,10,13,11,9,292,7,5,2,175,174,173,3,26,22,185,25,20,177,184,179,16,15,30,18])). % 117.24/117.58 cnf(3263,plain, % 117.24/117.58 (~P11(f31(a2),f16(a2))), % 117.24/117.58 inference(scs_inference,[],[80,2583,3178,1429,2787,3058,3114,3118,3072,3240,3073,3151,3124,2919,2783,3167,3173,3176,2993,3092,87,2910,2275,1983,37,133,2928,125,137,419,136,96,152,151,163,147,149,158,164,157,165,141,139,138,144,143,145,178,150,6,4,12,312,8,10,13,11,9,292,7,5,2,175,174,173,3,26,22,185,25,20,177,184,179,16,15,30,18,183,180])). % 117.24/117.58 cnf(3269,plain, % 117.24/117.58 (P13(f28(f32(a5)))), % 117.24/117.58 inference(scs_inference,[],[3143,151])). % 117.24/117.58 cnf(3273,plain, % 117.24/117.58 (P4(f28(f32(a5)))), % 117.24/117.58 inference(scs_inference,[],[3143,151,152,149])). % 117.24/117.58 cnf(3275,plain, % 117.24/117.58 (~P4(f16(f16(a29)))), % 117.24/117.58 inference(scs_inference,[],[3143,1864,151,152,149,158])). % 117.24/117.58 cnf(3289,plain, % 117.24/117.58 (P6(f11(a1),f31(f32(a1)))), % 117.24/117.58 inference(scs_inference,[],[3194,3143,1864,1116,90,151,152,149,158,147,165,157,141,139,143,178])). % 117.24/117.58 cnf(3297,plain, % 117.24/117.58 (P4(f32(f32(a5)))), % 117.24/117.58 inference(scs_inference,[],[3194,3143,1864,1116,90,151,152,149,158,147,165,157,141,139,143,178,144,138,145,150])). % 117.24/117.58 cnf(3303,plain, % 117.24/117.58 (P6(f15(x33031),x33031)), % 117.24/117.58 inference(rename_variables,[],[126])). % 117.24/117.58 cnf(3306,plain, % 117.24/117.58 (P6(f15(x33061),x33061)), % 117.24/117.58 inference(rename_variables,[],[126])). % 117.24/117.58 cnf(3309,plain, % 117.24/117.58 (P6(f15(x33091),x33091)), % 117.24/117.58 inference(rename_variables,[],[126])). % 117.24/117.58 cnf(3312,plain, % 117.24/117.58 (P1(f33(a1,a1))), % 117.24/117.58 inference(scs_inference,[],[2585,3206,3208,3194,3248,3252,3143,1043,2993,1864,1116,90,126,3303,3306,151,152,149,158,147,165,157,141,139,143,178,144,138,145,150,312,292,2,175,174,173,3,14])). % 117.24/117.58 cnf(3313,plain, % 117.24/117.58 (E(f33(x33131,f28(a1)),f33(x33131,a1))), % 117.24/117.58 inference(rename_variables,[],[2993])). % 117.24/117.58 cnf(3314,plain, % 117.24/117.58 (P8(f33(a1,a1))), % 117.24/117.58 inference(scs_inference,[],[2585,3206,3208,3194,3248,3252,3143,1043,2993,3313,1864,1047,1116,90,126,3303,3306,151,152,149,158,147,165,157,141,139,143,178,144,138,145,150,312,292,2,175,174,173,3,14,19])). % 117.24/117.58 cnf(3315,plain, % 117.24/117.58 (E(f33(x33151,f28(a1)),f33(x33151,a1))), % 117.24/117.58 inference(rename_variables,[],[2993])). % 117.24/117.58 cnf(3322,plain, % 117.24/117.58 (~E(f28(a5),f32(a21))), % 117.24/117.58 inference(scs_inference,[],[2585,2952,1097,3206,3210,3263,3208,2871,3194,3248,3252,3143,2895,1043,2993,3313,1864,777,1047,1116,90,2599,136,126,3303,3306,151,152,149,158,147,165,157,141,139,143,178,144,138,145,150,312,292,2,175,174,173,3,14,19,29,185,20,177,25])). % 117.24/117.58 cnf(3323,plain, % 117.24/117.58 (~P6(f31(a2),f31(f32(a5)))), % 117.24/117.58 inference(scs_inference,[],[2585,2952,1097,3206,3210,3249,3263,3208,2871,3194,3248,3252,3143,2895,1043,2993,3313,1864,777,1047,1116,90,2599,136,126,3303,3306,151,152,149,158,147,165,157,141,139,143,178,144,138,145,150,312,292,2,175,174,173,3,14,19,29,185,20,177,25,184])). % 117.24/117.58 cnf(3327,plain, % 117.24/117.58 (~P6(f32(a21),f31(f28(a5)))), % 117.24/117.58 inference(scs_inference,[],[2585,2952,1097,3206,3210,3249,3263,3208,2871,3194,3248,3252,3143,2895,1043,2993,3313,1864,777,1047,1116,90,3118,2599,136,126,3303,3306,151,152,149,158,147,165,157,141,139,143,178,144,138,145,150,312,292,2,175,174,173,3,14,19,29,185,20,177,25,184,156,179])). % 117.24/117.58 cnf(3330,plain, % 117.24/117.58 (~P6(a29,f31(f28(a5)))), % 117.24/117.58 inference(scs_inference,[],[2585,2952,1097,3206,3210,3249,3263,3208,3230,2871,3194,3248,3252,3143,2895,1043,2993,3313,1864,777,1047,1116,90,2928,3118,2599,778,136,126,3303,3306,151,152,149,158,147,165,157,141,139,143,178,144,138,145,150,312,292,2,175,174,173,3,14,19,29,185,20,177,25,184,156,179,17,16])). % 117.24/117.58 cnf(3331,plain, % 117.24/117.58 (P18(f33(f28(a8),a1),f33(a1,a1))), % 117.24/117.58 inference(scs_inference,[],[2585,2952,1097,3206,3210,3249,3263,3208,3239,3230,3258,2871,3194,3248,3252,3143,2895,1043,2993,3313,1864,777,1047,1116,90,2928,3118,2599,778,136,126,3303,3306,151,152,149,158,147,165,157,141,139,143,178,144,138,145,150,312,292,2,175,174,173,3,14,19,29,185,20,177,25,184,156,179,17,16,31])). % 117.24/117.58 cnf(3333,plain, % 117.24/117.58 (P6(f15(a1),f28(a5))), % 117.24/117.58 inference(scs_inference,[],[2585,2952,1097,3206,3210,3249,3263,3208,3239,3226,3230,3258,2871,3194,3248,3252,3143,2895,1043,2993,3313,1864,777,1047,1116,90,2928,3118,2599,778,136,126,3303,3306,3309,151,152,149,158,147,165,157,141,139,143,178,144,138,145,150,312,292,2,175,174,173,3,14,19,29,185,20,177,25,184,156,179,17,16,31,15])). % 117.24/117.58 cnf(3335,plain, % 117.24/117.58 (~P11(x33351,f28(a5))), % 117.24/117.58 inference(scs_inference,[],[2585,2952,1097,3206,3210,3249,3263,3208,3239,3226,3230,3258,2871,3194,3248,3252,3143,2895,1043,2993,3313,1864,777,1047,1116,90,2928,3118,2599,778,190,136,126,3303,3306,3309,151,152,149,158,147,165,157,141,139,143,178,144,138,145,150,312,292,2,175,174,173,3,14,19,29,185,20,177,25,184,156,179,17,16,31,15,18])). % 117.24/117.58 cnf(3342,plain, % 117.24/117.58 (P3(f33(a1,a1))), % 117.24/117.58 inference(scs_inference,[],[2585,2952,1097,3206,3210,3249,3263,3208,3239,3226,3230,2769,3140,3258,2871,3194,3248,3252,3143,1081,2895,1043,2993,3313,1864,777,1093,1047,1116,90,2928,2813,3118,2599,778,190,136,126,3303,3306,3309,151,152,149,158,147,165,157,141,139,143,178,144,138,145,150,312,292,2,175,174,173,3,14,19,29,185,20,177,25,184,156,179,17,16,31,15,18,183,159,142])). % 117.24/117.58 cnf(3344,plain, % 117.24/117.58 (P2(f33(a1,a1))), % 117.24/117.58 inference(scs_inference,[],[2585,2952,1097,3206,3210,3249,3263,3208,3239,3226,3230,2769,3140,3258,2871,3194,3248,3252,3143,1081,2895,1043,2993,3313,1864,777,1093,1047,1116,90,2928,2813,3118,2599,778,190,136,126,3303,3306,3309,151,152,149,158,147,165,157,141,139,143,178,144,138,145,150,312,292,2,175,174,173,3,14,19,29,185,20,177,25,184,156,179,17,16,31,15,18,183,159,142,140])). % 117.24/117.58 cnf(3348,plain, % 117.24/117.58 (P3(f33(f32(a1),a1))), % 117.24/117.58 inference(scs_inference,[],[2585,2952,1097,3110,3206,3210,3249,3263,3208,3239,3226,3230,2769,3140,2912,3258,2871,3194,3248,3252,3143,1081,2895,1043,2993,3313,3315,1864,777,1093,1047,1116,90,2928,2813,3118,2599,778,190,136,126,3303,3306,3309,151,152,149,158,147,165,157,141,139,143,178,144,138,145,150,312,292,2,175,174,173,3,14,19,29,185,20,177,25,184,156,179,17,16,31,15,18,183,159,142,140,161,21])). % 117.24/117.58 cnf(3356,plain, % 117.24/117.58 (P4(f28(f11(x33561)))), % 117.24/117.58 inference(scs_inference,[],[117,152,151,149])). % 117.24/117.58 cnf(3360,plain, % 117.24/117.58 (~P4(f16(f30(a29)))), % 117.24/117.58 inference(scs_inference,[],[1817,117,152,151,149,147,158])). % 117.24/117.58 cnf(3362,plain, % 117.24/117.58 (E(f33(a25,f28(a25)),f32(a25))), % 117.24/117.58 inference(scs_inference,[],[1817,85,117,152,151,149,147,158,165])). % 117.24/117.58 cnf(3376,plain, % 117.24/117.58 (E(f28(f32(a5)),a1)), % 117.24/117.58 inference(scs_inference,[],[3273,1817,1122,85,117,152,151,149,147,158,165,139,157,141,143,178,145,138])). % 117.24/117.58 cnf(3380,plain, % 117.24/117.58 (P4(f32(f11(x33801)))), % 117.24/117.58 inference(scs_inference,[],[3273,1817,1122,85,117,152,151,149,147,158,165,139,157,141,143,178,145,138,144,150])). % 117.24/117.58 cnf(3384,plain, % 117.24/117.58 (~E(f32(a1),f30(a12))), % 117.24/117.58 inference(scs_inference,[],[2627,3273,3254,1817,1122,85,117,152,151,149,147,158,165,139,157,141,143,178,145,138,144,150,312,292,2])). % 117.24/117.58 cnf(3386,plain, % 117.24/117.58 (P6(f15(x33861),x33861)), % 117.24/117.58 inference(rename_variables,[],[126])). % 117.24/117.58 cnf(3389,plain, % 117.24/117.58 (P6(f15(x33891),x33891)), % 117.24/117.58 inference(rename_variables,[],[126])). % 117.24/117.58 cnf(3394,plain, % 117.24/117.58 (E(f33(f28(a5),f28(a5)),f33(a1,a1))), % 117.24/117.58 inference(scs_inference,[],[3312,2627,3222,3227,3273,3254,1817,1122,85,117,126,3386,3389,152,151,149,147,158,165,139,157,141,143,178,145,138,144,150,312,292,2,175,174,173,3])). % 117.24/117.58 cnf(3397,plain, % 117.24/117.58 (~P11(a29,f16(a3))), % 117.24/117.58 inference(scs_inference,[],[3312,3126,2627,3222,3227,3273,3254,1817,1122,85,117,419,126,3386,3389,152,151,149,147,158,165,139,157,141,143,178,145,138,144,150,312,292,2,175,174,173,3,185])). % 117.24/117.58 cnf(3399,plain, % 117.24/117.58 (P11(f30(a23),f31(a23))), % 117.24/117.58 inference(scs_inference,[],[3312,2865,3126,2627,3222,3227,3273,3254,1817,1122,85,117,137,419,126,3386,3389,152,151,149,147,158,165,139,157,141,143,178,145,138,144,150,312,292,2,175,174,173,3,185,177])). % 117.24/117.58 cnf(3402,plain, % 117.24/117.58 (~E(f28(f32(a5)),f30(a29))), % 117.24/117.58 inference(scs_inference,[],[3312,2865,3126,2627,3222,3227,3273,3254,1817,1122,85,117,137,419,126,3386,3389,152,151,149,147,158,165,139,157,141,143,178,145,138,144,150,312,292,2,175,174,173,3,185,177,20])). % 117.24/117.58 cnf(3404,plain, % 117.24/117.58 (P6(f15(a1),f33(f28(a1),f28(a1)))), % 117.24/117.58 inference(scs_inference,[],[3312,2865,3126,2627,3222,3227,1266,3273,3254,1038,2909,1817,1122,85,117,137,419,136,126,3386,3389,152,151,149,147,158,165,139,157,141,143,178,145,138,144,150,312,292,2,175,174,173,3,185,177,20,25,16])). % 117.24/117.58 cnf(3406,plain, % 117.24/117.58 (~E(f28(a1),f31(a2))), % 117.24/117.59 inference(scs_inference,[],[3312,2865,3126,2627,3222,3227,1266,3273,3254,3323,1038,2792,2909,1817,1122,85,117,137,419,136,126,3386,3389,152,151,149,147,158,165,139,157,141,143,178,145,138,144,150,312,292,2,175,174,173,3,185,177,20,25,16,15])). % 117.24/117.59 cnf(3414,plain, % 117.24/117.59 (~P11(f31(a23),f30(a23))), % 117.24/117.59 inference(scs_inference,[],[80,3312,2865,3126,2627,3335,3222,3227,1266,3269,3273,3254,3323,1829,1038,2792,773,2909,1817,1122,85,117,137,419,136,96,126,3386,3389,152,151,149,147,158,165,139,157,141,143,178,145,138,144,150,312,292,2,175,174,173,3,185,177,20,25,16,15,18,183,159,180])). % 117.24/117.59 cnf(3417,plain, % 117.24/117.59 (~P6(f32(a21),f31(f16(a29)))), % 117.24/117.59 inference(scs_inference,[],[80,3312,2865,3126,2627,3335,3222,3227,1266,3269,3273,3254,3323,3075,1829,1038,2792,773,2909,1817,1122,85,117,137,419,136,96,126,3386,3389,152,151,149,147,158,165,139,157,141,143,178,145,138,144,150,312,292,2,175,174,173,3,185,177,20,25,16,15,18,183,159,180,2177,179])). % 117.24/117.59 cnf(3423,plain, % 117.24/117.59 (P13(f32(a4))), % 117.24/117.59 inference(scs_inference,[],[65,151,152])). % 117.24/117.59 cnf(3425,plain, % 117.24/117.59 (P4(f28(a4))), % 117.24/117.59 inference(scs_inference,[],[65,151,152,149])). % 117.24/117.59 cnf(3439,plain, % 117.24/117.59 (P6(f11(f28(a1)),f31(a1))), % 117.24/117.59 inference(scs_inference,[],[3356,777,1985,93,65,151,152,149,158,165,147,139,141,157,178])). % 117.24/117.59 cnf(3443,plain, % 117.24/117.59 (P7(f28(f11(x34431)))), % 117.24/117.59 inference(scs_inference,[],[3356,777,1985,93,65,151,152,149,158,165,147,139,141,157,178,143,144])). % 117.24/117.59 cnf(3449,plain, % 117.24/117.59 (P4(f32(a4))), % 117.24/117.59 inference(scs_inference,[],[3356,777,1985,93,65,151,152,149,158,165,147,139,141,157,178,143,144,138,145,150])). % 117.24/117.59 cnf(3453,plain, % 117.24/117.59 (~E(f28(a1),f30(a12))), % 117.24/117.59 inference(scs_inference,[],[2629,3356,3175,777,1985,93,65,151,152,149,158,165,147,139,141,157,178,143,144,138,145,150,312,292,2])). % 117.24/117.59 cnf(3455,plain, % 117.24/117.59 (P6(f15(x34551),x34551)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(3458,plain, % 117.24/117.59 (P6(f15(x34581),x34581)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(3460,plain, % 117.24/117.59 (P1(f15(a26))), % 117.24/117.59 inference(scs_inference,[],[2629,3356,3175,39,777,1985,93,65,126,3455,3458,151,152,149,158,165,147,139,141,157,178,143,144,138,145,150,312,292,2,175,174,173])). % 117.24/117.59 cnf(3461,plain, % 117.24/117.59 (P6(f15(x34611),x34611)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(3464,plain, % 117.24/117.59 (P9(f33(a1,a1))), % 117.24/117.59 inference(scs_inference,[],[2629,3402,3356,3175,3376,1049,39,2993,777,1985,93,65,126,3455,3458,151,152,149,158,165,147,139,141,157,178,143,144,138,145,150,312,292,2,175,174,173,3,24])). % 117.24/117.59 cnf(3466,plain, % 117.24/117.59 (P13(f33(a1,a1))), % 117.24/117.59 inference(scs_inference,[],[2629,3402,3356,3175,3243,3376,1049,2805,39,2993,777,1985,93,65,126,3455,3458,151,152,149,158,165,147,139,141,157,178,143,144,138,145,150,312,292,2,175,174,173,3,24,22])). % 117.24/117.59 cnf(3470,plain, % 117.24/117.59 (P4(f33(f32(a1),f32(a1)))), % 117.24/117.59 inference(scs_inference,[],[3190,2629,3402,3356,3101,3175,3243,3376,1049,2805,39,2993,777,1985,93,65,2538,126,3455,3458,3461,151,152,149,158,165,147,139,141,157,178,143,144,138,145,150,312,292,2,175,174,173,3,24,22,185,177])). % 117.24/117.59 cnf(3478,plain, % 117.24/117.59 (~P11(x34781,f33(f28(a5),f28(a5)))), % 117.24/117.59 inference(scs_inference,[],[3190,2629,3394,3402,2891,3356,3101,2877,3175,3243,3376,3231,3013,1049,2805,39,1079,2993,777,1985,93,65,127,2538,136,126,3455,3458,3461,151,152,149,158,165,147,139,141,157,178,143,144,138,145,150,312,292,2,175,174,173,3,24,22,185,177,20,25,15,18])). % 117.24/117.59 cnf(3481,plain, % 117.24/117.59 (~P6(f31(a23),f31(f32(a1)))), % 117.24/117.59 inference(scs_inference,[],[3190,2629,3399,3394,3402,2891,3356,3101,2877,3175,3243,3376,3231,91,3013,1049,2805,39,1079,2993,777,1985,93,65,127,2538,136,126,3455,3458,3461,151,152,149,158,165,147,139,141,157,178,143,144,138,145,150,312,292,2,175,174,173,3,24,22,185,177,20,25,15,18,160,184])). % 117.24/117.59 cnf(3483,plain, % 117.24/117.59 (~P6(f31(a23),f31(a1))), % 117.24/117.59 inference(scs_inference,[],[3190,2629,3399,3394,3402,2891,3356,3101,2877,3175,3243,3376,3231,91,3013,1049,2805,2702,39,1079,2993,777,1985,93,65,127,2538,136,126,3455,3458,3461,151,152,149,158,165,147,139,141,157,178,143,144,138,145,150,312,292,2,175,174,173,3,24,22,185,177,20,25,15,18,160,184,16])). % 117.24/117.59 cnf(3491,plain, % 117.24/117.59 (P4(f28(f28(a4)))), % 117.24/117.59 inference(scs_inference,[],[3425,152,151,149])). % 117.24/117.59 cnf(3497,plain, % 117.24/117.59 (~P4(f16(a23))), % 117.24/117.59 inference(scs_inference,[],[3425,3470,131,84,152,151,149,146,165,158])). % 117.24/117.59 cnf(3499,plain, % 117.24/117.59 (P7(f16(a13))), % 117.24/117.59 inference(scs_inference,[],[3425,3470,131,135,84,152,151,149,146,165,158,147])). % 117.24/117.59 cnf(3501,plain, % 117.24/117.59 (P1(f28(a4))), % 117.24/117.59 inference(scs_inference,[],[3425,3470,131,135,84,152,151,149,146,165,158,147,139])). % 117.24/117.59 cnf(3503,plain, % 117.24/117.59 (~P4(f30(a23))), % 117.24/117.59 inference(scs_inference,[],[3425,3470,131,135,84,152,151,149,146,165,158,147,139,157])). % 117.24/117.59 cnf(3507,plain, % 117.24/117.59 (P6(x35071,f31(x35071))), % 117.24/117.59 inference(scs_inference,[],[3425,3470,131,135,84,125,152,151,149,146,165,158,147,139,157,141,178])). % 117.24/117.59 cnf(3513,plain, % 117.24/117.59 (P7(f28(a4))), % 117.24/117.59 inference(scs_inference,[],[3425,3470,131,135,84,125,152,151,149,146,165,158,147,139,157,141,178,143,145,144])). % 117.24/117.59 cnf(3515,plain, % 117.24/117.59 (E(f28(a4),a1)), % 117.24/117.59 inference(scs_inference,[],[3425,3470,131,135,84,125,152,151,149,146,165,158,147,139,157,141,178,143,145,144,138])). % 117.24/117.59 cnf(3517,plain, % 117.24/117.59 (P4(f32(f28(a4)))), % 117.24/117.59 inference(scs_inference,[],[3425,3470,131,135,84,125,152,151,149,146,165,158,147,139,157,141,178,143,145,144,138,150])). % 117.24/117.59 cnf(3522,plain, % 117.24/117.59 (E(f31(f28(a4)),f31(a1))), % 117.24/117.59 inference(scs_inference,[],[3425,3470,131,135,84,125,152,151,149,146,165,158,147,139,157,141,178,143,145,144,138,150,8,4,12,7])). % 117.24/117.59 cnf(3532,plain, % 117.24/117.59 (P6(f15(x35321),x35321)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(3535,plain, % 117.24/117.59 (P6(f15(x35351),x35351)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(3544,plain, % 117.24/117.59 (P11(f16(a23),f31(a23))), % 117.24/117.59 inference(scs_inference,[],[2881,2568,2644,3425,3460,3483,3470,3256,3221,3010,131,135,84,125,137,126,3532,3535,152,151,149,146,165,158,147,139,157,141,178,143,145,144,138,150,8,4,12,7,10,13,11,9,5,312,292,2,175,174,173,3,185,177])). % 117.24/117.59 cnf(3547,plain, % 117.24/117.59 (~P6(f31(x35471),f31(f28(a4)))), % 117.24/117.59 inference(scs_inference,[],[2881,2568,2644,3425,3460,3483,3470,3256,3221,1921,3010,131,135,84,125,137,126,3532,3535,152,151,149,146,165,158,147,139,157,141,178,143,145,144,138,150,8,4,12,7,10,13,11,9,5,312,292,2,175,174,173,3,185,177,184])). % 117.24/117.59 cnf(3549,plain, % 117.24/117.59 (~E(f28(a4),f16(f30(a12)))), % 117.24/117.59 inference(scs_inference,[],[2881,2568,2644,3425,3460,3483,3470,2948,3256,3221,1921,3010,131,135,84,125,137,126,3532,3535,152,151,149,146,165,158,147,139,157,141,178,143,145,144,138,150,8,4,12,7,10,13,11,9,5,312,292,2,175,174,173,3,185,177,184,20])). % 117.24/117.59 cnf(3551,plain, % 117.24/117.59 (~P6(f31(a23),f31(f28(a1)))), % 117.24/117.59 inference(scs_inference,[],[2881,2568,2644,3425,3460,3483,3134,3470,2948,3256,3221,2992,1921,3010,131,135,84,125,137,136,126,3532,3535,152,151,149,146,165,158,147,139,157,141,178,143,145,144,138,150,8,4,12,7,10,13,11,9,5,312,292,2,175,174,173,3,185,177,184,20,25,16])). % 117.24/117.59 cnf(3557,plain, % 117.24/117.59 (~P11(f31(a23),f16(a23))), % 117.24/117.59 inference(scs_inference,[],[80,2881,2568,2644,3425,3460,3483,2887,783,3134,3470,2948,3256,3221,2992,1921,814,3010,3249,131,135,84,125,137,136,96,126,3532,3535,152,151,149,146,165,158,147,139,157,141,178,143,145,144,138,150,8,4,12,7,10,13,11,9,5,312,292,2,175,174,173,3,185,177,184,20,25,16,15,18,183,6,180])). % 117.24/117.59 cnf(3567,plain, % 117.24/117.59 (P4(f28(f32(a4)))), % 117.24/117.59 inference(scs_inference,[],[3449,151,152,149])). % 117.24/117.59 cnf(3579,plain, % 117.24/117.59 (P1(f32(a4))), % 117.24/117.59 inference(scs_inference,[],[3449,3497,89,151,152,149,165,158,147,157,141,139])). % 117.24/117.59 cnf(3583,plain, % 117.24/117.59 (P7(f32(a4))), % 117.24/117.59 inference(scs_inference,[],[3449,3497,89,151,152,149,165,158,147,157,141,139,143,144])). % 117.24/117.59 cnf(3585,plain, % 117.24/117.59 (E(f32(a4),a1)), % 117.24/117.59 inference(scs_inference,[],[3449,3497,89,151,152,149,165,158,147,157,141,139,143,144,138])). % 117.24/117.59 cnf(3587,plain, % 117.24/117.59 (P8(f32(a4))), % 117.24/117.59 inference(scs_inference,[],[3449,3497,89,151,152,149,165,158,147,157,141,139,143,144,138,145])). % 117.24/117.59 cnf(3590,plain, % 117.24/117.59 (P4(f32(f32(a4)))), % 117.24/117.59 inference(scs_inference,[],[3449,3497,89,151,152,149,165,158,147,157,141,139,143,144,138,145,6,150])). % 117.24/117.59 cnf(3605,plain, % 117.24/117.59 (P6(f15(x36051),x36051)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(3608,plain, % 117.24/117.59 (P6(f15(x36081),x36081)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(3614,plain, % 117.24/117.59 (~P6(f31(a23),f30(a23))), % 117.24/117.59 inference(scs_inference,[],[3414,2646,3449,3497,3501,3503,3515,3547,3549,89,126,3605,3608,151,152,149,165,158,147,157,141,139,143,144,138,145,6,150,8,4,12,7,13,11,9,10,5,312,292,2,175,174,173,3,177])). % 117.24/117.59 cnf(3616,plain, % 117.24/117.59 (~P6(f31(a23),f31(f32(a4)))), % 117.24/117.59 inference(scs_inference,[],[3414,2646,3449,3497,3501,3503,3544,3515,3547,3549,89,126,3605,3608,151,152,149,165,158,147,157,141,139,143,144,138,145,6,150,8,4,12,7,13,11,9,10,5,312,292,2,175,174,173,3,177,184])). % 117.24/117.59 cnf(3618,plain, % 117.24/117.59 (~E(f16(a13),f32(a21))), % 117.24/117.59 inference(scs_inference,[],[3414,2646,3449,3497,3499,3501,3503,3544,3515,3547,3549,89,136,126,3605,3608,151,152,149,165,158,147,157,141,139,143,144,138,145,6,150,8,4,12,7,13,11,9,10,5,312,292,2,175,174,173,3,177,184,25])). % 117.24/117.59 cnf(3619,plain, % 117.24/117.59 (~E(f32(a4),f16(a23))), % 117.24/117.59 inference(scs_inference,[],[3414,2646,3449,3497,3499,3501,3503,3544,3515,3547,3549,89,136,126,3605,3608,151,152,149,165,158,147,157,141,139,143,144,138,145,6,150,8,4,12,7,13,11,9,10,5,312,292,2,175,174,173,3,177,184,25,20])). % 117.24/117.59 cnf(3620,plain, % 117.24/117.59 (~P6(f32(a21),f31(f16(a13)))), % 117.24/117.59 inference(scs_inference,[],[3414,2646,3449,3497,3499,3501,3503,3544,3515,3547,3549,89,136,126,3605,3608,151,152,149,165,158,147,157,141,139,143,144,138,145,6,150,8,4,12,7,13,11,9,10,5,312,292,2,175,174,173,3,177,184,25,20,179])). % 117.24/117.59 cnf(3624,plain, % 117.24/117.59 (~P11(x36241,f28(a4))), % 117.24/117.59 inference(scs_inference,[],[3507,3414,2646,3449,3497,3499,3501,3503,3544,3515,3547,3330,3549,89,190,136,126,3605,3608,151,152,149,165,158,147,157,141,139,143,144,138,145,6,150,8,4,12,7,13,11,9,10,5,312,292,2,175,174,173,3,177,184,25,20,179,16,18])). % 117.24/117.59 cnf(3628,plain, % 117.24/117.59 (P3(f33(f28(a1),f28(a1)))), % 117.24/117.59 inference(scs_inference,[],[80,3507,3342,3414,2646,3449,3497,3499,3501,3503,3544,3515,3547,3330,3549,2995,89,190,136,96,126,3605,3608,151,152,149,165,158,147,157,141,139,143,144,138,145,6,150,8,4,12,7,13,11,9,10,5,312,292,2,175,174,173,3,177,184,25,20,179,16,18,183,213,21])). % 117.24/117.59 cnf(3633,plain, % 117.24/117.59 (P4(f28(a6))), % 117.24/117.59 inference(scs_inference,[],[66,149])). % 117.24/117.59 cnf(3639,plain, % 117.24/117.59 (E(f33(a19,f28(a19)),f32(a19))), % 117.24/117.59 inference(scs_inference,[],[94,66,64,149,152,151,165])). % 117.24/117.59 cnf(3647,plain, % 117.24/117.59 (P1(f28(f32(a4)))), % 117.24/117.59 inference(scs_inference,[],[3567,3503,94,66,64,149,152,151,165,158,147,157,139])). % 117.24/117.59 cnf(3657,plain, % 117.24/117.59 (E(f28(f32(a4)),a1)), % 117.24/117.59 inference(scs_inference,[],[3567,3503,94,66,64,149,152,151,165,158,147,157,139,141,143,144,145,138])). % 117.24/117.59 cnf(3659,plain, % 117.24/117.59 (P4(f32(a6))), % 117.24/117.59 inference(scs_inference,[],[3567,3503,94,66,64,149,152,151,165,158,147,157,139,141,143,144,145,138,150])). % 117.24/117.59 cnf(3665,plain, % 117.24/117.59 (P6(f15(x36651),x36651)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(3668,plain, % 117.24/117.59 (P6(f15(x36681),x36681)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(3671,plain, % 117.24/117.59 (P6(f15(x36711),x36711)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(3675,plain, % 117.24/117.59 (P2(f33(f32(a1),f32(a1)))), % 117.24/117.59 inference(scs_inference,[],[3344,2633,3579,3567,1041,3327,2825,3503,2909,94,66,64,126,3665,3668,149,152,151,165,158,147,157,139,141,143,144,145,138,150,312,292,2,175,174,173,26,23])). % 117.24/117.59 cnf(3677,plain, % 117.24/117.59 (P11(f16(a12),f31(a12))), % 117.24/117.59 inference(scs_inference,[],[2962,2740,3344,2633,3579,3567,1041,3327,2825,3503,2711,2909,94,66,137,64,126,3665,3668,149,152,151,165,158,147,157,139,141,143,144,145,138,150,312,292,2,175,174,173,26,23,3,177])). % 117.24/117.59 cnf(3680,plain, % 117.24/117.59 (~E(f28(a4),f32(a21))), % 117.24/117.59 inference(scs_inference,[],[2962,2740,3344,2633,3513,3579,3567,1041,3327,2825,3503,2711,2909,94,66,137,136,64,126,3665,3668,149,152,151,165,158,147,157,139,141,143,144,145,138,150,312,292,2,175,174,173,26,23,3,177,25])). % 117.24/117.59 cnf(3681,plain, % 117.24/117.59 (~E(f28(f32(a4)),f30(a23))), % 117.24/117.59 inference(scs_inference,[],[2962,2740,3344,2633,3513,3579,3567,1041,3327,2825,3503,2711,2909,94,66,137,136,64,126,3665,3668,149,152,151,165,158,147,157,139,141,143,144,145,138,150,312,292,2,175,174,173,26,23,3,177,25,20])). % 117.24/117.59 cnf(3682,plain, % 117.24/117.59 (~P6(f32(a21),f31(f28(a4)))), % 117.24/117.59 inference(scs_inference,[],[2962,2740,3344,2633,3513,3579,3567,1041,3327,2825,3503,2711,2909,94,66,137,136,64,126,3665,3668,149,152,151,165,158,147,157,139,141,143,144,145,138,150,312,292,2,175,174,173,26,23,3,177,25,20,179])). % 117.24/117.59 cnf(3691,plain, % 117.24/117.59 (~E(f31(x36911),f28(a4))), % 117.24/117.59 inference(scs_inference,[],[2962,2740,3344,3624,2633,3333,3513,3579,3585,3362,3628,2998,3567,1041,3327,2825,2900,1278,3503,2711,2909,94,125,66,137,136,64,126,3665,3668,3671,149,152,151,165,158,147,157,139,141,143,144,145,138,150,312,292,2,175,174,173,26,23,3,177,25,20,179,153,16,15,30,18])). % 117.24/117.59 cnf(3695,plain, % 117.24/117.59 (~P11(f31(a12),f16(a12))), % 117.24/117.59 inference(scs_inference,[],[2962,2740,3344,3624,2633,3333,3423,3513,3579,3587,3585,3362,3628,2998,3567,1041,3327,2825,2900,1278,3503,2711,2909,94,125,66,137,136,64,126,3665,3668,3671,149,152,151,165,158,147,157,139,141,143,144,145,138,150,312,292,2,175,174,173,26,23,3,177,25,20,179,153,16,15,30,18,183,180])). % 117.24/117.59 cnf(3704,plain, % 117.24/117.59 (P4(f28(f28(a6)))), % 117.24/117.59 inference(scs_inference,[],[3633,151,152,149])). % 117.24/117.59 cnf(3708,plain, % 117.24/117.59 (~P4(f16(a12))), % 117.24/117.59 inference(scs_inference,[],[3633,134,95,151,152,149,165,158])). % 117.24/117.59 cnf(3710,plain, % 117.24/117.59 (~P4(f30(a3))), % 117.24/117.59 inference(scs_inference,[],[3633,134,132,95,151,152,149,165,158,157])). % 117.24/117.59 cnf(3712,plain, % 117.24/117.59 (P7(f16(a3))), % 117.24/117.59 inference(scs_inference,[],[3633,134,132,95,151,152,149,165,158,157,147])). % 117.24/117.59 cnf(3714,plain, % 117.24/117.59 (P1(f28(a6))), % 117.24/117.59 inference(scs_inference,[],[3633,134,132,95,151,152,149,165,158,157,147,139])). % 117.24/117.59 cnf(3720,plain, % 117.24/117.59 (P7(f28(a6))), % 117.24/117.59 inference(scs_inference,[],[3633,134,132,95,151,152,149,165,158,157,147,139,141,143,144])). % 117.24/117.59 cnf(3722,plain, % 117.24/117.59 (E(f28(a6),a1)), % 117.24/117.59 inference(scs_inference,[],[3633,134,132,95,151,152,149,165,158,157,147,139,141,143,144,138])). % 117.24/117.59 cnf(3727,plain, % 117.24/117.59 (P4(f32(f28(a6)))), % 117.24/117.59 inference(scs_inference,[],[3633,134,132,95,151,152,149,165,158,157,147,139,141,143,144,138,6,145,150])). % 117.24/117.59 cnf(3729,plain, % 117.24/117.59 (E(f28(f28(a6)),f28(a1))), % 117.24/117.59 inference(scs_inference,[],[3633,134,132,95,151,152,149,165,158,157,147,139,141,143,144,138,6,145,150,4])). % 117.24/117.59 cnf(3732,plain, % 117.24/117.59 (E(f31(f28(a6)),f31(a1))), % 117.24/117.59 inference(scs_inference,[],[3633,134,132,95,151,152,149,165,158,157,147,139,141,143,144,138,6,145,150,4,8,12,7])). % 117.24/117.59 cnf(3733,plain, % 117.24/117.59 (E(f15(f28(a6)),f15(a1))), % 117.24/117.59 inference(scs_inference,[],[3633,134,132,95,151,152,149,165,158,157,147,139,141,143,144,138,6,145,150,4,8,12,7,13])). % 117.24/117.59 cnf(3740,plain, % 117.24/117.59 (~E(f28(a4),f31(x37401))), % 117.24/117.59 inference(scs_inference,[],[3691,3633,3417,134,132,95,151,152,149,165,158,157,147,139,141,143,144,138,6,145,150,4,8,12,7,13,9,10,11,5,312,292,2])). % 117.24/117.59 cnf(3742,plain, % 117.24/117.59 (P6(f15(x37421),x37421)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(3745,plain, % 117.24/117.59 (P6(f15(x37451),x37451)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(3747,plain, % 117.24/117.59 (P1(f15(a13))), % 117.24/117.59 inference(scs_inference,[],[3691,3633,3417,43,134,132,95,126,3742,3745,151,152,149,165,158,157,147,139,141,143,144,138,6,145,150,4,8,12,7,13,9,10,11,5,312,292,2,175,174,173])). % 117.24/117.59 cnf(3750,plain, % 117.24/117.59 (P1(f33(f32(a1),f28(a1)))), % 117.24/117.59 inference(scs_inference,[],[3691,3633,3417,43,1043,2709,134,132,95,126,3742,3745,151,152,149,165,158,157,147,139,141,143,144,138,6,145,150,4,8,12,7,13,9,10,11,5,312,292,2,175,174,173,14])). % 117.24/117.59 cnf(3751,plain, % 117.24/117.59 (E(f33(a1,x37511),f33(f32(a1),x37511))), % 117.24/117.59 inference(rename_variables,[],[2709])). % 117.24/117.59 cnf(3758,plain, % 117.24/117.59 (~P6(f31(a12),f31(f28(a6)))), % 117.24/117.59 inference(scs_inference,[],[3557,3691,1989,3633,3677,3681,3417,3657,43,1043,2910,2709,3751,1047,134,3497,132,95,126,3742,3745,151,152,149,165,158,157,147,139,141,143,144,138,6,145,150,4,8,12,7,13,9,10,11,5,312,292,2,175,174,173,14,19,29,3,177,184])). % 117.24/117.59 cnf(3760,plain, % 117.24/117.59 (~E(f32(a4),f32(a21))), % 117.24/117.59 inference(scs_inference,[],[3557,3691,1989,3583,3633,3677,3681,3417,3657,43,1043,2910,2709,3751,1047,134,3497,132,95,136,126,3742,3745,151,152,149,165,158,157,147,139,141,143,144,138,6,145,150,4,8,12,7,13,9,10,11,5,312,292,2,175,174,173,14,19,29,3,177,184,25])). % 117.24/117.59 cnf(3764,plain, % 117.24/117.59 (~P6(f32(a21),f31(f32(a4)))), % 117.24/117.59 inference(scs_inference,[],[3557,3691,1989,3583,3633,3677,3681,2964,3647,3417,3657,43,1043,2910,2709,3751,1047,134,3497,132,3567,95,136,126,3742,3745,151,152,149,165,158,157,147,139,141,143,144,138,6,145,150,4,8,12,7,13,9,10,11,5,312,292,2,175,174,173,14,19,29,3,177,184,25,156,20,179])). % 117.24/117.59 cnf(3767,plain, % 117.24/117.59 (P6(x37671,f31(x37671))), % 117.24/117.59 inference(rename_variables,[],[3507])). % 117.24/117.59 cnf(3768,plain, % 117.24/117.59 (~E(f16(a29),f32(a21))), % 117.24/117.59 inference(scs_inference,[],[3557,3691,1989,3583,3633,3677,3681,2964,3647,3417,3095,3657,3507,3767,43,1043,2910,2709,3751,1047,134,3497,132,3567,95,136,126,3742,3745,151,152,149,165,158,157,147,139,141,143,144,138,6,145,150,4,8,12,7,13,9,10,11,5,312,292,2,175,174,173,14,19,29,3,177,184,25,156,20,179,16,15])). % 117.24/117.59 cnf(3783,plain, % 117.24/117.59 (P4(f28(f32(a6)))), % 117.24/117.59 inference(scs_inference,[],[3750,3659,140,149])). % 117.24/117.59 cnf(3789,plain, % 117.24/117.59 (E(f33(a21,f28(a21)),f32(a21))), % 117.24/117.59 inference(scs_inference,[],[3750,3659,96,140,149,146,152,165])). % 117.24/117.59 cnf(3807,plain, % 117.24/117.59 (P4(f32(f32(a6)))), % 117.24/117.59 inference(scs_inference,[],[3708,3750,3704,3659,96,140,149,146,152,165,158,147,141,139,157,144,143,145,150])). % 117.24/117.59 cnf(3815,plain, % 117.24/117.59 (P6(f15(x38151),x38151)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(3818,plain, % 117.24/117.59 (P6(f15(x38181),x38181)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(3821,plain, % 117.24/117.59 (P6(f15(x38211),x38211)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(3824,plain, % 117.24/117.59 (P6(f15(f16(a2)),a2)), % 117.24/117.59 inference(scs_inference,[],[2738,2635,3708,3714,3750,3704,3481,3551,3659,2787,2895,778,96,126,3815,3818,140,149,146,152,165,158,147,141,139,157,144,143,145,150,138,312,292,2,175,174,173,3,185])). % 117.24/117.59 cnf(3826,plain, % 117.24/117.59 (P11(f30(a13),f31(a13))), % 117.24/117.59 inference(scs_inference,[],[3032,2738,2635,3708,3714,3750,3704,3481,3551,3659,2787,2895,137,778,96,126,3815,3818,140,149,146,152,165,158,147,141,139,157,144,143,145,150,138,312,292,2,175,174,173,3,185,177])). % 117.24/117.59 cnf(3831,plain, % 117.24/117.59 (~E(f16(a3),f32(a21))), % 117.24/117.59 inference(scs_inference,[],[3032,2738,2635,3708,3712,3714,3750,3704,3481,3551,3659,819,2787,2895,137,778,136,96,126,3815,3818,140,149,146,152,165,158,147,141,139,157,144,143,145,150,138,312,292,2,175,174,173,3,185,177,184,25])). % 117.24/117.59 cnf(3832,plain, % 117.24/117.59 (~E(f28(f28(a6)),f16(a12))), % 117.24/117.59 inference(scs_inference,[],[3032,2738,2635,3708,3712,3714,3750,3704,3481,3551,3659,819,2787,2895,137,778,136,96,126,3815,3818,140,149,146,152,165,158,147,141,139,157,144,143,145,150,138,312,292,2,175,174,173,3,185,177,184,25,20])). % 117.24/117.59 cnf(3833,plain, % 117.24/117.59 (~P6(f32(a21),f31(f16(a3)))), % 117.24/117.59 inference(scs_inference,[],[3032,2738,2635,3708,3712,3714,3750,3704,3481,3551,3659,819,2787,2895,137,778,136,96,126,3815,3818,140,149,146,152,165,158,147,141,139,157,144,143,145,150,138,312,292,2,175,174,173,3,185,177,184,25,20,179])). % 117.24/117.59 cnf(3845,plain, % 117.24/117.59 (~P11(f31(a13),f30(a13))), % 117.24/117.59 inference(scs_inference,[],[80,3032,2738,2635,3708,3712,3714,3722,2771,2901,2663,3750,3704,3481,3551,3659,819,2787,2895,3092,1835,2775,137,778,136,96,126,3815,3818,3821,140,149,146,152,165,158,147,141,139,157,144,143,145,150,138,312,292,2,175,174,173,3,185,177,184,25,20,179,15,16,18,183,159,180])). % 117.24/117.59 cnf(3853,plain, % 117.24/117.59 (P4(f28(a27))), % 117.24/117.59 inference(scs_inference,[],[64,149])). % 117.24/117.59 cnf(3871,plain, % 117.24/117.59 (P4(f32(a27))), % 117.24/117.59 inference(scs_inference,[],[3710,3727,64,149,152,147,158,139,141,157,144,143,150])). % 117.24/117.59 cnf(3881,plain, % 117.24/117.59 (P6(f15(x38811),x38811)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(3884,plain, % 117.24/117.59 (P6(f15(x38841),x38841)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(3889,plain, % 117.24/117.59 (~E(f28(a1),f16(a12))), % 117.24/117.59 inference(scs_inference,[],[2637,3710,3729,3832,3727,3616,3747,64,126,3881,3884,149,152,147,158,139,141,157,144,143,150,145,138,312,292,2,175,174,173,3])). % 117.24/117.59 cnf(3891,plain, % 117.24/117.59 (~P11(f31(a23),f31(f32(a4)))), % 117.24/117.59 inference(scs_inference,[],[2637,3710,3729,3832,3727,3616,1082,3747,3507,2714,64,126,3881,3884,149,152,147,158,139,141,157,144,143,150,145,138,312,292,2,175,174,173,3,24,185])). % 117.24/117.59 cnf(3892,plain, % 117.24/117.59 (P6(x38921,f31(x38921))), % 117.24/117.59 inference(rename_variables,[],[3507])). % 117.24/117.59 cnf(3894,plain, % 117.24/117.59 (~P6(f31(a12),f16(a12))), % 117.24/117.59 inference(scs_inference,[],[3695,2637,3710,3729,3832,3727,3616,1082,3747,3507,2714,3708,64,126,3881,3884,149,152,147,158,139,141,157,144,143,150,145,138,312,292,2,175,174,173,3,24,185,177])). % 117.24/117.59 cnf(3896,plain, % 117.24/117.59 (~E(f28(a6),f32(a21))), % 117.24/117.59 inference(scs_inference,[],[3695,2637,3710,3720,3729,3832,3727,3616,1082,3747,3507,2714,3708,64,136,126,3881,3884,149,152,147,158,139,141,157,144,143,150,145,138,312,292,2,175,174,173,3,24,185,177,25])). % 117.24/117.59 cnf(3898,plain, % 117.24/117.59 (~P6(f32(a21),f31(f28(a6)))), % 117.24/117.59 inference(scs_inference,[],[3695,2637,3710,3720,3729,3832,3727,3616,1082,3747,3507,2714,3708,64,136,126,3881,3884,149,152,147,158,139,141,157,144,143,150,145,138,312,292,2,175,174,173,3,24,185,177,25,20,179])). % 117.24/117.59 cnf(3900,plain, % 117.24/117.59 (~E(f32(a4),f31(a23))), % 117.24/117.59 inference(scs_inference,[],[3695,2637,3710,3720,3729,3832,3727,3616,1082,3747,3507,3892,2714,3708,64,136,126,3881,3884,149,152,147,158,139,141,157,144,143,150,145,138,312,292,2,175,174,173,3,24,185,177,25,20,179,15])). % 117.24/117.59 cnf(3921,plain, % 117.24/117.59 (P4(f28(f28(a27)))), % 117.24/117.59 inference(scs_inference,[],[3853,3871,151,152,149])). % 117.24/117.59 cnf(3925,plain, % 117.24/117.59 (P1(f28(a27))), % 117.24/117.59 inference(scs_inference,[],[3853,3871,1226,151,152,149,147,139])). % 117.24/117.59 cnf(3929,plain, % 117.24/117.59 (~P4(f30(a13))), % 117.24/117.59 inference(scs_inference,[],[3853,3871,135,1226,151,152,149,147,139,141,157])). % 117.24/117.59 cnf(3931,plain, % 117.24/117.59 (~P4(f16(a13))), % 117.24/117.59 inference(scs_inference,[],[3853,3871,135,1226,151,152,149,147,139,141,157,158])). % 117.24/117.59 cnf(3933,plain, % 117.24/117.59 (P7(f28(a27))), % 117.24/117.59 inference(scs_inference,[],[3853,3871,135,1226,151,152,149,147,139,141,157,158,144])). % 117.24/117.59 cnf(3939,plain, % 117.24/117.59 (P4(f32(f28(a27)))), % 117.24/117.59 inference(scs_inference,[],[3853,3871,135,1226,151,152,149,147,139,141,157,158,144,143,145,150])). % 117.24/117.59 cnf(3941,plain, % 117.24/117.59 (E(f28(a27),a1)), % 117.24/117.59 inference(scs_inference,[],[3853,3871,135,1226,151,152,149,147,139,141,157,158,144,143,145,150,138])). % 117.24/117.59 cnf(3945,plain, % 117.24/117.59 (E(f33(x39451,f28(a27)),f33(x39451,a1))), % 117.24/117.59 inference(scs_inference,[],[3853,3871,135,1226,151,152,149,147,139,141,157,158,144,143,145,150,138,8,4,12])). % 117.24/117.59 cnf(3946,plain, % 117.24/117.59 (E(f31(f28(a27)),f31(a1))), % 117.24/117.59 inference(scs_inference,[],[3853,3871,135,1226,151,152,149,147,139,141,157,158,144,143,145,150,138,8,4,12,7])). % 117.24/117.59 cnf(3962,plain, % 117.24/117.59 (P11(f16(a13),f31(a13))), % 117.24/117.59 inference(scs_inference,[],[3042,2747,2639,3853,3871,3620,3824,2895,135,37,1226,137,151,152,149,147,139,141,157,158,144,143,145,150,138,8,4,12,7,9,13,11,10,5,312,292,2,174,175,173,3,177])). % 117.24/117.59 cnf(3965,plain, % 117.24/117.59 (~P6(f31(a13),f31(f28(a27)))), % 117.24/117.59 inference(scs_inference,[],[3042,2747,2639,3853,3871,3620,3824,3826,2895,135,37,1226,137,151,152,149,147,139,141,157,158,144,143,145,150,138,8,4,12,7,9,13,11,10,5,312,292,2,174,175,173,3,177,184])). % 117.24/117.59 cnf(3968,plain, % 117.24/117.59 (~E(f28(a27),f16(f30(a2)))), % 117.24/117.59 inference(scs_inference,[],[3042,2747,2639,3853,3871,3443,3036,3620,3824,3826,2895,135,37,1226,137,136,151,152,149,147,139,141,157,158,144,143,145,150,138,8,4,12,7,9,13,11,10,5,312,292,2,174,175,173,3,177,184,25,20])). % 117.24/117.59 cnf(3969,plain, % 117.24/117.59 (~P6(f32(a21),f31(f11(a23)))), % 117.24/117.59 inference(scs_inference,[],[3042,2747,2639,3853,3871,3443,3036,3620,3824,3826,1195,2895,135,37,1226,137,136,151,152,149,147,139,141,157,158,144,143,145,150,138,8,4,12,7,9,13,11,10,5,312,292,2,174,175,173,3,177,184,25,20,179])). % 117.24/117.59 cnf(3971,plain, % 117.24/117.59 (~E(f28(a1),f31(a23))), % 117.24/117.59 inference(scs_inference,[],[3042,2747,2639,3853,3871,3443,3036,3620,3891,3824,3826,1195,2921,2895,135,37,1226,137,136,151,152,149,147,139,141,157,158,144,143,145,150,138,8,4,12,7,9,13,11,10,5,312,292,2,174,175,173,3,177,184,25,20,179,17])). % 117.24/117.59 cnf(3973,plain, % 117.24/117.59 (P6(f28(f32(a1)),f31(x39731))), % 117.24/117.59 inference(scs_inference,[],[3042,2747,2639,3853,3871,3443,3036,3620,3891,3824,3826,1195,2921,2792,2711,2895,135,37,1226,137,136,151,152,149,147,139,141,157,158,144,143,145,150,138,8,4,12,7,9,13,11,10,5,312,292,2,174,175,173,3,177,184,25,20,179,17,15])). % 117.24/117.59 cnf(3974,plain, % 117.24/117.59 (~P6(f31(a23),f31(f28(a6)))), % 117.24/117.59 inference(scs_inference,[],[3042,2747,2639,3853,3871,3732,3443,3036,3620,3891,3824,3826,1195,2921,2792,2711,2895,3483,135,37,1226,137,136,151,152,149,147,139,141,157,158,144,143,145,150,138,8,4,12,7,9,13,11,10,5,312,292,2,174,175,173,3,177,184,25,20,179,17,15,16])). % 117.24/117.59 cnf(3987,plain, % 117.24/117.59 (P4(f28(f32(a27)))), % 117.24/117.59 inference(scs_inference,[],[3871,149])). % 117.24/117.59 cnf(4007,plain, % 117.24/117.59 (P4(f32(f32(a27)))), % 117.24/117.59 inference(scs_inference,[],[3929,3921,3871,149,139,141,147,157,158,144,145,138,143,150])). % 117.24/117.59 cnf(4013,plain, % 117.24/117.59 (P6(f15(x40131),x40131)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(4016,plain, % 117.24/117.59 (P6(f15(x40161),x40161)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(4028,plain, % 117.24/117.59 (~P6(f32(a21),f31(f28(a27)))), % 117.24/117.59 inference(scs_inference,[],[3845,2641,3925,3929,3933,3962,3941,3921,3682,3968,3871,136,126,4013,4016,149,139,141,147,157,158,144,145,138,143,150,312,292,2,174,175,173,3,177,184,25,20,179])). % 117.24/117.59 cnf(4034,plain, % 117.24/117.59 (~P11(x40341,f28(a27))), % 117.24/117.59 inference(scs_inference,[],[3845,2641,3925,3929,3933,3962,3941,3973,3921,3682,3758,3968,3894,3871,3507,190,136,126,4013,4016,149,139,141,147,157,158,144,145,138,143,150,312,292,2,174,175,173,3,177,184,25,20,179,15,16,18])). % 117.24/117.59 cnf(4074,plain, % 117.24/117.59 (P1(f33(f32(a1),a1))), % 117.24/117.59 inference(scs_inference,[],[3198,2926,1071,2739,3931,1751,3675,3348,3987,3764,2810,2910,2714,137,136,147,141,139,158,157,144,145,138,143,312,292,2,26,23,3,177,25,20,153])). % 117.24/117.59 cnf(4078,plain, % 117.24/117.59 (P6(f33(f32(a1),a1),a29)), % 117.24/117.59 inference(scs_inference,[],[3198,2926,1071,2739,3931,1751,3675,3348,3987,3764,1377,2839,2810,2993,2910,2714,137,136,147,141,139,158,157,144,145,138,143,312,292,2,26,23,3,177,25,20,153,179,15])). % 117.24/117.59 cnf(4080,plain, % 117.24/117.59 (~P6(f31(a23),f31(f28(a27)))), % 117.24/117.59 inference(scs_inference,[],[3198,2926,1071,2739,3931,3946,1751,3675,3348,3987,3764,1377,2839,2810,2993,2910,2714,3483,137,136,147,141,139,158,157,144,145,138,143,312,292,2,26,23,3,177,25,20,153,179,15,16])). % 117.24/117.59 cnf(4085,plain, % 117.24/117.59 (~P11(f31(a10),f16(a10))), % 117.24/117.59 inference(scs_inference,[],[3198,2926,4034,1071,2739,3931,3639,3946,1751,3675,3348,3987,3764,1377,2839,3962,2810,2993,2910,2714,3483,125,137,136,147,141,139,158,157,144,145,138,143,312,292,2,26,23,3,177,25,20,153,179,15,16,30,18,180])). % 117.24/117.59 cnf(4096,plain, % 117.24/117.59 (P7(f16(f31(x40961)))), % 117.24/117.59 inference(scs_inference,[],[137,147])). % 117.24/117.59 cnf(4098,plain, % 117.24/117.59 (~P4(f16(a10))), % 117.24/117.59 inference(scs_inference,[],[133,137,147,158])). % 117.24/117.59 cnf(4110,plain, % 117.24/117.59 (E(f32(f32(a27)),a1)), % 117.24/117.59 inference(scs_inference,[],[4007,133,1226,137,147,158,139,141,157,145,144,138])). % 117.24/117.59 cnf(4157,plain, % 117.24/117.59 (E(f32(f28(a27)),a1)), % 117.24/117.59 inference(scs_inference,[],[4098,3939,147,139,141,158,157,145,138])). % 117.24/117.59 cnf(4167,plain, % 117.24/117.59 (P11(f11(f32(a1)),f31(a1))), % 117.24/117.59 inference(scs_inference,[],[3740,2917,4098,2972,3833,3939,3515,137,147,139,141,158,157,145,138,144,143,312,292,2,3,177])). % 117.24/117.59 cnf(4172,plain, % 117.24/117.59 (~E(f32(f28(a27)),f16(a10))), % 117.24/117.59 inference(scs_inference,[],[3740,2917,4098,2972,3833,4078,4074,3939,3515,137,147,139,141,158,157,145,138,144,143,312,292,2,3,177,168,20])). % 117.24/117.59 cnf(4174,plain, % 117.24/117.59 (P6(f33(f32(a1),f32(a1)),a29)), % 117.24/117.59 inference(scs_inference,[],[3740,2917,4098,2972,4096,3833,4078,4074,3939,2710,3515,137,136,147,139,141,158,157,145,138,144,143,312,292,2,3,177,168,20,25,15])). % 117.24/117.59 cnf(4176,plain, % 117.24/117.59 (~P6(f31(a23),f31(f28(a5)))), % 117.24/117.59 inference(scs_inference,[],[3740,2917,4098,2972,4096,3833,4078,4074,3939,3230,2710,3515,3483,137,136,147,139,141,158,157,145,138,144,143,312,292,2,3,177,168,20,25,15,16])). % 117.24/117.59 cnf(4186,plain, % 117.24/117.59 (~P4(f30(f31(x41861)))), % 117.24/117.59 inference(scs_inference,[],[3783,137,139,157])). % 117.24/117.59 cnf(4192,plain, % 117.24/117.59 (~P4(f16(a3))), % 117.24/117.59 inference(scs_inference,[],[3783,132,137,139,157,141,145,158])). % 117.24/117.59 cnf(4196,plain, % 117.24/117.59 (E(f28(f32(a6)),a1)), % 117.24/117.59 inference(scs_inference,[],[3783,132,137,139,157,141,145,158,144,138])). % 117.24/117.59 cnf(4204,plain, % 117.24/117.59 (~P11(f32(a21),f33(f28(a1),f28(a1)))), % 117.24/117.59 inference(scs_inference,[],[3464,3000,3974,3898,3783,2995,3010,132,137,139,157,141,145,158,144,138,143,312,292,2,24,185])). % 117.24/117.59 cnf(4210,plain, % 117.24/117.59 (~P6(f31(a1),f31(f32(a1)))), % 117.24/117.59 inference(scs_inference,[],[3464,4085,3000,4167,3974,3898,4110,3783,2995,3010,1078,4098,132,2519,137,139,157,141,145,158,144,138,143,312,292,2,24,185,3,177,184])). % 117.24/117.59 cnf(4245,plain, % 117.24/117.59 (E(f32(f32(a6)),a1)), % 117.24/117.59 inference(scs_inference,[],[4192,3807,139,157,141,158,145,144,138])). % 117.24/117.59 cnf(4253,plain, % 117.24/117.59 (P2(f15(a5))), % 117.24/117.59 inference(scs_inference,[],[3090,4192,4080,3807,3342,2825,41,126,139,157,141,158,145,144,138,143,312,2,292,21,174])). % 117.24/117.59 cnf(4254,plain, % 117.24/117.59 (P6(f15(x42541),x42541)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(4256,plain, % 117.24/117.59 (P3(f15(a5))), % 117.24/117.59 inference(scs_inference,[],[3090,4192,4080,3807,3342,2825,41,126,4254,139,157,141,158,145,144,138,143,312,2,292,21,174,175])). % 117.24/117.59 cnf(4264,plain, % 117.24/117.59 (~P6(f32(a21),f31(f28(a1)))), % 117.24/117.59 inference(scs_inference,[],[2727,3090,4192,3216,4080,3807,3342,1379,2825,41,3312,2895,137,136,126,4254,139,157,141,158,145,144,138,143,312,2,292,21,174,175,14,3,177,179])). % 117.24/117.59 cnf(4266,plain, % 117.24/117.59 (~E(f32(f32(a6)),f16(a3))), % 117.24/117.59 inference(scs_inference,[],[2727,3090,4192,3216,4080,3807,3342,1379,2825,41,3312,2895,137,136,126,4254,139,157,141,158,145,144,138,143,312,2,292,21,174,175,14,3,177,179,20])). % 117.24/117.59 cnf(4270,plain, % 117.24/117.59 (P6(f33(a1,a1),a29)), % 117.24/117.59 inference(scs_inference,[],[2727,3090,4192,3216,4080,1546,4174,3807,3342,1379,2914,3891,2825,41,1921,3312,2895,137,136,126,4254,139,157,141,158,145,144,138,143,312,2,292,21,174,175,14,3,177,179,20,25,17,15])). % 117.24/117.59 cnf(4302,plain, % 117.24/117.59 (~P6(a29,f30(a3))), % 117.24/117.59 inference(scs_inference,[],[3169,3245,4172,3965,4157,3590,113,3710,1226,126,139,141,158,145,138,144,143,312,2,292,173,3,177])). % 117.24/117.59 cnf(4305,plain, % 117.24/117.59 (~P6(f31(a1),f31(a1))), % 117.24/117.59 inference(scs_inference,[],[3169,3245,4172,4186,3965,4210,4157,3590,113,2702,1990,3710,1226,126,139,141,158,145,138,144,143,312,2,292,173,3,177,20,16])). % 117.24/117.59 cnf(4321,plain, % 117.24/117.59 (P1(f28(f28(a4)))), % 117.24/117.59 inference(scs_inference,[],[4305,3491,213,139])). % 117.24/117.59 cnf(4327,plain, % 117.24/117.59 (~P4(f16(f31(x43271)))), % 117.24/117.59 inference(scs_inference,[],[4305,3491,137,213,139,141,145,158])). % 117.24/117.59 cnf(4329,plain, % 117.24/117.59 (E(f28(f28(a4)),a1)), % 117.24/117.59 inference(scs_inference,[],[4305,3491,137,213,139,141,145,158,138])). % 117.24/117.59 cnf(4343,plain, % 117.24/117.59 (P1(f15(a5))), % 117.24/117.59 inference(scs_inference,[],[3247,3257,4253,4256,4270,4305,1034,3491,2906,1429,2711,2714,129,137,213,139,141,145,158,138,144,143,312,2,292,26,23,3,177,153])). % 117.24/117.59 cnf(4346,plain, % 117.24/117.59 (~P6(f32(a21),f31(a1))), % 117.24/117.59 inference(scs_inference,[],[3247,3257,4253,4256,4270,4305,4264,1034,2905,3491,2906,1429,188,2711,2714,129,137,213,139,141,145,158,138,144,143,312,2,292,26,23,3,177,153,20,16])). % 117.24/117.59 cnf(4347,plain, % 117.24/117.59 (~P6(f31(f28(a4)),f31(a1))), % 117.24/117.59 inference(scs_inference,[],[3247,3257,4253,4256,4270,4305,4264,1034,3522,2905,3491,2906,1429,188,2711,2714,129,137,213,139,141,145,158,138,144,143,312,2,292,26,23,3,177,153,20,16,15])). % 117.24/117.59 cnf(4378,plain, % 117.24/117.59 (P6(f15(x43781),x43781)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(4381,plain, % 117.24/117.59 (P6(f15(x43811),x43811)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(4391,plain, % 117.24/117.59 (~P6(a29,f16(a3))), % 117.24/117.59 inference(scs_inference,[],[3322,4343,4346,3397,4347,4321,4196,3517,1040,2709,4192,3491,2519,126,4378,4381,213,139,141,145,138,144,143,312,2,292,175,174,173,29,3,156,177])). % 117.24/117.59 cnf(4394,plain, % 117.24/117.59 (~E(f31(a29),f30(a3))), % 117.24/117.59 inference(scs_inference,[],[3322,4343,4346,3397,4302,4347,4327,4321,4196,3517,1040,2709,1033,4192,3507,3491,2519,126,4378,4381,213,139,141,145,138,144,143,312,2,292,175,174,173,29,3,156,177,20,16])). % 117.24/117.59 cnf(4396,plain, % 117.24/117.59 (~P6(f33(a21,f28(a21)),f31(a1))), % 117.24/117.59 inference(scs_inference,[],[3322,4343,4346,3397,4302,4347,4327,4321,4196,3517,1040,3789,2709,1033,4192,3507,3491,2519,126,4378,4381,213,139,141,145,138,144,143,312,2,292,175,174,173,29,3,156,177,20,16,15])). % 117.24/117.59 cnf(4421,plain, % 117.24/117.59 (P6(f15(x44211),x44211)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(4424,plain, % 117.24/117.59 (P6(f15(x44241),x44241)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(4426,plain, % 117.24/117.59 (P1(f15(a3))), % 117.24/117.59 inference(scs_inference,[],[3618,4391,4396,3380,40,126,4421,4424,141,139,213,145,138,143,144,292,2,312,175,174,173])). % 117.24/117.59 cnf(4430,plain, % 117.24/117.59 (P11(f11(f28(a1)),f31(a1))), % 117.24/117.59 inference(scs_inference,[],[3384,3618,4391,3439,4396,3380,40,2895,137,126,4421,4424,141,139,213,145,138,143,144,292,2,312,175,174,173,3,177])). % 117.24/117.59 cnf(4457,plain, % 117.24/117.59 (E(f32(f32(a5)),a1)), % 117.24/117.59 inference(scs_inference,[],[3297,141,139,145,138])). % 117.24/117.59 cnf(4467,plain, % 117.24/117.59 (P6(f15(x44671),x44671)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(4470,plain, % 117.24/117.59 (P6(f15(x44701),x44701)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(4473,plain, % 117.24/117.59 (P6(f15(x44731),x44731)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(4475,plain, % 117.24/117.59 (~P6(f31(a1),f31(f32(a6)))), % 117.24/117.59 inference(scs_inference,[],[3619,4426,4430,3969,3297,3659,126,4467,4470,141,139,145,138,143,144,2,292,312,174,175,173,184])). % 117.24/117.59 cnf(4478,plain, % 117.24/117.59 (P4(f33(f28(a5),f28(a5)))), % 117.24/117.59 inference(scs_inference,[],[3619,4426,4266,4430,3969,4245,3297,3478,3659,126,4467,4470,4473,141,139,145,138,143,144,2,292,312,174,175,173,184,3,177])). % 117.24/117.59 cnf(4506,plain, % 117.24/117.59 (E(f33(f28(a5),f28(a5)),a1)), % 117.24/117.59 inference(scs_inference,[],[4478,146,139,141,145,138])). % 117.24/117.59 cnf(4517,plain, % 117.24/117.59 (P6(f15(x45171),x45171)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(4520,plain, % 117.24/117.59 (P6(f15(x45201),x45201)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(4522,plain, % 117.24/117.59 (P1(f15(a8))), % 117.24/117.59 inference(scs_inference,[],[3680,4478,4028,42,595,2714,126,4517,4520,146,139,141,145,138,143,144,2,292,312,21,174,175,173])). % 117.24/117.59 cnf(4523,plain, % 117.24/117.59 (P6(f15(x45231),x45231)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(4530,plain, % 117.24/117.59 (~P6(f32(a21),f31(f7(x45301)))), % 117.24/117.59 inference(scs_inference,[],[3406,3680,3050,4478,4028,1075,118,42,595,2910,2714,137,136,126,4517,4520,146,139,141,145,138,143,144,2,292,312,21,174,175,173,14,3,177,179])). % 117.24/117.59 cnf(4533,plain, % 117.24/117.59 (~E(f33(f28(a5),f28(a5)),a2)), % 117.24/117.59 inference(scs_inference,[],[3406,3680,3050,4478,1793,4028,1075,118,42,595,2910,130,2714,137,136,126,4517,4520,146,139,141,145,138,143,144,2,292,312,21,174,175,173,14,3,177,179,25,20])). % 117.24/117.59 cnf(4536,plain, % 117.24/117.59 (P6(f33(f28(a1),f28(a1)),a29)), % 117.24/117.59 inference(scs_inference,[],[3406,3680,3050,4478,1793,4028,1075,4270,118,42,2995,3515,595,2910,130,2714,137,136,126,4517,4520,4523,146,139,141,145,138,143,144,2,292,312,21,174,175,173,14,3,177,179,25,20,16,15])). % 117.24/117.59 cnf(4561,plain, % 117.24/117.59 (P6(f15(x45611),x45611)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(4564,plain, % 117.24/117.59 (P6(f15(x45641),x45641)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(4567,plain, % 117.24/117.59 (P6(f15(x45671),x45671)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(4570,plain, % 117.24/117.59 (P4(f33(a8,f28(a8)))), % 117.24/117.59 inference(scs_inference,[],[3760,4522,4530,4176,3218,3260,2711,1420,126,4561,4564,4567,139,141,145,138,143,144,2,292,312,174,175,173,19,177])). % 117.24/117.59 cnf(4574,plain, % 117.24/117.59 (~E(a1,a2)), % 117.24/117.59 inference(scs_inference,[],[3760,4522,4530,4176,4506,4533,3218,3260,2711,1420,126,4561,4564,4567,139,141,145,138,143,144,2,292,312,174,175,173,19,177,3])). % 117.24/117.59 cnf(4591,plain, % 117.24/117.59 (P1(f33(a8,f28(a8)))), % 117.24/117.59 inference(scs_inference,[],[4570,146,139])). % 117.24/117.59 cnf(4601,plain, % 117.24/117.59 (P7(f33(a8,f28(a8)))), % 117.24/117.59 inference(scs_inference,[],[4570,146,139,141,145,138,143,144])). % 117.24/117.59 cnf(4607,plain, % 117.24/117.59 (P6(f15(x46071),x46071)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(4609,plain, % 117.24/117.59 (P1(f15(a22))), % 117.24/117.59 inference(scs_inference,[],[3768,4570,4475,38,126,4607,146,139,141,145,138,143,144,2,292,312,174,173])). % 117.24/117.59 cnf(4612,plain, % 117.24/117.59 (P12(f33(a1,a1))), % 117.24/117.59 inference(scs_inference,[],[3768,4570,4475,1041,38,2993,126,4607,146,139,141,145,138,143,144,2,292,312,174,173,26])). % 117.24/117.59 cnf(4613,plain, % 117.24/117.59 (E(f33(x46131,f28(a1)),f33(x46131,a1))), % 117.24/117.59 inference(rename_variables,[],[2993])). % 117.24/117.59 cnf(4627,plain, % 117.24/117.59 (P6(f33(f28(a1),a1),a29)), % 117.24/117.59 inference(scs_inference,[],[4574,3768,3138,4570,2533,4475,4536,3733,1041,3095,3072,38,3010,2993,4613,188,125,2519,137,136,126,4607,146,139,141,145,138,143,144,2,292,312,174,173,26,23,185,177,3,25,20,30,15])). % 117.24/117.59 cnf(4628,plain, % 117.24/117.59 (E(f33(x46281,f28(a1)),f33(x46281,a1))), % 117.24/117.59 inference(rename_variables,[],[2993])). % 117.24/117.59 cnf(4629,plain, % 117.24/117.59 (P6(f15(a1),f33(f28(a1),a1))), % 117.24/117.59 inference(scs_inference,[],[4574,3768,3138,4570,2533,4475,4536,3733,3404,1041,3095,3072,38,3010,2993,4613,4628,188,125,2519,137,136,126,4607,146,139,141,145,138,143,144,2,292,312,174,173,26,23,185,177,3,25,20,30,15,16])). % 117.24/117.59 cnf(4661,plain, % 117.24/117.59 (P6(f15(x46611),x46611)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(4664,plain, % 117.24/117.59 (P6(f15(x46641),x46641)), % 117.24/117.59 inference(rename_variables,[],[126])). % 117.24/117.59 cnf(4668,plain, % 117.24/117.59 (P4(f33(a1,a1))), % 117.24/117.59 inference(scs_inference,[],[3831,4609,4591,2924,2723,2946,3013,4570,126,4661,4664,139,141,145,138,143,144,292,2,312,174,173,156,177])). % 117.24/117.59 cnf(4684,plain, % 117.24/117.59 (P4(f28(f33(a1,a1)))), % 117.24/117.59 inference(scs_inference,[],[3831,4609,4591,4601,3200,4329,4457,2924,3614,2723,2946,3323,3013,3973,1033,4570,3507,2519,190,136,126,4661,4664,139,141,145,138,143,144,292,2,312,174,173,156,177,3,25,20,16,15,18,152,151,149])). % 117.24/117.59 cnf(4686,plain, % 117.24/117.59 (P4(f32(f33(a1,a1)))), % 117.24/117.59 inference(scs_inference,[],[3831,4609,4591,4601,3200,4329,4457,2924,3614,2723,2946,3323,3013,3973,1033,4570,3507,2519,190,136,126,4661,4664,139,141,145,138,143,144,292,2,312,174,173,156,177,3,25,20,16,15,18,152,151,149,150])). % 117.24/117.59 cnf(4698,plain, % 117.24/117.59 (E(f33(a1,a1),a1)), % 117.24/117.59 inference(scs_inference,[],[4668,4684,139,141,145,138])). % 117.24/117.59 cnf(4702,plain, % 117.24/117.59 (P7(f33(a1,a1))), % 117.24/117.59 inference(scs_inference,[],[4668,4684,139,141,145,138,143,144])). % 117.24/117.59 cnf(4707,plain, % 117.24/117.59 (~P6(f31(a1),f31(f33(a1,a1)))), % 117.24/117.59 inference(scs_inference,[],[4668,3889,4684,3012,4430,139,141,145,138,143,144,292,2,312,184])). % 117.24/117.59 cnf(4709,plain, % 117.24/117.59 (P11(f11(a1),f31(f32(a1)))), % 117.24/117.59 inference(scs_inference,[],[4668,3889,3289,4684,3012,4430,137,139,141,145,138,143,144,292,2,312,184,177])). % 117.24/117.59 cnf(4714,plain, % 117.24/117.59 (~E(f33(a1,a1),f16(f16(a29)))), % 117.24/117.59 inference(scs_inference,[],[4668,3453,3889,3289,2535,3275,4684,3012,4430,2910,137,136,139,141,145,138,143,144,292,2,312,184,177,3,25,20])). % 117.24/117.59 cnf(4722,plain, % 117.24/117.59 (P6(f33(f28(a8),a1),f31(a1))), % 117.24/117.59 inference(scs_inference,[],[4668,3453,3889,3331,3289,4204,2535,3275,4684,4629,4627,3012,2987,4430,2908,2710,2910,137,136,139,141,145,138,143,144,292,2,312,184,177,3,25,20,31,15,16,18,178])). % 117.24/117.59 cnf(4729,plain, % 117.24/117.59 (E(f11(f33(a1,a1)),f11(a1))), % 117.24/117.59 inference(scs_inference,[],[4668,3453,3889,3331,3289,4204,2535,3275,4684,4629,4627,3012,2987,4430,2908,2710,2910,137,136,139,141,145,138,143,144,292,2,312,184,177,3,25,20,31,15,16,18,178,6,8,4,7,12,9])). % 117.24/117.59 cnf(4730,plain, % 117.24/117.59 (E(f33(f33(a1,a1),x47301),f33(a1,x47301))), % 117.24/117.59 inference(scs_inference,[],[4668,3453,3889,3331,3289,4204,2535,3275,4684,4629,4627,3012,2987,4430,2908,2710,2910,137,136,139,141,145,138,143,144,292,2,312,184,177,3,25,20,31,15,16,18,178,6,8,4,7,12,9,11])). % 117.24/117.59 cnf(4733,plain, % 117.24/117.59 (E(f7(f33(a1,a1)),f7(a1))), % 117.24/117.59 inference(scs_inference,[],[4668,3453,3889,3331,3289,4204,2535,3275,4684,4629,4627,3012,2987,4430,2908,2710,2910,137,136,139,141,145,138,143,144,292,2,312,184,177,3,25,20,31,15,16,18,178,6,8,4,7,12,9,11,10,13,5])). % 117.24/117.59 cnf(4755,plain, % 117.24/117.59 (~P6(f31(f32(a1)),f31(a5))), % 117.24/117.59 inference(scs_inference,[],[3896,4707,4709,4686,1989,2711,67,139,141,145,138,143,144,292,2,312,29,184])). % 117.24/117.59 cnf(4757,plain, % 117.24/117.59 (P4(f15(f31(a4)))), % 117.24/117.59 inference(scs_inference,[],[3896,4707,4709,4686,1989,2711,67,909,126,139,141,145,138,143,144,292,2,312,29,184,177])). % 117.24/117.59 cnf(4762,plain, % 117.24/117.59 (~P6(f32(a21),f31(f33(a1,a1)))), % 117.24/117.59 inference(scs_inference,[],[4702,3896,4698,4714,4707,4709,4686,1989,2711,67,909,136,126,139,141,145,138,143,144,292,2,312,29,184,177,3,179])). % 117.24/117.59 cnf(4764,plain, % 117.24/117.59 (~E(f33(a1,a1),f32(a21))), % 117.24/117.59 inference(scs_inference,[],[4702,3896,4698,4714,4707,4709,4686,1989,2711,67,909,136,126,139,141,145,138,143,144,292,2,312,29,184,177,3,179,25])). % 117.24/117.59 cnf(4796,plain, % 117.24/117.59 (P11(f33(f28(a8),a1),f31(a1))), % 117.24/117.59 inference(scs_inference,[],[4764,4722,4755,4757,137,146,139,141,138,145,143,144,292,312,2,177])). % 117.24/117.59 cnf(4800,plain, % 117.24/117.59 (~P6(f32(a21),f31(a23))), % 117.24/117.59 inference(scs_inference,[],[4764,3971,4722,4755,4757,69,2910,137,136,146,139,141,138,145,143,144,292,312,2,177,3,179])). % 117.24/117.59 cnf(4847,plain, % 117.24/117.59 (~E(f31(f32(a21)),f31(a23))), % 117.24/117.59 inference(scs_inference,[],[3900,4800,4730,4796,3360,3945,2982,1078,3871,3789,3507,942,126,139,141,138,145,143,144,292,312,2,184,177,3,20,15,16])). % 117.24/117.59 cnf(4992,plain, % 117.24/117.59 (P15(f33(a1,a1))), % 117.24/117.59 inference(scs_inference,[],[4394,4762,3063,1040,2993,145,141,139,138,143,144,292,312,2,29])). % 117.24/117.59 cnf(5304,plain, % 117.24/117.59 (E(f33(x53041,f28(a1)),f33(x53041,a1))), % 117.24/117.59 inference(rename_variables,[],[2993])). % 117.24/117.59 cnf(5308,plain, % 117.24/117.59 (E(f33(a1,x53081),f33(f28(a1),x53081))), % 117.24/117.59 inference(rename_variables,[],[2909])). % 117.24/117.59 cnf(5315,plain, % 117.24/117.59 (P6(f33(f28(a1),f28(a1)),f31(x53151))), % 117.24/117.59 inference(rename_variables,[],[3010])). % 117.24/117.59 cnf(5321,plain, % 117.24/117.59 (E(f33(x53211,a1),f33(x53211,f32(a1)))), % 117.24/117.59 inference(rename_variables,[],[2710])). % 117.24/117.59 cnf(5330,plain, % 117.24/117.59 (E(f33(x53301,a1),f33(x53301,f32(a1)))), % 117.24/117.59 inference(rename_variables,[],[2710])). % 117.24/117.59 cnf(5332,plain, % 117.24/117.59 (E(f33(x53321,a1),f33(x53321,f32(a1)))), % 117.24/117.59 inference(rename_variables,[],[2710])). % 117.24/117.59 cnf(5334,plain, % 117.24/117.59 (E(f33(a1,x53341),f33(f28(a1),x53341))), % 117.24/117.59 inference(rename_variables,[],[2909])). % 117.24/117.59 cnf(5336,plain, % 117.24/117.59 (E(f33(x53361,a1),f33(x53361,f32(a1)))), % 117.24/117.59 inference(rename_variables,[],[2710])). % 117.24/117.59 cnf(5345,plain, % 117.24/117.59 ($false), % 117.24/117.59 inference(scs_inference,[],[80,126,96,136,63,190,186,3052,3789,3633,2897,2895,205,112,3483,3497,2993,5304,2909,5308,5334,2658,2908,2710,5321,5330,5332,5336,3010,5315,2702,3312,3714,4722,3342,3230,3466,3891,1915,4733,3760,2881,3060,3331,2998,3464,3733,2869,3068,2832,4847,3314,4992,4612,3074,4729,2701,2704,292,2,312,213,7,4,6,181,178,162,310,389,290,334,368,353,2113,2117,291,309,311,330,433,441,176,18,16,15,30,31,20,17,25,3,179,177,22,156,184,185,29,24,14,19,23,26,21,159,183]), % 117.24/117.59 ['proof']). % 117.24/117.59 % SZS output end Proof % 117.24/117.59 % Total time :116.580000s %------------------------------------------------------------------------------