%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU219+3 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n022.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:01:50 EDT 2024 % Result : Theorem 117.10s 117.13s % Output : CNFRefutation 117.10s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SEU219+3 : TPTP v8.2.0. Released v3.2.0. % 0.10/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n022.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Fri Jun 21 14:58:39 EDT 2024 % 0.13/0.33 % CPUTime : % 0.20/0.56 start to proof:theBenchmark % 117.01/117.11 %------------------------------------------- % 117.01/117.11 % File :CSE---1.7 % 117.01/117.11 % Problem :theBenchmark % 117.01/117.11 % Transform :cnf % 117.01/117.11 % Format :tptp:raw % 117.01/117.11 % Command :java -jar mcs_scs.jar %d %s % 117.01/117.11 % 117.01/117.11 % Result :Theorem 116.480000s % 117.01/117.11 % Output :CNFRefutation 116.480000s % 117.01/117.11 %------------------------------------------- % 117.01/117.12 %------------------------------------------------------------------------------ % 117.01/117.12 % File : SEU219+3 : TPTP v8.2.0. Released v3.2.0. % 117.01/117.12 % Domain : Set theory % 117.01/117.12 % Problem : Functions and their basic properties, theorem 55 % 117.01/117.12 % Version : [Urb06] axioms : Especial. % 117.01/117.12 % English : % 117.01/117.12 % 117.01/117.12 % Refs : [Byl90] Bylinski (1990), Functions and Their Basic Properties % 117.01/117.12 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 117.01/117.12 % Source : [Urb06] % 117.01/117.12 % Names : funct_1__t55_funct_1 [Urb06] % 117.01/117.12 % 117.01/117.12 % Status : Theorem % 117.01/117.12 % Rating : 0.11 v8.1.0, 0.06 v7.5.0, 0.03 v7.1.0, 0.04 v7.0.0, 0.03 v6.4.0, 0.08 v6.1.0, 0.13 v6.0.0, 0.09 v5.5.0, 0.11 v5.4.0, 0.18 v5.3.0, 0.22 v5.2.0, 0.10 v5.1.0, 0.14 v5.0.0, 0.12 v4.1.0, 0.17 v4.0.1, 0.13 v4.0.0, 0.12 v3.7.0, 0.05 v3.4.0, 0.11 v3.3.0, 0.07 v3.2.0 % 117.01/117.12 % Syntax : Number of formulae : 40 ( 6 unt; 0 def) % 117.01/117.12 % Number of atoms : 102 ( 8 equ) % 117.01/117.12 % Maximal formula atoms : 6 ( 2 avg) % 117.01/117.12 % Number of connectives : 76 ( 14 ~; 1 |; 37 &) % 117.01/117.12 % ( 1 <=>; 23 =>; 0 <=; 0 <~>) % 117.01/117.12 % Maximal formula depth : 7 ( 4 avg) % 117.01/117.12 % Maximal term depth : 3 ( 1 avg) % 117.01/117.12 % Number of predicates : 9 ( 8 usr; 0 prp; 1-2 aty) % 117.01/117.12 % Number of functors : 6 ( 6 usr; 1 con; 0-1 aty) % 117.01/117.12 % Number of variables : 51 ( 40 !; 11 ?) % 117.01/117.12 % SPC : FOF_THM_RFO_SEQ % 117.01/117.12 % 117.01/117.12 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 117.01/117.12 % library, www.mizar.org % 117.01/117.12 %------------------------------------------------------------------------------ % 117.01/117.12 fof(antisymmetry_r2_hidden,axiom, % 117.01/117.12 ! [A,B] : % 117.01/117.12 ( in(A,B) % 117.01/117.12 => ~ in(B,A) ) ). % 117.01/117.12 % 117.01/117.12 fof(cc1_funct_1,axiom, % 117.01/117.12 ! [A] : % 117.01/117.12 ( empty(A) % 117.01/117.12 => function(A) ) ). % 117.01/117.12 % 117.01/117.12 fof(cc1_relat_1,axiom, % 117.01/117.12 ! [A] : % 117.01/117.12 ( empty(A) % 117.01/117.12 => relation(A) ) ). % 117.01/117.12 % 117.01/117.12 fof(cc2_funct_1,axiom, % 117.01/117.12 ! [A] : % 117.01/117.12 ( ( relation(A) % 117.01/117.12 & empty(A) % 117.01/117.12 & function(A) ) % 117.01/117.12 => ( relation(A) % 117.01/117.12 & function(A) % 117.01/117.12 & one_to_one(A) ) ) ). % 117.01/117.12 % 117.01/117.12 fof(d9_funct_1,axiom, % 117.01/117.12 ! [A] : % 117.01/117.12 ( ( relation(A) % 117.01/117.12 & function(A) ) % 117.10/117.12 => ( one_to_one(A) % 117.10/117.12 => function_inverse(A) = relation_inverse(A) ) ) ). % 117.10/117.12 % 117.10/117.12 fof(dt_k2_funct_1,axiom, % 117.10/117.12 ! [A] : % 117.10/117.12 ( ( relation(A) % 117.10/117.12 & function(A) ) % 117.10/117.12 => ( relation(function_inverse(A)) % 117.10/117.12 & function(function_inverse(A)) ) ) ). % 117.10/117.12 % 117.10/117.12 fof(dt_k4_relat_1,axiom, % 117.10/117.12 ! [A] : % 117.10/117.12 ( relation(A) % 117.10/117.12 => relation(relation_inverse(A)) ) ). % 117.10/117.12 % 117.10/117.12 fof(existence_m1_subset_1,axiom, % 117.10/117.12 ! [A] : % 117.10/117.12 ? [B] : element(B,A) ). % 117.10/117.12 % 117.10/117.12 fof(fc11_relat_1,axiom, % 117.10/117.12 ! [A] : % 117.10/117.12 ( empty(A) % 117.10/117.12 => ( empty(relation_inverse(A)) % 117.10/117.12 & relation(relation_inverse(A)) ) ) ). % 117.10/117.12 % 117.10/117.12 fof(fc12_relat_1,axiom, % 117.10/117.12 ( empty(empty_set) % 117.10/117.12 & relation(empty_set) % 117.10/117.12 & relation_empty_yielding(empty_set) ) ). % 117.10/117.13 % 117.10/117.13 fof(fc1_subset_1,axiom, % 117.10/117.13 ! [A] : ~ empty(powerset(A)) ). % 117.10/117.13 % 117.10/117.13 fof(fc1_xboole_0,axiom, % 117.10/117.13 empty(empty_set) ). % 117.10/117.13 % 117.10/117.13 fof(fc3_funct_1,axiom, % 117.10/117.13 ! [A] : % 117.10/117.13 ( ( relation(A) % 117.10/117.13 & function(A) % 117.10/117.13 & one_to_one(A) ) % 117.10/117.13 => ( relation(relation_inverse(A)) % 117.10/117.13 & function(relation_inverse(A)) ) ) ). % 117.10/117.13 % 117.10/117.13 fof(fc4_relat_1,axiom, % 117.10/117.13 ( empty(empty_set) % 117.10/117.13 & relation(empty_set) ) ). % 117.10/117.13 % 117.10/117.13 fof(fc5_relat_1,axiom, % 117.10/117.13 ! [A] : % 117.10/117.13 ( ( ~ empty(A) % 117.10/117.13 & relation(A) ) % 117.10/117.13 => ~ empty(relation_dom(A)) ) ). % 117.10/117.13 % 117.10/117.13 fof(fc6_relat_1,axiom, % 117.10/117.13 ! [A] : % 117.10/117.13 ( ( ~ empty(A) % 117.10/117.13 & relation(A) ) % 117.10/117.13 => ~ empty(relation_rng(A)) ) ). % 117.10/117.13 % 117.10/117.13 fof(fc7_relat_1,axiom, % 117.10/117.13 ! [A] : % 117.10/117.13 ( empty(A) % 117.10/117.13 => ( empty(relation_dom(A)) % 117.10/117.13 & relation(relation_dom(A)) ) ) ). % 117.10/117.13 % 117.10/117.13 fof(fc8_relat_1,axiom, % 117.10/117.13 ! [A] : % 117.10/117.13 ( empty(A) % 117.10/117.13 => ( empty(relation_rng(A)) % 117.10/117.13 & relation(relation_rng(A)) ) ) ). % 117.10/117.13 % 117.10/117.13 fof(involutiveness_k4_relat_1,axiom, % 117.10/117.13 ! [A] : % 117.10/117.13 ( relation(A) % 117.10/117.13 => relation_inverse(relation_inverse(A)) = A ) ). % 117.10/117.13 % 117.10/117.13 fof(rc1_funct_1,axiom, % 117.10/117.13 ? [A] : % 117.10/117.13 ( relation(A) % 117.10/117.13 & function(A) ) ). % 117.10/117.13 % 117.10/117.13 fof(rc1_relat_1,axiom, % 117.10/117.13 ? [A] : % 117.10/117.13 ( empty(A) % 117.10/117.13 & relation(A) ) ). % 117.10/117.13 % 117.10/117.13 fof(rc1_subset_1,axiom, % 117.10/117.13 ! [A] : % 117.10/117.13 ( ~ empty(A) % 117.10/117.13 => ? [B] : % 117.10/117.13 ( element(B,powerset(A)) % 117.10/117.13 & ~ empty(B) ) ) ). % 117.10/117.13 % 117.10/117.13 fof(rc1_xboole_0,axiom, % 117.10/117.13 ? [A] : empty(A) ). % 117.10/117.13 % 117.10/117.13 fof(rc2_funct_1,axiom, % 117.10/117.13 ? [A] : % 117.10/117.13 ( relation(A) % 117.10/117.13 & empty(A) % 117.10/117.13 & function(A) ) ). % 117.10/117.13 % 117.10/117.13 fof(rc2_relat_1,axiom, % 117.10/117.13 ? [A] : % 117.10/117.13 ( ~ empty(A) % 117.10/117.13 & relation(A) ) ). % 117.10/117.13 % 117.10/117.13 fof(rc2_subset_1,axiom, % 117.10/117.13 ! [A] : % 117.10/117.13 ? [B] : % 117.10/117.13 ( element(B,powerset(A)) % 117.10/117.13 & empty(B) ) ). % 117.10/117.13 % 117.10/117.13 fof(rc2_xboole_0,axiom, % 117.10/117.13 ? [A] : ~ empty(A) ). % 117.10/117.13 % 117.10/117.13 fof(rc3_funct_1,axiom, % 117.10/117.13 ? [A] : % 117.10/117.13 ( relation(A) % 117.10/117.13 & function(A) % 117.10/117.13 & one_to_one(A) ) ). % 117.10/117.13 % 117.10/117.13 fof(rc3_relat_1,axiom, % 117.10/117.13 ? [A] : % 117.10/117.13 ( relation(A) % 117.10/117.13 & relation_empty_yielding(A) ) ). % 117.10/117.13 % 117.10/117.13 fof(reflexivity_r1_tarski,axiom, % 117.10/117.13 ! [A,B] : subset(A,A) ). % 117.10/117.13 % 117.10/117.13 fof(t1_subset,axiom, % 117.10/117.13 ! [A,B] : % 117.10/117.13 ( in(A,B) % 117.10/117.13 => element(A,B) ) ). % 117.10/117.13 % 117.10/117.13 fof(t2_subset,axiom, % 117.10/117.13 ! [A,B] : % 117.10/117.13 ( element(A,B) % 117.10/117.13 => ( empty(B) % 117.10/117.13 | in(A,B) ) ) ). % 117.10/117.13 % 117.10/117.13 fof(t37_relat_1,axiom, % 117.10/117.13 ! [A] : % 117.10/117.13 ( relation(A) % 117.10/117.13 => ( relation_rng(A) = relation_dom(relation_inverse(A)) % 117.10/117.13 & relation_dom(A) = relation_rng(relation_inverse(A)) ) ) ). % 117.10/117.13 % 117.10/117.13 fof(t3_subset,axiom, % 117.10/117.13 ! [A,B] : % 117.10/117.13 ( element(A,powerset(B)) % 117.10/117.13 <=> subset(A,B) ) ). % 117.10/117.13 % 117.10/117.13 fof(t4_subset,axiom, % 117.10/117.13 ! [A,B,C] : % 117.10/117.13 ( ( in(A,B) % 117.10/117.13 & element(B,powerset(C)) ) % 117.10/117.13 => element(A,C) ) ). % 117.10/117.13 % 117.10/117.13 fof(t55_funct_1,conjecture, % 117.10/117.13 ! [A] : % 117.10/117.13 ( ( relation(A) % 117.10/117.13 & function(A) ) % 117.10/117.13 => ( one_to_one(A) % 117.10/117.13 => ( relation_rng(A) = relation_dom(function_inverse(A)) % 117.10/117.13 & relation_dom(A) = relation_rng(function_inverse(A)) ) ) ) ). % 117.10/117.13 % 117.10/117.13 fof(t5_subset,axiom, % 117.10/117.13 ! [A,B,C] : % 117.10/117.13 ~ ( in(A,B) % 117.10/117.13 & element(B,powerset(C)) % 117.10/117.13 & empty(C) ) ). % 117.10/117.13 % 117.10/117.13 fof(t6_boole,axiom, % 117.10/117.13 ! [A] : % 117.10/117.13 ( empty(A) % 117.10/117.13 => A = empty_set ) ). % 117.10/117.13 % 117.10/117.13 fof(t7_boole,axiom, % 117.10/117.13 ! [A,B] : % 117.10/117.13 ~ ( in(A,B) % 117.10/117.13 & empty(B) ) ). % 117.10/117.13 % 117.10/117.13 fof(t8_boole,axiom, % 117.10/117.13 ! [A,B] : % 117.10/117.13 ~ ( empty(A) % 117.10/117.13 & A != B % 117.10/117.13 & empty(B) ) ). % 117.10/117.13 % 117.10/117.13 %------------------------------------------------------------------------------ % 117.10/117.13 %------------------------------------------- % 117.10/117.13 % Proof found % 117.10/117.13 % SZS status Theorem for theBenchmark % 117.10/117.13 % SZS output start Proof % 117.10/117.13 %ClaNum:85(EqnAxiom:22) % 117.10/117.13 %VarNum:106(SingletonVarNum:47) % 117.10/117.13 %MaxLitNum:4 % 117.10/117.13 %MaxfuncDepth:2 % 117.10/117.13 %SharedTerms:39 % 117.10/117.13 %goalClause: 32 41 43 75 % 117.10/117.13 %singleGoalClaCount:3 % 117.10/117.13 [25]P1(a1) % 117.10/117.13 [26]P1(a2) % 117.10/117.13 [27]P1(a8) % 117.10/117.13 [28]P1(a10) % 117.10/117.13 [29]P3(a3) % 117.10/117.13 [30]P3(a10) % 117.10/117.13 [31]P3(a4) % 117.10/117.13 [32]P3(a5) % 117.10/117.13 [34]P4(a1) % 117.10/117.13 [35]P4(a3) % 117.10/117.13 [36]P4(a2) % 117.10/117.13 [37]P4(a10) % 117.10/117.13 [38]P4(a11) % 117.10/117.13 [39]P4(a4) % 117.10/117.13 [40]P4(a6) % 117.10/117.13 [41]P4(a5) % 117.10/117.13 [42]P5(a4) % 117.10/117.13 [43]P5(a5) % 117.10/117.13 [44]P7(a1) % 117.10/117.13 [45]P7(a6) % 117.10/117.13 [50]~P1(a11) % 117.10/117.13 [51]~P1(a14) % 117.10/117.13 [47]P8(x471,x471) % 117.10/117.13 [46]P1(f12(x461)) % 117.10/117.13 [48]P2(f7(x481),x481) % 117.10/117.13 [49]P2(f12(x491),f13(x491)) % 117.10/117.13 [52]~P1(f13(x521)) % 117.10/117.13 [75]~E(f18(f15(a5)),f17(a5))+~E(f18(a5),f17(f15(a5))) % 117.10/117.13 [53]~P1(x531)+E(x531,a1) % 117.10/117.13 [54]~P1(x541)+P3(x541) % 117.10/117.13 [55]~P1(x551)+P4(x551) % 117.10/117.13 [57]~P1(x571)+P1(f16(x571)) % 117.10/117.13 [58]~P1(x581)+P1(f17(x581)) % 117.10/117.13 [59]~P1(x591)+P1(f18(x591)) % 117.10/117.13 [60]~P1(x601)+P4(f16(x601)) % 117.10/117.13 [61]~P4(x611)+P4(f16(x611)) % 117.10/117.13 [62]~P1(x621)+P4(f17(x621)) % 117.10/117.13 [63]~P1(x631)+P4(f18(x631)) % 117.10/117.13 [65]P1(x651)+~P1(f9(x651)) % 117.10/117.13 [76]P1(x761)+P2(f9(x761),f13(x761)) % 117.10/117.13 [64]~P4(x641)+E(f16(f16(x641)),x641) % 117.10/117.13 [66]~P4(x661)+E(f18(f16(x661)),f17(x661)) % 117.10/117.13 [67]~P4(x671)+E(f17(f16(x671)),f18(x671)) % 117.10/117.13 [74]~P1(x741)+~P6(x742,x741) % 117.10/117.13 [79]~P6(x791,x792)+P2(x791,x792) % 117.10/117.13 [82]~P6(x822,x821)+~P6(x821,x822) % 117.10/117.13 [81]~P8(x811,x812)+P2(x811,f13(x812)) % 117.10/117.13 [83]P8(x831,x832)+~P2(x831,f13(x832)) % 117.10/117.13 [68]~P3(x681)+~P4(x681)+P3(f15(x681)) % 117.10/117.13 [69]~P3(x691)+~P4(x691)+P4(f15(x691)) % 117.10/117.13 [71]~P4(x711)+P1(x711)+~P1(f17(x711)) % 117.10/117.13 [72]~P4(x721)+P1(x721)+~P1(f18(x721)) % 117.10/117.13 [56]~P1(x562)+~P1(x561)+E(x561,x562) % 117.10/117.13 [80]~P2(x802,x801)+P1(x801)+P6(x802,x801) % 117.10/117.13 [84]~P1(x841)+~P6(x842,x843)+~P2(x843,f13(x841)) % 117.10/117.13 [85]P2(x851,x852)+~P6(x851,x853)+~P2(x853,f13(x852)) % 117.10/117.13 [70]~P1(x701)+~P3(x701)+~P4(x701)+P5(x701) % 117.10/117.13 [73]~P3(x731)+~P4(x731)+~P5(x731)+E(f16(x731),f15(x731)) % 117.10/117.13 [77]~P3(x771)+~P4(x771)+~P5(x771)+P3(f16(x771)) % 117.10/117.13 %EqnAxiom % 117.10/117.13 [1]E(x11,x11) % 117.10/117.13 [2]E(x22,x21)+~E(x21,x22) % 117.10/117.13 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 117.10/117.13 [4]~E(x41,x42)+E(f12(x41),f12(x42)) % 117.10/117.13 [5]~E(x51,x52)+E(f7(x51),f7(x52)) % 117.10/117.13 [6]~E(x61,x62)+E(f13(x61),f13(x62)) % 117.10/117.13 [7]~E(x71,x72)+E(f16(x71),f16(x72)) % 117.10/117.13 [8]~E(x81,x82)+E(f9(x81),f9(x82)) % 117.10/117.13 [9]~E(x91,x92)+E(f17(x91),f17(x92)) % 117.10/117.13 [10]~E(x101,x102)+E(f15(x101),f15(x102)) % 117.10/117.13 [11]~E(x111,x112)+E(f18(x111),f18(x112)) % 117.10/117.13 [12]~P1(x121)+P1(x122)+~E(x121,x122) % 117.10/117.13 [13]P2(x132,x133)+~E(x131,x132)+~P2(x131,x133) % 117.10/117.13 [14]P2(x143,x142)+~E(x141,x142)+~P2(x143,x141) % 117.10/117.13 [15]P6(x152,x153)+~E(x151,x152)+~P6(x151,x153) % 117.10/117.13 [16]P6(x163,x162)+~E(x161,x162)+~P6(x163,x161) % 117.10/117.13 [17]~P4(x171)+P4(x172)+~E(x171,x172) % 117.10/117.13 [18]~P3(x181)+P3(x182)+~E(x181,x182) % 117.10/117.13 [19]P8(x192,x193)+~E(x191,x192)+~P8(x191,x193) % 117.10/117.13 [20]P8(x203,x202)+~E(x201,x202)+~P8(x203,x201) % 117.10/117.14 [21]~P5(x211)+P5(x212)+~E(x211,x212) % 117.10/117.14 [22]~P7(x221)+P7(x222)+~E(x221,x222) % 117.10/117.14 % 117.10/117.14 %------------------------------------------- % 117.10/117.15 cnf(86,plain, % 117.10/117.15 (~P6(x861,a1)), % 117.10/117.15 inference(scs_inference,[],[25,74])). % 117.10/117.15 cnf(88,plain, % 117.10/117.15 (P8(f7(f13(x881)),x881)), % 117.10/117.15 inference(scs_inference,[],[25,48,74,83])). % 117.10/117.15 cnf(89,plain, % 117.10/117.15 (P2(f7(x891),x891)), % 117.10/117.15 inference(rename_variables,[],[48])). % 117.10/117.15 cnf(91,plain, % 117.10/117.15 (P6(f7(a11),a11)), % 117.10/117.15 inference(scs_inference,[],[25,48,89,50,74,83,80])). % 117.10/117.15 cnf(92,plain, % 117.10/117.15 (P2(f7(x921),x921)), % 117.10/117.15 inference(rename_variables,[],[48])). % 117.10/117.15 cnf(94,plain, % 117.10/117.15 (~E(a11,a1)), % 117.10/117.15 inference(scs_inference,[],[25,48,89,50,74,83,80,16])). % 117.10/117.15 cnf(95,plain, % 117.10/117.15 (~P6(x951,f7(f13(a1)))), % 117.10/117.15 inference(scs_inference,[],[25,48,89,92,50,74,83,80,16,84])). % 117.10/117.15 cnf(96,plain, % 117.10/117.15 (P2(f7(x961),x961)), % 117.10/117.15 inference(rename_variables,[],[48])). % 117.10/117.15 cnf(98,plain, % 117.10/117.15 (P5(a10)), % 117.10/117.15 inference(scs_inference,[],[25,28,30,37,48,89,92,50,74,83,80,16,84,70])). % 117.10/117.15 cnf(100,plain, % 117.10/117.15 (~P6(a11,f7(a11))), % 117.10/117.15 inference(scs_inference,[],[25,28,30,37,48,89,92,50,74,83,80,16,84,70,82])). % 117.10/117.15 cnf(102,plain, % 117.10/117.15 (P2(x1021,x1022)+~E(f7(x1022),x1021)), % 117.10/117.15 inference(scs_inference,[],[25,28,30,37,48,89,92,96,50,74,83,80,16,84,70,82,13])). % 117.10/117.15 cnf(108,plain, % 117.10/117.15 (~P6(x1081,a2)), % 117.10/117.15 inference(scs_inference,[],[26,74])). % 117.10/117.15 cnf(110,plain, % 117.10/117.15 (P8(f12(x1101),x1101)), % 117.10/117.15 inference(scs_inference,[],[26,49,74,83])). % 117.10/117.15 cnf(113,plain, % 117.10/117.15 (P2(f12(x1131),f13(x1131))), % 117.10/117.15 inference(rename_variables,[],[49])). % 117.10/117.15 cnf(117,plain, % 117.10/117.15 (P6(f7(a14),a14)), % 117.10/117.15 inference(scs_inference,[],[91,26,95,49,51,48,74,83,84,16,80])). % 117.10/117.15 cnf(124,plain, % 117.10/117.15 (P2(x1241,f13(x1242))+~E(f12(x1242),x1241)), % 117.10/117.15 inference(scs_inference,[],[91,26,95,49,113,51,48,74,83,84,16,80,82,85,13])). % 117.10/117.15 cnf(128,plain, % 117.10/117.15 (P8(f7(f13(x1281)),x1282)+~E(x1281,x1282)), % 117.10/117.15 inference(scs_inference,[],[91,26,88,95,49,113,51,48,74,83,84,16,80,82,85,13,19,14,15,20])). % 117.10/117.15 cnf(134,plain, % 117.10/117.15 (~P6(x1341,a8)), % 117.10/117.15 inference(scs_inference,[],[27,74])). % 117.10/117.15 cnf(136,plain, % 117.10/117.15 (P6(f7(f13(x1361)),f13(x1361))), % 117.10/117.15 inference(scs_inference,[],[27,52,48,74,80])). % 117.10/117.15 cnf(137,plain, % 117.10/117.15 (P2(f7(x1371),x1371)), % 117.10/117.15 inference(rename_variables,[],[48])). % 117.10/117.15 cnf(139,plain, % 117.10/117.15 (~P6(x1391,f7(f13(a8)))), % 117.10/117.15 inference(scs_inference,[],[27,52,48,137,74,80,84])). % 117.10/117.15 cnf(153,plain, % 117.10/117.15 (~P6(x1531,f12(x1532))), % 117.10/117.15 inference(scs_inference,[],[46,74])). % 117.10/117.15 cnf(155,plain, % 117.10/117.15 (P6(f12(x1551),f13(x1551))), % 117.10/117.15 inference(scs_inference,[],[46,49,52,74,80])). % 117.10/117.15 cnf(160,plain, % 117.10/117.15 (P8(x1601,x1602)+~E(x1602,x1601)), % 117.10/117.15 inference(scs_inference,[],[136,46,49,139,52,47,74,80,16,19])). % 117.10/117.15 cnf(161,plain, % 117.10/117.15 (P8(x1611,x1612)+~E(x1611,x1612)), % 117.10/117.15 inference(scs_inference,[],[136,46,49,139,52,47,74,80,16,19,20])). % 117.10/117.15 cnf(162,plain, % 117.10/117.15 (P2(f7(x1621),x1622)+~E(x1621,x1622)), % 117.10/117.15 inference(scs_inference,[],[136,46,49,139,52,47,48,74,80,16,19,20,14])). % 117.10/117.15 cnf(170,plain, % 117.10/117.15 (~P6(x1701,a10)), % 117.10/117.15 inference(scs_inference,[],[28,74])). % 117.10/117.15 cnf(172,plain, % 117.10/117.15 (~P6(x1721,f7(f13(a10)))), % 117.10/117.15 inference(scs_inference,[],[28,48,74,84])). % 117.10/117.15 cnf(177,plain, % 117.10/117.15 (P8(f12(x1771),x1772)+~E(x1771,x1772)), % 117.10/117.15 inference(scs_inference,[],[136,28,48,153,110,74,84,16,20])). % 117.10/117.15 cnf(191,plain, % 117.10/117.15 (P6(x1911,f13(x1912))+~E(f12(x1912),x1911)), % 117.10/117.15 inference(scs_inference,[],[117,155,86,16,15])). % 117.10/117.15 cnf(197,plain, % 117.10/117.15 (~P6(x1971,f7(f13(a2)))), % 117.10/117.15 inference(scs_inference,[],[26,48,84])). % 117.10/117.15 cnf(218,plain, % 117.10/117.15 (~E(a8,x2181)+P3(x2181)), % 117.10/117.15 inference(scs_inference,[],[27,54,18])). % 117.10/117.15 cnf(219,plain, % 117.10/117.15 (P3(a8)), % 117.10/117.15 inference(equality_inference,[],[218])). % 117.10/117.15 cnf(222,plain, % 117.10/117.15 (~P4(a8)+P5(a8)), % 117.10/117.15 inference(scs_inference,[],[219,136,27,86,16,70])). % 117.10/117.15 cnf(244,plain, % 117.10/117.15 (P5(a8)), % 117.10/117.15 inference(scs_inference,[],[27,222,55])). % 117.10/117.15 cnf(245,plain, % 117.10/117.15 (E(f16(a1),a1)), % 117.10/117.15 inference(scs_inference,[],[25,53,57])). % 117.10/117.15 cnf(246,plain, % 117.10/117.15 (E(a1,f16(a1))), % 117.10/117.15 inference(scs_inference,[],[245,2])). % 117.10/117.15 cnf(247,plain, % 117.10/117.15 (P8(f7(f13(a1)),f16(a1))), % 117.10/117.15 inference(scs_inference,[],[245,2,128])). % 117.10/117.15 cnf(250,plain, % 117.10/117.15 (P2(f7(f16(a1)),a1)), % 117.10/117.15 inference(scs_inference,[],[245,2,128,160,161,162])). % 117.10/117.15 cnf(251,plain, % 117.10/117.15 (P8(f12(f16(a1)),a1)), % 117.10/117.15 inference(scs_inference,[],[245,2,128,160,161,162,177])). % 117.10/117.15 cnf(254,plain, % 117.10/117.15 (P1(f16(a1))), % 117.10/117.15 inference(scs_inference,[],[25,94,34,245,2,128,160,161,162,177,3,17,12])). % 117.10/117.15 cnf(255,plain, % 117.10/117.15 (P7(f16(a1))), % 117.10/117.15 inference(scs_inference,[],[25,94,34,245,44,2,128,160,161,162,177,3,17,12,22])). % 117.10/117.15 cnf(256,plain, % 117.10/117.15 (~P6(x2561,f16(a1))), % 117.10/117.15 inference(scs_inference,[],[25,94,34,245,44,2,128,160,161,162,177,3,17,12,22,74])). % 117.10/117.15 cnf(258,plain, % 117.10/117.15 (~P3(f16(a1))+P3(a1)), % 117.10/117.15 inference(scs_inference,[],[25,94,34,245,44,2,128,160,161,162,177,3,17,12,22,74,18])). % 117.10/117.15 cnf(265,plain, % 117.10/117.15 (P1(f17(f18(a1)))), % 117.10/117.15 inference(scs_inference,[],[25,58,59])). % 117.10/117.15 cnf(266,plain, % 117.10/117.15 (P2(f7(a1),f16(a1))), % 117.10/117.15 inference(scs_inference,[],[246,162])). % 117.10/117.15 cnf(270,plain, % 117.10/117.15 (~E(f13(x2701),f16(a1))), % 117.10/117.15 inference(scs_inference,[],[246,136,265,256,162,177,74,16])). % 117.10/117.15 cnf(272,plain, % 117.10/117.15 (P1(f18(a1))+~P4(f18(a1))), % 117.10/117.15 inference(scs_inference,[],[246,136,265,256,162,177,74,16,71])). % 117.10/117.15 cnf(274,plain, % 117.10/117.15 (~P5(a1)+P5(f16(a1))), % 117.10/117.15 inference(scs_inference,[],[246,136,265,256,162,177,74,16,71,21])). % 117.10/117.15 cnf(298,plain, % 117.10/117.15 (~P1(f9(a11))), % 117.10/117.15 inference(scs_inference,[],[91,65,74])). % 117.10/117.15 cnf(299,plain, % 117.10/117.15 (P6(f7(f9(a11)),f9(a11))), % 117.10/117.15 inference(scs_inference,[],[298,48,80])). % 117.10/117.15 cnf(308,plain, % 117.10/117.15 (P3(a1)), % 117.10/117.15 inference(scs_inference,[],[254,258,54])). % 117.10/117.15 cnf(312,plain, % 117.10/117.15 (P5(a1)), % 117.10/117.15 inference(scs_inference,[],[308,136,25,34,108,16,70])). % 117.10/117.15 cnf(314,plain, % 117.10/117.15 (P5(f16(a1))), % 117.10/117.15 inference(scs_inference,[],[308,136,25,34,108,16,70,274])). % 117.10/117.15 cnf(318,plain, % 117.10/117.15 (~P3(f18(a1))+~P4(f18(a1))+P5(f18(a1))), % 117.10/117.15 inference(scs_inference,[],[272,70])). % 117.10/117.15 cnf(324,plain, % 117.10/117.15 (P2(f9(a11),f13(a11))), % 117.10/117.15 inference(scs_inference,[],[94,76,53])). % 117.10/117.15 cnf(325,plain, % 117.10/117.15 (P8(f9(a11),a11)), % 117.10/117.15 inference(scs_inference,[],[324,83])). % 117.10/117.15 cnf(327,plain, % 117.10/117.15 (P2(f7(f9(a11)),a11)), % 117.10/117.15 inference(scs_inference,[],[299,324,83,85])). % 117.10/117.15 cnf(334,plain, % 117.10/117.15 (~P6(f13(a11),f9(a11))), % 117.10/117.15 inference(scs_inference,[],[299,324,52,95,83,85,80,16,82])). % 117.10/117.15 cnf(345,plain, % 117.10/117.15 (P2(f7(f13(a1)),f13(f16(a1)))), % 117.10/117.15 inference(scs_inference,[],[246,81,128])). % 117.10/117.15 cnf(346,plain, % 117.10/117.15 (~P2(f13(a11),f9(a11))), % 117.10/117.15 inference(scs_inference,[],[298,334,80])). % 117.10/117.15 cnf(388,plain, % 117.10/117.15 (~E(f17(a5),f18(f15(a5)))+~E(f18(a5),f17(f15(a5)))), % 117.10/117.15 inference(scs_inference,[],[75,2])). % 117.10/117.15 cnf(390,plain, % 117.10/117.15 (~E(x3901,f18(f15(a5)))+~E(f17(a5),x3901)+~E(f18(a5),f17(f15(a5)))), % 117.10/117.15 inference(scs_inference,[],[388,3])). % 117.10/117.15 cnf(399,plain, % 117.10/117.15 (E(a5,a1)+~P1(f18(a5))), % 117.10/117.15 inference(scs_inference,[],[41,72,53])). % 117.10/117.15 cnf(400,plain, % 117.10/117.15 (E(a5,a1)+~P1(f9(f18(a5)))), % 117.10/117.15 inference(scs_inference,[],[399,65])). % 117.10/117.15 cnf(402,plain, % 117.10/117.15 (~P1(f18(a1))+~P4(f18(a1))+P5(f18(a1))), % 117.10/117.15 inference(scs_inference,[],[318,54])). % 117.10/117.15 cnf(403,plain, % 117.10/117.15 (~P4(f18(a1))+P5(f18(a1))), % 117.10/117.15 inference(scs_inference,[],[25,402,59])). % 117.10/117.15 cnf(404,plain, % 117.10/117.15 (P5(f18(a1))), % 117.10/117.15 inference(scs_inference,[],[25,403,63])). % 117.10/117.15 cnf(410,plain, % 117.10/117.15 (~E(x4101,f15(a5))+~E(f17(a5),f18(x4101))+~E(f18(a5),f17(f15(a5)))), % 117.10/117.15 inference(scs_inference,[],[390,11])). % 117.10/117.15 cnf(415,plain, % 117.10/117.15 (~E(f18(x4151),f17(a5))+~E(x4151,f15(a5))+~E(f18(a5),f17(f15(a5)))), % 117.10/117.15 inference(scs_inference,[],[410,2])). % 117.10/117.15 cnf(416,plain, % 117.10/117.15 (~E(f18(f16(a5)),f17(a5))+~E(f18(a5),f17(f15(a5)))), % 117.10/117.15 inference(scs_inference,[],[43,41,32,415,73])). % 117.10/117.15 cnf(417,plain, % 117.10/117.15 (~E(f18(a5),f17(f15(a5)))), % 117.10/117.15 inference(scs_inference,[],[41,416,66])). % 117.10/117.15 cnf(418,plain, % 117.10/117.15 (~P1(f17(f15(a5)))+~P1(f18(a5))), % 117.10/117.15 inference(scs_inference,[],[417,56])). % 117.10/117.15 cnf(420,plain, % 117.10/117.15 (~P1(f15(a5))+~P1(f18(a5))), % 117.10/117.15 inference(scs_inference,[],[417,56,58])). % 117.10/117.15 cnf(422,plain, % 117.10/117.15 (P6(f7(f15(a5)),f15(a5))+~P1(f18(a5))), % 117.10/117.15 inference(scs_inference,[],[417,265,345,48,56,58,71,85,80])). % 117.10/117.15 cnf(425,plain, % 117.10/117.15 (~E(f15(a5),f7(f13(a8)))+~P1(f18(a5))), % 117.10/117.15 inference(scs_inference,[],[139,417,324,91,265,247,345,48,325,56,58,71,85,80,20,13,15,14,19,16])). % 117.10/117.15 cnf(429,plain, % 117.10/117.15 (~P1(f18(a5))+~P1(f9(f15(a5)))), % 117.10/117.15 inference(scs_inference,[],[420,65])). % 117.10/117.15 cnf(432,plain, % 117.10/117.15 (~P6(f15(a5),f7(f15(a5)))+~P1(f18(a5))), % 117.10/117.15 inference(scs_inference,[],[422,82])). % 117.10/117.15 cnf(433,plain, % 117.10/117.15 (~E(f7(f13(a8)),f15(a5))+~P1(f18(a5))), % 117.10/117.15 inference(scs_inference,[],[425,2])). % 117.10/117.15 cnf(442,plain, % 117.10/117.15 (P6(f7(f9(a11)),a11)), % 117.10/117.15 inference(scs_inference,[],[327,50,80])). % 117.10/117.15 cnf(472,plain, % 117.10/117.15 (P3(f18(a1))+~P4(f18(a1))), % 117.10/117.15 inference(scs_inference,[],[265,54,71])). % 117.10/117.15 cnf(514,plain, % 117.10/117.15 (E(a1,f17(f18(a1)))), % 117.10/117.15 inference(scs_inference,[],[265,53,2])). % 117.10/117.15 cnf(516,plain, % 117.10/117.15 (E(f17(f18(a1)),a1)), % 117.10/117.15 inference(scs_inference,[],[514,161,2])). % 117.10/117.15 cnf(561,plain, % 117.10/117.15 (~P1(f17(a11))), % 117.10/117.15 inference(scs_inference,[],[94,38,53,71])). % 117.10/117.15 cnf(574,plain, % 117.10/117.15 (~P1(f18(a11))), % 117.10/117.15 inference(scs_inference,[],[94,38,53,72])). % 117.10/117.15 cnf(594,plain, % 117.10/117.15 (P2(a1,f13(x5941))), % 117.10/117.15 inference(scs_inference,[],[46,53,124])). % 117.10/117.15 cnf(595,plain, % 117.10/117.15 (P8(a1,x5951)), % 117.10/117.15 inference(scs_inference,[],[594,83])). % 117.10/117.15 cnf(597,plain, % 117.10/117.15 (P2(f16(a1),f13(x5971))), % 117.10/117.15 inference(scs_inference,[],[246,594,83,13])). % 117.10/117.15 cnf(614,plain, % 117.10/117.15 (P6(a1,f13(x6141))), % 117.10/117.15 inference(scs_inference,[],[46,53,191])). % 117.10/117.15 cnf(615,plain, % 117.10/117.15 (P6(f16(a1),f13(x6151))), % 117.10/117.15 inference(scs_inference,[],[246,614,15])). % 117.10/117.15 cnf(647,plain, % 117.10/117.15 (P2(f17(f18(a1)),f13(x6471))), % 117.10/117.15 inference(scs_inference,[],[514,594,13])). % 117.10/117.15 cnf(648,plain, % 117.10/117.15 (P2(f7(f16(a1)),f17(f18(a1)))), % 117.10/117.15 inference(scs_inference,[],[514,250,594,13,14])). % 117.10/117.15 cnf(651,plain, % 117.10/117.15 (P6(f17(f18(a1)),f13(x6511))), % 117.10/117.15 inference(scs_inference,[],[514,250,251,594,614,595,13,14,20,19,15])). % 117.10/117.15 cnf(654,plain, % 117.10/117.15 (~E(f17(f18(a1)),f9(a11))+~E(f7(f16(a1)),f13(a11))), % 117.10/117.15 inference(scs_inference,[],[346,648,13,14])). % 117.10/117.15 cnf(660,plain, % 117.10/117.15 (~E(f13(a11),f7(f16(a1)))+~E(f17(f18(a1)),f9(a11))), % 117.10/117.15 inference(scs_inference,[],[654,2])). % 117.10/117.15 cnf(667,plain, % 117.10/117.15 (~E(x6671,f7(f16(a1)))+~E(f13(a11),x6671)+~E(f17(f18(a1)),f9(a11))), % 117.10/117.15 inference(scs_inference,[],[660,3])). % 117.10/117.15 cnf(675,plain, % 117.10/117.15 (E(f17(f18(a1)),f16(a1))), % 117.10/117.15 inference(scs_inference,[],[265,246,53,3])). % 117.10/117.15 cnf(676,plain, % 117.10/117.15 (E(f16(a1),f17(f18(a1)))), % 117.10/117.15 inference(scs_inference,[],[675,2])). % 117.10/117.15 cnf(681,plain, % 117.10/117.15 (P1(f16(f16(a1)))), % 117.10/117.15 inference(scs_inference,[],[246,25,57,12])). % 117.10/117.15 cnf(702,plain, % 117.10/117.15 (~P4(f18(a1))+P1(f16(f18(a1)))), % 117.10/117.15 inference(scs_inference,[],[265,57,71])). % 117.10/117.15 cnf(703,plain, % 117.10/117.15 (P1(f16(f18(a1)))), % 117.10/117.15 inference(scs_inference,[],[25,702,63])). % 117.10/117.15 cnf(704,plain, % 117.10/117.15 (~P6(x7041,f16(f18(a1)))), % 117.10/117.15 inference(scs_inference,[],[703,74])). % 117.10/117.15 cnf(706,plain, % 117.10/117.15 (P1(f16(a5))+~P1(f18(a5))), % 117.10/117.15 inference(scs_inference,[],[41,57,72])). % 117.10/117.15 cnf(757,plain, % 117.10/117.15 (~E(f16(a5),x7571)+P4(x7571)), % 117.10/117.15 inference(scs_inference,[],[41,61,17])). % 117.10/117.15 cnf(758,plain, % 117.10/117.15 (P4(f16(a5))), % 117.10/117.15 inference(equality_inference,[],[757])). % 117.10/117.15 cnf(759,plain, % 117.10/117.15 (~P3(f16(a5))+P3(f15(f16(a5)))), % 117.10/117.15 inference(scs_inference,[],[41,61,68])). % 117.10/117.15 cnf(762,plain, % 117.10/117.15 (P1(f16(a5))+~P1(f17(f16(a5)))), % 117.10/117.15 inference(scs_inference,[],[41,61,71])). % 117.10/117.15 cnf(766,plain, % 117.10/117.15 (~P3(f16(a5))+P4(f15(f16(a5)))), % 117.10/117.15 inference(scs_inference,[],[41,61,69])). % 117.10/117.15 cnf(768,plain, % 117.10/117.15 (P4(f16(a8))), % 117.10/117.15 inference(scs_inference,[],[27,61,55])). % 117.10/117.15 cnf(770,plain, % 117.10/117.15 (P1(f16(a5))+~P1(f18(f16(a5)))), % 117.10/117.15 inference(scs_inference,[],[41,61,72])). % 117.10/117.15 cnf(782,plain, % 117.10/117.15 (P4(f16(f12(x7821)))), % 117.10/117.15 inference(scs_inference,[],[46,61,55])). % 117.10/117.15 cnf(791,plain, % 117.10/117.15 (P4(f17(f16(a1)))), % 117.10/117.15 inference(scs_inference,[],[246,25,62,12])). % 117.10/117.15 cnf(795,plain, % 117.10/117.15 (P4(f17(a2))), % 117.10/117.15 inference(scs_inference,[],[108,48,62,80])). % 117.10/117.15 cnf(799,plain, % 117.10/117.15 (P4(f17(a5))+~P1(f18(a5))), % 117.10/117.15 inference(scs_inference,[],[41,62,72])). % 117.10/117.15 cnf(800,plain, % 117.10/117.15 (~P1(f18(a5))+P4(f16(f17(a5)))), % 117.10/117.15 inference(scs_inference,[],[799,61])). % 117.10/117.15 cnf(806,plain, % 117.10/117.15 (P4(f17(a10))), % 117.10/117.15 inference(scs_inference,[],[170,48,62,80])). % 117.10/117.15 cnf(817,plain, % 117.10/117.15 (P1(f18(a1))), % 117.10/117.15 inference(scs_inference,[],[25,63,272])). % 117.10/117.15 cnf(819,plain, % 117.10/117.15 (~P6(x8191,f18(a1))), % 117.10/117.15 inference(scs_inference,[],[817,74])). % 117.10/117.15 cnf(828,plain, % 117.10/117.15 (P4(f18(a1))), % 117.10/117.15 inference(scs_inference,[],[817,34,63,72])). % 117.10/117.15 cnf(830,plain, % 117.10/117.15 (P3(f18(a1))), % 117.10/117.15 inference(scs_inference,[],[828,472])). % 117.10/117.15 cnf(859,plain, % 117.10/117.15 (~E(f18(a1),f9(f17(a11)))), % 117.10/117.15 inference(scs_inference,[],[561,817,65,12])). % 117.10/117.15 cnf(860,plain, % 117.10/117.15 (~P1(f9(f17(a11)))), % 117.10/117.15 inference(scs_inference,[],[817,859,56])). % 117.10/117.15 cnf(863,plain, % 117.10/117.15 (~P1(f9(f13(x8631)))), % 117.10/117.15 inference(scs_inference,[],[270,254,65,56])). % 117.10/117.15 cnf(882,plain, % 117.10/117.15 (~E(a8,a5)+P3(f16(a5))), % 117.10/117.15 inference(scs_inference,[],[41,43,218,77])). % 117.10/117.16 cnf(883,plain, % 117.10/117.16 (~E(a5,a8)+P3(f16(a5))), % 117.10/117.16 inference(scs_inference,[],[882,2])). % 117.10/117.16 cnf(884,plain, % 117.10/117.16 (~P1(a5)+P3(f16(a5))), % 117.10/117.16 inference(scs_inference,[],[27,883,56])). % 117.10/117.16 cnf(885,plain, % 117.10/117.16 (P3(f15(f16(a5)))+~P1(a5)), % 117.10/117.16 inference(scs_inference,[],[884,759])). % 117.10/117.16 cnf(888,plain, % 117.10/117.16 (E(f16(a5),f15(a5))+~E(a8,a5)), % 117.10/117.16 inference(scs_inference,[],[41,43,218,73])). % 117.10/117.16 cnf(889,plain, % 117.10/117.16 (~E(a5,a8)+E(f16(a5),f15(a5))), % 117.10/117.16 inference(scs_inference,[],[888,2])). % 117.10/117.16 cnf(890,plain, % 117.10/117.16 (~P1(a5)+E(f16(a5),f15(a5))), % 117.10/117.16 inference(scs_inference,[],[27,889,56])). % 117.10/117.16 cnf(891,plain, % 117.10/117.16 (E(f12(f16(a5)),f12(f15(a5)))+~P1(a5)), % 117.10/117.16 inference(scs_inference,[],[890,4])). % 117.10/117.16 cnf(892,plain, % 117.10/117.16 (P2(f12(f15(a5)),f13(f16(a5)))+~P1(a5)), % 117.10/117.16 inference(scs_inference,[],[49,891,13])). % 117.10/117.16 cnf(893,plain, % 117.10/117.16 (P8(f12(f15(a5)),f16(a5))+~P1(a5)), % 117.10/117.16 inference(scs_inference,[],[892,83])). % 117.10/117.16 cnf(992,plain, % 117.10/117.16 (P4(f15(f16(a5)))+~P1(a5)), % 117.10/117.16 inference(scs_inference,[],[884,766])). % 117.10/117.16 cnf(1006,plain, % 117.10/117.16 (P3(f16(a5))+~P1(f17(a5))), % 117.10/117.16 inference(scs_inference,[],[41,884,71])). % 117.10/117.16 cnf(1007,plain, % 117.10/117.16 (P3(f15(f16(a5)))+~P1(f17(a5))), % 117.10/117.16 inference(scs_inference,[],[1006,759])). % 117.10/117.16 cnf(1012,plain, % 117.10/117.16 (P3(f16(a5))+~P1(f18(a5))), % 117.10/117.16 inference(scs_inference,[],[41,884,72])). % 117.10/117.16 cnf(1013,plain, % 117.10/117.16 (P4(f15(f16(a5)))+~P1(f18(a5))), % 117.10/117.16 inference(scs_inference,[],[1012,766])). % 117.10/117.16 cnf(1015,plain, % 117.10/117.16 (P6(f7(a5),a5)+P3(f16(a5))), % 117.10/117.16 inference(scs_inference,[],[48,884,80])). % 117.10/117.16 cnf(1016,plain, % 117.10/117.16 (P3(f15(f16(a5)))+P6(f7(a5),a5)), % 117.10/117.16 inference(scs_inference,[],[1015,759])). % 117.10/117.16 cnf(1076,plain, % 117.10/117.16 (E(f12(f16(a1)),f12(a1))), % 117.10/117.16 inference(scs_inference,[],[246,2,4])). % 117.10/117.16 cnf(1077,plain, % 117.10/117.16 (P2(f12(a1),f13(f16(a1)))), % 117.10/117.16 inference(scs_inference,[],[1076,124])). % 117.10/117.16 cnf(1078,plain, % 117.10/117.16 (P6(f12(a1),f13(f16(a1)))), % 117.10/117.16 inference(scs_inference,[],[1076,124,191])). % 117.10/117.16 cnf(1081,plain, % 117.10/117.16 (E(f12(a1),f12(f16(a1)))), % 117.10/117.16 inference(scs_inference,[],[1076,124,191,161,160,2])). % 117.10/117.16 cnf(1082,plain, % 117.10/117.16 (P8(f12(f12(a1)),f12(f16(a1)))), % 117.10/117.16 inference(scs_inference,[],[1076,124,191,161,160,2,177])). % 117.10/117.16 cnf(1083,plain, % 117.10/117.16 (P2(f7(f12(a1)),f12(f16(a1)))), % 117.10/117.16 inference(scs_inference,[],[1076,124,191,161,160,2,177,162])). % 117.10/117.16 cnf(1084,plain, % 117.10/117.16 (~P3(f12(f16(a1)))+P3(f12(a1))), % 117.10/117.16 inference(scs_inference,[],[1076,124,191,161,160,2,177,162,18])). % 117.10/117.16 cnf(1090,plain, % 117.10/117.16 (P3(f12(a1))), % 117.10/117.16 inference(scs_inference,[],[46,1084,54])). % 117.10/117.16 cnf(1091,plain, % 117.10/117.16 (P6(f12(f16(a1)),f13(a1))), % 117.10/117.16 inference(scs_inference,[],[1081,191])). % 117.10/117.16 cnf(1100,plain, % 117.10/117.16 (~P4(f12(a1))+P5(f12(a1))), % 117.10/117.16 inference(scs_inference,[],[1076,1081,1090,46,1077,1082,1083,191,124,18,22,17,21,13,14,19,70])). % 117.10/117.16 cnf(1139,plain, % 117.10/117.16 (P5(f12(a1))), % 117.10/117.16 inference(scs_inference,[],[46,1100,55])). % 117.10/117.16 cnf(1146,plain, % 117.10/117.16 (E(f7(f16(a1)),f7(a1))), % 117.10/117.16 inference(scs_inference,[],[246,2,5])). % 117.10/117.16 cnf(1149,plain, % 117.10/117.16 (E(f7(a1),f7(f16(a1)))), % 117.10/117.16 inference(scs_inference,[],[1146,161,160,2])). % 117.10/117.16 cnf(1219,plain, % 117.10/117.16 (E(a5,f16(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[41,2,64])). % 117.10/117.16 cnf(1221,plain, % 117.10/117.16 (P2(f7(a5),f16(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[1219,128,162])). % 117.10/117.16 cnf(1222,plain, % 117.10/117.16 (E(f16(f16(a5)),a5)), % 117.10/117.16 inference(scs_inference,[],[1219,128,162,2])). % 117.10/117.16 cnf(1224,plain, % 117.10/117.16 (P8(f16(f16(a5)),a5)), % 117.10/117.16 inference(scs_inference,[],[1219,128,162,2,161,160])). % 117.10/117.16 cnf(1229,plain, % 117.10/117.16 (~P1(a5)+P1(f16(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[32,43,41,1219,128,162,2,161,160,177,18,17,21,12])). % 117.10/117.16 cnf(1235,plain, % 117.10/117.16 (P1(f16(f16(a5)))+~P1(f9(a5))), % 117.10/117.16 inference(scs_inference,[],[1229,65])). % 117.10/117.16 cnf(1236,plain, % 117.10/117.16 (~P1(f16(f16(a5)))+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[1222,12])). % 117.10/117.16 cnf(1248,plain, % 117.10/117.16 (E(f15(a5),f16(a5))+~P1(f16(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[1222,12,884,885,890,891,892,893,992,1229,191,162,160,2])). % 117.10/117.16 cnf(1250,plain, % 117.10/117.16 (~P6(x12501,a5)+~P1(f16(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[1222,12,884,885,890,891,892,893,992,1229,191,162,160,2,161,74])). % 117.10/117.16 cnf(1265,plain, % 117.10/117.16 (~P1(f16(a5))+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[1236,57])). % 117.10/117.16 cnf(1269,plain, % 117.10/117.16 (P1(f16(f16(a5)))+P2(f9(f9(a5)),f13(f9(a5)))), % 117.10/117.16 inference(scs_inference,[],[1235,76])). % 117.10/117.16 cnf(1271,plain, % 117.10/117.16 (~P1(f16(a5))+~P6(x12711,a5)), % 117.10/117.16 inference(scs_inference,[],[1250,57])). % 117.10/117.16 cnf(1272,plain, % 117.10/117.16 (~P6(x12721,a5)+~P1(f18(a5))), % 117.10/117.16 inference(scs_inference,[],[1271,706])). % 117.10/117.16 cnf(1273,plain, % 117.10/117.16 (P3(f15(f16(a5)))+~P1(f18(a5))), % 117.10/117.16 inference(scs_inference,[],[1272,1016])). % 117.10/117.16 cnf(1327,plain, % 117.10/117.16 (~P1(f18(a5))+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[1265,706])). % 117.10/117.16 cnf(1331,plain, % 117.10/117.16 (~P1(f17(f16(a5)))+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[1265,762])). % 117.10/117.16 cnf(1333,plain, % 117.10/117.16 (~P1(f18(f16(a5)))+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[1265,770])). % 117.10/117.16 cnf(1335,plain, % 117.10/117.16 (~E(f18(a1),f16(a5))+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[817,1265,12])). % 117.10/117.16 cnf(1336,plain, % 117.10/117.16 (~E(f16(a5),f18(a1))+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[1335,2])). % 117.10/117.16 cnf(1337,plain, % 117.10/117.16 (P1(f16(f16(a5)))+~E(f16(a5),f18(a1))), % 117.10/117.16 inference(scs_inference,[],[1219,1336,12])). % 117.10/117.16 cnf(1338,plain, % 117.10/117.16 (~E(f18(a1),f16(a5))+P1(f16(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[1337,2])). % 117.10/117.16 cnf(1339,plain, % 117.10/117.16 (P6(f7(f16(a5)),f16(a5))+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[48,1265,80])). % 117.10/117.16 cnf(1499,plain, % 117.10/117.16 (P2(f9(f18(a5)),f13(f18(a5)))+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[1327,76])). % 117.10/117.16 cnf(1500,plain, % 117.10/117.16 (P8(f9(f18(a5)),f18(a5))+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[1499,83])). % 117.10/117.16 cnf(1501,plain, % 117.10/117.16 (P8(x15011,f18(a5))+~E(f9(f18(a5)),x15011)+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[1500,19])). % 117.10/117.16 cnf(1503,plain, % 117.10/117.16 (~E(f18(a1),f18(a5))+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[817,1327,12])). % 117.10/117.16 cnf(1504,plain, % 117.10/117.16 (~E(f18(a5),f18(a1))+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[1503,2])). % 117.10/117.16 cnf(1505,plain, % 117.10/117.16 (~E(a5,a1)+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[1504,11])). % 117.10/117.16 cnf(1506,plain, % 117.10/117.16 (~E(a1,a5)+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[1505,2])). % 117.10/117.16 cnf(1507,plain, % 117.10/117.16 (~E(a1,f16(f16(a5)))+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[1222,1506,3])). % 117.10/117.16 cnf(1508,plain, % 117.10/117.16 (~E(f16(f16(a5)),a1)+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[1507,2])). % 117.10/117.16 cnf(1509,plain, % 117.10/117.16 (~E(f16(f16(a5)),f17(f18(a1)))+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[516,1508,3])). % 117.10/117.16 cnf(1510,plain, % 117.10/117.16 (~E(f17(f18(a1)),f16(f16(a5)))+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[1509,2])). % 117.10/117.16 cnf(1511,plain, % 117.10/117.16 (~E(f17(f18(a1)),a5)+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[1219,1510,3])). % 117.10/117.16 cnf(1512,plain, % 117.10/117.16 (~E(a5,f17(f18(a1)))+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[1511,2])). % 117.10/117.16 cnf(1513,plain, % 117.10/117.16 (P1(f16(f16(a5)))+~E(a5,f17(f18(a1)))), % 117.10/117.16 inference(scs_inference,[],[1219,1512,12])). % 117.10/117.16 cnf(1514,plain, % 117.10/117.16 (~E(f17(f18(a1)),a5)+P1(f16(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[1513,2])). % 117.10/117.16 cnf(1515,plain, % 117.10/117.16 (~E(f17(f18(a1)),f16(f16(a5)))+P1(f16(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[1222,1514,3])). % 117.10/117.16 cnf(1516,plain, % 117.10/117.16 (~E(f16(f16(a5)),f17(f18(a1)))+P1(f16(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[1515,2])). % 117.10/117.16 cnf(1517,plain, % 117.10/117.16 (~E(f16(f16(a5)),a1)+P1(f16(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[514,1516,3])). % 117.10/117.16 cnf(1518,plain, % 117.10/117.16 (~E(a1,f16(f16(a5)))+P1(f16(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[1517,2])). % 117.10/117.16 cnf(1519,plain, % 117.10/117.16 (~E(a1,a5)+P1(f16(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[1219,1518,3])). % 117.10/117.16 cnf(1520,plain, % 117.10/117.16 (~E(a5,a1)+P1(f16(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[1519,2])). % 117.10/117.16 cnf(1521,plain, % 117.10/117.16 (P1(f16(f16(a5)))+~P1(f18(a5))), % 117.10/117.16 inference(scs_inference,[],[1520,399])). % 117.10/117.16 cnf(1524,plain, % 117.10/117.16 (P6(f7(f18(a5)),f18(a5))+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[48,1327,80])). % 117.10/117.16 cnf(1525,plain, % 117.10/117.16 (~P6(f18(a5),f7(f18(a5)))+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[1524,82])). % 117.10/117.16 cnf(1526,plain, % 117.10/117.16 (~P6(x15261,f7(f18(a5)))+~E(x15261,f18(a5))+P1(a5)), % 117.10/117.16 inference(scs_inference,[],[1525,15])). % 117.10/117.16 cnf(1529,plain, % 117.10/117.16 (E(f17(a5),f18(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[41,2,66])). % 117.10/117.16 cnf(1530,plain, % 117.10/117.16 (P2(f7(f17(a5)),f18(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[1529,162])). % 117.10/117.16 cnf(1532,plain, % 117.10/117.16 (E(f18(f16(a5)),f17(a5))), % 117.10/117.16 inference(scs_inference,[],[1529,162,160,2])). % 117.10/117.16 cnf(1535,plain, % 117.10/117.16 (~P1(f17(a5))+P1(f18(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[1529,162,160,2,161,177,12])). % 117.10/117.16 cnf(1536,plain, % 117.10/117.16 (~P6(x15361,f18(f16(a5)))+~P1(f17(a5))), % 117.10/117.16 inference(scs_inference,[],[1529,162,160,2,161,177,12,74])). % 117.10/117.16 cnf(1538,plain, % 117.10/117.16 (P1(f16(a5))+~P1(f17(a5))), % 117.10/117.16 inference(scs_inference,[],[1529,758,162,160,2,161,177,12,74,72])). % 117.10/117.16 cnf(1545,plain, % 117.10/117.16 (~P1(f18(f16(a5)))+P1(f17(a5))), % 117.10/117.16 inference(scs_inference,[],[1532,12])). % 117.10/117.16 cnf(1547,plain, % 117.10/117.16 (~P1(f18(f16(a5)))+P1(f18(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[1532,12,1007,1535])). % 117.10/117.16 cnf(1548,plain, % 117.10/117.16 (~P6(x15481,f17(a5))+~P1(f18(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[1532,12,1007,1535,74])). % 117.10/117.16 cnf(1566,plain, % 117.10/117.16 (~P1(f18(f16(a5)))+P3(f17(a5))), % 117.10/117.16 inference(scs_inference,[],[1532,18,54])). % 117.10/117.16 cnf(1601,plain, % 117.10/117.16 (~P1(f16(a5))+P3(f17(a5))), % 117.10/117.16 inference(scs_inference,[],[1566,59])). % 117.10/117.16 cnf(1602,plain, % 117.10/117.16 (~P1(a5)+P3(f17(a5))), % 117.10/117.16 inference(scs_inference,[],[1601,57])). % 117.10/117.16 cnf(1776,plain, % 117.10/117.16 (P6(f7(a5),a5)+P3(f17(a5))), % 117.10/117.16 inference(scs_inference,[],[48,1602,80])). % 117.10/117.16 cnf(1777,plain, % 117.10/117.16 (~P6(a5,f7(a5))+P3(f17(a5))), % 117.10/117.16 inference(scs_inference,[],[1776,82])). % 117.10/117.16 cnf(1778,plain, % 117.10/117.16 (~P6(f16(f16(a5)),f7(a5))+P3(f17(a5))), % 117.10/117.16 inference(scs_inference,[],[1222,1777,15])). % 117.10/117.16 cnf(1779,plain, % 117.10/117.16 (~P6(f16(f16(a5)),x17791)+~E(x17791,f7(a5))+P3(f17(a5))), % 117.10/117.16 inference(scs_inference,[],[1778,16])). % 117.10/117.16 cnf(1782,plain, % 117.10/117.16 (E(f18(a5),f17(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[41,2,67])). % 117.10/117.16 cnf(1784,plain, % 117.10/117.16 (P2(f7(f18(a5)),f17(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[1782,160,162])). % 117.10/117.16 cnf(1786,plain, % 117.10/117.16 (E(f17(f16(a5)),f18(a5))), % 117.10/117.16 inference(scs_inference,[],[1782,160,162,161,2])). % 117.10/117.16 cnf(1788,plain, % 117.10/117.16 (~P1(f18(a5))+P1(f17(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[1782,160,162,161,2,177,12])). % 117.10/117.16 cnf(1789,plain, % 117.10/117.16 (~P6(x17891,f17(f16(a5)))+~P1(f18(a5))), % 117.10/117.16 inference(scs_inference,[],[1782,160,162,161,2,177,12,74])). % 117.10/117.16 cnf(1793,plain, % 117.10/117.16 (~P1(a5)+P1(f17(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[1788,59])). % 117.10/117.16 cnf(1794,plain, % 117.10/117.16 (~P1(f17(f16(a5)))+P1(f18(a5))), % 117.10/117.16 inference(scs_inference,[],[1786,12])). % 117.10/117.16 cnf(1804,plain, % 117.10/117.16 (~P1(f17(f16(a5)))+P1(f16(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[1786,12,418,422,425,429,432,433,800,1013,1273,1521])). % 117.10/117.16 cnf(1896,plain, % 117.10/117.16 (P1(f17(f16(a5)))+~P1(f9(a5))), % 117.10/117.16 inference(scs_inference,[],[1793,65])). % 117.10/117.16 cnf(1899,plain, % 117.10/117.16 (~P1(f16(a5))+P1(f18(a5))), % 117.10/117.16 inference(scs_inference,[],[1794,58])). % 117.10/117.16 cnf(1900,plain, % 117.10/117.16 (P1(f18(a5))+~P1(f18(a5))), % 117.10/117.16 inference(scs_inference,[],[1899,706])). % 117.10/117.16 cnf(2222,plain, % 117.10/117.16 (~E(f17(f15(a5)),f17(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[417,1786,2,3])). % 117.10/117.16 cnf(2223,plain, % 117.10/117.16 (~E(f15(a5),f16(a5))), % 117.10/117.16 inference(scs_inference,[],[2222,9])). % 117.10/117.16 cnf(2225,plain, % 117.10/117.16 (~P1(f16(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[1782,2222,9,3,1248])). % 117.10/117.16 cnf(2228,plain, % 117.10/117.16 (~E(a5,f17(f18(a1)))), % 117.10/117.16 inference(scs_inference,[],[1782,2222,9,3,1248,1337,1338,1513])). % 117.10/117.16 cnf(2229,plain, % 117.10/117.16 (~E(f17(f18(a1)),a5)), % 117.10/117.16 inference(scs_inference,[],[1782,2222,9,3,1248,1337,1338,1513,1514])). % 117.10/117.16 cnf(2231,plain, % 117.10/117.16 (~E(f16(f16(a5)),f17(f18(a1)))), % 117.10/117.16 inference(scs_inference,[],[1782,2222,9,3,1248,1337,1338,1513,1514,1515,1516])). % 117.10/117.16 cnf(2235,plain, % 117.10/117.16 (~E(a5,a1)), % 117.10/117.16 inference(scs_inference,[],[1782,2222,9,3,1248,1337,1338,1513,1514,1515,1516,1517,1518,1519,1520])). % 117.10/117.16 cnf(2236,plain, % 117.10/117.16 (~P1(f16(a5))), % 117.10/117.16 inference(scs_inference,[],[1782,2222,9,3,1248,1337,1338,1513,1514,1515,1516,1517,1518,1519,1520,57])). % 117.10/117.16 cnf(2239,plain, % 117.10/117.16 (~P1(a5)), % 117.10/117.16 inference(scs_inference,[],[1782,2222,9,3,1248,1337,1338,1513,1514,1515,1516,1517,1518,1519,1520,57,400,53])). % 117.10/117.16 cnf(2247,plain, % 117.10/117.16 (P6(f7(a5),f16(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[1782,1786,2222,1221,9,3,1248,1337,1338,1513,1514,1515,1516,1517,1518,1519,1520,57,400,53,1269,83,1501,1526,80])). % 117.10/117.16 cnf(2274,plain, % 117.10/117.16 (~P1(f18(a5))), % 117.10/117.16 inference(scs_inference,[],[2235,399])). % 117.10/117.16 cnf(2278,plain, % 117.10/117.16 (~P1(f17(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[2236,762])). % 117.10/117.16 cnf(2279,plain, % 117.10/117.16 (~P1(f18(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[2236,770])). % 117.10/117.16 cnf(2281,plain, % 117.10/117.16 (~P1(f9(a5))), % 117.10/117.16 inference(scs_inference,[],[2225,1235])). % 117.10/117.16 cnf(2289,plain, % 117.10/117.16 (~P1(f17(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[2239,1331])). % 117.10/117.16 cnf(2291,plain, % 117.10/117.16 (~P1(f18(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[2239,1333])). % 117.10/117.16 cnf(2293,plain, % 117.10/117.16 (P6(f7(f16(a5)),f16(a5))), % 117.10/117.16 inference(scs_inference,[],[2239,1339])). % 117.10/117.16 cnf(2299,plain, % 117.10/117.16 (~P1(f18(a5))), % 117.10/117.16 inference(scs_inference,[],[2225,1521])). % 117.10/117.16 cnf(2301,plain, % 117.10/117.16 (P6(f7(f18(a5)),f18(a5))), % 117.10/117.16 inference(scs_inference,[],[2239,1524])). % 117.10/117.16 cnf(2304,plain, % 117.10/117.16 (~P1(f17(a5))), % 117.10/117.16 inference(scs_inference,[],[2236,1538])). % 117.10/117.16 cnf(2305,plain, % 117.10/117.16 (~P1(f17(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[2225,1804])). % 117.10/117.16 cnf(2310,plain, % 117.10/117.16 (~P1(f17(a5))), % 117.10/117.16 inference(scs_inference,[],[2279,1535])). % 117.10/117.16 cnf(2311,plain, % 117.10/117.16 (~P1(f18(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[2304,1545])). % 117.10/117.16 cnf(2312,plain, % 117.10/117.16 (~P1(f18(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[2279,1547])). % 117.10/117.16 cnf(2316,plain, % 117.10/117.16 (~P1(f18(a5))), % 117.10/117.16 inference(scs_inference,[],[2278,1788])). % 117.10/117.16 cnf(2317,plain, % 117.10/117.16 (~P1(f17(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[2274,1794])). % 117.10/117.16 cnf(2320,plain, % 117.10/117.16 (~P1(f9(a5))), % 117.10/117.16 inference(scs_inference,[],[2278,1896])). % 117.10/117.16 cnf(2321,plain, % 117.10/117.16 (~P1(f18(a5))), % 117.10/117.16 inference(scs_inference,[],[2274,1900])). % 117.10/117.16 cnf(2325,plain, % 117.10/117.16 (P6(f7(f18(a5)),f17(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[676,2231,2278,1784,2247,82,3,80])). % 117.10/117.16 cnf(2327,plain, % 117.10/117.16 (~E(f16(a5),f16(f18(a1)))), % 117.10/117.16 inference(scs_inference,[],[676,2231,2278,1784,2293,2247,704,82,3,80,16])). % 117.10/117.16 cnf(2336,plain, % 117.10/117.16 (~P1(f18(a5))), % 117.10/117.16 inference(scs_inference,[],[2325,1789])). % 117.10/117.16 cnf(2339,plain, % 117.10/117.16 (P6(f7(f17(a5)),f18(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[676,2279,2228,1530,2327,7,3,80])). % 117.10/117.16 cnf(2351,plain, % 117.10/117.16 (~P1(f17(a5))), % 117.10/117.16 inference(scs_inference,[],[2339,1536])). % 117.10/117.16 cnf(2352,plain, % 117.10/117.16 (P6(f7(f17(a5)),f17(a5))), % 117.10/117.16 inference(scs_inference,[],[2304,48,80])). % 117.10/117.16 cnf(2365,plain, % 117.10/117.16 (~P1(f18(f16(a5)))), % 117.10/117.16 inference(scs_inference,[],[2352,1548])). % 117.10/117.16 cnf(2366,plain, % 117.10/117.16 (P6(f7(f9(a5)),f9(a5))), % 117.10/117.16 inference(scs_inference,[],[2281,48,80])). % 117.10/117.16 cnf(2371,plain, % 117.10/117.16 (~P6(f9(a5),f7(f9(a5)))), % 117.10/117.16 inference(scs_inference,[],[2325,2281,48,86,80,16,82])). % 117.10/117.16 cnf(2387,plain, % 117.10/117.16 (P6(f7(a5),a5)), % 117.10/117.16 inference(scs_inference,[],[48,2239,80])). % 117.10/117.16 cnf(2400,plain, % 117.10/117.16 (~P1(f18(a5))), % 117.10/117.16 inference(scs_inference,[],[2387,1272])). % 117.10/117.16 cnf(2418,plain, % 117.10/117.16 (~E(f9(a5),f12(x24181))), % 117.10/117.16 inference(scs_inference,[],[2366,153,16])). % 117.10/117.16 cnf(2462,plain, % 117.10/117.16 (P6(x24621,f16(f16(a5)))+~E(f7(a5),x24621)), % 117.10/117.16 inference(scs_inference,[],[2366,2247,704,16,15])). % 117.10/117.16 cnf(2468,plain, % 117.10/117.16 (~E(f9(a5),f16(a1))), % 117.10/117.16 inference(scs_inference,[],[2366,256,16])). % 117.10/117.16 cnf(2470,plain, % 117.10/117.16 (~E(f9(a5),f18(a1))), % 117.10/117.16 inference(scs_inference,[],[2366,819,16])). % 117.10/117.16 cnf(2474,plain, % 117.10/117.16 (~E(f9(a5),a2)), % 117.10/117.16 inference(scs_inference,[],[2366,108,16])). % 117.10/117.16 cnf(2476,plain, % 117.10/117.16 (~E(a5,a8)), % 117.10/117.16 inference(scs_inference,[],[2387,134,16])). % 117.10/117.16 cnf(2478,plain, % 117.10/117.16 (~E(a5,a10)), % 117.10/117.16 inference(scs_inference,[],[2387,170,16])). % 117.10/117.16 cnf(2480,plain, % 117.10/117.16 (~E(a5,f12(x24801))), % 117.10/117.16 inference(scs_inference,[],[2387,153,16])). % 117.10/117.16 cnf(2494,plain, % 117.10/117.16 (~E(f17(a5),f16(a1))), % 117.10/117.16 inference(scs_inference,[],[2352,256,16])). % 117.10/117.16 cnf(2501,plain, % 117.10/117.16 (~E(a5,a2)), % 117.10/117.16 inference(scs_inference,[],[2387,108,16])). % 117.10/117.16 cnf(2505,plain, % 117.10/117.16 (~E(f16(a5),a10)), % 117.10/117.16 inference(scs_inference,[],[2293,170,16])). % 117.10/117.16 cnf(2507,plain, % 117.10/117.16 (~E(f16(f16(a5)),f12(x25071))), % 117.10/117.16 inference(scs_inference,[],[2247,153,16])). % 117.10/117.16 cnf(2523,plain, % 117.10/117.16 (~E(f17(f16(a5)),f16(a1))), % 117.10/117.16 inference(scs_inference,[],[2325,256,16])). % 117.10/117.16 cnf(2525,plain, % 117.10/117.16 (~E(f17(a5),f18(a1))), % 117.10/117.16 inference(scs_inference,[],[2352,819,16])). % 117.10/117.16 cnf(2530,plain, % 117.10/117.16 (~E(f18(a5),a2)), % 117.10/117.16 inference(scs_inference,[],[2301,108,16])). % 117.10/117.16 cnf(2532,plain, % 117.10/117.16 (~E(f16(a5),a8)), % 117.10/117.16 inference(scs_inference,[],[2293,134,16])). % 117.10/117.16 cnf(2536,plain, % 117.10/117.16 (~E(f18(a5),f12(x25361))), % 117.10/117.16 inference(scs_inference,[],[2301,153,16])). % 117.10/117.16 cnf(2553,plain, % 117.10/117.16 (~E(f18(f16(a5)),f16(a1))), % 117.10/117.16 inference(scs_inference,[],[2339,256,16])). % 117.10/117.16 cnf(2555,plain, % 117.10/117.16 (~E(f16(f16(a5)),f18(a1))), % 117.10/117.16 inference(scs_inference,[],[2247,819,16])). % 117.10/117.16 cnf(2559,plain, % 117.10/117.16 (~E(f16(a5),a2)), % 117.10/117.16 inference(scs_inference,[],[2293,108,16])). % 117.10/117.16 cnf(2564,plain, % 117.10/117.16 (~E(f18(a5),a10)), % 117.10/117.16 inference(scs_inference,[],[2301,170,16])). % 117.10/117.16 cnf(2566,plain, % 117.10/117.16 (~E(f16(a5),f12(x25661))), % 117.10/117.16 inference(scs_inference,[],[2293,153,16])). % 117.10/117.16 cnf(2732,plain, % 117.10/117.16 (P4(f16(a2))), % 117.10/117.16 inference(scs_inference,[],[26,60])). % 117.10/117.16 cnf(2736,plain, % 117.10/117.16 (~P1(f9(f9(a5)))), % 117.10/117.16 inference(scs_inference,[],[768,2320,26,60,61,65])). % 117.10/117.16 cnf(2740,plain, % 117.10/117.16 (P2(f9(a5),f13(a5))), % 117.10/117.16 inference(scs_inference,[],[768,2320,37,2239,26,60,61,65,64,76])). % 117.10/117.16 cnf(2742,plain, % 117.10/117.16 (E(f15(f16(a1)),f15(a1))), % 117.10/117.16 inference(scs_inference,[],[768,2320,37,2239,26,245,60,61,65,64,76,10])). % 117.10/117.16 cnf(2747,plain, % 117.10/117.16 (E(f18(f16(a1)),f18(a1))), % 117.10/117.16 inference(scs_inference,[],[768,2320,37,2239,26,245,60,61,65,64,76,10,66,67,11])). % 117.10/117.16 cnf(2748,plain, % 117.10/117.16 (P1(f18(a2))), % 117.10/117.16 inference(scs_inference,[],[768,2320,37,2239,26,245,60,61,65,64,76,10,66,67,11,59])). % 117.10/117.16 cnf(2750,plain, % 117.10/117.16 (P1(f16(a2))), % 117.10/117.16 inference(scs_inference,[],[768,2320,37,2239,26,245,60,61,65,64,76,10,66,67,11,59,57])). % 117.10/117.16 cnf(2752,plain, % 117.10/117.16 (P2(f16(f16(a5)),f13(a5))), % 117.10/117.16 inference(scs_inference,[],[768,2320,1224,37,2239,26,245,60,61,65,64,76,10,66,67,11,59,57,81])). % 117.10/117.16 cnf(2756,plain, % 117.10/117.16 (P1(f17(a2))), % 117.10/117.16 inference(scs_inference,[],[768,2320,1224,37,2239,681,26,245,60,61,65,64,76,10,66,67,11,59,57,81,53,58])). % 117.10/117.16 cnf(2758,plain, % 117.10/117.16 (P4(f17(a8))), % 117.10/117.16 inference(scs_inference,[],[768,2320,1224,37,2239,681,26,27,245,60,61,65,64,76,10,66,67,11,59,57,81,53,58,62])). % 117.10/117.16 cnf(2760,plain, % 117.10/117.16 (P4(f18(a2))), % 117.10/117.16 inference(scs_inference,[],[768,2320,1224,37,2239,681,26,27,245,60,61,65,64,76,10,66,67,11,59,57,81,53,58,62,63])). % 117.10/117.16 cnf(2762,plain, % 117.10/117.16 (E(f17(f16(a1)),f17(a1))), % 117.10/117.16 inference(scs_inference,[],[768,2320,1224,37,2239,681,26,27,245,60,61,65,64,76,10,66,67,11,59,57,81,53,58,62,63,9])). % 117.10/117.16 cnf(2764,plain, % 117.10/117.16 (E(f13(f16(a1)),f13(a1))), % 117.10/117.16 inference(scs_inference,[],[768,2320,1224,37,2239,681,26,27,245,60,61,65,64,76,10,66,67,11,59,57,81,53,58,62,63,9,8,6])). % 117.10/117.16 cnf(2767,plain, % 117.10/117.16 (E(f16(f16(a1)),f16(a1))), % 117.10/117.16 inference(scs_inference,[],[768,2320,1224,37,2239,681,703,26,27,245,60,61,65,64,76,10,66,67,11,59,57,81,53,58,62,63,9,8,6,55,7])). % 117.10/117.16 cnf(2770,plain, % 117.10/117.16 (~E(a8,a5)), % 117.10/117.16 inference(scs_inference,[],[2476,768,2320,1224,37,2239,681,703,26,27,245,60,61,65,64,76,10,66,67,11,59,57,81,53,58,62,63,9,8,6,55,7,54,2])). % 117.10/117.16 cnf(2771,plain, % 117.10/117.16 (P3(f15(a5))), % 117.10/117.16 inference(scs_inference,[],[41,2476,768,2320,1224,37,2239,681,703,26,27,245,32,60,61,65,64,76,10,66,67,11,59,57,81,53,58,62,63,9,8,6,55,7,54,2,68])). % 117.10/117.16 cnf(2773,plain, % 117.10/117.16 (P4(f15(a5))), % 117.10/117.16 inference(scs_inference,[],[41,2476,768,2320,1224,37,2239,681,703,26,27,245,32,60,61,65,64,76,10,66,67,11,59,57,81,53,58,62,63,9,8,6,55,7,54,2,68,69])). % 117.10/117.16 cnf(2775,plain, % 117.10/117.16 (~E(f16(a1),a5)), % 117.10/117.16 inference(scs_inference,[],[41,2476,768,2320,2229,1224,37,2239,675,681,703,26,27,245,32,60,61,65,64,76,10,66,67,11,59,57,81,53,58,62,63,9,8,6,55,7,54,2,68,69,3])). % 117.10/117.16 cnf(2776,plain, % 117.10/117.16 (~P2(f13(a1),f13(a2))), % 117.10/117.16 inference(scs_inference,[],[41,2476,768,2320,2229,1091,1224,37,2239,675,681,703,26,27,245,32,60,61,65,64,76,10,66,67,11,59,57,81,53,58,62,63,9,8,6,55,7,54,2,68,69,3,84])). % 117.10/117.16 cnf(2778,plain, % 117.10/117.16 (P1(f7(f13(a1)))), % 117.10/117.16 inference(scs_inference,[],[41,2476,768,2320,2229,1091,1224,37,2239,675,681,703,26,27,245,95,32,48,60,61,65,64,76,10,66,67,11,59,57,81,53,58,62,63,9,8,6,55,7,54,2,68,69,3,84,80])). % 117.10/117.16 cnf(2783,plain, % 117.10/117.16 (~P2(f13(f16(a1)),f13(a2))), % 117.10/117.16 inference(scs_inference,[],[41,2476,768,863,2320,2229,1091,1224,37,2239,675,681,703,26,27,245,95,32,48,60,61,65,64,76,10,66,67,11,59,57,81,53,58,62,63,9,8,6,55,7,54,2,68,69,3,84,80,12,13])). % 117.10/117.16 cnf(2784,plain, % 117.10/117.16 (~P6(x27841,f16(f16(a10)))), % 117.10/117.16 inference(scs_inference,[],[41,2476,768,863,2320,2229,1091,1224,37,2239,675,681,703,26,27,245,170,95,32,48,60,61,65,64,76,10,66,67,11,59,57,81,53,58,62,63,9,8,6,55,7,54,2,68,69,3,84,80,12,13,16])). % 117.10/117.16 cnf(2787,plain, % 117.10/117.16 (E(f16(a10),f15(a10))), % 117.10/117.16 inference(scs_inference,[],[41,2476,98,404,768,863,2320,2229,1091,830,1224,37,2239,30,675,681,703,828,26,27,245,170,95,32,48,60,61,65,64,76,10,66,67,11,59,57,81,53,58,62,63,9,8,6,55,7,54,2,68,69,3,84,80,12,13,16,77,73])). % 117.10/117.16 cnf(2800,plain, % 117.10/117.16 (P1(f18(f18(a2)))), % 117.10/117.16 inference(scs_inference,[],[795,2748,61,59])). % 117.10/117.16 cnf(2804,plain, % 117.10/117.16 (P2(f9(a14),f13(a14))), % 117.10/117.16 inference(scs_inference,[],[795,2748,39,51,61,59,64,76])). % 117.10/117.16 cnf(2810,plain, % 117.10/117.16 (~P1(f9(f17(a5)))), % 117.10/117.16 inference(scs_inference,[],[795,2748,2351,39,51,61,59,64,76,67,60,65])). % 117.10/117.16 cnf(2812,plain, % 117.10/117.16 (E(f15(a1),f15(f16(a1)))), % 117.10/117.16 inference(scs_inference,[],[795,2748,2351,39,51,246,61,59,64,76,67,60,65,10])). % 117.10/117.16 cnf(2815,plain, % 117.10/117.16 (E(f18(a1),f18(f16(a1)))), % 117.10/117.16 inference(scs_inference,[],[795,2748,2351,39,51,246,61,59,64,76,67,60,65,10,66,11])). % 117.10/117.16 cnf(2816,plain, % 117.10/117.16 (P1(f16(f18(a2)))), % 117.10/117.16 inference(scs_inference,[],[795,2748,2351,39,51,246,61,59,64,76,67,60,65,10,66,11,57])). % 117.10/117.16 cnf(2818,plain, % 117.10/117.16 (P2(x28181,f13(x28181))), % 117.10/117.16 inference(scs_inference,[],[795,2748,2351,39,51,47,246,61,59,64,76,67,60,65,10,66,11,57,81])). % 117.10/117.16 cnf(2820,plain, % 117.10/117.16 (E(f18(a2),a1)), % 117.10/117.16 inference(scs_inference,[],[795,2748,2351,39,51,47,246,61,59,64,76,67,60,65,10,66,11,57,81,53])). % 117.10/117.16 cnf(2822,plain, % 117.10/117.16 (P1(f17(f18(a2)))), % 117.10/117.16 inference(scs_inference,[],[795,2748,2351,39,51,47,246,61,59,64,76,67,60,65,10,66,11,57,81,53,58])). % 117.10/117.16 cnf(2828,plain, % 117.10/117.16 (E(f17(a1),f17(f16(a1)))), % 117.10/117.16 inference(scs_inference,[],[795,2748,2351,39,51,47,246,61,59,64,76,67,60,65,10,66,11,57,81,53,58,62,63,9])). % 117.10/117.16 cnf(2829,plain, % 117.10/117.16 (E(f9(a1),f9(f16(a1)))), % 117.10/117.16 inference(scs_inference,[],[795,2748,2351,39,51,47,246,61,59,64,76,67,60,65,10,66,11,57,81,53,58,62,63,9,8])). % 117.10/117.16 cnf(2830,plain, % 117.10/117.16 (E(f13(a1),f13(f16(a1)))), % 117.10/117.16 inference(scs_inference,[],[795,2748,2351,39,51,47,246,61,59,64,76,67,60,65,10,66,11,57,81,53,58,62,63,9,8,6])). % 117.10/117.16 cnf(2834,plain, % 117.10/117.16 (E(f16(a1),f16(f16(a1)))), % 117.10/117.16 inference(scs_inference,[],[795,2748,2783,2778,2351,39,51,47,246,61,59,64,76,67,60,65,10,66,11,57,81,53,58,62,63,9,8,6,124,55,7])). % 117.10/117.16 cnf(2835,plain, % 117.10/117.16 (P3(f18(a2))), % 117.10/117.16 inference(scs_inference,[],[795,2748,2783,2778,2351,39,51,47,246,61,59,64,76,67,60,65,10,66,11,57,81,53,58,62,63,9,8,6,124,55,7,54])). % 117.10/117.16 cnf(2842,plain, % 117.10/117.16 (~E(f17(f16(a5)),f12(x28421))), % 117.10/117.16 inference(scs_inference,[],[2478,2536,795,2748,2760,2771,2773,2783,2778,2351,39,51,47,1782,246,61,59,64,76,67,60,65,10,66,11,57,81,53,58,62,63,9,8,6,124,55,7,54,2,68,69,3])). % 117.10/117.16 cnf(2843,plain, % 117.10/117.16 (~P2(f13(x28431),f13(f18(a2)))), % 117.10/117.16 inference(scs_inference,[],[2478,2536,795,2748,2760,2771,2773,2783,2778,2351,615,39,51,47,1782,246,61,59,64,76,67,60,65,10,66,11,57,81,53,58,62,63,9,8,6,124,55,7,54,2,68,69,3,84])). % 117.10/117.16 cnf(2845,plain, % 117.10/117.16 (P2(f7(f9(a5)),a5)), % 117.10/117.16 inference(scs_inference,[],[2478,2740,2536,795,2748,2760,2771,2773,2783,2778,2351,615,39,51,47,1782,246,2366,61,59,64,76,67,60,65,10,66,11,57,81,53,58,62,63,9,8,6,124,55,7,54,2,68,69,3,84,85])). % 117.10/117.16 cnf(2847,plain, % 117.10/117.16 (P6(f9(a5),f13(a5))), % 117.10/117.16 inference(scs_inference,[],[2478,2740,2536,795,2748,2760,2771,2773,2783,2778,2351,615,39,51,47,52,1782,246,2366,61,59,64,76,67,60,65,10,66,11,57,81,53,58,62,63,9,8,6,124,55,7,54,2,68,69,3,84,85,80])). % 117.10/117.16 cnf(2851,plain, % 117.10/117.16 (~E(f13(f13(a1)),f13(a2))), % 117.10/117.16 inference(scs_inference,[],[2478,2740,2536,795,2748,2760,2771,2773,2776,2783,860,2778,2351,615,39,51,47,52,1782,246,2366,61,59,64,76,67,60,65,10,66,11,57,81,53,58,62,63,9,8,6,124,55,7,54,2,68,69,3,84,85,80,12,14])). % 117.10/117.16 cnf(2852,plain, % 117.10/117.16 (P2(f16(f16(a1)),f13(x28521))), % 117.10/117.16 inference(scs_inference,[],[2478,2740,2536,795,2748,2760,2771,2773,2776,2783,860,2778,2351,615,39,597,51,47,52,1782,246,2366,61,59,64,76,67,60,65,10,66,11,57,81,53,58,62,63,9,8,6,124,55,7,54,2,68,69,3,84,85,80,12,14,13])). % 117.10/117.16 cnf(2858,plain, % 117.10/117.16 (E(f16(a5),f15(a5))), % 117.10/117.16 inference(scs_inference,[],[41,2478,2740,2536,795,2748,2760,2771,2773,2776,2747,2783,860,2778,2351,615,39,597,51,47,819,43,52,1782,246,2366,32,61,59,64,76,67,60,65,10,66,11,57,81,53,58,62,63,9,8,6,124,55,7,54,2,68,69,3,84,85,80,12,14,13,19,16,77,73])). % 117.10/117.16 cnf(2862,plain, % 117.10/117.16 (~P6(f13(a5),f9(a5))), % 117.10/117.16 inference(scs_inference,[],[41,2478,2740,2536,795,2748,2760,2771,2773,2776,2747,2783,860,2778,2351,615,39,597,51,47,819,43,52,1782,246,2366,32,61,59,64,76,67,60,65,10,66,11,57,81,53,58,62,63,9,8,6,124,55,7,54,2,68,69,3,84,85,80,12,14,13,19,16,77,73,4,5,82])). % 117.10/117.16 cnf(2886,plain, % 117.10/117.16 (P1(f18(f16(a2)))), % 117.10/117.16 inference(scs_inference,[],[2750,59])). % 117.10/117.16 cnf(2888,plain, % 117.10/117.16 (P4(f16(f17(a10)))), % 117.10/117.16 inference(scs_inference,[],[806,2750,59,61])). % 117.10/117.16 cnf(2894,plain, % 117.10/117.16 (P4(f16(a10))), % 117.10/117.16 inference(scs_inference,[],[806,2750,40,28,59,61,67,64,60])). % 117.10/117.16 cnf(2899,plain, % 117.10/117.16 (~P1(f9(f18(a11)))), % 117.10/117.16 inference(scs_inference,[],[806,2750,2820,40,574,28,59,61,67,64,60,66,11,65])). % 117.10/117.16 cnf(2901,plain, % 117.10/117.16 (P1(f16(f16(a2)))), % 117.10/117.16 inference(scs_inference,[],[806,2750,2820,40,574,28,59,61,67,64,60,66,11,65,57])). % 117.10/117.16 cnf(2904,plain, % 117.10/117.16 (P1(f17(f16(a2)))), % 117.10/117.16 inference(scs_inference,[],[806,2750,2820,40,574,28,59,61,67,64,60,66,11,65,57,10,58])). % 117.10/117.16 cnf(2906,plain, % 117.10/117.16 (E(f16(a2),a1)), % 117.10/117.16 inference(scs_inference,[],[806,2750,2820,40,574,28,59,61,67,64,60,66,11,65,57,10,58,53])). % 117.10/117.16 cnf(2912,plain, % 117.10/117.16 (E(f17(f18(a2)),f17(a1))), % 117.10/117.16 inference(scs_inference,[],[806,2750,2820,40,574,28,59,61,67,64,60,66,11,65,57,10,58,53,62,63,9])). % 117.10/117.16 cnf(2914,plain, % 117.10/117.16 (E(f13(f18(a2)),f13(a1))), % 117.10/117.16 inference(scs_inference,[],[806,2750,2820,40,574,28,59,61,67,64,60,66,11,65,57,10,58,53,62,63,9,8,6])). % 117.10/117.16 cnf(2916,plain, % 117.10/117.16 (P4(a8)), % 117.10/117.16 inference(scs_inference,[],[806,2750,2820,2843,40,574,28,27,59,61,67,64,60,66,11,65,57,10,58,53,62,63,9,8,6,124,55])). % 117.10/117.16 cnf(2919,plain, % 117.10/117.16 (P3(f16(a2))), % 117.10/117.16 inference(scs_inference,[],[806,2750,2820,2843,40,574,28,27,59,61,67,64,60,66,11,65,57,10,58,53,62,63,9,8,6,124,55,7,54])). % 117.10/117.16 cnf(2921,plain, % 117.10/117.16 (~E(a2,a5)), % 117.10/117.16 inference(scs_inference,[],[2501,806,2750,2820,2843,40,574,28,27,59,61,67,64,60,66,11,65,57,10,58,53,62,63,9,8,6,124,55,7,54,2])). % 117.10/117.16 cnf(2924,plain, % 117.10/117.16 (P4(f15(f16(a2)))), % 117.10/117.16 inference(scs_inference,[],[2501,806,2732,2750,2820,2843,40,2771,2773,574,28,27,59,61,67,64,60,66,11,65,57,10,58,53,62,63,9,8,6,124,55,7,54,2,68,69])). % 117.10/117.16 cnf(2926,plain, % 117.10/117.16 (~E(f15(a5),a10)), % 117.10/117.16 inference(scs_inference,[],[2501,2858,2505,806,2732,2750,2820,2843,40,2771,2773,574,28,27,59,61,67,64,60,66,11,65,57,10,58,53,62,63,9,8,6,124,55,7,54,2,68,69,3])). % 117.10/117.16 cnf(2927,plain, % 117.10/117.16 (~P2(f13(a5),f13(f16(a2)))), % 117.10/117.16 inference(scs_inference,[],[2501,2858,2505,2847,806,2732,2750,2820,2843,40,2771,2773,574,28,27,59,61,67,64,60,66,11,65,57,10,58,53,62,63,9,8,6,124,55,7,54,2,68,69,3,84])). % 117.10/117.16 cnf(2930,plain, % 117.10/117.16 (P2(x29301,f13(x29301))), % 117.10/117.16 inference(rename_variables,[],[2818])). % 117.10/117.16 cnf(2932,plain, % 117.10/117.16 (~P2(f13(a5),f9(a5))), % 117.10/117.16 inference(scs_inference,[],[2501,2818,2858,2505,2847,2862,806,2732,2750,2820,2843,40,2771,2773,2281,574,28,27,59,61,67,64,60,66,11,65,57,10,58,53,62,63,9,8,6,124,55,7,54,2,68,69,3,84,85,80])). % 117.10/117.16 cnf(2935,plain, % 117.10/117.16 (P4(f17(a1))), % 117.10/117.16 inference(scs_inference,[],[2501,2818,2858,2505,2847,2862,806,2732,2750,2820,2843,791,2736,2762,40,2771,2773,2281,574,28,27,59,61,67,64,60,66,11,65,57,10,58,53,62,63,9,8,6,124,55,7,54,2,68,69,3,84,85,80,12,17])). % 117.10/117.16 cnf(2940,plain, % 117.10/117.16 (~E(f16(a2),f13(a5))), % 117.10/117.16 inference(scs_inference,[],[2501,2818,2930,2858,2505,2847,2862,255,314,806,2732,2750,2820,2843,791,2736,2834,2762,40,2771,2773,2281,574,28,27,48,59,61,67,64,60,66,11,65,57,10,58,53,62,63,9,8,6,124,55,7,54,2,68,69,3,84,85,80,12,17,21,22,14,13])). % 117.10/117.16 cnf(2942,plain, % 117.10/117.16 (P6(f7(f16(a5)),f15(a5))), % 117.10/117.16 inference(scs_inference,[],[2501,2818,2930,2858,2505,2847,2862,255,314,806,2732,2750,2820,2843,791,2736,2834,2762,40,2771,2773,2281,574,28,2293,27,48,59,61,67,64,60,66,11,65,57,10,58,53,62,63,9,8,6,124,55,7,54,2,68,69,3,84,85,80,12,17,21,22,14,13,16])). % 117.10/117.16 cnf(2943,plain, % 117.10/117.16 (P3(f16(a4))), % 117.10/117.16 inference(scs_inference,[],[2501,42,2818,2930,2858,2505,2847,2862,255,314,806,2732,2750,2820,2843,791,2736,2834,2762,40,2771,2773,2281,574,31,39,28,2293,27,48,59,61,67,64,60,66,11,65,57,10,58,53,62,63,9,8,6,124,55,7,54,2,68,69,3,84,85,80,12,17,21,22,14,13,16,77])). % 117.10/117.16 cnf(2945,plain, % 117.10/117.16 (E(f16(a4),f15(a4))), % 117.10/117.16 inference(scs_inference,[],[2501,42,2818,2930,2858,2505,2847,2862,255,314,806,2732,2750,2820,2843,791,2736,2834,2762,40,2771,2773,2281,574,31,39,28,2293,27,48,59,61,67,64,60,66,11,65,57,10,58,53,62,63,9,8,6,124,55,7,54,2,68,69,3,84,85,80,12,17,21,22,14,13,16,77,73])). % 117.10/117.16 cnf(2950,plain, % 117.10/117.16 (~P1(f15(a5))), % 117.10/117.16 inference(scs_inference,[],[2501,42,2818,2930,2858,2505,2847,2862,255,314,806,2732,2750,2820,2843,791,2736,2834,2762,40,2771,2773,2281,574,31,39,28,2293,27,48,59,61,67,64,60,66,11,65,57,10,58,53,62,63,9,8,6,124,55,7,54,2,68,69,3,84,85,80,12,17,21,22,14,13,16,77,73,4,5,102,74])). % 117.10/117.16 cnf(2956,plain, % 117.10/117.16 (~P1(f17(f15(a5)))), % 117.10/117.16 inference(scs_inference,[],[2501,42,2818,2930,2858,2505,2847,2862,255,314,806,2732,2750,2820,2843,791,2736,2834,2762,40,2771,2773,2281,574,31,39,28,2293,27,48,59,61,67,64,60,66,11,65,57,10,58,53,62,63,9,8,6,124,55,7,54,2,68,69,3,84,85,80,12,17,21,22,14,13,16,77,73,4,5,102,74,82,72,71])). % 117.10/117.16 cnf(2958,plain, % 117.10/117.16 (P5(f16(a2))), % 117.10/117.16 inference(scs_inference,[],[2501,42,2818,2930,2858,2505,2847,2862,255,314,806,2732,2750,2820,2843,791,2736,2834,2762,40,2771,2773,2281,574,31,39,28,2293,27,48,59,61,67,64,60,66,11,65,57,10,58,53,62,63,9,8,6,124,55,7,54,2,68,69,3,84,85,80,12,17,21,22,14,13,16,77,73,4,5,102,74,82,72,71,70])). % 117.10/117.16 cnf(2964,plain, % 117.10/117.16 (P1(f18(f17(a2)))), % 117.10/117.16 inference(scs_inference,[],[2756,2935,61,59])). % 117.10/117.16 cnf(2968,plain, % 117.10/117.16 (E(f17(f16(a8)),f18(a8))), % 117.10/117.16 inference(scs_inference,[],[2916,2756,2935,61,59,64,67])). % 117.10/117.16 cnf(2972,plain, % 117.10/117.16 (~P1(f9(f15(a5)))), % 117.10/117.16 inference(scs_inference,[],[2916,2756,2935,2950,61,59,64,67,66,65])). % 117.10/117.16 cnf(2974,plain, % 117.10/117.16 (P1(f16(f17(a2)))), % 117.10/117.16 inference(scs_inference,[],[2916,2756,2935,2950,61,59,64,67,66,65,57])). % 117.10/117.16 cnf(2976,plain, % 117.10/117.16 (E(f15(f16(a2)),f15(a1))), % 117.10/117.16 inference(scs_inference,[],[2916,2756,2935,2950,2906,61,59,64,67,66,65,57,10])). % 117.10/117.16 cnf(2978,plain, % 117.10/117.16 (P1(f17(f17(a2)))), % 117.10/117.16 inference(scs_inference,[],[2916,2756,2935,2950,2906,61,59,64,67,66,65,57,10,11,58])). % 117.10/117.16 cnf(2980,plain, % 117.10/117.16 (E(f17(a2),a1)), % 117.10/117.16 inference(scs_inference,[],[2916,2756,2935,2950,2906,61,59,64,67,66,65,57,10,11,58,53])). % 117.10/117.16 cnf(2988,plain, % 117.10/117.16 (E(f13(f16(a2)),f13(a1))), % 117.10/117.16 inference(scs_inference,[],[2916,2756,2935,2950,2906,61,59,64,67,66,65,57,10,11,58,53,62,63,9,8,6])). % 117.10/117.16 cnf(2990,plain, % 117.10/117.16 (P4(f12(x29901))), % 117.10/117.16 inference(scs_inference,[],[2916,2756,2935,2950,2906,2927,46,61,59,64,67,66,65,57,10,11,58,53,62,63,9,8,6,124,55])). % 117.10/117.16 cnf(2993,plain, % 117.10/117.16 (P3(f17(a2))), % 117.10/117.16 inference(scs_inference,[],[2916,2756,2935,2950,2906,2927,46,61,59,64,67,66,65,57,10,11,58,53,62,63,9,8,6,124,55,7,54])). % 117.10/117.16 cnf(2995,plain, % 117.10/117.16 (~E(f16(a1),f9(a5))), % 117.10/117.16 inference(scs_inference,[],[2916,2468,2756,2935,2950,2906,2927,46,61,59,64,67,66,65,57,10,11,58,53,62,63,9,8,6,124,55,7,54,2])). % 117.10/117.16 cnf(2996,plain, % 117.10/117.16 (P3(f15(a8))), % 117.10/117.16 inference(scs_inference,[],[2916,2468,2756,2935,2950,2906,2927,219,46,61,59,64,67,66,65,57,10,11,58,53,62,63,9,8,6,124,55,7,54,2,68])). % 117.10/117.16 cnf(3000,plain, % 117.10/117.16 (~P1(f18(f15(a5)))), % 117.10/117.16 inference(scs_inference,[],[2916,2468,2756,2835,2935,2950,2906,2927,2760,219,2773,46,61,59,64,67,66,65,57,10,11,58,53,62,63,9,8,6,124,55,7,54,2,68,69,72])). % 117.10/117.16 cnf(3003,plain, % 117.10/117.16 (~P2(f15(a5),f13(f17(a2)))), % 117.10/117.16 inference(scs_inference,[],[2916,2468,2756,2835,2935,2940,2950,2906,2942,2927,2760,219,2773,46,61,59,64,67,66,65,57,10,11,58,53,62,63,9,8,6,124,55,7,54,2,68,69,72,3,84])). % 117.10/117.16 cnf(3005,plain, % 117.10/117.16 (P6(f9(a14),f13(a14))), % 117.10/117.16 inference(scs_inference,[],[2916,2468,2804,2756,2835,2935,2940,2950,2906,2942,2927,2760,219,2773,46,52,61,59,64,67,66,65,57,10,11,58,53,62,63,9,8,6,124,55,7,54,2,68,69,72,3,84,80])). % 117.10/117.16 cnf(3008,plain, % 117.10/117.16 (~E(f17(a2),f15(a5))), % 117.10/117.16 inference(scs_inference,[],[2916,2468,2804,2756,2835,2935,2940,2950,2906,2942,2927,2760,219,2773,46,52,61,59,64,67,66,65,57,10,11,58,53,62,63,9,8,6,124,55,7,54,2,68,69,72,3,84,80,12])). % 117.10/117.16 cnf(3009,plain, % 117.10/117.16 (~E(f13(f13(a5)),f9(a5))), % 117.10/117.16 inference(scs_inference,[],[2916,2468,2804,2756,2835,2932,2935,2940,2950,2906,2942,2927,2818,2760,219,2773,46,52,61,59,64,67,66,65,57,10,11,58,53,62,63,9,8,6,124,55,7,54,2,68,69,72,3,84,80,12,14])). % 117.10/117.16 cnf(3010,plain, % 117.10/117.16 (P2(x30101,f13(x30101))), % 117.10/117.16 inference(rename_variables,[],[2818])). % 117.10/117.16 cnf(3011,plain, % 117.10/117.16 (P2(f15(a4),f13(f16(a4)))), % 117.10/117.16 inference(scs_inference,[],[2916,2468,2804,2756,2835,2932,2935,2940,2945,2950,2906,2942,2927,2818,3010,2760,219,2773,46,52,61,59,64,67,66,65,57,10,11,58,53,62,63,9,8,6,124,55,7,54,2,68,69,72,3,84,80,12,14,13])). % 117.10/117.16 cnf(3014,plain, % 117.10/117.16 (P3(f16(f16(a2)))), % 117.10/117.16 inference(scs_inference,[],[2916,2468,2804,2756,2835,2919,2932,2935,2940,2945,2950,2958,2906,2942,2371,2927,2818,3010,2847,2760,219,2732,2773,46,52,61,59,64,67,66,65,57,10,11,58,53,62,63,9,8,6,124,55,7,54,2,68,69,72,3,84,80,12,14,13,16,77])). % 117.10/117.16 cnf(3016,plain, % 117.10/117.16 (E(f16(a8),f15(a8))), % 117.10/117.16 inference(scs_inference,[],[244,2916,2468,2804,2756,2835,2919,2932,2935,2940,2945,2950,2958,2906,2942,2371,2927,2818,3010,2847,2760,219,2732,2773,46,52,61,59,64,67,66,65,57,10,11,58,53,62,63,9,8,6,124,55,7,54,2,68,69,72,3,84,80,12,14,13,16,77,73])). % 117.10/117.16 cnf(3018,plain, % 117.10/117.16 (P5(f17(a2))), % 117.10/117.16 inference(scs_inference,[],[244,2916,2468,2804,2756,2835,2919,2932,2935,2940,2945,2950,2958,2906,2942,2371,2927,2818,3010,795,2847,2760,219,2732,2773,46,52,61,59,64,67,66,65,57,10,11,58,53,62,63,9,8,6,124,55,7,54,2,68,69,72,3,84,80,12,14,13,16,77,73,70])). % 117.10/117.16 cnf(3022,plain, % 117.10/117.16 (~P6(f13(a14),f9(a14))), % 117.10/117.16 inference(scs_inference,[],[244,2916,2468,2804,2756,2835,2919,2932,2935,2940,2945,2950,2958,2906,2942,2371,2927,2818,3010,795,2847,2760,219,2732,2773,46,52,61,59,64,67,66,65,57,10,11,58,53,62,63,9,8,6,124,55,7,54,2,68,69,72,3,84,80,12,14,13,16,77,73,70,4,5,82])). % 117.10/117.16 cnf(3036,plain, % 117.10/117.16 (P1(f18(f16(a1)))), % 117.10/117.16 inference(scs_inference,[],[254,59])). % 117.10/117.16 cnf(3038,plain, % 117.10/117.16 (P4(f16(a11))), % 117.10/117.16 inference(scs_inference,[],[38,254,59,61])). % 117.10/117.16 cnf(3040,plain, % 117.10/117.16 (E(f17(f16(a2)),f18(a2))), % 117.10/117.16 inference(scs_inference,[],[36,38,254,59,61,67])). % 117.10/117.16 cnf(3042,plain, % 117.10/117.16 (E(f16(f16(a2)),a2)), % 117.10/117.16 inference(scs_inference,[],[36,38,254,59,61,67,64])). % 117.10/117.16 cnf(3044,plain, % 117.10/117.16 (E(f18(f16(a2)),f17(a2))), % 117.10/117.16 inference(scs_inference,[],[36,38,254,59,61,67,64,66])). % 117.10/117.16 cnf(3046,plain, % 117.10/117.16 (~P1(f9(f9(a11)))), % 117.10/117.16 inference(scs_inference,[],[36,38,298,254,59,61,67,64,66,65])). % 117.10/117.16 cnf(3048,plain, % 117.10/117.16 (P1(f16(a10))), % 117.10/117.16 inference(scs_inference,[],[36,38,298,254,28,59,61,67,64,66,65,57])). % 117.10/117.16 cnf(3052,plain, % 117.10/117.16 (P1(f17(f16(a1)))), % 117.10/117.16 inference(scs_inference,[],[2980,36,38,298,254,28,59,61,67,64,66,65,57,10,11,58])). % 117.10/117.16 cnf(3054,plain, % 117.10/117.16 (E(f18(f18(a2)),a1)), % 117.10/117.16 inference(scs_inference,[],[2980,2800,36,38,298,254,28,59,61,67,64,66,65,57,10,11,58,53])). % 117.10/117.16 cnf(3058,plain, % 117.10/117.16 (P4(f18(a10))), % 117.10/117.16 inference(scs_inference,[],[2980,2800,36,38,298,254,28,46,59,61,67,64,66,65,57,10,11,58,53,62,63])). % 117.10/117.16 cnf(3060,plain, % 117.10/117.16 (E(f17(f17(a2)),f17(a1))), % 117.10/117.16 inference(scs_inference,[],[2980,2800,36,38,298,254,28,46,59,61,67,64,66,65,57,10,11,58,53,62,63,9])). % 117.10/117.16 cnf(3062,plain, % 117.10/117.16 (E(f13(f17(a2)),f13(a1))), % 117.10/117.16 inference(scs_inference,[],[2980,2800,36,38,298,254,28,46,59,61,67,64,66,65,57,10,11,58,53,62,63,9,8,6])). % 117.10/117.16 cnf(3063,plain, % 117.10/117.16 (~E(f12(f17(a2)),f15(a5))), % 117.10/117.16 inference(scs_inference,[],[2980,2800,3003,36,38,298,254,28,46,59,61,67,64,66,65,57,10,11,58,53,62,63,9,8,6,124])). % 117.10/117.16 cnf(3067,plain, % 117.10/117.16 (~E(f16(a1),f17(a5))), % 117.10/117.16 inference(scs_inference,[],[2494,2980,2800,3003,36,38,298,254,28,46,59,61,67,64,66,65,57,10,11,58,53,62,63,9,8,6,124,7,54,2])). % 117.10/117.16 cnf(3072,plain, % 117.10/117.16 (~E(a1,f15(a5))), % 117.10/117.16 inference(scs_inference,[],[2494,2993,3008,2980,2800,3003,795,36,38,298,254,28,46,59,61,67,64,66,65,57,10,11,58,53,62,63,9,8,6,124,7,54,2,68,69,3])). % 117.10/117.16 cnf(3073,plain, % 117.10/117.16 (~P2(f13(a14),f13(f16(a1)))), % 117.10/117.16 inference(scs_inference,[],[2494,2993,3005,3008,2980,2800,3003,795,36,38,298,254,28,46,59,61,67,64,66,65,57,10,11,58,53,62,63,9,8,6,124,7,54,2,68,69,3,84])). % 117.10/117.16 cnf(3075,plain, % 117.10/117.16 (P1(f16(f16(a10)))), % 117.10/117.16 inference(scs_inference,[],[2494,2993,3005,3008,2980,2784,2800,3003,795,36,38,298,254,28,46,48,59,61,67,64,66,65,57,10,11,58,53,62,63,9,8,6,124,7,54,2,68,69,3,84,80])). % 117.10/117.16 cnf(3077,plain, % 117.10/117.16 (P2(f7(x30771),x30771)), % 117.10/117.16 inference(rename_variables,[],[48])). % 117.10/117.16 cnf(3079,plain, % 117.10/117.16 (~E(f18(f18(a2)),f17(a5))), % 117.10/117.16 inference(scs_inference,[],[2494,2993,3005,3008,2980,2784,2800,3003,2310,795,36,38,298,254,28,46,48,59,61,67,64,66,65,57,10,11,58,53,62,63,9,8,6,124,7,54,2,68,69,3,84,80,12])). % 117.10/117.16 cnf(3080,plain, % 117.10/117.16 (P4(f15(a10))), % 117.10/117.16 inference(scs_inference,[],[2494,2894,2993,3005,3008,2980,2784,2800,3003,2787,2310,795,36,38,298,254,28,46,48,59,61,67,64,66,65,57,10,11,58,53,62,63,9,8,6,124,7,54,2,68,69,3,84,80,12,17])). % 117.10/117.16 cnf(3081,plain, % 117.10/117.16 (P2(f7(f16(a8)),f15(a8))), % 117.10/117.16 inference(scs_inference,[],[2494,2894,2993,3005,3008,3016,2980,2784,2800,3003,2787,2310,795,36,38,298,254,28,46,48,3077,59,61,67,64,66,65,57,10,11,58,53,62,63,9,8,6,124,7,54,2,68,69,3,84,80,12,17,14])). % 117.10/117.16 cnf(3083,plain, % 117.10/117.16 (~P2(f16(a5),f13(f17(a2)))), % 117.10/117.16 inference(scs_inference,[],[2494,2894,2993,3005,3008,3016,2980,2784,2800,3003,2787,2310,795,36,38,2858,298,254,28,46,48,3077,59,61,67,64,66,65,57,10,11,58,53,62,63,9,8,6,124,7,54,2,68,69,3,84,80,12,17,14,13])). % 117.10/117.16 cnf(3084,plain, % 117.10/117.16 (~P6(x30841,f17(a2))), % 117.10/117.16 inference(scs_inference,[],[2494,2894,2993,3005,3008,3016,2980,2784,2800,3003,2787,2310,795,36,38,2858,298,254,28,86,46,48,3077,59,61,67,64,66,65,57,10,11,58,53,62,63,9,8,6,124,7,54,2,68,69,3,84,80,12,17,14,13,16])). % 117.10/117.16 cnf(3085,plain, % 117.10/117.16 (P3(f16(f12(a1)))), % 117.10/117.16 inference(scs_inference,[],[2494,2990,1139,2894,2993,3005,3008,3016,2980,2784,2800,3003,2787,2310,795,36,38,2858,298,1090,254,28,86,46,48,3077,59,61,67,64,66,65,57,10,11,58,53,62,63,9,8,6,124,7,54,2,68,69,3,84,80,12,17,14,13,16,77])). % 117.10/117.16 cnf(3088,plain, % 117.10/117.16 (E(f16(a1),f15(a1))), % 117.10/117.17 inference(scs_inference,[],[2494,2990,1139,2894,2993,3005,3008,3016,2980,2784,2800,3003,2787,2310,312,795,36,308,38,2858,298,1090,254,28,34,86,46,48,3077,59,61,67,64,66,65,57,10,11,58,53,62,63,9,8,6,124,7,54,2,68,69,3,84,80,12,17,14,13,16,77,73])). % 117.10/117.17 cnf(3097,plain, % 117.10/117.17 (P1(f18(f16(a10)))), % 117.10/117.17 inference(scs_inference,[],[3038,3048,61,59])). % 117.10/117.17 cnf(3099,plain, % 117.10/117.17 (E(f16(f16(a11)),a11)), % 117.10/117.17 inference(scs_inference,[],[3038,3048,38,61,59,64])). % 117.10/117.17 cnf(3105,plain, % 117.10/117.17 (~P1(f9(a14))), % 117.10/117.17 inference(scs_inference,[],[3038,3048,38,51,61,59,64,67,66,65])). % 117.10/117.17 cnf(3107,plain, % 117.10/117.17 (P1(f16(a8))), % 117.10/117.17 inference(scs_inference,[],[3038,3048,38,51,27,61,59,64,67,66,65,57])). % 117.10/117.17 cnf(3109,plain, % 117.10/117.17 (P1(f17(f16(a10)))), % 117.10/117.17 inference(scs_inference,[],[3038,3048,38,51,27,61,59,64,67,66,65,57,58])). % 117.10/117.17 cnf(3111,plain, % 117.10/117.17 (E(f16(a10),a1)), % 117.10/117.17 inference(scs_inference,[],[3038,3048,38,51,27,61,59,64,67,66,65,57,58,53])). % 117.10/117.17 cnf(3115,plain, % 117.10/117.17 (P4(f18(f16(a10)))), % 117.10/117.17 inference(scs_inference,[],[3038,3048,38,51,27,61,59,64,67,66,65,57,58,53,62,63])). % 117.10/117.17 cnf(3119,plain, % 117.10/117.17 (E(f13(f16(a10)),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[3038,3048,38,51,27,61,59,64,67,66,65,57,58,53,62,63,9,8,6])). % 117.10/117.17 cnf(3122,plain, % 117.10/117.17 (P3(f16(a10))), % 117.10/117.17 inference(scs_inference,[],[3038,3048,3073,38,51,27,61,59,64,67,66,65,57,58,53,62,63,9,8,6,124,7,54])). % 117.10/117.17 cnf(3129,plain, % 117.10/117.17 (~E(f15(a1),f17(a5))), % 117.10/117.17 inference(scs_inference,[],[2470,3067,3038,3048,3088,3073,2894,830,38,51,828,27,61,59,64,67,66,65,57,58,53,62,63,9,8,6,124,7,54,2,69,68,3])). % 117.10/117.17 cnf(3130,plain, % 117.10/117.17 (~P2(f13(x31301),f13(f16(a10)))), % 117.10/117.17 inference(scs_inference,[],[2470,3067,3038,3048,3088,3073,651,2894,830,38,51,828,27,61,59,64,67,66,65,57,58,53,62,63,9,8,6,124,7,54,2,69,68,3,84])). % 117.10/117.17 cnf(3132,plain, % 117.10/117.17 (P6(f16(f16(a5)),f13(a5))), % 117.10/117.17 inference(scs_inference,[],[2470,3067,3038,3048,3088,2752,3073,651,2894,830,38,51,828,27,52,61,59,64,67,66,65,57,58,53,62,63,9,8,6,124,7,54,2,69,68,3,84,80])). % 117.10/117.17 cnf(3135,plain, % 117.10/117.17 (~E(f16(a10),f9(f17(a5)))), % 117.10/117.17 inference(scs_inference,[],[2470,3067,3038,3048,3088,2752,2810,3073,651,2894,830,38,51,828,27,52,61,59,64,67,66,65,57,58,53,62,63,9,8,6,124,7,54,2,69,68,3,84,80,12])). % 117.10/117.17 cnf(3136,plain, % 117.10/117.17 (~P2(f13(a14),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[2470,3067,3038,3048,3088,2752,2810,3073,2830,651,2894,830,38,51,828,27,52,61,59,64,67,66,65,57,58,53,62,63,9,8,6,124,7,54,2,69,68,3,84,80,12,14])). % 117.10/117.17 cnf(3137,plain, % 117.10/117.17 (P2(f15(a1),f13(f16(a1)))), % 117.10/117.17 inference(scs_inference,[],[2470,3067,3038,3048,3088,2752,2810,3073,2830,651,2894,830,2818,38,51,828,27,52,61,59,64,67,66,65,57,58,53,62,63,9,8,6,124,7,54,2,69,68,3,84,80,12,14,13])). % 117.10/117.17 cnf(3140,plain, % 117.10/117.17 (~P6(x31401,f18(f16(a2)))), % 117.10/117.17 inference(scs_inference,[],[100,2470,3067,3084,3038,3048,3088,2752,3044,2810,3073,2830,651,2894,830,2818,38,51,828,27,52,61,59,64,67,66,65,57,58,53,62,63,9,8,6,124,7,54,2,69,68,3,84,80,12,14,13,15,16])). % 117.10/117.17 cnf(3147,plain, % 117.10/117.17 (~P6(f13(a5),f16(f16(a5)))), % 117.10/117.17 inference(scs_inference,[],[100,2470,3067,3084,3018,3038,3048,3088,2752,3044,2810,3073,2830,651,2894,830,2818,2993,795,38,51,828,27,52,61,59,64,67,66,65,57,58,53,62,63,9,8,6,124,7,54,2,69,68,3,84,80,12,14,13,15,16,77,4,5,10,11,82])). % 117.10/117.17 cnf(3151,plain, % 117.10/117.17 (~E(f7(a5),f13(a5))), % 117.10/117.17 inference(scs_inference,[],[100,2470,3067,3084,3018,3038,3048,3088,2752,3044,2810,3073,2830,651,2894,830,2818,2993,795,38,51,828,27,52,61,59,64,67,66,65,57,58,53,62,63,9,8,6,124,7,54,2,69,68,3,84,80,12,14,13,15,16,77,4,5,10,11,82,1779,2462])). % 117.10/117.17 cnf(3155,plain, % 117.10/117.17 (P1(f18(f16(a8)))), % 117.10/117.17 inference(scs_inference,[],[3107,59])). % 117.10/117.17 cnf(3159,plain, % 117.10/117.17 (E(f17(f16(a1)),f18(a1))), % 117.10/117.17 inference(scs_inference,[],[3058,3107,34,59,61,67])). % 117.10/117.17 cnf(3163,plain, % 117.10/117.17 (E(f18(f16(a1)),f17(a1))), % 117.10/117.17 inference(scs_inference,[],[3058,3107,34,35,59,61,67,64,66])). % 117.10/117.17 cnf(3165,plain, % 117.10/117.17 (~P1(f9(f9(a14)))), % 117.10/117.17 inference(scs_inference,[],[3058,3105,3107,34,35,59,61,67,64,66,65])). % 117.10/117.17 cnf(3167,plain, % 117.10/117.17 (P1(f16(f16(a8)))), % 117.10/117.17 inference(scs_inference,[],[3058,3105,3107,34,35,59,61,67,64,66,65,57])). % 117.10/117.17 cnf(3169,plain, % 117.10/117.17 (P1(f17(f16(a8)))), % 117.10/117.17 inference(scs_inference,[],[3058,3105,3107,34,35,59,61,67,64,66,65,57,58])). % 117.10/117.17 cnf(3171,plain, % 117.10/117.17 (E(f16(a8),a1)), % 117.10/117.17 inference(scs_inference,[],[3058,3105,3107,34,35,59,61,67,64,66,65,57,58,53])). % 117.10/117.17 cnf(3179,plain, % 117.10/117.17 (E(f13(f16(a8)),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[3058,3105,3107,34,35,59,61,67,64,66,65,57,58,53,62,63,9,8,6])). % 117.10/117.17 cnf(3181,plain, % 117.10/117.17 (E(f16(f16(a8)),f16(a1))), % 117.10/117.17 inference(scs_inference,[],[3058,3105,3107,3136,34,35,59,61,67,64,66,65,57,58,53,62,63,9,8,6,124,7])). % 117.10/117.17 cnf(3182,plain, % 117.10/117.17 (P3(f16(a8))), % 117.10/117.17 inference(scs_inference,[],[3058,3105,3107,3136,34,35,59,61,67,64,66,65,57,58,53,62,63,9,8,6,124,7,54])). % 117.10/117.17 cnf(3190,plain, % 117.10/117.17 (~P2(f13(a5),f13(f16(a8)))), % 117.10/117.17 inference(scs_inference,[],[2474,3058,3105,3107,3136,3111,3132,3135,2919,768,2732,34,35,59,61,67,64,66,65,57,58,53,62,63,9,8,6,124,7,54,2,69,68,3,84])). % 117.10/117.17 cnf(3192,plain, % 117.10/117.17 (~P2(f13(a14),f9(a14))), % 117.10/117.17 inference(scs_inference,[],[3022,2474,3058,3105,3107,3136,3111,3132,3135,2919,768,2732,34,35,59,61,67,64,66,65,57,58,53,62,63,9,8,6,124,7,54,2,69,68,3,84,80])). % 117.10/117.17 cnf(3194,plain, % 117.10/117.17 (~E(f16(a8),f9(a14))), % 117.10/117.17 inference(scs_inference,[],[3022,2474,3058,3105,3107,3136,3111,3132,3135,2919,768,2732,34,35,59,61,67,64,66,65,57,58,53,62,63,9,8,6,124,7,54,2,69,68,3,84,80,12])). % 117.10/117.17 cnf(3197,plain, % 117.10/117.17 (~E(f16(f16(a1)),f13(a14))), % 117.10/117.17 inference(scs_inference,[],[3022,2474,3058,3105,3107,3136,3111,2852,3132,3135,2919,768,2732,34,35,48,59,61,67,64,66,65,57,58,53,62,63,9,8,6,124,7,54,2,69,68,3,84,80,12,14,13])). % 117.10/117.17 cnf(3199,plain, % 117.10/117.17 (~P6(x31991,f16(a10))), % 117.10/117.17 inference(scs_inference,[],[3022,2474,3058,3105,3107,3136,3111,2852,3132,3135,2919,768,2732,34,86,35,48,59,61,67,64,66,65,57,58,53,62,63,9,8,6,124,7,54,2,69,68,3,84,80,12,14,13,16])). % 117.10/117.17 cnf(3201,plain, % 117.10/117.17 (E(f7(f16(a8)),f7(a1))), % 117.10/117.17 inference(scs_inference,[],[3022,2474,3058,3105,3107,3136,3111,2852,3132,3135,2919,768,2732,34,86,35,48,59,61,67,64,66,65,57,58,53,62,63,9,8,6,124,7,54,2,69,68,3,84,80,12,14,13,16,4,5])). % 117.10/117.17 cnf(3204,plain, % 117.10/117.17 (~E(f7(f9(a14)),f13(a14))), % 117.10/117.17 inference(scs_inference,[],[3022,2474,3058,3105,3107,3136,3111,2852,3132,3135,2919,768,2732,34,86,35,48,59,61,67,64,66,65,57,58,53,62,63,9,8,6,124,7,54,2,69,68,3,84,80,12,14,13,16,4,5,10,11,102])). % 117.10/117.17 cnf(3214,plain, % 117.10/117.17 (P1(f18(a10))), % 117.10/117.17 inference(scs_inference,[],[3080,28,61,59])). % 117.10/117.17 cnf(3220,plain, % 117.10/117.17 (P1(f16(f12(x32201)))), % 117.10/117.17 inference(scs_inference,[],[3080,28,46,35,61,59,66,67,57])). % 117.10/117.17 cnf(3222,plain, % 117.10/117.17 (P1(f17(a10))), % 117.10/117.17 inference(scs_inference,[],[3080,28,46,35,61,59,66,67,57,58])). % 117.10/117.17 cnf(3224,plain, % 117.10/117.17 (E(f18(f16(a8)),a1)), % 117.10/117.17 inference(scs_inference,[],[3080,3155,28,46,35,61,59,66,67,57,58,53])). % 117.10/117.17 cnf(3228,plain, % 117.10/117.17 (P4(f18(a8))), % 117.10/117.17 inference(scs_inference,[],[3080,3155,28,27,46,35,61,59,66,67,57,58,53,62,63])). % 117.10/117.17 cnf(3238,plain, % 117.10/117.17 (~E(a1,f9(a14))), % 117.10/117.17 inference(scs_inference,[],[3151,3080,3122,3182,3194,3171,3155,3190,2894,768,28,27,46,35,61,59,66,67,57,58,53,62,63,124,54,2,69,68,3])). % 117.10/117.17 cnf(3239,plain, % 117.10/117.17 (P6(f7(f9(a5)),a5)), % 117.10/117.17 inference(scs_inference,[],[3151,3080,3122,3182,3194,3171,3155,2845,3190,2894,2239,768,28,27,46,35,61,59,66,67,57,58,53,62,63,124,54,2,69,68,3,80])). % 117.10/117.17 cnf(3241,plain, % 117.10/117.17 (~E(f16(a10),f9(f18(a11)))), % 117.10/117.17 inference(scs_inference,[],[3151,3080,3122,3182,3194,3171,2899,3155,2845,3190,2894,2239,768,3048,28,27,46,35,61,59,66,67,57,58,53,62,63,124,54,2,69,68,3,80,12])). % 117.10/117.17 cnf(3242,plain, % 117.10/117.17 (P4(f15(a1))), % 117.10/117.17 inference(scs_inference,[],[3151,3080,3122,3182,3194,3171,2899,2924,3155,2845,3190,2976,2894,2239,768,3048,28,27,46,35,61,59,66,67,57,58,53,62,63,124,54,2,69,68,3,80,12,17])). % 117.10/117.17 cnf(3243,plain, % 117.10/117.17 (~E(f13(f13(a14)),f9(a14))), % 117.10/117.17 inference(scs_inference,[],[3151,3080,3122,3182,3192,3194,3171,2899,2924,3155,2845,3190,2976,2894,2239,2818,768,3048,28,27,46,35,61,59,66,67,57,58,53,62,63,124,54,2,69,68,3,80,12,17,14])). % 117.10/117.17 cnf(3245,plain, % 117.10/117.17 (P2(f7(a1),f15(a8))), % 117.10/117.17 inference(scs_inference,[],[3151,3080,3122,3182,3192,3194,3171,3081,3201,2899,2924,3155,2845,3190,2976,2894,2239,2818,768,3048,28,27,46,35,61,59,66,67,57,58,53,62,63,124,54,2,69,68,3,80,12,17,14,13])). % 117.10/117.17 cnf(3248,plain, % 117.10/117.17 (~E(f13(f16(a1)),f16(a10))), % 117.10/117.17 inference(scs_inference,[],[3151,3199,3080,3122,3182,3192,3194,3171,3081,3159,3201,2899,2924,3155,2845,3190,2976,1078,2894,2239,2818,768,3048,28,47,27,46,35,61,59,66,67,57,58,53,62,63,124,54,2,69,68,3,80,12,17,14,13,19,16])). % 117.10/117.17 cnf(3254,plain, % 117.10/117.17 (~P2(f13(f16(a1)),f13(a10))), % 117.10/117.17 inference(scs_inference,[],[3151,3199,3080,3122,3182,3192,3194,3171,3081,3159,3201,2899,2924,3155,2845,3190,2976,1078,2894,2239,2818,768,3048,28,47,27,46,35,61,59,66,67,57,58,53,62,63,124,54,2,69,68,3,80,12,17,14,13,19,16,82,72,84])). % 117.10/117.17 cnf(3258,plain, % 117.10/117.17 (P1(f18(f18(a10)))), % 117.10/117.17 inference(scs_inference,[],[3214,59])). % 117.10/117.17 cnf(3262,plain, % 117.10/117.17 (P1(f16(f18(a10)))), % 117.10/117.17 inference(scs_inference,[],[3214,3228,59,61,57])). % 117.10/117.17 cnf(3264,plain, % 117.10/117.17 (P1(f17(f18(a10)))), % 117.10/117.17 inference(scs_inference,[],[3214,3228,59,61,57,58])). % 117.10/117.17 cnf(3266,plain, % 117.10/117.17 (E(f18(a10),a1)), % 117.10/117.17 inference(scs_inference,[],[3214,3228,59,61,57,58,53])). % 117.10/117.17 cnf(3273,plain, % 117.10/117.17 (E(f13(f18(a10)),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[3214,3222,3228,59,61,57,58,53,62,63,9,6])). % 117.10/117.17 cnf(3276,plain, % 117.10/117.17 (E(f16(f18(a10)),f16(a1))), % 117.10/117.17 inference(scs_inference,[],[3214,3222,3228,3254,59,61,57,58,53,62,63,9,6,8,124,7])). % 117.10/117.17 cnf(3277,plain, % 117.10/117.17 (P3(f18(a10))), % 117.10/117.17 inference(scs_inference,[],[3214,3222,3228,3254,59,61,57,58,53,62,63,9,6,8,124,7,54])). % 117.10/117.17 cnf(3285,plain, % 117.10/117.17 (~P2(a5,f13(f18(a10)))), % 117.10/117.17 inference(scs_inference,[],[2532,3214,3222,3228,3254,3239,3181,3058,3088,830,828,59,61,57,58,53,62,63,9,6,8,124,7,54,2,69,68,3,84])). % 117.10/117.17 cnf(3287,plain, % 117.10/117.17 (~P2(f13(a5),f16(f16(a5)))), % 117.10/117.17 inference(scs_inference,[],[2532,3214,3222,3228,3254,3239,3181,3147,2225,3058,3088,830,828,59,61,57,58,53,62,63,9,6,8,124,7,54,2,69,68,3,84,80])). % 117.10/117.17 cnf(3289,plain, % 117.10/117.17 (~E(f18(a10),f17(f15(a5)))), % 117.10/117.17 inference(scs_inference,[],[2532,3214,3222,3228,3254,2956,3239,3181,3147,2225,3058,3088,830,828,59,61,57,58,53,62,63,9,6,8,124,7,54,2,69,68,3,84,80,12])). % 117.10/117.17 cnf(3290,plain, % 117.10/117.17 (P5(f15(a1))), % 117.10/117.17 inference(scs_inference,[],[2532,3214,3222,3228,3254,2956,3239,3181,3147,2225,314,3058,3088,830,828,59,61,57,58,53,62,63,9,6,8,124,7,54,2,69,68,3,84,80,12,21])). % 117.10/117.17 cnf(3291,plain, % 117.10/117.17 (P7(f15(a1))), % 117.10/117.17 inference(scs_inference,[],[2532,3214,3222,3228,3254,2956,3239,3181,3147,2225,255,314,3058,3088,830,828,59,61,57,58,53,62,63,9,6,8,124,7,54,2,69,68,3,84,80,12,21,22])). % 117.10/117.17 cnf(3292,plain, % 117.10/117.17 (~P2(f13(a14),f13(f16(a8)))), % 117.10/117.17 inference(scs_inference,[],[2532,3214,3222,3228,3254,2956,3239,3179,3181,3147,2225,255,314,3058,3136,3088,830,828,59,61,57,58,53,62,63,9,6,8,124,7,54,2,69,68,3,84,80,12,21,22,14])). % 117.10/117.17 cnf(3293,plain, % 117.10/117.17 (~P2(f13(a1),f13(a10))), % 117.10/117.17 inference(scs_inference,[],[2532,3214,3222,3228,3254,2956,3239,3179,3181,3147,2225,255,314,3058,2830,3136,3088,830,828,59,61,57,58,53,62,63,9,6,8,124,7,54,2,69,68,3,84,80,12,21,22,14,13])). % 117.10/117.17 cnf(3295,plain, % 117.10/117.17 (E(f12(f18(a10)),f12(a1))), % 117.10/117.17 inference(scs_inference,[],[2532,3214,3222,3228,3254,2956,3224,3239,3179,3181,3147,2225,255,314,3058,2830,3136,3088,830,828,86,59,61,57,58,53,62,63,9,6,8,124,7,54,2,69,68,3,84,80,12,21,22,14,13,16,4])). % 117.10/117.17 cnf(3297,plain, % 117.10/117.17 (E(f15(f18(a10)),f15(a1))), % 117.10/117.17 inference(scs_inference,[],[2532,3214,3222,3228,3254,2956,3224,3239,3179,3181,3147,2225,255,314,3058,2830,3136,3088,830,828,86,59,61,57,58,53,62,63,9,6,8,124,7,54,2,69,68,3,84,80,12,21,22,14,13,16,4,5,10])). % 117.10/117.17 cnf(3309,plain, % 117.10/117.17 (P1(f18(f17(a10)))), % 117.10/117.17 inference(scs_inference,[],[3222,59])). % 117.10/117.17 cnf(3311,plain, % 117.10/117.17 (P4(f16(a6))), % 117.10/117.17 inference(scs_inference,[],[3222,40,59,61])). % 117.10/117.17 cnf(3313,plain, % 117.10/117.17 (P1(f16(f17(a10)))), % 117.10/117.17 inference(scs_inference,[],[3222,40,59,61,57])). % 117.10/117.17 cnf(3315,plain, % 117.10/117.17 (P1(f17(f17(a10)))), % 117.10/117.17 inference(scs_inference,[],[3222,40,59,61,57,58])). % 117.10/117.17 cnf(3321,plain, % 117.10/117.17 (~E(f12(a10),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[3293,3258,3222,40,46,59,61,57,58,53,63,124])). % 117.10/117.17 cnf(3325,plain, % 117.10/117.17 (P4(f15(a8))), % 117.10/117.17 inference(scs_inference,[],[2418,3293,3258,3222,219,40,2916,46,59,61,57,58,53,63,124,54,2,69])). % 117.10/117.17 cnf(3330,plain, % 117.10/117.17 (~P2(a11,f13(f17(a10)))), % 117.10/117.17 inference(scs_inference,[],[2418,3277,3293,3266,3258,3289,442,3222,3058,219,40,2916,46,59,61,57,58,53,63,124,54,2,69,68,3,84])). % 117.10/117.17 cnf(3332,plain, % 117.10/117.17 (P6(f15(a4),f13(f16(a4)))), % 117.10/117.17 inference(scs_inference,[],[2418,3277,3293,3266,3258,3011,3289,442,3222,3058,219,40,2916,46,52,59,61,57,58,53,63,124,54,2,69,68,3,84,80])). % 117.10/117.17 cnf(3336,plain, % 117.10/117.17 (~E(f13(f13(a1)),f13(a10))), % 117.10/117.17 inference(scs_inference,[],[2418,3277,3293,3266,2972,3258,3011,3289,442,3222,3058,219,2818,40,2916,46,52,59,61,57,58,53,63,124,54,2,69,68,3,84,80,12,14])). % 117.10/117.17 cnf(3338,plain, % 117.10/117.17 (~P2(f13(f18(a10)),f13(a10))), % 117.10/117.17 inference(scs_inference,[],[2418,3277,3293,3266,3273,2972,3258,3011,3289,442,3222,3058,219,2818,40,2916,46,52,59,61,57,58,53,63,124,54,2,69,68,3,84,80,12,14,13])). % 117.10/117.17 cnf(3345,plain, % 117.10/117.17 (~P6(f13(f16(a4)),f15(a4))), % 117.10/117.17 inference(scs_inference,[],[2418,3277,3293,3266,3273,782,3140,2972,3085,3258,3011,3289,3220,442,3222,3058,219,2818,40,2916,46,52,59,61,57,58,53,63,124,54,2,69,68,3,84,80,12,14,13,16,70,82])). % 117.10/117.17 cnf(3352,plain, % 117.10/117.17 (P1(f18(a8))), % 117.10/117.17 inference(scs_inference,[],[27,59])). % 117.10/117.17 cnf(3356,plain, % 117.10/117.17 (P1(f16(f18(a8)))), % 117.10/117.17 inference(scs_inference,[],[3311,27,59,61,57])). % 117.10/117.17 cnf(3358,plain, % 117.10/117.17 (~E(f18(a1),f17(a5))), % 117.10/117.17 inference(scs_inference,[],[2525,3311,27,59,61,57,2])). % 117.10/117.17 cnf(3359,plain, % 117.10/117.17 (P1(f17(a8))), % 117.10/117.17 inference(scs_inference,[],[2525,3311,27,59,61,57,2,58])). % 117.10/117.17 cnf(3363,plain, % 117.10/117.17 (E(f18(f17(a10)),a1)), % 117.10/117.17 inference(scs_inference,[],[2525,3311,3309,27,59,61,57,2,58,54,53])). % 117.10/117.17 cnf(3376,plain, % 117.10/117.17 (~E(f18(f17(a10)),f18(a5))), % 117.10/117.17 inference(scs_inference,[],[2525,2996,3311,3325,3338,3309,3083,2316,2852,27,59,61,57,2,58,54,53,62,63,124,68,69,13,12])). % 117.10/117.17 cnf(3377,plain, % 117.10/117.17 (P1(f7(f13(a8)))), % 117.10/117.17 inference(scs_inference,[],[2525,2996,3311,3325,3338,3309,3083,2316,2852,139,27,48,59,61,57,2,58,54,53,62,63,124,68,69,13,12,80])). % 117.10/117.17 cnf(3383,plain, % 117.10/117.17 (~P2(f13(a14),f13(f17(a2)))), % 117.10/117.17 inference(scs_inference,[],[2525,2996,3311,3325,3276,3338,3309,3062,3040,3083,2316,2852,3136,2820,256,139,27,48,59,61,57,2,58,54,53,62,63,124,68,69,13,12,80,16,3,14])). % 117.10/117.17 cnf(3394,plain, % 117.10/117.17 (P1(f18(f18(a8)))), % 117.10/117.17 inference(scs_inference,[],[3352,59])). % 117.10/117.17 cnf(3398,plain, % 117.10/117.17 (P1(f16(f17(a8)))), % 117.10/117.17 inference(scs_inference,[],[3352,3359,3325,59,61,57])). % 117.10/117.17 cnf(3401,plain, % 117.10/117.17 (P1(f17(f18(a8)))), % 117.10/117.17 inference(scs_inference,[],[2566,3352,3359,3325,59,61,57,2,58])). % 117.10/117.17 cnf(3403,plain, % 117.10/117.17 (P3(f18(a8))), % 117.10/117.17 inference(scs_inference,[],[2566,3352,3359,3325,59,61,57,2,58,54])). % 117.10/117.17 cnf(3405,plain, % 117.10/117.17 (E(f18(a8),a1)), % 117.10/117.17 inference(scs_inference,[],[2566,3352,3359,3325,59,61,57,2,58,54,53])). % 117.10/117.17 cnf(3412,plain, % 117.10/117.17 (E(f13(f18(a8)),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[2566,3352,3359,3325,59,61,57,2,58,54,53,62,63,9,6])). % 117.10/117.17 cnf(3414,plain, % 117.10/117.17 (P4(f7(f13(a8)))), % 117.10/117.17 inference(scs_inference,[],[2566,3352,3359,3377,3325,59,61,57,2,58,54,53,62,63,9,6,8,55])). % 117.10/117.17 cnf(3419,plain, % 117.10/117.17 (~P2(a5,f13(f18(a8)))), % 117.10/117.17 inference(scs_inference,[],[2566,3352,3359,3377,3383,3228,3239,3325,59,61,57,2,58,54,53,62,63,9,6,8,55,124,68,84])). % 117.10/117.17 cnf(3421,plain, % 117.10/117.17 (P4(f15(a4))), % 117.10/117.17 inference(scs_inference,[],[2566,3352,3359,3377,3383,3228,3239,3325,31,39,59,61,57,2,58,54,53,62,63,9,6,8,55,124,68,84,69])). % 117.10/117.17 cnf(3423,plain, % 117.10/117.17 (P2(f15(a8),f13(f16(a8)))), % 117.10/117.17 inference(scs_inference,[],[2566,3352,3359,3377,3383,3228,3239,3016,3325,31,2818,39,59,61,57,2,58,54,53,62,63,9,6,8,55,124,68,84,69,13])). % 117.10/117.17 cnf(3424,plain, % 117.10/117.17 (P2(x34241,f13(x34241))), % 117.10/117.17 inference(rename_variables,[],[2818])). % 117.10/117.17 cnf(3426,plain, % 117.10/117.17 (P6(f15(a1),f13(f16(a1)))), % 117.10/117.17 inference(scs_inference,[],[2566,3352,3359,3000,3377,3137,3383,3228,3239,3016,3325,31,2818,39,52,59,61,57,2,58,54,53,62,63,9,6,8,55,124,68,84,69,13,12,80])). % 117.10/117.17 cnf(3430,plain, % 117.10/117.17 (~E(a1,f18(a5))), % 117.10/117.17 inference(scs_inference,[],[2566,3352,3359,3345,3376,3000,3377,3137,3383,3363,3228,3239,3016,2945,3325,31,2818,39,52,59,61,57,2,58,54,53,62,63,9,6,8,55,124,68,84,69,13,12,80,16,3])). % 117.10/117.17 cnf(3433,plain, % 117.10/117.17 (E(f16(f18(a8)),f16(a1))), % 117.10/117.17 inference(scs_inference,[],[2566,3352,3359,3345,3376,3000,3377,3137,3383,3363,3330,3228,3239,3016,2945,3325,31,2818,3424,39,52,59,61,57,2,58,54,53,62,63,9,6,8,55,124,68,84,69,13,12,80,16,3,14,7])). % 117.10/117.17 cnf(3436,plain, % 117.10/117.17 (E(f15(f18(a8)),f15(a1))), % 117.10/117.17 inference(scs_inference,[],[2566,3352,3359,3345,3376,3000,3377,3137,3383,3363,3330,3228,3239,3016,2945,3325,31,2818,3424,39,52,59,61,57,2,58,54,53,62,63,9,6,8,55,124,68,84,69,13,12,80,16,3,14,7,4,5,10])). % 117.10/117.17 cnf(3440,plain, % 117.10/117.17 (P3(f15(a4))), % 117.10/117.17 inference(scs_inference,[],[2566,2943,3352,3359,3345,3376,3000,3377,3137,3383,3363,3330,3228,3239,3016,2945,3325,31,2818,3424,39,52,59,61,57,2,58,54,53,62,63,9,6,8,55,124,68,84,69,13,12,80,16,3,14,7,4,5,10,11,82,18])). % 117.10/117.17 cnf(3443,plain, % 117.10/117.17 (~P6(f13(a1),f15(a1))), % 117.10/117.17 inference(scs_inference,[],[2566,2943,3352,3359,3345,3376,3000,3377,3137,3383,3363,3330,3038,3228,3239,3016,2945,3325,2830,31,2818,3424,39,52,59,61,57,2,58,54,53,62,63,9,6,8,55,124,68,84,69,13,12,80,16,3,14,7,4,5,10,11,82,18,71,15])). % 117.10/117.17 cnf(3446,plain, % 117.10/117.17 (P1(f18(f17(a8)))), % 117.10/117.17 inference(scs_inference,[],[3359,59])). % 117.10/117.17 cnf(3448,plain, % 117.10/117.17 (P4(f16(a4))), % 117.10/117.17 inference(scs_inference,[],[3359,39,59,61])). % 117.10/117.17 cnf(3451,plain, % 117.10/117.17 (P1(f17(f17(a8)))), % 117.10/117.17 inference(scs_inference,[],[2530,3359,39,59,61,2,58])). % 117.10/117.17 cnf(3462,plain, % 117.10/117.17 (~P2(f13(f16(a1)),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[2530,3421,3440,3356,3426,3419,3359,39,25,59,61,2,58,54,53,124,68,69,84])). % 117.10/117.17 cnf(3464,plain, % 117.10/117.17 (~E(f15(a8),f13(a14))), % 117.10/117.17 inference(scs_inference,[],[2530,3421,3440,3356,3423,3426,3419,3292,3359,39,25,59,61,2,58,54,53,124,68,69,84,13])). % 117.10/117.17 cnf(3465,plain, % 117.10/117.17 (~E(f16(f18(a8)),f18(a5))), % 117.10/117.17 inference(scs_inference,[],[2530,3421,3440,3356,3423,3426,3419,3292,2321,3359,39,25,59,61,2,58,54,53,124,68,69,84,13,12])). % 117.10/117.17 cnf(3466,plain, % 117.10/117.17 (P1(f7(f13(a10)))), % 117.10/117.17 inference(scs_inference,[],[2530,3421,3440,3356,3423,3426,3419,3292,2321,3359,39,172,25,48,59,61,2,58,54,53,124,68,69,84,13,12,80])). % 117.10/117.17 cnf(3470,plain, % 117.10/117.17 (~P6(x34701,f18(a8))), % 117.10/117.17 inference(scs_inference,[],[2530,3421,3440,3405,3356,3423,3426,3419,3292,2321,3359,39,172,86,25,48,59,61,2,58,54,53,124,68,69,84,13,12,80,16])). % 117.10/117.17 cnf(3481,plain, % 117.10/117.17 (P1(f18(f12(x34811)))), % 117.10/117.17 inference(scs_inference,[],[46,59])). % 117.10/117.17 cnf(3486,plain, % 117.10/117.17 (P1(f17(a1))), % 117.10/117.17 inference(scs_inference,[],[2559,3448,25,46,59,61,2,58])). % 117.10/117.17 cnf(3490,plain, % 117.10/117.17 (E(f18(f17(a8)),a1)), % 117.10/117.17 inference(scs_inference,[],[2559,3448,3446,25,46,59,61,2,58,54,53])). % 117.10/117.17 cnf(3494,plain, % 117.10/117.17 (P4(f17(f17(a1)))), % 117.10/117.17 inference(scs_inference,[],[2559,3448,3446,25,46,59,61,2,58,54,53,63,62])). % 117.10/117.17 cnf(3496,plain, % 117.10/117.17 (P4(f7(f13(a10)))), % 117.10/117.17 inference(scs_inference,[],[2559,3448,3446,3466,25,46,59,61,2,58,54,53,63,62,55])). % 117.10/117.17 cnf(3503,plain, % 117.10/117.17 (P2(f15(a10),f13(f16(a10)))), % 117.10/117.17 inference(scs_inference,[],[2559,3403,3448,3462,3446,3466,2943,2787,3228,2818,25,46,59,61,2,58,54,53,63,62,55,124,68,69,13])). % 117.10/117.17 cnf(3504,plain, % 117.10/117.17 (P2(x35041,f13(x35041))), % 117.10/117.17 inference(rename_variables,[],[2818])). % 117.10/117.17 cnf(3506,plain, % 117.10/117.17 (P6(f15(a8),f13(f16(a8)))), % 117.10/117.17 inference(scs_inference,[],[2559,3403,3448,3462,3046,3446,3466,2943,3423,2787,3228,3359,2818,25,46,52,59,61,2,58,54,53,63,62,55,124,68,69,13,12,80])). % 117.10/117.17 cnf(3516,plain, % 117.10/117.17 (P2(f12(a1),f13(f18(a10)))), % 117.10/117.17 inference(scs_inference,[],[3470,2559,3403,3448,3295,3433,3462,3465,3046,3446,3466,3119,3285,2968,2943,3443,3423,2787,3228,3359,110,2818,3504,25,46,52,59,61,2,58,54,53,63,62,55,124,68,69,13,12,80,19,16,3,15,14,81])). % 117.10/117.17 cnf(3518,plain, % 117.10/117.17 (P1(f16(f17(a1)))), % 117.10/117.17 inference(scs_inference,[],[3470,2559,3403,3448,3295,3433,3462,3465,3046,3446,3466,3119,3285,2968,2943,3443,3423,2787,3228,3359,110,2818,3504,25,46,52,59,61,2,58,54,53,63,62,55,124,68,69,13,12,80,19,16,3,15,14,81,57])). % 117.10/117.17 cnf(3520,plain, % 117.10/117.17 (~P6(f13(f16(a8)),f15(a8))), % 117.10/117.17 inference(scs_inference,[],[3470,2559,3403,3448,3295,3433,3462,3465,3046,3446,3466,3119,3285,2968,2943,3443,3423,2787,3228,3359,110,2818,3504,25,46,52,59,61,2,58,54,53,63,62,55,124,68,69,13,12,80,19,16,3,15,14,81,57,82])). % 117.10/117.17 cnf(3526,plain, % 117.10/117.17 (P1(f18(f17(a1)))), % 117.10/117.17 inference(scs_inference,[],[3486,59])). % 117.10/117.17 cnf(3528,plain, % 117.10/117.17 (P4(f16(a3))), % 117.10/117.17 inference(scs_inference,[],[3486,35,59,61])). % 117.10/117.17 cnf(3530,plain, % 117.10/117.17 (P1(f17(f17(a1)))), % 117.10/117.17 inference(scs_inference,[],[3486,35,59,61,58])). % 117.10/117.17 cnf(3532,plain, % 117.10/117.17 (P3(f17(a1))), % 117.10/117.17 inference(scs_inference,[],[3486,35,59,61,58,54])). % 117.10/117.17 cnf(3535,plain, % 117.10/117.17 (E(f17(a1),a1)), % 117.10/117.17 inference(scs_inference,[],[2564,3486,35,59,61,58,54,2,53])). % 117.10/117.17 cnf(3537,plain, % 117.10/117.17 (E(f17(f17(a1)),f17(a1))), % 117.10/117.17 inference(scs_inference,[],[2564,3486,35,59,61,58,54,2,53,9])). % 117.10/117.17 cnf(3538,plain, % 117.10/117.17 (E(f13(f17(a1)),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[2564,3486,35,59,61,58,54,2,53,9,6])). % 117.10/117.17 cnf(3539,plain, % 117.10/117.17 (E(f9(f17(a1)),f9(a1))), % 117.10/117.17 inference(scs_inference,[],[2564,3486,35,59,61,58,54,2,53,9,6,8])). % 117.10/117.17 cnf(3541,plain, % 117.10/117.17 (~P2(f13(a14),f13(f17(a1)))), % 117.10/117.17 inference(scs_inference,[],[2564,3486,3130,3005,35,59,61,58,54,2,53,9,6,8,124,84])). % 117.10/117.17 cnf(3543,plain, % 117.10/117.17 (P3(f15(a10))), % 117.10/117.17 inference(scs_inference,[],[2564,3486,3130,3005,30,37,35,59,61,58,54,2,53,9,6,8,124,84,68])). % 117.10/117.17 cnf(3547,plain, % 117.10/117.17 (~P2(f13(a1),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[2564,3486,3130,3462,2935,3005,30,2830,37,35,59,61,58,54,2,53,9,6,8,124,84,68,69,13])). % 117.10/117.17 cnf(3548,plain, % 117.10/117.17 (~E(f17(a1),f9(f9(a14)))), % 117.10/117.17 inference(scs_inference,[],[2564,3486,3165,3130,3462,2935,3005,30,2830,37,35,59,61,58,54,2,53,9,6,8,124,84,68,69,13,12])). % 117.10/117.17 cnf(3549,plain, % 117.10/117.17 (P1(f7(f13(a2)))), % 117.10/117.17 inference(scs_inference,[],[2564,3486,3165,3130,3462,2935,3005,30,2830,37,197,35,48,59,61,58,54,2,53,9,6,8,124,84,68,69,13,12,80])). % 117.10/117.17 cnf(3551,plain, % 117.10/117.17 (P2(f7(x35511),x35511)), % 117.10/117.17 inference(rename_variables,[],[48])). % 117.10/117.17 cnf(3560,plain, % 117.10/117.17 (E(f12(f17(a1)),f12(a1))), % 117.10/117.17 inference(scs_inference,[],[2770,2564,3290,3291,3486,3165,3490,2812,3130,3462,2935,3005,3266,30,2830,37,197,86,35,1222,48,3551,59,61,58,54,2,53,9,6,8,124,84,68,69,13,12,80,16,3,21,22,14,7,4])). % 117.10/117.17 cnf(3561,plain, % 117.10/117.17 (E(f7(f17(a1)),f7(a1))), % 117.10/117.17 inference(scs_inference,[],[2770,2564,3290,3291,3486,3165,3490,2812,3130,3462,2935,3005,3266,30,2830,37,197,86,35,1222,48,3551,59,61,58,54,2,53,9,6,8,124,84,68,69,13,12,80,16,3,21,22,14,7,4,5])). % 117.10/117.17 cnf(3562,plain, % 117.10/117.17 (E(f15(f17(a1)),f15(a1))), % 117.10/117.17 inference(scs_inference,[],[2770,2564,3290,3291,3486,3165,3490,2812,3130,3462,2935,3005,3266,30,2830,37,197,86,35,1222,48,3551,59,61,58,54,2,53,9,6,8,124,84,68,69,13,12,80,16,3,21,22,14,7,4,5,10])). % 117.10/117.17 cnf(3563,plain, % 117.10/117.17 (E(f18(f17(a1)),f18(a1))), % 117.10/117.17 inference(scs_inference,[],[2770,2564,3290,3291,3486,3165,3490,2812,3130,3462,2935,3005,3266,30,2830,37,197,86,35,1222,48,3551,59,61,58,54,2,53,9,6,8,124,84,68,69,13,12,80,16,3,21,22,14,7,4,5,10,11])). % 117.10/117.17 cnf(3575,plain, % 117.10/117.17 (P1(f18(f18(a1)))), % 117.10/117.17 inference(scs_inference,[],[817,59])). % 117.10/117.17 cnf(3581,plain, % 117.10/117.17 (P1(f17(f12(x35811)))), % 117.10/117.17 inference(scs_inference,[],[3528,3526,46,817,59,61,54,58])). % 117.10/117.17 cnf(3589,plain, % 117.10/117.17 (~P2(f13(f16(a8)),f13(a2))), % 117.10/117.17 inference(scs_inference,[],[2480,3528,3547,3526,3549,3506,26,46,817,59,61,54,58,2,53,55,124,84])). % 117.10/117.17 cnf(3595,plain, % 117.10/117.17 (~P2(f13(f17(a1)),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[2480,3528,3543,3547,3538,3526,3549,3506,3080,26,46,817,59,61,54,58,2,53,55,124,84,68,69,13])). % 117.10/117.17 cnf(3597,plain, % 117.10/117.17 (P6(f12(a1),f13(f18(a10)))), % 117.10/117.17 inference(scs_inference,[],[2480,3528,3543,3547,3538,3516,3526,3549,3506,2365,3080,3486,26,46,52,817,59,61,54,58,2,53,55,124,84,68,69,13,12,80])). % 117.10/117.17 cnf(3602,plain, % 117.10/117.17 (~P2(f13(a1),f13(f17(a1)))), % 117.10/117.17 inference(scs_inference,[],[2480,3528,3543,3547,3535,3520,3538,3516,3526,3549,3548,3506,2365,3080,3016,3486,26,46,52,817,59,61,54,58,2,53,55,124,84,68,69,13,12,80,16,3,14])). % 117.10/117.17 cnf(3613,plain, % 117.10/117.17 (E(f17(f12(x36131)),a1)), % 117.10/117.17 inference(scs_inference,[],[3129,3581,54,2,53])). % 117.10/117.17 cnf(3622,plain, % 117.10/117.17 (~E(f17(f12(x36221)),f16(a5))), % 117.10/117.17 inference(scs_inference,[],[3129,3532,3589,3581,3541,2236,647,2943,2935,3448,54,2,53,124,68,69,13,12])). % 117.10/117.17 cnf(3641,plain, % 117.10/117.17 (~E(f13(a14),f15(a8))), % 117.10/117.17 inference(scs_inference,[],[3464,3530,54,2])). % 117.10/117.17 cnf(3642,plain, % 117.10/117.17 (E(f17(f17(a1)),a1)), % 117.10/117.17 inference(scs_inference,[],[3464,3530,54,2,53])). % 117.10/117.17 cnf(3645,plain, % 117.10/117.17 (P3(f15(a1))), % 117.10/117.17 inference(scs_inference,[],[3464,3595,3530,308,34,54,2,53,124,68])). % 117.10/117.17 cnf(3650,plain, % 117.10/117.17 (P2(f15(a1),f13(x36501))), % 117.10/117.17 inference(scs_inference,[],[3464,3595,3530,2990,597,308,1090,3088,34,54,2,53,124,68,69,13])). % 117.10/117.17 cnf(3652,plain, % 117.10/117.17 (~E(f13(f18(a10)),f16(a10))), % 117.10/117.17 inference(scs_inference,[],[3464,3595,3530,3597,2311,3199,2990,597,308,1090,3088,3352,34,54,2,53,124,68,69,13,12,16])). % 117.10/117.17 cnf(3659,plain, % 117.10/117.17 (P5(f17(f17(a1)))), % 117.10/117.17 inference(scs_inference,[],[3464,3622,3595,3494,3613,3530,3597,3287,2311,3290,3199,3242,2990,597,308,1090,3088,3352,34,1219,54,2,53,124,68,69,13,12,16,3,14,77,70])). % 117.10/117.17 cnf(3675,plain, % 117.10/117.17 (E(f18(f18(a1)),a1)), % 117.10/117.17 inference(scs_inference,[],[2926,3575,54,2,53])). % 117.10/117.17 cnf(3683,plain, % 117.10/117.17 (P2(f15(a1),f13(x36831))), % 117.10/117.17 inference(rename_variables,[],[3650])). % 117.10/117.17 cnf(3684,plain, % 117.10/117.17 (~E(f18(f18(a1)),f18(a5))), % 117.10/117.17 inference(scs_inference,[],[3650,3645,2926,3575,3602,3338,2400,3242,54,2,53,124,69,68,13,12])). % 117.10/117.17 cnf(3685,plain, % 117.10/117.17 (~P6(x36851,f18(f17(a1)))), % 117.10/117.17 inference(scs_inference,[],[3650,3645,2926,3563,3575,3602,3338,2400,3242,819,54,2,53,124,69,68,13,12,16])). % 117.10/117.17 cnf(3691,plain, % 117.10/117.17 (~P2(f13(f16(a4)),f13(a10))), % 117.10/117.17 inference(scs_inference,[],[2921,3650,3645,2926,3563,3575,3602,3332,3338,2400,3171,3242,298,28,819,1222,48,54,2,53,124,69,68,13,12,16,3,14,71,84])). % 117.10/117.17 cnf(3693,plain, % 117.10/117.17 (P6(f15(a1),f13(x36931))), % 117.10/117.17 inference(scs_inference,[],[2921,3650,3683,3645,2926,3563,3575,3602,3332,3338,2400,3171,3242,298,28,819,52,1222,48,54,2,53,124,69,68,13,12,16,3,14,71,84,80])). % 117.10/117.17 cnf(3714,plain, % 117.10/117.17 (~P6(f13(x37141),f15(a1))), % 117.10/117.17 inference(scs_inference,[],[3693,3072,3481,54,53,2,82])). % 117.10/117.17 cnf(3717,plain, % 117.10/117.17 (P3(f15(a3))), % 117.10/117.17 inference(scs_inference,[],[3693,3072,3691,3481,29,35,54,53,2,82,124,68])). % 117.10/117.17 cnf(3719,plain, % 117.10/117.17 (P4(f15(a3))), % 117.10/117.17 inference(scs_inference,[],[3693,3072,3691,3481,29,35,54,53,2,82,124,68,69])). % 117.10/117.17 cnf(3721,plain, % 117.10/117.17 (P2(f15(f16(a1)),f13(x37211))), % 117.10/117.17 inference(scs_inference,[],[3693,3072,3691,3481,3650,2812,29,35,54,53,2,82,124,68,69,13])). % 117.10/117.17 cnf(3723,plain, % 117.10/117.17 (P8(f17(a1),f17(f17(a1)))), % 117.10/117.17 inference(scs_inference,[],[3693,3072,3537,3691,3481,2312,3650,2812,3359,47,29,35,54,53,2,82,124,68,69,13,12,19])). % 117.10/117.17 cnf(3727,plain, % 117.10/117.17 (~E(a1,f17(a5))), % 117.10/117.17 inference(scs_inference,[],[3693,3072,3537,3079,3691,3685,3481,3054,2312,3650,2812,3359,47,29,35,54,53,2,82,124,68,69,13,12,19,16,3])). % 117.10/117.17 cnf(3743,plain, % 117.10/117.17 (E(f17(f17(a8)),a1)), % 117.10/117.17 inference(scs_inference,[],[3451,54,53])). % 117.10/117.17 cnf(3751,plain, % 117.10/117.17 (~E(f15(f16(a1)),f13(a14))), % 117.10/117.17 inference(scs_inference,[],[3717,3719,3238,3721,3451,3541,54,53,2,124,68,69,13])). % 117.10/117.17 cnf(3753,plain, % 117.10/117.17 (~E(f17(f17(a8)),f18(a5))), % 117.10/117.17 inference(scs_inference,[],[3717,3719,3238,3721,3451,3541,2336,54,53,2,124,68,69,13,12])). % 117.10/117.17 cnf(3758,plain, % 117.10/117.17 (P8(f17(a1),a1)), % 117.10/117.17 inference(scs_inference,[],[3430,3714,3717,3719,3238,3562,3721,3723,3642,3451,404,3541,2336,266,2834,2815,514,54,53,2,124,68,69,13,12,16,3,21,14,20])). % 117.10/117.17 cnf(3769,plain, % 117.10/117.17 (P2(f17(a1),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[3758,3330,124,81])). % 117.10/117.17 cnf(3776,plain, % 117.10/117.17 (~E(f13(f13(a11)),f9(a11))), % 117.10/117.17 inference(scs_inference,[],[3758,2523,3518,3330,346,2818,124,81,54,53,2,14])). % 117.10/117.17 cnf(3781,plain, % 117.10/117.17 (~E(f15(a1),f13(a14))), % 117.10/117.17 inference(scs_inference,[],[3245,3758,2523,3751,3297,3518,2742,2317,3714,3330,3222,346,2818,1149,124,81,54,53,2,14,13,12,16,3])). % 117.10/117.17 cnf(3798,plain, % 117.10/117.17 (~E(f13(a14),f15(a1))), % 117.10/117.17 inference(scs_inference,[],[3781,3394,3292,124,54,53,2])). % 117.10/117.17 cnf(3799,plain, % 117.10/117.17 (P3(a2)), % 117.10/117.17 inference(scs_inference,[],[3781,3014,3042,3394,3292,124,54,53,2,18])). % 117.10/117.17 cnf(3800,plain, % 117.10/117.17 (~P2(f13(f18(a10)),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[25,3781,3014,3042,3394,3292,3597,124,54,53,2,18,84])). % 117.10/117.17 cnf(3832,plain, % 117.10/117.17 (~P2(f13(f16(a8)),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[25,2553,3800,3398,3506,124,54,53,2,84])). % 117.10/117.17 cnf(3834,plain, % 117.10/117.17 (~P2(f13(a1),f13(f16(a1)))), % 117.10/117.17 inference(scs_inference,[],[25,2553,3800,3398,2764,3506,3547,124,54,53,2,84,14])). % 117.10/117.17 cnf(3864,plain, % 117.10/117.17 (~P2(f13(f16(a4)),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[25,3204,3832,3401,3332,124,54,53,2,84])). % 117.10/117.17 cnf(3868,plain, % 117.10/117.17 (P6(f15(a10),f13(f16(a10)))), % 117.10/117.17 inference(scs_inference,[],[25,3204,3832,3503,3401,3332,2945,52,48,124,54,53,2,84,14,80])). % 117.10/117.17 cnf(3874,plain, % 117.10/117.17 (~E(f18(f16(a1)),f17(a5))), % 117.10/117.17 inference(scs_inference,[],[25,3358,3204,3832,3503,3675,3401,2291,3769,3332,2945,2815,86,52,48,124,54,53,2,84,14,80,13,12,16,3])). % 117.10/117.17 cnf(3875,plain, % 117.10/117.17 (~P6(f13(a1),f15(f16(a1)))), % 117.10/117.17 inference(scs_inference,[],[25,3358,3204,3832,3503,3834,3675,3401,2291,3769,3721,3332,2945,2815,86,52,48,124,54,53,2,84,14,80,13,12,16,3,85])). % 117.10/117.17 cnf(3892,plain, % 117.10/117.17 (P3(f16(f17(a10)))), % 117.10/117.17 inference(scs_inference,[],[3864,3313,124,54])). % 117.10/117.17 cnf(3897,plain, % 117.10/117.17 (~P2(f13(f16(a10)),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[25,2851,3864,3868,3313,124,54,53,2,84])). % 117.10/117.17 cnf(3899,plain, % 117.10/117.17 (~P2(f13(a1),f13(f18(a10)))), % 117.10/117.17 inference(scs_inference,[],[25,2851,3864,3868,3313,3273,3547,124,54,53,2,84,14])). % 117.10/117.17 cnf(3902,plain, % 117.10/117.17 (P2(f17(f16(a1)),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[25,3539,2851,3864,3868,3313,3273,2828,3769,3547,47,124,54,53,2,84,14,19,13])). % 117.10/117.17 cnf(3905,plain, % 117.10/117.17 (~E(f17(a1),f17(a5))), % 117.10/117.17 inference(scs_inference,[],[25,3539,2851,3864,3874,3868,3436,3163,3313,2305,3273,2828,3769,3714,3547,3352,47,124,54,53,2,84,14,19,13,12,16,3])). % 117.10/117.17 cnf(3920,plain, % 117.10/117.17 (E(f17(f17(a10)),a1)), % 117.10/117.17 inference(scs_inference,[],[3897,3315,124,54,53])). % 117.10/117.17 cnf(3922,plain, % 117.10/117.17 (~E(f17(a5),f17(a1))), % 117.10/117.17 inference(scs_inference,[],[3905,3897,3315,124,54,53,2])). % 117.10/117.17 cnf(3923,plain, % 117.10/117.17 (~P2(f15(a5),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[25,3905,3897,3315,2942,124,54,53,2,84])). % 117.10/117.17 cnf(3925,plain, % 117.10/117.17 (P2(f7(a1),f15(a1))), % 117.10/117.17 inference(scs_inference,[],[25,3905,3897,3315,2942,266,3088,124,54,53,2,84,14])). % 117.10/117.17 cnf(3929,plain, % 117.10/117.17 (P5(f17(a1))), % 117.10/117.17 inference(scs_inference,[],[25,3905,3897,3659,3315,3537,3589,863,2942,3650,266,3088,124,54,53,2,84,14,13,12,21])). % 117.10/117.17 cnf(3932,plain, % 117.10/117.17 (~E(f7(f13(a1)),f15(a5))), % 117.10/117.17 inference(scs_inference,[],[25,2775,3905,3897,3659,3743,3315,3537,3589,863,2942,3650,266,2834,3088,86,124,54,53,2,84,14,13,12,21,16,3,102])). % 117.10/117.17 cnf(3940,plain, % 117.10/117.17 (~E(f12(a1),f15(a5))), % 117.10/117.17 inference(scs_inference,[],[3923,124])). % 117.10/117.17 cnf(3946,plain, % 117.10/117.17 (~P2(f13(f16(a10)),f13(a2))), % 117.10/117.17 inference(scs_inference,[],[3923,3009,3262,3868,26,124,54,53,2,84])). % 117.10/117.17 cnf(3948,plain, % 117.10/117.17 (~P2(f15(a5),f13(f18(a8)))), % 117.10/117.17 inference(scs_inference,[],[3923,3009,3262,3412,3868,26,124,54,53,2,84,14])). % 117.10/117.17 cnf(3949,plain, % 117.10/117.17 (P6(f17(f16(a1)),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[3923,3009,3902,3262,3412,3868,26,52,124,54,53,2,84,14,80])). % 117.10/117.17 cnf(3952,plain, % 117.10/117.17 (P2(f18(a1),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[3923,3009,3902,3262,3412,3159,3868,26,52,124,54,53,2,84,14,80,13])). % 117.10/117.17 cnf(3954,plain, % 117.10/117.17 (~E(f13(f16(a10)),f16(a10))), % 117.10/117.17 inference(scs_inference,[],[25,3923,3009,3902,3262,860,3412,3159,3868,3199,26,52,124,54,53,2,84,14,80,13,12,16])). % 117.10/117.17 cnf(3957,plain, % 117.10/117.17 (~P6(f13(a1),f17(f16(a1)))), % 117.10/117.17 inference(scs_inference,[],[25,3923,3009,3197,3902,2767,3262,860,3412,3159,3868,3199,26,52,124,54,53,2,84,14,80,13,12,16,3,82])). % 117.10/117.17 cnf(3971,plain, % 117.10/117.17 (~E(f15(a5),f12(a1))), % 117.10/117.17 inference(scs_inference,[],[3940,3946,3264,124,54,53,2])). % 117.10/117.17 cnf(3972,plain, % 117.10/117.17 (~P2(f13(x39721),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[25,3940,3946,3264,615,124,54,53,2,84])). % 117.10/117.17 cnf(3977,plain, % 117.10/117.17 (~P6(x39771,f17(f17(a10)))), % 117.10/117.17 inference(scs_inference,[],[25,3925,3940,3946,3948,3920,3264,2736,615,2812,2858,86,124,54,53,2,84,14,13,12,16])). % 117.10/117.17 cnf(3991,plain, % 117.10/117.17 (E(f16(f16(a8)),a1)), % 117.10/117.17 inference(scs_inference,[],[3972,3167,124,54,53])). % 117.10/117.17 cnf(3994,plain, % 117.10/117.17 (~P2(f13(a1),f13(f17(a8)))), % 117.10/117.17 inference(scs_inference,[],[3972,3932,3949,3167,3359,124,54,53,2,84])). % 117.10/117.17 cnf(3996,plain, % 117.10/117.17 (~P2(f13(x39961),f13(f16(a8)))), % 117.10/117.17 inference(scs_inference,[],[3972,3932,3949,3167,3179,3359,124,54,53,2,84,14])). % 117.10/117.17 cnf(3997,plain, % 117.10/117.17 (P2(f18(f16(a1)),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[3972,3952,3932,3949,3167,3179,2815,3359,124,54,53,2,84,14,13])). % 117.10/117.17 cnf(3999,plain, % 117.10/117.17 (~P6(f13(a1),f17(a1))), % 117.10/117.17 inference(scs_inference,[],[3972,3952,3932,3957,3949,3167,2810,3179,2828,2815,3359,124,54,53,2,84,14,13,12,16])). % 117.10/117.17 cnf(4011,plain, % 117.10/117.17 (~P2(a5,f13(a1))), % 117.10/117.17 inference(scs_inference,[],[25,3243,3996,3169,3239,124,54,53,2,84])). % 117.10/117.17 cnf(4013,plain, % 117.10/117.17 (~P2(f13(x40131),f13(f17(a2)))), % 117.10/117.17 inference(scs_inference,[],[25,3243,3996,3169,3062,3972,3239,124,54,53,2,84,14])). % 117.10/117.17 cnf(4014,plain, % 117.10/117.17 (P6(f18(f16(a1)),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[25,3243,3997,3996,3169,3062,3972,3239,52,124,54,53,2,84,14,80])). % 117.10/117.17 cnf(4020,plain, % 117.10/117.17 (~P6(f13(f16(a10)),f17(a1))), % 117.10/117.17 inference(scs_inference,[],[25,3999,3243,3997,3996,3169,2899,3119,3062,2927,2852,3972,3239,52,124,54,53,2,84,14,80,13,12,15])). % 117.10/117.17 cnf(4043,plain, % 117.10/117.17 (~P2(f13(a1),f13(f17(a10)))), % 117.10/117.17 inference(scs_inference,[],[3336,4014,4013,3097,3222,124,54,53,2,84])). % 117.10/117.17 cnf(4045,plain, % 117.10/117.17 (~P2(a5,f13(f16(a2)))), % 117.10/117.17 inference(scs_inference,[],[4011,3336,4014,4013,3097,2988,3222,124,54,53,2,84,14])). % 117.10/117.17 cnf(4046,plain, % 117.10/117.17 (P8(f12(a1),f17(a1))), % 117.10/117.17 inference(scs_inference,[],[4011,3336,4014,4013,3560,3097,2988,110,3222,124,54,53,2,84,14,19])). % 117.10/117.17 cnf(4048,plain, % 117.10/117.17 (~P2(f16(f16(a5)),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[4011,3336,4014,4013,3560,3097,2988,110,3222,1222,124,54,53,2,84,14,19,13])). % 117.10/117.17 cnf(4053,plain, % 117.10/117.17 (~P6(a5,f15(f16(a1)))), % 117.10/117.17 inference(scs_inference,[],[4011,3336,4014,3977,4013,3560,3060,3097,2956,2988,3721,3535,110,3222,1222,124,54,53,2,84,14,19,13,12,16,3,85])). % 117.10/117.17 cnf(4058,plain, % 117.10/117.17 (P2(f12(a1),f13(f17(a1)))), % 117.10/117.17 inference(scs_inference,[],[4011,3336,4014,3977,4013,3560,3115,3060,3097,2956,2988,3721,3535,110,3222,1222,124,54,53,2,84,14,19,13,12,16,3,85,70,81])). % 117.10/117.17 cnf(4077,plain, % 117.10/117.17 (P8(f12(a1),f17(f16(a1)))), % 117.10/117.17 inference(scs_inference,[],[4046,3684,4048,3109,3036,2828,124,54,53,2,20])). % 117.10/117.17 cnf(4078,plain, % 117.10/117.17 (~P2(a11,f13(a1))), % 117.10/117.17 inference(scs_inference,[],[25,4046,3684,4048,3109,3036,442,2828,124,54,53,2,20,84])). % 117.10/117.17 cnf(4085,plain, % 117.10/117.17 (~P6(x40851,f16(f16(a8)))), % 117.10/117.17 inference(scs_inference,[],[25,3929,4046,3684,4048,3991,3109,3036,2972,2914,2776,442,2828,2906,86,48,124,54,53,2,20,84,14,13,12,21,16])). % 117.10/117.17 cnf(4086,plain, % 117.10/117.17 (~P2(f13(a5),f13(f13(a1)))), % 117.10/117.17 inference(scs_inference,[],[25,3929,4046,3684,4048,3991,3109,3036,2972,2914,2776,442,2828,3132,2906,86,48,124,54,53,2,20,84,14,13,12,21,16,85])). % 117.10/117.17 cnf(4098,plain, % 117.10/117.17 (E(a2,a1)), % 117.10/117.17 inference(scs_inference,[],[26,4078,3075,124,54,53])). % 117.10/117.17 cnf(4100,plain, % 117.10/117.17 (E(f17(a2),f17(a1))), % 117.10/117.17 inference(scs_inference,[],[26,4078,3075,124,54,53,9])). % 117.10/117.17 cnf(4102,plain, % 117.10/117.17 (E(f13(a2),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[26,4078,2507,3075,124,54,53,9,2,6])). % 117.10/117.17 cnf(4103,plain, % 117.10/117.17 (E(f9(a2),f9(a1))), % 117.10/117.17 inference(scs_inference,[],[26,4078,2507,3075,124,54,53,9,2,6,8])). % 117.10/117.17 cnf(4104,plain, % 117.10/117.17 (~P2(f13(a1),f13(f18(a8)))), % 117.10/117.17 inference(scs_inference,[],[26,4078,2507,3075,3949,3352,124,54,53,9,2,6,8,84])). % 117.10/117.17 cnf(4106,plain, % 117.10/117.17 (P6(f12(a1),f13(f17(a1)))), % 117.10/117.17 inference(scs_inference,[],[26,4078,2507,4058,3075,3949,3352,52,124,54,53,9,2,6,8,84,80])). % 117.10/117.17 cnf(4110,plain, % 117.10/117.17 (~P2(f16(f16(a11)),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[26,4078,2507,4058,3075,3099,2764,3949,3352,52,124,54,53,9,2,6,8,84,80,14,13])). % 117.10/117.17 cnf(4115,plain, % 117.10/117.17 (E(f16(a2),f16(a1))), % 117.10/117.17 inference(scs_inference,[],[26,4078,2507,4058,4085,2912,3075,3000,3099,2764,3949,3535,3352,52,124,54,53,9,2,6,8,84,80,14,13,12,16,3,7])). % 117.10/117.17 cnf(4116,plain, % 117.10/117.17 (E(f12(a2),f12(a1))), % 117.10/117.17 inference(scs_inference,[],[26,4078,2507,4058,4085,2912,3075,3000,3099,2764,3949,3535,3352,52,124,54,53,9,2,6,8,84,80,14,13,12,16,3,7,4])). % 117.10/117.17 cnf(4117,plain, % 117.10/117.17 (E(f7(a2),f7(a1))), % 117.10/117.17 inference(scs_inference,[],[26,4078,2507,4058,4085,2912,3075,3000,3099,2764,3949,3535,3352,52,124,54,53,9,2,6,8,84,80,14,13,12,16,3,7,4,5])). % 117.10/117.17 cnf(4118,plain, % 117.10/117.17 (E(f15(a2),f15(a1))), % 117.10/117.17 inference(scs_inference,[],[26,4078,2507,4058,4085,2912,3075,3000,3099,2764,3949,3535,3352,52,124,54,53,9,2,6,8,84,80,14,13,12,16,3,7,4,5,10])). % 117.10/117.17 cnf(4119,plain, % 117.10/117.17 (E(f18(a2),f18(a1))), % 117.10/117.17 inference(scs_inference,[],[26,4078,2507,4058,4085,2912,3075,3000,3099,2764,3949,3535,3352,52,124,54,53,9,2,6,8,84,80,14,13,12,16,3,7,4,5,10,11])). % 117.10/117.17 cnf(4135,plain, % 117.10/117.17 (~P2(f13(f17(a1)),f13(a2))), % 117.10/117.17 inference(scs_inference,[],[26,2842,4110,4106,3052,2816,124,54,53,2,84])). % 117.10/117.17 cnf(4141,plain, % 117.10/117.17 (~P6(x41411,f16(a2))), % 117.10/117.17 inference(scs_inference,[],[26,4098,4115,2842,4110,4106,3052,2816,3952,3046,256,48,124,54,53,2,84,14,13,12,16])). % 117.10/117.17 cnf(4150,plain, % 117.10/117.17 (E(f16(f16(a2)),a1)), % 117.10/117.17 inference(scs_inference,[],[4135,2822,2901,124,54,53])). % 117.10/117.17 cnf(4153,plain, % 117.10/117.17 (~P2(f13(f17(a1)),f13(a10))), % 117.10/117.17 inference(scs_inference,[],[2555,4135,2822,2901,4106,28,124,54,53,2,84])). % 117.10/117.17 cnf(4155,plain, % 117.10/117.17 (P6(f18(a1),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[2555,4135,2822,2901,4106,3952,28,52,124,54,53,2,84,80])). % 117.10/117.17 cnf(4159,plain, % 117.10/117.17 (P2(x41591,f13(x41591))), % 117.10/117.17 inference(rename_variables,[],[2818])). % 117.10/117.17 cnf(4160,plain, % 117.10/117.17 (P2(f17(a1),f13(f17(a2)))), % 117.10/117.17 inference(scs_inference,[],[2555,4135,4045,4100,2822,2901,4106,3952,2818,4159,28,52,124,54,53,2,84,80,14,13])). % 117.10/117.17 cnf(4165,plain, % 117.10/117.17 (~E(f17(a1),f15(a5))), % 117.10/117.17 inference(scs_inference,[],[26,4141,2555,4135,4045,4100,2822,2901,3008,3165,4106,3952,2818,4159,28,52,124,54,53,2,84,80,14,13,12,16,3])). % 117.10/117.17 cnf(4183,plain, % 117.10/117.17 (~P2(f13(x41831),f13(a2))), % 117.10/117.17 inference(scs_inference,[],[26,4165,4153,2886,2964,651,124,54,53,2,84])). % 117.10/117.17 cnf(4190,plain, % 117.10/117.17 (~P6(x41901,f16(f16(a2)))), % 117.10/117.17 inference(scs_inference,[],[26,4165,4153,3875,3899,4150,4103,2886,2964,4102,2365,651,86,48,124,54,53,2,84,14,13,15,12,16])). % 117.10/117.17 cnf(4191,plain, % 117.10/117.17 (~E(f17(f18(a1)),f17(a5))), % 117.10/117.17 inference(scs_inference,[],[26,3727,4165,4153,3875,3899,4150,4103,2886,2964,4102,2365,651,514,86,48,124,54,53,2,84,14,13,15,12,16,3])). % 117.10/117.17 cnf(4192,plain, % 117.10/117.17 (~E(f7(f13(a2)),f13(x41921))), % 117.10/117.17 inference(scs_inference,[],[26,3727,4165,4153,3875,3899,4150,4103,2886,2964,4102,2365,651,514,86,48,124,54,53,2,84,14,13,15,12,16,3,102])). % 117.10/117.17 cnf(4200,plain, % 117.10/117.17 (E(f16(f17(a2)),a1)), % 117.10/117.17 inference(scs_inference,[],[4183,2904,2974,124,54,53])). % 117.10/117.17 cnf(4205,plain, % 117.10/117.17 (P6(f17(a1),f13(f17(a2)))), % 117.10/117.17 inference(scs_inference,[],[4183,3063,4160,4155,2904,2974,2750,52,124,54,53,2,84,80])). % 117.10/117.17 cnf(4210,plain, % 117.10/117.17 (~E(f13(f13(x42101)),f13(a2))), % 117.10/117.17 inference(scs_inference,[],[4183,3063,4160,4116,4155,2904,2974,110,2818,2750,52,124,54,53,2,84,80,19,14])). % 117.10/117.17 cnf(4211,plain, % 117.10/117.17 (P2(x42111,f13(x42111))), % 117.10/117.17 inference(rename_variables,[],[2818])). % 117.10/117.17 cnf(4212,plain, % 117.10/117.17 (P2(f12(a1),f13(f12(a2)))), % 117.10/117.17 inference(scs_inference,[],[4183,3063,4160,4116,4155,2904,2974,110,2818,4211,2750,52,124,54,53,2,84,80,19,14,13])). % 117.10/117.17 cnf(4220,plain, % 117.10/117.17 (P2(f12(a1),f13(a2))), % 117.10/117.17 inference(scs_inference,[],[4183,3063,4190,3892,4160,4116,4117,4155,2888,2904,2974,2311,3313,110,3214,2818,4211,2750,52,1149,124,54,53,2,84,80,19,14,13,12,16,3,70,81])). % 117.10/117.17 cnf(4222,plain, % 117.10/117.17 (~P6(f13(f17(a2)),f17(a1))), % 117.10/117.17 inference(scs_inference,[],[4183,3063,4190,3892,4160,4116,4117,4155,2888,2904,2974,2311,3313,110,3214,2818,4211,2750,52,1149,124,54,53,2,84,80,19,14,13,12,16,3,70,81,82])). % 117.10/117.17 cnf(4225,plain, % 117.10/117.17 (P8(f12(a1),f18(a1))), % 117.10/117.17 inference(scs_inference,[],[4183,3063,4190,3892,4077,4160,4116,4117,4155,2888,2904,2974,2311,3159,3313,110,3214,2818,4211,2750,52,1149,124,54,53,2,84,80,19,14,13,12,16,3,70,81,82,667,20])). % 117.10/117.17 cnf(4228,plain, % 117.10/117.17 (P2(f12(a1),f13(f18(a1)))), % 117.10/117.17 inference(scs_inference,[],[4225,81])). % 117.10/117.17 cnf(4233,plain, % 117.10/117.17 (E(f7(f13(a2)),a1)), % 117.10/117.17 inference(scs_inference,[],[4225,4086,2978,3549,81,124,54,53])). % 117.10/117.17 cnf(4236,plain, % 117.10/117.17 (~P2(f15(a5),f13(a2))), % 117.10/117.17 inference(scs_inference,[],[26,4225,4210,4086,2978,3549,2942,81,124,54,53,2,84])). % 117.10/117.17 cnf(4240,plain, % 117.10/117.17 (~E(f17(a1),f16(a5))), % 117.10/117.17 inference(scs_inference,[],[26,4225,4210,4086,4118,2978,4160,3083,3549,2942,48,81,124,54,53,2,84,14,13])). % 117.10/117.17 cnf(4244,plain, % 117.10/117.17 (P5(a2)), % 117.10/117.17 inference(scs_inference,[],[26,2995,4225,4210,4086,4200,4118,3799,2978,4160,3083,2317,3549,2942,2834,36,86,48,81,124,54,53,2,84,14,13,12,16,3,70])). % 117.10/117.17 cnf(4246,plain, % 117.10/117.17 (~E(f7(f13(a2)),f15(a5))), % 117.10/117.17 inference(scs_inference,[],[26,2995,4225,4210,4086,4200,4118,3799,2978,4160,3083,2317,3549,2942,2834,36,86,48,81,124,54,53,2,84,14,13,12,16,3,70,102])). % 117.10/117.17 cnf(4258,plain, % 117.10/117.17 (~E(f12(a2),f15(a5))), % 117.10/117.17 inference(scs_inference,[],[4236,124])). % 117.10/117.17 cnf(4259,plain, % 117.10/117.17 (P3(f7(f13(a10)))), % 117.10/117.17 inference(scs_inference,[],[4236,3466,124,54])). % 117.10/117.17 cnf(4264,plain, % 117.10/117.17 (~P2(f13(f17(a2)),f13(a10))), % 117.10/117.17 inference(scs_inference,[],[4236,4240,4205,3466,28,124,54,53,2,84])). % 117.10/117.17 cnf(4266,plain, % 117.10/117.17 (~E(f13(f15(a5)),f13(a2))), % 117.10/117.17 inference(scs_inference,[],[4236,4240,4205,3466,2818,28,124,54,53,2,84,14])). % 117.10/117.17 cnf(4267,plain, % 117.10/117.17 (P2(x42671,f13(x42671))), % 117.10/117.17 inference(rename_variables,[],[2818])). % 117.10/117.17 cnf(4271,plain, % 117.10/117.17 (~P6(a5,f15(a1))), % 117.10/117.17 inference(scs_inference,[],[4236,4240,4053,4205,4119,2312,3466,2812,3222,2818,4267,28,124,54,53,2,84,14,13,12,16])). % 117.10/117.17 cnf(4273,plain, % 117.10/117.17 (E(f16(a2),f15(a2))), % 117.10/117.17 inference(scs_inference,[],[4244,4236,4240,4192,4053,4233,4205,4119,2312,3466,3799,2812,36,3222,2818,4267,28,124,54,53,2,84,14,13,12,16,3,73])). % 117.10/117.17 cnf(4288,plain, % 117.10/117.17 (P3(f7(f13(a8)))), % 117.10/117.17 inference(scs_inference,[],[4264,3377,124,54])). % 117.10/117.17 cnf(4293,plain, % 117.10/117.17 (~P2(a5,f13(a2))), % 117.10/117.17 inference(scs_inference,[],[26,4258,4264,3377,3239,124,54,53,2,84])). % 117.10/117.17 cnf(4298,plain, % 117.10/117.17 (~P6(f16(f16(a5)),f15(a1))), % 117.10/117.17 inference(scs_inference,[],[26,4273,4258,4271,4264,2958,3377,3239,1222,48,124,54,53,2,84,14,21,15])). % 117.10/117.17 cnf(4299,plain, % 117.10/117.17 (~P2(f16(a5),f13(a2))), % 117.10/117.17 inference(scs_inference,[],[26,4273,4258,4271,4264,2958,3377,4236,3239,2858,1222,48,124,54,53,2,84,14,21,15,13])). % 117.10/117.17 cnf(4313,plain, % 117.10/117.17 (E(f16(f12(x43131)),a1)), % 117.10/117.17 inference(scs_inference,[],[4299,3994,3220,124,102,54,53])). % 117.10/117.17 cnf(4316,plain, % 117.10/117.17 (~P2(f13(f17(a2)),f13(a8))), % 117.10/117.17 inference(scs_inference,[],[4299,4246,3994,4205,3220,27,124,102,54,53,2,84])). % 117.10/117.17 cnf(4318,plain, % 117.10/117.17 (P6(f12(a1),f13(a2))), % 117.10/117.17 inference(scs_inference,[],[4220,4299,4246,3994,4205,3220,27,52,124,102,54,53,2,84,80])). % 117.10/117.17 cnf(4342,plain, % 117.10/117.17 (~P2(a11,f13(a2))), % 117.10/117.17 inference(scs_inference,[],[26,3248,4316,3075,2778,442,54,124,53,2,84])). % 117.10/117.17 cnf(4346,plain, % 117.10/117.17 (~P2(f16(f16(a5)),f13(a2))), % 117.10/117.17 inference(scs_inference,[],[26,4293,3248,4316,4115,3075,2778,442,1222,48,54,124,53,2,84,14,13])). % 117.10/117.17 cnf(4348,plain, % 117.10/117.17 (~P6(x43481,f16(f12(x43482)))), % 117.10/117.17 inference(scs_inference,[],[26,4293,3248,4316,4313,4115,3075,2778,860,442,86,1222,48,54,124,53,2,84,14,13,12,16])). % 117.10/117.17 cnf(4365,plain, % 117.10/117.17 (E(f16(f18(a2)),a1)), % 117.10/117.17 inference(scs_inference,[],[4342,2816,2964,54,124,53])). % 117.10/117.17 cnf(4375,plain, % 117.10/117.17 (~E(f13(a11),f13(a2))), % 117.10/117.17 inference(scs_inference,[],[4342,3652,4348,4318,3561,2829,4103,2816,2964,3486,47,2818,54,124,53,2,16,3,84,19,14])). % 117.10/117.17 cnf(4377,plain, % 117.10/117.17 (~P2(f13(a5),f13(f13(a2)))), % 117.10/117.17 inference(scs_inference,[],[4342,3652,4346,4348,4318,3561,2829,4103,2816,2964,3132,3486,47,2818,54,124,53,2,16,3,84,19,14,85])). % 117.10/117.17 cnf(4394,plain, % 117.10/117.17 (E(f13(a8),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[27,4043,3549,54,124,53,6])). % 117.10/117.17 cnf(4395,plain, % 117.10/117.17 (E(f9(a8),f9(a1))), % 117.10/117.17 inference(scs_inference,[],[27,4043,3549,54,124,53,6,8])). % 117.10/117.17 cnf(4398,plain, % 117.10/117.17 (~E(f13(a14),f16(a8))), % 117.10/117.17 inference(scs_inference,[],[27,3641,4375,4043,4365,3549,3016,86,54,124,53,6,8,2,16,3])). % 117.10/117.17 cnf(4399,plain, % 117.10/117.17 (~P2(f13(a1),f13(a8))), % 117.10/117.17 inference(scs_inference,[],[27,3641,4375,4043,4365,1091,3549,3016,86,54,124,53,6,8,2,16,3,84])). % 117.10/117.17 cnf(4404,plain, % 117.10/117.17 (~P2(f16(f16(a11)),f13(a2))), % 117.10/117.17 inference(scs_inference,[],[27,3641,4375,4043,4365,4117,1091,3999,4342,3273,3549,3099,3016,86,48,54,124,53,6,8,2,16,3,84,14,15,13])). % 117.10/117.17 cnf(4408,plain, % 117.10/117.17 (E(f16(a8),f16(a1))), % 117.10/117.17 inference(scs_inference,[],[27,3641,4375,4043,4288,4365,3414,4117,2305,1091,3999,4342,3273,3549,3099,3377,3016,86,48,54,124,53,6,8,2,16,3,84,14,15,13,12,70,7])). % 117.10/117.17 cnf(4409,plain, % 117.10/117.17 (E(f12(a8),f12(a1))), % 117.10/117.17 inference(scs_inference,[],[27,3641,4375,4043,4288,4365,3414,4117,2305,1091,3999,4342,3273,3549,3099,3377,3016,86,48,54,124,53,6,8,2,16,3,84,14,15,13,12,70,7,4])). % 117.10/117.17 cnf(4410,plain, % 117.10/117.17 (E(f7(a8),f7(a1))), % 117.10/117.17 inference(scs_inference,[],[27,3641,4375,4043,4288,4365,3414,4117,2305,1091,3999,4342,3273,3549,3099,3377,3016,86,48,54,124,53,6,8,2,16,3,84,14,15,13,12,70,7,4,5])). % 117.10/117.17 cnf(4412,plain, % 117.10/117.17 (E(f18(a8),f18(a1))), % 117.10/117.17 inference(scs_inference,[],[27,3641,4375,4043,4288,4365,3414,4117,2305,1091,3999,4342,3273,3549,3099,3377,3016,86,48,54,124,53,6,8,2,16,3,84,14,15,13,12,70,7,4,5,10,11])). % 117.10/117.17 cnf(4414,plain, % 117.10/117.17 (E(f17(a8),f17(a1))), % 117.10/117.17 inference(scs_inference,[],[27,3641,4375,4043,4288,4365,3414,4117,2305,1091,3999,4342,3273,3549,3099,3377,3016,86,48,54,124,53,6,8,2,16,3,84,14,15,13,12,70,7,4,5,10,11,102,9])). % 117.10/117.17 cnf(4431,plain, % 117.10/117.17 (~P2(f13(a2),f13(a8))), % 117.10/117.17 inference(scs_inference,[],[27,4395,4398,4399,4414,4222,2829,4318,2778,2758,3359,54,124,53,2,16,3,68,69,84])). % 117.10/117.17 cnf(4435,plain, % 117.10/117.17 (~P2(f13(a8),f13(a8))), % 117.10/117.17 inference(scs_inference,[],[27,4394,4395,4398,4399,4414,4222,2829,4318,2778,2758,3359,2818,54,124,53,2,16,3,68,69,84,14,13])). % 117.10/117.17 cnf(4456,plain, % 117.10/117.17 (~P6(x44561,f16(a8))), % 117.10/117.17 inference(scs_inference,[],[4431,4435,3753,4408,703,3222,256,54,124,102,53,2,16])). % 117.10/117.17 cnf(4462,plain, % 117.10/117.17 (~P2(f13(f18(a10)),f13(a8))), % 117.10/117.17 inference(scs_inference,[],[27,3321,4431,4435,3753,4408,4394,806,3597,703,3222,256,54,124,102,53,2,16,3,69,68,84])). % 117.10/117.17 cnf(4476,plain, % 117.10/117.17 (E(f17(a8),a1)), % 117.10/117.17 inference(scs_inference,[],[4404,3359,46,54,124,53])). % 117.10/117.17 cnf(4481,plain, % 117.10/117.17 (~E(f13(a1),f16(a8))), % 117.10/117.17 inference(scs_inference,[],[4456,3776,4404,4155,3359,46,54,124,53,6,8,2,16])). % 117.10/117.17 cnf(4486,plain, % 117.10/117.17 (P6(f12(a1),f13(f18(a1)))), % 117.10/117.17 inference(scs_inference,[],[4456,3776,4404,4228,4410,4155,3359,46,52,1149,54,124,53,6,8,2,16,3,84,80])). % 117.10/117.17 cnf(4490,plain, % 117.10/117.17 (P2(x44901,f13(x44901))), % 117.10/117.17 inference(rename_variables,[],[2818])). % 117.10/117.17 cnf(4495,plain, % 117.10/117.17 (E(f12(f17(a8)),f12(a1))), % 117.10/117.17 inference(scs_inference,[],[4456,3776,4404,4228,4409,4410,4435,2278,4155,3107,3359,2818,4490,46,52,1149,54,124,53,6,8,2,16,3,84,80,14,13,12,7,4])). % 117.10/117.17 cnf(4497,plain, % 117.10/117.17 (E(f15(f17(a8)),f15(a1))), % 117.10/117.17 inference(scs_inference,[],[4456,3776,4404,4228,4409,4410,4435,2278,4155,3107,3359,2818,4490,46,52,1149,54,124,53,6,8,2,16,3,84,80,14,13,12,7,4,5,10])). % 117.10/117.17 cnf(4499,plain, % 117.10/117.17 (E(f17(f17(a8)),f17(a1))), % 117.10/117.17 inference(scs_inference,[],[4456,3776,4404,4228,4409,4410,4435,2278,4155,3107,3359,2818,4490,46,52,1149,54,124,53,6,8,2,16,3,84,80,14,13,12,7,4,5,10,11,9])). % 117.10/117.17 cnf(4515,plain, % 117.10/117.17 (~P2(f13(f18(a1)),f13(a8))), % 117.10/117.17 inference(scs_inference,[],[27,3798,4481,4476,4462,4497,4486,3222,86,124,53,9,6,8,2,16,3,84])). % 117.10/117.17 cnf(4519,plain, % 117.10/117.17 (~E(f15(a1),f13(a5))), % 117.10/117.17 inference(scs_inference,[],[27,3798,4481,4476,4462,4497,4377,4486,3650,3222,86,48,124,53,9,6,8,2,16,3,84,14,13])). % 117.10/117.17 cnf(4521,plain, % 117.10/117.17 (~E(a8,f18(a5))), % 117.10/117.17 inference(scs_inference,[],[27,3798,4481,4476,4462,4497,4377,4486,2299,3650,3222,86,48,124,53,9,6,8,2,16,3,84,14,13,12])). % 117.10/117.17 cnf(4546,plain, % 117.10/117.17 (E(a10,a1)), % 117.10/117.17 inference(scs_inference,[],[4515,28,124,53])). % 117.10/117.17 cnf(4548,plain, % 117.10/117.17 (E(f17(a10),f17(a1))), % 117.10/117.17 inference(scs_inference,[],[4515,28,124,53,9])). % 117.10/117.17 cnf(4549,plain, % 117.10/117.17 (E(f13(a10),f13(a1))), % 117.10/117.17 inference(scs_inference,[],[4515,28,124,53,9,6])). % 117.10/117.17 cnf(4554,plain, % 117.10/117.17 (~E(f17(a1),f18(a5))), % 117.10/117.17 inference(scs_inference,[],[4519,4499,4515,3753,4456,4486,28,124,53,9,6,8,2,16,3])). % 117.10/117.17 cnf(4555,plain, % 117.10/117.17 (~P2(f13(f18(a1)),f13(a10))), % 117.10/117.17 inference(scs_inference,[],[4519,4499,4515,3753,4456,4486,28,124,53,9,6,8,2,16,3,84])). % 117.10/117.17 cnf(4559,plain, % 117.10/117.17 (~E(f13(a5),f13(a2))), % 117.10/117.17 inference(scs_inference,[],[4519,4495,4499,4515,2752,4346,3753,4456,4486,110,28,124,53,9,6,8,2,16,3,84,19,14])). % 117.10/117.17 cnf(4563,plain, % 117.10/117.17 (E(f16(a10),f16(a1))), % 117.10/117.17 inference(scs_inference,[],[4519,4495,4499,4515,4412,2752,4346,3753,4456,4486,2289,110,3048,28,2818,124,53,9,6,8,2,16,3,84,19,14,13,12,7])). % 117.10/117.17 cnf(4566,plain, % 117.10/117.17 (E(f12(a10),f12(a1))), % 117.10/117.17 inference(scs_inference,[],[4519,4495,4499,4515,4412,2752,4346,3753,4456,4486,2289,110,3048,28,2818,124,53,9,6,8,2,16,3,84,19,14,13,12,7,81,4])). % 117.10/117.17 cnf(4567,plain, % 117.10/117.17 (E(f7(a10),f7(a1))), % 117.10/117.17 inference(scs_inference,[],[4519,4495,4499,4515,4412,2752,4346,3753,4456,4486,2289,110,3048,28,2818,124,53,9,6,8,2,16,3,84,19,14,13,12,7,81,4,5])). % 117.10/117.17 cnf(4568,plain, % 117.10/117.17 (E(f15(a10),f15(a1))), % 117.10/117.17 inference(scs_inference,[],[4519,4495,4499,4515,4412,2752,4346,3753,4456,4486,2289,110,3048,28,2818,124,53,9,6,8,2,16,3,84,19,14,13,12,7,81,4,5,10])). % 117.10/117.17 cnf(4580,plain, % 117.10/117.17 (E(f17(f12(x45801)),f17(a1))), % 117.10/117.17 inference(scs_inference,[],[4555,46,124,53,9])). % 117.10/117.17 cnf(4586,plain, % 117.10/117.17 (~P2(f13(f16(a8)),f13(a8))), % 117.10/117.17 inference(scs_inference,[],[27,3922,4548,4554,4020,4555,3506,1529,46,124,53,9,6,8,2,16,3,84])). % 117.10/117.17 cnf(4588,plain, % 117.10/117.17 (~P6(f13(a10),f17(f16(a1)))), % 117.10/117.17 inference(scs_inference,[],[27,3922,4548,4549,4554,4020,4555,3957,3506,1529,46,124,53,9,6,8,2,16,3,84,15])). % 117.10/117.17 cnf(4600,plain, % 117.10/117.17 (P6(f12(a1),f13(f12(a2)))), % 117.10/117.17 inference(scs_inference,[],[27,4546,3922,4548,4549,4554,4020,4555,4104,4212,3957,863,3506,3311,1529,46,52,48,124,53,9,6,8,2,16,3,84,15,14,13,12,7,4,5,10,11,69,80])). % 117.10/117.17 cnf(4617,plain, % 117.10/117.17 (~P6(f13(a10),f17(a1))), % 117.10/117.17 inference(scs_inference,[],[4521,4586,4588,2828,817,124,53,9,6,8,2,16])). % 117.10/117.17 cnf(4619,plain, % 117.10/117.17 (~P2(f13(f12(a2)),f13(a8))), % 117.10/117.17 inference(scs_inference,[],[27,4563,4521,4586,3241,4588,4600,2828,817,124,53,9,6,8,2,16,3,84])). % 117.10/117.17 cnf(4622,plain, % 117.10/117.17 (P2(x46221,f13(x46221))), % 117.10/117.17 inference(rename_variables,[],[2818])). % 117.10/117.17 cnf(4629,plain, % 117.10/117.17 (E(f12(f18(a1)),f12(a1))), % 117.10/117.17 inference(scs_inference,[],[27,4563,4566,4521,4586,4259,3241,4588,4600,3496,2291,4431,3466,2828,3107,2818,4622,817,124,53,9,6,8,2,16,3,84,14,12,13,70,7,4])). % 117.10/117.17 cnf(4651,plain, % 117.10/117.17 (~P2(f13(f16(a4)),f13(a8))), % 117.10/117.17 inference(scs_inference,[],[27,4559,3971,4619,4629,4568,4298,3332,124,2,16,3,84])). % 117.10/117.17 cnf(4673,plain, % 117.10/117.17 (E(f7(a10),f7(f16(a1)))), % 117.10/117.17 inference(scs_inference,[],[4617,3954,4651,4567,4580,1149,124,2,16,3])). % 117.10/117.17 cnf(5243,plain, % 117.10/117.17 ($false), % 117.10/117.17 inference(scs_inference,[],[2858,3222,4673,4266,4191,2223,161,6,160,102,9,74,2]), % 117.10/117.17 ['proof']). % 117.10/117.17 % SZS output end Proof % 117.10/117.17 % Total time :116.480000s %------------------------------------------------------------------------------