%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU255+1 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n026.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:02:05 EDT 2024 % Result : Theorem 119.12s 119.11s % Output : CNFRefutation 119.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : SEU255+1 : TPTP v8.2.0. Released v3.3.0. % 0.08/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n026.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Fri Jun 21 12:37:38 EDT 2024 % 0.13/0.34 % CPUTime : % 0.54/0.58 start to proof:theBenchmark % 119.10/119.08 %------------------------------------------- % 119.10/119.08 % File :CSE---1.7 % 119.10/119.08 % Problem :theBenchmark % 119.10/119.08 % Transform :cnf % 119.10/119.08 % Format :tptp:raw % 119.10/119.08 % Command :java -jar mcs_scs.jar %d %s % 119.10/119.08 % 119.10/119.08 % Result :Theorem 118.460000s % 119.10/119.08 % Output :CNFRefutation 118.460000s % 119.10/119.08 %------------------------------------------- % 119.10/119.10 %------------------------------------------------------------------------------ % 119.10/119.10 % File : SEU255+1 : TPTP v8.2.0. Released v3.3.0. % 119.10/119.10 % Domain : Set theory % 119.10/119.10 % Problem : MPTP bushy problem t25_wellord1 % 119.10/119.10 % Version : [Urb07] axioms : Especial. % 119.10/119.10 % English : % 119.10/119.10 % 119.10/119.10 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 119.10/119.10 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 119.10/119.10 % Source : [Urb07] % 119.10/119.10 % Names : bushy-t25_wellord1 [Urb07] % 119.10/119.10 % 119.10/119.10 % Status : Theorem % 119.10/119.10 % Rating : 0.17 v8.2.0, 0.14 v8.1.0, 0.17 v7.5.0, 0.19 v7.4.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.13 v6.4.0, 0.15 v6.3.0, 0.17 v6.2.0, 0.20 v6.1.0, 0.27 v6.0.0, 0.22 v5.5.0, 0.26 v5.4.0, 0.32 v5.3.0, 0.41 v5.2.0, 0.25 v5.1.0, 0.29 v4.1.0, 0.30 v4.0.0, 0.33 v3.7.0, 0.30 v3.5.0, 0.32 v3.3.0 % 119.10/119.10 % Syntax : Number of formulae : 33 ( 17 unt; 0 def) % 119.10/119.10 % Number of atoms : 63 ( 9 equ) % 119.10/119.10 % Maximal formula atoms : 6 ( 1 avg) % 119.10/119.10 % Number of connectives : 36 ( 6 ~; 1 |; 14 &) % 119.10/119.10 % ( 2 <=>; 13 =>; 0 <=; 0 <~>) % 119.10/119.10 % Maximal formula depth : 8 ( 3 avg) % 119.12/119.10 % Maximal term depth : 3 ( 1 avg) % 119.12/119.10 % Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty) % 119.12/119.10 % Number of functors : 7 ( 7 usr; 1 con; 0-2 aty) % 119.12/119.10 % Number of variables : 43 ( 37 !; 6 ?) % 119.12/119.10 % SPC : FOF_THM_RFO_SEQ % 119.12/119.10 % 119.12/119.11 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 119.12/119.11 % library, www.mizar.org % 119.12/119.11 %------------------------------------------------------------------------------ % 119.12/119.11 fof(antisymmetry_r2_hidden,axiom, % 119.12/119.11 ! [A,B] : % 119.12/119.11 ( in(A,B) % 119.12/119.11 => ~ in(B,A) ) ). % 119.12/119.11 % 119.12/119.11 fof(cc1_funct_1,axiom, % 119.12/119.11 ! [A] : % 119.12/119.11 ( empty(A) % 119.12/119.11 => function(A) ) ). % 119.12/119.11 % 119.12/119.11 fof(cc2_funct_1,axiom, % 119.12/119.11 ! [A] : % 119.12/119.11 ( ( relation(A) % 119.12/119.11 & empty(A) % 119.12/119.11 & function(A) ) % 119.12/119.11 => ( relation(A) % 119.12/119.11 & function(A) % 119.12/119.11 & one_to_one(A) ) ) ). % 119.12/119.11 % 119.12/119.11 fof(commutativity_k2_tarski,axiom, % 119.12/119.11 ! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) ). % 119.12/119.11 % 119.12/119.11 fof(commutativity_k3_xboole_0,axiom, % 119.12/119.11 ! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) ). % 119.12/119.11 % 119.12/119.11 fof(d5_tarski,axiom, % 119.12/119.11 ! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)) ). % 119.12/119.11 % 119.12/119.11 fof(d6_wellord1,axiom, % 119.12/119.11 ! [A] : % 119.12/119.11 ( relation(A) % 119.12/119.11 => ! [B] : relation_restriction(A,B) = set_intersection2(A,cartesian_product2(B,B)) ) ). % 119.12/119.11 % 119.12/119.11 fof(dt_k1_tarski,axiom, % 119.12/119.11 $true ). % 119.12/119.11 % 119.12/119.11 fof(dt_k1_xboole_0,axiom, % 119.12/119.11 $true ). % 119.12/119.11 % 119.12/119.11 fof(dt_k2_tarski,axiom, % 119.12/119.11 $true ). % 119.12/119.11 % 119.12/119.11 fof(dt_k2_wellord1,axiom, % 119.12/119.11 ! [A,B] : % 119.12/119.11 ( relation(A) % 119.12/119.11 => relation(relation_restriction(A,B)) ) ). % 119.12/119.11 % 119.12/119.11 fof(dt_k2_zfmisc_1,axiom, % 119.12/119.11 $true ). % 119.12/119.11 % 119.12/119.11 fof(dt_k3_xboole_0,axiom, % 119.12/119.11 $true ). % 119.12/119.11 % 119.12/119.11 fof(dt_k4_tarski,axiom, % 119.12/119.11 $true ). % 119.12/119.11 % 119.12/119.11 fof(dt_m1_subset_1,axiom, % 119.12/119.11 $true ). % 119.12/119.11 % 119.12/119.11 fof(existence_m1_subset_1,axiom, % 119.12/119.11 ! [A] : % 119.12/119.11 ? [B] : element(B,A) ). % 119.12/119.11 % 119.12/119.11 fof(fc1_xboole_0,axiom, % 119.12/119.11 empty(empty_set) ). % 119.12/119.11 % 119.12/119.11 fof(fc1_zfmisc_1,axiom, % 119.12/119.11 ! [A,B] : ~ empty(ordered_pair(A,B)) ). % 119.12/119.11 % 119.12/119.11 fof(idempotence_k3_xboole_0,axiom, % 119.12/119.11 ! [A,B] : set_intersection2(A,A) = A ). % 119.12/119.11 % 119.12/119.11 fof(l3_wellord1,axiom, % 119.12/119.11 ! [A] : % 119.12/119.11 ( relation(A) % 119.12/119.11 => ( antisymmetric(A) % 119.12/119.11 <=> ! [B,C] : % 119.12/119.11 ( ( in(ordered_pair(B,C),A) % 119.12/119.11 & in(ordered_pair(C,B),A) ) % 119.12/119.11 => B = C ) ) ) ). % 119.12/119.11 % 119.12/119.11 fof(rc1_funct_1,axiom, % 119.12/119.11 ? [A] : % 119.12/119.11 ( relation(A) % 119.12/119.11 & function(A) ) ). % 119.12/119.11 % 119.12/119.11 fof(rc1_xboole_0,axiom, % 119.12/119.11 ? [A] : empty(A) ). % 119.12/119.11 % 119.12/119.11 fof(rc2_funct_1,axiom, % 119.12/119.11 ? [A] : % 119.12/119.11 ( relation(A) % 119.12/119.11 & empty(A) % 119.12/119.11 & function(A) ) ). % 119.12/119.11 % 119.12/119.11 fof(rc2_xboole_0,axiom, % 119.12/119.11 ? [A] : ~ empty(A) ). % 119.12/119.11 % 119.12/119.11 fof(rc3_funct_1,axiom, % 119.12/119.11 ? [A] : % 119.12/119.11 ( relation(A) % 119.12/119.11 & function(A) % 119.12/119.11 & one_to_one(A) ) ). % 119.12/119.11 % 119.12/119.11 fof(t16_wellord1,axiom, % 119.12/119.11 ! [A,B,C] : % 119.12/119.11 ( relation(C) % 119.12/119.11 => ( in(A,relation_restriction(C,B)) % 119.12/119.11 <=> ( in(A,C) % 119.12/119.11 & in(A,cartesian_product2(B,B)) ) ) ) ). % 119.12/119.11 % 119.12/119.11 fof(t1_subset,axiom, % 119.12/119.11 ! [A,B] : % 119.12/119.11 ( in(A,B) % 119.12/119.11 => element(A,B) ) ). % 119.12/119.11 % 119.12/119.11 fof(t25_wellord1,conjecture, % 119.12/119.11 ! [A,B] : % 119.12/119.11 ( relation(B) % 119.12/119.11 => ( antisymmetric(B) % 119.12/119.11 => antisymmetric(relation_restriction(B,A)) ) ) ). % 119.12/119.11 % 119.12/119.11 fof(t2_boole,axiom, % 119.12/119.11 ! [A] : set_intersection2(A,empty_set) = empty_set ). % 119.12/119.11 % 119.12/119.11 fof(t2_subset,axiom, % 119.12/119.11 ! [A,B] : % 119.12/119.11 ( element(A,B) % 119.12/119.11 => ( empty(B) % 119.12/119.11 | in(A,B) ) ) ). % 119.12/119.11 % 119.12/119.11 fof(t6_boole,axiom, % 119.12/119.11 ! [A] : % 119.12/119.11 ( empty(A) % 119.12/119.11 => A = empty_set ) ). % 119.12/119.11 % 119.12/119.11 fof(t7_boole,axiom, % 119.12/119.11 ! [A,B] : % 119.12/119.11 ~ ( in(A,B) % 119.12/119.11 & empty(B) ) ). % 119.12/119.11 % 119.12/119.11 fof(t8_boole,axiom, % 119.12/119.11 ! [A,B] : % 119.12/119.11 ~ ( empty(A) % 119.12/119.11 & A != B % 119.12/119.11 & empty(B) ) ). % 119.12/119.11 % 119.12/119.11 %------------------------------------------------------------------------------ % 119.12/119.11 %------------------------------------------- % 119.12/119.11 % Proof found % 119.12/119.11 % SZS status Theorem for theBenchmark % 119.12/119.11 % SZS output start Proof % 119.12/119.12 %ClaNum:61(EqnAxiom:24) % 119.12/119.12 %VarNum:104(SingletonVarNum:41) % 119.12/119.12 %MaxLitNum:5 % 119.12/119.12 %MaxfuncDepth:3 % 119.12/119.12 %SharedTerms:23 % 119.12/119.12 %goalClause: 34 36 43 % 119.12/119.12 %singleGoalClaCount:3 % 119.12/119.12 [25]P1(a1) % 119.12/119.12 [26]P1(a3) % 119.12/119.12 [27]P1(a9) % 119.12/119.12 [28]P4(a4) % 119.12/119.12 [29]P4(a9) % 119.12/119.12 [30]P4(a10) % 119.12/119.12 [31]P5(a4) % 119.12/119.12 [32]P5(a9) % 119.12/119.12 [33]P5(a10) % 119.12/119.12 [34]P5(a5) % 119.12/119.12 [35]P6(a10) % 119.12/119.12 [36]P2(a5) % 119.12/119.12 [42]~P1(a11) % 119.12/119.12 [43]~P2(f14(a5,a13)) % 119.12/119.12 [37]E(f12(x371,a1),a1) % 119.12/119.12 [38]E(f12(x381,x381),x381) % 119.12/119.12 [39]P3(f6(x391),x391) % 119.12/119.12 [40]E(f15(x401,x402),f15(x402,x401)) % 119.12/119.12 [41]E(f12(x411,x412),f12(x412,x411)) % 119.12/119.12 [44]~P1(f15(f15(x441,x442),f16(x441))) % 119.12/119.12 [45]~P1(x451)+E(x451,a1) % 119.12/119.12 [46]~P1(x461)+P4(x461) % 119.12/119.12 [50]~P1(x501)+~P7(x502,x501) % 119.12/119.12 [51]~P7(x511,x512)+P3(x511,x512) % 119.12/119.12 [54]~P7(x542,x541)+~P7(x541,x542) % 119.12/119.12 [52]~P5(x521)+P5(f14(x521,x522)) % 119.12/119.12 [55]~P5(x551)+E(f12(x551,f2(x552,x552)),f14(x551,x552)) % 119.12/119.12 [48]~P5(x481)+P2(x481)+~E(f7(x481),f8(x481)) % 119.12/119.12 [59]~P5(x591)+P2(x591)+P7(f15(f15(f8(x591),f7(x591)),f16(f8(x591))),x591) % 119.12/119.12 [60]~P5(x601)+P2(x601)+P7(f15(f15(f7(x601),f8(x601)),f16(f7(x601))),x601) % 119.12/119.12 [47]~P1(x472)+~P1(x471)+E(x471,x472) % 119.12/119.12 [53]~P3(x532,x531)+P1(x531)+P7(x532,x531) % 119.12/119.12 [56]~P5(x562)+P7(x561,x562)+~P7(x561,f14(x562,x563)) % 119.12/119.12 [57]~P5(x573)+~P7(x571,f14(x573,x572))+P7(x571,f2(x572,x572)) % 119.12/119.12 [49]~P1(x491)+~P4(x491)+~P5(x491)+P6(x491) % 119.12/119.12 [58]~P5(x582)+~P7(x581,x582)+~P7(x581,f2(x583,x583))+P7(x581,f14(x582,x583)) % 119.12/119.12 [61]~P2(x613)+E(x611,x612)+~P5(x613)+~P7(f15(f15(x612,x611),f16(x612)),x613)+~P7(f15(f15(x611,x612),f16(x611)),x613) % 119.12/119.12 %EqnAxiom % 119.12/119.12 [1]E(x11,x11) % 119.12/119.12 [2]E(x22,x21)+~E(x21,x22) % 119.12/119.12 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 119.12/119.12 [4]~E(x41,x42)+E(f12(x41,x43),f12(x42,x43)) % 119.12/119.12 [5]~E(x51,x52)+E(f12(x53,x51),f12(x53,x52)) % 119.12/119.12 [6]~E(x61,x62)+E(f15(x61,x63),f15(x62,x63)) % 119.12/119.12 [7]~E(x71,x72)+E(f15(x73,x71),f15(x73,x72)) % 119.12/119.12 [8]~E(x81,x82)+E(f6(x81),f6(x82)) % 119.12/119.12 [9]~E(x91,x92)+E(f16(x91),f16(x92)) % 119.12/119.12 [10]~E(x101,x102)+E(f8(x101),f8(x102)) % 119.12/119.12 [11]~E(x111,x112)+E(f7(x111),f7(x112)) % 119.12/119.12 [12]~E(x121,x122)+E(f14(x121,x123),f14(x122,x123)) % 119.12/119.12 [13]~E(x131,x132)+E(f14(x133,x131),f14(x133,x132)) % 119.12/119.12 [14]~E(x141,x142)+E(f2(x141,x143),f2(x142,x143)) % 119.12/119.12 [15]~E(x151,x152)+E(f2(x153,x151),f2(x153,x152)) % 119.12/119.12 [16]~P1(x161)+P1(x162)+~E(x161,x162) % 119.12/119.12 [17]P7(x172,x173)+~E(x171,x172)+~P7(x171,x173) % 119.12/119.12 [18]P7(x183,x182)+~E(x181,x182)+~P7(x183,x181) % 119.12/119.12 [19]~P5(x191)+P5(x192)+~E(x191,x192) % 119.12/119.12 [20]~P4(x201)+P4(x202)+~E(x201,x202) % 119.12/119.12 [21]~P2(x211)+P2(x212)+~E(x211,x212) % 119.12/119.12 [22]P3(x222,x223)+~E(x221,x222)+~P3(x221,x223) % 119.12/119.12 [23]P3(x233,x232)+~E(x231,x232)+~P3(x233,x231) % 119.12/119.12 [24]~P6(x241)+P6(x242)+~E(x241,x242) % 119.12/119.12 % 119.12/119.12 %------------------------------------------- % 119.17/119.15 cnf(62,plain, % 119.17/119.15 (E(x621,f12(x621,x621))), % 119.17/119.15 inference(scs_inference,[],[38,2])). % 119.17/119.15 cnf(63,plain, % 119.17/119.15 (~P7(x631,a1)), % 119.17/119.15 inference(scs_inference,[],[38,25,2,50])). % 119.17/119.15 cnf(65,plain, % 119.17/119.15 (P5(f12(a5,a5))), % 119.17/119.15 inference(scs_inference,[],[34,38,25,2,50,19])). % 119.17/119.15 cnf(66,plain, % 119.17/119.15 (P2(f12(a5,a5))), % 119.17/119.15 inference(scs_inference,[],[34,36,38,25,2,50,19,21])). % 119.17/119.15 cnf(67,plain, % 119.17/119.15 (E(f12(a1,x671),a1)), % 119.17/119.15 inference(scs_inference,[],[34,36,38,41,25,37,2,50,19,21,3])). % 119.17/119.15 cnf(70,plain, % 119.17/119.15 (~P1(f15(f16(x701),f15(x701,x702)))), % 119.17/119.15 inference(scs_inference,[],[34,36,38,40,41,25,37,44,2,50,19,21,3,16])). % 119.17/119.15 cnf(72,plain, % 119.17/119.15 (P3(f6(f12(a5,a5)),a5)), % 119.17/119.15 inference(scs_inference,[],[34,36,38,39,40,41,25,37,44,2,50,19,21,3,16,23])). % 119.17/119.15 cnf(73,plain, % 119.17/119.15 (P3(f6(x731),x731)), % 119.17/119.15 inference(rename_variables,[],[39])). % 119.17/119.15 cnf(74,plain, % 119.17/119.15 (E(f12(x741,x741),x741)), % 119.17/119.15 inference(rename_variables,[],[38])). % 119.17/119.15 cnf(75,plain, % 119.17/119.15 (P7(f6(a11),a11)), % 119.17/119.15 inference(scs_inference,[],[34,36,38,39,73,40,41,25,42,37,44,2,50,19,21,3,16,23,53])). % 119.17/119.15 cnf(76,plain, % 119.17/119.15 (P3(f6(x761),x761)), % 119.17/119.15 inference(rename_variables,[],[39])). % 119.17/119.15 cnf(78,plain, % 119.17/119.15 (P6(a9)), % 119.17/119.15 inference(scs_inference,[],[34,36,32,38,39,73,40,41,25,27,29,42,37,44,2,50,19,21,3,16,23,53,49])). % 119.17/119.15 cnf(80,plain, % 119.17/119.15 (~P7(a11,f6(a11))), % 119.17/119.15 inference(scs_inference,[],[34,36,32,38,39,73,40,41,25,27,29,42,37,44,2,50,19,21,3,16,23,53,49,54])). % 119.17/119.15 cnf(82,plain, % 119.17/119.15 (P2(a1)+~P5(a1)), % 119.17/119.15 inference(scs_inference,[],[34,36,32,38,39,73,40,41,25,27,29,42,37,44,2,50,19,21,3,16,23,53,49,54,59])). % 119.17/119.15 cnf(85,plain, % 119.17/119.15 (P7(f6(a11),x851)+~E(a11,x851)), % 119.17/119.15 inference(scs_inference,[],[34,36,32,38,39,73,40,41,25,27,29,42,37,44,2,50,19,21,3,16,23,53,49,54,59,17,18])). % 119.17/119.15 cnf(86,plain, % 119.17/119.15 (~P4(f12(x861,x861))+P4(x861)), % 119.17/119.15 inference(scs_inference,[],[34,36,32,38,74,39,73,40,41,25,27,29,42,37,44,2,50,19,21,3,16,23,53,49,54,59,17,18,20])). % 119.17/119.15 cnf(87,plain, % 119.17/119.15 (P3(x871,x872)+~E(f6(x872),x871)), % 119.17/119.15 inference(scs_inference,[],[34,36,32,38,74,39,73,76,40,41,25,27,29,42,37,44,2,50,19,21,3,16,23,53,49,54,59,17,18,20,22])). % 119.17/119.15 cnf(88,plain, % 119.17/119.15 (~P6(f12(x881,x881))+P6(x881)), % 119.17/119.15 inference(scs_inference,[],[34,36,32,38,74,39,73,76,40,41,25,27,29,42,37,44,2,50,19,21,3,16,23,53,49,54,59,17,18,20,22,24])). % 119.17/119.15 cnf(92,plain, % 119.17/119.15 (P7(f6(a11),f12(a11,a11))), % 119.17/119.15 inference(scs_inference,[],[62,85])). % 119.17/119.15 cnf(93,plain, % 119.17/119.15 (E(x931,f12(x931,x931))), % 119.17/119.15 inference(rename_variables,[],[62])). % 119.17/119.15 cnf(94,plain, % 119.17/119.15 (P3(f12(f6(x941),f6(x941)),x941)), % 119.17/119.15 inference(scs_inference,[],[62,93,85,87])). % 119.17/119.15 cnf(95,plain, % 119.17/119.15 (E(x951,f12(x951,x951))), % 119.17/119.15 inference(rename_variables,[],[62])). % 119.17/119.15 cnf(96,plain, % 119.17/119.15 (~P7(x961,a3)), % 119.17/119.15 inference(scs_inference,[],[62,93,26,85,87,50])). % 119.17/119.15 cnf(98,plain, % 119.17/119.15 (~P7(f12(a11,a11),f6(a11))), % 119.17/119.15 inference(scs_inference,[],[62,93,26,85,87,50,54])). % 119.17/119.15 cnf(100,plain, % 119.17/119.15 (E(a1,f12(a1,x1001))), % 119.17/119.15 inference(scs_inference,[],[62,93,67,26,85,87,50,54,2])). % 119.17/119.15 cnf(101,plain, % 119.17/119.15 (P1(f12(a3,a3))), % 119.17/119.15 inference(scs_inference,[],[62,93,95,67,26,85,87,50,54,2,16])). % 119.17/119.15 cnf(102,plain, % 119.17/119.15 (E(x1021,f12(x1021,x1021))), % 119.17/119.15 inference(rename_variables,[],[62])). % 119.17/119.15 cnf(103,plain, % 119.17/119.15 (P4(f12(a4,a4))), % 119.17/119.15 inference(scs_inference,[],[62,93,95,102,67,26,28,85,87,50,54,2,16,20])). % 119.17/119.15 cnf(104,plain, % 119.17/119.15 (E(x1041,f12(x1041,x1041))), % 119.17/119.15 inference(rename_variables,[],[62])). % 119.17/119.15 cnf(105,plain, % 119.17/119.15 (P3(f6(x1051),f12(x1051,x1051))), % 119.17/119.15 inference(scs_inference,[],[62,93,95,102,104,67,26,28,39,85,87,50,54,2,16,20,23])). % 119.17/119.15 cnf(106,plain, % 119.17/119.15 (P3(f6(x1061),x1061)), % 119.17/119.15 inference(rename_variables,[],[39])). % 119.17/119.15 cnf(108,plain, % 119.17/119.15 (E(x1081,f12(x1081,x1081))), % 119.17/119.15 inference(rename_variables,[],[62])). % 119.17/119.15 cnf(109,plain, % 119.17/119.15 (E(f12(a1,x1091),f12(a1,a1))), % 119.17/119.15 inference(scs_inference,[],[62,93,95,102,104,108,72,67,26,28,39,85,87,50,54,2,16,20,23,22,3])). % 119.17/119.15 cnf(110,plain, % 119.17/119.15 (E(x1101,f12(x1101,x1101))), % 119.17/119.15 inference(rename_variables,[],[62])). % 119.17/119.15 cnf(111,plain, % 119.17/119.15 (P7(f6(f15(f16(x1111),f15(x1111,x1112))),f15(f16(x1111),f15(x1111,x1112)))), % 119.17/119.15 inference(scs_inference,[],[62,93,95,102,104,108,70,72,67,26,28,39,106,85,87,50,54,2,16,20,23,22,3,53])). % 119.17/119.15 cnf(115,plain, % 119.17/119.15 (E(x1151,f12(x1151,x1151))), % 119.17/119.15 inference(rename_variables,[],[62])). % 119.17/119.15 cnf(116,plain, % 119.17/119.15 (P7(f12(f6(a11),f6(a11)),a11)), % 119.17/119.15 inference(scs_inference,[],[78,62,93,95,102,104,108,110,115,70,72,67,75,26,28,39,106,85,87,50,54,2,16,20,23,22,3,53,24,17])). % 119.17/119.15 cnf(118,plain, % 119.17/119.15 (~E(a11,a1)), % 119.17/119.15 inference(scs_inference,[],[78,62,93,95,102,104,108,110,115,70,72,67,75,63,26,28,39,106,85,87,50,54,2,16,20,23,22,3,53,24,17,18])). % 119.17/119.15 cnf(123,plain, % 119.17/119.15 (~P5(f12(a1,x1231))+P5(a1)), % 119.17/119.15 inference(scs_inference,[],[78,62,93,95,102,104,108,110,115,70,72,67,75,63,26,28,39,106,85,87,50,54,2,16,20,23,22,3,53,24,17,18,60,21,19])). % 119.17/119.15 cnf(128,plain, % 119.17/119.15 (~P7(x1281,f12(a3,a3))), % 119.17/119.15 inference(scs_inference,[],[101,116,54,50])). % 119.17/119.15 cnf(131,plain, % 119.17/119.15 (P1(f12(a1,x1311))), % 119.17/119.15 inference(scs_inference,[],[109,101,100,116,25,54,50,2,16])). % 119.17/119.15 cnf(132,plain, % 119.17/119.15 (P4(f12(f12(a4,a4),f12(a4,a4)))), % 119.17/119.15 inference(scs_inference,[],[109,101,103,100,116,62,25,54,50,2,16,20])). % 119.17/119.15 cnf(133,plain, % 119.17/119.15 (E(x1331,f12(x1331,x1331))), % 119.17/119.15 inference(rename_variables,[],[62])). % 119.17/119.15 cnf(134,plain, % 119.17/119.15 (P3(f12(f6(x1341),f6(x1341)),f12(x1341,x1341))), % 119.17/119.15 inference(scs_inference,[],[105,109,101,103,100,116,62,133,25,54,50,2,16,20,22])). % 119.17/119.15 cnf(135,plain, % 119.17/119.15 (E(x1351,f12(x1351,x1351))), % 119.17/119.15 inference(rename_variables,[],[62])). % 119.17/119.15 cnf(138,plain, % 119.17/119.15 (P3(f12(f6(f12(a1,x1381)),f6(f12(a1,x1381))),f12(a1,a1))), % 119.17/119.15 inference(scs_inference,[],[105,94,109,92,101,103,100,116,62,133,96,25,54,50,2,16,20,22,18,23])). % 119.17/119.15 cnf(140,plain, % 119.17/119.15 (E(f12(a1,x1401),f12(a1,x1402))), % 119.17/119.15 inference(scs_inference,[],[105,94,109,92,101,103,100,116,62,133,67,96,25,54,50,2,16,20,22,18,23,3])). % 119.17/119.15 cnf(141,plain, % 119.17/119.15 (P7(f12(f6(a11),f6(a11)),f12(a11,a11))), % 119.17/119.15 inference(scs_inference,[],[105,94,109,92,101,103,100,116,62,133,135,67,96,25,54,50,2,16,20,22,18,23,3,17])). % 119.17/119.15 cnf(143,plain, % 119.17/119.15 (~P1(f12(a11,a11))), % 119.17/119.15 inference(scs_inference,[],[105,94,109,92,101,103,100,116,62,133,135,67,96,25,26,54,50,2,16,20,22,18,23,3,17,47])). % 119.17/119.15 cnf(154,plain, % 119.17/119.15 (~P7(x1541,f12(a1,x1542))), % 119.17/119.15 inference(scs_inference,[],[141,131,54,50])). % 119.17/119.15 cnf(156,plain, % 119.17/119.15 (E(a1,f12(x1561,a1))), % 119.17/119.15 inference(scs_inference,[],[141,131,37,54,50,2])). % 119.17/119.15 cnf(157,plain, % 119.17/119.15 (P1(f12(f12(a1,x1571),f12(a1,x1571)))), % 119.17/119.15 inference(scs_inference,[],[141,131,62,37,54,50,2,16])). % 119.17/119.15 cnf(158,plain, % 119.17/119.15 (E(x1581,f12(x1581,x1581))), % 119.17/119.15 inference(rename_variables,[],[62])). % 119.17/119.15 cnf(159,plain, % 119.17/119.15 (P3(f12(f12(f6(x1591),f6(x1591)),f12(f6(x1591),f6(x1591))),f12(x1591,x1591))), % 119.17/119.15 inference(scs_inference,[],[134,141,131,62,158,37,54,50,2,16,22])). % 119.17/119.15 cnf(160,plain, % 119.17/119.15 (E(x1601,f12(x1601,x1601))), % 119.17/119.15 inference(rename_variables,[],[62])). % 119.17/119.15 cnf(162,plain, % 119.17/119.15 (E(x1621,f12(x1621,x1621))), % 119.17/119.15 inference(rename_variables,[],[62])). % 119.17/119.15 cnf(165,plain, % 119.17/119.15 (E(f12(a1,x1651),f12(f12(a1,x1652),f12(a1,x1652)))), % 119.17/119.15 inference(scs_inference,[],[134,141,131,140,132,62,158,160,162,63,37,54,50,2,16,22,20,18,3])). % 119.17/119.15 cnf(166,plain, % 119.17/119.15 (E(x1661,f12(x1661,x1661))), % 119.17/119.15 inference(rename_variables,[],[62])). % 119.17/119.15 cnf(167,plain, % 119.17/119.15 (P3(f12(f6(a1),f6(a1)),f12(a1,x1671))), % 119.17/119.15 inference(scs_inference,[],[134,141,131,140,132,62,158,160,162,63,37,54,50,2,16,22,20,18,3,23])). % 119.17/119.15 cnf(170,plain, % 119.17/119.15 (P7(f12(f12(f6(a11),f6(a11)),f12(f6(a11),f6(a11))),f12(a11,a11))), % 119.17/119.15 inference(scs_inference,[],[134,141,131,140,132,62,158,160,162,166,63,37,54,50,2,16,22,20,18,3,23,17])). % 119.17/119.15 cnf(183,plain, % 119.17/119.15 (E(f12(f12(a1,x1831),f12(a1,x1831)),f12(a1,x1832))), % 119.17/119.15 inference(scs_inference,[],[170,157,165,50,54,2])). % 119.17/119.15 cnf(184,plain, % 119.17/119.15 (P1(f12(x1841,a1))), % 119.17/119.15 inference(scs_inference,[],[170,157,165,156,25,50,54,2,16])). % 119.17/119.15 cnf(186,plain, % 119.17/119.15 (E(x1861,f12(x1861,x1861))), % 119.17/119.15 inference(rename_variables,[],[62])). % 119.17/119.15 cnf(191,plain, % 119.17/119.15 (E(f12(a1,x1911),f12(f12(a1,x1912),f12(a1,x1912)))), % 119.17/119.15 inference(rename_variables,[],[165])). % 119.17/119.15 cnf(192,plain, % 119.17/119.15 (E(a1,f12(f12(a1,x1921),f12(a1,x1921)))), % 119.17/119.15 inference(scs_inference,[],[159,170,157,165,191,167,156,62,63,111,25,50,54,2,16,22,18,23,3])). % 119.17/119.15 cnf(195,plain, % 119.17/119.15 (P7(f12(f12(f6(a11),f6(a11)),f12(f6(a11),f6(a11))),a11)), % 119.17/119.15 inference(scs_inference,[],[159,170,157,165,191,167,156,116,62,186,63,111,25,50,54,2,16,22,18,23,3,17])). % 119.17/119.15 cnf(206,plain, % 119.17/119.15 (~P7(x2061,f12(x2062,a1))), % 119.17/119.15 inference(scs_inference,[],[184,195,54,50])). % 119.17/119.15 cnf(208,plain, % 119.17/119.15 (E(f12(f12(a1,x2081),f12(a1,x2081)),a1)), % 119.17/119.15 inference(scs_inference,[],[184,195,192,54,50,2])). % 119.17/119.15 cnf(209,plain, % 119.17/119.15 (P1(f12(f12(x2091,a1),f12(x2091,a1)))), % 119.17/119.15 inference(scs_inference,[],[184,195,192,62,54,50,2,16])). % 119.17/119.15 cnf(210,plain, % 119.17/119.15 (E(x2101,f12(x2101,x2101))), % 119.17/119.15 inference(rename_variables,[],[62])). % 119.17/119.15 cnf(213,plain, % 119.17/119.15 (P3(f12(f12(f6(x2131),f6(x2131)),f12(f6(x2131),f6(x2131))),x2131)), % 119.17/119.15 inference(scs_inference,[],[184,195,192,94,62,210,128,54,50,2,16,18,22])). % 119.17/119.15 cnf(216,plain, % 119.17/119.15 (E(f12(a1,x2161),f12(f12(a1,x2162),f12(a1,x2162)))), % 119.17/119.15 inference(rename_variables,[],[165])). % 119.17/119.15 cnf(217,plain, % 119.17/119.15 (E(f12(f12(a1,x2171),f12(a1,x2171)),f12(f12(a1,x2172),f12(a1,x2172)))), % 119.17/119.15 inference(scs_inference,[],[183,184,138,195,192,94,165,216,62,210,128,54,50,2,16,18,22,23,3])). % 119.17/119.15 cnf(226,plain, % 119.17/119.15 (~P7(x2261,f12(f12(x2262,a1),f12(x2262,a1)))), % 119.17/119.15 inference(scs_inference,[],[209,50])). % 119.17/119.15 cnf(228,plain, % 119.17/119.15 (~P7(f15(f16(x2281),f15(x2281,x2282)),f6(f15(f16(x2281),f15(x2281,x2282))))), % 119.17/119.15 inference(scs_inference,[],[209,111,50,54])). % 119.17/119.15 cnf(230,plain, % 119.17/119.15 (P1(f12(f12(f12(x2301,a1),f12(x2301,a1)),f12(f12(x2301,a1),f12(x2301,a1))))), % 119.17/119.15 inference(scs_inference,[],[209,62,111,50,54,16])). % 119.17/119.15 cnf(234,plain, % 119.17/119.15 (P3(f6(f12(a1,x2341)),f12(f12(a1,x2342),f12(a1,x2342)))), % 119.17/119.15 inference(scs_inference,[],[116,209,217,105,62,96,111,50,54,16,18,23])). % 119.17/119.15 cnf(236,plain, % 119.17/119.15 (~E(a11,f12(f12(a1,x2361),f12(a1,x2361)))), % 119.17/119.15 inference(scs_inference,[],[118,116,209,217,208,105,62,96,111,50,54,16,18,23,3])). % 119.17/119.15 cnf(237,plain, % 119.17/119.15 (~P4(f12(f12(a1,x2371),f12(a1,x2371)))+P4(a1)), % 119.17/119.15 inference(scs_inference,[],[118,116,209,217,208,105,62,96,111,50,54,16,18,23,3,20])). % 119.17/119.15 cnf(238,plain, % 119.17/119.15 (~P4(f12(f12(f12(a1,x2381),f12(a1,x2381)),f12(f12(a1,x2381),f12(a1,x2381))))+P4(a1)), % 119.17/119.15 inference(scs_inference,[],[118,116,209,217,208,105,62,96,111,50,54,16,18,23,3,20,86])). % 119.17/119.15 cnf(244,plain, % 119.17/119.15 (~P7(x2441,f12(f12(f12(x2442,a1),f12(x2442,a1)),f12(f12(x2442,a1),f12(x2442,a1))))), % 119.17/119.15 inference(scs_inference,[],[230,50])). % 119.17/119.15 cnf(246,plain, % 119.17/119.15 (~E(f12(a11,a11),f12(a1,x2461))), % 119.17/119.15 inference(scs_inference,[],[92,230,154,50,18])). % 119.17/119.15 cnf(248,plain, % 119.17/119.15 (P3(f12(f6(f12(a1,x2481)),f6(f12(a1,x2481))),f12(a1,x2482))), % 119.17/119.15 inference(scs_inference,[],[92,140,230,138,154,50,18,23])). % 119.17/119.15 cnf(252,plain, % 119.17/119.15 (~P4(a1)+P4(f12(f12(a1,x2521),f12(a1,x2521)))), % 119.17/119.15 inference(scs_inference,[],[92,192,140,165,230,236,138,154,50,18,23,3,20])). % 119.17/119.15 cnf(259,plain, % 119.17/119.15 (~P7(x2591,a9)), % 119.17/119.15 inference(scs_inference,[],[27,50])). % 119.17/119.15 cnf(261,plain, % 119.17/119.15 (P2(a9)), % 119.17/119.15 inference(scs_inference,[],[32,27,50,60])). % 119.17/119.15 cnf(286,plain, % 119.17/119.15 (~P4(f12(a1,a1))+P4(f12(x2861,a1))), % 119.17/119.15 inference(scs_inference,[],[118,156,67,248,37,25,23,3,20,238,237,46,86])). % 119.17/119.15 cnf(292,plain, % 119.17/119.16 (P3(f12(f6(x2921),f6(x2921)),f12(f12(x2921,x2921),f12(x2921,x2921)))), % 119.17/119.16 inference(scs_inference,[],[62,134,23])). % 119.17/119.16 cnf(293,plain, % 119.17/119.16 (E(x2931,f12(x2931,x2931))), % 119.17/119.16 inference(rename_variables,[],[62])). % 119.17/119.16 cnf(294,plain, % 119.17/119.16 (P3(f12(f12(f6(x2941),f6(x2941)),f12(f6(x2941),f6(x2941))),f12(f12(x2941,x2941),f12(x2941,x2941)))), % 119.17/119.16 inference(scs_inference,[],[62,293,134,23,22])). % 119.17/119.16 cnf(296,plain, % 119.17/119.16 (~P4(f12(a1,x2961))+P4(a1)), % 119.17/119.16 inference(scs_inference,[],[62,293,67,134,23,22,20])). % 119.17/119.16 cnf(302,plain, % 119.17/119.16 (P7(f12(f6(f12(a11,a11)),f6(f12(a11,a11))),f12(a11,a11))), % 119.17/119.16 inference(scs_inference,[],[94,143,53])). % 119.17/119.16 cnf(307,plain, % 119.17/119.16 (P3(f6(f12(f12(a1,x3071),f12(a1,x3071))),f12(f12(a1,x3072),f12(a1,x3072)))), % 119.17/119.16 inference(scs_inference,[],[217,246,94,41,143,39,53,3,23])). % 119.17/119.16 cnf(316,plain, % 119.17/119.16 (~P5(f12(f12(a1,x3161),f12(a1,x3161)))+P5(f12(f12(a1,x3162),f12(a1,x3162)))), % 119.17/119.16 inference(scs_inference,[],[217,19])). % 119.17/119.16 cnf(324,plain, % 119.17/119.16 (~P5(a1)+P5(f12(f12(a1,x3241),f12(a1,x3241)))), % 119.17/119.16 inference(scs_inference,[],[62,192,234,23,19])). % 119.17/119.16 cnf(325,plain, % 119.17/119.16 (P5(f12(f12(a1,x3251),f12(a1,x3251)))+~P5(f12(a1,x3252))), % 119.17/119.16 inference(scs_inference,[],[62,192,234,23,19,123])). % 119.17/119.16 cnf(339,plain, % 119.17/119.16 (P1(f12(f12(f12(a1,x3391),f12(a1,x3391)),f12(f12(a1,x3391),f12(a1,x3391))))), % 119.17/119.16 inference(scs_inference,[],[62,157,16])). % 119.17/119.16 cnf(341,plain, % 119.17/119.16 (~P7(x3411,f12(f12(f12(a1,x3412),f12(a1,x3412)),f12(f12(a1,x3412),f12(a1,x3412))))), % 119.17/119.16 inference(scs_inference,[],[62,157,16,50])). % 119.17/119.16 cnf(355,plain, % 119.17/119.16 (P1(f12(f12(a3,a3),f12(a3,a3)))), % 119.17/119.16 inference(scs_inference,[],[62,101,16])). % 119.17/119.16 cnf(357,plain, % 119.17/119.16 (~P7(x3571,f12(f12(a3,a3),f12(a3,a3)))), % 119.17/119.16 inference(scs_inference,[],[62,101,16,50])). % 119.17/119.16 cnf(361,plain, % 119.17/119.16 (~P5(a1)+P5(f12(a1,x3611))), % 119.17/119.16 inference(scs_inference,[],[100,62,101,16,50,60,19])). % 119.17/119.16 cnf(367,plain, % 119.17/119.16 (~P5(a1)+P5(f12(x3671,a1))), % 119.17/119.16 inference(scs_inference,[],[156,19])). % 119.17/119.16 cnf(368,plain, % 119.17/119.16 (P5(f12(x3681,a1))+~P5(f12(a1,x3682))), % 119.17/119.16 inference(scs_inference,[],[156,19,123])). % 119.17/119.16 cnf(381,plain, % 119.17/119.16 (~P2(a1)+P2(f12(a1,x3811))), % 119.17/119.16 inference(scs_inference,[],[100,208,19,24,21])). % 119.17/119.16 cnf(384,plain, % 119.17/119.16 (~P5(f12(f12(a1,x3841),f12(a1,x3841)))+P5(f12(a1,x3842))), % 119.17/119.16 inference(scs_inference,[],[183,19])). % 119.17/119.16 cnf(385,plain, % 119.17/119.16 (~P6(a1)+P6(f12(x3851,a1))), % 119.17/119.16 inference(scs_inference,[],[156,183,19,24])). % 119.17/119.16 cnf(386,plain, % 119.17/119.16 (~P2(a1)+P2(f12(x3861,a1))), % 119.17/119.16 inference(scs_inference,[],[156,183,19,24,21])). % 119.17/119.16 cnf(389,plain, % 119.17/119.16 (~P5(f12(a1,x3891))+P5(f12(a1,x3892))), % 119.17/119.16 inference(scs_inference,[],[140,19])). % 119.17/119.16 cnf(390,plain, % 119.17/119.16 (~P6(f12(f12(a1,x3901),f12(a1,x3901)))+P6(a1)), % 119.17/119.16 inference(scs_inference,[],[208,140,19,24])). % 119.17/119.16 cnf(394,plain, % 119.17/119.16 (~P5(f12(x3941,a1))+P5(a1)), % 119.17/119.16 inference(scs_inference,[],[37,19])). % 119.17/119.16 cnf(401,plain, % 119.17/119.16 (~P2(f12(a1,x4011))+P2(f12(f12(a1,x4012),f12(a1,x4012)))), % 119.17/119.16 inference(scs_inference,[],[67,165,40,19,24,21])). % 119.17/119.16 cnf(404,plain, % 119.17/119.16 (~P6(f12(a1,x4041))+P6(f12(f12(a1,x4042),f12(a1,x4042)))), % 119.17/119.16 inference(scs_inference,[],[165,24])). % 119.17/119.16 cnf(408,plain, % 119.17/119.16 (~P6(f12(a1,x4081))+P6(f12(a1,x4082))), % 119.17/119.16 inference(scs_inference,[],[140,24])). % 119.17/119.16 cnf(463,plain, % 119.17/119.16 (E(a1,f12(f12(f12(x4631,a1),f12(x4631,a1)),f12(f12(x4631,a1),f12(x4631,a1))))), % 119.17/119.16 inference(scs_inference,[],[230,45,2])). % 119.17/119.16 cnf(464,plain, % 119.17/119.16 (E(f12(f12(f12(x4641,a1),f12(x4641,a1)),f12(f12(x4641,a1),f12(x4641,a1))),a1)), % 119.17/119.16 inference(scs_inference,[],[463,2])). % 119.17/119.16 cnf(502,plain, % 119.17/119.16 (~P6(a1)+P6(f12(f12(f12(x5021,a1),f12(x5021,a1)),f12(f12(x5021,a1),f12(x5021,a1))))), % 119.17/119.16 inference(scs_inference,[],[463,464,19,24])). % 119.17/119.16 cnf(551,plain, % 119.17/119.16 (~P5(f12(a1,x5511))+P5(f14(a1,x5512))), % 119.17/119.16 inference(scs_inference,[],[52,123])). % 119.17/119.16 cnf(582,plain, % 119.17/119.16 (P3(f6(a1),f12(f12(f12(x5821,a1),f12(x5821,a1)),f12(f12(x5821,a1),f12(x5821,a1))))), % 119.17/119.16 inference(scs_inference,[],[463,39,23])). % 119.17/119.16 cnf(642,plain, % 119.17/119.16 (~P5(a1)+P5(f14(f12(a1,x6421),x6422))), % 119.17/119.16 inference(scs_inference,[],[361,52])). % 119.17/119.16 cnf(736,plain, % 119.17/119.16 (~P6(f12(a1,a1))+P6(f12(x7361,a1))), % 119.17/119.16 inference(scs_inference,[],[385,88])). % 119.17/119.16 cnf(832,plain, % 119.17/119.16 (~P1(f12(f15(f16(x8321),f15(x8321,x8322)),f15(f16(x8321),f15(x8321,x8322))))), % 119.17/119.16 inference(scs_inference,[],[70,38,16])). % 119.17/119.16 cnf(994,plain, % 119.17/119.16 (P4(f12(x9941,a1))), % 119.17/119.16 inference(scs_inference,[],[131,286,46])). % 119.17/119.16 cnf(996,plain, % 119.17/119.16 (P4(a1)), % 119.17/119.16 inference(scs_inference,[],[994,296])). % 119.17/119.16 cnf(1002,plain, % 119.17/119.16 (P4(f12(f12(x10021,a1),f12(x10021,a1)))), % 119.17/119.16 inference(scs_inference,[],[62,994,20])). % 119.17/119.16 cnf(1009,plain, % 119.17/119.16 (~P5(f12(a1,a1))+P6(f12(a1,x10091))), % 119.17/119.16 inference(scs_inference,[],[62,131,994,20,49,404,408])). % 119.17/119.16 cnf(1015,plain, % 119.17/119.16 (P4(f12(f12(a1,x10151),f12(a1,x10151)))), % 119.17/119.16 inference(scs_inference,[],[996,252])). % 119.17/119.16 cnf(1208,plain, % 119.17/119.16 (~P5(f12(f12(a1,x12081),f12(a1,x12081)))+P5(f14(a1,x12082))), % 119.17/119.16 inference(scs_inference,[],[551,384])). % 119.17/119.16 cnf(1278,plain, % 119.17/119.16 (P6(f12(a1,x12781))+~P5(a1)), % 119.17/119.16 inference(scs_inference,[],[1009,361])). % 119.17/119.16 cnf(1294,plain, % 119.17/119.16 (P6(f12(x12941,a1))+~P5(a1)), % 119.17/119.16 inference(scs_inference,[],[1278,736])). % 119.17/119.16 cnf(1310,plain, % 119.17/119.16 (P6(f12(x13101,a1))+~P5(f12(a1,x13102))), % 119.17/119.16 inference(scs_inference,[],[1294,123])). % 119.17/119.16 cnf(1342,plain, % 119.17/119.16 (P6(f12(f12(a1,x13421),f12(a1,x13421)))+~P5(f12(a1,x13422))), % 119.17/119.16 inference(scs_inference,[],[1310,404])). % 119.17/119.16 cnf(1359,plain, % 119.17/119.16 (P4(f12(a9,a9))), % 119.17/119.16 inference(scs_inference,[],[29,62,20])). % 119.17/119.16 cnf(1473,plain, % 119.17/119.16 (P5(f12(f12(a1,x14731),f12(a1,x14731)))+~P5(f12(x14732,a1))), % 119.17/119.16 inference(scs_inference,[],[324,394])). % 119.17/119.16 cnf(1611,plain, % 119.17/119.16 (P5(f12(a4,a4))), % 119.17/119.16 inference(scs_inference,[],[31,62,19])). % 119.17/119.16 cnf(1731,plain, % 119.17/119.16 (P5(f12(a9,a9))), % 119.17/119.16 inference(scs_inference,[],[32,62,19])). % 119.17/119.16 cnf(1807,plain, % 119.17/119.16 (P5(f14(a1,x18071))+~P5(f12(x18072,a1))), % 119.17/119.16 inference(scs_inference,[],[1208,1473])). % 119.17/119.16 cnf(1823,plain, % 119.17/119.16 (~P5(f12(x18231,a1))+P5(f14(f14(a1,x18232),x18233))), % 119.17/119.16 inference(scs_inference,[],[1807,52])). % 119.17/119.16 cnf(1853,plain, % 119.17/119.16 (P5(f12(a10,a10))), % 119.17/119.16 inference(scs_inference,[],[33,62,19])). % 119.17/119.16 cnf(1976,plain, % 119.17/119.16 (P4(f12(f12(a9,a9),f12(a9,a9)))), % 119.17/119.16 inference(scs_inference,[],[1359,62,20])). % 119.17/119.16 cnf(2232,plain, % 119.17/119.16 (E(f12(x22321,x22321),x22321)), % 119.17/119.16 inference(rename_variables,[],[38])). % 119.17/119.16 cnf(2234,plain, % 119.17/119.16 (E(f12(x22341,x22341),x22341)), % 119.17/119.16 inference(rename_variables,[],[38])). % 119.17/119.16 cnf(2235,plain, % 119.17/119.16 (P3(f6(a1),f12(a1,x22351))), % 119.17/119.16 inference(scs_inference,[],[38,2232,2234,167,234,302,23,17,22])). % 119.17/119.16 cnf(2240,plain, % 119.17/119.16 (P3(f12(f6(f12(x22401,x22401)),f6(f12(x22401,x22401))),x22401)), % 119.17/119.16 inference(scs_inference,[],[38,94,23])). % 119.17/119.16 cnf(2242,plain, % 119.17/119.16 (P3(f6(x22421),f12(f12(x22421,x22421),f12(x22421,x22421)))), % 119.17/119.16 inference(scs_inference,[],[38,292,94,23,22])). % 119.17/119.16 cnf(2246,plain, % 119.17/119.16 (P3(f6(f12(f12(a1,x22461),f12(a1,x22461))),f12(a1,x22462))), % 119.17/119.16 inference(scs_inference,[],[38,307,23])). % 119.17/119.16 cnf(2247,plain, % 119.17/119.16 (E(f12(x22471,x22471),x22471)), % 119.17/119.16 inference(rename_variables,[],[38])). % 119.17/119.16 cnf(2248,plain, % 119.17/119.16 (P3(f6(f12(x22481,x22481)),x22481)), % 119.17/119.16 inference(scs_inference,[],[38,2247,307,2240,23,22])). % 119.17/119.16 cnf(2254,plain, % 119.17/119.16 (P3(f12(f6(a1),f6(a1)),f12(f12(x22541,a1),f12(x22541,a1)))), % 119.17/119.16 inference(scs_inference,[],[38,62,582,23,22])). % 119.17/119.16 cnf(2264,plain, % 119.17/119.16 (P3(f6(f12(f12(x22641,x22641),f12(x22641,x22641))),x22641)), % 119.17/119.16 inference(scs_inference,[],[38,2248,23])). % 119.17/119.16 cnf(2268,plain, % 119.17/119.16 (P3(f12(f6(a1),f6(a1)),f12(x22681,a1))), % 119.17/119.16 inference(scs_inference,[],[38,2254,23])). % 119.17/119.16 cnf(2415,plain, % 119.17/119.16 (P7(f6(f15(f15(x24151,x24152),f16(x24151))),f15(f15(x24151,x24152),f16(x24151)))), % 119.17/119.16 inference(scs_inference,[],[39,44,53])). % 119.17/119.16 cnf(2418,plain, % 119.17/119.16 (~E(f15(f15(x24181,x24182),f16(x24181)),a1)), % 119.17/119.16 inference(scs_inference,[],[39,63,44,53,18])). % 119.17/119.16 cnf(2422,plain, % 119.17/119.16 (~P7(f15(f15(x24221,x24222),f16(x24221)),f6(f15(f15(x24221,x24222),f16(x24221))))), % 119.17/119.16 inference(scs_inference,[],[39,62,2268,63,44,53,18,22,54])). % 119.17/119.16 cnf(2425,plain, % 119.17/119.16 (~E(f15(f16(x24251),f15(x24251,x24252)),f12(a3,a3))), % 119.17/119.16 inference(scs_inference,[],[128,111,18])). % 119.17/119.16 cnf(2431,plain, % 119.17/119.16 (~E(f15(f16(x24311),f15(x24311,x24312)),a3)), % 119.17/119.16 inference(scs_inference,[],[96,111,18])). % 119.17/119.16 cnf(2435,plain, % 119.17/119.16 (~E(f15(f16(x24351),f15(x24351,x24352)),f12(a1,x24353))), % 119.17/119.16 inference(scs_inference,[],[154,111,18])). % 119.17/119.16 cnf(2440,plain, % 119.17/119.16 (~E(f15(f16(x24401),f15(x24401,x24402)),f12(x24403,a1))), % 119.17/119.16 inference(scs_inference,[],[206,111,18])). % 119.17/119.16 cnf(2562,plain, % 119.17/119.16 (P3(f6(f12(f15(x25621,x25622),f15(x25621,x25622))),f15(x25622,x25621))), % 119.17/119.16 inference(scs_inference,[],[40,2248,23])). % 119.17/119.16 cnf(2566,plain, % 119.17/119.16 (P3(f6(f15(x25661,x25662)),f15(x25662,x25661))), % 119.17/119.16 inference(scs_inference,[],[40,39,23])). % 119.17/119.16 cnf(2685,plain, % 119.17/119.16 (P3(f12(f6(f12(x26851,x26852)),f6(f12(x26851,x26852))),f12(x26852,x26851))), % 119.17/119.16 inference(scs_inference,[],[41,94,23])). % 119.17/119.16 cnf(2693,plain, % 119.17/119.16 (P3(f6(f12(f15(x26931,x26932),f15(x26931,x26932))),f12(f15(x26932,x26931),f15(x26932,x26931)))), % 119.17/119.16 inference(scs_inference,[],[62,2562,23])). % 119.17/119.16 cnf(2701,plain, % 119.17/119.16 (P3(f6(f12(f12(a1,x27011),f12(a1,x27011))),f12(x27012,a1))), % 119.17/119.16 inference(scs_inference,[],[41,2246,23])). % 119.17/119.16 cnf(2712,plain, % 119.17/119.16 (P3(f6(f12(f12(x27121,x27122),f12(x27121,x27122))),f12(x27122,x27121))), % 119.17/119.16 inference(scs_inference,[],[41,2248,23])). % 119.17/119.16 cnf(2716,plain, % 119.17/119.16 (P3(f6(f12(x27161,x27162)),f12(x27162,x27161))), % 119.17/119.16 inference(scs_inference,[],[41,39,23])). % 119.17/119.16 cnf(2779,plain, % 119.17/119.16 (P6(f12(f12(x27791,a1),f12(x27791,a1)))+~P6(a1)), % 119.17/119.16 inference(scs_inference,[],[502,88])). % 119.17/119.16 cnf(2795,plain, % 119.17/119.16 (P6(f12(f12(x27951,a1),f12(x27951,a1)))+~P6(f12(f12(a1,x27952),f12(a1,x27952)))), % 119.17/119.16 inference(scs_inference,[],[2779,390])). % 119.17/119.16 cnf(2811,plain, % 119.17/119.16 (~P5(f12(f12(a1,a1),f12(a1,a1)))+P6(f12(f12(x28111,a1),f12(x28111,a1)))), % 119.17/119.16 inference(scs_inference,[],[1002,157,2795,49])). % 119.17/119.16 cnf(2827,plain, % 119.17/119.16 (P6(f12(f12(x28271,a1),f12(x28271,a1)))+~P5(f12(f12(a1,x28272),f12(a1,x28272)))), % 119.17/119.16 inference(scs_inference,[],[2811,316])). % 119.17/119.16 cnf(2846,plain, % 119.17/119.16 (P6(f12(f12(x28461,a1),f12(x28461,a1)))+~P5(a1)), % 119.17/119.16 inference(scs_inference,[],[2827,324])). % 119.17/119.16 cnf(2862,plain, % 119.17/119.16 (P6(f12(f12(x28621,a1),f12(x28621,a1)))+~P5(f12(a1,x28622))), % 119.17/119.16 inference(scs_inference,[],[2846,123])). % 119.17/119.16 cnf(2954,plain, % 119.17/119.16 (~P1(f12(f15(f15(x29541,x29542),f16(x29541)),f15(f15(x29541,x29542),f16(x29541))))), % 119.17/119.16 inference(scs_inference,[],[44,62,2701,38,23,16])). % 119.17/119.16 cnf(3091,plain, % 119.17/119.16 (P3(f12(f6(f12(x30911,x30912)),f6(f12(x30911,x30912))),f12(f12(x30912,x30911),f12(x30912,x30911)))), % 119.17/119.16 inference(scs_inference,[],[62,2685,23])). % 119.17/119.16 cnf(3099,plain, % 119.17/119.16 (P3(f6(f12(x30991,x30992)),f12(f12(x30992,x30991),f12(x30992,x30991)))), % 119.17/119.16 inference(scs_inference,[],[62,2716,23])). % 119.17/119.16 cnf(3103,plain, % 119.17/119.16 (P3(f6(x31031),f12(f12(f12(x31031,x31031),f12(x31031,x31031)),f12(f12(x31031,x31031),f12(x31031,x31031))))), % 119.17/119.16 inference(scs_inference,[],[62,2242,23])). % 119.17/119.16 cnf(3339,plain, % 119.17/119.16 (P5(f12(f12(a5,a5),f12(a5,a5)))), % 119.17/119.16 inference(scs_inference,[],[65,62,19])). % 119.17/119.16 cnf(3446,plain, % 119.17/119.16 (P5(f14(a5,x34461))), % 119.17/119.16 inference(scs_inference,[],[34,52])). % 119.17/119.16 cnf(3454,plain, % 119.17/119.16 (E(f14(f12(a1,x34541),x34542),f14(f12(f12(a1,x34543),f12(a1,x34543)),x34542))), % 119.17/119.16 inference(scs_inference,[],[34,165,52,8,9,10,11,6,7,12])). % 119.17/119.16 cnf(3458,plain, % 119.17/119.16 (E(f12(a5,f2(x34581,x34581)),f14(a5,x34581))), % 119.17/119.16 inference(scs_inference,[],[34,165,52,8,9,10,11,6,7,12,13,14,15,55])). % 119.17/119.16 cnf(3460,plain, % 119.17/119.16 (E(f12(x34601,f12(a1,x34602)),f12(x34601,f12(f12(a1,x34603),f12(a1,x34603))))), % 119.17/119.16 inference(scs_inference,[],[34,165,52,8,9,10,11,6,7,12,13,14,15,55,5])). % 119.17/119.16 cnf(3461,plain, % 119.17/119.16 (E(f12(f12(a1,x34611),x34612),f12(f12(f12(a1,x34613),f12(a1,x34613)),x34612))), % 119.17/119.16 inference(scs_inference,[],[34,165,52,8,9,10,11,6,7,12,13,14,15,55,5,4])). % 119.17/119.16 cnf(3462,plain, % 119.17/119.16 (E(f12(f12(a3,a3),f12(a3,a3)),a1)), % 119.17/119.16 inference(scs_inference,[],[34,355,165,52,8,9,10,11,6,7,12,13,14,15,55,5,4,45])). % 119.17/119.16 cnf(3465,plain, % 119.17/119.16 (~E(a11,f12(f12(a3,a3),f12(a3,a3)))), % 119.17/119.16 inference(scs_inference,[],[34,2425,357,355,165,52,8,9,10,11,6,7,12,13,14,15,55,5,4,45,2,85])). % 119.17/119.16 cnf(3467,plain, % 119.17/119.16 (P4(f12(f12(a3,a3),f12(a3,a3)))), % 119.17/119.16 inference(scs_inference,[],[34,2425,357,355,165,52,8,9,10,11,6,7,12,13,14,15,55,5,4,45,2,85,46])). % 119.17/119.16 cnf(3469,plain, % 119.17/119.16 (~E(f7(f14(a5,a13)),f8(f14(a5,a13)))), % 119.17/119.16 inference(scs_inference,[],[34,43,2425,357,355,165,52,8,9,10,11,6,7,12,13,14,15,55,5,4,45,2,85,46,48])). % 119.17/119.16 cnf(3471,plain, % 119.17/119.16 (~P7(x34711,f14(a9,x34712))), % 119.17/119.16 inference(scs_inference,[],[34,43,2425,357,355,32,259,165,52,8,9,10,11,6,7,12,13,14,15,55,5,4,45,2,85,46,48,56])). % 119.17/119.16 cnf(3473,plain, % 119.17/119.16 (~E(a9,f14(a5,a13))), % 119.17/119.16 inference(scs_inference,[],[34,261,43,2425,357,355,32,259,165,52,8,9,10,11,6,7,12,13,14,15,55,5,4,45,2,85,46,48,56,21])). % 119.17/119.16 cnf(3474,plain, % 119.17/119.16 (P1(f14(a9,x34741))), % 119.17/119.16 inference(scs_inference,[],[34,261,43,2425,357,2264,355,32,259,165,52,8,9,10,11,6,7,12,13,14,15,55,5,4,45,2,85,46,48,56,21,53])). % 119.17/119.16 cnf(3477,plain, % 119.17/119.16 (~E(f15(f15(x34771,x34772),f16(x34771)),f12(a3,a3))), % 119.17/119.16 inference(scs_inference,[],[34,261,43,2425,357,2264,355,32,259,165,40,52,8,9,10,11,6,7,12,13,14,15,55,5,4,45,2,85,46,48,56,21,53,3])). % 119.17/119.16 cnf(3478,plain, % 119.17/119.16 (E(f15(x34781,x34782),f15(x34782,x34781))), % 119.17/119.16 inference(rename_variables,[],[40])). % 119.17/119.16 cnf(3479,plain, % 119.17/119.16 (P7(f6(f15(f15(x34791,x34792),f16(x34791))),f15(f16(x34791),f15(x34791,x34792)))), % 119.17/119.16 inference(scs_inference,[],[34,261,43,2425,357,2264,2415,355,32,259,165,40,3478,52,8,9,10,11,6,7,12,13,14,15,55,5,4,45,2,85,46,48,56,21,53,3,18])). % 119.17/119.16 cnf(3481,plain, % 119.17/119.16 (~E(f12(f12(a3,a3),f12(a3,a3)),f12(f15(f16(x34811),f15(x34811,x34812)),f15(f16(x34811),f15(x34811,x34812))))), % 119.17/119.16 inference(scs_inference,[],[34,261,43,2425,357,2264,2415,832,355,32,259,165,40,3478,52,8,9,10,11,6,7,12,13,14,15,55,5,4,45,2,85,46,48,56,21,53,3,18,16])). % 119.17/119.16 cnf(3482,plain, % 119.17/119.16 (P5(f12(f14(a5,a13),f14(a5,a13)))), % 119.17/119.16 inference(scs_inference,[],[34,261,43,2425,357,2264,2415,832,355,32,259,165,40,3478,62,52,8,9,10,11,6,7,12,13,14,15,55,5,4,45,2,85,46,48,56,21,53,3,18,16,19])). % 119.17/119.16 cnf(3484,plain, % 119.17/119.16 (~P7(f15(f16(x34841),f15(x34841,x34842)),f6(f15(f15(x34841,x34842),f16(x34841))))), % 119.17/119.16 inference(scs_inference,[],[34,261,43,2425,357,2264,2415,832,355,32,259,165,40,3478,62,52,8,9,10,11,6,7,12,13,14,15,55,5,4,45,2,85,46,48,56,21,53,3,18,16,19,54])). % 119.17/119.16 cnf(3486,plain, % 119.17/119.16 (P4(f12(a3,a3))), % 119.17/119.16 inference(scs_inference,[],[34,261,43,2425,357,2264,2415,832,355,32,259,165,40,3478,62,52,8,9,10,11,6,7,12,13,14,15,55,5,4,45,2,85,46,48,56,21,53,3,18,16,19,54,86])). % 119.17/119.16 cnf(3495,plain, % 119.17/119.16 (E(f14(a9,x34951),a1)), % 119.17/119.16 inference(scs_inference,[],[1611,3474,3458,55,12,7,10,45])). % 119.17/119.16 cnf(3500,plain, % 119.17/119.16 (P5(f14(f12(a4,a4),x35001))), % 119.17/119.16 inference(scs_inference,[],[1611,3474,3458,55,12,7,10,45,9,13,4,52])). % 119.17/119.16 cnf(3508,plain, % 119.17/119.16 (~E(f14(a5,a13),a9)), % 119.17/119.16 inference(scs_inference,[],[1611,3474,3473,3458,55,12,7,10,45,9,13,4,52,6,14,8,11,15,5,2])). % 119.17/119.16 cnf(3510,plain, % 119.17/119.16 (~E(a11,f14(a9,x35101))), % 119.17/119.16 inference(scs_inference,[],[1611,3486,3471,3474,3473,3458,55,12,7,10,45,9,13,4,52,6,14,8,11,15,5,2,86,85])). % 119.17/119.16 cnf(3514,plain, % 119.17/119.16 (~E(f12(a5,a5),f14(a5,a13))), % 119.17/119.16 inference(scs_inference,[],[1611,3486,3471,66,3474,3473,3458,43,55,12,7,10,45,9,13,4,52,6,14,8,11,15,5,2,86,85,46,21])). % 119.17/119.16 cnf(3515,plain, % 119.17/119.16 (~P7(x35151,f12(f12(f12(a1,a1),f12(a1,a1)),f12(a1,x35152)))), % 119.17/119.16 inference(scs_inference,[],[1611,3486,3471,66,3474,3473,3458,244,3460,43,55,12,7,10,45,9,13,4,52,6,14,8,11,15,5,2,86,85,46,21,18])). % 119.17/119.16 cnf(3517,plain, % 119.17/119.16 (E(f12(x35171,f12(a1,x35172)),f12(x35171,f12(f12(a1,x35173),f12(a1,x35173))))), % 119.17/119.16 inference(rename_variables,[],[3460])). % 119.17/119.16 cnf(3522,plain, % 119.17/119.16 (P4(f12(f12(a1,x35221),f12(f12(a1,x35222),f12(a1,x35222))))), % 119.17/119.16 inference(scs_inference,[],[80,1611,3486,3471,66,3474,3473,3458,3462,2954,244,3460,3517,3481,1015,43,55,12,7,10,45,9,13,4,52,6,14,8,11,15,5,2,86,85,46,21,18,3,16,56,20])). % 119.17/119.16 cnf(3534,plain, % 119.17/119.16 (P5(f14(f12(a9,a9),x35341))), % 119.17/119.16 inference(scs_inference,[],[1731,339,55,45,52])). % 119.17/119.16 cnf(3537,plain, % 119.17/119.16 (E(f15(x35371,f14(a9,x35372)),f15(x35371,a1))), % 119.17/119.16 inference(scs_inference,[],[1731,3495,339,55,45,52,10,7])). % 119.17/119.16 cnf(3538,plain, % 119.17/119.16 (E(f14(x35381,f14(a9,x35382)),f14(x35381,a1))), % 119.17/119.16 inference(scs_inference,[],[1731,3495,339,55,45,52,10,7,13])). % 119.17/119.16 cnf(3539,plain, % 119.17/119.16 (E(f12(f14(a9,x35391),x35392),f12(a1,x35392))), % 119.17/119.16 inference(scs_inference,[],[1731,3495,339,55,45,52,10,7,13,4])). % 119.17/119.16 cnf(3540,plain, % 119.17/119.16 (E(f14(f14(a9,x35401),x35402),f14(a1,x35402))), % 119.17/119.16 inference(scs_inference,[],[1731,3495,339,55,45,52,10,7,13,4,12])). % 119.17/119.16 cnf(3541,plain, % 119.17/119.16 (E(f6(f14(a9,x35411)),f6(a1))), % 119.17/119.16 inference(scs_inference,[],[1731,3495,339,55,45,52,10,7,13,4,12,8])). % 119.17/119.16 cnf(3543,plain, % 119.17/119.16 (E(f15(f14(a9,x35431),x35432),f15(a1,x35432))), % 119.17/119.16 inference(scs_inference,[],[1731,3495,339,55,45,52,10,7,13,4,12,8,9,6])). % 119.17/119.16 cnf(3547,plain, % 119.17/119.16 (E(f12(x35471,f14(a9,x35472)),f12(x35471,a1))), % 119.17/119.16 inference(scs_inference,[],[1731,3495,339,55,45,52,10,7,13,4,12,8,9,6,15,14,11,5])). % 119.17/119.16 cnf(3548,plain, % 119.17/119.16 (~E(f14(a5,a13),f12(a5,a5))), % 119.17/119.16 inference(scs_inference,[],[1731,3514,3495,339,55,45,52,10,7,13,4,12,8,9,6,15,14,11,5,2])). % 119.17/119.16 cnf(3549,plain, % 119.17/119.16 (~E(a11,f12(f12(x35491,a1),f12(x35491,a1)))), % 119.17/119.16 inference(scs_inference,[],[1731,3514,3495,226,339,55,45,52,10,7,13,4,12,8,9,6,15,14,11,5,2,85])). % 119.17/119.16 cnf(3551,plain, % 119.17/119.16 (P1(f12(f12(f12(a1,a1),f12(a1,a1)),f12(a1,x35511)))), % 119.17/119.16 inference(scs_inference,[],[1731,3514,3495,226,3515,213,339,55,45,52,10,7,13,4,12,8,9,6,15,14,11,5,2,85,53])). % 119.17/119.16 cnf(3552,plain, % 119.17/119.16 (~P7(x35521,f12(f12(f12(a1,a1),f12(a1,a1)),f12(a1,x35522)))), % 119.17/119.16 inference(rename_variables,[],[3515])). % 119.17/119.16 cnf(3555,plain, % 119.17/119.16 (~P7(f15(f15(x35551,x35552),f16(x35551)),f6(f15(f16(x35551),f15(x35551,x35552))))), % 119.17/119.16 inference(scs_inference,[],[1731,3514,3495,226,3515,228,213,339,40,55,45,52,10,7,13,4,12,8,9,6,15,14,11,5,2,85,53,17])). % 119.17/119.16 cnf(3557,plain, % 119.17/119.16 (~P7(x35571,f12(f12(a1,x35572),f12(a1,x35573)))), % 119.17/119.16 inference(scs_inference,[],[1731,3514,3495,226,3515,3552,228,3461,213,339,40,55,45,52,10,7,13,4,12,8,9,6,15,14,11,5,2,85,53,17,18])). % 119.17/119.16 cnf(3559,plain, % 119.17/119.16 (~E(f12(f14(a5,a13),f14(a5,a13)),a9)), % 119.17/119.16 inference(scs_inference,[],[1731,3514,3508,3495,226,3515,3552,228,3461,213,339,40,62,55,45,52,10,7,13,4,12,8,9,6,15,14,11,5,2,85,53,17,18,3])). % 119.17/119.16 cnf(3562,plain, % 119.17/119.16 (P7(x35621,a5)+~P7(x35621,f14(a5,x35622))), % 119.17/119.16 inference(scs_inference,[],[34,1731,3514,3508,3495,226,3515,3552,228,3461,213,339,832,27,40,62,55,45,52,10,7,13,4,12,8,9,6,15,14,11,5,2,85,53,17,18,3,16,56])). % 119.17/119.16 cnf(3589,plain, % 119.17/119.16 (E(f15(f15(x35891,f14(a9,x35892)),x35893),f15(f15(x35891,a1),x35893))), % 119.17/119.16 inference(scs_inference,[],[3537,3534,3551,52,45,10,4,12,55,13,7,8,9,15,6])). % 119.17/119.16 cnf(3592,plain, % 119.17/119.16 (E(f12(x35921,f15(x35922,f14(a9,x35923))),f12(x35921,f15(x35922,a1)))), % 119.17/119.16 inference(scs_inference,[],[3537,3534,3551,52,45,10,4,12,55,13,7,8,9,15,6,11,14,5])). % 119.17/119.16 cnf(3596,plain, % 119.17/119.16 (~E(a11,f12(f12(a1,x35961),f12(a1,x35962)))), % 119.17/119.16 inference(scs_inference,[],[3510,3537,3534,3557,3551,52,45,10,4,12,55,13,7,8,9,15,6,11,14,5,2,46,85])). % 119.17/119.16 cnf(3597,plain, % 119.17/119.16 (~P7(x35971,f12(f12(a1,x35972),f12(a1,x35973)))), % 119.17/119.16 inference(rename_variables,[],[3557])). % 119.17/119.16 cnf(3598,plain, % 119.17/119.16 (P1(f12(f12(a1,x35981),f12(a1,x35982)))), % 119.17/119.16 inference(scs_inference,[],[3510,3537,3534,3557,3597,3551,2716,52,45,10,4,12,55,13,7,8,9,15,6,11,14,5,2,46,85,53])). % 119.17/119.16 cnf(3602,plain, % 119.17/119.16 (~P7(f12(f12(a11,a11),f12(a11,a11)),f6(a11))), % 119.17/119.16 inference(scs_inference,[],[98,3510,3537,3534,3557,3597,3551,2716,38,52,45,10,4,12,55,13,7,8,9,15,6,11,14,5,2,46,85,53,17])). % 119.17/119.16 cnf(3604,plain, % 119.17/119.16 (~P7(x36041,f12(f12(f12(a1,x36042),f12(a1,x36042)),f12(a1,x36043)))), % 119.17/119.16 inference(scs_inference,[],[98,3510,3537,3534,3557,3597,3551,341,3460,2716,38,52,45,10,4,12,55,13,7,8,9,15,6,11,14,5,2,46,85,53,17,18])). % 119.17/119.16 cnf(3610,plain, % 119.17/119.16 (~E(f12(f12(f12(a1,a1),f12(a1,a1)),f12(a1,x36101)),f12(a11,a11))), % 119.17/119.16 inference(scs_inference,[],[98,3510,3537,3543,3534,3557,3597,3551,341,3460,2716,143,38,52,45,10,4,12,55,13,7,8,9,15,6,11,14,5,2,46,85,53,17,18,3,16])). % 119.17/119.16 cnf(3620,plain, % 119.17/119.16 (P5(f14(f12(a10,a10),x36201))), % 119.17/119.16 inference(scs_inference,[],[3598,1853,45,55,52])). % 119.17/119.16 cnf(3633,plain, % 119.17/119.16 (~E(f12(a3,a3),f15(f15(x36331,x36332),f16(x36331)))), % 119.17/119.16 inference(scs_inference,[],[3477,3538,3598,1853,45,55,52,4,10,13,7,12,8,9,6,15,14,11,2])). % 119.17/119.16 cnf(3638,plain, % 119.17/119.16 (~P7(x36381,f12(f12(f12(a1,x36382),f12(a1,x36382)),f12(a1,x36383)))), % 119.17/119.16 inference(rename_variables,[],[3604])). % 119.17/119.16 cnf(3639,plain, % 119.17/119.16 (~E(a5,f14(a5,a13))), % 119.17/119.16 inference(scs_inference,[],[3477,3538,3598,3604,1853,36,43,45,55,52,4,10,13,7,12,8,9,6,15,14,11,2,5,46,85,21])). % 119.17/119.16 cnf(3640,plain, % 119.17/119.16 (P1(f12(f12(f12(a1,x36401),f12(a1,x36401)),f12(a1,x36402)))), % 119.17/119.16 inference(scs_inference,[],[3477,3538,3598,3604,3638,1853,2712,36,43,45,55,52,4,10,13,7,12,8,9,6,15,14,11,2,5,46,85,21,53])). % 119.17/119.16 cnf(3644,plain, % 119.17/119.16 (~P7(f15(f15(x36441,f14(a9,x36442)),f16(x36441)),f6(f15(f15(x36441,a1),f16(x36441))))), % 119.17/119.16 inference(scs_inference,[],[3477,3538,3598,3604,3638,3589,2422,1853,2712,36,43,45,55,52,4,10,13,7,12,8,9,6,15,14,11,2,5,46,85,21,53,17])). % 119.17/119.16 cnf(3647,plain, % 119.17/119.16 (~P7(x36471,f12(x36472,f14(a9,x36473)))), % 119.17/119.16 inference(scs_inference,[],[3477,3538,3547,3598,3604,3638,3589,2422,1853,2712,206,36,43,45,55,52,4,10,13,7,12,8,9,6,15,14,11,2,5,46,85,21,53,17,18])). % 119.17/119.16 cnf(3649,plain, % 119.17/119.16 (~E(f12(f14(a5,a13),f14(a5,a13)),f12(a5,a5))), % 119.17/119.16 inference(scs_inference,[],[3548,3477,3538,3547,3598,3604,3638,3589,2422,1853,2712,206,36,43,62,45,55,52,4,10,13,7,12,8,9,6,15,14,11,2,5,46,85,21,53,17,18,3])). % 119.17/119.16 cnf(3660,plain, % 119.17/119.16 (E(f12(f12(f12(a1,x36601),f12(a1,x36601)),f12(a1,x36602)),a1)), % 119.17/119.16 inference(scs_inference,[],[3620,3640,52,55,45])). % 119.17/119.16 cnf(3662,plain, % 119.17/119.16 (E(f12(f12(f14(a9,x36621),x36622),x36623),f12(f12(a1,x36622),x36623))), % 119.17/119.16 inference(scs_inference,[],[3539,3620,3640,52,55,45,4])). % 119.17/119.16 cnf(3673,plain, % 119.17/119.16 (E(f12(x36731,f12(f14(a9,x36732),x36733)),f12(x36731,f12(a1,x36733)))), % 119.17/119.16 inference(scs_inference,[],[3539,3620,3640,52,55,45,4,7,12,10,13,8,9,15,6,11,14,5])). % 119.17/119.16 cnf(3674,plain, % 119.17/119.16 (~E(f14(a5,a13),a5)), % 119.17/119.16 inference(scs_inference,[],[3639,3539,3620,3640,52,55,45,4,7,12,10,13,8,9,15,6,11,14,5,2])). % 119.17/119.16 cnf(3677,plain, % 119.17/119.16 (~E(a11,f12(x36771,f14(a9,x36772)))), % 119.17/119.16 inference(scs_inference,[],[3639,3539,3620,3647,3640,52,55,45,4,7,12,10,13,8,9,15,6,11,14,5,2,46,85])). % 119.17/119.16 cnf(3678,plain, % 119.17/119.16 (~P7(x36781,f12(x36782,f14(a9,x36783)))), % 119.17/119.16 inference(rename_variables,[],[3647])). % 119.17/119.16 cnf(3679,plain, % 119.17/119.16 (P1(f12(x36791,f14(a9,x36792)))), % 119.17/119.16 inference(scs_inference,[],[3639,3539,3620,3647,3678,3640,2264,52,55,45,4,7,12,10,13,8,9,15,6,11,14,5,2,46,85,53])). % 119.17/119.16 cnf(3683,plain, % 119.17/119.16 (~P7(f12(f12(a11,a11),f12(a11,a11)),f12(f6(a11),f6(a11)))), % 119.17/119.16 inference(scs_inference,[],[3639,3539,3620,3647,3678,3640,3602,2264,38,52,55,45,4,7,12,10,13,8,9,15,6,11,14,5,2,46,85,53,18])). % 119.17/119.16 cnf(3685,plain, % 119.17/119.16 (E(f12(f14(a9,x36851),f15(x36852,f14(a9,x36853))),f12(a1,f15(x36852,a1)))), % 119.17/119.16 inference(scs_inference,[],[3639,3539,3620,3647,3678,3640,3592,3602,2264,38,52,55,45,4,7,12,10,13,8,9,15,6,11,14,5,2,46,85,53,18,3])). % 119.17/119.16 cnf(3696,plain, % 119.17/119.16 (P7(f15(f15(f8(f14(a5,a13)),f7(f14(a5,a13))),f16(f8(f14(a5,a13)))),a5)), % 119.17/119.16 inference(scs_inference,[],[43,3446,3562,59])). % 119.17/119.16 cnf(3697,plain, % 119.17/119.16 (E(f12(x36971,f14(a9,x36972)),a1)), % 119.17/119.16 inference(scs_inference,[],[3679,45])). % 119.17/119.16 cnf(3720,plain, % 119.17/119.16 (~P7(f15(f15(x37201,f14(a9,x37202)),f16(x37201)),f6(f15(f16(x37201),f15(x37201,a1))))), % 119.17/119.16 inference(scs_inference,[],[3649,3679,3660,3555,3339,341,3589,45,55,52,4,10,13,7,12,8,9,6,15,14,11,46,2,5,85,17])). % 119.17/119.16 cnf(3723,plain, % 119.17/119.16 (~P7(x37231,f12(f12(a1,a1),f12(f14(a9,x37232),a1)))), % 119.17/119.16 inference(scs_inference,[],[3649,3679,3660,3673,3555,3339,226,341,3589,45,55,52,4,10,13,7,12,8,9,6,15,14,11,46,2,5,85,17,18])). % 119.17/119.16 cnf(3726,plain, % 119.17/119.16 (~E(f12(f14(a5,a13),f14(a5,a13)),a5)), % 119.17/119.16 inference(scs_inference,[],[3674,3649,3679,3660,3673,3555,3339,226,341,3589,62,45,55,52,4,10,13,7,12,8,9,6,15,14,11,46,2,5,85,17,18,3])). % 119.17/119.16 cnf(3728,plain, % 119.17/119.16 (~E(f12(x37281,f14(a9,x37282)),f15(f16(x37283),f15(x37283,x37284)))), % 119.17/119.16 inference(scs_inference,[],[3674,3649,3679,3660,3673,3555,3339,226,341,3589,70,62,45,55,52,4,10,13,7,12,8,9,6,15,14,11,46,2,5,85,17,18,3,16])). % 119.17/119.16 cnf(3736,plain, % 119.17/119.16 (P1(f12(f12(a1,a1),f12(f14(a9,x37361),a1)))), % 119.17/119.16 inference(scs_inference,[],[3674,3649,3679,3660,3522,3673,3555,3339,3091,226,341,33,2685,3589,3461,70,3462,62,45,55,52,4,10,13,7,12,8,9,6,15,14,11,46,2,5,85,17,18,3,16,60,20,23,53])). % 119.17/119.16 cnf(3745,plain, % 119.17/119.16 (E(f12(f12(a1,a1),f12(f14(a9,x37451),a1)),a1)), % 119.17/119.16 inference(scs_inference,[],[3736,3500,55,52,45])). % 119.17/119.16 cnf(3747,plain, % 119.17/119.16 (E(f12(f12(x37471,f14(a9,x37472)),x37473),f12(a1,x37473))), % 119.17/119.16 inference(scs_inference,[],[3697,3736,3500,55,52,45,4])). % 119.17/119.16 cnf(3748,plain, % 119.17/119.16 (E(f15(x37481,f12(x37482,f14(a9,x37483))),f15(x37481,a1))), % 119.17/119.16 inference(scs_inference,[],[3697,3736,3500,55,52,45,4,7])). % 119.17/119.16 cnf(3749,plain, % 119.17/119.16 (E(f14(f12(x37491,f14(a9,x37492)),x37493),f14(a1,x37493))), % 119.17/119.16 inference(scs_inference,[],[3697,3736,3500,55,52,45,4,7,12])). % 119.17/119.16 cnf(3750,plain, % 119.17/119.16 (E(f14(x37501,f12(x37502,f14(a9,x37503))),f14(x37501,a1))), % 119.17/119.16 inference(scs_inference,[],[3697,3736,3500,55,52,45,4,7,12,13])). % 119.17/119.16 cnf(3755,plain, % 119.17/119.16 (E(f15(f12(x37551,f14(a9,x37552)),x37553),f15(a1,x37553))), % 119.17/119.16 inference(scs_inference,[],[3697,3736,3500,55,52,45,4,7,12,13,10,8,9,15,6])). % 119.17/119.16 cnf(3761,plain, % 119.17/119.16 (E(f12(x37611,f12(x37612,f14(a9,x37613))),f12(x37611,a1))), % 119.17/119.16 inference(scs_inference,[],[2435,3697,3736,3500,55,52,45,4,7,12,13,10,8,9,15,6,46,11,14,2,5])). % 119.17/119.16 cnf(3763,plain, % 119.17/119.16 (~P7(x37631,f12(f12(a1,a1),f12(f14(a9,x37632),a1)))), % 119.17/119.16 inference(rename_variables,[],[3723])). % 119.17/119.16 cnf(3766,plain, % 119.17/119.16 (~P7(x37661,f12(f12(f14(a9,x37662),a1),f12(f14(a9,x37663),a1)))), % 119.17/119.16 inference(scs_inference,[],[2435,3697,3728,3723,3763,3736,3500,3662,55,52,45,4,7,12,13,10,8,9,15,6,46,11,14,2,5,85,3,18])). % 119.17/119.16 cnf(3782,plain, % 119.17/119.16 (E(f12(a3,a3),a1)), % 119.17/119.16 inference(scs_inference,[],[3482,101,52,45])). % 119.17/119.16 cnf(3800,plain, % 119.17/119.16 (~P7(x38001,f12(f12(f14(a9,x38002),a1),f12(f14(a9,x38003),a1)))), % 119.17/119.16 inference(rename_variables,[],[3766])). % 119.17/119.16 cnf(3801,plain, % 119.17/119.16 (P1(f12(f12(f14(a9,x38011),a1),f12(f14(a9,x38012),a1)))), % 119.17/119.16 inference(scs_inference,[],[2440,3766,3800,3540,3482,2240,101,52,45,55,4,13,10,12,7,8,9,6,15,11,14,2,5,85,53])). % 119.17/119.16 cnf(3805,plain, % 119.17/119.16 (~E(f12(a11,a11),f12(f12(a3,a3),f12(a3,a3)))), % 119.17/119.16 inference(scs_inference,[],[2440,3465,3766,3800,3540,3482,2240,101,62,52,45,55,4,13,10,12,7,8,9,6,15,11,14,2,5,85,53,3])). % 119.17/119.16 cnf(3808,plain, % 119.17/119.16 (~P7(x38081,f12(x38082,f12(x38083,f14(a9,x38084))))), % 119.17/119.16 inference(scs_inference,[],[2440,3465,3761,3766,3800,3540,3482,2240,832,101,206,62,52,45,55,4,13,10,12,7,8,9,6,15,11,14,2,5,85,53,3,16,18])). % 119.17/119.16 cnf(3818,plain, % 119.17/119.16 (P5(f14(f14(a5,x38181),x38182))), % 119.17/119.16 inference(scs_inference,[],[3801,3446,45,55,52])). % 119.17/119.16 cnf(3820,plain, % 119.17/119.16 (E(f12(f12(a3,a3),x38201),f12(a1,x38201))), % 119.17/119.16 inference(scs_inference,[],[3782,3801,3446,45,55,52,4])). % 119.17/119.16 cnf(3821,plain, % 119.17/119.16 (E(f15(x38211,f12(a3,a3)),f15(x38211,a1))), % 119.17/119.16 inference(scs_inference,[],[3782,3801,3446,45,55,52,4,7])). % 119.17/119.16 cnf(3822,plain, % 119.17/119.16 (E(f14(f12(a3,a3),x38221),f14(a1,x38221))), % 119.17/119.16 inference(scs_inference,[],[3782,3801,3446,45,55,52,4,7,12])). % 119.17/119.16 cnf(3823,plain, % 119.17/119.16 (E(f8(f12(a3,a3)),f8(a1))), % 119.17/119.16 inference(scs_inference,[],[3782,3801,3446,45,55,52,4,7,12,10])). % 119.17/119.16 cnf(3824,plain, % 119.17/119.16 (E(f14(x38241,f12(a3,a3)),f14(x38241,a1))), % 119.17/119.16 inference(scs_inference,[],[3782,3801,3446,45,55,52,4,7,12,10,13])). % 119.17/119.16 cnf(3825,plain, % 119.17/119.16 (E(f6(f12(a3,a3)),f6(a1))), % 119.17/119.16 inference(scs_inference,[],[3782,3801,3446,45,55,52,4,7,12,10,13,8])). % 119.17/119.16 cnf(3827,plain, % 119.17/119.16 (E(f2(x38271,f12(a3,a3)),f2(x38271,a1))), % 119.17/119.16 inference(scs_inference,[],[3782,3801,3446,45,55,52,4,7,12,10,13,8,9,15])). % 119.17/119.16 cnf(3830,plain, % 119.17/119.16 (E(f15(f12(a3,a3),x38301),f15(a1,x38301))), % 119.17/119.16 inference(scs_inference,[],[3782,3801,3446,45,55,52,4,7,12,10,13,8,9,15,46,6])). % 119.17/119.16 cnf(3832,plain, % 119.17/119.16 (E(f2(f12(a3,a3),x38321),f2(a1,x38321))), % 119.17/119.16 inference(scs_inference,[],[3782,3801,3446,45,55,52,4,7,12,10,13,8,9,15,46,6,11,14])). % 119.17/119.16 cnf(3833,plain, % 119.17/119.16 (~E(f12(f12(a3,a3),f12(a3,a3)),f12(a11,a11))), % 119.17/119.16 inference(scs_inference,[],[3782,3805,3801,3446,45,55,52,4,7,12,10,13,8,9,15,46,6,11,14,2])). % 119.17/119.16 cnf(3834,plain, % 119.17/119.16 (E(f12(x38341,f12(a3,a3)),f12(x38341,a1))), % 119.17/119.16 inference(scs_inference,[],[3782,3805,3801,3446,45,55,52,4,7,12,10,13,8,9,15,46,6,11,14,2,5])). % 119.17/119.16 cnf(3840,plain, % 119.17/119.16 (~P7(x38401,f12(f12(a1,x38402),f12(f14(a9,x38403),x38404)))), % 119.17/119.16 inference(scs_inference,[],[3782,3805,3748,3755,3808,3801,3673,3446,3557,45,55,52,4,7,12,10,13,8,9,15,46,6,11,14,2,5,85,3,18])). % 119.17/119.16 cnf(3869,plain, % 119.17/119.16 (E(a3,a1)), % 119.17/119.16 inference(scs_inference,[],[3818,26,55,52,45])). % 119.17/119.16 cnf(3871,plain, % 119.17/119.16 (E(f12(f12(f12(a3,a3),x38711),x38712),f12(f12(a1,x38711),x38712))), % 119.17/119.16 inference(scs_inference,[],[3820,3818,26,55,52,45,4])). % 119.17/119.16 cnf(3882,plain, % 119.17/119.16 (~E(a1,f15(f15(x38821,x38822),f16(x38821)))), % 119.17/119.16 inference(scs_inference,[],[3820,3818,2418,26,55,52,45,4,10,13,12,7,8,9,15,6,11,14,2])). % 119.17/119.16 cnf(3883,plain, % 119.17/119.16 (E(f12(x38831,f12(f12(a3,a3),x38832)),f12(x38831,f12(a1,x38832)))), % 119.17/119.16 inference(scs_inference,[],[3820,3818,2418,26,55,52,45,4,10,13,12,7,8,9,15,6,11,14,2,5])). % 119.17/119.16 cnf(3886,plain, % 119.17/119.16 (P1(f12(f12(f14(a9,x38861),f14(a9,x38861)),f12(f14(a9,x38861),f14(a9,x38861))))), % 119.17/119.16 inference(scs_inference,[],[3820,3818,2418,3840,294,3808,26,55,52,45,4,10,13,12,7,8,9,15,6,11,14,2,5,85,53])). % 119.17/119.16 cnf(3890,plain, % 119.17/119.16 (~E(f12(a1,f12(a3,a3)),f12(a11,a11))), % 119.17/119.16 inference(scs_inference,[],[3833,3820,3818,2418,3840,294,3808,26,55,52,45,4,10,13,12,7,8,9,15,6,11,14,2,5,85,53,3])). % 119.17/119.16 cnf(3892,plain, % 119.17/119.16 (~E(f12(x38921,f14(a9,x38922)),f12(f15(f15(x38923,x38924),f16(x38923)),f15(f15(x38923,x38924),f16(x38923))))), % 119.17/119.16 inference(scs_inference,[],[3833,3820,3818,2418,3840,294,3808,2954,3679,26,55,52,45,4,10,13,12,7,8,9,15,6,11,14,2,5,85,53,3,16])). % 119.17/119.16 cnf(3893,plain, % 119.17/119.16 (~P7(x38931,f12(f14(a9,x38932),f15(x38933,f14(a9,x38934))))), % 119.17/119.16 inference(scs_inference,[],[3833,3820,3818,2418,3840,3685,294,3808,2954,154,3679,26,55,52,45,4,10,13,12,7,8,9,15,6,11,14,2,5,85,53,3,16,18])). % 119.17/119.16 cnf(3902,plain, % 119.17/119.16 (P5(f14(f12(a5,a5),x39021))), % 119.17/119.16 inference(scs_inference,[],[65,52])). % 119.17/119.16 cnf(3904,plain, % 119.17/119.16 (E(f12(f12(f14(a9,x39041),f14(a9,x39041)),f12(f14(a9,x39041),f14(a9,x39041))),a1)), % 119.17/119.16 inference(scs_inference,[],[3886,65,52,45])). % 119.17/119.16 cnf(3908,plain, % 119.17/119.16 (E(f12(a3,x39081),f12(a1,x39081))), % 119.17/119.16 inference(scs_inference,[],[3869,3886,65,52,45,55,4])). % 119.17/119.16 cnf(3909,plain, % 119.17/119.16 (E(f14(a3,x39091),f14(a1,x39091))), % 119.17/119.16 inference(scs_inference,[],[3869,3886,65,52,45,55,4,12])). % 119.17/119.16 cnf(3911,plain, % 119.17/119.16 (E(f14(x39111,a3),f14(x39111,a1))), % 119.17/119.16 inference(scs_inference,[],[3869,3886,65,52,45,55,4,12,7,13])). % 119.17/119.16 cnf(3912,plain, % 119.17/119.16 (E(f8(a3),f8(a1))), % 119.17/119.16 inference(scs_inference,[],[3869,3886,65,52,45,55,4,12,7,13,10])). % 119.17/119.16 cnf(3913,plain, % 119.17/119.16 (E(f6(a3),f6(a1))), % 119.17/119.16 inference(scs_inference,[],[3869,3886,65,52,45,55,4,12,7,13,10,8])). % 119.17/119.16 cnf(3914,plain, % 119.17/119.16 (E(f16(a3),f16(a1))), % 119.17/119.16 inference(scs_inference,[],[3869,3886,65,52,45,55,4,12,7,13,10,8,9])). % 119.17/119.16 cnf(3915,plain, % 119.17/119.16 (E(f15(a3,x39151),f15(a1,x39151))), % 119.17/119.16 inference(scs_inference,[],[3869,3886,65,52,45,55,4,12,7,13,10,8,9,6])). % 119.17/119.16 cnf(3916,plain, % 119.17/119.16 (E(f2(x39161,a3),f2(x39161,a1))), % 119.17/119.16 inference(scs_inference,[],[3869,3886,65,52,45,55,4,12,7,13,10,8,9,6,15])). % 119.17/119.16 cnf(3917,plain, % 119.17/119.16 (E(f2(a3,x39171),f2(a1,x39171))), % 119.17/119.16 inference(scs_inference,[],[3869,3886,65,52,45,55,4,12,7,13,10,8,9,6,15,14])). % 119.17/119.16 cnf(3918,plain, % 119.17/119.16 (E(f7(a3),f7(a1))), % 119.17/119.16 inference(scs_inference,[],[3869,3886,65,52,45,55,4,12,7,13,10,8,9,6,15,14,11])). % 119.17/119.16 cnf(3920,plain, % 119.17/119.16 (E(f12(x39201,a3),f12(x39201,a1))), % 119.17/119.16 inference(scs_inference,[],[3869,2431,3886,65,52,45,55,4,12,7,13,10,8,9,6,15,14,11,2,5])). % 119.17/119.16 cnf(3922,plain, % 119.17/119.16 (~P7(x39221,f12(f14(a9,x39222),f15(x39223,f14(a9,x39224))))), % 119.17/119.16 inference(rename_variables,[],[3893])). % 119.17/119.16 cnf(3925,plain, % 119.17/119.16 (E(f12(f12(f12(a3,a3),x39251),x39252),f12(f12(a1,x39251),x39252))), % 119.17/119.16 inference(rename_variables,[],[3871])). % 119.17/119.16 cnf(3927,plain, % 119.17/119.16 (P3(f6(f12(x39271,x39272)),f12(x39272,x39271))), % 119.17/119.16 inference(rename_variables,[],[2716])). % 119.17/119.16 cnf(3928,plain, % 119.17/119.16 (P1(f12(f14(a9,x39281),f15(x39282,f14(a9,x39283))))), % 119.17/119.16 inference(scs_inference,[],[3869,2431,3893,3922,3745,3871,3886,65,1002,2716,3927,52,45,55,4,12,7,13,10,8,9,6,15,14,11,2,5,85,20,23,53])). % 119.17/119.16 cnf(3935,plain, % 119.17/119.16 (~P7(x39351,f12(f12(f12(a3,a3),x39352),f12(f14(a9,x39353),x39354)))), % 119.17/119.16 inference(scs_inference,[],[3869,2431,3749,3750,3893,3922,3745,3871,3925,3886,3840,65,1002,2716,3927,52,45,55,4,12,7,13,10,8,9,6,15,14,11,2,5,85,20,23,53,3,18])). % 119.17/119.16 cnf(3953,plain, % 119.17/119.16 (E(f2(f12(a3,x39531),x39532),f2(f12(a1,x39531),x39532))), % 119.17/119.16 inference(scs_inference,[],[3908,11,14])). % 119.17/119.16 cnf(3956,plain, % 119.17/119.16 (E(f12(x39561,f12(a3,x39562)),f12(x39561,f12(a1,x39562)))), % 119.17/119.16 inference(scs_inference,[],[3908,3726,11,14,2,8,5])). % 119.17/119.16 cnf(3966,plain, % 119.17/119.16 (E(f2(x39661,f12(a3,x39662)),f2(x39661,f12(a1,x39662)))), % 119.17/119.16 inference(scs_inference,[],[3908,3902,3726,3928,3935,11,14,2,8,5,45,9,55,52,85,15])). % 119.17/119.16 cnf(3967,plain, % 119.17/119.16 (E(f12(f12(a3,x39671),x39672),f12(f12(a1,x39671),x39672))), % 119.17/119.16 inference(scs_inference,[],[3908,3902,3726,3928,3935,11,14,2,8,5,45,9,55,52,85,15,4])). % 119.17/119.16 cnf(3975,plain, % 119.17/119.16 (~E(f12(a1,a1),f12(a11,a11))), % 119.17/119.16 inference(scs_inference,[],[3908,3913,3890,3902,3726,3928,3935,3834,3103,11,14,2,8,5,45,9,55,52,85,15,4,6,13,10,7,12,22,3])). % 119.17/119.16 cnf(3977,plain, % 119.17/119.16 (~P7(x39771,f12(x39772,a3))), % 119.17/119.16 inference(scs_inference,[],[3908,3920,3913,3890,3902,3726,3928,3935,3834,3103,206,11,14,2,8,5,45,9,55,52,85,15,4,6,13,10,7,12,22,3,18])). % 119.17/119.17 cnf(3980,plain, % 119.17/119.17 (P7(f6(f15(f16(x39801),f15(x39801,x39802))),f15(f15(x39801,x39802),f16(x39801)))), % 119.17/119.17 inference(scs_inference,[],[3908,3920,3913,3890,3902,3726,3928,3935,3834,3103,2566,44,206,11,14,2,8,5,45,9,55,52,85,15,4,6,13,10,7,12,22,3,18,16,53])). % 119.17/119.17 cnf(3992,plain, % 119.17/119.17 (E(f12(a4,f2(x39921,x39921)),f14(a4,x39921))), % 119.17/119.17 inference(scs_inference,[],[3559,3909,31,14,11,8,2,55])). % 119.17/119.17 cnf(3995,plain, % 119.17/119.17 (E(a9,a1)), % 119.17/119.17 inference(scs_inference,[],[3559,3909,31,27,14,11,8,2,55,5,45])). % 119.17/119.17 cnf(3998,plain, % 119.17/119.17 (P5(f14(a4,x39981))), % 119.17/119.17 inference(scs_inference,[],[3559,3909,31,27,14,11,8,2,55,5,45,9,52])). % 119.17/119.17 cnf(4000,plain, % 119.17/119.17 (~E(a11,f12(x40001,a3))), % 119.17/119.17 inference(scs_inference,[],[3977,3559,3909,31,27,14,11,8,2,55,5,45,9,52,85])). % 119.17/119.17 cnf(4002,plain, % 119.17/119.17 (E(f12(f14(a3,x40021),x40022),f12(f14(a1,x40021),x40022))), % 119.17/119.17 inference(scs_inference,[],[3977,3559,3909,31,27,14,11,8,2,55,5,45,9,52,85,4])). % 119.17/119.17 cnf(4008,plain, % 119.17/119.17 (E(f14(f14(a3,x40081),x40082),f14(f14(a1,x40081),x40082))), % 119.17/119.17 inference(scs_inference,[],[3977,3559,3909,31,27,14,11,8,2,55,5,45,9,52,85,4,15,6,13,10,7,12])). % 119.17/119.17 cnf(4012,plain, % 119.17/119.17 (~P7(x40121,f12(f12(f14(a9,x40122),x40123),f12(f12(a3,a3),x40124)))), % 119.17/119.17 inference(scs_inference,[],[3977,3559,3953,3966,3909,3935,31,27,41,14,11,8,2,55,5,45,9,52,85,4,15,6,13,10,7,12,3,18])). % 119.17/119.17 cnf(4015,plain, % 119.17/119.17 (P1(f12(f12(f12(a3,a3),x40151),f12(f14(a9,x40152),x40153)))), % 119.17/119.17 inference(scs_inference,[],[3977,3559,3953,3966,3909,3935,339,2712,31,27,143,41,14,11,8,2,55,5,45,9,52,85,4,15,6,13,10,7,12,3,18,16,53])). % 119.17/119.17 cnf(4034,plain, % 119.17/119.17 (E(f2(a9,x40341),f2(a1,x40341))), % 119.17/119.17 inference(scs_inference,[],[3995,4015,46,14])). % 119.17/119.17 cnf(4035,plain, % 119.17/119.17 (E(f7(a9),f7(a1))), % 119.17/119.17 inference(scs_inference,[],[3995,4015,46,14,11])). % 119.17/119.17 cnf(4036,plain, % 119.17/119.17 (E(f6(a9),f6(a1))), % 119.17/119.17 inference(scs_inference,[],[3995,4015,46,14,11,8])). % 119.17/119.17 cnf(4040,plain, % 119.17/119.17 (E(f12(x40401,a9),f12(x40401,a1))), % 119.17/119.17 inference(scs_inference,[],[3995,3998,4000,4015,46,14,11,8,2,55,5])). % 119.17/119.17 cnf(4043,plain, % 119.17/119.17 (E(f16(a9),f16(a1))), % 119.17/119.17 inference(scs_inference,[],[3995,3998,4000,4015,46,14,11,8,2,55,5,45,9])). % 119.17/119.17 cnf(4044,plain, % 119.17/119.17 (P5(f14(f14(a4,x40441),x40442))), % 119.17/119.17 inference(scs_inference,[],[3995,3998,4000,4015,46,14,11,8,2,55,5,45,9,52])). % 119.17/119.17 cnf(4047,plain, % 119.17/119.17 (~P7(x40471,f12(f12(f14(a9,x40472),x40473),f12(f12(a3,a3),x40474)))), % 119.17/119.17 inference(rename_variables,[],[4012])). % 119.17/119.17 cnf(4048,plain, % 119.17/119.17 (E(f12(a9,x40481),f12(a1,x40481))), % 119.17/119.17 inference(scs_inference,[],[3995,3998,4000,4012,4015,46,14,11,8,2,55,5,45,9,52,85,4])). % 119.17/119.17 cnf(4049,plain, % 119.17/119.17 (E(f2(x40491,a9),f2(x40491,a1))), % 119.17/119.17 inference(scs_inference,[],[3995,3998,4000,4012,4015,46,14,11,8,2,55,5,45,9,52,85,4,15])). % 119.17/119.17 cnf(4050,plain, % 119.17/119.17 (E(f15(a9,x40501),f15(a1,x40501))), % 119.17/119.17 inference(scs_inference,[],[3995,3998,4000,4012,4015,46,14,11,8,2,55,5,45,9,52,85,4,15,6])). % 119.17/119.17 cnf(4051,plain, % 119.17/119.17 (E(f14(x40511,a9),f14(x40511,a1))), % 119.17/119.17 inference(scs_inference,[],[3995,3998,4000,4012,4015,46,14,11,8,2,55,5,45,9,52,85,4,15,6,13])). % 119.17/119.17 cnf(4053,plain, % 119.17/119.17 (E(f8(a9),f8(a1))), % 119.17/119.17 inference(scs_inference,[],[3995,3998,4000,4012,4015,46,14,11,8,2,55,5,45,9,52,85,4,15,6,13,7,10])). % 119.17/119.17 cnf(4057,plain, % 119.17/119.17 (~P7(x40571,f12(f12(f12(a1,x40572),f12(a1,x40572)),f12(a3,x40573)))), % 119.17/119.17 inference(scs_inference,[],[3995,3975,3998,4000,4012,4015,3956,3604,140,46,14,11,8,2,55,5,45,9,52,85,4,15,6,13,7,10,12,3,18])). % 119.17/119.17 cnf(4060,plain, % 119.17/119.17 (P1(f12(f12(f14(a9,x40601),x40602),f12(f12(a3,a3),x40603)))), % 119.17/119.17 inference(scs_inference,[],[3995,3975,3998,4000,4012,4047,4015,3956,3604,2264,832,3598,140,46,14,11,8,2,55,5,45,9,52,85,4,15,6,13,7,10,12,3,18,16,53])). % 119.17/119.17 cnf(4064,plain, % 119.17/119.17 (P5(a1)), % 119.17/119.17 inference(scs_inference,[],[3995,3975,3998,4000,4012,4047,4015,3956,3604,2264,832,3598,32,140,46,14,11,8,2,55,5,45,9,52,85,4,15,6,13,7,10,12,3,18,16,53,19])). % 119.17/119.17 cnf(4067,plain, % 119.17/119.17 (P2(a1)), % 119.17/119.17 inference(scs_inference,[],[3995,3975,3998,4000,4012,4047,4015,3956,996,3604,2264,832,3598,32,25,140,46,14,11,8,2,55,5,45,9,52,85,4,15,6,13,7,10,12,3,18,16,53,19,49,82])). % 119.17/119.17 cnf(4070,plain, % 119.17/119.17 (~E(a1,f14(a5,a13))), % 119.17/119.17 inference(scs_inference,[],[3995,3975,3998,4000,4012,4047,4015,3956,3683,996,3604,2264,832,3598,32,43,25,140,46,14,11,8,2,55,5,45,9,52,85,4,15,6,13,7,10,12,3,18,16,53,19,49,82,56,21])). % 119.17/119.17 cnf(4076,plain, % 119.17/119.17 (P5(f12(a1,x40761))), % 119.17/119.17 inference(scs_inference,[],[4064,361])). % 119.17/119.17 cnf(4080,plain, % 119.17/119.17 (P5(f12(x40801,a1))), % 119.17/119.17 inference(scs_inference,[],[4064,367])). % 119.17/119.17 cnf(4081,plain, % 119.17/119.17 (P2(f12(a1,x40811))), % 119.17/119.17 inference(scs_inference,[],[4067,381])). % 119.17/119.17 cnf(4082,plain, % 119.17/119.17 (P2(f12(x40821,a1))), % 119.17/119.17 inference(scs_inference,[],[4067,386])). % 119.17/119.17 cnf(4087,plain, % 119.17/119.17 (P5(f14(f12(a1,x40871),x40872))), % 119.17/119.17 inference(scs_inference,[],[4064,642])). % 119.17/119.17 cnf(4105,plain, % 119.17/119.17 (~E(f14(a5,a13),a1)), % 119.17/119.17 inference(scs_inference,[],[4034,4070,4060,46,14,11,8,2])). % 119.17/119.17 cnf(4106,plain, % 119.17/119.17 (E(f12(a1,f2(x41061,x41061)),f14(a1,x41061))), % 119.17/119.17 inference(scs_inference,[],[4064,4034,4070,4060,46,14,11,8,2,55])). % 119.17/119.17 cnf(4108,plain, % 119.17/119.17 (E(f12(x41081,f2(a9,x41082)),f12(x41081,f2(a1,x41082)))), % 119.17/119.17 inference(scs_inference,[],[4064,4034,4070,4060,46,14,11,8,2,55,5])). % 119.17/119.17 cnf(4112,plain, % 119.17/119.17 (P5(f14(a1,x41121))), % 119.17/119.17 inference(scs_inference,[],[4064,4034,4070,4060,46,14,11,8,2,55,5,45,9,52])). % 119.17/119.17 cnf(4115,plain, % 119.17/119.17 (~P7(x41151,f12(f12(f12(a1,x41152),f12(a1,x41152)),f12(a3,x41153)))), % 119.17/119.17 inference(rename_variables,[],[4057])). % 119.17/119.17 cnf(4116,plain, % 119.17/119.17 (E(f12(f2(a9,x41161),x41162),f12(f2(a1,x41161),x41162))), % 119.17/119.17 inference(scs_inference,[],[4064,4034,4070,4057,4060,46,14,11,8,2,55,5,45,9,52,85,4])). % 119.17/119.17 cnf(4123,plain, % 119.17/119.17 (E(f2(a9,a9),f2(a1,a1))), % 119.17/119.17 inference(scs_inference,[],[4064,4034,4049,4070,4057,4060,46,14,11,8,2,55,5,45,9,52,85,4,15,6,13,7,10,12,3])). % 119.17/119.17 cnf(4126,plain, % 119.17/119.17 (~P7(x41261,f14(a1,x41262))), % 119.17/119.17 inference(scs_inference,[],[4064,4034,4049,4070,4057,4060,63,46,14,11,8,2,55,5,45,9,52,85,4,15,6,13,7,10,12,3,56])). % 119.17/119.17 cnf(4129,plain, % 119.17/119.17 (~P7(x41291,f12(f12(f12(a1,x41292),f12(a1,x41292)),f12(a3,x41293)))), % 119.17/119.17 inference(rename_variables,[],[4057])). % 119.17/119.17 cnf(4131,plain, % 119.17/119.17 (P2(f14(a1,x41311))), % 119.17/119.17 inference(scs_inference,[],[4064,4034,4049,4070,4057,4115,4060,3461,63,46,14,11,8,2,55,5,45,9,52,85,4,15,6,13,7,10,12,3,56,18,59])). % 119.17/119.17 cnf(4134,plain, % 119.17/119.17 (P1(f12(f12(f12(a1,x41341),f12(a1,x41341)),f12(a3,x41342)))), % 119.17/119.17 inference(scs_inference,[],[4064,4034,4049,4070,4057,4115,4129,4060,2685,3461,42,63,46,14,11,8,2,55,5,45,9,52,85,4,15,6,13,7,10,12,3,56,18,59,16,53])). % 119.17/119.17 cnf(4140,plain, % 119.17/119.17 (P3(f6(f12(f15(x41401,a9),f15(x41401,a9))),f15(a1,x41401))), % 119.17/119.17 inference(scs_inference,[],[4064,4034,4049,4050,4070,4057,4115,4129,4060,3967,3467,2562,2685,3461,42,63,46,14,11,8,2,55,5,45,9,52,85,4,15,6,13,7,10,12,3,56,18,59,16,53,20,23])). % 119.17/119.17 cnf(4146,plain, % 119.17/119.17 (P5(f12(f12(a1,x41461),f12(a1,x41461)))), % 119.17/119.17 inference(scs_inference,[],[4076,325])). % 119.17/119.17 cnf(4147,plain, % 119.17/119.17 (P5(f12(x41471,a1))), % 119.17/119.17 inference(scs_inference,[],[4076,368])). % 119.17/119.17 cnf(4148,plain, % 119.17/119.17 (P5(f12(a1,x41481))), % 119.17/119.17 inference(scs_inference,[],[4076,389])). % 119.17/119.17 cnf(4149,plain, % 119.17/119.17 (P2(f12(f12(a1,x41491),f12(a1,x41491)))), % 119.17/119.17 inference(scs_inference,[],[4081,401])). % 119.17/119.17 cnf(4154,plain, % 119.17/119.17 (P6(f12(f12(a1,x41541),f12(a1,x41541)))), % 119.17/119.17 inference(scs_inference,[],[4076,1342])). % 119.17/119.17 cnf(4155,plain, % 119.17/119.17 (P5(f12(f12(a1,x41551),f12(a1,x41551)))), % 119.17/119.17 inference(scs_inference,[],[4076,1473])). % 119.17/119.17 cnf(4159,plain, % 119.17/119.17 (P5(f14(f14(a1,x41591),x41592))), % 119.17/119.17 inference(scs_inference,[],[4076,1823])). % 119.17/119.17 cnf(4165,plain, % 119.17/119.17 (P6(f12(f12(x41651,a1),f12(x41651,a1)))), % 119.17/119.17 inference(scs_inference,[],[4076,2862])). % 119.17/119.17 cnf(4180,plain, % 119.17/119.17 (E(f12(f12(a1,x41801),f2(x41802,x41802)),f14(f12(a1,x41801),x41802))), % 119.17/119.17 inference(scs_inference,[],[4040,4076,3677,4134,46,14,11,8,2,55])). % 119.17/119.17 cnf(4182,plain, % 119.17/119.17 (E(f12(x41821,f12(x41822,a9)),f12(x41821,f12(x41822,a1)))), % 119.17/119.17 inference(scs_inference,[],[4040,4076,3677,4134,46,14,11,8,2,55,5])). % 119.17/119.17 cnf(4183,plain, % 119.17/119.17 (E(f12(f12(f12(a1,x41831),f12(a1,x41831)),f12(a3,x41832)),a1)), % 119.17/119.17 inference(scs_inference,[],[4040,4076,3677,4134,46,14,11,8,2,55,5,45])). % 119.17/119.17 cnf(4186,plain, % 119.17/119.17 (P5(f14(f12(x41861,a1),x41862))), % 119.17/119.17 inference(scs_inference,[],[4040,4076,4080,3677,4134,46,14,11,8,2,55,5,45,9,52])). % 119.17/119.17 cnf(4188,plain, % 119.17/119.17 (~E(a11,f14(a1,x41881))), % 119.17/119.17 inference(scs_inference,[],[4126,4040,4076,4080,3677,4134,46,14,11,8,2,55,5,45,9,52,85])). % 119.17/119.17 cnf(4189,plain, % 119.17/119.17 (~P7(x41891,f14(a1,x41892))), % 119.17/119.17 inference(rename_variables,[],[4126])). % 119.17/119.17 cnf(4190,plain, % 119.17/119.17 (E(f12(f12(x41901,a9),x41902),f12(f12(x41901,a1),x41902))), % 119.17/119.17 inference(scs_inference,[],[4126,4040,4076,4080,3677,4134,46,14,11,8,2,55,5,45,9,52,85,4])). % 119.17/119.17 cnf(4193,plain, % 119.17/119.17 (E(f14(x41931,f12(x41932,a9)),f14(x41931,f12(x41932,a1)))), % 119.17/119.17 inference(scs_inference,[],[4126,4040,4076,4080,3677,4134,46,14,11,8,2,55,5,45,9,52,85,4,15,6,13])). % 119.17/119.17 cnf(4197,plain, % 119.17/119.17 (~P7(x41971,f14(f14(a1,x41972),x41973))), % 119.17/119.17 inference(scs_inference,[],[4126,4189,4040,4076,4080,4112,3677,4134,46,14,11,8,2,55,5,45,9,52,85,4,15,6,13,7,10,12,56])). % 119.17/119.17 cnf(4198,plain, % 119.17/119.17 (~P7(x41981,f14(a1,x41982))), % 119.17/119.17 inference(rename_variables,[],[4126])). % 119.17/119.17 cnf(4200,plain, % 119.17/119.17 (~E(f12(f14(a5,a13),f14(a5,a13)),a1)), % 119.17/119.17 inference(scs_inference,[],[4126,4189,4040,4076,4080,4112,4105,3677,4134,62,46,14,11,8,2,55,5,45,9,52,85,4,15,6,13,7,10,12,56,3])). % 119.17/119.17 cnf(4205,plain, % 119.17/119.17 (P1(f14(a1,x42051))), % 119.17/119.17 inference(scs_inference,[],[4126,4189,4198,4040,4076,4080,4112,4105,3677,4008,4134,2240,2954,355,62,46,14,11,8,2,55,5,45,9,52,85,4,15,6,13,7,10,12,56,3,18,16,53])). % 119.17/119.17 cnf(4218,plain, % 119.17/119.17 (~E(f14(a1,x42181),a11)), % 119.17/119.17 inference(scs_inference,[],[4205,4188,4183,46,14,11,8,2])). % 119.17/119.17 cnf(4222,plain, % 119.17/119.17 (E(f14(a1,x42221),a1)), % 119.17/119.17 inference(scs_inference,[],[4205,4188,4186,4183,46,14,11,8,2,55,5,45])). % 119.17/119.17 cnf(4224,plain, % 119.17/119.17 (P5(f14(f14(f12(a1,x42241),x42242),x42243))), % 119.17/119.17 inference(scs_inference,[],[4205,4188,4087,4186,4183,46,14,11,8,2,55,5,45,52])). % 119.17/119.17 cnf(4227,plain, % 119.17/119.17 (~E(a11,f14(f14(a1,x42271),x42272))), % 119.17/119.17 inference(scs_inference,[],[4205,4188,4197,4087,4186,4183,46,14,11,8,2,55,5,45,52,9,85])). % 119.17/119.17 cnf(4228,plain, % 119.17/119.17 (~P7(x42281,f14(f14(a1,x42282),x42283))), % 119.17/119.17 inference(rename_variables,[],[4197])). % 119.17/119.17 cnf(4235,plain, % 119.17/119.17 (E(f14(f12(f12(f12(a1,x42351),f12(a1,x42351)),f12(a3,x42352)),x42353),f14(a1,x42353))), % 119.17/119.17 inference(scs_inference,[],[4205,4188,4197,4087,4186,4183,46,14,11,8,2,55,5,45,52,9,85,4,15,6,13,7,10,12])). % 119.17/119.17 cnf(4236,plain, % 119.17/119.17 (~P7(x42361,f14(f12(a1,a1),x42362))), % 119.17/119.17 inference(scs_inference,[],[4147,4205,4188,4197,4087,4186,4183,154,46,14,11,8,2,55,5,45,52,9,85,4,15,6,13,7,10,12,56])). % 119.17/119.17 cnf(4243,plain, % 119.17/119.17 (~P7(x42431,f12(f12(f14(a9,x42432),a1),f12(f14(a9,x42433),a9)))), % 119.17/119.17 inference(scs_inference,[],[4147,4205,4188,4197,4087,4186,4180,4182,4193,4183,3766,154,46,14,11,8,2,55,5,45,52,9,85,4,15,6,13,7,10,12,56,3,18])). % 119.17/119.17 cnf(4245,plain, % 119.17/119.17 (~E(f14(a1,x42451),f15(f16(x42452),f15(x42452,x42453)))), % 119.17/119.17 inference(scs_inference,[],[4147,4205,4188,4197,4087,4186,4180,4182,4193,4183,3766,154,70,46,14,11,8,2,55,5,45,52,9,85,4,15,6,13,7,10,12,56,3,18,16])). % 119.17/119.17 cnf(4246,plain, % 119.17/119.17 (P1(f14(f14(a1,x42461),x42462))), % 119.17/119.17 inference(scs_inference,[],[4147,4205,4188,4197,4228,4087,4186,4180,4182,4193,4183,3766,213,154,70,46,14,11,8,2,55,5,45,52,9,85,4,15,6,13,7,10,12,56,3,18,16,53])). % 119.17/119.17 cnf(4256,plain, % 119.17/119.17 (P4(f14(f14(a1,x42561),x42562))), % 119.17/119.17 inference(scs_inference,[],[4246,46])). % 119.17/119.17 cnf(4258,plain, % 119.17/119.17 (E(f2(f14(a1,x42581),x42582),f2(a1,x42582))), % 119.17/119.17 inference(scs_inference,[],[4222,4246,46,14])). % 119.17/119.17 cnf(4259,plain, % 119.17/119.17 (E(f7(f14(a1,x42591)),f7(a1))), % 119.17/119.17 inference(scs_inference,[],[4222,4246,46,14,11])). % 119.17/119.17 cnf(4260,plain, % 119.17/119.17 (E(f6(f14(a1,x42601)),f6(a1))), % 119.17/119.17 inference(scs_inference,[],[4222,4246,46,14,11,8])). % 119.17/119.17 cnf(4261,plain, % 119.17/119.17 (~E(f15(f16(x42611),f15(x42611,x42612)),f14(a1,x42613))), % 119.17/119.17 inference(scs_inference,[],[4222,4246,4245,46,14,11,8,2])). % 119.17/119.17 cnf(4264,plain, % 119.17/119.17 (E(f12(x42641,f14(a1,x42642)),f12(x42641,a1))), % 119.17/119.17 inference(scs_inference,[],[4222,4246,4245,4146,46,14,11,8,2,55,5])). % 119.17/119.17 cnf(4265,plain, % 119.17/119.17 (E(f14(f14(a1,x42651),x42652),a1)), % 119.17/119.17 inference(scs_inference,[],[4222,4246,4245,4146,46,14,11,8,2,55,5,45])). % 119.17/119.17 cnf(4269,plain, % 119.17/119.17 (E(f16(f14(a1,x42691)),f16(a1))), % 119.17/119.17 inference(scs_inference,[],[4222,4159,4246,4245,4146,46,14,11,8,2,55,5,45,52,9])). % 119.17/119.17 cnf(4270,plain, % 119.17/119.17 (~E(a11,f14(f12(a1,a1),x42701))), % 119.17/119.17 inference(scs_inference,[],[4222,4236,4159,4246,4245,4146,46,14,11,8,2,55,5,45,52,9,85])). % 119.17/119.17 cnf(4271,plain, % 119.17/119.17 (~P7(x42711,f14(f12(a1,a1),x42712))), % 119.17/119.17 inference(rename_variables,[],[4236])). % 119.17/119.17 cnf(4272,plain, % 119.17/119.17 (E(f12(f14(a1,x42721),x42722),f12(a1,x42722))), % 119.17/119.17 inference(scs_inference,[],[4222,4236,4159,4246,4245,4146,46,14,11,8,2,55,5,45,52,9,85,4])). % 119.17/119.17 cnf(4273,plain, % 119.17/119.17 (E(f2(x42731,f14(a1,x42732)),f2(x42731,a1))), % 119.17/119.17 inference(scs_inference,[],[4222,4236,4159,4246,4245,4146,46,14,11,8,2,55,5,45,52,9,85,4,15])). % 119.17/119.17 cnf(4274,plain, % 119.17/119.17 (E(f15(f14(a1,x42741),x42742),f15(a1,x42742))), % 119.17/119.17 inference(scs_inference,[],[4222,4236,4159,4246,4245,4146,46,14,11,8,2,55,5,45,52,9,85,4,15,6])). % 119.17/119.17 cnf(4275,plain, % 119.17/119.17 (E(f14(x42751,f14(a1,x42752)),f14(x42751,a1))), % 119.17/119.17 inference(scs_inference,[],[4222,4236,4159,4246,4245,4146,46,14,11,8,2,55,5,45,52,9,85,4,15,6,13])). % 119.17/119.17 cnf(4276,plain, % 119.17/119.17 (E(f15(x42761,f14(a1,x42762)),f15(x42761,a1))), % 119.17/119.17 inference(scs_inference,[],[4222,4236,4159,4246,4245,4146,46,14,11,8,2,55,5,45,52,9,85,4,15,6,13,7])). % 119.17/119.17 cnf(4277,plain, % 119.17/119.17 (E(f8(f14(a1,x42771)),f8(a1))), % 119.17/119.17 inference(scs_inference,[],[4222,4236,4159,4246,4245,4146,46,14,11,8,2,55,5,45,52,9,85,4,15,6,13,7,10])). % 119.17/119.17 cnf(4278,plain, % 119.17/119.17 (E(f14(f14(a1,x42781),x42782),f14(a1,x42782))), % 119.17/119.17 inference(scs_inference,[],[4222,4236,4159,4246,4245,4146,46,14,11,8,2,55,5,45,52,9,85,4,15,6,13,7,10,12])). % 119.17/119.17 cnf(4279,plain, % 119.17/119.17 (~P7(x42791,f14(f14(f12(a1,a1),x42792),x42793))), % 119.17/119.17 inference(scs_inference,[],[4222,4236,4271,4159,4246,4245,4146,4087,46,14,11,8,2,55,5,45,52,9,85,4,15,6,13,7,10,12,56])). % 119.17/119.17 cnf(4285,plain, % 119.17/119.17 (~P7(x42851,f12(f12(f14(a9,x42852),a9),f12(f14(a9,x42853),a9)))), % 119.17/119.17 inference(scs_inference,[],[4218,4222,4236,4271,4159,4246,4245,4190,4243,4146,4087,46,14,11,8,2,55,5,45,52,9,85,4,15,6,13,7,10,12,56,3,18])). % 119.17/119.17 cnf(4286,plain, % 119.17/119.17 (E(f12(f12(x42861,a9),x42862),f12(f12(x42861,a1),x42862))), % 119.17/119.17 inference(rename_variables,[],[4190])). % 119.17/119.17 cnf(4288,plain, % 119.17/119.17 (P1(f12(f12(f14(a9,x42881),a1),f12(f14(a9,x42882),a9)))), % 119.17/119.17 inference(scs_inference,[],[4218,4222,4236,4271,4159,4246,4245,4190,4243,4146,4087,2716,832,46,14,11,8,2,55,5,45,52,9,85,4,15,6,13,7,10,12,56,3,18,16,53])). % 119.17/119.17 cnf(4292,plain, % 119.17/119.17 (P5(f12(f12(a1,a1),f12(a1,a9)))), % 119.17/119.17 inference(scs_inference,[],[4218,4222,4236,4271,4159,4246,4245,4190,4286,4243,4146,4087,2716,832,46,14,11,8,2,55,5,45,52,9,85,4,15,6,13,7,10,12,56,3,18,16,53,19])). % 119.17/119.17 cnf(4295,plain, % 119.17/119.17 (~E(f12(a1,x42951),f14(a5,a13))), % 119.17/119.17 inference(scs_inference,[],[4081,4218,4222,4236,4271,4159,4246,4245,4190,4286,4243,4146,4087,2716,832,43,46,14,11,8,2,55,5,45,52,9,85,4,15,6,13,7,10,12,56,3,18,16,53,19,21])). % 119.17/119.17 cnf(4307,plain, % 119.17/119.17 (~E(f14(a5,a13),f12(a1,x43071))), % 119.17/119.17 inference(scs_inference,[],[4295,4258,4288,46,14,11,8,2])). % 119.17/119.17 cnf(4308,plain, % 119.17/119.17 (E(f12(f12(f12(a1,a1),f12(a1,a9)),f2(x43081,x43081)),f14(f12(f12(a1,a1),f12(a1,a9)),x43081))), % 119.17/119.17 inference(scs_inference,[],[4295,4258,4292,4288,46,14,11,8,2,55])). % 119.17/119.17 cnf(4310,plain, % 119.17/119.17 (E(f12(x43101,f2(f14(a1,x43102),x43103)),f12(x43101,f2(a1,x43103)))), % 119.17/119.17 inference(scs_inference,[],[4295,4258,4292,4288,46,14,11,8,2,55,5])). % 119.17/119.17 cnf(4317,plain, % 119.17/119.17 (~P7(x43171,f14(f14(f12(a1,a1),x43172),x43173))), % 119.17/119.17 inference(rename_variables,[],[4279])). % 119.17/119.17 cnf(4325,plain, % 119.17/119.17 (~P7(x43251,f14(f12(f12(a1,a1),f12(a1,a9)),x43252))), % 119.17/119.17 inference(scs_inference,[],[4295,4258,4292,4279,4288,3557,46,14,11,8,2,55,5,45,52,9,85,4,15,6,13,7,10,12,56])). % 119.17/119.17 cnf(4326,plain, % 119.17/119.17 (~P7(x43261,f12(f12(a1,x43262),f12(a1,x43263)))), % 119.17/119.17 inference(rename_variables,[],[3557])). % 119.17/119.17 cnf(4328,plain, % 119.17/119.17 (E(f2(f14(a1,x43281),f14(a1,x43282)),f2(a1,a1))), % 119.17/119.17 inference(scs_inference,[],[4295,4258,4273,4292,4279,4288,3557,46,14,11,8,2,55,5,45,52,9,85,4,15,6,13,7,10,12,56,3])). % 119.17/119.17 cnf(4331,plain, % 119.17/119.17 (~P7(x43311,f12(f12(a1,x43312),f12(f12(a3,a3),x43313)))), % 119.17/119.17 inference(scs_inference,[],[4295,4258,4273,4292,4279,4288,3883,3557,4326,46,14,11,8,2,55,5,45,52,9,85,4,15,6,13,7,10,12,56,3,18])). % 119.17/119.17 cnf(4335,plain, % 119.17/119.17 (P1(f14(f14(f12(a1,a1),x43351),x43352))), % 119.17/119.17 inference(scs_inference,[],[4295,4258,4273,4292,4279,4317,4288,3883,3557,4326,2248,143,46,14,11,8,2,55,5,45,52,9,85,4,15,6,13,7,10,12,56,3,18,16,53])). % 119.17/119.17 cnf(4337,plain, % 119.17/119.17 (P3(f6(f12(x43371,x43371)),x43371)), % 119.17/119.17 inference(rename_variables,[],[2248])). % 119.17/119.17 cnf(4345,plain, % 119.17/119.17 (P3(f6(f12(f14(x43451,a9),f14(x43451,a9))),f14(x43451,a1))), % 119.17/119.17 inference(scs_inference,[],[4295,4258,4273,4256,4292,4279,4317,4288,4051,3883,4159,3956,3467,3557,4326,4246,2248,4337,143,46,14,11,8,2,55,5,45,52,9,85,4,15,6,13,7,10,12,56,3,18,16,53,49,20,23])). % 119.17/119.17 cnf(4352,plain, % 119.17/119.17 (P4(f14(f14(f12(a1,a1),x43521),x43522))), % 119.17/119.17 inference(scs_inference,[],[4335,46])). % 119.17/119.17 cnf(4360,plain, % 119.17/119.17 (E(f14(f14(f12(a1,a1),x43601),x43602),a1)), % 119.17/119.17 inference(scs_inference,[],[4264,4270,4335,4044,46,14,11,8,2,55,45])). % 119.17/119.17 cnf(4367,plain, % 119.17/119.17 (~P7(x43671,f14(f12(f12(a1,a1),f12(a1,a9)),x43672))), % 119.17/119.17 inference(rename_variables,[],[4325])). % 119.17/119.17 cnf(4368,plain, % 119.17/119.17 (E(f12(f12(x43681,f14(a1,x43682)),x43683),f12(f12(x43681,a1),x43683))), % 119.17/119.17 inference(scs_inference,[],[4264,4270,4335,4325,4155,4044,46,14,11,8,2,55,45,5,52,9,85,4])). % 119.17/119.17 cnf(4375,plain, % 119.17/119.17 (~P7(x43751,f14(f14(f14(a1,x43752),x43753),x43754))), % 119.17/119.17 inference(scs_inference,[],[4264,4270,4335,4325,4155,4197,4044,4159,46,14,11,8,2,55,45,5,52,9,85,4,15,6,13,7,10,12,56])). % 119.17/119.17 cnf(4378,plain, % 119.17/119.17 (~E(f12(f14(a5,a13),f14(a5,a13)),f12(a1,x43781))), % 119.17/119.17 inference(scs_inference,[],[4307,4264,4270,4335,4325,4155,4197,4044,4159,62,46,14,11,8,2,55,45,5,52,9,85,4,15,6,13,7,10,12,56,3])). % 119.17/119.17 cnf(4380,plain, % 119.17/119.17 (~P7(x43801,f12(f12(f12(a1,a1),f12(a1,a9)),f2(x43802,x43802)))), % 119.17/119.17 inference(scs_inference,[],[4307,4264,4270,4335,4325,4367,4308,4155,4197,4044,4159,62,46,14,11,8,2,55,45,5,52,9,85,4,15,6,13,7,10,12,56,3,18])). % 119.17/119.17 cnf(4383,plain, % 119.17/119.17 (P1(f14(f12(f12(a1,a1),f12(a1,a9)),a1))), % 119.17/119.17 inference(scs_inference,[],[4307,4264,4270,4345,4335,4325,4367,4308,4155,4197,4044,4159,4205,2954,62,46,14,11,8,2,55,45,5,52,9,85,4,15,6,13,7,10,12,56,3,18,16,53])). % 119.17/119.17 cnf(4392,plain, % 119.17/119.17 (E(f2(f12(f14(a1,x43921),x43922),x43923),f2(f12(a1,x43922),x43923))), % 119.17/119.17 inference(scs_inference,[],[4383,4272,46,14])). % 119.17/119.17 cnf(4396,plain, % 119.17/119.17 (E(f12(f14(a1,x43961),f2(x43962,x43962)),f14(f14(a1,x43961),x43962))), % 119.17/119.17 inference(scs_inference,[],[4378,4383,4272,4112,46,14,11,8,2,55])). % 119.17/119.17 cnf(4400,plain, % 119.17/119.17 (E(f12(x44001,f12(f14(a1,x44002),x44003)),f12(x44001,f12(a1,x44003)))), % 119.17/119.17 inference(scs_inference,[],[4378,4383,4272,4112,46,14,11,8,2,55,45,5])). % 119.17/119.17 cnf(4404,plain, % 119.17/119.17 (~E(a11,f12(f12(f12(a1,a1),f12(a1,a9)),f2(x44041,x44041)))), % 119.17/119.17 inference(scs_inference,[],[4378,4380,4383,4272,4186,4112,46,14,11,8,2,55,45,5,52,9,85])). % 119.17/119.17 cnf(4405,plain, % 119.17/119.17 (~P7(x44051,f12(f12(f12(a1,a1),f12(a1,a9)),f2(x44052,x44052)))), % 119.17/119.17 inference(rename_variables,[],[4380])). % 119.17/119.17 cnf(4406,plain, % 119.17/119.17 (E(f12(f12(f14(a1,x44061),x44062),x44063),f12(f12(a1,x44062),x44063))), % 119.17/119.17 inference(scs_inference,[],[4378,4380,4383,4272,4186,4112,46,14,11,8,2,55,45,5,52,9,85,4])). % 119.17/119.17 cnf(4407,plain, % 119.17/119.17 (E(f2(x44071,f12(f14(a1,x44072),x44073)),f2(x44071,f12(a1,x44073)))), % 119.17/119.17 inference(scs_inference,[],[4378,4380,4383,4272,4186,4112,46,14,11,8,2,55,45,5,52,9,85,4,15])). % 119.17/119.17 cnf(4412,plain, % 119.17/119.17 (E(f14(f12(f14(a1,x44121),x44122),x44123),f14(f12(a1,x44122),x44123))), % 119.17/119.17 inference(scs_inference,[],[4378,4380,4383,4272,4186,4112,46,14,11,8,2,55,45,5,52,9,85,4,15,6,7,13,10,12])). % 119.17/119.17 cnf(4413,plain, % 119.17/119.17 (~P7(x44131,f14(f12(a1,a3),x44132))), % 119.17/119.17 inference(scs_inference,[],[4378,4380,4383,4272,4148,4186,3977,4112,46,14,11,8,2,55,45,5,52,9,85,4,15,6,7,13,10,12,56])). % 119.17/119.17 cnf(4418,plain, % 119.17/119.17 (~P7(x44181,f12(f12(f12(a1,a1),f12(a1,a9)),f2(f14(a1,x44182),a1)))), % 119.17/119.17 inference(scs_inference,[],[4378,4380,4405,4383,4360,4310,4272,4148,4186,3977,4112,156,46,14,11,8,2,55,45,5,52,9,85,4,15,6,7,13,10,12,56,3,18])). % 119.17/119.17 cnf(4419,plain, % 119.17/119.17 (~P7(x44191,f12(f12(f12(a1,a1),f12(a1,a9)),f2(x44192,x44192)))), % 119.17/119.17 inference(rename_variables,[],[4380])). % 119.17/119.17 cnf(4422,plain, % 119.17/119.17 (P1(f12(f12(f12(a1,a1),f12(a1,a9)),f2(x44221,x44221)))), % 119.17/119.17 inference(scs_inference,[],[4378,4380,4405,4419,4383,4360,4310,4272,4148,4186,3977,4112,2712,42,156,46,14,11,8,2,55,45,5,52,9,85,4,15,6,7,13,10,12,56,3,18,16,53])). % 119.17/119.17 cnf(4431,plain, % 119.17/119.17 (P4(f12(f12(f12(a1,a1),f12(a1,a9)),f2(x44311,x44311)))), % 119.17/119.17 inference(scs_inference,[],[4422,46])). % 119.17/119.17 cnf(4437,plain, % 119.17/119.17 (E(f12(a10,f2(x44371,x44371)),f14(a10,x44371))), % 119.17/119.17 inference(scs_inference,[],[4200,4422,4274,33,46,14,11,8,2,55])). % 119.17/119.17 cnf(4439,plain, % 119.17/119.17 (E(f12(f12(f12(a1,a1),f12(a1,a9)),f2(x44391,x44391)),a1)), % 119.17/119.17 inference(scs_inference,[],[4200,4422,4274,33,46,14,11,8,2,55,45])). % 119.17/119.17 cnf(4445,plain, % 119.17/119.17 (~E(a11,f14(f12(a1,a3),x44451))), % 119.17/119.17 inference(scs_inference,[],[4413,4200,4422,4274,4044,33,46,14,11,8,2,55,45,5,52,9,85])). % 119.17/119.17 cnf(4446,plain, % 119.17/119.17 (~P7(x44461,f14(f12(a1,a3),x44462))), % 119.17/119.17 inference(rename_variables,[],[4413])). % 119.17/119.17 cnf(4449,plain, % 119.17/119.17 (E(f15(f15(f14(a1,x44491),x44492),x44493),f15(f15(a1,x44492),x44493))), % 119.17/119.17 inference(scs_inference,[],[4413,4200,4422,4274,4044,33,46,14,11,8,2,55,45,5,52,9,85,4,15,6])). % 119.17/119.17 cnf(4451,plain, % 119.17/119.17 (E(f15(x44511,f15(f14(a1,x44512),x44513)),f15(x44511,f15(a1,x44513)))), % 119.17/119.17 inference(scs_inference,[],[4413,4200,4422,4274,4044,33,46,14,11,8,2,55,45,5,52,9,85,4,15,6,13,7])). % 119.17/119.17 cnf(4454,plain, % 119.17/119.17 (~P7(x44541,f14(f14(f12(a1,a3),x44542),x44543))), % 119.17/119.17 inference(scs_inference,[],[4413,4446,4200,4422,4274,4044,4087,33,46,14,11,8,2,55,45,5,52,9,85,4,15,6,13,7,10,12,56])). % 119.17/119.17 cnf(4455,plain, % 119.17/119.17 (~P7(x44551,f14(f12(a1,a3),x44552))), % 119.17/119.17 inference(rename_variables,[],[4413])). % 119.17/119.17 cnf(4458,plain, % 119.17/119.17 (~E(f12(a3,a1),f15(f15(x44581,x44582),f16(x44581)))), % 119.17/119.17 inference(scs_inference,[],[3633,4413,4446,4200,4422,4274,3920,4044,4087,33,46,14,11,8,2,55,45,5,52,9,85,4,15,6,13,7,10,12,56,3])). % 119.17/119.17 cnf(4460,plain, % 119.17/119.17 (~P7(x44601,f12(f14(a1,x44602),f2(x44603,x44603)))), % 119.17/119.17 inference(scs_inference,[],[3633,4413,4446,4200,4422,4396,4274,3920,4044,4087,4197,33,46,14,11,8,2,55,45,5,52,9,85,4,15,6,13,7,10,12,56,3,18])). % 119.17/119.17 cnf(4463,plain, % 119.17/119.17 (P1(f14(f12(a1,a3),a1))), % 119.17/119.17 inference(scs_inference,[],[3633,4413,4446,4455,4200,4422,4396,4274,4345,3920,4044,4087,4197,33,70,46,14,11,8,2,55,45,5,52,9,85,4,15,6,13,7,10,12,56,3,18,16,53])). % 119.17/119.17 cnf(4467,plain, % 119.17/119.17 (~E(f12(x44671,a1),f14(a5,a13))), % 119.17/119.17 inference(scs_inference,[],[4082,3633,4413,4446,4455,4200,4422,4396,4274,4345,3920,4044,4087,4197,33,70,43,46,14,11,8,2,55,45,5,52,9,85,4,15,6,13,7,10,12,56,3,18,16,53,21])). % 119.17/119.17 cnf(4480,plain, % 119.17/119.17 (~E(a11,f12(f14(a1,x44801),f2(x44802,x44802)))), % 119.17/119.17 inference(scs_inference,[],[4460,85])). % 119.17/119.17 cnf(4481,plain, % 119.17/119.17 (~P7(x44811,f12(f14(a1,x44812),f2(x44813,x44813)))), % 119.17/119.17 inference(rename_variables,[],[4460])). % 119.17/119.17 cnf(4493,plain, % 119.17/119.17 (E(f12(a9,f2(x44931,x44931)),f14(a9,x44931))), % 119.17/119.17 inference(scs_inference,[],[4437,4460,4463,32,85,4,15,46,6,7,13,10,12,14,11,55])). % 119.17/119.17 cnf(4496,plain, % 119.17/119.17 (~E(f14(a5,a13),f12(x44961,a1))), % 119.17/119.17 inference(scs_inference,[],[4467,4437,4460,4463,32,85,4,15,46,6,7,13,10,12,14,11,55,8,2])). % 119.17/119.17 cnf(4497,plain, % 119.17/119.17 (E(f14(f12(a1,a3),a1),a1)), % 119.17/119.17 inference(scs_inference,[],[4467,4437,4460,4463,32,85,4,15,46,6,7,13,10,12,14,11,55,8,2,45])). % 119.17/119.17 cnf(4499,plain, % 119.17/119.17 (P5(f14(a10,x44991))), % 119.17/119.17 inference(scs_inference,[],[4467,4437,4460,4463,33,32,85,4,15,46,6,7,13,10,12,14,11,55,8,2,45,52])). % 119.17/119.17 cnf(4503,plain, % 119.17/119.17 (~E(f14(f12(a1,a3),a1),f15(f15(x45031,x45032),f16(x45031)))), % 119.17/119.17 inference(scs_inference,[],[4467,4437,4460,4463,33,44,32,85,4,15,46,6,7,13,10,12,14,11,55,8,2,45,52,5,9,16])). % 119.17/119.17 cnf(4504,plain, % 119.17/119.17 (P1(f12(f14(a1,x45041),f2(x45042,x45042)))), % 119.17/119.17 inference(scs_inference,[],[4467,4437,4460,4481,4463,2264,33,44,32,85,4,15,46,6,7,13,10,12,14,11,55,8,2,45,52,5,9,16,53])). % 119.17/119.17 cnf(4505,plain, % 119.17/119.17 (~P7(x45051,f12(f14(a1,x45052),f2(x45053,x45053)))), % 119.17/119.17 inference(rename_variables,[],[4460])). % 119.17/119.17 cnf(4508,plain, % 119.17/119.17 (~P7(x45081,f14(f12(a1,f14(a9,x45082)),x45083))), % 119.17/119.17 inference(scs_inference,[],[4467,4437,4460,4481,4463,4148,3647,2264,33,44,32,85,4,15,46,6,7,13,10,12,14,11,55,8,2,45,52,5,9,16,53,56])). % 119.17/119.17 cnf(4515,plain, % 119.17/119.17 (~P7(x45151,f12(f14(a3,x45152),f2(x45153,x45153)))), % 119.17/119.17 inference(scs_inference,[],[4467,4437,4460,4481,4505,4463,4392,4407,4002,4148,3647,2264,33,44,32,85,4,15,46,6,7,13,10,12,14,11,55,8,2,45,52,5,9,16,53,56,3,18])). % 119.17/119.17 cnf(4525,plain, % 119.17/119.17 (P6(f14(f12(a1,a3),a1))), % 119.17/119.17 inference(scs_inference,[],[4467,4437,4460,4481,4505,4463,4392,4400,4407,3904,4002,2242,4148,3647,1002,4087,2264,33,44,32,85,4,15,46,6,7,13,10,12,14,11,55,8,2,45,52,5,9,16,53,56,3,18,20,23,59,49])). % 119.17/119.17 cnf(4529,plain, % 119.17/119.17 (~E(a11,f12(f14(a3,x45291),f2(x45292,x45292)))), % 119.17/119.17 inference(scs_inference,[],[4515,85])). % 119.17/119.17 cnf(4532,plain, % 119.17/119.17 (E(f2(x45321,f12(a9,f2(x45322,x45322))),f2(x45321,f14(a9,x45322)))), % 119.17/119.17 inference(scs_inference,[],[4493,4515,85,4,15])). % 119.17/119.17 cnf(4540,plain, % 119.17/119.17 (E(f2(f12(a9,f2(x45401,x45401)),x45402),f2(f14(a9,x45401),x45402))), % 119.17/119.17 inference(scs_inference,[],[4493,4515,4504,85,4,15,46,6,7,13,10,12,14])). % 119.17/119.17 cnf(4545,plain, % 119.17/119.17 (~E(f15(f15(x45451,x45452),f16(x45451)),f12(a3,a1))), % 119.17/119.17 inference(scs_inference,[],[4499,4493,4458,4515,4504,85,4,15,46,6,7,13,10,12,14,11,55,8,2])). % 119.17/119.17 cnf(4546,plain, % 119.17/119.17 (P5(f14(f14(a10,x45461),x45462))), % 119.17/119.17 inference(scs_inference,[],[4499,4493,4458,4515,4504,85,4,15,46,6,7,13,10,12,14,11,55,8,2,52])). % 119.17/119.17 cnf(4548,plain, % 119.17/119.17 (E(f12(f14(a1,x45481),f2(x45482,x45482)),a1)), % 119.17/119.17 inference(scs_inference,[],[4499,4493,4458,4515,4504,85,4,15,46,6,7,13,10,12,14,11,55,8,2,52,45])). % 119.17/119.17 cnf(4553,plain, % 119.17/119.17 (P1(f12(f12(f14(a9,x45531),a9),f12(f14(a9,x45531),a9)))), % 119.17/119.17 inference(scs_inference,[],[4499,4493,4458,4515,4504,4285,3099,832,85,4,15,46,6,7,13,10,12,14,11,55,8,2,52,45,5,9,16,53])). % 119.17/119.17 cnf(4557,plain, % 119.17/119.17 (~P7(x45571,f14(f12(f12(a1,a1),f12(a1,a1)),x45572))), % 119.17/119.17 inference(scs_inference,[],[4499,4493,4458,4515,4504,4285,3099,4155,226,832,85,4,15,46,6,7,13,10,12,14,11,55,8,2,52,45,5,9,16,53,56])). % 119.17/119.17 cnf(4561,plain, % 119.17/119.17 (~E(f12(f14(a5,a13),f14(a5,a13)),f12(x45611,a1))), % 119.17/119.17 inference(scs_inference,[],[4496,4499,4493,4458,4515,4504,4285,3099,4155,226,832,62,85,4,15,46,6,7,13,10,12,14,11,55,8,2,52,45,5,9,16,53,56,3])). % 119.17/119.17 cnf(4563,plain, % 119.17/119.17 (~P7(x45631,f12(a9,f2(x45632,x45632)))), % 119.17/119.17 inference(scs_inference,[],[4496,4499,4493,4458,4515,4504,4285,3099,4155,226,3471,832,62,85,4,15,46,6,7,13,10,12,14,11,55,8,2,52,45,5,9,16,53,56,3,18])). % 119.17/119.17 cnf(4566,plain, % 119.17/119.17 (~E(a11,f12(a9,f2(x45661,x45661)))), % 119.17/119.17 inference(scs_inference,[],[4563,85])). % 119.17/119.17 cnf(4567,plain, % 119.17/119.17 (~P7(x45671,f12(a9,f2(x45672,x45672)))), % 119.17/119.17 inference(rename_variables,[],[4563])). % 119.17/119.17 cnf(4576,plain, % 119.17/119.17 (E(f14(f12(f14(a1,x45761),f2(x45762,x45762)),x45763),f14(a1,x45763))), % 119.17/119.17 inference(scs_inference,[],[4563,4548,4553,85,4,15,46,6,7,13,10,12])). % 119.17/119.17 cnf(4591,plain, % 119.17/119.17 (P1(f12(a9,f2(x45911,x45911)))), % 119.17/119.17 inference(scs_inference,[],[4561,4546,4563,4567,4548,4553,2685,143,85,4,15,46,6,7,13,10,12,14,55,11,8,86,2,45,52,5,9,16,53])). % 119.17/119.17 cnf(4592,plain, % 119.17/119.17 (~P7(x45921,f12(a9,f2(x45922,x45922)))), % 119.17/119.17 inference(rename_variables,[],[4563])). % 119.17/119.17 cnf(4598,plain, % 119.17/119.17 (~P7(x45981,f12(a9,f2(a9,a1)))), % 119.17/119.17 inference(scs_inference,[],[4561,4546,4563,4567,4592,4548,4532,4540,4553,4108,2685,143,85,4,15,46,6,7,13,10,12,14,55,11,8,86,2,45,52,5,9,16,53,3,18])). % 119.17/119.17 cnf(4605,plain, % 119.17/119.17 (~E(a11,f12(a9,f2(a9,a1)))), % 119.17/119.17 inference(scs_inference,[],[4598,85])). % 119.17/119.17 cnf(4620,plain, % 119.17/119.17 (E(f12(a9,f2(x46201,x46201)),a1)), % 119.17/119.17 inference(scs_inference,[],[4598,4591,4445,4497,85,4,15,46,6,7,13,10,12,14,11,8,2,45])). % 119.17/119.17 cnf(4622,plain, % 119.17/119.17 (P5(f14(a9,x46221))), % 119.17/119.17 inference(scs_inference,[],[4598,4591,4445,4497,32,85,4,15,46,6,7,13,10,12,14,11,8,2,45,52])). % 119.17/119.17 cnf(4626,plain, % 119.17/119.17 (~E(f12(a9,f2(x46261,x46261)),f12(f15(f15(x46262,x46263),f16(x46262)),f15(f15(x46262,x46263),f16(x46262))))), % 119.17/119.17 inference(scs_inference,[],[4598,4591,4445,4497,2954,32,85,4,15,46,6,7,13,10,12,14,11,8,2,45,52,5,9,16])). % 119.17/119.17 cnf(4627,plain, % 119.17/119.17 (P1(f14(f12(f12(a1,a1),f12(a1,a1)),a1))), % 119.17/119.17 inference(scs_inference,[],[4598,4591,4445,4557,4497,4345,2954,32,85,4,15,46,6,7,13,10,12,14,11,8,2,45,52,5,9,16,53])). % 119.17/119.17 cnf(4631,plain, % 119.17/119.17 (~P7(x46311,f14(f14(a9,x46312),x46313))), % 119.17/119.17 inference(scs_inference,[],[4598,4591,4445,4557,4497,4345,3471,2954,32,85,4,15,46,6,7,13,10,12,14,11,8,2,45,52,5,9,16,53,56])). % 119.17/119.17 cnf(4633,plain, % 119.17/119.17 (~E(f15(f15(a1,x46331),f16(f14(a1,x46332))),f12(a3,a1))), % 119.17/119.17 inference(scs_inference,[],[4545,4598,4591,4445,4557,4497,4449,4345,3471,2954,32,85,4,15,46,6,7,13,10,12,14,11,8,2,45,52,5,9,16,53,56,3])). % 119.17/119.17 cnf(4635,plain, % 119.17/119.17 (E(f15(f15(f14(a1,x46351),x46352),x46353),f15(f15(a1,x46352),x46353))), % 119.17/119.17 inference(rename_variables,[],[4449])). % 119.17/119.17 cnf(4636,plain, % 119.17/119.17 (~P7(x46361,f14(f12(f14(a1,x46362),f2(x46363,x46363)),x46364))), % 119.17/119.17 inference(scs_inference,[],[4545,4598,4591,4445,4576,4557,4497,4449,4126,4345,3471,2954,32,85,4,15,46,6,7,13,10,12,14,11,8,2,45,52,5,9,16,53,56,3,18])). % 119.17/119.17 cnf(4642,plain, % 119.17/119.17 (E(f12(f14(a9,x46421),f2(x46422,x46422)),f14(f14(a9,x46421),x46422))), % 119.17/119.17 inference(scs_inference,[],[4545,4598,4591,4445,4576,4352,4557,4224,4497,4449,4126,4345,4335,3471,2954,32,85,4,15,46,6,7,13,10,12,14,11,8,2,45,52,5,9,16,53,56,3,18,49,55])). % 119.17/119.17 cnf(4650,plain, % 119.17/119.17 (P2(f14(a9,x46501))), % 119.17/119.17 inference(scs_inference,[],[4545,4598,4591,4445,4576,4352,4557,3644,4224,4497,4449,4635,4368,4126,4345,4335,4155,3471,2954,32,85,4,15,46,6,7,13,10,12,14,11,8,2,45,52,5,9,16,53,56,3,18,49,55,17,19,60])). % 119.17/119.17 cnf(4655,plain, % 119.17/119.17 (~E(f14(a1,x46551),f14(a5,a13))), % 119.17/119.17 inference(scs_inference,[],[43,4131,4545,4598,4591,4445,4576,4352,4557,3644,4224,4497,4449,4635,4368,4126,4076,4345,4335,4155,3471,2954,32,85,4,15,46,6,7,13,10,12,14,11,8,2,45,52,5,9,16,53,56,3,18,49,55,17,19,60,57,21])). % 119.17/119.17 cnf(4659,plain, % 119.17/119.17 (~E(a11,f14(f14(a9,x46591),x46592))), % 119.17/119.17 inference(scs_inference,[],[4631,85])). % 119.17/119.17 cnf(4660,plain, % 119.17/119.17 (~P7(x46601,f14(f14(a9,x46602),x46603))), % 119.17/119.17 inference(rename_variables,[],[4631])). % 119.17/119.17 cnf(4668,plain, % 119.17/119.17 (E(f14(f12(a9,f2(x46681,x46681)),x46682),f14(a1,x46682))), % 119.17/119.17 inference(scs_inference,[],[4631,4620,4627,85,4,15,46,6,7,13,12])). % 119.17/119.17 cnf(4673,plain, % 119.17/119.17 (~E(f14(a5,a13),f14(a1,x46731))), % 119.17/119.17 inference(scs_inference,[],[4655,4631,4620,4627,85,4,15,46,6,7,13,12,10,14,11,8,2])). % 119.17/119.17 cnf(4676,plain, % 119.17/119.17 (P5(f14(f14(a9,x46761),x46762))), % 119.17/119.17 inference(scs_inference,[],[4655,4622,4631,4620,4627,85,4,15,46,6,7,13,12,10,14,11,8,2,45,52])). % 119.17/119.17 cnf(4681,plain, % 119.17/119.17 (P1(f14(f14(a9,x46811),a1))), % 119.17/119.17 inference(scs_inference,[],[4655,4622,4631,4660,4620,4627,4345,42,85,4,15,46,6,7,13,12,10,14,11,8,2,45,52,5,9,16,53])). % 119.17/119.17 cnf(4682,plain, % 119.17/119.17 (~P7(x46821,f14(f14(a9,x46822),x46823))), % 119.17/119.17 inference(rename_variables,[],[4631])). % 119.17/119.17 cnf(4685,plain, % 119.17/119.17 (~P7(x46851,f14(f14(f14(a9,x46852),x46853),x46854))), % 119.17/119.17 inference(scs_inference,[],[4655,4622,4631,4660,4682,4620,4627,4345,42,85,4,15,46,6,7,13,12,10,14,11,8,2,45,52,5,9,16,53,56])). % 119.17/119.17 cnf(4686,plain, % 119.17/119.17 (~P7(x46861,f14(f14(a9,x46862),x46863))), % 119.17/119.17 inference(rename_variables,[],[4631])). % 119.17/119.17 cnf(4690,plain, % 119.17/119.17 (~P7(x46901,f12(f14(a9,x46902),f2(x46903,x46903)))), % 119.17/119.17 inference(scs_inference,[],[4655,4622,4631,4660,4682,4686,4620,4642,4627,4626,4345,42,85,4,15,46,6,7,13,12,10,14,11,8,2,45,52,5,9,16,53,56,3,18])). % 119.17/119.17 cnf(4705,plain, % 119.17/119.17 (~E(a11,f12(f14(a9,x47051),f2(x47052,x47052)))), % 119.17/119.17 inference(scs_inference,[],[4690,85])). % 119.17/119.17 cnf(4706,plain, % 119.17/119.17 (~P7(x47061,f12(f14(a9,x47062),f2(x47063,x47063)))), % 119.17/119.17 inference(rename_variables,[],[4690])). % 119.17/119.17 cnf(4714,plain, % 119.17/119.17 (E(f14(f12(f12(f12(a1,a1),f12(a1,a9)),f2(x47141,x47141)),x47142),f14(a1,x47142))), % 119.17/119.17 inference(scs_inference,[],[4690,4681,4439,85,4,15,46,6,7,13,12])). % 119.17/119.17 cnf(4715,plain, % 119.17/119.17 (E(f8(f12(f12(f12(a1,a1),f12(a1,a9)),f2(x47151,x47151))),f8(a1))), % 119.17/119.17 inference(scs_inference,[],[4690,4681,4439,85,4,15,46,6,7,13,12,10])). % 119.17/119.17 cnf(4719,plain, % 119.17/119.17 (~E(f12(f14(a1,x47191),f2(x47192,x47192)),a11)), % 119.17/119.17 inference(scs_inference,[],[4690,4681,4480,4439,85,4,15,46,6,7,13,12,10,14,11,8,2])). % 119.17/119.17 cnf(4720,plain, % 119.17/119.17 (E(f14(f14(a9,x47201),a1),a1)), % 119.17/119.17 inference(scs_inference,[],[4690,4681,4480,4439,85,4,15,46,6,7,13,12,10,14,11,8,2,45])). % 119.17/119.17 cnf(4726,plain, % 119.17/119.17 (~E(f14(f14(a9,x47261),a1),f15(f16(x47262),f15(x47262,x47263)))), % 119.17/119.17 inference(scs_inference,[],[4690,4676,4681,4480,4439,70,85,4,15,46,6,7,13,12,10,14,11,8,2,45,52,5,9,16])). % 119.17/119.17 cnf(4727,plain, % 119.17/119.17 (P1(f12(f14(a9,x47271),f2(x47272,x47272)))), % 119.17/119.17 inference(scs_inference,[],[4690,4706,4676,4681,4480,4439,2240,70,85,4,15,46,6,7,13,12,10,14,11,8,2,45,52,5,9,16,53])). % 119.17/119.17 cnf(4731,plain, % 119.17/119.17 (~E(f12(f14(a5,a13),f14(a5,a13)),f14(a1,x47311))), % 119.17/119.17 inference(scs_inference,[],[4673,4690,4706,4676,4681,4480,4439,2240,70,62,85,4,15,46,6,7,13,12,10,14,11,8,2,45,52,5,9,16,53,3])). % 119.17/119.17 cnf(4733,plain, % 119.17/119.17 (~P7(x47331,f14(f12(a9,f2(x47332,x47332)),x47333))), % 119.17/119.17 inference(scs_inference,[],[4673,4690,4706,4676,4681,4480,4668,4439,4126,2240,70,62,85,4,15,46,6,7,13,12,10,14,11,8,2,45,52,5,9,16,53,3,18])). % 119.17/119.17 cnf(4740,plain, % 119.17/119.17 (~P7(x47401,f14(f14(f12(a1,a3),x47402),x47403))), % 119.17/119.17 inference(rename_variables,[],[4454])). % 119.17/119.17 cnf(4742,plain, % 119.17/119.17 (E(f2(x47421,f14(f14(a9,x47422),a1)),f2(x47421,a1))), % 119.17/119.17 inference(scs_inference,[],[4720,4454,85,4,15])). % 119.17/119.17 cnf(4750,plain, % 119.17/119.17 (E(f2(f14(f14(a9,x47501),a1),x47502),f2(a1,x47502))), % 119.17/119.17 inference(scs_inference,[],[4727,4720,4454,85,4,15,46,6,7,13,12,10,14])). % 119.17/119.17 cnf(4754,plain, % 119.17/119.17 (E(f12(f14(a9,x47541),f2(x47542,x47542)),a1)), % 119.17/119.17 inference(scs_inference,[],[4731,4727,4720,4454,85,4,15,46,6,7,13,12,10,14,11,8,2,45])). % 119.17/119.17 cnf(4758,plain, % 119.17/119.17 (P1(f14(f14(f12(a1,a3),x47581),x47582))), % 119.17/119.17 inference(scs_inference,[],[4731,4727,4720,4454,4740,213,85,4,15,46,6,7,13,12,10,14,11,8,2,45,9,5,53])). % 119.17/119.17 cnf(4762,plain, % 119.17/119.17 (~E(f12(f14(a9,x47621),f2(x47622,x47622)),f15(f15(x47623,x47624),f16(x47623)))), % 119.17/119.17 inference(scs_inference,[],[4731,4727,4720,4454,4740,213,44,85,4,15,46,6,7,13,12,10,14,11,8,2,45,9,5,53,16])). % 119.17/119.17 cnf(4763,plain, % 119.17/119.17 (~P7(x47631,f14(f12(x47632,a1),x47633))), % 119.17/119.17 inference(scs_inference,[],[4731,4727,4720,4454,4740,4147,213,206,44,85,4,15,46,6,7,13,12,10,14,11,8,2,45,9,5,53,16,56])). % 119.17/119.17 cnf(4768,plain, % 119.17/119.17 (~P7(x47681,f12(f2(f14(a1,x47682),a1),f12(f12(a1,a1),f12(a1,a9))))), % 119.17/119.17 inference(scs_inference,[],[4731,4727,4720,4454,4740,4715,4418,4147,213,206,44,41,62,85,4,15,46,6,7,13,12,10,14,11,8,2,45,9,5,53,16,56,3,18])). % 119.17/119.17 cnf(4776,plain, % 119.17/119.17 (~E(a11,f14(f12(x47761,a1),x47762))), % 119.17/119.17 inference(scs_inference,[],[4763,85])). % 119.17/119.17 cnf(4777,plain, % 119.17/119.17 (~P7(x47771,f14(f12(x47772,a1),x47773))), % 119.17/119.17 inference(rename_variables,[],[4763])). % 119.17/119.17 cnf(4779,plain, % 119.17/119.17 (E(f2(x47791,f12(f14(a9,x47792),f2(x47793,x47793))),f2(x47791,a1))), % 119.17/119.17 inference(scs_inference,[],[4763,4754,85,4,15])). % 119.17/119.17 cnf(4782,plain, % 119.17/119.17 (E(f15(f12(f14(a9,x47821),f2(x47822,x47822)),x47823),f15(a1,x47823))), % 119.17/119.17 inference(scs_inference,[],[4763,4754,4758,85,4,15,46,6])). % 119.17/119.17 cnf(4783,plain, % 119.17/119.17 (E(f15(x47831,f12(f14(a9,x47832),f2(x47833,x47833))),f15(x47831,a1))), % 119.17/119.17 inference(scs_inference,[],[4763,4754,4758,85,4,15,46,6,7])). % 119.17/119.17 cnf(4785,plain, % 119.17/119.17 (E(f14(f12(f14(a9,x47851),f2(x47852,x47852)),x47853),f14(a1,x47853))), % 119.17/119.17 inference(scs_inference,[],[4763,4754,4758,85,4,15,46,6,7,13,12])). % 119.17/119.17 cnf(4787,plain, % 119.17/119.17 (E(f2(f12(f14(a9,x47871),f2(x47872,x47872)),x47873),f2(a1,x47873))), % 119.17/119.17 inference(scs_inference,[],[4763,4754,4758,85,4,15,46,6,7,13,12,10,14])). % 119.17/119.17 cnf(4795,plain, % 119.17/119.17 (P1(f14(f12(x47951,a1),a1))), % 119.17/119.17 inference(scs_inference,[],[4763,4777,4529,4754,4758,4345,85,4,15,46,6,7,13,12,10,14,11,8,2,45,9,5,53])). % 119.17/119.17 cnf(4797,plain, % 119.17/119.17 (~P7(x47971,f14(f12(x47972,a1),x47973))), % 119.17/119.17 inference(rename_variables,[],[4763])). % 119.17/119.17 cnf(4800,plain, % 119.17/119.17 (~P7(x48001,f14(f14(f12(x48002,a1),x48003),x48004))), % 119.17/119.17 inference(scs_inference,[],[4763,4777,4797,4529,4754,4758,4186,4727,4345,832,85,4,15,46,6,7,13,12,10,14,11,8,2,45,9,5,53,16,56])). % 119.17/119.17 cnf(4803,plain, % 119.17/119.17 (~E(f15(f16(f14(a1,x48031)),f15(a1,x48032)),f14(a1,x48033))), % 119.17/119.17 inference(scs_inference,[],[4261,4763,4777,4797,4529,4754,4758,4451,4186,4727,4345,832,85,4,15,46,6,7,13,12,10,14,11,8,2,45,9,5,53,16,56,3])). % 119.17/119.17 cnf(4806,plain, % 119.17/119.17 (~P7(x48061,f14(f12(f12(f12(a1,a1),f12(a1,a9)),f2(x48062,x48062)),x48063))), % 119.17/119.17 inference(scs_inference,[],[4261,4763,4777,4797,4529,4754,4758,4714,4451,4186,4727,4126,4345,832,85,4,15,46,6,7,13,12,10,14,11,8,2,45,9,5,53,16,56,3,18])). % 119.17/119.17 cnf(4808,plain, % 119.17/119.17 (~P7(f15(f15(f14(a1,x48081),f14(a9,x48082)),f16(a1)),f6(f15(f16(a1),f15(a1,a1))))), % 119.17/119.17 inference(scs_inference,[],[4261,4763,4777,4797,4529,4754,4758,4714,3720,4451,4449,4186,4727,4126,4345,832,85,4,15,46,6,7,13,12,10,14,11,8,2,45,9,5,53,16,56,3,18,17])). % 119.17/119.17 cnf(4816,plain, % 119.17/119.17 (~P7(x48161,f14(f12(f14(a1,x48162),f2(x48163,x48163)),x48164))), % 119.17/119.17 inference(rename_variables,[],[4636])). % 119.17/119.17 cnf(4829,plain, % 119.17/119.17 (E(f14(f12(x48291,a1),a1),a1)), % 119.17/119.17 inference(scs_inference,[],[4795,4636,4275,85,4,46,15,6,7,13,12,10,14,11,8,45])). % 119.17/119.17 cnf(4834,plain, % 119.17/119.17 (P1(f14(f12(f14(a1,x48341),f2(x48342,x48342)),x48343))), % 119.17/119.17 inference(scs_inference,[],[4795,4705,4636,4816,4275,2248,85,4,46,15,6,7,13,12,10,14,11,8,45,2,9,5,53])). % 119.17/119.17 cnf(4839,plain, % 119.17/119.17 (~E(f14(a9,x48391),f14(a5,a13))), % 119.17/119.17 inference(scs_inference,[],[43,4795,4705,4636,4816,4650,4275,2248,2954,85,4,46,15,6,7,13,12,10,14,11,8,45,2,9,5,53,16,21])). % 119.17/119.17 cnf(4845,plain, % 119.17/119.17 (~P7(x48451,f12(f12(f14(a1,x48452),x48453),f12(f12(a3,a3),x48454)))), % 119.17/119.17 inference(scs_inference,[],[43,4795,4705,4779,4787,4636,4816,4650,4525,4331,4275,4406,3454,2248,2954,85,4,46,15,6,7,13,12,10,14,11,8,45,2,9,5,53,16,21,3,24,18])). % 119.17/119.17 cnf(4848,plain, % 119.17/119.17 (P4(f12(f12(f12(a1,a1),f12(a1,a9)),f2(a1,f14(a1,x48481))))), % 119.17/119.17 inference(scs_inference,[],[43,4795,4705,4431,4779,4787,4636,4816,4650,4525,4331,4275,4310,4406,3454,2248,2954,85,4,46,15,6,7,13,12,10,14,11,8,45,2,9,5,53,16,21,3,24,18,20])). % 119.17/119.17 cnf(4874,plain, % 119.17/119.17 (~E(f14(a5,a13),f14(a9,x48741))), % 119.17/119.17 inference(scs_inference,[],[4839,4829,4685,4834,85,4,46,15,6,7,13,12,10,14,8,11,45,2])). % 119.17/119.17 cnf(4877,plain, % 119.17/119.17 (P1(f12(f12(f14(a1,x48771),x48772),f12(f12(a3,a3),x48773)))), % 119.17/119.17 inference(scs_inference,[],[4839,4829,4685,4834,4845,2712,85,4,46,15,6,7,13,12,10,14,8,11,45,2,9,5,53])). % 119.17/119.17 cnf(4882,plain, % 119.17/119.17 (~E(f12(a1,x48821),f15(f15(x48822,x48823),f16(x48822)))), % 119.17/119.17 inference(scs_inference,[],[4839,3882,4829,4685,4834,4845,2712,143,100,85,4,46,15,6,7,13,12,10,14,8,11,45,2,9,5,53,16,3])). % 119.17/119.17 cnf(4883,plain, % 119.17/119.17 (~P7(x48831,f14(f12(f14(a9,x48832),f2(x48833,x48833)),x48834))), % 119.17/119.17 inference(scs_inference,[],[4839,3882,4829,4785,4685,4834,4845,2712,4126,143,100,85,4,46,15,6,7,13,12,10,14,8,11,45,2,9,5,53,16,3,18])). % 119.17/119.17 cnf(4893,plain, % 119.17/119.17 (~P7(x48931,f14(f12(f14(a9,x48932),f2(x48933,x48933)),x48934))), % 119.17/119.17 inference(rename_variables,[],[4883])). % 119.17/119.17 cnf(4898,plain, % 119.17/119.17 (E(f15(f15(x48981,f14(a1,x48982)),x48983),f15(f15(x48981,a1),x48983))), % 119.17/119.17 inference(scs_inference,[],[4883,4877,4276,85,4,46,15,6])). % 119.17/119.17 cnf(4899,plain, % 119.17/119.17 (E(f15(x48991,f15(x48992,f14(a1,x48993))),f15(x48991,f15(x48992,a1)))), % 119.17/119.17 inference(scs_inference,[],[4883,4877,4276,85,4,46,15,6,7])). % 119.17/119.17 cnf(4908,plain, % 119.17/119.17 (~E(f15(f15(x49081,x49082),f16(x49081)),f12(a1,x49083))), % 119.17/119.17 inference(scs_inference,[],[4882,4883,4877,4276,85,4,46,15,6,7,13,12,10,14,8,11,45,2])). % 119.17/119.17 cnf(4911,plain, % 119.17/119.17 (P1(f14(f12(f14(a9,x49111),f2(x49112,x49112)),x49113))), % 119.17/119.17 inference(scs_inference,[],[4882,4883,4893,4877,4276,2264,85,4,46,15,6,7,13,12,10,14,8,11,45,2,9,5,53])). % 119.17/119.17 cnf(4919,plain, % 119.17/119.17 (~P7(x49191,f12(f2(a9,a1),a9))), % 119.17/119.17 inference(scs_inference,[],[4882,4782,4783,4883,4893,4877,4276,4598,2264,42,41,85,4,46,15,6,7,13,12,10,14,8,11,45,2,9,5,53,16,3,18])). % 119.17/119.17 cnf(4927,plain, % 119.17/119.17 (~E(a11,f12(f2(a9,a1),a9))), % 119.17/119.17 inference(scs_inference,[],[4919,4278,9,5,85])). % 119.17/119.17 cnf(4928,plain, % 119.17/119.17 (~P7(x49281,f12(f2(a9,a1),a9))), % 119.17/119.17 inference(rename_variables,[],[4919])). % 119.17/119.17 cnf(4929,plain, % 119.17/119.17 (E(f12(f14(f14(a1,x49291),x49292),x49293),f12(f14(a1,x49292),x49293))), % 119.17/119.17 inference(scs_inference,[],[4919,4278,9,5,85,4])). % 119.17/119.17 cnf(4944,plain, % 119.17/119.17 (P1(f12(f2(a9,a1),a9))), % 119.17/119.17 inference(scs_inference,[],[4919,4928,4227,4911,4278,2685,9,5,85,4,15,46,6,7,13,12,10,14,8,11,45,2,53])). % 119.17/119.17 cnf(4948,plain, % 119.17/119.17 (P7(f6(f15(f15(x49481,f14(a1,x49482)),f16(x49481))),f15(f16(x49481),f15(x49481,a1)))), % 119.17/119.17 inference(scs_inference,[],[4919,4928,4227,4911,4899,4278,3479,2685,9,5,85,4,15,46,6,7,13,12,10,14,8,11,45,2,53,18])). % 119.17/119.17 cnf(4952,plain, % 119.17/119.17 (~E(f12(f14(a5,a13),f14(a5,a13)),f14(a9,x49521))), % 119.17/119.17 inference(scs_inference,[],[4874,4919,4928,4227,4911,4899,4278,3479,2685,70,62,9,5,85,4,15,46,6,7,13,12,10,14,8,11,45,2,53,18,16,3])). % 119.17/119.17 cnf(4965,plain, % 119.17/119.17 (E(f12(x49651,f2(f14(a1,x49652),f14(a1,x49653))),f12(x49651,f2(a1,a1)))), % 119.17/119.17 inference(scs_inference,[],[4328,9,5])). % 119.17/119.17 cnf(4967,plain, % 119.17/119.17 (~P7(x49671,f14(f14(f12(x49672,a1),x49673),x49674))), % 119.17/119.17 inference(rename_variables,[],[4800])). % 119.17/119.17 cnf(4983,plain, % 119.17/119.17 (E(f12(f2(a9,a1),a9),a1)), % 119.17/119.17 inference(scs_inference,[],[4944,4800,4948,4328,9,5,85,4,46,15,6,51,7,13,12,10,54,14,8,45])). % 119.17/119.17 cnf(4987,plain, % 119.17/119.17 (P1(f14(f14(f12(x49871,a1),x49872),x49873))), % 119.17/119.17 inference(scs_inference,[],[4952,4944,4800,4967,4948,4328,2240,9,5,85,4,46,15,6,51,7,13,12,10,54,14,8,45,11,2,53])). % 119.17/119.17 cnf(4991,plain, % 119.17/119.17 (~P7(x49911,f12(f12(f12(a1,a1),f12(a1,a9)),f2(a9,a1)))), % 119.17/119.17 inference(scs_inference,[],[4952,4944,4800,4967,4948,4328,4380,4108,2240,9,5,85,4,46,15,6,51,7,13,12,10,54,14,8,45,11,2,53,18])). % 119.17/119.17 cnf(4994,plain, % 119.17/119.17 (~E(a1,f12(a11,a11))), % 119.17/119.17 inference(scs_inference,[],[25,4952,4944,4800,4967,4948,4328,4380,4108,2240,143,9,5,85,4,46,15,6,51,7,13,12,10,54,14,8,45,11,2,53,18,16])). % 119.17/119.17 cnf(5000,plain, % 119.17/119.17 (P3(f6(a1),f14(a1,x50001))), % 119.17/119.17 inference(scs_inference,[],[25,4952,4944,4742,4750,4800,4967,4848,4948,2235,4328,4106,4380,4108,2240,143,41,9,5,85,4,46,15,6,51,7,13,12,10,54,14,8,45,11,2,53,18,16,3,20,23])). % 119.17/119.17 cnf(5014,plain, % 119.17/119.17 (~P7(x50141,f12(f12(f12(a1,a1),f12(a1,a9)),f2(a9,a1)))), % 119.17/119.17 inference(rename_variables,[],[4991])). % 119.17/119.17 cnf(5022,plain, % 119.17/119.17 (E(f14(f12(f2(a9,a1),a9),x50221),f14(a1,x50221))), % 119.17/119.17 inference(scs_inference,[],[4983,4991,4987,9,5,85,4,46,15,6,7,13,12])). % 119.17/119.17 cnf(5030,plain, % 119.17/119.17 (P1(f12(f12(f12(a1,a1),f12(a1,a9)),f2(a9,a1)))), % 119.17/119.17 inference(scs_inference,[],[4659,4983,4991,5014,4987,213,9,5,85,4,46,15,6,7,13,12,10,14,8,45,11,2,53])). % 119.17/119.17 cnf(5034,plain, % 119.17/119.17 (~P7(x50341,f12(f14(a9,x50342),f2(f14(a1,x50343),f14(a1,x50344))))), % 119.17/119.17 inference(scs_inference,[],[4659,4983,4991,5014,4987,4965,4690,213,9,5,85,4,46,15,6,7,13,12,10,14,8,45,11,2,53,18])). % 119.17/119.17 cnf(5040,plain, % 119.17/119.17 (~E(f12(f12(a1,x50401),f12(a1,x50401)),f14(a5,a13))), % 119.17/119.17 inference(scs_inference,[],[4994,4659,4983,4991,5014,4987,4965,4149,4690,213,44,156,43,9,5,85,4,46,15,6,7,13,12,10,14,8,45,11,2,53,18,16,3,22,21])). % 119.17/119.17 cnf(5046,plain, % 119.17/119.17 (~P7(x50461,f14(f12(a9,f2(x50462,x50462)),x50463))), % 119.17/119.17 inference(rename_variables,[],[4733])). % 119.17/119.17 cnf(5058,plain, % 119.17/119.17 (E(f12(f12(f12(a1,a1),f12(a1,a9)),f2(a9,a1)),a1)), % 119.17/119.17 inference(scs_inference,[],[5030,4733,4259,5,9,85,46,4,15,6,7,13,12,10,14,8,45])). % 119.17/119.17 cnf(5061,plain, % 119.17/119.17 (~E(f14(a5,a13),f12(f12(a1,x50611),f12(a1,x50611)))), % 119.17/119.17 inference(scs_inference,[],[5040,5030,4733,4259,5,9,85,46,4,15,6,7,13,12,10,14,8,45,11,2])). % 119.17/119.17 cnf(5062,plain, % 119.17/119.17 (P1(f14(f12(a9,f2(x50621,x50621)),a1))), % 119.17/119.17 inference(scs_inference,[],[5040,5030,4733,5046,4259,4345,5,9,85,46,4,15,6,7,13,12,10,14,8,45,11,2,53])). % 119.17/119.17 cnf(5066,plain, % 119.17/119.17 (~P7(x50661,f12(a9,f2(f14(a1,x50662),f14(a1,x50663))))), % 119.17/119.17 inference(scs_inference,[],[5040,5030,4733,5046,4259,4563,4965,4345,5,9,85,46,4,15,6,7,13,12,10,14,8,45,11,2,53,18])). % 119.17/119.17 cnf(5089,plain, % 119.17/119.17 (E(f14(f12(f12(f12(a1,a1),f12(a1,a9)),f2(a9,a1)),x50891),f14(a1,x50891))), % 119.17/119.17 inference(scs_inference,[],[5058,4508,5062,9,5,85,46,4,15,6,7,13,12])). % 119.17/119.17 cnf(5097,plain, % 119.17/119.17 (P1(f12(f14(a9,x50971),f2(f14(a1,x50972),f14(a1,x50973))))), % 119.17/119.17 inference(scs_inference,[],[4776,5058,4508,5034,5062,2716,9,5,85,46,4,15,6,7,13,12,10,14,45,8,11,2,53])). % 119.17/119.17 cnf(5101,plain, % 119.17/119.17 (~P7(x51011,f14(f12(f2(a9,a1),a9),x51012))), % 119.17/119.17 inference(scs_inference,[],[4776,5058,5022,4508,5034,5062,2716,4126,9,5,85,46,4,15,6,7,13,12,10,14,45,8,11,2,53,18])). % 119.17/119.17 cnf(5103,plain, % 119.17/119.17 (~E(f12(f14(a5,a13),f14(a5,a13)),f12(f12(a1,x51031),f12(a1,x51031)))), % 119.17/119.17 inference(scs_inference,[],[5061,4776,5058,5022,4508,5034,5062,2716,4126,62,9,5,85,46,4,15,6,7,13,12,10,14,45,8,11,2,53,18,3])). % 119.17/119.17 cnf(5119,plain, % 119.17/119.17 (~P7(x51191,f14(f12(f2(a9,a1),a9),x51192))), % 119.17/119.17 inference(rename_variables,[],[5101])). % 119.17/119.17 cnf(5135,plain, % 119.17/119.17 (P1(f14(f12(f2(a9,a1),a9),x51351))), % 119.17/119.17 inference(scs_inference,[],[3549,5101,5119,5097,4260,2248,5,9,85,46,4,15,6,7,12,13,10,14,45,8,11,2,53])). % 119.17/119.17 cnf(5139,plain, % 119.17/119.17 (~P7(x51391,f12(f2(f14(a1,x51392),f14(a1,x51393)),a9))), % 119.17/119.17 inference(scs_inference,[],[3549,5101,5119,5097,5066,4260,2248,41,5,9,85,46,4,15,6,7,12,13,10,14,45,8,11,2,53,18])). % 119.17/119.17 cnf(5157,plain, % 119.17/119.17 (~P7(x51571,f12(f2(f14(a1,x51572),f14(a1,x51573)),a9))), % 119.17/119.17 inference(rename_variables,[],[5139])). % 119.17/119.17 cnf(5162,plain, % 119.17/119.17 (E(f15(f16(f14(a1,x51621)),x51622),f15(f16(a1),x51622))), % 119.17/119.17 inference(scs_inference,[],[5135,5139,4269,9,5,85,46,4,15,6])). % 119.17/119.17 cnf(5163,plain, % 119.17/119.17 (E(f15(x51631,f16(f14(a1,x51632))),f15(x51631,f16(a1)))), % 119.17/119.17 inference(scs_inference,[],[5135,5139,4269,9,5,85,46,4,15,6,7])). % 119.17/119.17 cnf(5172,plain, % 119.17/119.17 (~E(f12(f12(a1,x51721),f12(a1,x51722)),a11)), % 119.17/119.17 inference(scs_inference,[],[3596,5135,5139,4269,9,5,85,46,4,15,6,7,13,12,10,45,14,8,11,2])). % 119.17/119.17 cnf(5173,plain, % 119.17/119.17 (P1(f12(f2(f14(a1,x51731),f14(a1,x51732)),a9))), % 119.17/119.17 inference(scs_inference,[],[3596,5135,5139,5157,4269,2712,9,5,85,46,4,15,6,7,13,12,10,45,14,8,11,2,53])). % 119.17/119.17 cnf(5177,plain, % 119.17/119.17 (~P7(x51771,f14(f12(f12(f12(a1,a1),f12(a1,a9)),f2(a9,a1)),x51772))), % 119.17/119.17 inference(scs_inference,[],[3596,5135,5139,5157,5089,4269,2712,4126,9,5,85,46,4,15,6,7,13,12,10,45,14,8,11,2,53,18])). % 119.17/119.17 cnf(5179,plain, % 119.17/119.17 (~E(f12(a11,a11),f12(f12(a1,x51791),f12(a1,x51792)))), % 119.17/119.17 inference(scs_inference,[],[3596,5135,5139,5157,5089,4269,2712,4126,62,9,5,85,46,4,15,6,7,13,12,10,45,14,8,11,2,53,18,3])). % 119.17/119.17 cnf(5188,plain, % 119.17/119.17 (~P7(x51881,f14(f12(f12(f12(a1,a1),f12(a1,a9)),f2(x51882,x51882)),x51883))), % 119.17/119.17 inference(rename_variables,[],[4806])). % 119.17/119.17 cnf(5204,plain, % 119.17/119.17 (~P7(f15(f16(f14(a1,x52041)),f15(a1,x52042)),f6(f15(f15(a1,x52042),f16(a1))))), % 119.17/119.17 inference(scs_inference,[],[5179,5173,5162,3484,4806,4277,9,5,85,46,4,15,6,7,13,12,10,45,14,8,11,2,17])). % 119.17/119.17 cnf(5207,plain, % 119.17/119.17 (P1(f14(f12(f12(f12(a1,a1),f12(a1,a9)),f2(x52071,x52071)),x52072))), % 119.17/119.17 inference(scs_inference,[],[5179,5173,5162,3484,4806,5188,4277,2264,9,5,85,46,4,15,6,7,13,12,10,45,14,8,11,2,17,53])). % 119.17/119.17 cnf(5211,plain, % 119.17/119.17 (~P7(x52111,f12(f2(a9,a1),f12(f12(a1,a1),f12(a1,a9))))), % 119.17/119.17 inference(scs_inference,[],[5179,5173,5162,3484,4806,5188,4277,4991,2264,41,9,5,85,46,4,15,6,7,13,12,10,45,14,8,11,2,17,53,18])). % 119.17/119.17 cnf(5230,plain, % 119.17/119.17 (~P7(x52301,f12(f2(a9,a1),f12(f12(a1,a1),f12(a1,a9))))), % 119.17/119.17 inference(rename_variables,[],[5211])). % 119.17/119.17 cnf(5245,plain, % 119.17/119.17 (~E(f12(a9,f2(x52451,x52451)),a11)), % 119.17/119.17 inference(scs_inference,[],[4566,5211,5207,4265,5,9,85,46,4,15,6,7,13,12,10,45,14,8,11,2])). % 119.17/119.17 cnf(5246,plain, % 119.17/119.17 (P1(f12(f2(a9,a1),f12(f12(a1,a1),f12(a1,a9))))), % 119.17/119.17 inference(scs_inference,[],[4566,5211,5230,5207,4265,2685,5,9,85,46,4,15,6,7,13,12,10,45,14,8,11,2,53])). % 119.17/119.17 cnf(5250,plain, % 119.17/119.17 (~P7(x52501,f12(f14(f14(a1,x52502),x52503),f2(x52504,x52504)))), % 119.17/119.17 inference(scs_inference,[],[4566,5211,5230,5207,4929,4265,4460,2685,5,9,85,46,4,15,6,7,13,12,10,45,14,8,11,2,53,18])). % 119.17/119.17 cnf(5252,plain, % 119.17/119.17 (~E(f15(f15(f14(a1,x52521),x52522),f16(a1)),f12(a1,x52523))), % 119.17/119.17 inference(scs_inference,[],[4908,4566,5211,5230,5163,5207,4929,4265,4460,2685,5,9,85,46,4,15,6,7,13,12,10,45,14,8,11,2,53,18,3])). % 119.17/119.17 cnf(5263,plain, % 119.17/119.17 (~P7(x52631,f12(f14(f14(a1,x52632),x52633),f2(x52634,x52634)))), % 119.17/119.17 inference(rename_variables,[],[5250])). % 119.17/119.17 cnf(5267,plain, % 119.17/119.17 (E(f2(x52671,f7(a9)),f2(x52671,f7(a1)))), % 119.17/119.17 inference(scs_inference,[],[5250,5246,4035,9,5,85,46,4,15])). % 119.17/119.17 cnf(5276,plain, % 119.17/119.17 (E(f2(f7(a9),x52761),f2(f7(a1),x52761))), % 119.17/119.17 inference(scs_inference,[],[5250,5246,4035,9,5,85,46,4,15,6,7,13,12,10,45,8,14])). % 119.17/119.17 cnf(5278,plain, % 119.17/119.17 (~E(f12(f2(a9,a1),a9),a11)), % 119.17/119.17 inference(scs_inference,[],[4927,5250,5246,4035,9,5,85,46,4,15,6,7,13,12,10,45,8,14,11,2])). % 119.17/119.17 cnf(5279,plain, % 119.17/119.17 (P1(f12(f14(f14(a1,x52791),x52792),f2(x52793,x52793)))), % 119.17/119.17 inference(scs_inference,[],[4927,5250,5263,5246,4035,2240,9,5,85,46,4,15,6,7,13,12,10,45,8,14,11,2,53])). % 119.17/119.17 cnf(5283,plain, % 119.17/119.17 (~P7(x52831,f12(f12(f12(a1,a1),f12(a1,a9)),f2(f14(a1,x52832),f14(a1,x52833))))), % 119.17/119.17 inference(scs_inference,[],[4927,5250,5263,5246,4035,4965,4380,2240,9,5,85,46,4,15,6,7,13,12,10,45,8,14,11,2,53,18])). % 119.17/119.17 cnf(5307,plain, % 119.17/119.17 (~P7(x53071,f14(f12(f12(f12(a1,a1),f12(a1,a9)),f2(a9,a1)),x53072))), % 119.17/119.17 inference(rename_variables,[],[5177])). % 119.17/119.17 cnf(5317,plain, % 119.17/119.17 (E(f12(f14(f14(a1,x53171),x53172),f2(x53173,x53173)),a1)), % 119.17/119.17 inference(scs_inference,[],[5279,5177,4036,9,5,85,46,4,15,6,7,12,13,10,45])). % 119.17/119.17 cnf(5322,plain, % 119.17/119.17 (~E(f12(a9,f2(a9,a1)),a11)), % 119.17/119.17 inference(scs_inference,[],[4605,5279,5177,4036,9,5,85,46,4,15,6,7,12,13,10,45,8,14,11,2])). % 119.17/119.17 cnf(5323,plain, % 119.17/119.17 (P1(f14(f12(f12(f12(a1,a1),f12(a1,a9)),f2(a9,a1)),x53231))), % 119.17/119.17 inference(scs_inference,[],[4605,5279,5177,5307,4036,213,9,5,85,46,4,15,6,7,12,13,10,45,8,14,11,2,53])). % 119.17/119.17 cnf(5327,plain, % 119.17/119.17 (~P7(x53271,f14(f12(f12(f12(a1,x53272),f12(a1,x53272)),f12(a3,x53273)),x53274))), % 119.17/119.17 inference(scs_inference,[],[4605,5279,5177,5307,4235,4036,213,4126,9,5,85,46,4,15,6,7,12,13,10,45,8,14,11,2,53,18])). % 119.17/119.17 cnf(5329,plain, % 119.17/119.17 (~E(f12(f2(a1,a1),a9),a11)), % 119.17/119.17 inference(scs_inference,[],[5278,4605,5279,5177,5307,4235,4036,4116,213,4126,9,5,85,46,4,15,6,7,12,13,10,45,8,14,11,2,53,18,3])). % 119.17/119.17 cnf(5344,plain, % 119.17/119.17 (~E(a11,f12(f2(a1,a1),a9))), % 119.17/119.17 inference(scs_inference,[],[5329,5317,5323,10,45,8,14,11,2])). % 119.17/119.17 cnf(5348,plain, % 119.17/119.17 (~P7(x53481,f14(f12(f12(f12(a1,x53482),f12(a1,x53482)),f12(a3,x53483)),x53484))), % 119.17/119.17 inference(rename_variables,[],[5327])). % 119.17/119.17 cnf(5356,plain, % 119.17/119.17 (E(f14(f12(f14(f14(a1,x53561),x53562),f2(x53563,x53563)),x53564),f14(a1,x53564))), % 119.17/119.17 inference(scs_inference,[],[5329,5317,5323,5327,10,45,8,14,11,2,9,5,85,46,4,15,6,7,13,12])). % 119.17/119.17 cnf(5357,plain, % 119.17/119.17 (E(f2(f7(a9),f7(a9)),f2(f7(a1),f7(a1)))), % 119.17/119.17 inference(scs_inference,[],[5329,5267,5276,5317,5323,5327,10,45,8,14,11,2,9,5,85,46,4,15,6,7,13,12,3])). % 119.17/119.17 cnf(5360,plain, % 119.17/119.17 (P1(f14(f12(f12(f12(a1,x53601),f12(a1,x53601)),f12(a3,x53602)),a1))), % 119.17/119.17 inference(scs_inference,[],[5329,5267,5276,5317,5323,5327,5348,4345,10,45,8,14,11,2,9,5,85,46,4,15,6,7,13,12,3,53])). % 119.17/119.17 cnf(5364,plain, % 119.17/119.17 (~P7(x53641,f12(f2(f14(a1,x53642),f14(a1,x53643)),f12(f12(a1,a1),f12(a1,a9))))), % 119.17/119.17 inference(scs_inference,[],[5329,5267,5276,5317,5323,5327,5348,5283,4345,41,10,45,8,14,11,2,9,5,85,46,4,15,6,7,13,12,3,53,18])). % 119.17/119.17 cnf(5376,plain, % 119.17/119.17 (E(f2(f16(a9),x53761),f2(f16(a1),x53761))), % 119.17/119.17 inference(scs_inference,[],[5360,4043,45,10,8,14])). % 119.17/119.17 cnf(5382,plain, % 119.17/119.17 (~P7(x53821,f12(f2(f14(a1,x53822),f14(a1,x53823)),f12(f12(a1,a1),f12(a1,a9))))), % 119.17/119.17 inference(rename_variables,[],[5364])). % 119.17/119.17 cnf(5386,plain, % 119.17/119.17 (E(f2(x53861,f16(a9)),f2(x53861,f16(a1)))), % 119.17/119.17 inference(scs_inference,[],[3610,5364,5360,4043,45,10,8,14,11,2,9,5,85,46,4,15])). % 119.17/119.17 cnf(5388,plain, % 119.17/119.17 (E(f15(x53881,f16(a9)),f15(x53881,f16(a1)))), % 119.17/119.17 inference(scs_inference,[],[3610,5364,5360,4043,45,10,8,14,11,2,9,5,85,46,4,15,6,7])). % 119.17/119.17 cnf(5393,plain, % 119.17/119.17 (P1(f12(f2(f14(a1,x53931),f14(a1,x53932)),f12(f12(a1,a1),f12(a1,a9))))), % 119.17/119.17 inference(scs_inference,[],[3610,5357,5364,5382,5360,4043,2716,62,45,10,8,14,11,2,9,5,85,46,4,15,6,7,12,13,3,53])). % 119.17/119.17 cnf(5398,plain, % 119.17/119.17 (~P7(x53981,f14(f12(f14(f14(a1,x53982),x53983),f2(x53984,x53984)),x53985))), % 119.17/119.17 inference(scs_inference,[],[26,3610,5357,5356,5364,5382,5360,4043,2716,42,4126,62,45,10,8,14,11,2,9,5,85,46,4,15,6,7,12,13,3,53,16,18])). % 119.17/119.17 cnf(5417,plain, % 119.17/119.17 (~P7(x54171,f14(f12(f14(f14(a1,x54172),x54173),f2(x54174,x54174)),x54175))), % 119.17/119.17 inference(rename_variables,[],[5398])). % 119.17/119.17 cnf(5428,plain, % 119.17/119.17 (P1(f14(f12(f14(f14(a1,x54281),x54282),f2(x54283,x54283)),x54284))), % 119.17/119.17 inference(scs_inference,[],[5322,4803,5398,5417,5393,4053,4048,2248,10,45,8,14,11,2,9,5,85,46,15,4,6,7,13,12,3,53])). % 119.17/119.17 cnf(5433,plain, % 119.17/119.17 (~P7(x54331,f12(a9,f2(f14(a1,x54332),a1)))), % 119.17/119.17 inference(scs_inference,[],[5322,4803,5398,5417,5393,4053,4048,4563,4310,2248,70,10,45,8,14,11,2,9,5,85,46,15,4,6,7,13,12,3,53,16,18])). % 119.17/119.17 cnf(5436,plain, % 119.17/119.17 (~P7(x54361,f14(f12(a1,x54362),x54363))), % 119.17/119.17 inference(scs_inference,[],[5322,4803,5398,5417,5393,4053,4048,4563,4310,4148,154,2248,70,10,45,8,14,11,2,9,5,85,46,15,4,6,7,13,12,3,53,16,18,56])). % 119.17/119.17 cnf(5460,plain, % 119.17/119.17 (~E(a11,f14(f12(a1,x54601),x54602))), % 119.17/119.17 inference(scs_inference,[],[5436,5252,5428,4123,45,10,8,14,11,2,9,5,85])). % 119.17/119.17 cnf(5461,plain, % 119.17/119.17 (~P7(x54611,f14(f12(a1,x54612),x54613))), % 119.17/119.17 inference(rename_variables,[],[5436])). % 119.17/119.17 cnf(5473,plain, % 119.17/119.17 (P1(f12(a9,f2(f14(a1,x54731),a1)))), % 119.17/119.17 inference(scs_inference,[],[5436,5252,5376,5386,5433,5428,4123,2712,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12,3,53])). % 119.17/119.17 cnf(5477,plain, % 119.17/119.17 (~E(a3,f15(f15(x54771,x54772),f16(x54771)))), % 119.17/119.17 inference(scs_inference,[],[26,5436,5252,5376,5386,5433,5428,4123,2712,44,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12,3,53,16])). % 119.17/119.17 cnf(5481,plain, % 119.17/119.17 (~P7(x54811,f14(f14(f12(a1,x54812),x54813),x54814))), % 119.17/119.17 inference(scs_inference,[],[26,5436,5461,5252,5376,5386,5388,5433,5428,4123,3980,4087,2712,44,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12,3,53,16,18,56])). % 119.17/119.17 cnf(5484,plain, % 119.17/119.17 (~P1(f15(f15(a9,x54841),f16(a1)))), % 119.17/119.17 inference(scs_inference,[],[26,5436,5461,5252,5376,5386,5388,5433,5428,4123,3980,4087,2712,44,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12,3,53,16,18,56,50])). % 119.17/119.17 cnf(5488,plain, % 119.17/119.17 (~P7(f15(f15(a9,x54881),f16(a1)),f6(f15(f16(a9),f15(a9,x54881))))), % 119.17/119.17 inference(scs_inference,[],[26,5436,5461,5252,5376,5386,5388,5433,5428,4123,3980,4087,2712,44,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12,3,53,16,18,56,50,51,54])). % 119.17/119.17 cnf(5493,plain, % 119.17/119.17 (E(f12(a9,f2(f14(a1,x54931),a1)),a1)), % 119.17/119.17 inference(scs_inference,[],[5473,45])). % 119.17/119.17 cnf(5499,plain, % 119.17/119.17 (~E(f15(f15(x54991,x54992),f16(x54991)),a3)), % 119.17/119.17 inference(scs_inference,[],[5477,5473,3992,45,10,8,14,11,2])). % 119.17/119.17 cnf(5503,plain, % 119.17/119.17 (~P7(x55031,f14(f14(f12(a1,x55032),x55033),x55034))), % 119.17/119.17 inference(rename_variables,[],[5481])). % 119.17/119.17 cnf(5512,plain, % 119.17/119.17 (~E(f12(a11,a11),f14(f12(a1,x55121),x55122))), % 119.17/119.17 inference(scs_inference,[],[5477,5460,5481,5473,3992,62,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12,3])). % 119.17/119.17 cnf(5514,plain, % 119.17/119.17 (P1(f14(f14(f12(a1,x55141),x55142),x55143))), % 119.17/119.17 inference(scs_inference,[],[5477,5460,5481,5503,5473,3992,2264,62,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12,3,53])). % 119.17/119.17 cnf(5518,plain, % 119.17/119.17 (~E(a3,f15(f15(a9,x55181),f16(a1)))), % 119.17/119.17 inference(scs_inference,[],[26,5484,5477,5460,5481,5503,5473,3992,2264,62,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12,3,53,16])). % 119.17/119.17 cnf(5519,plain, % 119.17/119.17 (~P7(x55191,f12(f2(f14(a1,x55192),a1),a9))), % 119.17/119.17 inference(scs_inference,[],[26,5484,5477,5460,5481,5503,5473,3992,5433,2264,41,62,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12,3,53,16,18])). % 119.17/119.17 cnf(5551,plain, % 119.17/119.17 (~P7(x55511,f14(f12(f14(a1,x55512),x55513),x55514))), % 119.17/119.17 inference(scs_inference,[],[26,5512,5514,5519,5493,4412,3911,5436,5484,2566,832,100,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12,3,53,16,18])). % 119.17/119.17 cnf(5553,plain, % 119.17/119.17 (~P7(f15(f15(a9,x55531),f16(a1)),f6(f15(f16(a1),f15(a9,x55531))))), % 119.17/119.17 inference(scs_inference,[],[26,5512,5514,5519,5493,4412,3911,5436,5484,2566,832,100,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12,3,53,16,18,54])). % 119.17/119.17 cnf(5562,plain, % 119.17/119.17 (E(f12(f12(x55621,a1),f12(x55621,a1)),a1)), % 119.17/119.17 inference(scs_inference,[],[209,45])). % 119.17/119.17 cnf(5566,plain, % 119.17/119.17 (E(f2(f15(a3,x55661),x55662),f2(f15(a1,x55661),x55662))), % 119.17/119.17 inference(scs_inference,[],[3915,209,45,10,8,14])). % 119.17/119.17 cnf(5570,plain, % 119.17/119.17 (E(f12(x55701,f15(a3,x55702)),f12(x55701,f15(a1,x55702)))), % 119.17/119.17 inference(scs_inference,[],[5518,3915,209,45,10,8,14,11,2,9,5])). % 119.17/119.17 cnf(5572,plain, % 119.17/119.17 (~P7(x55721,f14(f12(f14(a1,x55722),x55723),x55724))), % 119.17/119.17 inference(rename_variables,[],[5551])). % 119.17/119.17 cnf(5574,plain, % 119.17/119.17 (E(f2(x55741,f15(a3,x55742)),f2(x55741,f15(a1,x55742)))), % 119.17/119.17 inference(scs_inference,[],[5518,5551,3915,209,45,10,8,14,11,2,9,5,85,4,15])). % 119.17/119.17 cnf(5575,plain, % 119.17/119.17 (E(f15(f15(a3,x55751),x55752),f15(f15(a1,x55751),x55752))), % 119.17/119.17 inference(scs_inference,[],[5518,5551,3915,209,45,10,8,14,11,2,9,5,85,4,15,6])). % 119.17/119.17 cnf(5576,plain, % 119.17/119.17 (E(f15(x55761,f15(a3,x55762)),f15(x55761,f15(a1,x55762)))), % 119.17/119.17 inference(scs_inference,[],[5518,5551,3915,209,45,10,8,14,11,2,9,5,85,4,15,6,7])). % 119.17/119.17 cnf(5577,plain, % 119.17/119.17 (E(f14(x55771,f15(a3,x55772)),f14(x55771,f15(a1,x55772)))), % 119.17/119.17 inference(scs_inference,[],[5518,5551,3915,209,45,10,8,14,11,2,9,5,85,4,15,6,7,13])). % 119.17/119.17 cnf(5578,plain, % 119.17/119.17 (E(f14(f15(a3,x55781),x55782),f14(f15(a1,x55781),x55782))), % 119.17/119.17 inference(scs_inference,[],[5518,5551,3915,209,45,10,8,14,11,2,9,5,85,4,15,6,7,13,12])). % 119.17/119.17 cnf(5582,plain, % 119.17/119.17 (P1(f14(f12(f14(a1,x55821),x55822),x55823))), % 119.17/119.17 inference(scs_inference,[],[5499,5518,5551,5572,3915,5163,209,2240,45,10,8,14,11,2,9,5,85,4,15,6,7,13,12,3,53])). % 119.17/119.17 cnf(5587,plain, % 119.17/119.17 (~P7(x55871,f12(f12(f14(a9,x55872),f14(a1,x55873)),f12(f14(a9,x55874),a9)))), % 119.17/119.17 inference(scs_inference,[],[5499,5518,5551,5572,3915,5163,4368,5484,5279,4243,209,2240,45,10,8,14,11,2,9,5,85,4,15,6,7,13,12,3,53,16,18])). % 119.17/119.17 cnf(5604,plain, % 119.17/119.17 (E(f2(f12(f12(x56041,a1),f12(x56041,a1)),x56042),f2(a1,x56042))), % 119.17/119.17 inference(scs_inference,[],[5562,5582,45,10,8,14])). % 119.17/119.17 cnf(5610,plain, % 119.17/119.17 (~P7(x56101,f12(f12(f14(a9,x56102),f14(a1,x56103)),f12(f14(a9,x56104),a9)))), % 119.17/119.17 inference(rename_variables,[],[5587])). % 119.17/119.17 cnf(5614,plain, % 119.17/119.17 (E(f2(x56141,f12(f12(x56142,a1),f12(x56142,a1))),f2(x56141,a1))), % 119.17/119.17 inference(scs_inference,[],[5562,3469,5582,5587,45,10,8,14,11,2,9,5,85,46,4,15])). % 119.17/119.17 cnf(5618,plain, % 119.17/119.17 (E(f14(f12(f12(x56181,a1),f12(x56181,a1)),x56182),f14(a1,x56182))), % 119.17/119.17 inference(scs_inference,[],[5562,3469,5582,5587,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12])). % 119.17/119.17 cnf(5625,plain, % 119.17/119.17 (P1(f12(f12(f14(a9,x56251),f14(a1,x56252)),f12(f14(a9,x56253),a9)))), % 119.17/119.17 inference(scs_inference,[],[5562,3469,5566,5574,5582,5587,5610,5488,4898,2685,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12,17,3,53])). % 119.17/119.17 cnf(5636,plain, % 119.17/119.17 (~P1(f15(f15(a1,x56361),f16(a3)))), % 119.17/119.17 inference(scs_inference,[],[26,5562,3469,5566,5570,5574,5575,5582,2693,5587,5610,5488,4898,3980,2685,2954,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12,17,3,53,16,18,23,50])). % 119.17/119.17 cnf(5638,plain, % 119.17/119.17 (P3(f6(f15(f16(a3),f15(a3,x56381))),f15(f15(a1,x56381),f16(a3)))), % 119.17/119.17 inference(scs_inference,[],[26,5562,3469,5566,5570,5574,5575,5582,2693,5587,5610,5488,4898,3980,2685,2954,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12,17,3,53,16,18,23,50,51])). % 119.17/119.17 cnf(5640,plain, % 119.17/119.17 (~P7(f15(f15(a1,x56401),f16(a3)),f6(f15(f16(a3),f15(a3,x56401))))), % 119.17/119.17 inference(scs_inference,[],[26,5562,3469,5566,5570,5574,5575,5582,2693,5587,5610,5488,4898,3980,2685,2954,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12,17,3,53,16,18,23,50,51,54])). % 119.17/119.17 cnf(5653,plain, % 119.17/119.17 (E(f12(x56531,f2(x56532,a3)),f12(x56531,f2(x56532,a1)))), % 119.17/119.17 inference(scs_inference,[],[4762,5625,3916,45,10,8,14,11,2,9,5])). % 119.17/119.17 cnf(5655,plain, % 119.17/119.17 (~P7(x56551,f12(f2(f14(a1,x56552),a1),f12(f12(a1,a1),f12(a1,a9))))), % 119.17/119.17 inference(rename_variables,[],[4768])). % 119.17/119.17 cnf(5658,plain, % 119.17/119.17 (E(f12(f2(x56581,a3),x56582),f12(f2(x56581,a1),x56582))), % 119.17/119.17 inference(scs_inference,[],[4762,5625,4768,3916,45,10,8,14,11,2,9,5,85,46,4])). % 119.17/119.17 cnf(5666,plain, % 119.17/119.17 (~E(f12(a11,a11),f12(f2(a1,a1),a9))), % 119.17/119.17 inference(scs_inference,[],[5344,4762,5576,5625,5204,4768,3916,62,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12,17,3])). % 119.17/119.17 cnf(5668,plain, % 119.17/119.17 (P1(f12(f2(f14(a1,x56681),a1),f12(f12(a1,a1),f12(a1,a9))))), % 119.17/119.17 inference(scs_inference,[],[5344,4762,5576,5625,5204,4768,5655,3916,213,62,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12,17,3,53])). % 119.17/119.17 cnf(5672,plain, % 119.17/119.17 (~E(a3,f15(f15(a1,x56721),f16(a3)))), % 119.17/119.17 inference(scs_inference,[],[26,5636,5344,4762,5576,5625,5204,4768,5655,3916,213,62,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12,17,3,53,16])). % 119.17/119.17 cnf(5673,plain, % 119.17/119.17 (~P7(x56731,f12(f12(f14(a9,x56732),a9),f12(f14(a9,x56733),f14(a1,x56734))))), % 119.17/119.17 inference(scs_inference,[],[26,5636,5344,4762,5576,5625,5204,4768,5655,3916,5587,213,41,62,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12,17,3,53,16,18])). % 119.17/119.17 cnf(5690,plain, % 119.17/119.17 (E(f12(x56901,f2(a3,x56902)),f12(x56901,f2(a1,x56902)))), % 119.17/119.17 inference(scs_inference,[],[5666,5668,3917,45,10,8,14,11,2,9,5])). % 119.17/119.17 cnf(5710,plain, % 119.17/119.17 (~P7(x57101,f12(f12(f12(a1,a1),f12(a1,a9)),f2(f14(a1,x57102),a3)))), % 119.17/119.17 inference(scs_inference,[],[26,5666,5577,5578,5653,5673,5668,5553,3917,5636,5388,4418,2566,143,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12,17,3,53,16,18])). % 119.17/119.17 cnf(5712,plain, % 119.17/119.17 (~P7(f15(f15(a1,x57121),f16(a3)),f6(f15(f16(a3),f15(a1,x57121))))), % 119.17/119.17 inference(scs_inference,[],[26,5666,5577,5578,5653,5673,5668,5553,3917,5636,5388,4418,2566,143,45,10,8,14,11,2,9,5,85,46,4,15,6,7,13,12,17,3,53,16,18,54])). % 119.17/119.17 cnf(5726,plain, % 119.17/119.17 (E(f2(f8(a3),x57261),f2(f8(a1),x57261))), % 119.17/119.17 inference(scs_inference,[],[3912,10,8,14])). % 119.17/119.17 cnf(5732,plain, % 119.17/119.17 (~P7(x57321,f12(f12(f12(a1,a1),f12(a1,a9)),f2(f14(a1,x57322),a3)))), % 119.17/119.17 inference(rename_variables,[],[5710])). % 119.17/119.17 cnf(5734,plain, % 119.17/119.17 (E(f2(x57341,f8(a3)),f2(x57341,f8(a1)))), % 119.17/119.17 inference(scs_inference,[],[5672,5710,3912,10,8,14,11,2,9,5,85,4,15])). % 119.17/119.17 cnf(5739,plain, % 119.17/119.18 (~E(f12(f14(a1,x57391),f2(a1,a3)),a11)), % 119.17/119.18 inference(scs_inference,[],[4719,5672,5690,5710,3912,10,8,14,11,2,9,5,85,4,15,6,7,13,12,3])). % 119.17/119.18 cnf(5742,plain, % 119.17/119.18 (P1(f12(f12(f12(a1,a1),f12(a1,a9)),f2(f14(a1,x57421),a3)))), % 119.17/119.18 inference(scs_inference,[],[4719,5672,5690,5710,5732,3912,2716,10,8,14,11,2,9,5,85,4,15,6,7,13,12,3,53])). % 119.17/119.18 cnf(5743,plain, % 119.17/119.18 (~P7(x57431,f12(f12(f12(a1,a1),f12(a1,a9)),f2(f14(a1,x57432),a3)))), % 119.17/119.18 inference(rename_variables,[],[5710])). % 119.17/119.18 cnf(5747,plain, % 119.17/119.18 (~P7(x57471,f12(f2(f14(a1,x57472),a3),f12(f12(a1,a1),f12(a1,a9))))), % 119.17/119.18 inference(scs_inference,[],[4719,5672,5690,5710,5732,5743,3912,5636,5668,2716,41,10,8,14,11,2,9,5,85,4,15,6,7,13,12,3,53,16,18])). % 119.17/119.18 cnf(5762,plain, % 119.17/119.18 (E(f15(f16(a3),x57621),f15(f16(a1),x57621))), % 119.17/119.18 inference(scs_inference,[],[3914,6])). % 119.17/119.18 cnf(5763,plain, % 119.17/119.18 (E(f15(x57631,f16(a3)),f15(x57631,f16(a1)))), % 119.17/119.18 inference(scs_inference,[],[3914,6,7])). % 119.17/119.18 cnf(5772,plain, % 119.17/119.18 (~E(a11,f12(f14(a1,x57721),f2(a1,a3)))), % 119.17/119.18 inference(scs_inference,[],[5739,5742,3914,6,7,45,13,12,10,8,14,11,2])). % 119.17/119.18 cnf(5784,plain, % 119.17/119.18 (P1(f14(f14(f14(a1,x57841),x57842),a1))), % 119.17/119.18 inference(scs_inference,[],[5739,5726,5734,5747,5742,4375,3914,4345,6,7,45,13,12,10,8,14,11,2,9,5,46,85,4,15,3,53])). % 119.17/119.18 cnf(5788,plain, % 119.17/119.18 (~P7(x57881,f14(f12(f12(x57882,a1),f12(x57882,a1)),x57883))), % 119.17/119.18 inference(scs_inference,[],[5739,5726,5734,5618,5747,5742,4375,3914,4345,4126,6,7,45,13,12,10,8,14,11,2,9,5,46,85,4,15,3,53,18])). % 119.17/119.18 cnf(5793,plain, % 119.17/119.18 (E(f15(f7(a3),x57931),f15(f7(a1),x57931))), % 119.17/119.18 inference(scs_inference,[],[3918,6])). % 119.17/119.18 cnf(5794,plain, % 119.17/119.18 (E(f15(x57941,f7(a3)),f15(x57941,f7(a1)))), % 119.17/119.18 inference(scs_inference,[],[3918,6,7])). % 119.17/119.18 cnf(5797,plain, % 119.17/119.18 (E(f14(x57971,f7(a3)),f14(x57971,f7(a1)))), % 119.17/119.18 inference(scs_inference,[],[5784,3918,6,7,45,13])). % 119.17/119.18 cnf(5798,plain, % 119.17/119.18 (E(f14(f7(a3),x57981),f14(f7(a1),x57981))), % 119.17/119.18 inference(scs_inference,[],[5784,3918,6,7,45,13,12])). % 119.17/119.18 cnf(5801,plain, % 119.17/119.18 (E(f2(f7(a3),x58011),f2(f7(a1),x58011))), % 119.17/119.18 inference(scs_inference,[],[5784,3918,6,7,45,13,12,10,8,14])). % 119.17/119.18 cnf(5809,plain, % 119.17/119.18 (~P7(x58091,f14(f12(f12(x58092,a1),f12(x58092,a1)),x58093))), % 119.17/119.18 inference(rename_variables,[],[5788])). % 119.17/119.18 cnf(5811,plain, % 119.17/119.18 (E(f2(x58111,f7(a3)),f2(x58111,f7(a1)))), % 119.17/119.18 inference(scs_inference,[],[5103,5788,5784,3918,6,7,45,13,12,10,8,14,11,2,9,5,46,85,4,15])). % 119.17/119.18 cnf(5815,plain, % 119.17/119.18 (P1(f14(f12(f12(x58151,a1),f12(x58151,a1)),x58152))), % 119.17/119.18 inference(scs_inference,[],[5172,5103,5788,5809,5784,3747,3918,2248,6,7,45,13,12,10,8,14,11,2,9,5,46,85,4,15,3,53])). % 119.17/119.18 cnf(5819,plain, % 119.17/119.18 (~E(a9,f15(f15(a9,x58191),f16(a1)))), % 119.17/119.18 inference(scs_inference,[],[27,5172,5103,5788,5809,5784,3747,3918,5484,2248,6,7,45,13,12,10,8,14,11,2,9,5,46,85,4,15,3,53,16])). % 119.17/119.18 cnf(5820,plain, % 119.17/119.18 (~P7(x58201,f12(f2(f14(a1,x58202),a3),a9))), % 119.17/119.18 inference(scs_inference,[],[27,5172,5103,5788,5809,5784,5658,3747,3918,5519,5484,2248,6,7,45,13,12,10,8,14,11,2,9,5,46,85,4,15,3,53,16,18])). % 119.17/119.18 cnf(5822,plain, % 119.17/119.18 (P3(f6(f15(f16(a3),f15(a3,x58221))),f15(f15(a1,x58221),f16(a1)))), % 119.17/119.18 inference(scs_inference,[],[27,5172,5103,5763,5788,5809,5784,5638,5658,3747,3918,5519,5484,2248,6,7,45,13,12,10,8,14,11,2,9,5,46,85,4,15,3,53,16,18,23])). % 119.17/119.18 cnf(5832,plain, % 119.17/119.18 (E(f15(f15(x58321,f12(a3,a3)),x58322),f15(f15(x58321,a1),x58322))), % 119.17/119.18 inference(scs_inference,[],[3821,6])). % 119.17/119.18 cnf(5833,plain, % 119.17/119.18 (E(f15(x58331,f15(x58332,f12(a3,a3))),f15(x58331,f15(x58332,a1)))), % 119.17/119.18 inference(scs_inference,[],[3821,6,7])). % 119.17/119.18 cnf(5858,plain, % 119.17/119.18 (~E(a9,f15(f15(a1,x58581),f16(a3)))), % 119.17/119.18 inference(scs_inference,[],[27,5819,5793,5794,5815,5820,5822,3821,5636,44,6,7,45,13,10,12,8,14,11,2,5,9,46,85,15,4,3,53,16])). % 119.17/119.18 cnf(5859,plain, % 119.17/119.18 (P7(f6(f15(f15(a3,x58591),f16(a3))),f15(f16(a1),f15(a3,x58591)))), % 119.17/119.18 inference(scs_inference,[],[27,5819,5793,5794,5815,5820,5822,5762,3821,3479,5636,44,6,7,45,13,10,12,8,14,11,2,5,9,46,85,15,4,3,53,16,18])). % 119.17/119.18 cnf(5862,plain, % 119.17/119.18 (~P1(f15(f16(a1),f15(a3,x58621)))), % 119.17/119.18 inference(scs_inference,[],[27,5819,5793,5794,5815,5820,5822,5762,3821,3479,5636,44,6,7,45,13,10,12,8,14,11,2,5,9,46,85,15,4,3,53,16,18,50])). % 119.17/119.18 cnf(5868,plain, % 119.17/119.18 (~P7(f15(f15(a3,x58681),f16(a3)),f6(f15(f16(a3),f15(a1,x58681))))), % 119.17/119.18 inference(scs_inference,[],[27,5819,5793,5794,5815,5820,5822,5712,5762,3821,5575,3479,5636,44,6,7,45,13,10,12,8,14,11,2,5,9,46,85,15,4,3,53,16,18,50,51,54,17])). % 119.17/119.18 cnf(5878,plain, % 119.17/119.18 (E(f14(f14(f12(a3,a3),x58781),x58782),f14(f14(a1,x58781),x58782))), % 119.17/119.18 inference(scs_inference,[],[3822,6,7,13,12])). % 119.17/119.18 cnf(5883,plain, % 119.17/119.18 (~E(f15(f15(a1,x58831),f16(a3)),a9)), % 119.17/119.18 inference(scs_inference,[],[5858,3822,6,7,13,12,10,8,14,11,2])). % 119.17/119.18 cnf(5890,plain, % 119.17/119.18 (~P7(f15(f16(a1),f15(a3,x58901)),f6(f15(f15(a3,x58901),f16(a3))))), % 119.17/119.18 inference(scs_inference,[],[5858,5859,3822,5034,6,7,13,12,10,8,14,11,2,5,9,85,15,4,54])). % 119.17/119.18 cnf(5895,plain, % 119.17/119.18 (~E(f12(a11,a11),f12(f14(a1,x58951),f2(a1,a3)))), % 119.17/119.18 inference(scs_inference,[],[5772,5858,5832,5859,5640,3822,5034,62,6,7,13,12,10,8,14,11,2,5,9,85,15,4,54,17,3])). % 119.17/119.18 cnf(5897,plain, % 119.17/119.18 (P1(f12(f2(f14(a1,x58971),a3),a9))), % 119.17/119.18 inference(scs_inference,[],[5772,5858,5832,5859,5640,3822,5820,5034,2712,62,6,7,13,12,10,8,14,11,2,5,9,85,15,4,54,17,3,53])). % 119.17/119.18 cnf(5898,plain, % 119.17/119.18 (~P7(x58981,f12(f2(f14(a1,x58982),a3),a9))), % 119.17/119.18 inference(rename_variables,[],[5820])). % 119.17/119.18 cnf(5901,plain, % 119.17/119.18 (~E(a9,f15(f16(a1),f15(a3,x59011)))), % 119.17/119.18 inference(scs_inference,[],[27,5862,5772,5858,5832,5859,5640,3822,5820,5034,2712,62,6,7,13,12,10,8,14,11,2,5,9,85,15,4,54,17,3,53,16])). % 119.17/119.18 cnf(5902,plain, % 119.17/119.18 (~P7(x59021,f12(a9,f2(f14(a1,x59022),a3)))), % 119.17/119.18 inference(scs_inference,[],[27,5862,5772,5858,5832,5859,5640,3822,5820,5898,5034,2712,41,62,6,7,13,12,10,8,14,11,2,5,9,85,15,4,54,17,3,53,16,18])). % 119.17/119.18 cnf(5940,plain, % 119.17/119.18 (P7(f6(f15(f15(a3,f12(a3,a3)),f16(a3))),f15(f16(a1),f15(a3,a1)))), % 119.17/119.18 inference(scs_inference,[],[5895,5797,5798,5902,5897,5833,5868,3824,5862,5832,5859,2566,6,45,7,13,12,10,8,14,11,2,5,9,46,85,15,4,17,3,53,16,18])). % 119.17/119.18 cnf(5965,plain, % 119.17/119.18 (E(f12(x59651,f2(x59652,f12(a3,a3))),f12(x59651,f2(x59652,a1)))), % 119.17/119.18 inference(scs_inference,[],[5901,3827,6,7,13,12,10,8,14,11,2,5])). % 119.17/119.18 cnf(5971,plain, % 119.17/119.18 (E(f12(f2(x59711,f12(a3,a3)),x59712),f12(f2(x59711,a1),x59712))), % 119.17/119.18 inference(scs_inference,[],[5901,5940,3827,5066,6,7,13,12,10,8,14,11,2,5,9,51,85,4])). % 119.17/119.18 cnf(5977,plain, % 119.17/119.18 (P1(f12(a9,f2(f14(a1,x59771),a3)))), % 119.17/119.18 inference(scs_inference,[],[5901,5890,5940,3827,5902,5162,5066,2264,6,7,13,12,10,8,14,11,2,5,9,51,85,4,15,54,17,53])). % 119.17/119.18 cnf(5981,plain, % 119.17/119.18 (~E(f15(f15(a1,x59811),f16(a1)),a9)), % 119.17/119.18 inference(scs_inference,[],[5883,5901,5890,5940,3827,5763,5902,5162,5066,2264,6,7,13,12,10,8,14,11,2,5,9,51,85,4,15,54,17,53,3])). % 119.17/119.18 cnf(5984,plain, % 119.17/119.18 (~P7(x59841,f12(f2(a9,a3),f12(f12(a1,a1),f12(a1,a9))))), % 119.17/119.18 inference(scs_inference,[],[27,5883,5901,5890,5940,3827,5763,5902,5162,5658,5211,5066,2264,42,6,7,13,12,10,8,14,11,2,5,9,51,85,4,15,54,17,53,3,16,18])). % 119.17/119.18 cnf(5993,plain, % 119.17/119.18 (E(f15(f15(f12(a3,a3),x59931),x59932),f15(f15(a1,x59931),x59932))), % 119.17/119.18 inference(scs_inference,[],[3830,6])). % 119.17/119.18 cnf(6009,plain, % 119.17/119.18 (~P7(x60091,f12(f2(a9,a3),f12(f12(a1,a1),f12(a1,a9))))), % 119.17/119.18 inference(rename_variables,[],[5984])). % 119.17/119.18 cnf(6014,plain, % 119.17/119.18 (P1(f12(f2(a9,a3),f12(f12(a1,a1),f12(a1,a9))))), % 119.17/119.18 inference(scs_inference,[],[5981,5984,6009,5977,4808,3830,5763,2685,6,45,7,13,12,10,8,14,11,2,5,46,9,85,4,15,17,53])). % 119.17/119.18 cnf(6022,plain, % 119.17/119.18 (~P7(x60221,f14(f14(f12(a3,a3),x60222),x60223))), % 119.17/119.18 inference(scs_inference,[],[5981,5801,5811,5984,6009,5977,5878,4808,3830,5763,5862,4197,2685,6,45,7,13,12,10,8,14,11,2,5,46,9,85,4,15,17,53,3,16,18])). % 119.17/119.18 cnf(6044,plain, % 119.17/119.18 (~P7(x60441,f14(f14(f12(a3,a3),x60442),x60443))), % 119.17/119.18 inference(rename_variables,[],[6022])). % 119.17/119.18 cnf(6047,plain, % 119.17/119.18 (P1(f14(f14(f12(a3,a3),x60471),x60472))), % 119.17/119.18 inference(scs_inference,[],[4503,6022,6044,6014,3832,2240,6,45,7,12,13,10,8,14,11,2,46,5,9,85,4,15,53])). % 119.17/119.18 cnf(6055,plain, % 119.17/119.18 (~P7(x60551,f12(f12(f12(a1,a1),f12(a1,a9)),f2(a9,a3)))), % 119.17/119.18 inference(scs_inference,[],[27,5245,4503,6022,6044,6014,5965,3832,5984,2240,70,41,6,45,7,12,13,10,8,14,11,2,46,5,9,85,4,15,53,3,16,18])). % 119.17/119.18 cnf(6080,plain, % 119.17/119.18 (~P7(x60801,f12(f12(f12(a1,a1),f12(a1,a9)),f2(a9,a3)))), % 119.17/119.18 inference(rename_variables,[],[6055])). % 119.17/119.18 cnf(6083,plain, % 119.17/119.18 (P1(f12(f12(f12(a1,a1),f12(a1,a9)),f2(a9,a3)))), % 119.17/119.18 inference(scs_inference,[],[6055,6080,4726,6047,3823,213,6,45,7,12,13,10,8,14,11,2,46,5,9,85,4,15,53])). % 119.17/119.18 cnf(6091,plain, % 119.17/119.18 (~P7(x60911,f12(f2(f14(a1,x60912),f12(a3,a3)),f12(f12(a1,a1),f12(a1,a9))))), % 119.17/119.18 inference(scs_inference,[],[6055,6080,4726,5604,5614,6047,5971,3823,4768,5484,213,6,45,7,12,13,10,8,14,11,2,46,5,9,85,4,15,53,3,16,18])). % 119.17/119.18 cnf(6099,plain, % 119.17/119.18 (E(f12(f12(f12(a1,a1),f12(a1,a9)),f2(a9,a3)),a1)), % 119.17/119.18 inference(scs_inference,[],[6083,45])). % 119.17/119.18 cnf(6115,plain, % 119.17/119.18 (~P7(x61151,f12(f2(f14(a1,x61152),f12(a3,a3)),f12(f12(a1,a1),f12(a1,a9))))), % 119.17/119.18 inference(rename_variables,[],[6091])). % 119.17/119.18 cnf(6118,plain, % 119.17/119.18 (P1(f12(f2(f14(a1,x61181),f12(a3,a3)),f12(f12(a1,a1),f12(a1,a9))))), % 119.17/119.18 inference(scs_inference,[],[6083,4404,6091,6115,3825,2716,45,6,7,12,13,10,8,14,11,2,46,5,9,85,4,15,53])). % 119.17/119.18 cnf(6138,plain, % 119.17/119.18 (E(f6(f12(f12(f12(a1,a1),f12(a1,a9)),f2(a9,a3))),f6(a1))), % 119.17/119.18 inference(scs_inference,[],[6099,6118,45,6,7,12,13,10,8])). % 119.17/119.18 cnf(6560,plain, % 119.17/119.18 (E(a1,f12(f12(f12(a1,a1),f12(a1,a9)),f2(a9,a3)))), % 119.17/119.18 inference(scs_inference,[],[6099,2])). % 119.17/119.18 cnf(6562,plain, % 119.17/119.18 (~E(f14(a1,x65621),f14(a5,a13))), % 119.17/119.18 inference(rename_variables,[],[4655])). % 119.17/119.18 cnf(6569,plain, % 119.17/119.18 (E(x65691,f12(x65691,x65691))), % 119.17/119.18 inference(rename_variables,[],[62])). % 119.17/119.18 cnf(6571,plain, % 119.17/119.18 (E(x65711,f12(x65711,x65711))), % 119.17/119.18 inference(rename_variables,[],[62])). % 119.17/119.18 cnf(6576,plain, % 119.17/119.18 (E(x65761,f12(x65761,x65761))), % 119.17/119.18 inference(rename_variables,[],[62])). % 119.17/119.18 cnf(6578,plain, % 119.17/119.18 (E(x65781,f12(x65781,x65781))), % 119.17/119.18 inference(rename_variables,[],[62])). % 119.17/119.18 cnf(6579,plain, % 119.17/119.18 (P7(f12(f6(f12(a11,a11)),f6(f12(a11,a11))),a11)), % 119.17/119.18 inference(scs_inference,[],[1976,62,6569,6571,6576,6578,217,43,6099,4036,3458,4345,2248,42,4655,4200,5000,2,12,45,87,21,3,23,53,22,20,17])). % 119.17/119.18 cnf(6580,plain, % 119.17/119.18 (E(x65801,f12(x65801,x65801))), % 119.17/119.18 inference(rename_variables,[],[62])). % 119.17/119.18 cnf(6581,plain, % 119.17/119.18 (P5(f12(f12(f12(a1,x65811),f12(a1,x65811)),f12(a1,x65812)))), % 119.17/119.18 inference(scs_inference,[],[1976,62,6569,6571,6576,6578,217,43,6099,4036,3458,4345,2248,42,4146,3461,4655,4200,5000,2,12,45,87,21,3,23,53,22,20,17,19])). % 119.17/119.18 cnf(6582,plain, % 119.17/119.18 (E(f12(f12(a1,x65821),x65822),f12(f12(f12(a1,x65823),f12(a1,x65823)),x65822))), % 119.17/119.18 inference(rename_variables,[],[3461])). % 119.17/119.18 cnf(6590,plain, % 119.17/119.18 (~P1(f14(a5,a13))), % 119.17/119.18 inference(scs_inference,[],[1976,62,6569,6571,6576,6578,6580,217,43,6099,4036,3458,4345,2248,44,42,92,4205,4146,4449,3461,6582,4655,6562,4200,4154,5000,2,12,45,87,21,3,23,53,22,20,17,19,18,16,24,47])). % 119.17/119.18 cnf(6599,plain, % 119.17/119.18 (E(a1,f12(f12(x65991,a1),f12(x65991,a1)))), % 119.17/119.18 inference(scs_inference,[],[5562,2])). % 119.17/119.18 cnf(6609,plain, % 119.17/119.18 (P7(f12(f6(f15(f16(x66091),f15(x66091,x66092))),f6(f15(f16(x66091),f15(x66091,x66092)))),f15(f16(x66091),f15(x66091,x66092)))), % 119.17/119.18 inference(scs_inference,[],[62,5562,3825,111,4673,3892,6579,2,12,87,45,54,5,17])). % 119.17/119.18 cnf(6610,plain, % 119.17/119.18 (E(x66101,f12(x66101,x66101))), % 119.17/119.18 inference(rename_variables,[],[62])). % 119.17/119.18 cnf(6612,plain, % 119.17/119.18 (E(x66121,f12(x66121,x66121))), % 119.17/119.18 inference(rename_variables,[],[62])). % 119.17/119.18 cnf(6614,plain, % 119.17/119.18 (E(x66141,f12(x66141,x66141))), % 119.17/119.18 inference(rename_variables,[],[62])). % 119.17/119.18 cnf(6645,plain, % 119.17/119.18 (~P7(f15(f15(f7(f14(a5,a13)),f8(f14(a5,a13))),f16(f7(f14(a5,a13)))),f14(a5,x66451))), % 119.17/119.18 inference(scs_inference,[],[36,62,6610,6612,6614,38,34,463,5562,3458,3825,4345,2248,44,111,184,4146,4197,4431,3604,4108,4159,4140,3871,4182,4633,3469,4673,4165,3892,6560,6579,3696,6590,6581,4067,2,12,87,45,54,5,17,23,18,3,19,21,16,22,20,24,59,53,47,60,61,3562])). % 119.17/119.18 cnf(6663,plain, % 119.17/119.18 (E(x66631,f12(x66631,x66631))), % 119.17/119.18 inference(rename_variables,[],[62])). % 119.17/119.18 cnf(6669,plain, % 119.17/119.18 (E(x66691,f12(x66691,x66691))), % 119.17/119.18 inference(rename_variables,[],[62])). % 119.17/119.18 cnf(6671,plain, % 119.17/119.18 (E(x66711,f12(x66711,x66711))), % 119.17/119.18 inference(rename_variables,[],[62])). % 119.17/119.18 cnf(6685,plain, % 119.17/119.18 (P2(f14(f12(a1,x66851),x66852))), % 119.17/119.18 inference(scs_inference,[],[62,6663,6669,6671,38,6099,3458,2248,44,3541,70,2685,141,4146,4087,4431,4182,5965,5993,5436,5940,3460,4154,3696,5000,4839,4067,6599,2,12,87,54,19,17,16,21,18,22,23,3,20,24,53,60])). % 119.17/119.18 cnf(6706,plain, % 119.17/119.18 (E(x67061,f12(x67061,x67061))), % 119.17/119.18 inference(rename_variables,[],[62])). % 119.17/119.18 cnf(6715,plain, % 119.17/119.18 (E(x67151,f12(x67151,x67151))), % 119.17/119.18 inference(rename_variables,[],[62])). % 119.17/119.18 cnf(6717,plain, % 119.17/119.18 (E(x67171,f12(x67171,x67171))), % 119.17/119.18 inference(rename_variables,[],[62])). % 119.17/119.18 cnf(6728,plain, % 119.17/119.18 ($false), % 119.17/119.18 inference(scs_inference,[],[62,6706,6715,6717,38,3458,43,2248,4983,70,143,2712,3446,5940,3460,4154,4064,1002,5762,3673,5859,3454,6138,6560,2693,4874,6609,6685,6645,2,12,87,54,19,17,3,21,16,22,23,20,18,24,53,60]), % 119.17/119.18 ['proof']). % 119.17/119.18 % SZS output end Proof % 119.17/119.18 % Total time :118.460000s %------------------------------------------------------------------------------