%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU046+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 : n019.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 15:00:55 EDT 2024 % Result : Theorem 117.92s 117.95s % Output : CNFRefutation 117.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU046+1 : TPTP v8.2.0. Released v3.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n019.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Jun 21 13:45:39 EDT 2024 % 0.12/0.34 % CPUTime : % 0.54/0.58 start to proof:theBenchmark % 117.92/117.93 %------------------------------------------- % 117.92/117.93 % File :CSE---1.7 % 117.92/117.93 % Problem :theBenchmark % 117.92/117.93 % Transform :cnf % 117.92/117.93 % Format :tptp:raw % 117.92/117.93 % Command :java -jar mcs_scs.jar %d %s % 117.92/117.93 % 117.92/117.93 % Result :Theorem 117.290000s % 117.92/117.93 % Output :CNFRefutation 117.290000s % 117.92/117.93 %------------------------------------------- % 117.92/117.94 %------------------------------------------------------------------------------ % 117.92/117.94 % File : SEU046+1 : TPTP v8.2.0. Released v3.2.0. % 117.92/117.94 % Domain : Set theory % 117.92/117.95 % Problem : Functions and their basic properties, theorem 89 % 117.92/117.95 % Version : [Urb06] axioms : Especial. % 117.92/117.95 % English : % 117.92/117.95 % 117.92/117.95 % Refs : [Byl90] Bylinski (1990), Functions and Their Basic Properties % 117.92/117.95 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 117.92/117.95 % Source : [Urb06] % 117.92/117.95 % Names : funct_1__t89_funct_1 [Urb06] % 117.92/117.95 % 117.92/117.95 % Status : Theorem % 117.92/117.95 % Rating : 0.33 v8.2.0, 0.36 v8.1.0, 0.28 v7.4.0, 0.27 v7.3.0, 0.24 v7.2.0, 0.21 v7.1.0, 0.22 v7.0.0, 0.27 v6.4.0, 0.31 v6.3.0, 0.25 v6.2.0, 0.36 v6.1.0, 0.53 v6.0.0, 0.48 v5.5.0, 0.52 v5.4.0, 0.54 v5.3.0, 0.52 v5.2.0, 0.35 v5.1.0, 0.43 v5.0.0, 0.50 v4.1.0, 0.48 v4.0.1, 0.43 v4.0.0, 0.42 v3.7.0, 0.35 v3.5.0, 0.37 v3.4.0, 0.47 v3.3.0, 0.43 v3.2.0 % 117.92/117.95 % Syntax : Number of formulae : 38 ( 6 unt; 0 def) % 117.92/117.95 % Number of atoms : 99 ( 4 equ) % 117.92/117.95 % Maximal formula atoms : 10 ( 2 avg) % 117.92/117.95 % Number of connectives : 75 ( 14 ~; 1 |; 35 &) % 117.92/117.95 % ( 4 <=>; 21 =>; 0 <=; 0 <~>) % 117.92/117.95 % Maximal formula depth : 11 ( 4 avg) % 117.92/117.95 % Maximal term depth : 3 ( 1 avg) % 117.92/117.95 % Number of predicates : 9 ( 8 usr; 0 prp; 1-2 aty) % 117.92/117.95 % Number of functors : 6 ( 6 usr; 1 con; 0-2 aty) % 117.92/117.95 % Number of variables : 59 ( 48 !; 11 ?) % 117.92/117.95 % SPC : FOF_THM_RFO_SEQ % 117.92/117.95 % 117.92/117.95 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 117.92/117.95 % library, www.mizar.org % 117.92/117.95 %------------------------------------------------------------------------------ % 117.92/117.95 fof(antisymmetry_r2_hidden,axiom, % 117.92/117.95 ! [A,B] : % 117.92/117.95 ( in(A,B) % 117.92/117.95 => ~ in(B,A) ) ). % 117.92/117.95 % 117.92/117.95 fof(cc1_funct_1,axiom, % 117.92/117.95 ! [A] : % 117.92/117.95 ( empty(A) % 117.92/117.95 => function(A) ) ). % 117.92/117.95 % 117.92/117.95 fof(cc1_relat_1,axiom, % 117.92/117.95 ! [A] : % 117.92/117.95 ( empty(A) % 117.92/117.95 => relation(A) ) ). % 117.92/117.95 % 117.92/117.95 fof(cc2_funct_1,axiom, % 117.92/117.95 ! [A] : % 117.92/117.95 ( ( relation(A) % 117.92/117.95 & empty(A) % 117.92/117.95 & function(A) ) % 117.92/117.95 => ( relation(A) % 117.92/117.95 & function(A) % 117.92/117.95 & one_to_one(A) ) ) ). % 117.92/117.95 % 117.92/117.95 fof(d3_tarski,axiom, % 117.92/117.95 ! [A,B] : % 117.92/117.95 ( subset(A,B) % 117.92/117.95 <=> ! [C] : % 117.92/117.95 ( in(C,A) % 117.92/117.95 => in(C,B) ) ) ). % 117.92/117.95 % 117.92/117.95 fof(dt_k8_relat_1,axiom, % 117.92/117.95 ! [A,B] : % 117.92/117.95 ( relation(B) % 117.92/117.95 => relation(relation_rng_restriction(A,B)) ) ). % 117.92/117.95 % 117.92/117.95 fof(existence_m1_subset_1,axiom, % 117.92/117.95 ! [A] : % 117.92/117.95 ? [B] : element(B,A) ). % 117.92/117.95 % 117.92/117.95 fof(fc12_relat_1,axiom, % 117.92/117.95 ( empty(empty_set) % 117.92/117.95 & relation(empty_set) % 117.92/117.95 & relation_empty_yielding(empty_set) ) ). % 117.92/117.95 % 117.92/117.95 fof(fc1_subset_1,axiom, % 117.92/117.95 ! [A] : ~ empty(powerset(A)) ). % 117.92/117.95 % 117.92/117.95 fof(fc1_xboole_0,axiom, % 117.92/117.95 empty(empty_set) ). % 117.92/117.95 % 117.92/117.95 fof(fc4_relat_1,axiom, % 117.92/117.95 ( empty(empty_set) % 117.92/117.95 & relation(empty_set) ) ). % 117.92/117.95 % 117.92/117.95 fof(fc5_funct_1,axiom, % 117.92/117.95 ! [A,B] : % 117.92/117.95 ( ( relation(B) % 117.92/117.95 & function(B) ) % 117.92/117.95 => ( relation(relation_rng_restriction(A,B)) % 117.92/117.95 & function(relation_rng_restriction(A,B)) ) ) ). % 117.92/117.95 % 117.92/117.95 fof(fc5_relat_1,axiom, % 117.92/117.95 ! [A] : % 117.92/117.95 ( ( ~ empty(A) % 117.92/117.95 & relation(A) ) % 117.92/117.95 => ~ empty(relation_dom(A)) ) ). % 117.92/117.95 % 117.92/117.95 fof(fc6_relat_1,axiom, % 117.92/117.95 ! [A] : % 117.92/117.95 ( ( ~ empty(A) % 117.92/117.95 & relation(A) ) % 117.92/117.95 => ~ empty(relation_rng(A)) ) ). % 117.92/117.95 % 117.92/117.95 fof(fc7_relat_1,axiom, % 117.92/117.95 ! [A] : % 117.92/117.95 ( empty(A) % 117.92/117.95 => ( empty(relation_dom(A)) % 117.92/117.95 & relation(relation_dom(A)) ) ) ). % 117.92/117.95 % 117.92/117.95 fof(fc8_relat_1,axiom, % 117.92/117.95 ! [A] : % 117.92/117.95 ( empty(A) % 117.92/117.95 => ( empty(relation_rng(A)) % 117.92/117.95 & relation(relation_rng(A)) ) ) ). % 117.92/117.95 % 117.92/117.95 fof(rc1_funct_1,axiom, % 117.92/117.95 ? [A] : % 117.92/117.95 ( relation(A) % 117.92/117.95 & function(A) ) ). % 117.92/117.95 % 117.92/117.95 fof(rc1_relat_1,axiom, % 117.92/117.95 ? [A] : % 117.92/117.95 ( empty(A) % 117.92/117.95 & relation(A) ) ). % 117.92/117.95 % 117.92/117.95 fof(rc1_subset_1,axiom, % 117.92/117.95 ! [A] : % 117.92/117.95 ( ~ empty(A) % 117.92/117.95 => ? [B] : % 117.92/117.95 ( element(B,powerset(A)) % 117.92/117.95 & ~ empty(B) ) ) ). % 117.92/117.95 % 117.92/117.95 fof(rc1_xboole_0,axiom, % 117.92/117.95 ? [A] : empty(A) ). % 117.92/117.95 % 117.92/117.95 fof(rc2_funct_1,axiom, % 117.92/117.95 ? [A] : % 117.92/117.95 ( relation(A) % 117.92/117.95 & empty(A) % 117.92/117.95 & function(A) ) ). % 117.92/117.95 % 117.92/117.95 fof(rc2_relat_1,axiom, % 117.92/117.95 ? [A] : % 117.92/117.95 ( ~ empty(A) % 117.92/117.95 & relation(A) ) ). % 117.92/117.95 % 117.92/117.95 fof(rc2_subset_1,axiom, % 117.92/117.95 ! [A] : % 117.92/117.95 ? [B] : % 117.92/117.95 ( element(B,powerset(A)) % 117.92/117.95 & empty(B) ) ). % 117.92/117.95 % 117.92/117.95 fof(rc2_xboole_0,axiom, % 117.92/117.95 ? [A] : ~ empty(A) ). % 117.92/117.95 % 117.92/117.95 fof(rc3_funct_1,axiom, % 117.92/117.95 ? [A] : % 117.92/117.95 ( relation(A) % 117.92/117.95 & function(A) % 117.92/117.95 & one_to_one(A) ) ). % 117.92/117.95 % 117.92/117.95 fof(rc3_relat_1,axiom, % 117.92/117.95 ? [A] : % 117.92/117.95 ( relation(A) % 117.92/117.95 & relation_empty_yielding(A) ) ). % 117.92/117.95 % 117.92/117.95 fof(reflexivity_r1_tarski,axiom, % 117.92/117.95 ! [A,B] : subset(A,A) ). % 117.92/117.95 % 117.92/117.95 fof(t118_relat_1,axiom, % 117.92/117.95 ! [A,B] : % 117.92/117.95 ( relation(B) % 117.92/117.95 => subset(relation_rng(relation_rng_restriction(A,B)),relation_rng(B)) ) ). % 117.92/117.95 % 117.92/117.95 fof(t1_subset,axiom, % 117.92/117.95 ! [A,B] : % 117.92/117.95 ( in(A,B) % 117.92/117.95 => element(A,B) ) ). % 117.92/117.95 % 117.92/117.95 fof(t2_subset,axiom, % 117.92/117.95 ! [A,B] : % 117.92/117.95 ( element(A,B) % 117.92/117.95 => ( empty(B) % 117.92/117.95 | in(A,B) ) ) ). % 117.92/117.95 % 117.92/117.95 fof(t3_subset,axiom, % 117.92/117.95 ! [A,B] : % 117.92/117.95 ( element(A,powerset(B)) % 117.92/117.95 <=> subset(A,B) ) ). % 117.92/117.95 % 117.92/117.95 fof(t4_subset,axiom, % 117.92/117.95 ! [A,B,C] : % 117.92/117.95 ( ( in(A,B) % 117.92/117.95 & element(B,powerset(C)) ) % 117.92/117.95 => element(A,C) ) ). % 117.92/117.95 % 117.92/117.95 fof(t5_subset,axiom, % 117.92/117.95 ! [A,B,C] : % 117.92/117.95 ~ ( in(A,B) % 117.92/117.95 & element(B,powerset(C)) % 117.92/117.95 & empty(C) ) ). % 117.92/117.95 % 117.92/117.95 fof(t6_boole,axiom, % 117.92/117.95 ! [A] : % 117.92/117.95 ( empty(A) % 117.92/117.95 => A = empty_set ) ). % 117.92/117.95 % 117.92/117.95 fof(t7_boole,axiom, % 117.92/117.95 ! [A,B] : % 117.92/117.95 ~ ( in(A,B) % 117.92/117.95 & empty(B) ) ). % 117.92/117.95 % 117.92/117.95 fof(t85_funct_1,axiom, % 117.92/117.95 ! [A,B] : % 117.92/117.95 ( ( relation(B) % 117.92/117.95 & function(B) ) % 117.92/117.95 => ! [C] : % 117.92/117.95 ( ( relation(C) % 117.92/117.95 & function(C) ) % 117.92/117.95 => ( B = relation_rng_restriction(A,C) % 117.92/117.95 <=> ( ! [D] : % 117.92/117.95 ( in(D,relation_dom(B)) % 117.92/117.95 <=> ( in(D,relation_dom(C)) % 117.92/117.95 & in(apply(C,D),A) ) ) % 117.92/117.95 & ! [D] : % 117.92/117.95 ( in(D,relation_dom(B)) % 117.92/117.95 => apply(B,D) = apply(C,D) ) ) ) ) ) ). % 117.92/117.95 % 117.92/117.95 fof(t89_funct_1,conjecture, % 117.92/117.95 ! [A,B] : % 117.92/117.95 ( ( relation(B) % 117.92/117.95 & function(B) ) % 117.92/117.95 => ( subset(relation_dom(relation_rng_restriction(A,B)),relation_dom(B)) % 117.92/117.95 & subset(relation_rng(relation_rng_restriction(A,B)),relation_rng(B)) ) ) ). % 117.92/117.95 % 117.92/117.95 fof(t8_boole,axiom, % 117.92/117.95 ! [A,B] : % 117.92/117.95 ~ ( empty(A) % 117.92/117.95 & A != B % 117.92/117.95 & empty(B) ) ). % 117.92/117.95 % 117.92/117.95 %------------------------------------------------------------------------------ % 117.92/117.95 %------------------------------------------- % 117.92/117.95 % Proof found % 117.92/117.95 % SZS status Theorem for theBenchmark % 117.92/117.95 % SZS output start Proof % 117.92/117.96 %ClaNum:100(EqnAxiom:32) % 117.92/117.96 %VarNum:291(SingletonVarNum:84) % 117.92/117.96 %MaxLitNum:9 % 117.92/117.96 %MaxfuncDepth:2 % 117.92/117.96 %SharedTerms:39 % 117.92/117.96 %goalClause: 42 51 94 % 117.92/117.96 %singleGoalClaCount:2 % 117.92/117.96 [35]P1(a1) % 117.92/117.96 [36]P1(a3) % 117.92/117.96 [37]P1(a14) % 117.92/117.96 [38]P1(a16) % 117.92/117.96 [39]P3(a4) % 117.92/117.96 [40]P3(a16) % 117.92/117.96 [41]P3(a5) % 117.92/117.96 [42]P3(a7) % 117.92/117.96 [44]P4(a1) % 117.92/117.96 [45]P4(a4) % 117.92/117.96 [46]P4(a3) % 117.92/117.96 [47]P4(a16) % 117.92/117.96 [48]P4(a17) % 117.92/117.96 [49]P4(a5) % 117.92/117.96 [50]P4(a8) % 117.92/117.96 [51]P4(a7) % 117.92/117.96 [52]P5(a5) % 117.92/117.96 [53]P7(a1) % 117.92/117.96 [54]P7(a8) % 117.92/117.96 [59]~P1(a17) % 117.92/117.96 [60]~P1(a6) % 117.92/117.96 [56]P8(x561,x561) % 117.92/117.96 [55]P1(f18(x551)) % 117.92/117.96 [57]P2(f12(x571),x571) % 117.92/117.96 [58]P2(f18(x581),f19(x581)) % 117.92/117.96 [61]~P1(f19(x611)) % 117.92/117.96 [94]~P8(f21(f22(a9,a7)),f21(a7))+~P8(f20(f22(a9,a7)),f20(a7)) % 117.92/117.96 [62]~P1(x621)+E(x621,a1) % 117.92/117.96 [63]~P1(x631)+P3(x631) % 117.92/117.96 [64]~P1(x641)+P4(x641) % 117.92/117.96 [66]~P1(x661)+P1(f20(x661)) % 117.92/117.96 [67]~P1(x671)+P1(f21(x671)) % 117.92/117.96 [68]~P1(x681)+P4(f20(x681)) % 117.92/117.96 [69]~P1(x691)+P4(f21(x691)) % 117.92/117.96 [70]P1(x701)+~P1(f15(x701)) % 117.92/117.96 [75]P1(x751)+P2(f15(x751),f19(x751)) % 117.92/117.96 [74]~P1(x741)+~P6(x742,x741) % 117.92/117.96 [76]~P6(x761,x762)+P2(x761,x762) % 117.92/117.96 [82]~P6(x822,x821)+~P6(x821,x822) % 117.92/117.96 [77]~P4(x772)+P4(f22(x771,x772)) % 117.92/117.96 [79]~P8(x791,x792)+P2(x791,f19(x792)) % 117.92/117.96 [83]P8(x831,x832)+~P2(x831,f19(x832)) % 117.92/117.96 [84]P8(x841,x842)+P6(f13(x841,x842),x841) % 117.92/117.96 [88]P8(x881,x882)+~P6(f13(x881,x882),x882) % 117.92/117.96 [89]~P4(x892)+P8(f21(f22(x891,x892)),f21(x892)) % 117.92/117.96 [72]~P4(x721)+P1(x721)+~P1(f20(x721)) % 117.92/117.96 [73]~P4(x731)+P1(x731)+~P1(f21(x731)) % 117.92/117.96 [65]~P1(x652)+~P1(x651)+E(x651,x652) % 117.92/117.96 [78]~P2(x782,x781)+P1(x781)+P6(x782,x781) % 117.92/117.96 [80]~P3(x802)+~P4(x802)+P3(f22(x801,x802)) % 117.92/117.96 [85]~P8(x853,x852)+P6(x851,x852)+~P6(x851,x853) % 117.92/117.96 [86]~P1(x861)+~P6(x862,x863)+~P2(x863,f19(x861)) % 117.92/117.96 [87]P2(x871,x872)+~P6(x871,x873)+~P2(x873,f19(x872)) % 117.92/117.96 [71]~P1(x711)+~P3(x711)+~P4(x711)+P5(x711) % 117.92/117.96 [90]~P3(x903)+~P3(x902)+~P4(x903)+~P4(x902)+~P6(x901,f20(x903))+P6(x901,f20(x902))+~E(x903,f22(x904,x902)) % 117.92/117.96 [91]~P3(x913)+~P3(x911)+~P4(x913)+~P4(x911)+~P6(x912,f20(x911))+E(f2(x911,x912),f2(x913,x912))+~E(x911,f22(x914,x913)) % 117.92/117.96 [92]~P3(x924)+~P3(x921)+~P4(x924)+~P4(x921)+~P6(x922,f20(x924))+P6(f2(x921,x922),x923)+~E(x924,f22(x923,x921)) % 117.92/117.96 [95]~P3(x953)+~P3(x951)+~P4(x953)+~P4(x951)+P6(f10(x952,x951,x953),f20(x953))+P6(f10(x952,x951,x953),f20(x951))+P6(f11(x952,x951,x953),f20(x951))+E(x951,f22(x952,x953)) % 117.92/117.96 [96]~P3(x963)+~P3(x961)+~P4(x963)+~P4(x961)+P6(f10(x962,x961,x963),f20(x961))+P6(f11(x962,x961,x963),f20(x961))+E(x961,f22(x962,x963))+P6(f2(x963,f10(x962,x961,x963)),x962) % 117.92/117.96 [97]~P3(x973)+~P3(x971)+~P4(x973)+~P4(x971)+P6(f10(x972,x971,x973),f20(x973))+P6(f10(x972,x971,x973),f20(x971))+E(x971,f22(x972,x973))+~E(f2(x971,f11(x972,x971,x973)),f2(x973,f11(x972,x971,x973))) % 117.92/117.96 [98]~P3(x983)+~P3(x981)+~P4(x983)+~P4(x981)+P6(f10(x982,x981,x983),f20(x981))+E(x981,f22(x982,x983))+P6(f2(x983,f10(x982,x981,x983)),x982)+~E(f2(x981,f11(x982,x981,x983)),f2(x983,f11(x982,x981,x983))) % 117.92/117.96 [93]~P3(x932)+~P3(x934)+~P4(x932)+~P4(x934)+~P6(x931,f20(x934))+~P6(f2(x934,x931),x933)+P6(x931,f20(x932))+~E(x932,f22(x933,x934)) % 117.92/117.96 [99]~P3(x993)+~P3(x991)+~P4(x993)+~P4(x991)+P6(f11(x992,x991,x993),f20(x991))+~P6(f10(x992,x991,x993),f20(x993))+~P6(f10(x992,x991,x993),f20(x991))+E(x991,f22(x992,x993))+~P6(f2(x993,f10(x992,x991,x993)),x992) % 117.92/117.96 [100]~P3(x1003)+~P3(x1001)+~P4(x1003)+~P4(x1001)+~P6(f10(x1002,x1001,x1003),f20(x1003))+~P6(f10(x1002,x1001,x1003),f20(x1001))+E(x1001,f22(x1002,x1003))+~E(f2(x1001,f11(x1002,x1001,x1003)),f2(x1003,f11(x1002,x1001,x1003)))+~P6(f2(x1003,f10(x1002,x1001,x1003)),x1002) % 117.92/117.96 %EqnAxiom % 117.92/117.96 [1]E(x11,x11) % 117.92/117.96 [2]E(x22,x21)+~E(x21,x22) % 117.92/117.96 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 117.92/117.96 [4]~E(x41,x42)+E(f18(x41),f18(x42)) % 117.92/117.96 [5]~E(x51,x52)+E(f12(x51),f12(x52)) % 117.92/117.96 [6]~E(x61,x62)+E(f2(x61,x63),f2(x62,x63)) % 117.92/117.96 [7]~E(x71,x72)+E(f2(x73,x71),f2(x73,x72)) % 117.92/117.96 [8]~E(x81,x82)+E(f19(x81),f19(x82)) % 117.92/117.96 [9]~E(x91,x92)+E(f10(x91,x93,x94),f10(x92,x93,x94)) % 117.92/117.96 [10]~E(x101,x102)+E(f10(x103,x101,x104),f10(x103,x102,x104)) % 117.92/117.96 [11]~E(x111,x112)+E(f10(x113,x114,x111),f10(x113,x114,x112)) % 117.92/117.96 [12]~E(x121,x122)+E(f20(x121),f20(x122)) % 117.92/117.96 [13]~E(x131,x132)+E(f21(x131),f21(x132)) % 117.92/117.96 [14]~E(x141,x142)+E(f11(x141,x143,x144),f11(x142,x143,x144)) % 117.92/117.96 [15]~E(x151,x152)+E(f11(x153,x151,x154),f11(x153,x152,x154)) % 117.92/117.96 [16]~E(x161,x162)+E(f11(x163,x164,x161),f11(x163,x164,x162)) % 117.92/117.96 [17]~E(x171,x172)+E(f22(x171,x173),f22(x172,x173)) % 117.92/117.96 [18]~E(x181,x182)+E(f22(x183,x181),f22(x183,x182)) % 117.92/117.96 [19]~E(x191,x192)+E(f15(x191),f15(x192)) % 117.92/117.96 [20]~E(x201,x202)+E(f13(x201,x203),f13(x202,x203)) % 117.92/117.96 [21]~E(x211,x212)+E(f13(x213,x211),f13(x213,x212)) % 117.92/117.96 [22]~P1(x221)+P1(x222)+~E(x221,x222) % 117.92/117.96 [23]P6(x232,x233)+~E(x231,x232)+~P6(x231,x233) % 117.92/117.96 [24]P6(x243,x242)+~E(x241,x242)+~P6(x243,x241) % 117.92/117.96 [25]~P4(x251)+P4(x252)+~E(x251,x252) % 117.92/117.96 [26]~P3(x261)+P3(x262)+~E(x261,x262) % 117.92/117.96 [27]P8(x272,x273)+~E(x271,x272)+~P8(x271,x273) % 117.92/117.96 [28]P8(x283,x282)+~E(x281,x282)+~P8(x283,x281) % 117.92/117.96 [29]P2(x292,x293)+~E(x291,x292)+~P2(x291,x293) % 117.92/117.96 [30]P2(x303,x302)+~E(x301,x302)+~P2(x303,x301) % 117.92/117.96 [31]~P5(x311)+P5(x312)+~E(x311,x312) % 117.92/117.96 [32]~P7(x321)+P7(x322)+~E(x321,x322) % 117.92/117.96 % 117.92/117.96 %------------------------------------------- % 117.92/117.98 cnf(101,plain, % 117.92/117.98 (~P4(f22(x1011,x1012))+~P4(x1012)+~P3(f22(x1011,x1012))+~P3(x1012)+P6(x1013,f20(x1012))+~P6(x1013,f20(f22(x1011,x1012)))), % 117.92/117.98 inference(equality_inference,[],[90])). % 117.92/117.98 cnf(103,plain, % 117.92/117.98 (~P4(f22(x1031,x1032))+~P4(x1032)+~P3(f22(x1031,x1032))+~P3(x1032)+P6(f2(x1032,x1033),x1031)+~P6(x1033,f20(f22(x1031,x1032)))), % 117.92/117.98 inference(equality_inference,[],[92])). % 117.92/117.98 cnf(105,plain, % 117.92/117.98 (~P4(x1051)+~P4(x1051)+~P3(x1051)+~P3(x1051)+E(x1051,f22(x1052,x1051))+P6(f10(x1052,x1051,x1051),f20(x1051))+P6(f10(x1052,x1051,x1051),f20(x1051))), % 117.92/117.98 inference(equality_inference,[],[97])). % 117.92/117.98 cnf(108,plain, % 117.92/117.98 (P8(f12(f19(x1081)),x1081)), % 117.92/117.98 inference(scs_inference,[],[57,83])). % 117.92/117.98 cnf(109,plain, % 117.92/117.98 (P2(f12(x1091),x1091)), % 117.92/117.98 inference(rename_variables,[],[57])). % 117.92/117.98 cnf(111,plain, % 117.92/117.98 (~P6(x1111,a1)), % 117.92/117.98 inference(scs_inference,[],[35,57,83,74])). % 117.92/117.98 cnf(113,plain, % 117.92/117.98 (P6(f12(a17),a17)), % 117.92/117.98 inference(scs_inference,[],[35,57,109,59,83,74,78])). % 117.92/117.98 cnf(114,plain, % 117.92/117.98 (P2(f12(x1141),x1141)), % 117.92/117.98 inference(rename_variables,[],[57])). % 117.92/117.98 cnf(116,plain, % 117.92/117.98 (~P6(x1161,f12(f19(a1)))), % 117.92/117.98 inference(scs_inference,[],[35,57,109,114,59,83,74,78,86])). % 117.92/117.98 cnf(119,plain, % 117.92/117.98 (~E(a17,a1)), % 117.92/117.98 inference(scs_inference,[],[35,57,109,114,59,83,74,78,86,24])). % 117.92/117.98 cnf(120,plain, % 117.92/117.98 (P5(a16)), % 117.92/117.98 inference(scs_inference,[],[35,38,40,47,57,109,114,59,83,74,78,86,24,71])). % 117.92/117.98 cnf(122,plain, % 117.92/117.98 (P8(f12(f19(a1)),x1221)), % 117.92/117.98 inference(scs_inference,[],[35,38,40,47,57,109,114,59,83,74,78,86,24,71,84])). % 117.92/117.98 cnf(126,plain, % 117.92/117.98 (P8(x1261,x1262)+~E(x1262,x1261)), % 117.92/117.98 inference(scs_inference,[],[35,38,40,47,56,57,109,114,59,83,74,78,86,24,71,84,82,27])). % 117.92/117.98 cnf(133,plain, % 117.92/117.98 (~P6(x1331,a3)), % 117.92/117.98 inference(scs_inference,[],[36,74])). % 117.92/117.98 cnf(135,plain, % 117.92/117.98 (P8(f18(x1351),x1351)), % 117.92/117.98 inference(scs_inference,[],[36,58,74,83])). % 117.92/117.98 cnf(137,plain, % 117.92/117.98 (P8(a1,x1371)), % 117.92/117.98 inference(scs_inference,[],[111,36,58,74,83,84])). % 117.92/117.98 cnf(140,plain, % 117.92/117.98 (~P6(x1401,f18(a3))), % 117.92/117.98 inference(scs_inference,[],[111,36,58,74,83,84,86])). % 117.92/117.98 cnf(141,plain, % 117.92/117.98 (P2(f18(x1411),f19(x1411))), % 117.92/117.98 inference(rename_variables,[],[58])). % 117.92/117.98 cnf(143,plain, % 117.92/117.98 (P6(f12(a6),a6)), % 117.92/117.98 inference(scs_inference,[],[111,36,58,60,57,74,83,84,86,78])). % 117.92/117.98 cnf(155,plain, % 117.92/117.98 (P8(f12(f19(x1551)),x1552)+~E(x1551,x1552)), % 117.92/117.98 inference(scs_inference,[],[108,116,111,113,36,58,141,60,57,74,83,84,86,78,24,82,87,30,23,27,28])). % 117.92/117.98 cnf(156,plain, % 117.92/117.98 (P2(x1561,f19(x1562))+~E(f18(x1562),x1561)), % 117.92/117.98 inference(scs_inference,[],[108,116,111,113,36,58,141,60,57,74,83,84,86,78,24,82,87,30,23,27,28,29])). % 117.92/117.98 cnf(162,plain, % 117.92/117.98 (~P6(x1621,a14)), % 117.92/117.98 inference(scs_inference,[],[37,74])). % 117.92/117.98 cnf(167,plain, % 117.92/117.98 (~P6(x1671,f12(f19(a14)))), % 117.92/117.98 inference(scs_inference,[],[140,37,57,74,84,86])). % 117.92/117.98 cnf(168,plain, % 117.92/117.98 (P2(f12(x1681),x1681)), % 117.92/117.98 inference(rename_variables,[],[57])). % 117.92/117.98 cnf(170,plain, % 117.92/117.98 (P6(f12(f19(x1701)),f19(x1701))), % 117.92/117.98 inference(scs_inference,[],[140,37,61,57,168,74,84,86,78])). % 117.92/117.98 cnf(184,plain, % 117.92/117.98 (~P6(x1841,f18(x1842))), % 117.92/117.98 inference(scs_inference,[],[55,74])). % 117.92/117.98 cnf(186,plain, % 117.92/117.98 (P8(f12(f19(a14)),x1861)), % 117.92/117.98 inference(scs_inference,[],[167,55,74,84])). % 117.92/117.98 cnf(187,plain, % 117.92/117.98 (~P6(x1871,f12(f19(a14)))), % 117.92/117.98 inference(rename_variables,[],[167])). % 117.92/117.98 cnf(189,plain, % 117.92/117.98 (~P6(x1891,f12(f19(f18(x1892))))), % 117.92/117.98 inference(scs_inference,[],[167,55,57,74,84,86])). % 117.92/117.98 cnf(190,plain, % 117.92/117.98 (P2(f12(x1901),x1901)), % 117.92/117.98 inference(rename_variables,[],[57])). % 117.92/117.98 cnf(192,plain, % 117.92/117.98 (P6(f18(x1921),f19(x1921))), % 117.92/117.98 inference(scs_inference,[],[167,55,58,61,57,74,84,86,78])). % 117.92/117.98 cnf(198,plain, % 117.92/117.98 (P2(f12(x1981),x1982)+~E(x1981,x1982)), % 117.92/117.98 inference(scs_inference,[],[135,170,167,187,55,58,61,57,190,74,84,86,78,24,28,30])). % 117.92/117.98 cnf(199,plain, % 117.92/117.98 (P8(x1991,x1992)+~E(f12(f19(a1)),x1991)), % 117.92/117.98 inference(scs_inference,[],[122,135,170,167,187,55,58,61,57,190,74,84,86,78,24,28,30,27])). % 117.92/117.98 cnf(201,plain, % 117.92/117.98 (P2(x2011,x2012)+~E(f12(x2012),x2011)), % 117.92/117.98 inference(scs_inference,[],[122,135,170,167,187,55,58,61,57,190,74,84,86,78,24,28,30,27,23,29])). % 117.92/117.98 cnf(209,plain, % 117.92/117.98 (~P6(x2091,a16)), % 117.92/117.98 inference(scs_inference,[],[38,74])). % 117.92/117.98 cnf(212,plain, % 117.92/117.98 (~P6(x2121,f18(x2122))), % 117.92/117.98 inference(rename_variables,[],[184])). % 117.92/117.98 cnf(214,plain, % 117.92/117.98 (~P6(x2141,f12(f19(a16)))), % 117.92/117.98 inference(scs_inference,[],[184,38,57,74,84,86])). % 117.92/117.98 cnf(219,plain, % 117.92/117.98 (P8(x2191,x2192)+~E(x2191,x2192)), % 117.92/117.98 inference(scs_inference,[],[170,184,212,38,56,57,74,84,86,24,28])). % 117.92/117.98 cnf(229,plain, % 117.92/117.98 (P8(f12(f19(a16)),x2291)), % 117.92/117.98 inference(scs_inference,[],[214,84])). % 117.92/117.98 cnf(234,plain, % 117.92/117.98 (P8(x2341,x2342)+~E(a1,x2341)), % 117.92/117.98 inference(scs_inference,[],[137,113,189,214,84,24,27])). % 117.92/117.98 cnf(243,plain, % 117.92/117.98 (P8(a3,x2431)), % 117.92/117.98 inference(scs_inference,[],[133,84])). % 117.92/117.98 cnf(244,plain, % 117.92/117.98 (~P6(x2441,a3)), % 117.92/117.98 inference(rename_variables,[],[133])). % 117.92/117.98 cnf(246,plain, % 117.92/117.98 (~P6(x2461,f12(f19(a3)))), % 117.92/117.98 inference(scs_inference,[],[36,133,57,84,86])). % 117.92/117.98 cnf(252,plain, % 117.92/117.98 (P8(x2521,a6)+~E(f12(a6),f13(x2521,a6))), % 117.92/117.98 inference(scs_inference,[],[143,36,133,244,57,84,86,24,23,88])). % 117.92/117.98 cnf(259,plain, % 117.92/117.98 (P8(f12(f19(a3)),x2591)), % 117.92/117.98 inference(scs_inference,[],[246,84])). % 117.92/117.98 cnf(260,plain, % 117.92/117.98 (~P6(x2601,f12(f19(a3)))), % 117.92/117.98 inference(rename_variables,[],[246])). % 117.92/117.98 cnf(264,plain, % 117.92/117.98 (P8(x2641,x2642)+~E(f12(f19(a14)),x2641)), % 117.92/117.98 inference(scs_inference,[],[186,113,246,260,84,24,27])). % 117.92/117.98 cnf(272,plain, % 117.92/117.98 (P8(a14,x2721)), % 117.92/117.98 inference(scs_inference,[],[162,84])). % 117.92/117.98 cnf(284,plain, % 117.92/117.98 (P8(a16,x2841)), % 117.92/117.98 inference(scs_inference,[],[209,84])). % 117.92/117.98 cnf(285,plain, % 117.92/117.98 (~P6(x2851,a16)), % 117.92/117.98 inference(rename_variables,[],[209])). % 117.92/117.98 cnf(287,plain, % 117.92/117.98 (~E(f19(x2871),a16)), % 117.92/117.98 inference(scs_inference,[],[170,209,285,84,24])). % 117.92/117.98 cnf(289,plain, % 117.92/117.98 (P8(x2891,x2892)+~E(f12(f19(a16)),x2891)), % 117.92/117.98 inference(scs_inference,[],[229,170,209,285,84,24,27])). % 117.92/117.98 cnf(300,plain, % 117.92/117.98 (P6(x3001,f19(x3002))+~E(f18(x3002),x3001)), % 117.92/117.98 inference(scs_inference,[],[113,192,184,24,23])). % 117.92/117.98 cnf(311,plain, % 117.92/117.98 (P8(x3111,x3112)+~E(f12(f19(a3)),x3111)), % 117.92/117.98 inference(scs_inference,[],[259,143,116,24,27])). % 117.92/117.98 cnf(322,plain, % 117.92/117.98 (P8(x3221,x3222)+~E(a3,x3221)), % 117.92/117.98 inference(scs_inference,[],[243,113,167,24,27])). % 117.92/117.98 cnf(331,plain, % 117.92/117.98 (P8(x3311,x3312)+~E(a14,x3311)), % 117.92/117.98 inference(scs_inference,[],[272,113,214,24,27])). % 117.92/117.98 cnf(343,plain, % 117.92/117.98 (P8(x3431,x3432)+~E(a16,x3431)), % 117.92/117.98 inference(scs_inference,[],[284,170,246,24,27])). % 117.92/117.98 cnf(359,plain, % 117.92/117.98 (P3(f22(x3591,a3))), % 117.92/117.98 inference(scs_inference,[],[36,46,63,80])). % 117.92/117.98 cnf(380,plain, % 117.92/117.98 (P6(f10(x3801,a16,a16),f20(a16))+E(a16,f22(x3801,a16))), % 117.92/117.98 inference(scs_inference,[],[113,40,209,47,24,105])). % 117.92/117.98 cnf(432,plain, % 117.92/117.98 (P4(f22(x4321,f18(x4322)))), % 117.92/117.98 inference(scs_inference,[],[55,64,77])). % 117.92/117.98 cnf(500,plain, % 117.92/117.98 (E(f20(a1),a1)), % 117.92/117.98 inference(scs_inference,[],[35,62,66])). % 117.92/117.98 cnf(504,plain, % 117.92/117.98 (E(a1,f20(a1))), % 117.92/117.98 inference(scs_inference,[],[500,155,219,198,2])). % 117.92/117.98 cnf(505,plain, % 117.92/117.98 (P4(f20(a1))), % 117.92/117.98 inference(scs_inference,[],[44,500,155,219,198,2,25])). % 117.92/117.98 cnf(507,plain, % 117.92/117.98 (P1(f20(a1))), % 117.92/117.98 inference(scs_inference,[],[119,35,44,500,155,219,198,2,25,3,22])). % 117.92/117.98 cnf(508,plain, % 117.92/117.98 (P7(f20(a1))), % 117.92/117.98 inference(scs_inference,[],[119,35,44,500,53,155,219,198,2,25,3,22,32])). % 117.92/117.98 cnf(510,plain, % 117.92/117.98 (~P6(x5101,f20(a1))), % 117.92/117.98 inference(scs_inference,[],[137,119,35,44,500,53,155,219,198,2,25,3,22,32,27,74])). % 117.92/117.98 cnf(512,plain, % 117.92/117.98 (~P3(f20(a1))+P3(a1)), % 117.92/117.98 inference(scs_inference,[],[137,119,35,44,500,53,155,219,198,2,25,3,22,32,27,74,26])). % 117.92/117.98 cnf(518,plain, % 117.92/117.98 (~P3(a1)+P3(f20(a1))), % 117.92/117.98 inference(scs_inference,[],[504,198,26])). % 117.92/117.98 cnf(519,plain, % 117.92/117.98 (P3(f20(a1))+~P3(f20(a1))), % 117.92/117.98 inference(scs_inference,[],[504,198,26,512])). % 117.92/117.98 cnf(524,plain, % 117.92/117.98 (~P5(a1)+P5(f20(a1))), % 117.92/117.98 inference(scs_inference,[],[504,31])). % 117.92/117.98 cnf(550,plain, % 117.92/117.98 (P1(f21(f20(a3)))), % 117.92/117.98 inference(scs_inference,[],[36,67,66])). % 117.92/117.98 cnf(551,plain, % 117.92/117.98 (~P6(x5511,f21(f20(a3)))), % 117.92/117.98 inference(scs_inference,[],[550,74])). % 117.92/117.98 cnf(555,plain, % 117.92/117.98 (P1(f20(a3))+~P4(f20(a3))), % 117.92/117.98 inference(scs_inference,[],[550,74,84,73])). % 117.92/117.98 cnf(557,plain, % 117.92/117.98 (P8(x5571,x5572)+~E(f21(f20(a3)),x5571)), % 117.92/117.98 inference(scs_inference,[],[550,74,84,73,27])). % 117.92/117.98 cnf(620,plain, % 117.92/117.98 (~P1(f15(a17))), % 117.92/117.98 inference(scs_inference,[],[113,70,74])). % 117.92/117.98 cnf(621,plain, % 117.92/117.98 (P6(f12(f15(a17)),f15(a17))), % 117.92/117.98 inference(scs_inference,[],[620,57,78])). % 117.92/117.98 cnf(624,plain, % 117.92/117.98 (~E(f15(a17),f12(f19(a1)))), % 117.92/117.98 inference(scs_inference,[],[116,620,57,78,24])). % 117.92/117.98 cnf(796,plain, % 117.92/117.98 (~P6(x7961,f12(f19(f20(a3))))+~P4(f20(a3))), % 117.92/117.98 inference(scs_inference,[],[57,555,86])). % 117.92/117.98 cnf(817,plain, % 117.92/117.98 (P2(f15(a17),f19(a17))), % 117.92/117.98 inference(scs_inference,[],[119,75,62])). % 117.92/117.98 cnf(818,plain, % 117.92/117.98 (P8(f15(a17),a17)), % 117.92/117.98 inference(scs_inference,[],[817,83])). % 117.92/117.98 cnf(825,plain, % 117.92/117.98 (~P6(f19(a17),f15(a17))), % 117.92/117.98 inference(scs_inference,[],[621,817,61,83,78,87,82])). % 117.92/117.98 cnf(827,plain, % 117.92/117.98 (~E(f12(f15(a17)),f19(a17))), % 117.92/117.98 inference(scs_inference,[],[621,817,61,83,78,87,82,23])). % 117.92/117.98 cnf(838,plain, % 117.92/117.98 (P6(f12(f15(a17)),a17)), % 117.92/117.98 inference(scs_inference,[],[818,621,85])). % 117.92/117.98 cnf(840,plain, % 117.92/117.98 (~P2(f19(a17),f15(a17))), % 117.92/117.98 inference(scs_inference,[],[818,621,825,620,85,78])). % 117.92/117.98 cnf(885,plain, % 117.92/117.98 (P2(f12(f19(a14)),f19(x8851))), % 117.92/117.98 inference(scs_inference,[],[167,79,84])). % 117.92/117.98 cnf(891,plain, % 117.92/117.98 (P2(x8911,f19(x8912))+~E(f12(f19(a14)),x8911)), % 117.92/117.98 inference(scs_inference,[],[885,29])). % 117.92/117.98 cnf(912,plain, % 117.92/117.98 (E(f18(f20(a1)),f18(a1))), % 117.92/117.98 inference(scs_inference,[],[504,4,2])). % 117.92/117.98 cnf(913,plain, % 117.92/117.98 (P2(f18(a1),f19(f20(a1)))), % 117.92/117.98 inference(scs_inference,[],[912,156])). % 117.92/117.98 cnf(914,plain, % 117.92/117.98 (P6(f18(a1),f19(f20(a1)))), % 117.92/117.98 inference(scs_inference,[],[912,156,300])). % 117.92/117.98 cnf(915,plain, % 117.92/117.98 (E(f18(a1),f18(f20(a1)))), % 117.92/117.98 inference(scs_inference,[],[912,156,300,2])). % 117.92/117.98 cnf(921,plain, % 117.92/117.98 (P2(f18(f20(a1)),f19(a1))), % 117.92/117.98 inference(scs_inference,[],[915,156])). % 117.92/117.98 cnf(922,plain, % 117.92/117.98 (P6(f18(f20(a1)),f19(a1))), % 117.92/117.98 inference(scs_inference,[],[915,156,300])). % 117.92/117.98 cnf(923,plain, % 117.92/117.98 (P2(f12(f18(a1)),f18(f20(a1)))), % 117.92/117.98 inference(scs_inference,[],[915,156,300,198])). % 117.92/117.98 cnf(941,plain, % 117.92/117.98 (~E(f18(f20(a1)),f19(a17))+~E(f19(a1),f15(a17))), % 117.92/117.98 inference(scs_inference,[],[840,921,30,29])). % 117.92/117.98 cnf(1315,plain, % 117.92/117.98 (~E(f13(x13151,a6),f12(a6))+P8(x13151,a6)), % 117.92/117.98 inference(scs_inference,[],[252,2])). % 117.92/117.98 cnf(1336,plain, % 117.92/117.98 (P1(f12(f19(f20(a3))))+~P4(f20(a3))), % 117.92/117.98 inference(scs_inference,[],[57,796,78])). % 117.92/117.98 cnf(1357,plain, % 117.92/117.98 (P1(f12(f19(f20(a3))))), % 117.92/117.98 inference(scs_inference,[],[36,1336,68])). % 117.92/117.98 cnf(1381,plain, % 117.92/117.98 (~E(x13811,f12(a6))+~E(f13(x13812,a6),x13811)+P8(x13812,a6)), % 117.92/117.98 inference(scs_inference,[],[1315,3])). % 117.92/117.98 cnf(1718,plain, % 117.92/117.98 (~E(f15(a17),f19(a1))+~E(f18(f20(a1)),f19(a17))), % 117.92/117.98 inference(scs_inference,[],[941,2])). % 117.92/117.98 cnf(1953,plain, % 117.92/117.98 (~E(f18(a1),f19(a17))+~E(f15(a17),f19(a1))), % 117.92/117.98 inference(scs_inference,[],[912,1718,3])). % 117.92/117.98 cnf(1974,plain, % 117.92/117.98 (~E(f19(a1),f15(a17))+~E(f18(a1),f19(a17))), % 117.92/117.98 inference(scs_inference,[],[1953,2])). % 117.92/117.98 cnf(1995,plain, % 117.92/117.98 (~E(x19951,f15(a17))+~E(f19(a1),x19951)+~E(f18(a1),f19(a17))), % 117.92/117.98 inference(scs_inference,[],[1974,3])). % 117.92/117.98 cnf(2371,plain, % 117.92/117.98 (~P1(f20(a16))+E(a16,f22(x23711,a16))), % 117.92/117.98 inference(scs_inference,[],[380,74])). % 117.92/117.98 cnf(2397,plain, % 117.92/117.98 (E(a16,f22(x23971,a16))), % 117.92/117.98 inference(scs_inference,[],[38,2371,66])). % 117.92/117.98 cnf(2400,plain, % 117.92/117.98 (E(f22(x24001,a16),a16)), % 117.92/117.98 inference(scs_inference,[],[2397,126,343,2])). % 117.92/117.98 cnf(2401,plain, % 117.92/117.98 (P2(f12(a16),f22(x24011,a16))), % 117.92/117.98 inference(scs_inference,[],[2397,126,343,2,198])). % 117.92/117.98 cnf(2402,plain, % 117.92/117.98 (P1(f22(x24021,a16))), % 117.92/117.98 inference(scs_inference,[],[2397,38,126,343,2,198,22])). % 117.92/117.98 cnf(2403,plain, % 117.92/117.98 (P4(f22(x24031,a16))), % 117.92/117.98 inference(scs_inference,[],[2397,38,47,126,343,2,198,22,25])). % 117.92/117.98 cnf(2404,plain, % 117.92/117.98 (~E(f19(x24041),f22(x24042,a16))), % 117.92/117.98 inference(scs_inference,[],[2397,38,287,47,126,343,2,198,22,25,3])). % 117.92/117.98 cnf(2405,plain, % 117.92/117.98 (P3(f22(x24051,a16))), % 117.92/117.98 inference(scs_inference,[],[2397,40,38,287,47,126,343,2,198,22,25,3,26])). % 117.92/117.98 cnf(2406,plain, % 117.92/117.98 (P5(f22(x24061,a16))), % 117.92/117.98 inference(scs_inference,[],[2397,120,40,38,287,47,126,343,2,198,22,25,3,26,31])). % 117.92/117.98 cnf(2407,plain, % 117.92/117.98 (~P6(x24071,f20(a16))), % 117.92/117.98 inference(scs_inference,[],[2397,120,40,38,246,287,47,126,343,2,198,22,25,3,26,31,92])). % 117.92/117.98 cnf(2408,plain, % 117.92/117.98 (E(a16,f22(x24081,a16))), % 117.92/117.98 inference(rename_variables,[],[2397])). % 117.92/117.98 cnf(2417,plain, % 117.92/117.98 (P8(x24171,x24172)+~E(f20(a16),x24171)), % 117.92/117.98 inference(scs_inference,[],[2397,2408,120,40,38,246,287,47,126,343,2,198,22,25,3,26,31,92,74,84,32,29,27])). % 117.92/117.98 cnf(2426,plain, % 117.92/117.98 (~P6(x24261,f22(x24262,a16))), % 117.92/117.98 inference(scs_inference,[],[2402,2400,155,74])). % 117.92/117.98 cnf(2430,plain, % 117.92/117.98 (~P6(x24301,f20(a16))), % 117.92/117.98 inference(rename_variables,[],[2407])). % 117.92/117.98 cnf(2432,plain, % 117.92/117.98 (P2(f12(f22(x24321,a16)),f22(x24322,a16))), % 117.92/117.98 inference(scs_inference,[],[2407,2397,143,2402,2400,155,74,198,24,28,30])). % 117.92/117.98 cnf(2433,plain, % 117.92/117.98 (~P6(x24331,f20(f22(x24332,a16)))), % 117.92/117.98 inference(scs_inference,[],[2403,2405,2407,2430,2397,143,40,2402,2400,47,155,74,198,24,28,30,101])). % 117.92/117.98 cnf(2434,plain, % 117.92/117.98 (P4(f22(x24341,a16))), % 117.92/117.98 inference(rename_variables,[],[2403])). % 117.92/117.98 cnf(2436,plain, % 117.92/117.98 (E(f22(x24361,a16),f22(x24362,f22(x24361,a16)))), % 117.92/117.98 inference(scs_inference,[],[2403,2434,2405,2407,2430,2397,143,40,2402,2400,47,155,74,198,24,28,30,101,105])). % 117.92/117.98 cnf(2437,plain, % 117.92/117.98 (P3(f22(x24371,a16))), % 117.92/117.98 inference(rename_variables,[],[2405])). % 117.92/117.98 cnf(2440,plain, % 117.92/117.98 (E(f22(x24401,f22(x24402,a16)),f22(x24402,a16))), % 117.92/117.98 inference(scs_inference,[],[2403,2434,2405,2407,2430,2397,143,40,2402,2400,47,155,74,198,24,28,30,101,105,126,2])). % 117.92/117.98 cnf(2441,plain, % 117.92/117.98 (P1(f22(x24411,f22(x24412,a16)))), % 117.92/117.98 inference(scs_inference,[],[2403,2434,2405,2407,2430,2397,143,40,2402,2400,47,155,74,198,24,28,30,101,105,126,2,22])). % 117.92/117.98 cnf(2442,plain, % 117.92/117.98 (E(a16,f22(x24421,f22(x24422,a16)))), % 117.92/117.98 inference(scs_inference,[],[2403,2434,2405,2407,2430,2397,143,40,2402,2400,47,155,74,198,24,28,30,101,105,126,2,22,3])). % 117.92/117.98 cnf(2443,plain, % 117.92/117.99 (P4(f22(x24431,f22(x24432,a16)))), % 117.92/117.99 inference(scs_inference,[],[2403,2434,2405,2407,2430,2397,143,40,2402,2400,47,155,74,198,24,28,30,101,105,126,2,22,3,25])). % 117.92/117.99 cnf(2446,plain, % 117.92/117.99 (P3(f22(x24461,f22(x24462,a16)))), % 117.92/117.99 inference(scs_inference,[],[2403,2434,2405,2437,2407,2430,2397,143,40,2402,2401,2400,47,155,74,198,24,28,30,101,105,126,2,22,3,25,29,26])). % 117.92/117.99 cnf(2465,plain, % 117.92/117.99 (E(f22(x24651,f22(x24652,a16)),a16)), % 117.92/117.99 inference(scs_inference,[],[2441,2442,343,74,2])). % 117.92/117.99 cnf(2467,plain, % 117.92/117.99 (P8(f20(f22(x24671,a16)),x24672)), % 117.92/117.99 inference(scs_inference,[],[2433,2436,2441,2442,343,74,2,198,84])). % 117.92/117.99 cnf(2468,plain, % 117.92/117.99 (~P6(x24681,f20(f22(x24682,a16)))), % 117.92/117.99 inference(rename_variables,[],[2433])). % 117.92/117.99 cnf(2471,plain, % 117.92/117.99 (~P6(x24711,f20(f22(x24712,a16)))), % 117.92/117.99 inference(rename_variables,[],[2433])). % 117.92/117.99 cnf(2476,plain, % 117.92/117.99 (~P6(x24761,f20(f22(x24762,f22(x24763,a16))))), % 117.92/117.99 inference(scs_inference,[],[2433,2468,2471,2443,2446,2436,2403,2405,170,2404,2441,2440,2432,2442,343,74,2,198,84,24,3,30,101])). % 117.92/117.99 cnf(2500,plain, % 117.92/117.99 (P2(f12(f22(x25001,f22(x25002,a16))),f22(x25003,a16))), % 117.92/117.99 inference(scs_inference,[],[2397,2433,143,2465,198,24,30])). % 117.92/117.99 cnf(2507,plain, % 117.92/117.99 (P8(x25071,x25072)+~E(f20(f22(x25073,a16)),x25071)), % 117.92/117.99 inference(scs_inference,[],[2407,2467,170,24,27])). % 117.92/117.99 cnf(2551,plain, % 117.92/117.99 (E(f22(x25511,a16),f22(x25512,a16))+P6(f10(x25512,f22(x25511,a16),a16),f20(f22(x25511,a16)))), % 117.92/117.99 inference(scs_inference,[],[2405,2403,2407,2433,40,47,95])). % 117.92/117.99 cnf(2939,plain, % 117.92/117.99 (~P6(x29391,f20(f22(x29392,f22(x29393,a16))))), % 117.92/117.99 inference(rename_variables,[],[2476])). % 117.92/117.99 cnf(2940,plain, % 117.92/117.99 (E(a16,f22(x29401,f22(x29402,f22(x29403,a16))))+P6(f10(x29401,a16,f22(x29402,f22(x29403,a16))),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[2476,2939,2407,2446,2443,47,113,40,24,95])). % 117.92/117.99 cnf(2945,plain, % 117.92/117.99 (E(f22(x29451,f22(x29452,f22(x29453,a16))),a16)+P6(f10(x29451,a16,f22(x29452,f22(x29453,a16))),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[2476,2939,2407,2446,2443,47,113,40,24,95,2])). % 117.92/117.99 cnf(2996,plain, % 117.92/117.99 (~E(f19(x29961),f20(f22(x29962,f22(x29963,a16))))), % 117.92/117.99 inference(scs_inference,[],[2476,170,24])). % 117.92/117.99 cnf(3104,plain, % 117.92/117.99 (E(a16,f22(f20(f22(x31041,a16)),a5))+P6(f10(f20(f22(x31041,a16)),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,2433,47,40,41,96])). % 117.92/117.99 cnf(3108,plain, % 117.92/117.99 (P2(f12(a16),f22(f20(f22(x31081,a16)),a5))+P6(f10(f20(f22(x31081,a16)),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,2433,47,40,41,96,198])). % 117.92/117.99 cnf(3109,plain, % 117.92/117.99 (E(f22(f20(f22(x31091,a16)),a5),a16)+P6(f10(f20(f22(x31091,a16)),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,2433,47,40,41,96,198,2])). % 117.92/117.99 cnf(3111,plain, % 117.92/117.99 (P8(f22(f20(f22(x31111,a16)),a5),x31112)+P6(f10(f20(f22(x31111,a16)),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,2433,47,40,41,96,198,2,126,343])). % 117.92/117.99 cnf(3113,plain, % 117.92/117.99 (P1(f22(f20(f22(x31131,a16)),a5))+P6(f10(f20(f22(x31131,a16)),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,2433,2500,550,47,40,41,38,96,198,2,126,343,29,73,22])). % 117.92/117.99 cnf(3117,plain, % 117.92/117.99 (~P6(x31171,f20(a16))), % 117.92/117.99 inference(rename_variables,[],[2407])). % 117.92/117.99 cnf(3119,plain, % 117.92/117.99 (~P6(x31191,f20(a16))), % 117.92/117.99 inference(rename_variables,[],[2407])). % 117.92/117.99 cnf(3120,plain, % 117.92/117.99 (P1(f22(f20(f22(x31201,a16)),a5))), % 117.92/117.99 inference(scs_inference,[],[2407,3117,3119,3108,3111,3113])). % 117.92/117.99 cnf(3137,plain, % 117.92/117.99 (E(a16,f22(a3,a5))+P6(f10(a3,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,133,40,41,96])). % 117.92/117.99 cnf(3141,plain, % 117.92/117.99 (P2(f12(a16),f22(a3,a5))+P6(f10(a3,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,133,40,41,96,198])). % 117.92/117.99 cnf(3142,plain, % 117.92/117.99 (E(f22(a3,a5),a16)+P6(f10(a3,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,133,40,41,96,198,2])). % 117.92/117.99 cnf(3144,plain, % 117.92/117.99 (P8(f22(a3,a5),x31441)+P6(f10(a3,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,133,40,41,96,198,2,126,343])). % 117.92/117.99 cnf(3146,plain, % 117.92/117.99 (E(f22(x31461,a16),f22(a3,a5))+P6(f10(a3,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,2500,550,47,133,40,41,2400,96,198,2,126,343,73,29,3])). % 117.92/117.99 cnf(3148,plain, % 117.92/117.99 (P1(f22(a3,a5))+P6(f10(a3,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,2500,550,47,133,40,41,2400,143,913,38,96,198,2,126,343,73,29,3,23,87,22])). % 117.92/117.99 cnf(3151,plain, % 117.92/117.99 (E(a16,f22(a3,a5))), % 117.92/117.99 inference(scs_inference,[],[2407,3137])). % 117.92/117.99 cnf(3152,plain, % 117.92/117.99 (P2(f12(a16),f22(a3,a5))), % 117.92/117.99 inference(scs_inference,[],[2407,3141])). % 117.92/117.99 cnf(3153,plain, % 117.92/117.99 (E(f22(a3,a5),a16)), % 117.92/117.99 inference(scs_inference,[],[2407,3142])). % 117.92/117.99 cnf(3154,plain, % 117.92/117.99 (P8(f22(a3,a5),x31541)), % 117.92/117.99 inference(scs_inference,[],[2407,3144])). % 117.92/117.99 cnf(3155,plain, % 117.92/117.99 (E(f22(x31551,a16),f22(a3,a5))), % 117.92/117.99 inference(scs_inference,[],[2407,3146])). % 117.92/117.99 cnf(3156,plain, % 117.92/117.99 (P1(f22(a3,a5))), % 117.92/117.99 inference(scs_inference,[],[2407,3148])). % 117.92/117.99 cnf(3162,plain, % 117.92/117.99 (P2(f12(f22(x31621,a16)),f22(a3,a5))), % 117.92/117.99 inference(scs_inference,[],[3155,155,198])). % 117.92/117.99 cnf(3165,plain, % 117.92/117.99 (E(f22(a3,a5),f22(x31651,a16))), % 117.92/117.99 inference(scs_inference,[],[3156,3155,155,198,74,2])). % 117.92/117.99 cnf(3166,plain, % 117.92/117.99 (P3(f22(a3,a5))), % 117.92/117.99 inference(scs_inference,[],[3151,40,3156,3155,155,198,74,2,26])). % 117.92/117.99 cnf(3167,plain, % 117.92/117.99 (P4(f22(a3,a5))), % 117.92/117.99 inference(scs_inference,[],[3151,47,40,3156,3155,155,198,74,2,26,25])). % 117.92/117.99 cnf(3168,plain, % 117.92/117.99 (P5(f22(a3,a5))), % 117.92/117.99 inference(scs_inference,[],[3151,120,47,40,3156,3155,155,198,74,2,26,25,31])). % 117.92/117.99 cnf(3169,plain, % 117.92/117.99 (~E(f19(x31691),f22(a3,a5))), % 117.92/117.99 inference(scs_inference,[],[3151,120,47,40,287,3156,3155,3153,155,198,74,2,26,25,31,3])). % 117.92/117.99 cnf(3170,plain, % 117.92/117.99 (~P6(x31701,f20(f22(a3,a5)))), % 117.92/117.99 inference(scs_inference,[],[49,3151,120,47,133,40,41,287,3156,3155,3153,155,198,74,2,26,25,31,3,103])). % 117.92/117.99 cnf(3173,plain, % 117.92/117.99 (E(f22(a3,a5),f22(x31731,f22(a3,a5)))), % 117.92/117.99 inference(scs_inference,[],[49,3151,120,47,133,40,41,287,3156,3155,3153,155,198,74,2,26,25,31,3,103,105])). % 117.92/117.99 cnf(3177,plain, % 117.92/117.99 (P1(f22(x31771,f22(a3,a5)))), % 117.92/117.99 inference(scs_inference,[],[49,3151,120,47,133,40,41,287,3156,3155,3152,3153,155,198,74,2,26,25,31,3,103,105,126,29,22])). % 117.92/117.99 cnf(3183,plain, % 117.92/117.99 (P8(f20(f22(a3,a5)),x31831)), % 117.92/117.99 inference(scs_inference,[],[3170,84])). % 117.92/117.99 cnf(3190,plain, % 117.92/117.99 (E(f22(x31901,f22(a3,a5)),f22(a3,a5))), % 117.92/117.99 inference(scs_inference,[],[3170,3173,3153,3177,84,155,198,74,2])). % 117.92/117.99 cnf(3191,plain, % 117.92/117.99 (P3(f22(x31911,f22(a3,a5)))), % 117.92/117.99 inference(scs_inference,[],[3170,3173,3166,3153,3177,84,155,198,74,2,26])). % 117.92/117.99 cnf(3193,plain, % 117.92/117.99 (P4(f22(x31931,f22(a3,a5)))), % 117.92/117.99 inference(scs_inference,[],[3154,3170,3173,3166,3167,3153,3177,84,155,198,74,2,26,27,25])). % 117.92/117.99 cnf(3196,plain, % 117.92/117.99 (E(a16,f22(x31961,f22(a3,a5)))), % 117.92/117.99 inference(scs_inference,[],[2397,3151,3154,3170,3173,3166,3167,3153,3177,3168,84,155,198,74,2,26,27,25,31,28,3])). % 117.92/117.99 cnf(3206,plain, % 117.92/117.99 (E(f22(x32061,f22(a3,a5)),a16)), % 117.92/117.99 inference(scs_inference,[],[3165,3196,198,2])). % 117.92/117.99 cnf(3209,plain, % 117.92/117.99 (P8(x32091,x32092)+~E(f20(f22(a3,a5)),x32091)), % 117.92/117.99 inference(scs_inference,[],[3173,3183,3165,3190,3169,3162,3196,198,2,3,30,27])). % 117.92/117.99 cnf(3308,plain, % 117.92/117.99 (P8(f22(f20(f22(a3,a5)),a5),x33081)+P6(f10(f20(f22(a3,a5)),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,3170,47,40,41,96,343])). % 117.92/117.99 cnf(3315,plain, % 117.92/117.99 (E(a16,f22(a14,a5))+P6(f10(a14,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,162,41,96])). % 117.92/117.99 cnf(3319,plain, % 117.92/117.99 (P8(f22(a14,a5),x33191)+P6(f10(a14,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,162,41,96,343])). % 117.92/117.99 cnf(3320,plain, % 117.92/117.99 (E(f22(a14,a5),a16)+P6(f10(a14,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,162,41,96,343,2])). % 117.92/117.99 cnf(3321,plain, % 117.92/117.99 (P2(f12(a16),f22(a14,a5))+P6(f10(a14,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,162,41,96,343,2,198])). % 117.92/117.99 cnf(3322,plain, % 117.92/117.99 (P1(f22(a14,a5))+P6(f10(a14,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,162,41,38,96,343,2,198,22])). % 117.92/117.99 cnf(3323,plain, % 117.92/117.99 (E(f22(x33231,a16),f22(a14,a5))+P6(f10(a14,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,2400,47,40,162,41,38,96,343,2,198,22,3])). % 117.92/117.99 cnf(3327,plain, % 117.92/117.99 (P8(f22(f20(f22(a3,a5)),a5),x33271)), % 117.92/117.99 inference(scs_inference,[],[2407,3308])). % 117.92/117.99 cnf(3332,plain, % 117.92/117.99 (E(a16,f22(a16,a5))+P6(f10(a16,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,209,41,96])). % 117.92/117.99 cnf(3337,plain, % 117.92/117.99 (P8(f22(a16,a5),x33371)+P6(f10(a16,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,209,41,96,126,343])). % 117.92/117.99 cnf(3338,plain, % 117.92/117.99 (E(f22(a16,a5),a16)+P6(f10(a16,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,209,41,96,126,343,2])). % 117.92/117.99 cnf(3339,plain, % 117.92/117.99 (P2(f12(a16),f22(a16,a5))+P6(f10(a16,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,209,41,96,126,343,2,198])). % 117.92/117.99 cnf(3340,plain, % 117.92/117.99 (P1(f22(a16,a5))+P6(f10(a16,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,209,41,38,96,126,343,2,198,22])). % 117.92/117.99 cnf(3342,plain, % 117.92/117.99 (E(f22(x33421,a16),f22(a16,a5))+P6(f10(a16,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,550,2400,47,40,209,41,38,96,126,343,2,198,22,73,3])). % 117.92/117.99 cnf(3345,plain, % 117.92/117.99 (E(a16,f22(a14,a5))), % 117.92/117.99 inference(scs_inference,[],[2407,3315])). % 117.92/117.99 cnf(3346,plain, % 117.92/117.99 (P8(f22(a14,a5),x33461)), % 117.92/117.99 inference(scs_inference,[],[2407,3319])). % 117.92/117.99 cnf(3347,plain, % 117.92/117.99 (E(f22(a14,a5),a16)), % 117.92/117.99 inference(scs_inference,[],[2407,3320])). % 117.92/117.99 cnf(3348,plain, % 117.92/117.99 (P2(f12(a16),f22(a14,a5))), % 117.92/117.99 inference(scs_inference,[],[2407,3321])). % 117.92/117.99 cnf(3349,plain, % 117.92/117.99 (P1(f22(a14,a5))), % 117.92/117.99 inference(scs_inference,[],[2407,3322])). % 117.92/117.99 cnf(3350,plain, % 117.92/117.99 (E(f22(x33501,a16),f22(a14,a5))), % 117.92/117.99 inference(scs_inference,[],[2407,3323])). % 117.92/117.99 cnf(3365,plain, % 117.92/117.99 (E(a16,f22(a16,a5))), % 117.92/117.99 inference(scs_inference,[],[2407,3332])). % 117.92/117.99 cnf(3366,plain, % 117.92/117.99 (P8(f22(a16,a5),x33661)), % 117.92/117.99 inference(scs_inference,[],[2407,3337])). % 117.92/117.99 cnf(3367,plain, % 117.92/117.99 (E(f22(a16,a5),a16)), % 117.92/117.99 inference(scs_inference,[],[2407,3338])). % 117.92/117.99 cnf(3368,plain, % 117.92/117.99 (P2(f12(a16),f22(a16,a5))), % 117.92/117.99 inference(scs_inference,[],[2407,3339])). % 117.92/117.99 cnf(3369,plain, % 117.92/117.99 (P1(f22(a16,a5))), % 117.92/117.99 inference(scs_inference,[],[2407,3340])). % 117.92/117.99 cnf(3370,plain, % 117.92/117.99 (E(f22(x33701,a16),f22(a16,a5))), % 117.92/117.99 inference(scs_inference,[],[2407,3342])). % 117.92/117.99 cnf(3374,plain, % 117.92/117.99 (E(f22(a14,a5),f22(x33741,a16))), % 117.92/117.99 inference(scs_inference,[],[3349,3350,155,74,2])). % 117.92/117.99 cnf(3375,plain, % 117.92/117.99 (P2(f12(f22(x33751,a16)),f22(a14,a5))), % 117.92/117.99 inference(scs_inference,[],[3349,3350,155,74,2,198])). % 117.92/117.99 cnf(3377,plain, % 117.92/117.99 (P3(f22(a14,a5))), % 117.92/117.99 inference(scs_inference,[],[3345,40,287,3349,3350,3347,155,74,2,198,3,26])). % 117.92/117.99 cnf(3378,plain, % 117.92/117.99 (P4(f22(a14,a5))), % 117.92/117.99 inference(scs_inference,[],[3345,47,40,287,3349,3350,3347,155,74,2,198,3,26,25])). % 117.92/117.99 cnf(3379,plain, % 117.92/117.99 (P5(f22(a14,a5))), % 117.92/117.99 inference(scs_inference,[],[3345,120,47,40,287,3349,3350,3347,155,74,2,198,3,26,25,31])). % 117.92/117.99 cnf(3380,plain, % 117.92/117.99 (~P6(x33801,f20(f22(a14,a5)))), % 117.92/117.99 inference(scs_inference,[],[2407,3345,120,47,40,287,3349,3350,3347,155,74,2,198,3,26,25,31,92])). % 117.92/117.99 cnf(3383,plain, % 117.92/117.99 (E(f22(a14,a5),f22(x33831,f22(a14,a5)))), % 117.92/117.99 inference(scs_inference,[],[2407,3345,120,47,40,287,3349,3350,3347,155,74,2,198,3,26,25,31,92,105])). % 117.92/117.99 cnf(3385,plain, % 117.92/117.99 (P8(f22(x33851,f22(a14,a5)),f22(a14,a5))), % 117.92/117.99 inference(scs_inference,[],[2407,3345,120,47,40,287,3349,3350,3347,155,74,2,198,3,26,25,31,92,105,126])). % 117.92/117.99 cnf(3386,plain, % 117.92/117.99 (P1(f22(x33861,f22(a14,a5)))), % 117.92/117.99 inference(scs_inference,[],[2407,3345,120,47,40,287,3349,3350,3347,155,74,2,198,3,26,25,31,92,105,126,22])). % 117.92/117.99 cnf(3395,plain, % 117.92/117.99 (P8(f20(f22(a14,a5)),x33951)), % 117.92/117.99 inference(scs_inference,[],[3380,84])). % 117.92/117.99 cnf(3404,plain, % 117.92/117.99 (P8(f22(x34041,f22(a14,a5)),x34042)), % 117.92/117.99 inference(scs_inference,[],[3346,3380,3385,3383,3386,3370,84,155,74,2,198,28,27])). % 117.92/117.99 cnf(3406,plain, % 117.92/117.99 (P4(f22(x34061,f22(a14,a5)))), % 117.92/117.99 inference(scs_inference,[],[3346,3345,3380,3385,3383,3378,3386,3370,84,155,74,2,198,28,27,3,25])). % 117.92/117.99 cnf(3407,plain, % 117.92/117.99 (P3(f22(x34071,f22(a14,a5)))), % 117.92/117.99 inference(scs_inference,[],[3346,3345,3380,3385,3383,3377,3378,3386,3370,84,155,74,2,198,28,27,3,25,26])). % 117.92/117.99 cnf(3410,plain, % 117.92/117.99 (~P6(x34101,f20(f22(f20(a16),f22(a14,a5))))), % 117.92/117.99 inference(scs_inference,[],[2407,3346,3345,3380,3385,3383,3377,3378,3348,3386,3379,3370,84,155,74,2,198,28,27,3,25,26,31,30,103])). % 117.92/117.99 cnf(3419,plain, % 117.92/117.99 (P8(f12(f19(f22(a14,a5))),f22(x34191,a16))), % 117.92/117.99 inference(scs_inference,[],[3374,155])). % 117.92/117.99 cnf(3420,plain, % 117.92/117.99 (~P6(x34201,f22(a16,a5))), % 117.92/117.99 inference(scs_inference,[],[3374,3369,155,74])). % 117.92/117.99 cnf(3422,plain, % 117.92/117.99 (P2(f12(f22(a14,a5)),f22(x34221,a16))), % 117.92/117.99 inference(scs_inference,[],[3374,3369,155,74,198])). % 117.92/117.99 cnf(3423,plain, % 117.92/117.99 (E(f22(a16,a5),f22(x34231,a16))), % 117.92/117.99 inference(scs_inference,[],[3374,3370,3369,155,74,198,2])). % 117.92/117.99 cnf(3424,plain, % 117.92/117.99 (P4(f22(a16,a5))), % 117.92/117.99 inference(scs_inference,[],[3365,47,3374,3370,3369,155,74,198,2,25])). % 117.92/117.99 cnf(3426,plain, % 117.92/117.99 (P3(f22(a16,a5))), % 117.92/117.99 inference(scs_inference,[],[3365,47,40,287,3374,3370,3367,3369,155,74,198,2,25,3,26])). % 117.92/117.99 cnf(3427,plain, % 117.92/117.99 (P5(f22(a16,a5))), % 117.92/117.99 inference(scs_inference,[],[3365,120,47,40,287,3374,3370,3367,3369,155,74,198,2,25,3,26,31])). % 117.92/117.99 cnf(3430,plain, % 117.92/117.99 (P4(f22(x34301,f22(a14,a5)))), % 117.92/117.99 inference(rename_variables,[],[3406])). % 117.92/117.99 cnf(3432,plain, % 117.92/117.99 (~P6(x34321,f20(f22(a16,a5)))), % 117.92/117.99 inference(scs_inference,[],[2407,3365,3377,3378,3406,3407,3380,120,3383,47,40,287,3374,3370,3367,3369,3375,155,74,198,2,25,3,26,31,30,101,92])). % 117.92/117.99 cnf(3433,plain, % 117.92/117.99 (~P6(x34331,f20(a16))), % 117.92/117.99 inference(rename_variables,[],[2407])). % 117.92/117.99 cnf(3435,plain, % 117.92/117.99 (E(f22(a16,a5),f22(x34351,f22(a16,a5)))), % 117.92/117.99 inference(scs_inference,[],[2407,3365,3377,3378,3406,3407,3380,120,3383,47,40,287,3374,3370,3367,3369,3375,155,74,198,2,25,3,26,31,30,101,92,105])). % 117.92/117.99 cnf(3437,plain, % 117.92/117.99 (E(f22(f20(a16),f22(a14,a5)),f22(x34371,a16))), % 117.92/117.99 inference(scs_inference,[],[2407,3433,3365,3377,3378,3406,3430,3407,3410,3380,120,3383,47,40,287,3374,3370,3367,3369,3375,155,74,198,2,25,3,26,31,30,101,92,105,95])). % 117.92/117.99 cnf(3443,plain, % 117.92/117.99 (P8(f22(x34431,f22(a16,a5)),f22(a16,a5))), % 117.92/117.99 inference(scs_inference,[],[2407,3433,3365,3377,3378,3406,3430,3407,3410,3380,120,3383,47,40,287,3374,3370,3367,3369,3375,155,74,198,2,25,3,26,31,30,101,92,105,95,126])). % 117.92/117.99 cnf(3444,plain, % 117.92/117.99 (P1(f22(x34441,f22(a16,a5)))), % 117.92/117.99 inference(scs_inference,[],[2407,3433,3365,3377,3378,3406,3430,3407,3410,3380,120,3383,47,40,287,3374,3370,3367,3369,3375,155,74,198,2,25,3,26,31,30,101,92,105,95,126,22])). % 117.92/117.99 cnf(3446,plain, % 117.92/117.99 (P8(x34461,x34462)+~E(f20(f22(a14,a5)),x34461)), % 117.92/117.99 inference(scs_inference,[],[2407,3433,3365,3377,3378,3395,3406,3430,3407,3410,3380,120,3383,47,40,287,3374,3370,3367,3369,3375,155,74,198,2,25,3,26,31,30,101,92,105,95,126,22,28,27])). % 117.92/117.99 cnf(3454,plain, % 117.92/117.99 (P8(f20(f22(a16,a5)),x34541)), % 117.92/117.99 inference(scs_inference,[],[3432,84])). % 117.92/117.99 cnf(3464,plain, % 117.92/117.99 (P4(f22(x34641,f22(a16,a5)))), % 117.92/117.99 inference(scs_inference,[],[3432,3366,3443,3435,3424,3347,3444,84,155,74,198,2,28,27,25])). % 117.92/117.99 cnf(3465,plain, % 117.92/117.99 (P3(f22(x34651,f22(a16,a5)))), % 117.92/117.99 inference(scs_inference,[],[3432,3366,3443,3435,3424,3426,3347,3444,84,155,74,198,2,28,27,25,26])). % 117.92/117.99 cnf(3470,plain, % 117.92/117.99 (~P6(x34701,f20(f22(f20(a16),f22(a16,a5))))), % 117.92/117.99 inference(scs_inference,[],[2436,2407,3365,3432,3366,3443,3435,3424,3426,3347,3444,3427,3422,84,155,74,198,2,28,27,25,26,3,31,30,103])). % 117.92/117.99 cnf(3481,plain, % 117.92/117.99 (P8(f12(f19(f22(a16,a5))),f22(x34811,a16))), % 117.92/117.99 inference(scs_inference,[],[3423,155])). % 117.92/117.99 cnf(3488,plain, % 117.92/117.99 (P4(f22(x34881,f22(a16,a5)))), % 117.92/117.99 inference(rename_variables,[],[3464])). % 117.92/117.99 cnf(3496,plain, % 117.92/117.99 (P8(x34961,x34962)+~E(f20(f22(a16,a5)),x34961)), % 117.92/117.99 inference(scs_inference,[],[2407,3437,3426,3424,3435,3454,3464,3488,3465,3470,3432,47,40,2404,3423,3368,155,198,2,3,30,101,95,27])). % 117.92/117.99 cnf(3732,plain, % 117.92/117.99 (E(f22(x37321,a16),f22(f20(a16),a5))+P6(f10(f20(a16),f22(x37321,a16),a5),f20(f22(x37321,a16)))), % 117.92/117.99 inference(scs_inference,[],[49,2403,2405,2407,2433,41,96])). % 117.92/117.99 cnf(3737,plain, % 117.92/117.99 (P8(f22(f20(a16),a5),f22(x37371,a16))+P6(f10(f20(a16),f22(x37371,a16),a5),f20(f22(x37371,a16)))), % 117.92/117.99 inference(scs_inference,[],[49,2403,2405,2407,2433,41,96,126])). % 117.92/117.99 cnf(3738,plain, % 117.92/117.99 (E(f22(f20(a16),a5),f22(x37381,a16))+P6(f10(f20(a16),f22(x37381,a16),a5),f20(f22(x37381,a16)))), % 117.92/117.99 inference(scs_inference,[],[49,2403,2405,2407,2433,41,96,126,2])). % 117.92/117.99 cnf(3739,plain, % 117.92/117.99 (P2(f12(f22(x37391,a16)),f22(f20(a16),a5))+P6(f10(f20(a16),f22(x37391,a16),a5),f20(f22(x37391,a16)))), % 117.92/117.99 inference(scs_inference,[],[49,2403,2405,2407,2433,41,96,126,2,198])). % 117.92/117.99 cnf(3740,plain, % 117.92/117.99 (P1(f22(f20(a16),a5))+P6(f10(f20(a16),f22(x37401,a16),a5),f20(f22(x37401,a16)))), % 117.92/117.99 inference(scs_inference,[],[49,2403,2405,2407,2433,41,2402,96,126,2,198,22])). % 117.92/117.99 cnf(3745,plain, % 117.92/117.99 (E(f22(x37451,a16),f22(f20(a16),a5))), % 117.92/117.99 inference(scs_inference,[],[2433,3732])). % 117.92/117.99 cnf(3746,plain, % 117.92/117.99 (~P6(x37461,f20(f22(x37462,a16)))), % 117.92/117.99 inference(rename_variables,[],[2433])). % 117.92/117.99 cnf(3749,plain, % 117.92/117.99 (~P6(x37491,f20(f22(x37492,a16)))), % 117.92/117.99 inference(rename_variables,[],[2433])). % 117.92/117.99 cnf(3752,plain, % 117.92/117.99 (~P6(x37521,f20(f22(x37522,a16)))), % 117.92/117.99 inference(rename_variables,[],[2433])). % 117.92/117.99 cnf(3755,plain, % 117.92/117.99 (~P6(x37551,f20(f22(x37552,a16)))), % 117.92/117.99 inference(rename_variables,[],[2433])). % 117.92/117.99 cnf(3757,plain, % 117.92/117.99 (P1(f22(f20(a16),a5))), % 117.92/117.99 inference(scs_inference,[],[2433,3746,3749,3752,3755,3732,3737,3738,3739,3740])). % 117.92/117.99 cnf(3764,plain, % 117.92/117.99 (P4(f22(f20(a16),a5))), % 117.92/117.99 inference(scs_inference,[],[2397,2403,2433,3746,3749,3752,3755,3732,3737,3738,3739,3740,74,198,3,25])). % 117.92/117.99 cnf(3765,plain, % 117.92/117.99 (P3(f22(f20(a16),a5))), % 117.92/117.99 inference(scs_inference,[],[2397,2403,2405,2433,3746,3749,3752,3755,3732,3737,3738,3739,3740,74,198,3,25,26])). % 117.92/117.99 cnf(3773,plain, % 117.92/117.99 (E(f22(f20(a16),a5),a16)), % 117.92/117.99 inference(scs_inference,[],[2397,2436,2403,2405,2407,2433,3746,3749,3752,3755,47,40,2406,3732,3737,3738,3739,3740,74,198,3,25,26,31,28,92,84,2])). % 117.92/117.99 cnf(3827,plain, % 117.92/117.99 (P8(f22(f20(f22(a14,a5)),a5),x38271)+P6(f10(f20(f22(a14,a5)),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,3380,47,40,41,96,343])). % 117.92/117.99 cnf(3838,plain, % 117.92/117.99 (P8(f22(f20(f22(a16,a5)),a5),x38381)+P6(f10(f20(f22(a16,a5)),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,3432,47,40,41,96,343])). % 117.92/117.99 cnf(3839,plain, % 117.92/117.99 (E(f22(f20(f22(a16,a5)),a5),a16)+P6(f10(f20(f22(a16,a5)),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,3432,47,40,41,96,343,2])). % 117.92/117.99 cnf(3841,plain, % 117.92/117.99 (P1(f22(f20(f22(a16,a5)),a5))+P6(f10(f20(f22(a16,a5)),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,3432,47,40,41,38,96,343,2,198,22])). % 117.92/117.99 cnf(3843,plain, % 117.92/117.99 (E(f22(x38431,a16),f22(f20(f22(a16,a5)),a5))+P6(f10(f20(f22(a16,a5)),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,3432,2400,550,624,913,47,40,41,38,96,343,2,198,22,87,73,65,3])). % 117.92/117.99 cnf(3846,plain, % 117.92/117.99 (P8(f22(f20(f22(a14,a5)),a5),x38461)), % 117.92/117.99 inference(scs_inference,[],[2407,3827])). % 117.92/117.99 cnf(3855,plain, % 117.92/117.99 (P8(f22(f12(f19(a14)),a5),x38551)+P6(f10(f12(f19(a14)),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,167,41,96,343])). % 117.92/117.99 cnf(3862,plain, % 117.92/117.99 (P8(f22(f20(f22(a16,a5)),a5),x38621)), % 117.92/117.99 inference(scs_inference,[],[2407,3838])). % 117.92/117.99 cnf(3863,plain, % 117.92/117.99 (E(f22(f20(f22(a16,a5)),a5),a16)), % 117.92/117.99 inference(scs_inference,[],[2407,3839])). % 117.92/117.99 cnf(3865,plain, % 117.92/117.99 (P1(f22(f20(f22(a16,a5)),a5))), % 117.92/117.99 inference(scs_inference,[],[2407,3841])). % 117.92/117.99 cnf(3866,plain, % 117.92/117.99 (E(f22(x38661,a16),f22(f20(f22(a16,a5)),a5))), % 117.92/117.99 inference(scs_inference,[],[2407,3843])). % 117.92/117.99 cnf(3888,plain, % 117.92/117.99 (P8(f22(f12(f19(a14)),a5),x38881)), % 117.92/117.99 inference(scs_inference,[],[2407,3855])). % 117.92/117.99 cnf(3894,plain, % 117.92/117.99 (E(f22(f20(f22(a16,a5)),a5),f22(x38941,a16))), % 117.92/117.99 inference(scs_inference,[],[3865,3866,74,2])). % 117.92/117.99 cnf(3955,plain, % 117.92/117.99 (~P6(x39551,f20(a16))), % 117.92/117.99 inference(rename_variables,[],[2407])). % 117.92/117.99 cnf(3956,plain, % 117.92/117.99 (E(a16,f22(f12(f19(a16)),a5))+P6(f10(f12(f19(a16)),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,42,51,2407,3955,359,47,40,214,41,3894,32,71,103,96])). % 117.92/117.99 cnf(3963,plain, % 117.92/117.99 (E(a16,f22(f12(f19(a16)),a5))), % 117.92/117.99 inference(scs_inference,[],[2407,3956])). % 117.92/117.99 cnf(3968,plain, % 117.92/117.99 (P8(f22(f12(f19(a16)),a5),x39681)), % 117.92/117.99 inference(scs_inference,[],[3963,126,343])). % 117.92/117.99 cnf(3969,plain, % 117.92/117.99 (E(f22(f12(f19(a16)),a5),a16)), % 117.92/117.99 inference(scs_inference,[],[3963,126,343,2])). % 117.92/117.99 cnf(4001,plain, % 117.92/117.99 (~P6(x40011,f20(a16))), % 117.92/117.99 inference(rename_variables,[],[2407])). % 117.92/117.99 cnf(4002,plain, % 117.92/117.99 (E(a16,f22(f12(f19(a3)),a5))+P6(f10(f12(f19(a3)),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,42,51,2407,4001,359,47,40,246,41,3863,32,71,103,96])). % 117.92/117.99 cnf(4009,plain, % 117.92/117.99 (E(a16,f22(f12(f19(a3)),a5))), % 117.92/117.99 inference(scs_inference,[],[2407,4002])). % 117.92/117.99 cnf(4012,plain, % 117.92/117.99 (P8(f22(f12(f19(a3)),a5),x40121)), % 117.92/117.99 inference(scs_inference,[],[4009,126,343])). % 117.92/117.99 cnf(4050,plain, % 117.92/117.99 (~P6(x40501,f20(a16))), % 117.92/117.99 inference(rename_variables,[],[2407])). % 117.92/117.99 cnf(4051,plain, % 117.92/117.99 (E(a16,f22(f18(x40511),a5))+P6(f10(f18(x40511),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,42,51,2407,4050,359,47,40,184,41,3969,32,71,103,96])). % 117.92/117.99 cnf(4061,plain, % 117.92/117.99 (E(a16,f22(f12(f19(a1)),a5))+P6(f10(f12(f19(a1)),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,116,41,96])). % 117.92/117.99 cnf(4065,plain, % 117.92/117.99 (P8(f22(f12(f19(a1)),a5),x40651)+P6(f10(f12(f19(a1)),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,116,41,96,343])). % 117.92/117.99 cnf(4067,plain, % 117.92/117.99 (P2(f12(a16),f22(f12(f19(a1)),a5))+P6(f10(f12(f19(a1)),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,116,41,96,343,2,198])). % 117.92/117.99 cnf(4068,plain, % 117.92/117.99 (P1(f22(f12(f19(a1)),a5))+P6(f10(f12(f19(a1)),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,116,41,38,96,343,2,198,22])). % 117.92/117.99 cnf(4071,plain, % 117.92/117.99 (E(a16,f22(a1,a5))+P6(f10(a1,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,111,41,96])). % 117.92/117.99 cnf(4076,plain, % 117.92/117.99 (P8(f22(a1,a5),x40761)+P6(f10(a1,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,111,41,96,126,343])). % 117.92/117.99 cnf(4077,plain, % 117.92/117.99 (E(f22(a1,a5),a16)+P6(f10(a1,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,111,41,96,126,343,2])). % 117.92/117.99 cnf(4079,plain, % 117.92/117.99 (P1(f22(a1,a5))+P6(f10(a1,a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,111,41,38,96,126,343,2,198,22])). % 117.92/117.99 cnf(4082,plain, % 117.92/117.99 (E(a16,f22(f12(f19(a1)),a5))), % 117.92/117.99 inference(scs_inference,[],[2407,4061])). % 117.92/117.99 cnf(4083,plain, % 117.92/117.99 (P8(f22(f12(f19(a1)),a5),x40831)), % 117.92/117.99 inference(scs_inference,[],[2407,4065])). % 117.92/117.99 cnf(4085,plain, % 117.92/117.99 (P2(f12(a16),f22(f12(f19(a1)),a5))), % 117.92/117.99 inference(scs_inference,[],[2407,4067])). % 117.92/117.99 cnf(4086,plain, % 117.92/117.99 (P1(f22(f12(f19(a1)),a5))), % 117.92/117.99 inference(scs_inference,[],[2407,4068])). % 117.92/117.99 cnf(4087,plain, % 117.92/117.99 (E(a16,f22(f20(a1),a5))+P6(f10(f20(a1),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,510,41,96])). % 117.92/117.99 cnf(4092,plain, % 117.92/117.99 (P8(f22(f20(a1),a5),x40921)+P6(f10(f20(a1),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,510,41,96,126,343])). % 117.92/117.99 cnf(4093,plain, % 117.92/117.99 (E(f22(f20(a1),a5),a16)+P6(f10(f20(a1),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,510,41,96,126,343,2])). % 117.92/117.99 cnf(4095,plain, % 117.92/117.99 (P1(f22(f20(a1),a5))+P6(f10(f20(a1),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2407,47,40,510,41,38,96,126,343,2,198,22])). % 117.92/117.99 cnf(4098,plain, % 117.92/117.99 (E(a16,f22(a1,a5))), % 117.92/117.99 inference(scs_inference,[],[2407,4071])). % 117.92/117.99 cnf(4099,plain, % 117.92/117.99 (P8(f22(a1,a5),x40991)), % 117.92/117.99 inference(scs_inference,[],[2407,4076])). % 117.92/117.99 cnf(4100,plain, % 117.92/117.99 (E(f22(a1,a5),a16)), % 117.92/117.99 inference(scs_inference,[],[2407,4077])). % 117.92/117.99 cnf(4102,plain, % 117.92/117.99 (P1(f22(a1,a5))), % 117.92/117.99 inference(scs_inference,[],[2407,4079])). % 117.92/117.99 cnf(4104,plain, % 117.92/117.99 (E(a16,f22(f20(a1),a5))), % 117.92/117.99 inference(scs_inference,[],[2407,4087])). % 117.92/117.99 cnf(4105,plain, % 117.92/117.99 (P8(f22(f20(a1),a5),x41051)), % 117.92/117.99 inference(scs_inference,[],[2407,4092])). % 117.92/117.99 cnf(4106,plain, % 117.92/117.99 (E(f22(f20(a1),a5),a16)), % 117.92/117.99 inference(scs_inference,[],[2407,4093])). % 117.92/117.99 cnf(4108,plain, % 117.92/117.99 (P1(f22(f20(a1),a5))), % 117.92/117.99 inference(scs_inference,[],[2407,4095])). % 117.92/117.99 cnf(4109,plain, % 117.92/117.99 (P8(f12(f19(f22(a1,a5))),a16)), % 117.92/117.99 inference(scs_inference,[],[4100,155])). % 117.92/117.99 cnf(4115,plain, % 117.92/117.99 (P8(f12(f19(f22(a1,a5))),f22(x41151,a16))), % 117.92/117.99 inference(scs_inference,[],[2397,4082,120,2400,4086,4100,155,74,198,3,31,28])). % 117.92/117.99 cnf(4118,plain, % 117.92/117.99 (P2(f12(f22(a1,a5)),f22(x41181,a16))), % 117.92/117.99 inference(scs_inference,[],[2397,4082,120,2400,47,40,4086,4100,155,74,198,3,31,28,26,25,30])). % 117.92/117.99 cnf(4124,plain, % 117.92/117.99 (E(a16,f22(f21(f20(a3)),a5))+P6(f10(f21(f20(a3)),a16,a5),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[49,2397,2407,4082,120,359,2400,47,40,551,41,4086,4085,4100,155,74,198,3,31,28,26,25,30,2,27,29,32,71,96])). % 117.92/117.99 cnf(4132,plain, % 117.92/117.99 (P2(f12(f22(f20(a1),a5)),a16)), % 117.92/117.99 inference(scs_inference,[],[4108,4106,74,198])). % 117.92/117.99 cnf(4133,plain, % 117.92/117.99 (P5(f22(a1,a5))), % 117.92/117.99 inference(scs_inference,[],[4098,120,4108,4106,74,198,31])). % 117.92/117.99 cnf(4134,plain, % 117.92/117.99 (E(f22(x41341,a16),f22(a1,a5))), % 117.92/117.99 inference(scs_inference,[],[4098,120,2400,4108,4106,74,198,31,3])). % 117.92/117.99 cnf(4135,plain, % 117.92/117.99 (P3(f22(a1,a5))), % 117.92/117.99 inference(scs_inference,[],[4098,120,2400,40,4108,4106,74,198,31,3,26])). % 117.92/117.99 cnf(4136,plain, % 117.92/117.99 (P4(f22(a1,a5))), % 117.92/117.99 inference(scs_inference,[],[4098,120,2400,47,40,4108,4106,74,198,31,3,26,25])). % 117.92/117.99 cnf(4140,plain, % 117.92/117.99 (E(f22(a1,a5),f22(x41401,a16))), % 117.92/117.99 inference(scs_inference,[],[2436,4098,120,2400,47,40,4108,4118,4106,74,198,31,3,26,25,30,155,2])). % 117.92/117.99 cnf(4143,plain, % 117.92/117.99 (~E(f12(f19(f22(a1,a5))),x41431)+~P6(x41432,f20(f22(a1,a5)))), % 117.92/117.99 inference(scs_inference,[],[2436,2407,4098,4115,120,2400,47,40,4108,4118,4106,74,198,31,3,26,25,30,155,2,27,28,92])). % 117.92/117.99 cnf(4146,plain, % 117.92/117.99 (E(f22(a1,a5),f22(x41461,f22(a1,a5)))+~E(f12(f19(f22(a1,a5))),x41462)), % 117.92/117.99 inference(scs_inference,[],[2436,2407,4098,4115,120,2400,47,40,4108,4118,4106,74,198,31,3,26,25,30,155,2,27,28,92,105])). % 117.92/117.99 cnf(4148,plain, % 117.92/117.99 (P8(f22(x41481,f22(a1,a5)),f22(a1,a5))+~E(f12(f19(f22(a1,a5))),x41482)), % 117.92/117.99 inference(scs_inference,[],[2436,2407,4098,4115,120,2400,47,40,4108,4118,4106,74,198,31,3,26,25,30,155,2,27,28,92,105,126])). % 117.92/117.99 cnf(4149,plain, % 117.92/117.99 (~E(f12(f19(f22(a1,a5))),x41491)+P1(f22(x41492,f22(a1,a5)))), % 117.92/117.99 inference(scs_inference,[],[2436,2407,4098,4115,120,2400,47,40,4108,4102,4118,4106,74,198,31,3,26,25,30,155,2,27,28,92,105,126,22])). % 117.92/117.99 cnf(4154,plain, % 117.92/117.99 (~P6(x41541,f20(f22(a1,a5)))), % 117.92/117.99 inference(equality_inference,[],[4143])). % 117.92/117.99 cnf(4155,plain, % 117.92/117.99 (E(f22(a1,a5),f22(x41551,f22(a1,a5)))), % 117.92/117.99 inference(equality_inference,[],[4146])). % 117.92/117.99 cnf(4156,plain, % 117.92/117.99 (P8(f22(x41561,f22(a1,a5)),f22(a1,a5))), % 117.92/117.99 inference(equality_inference,[],[4148])). % 117.92/117.99 cnf(4157,plain, % 117.92/117.99 (P1(f22(x41571,f22(a1,a5)))), % 117.92/117.99 inference(equality_inference,[],[4149])). % 117.92/117.99 cnf(4158,plain, % 117.92/117.99 (E(a16,f22(f21(f20(a3)),a5))), % 117.92/117.99 inference(scs_inference,[],[2407,4124])). % 117.92/117.99 cnf(4159,plain, % 117.92/117.99 (P8(f20(f22(a1,a5)),x41591)), % 117.92/117.99 inference(scs_inference,[],[4154,84])). % 117.92/117.99 cnf(4168,plain, % 117.92/117.99 (P8(f22(x41681,f22(a1,a5)),x41682)), % 117.92/117.99 inference(scs_inference,[],[4104,4099,4154,4156,4155,120,4157,84,74,2,198,31,28,27])). % 117.92/117.99 cnf(4170,plain, % 117.92/117.99 (P3(f22(f20(a1),a5))), % 117.92/117.99 inference(scs_inference,[],[4104,4099,4154,4156,4155,120,2400,40,4157,84,74,2,198,31,28,27,3,26])). % 117.92/117.99 cnf(4171,plain, % 117.92/117.99 (P4(f22(f20(a1),a5))), % 117.92/117.99 inference(scs_inference,[],[4104,4099,4154,4156,4155,120,2400,47,40,4157,84,74,2,198,31,28,27,3,26,25])). % 117.92/117.99 cnf(4179,plain, % 117.92/117.99 (~P6(x41791,f22(a1,a5))), % 117.92/117.99 inference(scs_inference,[],[4102,74])). % 117.92/117.99 cnf(4182,plain, % 117.92/117.99 (P8(f22(f21(f20(a3)),a5),x41821)), % 117.92/117.99 inference(scs_inference,[],[4158,4102,74,126,343])). % 117.92/117.99 cnf(4186,plain, % 117.92/117.99 (P3(f22(x41861,f22(a1,a5)))), % 117.92/117.99 inference(scs_inference,[],[4155,4135,4158,38,4102,74,126,343,2,198,22,26])). % 117.92/117.99 cnf(4188,plain, % 117.92/117.99 (E(a16,f22(x41881,f22(a1,a5)))), % 117.92/117.99 inference(scs_inference,[],[4098,4155,4135,4158,38,4133,4102,74,126,343,2,198,22,26,31,3])). % 117.92/117.99 cnf(4189,plain, % 117.92/117.99 (P4(f22(x41891,f22(a1,a5)))), % 117.92/117.99 inference(scs_inference,[],[4098,4155,4135,4136,4158,38,4133,4102,74,126,343,2,198,22,26,31,3,25])). % 117.92/117.99 cnf(4196,plain, % 117.92/117.99 (P8(x41961,x41962)+~E(f20(f22(a1,a5)),x41961)), % 117.92/117.99 inference(scs_inference,[],[2397,2407,4098,4155,4135,4159,4136,4158,38,4133,4132,4102,74,126,343,2,198,22,26,31,3,25,30,103,84,27])). % 117.92/117.99 cnf(4476,plain, % 117.92/117.99 (E(f22(a3,a5),f22(x44761,f22(x44762,a16)))+P6(f10(x44761,f22(a3,a5),f22(x44762,a16)),f20(f22(a3,a5)))), % 117.92/117.99 inference(scs_inference,[],[2403,2405,3167,3166,2433,3170,95])). % 117.92/117.99 cnf(4481,plain, % 117.92/117.99 (E(f22(x44811,f22(x44812,a16)),f22(a3,a5))+P6(f10(x44811,f22(a3,a5),f22(x44812,a16)),f20(f22(a3,a5)))), % 117.92/117.99 inference(scs_inference,[],[2403,2405,3167,3166,2433,3170,95,2])). % 117.92/117.99 cnf(4484,plain, % 117.92/117.99 (E(f22(a14,a5),f22(x44841,f22(x44842,a16)))+P6(f10(x44841,f22(a14,a5),f22(x44842,a16)),f20(f22(a14,a5)))), % 117.92/117.99 inference(scs_inference,[],[2403,2405,3378,3377,2433,3380,95])). % 117.92/117.99 cnf(4489,plain, % 117.92/117.99 (E(f22(x44891,f22(x44892,a16)),f22(a14,a5))+P6(f10(x44891,f22(a14,a5),f22(x44892,a16)),f20(f22(a14,a5)))), % 117.92/117.99 inference(scs_inference,[],[2403,2405,3378,3377,2433,3380,95,2])). % 117.92/117.99 cnf(4492,plain, % 117.92/117.99 (E(f22(a16,a5),f22(x44921,f22(x44922,a16)))+P6(f10(x44921,f22(a16,a5),f22(x44922,a16)),f20(f22(a16,a5)))), % 117.92/117.99 inference(scs_inference,[],[2403,2405,3424,3426,2433,3432,95])). % 117.92/117.99 cnf(4497,plain, % 117.92/117.99 (E(f22(x44971,f22(x44972,a16)),f22(a16,a5))+P6(f10(x44971,f22(a16,a5),f22(x44972,a16)),f20(f22(a16,a5)))), % 117.92/117.99 inference(scs_inference,[],[2403,2405,3424,3426,2433,3432,95,2])). % 117.92/117.99 cnf(4500,plain, % 117.92/117.99 (E(f22(a1,a5),f22(x45001,f22(x45002,a16)))+P6(f10(x45001,f22(a1,a5),f22(x45002,a16)),f20(f22(a1,a5)))), % 117.92/117.99 inference(scs_inference,[],[2403,2405,2433,4136,4135,4154,95])). % 117.92/117.99 cnf(4505,plain, % 117.92/117.99 (E(f22(x45051,f22(x45052,a16)),f22(a1,a5))+P6(f10(x45051,f22(a1,a5),f22(x45052,a16)),f20(f22(a1,a5)))), % 117.92/117.99 inference(scs_inference,[],[2403,2405,2433,4136,4135,4154,95,2])). % 117.92/117.99 cnf(4640,plain, % 117.92/117.99 (E(a16,f22(f20(f22(x46401,a16)),a7))+P6(f10(f20(f22(x46401,a16)),a16,a7),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[42,51,2433,2407,47,40,96])). % 117.92/117.99 cnf(4645,plain, % 117.92/117.99 (P8(f22(f20(f22(x46451,a16)),a7),x46452)+P6(f10(f20(f22(x46451,a16)),a16,a7),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[42,51,2433,2407,47,40,96,126,343])). % 117.92/117.99 cnf(4646,plain, % 117.92/117.99 (P2(f12(a16),f22(f20(f22(x46461,a16)),a7))+P6(f10(f20(f22(x46461,a16)),a16,a7),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[42,51,2433,2407,47,40,96,126,343,198])). % 117.92/117.99 cnf(4647,plain, % 117.92/117.99 (E(f22(f20(f22(x46471,a16)),a7),a16)+P6(f10(f20(f22(x46471,a16)),a16,a7),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[42,51,2433,2407,47,40,96,126,343,198,2])). % 117.92/117.99 cnf(4648,plain, % 117.92/117.99 (~E(f19(x46481),f22(f20(f22(x46482,a16)),a7))+P6(f10(f20(f22(x46482,a16)),a16,a7),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[42,51,2433,2407,47,40,287,96,126,343,198,2,3])). % 117.92/117.99 cnf(4649,plain, % 117.92/117.99 (P1(f22(f20(f22(x46491,a16)),a7))+P6(f10(f20(f22(x46491,a16)),a16,a7),f20(a16))), % 117.92/117.99 inference(scs_inference,[],[42,51,4158,2433,2407,923,913,47,38,40,287,96,126,343,198,2,3,29,32,30,22])). % 117.92/117.99 cnf(4653,plain, % 117.92/117.99 (~P6(x46531,f20(a16))), % 117.92/117.99 inference(rename_variables,[],[2407])). % 117.92/117.99 cnf(4655,plain, % 117.92/117.99 (~P6(x46551,f20(a16))), % 117.92/117.99 inference(rename_variables,[],[2407])). % 117.92/117.99 cnf(4657,plain, % 117.92/117.99 (~P6(x46571,f20(a16))), % 117.92/117.99 inference(rename_variables,[],[2407])). % 117.92/117.99 cnf(4658,plain, % 117.92/117.99 (P1(f22(f20(f22(x46581,a16)),a7))), % 117.92/117.99 inference(scs_inference,[],[2407,4653,4655,4657,4645,4646,4648,4649])). % 117.92/117.99 cnf(4675,plain, % 117.92/117.99 (E(f22(x46751,a16),f22(f20(a16),a7))+P6(f10(f20(a16),f22(x46751,a16),a7),f20(f22(x46751,a16)))), % 117.92/117.99 inference(scs_inference,[],[42,51,2405,2433,2407,2403,96])). % 117.92/117.99 cnf(4680,plain, % 117.92/117.99 (P8(f22(f20(a16),a7),f22(x46801,a16))+P6(f10(f20(a16),f22(x46801,a16),a7),f20(f22(x46801,a16)))), % 117.92/117.99 inference(scs_inference,[],[42,51,2405,2433,2407,2403,96,126])). % 117.92/117.99 cnf(4681,plain, % 117.92/117.99 (P2(f12(f22(x46811,a16)),f22(f20(a16),a7))+P6(f10(f20(a16),f22(x46811,a16),a7),f20(f22(x46811,a16)))), % 117.92/117.99 inference(scs_inference,[],[42,51,2405,2433,2407,2403,96,126,198])). % 117.92/117.99 cnf(4682,plain, % 117.92/117.99 (E(f22(f20(a16),a7),f22(x46821,a16))+P6(f10(f20(a16),f22(x46821,a16),a7),f20(f22(x46821,a16)))), % 117.92/117.99 inference(scs_inference,[],[42,51,2405,2433,2407,2403,96,126,198,2])). % 117.92/117.99 cnf(4686,plain, % 117.92/117.99 (E(f22(x46861,a16),f22(f20(a16),a7))), % 117.92/117.99 inference(scs_inference,[],[2433,4675])). % 117.92/117.99 cnf(4687,plain, % 117.92/117.99 (~P6(x46871,f20(f22(x46872,a16)))), % 117.92/117.99 inference(rename_variables,[],[2433])). % 117.92/117.99 cnf(4690,plain, % 117.92/117.99 (~P6(x46901,f20(f22(x46902,a16)))), % 117.92/117.99 inference(rename_variables,[],[2433])). % 117.92/117.99 cnf(4692,plain, % 117.92/117.99 (P2(f12(f22(x46921,a16)),f22(f20(a16),a7))), % 117.92/117.99 inference(scs_inference,[],[2433,4687,4690,4675,4680,4681])). % 117.92/117.99 cnf(4693,plain, % 117.92/117.99 (~P6(x46931,f20(f22(x46932,a16)))), % 117.92/117.99 inference(rename_variables,[],[2433])). % 117.92/117.99 cnf(4695,plain, % 117.92/117.99 (E(f22(f20(a16),a7),f22(x46951,a16))), % 117.92/117.99 inference(scs_inference,[],[2433,4687,4690,4693,4675,4680,4681,4682])). % 117.92/117.99 cnf(4699,plain, % 117.92/117.99 (E(a16,f22(f20(a16),a7))), % 117.92/117.99 inference(scs_inference,[],[2397,2433,4687,4690,4693,4675,4680,4681,4682,198,3])). % 117.92/117.99 cnf(4700,plain, % 117.92/117.99 (P1(f22(f20(a16),a7))), % 117.92/117.99 inference(scs_inference,[],[2397,2433,4687,4690,4693,2402,4675,4680,4681,4682,198,3,22])). % 117.92/117.99 cnf(4701,plain, % 117.92/117.99 (P3(f22(f20(a16),a7))), % 117.92/117.99 inference(scs_inference,[],[2397,2405,2433,4687,4690,4693,2402,4675,4680,4681,4682,198,3,22,26])). % 117.92/117.99 cnf(4703,plain, % 117.92/117.99 (P4(f22(f20(a16),a7))), % 117.92/117.99 inference(scs_inference,[],[2397,2405,2433,4687,4690,4693,2403,2402,2406,4675,4680,4681,4682,198,3,22,26,31,25])). % 117.92/117.99 cnf(4705,plain, % 117.92/117.99 (~P6(x47051,f20(f22(f20(a16),a7)))), % 117.92/117.99 inference(scs_inference,[],[42,51,2397,2405,3745,2433,4687,4690,4693,2407,2403,2402,2406,4675,4680,4681,4682,198,3,22,26,31,25,28,103])). % 117.92/117.99 cnf(4712,plain, % 117.92/117.99 (P8(f22(f20(a16),a7),x47121)), % 117.92/117.99 inference(scs_inference,[],[42,51,2397,2405,3745,2433,4687,4690,4693,2407,2403,2402,2406,4675,4680,4681,4682,198,3,22,26,31,25,28,103,84,74,343])). % 117.92/117.99 cnf(4713,plain, % 117.92/117.99 (E(f22(f20(a16),a7),a16)), % 117.92/117.99 inference(scs_inference,[],[42,51,2397,2405,3745,2433,4687,4690,4693,2407,2403,2402,2406,4675,4680,4681,4682,198,3,22,26,31,25,28,103,84,74,343,2])). % 117.92/117.99 cnf(4736,plain, % 117.92/117.99 (P2(f12(a16),f22(f20(a16),a7))), % 117.92/117.99 inference(scs_inference,[],[4699,198])). % 117.92/117.99 cnf(4739,plain, % 117.92/117.99 (P2(x47391,f22(f20(a16),a7))+~E(f12(f22(x47392,a16)),x47391)), % 117.92/117.99 inference(scs_inference,[],[2404,4692,4695,4699,198,3,29])). % 117.92/117.99 cnf(4753,plain, % 117.92/117.99 (P2(x47531,f22(f20(a16),a7))+~E(f12(a16),x47531)), % 117.92/117.99 inference(scs_inference,[],[4736,29])). % 117.92/117.99 cnf(4767,plain, % 117.92/117.99 (E(f22(x47671,a16),f22(f20(f22(a3,a5)),a7))+P6(f10(f20(f22(a3,a5)),f22(x47671,a16),a7),f20(f22(x47671,a16)))), % 117.92/117.99 inference(scs_inference,[],[42,51,2405,2433,3170,2403,96])). % 117.92/117.99 cnf(4772,plain, % 117.92/117.99 (P8(f22(f20(f22(a3,a5)),a7),f22(x47721,a16))+P6(f10(f20(f22(a3,a5)),f22(x47721,a16),a7),f20(f22(x47721,a16)))), % 117.92/117.99 inference(scs_inference,[],[42,51,2405,2433,3170,2403,96,126])). % 117.92/117.99 cnf(4773,plain, % 117.92/117.99 (E(f22(f20(f22(a3,a5)),a7),f22(x47731,a16))+P6(f10(f20(f22(a3,a5)),f22(x47731,a16),a7),f20(f22(x47731,a16)))), % 117.92/117.99 inference(scs_inference,[],[42,51,2405,2433,3170,2403,96,126,2])). % 117.92/117.99 cnf(4774,plain, % 117.92/117.99 (E(a16,f22(f20(f22(a3,a5)),a7))+P6(f10(f20(f22(a3,a5)),f22(x47741,a16),a7),f20(f22(x47741,a16)))), % 117.92/117.99 inference(scs_inference,[],[42,51,2397,2405,2433,3170,2403,96,126,2,3])). % 117.92/117.99 cnf(4776,plain, % 117.92/117.99 (P1(f22(f20(f22(a3,a5)),a7))+P6(f10(f20(f22(a3,a5)),f22(x47761,a16),a7),f20(f22(x47761,a16)))), % 117.92/117.99 inference(scs_inference,[],[42,51,2397,2405,2433,3170,2403,550,2402,96,126,2,3,73,22])). % 117.92/117.99 cnf(4779,plain, % 117.92/117.99 (P1(f22(f20(f22(a3,a5)),a7))), % 117.92/117.99 inference(scs_inference,[],[2433,4776])). % 117.92/117.99 cnf(4780,plain, % 117.92/117.99 (~P6(x47801,f20(f22(x47802,a16)))), % 117.92/117.99 inference(rename_variables,[],[2433])). % 117.92/117.99 cnf(4784,plain, % 117.92/117.99 (E(f22(x47841,a16),f22(f20(f22(a14,a5)),a7))+P6(f10(f20(f22(a14,a5)),f22(x47841,a16),a7),f20(f22(x47841,a16)))), % 117.92/117.99 inference(scs_inference,[],[42,51,2405,2433,4780,3380,2403,4776,74,96])). % 117.92/117.99 cnf(4789,plain, % 117.92/117.99 (P8(f22(f20(f22(a14,a5)),a7),f22(x47891,a16))+P6(f10(f20(f22(a14,a5)),f22(x47891,a16),a7),f20(f22(x47891,a16)))), % 117.92/117.99 inference(scs_inference,[],[42,51,2405,2433,4780,3380,2403,4776,74,96,126])). % 117.92/117.99 cnf(4790,plain, % 117.92/117.99 (E(f22(f20(f22(a14,a5)),a7),f22(x47901,a16))+P6(f10(f20(f22(a14,a5)),f22(x47901,a16),a7),f20(f22(x47901,a16)))), % 117.92/117.99 inference(scs_inference,[],[42,51,2405,2433,4780,3380,2403,4776,74,96,126,2])). % 117.92/117.99 cnf(4791,plain, % 117.92/117.99 (E(a16,f22(f20(f22(a14,a5)),a7))+P6(f10(f20(f22(a14,a5)),f22(x47911,a16),a7),f20(f22(x47911,a16)))), % 117.92/117.99 inference(scs_inference,[],[42,51,2397,2405,2433,4780,3380,2403,4776,74,96,126,2,3])). % 117.92/117.99 cnf(4793,plain, % 117.92/117.99 (P1(f22(f20(f22(a14,a5)),a7))+P6(f10(f20(f22(a14,a5)),f22(x47931,a16),a7),f20(f22(x47931,a16)))), % 117.92/117.99 inference(scs_inference,[],[42,51,2397,2405,2433,4780,3380,2403,550,2402,4776,74,96,126,2,3,73,22])). % 117.92/117.99 cnf(4796,plain, % 117.92/117.99 (P1(f22(f20(f22(a14,a5)),a7))), % 117.92/117.99 inference(scs_inference,[],[2433,4793])). % 117.92/117.99 cnf(4797,plain, % 117.92/117.99 (~P6(x47971,f20(f22(x47972,a16)))), % 117.92/117.99 inference(rename_variables,[],[2433])). % 117.92/117.99 cnf(4801,plain, % 117.92/117.99 (E(f22(x48011,a16),f22(f20(f22(a16,a5)),a7))+P6(f10(f20(f22(a16,a5)),f22(x48011,a16),a7),f20(f22(x48011,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2405,2433,4797,3432,2403,4793,74,96])). % 117.92/118.00 cnf(4806,plain, % 117.92/118.00 (P8(f22(f20(f22(a16,a5)),a7),f22(x48061,a16))+P6(f10(f20(f22(a16,a5)),f22(x48061,a16),a7),f20(f22(x48061,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2405,2433,4797,3432,2403,4793,74,96,126])). % 117.92/118.00 cnf(4807,plain, % 117.92/118.00 (E(f22(f20(f22(a16,a5)),a7),f22(x48071,a16))+P6(f10(f20(f22(a16,a5)),f22(x48071,a16),a7),f20(f22(x48071,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2405,2433,4797,3432,2403,4793,74,96,126,2])). % 117.92/118.00 cnf(4809,plain, % 117.92/118.00 (E(a16,f22(f20(f22(a16,a5)),a7))+P6(f10(f20(f22(a16,a5)),f22(x48091,a16),a7),f20(f22(x48091,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2397,2405,2433,4797,3432,2403,550,4793,74,96,126,2,73,3])). % 117.92/118.00 cnf(4811,plain, % 117.92/118.00 (P1(f22(f20(f22(a16,a5)),a7))+P6(f10(f20(f22(a16,a5)),f22(x48111,a16),a7),f20(f22(x48111,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2397,2405,2433,4797,3432,2403,913,550,2402,4793,74,96,126,2,73,3,87,22])). % 117.92/118.00 cnf(4814,plain, % 117.92/118.00 (P1(f22(f20(f22(a16,a5)),a7))), % 117.92/118.00 inference(scs_inference,[],[2433,4811])). % 117.92/118.00 cnf(4815,plain, % 117.92/118.00 (~P6(x48151,f20(f22(x48152,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(4819,plain, % 117.92/118.00 (E(f22(x48191,a16),f22(f20(f22(a1,a5)),a7))+P6(f10(f20(f22(a1,a5)),f22(x48191,a16),a7),f20(f22(x48191,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2405,2433,4815,4154,2403,4811,74,96])). % 117.92/118.00 cnf(4824,plain, % 117.92/118.00 (P8(f22(f20(f22(a1,a5)),a7),f22(x48241,a16))+P6(f10(f20(f22(a1,a5)),f22(x48241,a16),a7),f20(f22(x48241,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2405,2433,4815,4154,2403,4811,74,96,126])). % 117.92/118.00 cnf(4825,plain, % 117.92/118.00 (E(f22(f20(f22(a1,a5)),a7),f22(x48251,a16))+P6(f10(f20(f22(a1,a5)),f22(x48251,a16),a7),f20(f22(x48251,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2405,2433,4815,4154,2403,4811,74,96,126,2])). % 117.92/118.00 cnf(4827,plain, % 117.92/118.00 (E(a16,f22(f20(f22(a1,a5)),a7))+P6(f10(f20(f22(a1,a5)),f22(x48271,a16),a7),f20(f22(x48271,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2397,2405,2433,4815,4154,2403,550,4811,74,96,126,2,73,3])). % 117.92/118.00 cnf(4829,plain, % 117.92/118.00 (P1(f22(f20(f22(a1,a5)),a7))+P6(f10(f20(f22(a1,a5)),f22(x48291,a16),a7),f20(f22(x48291,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2397,2405,2433,4815,4154,2403,913,2996,550,2402,4811,74,96,126,2,73,3,65,87,22])). % 117.92/118.00 cnf(4831,plain, % 117.92/118.00 (P1(f22(f20(f22(a1,a5)),a7))), % 117.92/118.00 inference(scs_inference,[],[2433,4829])). % 117.92/118.00 cnf(4832,plain, % 117.92/118.00 (~P6(x48321,f20(f22(x48322,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(4842,plain, % 117.92/118.00 (E(f22(f12(f19(a16)),a7),f22(x48421,a16))+P6(f10(f12(f19(a16)),f22(x48421,a16),a7),f20(f22(x48421,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2405,2433,4832,2403,214,4829,74,96,126,2])). % 117.92/118.00 cnf(4844,plain, % 117.92/118.00 (E(a16,f22(f12(f19(a16)),a7))+P6(f10(f12(f19(a16)),f22(x48441,a16),a7),f20(f22(x48441,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2397,2405,2433,4832,2403,550,214,4829,74,96,126,2,73,3])). % 117.92/118.00 cnf(4846,plain, % 117.92/118.00 (P1(f22(f12(f19(a16)),a7))+P6(f10(f12(f19(a16)),f22(x48461,a16),a7),f20(f22(x48461,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2397,2405,2433,4832,2403,913,2996,550,214,504,2402,4829,74,96,126,2,73,3,87,65,26,22])). % 117.92/118.00 cnf(4849,plain, % 117.92/118.00 (~P6(x48491,f20(f22(x48492,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(4852,plain, % 117.92/118.00 (~P6(x48521,f20(f22(x48522,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(4864,plain, % 117.92/118.00 (E(f22(x48641,a16),f22(f12(f19(a3)),a7))+P6(f10(f12(f19(a3)),f22(x48641,a16),a7),f20(f22(x48641,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2405,2433,4849,4852,2403,4705,4701,4703,359,246,2404,2406,4842,4846,219,74,2,3,26,31,25,32,71,101,96])). % 117.92/118.00 cnf(4893,plain, % 117.92/118.00 (E(f22(x48931,a16),f22(f18(x48932),a7))+P6(f10(f18(x48932),f22(x48931,a16),a7),f20(f22(x48931,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2405,2433,2403,184,96])). % 117.92/118.00 cnf(4898,plain, % 117.92/118.00 (P2(f12(f22(x48981,a16)),f22(f18(x48982),a7))+P6(f10(f18(x48982),f22(x48981,a16),a7),f20(f22(x48981,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2405,2433,2403,184,96,198])). % 117.92/118.00 cnf(4899,plain, % 117.92/118.00 (P8(f22(f18(x48991),a7),f22(x48992,a16))+P6(f10(f18(x48991),f22(x48992,a16),a7),f20(f22(x48992,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2405,2433,2403,184,96,198,126])). % 117.92/118.00 cnf(4900,plain, % 117.92/118.00 (E(f22(f18(x49001),a7),f22(x49002,a16))+P6(f10(f18(x49001),f22(x49002,a16),a7),f20(f22(x49002,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2405,2433,2403,184,96,198,126,2])). % 117.92/118.00 cnf(4902,plain, % 117.92/118.00 (E(a16,f22(f18(x49021),a7))+P6(f10(f18(x49021),f22(x49022,a16),a7),f20(f22(x49022,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2397,2405,2433,2403,550,184,96,198,126,2,73,3])). % 117.92/118.00 cnf(4904,plain, % 117.92/118.00 (P1(f22(f18(x49041),a7))+P6(f10(f18(x49041),f22(x49042,a16),a7),f20(f22(x49042,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2397,2405,2433,2403,913,2996,550,184,504,2402,96,198,126,2,73,3,65,87,26,22])). % 117.92/118.00 cnf(4911,plain, % 117.92/118.00 (P8(f12(f19(f22(x49111,a16))),f22(a14,a7))+P6(f10(a14,f22(x49111,a16),a7),f20(f22(x49111,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2405,2433,2403,162,96,155])). % 117.92/118.00 cnf(4912,plain, % 117.92/118.00 (P2(f12(f22(x49121,a16)),f22(a14,a7))+P6(f10(a14,f22(x49121,a16),a7),f20(f22(x49121,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2405,2433,2403,162,96,155,198])). % 117.92/118.00 cnf(4913,plain, % 117.92/118.00 (P8(f22(a14,a7),f22(x49131,a16))+P6(f10(a14,f22(x49131,a16),a7),f20(f22(x49131,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2405,2433,2403,162,96,155,198,126])). % 117.92/118.00 cnf(4914,plain, % 117.92/118.00 (E(f22(a14,a7),f22(x49141,a16))+P6(f10(a14,f22(x49141,a16),a7),f20(f22(x49141,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2405,2433,2403,162,96,155,198,126,2])). % 117.92/118.00 cnf(4916,plain, % 117.92/118.00 (E(a16,f22(a14,a7))+P6(f10(a14,f22(x49161,a16),a7),f20(f22(x49161,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2397,2405,2433,2403,550,162,96,155,198,126,2,73,3])). % 117.92/118.00 cnf(4918,plain, % 117.92/118.00 (P1(f22(a14,a7))+P6(f10(a14,f22(x49181,a16),a7),f20(f22(x49181,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,51,2397,2405,2433,2403,913,2996,550,162,2402,96,155,198,126,2,73,3,65,30,22])). % 117.92/118.00 cnf(4921,plain, % 117.92/118.00 (P8(f12(f19(f22(x49211,a16))),f22(a14,a7))), % 117.92/118.00 inference(scs_inference,[],[2433,4911])). % 117.92/118.00 cnf(4922,plain, % 117.92/118.00 (~P6(x49221,f20(f22(x49222,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(4924,plain, % 117.92/118.00 (P2(f12(f22(x49241,a16)),f22(a14,a7))), % 117.92/118.00 inference(scs_inference,[],[2433,4922,4911,4912])). % 117.92/118.00 cnf(4925,plain, % 117.92/118.00 (~P6(x49251,f20(f22(x49252,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(4928,plain, % 117.92/118.00 (~P6(x49281,f20(f22(x49282,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(4930,plain, % 117.92/118.00 (E(f22(a14,a7),f22(x49301,a16))), % 117.92/118.00 inference(scs_inference,[],[2433,4922,4925,4928,4911,4912,4913,4914])). % 117.92/118.00 cnf(4931,plain, % 117.92/118.00 (~P6(x49311,f20(f22(x49312,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(4933,plain, % 117.92/118.00 (P1(f22(a14,a7))), % 117.92/118.00 inference(scs_inference,[],[2433,4922,4925,4928,4931,4911,4912,4913,4914,4918])). % 117.92/118.00 cnf(4934,plain, % 117.92/118.00 (~P6(x49341,f20(f22(x49342,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(4936,plain, % 117.92/118.00 (P8(f12(f19(f22(a14,a7))),f22(x49361,a16))), % 117.92/118.00 inference(scs_inference,[],[2433,4922,4925,4928,4931,4911,4912,4913,4914,4918,155])). % 117.92/118.00 cnf(4937,plain, % 117.92/118.00 (~P6(x49371,f22(a14,a7))), % 117.92/118.00 inference(scs_inference,[],[2433,4922,4925,4928,4931,4911,4912,4913,4914,4918,155,74])). % 117.92/118.00 cnf(4940,plain, % 117.92/118.00 (E(f22(x49401,a16),f22(a14,a7))), % 117.92/118.00 inference(scs_inference,[],[2433,4922,4925,4928,4931,4911,4912,4913,4914,4918,155,74,198,2])). % 117.92/118.00 cnf(4942,plain, % 117.92/118.00 (P5(f22(a14,a7))), % 117.92/118.00 inference(scs_inference,[],[2433,4922,4925,4928,4931,2404,2406,4911,4912,4913,4914,4918,155,74,198,2,3,31])). % 117.92/118.00 cnf(4944,plain, % 117.92/118.00 (P3(f22(a14,a7))), % 117.92/118.00 inference(scs_inference,[],[3745,2405,2433,4922,4925,4928,4931,2404,2406,4911,4912,4913,4914,4918,155,74,198,2,3,31,30,26])). % 117.92/118.00 cnf(4947,plain, % 117.92/118.00 (P4(f22(a14,a7))), % 117.92/118.00 inference(scs_inference,[],[3745,2405,2433,4922,4925,4928,4931,2403,2404,2406,4911,4912,4913,4914,4918,155,74,198,2,3,31,30,26,28,25])). % 117.92/118.00 cnf(4948,plain, % 117.92/118.00 (~P6(x49481,f20(f22(a14,a7)))), % 117.92/118.00 inference(scs_inference,[],[3745,2405,2433,4922,4925,4928,4931,4934,2403,47,40,2404,2406,4911,4912,4913,4914,4918,155,74,198,2,3,31,30,26,28,25,92])). % 117.92/118.00 cnf(4951,plain, % 117.92/118.00 (E(f22(a14,a7),f22(x49511,f22(a14,a7)))), % 117.92/118.00 inference(scs_inference,[],[3745,2405,2433,4922,4925,4928,4931,4934,2403,47,40,2404,2406,4911,4912,4913,4914,4918,155,74,198,2,3,31,30,26,28,25,92,105])). % 117.92/118.00 cnf(4954,plain, % 117.92/118.00 (P8(f22(a14,a7),x49541)), % 117.92/118.00 inference(scs_inference,[],[3745,2405,2433,4922,4925,4928,4931,4934,2403,47,40,2404,2406,4911,4912,4913,4914,4918,155,74,198,2,3,31,30,26,28,25,92,105,219,84])). % 117.92/118.00 cnf(4956,plain, % 117.92/118.00 (P8(f22(x49561,f22(a14,a7)),f22(a14,a7))), % 117.92/118.00 inference(scs_inference,[],[3745,2405,2433,4922,4925,4928,4931,4934,2403,47,40,2404,2406,4911,4912,4913,4914,4918,155,74,198,2,3,31,30,26,28,25,92,105,219,84,126])). % 117.92/118.00 cnf(4957,plain, % 117.92/118.00 (P1(f22(x49571,f22(a14,a7)))), % 117.92/118.00 inference(scs_inference,[],[3745,2405,2433,4922,4925,4928,4931,4934,2403,47,40,2404,2406,4911,4912,4913,4914,4918,155,74,198,2,3,31,30,26,28,25,92,105,219,84,126,22])). % 117.92/118.00 cnf(4965,plain, % 117.92/118.00 (P8(f20(f22(a14,a7)),x49651)), % 117.92/118.00 inference(scs_inference,[],[4948,84])). % 117.92/118.00 cnf(4971,plain, % 117.92/118.00 (E(f22(x49711,f22(a14,a7)),f22(a14,a7))), % 117.92/118.00 inference(scs_inference,[],[4948,4951,4957,84,74,198,2])). % 117.92/118.00 cnf(4972,plain, % 117.92/118.00 (E(f22(x49721,a16),f22(x49722,f22(a14,a7)))), % 117.92/118.00 inference(scs_inference,[],[4948,4951,4957,4940,84,74,198,2,3])). % 117.92/118.00 cnf(4975,plain, % 117.92/118.00 (P3(f22(x49751,f22(a14,a7)))), % 117.92/118.00 inference(scs_inference,[],[4948,4951,4944,4957,4942,4924,4940,84,74,198,2,3,31,30,26])). % 117.92/118.00 cnf(4977,plain, % 117.92/118.00 (P8(f22(x49771,f22(a14,a7)),x49772)), % 117.92/118.00 inference(scs_inference,[],[4948,4954,4956,4951,4944,4957,4942,4924,4940,84,74,198,2,3,31,30,26,28,27])). % 117.92/118.00 cnf(4978,plain, % 117.92/118.00 (P4(f22(x49781,f22(a14,a7)))), % 117.92/118.00 inference(scs_inference,[],[4948,4954,4956,4951,4944,4947,4957,4942,4924,4940,84,74,198,2,3,31,30,26,28,27,25])). % 117.92/118.00 cnf(4989,plain, % 117.92/118.00 (E(f22(x49891,f22(a14,a7)),f22(x49892,a16))), % 117.92/118.00 inference(scs_inference,[],[4971,4972,198,2])). % 117.92/118.00 cnf(4996,plain, % 117.92/118.00 (P2(f12(f22(x49961,f22(a14,a7))),f22(x49962,a16))), % 117.92/118.00 inference(scs_inference,[],[4989,198])). % 117.92/118.00 cnf(5064,plain, % 117.92/118.00 (P8(x50641,x50642)+~E(f20(f22(a14,a7)),x50641)), % 117.92/118.00 inference(scs_inference,[],[4965,4971,4996,32,29,27])). % 117.92/118.00 cnf(5070,plain, % 117.92/118.00 (P1(f20(f22(a14,a7)))), % 117.92/118.00 inference(scs_inference,[],[4933,66])). % 117.92/118.00 cnf(5072,plain, % 117.92/118.00 (P1(f21(f22(a14,a7)))), % 117.92/118.00 inference(scs_inference,[],[4933,66,67])). % 117.92/118.00 cnf(5074,plain, % 117.92/118.00 (P4(f20(f22(a14,a7)))), % 117.92/118.00 inference(scs_inference,[],[4933,66,67,68])). % 117.92/118.00 cnf(5076,plain, % 117.92/118.00 (P4(f21(f22(a14,a7)))), % 117.92/118.00 inference(scs_inference,[],[4933,66,67,68,69])). % 117.92/118.00 cnf(5078,plain, % 117.92/118.00 (~P1(f15(f15(a17)))), % 117.92/118.00 inference(scs_inference,[],[4933,620,66,67,68,69,70])). % 117.92/118.00 cnf(5080,plain, % 117.92/118.00 (P4(f22(x50801,f20(a1)))), % 117.92/118.00 inference(scs_inference,[],[505,4933,620,66,67,68,69,70,77])). % 117.92/118.00 cnf(5084,plain, % 117.92/118.00 (P2(f15(f15(a17)),f19(f15(a17)))), % 117.92/118.00 inference(scs_inference,[],[505,4921,4933,620,66,67,68,69,70,77,79,75])). % 117.92/118.00 cnf(5105,plain, % 117.92/118.00 (E(a16,f22(f18(x51051),a5))), % 117.92/118.00 inference(scs_inference,[],[505,4921,4933,4686,620,2407,66,67,68,69,70,77,79,75,4,5,8,12,19,89,6,7,17,18,20,21,9,10,11,14,15,16,4051])). % 117.92/118.00 cnf(5106,plain, % 117.92/118.00 (~P6(x51061,f20(a16))), % 117.92/118.00 inference(rename_variables,[],[2407])). % 117.92/118.00 cnf(5107,plain, % 117.92/118.00 (P1(f22(f18(x51071),a7))), % 117.92/118.00 inference(scs_inference,[],[505,4921,4933,4686,620,2433,2407,66,67,68,69,70,77,79,75,4,5,8,12,19,89,6,7,17,18,20,21,9,10,11,14,15,16,4051,4904])). % 117.92/118.00 cnf(5108,plain, % 117.92/118.00 (~P6(x51081,f20(f22(x51082,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5110,plain, % 117.92/118.00 (E(a16,f22(a14,a7))), % 117.92/118.00 inference(scs_inference,[],[505,4921,4933,4686,620,2433,5108,2407,66,67,68,69,70,77,79,75,4,5,8,12,19,89,6,7,17,18,20,21,9,10,11,14,15,16,4051,4904,4916])). % 117.92/118.00 cnf(5111,plain, % 117.92/118.00 (~P6(x51111,f20(f22(x51112,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5113,plain, % 117.92/118.00 (E(f22(x51131,a16),f22(x51132,a16))), % 117.92/118.00 inference(scs_inference,[],[505,4921,4933,4686,620,2433,5108,5111,2407,66,67,68,69,70,77,79,75,4,5,8,12,19,89,6,7,17,18,20,21,9,10,11,14,15,16,4051,4904,4916,2551])). % 117.92/118.00 cnf(5114,plain, % 117.92/118.00 (~P6(x51141,f20(f22(x51142,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5116,plain, % 117.92/118.00 (E(a16,f22(f18(x51161),a7))), % 117.92/118.00 inference(scs_inference,[],[505,4921,4933,4686,620,2433,5108,5111,5114,2407,66,67,68,69,70,77,79,75,4,5,8,12,19,89,6,7,17,18,20,21,9,10,11,14,15,16,4051,4904,4916,2551,4902])). % 117.92/118.00 cnf(5117,plain, % 117.92/118.00 (~P6(x51171,f20(f22(x51172,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5120,plain, % 117.92/118.00 (~P6(x51201,f20(a16))), % 117.92/118.00 inference(rename_variables,[],[2407])). % 117.92/118.00 cnf(5122,plain, % 117.92/118.00 (~P6(x51221,f20(a16))), % 117.92/118.00 inference(rename_variables,[],[2407])). % 117.92/118.00 cnf(5124,plain, % 117.92/118.00 (~P6(x51241,f20(a16))), % 117.92/118.00 inference(rename_variables,[],[2407])). % 117.92/118.00 cnf(5126,plain, % 117.92/118.00 (~P6(x51261,f20(a16))), % 117.92/118.00 inference(rename_variables,[],[2407])). % 117.92/118.00 cnf(5128,plain, % 117.92/118.00 (~P6(x51281,f20(a16))), % 117.92/118.00 inference(rename_variables,[],[2407])). % 117.92/118.00 cnf(5132,plain, % 117.92/118.00 (~P6(x51321,f20(f22(x51322,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5134,plain, % 117.92/118.00 (P8(f22(f18(x51341),a7),f22(x51342,a16))), % 117.92/118.00 inference(scs_inference,[],[505,4921,4933,4686,620,2433,5108,5111,5114,5117,5132,2407,5106,5120,5122,5124,5126,5128,66,67,68,69,70,77,79,75,4,5,8,12,19,89,6,7,17,18,20,21,9,10,11,14,15,16,4051,4904,4916,2551,4902,2940,2945,3104,3109,4640,4647,4893,4899])). % 117.92/118.00 cnf(5135,plain, % 117.92/118.00 (~P6(x51351,f20(f22(x51352,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5137,plain, % 117.92/118.00 (E(f22(f18(x51371),a7),f22(x51372,a16))), % 117.92/118.00 inference(scs_inference,[],[505,4921,4933,4686,620,2433,5108,5111,5114,5117,5132,5135,2407,5106,5120,5122,5124,5126,5128,66,67,68,69,70,77,79,75,4,5,8,12,19,89,6,7,17,18,20,21,9,10,11,14,15,16,4051,4904,4916,2551,4902,2940,2945,3104,3109,4640,4647,4893,4899,4900])). % 117.92/118.00 cnf(5138,plain, % 117.92/118.00 (~P6(x51381,f20(f22(x51382,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5141,plain, % 117.92/118.00 (~P6(x51411,f20(f22(x51412,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5144,plain, % 117.92/118.00 (~P6(x51441,f20(f22(x51442,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5146,plain, % 117.92/118.00 (E(f22(a3,a5),f22(x51461,f22(x51462,a16)))), % 117.92/118.00 inference(scs_inference,[],[505,4921,4933,4686,3170,620,2433,5108,5111,5114,5117,5132,5135,5138,5141,2407,5106,5120,5122,5124,5126,5128,66,67,68,69,70,77,79,75,4,5,8,12,19,89,6,7,17,18,20,21,9,10,11,14,15,16,4051,4904,4916,2551,4902,2940,2945,3104,3109,4640,4647,4893,4899,4900,4898,4844,4476])). % 117.92/118.00 cnf(5147,plain, % 117.92/118.00 (~P6(x51471,f20(f22(a3,a5)))), % 117.92/118.00 inference(rename_variables,[],[3170])). % 117.92/118.00 cnf(5148,plain, % 117.92/118.00 (E(f22(x51481,f22(x51482,a16)),f22(a3,a5))), % 117.92/118.00 inference(scs_inference,[],[505,4921,4933,4686,3170,5147,620,2433,5108,5111,5114,5117,5132,5135,5138,5141,2407,5106,5120,5122,5124,5126,5128,66,67,68,69,70,77,79,75,4,5,8,12,19,89,6,7,17,18,20,21,9,10,11,14,15,16,4051,4904,4916,2551,4902,2940,2945,3104,3109,4640,4647,4893,4899,4900,4898,4844,4476,4481])). % 117.92/118.00 cnf(5151,plain, % 117.92/118.00 (~P6(x51511,f20(f22(a14,a5)))), % 117.92/118.00 inference(rename_variables,[],[3380])). % 117.92/118.00 cnf(5155,plain, % 117.92/118.00 (~P6(x51551,f20(f22(a16,a5)))), % 117.92/118.00 inference(rename_variables,[],[3432])). % 117.92/118.00 cnf(5159,plain, % 117.92/118.00 (~P6(x51591,f20(f22(a1,a5)))), % 117.92/118.00 inference(rename_variables,[],[4154])). % 117.92/118.00 cnf(5163,plain, % 117.92/118.00 (~P6(x51631,f20(f22(x51632,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5166,plain, % 117.92/118.00 (~P6(x51661,f20(f22(x51662,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5169,plain, % 117.92/118.00 (~P6(x51691,f20(f22(x51692,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5172,plain, % 117.92/118.00 (~P6(x51721,f20(f22(x51722,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5175,plain, % 117.92/118.00 (~P6(x51751,f20(f22(x51752,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5178,plain, % 117.92/118.00 (~P6(x51781,f20(f22(x51782,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5181,plain, % 117.92/118.00 (~P6(x51811,f20(f22(x51812,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5184,plain, % 117.92/118.00 (~P6(x51841,f20(f22(x51842,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5187,plain, % 117.92/118.00 (~P6(x51871,f20(f22(x51872,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5190,plain, % 117.92/118.00 (~P6(x51901,f20(f22(x51902,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5193,plain, % 117.92/118.00 (~P6(x51931,f20(f22(x51932,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5196,plain, % 117.92/118.00 (~P6(x51961,f20(f22(x51962,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5199,plain, % 117.92/118.00 (~P6(x51991,f20(f22(x51992,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5202,plain, % 117.92/118.00 (~P6(x52021,f20(f22(x52022,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5205,plain, % 117.92/118.00 (~P6(x52051,f20(f22(x52052,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5208,plain, % 117.92/118.00 (~P6(x52081,f20(f22(x52082,a16)))), % 117.92/118.00 inference(rename_variables,[],[2433])). % 117.92/118.00 cnf(5213,plain, % 117.92/118.00 (E(f22(a14,a7),a1)), % 117.92/118.00 inference(scs_inference,[],[505,4921,4933,4686,4154,5159,3170,5147,620,3432,5155,3380,5151,2433,5108,5111,5114,5117,5132,5135,5138,5141,5144,5163,5166,5169,5172,5175,5178,5181,5184,5187,5190,5193,5196,5199,5202,5205,5208,2407,5106,5120,5122,5124,5126,5128,66,67,68,69,70,77,79,75,4,5,8,12,19,89,6,7,17,18,20,21,9,10,11,14,15,16,4051,4904,4916,2551,4902,2940,2945,3104,3109,4640,4647,4893,4899,4900,4898,4844,4476,4481,4484,4489,4492,4497,4500,4505,4864,4774,4791,4809,4827,4767,4772,4773,4784,4789,4790,4801,4806,4807,4819,4824,4825,62])). % 117.92/118.00 cnf(5224,plain, % 117.92/118.00 (~P1(f20(a17))), % 117.92/118.00 inference(scs_inference,[],[505,827,4978,4921,4933,4975,4779,4686,4154,5159,3170,5147,620,3432,5155,3380,5151,59,2433,5108,5111,5114,5117,5132,5135,5138,5141,5144,5163,5166,5169,5172,5175,5178,5181,5184,5187,5190,5193,5196,5199,5202,5205,5208,48,2407,5106,5120,5122,5124,5126,5128,66,67,68,69,70,77,79,75,4,5,8,12,19,89,6,7,17,18,20,21,9,10,11,14,15,16,4051,4904,4916,2551,4902,2940,2945,3104,3109,4640,4647,4893,4899,4900,4898,4844,4476,4481,4484,4489,4492,4497,4500,4505,4864,4774,4791,4809,4827,4767,4772,4773,4784,4789,4790,4801,4806,4807,4819,4824,4825,62,64,63,13,2,80,72])). % 117.92/118.00 cnf(5226,plain, % 117.92/118.00 (~P6(x52261,f12(f19(f22(x52262,a16))))), % 117.92/118.00 inference(scs_inference,[],[505,827,4978,4921,4937,4933,4975,4779,4686,4154,5159,3170,5147,620,3432,5155,3380,5151,59,2433,5108,5111,5114,5117,5132,5135,5138,5141,5144,5163,5166,5169,5172,5175,5178,5181,5184,5187,5190,5193,5196,5199,5202,5205,5208,48,2407,5106,5120,5122,5124,5126,5128,66,67,68,69,70,77,79,75,4,5,8,12,19,89,6,7,17,18,20,21,9,10,11,14,15,16,4051,4904,4916,2551,4902,2940,2945,3104,3109,4640,4647,4893,4899,4900,4898,4844,4476,4481,4484,4489,4492,4497,4500,4505,4864,4774,4791,4809,4827,4767,4772,4773,4784,4789,4790,4801,4806,4807,4819,4824,4825,62,64,63,13,2,80,72,85])). % 117.92/118.00 cnf(5228,plain, % 117.92/118.00 (~P2(f19(f20(a1)),f19(f22(a14,a7)))), % 117.92/118.00 inference(scs_inference,[],[505,827,4978,4921,4937,4933,4975,4779,914,4686,4154,5159,3170,5147,620,3432,5155,3380,5151,59,2433,5108,5111,5114,5117,5132,5135,5138,5141,5144,5163,5166,5169,5172,5175,5178,5181,5184,5187,5190,5193,5196,5199,5202,5205,5208,48,2407,5106,5120,5122,5124,5126,5128,66,67,68,69,70,77,79,75,4,5,8,12,19,89,6,7,17,18,20,21,9,10,11,14,15,16,4051,4904,4916,2551,4902,2940,2945,3104,3109,4640,4647,4893,4899,4900,4898,4844,4476,4481,4484,4489,4492,4497,4500,4505,4864,4774,4791,4809,4827,4767,4772,4773,4784,4789,4790,4801,4806,4807,4819,4824,4825,62,64,63,13,2,80,72,85,86])). % 117.92/118.00 cnf(5232,plain, % 117.92/118.00 (P6(f12(f19(a14)),f19(x52321))), % 117.92/118.00 inference(scs_inference,[],[505,827,4978,4921,4937,4933,4975,4779,914,4686,885,192,4154,5159,3170,5147,620,3432,5155,3380,5151,61,59,2433,5108,5111,5114,5117,5132,5135,5138,5141,5144,5163,5166,5169,5172,5175,5178,5181,5184,5187,5190,5193,5196,5199,5202,5205,5208,48,2407,5106,5120,5122,5124,5126,5128,66,67,68,69,70,77,79,75,4,5,8,12,19,89,6,7,17,18,20,21,9,10,11,14,15,16,4051,4904,4916,2551,4902,2940,2945,3104,3109,4640,4647,4893,4899,4900,4898,4844,4476,4481,4484,4489,4492,4497,4500,4505,4864,4774,4791,4809,4827,4767,4772,4773,4784,4789,4790,4801,4806,4807,4819,4824,4825,62,64,63,13,2,80,72,85,86,24,78])). % 117.92/118.00 cnf(5235,plain, % 117.92/118.00 (~P1(f21(a17))), % 117.92/118.00 inference(scs_inference,[],[505,827,4978,4921,4937,4933,4975,4779,914,4686,885,192,4154,5159,3170,5147,620,3432,5155,3380,5151,61,59,2433,5108,5111,5114,5117,5132,5135,5138,5141,5144,5163,5166,5169,5172,5175,5178,5181,5184,5187,5190,5193,5196,5199,5202,5205,5208,48,2407,5106,5120,5122,5124,5126,5128,66,67,68,69,70,77,79,75,4,5,8,12,19,89,6,7,17,18,20,21,9,10,11,14,15,16,4051,4904,4916,2551,4902,2940,2945,3104,3109,4640,4647,4893,4899,4900,4898,4844,4476,4481,4484,4489,4492,4497,4500,4505,4864,4774,4791,4809,4827,4767,4772,4773,4784,4789,4790,4801,4806,4807,4819,4824,4825,62,64,63,13,2,80,72,85,86,24,78,73])). % 117.92/118.00 cnf(5237,plain, % 117.92/118.00 (~E(f22(a14,a7),f15(a17))), % 117.92/118.00 inference(scs_inference,[],[505,827,4978,4921,4937,4933,4975,4779,914,4686,885,192,4154,5159,3170,5147,620,3432,5155,3380,5151,61,59,2433,5108,5111,5114,5117,5132,5135,5138,5141,5144,5163,5166,5169,5172,5175,5178,5181,5184,5187,5190,5193,5196,5199,5202,5205,5208,48,2407,5106,5120,5122,5124,5126,5128,66,67,68,69,70,77,79,75,4,5,8,12,19,89,6,7,17,18,20,21,9,10,11,14,15,16,4051,4904,4916,2551,4902,2940,2945,3104,3109,4640,4647,4893,4899,4900,4898,4844,4476,4481,4484,4489,4492,4497,4500,4505,4864,4774,4791,4809,4827,4767,4772,4773,4784,4789,4790,4801,4806,4807,4819,4824,4825,62,64,63,13,2,80,72,85,86,24,78,73,22])). % 117.92/118.00 cnf(5264,plain, % 117.92/118.00 (P2(f15(f20(a17)),f19(f20(a17)))), % 117.92/118.00 inference(scs_inference,[],[5224,5134,79,75])). % 117.92/118.00 cnf(5266,plain, % 117.92/118.00 (P8(f21(f22(x52661,a8)),f21(a8))), % 117.92/118.00 inference(scs_inference,[],[5224,5134,50,79,75,89])). % 117.92/118.00 cnf(5270,plain, % 117.92/118.00 (P1(f20(f21(f22(a14,a7))))), % 117.92/118.00 inference(scs_inference,[],[5113,5224,5134,5072,50,79,75,89,9,7,66])). % 117.92/118.00 cnf(5272,plain, % 117.92/118.00 (E(f18(f22(x52721,a16)),f18(f22(x52722,a16)))), % 117.92/118.00 inference(scs_inference,[],[5113,5224,5134,5072,50,79,75,89,9,7,66,4])). % 117.92/118.00 cnf(5275,plain, % 117.92/118.00 (P4(f21(f21(f22(a14,a7))))), % 117.92/118.00 inference(scs_inference,[],[5113,5224,5134,5072,50,79,75,89,9,7,66,4,19,5,69])). % 117.92/118.00 cnf(5279,plain, % 117.92/118.00 (P1(f21(f21(f22(a14,a7))))), % 117.92/118.00 inference(scs_inference,[],[5113,5224,5134,5072,50,79,75,89,9,7,66,4,19,5,69,20,18,67])). % 117.92/118.00 cnf(5284,plain, % 117.92/118.00 (~P1(f15(f20(a17)))), % 117.92/118.00 inference(scs_inference,[],[5113,5224,5134,5072,50,79,75,89,9,7,66,4,19,5,69,20,18,67,68,17,70])). % 117.92/118.00 cnf(5288,plain, % 117.92/118.00 (E(f21(f22(a14,a7)),a1)), % 117.92/118.00 inference(scs_inference,[],[5113,5224,5134,432,5072,50,79,75,89,9,7,66,4,19,5,69,20,18,67,68,17,70,77,62])). % 117.92/118.00 cnf(5299,plain, % 117.92/118.00 (P4(f22(f18(x52991),a7))), % 117.92/118.00 inference(scs_inference,[],[5113,5224,5134,432,5072,5107,50,79,75,89,9,7,66,4,19,5,69,20,18,67,68,17,70,77,62,14,21,11,8,16,6,10,12,15,64])). % 117.92/118.00 cnf(5301,plain, % 117.92/118.00 (P3(f21(f22(a14,a7)))), % 117.92/118.00 inference(scs_inference,[],[5113,5224,5134,432,5072,5107,50,79,75,89,9,7,66,4,19,5,69,20,18,67,68,17,70,77,62,14,21,11,8,16,6,10,12,15,64,63])). % 117.92/118.00 cnf(5304,plain, % 117.92/118.00 (~E(f15(a17),f22(a14,a7))), % 117.92/118.00 inference(scs_inference,[],[5237,5113,5224,5134,432,5072,5107,50,79,75,89,9,7,66,4,19,5,69,20,18,67,68,17,70,77,62,14,21,11,8,16,6,10,12,15,64,63,13,2])). % 117.92/118.00 cnf(5305,plain, % 117.92/118.00 (P3(f22(x53051,a7))), % 117.92/118.00 inference(scs_inference,[],[42,5237,5113,5224,5134,432,5072,5107,50,51,79,75,89,9,7,66,4,19,5,69,20,18,67,68,17,70,77,62,14,21,11,8,16,6,10,12,15,64,63,13,2,80])). % 117.92/118.00 cnf(5312,plain, % 117.92/118.00 (P1(f12(f19(f22(x53121,a16))))), % 117.92/118.00 inference(scs_inference,[],[42,5237,5113,5224,5232,5134,432,5072,5107,5226,2426,57,50,51,79,75,89,9,7,66,4,19,5,69,20,18,67,68,17,70,77,62,14,21,11,8,16,6,10,12,15,64,63,13,2,80,85,86,78])). % 117.92/118.00 cnf(5313,plain, % 117.92/118.00 (~P6(x53131,f12(f19(f22(x53132,a16))))), % 117.92/118.00 inference(rename_variables,[],[5226])). % 117.92/118.00 cnf(5318,plain, % 117.92/118.00 (~E(f21(f22(a14,a7)),f20(a17))), % 117.92/118.00 inference(scs_inference,[],[42,5237,5113,5224,5232,5134,432,5072,5107,5226,5313,2426,57,50,51,79,75,89,9,7,66,4,19,5,69,20,18,67,68,17,70,77,62,14,21,11,8,16,6,10,12,15,64,63,13,2,80,85,86,78,24,22])). % 117.92/118.00 cnf(5319,plain, % 117.92/118.00 (~E(a1,f15(a17))), % 117.92/118.00 inference(scs_inference,[],[42,5237,5113,5224,5213,5232,5134,432,5072,5107,5226,5313,2426,57,50,51,79,75,89,9,7,66,4,19,5,69,20,18,67,68,17,70,77,62,14,21,11,8,16,6,10,12,15,64,63,13,2,80,85,86,78,24,22,3])). % 117.92/118.00 cnf(5320,plain, % 117.92/118.00 (P5(a1)), % 117.92/118.00 inference(scs_inference,[],[42,5237,5113,5224,5213,5232,5134,432,5072,5107,5226,5313,2426,4942,57,50,51,79,75,89,9,7,66,4,19,5,69,20,18,67,68,17,70,77,62,14,21,11,8,16,6,10,12,15,64,63,13,2,80,85,86,78,24,22,3,31])). % 117.92/118.00 cnf(5321,plain, % 117.92/118.00 (P2(f22(x53211,a16),f19(f22(x53212,a16)))), % 117.92/118.00 inference(scs_inference,[],[42,5237,5113,5224,5213,5232,5134,5137,432,5072,5107,5226,5313,2426,4942,57,50,51,79,75,89,9,7,66,4,19,5,69,20,18,67,68,17,70,77,62,14,21,11,8,16,6,10,12,15,64,63,13,2,80,85,86,78,24,22,3,31,29])). % 117.92/118.00 cnf(5323,plain, % 117.92/118.00 (~P6(x53231,f20(f22(f18(x53232),a7)))), % 117.92/118.00 inference(scs_inference,[],[42,5237,5113,5224,5213,5232,5134,5137,432,5072,5107,5226,5313,2426,4942,184,57,50,51,79,75,89,9,7,66,4,19,5,69,20,18,67,68,17,70,77,62,14,21,11,8,16,6,10,12,15,64,63,13,2,80,85,86,78,24,22,3,31,29,103])). % 117.92/118.00 cnf(5330,plain, % 117.92/118.00 (~P6(f19(a17),f15(f15(a17)))), % 117.92/118.00 inference(scs_inference,[],[42,5237,5113,5224,5213,5232,5134,5137,432,5072,5107,5084,5226,5313,2426,4942,184,57,50,840,51,79,75,89,9,7,66,4,19,5,69,20,18,67,68,17,70,77,62,14,21,11,8,16,6,10,12,15,64,63,13,2,80,85,86,78,24,22,3,31,29,103,891,156,72,87])). % 117.92/118.00 cnf(5337,plain, % 117.92/118.00 (P5(f20(a1))), % 117.92/118.00 inference(scs_inference,[],[5320,524])). % 117.92/118.00 cnf(5345,plain, % 117.92/118.00 (~P1(f15(f21(a17)))), % 117.92/118.00 inference(scs_inference,[],[5235,5266,5070,79,69,70])). % 117.92/118.00 cnf(5349,plain, % 117.92/118.00 (P2(f15(f21(a17)),f19(f21(a17)))), % 117.92/118.00 inference(scs_inference,[],[5235,5266,5070,79,69,70,67,75])). % 117.92/118.00 cnf(5352,plain, % 117.92/118.00 (E(f20(f22(a14,a7)),a1)), % 117.92/118.00 inference(scs_inference,[],[5235,5266,5070,5288,79,69,70,67,75,4,62])). % 117.92/118.00 cnf(5356,plain, % 117.92/118.00 (P8(f21(f22(x53561,a3)),f21(a3))), % 117.92/118.00 inference(scs_inference,[],[5235,5266,5070,5288,46,79,69,70,67,75,4,62,68,89])). % 117.92/118.00 cnf(5360,plain, % 117.92/118.00 (E(f12(f21(f22(a14,a7))),f12(a1))), % 117.92/118.00 inference(scs_inference,[],[5235,5266,5070,5074,5288,46,79,69,70,67,75,4,62,68,89,77,5])). % 117.92/118.00 cnf(5372,plain, % 117.92/118.00 (E(f22(f21(f22(a14,a7)),x53721),f22(a1,x53721))), % 117.92/118.00 inference(scs_inference,[],[5235,5266,5070,5074,5288,5312,46,79,69,70,67,75,4,62,68,89,77,5,19,66,11,14,9,20,21,7,64,17])). % 117.92/118.00 cnf(5374,plain, % 117.92/118.00 (E(f2(f21(f22(a14,a7)),x53741),f2(a1,x53741))), % 117.92/118.00 inference(scs_inference,[],[5235,5266,5070,5074,5288,5312,46,79,69,70,67,75,4,62,68,89,77,5,19,66,11,14,9,20,21,7,64,17,18,6])). % 117.92/118.00 cnf(5376,plain, % 117.92/118.00 (P3(f20(f22(a14,a7)))), % 117.92/118.00 inference(scs_inference,[],[5235,5266,5070,5074,5288,5312,46,79,69,70,67,75,4,62,68,89,77,5,19,66,11,14,9,20,21,7,64,17,18,6,16,63])). % 117.92/118.00 cnf(5380,plain, % 117.92/118.00 (E(f20(f21(f22(a14,a7))),f20(a1))), % 117.92/118.00 inference(scs_inference,[],[5235,5266,5070,5074,5288,5312,46,79,69,70,67,75,4,62,68,89,77,5,19,66,11,14,9,20,21,7,64,17,18,6,16,63,8,15,12])). % 117.92/118.00 cnf(5386,plain, % 117.92/118.00 (~P6(x53861,f12(f19(f22(a1,a5))))), % 117.92/118.00 inference(scs_inference,[],[5235,5318,5266,5070,5074,5288,5312,4109,46,209,79,69,70,67,75,4,62,68,89,77,5,19,66,11,14,9,20,21,7,64,17,18,6,16,63,8,15,12,10,13,2,80,85])). % 117.92/118.00 cnf(5390,plain, % 117.92/118.00 (P6(f22(x53901,a16),f19(f22(x53902,a16)))), % 117.92/118.00 inference(scs_inference,[],[5235,5318,5266,5070,5074,5321,5288,5312,922,4109,61,46,209,79,69,70,67,75,4,62,68,89,77,5,19,66,11,14,9,20,21,7,64,17,18,6,16,63,8,15,12,10,13,2,80,85,86,78])). % 117.92/118.00 cnf(5393,plain, % 117.92/118.00 (~P6(x53931,f21(f22(a14,a7)))), % 117.92/118.00 inference(scs_inference,[],[5235,5318,5266,5070,5074,5321,5288,5312,922,4109,61,46,209,111,79,69,70,67,75,4,62,68,89,77,5,19,66,11,14,9,20,21,7,64,17,18,6,16,63,8,15,12,10,13,2,80,85,86,78,24])). % 117.92/118.00 cnf(5394,plain, % 117.92/118.00 (~E(f20(f22(a14,a7)),f21(a17))), % 117.92/118.00 inference(scs_inference,[],[5235,5318,5266,5070,5074,5321,5288,5312,922,4109,61,46,209,111,79,69,70,67,75,4,62,68,89,77,5,19,66,11,14,9,20,21,7,64,17,18,6,16,63,8,15,12,10,13,2,80,85,86,78,24,22])). % 117.92/118.00 cnf(5396,plain, % 117.92/118.00 (P4(f21(a1))), % 117.92/118.00 inference(scs_inference,[],[5235,5148,5318,5266,5070,5074,5321,5288,5275,5312,5146,922,4109,61,46,209,111,79,69,70,67,75,4,62,68,89,77,5,19,66,11,14,9,20,21,7,64,17,18,6,16,63,8,15,12,10,13,2,80,85,86,78,24,22,3,25])). % 117.92/118.00 cnf(5400,plain, % 117.92/118.00 (P2(f18(f22(x54001,a16)),f19(f22(x54002,a16)))), % 117.92/118.00 inference(scs_inference,[],[5235,5148,5318,5266,5070,5074,5321,5288,5272,5275,5312,5146,922,4109,61,58,46,209,111,79,69,70,67,75,4,62,68,89,77,5,19,66,11,14,9,20,21,7,64,17,18,6,16,63,8,15,12,10,13,2,80,85,86,78,24,22,3,25,156,1381,29])). % 117.92/118.00 cnf(5407,plain, % 117.92/118.00 (E(f20(f21(f22(a14,a7))),a1)), % 117.92/118.00 inference(scs_inference,[],[5356,5270,79,62])). % 117.92/118.00 cnf(5409,plain, % 117.92/118.00 (P8(f21(f22(x54091,a5)),f21(a5))), % 117.92/118.00 inference(scs_inference,[],[5356,5270,49,79,62,89])). % 117.92/118.00 cnf(5413,plain, % 117.92/118.00 (P4(f22(x54131,f21(a1)))), % 117.92/118.00 inference(scs_inference,[],[5396,5356,5270,4700,49,79,62,89,68,77])). % 117.92/118.00 cnf(5417,plain, % 117.92/118.00 (P1(f21(f22(f20(a16),a7)))), % 117.92/118.00 inference(scs_inference,[],[5396,5356,5270,4700,49,79,62,89,68,77,66,67])). % 117.92/118.00 cnf(5421,plain, % 117.92/118.00 (~P1(f15(f15(f15(a17))))), % 117.92/118.00 inference(scs_inference,[],[5396,5356,5078,5270,4700,49,79,62,89,68,77,66,67,69,70])). % 117.92/118.00 cnf(5423,plain, % 117.92/118.00 (P2(f15(a6),f19(a6))), % 117.92/118.00 inference(scs_inference,[],[5396,5356,5078,5270,4700,60,49,79,62,89,68,77,66,67,69,70,75])). % 117.92/118.00 cnf(5445,plain, % 117.92/118.00 (E(f20(f20(f22(a14,a7))),f20(a1))), % 117.92/118.00 inference(scs_inference,[],[5396,5356,5078,5352,5270,4796,4700,60,49,79,62,89,68,77,66,67,69,70,75,9,11,5,64,4,17,19,7,21,20,14,16,6,63,18,15,10,8,12])). % 117.92/118.00 cnf(5452,plain, % 117.92/118.00 (~E(f19(f22(x54521,a16)),f21(f22(a14,a7)))), % 117.92/118.00 inference(scs_inference,[],[5396,5394,5356,5393,5301,5390,5078,5330,5352,5270,4796,4700,5076,60,49,79,62,89,68,77,66,67,69,70,75,9,11,5,64,4,17,19,7,21,20,14,16,6,63,18,15,10,8,12,13,2,80,78,24])). % 117.92/118.00 cnf(5454,plain, % 117.92/118.00 (~E(f20(f21(f22(a14,a7))),f20(a17))), % 117.92/118.00 inference(scs_inference,[],[5396,5394,5356,5393,5301,5390,5078,5330,5352,5270,4796,4700,5076,5224,60,49,79,62,89,68,77,66,67,69,70,75,9,11,5,64,4,17,19,7,21,20,14,16,6,63,18,15,10,8,12,13,2,80,78,24,22])). % 117.92/118.00 cnf(5455,plain, % 117.92/118.00 (~E(f20(a1),f15(a17))), % 117.92/118.00 inference(scs_inference,[],[5396,5319,5394,5356,5393,5301,5390,5078,5330,5352,5270,4796,4700,5076,5224,60,504,49,79,62,89,68,77,66,67,69,70,75,9,11,5,64,4,17,19,7,21,20,14,16,6,63,18,15,10,8,12,13,2,80,78,24,22,3])). % 117.92/118.00 cnf(5474,plain, % 117.92/118.00 (P1(f21(f22(f20(a16),a5)))), % 117.92/118.00 inference(scs_inference,[],[5409,5413,5417,3757,62,79,68,66,77,69,67])). % 117.92/118.00 cnf(5476,plain, % 117.92/118.00 (P8(f21(f22(x54761,a17)),f21(a17))), % 117.92/118.00 inference(scs_inference,[],[5409,5413,5417,3757,48,62,79,68,66,77,69,67,89])). % 117.92/118.00 cnf(5478,plain, % 117.92/118.00 (~P1(f15(f15(f20(a17))))), % 117.92/118.00 inference(scs_inference,[],[5409,5413,5284,5417,3757,48,62,79,68,66,77,69,67,89,70])). % 117.92/118.00 cnf(5480,plain, % 117.92/118.00 (P2(f15(f19(x54801)),f19(f19(x54801)))), % 117.92/118.00 inference(scs_inference,[],[5409,5413,5284,5417,3757,61,48,62,79,68,66,77,69,67,89,70,75])). % 117.92/118.00 cnf(5482,plain, % 117.92/118.00 (E(f10(a16,x54821,x54822),f10(f22(a14,a7),x54821,x54822))), % 117.92/118.00 inference(scs_inference,[],[5409,5413,5284,5417,5110,3757,61,48,62,79,68,66,77,69,67,89,70,75,9])). % 117.92/118.00 cnf(5485,plain, % 117.92/118.00 (E(f10(x54851,x54852,a16),f10(x54851,x54852,f22(a14,a7)))), % 117.92/118.00 inference(scs_inference,[],[5409,5413,5284,5417,5110,4831,3757,61,48,62,79,68,66,77,69,67,89,70,75,9,64,11])). % 117.92/118.00 cnf(5490,plain, % 117.92/118.00 (E(f12(a16),f12(f22(a14,a7)))), % 117.92/118.00 inference(scs_inference,[],[5409,5413,5284,5417,5110,4831,3757,61,48,62,79,68,66,77,69,67,89,70,75,9,64,11,63,20,19,5])). % 117.92/118.00 cnf(5498,plain, % 117.92/118.00 (E(f19(a16),f19(f22(a14,a7)))), % 117.92/118.00 inference(scs_inference,[],[5409,5413,5284,5417,5110,4831,3757,61,48,62,79,68,66,77,69,67,89,70,75,9,64,11,63,20,19,5,14,7,17,4,21,6,16,8])). % 117.92/118.00 cnf(5502,plain, % 117.92/118.00 (E(f10(x55021,a16,x55022),f10(x55021,f22(a14,a7),x55022))), % 117.92/118.00 inference(scs_inference,[],[5409,5413,5284,5417,5110,5105,4831,3757,61,48,62,79,68,66,77,69,67,89,70,75,9,64,11,63,20,19,5,14,7,17,4,21,6,16,8,18,15,12,10])). % 117.92/118.00 cnf(5503,plain, % 117.92/118.00 (E(f21(a16),f21(f22(a14,a7)))), % 117.92/118.00 inference(scs_inference,[],[5409,5413,5284,5417,5110,5105,4831,3757,61,48,62,79,68,66,77,69,67,89,70,75,9,64,11,63,20,19,5,14,7,17,4,21,6,16,8,18,15,12,10,13])). % 117.92/118.00 cnf(5504,plain, % 117.92/118.00 (~E(f15(a17),f20(a1))), % 117.92/118.00 inference(scs_inference,[],[5455,5409,5413,5284,5417,5110,5105,4831,3757,61,48,62,79,68,66,77,69,67,89,70,75,9,64,11,63,20,19,5,14,7,17,4,21,6,16,8,18,15,12,10,13,2])). % 117.92/118.00 cnf(5508,plain, % 117.92/118.00 (P6(f15(a6),f19(a6))), % 117.92/118.00 inference(scs_inference,[],[5423,5455,5409,5413,5284,5299,5417,5305,5110,5105,4831,3757,61,48,62,79,68,66,77,69,67,89,70,75,9,64,11,63,20,19,5,14,7,17,4,21,6,16,8,18,15,12,10,13,2,80,78])). % 117.92/118.00 cnf(5511,plain, % 117.92/118.00 (~P6(x55111,f20(f21(f22(a14,a7))))), % 117.92/118.00 inference(scs_inference,[],[5423,5455,5409,5413,5284,5299,5380,5417,5305,5110,5105,4831,3757,61,48,510,62,79,68,66,77,69,67,89,70,75,9,64,11,63,20,19,5,14,7,17,4,21,6,16,8,18,15,12,10,13,2,80,78,24])). % 117.92/118.00 cnf(5513,plain, % 117.92/118.00 (~E(f20(a1),f20(a17))), % 117.92/118.00 inference(scs_inference,[],[5423,5455,5409,5413,5284,5299,5380,5454,5417,5305,5110,5105,4831,3757,61,48,510,62,79,68,66,77,69,67,89,70,75,9,64,11,63,20,19,5,14,7,17,4,21,6,16,8,18,15,12,10,13,2,80,78,24,22,3])). % 117.92/118.00 cnf(5514,plain, % 117.92/118.00 (~P2(f19(f20(a1)),f19(a16))), % 117.92/118.00 inference(scs_inference,[],[5423,5455,5409,5413,5284,5299,5380,5454,5417,5305,5110,5105,5228,4831,3757,61,48,510,62,79,68,66,77,69,67,89,70,75,9,64,11,63,20,19,5,14,7,17,4,21,6,16,8,18,15,12,10,13,2,80,78,24,22,3,30])). % 117.92/118.00 cnf(5515,plain, % 117.92/118.00 (P2(f12(a1),f21(f22(a14,a7)))), % 117.92/118.00 inference(scs_inference,[],[5423,5455,5409,5413,5284,5299,5360,5380,5454,5417,5305,5110,5105,5228,4831,3757,61,57,48,510,62,79,68,66,77,69,67,89,70,75,9,64,11,63,20,19,5,14,7,17,4,21,6,16,8,18,15,12,10,13,2,80,78,24,22,3,30,29])). % 117.92/118.00 cnf(5536,plain, % 117.92/118.00 (P8(f21(f22(x55361,a16)),f21(a16))), % 117.92/118.00 inference(scs_inference,[],[5476,5474,5107,47,79,62,66,68,89])). % 117.92/118.00 cnf(5544,plain, % 117.92/118.00 (~P1(f15(f15(f21(a17))))), % 117.92/118.00 inference(scs_inference,[],[5476,5345,5474,5107,4978,47,79,62,66,68,89,69,67,77,70])). % 117.92/118.00 cnf(5559,plain, % 117.92/118.00 (E(f2(a16,x55591),f2(f22(f18(x55592),a7),x55591))), % 117.92/118.00 inference(scs_inference,[],[5476,5345,5474,5116,4814,5107,4978,47,79,62,66,68,89,69,67,77,70,64,9,63,5,17,11,19,14,4,20,7,6])). % 117.92/118.00 cnf(5568,plain, % 117.92/118.00 (~E(f20(a17),f20(a1))), % 117.92/118.00 inference(scs_inference,[],[5513,5476,5345,5474,5116,4814,5107,4978,47,79,62,66,68,89,69,67,77,70,64,9,63,5,17,11,19,14,4,20,7,6,16,21,12,18,8,10,15,13,2])). % 117.92/118.00 cnf(5571,plain, % 117.92/118.00 (P1(f12(f19(f22(a1,a5))))), % 117.92/118.00 inference(scs_inference,[],[5513,5476,5345,5474,5386,5116,4814,5107,4978,4171,4170,57,47,79,62,66,68,89,69,67,77,70,64,9,63,5,17,11,19,14,4,20,7,6,16,21,12,18,8,10,15,13,2,80,78])). % 117.92/118.00 cnf(5573,plain, % 117.92/118.00 (P2(f12(x55731),x55731)), % 117.92/118.00 inference(rename_variables,[],[57])). % 117.92/118.00 cnf(5577,plain, % 117.92/118.00 (~E(f21(f22(f20(a16),a5)),f21(a17))), % 117.92/118.00 inference(scs_inference,[],[5508,5513,5476,5345,5474,5511,5386,5116,4814,5107,4978,4171,4170,5235,57,47,79,62,66,68,89,69,67,77,70,64,9,63,5,17,11,19,14,4,20,7,6,16,21,12,18,8,10,15,13,2,80,78,24,22])). % 117.92/118.00 cnf(5578,plain, % 117.92/118.00 (~E(f15(a17),f22(x55781,a16))), % 117.92/118.00 inference(scs_inference,[],[5304,5508,5513,5476,5345,5474,5511,5386,5116,4814,5107,4978,4171,4170,4940,5235,57,47,79,62,66,68,89,69,67,77,70,64,9,63,5,17,11,19,14,4,20,7,6,16,21,12,18,8,10,15,13,2,80,78,24,22,3])). % 117.92/118.00 cnf(5579,plain, % 117.92/118.00 (P2(f12(f10(a16,x55791,x55792)),f10(f22(a14,a7),x55791,x55792))), % 117.92/118.00 inference(scs_inference,[],[5304,5508,5513,5476,5482,5345,5474,5511,5386,5116,4814,5107,4978,4171,4170,4940,5235,57,5573,47,79,62,66,68,89,69,67,77,70,64,9,63,5,17,11,19,14,4,20,7,6,16,21,12,18,8,10,15,13,2,80,78,24,22,3,30])). % 117.92/118.00 cnf(5587,plain, % 117.92/118.00 (P2(f21(f22(x55871,a16)),f19(f21(a16)))), % 117.92/118.00 inference(scs_inference,[],[5536,5279,62,79])). % 117.92/118.00 cnf(5591,plain, % 117.92/118.00 (P4(f21(f22(x55911,f22(a14,a7))))), % 117.92/118.00 inference(scs_inference,[],[5536,5279,4957,62,79,68,69])). % 117.92/118.00 cnf(5595,plain, % 117.92/118.00 (P1(f21(f22(x55951,f22(a14,a7))))), % 117.92/118.00 inference(scs_inference,[],[5536,5279,5080,4957,62,79,68,69,77,67])). % 117.92/118.00 cnf(5597,plain, % 117.92/118.00 (P1(f20(f22(x55971,f22(a14,a7))))), % 117.92/118.00 inference(scs_inference,[],[5536,5279,5080,4957,62,79,68,69,77,67,66])). % 117.92/118.00 cnf(5599,plain, % 117.92/118.00 (P8(f21(f22(x55991,a4)),f21(a4))), % 117.92/118.00 inference(scs_inference,[],[5536,5279,5080,4957,45,62,79,68,69,77,67,66,89])). % 117.92/118.00 cnf(5601,plain, % 117.92/118.00 (~P1(f15(a6))), % 117.92/118.00 inference(scs_inference,[],[5536,5279,5080,4957,60,45,62,79,68,69,77,67,66,89,70])). % 117.92/118.00 cnf(5603,plain, % 117.92/118.00 (P2(f15(f15(a6)),f19(f15(a6)))), % 117.92/118.00 inference(scs_inference,[],[5536,5279,5080,4957,60,45,62,79,68,69,77,67,66,89,70,75])). % 117.92/118.00 cnf(5631,plain, % 117.92/118.00 (P6(f15(f19(x56311)),f19(f19(x56311)))), % 117.92/118.00 inference(scs_inference,[],[5578,5536,5480,5279,5571,5080,5105,4957,4930,3193,3191,60,61,45,62,79,68,69,77,67,66,89,70,75,63,9,64,14,5,17,4,7,19,11,6,20,21,16,12,15,8,18,10,13,2,80,78])). % 117.92/118.00 cnf(5634,plain, % 117.92/118.00 (~P6(x56341,f21(a16))), % 117.92/118.00 inference(scs_inference,[],[5578,5536,5503,5480,5279,5571,5080,5393,5105,4957,4930,3193,3191,60,61,45,62,79,68,69,77,67,66,89,70,75,63,9,64,14,5,17,4,7,19,11,6,20,21,16,12,15,8,18,10,13,2,80,78,24])). % 117.92/118.00 cnf(5635,plain, % 117.92/118.00 (P3(a1)), % 117.92/118.00 inference(scs_inference,[],[5578,5536,5376,5503,5480,5279,5571,5080,5393,5105,4957,4930,3193,3191,60,61,5352,45,62,79,68,69,77,67,66,89,70,75,63,9,64,14,5,17,4,7,19,11,6,20,21,16,12,15,8,18,10,13,2,80,78,24,26])). % 117.92/118.00 cnf(5638,plain, % 117.92/118.00 (P8(f10(x56381,x56382,f22(a14,a7)),f10(x56381,x56382,a16))), % 117.92/118.00 inference(scs_inference,[],[5578,5536,5376,5485,5503,5480,5279,5571,5421,5080,5393,5105,4957,4930,507,3193,3191,56,60,61,5352,45,62,79,68,69,77,67,66,89,70,75,63,9,64,14,5,17,4,7,19,11,6,20,21,16,12,15,8,18,10,13,2,80,78,24,26,22,28,27])). % 117.92/118.00 cnf(5643,plain, % 117.92/118.00 (E(a1,f22(x56431,a1))), % 117.92/118.00 inference(scs_inference,[],[5578,5536,5376,5485,5502,5503,5480,5279,5571,5421,5080,5393,5105,4957,4930,507,3193,3191,56,60,61,5352,45,510,44,62,79,68,69,77,67,66,89,70,75,63,9,64,14,5,17,4,7,19,11,6,20,21,16,12,15,8,18,10,13,2,80,78,24,26,22,28,27,3,105])). % 117.92/118.00 cnf(5644,plain, % 117.92/118.00 (~P6(x56441,f20(a1))), % 117.92/118.00 inference(rename_variables,[],[510])). % 117.92/118.00 cnf(5645,plain, % 117.92/118.00 (~P6(x56451,f20(a1))), % 117.92/118.00 inference(rename_variables,[],[510])). % 117.92/118.00 cnf(5651,plain, % 117.92/118.00 (~P6(x56511,f21(f22(x56512,a16)))), % 117.92/118.00 inference(scs_inference,[],[5578,5536,5376,5485,5502,5503,5480,5279,5571,5421,5080,5393,5105,4957,4930,507,5396,3193,3191,56,60,61,5352,45,510,44,62,79,68,69,77,67,66,89,70,75,63,9,64,14,5,17,4,7,19,11,6,20,21,16,12,15,8,18,10,13,2,80,78,24,26,22,28,27,3,105,82,72,85])). % 117.92/118.00 cnf(5654,plain, % 117.92/118.00 (~P6(x56541,f20(f22(f18(x56542),a7)))), % 117.92/118.00 inference(rename_variables,[],[5323])). % 117.92/118.00 cnf(5656,plain, % 117.92/118.00 (P4(f22(f18(x56561),a7))), % 117.92/118.00 inference(rename_variables,[],[5299])). % 117.92/118.00 cnf(5657,plain, % 117.92/118.00 (P3(f22(x56571,a7))), % 117.92/118.00 inference(rename_variables,[],[5305])). % 117.92/118.00 cnf(5660,plain, % 117.92/118.00 (E(a1,f22(x56601,f22(f18(x56602),a7)))), % 117.92/118.00 inference(scs_inference,[],[5578,5536,5376,5485,5502,5503,5480,5279,5571,5421,5559,5323,5654,5080,5305,5657,5299,5656,5393,5105,4957,4930,507,5396,3193,3191,56,60,61,5352,40,47,45,2407,510,5645,5644,44,62,79,68,69,77,67,66,89,70,75,63,9,64,14,5,17,4,7,19,11,6,20,21,16,12,15,8,18,10,13,2,80,78,24,26,22,28,27,3,105,82,72,85,97,95])). % 117.92/118.00 cnf(5668,plain, % 117.92/118.00 (P3(f20(a1))), % 117.92/118.00 inference(scs_inference,[],[5635,518])). % 117.92/118.00 cnf(5672,plain, % 117.92/118.00 (P2(f10(x56721,x56722,f22(a14,a7)),f19(f10(x56721,x56722,a16)))), % 117.92/118.00 inference(scs_inference,[],[5638,79])). % 117.92/118.00 cnf(5678,plain, % 117.92/118.00 (P8(f21(f22(x56781,a1)),f21(a1))), % 117.92/118.00 inference(scs_inference,[],[5638,5595,4157,44,79,62,69,89])). % 117.92/118.00 cnf(5680,plain, % 117.92/118.00 (P1(f21(f22(x56801,f22(a1,a5))))), % 117.92/118.00 inference(scs_inference,[],[5638,5595,4157,44,79,62,69,89,67])). % 117.92/118.00 cnf(5688,plain, % 117.92/118.00 (~P1(f15(f15(a6)))), % 117.92/118.00 inference(scs_inference,[],[5601,5638,5595,4157,5299,44,79,62,69,89,67,66,68,77,70])). % 117.92/118.00 cnf(5694,plain, % 117.92/118.00 (E(f10(a1,x56941,x56942),f10(f22(x56943,a1),x56941,x56942))), % 117.92/118.00 inference(scs_inference,[],[5601,5643,5638,5595,4658,4157,5299,44,79,62,69,89,67,66,68,77,70,63,64,9])). % 117.92/118.00 cnf(5696,plain, % 117.92/118.00 (E(f18(a1),f18(f22(x56961,a1)))), % 117.92/118.00 inference(scs_inference,[],[5601,5643,5638,5595,4658,4157,5299,44,79,62,69,89,67,66,68,77,70,63,64,9,11,4])). % 117.92/118.00 cnf(5697,plain, % 117.92/118.00 (E(f2(a1,x56971),f2(f22(x56972,a1),x56971))), % 117.92/118.00 inference(scs_inference,[],[5601,5643,5638,5595,4658,4157,5299,44,79,62,69,89,67,66,68,77,70,63,64,9,11,4,6])). % 117.92/118.00 cnf(5706,plain, % 117.92/118.00 (E(f20(a1),f20(f22(x57061,a1)))), % 117.92/118.00 inference(scs_inference,[],[5601,5643,5638,5595,4658,4157,5299,44,79,62,69,89,67,66,68,77,70,63,64,9,11,4,6,14,7,17,5,19,16,20,21,12])). % 117.92/118.00 cnf(5709,plain, % 117.92/118.00 (E(f19(a1),f19(f22(x57091,a1)))), % 117.92/118.00 inference(scs_inference,[],[5601,5643,5638,5595,4658,4157,5299,44,79,62,69,89,67,66,68,77,70,63,64,9,11,4,6,14,7,17,5,19,16,20,21,12,18,15,8])). % 117.92/118.00 cnf(5711,plain, % 117.92/118.00 (E(f10(x57111,a1,x57112),f10(x57111,f22(x57113,a1),x57112))), % 117.92/118.00 inference(scs_inference,[],[5601,5643,5638,5595,4658,4157,5299,44,79,62,69,89,67,66,68,77,70,63,64,9,11,4,6,14,7,17,5,19,16,20,21,12,18,15,8,13,10])). % 117.92/118.00 cnf(5712,plain, % 117.92/118.00 (~E(f21(f22(a14,a7)),f19(f22(x57121,a16)))), % 117.92/118.00 inference(scs_inference,[],[5601,5643,5638,5452,5595,4658,4157,5299,44,79,62,69,89,67,66,68,77,70,63,64,9,11,4,6,14,7,17,5,19,16,20,21,12,18,15,8,13,10,2])). % 117.92/118.00 cnf(5718,plain, % 117.92/118.00 (~P2(f19(f19(x57181)),f19(f22(a1,a5)))), % 117.92/118.00 inference(scs_inference,[],[5635,5601,5643,5638,5631,5452,5595,4658,3419,4157,2426,5299,4102,44,79,62,69,89,67,66,68,77,70,63,64,9,11,4,6,14,7,17,5,19,16,20,21,12,18,15,8,13,10,2,85,80,86])). % 117.92/118.00 cnf(5720,plain, % 117.92/118.00 (P1(f21(a16))), % 117.92/118.00 inference(scs_inference,[],[5635,5634,5601,5643,5638,5631,5452,5595,4658,3419,4157,2426,5299,4102,57,44,79,62,69,89,67,66,68,77,70,63,64,9,11,4,6,14,7,17,5,19,16,20,21,12,18,15,8,13,10,2,85,80,86,78])). % 117.92/118.00 cnf(5721,plain, % 117.92/118.00 (~P6(x57211,f21(a16))), % 117.92/118.00 inference(rename_variables,[],[5634])). % 117.92/118.00 cnf(5724,plain, % 117.92/118.00 (~E(f19(f19(x57241)),f21(a16))), % 117.92/118.00 inference(scs_inference,[],[5635,5634,5721,5601,5643,5638,5631,5452,5595,4658,3419,4157,2426,5299,4102,57,44,79,62,69,89,67,66,68,77,70,63,64,9,11,4,6,14,7,17,5,19,16,20,21,12,18,15,8,13,10,2,85,80,86,78,24])). % 117.92/118.00 cnf(5738,plain, % 117.92/118.00 (E(f21(f22(a14,a7)),f22(x57381,a1))), % 117.92/118.00 inference(scs_inference,[],[5320,5635,5634,5721,5504,5601,5643,5638,5631,5452,5374,5445,5591,5595,5514,4658,3419,53,5301,5480,5511,4157,2426,5299,5076,4102,57,510,44,79,62,69,89,67,66,68,77,70,63,64,9,11,4,6,14,7,17,5,19,16,20,21,12,18,15,8,13,10,2,85,80,86,78,24,87,31,32,22,3,71,156,1995,97])). % 117.92/118.00 cnf(5745,plain, % 117.92/118.00 (P3(f20(a1))), % 117.92/118.00 inference(scs_inference,[],[5668,519])). % 117.92/118.00 cnf(5746,plain, % 117.92/118.00 (E(f21(a16),a1)), % 117.92/118.00 inference(scs_inference,[],[5720,62])). % 117.92/118.00 cnf(5750,plain, % 117.92/118.00 (P4(f21(f21(a16)))), % 117.92/118.00 inference(scs_inference,[],[5720,5599,62,79,69])). % 117.92/118.00 cnf(5754,plain, % 117.92/118.00 (~P1(f15(f15(f15(a6))))), % 117.92/118.00 inference(scs_inference,[],[5720,5599,5688,3406,62,79,69,77,70])). % 117.92/118.00 cnf(5756,plain, % 117.92/118.00 (P8(f21(f22(x57561,a7)),f21(a7))), % 117.92/118.00 inference(scs_inference,[],[5720,5599,5688,3406,51,62,79,69,77,70,89])). % 117.92/118.00 cnf(5758,plain, % 117.92/118.00 (P1(f21(f21(a16)))), % 117.92/118.00 inference(scs_inference,[],[5720,5599,5688,3406,51,62,79,69,77,70,89,67])). % 117.92/118.00 cnf(5760,plain, % 117.92/118.00 (P1(f20(f21(a16)))), % 117.92/118.00 inference(scs_inference,[],[5720,5599,5688,3406,51,62,79,69,77,70,89,67,66])). % 117.92/118.00 cnf(5762,plain, % 117.92/118.00 (P4(f20(f21(a16)))), % 117.92/118.00 inference(scs_inference,[],[5720,5599,5688,3406,51,62,79,69,77,70,89,67,66,68])). % 117.92/118.00 cnf(5764,plain, % 117.92/118.00 (P3(f21(a16))), % 117.92/118.00 inference(scs_inference,[],[5720,5599,5688,3406,51,62,79,69,77,70,89,67,66,68,63])). % 117.92/118.00 cnf(5766,plain, % 117.92/118.00 (P4(f21(a16))), % 117.92/118.00 inference(scs_inference,[],[5720,5599,5688,3406,51,62,79,69,77,70,89,67,66,68,63,64])). % 117.92/118.00 cnf(5775,plain, % 117.92/118.00 (E(f22(f22(x57751,f22(a3,a5)),x57752),f22(a16,x57752))), % 117.92/118.00 inference(scs_inference,[],[5720,5599,5688,3206,3406,51,62,79,69,77,70,89,67,66,68,63,64,9,11,4,7,14,5,6,17])). % 117.92/118.00 cnf(5781,plain, % 117.92/118.00 (E(f21(f22(x57811,f22(a3,a5))),f21(a16))), % 117.92/118.00 inference(scs_inference,[],[5720,5599,5688,3206,3406,51,62,79,69,77,70,89,67,66,68,63,64,9,11,4,7,14,5,6,17,20,16,21,19,12,13])). % 117.92/118.00 cnf(5782,plain, % 117.92/118.00 (E(f22(x57821,f22(x57822,f22(a3,a5))),f22(x57821,a16))), % 117.92/118.00 inference(scs_inference,[],[5720,5599,5688,3206,3406,51,62,79,69,77,70,89,67,66,68,63,64,9,11,4,7,14,5,6,17,20,16,21,19,12,13,18])). % 117.92/118.00 cnf(5787,plain, % 117.92/118.00 (P3(f22(x57871,f20(a1)))), % 117.92/118.00 inference(scs_inference,[],[5668,5720,5724,5599,5688,3206,505,3406,51,62,79,69,77,70,89,67,66,68,63,64,9,11,4,7,14,5,6,17,20,16,21,19,12,13,18,15,8,10,2,80])). % 117.92/118.00 cnf(5789,plain, % 117.92/118.00 (~P2(f19(a6),f19(f21(a16)))), % 117.92/118.00 inference(scs_inference,[],[5668,5720,5724,5599,5688,5508,3206,505,3406,51,62,79,69,77,70,89,67,66,68,63,64,9,11,4,7,14,5,6,17,20,16,21,19,12,13,18,15,8,10,2,80,86])). % 117.92/118.00 cnf(5794,plain, % 117.92/118.00 (P6(f18(f20(a1)),f19(f22(x57941,a1)))), % 117.92/118.00 inference(scs_inference,[],[5668,5720,5724,5599,5688,5709,5264,5508,922,3206,505,3406,61,51,62,79,69,77,70,89,67,66,68,63,64,9,11,4,7,14,5,6,17,20,16,21,19,12,13,18,15,8,10,2,80,86,78,24])). % 117.92/118.00 cnf(5796,plain, % 117.92/118.00 (~E(f22(x57961,a1),f19(f22(x57962,a16)))), % 117.92/118.00 inference(scs_inference,[],[5668,5720,5738,5724,5599,5688,5709,5264,5712,5508,922,3206,505,3406,61,51,62,79,69,77,70,89,67,66,68,63,64,9,11,4,7,14,5,6,17,20,16,21,19,12,13,18,15,8,10,2,80,86,78,24,22,3])). % 117.92/118.00 cnf(5798,plain, % 117.92/118.00 (~E(f21(f22(x57981,a16)),f19(a6))), % 117.92/118.00 inference(scs_inference,[],[5668,5720,5738,5724,5599,5688,5515,5709,5264,5712,5587,5508,922,3206,505,3406,61,51,62,79,69,77,70,89,67,66,68,63,64,9,11,4,7,14,5,6,17,20,16,21,19,12,13,18,15,8,10,2,80,86,78,24,22,3,30,29])). % 117.92/118.00 cnf(5799,plain, % 117.92/118.00 (P5(f21(a16))), % 117.92/118.00 inference(scs_inference,[],[5668,5720,5738,5724,5599,5688,5515,5709,5264,5712,5587,5508,922,3206,505,3406,61,51,62,79,69,77,70,89,67,66,68,63,64,9,11,4,7,14,5,6,17,20,16,21,19,12,13,18,15,8,10,2,80,86,78,24,22,3,30,29,71])). % 117.92/118.00 cnf(5804,plain, % 117.92/118.00 (~P6(f19(f20(a17)),f15(f20(a17)))), % 117.92/118.00 inference(scs_inference,[],[5668,5720,5738,5724,5599,5688,5515,5709,5264,5712,5587,5508,922,3206,505,3406,61,51,62,79,69,77,70,89,67,66,68,63,64,9,11,4,7,14,5,6,17,20,16,21,19,12,13,18,15,8,10,2,80,86,78,24,22,3,30,29,71,76,201,82])). % 117.92/118.00 cnf(5806,plain, % 117.92/118.00 (~E(f18(f21(a16)),f19(a6))), % 117.92/118.00 inference(scs_inference,[],[5668,5720,5738,5724,5599,5688,5515,5709,5264,5712,5587,5508,922,3206,505,3406,61,51,62,79,69,77,70,89,67,66,68,63,64,9,11,4,7,14,5,6,17,20,16,21,19,12,13,18,15,8,10,2,80,86,78,24,22,3,30,29,71,76,201,82,156])). % 117.92/118.00 cnf(5811,plain, % 117.92/118.00 (~P8(f20(f22(a9,a7)),f20(a7))), % 117.92/118.00 inference(scs_inference,[],[5756,94])). % 117.92/118.00 cnf(5814,plain, % 117.92/118.00 (E(f21(f21(a16)),a1)), % 117.92/118.00 inference(scs_inference,[],[5678,5758,79,62])). % 117.92/118.00 cnf(5822,plain, % 117.92/118.00 (P4(f22(x58221,f21(a16)))), % 117.92/118.00 inference(scs_inference,[],[5766,5678,5758,79,62,69,68,66,77])). % 117.92/118.00 cnf(5824,plain, % 117.92/118.00 (~P1(f15(f19(x58241)))), % 117.92/118.00 inference(scs_inference,[],[5766,5678,5758,61,79,62,69,68,66,77,70])). % 117.92/118.00 cnf(5826,plain, % 117.92/118.00 (P3(f21(f21(a16)))), % 117.92/118.00 inference(scs_inference,[],[5766,5678,5758,61,79,62,69,68,66,77,70,63])). % 117.92/118.00 cnf(5832,plain, % 117.92/118.00 (E(f10(x58321,x58322,f21(a16)),f10(x58321,x58322,a1))), % 117.92/118.00 inference(scs_inference,[],[5766,5746,5678,5758,3120,61,79,62,69,68,66,77,70,63,67,64,11])). % 117.92/118.00 cnf(5833,plain, % 117.92/118.00 (E(f10(f21(a16),x58331,x58332),f10(a1,x58331,x58332))), % 117.92/118.00 inference(scs_inference,[],[5766,5746,5678,5758,3120,61,79,62,69,68,66,77,70,63,67,64,11,9])). % 117.92/118.00 cnf(5834,plain, % 117.92/118.00 (E(f12(f21(a16)),f12(a1))), % 117.92/118.00 inference(scs_inference,[],[5766,5746,5678,5758,3120,61,79,62,69,68,66,77,70,63,67,64,11,9,5])). % 117.92/118.00 cnf(5835,plain, % 117.92/118.00 (E(f11(f21(a16),x58351,x58352),f11(a1,x58351,x58352))), % 117.92/118.00 inference(scs_inference,[],[5766,5746,5678,5758,3120,61,79,62,69,68,66,77,70,63,67,64,11,9,5,14])). % 117.92/118.00 cnf(5836,plain, % 117.92/118.00 (E(f2(x58361,f21(a16)),f2(x58361,a1))), % 117.92/118.00 inference(scs_inference,[],[5766,5746,5678,5758,3120,61,79,62,69,68,66,77,70,63,67,64,11,9,5,14,7])). % 117.92/118.00 cnf(5837,plain, % 117.92/118.00 (E(f18(f21(a16)),f18(a1))), % 117.92/118.00 inference(scs_inference,[],[5766,5746,5678,5758,3120,61,79,62,69,68,66,77,70,63,67,64,11,9,5,14,7,4])). % 117.92/118.00 cnf(5842,plain, % 117.92/118.00 (E(f11(x58421,x58422,f21(a16)),f11(x58421,x58422,a1))), % 117.92/118.00 inference(scs_inference,[],[5766,5746,5678,5758,3120,61,79,62,69,68,66,77,70,63,67,64,11,9,5,14,7,4,17,6,21,19,16])). % 117.92/118.00 cnf(5844,plain, % 117.92/118.00 (E(f20(f21(a16)),f20(a1))), % 117.92/118.00 inference(scs_inference,[],[5766,5746,5678,5758,3120,61,79,62,69,68,66,77,70,63,67,64,11,9,5,14,7,4,17,6,21,19,16,20,12])). % 117.92/118.00 cnf(5846,plain, % 117.92/118.00 (E(f21(f21(a16)),f21(a1))), % 117.92/118.00 inference(scs_inference,[],[5766,5746,5678,5758,3120,61,79,62,69,68,66,77,70,63,67,64,11,9,5,14,7,4,17,6,21,19,16,20,12,8,13])). % 117.92/118.00 cnf(5849,plain, % 117.92/118.00 (E(f10(x58491,f21(a16),x58492),f10(x58491,a1,x58492))), % 117.92/118.00 inference(scs_inference,[],[5766,5746,5678,5758,3120,61,79,62,69,68,66,77,70,63,67,64,11,9,5,14,7,4,17,6,21,19,16,20,12,8,13,15,18,10])). % 117.92/118.00 cnf(5851,plain, % 117.92/118.00 (~P6(x58511,f12(f19(f22(a16,a5))))), % 117.92/118.00 inference(scs_inference,[],[5766,5746,5678,5798,5758,3120,3481,2426,61,79,62,69,68,66,77,70,63,67,64,11,9,5,14,7,4,17,6,21,19,16,20,12,8,13,15,18,10,2,85])). % 117.92/118.00 cnf(5854,plain, % 117.92/118.00 (P3(f22(x58541,f21(a16)))), % 117.92/118.00 inference(scs_inference,[],[5764,5766,5746,5678,5798,5758,3120,3481,2426,61,79,62,69,68,66,77,70,63,67,64,11,9,5,14,7,4,17,6,21,19,16,20,12,8,13,15,18,10,2,85,80])). % 117.92/118.00 cnf(5856,plain, % 117.92/118.00 (~P2(f19(f22(x58561,a1)),f19(f22(a14,a5)))), % 117.92/118.00 inference(scs_inference,[],[5764,5766,5746,5678,5798,5758,5794,3120,3481,3349,2426,61,79,62,69,68,66,77,70,63,67,64,11,9,5,14,7,4,17,6,21,19,16,20,12,8,13,15,18,10,2,85,80,86])). % 117.92/118.00 cnf(5864,plain, % 117.92/118.00 (P2(f10(f22(x58641,a1),x58642,f22(a14,a7)),f19(f10(a1,x58642,a16)))), % 117.92/118.00 inference(scs_inference,[],[5568,5764,5766,5746,5678,5798,5694,5758,5672,5794,5804,5372,4179,3120,3481,5445,5345,3349,2426,5284,61,79,62,69,68,66,77,70,63,67,64,11,9,5,14,7,4,17,6,21,19,16,20,12,8,13,15,18,10,2,85,80,86,78,24,22,3,29])). % 117.92/118.00 cnf(5867,plain, % 117.92/118.00 (~P6(x58671,f20(f22(x58672,f21(a16))))), % 117.92/118.00 inference(scs_inference,[],[5568,5764,5766,5746,5678,5798,5694,5758,5672,5794,5804,5372,4179,3120,3481,5445,5345,5635,3349,2426,5284,61,510,44,79,62,69,68,66,77,70,63,67,64,11,9,5,14,7,4,17,6,21,19,16,20,12,8,13,15,18,10,2,85,80,86,78,24,22,3,29,90])). % 117.92/118.00 cnf(5890,plain, % 117.92/118.00 (E(f20(f21(a16)),a1)), % 117.92/118.00 inference(scs_inference,[],[5760,5811,322,331,2417,199,264,289,311,557,2507,3209,3446,3496,4196,234,219,62])). % 117.92/118.00 cnf(5894,plain, % 117.92/118.00 (P2(f21(f22(x58941,a7)),f19(f21(a7)))), % 117.92/118.00 inference(scs_inference,[],[5756,5760,5811,322,331,2417,199,264,289,311,557,2507,3209,3446,3496,4196,234,219,62,83,79])). % 117.92/118.00 cnf(5911,plain, % 117.92/118.00 (P3(f20(f21(a16)))), % 117.92/118.00 inference(scs_inference,[],[5756,5760,5811,322,331,2417,199,264,289,311,557,2507,3209,3446,3496,4196,234,219,62,83,79,88,84,343,69,67,68,82,66,63])). % 117.92/118.00 cnf(5919,plain, % 117.92/118.00 (~P1(f20(f22(a9,a7)))), % 117.92/118.00 inference(scs_inference,[],[5756,5824,5822,5760,5811,1357,322,331,2417,199,264,289,311,557,2507,3209,3446,3496,4196,234,219,62,83,79,88,84,343,69,67,68,82,66,63,77,70,64,74])). % 117.92/118.00 cnf(5941,plain, % 117.92/118.00 (~E(f19(f22(x59411,a16)),f22(x59412,a1))), % 117.92/118.00 inference(scs_inference,[],[5756,5824,5822,5796,5760,5814,5811,1357,322,331,2417,199,264,289,311,557,2507,3209,3446,3496,4196,234,219,62,83,79,88,84,343,69,67,68,82,66,63,77,70,64,74,156,5,11,17,4,14,7,9,6,21,16,12,126,20,19,8,18,13,10,15,2])). % 117.92/118.00 cnf(5943,plain, % 117.92/118.00 (P4(f22(x59431,f21(a16)))), % 117.92/118.00 inference(rename_variables,[],[5822])). % 117.92/118.00 cnf(5945,plain, % 117.92/118.00 (~P2(a17,f19(f20(f21(a16))))), % 117.92/118.00 inference(scs_inference,[],[5756,5824,5822,5854,5796,5760,5814,5811,1357,838,322,331,2417,199,264,289,311,557,2507,3209,3446,3496,4196,234,219,62,83,79,88,84,343,69,67,68,82,66,63,77,70,64,74,156,5,11,17,4,14,7,9,6,21,16,12,126,20,19,8,18,13,10,15,2,80,86])). % 117.92/118.00 cnf(5947,plain, % 117.92/118.00 (P6(f15(f21(a17)),f19(f21(a17)))), % 117.92/118.00 inference(scs_inference,[],[5756,5824,5822,5854,5796,5760,5814,5811,5349,1357,838,61,322,331,2417,199,264,289,311,557,2507,3209,3446,3496,4196,234,219,62,83,79,88,84,343,69,67,68,82,66,63,77,70,64,74,156,5,11,17,4,14,7,9,6,21,16,12,126,20,19,8,18,13,10,15,2,80,86,78])). % 117.92/118.00 cnf(5950,plain, % 117.92/118.00 (~P6(x59501,f20(f21(a16)))), % 117.92/118.00 inference(scs_inference,[],[5756,5844,5824,5822,5854,5796,5760,5814,5811,5349,1357,838,61,510,322,331,2417,199,264,289,311,557,2507,3209,3446,3496,4196,234,219,62,83,79,88,84,343,69,67,68,82,66,63,77,70,64,74,156,5,11,17,4,14,7,9,6,21,16,12,126,20,19,8,18,13,10,15,2,80,86,78,24])). % 117.92/118.00 cnf(5954,plain, % 117.92/118.00 (E(f10(f21(a16),x59541,f21(a16)),f10(a1,x59541,a1))), % 117.92/118.00 inference(scs_inference,[],[5832,5833,5756,5844,5824,5822,5854,5796,5760,5814,5811,5349,4977,1357,838,61,510,322,331,2417,199,264,289,311,557,2507,3209,3446,3496,4196,234,219,62,83,79,88,84,343,69,67,68,82,66,63,77,70,64,74,156,5,11,17,4,14,7,9,6,21,16,12,126,20,19,8,18,13,10,15,2,80,86,78,24,27,22,3])). % 117.92/118.00 cnf(5957,plain, % 117.92/118.00 (~P2(f19(a1),f19(f22(a14,a5)))), % 117.92/118.00 inference(scs_inference,[],[5832,5833,5756,5844,5824,5822,5854,5796,5760,5814,5811,5349,5856,4977,5709,1357,838,61,510,322,331,2417,199,264,289,311,557,2507,3209,3446,3496,4196,234,219,62,83,79,88,84,343,69,67,68,82,66,63,77,70,64,74,156,5,11,17,4,14,7,9,6,21,16,12,126,20,19,8,18,13,10,15,2,80,86,78,24,27,22,3,29])). % 117.92/118.00 cnf(5959,plain, % 117.92/118.00 (~P4(f22(a9,a7))), % 117.92/118.00 inference(scs_inference,[],[42,5832,5833,5756,5844,5824,5822,5854,5796,5760,5814,5811,5349,5856,4977,5709,1357,838,5305,61,510,51,322,331,2417,199,264,289,311,557,2507,3209,3446,3496,4196,234,219,62,83,79,88,84,343,69,67,68,82,66,63,77,70,64,74,156,5,11,17,4,14,7,9,6,21,16,12,126,20,19,8,18,13,10,15,2,80,86,78,24,27,22,3,29,101])). % 117.92/118.00 cnf(5962,plain, % 117.92/118.00 (E(f21(a16),f22(x59621,f21(a16)))), % 117.92/118.00 inference(scs_inference,[],[42,5832,5833,5756,5844,5824,5822,5854,5796,5760,5814,5811,5349,5856,4977,5764,5709,1357,838,5766,5305,61,510,51,322,331,2417,199,264,289,311,557,2507,3209,3446,3496,4196,234,219,62,83,79,88,84,343,69,67,68,82,66,63,77,70,64,74,156,5,11,17,4,14,7,9,6,21,16,12,126,20,19,8,18,13,10,15,2,80,86,78,24,27,22,3,29,101,105])). % 117.92/118.00 cnf(5971,plain, % 117.92/118.00 (~E(f22(x59711,f21(a16)),f22(a9,a7))), % 117.92/118.00 inference(scs_inference,[],[42,5832,5833,5756,5844,5824,5822,5943,5854,5796,5760,5814,5811,5349,5856,4977,5764,5709,1357,838,5766,5305,61,510,51,322,331,2417,199,264,289,311,557,2507,3209,3446,3496,4196,234,219,62,83,79,88,84,343,69,67,68,82,66,63,77,70,64,74,156,5,11,17,4,14,7,9,6,21,16,12,126,20,19,8,18,13,10,15,2,80,86,78,24,27,22,3,29,101,105,5064,891,76,201,72,25])). % 117.92/118.00 cnf(5976,plain, % 117.92/118.00 (P2(f22(f20(a16),a7),f19(x59761))), % 117.92/118.00 inference(scs_inference,[],[5597,4712,62,79])). % 117.92/118.00 cnf(5982,plain, % 117.92/118.00 (~P6(f19(f21(a17)),f15(f21(a17)))), % 117.92/118.00 inference(scs_inference,[],[5762,5947,5597,4712,4108,62,79,69,77,82])). % 117.92/118.00 cnf(5992,plain, % 117.92/118.00 (~P1(f15(f20(f22(a9,a7))))), % 117.92/118.00 inference(scs_inference,[],[5919,5762,5947,5597,4712,4108,62,79,69,77,82,68,67,66,63,70])). % 117.92/118.00 cnf(5994,plain, % 117.92/118.00 (P4(a14)), % 117.92/118.00 inference(scs_inference,[],[5919,5762,5947,5597,4712,4108,37,62,79,69,77,82,68,67,66,63,70,64])). % 117.92/118.00 cnf(6019,plain, % 117.92/118.00 (~P2(f19(f21(a17)),f19(f22(a16,a5)))), % 117.92/118.00 inference(scs_inference,[],[5971,5787,5919,5762,5957,5890,5947,5597,4712,4108,5080,3369,37,62,79,69,77,82,68,67,66,63,70,64,11,5,156,17,9,7,4,14,16,12,6,21,19,20,8,13,18,10,15,2,80,86])). % 117.92/118.00 cnf(6021,plain, % 117.92/118.00 (P1(f12(f19(f22(a16,a5))))), % 117.92/118.00 inference(scs_inference,[],[5971,5787,5919,5762,5957,5890,5947,5597,5851,4712,4108,5080,3369,37,57,62,79,69,77,82,68,67,66,63,70,64,11,5,156,17,9,7,4,14,16,12,6,21,19,20,8,13,18,10,15,2,80,86,78])). % 117.92/118.00 cnf(6023,plain, % 117.92/118.00 (P2(f12(x60231),x60231)), % 117.92/118.00 inference(rename_variables,[],[57])). % 117.92/118.00 cnf(6027,plain, % 117.92/118.00 (P8(f11(a1,x60271,x60272),f11(f21(a16),x60271,x60272))), % 117.92/118.00 inference(scs_inference,[],[5971,5835,5787,5919,5950,5762,5957,5890,5947,5597,5851,4712,4108,5080,3369,37,56,57,62,79,69,77,82,68,67,66,63,70,64,11,5,156,17,9,7,4,14,16,12,6,21,19,20,8,13,18,10,15,2,80,86,78,24,27])). % 117.92/118.00 cnf(6030,plain, % 117.92/118.00 (~E(f20(f21(a16)),f22(a9,a7))), % 117.92/118.00 inference(scs_inference,[],[5959,5971,5835,5787,5919,5950,5762,5957,5890,5947,5597,5851,4712,4108,5080,5601,3369,37,56,57,62,79,69,77,82,68,67,66,63,70,64,11,5,156,17,9,7,4,14,16,12,6,21,19,20,8,13,18,10,15,2,80,86,78,24,27,22,25])). % 117.92/118.00 cnf(6031,plain, % 117.92/118.00 (~E(f18(a1),f19(a6))), % 117.92/118.00 inference(scs_inference,[],[5959,5806,5971,5835,5787,5919,5950,5762,5957,5890,5947,5597,5837,5851,4712,4108,5080,5601,3369,37,56,57,62,79,69,77,82,68,67,66,63,70,64,11,5,156,17,9,7,4,14,16,12,6,21,19,20,8,13,18,10,15,2,80,86,78,24,27,22,25,3])). % 117.92/118.00 cnf(6034,plain, % 117.92/118.00 (P8(f21(f22(x60341,a14)),f21(a14))), % 117.92/118.00 inference(scs_inference,[],[5959,5806,5971,5835,5834,5787,5919,5950,5762,5957,5890,5947,5597,5837,5851,4712,4108,5080,5601,3369,37,56,57,6023,62,79,69,77,82,68,67,66,63,70,64,11,5,156,17,9,7,4,14,16,12,6,21,19,20,8,13,18,10,15,2,80,86,78,24,27,22,25,3,29,89])). % 117.92/118.00 cnf(6049,plain, % 117.92/118.00 (P4(f22(x60491,a14))), % 117.92/118.00 inference(scs_inference,[],[5994,6034,5680,3386,62,69,79,68,77])). % 117.92/118.00 cnf(6051,plain, % 117.92/118.00 (P1(f21(f22(x60511,f22(a14,a5))))), % 117.92/118.00 inference(scs_inference,[],[5994,6034,5680,3386,62,69,79,68,77,67])). % 117.92/118.00 cnf(6060,plain, % 117.92/118.00 (E(f12(f22(x60601,a16)),f12(f22(a1,a5)))), % 117.92/118.00 inference(scs_inference,[],[5994,6034,5680,6021,3386,4134,62,69,79,68,77,67,66,63,64,11,5])). % 117.92/118.00 cnf(6074,plain, % 117.92/118.00 (E(f19(f22(x60741,a16)),f19(f22(a1,a5)))), % 117.92/118.00 inference(scs_inference,[],[5994,6034,6019,5680,6021,3386,4134,62,69,79,68,77,67,66,63,64,11,5,17,156,9,7,6,14,4,12,16,20,19,21,18,8])). % 117.92/118.00 cnf(6075,plain, % 117.92/118.00 (E(f21(f22(x60751,a16)),f21(f22(a1,a5)))), % 117.92/118.00 inference(scs_inference,[],[5994,6034,6019,5680,6021,3386,4134,62,69,79,68,77,67,66,63,64,11,5,17,156,9,7,6,14,4,12,16,20,19,21,18,8,13])). % 117.92/118.00 cnf(6081,plain, % 117.92/118.00 (P6(f22(f20(a16),a7),f19(x60811))), % 117.92/118.00 inference(scs_inference,[],[5994,5976,6030,6034,5826,6019,5680,6021,5750,3386,4134,61,62,69,79,68,77,67,66,63,64,11,5,17,156,9,7,6,14,4,12,16,20,19,21,18,8,13,15,10,2,80,78])). % 117.92/118.00 cnf(6090,plain, % 117.92/118.00 (~P2(f19(f19(x60901)),f19(f22(x60902,a16)))), % 117.92/118.00 inference(scs_inference,[],[5994,5745,5976,5842,6030,6034,6027,5826,5706,6019,5782,5680,6021,5750,5718,3386,4134,2426,61,62,69,79,68,77,67,66,63,64,11,5,17,156,9,7,6,14,4,12,16,20,19,21,18,8,13,15,10,2,80,78,24,26,28,30])). % 117.92/118.00 cnf(6091,plain, % 117.92/118.00 (~E(a14,f22(a9,a7))), % 117.92/118.00 inference(scs_inference,[],[5994,5745,5976,5842,6030,6034,6027,5826,5706,6019,5782,5680,6021,5750,5718,5959,3386,4134,2426,61,62,69,79,68,77,67,66,63,64,11,5,17,156,9,7,6,14,4,12,16,20,19,21,18,8,13,15,10,2,80,78,24,26,28,30,25])). % 117.92/118.00 cnf(6112,plain, % 117.92/118.00 (P4(f22(x61121,f22(x61122,a14)))), % 117.92/118.00 inference(scs_inference,[],[6049,6051,4182,3444,62,79,69,68,77])). % 117.92/118.00 cnf(6114,plain, % 117.92/118.00 (P1(f21(f22(x61141,f22(a16,a5))))), % 117.92/118.00 inference(scs_inference,[],[6049,6051,4182,3444,62,79,69,68,77,67])). % 117.92/118.00 cnf(6120,plain, % 117.92/118.00 (P4(f18(x61201))), % 117.92/118.00 inference(scs_inference,[],[6049,6051,4182,3444,55,62,79,69,68,77,67,66,63,64])). % 117.92/118.00 cnf(6138,plain, % 117.92/118.00 (E(f21(f22(a1,a5)),f21(f22(x61381,a16)))), % 117.92/118.00 inference(scs_inference,[],[6049,6090,6051,4182,3444,4140,55,62,79,69,68,77,67,66,63,64,5,11,17,156,9,7,6,19,14,12,20,4,16,21,8,18,13])). % 117.92/118.00 cnf(6152,plain, % 117.92/118.00 (~E(f22(x61521,a14),f22(a9,a7))), % 117.92/118.00 inference(scs_inference,[],[6049,508,5337,6091,6081,5836,5911,5982,6090,6051,5867,4182,5706,3444,4140,5959,5762,5345,55,57,62,79,69,68,77,67,66,63,64,5,11,17,156,9,7,6,19,14,12,20,4,16,21,8,18,13,10,15,2,80,78,24,32,31,30,25])). % 117.92/118.00 cnf(6155,plain, % 117.92/118.00 (P2(f10(f22(x61551,a1),f22(x61552,a1),f22(a14,a7)),f19(f10(a1,a1,a16)))), % 117.92/118.00 inference(scs_inference,[],[6049,508,5337,6031,6091,6081,5836,5711,5911,5982,6090,5864,6051,5696,5867,4182,5706,3444,4140,5959,5762,5345,5601,55,57,62,79,69,68,77,67,66,63,64,5,11,17,156,9,7,6,19,14,12,20,4,16,21,8,18,13,10,15,2,80,78,24,32,31,30,25,3,22,29])). % 117.92/118.00 cnf(6168,plain, % 117.92/118.00 (P2(f22(x61681,f22(a1,a5)),f19(x61682))), % 117.92/118.00 inference(scs_inference,[],[6114,4168,62,79])). % 117.92/118.00 cnf(6170,plain, % 117.92/118.00 (P4(f21(f22(x61701,f22(a3,a5))))), % 117.92/118.00 inference(scs_inference,[],[6114,4168,3177,62,79,69])). % 117.92/118.00 cnf(6174,plain, % 117.92/118.00 (P4(f20(f22(x61741,f22(a3,a5))))), % 117.92/118.00 inference(scs_inference,[],[6112,6114,4168,3177,62,79,69,77,68])). % 117.92/118.00 cnf(6176,plain, % 117.92/118.00 (P1(f21(f22(x61761,f22(a3,a5))))), % 117.92/118.00 inference(scs_inference,[],[6112,6114,4168,3177,62,79,69,77,68,67])). % 117.92/118.00 cnf(6182,plain, % 117.92/118.00 (P4(f21(f20(a3)))), % 117.92/118.00 inference(scs_inference,[],[6112,6114,4168,3177,550,62,79,69,77,68,67,66,63,64])). % 117.92/118.00 cnf(6185,plain, % 117.92/118.00 (E(f10(x61851,x61852,f22(a14,a7)),f10(x61851,x61852,a1))), % 117.92/118.00 inference(scs_inference,[],[6112,6114,4168,3177,5213,550,62,79,69,77,68,67,66,63,64,5,11])). % 117.92/118.00 cnf(6188,plain, % 117.92/118.00 (E(f10(f22(a14,a7),x61881,x61882),f10(a1,x61881,x61882))), % 117.92/118.00 inference(scs_inference,[],[6112,6114,5945,4168,3177,5213,550,62,79,69,77,68,67,66,63,64,5,11,17,156,9])). % 117.92/118.00 cnf(6189,plain, % 117.92/118.00 (E(f2(x61891,f22(a14,a7)),f2(x61891,a1))), % 117.92/118.00 inference(scs_inference,[],[6112,6114,5945,4168,3177,5213,550,62,79,69,77,68,67,66,63,64,5,11,17,156,9,7])). % 117.92/118.00 cnf(6190,plain, % 117.92/118.00 (E(f2(f22(a14,a7),x61901),f2(a1,x61901))), % 117.92/118.00 inference(scs_inference,[],[6112,6114,5945,4168,3177,5213,550,62,79,69,77,68,67,66,63,64,5,11,17,156,9,7,6])). % 117.92/118.00 cnf(6191,plain, % 117.92/118.00 (E(f11(f22(a14,a7),x61911,x61912),f11(a1,x61911,x61912))), % 117.92/118.00 inference(scs_inference,[],[6112,6114,5945,4168,3177,5213,550,62,79,69,77,68,67,66,63,64,5,11,17,156,9,7,6,14])). % 117.92/118.00 cnf(6196,plain, % 117.92/118.00 (E(f11(x61961,x61962,f22(a14,a7)),f11(x61961,x61962,a1))), % 117.92/118.00 inference(scs_inference,[],[6112,6114,5945,4168,3177,5213,550,62,79,69,77,68,67,66,63,64,5,11,17,156,9,7,6,14,12,20,19,21,16])). % 117.92/118.00 cnf(6200,plain, % 117.92/118.00 (E(f21(f22(a14,a7)),f21(a1))), % 117.92/118.00 inference(scs_inference,[],[6112,6114,5945,4168,3177,5213,550,62,79,69,77,68,67,66,63,64,5,11,17,156,9,7,6,14,12,20,19,21,16,4,8,18,13])). % 117.92/118.00 cnf(6201,plain, % 117.92/118.00 (E(f11(x62011,f22(a14,a7),x62012),f11(x62011,a1,x62012))), % 117.92/118.00 inference(scs_inference,[],[6112,6114,5945,4168,3177,5213,550,62,79,69,77,68,67,66,63,64,5,11,17,156,9,7,6,14,12,20,19,21,16,4,8,18,13,15])). % 117.92/118.00 cnf(6202,plain, % 117.92/118.00 (E(f10(x62021,f22(a14,a7),x62022),f10(x62021,a1,x62022))), % 117.92/118.00 inference(scs_inference,[],[6112,6114,5945,4168,3177,5213,550,62,79,69,77,68,67,66,63,64,5,11,17,156,9,7,6,14,12,20,19,21,16,4,8,18,13,15,10])). % 117.92/118.00 cnf(6207,plain, % 117.92/118.00 (P6(f15(f15(a6)),f19(f15(a6)))), % 117.92/118.00 inference(scs_inference,[],[6152,6112,5603,6114,5945,4168,3177,5213,3464,3465,61,550,62,79,69,77,68,67,66,63,64,5,11,17,156,9,7,6,14,12,20,19,21,16,4,8,18,13,15,10,2,80,78])). % 117.92/118.00 cnf(6210,plain, % 117.92/118.00 (~P6(x62101,f21(f22(a1,a5)))), % 117.92/118.00 inference(scs_inference,[],[6152,6112,5603,6138,6114,5945,5651,4168,3177,5213,3464,3465,61,550,62,79,69,77,68,67,66,63,64,5,11,17,156,9,7,6,14,12,20,19,21,16,4,8,18,13,15,10,2,80,78,24])). % 117.92/118.00 cnf(6213,plain, % 117.92/118.00 (E(f10(x62131,f21(a16),x62132),f10(x62131,a1,x62132))), % 117.92/118.00 inference(rename_variables,[],[5849])). % 117.92/118.00 cnf(6219,plain, % 117.92/118.00 (~E(f18(x62191),f22(a9,a7))), % 117.92/118.00 inference(scs_inference,[],[6120,6152,5849,6213,5954,6112,5603,6138,6114,5992,5945,5651,4168,5638,3177,5213,507,5959,3464,3465,61,550,62,79,69,77,68,67,66,63,64,5,11,17,156,9,7,6,14,12,20,19,21,16,4,8,18,13,15,10,2,80,78,24,27,3,22,25])). % 117.92/118.00 cnf(6242,plain, % 117.92/118.00 (P2(f22(f12(f19(a1)),a5),f19(x62421))), % 117.92/118.00 inference(scs_inference,[],[6182,6176,4083,2441,62,69,77,79])). % 117.92/118.00 cnf(6265,plain, % 117.92/118.00 (E(f19(f22(a14,a7)),f19(f22(x62651,a16)))), % 117.92/118.00 inference(scs_inference,[],[6182,6176,4083,2441,4930,62,69,77,79,68,67,66,63,5,17,11,9,7,6,14,19,12,21,16,4,20,8])). % 117.92/118.00 cnf(6266,plain, % 117.92/118.00 (E(f22(x62661,f22(f20(a16),a7)),f22(x62661,a16))), % 117.92/118.00 inference(scs_inference,[],[6182,6176,4083,2441,4930,4713,62,69,77,79,68,67,66,63,5,17,11,9,7,6,14,19,12,21,16,4,20,8,18])). % 117.92/118.00 cnf(6273,plain, % 117.92/118.00 (P1(f21(f22(a1,a5)))), % 117.92/118.00 inference(scs_inference,[],[6219,6210,6182,6176,4083,2441,4930,4713,3764,3765,57,62,69,77,79,68,67,66,63,5,17,11,9,7,6,14,19,12,21,16,4,20,8,18,10,13,15,2,80,78])). % 117.92/118.00 cnf(6277,plain, % 117.92/118.00 (~P6(x62771,f22(f22(x62772,f22(a3,a5)),a5))), % 117.92/118.00 inference(scs_inference,[],[6219,6210,6182,5775,6176,4083,3420,2441,4930,4713,3764,3765,57,62,69,77,79,68,67,66,63,5,17,11,9,7,6,14,19,12,21,16,4,20,8,18,10,13,15,2,80,78,24])). % 117.92/118.00 cnf(6279,plain, % 117.92/118.00 (~E(f19(f22(a1,a5)),f22(x62791,a1))), % 117.92/118.00 inference(scs_inference,[],[6219,5941,6210,6182,6074,5775,6176,4083,3420,2441,4930,4713,3764,3765,57,62,69,77,79,68,67,66,63,5,17,11,9,7,6,14,19,12,21,16,4,20,8,18,10,13,15,2,80,78,24,3])). % 117.92/118.00 cnf(6282,plain, % 117.92/118.00 (~E(f21(f20(a3)),f22(a9,a7))), % 117.92/118.00 inference(scs_inference,[],[6219,5941,6210,6182,6074,5775,6176,4083,3420,2441,4930,4713,3764,3765,5959,5601,57,62,69,77,79,68,67,66,63,5,17,11,9,7,6,14,19,12,21,16,4,20,8,18,10,13,15,2,80,78,24,3,22,25])). % 117.92/118.00 cnf(6288,plain, % 117.92/118.00 (P4(f21(f22(a1,a5)))), % 117.92/118.00 inference(scs_inference,[],[6219,6185,5941,6210,6182,6074,6155,5775,6170,6176,4083,3420,2441,4930,4713,3764,3765,5959,5601,57,62,69,77,79,68,67,66,63,5,17,11,9,7,6,14,19,12,21,16,4,20,8,18,10,13,15,2,80,78,24,3,22,25,29,71,64])). % 117.92/118.00 cnf(6293,plain, % 117.92/118.00 (E(f21(f22(a1,a5)),a1)), % 117.92/118.00 inference(scs_inference,[],[6273,62])). % 117.92/118.00 cnf(6299,plain, % 117.92/118.00 (P2(f22(f20(a1),a5),f19(x62991))), % 117.92/118.00 inference(scs_inference,[],[6273,6288,4105,62,77,69,79])). % 117.92/118.00 cnf(6303,plain, % 117.92/118.00 (P1(f21(f21(f22(a1,a5))))), % 117.92/118.00 inference(scs_inference,[],[6273,6288,4105,62,77,69,79,68,67])). % 117.92/118.00 cnf(6307,plain, % 117.92/118.00 (P3(f21(f22(a1,a5)))), % 117.92/118.00 inference(scs_inference,[],[6273,6288,4105,62,77,69,79,68,67,66,63])). % 117.92/118.00 cnf(6332,plain, % 117.92/118.00 (P6(f22(x63321,f22(a1,a5)),f19(x63322))), % 117.92/118.00 inference(scs_inference,[],[6168,6282,6273,6288,4105,6081,4699,61,62,77,69,79,68,67,66,63,17,5,11,9,14,6,19,12,7,20,16,21,4,8,18,13,10,15,2,80,86,78])). % 117.92/118.00 cnf(6335,plain, % 117.92/118.00 (~P6(x63351,f22(x63352,f22(f20(a16),a7)))), % 117.92/118.00 inference(scs_inference,[],[6168,6282,6273,6288,6266,4105,6081,4699,2426,61,62,77,69,79,68,67,66,63,17,5,11,9,14,6,19,12,7,20,16,21,4,8,18,13,10,15,2,80,86,78,24])). % 117.92/118.00 cnf(6340,plain, % 117.92/118.00 (E(f10(f22(a14,a7),x63401,x63402),f10(a1,x63401,x63402))), % 117.92/118.00 inference(rename_variables,[],[6188])). % 117.92/118.00 cnf(6345,plain, % 117.92/118.00 (~E(f21(f22(a1,a5)),f22(a9,a7))), % 117.92/118.00 inference(scs_inference,[],[6168,6188,6340,6202,6282,6273,6288,5579,6266,5478,4105,6081,4699,4102,5959,2426,61,5811,62,77,69,79,68,67,66,63,17,5,11,9,14,6,19,12,7,20,16,21,4,8,18,13,10,15,2,80,86,78,24,27,30,3,22,25])). % 117.92/118.00 cnf(6359,plain, % 117.92/118.00 (P4(f21(f22(a14,a5)))), % 117.92/118.00 inference(scs_inference,[],[6303,4012,5750,3349,62,77,79,69])). % 117.92/118.00 cnf(6361,plain, % 117.92/118.00 (P1(f21(f22(a14,a5)))), % 117.92/118.00 inference(scs_inference,[],[6303,4012,5750,3349,62,77,79,69,67])). % 117.92/118.00 cnf(6363,plain, % 117.92/118.00 (P4(f20(f22(a14,a5)))), % 117.92/118.00 inference(scs_inference,[],[6303,4012,5750,3349,62,77,79,69,67,68])). % 117.92/118.00 cnf(6365,plain, % 117.92/118.00 (P1(f20(f22(a14,a5)))), % 117.92/118.00 inference(scs_inference,[],[6303,4012,5750,3349,62,77,79,69,67,68,66])). % 117.92/118.00 cnf(6387,plain, % 117.92/118.00 (~E(f22(a9,a7),f21(f22(a1,a5)))), % 117.92/118.00 inference(scs_inference,[],[6345,6293,6303,4012,5750,3349,62,77,79,69,67,68,66,63,17,5,11,9,14,19,6,12,7,20,16,4,21,8,10,13,18,15,2])). % 117.92/118.00 cnf(6393,plain, % 117.92/118.00 (P1(f22(x63931,f22(f20(a16),a7)))), % 117.92/118.00 inference(scs_inference,[],[6332,6345,6293,6335,6303,4012,5750,4189,3349,4186,57,62,77,79,69,67,68,66,63,17,5,11,9,14,19,6,12,7,20,16,4,21,8,10,13,18,15,2,86,80,78])). % 117.92/118.00 cnf(6399,plain, % 117.92/118.00 (P8(f11(a1,x63991,x63992),f11(f22(a14,a7),x63991,x63992))), % 117.92/118.00 inference(scs_inference,[],[6332,6345,6191,6293,6335,6303,6277,4012,5750,4189,3349,4186,56,57,62,77,79,69,67,68,66,63,17,5,11,9,14,19,6,12,7,20,16,4,21,8,10,13,18,15,2,86,80,78,24,27])). % 117.92/118.00 cnf(6401,plain, % 117.92/118.00 (~P2(f19(f19(x64011)),f19(f22(a14,a7)))), % 117.92/118.00 inference(scs_inference,[],[6332,6345,6191,6293,6335,6303,6265,6277,4012,6090,5750,4189,3349,4186,56,57,62,77,79,69,67,68,66,63,17,5,11,9,14,19,6,12,7,20,16,4,21,8,10,13,18,15,2,86,80,78,24,27,30])). % 117.92/118.00 cnf(6403,plain, % 117.92/118.00 (~E(a1,f22(a9,a7))), % 117.92/118.00 inference(scs_inference,[],[6332,6345,6191,6293,6335,6303,6265,6277,4012,6090,5750,4189,3349,4186,56,57,62,77,79,69,67,68,66,63,17,5,11,9,14,19,6,12,7,20,16,4,21,8,10,13,18,15,2,86,80,78,24,27,30,3])). % 117.92/118.00 cnf(6406,plain, % 117.92/118.00 (P2(f21(a1),f19(f21(a7)))), % 117.92/118.00 inference(scs_inference,[],[6332,6345,6191,6200,6293,5894,6174,6335,6303,6265,6277,4012,6090,5750,4189,3349,5224,4186,5959,56,57,62,77,79,69,67,68,66,63,17,5,11,9,14,19,6,12,7,20,16,4,21,8,10,13,18,15,2,86,80,78,24,27,30,3,22,25,29])). % 117.92/118.00 cnf(6415,plain, % 117.92/118.00 (E(f21(f22(a14,a5)),a1)), % 117.92/118.00 inference(scs_inference,[],[6361,62])). % 117.92/118.00 cnf(6429,plain, % 117.92/118.00 (P4(f22(x64291,f22(f20(a16),a7)))), % 117.92/118.00 inference(scs_inference,[],[6359,6361,6399,6393,62,79,77,67,69,68,66,64])). % 117.92/118.00 cnf(6448,plain, % 117.92/118.00 (E(f22(x64481,f22(f20(a16),a5)),f22(x64481,a16))), % 117.92/118.00 inference(scs_inference,[],[6359,6361,6399,6401,6393,3773,62,79,77,67,69,68,66,64,63,156,5,17,11,9,14,19,12,6,7,20,16,21,4,13,18])). % 117.92/118.00 cnf(6452,plain, % 117.92/118.00 (~E(f22(a9,a7),a1)), % 117.92/118.00 inference(scs_inference,[],[6403,6359,6361,6399,6401,6393,3773,62,79,77,67,69,68,66,64,63,156,5,17,11,9,14,19,12,6,7,20,16,21,4,13,18,10,8,15,2])). % 117.92/118.00 cnf(6453,plain, % 117.92/118.00 (~P6(x64531,f12(f19(f22(a14,a7))))), % 117.92/118.00 inference(scs_inference,[],[6403,6359,6361,6399,6401,6393,4936,3773,2426,62,79,77,67,69,68,66,64,63,156,5,17,11,9,14,19,12,6,7,20,16,21,4,13,18,10,8,15,2,85])). % 117.92/118.00 cnf(6456,plain, % 117.92/118.00 (~P2(f19(x64561),f19(f21(f22(a14,a5))))), % 117.92/118.00 inference(scs_inference,[],[6403,6359,6361,6399,6401,6393,4936,6332,3773,2426,62,79,77,67,69,68,66,64,63,156,5,17,11,9,14,19,12,6,7,20,16,21,4,13,18,10,8,15,2,85,86])). % 117.92/118.00 cnf(6460,plain, % 117.92/118.00 (P6(f22(f20(a1),a5),f19(x64601))), % 117.92/118.01 inference(scs_inference,[],[6403,6299,6359,6361,6399,6401,6393,4936,6332,3773,2426,61,62,79,77,67,69,68,66,64,63,156,5,17,11,9,14,19,12,6,7,20,16,21,4,13,18,10,8,15,2,85,86,80,78])). % 117.92/118.01 cnf(6463,plain, % 117.92/118.01 (~P6(x64631,f21(f22(x64632,f22(a3,a5))))), % 117.92/118.01 inference(scs_inference,[],[6403,6299,6359,6361,6399,6401,5781,6393,4936,5634,6332,3773,2426,61,62,79,77,67,69,68,66,64,63,156,5,17,11,9,14,19,12,6,7,20,16,21,4,13,18,10,8,15,2,85,86,80,78,24])). % 117.92/118.01 cnf(6466,plain, % 117.92/118.01 (E(f11(x64661,x64662,f22(a14,a7)),f11(x64661,x64662,a1))), % 117.92/118.01 inference(rename_variables,[],[6196])). % 117.92/118.01 cnf(6474,plain, % 117.92/118.01 (~E(f21(f22(a14,a5)),f22(a9,a7))), % 117.92/118.01 inference(scs_inference,[],[6403,6299,6196,6466,6201,6359,6361,6307,6399,6401,5781,6393,5544,6138,4936,5634,6332,3773,3369,2426,5959,61,57,62,79,77,67,69,68,66,64,63,156,5,17,11,9,14,19,12,6,7,20,16,21,4,13,18,10,8,15,2,85,86,80,78,24,26,28,30,3,22,25])). % 117.92/118.01 cnf(6482,plain, % 117.92/118.01 (E(f20(f22(a14,a5)),a1)), % 117.92/118.01 inference(scs_inference,[],[6365,62])). % 117.92/118.01 cnf(6492,plain, % 117.92/118.01 (P1(f21(f20(f22(a14,a5))))), % 117.92/118.01 inference(scs_inference,[],[6363,6365,3968,62,77,79,69,68,67])). % 117.92/118.01 cnf(6496,plain, % 117.92/118.01 (P3(f20(f22(a14,a5)))), % 117.92/118.01 inference(scs_inference,[],[6363,6365,3968,62,77,79,69,68,67,66,63])). % 117.92/118.01 cnf(6523,plain, % 117.92/118.01 (P1(f12(f19(f22(a14,a7))))), % 117.92/118.01 inference(scs_inference,[],[6460,6474,6363,6365,6415,6456,6453,3968,3406,3407,57,62,77,79,69,68,67,66,63,156,5,11,17,9,19,14,12,6,7,20,16,4,13,21,18,10,8,15,2,86,80,78])). % 117.92/118.01 cnf(6531,plain, % 117.92/118.01 (~P2(f19(f19(x65311)),f19(a16))), % 117.92/118.01 inference(scs_inference,[],[5799,6460,6474,6363,6365,5498,5962,6415,6463,6456,6453,5660,3968,53,6401,3406,3407,57,62,77,79,69,68,67,66,63,156,5,11,17,9,19,14,12,6,7,20,16,4,13,21,18,10,8,15,2,86,80,78,24,32,31,30])). % 117.92/118.01 cnf(6534,plain, % 117.92/118.01 (~E(f20(f22(a14,a5)),f22(a9,a7))), % 117.92/118.01 inference(scs_inference,[],[5799,6460,6474,6387,6363,6365,5498,5962,6415,6075,6463,6456,6453,5660,3968,53,6401,5078,3406,3407,5959,57,62,77,79,69,68,67,66,63,156,5,11,17,9,19,14,12,6,7,20,16,4,13,21,18,10,8,15,2,86,80,78,24,32,31,30,3,22,25])). % 117.92/118.01 cnf(6547,plain, % 117.92/118.01 (P1(f21(f22(a3,a5)))), % 117.92/118.01 inference(scs_inference,[],[6492,3888,3156,62,79,67])). % 117.92/118.01 cnf(6549,plain, % 117.92/118.01 (P4(f21(f22(a3,a5)))), % 117.92/118.01 inference(scs_inference,[],[6492,3888,3156,62,79,67,69])). % 117.92/118.01 cnf(6551,plain, % 117.92/118.01 (P4(f20(f22(a3,a5)))), % 117.92/118.01 inference(scs_inference,[],[6492,3888,3156,62,79,67,69,68])). % 117.92/118.01 cnf(6555,plain, % 117.92/118.01 (P1(f20(f22(a3,a5)))), % 117.92/118.01 inference(scs_inference,[],[6492,3888,4171,3156,62,79,67,69,68,77,66])). % 117.92/118.01 cnf(6583,plain, % 117.92/118.01 (P6(f21(a1),f19(f21(a7)))), % 117.92/118.01 inference(scs_inference,[],[6534,6531,6496,6406,6482,6492,6523,3888,6363,4171,3156,61,62,79,67,69,68,77,66,64,63,156,5,11,17,19,14,9,12,7,16,6,21,20,13,10,4,18,8,15,2,80,78])). % 117.92/118.01 cnf(6586,plain, % 117.92/118.01 (~P6(x65861,f22(x65862,f22(f20(a16),a5)))), % 117.92/118.01 inference(scs_inference,[],[6534,6531,6496,6406,6482,6448,6492,6523,3888,6363,4171,3156,2426,61,62,79,67,69,68,77,66,64,63,156,5,11,17,19,14,9,12,7,16,6,21,20,13,10,4,18,8,15,2,80,78,24])). % 117.92/118.01 cnf(6590,plain, % 117.92/118.01 (E(f2(f22(a14,a7),f22(a14,a7)),f2(a1,a1))), % 117.92/118.01 inference(scs_inference,[],[6534,6189,6190,6531,6496,6406,6482,6448,6492,6523,3888,6363,4171,3156,2426,61,57,62,79,67,69,68,77,66,64,63,156,5,11,17,19,14,9,12,7,16,6,21,20,13,10,4,18,8,15,2,80,78,24,30,3])). % 117.92/118.01 cnf(6597,plain, % 117.92/118.01 (~P6(f19(f21(a7)),f21(a1))), % 117.92/118.01 inference(scs_inference,[],[6534,6189,6190,6531,6496,6406,6482,6242,6448,6429,6492,6523,5754,5789,3888,6363,4171,3156,2426,5959,61,57,62,79,67,69,68,77,66,64,63,156,5,11,17,19,14,9,12,7,16,6,21,20,13,10,4,18,8,15,2,80,78,24,30,3,22,25,29,82])). % 117.92/118.01 cnf(6601,plain, % 117.92/118.01 (~P2(f19(f15(a6)),f19(f22(a3,a5)))), % 117.92/118.01 inference(scs_inference,[],[6534,6189,6190,6531,6496,6406,6482,6242,6448,6429,6492,6523,5754,6207,5789,3888,6363,4171,3156,5601,2426,5959,61,57,62,79,67,69,68,77,66,64,63,156,5,11,17,19,14,9,12,7,16,6,21,20,13,10,4,18,8,15,2,80,78,24,30,3,22,25,29,82,72,86])). % 117.92/118.01 cnf(6606,plain, % 117.92/118.01 (E(f21(f22(a3,a5)),a1)), % 117.92/118.01 inference(scs_inference,[],[6547,5490,4753,62])). % 117.92/118.01 cnf(6608,plain, % 117.92/118.01 (P1(f21(f21(f22(a3,a5))))), % 117.92/118.01 inference(scs_inference,[],[6547,5490,4753,62,67])). % 117.92/118.01 cnf(6610,plain, % 117.92/118.01 (P4(f22(x66101,f21(f22(a3,a5))))), % 117.92/118.01 inference(scs_inference,[],[6547,6549,5490,4753,62,67,77])). % 117.92/118.01 cnf(6618,plain, % 117.92/118.01 (P1(f20(f21(f22(a3,a5))))), % 117.92/118.01 inference(scs_inference,[],[6547,6549,5490,3862,4753,62,67,77,68,79,69,66])). % 117.92/118.01 cnf(6620,plain, % 117.92/118.01 (P3(f21(f22(a3,a5)))), % 117.92/118.01 inference(scs_inference,[],[6547,6549,5490,3862,4753,62,67,77,68,79,69,66,63])). % 117.92/118.01 cnf(6642,plain, % 117.92/118.01 (~P2(f19(x66421),f19(f21(f22(a3,a5))))), % 117.92/118.01 inference(scs_inference,[],[6279,6547,6549,5490,6601,3862,6460,4188,4753,62,67,77,68,79,69,66,63,156,5,11,17,19,14,9,12,7,6,13,20,16,4,21,10,18,8,15,2,86])). % 117.92/118.01 cnf(6647,plain, % 117.92/118.01 (P1(f22(x66471,f22(f20(a16),a5)))), % 117.92/118.01 inference(scs_inference,[],[6279,6547,6549,5490,6601,6586,3862,6460,4188,57,2443,2446,4753,62,67,77,68,79,69,66,63,156,5,11,17,19,14,9,12,7,6,13,20,16,4,21,10,18,8,15,2,86,80,78])). % 117.92/118.01 cnf(6653,plain, % 117.92/118.01 (~E(f21(f22(a3,a5)),f22(a9,a7))), % 117.92/118.01 inference(scs_inference,[],[6452,6279,5846,6597,6547,6549,5490,6601,6586,5407,3862,6460,4188,5959,57,2443,2446,4753,62,67,77,68,79,69,66,63,156,5,11,17,19,14,9,12,7,6,13,20,16,4,21,10,18,8,15,2,86,80,78,24,3,25])). % 117.92/118.01 cnf(6710,plain, % 117.92/118.01 (P8(f2(a1,a1),f2(f22(a14,a7),f22(a14,a7)))), % 117.92/118.01 inference(scs_inference,[],[6653,6590,6620,6606,5400,6608,6642,6647,6551,6555,6583,3846,6549,507,56,61,111,62,69,68,77,79,67,66,64,63,156,5,11,14,19,17,9,12,13,7,6,20,4,21,10,16,18,8,15,2,86,80,78,24,27])). % 117.92/118.01 cnf(6714,plain, % 117.92/118.01 (~E(f22(x67141,f21(f22(a3,a5))),f22(a9,a7))), % 117.92/118.01 inference(scs_inference,[],[6653,6590,6620,5697,6606,5400,6608,6610,6642,6647,6551,6555,6583,3846,6549,507,56,5959,61,111,62,69,68,77,79,67,66,64,63,156,5,11,14,19,17,9,12,13,7,6,20,4,21,10,16,18,8,15,2,86,80,78,24,27,3,25])). % 117.92/118.01 cnf(6732,plain, % 117.92/118.01 (P4(f21(f22(a16,a5)))), % 117.92/118.01 inference(scs_inference,[],[6618,6060,5076,4102,3369,4739,62,77,68,69])). % 117.92/118.01 cnf(6736,plain, % 117.92/118.01 (P1(f21(f22(a16,a5)))), % 117.92/118.01 inference(scs_inference,[],[6710,6618,6060,5076,4102,3369,4739,62,77,68,69,79,67])). % 117.92/118.01 cnf(6796,plain, % 117.92/118.01 (P1(f20(f21(f22(a16,a5))))), % 117.92/118.01 inference(scs_inference,[],[6732,6736,3404,62,69,79,77,68,67,66])). % 117.92/118.01 cnf(6915,plain, % 117.92/118.01 (P1(f21(a14))), % 117.92/118.01 inference(scs_inference,[],[6796,3327,3193,3369,37,62,69,68,77,79,67])). % 117.92/118.01 cnf(6964,plain, % 117.92/118.01 (E(f21(a14),a1)), % 117.92/118.01 inference(scs_inference,[],[6915,62])). % 117.92/118.01 cnf(8118,plain, % 117.92/118.01 ($false), % 117.92/118.01 inference(scs_inference,[],[51,5959,6964,5696,6714,5513,5577,2,18,12,13,156,77]), % 117.92/118.01 ['proof']). % 117.92/118.01 % SZS output end Proof % 117.92/118.01 % Total time :117.290000s %------------------------------------------------------------------------------