%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU362+1 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n032.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 15:02:39 EDT 2024 % Result : Theorem 68.04s 68.22s % Output : CNFRefutation 68.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.07 % Problem : SEU362+1 : TPTP v8.2.0. Released v3.3.0. % 0.00/0.07 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.07/0.26 % Computer : n032.cluster.edu % 0.07/0.26 % Model : x86_64 x86_64 % 0.07/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.26 % Memory : 8042.1875MB % 0.07/0.26 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.26 % CPULimit : 300 % 0.07/0.26 % WCLimit : 300 % 0.07/0.26 % DateTime : Fri Jun 21 11:42:08 EDT 2024 % 0.07/0.26 % CPUTime : % 0.12/0.43 start to proof:theBenchmark % 68.04/68.20 %------------------------------------------- % 68.04/68.20 % File :CSE---1.7 % 68.04/68.20 % Problem :theBenchmark % 68.04/68.20 % Transform :cnf % 68.04/68.20 % Format :tptp:raw % 68.04/68.20 % Command :java -jar mcs_scs.jar %d %s % 68.04/68.20 % 68.04/68.20 % Result :Theorem 67.650000s % 68.04/68.20 % Output :CNFRefutation 67.650000s % 68.04/68.20 %------------------------------------------- % 68.04/68.21 %------------------------------------------------------------------------------ % 68.04/68.21 % File : SEU362+1 : TPTP v8.2.0. Released v3.3.0. % 68.04/68.21 % Domain : Set theory % 68.04/68.21 % Problem : MPTP bushy problem t60_yellow_0 % 68.04/68.21 % Version : [Urb07] axioms : Especial. % 68.04/68.21 % English : % 68.04/68.21 % 68.04/68.21 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 68.04/68.21 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 68.04/68.21 % Source : [Urb07] % 68.04/68.21 % Names : bushy-t60_yellow_0 [Urb07] % 68.04/68.21 % 68.04/68.21 % Status : Theorem % 68.04/68.21 % Rating : 0.31 v8.2.0, 0.28 v7.5.0, 0.31 v7.4.0, 0.20 v7.3.0, 0.24 v7.2.0, 0.21 v7.1.0, 0.30 v7.0.0, 0.23 v6.4.0, 0.31 v6.3.0, 0.38 v6.2.0, 0.40 v6.1.0, 0.47 v6.0.0, 0.26 v5.5.0, 0.41 v5.4.0, 0.43 v5.3.0, 0.52 v5.2.0, 0.40 v5.1.0, 0.38 v5.0.0, 0.42 v4.1.0, 0.48 v4.0.1, 0.52 v4.0.0, 0.54 v3.7.0, 0.55 v3.5.0, 0.58 v3.4.0, 0.53 v3.3.0 % 68.04/68.21 % Syntax : Number of formulae : 42 ( 17 unt; 0 def) % 68.04/68.21 % Number of atoms : 92 ( 4 equ) % 68.04/68.21 % Maximal formula atoms : 10 ( 2 avg) % 68.04/68.21 % Number of connectives : 61 ( 11 ~; 1 |; 15 &) % 68.04/68.21 % ( 4 <=>; 30 =>; 0 <=; 0 <~>) % 68.04/68.21 % Maximal formula depth : 16 ( 4 avg) % 68.04/68.21 % Maximal term depth : 3 ( 1 avg) % 68.04/68.21 % Number of predicates : 14 ( 12 usr; 1 prp; 0-3 aty) % 68.04/68.21 % Number of functors : 6 ( 6 usr; 1 con; 0-2 aty) % 68.04/68.21 % Number of variables : 69 ( 58 !; 11 ?) % 68.04/68.21 % SPC : FOF_THM_RFO_SEQ % 68.04/68.21 % 68.04/68.21 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 68.04/68.21 % library, www.mizar.org % 68.04/68.21 %------------------------------------------------------------------------------ % 68.04/68.22 fof(antisymmetry_r2_hidden,axiom, % 68.04/68.22 ! [A,B] : % 68.04/68.22 ( in(A,B) % 68.04/68.22 => ~ in(B,A) ) ). % 68.04/68.22 % 68.04/68.22 fof(cc1_finset_1,axiom, % 68.04/68.22 ! [A] : % 68.04/68.22 ( empty(A) % 68.04/68.22 => finite(A) ) ). % 68.04/68.22 % 68.04/68.22 fof(cc1_relset_1,axiom, % 68.04/68.22 ! [A,B,C] : % 68.04/68.22 ( element(C,powerset(cartesian_product2(A,B))) % 68.04/68.22 => relation(C) ) ). % 68.04/68.22 % 68.04/68.22 fof(cc2_finset_1,axiom, % 68.04/68.22 ! [A] : % 68.04/68.22 ( finite(A) % 68.04/68.22 => ! [B] : % 68.04/68.22 ( element(B,powerset(A)) % 68.04/68.22 => finite(B) ) ) ). % 68.04/68.22 % 68.04/68.22 fof(d13_yellow_0,axiom, % 68.04/68.22 ! [A] : % 68.04/68.22 ( rel_str(A) % 68.04/68.22 => ! [B] : % 68.04/68.22 ( rel_str(B) % 68.04/68.22 => ( subrelstr(B,A) % 68.04/68.22 <=> ( subset(the_carrier(B),the_carrier(A)) % 68.04/68.22 & subset(the_InternalRel(B),the_InternalRel(A)) ) ) ) ) ). % 68.04/68.22 % 68.04/68.22 fof(d9_orders_2,axiom, % 68.04/68.22 ! [A] : % 68.04/68.22 ( rel_str(A) % 68.04/68.22 => ! [B] : % 68.04/68.22 ( element(B,the_carrier(A)) % 68.04/68.22 => ! [C] : % 68.04/68.22 ( element(C,the_carrier(A)) % 68.04/68.22 => ( related(A,B,C) % 68.04/68.22 <=> in(ordered_pair(B,C),the_InternalRel(A)) ) ) ) ) ). % 68.04/68.22 % 68.04/68.22 fof(dt_k1_xboole_0,axiom, % 68.04/68.22 $true ). % 68.04/68.22 % 68.04/68.22 fof(dt_k1_zfmisc_1,axiom, % 68.04/68.22 $true ). % 68.04/68.22 % 68.04/68.22 fof(dt_k2_zfmisc_1,axiom, % 68.04/68.22 $true ). % 68.04/68.22 % 68.04/68.22 fof(dt_k4_tarski,axiom, % 68.04/68.22 $true ). % 68.04/68.22 % 68.04/68.22 fof(dt_l1_orders_2,axiom, % 68.04/68.22 ! [A] : % 68.04/68.22 ( rel_str(A) % 68.04/68.22 => one_sorted_str(A) ) ). % 68.04/68.22 % 68.04/68.22 fof(dt_l1_struct_0,axiom, % 68.04/68.22 $true ). % 68.04/68.22 % 68.04/68.22 fof(dt_m1_relset_1,axiom, % 68.04/68.22 $true ). % 68.04/68.22 % 68.04/68.22 fof(dt_m1_subset_1,axiom, % 68.04/68.22 $true ). % 68.04/68.22 % 68.04/68.22 fof(dt_m1_yellow_0,axiom, % 68.04/68.22 ! [A] : % 68.04/68.22 ( rel_str(A) % 68.04/68.22 => ! [B] : % 68.04/68.22 ( subrelstr(B,A) % 68.04/68.22 => rel_str(B) ) ) ). % 68.04/68.22 % 68.04/68.22 fof(dt_m2_relset_1,axiom, % 68.04/68.22 ! [A,B,C] : % 68.04/68.22 ( relation_of2_as_subset(C,A,B) % 68.04/68.22 => element(C,powerset(cartesian_product2(A,B))) ) ). % 68.04/68.22 % 68.04/68.22 fof(dt_u1_orders_2,axiom, % 68.04/68.22 ! [A] : % 68.04/68.22 ( rel_str(A) % 68.04/68.22 => relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)) ) ). % 68.04/68.22 % 68.04/68.22 fof(dt_u1_struct_0,axiom, % 68.04/68.22 $true ). % 68.04/68.22 % 68.04/68.22 fof(existence_l1_orders_2,axiom, % 68.04/68.22 ? [A] : rel_str(A) ). % 68.04/68.22 % 68.04/68.22 fof(existence_l1_struct_0,axiom, % 68.04/68.22 ? [A] : one_sorted_str(A) ). % 68.04/68.22 % 68.04/68.22 fof(existence_m1_relset_1,axiom, % 68.04/68.22 ! [A,B] : % 68.04/68.22 ? [C] : relation_of2(C,A,B) ). % 68.04/68.22 % 68.04/68.22 fof(existence_m1_subset_1,axiom, % 68.04/68.22 ! [A] : % 68.04/68.22 ? [B] : element(B,A) ). % 68.04/68.22 % 68.04/68.22 fof(existence_m1_yellow_0,axiom, % 68.04/68.22 ! [A] : % 68.04/68.22 ( rel_str(A) % 68.04/68.22 => ? [B] : subrelstr(B,A) ) ). % 68.04/68.22 % 68.04/68.22 fof(existence_m2_relset_1,axiom, % 68.04/68.22 ! [A,B] : % 68.04/68.22 ? [C] : relation_of2_as_subset(C,A,B) ). % 68.04/68.22 % 68.04/68.22 fof(fc14_finset_1,axiom, % 68.04/68.22 ! [A,B] : % 68.04/68.22 ( ( finite(A) % 68.04/68.22 & finite(B) ) % 68.04/68.22 => finite(cartesian_product2(A,B)) ) ). % 68.04/68.22 % 68.04/68.22 fof(fc1_xboole_0,axiom, % 68.04/68.22 empty(empty_set) ). % 68.04/68.22 % 68.04/68.22 fof(rc1_finset_1,axiom, % 68.04/68.22 ? [A] : % 68.04/68.22 ( ~ empty(A) % 68.04/68.22 & finite(A) ) ). % 68.04/68.22 % 68.04/68.22 fof(rc1_xboole_0,axiom, % 68.04/68.22 ? [A] : empty(A) ). % 68.04/68.22 % 68.04/68.22 fof(rc2_xboole_0,axiom, % 68.04/68.22 ? [A] : ~ empty(A) ). % 68.04/68.22 % 68.04/68.22 fof(rc3_finset_1,axiom, % 68.04/68.22 ! [A] : % 68.04/68.22 ( ~ empty(A) % 68.04/68.22 => ? [B] : % 68.04/68.22 ( element(B,powerset(A)) % 68.04/68.22 & ~ empty(B) % 68.04/68.22 & finite(B) ) ) ). % 68.04/68.22 % 68.04/68.22 fof(rc4_finset_1,axiom, % 68.04/68.22 ! [A] : % 68.04/68.22 ( ~ empty(A) % 68.04/68.22 => ? [B] : % 68.04/68.22 ( element(B,powerset(A)) % 68.04/68.22 & ~ empty(B) % 68.04/68.22 & finite(B) ) ) ). % 68.04/68.22 % 68.04/68.22 fof(redefinition_m2_relset_1,axiom, % 68.04/68.22 ! [A,B,C] : % 68.04/68.22 ( relation_of2_as_subset(C,A,B) % 68.04/68.22 <=> relation_of2(C,A,B) ) ). % 68.04/68.22 % 68.04/68.22 fof(reflexivity_r1_tarski,axiom, % 68.04/68.22 ! [A,B] : subset(A,A) ). % 68.04/68.22 % 68.04/68.22 fof(t1_subset,axiom, % 68.04/68.22 ! [A,B] : % 68.04/68.22 ( in(A,B) % 68.04/68.22 => element(A,B) ) ). % 68.04/68.22 % 68.04/68.22 fof(t2_subset,axiom, % 68.04/68.22 ! [A,B] : % 68.04/68.22 ( element(A,B) % 68.04/68.22 => ( empty(B) % 68.04/68.22 | in(A,B) ) ) ). % 68.04/68.22 % 68.04/68.22 fof(t3_subset,axiom, % 68.04/68.22 ! [A,B] : % 68.04/68.22 ( element(A,powerset(B)) % 68.04/68.22 <=> subset(A,B) ) ). % 68.04/68.22 % 68.04/68.22 fof(t4_subset,axiom, % 68.04/68.22 ! [A,B,C] : % 68.04/68.22 ( ( in(A,B) % 68.04/68.22 & element(B,powerset(C)) ) % 68.04/68.22 => element(A,C) ) ). % 68.04/68.22 % 68.04/68.22 fof(t5_subset,axiom, % 68.04/68.22 ! [A,B,C] : % 68.04/68.22 ~ ( in(A,B) % 68.04/68.22 & element(B,powerset(C)) % 68.04/68.22 & empty(C) ) ). % 68.04/68.22 % 68.04/68.22 fof(t60_yellow_0,conjecture, % 68.04/68.22 ! [A] : % 68.04/68.22 ( rel_str(A) % 68.04/68.22 => ! [B] : % 68.04/68.22 ( subrelstr(B,A) % 68.04/68.22 => ! [C] : % 68.04/68.22 ( element(C,the_carrier(A)) % 68.04/68.22 => ! [D] : % 68.04/68.22 ( element(D,the_carrier(A)) % 68.04/68.22 => ! [E] : % 68.04/68.22 ( element(E,the_carrier(B)) % 68.04/68.22 => ! [F] : % 68.04/68.22 ( element(F,the_carrier(B)) % 68.04/68.22 => ( ( E = C % 68.04/68.22 & F = D % 68.04/68.22 & related(B,E,F) ) % 68.04/68.22 => related(A,C,D) ) ) ) ) ) ) ) ). % 68.04/68.22 % 68.04/68.22 fof(t6_boole,axiom, % 68.04/68.22 ! [A] : % 68.04/68.22 ( empty(A) % 68.04/68.22 => A = empty_set ) ). % 68.04/68.22 % 68.04/68.22 fof(t7_boole,axiom, % 68.04/68.22 ! [A,B] : % 68.04/68.22 ~ ( in(A,B) % 68.04/68.22 & empty(B) ) ). % 68.04/68.22 % 68.04/68.22 fof(t8_boole,axiom, % 68.04/68.22 ! [A,B] : % 68.04/68.22 ~ ( empty(A) % 68.04/68.22 & A != B % 68.04/68.22 & empty(B) ) ). % 68.04/68.22 % 68.04/68.22 %------------------------------------------------------------------------------ % 68.04/68.22 %------------------------------------------- % 68.04/68.22 % Proof found % 68.04/68.22 % SZS status Theorem for theBenchmark % 68.04/68.22 % SZS output start Proof % 68.11/68.22 %ClaNum:93(EqnAxiom:40) % 68.11/68.22 %VarNum:154(SingletonVarNum:67) % 68.11/68.22 %MaxLitNum:5 % 68.11/68.22 %MaxfuncDepth:2 % 68.11/68.22 %SharedTerms:31 % 68.11/68.22 %goalClause: 41 42 47 49 51 52 53 54 56 61 % 68.11/68.22 %singleGoalClaCount:10 % 68.11/68.22 [41]E(a1,a2) % 68.11/68.22 [42]E(a9,a10) % 68.11/68.22 [43]P1(a3) % 68.11/68.22 [44]P1(a11) % 68.11/68.23 [45]P3(a12) % 68.11/68.23 [46]P4(a13) % 68.11/68.23 [47]P4(a5) % 68.11/68.23 [48]P5(a14) % 68.11/68.23 [49]P7(a8,a5) % 68.11/68.23 [56]P8(a8,a1,a10) % 68.11/68.23 [59]~P1(a12) % 68.11/68.23 [60]~P1(a20) % 68.11/68.23 [61]~P8(a5,a2,a9) % 68.11/68.23 [51]P2(a2,f19(a5)) % 68.11/68.23 [52]P2(a9,f19(a5)) % 68.11/68.23 [53]P2(a1,f19(a8)) % 68.11/68.23 [54]P2(a10,f19(a8)) % 68.11/68.23 [50]P12(x501,x501) % 68.11/68.23 [55]P2(f15(x551),x551) % 68.11/68.23 [57]P9(f17(x571,x572),x571,x572) % 68.11/68.23 [58]P10(f16(x581,x582),x581,x582) % 68.11/68.23 [62]~P1(x621)+E(x621,a3) % 68.11/68.23 [63]~P1(x631)+P3(x631) % 68.11/68.23 [64]~P4(x641)+P5(x641) % 68.11/68.23 [65]P1(x651)+P3(f6(x651)) % 68.11/68.23 [66]P1(x661)+P3(f7(x661)) % 68.11/68.23 [68]P1(x681)+~P1(f6(x681)) % 68.11/68.23 [69]P1(x691)+~P1(f7(x691)) % 68.11/68.23 [70]~P4(x701)+P7(f18(x701),x701) % 68.11/68.23 [72]P1(x721)+P2(f6(x721),f21(x721)) % 68.11/68.23 [73]P1(x731)+P2(f7(x731),f21(x731)) % 68.11/68.23 [86]~P4(x861)+P9(f23(x861),f19(x861),f19(x861)) % 68.11/68.23 [71]~P1(x711)+~P6(x712,x711) % 68.11/68.23 [75]~P6(x751,x752)+P2(x751,x752) % 68.11/68.23 [80]~P6(x802,x801)+~P6(x801,x802) % 68.11/68.23 [77]~P12(x771,x772)+P2(x771,f21(x772)) % 68.11/68.23 [81]P12(x811,x812)+~P2(x811,f21(x812)) % 68.11/68.23 [89]~P10(x891,x892,x893)+P9(x891,x892,x893) % 68.11/68.23 [90]~P9(x901,x902,x903)+P10(x901,x902,x903) % 68.11/68.23 [88]P11(x881)+~P2(x881,f21(f4(x882,x883))) % 68.11/68.23 [91]~P9(x911,x912,x913)+P2(x911,f21(f4(x912,x913))) % 68.11/68.23 [67]~P1(x672)+~P1(x671)+E(x671,x672) % 68.11/68.23 [74]~P7(x741,x742)+P4(x741)+~P4(x742) % 68.11/68.23 [76]~P2(x762,x761)+P1(x761)+P6(x762,x761) % 68.11/68.23 [78]P3(x781)+~P3(x782)+~P2(x781,f21(x782)) % 68.11/68.23 [79]~P3(x792)+~P3(x791)+P3(f4(x791,x792)) % 68.11/68.23 [82]~P1(x821)+~P6(x822,x823)+~P2(x823,f21(x821)) % 68.11/68.23 [85]P2(x851,x852)+~P6(x851,x853)+~P2(x853,f21(x852)) % 68.11/68.23 [83]~P4(x832)+~P4(x831)+~P7(x831,x832)+P12(f19(x831),f19(x832)) % 68.11/68.23 [84]~P4(x842)+~P4(x841)+~P7(x841,x842)+P12(f23(x841),f23(x842)) % 68.11/68.23 [87]~P4(x872)+~P4(x871)+P7(x871,x872)+~P12(f19(x871),f19(x872))+~P12(f23(x871),f23(x872)) % 68.11/68.23 [92]~P4(x921)+P8(x921,x922,x923)+~P2(x923,f19(x921))+~P2(x922,f19(x921))+~P6(f22(x922,x923),f23(x921)) % 68.11/68.23 [93]~P4(x933)+~P8(x933,x931,x932)+~P2(x932,f19(x933))+~P2(x931,f19(x933))+P6(f22(x931,x932),f23(x933)) % 68.11/68.23 %EqnAxiom % 68.11/68.23 [1]E(x11,x11) % 68.11/68.23 [2]E(x22,x21)+~E(x21,x22) % 68.11/68.23 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 68.11/68.23 [4]~E(x41,x42)+E(f19(x41),f19(x42)) % 68.11/68.23 [5]~E(x51,x52)+E(f23(x51),f23(x52)) % 68.11/68.23 [6]~E(x61,x62)+E(f22(x61,x63),f22(x62,x63)) % 68.11/68.23 [7]~E(x71,x72)+E(f22(x73,x71),f22(x73,x72)) % 68.11/68.23 [8]~E(x81,x82)+E(f4(x81,x83),f4(x82,x83)) % 68.11/68.23 [9]~E(x91,x92)+E(f4(x93,x91),f4(x93,x92)) % 68.11/68.23 [10]~E(x101,x102)+E(f15(x101),f15(x102)) % 68.11/68.23 [11]~E(x111,x112)+E(f17(x111,x113),f17(x112,x113)) % 68.11/68.23 [12]~E(x121,x122)+E(f17(x123,x121),f17(x123,x122)) % 68.11/68.23 [13]~E(x131,x132)+E(f16(x131,x133),f16(x132,x133)) % 68.11/68.23 [14]~E(x141,x142)+E(f16(x143,x141),f16(x143,x142)) % 68.11/68.23 [15]~E(x151,x152)+E(f6(x151),f6(x152)) % 68.11/68.23 [16]~E(x161,x162)+E(f7(x161),f7(x162)) % 68.11/68.23 [17]~E(x171,x172)+E(f21(x171),f21(x172)) % 68.11/68.23 [18]~E(x181,x182)+E(f18(x181),f18(x182)) % 68.11/68.23 [19]~P1(x191)+P1(x192)+~E(x191,x192) % 68.11/68.23 [20]P2(x202,x203)+~E(x201,x202)+~P2(x201,x203) % 68.11/68.23 [21]P2(x213,x212)+~E(x211,x212)+~P2(x213,x211) % 68.11/68.23 [22]~P3(x221)+P3(x222)+~E(x221,x222) % 68.11/68.23 [23]~P4(x231)+P4(x232)+~E(x231,x232) % 68.11/68.23 [24]P12(x242,x243)+~E(x241,x242)+~P12(x241,x243) % 68.11/68.23 [25]P12(x253,x252)+~E(x251,x252)+~P12(x253,x251) % 68.11/68.23 [26]~P5(x261)+P5(x262)+~E(x261,x262) % 68.11/68.23 [27]P7(x272,x273)+~E(x271,x272)+~P7(x271,x273) % 68.11/68.23 [28]P7(x283,x282)+~E(x281,x282)+~P7(x283,x281) % 68.11/68.23 [29]P9(x292,x293,x294)+~E(x291,x292)+~P9(x291,x293,x294) % 68.11/68.23 [30]P9(x303,x302,x304)+~E(x301,x302)+~P9(x303,x301,x304) % 68.11/68.23 [31]P9(x313,x314,x312)+~E(x311,x312)+~P9(x313,x314,x311) % 68.11/68.23 [32]P6(x322,x323)+~E(x321,x322)+~P6(x321,x323) % 68.11/68.23 [33]P6(x333,x332)+~E(x331,x332)+~P6(x333,x331) % 68.11/68.23 [34]P10(x342,x343,x344)+~E(x341,x342)+~P10(x341,x343,x344) % 68.11/68.23 [35]P10(x353,x352,x354)+~E(x351,x352)+~P10(x353,x351,x354) % 68.11/68.23 [36]P10(x363,x364,x362)+~E(x361,x362)+~P10(x363,x364,x361) % 68.11/68.23 [37]P8(x372,x373,x374)+~E(x371,x372)+~P8(x371,x373,x374) % 68.11/68.23 [38]P8(x383,x382,x384)+~E(x381,x382)+~P8(x383,x381,x384) % 68.11/68.23 [39]P8(x393,x394,x392)+~E(x391,x392)+~P8(x393,x394,x391) % 68.11/68.23 [40]~P11(x401)+P11(x402)+~E(x401,x402) % 68.11/68.23 % 68.11/68.23 %------------------------------------------- % 68.11/68.24 cnf(94,plain, % 68.11/68.24 (E(a2,a1)), % 68.11/68.24 inference(scs_inference,[],[41,2])). % 68.11/68.24 cnf(95,plain, % 68.11/68.24 (~P6(x951,a3)), % 68.11/68.24 inference(scs_inference,[],[41,43,2,71])). % 68.11/68.24 cnf(97,plain, % 68.11/68.24 (P12(f15(f21(x971)),x971)), % 68.11/68.24 inference(scs_inference,[],[41,55,43,2,71,81])). % 68.11/68.24 cnf(98,plain, % 68.11/68.24 (P2(f15(x981),x981)), % 68.11/68.24 inference(rename_variables,[],[55])). % 68.11/68.24 cnf(100,plain, % 68.11/68.24 (P2(a1,f19(a5))), % 68.11/68.24 inference(scs_inference,[],[41,51,55,43,2,71,81,20])). % 68.11/68.24 cnf(102,plain, % 68.11/68.24 (P2(f15(x1021),x1021)), % 68.11/68.24 inference(rename_variables,[],[55])). % 68.11/68.24 cnf(103,plain, % 68.11/68.24 (P12(a2,a1)), % 68.11/68.24 inference(scs_inference,[],[41,51,50,55,98,43,2,71,81,20,21,24])). % 68.11/68.24 cnf(104,plain, % 68.11/68.24 (P12(x1041,x1041)), % 68.11/68.24 inference(rename_variables,[],[50])). % 68.11/68.24 cnf(105,plain, % 68.11/68.24 (P12(a1,a2)), % 68.11/68.24 inference(scs_inference,[],[41,51,50,104,55,98,43,2,71,81,20,21,24,25])). % 68.11/68.24 cnf(107,plain, % 68.11/68.24 (P9(f17(a1,x1071),a2,x1071)), % 68.11/68.25 inference(scs_inference,[],[41,51,50,104,57,55,98,43,2,71,81,20,21,24,25,30])). % 68.11/68.25 cnf(108,plain, % 68.11/68.25 (P9(f17(x1081,x1082),x1081,x1082)), % 68.11/68.25 inference(rename_variables,[],[57])). % 68.11/68.25 cnf(109,plain, % 68.11/68.25 (P9(f17(x1091,a1),x1091,a2)), % 68.11/68.25 inference(scs_inference,[],[41,51,50,104,57,108,55,98,43,2,71,81,20,21,24,25,30,31])). % 68.11/68.25 cnf(111,plain, % 68.11/68.25 (P10(f16(a1,x1111),a2,x1111)), % 68.11/68.25 inference(scs_inference,[],[41,51,50,104,57,108,58,55,98,43,2,71,81,20,21,24,25,30,31,35])). % 68.11/68.25 cnf(112,plain, % 68.11/68.25 (P10(f16(x1121,x1122),x1121,x1122)), % 68.11/68.25 inference(rename_variables,[],[58])). % 68.11/68.25 cnf(113,plain, % 68.11/68.25 (P6(f15(a12),a12)), % 68.11/68.25 inference(scs_inference,[],[41,51,50,104,57,108,58,55,98,102,43,59,2,71,81,20,21,24,25,30,31,35,76])). % 68.11/68.25 cnf(114,plain, % 68.11/68.25 (P2(f15(x1141),x1141)), % 68.11/68.25 inference(rename_variables,[],[55])). % 68.11/68.25 cnf(117,plain, % 68.11/68.25 (P2(f15(x1171),x1171)), % 68.11/68.25 inference(rename_variables,[],[55])). % 68.11/68.25 cnf(119,plain, % 68.11/68.25 (~P6(x1191,f15(f21(a3)))), % 68.11/68.25 inference(scs_inference,[],[41,51,50,104,57,108,58,55,98,102,114,117,43,45,59,2,71,81,20,21,24,25,30,31,35,76,78,82])). % 68.11/68.25 cnf(122,plain, % 68.11/68.25 (P10(f16(x1221,a1),x1221,a2)), % 68.11/68.25 inference(scs_inference,[],[41,51,50,104,57,108,58,112,55,98,102,114,117,43,45,59,2,71,81,20,21,24,25,30,31,35,76,78,82,36])). % 68.11/68.25 cnf(132,plain, % 68.11/68.25 (~P6(x1321,a11)), % 68.11/68.25 inference(scs_inference,[],[44,71])). % 68.11/68.25 cnf(134,plain, % 68.14/68.25 (E(a10,a9)), % 68.14/68.25 inference(scs_inference,[],[42,44,71,2])). % 68.14/68.25 cnf(135,plain, % 68.14/68.25 (P8(a8,a1,a9)), % 68.14/68.25 inference(scs_inference,[],[42,56,44,71,2,39])). % 68.14/68.25 cnf(136,plain, % 68.14/68.25 (~P6(x1361,f15(f21(a11)))), % 68.14/68.25 inference(scs_inference,[],[42,56,44,55,71,2,39,82])). % 68.14/68.25 cnf(137,plain, % 68.14/68.25 (P2(f15(x1371),x1371)), % 68.14/68.25 inference(rename_variables,[],[55])). % 68.14/68.25 cnf(143,plain, % 68.14/68.25 (P6(f15(a20),a20)), % 68.14/68.25 inference(scs_inference,[],[41,42,56,119,122,113,44,60,55,137,71,2,39,82,33,35,76])). % 68.14/68.25 cnf(146,plain, % 68.14/68.25 (P2(a10,f19(a5))), % 68.14/68.25 inference(scs_inference,[],[41,52,42,56,119,122,113,44,60,55,137,71,2,39,82,33,35,76,20])). % 68.14/68.25 cnf(149,plain, % 68.14/68.25 (P12(f15(f21(a1)),a2)), % 68.14/68.25 inference(scs_inference,[],[41,52,42,56,109,97,119,122,113,44,60,55,137,71,2,39,82,33,35,76,20,30,25])). % 68.14/68.25 cnf(151,plain, % 68.14/68.25 (P8(a8,a2,a9)), % 68.14/68.25 inference(scs_inference,[],[41,52,42,56,109,97,119,122,113,44,60,55,137,71,2,39,82,33,35,76,20,30,25,38])). % 68.14/68.25 cnf(154,plain, % 68.14/68.25 (P9(x1541,a2,x1542)+~E(f17(a1,x1542),x1541)), % 68.14/68.25 inference(scs_inference,[],[41,52,42,56,107,109,97,119,122,113,44,60,55,137,71,2,39,82,33,35,76,20,30,25,38,80,29])). % 68.14/68.25 cnf(165,plain, % 68.14/68.25 (P2(a2,f19(a8))), % 68.14/68.25 inference(scs_inference,[],[41,53,136,143,33,20])). % 68.14/68.25 cnf(173,plain, % 68.14/68.25 (P2(a9,f19(a8))), % 68.14/68.25 inference(scs_inference,[],[134,54,20])). % 68.14/68.25 cnf(174,plain, % 68.14/68.25 (~E(a20,a3)), % 68.14/68.25 inference(scs_inference,[],[134,54,143,95,20,33])). % 68.14/68.25 cnf(197,plain, % 68.14/68.25 (P10(x1971,a2,x1972)+~E(f16(a1,x1972),x1971)), % 68.14/68.25 inference(scs_inference,[],[49,111,143,113,119,33,27,32,34])). % 68.14/68.25 cnf(208,plain, % 68.14/68.25 (P9(x2081,x2082,a2)+~E(f17(x2082,a1),x2081)), % 68.14/68.25 inference(scs_inference,[],[109,113,136,33,29])). % 68.14/68.25 cnf(216,plain, % 68.14/68.25 (~E(a12,a3)), % 68.14/68.25 inference(scs_inference,[],[113,95,33])). % 68.14/68.25 cnf(228,plain, % 68.14/68.25 (P10(x2281,x2282,a2)+~E(f16(x2282,a1),x2281)), % 68.14/68.25 inference(scs_inference,[],[41,58,143,132,33,34,36])). % 68.14/68.25 cnf(332,plain, % 68.14/68.25 (P12(x3321,x3322)+~E(f15(f21(x3322)),x3321)), % 68.14/68.25 inference(scs_inference,[],[94,135,97,40,37,24])). % 68.14/68.25 cnf(422,plain, % 68.14/68.25 (~P8(a5,a9,a9)+~E(f23(a5),a3)), % 68.14/68.25 inference(scs_inference,[],[52,47,95,93,80,33])). % 68.14/68.25 cnf(432,plain, % 68.14/68.25 (~P8(a5,a2,a2)+P6(f22(a2,a2),f23(a5))), % 68.14/68.25 inference(scs_inference,[],[51,47,93])). % 68.14/68.25 cnf(434,plain, % 68.14/68.25 (~P6(f23(a5),f22(a2,a2))+~P8(a5,a2,a2)), % 68.14/68.25 inference(scs_inference,[],[51,47,93,80])). % 68.14/68.25 cnf(436,plain, % 68.14/68.25 (~P8(a5,a2,a2)+~E(f23(a5),a11)), % 68.14/68.25 inference(scs_inference,[],[51,47,132,93,80,33])). % 68.14/68.25 cnf(537,plain, % 68.14/68.25 (P9(f17(a1,a9),a2,a10)), % 68.14/68.25 inference(scs_inference,[],[42,107,31])). % 68.14/68.25 cnf(539,plain, % 68.14/68.25 (P9(f17(a9,a1),a10,a2)), % 68.14/68.25 inference(scs_inference,[],[42,107,109,31,30])). % 68.14/68.25 cnf(541,plain, % 68.14/68.25 (P10(f16(a9,x5411),a10,x5411)), % 68.14/68.25 inference(scs_inference,[],[42,107,109,58,31,30,35])). % 68.14/68.25 cnf(547,plain, % 68.14/68.25 (P12(a10,a9)), % 68.14/68.25 inference(scs_inference,[],[42,107,109,111,55,58,50,31,30,35,36,21,24])). % 68.14/68.25 cnf(548,plain, % 68.14/68.25 (P12(x5481,x5481)), % 68.14/68.25 inference(rename_variables,[],[50])). % 68.14/68.25 cnf(549,plain, % 68.14/68.25 (P12(a9,a10)), % 68.14/68.25 inference(scs_inference,[],[42,107,109,111,55,58,50,548,31,30,35,36,21,24,25])). % 68.14/68.25 cnf(552,plain, % 68.14/68.25 (P10(x5521,a10,x5522)+~E(f16(a9,x5522),x5521)), % 68.14/68.25 inference(scs_inference,[],[42,107,109,111,55,58,50,548,31,30,35,36,21,24,25,20,34])). % 68.14/68.25 cnf(563,plain, % 68.14/68.25 (P10(f16(a9,a9),a10,a10)), % 68.14/68.25 inference(scs_inference,[],[42,94,537,541,539,122,30,31,35,36])). % 68.14/68.25 cnf(565,plain, % 68.14/68.25 (P12(f15(f21(a9)),a10)), % 68.14/68.25 inference(scs_inference,[],[42,94,537,541,539,122,97,30,31,35,36,25])). % 68.14/68.25 cnf(575,plain, % 68.14/68.25 (P9(f17(x5751,a9),x5751,a10)), % 68.14/68.25 inference(scs_inference,[],[42,57,31])). % 68.14/68.25 cnf(576,plain, % 68.14/68.25 (P9(f17(x5761,x5762),x5761,x5762)), % 68.14/68.25 inference(rename_variables,[],[57])). % 68.14/68.25 cnf(577,plain, % 68.14/68.25 (P9(f17(a9,x5771),a10,x5771)), % 68.14/68.25 inference(scs_inference,[],[42,57,576,31,30])). % 68.14/68.25 cnf(580,plain, % 68.14/68.25 (P10(f16(x5801,a9),x5801,a10)), % 68.14/68.25 inference(scs_inference,[],[42,134,57,576,58,563,31,30,35,36])). % 68.14/68.25 cnf(588,plain, % 68.14/68.25 (P9(f17(a9,a9),a10,a10)), % 68.14/68.25 inference(scs_inference,[],[42,575,30])). % 68.14/68.25 cnf(589,plain, % 68.14/68.25 (P9(f17(x5891,a9),x5891,a10)), % 68.14/68.25 inference(rename_variables,[],[575])). % 68.14/68.25 cnf(590,plain, % 68.14/68.25 (P9(x5901,x5902,a10)+~E(f17(x5902,a9),x5901)), % 68.14/68.25 inference(scs_inference,[],[42,575,589,30,29])). % 68.14/68.25 cnf(591,plain, % 68.14/68.25 (P10(x5911,x5912,a10)+~E(f16(x5912,a9),x5911)), % 68.14/68.25 inference(scs_inference,[],[42,575,589,580,30,29,34])). % 68.14/68.25 cnf(596,plain, % 68.14/68.25 (P9(x5961,a10,x5962)+~E(f17(a9,x5962),x5961)), % 68.14/68.25 inference(scs_inference,[],[577,29])). % 68.14/68.25 cnf(972,plain, % 68.14/68.25 (P3(f7(a20))), % 68.14/68.25 inference(scs_inference,[],[174,62,66])). % 68.14/68.25 cnf(2058,plain, % 68.14/68.25 (~P6(a20,f21(a11))), % 68.14/68.25 inference(scs_inference,[],[44,143,75,82])). % 68.14/68.25 cnf(2917,plain, % 68.14/68.25 (E(f19(a2),f19(a1))), % 68.14/68.25 inference(scs_inference,[],[41,4,2])). % 68.14/68.25 cnf(2918,plain, % 68.14/68.25 (E(f19(a1),f19(a2))), % 68.14/68.25 inference(scs_inference,[],[2917,2])). % 68.14/68.25 cnf(3113,plain, % 68.14/68.25 (P12(f19(a1),f19(a2))), % 68.14/68.25 inference(scs_inference,[],[2918,109,111,55,50,30,21,36,25])). % 68.14/68.25 cnf(3114,plain, % 68.14/68.25 (P12(x31141,x31141)), % 68.14/68.25 inference(rename_variables,[],[50])). % 68.14/68.25 cnf(3115,plain, % 68.14/68.25 (P12(f19(a2),f19(a1))), % 68.14/68.25 inference(scs_inference,[],[2918,109,111,55,50,3114,30,21,36,25,24])). % 68.14/68.25 cnf(3117,plain, % 68.14/68.25 (P9(f17(a9,f19(a1)),a10,f19(a2))), % 68.14/68.25 inference(scs_inference,[],[2918,109,111,577,55,50,3114,30,21,36,25,24,31])). % 68.14/68.25 cnf(3119,plain, % 68.14/68.25 (P10(f16(f19(a1),x31191),f19(a2),x31191)), % 68.14/68.25 inference(scs_inference,[],[2918,109,111,577,58,55,50,3114,30,21,36,25,24,31,35])). % 68.14/68.25 cnf(3138,plain, % 68.14/68.25 (P10(x31381,f19(a2),x31382)+~E(f16(f19(a1),x31382),x31381)), % 68.14/68.25 inference(scs_inference,[],[2918,541,575,107,3119,3117,122,30,36,31,35,29,34])). % 68.14/68.25 cnf(3156,plain, % 68.14/68.25 (P10(f16(x31561,f19(a1)),x31561,f19(a2))), % 68.14/68.25 inference(scs_inference,[],[2918,134,3117,58,30,36])). % 68.14/68.25 cnf(3165,plain, % 68.14/68.25 (P9(f17(f19(a1),x31651),f19(a2),x31651)), % 68.14/68.25 inference(scs_inference,[],[2918,57,30])). % 68.14/68.25 cnf(3166,plain, % 68.14/68.25 (P9(f17(x31661,x31662),x31661,x31662)), % 68.14/68.25 inference(rename_variables,[],[57])). % 68.14/68.25 cnf(3167,plain, % 68.14/68.25 (P9(f17(x31671,f19(a1)),x31671,f19(a2))), % 68.14/68.25 inference(scs_inference,[],[2918,57,3166,30,31])). % 68.14/68.25 cnf(3177,plain, % 68.14/68.25 (P9(x31771,f19(a2),x31772)+~E(f17(f19(a1),x31772),x31771)), % 68.14/68.25 inference(scs_inference,[],[2918,3165,3167,30,29])). % 68.14/68.25 cnf(3189,plain, % 68.14/68.25 (P9(x31891,x31892,f19(a2))+~E(f17(x31892,f19(a1)),x31891)), % 68.14/68.25 inference(scs_inference,[],[3167,29])). % 68.14/68.25 cnf(3195,plain, % 68.14/68.25 (P10(x31951,x31952,f19(a2))+~E(f16(x31952,f19(a1)),x31951)), % 68.14/68.25 inference(scs_inference,[],[3156,34])). % 68.14/68.25 cnf(3308,plain, % 68.14/68.25 (P9(f17(a2,a9),a1,a10)), % 68.14/68.25 inference(scs_inference,[],[94,575,30])). % 68.14/68.25 cnf(3318,plain, % 68.14/68.25 (P12(f15(f21(a2)),a1)), % 68.14/68.25 inference(scs_inference,[],[94,541,577,575,580,55,97,30,35,21,31,36,25])). % 68.14/68.25 cnf(3334,plain, % 68.14/68.25 (P9(f17(a1,a2),a2,a1)), % 68.14/68.25 inference(scs_inference,[],[94,107,109,3156,30,35,31])). % 68.14/68.25 cnf(3344,plain, % 68.14/68.25 (P9(f17(a2,f19(a1)),a1,f19(a2))), % 68.14/68.25 inference(scs_inference,[],[94,3167,30])). % 68.14/68.25 cnf(3350,plain, % 68.14/68.25 (P9(f17(f19(a1),a2),f19(a2),a1)), % 68.14/68.25 inference(scs_inference,[],[94,111,3165,3167,122,30,35,36,31])). % 68.14/68.25 cnf(3360,plain, % 68.14/68.25 (P10(f16(a2,x33601),a1,x33601)), % 68.14/68.25 inference(scs_inference,[],[94,134,3308,3334,58,30,31,35])). % 68.14/68.25 cnf(3361,plain, % 68.14/68.25 (P10(f16(x33611,x33612),x33611,x33612)), % 68.14/68.25 inference(rename_variables,[],[58])). % 68.14/68.25 cnf(3362,plain, % 68.14/68.25 (P10(f16(x33621,a2),x33621,a1)), % 68.14/68.25 inference(scs_inference,[],[94,134,3308,3334,58,3361,30,31,35,36])). % 68.14/68.25 cnf(3374,plain, % 68.14/68.25 (P10(f16(a2,x33741),a1,x33741)), % 68.14/68.25 inference(rename_variables,[],[3360])). % 68.14/68.25 cnf(3375,plain, % 68.14/68.25 (P10(x33751,a1,x33752)+~E(f16(a2,x33752),x33751)), % 68.14/68.25 inference(scs_inference,[],[94,2917,3344,3350,3360,3374,30,31,36,34])). % 68.14/68.25 cnf(3390,plain, % 68.14/68.25 (P9(f17(a2,x33901),a1,x33901)), % 68.14/68.25 inference(scs_inference,[],[94,57,30])). % 68.14/68.25 cnf(3391,plain, % 68.14/68.25 (P9(f17(x33911,x33912),x33911,x33912)), % 68.14/68.25 inference(rename_variables,[],[57])). % 68.14/68.25 cnf(3392,plain, % 68.14/68.25 (P9(f17(x33921,a2),x33921,a1)), % 68.14/68.25 inference(scs_inference,[],[94,57,3391,30,31])). % 68.14/68.25 cnf(3400,plain, % 68.14/68.25 (P9(f17(a2,a2),a1,a1)), % 68.14/68.25 inference(scs_inference,[],[94,3392,30])). % 68.14/68.25 cnf(3402,plain, % 68.14/68.25 (P10(x34021,x34022,a1)+~E(f16(x34022,a2),x34021)), % 68.14/68.25 inference(scs_inference,[],[94,3392,3362,30,34])). % 68.14/68.25 cnf(3409,plain, % 68.14/68.25 (P9(x34091,a1,x34092)+~E(f17(a2,x34092),x34091)), % 68.14/68.25 inference(scs_inference,[],[3390,29])). % 68.14/68.25 cnf(3422,plain, % 68.14/68.25 (P9(x34221,x34222,a1)+~E(f17(x34222,a2),x34221)), % 68.14/68.25 inference(scs_inference,[],[3392,29])). % 68.14/68.25 cnf(3738,plain, % 68.14/68.25 (E(f23(a2),f23(a1))), % 68.14/68.25 inference(scs_inference,[],[41,5,2])). % 68.14/68.25 cnf(3739,plain, % 68.14/68.25 (E(f23(a1),f23(a2))), % 68.14/68.25 inference(scs_inference,[],[3738,2])). % 68.14/68.25 cnf(3782,plain, % 68.14/68.25 (P12(f23(a2),f23(a1))), % 68.14/68.25 inference(scs_inference,[],[3739,50,24])). % 68.14/68.25 cnf(3783,plain, % 68.14/68.25 (P12(x37831,x37831)), % 68.14/68.25 inference(rename_variables,[],[50])). % 68.14/68.25 cnf(3786,plain, % 68.14/68.25 (P10(f16(f19(a1),f23(a1)),f19(a2),f23(a2))), % 68.14/68.25 inference(scs_inference,[],[3739,3119,107,50,24,31,36])). % 68.14/68.25 cnf(3790,plain, % 68.14/68.25 (P12(f23(a1),f23(a2))), % 68.14/68.25 inference(scs_inference,[],[3739,3119,107,55,50,3783,24,31,36,21,25])). % 68.14/68.25 cnf(3824,plain, % 68.14/68.25 (P10(f16(f23(a1),x38241),f23(a2),x38241)), % 68.14/68.25 inference(scs_inference,[],[3739,3360,3390,58,31,36,35])). % 68.14/68.25 cnf(3841,plain, % 68.14/68.25 (P9(f17(f23(a1),a9),f23(a2),a10)), % 68.14/68.25 inference(scs_inference,[],[3739,541,577,575,3362,31,36,35,30])). % 68.14/68.25 cnf(3843,plain, % 68.14/68.25 (P10(x38431,f23(a2),x38432)+~E(f16(f23(a1),x38432),x38431)), % 68.14/68.25 inference(scs_inference,[],[3739,541,577,575,3824,3362,31,36,35,30,34])). % 68.14/68.25 cnf(3863,plain, % 68.14/68.25 (P10(f16(x38631,f23(a1)),x38631,f23(a2))), % 68.14/68.25 inference(scs_inference,[],[3739,134,3841,58,31,36])). % 68.14/68.25 cnf(3888,plain, % 68.14/68.25 (P9(f17(x38881,f23(a1)),x38881,f23(a2))), % 68.14/68.25 inference(scs_inference,[],[3739,57,31])). % 68.14/68.25 cnf(3889,plain, % 68.14/68.25 (P9(f17(x38891,x38892),x38891,x38892)), % 68.14/68.25 inference(rename_variables,[],[57])). % 68.14/68.25 cnf(3890,plain, % 68.14/68.25 (P9(f17(f23(a1),x38901),f23(a2),x38901)), % 68.14/68.25 inference(scs_inference,[],[3739,57,3889,31,30])). % 68.14/68.25 cnf(3899,plain, % 68.14/68.25 (P9(f17(f23(a1),f23(a1)),f23(a2),f23(a2))), % 68.14/68.25 inference(scs_inference,[],[3739,3890,31])). % 68.14/68.25 cnf(3907,plain, % 68.14/68.25 (P10(x39071,x39072,f23(a2))+~E(f16(x39072,f23(a1)),x39071)), % 68.14/68.25 inference(scs_inference,[],[3863,34])). % 68.14/68.25 cnf(3908,plain, % 68.14/68.25 (P9(x39081,x39082,f23(a2))+~E(f17(x39082,f23(a1)),x39081)), % 68.14/68.25 inference(scs_inference,[],[3888,3863,34,29])). % 68.14/68.25 cnf(3928,plain, % 68.14/68.25 (P9(x39281,f23(a2),x39282)+~E(f17(f23(a1),x39282),x39281)), % 68.14/68.25 inference(scs_inference,[],[3890,29])). % 68.14/68.25 cnf(4502,plain, % 68.14/68.25 (E(f15(f23(a2)),f15(f23(a1)))), % 68.14/68.25 inference(scs_inference,[],[3739,10,2])). % 68.14/68.25 cnf(4503,plain, % 68.14/68.25 (E(f15(f23(a1)),f15(f23(a2)))), % 68.14/68.25 inference(scs_inference,[],[4502,2])). % 68.14/68.25 cnf(4569,plain, % 68.14/68.25 (P1(f15(f21(a3)))), % 68.14/68.25 inference(scs_inference,[],[55,119,76])). % 68.14/68.25 cnf(4574,plain, % 68.14/68.25 (P1(f15(f21(a11)))), % 68.14/68.25 inference(scs_inference,[],[55,136,76])). % 68.14/68.25 cnf(4643,plain, % 68.14/68.25 (~P6(a20,x46431)+~E(x46431,f21(a11))), % 68.14/68.25 inference(scs_inference,[],[2058,33])). % 68.14/68.25 cnf(4668,plain, % 68.14/68.25 (P5(a13)), % 68.14/68.25 inference(scs_inference,[],[46,64])). % 68.14/68.25 cnf(4703,plain, % 68.14/68.25 (~E(x47031,a3)+~E(a20,x47031)), % 68.14/68.25 inference(scs_inference,[],[174,3])). % 68.14/68.25 cnf(4707,plain, % 68.14/68.25 (~E(x47071,a3)+~E(a12,x47071)), % 68.14/68.25 inference(scs_inference,[],[216,3])). % 68.14/68.25 cnf(5232,plain, % 68.14/68.25 (P3(f6(a20))), % 68.14/68.25 inference(scs_inference,[],[60,65])). % 68.14/68.25 cnf(5234,plain, % 68.14/68.25 (P3(f7(a12))), % 68.14/68.25 inference(scs_inference,[],[60,59,65,66])). % 68.14/68.25 cnf(5236,plain, % 68.14/68.25 (~P1(f6(a20))), % 68.14/68.25 inference(scs_inference,[],[60,59,65,66,68])). % 68.14/68.25 cnf(5238,plain, % 68.14/68.25 (~P1(f7(a20))), % 68.14/68.25 inference(scs_inference,[],[60,59,65,66,68,69])). % 68.14/68.25 cnf(5240,plain, % 68.14/68.25 (P7(f18(a13),a13)), % 68.14/68.25 inference(scs_inference,[],[46,60,59,65,66,68,69,70])). % 68.14/68.25 cnf(5250,plain, % 68.14/68.25 (P2(f7(a20),f21(a20))), % 68.14/68.25 inference(scs_inference,[],[547,3899,3786,46,60,59,65,66,68,69,70,77,89,90,72,73])). % 68.14/68.25 cnf(5254,plain, % 68.14/68.25 (E(f15(a1),f15(a2))), % 68.14/68.25 inference(scs_inference,[],[41,547,3899,3786,46,60,59,3738,65,66,68,69,70,77,89,90,72,73,4,5,10])). % 68.14/68.25 cnf(5255,plain, % 68.14/68.25 (E(f6(a1),f6(a2))), % 68.14/68.25 inference(scs_inference,[],[41,547,3899,3786,46,60,59,3738,65,66,68,69,70,77,89,90,72,73,4,5,10,15])). % 68.14/68.25 cnf(5256,plain, % 68.14/68.25 (E(f7(a1),f7(a2))), % 68.14/68.25 inference(scs_inference,[],[41,547,3899,3786,46,60,59,3738,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16])). % 68.14/68.25 cnf(5258,plain, % 68.14/68.25 (E(f18(a1),f18(a2))), % 68.14/68.25 inference(scs_inference,[],[41,547,3899,3786,46,60,59,3738,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16,17,18])). % 68.14/68.25 cnf(5259,plain, % 68.14/68.25 (P9(f23(a13),f19(a13),f19(a13))), % 68.14/68.25 inference(scs_inference,[],[41,547,3899,3786,46,60,59,3738,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16,17,18,86])). % 68.14/68.25 cnf(5264,plain, % 68.14/68.25 (E(f22(x52641,a1),f22(x52641,a2))), % 68.14/68.25 inference(scs_inference,[],[41,547,3899,3786,588,46,60,59,3738,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16,17,18,86,91,6,7])). % 68.14/68.25 cnf(5265,plain, % 68.14/68.25 (E(f4(a1,x52651),f4(a2,x52651))), % 68.14/68.25 inference(scs_inference,[],[41,547,3899,3786,588,46,60,59,3738,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16,17,18,86,91,6,7,8])). % 68.14/68.25 cnf(5266,plain, % 68.14/68.25 (E(f4(x52661,a1),f4(x52661,a2))), % 68.14/68.25 inference(scs_inference,[],[41,547,3899,3786,588,46,60,59,3738,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16,17,18,86,91,6,7,8,9])). % 68.14/68.25 cnf(5267,plain, % 68.14/68.25 (E(f17(a1,x52671),f17(a2,x52671))), % 68.14/68.25 inference(scs_inference,[],[41,547,3899,3786,588,46,60,59,3738,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16,17,18,86,91,6,7,8,9,11])). % 68.14/68.25 cnf(5268,plain, % 68.14/68.25 (E(f17(x52681,a1),f17(x52681,a2))), % 68.14/68.25 inference(scs_inference,[],[41,547,3899,3786,588,46,60,59,3738,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16,17,18,86,91,6,7,8,9,11,12])). % 68.14/68.25 cnf(5269,plain, % 68.14/68.25 (E(f16(a1,x52691),f16(a2,x52691))), % 68.14/68.25 inference(scs_inference,[],[41,547,3899,3786,588,46,60,59,3738,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16,17,18,86,91,6,7,8,9,11,12,13])). % 68.14/68.25 cnf(5270,plain, % 68.14/68.25 (E(f16(x52701,a1),f16(x52701,a2))), % 68.14/68.25 inference(scs_inference,[],[41,547,3899,3786,588,46,60,59,3738,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16,17,18,86,91,6,7,8,9,11,12,13,14])). % 68.14/68.25 cnf(5271,plain, % 68.14/68.25 (E(f15(f21(a3)),a3)), % 68.14/68.25 inference(scs_inference,[],[41,547,3899,3786,588,46,4569,60,59,3738,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16,17,18,86,91,6,7,8,9,11,12,13,14,62])). % 68.14/68.26 cnf(5278,plain, % 68.14/68.26 (P6(f15(f6(a20)),f6(a20))), % 68.14/68.26 inference(scs_inference,[],[41,972,547,3899,3786,588,46,4569,60,59,3738,55,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16,17,18,86,91,6,7,8,9,11,12,13,14,62,2,63,79,76])). % 68.14/68.26 cnf(5279,plain, % 68.14/68.26 (P2(f15(x52791),x52791)), % 68.14/68.26 inference(rename_variables,[],[55])). % 68.14/68.26 cnf(5283,plain, % 68.14/68.26 (P3(a3)), % 68.14/68.26 inference(scs_inference,[],[41,972,547,3899,3786,588,46,4569,95,60,59,3738,55,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16,17,18,86,91,6,7,8,9,11,12,13,14,62,2,63,79,76,33,22])). % 68.14/68.26 cnf(5284,plain, % 68.14/68.26 (E(f22(a1,a1),f22(a2,a2))), % 68.14/68.26 inference(scs_inference,[],[41,972,547,3899,3786,588,46,4569,95,60,59,3738,55,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16,17,18,86,91,6,7,8,9,11,12,13,14,62,2,63,79,76,33,22,3])). % 68.14/68.26 cnf(5285,plain, % 68.14/68.26 (~P8(a5,a2,a10)), % 68.14/68.26 inference(scs_inference,[],[41,972,547,3899,3786,588,61,46,4569,95,60,59,3738,134,55,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16,17,18,86,91,6,7,8,9,11,12,13,14,62,2,63,79,76,33,22,3,39])). % 68.14/68.26 cnf(5286,plain, % 68.14/68.26 (~P8(a5,a1,a9)), % 68.14/68.26 inference(scs_inference,[],[41,972,547,3899,3786,588,61,46,4569,95,60,59,3738,134,55,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16,17,18,86,91,6,7,8,9,11,12,13,14,62,2,63,79,76,33,22,3,39,38])). % 68.14/68.26 cnf(5292,plain, % 68.14/68.26 (P2(f15(f6(a20)),a20)), % 68.14/68.26 inference(scs_inference,[],[41,972,547,3899,3786,588,61,46,4569,95,60,59,51,3738,52,134,55,47,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16,17,18,86,91,6,7,8,9,11,12,13,14,62,2,63,79,76,33,22,3,39,38,92,80,34,85])). % 68.14/68.26 cnf(5294,plain, % 68.14/68.26 (P10(f16(f23(a2),f23(a1)),f23(a1),f23(a2))), % 68.14/68.26 inference(scs_inference,[],[41,972,547,3899,3786,588,3863,61,46,4569,95,60,59,51,3738,52,134,55,47,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16,17,18,86,91,6,7,8,9,11,12,13,14,62,2,63,79,76,33,22,3,39,38,92,80,34,85,35])). % 68.14/68.26 cnf(5296,plain, % 68.14/68.26 (P4(a8)), % 68.14/68.26 inference(scs_inference,[],[41,972,547,3899,3786,588,3863,61,46,4569,95,60,59,51,3738,52,134,49,55,47,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16,17,18,86,91,6,7,8,9,11,12,13,14,62,2,63,79,76,33,22,3,39,38,92,80,34,85,35,74])). % 68.14/68.26 cnf(5300,plain, % 68.14/68.26 (P2(f15(x53001),x53001)), % 68.14/68.26 inference(rename_variables,[],[55])). % 68.14/68.26 cnf(5303,plain, % 68.14/68.26 (P2(a3,f21(a3))), % 68.14/68.26 inference(scs_inference,[],[41,972,547,3899,3786,588,3863,61,46,4569,95,60,59,4503,51,3738,52,134,49,55,5279,5300,50,47,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16,17,18,86,91,6,7,8,9,11,12,13,14,62,2,63,79,76,33,22,3,39,38,92,80,34,85,35,74,19,21,24,20])). % 68.14/68.26 cnf(5305,plain, % 68.14/68.26 (~P2(a12,f21(a3))), % 68.14/68.26 inference(scs_inference,[],[41,972,547,3899,3786,588,3863,61,46,4569,95,60,59,4503,113,51,3738,43,52,134,49,55,5279,5300,50,47,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16,17,18,86,91,6,7,8,9,11,12,13,14,62,2,63,79,76,33,22,3,39,38,92,80,34,85,35,74,19,21,24,20,82])). % 68.14/68.26 cnf(5309,plain, % 68.14/68.26 (P10(f16(f23(a1),f15(a1)),f23(a2),f15(a2))), % 68.14/68.26 inference(scs_inference,[],[41,972,547,3899,3786,588,3863,61,46,4569,3890,3824,95,60,59,4503,113,51,3738,43,52,134,49,55,5279,5300,50,47,65,66,68,69,70,77,89,90,72,73,4,5,10,15,16,17,18,86,91,6,7,8,9,11,12,13,14,62,2,63,79,76,33,22,3,39,38,92,80,34,85,35,74,19,21,24,20,82,31,36])). % 68.14/68.26 cnf(5319,plain, % 68.14/68.26 (~P1(f6(f6(a20)))), % 68.14/68.26 inference(scs_inference,[],[5236,68])). % 68.14/68.26 cnf(5325,plain, % 68.14/68.26 (P2(f17(a2,a2),f21(f4(a1,a1)))), % 68.14/68.26 inference(scs_inference,[],[5296,5236,5294,3400,68,89,70,91])). % 68.14/68.26 cnf(5329,plain, % 68.14/68.26 (E(f15(f21(a11)),a3)), % 68.14/68.26 inference(scs_inference,[],[5296,5236,5294,3400,4574,59,68,89,70,91,73,62])). % 68.14/68.26 cnf(5337,plain, % 68.14/68.26 (E(f16(a10,x53371),f16(a9,x53371))), % 68.14/68.26 inference(scs_inference,[],[5296,5236,5259,5294,3400,4574,59,134,68,89,70,91,73,62,66,90,69,13])). % 68.14/68.26 cnf(5339,plain, % 68.14/68.26 (E(f22(a10,x53391),f22(a9,x53391))), % 68.14/68.26 inference(scs_inference,[],[5296,5236,5259,5294,3400,4574,59,134,68,89,70,91,73,62,66,90,69,13,10,6])). % 68.14/68.26 cnf(5340,plain, % 68.14/68.26 (E(f22(x53401,a10),f22(x53401,a9))), % 68.14/68.26 inference(scs_inference,[],[5296,5236,5259,5294,3400,4574,59,134,68,89,70,91,73,62,66,90,69,13,10,6,7])). % 68.14/68.26 cnf(5342,plain, % 68.14/68.26 (E(f17(a10,x53421),f17(a9,x53421))), % 68.14/68.26 inference(scs_inference,[],[5296,5236,5259,5294,3400,4574,59,134,68,89,70,91,73,62,66,90,69,13,10,6,7,5,11])). % 68.14/68.26 cnf(5345,plain, % 68.14/68.26 (P2(f6(a12),f21(a12))), % 68.14/68.26 inference(scs_inference,[],[5296,5236,5259,5294,549,3400,4574,59,134,68,89,70,91,73,62,66,90,69,13,10,6,7,5,11,77,72])). % 68.14/68.26 cnf(5348,plain, % 68.14/68.26 (P9(f23(a8),f19(a8),f19(a8))), % 68.14/68.26 inference(scs_inference,[],[5296,5236,5259,5294,549,3400,4574,59,134,68,89,70,91,73,62,66,90,69,13,10,6,7,5,11,77,72,17,86])). % 68.14/68.26 cnf(5352,plain, % 68.14/68.26 (E(f4(a10,x53521),f4(a9,x53521))), % 68.14/68.26 inference(scs_inference,[],[5296,5236,5259,5294,549,3400,4574,59,134,68,89,70,91,73,62,66,90,69,13,10,6,7,5,11,77,72,17,86,65,8])). % 68.14/68.26 cnf(5353,plain, % 68.14/68.26 (E(f4(x53531,a10),f4(x53531,a9))), % 68.14/68.26 inference(scs_inference,[],[5296,5236,5259,5294,549,3400,4574,59,134,68,89,70,91,73,62,66,90,69,13,10,6,7,5,11,77,72,17,86,65,8,9])). % 68.14/68.26 cnf(5355,plain, % 68.14/68.26 (E(f16(x53551,a10),f16(x53551,a9))), % 68.14/68.26 inference(scs_inference,[],[5296,5236,5259,5294,549,3400,4574,59,134,68,89,70,91,73,62,66,90,69,13,10,6,7,5,11,77,72,17,86,65,8,9,15,14])). % 68.14/68.26 cnf(5356,plain, % 68.14/68.26 (E(f17(x53561,a10),f17(x53561,a9))), % 68.14/68.26 inference(scs_inference,[],[5296,5236,5259,5294,549,3400,4574,59,134,68,89,70,91,73,62,66,90,69,13,10,6,7,5,11,77,72,17,86,65,8,9,15,14,12])). % 68.14/68.26 cnf(5362,plain, % 68.14/68.26 (E(f22(a2,a2),f22(a1,a1))), % 68.14/68.26 inference(scs_inference,[],[5296,5284,5236,5259,5294,549,3400,4574,59,134,68,89,70,91,73,62,66,90,69,13,10,6,7,5,11,77,72,17,86,65,8,9,15,14,12,18,16,4,63,2])). % 68.14/68.26 cnf(5365,plain, % 68.14/68.26 (P3(f4(a3,a3))), % 68.14/68.26 inference(scs_inference,[],[5283,5296,5284,5236,5259,5294,5292,549,3400,4574,59,60,134,68,89,70,91,73,62,66,90,69,13,10,6,7,5,11,77,72,17,86,65,8,9,15,14,12,18,16,4,63,2,76,79])). % 68.14/68.26 cnf(5367,plain, % 68.14/68.26 (P4(f18(a8))), % 68.14/68.26 inference(scs_inference,[],[5283,5296,5284,5236,5259,5294,5292,549,3400,4574,59,60,134,68,89,70,91,73,62,66,90,69,13,10,6,7,5,11,77,72,17,86,65,8,9,15,14,12,18,16,4,63,2,76,79,74])). % 68.14/68.26 cnf(5369,plain, % 68.14/68.26 (E(f4(a1,a1),f4(a2,a2))), % 68.14/68.26 inference(scs_inference,[],[5283,5296,5284,5265,5266,5236,5259,5294,5292,549,3400,4574,59,60,134,68,89,70,91,73,62,66,90,69,13,10,6,7,5,11,77,72,17,86,65,8,9,15,14,12,18,16,4,63,2,76,79,74,3])). % 68.14/68.26 cnf(5373,plain, % 68.14/68.26 (~P8(a5,a1,a10)), % 68.14/68.26 inference(scs_inference,[],[5283,5286,5296,5284,5265,5266,5236,5259,5294,5292,549,3400,4574,59,60,134,68,89,70,91,73,62,66,90,69,13,10,6,7,5,11,77,72,17,86,65,8,9,15,14,12,18,16,4,63,2,76,79,74,3,19,39])). % 68.14/68.26 cnf(5374,plain, % 68.14/68.26 (P12(f19(a8),f19(a5))), % 68.14/68.26 inference(scs_inference,[],[5283,5286,5296,5284,5265,5266,5236,5259,5294,5292,549,3400,4574,59,60,134,49,47,68,89,70,91,73,62,66,90,69,13,10,6,7,5,11,77,72,17,86,65,8,9,15,14,12,18,16,4,63,2,76,79,74,3,19,39,83])). % 68.14/68.26 cnf(5376,plain, % 68.14/68.26 (P12(f23(a8),f23(a5))), % 68.14/68.26 inference(scs_inference,[],[5283,5286,5296,5284,5265,5266,5236,5259,5294,5292,549,3400,4574,59,60,134,49,47,68,89,70,91,73,62,66,90,69,13,10,6,7,5,11,77,72,17,86,65,8,9,15,14,12,18,16,4,63,2,76,79,74,3,19,39,83,84])). % 68.14/68.26 cnf(5378,plain, % 68.14/68.26 (P6(f22(a2,a9),f23(a8))), % 68.14/68.26 inference(scs_inference,[],[5283,5286,5296,5284,5265,5266,5236,5259,5294,5292,549,151,3400,173,165,4574,59,60,134,49,47,68,89,70,91,73,62,66,90,69,13,10,6,7,5,11,77,72,17,86,65,8,9,15,14,12,18,16,4,63,2,76,79,74,3,19,39,83,84,93])). % 68.14/68.26 cnf(5380,plain, % 68.14/68.26 (P12(a3,a11)), % 68.14/68.26 inference(scs_inference,[],[5283,5286,5296,5284,5265,5266,5236,5259,5294,5292,549,151,3400,173,165,4574,59,60,134,49,47,68,89,70,91,73,62,66,90,69,13,10,6,7,5,11,77,72,17,86,65,8,9,15,14,12,18,16,4,63,2,76,79,74,3,19,39,83,84,93,332])). % 68.14/68.26 cnf(5383,plain, % 68.14/68.26 (~P1(f23(a8))), % 68.14/68.26 inference(scs_inference,[],[5283,5286,5296,5284,5265,5266,5236,5259,5294,5292,549,151,3400,173,165,4574,59,60,134,49,47,68,89,70,91,73,62,66,90,69,13,10,6,7,5,11,77,72,17,86,65,8,9,15,14,12,18,16,4,63,2,76,79,74,3,19,39,83,84,93,332,75,71])). % 68.14/68.26 cnf(5395,plain, % 68.14/68.26 (P7(f18(f18(a8)),f18(a8))), % 68.14/68.26 inference(scs_inference,[],[5367,70])). % 68.14/68.26 cnf(5409,plain, % 68.14/68.26 (E(a11,a3)), % 68.14/68.26 inference(scs_inference,[],[5238,5348,5367,5309,3308,44,70,66,89,91,68,90,65,62])). % 68.14/68.26 cnf(5411,plain, % 68.14/68.26 (P2(a3,f21(a11))), % 68.14/68.26 inference(scs_inference,[],[5380,5238,5348,5367,5309,3308,44,70,66,89,91,68,90,65,62,77])). % 68.14/68.26 cnf(5413,plain, % 68.14/68.26 (P9(f23(a5),f19(a5),f19(a5))), % 68.14/68.26 inference(scs_inference,[],[5380,5238,5348,5367,5309,3308,44,47,70,66,89,91,68,90,65,62,77,86])). % 68.14/68.26 cnf(5415,plain, % 68.14/68.26 (E(f22(x54151,a9),f22(x54151,a10))), % 68.14/68.26 inference(scs_inference,[],[5380,5238,5348,5367,5309,3308,44,42,47,70,66,89,91,68,90,65,62,77,86,7])). % 68.14/68.26 cnf(5419,plain, % 68.14/68.26 (E(f16(a9,x54191),f16(a10,x54191))), % 68.14/68.26 inference(scs_inference,[],[5380,5238,5348,5367,5309,3308,44,42,47,70,66,89,91,68,90,65,62,77,86,7,6,69,13])). % 68.14/68.26 cnf(5420,plain, % 68.14/68.26 (E(f4(a9,x54201),f4(a10,x54201))), % 68.14/68.26 inference(scs_inference,[],[5380,5238,5348,5367,5309,3308,44,42,47,70,66,89,91,68,90,65,62,77,86,7,6,69,13,8])). % 68.14/68.26 cnf(5423,plain, % 68.14/68.26 (E(f16(x54231,a9),f16(x54231,a10))), % 68.14/68.26 inference(scs_inference,[],[5380,5238,5348,5367,5309,3308,44,42,47,70,66,89,91,68,90,65,62,77,86,7,6,69,13,8,5,18,14])). % 68.14/68.26 cnf(5426,plain, % 68.14/68.26 (E(f17(a9,x54261),f17(a10,x54261))), % 68.14/68.26 inference(scs_inference,[],[5380,5238,5348,5367,5309,3308,44,42,47,70,66,89,91,68,90,65,62,77,86,7,6,69,13,8,5,18,14,4,10,11])). % 68.14/68.26 cnf(5427,plain, % 68.14/68.26 (E(f4(x54271,a9),f4(x54271,a10))), % 68.14/68.26 inference(scs_inference,[],[5380,5238,5348,5367,5309,3308,44,42,47,70,66,89,91,68,90,65,62,77,86,7,6,69,13,8,5,18,14,4,10,11,9])). % 68.14/68.26 cnf(5429,plain, % 68.14/68.26 (P3(a11)), % 68.14/68.26 inference(scs_inference,[],[5380,5238,5348,5367,5309,3308,44,42,47,70,66,89,91,68,90,65,62,77,86,7,6,69,13,8,5,18,14,4,10,11,9,15,63])). % 68.14/68.26 cnf(5432,plain, % 68.14/68.26 (E(f17(x54321,a9),f17(x54321,a10))), % 68.14/68.26 inference(scs_inference,[],[5380,5238,5348,5367,5309,3308,44,42,47,70,66,89,91,68,90,65,62,77,86,7,6,69,13,8,5,18,14,4,10,11,9,15,63,17,12])). % 68.14/68.26 cnf(5439,plain, % 68.14/68.26 (P6(f15(f7(a20)),f7(a20))), % 68.14/68.26 inference(scs_inference,[],[5380,5254,5378,5232,5238,5348,5367,5309,3308,44,42,55,47,70,66,89,91,68,90,65,62,77,86,7,6,69,13,8,5,18,14,4,10,11,9,15,63,17,12,16,2,80,79,76])). % 68.14/68.26 cnf(5444,plain, % 68.14/68.26 (P4(f18(a13))), % 68.14/68.26 inference(scs_inference,[],[5380,5254,5340,5378,5232,5238,5348,5367,5240,5309,3308,46,44,42,55,47,70,66,89,91,68,90,65,62,77,86,7,6,69,13,8,5,18,14,4,10,11,9,15,63,17,12,16,2,80,79,76,33,74])). % 68.14/68.26 cnf(5446,plain, % 68.14/68.26 (P6(f22(a2,a10),f23(a8))), % 68.14/68.26 inference(scs_inference,[],[5380,5254,5340,5378,5232,5238,5348,5367,5240,5309,3308,46,44,42,55,47,70,66,89,91,68,90,65,62,77,86,7,6,69,13,8,5,18,14,4,10,11,9,15,63,17,12,16,2,80,79,76,33,74,32])). % 68.14/68.26 cnf(5454,plain, % 68.14/68.26 (P6(f22(a1,a9),f23(a8))), % 68.14/68.26 inference(scs_inference,[],[5380,5362,5254,5264,5340,5378,5232,5238,5348,5367,5240,5309,135,3308,173,46,4569,5296,44,42,55,53,47,70,66,89,91,68,90,65,62,77,86,7,6,69,13,8,5,18,14,4,10,11,9,15,63,17,12,16,2,80,79,76,33,74,32,3,19,83,84,93])). % 68.14/68.26 cnf(5458,plain, % 68.14/68.26 (P10(f16(a9,a10),a10,a9)), % 68.14/68.26 inference(scs_inference,[],[5373,5380,5362,5254,5264,5340,5378,5232,5238,5348,5367,5240,5309,135,3308,173,146,46,4569,5296,44,100,42,55,53,47,70,66,89,91,68,90,65,62,77,86,7,6,69,13,8,5,18,14,4,10,11,9,15,63,17,12,16,2,80,79,76,33,74,32,3,19,83,84,93,92,552])). % 68.14/68.26 cnf(5459,plain, % 68.14/68.26 (P9(f17(a10,a9),a9,a10)), % 68.14/68.26 inference(scs_inference,[],[5373,5380,5362,5254,5264,5340,5378,5232,5238,5348,5367,5240,5309,135,3308,173,146,46,4569,5296,44,100,42,55,53,47,70,66,89,91,68,90,65,62,77,86,7,6,69,13,8,5,18,14,4,10,11,9,15,63,17,12,16,2,80,79,76,33,74,32,3,19,83,84,93,92,552,590])). % 68.14/68.26 cnf(5460,plain, % 68.14/68.26 (P10(f16(a10,a9),a9,a10)), % 68.14/68.26 inference(scs_inference,[],[5373,5380,5362,5254,5264,5340,5378,5232,5238,5348,5367,5240,5309,135,3308,173,146,46,4569,5296,44,100,42,55,53,47,70,66,89,91,68,90,65,62,77,86,7,6,69,13,8,5,18,14,4,10,11,9,15,63,17,12,16,2,80,79,76,33,74,32,3,19,83,84,93,92,552,590,591])). % 68.14/68.26 cnf(5461,plain, % 68.14/68.26 (P9(f17(a9,a10),a10,a9)), % 68.14/68.26 inference(scs_inference,[],[5373,5380,5362,5254,5264,5340,5378,5232,5238,5348,5367,5240,5309,135,3308,173,146,46,4569,5296,44,100,42,55,53,47,70,66,89,91,68,90,65,62,77,86,7,6,69,13,8,5,18,14,4,10,11,9,15,63,17,12,16,2,80,79,76,33,74,32,3,19,83,84,93,92,552,590,591,596])). % 68.14/68.26 cnf(5467,plain, % 68.14/68.26 (P10(f16(a2,a10),a1,a9)), % 68.14/68.26 inference(scs_inference,[],[5423,3375])). % 68.14/68.26 cnf(5468,plain, % 68.14/68.26 (E(f16(x54681,a9),f16(x54681,a10))), % 68.14/68.26 inference(rename_variables,[],[5423])). % 68.14/68.26 cnf(5469,plain, % 68.14/68.26 (P10(f16(a10,a2),a9,a1)), % 68.14/68.26 inference(scs_inference,[],[5419,5423,3375,3402])). % 68.14/68.26 cnf(5470,plain, % 68.14/68.26 (E(f16(a9,x54701),f16(a10,x54701))), % 68.14/68.26 inference(rename_variables,[],[5419])). % 68.14/68.26 cnf(5472,plain, % 68.14/68.26 (E(f17(x54721,a9),f17(x54721,a10))), % 68.14/68.26 inference(rename_variables,[],[5432])). % 68.14/68.26 cnf(5473,plain, % 68.14/68.26 (P9(f17(a10,a2),a9,a1)), % 68.14/68.26 inference(scs_inference,[],[5419,5423,5426,5432,3375,3402,3409,3422])). % 68.14/68.26 cnf(5474,plain, % 68.14/68.26 (E(f17(a9,x54741),f17(a10,x54741))), % 68.14/68.26 inference(rename_variables,[],[5426])). % 68.14/68.26 cnf(5476,plain, % 68.14/68.26 (E(f16(x54761,a9),f16(x54761,a10))), % 68.14/68.26 inference(rename_variables,[],[5423])). % 68.14/68.26 cnf(5478,plain, % 68.14/68.26 (E(f17(x54781,a9),f17(x54781,a10))), % 68.14/68.26 inference(rename_variables,[],[5432])). % 68.14/68.26 cnf(5480,plain, % 68.14/68.26 (E(f17(a9,x54801),f17(a10,x54801))), % 68.14/68.26 inference(rename_variables,[],[5426])). % 68.14/68.26 cnf(5482,plain, % 68.14/68.26 (E(f16(a9,x54821),f16(a10,x54821))), % 68.14/68.26 inference(rename_variables,[],[5419])). % 68.14/68.26 cnf(5484,plain, % 68.14/68.26 (E(f16(x54841,a9),f16(x54841,a10))), % 68.14/68.26 inference(rename_variables,[],[5423])). % 68.14/68.26 cnf(5486,plain, % 68.14/68.26 (E(f16(a9,x54861),f16(a10,x54861))), % 68.14/68.26 inference(rename_variables,[],[5419])). % 68.14/68.26 cnf(5488,plain, % 68.14/68.26 (E(f17(a9,x54881),f17(a10,x54881))), % 68.14/68.26 inference(rename_variables,[],[5426])). % 68.14/68.26 cnf(5490,plain, % 68.14/68.26 (E(f17(x54901,a9),f17(x54901,a10))), % 68.14/68.26 inference(rename_variables,[],[5432])). % 68.14/68.26 cnf(5491,plain, % 68.14/68.26 (P9(f17(a1,a10),a2,a9)), % 68.14/68.26 inference(scs_inference,[],[5419,5470,5482,5423,5468,5476,5426,5474,5480,5432,5472,5478,5490,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154])). % 68.14/68.26 cnf(5493,plain, % 68.14/68.26 (P10(f16(a1,a10),a2,a9)), % 68.14/68.26 inference(scs_inference,[],[5419,5470,5482,5423,5468,5476,5484,5426,5474,5480,5432,5472,5478,5490,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197])). % 68.14/68.26 cnf(5495,plain, % 68.14/68.26 (P9(f17(a10,a1),a9,a2)), % 68.14/68.26 inference(scs_inference,[],[5419,5470,5482,5423,5468,5476,5484,5426,5474,5480,5488,5432,5472,5478,5490,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197,208])). % 68.14/68.26 cnf(5497,plain, % 68.14/68.26 (P10(f16(a10,a1),a9,a2)), % 68.14/68.26 inference(scs_inference,[],[5419,5470,5482,5486,5423,5468,5476,5484,5426,5474,5480,5488,5432,5472,5478,5490,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197,208,228])). % 68.14/68.26 cnf(5513,plain, % 68.14/68.26 (~P1(f7(f23(a8)))), % 68.14/68.26 inference(scs_inference,[],[5419,5470,5482,5486,5423,5468,5476,5484,5426,5474,5480,5488,5432,5472,5478,5490,5454,5383,5444,5458,5459,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197,208,228,89,75,66,68,70,65,91,69])). % 68.14/68.26 cnf(5517,plain, % 68.14/68.26 (E(f22(a11,x55171),f22(a3,x55171))), % 68.14/68.26 inference(scs_inference,[],[5409,5419,5470,5482,5486,5423,5468,5476,5484,5426,5474,5480,5488,5432,5472,5478,5490,5454,5383,5413,5444,5458,5459,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197,208,228,89,75,66,68,70,65,91,69,90,6])). % 68.14/68.26 cnf(5520,plain, % 68.14/68.26 (E(f16(a11,x55201),f16(a3,x55201))), % 68.14/68.26 inference(scs_inference,[],[5409,5419,5470,5482,5486,5423,5468,5476,5484,5426,5474,5480,5488,5432,5472,5478,5490,5454,5374,5383,5413,5444,5458,5459,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197,208,228,89,75,66,68,70,65,91,69,90,6,77,13])). % 68.14/68.26 cnf(5524,plain, % 68.14/68.26 (E(f17(a11,x55241),f17(a3,x55241))), % 68.14/68.26 inference(scs_inference,[],[5409,5419,5470,5482,5486,5423,5468,5476,5484,5426,5474,5480,5488,5432,5472,5478,5490,5454,5374,5383,5413,5444,5458,5459,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197,208,228,89,75,66,68,70,65,91,69,90,6,77,13,10,7,5,11])). % 68.14/68.26 cnf(5526,plain, % 68.14/68.26 (E(f4(a11,x55261),f4(a3,x55261))), % 68.14/68.26 inference(scs_inference,[],[5409,5419,5470,5482,5486,5423,5468,5476,5484,5426,5474,5480,5488,5432,5472,5478,5490,5454,5374,5383,5413,5444,5458,5459,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197,208,228,89,75,66,68,70,65,91,69,90,6,77,13,10,7,5,11,4,8])). % 68.14/68.26 cnf(5527,plain, % 68.14/68.26 (E(f17(x55271,a11),f17(x55271,a3))), % 68.14/68.26 inference(scs_inference,[],[5409,5419,5470,5482,5486,5423,5468,5476,5484,5426,5474,5480,5488,5432,5472,5478,5490,5454,5374,5383,5413,5444,5458,5459,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197,208,228,89,75,66,68,70,65,91,69,90,6,77,13,10,7,5,11,4,8,12])). % 68.14/68.26 cnf(5529,plain, % 68.14/68.26 (E(f4(x55291,a11),f4(x55291,a3))), % 68.14/68.26 inference(scs_inference,[],[5409,5419,5470,5482,5486,5423,5468,5476,5484,5426,5474,5480,5488,5432,5472,5478,5490,5454,5374,5383,5413,5444,5458,5459,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197,208,228,89,75,66,68,70,65,91,69,90,6,77,13,10,7,5,11,4,8,12,18,9])). % 68.14/68.26 cnf(5531,plain, % 68.14/68.26 (E(f16(x55311,a11),f16(x55311,a3))), % 68.14/68.26 inference(scs_inference,[],[5409,5419,5470,5482,5486,5423,5468,5476,5484,5426,5474,5480,5488,5432,5472,5478,5490,5454,5374,5383,5413,5444,5458,5459,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197,208,228,89,75,66,68,70,65,91,69,90,6,77,13,10,7,5,11,4,8,12,18,9,15,14])). % 68.14/68.26 cnf(5532,plain, % 68.14/68.26 (E(a3,a11)), % 68.14/68.26 inference(scs_inference,[],[5409,5419,5470,5482,5486,5423,5468,5476,5484,5426,5474,5480,5488,5432,5472,5478,5490,5454,5374,5383,5413,5444,5458,5459,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197,208,228,89,75,66,68,70,65,91,69,90,6,77,13,10,7,5,11,4,8,12,18,9,15,14,2])). % 68.14/68.26 cnf(5533,plain, % 68.14/68.26 (E(f21(a11),f21(a3))), % 68.14/68.26 inference(scs_inference,[],[5409,5419,5470,5482,5486,5423,5468,5476,5484,5426,5474,5480,5488,5432,5472,5478,5490,5454,5374,5383,5413,5444,5458,5459,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197,208,228,89,75,66,68,70,65,91,69,90,6,77,13,10,7,5,11,4,8,12,18,9,15,14,2,17])). % 68.14/68.26 cnf(5537,plain, % 68.14/68.26 (P3(f4(a11,a11))), % 68.14/68.26 inference(scs_inference,[],[5409,5429,5419,5470,5482,5486,5423,5468,5476,5484,5426,5474,5480,5488,5432,5472,5478,5490,5454,5374,5383,5413,5444,5458,5459,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197,208,228,89,75,66,68,70,65,91,69,90,6,77,13,10,7,5,11,4,8,12,18,9,15,14,2,17,80,16,79])). % 68.14/68.26 cnf(5539,plain, % 68.14/68.26 (P6(f15(f23(a8)),f23(a8))), % 68.14/68.26 inference(scs_inference,[],[5409,5429,5419,5470,5482,5486,5423,5468,5476,5484,5426,5474,5480,5488,5432,5472,5478,5490,5454,5374,5383,5413,5444,5458,5459,55,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197,208,228,89,75,66,68,70,65,91,69,90,6,77,13,10,7,5,11,4,8,12,18,9,15,14,2,17,80,16,79,76])). % 68.14/68.26 cnf(5542,plain, % 68.14/68.26 (~P2(a12,f21(a11))), % 68.14/68.26 inference(scs_inference,[],[5409,5429,5419,5470,5482,5486,5423,5468,5476,5484,5426,5474,5480,5488,5432,5472,5478,5490,5454,5374,5383,5413,5444,5458,5459,5305,55,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197,208,228,89,75,66,68,70,65,91,69,90,6,77,13,10,7,5,11,4,8,12,18,9,15,14,2,17,80,16,79,76,21])). % 68.14/68.26 cnf(5547,plain, % 68.14/68.26 (P6(f22(a1,a10),f23(a8))), % 68.14/68.26 inference(scs_inference,[],[5409,5429,5446,5415,5419,5470,5482,5486,5423,5468,5476,5484,5426,5474,5480,5488,5432,5472,5478,5490,5454,5374,5383,5413,5444,5458,5459,5305,132,55,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197,208,228,89,75,66,68,70,65,91,69,90,6,77,13,10,7,5,11,4,8,12,18,9,15,14,2,17,80,16,79,76,21,33,74,32])). % 68.14/68.26 cnf(5548,plain, % 68.14/68.26 (E(f22(x55481,a9),f22(x55481,a10))), % 68.14/68.26 inference(rename_variables,[],[5415])). % 68.14/68.26 cnf(5553,plain, % 68.14/68.26 (P9(f17(a3,a9),a11,a10)), % 68.14/68.26 inference(scs_inference,[],[5409,5429,5446,5339,5415,5548,5419,5470,5482,5486,5423,5468,5476,5484,5426,5474,5480,5488,5432,5472,5478,5490,5454,5374,5383,5413,5444,5458,5459,5305,132,4574,55,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197,208,228,89,75,66,68,70,65,91,69,90,6,77,13,10,7,5,11,4,8,12,18,9,15,14,2,17,80,16,79,76,21,33,74,32,3,19,590])). % 68.14/68.26 cnf(5554,plain, % 68.14/68.26 (P10(f16(a9,a3),a10,a11)), % 68.14/68.26 inference(scs_inference,[],[5409,5429,5446,5339,5415,5548,5419,5470,5482,5486,5423,5468,5476,5484,5426,5474,5480,5488,5432,5472,5478,5490,5454,5374,5383,5413,5444,5458,5459,5305,132,4574,55,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197,208,228,89,75,66,68,70,65,91,69,90,6,77,13,10,7,5,11,4,8,12,18,9,15,14,2,17,80,16,79,76,21,33,74,32,3,19,590,552])). % 68.14/68.26 cnf(5555,plain, % 68.14/68.26 (P9(f17(a9,a3),a10,a11)), % 68.14/68.26 inference(scs_inference,[],[5409,5429,5446,5339,5415,5548,5419,5470,5482,5486,5423,5468,5476,5484,5426,5474,5480,5488,5432,5472,5478,5490,5454,5374,5383,5413,5444,5458,5459,5305,132,4574,55,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197,208,228,89,75,66,68,70,65,91,69,90,6,77,13,10,7,5,11,4,8,12,18,9,15,14,2,17,80,16,79,76,21,33,74,32,3,19,590,552,596])). % 68.14/68.26 cnf(5556,plain, % 68.14/68.26 (P10(f16(a3,a9),a11,a10)), % 68.14/68.26 inference(scs_inference,[],[5409,5429,5446,5339,5415,5548,5419,5470,5482,5486,5423,5468,5476,5484,5426,5474,5480,5488,5432,5472,5478,5490,5454,5374,5383,5413,5444,5458,5459,5305,132,4574,55,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197,208,228,89,75,66,68,70,65,91,69,90,6,77,13,10,7,5,11,4,8,12,18,9,15,14,2,17,80,16,79,76,21,33,74,32,3,19,590,552,596,591])). % 68.14/68.26 cnf(5557,plain, % 68.14/68.26 (P12(f15(f21(a3)),a11)), % 68.14/68.26 inference(scs_inference,[],[5409,5429,5446,5339,5415,5548,5419,5470,5482,5486,5423,5468,5476,5484,5426,5474,5480,5488,5432,5472,5478,5490,5454,5374,5383,5413,5444,5458,5459,5305,132,97,4574,55,3375,3402,3409,3422,3138,3177,3189,3195,3843,3907,3908,3928,154,197,208,228,89,75,66,68,70,65,91,69,90,6,77,13,10,7,5,11,4,8,12,18,9,15,14,2,17,80,16,79,76,21,33,74,32,3,19,590,552,596,591,25])). % 68.14/68.26 cnf(5562,plain, % 68.14/68.26 (P9(f17(a2,a3),a1,a11)), % 68.14/68.26 inference(scs_inference,[],[5527,3409])). % 68.14/68.26 cnf(5563,plain, % 68.14/68.26 (E(f17(x55631,a11),f17(x55631,a3))), % 68.14/68.26 inference(rename_variables,[],[5527])). % 68.14/68.26 cnf(5565,plain, % 68.14/68.26 (E(f17(a11,x55651),f17(a3,x55651))), % 68.14/68.26 inference(rename_variables,[],[5524])). % 68.14/68.26 cnf(5567,plain, % 68.14/68.26 (E(f16(x55671,a11),f16(x55671,a3))), % 68.14/68.26 inference(rename_variables,[],[5531])). % 68.14/68.26 cnf(5568,plain, % 68.14/68.26 (P9(f17(a1,a3),a2,a11)), % 68.14/68.26 inference(scs_inference,[],[5524,5527,5563,5531,3409,3189,3138,154])). % 68.14/68.26 cnf(5569,plain, % 68.14/68.26 (E(f17(x55691,a11),f17(x55691,a3))), % 68.14/68.26 inference(rename_variables,[],[5527])). % 68.14/68.26 cnf(5571,plain, % 68.14/68.26 (E(f17(x55711,a11),f17(x55711,a3))), % 68.14/68.26 inference(rename_variables,[],[5527])). % 68.14/68.26 cnf(5573,plain, % 68.14/68.26 (E(f16(a11,x55731),f16(a3,x55731))), % 68.14/68.26 inference(rename_variables,[],[5520])). % 68.14/68.26 cnf(5574,plain, % 68.14/68.26 (P10(f16(a3,a1),a11,a2)), % 68.14/68.26 inference(scs_inference,[],[5520,5573,5524,5527,5563,5569,5531,3409,3189,3138,154,3928,3907,228])). % 68.14/68.26 cnf(5575,plain, % 68.14/68.26 (E(f16(a11,x55751),f16(a3,x55751))), % 68.14/68.26 inference(rename_variables,[],[5520])). % 68.14/68.26 cnf(5576,plain, % 68.14/68.26 (P10(f16(a3,a2),a11,a1)), % 68.14/68.26 inference(scs_inference,[],[5520,5573,5575,5524,5527,5563,5569,5531,3409,3189,3138,154,3928,3907,228,3402])). % 68.14/68.26 cnf(5577,plain, % 68.14/68.26 (E(f16(a11,x55771),f16(a3,x55771))), % 68.14/68.26 inference(rename_variables,[],[5520])). % 68.14/68.26 cnf(5580,plain, % 68.14/68.26 (P9(f17(a3,a2),a11,a1)), % 68.14/68.26 inference(scs_inference,[],[5520,5573,5575,5577,5524,5565,5527,5563,5569,5531,3409,3189,3138,154,3928,3907,228,3402,3195,3422])). % 68.14/68.26 cnf(5581,plain, % 68.14/68.26 (E(f17(a11,x55811),f17(a3,x55811))), % 68.14/68.26 inference(rename_variables,[],[5524])). % 68.14/68.26 cnf(5582,plain, % 68.14/68.26 (P10(f16(a1,a3),a2,a11)), % 68.14/68.26 inference(scs_inference,[],[5520,5573,5575,5577,5524,5565,5527,5563,5569,5531,5567,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197])). % 68.14/68.26 cnf(5583,plain, % 68.14/68.26 (E(f16(x55831,a11),f16(x55831,a3))), % 68.14/68.26 inference(rename_variables,[],[5531])). % 68.14/68.26 cnf(5584,plain, % 68.14/68.26 (~P1(f6(a12))), % 68.14/68.26 inference(scs_inference,[],[5520,5573,5575,5577,5524,5565,5527,5563,5569,5531,5567,59,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68])). % 68.14/68.26 cnf(5586,plain, % 68.14/68.26 (P7(f18(a5),a5)), % 68.14/68.26 inference(scs_inference,[],[5520,5573,5575,5577,5524,5565,5527,5563,5569,5531,5567,59,47,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68,70])). % 68.14/68.26 cnf(5594,plain, % 68.14/68.26 (P9(f17(a3,a1),a11,a2)), % 68.14/68.26 inference(scs_inference,[],[5460,5520,5573,5575,5577,5524,5565,5581,5527,5563,5569,5571,5531,5567,59,47,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68,70,66,3177,89,208])). % 68.14/68.26 cnf(5595,plain, % 68.14/68.26 (E(f17(a11,x55951),f17(a3,x55951))), % 68.14/68.26 inference(rename_variables,[],[5524])). % 68.14/68.26 cnf(5597,plain, % 68.14/68.26 (E(f16(x55971,a11),f16(x55971,a3))), % 68.14/68.26 inference(rename_variables,[],[5531])). % 68.14/68.26 cnf(5600,plain, % 68.14/68.26 (P10(f16(a2,a3),a1,a11)), % 68.14/68.26 inference(scs_inference,[],[5460,5520,5573,5575,5577,5524,5565,5581,5595,5527,5563,5569,5571,5531,5567,5583,5597,59,47,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68,70,66,3177,89,208,3843,3908,3375])). % 68.14/68.26 cnf(5602,plain, % 68.14/68.26 (P3(f6(a12))), % 68.14/68.26 inference(scs_inference,[],[5460,5520,5573,5575,5577,5524,5565,5581,5595,5527,5563,5569,5571,5531,5567,5583,5597,59,47,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68,70,66,3177,89,208,3843,3908,3375,65])). % 68.14/68.26 cnf(5604,plain, % 68.14/68.26 (~P1(f7(a12))), % 68.14/68.26 inference(scs_inference,[],[5460,5520,5573,5575,5577,5524,5565,5581,5595,5527,5563,5569,5571,5531,5567,5583,5597,59,47,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68,70,66,3177,89,208,3843,3908,3375,65,69])). % 68.14/68.26 cnf(5612,plain, % 68.14/68.26 (E(f22(a3,x56121),f22(a11,x56121))), % 68.14/68.26 inference(scs_inference,[],[5532,5460,5461,5520,5573,5575,5577,5524,5565,5581,5595,5527,5563,5569,5571,5531,5567,5583,5597,5547,59,47,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68,70,66,3177,89,208,3843,3908,3375,65,69,75,91,90,6])). % 68.14/68.26 cnf(5613,plain, % 68.14/68.26 (P2(f23(a8),f21(f23(a5)))), % 68.14/68.26 inference(scs_inference,[],[5532,5460,5461,5520,5573,5575,5577,5524,5565,5581,5595,5527,5563,5569,5571,5531,5567,5583,5597,5547,5376,59,47,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68,70,66,3177,89,208,3843,3908,3375,65,69,75,91,90,6,77])). % 68.14/68.26 cnf(5615,plain, % 68.14/68.26 (E(f16(a3,x56151),f16(a11,x56151))), % 68.14/68.27 inference(scs_inference,[],[5532,5460,5461,5520,5573,5575,5577,5524,5565,5581,5595,5527,5563,5569,5571,5531,5567,5583,5597,5547,5376,59,47,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68,70,66,3177,89,208,3843,3908,3375,65,69,75,91,90,6,77,13])). % 68.14/68.27 cnf(5616,plain, % 68.14/68.27 (E(f22(x56161,a3),f22(x56161,a11))), % 68.14/68.27 inference(scs_inference,[],[5532,5460,5461,5520,5573,5575,5577,5524,5565,5581,5595,5527,5563,5569,5571,5531,5567,5583,5597,5547,5376,59,47,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68,70,66,3177,89,208,3843,3908,3375,65,69,75,91,90,6,77,13,7])). % 68.14/68.27 cnf(5617,plain, % 68.14/68.27 (E(f17(a3,x56171),f17(a11,x56171))), % 68.14/68.27 inference(scs_inference,[],[5532,5460,5461,5520,5573,5575,5577,5524,5565,5581,5595,5527,5563,5569,5571,5531,5567,5583,5597,5547,5376,59,47,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68,70,66,3177,89,208,3843,3908,3375,65,69,75,91,90,6,77,13,7,11])). % 68.14/68.27 cnf(5623,plain, % 68.14/68.27 (E(f16(x56231,a3),f16(x56231,a11))), % 68.14/68.27 inference(scs_inference,[],[5532,5460,5461,5520,5573,5575,5577,5524,5565,5581,5595,5527,5563,5569,5571,5531,5567,5583,5597,5547,5376,59,47,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68,70,66,3177,89,208,3843,3908,3375,65,69,75,91,90,6,77,13,7,11,80,10,4,5,14])). % 68.14/68.27 cnf(5624,plain, % 68.14/68.27 (E(f4(x56241,a3),f4(x56241,a11))), % 68.14/68.27 inference(scs_inference,[],[5532,5460,5461,5520,5573,5575,5577,5524,5565,5581,5595,5527,5563,5569,5571,5531,5567,5583,5597,5547,5376,59,47,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68,70,66,3177,89,208,3843,3908,3375,65,69,75,91,90,6,77,13,7,11,80,10,4,5,14,9])). % 68.14/68.27 cnf(5625,plain, % 68.14/68.27 (E(f4(a3,x56251),f4(a11,x56251))), % 68.14/68.27 inference(scs_inference,[],[5532,5460,5461,5520,5573,5575,5577,5524,5565,5581,5595,5527,5563,5569,5571,5531,5567,5583,5597,5547,5376,59,47,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68,70,66,3177,89,208,3843,3908,3375,65,69,75,91,90,6,77,13,7,11,80,10,4,5,14,9,8])). % 68.14/68.27 cnf(5627,plain, % 68.14/68.27 (E(f21(a3),f21(a11))), % 68.14/68.27 inference(scs_inference,[],[5532,5255,5460,5461,5520,5573,5575,5577,5524,5565,5581,5595,5527,5563,5569,5571,5531,5567,5583,5597,5547,5376,59,47,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68,70,66,3177,89,208,3843,3908,3375,65,69,75,91,90,6,77,13,7,11,80,10,4,5,14,9,8,2,17])). % 68.14/68.27 cnf(5629,plain, % 68.14/68.27 (E(f17(x56291,a3),f17(x56291,a11))), % 68.14/68.27 inference(scs_inference,[],[5532,5255,5460,5461,5520,5573,5575,5577,5524,5565,5581,5595,5527,5563,5569,5571,5531,5567,5583,5597,5547,5376,59,47,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68,70,66,3177,89,208,3843,3908,3375,65,69,75,91,90,6,77,13,7,11,80,10,4,5,14,9,8,2,17,18,12])). % 68.14/68.27 cnf(5634,plain, % 68.14/68.27 (P6(f15(f6(a12)),f6(a12))), % 68.14/68.27 inference(scs_inference,[],[5532,5255,5460,5461,5520,5573,5575,5577,5524,5565,5581,5595,5527,5563,5569,5571,5531,5567,5583,5597,5547,5234,5376,59,55,47,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68,70,66,3177,89,208,3843,3908,3375,65,69,75,91,90,6,77,13,7,11,80,10,4,5,14,9,8,2,17,18,12,15,16,79,76])). % 68.14/68.27 cnf(5635,plain, % 68.14/68.27 (P2(f15(x56351),x56351)), % 68.14/68.27 inference(rename_variables,[],[55])). % 68.14/68.27 cnf(5637,plain, % 68.14/68.27 (P2(f15(a3),a11)), % 68.14/68.27 inference(scs_inference,[],[5532,5255,5460,5461,5520,5573,5575,5577,5524,5565,5581,5595,5527,5563,5569,5571,5531,5567,5583,5597,5547,5234,5376,59,55,5635,47,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68,70,66,3177,89,208,3843,3908,3375,65,69,75,91,90,6,77,13,7,11,80,10,4,5,14,9,8,2,17,18,12,15,16,79,76,21])). % 68.14/68.27 cnf(5644,plain, % 68.14/68.27 (P9(f17(a11,a9),a3,a10)), % 68.14/68.27 inference(scs_inference,[],[5532,5255,5460,5461,5520,5573,5575,5577,5524,5565,5581,5595,5527,5563,5569,5571,5531,5567,5583,5597,5547,5234,5376,5395,5329,5367,5383,4569,59,2058,55,5635,47,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68,70,66,3177,89,208,3843,3908,3375,65,69,75,91,90,6,77,13,7,11,80,10,4,5,14,9,8,2,17,18,12,15,16,79,76,21,74,33,3,19,590])). % 68.14/68.27 cnf(5645,plain, % 68.14/68.27 (P9(f17(a9,a11),a10,a3)), % 68.14/68.27 inference(scs_inference,[],[5532,5255,5460,5461,5520,5573,5575,5577,5524,5565,5581,5595,5527,5563,5569,5571,5531,5567,5583,5597,5547,5234,5376,5395,5329,5367,5383,4569,59,2058,55,5635,47,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68,70,66,3177,89,208,3843,3908,3375,65,69,75,91,90,6,77,13,7,11,80,10,4,5,14,9,8,2,17,18,12,15,16,79,76,21,74,33,3,19,590,596])). % 68.14/68.27 cnf(5646,plain, % 68.14/68.27 (P10(f16(a9,a11),a10,a3)), % 68.14/68.27 inference(scs_inference,[],[5532,5255,5460,5461,5520,5573,5575,5577,5524,5565,5581,5595,5527,5563,5569,5571,5531,5567,5583,5597,5547,5234,5376,5395,5329,5367,5383,4569,59,2058,55,5635,47,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68,70,66,3177,89,208,3843,3908,3375,65,69,75,91,90,6,77,13,7,11,80,10,4,5,14,9,8,2,17,18,12,15,16,79,76,21,74,33,3,19,590,596,552])). % 68.14/68.27 cnf(5647,plain, % 68.14/68.27 (P10(f16(a11,a9),a3,a10)), % 68.14/68.27 inference(scs_inference,[],[5532,5255,5460,5461,5520,5573,5575,5577,5524,5565,5581,5595,5527,5563,5569,5571,5531,5567,5583,5597,5547,5234,5376,5395,5329,5367,5383,4569,59,2058,55,5635,47,3409,3189,3138,154,3928,3907,228,3402,3195,3422,197,68,70,66,3177,89,208,3843,3908,3375,65,69,75,91,90,6,77,13,7,11,80,10,4,5,14,9,8,2,17,18,12,15,16,79,76,21,74,33,3,19,590,596,552,591])). % 68.14/68.27 cnf(5653,plain, % 68.14/68.27 (E(f16(x56531,a3),f16(x56531,a11))), % 68.14/68.27 inference(rename_variables,[],[5623])). % 68.14/68.27 cnf(5655,plain, % 68.14/68.27 (E(f17(x56551,a3),f17(x56551,a11))), % 68.14/68.27 inference(rename_variables,[],[5629])). % 68.14/68.27 cnf(5656,plain, % 68.14/68.27 (~P1(f6(f6(a12)))), % 68.14/68.27 inference(scs_inference,[],[5623,5629,5584,3138,3928,68])). % 68.14/68.27 cnf(5658,plain, % 68.14/68.27 (P10(f16(a11,a1),a3,a2)), % 68.14/68.27 inference(scs_inference,[],[5615,5623,5629,5584,3138,3928,68,228])). % 68.14/68.27 cnf(5659,plain, % 68.14/68.27 (E(f16(a3,x56591),f16(a11,x56591))), % 68.14/68.27 inference(rename_variables,[],[5615])). % 68.14/68.27 cnf(5661,plain, % 68.14/68.27 (E(f17(a3,x56611),f17(a11,x56611))), % 68.14/68.27 inference(rename_variables,[],[5617])). % 68.14/68.27 cnf(5662,plain, % 68.14/68.27 (P9(f17(a1,a11),a2,a3)), % 68.14/68.27 inference(scs_inference,[],[5615,5617,5623,5629,5655,5584,3138,3928,68,228,3189,154])). % 68.14/68.27 cnf(5663,plain, % 68.14/68.27 (E(f17(x56631,a3),f17(x56631,a11))), % 68.14/68.27 inference(rename_variables,[],[5629])). % 68.14/68.27 cnf(5666,plain, % 68.14/68.27 (P9(f17(a11,a2),a3,a1)), % 68.14/68.27 inference(scs_inference,[],[5554,5615,5617,5661,5623,5629,5655,5584,3138,3928,68,228,3189,154,89,3422])). % 68.14/68.27 cnf(5667,plain, % 68.14/68.27 (E(f17(a3,x56671),f17(a11,x56671))), % 68.14/68.27 inference(rename_variables,[],[5617])). % 68.14/68.27 cnf(5672,plain, % 68.14/68.27 (P10(f16(a11,a2),a3,a1)), % 68.14/68.27 inference(scs_inference,[],[5554,5615,5659,5617,5661,5623,5629,5655,5584,5604,3138,3928,68,228,3189,154,89,3422,65,66,3402])). % 68.14/68.27 cnf(5673,plain, % 68.14/68.27 (E(f16(a3,x56731),f16(a11,x56731))), % 68.14/68.27 inference(rename_variables,[],[5615])). % 68.14/68.27 cnf(5674,plain, % 68.14/68.27 (P9(f17(a2,a11),a1,a3)), % 68.14/68.27 inference(scs_inference,[],[5554,5615,5659,5617,5661,5623,5629,5655,5663,5584,5604,3138,3928,68,228,3189,154,89,3422,65,66,3402,3409])). % 68.14/68.27 cnf(5675,plain, % 68.14/68.27 (E(f17(x56751,a3),f17(x56751,a11))), % 68.14/68.27 inference(rename_variables,[],[5629])). % 68.14/68.27 cnf(5676,plain, % 68.14/68.27 (P10(f16(a2,a11),a1,a3)), % 68.14/68.27 inference(scs_inference,[],[5554,5615,5659,5617,5661,5623,5653,5629,5655,5663,5584,5604,3138,3928,68,228,3189,154,89,3422,65,66,3402,3409,3375])). % 68.14/68.27 cnf(5677,plain, % 68.14/68.27 (E(f16(x56771,a3),f16(x56771,a11))), % 68.14/68.27 inference(rename_variables,[],[5623])). % 68.14/68.27 cnf(5679,plain, % 68.14/68.27 (E(f16(a3,x56791),f16(a11,x56791))), % 68.14/68.27 inference(rename_variables,[],[5615])). % 68.14/68.27 cnf(5681,plain, % 68.14/68.27 (E(f17(a3,x56811),f17(a11,x56811))), % 68.14/68.27 inference(rename_variables,[],[5617])). % 68.14/68.27 cnf(5686,plain, % 68.14/68.27 (~P1(f7(f6(a12)))), % 68.14/68.27 inference(scs_inference,[],[5553,5554,5615,5659,5673,5679,5617,5661,5667,5623,5653,5629,5655,5663,5584,5604,3138,3928,68,228,3189,154,89,3422,65,66,3402,3409,3375,3907,3908,91,3195,69])). % 68.14/68.27 cnf(5688,plain, % 68.14/68.27 (P10(f16(a1,a11),a2,a3)), % 68.14/68.27 inference(scs_inference,[],[5553,5554,5615,5659,5673,5679,5617,5661,5667,5623,5653,5677,5629,5655,5663,5584,5604,3138,3928,68,228,3189,154,89,3422,65,66,3402,3409,3375,3907,3908,91,3195,69,197])). % 68.14/68.27 cnf(5689,plain, % 68.14/68.27 (E(f16(x56891,a3),f16(x56891,a11))), % 68.14/68.27 inference(rename_variables,[],[5623])). % 68.14/68.27 cnf(5692,plain, % 68.14/68.27 (P9(f17(a11,a1),a3,a2)), % 68.14/68.27 inference(scs_inference,[],[5553,5554,5615,5659,5673,5679,5617,5661,5667,5681,5623,5653,5677,5629,5655,5663,5675,5584,5604,3138,3928,68,228,3189,154,89,3422,65,66,3402,3409,3375,3907,3908,91,3195,69,197,3177,208])). % 68.14/68.27 cnf(5696,plain, % 68.14/68.27 (E(f22(a2,x56961),f22(a1,x56961))), % 68.14/68.27 inference(scs_inference,[],[5553,5554,5615,5659,5673,5679,5617,5661,5667,5681,5623,5653,5677,5689,5629,5655,5663,5675,5584,5604,94,3138,3928,68,228,3189,154,89,3422,65,66,3402,3409,3375,3907,3908,91,3195,69,197,3177,208,3843,6])). % 68.14/68.27 cnf(5701,plain, % 68.14/68.27 (E(f16(a2,x57011),f16(a1,x57011))), % 68.14/68.27 inference(scs_inference,[],[5553,5554,5615,5659,5673,5679,5617,5661,5667,5681,5623,5653,5677,5689,5629,5655,5663,5675,5584,5604,5557,94,3138,3928,68,228,3189,154,89,3422,65,66,3402,3409,3375,3907,3908,91,3195,69,197,3177,208,3843,6,90,77,13])). % 68.14/68.27 cnf(5702,plain, % 68.14/68.27 (E(f17(a2,x57021),f17(a1,x57021))), % 68.14/68.27 inference(scs_inference,[],[5553,5554,5615,5659,5673,5679,5617,5661,5667,5681,5623,5653,5677,5689,5629,5655,5663,5675,5584,5604,5557,94,3138,3928,68,228,3189,154,89,3422,65,66,3402,3409,3375,3907,3908,91,3195,69,197,3177,208,3843,6,90,77,13,11])). % 68.14/68.27 cnf(5705,plain, % 68.14/68.27 (E(f22(x57051,a2),f22(x57051,a1))), % 68.14/68.27 inference(scs_inference,[],[5553,5554,5615,5659,5673,5679,5617,5661,5667,5681,5623,5653,5677,5689,5629,5655,5663,5675,5584,5604,5634,5557,94,3138,3928,68,228,3189,154,89,3422,65,66,3402,3409,3375,3907,3908,91,3195,69,197,3177,208,3843,6,90,77,13,11,80,7])). % 68.14/68.27 cnf(5707,plain, % 68.14/68.27 (E(f17(x57071,a2),f17(x57071,a1))), % 68.14/68.27 inference(scs_inference,[],[5553,5554,5615,5659,5673,5679,5617,5661,5667,5681,5623,5653,5677,5689,5629,5655,5663,5675,5584,5604,5634,5557,94,3138,3928,68,228,3189,154,89,3422,65,66,3402,3409,3375,3907,3908,91,3195,69,197,3177,208,3843,6,90,77,13,11,80,7,17,12])). % 68.14/68.27 cnf(5708,plain, % 68.14/68.27 (E(f4(a2,x57081),f4(a1,x57081))), % 68.14/68.27 inference(scs_inference,[],[5553,5554,5615,5659,5673,5679,5617,5661,5667,5681,5623,5653,5677,5689,5629,5655,5663,5675,5584,5604,5634,5557,94,3138,3928,68,228,3189,154,89,3422,65,66,3402,3409,3375,3907,3908,91,3195,69,197,3177,208,3843,6,90,77,13,11,80,7,17,12,8])). % 68.14/68.27 cnf(5709,plain, % 68.14/68.27 (E(f18(a2),f18(a1))), % 68.14/68.27 inference(scs_inference,[],[5553,5554,5615,5659,5673,5679,5617,5661,5667,5681,5623,5653,5677,5689,5629,5655,5663,5675,5584,5604,5634,5557,94,3138,3928,68,228,3189,154,89,3422,65,66,3402,3409,3375,3907,3908,91,3195,69,197,3177,208,3843,6,90,77,13,11,80,7,17,12,8,18])). % 68.14/68.27 cnf(5710,plain, % 68.14/68.27 (E(f4(x57101,a2),f4(x57101,a1))), % 68.14/68.27 inference(scs_inference,[],[5553,5554,5615,5659,5673,5679,5617,5661,5667,5681,5623,5653,5677,5689,5629,5655,5663,5675,5584,5604,5634,5557,94,3138,3928,68,228,3189,154,89,3422,65,66,3402,3409,3375,3907,3908,91,3195,69,197,3177,208,3843,6,90,77,13,11,80,7,17,12,8,18,9])). % 68.14/68.27 cnf(5711,plain, % 68.14/68.27 (E(f16(x57111,a2),f16(x57111,a1))), % 68.14/68.27 inference(scs_inference,[],[5553,5554,5615,5659,5673,5679,5617,5661,5667,5681,5623,5653,5677,5689,5629,5655,5663,5675,5584,5604,5634,5557,94,3138,3928,68,228,3189,154,89,3422,65,66,3402,3409,3375,3907,3908,91,3195,69,197,3177,208,3843,6,90,77,13,11,80,7,17,12,8,18,9,14])). % 68.14/68.27 cnf(5715,plain, % 68.14/68.27 (P4(f18(a5))), % 68.14/68.27 inference(scs_inference,[],[5256,5553,5554,5615,5659,5673,5679,5617,5661,5667,5681,5623,5653,5677,5689,5629,5655,5663,5675,5365,5584,5604,5586,5634,5557,94,47,3138,3928,68,228,3189,154,89,3422,65,66,3402,3409,3375,3907,3908,91,3195,69,197,3177,208,3843,6,90,77,13,11,80,7,17,12,8,18,9,14,2,79,74])). % 68.14/68.27 cnf(5719,plain, % 68.14/68.27 (E(f4(a10,a10),f4(a9,a9))), % 68.14/68.27 inference(scs_inference,[],[5256,5553,5554,5352,5353,5615,5659,5673,5679,5617,5661,5667,5681,5623,5653,5677,5689,5629,5655,5663,5675,5365,5584,5604,5586,5634,5557,95,94,47,3138,3928,68,228,3189,154,89,3422,65,66,3402,3409,3375,3907,3908,91,3195,69,197,3177,208,3843,6,90,77,13,11,80,7,17,12,8,18,9,14,2,79,74,33,3])). % 68.14/68.27 cnf(5754,plain, % 68.14/68.27 (E(f4(a9,a9),f4(a10,a10))), % 68.14/68.27 inference(scs_inference,[],[5555,5556,5719,5539,3318,5604,68,89,91,65,69,90,77,80,2])). % 68.14/68.27 cnf(5760,plain, % 68.14/68.27 (P3(f4(a3,a11))), % 68.14/68.27 inference(scs_inference,[],[41,5555,5556,5526,5701,5719,5537,5467,5613,5539,3318,5604,68,89,91,65,69,90,77,80,2,85,34,35,22])). % 68.14/68.27 cnf(5762,plain, % 68.14/68.27 (P12(f18(a2),f18(a1))), % 68.14/68.27 inference(scs_inference,[],[41,5555,5556,5258,5526,5701,5719,5537,5467,5613,5539,3318,5604,50,68,89,91,65,69,90,77,80,2,85,34,35,22,24])). % 68.14/68.27 cnf(5768,plain, % 68.14/68.27 (~P2(f23(a8),f21(a3))), % 68.14/68.27 inference(scs_inference,[],[41,5555,5556,5258,5526,5701,5702,5719,5537,5467,5325,5613,5539,3318,5604,43,50,68,89,91,65,69,90,77,80,2,85,34,35,22,24,79,20,82])). % 68.14/68.27 cnf(5771,plain, % 68.14/68.27 (~P2(f23(a8),f21(a11))), % 68.14/68.27 inference(scs_inference,[],[41,5555,5556,5258,5526,5533,5701,5702,5719,5537,5467,5469,5325,5613,5539,3318,5604,43,50,68,89,91,65,69,90,77,80,2,85,34,35,22,24,79,20,82,36,21])). % 68.14/68.27 cnf(5773,plain, % 68.14/68.27 (P6(f15(f7(a12)),f7(a12))), % 68.14/68.27 inference(scs_inference,[],[41,5555,5556,5258,5526,5533,5701,5702,5719,5537,5467,5469,5473,5325,5613,5539,3318,5604,43,55,50,68,89,91,65,69,90,77,80,2,85,34,35,22,24,79,20,82,36,21,31,76])). % 68.14/68.27 cnf(5792,plain, % 68.14/68.27 (P2(f18(a2),f21(f18(a1)))), % 68.14/68.27 inference(scs_inference,[],[5644,5646,5762,89,91,77])). % 68.14/68.27 cnf(5804,plain, % 68.14/68.27 (E(f4(a9,a11),f4(a10,a3))), % 68.14/68.27 inference(scs_inference,[],[5754,5644,5646,5420,5529,5369,5602,5762,5768,5303,5773,55,89,91,77,90,80,2,79,20,21,3])). % 68.14/68.27 cnf(5808,plain, % 68.14/68.27 (~P6(f22(a2,a10),f23(a5))), % 68.14/68.27 inference(scs_inference,[],[5754,5644,5646,5420,5529,5369,5602,5762,5768,5303,5773,5319,5285,146,51,43,55,47,89,91,77,90,80,2,79,20,21,3,19,92])). % 68.14/68.27 cnf(5847,plain, % 68.14/68.27 (E(f4(a3,a9),f4(a11,a10))), % 68.14/68.27 inference(scs_inference,[],[5645,5647,5760,5804,5792,5709,5427,5625,5439,565,91,89,90,77,80,2,79,20,3])). % 68.14/68.27 cnf(5859,plain, % 68.14/68.27 (~P8(a5,a2,a1)+~P1(f23(a5))), % 68.14/68.27 inference(scs_inference,[],[41,5645,5647,5760,5804,5792,5709,5427,5625,5439,5586,5715,565,5238,4574,47,91,89,90,77,80,2,79,20,3,19,83,84,39,436,432,434,71])). % 68.14/68.27 cnf(5872,plain, % 68.14/68.27 (P9(f16(a1,a10),a2,a9)), % 68.14/68.27 inference(scs_inference,[],[5493,89])). % 68.14/68.27 cnf(5880,plain, % 68.14/68.27 (E(f4(a11,a10),f4(a3,a9))), % 68.14/68.27 inference(scs_inference,[],[5491,5493,5847,105,89,91,77,90,2])). % 68.14/68.27 cnf(5881,plain, % 68.14/68.27 (P9(f17(a3,a1),a11,a1)), % 68.14/68.27 inference(scs_inference,[],[5491,5493,5580,5847,5707,105,89,91,77,90,2,29])). % 68.14/68.27 cnf(5883,plain, % 68.14/68.27 (P3(f4(a12,a12))), % 68.14/68.27 inference(scs_inference,[],[5491,5493,5580,5847,5707,45,105,89,91,77,90,2,29,79])). % 68.14/68.27 cnf(5885,plain, % 68.14/68.27 (E(f22(a11,a3),f22(a3,a11))), % 68.14/68.27 inference(scs_inference,[],[5491,5493,5580,5847,5517,5616,5707,45,105,89,91,77,90,2,29,79,3])). % 68.14/68.27 cnf(5920,plain, % 68.14/68.27 (P10(f17(a10,a1),a9,a2)), % 68.14/68.27 inference(scs_inference,[],[5495,5497,89,91,90])). % 68.14/68.27 cnf(5931,plain, % 68.14/68.27 (E(f4(a2,a3),f4(a1,a11))), % 68.14/68.27 inference(scs_inference,[],[5880,5495,5497,5883,5885,5624,5708,5278,103,132,55,89,91,90,77,2,79,33,21,3])). % 68.14/68.27 cnf(5949,plain, % 68.14/68.27 (P10(f17(a2,a3),a1,a11)), % 68.14/68.27 inference(scs_inference,[],[5562,5574,149,89,91,77,90])). % 68.14/68.27 cnf(5951,plain, % 68.14/68.27 (E(f4(a1,a11),f4(a2,a3))), % 68.14/68.27 inference(scs_inference,[],[5562,5574,5931,149,89,91,77,90,2])). % 68.14/68.27 cnf(5952,plain, % 68.14/68.27 (E(f22(a3,a2),f22(a11,a1))), % 68.14/68.27 inference(scs_inference,[],[5562,5574,5931,5612,5705,149,89,91,77,90,2,3])). % 68.14/68.27 cnf(5961,plain, % 68.14/68.27 (P9(f16(a3,a2),a11,a1)), % 68.14/68.27 inference(scs_inference,[],[5568,5576,91,89])). % 68.14/68.27 cnf(5963,plain, % 68.14/68.27 (P2(x59631,f21(x59631))), % 68.14/68.27 inference(scs_inference,[],[5568,5576,50,91,89,77])). % 68.14/68.27 cnf(5967,plain, % 68.14/68.27 (E(f22(a11,a1),f22(a3,a2))), % 68.14/68.27 inference(scs_inference,[],[5568,5576,5952,50,91,89,77,90,2])). % 68.14/68.27 cnf(5968,plain, % 68.14/68.27 (P10(f16(a2,a3),a2,a11)), % 68.14/68.27 inference(scs_inference,[],[41,5568,5576,5600,5952,50,91,89,77,90,2,35])). % 68.14/68.27 cnf(5971,plain, % 68.14/68.27 (P10(f17(a9,a1),a9,a2)), % 68.14/68.27 inference(scs_inference,[],[41,5568,5576,5600,5952,5920,5342,5365,5625,50,91,89,77,90,2,35,22,34])). % 68.14/68.27 cnf(5973,plain, % 68.14/68.27 (P12(f4(a2,a3),f4(a1,a11))), % 68.14/68.27 inference(scs_inference,[],[41,5951,5568,5576,5600,5952,5920,5342,5365,5625,50,91,89,77,90,2,35,22,34,24])). % 68.14/68.27 cnf(5975,plain, % 68.14/68.27 (~P2(f7(a12),f21(a11))), % 68.14/68.27 inference(scs_inference,[],[41,5951,5568,5576,5600,5952,5920,5342,5365,5625,5773,44,50,91,89,77,90,2,35,22,34,24,82])). % 68.14/68.27 cnf(5977,plain, % 68.14/68.27 (P9(f17(a11,a2),a3,a2)), % 68.14/68.27 inference(scs_inference,[],[41,5951,5568,5576,5600,5666,5952,5920,5342,5365,5625,5773,44,50,91,89,77,90,2,35,22,34,24,82,31])). % 68.14/68.27 cnf(5983,plain, % 68.14/68.27 (~P2(f7(a12),f21(a3))), % 68.14/68.27 inference(scs_inference,[],[41,5951,5568,5576,5600,5666,5674,5411,5952,5920,5627,5342,5365,5625,5773,44,50,91,89,77,90,2,35,22,34,24,82,31,79,20,36,30,21])). % 68.14/68.27 cnf(5986,plain, % 68.14/68.27 (E(f4(a9,a2),f4(a10,a1))), % 68.14/68.27 inference(scs_inference,[],[41,5951,5568,5576,5600,5666,5674,5411,5952,5920,5710,5627,5342,5365,5420,5625,5773,95,44,50,91,89,77,90,2,35,22,34,24,82,31,79,20,36,30,21,33,3])). % 68.14/68.27 cnf(5994,plain, % 68.14/68.27 (P9(f16(a1,a3),a2,a11)), % 68.14/68.27 inference(scs_inference,[],[5582,89])). % 68.14/68.27 cnf(6003,plain, % 68.14/68.27 (P12(f4(a2,a3),f4(a1,a3))), % 68.14/68.27 inference(scs_inference,[],[5582,5594,5973,5986,5529,89,91,77,90,2,25])). % 68.14/68.27 cnf(6005,plain, % 68.14/68.27 (~P6(f7(a12),f21(a11))), % 68.14/68.27 inference(scs_inference,[],[5963,5582,5594,5973,5986,5975,5529,89,91,77,90,2,25,85])). % 68.14/68.27 cnf(6006,plain, % 68.14/68.27 (P2(x60061,f21(x60061))), % 68.14/68.27 inference(rename_variables,[],[5963])). % 68.14/68.27 cnf(6012,plain, % 68.14/68.27 (E(f22(a2,a3),f22(a1,a11))), % 68.14/68.27 inference(scs_inference,[],[5963,6006,5582,5594,5967,5973,5986,5975,5696,5529,5616,55,89,91,77,90,2,25,85,20,21,3])). % 68.14/68.27 cnf(6020,plain, % 68.14/68.27 (P9(f16(a11,a1),a3,a2)), % 68.14/68.27 inference(scs_inference,[],[5658,5662,91,89])). % 68.14/68.27 cnf(6027,plain, % 68.14/68.27 (P2(f15(f6(a12)),a12)), % 68.14/68.27 inference(scs_inference,[],[5658,5662,5345,6003,6012,5634,91,89,77,90,2,85])). % 68.14/68.27 cnf(6031,plain, % 68.14/68.27 (E(f16(a10,a10),f16(a9,a9))), % 68.14/68.27 inference(scs_inference,[],[5658,5662,5345,6003,6012,5337,5355,5439,5634,132,91,89,77,90,2,85,33,3])). % 68.14/68.27 cnf(6040,plain, % 68.14/68.27 (P9(f16(a11,a2),a3,a1)), % 68.14/68.27 inference(scs_inference,[],[5672,89])). % 68.14/68.27 cnf(6048,plain, % 68.14/68.27 (E(f16(a9,a9),f16(a10,a10))), % 68.14/68.27 inference(scs_inference,[],[5672,5692,6031,3113,89,91,77,90,2])). % 68.14/68.27 cnf(6052,plain, % 68.14/68.27 (P9(f16(a3,a1),a11,a1)), % 68.14/68.27 inference(scs_inference,[],[5672,5692,6031,5961,5983,5711,5963,3113,89,91,77,90,2,85,29])). % 68.14/68.27 cnf(6054,plain, % 68.14/68.27 (P6(f15(f6(a12)),a12)), % 68.14/68.27 inference(scs_inference,[],[5672,5692,6031,5961,6027,5983,5711,5963,59,3113,89,91,77,90,2,85,29,76])). % 68.14/68.27 cnf(6056,plain, % 68.14/68.27 (E(f17(a1,a10),f17(a2,a9))), % 68.14/68.27 inference(scs_inference,[],[5672,5692,6031,5961,6027,5983,5356,5711,5267,5963,59,3113,89,91,77,90,2,85,29,76,3])). % 68.14/68.27 cnf(6059,plain, % 68.14/68.27 (P10(f16(a10,a10),a9,a10)), % 68.14/68.27 inference(scs_inference,[],[5672,5692,6031,5961,6027,5983,5356,5711,5267,5963,59,3113,89,91,77,90,2,85,29,76,3,591])). % 68.14/68.27 cnf(6060,plain, % 68.14/68.27 (P10(f16(a10,a10),a10,a9)), % 68.14/68.27 inference(scs_inference,[],[5672,5692,6031,5961,6027,5983,5356,5711,5267,5963,59,3113,89,91,77,90,2,85,29,76,3,591,552])). % 68.14/68.27 cnf(6067,plain, % 68.14/68.27 (P9(f16(a2,a11),a1,a3)), % 68.14/68.27 inference(scs_inference,[],[5676,5994,91,89])). % 68.14/68.27 cnf(6074,plain, % 68.14/68.27 (P2(f22(a2,a10),f23(a5))), % 68.14/68.27 inference(scs_inference,[],[5676,6056,5994,6052,5613,5446,3115,91,89,77,90,2,85])). % 68.14/68.27 cnf(6080,plain, % 68.14/68.27 (E(f16(a1,a1),f16(a2,a2))), % 68.14/68.27 inference(scs_inference,[],[5676,6048,6056,5994,6052,5269,5270,5613,5278,5446,5963,119,3115,91,89,77,90,2,85,20,33,3])). % 68.14/68.27 cnf(6083,plain, % 68.14/68.27 (P9(f17(a1,a10),a1,a9)), % 68.14/68.27 inference(scs_inference,[],[5676,6048,6056,5994,6052,5269,5270,5613,5278,5446,5963,119,3115,91,89,77,90,2,85,20,33,3,3409])). % 68.14/68.27 cnf(6089,plain, % 68.14/68.27 (P9(f16(a1,a11),a2,a3)), % 68.14/68.27 inference(scs_inference,[],[5688,6020,91,89])). % 68.14/68.27 cnf(6095,plain, % 68.14/68.27 (E(f16(a2,a2),f16(a1,a1))), % 68.14/68.27 inference(scs_inference,[],[6080,5688,6020,6083,3790,91,89,77,90,2])). % 68.14/68.27 cnf(6099,plain, % 68.14/68.27 (E(f17(a3,a1),f17(a11,a2))), % 68.14/68.27 inference(scs_inference,[],[6080,5688,6020,6083,5771,5268,5617,5963,3790,91,89,77,90,2,85,3])). % 68.14/68.27 cnf(6100,plain, % 68.14/68.27 (E(f17(x61001,a1),f17(x61001,a2))), % 68.14/68.27 inference(rename_variables,[],[5268])). % 68.14/68.27 cnf(6103,plain, % 68.14/68.27 (P10(f17(a2,a3),a2,a11)), % 68.14/68.27 inference(scs_inference,[],[41,4668,6080,5688,6020,6083,5949,5771,5268,5617,5963,3790,91,89,77,90,2,85,3,26,35])). % 68.14/68.27 cnf(6106,plain, % 68.14/68.27 (P12(f16(a2,a2),f16(a1,a1))), % 68.14/68.27 inference(scs_inference,[],[41,4668,6080,5688,5971,6020,6083,5949,5771,5268,6100,5617,5963,50,3790,91,89,77,90,2,85,3,26,35,34,24])). % 68.14/68.27 cnf(6114,plain, % 68.14/68.27 (P9(f16(a10,a10),a9,a10)), % 68.14/68.27 inference(scs_inference,[],[6059,5977,91,89])). % 68.14/68.27 cnf(6121,plain, % 68.14/68.27 (P12(f16(a2,a2),f16(a2,a1))), % 68.14/68.27 inference(scs_inference,[],[6106,6099,6059,5977,5269,91,89,77,90,2,25])). % 68.14/68.27 cnf(6123,plain, % 68.14/68.27 (P2(f15(f7(a20)),a20)), % 68.14/68.27 inference(scs_inference,[],[6106,6099,6059,5977,5250,5269,5439,91,89,77,90,2,25,85])). % 68.14/68.27 cnf(6125,plain, % 68.14/68.27 (P9(f16(a11,a2),a3,a2)), % 68.14/68.27 inference(scs_inference,[],[41,6106,6099,6059,5977,6040,5250,5269,5439,91,89,77,90,2,25,85,31])). % 68.14/68.27 cnf(6128,plain, % 68.14/68.27 (P9(f16(a2,a11),a2,a3)), % 68.14/68.27 inference(scs_inference,[],[41,6095,6106,6099,6059,5977,6040,6067,5250,5269,5439,3360,91,89,77,90,2,25,85,31,36,30])). % 68.14/68.27 cnf(6131,plain, % 68.14/68.27 (E(f22(a11,a2),f22(a3,a1))), % 68.14/68.27 inference(scs_inference,[],[41,6095,6106,6099,6059,5977,6040,6067,5250,5517,5705,5269,5439,3360,55,91,89,77,90,2,25,85,31,36,30,21,3])). % 68.14/68.27 cnf(6147,plain, % 68.14/68.27 (P9(f16(a10,a10),a10,a9)), % 68.14/68.27 inference(scs_inference,[],[6060,5881,91,89])). % 68.14/68.27 cnf(6157,plain, % 68.14/68.27 (P6(f15(f7(a20)),a20)), % 68.14/68.27 inference(scs_inference,[],[6121,6060,5881,6131,6123,5542,5963,60,91,89,77,90,2,85,76])). % 68.14/68.27 cnf(6159,plain, % 68.14/68.27 (E(f15(f21(a3)),a11)), % 68.14/68.27 inference(scs_inference,[],[6121,6060,5881,6131,6123,5542,5271,5963,60,5532,91,89,77,90,2,85,76,3])). % 68.14/68.27 cnf(6160,plain, % 68.14/68.27 (P12(a11,a3)), % 68.14/68.27 inference(scs_inference,[],[6121,6060,5881,6131,6123,5542,5271,5963,60,5532,91,89,77,90,2,85,76,3,332])). % 68.14/68.27 cnf(6168,plain, % 68.14/68.27 (P9(f17(a2,a3),a2,a11)), % 68.14/68.27 inference(scs_inference,[],[6089,6103,91,89])). % 68.14/68.27 cnf(6172,plain, % 68.14/68.27 (P2(a11,f21(a3))), % 68.14/68.27 inference(scs_inference,[],[6160,6089,6103,6125,91,89,90,77])). % 68.14/68.27 cnf(6183,plain, % 68.14/68.27 (P1(f23(a5))), % 68.14/68.27 inference(scs_inference,[],[6160,6074,6089,6103,6114,6125,6157,6159,5808,6031,5533,5613,5278,5547,136,43,91,89,90,77,2,29,85,82,21,33,76])). % 68.14/68.27 cnf(6185,plain, % 68.14/68.27 (E(f16(a3,a10),f16(a11,a9))), % 68.14/68.27 inference(scs_inference,[],[6160,6074,6089,6103,6114,6125,6157,6159,5808,6031,5533,5355,5615,5613,5278,5547,136,43,91,89,90,77,2,29,85,82,21,33,76,3])). % 68.14/68.27 cnf(6190,plain, % 68.14/68.27 (E(f23(a5),a3)), % 68.14/68.27 inference(scs_inference,[],[6160,6074,6089,6103,6114,6125,5513,6157,6159,5808,6031,5533,5355,5615,5613,5278,5547,136,43,91,89,90,77,2,29,85,82,21,33,76,3,19,5859,62])). % 68.14/68.27 cnf(6192,plain, % 68.14/68.27 (E(f17(f23(a5),x61921),f17(a3,x61921))), % 68.14/68.27 inference(scs_inference,[],[6160,6074,6089,6103,6114,6125,5513,6157,6159,5808,6031,5533,5355,5615,5613,5278,5547,136,43,91,89,90,77,2,29,85,82,21,33,76,3,19,5859,62,11])). % 68.14/68.27 cnf(6196,plain, % 68.14/68.27 (P3(f23(a5))), % 68.14/68.27 inference(scs_inference,[],[6160,6074,6089,6103,6114,6125,5513,6157,6159,5808,6031,5533,5355,5615,5613,5278,5547,136,43,91,89,90,77,2,29,85,82,21,33,76,3,19,5859,62,11,3908,7,10,63])). % 68.14/68.27 cnf(6198,plain, % 68.14/68.27 (E(f21(f23(a5)),f21(a3))), % 68.14/68.27 inference(scs_inference,[],[6160,6074,6089,6103,6114,6125,5513,6157,6159,5808,6031,5533,5355,5615,5613,5278,5547,136,43,91,89,90,77,2,29,85,82,21,33,76,3,19,5859,62,11,3908,7,10,63,17])). % 68.14/68.27 cnf(6200,plain, % 68.14/68.27 (E(f16(x62001,f23(a5)),f16(x62001,a3))), % 68.14/68.27 inference(scs_inference,[],[6160,6074,6089,6103,6114,6125,5513,6157,6159,5808,6031,5533,5355,5615,5613,5278,5547,136,43,91,89,90,77,2,29,85,82,21,33,76,3,19,5859,62,11,3908,7,10,63,17,18,14])). % 68.14/68.27 cnf(6226,plain, % 68.14/68.27 (~P8(a5,a9,a9)), % 68.14/68.27 inference(scs_inference,[],[6190,422])). % 68.14/68.27 cnf(6231,plain, % 68.14/68.27 (E(f4(f23(a5),x62311),f4(a3,x62311))), % 68.14/68.27 inference(scs_inference,[],[6190,4703,4707,15,8])). % 68.14/68.27 cnf(6232,plain, % 68.14/68.27 (E(f17(x62321,f23(a5)),f17(x62321,a3))), % 68.14/68.27 inference(scs_inference,[],[6190,4703,4707,15,8,12])). % 68.14/68.27 cnf(6235,plain, % 68.14/68.27 (E(f4(x62351,f23(a5)),f4(x62351,a3))), % 68.14/68.27 inference(scs_inference,[],[6128,6190,4703,4707,15,8,12,91,9])). % 68.14/68.27 cnf(6236,plain, % 68.14/68.27 (E(f16(f23(a5),x62361),f16(a3,x62361))), % 68.14/68.27 inference(scs_inference,[],[6128,6190,4703,4707,15,8,12,91,9,13])). % 68.14/68.27 cnf(6237,plain, % 68.14/68.27 (P9(f16(a2,a3),a2,a11)), % 68.14/68.27 inference(scs_inference,[],[6128,5968,6190,4703,4707,15,8,12,91,9,13,89])). % 68.14/68.27 cnf(6241,plain, % 68.14/68.28 (E(f17(f23(a5),x62411),f17(a3,x62411))), % 68.14/68.28 inference(rename_variables,[],[6192])). % 68.14/68.28 cnf(6242,plain, % 68.14/68.28 (P9(f17(a3,a9),f23(a5),a10)), % 68.14/68.28 inference(scs_inference,[],[6128,5968,6190,6192,6241,4703,4707,15,8,12,91,9,13,89,6,3189,590])). % 68.14/68.28 cnf(6243,plain, % 68.14/68.28 (E(f17(f23(a5),x62431),f17(a3,x62431))), % 68.14/68.28 inference(rename_variables,[],[6192])). % 68.14/68.28 cnf(6244,plain, % 68.14/68.28 (P9(f17(a9,a3),a10,f23(a5))), % 68.14/68.28 inference(scs_inference,[],[6128,5968,6190,6192,6241,4703,4707,15,8,12,91,9,13,89,6,3189,590,596])). % 68.14/68.28 cnf(6249,plain, % 68.14/68.28 (P10(f16(a3,a1),f23(a5),a2)), % 68.14/68.28 inference(scs_inference,[],[6128,5968,6190,6192,6241,3782,4703,4707,15,8,12,91,9,13,89,6,3189,590,596,90,77,228])). % 68.14/68.28 cnf(6251,plain, % 68.14/68.28 (E(f16(x62511,f23(a5)),f16(x62511,a3))), % 68.14/68.28 inference(rename_variables,[],[6200])). % 68.14/68.28 cnf(6253,plain, % 68.14/68.28 (E(f16(x62531,f23(a5)),f16(x62531,a3))), % 68.14/68.28 inference(rename_variables,[],[6200])). % 68.14/68.28 cnf(6255,plain, % 68.14/68.28 (E(f17(f23(a5),x62551),f17(a3,x62551))), % 68.14/68.28 inference(rename_variables,[],[6192])). % 68.14/68.28 cnf(6260,plain, % 68.14/68.28 (E(f16(x62601,f23(a5)),f16(x62601,a3))), % 68.14/68.28 inference(rename_variables,[],[6200])). % 68.14/68.28 cnf(6263,plain, % 68.14/68.28 (E(f16(x62631,f23(a5)),f16(x62631,a3))), % 68.14/68.28 inference(rename_variables,[],[6200])). % 68.14/68.28 cnf(6266,plain, % 68.14/68.28 (E(f16(a11,a9),f16(a3,a10))), % 68.14/68.28 inference(scs_inference,[],[6185,6128,5968,6190,6192,6241,6243,6255,6200,6251,6253,6260,6263,3782,4703,4707,15,8,12,91,9,13,89,6,3189,590,596,90,77,228,3138,3375,3422,5,208,197,16,552,3843,2])). % 68.14/68.28 cnf(6270,plain, % 68.14/68.28 (~P2(a20,f21(f23(a5)))), % 68.14/68.28 inference(scs_inference,[],[6185,6183,6128,5968,6190,6192,6241,6243,6255,6200,6251,6253,6260,6263,6157,5768,5963,3782,4703,4707,15,8,12,91,9,13,89,6,3189,590,596,90,77,228,3138,3375,3422,5,208,197,16,552,3843,2,85,82])). % 68.14/68.28 cnf(6274,plain, % 68.14/68.28 (~P6(x62741,f23(a5))), % 68.14/68.28 inference(scs_inference,[],[6185,6183,6128,5968,6190,6192,6241,6243,6255,6200,6251,6253,6260,6263,6157,5768,5963,95,3782,55,4703,4707,15,8,12,91,9,13,89,6,3189,590,596,90,77,228,3138,3375,3422,5,208,197,16,552,3843,2,85,82,21,33])). % 68.14/68.28 cnf(6277,plain, % 68.14/68.28 (E(f23(a5),a11)), % 68.14/68.28 inference(scs_inference,[],[6185,6183,6196,6128,5968,6190,6192,6241,6243,6255,6200,6251,6253,6260,6263,6157,5768,5613,5963,95,5532,3782,55,4703,4707,15,8,12,91,9,13,89,6,3189,590,596,90,77,228,3138,3375,3422,5,208,197,16,552,3843,2,85,82,21,33,78,3])). % 68.14/68.28 cnf(6280,plain, % 68.14/68.28 (P10(f16(a3,a10),a11,a10)), % 68.14/68.28 inference(scs_inference,[],[6185,6183,6196,6128,5968,6172,6190,6192,6241,6243,6255,6200,6251,6253,6260,6263,5656,6157,5983,5768,5613,5963,95,5532,3782,55,4703,4707,15,8,12,91,9,13,89,6,3189,590,596,90,77,228,3138,3375,3422,5,208,197,16,552,3843,2,85,82,21,33,78,3,19,20,591])). % 68.14/68.28 cnf(6281,plain, % 68.14/68.28 (E(f17(f23(a5),x62811),f17(a11,x62811))), % 68.14/68.28 inference(scs_inference,[],[6185,6183,6196,6128,5968,6172,6190,6192,6241,6243,6255,6200,6251,6253,6260,6263,5656,6157,5983,5768,5613,5963,95,5532,3782,55,4703,4707,15,8,12,91,9,13,89,6,3189,590,596,90,77,228,3138,3375,3422,5,208,197,16,552,3843,2,85,82,21,33,78,3,19,20,591,11])). % 68.14/68.28 cnf(6285,plain, % 68.14/68.28 (E(f21(f23(a5)),f21(a11))), % 68.14/68.28 inference(scs_inference,[],[6185,6183,6196,6128,5968,6172,6190,6192,6241,6243,6255,6200,6251,6253,6260,6263,5656,6157,5983,5768,5613,5963,95,5532,3782,55,4703,4707,15,8,12,91,9,13,89,6,3189,590,596,90,77,228,3138,3375,3422,5,208,197,16,552,3843,2,85,82,21,33,78,3,19,20,591,11,3908,7,10,17])). % 68.14/68.28 cnf(6288,plain, % 68.14/68.28 (E(f16(x62881,f23(a5)),f16(x62881,a11))), % 68.14/68.28 inference(scs_inference,[],[6185,6183,6196,6128,5968,6172,6190,6192,6241,6243,6255,6200,6251,6253,6260,6263,5656,6157,5983,5768,5613,5963,95,5532,3782,55,4703,4707,15,8,12,91,9,13,89,6,3189,590,596,90,77,228,3138,3375,3422,5,208,197,16,552,3843,2,85,82,21,33,78,3,19,20,591,11,3908,7,10,17,18,4,14])). % 68.14/68.28 cnf(6305,plain, % 68.14/68.28 (E(f17(x63051,f23(a5)),f17(x63051,a11))), % 68.14/68.28 inference(scs_inference,[],[6147,6277,6285,4643,15,8,91,12])). % 68.14/68.28 cnf(6307,plain, % 68.14/68.28 (E(f16(f23(a5),x63071),f16(a11,x63071))), % 68.14/68.28 inference(scs_inference,[],[6147,6277,6285,4643,15,8,91,12,9,13])). % 68.14/68.28 cnf(6311,plain, % 68.14/68.28 (E(f17(f23(a5),x63111),f17(a11,x63111))), % 68.14/68.28 inference(rename_variables,[],[6281])). % 68.14/68.28 cnf(6314,plain, % 68.14/68.28 (E(f17(x63141,f23(a5)),f17(x63141,a3))), % 68.14/68.28 inference(rename_variables,[],[6232])). % 68.14/68.28 cnf(6317,plain, % 68.14/68.28 (P9(f17(a9,a11),a10,f23(a5))), % 68.14/68.28 inference(scs_inference,[],[6249,6242,6147,6277,6232,6281,6285,4643,15,8,91,12,9,13,89,3189,6,3928,90,596])). % 68.14/68.28 cnf(6319,plain, % 68.14/68.28 (E(f17(f23(a5),x63191),f17(a11,x63191))), % 68.14/68.28 inference(rename_variables,[],[6281])). % 68.14/68.28 cnf(6321,plain, % 68.14/68.28 (E(f16(x63211,f23(a5)),f16(x63211,a11))), % 68.14/68.28 inference(rename_variables,[],[6288])). % 68.14/68.28 cnf(6322,plain, % 68.14/68.28 (P10(f16(a11,a1),f23(a5),a2)), % 68.14/68.28 inference(scs_inference,[],[6249,6242,6147,6277,6232,6281,6311,6288,6285,4643,15,8,91,12,9,13,89,3189,6,3928,90,596,590,3138,228])). % 68.14/68.28 cnf(6324,plain, % 68.14/68.28 (E(f16(x63241,f23(a5)),f16(x63241,a11))), % 68.14/68.28 inference(rename_variables,[],[6288])). % 68.14/68.28 cnf(6326,plain, % 68.14/68.28 (E(f17(x63261,f23(a5)),f17(x63261,a3))), % 68.14/68.28 inference(rename_variables,[],[6232])). % 68.14/68.28 cnf(6328,plain, % 68.14/68.28 (E(f17(f23(a5),x63281),f17(a11,x63281))), % 68.14/68.28 inference(rename_variables,[],[6281])). % 68.14/68.28 cnf(6330,plain, % 68.14/68.28 (E(f17(x63301,f23(a5)),f17(x63301,a3))), % 68.14/68.28 inference(rename_variables,[],[6232])). % 68.14/68.28 cnf(6335,plain, % 68.14/68.28 (E(f16(f23(a5),x63351),f16(a3,x63351))), % 68.14/68.28 inference(rename_variables,[],[6236])). % 68.14/68.28 cnf(6337,plain, % 68.14/68.28 (E(f16(f23(a5),x63371),f16(a3,x63371))), % 68.14/68.28 inference(rename_variables,[],[6236])). % 68.14/68.28 cnf(6339,plain, % 68.14/68.28 (E(f16(f23(a5),x63391),f16(a3,x63391))), % 68.14/68.28 inference(rename_variables,[],[6236])). % 68.14/68.28 cnf(6344,plain, % 68.14/68.28 (E(f16(x63441,f23(a5)),f16(x63441,a11))), % 68.14/68.28 inference(rename_variables,[],[6288])). % 68.14/68.28 cnf(6348,plain, % 68.14/68.28 (E(f16(x63481,f23(a5)),f16(x63481,a11))), % 68.14/68.28 inference(rename_variables,[],[6288])). % 68.14/68.28 cnf(6351,plain, % 68.14/68.28 (E(a11,f23(a5))), % 68.14/68.28 inference(scs_inference,[],[6249,6242,6147,6277,6232,6314,6326,6330,6236,6335,6337,6339,6281,6311,6319,6328,6288,6321,6324,6344,6348,6285,4643,15,8,91,12,9,13,89,3189,6,3928,90,596,590,3138,228,3375,154,3422,3409,5,3177,3907,591,3402,208,16,197,3195,552,3843,2])). % 68.14/68.28 cnf(6354,plain, % 68.14/68.28 (~P2(a12,f21(f23(a5)))), % 68.14/68.28 inference(scs_inference,[],[6249,6242,6147,6277,6232,6314,6326,6330,6236,6335,6337,6339,6281,6311,6319,6328,6288,6321,6324,6344,6348,6285,6054,6183,5378,5613,4643,15,8,91,12,9,13,89,3189,6,3928,90,596,590,3138,228,3375,154,3422,3409,5,3177,3907,591,3402,208,16,197,3195,552,3843,2,85,82])). % 68.14/68.28 cnf(6359,plain, % 68.14/68.28 (P2(x63591,f21(x63591))), % 68.14/68.28 inference(rename_variables,[],[5963])). % 68.14/68.28 cnf(6364,plain, % 68.14/68.28 (E(f4(f23(a5),f23(a5)),f4(a3,a3))), % 68.14/68.28 inference(scs_inference,[],[6226,6266,6249,6274,6242,6147,6277,6231,6232,6314,6326,6330,6235,6236,6335,6337,6339,6281,6311,6319,6328,6288,6321,6324,6344,6348,6285,6270,6054,6183,5446,5378,5613,5963,134,50,4643,15,8,91,12,9,13,89,3189,6,3928,90,596,590,3138,228,3375,154,3422,3409,5,3177,3907,591,3402,208,16,197,3195,552,3843,2,85,82,24,21,38,33,39,3])). % 68.14/68.28 cnf(6370,plain, % 68.14/68.28 (E(f17(a11,x63701),f17(f23(a5),x63701))), % 68.14/68.28 inference(scs_inference,[],[6226,6266,6249,6274,6242,6147,6277,6231,6232,6314,6326,6330,6235,6236,6335,6337,6339,6281,6311,6319,6328,6288,6321,6324,6344,6348,6285,5686,6270,6054,6183,5446,5378,5613,5963,6359,134,50,4643,15,8,91,12,9,13,89,3189,6,3928,90,596,590,3138,228,3375,154,3422,3409,5,3177,3907,591,3402,208,16,197,3195,552,3843,2,85,82,24,21,38,33,39,3,19,20,11])). % 68.14/68.28 cnf(6377,plain, % 68.14/68.28 (E(f16(x63771,a11),f16(x63771,f23(a5)))), % 68.14/68.28 inference(scs_inference,[],[6226,6266,6249,6274,6242,6147,6277,6231,6232,6314,6326,6330,6235,6236,6335,6337,6339,6281,6311,6319,6328,6288,6321,6324,6344,6348,6285,5686,6270,6054,6183,5446,5378,5613,5963,6359,134,50,4643,15,8,91,12,9,13,89,3189,6,3928,90,596,590,3138,228,3375,154,3422,3409,5,3177,3907,591,3402,208,16,197,3195,552,3843,2,85,82,24,21,38,33,39,3,19,20,11,7,3908,10,17,18,4,14])). % 68.14/68.28 cnf(6388,plain, % 68.14/68.28 (E(f17(x63881,a11),f17(x63881,f23(a5)))), % 68.14/68.28 inference(scs_inference,[],[6168,6351,15,8,91,12])). % 68.14/68.28 cnf(6392,plain, % 68.14/68.28 (E(f16(a11,x63921),f16(f23(a5),x63921))), % 68.14/68.28 inference(scs_inference,[],[6280,6168,6351,15,8,91,12,9,89,13])). % 68.14/68.28 cnf(6395,plain, % 68.14/68.28 (E(f17(x63951,f23(a5)),f17(x63951,a11))), % 68.14/68.28 inference(rename_variables,[],[6305])). % 68.14/68.28 cnf(6399,plain, % 68.14/68.28 (E(f17(a11,x63991),f17(f23(a5),x63991))), % 68.14/68.28 inference(rename_variables,[],[6370])). % 68.14/68.28 cnf(6403,plain, % 68.14/68.28 (E(f16(x64031,a11),f16(x64031,f23(a5)))), % 68.14/68.28 inference(rename_variables,[],[6377])). % 68.14/68.28 cnf(6405,plain, % 68.14/68.28 (E(f17(x64051,f23(a5)),f17(x64051,a11))), % 68.14/68.28 inference(rename_variables,[],[6305])). % 68.14/68.28 cnf(6407,plain, % 68.14/68.28 (E(f17(a11,x64071),f17(f23(a5),x64071))), % 68.14/68.28 inference(rename_variables,[],[6370])). % 68.14/68.28 cnf(6409,plain, % 68.14/68.28 (E(f17(x64091,f23(a5)),f17(x64091,a11))), % 68.14/68.28 inference(rename_variables,[],[6305])). % 68.14/68.28 cnf(6411,plain, % 68.14/68.28 (E(f16(f23(a5),x64111),f16(a11,x64111))), % 68.14/68.28 inference(rename_variables,[],[6307])). % 68.14/68.28 cnf(6416,plain, % 68.14/68.28 (E(f16(f23(a5),x64161),f16(a11,x64161))), % 68.14/68.28 inference(rename_variables,[],[6307])). % 68.14/68.28 cnf(6418,plain, % 68.14/68.28 (E(f16(f23(a5),x64181),f16(a11,x64181))), % 68.14/68.28 inference(rename_variables,[],[6307])). % 68.14/68.28 cnf(6422,plain, % 68.14/68.28 (E(f16(x64221,a11),f16(x64221,f23(a5)))), % 68.14/68.28 inference(rename_variables,[],[6377])). % 68.14/68.28 cnf(6437,plain, % 68.14/68.28 (E(f4(f23(a5),f23(a5)),f4(a3,a11))), % 68.14/68.28 inference(scs_inference,[],[42,6244,5637,6280,6005,6168,5872,6351,6364,6305,6395,6405,6409,6307,6411,6416,6418,6370,6399,6407,6377,6403,6422,6354,6285,5624,5773,6183,5963,15,8,91,12,9,89,13,6,3928,90,590,596,228,3375,154,3422,3409,3907,3177,5,591,3402,208,197,16,3195,552,2,85,82,31,21,33,3])). % 68.14/68.28 cnf(6454,plain, % 68.14/68.28 (E(f17(x64541,a11),f17(x64541,f23(a5)))), % 68.14/68.28 inference(rename_variables,[],[6388])). % 68.14/68.28 cnf(6458,plain, % 68.14/68.28 (E(f16(a11,x64581),f16(f23(a5),x64581))), % 68.14/68.28 inference(rename_variables,[],[6392])). % 68.14/68.28 cnf(6464,plain, % 68.14/68.28 ($false), % 68.14/68.28 inference(scs_inference,[],[6317,6322,6237,6437,6388,6454,6392,6458,6198,5768,5454,5613,91,89,90,154,3409,3402,591,2,85,21]), % 68.14/68.28 ['proof']). % 68.14/68.28 % SZS output end Proof % 68.14/68.28 % Total time :67.650000s %------------------------------------------------------------------------------