%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU198+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 : 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:01:42 EDT 2024 % Result : Theorem 117.84s 117.98s % Output : CNFRefutation 117.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SEU198+1 : TPTP v8.2.0. Released v3.3.0. % 0.00/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n026.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Fri Jun 21 15:18:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.20/0.56 start to proof:theBenchmark % 117.84/117.96 %------------------------------------------- % 117.84/117.96 % File :CSE---1.7 % 117.84/117.96 % Problem :theBenchmark % 117.84/117.96 % Transform :cnf % 117.84/117.96 % Format :tptp:raw % 117.84/117.96 % Command :java -jar mcs_scs.jar %d %s % 117.84/117.96 % 117.84/117.96 % Result :Theorem 117.300000s % 117.84/117.96 % Output :CNFRefutation 117.300000s % 117.84/117.96 %------------------------------------------- % 117.84/117.97 %------------------------------------------------------------------------------ % 117.84/117.97 % File : SEU198+1 : TPTP v8.2.0. Released v3.3.0. % 117.84/117.97 % Domain : Set theory % 117.84/117.97 % Problem : MPTP bushy problem t116_relat_1 % 117.84/117.97 % Version : [Urb07] axioms : Especial. % 117.84/117.97 % English : % 117.84/117.97 % 117.84/117.97 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 117.84/117.97 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 117.84/117.97 % Source : [Urb07] % 117.84/117.97 % Names : bushy-t116_relat_1 [Urb07] % 117.84/117.97 % 117.84/117.97 % Status : Theorem % 117.84/117.97 % Rating : 0.14 v8.1.0, 0.11 v7.5.0, 0.12 v7.4.0, 0.13 v7.3.0, 0.14 v7.2.0, 0.10 v7.1.0, 0.09 v7.0.0, 0.13 v6.4.0, 0.19 v6.3.0, 0.12 v6.1.0, 0.23 v6.0.0, 0.26 v5.4.0, 0.32 v5.3.0, 0.33 v5.2.0, 0.20 v5.1.0, 0.24 v5.0.0, 0.21 v4.1.0, 0.22 v4.0.0, 0.25 v3.7.0, 0.10 v3.5.0, 0.11 v3.4.0, 0.16 v3.3.0 % 117.84/117.97 % Syntax : Number of formulae : 31 ( 10 unt; 0 def) % 117.84/117.97 % Number of atoms : 62 ( 2 equ) % 117.84/117.97 % Maximal formula atoms : 4 ( 2 avg) % 117.84/117.97 % Number of connectives : 43 ( 12 ~; 1 |; 14 &) % 117.84/117.97 % ( 3 <=>; 13 =>; 0 <=; 0 <~>) % 117.84/117.97 % Maximal formula depth : 7 ( 4 avg) % 117.84/117.97 % Maximal term depth : 3 ( 1 avg) % 117.84/117.97 % Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty) % 117.84/117.97 % Number of functors : 4 ( 4 usr; 1 con; 0-2 aty) % 117.84/117.97 % Number of variables : 45 ( 38 !; 7 ?) % 117.84/117.97 % SPC : FOF_THM_RFO_SEQ % 117.84/117.97 % 117.84/117.97 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 117.84/117.97 % library, www.mizar.org % 117.84/117.97 %------------------------------------------------------------------------------ % 117.84/117.97 fof(antisymmetry_r2_hidden,axiom, % 117.84/117.97 ! [A,B] : % 117.84/117.97 ( in(A,B) % 117.84/117.97 => ~ in(B,A) ) ). % 117.84/117.97 % 117.84/117.97 fof(cc1_relat_1,axiom, % 117.84/117.97 ! [A] : % 117.84/117.97 ( empty(A) % 117.84/117.97 => relation(A) ) ). % 117.84/117.97 % 117.84/117.97 fof(d3_tarski,axiom, % 117.84/117.97 ! [A,B] : % 117.84/117.97 ( subset(A,B) % 117.84/117.97 <=> ! [C] : % 117.84/117.97 ( in(C,A) % 117.84/117.97 => in(C,B) ) ) ). % 117.84/117.97 % 117.84/117.97 fof(dt_k1_xboole_0,axiom, % 117.84/117.97 $true ). % 117.84/117.97 % 117.84/117.97 fof(dt_k1_zfmisc_1,axiom, % 117.84/117.97 $true ). % 117.84/117.97 % 117.84/117.97 fof(dt_k2_relat_1,axiom, % 117.84/117.97 $true ). % 117.84/117.97 % 117.84/117.97 fof(dt_k8_relat_1,axiom, % 117.84/117.97 ! [A,B] : % 117.84/117.97 ( relation(B) % 117.84/117.97 => relation(relation_rng_restriction(A,B)) ) ). % 117.84/117.97 % 117.84/117.97 fof(dt_m1_subset_1,axiom, % 117.84/117.97 $true ). % 117.84/117.97 % 117.84/117.97 fof(existence_m1_subset_1,axiom, % 117.84/117.97 ! [A] : % 117.84/117.97 ? [B] : element(B,A) ). % 117.84/117.97 % 117.84/117.97 fof(fc1_subset_1,axiom, % 117.84/117.97 ! [A] : ~ empty(powerset(A)) ). % 117.84/117.97 % 117.84/117.97 fof(fc1_xboole_0,axiom, % 117.84/117.97 empty(empty_set) ). % 117.84/117.97 % 117.84/117.97 fof(fc4_relat_1,axiom, % 117.84/117.97 ( empty(empty_set) % 117.84/117.97 & relation(empty_set) ) ). % 117.84/117.97 % 117.84/117.97 fof(fc6_relat_1,axiom, % 117.84/117.97 ! [A] : % 117.84/117.97 ( ( ~ empty(A) % 117.84/117.97 & relation(A) ) % 117.84/117.97 => ~ empty(relation_rng(A)) ) ). % 117.84/117.97 % 117.84/117.97 fof(fc8_relat_1,axiom, % 117.84/117.97 ! [A] : % 117.84/117.97 ( empty(A) % 117.84/117.97 => ( empty(relation_rng(A)) % 117.84/117.97 & relation(relation_rng(A)) ) ) ). % 117.84/117.97 % 117.84/117.97 fof(rc1_relat_1,axiom, % 117.84/117.97 ? [A] : % 117.84/117.97 ( empty(A) % 117.84/117.97 & relation(A) ) ). % 117.84/117.97 % 117.84/117.97 fof(rc1_subset_1,axiom, % 117.84/117.97 ! [A] : % 117.84/117.97 ( ~ empty(A) % 117.84/117.97 => ? [B] : % 117.84/117.97 ( element(B,powerset(A)) % 117.84/117.97 & ~ empty(B) ) ) ). % 117.84/117.97 % 117.84/117.97 fof(rc1_xboole_0,axiom, % 117.84/117.97 ? [A] : empty(A) ). % 117.84/117.97 % 117.84/117.97 fof(rc2_relat_1,axiom, % 117.84/117.97 ? [A] : % 117.84/117.97 ( ~ empty(A) % 117.84/117.97 & relation(A) ) ). % 117.84/117.97 % 117.84/117.97 fof(rc2_subset_1,axiom, % 117.84/117.97 ! [A] : % 117.84/117.97 ? [B] : % 117.84/117.97 ( element(B,powerset(A)) % 117.84/117.97 & empty(B) ) ). % 117.84/117.97 % 117.84/117.97 fof(rc2_xboole_0,axiom, % 117.84/117.97 ? [A] : ~ empty(A) ). % 117.84/117.97 % 117.84/117.97 fof(reflexivity_r1_tarski,axiom, % 117.84/117.97 ! [A,B] : subset(A,A) ). % 117.84/117.97 % 117.84/117.97 fof(t115_relat_1,axiom, % 117.84/117.97 ! [A,B,C] : % 117.84/117.97 ( relation(C) % 117.84/117.97 => ( in(A,relation_rng(relation_rng_restriction(B,C))) % 117.84/117.97 <=> ( in(A,B) % 117.84/117.97 & in(A,relation_rng(C)) ) ) ) ). % 117.84/117.97 % 117.84/117.97 fof(t116_relat_1,conjecture, % 117.84/117.97 ! [A,B] : % 117.84/117.98 ( relation(B) % 117.84/117.98 => subset(relation_rng(relation_rng_restriction(A,B)),A) ) ). % 117.84/117.98 % 117.84/117.98 fof(t1_subset,axiom, % 117.84/117.98 ! [A,B] : % 117.84/117.98 ( in(A,B) % 117.84/117.98 => element(A,B) ) ). % 117.84/117.98 % 117.84/117.98 fof(t2_subset,axiom, % 117.84/117.98 ! [A,B] : % 117.84/117.98 ( element(A,B) % 117.84/117.98 => ( empty(B) % 117.84/117.98 | in(A,B) ) ) ). % 117.84/117.98 % 117.84/117.98 fof(t3_subset,axiom, % 117.84/117.98 ! [A,B] : % 117.84/117.98 ( element(A,powerset(B)) % 117.84/117.98 <=> subset(A,B) ) ). % 117.84/117.98 % 117.84/117.98 fof(t4_subset,axiom, % 117.84/117.98 ! [A,B,C] : % 117.84/117.98 ( ( in(A,B) % 117.84/117.98 & element(B,powerset(C)) ) % 117.84/117.98 => element(A,C) ) ). % 117.84/117.98 % 117.84/117.98 fof(t5_subset,axiom, % 117.84/117.98 ! [A,B,C] : % 117.84/117.98 ~ ( in(A,B) % 117.84/117.98 & element(B,powerset(C)) % 117.84/117.98 & empty(C) ) ). % 117.84/117.98 % 117.84/117.98 fof(t6_boole,axiom, % 117.84/117.98 ! [A] : % 117.84/117.98 ( empty(A) % 117.84/117.98 => A = empty_set ) ). % 117.84/117.98 % 117.84/117.98 fof(t7_boole,axiom, % 117.84/117.98 ! [A,B] : % 117.84/117.98 ~ ( in(A,B) % 117.84/117.98 & empty(B) ) ). % 117.84/117.98 % 117.84/117.98 fof(t8_boole,axiom, % 117.84/117.98 ! [A,B] : % 117.84/117.98 ~ ( empty(A) % 117.84/117.98 & A != B % 117.84/117.98 & empty(B) ) ). % 117.84/117.98 % 117.84/117.98 %------------------------------------------------------------------------------ % 117.84/117.98 %------------------------------------------- % 117.84/117.98 % Proof found % 117.84/117.98 % SZS status Theorem for theBenchmark % 117.84/117.98 % SZS output start Proof % 117.94/117.99 %ClaNum:59(EqnAxiom:20) % 117.94/117.99 %VarNum:102(SingletonVarNum:50) % 117.94/117.99 %MaxLitNum:4 % 117.94/117.99 %MaxfuncDepth:2 % 117.94/117.99 %SharedTerms:19 % 117.94/117.99 %goalClause: 28 36 % 117.94/117.99 %singleGoalClaCount:2 % 117.94/117.99 [22]P1(a1) % 117.94/117.99 [23]P1(a2) % 117.94/117.99 [24]P1(a6) % 117.94/117.99 [25]P3(a1) % 117.94/117.99 [26]P3(a2) % 117.94/117.99 [27]P3(a8) % 117.94/117.99 [28]P3(a3) % 117.94/117.99 [33]~P1(a8) % 117.94/117.99 [34]~P1(a11) % 117.94/117.99 [36]~P5(f14(f13(a12,a3)),a12) % 117.94/117.99 [30]P5(x301,x301) % 117.94/117.99 [29]P1(f9(x291)) % 117.94/117.99 [31]P2(f4(x311),x311) % 117.94/117.99 [32]P2(f9(x321),f10(x321)) % 117.94/117.99 [35]~P1(f10(x351)) % 117.94/117.99 [37]~P1(x371)+E(x371,a1) % 117.94/117.99 [38]~P1(x381)+P3(x381) % 117.94/117.99 [40]~P1(x401)+P1(f14(x401)) % 117.94/117.99 [41]~P1(x411)+P3(f14(x411)) % 117.94/117.99 [42]P1(x421)+~P1(f7(x421)) % 117.94/117.99 [45]P1(x451)+P2(f7(x451),f10(x451)) % 117.94/117.99 [44]~P1(x441)+~P4(x442,x441) % 117.94/117.99 [46]~P4(x461,x462)+P2(x461,x462) % 117.94/117.99 [50]~P4(x502,x501)+~P4(x501,x502) % 117.94/117.99 [47]~P3(x472)+P3(f13(x471,x472)) % 117.94/117.99 [49]~P5(x491,x492)+P2(x491,f10(x492)) % 117.94/117.99 [51]P5(x511,x512)+~P2(x511,f10(x512)) % 117.94/117.99 [52]P5(x521,x522)+P4(f5(x521,x522),x521) % 117.94/117.99 [56]P5(x561,x562)+~P4(f5(x561,x562),x562) % 117.94/117.99 [43]~P3(x431)+P1(x431)+~P1(f14(x431)) % 117.94/117.99 [39]~P1(x392)+~P1(x391)+E(x391,x392) % 117.94/117.99 [48]~P2(x482,x481)+P1(x481)+P4(x482,x481) % 117.94/117.99 [53]~P5(x533,x532)+P4(x531,x532)+~P4(x531,x533) % 117.94/117.99 [54]~P1(x541)+~P4(x542,x543)+~P2(x543,f10(x541)) % 117.94/117.99 [55]P2(x551,x552)+~P4(x551,x553)+~P2(x553,f10(x552)) % 117.94/117.99 [58]P4(x581,x582)+~P3(x583)+~P4(x581,f14(f13(x582,x583))) % 117.94/117.99 [59]~P3(x592)+P4(x591,f14(x592))+~P4(x591,f14(f13(x593,x592))) % 117.94/117.99 [57]~P3(x573)+~P4(x571,x572)+~P4(x571,f14(x573))+P4(x571,f14(f13(x572,x573))) % 117.94/117.99 %EqnAxiom % 117.94/117.99 [1]E(x11,x11) % 117.94/117.99 [2]E(x22,x21)+~E(x21,x22) % 117.94/117.99 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 117.94/117.99 [4]~E(x41,x42)+E(f9(x41),f9(x42)) % 117.94/117.99 [5]~E(x51,x52)+E(f4(x51),f4(x52)) % 117.94/117.99 [6]~E(x61,x62)+E(f14(x61),f14(x62)) % 117.94/117.99 [7]~E(x71,x72)+E(f10(x71),f10(x72)) % 117.94/117.99 [8]~E(x81,x82)+E(f5(x81,x83),f5(x82,x83)) % 117.94/117.99 [9]~E(x91,x92)+E(f5(x93,x91),f5(x93,x92)) % 117.94/117.99 [10]~E(x101,x102)+E(f13(x101,x103),f13(x102,x103)) % 117.94/117.99 [11]~E(x111,x112)+E(f13(x113,x111),f13(x113,x112)) % 117.94/117.99 [12]~E(x121,x122)+E(f7(x121),f7(x122)) % 117.94/117.99 [13]~P1(x131)+P1(x132)+~E(x131,x132) % 117.94/117.99 [14]P4(x142,x143)+~E(x141,x142)+~P4(x141,x143) % 117.94/117.99 [15]P4(x153,x152)+~E(x151,x152)+~P4(x153,x151) % 117.94/117.99 [16]~P3(x161)+P3(x162)+~E(x161,x162) % 117.94/117.99 [17]P5(x172,x173)+~E(x171,x172)+~P5(x171,x173) % 117.94/117.99 [18]P5(x183,x182)+~E(x181,x182)+~P5(x183,x181) % 117.94/117.99 [19]P2(x192,x193)+~E(x191,x192)+~P2(x191,x193) % 117.94/117.99 [20]P2(x203,x202)+~E(x201,x202)+~P2(x203,x201) % 117.94/117.99 % 117.94/117.99 %------------------------------------------- % 117.94/118.01 cnf(60,plain, % 117.94/118.01 (P5(f4(f10(x601)),x601)), % 117.94/118.01 inference(scs_inference,[],[31,51])). % 117.94/118.01 cnf(61,plain, % 117.94/118.01 (P2(f4(x611),x611)), % 117.94/118.01 inference(rename_variables,[],[31])). % 117.94/118.01 cnf(63,plain, % 117.94/118.01 (~P4(x631,a1)), % 117.94/118.01 inference(scs_inference,[],[31,22,51,44])). % 117.94/118.01 cnf(66,plain, % 117.94/118.01 (P5(x661,x661)), % 117.94/118.01 inference(rename_variables,[],[30])). % 117.94/118.01 cnf(69,plain, % 117.94/118.01 (P4(f4(a8),a8)), % 117.94/118.01 inference(scs_inference,[],[36,30,66,31,61,22,33,51,44,17,18,48])). % 117.94/118.01 cnf(70,plain, % 117.94/118.01 (P2(f4(x701),x701)), % 117.94/118.01 inference(rename_variables,[],[31])). % 117.94/118.01 cnf(72,plain, % 117.94/118.01 (~P4(x721,f4(f10(a1)))), % 117.94/118.01 inference(scs_inference,[],[36,30,66,31,61,70,22,33,51,44,17,18,48,54])). % 117.94/118.01 cnf(75,plain, % 117.94/118.01 (~E(a8,a1)), % 117.94/118.01 inference(scs_inference,[],[36,30,66,31,61,70,22,33,51,44,17,18,48,54,15])). % 117.94/118.01 cnf(87,plain, % 117.94/118.01 (P5(f9(x871),x871)), % 117.94/118.01 inference(scs_inference,[],[32,51])). % 117.94/118.01 cnf(89,plain, % 117.94/118.01 (~P4(x891,a2)), % 117.94/118.01 inference(scs_inference,[],[32,23,51,44])). % 117.94/118.01 cnf(91,plain, % 117.94/118.01 (P5(a1,x911)), % 117.94/118.01 inference(scs_inference,[],[63,32,23,51,44,52])). % 117.94/118.01 cnf(94,plain, % 117.94/118.01 (P4(f4(a11),a11)), % 117.94/118.01 inference(scs_inference,[],[63,32,23,34,31,51,44,52,48])). % 117.94/118.01 cnf(97,plain, % 117.94/118.01 (~P4(x971,f9(a2))), % 117.94/118.01 inference(scs_inference,[],[63,32,23,34,31,51,44,52,48,54])). % 117.94/118.01 cnf(98,plain, % 117.94/118.01 (P2(f9(x981),f10(x981))), % 117.94/118.01 inference(rename_variables,[],[32])). % 117.94/118.01 cnf(106,plain, % 117.94/118.01 (P2(x1061,f10(x1062))+~E(f9(x1062),x1061)), % 117.94/118.01 inference(scs_inference,[],[36,60,72,63,32,98,69,23,34,31,51,44,52,48,54,15,17,50,19])). % 117.94/118.01 cnf(112,plain, % 117.94/118.01 (~P4(x1121,f9(a2))), % 117.94/118.01 inference(rename_variables,[],[97])). % 117.94/118.01 cnf(114,plain, % 117.94/118.01 (~P4(x1141,a6)), % 117.94/118.01 inference(scs_inference,[],[97,24,52,44])). % 117.94/118.01 cnf(116,plain, % 117.94/118.01 (~P4(x1161,f4(f10(a6)))), % 117.94/118.01 inference(scs_inference,[],[97,24,31,52,44,54])). % 117.94/118.01 cnf(117,plain, % 117.94/118.01 (P2(f4(x1171),x1171)), % 117.94/118.01 inference(rename_variables,[],[31])). % 117.94/118.01 cnf(119,plain, % 117.94/118.01 (P4(f4(f10(x1191)),f10(x1191))), % 117.94/118.01 inference(scs_inference,[],[97,24,35,31,117,52,44,54,48])). % 117.94/118.01 cnf(120,plain, % 117.94/118.01 (P2(f4(x1201),x1201)), % 117.94/118.01 inference(rename_variables,[],[31])). % 117.94/118.01 cnf(126,plain, % 117.94/118.01 (~P1(f14(f13(a12,a3)))), % 117.94/118.01 inference(scs_inference,[],[36,87,97,112,94,24,29,35,31,117,52,44,54,48,17,15,39])). % 117.94/118.01 cnf(129,plain, % 117.94/118.01 (~P1(f13(a12,a3))), % 117.94/118.01 inference(scs_inference,[],[36,87,97,112,94,24,29,35,31,117,52,44,54,48,17,15,39,40])). % 117.94/118.01 cnf(133,plain, % 117.94/118.01 (P2(x1331,x1332)+~E(f4(x1332),x1331)), % 117.94/118.01 inference(scs_inference,[],[36,87,97,112,94,24,29,35,31,117,120,52,44,54,48,17,15,39,40,50,19])). % 117.94/118.01 cnf(144,plain, % 117.94/118.01 (~P4(x1441,f9(x1442))), % 117.94/118.01 inference(scs_inference,[],[116,29,52,44])). % 117.94/118.01 cnf(146,plain, % 117.94/118.01 (P4(f4(f13(a12,a3)),f13(a12,a3))), % 117.94/118.01 inference(scs_inference,[],[116,129,29,31,52,44,48])). % 117.94/118.01 cnf(163,plain, % 117.94/118.01 (P4(f9(x1631),f10(x1631))), % 117.94/118.01 inference(scs_inference,[],[32,144,35,52,48])). % 117.94/118.01 cnf(177,plain, % 117.94/118.01 (P5(a2,x1771)), % 117.94/118.01 inference(scs_inference,[],[89,52])). % 117.94/118.01 cnf(191,plain, % 117.94/118.01 (P5(a6,x1911)), % 117.94/118.01 inference(scs_inference,[],[114,52])). % 117.94/118.01 cnf(192,plain, % 117.94/118.01 (~P4(x1921,a6)), % 117.94/118.01 inference(rename_variables,[],[114])). % 117.94/118.01 cnf(199,plain, % 117.94/118.01 (P5(x1991,a8)+~E(f4(a8),f5(x1991,a8))), % 117.94/118.01 inference(scs_inference,[],[36,91,146,69,114,192,52,15,17,14,56])). % 117.94/118.01 cnf(201,plain, % 117.94/118.01 (~P4(a8,f5(x2011,a8))+~E(f4(a8),f5(x2011,a8))), % 117.94/118.01 inference(scs_inference,[],[36,91,146,69,114,192,52,15,17,14,56,50])). % 117.94/118.01 cnf(209,plain, % 117.94/118.01 (P4(x2091,a11)+~E(f4(a11),x2091)), % 117.94/118.01 inference(scs_inference,[],[36,177,119,94,144,15,17,14])). % 117.94/118.01 cnf(220,plain, % 117.94/118.01 (P4(x2201,f10(x2202))+~E(f9(x2202),x2201)), % 117.94/118.01 inference(scs_inference,[],[36,191,146,163,72,15,17,14])). % 117.94/118.01 cnf(221,plain, % 117.94/118.01 (P5(x2211,f10(x2212))+~E(f9(x2212),f5(x2211,f10(x2212)))), % 117.94/118.01 inference(scs_inference,[],[36,191,146,163,72,15,17,14,56])). % 117.94/118.01 cnf(235,plain, % 117.94/118.01 (P2(f4(x2351),x2352)+~E(x2351,x2352)), % 117.94/118.01 inference(scs_inference,[],[31,119,63,15,20])). % 117.94/118.01 cnf(238,plain, % 117.94/118.01 (~P4(x2381,f4(x2382))+~E(x2382,f10(a1))), % 117.94/118.01 inference(scs_inference,[],[31,119,22,63,15,20,51,54])). % 117.94/118.01 cnf(244,plain, % 117.94/118.01 (~P4(x2441,f4(f10(a2)))), % 117.94/118.01 inference(scs_inference,[],[31,23,54])). % 117.94/118.01 cnf(249,plain, % 117.94/118.01 (P5(f4(f10(a2)),x2491)), % 117.94/118.01 inference(scs_inference,[],[31,146,23,89,54,15,52])). % 117.94/118.01 cnf(262,plain, % 117.94/118.01 (P3(f13(x2621,a6))), % 117.94/118.01 inference(scs_inference,[],[24,38,47])). % 117.94/118.01 cnf(265,plain, % 117.94/118.01 (E(f14(f9(x2651)),a1)), % 117.94/118.01 inference(scs_inference,[],[29,37,40])). % 117.94/118.01 cnf(266,plain, % 117.94/118.01 (E(a1,f14(f9(x2661)))), % 117.94/118.01 inference(scs_inference,[],[265,2])). % 117.94/118.01 cnf(269,plain, % 117.94/118.01 (P1(f14(f9(x2691)))), % 117.94/118.01 inference(scs_inference,[],[25,75,22,265,2,16,3,13])). % 117.94/118.01 cnf(270,plain, % 117.94/118.01 (P2(f4(a1),f14(f9(x2701)))), % 117.94/118.01 inference(scs_inference,[],[25,75,22,265,2,16,3,13,235])). % 117.94/118.01 cnf(280,plain, % 117.94/118.01 (~P1(f7(f13(a12,a3)))), % 117.94/118.01 inference(scs_inference,[],[146,42,44])). % 117.94/118.01 cnf(282,plain, % 117.94/118.01 (P2(f7(a8),f10(a8))), % 117.94/118.01 inference(scs_inference,[],[75,45,37])). % 117.94/118.01 cnf(283,plain, % 117.94/118.01 (P5(f7(a8),a8)), % 117.94/118.01 inference(scs_inference,[],[282,51])). % 117.94/118.01 cnf(285,plain, % 117.94/118.01 (P2(x2851,a8)+~P4(x2851,f7(a8))), % 117.94/118.01 inference(scs_inference,[],[282,51,55])). % 117.94/118.01 cnf(302,plain, % 117.94/118.01 (P5(f7(a8),x3021)+P2(f5(f7(a8),x3021),a8)), % 117.94/118.01 inference(scs_inference,[],[285,52])). % 117.94/118.01 cnf(309,plain, % 117.94/118.01 (P2(f7(a8),x3091)+~E(f10(a8),x3091)), % 117.94/118.01 inference(scs_inference,[],[283,282,18,20])). % 117.94/118.01 cnf(321,plain, % 117.94/118.01 (~E(f5(x3211,a8),f4(a8))+P5(x3211,a8)), % 117.94/118.01 inference(scs_inference,[],[199,2])). % 117.94/118.01 cnf(327,plain, % 117.94/118.01 (~E(x3271,f4(a8))+~E(f5(x3272,a8),x3271)+P5(x3272,a8)), % 117.94/118.01 inference(scs_inference,[],[321,3])). % 117.94/118.01 cnf(333,plain, % 117.94/118.01 (P2(f7(a8),f10(x3331))+P2(f5(f7(a8),x3331),a8)), % 117.94/118.01 inference(scs_inference,[],[302,49])). % 117.94/118.01 cnf(339,plain, % 117.94/118.01 (~E(f5(x3391,a8),f4(a8))+~P4(a8,f5(x3391,a8))), % 117.94/118.01 inference(scs_inference,[],[201,2])). % 117.94/118.01 cnf(341,plain, % 117.94/118.01 (~E(f5(x3411,f10(x3412)),f9(x3412))+P5(x3411,f10(x3412))), % 117.94/118.01 inference(scs_inference,[],[221,2])). % 117.94/118.01 cnf(344,plain, % 117.94/118.01 (~E(x3441,f4(a8))+~E(f5(x3442,a8),x3441)+~P4(a8,f5(x3442,a8))), % 117.94/118.01 inference(scs_inference,[],[339,3])). % 117.94/118.01 cnf(346,plain, % 117.94/118.01 (P5(x3461,f10(x3462))+~P1(f5(x3461,f10(x3462)))), % 117.94/118.01 inference(scs_inference,[],[29,341,39])). % 117.94/118.01 cnf(347,plain, % 117.94/118.01 (~P1(f5(x3471,f10(x3472)))+P2(x3471,f10(f10(x3472)))), % 117.94/118.01 inference(scs_inference,[],[346,49])). % 117.94/118.01 cnf(368,plain, % 117.94/118.01 (P4(f7(a8),f10(a8))), % 117.94/118.01 inference(scs_inference,[],[282,35,48])). % 117.94/118.01 cnf(371,plain, % 117.94/118.01 (~P4(f10(a8),f7(a8))), % 117.94/118.01 inference(scs_inference,[],[282,35,48,50])). % 117.94/118.01 cnf(434,plain, % 117.94/118.01 (~P1(f7(a8))), % 117.94/118.01 inference(scs_inference,[],[75,37,42])). % 117.94/118.01 cnf(435,plain, % 117.94/118.01 (P4(f4(f7(a8)),f7(a8))), % 117.94/118.01 inference(scs_inference,[],[31,434,48])). % 117.94/118.01 cnf(474,plain, % 117.94/118.01 (~P1(f14(a8))), % 117.94/118.01 inference(scs_inference,[],[75,27,37,43])). % 117.94/118.01 cnf(475,plain, % 117.94/118.01 (P4(f4(f14(a8)),f14(a8))), % 117.94/118.01 inference(scs_inference,[],[474,31,48])). % 117.94/118.01 cnf(502,plain, % 117.94/118.01 (P2(a1,f10(x5021))), % 117.94/118.01 inference(scs_inference,[],[29,37,106])). % 117.94/118.01 cnf(503,plain, % 117.94/118.01 (P2(f14(f9(x5031)),f10(x5032))), % 117.94/118.01 inference(scs_inference,[],[266,502,19])). % 117.94/118.01 cnf(536,plain, % 117.94/118.01 (~P1(f7(f10(x5361)))), % 117.94/118.01 inference(scs_inference,[],[119,42,44])). % 117.94/118.01 cnf(537,plain, % 117.94/118.01 (~E(f14(f9(x5371)),f7(f14(a8)))), % 117.94/118.01 inference(scs_inference,[],[474,269,42,13])). % 117.94/118.01 cnf(538,plain, % 117.94/118.01 (~P1(f7(f14(a8)))), % 117.94/118.01 inference(scs_inference,[],[269,537,39])). % 117.94/118.01 cnf(542,plain, % 117.94/118.01 (P2(f7(f7(a8)),f10(f7(a8)))), % 117.94/118.01 inference(scs_inference,[],[33,42,45])). % 117.94/118.01 cnf(606,plain, % 117.94/118.01 (P2(f7(f10(x6061)),f10(f10(x6061)))), % 117.94/118.01 inference(scs_inference,[],[119,44,45])). % 117.94/118.01 cnf(609,plain, % 117.94/118.01 (P2(x6091,f10(x6092))+~P4(x6091,f7(f10(x6092)))), % 117.94/118.01 inference(scs_inference,[],[606,51,55])). % 117.94/118.01 cnf(655,plain, % 117.94/118.01 (~P2(f10(a8),f7(a8))), % 117.94/118.01 inference(scs_inference,[],[434,371,48])). % 117.94/118.01 cnf(657,plain, % 117.94/118.01 (~P4(f10(a8),f7(f7(a8)))), % 117.94/118.01 inference(scs_inference,[],[542,434,371,48,55])). % 117.94/118.01 cnf(715,plain, % 117.94/118.01 (~P5(f10(x7151),f9(x7152))), % 117.94/118.01 inference(scs_inference,[],[119,144,53])). % 117.94/118.01 cnf(727,plain, % 117.94/118.01 (~P5(f13(a12,a3),a2)), % 117.94/118.01 inference(scs_inference,[],[146,89,53])). % 117.94/118.01 cnf(731,plain, % 117.94/118.01 (~P5(f10(x7311),a6)), % 117.94/118.01 inference(scs_inference,[],[119,114,53])). % 117.94/118.01 cnf(736,plain, % 117.94/118.01 (~P5(f13(a12,a3),f9(x7361))), % 117.94/118.01 inference(scs_inference,[],[146,144,53])). % 117.94/118.01 cnf(748,plain, % 117.94/118.01 (~P5(f10(x7481),a2)), % 117.94/118.01 inference(scs_inference,[],[119,89,53])). % 117.94/118.01 cnf(752,plain, % 117.94/118.01 (~P5(f13(a12,a3),a6)), % 117.94/118.01 inference(scs_inference,[],[146,114,53])). % 117.94/118.01 cnf(756,plain, % 117.94/118.01 (~P5(a8,f9(x7561))), % 117.94/118.01 inference(scs_inference,[],[69,144,53])). % 117.94/118.01 cnf(767,plain, % 117.94/118.01 (~P5(a8,a2)), % 117.94/118.01 inference(scs_inference,[],[69,89,53])). % 117.94/118.01 cnf(771,plain, % 117.94/118.01 (~P5(a11,a6)), % 117.94/118.01 inference(scs_inference,[],[94,114,53])). % 117.94/118.01 cnf(775,plain, % 117.94/118.01 (~P5(a11,f9(x7751))), % 117.94/118.01 inference(scs_inference,[],[94,144,53])). % 117.94/118.01 cnf(787,plain, % 117.94/118.01 (~P5(a11,a2)), % 117.94/118.01 inference(scs_inference,[],[94,89,53])). % 117.94/118.01 cnf(791,plain, % 117.94/118.01 (~P5(a8,a6)), % 117.94/118.01 inference(scs_inference,[],[69,114,53])). % 117.94/118.01 cnf(795,plain, % 117.94/118.01 (~P5(f14(a8),f9(x7951))), % 117.94/118.01 inference(scs_inference,[],[475,144,53])). % 117.94/118.01 cnf(806,plain, % 117.94/118.02 (~P5(f14(a8),a2)), % 117.94/118.02 inference(scs_inference,[],[475,89,53])). % 117.94/118.02 cnf(810,plain, % 117.94/118.02 (~P5(f14(a8),a6)), % 117.94/118.02 inference(scs_inference,[],[475,114,53])). % 117.94/118.02 cnf(814,plain, % 117.94/118.02 (~P5(f7(a8),f9(x8141))), % 117.94/118.02 inference(scs_inference,[],[435,144,53])). % 117.94/118.02 cnf(826,plain, % 117.94/118.02 (~P5(f7(a8),a2)), % 117.94/118.02 inference(scs_inference,[],[435,89,53])). % 117.94/118.02 cnf(830,plain, % 117.94/118.02 (~P5(f7(a8),a6)), % 117.94/118.02 inference(scs_inference,[],[435,114,53])). % 117.94/118.02 cnf(1022,plain, % 117.94/118.02 (~E(a1,a11)), % 117.94/118.02 inference(scs_inference,[],[771,91,17])). % 117.94/118.02 cnf(1125,plain, % 117.94/118.02 (P2(f7(a11),f10(a11))), % 117.94/118.02 inference(scs_inference,[],[1022,22,45,39])). % 117.94/118.02 cnf(1128,plain, % 117.94/118.02 (P2(x11281,a11)+~P4(x11281,f7(a11))), % 117.94/118.02 inference(scs_inference,[],[1125,51,55])). % 117.94/118.02 cnf(1191,plain, % 117.94/118.02 (~P4(f10(a11),f7(a11))), % 117.94/118.02 inference(scs_inference,[],[1125,35,48,50])). % 117.94/118.02 cnf(1215,plain, % 117.94/118.02 (~P5(f10(x12151),a1)), % 117.94/118.02 inference(scs_inference,[],[63,119,53])). % 117.94/118.02 cnf(1219,plain, % 117.94/118.02 (~P5(f13(a12,a3),a1)), % 117.94/118.02 inference(scs_inference,[],[63,146,53])). % 117.94/118.02 cnf(1223,plain, % 117.94/118.02 (~P5(a8,a1)), % 117.94/118.02 inference(scs_inference,[],[63,69,53])). % 117.94/118.02 cnf(1227,plain, % 117.94/118.02 (~P5(a11,a1)), % 117.94/118.02 inference(scs_inference,[],[63,94,53])). % 117.94/118.02 cnf(1231,plain, % 117.94/118.02 (~P5(f14(a8),a1)), % 117.94/118.02 inference(scs_inference,[],[63,475,53])). % 117.94/118.02 cnf(1234,plain, % 117.94/118.02 (~P5(f7(a8),a1)), % 117.94/118.02 inference(scs_inference,[],[63,435,53])). % 117.94/118.02 cnf(1511,plain, % 117.94/118.02 (P2(a2,f10(x15111))), % 117.94/118.02 inference(scs_inference,[],[89,49,52])). % 117.94/118.02 cnf(1529,plain, % 117.94/118.02 (P2(f5(f7(a8),a1),a8)), % 117.94/118.02 inference(scs_inference,[],[1234,51,333])). % 117.94/118.02 cnf(1596,plain, % 117.94/118.02 (P4(a2,f10(x15961))), % 117.94/118.02 inference(scs_inference,[],[1511,35,48])). % 117.94/118.02 cnf(1604,plain, % 117.94/118.02 (~P4(a8,f5(f7(a8),a1))), % 117.94/118.02 inference(scs_inference,[],[1529,33,48,50])). % 117.94/118.02 cnf(1639,plain, % 117.94/118.02 (~E(f10(a8),f10(a2))), % 117.94/118.02 inference(scs_inference,[],[826,51,309])). % 117.94/118.02 cnf(1723,plain, % 117.94/118.02 (~E(x17231,f10(a8))+~E(f4(f7(a8)),x17231)), % 117.94/118.02 inference(scs_inference,[],[655,133,3])). % 117.94/118.02 cnf(1724,plain, % 117.94/118.02 (~E(x17241,f4(f7(a8)))+~E(x17241,f10(a8))), % 117.94/118.02 inference(scs_inference,[],[1723,2])). % 117.94/118.02 cnf(1725,plain, % 117.94/118.02 (~E(x17251,f7(a8))+~E(f4(x17251),f10(a8))), % 117.94/118.02 inference(scs_inference,[],[1724,5])). % 117.94/118.02 cnf(1726,plain, % 117.94/118.02 (~E(f10(a8),f4(x17261))+~E(x17261,f7(a8))), % 117.94/118.02 inference(scs_inference,[],[1725,2])). % 117.94/118.02 cnf(1727,plain, % 117.94/118.02 (~E(x17271,a8)+~E(f10(a8),f4(f7(x17271)))), % 117.94/118.02 inference(scs_inference,[],[1726,12])). % 117.94/118.02 cnf(1728,plain, % 117.94/118.02 (~E(f4(f7(x17281)),f10(a8))+~E(x17281,a8)), % 117.94/118.02 inference(scs_inference,[],[1727,2])). % 117.94/118.02 cnf(1729,plain, % 117.94/118.02 (~E(x17291,f10(a8))+~E(f4(f7(x17292)),x17291)+~E(x17292,a8)), % 117.94/118.02 inference(scs_inference,[],[1728,3])). % 117.94/118.02 cnf(1730,plain, % 117.94/118.02 (~E(f7(x17301),x17302)+~E(f4(x17302),f10(a8))+~E(x17301,a8)), % 117.94/118.02 inference(scs_inference,[],[1729,5])). % 117.94/118.02 cnf(1799,plain, % 117.94/118.02 (~P1(f4(a11))+P4(a1,a11)), % 117.94/118.02 inference(scs_inference,[],[209,37])). % 117.94/118.02 cnf(1828,plain, % 117.94/118.02 (P4(f4(f4(a11)),f4(a11))+P4(a1,a11)), % 117.94/118.02 inference(scs_inference,[],[31,1799,48])). % 117.94/118.02 cnf(1986,plain, % 117.94/118.02 (P1(f7(a11))+P2(f4(f7(a11)),a11)), % 117.94/118.02 inference(scs_inference,[],[31,1128,48])). % 117.94/118.02 cnf(1987,plain, % 117.94/118.02 (P2(f4(f7(a11)),a11)), % 117.94/118.02 inference(scs_inference,[],[34,1986,42])). % 117.94/118.02 cnf(2095,plain, % 117.94/118.02 (P5(x20951,a11)+~E(f4(f7(a11)),f5(x20951,a11))), % 117.94/118.02 inference(scs_inference,[],[1987,34,48,50,14,56])). % 117.94/118.02 cnf(2099,plain, % 117.94/118.02 (~E(f5(x20991,a11),f4(f7(a11)))+P5(x20991,a11)), % 117.94/118.02 inference(scs_inference,[],[2095,2])). % 117.94/118.02 cnf(2100,plain, % 117.94/118.02 (~E(x21001,f4(f7(a11)))+~E(f5(x21002,a11),x21001)+P5(x21002,a11)), % 117.94/118.02 inference(scs_inference,[],[2099,3])). % 117.94/118.02 cnf(2292,plain, % 117.94/118.02 (P4(f5(f14(f13(a12,a3)),a12),a12)), % 117.94/118.02 inference(scs_inference,[],[36,28,52,58])). % 117.94/118.02 cnf(2335,plain, % 117.94/118.02 (~E(f9(x23351),x23352)+~P2(f10(x23351),f10(a1))), % 117.94/118.02 inference(scs_inference,[],[22,220,54])). % 117.94/118.02 cnf(2336,plain, % 117.94/118.02 (~P2(f10(x23361),f10(a1))), % 117.94/118.02 inference(equality_inference,[],[2335])). % 117.94/118.02 cnf(2337,plain, % 117.94/118.02 (~P4(f10(x23371),f7(f10(a1)))), % 117.94/118.02 inference(scs_inference,[],[2336,609])). % 117.94/118.02 cnf(2339,plain, % 117.94/118.02 (~P4(f10(x23391),f10(a1))), % 117.94/118.02 inference(scs_inference,[],[2336,609,46])). % 117.94/118.02 cnf(2397,plain, % 117.94/118.02 (P4(a1,a11)+~E(a11,f10(a1))), % 117.94/118.02 inference(scs_inference,[],[238,1828])). % 117.94/118.02 cnf(2409,plain, % 117.94/118.02 (P2(a1,x24091)+~E(a11,f10(a1))+~P2(a11,f10(x24091))), % 117.94/118.02 inference(scs_inference,[],[2397,55])). % 117.94/118.02 cnf(2410,plain, % 117.94/118.02 (~E(a11,f10(a1))+P2(a1,a11)), % 117.94/118.02 inference(scs_inference,[],[30,2409,49])). % 117.94/118.02 cnf(2426,plain, % 117.94/118.02 (~E(x24261,f10(a1))+~E(a11,x24261)+P2(a1,a11)), % 117.94/118.02 inference(scs_inference,[],[2410,3])). % 117.94/118.02 cnf(2475,plain, % 117.94/118.02 (P3(a6)), % 117.94/118.02 inference(scs_inference,[],[24,38])). % 117.94/118.02 cnf(2479,plain, % 117.94/118.02 (~P1(f7(f7(a8)))), % 117.94/118.02 inference(scs_inference,[],[434,23,24,38,41,42])). % 117.94/118.02 cnf(2481,plain, % 117.94/118.02 (P3(f13(x24811,a2))), % 117.94/118.02 inference(scs_inference,[],[26,434,23,24,38,41,42,47])). % 117.94/118.02 cnf(2483,plain, % 117.94/118.02 (P2(f5(f7(a8),a2),a8)), % 117.94/118.02 inference(scs_inference,[],[26,826,434,23,24,38,41,42,47,302])). % 117.94/118.02 cnf(2485,plain, % 117.94/118.02 (P2(f4(f10(a2)),f10(x24851))), % 117.94/118.02 inference(scs_inference,[],[26,826,434,249,23,24,38,41,42,47,302,49])). % 117.94/118.02 cnf(2489,plain, % 117.94/118.02 (E(f14(a2),f14(a1))), % 117.94/118.02 inference(scs_inference,[],[26,826,434,249,23,24,38,41,42,47,302,49,37,6])). % 117.94/118.02 cnf(2490,plain, % 117.94/118.02 (~E(f10(a2),f10(a8))), % 117.94/118.02 inference(scs_inference,[],[26,1639,826,434,249,23,24,38,41,42,47,302,49,37,6,2])). % 117.94/118.02 cnf(2491,plain, % 117.94/118.02 (P1(f14(a2))), % 117.94/118.02 inference(scs_inference,[],[26,1639,826,434,249,23,24,38,41,42,47,302,49,37,6,2,40])). % 117.94/118.02 cnf(2493,plain, % 117.94/118.02 (P4(f5(a8,a6),a8)), % 117.94/118.02 inference(scs_inference,[],[791,26,1639,826,434,249,23,24,38,41,42,47,302,49,37,6,2,40,52])). % 117.94/118.02 cnf(2499,plain, % 117.94/118.02 (~E(f14(a2),f14(f13(a12,a3)))), % 117.94/118.02 inference(scs_inference,[],[36,791,26,1639,126,826,434,249,23,24,38,41,42,47,302,49,37,6,2,40,52,51,50,13])). % 117.94/118.02 cnf(2500,plain, % 117.94/118.02 (P3(f14(a1))), % 117.94/118.02 inference(scs_inference,[],[36,791,26,1639,126,826,434,249,23,24,38,41,42,47,302,49,37,6,2,40,52,51,50,13,16])). % 117.94/118.02 cnf(2502,plain, % 117.94/118.02 (~P2(f10(x25021),f10(a2))), % 117.94/118.02 inference(scs_inference,[],[36,791,26,1639,1596,126,826,434,249,23,24,38,41,42,47,302,49,37,6,2,40,52,51,50,13,16,3,54])). % 117.94/118.02 cnf(2506,plain, % 117.94/118.02 (E(f9(a2),f9(a1))), % 117.94/118.02 inference(scs_inference,[],[36,791,26,657,1639,1596,126,826,434,249,23,24,38,41,42,47,302,49,37,6,2,40,52,51,50,13,16,3,54,48,4])). % 117.94/118.02 cnf(2508,plain, % 117.94/118.02 (E(f7(a2),f7(a1))), % 117.94/118.02 inference(scs_inference,[],[36,791,26,657,1639,1596,126,826,434,249,23,24,38,41,42,47,302,49,37,6,2,40,52,51,50,13,16,3,54,48,4,5,12])). % 117.94/118.02 cnf(2509,plain, % 117.94/118.02 (E(f5(a2,x25091),f5(a1,x25091))), % 117.94/118.02 inference(scs_inference,[],[36,791,26,657,1639,1596,126,826,434,249,23,24,38,41,42,47,302,49,37,6,2,40,52,51,50,13,16,3,54,48,4,5,12,8])). % 117.94/118.02 cnf(2510,plain, % 117.94/118.02 (E(f5(x25101,a2),f5(x25101,a1))), % 117.94/118.02 inference(scs_inference,[],[36,791,26,657,1639,1596,126,826,434,249,23,24,38,41,42,47,302,49,37,6,2,40,52,51,50,13,16,3,54,48,4,5,12,8,9])). % 117.94/118.02 cnf(2511,plain, % 117.94/118.02 (E(f13(a2,x25111),f13(a1,x25111))), % 117.94/118.02 inference(scs_inference,[],[36,791,26,657,1639,1596,126,826,434,249,23,24,38,41,42,47,302,49,37,6,2,40,52,51,50,13,16,3,54,48,4,5,12,8,9,10])). % 117.94/118.02 cnf(2512,plain, % 117.94/118.02 (E(f13(x25121,a2),f13(x25121,a1))), % 117.94/118.02 inference(scs_inference,[],[36,791,26,657,1639,1596,126,826,434,249,23,24,38,41,42,47,302,49,37,6,2,40,52,51,50,13,16,3,54,48,4,5,12,8,9,10,11])). % 117.94/118.02 cnf(2513,plain, % 117.94/118.02 (E(f10(a2),f10(a1))), % 117.94/118.02 inference(scs_inference,[],[36,791,26,657,1639,1596,126,826,434,249,23,24,38,41,42,47,302,49,37,6,2,40,52,51,50,13,16,3,54,48,4,5,12,8,9,10,11,7])). % 117.94/118.02 cnf(2533,plain, % 117.94/118.02 (P2(x25331,f10(x25331))), % 117.94/118.02 inference(scs_inference,[],[814,30,302,49])). % 117.94/118.02 cnf(2535,plain, % 117.94/118.02 (P3(f14(a6))), % 117.94/118.02 inference(scs_inference,[],[814,30,24,302,49,41])). % 117.94/118.02 cnf(2537,plain, % 117.94/118.02 (P3(f9(x25371))), % 117.94/118.02 inference(scs_inference,[],[814,29,30,24,302,49,41,38])). % 117.94/118.02 cnf(2539,plain, % 117.94/118.02 (~P1(f7(a11))), % 117.94/118.02 inference(scs_inference,[],[34,814,29,30,24,302,49,41,38,42])). % 117.94/118.02 cnf(2543,plain, % 117.94/118.02 (E(f14(a2),a1)), % 117.94/118.02 inference(scs_inference,[],[262,2491,34,814,29,30,24,302,49,41,38,42,47,37])). % 117.94/118.02 cnf(2549,plain, % 117.94/118.02 (E(f5(f14(a2),x25491),f5(a1,x25491))), % 117.94/118.02 inference(scs_inference,[],[262,2491,34,814,29,30,24,302,49,41,38,42,47,37,5,10,12,11,8])). % 117.94/118.02 cnf(2550,plain, % 117.94/118.02 (E(f10(f14(a2)),f10(a1))), % 117.94/118.02 inference(scs_inference,[],[262,2491,34,814,29,30,24,302,49,41,38,42,47,37,5,10,12,11,8,7])). % 117.94/118.02 cnf(2551,plain, % 117.94/118.02 (E(f5(x25511,f14(a2)),f5(x25511,a1))), % 117.94/118.02 inference(scs_inference,[],[262,2491,34,814,29,30,24,302,49,41,38,42,47,37,5,10,12,11,8,7,9])). % 117.94/118.02 cnf(2555,plain, % 117.94/118.02 (P1(f14(f14(a2)))), % 117.94/118.02 inference(scs_inference,[],[262,2491,2499,34,814,29,30,24,302,49,41,38,42,47,37,5,10,12,11,8,7,9,4,6,2,40])). % 117.94/118.02 cnf(2557,plain, % 117.94/118.02 (P4(f5(f13(a12,a3),f9(x25571)),f13(a12,a3))), % 117.94/118.02 inference(scs_inference,[],[262,2491,2499,736,34,814,29,30,24,302,49,41,38,42,47,37,5,10,12,11,8,7,9,4,6,2,40,52])). % 117.94/118.02 cnf(2563,plain, % 117.94/118.02 (~E(f14(a2),f7(f7(a8)))), % 117.94/118.02 inference(scs_inference,[],[262,2491,2479,2499,736,34,814,29,30,24,302,49,41,38,42,47,37,5,10,12,11,8,7,9,4,6,2,40,52,51,50,13])). % 117.94/118.02 cnf(2564,plain, % 117.94/118.02 (E(f5(a2,a2),f5(a1,a1))), % 117.94/118.02 inference(scs_inference,[],[2509,2510,262,2491,2479,2499,736,34,814,29,30,24,302,49,41,38,42,47,37,5,10,12,11,8,7,9,4,6,2,40,52,51,50,13,3])). % 117.94/118.02 cnf(2569,plain, % 117.94/118.02 (~P2(f10(a11),f7(a11))), % 117.94/118.02 inference(scs_inference,[],[1191,2509,2510,262,2491,2493,2479,2499,736,34,814,29,30,24,302,49,41,38,42,47,37,5,10,12,11,8,7,9,4,6,2,40,52,51,50,13,3,54,48])). % 117.94/118.02 cnf(2571,plain, % 117.94/118.02 (~E(f4(f7(a11)),f10(a11))), % 117.94/118.02 inference(scs_inference,[],[1191,2509,2510,262,2491,2493,2479,2499,736,34,814,29,30,24,31,302,49,41,38,42,47,37,5,10,12,11,8,7,9,4,6,2,40,52,51,50,13,3,54,48,19])). % 117.94/118.02 cnf(2573,plain, % 117.94/118.02 (~E(f10(f10(x25731)),f10(a2))), % 117.94/118.02 inference(scs_inference,[],[1191,2509,2510,262,2502,2491,2493,2479,2499,736,34,814,29,30,24,31,302,49,41,38,42,47,37,5,10,12,11,8,7,9,4,6,2,40,52,51,50,13,3,54,48,19,20])). % 117.94/118.02 cnf(2574,plain, % 117.94/118.02 (~P5(a8,f14(a2))), % 117.94/118.02 inference(scs_inference,[],[1191,2509,2510,262,2502,2491,2493,2479,2499,736,1223,34,814,29,30,24,31,302,49,41,38,42,47,37,5,10,12,11,8,7,9,4,6,2,40,52,51,50,13,3,54,48,19,20,18])). % 117.94/118.02 cnf(2595,plain, % 117.94/118.02 (~P1(f7(f7(a11)))), % 117.94/118.02 inference(scs_inference,[],[2539,42])). % 117.94/118.02 cnf(2599,plain, % 117.94/118.02 (E(f14(f14(a2)),a1)), % 117.94/118.02 inference(scs_inference,[],[2537,2539,2555,42,47,37])). % 117.94/118.02 cnf(2601,plain, % 117.94/118.02 (P1(f14(a6))), % 117.94/118.02 inference(scs_inference,[],[2537,2539,2555,24,42,47,37,40])). % 117.94/118.02 cnf(2604,plain, % 117.94/118.02 (P4(f5(a8,f14(a2)),a8)), % 117.94/118.02 inference(scs_inference,[],[2537,2539,2574,2571,2555,24,42,47,37,40,2,52])). % 117.94/118.02 cnf(2606,plain, % 117.94/118.02 (~P2(a11,f10(f9(x26061)))), % 117.94/118.02 inference(scs_inference,[],[2537,2539,2574,2571,2555,775,24,42,47,37,40,2,52,51])). % 117.94/118.02 cnf(2610,plain, % 117.94/118.02 (~E(f14(f14(a2)),f7(a11))), % 117.94/118.02 inference(scs_inference,[],[2537,2539,2574,2571,2555,775,24,42,47,37,40,2,52,51,50,13])). % 117.94/118.02 cnf(2612,plain, % 117.94/118.02 (~P2(f13(a12,a3),f10(f14(a2)))), % 117.94/118.02 inference(scs_inference,[],[2537,2489,2539,2574,2557,2571,2555,2563,775,2491,24,42,47,37,40,2,52,51,50,13,3,54])). % 117.94/118.02 cnf(2618,plain, % 117.94/118.02 (P2(x26181,f10(x26181))), % 117.94/118.02 inference(rename_variables,[],[2533])). % 117.94/118.02 cnf(2620,plain, % 117.94/118.02 (P2(f14(a1),f10(f14(a2)))), % 117.94/118.02 inference(scs_inference,[],[2533,2618,2537,2489,2539,2574,2557,2571,2555,2563,2337,775,2491,24,536,42,47,37,40,2,52,51,50,13,3,54,48,55,19])). % 117.94/118.02 cnf(2622,plain, % 117.94/118.02 (P2(f4(f14(a2)),f14(a1))), % 117.94/118.02 inference(scs_inference,[],[2533,2618,2537,2489,2539,2574,2557,2571,2555,2563,2337,775,2491,24,536,31,42,47,37,40,2,52,51,50,13,3,54,48,55,19,20])). % 117.94/118.02 cnf(2624,plain, % 117.94/118.02 (~E(a8,f14(a2))), % 117.94/118.02 inference(scs_inference,[],[2533,2618,2537,2489,2539,2574,2557,2571,2555,2563,2337,775,2491,30,24,536,31,42,47,37,40,2,52,51,50,13,3,54,48,55,19,20,18])). % 117.94/118.02 cnf(2625,plain, % 117.94/118.02 (P5(x26251,x26251)), % 117.94/118.02 inference(rename_variables,[],[30])). % 117.94/118.02 cnf(2626,plain, % 117.94/118.02 (~P4(x26261,f14(a2))), % 117.94/118.02 inference(scs_inference,[],[2533,2618,2537,2489,2539,2543,2574,2557,2571,2555,2563,2337,775,2491,30,24,63,536,31,42,47,37,40,2,52,51,50,13,3,54,48,55,19,20,18,15])). % 117.94/118.02 cnf(2630,plain, % 117.94/118.02 (~P4(x26301,f14(f13(x26302,a2)))), % 117.94/118.02 inference(scs_inference,[],[2533,2618,2537,2489,2539,2543,2574,2557,2571,2549,2555,2563,2337,775,26,2491,30,24,63,536,31,42,47,37,40,2,52,51,50,13,3,54,48,55,19,20,18,15,327,59])). % 117.94/118.02 cnf(2632,plain, % 117.94/118.02 (P5(f14(a1),f14(a2))), % 117.94/118.02 inference(scs_inference,[],[2533,2618,2537,2489,2539,2543,2574,2557,2571,2549,2555,2563,2337,775,26,2491,30,2625,24,63,536,31,42,47,37,40,2,52,51,50,13,3,54,48,55,19,20,18,15,327,59,17])). % 117.94/118.02 cnf(2638,plain, % 117.94/118.02 (E(f14(a6),a1)), % 117.94/118.02 inference(scs_inference,[],[2481,2601,47,37])). % 117.94/118.02 cnf(2642,plain, % 117.94/118.02 (E(f7(f14(a6)),f7(a1))), % 117.94/118.02 inference(scs_inference,[],[2481,2601,47,37,10,7,12])). % 117.94/118.02 cnf(2644,plain, % 117.94/118.02 (E(f5(x26441,f14(a6)),f5(x26441,a1))), % 117.94/118.02 inference(scs_inference,[],[2481,2601,47,37,10,7,12,5,9])). % 117.94/118.02 cnf(2649,plain, % 117.94/118.02 (P1(f14(f14(a6)))), % 117.94/118.02 inference(scs_inference,[],[2481,2601,47,37,10,7,12,5,9,11,8,4,6,40])). % 117.94/118.02 cnf(2652,plain, % 117.94/118.02 (P4(f5(a8,a2),a8)), % 117.94/118.02 inference(scs_inference,[],[2481,2601,2624,767,47,37,10,7,12,5,9,11,8,4,6,40,2,52])). % 117.94/118.02 cnf(2659,plain, % 117.94/118.02 (E(f13(a2,a2),f13(a1,a1))), % 117.94/118.02 inference(scs_inference,[],[2511,2512,2481,2601,2624,2595,767,47,37,10,7,12,5,9,11,8,4,6,40,2,52,51,50,13,3])). % 117.94/118.02 cnf(2664,plain, % 117.94/118.02 (P1(f14(f13(x26641,a2)))), % 117.94/118.03 inference(scs_inference,[],[2511,2512,2481,2601,2624,2630,2595,2604,767,31,47,37,10,7,12,5,9,11,8,4,6,40,2,52,51,50,13,3,54,48])). % 117.94/118.03 cnf(2665,plain, % 117.94/118.03 (~P4(x26651,f14(f13(x26652,a2)))), % 117.94/118.03 inference(rename_variables,[],[2630])). % 117.94/118.03 cnf(2668,plain, % 117.94/118.03 (~P4(x26681,f14(a1))), % 117.94/118.03 inference(scs_inference,[],[2511,2512,2481,2626,2601,2632,2624,2630,2595,2604,767,31,47,37,10,7,12,5,9,11,8,4,6,40,2,52,51,50,13,3,54,48,53])). % 117.94/118.03 cnf(2672,plain, % 117.94/118.03 (~P5(f13(a12,a3),f14(f14(a2)))), % 117.94/118.03 inference(scs_inference,[],[2511,2512,2481,2626,2601,2632,2624,2630,2595,2606,2604,2599,767,1219,2533,31,47,37,10,7,12,5,9,11,8,4,6,40,2,52,51,50,13,3,54,48,53,20,18])). % 117.94/118.03 cnf(2675,plain, % 117.94/118.03 (~E(f14(a1),a8)), % 117.94/118.03 inference(scs_inference,[],[2511,2512,2481,2626,2601,2632,2624,2630,2665,2595,2606,2604,2599,767,1219,2533,2574,31,47,37,10,7,12,5,9,11,8,4,6,40,2,52,51,50,13,3,54,48,53,20,18,15,17])). % 117.94/118.03 cnf(2680,plain, % 117.94/118.03 (~P4(x26801,f14(f13(x26802,a1)))), % 117.94/118.03 inference(scs_inference,[],[2511,2512,2481,2626,2601,2632,2624,2630,2665,2595,2606,2604,2599,2550,767,1219,2533,25,2574,31,47,37,10,7,12,5,9,11,8,4,6,40,2,52,51,50,13,3,54,48,53,20,18,15,17,46,2426,59])). % 117.94/118.03 cnf(2682,plain, % 117.94/118.03 (P1(f13(x26821,a2))), % 117.94/118.03 inference(scs_inference,[],[2511,2512,2481,2626,2601,2632,2624,2630,2665,2595,2606,2604,2599,2550,767,1219,2533,25,2574,31,47,37,10,7,12,5,9,11,8,4,6,40,2,52,51,50,13,3,54,48,53,20,18,15,17,46,2426,59,43])). % 117.94/118.03 cnf(2691,plain, % 117.94/118.03 (E(f13(x26911,a2),a1)), % 117.94/118.03 inference(scs_inference,[],[2682,2500,47,37])). % 117.94/118.03 cnf(2693,plain, % 117.94/118.03 (E(f13(f13(x26931,a2),x26932),f13(a1,x26932))), % 117.94/118.03 inference(scs_inference,[],[2682,2500,47,37,10])). % 117.94/118.03 cnf(2697,plain, % 117.94/118.03 (E(f5(f13(x26971,a2),x26972),f5(a1,x26972))), % 117.94/118.03 inference(scs_inference,[],[2682,2500,47,37,10,12,5,7,8])). % 117.94/118.03 cnf(2698,plain, % 117.94/118.03 (E(f5(x26981,f13(x26982,a2)),f5(x26981,a1))), % 117.94/118.03 inference(scs_inference,[],[2682,2500,47,37,10,12,5,7,8,9])). % 117.94/118.03 cnf(2699,plain, % 117.94/118.03 (E(f13(x26991,f13(x26992,a2)),f13(x26991,a1))), % 117.94/118.03 inference(scs_inference,[],[2682,2500,47,37,10,12,5,7,8,9,11])). % 117.94/118.03 cnf(2701,plain, % 117.94/118.03 (E(f14(f13(x27011,a2)),f14(a1))), % 117.94/118.03 inference(scs_inference,[],[2682,2500,47,37,10,12,5,7,8,9,11,4,6])). % 117.94/118.03 cnf(2702,plain, % 117.94/118.03 (P1(f14(a1))), % 117.94/118.03 inference(scs_inference,[],[2682,2500,22,47,37,10,12,5,7,8,9,11,4,6,40])). % 117.94/118.03 cnf(2704,plain, % 117.94/118.03 (~E(a8,f14(a1))), % 117.94/118.03 inference(scs_inference,[],[2682,2500,2675,22,47,37,10,12,5,7,8,9,11,4,6,40,2])). % 117.94/118.03 cnf(2705,plain, % 117.94/118.03 (P4(f5(f13(a12,a3),a6),f13(a12,a3))), % 117.94/118.03 inference(scs_inference,[],[2682,2500,2675,752,22,47,37,10,12,5,7,8,9,11,4,6,40,2,52])). % 117.94/118.03 cnf(2707,plain, % 117.94/118.03 (~P2(f13(a12,a3),f10(a6))), % 117.94/118.03 inference(scs_inference,[],[2682,2500,2675,752,22,47,37,10,12,5,7,8,9,11,4,6,40,2,52,51])). % 117.94/118.03 cnf(2711,plain, % 117.94/118.03 (~E(f13(x27111,a2),f7(f7(a8)))), % 117.94/118.03 inference(scs_inference,[],[2682,2500,2675,752,2479,22,47,37,10,12,5,7,8,9,11,4,6,40,2,52,51,50,13])). % 117.94/118.03 cnf(2716,plain, % 117.94/118.03 (P1(f14(f13(x27161,a1)))), % 117.94/118.03 inference(scs_inference,[],[2682,2500,2659,2652,2675,2680,752,2479,22,31,47,37,10,12,5,7,8,9,11,4,6,40,2,52,51,50,13,3,54,48])). % 117.94/118.03 cnf(2718,plain, % 117.94/118.03 (P2(f4(x27181),x27181)), % 117.94/118.03 inference(rename_variables,[],[31])). % 117.94/118.03 cnf(2723,plain, % 117.94/118.03 (P5(x27231,x27231)), % 117.94/118.03 inference(rename_variables,[],[30])). % 117.94/118.03 cnf(2724,plain, % 117.94/118.03 (~P4(x27241,f14(a6))), % 117.94/118.03 inference(scs_inference,[],[2508,2682,2500,2659,2652,2638,2675,2680,2672,752,2479,30,63,22,31,2718,47,37,10,12,5,7,8,9,11,4,6,40,2,52,51,50,13,3,54,48,20,18,15])). % 117.94/118.03 cnf(2727,plain, % 117.94/118.03 (P2(f7(a1),f10(f7(a2)))), % 117.94/118.03 inference(scs_inference,[],[2508,2682,2500,2659,2652,2638,2675,2680,2672,752,2479,30,2723,63,22,31,2718,47,37,10,12,5,7,8,9,11,4,6,40,2,52,51,50,13,3,54,48,20,18,15,17,49])). % 117.94/118.03 cnf(2734,plain, % 117.94/118.03 (~P4(x27341,f14(f13(x27342,a6)))), % 117.94/118.03 inference(scs_inference,[],[2508,2682,2500,2659,2652,2638,2675,2642,2680,2672,752,2479,2475,30,2723,63,22,31,2718,47,37,10,12,5,7,8,9,11,4,6,40,2,52,51,50,13,3,54,48,20,18,15,17,49,41,46,1730,59])). % 117.94/118.03 cnf(2768,plain, % 117.94/118.03 (E(f14(a1),a1)), % 117.94/118.03 inference(scs_inference,[],[2535,2702,2716,38,47,37])). % 117.94/118.03 cnf(2771,plain, % 117.94/118.03 (E(f13(f14(a1),x27711),f13(a1,x27711))), % 117.94/118.03 inference(scs_inference,[],[2535,2702,2716,38,47,37,5,10])). % 117.94/118.03 cnf(2774,plain, % 117.94/118.03 (E(f5(f14(a1),x27741),f5(a1,x27741))), % 117.94/118.03 inference(scs_inference,[],[2535,2702,2716,38,47,37,5,10,7,12,8])). % 117.94/118.03 cnf(2775,plain, % 117.94/118.03 (E(f13(x27751,f14(a1)),f13(x27751,a1))), % 117.94/118.03 inference(scs_inference,[],[2535,2702,2716,38,47,37,5,10,7,12,8,11])). % 117.94/118.03 cnf(2776,plain, % 117.94/118.03 (E(f5(x27761,f14(a1)),f5(x27761,a1))), % 117.94/118.03 inference(scs_inference,[],[2535,2702,2716,38,47,37,5,10,7,12,8,11,9])). % 117.94/118.03 cnf(2778,plain, % 117.94/118.03 (E(f14(f14(a1)),f14(a1))), % 117.94/118.03 inference(scs_inference,[],[2535,2702,2716,38,47,37,5,10,7,12,8,11,9,4,6])). % 117.94/118.03 cnf(2779,plain, % 117.94/118.03 (P1(f14(f14(a1)))), % 117.94/118.03 inference(scs_inference,[],[2535,2702,2716,38,47,37,5,10,7,12,8,11,9,4,6,40])). % 117.94/118.03 cnf(2784,plain, % 117.94/118.03 (~P2(f14(a8),f10(a6))), % 117.94/118.03 inference(scs_inference,[],[2535,2702,2573,2716,810,38,47,37,5,10,7,12,8,11,9,4,6,40,2,52,51])). % 117.94/118.03 cnf(2790,plain, % 117.94/118.03 (E(f13(x27901,a2),a1)), % 117.94/118.03 inference(rename_variables,[],[2691])). % 117.94/118.03 cnf(2793,plain, % 117.94/118.03 (P4(f4(f10(a2)),f10(x27931))), % 117.94/118.03 inference(scs_inference,[],[2535,2702,2691,2705,2485,2573,2716,2711,810,2595,35,38,47,37,5,10,7,12,8,11,9,4,6,40,2,52,51,50,13,3,54,48])). % 117.94/118.03 cnf(2796,plain, % 117.94/118.03 (~E(f10(f13(a12,a3)),f10(a6))), % 117.94/118.03 inference(scs_inference,[],[2707,2535,2702,2691,2705,2485,2573,2716,2711,810,2595,2533,35,38,47,37,5,10,7,12,8,11,9,4,6,40,2,52,51,50,13,3,54,48,20])). % 117.94/118.03 cnf(2798,plain, % 117.94/118.03 (~P5(f14(a8),f13(x27981,a2))), % 117.94/118.03 inference(scs_inference,[],[2707,2535,2702,2691,2790,2705,2485,2573,2716,2711,810,1231,2595,2533,35,38,47,37,5,10,7,12,8,11,9,4,6,40,2,52,51,50,13,3,54,48,20,18])). % 117.94/118.03 cnf(2799,plain, % 117.94/118.03 (~E(f13(a12,a3),f14(a6))), % 117.94/118.03 inference(scs_inference,[],[2724,2707,2535,2702,2691,2790,2705,2485,2573,2716,2711,810,1231,2595,2533,35,38,47,37,5,10,7,12,8,11,9,4,6,40,2,52,51,50,13,3,54,48,20,18,15])). % 117.94/118.03 cnf(2803,plain, % 117.94/118.03 (~P4(f5(f14(a8),f13(x28031,a2)),f13(x28031,a2))), % 117.94/118.03 inference(scs_inference,[],[2724,2707,2535,2702,2691,2790,2705,2485,2573,2716,2711,810,1231,2595,2533,35,38,47,37,5,10,7,12,8,11,9,4,6,40,2,52,51,50,13,3,54,48,20,18,15,46,56])). % 117.94/118.03 cnf(2808,plain, % 117.94/118.03 (P3(f13(x28081,a1))), % 117.94/118.03 inference(scs_inference,[],[25,47])). % 117.94/118.03 cnf(2813,plain, % 117.94/118.03 (P4(f5(f14(a8),f13(x28131,a2)),f14(a8))), % 117.94/118.03 inference(scs_inference,[],[2799,2798,2779,25,47,37,2,52])). % 117.94/118.03 cnf(2819,plain, % 117.94/118.03 (~E(f14(f14(a1)),f13(a12,a3))), % 117.94/118.03 inference(scs_inference,[],[2799,2798,2779,129,25,47,37,2,52,51,50,13])). % 117.94/118.03 cnf(2822,plain, % 117.94/118.03 (E(f5(x28221,f14(a1)),f5(x28221,a1))), % 117.94/118.03 inference(rename_variables,[],[2776])). % 117.94/118.03 cnf(2825,plain, % 117.94/118.03 (P1(f14(f13(x28251,a6)))), % 117.94/118.03 inference(scs_inference,[],[2799,2798,2793,2774,2776,2734,2779,129,2682,25,31,47,37,2,52,51,50,13,3,54,48])). % 117.94/118.03 cnf(2829,plain, % 117.94/118.03 (~E(f14(a1),f13(a12,a3))), % 117.94/118.03 inference(scs_inference,[],[2799,2798,2793,2774,2776,2620,2734,2779,2612,129,2682,25,31,47,37,2,52,51,50,13,3,54,48,19])). % 117.94/118.03 cnf(2831,plain, % 117.94/118.03 (~P5(a8,f14(a1))), % 117.94/118.03 inference(scs_inference,[],[2799,2798,2768,2793,2774,2776,2622,2620,2734,2779,2612,1223,129,2682,25,31,47,37,2,52,51,50,13,3,54,48,19,20,18])). % 117.94/118.03 cnf(2834,plain, % 117.94/118.03 (P2(f5(f14(a8),f13(x28341,a2)),f14(a8))), % 117.94/118.03 inference(scs_inference,[],[2799,2798,2768,2793,2774,2776,2822,2622,2620,2734,2779,2612,1604,1223,129,2682,25,31,47,37,2,52,51,50,13,3,54,48,19,20,18,15,46])). % 117.94/118.03 cnf(2844,plain, % 117.94/118.03 (E(f14(f13(x28441,a6)),a1)), % 117.94/118.03 inference(scs_inference,[],[2808,2825,38,47,37])). % 117.94/118.03 cnf(2846,plain, % 117.94/118.03 (~E(f13(a12,a3),f14(a1))), % 117.94/118.03 inference(scs_inference,[],[2808,2829,2825,38,47,37,2])). % 117.94/118.03 cnf(2854,plain, % 117.94/118.03 (E(f13(f14(a1),f14(a1)),f13(a1,a1))), % 117.94/118.03 inference(scs_inference,[],[2808,2829,2831,2771,2775,2825,126,2682,38,47,37,2,52,51,50,13,3])). % 117.94/118.03 cnf(2861,plain, % 117.94/118.03 (P2(f5(f14(a8),a1),f14(a8))), % 117.94/118.03 inference(scs_inference,[],[2808,2829,2831,2771,2775,2813,2834,2483,2825,2698,126,2682,2702,33,38,47,37,2,52,51,50,13,3,54,48,19])). % 117.94/118.03 cnf(2866,plain, % 117.94/118.03 (~P4(x28661,f14(f14(a1)))), % 117.94/118.03 inference(scs_inference,[],[2808,2829,2831,2778,2771,2775,2813,2834,2483,2825,2668,2698,2784,126,2533,2682,2702,33,38,47,37,2,52,51,50,13,3,54,48,19,20,18,15])). % 117.94/118.03 cnf(2867,plain, % 117.94/118.03 (P2(f5(a8,f14(a1)),a8)), % 117.94/118.03 inference(scs_inference,[],[2808,2829,2831,2778,2771,2775,2813,2834,2483,2825,2668,2698,2784,126,2533,2682,2702,33,38,47,37,2,52,51,50,13,3,54,48,19,20,18,15,46])). % 117.94/118.03 cnf(2875,plain, % 117.94/118.03 (P3(f13(x28751,a8))), % 117.94/118.03 inference(scs_inference,[],[27,47])). % 117.94/118.03 cnf(2877,plain, % 117.94/118.03 (E(f14(f13(x28771,a2)),a1)), % 117.94/118.03 inference(scs_inference,[],[2664,27,47,37])). % 117.94/118.03 cnf(2882,plain, % 117.94/118.03 (~P2(f13(a12,a3),f10(a2))), % 117.94/118.03 inference(scs_inference,[],[2819,2664,727,27,47,37,2,52,51])). % 117.94/118.03 cnf(2886,plain, % 117.94/118.03 (~E(f14(f13(x28861,a2)),f7(a11))), % 117.94/118.03 inference(scs_inference,[],[2819,2664,727,2539,27,47,37,2,52,51,50,13])). % 117.94/118.03 cnf(2887,plain, % 117.94/118.03 (E(f5(f13(x28871,a2),f14(a2)),f5(a1,a1))), % 117.94/118.03 inference(scs_inference,[],[2819,2697,2664,2551,727,2539,27,47,37,2,52,51,50,13,3])). % 117.94/118.03 cnf(2906,plain, % 117.94/118.03 (E(f14(f14(a6)),a1)), % 117.94/118.03 inference(scs_inference,[],[2875,2649,47,37])). % 117.94/118.03 cnf(2909,plain, % 117.94/118.03 (P4(f5(f14(a8),a2),f14(a8))), % 117.94/118.03 inference(scs_inference,[],[2875,2886,2649,806,47,37,2,52])). % 117.94/118.03 cnf(2911,plain, % 117.94/118.03 (~P2(f14(a8),f10(a2))), % 117.94/118.03 inference(scs_inference,[],[2875,2886,2649,806,47,37,2,52,51])). % 117.94/118.03 cnf(2916,plain, % 117.94/118.03 (~E(a1,f7(a11))), % 117.94/118.03 inference(scs_inference,[],[2875,2886,2877,2649,806,538,2601,47,37,2,52,51,50,13,3])). % 117.94/118.03 cnf(2918,plain, % 117.94/118.03 (P1(f13(x29181,a6))), % 117.94/118.03 inference(scs_inference,[],[2875,2886,2877,2649,806,262,538,2825,2601,47,37,2,52,51,50,13,3,43])). % 117.94/118.03 cnf(2921,plain, % 117.94/118.03 (P4(f5(f14(a8),a1),f14(a8))), % 117.94/118.03 inference(scs_inference,[],[2875,2861,2886,2877,2649,806,262,538,2825,2601,474,47,37,2,52,51,50,13,3,43,48])). % 117.94/118.03 cnf(2925,plain, % 117.94/118.03 (~P5(f13(a12,a3),f14(f13(x29251,a6)))), % 117.94/118.03 inference(scs_inference,[],[2875,2882,2861,2886,2844,2877,2649,806,262,1219,538,2825,2533,2601,474,47,37,2,52,51,50,13,3,43,48,20,18])). % 117.94/118.03 cnf(2934,plain, % 117.94/118.03 (P3(f13(x29341,a3))), % 117.94/118.03 inference(scs_inference,[],[28,47])). % 117.94/118.03 cnf(2936,plain, % 117.94/118.03 (E(f13(x29361,a6),a1)), % 117.94/118.03 inference(scs_inference,[],[2918,28,47,37])). % 117.94/118.03 cnf(2938,plain, % 117.94/118.03 (E(f13(f13(x29381,a6),x29382),f13(a1,x29382))), % 117.94/118.03 inference(scs_inference,[],[2918,28,47,37,10])). % 117.94/118.03 cnf(2939,plain, % 117.94/118.03 (E(f10(f13(x29391,a6)),f10(a1))), % 117.94/118.03 inference(scs_inference,[],[2918,28,47,37,10,7])). % 117.94/118.03 cnf(2942,plain, % 117.94/118.03 (E(f13(x29421,f13(x29422,a6)),f13(x29421,a1))), % 117.94/118.03 inference(scs_inference,[],[2918,28,47,37,10,7,5,12,11])). % 117.94/118.03 cnf(2943,plain, % 117.94/118.03 (E(f5(f13(x29431,a6),x29432),f5(a1,x29432))), % 117.94/118.03 inference(scs_inference,[],[2918,28,47,37,10,7,5,12,11,8])). % 117.94/118.03 cnf(2944,plain, % 117.94/118.03 (E(f5(x29441,f13(x29442,a6)),f5(x29441,a1))), % 117.94/118.03 inference(scs_inference,[],[2918,28,47,37,10,7,5,12,11,8,9])). % 117.94/118.03 cnf(2946,plain, % 117.94/118.03 (E(f14(f13(x29461,a6)),f14(a1))), % 117.94/118.03 inference(scs_inference,[],[2918,28,47,37,10,7,5,12,11,8,9,4,6])). % 117.94/118.03 cnf(2947,plain, % 117.94/118.03 (~E(f7(a11),a1)), % 117.94/118.03 inference(scs_inference,[],[2916,2918,28,47,37,10,7,5,12,11,8,9,4,6,2])). % 117.94/118.03 cnf(2948,plain, % 117.94/118.03 (~P4(f14(a8),f5(f14(a8),a1))), % 117.94/118.03 inference(scs_inference,[],[2916,2918,2921,28,47,37,10,7,5,12,11,8,9,4,6,2,50])). % 117.94/118.03 cnf(2950,plain, % 117.94/118.03 (P4(f5(f10(x29501),a6),f10(x29501))), % 117.94/118.03 inference(scs_inference,[],[2916,2918,2921,731,28,47,37,10,7,5,12,11,8,9,4,6,2,50,52])). % 117.94/118.03 cnf(2952,plain, % 117.94/118.03 (~P2(f10(x29521),f10(a6))), % 117.94/118.03 inference(scs_inference,[],[2916,2918,2921,731,28,47,37,10,7,5,12,11,8,9,4,6,2,50,52,51])). % 117.94/118.03 cnf(2954,plain, % 117.94/118.03 (E(f13(f13(x29541,a2),f13(x29542,a2)),f13(a1,a1))), % 117.94/118.03 inference(scs_inference,[],[2916,2918,2921,2693,2699,731,28,47,37,10,7,5,12,11,8,9,4,6,2,50,52,51,3])). % 117.94/118.03 cnf(2957,plain, % 117.94/118.03 (P2(f5(a8,a1),a8)), % 117.94/118.03 inference(scs_inference,[],[2916,2918,2921,2867,2693,2699,731,2776,28,47,37,10,7,5,12,11,8,9,4,6,2,50,52,51,3,19])). % 117.94/118.03 cnf(2959,plain, % 117.94/118.03 (P2(f4(f9(a2)),f9(a1))), % 117.94/118.03 inference(scs_inference,[],[2916,2918,2921,2867,2693,2699,2506,731,2776,28,31,47,37,10,7,5,12,11,8,9,4,6,2,50,52,51,3,19,20])). % 117.94/118.03 cnf(2960,plain, % 117.94/118.03 (P2(f4(x29601),x29601)), % 117.94/118.03 inference(rename_variables,[],[31])). % 117.94/118.03 cnf(2966,plain, % 117.94/118.03 (P5(x29661,x29661)), % 117.94/118.03 inference(rename_variables,[],[30])). % 117.94/118.03 cnf(2969,plain, % 117.94/118.03 (P1(f4(f10(a2)))), % 117.94/118.03 inference(scs_inference,[],[2916,2918,2887,2909,2921,2867,2925,2906,2693,2699,2506,731,2776,2479,244,30,2966,63,28,31,2960,47,37,10,7,5,12,11,8,9,4,6,2,50,52,51,3,19,20,15,13,54,17,18,48])). % 117.94/118.03 cnf(2973,plain, % 117.94/118.03 (P2(f5(f10(x29731),a6),f10(x29731))), % 117.94/118.03 inference(scs_inference,[],[2916,2918,2887,2909,2921,2867,2925,2906,2693,2699,2506,731,2776,2479,244,30,2966,63,28,31,2960,47,37,10,7,5,12,11,8,9,4,6,2,50,52,51,3,19,20,15,13,54,17,18,48,46])). % 117.94/118.03 cnf(2987,plain, % 117.94/118.03 (E(f14(f13(x29871,a1)),a1)), % 117.94/118.03 inference(scs_inference,[],[2934,2969,2716,38,47,37])). % 117.94/118.03 cnf(2990,plain, % 117.94/118.03 (P4(f5(f10(x29901),a2),f10(x29901))), % 117.94/118.03 inference(scs_inference,[],[2934,2610,2969,748,2716,38,47,37,2,52])). % 117.94/118.03 cnf(2996,plain, % 117.94/118.03 (~E(f7(a11),f13(x29961,a6))), % 117.94/118.03 inference(scs_inference,[],[2947,2934,2936,2950,2610,2969,748,2716,791,38,47,37,2,52,50,51,3])). % 117.94/118.03 cnf(2999,plain, % 117.94/118.03 (~E(f10(f10(x29991)),f10(a6))), % 117.94/118.03 inference(scs_inference,[],[2947,2934,2952,2936,2950,2973,2610,2969,2911,748,2716,791,2533,38,47,37,2,52,50,51,3,19,20])). % 117.94/118.03 cnf(3006,plain, % 117.94/118.03 (~P5(f14(a8),f13(x30061,a6))), % 117.94/118.03 inference(scs_inference,[],[22,2947,2934,2952,2936,2950,2973,2610,2866,2969,2911,748,2716,791,1231,2595,2918,2533,38,47,37,2,52,50,51,3,19,20,15,13,54,18])). % 117.94/118.03 cnf(3007,plain, % 117.94/118.03 (P4(f5(a8,a1),a8)), % 117.94/118.03 inference(scs_inference,[],[22,2947,2934,2952,2957,2936,2950,2973,2610,2866,2969,2911,748,2716,791,1231,2595,2918,2533,33,38,47,37,2,52,50,51,3,19,20,15,13,54,18,48])). % 117.94/118.03 cnf(3009,plain, % 117.94/118.03 (P2(f5(f10(x30091),a2),f10(x30091))), % 117.94/118.03 inference(scs_inference,[],[22,2947,2934,2952,2957,2936,2950,2973,2610,2866,2969,2911,748,2716,791,1231,2595,2918,2533,33,38,47,37,2,52,50,51,3,19,20,15,13,54,18,48,46])). % 117.94/118.03 cnf(3020,plain, % 117.94/118.03 (E(f13(f9(x30201),x30202),f13(a1,x30202))), % 117.94/118.03 inference(scs_inference,[],[29,37,10])). % 117.94/118.03 cnf(3021,plain, % 117.94/118.03 (E(f4(f9(x30211)),f4(a1))), % 117.94/118.03 inference(scs_inference,[],[29,37,10,5])). % 117.94/118.03 cnf(3022,plain, % 117.94/118.03 (E(f10(f9(x30221)),f10(a1))), % 117.94/118.03 inference(scs_inference,[],[29,37,10,5,7])). % 117.94/118.03 cnf(3023,plain, % 117.94/118.03 (E(f13(x30231,f9(x30232)),f13(x30231,a1))), % 117.94/118.03 inference(scs_inference,[],[29,37,10,5,7,11])). % 117.94/118.03 cnf(3027,plain, % 117.94/118.03 (E(f5(x30271,f9(x30272)),f5(x30271,a1))), % 117.94/118.03 inference(scs_inference,[],[29,37,10,5,7,11,12,8,4,9])). % 117.94/118.03 cnf(3028,plain, % 117.94/118.03 (E(f14(f9(x30281)),f14(a1))), % 117.94/118.03 inference(scs_inference,[],[29,37,10,5,7,11,12,8,4,9,6])). % 117.94/118.03 cnf(3029,plain, % 117.94/118.03 (~E(f13(x30291,a6),f7(a11))), % 117.94/118.03 inference(scs_inference,[],[2996,29,37,10,5,7,11,12,8,4,9,6,2])). % 117.94/118.03 cnf(3030,plain, % 117.94/118.03 (~P4(a8,f5(a8,a1))), % 117.94/118.03 inference(scs_inference,[],[2996,3007,29,37,10,5,7,11,12,8,4,9,6,2,50])). % 117.94/118.03 cnf(3032,plain, % 117.94/118.03 (P4(f5(f14(a8),f13(x30321,a6)),f14(a8))), % 117.94/118.03 inference(scs_inference,[],[2996,3006,3007,29,37,10,5,7,11,12,8,4,9,6,2,50,52])). % 117.94/118.03 cnf(3036,plain, % 117.94/118.03 (E(f13(f13(x30361,a6),f13(x30362,a6)),f13(a1,a1))), % 117.94/118.03 inference(scs_inference,[],[2996,3006,3007,2938,2942,1227,29,37,10,5,7,11,12,8,4,9,6,2,50,52,51,3])). % 117.94/118.03 cnf(3039,plain, % 117.94/118.03 (P2(f5(a1,x30391),f10(f5(a2,x30391)))), % 117.94/118.03 inference(scs_inference,[],[2996,3006,3007,2938,2942,2509,1227,2533,29,37,10,5,7,11,12,8,4,9,6,2,50,52,51,3,19])). % 117.94/118.03 cnf(3042,plain, % 117.94/118.03 (P2(f4(x30421),x30421)), % 117.94/118.03 inference(rename_variables,[],[31])). % 117.94/118.03 cnf(3046,plain, % 117.94/118.03 (~P2(a8,f10(a1))), % 117.94/118.03 inference(scs_inference,[],[22,2996,3006,3007,2938,2942,2944,2948,2509,1227,280,2533,29,31,37,10,5,7,11,12,8,4,9,6,2,50,52,51,3,19,20,15,13,54])). % 117.94/118.03 cnf(3048,plain, % 117.94/118.03 (~P5(f10(x30481),f14(f13(x30482,a1)))), % 117.94/118.03 inference(scs_inference,[],[22,2996,3006,3007,2938,2942,2944,2948,2987,2509,1215,1227,280,2533,29,31,37,10,5,7,11,12,8,4,9,6,2,50,52,51,3,19,20,15,13,54,18])). % 117.94/118.03 cnf(3049,plain, % 117.94/118.03 (P1(f4(f10(a6)))), % 117.94/118.03 inference(scs_inference,[],[22,2996,3006,3007,2938,2942,2944,2948,2987,2509,1215,1227,280,2533,29,116,31,3042,37,10,5,7,11,12,8,4,9,6,2,50,52,51,3,19,20,15,13,54,18,48])). % 117.94/118.03 cnf(3068,plain, % 117.94/118.03 (P4(f5(a11,f9(x30681)),a11)), % 117.94/118.03 inference(scs_inference,[],[2999,3049,775,38,37,2,52])). % 117.94/118.03 cnf(3070,plain, % 117.94/118.03 (~P4(f10(x30701),f5(f10(x30701),a2))), % 117.94/118.03 inference(scs_inference,[],[2999,3049,2990,775,38,37,2,52,50])). % 117.94/118.03 cnf(3080,plain, % 117.94/118.03 (~P2(a8,f10(f9(x30801)))), % 117.94/118.03 inference(scs_inference,[],[3046,2490,3009,2999,3022,3049,2990,775,787,2513,2533,38,37,2,52,50,51,3,55,19,20])). % 117.94/118.03 cnf(3083,plain, % 117.94/118.03 (~E(f14(f14(a6)),f13(a12,a3))), % 117.94/118.03 inference(scs_inference,[],[3046,2490,3030,3009,3027,2999,3022,3049,2990,2649,775,787,129,2513,2533,38,37,2,52,50,51,3,55,19,20,15,13])). % 117.94/118.03 cnf(3084,plain, % 117.94/118.03 (~P2(f14(a8),f10(a1))), % 117.94/118.03 inference(scs_inference,[],[22,3046,2490,3030,3009,3027,2999,3022,3032,3049,2990,2649,775,787,129,2513,2533,38,37,2,52,50,51,3,55,19,20,15,13,54])). % 117.94/118.03 cnf(3086,plain, % 117.94/118.03 (~P5(a8,f14(f13(x30861,a6)))), % 117.94/118.03 inference(scs_inference,[],[22,3046,2490,3030,3009,3027,2999,3022,2946,3032,3049,2990,2649,775,787,129,2831,2513,2533,38,37,2,52,50,51,3,55,19,20,15,13,54,18])). % 117.94/118.03 cnf(3087,plain, % 117.94/118.03 (P4(f7(a1),f10(f7(a2)))), % 117.94/118.03 inference(scs_inference,[],[22,3046,2490,3030,3009,3027,2999,3022,2946,3032,2727,3049,2990,2649,775,787,129,2831,2513,2533,35,38,37,2,52,50,51,3,55,19,20,15,13,54,18,48])). % 117.94/118.03 cnf(3094,plain, % 117.94/118.03 (E(a6,a1)), % 117.94/118.03 inference(scs_inference,[],[24,37])). % 117.94/118.03 cnf(3096,plain, % 117.94/118.03 (E(f13(a6,x30961),f13(a1,x30961))), % 117.94/118.03 inference(scs_inference,[],[24,37,10])). % 117.94/118.03 cnf(3098,plain, % 117.94/118.03 (E(f10(a6),f10(a1))), % 117.94/118.03 inference(scs_inference,[],[24,37,10,5,7])). % 117.94/118.03 cnf(3099,plain, % 117.94/118.03 (E(f7(a6),f7(a1))), % 117.94/118.03 inference(scs_inference,[],[24,37,10,5,7,12])). % 117.94/118.03 cnf(3100,plain, % 117.94/118.04 (E(f13(x31001,a6),f13(x31001,a1))), % 117.94/118.04 inference(scs_inference,[],[24,37,10,5,7,12,11])). % 117.94/118.04 cnf(3102,plain, % 117.94/118.04 (E(f9(a6),f9(a1))), % 117.94/118.04 inference(scs_inference,[],[24,37,10,5,7,12,11,8,4])). % 117.94/118.04 cnf(3103,plain, % 117.94/118.04 (E(f5(x31031,a6),f5(x31031,a1))), % 117.94/118.04 inference(scs_inference,[],[24,37,10,5,7,12,11,8,4,9])). % 117.94/118.04 cnf(3104,plain, % 117.94/118.04 (E(f14(a6),f14(a1))), % 117.94/118.04 inference(scs_inference,[],[24,37,10,5,7,12,11,8,4,9,6])). % 117.94/118.04 cnf(3106,plain, % 117.94/118.04 (P4(f5(a8,f9(x31061)),a8)), % 117.94/118.04 inference(scs_inference,[],[3083,756,24,37,10,5,7,12,11,8,4,9,6,2,52])). % 117.94/118.04 cnf(3108,plain, % 117.94/118.04 (~P4(f10(f7(a2)),f7(a1))), % 117.94/118.04 inference(scs_inference,[],[3083,3087,756,24,37,10,5,7,12,11,8,4,9,6,2,52,50])). % 117.94/118.04 cnf(3110,plain, % 117.94/118.04 (~P2(f13(a12,a3),f10(a1))), % 117.94/118.04 inference(scs_inference,[],[3083,3087,756,1219,24,37,10,5,7,12,11,8,4,9,6,2,52,50,51])). % 117.94/118.04 cnf(3112,plain, % 117.94/118.04 (E(f13(f9(x31121),f9(x31122)),f13(a1,a1))), % 117.94/118.04 inference(scs_inference,[],[3020,3023,3083,3087,756,1219,24,37,10,5,7,12,11,8,4,9,6,2,52,50,51,3])). % 117.94/118.04 cnf(3115,plain, % 117.94/118.04 (P2(f14(a1),f10(x31151))), % 117.94/118.04 inference(scs_inference,[],[3020,3023,3083,3028,3087,503,756,1219,24,37,10,5,7,12,11,8,4,9,6,2,52,50,51,3,19])). % 117.94/118.04 cnf(3116,plain, % 117.94/118.04 (E(f14(f9(x31161)),f14(a1))), % 117.94/118.04 inference(rename_variables,[],[3028])). % 117.94/118.04 cnf(3122,plain, % 117.94/118.04 (~P2(f7(a8),f10(a1))), % 117.94/118.04 inference(scs_inference,[],[22,3020,3023,3083,3028,3116,3087,2644,270,3030,503,756,1219,538,24,435,37,10,5,7,12,11,8,4,9,6,2,52,50,51,3,19,20,15,13,54])). % 117.94/118.04 cnf(3133,plain, % 117.94/118.04 (~P1(f5(f10(a8),f10(a1)))), % 117.94/118.04 inference(scs_inference,[],[22,3020,3023,3083,3028,3116,3048,3087,2644,270,3030,2943,503,756,1219,538,368,24,30,435,37,10,5,7,12,11,8,4,9,6,2,52,50,51,3,19,20,15,13,54,18,46,2100,55,347])). % 117.94/118.04 cnf(3140,plain, % 117.94/118.04 (P4(f5(f10(x31401),a1),f10(x31401))), % 117.94/118.04 inference(scs_inference,[],[2796,3068,1215,2,50,52])). % 117.94/118.04 cnf(3142,plain, % 117.94/118.04 (~P2(f7(a8),f10(a6))), % 117.94/118.04 inference(scs_inference,[],[2796,3068,1215,830,2,50,52,51])). % 117.94/118.04 cnf(3144,plain, % 117.94/118.04 (~E(a8,f14(a6))), % 117.94/118.04 inference(scs_inference,[],[3104,2704,2796,3068,1215,830,2,50,52,51,3])). % 117.94/118.04 cnf(3145,plain, % 117.94/118.04 (P2(f5(f10(x31451),a1),f10(x31451))), % 117.94/118.04 inference(scs_inference,[],[3104,2704,2796,3068,1215,830,2533,2,50,52,51,3,55])). % 117.94/118.04 cnf(3146,plain, % 117.94/118.04 (P2(x31461,f10(x31461))), % 117.94/118.04 inference(rename_variables,[],[2533])). % 117.94/118.04 cnf(3148,plain, % 117.94/118.04 (~E(f14(a1),f7(a8))), % 117.94/118.04 inference(scs_inference,[],[3115,3104,3122,2704,2796,3068,1215,830,2533,2,50,52,51,3,55,19])). % 117.94/118.04 cnf(3152,plain, % 117.94/118.04 (~P4(f5(f14(a8),f13(a1,a2)),f13(a6,a2))), % 117.94/118.04 inference(scs_inference,[],[3096,3115,3104,3122,2704,2803,2796,3068,3080,1215,830,2533,3146,2,50,52,51,3,55,19,20,15])). % 117.94/118.04 cnf(3158,plain, % 117.94/118.04 (~P5(a8,f14(a6))), % 117.94/118.04 inference(scs_inference,[],[22,3096,3115,3104,3122,2704,2803,2796,3133,3106,3068,3080,1215,830,2831,2918,2533,3146,2,50,52,51,3,55,19,20,15,13,54,18])). % 117.94/118.04 cnf(3161,plain, % 117.94/118.04 (P1(f13(x31611,a1))), % 117.94/118.04 inference(scs_inference,[],[22,3096,3115,3098,3104,3122,2704,2803,2796,3070,3133,3106,3068,3080,2808,2716,1215,830,2831,2918,2533,3146,2,50,52,51,3,55,19,20,15,13,54,18,14,43])). % 117.94/118.04 cnf(3164,plain, % 117.94/118.04 (E(f13(x31641,a1),a1)), % 117.94/118.04 inference(scs_inference,[],[22,3096,3115,3098,3104,3122,2704,2803,2796,3070,3133,3106,3068,3080,2808,2716,1215,830,2831,2918,2533,3146,2,50,52,51,3,55,19,20,15,13,54,18,14,43,37])). % 117.94/118.04 cnf(3166,plain, % 117.94/118.04 (E(f13(f13(x31661,a1),x31662),f13(a1,x31662))), % 117.94/118.04 inference(scs_inference,[],[22,3096,3115,3098,3104,3122,2704,2803,2796,3070,3133,3106,3068,3080,2808,2716,1215,830,2831,2918,2533,3146,2,50,52,51,3,55,19,20,15,13,54,18,14,43,37,10])). % 117.94/118.04 cnf(3170,plain, % 117.94/118.04 (E(f13(x31701,f13(x31702,a1)),f13(x31701,a1))), % 117.94/118.04 inference(scs_inference,[],[22,3096,3115,3098,3104,3122,2704,2803,2796,3070,3133,3106,3068,3080,2808,2716,1215,830,2831,2918,2533,3146,2,50,52,51,3,55,19,20,15,13,54,18,14,43,37,10,5,12,7,11])). % 117.94/118.04 cnf(3171,plain, % 117.94/118.04 (E(f5(f13(x31711,a1),x31712),f5(a1,x31712))), % 117.94/118.04 inference(scs_inference,[],[22,3096,3115,3098,3104,3122,2704,2803,2796,3070,3133,3106,3068,3080,2808,2716,1215,830,2831,2918,2533,3146,2,50,52,51,3,55,19,20,15,13,54,18,14,43,37,10,5,12,7,11,8])). % 117.94/118.04 cnf(3173,plain, % 117.94/118.04 (E(f5(x31731,f13(x31732,a1)),f5(x31731,a1))), % 117.94/118.04 inference(scs_inference,[],[22,3096,3115,3098,3104,3122,2704,2803,2796,3070,3133,3106,3068,3080,2808,2716,1215,830,2831,2918,2533,3146,2,50,52,51,3,55,19,20,15,13,54,18,14,43,37,10,5,12,7,11,8,4,9])). % 117.94/118.04 cnf(3174,plain, % 117.94/118.04 (E(f14(f13(x31741,a1)),f14(a1))), % 117.94/118.04 inference(scs_inference,[],[22,3096,3115,3098,3104,3122,2704,2803,2796,3070,3133,3106,3068,3080,2808,2716,1215,830,2831,2918,2533,3146,2,50,52,51,3,55,19,20,15,13,54,18,14,43,37,10,5,12,7,11,8,4,9,6])). % 117.94/118.04 cnf(3180,plain, % 117.94/118.04 (~E(f7(a8),f14(a1))), % 117.94/118.04 inference(scs_inference,[],[3148,2])). % 117.94/118.04 cnf(3181,plain, % 117.94/118.04 (~P4(f10(x31811),f5(f10(x31811),a1))), % 117.94/118.04 inference(scs_inference,[],[3148,3140,2,50])). % 117.94/118.04 cnf(3185,plain, % 117.94/118.04 (~P2(f7(a8),f10(a2))), % 117.94/118.04 inference(scs_inference,[],[3148,3158,3140,826,2,50,52,51])). % 117.94/118.04 cnf(3187,plain, % 117.94/118.04 (~E(f13(x31871,a1),f7(a11))), % 117.94/118.04 inference(scs_inference,[],[3100,3029,3148,3158,3140,826,2,50,52,51,3])). % 117.94/118.04 cnf(3198,plain, % 117.94/118.04 (P5(x31981,x31981)), % 117.94/118.04 inference(rename_variables,[],[30])). % 117.94/118.04 cnf(3201,plain, % 117.94/118.04 (~P1(f5(f10(a8),f10(a6)))), % 117.94/118.04 inference(scs_inference,[],[22,3094,3099,3100,3142,3029,3148,3158,3140,3108,3086,826,2533,368,30,3198,536,31,2,50,52,51,3,55,19,20,15,13,17,18,347])). % 117.94/118.04 cnf(3208,plain, % 117.94/118.04 (P4(f5(a1,x32081),f10(f5(a2,x32081)))), % 117.94/118.04 inference(scs_inference,[],[22,3094,3099,3100,3142,3029,3148,3158,3140,3171,3108,3039,3086,826,2533,368,30,3198,536,35,31,2,50,52,51,3,55,19,20,15,13,17,18,347,46,344,48])). % 117.94/118.04 cnf(3215,plain, % 117.94/118.04 (~P4(f10(f5(a2,x32151)),f5(a1,x32151))), % 117.94/118.04 inference(scs_inference,[],[3144,3208,2,50])). % 117.94/118.04 cnf(3217,plain, % 117.94/118.04 (P4(f5(f7(a8),a1),f7(a8))), % 117.94/118.04 inference(scs_inference,[],[3144,3208,1234,2,50,52])). % 117.94/118.04 cnf(3219,plain, % 117.94/118.04 (~P2(f14(a8),f10(f9(x32191)))), % 117.94/118.04 inference(scs_inference,[],[3144,3208,1234,795,2,50,52,51])). % 117.94/118.04 cnf(3228,plain, % 117.94/118.04 (~E(f14(a8),f13(a6,a2))), % 117.94/118.04 inference(scs_inference,[],[2846,3144,3185,3152,3174,3208,3145,2813,1234,795,2533,368,2,50,52,51,3,55,19,20,15])). % 117.94/118.04 cnf(3231,plain, % 117.94/118.04 (~P4(f10(a6),f5(f10(a1),a1))), % 117.94/118.04 inference(scs_inference,[],[22,2846,3144,3185,3152,3174,3181,3208,3201,3145,2813,3098,1234,795,2533,368,2,50,52,51,3,55,19,20,15,13,14])). % 117.94/118.04 cnf(3234,plain, % 117.94/118.04 (~P1(f5(f10(a8),f10(a2)))), % 117.94/118.04 inference(scs_inference,[],[22,2846,3144,3185,3152,3174,3181,3208,3201,3145,2813,3098,1234,2831,795,2533,368,2,50,52,51,3,55,19,20,15,13,14,18,347])). % 117.94/118.04 cnf(3244,plain, % 117.94/118.04 (~E(f7(a11),f13(x32441,a1))), % 117.94/118.04 inference(scs_inference,[],[3187,2])). % 117.94/118.04 cnf(3247,plain, % 117.94/118.04 (P4(f5(a11,a1),a11)), % 117.94/118.04 inference(scs_inference,[],[3187,3217,1227,2,50,52])). % 117.94/118.04 cnf(3261,plain, % 117.94/118.04 (~E(f5(f7(a8),a1),f10(a8))), % 117.94/118.04 inference(scs_inference,[],[22,3187,3112,3215,3217,3234,2959,3102,3103,3164,3021,371,1227,715,31,2,50,52,51,3,19,20,15,13,14])). % 117.94/118.04 cnf(3275,plain, % 117.94/118.04 (~E(f13(a6,a2),f14(a8))), % 117.94/118.04 inference(scs_inference,[],[3228,2])). % 117.94/118.04 cnf(3278,plain, % 117.94/118.04 (P4(f5(a11,a2),a11)), % 117.94/118.04 inference(scs_inference,[],[3228,3247,787,2,50,52])). % 117.94/118.04 cnf(3280,plain, % 117.94/118.04 (~P2(a11,f10(a6))), % 117.94/118.04 inference(scs_inference,[],[3228,3247,787,771,2,50,52,51])). % 117.94/118.04 cnf(3284,plain, % 117.94/118.04 (~E(f14(a1),f14(a8))), % 117.94/118.04 inference(scs_inference,[],[3228,3244,3247,3036,3219,3115,787,771,2,50,52,51,3,19])). % 117.94/118.04 cnf(3301,plain, % 117.94/118.04 (P4(f5(f13(a12,a3),a1),f13(a12,a3))), % 117.94/118.04 inference(scs_inference,[],[3278,3284,1219,2,50,52])). % 117.94/118.04 cnf(3305,plain, % 117.94/118.04 (E(f13(f13(x33051,a2),f13(x33052,a2)),a1)), % 117.94/118.04 inference(scs_inference,[],[3278,3284,2954,3164,1219,814,2,50,52,51,3])). % 117.94/118.04 cnf(3323,plain, % 117.94/118.04 (~P4(f13(a12,a3),f5(f13(a12,a3),a1))), % 117.94/118.04 inference(scs_inference,[],[3261,3301,2,50])). % 117.94/118.04 cnf(3325,plain, % 117.94/118.04 (P4(f5(f7(a8),a6),f7(a8))), % 117.94/118.04 inference(scs_inference,[],[3261,3301,830,2,50,52])). % 117.94/118.04 cnf(3327,plain, % 117.94/118.04 (~P5(f14(a8),f13(f13(x33271,a2),f13(x33272,a2)))), % 117.94/118.04 inference(scs_inference,[],[3261,3301,3305,1231,830,2,50,52,18])). % 117.94/118.04 cnf(3328,plain, % 117.94/118.04 (~E(f13(a6,a1),f14(a8))), % 117.94/118.04 inference(scs_inference,[],[3275,3261,3301,3305,2512,1231,830,2,50,52,18,3])). % 117.94/118.04 cnf(3332,plain, % 117.94/118.04 (~E(f10(a11),f10(a6))), % 117.94/118.04 inference(scs_inference,[],[3275,3261,3301,3305,3280,2973,2512,1231,830,2533,2,50,52,18,3,19,20])). % 117.94/118.04 cnf(3348,plain, % 117.94/118.04 (P4(f5(f7(a8),a2),f7(a8))), % 117.94/118.04 inference(scs_inference,[],[3328,3325,826,2,50,52])). % 117.94/118.04 cnf(3351,plain, % 117.94/118.04 (P5(x33511,x33511)), % 117.94/118.04 inference(rename_variables,[],[30])). % 117.94/118.04 cnf(3352,plain, % 117.94/118.04 (E(f13(f14(a1),f14(a1)),a1)), % 117.94/118.04 inference(scs_inference,[],[3328,2854,3325,3327,3164,826,30,2,50,52,18,3])). % 117.94/118.04 cnf(3359,plain, % 117.94/118.04 (P5(f13(a1,a1),f13(f14(a1),f14(a1)))), % 117.94/118.04 inference(scs_inference,[],[23,3328,2854,3325,3327,3110,2939,3234,2564,2339,3164,826,2533,30,3351,2,50,52,18,3,19,20,15,13,17])). % 117.94/118.04 cnf(3376,plain, % 117.94/118.04 (P4(f5(f14(a8),f9(x33761)),f14(a8))), % 117.94/118.04 inference(scs_inference,[],[3332,3348,795,2,50,52])). % 117.94/118.04 cnf(3378,plain, % 117.94/118.04 (~P5(a8,f13(f14(a1),f14(a1)))), % 117.94/118.04 inference(scs_inference,[],[3332,3348,3352,1223,795,2,50,52,18])). % 117.94/118.04 cnf(3387,plain, % 117.94/118.04 (~E(f13(a1,a1),a8)), % 117.94/118.04 inference(scs_inference,[],[23,3180,3332,3348,3323,3359,3352,2701,2569,3084,3009,2944,3133,1223,795,2533,2,50,52,18,3,19,15,20,13,17])). % 117.94/118.04 cnf(3400,plain, % 117.94/118.04 (P5(x34001,x34001)), % 117.94/118.04 inference(rename_variables,[],[30])). % 117.94/118.04 cnf(3403,plain, % 117.94/118.04 (E(f13(f13(x34031,a1),x34032),f13(a1,x34032))), % 117.94/118.04 inference(rename_variables,[],[3166])). % 117.94/118.04 cnf(3415,plain, % 117.94/118.04 (P2(f5(f10(x34151),f9(x34152)),f10(x34151))), % 117.94/118.04 inference(scs_inference,[],[23,3387,3166,3403,3170,3376,3231,3378,3173,2659,3201,3161,715,2533,30,3400,31,2,50,52,18,3,19,15,20,54,13,17,46])). % 117.94/118.04 cnf(4582,plain, % 117.94/118.04 ($false), % 117.94/118.04 inference(scs_inference,[],[36,2513,3415,2292,2,51,56]), % 117.94/118.04 ['proof']). % 117.94/118.04 % SZS output end Proof % 117.94/118.04 % Total time :117.300000s %------------------------------------------------------------------------------