%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU114+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 : n028.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:05 EDT 2024 % Result : Theorem 180.83s 180.81s % Output : CNFRefutation 180.83s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SEU114+1 : TPTP v8.2.0. Released v3.2.0. % 0.10/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.11/0.32 % Computer : n028.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Fri Jun 21 17:01:39 EDT 2024 % 0.11/0.33 % CPUTime : % 0.19/0.57 start to proof:theBenchmark % 180.83/180.78 %------------------------------------------- % 180.83/180.78 % File :CSE---1.7 % 180.83/180.78 % Problem :theBenchmark % 180.83/180.78 % Transform :cnf % 180.83/180.78 % Format :tptp:raw % 180.83/180.78 % Command :java -jar mcs_scs.jar %d %s % 180.83/180.78 % 180.83/180.78 % Result :Theorem 180.170000s % 180.83/180.78 % Output :CNFRefutation 180.170000s % 180.83/180.78 %------------------------------------------- % 180.83/180.80 %------------------------------------------------------------------------------ % 180.83/180.80 % File : SEU114+1 : TPTP v8.2.0. Released v3.2.0. % 180.83/180.80 % Domain : Set theory % 180.83/180.80 % Problem : Boolean domains, theorem 27 % 180.83/180.80 % Version : [Urb06] axioms : Especial. % 180.83/180.80 % English : % 180.83/180.80 % 180.83/180.80 % Refs : [TD90] Trybulec & Darmochwal (1990), Boolean Domains % 180.83/180.80 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 180.83/180.80 % Source : [Urb06] % 180.83/180.80 % Names : finsub_1__t27_finsub_1 [Urb06] % 180.83/180.80 % 180.83/180.80 % Status : Theorem % 180.83/180.80 % Rating : 0.25 v8.2.0, 0.22 v8.1.0, 0.25 v7.4.0, 0.20 v7.3.0, 0.21 v7.2.0, 0.17 v7.1.0, 0.13 v7.0.0, 0.20 v6.4.0, 0.27 v6.3.0, 0.21 v6.2.0, 0.32 v6.1.0, 0.37 v6.0.0, 0.30 v5.5.0, 0.44 v5.4.0, 0.46 v5.3.0, 0.48 v5.2.0, 0.30 v5.1.0, 0.38 v5.0.0, 0.42 v4.1.0, 0.43 v4.0.1, 0.52 v4.0.0, 0.50 v3.7.0, 0.40 v3.5.0, 0.42 v3.3.0, 0.50 v3.2.0 % 180.83/180.80 % Syntax : Number of formulae : 36 ( 8 unt; 0 def) % 180.83/180.80 % Number of atoms : 97 ( 5 equ) % 180.83/180.80 % Maximal formula atoms : 10 ( 2 avg) % 180.83/180.80 % Number of connectives : 78 ( 17 ~; 1 |; 37 &) % 180.83/180.80 % ( 5 <=>; 18 =>; 0 <=; 0 <~>) % 180.83/180.80 % Maximal formula depth : 12 ( 5 avg) % 180.83/180.80 % Maximal term depth : 2 ( 1 avg) % 180.83/180.80 % Number of predicates : 17 ( 16 usr; 0 prp; 1-2 aty) % 180.83/180.80 % Number of functors : 3 ( 3 usr; 1 con; 0-1 aty) % 180.83/180.80 % Number of variables : 60 ( 50 !; 10 ?) % 180.83/180.80 % SPC : FOF_THM_RFO_SEQ % 180.83/180.80 % 180.83/180.80 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 180.83/180.80 % library, www.mizar.org % 180.83/180.80 %------------------------------------------------------------------------------ % 180.83/180.80 fof(antisymmetry_r2_hidden,axiom, % 180.83/180.80 ! [A,B] : % 180.83/180.80 ( in(A,B) % 180.83/180.80 => ~ in(B,A) ) ). % 180.83/180.80 % 180.83/180.80 fof(cc1_finset_1,axiom, % 180.83/180.80 ! [A] : % 180.83/180.80 ( empty(A) % 180.83/180.80 => finite(A) ) ). % 180.83/180.80 % 180.83/180.80 fof(cc1_finsub_1,axiom, % 180.83/180.80 ! [A] : % 180.83/180.80 ( preboolean(A) % 180.83/180.80 => ( cup_closed(A) % 180.83/180.80 & diff_closed(A) ) ) ). % 180.83/180.80 % 180.83/180.80 fof(cc2_finset_1,axiom, % 180.83/180.80 ! [A] : % 180.83/180.80 ( finite(A) % 180.83/180.80 => ! [B] : % 180.83/180.80 ( element(B,powerset(A)) % 180.83/180.80 => finite(B) ) ) ). % 180.83/180.80 % 180.83/180.80 fof(cc2_finsub_1,axiom, % 180.83/180.80 ! [A] : % 180.83/180.80 ( ( cup_closed(A) % 180.83/180.80 & diff_closed(A) ) % 180.83/180.80 => preboolean(A) ) ). % 180.83/180.80 % 180.83/180.80 fof(cc3_finsub_1,axiom, % 180.83/180.80 ! [A,B] : % 180.83/180.80 ( element(B,finite_subsets(A)) % 180.83/180.80 => finite(B) ) ). % 180.83/180.80 % 180.83/180.80 fof(d10_xboole_0,axiom, % 180.83/180.80 ! [A,B] : % 180.83/180.80 ( A = B % 180.83/180.80 <=> ( subset(A,B) % 180.83/180.80 & subset(B,A) ) ) ). % 180.83/180.80 % 180.83/180.80 fof(d3_tarski,axiom, % 180.83/180.80 ! [A,B] : % 180.83/180.80 ( subset(A,B) % 180.83/180.80 <=> ! [C] : % 180.83/180.80 ( in(C,A) % 180.83/180.80 => in(C,B) ) ) ). % 180.83/180.80 % 180.83/180.80 fof(d5_finsub_1,axiom, % 180.83/180.80 ! [A,B] : % 180.83/180.80 ( preboolean(B) % 180.83/180.80 => ( B = finite_subsets(A) % 180.83/180.80 <=> ! [C] : % 180.83/180.80 ( in(C,B) % 180.83/180.80 <=> ( subset(C,A) % 180.83/180.80 & finite(C) ) ) ) ) ). % 180.83/180.80 % 180.83/180.80 fof(dt_k5_finsub_1,axiom, % 180.83/180.80 ! [A] : preboolean(finite_subsets(A)) ). % 180.83/180.80 % 180.83/180.80 fof(existence_m1_subset_1,axiom, % 180.83/180.80 ! [A] : % 180.83/180.80 ? [B] : element(B,A) ). % 180.83/180.80 % 180.83/180.80 fof(fc1_finsub_1,axiom, % 180.83/180.80 ! [A] : % 180.83/180.80 ( ~ empty(powerset(A)) % 180.83/180.80 & cup_closed(powerset(A)) % 180.83/180.80 & diff_closed(powerset(A)) % 180.83/180.81 & preboolean(powerset(A)) ) ). % 180.83/180.81 % 180.83/180.81 fof(fc1_subset_1,axiom, % 180.83/180.81 ! [A] : ~ empty(powerset(A)) ). % 180.83/180.81 % 180.83/180.81 fof(fc1_xboole_0,axiom, % 180.83/180.81 empty(empty_set) ). % 180.83/180.81 % 180.83/180.81 fof(fc2_finsub_1,axiom, % 180.83/180.81 ! [A] : % 180.83/180.81 ( ~ empty(finite_subsets(A)) % 180.83/180.81 & cup_closed(finite_subsets(A)) % 180.83/180.81 & diff_closed(finite_subsets(A)) % 180.83/180.81 & preboolean(finite_subsets(A)) ) ). % 180.83/180.81 % 180.83/180.81 fof(rc1_finset_1,axiom, % 180.83/180.81 ? [A] : % 180.83/180.81 ( ~ empty(A) % 180.83/180.81 & finite(A) ) ). % 180.83/180.81 % 180.83/180.81 fof(rc1_finsub_1,axiom, % 180.83/180.81 ? [A] : % 180.83/180.81 ( ~ empty(A) % 180.83/180.81 & cup_closed(A) % 180.83/180.81 & cap_closed(A) % 180.83/180.81 & diff_closed(A) % 180.83/180.81 & preboolean(A) ) ). % 180.83/180.81 % 180.83/180.81 fof(rc1_subset_1,axiom, % 180.83/180.81 ! [A] : % 180.83/180.81 ( ~ empty(A) % 180.83/180.81 => ? [B] : % 180.83/180.81 ( element(B,powerset(A)) % 180.83/180.81 & ~ empty(B) ) ) ). % 180.83/180.81 % 180.83/180.81 fof(rc1_xboole_0,axiom, % 180.83/180.81 ? [A] : empty(A) ). % 180.83/180.81 % 180.83/180.81 fof(rc2_finset_1,axiom, % 180.83/180.81 ! [A] : % 180.83/180.81 ? [B] : % 180.83/180.81 ( element(B,powerset(A)) % 180.83/180.81 & empty(B) % 180.83/180.81 & relation(B) % 180.83/180.81 & function(B) % 180.83/180.81 & one_to_one(B) % 180.83/180.81 & epsilon_transitive(B) % 180.83/180.81 & epsilon_connected(B) % 180.83/180.81 & ordinal(B) % 180.83/180.81 & natural(B) % 180.83/180.81 & finite(B) ) ). % 180.83/180.81 % 180.83/180.81 fof(rc2_subset_1,axiom, % 180.83/180.81 ! [A] : % 180.83/180.81 ? [B] : % 180.83/180.81 ( element(B,powerset(A)) % 180.83/180.81 & empty(B) ) ). % 180.83/180.81 % 180.83/180.81 fof(rc2_xboole_0,axiom, % 180.83/180.81 ? [A] : ~ empty(A) ). % 180.83/180.81 % 180.83/180.81 fof(rc3_finset_1,axiom, % 180.83/180.81 ! [A] : % 180.83/180.81 ( ~ empty(A) % 180.83/180.81 => ? [B] : % 180.83/180.81 ( element(B,powerset(A)) % 180.83/180.81 & ~ empty(B) % 180.83/180.81 & finite(B) ) ) ). % 180.83/180.81 % 180.83/180.81 fof(rc4_finset_1,axiom, % 180.83/180.81 ! [A] : % 180.83/180.81 ( ~ empty(A) % 180.83/180.81 => ? [B] : % 180.83/180.81 ( element(B,powerset(A)) % 180.83/180.81 & ~ empty(B) % 180.83/180.81 & finite(B) ) ) ). % 180.83/180.81 % 180.83/180.81 fof(reflexivity_r1_tarski,axiom, % 180.83/180.81 ! [A,B] : subset(A,A) ). % 180.83/180.81 % 180.83/180.81 fof(t13_finset_1,axiom, % 180.83/180.81 ! [A,B] : % 180.83/180.81 ( ( subset(A,B) % 180.83/180.81 & finite(B) ) % 180.83/180.81 => finite(A) ) ). % 180.83/180.81 % 180.83/180.81 fof(t1_subset,axiom, % 180.83/180.81 ! [A,B] : % 180.83/180.81 ( in(A,B) % 180.83/180.81 => element(A,B) ) ). % 180.83/180.81 % 180.83/180.81 fof(t26_finsub_1,axiom, % 180.83/180.81 ! [A] : subset(finite_subsets(A),powerset(A)) ). % 180.83/180.81 % 180.83/180.81 fof(t27_finsub_1,conjecture, % 180.83/180.81 ! [A] : % 180.83/180.81 ( finite(A) % 180.83/180.81 => finite_subsets(A) = powerset(A) ) ). % 180.83/180.81 % 180.83/180.81 fof(t2_subset,axiom, % 180.83/180.81 ! [A,B] : % 180.83/180.81 ( element(A,B) % 180.83/180.81 => ( empty(B) % 180.83/180.81 | in(A,B) ) ) ). % 180.83/180.81 % 180.83/180.81 fof(t3_subset,axiom, % 180.83/180.81 ! [A,B] : % 180.83/180.81 ( element(A,powerset(B)) % 180.83/180.81 <=> subset(A,B) ) ). % 180.83/180.81 % 180.83/180.81 fof(t4_subset,axiom, % 180.83/180.81 ! [A,B,C] : % 180.83/180.81 ( ( in(A,B) % 180.83/180.81 & element(B,powerset(C)) ) % 180.83/180.81 => element(A,C) ) ). % 180.83/180.81 % 180.83/180.81 fof(t5_subset,axiom, % 180.83/180.81 ! [A,B,C] : % 180.83/180.81 ~ ( in(A,B) % 180.83/180.81 & element(B,powerset(C)) % 180.83/180.81 & empty(C) ) ). % 180.83/180.81 % 180.83/180.81 fof(t6_boole,axiom, % 180.83/180.81 ! [A] : % 180.83/180.81 ( empty(A) % 180.83/180.81 => A = empty_set ) ). % 180.83/180.81 % 180.83/180.81 fof(t7_boole,axiom, % 180.83/180.81 ! [A,B] : % 180.83/180.81 ~ ( in(A,B) % 180.83/180.81 & empty(B) ) ). % 180.83/180.81 % 180.83/180.81 fof(t8_boole,axiom, % 180.83/180.81 ! [A,B] : % 180.83/180.81 ~ ( empty(A) % 180.83/180.81 & A != B % 180.83/180.81 & empty(B) ) ). % 180.83/180.81 % 180.83/180.81 %------------------------------------------------------------------------------ % 180.83/180.81 %------------------------------------------- % 180.83/180.81 % Proof found % 180.83/180.81 % SZS status Theorem for theBenchmark % 180.83/180.81 % SZS output start Proof % 180.83/180.81 %ClaNum:108(EqnAxiom:34) % 180.83/180.81 %VarNum:183(SingletonVarNum:88) % 180.83/180.81 %MaxLitNum:5 % 180.83/180.81 %MaxfuncDepth:1 % 180.83/180.81 %SharedTerms:20 % 180.83/180.81 %goalClause: 38 68 % 180.83/180.81 %singleGoalClaCount:2 % 180.83/180.81 [35]P1(a1) % 180.83/180.81 [36]P1(a2) % 180.83/180.81 [37]P6(a3) % 180.83/180.81 [38]P6(a4) % 180.83/180.81 [39]P9(a11) % 180.83/180.81 [40]P2(a11) % 180.83/180.81 [41]P4(a11) % 180.83/180.81 [42]P3(a11) % 180.83/180.81 [65]~P1(a3) % 180.83/180.81 [66]~P1(a11) % 180.83/180.81 [67]~P1(a5) % 180.83/180.81 [68]~E(f16(a4),f15(a4)) % 180.83/180.81 [60]P16(x601,x601) % 180.83/180.81 [43]P1(f13(x431)) % 180.83/180.81 [44]P1(f14(x441)) % 180.83/180.81 [45]P6(f13(x451)) % 180.83/180.81 [46]P9(f15(x461)) % 180.83/180.81 [48]P9(f16(x481)) % 180.83/180.81 [49]P2(f15(x491)) % 180.83/180.81 [50]P2(f16(x501)) % 180.83/180.81 [51]P4(f15(x511)) % 180.83/180.81 [52]P4(f16(x521)) % 180.83/180.81 [53]P15(f13(x531)) % 180.83/180.81 [54]P10(f13(x541)) % 180.83/180.81 [55]P11(f13(x551)) % 180.83/180.81 [56]P7(f13(x561)) % 180.83/180.81 [57]P8(f13(x571)) % 180.83/180.81 [58]P14(f13(x581)) % 180.83/180.81 [59]P12(f13(x591)) % 180.83/180.81 [61]P5(f8(x611),x611) % 180.83/180.81 [62]P5(f13(x621),f15(x621)) % 180.83/180.81 [63]P5(f14(x631),f15(x631)) % 180.83/180.81 [64]P16(f16(x641),f15(x641)) % 180.83/180.81 [70]~P1(f15(x701)) % 180.83/180.81 [71]~P1(f16(x711)) % 180.83/180.81 [72]~P1(x721)+E(x721,a1) % 180.83/180.81 [73]~P1(x731)+P6(x731) % 180.83/180.81 [74]~P9(x741)+P2(x741) % 180.83/180.81 [75]~P9(x751)+P4(x751) % 180.83/180.81 [76]P1(x761)+P6(f6(x761)) % 180.83/180.81 [77]P1(x771)+P6(f7(x771)) % 180.83/180.81 [82]P1(x821)+~P1(f12(x821)) % 180.83/180.81 [83]P1(x831)+~P1(f6(x831)) % 180.83/180.81 [84]P1(x841)+~P1(f7(x841)) % 180.83/180.81 [86]P1(x861)+P5(f12(x861),f15(x861)) % 180.83/180.81 [87]P1(x871)+P5(f6(x871),f15(x871)) % 180.83/180.81 [88]P1(x881)+P5(f7(x881),f15(x881)) % 180.83/180.81 [80]~E(x801,x802)+P16(x801,x802) % 180.83/180.81 [85]~P1(x851)+~P13(x852,x851) % 180.83/180.81 [91]~P13(x911,x912)+P5(x911,x912) % 180.83/180.81 [96]~P13(x962,x961)+~P13(x961,x962) % 180.83/180.81 [90]P6(x901)+~P5(x901,f16(x902)) % 180.83/180.81 [94]~P16(x941,x942)+P5(x941,f15(x942)) % 180.83/180.81 [97]P16(x971,x972)+~P5(x971,f15(x972)) % 180.83/180.81 [100]P16(x1001,x1002)+P13(f9(x1001,x1002),x1001) % 180.83/180.81 [105]P16(x1051,x1052)+~P13(f9(x1051,x1052),x1052) % 180.83/180.81 [81]~P2(x811)+~P4(x811)+P9(x811) % 180.83/180.81 [78]~P1(x782)+~P1(x781)+E(x781,x782) % 180.83/180.81 [89]~P16(x891,x892)+P6(x891)+~P6(x892) % 180.83/180.81 [92]~P5(x922,x921)+P1(x921)+P13(x922,x921) % 180.83/180.81 [98]~P16(x982,x981)+~P16(x981,x982)+E(x981,x982) % 180.83/180.81 [95]P6(x951)+~P6(x952)+~P5(x951,f15(x952)) % 180.83/180.81 [101]~P16(x1013,x1012)+P13(x1011,x1012)+~P13(x1011,x1013) % 180.83/180.81 [103]~P1(x1031)+~P13(x1032,x1033)+~P5(x1033,f15(x1031)) % 180.83/180.81 [104]P5(x1041,x1042)+~P13(x1041,x1043)+~P5(x1043,f15(x1042)) % 180.83/180.82 [106]~P9(x1061)+P13(f10(x1062,x1061),x1061)+E(x1061,f16(x1062))+P6(f10(x1062,x1061)) % 180.83/180.82 [107]~P9(x1071)+P13(f10(x1072,x1071),x1071)+P16(f10(x1072,x1071),x1072)+E(x1071,f16(x1072)) % 180.83/180.82 [93]~P9(x932)+~P13(x931,x932)+P6(x931)+~E(x932,f16(x933)) % 180.83/180.82 [99]~P9(x993)+~P13(x991,x993)+P16(x991,x992)+~E(x993,f16(x992)) % 180.83/180.82 [108]~P9(x1081)+~P13(f10(x1082,x1081),x1081)+~P16(f10(x1082,x1081),x1082)+E(x1081,f16(x1082))+~P6(f10(x1082,x1081)) % 180.83/180.82 [102]~P6(x1021)+~P9(x1022)+~P16(x1021,x1023)+P13(x1021,x1022)+~E(x1022,f16(x1023)) % 180.83/180.82 %EqnAxiom % 180.83/180.82 [1]E(x11,x11) % 180.83/180.82 [2]E(x22,x21)+~E(x21,x22) % 180.83/180.82 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 180.83/180.82 [4]~E(x41,x42)+E(f13(x41),f13(x42)) % 180.83/180.82 [5]~E(x51,x52)+E(f14(x51),f14(x52)) % 180.83/180.82 [6]~E(x61,x62)+E(f10(x61,x63),f10(x62,x63)) % 180.83/180.82 [7]~E(x71,x72)+E(f10(x73,x71),f10(x73,x72)) % 180.83/180.82 [8]~E(x81,x82)+E(f15(x81),f15(x82)) % 180.83/180.82 [9]~E(x91,x92)+E(f16(x91),f16(x92)) % 180.83/180.82 [10]~E(x101,x102)+E(f6(x101),f6(x102)) % 180.83/180.82 [11]~E(x111,x112)+E(f7(x111),f7(x112)) % 180.83/180.82 [12]~E(x121,x122)+E(f12(x121),f12(x122)) % 180.83/180.82 [13]~E(x131,x132)+E(f9(x131,x133),f9(x132,x133)) % 180.83/180.82 [14]~E(x141,x142)+E(f9(x143,x141),f9(x143,x142)) % 180.83/180.82 [15]~E(x151,x152)+E(f8(x151),f8(x152)) % 180.83/180.82 [16]~P1(x161)+P1(x162)+~E(x161,x162) % 180.83/180.82 [17]P16(x172,x173)+~E(x171,x172)+~P16(x171,x173) % 180.83/180.82 [18]P16(x183,x182)+~E(x181,x182)+~P16(x183,x181) % 180.83/180.82 [19]~P6(x191)+P6(x192)+~E(x191,x192) % 180.83/180.82 [20]~P9(x201)+P9(x202)+~E(x201,x202) % 180.83/180.82 [21]P5(x212,x213)+~E(x211,x212)+~P5(x211,x213) % 180.83/180.82 [22]P5(x223,x222)+~E(x221,x222)+~P5(x223,x221) % 180.83/180.82 [23]~P2(x231)+P2(x232)+~E(x231,x232) % 180.83/180.82 [24]~P4(x241)+P4(x242)+~E(x241,x242) % 180.83/180.82 [25]~P3(x251)+P3(x252)+~E(x251,x252) % 180.83/180.82 [26]P13(x262,x263)+~E(x261,x262)+~P13(x261,x263) % 180.83/180.82 [27]P13(x273,x272)+~E(x271,x272)+~P13(x273,x271) % 180.83/180.82 [28]~P12(x281)+P12(x282)+~E(x281,x282) % 180.83/180.82 [29]~P14(x291)+P14(x292)+~E(x291,x292) % 180.83/180.82 [30]~P8(x301)+P8(x302)+~E(x301,x302) % 180.83/180.82 [31]~P7(x311)+P7(x312)+~E(x311,x312) % 180.83/180.82 [32]~P11(x321)+P11(x322)+~E(x321,x322) % 180.83/180.82 [33]~P10(x331)+P10(x332)+~E(x331,x332) % 180.83/180.82 [34]~P15(x341)+P15(x342)+~E(x341,x342) % 180.83/180.82 % 180.83/180.82 %------------------------------------------- % 180.83/180.83 cnf(110,plain, % 180.83/180.83 (P6(x1101)+~P9(f16(x1102))+~P13(x1101,f16(x1102))), % 180.83/180.83 inference(equality_inference,[],[93])). % 180.83/180.83 cnf(111,plain, % 180.83/180.83 (~P9(f16(x1111))+~P13(x1112,f16(x1111))+P16(x1112,x1111)), % 180.83/180.83 inference(equality_inference,[],[99])). % 180.83/180.83 cnf(112,plain, % 180.83/180.83 (P13(x1121,f16(x1122))+~P6(x1121)+~P16(x1121,x1122)+~P9(f16(x1122))), % 180.83/180.83 inference(equality_inference,[],[102])). % 180.83/180.83 cnf(113,plain, % 180.83/180.83 (~P13(x1131,a1)), % 180.83/180.83 inference(scs_inference,[],[35,85])). % 180.83/180.83 cnf(115,plain, % 180.83/180.83 (P6(f8(f16(x1151)))), % 180.83/180.83 inference(scs_inference,[],[61,35,85,90])). % 180.83/180.83 cnf(116,plain, % 180.83/180.83 (P5(f8(x1161),x1161)), % 180.83/180.83 inference(rename_variables,[],[61])). % 180.83/180.83 cnf(118,plain, % 180.83/180.83 (P16(f8(f15(x1181)),x1181)), % 180.83/180.83 inference(scs_inference,[],[61,116,35,85,90,97])). % 180.83/180.83 cnf(119,plain, % 180.83/180.83 (P5(f8(x1191),x1191)), % 180.83/180.83 inference(rename_variables,[],[61])). % 180.83/180.83 cnf(121,plain, % 180.83/180.83 (P16(a1,x1211)), % 180.83/180.83 inference(scs_inference,[],[61,116,35,85,90,97,100])). % 180.83/180.83 cnf(123,plain, % 180.83/180.83 (P6(f8(f15(a4)))), % 180.83/180.83 inference(scs_inference,[],[38,61,116,119,35,85,90,97,100,95])). % 180.83/180.83 cnf(124,plain, % 180.83/180.83 (P5(f8(x1241),x1241)), % 180.83/180.83 inference(rename_variables,[],[61])). % 180.83/180.83 cnf(126,plain, % 180.83/180.83 (~P16(f15(a4),f16(a4))), % 180.83/180.83 inference(scs_inference,[],[38,68,61,116,119,64,35,85,90,97,100,95,98])). % 180.83/180.83 cnf(129,plain, % 180.83/180.83 (P13(f8(a3),a3)), % 180.83/180.83 inference(scs_inference,[],[38,68,61,116,119,124,64,35,65,85,90,97,100,95,98,92])). % 180.83/180.83 cnf(130,plain, % 180.83/180.83 (P5(f8(x1301),x1301)), % 180.83/180.83 inference(rename_variables,[],[61])). % 180.83/180.83 cnf(132,plain, % 180.83/180.83 (~P13(x1321,f8(f15(a1)))), % 180.83/180.83 inference(scs_inference,[],[38,68,61,116,119,124,130,64,35,65,85,90,97,100,95,98,92,103])). % 180.83/180.83 cnf(133,plain, % 180.83/180.83 (P5(f8(x1331),x1331)), % 180.83/180.83 inference(rename_variables,[],[61])). % 180.83/180.83 cnf(135,plain, % 180.83/180.83 (~P13(f15(a4),f16(f16(a4)))), % 180.83/180.83 inference(scs_inference,[],[38,68,61,116,119,124,130,64,35,48,65,85,90,97,100,95,98,92,103,111])). % 180.83/180.83 cnf(136,plain, % 180.83/180.83 (P9(f16(x1361))), % 180.83/180.83 inference(rename_variables,[],[48])). % 180.83/180.83 cnf(138,plain, % 180.83/180.83 (~E(a1,f15(a4))), % 180.83/180.83 inference(scs_inference,[],[38,68,61,116,119,124,130,64,35,48,65,85,90,97,100,95,98,92,103,111,17])). % 180.83/180.83 cnf(140,plain, % 180.83/180.83 (P16(x1401,x1401)), % 180.83/180.83 inference(rename_variables,[],[60])). % 180.83/180.83 cnf(141,plain, % 180.83/180.83 (~E(a3,f8(f15(a1)))), % 180.83/180.83 inference(scs_inference,[],[38,68,60,61,116,119,124,130,64,35,48,65,85,90,97,100,95,98,92,103,111,17,18,27])). % 180.83/180.83 cnf(142,plain, % 180.83/180.83 (P13(a4,f16(a4))), % 180.83/180.83 inference(scs_inference,[],[38,68,60,140,61,116,119,124,130,64,35,48,136,65,85,90,97,100,95,98,92,103,111,17,18,27,112])). % 180.83/180.83 cnf(146,plain, % 180.83/180.83 (~P13(a3,f8(a3))), % 180.83/180.83 inference(scs_inference,[],[38,68,60,140,61,116,119,124,130,64,35,48,136,65,85,90,97,100,95,98,92,103,111,17,18,27,112,96])). % 180.83/180.83 cnf(148,plain, % 180.83/180.83 (P5(x1481,x1482)+~P13(x1481,f8(f15(x1482)))), % 180.83/180.83 inference(scs_inference,[],[38,68,60,140,61,116,119,124,130,133,64,35,48,136,65,85,90,97,100,95,98,92,103,111,17,18,27,112,96,104])). % 180.83/180.83 cnf(149,plain, % 180.83/180.83 (P5(f8(x1491),x1491)), % 180.83/180.83 inference(rename_variables,[],[61])). % 180.83/180.83 cnf(151,plain, % 180.83/180.83 (P5(x1511,x1512)+~E(f8(x1512),x1511)), % 180.83/180.83 inference(scs_inference,[],[38,68,60,140,61,116,119,124,130,133,149,64,35,48,136,65,85,90,97,100,95,98,92,103,111,17,18,27,112,96,104,21])). % 180.83/180.83 cnf(152,plain, % 180.83/180.83 (P5(f8(x1521),x1522)+~E(x1521,x1522)), % 180.83/180.84 inference(scs_inference,[],[38,68,60,140,61,116,119,124,130,133,149,64,35,48,136,65,85,90,97,100,95,98,92,103,111,17,18,27,112,96,104,21,22])). % 180.83/180.84 cnf(160,plain, % 180.83/180.84 (~P13(x1601,a2)), % 180.83/180.84 inference(scs_inference,[],[36,85])). % 180.83/180.84 cnf(164,plain, % 180.83/180.84 (P16(f13(x1641),x1641)), % 180.83/180.84 inference(scs_inference,[],[142,62,36,85,96,97])). % 180.83/180.84 cnf(166,plain, % 180.83/180.84 (P13(f8(a11),a11)), % 180.83/180.84 inference(scs_inference,[],[142,62,36,61,66,85,96,97,92])). % 180.83/180.84 cnf(167,plain, % 180.83/180.84 (P5(f8(x1671),x1671)), % 180.83/180.84 inference(rename_variables,[],[61])). % 180.83/180.84 cnf(169,plain, % 180.83/180.84 (E(f8(f15(a1)),a1)), % 180.83/180.84 inference(scs_inference,[],[142,118,121,62,36,61,66,85,96,97,92,98])). % 180.83/180.84 cnf(173,plain, % 180.83/180.84 (~P13(x1731,f13(a2))), % 180.83/180.84 inference(scs_inference,[],[142,118,121,62,36,61,66,85,96,97,92,98,103])). % 180.83/180.84 cnf(178,plain, % 180.83/180.84 (P6(f14(a4))), % 180.83/180.84 inference(scs_inference,[],[38,142,118,132,121,62,63,36,61,66,85,96,97,92,98,103,27,95])). % 180.83/180.84 cnf(181,plain, % 180.83/180.84 (P5(a1,f15(a1))), % 180.83/180.84 inference(scs_inference,[],[38,142,118,132,121,62,63,36,61,167,66,85,96,97,92,98,103,27,95,21])). % 180.83/180.84 cnf(183,plain, % 180.83/180.84 (P13(a3,f16(a3))), % 180.83/180.84 inference(scs_inference,[],[38,142,60,118,132,121,62,63,36,37,61,167,48,66,85,96,97,92,98,103,27,95,21,112])). % 180.83/180.84 cnf(187,plain, % 180.83/180.84 (E(a1,f8(f15(a1)))), % 180.83/180.84 inference(scs_inference,[],[38,142,60,118,132,121,62,63,36,37,61,167,48,66,85,96,97,92,98,103,27,95,21,112,2])). % 180.83/180.84 cnf(188,plain, % 180.83/180.84 (P5(f8(a1),f8(f15(a1)))), % 180.83/180.84 inference(scs_inference,[],[38,142,60,118,132,121,62,63,36,37,61,167,48,66,85,96,97,92,98,103,27,95,21,112,2,152])). % 180.83/180.84 cnf(189,plain, % 180.83/180.84 (P16(a2,x1891)), % 180.83/180.84 inference(scs_inference,[],[38,142,60,118,132,121,62,63,36,37,61,167,48,66,85,96,97,92,98,103,27,95,21,112,2,152,100])). % 180.83/180.84 cnf(191,plain, % 180.83/180.84 (~E(a3,a1)), % 180.83/180.84 inference(scs_inference,[],[38,142,60,118,132,121,62,63,141,36,37,61,167,48,66,85,96,97,92,98,103,27,95,21,112,2,152,100,3])). % 180.83/180.84 cnf(192,plain, % 180.83/180.84 (~P6(f8(f15(a1)))+P6(a1)), % 180.83/180.84 inference(scs_inference,[],[38,142,60,118,132,121,62,63,141,36,37,61,167,48,66,85,96,97,92,98,103,27,95,21,112,2,152,100,3,19])). % 180.83/180.84 cnf(204,plain, % 180.83/180.84 (P16(f13(a2),x2041)), % 180.83/180.84 inference(scs_inference,[],[173,100])). % 180.83/180.84 cnf(205,plain, % 180.83/180.84 (~P13(x2051,f13(a2))), % 180.83/180.84 inference(rename_variables,[],[173])). % 180.83/180.84 cnf(207,plain, % 180.83/180.84 (~P13(x2071,f13(x2072))), % 180.83/180.84 inference(scs_inference,[],[173,43,100,85])). % 180.83/180.84 cnf(209,plain, % 180.83/180.84 (~P13(f16(a3),a3)), % 180.83/180.84 inference(scs_inference,[],[183,173,43,100,85,96])). % 180.83/180.84 cnf(211,plain, % 180.83/180.84 (P16(f14(x2111),x2111)), % 180.83/180.84 inference(scs_inference,[],[183,173,43,63,100,85,96,97])). % 180.83/180.84 cnf(213,plain, % 180.83/180.84 (P13(f8(a5),a5)), % 180.83/180.84 inference(scs_inference,[],[183,173,43,63,61,67,100,85,96,97,92])). % 180.83/180.84 cnf(219,plain, % 180.83/180.84 (E(f13(a2),a2)), % 180.83/180.84 inference(scs_inference,[],[183,164,173,189,43,63,61,67,100,85,96,97,92,103,98])). % 180.83/180.84 cnf(220,plain, % 180.83/180.84 (P16(f13(x2201),x2201)), % 180.83/180.84 inference(rename_variables,[],[164])). % 180.83/180.84 cnf(223,plain, % 180.83/180.84 (~E(f16(a3),f13(a2))), % 180.83/180.84 inference(scs_inference,[],[183,164,173,205,189,43,63,61,67,100,85,96,97,92,103,98,27])). % 180.83/180.84 cnf(225,plain, % 180.83/180.84 (P12(a2)), % 180.83/180.84 inference(scs_inference,[],[183,164,173,205,189,43,63,61,67,59,100,85,96,97,92,103,98,27,28])). % 180.83/180.84 cnf(227,plain, % 180.83/180.84 (P1(f8(f15(a1)))), % 180.83/180.84 inference(scs_inference,[],[187,183,164,173,205,189,43,63,61,35,67,59,100,85,96,97,92,103,98,27,28,16])). % 180.83/180.84 cnf(228,plain, % 180.83/180.84 (P16(f14(f13(a2)),a2)), % 180.83/180.84 inference(scs_inference,[],[187,183,164,173,205,189,43,63,61,35,67,59,100,85,96,97,92,103,98,27,28,16,18])). % 180.83/180.84 cnf(232,plain, % 180.83/180.84 (P5(a2,f15(a2))), % 180.83/180.84 inference(scs_inference,[],[126,187,183,164,220,173,205,129,189,43,63,61,62,35,67,59,100,85,96,97,92,103,98,27,28,16,18,17,26,21])). % 180.83/180.84 cnf(234,plain, % 180.83/180.84 (P13(f14(a4),f16(f14(a4)))), % 180.83/180.84 inference(scs_inference,[],[126,178,187,183,60,164,220,173,205,129,189,43,63,61,62,48,35,67,59,100,85,96,97,92,103,98,27,28,16,18,17,26,21,112])). % 180.83/180.84 cnf(239,plain, % 180.83/180.84 (E(a2,f13(a2))), % 180.83/180.84 inference(scs_inference,[],[126,178,187,183,60,164,220,173,205,129,189,43,63,61,62,48,35,67,59,100,85,96,97,92,103,98,27,28,16,18,17,26,21,112,152,2])). % 180.83/180.84 cnf(241,plain, % 180.83/180.84 (P8(a2)), % 180.83/180.84 inference(scs_inference,[],[126,178,169,187,183,60,164,220,173,205,129,189,43,63,61,62,48,35,67,57,59,100,85,96,97,92,103,98,27,28,16,18,17,26,21,112,152,2,29,30])). % 180.83/180.84 cnf(243,plain, % 180.83/180.84 (P7(a2)), % 180.83/180.84 inference(scs_inference,[],[126,178,169,187,183,60,164,220,173,205,129,189,43,63,61,62,48,35,67,56,57,59,100,85,96,97,92,103,98,27,28,16,18,17,26,21,112,152,2,29,30,31])). % 180.83/180.84 cnf(245,plain, % 180.83/180.84 (P11(a2)), % 180.83/180.84 inference(scs_inference,[],[126,178,169,187,183,60,164,220,173,205,129,189,43,63,61,62,48,35,67,55,56,57,59,100,85,96,97,92,103,98,27,28,16,18,17,26,21,112,152,2,29,30,31,32])). % 180.83/180.84 cnf(247,plain, % 180.83/180.84 (P10(a2)), % 180.83/180.84 inference(scs_inference,[],[126,178,169,187,183,60,164,220,173,205,129,189,43,63,61,62,48,35,67,54,55,56,57,59,100,85,96,97,92,103,98,27,28,16,18,17,26,21,112,152,2,29,30,31,32,33])). % 180.83/180.84 cnf(249,plain, % 180.83/180.84 (P15(a2)), % 180.83/180.84 inference(scs_inference,[],[126,178,169,187,183,60,164,220,173,205,129,189,43,63,61,62,48,35,67,53,54,55,56,57,59,100,85,96,97,92,103,98,27,28,16,18,17,26,21,112,152,2,29,30,31,32,33,34])). % 180.83/180.84 cnf(251,plain, % 180.83/180.84 (P6(a2)), % 180.83/180.84 inference(scs_inference,[],[126,178,169,187,183,60,164,220,173,205,129,189,43,45,63,61,62,48,35,67,53,54,55,56,57,59,100,85,96,97,92,103,98,27,28,16,18,17,26,21,112,152,2,29,30,31,32,33,34,19])). % 180.83/180.84 cnf(253,plain, % 180.83/180.84 (~E(f16(a3),a2)), % 180.83/180.84 inference(scs_inference,[],[126,178,169,187,183,60,164,220,173,205,129,189,43,45,63,61,62,48,35,67,53,54,55,56,57,59,100,85,96,97,92,103,98,27,28,16,18,17,26,21,112,152,2,29,30,31,32,33,34,19,3])). % 180.83/180.84 cnf(261,plain, % 180.83/180.84 (P16(f13(x2611),x2612)), % 180.83/180.84 inference(scs_inference,[],[207,100])). % 180.83/180.84 cnf(262,plain, % 180.83/180.84 (~P13(x2621,f13(x2622))), % 180.83/180.84 inference(rename_variables,[],[207])). % 180.83/180.84 cnf(264,plain, % 180.83/180.84 (~P13(x2641,f14(x2642))), % 180.83/180.84 inference(scs_inference,[],[207,44,100,85])). % 180.83/180.84 cnf(266,plain, % 180.83/180.84 (~P13(a11,f8(a11))), % 180.83/180.84 inference(scs_inference,[],[207,166,44,100,85,96])). % 180.83/180.84 cnf(268,plain, % 180.83/180.84 (P5(f8(a2),f13(a2))), % 180.83/180.84 inference(scs_inference,[],[239,207,166,44,100,85,96,152])). % 180.83/180.84 cnf(269,plain, % 180.83/180.84 (E(f14(f13(a2)),f13(a2))), % 180.83/180.84 inference(scs_inference,[],[239,211,207,204,166,44,100,85,96,152,98])). % 180.83/180.84 cnf(270,plain, % 180.83/180.84 (P16(f14(x2701),x2701)), % 180.83/180.84 inference(rename_variables,[],[211])). % 180.83/180.84 cnf(276,plain, % 180.83/180.84 (P14(a2)), % 180.83/180.84 inference(scs_inference,[],[219,239,181,211,207,204,166,44,58,70,100,85,96,152,98,92,29])). % 180.83/180.84 cnf(278,plain, % 180.83/180.84 (~E(f16(f14(a4)),f13(x2781))), % 180.83/180.84 inference(scs_inference,[],[234,219,239,181,211,207,262,204,166,44,58,70,100,85,96,152,98,92,29,27])). % 180.83/180.84 cnf(284,plain, % 180.83/180.84 (P5(f13(a2),f15(f13(a2)))), % 180.83/180.84 inference(scs_inference,[],[126,187,234,219,239,181,211,270,207,262,204,223,166,44,63,58,70,100,85,96,152,98,92,29,27,3,17,26,21])). % 180.83/180.84 cnf(286,plain, % 180.83/180.84 (P13(a2,f16(a2))), % 180.83/180.84 inference(scs_inference,[],[126,187,234,219,239,251,60,181,211,270,207,262,204,223,166,44,63,48,58,70,100,85,96,152,98,92,29,27,3,17,26,21,112])). % 180.83/180.84 cnf(290,plain, % 180.83/180.84 (E(f13(a2),f14(f13(a2)))), % 180.83/180.84 inference(scs_inference,[],[126,187,234,219,239,251,60,181,211,270,207,262,204,223,166,44,63,48,58,70,100,85,96,152,98,92,29,27,3,17,26,21,112,2])). % 180.83/180.84 cnf(310,plain, % 180.83/180.84 (P16(f14(x3101),x3102)), % 180.83/180.84 inference(scs_inference,[],[264,100])). % 180.83/180.84 cnf(311,plain, % 180.83/180.84 (~P13(x3111,f14(x3112))), % 180.83/180.84 inference(rename_variables,[],[264])). % 180.83/180.84 cnf(313,plain, % 180.83/180.84 (~P13(a5,f8(a5))), % 180.83/180.84 inference(scs_inference,[],[264,213,100,96])). % 180.83/180.84 cnf(315,plain, % 180.83/180.84 (~P5(f15(a4),f16(f16(a4)))), % 180.83/180.84 inference(scs_inference,[],[264,135,213,71,100,96,92])). % 180.83/180.84 cnf(322,plain, % 180.83/180.84 (E(f14(f13(a2)),a2)), % 180.83/180.84 inference(scs_inference,[],[290,228,189,264,135,213,71,53,58,100,96,92,34,29,98])). % 180.83/180.84 cnf(323,plain, % 180.83/180.84 (P16(a2,x3231)), % 180.83/180.84 inference(rename_variables,[],[189])). % 180.83/180.84 cnf(329,plain, % 180.83/180.84 (~E(a2,f15(a4))), % 180.83/180.84 inference(scs_inference,[],[126,290,286,239,228,189,323,264,311,135,278,213,71,53,58,100,96,92,34,29,98,27,3,17])). % 180.83/180.84 cnf(331,plain, % 180.83/180.84 (P5(a2,f15(f13(a2)))), % 180.83/180.84 inference(scs_inference,[],[126,219,290,286,239,228,189,323,264,311,135,278,284,213,71,53,58,100,96,92,34,29,98,27,3,17,21])). % 180.83/180.84 cnf(332,plain, % 180.83/180.84 (P13(f13(a2),f16(a2))), % 180.83/180.84 inference(scs_inference,[],[126,219,290,286,239,228,189,323,264,311,135,278,284,213,71,53,58,100,96,92,34,29,98,27,3,17,21,26])). % 180.83/180.84 cnf(333,plain, % 180.83/180.84 (P13(f13(x3331),f16(f13(x3331)))), % 180.83/180.84 inference(scs_inference,[],[126,219,290,286,239,60,228,189,323,264,311,135,278,284,213,45,48,71,53,58,100,96,92,34,29,98,27,3,17,21,26,112])). % 180.83/180.84 cnf(337,plain, % 180.83/180.84 (E(a2,f14(f13(a2)))), % 180.83/180.84 inference(scs_inference,[],[126,219,290,286,239,60,228,189,323,264,311,135,278,284,213,45,48,71,53,58,100,96,92,34,29,98,27,3,17,21,26,112,2])). % 180.83/180.84 cnf(338,plain, % 180.83/180.84 (P5(a2,x3381)+~E(f15(a2),x3381)), % 180.83/180.84 inference(scs_inference,[],[126,219,290,286,239,60,232,228,189,323,264,311,135,278,284,213,45,48,71,53,58,100,96,92,34,29,98,27,3,17,21,26,112,2,22])). % 180.83/180.84 cnf(339,plain, % 180.83/180.84 (P5(f8(a2),f14(f13(a2)))), % 180.83/180.84 inference(scs_inference,[],[126,219,290,286,239,60,232,228,189,323,264,311,135,278,284,213,45,48,71,53,58,100,96,92,34,29,98,27,3,17,21,26,112,2,22,152])). % 180.83/180.84 cnf(346,plain, % 180.83/180.84 (~P5(f16(a3),a3)), % 180.83/180.84 inference(scs_inference,[],[209,65,92])). % 180.83/180.84 cnf(353,plain, % 180.83/180.84 (~E(f13(x3531),f15(a4))), % 180.83/180.84 inference(scs_inference,[],[126,333,209,121,261,138,113,65,92,98,27,17])). % 180.83/180.84 cnf(355,plain, % 180.83/180.84 (P13(a2,f16(f13(a2)))), % 180.83/180.84 inference(scs_inference,[],[219,126,333,209,121,261,138,113,65,92,98,27,17,26])). % 180.83/180.84 cnf(359,plain, % 180.83/180.84 (~P13(f15(a4),f16(a1))), % 180.83/180.84 inference(scs_inference,[],[219,126,333,209,121,261,138,113,48,65,92,98,27,17,26,80,111])). % 180.83/180.84 cnf(362,plain, % 180.83/180.84 (~P15(a1)+P15(f8(f15(a1)))), % 180.83/180.84 inference(scs_inference,[],[219,126,187,333,209,121,261,138,113,48,65,92,98,27,17,26,80,111,34])). % 180.83/180.84 cnf(382,plain, % 180.83/180.84 (~P13(f15(a4),f16(a2))), % 180.83/180.84 inference(scs_inference,[],[337,126,142,286,232,189,310,160,329,359,48,71,92,98,27,21,17,26,80,111])). % 180.83/180.84 cnf(385,plain, % 180.83/180.84 (P16(f16(x3851),x3852)+~E(f15(x3851),x3852)), % 180.83/180.84 inference(scs_inference,[],[337,126,142,286,232,189,310,160,329,359,64,48,71,92,98,27,21,17,26,80,111,18])). % 180.83/180.84 cnf(386,plain, % 180.83/180.84 (~P8(a1)+P8(f8(f15(a1)))), % 180.83/180.84 inference(scs_inference,[],[337,126,187,142,286,232,189,310,160,329,359,64,48,71,92,98,27,21,17,26,80,111,18,30])). % 180.83/180.84 cnf(388,plain, % 180.83/180.84 (~P7(a1)+P7(f8(f15(a1)))), % 180.83/180.84 inference(scs_inference,[],[337,126,187,142,286,232,62,189,310,160,329,359,64,48,71,92,98,27,21,17,26,80,111,18,30,22,31])). % 180.83/180.84 cnf(389,plain, % 180.83/180.84 (~P11(a1)+P11(f8(f15(a1)))), % 180.83/180.84 inference(scs_inference,[],[337,126,187,142,286,232,62,189,310,160,329,359,64,48,71,92,98,27,21,17,26,80,111,18,30,22,31,32])). % 180.83/180.84 cnf(390,plain, % 180.83/180.84 (~P6(a1)+P6(f8(f15(a1)))), % 180.83/180.84 inference(scs_inference,[],[337,126,187,142,286,232,62,189,310,160,329,359,64,48,71,92,98,27,21,17,26,80,111,18,30,22,31,32,19])). % 180.83/180.84 cnf(396,plain, % 180.83/180.84 (~P16(f15(a4),f13(x3961))), % 180.83/180.84 inference(scs_inference,[],[261,353,382,71,92,98])). % 180.83/180.84 cnf(480,plain, % 180.83/180.84 (E(f8(f15(a2)),a2)), % 180.83/180.84 inference(scs_inference,[],[189,118,98])). % 180.83/180.84 cnf(487,plain, % 180.83/180.84 (E(a2,f8(f15(a2)))), % 180.83/180.84 inference(scs_inference,[],[333,253,189,207,118,98,3,27,2])). % 180.83/180.84 cnf(489,plain, % 180.83/180.84 (P1(f8(f15(a2)))), % 180.83/180.84 inference(scs_inference,[],[333,253,189,36,207,249,118,98,3,27,2,34,16])). % 180.83/180.84 cnf(511,plain, % 180.83/180.84 (~P13(x5111,f8(f15(a2)))), % 180.83/180.84 inference(scs_inference,[],[489,85])). % 180.83/180.84 cnf(513,plain, % 180.83/180.84 (P5(f8(a2),f8(f15(a2)))), % 180.83/180.84 inference(scs_inference,[],[487,489,85,152])). % 180.83/180.84 cnf(552,plain, % 180.83/180.84 (P16(x5521,f15(x5522))+~E(f16(x5522),x5521)), % 180.83/180.84 inference(scs_inference,[],[286,160,64,27,17])). % 180.83/180.84 cnf(565,plain, % 180.83/180.84 (P5(x5651,f8(f15(a1)))+~E(f8(a1),x5651)), % 180.83/180.84 inference(scs_inference,[],[142,188,207,27,21])). % 180.83/180.84 cnf(566,plain, % 180.83/180.84 (~P10(a1)+P10(f8(f15(a1)))), % 180.83/180.84 inference(scs_inference,[],[187,142,188,207,27,21,33])). % 180.83/180.84 cnf(567,plain, % 180.83/180.84 (~P14(a1)+P14(f8(f15(a1)))), % 180.83/180.84 inference(scs_inference,[],[187,142,188,207,27,21,33,29])). % 180.83/180.84 cnf(578,plain, % 180.83/180.84 (P13(x5781,f16(a3))+~E(a3,x5781)), % 180.83/180.84 inference(scs_inference,[],[219,337,183,284,264,27,22,24,25,20,26])). % 180.83/180.84 cnf(605,plain, % 180.83/180.84 (P5(x6051,f14(f13(a2)))+~E(f8(a2),x6051)), % 180.83/180.84 inference(scs_inference,[],[129,339,160,27,21])). % 180.83/180.84 cnf(608,plain, % 180.83/180.84 (P13(x6081,f16(a4))+~E(a4,x6081)), % 180.83/180.84 inference(scs_inference,[],[322,142,129,339,160,27,21,20,25,26])). % 180.83/180.84 cnf(635,plain, % 180.83/180.84 (~P12(a1)+P12(f8(f15(a1)))), % 180.83/180.84 inference(scs_inference,[],[187,234,264,27,28])). % 180.83/180.84 cnf(653,plain, % 180.83/180.84 (P16(x6531,a11)+~E(f8(a11),f9(x6531,a11))), % 180.83/180.84 inference(scs_inference,[],[234,166,113,27,26,105])). % 180.83/180.84 cnf(673,plain, % 180.83/180.84 (P5(x6731,f8(f15(a2)))+~E(f8(a2),x6731)), % 180.83/180.84 inference(scs_inference,[],[331,213,160,513,27,22,21])). % 180.83/180.84 cnf(738,plain, % 180.83/180.84 (~E(a11,a2)), % 180.83/180.84 inference(scs_inference,[],[166,160,27])). % 180.83/180.84 cnf(858,plain, % 180.83/180.84 (P6(f6(a3))), % 180.83/180.84 inference(scs_inference,[],[191,72,76])). % 180.83/180.84 cnf(859,plain, % 180.83/180.84 (P13(f6(a3),f16(f6(a3)))), % 180.83/180.84 inference(scs_inference,[],[60,858,48,112])). % 180.83/180.84 cnf(863,plain, % 180.83/180.84 (~P13(f16(f6(a3)),f6(a3))), % 180.83/180.84 inference(scs_inference,[],[60,858,48,112,96])). % 180.83/180.84 cnf(865,plain, % 180.83/180.84 (P13(x8651,f16(f6(a3)))+~E(f6(a3),x8651)), % 180.83/180.84 inference(scs_inference,[],[60,858,48,112,96,26])). % 180.83/180.84 cnf(888,plain, % 180.83/180.84 (P6(f7(f12(a11)))), % 180.83/180.84 inference(scs_inference,[],[66,77,82])). % 180.83/180.84 cnf(904,plain, % 180.83/180.84 (~P1(f6(f7(a5)))), % 180.83/180.84 inference(scs_inference,[],[67,83,84])). % 180.83/180.84 cnf(927,plain, % 180.83/180.84 (P13(a2,f15(a2))), % 180.83/180.84 inference(scs_inference,[],[232,70,92])). % 180.83/180.84 cnf(1050,plain, % 180.83/180.84 (P13(f13(x10501),f15(x10501))), % 180.83/180.84 inference(scs_inference,[],[62,70,92])). % 180.83/180.84 cnf(1105,plain, % 180.83/180.84 (P5(f9(f15(a4),f16(a4)),f15(a4))), % 180.83/180.84 inference(scs_inference,[],[126,91,100])). % 180.83/180.84 cnf(1106,plain, % 180.83/180.84 (P16(f9(f15(a4),f16(a4)),a4)), % 180.83/180.84 inference(scs_inference,[],[1105,97])). % 180.83/180.84 cnf(1108,plain, % 180.83/180.84 (P6(f9(f15(a4),f16(a4)))), % 180.83/180.84 inference(scs_inference,[],[38,1105,97,95])). % 180.83/180.84 cnf(1123,plain, % 180.83/180.84 (E(a4,f9(f15(a4),f16(a4)))+~P16(a4,f9(f15(a4),f16(a4)))), % 180.83/180.84 inference(scs_inference,[],[1105,1106,98,21,2])). % 180.83/180.84 cnf(1151,plain, % 180.83/180.84 (P6(a1)), % 180.83/180.84 inference(scs_inference,[],[227,192,73])). % 180.83/180.84 cnf(1152,plain, % 180.83/180.84 (P6(f8(f15(a1)))), % 180.83/180.84 inference(scs_inference,[],[1151,390])). % 180.83/180.84 cnf(1153,plain, % 180.83/180.84 (P13(a1,f16(a1))), % 180.83/180.84 inference(scs_inference,[],[60,1151,48,112])). % 180.83/180.84 cnf(1217,plain, % 180.83/180.84 (P13(x12171,f15(a4))+~E(f9(f15(a4),f16(a4)),x12171)), % 180.83/180.84 inference(scs_inference,[],[1105,70,92,96,26])). % 180.83/180.84 cnf(1337,plain, % 180.83/180.84 (P16(f8(f15(a2)),f13(a2))), % 180.83/180.84 inference(scs_inference,[],[239,118,18])). % 180.83/180.84 cnf(1339,plain, % 180.83/180.84 (E(f8(f15(a2)),f13(a2))), % 180.83/180.84 inference(scs_inference,[],[239,261,118,18,98])). % 180.83/180.84 cnf(1342,plain, % 180.83/180.84 (~E(f8(f15(a2)),f15(a4))), % 180.83/180.84 inference(scs_inference,[],[239,396,261,118,18,98,17])). % 180.83/180.84 cnf(1347,plain, % 180.83/180.84 (P13(f14(a3),f16(f14(a3)))), % 180.83/180.84 inference(scs_inference,[],[37,239,396,60,63,261,118,48,18,98,17,95,112])). % 180.83/180.84 cnf(1351,plain, % 180.83/180.84 (E(f13(a2),f8(f15(a2)))), % 180.83/180.84 inference(scs_inference,[],[37,239,396,60,63,261,118,48,18,98,17,95,112,2])). % 180.83/180.84 cnf(1360,plain, % 180.83/180.84 (P6(f8(f15(a3)))), % 180.83/180.84 inference(scs_inference,[],[37,859,61,113,27,95])). % 180.83/180.84 cnf(1879,plain, % 180.83/180.84 (P5(f12(a3),f15(a3))), % 180.83/180.84 inference(scs_inference,[],[191,86,72])). % 180.83/180.84 cnf(1880,plain, % 180.83/180.84 (P16(f12(a3),a3)), % 180.83/180.84 inference(scs_inference,[],[1879,97])). % 180.83/180.84 cnf(1882,plain, % 180.83/180.84 (P6(f12(a3))), % 180.83/180.84 inference(scs_inference,[],[37,1879,97,95])). % 180.83/180.84 cnf(1884,plain, % 180.83/180.84 (~P13(f16(a3),f12(a3))), % 180.83/180.84 inference(scs_inference,[],[37,346,1879,97,95,104])). % 180.83/180.84 cnf(1886,plain, % 180.83/180.84 (P13(f12(a3),f16(f12(a3)))), % 180.83/180.84 inference(scs_inference,[],[60,37,346,1879,48,97,95,104,112])). % 180.83/180.84 cnf(1890,plain, % 180.83/180.84 (~P13(f16(f12(a3)),f12(a3))), % 180.83/180.84 inference(scs_inference,[],[60,37,346,1879,48,97,95,104,112,96])). % 180.83/180.84 cnf(1892,plain, % 180.83/180.84 (P13(x18921,f16(f12(a3)))+~E(f12(a3),x18921)), % 180.83/180.84 inference(scs_inference,[],[60,37,346,1879,48,97,95,104,112,96,26])). % 180.83/180.84 cnf(1908,plain, % 180.83/180.84 (P16(f12(a3),x19081)+~E(f15(a3),f15(x19081))), % 180.83/180.84 inference(scs_inference,[],[1886,207,1879,27,22,97])). % 180.83/180.84 cnf(1961,plain, % 180.83/180.84 (P5(a1,f15(x19611))), % 180.83/180.84 inference(scs_inference,[],[113,94,100])). % 180.83/180.84 cnf(1963,plain, % 180.83/180.84 (P16(f8(f15(a1)),x19631)), % 180.83/180.84 inference(scs_inference,[],[187,1961,21,97])). % 180.83/180.84 cnf(1972,plain, % 180.83/180.84 (P5(f16(a4),f15(a1))+~P16(f16(a4),f8(f15(a1)))), % 180.83/180.84 inference(scs_inference,[],[38,187,126,60,1961,132,21,97,17,98,102,151])). % 180.83/180.84 cnf(2309,plain, % 180.83/180.84 (P13(f12(a3),f15(a3))), % 180.83/180.84 inference(scs_inference,[],[1879,70,92])). % 180.83/180.84 cnf(2312,plain, % 180.83/180.84 (~P13(f15(a3),f12(a3))), % 180.83/180.84 inference(scs_inference,[],[1879,70,92,96])). % 180.83/180.84 cnf(2314,plain, % 180.83/180.84 (P13(x23141,f15(a3))+~E(f12(a3),x23141)), % 180.83/180.84 inference(scs_inference,[],[1879,70,92,96,26])). % 180.83/180.84 cnf(2414,plain, % 180.83/180.84 (E(f13(f13(a2)),f13(f14(f13(a2))))), % 180.83/180.84 inference(scs_inference,[],[269,4,2])). % 180.83/180.84 cnf(2446,plain, % 180.83/180.84 (E(f15(f10(x24461,f8(f15(a1)))),f15(f10(x24461,a1)))), % 180.83/180.84 inference(scs_inference,[],[169,8,7])). % 180.83/180.84 cnf(2462,plain, % 180.83/180.84 (E(f16(f6(f8(f15(a1)))),f16(f6(a1)))), % 180.83/180.84 inference(scs_inference,[],[169,9,10])). % 180.83/180.84 cnf(2494,plain, % 180.83/180.84 (E(f8(f9(f8(f15(a1)),x24941)),f8(f9(a1,x24941)))), % 180.83/180.84 inference(scs_inference,[],[169,15,13])). % 180.83/180.84 cnf(2587,plain, % 180.83/180.84 (~P16(f16(a3),f13(x25871))), % 180.83/180.84 inference(scs_inference,[],[183,207,101])). % 180.83/180.84 cnf(2949,plain, % 180.83/180.84 (~P16(a5,f13(x29491))), % 180.83/180.84 inference(scs_inference,[],[213,207,101])). % 180.83/180.84 cnf(2952,plain, % 180.83/180.84 (~P13(a5,f16(f13(x29521)))), % 180.83/180.84 inference(scs_inference,[],[48,213,207,101,111])). % 180.83/180.84 cnf(2964,plain, % 180.83/180.84 (~P13(f15(a3),f16(f13(x29641)))), % 180.83/180.84 inference(scs_inference,[],[48,333,2309,207,2952,71,26,101,92,111])). % 180.83/180.84 cnf(2976,plain, % 180.83/180.84 (~P13(a11,f16(f14(x29761)))), % 180.83/180.84 inference(scs_inference,[],[48,333,166,264,2964,71,26,101,92,111])). % 180.83/180.84 cnf(2981,plain, % 180.83/180.84 (~P13(a11,f16(f14(x29811)))), % 180.83/180.84 inference(rename_variables,[],[2976])). % 180.83/180.84 cnf(2988,plain, % 180.83/180.84 (~P13(f16(f14(a3)),f16(a1))), % 180.83/180.84 inference(scs_inference,[],[48,234,1347,113,2976,2981,71,26,101,92,111])). % 180.83/180.84 cnf(2993,plain, % 180.83/180.84 (~P16(a3,f13(x29931))), % 180.83/180.84 inference(scs_inference,[],[1153,129,207,2988,26,101])). % 180.83/180.84 cnf(2999,plain, % 180.83/180.84 (~P13(a3,f16(f13(x29991)))), % 180.83/180.84 inference(scs_inference,[],[48,1153,129,207,2988,71,26,101,92,111])). % 180.83/180.84 cnf(3009,plain, % 180.83/180.84 (~P16(a5,f14(x30091))), % 180.83/180.84 inference(scs_inference,[],[213,264,101])). % 180.83/180.84 cnf(3012,plain, % 180.83/180.84 (~E(f13(x30121),a3)), % 180.83/180.84 inference(scs_inference,[],[333,213,264,2999,101,26])). % 180.83/180.84 cnf(3095,plain, % 180.83/180.84 (~P13(f15(x30951),f16(f13(x30952)))), % 180.83/180.84 inference(scs_inference,[],[48,1050,207,101,111])). % 180.83/180.84 cnf(3109,plain, % 180.83/180.84 (~P16(a11,a1)), % 180.83/180.84 inference(scs_inference,[],[166,113,101])). % 180.83/180.84 cnf(3112,plain, % 180.83/180.84 (~P13(a11,f16(a1))), % 180.83/180.84 inference(scs_inference,[],[48,166,113,101,111])). % 180.83/180.84 cnf(3120,plain, % 180.83/180.84 (~E(f13(x31201),f15(x31202))), % 180.83/180.84 inference(scs_inference,[],[48,333,166,113,1337,2587,3095,71,101,111,17,92,26])). % 180.83/180.84 cnf(3124,plain, % 180.83/180.84 (~P16(a5,a1)), % 180.83/180.84 inference(scs_inference,[],[213,113,101])). % 180.83/180.84 cnf(3127,plain, % 180.83/180.84 (~P13(a5,f16(a1))), % 180.83/180.84 inference(scs_inference,[],[48,213,113,101,111])). % 180.83/180.84 cnf(3130,plain, % 180.83/180.84 (~P5(a11,f16(a1))), % 180.83/180.84 inference(scs_inference,[],[48,213,113,3112,71,101,111,92])). % 180.83/180.84 cnf(3133,plain, % 180.83/180.84 (~E(a1,a11)), % 180.83/180.84 inference(scs_inference,[],[48,1153,213,113,3112,71,101,111,92,26])). % 180.83/180.84 cnf(3142,plain, % 180.83/180.84 (~P5(a5,f16(a1))), % 180.83/180.84 inference(scs_inference,[],[48,2309,113,3127,71,101,111,92])). % 180.83/180.84 cnf(3145,plain, % 180.83/180.84 (~E(a1,a5)), % 180.83/180.84 inference(scs_inference,[],[48,1153,2309,113,3127,71,101,111,92,26])). % 180.83/180.84 cnf(3148,plain, % 180.83/180.84 (~P16(a3,a1)), % 180.83/180.84 inference(scs_inference,[],[129,113,101])). % 180.83/180.84 cnf(3151,plain, % 180.83/180.84 (~P13(a3,f16(a1))), % 180.83/180.84 inference(scs_inference,[],[48,129,113,101,111])). % 180.83/180.84 cnf(3163,plain, % 180.83/180.84 (~P13(f15(x31631),f16(a1))), % 180.83/180.84 inference(scs_inference,[],[48,1050,113,101,111])). % 180.83/180.84 cnf(3166,plain, % 180.83/180.84 (~P5(a3,f16(a1))), % 180.83/180.84 inference(scs_inference,[],[48,1050,113,3151,71,101,111,92])). % 180.83/180.84 cnf(3169,plain, % 180.83/180.84 (~E(a1,a3)), % 180.83/180.84 inference(scs_inference,[],[48,1153,1050,113,3151,71,101,111,92,26])). % 180.83/180.84 cnf(3172,plain, % 180.83/180.84 (~P5(f15(x31721),f16(a1))), % 180.83/180.84 inference(scs_inference,[],[3163,71,92])). % 180.83/180.84 cnf(3190,plain, % 180.83/180.84 (~E(a2,f15(x31901))), % 180.83/180.84 inference(scs_inference,[],[355,3095,26])). % 180.83/180.84 cnf(3618,plain, % 180.83/180.84 (P13(a1,f15(x36181))), % 180.83/180.84 inference(scs_inference,[],[1961,70,92])). % 180.83/180.84 cnf(3621,plain, % 180.83/180.84 (P13(f8(f15(a1)),f15(x36211))), % 180.83/180.84 inference(scs_inference,[],[187,1961,70,92,26])). % 180.83/180.84 cnf(3765,plain, % 180.83/180.84 (P13(f8(f16(x37651)),f16(x37651))), % 180.83/180.84 inference(scs_inference,[],[61,71,92])). % 180.83/180.84 cnf(3772,plain, % 180.83/180.84 (~P13(f16(x37721),f8(f16(x37721)))), % 180.83/180.84 inference(scs_inference,[],[3765,96])). % 180.83/180.84 cnf(3775,plain, % 180.83/180.84 (~P13(x37751,a1)), % 180.83/180.84 inference(rename_variables,[],[113])). % 180.83/180.84 cnf(3776,plain, % 180.83/180.84 (~P16(f16(x37761),a1)), % 180.83/180.84 inference(scs_inference,[],[113,3775,3765,96,27,101])). % 180.83/180.84 cnf(3791,plain, % 180.83/180.84 (~P13(x37911,f13(x37912))), % 180.83/180.84 inference(rename_variables,[],[207])). % 180.83/180.84 cnf(3795,plain, % 180.83/180.84 (~P13(f16(x37951),f16(f13(x37952)))), % 180.83/180.84 inference(scs_inference,[],[207,3791,3765,48,27,101,111])). % 180.83/180.84 cnf(3816,plain, % 180.83/180.84 (~E(f16(x38161),f14(x38162))), % 180.83/180.84 inference(scs_inference,[],[264,1337,2949,3765,17,27])). % 180.83/180.84 cnf(3817,plain, % 180.83/180.84 (~P13(x38171,f14(x38172))), % 180.83/180.84 inference(rename_variables,[],[264])). % 180.83/180.84 cnf(3821,plain, % 180.83/180.84 (~E(a2,f16(x38211))), % 180.83/180.84 inference(scs_inference,[],[355,264,3817,1337,2949,3765,3795,17,27,101,26])). % 180.83/180.84 cnf(3834,plain, % 180.83/180.84 (~P16(f15(x38341),a2)), % 180.83/180.84 inference(scs_inference,[],[189,3190,98])). % 180.83/180.84 cnf(3860,plain, % 180.83/180.84 (~P16(f16(x38601),a2)), % 180.83/180.84 inference(scs_inference,[],[189,3821,98])). % 180.83/180.84 cnf(3865,plain, % 180.83/180.84 (~P13(f16(x38651),f16(a2))), % 180.83/180.84 inference(scs_inference,[],[189,3821,48,98,80,111])). % 180.83/180.84 cnf(3943,plain, % 180.83/180.84 (P5(x39431,f15(x39432))+~E(a1,x39431)), % 180.83/180.84 inference(scs_inference,[],[1961,21])). % 180.83/180.84 cnf(3946,plain, % 180.83/180.84 (P13(x39461,f16(x39461))+~E(a1,x39461)), % 180.83/180.84 inference(scs_inference,[],[38,60,1961,48,21,95,112])). % 180.83/180.84 cnf(3959,plain, % 180.83/180.84 (P5(x39591,f15(x39592))+~E(f14(x39592),x39591)), % 180.83/180.84 inference(scs_inference,[],[63,21])). % 180.83/180.84 cnf(3975,plain, % 180.83/180.84 (P13(x39751,f15(x39752))+~E(a1,x39751)), % 180.83/180.84 inference(scs_inference,[],[3618,26])). % 180.83/180.84 cnf(3990,plain, % 180.83/180.84 (P6(f6(a11))), % 180.83/180.84 inference(scs_inference,[],[66,76])). % 180.83/180.84 cnf(3994,plain, % 180.83/180.84 (~P1(f12(a3))), % 180.83/180.84 inference(scs_inference,[],[65,66,76,77,82])). % 180.83/180.84 cnf(3996,plain, % 180.83/180.84 (~P1(f6(a3))), % 180.83/180.84 inference(scs_inference,[],[65,66,76,77,82,83])). % 180.83/180.84 cnf(3998,plain, % 180.83/180.84 (~P1(f7(a3))), % 180.83/180.84 inference(scs_inference,[],[65,66,76,77,82,83,84])). % 180.83/180.84 cnf(4000,plain, % 180.83/180.84 (P5(f13(x40001),f15(x40002))), % 180.83/180.84 inference(scs_inference,[],[65,66,261,76,77,82,83,84,94])). % 180.83/180.84 cnf(4002,plain, % 180.83/180.84 (P5(f12(a11),f15(a11))), % 180.83/180.84 inference(scs_inference,[],[65,66,261,76,77,82,83,84,94,86])). % 180.83/180.84 cnf(4004,plain, % 180.83/180.84 (P5(f6(a3),f15(a3))), % 180.83/180.84 inference(scs_inference,[],[65,66,261,76,77,82,83,84,94,86,87])). % 180.83/180.84 cnf(4006,plain, % 180.83/180.84 (P5(f7(a3),f15(a3))), % 180.83/180.84 inference(scs_inference,[],[65,66,261,76,77,82,83,84,94,86,87,88])). % 180.83/180.84 cnf(4008,plain, % 180.83/180.84 (E(f14(x40081),a1)), % 180.83/180.84 inference(scs_inference,[],[44,65,66,261,76,77,82,83,84,94,86,87,88,72])). % 180.83/180.84 cnf(4012,plain, % 180.83/180.84 (P6(f14(x40121))), % 180.83/180.84 inference(scs_inference,[],[332,44,65,66,261,76,77,82,83,84,94,86,87,88,72,91,73])). % 180.83/180.84 cnf(4014,plain, % 180.83/180.84 (P13(f9(a11,a1),a11)), % 180.83/180.84 inference(scs_inference,[],[3109,332,44,65,66,261,76,77,82,83,84,94,86,87,88,72,91,73,100])). % 180.83/180.84 cnf(4025,plain, % 180.83/180.84 (~P16(a3,a2)), % 180.83/180.84 inference(scs_inference,[],[146,3816,3860,3012,3109,2993,332,44,65,66,261,183,239,219,76,77,82,83,84,94,86,87,88,72,91,73,100,2,96,97,27,3,16,18])). % 180.83/180.84 cnf(4031,plain, % 180.83/180.84 (~E(f16(a1),f16(a3))), % 180.83/180.84 inference(scs_inference,[],[146,1884,3816,3860,3012,3109,2993,332,44,3151,65,66,37,35,261,183,239,60,48,219,76,77,82,83,84,94,86,87,88,72,91,73,100,2,96,97,27,3,16,18,103,92,102])). % 180.83/180.84 cnf(4037,plain, % 180.83/180.84 (~P16(a11,a2)), % 180.83/180.84 inference(scs_inference,[],[146,1884,3816,3860,3012,3109,2993,332,738,44,3151,65,66,37,35,261,64,189,183,239,60,48,219,76,77,82,83,84,94,86,87,88,72,91,73,100,2,96,97,27,3,16,18,103,92,102,89,98])). % 180.83/180.84 cnf(4050,plain, % 180.83/180.84 (P6(f7(a5))), % 180.83/180.84 inference(scs_inference,[],[67,77])). % 180.83/180.84 cnf(4052,plain, % 180.83/180.85 (P5(f6(a5),f15(a5))), % 180.83/180.85 inference(scs_inference,[],[67,77,87])). % 180.83/180.85 cnf(4054,plain, % 180.83/180.85 (P5(f12(a5),f15(a5))), % 180.83/180.85 inference(scs_inference,[],[67,77,87,86])). % 180.83/180.85 cnf(4056,plain, % 180.83/180.85 (~P1(f7(a5))), % 180.83/180.85 inference(scs_inference,[],[67,77,87,86,84])). % 180.83/180.85 cnf(4058,plain, % 180.83/180.85 (P5(f7(a5),f15(a5))), % 180.83/180.85 inference(scs_inference,[],[67,77,87,86,84,88])). % 180.83/180.85 cnf(4060,plain, % 180.83/180.85 (P5(f14(x40601),f15(x40602))), % 180.83/180.85 inference(scs_inference,[],[67,310,77,87,86,84,88,94])). % 180.83/180.85 cnf(4064,plain, % 180.83/180.85 (E(a2,a1)), % 180.83/180.85 inference(scs_inference,[],[67,36,310,77,87,86,84,88,94,76,72])). % 180.83/180.85 cnf(4066,plain, % 180.83/180.85 (~P1(f6(a5))), % 180.83/180.85 inference(scs_inference,[],[67,36,310,77,87,86,84,88,94,76,72,83])). % 180.83/180.85 cnf(4070,plain, % 180.83/180.85 (~P1(f12(a5))), % 180.83/180.85 inference(scs_inference,[],[4014,67,36,310,77,87,86,84,88,94,76,72,83,91,82])). % 180.83/180.85 cnf(4072,plain, % 180.83/180.85 (P13(f9(a3,a2),a3)), % 180.83/180.85 inference(scs_inference,[],[4025,4014,67,36,310,77,87,86,84,88,94,76,72,83,91,82,100])). % 180.83/180.85 cnf(4074,plain, % 180.83/180.85 (~P13(a3,f9(a3,a2))), % 180.83/180.85 inference(scs_inference,[],[4025,4014,67,36,310,77,87,86,84,88,94,76,72,83,91,82,100,96])). % 180.83/180.85 cnf(4076,plain, % 180.83/180.85 (~P5(a3,f15(a2))), % 180.83/180.85 inference(scs_inference,[],[4025,4014,67,36,310,77,87,86,84,88,94,76,72,83,91,82,100,96,97])). % 180.83/180.85 cnf(4078,plain, % 180.83/180.85 (~E(f16(a3),f16(a1))), % 180.83/180.85 inference(scs_inference,[],[4025,4031,4014,67,36,310,77,87,86,84,88,94,76,72,83,91,82,100,96,97,2])). % 180.83/180.85 cnf(4079,plain, % 180.83/180.85 (~E(a2,f12(a3))), % 180.83/180.85 inference(scs_inference,[],[4025,3994,4031,4014,67,36,310,77,87,86,84,88,94,76,72,83,91,82,100,96,97,2,16])). % 180.83/180.85 cnf(4080,plain, % 180.83/180.85 (~P5(a11,f15(a2))), % 180.83/180.85 inference(scs_inference,[],[4025,3994,4031,4014,67,36,310,77,87,86,84,88,94,76,72,83,91,82,100,96,97,2,16,103])). % 180.83/180.85 cnf(4082,plain, % 180.83/180.85 (P13(f13(x40821),f15(x40822))), % 180.83/180.85 inference(scs_inference,[],[4025,4000,3994,4031,4014,67,36,310,70,77,87,86,84,88,94,76,72,83,91,82,100,96,97,2,16,103,92])). % 180.83/180.85 cnf(4085,plain, % 180.83/180.85 (E(f13(a2),f13(a1))), % 180.83/180.85 inference(scs_inference,[],[4025,4000,3994,4031,4014,67,36,310,70,77,87,86,84,88,94,76,72,83,91,82,100,96,97,2,16,103,92,4])). % 180.83/180.85 cnf(4086,plain, % 180.83/180.85 (E(f14(a2),f14(a1))), % 180.83/180.85 inference(scs_inference,[],[4025,4000,3994,4031,4014,67,36,310,70,77,87,86,84,88,94,76,72,83,91,82,100,96,97,2,16,103,92,4,5])). % 180.83/180.85 cnf(4087,plain, % 180.83/180.85 (E(f15(a2),f15(a1))), % 180.83/180.85 inference(scs_inference,[],[4025,4000,3994,4031,4014,67,36,310,70,77,87,86,84,88,94,76,72,83,91,82,100,96,97,2,16,103,92,4,5,8])). % 180.83/180.85 cnf(4088,plain, % 180.83/180.85 (E(f16(a2),f16(a1))), % 180.83/180.85 inference(scs_inference,[],[4025,4000,3994,4031,4014,67,36,310,70,77,87,86,84,88,94,76,72,83,91,82,100,96,97,2,16,103,92,4,5,8,9])). % 180.83/180.85 cnf(4089,plain, % 180.83/180.85 (E(f6(a2),f6(a1))), % 180.83/180.85 inference(scs_inference,[],[4025,4000,3994,4031,4014,67,36,310,70,77,87,86,84,88,94,76,72,83,91,82,100,96,97,2,16,103,92,4,5,8,9,10])). % 180.83/180.85 cnf(4090,plain, % 180.83/180.85 (E(f7(a2),f7(a1))), % 180.83/180.85 inference(scs_inference,[],[4025,4000,3994,4031,4014,67,36,310,70,77,87,86,84,88,94,76,72,83,91,82,100,96,97,2,16,103,92,4,5,8,9,10,11])). % 180.83/180.85 cnf(4091,plain, % 180.83/180.85 (E(f12(a2),f12(a1))), % 180.83/180.85 inference(scs_inference,[],[4025,4000,3994,4031,4014,67,36,310,70,77,87,86,84,88,94,76,72,83,91,82,100,96,97,2,16,103,92,4,5,8,9,10,11,12])). % 180.83/180.85 cnf(4092,plain, % 180.83/180.85 (E(f8(a2),f8(a1))), % 180.83/180.85 inference(scs_inference,[],[4025,4000,3994,4031,4014,67,36,310,70,77,87,86,84,88,94,76,72,83,91,82,100,96,97,2,16,103,92,4,5,8,9,10,11,12,15])). % 180.83/180.85 cnf(4093,plain, % 180.83/180.85 (E(f10(a2,x40931),f10(a1,x40931))), % 180.83/180.85 inference(scs_inference,[],[4025,4000,3994,4031,4014,67,36,310,70,77,87,86,84,88,94,76,72,83,91,82,100,96,97,2,16,103,92,4,5,8,9,10,11,12,15,6])). % 180.83/180.85 cnf(4094,plain, % 180.83/180.85 (E(f10(x40941,a2),f10(x40941,a1))), % 180.83/180.85 inference(scs_inference,[],[4025,4000,3994,4031,4014,67,36,310,70,77,87,86,84,88,94,76,72,83,91,82,100,96,97,2,16,103,92,4,5,8,9,10,11,12,15,6,7])). % 180.83/180.85 cnf(4095,plain, % 180.83/180.85 (E(f9(a2,x40951),f9(a1,x40951))), % 180.83/180.85 inference(scs_inference,[],[4025,4000,3994,4031,4014,67,36,310,70,77,87,86,84,88,94,76,72,83,91,82,100,96,97,2,16,103,92,4,5,8,9,10,11,12,15,6,7,13])). % 180.83/180.85 cnf(4096,plain, % 180.83/180.85 (E(f9(x40961,a2),f9(x40961,a1))), % 180.83/180.85 inference(scs_inference,[],[4025,4000,3994,4031,4014,67,36,310,70,77,87,86,84,88,94,76,72,83,91,82,100,96,97,2,16,103,92,4,5,8,9,10,11,12,15,6,7,13,14])). % 180.83/180.85 cnf(4102,plain, % 180.83/180.85 (P16(f6(a1),f6(a2))), % 180.83/180.85 inference(scs_inference,[],[4025,4000,3994,4031,4014,927,67,36,310,70,60,77,87,86,84,88,94,76,72,83,91,82,100,96,97,2,16,103,92,4,5,8,9,10,11,12,15,6,7,13,14,3959,80,101,17])). % 180.83/180.85 cnf(4104,plain, % 180.83/180.85 (~E(f6(a1),x41041)+E(f6(a2),x41041)), % 180.83/180.85 inference(scs_inference,[],[4025,4000,3994,4031,4014,927,67,36,310,70,60,77,87,86,84,88,94,76,72,83,91,82,100,96,97,2,16,103,92,4,5,8,9,10,11,12,15,6,7,13,14,3959,80,101,17,3])). % 180.83/180.85 cnf(4121,plain, % 180.83/180.85 (P5(f6(a11),f15(a11))), % 180.83/180.85 inference(scs_inference,[],[4087,66,338,87])). % 180.83/180.85 cnf(4123,plain, % 180.83/180.85 (P6(f7(a11))), % 180.83/180.85 inference(scs_inference,[],[4087,66,338,87,77])). % 180.83/180.85 cnf(4125,plain, % 180.83/180.85 (E(f13(x41251),a1)), % 180.83/180.85 inference(scs_inference,[],[4087,66,43,338,87,77,72])). % 180.83/180.85 cnf(4127,plain, % 180.83/180.85 (P5(f7(a11),f15(a11))), % 180.83/180.85 inference(scs_inference,[],[4087,66,43,338,87,77,72,88])). % 180.83/180.85 cnf(4129,plain, % 180.83/180.85 (P5(a2,f15(x41291))), % 180.83/180.85 inference(scs_inference,[],[4087,66,189,43,338,87,77,72,88,94])). % 180.83/180.85 cnf(4131,plain, % 180.83/180.85 (~P1(f6(a11))), % 180.83/180.85 inference(scs_inference,[],[4087,66,189,43,338,87,77,72,88,94,83])). % 180.83/180.85 cnf(4133,plain, % 180.83/180.85 (~P1(f7(a11))), % 180.83/180.85 inference(scs_inference,[],[4087,66,189,43,338,87,77,72,88,94,83,84])). % 180.83/180.85 cnf(4137,plain, % 180.83/180.85 (P16(f6(a2),f6(a1))), % 180.83/180.85 inference(scs_inference,[],[4089,4087,4072,66,189,43,338,87,77,72,88,94,83,84,91,80])). % 180.83/180.85 cnf(4139,plain, % 180.83/180.85 (~P1(f12(a11))), % 180.83/180.85 inference(scs_inference,[],[4089,4087,4072,66,189,43,338,87,77,72,88,94,83,84,91,80,82])). % 180.83/180.85 cnf(4141,plain, % 180.83/180.85 (P13(f9(a11,a2),a11)), % 180.83/180.85 inference(scs_inference,[],[4089,4087,4072,4037,66,189,43,338,87,77,72,88,94,83,84,91,80,82,100])). % 180.83/180.85 cnf(4143,plain, % 180.83/180.85 (~P13(a11,f9(a11,a2))), % 180.83/180.85 inference(scs_inference,[],[4089,4087,4072,4037,66,189,43,338,87,77,72,88,94,83,84,91,80,82,100,96])). % 180.83/180.85 cnf(4147,plain, % 180.83/180.85 (~E(f12(a3),a2)), % 180.83/180.85 inference(scs_inference,[],[4089,4087,4072,4079,4037,3834,66,189,43,338,87,77,72,88,94,83,84,91,80,82,100,96,97,2])). % 180.83/180.85 cnf(4148,plain, % 180.83/180.85 (~E(f9(a3,a2),f16(a3))), % 180.83/180.85 inference(scs_inference,[],[4089,4087,4072,4079,4037,3834,209,66,189,43,338,87,77,72,88,94,83,84,91,80,82,100,96,97,2,26])). % 180.83/180.85 cnf(4149,plain, % 180.83/180.85 (P14(a1)), % 180.83/180.85 inference(scs_inference,[],[4064,4089,4087,4072,4079,4037,3834,276,209,66,189,43,338,87,77,72,88,94,83,84,91,80,82,100,96,97,2,26,29])). % 180.83/180.85 cnf(4150,plain, % 180.83/180.85 (~E(f16(a3),f16(a2))), % 180.83/180.85 inference(scs_inference,[],[4064,4078,4089,4087,4088,4072,4079,4037,3834,276,209,66,189,43,338,87,77,72,88,94,83,84,91,80,82,100,96,97,2,26,29,3])). % 180.83/180.85 cnf(4151,plain, % 180.83/180.85 (P12(a1)), % 180.83/180.85 inference(scs_inference,[],[4064,4078,4089,4087,4088,4072,4079,4037,3834,225,276,209,66,189,43,338,87,77,72,88,94,83,84,91,80,82,100,96,97,2,26,29,3,28])). % 180.83/180.85 cnf(4152,plain, % 180.83/180.85 (P11(a1)), % 180.83/180.85 inference(scs_inference,[],[4064,4078,4089,4087,4088,4072,4079,4037,3834,225,245,276,209,66,189,43,338,87,77,72,88,94,83,84,91,80,82,100,96,97,2,26,29,3,28,32])). % 180.83/180.85 cnf(4155,plain, % 180.83/180.85 (P7(a1)), % 180.83/180.85 inference(scs_inference,[],[4064,4078,4089,4087,4088,4072,4079,4037,3834,225,243,245,276,209,66,64,189,43,338,87,77,72,88,94,83,84,91,80,82,100,96,97,2,26,29,3,28,32,18,31])). % 180.83/180.85 cnf(4156,plain, % 180.83/180.85 (~E(f14(x41561),f6(a3))), % 180.83/180.85 inference(scs_inference,[],[4064,4078,4089,3996,4087,4088,4072,4079,4037,3834,225,243,245,276,209,66,44,64,189,43,338,87,77,72,88,94,83,84,91,80,82,100,96,97,2,26,29,3,28,32,18,31,16])). % 180.83/180.85 cnf(4158,plain, % 180.83/180.85 (~P5(f15(x41581),f15(a1))), % 180.83/180.85 inference(scs_inference,[],[4064,4082,4078,4089,3996,4087,4088,4074,4072,4079,4037,3834,225,243,245,276,209,66,44,35,64,189,183,43,338,87,77,72,88,94,83,84,91,80,82,100,96,97,2,26,29,3,28,32,18,31,16,27,103])). % 180.83/180.85 cnf(4160,plain, % 180.83/180.85 (~P16(f12(a3),a2)), % 180.83/180.85 inference(scs_inference,[],[4064,4082,4078,4089,3996,4087,4088,4074,4072,4079,4037,3834,225,243,245,276,209,66,44,35,64,189,183,43,338,87,77,72,88,94,83,84,91,80,82,100,96,97,2,26,29,3,28,32,18,31,16,27,103,98])). % 180.83/180.85 cnf(4168,plain, % 180.83/180.85 (~E(f15(a3),f16(a2))), % 180.83/180.85 inference(scs_inference,[],[4064,2312,4060,4082,4078,4089,3996,4087,4088,4074,4072,4079,4080,4037,3834,3172,225,243,245,276,3994,46,209,66,44,2309,35,64,189,183,43,338,87,77,72,88,94,83,84,91,80,82,100,96,97,2,26,29,3,28,32,18,31,16,27,103,98,21,22,92,99])). % 180.83/180.85 cnf(4171,plain, % 180.83/180.85 (P13(f13(x41711),f16(x41712))), % 180.83/180.85 inference(scs_inference,[],[4064,2312,4060,4082,4078,4089,3996,4087,4088,4074,4072,4079,4080,4037,3834,3172,225,243,245,276,3994,46,209,66,44,2309,35,64,261,189,183,45,43,48,338,87,77,72,88,94,83,84,91,80,82,100,96,97,2,26,29,3,28,32,18,31,16,27,103,98,21,22,92,99,112])). % 180.83/180.85 cnf(4172,plain, % 180.83/180.85 (P16(f13(x41721),x41722)), % 180.83/180.85 inference(rename_variables,[],[261])). % 180.83/180.85 cnf(4174,plain, % 180.83/180.85 (~E(f15(a3),f15(a2))), % 180.83/180.85 inference(scs_inference,[],[4064,2312,4060,4082,4078,4089,3996,4087,4088,4074,4072,4079,4080,4037,3834,3172,225,243,245,276,3994,46,209,66,44,2309,35,64,261,189,183,45,43,48,338,87,77,72,88,94,83,84,91,80,82,100,96,97,2,26,29,3,28,32,18,31,16,27,103,98,21,22,92,99,112,1908])). % 180.83/180.85 cnf(4177,plain, % 180.83/180.85 (P15(a1)), % 180.83/180.85 inference(scs_inference,[],[4064,2312,4060,4082,4078,4089,3996,4087,4088,4074,4072,4079,4080,4037,3834,3172,225,243,245,276,3994,249,46,209,66,44,2309,35,64,261,189,183,45,43,48,338,87,77,72,88,94,83,84,91,80,82,100,96,97,2,26,29,3,28,32,18,31,16,27,103,98,21,22,92,99,112,1908,3959,34])). % 180.83/180.85 cnf(4178,plain, % 180.83/180.85 (P8(a1)), % 180.83/180.85 inference(scs_inference,[],[4064,2312,4060,4082,4078,4089,3996,4087,4088,4074,4072,4079,4080,4037,3834,3172,225,243,245,276,3994,241,249,46,209,66,44,2309,35,64,261,189,183,45,43,48,338,87,77,72,88,94,83,84,91,80,82,100,96,97,2,26,29,3,28,32,18,31,16,27,103,98,21,22,92,99,112,1908,3959,34,30])). % 180.83/180.85 cnf(4179,plain, % 180.83/180.85 (~E(f13(x41791),f12(a3))), % 180.83/180.85 inference(scs_inference,[],[4064,2312,4060,4082,4078,4089,3996,4087,4088,4074,4072,4079,4080,4037,3834,3172,225,243,245,276,3994,241,249,46,209,66,44,2309,35,64,261,4172,189,183,45,43,48,338,87,77,72,88,94,83,84,91,80,82,100,96,97,2,26,29,3,28,32,18,31,16,27,103,98,21,22,92,99,112,1908,3959,34,30,17])). % 180.83/180.85 cnf(4181,plain, % 180.83/180.85 (P10(a1)), % 180.83/180.85 inference(scs_inference,[],[4064,2312,4060,4082,4078,4089,3996,4087,4088,4074,4072,4079,4080,4037,3834,3172,225,243,245,276,3994,241,247,249,46,209,66,44,2309,35,64,261,4172,189,183,45,43,48,338,87,77,72,88,94,83,84,91,80,82,100,96,97,2,26,29,3,28,32,18,31,16,27,103,98,21,22,92,99,112,1908,3959,34,30,17,33])). % 180.83/180.85 cnf(4186,plain, % 180.83/180.85 (P15(f8(f15(a1)))), % 180.83/180.85 inference(scs_inference,[],[4177,362])). % 180.83/180.85 cnf(4187,plain, % 180.83/180.85 (P8(f8(f15(a1)))), % 180.83/180.85 inference(scs_inference,[],[4178,386])). % 180.83/180.85 cnf(4188,plain, % 180.83/180.85 (P7(f8(f15(a1)))), % 180.83/180.85 inference(scs_inference,[],[4155,388])). % 180.83/180.85 cnf(4189,plain, % 180.83/180.85 (P11(f8(f15(a1)))), % 180.83/180.85 inference(scs_inference,[],[4152,389])). % 180.83/180.85 cnf(4190,plain, % 180.83/180.85 (P10(f8(f15(a1)))), % 180.83/180.85 inference(scs_inference,[],[4181,566])). % 180.83/180.85 cnf(4191,plain, % 180.83/180.85 (P14(f8(f15(a1)))), % 180.83/180.85 inference(scs_inference,[],[4149,567])). % 180.83/180.85 cnf(4192,plain, % 180.83/180.85 (P12(f8(f15(a1)))), % 180.83/180.85 inference(scs_inference,[],[4151,635])). % 180.83/180.85 cnf(4193,plain, % 180.83/180.85 (P5(x41931,f15(x41931))), % 180.83/180.85 inference(scs_inference,[],[60,94])). % 180.83/180.85 cnf(4195,plain, % 180.83/180.85 (P5(f13(x41951),f16(x41952))), % 180.83/180.85 inference(scs_inference,[],[4171,60,94,91])). % 180.83/180.85 cnf(4197,plain, % 180.83/180.85 (P16(f7(a2),f7(a1))), % 180.83/180.85 inference(scs_inference,[],[4171,4090,60,94,91,80])). % 180.83/180.85 cnf(4200,plain, % 180.83/180.85 (P13(f9(a5,a1),a5)), % 180.83/180.85 inference(scs_inference,[],[4171,4090,4158,3124,60,94,91,80,3959,100])). % 180.83/180.85 cnf(4202,plain, % 180.83/180.85 (~P13(a5,f9(a5,a1))), % 180.83/180.85 inference(scs_inference,[],[4171,4090,4158,3124,60,94,91,80,3959,100,96])). % 180.83/180.85 cnf(4207,plain, % 180.83/180.85 (P16(f7(a1),f7(a2))), % 180.83/180.85 inference(scs_inference,[],[4171,4090,4150,4158,4160,3124,60,94,91,80,3959,100,96,97,2,17])). % 180.83/180.85 cnf(4209,plain, % 180.83/180.85 (~P13(f16(a3),f6(a3))), % 180.83/180.85 inference(scs_inference,[],[4171,4090,4150,4158,4004,4160,3124,346,60,94,91,80,3959,100,96,97,2,17,104])). % 180.83/180.85 cnf(4211,plain, % 180.83/180.85 (E(f10(a2,a2),f10(a1,a1))), % 180.83/180.85 inference(scs_inference,[],[4171,4090,4150,4093,4094,4158,4004,4160,3124,346,60,94,91,80,3959,100,96,97,2,17,104,3])). % 180.83/180.85 cnf(4214,plain, % 180.83/180.85 (E(f6(a1),f6(a2))), % 180.83/180.85 inference(scs_inference,[],[4171,4090,4150,4093,4094,4158,4004,4102,4137,4160,3124,346,60,94,91,80,3959,100,96,97,2,17,104,3,98])). % 180.83/180.85 cnf(4216,plain, % 180.83/180.85 (~E(f14(x42161),f7(a3))), % 180.83/180.85 inference(scs_inference,[],[4171,4090,4150,4093,4094,4158,3998,4004,4102,4137,4160,3124,346,44,60,94,91,80,3959,100,96,97,2,17,104,3,98,16])). % 180.83/180.85 cnf(4217,plain, % 180.83/180.85 (~P16(f12(a3),f13(a2))), % 180.83/180.85 inference(scs_inference,[],[4171,4090,4150,4093,4094,4158,3998,4004,4102,4137,4160,3124,346,44,60,219,94,91,80,3959,100,96,97,2,17,104,3,98,16,18])). % 180.83/180.85 cnf(4218,plain, % 180.83/180.85 (P5(f8(a2),f13(a1))), % 180.83/180.85 inference(scs_inference,[],[4171,4085,4090,4150,4093,4094,4158,3998,4004,4102,4137,4160,3124,346,268,44,60,219,94,91,80,3959,100,96,97,2,17,104,3,98,16,18,22])). % 180.83/180.85 cnf(4219,plain, % 180.83/180.85 (P13(f12(a11),f15(a11))), % 180.83/180.85 inference(scs_inference,[],[4171,4002,4085,4090,4150,4093,4094,4158,3998,4004,4102,4137,4160,3124,346,268,44,70,60,219,94,91,80,3959,100,96,97,2,17,104,3,98,16,18,22,92])). % 180.83/180.85 cnf(4222,plain, % 180.83/180.85 (P5(f8(a1),f13(a2))), % 180.83/180.85 inference(scs_inference,[],[4171,4002,4085,4090,4092,4150,4093,4094,4158,3998,4004,4102,4137,4160,3124,346,268,44,70,60,219,94,91,80,3959,100,96,97,2,17,104,3,98,16,18,22,92,21])). % 180.83/180.85 cnf(4223,plain, % 180.83/180.85 (~E(a1,f12(a3))), % 180.83/180.85 inference(scs_inference,[],[4171,4002,4085,4090,4092,4150,4093,4094,4158,3998,4004,4102,4137,4160,3124,346,268,44,70,60,219,94,91,80,3959,100,96,97,2,17,104,3,98,16,18,22,92,21,3943])). % 180.83/180.85 cnf(4227,plain, % 180.83/180.85 (P5(f9(a5,a1),a5)), % 180.83/180.85 inference(scs_inference,[],[4200,91])). % 180.83/180.85 cnf(4229,plain, % 180.83/180.85 (P16(f10(a2,a2),f10(a1,a1))), % 180.83/180.85 inference(scs_inference,[],[4211,4200,91,80])). % 180.83/180.85 cnf(4231,plain, % 180.83/180.85 (P13(f9(a3,a1),a3)), % 180.83/180.85 inference(scs_inference,[],[4211,4200,3148,91,80,100])). % 180.83/180.85 cnf(4233,plain, % 180.83/180.85 (~P13(f15(a11),f12(a11))), % 180.83/180.85 inference(scs_inference,[],[4211,4219,4200,3148,91,80,100,96])). % 180.83/180.85 cnf(4235,plain, % 180.83/180.85 (~P5(f16(x42351),f15(a1))), % 180.83/180.85 inference(scs_inference,[],[4211,4219,4200,3776,3148,91,80,100,96,97])). % 180.83/180.85 cnf(4237,plain, % 180.83/180.85 (~E(f15(a2),f15(a3))), % 180.83/180.85 inference(scs_inference,[],[4211,4174,4219,4200,3776,3148,91,80,100,96,97,2])). % 180.83/180.85 cnf(4238,plain, % 180.83/180.85 (~E(f14(x42381),f12(a3))), % 180.83/180.85 inference(scs_inference,[],[4211,4174,4217,4219,4200,3776,3148,310,91,80,100,96,97,2,17])). % 180.83/180.85 cnf(4239,plain, % 180.83/180.85 (P16(f14(x42391),x42392)), % 180.83/180.85 inference(rename_variables,[],[310])). % 180.83/180.85 cnf(4240,plain, % 180.83/180.85 (~P5(a5,f15(a1))), % 180.83/180.85 inference(scs_inference,[],[4211,4174,4217,4219,4200,3776,3148,35,310,91,80,100,96,97,2,17,103])). % 180.83/180.85 cnf(4245,plain, % 180.83/180.85 (~P13(a5,f9(a5,a2))), % 180.83/180.85 inference(scs_inference,[],[4193,4211,4174,4217,4219,4202,4200,4096,4141,3776,3148,35,310,91,80,100,96,97,2,17,103,104,27])). % 180.83/180.85 cnf(4246,plain, % 180.83/180.85 (E(f9(x42461,a2),f9(x42461,a1))), % 180.83/180.85 inference(rename_variables,[],[4096])). % 180.83/180.85 cnf(4247,plain, % 180.83/180.85 (~P16(f6(a3),f14(x42471))), % 180.83/180.85 inference(scs_inference,[],[4193,4211,4174,4156,4217,4219,4202,4200,4096,4141,3776,3148,35,310,4239,91,80,100,96,97,2,17,103,104,27,98])). % 180.83/180.85 cnf(4251,plain, % 180.83/180.85 (~E(f9(a3,a1),f16(a3))), % 180.83/180.85 inference(scs_inference,[],[4193,4211,4174,4156,4148,4217,4219,4202,4200,4096,4246,4141,3776,3148,35,310,4239,91,80,100,96,97,2,17,103,104,27,98,3])). % 180.83/180.85 cnf(4253,plain, % 180.83/180.85 (~E(a1,f7(a5))), % 180.83/180.85 inference(scs_inference,[],[4193,4211,4174,4156,4148,4056,4217,4219,4202,4200,4096,4246,4141,3776,3148,35,310,4239,91,80,100,96,97,2,17,103,104,27,98,3,16])). % 180.83/180.85 cnf(4256,plain, % 180.83/180.85 (~P5(a11,f16(a2))), % 180.83/180.85 inference(scs_inference,[],[4193,4211,4174,4156,4148,4056,4209,4217,4219,4202,4200,4096,4246,4141,3130,3776,3996,3148,4088,35,310,4239,91,80,100,96,97,2,17,103,104,27,98,3,16,92,22])). % 180.83/180.85 cnf(4264,plain, % 180.83/180.85 (~P16(f16(a4),f8(f15(a1)))), % 180.83/180.85 inference(scs_inference,[],[4235,1972])). % 180.83/180.85 cnf(4267,plain, % 180.83/180.85 (P16(f12(a2),f12(a1))), % 180.83/180.85 inference(scs_inference,[],[4091,4231,91,80])). % 180.83/180.85 cnf(4270,plain, % 180.83/180.85 (~P13(a3,f9(a3,a1))), % 180.83/180.85 inference(scs_inference,[],[4091,4231,4240,91,80,3959,96])). % 180.83/180.85 cnf(4274,plain, % 180.83/180.85 (~E(f12(a3),a1)), % 180.83/180.85 inference(scs_inference,[],[4091,4223,4231,4240,3109,91,80,3959,96,97,2])). % 180.83/180.85 cnf(4275,plain, % 180.83/180.85 (P16(f12(a1),f12(a2))), % 180.83/180.85 inference(scs_inference,[],[4091,4223,4231,4240,3109,60,91,80,3959,96,97,2,17])). % 180.83/180.85 cnf(4277,plain, % 180.83/180.85 (~P13(f16(a3),f7(a3))), % 180.83/180.85 inference(scs_inference,[],[4091,4006,4223,4231,4240,3109,346,60,91,80,3959,96,97,2,17,104])). % 180.83/180.85 cnf(4279,plain, % 180.83/180.85 (E(f7(a1),f7(a2))), % 180.83/180.85 inference(scs_inference,[],[4091,4006,4223,4197,4207,4231,4240,3109,346,60,91,80,3959,96,97,2,17,104,98])). % 180.83/180.85 cnf(4282,plain, % 180.83/180.85 (E(f9(a2,a2),f9(a1,a1))), % 180.83/180.85 inference(scs_inference,[],[4091,4006,4223,4095,4197,4207,4231,4240,4096,3109,3112,346,4088,60,91,80,3959,96,97,2,17,104,98,27,3])). % 180.83/180.85 cnf(4285,plain, % 180.83/180.85 (~E(a2,f6(a5))), % 180.83/180.85 inference(scs_inference,[],[4091,4006,4223,4095,4066,4197,4207,4231,4240,4096,3109,3112,346,4088,36,60,91,80,3959,96,97,2,17,104,98,27,3,16])). % 180.83/180.85 cnf(4286,plain, % 180.83/180.85 (P13(f12(a5),f15(a5))), % 180.83/180.85 inference(scs_inference,[],[4054,4091,4006,4223,4095,4066,4197,4207,4231,4240,4096,3109,3112,346,4088,36,70,60,91,80,3959,96,97,2,17,104,98,27,3,16,92])). % 180.83/180.85 cnf(4290,plain, % 180.83/180.85 (E(f13(x42901),a1)), % 180.83/180.85 inference(rename_variables,[],[4125])). % 180.83/180.85 cnf(4291,plain, % 180.83/180.85 (P5(a1,f16(x42911))), % 180.83/180.85 inference(scs_inference,[],[4195,4054,4091,4006,4223,4095,4066,4197,4207,4218,4231,4240,4125,4290,4096,3109,3112,346,4088,36,70,60,91,80,3959,96,97,2,17,104,98,27,3,16,92,22,21])). % 180.83/180.85 cnf(4295,plain, % 180.83/180.85 (~P13(x42951,f10(a2,a2))+P13(x42951,f10(a1,a1))), % 180.83/180.85 inference(scs_inference,[],[4195,4229,4054,4091,4006,4223,4095,4066,4197,4207,4218,4231,4240,4125,4290,4096,4141,39,3109,3112,346,4088,36,70,60,91,80,3959,96,97,2,17,104,98,27,3,16,92,22,21,93,101])). % 180.83/180.85 cnf(4299,plain, % 180.83/180.85 (P16(f9(a2,a2),f9(a1,a1))), % 180.83/180.85 inference(scs_inference,[],[4282,142,91,80])). % 180.83/180.85 cnf(4301,plain, % 180.83/180.85 (~P13(f15(a5),f12(a5))), % 180.83/180.85 inference(scs_inference,[],[4282,4286,142,91,80,96])). % 180.83/180.85 cnf(4305,plain, % 180.83/180.85 (~E(f16(a2),f15(a3))), % 180.83/180.85 inference(scs_inference,[],[4168,4282,4286,3148,142,91,80,96,97,2])). % 180.83/180.85 cnf(4307,plain, % 180.83/180.85 (P5(x43071,f15(x43071))), % 180.83/180.85 inference(rename_variables,[],[4193])). % 180.83/180.85 cnf(4309,plain, % 180.83/180.85 (~E(f13(x43091),f6(a3))), % 180.83/180.85 inference(scs_inference,[],[4168,4247,4282,4286,4193,3148,261,142,286,91,80,96,97,2,104,17])). % 180.83/180.85 cnf(4310,plain, % 180.83/180.85 (P16(f13(x43101),x43102)), % 180.83/180.85 inference(rename_variables,[],[261])). % 180.83/180.85 cnf(4311,plain, % 180.83/180.85 (~P16(f12(a3),f13(x43111))), % 180.83/180.85 inference(scs_inference,[],[4168,4179,4247,4282,4286,4193,3148,261,4310,142,286,91,80,96,97,2,104,17,98])). % 180.83/180.85 cnf(4318,plain, % 180.83/180.85 (~E(f14(x43181),f12(a5))), % 180.83/180.85 inference(scs_inference,[],[4168,4179,4247,4070,4139,4233,4237,4282,4286,4193,4087,3148,44,261,4310,142,286,91,80,96,97,2,104,17,98,92,3,16])). % 180.83/180.85 cnf(4319,plain, % 180.83/180.85 (~E(a2,a5)), % 180.83/180.85 inference(scs_inference,[],[4168,4179,4247,4070,4129,4139,4233,4237,4282,4286,4193,4240,4087,3148,44,261,4310,142,286,91,80,96,97,2,104,17,98,92,3,16,21])). % 180.83/180.85 cnf(4321,plain, % 180.83/180.85 (~E(f15(a11),f16(a2))), % 180.83/180.85 inference(scs_inference,[],[4168,4179,4247,4070,4129,4139,4233,4237,4282,4286,4256,4193,4307,4240,4087,3148,44,261,4310,142,286,91,80,96,97,2,104,17,98,92,3,16,21,22])). % 180.83/180.85 cnf(4328,plain, % 180.83/180.85 (P16(f8(a2),f8(a1))), % 180.83/180.85 inference(scs_inference,[],[4092,80])). % 180.83/180.85 cnf(4330,plain, % 180.83/180.85 (P5(a3,f16(a3))), % 180.83/180.85 inference(scs_inference,[],[4092,183,80,91])). % 180.83/180.85 cnf(4332,plain, % 180.83/180.85 (~E(f7(a3),f14(x43321))), % 180.83/180.85 inference(scs_inference,[],[4216,4092,183,80,91,2])). % 180.83/180.85 cnf(4333,plain, % 180.83/180.85 (P16(f8(a1),f8(a2))), % 180.83/180.85 inference(scs_inference,[],[4216,4092,183,60,80,91,2,17])). % 180.83/180.85 cnf(4335,plain, % 180.83/180.85 (E(f12(a1),f12(a2))), % 180.83/180.85 inference(scs_inference,[],[4216,4267,4275,4092,183,60,80,91,2,17,98])). % 180.83/180.85 cnf(4341,plain, % 180.83/180.85 (~E(a1,f6(a3))), % 180.83/180.85 inference(scs_inference,[],[4052,4216,4309,4267,4275,4092,4125,3127,4088,70,183,60,80,91,2,17,98,92,27,3])). % 180.83/180.85 cnf(4343,plain, % 180.83/180.85 (~E(a2,f6(a11))), % 180.83/180.85 inference(scs_inference,[],[4052,4216,4309,4131,4267,4275,4092,4125,3127,4088,36,70,183,60,80,91,2,17,98,92,27,3,16])). % 180.83/180.85 cnf(4345,plain, % 180.83/180.85 (~P13(f15(a5),f6(a5))), % 180.83/180.85 inference(scs_inference,[],[4052,4216,4309,4131,4222,4267,4275,4092,4085,4125,3127,4088,36,70,183,60,80,91,2,17,98,92,27,3,16,22,96])). % 180.83/180.85 cnf(4348,plain, % 180.83/180.85 (~P5(a5,f15(a2))), % 180.83/180.85 inference(scs_inference,[],[4052,4216,4309,4131,4222,4267,4275,4301,4092,4085,4125,4200,3127,4088,36,70,183,60,80,91,2,17,98,92,27,3,16,22,96,26,103])). % 180.83/180.85 cnf(4350,plain, % 180.83/180.85 (~E(a1,x43501)+P15(x43501)), % 180.83/180.85 inference(scs_inference,[],[4177,4052,4216,4309,4131,4222,4267,4275,4301,4092,4085,4125,4200,3127,4088,36,70,183,60,80,91,2,17,98,92,27,3,16,22,96,26,103,34])). % 180.83/180.85 cnf(4353,plain, % 180.83/180.85 (P16(f10(a2,x43531),f10(a1,x43531))), % 180.83/180.85 inference(scs_inference,[],[4093,80])). % 180.83/180.85 cnf(4356,plain, % 180.83/180.85 (~P16(a5,a2)), % 180.83/180.85 inference(scs_inference,[],[4319,4251,4093,189,80,2,98])). % 180.83/180.85 cnf(4360,plain, % 180.83/180.85 (P16(f14(x43601),x43602)), % 180.83/180.85 inference(rename_variables,[],[310])). % 180.83/180.85 cnf(4363,plain, % 180.83/180.85 (~E(f16(a1),f15(a3))), % 180.83/180.85 inference(scs_inference,[],[4319,4251,4305,4345,3009,4066,4093,4088,310,189,80,2,98,17,92,3])). % 180.83/180.85 cnf(4364,plain, % 180.83/180.85 (~E(f14(x43641),f7(a11))), % 180.83/180.85 inference(scs_inference,[],[4319,4251,4133,4305,4345,3009,4066,4093,4088,44,310,189,80,2,98,17,92,3,16])). % 180.83/180.85 cnf(4365,plain, % 180.83/180.85 (~E(f15(a5),f15(a2))), % 180.83/180.85 inference(scs_inference,[],[4319,4251,4133,4305,4345,4348,3009,4066,4093,4193,4088,44,310,189,80,2,98,17,92,3,16,22])). % 180.83/180.85 cnf(4367,plain, % 180.83/180.85 (P13(f9(a5,a2),a5)), % 180.83/180.85 inference(scs_inference,[],[4319,4251,4133,4305,4345,4348,3009,4066,4093,4193,4088,44,310,189,80,2,98,17,92,3,16,22,100])). % 180.83/180.85 cnf(4370,plain, % 180.83/180.85 (P13(f14(x43701),f16(x43702))), % 180.83/180.85 inference(scs_inference,[],[4319,4251,4133,4305,4345,4348,4123,4012,3009,4066,4093,4193,4088,44,310,4360,189,48,80,2,98,17,92,3,16,22,100,19,112])). % 180.83/180.85 cnf(4380,plain, % 180.83/180.85 (P16(f10(x43801,a2),f10(x43801,a1))), % 180.83/180.85 inference(scs_inference,[],[4370,4094,91,80])). % 180.83/180.85 cnf(4382,plain, % 180.83/180.85 (~E(f12(a3),f14(x43821))), % 180.83/180.85 inference(scs_inference,[],[4370,4238,4094,91,80,2])). % 180.83/180.85 cnf(4383,plain, % 180.83/180.85 (E(f8(a1),f8(a2))), % 180.83/180.85 inference(scs_inference,[],[4370,4238,4328,4333,4094,91,80,2,98])). % 180.83/180.85 cnf(4385,plain, % 180.83/180.85 (P16(f10(a1,a1),f10(a1,a2))), % 180.83/180.85 inference(scs_inference,[],[4370,4353,4238,4328,4333,4211,4094,91,80,2,98,17])). % 180.83/180.85 cnf(4390,plain, % 180.83/180.85 (~E(a1,f7(a3))), % 180.83/180.85 inference(scs_inference,[],[4370,4058,4353,4238,4328,4333,3998,4211,4094,35,70,91,80,2,98,17,92,16])). % 180.83/180.85 cnf(4392,plain, % 180.83/180.85 (~P13(f15(a5),f7(a5))), % 180.83/180.85 inference(scs_inference,[],[4370,4058,4353,4238,4328,4333,3998,4222,4211,4094,35,70,219,91,80,2,98,17,92,16,22,96])). % 180.83/180.85 cnf(4394,plain, % 180.83/180.85 (~P13(x43941,f12(a1))+P13(x43941,f12(a2))), % 180.83/180.85 inference(scs_inference,[],[4370,4058,4353,4238,4328,4333,4335,3998,4222,4211,4094,35,70,219,91,80,2,98,17,92,16,22,96,27])). % 180.83/180.85 cnf(4398,plain, % 180.83/180.85 (P16(f9(a2,x43981),f9(a1,x43981))), % 180.83/180.85 inference(scs_inference,[],[4095,80])). % 180.83/180.85 cnf(4407,plain, % 180.83/180.85 (~P5(f15(a5),f7(a5))), % 180.83/180.85 inference(scs_inference,[],[4318,4392,4367,4056,4095,310,80,91,2,98,92])). % 180.83/180.85 cnf(4409,plain, % 180.83/180.85 (~E(f13(x44091),f12(a5))), % 180.83/180.85 inference(scs_inference,[],[4318,4392,4367,4056,4095,261,310,80,91,2,98,92,17])). % 180.83/180.85 cnf(4412,plain, % 180.83/180.85 (~E(f14(x44121),f7(a5))), % 180.83/180.85 inference(scs_inference,[],[4318,4392,4367,4056,4095,3151,4088,44,261,310,80,91,2,98,92,17,27,16])). % 180.83/180.85 cnf(4413,plain, % 180.83/180.85 (~E(f16(a3),f15(a2))), % 180.83/180.85 inference(scs_inference,[],[4330,4318,4392,4367,4076,4056,4095,3151,4088,44,261,310,80,91,2,98,92,17,27,16,22])). % 180.83/180.85 cnf(4414,plain, % 180.83/180.85 (~E(f9(a1,a1),x44141)+E(f9(a2,a2),x44141)), % 180.83/180.85 inference(scs_inference,[],[4330,4318,4392,4367,4076,4056,4282,4095,3151,4088,44,261,310,80,91,2,98,92,17,27,16,22,3])). % 180.83/180.85 cnf(4419,plain, % 180.83/180.85 (P16(f9(x44191,a2),f9(x44191,a1))), % 180.83/180.85 inference(scs_inference,[],[4096,80])). % 180.83/180.85 cnf(4421,plain, % 180.83/180.85 (~E(f7(a11),f14(x44211))), % 180.83/180.85 inference(scs_inference,[],[4364,4096,80,2])). % 180.83/180.85 cnf(4422,plain, % 180.83/180.85 (E(f10(a1,a1),f10(a1,a2))), % 180.83/180.85 inference(scs_inference,[],[4385,4380,4364,4096,80,2,98])). % 180.83/180.85 cnf(4423,plain, % 180.83/180.85 (P16(f10(x44231,a2),f10(x44231,a1))), % 180.83/180.85 inference(rename_variables,[],[4380])). % 180.83/180.85 cnf(4428,plain, % 180.83/180.85 (P16(f10(a1,a1),f10(a2,a1))), % 180.83/180.85 inference(scs_inference,[],[4385,4121,4380,4423,4364,4211,4096,70,80,2,98,92,17])). % 180.83/180.85 cnf(4430,plain, % 180.83/180.85 (~E(a1,f12(a5))), % 180.83/180.85 inference(scs_inference,[],[4385,4121,4380,4423,4364,4409,4211,4125,4096,70,80,2,98,92,17,3])). % 180.83/180.85 cnf(4432,plain, % 180.83/180.85 (~E(a1,f6(a11))), % 180.83/180.85 inference(scs_inference,[],[4385,4121,4380,4423,4364,4409,4131,4211,4125,4096,35,70,80,2,98,92,17,3,16])). % 180.83/180.85 cnf(4433,plain, % 180.83/180.85 (~P13(f15(a11),f6(a11))), % 180.83/180.85 inference(scs_inference,[],[4385,4121,4380,4423,4364,4409,4131,4211,4125,4096,35,70,80,2,98,92,17,3,16,96])). % 180.83/180.85 cnf(4441,plain, % 180.83/180.85 (P16(f16(a2),f16(a1))), % 180.83/180.85 inference(scs_inference,[],[4088,80])). % 180.83/180.85 cnf(4443,plain, % 180.83/180.85 (~E(f7(a5),f14(x44431))), % 180.83/180.85 inference(scs_inference,[],[4412,4088,80,2])). % 180.83/180.85 cnf(4444,plain, % 180.83/180.85 (~P5(f15(a11),f6(a11))), % 180.83/180.85 inference(scs_inference,[],[4412,4433,4131,4088,80,2,92])). % 180.83/180.85 cnf(4446,plain, % 180.83/180.85 (~P16(f7(a3),f14(x44461))), % 180.83/180.85 inference(scs_inference,[],[4332,4412,4433,4131,4088,310,80,2,92,98])). % 180.83/180.85 cnf(4450,plain, % 180.83/180.85 (~E(f13(x44501),f7(a3))), % 180.83/180.85 inference(scs_inference,[],[4332,4412,4433,4131,4088,261,310,80,2,92,98,17])). % 180.83/180.85 cnf(4452,plain, % 180.83/180.85 (E(f10(a2,a1),f10(a1,a2))), % 180.83/180.85 inference(scs_inference,[],[4422,4332,4412,4433,4131,4093,4088,261,310,80,2,92,98,17,3])). % 180.83/180.85 cnf(4455,plain, % 180.83/180.85 (~P13(x44551,f10(a1,a1))+P13(x44551,f10(a1,a2))), % 180.83/180.85 inference(scs_inference,[],[4422,4332,4412,4433,4070,4131,4093,4088,36,261,310,80,2,92,98,17,3,16,27])). % 180.83/180.85 cnf(4465,plain, % 180.83/180.85 (P16(f10(a2,a1),f10(a1,a2))), % 180.83/180.85 inference(scs_inference,[],[4452,80])). % 180.83/180.85 cnf(4467,plain, % 180.83/180.85 (~E(f7(a3),f13(x44671))), % 180.83/180.85 inference(scs_inference,[],[4452,4450,80,2])). % 180.83/180.85 cnf(4468,plain, % 180.83/180.85 (E(f10(a1,a1),f10(a2,a1))), % 180.83/180.85 inference(scs_inference,[],[4428,4452,4450,4353,80,2,98])). % 180.83/180.85 cnf(4476,plain, % 180.83/180.85 (~E(f14(x44761),f12(a11))), % 180.83/180.85 inference(scs_inference,[],[4428,4452,4127,4450,4147,4353,4139,4422,44,70,219,80,2,98,92,17,3,16])). % 180.83/180.85 cnf(4477,plain, % 180.83/180.85 (~P13(f15(a11),f7(a11))), % 180.83/180.85 inference(scs_inference,[],[4428,4452,4127,4450,4147,4353,4139,4422,44,70,219,80,2,98,92,17,3,16,96])). % 180.83/180.85 cnf(4479,plain, % 180.83/180.85 (~P13(x44791,f10(a1,a1))+P13(x44791,f10(a2,a1))), % 180.83/180.85 inference(scs_inference,[],[4428,4452,4127,4450,4147,4353,4139,4422,44,70,219,80,2,98,92,17,3,16,96,101])). % 180.83/180.85 cnf(4494,plain, % 180.83/180.85 (~E(f12(a11),f14(x44941))), % 180.83/180.85 inference(scs_inference,[],[4476,2])). % 180.83/180.85 cnf(4495,plain, % 180.83/180.85 (~P5(f15(a11),f7(a11))), % 180.83/180.85 inference(scs_inference,[],[4476,4477,4133,2,92])). % 180.83/180.85 cnf(4497,plain, % 180.83/180.85 (~P16(f12(a3),f14(x44971))), % 180.83/180.85 inference(scs_inference,[],[4382,4476,4477,4133,310,2,92,98])). % 180.83/180.85 cnf(4501,plain, % 180.83/180.85 (E(f10(a1,a2),f10(a2,a1))), % 180.83/180.85 inference(scs_inference,[],[4468,4382,4476,4477,4133,4094,310,2,92,98,3])). % 180.83/180.85 cnf(4503,plain, % 180.83/180.85 (~E(a1,f7(a11))), % 180.83/180.85 inference(scs_inference,[],[4468,4382,4476,4477,4133,4094,35,310,2,92,98,3,16])). % 180.83/180.85 cnf(4504,plain, % 180.83/180.85 (~P13(x45041,f7(a1))+P13(x45041,f7(a2))), % 180.83/180.85 inference(scs_inference,[],[4468,4382,4476,4477,4279,4133,4094,35,310,2,92,98,3,16,27])). % 180.83/180.85 cnf(4510,plain, % 180.83/180.85 (~E(f12(a5),a1)), % 180.83/180.85 inference(scs_inference,[],[4430,2])). % 180.83/180.85 cnf(4511,plain, % 180.83/180.85 (~P16(f7(a3),f13(x45111))), % 180.83/180.85 inference(scs_inference,[],[4467,4430,261,2,98])). % 180.83/180.85 cnf(4517,plain, % 180.83/180.85 (~E(a1,f6(a5))), % 180.83/180.85 inference(scs_inference,[],[4467,4430,4291,4285,4064,261,71,2,98,92,3])). % 180.83/180.85 cnf(4518,plain, % 180.83/180.85 (~E(f14(x45181),f6(a5))), % 180.83/180.85 inference(scs_inference,[],[4467,4430,4291,4285,4066,4064,44,261,71,2,98,92,3,16])). % 180.83/180.85 cnf(4519,plain, % 180.83/180.85 (~P13(a5,x45191)+~E(x45191,f9(a5,a2))), % 180.83/180.85 inference(scs_inference,[],[4467,4430,4291,4285,4245,4066,4064,44,261,71,2,98,92,3,16,27])). % 180.83/180.85 cnf(4523,plain, % 180.83/180.85 (~E(f6(a5),f14(x45231))), % 180.83/180.85 inference(scs_inference,[],[4518,2])). % 180.83/180.85 cnf(4524,plain, % 180.83/180.85 (~P5(f15(a5),f12(a5))), % 180.83/180.85 inference(scs_inference,[],[4518,4301,4070,2,92])). % 180.83/180.85 cnf(4530,plain, % 180.83/180.85 (~E(f13(x45301),f7(a11))), % 180.83/180.85 inference(scs_inference,[],[4421,4518,4301,4070,261,310,2,92,98,17])). % 180.83/180.85 cnf(4532,plain, % 180.83/180.85 (~P16(f7(a3),a2)), % 180.83/180.85 inference(scs_inference,[],[4421,4511,4518,4301,4070,261,310,239,2,92,98,17,18])). % 180.83/180.85 cnf(4534,plain, % 180.83/180.85 (~P13(x45341,f10(a1,a2))+P13(x45341,f10(a2,a1))), % 180.83/180.85 inference(scs_inference,[],[4421,4511,4518,4501,4301,4070,261,310,239,2,92,98,17,18,27])). % 180.83/180.85 cnf(4535,plain, % 180.83/180.85 (~E(a2,f6(a3))), % 180.83/180.85 inference(scs_inference,[],[4421,4511,4518,4501,4301,3996,4070,36,261,310,239,2,92,98,17,18,27,16])). % 180.83/180.85 cnf(4549,plain, % 180.83/180.85 (~E(f7(a11),f13(x45491))), % 180.83/180.85 inference(scs_inference,[],[4530,4532,97,2])). % 180.83/180.85 cnf(4550,plain, % 180.83/180.85 (~P16(f12(a3),a1)), % 180.83/180.85 inference(scs_inference,[],[4530,4274,4532,121,97,2,98])). % 180.83/180.85 cnf(4556,plain, % 180.83/180.85 (P16(f9(a1,a1),f9(a1,a2))), % 180.83/180.85 inference(scs_inference,[],[4398,4530,4274,4532,4060,4282,70,121,97,2,98,92,17])). % 180.83/180.85 cnf(4558,plain, % 180.83/180.85 (~P5(a5,f16(a2))), % 180.83/180.85 inference(scs_inference,[],[4398,4530,4274,4532,3142,4060,4282,4088,70,121,97,2,98,92,17,22])). % 180.83/180.85 cnf(4561,plain, % 180.83/180.85 (~E(a2,f7(a3))), % 180.83/180.85 inference(scs_inference,[],[4398,4530,4274,4532,3142,4060,3998,4282,4088,36,70,121,219,97,2,98,92,17,22,3,16])). % 180.83/180.85 cnf(4564,plain, % 180.83/180.85 (~P13(x45641,f10(a2,a1))+P13(x45641,f10(a1,a2))), % 180.83/180.85 inference(scs_inference,[],[4465,4398,4530,4274,4532,3142,4060,3998,4282,4088,36,70,121,219,97,2,98,92,17,22,3,16,1908,101])). % 180.83/180.85 cnf(4575,plain, % 180.83/180.85 (~P5(f12(a3),f15(a1))), % 180.83/180.85 inference(scs_inference,[],[4550,97])). % 180.83/180.85 cnf(4580,plain, % 180.83/180.85 (~P16(f7(a3),a1)), % 180.83/180.85 inference(scs_inference,[],[4390,4550,4277,3998,121,97,2,92,98])). % 180.83/180.85 cnf(4583,plain, % 180.83/180.85 (~E(a1,f12(a11))), % 180.83/180.85 inference(scs_inference,[],[4390,4550,4277,4139,3998,35,121,97,2,92,98,16])). % 180.83/180.85 cnf(4590,plain, % 180.83/180.85 (~P5(f7(a3),f15(a1))), % 180.83/180.85 inference(scs_inference,[],[4580,97])). % 180.83/180.85 cnf(4592,plain, % 180.83/180.85 (~E(f7(a11),a1)), % 180.83/180.85 inference(scs_inference,[],[4503,4580,97,2])). % 180.83/180.85 cnf(4593,plain, % 180.83/180.85 (E(f9(a1,a1),f9(a1,a2))), % 180.83/180.85 inference(scs_inference,[],[4503,4419,4556,4580,97,2,98])). % 180.83/180.85 cnf(4604,plain, % 180.83/180.85 (~P13(f15(a3),f6(a3))), % 180.83/180.85 inference(scs_inference,[],[4503,4419,4556,4580,4004,251,189,70,48,97,2,98,92,112,91,96])). % 180.83/180.85 cnf(4606,plain, % 180.83/180.85 (~P13(x46061,f8(a1))+P13(x46061,f8(a2))), % 180.83/180.85 inference(scs_inference,[],[4503,4419,4556,4580,4383,4004,251,189,70,48,97,2,98,92,112,91,96,27])). % 180.83/180.85 cnf(4612,plain, % 180.83/180.85 (~E(f6(a3),a1)), % 180.83/180.85 inference(scs_inference,[],[4341,2])). % 180.83/180.85 cnf(4615,plain, % 180.83/180.85 (~P16(f7(a5),f14(x46151))), % 180.83/180.85 inference(scs_inference,[],[4443,4341,4604,3996,310,2,92,98])). % 180.83/180.85 cnf(4621,plain, % 180.83/180.85 (P16(f9(a2,a1),f9(a1,a2))), % 180.83/180.85 inference(scs_inference,[],[4593,4443,4341,4604,4095,3996,310,2,92,98,3,80])). % 180.83/180.85 cnf(4623,plain, % 180.83/180.85 (~P13(f15(a3),x46231)+~E(x46231,f6(a3))), % 180.83/180.85 inference(scs_inference,[],[4593,4443,4341,4604,4095,3996,310,2,92,98,3,80,27])). % 180.83/180.85 cnf(4628,plain, % 180.83/180.85 (~E(f13(x46281),f7(a5))), % 180.83/180.85 inference(scs_inference,[],[4615,4432,261,2,17])). % 180.83/180.85 cnf(4630,plain, % 180.83/180.85 (P13(f7(a3),f15(a3))), % 180.83/180.85 inference(scs_inference,[],[4615,4432,4006,261,70,2,17,92])). % 180.83/180.85 cnf(4633,plain, % 180.83/180.85 (~P16(f12(a5),a1)), % 180.83/180.85 inference(scs_inference,[],[4615,4432,4510,4006,261,70,121,2,17,92,98])). % 180.83/180.85 cnf(4637,plain, % 180.83/180.85 (~P5(f12(a5),f15(a1))), % 180.83/180.85 inference(scs_inference,[],[4615,4432,4510,4612,4008,4006,261,70,121,2,17,92,98,3,97])). % 180.83/180.85 cnf(4639,plain, % 180.83/180.85 (~P13(f15(a3),f7(a3))), % 180.83/180.85 inference(scs_inference,[],[4615,4432,4510,4612,4008,4006,261,70,121,2,17,92,98,3,97,96])). % 180.83/180.85 cnf(4641,plain, % 180.83/180.85 (~P13(x46411,f9(a2,a1))+P13(x46411,f9(a1,a2))), % 180.83/180.85 inference(scs_inference,[],[4621,4615,4432,4510,4612,4008,4006,261,70,121,2,17,92,98,3,97,96,101])). % 180.83/180.85 cnf(4651,plain, % 180.83/180.85 (~E(f7(a5),f13(x46511))), % 180.83/180.85 inference(scs_inference,[],[4628,2])). % 180.83/180.85 cnf(4652,plain, % 180.83/180.85 (~P16(f12(a5),f13(x46521))), % 180.83/180.85 inference(scs_inference,[],[4628,4633,4125,2,18])). % 180.83/180.85 cnf(4654,plain, % 180.83/180.85 (~P16(f12(a11),f14(x46541))), % 180.83/180.85 inference(scs_inference,[],[4494,4628,4637,4633,4125,4087,310,2,18,22,98])). % 180.83/180.85 cnf(4662,plain, % 180.83/180.85 (~P13(x46621,f9(a1,a1))+P13(x46621,f9(a1,a2))), % 180.83/180.85 inference(scs_inference,[],[4494,4628,4637,4639,4633,4593,4125,4087,3998,310,219,2,18,22,98,92,3,27])). % 180.83/180.85 cnf(4676,plain, % 180.83/180.85 (~E(f15(a5),f16(a2))), % 180.83/180.85 inference(scs_inference,[],[4253,4558,4193,2,22])). % 180.83/180.85 cnf(4688,plain, % 180.83/180.85 (~E(f15(a2),f15(a5))), % 180.83/180.85 inference(scs_inference,[],[4365,2])). % 180.83/180.85 cnf(4697,plain, % 180.83/180.85 (~P13(a11,x46971)+~E(x46971,f9(a11,a2))), % 180.83/180.85 inference(scs_inference,[],[4365,4523,4143,3865,4131,44,310,71,2,98,92,16,27])). % 180.83/180.85 cnf(4701,plain, % 180.83/180.85 (~E(f16(a2),f15(a5))), % 180.83/180.85 inference(scs_inference,[],[4676,2])). % 180.83/180.85 cnf(4702,plain, % 180.83/180.85 (~E(f15(a11),f15(a2))), % 180.83/180.85 inference(scs_inference,[],[4676,4080,4193,2,22])). % 180.83/180.85 cnf(4703,plain, % 180.83/180.85 (P5(x47031,f15(x47031))), % 180.83/180.85 inference(rename_variables,[],[4193])). % 180.83/180.85 cnf(4704,plain, % 180.83/180.85 (P13(x47041,f15(x47041))), % 180.83/180.85 inference(scs_inference,[],[4676,4080,4193,4703,70,2,22,92])). % 180.83/180.85 cnf(4709,plain, % 180.83/180.85 (~P13(f15(a5),a5)), % 180.83/180.85 inference(scs_inference,[],[4676,4688,4080,4193,4703,4087,70,2,22,92,3,4519,96])). % 180.83/180.85 cnf(4717,plain, % 180.83/180.85 (~P13(f15(x47171),x47171)), % 180.83/180.85 inference(scs_inference,[],[4704,96])). % 180.83/180.85 cnf(4719,plain, % 180.83/180.85 (~E(f16(a2),f15(a11))), % 180.83/180.85 inference(scs_inference,[],[4704,4321,96,2])). % 180.83/180.85 cnf(4721,plain, % 180.83/180.85 (~P16(f7(a11),f13(x47211))), % 180.83/180.85 inference(scs_inference,[],[4704,4321,4549,4709,4367,261,96,2,26,98])). % 180.83/180.85 cnf(4727,plain, % 180.83/180.85 (~E(f16(a1),f15(a5))), % 180.83/180.85 inference(scs_inference,[],[4704,4321,4549,4701,4709,4367,67,4088,261,96,2,26,98,92,3])). % 180.83/180.85 cnf(4728,plain, % 180.83/180.85 (~E(f15(a11),f9(a11,a2))), % 180.83/180.85 inference(scs_inference,[],[4704,4321,4549,4701,4709,4367,67,4088,261,96,2,26,98,92,3,4697])). % 180.83/180.85 cnf(4730,plain, % 180.83/180.85 (~E(f8(a5),f15(a5))), % 180.83/180.85 inference(scs_inference,[],[4704,4321,4549,4701,4709,4367,67,4088,261,96,2,26,98,92,3,4697,151])). % 180.83/180.85 cnf(4731,plain, % 180.83/180.85 (~E(f9(a5,a1),f15(a5))), % 180.83/180.85 inference(scs_inference,[],[4704,4227,4321,4549,4701,4709,4367,67,4088,261,96,2,26,98,92,3,4697,151,21])). % 180.83/180.85 cnf(4732,plain, % 180.83/180.85 (~P13(x47321,f6(a2))+P13(x47321,f6(a1))), % 180.83/180.85 inference(scs_inference,[],[4704,4227,4321,4549,4701,4709,4089,4367,67,4088,261,96,2,26,98,92,3,4697,151,21,27])). % 180.83/180.85 cnf(4740,plain, % 180.83/180.85 (~E(f15(a2),f16(a3))), % 180.83/180.85 inference(scs_inference,[],[4413,2])). % 180.83/180.85 cnf(4741,plain, % 180.83/180.85 (~E(f13(x47411),f12(a11))), % 180.83/180.85 inference(scs_inference,[],[4413,4654,261,2,17])). % 180.83/180.85 cnf(4745,plain, % 180.83/180.85 (E(f10(a1,a1),f10(a2,a2))+~P16(f10(a1,a1),f10(a2,a2))), % 180.83/180.85 inference(scs_inference,[],[4413,4654,313,4229,4704,261,2,17,27,98])). % 180.83/180.85 cnf(4747,plain, % 180.83/180.85 (~E(f16(a1),f15(a11))), % 180.83/180.85 inference(scs_inference,[],[4413,4654,4719,313,4229,4704,4088,261,2,17,27,98,3])). % 180.83/180.85 cnf(4755,plain, % 180.83/180.85 (~P16(f12(a11),f13(x47551))), % 180.83/180.85 inference(scs_inference,[],[4731,4652,4741,261,239,2,18,98])). % 180.83/180.85 cnf(4759,plain, % 180.83/180.85 (~E(f15(a1),f16(a3))), % 180.83/180.85 inference(scs_inference,[],[4731,4652,4741,4740,4087,261,239,2,18,98,3])). % 180.83/180.85 cnf(4763,plain, % 180.83/180.85 (~E(a1,x47631)+P10(x47631)), % 180.83/180.85 inference(scs_inference,[],[4731,4652,4741,4740,4181,3821,4087,261,239,160,2,18,98,3,106,33])). % 180.83/180.85 cnf(4766,plain, % 180.83/180.85 (~E(f9(a11,a1),f15(a11))), % 180.83/180.85 inference(scs_inference,[],[4728,4096,2,3])). % 180.83/180.85 cnf(4774,plain, % 180.83/180.85 (~P16(f6(a5),a1)), % 180.83/180.85 inference(scs_inference,[],[4517,121,2,98])). % 180.83/180.85 cnf(4777,plain, % 180.83/180.85 (~E(f13(a2),f6(a11))), % 180.83/180.85 inference(scs_inference,[],[4517,4343,239,121,2,98,3])). % 180.83/180.85 cnf(4781,plain, % 180.83/180.85 (P5(f12(a3),f16(a3))), % 180.83/180.85 inference(scs_inference,[],[4517,4343,1882,239,121,1880,48,2,98,3,112,91])). % 180.83/180.85 cnf(4783,plain, % 180.83/180.85 (~P5(f6(a5),f15(a1))), % 180.83/180.85 inference(scs_inference,[],[4517,4343,1882,239,121,1880,48,2,98,3,112,91,97])). % 180.83/180.85 cnf(4785,plain, % 180.83/180.85 (~E(f15(a11),f8(a11))), % 180.83/180.85 inference(scs_inference,[],[4517,4343,1882,266,4704,239,121,1880,48,2,98,3,112,91,97,27])). % 180.83/180.85 cnf(4797,plain, % 180.83/180.85 (~P5(f6(a5),f15(a2))), % 180.83/180.85 inference(scs_inference,[],[4766,4783,4087,2,22])). % 180.83/180.85 cnf(4798,plain, % 180.83/180.85 (~E(f13(a1),f6(a11))), % 180.83/180.85 inference(scs_inference,[],[4766,4777,4783,4085,4087,2,22,3])). % 180.83/180.85 cnf(4801,plain, % 180.83/180.85 (~E(a1,x48011)+P8(x48011)), % 180.83/180.85 inference(scs_inference,[],[4766,4777,4783,4270,4178,4085,4087,2,22,3,92,30])). % 180.83/180.85 cnf(4826,plain, % 180.83/180.85 (~E(a1,x48261)+P12(x48261)), % 180.83/180.85 inference(scs_inference,[],[4730,4759,4774,4151,4064,2,18,98,28])). % 180.83/180.85 cnf(4828,plain, % 180.83/180.85 (~E(f15(a2),f15(a11))), % 180.83/180.85 inference(scs_inference,[],[4702,2])). % 180.83/180.85 cnf(4842,plain, % 180.83/180.85 (~E(f15(a1),f15(a11))), % 180.83/180.85 inference(scs_inference,[],[4785,4798,4828,4074,4704,4087,261,2,98,27,3])). % 180.83/180.85 cnf(4843,plain, % 180.83/180.85 (~P16(f6(a11),f13(a2))), % 180.83/180.85 inference(scs_inference,[],[4785,4798,4828,4074,4085,4704,4087,261,2,98,27,3,18])). % 180.83/180.85 cnf(4882,plain, % 180.83/180.85 (~P5(f6(a11),f15(a2))), % 180.83/180.85 inference(scs_inference,[],[4842,4843,4535,189,239,2,18,98,97])). % 180.83/180.85 cnf(4884,plain, % 180.83/180.85 (~E(a1,x48841)+P11(x48841)), % 180.83/180.85 inference(scs_inference,[],[4842,4843,4535,4152,189,239,2,18,98,97,32])). % 180.83/180.85 cnf(4946,plain, % 180.83/180.85 (~P16(f7(a11),a1)), % 180.83/180.85 inference(scs_inference,[],[4561,4592,121,2,98])). % 180.83/180.85 cnf(4949,plain, % 180.83/180.85 (~P5(f7(a11),f15(a1))), % 180.83/180.85 inference(scs_inference,[],[4561,4592,121,2,98,97])). % 180.83/180.85 cnf(4951,plain, % 180.83/180.85 (~E(a1,x49511)+P14(x49511)), % 180.83/180.85 inference(scs_inference,[],[4561,4592,4149,121,2,98,97,29])). % 180.83/180.85 cnf(4988,plain, % 180.83/180.85 (~E(f6(a3),f13(x49881))), % 180.83/180.85 inference(scs_inference,[],[4309,2])). % 180.83/180.85 cnf(5014,plain, % 180.83/180.85 (~E(a1,x50141)+P7(x50141)), % 180.83/180.85 inference(scs_inference,[],[4741,4155,2,31])). % 180.83/180.85 cnf(5094,plain, % 180.83/180.85 (~P16(f7(a5),f13(x50941))), % 180.83/180.85 inference(scs_inference,[],[4651,261,98])). % 180.83/180.85 cnf(5098,plain, % 180.83/180.85 (~E(x50981,f15(a11))+~E(f16(a1),x50981)), % 180.83/180.85 inference(scs_inference,[],[4747,4651,261,98,3])). % 180.83/180.85 cnf(5114,plain, % 180.83/180.85 (~E(x51141,f15(a3))+~E(f16(a1),x51141)), % 180.83/180.85 inference(scs_inference,[],[4363,3])). % 180.83/180.85 cnf(5132,plain, % 180.83/180.85 (~E(x51321,f15(a5))+~E(f16(a1),x51321)), % 180.83/180.85 inference(scs_inference,[],[4727,4233,26,3])). % 180.83/180.85 cnf(5192,plain, % 180.83/180.85 (P16(a4,x51921)+~E(f16(a4),f16(x51921))), % 180.83/180.85 inference(scs_inference,[],[142,48,99])). % 180.83/180.85 cnf(5216,plain, % 180.83/180.85 (P16(a4,x52161)+~E(f16(x52161),f16(a4))), % 180.83/180.85 inference(scs_inference,[],[38,60,48,102,91,96,111])). % 180.83/180.85 cnf(5229,plain, % 180.83/180.85 (~E(x52291,a11)+~E(a1,x52291)), % 180.83/180.85 inference(scs_inference,[],[3133,3])). % 180.83/180.85 cnf(5241,plain, % 180.83/180.85 (~E(x52411,a5)+~E(a1,x52411)), % 180.83/180.85 inference(scs_inference,[],[3145,2312,26,3])). % 180.83/180.85 cnf(5270,plain, % 180.83/180.85 (~E(x52701,a3)+~E(a1,x52701)), % 180.83/180.85 inference(scs_inference,[],[3169,3])). % 180.83/180.85 cnf(5324,plain, % 180.83/180.85 (~E(x53241,f16(a3))+~E(f16(a1),x53241)), % 180.83/180.85 inference(scs_inference,[],[4031,3])). % 180.83/180.85 cnf(5390,plain, % 180.83/180.85 (~E(x53901,f12(a3))+~E(a1,x53901)), % 180.83/180.85 inference(scs_inference,[],[4223,3])). % 180.83/180.85 cnf(5393,plain, % 180.83/180.85 (~E(x53931,f7(a5))+~E(a1,x53931)), % 180.83/180.85 inference(scs_inference,[],[4253,3])). % 180.83/180.85 cnf(5603,plain, % 180.83/180.85 (~E(x56031,f12(a5))+~E(a1,x56031)), % 180.83/180.85 inference(scs_inference,[],[4430,3])). % 180.83/180.85 cnf(5624,plain, % 180.83/180.85 (~E(x56241,f7(a11))+~E(a1,x56241)), % 180.83/180.85 inference(scs_inference,[],[4503,3])). % 180.83/180.85 cnf(5640,plain, % 180.83/180.85 (~E(x56401,f12(a11))+~E(a1,x56401)), % 180.83/180.85 inference(scs_inference,[],[4583,3])). % 180.83/180.85 cnf(5738,plain, % 180.83/180.85 (~E(x57381,f6(a3))+~E(a1,x57381)), % 180.83/180.85 inference(scs_inference,[],[4341,3])). % 180.83/180.85 cnf(5742,plain, % 180.83/180.85 (~E(x57421,f7(a3))+~E(a1,x57421)), % 180.83/180.85 inference(scs_inference,[],[4390,3])). % 180.83/180.85 cnf(5751,plain, % 180.83/180.85 (~E(x57511,f6(a11))+~E(a1,x57511)), % 180.83/180.85 inference(scs_inference,[],[4432,3])). % 180.83/180.85 cnf(5759,plain, % 180.83/180.85 (~E(x57591,f6(a5))+~E(a1,x57591)), % 180.83/180.85 inference(scs_inference,[],[4517,3])). % 180.83/180.85 cnf(5795,plain, % 180.83/180.85 (~P13(f7(a11),f16(a2))), % 180.83/180.85 inference(scs_inference,[],[48,4946,4088,99])). % 180.83/180.85 cnf(5796,plain, % 180.83/180.85 (P9(f16(x57961))), % 180.83/180.85 inference(rename_variables,[],[48])). % 180.83/180.85 cnf(5801,plain, % 180.83/180.85 (P13(f12(a3),f16(x58011))+~E(f16(x58011),f16(a3))), % 180.83/180.85 inference(scs_inference,[],[48,5796,4946,1882,4251,4088,1880,71,99,92,106,102])). % 180.83/180.85 cnf(5918,plain, % 180.83/180.85 (P16(f10(a1,x59181),f10(a2,x59181))), % 180.83/180.85 inference(scs_inference,[],[60,4093,17])). % 180.83/180.85 cnf(5937,plain, % 180.83/180.85 (P16(f10(a1,a1),f10(a2,a2))), % 180.83/180.85 inference(scs_inference,[],[60,4211,17])). % 180.83/180.85 cnf(5939,plain, % 180.83/180.85 (E(f10(a1,a1),f10(a2,a2))), % 180.83/180.85 inference(scs_inference,[],[5937,4745])). % 180.83/180.85 cnf(5962,plain, % 180.83/180.85 (P16(f10(x59621,a1),f10(x59621,a2))), % 180.83/180.85 inference(scs_inference,[],[60,4094,17])). % 180.83/180.85 cnf(5967,plain, % 180.83/180.85 (E(f10(x59671,a1),f10(x59671,a2))), % 180.83/180.85 inference(scs_inference,[],[5962,4380,98])). % 180.83/180.85 cnf(6037,plain, % 180.83/180.85 (~P5(f15(a3),a3)), % 180.83/180.85 inference(scs_inference,[],[65,4717,92])). % 180.83/180.85 cnf(6058,plain, % 180.83/180.85 (~E(f8(f15(a1)),f12(a3))), % 180.83/180.85 inference(scs_inference,[],[4444,187,5241,148,5390])). % 180.83/180.85 cnf(6066,plain, % 180.83/180.85 (~P13(f15(x60661),x60661)), % 180.83/180.85 inference(rename_variables,[],[4717])). % 180.83/180.85 cnf(6068,plain, % 180.83/180.85 (~P13(f15(x60681),x60681)), % 180.83/180.85 inference(rename_variables,[],[4717])). % 180.83/180.85 cnf(6070,plain, % 180.83/180.85 (~P13(f15(x60701),x60701)), % 180.83/180.85 inference(rename_variables,[],[4717])). % 180.83/180.85 cnf(6072,plain, % 180.83/180.85 (~P13(f15(x60721),x60721)), % 180.83/180.85 inference(rename_variables,[],[4717])). % 180.83/180.85 cnf(6074,plain, % 180.83/180.85 (~P13(f15(x60741),x60741)), % 180.83/180.85 inference(rename_variables,[],[4717])). % 180.83/180.85 cnf(6075,plain, % 180.83/180.85 (~P13(f15(f10(a1,a2)),f10(a1,a1))), % 180.83/180.85 inference(scs_inference,[],[4444,4717,6066,6068,6070,6072,6074,187,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455])). % 180.83/180.85 cnf(6076,plain, % 180.83/180.85 (~P13(f15(x60761),x60761)), % 180.83/180.85 inference(rename_variables,[],[4717])). % 180.83/180.85 cnf(6077,plain, % 180.83/180.85 (~P13(f15(f10(a2,a1)),f10(a1,a2))), % 180.83/180.85 inference(scs_inference,[],[4444,4717,6066,6068,6070,6072,6074,6076,187,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455,4534])). % 180.83/180.85 cnf(6078,plain, % 180.83/180.85 (~P13(f15(x60781),x60781)), % 180.83/180.85 inference(rename_variables,[],[4717])). % 180.83/180.85 cnf(6080,plain, % 180.83/180.85 (~P13(f15(x60801),x60801)), % 180.83/180.85 inference(rename_variables,[],[4717])). % 180.83/180.85 cnf(6083,plain, % 180.83/180.85 (~P13(f15(x60831),x60831)), % 180.83/180.85 inference(rename_variables,[],[4717])). % 180.83/180.85 cnf(6084,plain, % 180.83/180.85 (P13(f9(f16(a4),f8(f15(a1))),f16(a4))), % 180.83/180.85 inference(scs_inference,[],[4444,4264,4717,6066,6068,6070,6072,6074,6076,6078,6080,187,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455,4534,4641,4662,100])). % 180.83/180.85 cnf(6086,plain, % 180.83/180.85 (P5(f6(f6(f7(a5))),f15(f6(f7(a5))))), % 180.83/180.85 inference(scs_inference,[],[4444,4264,904,4717,6066,6068,6070,6072,6074,6076,6078,6080,187,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455,4534,4641,4662,100,87])). % 180.83/180.85 cnf(6088,plain, % 180.83/180.85 (P5(f10(a1,a1),f15(f10(a2,a2)))), % 180.83/180.85 inference(scs_inference,[],[4444,4264,904,5937,4717,6066,6068,6070,6072,6074,6076,6078,6080,187,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455,4534,4641,4662,100,87,94])). % 180.83/180.85 cnf(6095,plain, % 180.83/180.85 (E(f16(f13(f13(a2))),f16(f13(f14(f13(a2)))))), % 180.83/180.85 inference(scs_inference,[],[4444,4264,2414,4497,904,5937,4717,6066,6068,6070,6072,6074,6076,6078,6080,187,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455,4534,4641,4662,100,87,94,97,1908,7,9])). % 180.83/180.85 cnf(6096,plain, % 180.83/180.85 (~P13(f9(f15(a4),f16(a4)),f16(a4))), % 180.83/180.85 inference(scs_inference,[],[4444,4264,2414,4497,904,5937,4717,6066,6068,6070,6072,6074,6076,6078,6080,126,187,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455,4534,4641,4662,100,87,94,97,1908,7,9,105])). % 180.83/180.85 cnf(6100,plain, % 180.83/180.85 (~P13(f15(x61001),x61001)), % 180.83/180.85 inference(rename_variables,[],[4717])). % 180.83/180.85 cnf(6106,plain, % 180.83/180.85 (~P13(f15(x61061),x61061)), % 180.83/180.85 inference(rename_variables,[],[4717])). % 180.83/180.85 cnf(6110,plain, % 180.83/180.85 (P5(f12(f6(f7(a5))),f15(f6(f7(a5))))), % 180.83/180.85 inference(scs_inference,[],[4444,4264,2414,4497,904,5937,4704,4717,6066,6068,6070,6072,6074,6076,6078,6080,6083,6100,126,187,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455,4534,4641,4662,100,87,94,97,1908,7,9,105,12,578,76,4623,608,13,10,4,86])). % 180.83/180.85 cnf(6112,plain, % 180.83/180.85 (P16(f15(f10(x61121,f8(f15(a1)))),f15(f10(x61121,a1)))), % 180.83/180.85 inference(scs_inference,[],[4444,4264,2414,2446,4497,904,5937,4704,4717,6066,6068,6070,6072,6074,6076,6078,6080,6083,6100,126,187,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455,4534,4641,4662,100,87,94,97,1908,7,9,105,12,578,76,4623,608,13,10,4,86,80])). % 180.83/180.85 cnf(6114,plain, % 180.83/180.85 (P5(f7(f6(f7(a5))),f15(f6(f7(a5))))), % 180.83/180.85 inference(scs_inference,[],[4444,4264,2414,2446,4497,904,5937,4704,4717,6066,6068,6070,6072,6074,6076,6078,6080,6083,6100,126,187,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455,4534,4641,4662,100,87,94,97,1908,7,9,105,12,578,76,4623,608,13,10,4,86,80,88])). % 180.83/180.85 cnf(6117,plain, % 180.83/180.85 (E(f15(f13(f13(a2))),f15(f13(f14(f13(a2)))))), % 180.83/180.85 inference(scs_inference,[],[4444,4264,2414,2446,4497,904,5937,4704,4717,6066,6068,6070,6072,6074,6076,6078,6080,6083,6100,126,187,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455,4534,4641,4662,100,87,94,97,1908,7,9,105,12,578,76,4623,608,13,10,4,86,80,88,6,8])). % 180.83/180.85 cnf(6118,plain, % 180.83/180.85 (E(f8(f13(f13(a2))),f8(f13(f14(f13(a2)))))), % 180.83/180.85 inference(scs_inference,[],[4444,4264,2414,2446,4497,904,5937,4704,4717,6066,6068,6070,6072,6074,6076,6078,6080,6083,6100,126,187,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455,4534,4641,4662,100,87,94,97,1908,7,9,105,12,578,76,4623,608,13,10,4,86,80,88,6,8,15])). % 180.83/180.85 cnf(6120,plain, % 180.83/180.85 (~P1(f7(f6(f7(a5))))), % 180.83/180.85 inference(scs_inference,[],[4444,4264,2414,2446,4497,904,5937,4704,4717,6066,6068,6070,6072,6074,6076,6078,6080,6083,6100,126,187,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455,4534,4641,4662,100,87,94,97,1908,7,9,105,12,578,76,4623,608,13,10,4,86,80,88,6,8,15,14,84])). % 180.83/180.85 cnf(6123,plain, % 180.83/180.85 (~P1(f6(f6(f7(a5))))), % 180.83/180.85 inference(scs_inference,[],[4444,4264,2414,2446,4497,904,5937,4704,4717,6066,6068,6070,6072,6074,6076,6078,6080,6083,6100,126,187,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455,4534,4641,4662,100,87,94,97,1908,7,9,105,12,578,76,4623,608,13,10,4,86,80,88,6,8,15,14,84,5,83])). % 180.83/180.85 cnf(6125,plain, % 180.83/180.85 (E(f8(f15(a2)),a1)), % 180.83/180.85 inference(scs_inference,[],[4444,4264,2414,2446,4497,489,904,5937,4704,4717,6066,6068,6070,6072,6074,6076,6078,6080,6083,6100,126,187,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455,4534,4641,4662,100,87,94,97,1908,7,9,105,12,578,76,4623,608,13,10,4,86,80,88,6,8,15,14,84,5,83,72])). % 180.83/180.85 cnf(6133,plain, % 180.83/180.85 (~P1(f12(f6(f7(a5))))), % 180.83/180.85 inference(scs_inference,[],[4444,1342,4264,2414,2446,4497,489,904,5937,4704,4717,6066,6068,6070,6072,6074,6076,6078,6080,6083,6100,126,187,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455,4534,4641,4662,100,87,94,97,1908,7,9,105,12,578,76,4623,608,13,10,4,86,80,88,6,8,15,14,84,5,83,72,11,77,2,96,82])). % 180.83/180.85 cnf(6138,plain, % 180.83/180.85 (~P16(f7(a5),f8(f15(a2)))), % 180.83/180.85 inference(scs_inference,[],[4444,1342,4264,2414,2446,5094,4497,489,1339,904,5937,859,4704,4717,6066,6068,6070,6072,6074,6076,6078,6080,6083,6100,126,187,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455,4534,4641,4662,100,87,94,97,1908,7,9,105,12,578,76,4623,608,13,10,4,86,80,88,6,8,15,14,84,5,83,72,11,77,2,96,82,151,91,18])). % 180.83/180.85 cnf(6140,plain, % 180.83/180.85 (~P5(f15(a3),f15(f15(a1)))), % 180.83/180.85 inference(scs_inference,[],[4444,1342,4264,2414,2446,5094,4590,4497,4630,489,1339,904,5937,859,4704,4717,6066,6068,6070,6072,6074,6076,6078,6080,6083,6100,126,187,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455,4534,4641,4662,100,87,94,97,1908,7,9,105,12,578,76,4623,608,13,10,4,86,80,88,6,8,15,14,84,5,83,72,11,77,2,96,82,151,91,18,104])). % 180.83/180.85 cnf(6145,plain, % 180.83/180.85 (P9(f16(x61451))), % 180.83/180.85 inference(rename_variables,[],[48])). % 180.83/180.85 cnf(6152,plain, % 180.83/180.85 (~P13(f15(x61521),x61521)), % 180.83/180.85 inference(rename_variables,[],[4717])). % 180.83/180.85 cnf(6162,plain, % 180.83/180.85 (P16(f8(f15(a1)),x61621)), % 180.83/180.85 inference(rename_variables,[],[1963])). % 180.83/180.85 cnf(6163,plain, % 180.83/180.85 (~P5(f15(x61631),f15(f8(f15(a2))))), % 180.83/180.85 inference(scs_inference,[],[65,4444,4495,863,1342,115,3772,4264,2414,2446,2462,1351,3621,5094,3120,4590,4497,4630,1963,489,1339,904,5937,118,3996,859,4193,4704,4717,6066,6068,6070,6072,6074,6076,6078,6080,6083,6100,6106,61,126,187,48,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455,4534,4641,4662,100,87,94,97,1908,7,9,105,12,578,76,4623,608,13,10,4,86,80,88,6,8,15,14,84,5,83,72,11,77,2,96,82,151,91,18,104,26,110,21,3,27,89,92,22,16,17,103])). % 180.83/180.85 cnf(6166,plain, % 180.83/180.85 (P16(f8(f15(a1)),x61661)), % 180.83/180.85 inference(rename_variables,[],[1963])). % 180.83/180.85 cnf(6169,plain, % 180.83/180.85 (~P13(f15(x61691),x61691)), % 180.83/180.85 inference(rename_variables,[],[4717])). % 180.83/180.85 cnf(6171,plain, % 180.83/180.85 (P13(f8(f15(a1)),f16(x61711))), % 180.83/180.85 inference(scs_inference,[],[65,4444,4495,863,1342,115,3772,4264,1152,2414,2446,2462,1351,3621,5094,3120,4590,4497,4630,1963,6162,6166,489,141,1339,904,5937,118,3996,859,4193,4704,4717,6066,6068,6070,6072,6074,6076,6078,6080,6083,6100,6106,6152,61,126,187,48,6145,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455,4534,4641,4662,100,87,94,97,1908,7,9,105,12,578,76,4623,608,13,10,4,86,80,88,6,8,15,14,84,5,83,72,11,77,2,96,82,151,91,18,104,26,110,21,3,27,89,92,22,16,17,103,98,101,112])). % 180.83/180.85 cnf(6172,plain, % 180.83/180.85 (P9(f16(x61721))), % 180.83/180.85 inference(rename_variables,[],[48])). % 180.83/180.85 cnf(6177,plain, % 180.83/180.85 (~E(f16(a2),f16(f7(a11)))), % 180.83/180.85 inference(scs_inference,[],[65,4444,4495,863,1342,115,3772,4264,1152,2414,2446,2462,1351,5795,3621,5094,4446,3120,4590,4497,4630,1963,6162,6166,489,141,1339,904,5937,118,4123,3996,859,4193,4704,4717,6066,6068,6070,6072,6074,6076,6078,6080,6083,6100,6106,6152,61,126,46,187,60,48,6145,6172,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455,4534,4641,4662,100,87,94,97,1908,7,9,105,12,578,76,4623,608,13,10,4,86,80,88,6,8,15,14,84,5,83,72,11,77,2,96,82,151,91,18,104,26,110,21,3,27,89,92,22,16,17,103,98,101,112,99,102])). % 180.83/180.85 cnf(6186,plain, % 180.83/180.85 (~P13(f15(x61861),x61861)), % 180.83/180.85 inference(rename_variables,[],[4717])). % 180.83/180.85 cnf(6188,plain, % 180.83/180.85 (~P13(f15(x61881),x61881)), % 180.83/180.85 inference(rename_variables,[],[4717])). % 180.83/180.85 cnf(6190,plain, % 180.83/180.85 (~P13(f15(x61901),x61901)), % 180.83/180.85 inference(rename_variables,[],[4717])). % 180.83/180.85 cnf(6192,plain, % 180.83/180.85 (~P13(f15(f10(a2,a1)),f10(a1,a1))), % 180.83/180.85 inference(scs_inference,[],[65,4444,4495,863,1342,115,3772,4264,1152,2414,2446,2462,1351,5795,3621,5094,4446,3120,4590,4497,4630,1963,6162,6166,489,141,1339,904,5937,118,4123,3996,859,4193,4704,4717,6066,6068,6070,6072,6074,6076,6078,6080,6083,6100,6106,6152,6169,6186,6188,6190,61,126,46,187,60,48,6145,6172,5241,148,5390,5603,5640,5738,5742,5751,5759,2314,4504,4732,865,1892,4455,4534,4641,4662,100,87,94,97,1908,7,9,105,12,578,76,4623,608,13,10,4,86,80,88,6,8,15,14,84,5,83,72,11,77,2,96,82,151,91,18,104,26,110,21,3,27,89,92,22,16,17,103,98,101,112,99,102,5229,5270,5393,5624,4394,4606,4295,4479])). % 180.83/180.85 cnf(6215,plain, % 180.83/180.85 (P5(f6(f7(a5)),f15(f7(a5)))), % 180.83/180.85 inference(scs_inference,[],[4524,6138,4056,148,100,87])). % 180.83/180.85 cnf(6217,plain, % 180.83/180.85 (P5(f15(f10(x62171,f8(f15(a1)))),f15(f15(f10(x62171,a1))))), % 180.83/180.85 inference(scs_inference,[],[4524,6138,6112,4056,148,100,87,94])). % 180.83/180.85 cnf(6219,plain, % 180.83/180.85 (~P5(f7(a5),f15(f8(f15(a2))))), % 180.83/180.85 inference(scs_inference,[],[4524,6138,6112,4056,148,100,87,94,97])). % 180.83/180.85 cnf(6224,plain, % 180.83/180.85 (E(f16(f8(f15(a2))),f16(a1))), % 180.83/180.85 inference(scs_inference,[],[4524,6138,6125,6112,4311,4056,148,100,87,94,97,1908,7,9])). % 180.83/180.85 cnf(6228,plain, % 180.83/180.85 (~E(a4,f9(f15(a4),f16(a4)))), % 180.83/180.85 inference(scs_inference,[],[4524,6096,6138,6125,6120,6112,4311,4056,148,100,87,94,97,1908,7,9,76,12,608])). % 180.83/180.85 cnf(6234,plain, % 180.83/180.85 (P5(f7(f7(a5)),f15(f7(a5)))), % 180.83/180.85 inference(scs_inference,[],[4524,6096,6138,6125,6120,6112,4311,4056,148,100,87,94,97,1908,7,9,76,12,608,10,13,80,4,88])). % 180.83/180.85 cnf(6236,plain, % 180.83/180.85 (P5(f12(f7(a5)),f15(f7(a5)))), % 180.83/180.85 inference(scs_inference,[],[4524,6096,6138,6125,6120,6112,4311,4056,148,100,87,94,97,1908,7,9,76,12,608,10,13,80,4,88,86])). % 180.83/180.85 cnf(6240,plain, % 180.83/180.85 (E(f10(f8(f15(a2)),x62401),f10(a1,x62401))), % 180.83/180.85 inference(scs_inference,[],[4524,6096,6138,6125,6120,6112,4311,4056,148,100,87,94,97,1908,7,9,76,12,608,10,13,80,4,88,86,84,6])). % 180.83/180.85 cnf(6241,plain, % 180.83/180.85 (E(f15(f8(f15(a2))),f15(a1))), % 180.83/180.85 inference(scs_inference,[],[4524,6096,6138,6125,6120,6112,4311,4056,148,100,87,94,97,1908,7,9,76,12,608,10,13,80,4,88,86,84,6,8])). % 180.83/180.85 cnf(6258,plain, % 180.83/180.85 (~P16(a5,f8(f15(a2)))), % 180.83/180.85 inference(scs_inference,[],[4524,6058,6096,6171,6138,6125,6120,6112,4356,4311,4056,480,148,100,87,94,97,1908,7,9,76,12,608,10,13,80,4,88,86,84,6,8,83,14,15,5,11,77,2,96,82,151,91,18])). % 180.83/180.85 cnf(6259,plain, % 180.83/180.85 (~P5(f15(f15(a5)),f15(f12(a5)))), % 180.83/180.85 inference(scs_inference,[],[4524,6058,6096,6171,6138,6125,6120,6112,4356,4311,4056,480,4704,148,100,87,94,97,1908,7,9,76,12,608,10,13,80,4,88,86,84,6,8,83,14,15,5,11,77,2,96,82,151,91,18,104])). % 180.83/180.85 cnf(6260,plain, % 180.83/180.85 (P13(x62601,f15(x62601))), % 180.83/180.85 inference(rename_variables,[],[4704])). % 180.83/180.85 cnf(6262,plain, % 180.83/180.85 (~P13(f15(f10(a2,f8(f15(a1)))),f10(a1,a2))), % 180.83/180.85 inference(scs_inference,[],[4524,6058,6077,6096,6171,6138,6125,6120,6112,4356,4311,2446,4056,480,4704,148,100,87,94,97,1908,7,9,76,12,608,10,13,80,4,88,86,84,6,8,83,14,15,5,11,77,2,96,82,151,91,18,104,26])). % 180.83/180.85 cnf(6265,plain, % 180.83/180.85 (P5(f10(a1,a2),f15(f10(a2,a2)))), % 180.83/180.85 inference(scs_inference,[],[4524,6058,6077,6096,6171,6088,6177,6138,6125,6120,6112,4356,4311,5967,2446,4056,480,4704,4088,148,100,87,94,97,1908,7,9,76,12,608,10,13,80,4,88,86,84,6,8,83,14,15,5,11,77,2,96,82,151,91,18,104,26,3,21])). % 180.83/180.85 cnf(6272,plain, % 180.83/180.85 (P5(f8(f10(a1,a1)),f10(a2,a2))), % 180.83/180.85 inference(scs_inference,[],[4524,1890,6058,6077,6096,6171,6088,6177,6138,6125,6120,6112,4356,5939,4311,5967,2446,4056,480,4704,6260,61,70,4088,148,100,87,94,97,1908,7,9,76,12,608,10,13,80,4,88,86,84,6,8,83,14,15,5,11,77,2,96,82,151,91,18,104,26,3,21,27,92,22])). % 180.83/180.85 cnf(6277,plain, % 180.83/180.85 (~P5(f16(x62771),f15(f8(f15(a1))))), % 180.83/180.85 inference(scs_inference,[],[4524,1890,6058,6077,6096,6171,6088,6177,6138,6125,6120,2494,6112,4356,5939,4311,5967,2446,227,4056,480,4704,6260,61,70,4088,60,148,100,87,94,97,1908,7,9,76,12,608,10,13,80,4,88,86,84,6,8,83,14,15,5,11,77,2,96,82,151,91,18,104,26,3,21,27,92,22,16,17,103])). % 180.83/180.85 cnf(6279,plain, % 180.83/180.85 (E(f8(f15(a1)),f8(f15(f8(f15(a1)))))), % 180.83/180.85 inference(scs_inference,[],[4524,1890,6058,6077,6096,6171,6088,6177,6138,6125,6120,2494,6112,4356,5939,4311,5967,2446,1963,227,4056,118,480,4704,6260,61,70,4088,60,148,100,87,94,97,1908,7,9,76,12,608,10,13,80,4,88,86,84,6,8,83,14,15,5,11,77,2,96,82,151,91,18,104,26,3,21,27,92,22,16,17,103,98])). % 180.83/180.85 cnf(6302,plain, % 180.83/180.85 (~P16(a4,f9(f15(a4),f16(a4)))), % 180.83/180.85 inference(scs_inference,[],[6228,1123])). % 180.83/180.85 cnf(6309,plain, % 180.83/180.85 (P5(f8(f16(a2)),f16(a1))), % 180.83/180.85 inference(scs_inference,[],[4088,6138,4080,91,2,80,552,152])). % 180.83/180.85 cnf(6312,plain, % 180.83/180.85 (~P16(f15(a3),f15(a1))), % 180.83/180.85 inference(scs_inference,[],[4088,6138,4080,4002,6140,91,2,80,552,152,97,94])). % 180.83/180.85 cnf(6322,plain, % 180.83/180.85 (P9(f16(x63221))), % 180.83/180.85 inference(rename_variables,[],[48])). % 180.83/180.85 cnf(6324,plain, % 180.83/180.85 (P5(f8(f10(a1,a1)),f10(a2,a1))), % 180.83/180.85 inference(scs_inference,[],[48,4088,4094,1337,6138,4080,4092,4160,4002,4383,5094,6272,6140,6075,91,2,80,552,152,97,94,4295,565,605,673,17,111,22])). % 180.83/180.85 cnf(6327,plain, % 180.83/180.85 (~P13(f15(x63271),x63271)), % 180.83/180.85 inference(rename_variables,[],[4717])). % 180.83/180.85 cnf(6331,plain, % 180.83/180.85 (~E(x63311,f15(f15(x63311)))), % 180.83/180.85 inference(scs_inference,[],[48,71,4088,4704,4717,6327,480,4094,1337,6138,4080,4092,4160,4002,4383,5094,4147,6272,6140,6075,4781,91,2,80,552,152,97,94,4295,565,605,673,17,111,22,92,3,21,26])). % 180.83/180.85 cnf(6333,plain, % 180.83/180.85 (P16(f8(f16(a2)),a1)), % 180.83/180.85 inference(scs_inference,[],[48,6322,71,4088,4704,4717,6327,3765,480,4094,1337,6138,4080,4092,4160,4002,4383,5094,4147,6272,6140,6075,4781,91,2,80,552,152,97,94,4295,565,605,673,17,111,22,92,3,21,26,99])). % 180.83/180.85 cnf(6355,plain, % 180.83/180.85 (~P16(f15(f15(a5)),f12(a5))), % 180.83/180.85 inference(scs_inference,[],[169,6125,4240,6259,2,152,91,94])). % 180.83/180.85 cnf(6364,plain, % 180.83/180.85 (P5(f8(f9(a1,x63641)),f9(f8(f15(a1)),x63641))), % 180.83/180.85 inference(scs_inference,[],[169,6125,4004,4240,2494,2462,6259,6258,6192,2,152,91,94,552,4295,97,80,151])). % 180.83/180.85 cnf(6367,plain, % 180.83/180.85 (~E(x63671,f15(f15(x63671)))), % 180.83/180.85 inference(rename_variables,[],[6331])). % 180.83/180.85 cnf(6376,plain, % 180.83/180.85 (~P13(f15(f10(a2,f8(f15(a1)))),f10(a1,a1))), % 180.83/180.85 inference(scs_inference,[],[169,6125,511,4004,4240,2494,2462,6262,6331,6367,6259,6258,6192,2,152,91,94,552,4295,97,80,151,3943,4414,4104,100,5624,5751,5390,4455])). % 180.83/180.85 cnf(6391,plain, % 180.83/180.85 (~P13(f15(x63911),x63911)), % 180.83/180.85 inference(rename_variables,[],[4717])). % 180.83/180.85 cnf(6395,plain, % 180.83/180.85 (P16(f8(f15(x63951)),x63951)), % 180.83/180.85 inference(rename_variables,[],[118])). % 180.83/180.85 cnf(6397,plain, % 180.83/180.85 (P5(f8(x63971),x63971)), % 180.83/180.85 inference(rename_variables,[],[61])). % 180.83/180.85 cnf(6407,plain, % 180.83/180.85 (P9(f16(x64071))), % 180.83/180.85 inference(rename_variables,[],[48])). % 180.83/180.85 cnf(6410,plain, % 180.83/180.85 (~P13(f15(x64101),x64101)), % 180.83/180.85 inference(rename_variables,[],[4717])). % 180.83/180.85 cnf(6411,plain, % 180.83/180.86 (~P13(x64111,f8(f15(f13(x64112))))), % 180.83/180.86 inference(scs_inference,[],[48,169,126,121,43,6125,61,6397,4717,6391,3765,4193,118,6138,315,2446,511,4004,4240,1339,2494,2462,4988,6279,6333,6262,6331,6367,6259,6302,6258,4186,6192,2,152,91,94,552,4295,97,80,151,3943,4414,4104,100,5624,5751,5390,4455,5603,5742,5759,5640,5738,4564,5216,5192,3946,1217,3975,385,17,21,98,22,3,34,111,26,103])). % 180.83/180.86 cnf(6414,plain, % 180.83/180.86 (~P5(f15(f15(x64141)),f15(x64141))), % 180.83/180.86 inference(scs_inference,[],[48,169,126,121,70,43,6125,61,6397,4717,6391,6410,3765,4193,118,6138,315,2446,511,4004,4240,1339,2494,2462,4988,6279,6333,6262,6331,6367,6259,6302,6258,4186,6192,2,152,91,94,552,4295,97,80,151,3943,4414,4104,100,5624,5751,5390,4455,5603,5742,5759,5640,5738,4564,5216,5192,3946,1217,3975,385,17,21,98,22,3,34,111,26,103,92])). % 180.83/180.86 cnf(6428,plain, % 180.83/180.86 (P16(f8(f15(f13(a2))),a2)), % 180.83/180.86 inference(scs_inference,[],[219,48,169,126,121,70,43,6125,61,6397,4717,6391,6410,3765,4193,118,6395,6138,315,227,2446,511,4004,4240,4050,1339,2494,2462,4407,4988,6279,6333,6215,6262,6331,6367,6259,6302,6258,4186,4189,6192,4187,4188,4190,4191,4192,2,152,91,94,552,4295,97,80,151,3943,4414,4104,100,5624,5751,5390,4455,5603,5742,5759,5640,5738,4564,5216,5192,3946,1217,3975,385,17,21,98,22,3,34,111,26,103,92,32,33,31,28,16,29,95,30,104,18])). % 180.83/180.86 cnf(6431,plain, % 180.83/180.86 (P16(f8(f16(f6(f8(f15(a1))))),f6(a1))), % 180.83/180.86 inference(scs_inference,[],[219,48,6407,169,126,121,70,43,6125,61,6397,4717,6391,6410,3765,4193,118,6395,6138,315,227,2446,511,4004,4240,4050,1339,2494,2462,4407,1152,4988,6279,6333,6215,6262,6331,6367,6259,6302,6258,4186,4189,6192,4187,4188,4190,4191,4192,2,152,91,94,552,4295,97,80,151,3943,4414,4104,100,5624,5751,5390,4455,5603,5742,5759,5640,5738,4564,5216,5192,3946,1217,3975,385,17,21,98,22,3,34,111,26,103,92,32,33,31,28,16,29,95,30,104,18,19,99])). % 180.83/180.86 cnf(6459,plain, % 180.83/180.86 (~P16(f15(f15(x64591)),x64591)), % 180.83/180.86 inference(scs_inference,[],[6125,2414,6279,6215,6140,6241,6414,6224,2,152,552,91,385,97,151,94])). % 180.83/180.86 cnf(6479,plain, % 180.83/180.86 (~P13(f15(x64791),x64791)), % 180.83/180.86 inference(rename_variables,[],[4717])). % 180.83/180.86 cnf(6481,plain, % 180.83/180.86 (P9(f16(x64811))), % 180.83/180.86 inference(rename_variables,[],[48])). % 180.83/180.86 cnf(6486,plain, % 180.83/180.86 (P16(f8(f16(a2)),f8(f15(a1)))), % 180.83/180.86 inference(scs_inference,[],[48,187,189,6125,2414,4717,6479,66,6279,4452,4264,3109,4002,4286,6215,6333,6140,6241,6428,6324,6376,6411,6414,6355,6224,2,152,552,91,385,97,151,94,100,80,4295,653,21,17,3,98,22,26,111,92,18])). % 180.83/180.86 cnf(6487,plain, % 180.83/180.86 (P6(f7(f7(a5)))), % 180.83/180.86 inference(scs_inference,[],[48,187,189,6125,2414,4717,6479,66,6279,4452,4264,3109,4002,4050,4286,6215,6333,6140,6241,6428,6324,6234,6376,6411,6414,6355,6224,2,152,552,91,385,97,151,94,100,80,4295,653,21,17,3,98,22,26,111,92,18,95])). % 180.83/180.86 cnf(6491,plain, % 180.83/180.86 (P16(f8(f16(f8(f15(a2)))),a1)), % 180.83/180.86 inference(scs_inference,[],[48,6481,187,189,6125,2414,3765,4717,6479,66,6279,4452,4264,3109,4002,4050,4286,6215,4407,6333,6140,6241,6428,6324,6234,6376,6411,6414,6355,6224,2,152,552,91,385,97,151,94,100,80,4295,653,21,17,3,98,22,26,111,92,18,95,104,99])). % 180.83/180.86 cnf(6493,plain, % 180.83/180.86 (P9(f16(x64931))), % 180.83/180.86 inference(rename_variables,[],[48])). % 180.83/180.86 cnf(6495,plain, % 180.83/180.86 (P13(f6(a11),f16(f6(a11)))), % 180.83/180.86 inference(scs_inference,[],[48,6481,6493,187,60,189,6125,2414,3765,4717,6479,66,6279,4452,4264,3109,4002,3990,4050,4286,6215,4407,6333,6140,6241,6428,6324,6234,6376,6411,6414,6355,6224,2,152,552,91,385,97,151,94,100,80,4295,653,21,17,3,98,22,26,111,92,18,95,104,99,112])). % 180.83/180.86 cnf(6499,plain, % 180.83/180.86 (P5(f8(f15(f8(f15(a1)))),f15(x64991))), % 180.83/180.86 inference(scs_inference,[],[48,6481,6493,187,60,189,6125,2414,3765,4717,6479,66,6279,4452,4264,3109,4002,3990,4050,4286,6215,4407,6333,6140,6241,6428,6324,6234,6376,6411,6414,6355,6224,2,152,552,91,385,97,151,94,100,80,4295,653,21,17,3,98,22,26,111,92,18,95,104,99,112,3943])). % 180.83/180.86 cnf(6523,plain, % 180.83/180.86 (P5(f8(f13(f13(a2))),f13(f14(f13(a2))))), % 180.83/180.86 inference(scs_inference,[],[2414,4064,2,152])). % 180.83/180.86 cnf(6527,plain, % 180.83/180.86 (~E(f15(f15(x65271)),x65271)), % 180.83/180.86 inference(scs_inference,[],[2414,4064,6117,6118,6459,6095,2,152,552,385,151,80])). % 180.83/180.86 cnf(6533,plain, % 180.83/180.86 (~P16(f15(x65331),f8(f15(a2)))), % 180.83/180.86 inference(scs_inference,[],[2414,4064,6234,6259,6117,6118,6163,6459,6095,2,152,552,385,151,80,91,97,94])). % 180.83/180.86 cnf(6545,plain, % 180.83/180.86 (~P13(f15(x65451),x65451)), % 180.83/180.86 inference(rename_variables,[],[4717])). % 180.83/180.86 cnf(6555,plain, % 180.83/180.86 (P9(f16(x65551))), % 180.83/180.86 inference(rename_variables,[],[48])). % 180.83/180.86 cnf(6560,plain, % 180.83/180.86 (P16(f8(f16(f13(f13(a2)))),f13(f14(f13(a2))))), % 180.83/180.86 inference(scs_inference,[],[48,6555,2414,4064,3765,4717,6545,4096,904,4299,4095,4050,6088,4407,1963,6234,6414,6302,6171,4214,6259,6117,6118,6431,6486,6236,6364,6163,6459,6095,2,152,552,385,151,80,91,97,94,21,17,22,3,26,98,92,95,111,104,18,99])). % 180.83/180.86 cnf(6562,plain, % 180.83/180.86 (P9(f16(x65621))), % 180.83/180.86 inference(rename_variables,[],[48])). % 180.83/180.86 cnf(6564,plain, % 180.83/180.86 (P13(f7(a5),f16(f7(a5)))), % 180.83/180.86 inference(scs_inference,[],[48,6555,6562,60,2414,4064,3765,4717,6545,4096,904,4299,4095,4050,6088,4407,1963,6234,6414,6302,6171,4214,6259,6117,6118,6431,6486,6236,6364,6163,6459,6095,2,152,552,385,151,80,91,97,94,21,17,22,3,26,98,92,95,111,104,18,99,112])). % 180.83/180.86 cnf(6594,plain, % 180.83/180.86 (E(f13(x65941),a1)), % 180.83/180.86 inference(rename_variables,[],[4125])). % 180.83/180.86 cnf(6598,plain, % 180.83/180.86 (P16(f8(f16(f13(f13(a2)))),a1)), % 180.83/180.86 inference(scs_inference,[],[261,4717,64,6279,4094,4125,6594,6414,6215,6459,6236,4630,6163,6560,6523,6527,6277,6533,2,152,97,80,94,91,21,17,3,26,22,98,18])). % 180.83/180.86 cnf(6664,plain, % 180.83/180.86 (P5(f8(f10(x66641,a2)),f10(x66641,a1))), % 180.83/180.86 inference(scs_inference,[],[4087,4094,2,152])). % 180.83/180.86 cnf(6704,plain, % 180.83/180.86 (P5(f8(f14(a2)),f14(a1))), % 180.83/180.86 inference(scs_inference,[],[4086,2,152])). % 180.83/180.86 cnf(6713,plain, % 180.83/180.86 (P5(f8(f10(a2,a2)),f10(a1,a2))), % 180.83/180.86 inference(scs_inference,[],[4717,4086,4452,6459,5962,6086,4882,6084,6664,2,152,91,97,26,17,22])). % 180.83/180.86 cnf(6719,plain, % 180.83/180.86 (P16(f8(f16(f8(f15(a2)))),f8(f15(a1)))), % 180.83/180.86 inference(scs_inference,[],[187,4717,4087,61,4086,6414,4452,6459,5962,6527,6086,4882,6084,6491,6664,2,152,91,97,26,17,22,21,3,18])). % 180.83/180.86 cnf(6755,plain, % 180.83/180.86 (~P13(f15(x67551),x67551)), % 180.83/180.86 inference(rename_variables,[],[4717])). % 180.83/180.86 cnf(6766,plain, % 180.83/180.86 (P9(f16(x67661))), % 180.83/180.86 inference(rename_variables,[],[48])). % 180.83/180.86 cnf(6768,plain, % 180.83/180.86 (P13(f7(f7(a5)),f16(f7(f7(a5))))), % 180.83/180.86 inference(scs_inference,[],[48,6766,187,60,4717,6755,6414,4125,6459,4008,4095,3996,6527,1963,4441,6110,4633,6114,4783,6564,6719,6598,6704,6487,2,152,97,91,22,17,21,26,3,18,98,92,111,112])). % 180.83/180.86 cnf(6793,plain, % 180.83/180.86 (~P13(f15(x67931),x67931)), % 180.83/180.86 inference(rename_variables,[],[4717])). % 180.83/180.86 cnf(6806,plain, % 180.83/180.86 (E(f8(f16(f13(f13(a2)))),a1)), % 180.83/180.86 inference(scs_inference,[],[48,121,4088,4717,6793,4094,6414,4452,6459,4008,6527,4131,4398,4004,4550,6598,4121,4797,6495,6713,2,152,91,97,4884,4951,5014,4826,4763,4801,4350,17,26,21,22,3,92,111,98])). % 180.83/180.86 cnf(6821,plain, % 180.83/180.86 (E(f9(a1,x68211),f9(a2,x68211))), % 180.83/180.86 inference(scs_inference,[],[4095,2])). % 180.83/180.86 cnf(6888,plain, % 180.83/180.86 (E(f9(a1,a1),f9(a2,a2))), % 180.83/180.86 inference(scs_inference,[],[4282,2])). % 180.83/180.86 cnf(6918,plain, % 180.83/180.86 (P5(f8(f8(f15(a2))),a2)), % 180.83/180.86 inference(scs_inference,[],[480,152])). % 180.83/180.86 cnf(6963,plain, % 180.83/180.86 (~P13(f15(x69631),x69631)), % 180.83/180.86 inference(rename_variables,[],[4717])). % 180.83/180.86 cnf(6967,plain, % 180.83/180.86 (P9(f16(x69671))), % 180.83/180.86 inference(rename_variables,[],[48])). % 180.83/180.86 cnf(6972,plain, % 180.83/180.86 (P13(f8(f15(a4)),f16(f8(f15(a4))))), % 180.83/180.86 inference(scs_inference,[],[48,6967,60,4717,6963,239,6414,6459,6527,4093,4380,2462,4090,4052,4652,4076,6768,6918,6123,123,6499,2,152,97,91,552,17,22,3,26,21,111,92,112])). % 180.83/180.86 cnf(6991,plain, % 180.83/180.86 (P5(f8(f9(f8(f15(a1)),x69911)),f9(a1,x69911))), % 180.83/180.86 inference(scs_inference,[],[4085,2494,4158,2,152,91,151])). % 180.83/180.86 cnf(7001,plain, % 180.83/180.86 (~P13(f15(x70011),x70011)), % 180.83/180.86 inference(rename_variables,[],[4717])). % 180.83/180.86 cnf(7006,plain, % 180.83/180.86 (P9(f16(x70061))), % 180.83/180.86 inference(rename_variables,[],[48])). % 180.83/180.86 cnf(7008,plain, % 180.83/180.86 (P13(f7(f12(a11)),f16(f7(f12(a11))))), % 180.83/180.86 inference(scs_inference,[],[48,7006,60,4717,7001,6414,6459,6527,4085,4229,4214,6163,2494,6265,4654,4158,6972,6133,888,6217,2,152,91,151,17,22,21,3,26,92,111,112])). % 180.83/180.86 cnf(7031,plain, % 180.83/180.86 (P5(f8(f9(f8(f15(a1)),a2)),f9(a1,a1))), % 180.83/180.86 inference(scs_inference,[],[4096,6459,6527,290,6333,4383,6224,4575,6991,2,152,91,5098,5324,5114,5132,17,3,22])). % 180.83/180.86 cnf(7039,plain, % 180.83/180.86 (P9(f16(x70391))), % 180.83/180.86 inference(rename_variables,[],[48])). % 180.83/180.86 cnf(7041,plain, % 180.83/180.86 (P13(f8(f15(a3)),f16(f8(f15(a3))))), % 180.83/180.86 inference(scs_inference,[],[48,7039,60,4717,4096,6414,6459,6527,290,6333,4383,6224,6499,4721,4575,7008,6991,1360,2,152,91,5098,5324,5114,5132,17,3,22,21,26,111,112])). % 180.83/180.86 cnf(7043,plain, % 180.83/180.86 (P9(f16(x70431))), % 180.83/180.86 inference(rename_variables,[],[48])). % 180.83/180.86 cnf(7052,plain, % 180.83/180.86 (P16(f8(f16(a1)),a1)), % 180.83/180.86 inference(scs_inference,[],[48,7039,7043,60,4717,4096,6125,6414,3765,6459,6527,290,2494,6333,4383,6224,6499,4721,4575,7008,6991,1360,2,152,91,5098,5324,5114,5132,17,3,22,21,26,111,112,99,96,20,18])). % 180.83/180.86 cnf(7076,plain, % 180.83/180.86 (E(f8(f16(a1)),a1)), % 180.83/180.86 inference(scs_inference,[],[48,187,121,4717,6459,6527,4214,6224,5918,6095,3166,4755,6888,7041,7052,6309,7031,6219,2,152,91,22,17,21,3,26,18,111,98])). % 180.83/180.86 cnf(7241,plain, % 180.83/180.86 (~P13(f12(a3),f16(f14(x72411)))), % 180.83/180.86 inference(scs_inference,[],[48,239,6459,6527,322,4267,4089,4497,6240,4949,2,152,91,22,17,3,111])). % 180.83/180.86 cnf(7841,plain, % 180.83/180.86 (P13(f8(f16(a1)),f15(x78411))), % 180.83/180.86 inference(scs_inference,[],[6806,7076,152,2,5742,5759,3943,3975])). % 180.83/180.86 cnf(8407,plain, % 180.83/180.86 (P16(f16(x84071),f15(x84071))), % 180.83/180.86 inference(rename_variables,[],[64])). % 180.83/180.86 cnf(8421,plain, % 180.83/180.86 ($false), % 180.83/180.86 inference(scs_inference,[],[48,71,44,64,8407,6037,7241,6096,1108,7841,6312,6821,6888,239,1106,4717,5801,148,105,7,76,12,10,13,4,84,8,6,15,83,14,77,5,11,27,82,101,9,80,94,100,103,3975,96,112]), % 180.83/180.86 ['proof']). % 180.83/180.86 % SZS output end Proof % 180.83/180.86 % Total time :180.170000s %------------------------------------------------------------------------------