%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU062+1 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n029.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:00:57 EDT 2024 % Result : Theorem 117.67s 117.68s % Output : CNFRefutation 117.67s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU062+1 : TPTP v8.2.0. Released v3.2.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n029.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Fri Jun 21 16:01:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.47/0.56 start to proof:theBenchmark % 117.61/117.66 %------------------------------------------- % 117.61/117.66 % File :CSE---1.7 % 117.61/117.66 % Problem :theBenchmark % 117.61/117.66 % Transform :cnf % 117.61/117.66 % Format :tptp:raw % 117.61/117.66 % Command :java -jar mcs_scs.jar %d %s % 117.61/117.66 % 117.61/117.66 % Result :Theorem 117.060000s % 117.61/117.66 % Output :CNFRefutation 117.060000s % 117.61/117.66 %------------------------------------------- % 117.67/117.67 %------------------------------------------------------------------------------ % 117.67/117.67 % File : SEU062+1 : TPTP v8.2.0. Released v3.2.0. % 117.67/117.68 % Domain : Set theory % 117.67/117.68 % Problem : Functions and their basic properties, theorem 143 % 117.67/117.68 % Version : [Urb06] axioms : Especial. % 117.67/117.68 % English : % 117.67/117.68 % 117.67/117.68 % Refs : [Byl90] Bylinski (1990), Functions and Their Basic Properties % 117.67/117.68 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 117.67/117.68 % Source : [Urb06] % 117.67/117.68 % Names : funct_1__t143_funct_1 [Urb06] % 117.67/117.68 % 117.67/117.68 % Status : Theorem % 117.67/117.68 % Rating : 0.14 v8.2.0, 0.17 v8.1.0, 0.11 v7.5.0, 0.09 v7.4.0, 0.10 v7.3.0, 0.14 v7.2.0, 0.10 v7.1.0, 0.09 v7.0.0, 0.13 v6.4.0, 0.15 v6.3.0, 0.17 v6.2.0, 0.12 v6.1.0, 0.20 v6.0.0, 0.22 v5.5.0, 0.26 v5.4.0, 0.32 v5.3.0, 0.33 v5.2.0, 0.20 v5.1.0, 0.24 v5.0.0, 0.21 v4.1.0, 0.22 v4.0.0, 0.21 v3.7.0, 0.10 v3.5.0, 0.11 v3.4.0, 0.16 v3.3.0, 0.21 v3.2.0 % 117.67/117.68 % Syntax : Number of formulae : 34 ( 7 unt; 0 def) % 117.67/117.68 % Number of atoms : 79 ( 4 equ) % 117.67/117.68 % Maximal formula atoms : 6 ( 2 avg) % 117.67/117.68 % Number of connectives : 60 ( 15 ~; 1 |; 26 &) % 117.67/117.68 % ( 3 <=>; 15 =>; 0 <=; 0 <~>) % 117.67/117.68 % Maximal formula depth : 8 ( 4 avg) % 117.67/117.68 % Maximal term depth : 3 ( 1 avg) % 117.67/117.68 % Number of predicates : 9 ( 8 usr; 0 prp; 1-2 aty) % 117.67/117.68 % Number of functors : 5 ( 5 usr; 1 con; 0-2 aty) % 117.67/117.68 % Number of variables : 50 ( 39 !; 11 ?) % 117.67/117.68 % SPC : FOF_THM_RFO_SEQ % 117.67/117.68 % 117.67/117.68 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 117.67/117.68 % library, www.mizar.org % 117.67/117.68 %------------------------------------------------------------------------------ % 117.67/117.68 fof(antisymmetry_r2_hidden,axiom, % 117.67/117.68 ! [A,B] : % 117.67/117.68 ( in(A,B) % 117.67/117.68 => ~ in(B,A) ) ). % 117.67/117.68 % 117.67/117.68 fof(cc1_funct_1,axiom, % 117.67/117.68 ! [A] : % 117.67/117.68 ( empty(A) % 117.67/117.68 => function(A) ) ). % 117.67/117.68 % 117.67/117.68 fof(cc1_relat_1,axiom, % 117.67/117.68 ! [A] : % 117.67/117.68 ( empty(A) % 117.67/117.68 => relation(A) ) ). % 117.67/117.68 % 117.67/117.68 fof(cc2_funct_1,axiom, % 117.67/117.68 ! [A] : % 117.67/117.68 ( ( relation(A) % 117.67/117.68 & empty(A) % 117.67/117.68 & function(A) ) % 117.67/117.68 => ( relation(A) % 117.67/117.68 & function(A) % 117.67/117.68 & one_to_one(A) ) ) ). % 117.67/117.68 % 117.67/117.68 fof(d3_tarski,axiom, % 117.67/117.68 ! [A,B] : % 117.67/117.68 ( subset(A,B) % 117.67/117.68 <=> ! [C] : % 117.67/117.68 ( in(C,A) % 117.67/117.68 => in(C,B) ) ) ). % 117.67/117.68 % 117.67/117.68 fof(existence_m1_subset_1,axiom, % 117.67/117.68 ! [A] : % 117.67/117.68 ? [B] : element(B,A) ). % 117.67/117.68 % 117.67/117.68 fof(fc12_relat_1,axiom, % 117.67/117.68 ( empty(empty_set) % 117.67/117.68 & relation(empty_set) % 117.67/117.68 & relation_empty_yielding(empty_set) ) ). % 117.67/117.68 % 117.67/117.68 fof(fc1_subset_1,axiom, % 117.67/117.68 ! [A] : ~ empty(powerset(A)) ). % 117.67/117.68 % 117.67/117.68 fof(fc1_xboole_0,axiom, % 117.67/117.68 empty(empty_set) ). % 117.67/117.68 % 117.67/117.68 fof(fc2_subset_1,axiom, % 117.67/117.68 ! [A] : ~ empty(singleton(A)) ). % 117.67/117.68 % 117.67/117.68 fof(fc4_relat_1,axiom, % 117.67/117.68 ( empty(empty_set) % 117.67/117.68 & relation(empty_set) ) ). % 117.67/117.68 % 117.67/117.68 fof(fc6_relat_1,axiom, % 117.67/117.68 ! [A] : % 117.67/117.68 ( ( ~ empty(A) % 117.67/117.68 & relation(A) ) % 117.67/117.68 => ~ empty(relation_rng(A)) ) ). % 117.67/117.68 % 117.67/117.68 fof(fc8_relat_1,axiom, % 117.67/117.68 ! [A] : % 117.67/117.68 ( empty(A) % 117.67/117.68 => ( empty(relation_rng(A)) % 117.67/117.68 & relation(relation_rng(A)) ) ) ). % 117.67/117.68 % 117.67/117.68 fof(rc1_funct_1,axiom, % 117.67/117.68 ? [A] : % 117.67/117.68 ( relation(A) % 117.67/117.68 & function(A) ) ). % 117.67/117.68 % 117.67/117.68 fof(rc1_relat_1,axiom, % 117.67/117.68 ? [A] : % 117.67/117.68 ( empty(A) % 117.67/117.68 & relation(A) ) ). % 117.67/117.68 % 117.67/117.68 fof(rc1_subset_1,axiom, % 117.67/117.68 ! [A] : % 117.67/117.68 ( ~ empty(A) % 117.67/117.68 => ? [B] : % 117.67/117.68 ( element(B,powerset(A)) % 117.67/117.68 & ~ empty(B) ) ) ). % 117.67/117.68 % 117.67/117.68 fof(rc1_xboole_0,axiom, % 117.67/117.68 ? [A] : empty(A) ). % 117.67/117.68 % 117.67/117.68 fof(rc2_funct_1,axiom, % 117.67/117.68 ? [A] : % 117.67/117.68 ( relation(A) % 117.67/117.68 & empty(A) % 117.67/117.68 & function(A) ) ). % 117.67/117.68 % 117.67/117.68 fof(rc2_relat_1,axiom, % 117.67/117.68 ? [A] : % 117.67/117.68 ( ~ empty(A) % 117.67/117.68 & relation(A) ) ). % 117.67/117.68 % 117.67/117.68 fof(rc2_subset_1,axiom, % 117.67/117.68 ! [A] : % 117.67/117.68 ? [B] : % 117.67/117.68 ( element(B,powerset(A)) % 117.67/117.68 & empty(B) ) ). % 117.67/117.68 % 117.67/117.68 fof(rc2_xboole_0,axiom, % 117.67/117.68 ? [A] : ~ empty(A) ). % 117.67/117.68 % 117.67/117.68 fof(rc3_funct_1,axiom, % 117.67/117.68 ? [A] : % 117.67/117.68 ( relation(A) % 117.67/117.68 & function(A) % 117.67/117.68 & one_to_one(A) ) ). % 117.67/117.68 % 117.67/117.68 fof(rc3_relat_1,axiom, % 117.67/117.68 ? [A] : % 117.67/117.68 ( relation(A) % 117.67/117.68 & relation_empty_yielding(A) ) ). % 117.67/117.68 % 117.67/117.68 fof(reflexivity_r1_tarski,axiom, % 117.67/117.68 ! [A,B] : subset(A,A) ). % 117.67/117.68 % 117.67/117.68 fof(t142_funct_1,axiom, % 117.67/117.68 ! [A,B] : % 117.67/117.68 ( relation(B) % 117.67/117.68 => ( in(A,relation_rng(B)) % 117.67/117.68 <=> relation_inverse_image(B,singleton(A)) != empty_set ) ) ). % 117.67/117.68 % 117.67/117.68 fof(t143_funct_1,conjecture, % 117.67/117.68 ! [A,B] : % 117.67/117.68 ( relation(B) % 117.67/117.68 => ( ! [C] : % 117.67/117.68 ~ ( in(C,A) % 117.67/117.68 & relation_inverse_image(B,singleton(C)) = empty_set ) % 117.67/117.68 => subset(A,relation_rng(B)) ) ) ). % 117.67/117.68 % 117.67/117.68 fof(t1_subset,axiom, % 117.67/117.68 ! [A,B] : % 117.67/117.68 ( in(A,B) % 117.67/117.68 => element(A,B) ) ). % 117.67/117.68 % 117.67/117.68 fof(t2_subset,axiom, % 117.67/117.68 ! [A,B] : % 117.67/117.68 ( element(A,B) % 117.67/117.68 => ( empty(B) % 117.67/117.68 | in(A,B) ) ) ). % 117.67/117.68 % 117.67/117.68 fof(t3_subset,axiom, % 117.67/117.68 ! [A,B] : % 117.67/117.68 ( element(A,powerset(B)) % 117.67/117.68 <=> subset(A,B) ) ). % 117.67/117.68 % 117.67/117.68 fof(t4_subset,axiom, % 117.67/117.68 ! [A,B,C] : % 117.67/117.68 ( ( in(A,B) % 117.67/117.68 & element(B,powerset(C)) ) % 117.67/117.68 => element(A,C) ) ). % 117.67/117.68 % 117.67/117.68 fof(t5_subset,axiom, % 117.67/117.68 ! [A,B,C] : % 117.67/117.68 ~ ( in(A,B) % 117.67/117.68 & element(B,powerset(C)) % 117.67/117.68 & empty(C) ) ). % 117.67/117.68 % 117.67/117.68 fof(t6_boole,axiom, % 117.67/117.68 ! [A] : % 117.67/117.68 ( empty(A) % 117.67/117.68 => A = empty_set ) ). % 117.67/117.68 % 117.67/117.68 fof(t7_boole,axiom, % 117.67/117.68 ! [A,B] : % 117.67/117.68 ~ ( in(A,B) % 117.67/117.68 & empty(B) ) ). % 117.67/117.68 % 117.67/117.68 fof(t8_boole,axiom, % 117.67/117.68 ! [A,B] : % 117.67/117.68 ~ ( empty(A) % 117.67/117.68 & A != B % 117.67/117.68 & empty(B) ) ). % 117.67/117.68 % 117.67/117.68 %------------------------------------------------------------------------------ % 117.67/117.68 %------------------------------------------- % 117.67/117.68 % Proof found % 117.67/117.68 % SZS status Theorem for theBenchmark % 117.67/117.68 % SZS output start Proof % 117.67/117.68 %ClaNum:78(EqnAxiom:24) % 117.67/117.68 %VarNum:98(SingletonVarNum:47) % 117.67/117.68 %MaxLitNum:4 % 117.67/117.68 %MaxfuncDepth:2 % 117.67/117.68 %SharedTerms:33 % 117.67/117.68 %goalClause: 42 54 72 % 117.67/117.68 %singleGoalClaCount:2 % 117.67/117.68 [27]P1(a1) % 117.67/117.68 [28]P1(a2) % 117.67/117.68 [29]P1(a11) % 117.67/117.68 [30]P1(a13) % 117.67/117.68 [31]P3(a3) % 117.67/117.68 [32]P3(a13) % 117.67/117.68 [33]P3(a4) % 117.67/117.68 [35]P4(a1) % 117.67/117.68 [36]P4(a3) % 117.67/117.68 [37]P4(a2) % 117.67/117.68 [38]P4(a13) % 117.67/117.68 [39]P4(a14) % 117.67/117.68 [40]P4(a4) % 117.67/117.69 [41]P4(a6) % 117.67/117.69 [42]P4(a7) % 117.67/117.69 [43]P5(a4) % 117.67/117.69 [44]P7(a1) % 117.67/117.69 [45]P7(a6) % 117.67/117.69 [50]~P1(a14) % 117.67/117.69 [51]~P1(a5) % 117.67/117.69 [54]~P8(a8,f18(a7)) % 117.67/117.69 [47]P8(x471,x471) % 117.67/117.69 [46]P1(f15(x461)) % 117.67/117.69 [48]P2(f9(x481),x481) % 117.67/117.69 [49]P2(f15(x491),f16(x491)) % 117.67/117.69 [52]~P1(f16(x521)) % 117.67/117.69 [53]~P1(f17(x531)) % 117.67/117.69 [55]~P1(x551)+E(x551,a1) % 117.67/117.69 [56]~P1(x561)+P3(x561) % 117.67/117.69 [57]~P1(x571)+P4(x571) % 117.67/117.69 [59]~P1(x591)+P1(f18(x591)) % 117.67/117.69 [60]~P1(x601)+P4(f18(x601)) % 117.67/117.69 [61]P1(x611)+~P1(f12(x611)) % 117.67/117.69 [65]P1(x651)+P2(f12(x651),f16(x651)) % 117.67/117.69 [72]~P6(x721,a8)+~E(f19(a7,f17(x721)),a1) % 117.67/117.69 [64]~P1(x641)+~P6(x642,x641) % 117.67/117.69 [66]~P6(x661,x662)+P2(x661,x662) % 117.67/117.69 [69]~P6(x692,x691)+~P6(x691,x692) % 117.67/117.69 [68]~P8(x681,x682)+P2(x681,f16(x682)) % 117.67/117.69 [70]P8(x701,x702)+~P2(x701,f16(x702)) % 117.67/117.69 [73]P8(x731,x732)+P6(f10(x731,x732),x731) % 117.67/117.69 [78]P8(x781,x782)+~P6(f10(x781,x782),x782) % 117.67/117.69 [63]~P4(x631)+P1(x631)+~P1(f18(x631)) % 117.67/117.69 [58]~P1(x582)+~P1(x581)+E(x581,x582) % 117.67/117.69 [67]~P2(x672,x671)+P1(x671)+P6(x672,x671) % 117.67/117.69 [71]~P4(x711)+P6(x712,f18(x711))+E(f19(x711,f17(x712)),a1) % 117.67/117.69 [77]~P4(x771)+~P6(x772,f18(x771))+~E(f19(x771,f17(x772)),a1) % 117.67/117.69 [74]~P8(x743,x742)+P6(x741,x742)+~P6(x741,x743) % 117.67/117.69 [75]~P1(x751)+~P6(x752,x753)+~P2(x753,f16(x751)) % 117.67/117.69 [76]P2(x761,x762)+~P6(x761,x763)+~P2(x763,f16(x762)) % 117.67/117.69 [62]~P1(x621)+~P3(x621)+~P4(x621)+P5(x621) % 117.67/117.69 %EqnAxiom % 117.67/117.69 [1]E(x11,x11) % 117.67/117.69 [2]E(x22,x21)+~E(x21,x22) % 117.67/117.69 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 117.67/117.69 [4]~E(x41,x42)+E(f15(x41),f15(x42)) % 117.67/117.69 [5]~E(x51,x52)+E(f9(x51),f9(x52)) % 117.67/117.69 [6]~E(x61,x62)+E(f10(x61,x63),f10(x62,x63)) % 117.67/117.69 [7]~E(x71,x72)+E(f10(x73,x71),f10(x73,x72)) % 117.67/117.69 [8]~E(x81,x82)+E(f16(x81),f16(x82)) % 117.67/117.69 [9]~E(x91,x92)+E(f19(x91,x93),f19(x92,x93)) % 117.67/117.69 [10]~E(x101,x102)+E(f19(x103,x101),f19(x103,x102)) % 117.67/117.69 [11]~E(x111,x112)+E(f17(x111),f17(x112)) % 117.67/117.69 [12]~E(x121,x122)+E(f18(x121),f18(x122)) % 117.67/117.69 [13]~E(x131,x132)+E(f12(x131),f12(x132)) % 117.67/117.69 [14]~P1(x141)+P1(x142)+~E(x141,x142) % 117.67/117.69 [15]P6(x152,x153)+~E(x151,x152)+~P6(x151,x153) % 117.67/117.69 [16]P6(x163,x162)+~E(x161,x162)+~P6(x163,x161) % 117.67/117.69 [17]P8(x172,x173)+~E(x171,x172)+~P8(x171,x173) % 117.67/117.69 [18]P8(x183,x182)+~E(x181,x182)+~P8(x183,x181) % 117.67/117.69 [19]P2(x192,x193)+~E(x191,x192)+~P2(x191,x193) % 117.67/117.69 [20]P2(x203,x202)+~E(x201,x202)+~P2(x203,x201) % 117.67/117.69 [21]~P4(x211)+P4(x212)+~E(x211,x212) % 117.67/117.69 [22]~P3(x221)+P3(x222)+~E(x221,x222) % 117.67/117.69 [23]~P5(x231)+P5(x232)+~E(x231,x232) % 117.67/117.69 [24]~P7(x241)+P7(x242)+~E(x241,x242) % 117.67/117.69 % 117.67/117.69 %------------------------------------------- % 117.67/117.70 cnf(79,plain, % 117.67/117.70 (P8(f9(f16(x791)),x791)), % 117.67/117.70 inference(scs_inference,[],[48,70])). % 117.67/117.70 cnf(80,plain, % 117.67/117.70 (P2(f9(x801),x801)), % 117.67/117.70 inference(rename_variables,[],[48])). % 117.67/117.70 cnf(82,plain, % 117.67/117.70 (~P6(x821,a1)), % 117.67/117.70 inference(scs_inference,[],[48,27,70,64])). % 117.67/117.70 cnf(84,plain, % 117.67/117.70 (P6(f9(a14),a14)), % 117.67/117.70 inference(scs_inference,[],[50,48,80,27,70,64,67])). % 117.67/117.70 cnf(85,plain, % 117.67/117.70 (P2(f9(x851),x851)), % 117.67/117.70 inference(rename_variables,[],[48])). % 117.67/117.70 cnf(87,plain, % 117.67/117.70 (~E(a14,a1)), % 117.67/117.70 inference(scs_inference,[],[50,48,80,27,70,64,67,16])). % 117.67/117.70 cnf(89,plain, % 117.67/117.70 (P8(x891,x891)), % 117.67/117.70 inference(rename_variables,[],[47])). % 117.67/117.70 cnf(92,plain, % 117.67/117.70 (~P6(x921,f9(f16(a1)))), % 117.67/117.70 inference(scs_inference,[],[54,50,47,89,48,80,85,27,70,64,67,16,17,18,75])). % 117.67/117.70 cnf(93,plain, % 117.67/117.70 (P2(f9(x931),x931)), % 117.67/117.70 inference(rename_variables,[],[48])). % 117.67/117.70 cnf(97,plain, % 117.67/117.70 (P8(f9(f16(a1)),x971)), % 117.67/117.70 inference(scs_inference,[],[54,38,50,47,89,48,80,85,27,30,32,70,64,67,16,17,18,75,62,73])). % 117.67/117.70 cnf(105,plain, % 117.67/117.70 (P2(f9(x1051),x1051)), % 117.67/117.70 inference(rename_variables,[],[48])). % 117.67/117.70 cnf(107,plain, % 117.67/117.70 (P2(x1071,x1072)+~E(f9(x1072),x1071)), % 117.67/117.70 inference(scs_inference,[],[54,38,50,47,89,48,80,85,93,105,27,30,32,70,64,67,16,17,18,75,62,73,69,58,15,76,19])). % 117.67/117.70 cnf(108,plain, % 117.67/117.70 (P2(f9(x1081),x1082)+~E(x1081,x1082)), % 117.67/117.70 inference(scs_inference,[],[54,38,50,47,89,48,80,85,93,105,27,30,32,70,64,67,16,17,18,75,62,73,69,58,15,76,19,20])). % 117.67/117.70 cnf(112,plain, % 117.67/117.70 (P8(a1,x1121)), % 117.67/117.70 inference(scs_inference,[],[82,73])). % 117.67/117.70 cnf(115,plain, % 117.67/117.70 (~P6(x1151,a2)), % 117.67/117.70 inference(scs_inference,[],[82,28,73,64])). % 117.67/117.70 cnf(117,plain, % 117.67/117.70 (P8(f15(x1171),x1171)), % 117.67/117.70 inference(scs_inference,[],[82,49,28,73,64,70])). % 117.67/117.70 cnf(119,plain, % 117.67/117.70 (~P6(x1191,f15(a2))), % 117.67/117.70 inference(scs_inference,[],[82,49,28,73,64,70,75])). % 117.67/117.70 cnf(120,plain, % 117.67/117.70 (P2(f15(x1201),f16(x1201))), % 117.67/117.70 inference(rename_variables,[],[49])). % 117.67/117.70 cnf(122,plain, % 117.67/117.70 (P6(f9(a5),a5)), % 117.67/117.70 inference(scs_inference,[],[82,51,49,28,48,73,64,70,75,67])). % 117.67/117.70 cnf(137,plain, % 117.67/117.70 (P2(x1371,f16(x1372))+~E(f15(x1372),x1371)), % 117.67/117.70 inference(scs_inference,[],[54,97,84,92,82,51,49,120,28,48,73,64,70,75,67,16,17,69,58,15,20,76,19])). % 117.67/117.70 cnf(138,plain, % 117.67/117.70 (P8(f9(f16(x1381)),x1382)+~E(x1381,x1382)), % 117.67/117.70 inference(scs_inference,[],[54,79,97,84,92,82,51,49,120,28,48,73,64,70,75,67,16,17,69,58,15,20,76,19,18])). % 117.67/117.70 cnf(143,plain, % 117.67/117.70 (~P6(x1431,a11)), % 117.67/117.70 inference(scs_inference,[],[29,64])). % 117.67/117.70 cnf(146,plain, % 117.67/117.70 (~P6(x1461,f15(a2))), % 117.67/117.70 inference(rename_variables,[],[119])). % 117.67/117.70 cnf(148,plain, % 117.67/117.70 (~P6(x1481,f9(f16(a11)))), % 117.67/117.70 inference(scs_inference,[],[119,29,48,64,73,75])). % 117.67/117.70 cnf(149,plain, % 117.67/117.70 (P2(f9(x1491),x1491)), % 117.67/117.70 inference(rename_variables,[],[48])). % 117.67/117.70 cnf(151,plain, % 117.67/117.70 (P6(f9(f16(x1511)),f16(x1511))), % 117.67/117.70 inference(scs_inference,[],[119,52,29,48,149,64,73,75,67])). % 117.67/117.70 cnf(160,plain, % 117.67/117.70 (~P1(a8)), % 117.67/117.70 inference(scs_inference,[],[54,84,117,119,146,52,29,46,48,149,64,73,75,67,17,16,69,58])). % 117.67/117.70 cnf(163,plain, % 117.67/117.70 (P6(x1631,f16(x1632))+~E(f9(f16(x1632)),x1631)), % 117.67/117.70 inference(scs_inference,[],[54,84,117,119,146,52,29,46,48,149,64,73,75,67,17,16,69,58,15])). % 117.67/117.70 cnf(169,plain, % 117.67/117.70 (P8(f9(f16(a11)),x1691)), % 117.67/117.70 inference(scs_inference,[],[148,73])). % 117.67/117.70 cnf(172,plain, % 117.67/117.70 (~P6(x1721,a13)), % 117.67/117.70 inference(scs_inference,[],[148,30,73,64])). % 117.67/117.70 cnf(174,plain, % 117.67/117.70 (~P6(x1741,f15(a13))), % 117.67/117.70 inference(scs_inference,[],[148,49,30,73,64,75])). % 117.67/117.70 cnf(177,plain, % 117.67/117.70 (P6(f9(a8),a8)), % 117.67/117.70 inference(scs_inference,[],[160,148,49,30,48,73,64,75,67])). % 117.67/117.70 cnf(191,plain, % 117.67/117.70 (~P6(x1911,f15(x1912))), % 117.67/117.70 inference(scs_inference,[],[46,64])). % 117.67/117.70 cnf(194,plain, % 117.67/117.70 (~P6(x1941,f15(a13))), % 117.67/117.70 inference(rename_variables,[],[174])). % 117.67/117.70 cnf(196,plain, % 117.67/117.70 (P6(f9(f17(x1961)),f17(x1961))), % 117.67/117.70 inference(scs_inference,[],[174,53,46,48,64,73,67])). % 117.67/117.70 cnf(203,plain, % 117.67/117.70 (~P6(f17(x2031),f9(f17(x2031)))), % 117.67/117.70 inference(scs_inference,[],[54,84,169,174,194,53,46,48,64,73,67,17,16,69])). % 117.67/117.70 cnf(210,plain, % 117.67/117.70 (P8(f15(x2101),x2102)), % 117.67/117.70 inference(scs_inference,[],[191,73])). % 117.67/117.70 cnf(227,plain, % 117.67/117.70 (P8(a2,x2271)), % 117.67/117.70 inference(scs_inference,[],[115,73])). % 117.67/117.70 cnf(236,plain, % 117.67/117.70 (P8(a11,x2361)), % 117.67/117.70 inference(scs_inference,[],[143,73])). % 117.67/117.70 cnf(243,plain, % 117.67/117.70 (P8(a13,x2431)), % 117.67/117.70 inference(scs_inference,[],[172,73])). % 117.67/117.70 cnf(268,plain, % 117.67/117.70 (P5(a1)), % 117.67/117.70 inference(scs_inference,[],[27,35,56,62])). % 117.67/117.70 cnf(269,plain, % 117.67/117.70 (~P6(x2691,f9(f16(a2)))), % 117.67/117.70 inference(scs_inference,[],[48,28,75])). % 117.67/117.70 cnf(305,plain, % 117.67/117.70 (~E(a11,x3051)+P4(x3051)), % 117.67/117.70 inference(scs_inference,[],[29,57,21])). % 117.67/117.70 cnf(306,plain, % 117.67/117.70 (P4(a11)), % 117.67/117.70 inference(equality_inference,[],[305])). % 117.67/117.70 cnf(331,plain, % 117.67/117.70 (E(f18(a1),a1)), % 117.67/117.70 inference(scs_inference,[],[27,55,59])). % 117.67/117.70 cnf(332,plain, % 117.67/117.70 (E(a1,f18(a1))), % 117.67/117.70 inference(scs_inference,[],[331,2])). % 117.67/117.70 cnf(336,plain, % 117.67/117.70 (P1(f18(a1))), % 117.67/117.70 inference(scs_inference,[],[27,87,331,35,2,108,3,21,14])). % 117.67/117.70 cnf(339,plain, % 117.67/117.70 (~P6(x3391,f18(a1))), % 117.67/117.70 inference(scs_inference,[],[27,87,331,268,35,44,2,108,3,21,14,23,24,64])). % 117.67/117.70 cnf(343,plain, % 117.67/117.70 (~P3(f18(a1))+P3(a1)), % 117.67/117.70 inference(scs_inference,[],[27,87,331,268,35,44,2,108,3,21,14,23,24,64,73,22])). % 117.67/117.70 cnf(359,plain, % 117.67/117.70 (~P1(f12(a14))), % 117.67/117.70 inference(scs_inference,[],[84,61,64])). % 117.67/117.70 cnf(360,plain, % 117.67/117.70 (P6(f9(f12(a14)),f12(a14))), % 117.67/117.70 inference(scs_inference,[],[359,48,67])). % 117.67/117.70 cnf(412,plain, % 117.67/117.70 (P2(f12(a14),f16(a14))), % 117.67/117.70 inference(scs_inference,[],[87,65,55])). % 117.67/117.70 cnf(413,plain, % 117.67/117.70 (P8(f12(a14),a14)), % 117.67/117.70 inference(scs_inference,[],[412,70])). % 117.67/117.70 cnf(415,plain, % 117.67/117.70 (~P6(x4151,f9(f16(a13)))), % 117.67/117.70 inference(scs_inference,[],[30,412,48,70,75])). % 117.67/117.70 cnf(418,plain, % 117.67/117.70 (P6(f12(a14),f16(a14))), % 117.67/117.70 inference(scs_inference,[],[30,52,412,48,70,75,67])). % 117.67/117.70 cnf(423,plain, % 117.67/117.70 (~P6(f16(a14),f12(a14))), % 117.67/117.70 inference(scs_inference,[],[30,360,52,412,48,70,75,67,76,69])). % 117.67/117.70 cnf(425,plain, % 117.67/117.70 (P8(f9(f16(a13)),x4251)), % 117.67/117.70 inference(scs_inference,[],[30,360,52,412,48,70,75,67,76,69,73])). % 117.67/117.70 cnf(427,plain, % 117.67/117.70 (P2(f12(a14),x4271)+~E(f16(a14),x4271)), % 117.67/117.70 inference(scs_inference,[],[30,360,52,412,48,70,75,67,76,69,73,20])). % 117.67/117.70 cnf(430,plain, % 117.67/117.70 (P8(f12(a14),x4301)+~E(a14,x4301)), % 117.67/117.70 inference(scs_inference,[],[30,54,360,52,412,48,70,75,67,76,69,73,20,15,17,18])). % 117.67/117.70 cnf(436,plain, % 117.67/117.70 (P6(f9(f12(a14)),a14)), % 117.67/117.70 inference(scs_inference,[],[360,413,74])). % 117.67/117.70 cnf(438,plain, % 117.67/117.70 (~P2(f16(a14),f12(a14))), % 117.67/117.70 inference(scs_inference,[],[360,413,359,423,74,67])). % 117.67/117.70 cnf(497,plain, % 117.67/117.70 (P8(x4971,a14)+~E(f9(f12(a14)),f10(x4971,a14))), % 117.67/117.70 inference(scs_inference,[],[436,15,78])). % 117.67/117.70 cnf(499,plain, % 117.67/117.70 (~P6(a14,f10(x4991,a14))+~E(f9(f12(a14)),f10(x4991,a14))), % 117.67/117.70 inference(scs_inference,[],[436,15,78,69])). % 117.67/117.70 cnf(517,plain, % 117.67/117.70 (E(f9(f18(a1)),f9(a1))), % 117.67/117.70 inference(scs_inference,[],[332,5,2])). % 117.67/117.70 cnf(518,plain, % 117.67/117.70 (E(f9(a1),f9(f18(a1)))), % 117.67/117.70 inference(scs_inference,[],[517,2])). % 117.67/117.70 cnf(579,plain, % 117.67/117.70 (E(f16(f18(a1)),f16(a1))), % 117.67/117.70 inference(scs_inference,[],[332,8,2])). % 117.67/117.70 cnf(580,plain, % 117.67/117.70 (E(f16(a1),f16(f18(a1)))), % 117.67/117.70 inference(scs_inference,[],[579,2])). % 117.67/117.70 cnf(586,plain, % 117.67/117.70 (P2(x5861,f16(f18(a1)))+~E(f9(f16(a1)),x5861)), % 117.67/117.70 inference(scs_inference,[],[579,2,108,24,21,23,22,19])). % 117.67/117.70 cnf(619,plain, % 117.67/117.70 (~E(f19(a7,f17(f10(a8,f18(a7)))),a1)), % 117.67/117.70 inference(scs_inference,[],[54,72,73])). % 117.67/117.70 cnf(634,plain, % 117.67/117.70 (~E(f10(x6341,a14),f9(f12(a14)))+P8(x6341,a14)), % 117.67/117.70 inference(scs_inference,[],[497,2])). % 117.67/117.70 cnf(640,plain, % 117.67/117.70 (~E(x6401,f9(f12(a14)))+~E(f10(x6402,a14),x6401)+P8(x6402,a14)), % 117.67/117.70 inference(scs_inference,[],[634,3])). % 117.67/117.70 cnf(667,plain, % 117.67/117.70 (~E(f10(x6671,a14),f9(f12(a14)))+~P6(a14,f10(x6671,a14))), % 117.67/117.70 inference(scs_inference,[],[499,2])). % 117.67/117.70 cnf(673,plain, % 117.67/117.70 (~E(x6731,f9(f12(a14)))+~E(f10(x6732,a14),x6731)+~P6(a14,f10(x6732,a14))), % 117.67/117.70 inference(scs_inference,[],[667,3])). % 117.67/117.70 cnf(712,plain, % 117.67/117.70 (~E(f9(f12(a14)),x7121)+~E(f10(x7122,a14),x7121)+~P6(a14,f10(x7122,a14))), % 117.67/117.70 inference(scs_inference,[],[673,2])). % 117.67/117.70 cnf(835,plain, % 117.67/117.70 (P3(a1)), % 117.67/117.70 inference(scs_inference,[],[336,56,343])). % 117.67/117.70 cnf(909,plain, % 117.67/117.70 (E(f10(f18(a1),x9091),f10(a1,x9091))), % 117.67/117.70 inference(scs_inference,[],[336,55,6])). % 117.67/117.70 cnf(910,plain, % 117.67/117.70 (E(f10(a1,x9101),f10(f18(a1),x9101))), % 117.67/117.70 inference(scs_inference,[],[909,2])). % 117.67/117.70 cnf(959,plain, % 117.67/117.70 (E(f18(f18(a1)),a1)), % 117.67/117.70 inference(scs_inference,[],[336,55,59])). % 117.67/117.70 cnf(963,plain, % 117.67/117.70 (P1(f18(f18(a1)))), % 117.67/117.70 inference(scs_inference,[],[87,959,27,2,108,3,14])). % 117.67/117.70 cnf(967,plain, % 117.67/117.70 (~P6(x9671,f18(f18(a1)))), % 117.67/117.70 inference(scs_inference,[],[518,87,959,268,27,44,2,108,3,14,24,23,19,64])). % 117.67/117.70 cnf(974,plain, % 117.67/117.70 (E(f10(x9741,f18(a1)),f10(x9741,a1))), % 117.67/117.70 inference(scs_inference,[],[336,55,7])). % 117.67/117.71 cnf(975,plain, % 117.67/117.71 (E(f10(x9751,a1),f10(x9751,f18(a1)))), % 117.67/117.71 inference(scs_inference,[],[974,2])). % 117.67/117.71 cnf(1210,plain, % 117.67/117.71 (~P8(a14,a1)), % 117.67/117.71 inference(scs_inference,[],[84,82,74])). % 117.67/117.71 cnf(1214,plain, % 117.67/117.71 (~P8(a14,a2)), % 117.67/117.71 inference(scs_inference,[],[84,115,74])). % 117.67/117.71 cnf(1218,plain, % 117.67/117.71 (~P8(a14,a13)), % 117.67/117.71 inference(scs_inference,[],[84,172,74])). % 117.67/117.71 cnf(1234,plain, % 117.67/117.71 (~P8(a5,a1)), % 117.67/117.71 inference(scs_inference,[],[122,82,74])). % 117.67/117.71 cnf(1238,plain, % 117.67/117.71 (~P8(a5,a2)), % 117.67/117.71 inference(scs_inference,[],[122,115,74])). % 117.67/117.71 cnf(1242,plain, % 117.67/117.71 (~P8(a5,a13)), % 117.67/117.71 inference(scs_inference,[],[122,172,74])). % 117.67/117.71 cnf(1257,plain, % 117.67/117.71 (~P8(f16(x12571),a1)), % 117.67/117.71 inference(scs_inference,[],[151,82,74])). % 117.67/117.71 cnf(1260,plain, % 117.67/117.71 (~P8(f16(x12601),a2)), % 117.67/117.71 inference(scs_inference,[],[151,115,74])). % 117.67/117.71 cnf(1264,plain, % 117.67/117.71 (~P8(f16(x12641),a13)), % 117.67/117.71 inference(scs_inference,[],[151,172,74])). % 117.67/117.71 cnf(1280,plain, % 117.67/117.71 (~P8(a8,a1)), % 117.67/117.71 inference(scs_inference,[],[177,82,74])). % 117.67/117.71 cnf(1284,plain, % 117.67/117.71 (~P8(a8,a2)), % 117.67/117.71 inference(scs_inference,[],[177,115,74])). % 117.67/117.71 cnf(1288,plain, % 117.67/117.71 (~P8(a8,a13)), % 117.67/117.71 inference(scs_inference,[],[177,172,74])). % 117.67/117.71 cnf(1299,plain, % 117.67/117.71 (~P8(f17(x12991),f9(f16(a2)))), % 117.67/117.71 inference(scs_inference,[],[196,269,74])). % 117.67/117.71 cnf(1303,plain, % 117.67/117.71 (~P8(f17(x13031),a1)), % 117.67/117.71 inference(scs_inference,[],[196,82,74])). % 117.67/117.71 cnf(1307,plain, % 117.67/117.71 (~P8(f17(x13071),a2)), % 117.67/117.71 inference(scs_inference,[],[196,115,74])). % 117.67/117.71 cnf(1311,plain, % 117.67/117.71 (~P8(f17(x13111),a13)), % 117.67/117.71 inference(scs_inference,[],[196,172,74])). % 117.67/117.71 cnf(1322,plain, % 117.67/117.71 (~P8(f12(a14),f9(f16(a2)))), % 117.67/117.71 inference(scs_inference,[],[360,269,74])). % 117.67/117.71 cnf(1326,plain, % 117.67/117.71 (~P8(f12(a14),a1)), % 117.67/117.71 inference(scs_inference,[],[360,82,74])). % 117.67/117.71 cnf(1330,plain, % 117.67/117.71 (~P8(f12(a14),a2)), % 117.67/117.71 inference(scs_inference,[],[360,115,74])). % 117.67/117.71 cnf(1334,plain, % 117.67/117.71 (~P8(f12(a14),a13)), % 117.67/117.71 inference(scs_inference,[],[360,172,74])). % 117.67/117.71 cnf(1623,plain, % 117.67/117.71 (~P8(a14,a11)), % 117.67/117.71 inference(scs_inference,[],[143,84,74])). % 117.67/117.71 cnf(1626,plain, % 117.67/117.71 (~P8(a5,a11)), % 117.67/117.71 inference(scs_inference,[],[143,122,74])). % 117.67/117.71 cnf(1629,plain, % 117.67/117.71 (~P8(f16(x16291),a11)), % 117.67/117.71 inference(scs_inference,[],[143,151,74])). % 117.67/117.71 cnf(1632,plain, % 117.67/117.71 (~P8(a8,a11)), % 117.67/117.71 inference(scs_inference,[],[143,177,74])). % 117.67/117.71 cnf(1635,plain, % 117.67/117.71 (~P8(f17(x16351),a11)), % 117.67/117.71 inference(scs_inference,[],[143,196,74])). % 117.67/117.71 cnf(1638,plain, % 117.67/117.71 (~P8(f12(a14),a11)), % 117.67/117.71 inference(scs_inference,[],[143,360,74])). % 117.67/117.71 cnf(1645,plain, % 117.67/117.71 (~P8(a14,f15(x16451))), % 117.67/117.71 inference(scs_inference,[],[191,84,74])). % 117.67/117.71 cnf(1649,plain, % 117.67/117.71 (~P8(a5,f15(x16491))), % 117.67/117.71 inference(scs_inference,[],[191,122,74])). % 117.67/117.71 cnf(1653,plain, % 117.67/117.71 (~P8(f16(x16531),f15(x16532))), % 117.67/117.71 inference(scs_inference,[],[191,151,74])). % 117.67/117.71 cnf(1657,plain, % 117.67/117.71 (~P8(a8,f15(x16571))), % 117.67/117.71 inference(scs_inference,[],[191,177,74])). % 117.67/117.71 cnf(1661,plain, % 117.67/117.71 (~P8(f17(x16611),f15(x16612))), % 117.67/117.71 inference(scs_inference,[],[191,196,74])). % 117.67/117.71 cnf(1665,plain, % 117.67/117.71 (~P8(f12(a14),f15(x16651))), % 117.67/117.71 inference(scs_inference,[],[191,360,74])). % 117.67/117.71 cnf(1708,plain, % 117.67/117.71 (~P1(f18(a14))), % 117.67/117.71 inference(scs_inference,[],[87,39,55,63])). % 117.67/117.71 cnf(1709,plain, % 117.67/117.71 (P6(f9(f18(a14)),f18(a14))), % 117.67/117.71 inference(scs_inference,[],[1708,48,67])). % 117.67/117.71 cnf(1712,plain, % 117.67/117.71 (~P8(f18(a14),f9(f16(a1)))), % 117.67/117.71 inference(scs_inference,[],[1708,92,48,67,74])). % 117.67/117.71 cnf(1739,plain, % 117.67/117.71 (~P8(f18(a14),a1)), % 117.67/117.71 inference(scs_inference,[],[1709,82,74])). % 117.67/117.71 cnf(1744,plain, % 117.67/117.71 (~P8(f18(a14),a2)), % 117.67/117.71 inference(scs_inference,[],[1709,115,74])). % 117.67/117.71 cnf(1749,plain, % 117.67/117.71 (~P8(f18(a14),a13)), % 117.67/117.71 inference(scs_inference,[],[1709,172,74])). % 117.67/117.71 cnf(1760,plain, % 117.67/117.71 (E(f19(f18(a1),x17601),f19(a1,x17601))), % 117.67/117.71 inference(scs_inference,[],[336,55,9])). % 117.67/117.71 cnf(1761,plain, % 117.67/117.71 (E(f19(a1,x17611),f19(f18(a1),x17611))), % 117.67/117.71 inference(scs_inference,[],[1760,2])). % 117.67/117.71 cnf(1766,plain, % 117.67/117.71 (P8(f19(a1,x17661),x17662)+~P1(f19(f18(a1),x17661))), % 117.67/117.71 inference(scs_inference,[],[1760,2,108,14,64,73])). % 117.67/117.71 cnf(1772,plain, % 117.67/117.71 (~P1(f19(a1,x17721))+P1(f19(f18(a1),x17721))), % 117.67/117.71 inference(scs_inference,[],[1761,14])). % 117.67/117.71 cnf(1773,plain, % 117.67/117.71 (~P1(f19(a1,x17731))+P8(f19(a1,x17731),x17732)), % 117.67/117.71 inference(scs_inference,[],[1761,14,1766])). % 117.67/117.71 cnf(1775,plain, % 117.67/117.71 (~P6(x17751,f19(f18(a1),x17752))+~P1(f19(a1,x17752))), % 117.67/117.71 inference(scs_inference,[],[1761,14,1766,64])). % 117.67/117.71 cnf(1777,plain, % 117.67/117.71 (P8(f19(f18(a1),x17771),x17772)+~P1(f19(a1,x17771))), % 117.67/117.71 inference(scs_inference,[],[1761,14,1766,64,73])). % 117.67/117.71 cnf(1782,plain, % 117.67/117.71 (~P7(f19(a1,x17821))+P7(f19(f18(a1),x17821))), % 117.67/117.71 inference(scs_inference,[],[1761,24])). % 117.67/117.71 cnf(1783,plain, % 117.67/117.71 (~P4(f19(a1,x17831))+P4(f19(f18(a1),x17831))), % 117.67/117.71 inference(scs_inference,[],[1761,24,21])). % 117.67/117.71 cnf(1784,plain, % 117.67/117.71 (~P3(f19(a1,x17841))+P3(f19(f18(a1),x17841))), % 117.67/117.71 inference(scs_inference,[],[1761,24,21,22])). % 117.67/117.71 cnf(1785,plain, % 117.67/117.71 (~P5(f19(a1,x17851))+P5(f19(f18(a1),x17851))), % 117.67/117.71 inference(scs_inference,[],[1761,24,21,22,23])). % 117.67/117.71 cnf(1793,plain, % 117.67/117.71 (~P1(f19(a1,x17931))+P2(f19(a1,x17931),f16(x17932))), % 117.67/117.71 inference(scs_inference,[],[1773,68])). % 117.67/117.71 cnf(1794,plain, % 117.67/117.71 (~P8(a14,f18(a1))), % 117.67/117.71 inference(scs_inference,[],[339,84,74])). % 117.67/117.71 cnf(1800,plain, % 117.67/117.71 (~P8(a5,f18(a1))), % 117.67/117.71 inference(scs_inference,[],[339,122,74])). % 117.67/117.71 cnf(1803,plain, % 117.67/117.71 (~P8(f16(x18031),f18(a1))), % 117.67/117.71 inference(scs_inference,[],[339,151,74])). % 117.67/117.71 cnf(1807,plain, % 117.67/117.71 (~P8(a8,f18(a1))), % 117.67/117.71 inference(scs_inference,[],[339,177,74])). % 117.67/117.71 cnf(1810,plain, % 117.67/117.71 (~P8(f17(x18101),f18(a1))), % 117.67/117.71 inference(scs_inference,[],[339,196,74])). % 117.67/117.71 cnf(1814,plain, % 117.67/117.71 (~P8(f12(a14),f18(a1))), % 117.67/117.71 inference(scs_inference,[],[339,360,74])). % 117.67/117.71 cnf(1817,plain, % 117.67/117.71 (~P8(f18(a14),f18(a1))), % 117.67/117.71 inference(scs_inference,[],[339,1709,74])). % 117.67/117.71 cnf(1823,plain, % 117.67/117.71 (~P1(f19(a1,x18231))+P2(f19(f18(a1),x18231),f16(x18232))), % 117.67/117.71 inference(scs_inference,[],[1777,68])). % 117.67/117.71 cnf(1824,plain, % 117.67/117.71 (P6(f19(a1,x18241),f16(x18242))+~P1(f19(a1,x18241))), % 117.67/117.71 inference(scs_inference,[],[52,1793,67])). % 117.67/117.71 cnf(1826,plain, % 117.67/117.71 (P6(f19(f18(a1),x18261),f16(x18262))+~P1(f19(a1,x18261))), % 117.67/117.71 inference(scs_inference,[],[1761,1824,15])). % 117.67/117.71 cnf(1831,plain, % 117.67/117.71 (~P1(f19(a1,x18311))+~P2(f16(x18312),f16(f18(a1)))), % 117.67/117.71 inference(scs_inference,[],[336,1826,75])). % 117.67/117.71 cnf(1832,plain, % 117.67/117.71 (~P6(f16(x18321),f16(f18(a1)))+~P1(f19(a1,x18322))), % 117.67/117.71 inference(scs_inference,[],[1831,66])). % 117.67/117.71 cnf(1855,plain, % 117.67/117.71 (E(f19(x18551,f18(a1)),f19(x18551,a1))), % 117.67/117.71 inference(scs_inference,[],[336,55,10])). % 117.67/117.71 cnf(2251,plain, % 117.67/117.71 (~E(a1,f18(a14))), % 117.67/117.71 inference(scs_inference,[],[1712,112,17])). % 117.67/117.71 cnf(2351,plain, % 117.67/117.71 (~P8(f18(a14),a11)), % 117.67/117.71 inference(scs_inference,[],[143,1709,74])). % 117.67/117.71 cnf(2363,plain, % 117.67/117.71 (~P8(f18(a14),f15(x23631))), % 117.67/117.71 inference(scs_inference,[],[191,1709,74])). % 117.67/117.71 cnf(2456,plain, % 117.67/117.71 (E(f18(f18(a1)),f18(a1))), % 117.67/117.71 inference(scs_inference,[],[336,55,12])). % 117.67/117.71 cnf(2457,plain, % 117.67/117.71 (E(f18(a1),f18(f18(a1)))), % 117.67/117.71 inference(scs_inference,[],[2456,2])). % 117.67/117.71 cnf(2458,plain, % 117.67/117.71 (E(f12(f18(a1)),f12(a1))), % 117.67/117.71 inference(scs_inference,[],[336,55,13])). % 117.67/117.71 cnf(2459,plain, % 117.67/117.71 (E(f12(a1),f12(f18(a1)))), % 117.67/117.71 inference(scs_inference,[],[2458,2])). % 117.67/117.71 cnf(2526,plain, % 117.67/117.71 (P2(f12(f12(a8)),f16(f12(a8)))), % 117.67/117.71 inference(scs_inference,[],[160,61,65])). % 117.67/117.71 cnf(2527,plain, % 117.67/117.71 (P8(f12(f12(a8)),f12(a8))), % 117.67/117.71 inference(scs_inference,[],[2526,70])). % 117.67/117.71 cnf(2597,plain, % 117.67/117.71 (~E(f18(a1),f12(a8))), % 117.67/117.71 inference(scs_inference,[],[160,336,61,14])). % 117.67/117.71 cnf(2598,plain, % 117.67/117.71 (~P1(f12(a8))), % 117.67/117.71 inference(scs_inference,[],[336,2597,58])). % 117.67/117.71 cnf(2600,plain, % 117.67/117.71 (P6(f9(f12(a8)),f12(a8))), % 117.67/117.71 inference(scs_inference,[],[336,2597,48,58,67])). % 117.67/117.71 cnf(2603,plain, % 117.67/117.71 (~P8(f12(a8),a2)), % 117.67/117.71 inference(scs_inference,[],[336,115,2597,48,58,67,74])). % 117.67/117.71 cnf(2604,plain, % 117.67/117.71 (~P6(x26041,a2)), % 117.67/117.71 inference(rename_variables,[],[115])). % 117.67/117.71 cnf(2607,plain, % 117.67/117.71 (~E(f12(a8),a2)), % 117.67/117.71 inference(scs_inference,[],[336,115,2604,2597,48,58,67,74,15,16])). % 117.67/117.71 cnf(2621,plain, % 117.67/117.71 (~P8(f12(a8),a13)), % 117.67/117.71 inference(scs_inference,[],[2600,172,69,74])). % 117.67/117.71 cnf(2622,plain, % 117.67/117.71 (~P6(x26221,a13)), % 117.67/117.71 inference(rename_variables,[],[172])). % 117.67/117.71 cnf(2624,plain, % 117.67/117.71 (~E(f12(a8),a13)), % 117.67/117.71 inference(scs_inference,[],[2600,172,2622,69,74,16])). % 117.67/117.71 cnf(2626,plain, % 117.67/117.71 (~P8(f12(a8),f9(f16(a11)))), % 117.67/117.71 inference(scs_inference,[],[2600,148,74])). % 117.67/117.71 cnf(2636,plain, % 117.67/117.71 (~P8(f12(a8),a1)), % 117.67/117.71 inference(scs_inference,[],[2600,82,74])). % 117.67/117.71 cnf(2637,plain, % 117.67/117.71 (~P6(x26371,a1)), % 117.67/117.71 inference(rename_variables,[],[82])). % 117.67/117.71 cnf(2639,plain, % 117.67/117.71 (~E(f12(a8),a1)), % 117.67/117.71 inference(scs_inference,[],[2600,82,2637,74,16])). % 117.67/117.71 cnf(2642,plain, % 117.67/117.71 (~P8(f12(a8),f18(f18(a1)))), % 117.67/117.71 inference(scs_inference,[],[967,2600,74])). % 117.67/117.71 cnf(2643,plain, % 117.67/117.71 (~P6(x26431,f18(f18(a1)))), % 117.67/117.71 inference(rename_variables,[],[967])). % 117.67/117.71 cnf(2645,plain, % 117.67/117.71 (~E(f12(a8),f18(f18(a1)))), % 117.67/117.71 inference(scs_inference,[],[967,2643,2600,74,16])). % 117.67/117.71 cnf(2661,plain, % 117.67/117.71 (E(f19(a1,f17(x26611)),a1)), % 117.67/117.71 inference(scs_inference,[],[336,35,64,71])). % 117.67/117.71 cnf(2662,plain, % 117.67/117.71 (E(a1,f19(a1,f17(x26621)))), % 117.67/117.71 inference(scs_inference,[],[2661,2])). % 117.67/117.71 cnf(2664,plain, % 117.67/117.71 (P1(f19(a1,f17(x26641)))), % 117.67/117.71 inference(scs_inference,[],[87,2661,27,2,3,14])). % 117.67/117.71 cnf(2673,plain, % 117.67/117.71 (P8(f19(a1,f17(x26731)),x26732)), % 117.67/117.71 inference(scs_inference,[],[87,2661,268,35,835,27,44,2,3,14,24,21,22,23,1783,1782,1784,1785,1773])). % 117.67/117.71 cnf(2677,plain, % 117.67/117.71 (P1(f19(f18(a1),f17(x26771)))), % 117.67/117.71 inference(scs_inference,[],[87,2661,268,35,835,27,44,2,3,14,24,21,22,23,1783,1782,1784,1785,1773,1775,1772])). % 117.67/117.71 cnf(2678,plain, % 117.67/117.71 (~P2(f16(x26781),f16(f18(a1)))), % 117.67/117.71 inference(scs_inference,[],[87,2661,268,35,835,27,44,2,3,14,24,21,22,23,1783,1782,1784,1785,1773,1775,1772,1831])). % 117.67/117.71 cnf(2680,plain, % 117.67/117.71 (P2(f19(f18(a1),f17(x26801)),f16(x26802))), % 117.67/117.71 inference(scs_inference,[],[87,2661,268,35,835,27,44,2,3,14,24,21,22,23,1783,1782,1784,1785,1773,1775,1772,1831,1823])). % 117.67/117.71 cnf(2682,plain, % 117.67/117.71 (P8(f19(f18(a1),f17(x26821)),x26822)), % 117.67/117.71 inference(scs_inference,[],[87,2661,268,35,835,27,44,2,3,14,24,21,22,23,1783,1782,1784,1785,1773,1775,1772,1831,1823,1777])). % 117.67/117.71 cnf(2684,plain, % 117.67/117.71 (~P6(f16(x26841),f16(f18(a1)))), % 117.67/117.71 inference(scs_inference,[],[87,2661,268,35,835,27,44,2,3,14,24,21,22,23,1783,1782,1784,1785,1773,1775,1772,1831,1823,1777,1832])). % 117.67/117.71 cnf(2686,plain, % 117.67/117.71 (P6(f19(f18(a1),f17(x26861)),f16(x26862))), % 117.67/117.71 inference(scs_inference,[],[87,2661,268,35,835,27,44,2,3,14,24,21,22,23,1783,1782,1784,1785,1773,1775,1772,1831,1823,1777,1832,1826])). % 117.67/117.71 cnf(2690,plain, % 117.67/117.71 (~P6(x26901,f19(a1,f17(x26902)))), % 117.67/117.71 inference(scs_inference,[],[87,2661,268,35,835,27,44,2,3,14,24,21,22,23,1783,1782,1784,1785,1773,1775,1772,1831,1823,1777,1832,1826,1793,64])). % 117.67/117.71 cnf(2695,plain, % 117.67/117.71 (~E(f19(f18(a1),f17(x26951)),f16(x26952))), % 117.67/117.71 inference(scs_inference,[],[1761,87,2661,268,35,835,27,44,2,3,14,24,21,22,23,1783,1782,1784,1785,1773,1775,1772,1831,1823,1777,1832,1826,1793,64,108,20,15])). % 117.67/117.71 cnf(2696,plain, % 117.67/117.71 (~E(f19(a1,f17(x26961)),f16(x26962))), % 117.67/117.71 inference(scs_inference,[],[1761,87,2661,268,35,835,27,44,2,3,14,24,21,22,23,1783,1782,1784,1785,1773,1775,1772,1831,1823,1777,1832,1826,1793,64,108,20,15,19])). % 117.67/117.71 cnf(2734,plain, % 117.67/117.71 (~E(f19(a1,f17(x27341)),f17(x27342))), % 117.67/117.71 inference(scs_inference,[],[1299,2673,17])). % 117.67/117.71 cnf(2736,plain, % 117.67/117.71 (~E(f19(f18(a1),f17(x27361)),f17(x27362))), % 117.67/117.71 inference(scs_inference,[],[1299,2682,17])). % 117.67/117.71 cnf(2746,plain, % 117.67/117.71 (~E(f19(f18(a1),f17(x27461)),f12(a14))), % 117.67/117.71 inference(scs_inference,[],[1322,2682,17])). % 117.67/117.71 cnf(2752,plain, % 117.67/117.71 (P4(f18(a2))), % 117.67/117.71 inference(scs_inference,[],[28,60])). % 117.67/117.71 cnf(2754,plain, % 117.67/117.71 (~P1(f12(f12(a8)))), % 117.67/117.71 inference(scs_inference,[],[2598,28,60,61])). % 117.67/117.71 cnf(2760,plain, % 117.67/117.71 (P1(f18(a2))), % 117.67/117.71 inference(scs_inference,[],[2598,2664,1708,28,60,61,65,1824,59])). % 117.67/117.71 cnf(2762,plain, % 117.67/117.71 (E(f19(f18(a1),f17(x27621)),a1)), % 117.67/117.71 inference(scs_inference,[],[2598,2677,2664,1708,28,60,61,65,1824,59,55])). % 117.67/117.71 cnf(2764,plain, % 117.67/117.71 (P2(x27641,f16(x27641))), % 117.67/117.71 inference(scs_inference,[],[2598,2677,2664,1708,47,28,60,61,65,1824,59,55,68])). % 117.67/117.71 cnf(2766,plain, % 117.67/117.71 (P4(f15(x27661))), % 117.67/117.71 inference(scs_inference,[],[2598,2677,2664,1708,47,28,46,60,61,65,1824,59,55,68,57])). % 117.67/117.71 cnf(2768,plain, % 117.67/117.71 (~P2(a14,f16(a1))), % 117.67/117.71 inference(scs_inference,[],[1210,2598,2677,2664,1708,47,28,46,60,61,65,1824,59,55,68,57,70])). % 117.67/117.71 cnf(2772,plain, % 117.67/117.71 (~P6(f10(a8,f18(a7)),f18(a7))), % 117.67/117.71 inference(scs_inference,[],[1210,2598,2677,2664,1708,47,28,46,54,60,61,65,1824,59,55,68,57,70,56,78])). % 117.67/117.71 cnf(2774,plain, % 117.67/117.71 (P6(f10(a14,a1),a14)), % 117.67/117.71 inference(scs_inference,[],[1210,2598,2677,2664,1708,47,28,46,54,60,61,65,1824,59,55,68,57,70,56,78,73])). % 117.67/117.71 cnf(2777,plain, % 117.67/117.71 (~P2(f16(x27771),f16(a2))), % 117.67/117.71 inference(scs_inference,[],[1210,2624,2598,2686,2677,2664,1708,47,28,46,54,60,61,65,1824,59,55,68,57,70,56,78,73,2,75])). % 117.67/117.71 cnf(2779,plain, % 117.67/117.71 (P1(f9(f16(a1)))), % 117.67/117.71 inference(scs_inference,[],[1210,2624,2598,2686,2677,2664,1708,47,28,46,92,48,54,60,61,65,1824,59,55,68,57,70,56,78,73,2,75,67])). % 117.67/117.71 cnf(2783,plain, % 117.67/117.71 (~E(f19(a1,f17(x27831)),f18(a14))), % 117.67/117.71 inference(scs_inference,[],[1210,2624,2598,2686,2677,2664,2662,2251,1708,47,28,46,92,48,54,60,61,65,1824,59,55,68,57,70,56,78,73,2,75,67,3])). % 117.67/117.71 cnf(2784,plain, % 117.67/117.71 (~E(f19(f18(a1),f17(x27841)),f12(a8))), % 117.67/117.71 inference(scs_inference,[],[1210,2624,2598,2686,2677,2664,2662,2251,1708,47,28,46,92,48,54,60,61,65,1824,59,55,68,57,70,56,78,73,2,75,67,3,14])). % 117.67/117.71 cnf(2785,plain, % 117.67/117.71 (~P2(f16(x27851),f16(a1))), % 117.67/117.71 inference(scs_inference,[],[1210,2624,2598,2686,2677,2678,2664,2662,2251,1708,47,28,46,92,48,580,54,60,61,65,1824,59,55,68,57,70,56,78,73,2,75,67,3,14,20])). % 117.67/117.71 cnf(2786,plain, % 117.67/117.71 (~P8(a14,f19(a1,f17(x27861)))), % 117.67/117.71 inference(scs_inference,[],[1210,2624,2598,2686,2677,2678,2664,2662,2251,1708,47,2661,28,46,92,48,580,54,60,61,65,1824,59,55,68,57,70,56,78,73,2,75,67,3,14,20,18])). % 117.67/117.71 cnf(2787,plain, % 117.67/117.71 (~E(f9(f16(a13)),f12(a8))), % 117.67/117.71 inference(scs_inference,[],[1210,2621,2624,2598,2686,2677,2678,2664,2662,2251,1708,79,47,2661,28,46,92,48,580,54,60,61,65,1824,59,55,68,57,70,56,78,73,2,75,67,3,14,20,18,17])). % 117.67/117.71 cnf(2789,plain, % 117.67/117.71 (~P6(f16(x27891),f16(a1))), % 117.67/117.71 inference(scs_inference,[],[1210,2621,2624,2598,2686,2677,2678,2684,2664,2662,2251,1708,79,47,2661,28,46,92,48,580,54,60,61,65,1824,59,55,68,57,70,56,78,73,2,75,67,3,14,20,18,17,16])). % 117.67/117.71 cnf(2792,plain, % 117.67/117.71 (P2(f10(a14,a1),a14)), % 117.67/117.71 inference(scs_inference,[],[1210,37,2621,2624,2598,2686,2677,2678,2684,2664,2662,2251,1708,79,47,2661,28,46,92,48,580,54,60,61,65,1824,59,55,68,57,70,56,78,73,2,75,67,3,14,20,18,17,16,62,66])). % 117.67/117.71 cnf(2794,plain, % 117.67/117.71 (~P6(a14,f10(a14,a1))), % 117.67/117.71 inference(scs_inference,[],[1210,37,2621,2624,2598,2686,2677,2678,2684,2664,2662,2251,1708,79,47,2661,28,46,92,48,580,54,60,61,65,1824,59,55,68,57,70,56,78,73,2,75,67,3,14,20,18,17,16,62,66,69])). % 117.67/117.71 cnf(2804,plain, % 117.67/117.71 (~P1(f12(a5))), % 117.67/117.71 inference(scs_inference,[],[51,61])). % 117.67/117.71 cnf(2808,plain, % 117.67/117.71 (P1(f18(f18(a2)))), % 117.67/117.71 inference(scs_inference,[],[2760,51,61,60,59])). % 117.67/117.71 cnf(2810,plain, % 117.67/117.71 (E(f18(a2),a1)), % 117.67/117.71 inference(scs_inference,[],[2760,51,61,60,59,55])). % 117.67/117.71 cnf(2812,plain, % 117.67/117.71 (P2(f12(a5),f16(a5))), % 117.67/117.71 inference(scs_inference,[],[2760,51,61,60,59,55,65])). % 117.67/117.71 cnf(2814,plain, % 117.67/117.71 (E(f12(f18(a2)),f12(a1))), % 117.67/117.71 inference(scs_inference,[],[2760,51,61,60,59,55,65,13])). % 117.67/117.71 cnf(2815,plain, % 117.67/117.71 (P2(f9(f16(a13)),f16(x28151))), % 117.67/117.71 inference(scs_inference,[],[2760,51,425,61,60,59,55,65,13,68])). % 117.67/117.71 cnf(2817,plain, % 117.67/117.71 (~P2(a14,f16(a2))), % 117.67/117.71 inference(scs_inference,[],[1214,2760,51,425,61,60,59,55,65,13,68,70])). % 117.67/117.71 cnf(2819,plain, % 117.67/117.71 (P4(f9(f16(a1)))), % 117.67/117.71 inference(scs_inference,[],[1214,2760,2779,51,425,61,60,59,55,65,13,68,70,57])). % 117.67/117.71 cnf(2823,plain, % 117.67/117.71 (P6(f10(a14,a2),a14)), % 117.67/117.71 inference(scs_inference,[],[1214,2760,2779,51,425,61,60,59,55,65,13,68,70,57,56,73])). % 117.67/117.71 cnf(2828,plain, % 117.67/117.71 (P1(f9(f16(a13)))), % 117.67/117.71 inference(scs_inference,[],[1214,2639,2760,2774,2779,51,425,415,48,61,60,59,55,65,13,68,70,57,56,73,2,75,67])). % 117.67/117.71 cnf(2830,plain, % 117.67/117.71 (P2(f9(x28301),x28301)), % 117.67/117.71 inference(rename_variables,[],[48])). % 117.67/117.71 cnf(2832,plain, % 117.67/117.71 (E(f18(a2),f19(a1,f17(x28321)))), % 117.67/117.71 inference(scs_inference,[],[1214,2639,2760,2774,2779,2662,51,425,415,48,61,60,59,55,65,13,68,70,57,56,73,2,75,67,3])). % 117.67/117.71 cnf(2834,plain, % 117.67/117.71 (P2(x28341,f16(x28341))), % 117.67/117.71 inference(rename_variables,[],[2764])). % 117.67/117.71 cnf(2836,plain, % 117.67/117.71 (~E(f18(a2),f12(f12(a8)))), % 117.67/117.71 inference(scs_inference,[],[1214,2764,2777,2639,2760,2774,2754,2779,2662,51,425,415,48,61,60,59,55,65,13,68,70,57,56,73,2,75,67,3,76,14])). % 117.67/117.71 cnf(2839,plain, % 117.67/117.71 (~P8(a5,f19(f18(a1),f17(x28391)))), % 117.67/117.71 inference(scs_inference,[],[1214,1234,2764,2777,2639,2760,2774,2754,2779,2762,2662,51,425,415,48,2830,61,60,59,55,65,13,68,70,57,56,73,2,75,67,3,76,14,20,18])). % 117.67/117.71 cnf(2840,plain, % 117.67/117.71 (~E(f18(a2),a14)), % 117.67/117.71 inference(scs_inference,[],[1214,1234,2764,2834,2777,2639,2760,2774,2754,2779,2762,2662,51,425,415,48,2830,61,60,59,55,65,13,68,70,57,56,73,2,75,67,3,76,14,20,18,19])). % 117.67/117.71 cnf(2842,plain, % 117.67/117.71 (P8(f19(x28421,a1),f19(x28421,f18(a1)))), % 117.67/117.71 inference(scs_inference,[],[1214,1234,2764,2834,2777,2639,2760,2774,2754,2779,2762,2662,51,47,425,1855,415,48,2830,61,60,59,55,65,13,68,70,57,56,73,2,75,67,3,76,14,20,18,19,17])). % 117.67/117.71 cnf(2849,plain, % 117.67/117.71 (E(f10(f18(a2),x28491),f10(a1,x28491))), % 117.67/117.71 inference(scs_inference,[],[1214,1234,2764,2834,2777,2639,2760,2794,2774,2754,2779,2762,2662,51,47,425,1855,974,415,48,2830,61,60,59,55,65,13,68,70,57,56,73,2,75,67,3,76,14,20,18,19,17,16,4,5,11,6])). % 117.67/117.71 cnf(2850,plain, % 117.67/117.71 (E(f10(x28501,f18(a2)),f10(x28501,a1))), % 117.67/117.71 inference(scs_inference,[],[1214,1234,2764,2834,2777,2639,2760,2794,2774,2754,2779,2762,2662,51,47,425,1855,974,415,48,2830,61,60,59,55,65,13,68,70,57,56,73,2,75,67,3,76,14,20,18,19,17,16,4,5,11,6,7])). % 117.67/117.71 cnf(2851,plain, % 117.67/117.71 (E(f19(f18(a2),x28511),f19(a1,x28511))), % 117.67/117.71 inference(scs_inference,[],[1214,1234,2764,2834,2777,2639,2760,2794,2774,2754,2779,2762,2662,51,47,425,1855,974,415,48,2830,61,60,59,55,65,13,68,70,57,56,73,2,75,67,3,76,14,20,18,19,17,16,4,5,11,6,7,9])). % 117.67/117.71 cnf(2852,plain, % 117.67/117.71 (E(f19(x28521,f18(a2)),f19(x28521,a1))), % 117.67/117.71 inference(scs_inference,[],[1214,1234,2764,2834,2777,2639,2760,2794,2774,2754,2779,2762,2662,51,47,425,1855,974,415,48,2830,61,60,59,55,65,13,68,70,57,56,73,2,75,67,3,76,14,20,18,19,17,16,4,5,11,6,7,9,10])). % 117.67/117.71 cnf(2853,plain, % 117.67/117.71 (E(f18(f18(a2)),f18(a1))), % 117.67/117.71 inference(scs_inference,[],[1214,1234,2764,2834,2777,2639,2760,2794,2774,2754,2779,2762,2662,51,47,425,1855,974,415,48,2830,61,60,59,55,65,13,68,70,57,56,73,2,75,67,3,76,14,20,18,19,17,16,4,5,11,6,7,9,10,12])). % 117.67/117.71 cnf(2854,plain, % 117.67/117.71 (E(f16(f18(a2)),f16(a1))), % 117.67/117.71 inference(scs_inference,[],[1214,1234,2764,2834,2777,2639,2760,2794,2774,2754,2779,2762,2662,51,47,425,1855,974,415,48,2830,61,60,59,55,65,13,68,70,57,56,73,2,75,67,3,76,14,20,18,19,17,16,4,5,11,6,7,9,10,12,8])). % 117.67/117.71 cnf(2866,plain, % 117.67/117.71 (~P1(f12(f12(a5)))), % 117.67/117.71 inference(scs_inference,[],[2804,61])). % 117.67/117.71 cnf(2868,plain, % 117.67/117.71 (P4(f18(a11))), % 117.67/117.71 inference(scs_inference,[],[2804,29,61,60])). % 117.67/117.71 cnf(2870,plain, % 117.67/117.71 (P2(f12(a8),f16(a8))), % 117.67/117.71 inference(scs_inference,[],[2804,29,160,61,60,65])). % 117.67/117.71 cnf(2872,plain, % 117.67/117.71 (P1(f18(a11))), % 117.67/117.71 inference(scs_inference,[],[2804,29,160,61,60,65,59])). % 117.67/117.71 cnf(2874,plain, % 117.67/117.71 (E(f18(f18(a2)),a1)), % 117.67/117.71 inference(scs_inference,[],[2804,2808,29,160,61,60,65,59,55])). % 117.67/117.71 cnf(2876,plain, % 117.67/117.71 (P2(a13,f16(x28761))), % 117.67/117.71 inference(scs_inference,[],[2804,2808,29,243,160,61,60,65,59,55,68])). % 117.67/117.71 cnf(2878,plain, % 117.67/117.71 (P4(f9(f16(a13)))), % 117.67/117.71 inference(scs_inference,[],[2804,2808,2828,29,243,160,61,60,65,59,55,68,57])). % 117.67/117.71 cnf(2889,plain, % 117.67/117.71 (P6(f12(a5),f16(a5))), % 117.67/117.71 inference(scs_inference,[],[2804,2812,2823,2607,2808,2828,1218,29,243,160,52,61,60,65,59,55,68,57,70,56,73,2,75,67])). % 117.67/117.71 cnf(2893,plain, % 117.67/117.71 (E(f10(f18(a2),x28931),f10(a1,x28931))), % 117.67/117.71 inference(rename_variables,[],[2849])). % 117.67/117.71 cnf(2896,plain, % 117.67/117.71 (P2(x28961,f16(x28961))), % 117.67/117.71 inference(rename_variables,[],[2764])). % 117.67/117.71 cnf(2898,plain, % 117.67/117.71 (~E(f18(f18(a2)),f12(a5))), % 117.67/117.71 inference(scs_inference,[],[2804,2812,2823,2607,2849,2850,2808,2828,1218,2764,29,243,160,52,61,60,65,59,55,68,57,70,56,73,2,75,67,3,76,14])). % 117.67/117.71 cnf(2899,plain, % 117.67/117.71 (~E(f16(a14),f16(a2))), % 117.67/117.71 inference(scs_inference,[],[2804,2812,2823,2607,2817,2849,2850,2808,2828,1218,2764,2896,29,243,160,52,61,60,65,59,55,68,57,70,56,73,2,75,67,3,76,14,20])). % 117.67/117.71 cnf(2901,plain, % 117.67/117.71 (~P8(f12(a8),f18(a1))), % 117.67/117.71 inference(scs_inference,[],[2804,2812,2823,2607,2817,2849,2850,2642,2808,2828,1218,2457,2764,2896,29,243,160,52,61,60,65,59,55,68,57,70,56,73,2,75,67,3,76,14,20,18])). % 117.67/117.71 cnf(2906,plain, % 117.67/117.71 (~P6(x29061,f18(a2))), % 117.67/117.71 inference(scs_inference,[],[2792,2804,2812,2823,2607,2810,2817,2849,2850,2642,2808,2828,1218,2603,2457,2764,2896,79,29,243,975,160,52,82,61,60,65,59,55,68,57,70,56,73,2,75,67,3,76,14,20,18,19,17,16])). % 117.67/117.71 cnf(2912,plain, % 117.67/117.71 (E(f19(a2,f17(x29121)),a1)), % 117.67/117.71 inference(scs_inference,[],[2792,2804,2812,2823,2607,2810,2817,2849,2893,2850,2642,2808,2828,1218,2603,2457,37,2764,2896,79,29,243,975,160,52,82,61,60,65,59,55,68,57,70,56,73,2,75,67,3,76,14,20,18,19,17,16,69,640,71])). % 117.67/117.71 cnf(2917,plain, % 117.67/117.71 (P4(f18(f18(a11)))), % 117.67/117.71 inference(scs_inference,[],[2872,60])). % 117.67/117.71 cnf(2919,plain, % 117.67/117.71 (~P1(f12(f18(a14)))), % 117.67/117.71 inference(scs_inference,[],[2872,1708,60,61])). % 117.67/117.71 cnf(2921,plain, % 117.67/117.71 (P2(a11,f16(x29211))), % 117.67/117.71 inference(scs_inference,[],[2872,1708,236,60,61,68])). % 117.67/117.71 cnf(2923,plain, % 117.67/117.71 (E(f18(a11),a1)), % 117.67/117.71 inference(scs_inference,[],[2872,1708,236,60,61,68,55])). % 117.67/117.71 cnf(2925,plain, % 117.67/117.71 (P1(f18(f18(a11)))), % 117.67/117.71 inference(scs_inference,[],[2872,1708,236,60,61,68,55,59])). % 117.67/117.71 cnf(2927,plain, % 117.67/117.71 (P3(f18(a11))), % 117.67/117.71 inference(scs_inference,[],[2872,1708,236,60,61,68,55,59,56])). % 117.67/117.71 cnf(2929,plain, % 117.67/117.71 (~P2(f12(a8),f16(f18(a1)))), % 117.67/117.71 inference(scs_inference,[],[2872,2901,1708,236,60,61,68,55,59,56,70])). % 117.67/117.71 cnf(2931,plain, % 117.67/117.71 (~P6(f16(a5),f12(a5))), % 117.67/117.71 inference(scs_inference,[],[2872,2889,2901,1708,236,60,61,68,55,59,56,70,69])). % 117.67/117.71 cnf(2933,plain, % 117.67/117.71 (P6(f10(f12(a8),f18(a1)),f12(a8))), % 117.67/117.71 inference(scs_inference,[],[2872,2889,2901,1708,236,60,61,68,55,59,56,70,69,73])). % 117.67/117.71 cnf(2935,plain, % 117.67/117.71 (~E(f16(a2),f16(a14))), % 117.67/117.71 inference(scs_inference,[],[2872,2889,2899,2901,1708,236,60,61,68,55,59,56,70,69,73,2])). % 117.67/117.71 cnf(2938,plain, % 117.67/117.71 (P1(f9(f16(a11)))), % 117.67/117.71 inference(scs_inference,[],[2872,2889,2899,2901,1708,236,148,48,60,61,68,55,59,56,70,69,73,2,75,67])). % 117.67/117.71 cnf(2942,plain, % 117.67/117.71 (~E(f18(a1),f12(a5))), % 117.67/117.71 inference(scs_inference,[],[2872,2889,2899,2901,2853,2898,1708,236,148,48,60,61,68,55,59,56,70,69,73,2,75,67,3])). % 117.67/117.71 cnf(2943,plain, % 117.67/117.71 (~E(f18(a11),f12(f12(a5)))), % 117.67/117.71 inference(scs_inference,[],[2872,2889,2899,2901,2853,2898,2866,1708,236,148,48,60,61,68,55,59,56,70,69,73,2,75,67,3,14])). % 117.67/117.71 cnf(2946,plain, % 117.67/117.71 (P8(x29461,x29461)), % 117.67/117.71 inference(rename_variables,[],[47])). % 117.67/117.71 cnf(2949,plain, % 117.67/117.71 (~E(f16(a5),f18(a2))), % 117.67/117.71 inference(scs_inference,[],[2906,2872,2889,2899,2901,2814,2853,2898,2866,2854,2785,1708,47,2946,236,148,48,60,61,68,55,59,56,70,69,73,2,75,67,3,14,20,18,17,16])). % 117.67/117.71 cnf(2951,plain, % 117.67/117.71 (~E(f9(f16(a1)),f12(a8))), % 117.67/117.71 inference(scs_inference,[],[2906,2872,2889,2899,2901,2814,2853,2898,2866,2854,2785,1708,47,2946,236,148,48,60,61,68,55,59,56,70,69,73,2,75,67,3,14,20,18,17,16,586])). % 117.67/117.71 cnf(2952,plain, % 117.67/117.71 (E(f18(f18(a11)),f18(a1))), % 117.67/117.71 inference(scs_inference,[],[2906,2872,2889,2899,2901,2814,2853,2898,2866,2854,2785,1708,47,2946,236,148,48,60,61,68,55,59,56,70,69,73,2,75,67,3,14,20,18,17,16,586,12])). % 117.67/117.71 cnf(2953,plain, % 117.67/117.71 (E(f19(x29531,f18(a11)),f19(x29531,a1))), % 117.67/117.71 inference(scs_inference,[],[2906,2872,2889,2899,2901,2814,2853,2898,2866,2854,2785,1708,47,2946,236,148,48,60,61,68,55,59,56,70,69,73,2,75,67,3,14,20,18,17,16,586,12,10])). % 117.67/117.71 cnf(2954,plain, % 117.67/117.71 (E(f9(f18(a11)),f9(a1))), % 117.67/117.71 inference(scs_inference,[],[2906,2872,2889,2899,2901,2814,2853,2898,2866,2854,2785,1708,47,2946,236,148,48,60,61,68,55,59,56,70,69,73,2,75,67,3,14,20,18,17,16,586,12,10,5])). % 117.67/117.71 cnf(2957,plain, % 117.67/117.71 (E(f10(x29571,f18(a11)),f10(x29571,a1))), % 117.67/117.71 inference(scs_inference,[],[2906,2872,2889,2899,2901,2814,2853,2898,2866,2854,2785,1708,47,2946,236,148,48,60,61,68,55,59,56,70,69,73,2,75,67,3,14,20,18,17,16,586,12,10,5,6,11,7])). % 117.67/117.71 cnf(2959,plain, % 117.67/117.71 (E(f19(f18(a11),x29591),f19(a1,x29591))), % 117.67/117.71 inference(scs_inference,[],[2906,2872,2889,2899,2901,2814,2853,2898,2866,2854,2785,1708,47,2946,236,148,48,60,61,68,55,59,56,70,69,73,2,75,67,3,14,20,18,17,16,586,12,10,5,6,11,7,4,9])). % 117.67/117.71 cnf(2960,plain, % 117.67/117.71 (E(f16(f18(a11)),f16(a1))), % 117.67/117.71 inference(scs_inference,[],[2906,2872,2889,2899,2901,2814,2853,2898,2866,2854,2785,1708,47,2946,236,148,48,60,61,68,55,59,56,70,69,73,2,75,67,3,14,20,18,17,16,586,12,10,5,6,11,7,4,9,8])). % 117.67/117.71 cnf(2961,plain, % 117.67/117.71 (P2(f10(f12(a8),f18(a1)),f12(a8))), % 117.67/117.71 inference(scs_inference,[],[2906,2872,2889,2899,2901,2814,2853,2898,2866,2854,2785,1708,47,2946,236,148,48,60,61,68,55,59,56,70,69,73,2,75,67,3,14,20,18,17,16,586,12,10,5,6,11,7,4,9,8,66])). % 117.67/117.71 cnf(2963,plain, % 117.67/117.71 (~E(f15(f18(a1)),f12(a8))), % 117.67/117.71 inference(scs_inference,[],[2906,2872,2889,2899,2901,2814,2853,2898,2866,2854,2785,1708,47,2946,236,148,48,60,61,68,55,59,56,70,69,73,2,75,67,3,14,20,18,17,16,586,12,10,5,6,11,7,4,9,8,66,137])). % 117.67/117.71 cnf(2970,plain, % 117.67/117.71 (P4(f18(a13))), % 117.67/117.71 inference(scs_inference,[],[30,60])). % 117.67/117.71 cnf(2972,plain, % 117.67/117.71 (~P1(f12(f12(a14)))), % 117.67/117.71 inference(scs_inference,[],[359,30,60,61])). % 117.67/117.71 cnf(2974,plain, % 117.67/117.71 (P2(a2,f16(x29741))), % 117.67/117.71 inference(scs_inference,[],[359,30,227,60,61,68])). % 117.67/117.71 cnf(2976,plain, % 117.67/117.71 (P1(f18(a13))), % 117.67/117.71 inference(scs_inference,[],[359,30,227,60,61,68,59])). % 117.67/117.71 cnf(2978,plain, % 117.67/117.71 (E(f18(f18(a11)),a1)), % 117.67/117.71 inference(scs_inference,[],[2925,359,30,227,60,61,68,59,55])). % 117.67/117.71 cnf(2980,plain, % 117.67/117.71 (P4(f9(f16(a11)))), % 117.67/117.71 inference(scs_inference,[],[2925,2938,359,30,227,60,61,68,59,55,57])). % 117.67/117.71 cnf(2982,plain, % 117.67/117.71 (P3(f18(f18(a11)))), % 117.67/117.71 inference(scs_inference,[],[2925,2938,359,30,227,60,61,68,59,55,57,56])). % 117.67/117.71 cnf(2984,plain, % 117.67/117.71 (~P2(a5,f16(a13))), % 117.67/117.71 inference(scs_inference,[],[2925,2938,1242,359,30,227,60,61,68,59,55,57,56,70])). % 117.67/117.71 cnf(2988,plain, % 117.67/117.71 (P6(f10(a5,a13),a5)), % 117.67/117.71 inference(scs_inference,[],[2933,2925,2938,1242,359,30,227,60,61,68,59,55,57,56,70,69,73])). % 117.67/117.71 cnf(2990,plain, % 117.67/117.71 (~E(f12(a5),f18(a1))), % 117.67/117.71 inference(scs_inference,[],[2942,2933,2925,2938,1242,359,30,227,60,61,68,59,55,57,56,70,69,73,2])). % 117.67/117.71 cnf(2991,plain, % 117.67/117.71 (~P2(f12(a8),f16(a13))), % 117.67/117.71 inference(scs_inference,[],[2942,2933,2925,2938,1242,359,30,227,60,61,68,59,55,57,56,70,69,73,2,75])). % 117.67/117.71 cnf(2993,plain, % 117.67/117.71 (P6(f12(a8),f16(a8))), % 117.67/117.71 inference(scs_inference,[],[2870,2942,2933,2925,2938,1242,359,30,227,52,60,61,68,59,55,57,56,70,69,73,2,75,67])). % 117.67/117.71 cnf(3000,plain, % 117.67/117.71 (~P2(f12(a8),f16(a1))), % 117.67/117.71 inference(scs_inference,[],[2870,2942,2923,2933,2919,2925,2938,2929,2943,1242,359,30,227,52,580,60,61,68,59,55,57,56,70,69,73,2,75,67,3,76,14,20])). % 117.67/117.71 cnf(3001,plain, % 117.67/117.71 (~P8(a5,f19(a1,f17(x30011)))), % 117.67/117.71 inference(scs_inference,[],[2870,2942,2923,2933,2919,2925,2938,2929,2943,2839,1242,359,30,227,52,1761,580,60,61,68,59,55,57,56,70,69,73,2,75,67,3,76,14,20,18])). % 117.67/117.71 cnf(3003,plain, % 117.67/117.71 (~E(f19(a1,f17(x30031)),f12(a8))), % 117.67/117.71 inference(scs_inference,[],[2870,2942,2923,2933,2919,2925,2938,2626,2929,2943,2839,1242,359,2673,30,227,52,1761,580,60,61,68,59,55,57,56,70,69,73,2,75,67,3,76,14,20,18,17])). % 117.67/117.71 cnf(3005,plain, % 117.67/117.71 (~P6(x30051,f18(a11))), % 117.67/117.71 inference(scs_inference,[],[2870,2942,2923,2933,2919,2925,2938,2626,2929,2943,2839,1242,359,2673,30,227,52,82,1761,580,60,61,68,59,55,57,56,70,69,73,2,75,67,3,76,14,20,18,17,16])). % 117.67/117.71 cnf(3008,plain, % 117.67/117.71 (~E(f15(a13),f12(a8))), % 117.67/117.71 inference(scs_inference,[],[2870,2942,2923,2933,2919,2925,2938,2626,2929,2943,2839,1242,359,2673,30,227,52,82,1761,580,60,61,68,59,55,57,56,70,69,73,2,75,67,3,76,14,20,18,17,16,66,137])). % 117.67/117.71 cnf(3011,plain, % 117.67/117.71 (E(f19(a11,f17(x30111)),a1)), % 117.67/117.71 inference(scs_inference,[],[2870,2942,2923,2933,2919,2925,2938,2626,2929,2943,2839,306,1242,2598,359,2673,30,227,52,82,1761,580,60,61,68,59,55,57,56,70,69,73,2,75,67,3,76,14,20,18,17,16,66,137,63,71])). % 117.67/117.71 cnf(3019,plain, % 117.67/117.71 (~E(f15(a1),f12(a8))), % 117.67/117.71 inference(scs_inference,[],[3000,137])). % 117.67/117.71 cnf(3020,plain, % 117.67/117.71 (~P1(f12(f17(x30201)))), % 117.67/117.71 inference(scs_inference,[],[3000,53,137,61])). % 117.67/117.71 cnf(3024,plain, % 117.67/117.71 (E(f18(a13),a1)), % 117.67/117.71 inference(scs_inference,[],[2976,3000,53,137,61,60,55])). % 117.67/117.71 cnf(3026,plain, % 117.67/117.71 (P2(f15(x30261),f16(x30262))), % 117.67/117.71 inference(scs_inference,[],[2976,3000,53,210,137,61,60,55,68])). % 117.67/117.71 cnf(3028,plain, % 117.67/117.71 (P1(f18(f18(a13)))), % 117.67/117.71 inference(scs_inference,[],[2976,3000,53,210,137,61,60,55,68,59])). % 117.67/117.71 cnf(3030,plain, % 117.67/117.71 (P3(f18(a13))), % 117.67/117.71 inference(scs_inference,[],[2976,3000,53,210,137,61,60,55,68,59,56])). % 117.67/117.71 cnf(3032,plain, % 117.67/117.71 (~P2(a8,f16(a1))), % 117.67/117.71 inference(scs_inference,[],[2976,3000,1280,53,210,137,61,60,55,68,59,56,70])). % 117.67/117.71 cnf(3034,plain, % 117.67/117.71 (~P6(f16(a8),f12(a8))), % 117.67/117.71 inference(scs_inference,[],[2976,2993,3000,1280,53,210,137,61,60,55,68,59,56,70,69])). % 117.67/117.71 cnf(3036,plain, % 117.67/117.71 (P6(f10(a8,a1),a8)), % 117.67/117.71 inference(scs_inference,[],[2976,2993,3000,1280,53,210,137,61,60,55,68,59,56,70,69,73])). % 117.67/117.71 cnf(3041,plain, % 117.67/117.71 (~P2(f16(a5),f12(a5))), % 117.67/117.71 inference(scs_inference,[],[2949,2976,2993,3000,2931,1280,2804,53,210,137,61,60,55,68,59,56,70,69,73,2,75,67])). % 117.67/117.71 cnf(3046,plain, % 117.67/117.71 (P2(f10(f12(a8),f18(a1)),a8)), % 117.67/117.71 inference(scs_inference,[],[2949,2976,2993,3000,2953,2959,2931,1280,2870,2933,2804,53,210,137,61,60,55,68,59,56,70,69,73,2,75,67,3,76])). % 117.67/117.71 cnf(3048,plain, % 117.67/117.71 (~P6(f16(a8),f12(f12(a8)))), % 117.67/117.71 inference(scs_inference,[],[2949,2976,2993,3000,2953,2959,2931,1280,2870,2933,2804,53,2527,210,137,61,60,55,68,59,56,70,69,73,2,75,67,3,76,74])). % 117.67/117.71 cnf(3050,plain, % 117.67/117.71 (~E(f18(a13),f12(f12(a14)))), % 117.67/117.71 inference(scs_inference,[],[2949,2976,2993,3000,2953,2959,2972,2931,1280,2870,2933,2804,53,2527,210,137,61,60,55,68,59,56,70,69,73,2,75,67,3,76,74,14])). % 117.67/117.71 cnf(3051,plain, % 117.67/117.71 (~P2(f12(a8),f16(f18(a11)))), % 117.67/117.71 inference(scs_inference,[],[2949,2976,2993,3000,2960,2953,2959,2972,2931,1280,2870,2933,2804,53,2527,210,137,61,60,55,68,59,56,70,69,73,2,75,67,3,76,74,14,20])). % 117.67/117.71 cnf(3052,plain, % 117.67/117.71 (~P8(a14,f18(f18(a11)))), % 117.67/117.71 inference(scs_inference,[],[2949,2976,2993,3000,2952,2960,2953,2959,2972,2931,1280,1794,2870,2933,2804,53,2527,210,137,61,60,55,68,59,56,70,69,73,2,75,67,3,76,74,14,20,18])). % 117.67/117.71 cnf(3053,plain, % 117.67/117.71 (~E(f9(f12(a5)),f16(a5))), % 117.67/117.71 inference(scs_inference,[],[2949,2976,2993,3000,2952,2960,2953,2959,2972,2931,1280,1794,2870,2933,2804,53,2527,210,48,137,61,60,55,68,59,56,70,69,73,2,75,67,3,76,74,14,20,18,19])). % 117.67/117.71 cnf(3057,plain, % 117.67/117.71 (~E(f16(a8),f18(a11))), % 117.67/117.71 inference(scs_inference,[],[3005,2949,2976,2993,3000,2952,2954,2960,2953,2959,2972,2931,1280,1794,2870,2933,2804,53,2527,47,210,48,137,61,60,55,68,59,56,70,69,73,2,75,67,3,76,74,14,20,18,19,17,16])). % 117.67/117.71 cnf(3060,plain, % 117.67/117.71 (E(f18(f18(a13)),f18(a1))), % 117.67/117.71 inference(scs_inference,[],[3005,2949,2976,2993,3000,2952,2954,2960,2953,2959,2972,2931,1280,1794,2870,2933,2804,53,2527,47,210,48,137,61,60,55,68,59,56,70,69,73,2,75,67,3,76,74,14,20,18,19,17,16,5,12])). % 117.67/117.71 cnf(3061,plain, % 117.67/117.71 (E(f19(x30611,f18(a13)),f19(x30611,a1))), % 117.67/117.71 inference(scs_inference,[],[3005,2949,2976,2993,3000,2952,2954,2960,2953,2959,2972,2931,1280,1794,2870,2933,2804,53,2527,47,210,48,137,61,60,55,68,59,56,70,69,73,2,75,67,3,76,74,14,20,18,19,17,16,5,12,10])). % 117.67/117.71 cnf(3063,plain, % 117.67/117.71 (E(f10(x30631,f18(a13)),f10(x30631,a1))), % 117.67/117.71 inference(scs_inference,[],[3005,2949,2976,2993,3000,2952,2954,2960,2953,2959,2972,2931,1280,1794,2870,2933,2804,53,2527,47,210,48,137,61,60,55,68,59,56,70,69,73,2,75,67,3,76,74,14,20,18,19,17,16,5,12,10,11,7])). % 117.67/117.71 cnf(3065,plain, % 117.67/117.71 (E(f10(f18(a13),x30651),f10(a1,x30651))), % 117.67/117.71 inference(scs_inference,[],[3005,2949,2976,2993,3000,2952,2954,2960,2953,2959,2972,2931,1280,1794,2870,2933,2804,53,2527,47,210,48,137,61,60,55,68,59,56,70,69,73,2,75,67,3,76,74,14,20,18,19,17,16,5,12,10,11,7,4,6])). % 117.67/117.71 cnf(3066,plain, % 117.67/117.71 (E(f19(f18(a13),x30661),f19(a1,x30661))), % 117.67/117.71 inference(scs_inference,[],[3005,2949,2976,2993,3000,2952,2954,2960,2953,2959,2972,2931,1280,1794,2870,2933,2804,53,2527,47,210,48,137,61,60,55,68,59,56,70,69,73,2,75,67,3,76,74,14,20,18,19,17,16,5,12,10,11,7,4,6,9])). % 117.67/117.71 cnf(3069,plain, % 117.67/117.71 (E(f16(f18(a13)),f16(a1))), % 117.67/117.71 inference(scs_inference,[],[3005,2949,2976,2993,3000,2952,2954,2960,2953,2959,2972,2931,1280,1794,2870,2933,2804,53,2527,47,210,48,137,61,60,55,68,59,56,70,69,73,2,75,67,3,76,74,14,20,18,19,17,16,5,12,10,11,7,4,6,9,66,8])). % 117.67/117.71 cnf(3073,plain, % 117.67/117.71 (~E(f10(f12(a8),f18(a1)),f16(a8))), % 117.67/117.71 inference(scs_inference,[],[42,3005,2949,2976,2993,3000,2952,2954,2960,2953,2959,2972,2931,1280,1794,2870,2933,2804,53,2527,47,210,48,137,61,60,55,68,59,56,70,69,73,2,75,67,3,76,74,14,20,18,19,17,16,5,12,10,11,7,4,6,9,66,8,13,63,15])). % 117.67/117.71 cnf(3077,plain, % 117.67/117.71 (~P1(f12(f16(x30771)))), % 117.67/117.71 inference(scs_inference,[],[52,61])). % 117.67/117.71 cnf(3079,plain, % 117.67/117.71 (~E(f15(f18(a11)),f12(a8))), % 117.67/117.71 inference(scs_inference,[],[3051,52,61,137])). % 117.67/117.71 cnf(3080,plain, % 117.67/117.71 (P4(f18(f15(x30801)))), % 117.67/117.71 inference(scs_inference,[],[3051,46,52,61,137,60])). % 117.67/117.71 cnf(3082,plain, % 117.67/117.71 (P1(f18(f15(x30821)))), % 117.67/117.71 inference(scs_inference,[],[3051,46,52,61,137,60,59])). % 117.67/117.71 cnf(3086,plain, % 117.67/117.71 (P2(f9(f16(a11)),f16(x30861))), % 117.67/117.71 inference(scs_inference,[],[3028,3051,169,46,52,61,137,60,59,56,68])). % 117.67/117.71 cnf(3088,plain, % 117.67/117.71 (E(f18(f18(a13)),a1)), % 117.67/117.71 inference(scs_inference,[],[3028,3051,169,46,52,61,137,60,59,56,68,55])). % 117.67/117.71 cnf(3092,plain, % 117.67/117.71 (~P6(a8,f10(a8,a1))), % 117.67/117.71 inference(scs_inference,[],[3036,3028,3051,1284,169,46,52,61,137,60,59,56,68,55,70,69])). % 117.67/117.71 cnf(3094,plain, % 117.67/117.71 (P6(f10(a8,a2),a8)), % 117.67/117.71 inference(scs_inference,[],[3036,3028,3051,1284,169,46,52,61,137,60,59,56,68,55,70,69,73])). % 117.67/117.72 cnf(3097,plain, % 117.67/117.72 (~P2(a8,f16(f18(a13)))), % 117.67/117.72 inference(scs_inference,[],[3008,3036,3028,3051,1284,2976,169,46,52,61,137,60,59,56,68,55,70,69,73,2,75])). % 117.67/117.72 cnf(3099,plain, % 117.67/117.72 (P6(f15(x30991),f16(x30992))), % 117.67/117.72 inference(scs_inference,[],[3026,3008,3036,3028,3051,1284,2976,169,46,52,61,137,60,59,56,68,55,70,69,73,2,75,67])). % 117.67/117.72 cnf(3105,plain, % 117.67/117.72 (~E(f18(a13),f12(f17(x31051)))), % 117.67/117.72 inference(scs_inference,[],[3026,3008,3036,3024,3020,3028,3050,3051,1284,3000,2993,2976,169,46,52,61,137,60,59,56,68,55,70,69,73,2,75,67,3,76,14])). % 117.67/117.72 cnf(3106,plain, % 117.67/117.72 (~E(f16(f16(a5)),f12(a5))), % 117.67/117.72 inference(scs_inference,[],[3026,3008,3041,3036,3024,3020,3028,3050,3051,1284,3000,2764,2993,2976,169,46,52,61,137,60,59,56,68,55,70,69,73,2,75,67,3,76,14,20])). % 117.67/117.72 cnf(3108,plain, % 117.67/117.72 (~P8(a14,f19(f18(a13),f17(x31081)))), % 117.67/117.72 inference(scs_inference,[],[3026,3008,3041,3036,3024,3066,3020,3028,3050,3051,2786,1284,3000,2764,2993,2976,169,46,52,61,137,60,59,56,68,55,70,69,73,2,75,67,3,76,14,20,18])). % 117.67/117.72 cnf(3110,plain, % 117.67/117.72 (P2(f10(f12(a8),a1),f12(a8))), % 117.67/117.72 inference(scs_inference,[],[3026,3008,3041,3036,3024,2961,3066,3020,3028,3050,3051,2786,1284,3000,2764,2993,2976,974,169,46,52,61,137,60,59,56,68,55,70,69,73,2,75,67,3,76,14,20,18,19])). % 117.67/117.72 cnf(3112,plain, % 117.67/117.72 (~P6(x31121,f18(a13))), % 117.67/117.72 inference(scs_inference,[],[3026,3008,3041,3036,3024,2961,3066,3020,3028,3050,3051,2786,1284,3000,2764,2993,2976,974,169,46,52,82,61,137,60,59,56,68,55,70,69,73,2,75,67,3,76,14,20,18,19,16])). % 117.67/117.72 cnf(3118,plain, % 117.67/117.72 (E(f19(a13,f17(x31181)),a1)), % 117.67/117.72 inference(scs_inference,[],[3026,3008,3041,3036,3024,2961,3065,3066,3020,3028,3050,3051,2786,1284,38,3000,2764,2993,2976,974,169,46,52,82,61,137,60,59,56,68,55,70,69,73,2,75,67,3,76,14,20,18,19,16,66,712,71])). % 117.67/117.72 cnf(3124,plain, % 117.67/117.72 (E(f18(f15(x31241)),a1)), % 117.67/117.72 inference(scs_inference,[],[3082,55])). % 117.67/117.72 cnf(3128,plain, % 117.67/117.72 (P2(f9(f16(a1)),f16(x31281))), % 117.67/117.72 inference(scs_inference,[],[3082,97,55,56,68])). % 117.67/117.72 cnf(3130,plain, % 117.67/117.72 (~P2(a8,f16(a13))), % 117.67/117.72 inference(scs_inference,[],[3082,1288,97,55,56,68,70])). % 117.67/117.72 cnf(3134,plain, % 117.67/117.72 (P6(f10(a8,a13),a8)), % 117.67/117.72 inference(scs_inference,[],[3094,3082,1288,97,55,56,68,70,69,73])). % 117.67/117.72 cnf(3136,plain, % 117.67/117.72 (~E(f12(a8),f15(a1))), % 117.67/117.72 inference(scs_inference,[],[3019,3094,3082,1288,97,55,56,68,70,69,73,2])). % 117.67/117.72 cnf(3137,plain, % 117.67/117.72 (~P2(f16(a8),f12(a8))), % 117.67/117.72 inference(scs_inference,[],[3019,3034,3094,3082,1288,2598,97,55,56,68,70,69,73,2,67])). % 117.67/117.72 cnf(3142,plain, % 117.67/117.72 (P2(f9(f12(a8)),a8)), % 117.67/117.72 inference(scs_inference,[],[3019,3034,3094,2957,3082,1288,3065,2870,2598,97,2600,55,56,68,70,69,73,2,67,3,76])). % 117.67/117.72 cnf(3145,plain, % 117.67/117.72 (~P2(a8,f16(f18(a11)))), % 117.67/117.72 inference(scs_inference,[],[3019,3034,3094,2957,3082,3032,1288,2960,3065,50,2870,2598,97,2600,55,56,68,70,69,73,2,67,3,76,14,20])). % 117.67/117.72 cnf(3146,plain, % 117.67/117.72 (~P8(a8,f18(f18(a13)))), % 117.67/117.72 inference(scs_inference,[],[3019,3034,3094,3060,2957,3082,3032,1288,1807,2960,3065,50,2870,2598,97,2600,55,56,68,70,69,73,2,67,3,76,14,20,18])). % 117.67/117.72 cnf(3147,plain, % 117.67/117.72 (~E(f10(f12(a8),a1),f16(a8))), % 117.67/117.72 inference(scs_inference,[],[3019,3034,3094,3060,2957,3110,3082,3032,1288,1807,2960,3065,50,2870,2598,97,2600,55,56,68,70,69,73,2,67,3,76,14,20,18,19])). % 117.67/117.72 cnf(3148,plain, % 117.67/117.72 (~E(f16(x31481),f18(a13))), % 117.67/117.72 inference(scs_inference,[],[3099,3112,3019,3034,3094,3060,2957,3110,3082,3032,1288,1807,2960,3065,50,2870,2598,97,2600,55,56,68,70,69,73,2,67,3,76,14,20,18,19,16])). % 117.67/117.72 cnf(3153,plain, % 117.67/117.72 (~E(f9(f12(a8)),f16(a8))), % 117.67/117.72 inference(scs_inference,[],[3099,3112,3019,3034,3094,3060,2957,3110,3080,3082,3032,1288,1807,2960,3065,50,2870,2598,97,2600,55,56,68,70,69,73,2,67,3,76,14,20,18,19,16,62,107])). % 117.67/117.72 cnf(3164,plain, % 117.67/117.72 (E(f9(f16(a11)),a1)), % 117.67/117.72 inference(scs_inference,[],[2938,55])). % 117.67/117.72 cnf(3172,plain, % 117.67/117.72 (P6(f10(a5,f18(a1)),a5)), % 117.67/117.72 inference(scs_inference,[],[3134,1800,2938,55,70,56,69,73])). % 117.67/117.72 cnf(3178,plain, % 117.67/117.72 (E(f19(f18(a2),f18(a13)),f19(a1,a1))), % 117.67/117.72 inference(scs_inference,[],[3148,2876,3134,3061,2851,1800,2938,52,55,70,56,69,73,2,67,3])). % 117.67/117.72 cnf(3182,plain, % 117.67/117.72 (~E(f16(f16(a8)),f12(a8))), % 117.67/117.72 inference(scs_inference,[],[3148,2876,3137,3134,3077,3061,2851,1800,2938,2764,2760,52,55,70,56,69,73,2,67,3,14,20])). % 117.67/117.72 cnf(3186,plain, % 117.67/117.72 (P2(f10(f12(a8),a1),a8)), % 117.67/117.72 inference(scs_inference,[],[3148,2876,3137,3134,3077,3046,3108,3061,2851,1800,2938,2764,47,2760,974,52,55,70,56,69,73,2,67,3,14,20,18,19])). % 117.67/117.72 cnf(3188,plain, % 117.67/117.72 (~P6(x31881,f18(f15(x31882)))), % 117.67/117.72 inference(scs_inference,[],[3148,2876,3137,3134,3077,3046,3124,3108,3061,2851,1800,2938,2764,47,2760,974,52,82,55,70,56,69,73,2,67,3,14,20,18,19,16])). % 117.67/117.72 cnf(3196,plain, % 117.67/117.72 (E(f19(f15(x31961),f17(x31962)),a1)), % 117.67/117.72 inference(scs_inference,[],[3148,2876,3137,3134,3077,2980,3046,3124,3108,3061,2851,2766,1800,2938,3065,2764,47,2760,974,52,82,55,70,56,69,73,2,67,3,14,20,18,19,16,62,66,640,71])). % 117.67/117.72 cnf(3201,plain, % 117.67/117.72 (E(f9(f16(a1)),a1)), % 117.67/117.72 inference(scs_inference,[],[2779,55])). % 117.67/117.72 cnf(3203,plain, % 117.67/117.72 (~P2(f18(a14),f16(f18(a1)))), % 117.67/117.72 inference(scs_inference,[],[1817,2779,55,70])). % 117.67/117.72 cnf(3205,plain, % 117.67/117.72 (P3(f9(f16(a1)))), % 117.67/117.72 inference(scs_inference,[],[1817,2779,55,70,56])). % 117.67/117.72 cnf(3207,plain, % 117.67/117.72 (~P6(a5,f10(a5,f18(a1)))), % 117.67/117.72 inference(scs_inference,[],[3172,1817,2779,55,70,56,69])). % 117.67/117.72 cnf(3209,plain, % 117.67/117.72 (P6(f10(f18(a14),f18(a1)),f18(a14))), % 117.67/117.72 inference(scs_inference,[],[3172,1817,2779,55,70,56,69,73])). % 117.67/117.72 cnf(3215,plain, % 117.67/117.72 (E(f10(x32151,f18(a13)),f10(x32151,a1))), % 117.67/117.72 inference(rename_variables,[],[3063])). % 117.67/117.72 cnf(3217,plain, % 117.67/117.72 (~E(f9(f16(a1)),f12(a5))), % 117.67/117.72 inference(scs_inference,[],[3057,3048,3172,3063,1817,2754,2779,2849,2804,55,70,56,69,73,2,67,3,14])). % 117.67/117.72 cnf(3219,plain, % 117.67/117.72 (~P8(f18(a14),f19(f15(x32191),f17(x32192)))), % 117.67/117.72 inference(scs_inference,[],[3057,3048,3172,3196,3069,3063,1817,1739,2768,2754,2779,2849,2804,55,70,56,69,73,2,67,3,14,20,18])). % 117.67/117.72 cnf(3220,plain, % 117.67/117.72 (~E(a11,f12(a8))), % 117.67/117.72 inference(scs_inference,[],[2921,3057,3048,3172,3196,3069,3063,1817,1739,2991,2768,2754,2779,2849,2804,55,70,56,69,73,2,67,3,14,20,18,19])). % 117.67/117.72 cnf(3224,plain, % 117.67/117.72 (P2(f10(f18(a14),f18(a1)),f18(a14))), % 117.67/117.72 inference(scs_inference,[],[2921,3057,3092,3048,3172,3196,3069,3063,3215,1817,1739,2991,2768,2754,2779,2849,2804,55,70,56,69,73,2,67,3,14,20,18,19,16,66])). % 117.67/117.72 cnf(3234,plain, % 117.67/117.72 (P3(f9(f16(a13)))), % 117.67/117.72 inference(scs_inference,[],[2828,55,56])). % 117.67/117.72 cnf(3240,plain, % 117.67/117.72 (P6(f10(f18(a14),f15(x32401)),f18(a14))), % 117.67/117.72 inference(scs_inference,[],[3209,2363,2828,55,56,70,69,73])). % 117.67/117.72 cnf(3243,plain, % 117.67/117.72 (P6(a2,f16(x32431))), % 117.67/117.72 inference(scs_inference,[],[3220,2974,3209,2363,2828,52,55,56,70,69,73,2,67])). % 117.67/117.72 cnf(3247,plain, % 117.67/117.72 (~E(f18(a11),f12(f17(x32471)))), % 117.67/117.72 inference(scs_inference,[],[3220,2974,2990,3209,2363,3020,2952,2828,2872,52,55,56,70,69,73,2,67,3,14])). % 117.67/117.72 cnf(3248,plain, % 117.67/117.72 (~P2(f18(a14),f16(a1))), % 117.67/117.72 inference(scs_inference,[],[3220,2974,2990,3209,3203,2363,3020,2952,2828,2872,52,580,55,56,70,69,73,2,67,3,14,20])). % 117.67/117.72 cnf(3251,plain, % 117.67/117.72 (P2(f10(f18(a14),a1),f18(a14))), % 117.67/117.72 inference(scs_inference,[],[3220,2974,2990,3209,3224,3219,3203,2363,3020,2952,2828,2872,47,974,52,580,55,56,70,69,73,2,67,3,14,20,18,19])). % 117.67/117.72 cnf(3258,plain, % 117.67/117.72 (E(f19(f18(a11),f17(x32581)),a1)), % 117.67/117.72 inference(scs_inference,[],[3220,2974,2990,3209,3224,3219,3203,2978,2868,2363,3020,2952,2828,359,2872,47,974,52,82,580,55,56,70,69,73,2,67,3,14,20,18,19,16,66,63,71])). % 117.67/117.72 cnf(3264,plain, % 117.67/117.72 (E(a11,a1)), % 117.67/117.72 inference(scs_inference,[],[29,55])). % 117.67/117.72 cnf(3266,plain, % 117.67/117.72 (~P2(a14,f16(f15(x32661)))), % 117.67/117.72 inference(scs_inference,[],[1645,29,55,70])). % 117.67/117.72 cnf(3272,plain, % 117.67/117.72 (P6(f10(a14,f15(x32721)),a14)), % 117.67/117.72 inference(scs_inference,[],[3240,1645,29,55,70,56,69,73])). % 117.67/117.72 cnf(3275,plain, % 117.67/117.72 (P1(f9(f16(a2)))), % 117.67/117.72 inference(scs_inference,[],[2840,3240,1645,29,269,48,55,70,56,69,73,2,67])). % 117.67/117.72 cnf(3284,plain, % 117.67/117.72 (~P8(f16(x32841),f19(f18(a11),f17(x32842)))), % 117.67/117.72 inference(scs_inference,[],[3248,2840,3240,3258,2852,1645,1257,3069,2959,2664,2804,29,269,48,55,70,56,69,73,2,67,3,14,20,18])). % 117.67/117.72 cnf(3285,plain, % 117.67/117.72 (~E(f19(f18(a1),f17(x32851)),f18(a14))), % 117.67/117.72 inference(scs_inference,[],[3248,2840,2680,3240,3258,2852,1645,1257,3069,2959,2664,2804,29,269,48,55,70,56,69,73,2,67,3,14,20,18,19])). % 117.67/117.72 cnf(3289,plain, % 117.67/117.72 (E(f9(a11),f9(a1))), % 117.67/117.72 inference(scs_inference,[],[3243,3248,2840,2680,3240,3188,3258,2852,1645,1257,3069,2959,2664,2804,29,269,48,55,70,56,69,73,2,67,3,14,20,18,19,16,5])). % 117.67/117.72 cnf(3290,plain, % 117.67/117.72 (E(f18(a11),f18(a1))), % 117.67/117.72 inference(scs_inference,[],[3243,3248,2840,2680,3240,3188,3258,2852,1645,1257,3069,2959,2664,2804,29,269,48,55,70,56,69,73,2,67,3,14,20,18,19,16,5,12])). % 117.67/117.72 cnf(3291,plain, % 117.67/117.72 (E(f19(a11,x32911),f19(a1,x32911))), % 117.67/117.72 inference(scs_inference,[],[3243,3248,2840,2680,3240,3188,3258,2852,1645,1257,3069,2959,2664,2804,29,269,48,55,70,56,69,73,2,67,3,14,20,18,19,16,5,12,9])). % 117.67/117.72 cnf(3293,plain, % 117.67/117.72 (E(f19(x32931,a11),f19(x32931,a1))), % 117.67/117.72 inference(scs_inference,[],[3243,3248,2840,2680,3240,3188,3258,2852,1645,1257,3069,2959,2664,2804,29,269,48,55,70,56,69,73,2,67,3,14,20,18,19,16,5,12,9,6,10])). % 117.67/117.72 cnf(3294,plain, % 117.67/117.72 (E(f17(a11),f17(a1))), % 117.67/117.72 inference(scs_inference,[],[3243,3248,2840,2680,3240,3188,3258,2852,1645,1257,3069,2959,2664,2804,29,269,48,55,70,56,69,73,2,67,3,14,20,18,19,16,5,12,9,6,10,11])). % 117.67/117.72 cnf(3295,plain, % 117.67/117.72 (E(f10(x32951,a11),f10(x32951,a1))), % 117.67/117.72 inference(scs_inference,[],[3243,3248,2840,2680,3240,3188,3258,2852,1645,1257,3069,2959,2664,2804,29,269,48,55,70,56,69,73,2,67,3,14,20,18,19,16,5,12,9,6,10,11,7])). % 117.67/117.72 cnf(3296,plain, % 117.67/117.72 (E(f15(a11),f15(a1))), % 117.67/117.72 inference(scs_inference,[],[3243,3248,2840,2680,3240,3188,3258,2852,1645,1257,3069,2959,2664,2804,29,269,48,55,70,56,69,73,2,67,3,14,20,18,19,16,5,12,9,6,10,11,7,4])). % 117.67/117.72 cnf(3297,plain, % 117.67/117.72 (E(f12(a11),f12(a1))), % 117.67/117.72 inference(scs_inference,[],[3243,3248,2840,2680,3240,3188,3258,2852,1645,1257,3069,2959,2664,2804,29,269,48,55,70,56,69,73,2,67,3,14,20,18,19,16,5,12,9,6,10,11,7,4,13])). % 117.67/117.72 cnf(3298,plain, % 117.67/117.72 (E(f16(a11),f16(a1))), % 117.67/117.72 inference(scs_inference,[],[3243,3248,2840,2680,3240,3188,3258,2852,1645,1257,3069,2959,2664,2804,29,269,48,55,70,56,69,73,2,67,3,14,20,18,19,16,5,12,9,6,10,11,7,4,13,8])). % 117.67/117.72 cnf(3307,plain, % 117.67/117.72 (P4(f9(f16(a2)))), % 117.67/117.72 inference(scs_inference,[],[3275,57])). % 117.67/117.72 cnf(3311,plain, % 117.67/117.72 (P3(f9(f16(a2)))), % 117.67/117.72 inference(scs_inference,[],[3275,57,55,56])). % 117.67/117.72 cnf(3313,plain, % 117.67/117.72 (~P2(a5,f16(f15(x33131)))), % 117.67/117.72 inference(scs_inference,[],[3275,1649,57,55,56,70])). % 117.67/117.72 cnf(3317,plain, % 117.67/117.72 (P6(f10(a5,f15(x33171)),a5)), % 117.67/117.72 inference(scs_inference,[],[3275,3272,1649,57,55,56,70,69,73])). % 117.67/117.72 cnf(3320,plain, % 117.67/117.72 (P6(f9(f16(a13)),f16(x33201))), % 117.67/117.72 inference(scs_inference,[],[2951,2815,3275,3272,1649,52,57,55,56,70,69,73,2,67])). % 117.67/117.72 cnf(3323,plain, % 117.67/117.72 (~E(f12(a8),f15(a11))), % 117.67/117.72 inference(scs_inference,[],[3136,3296,2951,2815,3275,3272,1649,52,57,55,56,70,69,73,2,67,3])). % 117.67/117.72 cnf(3325,plain, % 117.67/117.72 (P2(x33251,f16(x33251))), % 117.67/117.72 inference(rename_variables,[],[2764])). % 117.67/117.72 cnf(3327,plain, % 117.67/117.72 (~E(f18(a13),f12(f16(x33271)))), % 117.67/117.72 inference(scs_inference,[],[3136,3296,2951,2815,3275,3272,1649,3077,2764,2976,52,57,55,56,70,69,73,2,67,3,76,14])). % 117.67/117.72 cnf(3331,plain, % 117.67/117.72 (P2(x33311,f16(x33311))), % 117.67/117.72 inference(rename_variables,[],[2764])). % 117.67/117.72 cnf(3334,plain, % 117.67/117.72 (P2(f19(a1,x33341),f16(f19(a11,x33341)))), % 117.67/117.72 inference(scs_inference,[],[3291,3136,3294,3296,2951,2815,3284,3275,3266,3272,203,1649,3077,2764,3325,3331,2976,47,52,57,55,56,70,69,73,2,67,3,76,14,15,20,18,19])). % 117.67/117.72 cnf(3337,plain, % 117.67/117.72 (E(f19(a11,x33371),f19(a1,x33371))), % 117.67/117.72 inference(rename_variables,[],[3291])). % 117.67/117.72 cnf(3339,plain, % 117.67/117.72 (~P6(x33391,f19(a11,f17(x33392)))), % 117.67/117.72 inference(scs_inference,[],[3291,3337,3136,3294,3296,2951,2815,3284,2842,3275,3266,3272,203,2690,1649,3077,2764,3325,3331,2976,47,52,57,55,56,70,69,73,2,67,3,76,14,15,20,18,19,17,16])). % 117.67/117.72 cnf(3349,plain, % 117.67/117.72 (E(a2,a1)), % 117.67/117.72 inference(scs_inference,[],[28,46,56,55])). % 117.67/117.72 cnf(3351,plain, % 117.67/117.72 (~P2(a8,f16(f15(x33511)))), % 117.67/117.72 inference(scs_inference,[],[1657,28,46,56,55,70])). % 117.67/117.72 cnf(3355,plain, % 117.67/117.72 (P6(f10(a8,f15(x33551)),a8)), % 117.67/117.72 inference(scs_inference,[],[3317,1657,28,46,56,55,70,69,73])). % 117.67/117.72 cnf(3360,plain, % 117.67/117.72 (P1(f19(a11,f17(x33601)))), % 117.67/117.72 inference(scs_inference,[],[3323,3320,3339,3317,1657,28,2976,46,48,56,55,70,69,73,2,75,67])). % 117.67/117.72 cnf(3361,plain, % 117.67/117.72 (~P6(x33611,f19(a11,f17(x33612)))), % 117.67/117.72 inference(rename_variables,[],[3339])). % 117.67/117.72 cnf(3362,plain, % 117.67/117.72 (P2(f9(x33621),x33621)), % 117.67/117.72 inference(rename_variables,[],[48])). % 117.67/117.72 cnf(3368,plain, % 117.67/117.72 (~P8(f16(x33681),f18(a11))), % 117.67/117.72 inference(scs_inference,[],[3289,3290,3323,3320,3339,3317,1657,1803,3028,50,28,2976,46,48,3362,518,56,55,70,69,73,2,75,67,3,14,20,18])). % 117.67/117.72 cnf(3371,plain, % 117.67/117.72 (E(f10(a2,x33711),f10(a1,x33711))), % 117.67/117.72 inference(scs_inference,[],[3289,3290,3323,3320,3339,3361,3317,1657,1803,3028,50,28,2976,46,48,3362,518,56,55,70,69,73,2,75,67,3,14,20,18,16,6])). % 117.67/117.72 cnf(3372,plain, % 117.67/117.72 (E(f19(a2,x33721),f19(a1,x33721))), % 117.67/117.72 inference(scs_inference,[],[3289,3290,3323,3320,3339,3361,3317,1657,1803,3028,50,28,2976,46,48,3362,518,56,55,70,69,73,2,75,67,3,14,20,18,16,6,9])). % 117.67/117.72 cnf(3373,plain, % 117.67/117.72 (E(f19(x33731,a2),f19(x33731,a1))), % 117.67/117.72 inference(scs_inference,[],[3289,3290,3323,3320,3339,3361,3317,1657,1803,3028,50,28,2976,46,48,3362,518,56,55,70,69,73,2,75,67,3,14,20,18,16,6,9,10])). % 117.67/117.72 cnf(3374,plain, % 117.67/117.72 (E(f18(a2),f18(a1))), % 117.67/117.72 inference(scs_inference,[],[3289,3290,3323,3320,3339,3361,3317,1657,1803,3028,50,28,2976,46,48,3362,518,56,55,70,69,73,2,75,67,3,14,20,18,16,6,9,10,12])). % 117.67/117.72 cnf(3375,plain, % 117.67/117.72 (E(f15(a2),f15(a1))), % 117.67/117.72 inference(scs_inference,[],[3289,3290,3323,3320,3339,3361,3317,1657,1803,3028,50,28,2976,46,48,3362,518,56,55,70,69,73,2,75,67,3,14,20,18,16,6,9,10,12,4])). % 117.67/117.72 cnf(3376,plain, % 117.67/117.72 (E(f9(a2),f9(a1))), % 117.67/117.72 inference(scs_inference,[],[3289,3290,3323,3320,3339,3361,3317,1657,1803,3028,50,28,2976,46,48,3362,518,56,55,70,69,73,2,75,67,3,14,20,18,16,6,9,10,12,4,5])). % 117.67/117.72 cnf(3377,plain, % 117.67/117.72 (E(f17(a2),f17(a1))), % 117.67/117.72 inference(scs_inference,[],[3289,3290,3323,3320,3339,3361,3317,1657,1803,3028,50,28,2976,46,48,3362,518,56,55,70,69,73,2,75,67,3,14,20,18,16,6,9,10,12,4,5,11])). % 117.67/117.72 cnf(3378,plain, % 117.67/117.72 (E(f10(x33781,a2),f10(x33781,a1))), % 117.67/117.72 inference(scs_inference,[],[3289,3290,3323,3320,3339,3361,3317,1657,1803,3028,50,28,2976,46,48,3362,518,56,55,70,69,73,2,75,67,3,14,20,18,16,6,9,10,12,4,5,11,7])). % 117.67/117.72 cnf(3379,plain, % 117.67/117.72 (E(f12(a2),f12(a1))), % 117.67/117.72 inference(scs_inference,[],[3289,3290,3323,3320,3339,3361,3317,1657,1803,3028,50,28,2976,46,48,3362,518,56,55,70,69,73,2,75,67,3,14,20,18,16,6,9,10,12,4,5,11,7,13])). % 117.67/117.72 cnf(3380,plain, % 117.67/117.72 (E(f16(a2),f16(a1))), % 117.67/117.72 inference(scs_inference,[],[3289,3290,3323,3320,3339,3361,3317,1657,1803,3028,50,28,2976,46,48,3362,518,56,55,70,69,73,2,75,67,3,14,20,18,16,6,9,10,12,4,5,11,7,13,8])). % 117.67/117.72 cnf(3389,plain, % 117.67/117.72 (P4(f19(a11,f17(x33891)))), % 117.67/117.72 inference(scs_inference,[],[3360,57])). % 117.67/117.72 cnf(3391,plain, % 117.67/117.72 (P3(f19(a11,f17(x33911)))), % 117.67/117.72 inference(scs_inference,[],[3360,57,56])). % 117.67/117.72 cnf(3393,plain, % 117.67/117.72 (E(a13,a1)), % 117.67/117.72 inference(scs_inference,[],[3360,30,57,56,55])). % 117.67/117.72 cnf(3395,plain, % 117.67/117.72 (~P2(a8,f16(a11))), % 117.67/117.72 inference(scs_inference,[],[3360,1632,30,57,56,55,70])). % 117.67/117.72 cnf(3399,plain, % 117.67/117.72 (P6(f10(f16(x33991),f18(a11)),f16(x33991))), % 117.67/117.72 inference(scs_inference,[],[3368,3360,3355,1632,30,57,56,55,70,69,73])). % 117.67/117.72 cnf(3405,plain, % 117.67/117.72 (~E(f16(a1),f16(a14))), % 117.67/117.72 inference(scs_inference,[],[3368,2935,3380,2787,3086,3360,3355,1632,30,52,57,56,55,70,69,73,2,67,3])). % 117.67/117.72 cnf(3406,plain, % 117.67/117.72 (~E(f18(a2),f12(f12(a5)))), % 117.67/117.72 inference(scs_inference,[],[3368,2935,3380,2787,3086,3360,3355,1632,2866,2760,30,52,57,56,55,70,69,73,2,67,3,14])). % 117.67/117.72 cnf(3409,plain, % 117.67/117.72 (~E(f16(x34091),f18(a11))), % 117.67/117.72 inference(scs_inference,[],[3368,2935,3380,2787,3086,3360,3351,3355,1632,2866,2764,2760,30,47,52,57,56,55,70,69,73,2,67,3,14,20,18])). % 117.67/117.72 cnf(3411,plain, % 117.67/117.72 (~P6(x34111,f19(a2,f17(x34112)))), % 117.67/117.72 inference(scs_inference,[],[3372,3368,2935,3380,2787,3086,3360,3351,3355,1632,2866,2690,2764,2760,30,47,52,57,56,55,70,69,73,2,67,3,14,20,18,16])). % 117.67/117.72 cnf(3415,plain, % 117.67/117.72 (E(f18(a13),f18(a1))), % 117.67/117.72 inference(scs_inference,[],[3372,3368,2935,3380,2787,3086,2878,3234,3360,3351,3355,1632,2866,2690,2828,2764,2760,30,47,52,57,56,55,70,69,73,2,67,3,14,20,18,16,62,12])). % 117.67/117.72 cnf(3416,plain, % 117.67/117.72 (E(f19(x34161,a13),f19(x34161,a1))), % 117.67/117.72 inference(scs_inference,[],[3372,3368,2935,3380,2787,3086,2878,3234,3360,3351,3355,1632,2866,2690,2828,2764,2760,30,47,52,57,56,55,70,69,73,2,67,3,14,20,18,16,62,12,10])). % 117.67/117.72 cnf(3417,plain, % 117.67/117.72 (E(f19(a13,x34171),f19(a1,x34171))), % 117.67/117.72 inference(scs_inference,[],[3372,3368,2935,3380,2787,3086,2878,3234,3360,3351,3355,1632,2866,2690,2828,2764,2760,30,47,52,57,56,55,70,69,73,2,67,3,14,20,18,16,62,12,10,9])). % 117.67/117.72 cnf(3418,plain, % 117.67/117.72 (E(f10(a13,x34181),f10(a1,x34181))), % 117.67/117.72 inference(scs_inference,[],[3372,3368,2935,3380,2787,3086,2878,3234,3360,3351,3355,1632,2866,2690,2828,2764,2760,30,47,52,57,56,55,70,69,73,2,67,3,14,20,18,16,62,12,10,9,6])). % 117.67/117.72 cnf(3419,plain, % 117.67/117.72 (E(f15(a13),f15(a1))), % 117.67/117.72 inference(scs_inference,[],[3372,3368,2935,3380,2787,3086,2878,3234,3360,3351,3355,1632,2866,2690,2828,2764,2760,30,47,52,57,56,55,70,69,73,2,67,3,14,20,18,16,62,12,10,9,6,4])). % 117.67/117.72 cnf(3420,plain, % 117.67/117.72 (E(f10(x34201,a13),f10(x34201,a1))), % 117.67/117.72 inference(scs_inference,[],[3372,3368,2935,3380,2787,3086,2878,3234,3360,3351,3355,1632,2866,2690,2828,2764,2760,30,47,52,57,56,55,70,69,73,2,67,3,14,20,18,16,62,12,10,9,6,4,7])). % 117.67/117.72 cnf(3421,plain, % 117.67/117.72 (E(f9(a13),f9(a1))), % 117.67/117.72 inference(scs_inference,[],[3372,3368,2935,3380,2787,3086,2878,3234,3360,3351,3355,1632,2866,2690,2828,2764,2760,30,47,52,57,56,55,70,69,73,2,67,3,14,20,18,16,62,12,10,9,6,4,7,5])). % 117.67/117.72 cnf(3422,plain, % 117.67/117.72 (E(f17(a13),f17(a1))), % 117.67/117.72 inference(scs_inference,[],[3372,3368,2935,3380,2787,3086,2878,3234,3360,3351,3355,1632,2866,2690,2828,2764,2760,30,47,52,57,56,55,70,69,73,2,67,3,14,20,18,16,62,12,10,9,6,4,7,5,11])). % 117.67/117.72 cnf(3423,plain, % 117.67/117.72 (E(f12(a13),f12(a1))), % 117.67/117.72 inference(scs_inference,[],[3372,3368,2935,3380,2787,3086,2878,3234,3360,3351,3355,1632,2866,2690,2828,2764,2760,30,47,52,57,56,55,70,69,73,2,67,3,14,20,18,16,62,12,10,9,6,4,7,5,11,13])). % 117.67/117.72 cnf(3424,plain, % 117.67/117.72 (E(f16(a13),f16(a1))), % 117.67/117.72 inference(scs_inference,[],[3372,3368,2935,3380,2787,3086,2878,3234,3360,3351,3355,1632,2866,2690,2828,2764,2760,30,47,52,57,56,55,70,69,73,2,67,3,14,20,18,16,62,12,10,9,6,4,7,5,11,13,8])). % 117.67/117.72 cnf(3425,plain, % 117.67/117.72 (P2(f10(f16(x34251),f18(a11)),f16(x34251))), % 117.67/117.72 inference(scs_inference,[],[3372,3368,2935,3380,2787,3086,2878,3234,3360,3351,3355,1632,2866,2690,2828,2764,2760,30,47,52,57,56,55,70,69,73,2,67,3,14,20,18,16,62,12,10,9,6,4,7,5,11,13,8,66])). % 117.67/117.72 cnf(3433,plain, % 117.67/117.72 (E(f15(x34331),a1)), % 117.67/117.72 inference(scs_inference,[],[46,55])). % 117.67/117.72 cnf(3435,plain, % 117.67/117.72 (~P2(a5,f16(a11))), % 117.67/117.72 inference(scs_inference,[],[1626,46,55,70])). % 117.67/117.72 cnf(3437,plain, % 117.67/117.72 (~P6(f16(x34371),f10(f16(x34371),f18(a11)))), % 117.67/117.72 inference(scs_inference,[],[3399,1626,46,55,70,69])). % 117.67/117.72 cnf(3439,plain, % 117.67/117.72 (P6(f10(a14,a11),a14)), % 117.67/117.72 inference(scs_inference,[],[3399,1623,1626,46,55,70,69,73])). % 117.67/117.72 cnf(3442,plain, % 117.67/117.72 (P1(f19(a2,f17(x34421)))), % 117.67/117.72 inference(scs_inference,[],[3409,3399,3411,1623,1626,46,48,55,70,69,73,2,67])). % 117.67/117.72 cnf(3443,plain, % 117.67/117.72 (~P6(x34431,f19(a2,f17(x34432)))), % 117.67/117.72 inference(rename_variables,[],[3411])). % 117.67/117.72 cnf(3444,plain, % 117.67/117.72 (P2(f9(x34441),x34441)), % 117.67/117.72 inference(rename_variables,[],[48])). % 117.67/117.72 cnf(3446,plain, % 117.67/117.72 (E(f19(a13,a13),f19(a1,a1))), % 117.67/117.72 inference(scs_inference,[],[3416,3417,3409,3399,3411,1623,1626,46,48,55,70,69,73,2,67,3])). % 117.67/117.72 cnf(3448,plain, % 117.67/117.72 (E(f19(a13,x34481),f19(a1,x34481))), % 117.67/117.72 inference(rename_variables,[],[3417])). % 117.67/117.72 cnf(3452,plain, % 117.67/117.72 (~P8(a5,f19(a13,f17(x34521)))), % 117.67/117.72 inference(scs_inference,[],[3393,3416,3417,3448,3409,3399,3411,3001,1623,1626,3360,51,46,48,3444,55,70,69,73,2,67,3,14,20,18])). % 117.67/117.72 cnf(3462,plain, % 117.67/117.72 (E(f19(f15(x34621),x34622),f19(a1,x34622))), % 117.67/117.72 inference(scs_inference,[],[3393,3416,3417,3448,3409,3395,3399,3425,3411,3443,3389,3391,3001,1623,1626,3360,51,46,48,3444,55,70,69,73,2,67,3,14,20,18,19,16,62,9])). % 117.67/117.72 cnf(3463,plain, % 117.67/117.72 (E(f18(f15(x34631)),f18(a1))), % 117.67/117.72 inference(scs_inference,[],[3393,3416,3417,3448,3409,3395,3399,3425,3411,3443,3389,3391,3001,1623,1626,3360,51,46,48,3444,55,70,69,73,2,67,3,14,20,18,19,16,62,9,12])). % 117.67/117.72 cnf(3464,plain, % 117.67/117.72 (E(f19(x34641,f15(x34642)),f19(x34641,a1))), % 117.67/117.72 inference(scs_inference,[],[3393,3416,3417,3448,3409,3395,3399,3425,3411,3443,3389,3391,3001,1623,1626,3360,51,46,48,3444,55,70,69,73,2,67,3,14,20,18,19,16,62,9,12,10])). % 117.67/117.72 cnf(3465,plain, % 117.67/117.72 (E(f10(f15(x34651),x34652),f10(a1,x34652))), % 117.67/117.72 inference(scs_inference,[],[3393,3416,3417,3448,3409,3395,3399,3425,3411,3443,3389,3391,3001,1623,1626,3360,51,46,48,3444,55,70,69,73,2,67,3,14,20,18,19,16,62,9,12,10,6])). % 117.67/117.72 cnf(3466,plain, % 117.67/117.72 (E(f9(f15(x34661)),f9(a1))), % 117.67/117.72 inference(scs_inference,[],[3393,3416,3417,3448,3409,3395,3399,3425,3411,3443,3389,3391,3001,1623,1626,3360,51,46,48,3444,55,70,69,73,2,67,3,14,20,18,19,16,62,9,12,10,6,5])). % 117.67/117.72 cnf(3470,plain, % 117.67/117.72 (E(f10(x34701,f15(x34702)),f10(x34701,a1))), % 117.67/117.72 inference(scs_inference,[],[3393,3416,3417,3448,3409,3395,3399,3425,3411,3443,3389,3391,3001,1623,1626,3360,51,46,48,3444,55,70,69,73,2,67,3,14,20,18,19,16,62,9,12,10,6,5,4,66,7])). % 117.67/117.72 cnf(3480,plain, % 117.67/117.72 (P4(f19(a2,f17(x34801)))), % 117.67/117.72 inference(scs_inference,[],[3442,57])). % 117.67/117.72 cnf(3482,plain, % 117.67/117.72 (P3(f19(a2,f17(x34821)))), % 117.67/117.72 inference(scs_inference,[],[3442,57,56])). % 117.67/117.72 cnf(3488,plain, % 117.67/117.72 (P6(f10(f16(x34881),f15(x34882)),f16(x34881))), % 117.67/117.72 inference(scs_inference,[],[3439,3442,1653,57,56,70,69,73])). % 117.67/117.72 cnf(3495,plain, % 117.67/117.72 (~E(f18(a11),f12(f18(a14)))), % 117.67/117.72 inference(scs_inference,[],[3405,3439,3128,3442,1653,2919,2872,52,580,57,56,70,69,73,2,67,3,14])). % 117.67/117.72 cnf(3498,plain, % 117.67/117.72 (~E(f16(a5),f16(a11))), % 117.67/117.72 inference(scs_inference,[],[3405,3439,3435,3128,3437,3442,3424,1653,2919,2872,2764,52,580,57,56,70,69,73,2,67,3,14,15,20])). % 117.67/117.72 cnf(3499,plain, % 117.67/117.72 (P2(x34991,f16(x34991))), % 117.67/117.72 inference(rename_variables,[],[2764])). % 117.67/117.72 cnf(3502,plain, % 117.67/117.72 (P2(f19(a1,a1),f16(f19(a13,a13)))), % 117.67/117.72 inference(scs_inference,[],[3446,3405,3439,3435,3128,3437,3442,3052,3424,1653,2919,2872,2764,3499,47,52,580,57,56,70,69,73,2,67,3,14,15,20,18,19])). % 117.67/117.72 cnf(3504,plain, % 117.67/117.72 (~P6(x35041,f19(f15(x35042),f17(x35043)))), % 117.67/117.72 inference(scs_inference,[],[3446,3405,3439,3435,3128,3462,3437,3442,3052,3424,1653,2919,2690,2872,2764,3499,47,52,580,57,56,70,69,73,2,67,3,14,15,20,18,19,16])). % 117.67/117.72 cnf(3506,plain, % 117.67/117.72 (P2(f10(f16(x35061),f15(x35062)),f16(x35061))), % 117.67/117.72 inference(scs_inference,[],[3446,3405,3439,3435,3128,3462,3437,3442,3052,3424,1653,2919,2690,2872,2764,3499,47,52,580,57,56,70,69,73,2,67,3,14,15,20,18,19,16,66])). % 117.67/117.72 cnf(3515,plain, % 117.67/117.72 (~P6(f16(x35151),f10(f16(x35151),f15(x35152)))), % 117.67/117.72 inference(scs_inference,[],[3488,1661,70,69])). % 117.67/117.72 cnf(3517,plain, % 117.67/117.72 (P6(f10(f17(x35171),f15(x35172)),f17(x35171))), % 117.67/117.72 inference(scs_inference,[],[3488,1661,70,69,73])). % 117.67/117.72 cnf(3519,plain, % 117.67/117.72 (~E(f16(a11),f16(a5))), % 117.67/117.72 inference(scs_inference,[],[3498,3488,1661,70,69,73,2])). % 117.67/117.72 cnf(3520,plain, % 117.67/117.72 (P1(f19(f15(x35201),f17(x35202)))), % 117.67/117.72 inference(scs_inference,[],[3498,3488,3504,1661,48,70,69,73,2,67])). % 117.67/117.72 cnf(3521,plain, % 117.67/117.72 (~P6(x35211,f19(f15(x35212),f17(x35213)))), % 117.67/117.72 inference(rename_variables,[],[3504])). % 117.67/117.72 cnf(3522,plain, % 117.67/117.72 (P2(f9(x35221),x35221)), % 117.67/117.72 inference(rename_variables,[],[48])). % 117.67/117.72 cnf(3530,plain, % 117.67/117.72 (~P8(f17(x35301),f18(f15(x35302)))), % 117.67/117.72 inference(scs_inference,[],[3498,3488,3464,3463,3504,3415,1661,1810,3417,3442,50,48,3522,70,69,73,2,67,3,14,20,18])). % 117.67/117.72 cnf(3531,plain, % 117.67/117.72 (~E(f10(f16(a13),f15(x35311)),a8)), % 117.67/117.72 inference(scs_inference,[],[3498,3488,3506,3464,3463,3504,3415,1661,1810,3130,3417,3442,50,48,3522,70,69,73,2,67,3,14,20,18,19])). % 117.67/117.72 cnf(3535,plain, % 117.67/117.72 (P2(f10(f17(x35351),f15(x35352)),f17(x35351))), % 117.67/117.72 inference(scs_inference,[],[3498,3488,3506,3464,3463,3504,3521,3415,1661,1810,3130,3417,3442,50,48,3522,70,69,73,2,67,3,14,20,18,19,16,66])). % 117.67/117.72 cnf(3537,plain, % 117.67/117.72 (P6(x35371,f18(f18(a13)))+E(f19(f18(a13),f17(x35371)),a1)), % 117.67/117.72 inference(scs_inference,[],[3498,3488,3506,3464,3463,3504,3521,3415,1661,1810,3130,3417,2970,3442,50,48,3522,70,69,73,2,67,3,14,20,18,19,16,66,71])). % 117.67/117.72 cnf(3544,plain, % 117.67/117.72 (~P2(f18(a14),f16(a2))), % 117.67/117.72 inference(scs_inference,[],[3520,1744,57,56,70])). % 117.67/117.72 cnf(3548,plain, % 117.67/117.72 (P6(f10(f18(a14),a2),f18(a14))), % 117.67/117.72 inference(scs_inference,[],[3517,3520,1744,57,56,70,69,73])). % 117.67/117.72 cnf(3553,plain, % 117.67/117.72 (~E(f16(a1),f16(a5))), % 117.67/117.72 inference(scs_inference,[],[3519,3517,3053,3251,3520,3298,1744,1708,57,56,70,69,73,2,67,3])). % 117.67/117.72 cnf(3555,plain, % 117.67/117.72 (P2(x35551,f16(x35551))), % 117.67/117.72 inference(rename_variables,[],[2764])). % 117.67/117.72 cnf(3562,plain, % 117.67/117.72 (P2(f10(f17(x35621),a1),f17(x35621))), % 117.67/117.72 inference(scs_inference,[],[3519,3517,3535,3053,3470,3251,3520,3530,3298,3313,1744,2972,1708,2760,2764,3555,47,57,56,70,69,73,2,67,3,76,14,20,18,19])). % 117.67/117.72 cnf(3574,plain, % 117.67/117.72 (~P2(f18(a14),f16(a13))), % 117.67/117.72 inference(scs_inference,[],[1749,70])). % 117.67/117.72 cnf(3578,plain, % 117.67/117.72 (P6(f10(f18(a14),a13),f18(a14))), % 117.67/117.72 inference(scs_inference,[],[3548,1749,70,69,73])). % 117.67/117.72 cnf(3583,plain, % 117.67/117.72 (~E(a1,f12(a5))), % 117.67/117.72 inference(scs_inference,[],[3553,3548,3217,3201,1749,2872,70,69,73,2,75,3])). % 117.67/117.72 cnf(3584,plain, % 117.67/117.72 (~E(f19(f15(x35841),f17(x35842)),f12(a8))), % 117.67/117.72 inference(scs_inference,[],[3553,3548,3217,3201,1749,3520,2598,2872,70,69,73,2,75,3,14])). % 117.67/117.72 cnf(3585,plain, % 117.67/117.72 (P2(f9(f15(a13)),f15(a1))), % 117.67/117.72 inference(scs_inference,[],[3553,3548,3217,3201,3419,1749,3520,2598,2872,48,70,69,73,2,75,3,14,20])). % 117.67/117.72 cnf(3587,plain, % 117.67/117.72 (~P8(f17(x35871),f18(f18(a13)))), % 117.67/117.72 inference(scs_inference,[],[3553,3548,3217,3201,3419,3088,1749,1303,3520,2598,2872,48,70,69,73,2,75,3,14,20,18])). % 117.67/117.72 cnf(3600,plain, % 117.67/117.72 (~P2(f18(a14),f16(a11))), % 117.67/117.72 inference(scs_inference,[],[2351,70])). % 117.67/117.72 cnf(3604,plain, % 117.67/117.72 (P6(f10(f18(a14),a11),f18(a14))), % 117.67/117.72 inference(scs_inference,[],[3578,2351,70,69,73])). % 117.67/117.72 cnf(3606,plain, % 117.67/117.72 (~E(f12(a5),a1)), % 117.67/117.72 inference(scs_inference,[],[3583,3578,2351,70,69,73,2])). % 117.67/117.72 cnf(3607,plain, % 117.67/117.72 (~E(f12(a8),f18(a1))), % 117.67/117.72 inference(scs_inference,[],[3583,3578,2645,2351,2457,70,69,73,2,3])). % 117.67/117.72 cnf(3609,plain, % 117.67/117.72 (~E(f16(f18(a14)),f16(a13))), % 117.67/117.72 inference(scs_inference,[],[3574,3583,3578,2645,2351,2457,3020,28,2764,70,69,73,2,3,14,20])). % 117.67/117.72 cnf(3615,plain, % 117.67/117.72 (P6(f10(f17(a13),f15(x36151)),f17(a1))), % 117.67/117.72 inference(scs_inference,[],[3574,3583,3466,3578,3585,2645,3587,3422,2351,3517,2457,3020,28,2764,47,70,69,73,2,3,14,20,18,19,16])). % 117.67/117.72 cnf(3629,plain, % 117.67/117.72 (~P2(f16(x36291),f16(a13))), % 117.67/117.72 inference(scs_inference,[],[3615,1264,66,70])). % 117.67/117.72 cnf(3633,plain, % 117.67/117.72 (P6(f10(f16(x36331),a2),f16(x36331))), % 117.67/117.72 inference(scs_inference,[],[3604,3615,1260,1264,66,70,69,73])). % 117.67/117.72 cnf(3637,plain, % 117.67/117.72 (~E(f18(f18(a11)),f12(a14))), % 117.67/117.72 inference(scs_inference,[],[2963,3604,3615,3423,1260,1264,2925,359,2459,66,70,69,73,2,3,14])). % 117.67/117.72 cnf(3653,plain, % 117.67/117.72 (P2(f10(f16(x36531),a2),f16(x36531))), % 117.67/117.72 inference(scs_inference,[],[3633,66])). % 117.67/117.72 cnf(3655,plain, % 117.67/117.72 (~P2(f17(x36551),f16(a2))), % 117.67/117.72 inference(scs_inference,[],[3633,1307,66,70])). % 117.67/117.72 cnf(3657,plain, % 117.67/117.72 (~P6(f16(x36571),f10(f16(x36571),a2))), % 117.67/117.72 inference(scs_inference,[],[3633,1307,66,70,69])). % 117.67/117.72 cnf(3659,plain, % 117.67/117.72 (P6(f10(f17(x36591),a2),f17(x36591))), % 117.67/117.72 inference(scs_inference,[],[3633,1307,66,70,69,73])). % 117.67/117.72 cnf(3662,plain, % 117.67/117.72 (~E(f12(a8),f18(a2))), % 117.67/117.72 inference(scs_inference,[],[3607,3079,3633,3374,1307,66,70,69,73,2,3])). % 117.67/117.72 cnf(3663,plain, % 117.67/117.72 (~E(a11,f12(f16(x36631)))), % 117.67/117.72 inference(scs_inference,[],[3607,3079,3633,3374,1307,3077,29,66,70,69,73,2,3,14])). % 117.67/117.72 cnf(3664,plain, % 117.67/117.72 (~E(f16(f16(x36641)),f16(a13))), % 117.67/117.72 inference(scs_inference,[],[3607,3629,3079,3633,3374,1307,3077,29,2764,66,70,69,73,2,3,14,20])). % 117.67/117.72 cnf(3676,plain, % 117.67/117.72 (P1(f19(a13,f17(x36761)))), % 117.67/117.72 inference(scs_inference,[],[3607,3629,3079,3633,3482,3146,3118,3374,3480,3371,1307,3077,3442,29,47,2764,82,48,66,70,69,73,2,3,14,20,18,16,62,673,67])). % 117.67/117.72 cnf(3681,plain, % 117.67/117.72 (P4(f19(a13,f17(x36811)))), % 117.67/117.72 inference(scs_inference,[],[3676,57])). % 117.67/117.72 cnf(3685,plain, % 117.67/117.72 (P3(f19(a13,f17(x36851)))), % 117.67/117.72 inference(scs_inference,[],[3659,3676,57,66,56])). % 117.67/117.72 cnf(3687,plain, % 117.67/117.72 (~P2(f17(x36871),f16(a13))), % 117.67/117.72 inference(scs_inference,[],[3659,3676,1311,57,66,56,70])). % 117.67/117.72 cnf(3689,plain, % 117.67/117.72 (~P6(f17(x36891),f10(f17(x36891),a2))), % 117.67/117.72 inference(scs_inference,[],[3659,3676,1311,57,66,56,70,69])). % 117.67/117.72 cnf(3691,plain, % 117.67/117.72 (P6(f10(f17(x36911),a13),f17(x36911))), % 117.67/117.72 inference(scs_inference,[],[3659,3676,1311,57,66,56,70,69,73])). % 117.67/117.72 cnf(3694,plain, % 117.67/117.72 (P6(f10(f17(x36941),a1),f17(x36941))), % 117.67/117.72 inference(scs_inference,[],[3662,3562,3659,3676,1311,53,57,66,56,70,69,73,2,67])). % 117.67/117.72 cnf(3697,plain, % 117.67/117.72 (E(f10(a13,a13),f10(a1,a1))), % 117.67/117.72 inference(scs_inference,[],[3662,3562,3659,3676,3420,1311,3418,53,57,66,56,70,69,73,2,67,3])). % 117.67/117.72 cnf(3698,plain, % 117.67/117.72 (E(f10(x36981,a13),f10(x36981,a1))), % 117.67/117.72 inference(rename_variables,[],[3420])). % 117.67/117.72 cnf(3701,plain, % 117.67/117.72 (P2(f9(f10(x37011,a13)),f10(x37011,a1))), % 117.67/117.72 inference(scs_inference,[],[3662,3562,3659,3676,3420,3698,1311,3418,50,53,48,57,66,56,70,69,73,2,67,3,14,20])). % 117.67/117.72 cnf(3703,plain, % 117.67/117.72 (~P8(a5,f19(a11,f17(x37031)))), % 117.67/117.72 inference(scs_inference,[],[3662,3562,3659,3676,3420,3698,3011,1311,3418,1234,50,53,48,57,66,56,70,69,73,2,67,3,14,20,18])). % 117.67/117.72 cnf(3713,plain, % 117.67/117.72 (~P2(f16(x37131),f16(a11))), % 117.67/117.72 inference(scs_inference,[],[3691,1629,66,70])). % 117.67/117.72 cnf(3715,plain, % 117.67/117.72 (~P6(f17(x37151),f10(f17(x37151),a13))), % 117.67/117.72 inference(scs_inference,[],[3691,1629,66,70,69])). % 117.67/117.72 cnf(3717,plain, % 117.67/117.72 (P6(f10(f16(x37171),a11),f16(x37171))), % 117.67/117.72 inference(scs_inference,[],[3691,1629,66,70,69,73])). % 117.67/117.72 cnf(3721,plain, % 117.67/117.72 (P2(f10(f16(x37211),a11),f16(x37211))), % 117.67/117.72 inference(scs_inference,[],[3606,3153,3691,3164,1629,2764,66,70,69,73,2,3,76])). % 117.67/117.72 cnf(3722,plain, % 117.67/117.72 (P2(x37221,f16(x37221))), % 117.67/117.72 inference(rename_variables,[],[2764])). % 117.67/117.72 cnf(3725,plain, % 117.67/117.72 (~E(f16(f17(x37251)),f16(a13))), % 117.67/117.72 inference(scs_inference,[],[3687,3606,3153,3691,3164,1629,2754,2976,2764,3722,66,70,69,73,2,3,76,14,20])). % 117.67/117.72 cnf(3728,plain, % 117.67/117.72 (P8(x37281,x37281)), % 117.67/117.72 inference(rename_variables,[],[47])). % 117.67/117.72 cnf(3729,plain, % 117.67/117.72 (~E(f10(f16(a11),a2),f18(a14))), % 117.67/117.72 inference(scs_inference,[],[3687,3606,3153,3653,3691,3164,3452,3600,1629,2754,2976,47,2764,3722,66,70,69,73,2,3,76,14,20,18,19])). % 117.67/117.72 cnf(3733,plain, % 117.67/117.72 (P6(f10(f17(a2),a13),f17(a1))), % 117.67/117.72 inference(scs_inference,[],[3687,3697,3606,3153,3653,3691,3164,3452,3377,3600,1629,2754,2976,47,3728,2764,3722,66,70,69,73,2,3,76,14,20,18,19,17,16])). % 117.67/117.72 cnf(3735,plain, % 117.67/117.72 (P2(f10(a1,a1),f16(f10(a13,a13)))), % 117.67/117.72 inference(scs_inference,[],[3687,3697,3606,3153,3653,3691,3164,3452,3377,3600,1629,2754,2976,47,3728,2764,3722,66,70,69,73,2,3,76,14,20,18,19,17,16,68])). % 117.67/117.72 cnf(3745,plain, % 117.67/117.72 (~P2(f17(x37451),f16(a11))), % 117.67/117.72 inference(scs_inference,[],[3733,1635,66,70])). % 117.67/117.72 cnf(3749,plain, % 117.67/117.72 (P6(f10(f17(x37491),a11),f17(x37491))), % 117.67/117.72 inference(scs_inference,[],[3717,3733,1635,66,70,69,73])). % 117.67/117.72 cnf(3752,plain, % 117.67/117.72 (P6(f10(a1,a1),f16(f10(a13,a13)))), % 117.67/117.72 inference(scs_inference,[],[3073,3717,3733,3735,1635,52,66,70,69,73,2,67])). % 117.67/117.72 cnf(3756,plain, % 117.67/117.72 (~E(f19(f18(a1),f17(x37561)),f12(a5))), % 117.67/117.72 inference(scs_inference,[],[3073,3717,3733,3735,3376,1635,2677,2804,52,518,66,70,69,73,2,67,3,14])). % 117.67/117.72 cnf(3757,plain, % 117.67/117.72 (P2(f9(f15(a2)),f15(a1))), % 117.67/117.72 inference(scs_inference,[],[3073,3717,3733,3735,3375,3376,1635,2677,2804,52,48,518,66,70,69,73,2,67,3,14,20])). % 117.67/117.72 cnf(3759,plain, % 117.67/117.72 (~P8(f18(a14),f18(f18(a2)))), % 117.67/117.72 inference(scs_inference,[],[3073,3717,3733,3735,3375,3376,2874,1635,1739,2677,2804,52,48,518,66,70,69,73,2,67,3,14,20,18])). % 117.67/117.72 cnf(3760,plain, % 117.67/117.72 (P2(f9(a1),f16(f9(a2)))), % 117.67/117.72 inference(scs_inference,[],[3073,3717,3733,3735,3375,3376,2874,1635,1739,2677,2804,2764,52,48,518,66,70,69,73,2,67,3,14,20,18,19])). % 117.67/117.72 cnf(3770,plain, % 117.67/117.72 (~P2(f12(a14),f16(f18(a1)))), % 117.67/117.72 inference(scs_inference,[],[3749,1814,66,70])). % 117.67/117.72 cnf(3772,plain, % 117.67/117.72 (~P6(f17(x37721),f10(f17(x37721),a11))), % 117.67/117.72 inference(scs_inference,[],[3749,1814,66,70,69])). % 117.67/117.72 cnf(3774,plain, % 117.67/117.72 (P6(f10(f12(a14),f18(a1)),f12(a14))), % 117.67/117.72 inference(scs_inference,[],[3749,1814,66,70,69,73])). % 117.67/117.72 cnf(3779,plain, % 117.67/117.72 (~E(f10(f16(a11),a1),f18(a14))), % 117.67/117.72 inference(scs_inference,[],[2695,3749,3729,1814,3378,2760,66,70,69,73,2,75,3])). % 117.67/117.72 cnf(3784,plain, % 117.67/117.72 (~E(f16(f17(x37841)),f16(a11))), % 117.67/117.72 inference(scs_inference,[],[3745,2695,3749,3729,3515,1814,3424,3378,2866,2760,28,2764,66,70,69,73,2,75,3,14,15,20])). % 117.67/117.72 cnf(3788,plain, % 117.67/117.72 (~E(f10(f16(a2),a11),f18(a14))), % 117.67/117.72 inference(scs_inference,[],[3745,2695,3721,3749,3729,3515,3759,3544,1814,3424,3378,2866,2760,28,47,2764,66,70,69,73,2,75,3,14,15,20,18,19])). % 117.67/117.72 cnf(3803,plain, % 117.67/117.72 (~P6(f12(a14),f10(f12(a14),f18(a1)))), % 117.67/117.72 inference(scs_inference,[],[3774,1665,66,70,69])). % 117.67/117.72 cnf(3805,plain, % 117.67/117.72 (P6(f10(f12(a14),f15(x38051)),f12(a14))), % 117.67/117.72 inference(scs_inference,[],[3774,1665,66,70,69,73])). % 117.67/117.72 cnf(3809,plain, % 117.67/117.72 (P6(f10(f12(a14),f18(a1)),a14)), % 117.67/117.72 inference(scs_inference,[],[2736,3774,3379,1665,2459,413,66,70,69,73,2,3,74])). % 117.67/117.72 cnf(3811,plain, % 117.67/117.72 (~E(f10(f12(a14),f18(a1)),f16(a14))), % 117.67/117.72 inference(scs_inference,[],[2736,3774,3379,1665,423,2459,413,66,70,69,73,2,3,74,15])). % 117.67/117.72 cnf(3815,plain, % 117.67/117.72 (P2(f12(a1),f16(f12(a2)))), % 117.67/117.72 inference(scs_inference,[],[2736,3774,3379,2912,1665,1257,423,2459,2764,48,413,66,70,69,73,2,3,74,15,20,18,19])). % 117.67/117.72 cnf(3823,plain, % 117.67/117.72 (P2(f10(f12(a14),f15(x38231)),f12(a14))), % 117.67/117.72 inference(scs_inference,[],[3805,66])). % 117.67/117.72 cnf(3825,plain, % 117.67/117.72 (~P2(f12(a14),f16(a13))), % 117.67/117.72 inference(scs_inference,[],[3805,1334,66,70])). % 117.67/117.72 cnf(3829,plain, % 117.67/117.72 (P6(f10(f12(a14),a13),f12(a14))), % 117.67/117.72 inference(scs_inference,[],[3805,1334,66,70,69,73])). % 117.67/117.72 cnf(3832,plain, % 117.67/117.72 (P6(f19(a1,a1),f16(f19(a13,a13)))), % 117.67/117.72 inference(scs_inference,[],[2696,3805,3502,1334,52,66,70,69,73,2,67])). % 117.67/117.72 cnf(3835,plain, % 117.67/117.72 (~E(f10(f12(a14),a1),f16(a14))), % 117.67/117.72 inference(scs_inference,[],[2696,3811,3805,3502,1334,974,52,66,70,69,73,2,67,3])). % 117.67/117.72 cnf(3841,plain, % 117.67/117.72 (~P2(f12(a14),f16(a1))), % 117.67/117.72 inference(scs_inference,[],[2696,3811,3805,3502,3689,3770,1334,3377,418,974,52,580,66,70,69,73,2,67,3,76,15,20])). % 117.67/117.72 cnf(3850,plain, % 117.67/117.72 (~E(f16(a14),f16(a13))), % 117.67/117.72 inference(scs_inference,[],[2696,3811,3805,3502,3689,3681,3685,3703,3295,3770,1334,3092,3377,3676,418,974,47,52,580,66,70,69,73,2,67,3,76,15,20,18,16,62,427])). % 117.67/117.72 cnf(3858,plain, % 117.67/117.72 (~P2(f12(a14),f16(a11))), % 117.67/117.72 inference(scs_inference,[],[3829,1638,66,70])). % 117.67/117.72 cnf(3860,plain, % 117.67/117.72 (~P6(f12(a14),f10(f12(a14),a13))), % 117.67/117.72 inference(scs_inference,[],[3829,1638,66,70,69])). % 117.67/117.72 cnf(3862,plain, % 117.67/117.72 (P6(f10(f12(a14),a11),f12(a14))), % 117.67/117.72 inference(scs_inference,[],[3829,1638,66,70,69,73])). % 117.67/117.72 cnf(3872,plain, % 117.67/117.72 (~P8(a14,f18(a2))), % 117.67/117.72 inference(scs_inference,[],[3850,3829,3809,3421,2832,1638,2786,423,2764,48,518,66,70,69,73,2,3,76,15,20,18])). % 117.67/117.72 cnf(3878,plain, % 117.67/117.72 (~E(f16(a14),f16(a11))), % 117.67/117.72 inference(scs_inference,[],[3850,3829,3311,3803,3809,3421,3307,2832,1638,2786,423,3275,975,2764,48,518,66,70,69,73,2,3,76,15,20,18,16,62,427])). % 117.67/117.72 cnf(3892,plain, % 117.67/117.72 (P6(f10(a14,f18(a2)),a14)), % 117.67/117.72 inference(scs_inference,[],[3872,3862,1794,66,70,69,73])). % 117.67/117.72 cnf(3895,plain, % 117.67/117.72 (P6(f9(f12(a8)),a8)), % 117.67/117.72 inference(scs_inference,[],[3878,3872,3862,3142,1794,160,66,70,69,73,2,67])). % 117.67/117.72 cnf(3897,plain, % 117.67/117.72 (~E(f10(f16(a11),f18(a1)),f18(a14))), % 117.67/117.72 inference(scs_inference,[],[3878,3872,3862,3779,3142,1794,160,975,66,70,69,73,2,67,3])). % 117.67/117.72 cnf(3903,plain, % 117.67/117.72 (~E(f16(f12(a14)),f16(a11))), % 117.67/117.72 inference(scs_inference,[],[3858,3878,3872,3862,3779,3142,3657,3380,1794,418,160,975,2764,66,70,69,73,2,67,3,76,15,20])). % 117.67/117.72 cnf(3905,plain, % 117.67/117.72 (~P8(a5,f19(f15(x39051),f17(x39052)))), % 117.67/117.72 inference(scs_inference,[],[3858,3878,3872,3862,3779,3142,3657,3462,3001,3380,1794,418,160,975,2764,66,70,69,73,2,67,3,76,15,20,18])). % 117.67/117.72 cnf(3907,plain, % 117.67/117.72 (P2(f19(a1,a1),f16(f19(a11,a2)))), % 117.67/117.72 inference(scs_inference,[],[3858,3878,3872,3862,3779,3142,3657,3334,3373,3462,3001,3380,1794,418,160,975,2764,66,70,69,73,2,67,3,76,15,20,18,19])). % 117.67/117.72 cnf(3910,plain, % 117.67/117.72 (P8(f19(a1,a1),f19(f18(a2),f18(a13)))), % 117.67/117.72 inference(scs_inference,[],[3858,3878,3872,3178,3862,3779,3142,3657,3334,3373,3462,3001,3380,1794,418,160,975,47,2764,66,70,69,73,2,67,3,76,15,20,18,19,17])). % 117.67/117.72 cnf(3912,plain, % 117.67/117.72 (~P6(x39121,f19(f18(a11),f17(x39122)))), % 117.67/117.72 inference(scs_inference,[],[3858,3878,3872,3178,3862,3779,3142,3657,3334,3373,3462,3258,3001,3380,1794,418,160,975,47,2764,82,66,70,69,73,2,67,3,76,15,20,18,19,17,16])). % 117.67/117.72 cnf(3923,plain, % 117.67/117.72 (~P6(f16(f10(a13,a13)),f10(a1,a1))), % 117.67/117.72 inference(scs_inference,[],[3752,3892,1807,66,70,69])). % 117.67/117.72 cnf(3925,plain, % 117.67/117.72 (P6(f10(a8,f18(a1)),a8)), % 117.67/117.72 inference(scs_inference,[],[3752,3892,1807,66,70,69,73])). % 117.67/117.72 cnf(3928,plain, % 117.67/117.72 (P1(f19(f18(a11),f17(x39281)))), % 117.67/117.72 inference(scs_inference,[],[2734,3752,3912,3892,1807,48,66,70,69,73,2,67])). % 117.67/117.72 cnf(3930,plain, % 117.67/117.72 (P2(f9(x39301),x39301)), % 117.67/117.72 inference(rename_variables,[],[48])). % 117.67/117.72 cnf(3933,plain, % 117.67/117.72 (P2(x39331,f16(x39331))), % 117.67/117.72 inference(rename_variables,[],[2764])). % 117.67/117.72 cnf(3936,plain, % 117.67/117.72 (~E(a11,f12(f18(a14)))), % 117.67/117.72 inference(scs_inference,[],[2734,3752,3912,3892,3297,1807,2919,29,2459,2764,48,66,70,69,73,2,67,76,3,14])). % 117.67/117.72 cnf(3937,plain, % 117.67/117.72 (~E(f10(f12(a14),a11),f16(a14))), % 117.67/117.72 inference(scs_inference,[],[2734,3752,3912,3892,3297,1807,2919,3862,423,29,2459,2764,48,66,70,69,73,2,67,76,3,14,15])). % 117.67/117.72 cnf(3940,plain, % 117.67/117.72 (~P8(a8,f18(f15(x39401)))), % 117.67/117.72 inference(scs_inference,[],[2734,3752,3912,3892,3297,3463,1807,2919,3862,423,29,2459,2764,48,3930,66,70,69,73,2,67,76,3,14,15,20,18])). % 117.67/117.72 cnf(3944,plain, % 117.67/117.72 (P6(x39441,f18(f18(a2)))+E(f19(f18(a2),f17(x39441)),a1)), % 117.67/117.72 inference(scs_inference,[],[2734,3752,3912,3860,3892,3297,3463,1807,2919,3862,2752,423,418,29,2459,2764,3933,48,3930,66,70,69,73,2,67,76,3,14,15,20,18,16,19,71])). % 117.67/117.72 cnf(3954,plain, % 117.67/117.72 (~P6(f16(f19(a13,a13)),f19(a1,a1))), % 117.67/117.72 inference(scs_inference,[],[3832,3928,1238,57,56,70,69])). % 117.67/117.72 cnf(3956,plain, % 117.67/117.72 (P6(f10(a5,a2),a5)), % 117.67/117.72 inference(scs_inference,[],[3832,3928,1238,57,56,70,69,73])). % 117.67/117.72 cnf(3958,plain, % 117.67/117.72 (~E(f16(a14),f10(f12(a14),a1))), % 117.67/117.72 inference(scs_inference,[],[3835,3832,3928,1238,57,56,70,69,73,2])). % 117.67/117.72 cnf(3959,plain, % 117.67/117.72 (P6(f19(a1,a1),f16(f19(a11,a2)))), % 117.67/117.72 inference(scs_inference,[],[3835,3832,3907,3928,1238,52,57,56,70,69,73,2,67])). % 117.67/117.72 cnf(3964,plain, % 117.67/117.72 (~E(f10(f16(a2),a1),f18(a14))), % 117.67/117.72 inference(scs_inference,[],[3835,3788,3832,3907,3928,3841,3295,1238,418,52,57,56,70,69,73,2,67,76,3])). % 117.67/117.72 cnf(3966,plain, % 117.67/117.72 (~E(f19(f18(a11),f17(x39661)),f12(a8))), % 117.67/117.72 inference(scs_inference,[],[3835,3788,3832,3907,3928,3841,3295,1238,2598,418,52,57,56,70,69,73,2,67,76,3,14])). % 117.67/117.72 cnf(3969,plain, % 117.67/117.72 (~E(f16(f12(a14)),f16(a13))), % 117.67/117.72 inference(scs_inference,[],[3835,3788,3832,3715,3907,3928,3825,3841,3294,3295,1238,2598,418,2764,52,57,56,70,69,73,2,67,76,3,14,15,20])). % 117.67/117.72 cnf(3973,plain, % 117.67/117.72 (~P6(f16(f19(a13,a13)),f19(a1,a11))), % 117.67/117.72 inference(scs_inference,[],[3835,3788,3832,3715,3907,3928,3905,3293,3825,3841,3294,3295,1238,2598,418,47,2764,52,57,56,70,69,73,2,67,76,3,14,15,20,18,16])). % 117.67/117.72 cnf(3980,plain, % 117.67/117.72 (P6(f10(f12(a14),f15(x39801)),a14)), % 117.67/117.72 inference(scs_inference,[],[3835,3788,3832,3715,3907,3928,3905,3293,3825,3841,3294,3295,1238,3805,3418,2598,418,47,2764,52,413,57,56,70,69,73,2,67,76,3,14,15,20,18,16,66,673,74])). % 117.67/117.72 cnf(3986,plain, % 117.67/117.72 (~P2(f17(x39861),f16(f18(a1)))), % 117.67/117.72 inference(scs_inference,[],[3980,1810,66,70])). % 117.67/117.72 cnf(3990,plain, % 117.67/117.72 (P6(f10(a8,a11),a8)), % 117.67/117.72 inference(scs_inference,[],[3956,3980,1632,1810,66,70,69,73])). % 117.67/117.72 cnf(3997,plain, % 117.67/117.72 (~E(f18(a11),f12(f12(a14)))), % 117.67/117.72 inference(scs_inference,[],[3956,3147,3663,3980,3264,1632,1810,2972,2872,2764,66,70,69,73,2,76,3,14])). % 117.67/117.72 cnf(4000,plain, % 117.67/117.72 (~P8(f17(x40001),f19(f15(x40002),f17(x40003)))), % 117.67/117.72 inference(scs_inference,[],[3956,3147,3663,3980,3349,3264,3196,1632,1810,1303,2972,2872,2764,48,66,70,69,73,2,76,3,14,20,18])). % 117.67/117.72 cnf(4006,plain, % 117.67/117.72 (~P2(a5,f16(f18(a11)))), % 117.67/117.72 inference(scs_inference,[],[3956,3147,3973,3663,3980,3349,3264,3196,3372,1632,1810,1303,2972,2849,2872,2764,48,66,70,69,73,2,76,3,14,20,18,16,712,75])). % 117.67/117.72 cnf(4012,plain, % 117.67/117.72 (~P2(f12(a8),f16(a2))), % 117.67/117.72 inference(scs_inference,[],[2603,70])). % 117.67/117.72 cnf(4016,plain, % 117.67/117.72 (P6(f10(a5,a11),a5)), % 117.67/117.72 inference(scs_inference,[],[3959,1626,2603,70,69,73])). % 117.67/117.72 cnf(4019,plain, % 117.67/117.72 (P6(f9(a1),f16(f9(a2)))), % 117.67/117.72 inference(scs_inference,[],[3937,3959,3760,1626,2603,52,70,69,73,2,67])). % 117.67/117.72 cnf(4024,plain, % 117.67/117.72 (~E(f10(f16(a2),f18(a1)),f18(a14))), % 117.67/117.72 inference(scs_inference,[],[3937,3964,3959,3760,1626,2603,2993,975,52,70,69,73,2,67,76,3])). % 117.67/117.72 cnf(4031,plain, % 117.67/117.72 (~E(f15(a2),f12(a8))), % 117.67/117.72 inference(scs_inference,[],[3954,3937,3964,4000,3959,3986,3760,3416,1626,2603,2993,975,47,52,580,70,69,73,2,67,76,3,20,18,16,137])). % 117.67/117.72 cnf(4038,plain, % 117.67/117.72 (~P2(f12(a14),f16(a2))), % 117.67/117.72 inference(scs_inference,[],[1330,70])). % 117.67/117.72 cnf(4042,plain, % 117.67/117.72 (P6(f10(f12(a8),a13),f12(a8))), % 117.67/117.72 inference(scs_inference,[],[4016,2621,1330,70,69,73])). % 117.67/117.72 cnf(4045,plain, % 117.67/117.72 (P2(f10(f12(a8),a13),a8)), % 117.67/117.72 inference(scs_inference,[],[4016,4031,2621,1330,2870,70,69,73,2,76])). % 117.67/117.72 cnf(4047,plain, % 117.67/117.72 (E(f19(f18(a13),f15(x40471)),f19(a1,a1))), % 117.67/117.72 inference(scs_inference,[],[4016,4031,3464,3066,2621,1330,2870,70,69,73,2,76,3])). % 117.67/117.72 cnf(4054,plain, % 117.67/117.72 (~P8(f12(a8),f15(x40541))), % 117.67/117.72 inference(scs_inference,[],[4016,4031,3772,3433,3464,3446,3066,2621,2636,1330,3422,2870,48,70,69,73,2,76,3,15,20,18])). % 117.67/117.72 cnf(4072,plain, % 117.67/117.72 (P6(f10(f12(a8),f15(x40721)),f12(a8))), % 117.67/117.72 inference(scs_inference,[],[4054,4042,70,69,73])). % 117.67/117.72 cnf(4078,plain, % 117.67/117.72 (~E(f10(f12(a8),a13),f16(a8))), % 117.67/117.72 inference(scs_inference,[],[4054,4038,3584,4042,3406,3374,3034,418,70,69,73,2,76,3,15])). % 117.67/117.72 cnf(4082,plain, % 117.67/117.72 (P8(x40821,x40821)), % 117.67/117.72 inference(rename_variables,[],[47])). % 117.67/117.72 cnf(4088,plain, % 117.67/117.72 (~E(f15(f15(x40881)),f12(a8))), % 117.67/117.72 inference(scs_inference,[],[4054,4038,3923,4047,3584,4042,3406,3940,2982,2917,3697,3374,3034,2925,418,47,4082,2764,70,69,73,2,76,3,15,20,18,17,16,62,137])). % 117.67/117.72 cnf(4098,plain, % 117.67/117.72 (~P2(a5,f16(a1))), % 117.67/117.72 inference(scs_inference,[],[1234,70])). % 117.67/117.72 cnf(4102,plain, % 117.67/117.72 (P6(f10(f16(x41021),f18(a1)),f16(x41021))), % 117.67/117.72 inference(scs_inference,[],[4072,1803,1234,70,69,73])). % 117.67/117.72 cnf(4105,plain, % 117.67/117.72 (P6(f12(a1),f16(f12(a2)))), % 117.67/117.72 inference(scs_inference,[],[4078,4072,3815,1803,1234,52,70,69,73,2,67])). % 117.67/117.72 cnf(4114,plain, % 117.67/117.72 (~P8(f12(a14),f18(f15(x41141)))), % 117.67/117.72 inference(scs_inference,[],[4078,4072,3815,3531,3470,3124,3293,1803,1326,1234,2870,52,48,70,69,73,2,67,76,3,20,18])). % 117.67/117.72 cnf(4115,plain, % 117.67/117.72 (P2(f19(a1,a1),f16(f19(a11,a11)))), % 117.67/117.72 inference(scs_inference,[],[4078,4072,3815,3531,3470,3334,3124,3293,1803,1326,1234,2870,52,48,70,69,73,2,67,76,3,20,18,19])). % 117.67/117.72 cnf(4121,plain, % 117.67/117.72 (P2(f10(f16(x41211),f18(a1)),f16(x41211))), % 117.67/117.72 inference(scs_inference,[],[4078,4072,3815,3207,3531,3470,3334,3124,3293,1803,1326,1234,2870,975,52,48,70,69,73,2,67,76,3,20,18,19,16,430,66])). % 117.67/117.72 cnf(4126,plain, % 117.67/117.72 (P6(f10(f12(a14),a11),a14)), % 117.67/117.72 inference(scs_inference,[],[4078,4072,3815,3207,3531,3470,3334,3124,3293,1803,1326,1234,3862,2870,3065,975,52,48,413,70,69,73,2,67,76,3,20,18,19,16,430,66,673,74])). % 117.67/117.72 cnf(4132,plain, % 117.67/117.72 (~P2(a8,f16(f18(a7)))), % 117.67/117.72 inference(scs_inference,[],[4126,54,66,70])). % 117.67/117.72 cnf(4134,plain, % 117.67/117.72 (~P6(f16(x41341),f10(f16(x41341),f18(a1)))), % 117.67/117.72 inference(scs_inference,[],[4102,4126,54,66,70,69])). % 117.67/117.72 cnf(4136,plain, % 117.67/117.72 (P6(f10(f16(x41361),a13),f16(x41361))), % 117.67/117.72 inference(scs_inference,[],[4102,4126,1264,54,66,70,69,73])). % 117.67/117.72 cnf(4138,plain, % 117.67/117.72 (~E(f16(a13),f16(f16(x41381)))), % 117.67/117.72 inference(scs_inference,[],[4102,3664,4126,1264,54,66,70,69,73,2])). % 117.67/117.72 cnf(4141,plain, % 117.67/117.72 (~E(f10(f12(a8),f15(x41411)),f16(a8))), % 117.67/117.72 inference(scs_inference,[],[4102,3664,3495,4126,3290,1264,4072,3034,3020,30,54,66,70,69,73,2,3,14,15])). % 117.67/117.72 cnf(4142,plain, % 117.67/117.72 (~E(f16(a5),f16(f18(a11)))), % 117.67/117.72 inference(scs_inference,[],[4102,3664,3495,4126,4006,3290,1264,4072,3034,3020,30,2764,54,66,70,69,73,2,3,14,15,20])). % 117.67/117.72 cnf(4149,plain, % 117.67/117.72 (E(f19(f18(a13),f17(x41491)),a1)), % 117.67/117.72 inference(scs_inference,[],[4098,4102,4121,3664,3495,4114,4126,4006,3060,3290,1264,4072,3034,3020,339,30,47,2764,54,66,70,69,73,2,3,14,15,20,18,19,16,3537])). % 117.67/117.72 cnf(4160,plain, % 117.67/117.72 (P6(f10(a14,f18(a1)),a14)), % 117.67/117.72 inference(scs_inference,[],[4136,1794,66,69,73])). % 117.67/117.72 cnf(4170,plain, % 117.67/117.72 (~P8(a8,f19(f18(a13),f17(x41701)))), % 117.67/117.72 inference(scs_inference,[],[4136,3725,4134,4149,2953,2851,3373,3424,1794,1280,48,66,69,73,2,3,15,20,18])). % 117.67/117.72 cnf(4171,plain, % 117.67/117.72 (P2(f10(f16(x41711),a1),f16(x41711))), % 117.67/117.72 inference(scs_inference,[],[4136,3725,4134,4149,3425,2953,2851,3373,2957,3424,1794,1280,48,66,69,73,2,3,15,20,18,19])). % 117.67/117.72 cnf(4181,plain, % 117.67/117.72 (~P6(f16(f9(a2)),f9(a1))), % 117.67/117.72 inference(scs_inference,[],[4019,69])). % 117.67/117.72 cnf(4183,plain, % 117.67/117.72 (P6(f10(f17(x41831),f18(a1)),f17(x41831))), % 117.67/117.72 inference(scs_inference,[],[4019,1810,69,73])). % 117.67/117.72 cnf(4186,plain, % 117.67/117.72 (P6(f10(f16(x41861),a1),f16(x41861))), % 117.67/117.72 inference(scs_inference,[],[4171,3784,4019,1810,52,69,73,2,67])). % 117.67/117.72 cnf(4189,plain, % 117.67/117.72 (P2(f10(f17(x41891),f18(a1)),f17(x41891))), % 117.67/117.72 inference(scs_inference,[],[4171,3784,4019,1810,2764,52,69,73,2,67,76])). % 117.67/117.72 cnf(4190,plain, % 117.67/117.72 (P2(x41901,f16(x41901))), % 117.67/117.72 inference(rename_variables,[],[2764])). % 117.67/117.72 cnf(4198,plain, % 117.67/117.72 (~P6(x41981,f19(f18(a13),f17(x41982)))), % 117.67/117.72 inference(scs_inference,[],[4171,3784,3823,3105,4019,4170,4132,4149,3415,1810,438,47,2764,4190,82,52,69,73,2,67,76,3,20,18,19,16])). % 117.67/117.72 cnf(4205,plain, % 117.67/117.72 (~P6(f17(x42051),f10(f17(x42051),f18(a1)))), % 117.67/117.72 inference(scs_inference,[],[4183,69])). % 117.67/117.72 cnf(4207,plain, % 117.67/117.72 (P6(f10(f12(a8),a2),f12(a8))), % 117.67/117.72 inference(scs_inference,[],[4183,2603,69,73])). % 117.67/117.72 cnf(4212,plain, % 117.67/117.72 (P1(f19(f18(a13),f17(x42121)))), % 117.67/117.72 inference(scs_inference,[],[4183,4088,4198,2603,2976,48,69,73,2,75,67])). % 117.67/117.72 cnf(4213,plain, % 117.67/117.72 (~P6(x42131,f19(f18(a13),f17(x42132)))), % 117.67/117.72 inference(rename_variables,[],[4198])). % 117.67/117.72 cnf(4214,plain, % 117.67/117.72 (P2(f9(x42141),x42141)), % 117.67/117.72 inference(rename_variables,[],[48])). % 117.67/117.72 cnf(4216,plain, % 117.67/117.72 (E(f19(f15(x42161),f18(a13)),f19(a1,a1))), % 117.67/117.72 inference(scs_inference,[],[4183,4088,4198,3061,3462,2603,2976,48,69,73,2,75,67,3])). % 117.67/117.72 cnf(4217,plain, % 117.67/117.72 (E(f19(x42171,f18(a13)),f19(x42171,a1))), % 117.67/117.72 inference(rename_variables,[],[3061])). % 117.67/117.72 cnf(4223,plain, % 117.67/117.72 (P2(f19(a1,x42231),f16(f19(a13,x42231)))), % 117.67/117.72 inference(scs_inference,[],[4183,4088,3910,4198,3061,4217,3296,3462,3417,2603,2976,2764,48,4214,69,73,2,75,67,3,20,18,19])). % 117.67/117.72 cnf(4227,plain, % 117.67/117.72 (P2(f10(f12(a8),a2),f12(a8))), % 117.67/117.72 inference(scs_inference,[],[4183,4088,3910,4198,4213,3061,4217,3296,3462,3417,2603,2976,2764,48,4214,69,73,2,75,67,3,20,18,19,16,66])). % 117.67/117.72 cnf(4238,plain, % 117.67/117.72 (~P6(f16(f12(a2)),f12(a1))), % 117.67/117.72 inference(scs_inference,[],[4212,4105,57,56,69])). % 117.67/117.72 cnf(4243,plain, % 117.67/117.72 (P6(f19(a1,a1),f16(f19(a11,a11)))), % 117.67/117.72 inference(scs_inference,[],[2746,4115,4212,4105,2636,52,57,56,69,73,2,67])). % 117.67/117.72 cnf(4247,plain, % 117.67/117.72 (~E(f19(f18(a13),f17(x42471)),f18(a14))), % 117.67/117.72 inference(scs_inference,[],[2746,4115,4212,3327,4105,3415,2636,1708,52,57,56,69,73,2,67,3,14])). % 117.67/117.72 cnf(4248,plain, % 117.67/117.72 (~P6(f17(a2),f10(f17(a1),f18(a1)))), % 117.67/117.72 inference(scs_inference,[],[2746,4205,4115,4212,3327,4105,3377,3415,2636,1708,52,57,56,69,73,2,67,3,14,15])). % 117.67/117.72 cnf(4250,plain, % 117.67/117.72 (~E(f16(a8),f16(a2))), % 117.67/117.72 inference(scs_inference,[],[2746,4205,4115,4212,3327,4105,4012,3377,3415,2636,2870,1708,52,57,56,69,73,2,67,3,14,15,20])). % 117.67/117.72 cnf(4251,plain, % 117.67/117.72 (~P8(a5,f18(a2))), % 117.67/117.72 inference(scs_inference,[],[2746,4205,4115,4212,3327,4105,4012,2832,3001,3377,3415,2636,2870,1708,52,57,56,69,73,2,67,3,14,15,20,18])). % 117.67/117.72 cnf(4259,plain, % 117.67/117.72 (E(f19(f18(a2),f17(x42591)),a1)), % 117.67/117.72 inference(scs_inference,[],[4216,4227,2746,4205,4115,4212,3327,4105,3205,2819,4012,2853,2832,3137,3001,3377,3415,2636,2779,2870,1708,339,47,52,57,56,69,73,2,67,3,14,15,20,18,19,17,16,62,3944])). % 117.67/117.72 cnf(4261,plain, % 117.67/117.72 (~P2(a5,f16(f18(a2)))), % 117.67/117.72 inference(scs_inference,[],[4216,4227,2746,4205,4115,4212,3327,4105,3205,2819,4012,2853,2832,3137,3001,3377,3415,2636,2779,2870,1708,339,47,52,57,56,69,73,2,67,3,14,15,20,18,19,17,16,62,3944,70])). % 117.67/117.72 cnf(4269,plain, % 117.67/117.72 (P6(f10(a5,f18(a2)),a5)), % 117.67/117.72 inference(scs_inference,[],[4251,4243,69,73])). % 117.67/117.72 cnf(4271,plain, % 117.67/117.72 (~E(f16(a2),f16(a8))), % 117.67/117.72 inference(scs_inference,[],[4250,4251,4243,69,73,2])). % 117.67/117.72 cnf(4278,plain, % 117.67/117.72 (~P8(f18(a14),f19(f18(a2),f17(x42781)))), % 117.67/117.72 inference(scs_inference,[],[4250,4251,3757,4243,4259,2850,3433,3371,1739,3077,28,69,73,2,3,14,20,18])). % 117.67/117.72 cnf(4295,plain, % 117.67/117.72 (P6(f10(f12(a14),a1),f12(a14))), % 117.67/117.72 inference(scs_inference,[],[4269,1326,69,73])). % 117.67/117.72 cnf(4298,plain, % 117.67/117.72 (P6(f19(a1,x42981),f16(f19(a13,x42981)))), % 117.67/117.72 inference(scs_inference,[],[2784,4223,4269,1326,52,69,73,2,67])). % 117.67/117.72 cnf(4301,plain, % 117.67/117.72 (~E(f16(a1),f16(a8))), % 117.67/117.72 inference(scs_inference,[],[4271,2784,4223,4269,1326,3380,52,69,73,2,67,3])). % 117.67/117.72 cnf(4303,plain, % 117.67/117.72 (P2(x43031,f16(x43031))), % 117.67/117.72 inference(rename_variables,[],[2764])). % 117.67/117.72 cnf(4306,plain, % 117.67/117.72 (~P6(x43061,f19(f18(a2),f17(x43062)))), % 117.67/117.72 inference(scs_inference,[],[4271,2784,4223,4278,4269,4261,4259,1326,3380,47,2764,82,52,69,73,2,67,3,20,18,16])). % 117.67/117.72 cnf(4309,plain, % 117.67/117.72 (P2(f19(a1,x43091),f16(f19(a2,x43091)))), % 117.67/117.72 inference(scs_inference,[],[4271,2784,4223,4278,4269,4261,4259,3372,1326,3380,47,2764,4303,82,52,69,73,2,67,3,20,18,16,66,19])). % 117.67/117.72 cnf(4311,plain, % 117.67/117.72 (P2(f10(f12(a8),a2),a8)), % 117.67/117.72 inference(scs_inference,[],[4271,2784,4223,4278,4269,4261,4207,4259,3372,1326,3380,2870,47,2764,4303,82,52,69,73,2,67,3,20,18,16,66,19,76])). % 117.67/117.72 cnf(4315,plain, % 117.67/117.72 (P6(f10(f12(a14),a2),f12(a14))), % 117.67/117.72 inference(scs_inference,[],[4298,1330,69,73])). % 117.67/117.72 cnf(4318,plain, % 117.67/117.72 (P1(f19(f18(a2),f17(x43181)))), % 117.67/117.72 inference(scs_inference,[],[4301,4306,4298,1330,48,69,73,2,67])). % 117.67/117.72 cnf(4320,plain, % 117.67/117.72 (P2(f9(x43201),x43201)), % 117.67/117.72 inference(rename_variables,[],[48])). % 117.67/117.72 cnf(4324,plain, % 117.67/117.72 (P2(f9(a11),a1)), % 117.67/117.72 inference(scs_inference,[],[4301,4306,4298,3936,3264,1330,2754,29,48,4320,69,73,2,67,3,14,20])). % 117.67/117.72 cnf(4326,plain, % 117.67/117.72 (~P8(f16(x43261),f18(f18(a11)))), % 117.67/117.72 inference(scs_inference,[],[4301,4306,4298,3936,2978,3264,1257,1330,2754,29,48,4320,69,73,2,67,3,14,20,18])). % 117.67/117.72 cnf(4344,plain, % 117.67/117.72 (P6(f10(a5,a1),a5)), % 117.67/117.72 inference(scs_inference,[],[4315,4318,1234,57,56,69,73])). % 117.67/117.72 cnf(4356,plain, % 117.67/117.72 (P2(f19(a1,a1),f16(f19(a2,a13)))), % 117.67/117.72 inference(scs_inference,[],[4315,3285,4318,4326,2836,4309,3713,2810,3416,1234,359,47,2764,52,57,56,69,73,2,67,3,14,20,18,19])). % 117.67/117.72 cnf(4402,plain, % 117.67/117.72 (~P6(f16(x44021),f10(f16(x44021),a1))), % 117.67/117.72 inference(scs_inference,[],[4186,69])). % 117.67/117.72 cnf(4404,plain, % 117.67/117.72 (~E(f12(a5),f19(f18(a1),f17(x44041)))), % 117.67/117.72 inference(scs_inference,[],[3756,4186,69,2])). % 117.67/117.72 cnf(4405,plain, % 117.67/117.72 (P6(f19(a1,a1),f16(f19(a2,a13)))), % 117.67/117.72 inference(scs_inference,[],[3756,4356,4186,52,69,2,67])). % 117.67/117.72 cnf(4409,plain, % 117.67/117.72 (~E(f16(f17(x44091)),f16(a2))), % 117.67/117.72 inference(scs_inference,[],[3756,4356,4138,4186,3655,3424,2764,52,69,2,67,3,20])). % 117.67/117.72 cnf(4425,plain, % 117.67/117.72 (~P6(f16(a11),f10(f16(a1),a1))), % 117.67/117.72 inference(scs_inference,[],[4409,4402,4405,2852,3066,3298,69,2,3,15])). % 117.67/117.72 cnf(4460,plain, % 117.67/117.72 (P6(f10(f12(a8),a13),a8)), % 117.67/117.72 inference(scs_inference,[],[3966,4045,4344,3925,2976,160,69,2,75,67])). % 117.67/117.72 cnf(4473,plain, % 117.67/117.72 (P6(f10(f12(a14),a2),a14)), % 117.67/117.72 inference(scs_inference,[],[4141,4460,4315,413,69,2,74])). % 117.67/117.72 cnf(4484,plain, % 117.67/117.72 (P2(f19(a1,a1),f16(f19(a13,a2)))), % 117.67/117.72 inference(scs_inference,[],[4141,4460,4223,3118,2850,4315,3376,3373,3465,1280,2764,48,413,69,2,74,76,3,20,18,19])). % 117.67/117.72 cnf(4498,plain, % 117.67/117.72 (P6(f10(f12(a8),a2),a8)), % 117.67/117.72 inference(scs_inference,[],[4247,4311,4473,160,69,2,67])). % 117.67/117.72 cnf(4518,plain, % 117.67/117.72 (~P8(f18(a14),f19(f18(a1),f17(x45181)))), % 117.67/117.72 inference(scs_inference,[],[2783,4498,2762,2851,2852,3378,1739,48,69,2,3,20,18])). % 117.67/117.72 cnf(4519,plain, % 117.67/117.72 (~P6(f17(a2),f10(f17(a1),a1))), % 117.67/117.72 inference(scs_inference,[],[2783,4248,4498,2762,2851,2852,3378,1739,975,48,69,2,3,20,18,16])). % 117.67/117.72 cnf(4528,plain, % 117.67/117.72 (P6(f10(f12(a8),a1),a8)), % 117.67/117.72 inference(scs_inference,[],[3003,3186,3895,160,69,2,67])). % 117.67/117.72 cnf(4531,plain, % 117.67/117.72 (E(f19(a1,x45311),f19(f18(a1),x45311))), % 117.67/117.72 inference(rename_variables,[],[1761])). % 117.67/117.72 cnf(4534,plain, % 117.67/117.72 (~P8(f18(a14),f19(a1,f17(x45341)))), % 117.67/117.72 inference(scs_inference,[],[3003,3186,4404,4518,3895,3145,160,1761,4531,2764,69,2,67,3,20,18])). % 117.67/117.72 cnf(4540,plain, % 117.67/117.72 (~P2(a14,f16(f18(a11)))), % 117.67/117.72 inference(scs_inference,[],[3003,3186,4425,4404,4518,2927,4160,3895,3145,2868,3470,2872,160,1761,4531,2764,69,2,67,3,20,18,16,62,75])). % 117.67/117.72 cnf(4548,plain, % 117.67/117.72 (P2(f10(f17(a11),f18(a1)),f17(a1))), % 117.67/117.72 inference(scs_inference,[],[4189,3106,4528,2953,3294,3291,69,2,3,20])). % 117.67/117.72 cnf(4555,plain, % 117.67/117.72 (P6(f10(f12(a14),a1),a14)), % 117.67/117.72 inference(scs_inference,[],[4189,3106,4238,4519,4528,2874,2953,3420,4295,3294,3291,1257,413,69,2,3,20,18,16,67,74])). % 117.67/117.72 cnf(4568,plain, % 117.67/117.72 (P6(f10(f17(a11),f18(a1)),f17(a1))), % 117.67/117.72 inference(scs_inference,[],[3182,4548,4555,53,69,2,67])). % 117.67/117.72 cnf(4580,plain, % 117.67/117.72 (~P6(f17(a1),f10(f17(a11),f18(a1)))), % 117.67/117.72 inference(scs_inference,[],[4568,69])). % 117.67/117.72 cnf(4583,plain, % 117.67/117.72 (E(f19(f15(x45831),f15(x45832)),f19(a1,a1))), % 117.67/117.72 inference(scs_inference,[],[3609,4568,3462,3464,69,2,3])). % 117.67/117.72 cnf(4588,plain, % 117.67/117.72 (~P8(f17(x45881),f19(a2,f17(x45882)))), % 117.67/117.72 inference(scs_inference,[],[3609,4568,2912,3374,3462,3464,1303,48,69,2,3,20,18])). % 117.67/117.72 cnf(4593,plain, % 117.67/117.72 (~P6(f17(x45931),f10(f17(x45931),a1))), % 117.67/117.72 inference(scs_inference,[],[3694,69])). % 117.67/117.72 cnf(4596,plain, % 117.67/117.72 (P6(f19(a1,a1),f16(f19(a13,a2)))), % 117.67/117.72 inference(scs_inference,[],[3637,4484,3694,52,69,2,67])). % 117.67/117.72 cnf(4606,plain, % 117.67/117.72 (~P6(f16(f9(a2)),f9(a13))), % 117.67/117.72 inference(scs_inference,[],[3637,4484,4588,3958,4580,3694,3097,4181,3421,2957,3422,47,2764,52,69,2,67,3,15,20,18,16])). % 117.67/117.72 cnf(4607,plain, % 117.67/117.72 (~P2(a8,f16(f18(a2)))), % 117.67/117.72 inference(scs_inference,[],[3637,4484,4588,3958,4580,3990,3694,3097,4181,3421,2957,3422,2760,47,2764,52,69,2,67,3,15,20,18,16,75])). % 117.67/117.72 cnf(4621,plain, % 117.67/117.72 (~P6(f17(x46211),f10(f17(x46211),f18(a13)))), % 117.67/117.72 inference(scs_inference,[],[3897,4593,4596,3201,3061,3290,2959,3063,2636,48,69,2,3,20,18,16])). % 117.67/117.72 cnf(4628,plain, % 117.67/117.72 (P2(f19(a1,a1),f16(f19(a11,a13)))), % 117.67/117.72 inference(scs_inference,[],[3897,4606,4593,4596,3030,3201,3334,3061,3290,2970,2959,3063,3416,2636,3020,2976,29,48,69,2,3,20,18,16,62,67,14,19])). % 117.67/117.72 cnf(4631,plain, % 117.67/117.72 (P8(f19(a1,a1),f19(f15(x46311),f15(x46312)))), % 117.67/117.72 inference(scs_inference,[],[4583,3897,4606,4593,4596,3030,3201,3334,3061,3290,2970,2959,3063,3416,2636,3020,2976,29,47,48,69,2,3,20,18,16,62,67,14,19,17])). % 117.67/117.72 cnf(4638,plain, % 117.67/117.72 (P6(f19(a1,a1),f16(f19(a11,a13)))), % 117.67/117.72 inference(scs_inference,[],[3903,4628,2988,52,69,2,67])). % 117.67/117.72 cnf(4651,plain, % 117.67/117.72 (P6(f10(f18(a14),f18(a2)),f18(a14))), % 117.67/117.72 inference(scs_inference,[],[3903,4621,4628,3247,4534,4607,2988,4181,3289,2832,2923,3377,2764,52,69,2,67,3,15,20,18,16,70,73])). % 117.67/117.72 cnf(4664,plain, % 117.67/117.72 (~P8(f12(a8),f18(f15(x46641)))), % 117.67/117.72 inference(scs_inference,[],[4324,4651,3969,3463,2662,2901,2953,3066,69,2,3,20,18])). % 117.67/117.72 cnf(4682,plain, % 117.67/117.72 (~P6(f16(x46821),f16(f18(a11)))), % 117.67/117.72 inference(scs_inference,[],[4024,4664,3997,4638,2984,2960,3290,2789,47,2764,69,2,3,20,18,16])). % 117.67/117.72 cnf(5069,plain, % 117.67/117.72 (E(f10(a1,x50691),f10(f18(a1),x50691))), % 117.67/117.72 inference(rename_variables,[],[910])). % 117.67/117.72 cnf(5078,plain, % 117.67/117.72 (P2(f9(x50781),x50781)), % 117.67/117.72 inference(rename_variables,[],[48])). % 117.67/117.72 cnf(5081,plain, % 117.67/117.72 (P2(f9(x50811),x50811)), % 117.67/117.72 inference(rename_variables,[],[48])). % 117.67/117.72 cnf(5086,plain, % 117.67/117.72 ($false), % 117.67/117.72 inference(scs_inference,[],[42,518,910,5069,48,5078,5081,963,1761,517,438,2957,3420,3464,3020,2789,3334,3000,3425,3421,3701,4136,4607,4142,2772,4306,4631,4540,619,4682,2,73,70,66,108,55,8,68,107,163,138,17,18,20,19,15,3,67,76,75,71]), % 117.67/117.72 ['proof']). % 117.67/117.72 % SZS output end Proof % 117.67/117.72 % Total time :117.060000s %------------------------------------------------------------------------------