%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU110+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:01:04 EDT 2024 % Result : Theorem 201.12s 201.07s % Output : CNFRefutation 201.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU110+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.34 % Computer : n029.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Jun 21 15:10:54 EDT 2024 % 0.12/0.34 % CPUTime : % 0.44/0.61 start to proof:theBenchmark % 201.08/201.04 %------------------------------------------- % 201.08/201.04 % File :CSE---1.7 % 201.08/201.04 % Problem :theBenchmark % 201.08/201.04 % Transform :cnf % 201.08/201.04 % Format :tptp:raw % 201.08/201.04 % Command :java -jar mcs_scs.jar %d %s % 201.08/201.04 % 201.08/201.04 % Result :Theorem 200.370000s % 201.08/201.04 % Output :CNFRefutation 200.370000s % 201.08/201.04 %------------------------------------------- % 201.12/201.06 %------------------------------------------------------------------------------ % 201.12/201.06 % File : SEU110+1 : TPTP v8.2.0. Released v3.2.0. % 201.12/201.06 % Domain : Set theory % 201.12/201.06 % Problem : Boolean domains, theorem 23 % 201.12/201.06 % Version : [Urb06] axioms : Especial. % 201.12/201.06 % English : % 201.12/201.06 % 201.12/201.06 % Refs : [TD90] Trybulec & Darmochwal (1990), Boolean Domains % 201.12/201.06 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 201.12/201.06 % Source : [Urb06] % 201.12/201.06 % Names : finsub_1__t23_finsub_1 [Urb06] % 201.12/201.06 % 201.12/201.06 % Status : Theorem % 201.12/201.06 % Rating : 0.31 v7.5.0, 0.34 v7.4.0, 0.23 v7.3.0, 0.28 v7.2.0, 0.24 v7.1.0, 0.22 v7.0.0, 0.27 v6.4.0, 0.35 v6.3.0, 0.29 v6.2.0, 0.44 v6.1.0, 0.50 v6.0.0, 0.43 v5.5.0, 0.48 v5.4.0, 0.50 v5.3.0, 0.52 v5.2.0, 0.45 v5.1.0, 0.43 v5.0.0, 0.46 v4.1.0, 0.39 v4.0.1, 0.30 v4.0.0, 0.29 v3.7.0, 0.25 v3.5.0, 0.26 v3.4.0, 0.37 v3.3.0, 0.29 v3.2.0 % 201.12/201.06 % Syntax : Number of formulae : 34 ( 7 unt; 0 def) % 201.12/201.06 % Number of atoms : 93 ( 3 equ) % 201.12/201.06 % Maximal formula atoms : 10 ( 2 avg) % 201.12/201.06 % Number of connectives : 76 ( 17 ~; 1 |; 36 &) % 201.12/201.06 % ( 4 <=>; 18 =>; 0 <=; 0 <~>) % 201.12/201.06 % Maximal formula depth : 12 ( 5 avg) % 201.12/201.06 % Maximal term depth : 2 ( 1 avg) % 201.12/201.06 % Number of predicates : 17 ( 16 usr; 0 prp; 1-2 aty) % 201.12/201.06 % Number of functors : 3 ( 3 usr; 1 con; 0-1 aty) % 201.12/201.06 % Number of variables : 59 ( 49 !; 10 ?) % 201.12/201.06 % SPC : FOF_THM_RFO_SEQ % 201.12/201.06 % 201.12/201.06 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 201.12/201.06 % library, www.mizar.org % 201.12/201.06 %------------------------------------------------------------------------------ % 201.12/201.06 fof(antisymmetry_r2_hidden,axiom, % 201.12/201.06 ! [A,B] : % 201.12/201.06 ( in(A,B) % 201.12/201.06 => ~ in(B,A) ) ). % 201.12/201.06 % 201.12/201.06 fof(cc1_finset_1,axiom, % 201.12/201.06 ! [A] : % 201.12/201.06 ( empty(A) % 201.12/201.06 => finite(A) ) ). % 201.12/201.06 % 201.12/201.06 fof(cc1_finsub_1,axiom, % 201.12/201.06 ! [A] : % 201.12/201.06 ( preboolean(A) % 201.12/201.06 => ( cup_closed(A) % 201.12/201.06 & diff_closed(A) ) ) ). % 201.12/201.06 % 201.12/201.06 fof(cc2_finset_1,axiom, % 201.12/201.06 ! [A] : % 201.12/201.06 ( finite(A) % 201.12/201.06 => ! [B] : % 201.12/201.06 ( element(B,powerset(A)) % 201.12/201.06 => finite(B) ) ) ). % 201.12/201.06 % 201.12/201.06 fof(cc2_finsub_1,axiom, % 201.12/201.06 ! [A] : % 201.12/201.06 ( ( cup_closed(A) % 201.12/201.06 & diff_closed(A) ) % 201.12/201.06 => preboolean(A) ) ). % 201.12/201.06 % 201.12/201.06 fof(cc3_finsub_1,axiom, % 201.12/201.06 ! [A,B] : % 201.12/201.06 ( element(B,finite_subsets(A)) % 201.12/201.06 => finite(B) ) ). % 201.12/201.06 % 201.12/201.06 fof(d3_tarski,axiom, % 201.12/201.06 ! [A,B] : % 201.12/201.06 ( subset(A,B) % 201.12/201.06 <=> ! [C] : % 201.12/201.06 ( in(C,A) % 201.12/201.06 => in(C,B) ) ) ). % 201.12/201.06 % 201.12/201.06 fof(d5_finsub_1,axiom, % 201.12/201.06 ! [A,B] : % 201.12/201.06 ( preboolean(B) % 201.12/201.06 => ( B = finite_subsets(A) % 201.12/201.06 <=> ! [C] : % 201.12/201.06 ( in(C,B) % 201.12/201.06 <=> ( subset(C,A) % 201.12/201.06 & finite(C) ) ) ) ) ). % 201.12/201.06 % 201.12/201.06 fof(dt_k5_finsub_1,axiom, % 201.12/201.06 ! [A] : preboolean(finite_subsets(A)) ). % 201.12/201.06 % 201.12/201.06 fof(existence_m1_subset_1,axiom, % 201.12/201.06 ! [A] : % 201.12/201.06 ? [B] : element(B,A) ). % 201.12/201.06 % 201.12/201.06 fof(fc1_finsub_1,axiom, % 201.12/201.06 ! [A] : % 201.12/201.06 ( ~ empty(powerset(A)) % 201.12/201.06 & cup_closed(powerset(A)) % 201.12/201.06 & diff_closed(powerset(A)) % 201.12/201.07 & preboolean(powerset(A)) ) ). % 201.12/201.07 % 201.12/201.07 fof(fc1_subset_1,axiom, % 201.12/201.07 ! [A] : ~ empty(powerset(A)) ). % 201.12/201.07 % 201.12/201.07 fof(fc1_xboole_0,axiom, % 201.12/201.07 empty(empty_set) ). % 201.12/201.07 % 201.12/201.07 fof(fc2_finsub_1,axiom, % 201.12/201.07 ! [A] : % 201.12/201.07 ( ~ empty(finite_subsets(A)) % 201.12/201.07 & cup_closed(finite_subsets(A)) % 201.12/201.07 & diff_closed(finite_subsets(A)) % 201.12/201.07 & preboolean(finite_subsets(A)) ) ). % 201.12/201.07 % 201.12/201.07 fof(rc1_finset_1,axiom, % 201.12/201.07 ? [A] : % 201.12/201.07 ( ~ empty(A) % 201.12/201.07 & finite(A) ) ). % 201.12/201.07 % 201.12/201.07 fof(rc1_finsub_1,axiom, % 201.12/201.07 ? [A] : % 201.12/201.07 ( ~ empty(A) % 201.12/201.07 & cup_closed(A) % 201.12/201.07 & cap_closed(A) % 201.12/201.07 & diff_closed(A) % 201.12/201.07 & preboolean(A) ) ). % 201.12/201.07 % 201.12/201.07 fof(rc1_subset_1,axiom, % 201.12/201.07 ! [A] : % 201.12/201.07 ( ~ empty(A) % 201.12/201.07 => ? [B] : % 201.12/201.07 ( element(B,powerset(A)) % 201.12/201.07 & ~ empty(B) ) ) ). % 201.12/201.07 % 201.12/201.07 fof(rc1_xboole_0,axiom, % 201.12/201.07 ? [A] : empty(A) ). % 201.12/201.07 % 201.12/201.07 fof(rc2_finset_1,axiom, % 201.12/201.07 ! [A] : % 201.12/201.07 ? [B] : % 201.12/201.07 ( element(B,powerset(A)) % 201.12/201.07 & empty(B) % 201.12/201.07 & relation(B) % 201.12/201.07 & function(B) % 201.12/201.07 & one_to_one(B) % 201.12/201.07 & epsilon_transitive(B) % 201.12/201.07 & epsilon_connected(B) % 201.12/201.07 & ordinal(B) % 201.12/201.07 & natural(B) % 201.12/201.07 & finite(B) ) ). % 201.12/201.07 % 201.12/201.07 fof(rc2_subset_1,axiom, % 201.12/201.07 ! [A] : % 201.12/201.07 ? [B] : % 201.12/201.07 ( element(B,powerset(A)) % 201.12/201.07 & empty(B) ) ). % 201.12/201.07 % 201.12/201.07 fof(rc2_xboole_0,axiom, % 201.12/201.07 ? [A] : ~ empty(A) ). % 201.12/201.07 % 201.12/201.07 fof(rc3_finset_1,axiom, % 201.12/201.07 ! [A] : % 201.12/201.07 ( ~ empty(A) % 201.12/201.07 => ? [B] : % 201.12/201.07 ( element(B,powerset(A)) % 201.12/201.07 & ~ empty(B) % 201.12/201.07 & finite(B) ) ) ). % 201.12/201.07 % 201.12/201.07 fof(rc4_finset_1,axiom, % 201.12/201.07 ! [A] : % 201.12/201.07 ( ~ empty(A) % 201.12/201.07 => ? [B] : % 201.12/201.07 ( element(B,powerset(A)) % 201.12/201.07 & ~ empty(B) % 201.12/201.07 & finite(B) ) ) ). % 201.12/201.07 % 201.12/201.07 fof(reflexivity_r1_tarski,axiom, % 201.12/201.07 ! [A,B] : subset(A,A) ). % 201.12/201.07 % 201.12/201.07 fof(t1_subset,axiom, % 201.12/201.07 ! [A,B] : % 201.12/201.07 ( in(A,B) % 201.12/201.07 => element(A,B) ) ). % 201.12/201.07 % 201.12/201.07 fof(t1_xboole_1,axiom, % 201.12/201.07 ! [A,B,C] : % 201.12/201.07 ( ( subset(A,B) % 201.12/201.07 & subset(B,C) ) % 201.12/201.07 => subset(A,C) ) ). % 201.12/201.07 % 201.12/201.07 fof(t23_finsub_1,conjecture, % 201.12/201.07 ! [A,B] : % 201.12/201.07 ( subset(A,B) % 201.12/201.07 => subset(finite_subsets(A),finite_subsets(B)) ) ). % 201.12/201.07 % 201.12/201.07 fof(t2_subset,axiom, % 201.12/201.07 ! [A,B] : % 201.12/201.07 ( element(A,B) % 201.12/201.07 => ( empty(B) % 201.12/201.07 | in(A,B) ) ) ). % 201.12/201.07 % 201.12/201.07 fof(t3_subset,axiom, % 201.12/201.07 ! [A,B] : % 201.12/201.07 ( element(A,powerset(B)) % 201.12/201.07 <=> subset(A,B) ) ). % 201.12/201.07 % 201.12/201.07 fof(t4_subset,axiom, % 201.12/201.07 ! [A,B,C] : % 201.12/201.07 ( ( in(A,B) % 201.12/201.07 & element(B,powerset(C)) ) % 201.12/201.07 => element(A,C) ) ). % 201.12/201.07 % 201.12/201.07 fof(t5_subset,axiom, % 201.12/201.07 ! [A,B,C] : % 201.12/201.07 ~ ( in(A,B) % 201.12/201.07 & element(B,powerset(C)) % 201.12/201.07 & empty(C) ) ). % 201.12/201.07 % 201.12/201.07 fof(t6_boole,axiom, % 201.12/201.07 ! [A] : % 201.12/201.07 ( empty(A) % 201.12/201.07 => A = empty_set ) ). % 201.12/201.07 % 201.12/201.07 fof(t7_boole,axiom, % 201.12/201.07 ! [A,B] : % 201.12/201.07 ~ ( in(A,B) % 201.12/201.07 & empty(B) ) ). % 201.12/201.07 % 201.12/201.07 fof(t8_boole,axiom, % 201.12/201.07 ! [A,B] : % 201.12/201.07 ~ ( empty(A) % 201.12/201.07 & A != B % 201.12/201.07 & empty(B) ) ). % 201.12/201.07 % 201.12/201.07 %------------------------------------------------------------------------------ % 201.12/201.07 %------------------------------------------- % 201.12/201.07 % Proof found % 201.12/201.07 % SZS status Theorem for theBenchmark % 201.12/201.07 % SZS output start Proof % 201.12/201.08 %ClaNum:104(EqnAxiom:34) % 201.12/201.08 %VarNum:173(SingletonVarNum:84) % 201.12/201.08 %MaxLitNum:5 % 201.12/201.08 %MaxfuncDepth:1 % 201.12/201.08 %SharedTerms:21 % 201.12/201.08 %goalClause: 59 70 % 201.12/201.08 %singleGoalClaCount:2 % 201.12/201.08 [35]P1(a1) % 201.12/201.08 [36]P1(a2) % 201.12/201.08 [37]P6(a3) % 201.12/201.08 [38]P9(a12) % 201.12/201.08 [39]P2(a12) % 201.12/201.08 [40]P4(a12) % 201.12/201.08 [41]P3(a12) % 201.12/201.08 [59]P16(a4,a8) % 201.12/201.08 [64]~P1(a3) % 201.12/201.08 [65]~P1(a12) % 201.12/201.08 [66]~P1(a5) % 201.12/201.08 [70]~P16(f17(a4),f17(a8)) % 201.12/201.08 [60]P16(x601,x601) % 201.12/201.08 [42]P1(f14(x421)) % 201.12/201.08 [43]P1(f15(x431)) % 201.12/201.08 [44]P6(f14(x441)) % 201.12/201.08 [45]P9(f16(x451)) % 201.12/201.08 [47]P9(f17(x471)) % 201.12/201.08 [48]P2(f16(x481)) % 201.12/201.08 [49]P2(f17(x491)) % 201.12/201.08 [50]P4(f16(x501)) % 201.12/201.08 [51]P4(f17(x511)) % 201.12/201.08 [52]P15(f14(x521)) % 201.12/201.08 [53]P10(f14(x531)) % 201.12/201.08 [54]P11(f14(x541)) % 201.12/201.08 [55]P7(f14(x551)) % 201.12/201.08 [56]P8(f14(x561)) % 201.12/201.08 [57]P14(f14(x571)) % 201.12/201.08 [58]P12(f14(x581)) % 201.12/201.08 [61]P5(f9(x611),x611) % 201.12/201.08 [62]P5(f14(x621),f16(x621)) % 201.12/201.08 [63]P5(f15(x631),f16(x631)) % 201.12/201.08 [68]~P1(f16(x681)) % 201.12/201.08 [69]~P1(f17(x691)) % 201.12/201.08 [71]~P1(x711)+E(x711,a1) % 201.12/201.08 [72]~P1(x721)+P6(x721) % 201.12/201.08 [73]~P9(x731)+P2(x731) % 201.12/201.08 [74]~P9(x741)+P4(x741) % 201.12/201.08 [75]P1(x751)+P6(f6(x751)) % 201.12/201.08 [76]P1(x761)+P6(f7(x761)) % 201.12/201.08 [79]P1(x791)+~P1(f13(x791)) % 201.12/201.08 [80]P1(x801)+~P1(f6(x801)) % 201.12/201.08 [81]P1(x811)+~P1(f7(x811)) % 201.12/201.08 [83]P1(x831)+P5(f13(x831),f16(x831)) % 201.12/201.08 [84]P1(x841)+P5(f6(x841),f16(x841)) % 201.12/201.08 [85]P1(x851)+P5(f7(x851),f16(x851)) % 201.12/201.08 [82]~P1(x821)+~P13(x822,x821) % 201.12/201.08 [87]~P13(x871,x872)+P5(x871,x872) % 201.12/201.08 [92]~P13(x922,x921)+~P13(x921,x922) % 201.12/201.08 [86]P6(x861)+~P5(x861,f17(x862)) % 201.12/201.08 [90]~P16(x901,x902)+P5(x901,f16(x902)) % 201.12/201.08 [93]P16(x931,x932)+~P5(x931,f16(x932)) % 201.12/201.08 [95]P16(x951,x952)+P13(f10(x951,x952),x951) % 201.12/201.08 [101]P16(x1011,x1012)+~P13(f10(x1011,x1012),x1012) % 201.12/201.08 [78]~P2(x781)+~P4(x781)+P9(x781) % 201.12/201.08 [77]~P1(x772)+~P1(x771)+E(x771,x772) % 201.12/201.08 [88]~P5(x882,x881)+P1(x881)+P13(x882,x881) % 201.12/201.08 [91]P6(x911)+~P6(x912)+~P5(x911,f16(x912)) % 201.12/201.08 [96]~P16(x963,x962)+P13(x961,x962)+~P13(x961,x963) % 201.12/201.08 [97]~P16(x971,x973)+P16(x971,x972)+~P16(x973,x972) % 201.12/201.08 [99]~P1(x991)+~P13(x992,x993)+~P5(x993,f16(x991)) % 201.12/201.08 [100]P5(x1001,x1002)+~P13(x1001,x1003)+~P5(x1003,f16(x1002)) % 201.12/201.08 [102]~P9(x1021)+P13(f11(x1022,x1021),x1021)+E(x1021,f17(x1022))+P6(f11(x1022,x1021)) % 201.12/201.08 [103]~P9(x1031)+P13(f11(x1032,x1031),x1031)+P16(f11(x1032,x1031),x1032)+E(x1031,f17(x1032)) % 201.12/201.08 [89]~P9(x892)+~P13(x891,x892)+P6(x891)+~E(x892,f17(x893)) % 201.12/201.08 [94]~P9(x943)+~P13(x941,x943)+P16(x941,x942)+~E(x943,f17(x942)) % 201.12/201.08 [104]~P9(x1041)+~P13(f11(x1042,x1041),x1041)+~P16(f11(x1042,x1041),x1042)+E(x1041,f17(x1042))+~P6(f11(x1042,x1041)) % 201.12/201.08 [98]~P6(x981)+~P9(x982)+~P16(x981,x983)+P13(x981,x982)+~E(x982,f17(x983)) % 201.12/201.08 %EqnAxiom % 201.12/201.08 [1]E(x11,x11) % 201.12/201.08 [2]E(x22,x21)+~E(x21,x22) % 201.12/201.08 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 201.12/201.08 [4]~E(x41,x42)+E(f14(x41),f14(x42)) % 201.12/201.08 [5]~E(x51,x52)+E(f15(x51),f15(x52)) % 201.12/201.08 [6]~E(x61,x62)+E(f11(x61,x63),f11(x62,x63)) % 201.12/201.08 [7]~E(x71,x72)+E(f11(x73,x71),f11(x73,x72)) % 201.12/201.08 [8]~E(x81,x82)+E(f16(x81),f16(x82)) % 201.12/201.08 [9]~E(x91,x92)+E(f17(x91),f17(x92)) % 201.12/201.08 [10]~E(x101,x102)+E(f7(x101),f7(x102)) % 201.12/201.08 [11]~E(x111,x112)+E(f6(x111),f6(x112)) % 201.12/201.08 [12]~E(x121,x122)+E(f13(x121),f13(x122)) % 201.12/201.08 [13]~E(x131,x132)+E(f9(x131),f9(x132)) % 201.12/201.08 [14]~E(x141,x142)+E(f10(x141,x143),f10(x142,x143)) % 201.12/201.08 [15]~E(x151,x152)+E(f10(x153,x151),f10(x153,x152)) % 201.12/201.08 [16]~P1(x161)+P1(x162)+~E(x161,x162) % 201.12/201.08 [17]P16(x172,x173)+~E(x171,x172)+~P16(x171,x173) % 201.12/201.08 [18]P16(x183,x182)+~E(x181,x182)+~P16(x183,x181) % 201.12/201.08 [19]~P6(x191)+P6(x192)+~E(x191,x192) % 201.12/201.08 [20]~P9(x201)+P9(x202)+~E(x201,x202) % 201.12/201.08 [21]~P2(x211)+P2(x212)+~E(x211,x212) % 201.12/201.08 [22]~P4(x221)+P4(x222)+~E(x221,x222) % 201.12/201.08 [23]~P3(x231)+P3(x232)+~E(x231,x232) % 201.12/201.08 [24]P13(x242,x243)+~E(x241,x242)+~P13(x241,x243) % 201.12/201.08 [25]P13(x253,x252)+~E(x251,x252)+~P13(x253,x251) % 201.12/201.08 [26]P5(x262,x263)+~E(x261,x262)+~P5(x261,x263) % 201.12/201.08 [27]P5(x273,x272)+~E(x271,x272)+~P5(x273,x271) % 201.12/201.08 [28]~P12(x281)+P12(x282)+~E(x281,x282) % 201.12/201.08 [29]~P14(x291)+P14(x292)+~E(x291,x292) % 201.12/201.08 [30]~P8(x301)+P8(x302)+~E(x301,x302) % 201.12/201.08 [31]~P7(x311)+P7(x312)+~E(x311,x312) % 201.12/201.08 [32]~P11(x321)+P11(x322)+~E(x321,x322) % 201.12/201.08 [33]~P10(x331)+P10(x332)+~E(x331,x332) % 201.12/201.08 [34]~P15(x341)+P15(x342)+~E(x341,x342) % 201.12/201.08 % 201.12/201.08 %------------------------------------------- % 201.12/201.11 cnf(105,plain, % 201.12/201.11 (P6(x1051)+~P9(f17(x1052))+~P13(x1051,f17(x1052))), % 201.12/201.11 inference(equality_inference,[],[89])). % 201.12/201.11 cnf(106,plain, % 201.12/201.11 (~P9(f17(x1061))+~P13(x1062,f17(x1061))+P16(x1062,x1061)), % 201.12/201.11 inference(equality_inference,[],[94])). % 201.12/201.11 cnf(107,plain, % 201.12/201.11 (P13(x1071,f17(x1072))+~P6(x1071)+~P16(x1071,x1072)+~P9(f17(x1072))), % 201.12/201.11 inference(equality_inference,[],[98])). % 201.12/201.11 cnf(108,plain, % 201.12/201.11 (P16(f9(f16(x1081)),x1081)), % 201.12/201.11 inference(scs_inference,[],[61,93])). % 201.12/201.11 cnf(109,plain, % 201.12/201.11 (P5(f9(x1091),x1091)), % 201.12/201.11 inference(rename_variables,[],[61])). % 201.12/201.11 cnf(111,plain, % 201.12/201.11 (~P13(x1111,a1)), % 201.12/201.11 inference(scs_inference,[],[61,35,93,82])). % 201.12/201.11 cnf(113,plain, % 201.12/201.11 (P6(f9(f17(x1131)))), % 201.12/201.11 inference(scs_inference,[],[61,109,35,93,82,86])). % 201.12/201.11 cnf(114,plain, % 201.12/201.11 (P5(f9(x1141),x1141)), % 201.12/201.11 inference(rename_variables,[],[61])). % 201.12/201.11 cnf(116,plain, % 201.12/201.11 (~P13(f17(a4),f17(f17(a8)))), % 201.12/201.11 inference(scs_inference,[],[70,61,109,47,35,93,82,86,106])). % 201.12/201.11 cnf(117,plain, % 201.12/201.11 (P9(f17(x1171))), % 201.12/201.11 inference(rename_variables,[],[47])). % 201.12/201.11 cnf(119,plain, % 201.12/201.11 (~E(f17(a8),f17(a4))), % 201.12/201.11 inference(scs_inference,[],[70,60,61,109,47,35,93,82,86,106,17])). % 201.12/201.11 cnf(120,plain, % 201.12/201.11 (P16(x1201,x1201)), % 201.12/201.11 inference(rename_variables,[],[60])). % 201.12/201.11 cnf(121,plain, % 201.12/201.11 (~E(f17(a4),f17(a8))), % 201.12/201.11 inference(scs_inference,[],[70,60,120,61,109,47,35,93,82,86,106,17,18])). % 201.12/201.11 cnf(122,plain, % 201.12/201.11 (P16(x1221,x1221)), % 201.12/201.11 inference(rename_variables,[],[60])). % 201.12/201.11 cnf(123,plain, % 201.12/201.11 (P13(f9(a3),a3)), % 201.12/201.11 inference(scs_inference,[],[70,60,120,61,109,114,47,35,64,93,82,86,106,17,18,88])). % 201.12/201.11 cnf(124,plain, % 201.12/201.11 (P5(f9(x1241),x1241)), % 201.12/201.11 inference(rename_variables,[],[61])). % 201.12/201.11 cnf(126,plain, % 201.12/201.11 (P6(f9(f16(a3)))), % 201.12/201.11 inference(scs_inference,[],[70,60,120,61,109,114,124,37,47,35,64,93,82,86,106,17,18,88,91])). % 201.12/201.11 cnf(127,plain, % 201.12/201.11 (P5(f9(x1271),x1271)), % 201.12/201.11 inference(rename_variables,[],[61])). % 201.12/201.11 cnf(129,plain, % 201.12/201.11 (~P13(x1291,f9(f16(a1)))), % 201.12/201.11 inference(scs_inference,[],[70,60,120,61,109,114,124,127,37,47,35,64,93,82,86,106,17,18,88,91,99])). % 201.12/201.11 cnf(130,plain, % 201.12/201.11 (P5(f9(x1301),x1301)), % 201.12/201.11 inference(rename_variables,[],[61])). % 201.12/201.11 cnf(132,plain, % 201.12/201.11 (~E(a3,a1)), % 201.12/201.11 inference(scs_inference,[],[70,60,120,61,109,114,124,127,37,47,35,64,93,82,86,106,17,18,88,91,99,25])). % 201.12/201.11 cnf(133,plain, % 201.12/201.11 (P13(a3,f17(a3))), % 201.12/201.11 inference(scs_inference,[],[70,60,120,122,61,109,114,124,127,37,47,117,35,64,93,82,86,106,17,18,88,91,99,25,107])). % 201.12/201.11 cnf(137,plain, % 201.12/201.11 (P16(f9(f16(a1)),x1371)), % 201.12/201.11 inference(scs_inference,[],[70,60,120,122,61,109,114,124,127,37,47,117,35,64,93,82,86,106,17,18,88,91,99,25,107,95])). % 201.12/201.11 cnf(139,plain, % 201.12/201.11 (~P13(a3,f9(a3))), % 201.12/201.11 inference(scs_inference,[],[70,60,120,122,61,109,114,124,127,37,47,117,35,64,93,82,86,106,17,18,88,91,99,25,107,95,92])). % 201.12/201.11 cnf(144,plain, % 201.12/201.11 (P5(x1441,x1442)+~P13(x1441,f9(f16(x1442)))), % 201.12/201.11 inference(scs_inference,[],[70,60,120,122,61,109,114,124,127,130,37,47,117,35,64,93,82,86,106,17,18,88,91,99,25,107,95,92,9,77,100])). % 201.12/201.11 cnf(145,plain, % 201.12/201.11 (P5(f9(x1451),x1451)), % 201.12/201.11 inference(rename_variables,[],[61])). % 201.12/201.11 cnf(148,plain, % 201.12/201.11 (P5(x1481,x1482)+~E(f9(x1482),x1481)), % 201.12/201.11 inference(scs_inference,[],[70,60,120,122,61,109,114,124,127,130,145,37,47,117,35,64,93,82,86,106,17,18,88,91,99,25,107,95,92,9,77,100,24,26])). % 201.12/201.11 cnf(149,plain, % 201.12/201.11 (P5(f9(x1491),x1492)+~E(x1491,x1492)), % 201.12/201.11 inference(scs_inference,[],[70,60,120,122,61,109,114,124,127,130,145,37,47,117,35,64,93,82,86,106,17,18,88,91,99,25,107,95,92,9,77,100,24,26,27])). % 201.12/201.11 cnf(156,plain, % 201.12/201.11 (P16(f14(x1561),x1561)), % 201.12/201.11 inference(scs_inference,[],[62,93])). % 201.12/201.11 cnf(158,plain, % 201.12/201.11 (P16(a1,x1581)), % 201.12/201.11 inference(scs_inference,[],[111,62,93,95])). % 201.12/201.11 cnf(161,plain, % 201.12/201.11 (~P13(x1611,a2)), % 201.12/201.11 inference(scs_inference,[],[111,62,36,93,95,82])). % 201.12/201.11 cnf(163,plain, % 201.12/201.11 (~P13(f17(a3),a3)), % 201.12/201.11 inference(scs_inference,[],[133,111,62,36,93,95,82,92])). % 201.12/201.11 cnf(166,plain, % 201.12/201.11 (P16(f9(f16(a4)),a8)), % 201.12/201.11 inference(scs_inference,[],[59,108,121,133,111,62,36,93,95,82,92,9,97])). % 201.12/201.11 cnf(167,plain, % 201.12/201.11 (P16(f9(f16(x1671)),x1671)), % 201.12/201.11 inference(rename_variables,[],[108])). % 201.12/201.11 cnf(169,plain, % 201.12/201.11 (P13(f9(a12),a12)), % 201.12/201.11 inference(scs_inference,[],[59,108,121,133,111,62,61,36,65,93,95,82,92,9,97,88])). % 201.12/201.11 cnf(172,plain, % 201.12/201.11 (~P13(x1721,f14(a2))), % 201.12/201.11 inference(scs_inference,[],[59,108,121,133,111,62,61,36,65,93,95,82,92,9,97,88,99])). % 201.12/201.11 cnf(175,plain, % 201.12/201.11 (~E(f17(a3),f9(f16(a1)))), % 201.12/201.11 inference(scs_inference,[],[59,108,121,133,129,111,62,61,36,65,93,95,82,92,9,97,88,99,25])). % 201.12/201.11 cnf(178,plain, % 201.12/201.11 (~E(f9(f16(a1)),f17(a4))), % 201.12/201.11 inference(scs_inference,[],[59,70,108,137,121,133,129,123,111,62,61,36,65,93,95,82,92,9,97,88,99,25,24,17])). % 201.12/201.11 cnf(180,plain, % 201.12/201.11 (P13(f9(f16(a3)),f17(a3))), % 201.12/201.11 inference(scs_inference,[],[59,70,108,167,137,121,133,129,126,123,111,62,61,47,36,65,93,95,82,92,9,97,88,99,25,24,17,107])). % 201.12/201.11 cnf(191,plain, % 201.12/201.11 (P16(f15(x1911),x1911)), % 201.12/201.11 inference(scs_inference,[],[63,93])). % 201.12/201.11 cnf(194,plain, % 201.12/201.11 (~P13(x1941,f14(a2))), % 201.12/201.11 inference(rename_variables,[],[172])). % 201.12/201.11 cnf(198,plain, % 201.12/201.11 (~P13(x1981,f14(x1982))), % 201.12/201.11 inference(scs_inference,[],[180,172,63,42,93,95,92,82])). % 201.12/201.11 cnf(200,plain, % 201.12/201.11 (P13(f9(a5),a5)), % 201.12/201.11 inference(scs_inference,[],[180,172,63,61,66,42,93,95,92,82,88])). % 201.12/201.11 cnf(210,plain, % 201.12/201.11 (P13(f14(x2101),f17(f14(x2101)))), % 201.12/201.11 inference(scs_inference,[],[70,60,156,180,172,194,63,44,61,47,66,42,93,95,92,82,88,99,25,17,107])). % 201.12/201.11 cnf(227,plain, % 201.12/201.11 (P16(f14(x2271),x2272)), % 201.12/201.11 inference(scs_inference,[],[198,95])). % 201.12/201.11 cnf(228,plain, % 201.12/201.11 (~P13(x2281,f14(x2282))), % 201.12/201.11 inference(rename_variables,[],[198])). % 201.12/201.11 cnf(230,plain, % 201.12/201.11 (~P13(x2301,f15(x2302))), % 201.12/201.11 inference(scs_inference,[],[198,43,95,82])). % 201.12/201.11 cnf(232,plain, % 201.12/201.11 (~P13(a12,f9(a12))), % 201.12/201.11 inference(scs_inference,[],[198,169,43,95,82,92])). % 201.12/201.11 cnf(240,plain, % 201.12/201.11 (P16(f15(x2401),x2401)), % 201.12/201.11 inference(rename_variables,[],[191])). % 201.12/201.11 cnf(243,plain, % 201.12/201.11 (P5(x2431,f16(x2432))+~E(f14(x2432),x2431)), % 201.12/201.11 inference(scs_inference,[],[70,191,240,210,198,228,169,62,43,68,95,82,92,88,25,17,24,18,26])). % 201.12/201.11 cnf(251,plain, % 201.12/201.11 (P16(f15(x2511),x2512)), % 201.12/201.11 inference(scs_inference,[],[230,95])). % 201.12/201.11 cnf(254,plain, % 201.12/201.11 (~P13(a5,f9(a5))), % 201.12/201.11 inference(scs_inference,[],[230,200,95,92])). % 201.12/201.11 cnf(259,plain, % 201.12/201.11 (~P5(f17(a4),f17(f17(a8)))), % 201.12/201.11 inference(scs_inference,[],[116,63,44,230,200,69,95,92,91,88])). % 201.12/201.11 cnf(274,plain, % 201.12/201.11 (P16(a2,x2741)), % 201.12/201.11 inference(scs_inference,[],[161,95])). % 201.12/201.11 cnf(275,plain, % 201.12/201.11 (~P13(x2751,a2)), % 201.12/201.11 inference(rename_variables,[],[161])). % 201.12/201.11 cnf(277,plain, % 201.12/201.11 (~P5(f17(a3),a3)), % 201.12/201.11 inference(scs_inference,[],[163,161,64,95,88])). % 201.12/201.11 cnf(286,plain, % 201.12/201.11 (P13(f15(a3),f17(f15(a3)))), % 201.12/201.11 inference(scs_inference,[],[70,60,210,251,37,63,163,161,275,47,64,95,88,91,25,17,107])). % 201.12/201.11 cnf(300,plain, % 201.12/201.11 (P13(f9(f16(x3001)),f16(x3001))), % 201.12/201.11 inference(scs_inference,[],[61,68,88])). % 201.12/201.11 cnf(304,plain, % 201.12/201.11 (~E(a1,f17(a4))), % 201.12/201.11 inference(scs_inference,[],[70,133,158,61,139,68,88,25,17])). % 201.12/201.11 cnf(306,plain, % 201.12/201.11 (~P13(f16(x3061),f9(f16(x3061)))), % 201.12/201.11 inference(scs_inference,[],[70,133,158,61,139,68,88,25,17,92])). % 201.12/201.11 cnf(323,plain, % 201.12/201.11 (~P13(a12,f10(x3231,a12))+~E(f9(a12),f10(x3231,a12))), % 201.12/201.11 inference(scs_inference,[],[70,180,274,230,169,25,17,24,101,92])). % 201.12/201.11 cnf(343,plain, % 201.12/201.11 (P13(x3431,f16(x3432))+~E(f9(f16(x3432)),x3431)), % 201.12/201.11 inference(scs_inference,[],[133,161,300,25,24])). % 201.12/201.11 cnf(349,plain, % 201.12/201.11 (P16(f9(f16(x3491)),x3492)+~E(x3491,x3492)), % 201.12/201.11 inference(scs_inference,[],[180,108,198,25,18])). % 201.12/201.11 cnf(373,plain, % 201.12/201.11 (~P9(a1)+P16(f11(a4,a1),a4)), % 201.12/201.11 inference(scs_inference,[],[286,304,161,111,25,103])). % 201.12/201.12 cnf(433,plain, % 201.12/201.12 (~E(a12,a1)), % 201.12/201.12 inference(scs_inference,[],[169,111,25])). % 201.12/201.12 cnf(435,plain, % 201.12/201.12 (P13(f14(x4351),f17(x4352))), % 201.12/201.12 inference(scs_inference,[],[227,169,44,111,47,25,107])). % 201.12/201.12 cnf(440,plain, % 201.12/201.12 (~E(f17(x4401),a2)), % 201.12/201.12 inference(scs_inference,[],[435,161,25])). % 201.12/201.12 cnf(468,plain, % 201.12/201.12 (~E(a3,f15(x4681))), % 201.12/201.12 inference(scs_inference,[],[123,230,25])). % 201.12/201.12 cnf(472,plain, % 201.12/201.12 (~E(a5,a1)), % 201.12/201.12 inference(scs_inference,[],[200,111,25])). % 201.12/201.12 cnf(524,plain, % 201.12/201.12 (P6(f7(a3))), % 201.12/201.12 inference(scs_inference,[],[132,71,76])). % 201.12/201.12 cnf(525,plain, % 201.12/201.12 (P13(f7(a3),f17(f7(a3)))), % 201.12/201.12 inference(scs_inference,[],[60,524,47,107])). % 201.12/201.12 cnf(529,plain, % 201.12/201.12 (~P13(f17(f7(a3)),f7(a3))), % 201.12/201.12 inference(scs_inference,[],[60,524,47,107,92])). % 201.12/201.12 cnf(549,plain, % 201.12/201.12 (~P1(f13(f6(a12)))), % 201.12/201.12 inference(scs_inference,[],[65,79,80])). % 201.12/201.12 cnf(565,plain, % 201.12/201.12 (~P1(f7(f17(a3)))), % 201.12/201.12 inference(scs_inference,[],[180,81,82])). % 201.12/201.12 cnf(597,plain, % 201.12/201.12 (E(f7(x5971),f7(x5972))+~E(x5972,x5971)), % 201.12/201.12 inference(scs_inference,[],[2,10])). % 201.12/201.12 cnf(614,plain, % 201.12/201.12 (P5(f10(f17(a4),f17(a8)),f17(a4))), % 201.12/201.12 inference(scs_inference,[],[70,87,95])). % 201.12/201.12 cnf(615,plain, % 201.12/201.12 (P6(f10(f17(a4),f17(a8)))), % 201.12/201.12 inference(scs_inference,[],[614,86])). % 201.12/201.12 cnf(642,plain, % 201.12/201.12 (P5(f13(a3),f16(a3))), % 201.12/201.12 inference(scs_inference,[],[132,83,71])). % 201.12/201.12 cnf(643,plain, % 201.12/201.12 (P16(f13(a3),a3)), % 201.12/201.12 inference(scs_inference,[],[642,93])). % 201.12/201.12 cnf(645,plain, % 201.12/201.12 (~P13(f17(a3),f13(a3))), % 201.12/201.12 inference(scs_inference,[],[277,642,93,100])). % 201.12/201.12 cnf(647,plain, % 201.12/201.12 (P6(f13(a3))), % 201.12/201.12 inference(scs_inference,[],[37,277,642,93,100,91])). % 201.12/201.12 cnf(649,plain, % 201.12/201.12 (P13(f13(a3),f17(f13(a3)))), % 201.12/201.12 inference(scs_inference,[],[60,37,277,642,47,93,100,91,107])). % 201.12/201.12 cnf(653,plain, % 201.12/201.12 (~P13(f17(f13(a3)),f13(a3))), % 201.12/201.12 inference(scs_inference,[],[60,37,277,642,47,93,100,91,107,92])). % 201.12/201.12 cnf(674,plain, % 201.12/201.12 (P13(f13(a3),f17(a3))), % 201.12/201.12 inference(scs_inference,[],[643,647,47,107])). % 201.12/201.12 cnf(723,plain, % 201.12/201.12 (P5(f15(x7231),f16(x7232))), % 201.12/201.12 inference(scs_inference,[],[230,90,95])). % 201.12/201.12 cnf(724,plain, % 201.12/201.12 (P13(f15(x7241),f16(x7242))), % 201.12/201.12 inference(scs_inference,[],[723,68,88])). % 201.12/201.12 cnf(730,plain, % 201.12/201.12 (P13(f15(x7301),f17(x7302))), % 201.12/201.12 inference(scs_inference,[],[251,723,37,47,68,88,91,107])). % 201.12/201.12 cnf(742,plain, % 201.12/201.12 (P13(x7421,f16(x7422))+~E(f15(x7423),x7421)), % 201.12/201.12 inference(scs_inference,[],[724,24])). % 201.12/201.12 cnf(747,plain, % 201.12/201.12 (P16(a4,f16(x7471))+~E(f15(x7472),f10(a8,f16(x7471)))), % 201.12/201.12 inference(scs_inference,[],[59,642,724,24,101,92,99,97])). % 201.12/201.12 cnf(754,plain, % 201.12/201.12 (P5(x7541,f16(x7542))+~E(f15(x7543),x7541)), % 201.12/201.12 inference(scs_inference,[],[723,27,26])). % 201.12/201.12 cnf(771,plain, % 201.12/201.12 (P5(f11(a4,a1),f16(a4))+~P9(a1)), % 201.12/201.12 inference(scs_inference,[],[373,90])). % 201.12/201.12 cnf(820,plain, % 201.12/201.12 (~E(x8201,x8202)+E(f16(f11(x8201,x8203)),f16(f11(x8202,x8203)))), % 201.12/201.12 inference(scs_inference,[],[8,6])). % 201.12/201.12 cnf(837,plain, % 201.12/201.12 (~E(x8371,x8372)+E(f6(f11(x8373,x8371)),f6(f11(x8373,x8372)))), % 201.12/201.12 inference(scs_inference,[],[11,7])). % 201.12/201.12 cnf(854,plain, % 201.12/201.12 (~E(x8541,x8542)+E(f13(f17(x8541)),f13(f17(x8542)))), % 201.12/201.12 inference(scs_inference,[],[12,9])). % 201.12/201.12 cnf(871,plain, % 201.12/201.12 (~E(x8711,x8712)+E(f9(f10(x8711,x8713)),f9(f10(x8712,x8713)))), % 201.12/201.12 inference(scs_inference,[],[13,14])). % 201.12/201.12 cnf(894,plain, % 201.12/201.12 (~P13(x8941,f9(f16(a2)))), % 201.12/201.12 inference(scs_inference,[],[36,61,99])). % 201.12/201.12 cnf(897,plain, % 201.12/201.12 (P16(f9(f16(a2)),x8971)), % 201.12/201.12 inference(scs_inference,[],[36,61,99,95])). % 201.12/201.12 cnf(899,plain, % 201.12/201.12 (~E(f9(f16(a2)),f17(a4))), % 201.12/201.12 inference(scs_inference,[],[36,70,61,99,95,17])). % 201.12/201.12 cnf(943,plain, % 201.12/201.12 (P13(f11(a4,a1),f16(a4))+~P9(a1)), % 201.12/201.12 inference(scs_inference,[],[68,771,88])). % 201.12/201.12 cnf(944,plain, % 201.12/201.12 (P13(f10(f17(a4),f17(a8)),f17(a4))), % 201.12/201.12 inference(scs_inference,[],[614,69,88])). % 201.12/201.12 cnf(1015,plain, % 201.12/201.12 (~P5(f16(a4),f16(a2))+~P9(a1)), % 201.12/201.12 inference(scs_inference,[],[36,943,99])). % 201.12/201.12 cnf(1028,plain, % 201.12/201.12 (P13(f9(f17(x10281)),f17(x10281))), % 201.12/201.12 inference(scs_inference,[],[61,69,88])). % 201.12/201.12 cnf(1031,plain, % 201.12/201.12 (~P13(f17(x10311),f9(f17(x10311)))), % 201.12/201.12 inference(scs_inference,[],[61,69,88,92])). % 201.12/201.12 cnf(1036,plain, % 201.12/201.12 (~E(f9(f16(a2)),f16(a4))+~P9(a1)), % 201.12/201.12 inference(scs_inference,[],[1015,148])). % 201.12/201.12 cnf(1084,plain, % 201.12/201.12 (~E(f16(a4),f9(f16(a2)))+~P9(a1)), % 201.12/201.12 inference(scs_inference,[],[1036,2])). % 201.12/201.12 cnf(1100,plain, % 201.12/201.12 (~E(x11001,f9(f16(a2)))+~E(f16(a4),x11001)+~P9(a1)), % 201.12/201.12 inference(scs_inference,[],[1084,3])). % 201.12/201.12 cnf(1356,plain, % 201.12/201.12 (E(f10(x13561,f14(x13562)),f10(x13561,a1))), % 201.12/201.12 inference(scs_inference,[],[42,15,71])). % 201.12/201.12 cnf(1357,plain, % 201.12/201.12 (E(f10(x13571,a1),f10(x13571,f14(x13572)))), % 201.12/201.12 inference(scs_inference,[],[1356,2])). % 201.12/201.12 cnf(1359,plain, % 201.12/201.12 (~P6(f10(x13591,f14(x13592)))+P6(f10(x13591,a1))), % 201.12/201.12 inference(scs_inference,[],[1356,2,16,19])). % 201.12/201.12 cnf(1375,plain, % 201.12/201.12 (~P1(f10(x13751,a1))+P1(f10(x13751,f14(x13752)))), % 201.12/201.12 inference(scs_inference,[],[1357,1356,34,21,32,28,23,16])). % 201.12/201.12 cnf(1380,plain, % 201.12/201.12 (~P6(f10(x13801,a1))+P6(f10(x13801,f14(x13802)))), % 201.12/201.12 inference(scs_inference,[],[1357,1356,34,29,20,31,19])). % 201.12/201.12 cnf(1430,plain, % 201.12/201.12 (~P1(f10(x14301,f14(x14302)))+P6(f10(x14301,a1))), % 201.12/201.12 inference(scs_inference,[],[1359,72])). % 201.12/201.12 cnf(2118,plain, % 201.12/201.12 (~E(f10(x21181,a12),f9(a12))+~P13(a12,f10(x21181,a12))), % 201.12/201.12 inference(scs_inference,[],[323,2])). % 201.12/201.12 cnf(2182,plain, % 201.12/201.12 (~E(f10(a8,f16(x21821)),f15(x21822))+P16(a4,f16(x21821))), % 201.12/201.12 inference(scs_inference,[],[747,2])). % 201.12/201.12 cnf(2293,plain, % 201.12/201.12 (~E(x22931,f9(a12))+~E(f10(x22932,a12),x22931)+~P13(a12,f10(x22932,a12))), % 201.12/201.12 inference(scs_inference,[],[2118,3])). % 201.12/201.12 cnf(2341,plain, % 201.12/201.12 (~E(x23411,f15(x23412))+~E(f10(a8,f16(x23413)),x23411)+P16(a4,f16(x23413))), % 201.12/201.12 inference(scs_inference,[],[2182,3])). % 201.12/201.12 cnf(2569,plain, % 201.12/201.12 (~P16(f17(f7(a3)),f15(x25691))), % 201.12/201.12 inference(scs_inference,[],[525,230,96])). % 201.12/201.12 cnf(2613,plain, % 201.12/201.12 (~P16(f17(f13(a3)),f15(x26131))), % 201.12/201.12 inference(scs_inference,[],[649,230,96])). % 201.12/201.12 cnf(2622,plain, % 201.12/201.12 (~P16(f17(x26221),a1)), % 201.12/201.12 inference(scs_inference,[],[435,111,96])). % 201.12/201.12 cnf(2625,plain, % 201.12/201.12 (~P13(f17(x26251),f17(a1))), % 201.12/201.12 inference(scs_inference,[],[435,111,47,96,106])). % 201.12/201.12 cnf(2629,plain, % 201.12/201.12 (~P16(f16(x26291),a1)), % 201.12/201.12 inference(scs_inference,[],[724,111,96])). % 201.12/201.12 cnf(2663,plain, % 201.12/201.12 (~P16(f17(x26631),a2)), % 201.12/201.12 inference(scs_inference,[],[435,161,96])). % 201.12/201.12 cnf(2666,plain, % 201.12/201.12 (~P13(f17(x26661),f17(a2))), % 201.12/201.12 inference(scs_inference,[],[435,161,47,96,106])). % 201.12/201.12 cnf(2670,plain, % 201.12/201.12 (~P16(f16(x26701),a2)), % 201.12/201.12 inference(scs_inference,[],[724,161,96])). % 201.12/201.12 cnf(2675,plain, % 201.12/201.12 (~P13(f16(x26751),f17(a2))), % 201.12/201.12 inference(scs_inference,[],[730,2666,724,161,47,96,24,106])). % 201.12/201.12 cnf(2683,plain, % 201.12/201.12 (~P16(a12,a1)), % 201.12/201.12 inference(scs_inference,[],[169,111,96])). % 201.12/201.12 cnf(2686,plain, % 201.12/201.12 (~P13(a12,f17(a1))), % 201.12/201.12 inference(scs_inference,[],[169,111,47,96,106])). % 201.12/201.12 cnf(2690,plain, % 201.12/201.12 (~P16(a5,a1)), % 201.12/201.12 inference(scs_inference,[],[200,111,96])). % 201.12/201.12 cnf(2693,plain, % 201.12/201.12 (~P13(a5,f17(a1))), % 201.12/201.12 inference(scs_inference,[],[200,111,47,96,106])). % 201.12/201.12 cnf(2698,plain, % 201.12/201.12 (~P16(a3,a1)), % 201.12/201.12 inference(scs_inference,[],[123,111,96])). % 201.12/201.12 cnf(2701,plain, % 201.12/201.12 (~P13(a3,f17(a1))), % 201.12/201.12 inference(scs_inference,[],[123,111,47,96,106])). % 201.12/201.12 cnf(2705,plain, % 201.12/201.12 (~E(f17(a3),f17(a1))), % 201.12/201.12 inference(scs_inference,[],[133,2701,25])). % 201.12/201.12 cnf(2706,plain, % 201.12/201.12 (~P16(f17(a3),f17(a1))), % 201.12/201.12 inference(scs_inference,[],[133,2701,25,96])). % 201.12/201.12 cnf(3296,plain, % 201.12/201.12 (~E(x32961,f16(a2))+~E(f16(a4),f9(x32961))+~P9(a1)), % 201.12/201.12 inference(scs_inference,[],[1100,13])). % 201.12/201.12 cnf(3392,plain, % 201.12/201.12 (~E(f9(x33921),f16(a4))+~E(x33921,f16(a2))+~P9(a1)), % 201.12/201.12 inference(scs_inference,[],[3296,2])). % 201.12/201.12 cnf(3424,plain, % 201.12/201.12 (~E(x34241,a2)+~E(f9(f16(x34241)),f16(a4))+~P9(a1)), % 201.12/201.12 inference(scs_inference,[],[3392,8])). % 201.12/201.12 cnf(4152,plain, % 201.12/201.12 (~E(x41521,f10(a8,f16(x41522)))+~E(x41521,f15(x41523))+P16(a4,f16(x41522))), % 201.12/201.12 inference(scs_inference,[],[2341,2])). % 201.12/201.12 cnf(4207,plain, % 201.12/201.12 (~P16(f17(a3),f14(x42071))), % 201.12/201.12 inference(scs_inference,[],[180,198,96])). % 201.12/201.12 cnf(4214,plain, % 201.12/201.12 (~P16(f17(a3),f9(f16(a2)))), % 201.12/201.12 inference(scs_inference,[],[133,4207,894,47,106,96])). % 201.12/201.12 cnf(4218,plain, % 201.12/201.12 (~P16(f17(a3),f9(a3))), % 201.12/201.12 inference(scs_inference,[],[133,139,96])). % 201.12/201.12 cnf(4224,plain, % 201.12/201.12 (~P16(f17(a3),f9(f16(a1)))), % 201.12/201.12 inference(scs_inference,[],[180,129,96])). % 201.12/201.12 cnf(4235,plain, % 201.12/201.12 (P13(f13(a3),f16(a3))), % 201.12/201.12 inference(scs_inference,[],[642,68,88])). % 201.12/201.12 cnf(4239,plain, % 201.12/201.12 (~P13(f16(a3),f13(a3))), % 201.12/201.12 inference(scs_inference,[],[4235,92])). % 201.12/201.12 cnf(4267,plain, % 201.12/201.12 (~P6(f9(f16(a2)))+P13(f9(f16(a2)),f17(x42671))), % 201.12/201.12 inference(scs_inference,[],[897,47,107])). % 201.12/201.12 cnf(4274,plain, % 201.12/201.12 (P13(f9(f16(a2)),f17(x42741))+~P6(a2)), % 201.12/201.12 inference(scs_inference,[],[897,61,47,107,72,105,91])). % 201.12/201.12 cnf(4284,plain, % 201.12/201.12 (~P6(a1)+P13(a1,f17(x42841))), % 201.12/201.12 inference(scs_inference,[],[158,47,107])). % 201.12/201.12 cnf(4297,plain, % 201.12/201.12 (P13(f9(f16(a1)),f17(x42971))+~P6(a1)), % 201.12/201.12 inference(scs_inference,[],[137,61,47,107,72,105,91])). % 201.12/201.12 cnf(4318,plain, % 201.12/201.12 (~E(f17(a4),f9(f16(a1)))), % 201.12/201.12 inference(scs_inference,[],[178,2])). % 201.12/201.12 cnf(4321,plain, % 201.12/201.12 (~E(f17(a4),f9(f16(a2)))), % 201.12/201.12 inference(scs_inference,[],[899,2])). % 201.12/201.12 cnf(4329,plain, % 201.12/201.12 (P5(a3,x43291)+~E(f17(a3),x43291)), % 201.12/201.12 inference(scs_inference,[],[133,119,2705,2,9,87,3,27])). % 201.12/201.12 cnf(4361,plain, % 201.12/201.12 (P5(f14(x43611),f17(x43612))), % 201.12/201.12 inference(scs_inference,[],[435,87])). % 201.12/201.12 cnf(4368,plain, % 201.12/201.12 (P5(f15(x43681),f17(x43682))), % 201.12/201.12 inference(scs_inference,[],[730,87])). % 201.12/201.12 cnf(4404,plain, % 201.12/201.12 (~E(a2,f17(x44041))), % 201.12/201.12 inference(scs_inference,[],[440,2])). % 201.12/201.12 cnf(4410,plain, % 201.12/201.12 (~P16(f17(x44101),f15(x44102))+~P6(a1)), % 201.12/201.12 inference(scs_inference,[],[230,4284,96])). % 201.12/201.12 cnf(4420,plain, % 201.12/201.12 (~E(x44201,a1)+~E(f17(a3),f17(x44201))), % 201.12/201.12 inference(scs_inference,[],[2705,468,2,3,9])). % 201.12/201.12 cnf(4443,plain, % 201.12/201.12 (~E(x44431,a1)+~E(a3,x44431)), % 201.12/201.12 inference(scs_inference,[],[132,3])). % 201.12/201.12 cnf(4453,plain, % 201.12/201.12 (~E(x44531,a1)+~E(a12,x44531)), % 201.12/201.12 inference(scs_inference,[],[433,3])). % 201.12/201.12 cnf(4463,plain, % 201.12/201.12 (~E(x44631,a1)+~E(a5,x44631)), % 201.12/201.12 inference(scs_inference,[],[472,3])). % 201.12/201.12 cnf(4604,plain, % 201.12/201.12 (~E(x46041,a1)+~E(f17(a4),f9(f16(x46041)))), % 201.12/201.12 inference(scs_inference,[],[4318,3,13,8])). % 201.12/201.12 cnf(4609,plain, % 201.12/201.12 (~E(x46091,a2)+~E(f17(a4),f9(f16(x46091)))), % 201.12/201.12 inference(scs_inference,[],[4321,3,13,8])). % 201.12/201.12 cnf(4625,plain, % 201.12/201.12 (~E(x46251,a1)+~E(f17(a3),f9(f16(x46251)))), % 201.12/201.12 inference(scs_inference,[],[175,3,13,8])). % 201.12/201.12 cnf(4626,plain, % 201.12/201.12 (~E(f16(a1),f16(x46261))+~E(f17(a3),f9(f16(x46261)))), % 201.12/201.12 inference(scs_inference,[],[175,3,13,8,2])). % 201.12/201.12 cnf(4739,plain, % 201.12/201.12 (~E(x47391,a3)+~E(x47391,a1)), % 201.12/201.12 inference(scs_inference,[],[4443,2])). % 201.12/201.12 cnf(4755,plain, % 201.12/201.12 (~E(x47551,a12)+~E(x47551,a1)), % 201.12/201.12 inference(scs_inference,[],[4453,2])). % 201.12/201.12 cnf(4771,plain, % 201.12/201.12 (~E(x47711,a5)+~E(x47711,a1)), % 201.12/201.12 inference(scs_inference,[],[4463,2])). % 201.12/201.12 cnf(4907,plain, % 201.12/201.12 (P5(x49071,f17(x49072))+~E(f14(x49073),x49071)), % 201.12/201.12 inference(scs_inference,[],[4361,26])). % 201.12/201.12 cnf(4912,plain, % 201.12/201.12 (P5(x49121,f17(x49122))+~E(f15(x49123),x49121)), % 201.12/201.12 inference(scs_inference,[],[4368,26])). % 201.12/201.12 cnf(4923,plain, % 201.12/201.12 (P6(f6(a5))), % 201.12/201.12 inference(scs_inference,[],[66,75])). % 201.12/201.12 cnf(4925,plain, % 201.12/201.12 (P6(f7(a5))), % 201.12/201.12 inference(scs_inference,[],[66,75,76])). % 201.12/201.12 cnf(4927,plain, % 201.12/201.12 (~P1(f13(a5))), % 201.12/201.12 inference(scs_inference,[],[66,75,76,79])). % 201.12/201.12 cnf(4929,plain, % 201.12/201.12 (~P1(f6(a5))), % 201.12/201.12 inference(scs_inference,[],[66,75,76,79,80])). % 201.12/201.12 cnf(4931,plain, % 201.12/201.12 (~P1(f7(a5))), % 201.12/201.12 inference(scs_inference,[],[66,75,76,79,80,81])). % 201.12/201.12 cnf(4935,plain, % 201.12/201.12 (P5(f13(a5),f16(a5))), % 201.12/201.12 inference(scs_inference,[],[59,66,75,76,79,80,81,90,83])). % 201.12/201.12 cnf(4937,plain, % 201.12/201.12 (P5(f6(a5),f16(a5))), % 201.12/201.12 inference(scs_inference,[],[59,66,75,76,79,80,81,90,83,84])). % 201.12/201.12 cnf(4939,plain, % 201.12/201.12 (P5(f7(a5),f16(a5))), % 201.12/201.12 inference(scs_inference,[],[59,66,75,76,79,80,81,90,83,84,85])). % 201.12/201.12 cnf(4941,plain, % 201.12/201.12 (E(a2,a1)), % 201.12/201.12 inference(scs_inference,[],[59,66,36,75,76,79,80,81,90,83,84,85,71])). % 201.12/201.12 cnf(4945,plain, % 201.12/201.12 (E(f16(a2),f16(a1))), % 201.12/201.12 inference(scs_inference,[],[59,2683,66,36,75,76,79,80,81,90,83,84,85,71,93,8])). % 201.12/201.12 cnf(4946,plain, % 201.12/201.12 (~P13(a12,f16(a1))), % 201.12/201.12 inference(scs_inference,[],[59,2683,66,36,75,76,79,80,81,90,83,84,85,71,93,8,87])). % 201.12/201.12 cnf(4948,plain, % 201.12/201.12 (E(a1,a2)), % 201.12/201.12 inference(scs_inference,[],[59,2683,66,36,75,76,79,80,81,90,83,84,85,71,93,8,87,2])). % 201.12/201.12 cnf(4949,plain, % 201.12/201.12 (P6(a1)), % 201.12/201.12 inference(scs_inference,[],[59,2683,66,35,36,75,76,79,80,81,90,83,84,85,71,93,8,87,2,72])). % 201.12/201.12 cnf(4951,plain, % 201.12/201.12 (P13(f10(a12,a1),a12)), % 201.12/201.12 inference(scs_inference,[],[59,2683,66,35,36,75,76,79,80,81,90,83,84,85,71,93,8,87,2,72,95])). % 201.12/201.12 cnf(4953,plain, % 201.12/201.12 (E(f9(a2),f9(a1))), % 201.12/201.12 inference(scs_inference,[],[59,2683,66,35,36,75,76,79,80,81,90,83,84,85,71,93,8,87,2,72,95,13])). % 201.12/201.12 cnf(4954,plain, % 201.12/201.12 (E(f14(a2),f14(a1))), % 201.12/201.12 inference(scs_inference,[],[59,2683,66,35,36,75,76,79,80,81,90,83,84,85,71,93,8,87,2,72,95,13,4])). % 201.12/201.12 cnf(4956,plain, % 201.12/201.12 (P6(a2)), % 201.12/201.12 inference(scs_inference,[],[59,2683,66,35,36,75,76,79,80,81,90,83,84,85,71,93,8,87,2,72,95,13,4,5,19])). % 201.12/201.12 cnf(4957,plain, % 201.12/201.12 (~P5(f16(a3),f16(a1))), % 201.12/201.12 inference(scs_inference,[],[59,2683,66,4235,35,36,75,76,79,80,81,90,83,84,85,71,93,8,87,2,72,95,13,4,5,19,99])). % 201.12/201.12 cnf(4960,plain, % 201.12/201.12 (~P13(a12,f16(a2))), % 201.12/201.12 inference(scs_inference,[],[59,2683,66,4235,35,36,75,76,79,80,81,90,83,84,85,71,93,8,87,2,72,95,13,4,5,19,99,27,25])). % 201.12/201.12 cnf(4961,plain, % 201.12/201.12 (~P16(a12,a2)), % 201.12/201.12 inference(scs_inference,[],[59,2683,66,4235,35,36,75,76,79,80,81,90,83,84,85,71,93,8,87,2,72,95,13,4,5,19,99,27,25,18])). % 201.12/201.12 cnf(4962,plain, % 201.12/201.12 (~P5(a12,f17(a1))), % 201.12/201.12 inference(scs_inference,[],[59,2686,2683,66,4235,69,35,36,75,76,79,80,81,90,83,84,85,71,93,8,87,2,72,95,13,4,5,19,99,27,25,18,88])). % 201.12/201.12 cnf(4969,plain, % 201.12/201.12 (E(f7(a2),f7(a1))), % 201.12/201.12 inference(scs_inference,[],[59,2686,2683,66,4235,158,69,35,36,47,75,76,79,80,81,90,83,84,85,71,93,8,87,2,72,95,13,4,5,19,99,27,25,18,88,107,243,10])). % 201.12/201.12 cnf(4970,plain, % 201.12/201.12 (E(f6(a2),f6(a1))), % 201.12/201.12 inference(scs_inference,[],[59,2686,2683,66,4235,158,69,35,36,47,75,76,79,80,81,90,83,84,85,71,93,8,87,2,72,95,13,4,5,19,99,27,25,18,88,107,243,10,11])). % 201.12/201.12 cnf(4971,plain, % 201.12/201.12 (E(f13(a2),f13(a1))), % 201.12/201.12 inference(scs_inference,[],[59,2686,2683,66,4235,158,69,35,36,47,75,76,79,80,81,90,83,84,85,71,93,8,87,2,72,95,13,4,5,19,99,27,25,18,88,107,243,10,11,12])). % 201.12/201.12 cnf(4972,plain, % 201.12/201.12 (E(f11(a2,x49721),f11(a1,x49721))), % 201.12/201.12 inference(scs_inference,[],[59,2686,2683,66,4235,158,69,35,36,47,75,76,79,80,81,90,83,84,85,71,93,8,87,2,72,95,13,4,5,19,99,27,25,18,88,107,243,10,11,12,6])). % 201.12/201.12 cnf(4973,plain, % 201.12/201.12 (E(f11(x49731,a2),f11(x49731,a1))), % 201.12/201.12 inference(scs_inference,[],[59,2686,2683,66,4235,158,69,35,36,47,75,76,79,80,81,90,83,84,85,71,93,8,87,2,72,95,13,4,5,19,99,27,25,18,88,107,243,10,11,12,6,7])). % 201.12/201.12 cnf(4974,plain, % 201.12/201.12 (E(f10(a2,x49741),f10(a1,x49741))), % 201.12/201.12 inference(scs_inference,[],[59,2686,2683,66,4235,158,69,35,36,47,75,76,79,80,81,90,83,84,85,71,93,8,87,2,72,95,13,4,5,19,99,27,25,18,88,107,243,10,11,12,6,7,14])). % 201.12/201.12 cnf(4975,plain, % 201.12/201.12 (E(f10(x49751,a2),f10(x49751,a1))), % 201.12/201.12 inference(scs_inference,[],[59,2686,2683,66,4235,158,69,35,36,47,75,76,79,80,81,90,83,84,85,71,93,8,87,2,72,95,13,4,5,19,99,27,25,18,88,107,243,10,11,12,6,7,14,15])). % 201.12/201.12 cnf(4976,plain, % 201.12/201.12 (P5(f9(a1),a2)), % 201.12/201.12 inference(scs_inference,[],[59,2686,2683,66,4235,158,69,35,36,47,75,76,79,80,81,90,83,84,85,71,93,8,87,2,72,95,13,4,5,19,99,27,25,18,88,107,243,10,11,12,6,7,14,15,148])). % 201.12/201.12 cnf(4977,plain, % 201.12/201.12 (E(f17(a2),f17(a1))), % 201.12/201.12 inference(scs_inference,[],[59,2686,2683,66,4235,158,69,35,36,47,75,76,79,80,81,90,83,84,85,71,93,8,87,2,72,95,13,4,5,19,99,27,25,18,88,107,243,10,11,12,6,7,14,15,148,9])). % 201.12/201.12 cnf(4978,plain, % 201.12/201.12 (~P13(a12,f10(a12,a1))), % 201.12/201.12 inference(scs_inference,[],[59,2686,2683,66,4235,158,69,35,36,47,75,76,79,80,81,90,83,84,85,71,93,8,87,2,72,95,13,4,5,19,99,27,25,18,88,107,243,10,11,12,6,7,14,15,148,9,92])). % 201.12/201.12 cnf(4983,plain, % 201.12/201.12 (P16(f9(a1),f9(a2))), % 201.12/201.12 inference(scs_inference,[],[59,2686,2683,66,4235,158,69,35,36,60,47,75,76,79,80,81,90,83,84,85,71,93,8,87,2,72,95,13,4,5,19,99,27,25,18,88,107,243,10,11,12,6,7,14,15,148,9,92,2293,16,17])). % 201.12/201.12 cnf(4985,plain, % 201.12/201.12 (E(f11(a2,a2),f11(a1,a1))), % 201.12/201.12 inference(scs_inference,[],[59,2686,2683,66,4235,158,69,35,36,60,47,75,76,79,80,81,90,83,84,85,71,93,8,87,2,72,95,13,4,5,19,99,27,25,18,88,107,243,10,11,12,6,7,14,15,148,9,92,2293,16,17,3])). % 201.12/201.12 cnf(4989,plain, % 201.12/201.12 (P13(f9(f16(a2)),f17(x49891))), % 201.12/201.12 inference(scs_inference,[],[4956,4274])). % 201.12/201.12 cnf(4991,plain, % 201.12/201.12 (P13(f9(f16(a1)),f17(x49911))), % 201.12/201.12 inference(scs_inference,[],[4949,4297])). % 201.12/201.12 cnf(4993,plain, % 201.12/201.12 (~P16(f17(x49931),f15(x49932))), % 201.12/201.12 inference(scs_inference,[],[4949,4410])). % 201.12/201.12 cnf(4995,plain, % 201.12/201.12 (~P1(f13(a12))), % 201.12/201.12 inference(scs_inference,[],[65,79])). % 201.12/201.12 cnf(4997,plain, % 201.12/201.12 (P5(f13(a12),f16(a12))), % 201.12/201.12 inference(scs_inference,[],[65,79,83])). % 201.12/201.12 cnf(4999,plain, % 201.12/201.12 (~P1(f6(a12))), % 201.12/201.12 inference(scs_inference,[],[65,79,83,80])). % 201.12/201.12 cnf(5001,plain, % 201.12/201.12 (P5(f7(a12),f16(a12))), % 201.12/201.12 inference(scs_inference,[],[65,79,83,80,85])). % 201.12/201.12 cnf(5003,plain, % 201.12/201.12 (P5(f14(x50031),f16(x50032))), % 201.12/201.12 inference(scs_inference,[],[227,65,79,83,80,85,90])). % 201.12/201.12 cnf(5005,plain, % 201.12/201.12 (P5(f6(a12),f16(a12))), % 201.12/201.12 inference(scs_inference,[],[227,65,79,83,80,85,90,84])). % 201.12/201.12 cnf(5007,plain, % 201.12/201.12 (E(f6(a1),f6(a2))), % 201.12/201.12 inference(scs_inference,[],[4948,227,65,79,83,80,85,90,84,11])). % 201.12/201.12 cnf(5008,plain, % 201.12/201.12 (~P1(f7(a12))), % 201.12/201.12 inference(scs_inference,[],[4948,227,65,79,83,80,85,90,84,11,81])). % 201.12/201.12 cnf(5010,plain, % 201.12/201.12 (P6(f6(a12))), % 201.12/201.12 inference(scs_inference,[],[4948,227,65,79,83,80,85,90,84,11,81,75])). % 201.12/201.12 cnf(5012,plain, % 201.12/201.12 (P6(f7(a12))), % 201.12/201.12 inference(scs_inference,[],[4948,227,65,79,83,80,85,90,84,11,81,75,76])). % 201.12/201.12 cnf(5014,plain, % 201.12/201.12 (E(f11(a1,x50141),f11(a2,x50141))), % 201.12/201.12 inference(scs_inference,[],[4948,227,65,79,83,80,85,90,84,11,81,75,76,6])). % 201.12/201.12 cnf(5015,plain, % 201.12/201.12 (E(f10(x50151,a1),f10(x50151,a2))), % 201.12/201.12 inference(scs_inference,[],[4948,227,65,79,83,80,85,90,84,11,81,75,76,6,15])). % 201.12/201.12 cnf(5016,plain, % 201.12/201.12 (E(f17(a1),f17(a2))), % 201.12/201.12 inference(scs_inference,[],[4948,227,65,79,83,80,85,90,84,11,81,75,76,6,15,9])). % 201.12/201.12 cnf(5017,plain, % 201.12/201.12 (E(f10(a1,x50171),f10(a2,x50171))), % 201.12/201.12 inference(scs_inference,[],[4948,227,65,79,83,80,85,90,84,11,81,75,76,6,15,9,14])). % 201.12/201.12 cnf(5018,plain, % 201.12/201.12 (E(f11(x50181,a1),f11(x50181,a2))), % 201.12/201.12 inference(scs_inference,[],[4948,227,65,79,83,80,85,90,84,11,81,75,76,6,15,9,14,7])). % 201.12/201.12 cnf(5019,plain, % 201.12/201.12 (E(f13(a1),f13(a2))), % 201.12/201.12 inference(scs_inference,[],[4948,227,65,79,83,80,85,90,84,11,81,75,76,6,15,9,14,7,12])). % 201.12/201.12 cnf(5020,plain, % 201.12/201.12 (E(f14(x50201),a1)), % 201.12/201.12 inference(scs_inference,[],[4948,227,65,42,79,83,80,85,90,84,11,81,75,76,6,15,9,14,7,12,71])). % 201.12/201.12 cnf(5022,plain, % 201.12/201.12 (E(f7(a1),f7(a2))), % 201.12/201.12 inference(scs_inference,[],[4948,227,65,42,79,83,80,85,90,84,11,81,75,76,6,15,9,14,7,12,71,10])). % 201.12/201.12 cnf(5023,plain, % 201.12/201.12 (~P5(f17(x50231),f16(a1))), % 201.12/201.12 inference(scs_inference,[],[4948,2622,227,65,42,79,83,80,85,90,84,11,81,75,76,6,15,9,14,7,12,71,10,93])). % 201.12/201.12 cnf(5025,plain, % 201.12/201.12 (E(f16(a1),f16(a2))), % 201.12/201.12 inference(scs_inference,[],[4948,2622,227,65,42,79,83,80,85,90,84,11,81,75,76,6,15,9,14,7,12,71,10,93,8])). % 201.12/201.12 cnf(5026,plain, % 201.12/201.12 (~P13(f16(a3),f16(a1))), % 201.12/201.12 inference(scs_inference,[],[4948,4957,2622,227,65,42,79,83,80,85,90,84,11,81,75,76,6,15,9,14,7,12,71,10,93,8,87])). % 201.12/201.12 cnf(5028,plain, % 201.12/201.12 (P13(f10(a12,a2),a12)), % 201.12/201.12 inference(scs_inference,[],[4948,4961,4957,2622,227,65,42,79,83,80,85,90,84,11,81,75,76,6,15,9,14,7,12,71,10,93,8,87,95])). % 201.12/201.12 cnf(5030,plain, % 201.12/201.12 (E(f9(a1),f9(a2))), % 201.12/201.12 inference(scs_inference,[],[4948,4961,4957,2622,227,65,42,79,83,80,85,90,84,11,81,75,76,6,15,9,14,7,12,71,10,93,8,87,95,13])). % 201.12/201.12 cnf(5036,plain, % 201.12/201.12 (E(f10(x50361,a2),f10(x50361,a1))), % 201.12/201.12 inference(rename_variables,[],[4975])). % 201.12/201.12 cnf(5037,plain, % 201.12/201.12 (~P16(f17(a3),f17(a2))), % 201.12/201.12 inference(scs_inference,[],[4948,4961,4975,4927,4945,4954,4957,4977,4978,2706,2622,227,65,42,79,83,80,85,90,84,11,81,75,76,6,15,9,14,7,12,71,10,93,8,87,95,13,2,5,16,27,25,18])). % 201.12/201.12 cnf(5038,plain, % 201.12/201.12 (~P5(a5,f17(a1))), % 201.12/201.12 inference(scs_inference,[],[4948,4961,4975,4927,4945,4954,4957,4977,4978,2693,2706,2622,227,65,42,69,79,83,80,85,90,84,11,81,75,76,6,15,9,14,7,12,71,10,93,8,87,95,13,2,5,16,27,25,18,88])). % 201.12/201.12 cnf(5041,plain, % 201.12/201.12 (E(f10(a2,a2),f10(a1,a1))), % 201.12/201.12 inference(scs_inference,[],[4948,4961,4974,4975,5036,4927,4945,4954,4957,4977,4978,2693,2706,2622,227,65,42,69,79,83,80,85,90,84,11,81,75,76,6,15,9,14,7,12,71,10,93,8,87,95,13,2,5,16,27,25,18,88,3])). % 201.12/201.12 cnf(5046,plain, % 201.12/201.12 (P5(f9(a2),a1)), % 201.12/201.12 inference(scs_inference,[],[4948,4961,4974,4975,5036,4927,4945,4954,4957,4977,4978,2693,2706,2622,227,65,42,69,79,83,80,85,90,84,11,81,75,76,6,15,9,14,7,12,71,10,93,8,87,95,13,2,5,16,27,25,18,88,3,4907,243,148])). % 201.12/201.12 cnf(5047,plain, % 201.12/201.12 (~P5(f11(a2,x50471),x50472)+P5(f11(a1,x50471),x50472)), % 201.12/201.12 inference(scs_inference,[],[4948,4961,4972,4974,4975,5036,4927,4945,4954,4957,4977,4978,2693,2706,2622,227,65,42,69,79,83,80,85,90,84,11,81,75,76,6,15,9,14,7,12,71,10,93,8,87,95,13,2,5,16,27,25,18,88,3,4907,243,148,26])). % 201.12/201.12 cnf(5051,plain, % 201.12/201.12 (~P1(f6(a3))), % 201.12/201.12 inference(scs_inference,[],[64,80])). % 201.12/201.12 cnf(5053,plain, % 201.12/201.12 (P5(f7(a3),f16(a3))), % 201.12/201.12 inference(scs_inference,[],[64,80,85])). % 201.12/201.12 cnf(5055,plain, % 201.12/201.12 (~P1(f13(a3))), % 201.12/201.12 inference(scs_inference,[],[64,80,85,79])). % 201.12/201.12 cnf(5057,plain, % 201.12/201.12 (P5(f6(a3),f16(a3))), % 201.12/201.12 inference(scs_inference,[],[64,80,85,79,84])). % 201.12/201.12 cnf(5059,plain, % 201.12/201.12 (P6(f6(a3))), % 201.12/201.12 inference(scs_inference,[],[64,80,85,79,84,75])). % 201.12/201.12 cnf(5063,plain, % 201.12/201.12 (~P1(f7(a3))), % 201.12/201.12 inference(scs_inference,[],[274,64,80,85,79,84,75,90,81])). % 201.12/201.12 cnf(5065,plain, % 201.12/201.12 (E(f15(x50651),a1)), % 201.12/201.12 inference(scs_inference,[],[274,64,43,80,85,79,84,75,90,81,71])). % 201.12/201.12 cnf(5067,plain, % 201.12/201.12 (~P5(f16(x50671),f16(a1))), % 201.12/201.12 inference(scs_inference,[],[2629,274,64,43,80,85,79,84,75,90,81,71,93])). % 201.12/201.12 cnf(5069,plain, % 201.12/201.12 (~P13(f17(x50691),f16(a1))), % 201.12/201.12 inference(scs_inference,[],[5023,2629,274,64,43,80,85,79,84,75,90,81,71,93,87])). % 201.12/201.12 cnf(5071,plain, % 201.12/201.12 (P13(f10(a5,a1),a5)), % 201.12/201.12 inference(scs_inference,[],[5023,2629,2690,274,64,43,80,85,79,84,75,90,81,71,93,87,95])). % 201.12/201.12 cnf(5073,plain, % 201.12/201.12 (E(f11(a1,a1),f11(a2,a2))), % 201.12/201.12 inference(scs_inference,[],[4985,5023,2629,2690,274,64,43,80,85,79,84,75,90,81,71,93,87,95,2])). % 201.12/201.12 cnf(5076,plain, % 201.12/201.12 (~P16(f16(x50761),f14(x50762))), % 201.12/201.12 inference(scs_inference,[],[4985,5023,4929,5020,2629,2690,4945,274,64,43,80,85,79,84,75,90,81,71,93,87,95,2,27,16,18])). % 201.12/201.12 cnf(5080,plain, % 201.12/201.12 (E(f11(a1,a2),f11(a2,a1))), % 201.12/201.12 inference(scs_inference,[],[4985,4973,5014,5023,4929,5020,5026,645,2629,2690,4945,274,64,43,80,85,79,84,75,90,81,71,93,87,95,2,27,16,18,25,88,3])). % 201.12/201.12 cnf(5084,plain, % 201.12/201.12 (~P13(a5,f10(a5,a1))), % 201.12/201.12 inference(scs_inference,[],[4985,4973,5014,5023,4929,5020,5026,645,2629,2690,4945,274,64,43,80,85,79,84,75,90,81,71,93,87,95,2,27,16,18,25,88,3,742,92])). % 201.12/201.12 cnf(5088,plain, % 201.12/201.12 (~P13(x50881,a4)+P13(x50881,a8)), % 201.12/201.12 inference(scs_inference,[],[59,4985,4973,5014,5023,4929,5020,5026,38,645,2629,2690,4945,274,64,43,80,85,79,84,75,90,81,71,93,87,95,2,27,16,18,25,88,3,742,92,94,96])). % 201.12/201.12 cnf(5090,plain, % 201.12/201.12 (P5(x50901,f16(x50901))), % 201.12/201.12 inference(scs_inference,[],[60,90])). % 201.12/201.12 cnf(5092,plain, % 201.12/201.12 (~P5(f16(x50921),f16(a2))), % 201.12/201.12 inference(scs_inference,[],[2670,60,90,93])). % 201.12/201.12 cnf(5094,plain, % 201.12/201.12 (P13(f10(a3,a1),a3)), % 201.12/201.12 inference(scs_inference,[],[2670,2698,60,90,93,95])). % 201.12/201.12 cnf(5096,plain, % 201.12/201.12 (~P13(f16(x50961),f16(a1))), % 201.12/201.12 inference(scs_inference,[],[5067,2670,2698,60,90,93,95,87])). % 201.12/201.12 cnf(5098,plain, % 201.12/201.12 (E(f10(a1,a1),f10(a2,a2))), % 201.12/201.12 inference(scs_inference,[],[5067,5041,2670,2698,60,90,93,95,87,2])). % 201.12/201.12 cnf(5099,plain, % 201.12/201.12 (~P5(a5,f16(a2))), % 201.12/201.12 inference(scs_inference,[],[5067,5041,5071,2670,2698,36,60,90,93,95,87,2,99])). % 201.12/201.12 cnf(5102,plain, % 201.12/201.12 (~E(a2,f7(a5))), % 201.12/201.12 inference(scs_inference,[],[5067,4931,5041,5071,4962,2670,2698,4977,36,60,90,93,95,87,2,99,27,16])). % 201.12/201.12 cnf(5105,plain, % 201.12/201.12 (~P16(a3,f15(x51051))), % 201.12/201.12 inference(scs_inference,[],[5067,4931,5041,5055,5065,5071,4962,4239,2670,2698,4977,36,60,90,93,95,87,2,99,27,16,88,18])). % 201.12/201.12 cnf(5108,plain, % 201.12/201.12 (E(f10(a2,a1),f10(a1,a2))), % 201.12/201.12 inference(scs_inference,[],[5015,5067,4931,5041,5055,5065,5084,5071,4962,4239,2670,2698,4975,4974,4977,36,60,90,93,95,87,2,99,27,16,88,18,25,3])). % 201.12/201.12 cnf(5111,plain, % 201.12/201.12 (~P13(a3,f10(a3,a1))), % 201.12/201.12 inference(scs_inference,[],[5015,5067,4931,5041,5055,5065,5084,5071,4962,4239,2670,2698,4975,4974,4977,36,60,90,93,95,87,2,99,27,16,88,18,25,3,92])). % 201.12/201.12 cnf(5117,plain, % 201.12/201.12 (~P5(a5,f16(a1))), % 201.12/201.12 inference(scs_inference,[],[2690,93])). % 201.12/201.12 cnf(5119,plain, % 201.12/201.12 (~P13(f16(x51191),f16(a2))), % 201.12/201.12 inference(scs_inference,[],[5092,2690,93,87])). % 201.12/201.12 cnf(5122,plain, % 201.12/201.12 (~P13(a5,f16(a2))), % 201.12/201.12 inference(scs_inference,[],[5090,5092,5080,5099,2690,93,87,2,100])). % 201.12/201.12 cnf(5125,plain, % 201.12/201.12 (~E(f10(a3,a1),f17(a3))), % 201.12/201.12 inference(scs_inference,[],[5090,5092,5080,5094,5099,2690,163,93,87,2,100,24])). % 201.12/201.12 cnf(5126,plain, % 201.12/201.12 (~P5(a3,f16(a1))), % 201.12/201.12 inference(scs_inference,[],[5090,5092,5080,5094,5099,2690,163,35,93,87,2,100,24,99])). % 201.12/201.12 cnf(5128,plain, % 201.12/201.12 (~P5(a5,f17(a2))), % 201.12/201.12 inference(scs_inference,[],[5090,5092,5080,5094,5099,5038,2690,4977,163,35,93,87,2,100,24,99,27])). % 201.12/201.12 cnf(5129,plain, % 201.12/201.12 (~P5(f16(x51291),f17(a2))), % 201.12/201.12 inference(scs_inference,[],[5090,5092,5080,5094,5099,5038,2675,2690,4977,163,69,35,93,87,2,100,24,99,27,88])). % 201.12/201.12 cnf(5135,plain, % 201.12/201.12 (~P16(a5,a2)), % 201.12/201.12 inference(scs_inference,[],[5090,5092,4995,5080,5111,5094,5099,5038,2675,4941,2690,4975,4977,163,69,42,35,93,87,2,100,24,99,27,88,16,25,18])). % 201.12/201.12 cnf(5136,plain, % 201.12/201.12 (E(f15(x51361),a2)), % 201.12/201.12 inference(scs_inference,[],[5090,5092,4995,5080,5111,5094,5099,5038,2675,4941,5065,2690,4975,4977,163,69,42,35,4948,93,87,2,100,24,99,27,88,16,25,18,3])). % 201.12/201.12 cnf(5138,plain, % 201.12/201.12 (P13(f10(a5,a2),a5)), % 201.12/201.12 inference(scs_inference,[],[5090,5092,4995,5080,5111,5094,5099,5038,2675,4941,5065,2690,4975,4977,163,69,42,35,4948,93,87,2,100,24,99,27,88,16,25,18,3,742,95])). % 201.12/201.12 cnf(5147,plain, % 201.12/201.12 (E(f10(a1,a2),f10(a2,a1))), % 201.12/201.12 inference(scs_inference,[],[5117,5108,87,2])). % 201.12/201.12 cnf(5148,plain, % 201.12/201.12 (P5(f10(a5,a2),a5)), % 201.12/201.12 inference(scs_inference,[],[5117,5108,5138,5090,87,2,100])). % 201.12/201.12 cnf(5151,plain, % 201.12/201.12 (~P5(f16(x51511),f17(a1))), % 201.12/201.12 inference(scs_inference,[],[5129,5117,5108,5138,5016,5090,87,2,100,27])). % 201.12/201.12 cnf(5152,plain, % 201.12/201.12 (~P5(f17(x51521),f17(a1))), % 201.12/201.12 inference(scs_inference,[],[5129,5117,5108,5138,5016,5090,2625,69,87,2,100,27,88])). % 201.12/201.12 cnf(5156,plain, % 201.12/201.12 (~P16(a5,f15(x51561))), % 201.12/201.12 inference(scs_inference,[],[5135,5129,5117,4999,5108,5136,5138,5016,5090,2625,43,69,87,2,100,27,88,16,18])). % 201.12/201.12 cnf(5158,plain, % 201.12/201.12 (E(f14(x51581),a2)), % 201.12/201.12 inference(scs_inference,[],[5135,5129,5117,4999,5108,5136,5138,5016,5090,2686,2625,5020,4977,43,69,4948,87,2,100,27,88,16,18,25,3])). % 201.12/201.12 cnf(5164,plain, % 201.12/201.12 (~P13(a3,f16(a1))), % 201.12/201.12 inference(scs_inference,[],[5126,87])). % 201.12/201.12 cnf(5166,plain, % 201.12/201.12 (E(a2,f14(x51661))), % 201.12/201.12 inference(scs_inference,[],[5158,5126,87,2])). % 201.12/201.12 cnf(5181,plain, % 201.12/201.12 (P16(f10(a2,a1),f10(a1,a2))), % 201.12/201.12 inference(scs_inference,[],[5147,5158,54,57,5126,52,53,56,58,55,60,87,2,34,33,30,28,31,32,29,17])). % 201.12/201.12 cnf(5183,plain, % 201.12/201.12 (~P5(f17(x51831),f17(a2))), % 201.12/201.12 inference(scs_inference,[],[5147,5152,5158,54,57,5126,52,53,56,58,55,4977,60,87,2,34,33,30,28,31,32,29,17,27])). % 201.12/201.12 cnf(5184,plain, % 201.12/201.13 (~P5(a3,f17(a1))), % 201.12/201.13 inference(scs_inference,[],[5147,5152,5158,54,57,5126,52,53,56,58,55,4977,2701,69,60,87,2,34,33,30,28,31,32,29,17,27,88])). % 201.12/201.13 cnf(5188,plain, % 201.12/201.13 (~P16(f17(x51881),f14(x51882))), % 201.12/201.13 inference(scs_inference,[],[5147,5152,5008,5158,54,57,5126,52,53,56,58,55,2663,4977,2701,42,69,60,87,2,34,33,30,28,31,32,29,17,27,88,16,18])). % 201.12/201.13 cnf(5189,plain, % 201.12/201.13 (~P13(f17(x51891),f16(a2))), % 201.12/201.13 inference(scs_inference,[],[5147,5152,5008,5158,54,57,5126,52,53,56,58,55,5069,2663,4945,4977,2701,42,69,60,87,2,34,33,30,28,31,32,29,17,27,88,16,18,25])). % 201.12/201.13 cnf(5201,plain, % 201.12/201.13 (E(a2,f15(x52011))), % 201.12/201.13 inference(scs_inference,[],[5128,5136,87,2])). % 201.12/201.13 cnf(5204,plain, % 201.12/201.13 (P5(f9(a1),f14(x52041))), % 201.12/201.13 inference(scs_inference,[],[4976,5166,5148,5128,5136,4975,87,2,26,27])). % 201.12/201.13 cnf(5206,plain, % 201.12/201.13 (P16(f10(a2,a1),f10(a2,a2))), % 201.12/201.13 inference(scs_inference,[],[5181,4976,5051,5166,5148,5128,5017,5136,4975,43,87,2,26,27,16,18])). % 201.12/201.13 cnf(5209,plain, % 201.12/201.13 (E(f15(x52091),f14(x52092))), % 201.12/201.13 inference(scs_inference,[],[5181,4976,5051,5166,5148,5164,5128,5017,5136,4975,4945,43,87,2,26,27,16,18,25,3])). % 201.12/201.13 cnf(5211,plain, % 201.12/201.13 (P5(f10(a12,a1),a12)), % 201.12/201.13 inference(scs_inference,[],[5181,4976,5051,5166,5148,5164,5128,5017,4951,5136,5090,4975,4945,43,87,2,26,27,16,18,25,3,742,100])). % 201.12/201.13 cnf(5217,plain, % 201.12/201.13 (~P13(x52171,f10(a2,a1))+P13(x52171,f10(a1,a2))), % 201.12/201.13 inference(scs_inference,[],[5181,4976,5051,5166,5148,5164,5128,5017,4951,5136,5090,4404,4975,4945,43,161,87,2,26,27,16,18,25,3,742,100,102,96])). % 201.12/201.13 cnf(5219,plain, % 201.12/201.13 (E(f14(x52191),f15(x52192))), % 201.12/201.13 inference(scs_inference,[],[5209,2])). % 201.12/201.13 cnf(5220,plain, % 201.12/201.13 (~P5(a3,f16(a2))), % 201.12/201.13 inference(scs_inference,[],[5209,5094,36,2,99])). % 201.12/201.13 cnf(5222,plain, % 201.12/201.13 (~P5(a3,f17(a2))), % 201.12/201.13 inference(scs_inference,[],[5209,5184,5094,4977,36,2,99,27])). % 201.12/201.13 cnf(5223,plain, % 201.12/201.13 (~E(a2,f7(a3))), % 201.12/201.13 inference(scs_inference,[],[5209,5063,5184,5094,4977,36,2,99,27,16])). % 201.12/201.13 cnf(5224,plain, % 201.12/201.13 (~P16(f16(x52241),f15(x52242))), % 201.12/201.13 inference(scs_inference,[],[5209,5063,5076,5184,5094,4977,36,2,99,27,16,18])). % 201.12/201.13 cnf(5228,plain, % 201.12/201.13 (~P16(a3,a2)), % 201.12/201.13 inference(scs_inference,[],[5209,5063,5201,5076,5184,5094,5136,4977,2701,37,36,47,2,99,27,16,18,25,3,107])). % 201.12/201.13 cnf(5231,plain, % 201.12/201.13 (P13(f10(a3,a2),a3)), % 201.12/201.13 inference(scs_inference,[],[5209,5063,5201,5076,5184,5094,5136,4977,2701,37,36,47,2,99,27,16,18,25,3,107,95])). % 201.12/201.13 cnf(5243,plain, % 201.12/201.13 (E(a1,f15(x52431))), % 201.12/201.13 inference(scs_inference,[],[5065,2])). % 201.12/201.13 cnf(5247,plain, % 201.12/201.13 (P16(f10(a2,a1),f10(a1,a1))), % 201.12/201.13 inference(scs_inference,[],[5219,5204,5206,4927,5041,5065,43,2,27,16,18])). % 201.12/201.13 cnf(5248,plain, % 201.12/201.13 (~P13(x52481,f7(a2))+P13(x52481,f7(a1))), % 201.12/201.13 inference(scs_inference,[],[5219,5204,4969,5206,4927,5041,5065,43,2,27,16,18,25])). % 201.12/201.13 cnf(5255,plain, % 201.12/201.13 (E(a1,f14(x52551))), % 201.12/201.13 inference(scs_inference,[],[5020,2])). % 201.12/201.13 cnf(5258,plain, % 201.12/201.13 (~P16(a12,f15(x52581))), % 201.12/201.13 inference(scs_inference,[],[5231,4929,4961,5020,5136,163,35,2,24,16,18])). % 201.12/201.13 cnf(5260,plain, % 201.12/201.13 (~P13(a12,x52601)+~E(x52601,f9(a12))), % 201.12/201.13 inference(scs_inference,[],[5046,5243,5231,232,4929,4961,5020,5136,163,35,2,24,16,18,27,25])). % 201.12/201.13 cnf(5266,plain, % 201.12/201.13 (~P16(a3,f14(x52661))), % 201.12/201.13 inference(scs_inference,[],[5228,5158,18])). % 201.12/201.13 cnf(5268,plain, % 201.12/201.13 (~P13(x52681,f6(a2))+P13(x52681,f6(a1))), % 201.12/201.13 inference(scs_inference,[],[4970,5228,4931,5158,42,18,16,25])). % 201.12/201.13 cnf(5294,plain, % 201.12/201.13 (P5(f10(a3,a2),a3)), % 201.12/201.13 inference(scs_inference,[],[5231,5090,100])). % 201.12/201.13 cnf(5298,plain, % 201.12/201.13 (~P13(a5,x52981)+~E(x52981,f9(a5))), % 201.12/201.13 inference(scs_inference,[],[254,4999,5231,5090,42,100,16,25])). % 201.12/201.13 cnf(5304,plain, % 201.12/201.13 (P5(f10(a3,a1),a3)), % 201.12/201.13 inference(scs_inference,[],[5294,4975,26])). % 201.12/201.13 cnf(5307,plain, % 201.12/201.13 (~P13(x53071,f6(a1))+P13(x53071,f6(a2))), % 201.12/201.13 inference(scs_inference,[],[5294,5007,5008,4975,43,26,16,25])). % 201.12/201.13 cnf(5315,plain, % 201.12/201.13 (~P13(f17(a3),x53151)+~E(x53151,f13(a3))), % 201.12/201.13 inference(scs_inference,[],[5051,645,36,16,25])). % 201.12/201.13 cnf(5323,plain, % 201.12/201.13 (~P13(x53231,f13(a1))+P13(x53231,f13(a2))), % 201.12/201.13 inference(scs_inference,[],[5019,5255,5046,5055,35,27,16,25])). % 201.12/201.13 cnf(5331,plain, % 201.12/201.13 (~P13(f16(a3),x53311)+~E(x53311,f13(a3))), % 201.12/201.13 inference(scs_inference,[],[5063,4239,42,16,25])). % 201.12/201.13 cnf(5361,plain, % 201.12/201.13 (~P16(a12,f14(x53611))), % 201.12/201.13 inference(scs_inference,[],[5028,2683,5020,5090,100,18])). % 201.12/201.13 cnf(5377,plain, % 201.12/201.13 (~P13(x53771,f11(a1,a1))+P13(x53771,f11(a2,a2))), % 201.12/201.13 inference(scs_inference,[],[5073,4929,42,16,25])). % 201.12/201.13 cnf(5394,plain, % 201.12/201.13 (~E(a2,f7(a12))), % 201.12/201.13 inference(scs_inference,[],[5008,36,16])). % 201.12/201.13 cnf(5397,plain, % 201.12/201.13 (~P13(x53971,f9(a1))+P13(x53971,f9(a2))), % 201.12/201.13 inference(scs_inference,[],[4983,5008,4951,38,36,16,89,96])). % 201.12/201.13 cnf(5399,plain, % 201.12/201.13 (P16(f10(a2,a2),f10(a1,a1))), % 201.12/201.13 inference(scs_inference,[],[5098,60,17])). % 201.12/201.13 cnf(5413,plain, % 201.12/201.13 (P16(f10(a2,a2),f10(a1,a2))), % 201.12/201.13 inference(scs_inference,[],[5399,5015,5055,42,16,18])). % 201.12/201.13 cnf(5420,plain, % 201.12/201.13 (~P13(a3,f16(x54201))+~E(f16(x54201),f17(a2))), % 201.12/201.13 inference(scs_inference,[],[5228,5063,45,43,16,94])). % 201.12/201.13 cnf(5438,plain, % 201.12/201.13 (~P13(x54381,f11(x54382,a1))+P13(x54381,f11(x54382,a2))), % 201.12/201.13 inference(scs_inference,[],[5018,25])). % 201.12/201.13 cnf(5458,plain, % 201.12/201.13 (P16(f10(a2,a2),f10(a2,a1))), % 201.12/201.13 inference(scs_inference,[],[5413,5147,18])). % 201.12/201.13 cnf(5459,plain, % 201.12/201.13 (~E(a2,f6(a5))), % 201.12/201.13 inference(scs_inference,[],[5413,5147,4929,36,18,16])). % 201.12/201.13 cnf(5486,plain, % 201.12/201.13 (~P13(a5,f16(x54861))+~E(f16(x54861),f17(a2))), % 201.12/201.13 inference(scs_inference,[],[5135,5051,45,42,16,94])). % 201.12/201.13 cnf(5525,plain, % 201.12/201.13 (~E(a2,f6(a12))), % 201.12/201.13 inference(scs_inference,[],[4999,36,16])). % 201.12/201.13 cnf(5546,plain, % 201.12/201.13 (P16(f11(a2,a2),f11(a1,a1))), % 201.12/201.13 inference(scs_inference,[],[5073,60,17])). % 201.12/201.13 cnf(5548,plain, % 201.12/201.13 (~P13(f17(x55481),f16(x55482))+~E(f16(x55482),f17(a1))), % 201.12/201.13 inference(scs_inference,[],[5073,2622,45,60,17,94])). % 201.12/201.13 cnf(5553,plain, % 201.12/201.13 (P16(f11(a2,a2),f11(a1,a2))), % 201.12/201.13 inference(scs_inference,[],[5546,5018,18])). % 201.12/201.13 cnf(5567,plain, % 201.12/201.13 (~P13(x55671,f9(a2))+P13(x55671,f9(a1))), % 201.12/201.13 inference(scs_inference,[],[4953,40,22,25])). % 201.12/201.13 cnf(5576,plain, % 201.12/201.13 (P16(f11(a1,a1),f11(a1,a2))), % 201.12/201.13 inference(scs_inference,[],[5553,4985,17])). % 201.12/201.13 cnf(5592,plain, % 201.12/201.13 (~P13(x55921,f11(a1,a2))+P13(x55921,f11(a2,a1))), % 201.12/201.13 inference(scs_inference,[],[5080,25])). % 201.12/201.13 cnf(5604,plain, % 201.12/201.13 (P16(f11(a1,a1),f11(a2,a1))), % 201.12/201.13 inference(scs_inference,[],[5576,5080,18])). % 201.12/201.13 cnf(5612,plain, % 201.12/201.13 (P16(f11(a2,a2),f11(a2,a1))), % 201.12/201.13 inference(scs_inference,[],[5604,5546,97])). % 201.12/201.13 cnf(5620,plain, % 201.12/201.13 (P16(f10(a1,a2),f10(a1,a1))), % 201.12/201.13 inference(scs_inference,[],[5247,5108,17])). % 201.12/201.13 cnf(5634,plain, % 201.12/201.13 (~P13(x56341,f13(a2))+P13(x56341,f13(a1))), % 201.12/201.13 inference(scs_inference,[],[4971,25])). % 201.12/201.13 cnf(5639,plain, % 201.12/201.13 (P16(f10(a1,a2),f10(a2,a2))), % 201.12/201.13 inference(scs_inference,[],[5620,5098,18])). % 201.12/201.13 cnf(5642,plain, % 201.12/201.13 (P16(f10(a1,a2),f10(a2,a1))), % 201.12/201.13 inference(scs_inference,[],[5639,5458,97])). % 201.12/201.13 cnf(5644,plain, % 201.12/201.13 (P16(f11(a1,a2),f11(a2,a1))), % 201.12/201.13 inference(scs_inference,[],[5639,5612,5458,4972,97,17])). % 201.12/201.13 cnf(5658,plain, % 201.12/201.13 (~P13(x56581,f7(a1))+P13(x56581,f7(a2))), % 201.12/201.13 inference(scs_inference,[],[5022,25])). % 201.12/201.13 cnf(5666,plain, % 201.12/201.13 (P16(f11(a1,a2),f11(a2,a2))), % 201.12/201.13 inference(scs_inference,[],[5644,5018,18])). % 201.12/201.13 cnf(5676,plain, % 201.12/201.13 (P16(f11(a2,a1),f11(a2,a2))), % 201.12/201.13 inference(scs_inference,[],[5666,5576,5080,97,17])). % 201.12/201.13 cnf(5677,plain, % 201.12/201.13 (~P13(x56771,f11(x56772,a2))+P13(x56771,f11(x56772,a1))), % 201.12/201.13 inference(scs_inference,[],[5666,5576,4973,5080,97,17,25])). % 201.12/201.13 cnf(5707,plain, % 201.12/201.13 (~P13(f16(x57071),f16(x57072))+~E(f16(x57072),f17(a2))), % 201.12/201.13 inference(scs_inference,[],[2670,45,94])). % 201.12/201.13 cnf(5718,plain, % 201.12/201.13 (~P13(x57181,f11(a2,a2))+P13(x57181,f11(a1,a1))), % 201.12/201.13 inference(scs_inference,[],[4985,37,19,25])). % 201.12/201.13 cnf(5720,plain, % 201.12/201.13 (~P13(x57201,f10(a1,a2))+P13(x57201,f10(a1,a1))), % 201.12/201.13 inference(scs_inference,[],[5620,96])). % 201.12/201.13 cnf(5726,plain, % 201.12/201.13 (P16(f10(a1,a1),f10(a2,a2))), % 201.12/201.13 inference(scs_inference,[],[5639,4975,17])). % 201.12/201.13 cnf(5728,plain, % 201.12/201.13 (~P13(x57281,f10(a2,a2))+P13(x57281,f10(a1,a1))), % 201.12/201.13 inference(scs_inference,[],[5639,5041,4975,17,25])). % 201.12/201.13 cnf(5736,plain, % 201.12/201.13 (P16(f10(a1,a1),f10(a2,a1))), % 201.12/201.13 inference(scs_inference,[],[5726,4975,18])). % 201.12/201.13 cnf(5761,plain, % 201.12/201.13 (~P13(x57611,f11(a1,x57612))+P13(x57611,f11(a2,x57612))), % 201.12/201.13 inference(scs_inference,[],[5014,25])). % 201.12/201.13 cnf(5762,plain, % 201.12/201.13 (~P13(f17(x57621),f16(x57622))+~E(f16(x57622),f17(a2))), % 201.12/201.13 inference(scs_inference,[],[2663,45,94])). % 201.12/201.13 cnf(5776,plain, % 201.12/201.13 (~P13(x57761,f10(a1,a1))+P13(x57761,f10(a2,a2))), % 201.12/201.13 inference(scs_inference,[],[5726,96])). % 201.12/201.13 cnf(5782,plain, % 201.12/201.13 (~P13(x57821,f11(a2,x57822))+P13(x57821,f11(a1,x57822))), % 201.12/201.13 inference(scs_inference,[],[4972,25])). % 201.12/201.13 cnf(5792,plain, % 201.12/201.13 (~P13(x57921,f10(a1,x57922))+P13(x57921,f10(a2,x57922))), % 201.12/201.13 inference(scs_inference,[],[5017,25])). % 201.12/201.13 cnf(5813,plain, % 201.12/201.13 (~P13(a12,f16(x58131))+~E(f16(x58131),f17(a2))), % 201.12/201.13 inference(scs_inference,[],[5111,4961,45,24,94])). % 201.12/201.13 cnf(5816,plain, % 201.12/201.13 (~P13(x58161,f10(a2,a1))+P13(x58161,f10(a2,a2))), % 201.12/201.13 inference(scs_inference,[],[5206,96])). % 201.12/201.13 cnf(5821,plain, % 201.12/201.13 (~P13(x58211,f10(a2,x58212))+P13(x58211,f10(a1,x58212))), % 201.12/201.13 inference(scs_inference,[],[4974,25])). % 201.12/201.13 cnf(5855,plain, % 201.12/201.13 (~P13(a3,f16(x58551))+~E(f16(x58551),f17(a1))), % 201.12/201.13 inference(scs_inference,[],[254,2698,45,24,94])). % 201.12/201.13 cnf(5865,plain, % 201.12/201.13 (~P13(f16(x58651),f16(x58652))+~E(f16(x58652),f17(a1))), % 201.12/201.13 inference(scs_inference,[],[2629,45,94])). % 201.12/201.13 cnf(5874,plain, % 201.12/201.13 (~P13(a5,f16(x58741))+~E(f16(x58741),f17(a1))), % 201.12/201.13 inference(scs_inference,[],[2690,45,94])). % 201.12/201.13 cnf(5892,plain, % 201.12/201.13 (~P13(a12,f16(x58921))+~E(f16(x58921),f17(a1))), % 201.12/201.13 inference(scs_inference,[],[2683,45,94])). % 201.12/201.13 cnf(5898,plain, % 201.12/201.13 (P16(f11(a2,a1),f11(a1,a1))), % 201.12/201.13 inference(scs_inference,[],[5676,4985,18])). % 201.12/201.13 cnf(5901,plain, % 201.12/201.13 (P16(f11(a1,a2),f11(a1,a1))), % 201.12/201.13 inference(scs_inference,[],[5898,5644,97])). % 201.12/201.13 cnf(5950,plain, % 201.12/201.13 (P16(f11(a2,a1),f11(a1,a2))), % 201.12/201.13 inference(scs_inference,[],[5676,5553,97])). % 201.12/201.13 cnf(6075,plain, % 201.12/201.13 (P16(f9(a2),f9(a1))), % 201.12/201.13 inference(scs_inference,[],[60,4953,18])). % 201.12/201.13 cnf(6076,plain, % 201.12/201.13 (P16(x60761,x60761)), % 201.12/201.13 inference(rename_variables,[],[60])). % 201.12/201.13 cnf(6077,plain, % 201.12/201.13 (P16(f7(a1),f7(a2))), % 201.12/201.13 inference(scs_inference,[],[60,6076,4969,4953,18,17])). % 201.12/201.13 cnf(6085,plain, % 201.12/201.13 (P16(f6(a2),f6(a1))), % 201.12/201.13 inference(scs_inference,[],[60,4970,18])). % 201.12/201.13 cnf(6086,plain, % 201.12/201.13 (P16(x60861,x60861)), % 201.12/201.13 inference(rename_variables,[],[60])). % 201.12/201.13 cnf(6087,plain, % 201.12/201.13 (P16(f13(a2),f13(a1))), % 201.12/201.13 inference(scs_inference,[],[60,6086,5019,4970,18,17])). % 201.12/201.13 cnf(6094,plain, % 201.12/201.13 (P16(f10(x60941,a1),f10(x60941,a2))), % 201.12/201.13 inference(scs_inference,[],[60,5015,18])). % 201.12/201.13 cnf(6095,plain, % 201.12/201.13 (P16(x60951,x60951)), % 201.12/201.13 inference(rename_variables,[],[60])). % 201.12/201.13 cnf(6096,plain, % 201.12/201.13 (P16(f10(x60961,a2),f10(x60961,a1))), % 201.12/201.13 inference(scs_inference,[],[60,6095,5015,18,17])). % 201.12/201.13 cnf(6196,plain, % 201.12/201.13 (~P13(x61961,f13(a5))+P13(x61961,a5)), % 201.12/201.13 inference(scs_inference,[],[4935,93,96])). % 201.12/201.13 cnf(6209,plain, % 201.12/201.13 (P16(f6(a5),a5)), % 201.12/201.13 inference(scs_inference,[],[4937,93])). % 201.12/201.13 cnf(6211,plain, % 201.12/201.13 (~P13(x62111,f6(a5))+P13(x62111,a5)), % 201.12/201.13 inference(scs_inference,[],[4937,93,96])). % 201.12/201.13 cnf(6249,plain, % 201.12/201.13 (P16(f7(a5),a5)), % 201.12/201.13 inference(scs_inference,[],[4939,93])). % 201.12/201.13 cnf(6251,plain, % 201.12/201.13 (~P13(x62511,f7(a5))+P13(x62511,a5)), % 201.12/201.13 inference(scs_inference,[],[4939,93,96])). % 201.12/201.13 cnf(6268,plain, % 201.12/201.13 (~P13(x62681,f13(a12))+P13(x62681,a12)), % 201.12/201.13 inference(scs_inference,[],[4997,93,96])). % 201.12/201.13 cnf(6277,plain, % 201.12/201.13 (~P16(a5,f14(x62771))), % 201.12/201.13 inference(scs_inference,[],[5156,5219,18])). % 201.12/201.13 cnf(6286,plain, % 201.12/201.13 (~P13(f17(a5),x62861)+~E(x62861,f6(a5))), % 201.12/201.13 inference(scs_inference,[],[6209,4923,47,107,92,25])). % 201.12/201.13 cnf(6287,plain, % 201.12/201.13 (~P5(f17(a5),f6(a5))), % 201.12/201.13 inference(scs_inference,[],[6209,4923,4929,47,107,92,25,88])). % 201.12/201.13 cnf(6299,plain, % 201.12/201.13 (P16(f7(a12),a12)), % 201.12/201.13 inference(scs_inference,[],[5001,93])). % 201.12/201.13 cnf(6301,plain, % 201.12/201.13 (~P13(x63011,f7(a12))+P13(x63011,a12)), % 201.12/201.13 inference(scs_inference,[],[5001,93,96])). % 201.12/201.13 cnf(6319,plain, % 201.12/201.13 (P16(f6(a12),a12)), % 201.12/201.13 inference(scs_inference,[],[5005,93])). % 201.12/201.13 cnf(6321,plain, % 201.12/201.13 (~P13(x63211,f6(a12))+P13(x63211,a12)), % 201.12/201.13 inference(scs_inference,[],[5005,93,96])). % 201.12/201.13 cnf(6336,plain, % 201.12/201.13 (P13(f7(a5),f17(a5))), % 201.12/201.13 inference(scs_inference,[],[6249,4925,47,107])). % 201.12/201.13 cnf(6341,plain, % 201.12/201.13 (~P13(f17(a5),x63411)+~E(x63411,f7(a5))), % 201.12/201.13 inference(scs_inference,[],[6249,4925,47,107,92,25])). % 201.12/201.13 cnf(6342,plain, % 201.12/201.13 (~P5(f17(a5),f7(a5))), % 201.12/201.13 inference(scs_inference,[],[6249,4925,4931,47,107,92,25,88])). % 201.12/201.13 cnf(6353,plain, % 201.12/201.13 (P16(f7(a3),a3)), % 201.12/201.13 inference(scs_inference,[],[5053,6336,5090,100,93])). % 201.12/201.13 cnf(6359,plain, % 201.12/201.13 (~P13(f17(a3),f7(a3))), % 201.12/201.13 inference(scs_inference,[],[6353,163,96])). % 201.12/201.13 cnf(6361,plain, % 201.12/201.13 (~P5(f17(a3),f7(a3))), % 201.12/201.13 inference(scs_inference,[],[6353,5063,163,96,88])). % 201.12/201.13 cnf(6379,plain, % 201.12/201.13 (~P13(f17(a3),x63791)+~E(x63791,f7(a3))), % 201.12/201.13 inference(scs_inference,[],[6359,6353,524,45,98,25])). % 201.12/201.13 cnf(6384,plain, % 201.12/201.13 (P16(f6(a3),a3)), % 201.12/201.13 inference(scs_inference,[],[5057,93])). % 201.12/201.13 cnf(6395,plain, % 201.12/201.13 (~P13(f17(a3),f6(a3))), % 201.12/201.13 inference(scs_inference,[],[6384,5059,47,107,87,92])). % 201.12/201.13 cnf(6397,plain, % 201.12/201.13 (~P5(f17(a3),f6(a3))), % 201.12/201.13 inference(scs_inference,[],[6384,5059,5051,47,107,87,92,88])). % 201.12/201.13 cnf(6407,plain, % 201.12/201.13 (~P13(f17(a3),x64071)+~E(x64071,f6(a3))), % 201.12/201.13 inference(scs_inference,[],[6395,25])). % 201.12/201.13 cnf(6436,plain, % 201.12/201.13 (~P13(f17(a12),x64361)+~E(x64361,f7(a12))), % 201.12/201.13 inference(scs_inference,[],[6299,5012,47,107,92,25])). % 201.12/201.13 cnf(6437,plain, % 201.12/201.13 (~P5(f17(a12),f7(a12))), % 201.12/201.13 inference(scs_inference,[],[6299,5012,5008,47,107,92,25,88])). % 201.12/201.13 cnf(6461,plain, % 201.12/201.13 (P13(f6(a12),f17(a12))), % 201.12/201.13 inference(scs_inference,[],[6319,5010,47,107])). % 201.12/201.13 cnf(6467,plain, % 201.12/201.13 (~P5(f17(a12),f6(a12))), % 201.12/201.13 inference(scs_inference,[],[6461,4999,92,88])). % 201.12/201.13 cnf(6560,plain, % 201.12/201.13 (~E(f6(a5),a2)), % 201.12/201.13 inference(scs_inference,[],[5459,2])). % 201.12/201.13 cnf(6563,plain, % 201.12/201.13 (P13(f9(f13(a5)),a5)), % 201.12/201.13 inference(scs_inference,[],[4927,61,6196,88])). % 201.12/201.13 cnf(6574,plain, % 201.12/201.13 (P13(f9(f6(a5)),a5)), % 201.12/201.13 inference(scs_inference,[],[4929,61,6211,88])). % 201.12/201.13 cnf(6578,plain, % 201.12/201.13 (P13(f9(f7(a5)),a5)), % 201.12/201.13 inference(scs_inference,[],[4931,61,6251,88])). % 201.12/201.13 cnf(6579,plain, % 201.12/201.13 (P13(f9(f13(a12)),a12)), % 201.12/201.13 inference(scs_inference,[],[4995,61,6268,88])). % 201.12/201.13 cnf(6589,plain, % 201.12/201.13 (~E(f7(a5),a2)), % 201.12/201.13 inference(scs_inference,[],[5102,2])). % 201.12/201.13 cnf(6642,plain, % 201.12/201.13 (~E(f7(a3),a2)), % 201.12/201.13 inference(scs_inference,[],[5223,2])). % 201.12/201.13 cnf(6655,plain, % 201.12/201.13 (~E(f7(a12),a2)), % 201.12/201.13 inference(scs_inference,[],[5394,2])). % 201.12/201.13 cnf(6669,plain, % 201.12/201.13 (E(f9(f17(a1)),f9(f17(a2)))), % 201.12/201.13 inference(scs_inference,[],[2569,5016,5069,5065,5025,343,854,4604,4625,820,4626,4420,93,13])). % 201.12/201.13 cnf(6674,plain, % 201.12/201.13 (P6(f9(f16(a2)))), % 201.12/201.13 inference(scs_inference,[],[2569,4989,5016,5069,897,5065,5025,343,854,4604,4625,820,4626,4420,93,13,87,90,86])). % 201.12/201.13 cnf(6678,plain, % 201.12/201.13 (~P1(f7(f13(f6(a12))))), % 201.12/201.13 inference(scs_inference,[],[2569,4989,549,5016,5069,897,5065,5025,343,854,4604,4625,820,4626,4420,93,13,87,90,86,84,81])). % 201.12/201.13 cnf(6682,plain, % 201.12/201.13 (E(f10(x66821,f17(a1)),f10(x66821,f17(a2)))), % 201.12/201.13 inference(scs_inference,[],[2569,4989,549,5016,5069,897,5065,5025,343,854,4604,4625,820,4626,4420,93,13,87,90,86,84,81,85,15])). % 201.12/201.13 cnf(6683,plain, % 201.12/201.13 (E(f13(f17(a1)),f13(f17(a2)))), % 201.12/201.13 inference(scs_inference,[],[2569,4989,549,5016,5069,897,5065,5025,343,854,4604,4625,820,4626,4420,93,13,87,90,86,84,81,85,15,12])). % 201.12/201.13 cnf(6687,plain, % 201.12/201.13 (E(f16(f17(a1)),f16(f17(a2)))), % 201.12/201.13 inference(scs_inference,[],[2569,4989,549,5016,5069,897,5065,5025,343,854,4604,4625,820,4626,4420,93,13,87,90,86,84,81,85,15,12,2,148,9,8])). % 201.12/201.13 cnf(6691,plain, % 201.12/201.13 (P13(f9(f16(a1)),f17(x66911))), % 201.12/201.13 inference(rename_variables,[],[4991])). % 201.12/201.13 cnf(6693,plain, % 201.12/201.13 (E(f10(a1,f14(x66931)),f10(a2,a2))), % 201.12/201.13 inference(scs_inference,[],[2569,4989,4991,549,6563,5016,5069,897,5098,5065,1356,5025,47,343,854,4604,4625,820,4626,4420,93,13,87,90,86,84,81,85,15,12,2,148,9,8,92,105,3])). % 201.12/201.13 cnf(6696,plain, % 201.12/201.13 (~P13(f17(x66961),f9(f17(x66961)))), % 201.12/201.13 inference(rename_variables,[],[1031])). % 201.12/201.13 cnf(6698,plain, % 201.12/201.13 (P16(f9(f16(a2)),x66981)), % 201.12/201.13 inference(rename_variables,[],[897])). % 201.12/201.13 cnf(6700,plain, % 201.12/201.13 (P5(x67001,f16(x67001))), % 201.12/201.13 inference(rename_variables,[],[5090])). % 201.12/201.13 cnf(6704,plain, % 201.12/201.13 (P13(f9(f13(f6(a12))),f13(f6(a12)))), % 201.12/201.13 inference(scs_inference,[],[2569,4989,4991,549,6563,1031,6696,5016,5069,897,5022,5098,5065,1356,5025,43,61,5090,47,343,854,4604,4625,820,4626,4420,93,13,87,90,86,84,81,85,15,12,2,148,9,8,92,105,3,24,17,26,25,16,88])). % 201.12/201.13 cnf(6707,plain, % 201.12/201.13 (P16(f10(f17(a4),f17(a8)),a4)), % 201.12/201.13 inference(scs_inference,[],[2569,4989,4991,549,6563,1031,6696,944,5016,5069,897,5022,5098,5065,1356,5025,43,61,5090,47,343,854,4604,4625,820,4626,4420,93,13,87,90,86,84,81,85,15,12,2,148,9,8,92,105,3,24,17,26,25,16,88,106])). % 201.12/201.13 cnf(6708,plain, % 201.12/201.13 (P9(f17(x67081))), % 201.12/201.13 inference(rename_variables,[],[47])). % 201.12/201.13 cnf(6711,plain, % 201.12/201.13 (P5(x67111,f16(x67111))), % 201.12/201.13 inference(rename_variables,[],[5090])). % 201.12/201.13 cnf(6713,plain, % 201.12/201.13 (P5(x67131,f16(x67131))), % 201.12/201.13 inference(rename_variables,[],[5090])). % 201.12/201.13 cnf(6715,plain, % 201.12/201.13 (~P5(f17(x67151),f16(f15(x67152)))), % 201.12/201.13 inference(scs_inference,[],[6467,2569,4989,4991,6691,549,6563,1031,6696,944,5016,5069,897,5022,5098,5065,1356,5025,43,61,5090,6700,6711,47,343,854,4604,4625,820,4626,4420,93,13,87,90,86,84,81,85,15,12,2,148,9,8,92,105,3,24,17,26,25,16,88,106,27,100,99])). % 201.12/201.13 cnf(6717,plain, % 201.12/201.13 (P16(f9(f16(f17(a1))),f17(a2))), % 201.12/201.13 inference(scs_inference,[],[6467,2569,4989,4991,6691,549,6563,1031,6696,944,5016,5069,897,5022,5098,5065,1356,5025,43,61,5090,6700,6711,47,343,854,4604,4625,820,4626,4420,93,13,87,90,86,84,81,85,15,12,2,148,9,8,92,105,3,24,17,26,25,16,88,106,27,100,99,349])). % 201.12/201.13 cnf(6719,plain, % 201.12/201.13 (P5(f11(a1,x67191),f16(f11(a2,x67191)))), % 201.12/201.13 inference(scs_inference,[],[6467,2569,4989,4991,6691,549,6563,1031,6696,944,5016,5069,897,5022,5098,5065,5158,1356,5025,43,61,5090,6700,6711,6713,47,343,854,4604,4625,820,4626,4420,93,13,87,90,86,84,81,85,15,12,2,148,9,8,92,105,3,24,17,26,25,16,88,106,27,100,99,349,4609,5047])). % 201.12/201.13 cnf(6722,plain, % 201.12/201.13 (E(f9(f10(f17(a1),x67221)),f9(f10(f17(a2),x67221)))), % 201.12/201.13 inference(scs_inference,[],[6467,2569,4989,4991,6691,549,6563,1031,6696,944,5016,5069,897,5022,5098,5065,5158,1356,5025,43,61,5090,6700,6711,6713,47,343,854,4604,4625,820,4626,4420,93,13,87,90,86,84,81,85,15,12,2,148,9,8,92,105,3,24,17,26,25,16,88,106,27,100,99,349,4609,5047,837,871])). % 201.12/201.13 cnf(6727,plain, % 201.12/201.13 (P13(f10(f17(f7(a3)),f15(x67271)),f17(f7(a3)))), % 201.12/201.13 inference(scs_inference,[],[6467,2569,4989,4991,6691,549,6563,1031,6696,944,5016,5069,897,5022,5098,5065,5158,1356,5025,43,61,5090,6700,6711,6713,47,343,854,4604,4625,820,4626,4420,93,13,87,90,86,84,81,85,15,12,2,148,9,8,92,105,3,24,17,26,25,16,88,106,27,100,99,349,4609,5047,837,871,144,149,597,95])). % 201.12/201.13 cnf(6735,plain, % 201.12/201.13 (E(f6(f17(a1)),f6(f17(a2)))), % 201.12/201.13 inference(scs_inference,[],[6467,2569,4989,4991,6691,549,6563,1031,6696,944,5016,5069,897,5022,5098,5065,5158,1356,5025,43,61,5090,6700,6711,6713,47,343,854,4604,4625,820,4626,4420,93,13,87,90,86,84,81,85,15,12,2,148,9,8,92,105,3,24,17,26,25,16,88,106,27,100,99,349,4609,5047,837,871,144,149,597,95,79,83,80,11])). % 201.12/201.13 cnf(6736,plain, % 201.12/201.13 (P6(f7(f13(f6(a12))))), % 201.12/201.13 inference(scs_inference,[],[6467,2569,4989,4991,6691,549,6563,1031,6696,944,5016,5069,897,5022,5098,5065,5158,1356,5025,43,61,5090,6700,6711,6713,47,343,854,4604,4625,820,4626,4420,93,13,87,90,86,84,81,85,15,12,2,148,9,8,92,105,3,24,17,26,25,16,88,106,27,100,99,349,4609,5047,837,871,144,149,597,95,79,83,80,11,76])). % 201.12/201.13 cnf(6741,plain, % 201.12/201.13 (E(f11(x67411,f17(a1)),f11(x67411,f17(a2)))), % 201.12/201.13 inference(scs_inference,[],[6467,2569,4989,4991,6691,549,6563,1031,6696,944,5016,5069,897,5022,5098,5065,5158,1356,5025,43,61,5090,6700,6711,6713,47,343,854,4604,4625,820,4626,4420,93,13,87,90,86,84,81,85,15,12,2,148,9,8,92,105,3,24,17,26,25,16,88,106,27,100,99,349,4609,5047,837,871,144,149,597,95,79,83,80,11,76,6,75,7])). % 201.12/201.13 cnf(6742,plain, % 201.12/201.13 (E(f10(f17(a1),x67421),f10(f17(a2),x67421))), % 201.12/201.13 inference(scs_inference,[],[6467,2569,4989,4991,6691,549,6563,1031,6696,944,5016,5069,897,5022,5098,5065,5158,1356,5025,43,61,5090,6700,6711,6713,47,343,854,4604,4625,820,4626,4420,93,13,87,90,86,84,81,85,15,12,2,148,9,8,92,105,3,24,17,26,25,16,88,106,27,100,99,349,4609,5047,837,871,144,149,597,95,79,83,80,11,76,6,75,7,14])). % 201.12/201.13 cnf(6743,plain, % 201.12/201.13 (~P13(f10(f17(a3),f17(a2)),f17(a2))), % 201.12/201.13 inference(scs_inference,[],[6467,2569,4989,4991,6691,549,6563,1031,6696,5037,944,5016,5069,897,5022,5098,5065,5158,1356,5025,43,61,5090,6700,6711,6713,47,343,854,4604,4625,820,4626,4420,93,13,87,90,86,84,81,85,15,12,2,148,9,8,92,105,3,24,17,26,25,16,88,106,27,100,99,349,4609,5047,837,871,144,149,597,95,79,83,80,11,76,6,75,7,14,101])). % 201.12/201.13 cnf(6748,plain, % 201.12/201.13 (P16(f9(f16(f9(f16(a2)))),x67481)), % 201.12/201.13 inference(scs_inference,[],[6467,2569,4989,4991,6691,549,6563,1031,6696,5037,944,5016,5069,897,6698,5022,5098,5065,5158,1356,108,5025,43,61,5090,6700,6711,6713,47,343,854,4604,4625,820,4626,4420,93,13,87,90,86,84,81,85,15,12,2,148,9,8,92,105,3,24,17,26,25,16,88,106,27,100,99,349,4609,5047,837,871,144,149,597,95,79,83,80,11,76,6,75,7,14,101,10,3424,97])). % 201.12/201.13 cnf(6749,plain, % 201.12/201.13 (P16(f9(f16(x67491)),x67491)), % 201.12/201.13 inference(rename_variables,[],[108])). % 201.12/201.13 cnf(6755,plain, % 201.12/201.13 (P9(f17(x67551))), % 201.12/201.13 inference(rename_variables,[],[47])). % 201.12/201.13 cnf(6758,plain, % 201.12/201.13 (P16(f9(f17(a1)),a2)), % 201.12/201.13 inference(scs_inference,[],[6467,529,2569,4989,4991,6691,113,549,6563,1031,6696,5037,944,1028,5016,5069,897,6698,5022,5098,5065,5158,1356,108,6749,5025,43,61,5090,6700,6711,6713,60,47,6708,6755,343,854,4604,4625,820,4626,4420,93,13,87,90,86,84,81,85,15,12,2,148,9,8,92,105,3,24,17,26,25,16,88,106,27,100,99,349,4609,5047,837,871,144,149,597,95,79,83,80,11,76,6,75,7,14,101,10,3424,97,96,107,94])). % 201.12/201.13 cnf(6766,plain, % 201.12/201.13 (P13(f9(f16(a2)),f17(x67661))), % 201.12/201.13 inference(scs_inference,[],[6674,4267])). % 201.12/201.13 cnf(6768,plain, % 201.12/201.13 (P16(f11(a1,x67681),f11(a2,x67681))), % 201.12/201.13 inference(scs_inference,[],[6719,93])). % 201.12/201.13 cnf(6776,plain, % 201.12/201.13 (P6(f10(f17(f7(a3)),f15(x67761)))), % 201.12/201.13 inference(scs_inference,[],[5525,6715,6719,6574,6727,47,93,87,2,148,92,105])). % 201.12/201.13 cnf(6777,plain, % 201.12/201.13 (P9(f17(x67771))), % 201.12/201.13 inference(rename_variables,[],[47])). % 201.12/201.13 cnf(6779,plain, % 201.12/201.13 (E(f10(a2,f14(x67791)),f10(a2,a2))), % 201.12/201.13 inference(scs_inference,[],[5525,6693,6715,6719,6574,6727,4974,47,93,87,2,148,92,105,3])). % 201.12/201.13 cnf(6784,plain, % 201.12/201.13 (P16(x67841,x67841)), % 201.12/201.13 inference(rename_variables,[],[60])). % 201.12/201.13 cnf(6785,plain, % 201.12/201.13 (~E(f9(f7(a12)),f17(a12))), % 201.12/201.13 inference(scs_inference,[],[5525,6693,6715,6719,6574,6687,6727,6437,306,4974,61,60,47,93,87,2,148,92,105,3,24,17,26])). % 201.12/201.13 cnf(6786,plain, % 201.12/201.13 (P5(f9(x67861),x67861)), % 201.12/201.13 inference(rename_variables,[],[61])). % 201.12/201.13 cnf(6789,plain, % 201.12/201.13 (~P5(f17(f13(a3)),f13(a3))), % 201.12/201.13 inference(scs_inference,[],[5525,653,6693,6715,6719,6574,6687,6727,6437,306,5055,5111,4974,1356,61,60,47,93,87,2,148,92,105,3,24,17,26,25,88])). % 201.12/201.13 cnf(6791,plain, % 201.12/201.13 (~E(f14(x67911),f7(f17(a3)))), % 201.12/201.13 inference(scs_inference,[],[5525,653,6693,6715,6719,565,6574,6687,6727,6437,306,5055,5111,4974,1356,42,61,60,47,93,87,2,148,92,105,3,24,17,26,25,88,16])). % 201.12/201.13 cnf(6792,plain, % 201.12/201.13 (P16(f10(f17(f7(a3)),f15(x67921)),f7(a3))), % 201.12/201.13 inference(scs_inference,[],[5525,653,6693,6715,6719,565,6574,6687,6727,6437,306,5055,5111,4974,1356,42,61,60,47,6777,93,87,2,148,92,105,3,24,17,26,25,88,16,106])). % 201.12/201.13 cnf(6793,plain, % 201.12/201.13 (P9(f17(x67931))), % 201.12/201.13 inference(rename_variables,[],[47])). % 201.12/201.13 cnf(6795,plain, % 201.12/201.13 (P5(f9(f10(a1,f14(x67951))),f10(a2,a2))), % 201.12/201.13 inference(scs_inference,[],[5525,653,6693,6715,6719,565,6574,6687,6727,6437,306,5055,5111,4974,1356,42,61,6786,60,47,6777,93,87,2,148,92,105,3,24,17,26,25,88,16,106,27])). % 201.12/201.13 cnf(6801,plain, % 201.12/201.13 (P13(f7(f13(f6(a12))),f17(f7(f13(f6(a12)))))), % 201.12/201.13 inference(scs_inference,[],[5525,653,6693,6715,6719,565,6574,6687,6727,6736,6437,306,5222,5055,5111,4974,1356,42,61,6786,133,60,6784,47,6777,6793,93,87,2,148,92,105,3,24,17,26,25,88,16,106,27,100,99,107])). % 201.12/201.13 cnf(6820,plain, % 201.12/201.13 (P16(f11(a1,f17(a1)),f11(a2,f17(a2)))), % 201.12/201.13 inference(scs_inference,[],[6768,6779,6741,6722,6801,4214,93,87,2,148,92,18])). % 201.12/201.13 cnf(6824,plain, % 201.12/201.13 (~P13(f10(f17(a3),f17(a1)),f17(a2))), % 201.12/201.13 inference(scs_inference,[],[6768,6743,6779,6682,6741,6722,6801,4214,5041,93,87,2,148,92,18,3,24])). % 201.12/201.13 cnf(6829,plain, % 201.12/201.13 (P5(x68291,f16(x68291))), % 201.12/201.13 inference(rename_variables,[],[5090])). % 201.12/201.13 cnf(6830,plain, % 201.12/201.13 (~P5(f10(f17(a3),f17(a2)),f17(a2))), % 201.12/201.13 inference(scs_inference,[],[6768,6743,6779,6682,6741,6722,6748,6801,2613,4214,5041,69,5090,93,87,2,148,92,18,3,24,17,26,88])). % 201.12/201.13 cnf(6835,plain, % 201.12/201.13 (P16(f9(f17(x68351)),x68351)), % 201.12/201.13 inference(scs_inference,[],[6768,6743,6779,6682,6741,6678,6722,6748,6801,2613,4214,1028,5041,69,36,5016,5090,47,93,87,2,148,92,18,3,24,17,26,88,25,16,106])). % 201.12/201.13 cnf(6839,plain, % 201.12/201.13 (P5(x68391,f16(x68391))), % 201.12/201.13 inference(rename_variables,[],[5090])). % 201.12/201.13 cnf(6845,plain, % 201.12/201.13 (~E(f15(x68451),f10(f17(a3),f17(a2)))), % 201.12/201.13 inference(scs_inference,[],[6768,6743,6766,6779,6789,6682,6741,6678,6722,6748,6801,2613,4214,6578,1028,5041,69,36,5016,42,5090,6829,6839,47,93,87,2,148,92,18,3,24,17,26,88,25,16,106,27,100,99,4912])). % 201.12/201.13 cnf(6846,plain, % 201.12/201.13 (~E(f10(f17(f7(a3)),f15(x68461)),x68462)+P6(x68462)), % 201.12/201.13 inference(scs_inference,[],[6768,6743,6766,6779,6789,6776,6682,6741,6678,6722,6748,6801,2613,4214,6578,1028,5041,69,36,5016,42,5090,6829,6839,47,93,87,2,148,92,18,3,24,17,26,88,25,16,106,27,100,99,4912,19])). % 201.12/201.13 cnf(6858,plain, % 201.12/201.13 (~P13(f10(f17(a4),f17(a8)),f17(a8))), % 201.12/201.13 inference(scs_inference,[],[70,5158,6578,92,8,10,101])). % 201.12/201.13 cnf(6860,plain, % 201.12/201.13 (E(f10(f14(x68601),x68602),f10(a2,x68602))), % 201.12/201.13 inference(scs_inference,[],[70,5158,6578,92,8,10,101,14])). % 201.12/201.13 cnf(6863,plain, % 201.12/201.13 (E(f11(x68631,f14(x68632)),f11(x68631,a2))), % 201.12/201.13 inference(scs_inference,[],[70,5158,6693,6578,92,8,10,101,14,9,2,7])). % 201.12/201.13 cnf(6865,plain, % 201.12/201.13 (P6(f6(f17(x68651)))), % 201.12/201.13 inference(scs_inference,[],[70,69,5158,6693,6578,92,8,10,101,14,9,2,7,12,75])). % 201.12/201.13 cnf(6871,plain, % 201.12/201.13 (~P1(f7(f17(x68711)))), % 201.12/201.13 inference(scs_inference,[],[70,69,5158,6693,6578,92,8,10,101,14,9,2,7,12,75,15,6,76,81])). % 201.12/201.13 cnf(6875,plain, % 201.12/201.13 (~P1(f6(f17(x68751)))), % 201.12/201.13 inference(scs_inference,[],[70,69,5158,6693,6578,6830,92,8,10,101,14,9,2,7,12,75,15,6,76,81,4907,11,80])). % 201.12/201.13 cnf(6877,plain, % 201.12/201.13 (~P1(f13(f17(x68771)))), % 201.12/201.13 inference(scs_inference,[],[70,69,5158,6693,6578,6830,92,8,10,101,14,9,2,7,12,75,15,6,76,81,4907,11,80,79])). % 201.12/201.13 cnf(6883,plain, % 201.12/201.13 (P13(f10(f16(x68831),a1),f16(x68831))), % 201.12/201.13 inference(scs_inference,[],[70,69,5158,2629,6693,6096,6574,6578,6830,92,8,10,101,14,9,2,7,12,75,15,6,76,81,4907,11,80,79,90,87,95])). % 201.12/201.13 cnf(6893,plain, % 201.12/201.13 (P5(x68931,f16(x68931))), % 201.12/201.13 inference(rename_variables,[],[5090])). % 201.12/201.13 cnf(6894,plain, % 201.12/201.13 (~P13(a5,f17(f14(x68941)))), % 201.12/201.13 inference(scs_inference,[],[47,5090,5025,70,69,5158,277,5020,2629,6693,6096,6574,5189,6578,6277,6830,92,8,10,101,14,9,2,7,12,75,15,6,76,81,4907,11,80,79,90,87,95,13,93,597,343,4420,149,27,106])). % 201.12/201.13 cnf(6895,plain, % 201.12/201.13 (P9(f17(x68951))), % 201.12/201.13 inference(rename_variables,[],[47])). % 201.12/201.13 cnf(6897,plain, % 201.12/201.13 (P13(x68971,f16(x68971))), % 201.12/201.13 inference(scs_inference,[],[47,5090,6893,5025,70,69,5158,68,277,5020,2629,6693,6096,6574,5189,6578,6277,6830,92,8,10,101,14,9,2,7,12,75,15,6,76,81,4907,11,80,79,90,87,95,13,93,597,343,4420,149,27,106,88])). % 201.12/201.13 cnf(6902,plain, % 201.12/201.13 (P16(f10(a1,f14(x69021)),f10(a2,a1))), % 201.12/201.13 inference(scs_inference,[],[1357,47,5090,6893,5025,70,69,5158,68,277,5020,2629,5080,6693,6096,5736,6574,5189,6719,6578,6277,6830,92,8,10,101,14,9,2,7,12,75,15,6,76,81,4907,11,80,79,90,87,95,13,93,597,343,4420,149,27,106,88,26,17])). % 201.12/201.13 cnf(6903,plain, % 201.12/201.13 (E(f10(x69031,a1),f10(x69031,f14(x69032)))), % 201.12/201.13 inference(rename_variables,[],[1357])). % 201.12/201.13 cnf(6905,plain, % 201.12/201.13 (E(f10(x69051,a1),f10(x69051,f14(x69052)))), % 201.12/201.13 inference(rename_variables,[],[1357])). % 201.12/201.13 cnf(6906,plain, % 201.12/201.13 (~P1(f10(f17(a3),f17(a2)))), % 201.12/201.13 inference(scs_inference,[],[1357,6903,47,5090,6893,43,5025,70,5071,69,5158,68,277,5020,2629,5080,6693,6096,5736,6574,5189,6719,6578,6277,6830,6845,92,8,10,101,14,9,2,7,12,75,15,6,76,81,4907,11,80,79,90,87,95,13,93,597,343,4420,149,27,106,88,26,17,24,77])). % 201.12/201.13 cnf(6910,plain, % 201.12/201.13 (E(f10(x69101,a1),f10(x69101,f14(x69102)))), % 201.12/201.13 inference(rename_variables,[],[1357])). % 201.12/201.13 cnf(6911,plain, % 201.12/201.13 (P16(f10(x69111,a1),f10(x69111,f14(x69112)))), % 201.12/201.13 inference(scs_inference,[],[1357,6903,6905,6910,47,60,5125,5090,6893,43,5025,70,5071,69,5158,68,277,5020,2629,5080,6693,6096,5736,6574,5189,6719,6578,6277,6830,6845,92,8,10,101,14,9,2,7,12,75,15,6,76,81,4907,11,80,79,90,87,95,13,93,597,343,4420,149,27,106,88,26,17,24,77,3,18])). % 201.12/201.13 cnf(6913,plain, % 201.12/201.13 (P13(f9(f17(a1)),f17(a2))), % 201.12/201.13 inference(scs_inference,[],[1357,6903,6905,6910,47,6895,60,5125,5090,6893,43,5025,70,5071,69,5158,68,277,5020,2629,5080,6693,6096,5736,6574,5189,6719,6578,113,6277,6830,6845,6758,92,8,10,101,14,9,2,7,12,75,15,6,76,81,4907,11,80,79,90,87,95,13,93,597,343,4420,149,27,106,88,26,17,24,77,3,18,107])). % 201.12/201.13 cnf(6918,plain, % 201.12/201.13 (P5(f11(a1,a1),f16(f11(a2,a2)))), % 201.12/201.13 inference(scs_inference,[],[1357,6903,6905,6910,47,6895,60,5125,5090,6893,43,5025,70,5071,69,5158,68,277,5020,2629,5080,6693,6096,5736,6574,5189,6719,6578,113,6277,6830,6845,6758,92,8,10,101,14,9,2,7,12,75,15,6,76,81,4907,11,80,79,90,87,95,13,93,597,343,4420,149,27,106,88,26,17,24,77,3,18,107,5298,5047])). % 201.12/201.13 cnf(6921,plain, % 201.12/201.13 (~E(f16(a5),f17(a2))), % 201.12/201.13 inference(scs_inference,[],[1357,6903,6905,6910,47,6895,60,5125,5090,6893,43,5025,70,5071,69,5158,68,277,5020,2629,5080,6693,6096,5736,6574,5189,6719,6578,113,6277,6830,6845,6758,92,8,10,101,14,9,2,7,12,75,15,6,76,81,4907,11,80,79,90,87,95,13,93,597,343,4420,149,27,106,88,26,17,24,77,3,18,107,5298,5047,5874,5486])). % 201.12/201.13 cnf(6932,plain, % 201.12/201.13 (~P13(f10(f17(a3),f17(a1)),f17(a1))), % 201.12/201.13 inference(scs_inference,[],[1357,6727,2706,92,8,10,101])). % 201.12/201.13 cnf(6936,plain, % 201.12/201.13 (E(f10(x69361,f17(a2)),f10(x69361,f17(a1)))), % 201.12/201.13 inference(scs_inference,[],[1357,6727,6682,2706,92,8,10,101,14,9,2])). % 201.12/201.13 cnf(6939,plain, % 201.12/201.13 (P6(f6(f16(x69391)))), % 201.12/201.13 inference(scs_inference,[],[1357,68,6727,6682,2706,92,8,10,101,14,9,2,7,12,75])). % 201.12/201.13 cnf(6943,plain, % 201.12/201.13 (P6(f7(f16(x69431)))), % 201.12/201.13 inference(scs_inference,[],[1357,68,6727,6682,2706,92,8,10,101,14,9,2,7,12,75,15,6,76])). % 201.12/201.13 cnf(6948,plain, % 201.12/201.13 (~P1(f7(f16(x69481)))), % 201.12/201.13 inference(scs_inference,[],[1357,69,68,6727,6682,2706,92,8,10,101,14,9,2,7,12,75,15,6,76,85,11,81])). % 201.12/201.13 cnf(6951,plain, % 201.12/201.13 (P13(x69511,f16(x69511))), % 201.12/201.13 inference(rename_variables,[],[6897])). % 201.12/201.13 cnf(6952,plain, % 201.12/201.13 (P5(f6(f17(x69521)),f16(f17(x69521)))), % 201.12/201.13 inference(scs_inference,[],[1357,69,68,6727,6682,2706,6897,92,8,10,101,14,9,2,7,12,75,15,6,76,85,11,81,5260,84])). % 201.12/201.13 cnf(6954,plain, % 201.12/201.13 (~P1(f6(f16(x69541)))), % 201.12/201.13 inference(scs_inference,[],[1357,69,68,6727,6682,2706,6897,92,8,10,101,14,9,2,7,12,75,15,6,76,85,11,81,5260,84,80])). % 201.12/201.13 cnf(6956,plain, % 201.12/201.13 (P5(f13(f17(x69561)),f16(f17(x69561)))), % 201.12/201.13 inference(scs_inference,[],[1357,69,68,6727,6682,2706,6897,92,8,10,101,14,9,2,7,12,75,15,6,76,85,11,81,5260,84,80,83])). % 201.12/201.13 cnf(6958,plain, % 201.12/201.13 (~P1(f13(f16(x69581)))), % 201.12/201.13 inference(scs_inference,[],[1357,69,68,6727,6682,2706,6897,92,8,10,101,14,9,2,7,12,75,15,6,76,85,11,81,5260,84,80,83,79])). % 201.12/201.13 cnf(6964,plain, % 201.12/201.13 (E(f9(f10(x69641,a1)),f9(f10(x69641,f14(x69642))))), % 201.12/201.13 inference(scs_inference,[],[1357,69,68,5736,2663,6727,6682,2706,6897,92,8,10,101,14,9,2,7,12,75,15,6,76,85,11,81,5260,84,80,83,79,90,95,13])). % 201.12/201.13 cnf(6981,plain, % 201.12/201.13 (P13(x69811,f16(x69811))), % 201.12/201.13 inference(rename_variables,[],[6897])). % 201.12/201.13 cnf(6984,plain, % 201.12/201.13 (P13(x69841,f16(x69841))), % 201.12/201.13 inference(rename_variables,[],[6897])). % 201.12/201.13 cnf(6987,plain, % 201.12/201.13 (P13(x69871,f16(x69871))), % 201.12/201.13 inference(rename_variables,[],[6897])). % 201.12/201.13 cnf(6989,plain, % 201.12/201.13 (~E(f16(a3),f17(a2))), % 201.12/201.13 inference(scs_inference,[],[1357,69,68,5020,259,5736,2663,6727,5122,6682,5156,2706,6897,6951,6981,6984,6987,92,8,10,101,14,9,2,7,12,75,15,6,76,85,11,81,5260,84,80,83,79,90,95,13,87,597,93,149,343,871,349,854,4625,820,837,144,5855,5892,5813,5420])). % 201.12/201.13 cnf(7002,plain, % 201.12/201.13 (~P1(f10(f17(a3),f17(a1)))), % 201.12/201.13 inference(scs_inference,[],[1357,47,42,61,69,68,4974,5020,259,5736,2569,2663,6727,5122,6682,5156,2706,6897,6951,6981,6984,6987,6795,6906,92,8,10,101,14,9,2,7,12,75,15,6,76,85,11,81,5260,84,80,83,79,90,95,13,87,597,93,149,343,871,349,854,4625,820,837,144,5855,5892,5813,5420,99,100,27,106,16])). % 201.12/201.13 cnf(7027,plain, % 201.12/201.13 (~P13(f16(x70271),x70271)), % 201.12/201.13 inference(scs_inference,[],[6897,92])). % 201.12/201.13 cnf(7033,plain, % 201.12/201.13 (E(f10(f16(a2),x70331),f10(f16(a1),x70331))), % 201.12/201.13 inference(scs_inference,[],[4945,6897,4218,92,8,10,101,14])). % 201.12/201.13 cnf(7034,plain, % 201.12/201.13 (P5(f9(f10(x70341,f14(x70342))),f10(x70341,a1))), % 201.12/201.13 inference(scs_inference,[],[4945,6897,6964,4218,92,8,10,101,14,148])). % 201.12/201.13 cnf(7040,plain, % 201.12/201.13 (P6(f6(f6(a5)))), % 201.12/201.13 inference(scs_inference,[],[4945,4929,6741,6897,6964,4218,92,8,10,101,14,148,2,9,7,12,15,75])). % 201.12/201.13 cnf(7045,plain, % 201.12/201.13 (P5(f7(f16(x70451)),f16(f16(x70451)))), % 201.12/201.13 inference(scs_inference,[],[4945,68,4929,6741,6897,6964,4218,92,8,10,101,14,148,2,9,7,12,15,75,6,76,85])). % 201.12/201.13 cnf(7048,plain, % 201.12/201.13 (~P1(f7(f6(a5)))), % 201.12/201.13 inference(scs_inference,[],[4945,68,4929,6741,6897,6964,4218,92,8,10,101,14,148,2,9,7,12,15,75,6,76,85,11,81])). % 201.12/201.13 cnf(7050,plain, % 201.12/201.13 (P5(f6(f16(x70501)),f16(f16(x70501)))), % 201.12/201.13 inference(scs_inference,[],[4945,68,4929,6741,6897,6964,4218,92,8,10,101,14,148,2,9,7,12,15,75,6,76,85,11,81,84])). % 201.12/201.13 cnf(7052,plain, % 201.12/201.13 (~P1(f6(f6(a5)))), % 201.12/201.13 inference(scs_inference,[],[4945,68,4929,6741,6897,6964,4218,92,8,10,101,14,148,2,9,7,12,15,75,6,76,85,11,81,84,80])). % 201.12/201.13 cnf(7054,plain, % 201.12/201.13 (P5(f13(f16(x70541)),f16(f16(x70541)))), % 201.12/201.13 inference(scs_inference,[],[4945,68,4929,6741,6897,6964,4218,92,8,10,101,14,148,2,9,7,12,15,75,6,76,85,11,81,84,80,83])). % 201.12/201.13 cnf(7056,plain, % 201.12/201.13 (~P1(f13(f6(a5)))), % 201.12/201.13 inference(scs_inference,[],[4945,68,4929,6741,6897,6964,4218,92,8,10,101,14,148,2,9,7,12,15,75,6,76,85,11,81,84,80,83,79])). % 201.12/201.13 cnf(7059,plain, % 201.12/201.13 (P5(f6(a2),f16(f6(a1)))), % 201.12/201.13 inference(scs_inference,[],[4945,68,4929,6085,6741,6897,6964,4218,92,8,10,101,14,148,2,9,7,12,15,75,6,76,85,11,81,84,80,83,79,13,90])). % 201.12/201.13 cnf(7061,plain, % 201.12/201.13 (P13(f10(f16(x70611),a2),f16(x70611))), % 201.12/201.13 inference(scs_inference,[],[4945,68,4929,2670,6085,6741,6897,6964,4218,92,8,10,101,14,148,2,9,7,12,15,75,6,76,85,11,81,84,80,83,79,13,90,95])). % 201.12/201.13 cnf(7071,plain, % 201.12/201.13 (E(f9(f10(f16(a2),x70711)),f9(f10(f16(a1),x70711)))), % 201.12/201.13 inference(scs_inference,[],[4945,5158,68,4929,2670,6085,2706,6741,6897,6563,5119,6964,4218,92,8,10,101,14,148,2,9,7,12,15,75,6,76,85,11,81,84,80,83,79,13,90,95,87,597,93,343,149,349,871])). % 201.12/201.13 cnf(7075,plain, % 201.12/201.13 (~P13(f16(a8),a4)), % 201.12/201.13 inference(scs_inference,[],[4945,5158,68,4929,2670,6085,2706,6741,6897,6563,5119,6964,4218,92,8,10,101,14,148,2,9,7,12,15,75,6,76,85,11,81,84,80,83,79,13,90,95,87,597,93,343,149,349,871,837,820,854,5088])). % 201.12/201.13 cnf(7107,plain, % 201.12/201.13 (E(f16(f16(a1)),f16(f16(a2)))), % 201.12/201.13 inference(scs_inference,[],[5025,6704,92,8])). % 201.12/201.13 cnf(7122,plain, % 201.12/201.13 (P5(f7(f6(a5)),f16(f6(a5)))), % 201.12/201.13 inference(scs_inference,[],[5025,4929,4974,4927,6742,6704,7071,92,8,10,14,148,7,9,2,12,15,75,6,76,11,85])). % 201.12/201.13 cnf(7124,plain, % 201.12/201.13 (~P1(f7(f13(a5)))), % 201.12/201.13 inference(scs_inference,[],[5025,4929,4974,4927,6742,6704,7071,92,8,10,14,148,7,9,2,12,15,75,6,76,11,85,81])). % 201.12/201.13 cnf(7126,plain, % 201.12/201.13 (P5(f6(f6(a5)),f16(f6(a5)))), % 201.12/201.13 inference(scs_inference,[],[5025,4929,4974,4927,6742,6704,7071,92,8,10,14,148,7,9,2,12,15,75,6,76,11,85,81,84])). % 201.12/201.13 cnf(7128,plain, % 201.12/201.13 (~P1(f6(f13(a5)))), % 201.12/201.13 inference(scs_inference,[],[5025,4929,4974,4927,6742,6704,7071,92,8,10,14,148,7,9,2,12,15,75,6,76,11,85,81,84,80])). % 201.12/201.13 cnf(7130,plain, % 201.12/201.13 (P5(f13(f6(a5)),f16(f6(a5)))), % 201.12/201.13 inference(scs_inference,[],[5025,4929,4974,4927,6742,6704,7071,92,8,10,14,148,7,9,2,12,15,75,6,76,11,85,81,84,80,83])). % 201.12/201.13 cnf(7132,plain, % 201.12/201.13 (~P1(f13(f13(a5)))), % 201.12/201.13 inference(scs_inference,[],[5025,4929,4974,4927,6742,6704,7071,92,8,10,14,148,7,9,2,12,15,75,6,76,11,85,81,84,80,83,79])). % 201.12/201.13 cnf(7137,plain, % 201.12/201.13 (P13(f10(a5,f15(x71371)),a5)), % 201.12/201.13 inference(scs_inference,[],[5025,4929,4974,4927,6094,5156,6742,6704,7071,92,8,10,14,148,7,9,2,12,15,75,6,76,11,85,81,84,80,83,79,13,90,95])). % 201.12/201.13 cnf(7139,plain, % 201.12/201.13 (P5(f10(f16(x71391),a2),f16(x71391))), % 201.12/201.13 inference(scs_inference,[],[5025,4929,4974,4927,6094,5156,6742,6704,7071,7061,92,8,10,14,148,7,9,2,12,15,75,6,76,11,85,81,84,80,83,79,13,90,95,87])). % 201.12/201.13 cnf(7147,plain, % 201.12/201.13 (P16(f9(f16(f14(x71471))),a2)), % 201.12/201.13 inference(scs_inference,[],[5158,5025,4929,4974,4927,6094,5156,6742,6704,5076,5096,7071,7061,92,8,10,14,148,7,9,2,12,15,75,6,76,11,85,81,84,80,83,79,13,90,95,87,597,149,343,93,837,349])). % 201.12/201.13 cnf(7148,plain, % 201.12/201.13 (E(f9(f10(f14(x71481),x71482)),f9(f10(a2,x71482)))), % 201.12/201.13 inference(scs_inference,[],[5158,5025,4929,4974,4927,6094,5156,6742,6704,5076,5096,7071,7061,92,8,10,14,148,7,9,2,12,15,75,6,76,11,85,81,84,80,83,79,13,90,95,87,597,149,343,93,837,349,871])). % 201.12/201.13 cnf(7154,plain, % 201.12/201.13 (~P13(f16(x71541),x71541)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7156,plain, % 201.12/201.13 (~P13(f16(x71561),x71561)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7158,plain, % 201.12/201.13 (~P13(f16(x71581),x71581)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7161,plain, % 201.12/201.13 (~P13(f16(x71611),x71611)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7164,plain, % 201.12/201.13 (~P13(f16(x71641),x71641)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7167,plain, % 201.12/201.13 (~P13(f16(x71671),x71671)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7170,plain, % 201.12/201.13 (~P13(f16(x71701),x71701)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7173,plain, % 201.12/201.13 (~P13(f16(x71731),x71731)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7176,plain, % 201.12/201.13 (~P13(f16(x71761),x71761)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7178,plain, % 201.12/201.13 (~P13(f16(x71781),x71781)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7180,plain, % 201.12/201.13 (~P13(f16(f10(a2,x71801)),f10(a1,x71801))), % 201.12/201.13 inference(scs_inference,[],[5158,5025,4929,4974,4927,6094,5156,5126,6742,6704,5076,5096,7071,7061,7027,7154,7156,7158,7161,7164,7167,7170,7173,7176,7178,92,8,10,14,148,7,9,2,12,15,75,6,76,11,85,81,84,80,83,79,13,90,95,87,597,149,343,93,837,349,871,854,820,144,5438,5248,6321,6301,6268,6251,6211,6196,5821,5816,5792])). % 201.12/201.13 cnf(7181,plain, % 201.12/201.13 (~P13(f16(x71811),x71811)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7182,plain, % 201.12/201.13 (~P13(f16(f11(a1,x71821)),f11(a2,x71821))), % 201.12/201.13 inference(scs_inference,[],[5158,5025,4929,4974,4927,6094,5156,5126,6742,6704,5076,5096,7071,7061,7027,7154,7156,7158,7161,7164,7167,7170,7173,7176,7178,7181,92,8,10,14,148,7,9,2,12,15,75,6,76,11,85,81,84,80,83,79,13,90,95,87,597,149,343,93,837,349,871,854,820,144,5438,5248,6321,6301,6268,6251,6211,6196,5821,5816,5792,5782])). % 201.12/201.13 cnf(7183,plain, % 201.12/201.13 (~P13(f16(x71831),x71831)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7185,plain, % 201.12/201.13 (~P13(f16(x71851),x71851)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7188,plain, % 201.12/201.13 (~P13(f16(x71881),x71881)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7190,plain, % 201.12/201.13 (~P13(f16(x71901),x71901)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7192,plain, % 201.12/201.13 (~P13(f16(x71921),x71921)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7195,plain, % 201.12/201.13 (~P13(f16(x71951),x71951)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7197,plain, % 201.12/201.13 (~P13(f16(x71971),x71971)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7199,plain, % 201.12/201.13 (~P13(f16(x71991),x71991)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7201,plain, % 201.12/201.13 (~P13(f16(x72011),x72011)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7203,plain, % 201.12/201.13 (~P13(f16(x72031),x72031)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7205,plain, % 201.12/201.13 (~P13(f16(x72051),x72051)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7207,plain, % 201.12/201.13 (~P13(f16(x72071),x72071)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7210,plain, % 201.12/201.13 (~P13(f16(x72101),x72101)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7212,plain, % 201.12/201.13 (~P13(f16(x72121),x72121)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7214,plain, % 201.12/201.13 (~P13(f16(x72141),x72141)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7216,plain, % 201.12/201.13 (~P13(f16(x72161),x72161)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7217,plain, % 201.12/201.13 (~P13(f16(f10(a1,a2)),f10(a2,a1))), % 201.12/201.13 inference(scs_inference,[],[5158,5025,4929,4974,4927,6094,5156,5126,6742,6704,5076,5096,7071,7061,7027,7154,7156,7158,7161,7164,7167,7170,7173,7176,7178,7181,7183,7185,7188,7190,7192,7195,7197,7199,7201,7203,7205,7207,7210,7212,7214,7216,92,8,10,14,148,7,9,2,12,15,75,6,76,11,85,81,84,80,83,79,13,90,95,87,597,149,343,93,837,349,871,854,820,144,5438,5248,6321,6301,6268,6251,6211,6196,5821,5816,5792,5782,5776,5761,5728,5720,5718,5677,5658,5634,5592,5567,5397,5377,5323,5307,5268,5217])). % 201.12/201.13 cnf(7278,plain, % 201.12/201.13 (P5(f6(f6(a12)),f16(f6(a12)))), % 201.12/201.13 inference(scs_inference,[],[1356,4927,4975,4999,6687,7061,7148,92,8,10,14,148,7,2,9,12,15,6,75,76,11,85,81,84])). % 201.12/201.13 cnf(7289,plain, % 201.12/201.13 (P13(f10(f17(a3),f17(a1)),f17(a3))), % 201.12/201.13 inference(scs_inference,[],[1356,4927,4975,4999,5008,2706,166,6687,7061,7148,92,8,10,14,148,7,2,9,12,15,6,75,76,11,85,81,84,80,83,79,13,90,95])). % 201.12/201.13 cnf(7296,plain, % 201.12/201.13 (~P13(f16(x72961),x72961)), % 201.12/201.13 inference(rename_variables,[],[7027])). % 201.12/201.13 cnf(7302,plain, % 201.12/201.13 (E(f9(f10(f16(a1),x73021)),f9(f10(f16(a2),x73021)))), % 201.12/201.13 inference(scs_inference,[],[5025,1356,4927,5017,4975,4999,5008,2706,166,6687,7027,7061,4218,7148,7137,92,8,10,14,148,7,2,9,12,15,6,75,76,11,85,81,84,80,83,79,13,90,95,87,597,837,343,149,854,93,349,871])). % 201.12/201.13 cnf(7310,plain, % 201.12/201.13 (~P13(f16(f10(a2,x73101)),f10(a1,x73101))), % 201.12/201.13 inference(rename_variables,[],[7180])). % 201.12/201.13 cnf(7315,plain, % 201.12/201.13 (P5(f10(f16(x73151),a2),f16(x73151))), % 201.12/201.13 inference(rename_variables,[],[7139])). % 201.12/201.13 cnf(7320,plain, % 201.12/201.13 (P9(f17(x73201))), % 201.12/201.13 inference(rename_variables,[],[47])). % 201.12/201.13 cnf(7327,plain, % 201.12/201.13 (P16(f10(a2,f14(x73271)),f10(a1,a1))), % 201.12/201.13 inference(scs_inference,[],[1357,47,5025,5090,68,1356,4927,259,5017,4975,4999,5008,2706,166,6952,6687,5076,5023,5247,7027,6795,7061,4218,7148,7137,7217,7180,7310,7182,7139,92,8,10,14,148,7,2,9,12,15,6,75,76,11,85,81,84,80,83,79,13,90,95,87,597,837,343,149,854,93,349,871,820,5438,144,5792,5720,5728,100,27,106,26,88,17])). % 201.12/201.13 cnf(7328,plain, % 201.12/201.13 (E(f10(x73281,a1),f10(x73281,f14(x73282)))), % 201.12/201.13 inference(rename_variables,[],[1357])). % 201.12/201.13 cnf(7334,plain, % 201.12/201.13 (~E(a2,f7(f17(a3)))), % 201.12/201.13 inference(scs_inference,[],[1357,47,5025,5158,5090,68,5138,1356,37,4927,259,5017,4975,4999,5008,2706,166,6952,6687,5076,5023,5247,7027,7296,6795,7061,4218,7148,7137,7217,7180,7310,7182,6791,7139,7315,92,8,10,14,148,7,2,9,12,15,6,75,76,11,85,81,84,80,83,79,13,90,95,87,597,837,343,149,854,93,349,871,820,5438,144,5792,5720,5728,100,27,106,26,88,17,91,24,3])). % 201.12/201.13 cnf(7338,plain, % 201.12/201.13 (P13(f10(f16(a3),a2),f17(f10(f16(a3),a1)))), % 201.12/201.13 inference(scs_inference,[],[1357,7328,47,7320,5025,5158,5090,68,5138,1356,37,4927,259,5017,4975,4999,5008,6096,2706,166,6952,6687,5076,5023,5247,7027,7296,6795,7061,4218,7148,7137,7217,7180,7310,7182,6791,7139,7315,92,8,10,14,148,7,2,9,12,15,6,75,76,11,85,81,84,80,83,79,13,90,95,87,597,837,343,149,854,93,349,871,820,5438,144,5792,5720,5728,100,27,106,26,88,17,91,24,3,18,107])). % 201.12/201.13 cnf(7343,plain, % 201.12/201.13 (P6(f10(f16(a3),a1))), % 201.12/201.13 inference(scs_inference,[],[1357,7328,47,7320,5025,5158,5090,68,5138,1356,37,4927,259,5017,4975,4999,5008,6096,2706,166,6952,6687,5076,5023,5247,7027,7296,6795,7061,4218,7148,7137,7217,7180,7310,7182,6791,7139,7315,92,8,10,14,148,7,2,9,12,15,6,75,76,11,85,81,84,80,83,79,13,90,95,87,597,837,343,149,854,93,349,871,820,5438,144,5792,5720,5728,100,27,106,26,88,17,91,24,3,18,107,29,19])). % 201.12/201.13 cnf(7366,plain, % 201.12/201.13 (P5(f7(f6(a12)),f16(f6(a12)))), % 201.12/201.13 inference(scs_inference,[],[4974,4999,5201,5008,6735,7137,7302,92,8,10,14,148,7,9,2,12,15,6,75,76,11,85])). % 201.12/201.13 cnf(7370,plain, % 201.12/201.13 (P5(f6(f7(a12)),f16(f7(a12)))), % 201.12/201.13 inference(scs_inference,[],[4974,4999,5201,5008,6735,7137,7302,92,8,10,14,148,7,9,2,12,15,6,75,76,11,85,81,84])). % 201.12/201.13 cnf(7381,plain, % 201.12/201.13 (P13(f10(f16(x73811),f14(x73812)),f16(x73811))), % 201.12/201.13 inference(scs_inference,[],[4974,4999,5201,5008,4931,5076,6735,7137,7302,7289,92,8,10,14,148,7,9,2,12,15,6,75,76,11,85,81,84,80,83,79,13,87,95])). % 201.12/201.13 cnf(7385,plain, % 201.12/201.13 (P6(f10(f17(a3),f17(a1)))), % 201.12/201.13 inference(scs_inference,[],[4974,4999,5201,5008,4931,5247,5076,6735,7137,7302,7289,92,8,10,14,148,7,9,2,12,15,6,75,76,11,85,81,84,80,83,79,13,87,95,90,86])). % 201.12/201.13 cnf(7388,plain, % 201.12/201.13 (P5(f9(f10(x73881,a2)),f10(x73881,a1))), % 201.12/201.13 inference(scs_inference,[],[4974,4999,4975,5201,5008,4931,5247,5076,6735,7137,7302,7289,92,8,10,14,148,7,9,2,12,15,6,75,76,11,85,81,84,80,83,79,13,87,95,90,86,597,149])). % 201.12/201.13 cnf(7392,plain, % 201.12/201.13 (E(f9(f10(f10(x73921,f14(x73922)),x73923)),f9(f10(f10(x73921,a1),x73923)))), % 201.12/201.13 inference(scs_inference,[],[1356,4974,4999,4975,5201,5008,4931,5247,5076,6735,7137,4946,7302,7289,92,8,10,14,148,7,9,2,12,15,6,75,76,11,85,81,84,80,83,79,13,87,95,90,86,597,149,854,343,837,871])). % 201.12/201.13 cnf(7393,plain, % 201.12/201.13 (P16(f9(f16(f10(x73931,f14(x73932)))),f10(x73931,a1))), % 201.12/201.13 inference(scs_inference,[],[1356,4974,4999,4975,5201,5008,4931,5247,5076,6735,7137,4946,7302,7289,92,8,10,14,148,7,9,2,12,15,6,75,76,11,85,81,84,80,83,79,13,87,95,90,86,597,149,854,343,837,871,349])). % 201.12/201.13 cnf(7403,plain, % 201.12/201.13 (P5(f10(f16(a2),a2),f16(a1))), % 201.12/201.13 inference(scs_inference,[],[4945,1356,4974,4999,4975,5201,5008,4931,5247,6715,5076,6735,6789,7139,7137,4946,7302,7289,7045,7343,4224,92,8,10,14,148,7,9,2,12,15,6,75,76,11,85,81,84,80,83,79,13,87,95,90,86,597,149,854,343,837,871,349,93,820,144,1380,100,27])). % 201.12/201.13 cnf(7404,plain, % 201.12/201.13 (P5(f10(f16(x74041),a2),f16(x74041))), % 201.12/201.13 inference(rename_variables,[],[7139])). % 201.12/201.13 cnf(7405,plain, % 201.12/201.13 (P6(f10(f17(a3),f17(a2)))), % 201.12/201.13 inference(scs_inference,[],[4945,1356,4974,4999,4975,5201,5008,4931,5247,6682,6715,5076,6735,6789,7139,7137,4946,7302,7289,7045,7343,4224,92,8,10,14,148,7,9,2,12,15,6,75,76,11,85,81,84,80,83,79,13,87,95,90,86,597,149,854,343,837,871,349,93,820,144,1380,100,27,19])). % 201.12/201.13 cnf(7408,plain, % 201.12/201.13 (P9(f17(x74081))), % 201.12/201.13 inference(rename_variables,[],[47])). % 201.12/201.13 cnf(7410,plain, % 201.12/201.13 (P5(f10(f16(x74101),a1),f16(x74101))), % 201.12/201.13 inference(scs_inference,[],[47,4945,1356,4974,4999,4975,5201,5008,4931,5247,6682,6715,5076,6735,6789,7139,7404,7137,4214,4946,7302,7289,7045,7343,4224,92,8,10,14,148,7,9,2,12,15,6,75,76,11,85,81,84,80,83,79,13,87,95,90,86,597,149,854,343,837,871,349,93,820,144,1380,100,27,19,106,26])). % 201.12/201.13 cnf(7413,plain, % 201.12/201.13 (E(f10(x74131,a1),f10(x74131,f14(x74132)))), % 201.12/201.13 inference(rename_variables,[],[1357])). % 201.12/201.13 cnf(7419,plain, % 201.12/201.13 (~E(f10(a5,a1),f16(a5))), % 201.12/201.13 inference(scs_inference,[],[1357,47,4945,1356,68,5071,4974,4999,4975,5201,5008,4931,5010,5247,6682,6715,5076,7027,5181,6735,6789,7139,7404,6956,7137,4214,4946,7302,7289,7045,7343,4224,92,8,10,14,148,7,9,2,12,15,6,75,76,11,85,81,84,80,83,79,13,87,95,90,86,597,149,854,343,837,871,349,93,820,144,1380,100,27,19,106,26,17,88,91,24])). % 201.12/201.13 cnf(7424,plain, % 201.12/201.13 (P13(f10(f16(a3),a1),f17(f10(f16(a3),a2)))), % 201.12/201.13 inference(scs_inference,[],[1357,7413,47,7408,4945,1356,68,5071,4974,4999,4975,4941,5201,5008,4931,5010,6094,5247,6682,6715,5076,7027,5181,6735,6789,7139,7404,6956,7137,4214,4946,7302,7289,7334,7045,7343,6902,4224,92,8,10,14,148,7,9,2,12,15,6,75,76,11,85,81,84,80,83,79,13,87,95,90,86,597,149,854,343,837,871,349,93,820,144,1380,100,27,19,106,26,17,88,91,24,3,18,107])). % 201.12/201.13 cnf(7426,plain, % 201.12/201.13 (P9(f17(x74261))), % 201.12/201.13 inference(rename_variables,[],[47])). % 201.12/201.13 cnf(7428,plain, % 201.12/201.13 (~P16(f10(f17(a3),f17(a2)),a1)), % 201.12/201.13 inference(scs_inference,[],[1357,7413,47,7408,7426,4945,1356,68,5071,4974,4999,4975,4977,4941,5201,5008,4931,5010,6743,6094,5247,6682,6715,5076,7027,5181,6735,6789,7139,7404,6956,7137,4214,4946,7302,7289,7334,7045,7343,6902,4224,92,8,10,14,148,7,9,2,12,15,6,75,76,11,85,81,84,80,83,79,13,87,95,90,86,597,149,854,343,837,871,349,93,820,144,1380,100,27,19,106,26,17,88,91,24,3,18,107,98])). % 201.12/201.13 cnf(7461,plain, % 201.12/201.13 (P5(f13(f7(a12)),f16(f7(a12)))), % 201.12/201.13 inference(scs_inference,[],[4975,5008,5020,4931,7148,7289,7392,92,8,10,14,148,7,9,2,12,15,6,75,76,11,85,81,84,80,83])). % 201.12/201.13 cnf(7463,plain, % 201.12/201.13 (E(f9(f10(x74631,a2)),f9(f10(x74631,a1)))), % 201.12/201.13 inference(scs_inference,[],[4975,5008,5020,4931,7148,7289,7392,92,8,10,14,148,7,9,2,12,15,6,75,76,11,85,81,84,80,83,13])). % 201.12/201.13 cnf(7466,plain, % 201.12/201.13 (P5(f10(f16(x74661),f14(x74662)),f16(x74661))), % 201.12/201.13 inference(scs_inference,[],[4975,5008,5020,4931,5055,7148,7289,7392,7381,92,8,10,14,148,7,9,2,12,15,6,75,76,11,85,81,84,80,83,13,79,87])). % 201.12/201.13 cnf(7468,plain, % 201.12/201.13 (P13(f10(f17(f13(a3)),f15(x74681)),f17(f13(a3)))), % 201.12/201.13 inference(scs_inference,[],[4975,5008,5020,4931,5055,2613,7148,7289,7392,7381,92,8,10,14,148,7,9,2,12,15,6,75,76,11,85,81,84,80,83,13,79,87,95])). % 201.12/201.13 cnf(7477,plain, % 201.12/201.13 (P16(f9(f16(f10(a2,x74771))),f10(a1,x74771))), % 201.12/201.13 inference(scs_inference,[],[4974,4975,5008,5020,4931,5055,5726,2613,7148,7289,4960,7392,7381,92,8,10,14,148,7,9,2,12,15,6,75,76,11,85,81,84,80,83,13,79,87,95,90,597,149,343,854,837,349])). % 201.12/201.13 cnf(7478,plain, % 201.12/201.13 (E(f9(f10(f10(a2,x74781),x74782)),f9(f10(f10(a1,x74781),x74782)))), % 201.12/201.13 inference(scs_inference,[],[4974,4975,5008,5020,4931,5055,5726,2613,7148,7289,4960,7392,7381,92,8,10,14,148,7,9,2,12,15,6,75,76,11,85,81,84,80,83,13,79,87,95,90,597,149,343,854,837,349,871])). % 201.12/201.13 cnf(7479,plain, % 201.12/201.13 (~P5(f10(f17(a3),f17(a2)),f16(a1))), % 201.12/201.13 inference(scs_inference,[],[4974,4975,5008,5020,4931,5055,5726,2613,7148,7289,4960,7392,7381,7428,92,8,10,14,148,7,9,2,12,15,6,75,76,11,85,81,84,80,83,13,79,87,95,90,597,149,343,854,837,349,871,93])). % 201.12/201.13 cnf(7485,plain, % 201.12/201.13 (P5(f13(f17(x74851)),f16(f17(x74851)))), % 201.12/201.13 inference(rename_variables,[],[6956])). % 201.12/201.13 cnf(7487,plain, % 201.12/201.13 (P5(f10(f16(x74871),a1),f16(x74871))), % 201.12/201.13 inference(rename_variables,[],[7410])). % 201.12/201.13 cnf(7502,plain, % 201.12/201.13 (P6(f10(f16(a2),a2))), % 201.12/201.13 inference(scs_inference,[],[47,4974,68,42,70,4975,5008,259,5020,4931,5055,6687,5726,6956,7485,2613,4949,7148,7289,7045,6748,4224,6437,4960,6683,7392,7381,7428,7410,7487,7403,92,8,10,14,148,7,9,2,12,15,6,75,76,11,85,81,84,80,83,13,79,87,95,90,597,149,343,854,837,349,871,93,820,144,27,99,100,106,26,88,17,91])). % 201.12/201.13 cnf(7522,plain, % 201.12/201.13 (P5(f9(f10(x75221,a1)),f10(x75221,a2))), % 201.12/201.13 inference(scs_inference,[],[5201,5065,7381,7463,92,8,10,14,148])). % 201.12/201.13 cnf(7527,plain, % 201.12/201.13 (E(f10(x75271,a2),f10(x75271,f15(x75272)))), % 201.12/201.13 inference(scs_inference,[],[5201,5065,6683,7381,7463,92,8,10,14,148,9,7,12,2,15])). % 201.12/201.13 cnf(7540,plain, % 201.12/201.13 (P5(f13(f7(a5)),f16(f7(a5)))), % 201.12/201.13 inference(scs_inference,[],[4931,5201,5055,5065,6683,7381,7463,92,8,10,14,148,9,7,12,2,15,6,75,76,11,85,81,84,83])). % 201.12/201.13 cnf(7545,plain, % 201.12/201.13 (~P1(f13(f13(a12)))), % 201.12/201.13 inference(scs_inference,[],[4931,5201,5055,5065,4995,6683,7381,7463,92,8,10,14,148,9,7,12,2,15,6,75,76,11,85,81,84,83,80,13,79])). % 201.12/201.13 cnf(7549,plain, % 201.12/201.13 (P13(f10(f17(a3),f9(f16(a2))),f17(a3))), % 201.12/201.13 inference(scs_inference,[],[4931,5201,5055,5065,4995,4214,6683,7381,7463,7468,92,8,10,14,148,9,7,12,2,15,6,75,76,11,85,81,84,83,80,13,79,87,95])). % 201.12/201.13 cnf(7559,plain, % 201.12/201.13 (P16(f9(f16(f10(x75591,a2))),f10(x75591,a1))), % 201.12/201.13 inference(scs_inference,[],[4975,4931,5201,5055,5136,5065,4995,5612,4214,6683,7381,7463,7468,92,8,10,14,148,9,7,12,2,15,6,75,76,11,85,81,84,83,80,13,79,87,95,90,86,597,149,837,854,349])). % 201.12/201.13 cnf(7560,plain, % 201.12/201.13 (E(f9(f10(f10(x75601,a2),x75602)),f9(f10(f10(x75601,a1),x75602)))), % 201.12/201.13 inference(scs_inference,[],[4975,4931,5201,5055,5136,5065,4995,5612,4214,6683,7381,7463,7468,92,8,10,14,148,9,7,12,2,15,6,75,76,11,85,81,84,83,80,13,79,87,95,90,86,597,149,837,854,349,871])). % 201.12/201.13 cnf(7570,plain, % 201.12/201.13 (P5(f10(f16(x75701),f14(x75702)),f16(x75701))), % 201.12/201.13 inference(rename_variables,[],[7466])). % 201.12/201.13 cnf(7576,plain, % 201.12/201.13 (E(f10(x75761,a2),f10(x75761,a1))), % 201.12/201.13 inference(rename_variables,[],[4975])). % 201.12/201.13 cnf(7578,plain, % 201.12/201.13 (P9(f17(x75781))), % 201.12/201.13 inference(rename_variables,[],[47])). % 201.12/201.13 cnf(7580,plain, % 201.12/201.13 (P5(f10(f16(a2),a1),f16(a1))), % 201.12/201.13 inference(scs_inference,[],[47,42,4975,7576,259,4931,5201,5055,5136,5065,4995,5612,7045,4214,6683,7403,7381,6830,5188,7463,7468,7466,7570,7502,7107,5224,92,8,10,14,148,9,7,12,2,15,6,75,76,11,85,81,84,83,80,13,79,87,95,90,86,597,149,837,854,349,871,93,820,144,5047,27,100,99,19,106,26])). % 201.12/201.13 cnf(7582,plain, % 201.12/201.13 (~E(f9(f17(a1)),f17(x75821))), % 201.12/201.13 inference(scs_inference,[],[47,42,4975,7576,259,4931,5201,5055,5136,5065,4995,2663,5612,7045,6758,4214,6683,7403,7381,6830,5188,7463,7468,7466,7570,7502,7107,5224,92,8,10,14,148,9,7,12,2,15,6,75,76,11,85,81,84,83,80,13,79,87,95,90,86,597,149,837,854,349,871,93,820,144,5047,27,100,99,19,106,26,17])). % 201.12/201.13 cnf(7591,plain, % 201.12/201.13 (E(f10(x75911,a1),f10(x75911,f14(x75912)))), % 201.12/201.13 inference(rename_variables,[],[1357])). % 201.12/201.13 cnf(7592,plain, % 201.12/201.13 (P16(f9(f16(f10(x75921,f14(x75922)))),f10(x75921,f14(x75923)))), % 201.12/201.13 inference(scs_inference,[],[1357,7591,47,68,42,4975,7576,259,4931,5201,5055,5136,674,5065,4995,7027,2663,5012,5612,7045,6758,4214,6683,7403,7381,6830,5188,7463,7468,7419,7466,7570,7461,7502,7393,7107,5224,92,8,10,14,148,9,7,12,2,15,6,75,76,11,85,81,84,83,80,13,79,87,95,90,86,597,149,837,854,349,871,93,820,144,5047,27,100,99,19,106,26,17,88,24,91,3,18])). % 201.12/201.13 cnf(7594,plain, % 201.12/201.13 (P13(f10(f16(a2),a2),f17(f10(f16(a2),a1)))), % 201.12/201.13 inference(scs_inference,[],[1357,7591,47,7578,68,42,4975,7576,259,4931,5201,5055,5136,674,6096,5065,4995,7027,2663,5012,5612,7045,6758,4214,6683,7403,7381,6830,5188,7463,7468,7419,7466,7570,7461,7502,7393,7107,5224,92,8,10,14,148,9,7,12,2,15,6,75,76,11,85,81,84,83,80,13,79,87,95,90,86,597,149,837,854,349,871,93,820,144,5047,27,100,99,19,106,26,17,88,24,91,3,18,107])). % 201.12/201.13 cnf(7596,plain, % 201.12/201.13 (P9(f17(x75961))), % 201.12/201.13 inference(rename_variables,[],[47])). % 201.12/201.13 cnf(7598,plain, % 201.12/201.13 (~P16(f10(f17(a3),f17(a2)),f15(x75981))), % 201.12/201.13 inference(scs_inference,[],[1357,7591,47,7578,7596,68,42,4975,7576,259,4931,5201,5055,5136,674,6096,5065,6743,4995,7027,2663,5012,5612,7045,6758,4214,6683,7403,7381,6830,5188,7463,7468,7419,7466,7570,7461,7405,7502,7393,7107,5224,92,8,10,14,148,9,7,12,2,15,6,75,76,11,85,81,84,83,80,13,79,87,95,90,86,597,149,837,854,349,871,93,820,144,5047,27,100,99,19,106,26,17,88,24,91,3,18,107,98])). % 201.12/201.13 cnf(7616,plain, % 201.12/201.13 (E(f16(f11(a2,x76161)),f16(f11(f15(x76162),x76161)))), % 201.12/201.13 inference(scs_inference,[],[5201,5017,5080,7463,14,8,12,2,10,13,11,6,7,597,15,820])). % 201.12/201.13 cnf(7622,plain, % 201.12/201.13 (P5(f9(f17(a1)),f16(a2))), % 201.12/201.13 inference(scs_inference,[],[5201,5017,4995,5080,6758,7463,7478,14,8,12,2,10,13,11,6,7,597,15,820,9,148,854,75,90])). % 201.12/201.13 cnf(7624,plain, % 201.12/201.13 (P16(f9(f16(f10(a1,x76241))),f10(a2,x76241))), % 201.12/201.13 inference(scs_inference,[],[5201,5017,4995,5080,6758,7463,7478,14,8,12,2,10,13,11,6,7,597,15,820,9,148,854,75,90,349])). % 201.12/201.13 cnf(7642,plain, % 201.12/201.13 (P5(f13(f13(a3)),f16(f13(a3)))), % 201.12/201.13 inference(scs_inference,[],[5201,5055,5017,5065,4995,5051,5080,6758,7463,7468,7478,7598,14,8,12,2,10,13,11,6,7,597,15,820,9,148,854,75,90,349,79,80,76,84,93,81,92,149,871,837,83])). % 201.12/201.13 cnf(7646,plain, % 201.12/201.13 (P13(f10(f17(a3),f9(f16(a1))),f17(a3))), % 201.12/201.13 inference(scs_inference,[],[5201,5055,5017,5065,4995,5051,5080,6758,4224,7463,7468,7478,7598,14,8,12,2,10,13,11,6,7,597,15,820,9,148,854,75,90,349,79,80,76,84,93,81,92,149,871,837,83,85,95])). % 201.12/201.13 cnf(7653,plain, % 201.12/201.13 (~P13(x76531,f10(f16(a2),a1))), % 201.12/201.13 inference(scs_inference,[],[5201,35,5055,5017,5065,4995,5051,5080,6758,4224,7463,7468,5037,5220,7478,7549,7598,7580,6717,14,8,12,2,10,13,11,6,7,597,15,820,9,148,854,75,90,349,79,80,76,84,93,81,92,149,871,837,83,85,95,87,144,17,99])). % 201.12/201.13 cnf(7656,plain, % 201.12/201.13 (E(f10(x76561,a1),f10(x76561,f14(x76562)))), % 201.12/201.13 inference(rename_variables,[],[1357])). % 201.12/201.13 cnf(7666,plain, % 201.12/201.13 (P13(f13(f7(a12)),f16(f7(a12)))), % 201.12/201.13 inference(scs_inference,[],[1357,7656,68,5201,35,5055,5017,5065,4995,5051,5080,6719,6758,7502,6437,4224,7463,7468,7461,5037,5220,6669,7527,7478,7549,7582,7598,5211,7580,6717,7327,14,8,12,2,10,13,11,6,7,597,15,820,9,148,854,75,90,349,79,80,76,84,93,81,92,149,871,837,83,85,95,87,144,17,99,18,27,26,100,19,3,88])). % 201.12/201.13 cnf(7691,plain, % 201.12/201.13 (E(f11(x76911,f14(x76912)),f11(x76911,a1))), % 201.12/201.13 inference(scs_inference,[],[5020,6669,2,8,12,6,7])). % 201.12/201.13 cnf(7695,plain, % 201.12/201.13 (E(f10(x76951,f15(x76952)),f10(x76951,a1))), % 201.12/201.13 inference(scs_inference,[],[5017,5020,5065,6669,2,8,12,6,7,14,11,820,15])). % 201.12/201.13 cnf(7701,plain, % 201.12/201.13 (P5(f9(f11(a1,a2)),f11(a2,a1))), % 201.12/201.13 inference(scs_inference,[],[5017,5020,5065,5080,5108,6669,7560,2,8,12,6,7,14,11,820,15,148,10,13,9,597,149])). % 201.12/201.13 cnf(7702,plain, % 201.12/201.13 (P16(f9(f16(f14(x77021))),a1)), % 201.12/201.13 inference(scs_inference,[],[5017,5020,5065,5080,5108,6669,7560,2,8,12,6,7,14,11,820,15,148,10,13,9,597,149,349])). % 201.12/201.13 cnf(7718,plain, % 201.12/201.13 (E(f9(f10(f10(a1,x77181),x77182)),f9(f10(f10(a2,x77181),x77182)))), % 201.12/201.13 inference(scs_inference,[],[5017,5020,5065,5080,5051,5063,5108,5553,6669,7549,7560,2,8,12,6,7,14,11,820,15,148,10,13,9,597,149,349,854,80,76,81,79,90,75,92,871])). % 201.12/201.13 cnf(7732,plain, % 201.12/201.13 (P13(f10(f17(x77321),a1),f17(x77321))), % 201.12/201.13 inference(scs_inference,[],[5017,4995,5020,5065,5080,5051,5063,5108,5553,2622,6669,7549,5099,7560,7646,5258,2,8,12,6,7,14,11,820,15,148,10,13,9,597,149,349,854,80,76,81,79,90,75,92,871,837,83,87,93,84,85,144,95])). % 201.12/201.13 cnf(7736,plain, % 201.12/201.13 (E(f10(x77361,a1),f10(x77361,f14(x77362)))), % 201.12/201.13 inference(rename_variables,[],[1357])). % 201.12/201.13 cnf(7739,plain, % 201.12/201.13 (P16(f10(a1,f14(x77391)),f10(a1,a1))), % 201.12/201.13 inference(scs_inference,[],[1357,4974,5017,4995,5020,5065,5080,5051,5063,5108,5553,6918,2622,6669,7549,7580,7327,5099,7560,7616,7646,5258,2,8,12,6,7,14,11,820,15,148,10,13,9,597,149,349,854,80,76,81,79,90,75,92,871,837,83,87,93,84,85,144,95,6846,26,27,17])). % 201.12/201.13 cnf(7749,plain, % 201.12/201.13 (~P13(f17(a3),f17(f17(a2)))), % 201.12/201.13 inference(scs_inference,[],[1357,7736,47,4974,68,5017,4995,5020,5065,5080,5051,5063,5108,5553,6918,6845,2622,5037,6669,7549,7580,7327,5099,7560,7616,7646,7477,5258,2,8,12,6,7,14,11,820,15,148,10,13,9,597,149,349,854,80,76,81,79,90,75,92,871,837,83,87,93,84,85,144,95,6846,26,27,17,18,3,88,106])). % 201.12/201.13 cnf(7776,plain, % 201.12/201.13 (E(f11(f15(x77761),x77762),f11(a1,x77762))), % 201.12/201.13 inference(scs_inference,[],[5065,7560,8,12,7,2,13,6])). % 201.12/201.13 cnf(7782,plain, % 201.12/201.13 (P5(f9(f10(a2,a1)),f10(a1,a2))), % 201.12/201.13 inference(scs_inference,[],[5020,5065,5080,5108,5041,7560,7718,8,12,7,2,13,6,148,10,820,15,14,149])). % 201.12/201.13 cnf(7784,plain, % 201.12/201.13 (P16(f9(f16(f15(x77841))),a1)), % 201.12/201.13 inference(scs_inference,[],[5020,5065,5080,5108,5041,7560,7718,8,12,7,2,13,6,148,10,820,15,14,149,11,349])). % 201.12/201.13 cnf(7785,plain, % 201.12/201.13 (E(f17(f15(x77851)),f17(a1))), % 201.12/201.13 inference(scs_inference,[],[5020,5065,5080,5108,5041,7560,7718,8,12,7,2,13,6,148,10,820,15,14,149,11,349,9])). % 201.12/201.13 cnf(7790,plain, % 201.12/201.13 (E(f9(f10(f14(x77901),x77902)),f9(f10(a1,x77902)))), % 201.12/201.13 inference(scs_inference,[],[5020,5065,5080,5108,5063,5041,7560,7718,8,12,7,2,13,6,148,10,820,15,14,149,11,349,9,854,597,75,871])). % 201.12/201.13 cnf(7800,plain, % 201.12/201.14 (~P1(f13(f10(f17(a3),f17(a2))))), % 201.12/201.14 inference(scs_inference,[],[5020,5065,5080,5108,5063,5041,7560,7646,6906,7718,8,12,7,2,13,6,148,10,820,15,14,149,11,349,9,854,597,75,871,76,837,92,81,80,79])). % 201.12/201.14 cnf(7806,plain, % 201.12/201.14 (P5(f10(f17(x78061),a1),f17(x78061))), % 201.12/201.14 inference(scs_inference,[],[5020,5051,5065,5080,5108,5063,5041,5642,7560,7646,6906,7718,7732,8,12,7,2,13,6,148,10,820,15,14,149,11,349,9,854,597,75,871,76,837,92,81,80,79,90,85,87])). % 201.12/201.14 cnf(7808,plain, % 201.12/201.14 (P5(f13(f6(a3)),f16(f6(a3)))), % 201.12/201.14 inference(scs_inference,[],[5020,5051,5065,5080,5108,5063,5041,5642,7560,7646,6906,7718,7732,8,12,7,2,13,6,148,10,820,15,14,149,11,349,9,854,597,75,871,76,837,92,81,80,79,90,85,87,83])). % 201.12/201.14 cnf(7816,plain, % 201.12/201.14 (P13(f10(f17(a3),f17(a2)),f17(a3))), % 201.12/201.14 inference(scs_inference,[],[5020,5051,5065,5080,5108,5063,5041,5037,5642,7560,7646,6906,6342,7718,7732,5266,8,12,7,2,13,6,148,10,820,15,14,149,11,349,9,854,597,75,871,76,837,92,81,80,79,90,85,87,83,93,84,144,95])). % 201.12/201.14 cnf(7820,plain, % 201.12/201.14 (P5(f9(f17(a2)),f16(a2))), % 201.12/201.14 inference(scs_inference,[],[5158,5020,5051,5065,5080,5108,5063,5041,5037,5642,6669,7560,7646,7622,6906,6342,7718,7732,6589,5266,8,12,7,2,13,6,148,10,820,15,14,149,11,349,9,854,597,75,871,76,837,92,81,80,79,90,85,87,83,93,84,144,95,4329,3,26])). % 201.12/201.14 cnf(7823,plain, % 201.12/201.14 (E(f10(x78231,a1),f10(x78231,f14(x78232)))), % 201.12/201.14 inference(rename_variables,[],[1357])). % 201.12/201.14 cnf(7826,plain, % 201.12/201.14 (P13(f13(f7(a5)),f16(f7(a5)))), % 201.12/201.14 inference(scs_inference,[],[1357,7823,4945,5158,68,5020,5051,5065,5080,5108,5063,5041,5037,5642,6669,7540,7560,7646,7622,6911,6906,6342,7718,7732,7739,6589,5266,8,12,7,2,13,6,148,10,820,15,14,149,11,349,9,854,597,75,871,76,837,92,81,80,79,90,85,87,83,93,84,144,95,4329,3,26,27,18,17,88])). % 201.12/201.14 cnf(7831,plain, % 201.12/201.14 (~E(f10(a12,a1),f16(a12))), % 201.12/201.14 inference(scs_inference,[],[1357,7823,4945,5158,68,5020,5051,5065,5080,7027,5108,5063,5041,4951,5037,5642,6669,6789,7540,7560,7646,7622,7642,6911,6906,6342,7718,7732,7739,6589,5266,8,12,7,2,13,6,148,10,820,15,14,149,11,349,9,854,597,75,871,76,837,92,81,80,79,90,85,87,83,93,84,144,95,4329,3,26,27,18,17,88,100,24])). % 201.12/201.14 cnf(7854,plain, % 201.12/201.14 (E(f9(f11(a1,a2)),f9(f11(a2,a1)))), % 201.12/201.14 inference(scs_inference,[],[5080,12,8,7,13])). % 201.12/201.14 cnf(7856,plain, % 201.12/201.14 (P5(f9(f10(a2,a2)),f10(a1,a1))), % 201.12/201.14 inference(scs_inference,[],[5080,5041,6722,12,8,7,13,2,149])). % 201.12/201.14 cnf(7867,plain, % 201.12/201.14 (P16(f9(f16(f11(a1,a2))),f11(a2,a1))), % 201.12/201.14 inference(scs_inference,[],[5065,5080,5108,5041,6693,6722,7790,12,8,7,13,2,149,9,15,10,14,6,820,148,854,597,11,349])). % 201.12/201.14 cnf(7868,plain, % 201.12/201.14 (E(f9(f10(f15(x78681),x78682)),f9(f10(a1,x78682)))), % 201.12/201.14 inference(scs_inference,[],[5065,5080,5108,5041,6693,6722,7790,12,8,7,13,2,149,9,15,10,14,6,820,148,854,597,11,349,871])). % 201.12/201.14 cnf(7870,plain, % 201.12/201.14 (~P1(f7(f10(f17(a3),f17(a2))))), % 201.12/201.14 inference(scs_inference,[],[5065,5080,5108,5041,6693,6906,6722,7790,12,8,7,13,2,149,9,15,10,14,6,820,148,854,597,11,349,871,837,81])). % 201.12/201.14 cnf(7872,plain, % 201.12/201.14 (~P1(f6(f10(f17(a3),f17(a2))))), % 201.12/201.14 inference(scs_inference,[],[5065,5080,5108,5041,6693,6906,6722,7790,12,8,7,13,2,149,9,15,10,14,6,820,148,854,597,11,349,871,837,81,80])). % 201.12/201.14 cnf(7874,plain, % 201.12/201.14 (P6(f6(f10(f17(a3),f17(a2))))), % 201.12/201.14 inference(scs_inference,[],[5065,5080,5108,5041,6693,6906,6722,7790,12,8,7,13,2,149,9,15,10,14,6,820,148,854,597,11,349,871,837,81,80,75])). % 201.12/201.14 cnf(7876,plain, % 201.12/201.14 (P6(f7(f10(f17(a3),f17(a2))))), % 201.12/201.14 inference(scs_inference,[],[5065,5080,5108,5041,6693,6906,6722,7790,12,8,7,13,2,149,9,15,10,14,6,820,148,854,597,11,349,871,837,81,80,75,76])). % 201.12/201.14 cnf(7892,plain, % 201.12/201.14 (~P5(a12,f16(f14(x78921)))), % 201.12/201.14 inference(scs_inference,[],[5065,5063,5080,5108,5041,6693,5181,6906,6722,6678,7732,7790,7816,5361,12,8,7,13,2,149,9,15,10,14,6,820,148,854,597,11,349,871,837,81,80,75,76,79,90,92,84,85,87,83,93])). % 201.12/201.14 cnf(7896,plain, % 201.12/201.14 (P13(f10(f10(f17(a3),f17(a2)),f15(x78961)),f10(f17(a3),f17(a2)))), % 201.12/201.14 inference(scs_inference,[],[5065,5063,5080,5108,5041,6693,5181,6906,7598,6722,6678,7732,5117,7790,7816,5361,12,8,7,13,2,149,9,15,10,14,6,820,148,854,597,11,349,871,837,81,80,75,76,79,90,92,84,85,87,83,93,144,95])). % 201.12/201.14 cnf(7903,plain, % 201.12/201.14 (E(f10(x79031,a1),f10(x79031,f14(x79032)))), % 201.12/201.14 inference(rename_variables,[],[1357])). % 201.12/201.14 cnf(7906,plain, % 201.12/201.14 (P5(f10(f17(a1),a1),f17(a2))), % 201.12/201.14 inference(scs_inference,[],[1357,7903,5016,5065,5063,5080,5108,5041,6693,5014,5181,6906,7598,6722,6678,7732,5117,7790,7816,7831,5304,7806,7559,6820,5361,12,8,7,13,2,149,9,15,10,14,6,820,148,854,597,11,349,871,837,81,80,75,76,79,90,92,84,85,87,83,93,144,95,17,18,3,26,27])). % 201.12/201.14 cnf(7908,plain, % 201.12/201.14 (~E(f10(a3,a2),f16(a3))), % 201.12/201.14 inference(scs_inference,[],[1357,7903,5016,5065,5231,5063,5080,7027,5108,5041,6693,5014,5181,6906,7598,6722,6678,7732,5117,7790,7816,7831,5304,7806,7559,6820,5361,12,8,7,13,2,149,9,15,10,14,6,820,148,854,597,11,349,871,837,81,80,75,76,79,90,92,84,85,87,83,93,144,95,17,18,3,26,27,24])). % 201.12/201.14 cnf(7923,plain, % 201.12/201.14 (~E(f10(f17(a3),f17(a2)),a1)), % 201.12/201.14 inference(scs_inference,[],[1357,7903,47,68,111,5016,36,5065,5231,5063,5080,7027,5108,5041,6693,6715,7622,5014,5181,5059,6906,7598,6722,6678,7732,5258,5117,7790,7816,7831,5304,7806,7820,7050,7808,7559,6820,5361,12,8,7,13,2,149,9,15,10,14,6,820,148,854,597,11,349,871,837,81,80,75,76,79,90,92,84,85,87,83,93,144,95,17,18,3,26,27,24,88,99,100,106,91,25])). % 201.12/201.14 cnf(7934,plain, % 201.12/201.14 (E(f9(f10(a2,a1)),f9(f10(a1,a2)))), % 201.12/201.14 inference(scs_inference,[],[5108,12,8,13])). % 201.12/201.14 cnf(7949,plain, % 201.12/201.14 (E(f9(f10(f11(a1,a2),x79491)),f9(f10(f11(a2,a1),x79491)))), % 201.12/201.14 inference(scs_inference,[],[5080,4977,5108,5041,6682,7790,7854,12,8,13,7,2,9,15,149,820,148,597,6,349,14,10,11,854,871])). % 201.12/201.14 cnf(7978,plain, % 201.12/201.14 (P13(f10(f17(x79781),f14(x79782)),f17(x79781))), % 201.12/201.14 inference(scs_inference,[],[5080,4977,5108,5041,6906,6682,7327,6678,5188,7790,7816,5092,7854,7896,6871,5105,12,8,13,7,2,9,15,149,820,148,597,6,349,14,10,11,854,871,837,76,79,81,90,75,87,80,84,92,85,83,144,93,4329,95])). % 201.12/201.14 cnf(7989,plain, % 201.12/201.14 (~E(f10(f17(f7(a3)),f15(x79891)),f16(f17(f7(a3))))), % 201.12/201.14 inference(scs_inference,[],[1357,4945,4975,5080,4977,7027,5108,5041,6906,2663,6727,6682,4972,7327,6678,5188,7790,7816,7806,7820,6820,5092,7854,7896,7908,7876,7147,6871,5105,12,8,13,7,2,9,15,149,820,148,597,6,349,14,10,11,854,871,837,76,79,81,90,75,87,80,84,92,85,83,144,93,4329,95,26,18,3,27,19,17,24])). % 201.12/201.14 cnf(7996,plain, % 201.12/201.14 (~P13(a3,f17(f14(x79961)))), % 201.12/201.14 inference(scs_inference,[],[1357,47,4945,68,4975,5080,4977,7027,5108,5041,6906,2663,6727,6682,4972,7642,7327,6678,5188,7790,7816,7806,7820,7808,6820,5266,5092,7854,7896,7908,7876,7147,6871,6397,5105,12,8,13,7,2,9,15,149,820,148,597,6,349,14,10,11,854,871,837,76,79,81,90,75,87,80,84,92,85,83,144,93,4329,95,26,18,3,27,19,17,24,88,100,106])). % 201.12/201.14 cnf(8012,plain, % 201.12/201.14 (P5(f9(f10(a1,a2)),f10(a2,a1))), % 201.12/201.14 inference(scs_inference,[],[5108,5041,6687,7854,7934,12,8,149,9,2,820,148])). % 201.12/201.14 cnf(8015,plain, % 201.12/201.14 (E(f10(x80151,f15(x80152)),f10(x80151,a2))), % 201.12/201.14 inference(scs_inference,[],[5108,5041,5136,6687,7854,7934,12,8,149,9,2,820,148,13,7,15])). % 201.12/201.14 cnf(8023,plain, % 201.12/201.14 (E(f9(f10(f10(a2,a1),x80231)),f9(f10(f10(a1,a2),x80231)))), % 201.12/201.14 inference(scs_inference,[],[5108,5041,5136,6687,7854,7934,12,8,149,9,2,820,148,13,7,15,6,597,349,14,11,10,854,871])). % 201.12/201.14 cnf(8050,plain, % 201.12/201.14 (P13(f10(f16(x80501),f15(x80502)),f16(x80501))), % 201.12/201.14 inference(scs_inference,[],[5108,5041,5136,6687,6820,6871,5224,7854,7870,7896,6397,7934,7424,6875,12,8,149,9,2,820,148,13,7,15,6,597,349,14,11,10,854,871,837,81,90,79,87,76,75,83,80,84,85,144,92,6846,95])). % 201.12/201.14 cnf(8055,plain, % 201.12/201.14 (P5(f9(f10(a2,f14(x80551))),f10(a1,a2))), % 201.12/201.14 inference(scs_inference,[],[5201,5108,5041,5136,6687,6820,6871,5224,7854,6964,7050,7147,7870,7896,6397,7107,7934,7424,7782,6875,12,8,149,9,2,820,148,13,7,15,6,597,349,14,11,10,854,871,837,81,90,79,87,76,75,83,80,84,85,144,92,6846,95,27,18,26])). % 201.12/201.14 cnf(8079,plain, % 201.12/201.14 (P5(f9(f11(a2,a2)),f11(a1,a1))), % 201.12/201.14 inference(scs_inference,[],[5041,5136,4985,12,8,9,149])). % 201.12/201.14 cnf(8090,plain, % 201.12/201.14 (P16(f9(f16(f10(a2,a2))),f10(a1,a1))), % 201.12/201.14 inference(scs_inference,[],[5041,5136,6682,4985,7934,7868,12,8,9,149,148,7,2,13,820,15,597,14,6,11,349])). % 201.12/201.14 cnf(8093,plain, % 201.12/201.14 (E(f9(f10(f10(a2,a2),x80931)),f9(f10(f10(a1,a1),x80931)))), % 201.12/201.14 inference(scs_inference,[],[5041,5136,6682,4985,7934,7868,12,8,9,149,148,7,2,13,820,15,597,14,6,11,349,10,854,871])). % 201.12/201.14 cnf(8097,plain, % 201.12/201.14 (P5(f9(f16(f14(x80971))),f16(a2))), % 201.12/201.14 inference(scs_inference,[],[5041,5136,6682,4985,7147,7934,6875,7868,12,8,9,149,148,7,2,13,820,15,597,14,6,11,349,10,854,871,837,79,90])). % 201.12/201.14 cnf(8103,plain, % 201.12/201.14 (P5(f10(f16(x81031),f15(x81032)),f16(x81031))), % 201.12/201.14 inference(scs_inference,[],[5041,5136,6682,4985,7147,7870,7934,6875,7868,8050,12,8,9,149,148,7,2,13,820,15,597,14,6,11,349,10,854,871,837,79,90,81,75,87])). % 201.12/201.14 cnf(8107,plain, % 201.12/201.14 (P5(f13(f6(f17(x81071))),f16(f6(f17(x81071))))), % 201.12/201.14 inference(scs_inference,[],[5041,5136,6682,4985,7147,7870,7934,6875,7868,8050,12,8,9,149,148,7,2,13,820,15,597,14,6,11,349,10,854,871,837,79,90,81,75,87,76,83])). % 201.12/201.14 cnf(8119,plain, % 201.12/201.14 (P13(f10(a12,f15(x81191)),a12)), % 201.12/201.14 inference(scs_inference,[],[5041,5136,6682,4985,7147,7870,5258,7934,7424,6875,6361,7868,8050,6877,12,8,9,149,148,7,2,13,820,15,597,14,6,11,349,10,854,871,837,79,90,81,75,87,76,83,144,80,84,92,85,95])). % 201.12/201.14 cnf(8121,plain, % 201.12/201.14 (P5(f9(f11(a1,a2)),f11(a1,a1))), % 201.12/201.14 inference(scs_inference,[],[5041,5136,6682,4985,4972,7147,7870,5258,7934,7424,6875,6361,7868,8050,7701,6877,12,8,9,149,148,7,2,13,820,15,597,14,6,11,349,10,854,871,837,79,90,81,75,87,76,83,144,80,84,92,85,95,27])). % 201.12/201.14 cnf(8122,plain, % 201.12/201.14 (E(f11(a2,x81221),f11(a1,x81221))), % 201.12/201.14 inference(rename_variables,[],[4972])). % 201.12/201.14 cnf(8127,plain, % 201.12/201.14 (~E(f10(f17(f7(a3)),a2),f16(f17(f7(a3))))), % 201.12/201.14 inference(scs_inference,[],[1357,5041,5136,6682,4985,4972,8122,7147,7870,5258,7934,7424,6875,6361,8015,7868,8050,7989,7701,7906,7867,6877,12,8,9,149,148,7,2,13,820,15,597,14,6,11,349,10,854,871,837,79,90,81,75,87,76,83,144,80,84,92,85,95,27,26,18,3])). % 201.12/201.14 cnf(8152,plain, % 201.12/201.14 (E(f13(f10(x81521,f17(a1))),f13(f10(x81521,f17(a2))))), % 201.12/201.14 inference(scs_inference,[],[6682,12])). % 201.12/201.14 cnf(8153,plain, % 201.12/201.14 (E(f16(f10(x81531,f17(a1))),f16(f10(x81531,f17(a2))))), % 201.12/201.14 inference(scs_inference,[],[6682,12,8])). % 201.12/201.14 cnf(8157,plain, % 201.12/201.14 (E(f17(f15(x81571)),f17(a2))), % 201.12/201.14 inference(scs_inference,[],[5136,6682,7868,12,8,7,820,2,9])). % 201.12/201.14 cnf(8166,plain, % 201.12/201.14 (E(f6(f10(x81661,f17(a1))),f6(f10(x81661,f17(a2))))), % 201.12/201.14 inference(scs_inference,[],[5136,6682,6687,5014,7868,7949,12,8,7,820,2,9,149,148,13,15,597,6,14,349,11])). % 201.12/201.14 cnf(8169,plain, % 201.12/201.14 (E(f9(f10(f15(x81691),x81692)),f9(f10(a2,x81692)))), % 201.12/201.14 inference(scs_inference,[],[5136,6682,6687,5014,7868,7949,12,8,7,820,2,9,149,148,13,15,597,6,14,349,11,10,854,871])). % 201.12/201.14 cnf(8175,plain, % 201.12/201.14 (P5(f9(f16(f9(f16(a2)))),f16(x81751))), % 201.12/201.14 inference(scs_inference,[],[5136,6682,6687,5014,6875,6748,6877,7868,7949,12,8,7,820,2,9,149,148,13,15,597,6,14,349,11,10,854,871,837,79,81,90])). % 201.12/201.14 cnf(8202,plain, % 201.12/201.14 (~E(f10(f17(f7(a3)),a1),f16(f17(f7(a3))))), % 201.12/201.14 inference(scs_inference,[],[1357,4975,5136,6682,6687,5014,6875,7854,6748,6877,7107,5266,7868,7054,8050,5067,7949,8119,8127,8121,8090,6948,12,8,7,820,2,9,149,148,13,15,597,6,14,349,11,10,854,871,837,79,81,90,75,87,76,83,85,144,80,84,92,95,27,26,18,3])). % 201.12/201.14 cnf(8232,plain, % 201.12/201.14 (E(f9(f10(f11(a2,a1),x82321)),f9(f10(f11(a1,a2),x82321)))), % 201.12/201.14 inference(scs_inference,[],[6682,4948,6687,7949,12,8,820,7,9,2])). % 201.12/201.14 cnf(8233,plain, % 201.12/201.14 (P5(f9(f11(a2,x82331)),f11(a1,x82331))), % 201.12/201.14 inference(scs_inference,[],[6682,4948,6687,4972,7949,12,8,820,7,9,2,149])). % 201.12/201.14 cnf(8239,plain, % 201.12/201.14 (P16(f9(f16(f10(x82391,f17(a1)))),f10(x82391,f17(a2)))), % 201.12/201.14 inference(scs_inference,[],[6682,4948,6687,5014,4972,6669,7949,8169,12,8,820,7,9,2,149,597,148,13,15,6,349])). % 201.12/201.14 cnf(8262,plain, % 201.12/201.14 (P5(f13(f7(f16(x82621))),f16(f7(f16(x82621))))), % 201.12/201.14 inference(scs_inference,[],[6682,4948,6687,5014,6877,4972,6669,6948,6911,7949,5222,8169,7594,12,8,820,7,9,2,149,597,148,13,15,6,349,14,10,854,11,871,837,79,81,75,87,76,90,144,80,83])). % 201.12/201.14 cnf(8275,plain, % 201.12/201.14 (E(f10(x82751,a1),f10(x82751,f14(x82752)))), % 201.12/201.14 inference(rename_variables,[],[1357])). % 201.12/201.14 cnf(8276,plain, % 201.12/201.14 (~E(f10(f17(a3),f17(a1)),f16(f17(a3)))), % 201.12/201.14 inference(scs_inference,[],[1357,4945,6682,7027,4948,6687,5014,6877,4972,6669,7289,6948,6911,5105,7949,8103,8119,5222,8169,7594,8202,6954,12,8,820,7,9,2,149,597,148,13,15,6,349,14,10,854,11,871,837,79,81,75,87,76,90,144,80,83,85,92,84,95,27,3,24])). % 201.12/201.14 cnf(8279,plain, % 201.12/201.14 (P5(f9(f16(f9(f16(a2)))),f16(x82791))), % 201.12/201.14 inference(rename_variables,[],[8175])). % 201.12/201.14 cnf(8284,plain, % 201.12/201.14 (P13(f13(f16(x82841)),f16(f16(x82841)))), % 201.12/201.14 inference(scs_inference,[],[1357,8275,4945,68,6682,7027,4948,6687,5014,6715,2629,6877,4972,6669,7289,7054,6948,6911,5105,7949,8103,8119,5222,8169,7594,8202,8175,7624,7784,6954,12,8,820,7,9,2,149,597,148,13,15,6,349,14,10,854,11,871,837,79,81,75,87,76,90,144,80,83,85,92,84,95,27,3,24,26,18,17,88])). % 201.12/201.14 cnf(8296,plain, % 201.12/201.14 (P13(f9(f16(f9(f16(a2)))),f17(x82961))), % 201.12/201.14 inference(scs_inference,[],[1357,8275,47,4945,68,35,37,6682,7027,4948,6687,5014,6715,2629,6877,4972,6669,6748,7289,7054,6948,6911,5105,7949,8103,8119,5222,8169,8166,7594,8202,8175,8279,7122,7624,7784,6954,7872,6287,12,8,820,7,9,2,149,597,148,13,15,6,349,14,10,854,11,871,837,79,81,75,87,76,90,144,80,83,85,92,84,95,27,3,24,26,18,17,88,91,100,99,16,107])). % 201.12/201.14 cnf(8314,plain, % 201.12/201.14 (E(f9(f11(a1,x83141)),f9(f11(a2,x83141)))), % 201.12/201.14 inference(scs_inference,[],[6687,4977,5014,4985,6669,7854,8166,8023,12,8,7,149,820,148,2,15,9,597,6,13])). % 201.12/201.14 cnf(8321,plain, % 201.12/201.14 (E(f9(f10(f11(a2,a2),x83211)),f9(f10(f11(a1,a1),x83211)))), % 201.12/201.14 inference(scs_inference,[],[6687,4977,5014,4985,6669,7854,8166,8023,12,8,7,149,820,148,2,15,9,597,6,13,14,349,11,10,854,837,871])). % 201.12/201.14 cnf(8342,plain, % 201.12/201.14 (P5(f13(f6(f16(x83421))),f16(f6(f16(x83421))))), % 201.12/201.14 inference(scs_inference,[],[6687,4977,5014,4985,6669,6948,7854,6954,137,8166,6287,8023,8296,8284,6958,12,8,7,149,820,148,2,15,9,597,6,13,14,349,11,10,854,837,871,79,81,75,76,87,80,144,85,90,92,83])). % 201.12/201.14 cnf(8346,plain, % 201.12/201.14 (P13(f10(f17(a3),f9(a3)),f17(a3))), % 201.12/201.14 inference(scs_inference,[],[6687,4977,5014,4985,6669,6948,7854,6954,137,4218,8166,6287,8023,8296,8284,6958,12,8,7,149,820,148,2,15,9,597,6,13,14,349,11,10,854,837,871,79,81,75,76,87,80,144,85,90,92,83,84,95])). % 201.12/201.14 cnf(8352,plain, % 201.12/201.14 (P16(f10(f17(f7(a3)),a2),f7(a3))), % 201.12/201.14 inference(scs_inference,[],[1357,6682,6687,4977,5014,4985,6669,6948,7854,6954,137,4218,8166,8015,6287,8023,8296,8284,8276,7856,6958,6792,12,8,7,149,820,148,2,15,9,597,6,13,14,349,11,10,854,837,871,79,81,75,76,87,80,144,85,90,92,83,84,95,3,27,17])). % 201.12/201.14 cnf(8361,plain, % 201.12/201.14 (P16(f9(f16(f10(a2,f14(x83611)))),f10(a1,f14(x83612)))), % 201.12/201.14 inference(scs_inference,[],[1357,4974,6682,7027,6687,4977,5014,4985,6669,6948,7854,7148,7549,6954,137,4218,8166,8015,6287,8023,8296,8284,8276,7856,7034,7874,7592,6958,6792,12,8,7,149,820,148,2,15,9,597,6,13,14,349,11,10,854,837,871,79,81,75,76,87,80,144,85,90,92,83,84,95,3,27,17,19,26,24,18])). % 201.12/201.14 cnf(8367,plain, % 201.12/201.14 (P6(f9(f16(f14(x83671))))), % 201.12/201.14 inference(scs_inference,[],[1357,68,4974,6682,7027,6687,4977,5014,4985,6669,6948,7854,7148,7549,6954,7820,137,4218,4956,8166,8015,6287,8023,8296,8284,8276,7856,7034,8097,7874,7592,6958,6792,12,8,7,149,820,148,2,15,9,597,6,13,14,349,11,10,854,837,871,79,81,75,76,87,80,144,85,90,92,83,84,95,3,27,17,19,26,24,18,88,91])). % 201.12/201.14 cnf(8371,plain, % 201.12/201.14 (P13(f9(f16(f14(x83711))),f17(a2))), % 201.12/201.14 inference(scs_inference,[],[1357,47,68,4974,6682,7027,6687,4977,5014,4985,6669,6948,7854,7147,7148,7549,6954,7820,137,4218,4956,8166,8015,6287,8023,8296,8284,8276,7856,7034,8097,7126,7874,7592,6958,6792,12,8,7,149,820,148,2,15,9,597,6,13,14,349,11,10,854,837,871,79,81,75,76,87,80,144,85,90,92,83,84,95,3,27,17,19,26,24,18,88,91,100,107])). % 201.12/201.14 cnf(8382,plain, % 201.12/201.14 (E(f9(f10(f10(a1,a2),x83821)),f9(f10(f10(a2,a1),x83821)))), % 201.12/201.14 inference(scs_inference,[],[4985,6693,7854,8023,12,8,149,2])). % 201.12/201.14 cnf(8386,plain, % 201.12/201.14 (E(f9(f11(a2,a2)),f9(f11(a1,a1)))), % 201.12/201.14 inference(scs_inference,[],[5014,4985,6693,7854,8023,12,8,149,2,7,820,9,13])). % 201.12/201.14 cnf(8430,plain, % 201.12/201.14 (P16(f10(f17(f7(a3)),a1),f7(a3))), % 201.12/201.14 inference(scs_inference,[],[1357,4975,5014,4985,6693,7854,6954,7148,6958,6087,8023,7034,7428,5184,8093,8346,8352,7002,7923,6936,12,8,149,2,7,820,9,13,148,15,6,597,349,14,11,10,854,837,871,81,79,75,76,87,80,144,90,84,85,83,92,95,86,3,27,17])). % 201.12/201.14 cnf(8438,plain, % 201.12/201.14 (P13(f10(f17(a1),a1),f17(a2))), % 201.12/201.14 inference(scs_inference,[],[1357,4974,4975,69,5014,7027,4985,6693,7854,6954,7148,7646,6958,6087,5220,8023,7906,7034,8097,7428,5184,8093,8346,8352,8239,7002,7923,6936,12,8,149,2,7,820,9,13,148,15,6,597,349,14,11,10,854,837,871,81,79,75,76,87,80,144,90,84,85,83,92,95,86,3,27,17,24,18,26,88])). % 201.12/201.14 cnf(8446,plain, % 201.12/201.14 (P13(f9(f16(f14(x84461))),f17(a1))), % 201.12/201.14 inference(scs_inference,[],[1357,47,4974,4975,69,5014,7027,4985,6693,7854,6954,7148,6287,7646,6958,6087,5220,8023,7906,7034,6865,7702,8097,7428,5184,8093,8346,7130,8107,8367,8352,8239,7002,7923,6936,12,8,149,2,7,820,9,13,148,15,6,597,349,14,11,10,854,837,871,81,79,75,76,87,80,144,90,84,85,83,92,95,86,3,27,17,24,18,26,88,91,100,107])). % 201.12/201.14 cnf(8458,plain, % 201.12/201.14 (E(f9(f10(f10(a1,a1),x84581)),f9(f10(f10(a2,a2),x84581)))), % 201.12/201.14 inference(scs_inference,[],[4985,6693,6669,7148,8093,12,8,149,820,2])). % 201.12/201.14 cnf(8461,plain, % 201.12/201.14 (P5(f9(f11(a1,a1)),f11(a2,a2))), % 201.12/201.14 inference(scs_inference,[],[4985,6693,6669,7148,8093,8386,12,8,149,820,2,7,15,148])). % 201.12/201.14 cnf(8467,plain, % 201.12/201.14 (P16(f9(f16(f11(a2,a2))),f11(a1,a1))), % 201.12/201.14 inference(scs_inference,[],[4985,6693,6669,7148,7107,8093,8386,12,8,149,820,2,7,15,148,9,6,13,597,14,349])). % 201.12/201.14 cnf(8487,plain, % 201.12/201.14 (P5(f13(f10(f17(a3),f17(a1))),f16(f10(f17(a3),f17(a1))))), % 201.12/201.14 inference(scs_inference,[],[4985,6693,6669,4972,7148,6958,7107,7002,8093,7800,5152,8386,8371,12,8,149,820,2,7,15,148,9,6,13,597,14,349,10,11,837,854,871,81,79,75,76,87,144,80,83])). % 201.12/201.14 cnf(8491,plain, % 201.12/201.14 (~P13(f17(a2),f10(f17(a1),a1))), % 201.12/201.14 inference(scs_inference,[],[4985,6693,6669,4972,7148,6958,7107,7702,7002,8093,7800,5152,8386,8371,8438,12,8,149,820,2,7,15,148,9,6,13,597,14,349,10,11,837,854,871,81,79,75,76,87,144,80,83,90,92])). % 201.12/201.14 cnf(8497,plain, % 201.12/201.14 (P13(f10(f17(x84971),f15(x84972)),f17(x84971))), % 201.12/201.14 inference(scs_inference,[],[4985,6693,6669,4972,7148,6958,7107,7702,7002,8093,7800,4993,5152,8386,8371,8438,7048,12,8,149,820,2,7,15,148,9,6,13,597,14,349,10,11,837,854,871,81,79,75,76,87,144,80,83,90,92,85,84,95])). % 201.12/201.14 cnf(8500,plain, % 201.12/201.14 (E(f10(x85001,a1),f10(x85001,f14(x85002)))), % 201.12/201.14 inference(rename_variables,[],[1357])). % 201.12/201.14 cnf(8508,plain, % 201.12/201.14 (E(f10(x85081,a1),f10(x85081,f14(x85082)))), % 201.12/201.14 inference(rename_variables,[],[1357])). % 201.12/201.14 cnf(8512,plain, % 201.12/201.14 (P1(f10(f16(a2),a1))), % 201.12/201.14 inference(scs_inference,[],[1357,8500,5158,1356,7027,4985,6693,6669,4972,7148,6958,7107,8346,7034,7702,7002,8093,7800,4993,5152,8386,8371,8438,7653,8012,7388,8430,8361,7048,6655,12,8,149,820,2,7,15,148,9,6,13,597,14,349,10,11,837,854,871,81,79,75,76,87,144,80,83,90,92,85,84,95,27,3,24,26,17,18,88])). % 201.12/201.14 cnf(8521,plain, % 201.12/201.14 (P1(f10(f16(a2),f14(x85211)))), % 201.12/201.14 inference(scs_inference,[],[1357,8500,8508,5158,1356,7027,4985,6693,6669,4972,7148,6958,7107,8346,6467,7034,7702,7002,8093,7800,4993,5152,8386,8371,8438,7653,8012,7388,7278,8262,6943,8430,8361,7048,6655,12,8,149,820,2,7,15,148,9,6,13,597,14,349,10,11,837,854,871,81,79,75,76,87,144,80,83,90,92,85,84,95,27,3,24,26,17,18,88,91,100,16])). % 201.12/201.14 cnf(8546,plain, % 201.12/201.14 (P16(f9(f16(f10(a1,f14(x85461)))),f10(a2,a2))), % 201.12/201.14 inference(scs_inference,[],[6693,6669,4972,7107,4970,8386,8232,8,12,820,149,15,2,6,7,9,13,148,597,10,11,14,349])). % 201.12/201.14 cnf(8558,plain, % 201.12/201.14 (P5(f10(f17(x85581),f15(x85582)),f17(x85581))), % 201.12/201.14 inference(scs_inference,[],[6693,6669,4972,7107,5015,7800,5073,4970,7048,8386,8232,8497,8,12,820,149,15,2,6,7,9,13,148,597,10,11,14,349,837,854,871,79,81,75,76,87])). % 201.12/201.14 cnf(8574,plain, % 201.12/201.14 (P6(f10(f17(x85741),f15(x85742)))), % 201.12/201.14 inference(scs_inference,[],[6693,6669,4972,7107,5015,7800,5073,4970,7048,6075,8386,5128,8232,8497,7052,8,12,820,149,15,2,6,7,9,13,148,597,10,11,14,349,837,854,871,79,81,75,76,87,144,92,80,85,83,90,84,86])). % 201.12/201.14 cnf(8578,plain, % 201.12/201.14 (~E(f6(a5),f14(x85781))), % 201.12/201.14 inference(scs_inference,[],[1357,5158,6693,6669,4972,7107,5015,7800,5073,4970,7048,6075,8386,7388,5128,8232,8497,7052,6560,8,12,820,149,15,2,6,7,9,13,148,597,10,11,14,349,837,854,871,79,81,75,76,87,144,92,80,85,83,90,84,86,27,3])). % 201.12/201.14 cnf(8579,plain, % 201.12/201.14 (~E(f10(f16(a3),a1),f16(f17(f10(f16(a3),a2))))), % 201.12/201.14 inference(scs_inference,[],[1357,5158,7027,6693,6669,4972,7107,5015,7800,5073,4970,7424,7048,6075,8386,7388,5128,8232,8497,7052,6560,8,12,820,149,15,2,6,7,9,13,148,597,10,11,14,349,837,854,871,79,81,75,76,87,144,92,80,85,83,90,84,86,27,3,24])). % 201.12/201.14 cnf(8595,plain, % 201.12/201.14 (P1(f10(f16(a2),a2))), % 201.12/201.14 inference(scs_inference,[],[70,1357,68,5158,5014,7027,6693,6669,4972,7107,5015,6467,7800,5073,4970,7424,7048,8097,6075,8386,7388,5128,8314,8232,8497,8512,8461,7366,8342,6939,8467,7052,6835,6560,8,12,820,149,15,2,6,7,9,13,148,597,10,11,14,349,837,854,871,79,81,75,76,87,144,92,80,85,83,90,84,86,27,3,24,17,26,18,88,91,100,16])). % 201.12/201.14 cnf(8641,plain, % 201.12/201.14 (P5(f13(f6(f6(a5))),f16(f6(f6(a5))))), % 201.12/201.14 inference(scs_inference,[],[6669,4972,7148,7048,4970,4971,7052,5129,6860,8321,8446,7666,7056,12,8,820,149,6,13,9,2,597,15,148,10,7,11,349,14,837,854,871,81,79,75,76,87,92,85,80,144,83])). % 201.12/201.14 cnf(8650,plain, % 201.12/201.14 (E(f10(x86501,a1),f10(x86501,f14(x86502)))), % 201.12/201.14 inference(rename_variables,[],[1357])). % 201.12/201.14 cnf(8653,plain, % 201.12/201.14 (~E(f10(f17(x86531),f15(x86532)),f16(f17(x86531)))), % 201.12/201.14 inference(scs_inference,[],[1357,5014,7027,6669,4972,7148,7048,4970,4971,7052,8497,8015,6077,5129,6860,8321,8579,8446,7666,8079,8574,7056,12,8,820,149,6,13,9,2,597,15,148,10,7,11,349,14,837,854,871,81,79,75,76,87,92,85,80,144,83,84,90,27,3,19,24])). % 201.12/201.14 cnf(8658,plain, % 201.12/201.14 (P16(f9(f17(f10(x86581,a1))),f10(x86581,f14(x86582)))), % 201.12/201.14 inference(scs_inference,[],[1357,8650,5014,7027,6669,4972,7148,7048,4970,4971,7052,8497,6742,8015,6077,6835,5129,6860,8321,8579,8446,7666,8079,8558,8574,7056,12,8,820,149,6,13,9,2,597,15,148,10,7,11,349,14,837,854,871,81,79,75,76,87,92,85,80,144,83,84,90,27,3,19,24,26,18])). % 201.12/201.14 cnf(8667,plain, % 201.12/201.14 (P1(f10(f16(a1),a1))), % 201.12/201.14 inference(scs_inference,[],[1357,8650,68,5014,7027,6669,4972,7148,7048,4970,6437,4971,7052,8497,6742,8015,6077,7122,8512,6835,7033,5129,6860,8321,8579,8446,7666,8079,8558,7370,8487,7385,8574,7056,12,8,820,149,6,13,9,2,597,15,148,10,7,11,349,14,837,854,871,81,79,75,76,87,92,85,80,144,83,84,90,27,3,19,24,26,18,88,91,100,16])). % 201.12/201.14 cnf(8669,plain, % 201.12/201.14 (P13(f9(f17(f10(x86691,a1))),f17(f10(x86691,f14(x86692))))), % 201.12/201.14 inference(scs_inference,[],[1357,8650,47,68,5014,7027,6669,4972,7148,7048,4970,113,6437,4971,7052,8497,6742,8015,6077,7122,8512,6835,7033,5129,6860,8321,8579,8446,7666,8079,8558,7370,8487,7385,8574,7056,12,8,820,149,6,13,9,2,597,15,148,10,7,11,349,14,837,854,871,81,79,75,76,87,92,85,80,144,83,84,90,27,3,19,24,26,18,88,91,100,16,107])). % 201.12/201.14 cnf(8673,plain, % 201.12/201.14 (P1(f10(f16(a1),f14(x86731)))), % 201.12/201.14 inference(scs_inference,[],[1357,8650,47,68,5014,7027,6669,4972,7148,7048,4970,113,6437,4971,7052,8497,6742,8015,6077,7122,8512,6835,7033,5129,6860,8321,8579,8446,7666,8079,8558,7370,8487,7385,8574,7056,12,8,820,149,6,13,9,2,597,15,148,10,7,11,349,14,837,854,871,81,79,75,76,87,92,85,80,144,83,84,90,27,3,19,24,26,18,88,91,100,16,107,1375])). % 201.12/201.14 cnf(8718,plain, % 201.12/201.14 (P5(f9(f17(x87181)),f16(x87181))), % 201.12/201.14 inference(scs_inference,[],[4972,7148,4941,4970,7052,4971,6742,7056,6835,4962,6863,8382,7826,8669,7124,12,8,820,149,6,13,7,2,15,148,597,10,9,11,349,14,837,854,871,81,79,75,80,76,87,92,144,85,84,83,90])). % 201.12/201.14 cnf(8722,plain, % 201.12/201.14 (~E(f10(f17(a2),f15(x87221)),f16(f17(a1)))), % 201.12/201.14 inference(scs_inference,[],[5016,4972,7148,4941,4970,7052,4971,6742,7056,6835,8558,4962,6863,8382,8653,7826,8669,7124,12,8,820,149,6,13,7,2,15,148,597,10,9,11,349,14,837,854,871,81,79,75,80,76,87,92,144,85,84,83,90,27,3])). % 201.12/201.14 cnf(8734,plain, % 201.12/201.14 (P1(f10(f16(a2),f15(x87341)))), % 201.12/201.14 inference(scs_inference,[],[68,4974,5016,7027,4972,7148,4941,4970,7052,4971,6742,7056,6835,8119,8558,7126,8487,7527,4962,6863,8382,8653,7826,8669,8595,8546,7124,8152,12,8,820,149,6,13,7,2,15,148,597,10,9,11,349,14,837,854,871,81,79,75,80,76,87,92,144,85,84,83,90,27,3,24,26,18,88,16])). % 201.12/201.14 cnf(8751,plain, % 201.12/201.14 (E(f9(f6(a2)),f9(f6(a1)))), % 201.12/201.14 inference(scs_inference,[],[7148,4970,4971,8,12,820,6,13])). % 201.12/201.14 cnf(8796,plain, % 201.12/201.14 (~E(f10(f16(x87961),f15(x87962)),f16(f16(x87961)))), % 201.12/201.14 inference(scs_inference,[],[7027,7148,4970,4971,6742,7056,5098,8015,8487,7124,8050,5950,8152,8669,5038,8458,8722,7338,7128,8153,8,12,820,6,13,149,10,597,148,7,9,15,2,11,349,837,14,871,854,81,75,79,87,76,80,85,92,84,83,144,90,5047,27,3,24])). % 201.12/201.14 cnf(8798,plain, % 201.12/201.14 (P16(f9(f17(f10(a2,a1))),f10(a1,f14(x87981)))), % 201.12/201.14 inference(scs_inference,[],[4974,7027,7148,4970,4971,6742,7056,5098,8015,8487,7124,8050,5950,8152,8669,5038,8458,8722,7338,7128,8658,8153,8,12,820,6,13,149,10,597,148,7,9,15,2,11,349,837,14,871,854,81,75,79,87,76,80,85,92,84,83,144,90,5047,27,3,24,18])). % 201.12/201.14 cnf(8812,plain, % 201.12/201.14 (P13(f9(f17(f10(a2,a1))),f17(f10(a1,f14(x88121))))), % 201.12/201.14 inference(scs_inference,[],[47,68,4974,7027,259,7148,4970,4971,6742,7056,113,5098,8015,8487,7124,8050,5950,8152,8669,5038,8458,8722,7338,8718,7522,8641,7040,7128,8658,8153,8,12,820,6,13,149,10,597,148,7,9,15,2,11,349,837,14,871,854,81,75,79,87,76,80,85,92,84,83,144,90,5047,27,3,24,18,26,88,91,100,107])). % 201.12/201.14 cnf(8875,plain, % 201.12/201.14 (P13(f9(f17(x88751)),f16(x88751))), % 201.12/201.14 inference(scs_inference,[],[68,4975,1356,7027,4970,4971,6742,8015,7124,5022,8386,7128,8669,5901,7338,8718,8153,8751,8796,8812,8055,8233,8798,7132,7892,8,12,820,13,6,149,10,597,148,7,15,2,11,9,14,349,837,871,854,81,75,79,76,80,87,92,85,83,90,144,84,3,27,24,18,26,88])). % 201.12/201.14 cnf(9607,plain, % 201.12/201.14 (P16(f16(a2),f16(a1))), % 201.12/201.14 inference(scs_inference,[],[60,4945,5209,8578,3,18])). % 201.12/201.14 cnf(9677,plain, % 201.12/201.14 (~P13(f16(a3),f6(a3))), % 201.12/201.14 inference(scs_inference,[],[68,5158,5057,6642,3,88,92])). % 201.12/201.14 cnf(9723,plain, % 201.12/201.14 (~E(f16(f16(x97231)),f17(a1))), % 201.12/201.14 inference(scs_inference,[],[6897,5865])). % 201.12/201.14 cnf(9724,plain, % 201.12/201.14 (P13(x97241,f16(x97241))), % 201.12/201.14 inference(rename_variables,[],[6897])). % 201.12/201.14 cnf(9727,plain, % 201.12/201.14 (P13(x97271,f16(x97271))), % 201.12/201.14 inference(rename_variables,[],[6897])). % 201.12/201.14 cnf(9730,plain, % 201.12/201.14 (P13(x97301,f16(x97301))), % 201.12/201.14 inference(rename_variables,[],[6897])). % 201.12/201.14 cnf(9733,plain, % 201.12/201.14 (P13(x97331,f16(x97331))), % 201.12/201.14 inference(rename_variables,[],[6897])). % 201.12/201.14 cnf(9736,plain, % 201.12/201.14 (P13(x97361,f16(x97361))), % 201.12/201.14 inference(rename_variables,[],[6897])). % 201.12/201.14 cnf(9738,plain, % 201.12/201.14 (P13(x97381,f16(x97381))), % 201.12/201.14 inference(rename_variables,[],[6897])). % 201.12/201.14 cnf(9740,plain, % 201.12/201.14 (P13(x97401,f16(x97401))), % 201.12/201.14 inference(rename_variables,[],[6897])). % 201.12/201.14 cnf(9742,plain, % 201.12/201.14 (P13(x97421,f16(x97421))), % 201.12/201.14 inference(rename_variables,[],[6897])). % 201.12/201.14 cnf(9743,plain, % 201.12/201.14 (P6(f10(f16(a1),a1))), % 201.12/201.14 inference(scs_inference,[],[8673,6897,9724,9727,9730,9733,9736,9738,9740,5865,5762,5707,5548,6436,6407,6379,6341,1430])). % 201.12/201.14 cnf(9746,plain, % 201.12/201.14 (P13(x97461,f16(x97461))), % 201.12/201.14 inference(rename_variables,[],[6897])). % 201.12/201.14 cnf(9752,plain, % 201.12/201.14 (P13(x97521,f16(x97521))), % 201.12/201.14 inference(rename_variables,[],[6897])). % 201.12/201.14 cnf(9765,plain, % 201.12/201.14 (P16(x97651,x97651)), % 201.12/201.14 inference(rename_variables,[],[60])). % 201.12/201.14 cnf(9766,plain, % 201.12/201.14 (~P5(f17(a3),f16(f16(a1)))), % 201.12/201.14 inference(scs_inference,[],[69,60,8491,7691,8521,8673,7816,9607,7892,7479,7695,6897,9724,9727,9730,9733,9736,9738,9740,9742,9746,9752,5865,5762,5707,5548,6436,6407,6379,6341,1430,6286,82,72,5315,5331,71,25,16,90,87,17,100])). % 201.12/201.14 cnf(9770,plain, % 201.12/201.14 (~P5(f10(f17(a4),f17(a8)),f17(a8))), % 201.12/201.14 inference(scs_inference,[],[69,60,6858,8491,7691,8521,8673,7816,9607,8875,7892,7479,7695,6897,9724,9727,9730,9733,9736,9738,9740,9742,9746,9752,5865,5762,5707,5548,6436,6407,6379,6341,1430,6286,82,72,5315,5331,71,25,16,90,87,17,100,92,88])). % 201.12/201.14 cnf(9773,plain, % 201.12/201.14 (E(f10(a1,x97731),f10(f14(x97732),x97731))), % 201.12/201.14 inference(scs_inference,[],[69,60,6858,8491,7691,8521,8673,7816,9607,8875,7892,7479,7695,6897,9724,9727,9730,9733,9736,9738,9740,9742,9746,9752,5255,5865,5762,5707,5548,6436,6407,6379,6341,1430,6286,82,72,5315,5331,71,25,16,90,87,17,100,92,88,14])). % 201.12/201.14 cnf(9777,plain, % 201.12/201.14 (E(f10(x97771,a2),f10(x97771,f14(x97772)))), % 201.12/201.14 inference(scs_inference,[],[69,60,6858,8491,7691,8521,8673,7816,9607,8875,7892,7479,7695,7598,6897,9724,9727,9730,9733,9736,9738,9740,9742,9746,9752,5166,5201,5255,5865,5762,5707,5548,6436,6407,6379,6341,1430,6286,82,72,5315,5331,71,25,16,90,87,17,100,92,88,14,11,18,15])). % 201.12/201.14 cnf(9786,plain, % 201.12/201.14 (E(f16(a2),f16(f14(x97861)))), % 201.12/201.14 inference(scs_inference,[],[69,61,60,6785,6858,8491,7691,8521,8673,7816,6467,9607,6397,8875,7892,7479,7695,7598,6897,9724,9727,9730,9733,9736,9738,9740,9742,9746,9752,5166,5201,5255,5243,5865,5762,5707,5548,6436,6407,6379,6341,1430,6286,82,72,5315,5331,71,25,16,90,87,17,100,92,88,14,11,18,15,7,9,13,2,148,6,26,8])). % 201.12/201.14 cnf(9799,plain, % 201.12/201.14 (P9(f17(x97991))), % 201.12/201.14 inference(rename_variables,[],[47])). % 201.12/201.14 cnf(9801,plain, % 201.12/201.14 (~P5(f10(f17(a3),f17(a2)),f16(a2))), % 201.12/201.14 inference(scs_inference,[],[69,37,47,61,60,9765,6785,6858,8491,7691,7776,8521,8673,7996,7816,6467,9607,6397,8875,7892,7479,7695,7598,7785,5151,6897,9724,9727,9730,9733,9736,9738,9740,9742,9746,9752,5166,5201,5255,5243,5865,5762,5707,5548,6436,6407,6379,6341,1430,6286,82,72,5315,5331,71,25,16,90,87,17,100,92,88,14,11,18,15,7,9,13,2,148,6,26,8,12,3,27,4152,4463,4453,4443,98,93])). % 201.12/201.14 cnf(9803,plain, % 201.12/201.14 (~P16(f10(f17(a3),f17(a1)),a1)), % 201.12/201.14 inference(scs_inference,[],[69,37,47,9799,61,60,9765,6785,6858,6932,8491,7691,7776,8521,8673,7996,7385,7816,6467,9607,6397,8875,7892,7479,7695,7598,7785,5151,6897,9724,9727,9730,9733,9736,9738,9740,9742,9746,9752,5166,5201,5255,5243,5865,5762,5707,5548,6436,6407,6379,6341,1430,6286,82,72,5315,5331,71,25,16,90,87,17,100,92,88,14,11,18,15,7,9,13,2,148,6,26,8,12,3,27,4152,4463,4453,4443,98,93,107])). % 201.12/201.14 cnf(9817,plain, % 201.12/201.14 (~P13(x98171,f10(f16(a1),a1))), % 201.12/201.14 inference(scs_inference,[],[8667,82])). % 201.12/201.14 cnf(9819,plain, % 201.12/201.14 (E(f10(f16(a2),f15(x98191)),a1)), % 201.12/201.14 inference(scs_inference,[],[8734,8667,82,71])). % 201.12/201.14 cnf(9822,plain, % 201.12/201.14 (~P5(f10(f17(a3),f17(a1)),f16(a1))), % 201.12/201.14 inference(scs_inference,[],[8734,9803,8667,82,71,4443,93])). % 201.12/201.14 cnf(9827,plain, % 201.12/201.14 (P5(f10(f17(a4),f17(a8)),f16(a4))), % 201.12/201.14 inference(scs_inference,[],[35,7075,8734,7545,9803,8667,6707,6897,82,71,4443,93,25,16,90])). % 201.12/201.14 cnf(9841,plain, % 201.12/201.14 (E(f10(x98411,a1),f10(x98411,f15(x98412)))), % 201.12/201.14 inference(scs_inference,[],[69,35,7075,9766,7749,8734,9801,7545,9803,7816,8667,6707,7978,8157,5037,6897,5255,5243,82,71,4443,93,25,16,90,87,100,92,88,14,18,11,15])). % 201.12/201.14 cnf(9847,plain, % 201.12/201.14 (E(f16(a1),f16(f14(x98471)))), % 201.12/201.14 inference(scs_inference,[],[69,35,6921,7075,9766,7749,8734,9801,7545,9803,7816,8667,6361,6707,7978,8157,5037,6897,5255,5243,82,71,4443,93,25,16,90,87,100,92,88,14,18,11,15,2,9,148,13,7,8])). % 201.12/201.14 cnf(9850,plain, % 201.12/201.14 (E(f10(a1,x98501),f10(f14(x98502),x98501))), % 201.12/201.14 inference(rename_variables,[],[9773])). % 201.12/201.14 cnf(9859,plain, % 201.12/201.14 (~P16(f10(f17(a3),f17(a1)),a2)), % 201.12/201.14 inference(scs_inference,[],[69,35,47,6921,7075,9766,7749,9773,9850,9777,8734,6824,9801,7545,9803,7385,7816,8667,6361,6707,7978,8157,5037,5183,6897,5255,5243,82,71,4443,93,25,16,90,87,100,92,88,14,18,11,15,2,9,148,13,7,8,12,3,27,243,2293,4463,4453,107])). % 201.12/201.14 cnf(10003,plain, % 201.12/201.14 (P16(x100031,x100031)), % 201.12/201.14 inference(rename_variables,[],[60])). % 201.12/201.14 cnf(10006,plain, % 201.12/201.14 (P16(f16(a1),f16(a2))), % 201.12/201.14 inference(scs_inference,[],[60,10003,9677,5051,4974,5025,17,88,18])). % 201.12/201.14 cnf(10744,plain, % 201.12/201.14 (P13(x107441,f16(x107441))), % 201.12/201.14 inference(rename_variables,[],[6897])). % 201.12/201.14 cnf(10766,plain, % 201.12/201.14 ($false), % 201.12/201.14 inference(scs_inference,[],[59,7059,9723,9822,9827,9859,6858,6913,6894,10006,6989,6707,6883,6579,5003,5117,9817,9743,9841,9847,9819,9770,615,9786,8512,8157,7027,5030,6897,10744,47,5243,68,42,4755,4771,4739,12,149,11,13,8,9,71,4907,4912,754,93,90,92,87,2,19,96,77,27,26,100,3,97,25,88,24,18,17,107]), % 201.12/201.14 ['proof']). % 201.12/201.14 % SZS output end Proof % 201.12/201.14 % Total time :200.370000s %------------------------------------------------------------------------------