%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU323+1 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n017.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:27 EDT 2024 % Result : Theorem 117.21s 117.29s % Output : CNFRefutation 117.32s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU323+1 : TPTP v8.2.0. Released v3.3.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n017.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Jun 21 17:54:24 EDT 2024 % 0.12/0.34 % CPUTime : % 0.46/0.58 start to proof:theBenchmark % 117.21/117.27 %------------------------------------------- % 117.21/117.27 % File :CSE---1.7 % 117.21/117.27 % Problem :theBenchmark % 117.21/117.27 % Transform :cnf % 117.21/117.27 % Format :tptp:raw % 117.21/117.27 % Command :java -jar mcs_scs.jar %d %s % 117.21/117.27 % 117.21/117.27 % Result :Theorem 116.650000s % 117.21/117.27 % Output :CNFRefutation 116.650000s % 117.21/117.27 %------------------------------------------- % 117.21/117.29 %------------------------------------------------------------------------------ % 117.21/117.29 % File : SEU323+1 : TPTP v8.2.0. Released v3.3.0. % 117.21/117.29 % Domain : Set theory % 117.21/117.29 % Problem : MPTP bushy problem t51_tops_1 % 117.21/117.29 % Version : [Urb07] axioms : Especial. % 117.21/117.29 % English : % 117.21/117.29 % 117.21/117.29 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 117.21/117.29 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 117.21/117.29 % Source : [Urb07] % 117.21/117.29 % Names : bushy-t51_tops_1 [Urb07] % 117.21/117.29 % 117.21/117.29 % Status : Theorem % 117.21/117.29 % Rating : 0.11 v8.1.0, 0.14 v7.5.0, 0.16 v7.4.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.08 v6.2.0, 0.12 v6.1.0, 0.17 v6.0.0, 0.09 v5.5.0, 0.11 v5.4.0, 0.21 v5.3.0, 0.22 v5.2.0, 0.05 v5.0.0, 0.08 v4.1.0, 0.13 v4.0.0, 0.17 v3.7.0, 0.15 v3.5.0, 0.11 v3.4.0, 0.16 v3.3.0 % 117.21/117.29 % Syntax : Number of formulae : 21 ( 8 unt; 0 def) % 117.21/117.29 % Number of atoms : 51 ( 2 equ) % 117.21/117.29 % Maximal formula atoms : 5 ( 2 avg) % 117.21/117.29 % Number of connectives : 30 ( 0 ~; 0 |; 15 &) % 117.21/117.29 % ( 1 <=>; 14 =>; 0 <=; 0 <~>) % 117.21/117.29 % Maximal formula depth : 7 ( 4 avg) % 117.21/117.29 % Maximal term depth : 5 ( 1 avg) % 117.21/117.29 % Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty) % 117.21/117.29 % Number of functors : 5 ( 5 usr; 0 con; 1-2 aty) % 117.21/117.29 % Number of variables : 31 ( 26 !; 5 ?) % 117.21/117.29 % SPC : FOF_THM_RFO_SEQ % 117.21/117.29 % 117.21/117.29 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 117.21/117.29 % library, www.mizar.org % 117.21/117.29 %------------------------------------------------------------------------------ % 117.21/117.29 fof(fc3_tops_1,axiom, % 117.21/117.29 ! [A,B] : % 117.21/117.29 ( ( topological_space(A) % 117.21/117.29 & top_str(A) % 117.21/117.29 & closed_subset(B,A) % 117.21/117.29 & element(B,powerset(the_carrier(A))) ) % 117.21/117.29 => open_subset(subset_complement(the_carrier(A),B),A) ) ). % 117.21/117.29 % 117.21/117.29 fof(rc6_pre_topc,axiom, % 117.21/117.29 ! [A] : % 117.21/117.29 ( ( topological_space(A) % 117.21/117.29 & top_str(A) ) % 117.21/117.29 => ? [B] : % 117.21/117.29 ( element(B,powerset(the_carrier(A))) % 117.21/117.29 & closed_subset(B,A) ) ) ). % 117.21/117.29 % 117.21/117.29 fof(involutiveness_k3_subset_1,axiom, % 117.21/117.29 ! [A,B] : % 117.21/117.29 ( element(B,powerset(A)) % 117.21/117.29 => subset_complement(A,subset_complement(A,B)) = B ) ). % 117.21/117.29 % 117.21/117.29 fof(reflexivity_r1_tarski,axiom, % 117.21/117.29 ! [A,B] : subset(A,A) ). % 117.21/117.29 % 117.21/117.29 fof(existence_l1_struct_0,axiom, % 117.21/117.29 ? [A] : one_sorted_str(A) ). % 117.21/117.29 % 117.21/117.29 fof(dt_k3_subset_1,axiom, % 117.21/117.29 ! [A,B] : % 117.21/117.29 ( element(B,powerset(A)) % 117.21/117.29 => element(subset_complement(A,B),powerset(A)) ) ). % 117.21/117.29 % 117.21/117.29 fof(dt_k6_pre_topc,axiom, % 117.21/117.29 ! [A,B] : % 117.21/117.29 ( ( top_str(A) % 117.21/117.29 & element(B,powerset(the_carrier(A))) ) % 117.21/117.29 => element(topstr_closure(A,B),powerset(the_carrier(A))) ) ). % 117.21/117.29 % 117.21/117.29 fof(dt_l1_struct_0,axiom, % 117.21/117.29 $true ). % 117.21/117.29 % 117.21/117.29 fof(fc2_tops_1,axiom, % 117.21/117.29 ! [A,B] : % 117.21/117.29 ( ( topological_space(A) % 117.21/117.29 & top_str(A) % 117.21/117.29 & element(B,powerset(the_carrier(A))) ) % 117.21/117.29 => closed_subset(topstr_closure(A,B),A) ) ). % 117.21/117.29 % 117.21/117.29 fof(fc4_tops_1,axiom, % 117.21/117.29 ! [A,B] : % 117.21/117.29 ( ( topological_space(A) % 117.21/117.29 & top_str(A) % 117.21/117.29 & open_subset(B,A) % 117.21/117.29 & element(B,powerset(the_carrier(A))) ) % 117.21/117.29 => closed_subset(subset_complement(the_carrier(A),B),A) ) ). % 117.21/117.29 % 117.21/117.29 fof(existence_l1_pre_topc,axiom, % 117.21/117.29 ? [A] : top_str(A) ). % 117.21/117.29 % 117.21/117.29 fof(existence_m1_subset_1,axiom, % 117.21/117.29 ! [A] : % 117.21/117.29 ? [B] : element(B,A) ). % 117.21/117.29 % 117.21/117.29 fof(dt_k1_tops_1,axiom, % 117.21/117.29 ! [A,B] : % 117.21/117.29 ( ( top_str(A) % 117.21/117.29 & element(B,powerset(the_carrier(A))) ) % 117.21/117.29 => element(interior(A,B),powerset(the_carrier(A))) ) ). % 117.21/117.29 % 117.21/117.29 fof(dt_k1_zfmisc_1,axiom, % 117.21/117.29 $true ). % 117.21/117.29 % 117.21/117.29 fof(dt_l1_pre_topc,axiom, % 117.21/117.29 ! [A] : % 117.21/117.29 ( top_str(A) % 117.21/117.29 => one_sorted_str(A) ) ). % 117.21/117.29 % 117.21/117.29 fof(dt_m1_subset_1,axiom, % 117.21/117.29 $true ). % 117.21/117.29 % 117.21/117.29 fof(dt_u1_struct_0,axiom, % 117.21/117.29 $true ). % 117.21/117.29 % 117.21/117.29 fof(rc1_tops_1,axiom, % 117.21/117.29 ! [A] : % 117.21/117.29 ( ( topological_space(A) % 117.21/117.29 & top_str(A) ) % 117.21/117.29 => ? [B] : % 117.21/117.29 ( element(B,powerset(the_carrier(A))) % 117.21/117.29 & open_subset(B,A) ) ) ). % 117.21/117.29 % 117.21/117.29 fof(t3_subset,axiom, % 117.21/117.29 ! [A,B] : % 117.21/117.29 ( element(A,powerset(B)) % 117.21/117.29 <=> subset(A,B) ) ). % 117.21/117.29 % 117.21/117.29 fof(d1_tops_1,axiom, % 117.21/117.29 ! [A] : % 117.21/117.29 ( top_str(A) % 117.21/117.29 => ! [B] : % 117.21/117.29 ( element(B,powerset(the_carrier(A))) % 117.21/117.29 => interior(A,B) = subset_complement(the_carrier(A),topstr_closure(A,subset_complement(the_carrier(A),B))) ) ) ). % 117.21/117.29 % 117.21/117.29 fof(t51_tops_1,conjecture, % 117.21/117.29 ! [A] : % 117.21/117.29 ( ( topological_space(A) % 117.21/117.29 & top_str(A) ) % 117.21/117.29 => ! [B] : % 117.21/117.29 ( element(B,powerset(the_carrier(A))) % 117.21/117.29 => open_subset(interior(A,B),A) ) ) ). % 117.21/117.29 % 117.21/117.29 %------------------------------------------------------------------------------ % 117.21/117.29 %------------------------------------------- % 117.21/117.29 % Proof found % 117.21/117.29 % SZS status Theorem for theBenchmark % 117.21/117.29 % SZS output start Proof % 117.21/117.30 %ClaNum:48(EqnAxiom:25) % 117.21/117.30 %VarNum:87(SingletonVarNum:27) % 117.21/117.30 %MaxLitNum:5 % 117.21/117.30 %MaxfuncDepth:4 % 117.21/117.30 %SharedTerms:13 % 117.21/117.30 %goalClause: 26 28 32 33 % 117.21/117.30 %singleGoalClaCount:4 % 117.21/117.30 [26]P1(a1) % 117.21/117.30 [27]P2(a2) % 117.21/117.30 [28]P2(a1) % 117.21/117.30 [29]P3(a3) % 117.21/117.30 [33]~P7(f10(a1,a7),a1) % 117.21/117.30 [32]P4(a7,f9(f8(a1))) % 117.21/117.30 [30]P6(x301,x301) % 117.21/117.30 [31]P4(f5(x311),x311) % 117.21/117.30 [34]~P2(x341)+P3(x341) % 117.21/117.30 [37]~P6(x371,x372)+P4(x371,f9(x372)) % 117.21/117.30 [38]P6(x381,x382)+~P4(x381,f9(x382)) % 117.21/117.30 [42]~P4(x422,f9(x421))+P4(f11(x421,x422),f9(x421)) % 117.21/117.30 [41]~P4(x412,f9(x411))+E(f11(x411,f11(x411,x412)),x412) % 117.21/117.30 [35]~P1(x351)+~P2(x351)+P5(f4(x351),x351) % 117.21/117.30 [36]~P1(x361)+~P2(x361)+P7(f6(x361),x361) % 117.21/117.30 [39]~P1(x391)+~P2(x391)+P4(f4(x391),f9(f8(x391))) % 117.21/117.30 [40]~P1(x401)+~P2(x401)+P4(f6(x401),f9(f8(x401))) % 117.21/117.30 [44]~P2(x441)+~P4(x442,f9(f8(x441)))+P4(f12(x441,x442),f9(f8(x441))) % 117.21/117.30 [45]~P2(x451)+~P4(x452,f9(f8(x451)))+P4(f10(x451,x452),f9(f8(x451))) % 117.21/117.30 [48]~P2(x481)+~P4(x482,f9(f8(x481)))+E(f11(f8(x481),f12(x481,f11(f8(x481),x482))),f10(x481,x482)) % 117.21/117.30 [43]~P1(x431)+~P2(x431)+P5(f12(x431,x432),x431)+~P4(x432,f9(f8(x431))) % 117.21/117.30 [46]~P1(x461)+~P2(x461)+~P7(x462,x461)+~P4(x462,f9(f8(x461)))+P5(f11(f8(x461),x462),x461) % 117.21/117.30 [47]~P1(x471)+~P2(x471)+~P5(x472,x471)+~P4(x472,f9(f8(x471)))+P7(f11(f8(x471),x472),x471) % 117.21/117.30 %EqnAxiom % 117.21/117.30 [1]E(x11,x11) % 117.21/117.30 [2]E(x22,x21)+~E(x21,x22) % 117.21/117.30 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 117.21/117.30 [4]~E(x41,x42)+E(f5(x41),f5(x42)) % 117.21/117.30 [5]~E(x51,x52)+E(f8(x51),f8(x52)) % 117.21/117.30 [6]~E(x61,x62)+E(f9(x61),f9(x62)) % 117.21/117.30 [7]~E(x71,x72)+E(f10(x71,x73),f10(x72,x73)) % 117.21/117.30 [8]~E(x81,x82)+E(f10(x83,x81),f10(x83,x82)) % 117.21/117.30 [9]~E(x91,x92)+E(f4(x91),f4(x92)) % 117.21/117.30 [10]~E(x101,x102)+E(f6(x101),f6(x102)) % 117.21/117.30 [11]~E(x111,x112)+E(f11(x111,x113),f11(x112,x113)) % 117.21/117.30 [12]~E(x121,x122)+E(f11(x123,x121),f11(x123,x122)) % 117.21/117.30 [13]~E(x131,x132)+E(f12(x131,x133),f12(x132,x133)) % 117.21/117.30 [14]~E(x141,x142)+E(f12(x143,x141),f12(x143,x142)) % 117.21/117.30 [15]~P1(x151)+P1(x152)+~E(x151,x152) % 117.21/117.30 [16]~P2(x161)+P2(x162)+~E(x161,x162) % 117.21/117.30 [17]P4(x172,x173)+~E(x171,x172)+~P4(x171,x173) % 117.21/117.30 [18]P4(x183,x182)+~E(x181,x182)+~P4(x183,x181) % 117.21/117.30 [19]~P3(x191)+P3(x192)+~E(x191,x192) % 117.21/117.30 [20]P6(x202,x203)+~E(x201,x202)+~P6(x201,x203) % 117.21/117.30 [21]P6(x213,x212)+~E(x211,x212)+~P6(x213,x211) % 117.21/117.30 [22]P5(x222,x223)+~E(x221,x222)+~P5(x221,x223) % 117.21/117.30 [23]P5(x233,x232)+~E(x231,x232)+~P5(x233,x231) % 117.21/117.30 [24]P7(x242,x243)+~E(x241,x242)+~P7(x241,x243) % 117.21/117.30 [25]P7(x253,x252)+~E(x251,x252)+~P7(x253,x251) % 117.21/117.30 % 117.21/117.30 %------------------------------------------- % 117.32/117.31 cnf(49,plain, % 117.32/117.31 (P6(a7,f8(a1))), % 117.32/117.31 inference(scs_inference,[],[32,38])). % 117.32/117.31 cnf(51,plain, % 117.32/117.31 (P5(f12(a1,a7),a1)), % 117.32/117.31 inference(scs_inference,[],[26,28,32,38,43])). % 117.32/117.31 cnf(53,plain, % 117.32/117.32 (P4(x531,f9(f8(a1)))+~E(a7,x531)), % 117.32/117.32 inference(scs_inference,[],[26,28,32,38,43,17])). % 117.32/117.32 cnf(59,plain, % 117.32/117.32 (P6(f5(f9(x591)),x591)), % 117.32/117.32 inference(scs_inference,[],[31,38])). % 117.32/117.32 cnf(60,plain, % 117.32/117.32 (P4(f5(x601),x601)), % 117.32/117.32 inference(rename_variables,[],[31])). % 117.32/117.32 cnf(62,plain, % 117.32/117.32 (P5(f12(a1,f5(f9(f8(a1)))),a1)), % 117.32/117.32 inference(scs_inference,[],[26,28,31,60,38,43])). % 117.32/117.32 cnf(63,plain, % 117.32/117.32 (P4(f5(x631),x631)), % 117.32/117.32 inference(rename_variables,[],[31])). % 117.32/117.32 cnf(65,plain, % 117.32/117.32 (P6(a7,x651)+~E(f8(a1),x651)), % 117.32/117.32 inference(scs_inference,[],[26,28,49,31,60,38,43,21])). % 117.32/117.32 cnf(67,plain, % 117.32/117.32 (P5(x671,a1)+~E(f12(a1,a7),x671)), % 117.32/117.32 inference(scs_inference,[],[26,28,32,49,51,31,60,38,43,21,18,22])). % 117.32/117.32 cnf(69,plain, % 117.32/117.32 (P6(x691,f8(a1))+~E(a7,x691)), % 117.32/117.32 inference(scs_inference,[],[26,28,32,49,51,31,60,38,43,21,18,22,23,20])). % 117.32/117.32 cnf(70,plain, % 117.32/117.32 (P4(x701,x702)+~E(f5(x702),x701)), % 117.32/117.32 inference(scs_inference,[],[26,28,32,49,51,31,60,63,38,43,21,18,22,23,20,17])). % 117.32/117.32 cnf(77,plain, % 117.32/117.32 (P6(f5(f9(x771)),x772)+~E(x771,x772)), % 117.32/117.32 inference(scs_inference,[],[59,21])). % 117.32/117.32 cnf(78,plain, % 117.32/117.32 (P5(x781,a1)+~E(f12(a1,f5(f9(f8(a1)))),x781)), % 117.32/117.32 inference(scs_inference,[],[59,62,21,22])). % 117.32/117.32 cnf(80,plain, % 117.32/117.32 (P6(x801,x802)+~E(f5(f9(x802)),x801)), % 117.32/117.32 inference(scs_inference,[],[59,62,21,22,23,20])). % 117.32/117.32 cnf(81,plain, % 117.32/117.32 (P4(f5(x811),x812)+~E(x811,x812)), % 117.32/117.32 inference(scs_inference,[],[59,62,31,21,22,23,20,18])). % 117.32/117.32 cnf(92,plain, % 117.32/117.32 (P6(x921,x922)+~E(x921,x922)), % 117.32/117.32 inference(scs_inference,[],[30,21])). % 117.32/117.32 cnf(93,plain, % 117.32/117.32 (P6(x931,x932)+~E(x932,x931)), % 117.32/117.32 inference(scs_inference,[],[30,21,20])). % 117.32/117.32 cnf(94,plain, % 117.32/117.32 (~P7(f5(f9(f8(a1))),a1)+P5(f11(f8(a1),f5(f9(f8(a1)))),a1)), % 117.32/117.32 inference(scs_inference,[],[26,28,31,30,21,20,46])). % 117.32/117.32 cnf(108,plain, % 117.32/117.32 (E(a7,f11(f8(a1),f11(f8(a1),a7)))), % 117.32/117.32 inference(scs_inference,[],[32,2,41])). % 117.32/117.32 cnf(111,plain, % 117.32/117.32 (E(f11(f8(a1),f11(f8(a1),a7)),a7)), % 117.32/117.32 inference(scs_inference,[],[108,53,81,2])). % 117.32/117.32 cnf(123,plain, % 117.32/117.32 (P5(x1231,a1)+~E(f12(a1,f11(f8(a1),f11(f8(a1),a7))),x1231)), % 117.32/117.32 inference(scs_inference,[],[26,28,108,53,81,2,69,77,92,93,43,15,16,19,21,17,22])). % 117.32/117.32 cnf(327,plain, % 117.32/117.32 (E(f12(x3271,f11(f8(a1),f11(f8(a1),a7))),f12(x3271,a7))), % 117.32/117.32 inference(scs_inference,[],[108,14,2])). % 117.32/117.32 cnf(328,plain, % 117.32/117.32 (E(f12(x3281,a7),f12(x3281,f11(f8(a1),f11(f8(a1),a7))))), % 117.32/117.32 inference(scs_inference,[],[327,2])). % 117.32/117.32 cnf(329,plain, % 117.32/117.32 (P6(f12(x3291,f11(f8(a1),f11(f8(a1),a7))),f12(x3291,a7))), % 117.32/117.32 inference(scs_inference,[],[327,2,92])). % 117.32/117.32 cnf(391,plain, % 117.32/117.32 (P6(f11(f8(a1),a7),f8(a1))), % 117.32/117.32 inference(scs_inference,[],[32,42,38])). % 117.32/117.32 cnf(393,plain, % 117.32/117.32 (P6(x3931,f8(a1))+~E(f11(f8(a1),a7),x3931)), % 117.32/117.32 inference(scs_inference,[],[391,21,20])). % 117.32/117.32 cnf(529,plain, % 117.32/117.32 (~P7(x5291,a1)+~E(x5291,f5(f9(f8(a1))))+P5(f11(f8(a1),f5(f9(f8(a1)))),a1)), % 117.32/117.32 inference(scs_inference,[],[94,24])). % 117.32/117.32 cnf(885,plain, % 117.32/117.32 (P5(f4(a1),a1)), % 117.32/117.32 inference(scs_inference,[],[26,28,35,16])). % 117.32/117.32 cnf(887,plain, % 117.32/117.32 (P5(x8871,a1)+~E(f4(a1),x8871)), % 117.32/117.32 inference(scs_inference,[],[885,23,22])). % 117.32/117.32 cnf(896,plain, % 117.32/117.32 (P7(f6(a1),a1)), % 117.32/117.32 inference(scs_inference,[],[26,28,36,16])). % 117.32/117.32 cnf(897,plain, % 117.32/117.32 (~E(f6(a1),f10(a1,a7))), % 117.32/117.32 inference(scs_inference,[],[33,896,24])). % 117.32/117.32 cnf(903,plain, % 117.32/117.32 (P4(f4(a1),f9(f8(a1)))), % 117.32/117.32 inference(scs_inference,[],[26,28,39,16])). % 117.32/117.32 cnf(904,plain, % 117.32/117.32 (P6(f4(a1),f8(a1))), % 117.32/117.32 inference(scs_inference,[],[903,38])). % 117.32/117.32 cnf(906,plain, % 117.32/117.32 (P5(f12(a1,f4(a1)),a1)), % 117.32/117.32 inference(scs_inference,[],[26,28,903,38,43])). % 117.32/117.32 cnf(908,plain, % 117.32/117.32 (P7(f11(f8(a1),f4(a1)),a1)), % 117.32/117.32 inference(scs_inference,[],[26,28,885,903,38,43,47])). % 117.32/117.32 cnf(910,plain, % 117.32/117.32 (P4(x9101,f9(f8(a1)))+~E(f4(a1),x9101)), % 117.32/117.32 inference(scs_inference,[],[26,28,885,903,38,43,47,17])). % 117.32/117.32 cnf(911,plain, % 117.32/117.32 (~E(f11(f8(a1),f4(a1)),f10(a1,a7))), % 117.32/117.32 inference(scs_inference,[],[33,26,28,885,903,38,43,47,17,24])). % 117.32/117.32 cnf(929,plain, % 117.32/117.32 (P5(x9291,a1)+~E(f12(a1,f4(a1)),x9291)), % 117.32/117.32 inference(scs_inference,[],[908,906,904,23,25,21,22])). % 117.32/117.32 cnf(930,plain, % 117.32/117.32 (~E(f12(a1,f4(a1)),a7)+P7(f11(f8(a1),a7),a1)), % 117.32/117.32 inference(scs_inference,[],[32,26,28,908,906,904,23,25,21,22,47])). % 117.32/117.32 cnf(941,plain, % 117.32/117.32 (~E(f11(f8(a1),a7),f10(a1,a7))+~E(f12(a1,f4(a1)),a7)), % 117.32/117.32 inference(scs_inference,[],[33,930,24])). % 117.32/117.32 cnf(943,plain, % 117.32/117.32 (~E(f10(a1,a7),f11(f8(a1),a7))+~E(f12(a1,f4(a1)),a7)), % 117.32/117.32 inference(scs_inference,[],[941,2])). % 117.32/117.32 cnf(944,plain, % 117.32/117.32 (~E(x9441,f11(f8(a1),a7))+~E(f10(a1,a7),x9441)+~E(f12(a1,f4(a1)),a7)), % 117.32/117.32 inference(scs_inference,[],[943,3])). % 117.32/117.32 cnf(946,plain, % 117.32/117.32 (P4(f6(a1),f9(f8(a1)))), % 117.32/117.32 inference(scs_inference,[],[26,28,40,16])). % 117.32/117.32 cnf(947,plain, % 117.32/117.32 (P6(f6(a1),f8(a1))), % 117.32/117.32 inference(scs_inference,[],[946,38])). % 117.32/117.32 cnf(949,plain, % 117.32/117.32 (P5(f12(a1,f6(a1)),a1)), % 117.32/117.32 inference(scs_inference,[],[26,28,946,38,43])). % 117.32/117.32 cnf(951,plain, % 117.32/117.32 (P5(f11(f8(a1),f6(a1)),a1)), % 117.32/117.32 inference(scs_inference,[],[26,28,896,946,38,43,46])). % 117.32/117.32 cnf(954,plain, % 117.32/117.32 (P6(x9541,f8(a1))+~E(f6(a1),x9541)), % 117.32/117.32 inference(scs_inference,[],[26,28,896,946,38,43,46,18,20])). % 117.32/117.32 cnf(955,plain, % 117.32/117.32 (P4(x9551,f9(f8(a1)))+~E(f6(a1),x9551)), % 117.32/117.32 inference(scs_inference,[],[26,28,896,946,38,43,46,18,20,17])). % 117.32/117.32 cnf(958,plain, % 117.32/117.32 (P5(x9581,a1)+~E(f12(a1,f6(a1)),x9581)), % 117.32/117.32 inference(scs_inference,[],[26,28,896,946,38,43,46,18,20,17,23,21,22])). % 117.32/117.32 cnf(969,plain, % 117.32/117.32 (P5(x9691,a1)+~E(f11(f8(a1),f6(a1)),x9691)), % 117.32/117.32 inference(scs_inference,[],[951,23,22])). % 117.32/117.32 cnf(976,plain, % 117.32/117.32 (~P5(f6(a1),a1)+P7(f11(f8(a1),f6(a1)),a1)), % 117.32/117.32 inference(scs_inference,[],[26,28,946,47])). % 117.32/117.32 cnf(978,plain, % 117.32/117.32 (~P5(f6(a1),a1)+~E(f11(f8(a1),f6(a1)),f10(a1,a7))), % 117.32/117.32 inference(scs_inference,[],[33,26,28,391,946,47,529,20,24])). % 117.32/117.32 cnf(981,plain, % 117.32/117.32 (~E(f12(a1,a7),f6(a1))+P7(f11(f8(a1),f6(a1)),a1)), % 117.32/117.32 inference(scs_inference,[],[976,67])). % 117.32/117.32 cnf(982,plain, % 117.32/117.32 (~E(f12(a1,f5(f9(f8(a1)))),f6(a1))+~E(f11(f8(a1),f6(a1)),f10(a1,a7))), % 117.32/117.32 inference(scs_inference,[],[978,78])). % 117.32/117.32 cnf(983,plain, % 117.32/117.32 (~E(f11(f8(a1),f6(a1)),f10(a1,a7))+~E(f12(a1,a7),f6(a1))), % 117.32/117.32 inference(scs_inference,[],[33,981,24])). % 117.32/117.32 cnf(987,plain, % 117.32/117.32 (~E(f10(a1,a7),f11(f8(a1),f6(a1)))+~E(f12(a1,a7),f6(a1))), % 117.32/117.32 inference(scs_inference,[],[983,2])). % 117.32/117.32 cnf(989,plain, % 117.32/117.32 (~E(x9891,f11(f8(a1),f6(a1)))+~E(f10(a1,a7),x9891)+~E(f12(a1,a7),f6(a1))), % 117.32/117.32 inference(scs_inference,[],[987,3])). % 117.32/117.32 cnf(990,plain, % 117.32/117.32 (~E(f10(a1,a7),f11(f8(a1),f6(a1)))+~E(f12(a1,f5(f9(f8(a1)))),f6(a1))), % 117.32/117.32 inference(scs_inference,[],[982,2])). % 117.32/117.32 cnf(991,plain, % 117.32/117.32 (~E(x9911,f11(f8(a1),f6(a1)))+~E(f10(a1,a7),x9911)+~E(f12(a1,f5(f9(f8(a1)))),f6(a1))), % 117.32/117.32 inference(scs_inference,[],[990,3])). % 117.32/117.32 cnf(1355,plain, % 117.32/117.32 (~E(f11(f8(a1),f6(a1)),x13551)+~E(f10(a1,a7),x13551)+~E(f12(a1,f5(f9(f8(a1)))),f6(a1))), % 117.32/117.32 inference(scs_inference,[],[991,2])). % 117.32/117.32 cnf(1731,plain, % 117.32/117.32 (E(f5(f11(f8(a1),f11(f8(a1),a7))),f5(a7))), % 117.32/117.32 inference(scs_inference,[],[108,2,4])). % 117.32/117.32 cnf(1733,plain, % 117.32/117.32 (P6(f5(f11(f8(a1),f11(f8(a1),a7))),f5(a7))), % 117.32/117.32 inference(scs_inference,[],[1731,2,92])). % 117.32/117.32 cnf(1759,plain, % 117.32/117.32 (E(f8(f11(f8(a1),f11(f8(a1),a7))),f8(a7))), % 117.32/117.32 inference(scs_inference,[],[108,2,5])). % 117.32/117.32 cnf(1761,plain, % 117.32/117.32 (P6(f8(f11(f8(a1),f11(f8(a1),a7))),f8(a7))), % 117.32/117.32 inference(scs_inference,[],[1759,2,92])). % 117.32/117.32 cnf(1966,plain, % 117.32/117.32 (E(f9(f11(f8(a1),f11(f8(a1),a7))),f9(a7))), % 117.32/117.32 inference(scs_inference,[],[108,2,6])). % 117.32/117.32 cnf(1968,plain, % 117.32/117.32 (P6(f9(f11(f8(a1),f11(f8(a1),a7))),f9(a7))), % 117.32/117.32 inference(scs_inference,[],[1966,2,92])). % 117.32/117.32 cnf(2144,plain, % 117.32/117.32 (E(f10(a7,x21441),f10(f11(f8(a1),f11(f8(a1),a7)),x21441))), % 117.32/117.32 inference(scs_inference,[],[111,2,7])). % 117.32/117.32 cnf(2146,plain, % 117.32/117.32 (E(f10(f11(f8(a1),f11(f8(a1),a7)),x21461),f10(a7,x21461))), % 117.32/117.32 inference(scs_inference,[],[2144,81,2])). % 117.32/117.32 cnf(2163,plain, % 117.32/117.32 (E(f10(x21631,a7),f10(x21631,f11(f8(a1),f11(f8(a1),a7))))), % 117.32/117.32 inference(scs_inference,[],[111,2,8])). % 117.32/117.32 cnf(2166,plain, % 117.32/117.32 (P6(f10(x21661,f11(f8(a1),f11(f8(a1),a7))),f10(x21661,a7))), % 117.32/117.32 inference(scs_inference,[],[2163,81,2,93])). % 117.32/117.32 cnf(2582,plain, % 117.32/117.32 (E(f4(f11(f8(a1),f11(f8(a1),a7))),f4(a7))), % 117.32/117.32 inference(scs_inference,[],[108,2,9])). % 117.32/117.32 cnf(2583,plain, % 117.32/117.32 (E(f4(a7),f4(f11(f8(a1),f11(f8(a1),a7))))), % 117.32/117.32 inference(scs_inference,[],[2582,2])). % 117.32/117.32 cnf(2637,plain, % 117.32/117.32 (E(f10(a1,a7),f11(f8(a1),f12(a1,f11(f8(a1),a7))))), % 117.32/117.32 inference(scs_inference,[],[32,28,2,48])). % 117.32/117.32 cnf(2639,plain, % 117.32/117.32 (E(f11(f8(a1),f12(a1,f11(f8(a1),a7))),f10(a1,a7))), % 117.32/117.32 inference(scs_inference,[],[2637,81,2])). % 117.32/117.32 cnf(2642,plain, % 117.32/117.32 (~E(f11(f8(a1),f4(a1)),f11(f8(a1),f12(a1,f11(f8(a1),a7))))), % 117.32/117.32 inference(scs_inference,[],[911,2637,81,2,92,93,3])). % 117.32/117.32 cnf(2643,plain, % 117.32/117.32 (~E(f4(a1),f12(a1,f11(f8(a1),a7)))), % 117.32/117.32 inference(scs_inference,[],[911,2637,81,2,92,93,3,12])). % 117.32/117.32 cnf(2644,plain, % 117.32/117.32 (~E(f11(f8(a1),f6(a1)),f11(f8(a1),f12(a1,f11(f8(a1),a7))))+~E(f12(a1,f5(f9(f8(a1)))),f6(a1))), % 117.32/117.32 inference(scs_inference,[],[911,2637,81,2,92,93,3,12,1355])). % 117.32/117.32 cnf(2648,plain, % 117.32/117.32 (~E(f11(f8(a1),f12(a1,f11(f8(a1),a7))),f11(f8(a1),f6(a1)))+~E(f12(a1,a7),f6(a1))), % 117.32/117.32 inference(scs_inference,[],[911,2637,81,2,92,93,3,12,1355,991,989])). % 117.32/117.32 cnf(2656,plain, % 117.32/117.32 (~E(f6(a1),f11(f8(a1),f12(a1,f11(f8(a1),a7))))), % 117.32/117.32 inference(scs_inference,[],[897,2639,3])). % 117.32/117.32 cnf(2672,plain, % 117.32/117.32 (~E(f11(f8(a1),f6(a1)),f11(f8(a1),f12(a1,f11(f8(a1),a7))))+~E(f12(a1,a7),f6(a1))), % 117.32/117.32 inference(scs_inference,[],[2648,2])). % 117.32/117.32 cnf(2676,plain, % 117.32/117.32 (~E(f6(a1),f12(a1,f11(f8(a1),a7)))+~E(f12(a1,a7),f6(a1))), % 117.32/117.32 inference(scs_inference,[],[2672,12])). % 117.32/117.32 cnf(2677,plain, % 117.32/117.32 (~E(f6(a1),f12(a1,a7))+~E(f6(a1),f12(a1,f11(f8(a1),a7)))), % 117.32/117.32 inference(scs_inference,[],[2676,2])). % 117.32/117.32 cnf(2678,plain, % 117.32/117.32 (~E(f6(a1),f12(a1,f11(f8(a1),f11(f8(a1),a7))))+~E(f6(a1),f12(a1,f11(f8(a1),a7)))), % 117.32/117.32 inference(scs_inference,[],[327,2677,3])). % 117.32/117.32 cnf(2681,plain, % 117.32/117.32 (~E(f12(a1,f11(f8(a1),f11(f8(a1),a7))),f6(a1))+~E(f6(a1),f12(a1,f11(f8(a1),a7)))), % 117.32/117.32 inference(scs_inference,[],[2678,2])). % 117.32/117.32 cnf(2682,plain, % 117.32/117.32 (~E(f12(a1,f11(f8(a1),a7)),f6(a1))+~E(f12(a1,f11(f8(a1),f11(f8(a1),a7))),f6(a1))), % 117.32/117.32 inference(scs_inference,[],[2681,2])). % 117.32/117.32 cnf(2683,plain, % 117.32/117.32 (~E(f6(a1),f12(a1,f11(f8(a1),f11(f8(a1),a7))))+~E(f12(a1,f11(f8(a1),a7)),f6(a1))), % 117.32/117.32 inference(scs_inference,[],[2682,2])). % 117.32/117.32 cnf(2684,plain, % 117.32/117.32 (~E(f6(a1),f12(a1,a7))+~E(f12(a1,f11(f8(a1),a7)),f6(a1))), % 117.32/117.32 inference(scs_inference,[],[328,2683,3])). % 117.32/117.32 cnf(2685,plain, % 117.32/117.32 (~E(f12(a1,a7),f6(a1))+~E(f12(a1,f11(f8(a1),a7)),f6(a1))), % 117.32/117.32 inference(scs_inference,[],[2684,2])). % 117.32/117.32 cnf(2686,plain, % 117.32/117.32 (~E(x26861,f6(a1))+~E(f12(a1,f11(f8(a1),a7)),x26861)+~E(f12(a1,a7),f6(a1))), % 117.32/117.32 inference(scs_inference,[],[2685,3])). % 117.32/117.32 cnf(2687,plain, % 117.32/117.32 (~E(f6(a1),f12(a1,f11(f8(a1),a7)))+~E(f12(a1,f5(f9(f8(a1)))),f6(a1))), % 117.32/117.32 inference(scs_inference,[],[2644,12])). % 117.32/117.32 cnf(2688,plain, % 117.32/117.32 (~E(f12(a1,f11(f8(a1),a7)),f6(a1))+~E(f12(a1,f5(f9(f8(a1)))),f6(a1))), % 117.32/117.32 inference(scs_inference,[],[2687,2])). % 117.32/117.32 cnf(2689,plain, % 117.32/117.32 (~E(f6(a1),f12(a1,f5(f9(f8(a1)))))+~E(f12(a1,f11(f8(a1),a7)),f6(a1))), % 117.32/117.32 inference(scs_inference,[],[2688,2])). % 117.32/117.32 cnf(2690,plain, % 117.32/117.32 (~E(x26901,f12(a1,f5(f9(f8(a1)))))+~E(f6(a1),x26901)+~E(f12(a1,f11(f8(a1),a7)),f6(a1))), % 117.32/117.32 inference(scs_inference,[],[2689,3])). % 117.32/117.32 cnf(3051,plain, % 117.32/117.32 (~E(f12(a1,f5(f9(f8(a1)))),x30511)+~E(f12(a1,f11(f8(a1),a7)),f6(a1))+~E(f6(a1),x30511)), % 117.32/117.32 inference(scs_inference,[],[2690,2])). % 117.32/117.32 cnf(3053,plain, % 117.32/117.32 (~E(f5(f9(f8(a1))),x30531)+~E(f12(a1,f11(f8(a1),a7)),f6(a1))+~E(f6(a1),f12(a1,x30531))), % 117.32/117.32 inference(scs_inference,[],[3051,14])). % 117.32/117.32 cnf(3056,plain, % 117.32/117.32 (~E(f6(a1),f12(a1,f11(f8(a1),a7)))+~E(f5(f9(f8(a1))),x30561)+~E(f6(a1),f12(a1,x30561))), % 117.32/117.32 inference(scs_inference,[],[3053,2])). % 117.32/117.32 cnf(3058,plain, % 117.32/117.32 (~E(x30581,f12(a1,f11(f8(a1),a7)))+~E(f6(a1),x30581)+~E(f5(f9(f8(a1))),f11(f8(a1),a7))), % 117.32/117.32 inference(scs_inference,[],[3056,3])). % 117.32/117.32 cnf(3062,plain, % 117.32/117.32 (~E(f11(f8(a1),a7),f5(f9(f8(a1))))+~E(x30621,f12(a1,f11(f8(a1),a7)))+~E(f6(a1),x30621)), % 117.32/117.32 inference(scs_inference,[],[3058,2])). % 117.32/117.32 cnf(3065,plain, % 117.32/117.32 (~E(f12(a1,f11(f8(a1),a7)),f4(a1))), % 117.32/117.32 inference(scs_inference,[],[2642,2,12])). % 117.32/117.32 cnf(3066,plain, % 117.32/117.32 (~P7(f10(a1,f11(f8(a1),f11(f8(a1),a7))),a1)), % 117.32/117.32 inference(scs_inference,[],[2163,33,2,24])). % 117.32/117.32 cnf(3067,plain, % 117.32/117.32 (E(f6(a1),f11(f8(a1),f11(f8(a1),f6(a1))))), % 117.32/117.32 inference(scs_inference,[],[946,2,41])). % 117.32/117.32 cnf(3068,plain, % 117.32/117.32 (P4(f11(f8(a1),f11(f8(a1),f6(a1))),f9(f8(a1)))), % 117.32/117.32 inference(scs_inference,[],[3067,955])). % 117.32/117.32 cnf(3070,plain, % 117.32/117.32 (P6(f6(a1),f11(f8(a1),f11(f8(a1),f6(a1))))), % 117.32/117.32 inference(scs_inference,[],[3067,955,954,92])). % 117.32/117.32 cnf(3073,plain, % 117.32/117.32 (P6(f11(f8(a1),f11(f8(a1),f6(a1))),f6(a1))), % 117.32/117.32 inference(scs_inference,[],[3067,955,954,92,77,81,93])). % 117.32/117.32 cnf(3074,plain, % 117.32/117.32 (E(f11(f8(a1),f11(f8(a1),f6(a1))),f6(a1))), % 117.32/117.32 inference(scs_inference,[],[3067,955,954,92,77,81,93,2])). % 117.32/117.32 cnf(3091,plain, % 117.32/117.32 (P5(x30911,a1)+~E(f12(a1,f11(f8(a1),f11(f8(a1),f6(a1)))),x30911)), % 117.32/117.32 inference(scs_inference,[],[26,28,3067,955,954,92,77,81,93,2,43,2686,3058,3062,17,20,16,21,23,15,19,18,22])). % 117.32/117.32 cnf(3107,plain, % 117.32/117.32 (~P7(f11(f8(a1),f11(f8(a1),f6(a1))),a1)+P5(f11(f8(a1),f11(f8(a1),f11(f8(a1),f6(a1)))),a1)), % 117.32/117.32 inference(scs_inference,[],[26,28,3068,3074,81,17,16,15,19,46])). % 117.32/117.32 cnf(3122,plain, % 117.32/117.32 (P5(f11(f8(a1),f11(f8(a1),f11(f8(a1),f6(a1)))),a1)), % 117.32/117.32 inference(scs_inference,[],[896,3067,3107,24])). % 117.32/117.32 cnf(3124,plain, % 117.32/117.32 (P5(x31241,a1)+~E(f11(f8(a1),f11(f8(a1),f11(f8(a1),f6(a1)))),x31241)), % 117.32/117.32 inference(scs_inference,[],[3122,23,22])). % 117.32/117.32 cnf(3523,plain, % 117.32/117.32 (P4(a7,f9(f11(f8(a1),f11(f8(a1),a7))))), % 117.32/117.32 inference(scs_inference,[],[108,92,37])). % 117.32/117.32 cnf(3524,plain, % 117.32/117.32 (P4(a7,f9(a7))), % 117.32/117.32 inference(scs_inference,[],[1966,3523,18])). % 117.32/117.32 cnf(3525,plain, % 117.32/117.32 (P4(f11(f8(a1),f11(f8(a1),a7)),f9(a7))), % 117.32/117.32 inference(scs_inference,[],[108,1966,3523,18,17])). % 117.32/117.32 cnf(3526,plain, % 117.32/117.32 (P6(f11(a7,x35261),f11(f11(f8(a1),f11(f8(a1),a7)),x35261))), % 117.32/117.32 inference(scs_inference,[],[108,92,11])). % 117.32/117.32 cnf(3527,plain, % 117.32/117.32 (P6(x35271,f11(f11(f8(a1),f11(f8(a1),a7)),x35272))+~E(f11(a7,x35272),x35271)), % 117.32/117.32 inference(scs_inference,[],[3526,20])). % 117.32/117.32 cnf(3531,plain, % 117.32/117.32 (P6(f11(x35311,a7),f11(x35311,f11(f8(a1),f11(f8(a1),a7))))), % 117.32/117.32 inference(scs_inference,[],[108,92,12])). % 117.32/117.32 cnf(3532,plain, % 117.32/117.32 (P6(f11(x35321,a7),x35322)+~E(f11(x35321,f11(f8(a1),f11(f8(a1),a7))),x35322)), % 117.32/117.32 inference(scs_inference,[],[3531,21])). % 117.32/117.32 cnf(3536,plain, % 117.32/117.32 (P6(f12(a7,x35361),f12(f11(f8(a1),f11(f8(a1),a7)),x35361))), % 117.32/117.32 inference(scs_inference,[],[108,92,13])). % 117.32/117.32 cnf(3539,plain, % 117.32/117.32 (P6(f6(f11(f8(a1),f11(f8(a1),a7))),f6(a7))), % 117.32/117.32 inference(scs_inference,[],[111,92,10])). % 117.32/117.32 cnf(3544,plain, % 117.32/117.32 (P6(f11(x35441,f11(f8(a1),f11(f8(a1),a7))),f11(x35441,a7))), % 117.32/117.32 inference(scs_inference,[],[111,92,12])). % 117.32/117.32 cnf(3549,plain, % 117.32/117.32 (P6(f12(f11(f8(a1),f11(f8(a1),a7)),x35491),f12(a7,x35491))), % 117.32/117.32 inference(scs_inference,[],[111,92,13])). % 117.32/117.32 cnf(3553,plain, % 117.32/117.32 (P4(f10(f11(f8(a1),f11(f8(a1),a7)),x35531),f9(f10(a7,x35531)))), % 117.32/117.32 inference(scs_inference,[],[2144,93,37])). % 117.32/117.32 cnf(3554,plain, % 117.32/117.32 (P4(f10(a7,x35541),f9(f10(a7,x35541)))), % 117.32/117.32 inference(scs_inference,[],[2146,3553,17])). % 117.32/117.32 cnf(3555,plain, % 117.32/117.32 (P4(f10(f11(f8(a1),f11(f8(a1),a7)),x35551),f9(f10(a7,x35551)))), % 117.32/117.32 inference(rename_variables,[],[3553])). % 117.32/117.32 cnf(3557,plain, % 117.32/117.32 (P6(f10(f11(f8(a1),f11(f8(a1),a7)),x35571),x35572)+~E(f9(f10(a7,x35571)),f9(x35572))), % 117.32/117.32 inference(scs_inference,[],[2146,3553,3555,17,18,38])). % 117.32/117.32 cnf(3566,plain, % 117.32/117.32 (P4(f10(a7,x35661),x35662)+~E(f9(f10(a7,x35661)),x35662)), % 117.32/117.32 inference(scs_inference,[],[3554,18])). % 117.32/117.32 cnf(3612,plain, % 117.32/117.32 (P4(f11(f8(a1),f12(a1,f11(f8(a1),a7))),f9(f10(a1,a7)))), % 117.32/117.32 inference(scs_inference,[],[2637,93,37])). % 117.32/117.32 cnf(3613,plain, % 117.32/117.32 (P4(f10(a1,a7),f9(f10(a1,a7)))), % 117.32/117.32 inference(scs_inference,[],[2639,3612,17])). % 117.32/117.32 cnf(3657,plain, % 117.32/117.32 (P4(f4(f11(f8(a1),f11(f8(a1),a7))),f9(f4(a7)))), % 117.32/117.32 inference(scs_inference,[],[2583,93,37])). % 117.32/117.32 cnf(3658,plain, % 117.32/117.32 (P4(f4(a7),f9(f4(a7)))), % 117.32/117.32 inference(scs_inference,[],[2582,3657,17])). % 117.32/117.32 cnf(3711,plain, % 117.32/117.32 (P6(f10(a1,a7),f11(f10(a1,a7),f11(f10(a1,a7),f10(a1,a7))))), % 117.32/117.32 inference(scs_inference,[],[3613,93,41])). % 117.32/117.32 cnf(3712,plain, % 117.32/117.32 (P6(f10(a1,a7),x37121)+~E(f11(f10(a1,a7),f11(f10(a1,a7),f10(a1,a7))),x37121)), % 117.32/117.32 inference(scs_inference,[],[3711,21])). % 117.32/117.32 cnf(3723,plain, % 117.32/117.32 (E(f11(f8(a1),f11(f8(a1),f11(f8(a1),a7))),f11(f8(a1),a7))), % 117.32/117.32 inference(scs_inference,[],[391,37,41])). % 117.32/117.32 cnf(3724,plain, % 117.32/117.32 (E(f11(f8(a1),a7),f11(f8(a1),f11(f8(a1),f11(f8(a1),a7))))), % 117.32/117.32 inference(scs_inference,[],[3723,2])). % 117.32/117.32 cnf(4079,plain, % 117.32/117.32 (P4(f11(f8(a1),f6(a1)),f9(f8(a1)))), % 117.32/117.32 inference(scs_inference,[],[947,37,42])). % 117.32/117.32 cnf(4082,plain, % 117.32/117.32 (P5(f12(a1,f11(f8(a1),f6(a1))),a1)), % 117.32/117.32 inference(scs_inference,[],[26,28,4079,38,43])). % 117.32/117.32 cnf(4090,plain, % 117.32/117.32 (P5(x40901,a1)+~E(f12(a1,f11(f8(a1),f6(a1))),x40901)), % 117.32/117.32 inference(scs_inference,[],[33,26,28,951,4079,38,43,47,18,24,529,22])). % 117.32/117.32 cnf(4094,plain, % 117.32/117.32 (P4(x40941,f9(f8(a1)))+~E(f11(f8(a1),f6(a1)),x40941)), % 117.32/117.32 inference(scs_inference,[],[33,26,28,951,4079,38,43,47,18,24,529,22,21,25,20,17])). % 117.32/117.32 cnf(4119,plain, % 117.32/117.32 (P4(f12(a1,f6(a1)),f9(f8(a1)))), % 117.32/117.32 inference(scs_inference,[],[947,28,37,44])). % 117.32/117.32 cnf(4120,plain, % 117.32/117.32 (P6(f12(a1,f6(a1)),f8(a1))), % 117.32/117.32 inference(scs_inference,[],[4119,38])). % 117.32/117.32 cnf(4122,plain, % 117.32/117.32 (P5(f12(a1,f12(a1,f6(a1))),a1)), % 117.32/117.32 inference(scs_inference,[],[26,28,4119,38,43])). % 117.32/117.32 cnf(4124,plain, % 117.32/117.32 (P7(f11(f8(a1),f12(a1,f6(a1))),a1)), % 117.32/117.32 inference(scs_inference,[],[26,28,949,4119,38,43,47])). % 117.32/117.32 cnf(4127,plain, % 117.32/117.32 (~E(f11(f8(a1),f12(a1,f6(a1))),f10(a1,a7))), % 117.32/117.32 inference(scs_inference,[],[33,26,28,949,4119,38,43,47,18,24])). % 117.32/117.32 cnf(4130,plain, % 117.32/117.32 (P5(x41301,a1)+~E(f12(a1,f12(a1,f6(a1))),x41301)), % 117.32/117.32 inference(scs_inference,[],[33,26,28,949,4119,38,43,47,18,24,529,22])). % 117.32/117.32 cnf(4132,plain, % 117.32/117.32 (P6(x41321,f8(a1))+~E(f12(a1,f6(a1)),x41321)), % 117.32/117.32 inference(scs_inference,[],[33,26,28,949,4119,38,43,47,18,24,529,22,21,20])). % 117.32/117.32 cnf(4135,plain, % 117.32/117.32 (P4(x41351,f9(f8(a1)))+~E(f12(a1,f6(a1)),x41351)), % 117.32/117.32 inference(scs_inference,[],[33,26,28,949,4119,38,43,47,18,24,529,22,21,20,25,23,17])). % 117.32/117.32 cnf(4185,plain, % 117.32/117.32 (P4(f11(f8(a1),f11(f8(a1),f11(f8(a1),a7))),f9(f8(a1)))), % 117.32/117.32 inference(scs_inference,[],[3724,37,393])). % 117.32/117.32 cnf(4187,plain, % 117.32/117.32 (P5(f12(a1,f11(f8(a1),a7)),a1)), % 117.32/117.32 inference(scs_inference,[],[26,28,3723,4185,17,43])). % 117.32/117.32 cnf(4202,plain, % 117.32/117.32 (P5(x42021,a1)+~E(f12(a1,f11(f8(a1),a7)),x42021)), % 117.32/117.32 inference(scs_inference,[],[4187,22])). % 117.32/117.32 cnf(4270,plain, % 117.32/117.32 (P4(f11(f8(a1),a7),f9(f11(f8(a1),a7)))), % 117.32/117.32 inference(scs_inference,[],[3723,37,3532])). % 117.32/117.32 cnf(4279,plain, % 117.32/117.32 (E(f11(f8(a1),f11(f8(a1),f4(a1))),f4(a1))), % 117.32/117.32 inference(scs_inference,[],[904,37,41])). % 117.32/117.32 cnf(4282,plain, % 117.32/117.32 (E(f4(a1),f11(f8(a1),f11(f8(a1),f4(a1))))), % 117.32/117.32 inference(scs_inference,[],[4279,93,92,2])). % 117.32/117.32 cnf(4287,plain, % 117.32/117.32 (P4(f11(f8(a1),f11(f8(a1),f4(a1))),f9(f8(a1)))), % 117.32/117.32 inference(scs_inference,[],[903,885,904,4279,3065,93,92,2,81,3,22,20,17])). % 117.32/117.32 cnf(4288,plain, % 117.32/117.32 (P5(f12(a1,f11(f8(a1),f11(f8(a1),f4(a1)))),a1)), % 117.32/117.32 inference(scs_inference,[],[26,28,903,885,904,4279,3065,93,92,2,81,3,22,20,17,43])). % 117.32/117.32 cnf(4293,plain, % 117.32/117.32 (~E(f11(f8(a1),f11(f8(a1),f11(f8(a1),f4(a1)))),f10(a1,a7))), % 117.32/117.32 inference(scs_inference,[],[33,26,28,903,885,904,4279,3065,93,92,2,81,3,22,20,17,43,47,77,24])). % 117.32/117.32 cnf(4304,plain, % 117.32/117.32 (P5(x43041,a1)+~E(f12(a1,f11(f8(a1),f11(f8(a1),f4(a1)))),x43041)), % 117.32/117.32 inference(scs_inference,[],[4288,4279,4282,81,15,16,19,22])). % 117.32/117.32 cnf(4349,plain, % 117.32/117.32 (P4(f11(f8(a1),f4(a1)),f9(f8(a1)))), % 117.32/117.32 inference(scs_inference,[],[904,37,42])). % 117.32/117.32 cnf(4355,plain, % 117.32/117.32 (P5(x43551,a1)+~E(f12(a1,f11(f8(a1),f4(a1))),x43551)), % 117.32/117.32 inference(scs_inference,[],[26,28,4349,38,43,18,22])). % 117.32/117.32 cnf(4357,plain, % 117.32/117.32 (P6(x43571,f8(a1))+~E(f11(f8(a1),f4(a1)),x43571)), % 117.32/117.32 inference(scs_inference,[],[26,28,4349,38,43,18,22,21,20])). % 117.32/117.32 cnf(4358,plain, % 117.32/117.32 (P4(x43581,f9(f8(a1)))+~E(f11(f8(a1),f4(a1)),x43581)), % 117.32/117.32 inference(scs_inference,[],[26,28,4349,38,43,18,22,21,20,17])). % 117.32/117.32 cnf(4774,plain, % 117.32/117.32 (P4(f11(f8(a1),f11(f8(a1),f4(a1))),f9(f4(a1)))), % 117.32/117.32 inference(scs_inference,[],[4279,37,92])). % 117.32/117.32 cnf(4775,plain, % 117.32/117.32 (P4(f4(a1),f9(f4(a1)))), % 117.32/117.32 inference(scs_inference,[],[4279,4774,17])). % 117.32/117.32 cnf(4796,plain, % 117.32/117.32 (E(f11(f8(a1),f11(f8(a1),f12(a1,f6(a1)))),f12(a1,f6(a1)))), % 117.32/117.32 inference(scs_inference,[],[4120,37,41])). % 117.32/117.32 cnf(4797,plain, % 117.32/117.32 (P6(f11(f8(a1),f11(f8(a1),f12(a1,f6(a1)))),f12(a1,f6(a1)))), % 117.32/117.32 inference(scs_inference,[],[4796,92])). % 117.32/117.32 cnf(4828,plain, % 117.32/117.32 (P4(f11(f8(a1),f12(a1,f6(a1))),f9(f8(a1)))), % 117.32/117.32 inference(scs_inference,[],[4120,37,42])). % 117.32/117.32 cnf(4834,plain, % 117.32/117.32 (P4(x48341,f9(f8(a1)))+~E(f11(f8(a1),f12(a1,f6(a1))),x48341)), % 117.32/117.33 inference(scs_inference,[],[26,28,4828,38,43,18,17])). % 117.32/117.33 cnf(4838,plain, % 117.32/117.33 (P5(x48381,a1)+~E(f12(a1,f11(f8(a1),f12(a1,f6(a1)))),x48381)), % 117.32/117.33 inference(scs_inference,[],[26,28,4828,38,43,18,17,21,23,20,22])). % 117.32/117.33 cnf(4885,plain, % 117.32/117.33 (P4(f12(a1,f12(a1,f6(a1))),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[4120,28,37,44])). % 117.32/117.33 cnf(4892,plain, % 117.32/117.33 (~E(f11(f8(a1),f12(a1,f12(a1,f6(a1)))),f10(a1,a7))), % 117.32/117.33 inference(scs_inference,[],[33,26,28,4122,4885,38,43,47,24])). % 117.32/117.33 cnf(4894,plain, % 117.32/117.33 (P4(x48941,f9(f8(a1)))+~E(f12(a1,f12(a1,f6(a1))),x48941)), % 117.32/117.33 inference(scs_inference,[],[33,26,28,4122,4885,38,43,47,24,18,17])). % 117.32/117.33 cnf(4898,plain, % 117.32/117.33 (P5(x48981,a1)+~E(f12(a1,f12(a1,f12(a1,f6(a1)))),x48981)), % 117.32/117.33 inference(scs_inference,[],[33,26,28,4122,4885,38,43,47,24,18,17,25,23,21,22])). % 117.32/117.33 cnf(4921,plain, % 117.32/117.33 (P4(f10(a1,f12(a1,f6(a1))),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[4120,28,37,45])). % 117.32/117.33 cnf(4922,plain, % 117.32/117.33 (P6(f10(a1,f12(a1,f6(a1))),f8(a1))), % 117.32/117.33 inference(scs_inference,[],[4921,38])). % 117.32/117.33 cnf(4924,plain, % 117.32/117.33 (P5(f12(a1,f10(a1,f12(a1,f6(a1)))),a1)), % 117.32/117.33 inference(scs_inference,[],[26,28,4921,38,43])). % 117.32/117.33 cnf(4926,plain, % 117.32/117.33 (P4(x49261,f9(f8(a1)))+~E(f10(a1,f12(a1,f6(a1))),x49261)), % 117.32/117.33 inference(scs_inference,[],[26,28,4921,38,43,17])). % 117.32/117.33 cnf(4941,plain, % 117.32/117.33 (P5(x49411,a1)+~E(f12(a1,f10(a1,f12(a1,f6(a1)))),x49411)), % 117.32/117.33 inference(scs_inference,[],[4924,4922,21,20,23,22])). % 117.32/117.33 cnf(4998,plain, % 117.32/117.33 (P4(f12(a1,f6(a1)),f9(f12(a1,f6(a1))))), % 117.32/117.33 inference(scs_inference,[],[4797,4796,37,20])). % 117.32/117.33 cnf(5008,plain, % 117.32/117.33 (P6(f12(a1,a7),f8(a1))), % 117.32/117.33 inference(scs_inference,[],[32,28,38,44])). % 117.32/117.33 cnf(5009,plain, % 117.32/117.33 (P6(f12(a1,f11(f8(a1),f11(f8(a1),a7))),f8(a1))), % 117.32/117.33 inference(scs_inference,[],[5008,328,20])). % 117.32/117.33 cnf(5019,plain, % 117.32/117.33 (~E(x50191,f8(a1))+P6(a7,x50191)), % 117.32/117.33 inference(scs_inference,[],[65,2])). % 117.32/117.33 cnf(5502,plain, % 117.32/117.33 (P4(f11(a7,a7),f9(a7))), % 117.32/117.33 inference(scs_inference,[],[3524,1968,4282,37,4,5,6,9,10,7,8,11,13,14,42])). % 117.32/117.33 cnf(5504,plain, % 117.32/117.33 (E(f11(a7,f11(a7,a7)),a7)), % 117.32/117.33 inference(scs_inference,[],[3524,1968,4282,37,4,5,6,9,10,7,8,11,13,14,42,41])). % 117.32/117.33 cnf(5514,plain, % 117.32/117.33 (~P4(f12(a1,f11(f8(a1),a7)),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[28,4127,2643,3524,1968,30,4282,2639,4187,33,26,27,37,4,5,6,9,10,7,8,11,13,14,42,41,34,12,2,24,20,3,47])). % 117.32/117.33 cnf(5518,plain, % 117.32/117.33 (~E(f10(a1,f12(a1,f6(a1))),f12(a1,f11(f8(a1),a7)))), % 117.32/117.33 inference(scs_inference,[],[28,4127,2643,3524,1968,30,4282,2639,4187,33,26,27,37,4,5,6,9,10,7,8,11,13,14,42,41,34,12,2,24,20,3,47,4357,4358,4926])). % 117.32/117.33 cnf(5519,plain, % 117.32/117.33 (~E(f5(f9(f8(a1))),f12(a1,f11(f8(a1),a7)))), % 117.32/117.33 inference(scs_inference,[],[28,4127,2643,3524,1968,30,4282,2639,4187,33,26,27,37,4,5,6,9,10,7,8,11,13,14,42,41,34,12,2,24,20,3,47,4357,4358,4926,70])). % 117.32/117.33 cnf(5520,plain, % 117.32/117.33 (~E(a7,f12(a1,f11(f8(a1),a7)))), % 117.32/117.33 inference(scs_inference,[],[28,4127,2643,3524,1968,30,4282,2639,4187,33,26,27,37,4,5,6,9,10,7,8,11,13,14,42,41,34,12,2,24,20,3,47,4357,4358,4926,70,53])). % 117.32/117.33 cnf(5521,plain, % 117.32/117.33 (~E(f6(a1),f12(a1,f11(f8(a1),a7)))), % 117.32/117.33 inference(scs_inference,[],[28,4127,2643,3524,1968,30,4282,2639,4187,33,26,27,37,4,5,6,9,10,7,8,11,13,14,42,41,34,12,2,24,20,3,47,4357,4358,4926,70,53,955])). % 117.32/117.33 cnf(5533,plain, % 117.32/117.33 (E(f12(f11(a7,f11(a7,a7)),x55331),f12(a7,x55331))), % 117.32/117.33 inference(scs_inference,[],[5504,13])). % 117.32/117.33 cnf(5534,plain, % 117.32/117.33 (P4(f11(a7,f11(a7,a7)),f9(a7))), % 117.32/117.33 inference(scs_inference,[],[5502,5504,13,42])). % 117.32/117.33 cnf(5538,plain, % 117.32/117.33 (E(f10(f11(a7,f11(a7,a7)),x55381),f10(a7,x55381))), % 117.32/117.33 inference(scs_inference,[],[5502,5504,13,42,41,7])). % 117.32/117.33 cnf(5541,plain, % 117.32/117.33 (E(f11(f11(a7,f11(a7,a7)),x55411),f11(a7,x55411))), % 117.32/117.33 inference(scs_inference,[],[5502,5504,329,13,42,41,7,37,11])). % 117.32/117.33 cnf(5542,plain, % 117.32/117.33 (E(f12(x55421,f11(a7,f11(a7,a7))),f12(x55421,a7))), % 117.32/117.33 inference(scs_inference,[],[5502,5504,329,13,42,41,7,37,11,14])). % 117.32/117.33 cnf(5543,plain, % 117.32/117.33 (E(f10(x55431,f11(a7,f11(a7,a7))),f10(x55431,a7))), % 117.32/117.33 inference(scs_inference,[],[5502,5504,329,13,42,41,7,37,11,14,8])). % 117.32/117.33 cnf(5544,plain, % 117.32/117.33 (E(f8(f11(a7,f11(a7,a7))),f8(a7))), % 117.32/117.33 inference(scs_inference,[],[5502,5504,329,13,42,41,7,37,11,14,8,5])). % 117.32/117.33 cnf(5547,plain, % 117.32/117.33 (E(f4(f11(a7,f11(a7,a7))),f4(a7))), % 117.32/117.33 inference(scs_inference,[],[5502,5504,329,13,42,41,7,37,11,14,8,5,6,4,9])). % 117.32/117.33 cnf(5548,plain, % 117.32/117.33 (E(f6(f11(a7,f11(a7,a7))),f6(a7))), % 117.32/117.33 inference(scs_inference,[],[5502,5504,329,13,42,41,7,37,11,14,8,5,6,4,9,10])). % 117.32/117.33 cnf(5549,plain, % 117.32/117.33 (E(f11(x55491,f11(a7,f11(a7,a7))),f11(x55491,a7))), % 117.32/117.33 inference(scs_inference,[],[5502,5504,329,13,42,41,7,37,11,14,8,5,6,4,9,10,12])). % 117.32/117.33 cnf(5550,plain, % 117.32/117.33 (~E(f12(a1,f11(f8(a1),a7)),a7)), % 117.32/117.33 inference(scs_inference,[],[5502,5504,5520,329,13,42,41,7,37,11,14,8,5,6,4,9,10,12,2])). % 117.32/117.33 cnf(5551,plain, % 117.32/117.33 (E(f11(a7,f11(a7,a7)),f11(f8(a1),f11(f8(a1),a7)))), % 117.32/117.33 inference(scs_inference,[],[5502,5504,5520,329,108,13,42,41,7,37,11,14,8,5,6,4,9,10,12,2,3])). % 117.32/117.33 cnf(5554,plain, % 117.32/117.33 (P4(f10(a1,f11(f8(a1),f11(f8(a1),f6(a1)))),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[28,5502,5504,5520,329,3068,108,31,13,42,41,7,37,11,14,8,5,6,4,9,10,12,2,3,18,45])). % 117.32/117.33 cnf(5564,plain, % 117.32/117.33 (P4(f11(a7,f11(a7,f11(a7,a7))),f9(a7))), % 117.32/117.33 inference(scs_inference,[],[5534,41,42])). % 117.32/117.33 cnf(5566,plain, % 117.32/117.33 (P4(f11(f8(a1),f11(f8(a1),f6(a1))),f9(f6(a1)))), % 117.32/117.33 inference(scs_inference,[],[5534,3073,41,42,37])). % 117.32/117.33 cnf(5580,plain, % 117.32/117.33 (P4(f12(a1,f11(f8(a1),f11(f8(a1),f4(a1)))),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[28,5534,5538,5521,3073,4287,41,42,37,13,14,6,7,5,8,4,9,10,11,12,2,44])). % 117.32/117.33 cnf(5582,plain, % 117.32/117.33 (~P7(f10(a1,f11(a7,f11(a7,a7))),a1)), % 117.32/117.33 inference(scs_inference,[],[28,5534,5538,5543,5521,3073,4287,33,41,42,37,13,14,6,7,5,8,4,9,10,11,12,2,44,24])). % 117.32/117.33 cnf(5593,plain, % 117.32/117.33 (E(f11(f4(a1),f11(f4(a1),f4(a1))),f4(a1))), % 117.32/117.33 inference(scs_inference,[],[4775,41])). % 117.32/117.33 cnf(5601,plain, % 117.32/117.33 (E(f12(f11(f11(a7,f11(a7,a7)),x56011),x56012),f12(f11(a7,x56011),x56012))), % 117.32/117.33 inference(scs_inference,[],[5541,5564,3070,4775,41,42,37,7,4,13])). % 117.32/117.33 cnf(5604,plain, % 117.32/117.33 (E(f10(x56041,f11(f11(a7,f11(a7,a7)),x56042)),f10(x56041,f11(a7,x56042)))), % 117.32/117.33 inference(scs_inference,[],[5541,5564,3070,4775,41,42,37,7,4,13,14,6,8])). % 117.32/117.33 cnf(5606,plain, % 117.32/117.33 (E(f4(f11(f11(a7,f11(a7,a7)),x56061)),f4(f11(a7,x56061)))), % 117.32/117.33 inference(scs_inference,[],[5541,5564,3070,4775,41,42,37,7,4,13,14,6,8,5,9])). % 117.32/117.33 cnf(5611,plain, % 117.32/117.33 (~P7(f10(a1,f11(f11(a7,f11(a7,a7)),f11(a7,a7))),a1)), % 117.32/117.33 inference(scs_inference,[],[5541,5564,5582,4293,3070,4775,41,42,37,7,4,13,14,6,8,5,9,10,11,12,2,24])). % 117.32/117.33 cnf(5612,plain, % 117.32/117.33 (E(f11(f11(a7,f11(a7,a7)),f11(a7,a7)),f11(f8(a1),f11(f8(a1),a7)))), % 117.32/117.33 inference(scs_inference,[],[5541,5564,5582,5551,4293,3070,4775,41,42,37,7,4,13,14,6,8,5,9,10,11,12,2,24,3])). % 117.32/117.33 cnf(5618,plain, % 117.32/117.33 (E(f11(f4(a7),f11(f4(a7),f4(a7))),f4(a7))), % 117.32/117.33 inference(scs_inference,[],[3658,41])). % 117.32/117.33 cnf(5627,plain, % 117.32/117.33 (E(f5(f12(x56271,f11(a7,f11(a7,a7)))),f5(f12(x56271,a7)))), % 117.32/117.33 inference(scs_inference,[],[5542,5566,3549,3658,41,37,42,14,7,5,4])). % 117.32/117.33 cnf(5636,plain, % 117.32/117.33 (~E(f11(f8(a1),f12(a1,f6(a1))),f10(a1,f11(f11(a7,f11(a7,a7)),f11(a7,a7))))), % 117.32/117.33 inference(scs_inference,[],[5542,5566,5611,4892,4124,3549,3658,41,37,42,14,7,5,4,13,6,8,9,10,11,12,2,24])). % 117.32/117.33 cnf(5637,plain, % 117.32/117.33 (E(f12(f11(a7,f11(a7,a7)),f11(a7,f11(a7,a7))),f12(a7,a7))), % 117.32/117.33 inference(scs_inference,[],[5542,5533,5566,5611,4892,4124,3549,3658,41,37,42,14,7,5,4,13,6,8,9,10,11,12,2,24,3])). % 117.32/117.33 cnf(5646,plain, % 117.32/117.33 (E(f11(f10(a7,x56461),f11(f10(a7,x56461),f10(a7,x56461))),f10(a7,x56461))), % 117.32/117.33 inference(scs_inference,[],[3554,41])). % 117.32/117.33 cnf(5664,plain, % 117.32/117.33 (P6(f8(a7),f8(f11(a7,f11(a7,a7))))), % 117.32/117.33 inference(scs_inference,[],[5544,5519,3525,2166,3554,30,41,42,37,4,8,14,7,5,6,13,9,10,11,12,2,20])). % 117.32/117.33 cnf(5672,plain, % 117.32/117.33 (E(f11(f10(a1,a7),f11(f10(a1,a7),f10(a1,a7))),f10(a1,a7))), % 117.32/117.33 inference(scs_inference,[],[3613,41])). % 117.32/117.33 cnf(5680,plain, % 117.32/117.33 (E(f5(f11(f10(a7,x56801),f11(f10(a7,x56801),f10(a7,x56801)))),f5(f10(a7,x56801)))), % 117.32/117.33 inference(scs_inference,[],[5646,5664,4998,3613,41,37,42,7,13,4])). % 117.32/117.33 cnf(5687,plain, % 117.32/117.33 (E(f11(f11(f10(a7,x56871),f11(f10(a7,x56871),f10(a7,x56871))),x56872),f11(f10(a7,x56871),x56872))), % 117.32/117.33 inference(scs_inference,[],[5646,5664,4998,3613,41,37,42,7,13,4,8,14,6,5,9,10,11])). % 117.32/117.33 cnf(5690,plain, % 117.32/117.33 (~P7(f11(f10(a1,a7),f11(f10(a1,a7),f10(a1,a7))),a1)), % 117.32/117.33 inference(scs_inference,[],[5646,5664,2656,4998,3613,33,41,37,42,7,13,4,8,14,6,5,9,10,11,12,2,24])). % 117.32/117.33 cnf(5691,plain, % 117.32/117.33 (P4(f5(f12(x56911,a7)),f12(x56911,f11(a7,f11(a7,a7))))), % 117.32/117.33 inference(scs_inference,[],[5646,5664,2656,5627,4998,3613,33,31,41,37,42,7,13,4,8,14,6,5,9,10,11,12,2,24,17])). % 117.32/117.33 cnf(5693,plain, % 117.32/117.33 (E(f11(f11(a7,f11(a7,a7)),f11(a7,a7)),a7)), % 117.32/117.33 inference(scs_inference,[],[5646,5664,5612,2656,5627,4998,3613,111,33,31,41,37,42,7,13,4,8,14,6,5,9,10,11,12,2,24,17,3])). % 117.32/117.33 cnf(5704,plain, % 117.32/117.33 (E(f10(x57041,f11(f11(a7,f11(a7,a7)),f11(a7,a7))),f10(x57041,a7))), % 117.32/117.33 inference(scs_inference,[],[5693,1733,4270,4079,41,42,37,8])). % 117.32/117.33 cnf(5705,plain, % 117.32/117.33 (E(f8(f11(f11(a7,f11(a7,a7)),f11(a7,a7))),f8(a7))), % 117.32/117.33 inference(scs_inference,[],[5693,1733,4270,4079,41,42,37,8,5])). % 117.32/117.33 cnf(5706,plain, % 117.32/117.33 (E(f10(f11(f11(a7,f11(a7,a7)),f11(a7,a7)),x57061),f10(a7,x57061))), % 117.32/117.33 inference(scs_inference,[],[5693,1733,4270,4079,41,42,37,8,5,7])). % 117.32/117.33 cnf(5708,plain, % 117.32/117.33 (E(f9(f11(f11(a7,f11(a7,a7)),f11(a7,a7))),f9(a7))), % 117.32/117.33 inference(scs_inference,[],[5693,1733,4270,4079,41,42,37,8,5,7,13,6])). % 117.32/117.33 cnf(5709,plain, % 117.32/117.33 (E(f12(x57091,f11(f11(a7,f11(a7,a7)),f11(a7,a7))),f12(x57091,a7))), % 117.32/117.33 inference(scs_inference,[],[5693,1733,4270,4079,41,42,37,8,5,7,13,6,14])). % 117.32/117.33 cnf(5710,plain, % 117.32/117.33 (E(f5(f11(f11(a7,f11(a7,a7)),f11(a7,a7))),f5(a7))), % 117.32/117.33 inference(scs_inference,[],[5693,1733,4270,4079,41,42,37,8,5,7,13,6,14,4])). % 117.32/117.33 cnf(5711,plain, % 117.32/117.33 (E(f4(f11(f11(a7,f11(a7,a7)),f11(a7,a7))),f4(a7))), % 117.32/117.33 inference(scs_inference,[],[5693,1733,4270,4079,41,42,37,8,5,7,13,6,14,4,9])). % 117.32/117.33 cnf(5713,plain, % 117.32/117.33 (E(f11(f11(f11(a7,f11(a7,a7)),f11(a7,a7)),x57131),f11(a7,x57131))), % 117.32/117.33 inference(scs_inference,[],[5693,1733,4270,4079,41,42,37,8,5,7,13,6,14,4,9,10,11])). % 117.32/117.33 cnf(5714,plain, % 117.32/117.33 (E(f11(x57141,f11(f11(a7,f11(a7,a7)),f11(a7,a7))),f11(x57141,a7))), % 117.32/117.33 inference(scs_inference,[],[5693,1733,4270,4079,41,42,37,8,5,7,13,6,14,4,9,10,11,12])). % 117.32/117.33 cnf(5715,plain, % 117.32/117.33 (~E(f10(a1,f11(f11(a7,f11(a7,a7)),f11(a7,a7))),f11(f8(a1),f12(a1,f6(a1))))), % 117.32/117.33 inference(scs_inference,[],[5693,5636,1733,4270,4079,41,42,37,8,5,7,13,6,14,4,9,10,11,12,2])). % 117.32/117.33 cnf(5736,plain, % 117.32/117.33 (P4(f11(f4(a1),f4(a1)),f9(f4(a1)))), % 117.32/117.33 inference(scs_inference,[],[5009,4775,4349,41,37,42])). % 117.32/117.33 cnf(5750,plain, % 117.32/117.33 (E(f10(f11(f11(a7,f11(a7,a7)),f11(a7,a7)),f11(f11(a7,f11(a7,a7)),f11(a7,a7))),f10(a7,a7))), % 117.32/117.33 inference(scs_inference,[],[5618,5704,5706,2642,5009,4775,4349,41,37,42,13,4,8,5,7,14,6,9,10,11,12,2,3])). % 117.32/117.33 cnf(5759,plain, % 117.32/117.33 (P4(f11(f4(a1),f11(f4(a1),f4(a1))),f9(f4(a1)))), % 117.32/117.33 inference(scs_inference,[],[5736,41,42])). % 117.32/117.33 cnf(5798,plain, % 117.32/117.33 (E(f11(f11(f11(a7,f11(a7,a7)),f11(a7,a7)),f11(f11(a7,f11(a7,a7)),f11(a7,a7))),f11(a7,a7))), % 117.32/117.33 inference(scs_inference,[],[5547,5713,5714,5759,3711,37,42,4,14,5,6,8,13,7,9,10,11,12,3])). % 117.32/117.33 cnf(5821,plain, % 117.32/117.33 (P4(f12(a1,a7),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[32,5548,4774,3539,28,37,42,8,4,9,14,5,7,13,10,11,6,12,44])). % 117.32/117.33 cnf(5823,plain, % 117.32/117.33 (P4(f10(a1,a7),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[32,5548,4774,3539,28,37,42,8,4,9,14,5,7,13,10,11,6,12,44,45])). % 117.32/117.33 cnf(5825,plain, % 117.32/117.33 (P6(f6(a7),f6(f11(a7,f11(a7,a7))))), % 117.32/117.33 inference(scs_inference,[],[32,5548,4774,3539,30,28,37,42,8,4,9,14,5,7,13,10,11,6,12,44,45,20])). % 117.32/117.33 cnf(5827,plain, % 117.32/117.33 (E(f12(f11(f11(a7,f11(a7,a7)),f11(a7,a7)),f11(a7,f11(a7,a7))),f12(a7,a7))), % 117.32/117.33 inference(scs_inference,[],[32,5548,5637,5601,4774,3539,30,28,37,42,8,4,9,14,5,7,13,10,11,6,12,44,45,20,3])). % 117.32/117.33 cnf(5831,plain, % 117.32/117.33 (E(f11(f8(a1),f11(f8(a1),f12(a1,a7))),f12(a1,a7))), % 117.32/117.33 inference(scs_inference,[],[32,5548,5637,5601,4774,3539,30,51,26,28,37,42,8,4,9,14,5,7,13,10,11,6,12,44,45,20,3,47,41])). % 117.32/117.33 cnf(5839,plain, % 117.32/117.33 (E(f11(f8(a1),f11(f8(a1),f10(a1,a7))),f10(a1,a7))), % 117.32/117.33 inference(scs_inference,[],[5823,41])). % 117.32/117.33 cnf(5843,plain, % 117.32/117.33 (P4(f11(f8(a1),f10(a1,a7)),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[5823,5825,41,37,42])). % 117.32/117.33 cnf(5847,plain, % 117.32/117.33 (E(f11(f11(f8(a1),f11(f8(a1),f12(a1,a7))),x58471),f11(f12(a1,a7),x58471))), % 117.32/117.33 inference(scs_inference,[],[5823,5831,5825,41,37,42,5,8,11])). % 117.32/117.33 cnf(5849,plain, % 117.32/117.33 (E(f4(f11(f8(a1),f11(f8(a1),f12(a1,a7)))),f4(f12(a1,a7)))), % 117.32/117.33 inference(scs_inference,[],[5823,5831,5825,41,37,42,5,8,11,4,9])). % 117.32/117.33 cnf(5856,plain, % 117.32/117.33 (P4(f12(a1,f10(a1,a7)),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[5823,5831,5825,28,41,37,42,5,8,11,4,9,7,13,14,10,6,12,44])). % 117.32/117.33 cnf(5858,plain, % 117.32/117.33 (P4(f10(a1,f10(a1,a7)),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[5823,5831,5825,28,41,37,42,5,8,11,4,9,7,13,14,10,6,12,44,45])). % 117.32/117.33 cnf(5860,plain, % 117.32/117.33 (~E(f10(a1,f11(a7,f11(a7,a7))),f11(f8(a1),f12(a1,f6(a1))))), % 117.32/117.33 inference(scs_inference,[],[5823,5831,5825,5715,5604,28,41,37,42,5,8,11,4,9,7,13,14,10,6,12,44,45,3])). % 117.32/117.33 cnf(5864,plain, % 117.32/117.33 (~P7(f11(f8(a1),f11(f8(a1),f10(a1,a7))),a1)), % 117.32/117.33 inference(scs_inference,[],[5823,5831,5825,5680,5715,5604,33,31,28,41,37,42,5,8,11,4,9,7,13,14,10,6,12,44,45,3,17,24])). % 117.32/117.33 cnf(5875,plain, % 117.32/117.33 (P4(f11(f8(a1),f12(a1,a7)),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[5821,5843,3544,41,37,42])). % 117.32/117.33 cnf(5879,plain, % 117.32/117.33 (E(f12(x58791,f11(f8(a1),f11(f8(a1),f10(a1,a7)))),f12(x58791,f10(a1,a7)))), % 117.32/117.33 inference(scs_inference,[],[5821,5843,5839,3544,41,37,42,4,5,14])). % 117.32/117.33 cnf(5897,plain, % 117.32/117.33 (~P5(f11(f8(a1),f10(a1,a7)),a1)), % 117.32/117.33 inference(scs_inference,[],[5821,5843,5839,5690,5864,5860,5687,5549,3544,31,26,28,41,37,42,4,5,14,9,7,8,11,13,6,10,12,2,48,3,18,24,47])). % 117.32/117.33 cnf(5911,plain, % 117.32/117.33 (P4(f11(f8(a1),f11(f8(a1),f12(a1,a7))),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[5875,5856,1761,41,37,42])). % 117.32/117.33 cnf(5934,plain, % 117.32/117.33 (P4(x59341,f9(x59341))), % 117.32/117.33 inference(scs_inference,[],[5858,30,41,37])). % 117.32/117.33 cnf(5936,plain, % 117.32/117.33 (P4(f11(f8(a1),f10(a1,f10(a1,a7))),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[5858,30,41,37,42])). % 117.32/117.33 cnf(5941,plain, % 117.32/117.33 (E(f11(f11(f10(a1,a7),f11(f10(a1,a7),f10(a1,a7))),x59411),f11(f10(a1,a7),x59411))), % 117.32/117.33 inference(scs_inference,[],[5858,5672,30,41,37,42,5,4,9,11])). % 117.32/117.33 cnf(5948,plain, % 117.32/117.33 (E(f11(x59481,f11(f10(a1,a7),f11(f10(a1,a7),f10(a1,a7)))),f11(x59481,f10(a1,a7)))), % 117.32/117.33 inference(scs_inference,[],[5858,5672,30,41,37,42,5,4,9,11,7,8,13,14,6,10,12])). % 117.32/117.33 cnf(5949,plain, % 117.32/117.33 (P4(f12(a1,f10(a1,f10(a1,a7))),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[5858,5672,30,28,41,37,42,5,4,9,11,7,8,13,14,6,10,12,44])). % 117.32/117.33 cnf(5951,plain, % 117.32/117.33 (P4(f10(a1,f10(a1,f10(a1,a7))),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[5858,5672,30,28,41,37,42,5,4,9,11,7,8,13,14,6,10,12,44,45])). % 117.32/117.33 cnf(5956,plain, % 117.32/117.33 (~E(f9(f12(a1,f11(f8(a1),a7))),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[5858,5847,5672,5514,5549,30,28,41,37,42,5,4,9,11,7,8,13,14,6,10,12,44,45,3,18])). % 117.32/117.33 cnf(5957,plain, % 117.32/117.33 (~P7(f11(f11(f10(a1,a7),f11(f10(a1,a7),f10(a1,a7))),f11(f10(a1,a7),f10(a1,a7))),a1)), % 117.32/117.33 inference(scs_inference,[],[5858,5847,5672,5514,5690,5549,30,28,41,37,42,5,4,9,11,7,8,13,14,6,10,12,44,45,3,18,24])). % 117.32/117.33 cnf(5958,plain, % 117.32/117.33 (~E(f9(f8(a1)),f9(f12(a1,f11(f8(a1),a7))))), % 117.32/117.33 inference(scs_inference,[],[5858,5847,5672,5514,5690,5549,30,28,41,37,42,5,4,9,11,7,8,13,14,6,10,12,44,45,3,18,24,2])). % 117.32/117.33 cnf(5963,plain, % 117.32/117.33 (E(f11(x59631,f11(x59631,x59631)),x59631)), % 117.32/117.33 inference(scs_inference,[],[5934,41])). % 117.32/117.33 cnf(5965,plain, % 117.32/117.33 (P4(f11(x59651,x59651),f9(x59651))), % 117.32/117.33 inference(scs_inference,[],[5934,41,42])). % 117.32/117.33 cnf(5978,plain, % 117.32/117.33 (E(f11(f8(a2),f12(a2,f11(f8(a2),f8(a2)))),f10(a2,f8(a2)))), % 117.32/117.33 inference(scs_inference,[],[5934,5593,27,41,42,11,5,14,4,7,9,8,13,10,6,12,48])). % 117.32/117.33 cnf(5979,plain, % 117.32/117.33 (P4(x59791,f9(x59791))), % 117.32/117.33 inference(rename_variables,[],[5934])). % 117.32/117.33 cnf(5981,plain, % 117.32/117.33 (P4(f12(a2,f8(a2)),f9(f8(a2)))), % 117.32/117.33 inference(scs_inference,[],[5934,5979,5593,27,41,42,11,5,14,4,7,9,8,13,10,6,12,48,44])). % 117.32/117.33 cnf(5982,plain, % 117.32/117.33 (P4(x59821,f9(x59821))), % 117.32/117.33 inference(rename_variables,[],[5934])). % 117.32/117.33 cnf(5984,plain, % 117.32/117.33 (P4(f10(a2,f8(a2)),f9(f8(a2)))), % 117.32/117.33 inference(scs_inference,[],[5934,5979,5982,5593,27,41,42,11,5,14,4,7,9,8,13,10,6,12,48,44,45])). % 117.32/117.33 cnf(5992,plain, % 117.32/117.33 (~P5(f11(f8(a1),f11(f10(a1,a7),f11(f10(a1,a7),f10(a1,a7)))),a1)), % 117.32/117.33 inference(scs_inference,[],[5934,5979,5982,5705,5941,5948,5897,5593,5549,31,27,41,42,11,5,14,4,7,9,8,13,10,6,12,48,44,45,3,18,22])). % 117.32/117.33 cnf(6002,plain, % 117.32/117.33 (E(f11(x60021,f11(x60021,x60021)),x60021)), % 117.32/117.33 inference(rename_variables,[],[5963])). % 117.32/117.33 cnf(6007,plain, % 117.32/117.33 (P4(f11(x60071,f11(x60071,x60071)),f9(x60071))), % 117.32/117.33 inference(scs_inference,[],[5965,5963,5019,41,37,42])). % 117.32/117.33 cnf(6009,plain, % 117.32/117.33 (E(f10(f11(x60091,f11(x60091,x60091)),x60092),f10(x60091,x60092))), % 117.32/117.33 inference(scs_inference,[],[5965,5963,6002,5019,41,37,42,7])). % 117.32/117.33 cnf(6010,plain, % 117.32/117.33 (E(f11(f11(x60101,f11(x60101,x60101)),x60102),f11(x60101,x60102))), % 117.32/117.33 inference(scs_inference,[],[5965,5963,6002,5019,41,37,42,7,11])). % 117.32/117.33 cnf(6011,plain, % 117.32/117.33 (E(f8(f11(x60111,f11(x60111,x60111))),f8(x60111))), % 117.32/117.33 inference(scs_inference,[],[5965,5963,6002,5019,41,37,42,7,11,5])). % 117.32/117.33 cnf(6012,plain, % 117.32/117.33 (E(f6(f11(x60121,f11(x60121,x60121))),f6(x60121))), % 117.32/117.33 inference(scs_inference,[],[5965,5963,6002,5019,41,37,42,7,11,5,10])). % 117.32/117.33 cnf(6013,plain, % 117.32/117.33 (E(f4(f11(x60131,f11(x60131,x60131))),f4(x60131))), % 117.32/117.33 inference(scs_inference,[],[5965,5963,6002,5019,41,37,42,7,11,5,10,9])). % 117.32/117.33 cnf(6014,plain, % 117.32/117.33 (E(f12(x60141,f11(x60142,f11(x60142,x60142))),f12(x60141,x60142))), % 117.32/117.33 inference(scs_inference,[],[5965,5963,6002,5019,41,37,42,7,11,5,10,9,14])). % 117.32/117.33 cnf(6015,plain, % 117.32/117.33 (E(f10(x60151,f11(x60152,f11(x60152,x60152))),f10(x60151,x60152))), % 117.32/117.33 inference(scs_inference,[],[5965,5963,6002,5019,41,37,42,7,11,5,10,9,14,8])). % 117.32/117.33 cnf(6016,plain, % 117.32/117.33 (E(f5(f11(x60161,f11(x60161,x60161))),f5(x60161))), % 117.32/117.33 inference(scs_inference,[],[5965,5963,6002,5019,41,37,42,7,11,5,10,9,14,8,4])). % 117.32/117.33 cnf(6017,plain, % 117.32/117.33 (E(f12(f11(x60171,f11(x60171,x60171)),x60172),f12(x60171,x60172))), % 117.32/117.33 inference(scs_inference,[],[5965,5963,6002,5019,41,37,42,7,11,5,10,9,14,8,4,13])). % 117.32/117.33 cnf(6018,plain, % 117.32/117.33 (E(f9(f11(x60181,f11(x60181,x60181))),f9(x60181))), % 117.32/117.33 inference(scs_inference,[],[5965,5963,6002,5019,41,37,42,7,11,5,10,9,14,8,4,13,6])). % 117.32/117.33 cnf(6019,plain, % 117.32/117.33 (E(f11(x60191,f11(x60192,f11(x60192,x60192))),f11(x60191,x60192))), % 117.32/117.33 inference(scs_inference,[],[5965,5963,6002,5019,41,37,42,7,11,5,10,9,14,8,4,13,6,12])). % 117.32/117.33 cnf(6023,plain, % 117.32/117.33 (P4(f12(a1,f11(f8(a1),f8(a1))),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[5965,5963,6002,5934,28,5019,41,37,42,7,11,5,10,9,14,8,4,13,6,12,48,44])). % 117.32/117.33 cnf(6024,plain, % 117.32/117.33 (P4(f11(x60241,x60241),f9(x60241))), % 117.32/117.33 inference(rename_variables,[],[5965])). % 117.32/117.33 cnf(6026,plain, % 117.32/117.33 (P4(f10(a1,f11(f8(a1),f8(a1))),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[5965,6024,5963,6002,5934,28,5019,41,37,42,7,11,5,10,9,14,8,4,13,6,12,48,44,45])). % 117.32/117.33 cnf(6029,plain, % 117.32/117.33 (P6(a7,f11(f11(f8(a1),f11(f8(a1),a7)),f11(a7,a7)))), % 117.32/117.33 inference(scs_inference,[],[5965,6024,5963,6002,5934,3526,28,5019,41,37,42,7,11,5,10,9,14,8,4,13,6,12,48,44,45,20])). % 117.32/117.33 cnf(6045,plain, % 117.32/117.33 (P6(a7,f8(f11(a1,f11(a1,a1))))), % 117.32/117.33 inference(scs_inference,[],[6011,5019])). % 117.32/117.33 cnf(6046,plain, % 117.32/117.33 (E(f8(f11(x60461,f11(x60461,x60461))),f8(x60461))), % 117.32/117.33 inference(rename_variables,[],[6011])). % 117.32/117.33 cnf(6047,plain, % 117.32/117.33 (E(f11(x60471,f11(x60471,f11(x60471,f11(x60471,x60471)))),f11(x60471,f11(x60471,x60471)))), % 117.32/117.33 inference(scs_inference,[],[6007,6011,5019,41])). % 117.32/117.33 cnf(6051,plain, % 117.32/117.33 (P4(f11(x60511,f11(x60511,f11(x60511,x60511))),f9(x60511))), % 117.32/117.33 inference(scs_inference,[],[6007,6011,6029,5019,41,37,42])). % 117.32/117.33 cnf(6056,plain, % 117.32/117.33 (E(f11(f8(f11(x60561,f11(x60561,x60561))),x60562),f11(f8(x60561),x60562))), % 117.32/117.33 inference(scs_inference,[],[6007,6011,6046,6029,5019,41,37,42,5,7,8,11])). % 117.32/117.33 cnf(6065,plain, % 117.32/117.33 (P4(f11(x60651,f11(x60651,x60651)),f9(x60651))), % 117.32/117.33 inference(rename_variables,[],[6007])). % 117.32/117.33 cnf(6071,plain, % 117.32/117.33 (E(f11(x60711,f11(x60711,x60711)),x60711)), % 117.32/117.33 inference(rename_variables,[],[5963])). % 117.32/117.33 cnf(6074,plain, % 117.32/117.33 (E(f10(f11(x60741,f11(x60741,x60741)),f11(x60742,f11(x60742,x60742))),f10(x60741,x60742))), % 117.32/117.33 inference(scs_inference,[],[6007,6065,6011,6046,6009,6015,6029,5957,5992,5963,6071,27,5019,41,37,42,5,7,8,11,10,9,13,14,6,4,12,44,45,25,23,3])). % 117.32/117.33 cnf(6075,plain, % 117.32/117.33 (E(f10(f11(x60751,f11(x60751,x60751)),x60752),f10(x60751,x60752))), % 117.32/117.33 inference(rename_variables,[],[6009])). % 117.32/117.33 cnf(6078,plain, % 117.32/117.33 (~P7(f10(f11(a1,f11(a1,a1)),f11(f8(a1),f11(f8(a1),a7))),a1)), % 117.32/117.33 inference(scs_inference,[],[6007,6065,6011,6046,6009,6075,6015,6029,5957,5992,3066,5963,6071,5934,27,5019,41,37,42,5,7,8,11,10,9,13,14,6,4,12,44,45,25,23,3,17,24])). % 117.32/117.33 cnf(6094,plain, % 117.32/117.33 (P4(f11(f8(a2),f10(a2,f8(a2))),f9(f8(a2)))), % 117.32/117.33 inference(scs_inference,[],[5984,6045,41,37,42])). % 117.32/117.33 cnf(6107,plain, % 117.32/117.33 (P4(f12(a2,f10(a2,f8(a2))),f9(f8(a2)))), % 117.32/117.33 inference(scs_inference,[],[5984,6012,6045,27,41,37,42,5,7,8,9,10,13,11,6,14,4,12,44])). % 117.32/117.33 cnf(6109,plain, % 117.32/117.33 (P4(f10(a2,f10(a2,f8(a2))),f9(f8(a2)))), % 117.32/117.33 inference(scs_inference,[],[5984,6012,6045,27,41,37,42,5,7,8,9,10,13,11,6,14,4,12,44,45])). % 117.32/117.33 cnf(6111,plain, % 117.32/117.33 (~P5(f11(f8(a1),f10(a1,a7)),f11(a1,f11(a1,a1)))), % 117.32/117.33 inference(scs_inference,[],[5984,6012,6045,5897,5963,27,41,37,42,5,7,8,9,10,13,11,6,14,4,12,44,45,23])). % 117.32/117.33 cnf(6112,plain, % 117.32/117.33 (E(f11(x61121,f11(x61121,x61121)),x61121)), % 117.32/117.33 inference(rename_variables,[],[5963])). % 117.32/117.33 cnf(6115,plain, % 117.32/117.33 (~P7(f10(f11(a1,f11(a1,a1)),a7),a1)), % 117.32/117.33 inference(scs_inference,[],[5984,6012,6045,6078,5550,5897,5963,6112,2163,27,41,37,42,5,7,8,9,10,13,11,6,14,4,12,44,45,23,3,24])). % 117.32/117.33 cnf(6117,plain, % 117.32/117.33 (~E(f11(a7,f11(a7,a7)),f12(a1,f11(f8(a1),a7)))), % 117.32/117.33 inference(scs_inference,[],[5984,6012,6045,6078,5550,5897,5963,6112,2163,27,41,37,42,5,7,8,9,10,13,11,6,14,4,12,44,45,23,3,24,2])). % 117.32/117.33 cnf(6128,plain, % 117.32/117.33 (P4(f11(f8(a2),f12(a2,f8(a2))),f9(f8(a2)))), % 117.32/117.33 inference(scs_inference,[],[5981,41,42])). % 117.32/117.33 cnf(6141,plain, % 117.32/117.33 (P4(f12(a2,f12(a2,f8(a2))),f9(f8(a2)))), % 117.32/117.33 inference(scs_inference,[],[5981,6013,27,41,42,7,5,8,9,11,13,6,10,14,4,12,44])). % 117.32/117.33 cnf(6143,plain, % 117.32/117.33 (P4(f10(a2,f12(a2,f8(a2))),f9(f8(a2)))), % 117.32/117.33 inference(scs_inference,[],[5981,6013,27,41,42,7,5,8,9,11,13,6,10,14,4,12,44,45])). % 117.32/117.33 cnf(6145,plain, % 117.32/117.33 (~P7(f10(f11(a1,f11(a1,a1)),a7),f11(a1,f11(a1,a1)))), % 117.32/117.33 inference(scs_inference,[],[5981,6013,6115,5963,27,41,42,7,5,8,9,11,13,6,10,14,4,12,44,45,25])). % 117.32/117.33 cnf(6148,plain, % 117.32/117.33 (E(f11(x61481,f11(x61482,f11(x61482,x61482))),f11(x61481,x61482))), % 117.32/117.33 inference(rename_variables,[],[6019])). % 117.32/117.33 cnf(6149,plain, % 117.32/117.33 (E(f11(f8(f11(x61491,f11(x61491,x61491))),f11(x61492,f11(x61492,x61492))),f11(f8(x61491),x61492))), % 117.32/117.33 inference(scs_inference,[],[6111,5981,6013,6019,6148,6115,6056,5963,27,41,42,7,5,8,9,11,13,6,10,14,4,12,44,45,25,23,3])). % 117.32/117.33 cnf(6150,plain, % 117.32/117.33 (E(f11(f8(f11(x61501,f11(x61501,x61501))),x61502),f11(f8(x61501),x61502))), % 117.32/117.33 inference(rename_variables,[],[6056])). % 117.32/117.33 cnf(6154,plain, % 117.32/117.33 (~P7(f10(f11(a1,f11(a1,a1)),f11(a7,f11(a7,a7))),a1)), % 117.32/117.33 inference(scs_inference,[],[6111,5981,6013,6019,6148,6115,6074,6056,6150,5963,33,27,41,42,7,5,8,9,11,13,6,10,14,4,12,44,45,25,23,3,22,24])). % 117.32/117.33 cnf(6183,plain, % 117.32/117.33 (~P7(f10(a1,f11(f11(a7,f11(a7,a7)),f11(a7,a7))),f11(a1,f11(a1,a1)))), % 117.32/117.33 inference(scs_inference,[],[6051,6016,6145,5911,6015,5611,5963,5823,28,42,7,8,9,5,11,10,6,14,13,4,12,48,24,44,45,25])). % 117.32/117.33 cnf(6190,plain, % 117.32/117.33 (~E(f12(a1,f11(f8(a1),a7)),f11(f8(a1),f11(f8(a1),a7)))), % 117.32/117.33 inference(scs_inference,[],[6051,6016,6145,5911,6047,6117,6015,5611,5551,6111,5963,5823,31,28,42,7,8,9,5,11,10,6,14,13,4,12,48,24,44,45,25,23,3,18,2])). % 117.32/117.33 cnf(6209,plain, % 117.32/117.33 (~P7(f10(f11(a1,f11(a1,a1)),f11(f11(a7,f11(a7,a7)),f11(a7,a7))),f11(a1,f11(a1,a1)))), % 117.32/117.33 inference(scs_inference,[],[6014,6094,6183,6009,42,7,8,5,11,9,10,13,14,6,4,12,24])). % 117.32/117.33 cnf(6246,plain, % 117.32/117.33 (~P7(f10(f11(a1,f11(a1,a1)),f11(f11(a7,f11(a7,a7)),f11(a7,a7))),a1)), % 117.32/117.33 inference(scs_inference,[],[6128,6154,6017,5604,42,7,8,9,11,5,10,6,14,13,4,12,24])). % 117.32/117.33 cnf(6250,plain, % 117.32/117.33 (P6(f4(a7),f4(f11(f11(a7,f11(a7,a7)),f11(a7,a7))))), % 117.32/117.33 inference(scs_inference,[],[5711,6128,6154,6017,5604,30,27,42,7,8,9,11,5,10,6,14,13,4,12,24,44,20])). % 117.32/117.33 cnf(6254,plain, % 117.32/117.33 (~P7(f10(a1,a7),f11(a1,f11(a1,a1)))), % 117.32/117.33 inference(scs_inference,[],[33,5711,6128,6154,6017,5604,5963,30,27,42,7,8,9,11,5,10,6,14,13,4,12,24,44,20,45,25])). % 117.32/117.33 cnf(6257,plain, % 117.32/117.33 (E(f12(f11(x62571,f11(x62571,x62571)),x62572),f12(x62571,x62572))), % 117.32/117.33 inference(rename_variables,[],[6017])). % 117.32/117.33 cnf(6258,plain, % 117.32/117.33 (~P4(f12(f11(a1,f11(a1,a1)),f11(f8(a1),a7)),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[33,5711,6128,6154,5518,6017,6257,5604,5514,5963,30,27,42,7,8,9,11,5,10,6,14,13,4,12,24,44,20,45,25,3,17])). % 117.32/117.33 cnf(6260,plain, % 117.32/117.33 (~E(f4(a1),f12(f11(a1,f11(a1,a1)),f11(f8(a1),a7)))), % 117.32/117.33 inference(scs_inference,[],[33,5711,6128,6154,5518,6017,6257,5604,5514,5963,30,27,42,7,8,9,11,5,10,6,14,13,4,12,24,44,20,45,25,3,17,910])). % 117.32/117.33 cnf(6261,plain, % 117.32/117.33 (~E(f5(f9(f8(a1))),f12(f11(a1,f11(a1,a1)),f11(f8(a1),a7)))), % 117.32/117.33 inference(scs_inference,[],[33,5711,6128,6154,5518,6017,6257,5604,5514,5963,30,27,42,7,8,9,11,5,10,6,14,13,4,12,24,44,20,45,25,3,17,910,70])). % 117.32/117.33 cnf(6262,plain, % 117.32/117.33 (~E(a7,f12(f11(a1,f11(a1,a1)),f11(f8(a1),a7)))), % 117.32/117.33 inference(scs_inference,[],[33,5711,6128,6154,5518,6017,6257,5604,5514,5963,30,27,42,7,8,9,11,5,10,6,14,13,4,12,24,44,20,45,25,3,17,910,70,53])). % 117.32/117.33 cnf(6263,plain, % 117.32/117.33 (~E(f6(a1),f12(f11(a1,f11(a1,a1)),f11(f8(a1),a7)))), % 117.32/117.33 inference(scs_inference,[],[33,5711,6128,6154,5518,6017,6257,5604,5514,5963,30,27,42,7,8,9,11,5,10,6,14,13,4,12,24,44,20,45,25,3,17,910,70,53,955])). % 117.32/117.33 cnf(6284,plain, % 117.32/117.33 (E(f12(x62841,f11(x62842,f11(x62843,f11(x62843,x62843)))),f12(x62841,f11(x62842,x62843)))), % 117.32/117.33 inference(scs_inference,[],[6109,6250,6019,37,42,7,8,11,5,9,10,13,14])). % 117.32/117.33 cnf(6285,plain, % 117.32/117.33 (E(f5(f11(x62851,f11(x62852,f11(x62852,x62852)))),f5(f11(x62851,x62852)))), % 117.32/117.33 inference(scs_inference,[],[6109,6250,6019,37,42,7,8,11,5,9,10,13,14,4])). % 117.32/117.33 cnf(6287,plain, % 117.32/117.33 (E(f11(x62871,f11(x62872,f11(x62873,f11(x62873,x62873)))),f11(x62871,f11(x62872,x62873)))), % 117.32/117.33 inference(scs_inference,[],[6109,6250,6019,37,42,7,8,11,5,9,10,13,14,4,6,12])). % 117.32/117.33 cnf(6293,plain, % 117.32/117.33 (P6(f4(a7),f4(f11(a7,f11(a7,a7))))), % 117.32/117.33 inference(scs_inference,[],[6109,6026,6250,6260,5606,6019,28,37,42,7,8,11,5,9,10,13,14,4,6,12,2,44,45,21])). % 117.32/117.33 cnf(6310,plain, % 117.32/117.33 (E(f10(f11(f11(x63101,f11(x63101,x63101)),x63102),x63103),f10(f11(x63101,x63102),x63103))), % 117.32/117.33 inference(scs_inference,[],[6293,6143,6010,37,42,7])). % 117.32/117.33 cnf(6313,plain, % 117.32/117.33 (E(f11(f11(f11(x63131,f11(x63131,x63131)),x63132),x63133),f11(f11(x63131,x63132),x63133))), % 117.32/117.33 inference(scs_inference,[],[6293,6143,6010,37,42,7,8,5,11])). % 117.32/117.33 cnf(6316,plain, % 117.32/117.33 (E(f12(f11(f11(x63161,f11(x63161,x63161)),x63162),x63163),f12(f11(x63161,x63162),x63163))), % 117.32/117.33 inference(scs_inference,[],[6293,6143,6010,37,42,7,8,5,11,9,14,13])). % 117.32/117.33 cnf(6318,plain, % 117.32/117.33 (E(f5(f11(f11(x63181,f11(x63181,x63181)),x63182)),f5(f11(x63181,x63182)))), % 117.32/117.33 inference(scs_inference,[],[6293,6143,6010,37,42,7,8,5,11,9,14,13,10,4])). % 117.32/117.33 cnf(6320,plain, % 117.32/117.33 (E(f11(x63201,f11(f11(x63202,f11(x63202,x63202)),x63203)),f11(x63201,f11(x63202,x63203)))), % 117.32/117.33 inference(scs_inference,[],[6293,6143,6010,37,42,7,8,5,11,9,14,13,10,4,6,12])). % 117.32/117.33 cnf(6329,plain, % 117.32/117.33 (~P4(f12(a1,f11(f8(a1),f11(a7,f11(a7,a7)))),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[6293,6143,6263,6284,6287,6254,6010,5514,3067,27,37,42,7,8,5,11,9,14,13,10,4,6,12,2,44,45,25,3,17])). % 117.32/117.33 cnf(6340,plain, % 117.32/117.33 (~E(f4(a1),f12(a1,f11(f8(a1),f11(a7,f11(a7,a7)))))), % 117.32/117.33 inference(scs_inference,[],[6329,910])). % 117.32/117.33 cnf(6341,plain, % 117.32/117.33 (~E(a7,f12(a1,f11(f8(a1),f11(a7,f11(a7,a7)))))), % 117.32/117.33 inference(scs_inference,[],[6329,910,53])). % 117.32/117.33 cnf(6342,plain, % 117.32/117.33 (~E(f6(a1),f12(a1,f11(f8(a1),f11(a7,f11(a7,a7)))))), % 117.32/117.33 inference(scs_inference,[],[6329,910,53,955])). % 117.32/117.33 cnf(6348,plain, % 117.32/117.33 (E(f11(f10(x63481,f11(x63482,f11(x63482,x63482))),x63483),f11(f10(x63481,x63482),x63483))), % 117.32/117.33 inference(scs_inference,[],[6107,6329,6015,910,53,955,42,7,8,5,11])). % 117.32/117.33 cnf(6354,plain, % 117.32/117.33 (E(f9(f10(x63541,f11(x63542,f11(x63542,x63542)))),f9(f10(x63541,x63542)))), % 117.32/117.33 inference(scs_inference,[],[6107,6329,6015,910,53,955,42,7,8,5,11,9,14,10,13,4,6])). % 117.32/117.33 cnf(6355,plain, % 117.32/117.33 (E(f11(x63551,f10(x63552,f11(x63553,f11(x63553,x63553)))),f11(x63551,f10(x63552,x63553)))), % 117.32/117.33 inference(scs_inference,[],[6107,6329,6015,910,53,955,42,7,8,5,11,9,14,10,13,4,6,12])). % 117.32/117.33 cnf(6366,plain, % 117.32/117.33 (P4(f10(a7,f11(x63661,f11(x63661,x63661))),f9(f10(a7,x63661)))), % 117.32/117.33 inference(scs_inference,[],[5708,6107,5949,6262,6320,6329,6015,6111,5934,108,28,910,53,955,42,7,8,5,11,9,14,10,13,4,6,12,2,45,44,23,3,17,3566])). % 117.32/117.33 cnf(6378,plain, % 117.32/117.33 (E(f11(f10(f11(x63781,f11(x63781,x63781)),x63782),x63783),f11(f10(x63781,x63782),x63783))), % 117.32/117.33 inference(scs_inference,[],[6366,6009,42,7,5,8,11])). % 117.32/117.33 cnf(6385,plain, % 117.32/117.33 (E(f11(x63851,f10(f11(x63852,f11(x63852,x63852)),x63853)),f11(x63851,f10(x63852,x63853)))), % 117.32/117.33 inference(scs_inference,[],[6366,6009,42,7,5,8,11,14,9,10,13,4,6,12])). % 117.32/117.33 cnf(6387,plain, % 117.32/117.33 (~P7(f11(f10(a1,f11(a7,f11(a7,a7))),f11(f10(a1,a7),f10(a1,a7))),a1)), % 117.32/117.33 inference(scs_inference,[],[6366,6340,6348,5690,6009,42,7,5,8,11,14,9,10,13,4,6,12,2,24])). % 117.32/117.33 cnf(6395,plain, % 117.32/117.33 (~E(f12(a1,f11(f8(a1),a7)),f11(f11(a7,f11(a7,a7)),f11(a7,a7)))), % 117.32/117.33 inference(scs_inference,[],[6366,5951,5691,5827,6340,6348,6190,5612,5690,6009,28,42,7,5,8,11,14,9,10,13,4,6,12,2,24,45,44,18,3])). % 117.32/117.33 cnf(6399,plain, % 117.32/117.33 (~P5(f11(f8(a1),f10(a1,f11(a7,f11(a7,a7)))),a1)), % 117.32/117.33 inference(scs_inference,[],[6366,5951,5691,5827,6340,6348,6355,6190,5612,6149,5690,6009,5897,28,42,7,5,8,11,14,9,10,13,4,6,12,2,24,45,44,18,3,944,22])). % 117.32/117.33 cnf(6412,plain, % 117.32/117.33 (E(f5(f9(f11(x64121,f11(x64121,x64121)))),f5(f9(x64121)))), % 117.32/117.33 inference(scs_inference,[],[6141,6018,42,7,5,11,8,9,14,4])). % 117.32/117.33 cnf(6428,plain, % 117.32/117.33 (P4(f11(a7,a7),f9(f11(f11(a7,f11(a7,a7)),f11(a7,a7))))), % 117.32/117.33 inference(scs_inference,[],[6141,6395,6246,5798,6399,6310,6385,5965,6018,5963,27,42,7,5,11,8,9,14,4,10,13,6,12,2,24,44,45,23,22,17])). % 117.32/117.33 cnf(6443,plain, % 117.32/117.33 (E(f12(x64431,f11(f8(a1),f11(f8(a1),f4(a1)))),f12(x64431,f4(a1)))), % 117.32/117.33 inference(scs_inference,[],[6428,111,4279,41,42,7,5,8,11,14])). % 117.32/117.33 cnf(6446,plain, % 117.32/117.33 (E(f12(f11(f8(a1),f11(f8(a1),a7)),x64461),f12(a7,x64461))), % 117.32/117.33 inference(scs_inference,[],[6428,111,4279,41,42,7,5,8,11,14,4,9,13])). % 117.32/117.33 cnf(6453,plain, % 117.32/117.33 (P6(f5(a7),f5(f11(f11(a7,f11(a7,a7)),f11(a7,a7))))), % 117.32/117.33 inference(scs_inference,[],[5710,6428,6387,6342,6378,30,111,4279,41,42,7,5,8,11,14,4,9,13,10,6,12,2,24,20])). % 117.32/117.33 cnf(6475,plain, % 117.32/117.33 (E(f11(a7,x64751),f11(f11(f8(a1),f11(f8(a1),a7)),x64751))), % 117.32/117.33 inference(scs_inference,[],[6453,6023,108,3067,37,42,7,5,8,9,10,13,11])). % 117.32/117.33 cnf(6483,plain, % 117.32/117.33 (P6(f5(a7),f5(f11(a7,f11(a7,a7))))), % 117.32/117.33 inference(scs_inference,[],[6453,6209,6341,6318,6023,6310,108,3067,37,42,7,5,8,9,10,13,11,14,4,6,12,2,24,21])). % 117.32/117.33 cnf(6485,plain, % 117.32/117.33 (E(f12(f11(f8(a1),f11(f8(a1),a7)),f11(f11(a7,f11(a7,a7)),f11(a7,a7))),f12(a7,a7))), % 117.32/117.33 inference(scs_inference,[],[6453,6446,6209,6341,6318,5709,6023,6310,108,3067,37,42,7,5,8,9,10,13,11,14,4,6,12,2,24,21,3])). % 117.32/117.33 cnf(6500,plain, % 117.32/117.33 (E(f10(x65001,f11(f8(a1),f11(f8(a1),f6(a1)))),f10(x65001,f6(a1)))), % 117.32/117.33 inference(scs_inference,[],[6483,5856,3074,37,42,7,5,8])). % 117.32/117.33 cnf(6604,plain, % 117.32/117.33 (P4(f11(f8(a1),f11(f8(a1),f10(a1,a7))),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[6261,5843,2,42])). % 117.32/117.33 cnf(6622,plain, % 117.32/117.33 (~P7(f11(f8(a1),f11(f8(a1),f10(a1,a7))),f11(a1,f11(a1,a1)))), % 117.32/117.33 inference(scs_inference,[],[6604,5864,5963,28,42,45,44,25])). % 117.32/117.33 cnf(6624,plain, % 117.32/117.33 (P5(f12(a1,f11(f8(a1),f11(f8(a1),f10(a1,a7)))),a1)), % 117.32/117.33 inference(scs_inference,[],[6604,5864,5963,26,28,42,45,44,25,43])). % 117.32/117.33 cnf(6636,plain, % 117.32/117.33 (~P7(f11(f8(a1),f11(f8(a1),f10(a1,a7))),f11(f11(a1,f11(a1,a1)),f11(a1,a1)))), % 117.32/117.33 inference(scs_inference,[],[6622,5911,6010,42,25])). % 117.32/117.33 cnf(6649,plain, % 117.32/117.33 (P4(f5(f11(a7,x66491)),f11(f11(f8(a1),f11(f8(a1),a7)),x66491))), % 117.32/117.33 inference(scs_inference,[],[6475,5936,31,42,18])). % 117.32/117.33 cnf(6651,plain, % 117.32/117.33 (~P7(f11(f10(a1,a7),f11(f10(a1,a7),f10(a1,a7))),f11(a1,f11(a1,a1)))), % 117.32/117.33 inference(scs_inference,[],[6475,5936,5690,5963,31,42,18,25])). % 117.32/117.33 cnf(6669,plain, % 117.32/117.33 (~E(f10(f11(a1,f11(a1,a1)),f11(a7,f11(a7,a7))),f11(f8(a1),f12(a1,f6(a1))))), % 117.32/117.33 inference(scs_inference,[],[6636,6285,6649,6074,6313,4127,4921,42,17,25,3,2])). % 117.32/117.33 cnf(6686,plain, % 117.32/117.33 (P6(f12(a7,f11(f11(a7,f11(a7,a7)),f11(a7,a7))),f12(a7,a7))), % 117.32/117.33 inference(scs_inference,[],[6651,5750,3536,6669,6485,6378,4885,30,6015,42,20,24,3,2,25,21])). % 117.32/117.33 cnf(6696,plain, % 117.32/117.33 (P5(f12(a1,f10(a1,a7)),a1)), % 117.32/117.33 inference(scs_inference,[],[6686,6624,5879,31,37,42,22])). % 117.32/117.33 cnf(6726,plain, % 117.32/117.33 (~P4(f12(f11(f11(a1,f11(a1,a1)),f11(a1,a1)),f11(f8(a1),a7)),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[6316,4082,6258,3065,6013,26,28,3,2,47,17])). % 117.32/117.33 cnf(7048,plain, % 117.32/117.33 (P7(f11(f8(a1),f12(a1,f4(a1))),a1)+~P4(f12(a1,f4(a1)),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[906,26,28,47])). % 117.32/117.33 cnf(7053,plain, % 117.32/117.33 (P4(f12(a1,f11(f8(a1),f10(a1,a7))),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[5843,28,44])). % 117.32/117.33 cnf(7091,plain, % 117.32/117.33 (P4(f10(a1,f6(a1)),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[5849,6500,5554,3,17])). % 117.32/117.33 cnf(7105,plain, % 117.32/117.33 (P4(f12(a1,f10(a1,f6(a1))),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[7091,28,41,42,44])). % 117.32/117.33 cnf(7109,plain, % 117.32/117.33 (P5(f12(a1,f10(a1,f6(a1))),a1)), % 117.32/117.33 inference(scs_inference,[],[7091,26,28,41,42,44,45,43])). % 117.32/117.33 cnf(7146,plain, % 117.32/117.33 (P7(f11(f8(a1),f12(a1,f4(a1))),a1)), % 117.32/117.33 inference(scs_inference,[],[7109,7105,5978,5580,6443,26,28,42,44,45,43,3,17,47,7048])). % 117.32/117.33 cnf(7217,plain, % 117.32/117.33 (~E(f12(a1,f6(a1)),f12(a1,f11(f8(a1),f11(a7,f11(a7,a7)))))), % 117.32/117.33 inference(scs_inference,[],[6010,5963,6019,6016,7105,6726,5897,6329,5514,6354,5956,93,6,92,77,2,37,81,70,38,4094,4357,4358,4132,4941,4834,4838,4894,4898,4355,4202,4090,4130,3712,3527,3557,78,969,3091,4304,3124,887,929,123,67,393,4135])). % 117.32/117.33 cnf(7236,plain, % 117.32/117.33 (~P4(f11(a7,f11(a7,a7)),f9(f8(a1)))), % 117.32/117.33 inference(scs_inference,[],[26,28,108,33,30,6010,5963,6018,6019,6016,7105,5843,897,5965,7053,6726,5897,6329,5514,6412,7146,6696,6029,6354,5956,93,6,92,77,2,37,81,70,38,4094,4357,4358,4132,4941,4834,4838,4894,4898,4355,4202,4090,4130,3712,3527,3557,78,969,3091,4304,3124,887,929,123,67,393,4135,958,80,22,18,44,24,21,20,17,3,43,47,42])). % 117.32/117.33 cnf(7256,plain, % 117.32/117.33 ($false), % 117.32/117.33 inference(scs_inference,[],[2637,327,5963,6329,7236,7217,5958,93,6,14,92,77,2,37,81,53]), % 117.32/117.33 ['proof']). % 117.32/117.33 % SZS output end Proof % 117.32/117.33 % Total time :116.650000s %------------------------------------------------------------------------------