%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU374+1 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n018.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:42 EDT 2024 % Result : Theorem 64.64s 64.66s % Output : CNFRefutation 64.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU374+1 : TPTP v8.2.0. Released v3.3.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n018.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Fri Jun 21 11:41:39 EDT 2024 % 0.12/0.33 % CPUTime : % 0.52/0.55 start to proof:theBenchmark % 64.54/64.64 %------------------------------------------- % 64.54/64.64 % File :CSE---1.7 % 64.54/64.64 % Problem :theBenchmark % 64.54/64.64 % Transform :cnf % 64.54/64.64 % Format :tptp:raw % 64.54/64.64 % Command :java -jar mcs_scs.jar %d %s % 64.54/64.64 % 64.54/64.64 % Result :Theorem 64.050000s % 64.54/64.64 % Output :CNFRefutation 64.050000s % 64.54/64.64 %------------------------------------------- % 64.54/64.65 %------------------------------------------------------------------------------ % 64.54/64.65 % File : SEU374+1 : TPTP v8.2.0. Released v3.3.0. % 64.54/64.65 % Domain : Set theory % 64.54/64.65 % Problem : MPTP bushy problem t20_yellow_6 % 64.54/64.65 % Version : [Urb07] axioms : Especial. % 64.54/64.65 % English : % 64.54/64.65 % 64.54/64.65 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 64.54/64.65 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 64.54/64.65 % Source : [Urb07] % 64.54/64.65 % Names : bushy-t20_yellow_6 [Urb07] % 64.54/64.65 % 64.54/64.65 % Status : Theorem % 64.54/64.65 % Rating : 0.17 v8.2.0, 0.14 v8.1.0, 0.06 v7.4.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.17 v6.2.0, 0.16 v6.1.0, 0.20 v6.0.0, 0.22 v5.5.0, 0.15 v5.4.0, 0.21 v5.3.0, 0.22 v5.2.0, 0.10 v5.1.0, 0.14 v5.0.0, 0.25 v4.1.0, 0.30 v4.0.0, 0.33 v3.7.0, 0.25 v3.5.0, 0.26 v3.4.0, 0.37 v3.3.0 % 64.54/64.65 % Syntax : Number of formulae : 58 ( 14 unt; 0 def) % 64.54/64.65 % Number of atoms : 150 ( 8 equ) % 64.54/64.65 % Maximal formula atoms : 11 ( 2 avg) % 64.54/64.65 % Number of connectives : 104 ( 12 ~; 1 |; 42 &) % 64.54/64.65 % ( 3 <=>; 46 =>; 0 <=; 0 <~>) % 64.54/64.65 % Maximal formula depth : 18 ( 4 avg) % 64.54/64.65 % Maximal term depth : 3 ( 1 avg) % 64.54/64.65 % Number of predicates : 19 ( 17 usr; 1 prp; 0-3 aty) % 64.54/64.65 % Number of functors : 7 ( 7 usr; 1 con; 0-4 aty) % 64.54/64.65 % Number of variables : 105 ( 87 !; 18 ?) % 64.54/64.65 % SPC : FOF_THM_RFO_SEQ % 64.54/64.65 % 64.54/64.65 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 64.54/64.65 % library, www.mizar.org % 64.54/64.65 %------------------------------------------------------------------------------ % 64.54/64.65 fof(antisymmetry_r2_hidden,axiom, % 64.54/64.65 ! [A,B] : % 64.54/64.65 ( in(A,B) % 64.54/64.65 => ~ in(B,A) ) ). % 64.54/64.65 % 64.54/64.65 fof(cc1_funct_1,axiom, % 64.54/64.65 ! [A] : % 64.54/64.65 ( empty(A) % 64.54/64.65 => function(A) ) ). % 64.54/64.65 % 64.54/64.65 fof(cc1_relat_1,axiom, % 64.54/64.65 ! [A] : % 64.54/64.65 ( empty(A) % 64.54/64.65 => relation(A) ) ). % 64.54/64.65 % 64.54/64.65 fof(cc1_relset_1,axiom, % 64.54/64.65 ! [A,B,C] : % 64.54/64.65 ( element(C,powerset(cartesian_product2(A,B))) % 64.54/64.65 => relation(C) ) ). % 64.54/64.65 % 64.54/64.65 fof(cc2_funct_1,axiom, % 64.54/64.65 ! [A] : % 64.54/64.65 ( ( relation(A) % 64.54/64.65 & empty(A) % 64.54/64.65 & function(A) ) % 64.54/64.65 => ( relation(A) % 64.54/64.65 & function(A) % 64.54/64.65 & one_to_one(A) ) ) ). % 64.54/64.65 % 64.54/64.65 fof(d8_yellow_6,axiom, % 64.54/64.65 ! [A] : % 64.54/64.65 ( one_sorted_str(A) % 64.54/64.65 => ! [B] : % 64.54/64.65 ( net_str(B,A) % 64.54/64.65 => ! [C] : % 64.54/64.65 ( net_str(C,A) % 64.54/64.65 => ( subnetstr(C,A,B) % 64.54/64.65 <=> ( subrelstr(C,B) % 64.54/64.65 & the_mapping(A,C) = relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C)) ) ) ) ) ) ). % 64.54/64.65 % 64.54/64.65 fof(dt_k1_xboole_0,axiom, % 64.54/64.65 $true ). % 64.54/64.65 % 64.54/64.65 fof(dt_k1_zfmisc_1,axiom, % 64.54/64.65 $true ). % 64.54/64.65 % 64.54/64.65 fof(dt_k2_zfmisc_1,axiom, % 64.54/64.65 $true ). % 64.54/64.65 % 64.54/64.65 fof(dt_k7_relat_1,axiom, % 64.54/64.65 ! [A,B] : % 64.54/64.65 ( relation(A) % 64.54/64.65 => relation(relation_dom_restriction(A,B)) ) ). % 64.54/64.65 % 64.54/64.65 fof(dt_k8_relset_1,axiom, % 64.54/64.65 ! [A,B,C,D] : % 64.54/64.65 ( relation_of2(C,A,B) % 64.54/64.65 => relation_of2_as_subset(relation_dom_restr_as_relation_of(A,B,C,D),A,B) ) ). % 64.54/64.65 % 64.54/64.65 fof(dt_l1_orders_2,axiom, % 64.54/64.65 ! [A] : % 64.54/64.65 ( rel_str(A) % 64.54/64.65 => one_sorted_str(A) ) ). % 64.54/64.65 % 64.54/64.65 fof(dt_l1_struct_0,axiom, % 64.54/64.65 $true ). % 64.54/64.65 % 64.54/64.65 fof(dt_l1_waybel_0,axiom, % 64.54/64.65 ! [A] : % 64.54/64.65 ( one_sorted_str(A) % 64.54/64.65 => ! [B] : % 64.54/64.65 ( net_str(B,A) % 64.54/64.65 => rel_str(B) ) ) ). % 64.54/64.65 % 64.54/64.65 fof(dt_m1_relset_1,axiom, % 64.54/64.65 $true ). % 64.54/64.65 % 64.54/64.65 fof(dt_m1_subset_1,axiom, % 64.54/64.65 $true ). % 64.54/64.65 % 64.54/64.65 fof(dt_m1_yellow_0,axiom, % 64.54/64.65 ! [A] : % 64.54/64.65 ( rel_str(A) % 64.54/64.65 => ! [B] : % 64.54/64.65 ( subrelstr(B,A) % 64.54/64.65 => rel_str(B) ) ) ). % 64.54/64.65 % 64.54/64.65 fof(dt_m1_yellow_6,axiom, % 64.54/64.66 ! [A,B] : % 64.54/64.66 ( ( one_sorted_str(A) % 64.54/64.66 & net_str(B,A) ) % 64.54/64.66 => ! [C] : % 64.54/64.66 ( subnetstr(C,A,B) % 64.54/64.66 => net_str(C,A) ) ) ). % 64.54/64.66 % 64.54/64.66 fof(dt_m2_relset_1,axiom, % 64.54/64.66 ! [A,B,C] : % 64.54/64.66 ( relation_of2_as_subset(C,A,B) % 64.54/64.66 => element(C,powerset(cartesian_product2(A,B))) ) ). % 64.54/64.66 % 64.54/64.66 fof(dt_u1_struct_0,axiom, % 64.54/64.66 $true ). % 64.54/64.66 % 64.54/64.66 fof(dt_u1_waybel_0,axiom, % 64.54/64.66 ! [A,B] : % 64.54/64.66 ( ( one_sorted_str(A) % 64.54/64.66 & net_str(B,A) ) % 64.54/64.66 => ( function(the_mapping(A,B)) % 64.54/64.66 & quasi_total(the_mapping(A,B),the_carrier(B),the_carrier(A)) % 64.54/64.66 & relation_of2_as_subset(the_mapping(A,B),the_carrier(B),the_carrier(A)) ) ) ). % 64.54/64.66 % 64.54/64.66 fof(existence_l1_orders_2,axiom, % 64.54/64.66 ? [A] : rel_str(A) ). % 64.54/64.66 % 64.54/64.66 fof(existence_l1_struct_0,axiom, % 64.54/64.66 ? [A] : one_sorted_str(A) ). % 64.54/64.66 % 64.54/64.66 fof(existence_l1_waybel_0,axiom, % 64.54/64.66 ! [A] : % 64.54/64.66 ( one_sorted_str(A) % 64.54/64.66 => ? [B] : net_str(B,A) ) ). % 64.54/64.66 % 64.54/64.66 fof(existence_m1_relset_1,axiom, % 64.54/64.66 ! [A,B] : % 64.54/64.66 ? [C] : relation_of2(C,A,B) ). % 64.54/64.66 % 64.54/64.66 fof(existence_m1_subset_1,axiom, % 64.54/64.66 ! [A] : % 64.54/64.66 ? [B] : element(B,A) ). % 64.54/64.66 % 64.54/64.66 fof(existence_m1_yellow_0,axiom, % 64.54/64.66 ! [A] : % 64.54/64.66 ( rel_str(A) % 64.54/64.66 => ? [B] : subrelstr(B,A) ) ). % 64.54/64.66 % 64.54/64.66 fof(existence_m1_yellow_6,axiom, % 64.54/64.66 ! [A,B] : % 64.54/64.66 ( ( one_sorted_str(A) % 64.54/64.66 & net_str(B,A) ) % 64.54/64.66 => ? [C] : subnetstr(C,A,B) ) ). % 64.54/64.66 % 64.54/64.66 fof(existence_m2_relset_1,axiom, % 64.54/64.66 ! [A,B] : % 64.54/64.66 ? [C] : relation_of2_as_subset(C,A,B) ). % 64.54/64.66 % 64.54/64.66 fof(fc12_relat_1,axiom, % 64.54/64.66 ( empty(empty_set) % 64.54/64.66 & relation(empty_set) % 64.54/64.66 & relation_empty_yielding(empty_set) ) ). % 64.54/64.66 % 64.54/64.66 fof(fc13_relat_1,axiom, % 64.54/64.66 ! [A,B] : % 64.54/64.66 ( ( relation(A) % 64.54/64.66 & relation_empty_yielding(A) ) % 64.54/64.66 => ( relation(relation_dom_restriction(A,B)) % 64.54/64.66 & relation_empty_yielding(relation_dom_restriction(A,B)) ) ) ). % 64.54/64.66 % 64.54/64.66 fof(fc1_subset_1,axiom, % 64.54/64.66 ! [A] : ~ empty(powerset(A)) ). % 64.54/64.66 % 64.54/64.66 fof(fc4_funct_1,axiom, % 64.54/64.66 ! [A,B] : % 64.54/64.66 ( ( relation(A) % 64.54/64.66 & function(A) ) % 64.54/64.66 => ( relation(relation_dom_restriction(A,B)) % 64.54/64.66 & function(relation_dom_restriction(A,B)) ) ) ). % 64.64/64.66 % 64.64/64.66 fof(fc4_relat_1,axiom, % 64.64/64.66 ( empty(empty_set) % 64.64/64.66 & relation(empty_set) ) ). % 64.64/64.66 % 64.64/64.66 fof(fc4_subset_1,axiom, % 64.64/64.66 ! [A,B] : % 64.64/64.66 ( ( ~ empty(A) % 64.64/64.66 & ~ empty(B) ) % 64.64/64.66 => ~ empty(cartesian_product2(A,B)) ) ). % 64.64/64.66 % 64.64/64.66 fof(rc1_funct_1,axiom, % 64.64/64.66 ? [A] : % 64.64/64.66 ( relation(A) % 64.64/64.66 & function(A) ) ). % 64.64/64.66 % 64.64/64.66 fof(rc1_pboole,axiom, % 64.64/64.66 ? [A] : % 64.64/64.66 ( relation(A) % 64.64/64.66 & relation_empty_yielding(A) % 64.64/64.66 & function(A) ) ). % 64.64/64.66 % 64.64/64.66 fof(rc1_relat_1,axiom, % 64.64/64.66 ? [A] : % 64.64/64.66 ( empty(A) % 64.64/64.66 & relation(A) ) ). % 64.64/64.66 % 64.64/64.66 fof(rc1_subset_1,axiom, % 64.64/64.66 ! [A] : % 64.64/64.66 ( ~ empty(A) % 64.64/64.66 => ? [B] : % 64.64/64.66 ( element(B,powerset(A)) % 64.64/64.66 & ~ empty(B) ) ) ). % 64.64/64.66 % 64.64/64.66 fof(rc2_funct_1,axiom, % 64.64/64.66 ? [A] : % 64.64/64.66 ( relation(A) % 64.64/64.66 & empty(A) % 64.64/64.66 & function(A) ) ). % 64.64/64.66 % 64.64/64.66 fof(rc2_relat_1,axiom, % 64.64/64.66 ? [A] : % 64.64/64.66 ( ~ empty(A) % 64.64/64.66 & relation(A) ) ). % 64.64/64.66 % 64.64/64.66 fof(rc2_subset_1,axiom, % 64.64/64.66 ! [A] : % 64.64/64.66 ? [B] : % 64.64/64.66 ( element(B,powerset(A)) % 64.64/64.66 & empty(B) ) ). % 64.64/64.66 % 64.64/64.66 fof(rc3_funct_1,axiom, % 64.64/64.66 ? [A] : % 64.64/64.66 ( relation(A) % 64.64/64.66 & function(A) % 64.64/64.66 & one_to_one(A) ) ). % 64.64/64.66 % 64.64/64.66 fof(rc3_relat_1,axiom, % 64.64/64.66 ? [A] : % 64.64/64.66 ( relation(A) % 64.64/64.66 & relation_empty_yielding(A) ) ). % 64.64/64.66 % 64.64/64.66 fof(rc4_funct_1,axiom, % 64.64/64.66 ? [A] : % 64.64/64.66 ( relation(A) % 64.64/64.66 & relation_empty_yielding(A) % 64.64/64.66 & function(A) ) ). % 64.64/64.66 % 64.64/64.66 fof(redefinition_k8_relset_1,axiom, % 64.64/64.66 ! [A,B,C,D] : % 64.64/64.66 ( relation_of2(C,A,B) % 64.64/64.66 => relation_dom_restr_as_relation_of(A,B,C,D) = relation_dom_restriction(C,D) ) ). % 64.64/64.66 % 64.64/64.66 fof(redefinition_m2_relset_1,axiom, % 64.64/64.66 ! [A,B,C] : % 64.64/64.66 ( relation_of2_as_subset(C,A,B) % 64.64/64.66 <=> relation_of2(C,A,B) ) ). % 64.64/64.66 % 64.64/64.66 fof(reflexivity_r1_tarski,axiom, % 64.64/64.66 ! [A,B] : subset(A,A) ). % 64.64/64.66 % 64.64/64.66 fof(t1_subset,axiom, % 64.64/64.66 ! [A,B] : % 64.64/64.66 ( in(A,B) % 64.64/64.66 => element(A,B) ) ). % 64.64/64.66 % 64.64/64.66 fof(t20_yellow_6,conjecture, % 64.64/64.66 ! [A] : % 64.64/64.66 ( one_sorted_str(A) % 64.64/64.66 => ! [B] : % 64.64/64.66 ( net_str(B,A) % 64.64/64.66 => ! [C] : % 64.64/64.66 ( subnetstr(C,A,B) % 64.64/64.66 => ! [D] : % 64.64/64.66 ( element(D,the_carrier(B)) % 64.64/64.66 => ! [E] : % 64.64/64.66 ( element(E,the_carrier(B)) % 64.64/64.66 => ! [F] : % 64.64/64.66 ( element(F,the_carrier(C)) % 64.64/64.66 => ! [G] : % 64.64/64.66 ( element(G,the_carrier(C)) % 64.64/64.66 => ( ( D = F % 64.64/64.66 & E = G % 64.64/64.66 & related(C,F,G) ) % 64.64/64.66 => related(B,D,E) ) ) ) ) ) ) ) ) ). % 64.64/64.66 % 64.64/64.66 fof(t2_subset,axiom, % 64.64/64.66 ! [A,B] : % 64.64/64.66 ( element(A,B) % 64.64/64.66 => ( empty(B) % 64.64/64.66 | in(A,B) ) ) ). % 64.64/64.66 % 64.64/64.66 fof(t3_subset,axiom, % 64.64/64.66 ! [A,B] : % 64.64/64.66 ( element(A,powerset(B)) % 64.64/64.66 <=> subset(A,B) ) ). % 64.64/64.66 % 64.64/64.66 fof(t4_subset,axiom, % 64.64/64.66 ! [A,B,C] : % 64.64/64.66 ( ( in(A,B) % 64.64/64.66 & element(B,powerset(C)) ) % 64.64/64.66 => element(A,C) ) ). % 64.64/64.66 % 64.64/64.66 fof(t5_subset,axiom, % 64.64/64.66 ! [A,B,C] : % 64.64/64.66 ~ ( in(A,B) % 64.64/64.66 & element(B,powerset(C)) % 64.64/64.66 & empty(C) ) ). % 64.64/64.66 % 64.64/64.66 fof(t60_yellow_0,axiom, % 64.64/64.66 ! [A] : % 64.64/64.66 ( rel_str(A) % 64.64/64.66 => ! [B] : % 64.64/64.66 ( subrelstr(B,A) % 64.64/64.66 => ! [C] : % 64.64/64.66 ( element(C,the_carrier(A)) % 64.64/64.66 => ! [D] : % 64.64/64.66 ( element(D,the_carrier(A)) % 64.64/64.66 => ! [E] : % 64.64/64.66 ( element(E,the_carrier(B)) % 64.64/64.66 => ! [F] : % 64.64/64.66 ( element(F,the_carrier(B)) % 64.64/64.66 => ( ( E = C % 64.64/64.66 & F = D % 64.64/64.66 & related(B,E,F) ) % 64.64/64.66 => related(A,C,D) ) ) ) ) ) ) ) ). % 64.64/64.66 % 64.64/64.66 fof(t6_boole,axiom, % 64.64/64.66 ! [A] : % 64.64/64.66 ( empty(A) % 64.64/64.66 => A = empty_set ) ). % 64.64/64.66 % 64.64/64.66 fof(t7_boole,axiom, % 64.64/64.66 ! [A,B] : % 64.64/64.66 ~ ( in(A,B) % 64.64/64.66 & empty(B) ) ). % 64.64/64.66 % 64.64/64.66 fof(t8_boole,axiom, % 64.64/64.66 ! [A,B] : % 64.64/64.66 ~ ( empty(A) % 64.64/64.66 & A != B % 64.64/64.66 & empty(B) ) ). % 64.64/64.66 % 64.64/64.66 %------------------------------------------------------------------------------ % 64.64/64.66 %------------------------------------------- % 64.64/64.66 % Proof found % 64.64/64.66 % SZS status Theorem for theBenchmark % 64.64/64.66 % SZS output start Proof % 64.64/64.66 %ClaNum:144(EqnAxiom:58) % 64.64/64.66 %VarNum:238(SingletonVarNum:96) % 64.64/64.66 %MaxLitNum:10 % 64.64/64.66 %MaxfuncDepth:2 % 64.64/64.66 %SharedTerms:56 % 64.64/64.66 %goalClause: 59 60 82 89 91 92 93 94 97 98 103 % 64.64/64.66 %singleGoalClaCount:11 % 64.64/64.66 [59]E(a1,a2) % 64.64/64.66 [60]E(a18,a19) % 64.64/64.66 [62]P1(a3) % 64.64/64.66 [63]P1(a5) % 64.64/64.66 [64]P1(a7) % 64.64/64.66 [65]P3(a20) % 64.64/64.66 [66]P3(a6) % 64.64/64.66 [67]P3(a7) % 64.64/64.66 [68]P3(a9) % 64.64/64.66 [69]P3(a12) % 64.64/64.66 [71]P4(a3) % 64.64/64.66 [72]P4(a20) % 64.64/64.66 [73]P4(a6) % 64.64/64.66 [74]P4(a5) % 64.64/64.66 [75]P4(a7) % 64.64/64.66 [76]P4(a10) % 64.64/64.66 [77]P4(a9) % 64.64/64.66 [78]P4(a13) % 64.64/64.67 [79]P4(a12) % 64.64/64.67 [80]P5(a9) % 64.64/64.67 [81]P6(a21) % 64.64/64.67 [82]P6(a14) % 64.64/64.67 [83]P9(a15) % 64.64/64.67 [84]P12(a3) % 64.64/64.67 [85]P12(a6) % 64.64/64.67 [86]P12(a13) % 64.64/64.67 [87]P12(a12) % 64.64/64.67 [89]P7(a16,a14) % 64.64/64.67 [97]P14(a17,a14,a16) % 64.64/64.67 [98]P11(a17,a1,a19) % 64.64/64.67 [101]~P1(a10) % 64.64/64.67 [103]~P11(a16,a2,a18) % 64.64/64.67 [91]P2(a2,f28(a16)) % 64.64/64.67 [92]P2(a18,f28(a16)) % 64.64/64.67 [93]P2(a1,f28(a17)) % 64.64/64.67 [94]P2(a19,f28(a17)) % 64.64/64.67 [90]P13(x901,x901) % 64.64/64.67 [88]P1(f11(x881)) % 64.64/64.67 [95]P2(f22(x951),x951) % 64.64/64.67 [96]P2(f11(x961),f29(x961)) % 64.64/64.67 [102]~P1(f29(x1021)) % 64.64/64.67 [99]P15(f23(x991,x992),x991,x992) % 64.64/64.67 [100]P16(f25(x1001,x1002),x1001,x1002) % 64.64/64.67 [104]~P1(x1041)+E(x1041,a3) % 64.64/64.67 [105]~P1(x1051)+P3(x1051) % 64.64/64.67 [106]~P1(x1061)+P4(x1061) % 64.64/64.67 [107]~P9(x1071)+P6(x1071) % 64.64/64.67 [109]P1(x1091)+~P1(f8(x1091)) % 64.64/64.67 [111]~P6(x1111)+P7(f24(x1111),x1111) % 64.64/64.67 [112]~P9(x1121)+P17(f26(x1121),x1121) % 64.64/64.67 [114]P1(x1141)+P2(f8(x1141),f29(x1141)) % 64.64/64.67 [113]~P1(x1131)+~P8(x1132,x1131) % 64.64/64.67 [117]~P8(x1171,x1172)+P2(x1171,x1172) % 64.64/64.67 [125]~P8(x1252,x1251)+~P8(x1251,x1252) % 64.64/64.67 [118]~P4(x1181)+P4(f30(x1181,x1182)) % 64.64/64.67 [120]~P13(x1201,x1202)+P2(x1201,f29(x1202)) % 64.64/64.67 [126]P13(x1261,x1262)+~P2(x1261,f29(x1262)) % 64.64/64.67 [136]~P16(x1361,x1362,x1363)+P15(x1361,x1362,x1363) % 64.64/64.67 [137]~P15(x1371,x1372,x1373)+P16(x1371,x1372,x1373) % 64.64/64.67 [132]P4(x1321)+~P2(x1321,f29(f4(x1322,x1323))) % 64.64/64.67 [139]~P16(x1391,x1392,x1393)+P2(x1391,f29(f4(x1392,x1393))) % 64.64/64.67 [141]~P15(x1413,x1411,x1412)+E(f31(x1411,x1412,x1413,x1414),f30(x1413,x1414)) % 64.64/64.67 [144]~P15(x1443,x1441,x1442)+P16(f31(x1441,x1442,x1443,x1444),x1441,x1442) % 64.64/64.67 [108]~P1(x1082)+~P1(x1081)+E(x1081,x1082) % 64.64/64.67 [115]~P7(x1151,x1152)+P9(x1151)+~P6(x1152) % 64.64/64.67 [116]~P17(x1161,x1162)+P9(x1161)+~P9(x1162) % 64.64/64.67 [119]~P2(x1192,x1191)+P1(x1191)+P8(x1192,x1191) % 64.64/64.67 [121]~P3(x1211)+~P4(x1211)+P3(f30(x1211,x1212)) % 64.64/64.67 [124]~P4(x1241)+~P12(x1241)+P12(f30(x1241,x1242)) % 64.64/64.67 [127]P1(x1271)+P1(x1272)+~P1(f4(x1272,x1271)) % 64.64/64.67 [128]~P6(x1281)+~P7(x1282,x1281)+P3(f32(x1281,x1282)) % 64.64/64.67 [131]~P6(x1311)+~P7(x1312,x1311)+P14(f27(x1311,x1312),x1311,x1312) % 64.64/64.67 [133]~P6(x1331)+~P7(x1332,x1331)+P16(f32(x1331,x1332),f28(x1332),f28(x1331)) % 64.64/64.67 [134]~P6(x1341)+~P7(x1342,x1341)+P10(f32(x1341,x1342),f28(x1342),f28(x1341)) % 64.64/64.67 [129]~P1(x1291)+~P8(x1292,x1293)+~P2(x1293,f29(x1291)) % 64.64/64.67 [130]P2(x1301,x1302)+~P8(x1301,x1303)+~P2(x1303,f29(x1302)) % 64.64/64.67 [110]~P1(x1101)+~P3(x1101)+~P4(x1101)+P5(x1101) % 64.64/64.67 [135]~P6(x1352)+~P14(x1351,x1352,x1353)+P7(x1351,x1352)+~P7(x1353,x1352) % 64.64/64.67 [138]~P7(x1382,x1383)+~P7(x1381,x1383)+~P14(x1381,x1383,x1382)+P17(x1381,x1382)+~P6(x1383) % 64.64/64.67 [142]~P6(x1422)+~P7(x1421,x1422)+~P7(x1423,x1422)+~P14(x1423,x1422,x1421)+E(f31(f28(x1421),f28(x1422),f32(x1422,x1421),f28(x1423)),f32(x1422,x1423)) % 64.64/64.67 [143]~P6(x1432)+~P7(x1433,x1432)+~P7(x1431,x1432)+~P17(x1431,x1433)+P14(x1431,x1432,x1433)+~E(f31(f28(x1433),f28(x1432),f32(x1432,x1433),f28(x1431)),f32(x1432,x1431)) % 64.64/64.67 [140]~P9(x1401)+~P11(x1406,x1405,x1404)+P11(x1401,x1402,x1403)+~E(x1403,x1404)+~E(x1402,x1405)+~P17(x1406,x1401)+~P2(x1404,f28(x1406))+~P2(x1405,f28(x1406))+~P2(x1403,f28(x1401))+~P2(x1402,f28(x1401)) % 64.64/64.67 %EqnAxiom % 64.64/64.67 [1]E(x11,x11) % 64.64/64.67 [2]E(x22,x21)+~E(x21,x22) % 64.64/64.67 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 64.64/64.67 [4]~E(x41,x42)+E(f11(x41),f11(x42)) % 64.64/64.67 [5]~E(x51,x52)+E(f28(x51),f28(x52)) % 64.64/64.67 [6]~E(x61,x62)+E(f32(x61,x63),f32(x62,x63)) % 64.64/64.67 [7]~E(x71,x72)+E(f32(x73,x71),f32(x73,x72)) % 64.64/64.67 [8]~E(x81,x82)+E(f31(x81,x83,x84,x85),f31(x82,x83,x84,x85)) % 64.64/64.67 [9]~E(x91,x92)+E(f31(x93,x91,x94,x95),f31(x93,x92,x94,x95)) % 64.64/64.67 [10]~E(x101,x102)+E(f31(x103,x104,x101,x105),f31(x103,x104,x102,x105)) % 64.64/64.67 [11]~E(x111,x112)+E(f31(x113,x114,x115,x111),f31(x113,x114,x115,x112)) % 64.64/64.67 [12]~E(x121,x122)+E(f30(x121,x123),f30(x122,x123)) % 64.64/64.67 [13]~E(x131,x132)+E(f30(x133,x131),f30(x133,x132)) % 64.64/64.67 [14]~E(x141,x142)+E(f22(x141),f22(x142)) % 64.64/64.67 [15]~E(x151,x152)+E(f4(x151,x153),f4(x152,x153)) % 64.64/64.67 [16]~E(x161,x162)+E(f4(x163,x161),f4(x163,x162)) % 64.64/64.67 [17]~E(x171,x172)+E(f29(x171),f29(x172)) % 64.64/64.67 [18]~E(x181,x182)+E(f23(x181,x183),f23(x182,x183)) % 64.64/64.67 [19]~E(x191,x192)+E(f23(x193,x191),f23(x193,x192)) % 64.64/64.67 [20]~E(x201,x202)+E(f25(x201,x203),f25(x202,x203)) % 64.64/64.67 [21]~E(x211,x212)+E(f25(x213,x211),f25(x213,x212)) % 64.64/64.67 [22]~E(x221,x222)+E(f27(x221,x223),f27(x222,x223)) % 64.64/64.67 [23]~E(x231,x232)+E(f27(x233,x231),f27(x233,x232)) % 64.64/64.67 [24]~E(x241,x242)+E(f8(x241),f8(x242)) % 64.64/64.67 [25]~E(x251,x252)+E(f24(x251),f24(x252)) % 64.64/64.67 [26]~E(x261,x262)+E(f26(x261),f26(x262)) % 64.64/64.67 [27]~P1(x271)+P1(x272)+~E(x271,x272) % 64.64/64.67 [28]P15(x282,x283,x284)+~E(x281,x282)+~P15(x281,x283,x284) % 64.64/64.67 [29]P15(x293,x292,x294)+~E(x291,x292)+~P15(x293,x291,x294) % 64.64/64.67 [30]P15(x303,x304,x302)+~E(x301,x302)+~P15(x303,x304,x301) % 64.64/64.67 [31]P16(x312,x313,x314)+~E(x311,x312)+~P16(x311,x313,x314) % 64.64/64.67 [32]P16(x323,x322,x324)+~E(x321,x322)+~P16(x323,x321,x324) % 64.64/64.67 [33]P16(x333,x334,x332)+~E(x331,x332)+~P16(x333,x334,x331) % 64.64/64.67 [34]P17(x342,x343)+~E(x341,x342)+~P17(x341,x343) % 64.64/64.67 [35]P17(x353,x352)+~E(x351,x352)+~P17(x353,x351) % 64.64/64.67 [36]~P3(x361)+P3(x362)+~E(x361,x362) % 64.64/64.67 [37]P7(x372,x373)+~E(x371,x372)+~P7(x371,x373) % 64.64/64.67 [38]P7(x383,x382)+~E(x381,x382)+~P7(x383,x381) % 64.64/64.67 [39]~P6(x391)+P6(x392)+~E(x391,x392) % 64.64/64.67 [40]P2(x402,x403)+~E(x401,x402)+~P2(x401,x403) % 64.64/64.67 [41]P2(x413,x412)+~E(x411,x412)+~P2(x413,x411) % 64.64/64.67 [42]P10(x422,x423,x424)+~E(x421,x422)+~P10(x421,x423,x424) % 64.64/64.67 [43]P10(x433,x432,x434)+~E(x431,x432)+~P10(x433,x431,x434) % 64.64/64.67 [44]P10(x443,x444,x442)+~E(x441,x442)+~P10(x443,x444,x441) % 64.64/64.67 [45]~P4(x451)+P4(x452)+~E(x451,x452) % 64.64/64.67 [46]~P9(x461)+P9(x462)+~E(x461,x462) % 64.64/64.67 [47]P8(x472,x473)+~E(x471,x472)+~P8(x471,x473) % 64.64/64.67 [48]P8(x483,x482)+~E(x481,x482)+~P8(x483,x481) % 64.64/64.67 [49]P11(x492,x493,x494)+~E(x491,x492)+~P11(x491,x493,x494) % 64.64/64.67 [50]P11(x503,x502,x504)+~E(x501,x502)+~P11(x503,x501,x504) % 64.64/64.67 [51]P11(x513,x514,x512)+~E(x511,x512)+~P11(x513,x514,x511) % 64.64/64.67 [52]P14(x522,x523,x524)+~E(x521,x522)+~P14(x521,x523,x524) % 64.64/64.67 [53]P14(x533,x532,x534)+~E(x531,x532)+~P14(x533,x531,x534) % 64.64/64.67 [54]P14(x543,x544,x542)+~E(x541,x542)+~P14(x543,x544,x541) % 64.64/64.67 [55]~P12(x551)+P12(x552)+~E(x551,x552) % 64.64/64.67 [56]P13(x562,x563)+~E(x561,x562)+~P13(x561,x563) % 64.64/64.67 [57]P13(x573,x572)+~E(x571,x572)+~P13(x573,x571) % 64.64/64.67 [58]~P5(x581)+P5(x582)+~E(x581,x582) % 64.64/64.67 % 64.64/64.67 %------------------------------------------- % 64.64/64.67 cnf(145,plain, % 64.64/64.67 (E(a2,a1)), % 64.64/64.67 inference(scs_inference,[],[59,2])). % 64.64/64.67 cnf(146,plain, % 64.64/64.67 (~P8(x1461,a3)), % 64.64/64.67 inference(scs_inference,[],[59,62,2,113])). % 64.64/64.67 cnf(148,plain, % 64.64/64.67 (P13(f22(f29(x1481)),x1481)), % 64.64/64.67 inference(scs_inference,[],[59,95,62,2,113,126])). % 64.64/64.67 cnf(149,plain, % 64.64/64.67 (P2(f22(x1491),x1491)), % 64.64/64.67 inference(rename_variables,[],[95])). % 64.64/64.67 cnf(154,plain, % 64.64/64.67 (P15(f23(a1,x1541),a2,x1541)), % 64.64/64.67 inference(scs_inference,[],[59,99,95,96,62,2,113,126,132,29])). % 64.64/64.67 cnf(155,plain, % 64.64/64.67 (P15(f23(x1551,x1552),x1551,x1552)), % 64.64/64.67 inference(rename_variables,[],[99])). % 64.64/64.67 cnf(156,plain, % 64.64/64.67 (P15(f23(x1561,a1),x1561,a2)), % 64.64/64.67 inference(scs_inference,[],[59,99,155,95,96,62,2,113,126,132,29,30])). % 64.64/64.67 cnf(158,plain, % 64.64/64.67 (P16(f25(a1,x1581),a2,x1581)), % 64.64/64.67 inference(scs_inference,[],[59,99,155,100,95,96,62,2,113,126,132,29,30,32])). % 64.64/64.67 cnf(159,plain, % 64.64/64.67 (P16(f25(x1591,x1592),x1591,x1592)), % 64.64/64.67 inference(rename_variables,[],[100])). % 64.64/64.67 cnf(160,plain, % 64.64/64.67 (P16(f25(x1601,a1),x1601,a2)), % 64.64/64.67 inference(scs_inference,[],[59,99,155,100,159,95,96,62,2,113,126,132,29,30,32,33])). % 64.64/64.67 cnf(162,plain, % 64.64/64.67 (P2(a1,f28(a16))), % 64.64/64.67 inference(scs_inference,[],[59,91,99,155,100,159,95,96,62,2,113,126,132,29,30,32,33,40])). % 64.64/64.67 cnf(164,plain, % 64.64/64.67 (P2(f22(x1641),x1641)), % 64.64/64.67 inference(rename_variables,[],[95])). % 64.64/64.67 cnf(166,plain, % 64.64/64.67 (P13(a2,a1)), % 64.64/64.67 inference(scs_inference,[],[59,98,91,90,99,155,100,159,95,149,96,62,2,113,126,132,29,30,32,33,40,41,50,56])). % 64.64/64.67 cnf(167,plain, % 64.64/64.67 (P13(x1671,x1671)), % 64.64/64.67 inference(rename_variables,[],[90])). % 64.64/64.67 cnf(168,plain, % 64.64/64.67 (P13(a1,a2)), % 64.64/64.67 inference(scs_inference,[],[59,98,91,90,167,99,155,100,159,95,149,96,62,2,113,126,132,29,30,32,33,40,41,50,56,57])). % 64.64/64.67 cnf(170,plain, % 64.64/64.67 (P8(f22(a10),a10)), % 64.64/64.67 inference(scs_inference,[],[59,98,91,90,167,99,155,100,159,95,149,164,96,62,101,2,113,126,132,29,30,32,33,40,41,50,56,57,119])). % 64.64/64.67 cnf(171,plain, % 64.64/64.67 (P2(f22(x1711),x1711)), % 64.64/64.67 inference(rename_variables,[],[95])). % 64.64/64.67 cnf(173,plain, % 64.64/64.67 (~P8(x1731,f22(f29(a3)))), % 64.64/64.67 inference(scs_inference,[],[59,98,91,90,167,99,155,100,159,95,149,164,171,96,62,101,2,113,126,132,29,30,32,33,40,41,50,56,57,119,129])). % 64.64/64.67 cnf(181,plain, % 64.64/64.67 (~E(a3,a18)+P1(a19)), % 64.64/64.67 inference(scs_inference,[],[59,60,98,91,90,167,99,155,100,159,95,149,164,171,96,62,64,67,75,101,2,113,126,132,29,30,32,33,40,41,50,56,57,119,129,110,125,3,27])). % 64.64/64.67 cnf(189,plain, % 64.64/64.67 (P13(f11(x1891),x1891)), % 64.64/64.67 inference(scs_inference,[],[63,96,113,126])). % 64.64/64.67 cnf(191,plain, % 64.64/64.67 (E(a19,a18)), % 64.64/64.67 inference(scs_inference,[],[60,63,96,113,126,2])). % 64.64/64.67 cnf(193,plain, % 64.64/64.67 (~P8(x1931,f22(f29(a5)))), % 64.64/64.67 inference(scs_inference,[],[60,98,63,95,96,113,126,2,51,129])). % 64.64/64.67 cnf(194,plain, % 64.64/64.67 (P2(f22(x1941),x1941)), % 64.64/64.67 inference(rename_variables,[],[95])). % 64.64/64.67 cnf(196,plain, % 64.64/64.67 (P8(f22(f29(x1961)),f29(x1961))), % 64.64/64.67 inference(scs_inference,[],[60,98,63,102,95,194,96,113,126,2,51,129,119])). % 64.64/64.67 cnf(199,plain, % 64.64/64.67 (P11(a17,a2,a18)), % 64.64/64.67 inference(scs_inference,[],[59,60,98,63,102,95,194,96,113,126,2,51,129,119,50])). % 64.64/64.67 cnf(204,plain, % 64.64/64.67 (P2(a19,f28(a16))), % 64.64/64.67 inference(scs_inference,[],[59,92,60,98,158,148,63,102,95,194,96,113,126,2,51,129,119,50,33,57,40])). % 64.64/64.67 cnf(205,plain, % 64.64/64.67 (P15(f23(a1,a1),a2,a2)), % 64.64/64.67 inference(scs_inference,[],[59,92,60,98,154,158,148,63,102,95,194,96,113,126,2,51,129,119,50,33,57,40,30])). % 64.64/64.67 cnf(209,plain, % 64.64/64.67 (~P8(f29(x2091),f22(f29(x2091)))), % 64.64/64.67 inference(scs_inference,[],[59,92,60,98,154,158,148,173,170,63,102,95,194,96,113,126,2,51,129,119,50,33,57,40,30,48,125])). % 64.64/64.67 cnf(217,plain, % 64.64/64.67 (~P8(x2171,f11(x2172))), % 64.64/64.67 inference(scs_inference,[],[88,113])). % 64.64/64.67 cnf(219,plain, % 64.64/64.67 (P8(f11(x2191),f29(x2191))), % 64.64/64.67 inference(scs_inference,[],[96,88,102,113,119])). % 64.64/64.67 cnf(222,plain, % 64.64/64.67 (P13(f11(a1),a2)), % 64.64/64.67 inference(scs_inference,[],[59,96,189,88,102,113,119,57])). % 64.64/64.67 cnf(224,plain, % 64.64/64.67 (P2(a2,f28(a17))), % 64.64/64.67 inference(scs_inference,[],[59,93,96,189,88,102,113,119,57,40])). % 64.64/64.67 cnf(239,plain, % 64.64/64.67 (~P8(x2391,f22(f29(a7)))), % 64.64/64.67 inference(scs_inference,[],[95,64,113,129])). % 64.64/64.67 cnf(242,plain, % 64.64/64.67 (P2(a18,f28(a17))), % 64.64/64.67 inference(scs_inference,[],[94,191,95,64,113,129,40])). % 64.64/64.67 cnf(245,plain, % 64.64/64.67 (P8(x2451,f29(x2452))+~E(f22(f29(x2452)),x2451)), % 64.64/64.67 inference(scs_inference,[],[94,191,95,196,217,64,113,129,40,48,47])). % 64.64/64.67 cnf(260,plain, % 64.64/64.67 (~E(f29(x2601),a3)), % 64.64/64.67 inference(scs_inference,[],[196,146,48])). % 64.64/64.67 cnf(264,plain, % 64.64/64.67 (~P1(a1)+P1(a2)), % 64.64/64.67 inference(scs_inference,[],[59,60,97,196,146,48,55,54,27])). % 64.64/64.67 cnf(266,plain, % 64.64/64.67 (P15(x2661,x2662,a2)+~E(f23(x2662,a1),x2661)), % 64.64/64.67 inference(scs_inference,[],[59,60,97,156,196,146,48,55,54,27,52,28])). % 64.64/64.67 cnf(292,plain, % 64.64/64.67 (P16(x2921,x2922,a2)+~E(f25(x2922,a1),x2921)), % 64.64/64.67 inference(scs_inference,[],[160,170,217,48,31])). % 64.64/64.67 cnf(312,plain, % 64.64/64.67 (P8(f22(a18),a18)+P1(a19)), % 64.64/64.67 inference(scs_inference,[],[60,95,170,193,48,27,119])). % 64.64/64.67 cnf(329,plain, % 64.64/64.67 (P15(x3291,a2,x3292)+~E(f23(a1,x3292),x3291)), % 64.64/64.67 inference(scs_inference,[],[60,154,170,146,48,58,28])). % 64.64/64.67 cnf(331,plain, % 64.64/64.67 (P13(x3311,a2)+~E(f11(a1),x3311)), % 64.64/64.67 inference(scs_inference,[],[60,154,222,170,146,48,58,28,36,56])). % 64.64/64.67 cnf(355,plain, % 64.64/64.67 (~P1(a18)+P4(a19)), % 64.64/64.67 inference(scs_inference,[],[60,45,106])). % 64.64/64.67 cnf(365,plain, % 64.64/64.67 (P16(x3651,a2,x3652)+~E(f25(a1,x3652),x3651)), % 64.64/64.67 inference(scs_inference,[],[158,191,145,99,28,55,36,31])). % 64.64/64.67 cnf(366,plain, % 64.64/64.67 (P8(x3661,f29(x3662))+~E(f11(x3662),x3661)), % 64.64/64.67 inference(scs_inference,[],[158,191,145,99,219,28,55,36,31,47])). % 64.64/64.67 cnf(411,plain, % 64.64/64.67 (~P8(a18,f22(a18))+P1(a18)), % 64.64/64.67 inference(scs_inference,[],[191,27,181,312,125])). % 64.64/64.67 cnf(418,plain, % 64.64/64.67 (P2(x4181,f29(x4182))+~E(f11(x4182),x4181)), % 64.64/64.67 inference(scs_inference,[],[96,40])). % 64.64/64.67 cnf(442,plain, % 64.64/64.67 (P13(x4421,x4422)+~E(f11(x4422),x4421)), % 64.64/64.67 inference(scs_inference,[],[91,145,95,189,58,46,27,40,41,56])). % 64.64/64.67 cnf(458,plain, % 64.64/64.67 (P17(a17,a16)+~P7(a17,a14)), % 64.64/64.67 inference(scs_inference,[],[94,97,89,82,148,65,72,56,41,110,138])). % 64.64/64.67 cnf(585,plain, % 64.64/64.67 (P13(a19,a18)), % 64.64/64.67 inference(scs_inference,[],[60,90,56])). % 64.64/64.67 cnf(589,plain, % 64.64/64.67 (P15(f23(a1,a18),a2,a19)), % 64.64/64.67 inference(scs_inference,[],[60,154,95,90,56,41,30])). % 64.64/64.67 cnf(591,plain, % 64.64/64.68 (P16(f25(a18,a1),a19,a2)), % 64.64/64.68 inference(scs_inference,[],[60,160,154,95,90,56,41,30,32])). % 64.64/64.68 cnf(593,plain, % 64.64/64.68 (P16(f25(a1,a18),a2,a19)), % 64.64/64.68 inference(scs_inference,[],[60,160,154,158,95,90,56,41,30,32,33])). % 64.64/64.68 cnf(595,plain, % 64.64/64.68 (P15(f23(a18,a1),a19,a2)), % 64.64/64.68 inference(scs_inference,[],[60,156,160,154,158,95,90,56,41,30,32,33,29])). % 64.64/64.68 cnf(597,plain, % 64.64/64.68 (P13(f11(a18),a19)), % 64.64/64.68 inference(scs_inference,[],[60,156,160,154,158,95,189,90,56,41,30,32,33,29,57])). % 64.64/64.68 cnf(608,plain, % 64.64/64.68 (P13(f22(f29(a18)),a19)), % 64.64/64.68 inference(scs_inference,[],[60,145,591,593,595,148,32,33,30,57])). % 64.64/64.68 cnf(611,plain, % 64.64/64.68 (P13(x6111,a19)+~E(f11(a18),x6111)), % 64.64/64.68 inference(scs_inference,[],[60,145,589,591,597,593,595,148,32,33,30,57,29,56])). % 64.64/64.68 cnf(617,plain, % 64.64/64.68 (P16(f25(a18,x6171),a19,x6171)), % 64.64/64.68 inference(scs_inference,[],[60,100,32])). % 64.64/64.68 cnf(618,plain, % 64.64/64.68 (P16(f25(x6181,x6182),x6181,x6182)), % 64.64/64.68 inference(rename_variables,[],[100])). % 64.64/64.68 cnf(619,plain, % 64.64/64.68 (P16(f25(x6191,a18),x6191,a19)), % 64.64/64.68 inference(scs_inference,[],[60,100,618,32,33])). % 64.64/64.68 cnf(621,plain, % 64.64/64.68 (P15(f23(x6211,a18),x6211,a19)), % 64.64/64.68 inference(scs_inference,[],[60,99,100,618,32,33,30])). % 64.64/64.68 cnf(622,plain, % 64.64/64.68 (P15(f23(x6221,x6222),x6221,x6222)), % 64.64/64.68 inference(rename_variables,[],[99])). % 64.64/64.68 cnf(623,plain, % 64.64/64.68 (P13(a18,a19)), % 64.64/64.68 inference(scs_inference,[],[60,99,100,618,90,32,33,30,57])). % 64.64/64.68 cnf(625,plain, % 64.64/64.68 (P15(f23(a18,x6251),a19,x6251)), % 64.64/64.68 inference(scs_inference,[],[60,99,622,100,618,90,32,33,30,57,29])). % 64.64/64.68 cnf(633,plain, % 64.64/64.68 (P16(f25(a18,a18),a19,a19)), % 64.64/64.68 inference(scs_inference,[],[60,619,32])). % 64.64/64.68 cnf(637,plain, % 64.64/64.68 (P16(x6371,a19,x6372)+~E(f25(a18,x6372),x6371)), % 64.64/64.68 inference(scs_inference,[],[60,617,619,621,32,29,31])). % 64.64/64.68 cnf(644,plain, % 64.64/64.68 (P16(x6441,x6442,a19)+~E(f25(x6442,a18),x6441)), % 64.64/64.68 inference(scs_inference,[],[619,31])). % 64.64/64.68 cnf(645,plain, % 64.64/64.68 (P15(x6451,a19,x6452)+~E(f23(a18,x6452),x6451)), % 64.64/64.68 inference(scs_inference,[],[625,619,31,28])). % 64.64/64.68 cnf(656,plain, % 64.64/64.68 (P15(x6561,x6562,a19)+~E(f23(x6562,a18),x6561)), % 64.64/64.68 inference(scs_inference,[],[621,28])). % 64.64/64.68 cnf(678,plain, % 64.64/64.68 (P2(f8(a1),f29(a1))+P1(a2)), % 64.64/64.68 inference(scs_inference,[],[264,114])). % 64.64/64.68 cnf(838,plain, % 64.64/64.68 (~P8(a18,f22(a18))+P4(a19)), % 64.64/64.68 inference(scs_inference,[],[355,411])). % 64.64/64.68 cnf(1213,plain, % 64.64/64.68 (~P1(f8(f29(x12131)))), % 64.64/64.68 inference(scs_inference,[],[260,104,109])). % 64.64/64.68 cnf(2419,plain, % 64.64/64.68 (P17(a17,a16)), % 64.64/64.68 inference(scs_inference,[],[89,82,97,458,135])). % 64.64/64.68 cnf(2440,plain, % 64.64/64.68 (~P8(a19,f22(a18))+P4(a19)), % 64.64/64.68 inference(scs_inference,[],[191,838,47])). % 64.64/64.68 cnf(2840,plain, % 64.64/64.68 (~P8(a19,x28401)+~E(x28401,f22(a18))+P4(a19)), % 64.64/64.68 inference(scs_inference,[],[2440,48])). % 64.64/64.68 cnf(3051,plain, % 64.64/64.68 (P8(f11(a18),f29(a19))), % 64.64/64.68 inference(scs_inference,[],[597,102,120,119])). % 64.64/64.68 cnf(3071,plain, % 64.64/64.68 (P13(f8(a1),a1)+P1(a2)), % 64.64/64.68 inference(scs_inference,[],[678,126])). % 64.64/64.68 cnf(3087,plain, % 64.64/64.68 (P13(f8(a1),a2)+P1(a2)), % 64.64/64.68 inference(scs_inference,[],[59,3071,57])). % 64.64/64.68 cnf(3103,plain, % 64.64/64.68 (P2(f8(a1),f29(a2))+P1(a2)), % 64.64/64.68 inference(scs_inference,[],[3087,120])). % 64.64/64.68 cnf(3295,plain, % 64.64/64.68 (P8(f8(a1),f29(a2))+P1(a2)), % 64.64/64.68 inference(scs_inference,[],[102,3103,119])). % 64.64/64.68 cnf(3408,plain, % 64.64/64.68 (~P8(f29(a2),f8(a1))+P1(a2)), % 64.64/64.68 inference(scs_inference,[],[3295,125])). % 64.64/64.68 cnf(3520,plain, % 64.64/64.68 (~P8(f29(a2),x35201)+~E(x35201,f8(a1))+P1(a2)), % 64.64/64.68 inference(scs_inference,[],[3408,48])). % 64.64/64.68 cnf(3793,plain, % 64.64/64.68 (E(f11(a2),f11(a1))), % 64.64/64.68 inference(scs_inference,[],[59,4,2])). % 64.64/64.68 cnf(3796,plain, % 64.64/64.68 (E(f11(a1),f11(a2))), % 64.64/64.68 inference(scs_inference,[],[3793,366,418,2])). % 64.64/64.68 cnf(3801,plain, % 64.64/64.68 (~P4(f11(a2))+P4(f11(a1))), % 64.64/64.68 inference(scs_inference,[],[3793,366,418,2,442,58,39,46,45])). % 64.64/64.68 cnf(3803,plain, % 64.64/64.68 (~P3(f11(a2))+P3(f11(a1))), % 64.64/64.68 inference(scs_inference,[],[3793,366,418,2,442,58,39,46,45,41,36])). % 64.64/64.68 cnf(3805,plain, % 64.64/64.68 (P8(f11(a2),f29(a1))), % 64.64/64.68 inference(scs_inference,[],[3796,366])). % 64.64/64.68 cnf(3811,plain, % 64.64/64.68 (~P4(f11(a1))+P4(f11(a2))), % 64.64/64.68 inference(scs_inference,[],[3793,3796,366,418,55,39,46,58,45])). % 64.64/64.68 cnf(3815,plain, % 64.64/64.68 (~P3(f11(a1))+P3(f11(a2))), % 64.64/64.68 inference(scs_inference,[],[3796,55,36])). % 64.64/64.68 cnf(3878,plain, % 64.64/64.68 (P4(f11(a1))), % 64.64/64.68 inference(scs_inference,[],[88,3801,106])). % 64.64/64.68 cnf(3879,plain, % 64.64/64.68 (P4(f11(a2))), % 64.64/64.68 inference(scs_inference,[],[3878,3811])). % 64.64/64.68 cnf(3894,plain, % 64.64/64.68 (P3(f11(a1))), % 64.64/64.68 inference(scs_inference,[],[88,3803,105])). % 64.64/64.68 cnf(3895,plain, % 64.64/64.68 (P3(f11(a2))), % 64.64/64.68 inference(scs_inference,[],[3894,3815])). % 64.64/64.68 cnf(4057,plain, % 64.64/64.68 (E(f28(a2),f28(a1))), % 64.64/64.68 inference(scs_inference,[],[59,5,2])). % 64.64/64.68 cnf(4058,plain, % 64.64/64.68 (E(f28(a1),f28(a2))), % 64.64/64.68 inference(scs_inference,[],[4057,2])). % 64.64/64.68 cnf(4109,plain, % 64.64/64.68 (P1(f22(f29(a7)))), % 64.64/64.68 inference(scs_inference,[],[95,239,119])). % 64.64/64.68 cnf(4114,plain, % 64.64/64.68 (P1(f22(f29(a3)))), % 64.64/64.68 inference(scs_inference,[],[95,173,119])). % 64.64/64.68 cnf(4119,plain, % 64.64/64.68 (P1(f22(f29(a5)))), % 64.64/64.68 inference(scs_inference,[],[95,193,119])). % 64.64/64.68 cnf(4164,plain, % 64.64/64.68 (~P8(x41641,f22(f29(x41642)))+~E(x41641,f29(x41642))), % 64.64/64.68 inference(scs_inference,[],[209,47])). % 64.64/64.68 cnf(4198,plain, % 64.64/64.68 (P6(a15)), % 64.64/64.68 inference(scs_inference,[],[83,107])). % 64.64/64.68 cnf(6257,plain, % 64.64/64.68 (~P1(f8(a10))), % 64.64/64.68 inference(scs_inference,[],[101,109])). % 64.64/64.68 cnf(6261,plain, % 64.64/64.68 (P7(f24(a15),a15)), % 64.64/64.68 inference(scs_inference,[],[4198,101,3051,109,117,111])). % 64.64/64.68 cnf(6265,plain, % 64.64/64.68 (P4(f30(a5,x62651))), % 64.64/64.68 inference(scs_inference,[],[74,4198,101,3051,83,109,117,111,112,118])). % 64.64/64.68 cnf(6267,plain, % 64.64/64.68 (P15(f25(a18,a18),a19,a19)), % 64.64/64.68 inference(scs_inference,[],[74,4198,633,101,3051,83,109,117,111,112,118,136])). % 64.64/64.68 cnf(6269,plain, % 64.64/64.68 (P16(f23(a1,a1),a2,a2)), % 64.64/64.68 inference(scs_inference,[],[74,4198,633,205,101,3051,83,109,117,111,112,118,136,137])). % 64.64/64.68 cnf(6271,plain, % 64.64/64.68 (P2(f8(a10),f29(a10))), % 64.64/64.68 inference(scs_inference,[],[74,4198,633,205,101,3051,83,109,117,111,112,118,136,137,114])). % 64.64/64.68 cnf(6275,plain, % 64.64/64.68 (E(f8(a1),f8(a2))), % 64.64/64.68 inference(scs_inference,[],[59,74,4198,633,205,101,3051,4058,83,109,117,111,112,118,136,137,114,4,5,24])). % 64.64/64.68 cnf(6276,plain, % 64.64/64.68 (E(f24(a1),f24(a2))), % 64.64/64.68 inference(scs_inference,[],[59,74,4198,633,205,101,3051,4058,83,109,117,111,112,118,136,137,114,4,5,24,25])). % 64.64/64.68 cnf(6286,plain, % 64.64/64.68 (E(f23(a1,x62861),f23(a2,x62861))), % 64.64/64.68 inference(scs_inference,[],[59,74,4198,633,205,101,3051,4058,83,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18])). % 64.64/64.68 cnf(6287,plain, % 64.64/64.68 (E(f23(x62871,a1),f23(x62871,a2))), % 64.64/64.68 inference(scs_inference,[],[59,74,4198,633,205,101,3051,4058,83,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19])). % 64.64/64.68 cnf(6288,plain, % 64.64/64.68 (E(f25(a1,x62881),f25(a2,x62881))), % 64.64/64.68 inference(scs_inference,[],[59,74,4198,633,205,101,3051,4058,83,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20])). % 64.64/64.68 cnf(6289,plain, % 64.64/64.68 (E(f25(x62891,a1),f25(x62891,a2))), % 64.64/64.68 inference(scs_inference,[],[59,74,4198,633,205,101,3051,4058,83,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21])). % 64.64/64.68 cnf(6296,plain, % 64.64/64.68 (E(f31(a1,x62961,x62962,x62963),f31(a2,x62961,x62962,x62963))), % 64.64/64.68 inference(scs_inference,[],[59,74,4198,633,205,101,3051,4058,83,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8])). % 64.64/64.68 cnf(6297,plain, % 64.64/64.68 (E(f31(x62971,a1,x62972,x62973),f31(x62971,a2,x62972,x62973))), % 64.64/64.68 inference(scs_inference,[],[59,74,4198,633,205,101,3051,4058,83,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9])). % 64.64/64.68 cnf(6298,plain, % 64.64/64.68 (E(f31(x62981,x62982,a1,x62983),f31(x62981,x62982,a2,x62983))), % 64.64/64.68 inference(scs_inference,[],[59,74,4198,633,205,101,3051,4058,83,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10])). % 64.64/64.68 cnf(6299,plain, % 64.64/64.68 (E(f31(x62991,x62992,x62993,a1),f31(x62991,x62992,x62993,a2))), % 64.64/64.68 inference(scs_inference,[],[59,74,4198,633,205,101,3051,4058,83,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10,11])). % 64.64/64.68 cnf(6301,plain, % 64.64/64.68 (P3(f22(f29(a7)))), % 64.64/64.68 inference(scs_inference,[],[59,74,4198,4109,633,205,101,3051,4058,83,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10,11,14,105])). % 64.64/64.68 cnf(6305,plain, % 64.64/64.68 (P4(f22(f29(a7)))), % 64.64/64.68 inference(scs_inference,[],[59,74,4198,4109,633,205,101,3051,4058,83,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10,11,14,105,104,106])). % 64.64/64.68 cnf(6307,plain, % 64.64/64.68 (P2(a19,f29(a18))), % 64.64/64.68 inference(scs_inference,[],[59,74,4198,4109,585,633,205,101,3051,4058,83,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10,11,14,105,104,106,120])). % 64.64/64.68 cnf(6310,plain, % 64.64/64.68 (P8(a3,f29(a7))), % 64.64/64.68 inference(scs_inference,[],[59,74,4198,4109,585,633,205,101,3051,4058,83,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10,11,14,105,104,106,120,2,245])). % 64.64/64.68 cnf(6311,plain, % 64.64/64.68 (E(f29(a1),f29(a2))), % 64.64/64.68 inference(scs_inference,[],[59,74,4198,4109,585,633,205,101,3051,4058,83,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10,11,14,105,104,106,120,2,245,17])). % 64.64/64.68 cnf(6316,plain, % 64.64/64.68 (~P1(f4(a10,a10))), % 64.64/64.68 inference(scs_inference,[],[59,74,85,4198,3879,4109,3895,585,633,205,73,101,3051,4058,83,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10,11,14,105,104,106,120,2,245,17,121,124,127])). % 64.64/64.68 cnf(6320,plain, % 64.64/64.68 (P14(f27(a15,f24(a15)),a15,f24(a15))), % 64.64/64.68 inference(scs_inference,[],[59,74,85,4198,3879,4109,3895,585,633,205,73,101,3051,4058,83,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10,11,14,105,104,106,120,2,245,17,121,124,127,128,131])). % 64.64/64.68 cnf(6326,plain, % 64.64/64.68 (P9(f26(a15))), % 64.64/64.68 inference(scs_inference,[],[59,74,85,4198,3879,4109,3895,585,633,205,73,101,3051,4058,83,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10,11,14,105,104,106,120,2,245,17,121,124,127,128,131,133,134,116])). % 64.64/64.68 cnf(6329,plain, % 64.64/64.68 (~P2(f29(a1),f29(f11(x63291)))), % 64.64/64.68 inference(scs_inference,[],[59,74,85,4198,3879,1213,4109,3805,3895,585,633,205,73,101,3051,88,4058,83,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10,11,14,105,104,106,120,2,245,17,121,124,127,128,131,133,134,116,27,129])). % 64.64/64.68 cnf(6331,plain, % 64.64/64.68 (P8(f22(f29(a1)),f29(a2))), % 64.64/64.68 inference(scs_inference,[],[59,74,85,4198,3879,1213,4109,3805,3895,585,633,205,73,101,3051,88,4058,196,83,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10,11,14,105,104,106,120,2,245,17,121,124,127,128,131,133,134,116,27,129,48])). % 64.64/64.68 cnf(6333,plain, % 64.64/64.68 (P3(a3)), % 64.64/64.68 inference(scs_inference,[],[59,74,85,4198,3879,1213,4109,3805,3895,585,633,205,73,101,3051,88,4058,196,83,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10,11,14,105,104,106,120,2,245,17,121,124,127,128,131,133,134,116,27,129,48,36])). % 64.64/64.68 cnf(6334,plain, % 64.64/64.68 (P8(f22(f8(a10)),f8(a10))), % 64.64/64.68 inference(scs_inference,[],[59,74,85,4198,3879,1213,4109,3805,3895,585,633,205,73,101,3051,88,4058,196,83,95,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10,11,14,105,104,106,120,2,245,17,121,124,127,128,131,133,134,116,27,129,48,36,119])). % 64.64/64.68 cnf(6337,plain, % 64.64/64.68 (P9(f24(a15))), % 64.64/64.68 inference(scs_inference,[],[59,74,85,4198,3879,1213,4109,3805,3895,585,633,205,73,101,3051,88,4058,196,83,95,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10,11,14,105,104,106,120,2,245,17,121,124,127,128,131,133,134,116,27,129,48,36,119,115])). % 64.64/64.68 cnf(6341,plain, % 64.64/64.68 (~P11(a16,a1,a18)), % 64.64/64.68 inference(scs_inference,[],[59,74,85,4198,3879,1213,4109,3805,3895,585,633,205,103,73,101,3051,88,4058,196,191,83,95,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10,11,14,105,104,106,120,2,245,17,121,124,127,128,131,133,134,116,27,129,48,36,119,115,51,3,50])). % 64.64/64.68 cnf(6342,plain, % 64.64/64.68 (P7(a17,a14)), % 64.64/64.68 inference(scs_inference,[],[59,74,85,4198,3879,1213,4109,3805,3895,585,633,205,103,73,101,3051,88,4058,82,196,191,89,97,83,95,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10,11,14,105,104,106,120,2,245,17,121,124,127,128,131,133,134,116,27,129,48,36,119,115,51,3,50,135])). % 64.64/64.68 cnf(6344,plain, % 64.64/64.68 (P5(a3)), % 64.64/64.68 inference(scs_inference,[],[59,74,85,4198,3879,1213,4109,3805,3895,585,633,205,103,71,73,101,3051,88,4058,62,82,196,191,89,97,83,95,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10,11,14,105,104,106,120,2,245,17,121,124,127,128,131,133,134,116,27,129,48,36,119,115,51,3,50,135,110])). % 64.64/64.68 cnf(6348,plain, % 64.64/64.68 (P15(f23(a2,a1),a1,a2)), % 64.64/64.68 inference(scs_inference,[],[59,74,85,4198,3879,1213,4109,3805,3895,585,633,205,103,71,73,101,3051,88,4058,62,82,196,191,89,97,83,95,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10,11,14,105,104,106,120,2,245,17,121,124,127,128,131,133,134,116,27,129,48,36,119,115,51,3,50,135,110,142,266])). % 64.64/64.68 cnf(6349,plain, % 64.64/64.68 (P16(f25(a2,a1),a1,a2)), % 64.64/64.68 inference(scs_inference,[],[59,74,85,4198,3879,1213,4109,3805,3895,585,633,205,103,71,73,101,3051,88,4058,62,82,196,191,89,97,83,95,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10,11,14,105,104,106,120,2,245,17,121,124,127,128,131,133,134,116,27,129,48,36,119,115,51,3,50,135,110,142,266,292])). % 64.64/64.68 cnf(6350,plain, % 64.64/64.68 (P15(f23(a1,a2),a2,a1)), % 64.64/64.68 inference(scs_inference,[],[59,74,85,4198,3879,1213,4109,3805,3895,585,633,205,103,71,73,101,3051,88,4058,62,82,196,191,89,97,83,95,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10,11,14,105,104,106,120,2,245,17,121,124,127,128,131,133,134,116,27,129,48,36,119,115,51,3,50,135,110,142,266,292,329])). % 64.64/64.68 cnf(6351,plain, % 64.64/64.68 (P16(f25(a1,a2),a2,a1)), % 64.64/64.68 inference(scs_inference,[],[59,74,85,4198,3879,1213,4109,3805,3895,585,633,205,103,71,73,101,3051,88,4058,62,82,196,191,89,97,83,95,109,117,111,112,118,136,137,114,4,5,24,25,26,139,6,7,12,13,15,16,18,19,20,21,22,23,144,141,8,9,10,11,14,105,104,106,120,2,245,17,121,124,127,128,131,133,134,116,27,129,48,36,119,115,51,3,50,135,110,142,266,292,329,365])). % 64.64/64.68 cnf(6381,plain, % 64.64/64.68 (P16(f25(a18,a2),a19,a1)), % 64.64/64.68 inference(scs_inference,[],[6289,637])). % 64.64/64.68 cnf(6383,plain, % 64.64/64.68 (P16(f25(a2,a18),a1,a19)), % 64.64/64.68 inference(scs_inference,[],[6288,6289,637,644])). % 64.64/64.68 cnf(6385,plain, % 64.64/64.68 (P15(f23(a18,a2),a19,a1)), % 64.64/64.68 inference(scs_inference,[],[6287,6288,6289,637,644,645])). % 64.64/64.68 cnf(6387,plain, % 64.64/64.68 (P15(f23(a2,a18),a1,a19)), % 64.64/64.68 inference(scs_inference,[],[6286,6287,6288,6289,637,644,645,656])). % 64.64/64.68 cnf(6388,plain, % 64.64/64.68 (E(f23(a1,x63881),f23(a2,x63881))), % 64.64/64.68 inference(rename_variables,[],[6286])). % 64.64/64.68 cnf(6389,plain, % 64.64/64.68 (P16(f31(a19,a19,f25(a18,a18),x63891),a19,a19)), % 64.64/64.68 inference(scs_inference,[],[6286,6287,6288,6289,6267,637,644,645,656,144])). % 64.64/64.68 cnf(6393,plain, % 64.64/64.68 (P7(f24(a21),a21)), % 64.64/64.68 inference(scs_inference,[],[6286,6287,6288,6289,6326,6267,81,637,644,645,656,144,112,111])). % 64.64/64.68 cnf(6395,plain, % 64.64/64.68 (~P1(f8(f8(a10)))), % 64.64/64.68 inference(scs_inference,[],[6286,6287,6288,6289,6257,6326,6267,81,637,644,645,656,144,112,111,109])). % 64.64/64.68 cnf(6400,plain, % 64.64/64.68 (E(f31(x64001,x64002,x64003,a2),f31(x64001,x64002,x64003,a1))), % 64.64/64.68 inference(scs_inference,[],[6286,6287,6288,6289,6257,6326,6267,81,145,191,637,644,645,656,144,112,111,109,4,6,25,11])). % 64.64/64.68 cnf(6404,plain, % 64.64/64.68 (E(f31(x64041,a2,x64042,x64043),f31(x64041,a1,x64042,x64043))), % 64.64/64.68 inference(scs_inference,[],[6286,6287,6288,6289,6257,6326,6267,81,145,191,637,644,645,656,144,112,111,109,4,6,25,11,18,24,22,9])). % 64.64/64.68 cnf(6407,plain, % 64.64/64.68 (E(f25(x64071,a2),f25(x64071,a1))), % 64.64/64.68 inference(scs_inference,[],[6286,6287,6288,6289,6257,6326,6267,6349,81,145,191,637,644,645,656,144,112,111,109,4,6,25,11,18,24,22,9,136,21])). % 64.64/64.68 cnf(6416,plain, % 64.64/64.68 (P4(f30(a10,x64161))), % 64.64/64.68 inference(scs_inference,[],[76,6286,6287,6288,6289,6257,6326,6267,6348,6349,4114,81,145,191,637,644,645,656,144,112,111,109,4,6,25,11,18,24,22,9,136,21,23,137,19,15,104,7,118])). % 64.64/64.68 cnf(6423,plain, % 64.64/64.68 (E(f31(x64231,x64232,a2,x64233),f31(x64231,x64232,a1,x64233))), % 64.64/64.68 inference(scs_inference,[],[76,6286,6287,6288,6289,6310,6257,6326,6267,6269,6348,6349,4114,81,145,191,637,644,645,656,144,112,111,109,4,6,25,11,18,24,22,9,136,21,23,137,19,15,104,7,118,12,117,139,10])). % 64.64/64.68 cnf(6429,plain, % 64.64/64.68 (E(f31(a2,x64291,x64292,x64293),f31(a1,x64291,x64292,x64293))), % 64.64/64.68 inference(scs_inference,[],[76,6286,6287,6288,6289,6310,6257,6326,6267,6269,6348,6349,4114,81,145,191,637,644,645,656,144,112,111,109,4,6,25,11,18,24,22,9,136,21,23,137,19,15,104,7,118,12,117,139,10,106,14,20,5,8])). % 64.64/64.68 cnf(6435,plain, % 64.64/64.68 (P2(a18,f29(a19))), % 64.64/64.68 inference(scs_inference,[],[76,6286,6287,6288,6289,6310,6257,6326,6267,6269,6348,6349,4114,623,81,145,191,637,644,645,656,144,112,111,109,4,6,25,11,18,24,22,9,136,21,23,137,19,15,104,7,118,12,117,139,10,106,14,20,5,8,26,13,16,105,120])). % 64.64/64.68 cnf(6438,plain, % 64.64/64.68 (~P8(f8(a10),f22(f8(a10)))), % 64.64/64.68 inference(scs_inference,[],[76,6286,6287,6288,6289,6310,6257,6311,6326,6267,6269,6348,6349,6334,4114,623,81,145,191,637,644,645,656,144,112,111,109,4,6,25,11,18,24,22,9,136,21,23,137,19,15,104,7,118,12,117,139,10,106,14,20,5,8,26,13,16,105,120,2,125])). % 64.64/64.68 cnf(6440,plain, % 64.64/64.68 (P8(a3,f29(a3))), % 64.64/64.68 inference(scs_inference,[],[76,6286,6287,6288,6289,6310,6257,6311,6326,6267,6269,6348,6349,6334,4114,623,81,145,191,637,644,645,656,144,112,111,109,4,6,25,11,18,24,22,9,136,21,23,137,19,15,104,7,118,12,117,139,10,106,14,20,5,8,26,13,16,105,120,2,125,245])). % 64.64/64.68 cnf(6446,plain, % 64.64/64.68 (P14(f27(a14,a17),a14,a17)), % 64.64/64.68 inference(scs_inference,[],[76,6333,6342,6286,6287,6288,6289,6310,6257,6311,6326,6267,6269,6348,6349,6334,4114,623,81,71,82,145,191,637,644,645,656,144,112,111,109,4,6,25,11,18,24,22,9,136,21,23,137,19,15,104,7,118,12,117,139,10,106,14,20,5,8,26,13,16,105,120,2,125,245,17,121,134,131])). % 64.64/64.68 cnf(6448,plain, % 64.64/64.68 (~P1(f4(f8(a10),f8(a10)))), % 64.64/64.68 inference(scs_inference,[],[76,6333,6342,6286,6287,6288,6289,6310,6257,6311,6326,6267,6269,6348,6349,6334,4114,623,81,71,82,145,191,637,644,645,656,144,112,111,109,4,6,25,11,18,24,22,9,136,21,23,137,19,15,104,7,118,12,117,139,10,106,14,20,5,8,26,13,16,105,120,2,125,245,17,121,134,131,127])). % 64.64/64.68 cnf(6452,plain, % 64.64/64.68 (P12(f30(a13,x64521))), % 64.64/64.68 inference(scs_inference,[],[76,78,86,6333,6342,6286,6287,6288,6289,6310,6257,6311,6326,6267,6269,6348,6349,6334,4114,623,81,71,82,145,191,637,644,645,656,144,112,111,109,4,6,25,11,18,24,22,9,136,21,23,137,19,15,104,7,118,12,117,139,10,106,14,20,5,8,26,13,16,105,120,2,125,245,17,121,134,131,127,133,124])). % 64.64/64.68 cnf(6459,plain, % 64.64/64.68 (P8(f11(a19),f29(a18))), % 64.64/64.68 inference(scs_inference,[],[76,78,86,6333,6342,6286,6287,6288,6289,6310,6257,6311,6326,6267,6269,6348,6349,6334,4114,623,81,71,219,82,145,191,637,644,645,656,144,112,111,109,4,6,25,11,18,24,22,9,136,21,23,137,19,15,104,7,118,12,117,139,10,106,14,20,5,8,26,13,16,105,120,2,125,245,17,121,134,131,127,133,124,128,27,116,48])). % 64.64/64.68 cnf(6462,plain, % 64.64/64.68 (P8(f8(a10),f29(a10))), % 64.64/64.68 inference(scs_inference,[],[76,78,86,6333,6342,6286,6287,6288,6289,6310,6257,6271,6311,6326,6267,6269,6348,6349,6334,6329,4114,623,81,71,219,102,82,145,191,637,644,645,656,144,112,111,109,4,6,25,11,18,24,22,9,136,21,23,137,19,15,104,7,118,12,117,139,10,106,14,20,5,8,26,13,16,105,120,2,125,245,17,121,134,131,127,133,124,128,27,116,48,40,119])). % 64.64/64.68 cnf(6465,plain, % 64.64/64.68 (P9(a17)), % 64.64/64.68 inference(scs_inference,[],[76,78,86,6333,6342,6286,6287,6288,6289,6310,6257,6271,6311,6326,6267,6269,6348,6349,6334,6329,4114,623,81,71,219,102,82,145,191,637,644,645,656,144,112,111,109,4,6,25,11,18,24,22,9,136,21,23,137,19,15,104,7,118,12,117,139,10,106,14,20,5,8,26,13,16,105,120,2,125,245,17,121,134,131,127,133,124,128,27,116,48,40,119,115])). % 64.64/64.68 cnf(6467,plain, % 64.64/64.68 (~P11(a16,a1,a19)), % 64.64/64.68 inference(scs_inference,[],[76,78,86,6333,6341,6342,6286,6287,6288,6289,6310,6257,6271,6311,6326,6267,6269,6348,6349,6334,6329,4114,623,81,71,219,102,82,145,191,637,644,645,656,144,112,111,109,4,6,25,11,18,24,22,9,136,21,23,137,19,15,104,7,118,12,117,139,10,106,14,20,5,8,26,13,16,105,120,2,125,245,17,121,134,131,127,133,124,128,27,116,48,40,119,115,51])). % 64.64/64.68 cnf(6468,plain, % 64.64/64.68 (E(f31(a1,a1,x64681,x64682),f31(a2,a2,x64681,x64682))), % 64.64/64.68 inference(scs_inference,[],[76,78,86,6333,6341,6342,6296,6297,6286,6287,6288,6289,6310,6257,6271,6311,6326,6267,6269,6348,6349,6334,6329,4114,623,81,71,219,102,82,145,191,637,644,645,656,144,112,111,109,4,6,25,11,18,24,22,9,136,21,23,137,19,15,104,7,118,12,117,139,10,106,14,20,5,8,26,13,16,105,120,2,125,245,17,121,134,131,127,133,124,128,27,116,48,40,119,115,51,3])). % 64.64/64.68 cnf(6471,plain, % 64.64/64.68 (P7(f27(a15,f24(a15)),a15)), % 64.64/64.68 inference(scs_inference,[],[76,78,86,6333,6341,6342,6296,6297,6286,6287,6288,6289,6310,6257,6271,6311,6326,6267,6269,6261,6348,6349,6334,6320,6329,4114,623,81,71,219,4198,102,82,145,191,637,644,645,656,144,112,111,109,4,6,25,11,18,24,22,9,136,21,23,137,19,15,104,7,118,12,117,139,10,106,14,20,5,8,26,13,16,105,120,2,125,245,17,121,134,131,127,133,124,128,27,116,48,40,119,115,51,3,135])). % 64.64/64.68 cnf(6476,plain, % 64.64/64.68 (P15(f23(a2,a2),a2,a1)), % 64.64/64.68 inference(scs_inference,[],[76,78,86,6333,6341,6342,6296,6297,6286,6388,6287,6288,6289,6310,6257,6271,6311,6326,6267,6269,6261,6348,6349,6350,6334,6320,6329,4114,623,81,71,219,4198,102,82,145,191,637,644,645,656,144,112,111,109,4,6,25,11,18,24,22,9,136,21,23,137,19,15,104,7,118,12,117,139,10,106,14,20,5,8,26,13,16,105,120,2,125,245,17,121,134,131,127,133,124,128,27,116,48,40,119,115,51,3,135,4164,3520,28])). % 64.64/64.68 cnf(6497,plain, % 64.64/64.68 (P7(f24(a14),a14)), % 64.64/64.68 inference(scs_inference,[],[6465,6351,6265,6316,6459,6385,82,60,112,144,117,139,109,4,118,111])). % 64.64/64.68 cnf(6499,plain, % 64.64/64.68 (P15(f25(a1,a2),a2,a1)), % 64.64/64.68 inference(scs_inference,[],[6465,6351,6265,6316,6459,6385,82,60,112,144,117,139,109,4,118,111,136])). % 64.64/64.68 cnf(6503,plain, % 64.64/64.68 (E(f31(x65031,x65032,x65033,a19),f31(x65031,x65032,x65033,a18))), % 64.64/64.68 inference(scs_inference,[],[6465,6351,6265,6316,6459,6385,4119,82,191,60,112,144,117,139,109,4,118,111,136,106,11])). % 64.64/64.68 cnf(6510,plain, % 64.64/64.68 (P16(f23(a18,a2),a19,a1)), % 64.64/64.68 inference(scs_inference,[],[6465,6351,6265,6316,6459,6385,4119,82,191,60,112,144,117,139,109,4,118,111,136,106,11,22,25,104,19,23,137])). % 64.64/64.68 cnf(6512,plain, % 64.64/64.68 (E(f31(x65121,a19,x65122,x65123),f31(x65121,a18,x65122,x65123))), % 64.64/64.68 inference(scs_inference,[],[6465,6351,6265,6316,6459,6385,4119,82,191,60,112,144,117,139,109,4,118,111,136,106,11,22,25,104,19,23,137,9])). % 64.64/64.68 cnf(6524,plain, % 64.64/64.68 (P2(a1,f29(a2))), % 64.64/64.68 inference(scs_inference,[],[6465,6351,6265,6316,6459,6385,4119,168,82,191,60,112,144,117,139,109,4,118,111,136,106,11,22,25,104,19,23,137,9,7,15,12,6,20,5,13,18,26,21,14,120])). % 64.64/64.68 cnf(6529,plain, % 64.64/64.68 (E(f31(x65291,x65292,a19,x65293),f31(x65291,x65292,a18,x65293))), % 64.64/64.68 inference(scs_inference,[],[6465,6351,6265,6316,6459,6385,4119,168,82,191,60,112,144,117,139,109,4,118,111,136,106,11,22,25,104,19,23,137,9,7,15,12,6,20,5,13,18,26,21,14,120,24,105,10])). % 64.64/64.68 cnf(6531,plain, % 64.64/64.68 (E(f31(a19,x65311,x65312,x65313),f31(a18,x65311,x65312,x65313))), % 64.64/64.68 inference(scs_inference,[],[6465,6351,6265,6316,6459,6385,4119,168,82,191,60,112,144,117,139,109,4,118,111,136,106,11,22,25,104,19,23,137,9,7,15,12,6,20,5,13,18,26,21,14,120,24,105,10,16,8])). % 64.64/64.68 cnf(6535,plain, % 64.64/64.68 (P8(a3,f29(a5))), % 64.64/64.68 inference(scs_inference,[],[6465,6351,6468,6265,6316,6459,6462,6385,4119,168,82,191,60,112,144,117,139,109,4,118,111,136,106,11,22,25,104,19,23,137,9,7,15,12,6,20,5,13,18,26,21,14,120,24,105,10,16,8,125,2,245])). % 64.64/64.68 cnf(6536,plain, % 64.64/64.68 (E(f29(a18),f29(a19))), % 64.64/64.68 inference(scs_inference,[],[6465,6351,6468,6265,6316,6459,6462,6385,4119,168,82,191,60,112,144,117,139,109,4,118,111,136,106,11,22,25,104,19,23,137,9,7,15,12,6,20,5,13,18,26,21,14,120,24,105,10,16,8,125,2,245,17])). % 64.64/64.68 cnf(6543,plain, % 64.64/64.68 (P14(f27(a21,f24(a21)),a21,f24(a21))), % 64.64/64.68 inference(scs_inference,[],[87,6465,6351,6468,6265,6316,6459,6462,6393,6385,4119,168,79,81,82,191,89,60,112,144,117,139,109,4,118,111,136,106,11,22,25,104,19,23,137,9,7,15,12,6,20,5,13,18,26,21,14,120,24,105,10,16,8,125,2,245,17,124,134,127,131])). % 64.64/64.68 cnf(6551,plain, % 64.64/64.68 (P9(f26(a17))), % 64.64/64.68 inference(scs_inference,[],[87,6465,6351,6468,6265,6316,6459,6462,6393,6385,4119,168,72,79,65,81,82,191,89,60,112,144,117,139,109,4,118,111,136,106,11,22,25,104,19,23,137,9,7,15,12,6,20,5,13,18,26,21,14,120,24,105,10,16,8,125,2,245,17,124,134,127,131,121,133,128,116])). % 64.64/64.68 cnf(6555,plain, % 64.64/64.68 (P8(f22(f4(a10,a10)),f4(a10,a10))), % 64.64/64.68 inference(scs_inference,[],[87,6465,6351,6468,6265,6316,6459,6462,6393,6385,4119,168,72,79,6334,65,81,82,191,89,60,95,112,144,117,139,109,4,118,111,136,106,11,22,25,104,19,23,137,9,7,15,12,6,20,5,13,18,26,21,14,120,24,105,10,16,8,125,2,245,17,124,134,127,131,121,133,128,116,47,27,119])). % 64.64/64.68 cnf(6561,plain, % 64.64/64.68 (P9(f24(a21))), % 64.64/64.68 inference(scs_inference,[],[87,6465,6351,6468,6265,6407,6316,6459,6462,6393,6385,6438,4119,168,72,79,6334,65,81,82,191,89,60,95,112,144,117,139,109,4,118,111,136,106,11,22,25,104,19,23,137,9,7,15,12,6,20,5,13,18,26,21,14,120,24,105,10,16,8,125,2,245,17,124,134,127,131,121,133,128,116,47,27,119,48,40,115])). % 64.64/64.68 cnf(6563,plain, % 64.64/64.68 (E(f31(x65631,x65632,a1,a1),f31(x65631,x65632,a2,a2))), % 64.64/64.68 inference(scs_inference,[],[87,6465,6351,6298,6299,6468,6265,6407,6316,6459,6462,6393,6385,6438,4119,168,72,79,6334,65,81,82,191,89,60,95,112,144,117,139,109,4,118,111,136,106,11,22,25,104,19,23,137,9,7,15,12,6,20,5,13,18,26,21,14,120,24,105,10,16,8,125,2,245,17,124,134,127,131,121,133,128,116,47,27,119,48,40,115,3])). % 64.64/64.68 cnf(6566,plain, % 64.64/64.68 (P7(f27(a14,a17),a14)), % 64.64/64.68 inference(scs_inference,[],[87,6465,6351,6298,6299,6468,6265,6407,6316,6459,6462,6393,6385,6446,6438,4119,168,72,79,6334,65,81,6342,82,191,89,60,95,112,144,117,139,109,4,118,111,136,106,11,22,25,104,19,23,137,9,7,15,12,6,20,5,13,18,26,21,14,120,24,105,10,16,8,125,2,245,17,124,134,127,131,121,133,128,116,47,27,119,48,40,115,3,135])). % 64.64/64.68 cnf(6571,plain, % 64.64/64.68 (~P9(a16)), % 64.64/64.68 inference(scs_inference,[],[59,6467,87,6465,6351,6298,6299,6468,6265,6407,6316,6459,6462,6393,6385,6446,6438,4119,168,199,224,72,79,6334,65,162,204,242,81,6342,2419,82,191,89,60,95,112,144,117,139,109,4,118,111,136,106,11,22,25,104,19,23,137,9,7,15,12,6,20,5,13,18,26,21,14,120,24,105,10,16,8,125,2,245,17,124,134,127,131,121,133,128,116,47,27,119,48,40,115,3,135,4164,2840,140])). % 64.64/64.68 cnf(6577,plain, % 64.64/64.68 (P15(f25(a18,a2),a19,a1)), % 64.64/64.68 inference(scs_inference,[],[6381,139,136])). % 64.64/64.68 cnf(6588,plain, % 64.64/64.68 (P4(f11(x65881))), % 64.64/64.68 inference(scs_inference,[],[6381,6387,6416,6440,6337,88,60,139,136,112,117,144,118,22,106])). % 64.64/64.68 cnf(6590,plain, % 64.64/64.68 (E(f31(x65901,x65902,x65903,a18),f31(x65901,x65902,x65903,a19))), % 64.64/64.68 inference(scs_inference,[],[6381,6387,6416,6440,6337,88,60,139,136,112,117,144,118,22,106,11])). % 64.64/64.68 cnf(6591,plain, % 64.64/64.68 (P16(f23(a2,a18),a1,a19)), % 64.64/64.68 inference(scs_inference,[],[6381,6387,6416,6440,6337,88,60,139,136,112,117,144,118,22,106,11,137])). % 64.64/64.68 cnf(6593,plain, % 64.64/64.68 (E(f23(x65931,a18),f23(x65931,a19))), % 64.64/64.68 inference(scs_inference,[],[6381,6387,6416,6440,6337,88,60,139,136,112,117,144,118,22,106,11,137,19])). % 64.64/64.68 cnf(6594,plain, % 64.64/64.68 (P2(a2,f29(a1))), % 64.64/64.68 inference(scs_inference,[],[6381,6387,6416,6440,6337,166,88,60,139,136,112,117,144,118,22,106,11,137,19,120])). % 64.64/64.68 cnf(6597,plain, % 64.64/64.68 (E(a5,a3)), % 64.64/64.68 inference(scs_inference,[],[6381,6387,6416,6440,6337,166,63,88,60,139,136,112,117,144,118,22,106,11,137,19,120,12,104])). % 64.64/64.68 cnf(6599,plain, % 64.64/64.68 (P3(a5)), % 64.64/64.68 inference(scs_inference,[],[6381,6387,6416,6440,6337,166,63,88,60,139,136,112,117,144,118,22,106,11,137,19,120,12,104,105])). % 64.64/64.68 cnf(6605,plain, % 64.64/64.68 (E(f25(x66051,a18),f25(x66051,a19))), % 64.64/64.68 inference(scs_inference,[],[6381,6387,6416,6440,6337,166,63,88,60,139,136,112,117,144,118,22,106,11,137,19,120,12,104,105,7,23,26,6,21])). % 64.64/64.68 cnf(6609,plain, % 64.64/64.68 (E(f23(a18,x66091),f23(a19,x66091))), % 64.64/64.68 inference(scs_inference,[],[6381,6387,6416,6440,6337,166,63,88,60,139,136,112,117,144,118,22,106,11,137,19,120,12,104,105,7,23,26,6,21,13,5,25,18])). % 64.64/64.68 cnf(6610,plain, % 64.64/64.68 (E(f25(a18,x66101),f25(a19,x66101))), % 64.64/64.68 inference(scs_inference,[],[6381,6387,6416,6440,6337,166,63,88,60,139,136,112,117,144,118,22,106,11,137,19,120,12,104,105,7,23,26,6,21,13,5,25,18,20])). % 64.64/64.68 cnf(6621,plain, % 64.64/64.68 (E(f29(a5),f29(a3))), % 64.64/64.68 inference(scs_inference,[],[6381,6387,6563,6416,6440,6337,6555,166,63,88,60,139,136,112,117,144,118,22,106,11,137,19,120,12,104,105,7,23,26,6,21,13,5,25,18,20,9,10,15,24,14,125,8,16,2,17])). % 64.64/64.68 cnf(6626,plain, % 64.64/64.68 (~P1(f4(f29(x66261),f29(x66261)))), % 64.64/64.68 inference(scs_inference,[],[6381,6387,6563,6416,6440,6337,6497,6555,84,166,71,63,88,102,82,60,139,136,112,117,144,118,22,106,11,137,19,120,12,104,105,7,23,26,6,21,13,5,25,18,20,9,10,15,24,14,125,8,16,2,17,124,131,127])). % 64.64/64.68 cnf(6636,plain, % 64.64/64.68 (P8(a19,f29(a18))), % 64.64/64.68 inference(scs_inference,[],[6571,6381,6387,6563,6416,6440,6337,6307,6497,6555,84,3878,3894,166,71,6257,4109,63,88,102,82,60,139,136,112,117,144,118,22,106,11,137,19,120,12,104,105,7,23,26,6,21,13,5,25,18,20,9,10,15,24,14,125,8,16,2,17,124,131,127,46,128,121,116,27,119])). % 64.64/64.68 cnf(6639,plain, % 64.64/64.68 (P8(a18,f29(a18))), % 64.64/64.68 inference(scs_inference,[],[6571,6381,6387,6563,6416,6440,6337,6307,6497,6555,84,3878,3894,166,71,6257,4109,63,88,102,82,60,191,139,136,112,117,144,118,22,106,11,137,19,120,12,104,105,7,23,26,6,21,13,5,25,18,20,9,10,15,24,14,125,8,16,2,17,124,131,127,46,128,121,116,27,119,47])). % 64.64/64.68 cnf(6640,plain, % 64.64/64.68 (P9(f24(a14))), % 64.64/64.68 inference(scs_inference,[],[6571,6381,6387,6563,6416,6440,6337,6307,6497,6555,84,3878,3894,166,71,6257,4109,63,88,102,82,60,191,139,136,112,117,144,118,22,106,11,137,19,120,12,104,105,7,23,26,6,21,13,5,25,18,20,9,10,15,24,14,125,8,16,2,17,124,131,127,46,128,121,116,27,119,47,115])). % 64.64/64.68 cnf(6645,plain, % 64.64/64.68 (P7(f27(a14,f24(a14)),a14)), % 64.64/64.68 inference(scs_inference,[],[6571,6381,6387,6400,6404,6563,6416,6440,6337,6307,6497,6555,84,3878,3894,166,71,6257,4109,63,88,102,82,60,191,139,136,112,117,144,118,22,106,11,137,19,120,12,104,105,7,23,26,6,21,13,5,25,18,20,9,10,15,24,14,125,8,16,2,17,124,131,127,46,128,121,116,27,119,47,115,3,135])). % 64.64/64.68 cnf(6647,plain, % 64.64/64.68 (P15(f23(a19,a18),a18,a19)), % 64.64/64.68 inference(scs_inference,[],[6571,6381,6387,6400,6404,6563,6416,6440,6337,6307,6497,6555,84,3878,3894,166,71,6257,4109,63,88,102,82,60,191,139,136,112,117,144,118,22,106,11,137,19,120,12,104,105,7,23,26,6,21,13,5,25,18,20,9,10,15,24,14,125,8,16,2,17,124,131,127,46,128,121,116,27,119,47,115,3,135,656])). % 64.64/64.68 cnf(6648,plain, % 64.64/64.68 (P15(f23(a1,a19),a2,a18)), % 64.64/64.68 inference(scs_inference,[],[6571,6381,6387,6400,6404,6563,6416,6440,6337,6307,6497,6555,84,3878,3894,166,71,6257,4109,63,88,102,82,60,191,139,136,112,117,144,118,22,106,11,137,19,120,12,104,105,7,23,26,6,21,13,5,25,18,20,9,10,15,24,14,125,8,16,2,17,124,131,127,46,128,121,116,27,119,47,115,3,135,656,329])). % 64.64/64.68 cnf(6649,plain, % 64.64/64.68 (P16(f25(a18,a19),a19,a18)), % 64.64/64.68 inference(scs_inference,[],[6571,6381,6387,6400,6404,6563,6416,6440,6337,6307,6497,6555,84,3878,3894,166,71,6257,4109,63,88,102,82,60,191,139,136,112,117,144,118,22,106,11,137,19,120,12,104,105,7,23,26,6,21,13,5,25,18,20,9,10,15,24,14,125,8,16,2,17,124,131,127,46,128,121,116,27,119,47,115,3,135,656,329,637])). % 64.64/64.68 cnf(6650,plain, % 64.64/64.68 (P16(f25(a19,a1),a18,a2)), % 64.64/64.68 inference(scs_inference,[],[6571,6381,6387,6400,6404,6563,6416,6440,6337,6307,6497,6555,84,3878,3894,166,71,6257,4109,63,88,102,82,60,191,139,136,112,117,144,118,22,106,11,137,19,120,12,104,105,7,23,26,6,21,13,5,25,18,20,9,10,15,24,14,125,8,16,2,17,124,131,127,46,128,121,116,27,119,47,115,3,135,656,329,637,292])). % 64.64/64.68 cnf(6670,plain, % 64.64/64.68 (P15(f25(a2,a18),a1,a19)), % 64.64/64.68 inference(scs_inference,[],[6383,6535,6593,6605,6609,6610,6551,645,266,365,644,117,139,112,136])). % 64.64/64.68 cnf(6674,plain, % 64.64/64.68 (P3(f11(x66741))), % 64.64/64.68 inference(scs_inference,[],[6383,6535,6593,6605,6609,6610,6551,608,88,645,266,365,644,117,139,112,136,120,105])). % 64.64/64.68 cnf(6676,plain, % 64.64/64.68 (E(f31(x66761,x66762,x66763,a5),f31(x66761,x66762,x66763,a3))), % 64.64/64.68 inference(scs_inference,[],[6597,6383,6535,6593,6605,6609,6610,6551,608,88,645,266,365,644,117,139,112,136,120,105,11])). % 64.64/64.68 cnf(6683,plain, % 64.64/64.68 (E(f23(x66831,a5),f23(x66831,a3))), % 64.64/64.68 inference(scs_inference,[],[6597,6588,6383,6535,6593,6605,6609,6610,6551,6577,6476,608,88,645,266,365,644,117,139,112,136,120,105,11,118,137,144,19])). % 64.64/64.68 cnf(6686,plain, % 64.64/64.68 (E(a7,a3)), % 64.64/64.68 inference(scs_inference,[],[6597,6588,6383,6535,6593,6605,6609,6610,6551,6577,6476,608,64,88,645,266,365,644,117,139,112,136,120,105,11,118,137,144,19,22,13,104])). % 64.64/64.68 cnf(6692,plain, % 64.64/64.68 (E(f31(x66921,x66922,a5,x66923),f31(x66921,x66922,a3,x66923))), % 64.64/64.68 inference(scs_inference,[],[6597,6588,6383,6535,6593,6605,6609,6610,6551,6577,6476,608,64,88,645,266,365,644,117,139,112,136,120,105,11,118,137,144,19,22,13,104,6,7,23,5,10])). % 64.64/64.68 cnf(6693,plain, % 64.64/64.68 (E(f23(a5,x66931),f23(a3,x66931))), % 64.64/64.68 inference(scs_inference,[],[6597,6588,6383,6535,6593,6605,6609,6610,6551,6577,6476,608,64,88,645,266,365,644,117,139,112,136,120,105,11,118,137,144,19,22,13,104,6,7,23,5,10,18])). % 64.64/64.68 cnf(6695,plain, % 64.64/64.68 (E(f25(a5,x66951),f25(a3,x66951))), % 64.64/64.68 inference(scs_inference,[],[6597,6588,6383,6535,6593,6605,6609,6610,6551,6577,6476,608,64,88,645,266,365,644,117,139,112,136,120,105,11,118,137,144,19,22,13,104,6,7,23,5,10,18,15,20])). % 64.64/64.68 cnf(6701,plain, % 64.64/64.68 (E(f25(x67011,a5),f25(x67011,a3))), % 64.64/64.68 inference(scs_inference,[],[6597,6588,6383,6535,6593,6605,6609,6610,6551,6577,6476,608,64,88,645,266,365,644,117,139,112,136,120,105,11,118,137,144,19,22,13,104,6,7,23,5,10,18,15,20,4,12,9,25,26,21])). % 64.64/64.68 cnf(6708,plain, % 64.64/64.68 (E(a3,a5)), % 64.64/64.68 inference(scs_inference,[],[6597,6588,6383,6535,6593,6605,6609,6610,6551,6577,6636,6476,608,64,88,645,266,365,644,117,139,112,136,120,105,11,118,137,144,19,22,13,104,6,7,23,5,10,18,15,20,4,12,9,25,26,21,125,14,8,24,16,2])). % 64.64/64.68 cnf(6709,plain, % 64.64/64.68 (E(f29(a7),f29(a3))), % 64.64/64.68 inference(scs_inference,[],[6597,6588,6383,6535,6593,6605,6609,6610,6551,6577,6636,6476,608,64,88,645,266,365,644,117,139,112,136,120,105,11,118,137,144,19,22,13,104,6,7,23,5,10,18,15,20,4,12,9,25,26,21,125,14,8,24,16,2,17])). % 64.64/64.68 cnf(6716,plain, % 64.64/64.68 (P3(f30(a5,x67161))), % 64.64/64.68 inference(scs_inference,[],[6344,6597,6599,6588,6383,6535,6593,6605,6609,6610,6551,6577,6566,6636,6476,74,6571,608,64,88,82,645,266,365,644,117,139,112,136,120,105,11,118,137,144,19,22,13,104,6,7,23,5,10,18,15,20,4,12,9,25,26,21,125,14,8,24,16,2,17,58,131,46,128,121])). % 64.64/64.68 cnf(6722,plain, % 64.64/64.68 (P8(a18,f29(a19))), % 64.64/64.68 inference(scs_inference,[],[6344,6597,6599,6588,6383,6535,6593,6605,6609,6610,6435,6551,6577,6566,6636,6476,6626,6536,74,6571,608,64,88,102,82,645,266,365,644,117,139,112,136,120,105,11,118,137,144,19,22,13,104,6,7,23,5,10,18,15,20,4,12,9,25,26,21,125,14,8,24,16,2,17,58,131,46,128,121,116,27,48,119])). % 64.64/64.68 cnf(6725,plain, % 64.64/64.68 (P8(a5,f29(a5))), % 64.64/64.68 inference(scs_inference,[],[6344,6597,6599,6588,6383,6535,6593,6605,6609,6610,6435,6551,6577,6566,6636,6476,6626,6536,74,6571,608,64,88,102,82,645,266,365,644,117,139,112,136,120,105,11,118,137,144,19,22,13,104,6,7,23,5,10,18,15,20,4,12,9,25,26,21,125,14,8,24,16,2,17,58,131,46,128,121,116,27,48,119,47])). % 64.64/64.68 cnf(6731,plain, % 64.64/64.68 (P7(f27(a21,f24(a21)),a21)), % 64.64/64.68 inference(scs_inference,[],[6344,6597,6599,6588,6383,6535,6423,6429,6593,6605,6609,6610,6435,6551,6577,6566,6636,6476,6543,6626,6471,6536,74,6571,608,6393,81,4198,64,88,102,82,645,266,365,644,117,139,112,136,120,105,11,118,137,144,19,22,13,104,6,7,23,5,10,18,15,20,4,12,9,25,26,21,125,14,8,24,16,2,17,58,131,46,128,121,116,27,48,119,47,115,3,135])). % 64.64/64.68 cnf(6733,plain, % 64.64/64.68 (P15(f23(a3,a18),a5,a19)), % 64.64/64.68 inference(scs_inference,[],[6344,6597,6599,6588,6383,6535,6423,6429,6593,6605,6609,6610,6435,6551,6577,6566,6636,6476,6543,6626,6471,6536,74,6571,608,6393,81,4198,64,88,102,82,645,266,365,644,117,139,112,136,120,105,11,118,137,144,19,22,13,104,6,7,23,5,10,18,15,20,4,12,9,25,26,21,125,14,8,24,16,2,17,58,131,46,128,121,116,27,48,119,47,115,3,135,656])). % 64.64/64.68 cnf(6735,plain, % 64.64/64.68 (P16(f25(a3,a1),a5,a2)), % 64.64/64.68 inference(scs_inference,[],[6344,6597,6599,6588,6383,6535,6423,6429,6593,6605,6609,6610,6435,6551,6577,6566,6636,6476,6543,6626,6471,6536,74,6571,608,6393,81,4198,64,88,102,82,645,266,365,644,117,139,112,136,120,105,11,118,137,144,19,22,13,104,6,7,23,5,10,18,15,20,4,12,9,25,26,21,125,14,8,24,16,2,17,58,131,46,128,121,116,27,48,119,47,115,3,135,656,329,292])). % 64.64/64.68 cnf(6736,plain, % 64.64/64.68 (P16(f25(a18,a3),a19,a5)), % 64.64/64.68 inference(scs_inference,[],[6344,6597,6599,6588,6383,6535,6423,6429,6593,6605,6609,6610,6435,6551,6577,6566,6636,6476,6543,6626,6471,6536,74,6571,608,6393,81,4198,64,88,102,82,645,266,365,644,117,139,112,136,120,105,11,118,137,144,19,22,13,104,6,7,23,5,10,18,15,20,4,12,9,25,26,21,125,14,8,24,16,2,17,58,131,46,128,121,116,27,48,119,47,115,3,135,656,329,292,637])). % 64.64/64.68 cnf(6753,plain, % 64.64/64.68 (P2(x67531,f29(x67531))), % 64.64/64.68 inference(scs_inference,[],[6649,6683,6695,6701,6561,6639,90,645,644,365,139,117,112,120])). % 64.64/64.68 cnf(6759,plain, % 64.64/64.68 (P4(f30(a7,x67591))), % 64.64/64.68 inference(scs_inference,[],[6649,6683,6693,6695,6701,6561,6639,75,90,645,644,365,139,117,112,120,266,136,118])). % 64.64/64.68 cnf(6762,plain, % 64.64/64.68 (E(f23(x67621,a7),f23(x67621,a3))), % 64.64/64.68 inference(scs_inference,[],[6686,6649,6683,6693,6695,6701,6561,6639,75,90,645,644,365,139,117,112,120,266,136,118,11,19])). % 64.64/64.68 cnf(6772,plain, % 64.64/64.68 (E(f11(x67721),a3)), % 64.64/64.68 inference(scs_inference,[],[6686,6708,6647,6649,6683,6693,6695,6701,6561,6639,75,90,88,645,644,365,139,117,112,120,266,136,118,11,19,137,144,22,4,125,23,104])). % 64.64/64.68 cnf(6778,plain, % 64.64/64.68 (E(f23(a7,x67781),f23(a3,x67781))), % 64.64/64.68 inference(scs_inference,[],[6686,6708,6647,6649,6683,6693,6695,6701,6561,6639,75,90,88,645,644,365,139,117,112,120,266,136,118,11,19,137,144,22,4,125,23,104,12,6,13,15,18])). % 64.64/64.68 cnf(6780,plain, % 64.64/64.68 (E(f25(a7,x67801),f25(a3,x67801))), % 64.64/64.68 inference(scs_inference,[],[6686,6708,6647,6649,6683,6693,6695,6701,6561,6639,75,90,88,645,644,365,139,117,112,120,266,136,118,11,19,137,144,22,4,125,23,104,12,6,13,15,18,5,20])). % 64.64/64.68 cnf(6782,plain, % 64.64/64.68 (E(f25(x67821,a7),f25(x67821,a3))), % 64.64/64.68 inference(scs_inference,[],[6686,6708,6647,6649,6683,6693,6695,6701,6561,6639,75,90,88,645,644,365,139,117,112,120,266,136,118,11,19,137,144,22,4,125,23,104,12,6,13,15,18,5,20,25,21])). % 64.64/64.68 cnf(6791,plain, % 64.64/64.68 (E(a3,a7)), % 64.64/64.68 inference(scs_inference,[],[6686,6708,6647,6649,6683,6693,6695,6701,6561,6639,75,90,88,645,644,365,139,117,112,120,266,136,118,11,19,137,144,22,4,125,23,104,12,6,13,15,18,5,20,25,21,10,7,8,26,9,24,14,16,2])). % 64.64/64.68 cnf(6803,plain, % 64.64/64.68 (P8(a5,f29(a3))), % 64.64/64.68 inference(scs_inference,[],[6686,6708,6674,6647,6649,6683,6693,6695,6701,6561,6639,6725,6621,75,6588,6571,90,88,82,89,645,644,365,139,117,112,120,266,136,118,11,19,137,144,22,4,125,23,104,12,6,13,15,18,5,20,25,21,10,7,8,26,9,24,14,16,2,17,131,128,116,46,121,48])). % 64.64/64.68 cnf(6804,plain, % 64.64/64.68 (P8(a1,f29(a2))), % 64.64/64.68 inference(scs_inference,[],[6686,6708,6674,6647,6649,6683,6693,6695,6701,6524,6561,6639,6725,6621,75,6588,6571,90,88,102,82,89,645,644,365,139,117,112,120,266,136,118,11,19,137,144,22,4,125,23,104,12,6,13,15,18,5,20,25,21,10,7,8,26,9,24,14,16,2,17,131,128,116,46,121,48,119])). % 64.64/64.68 cnf(6809,plain, % 64.64/64.68 (P9(f27(a21,f24(a21)))), % 64.64/64.68 inference(scs_inference,[],[59,6686,6708,6674,6647,6649,6683,6693,6695,6701,6524,6561,6639,6725,6731,6621,75,6588,6571,6257,4119,81,90,88,102,82,89,645,644,365,139,117,112,120,266,136,118,11,19,137,144,22,4,125,23,104,12,6,13,15,18,5,20,25,21,10,7,8,26,9,24,14,16,2,17,131,128,116,46,121,48,119,27,47,115])). % 64.64/64.68 cnf(6811,plain, % 64.64/64.68 (E(a7,a5)), % 64.64/64.68 inference(scs_inference,[],[59,6686,6708,6674,6647,6649,6683,6693,6695,6701,6524,6561,6639,6725,6731,6621,75,6588,6571,6257,4119,81,90,88,102,82,89,645,644,365,139,117,112,120,266,136,118,11,19,137,144,22,4,125,23,104,12,6,13,15,18,5,20,25,21,10,7,8,26,9,24,14,16,2,17,131,128,116,46,121,48,119,27,47,115,3])). % 64.64/64.68 cnf(6812,plain, % 64.64/64.68 (P13(a3,a2)), % 64.64/64.68 inference(scs_inference,[],[59,6686,6708,6674,6647,6649,6683,6693,6695,6701,6524,6561,6639,6725,6731,6621,75,6588,6571,6257,4119,81,90,88,102,82,89,645,644,365,139,117,112,120,266,136,118,11,19,137,144,22,4,125,23,104,12,6,13,15,18,5,20,25,21,10,7,8,26,9,24,14,16,2,17,131,128,116,46,121,48,119,27,47,115,3,331])). % 64.64/64.68 cnf(6813,plain, % 64.64/64.68 (P15(f23(a3,a18),a7,a19)), % 64.64/64.68 inference(scs_inference,[],[59,6686,6708,6674,6647,6649,6683,6693,6695,6701,6524,6561,6639,6725,6731,6621,75,6588,6571,6257,4119,81,90,88,102,82,89,645,644,365,139,117,112,120,266,136,118,11,19,137,144,22,4,125,23,104,12,6,13,15,18,5,20,25,21,10,7,8,26,9,24,14,16,2,17,131,128,116,46,121,48,119,27,47,115,3,331,656])). % 64.64/64.68 cnf(6822,plain, % 64.64/64.68 (P13(a3,a19)), % 64.64/64.68 inference(scs_inference,[],[6772,611])). % 64.64/64.68 cnf(6823,plain, % 64.64/64.68 (E(f11(x68231),a3)), % 64.64/64.68 inference(rename_variables,[],[6772])). % 64.64/64.68 cnf(6845,plain, % 64.64/64.68 (E(f23(x68451,a3),f23(x68451,a7))), % 64.64/64.68 inference(scs_inference,[],[6791,6812,6650,6762,6778,6780,6782,6759,6640,6772,6803,611,139,645,136,365,112,120,117,118,644,266,11,19])). % 64.64/64.68 cnf(6858,plain, % 64.64/64.68 (E(f23(a3,x68581),f23(a7,x68581))), % 64.64/64.68 inference(scs_inference,[],[6791,6812,6648,6650,6762,6778,6780,6782,6759,6722,6640,6772,6803,611,139,645,136,365,112,120,117,118,644,266,11,19,137,329,125,22,144,6,25,4,5,18])). % 64.64/64.68 cnf(6859,plain, % 64.64/64.68 (E(f25(x68591,a3),f25(x68591,a7))), % 64.64/64.68 inference(scs_inference,[],[6791,6812,6648,6650,6762,6778,6780,6782,6759,6722,6640,6772,6803,611,139,645,136,365,112,120,117,118,644,266,11,19,137,329,125,22,144,6,25,4,5,18,21])). % 64.64/64.68 cnf(6861,plain, % 64.64/64.68 (E(f25(a3,x68611),f25(a7,x68611))), % 64.64/64.68 inference(scs_inference,[],[6791,6812,6648,6650,6762,6778,6780,6782,6759,6722,6640,6772,6803,611,139,645,136,365,112,120,117,118,644,266,11,19,137,329,125,22,144,6,25,4,5,18,21,13,20])). % 64.64/64.68 cnf(6873,plain, % 64.64/64.68 (E(a5,a7)), % 64.64/64.68 inference(scs_inference,[],[6791,6811,6812,6648,6650,6762,6778,6780,6782,6759,6722,6640,6772,6803,611,139,645,136,365,112,120,117,118,644,266,11,19,137,329,125,22,144,6,25,4,5,18,21,13,20,15,23,7,26,12,9,10,8,16,14,24,2])). % 64.64/64.68 cnf(6876,plain, % 64.64/64.68 (P2(x68761,f29(x68761))), % 64.64/64.68 inference(rename_variables,[],[6753])). % 64.64/64.68 cnf(6880,plain, % 64.64/64.68 (~P2(f29(a19),f29(a3))), % 64.64/64.68 inference(scs_inference,[],[6791,6811,6812,6753,6648,6650,6512,6762,6778,6780,6782,6759,6722,6640,6772,6803,6331,6389,62,611,139,645,136,365,112,120,117,118,644,266,11,19,137,329,125,22,144,6,25,4,5,18,21,13,20,15,23,7,26,12,9,10,8,16,14,24,2,17,130,31,129])). % 64.64/64.68 cnf(6882,plain, % 64.64/64.68 (P13(a7,a2)), % 64.64/64.68 inference(scs_inference,[],[6791,6811,6812,6753,6648,6650,6512,6762,6778,6780,6782,6759,6722,6640,6772,6803,6331,6389,62,611,139,645,136,365,112,120,117,118,644,266,11,19,137,329,125,22,144,6,25,4,5,18,21,13,20,15,23,7,26,12,9,10,8,16,14,24,2,17,130,31,129,56])). % 64.64/64.68 cnf(6897,plain, % 64.64/64.68 (P8(x68971,f29(x68971))), % 64.64/64.68 inference(scs_inference,[],[59,6791,6811,6812,6753,6876,6648,6650,6512,6762,6778,6780,6782,6759,6722,6640,6772,6591,6510,6670,6499,6803,6331,6389,77,6536,68,6571,148,62,102,95,611,139,645,136,365,112,120,117,118,644,266,11,19,137,329,125,22,144,6,25,4,5,18,21,13,20,15,23,7,26,12,9,10,8,16,14,24,2,17,130,31,129,56,41,116,32,121,57,40,33,46,30,29,119])). % 64.64/64.68 cnf(6900,plain, % 64.64/64.68 (P8(a7,f29(a3))), % 64.64/64.68 inference(scs_inference,[],[59,6791,6811,6812,6753,6876,6648,6650,6512,6762,6778,6780,6782,6759,6722,6640,6772,6591,6510,6670,6499,6803,6331,6389,77,6440,6536,68,6571,148,62,102,95,611,139,645,136,365,112,120,117,118,644,266,11,19,137,329,125,22,144,6,25,4,5,18,21,13,20,15,23,7,26,12,9,10,8,16,14,24,2,17,130,31,129,56,41,116,32,121,57,40,33,46,30,29,119,47])). % 64.64/64.68 cnf(6902,plain, % 64.64/64.68 (P9(f27(a14,f24(a14)))), % 64.64/64.68 inference(scs_inference,[],[59,6791,6811,6812,6753,6876,6648,6650,6512,6762,6778,6780,6782,6759,6722,6640,6772,6591,6510,6670,6499,6803,6331,6395,6645,6389,77,6440,6536,68,6571,148,62,102,82,95,611,139,645,136,365,112,120,117,118,644,266,11,19,137,329,125,22,144,6,25,4,5,18,21,13,20,15,23,7,26,12,9,10,8,16,14,24,2,17,130,31,129,56,41,116,32,121,57,40,33,46,30,29,119,47,27,115])). % 64.64/64.68 cnf(6904,plain, % 64.64/64.68 (P8(a5,f29(a7))), % 64.64/64.68 inference(scs_inference,[],[59,6791,6811,6812,6753,6876,6648,6650,6512,6762,6778,6780,6782,6759,6722,6640,6772,6591,6510,6670,6499,6803,6331,6395,6645,6389,77,6440,6536,68,6571,148,62,102,82,95,611,139,645,136,365,112,120,117,118,644,266,11,19,137,329,125,22,144,6,25,4,5,18,21,13,20,15,23,7,26,12,9,10,8,16,14,24,2,17,130,31,129,56,41,116,32,121,57,40,33,46,30,29,119,47,27,115,48])). % 64.64/64.68 cnf(6905,plain, % 64.64/64.68 (E(f11(x69051),a7)), % 64.64/64.68 inference(scs_inference,[],[59,6791,6811,6812,6753,6876,6648,6650,6512,6762,6778,6780,6782,6759,6722,6640,6772,6823,6591,6510,6670,6499,6803,6331,6395,6645,6389,77,6440,6536,68,6571,148,62,102,82,95,611,139,645,136,365,112,120,117,118,644,266,11,19,137,329,125,22,144,6,25,4,5,18,21,13,20,15,23,7,26,12,9,10,8,16,14,24,2,17,130,31,129,56,41,116,32,121,57,40,33,46,30,29,119,47,27,115,48,3])). % 64.64/64.68 cnf(6918,plain, % 64.64/64.68 (P4(f30(a13,x69181))), % 64.64/64.68 inference(scs_inference,[],[6735,6905,78,611,136,139,118])). % 64.64/64.68 cnf(6927,plain, % 64.64/64.68 (E(f23(a3,x69271),f23(a7,x69271))), % 64.64/64.68 inference(rename_variables,[],[6858])). % 64.64/64.68 cnf(6933,plain, % 64.64/64.68 (~P8(f29(x69331),x69331)), % 64.64/64.68 inference(scs_inference,[],[6882,6873,6897,6735,6858,6859,6861,6845,6905,6900,78,611,136,139,118,645,117,120,266,365,11,644,125])). % 64.64/64.68 cnf(6937,plain, % 64.64/64.68 (E(f23(x69371,a5),f23(x69371,a7))), % 64.64/64.68 inference(scs_inference,[],[6882,6873,6897,6733,6735,6858,6859,6861,6845,6905,6900,78,611,136,139,118,645,117,120,266,365,11,644,125,137,19])). % 64.64/64.68 cnf(6944,plain, % 64.64/64.68 (E(f25(x69441,a5),f25(x69441,a7))), % 64.64/64.68 inference(scs_inference,[],[6882,6873,6897,6733,6735,6858,6859,6861,6845,6905,6900,78,611,136,139,118,645,117,120,266,365,11,644,125,137,19,144,22,4,6,13,21])). % 64.64/64.68 cnf(6946,plain, % 64.64/64.68 (E(f25(a5,x69461),f25(a7,x69461))), % 64.64/64.68 inference(scs_inference,[],[6882,6873,6897,6733,6735,6858,6859,6861,6845,6905,6900,78,611,136,139,118,645,117,120,266,365,11,644,125,137,19,144,22,4,6,13,21,5,20])). % 64.64/64.68 cnf(6948,plain, % 64.64/64.68 (P16(f25(a18,a7),a19,a5)), % 64.64/64.68 inference(scs_inference,[],[6882,6873,6897,6733,6735,6858,6859,6861,6845,6905,6900,78,611,136,139,118,645,117,120,266,365,11,644,125,137,19,144,22,4,6,13,21,5,20,15,637])). % 64.64/64.68 cnf(6950,plain, % 64.64/64.68 (E(f23(a5,x69501),f23(a7,x69501))), % 64.64/64.68 inference(scs_inference,[],[6882,6873,6897,6733,6735,6858,6859,6861,6845,6905,6900,78,611,136,139,118,645,117,120,266,365,11,644,125,137,19,144,22,4,6,13,21,5,20,15,637,23,18])). % 64.64/64.68 cnf(6968,plain, % 64.64/64.68 (~P2(f29(a19),f29(a7))), % 64.64/64.68 inference(scs_inference,[],[6882,6873,6897,6733,6735,6676,6858,6927,6859,6861,6845,6452,6880,6905,6900,6709,78,611,136,139,118,645,117,120,266,365,11,644,125,137,19,144,22,4,6,13,21,5,20,15,637,23,18,26,9,25,10,12,7,14,16,8,24,2,17,124,28,41])). % 64.64/64.68 cnf(6978,plain, % 64.64/64.68 (P9(f27(a14,a17))), % 64.64/64.68 inference(scs_inference,[],[6882,6873,6897,6275,6733,6735,6676,6594,6858,6927,6859,6861,6845,6452,6716,6880,6905,6900,6809,6709,6753,6265,78,6566,6571,102,82,611,136,139,118,645,117,120,266,365,11,644,125,137,19,144,22,4,6,13,21,5,20,15,637,23,18,26,9,25,10,12,7,14,16,8,24,2,17,124,28,41,121,40,46,119,115])). % 64.64/64.68 cnf(6993,plain, % 64.64/64.68 (P15(f23(a1,a7),a2,a5)), % 64.64/64.68 inference(scs_inference,[],[6882,6873,6897,6275,6733,6735,6503,6529,6676,6594,6858,6927,6859,6861,6845,6452,6716,6880,6905,6900,6809,6301,6305,6709,6753,6265,78,6555,6566,146,6571,6316,4109,102,82,611,136,139,118,645,117,120,266,365,11,644,125,137,19,144,22,4,6,13,21,5,20,15,637,23,18,26,9,25,10,12,7,14,16,8,24,2,17,124,28,41,121,40,46,119,115,47,48,27,3,110,112,292,329])). % 64.64/64.68 cnf(7009,plain, % 64.64/64.68 (P2(a3,f29(a19))), % 64.64/64.68 inference(scs_inference,[],[6822,6736,6918,6904,118,139,136,117,120])). % 64.64/64.68 cnf(7063,plain, % 64.64/64.68 (E(f31(a19,x70631,x70632,a18),f31(a18,x70631,x70632,a19))), % 64.64/64.68 inference(scs_inference,[],[6822,6933,6276,6813,6736,6531,6590,6692,6978,6937,6944,6946,6950,6918,6804,6968,6904,6902,6448,6905,3805,67,75,84,6536,6708,6571,63,95,118,139,136,117,120,365,645,125,644,266,144,11,137,22,5,4,13,23,20,19,26,9,18,15,6,21,10,7,14,25,12,8,24,16,2,17,55,41,116,121,40,46,47,27,48,3])). % 64.64/64.68 cnf(7382,plain, % 64.64/64.68 (P4(f30(a12,x73821))), % 64.64/64.68 inference(scs_inference,[],[79,118])). % 64.64/64.68 cnf(7440,plain, % 64.64/64.68 ($false), % 64.64/64.68 inference(scs_inference,[],[6993,6948,7009,7063,7382,6571,102,89,82,118,139,136,137,144,2,119,115]), % 64.64/64.68 ['proof']). % 64.64/64.68 % SZS output end Proof % 64.64/64.68 % Total time :64.050000s %------------------------------------------------------------------------------