%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU171+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 : n023.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:32 EDT 2024 % Result : Theorem 31.41s 31.49s % Output : CNFRefutation 31.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SEU171+1 : TPTP v8.2.0. Released v3.3.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n023.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Fri Jun 21 17:19:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.49/0.59 start to proof:theBenchmark % 31.41/31.47 %------------------------------------------- % 31.41/31.47 % File :CSE---1.7 % 31.41/31.47 % Problem :theBenchmark % 31.41/31.47 % Transform :cnf % 31.41/31.47 % Format :tptp:raw % 31.41/31.47 % Command :java -jar mcs_scs.jar %d %s % 31.41/31.47 % 31.41/31.47 % Result :Theorem 30.850000s % 31.41/31.47 % Output :CNFRefutation 30.850000s % 31.41/31.47 %------------------------------------------- % 31.41/31.48 %------------------------------------------------------------------------------ % 31.41/31.48 % File : SEU171+1 : TPTP v8.2.0. Released v3.3.0. % 31.41/31.48 % Domain : Set theory % 31.41/31.48 % Problem : MPTP bushy problem t50_subset_1 % 31.41/31.48 % Version : [Urb07] axioms : Especial. % 31.41/31.48 % English : % 31.41/31.48 % 31.41/31.48 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 31.41/31.48 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 31.41/31.48 % Source : [Urb07] % 31.41/31.48 % Names : bushy-t50_subset_1 [Urb07] % 31.41/31.48 % 31.41/31.48 % Status : Theorem % 31.41/31.48 % Rating : 0.19 v7.5.0, 0.22 v7.4.0, 0.13 v7.3.0, 0.14 v7.1.0, 0.13 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.21 v6.2.0, 0.32 v6.1.0, 0.33 v6.0.0, 0.35 v5.5.0, 0.30 v5.4.0, 0.32 v5.3.0, 0.33 v5.2.0, 0.15 v5.1.0, 0.14 v5.0.0, 0.21 v4.1.0, 0.22 v4.0.1, 0.26 v4.0.0, 0.29 v3.7.0, 0.25 v3.5.0, 0.26 v3.4.0, 0.32 v3.3.0 % 31.41/31.48 % Syntax : Number of formulae : 23 ( 11 unt; 0 def) % 31.41/31.48 % Number of atoms : 46 ( 8 equ) % 31.41/31.48 % Maximal formula atoms : 6 ( 2 avg) % 31.41/31.48 % Number of connectives : 35 ( 12 ~; 0 |; 7 &) % 31.41/31.48 % ( 4 <=>; 12 =>; 0 <=; 0 <~>) % 31.41/31.48 % Maximal formula depth : 9 ( 4 avg) % 31.41/31.48 % Maximal term depth : 3 ( 1 avg) % 31.41/31.48 % Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty) % 31.41/31.48 % Number of functors : 4 ( 4 usr; 1 con; 0-2 aty) % 31.41/31.48 % Number of variables : 33 ( 28 !; 5 ?) % 31.41/31.48 % SPC : FOF_THM_RFO_SEQ % 31.41/31.48 % 31.41/31.48 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 31.41/31.48 % library, www.mizar.org % 31.41/31.48 %------------------------------------------------------------------------------ % 31.41/31.48 fof(antisymmetry_r2_hidden,axiom, % 31.41/31.48 ! [A,B] : % 31.41/31.48 ( in(A,B) % 31.41/31.48 => ~ in(B,A) ) ). % 31.41/31.48 % 31.41/31.48 fof(d2_subset_1,axiom, % 31.41/31.48 ! [A,B] : % 31.41/31.48 ( ( ~ empty(A) % 31.41/31.48 => ( element(B,A) % 31.41/31.48 <=> in(B,A) ) ) % 31.41/31.48 & ( empty(A) % 31.41/31.48 => ( element(B,A) % 31.41/31.48 <=> empty(B) ) ) ) ). % 31.41/31.48 % 31.41/31.48 fof(d4_xboole_0,axiom, % 31.41/31.48 ! [A,B,C] : % 31.41/31.48 ( C = set_difference(A,B) % 31.41/31.48 <=> ! [D] : % 31.41/31.48 ( in(D,C) % 31.41/31.48 <=> ( in(D,A) % 31.41/31.48 & ~ in(D,B) ) ) ) ). % 31.41/31.48 % 31.41/31.48 fof(d5_subset_1,axiom, % 31.41/31.48 ! [A,B] : % 31.41/31.48 ( element(B,powerset(A)) % 31.41/31.48 => subset_complement(A,B) = set_difference(A,B) ) ). % 31.41/31.48 % 31.41/31.48 fof(dt_k1_xboole_0,axiom, % 31.41/31.48 $true ). % 31.41/31.48 % 31.41/31.48 fof(dt_k1_zfmisc_1,axiom, % 31.41/31.48 $true ). % 31.41/31.48 % 31.41/31.48 fof(dt_k3_subset_1,axiom, % 31.41/31.48 ! [A,B] : % 31.41/31.48 ( element(B,powerset(A)) % 31.41/31.48 => element(subset_complement(A,B),powerset(A)) ) ). % 31.41/31.48 % 31.41/31.48 fof(dt_k4_xboole_0,axiom, % 31.41/31.48 $true ). % 31.41/31.48 % 31.41/31.48 fof(dt_m1_subset_1,axiom, % 31.41/31.48 $true ). % 31.41/31.48 % 31.41/31.48 fof(existence_m1_subset_1,axiom, % 31.41/31.48 ! [A] : % 31.41/31.48 ? [B] : element(B,A) ). % 31.41/31.48 % 31.41/31.48 fof(fc1_subset_1,axiom, % 31.41/31.48 ! [A] : ~ empty(powerset(A)) ). % 31.41/31.48 % 31.41/31.48 fof(fc1_xboole_0,axiom, % 31.41/31.48 empty(empty_set) ). % 31.41/31.48 % 31.41/31.48 fof(involutiveness_k3_subset_1,axiom, % 31.41/31.48 ! [A,B] : % 31.41/31.48 ( element(B,powerset(A)) % 31.41/31.48 => subset_complement(A,subset_complement(A,B)) = B ) ). % 31.41/31.48 % 31.41/31.48 fof(rc1_subset_1,axiom, % 31.41/31.48 ! [A] : % 31.41/31.48 ( ~ empty(A) % 31.41/31.48 => ? [B] : % 31.41/31.48 ( element(B,powerset(A)) % 31.41/31.48 & ~ empty(B) ) ) ). % 31.41/31.48 % 31.41/31.48 fof(rc1_xboole_0,axiom, % 31.41/31.48 ? [A] : empty(A) ). % 31.41/31.48 % 31.41/31.48 fof(rc2_subset_1,axiom, % 31.41/31.48 ! [A] : % 31.41/31.48 ? [B] : % 31.41/31.48 ( element(B,powerset(A)) % 31.41/31.48 & empty(B) ) ). % 31.41/31.48 % 31.41/31.48 fof(rc2_xboole_0,axiom, % 31.41/31.48 ? [A] : ~ empty(A) ). % 31.41/31.48 % 31.41/31.48 fof(t3_boole,axiom, % 31.41/31.48 ! [A] : set_difference(A,empty_set) = A ). % 31.41/31.48 % 31.41/31.48 fof(t4_boole,axiom, % 31.41/31.48 ! [A] : set_difference(empty_set,A) = empty_set ). % 31.41/31.48 % 31.41/31.48 fof(t50_subset_1,conjecture, % 31.41/31.48 ! [A] : % 31.41/31.48 ( A != empty_set % 31.41/31.48 => ! [B] : % 31.41/31.48 ( element(B,powerset(A)) % 31.41/31.48 => ! [C] : % 31.41/31.48 ( element(C,A) % 31.41/31.48 => ( ~ in(C,B) % 31.41/31.48 => in(C,subset_complement(A,B)) ) ) ) ) ). % 31.41/31.48 % 31.41/31.48 fof(t6_boole,axiom, % 31.41/31.48 ! [A] : % 31.41/31.48 ( empty(A) % 31.41/31.48 => A = empty_set ) ). % 31.41/31.48 % 31.41/31.48 fof(t7_boole,axiom, % 31.41/31.48 ! [A,B] : % 31.41/31.48 ~ ( in(A,B) % 31.41/31.48 & empty(B) ) ). % 31.41/31.48 % 31.41/31.48 fof(t8_boole,axiom, % 31.41/31.48 ! [A,B] : % 31.41/31.48 ~ ( empty(A) % 31.41/31.48 & A != B % 31.41/31.48 & empty(B) ) ). % 31.41/31.48 % 31.41/31.48 %------------------------------------------------------------------------------ % 31.41/31.49 %------------------------------------------- % 31.41/31.49 % Proof found % 31.41/31.49 % SZS status Theorem for theBenchmark % 31.41/31.49 % SZS output start Proof % 31.41/31.49 %ClaNum:52(EqnAxiom:19) % 31.41/31.49 %VarNum:122(SingletonVarNum:50) % 31.41/31.49 %MaxLitNum:4 % 31.41/31.49 %MaxfuncDepth:2 % 31.41/31.49 %SharedTerms:16 % 31.41/31.49 %goalClause: 23 26 29 32 33 % 31.41/31.49 %singleGoalClaCount:5 % 31.41/31.49 [20]P1(a1) % 31.41/31.49 [21]P1(a2) % 31.41/31.49 [23]P2(a7,a8) % 31.41/31.49 [29]~E(a8,a1) % 31.41/31.49 [30]~P1(a9) % 31.41/31.49 [32]~P3(a7,a10) % 31.41/31.49 [26]P2(a10,f12(a8)) % 31.41/31.49 [33]~P3(a7,f13(a8,a10)) % 31.41/31.49 [22]P1(f6(x221)) % 31.41/31.49 [24]E(f11(a1,x241),a1) % 31.41/31.49 [25]E(f11(x251,a1),x251) % 31.41/31.49 [27]P2(f3(x271),x271) % 31.41/31.49 [28]P2(f6(x281),f12(x281)) % 31.41/31.49 [31]~P1(f12(x311)) % 31.41/31.49 [34]~P1(x341)+E(x341,a1) % 31.41/31.49 [36]P1(x361)+~P1(f5(x361)) % 31.41/31.49 [39]P1(x391)+P2(f5(x391),f12(x391)) % 31.41/31.49 [38]~P1(x381)+~P3(x382,x381) % 31.41/31.49 [43]~P3(x432,x431)+~P3(x431,x432) % 31.41/31.49 [44]~P2(x442,f12(x441))+E(f13(x441,x442),f11(x441,x442)) % 31.41/31.49 [49]~P2(x492,f12(x491))+P2(f13(x491,x492),f12(x491)) % 31.41/31.49 [47]~P2(x472,f12(x471))+E(f13(x471,f13(x471,x472)),x472) % 31.41/31.49 [35]~P1(x352)+~P1(x351)+E(x351,x352) % 31.41/31.49 [37]~P1(x372)+~P1(x371)+P2(x371,x372) % 31.41/31.49 [40]~P2(x401,x402)+P1(x401)+~P1(x402) % 31.41/31.49 [41]~P2(x412,x411)+P1(x411)+P3(x412,x411) % 31.41/31.49 [42]~P3(x422,x421)+P1(x421)+P2(x422,x421) % 31.41/31.49 [50]P3(f4(x502,x503,x501),x501)+P3(f4(x502,x503,x501),x502)+E(x501,f11(x502,x503)) % 31.41/31.49 [51]P3(f4(x512,x513,x511),x511)+~P3(f4(x512,x513,x511),x513)+E(x511,f11(x512,x513)) % 31.41/31.49 [45]~P3(x451,x453)+P3(x451,x452)+~E(x453,f11(x452,x454)) % 31.41/31.49 [46]~P3(x464,x463)+~P3(x464,x461)+~E(x461,f11(x462,x463)) % 31.41/31.49 [52]P3(f4(x522,x523,x521),x523)+~P3(f4(x522,x523,x521),x521)+~P3(f4(x522,x523,x521),x522)+E(x521,f11(x522,x523)) % 31.41/31.49 [48]~P3(x481,x484)+P3(x481,x482)+P3(x481,x483)+~E(x482,f11(x484,x483)) % 31.41/31.49 %EqnAxiom % 31.41/31.49 [1]E(x11,x11) % 31.41/31.49 [2]E(x22,x21)+~E(x21,x22) % 31.41/31.49 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 31.41/31.49 [4]~E(x41,x42)+E(f6(x41),f6(x42)) % 31.41/31.49 [5]~E(x51,x52)+E(f11(x51,x53),f11(x52,x53)) % 31.41/31.49 [6]~E(x61,x62)+E(f11(x63,x61),f11(x63,x62)) % 31.41/31.49 [7]~E(x71,x72)+E(f4(x71,x73,x74),f4(x72,x73,x74)) % 31.41/31.49 [8]~E(x81,x82)+E(f4(x83,x81,x84),f4(x83,x82,x84)) % 31.41/31.49 [9]~E(x91,x92)+E(f4(x93,x94,x91),f4(x93,x94,x92)) % 31.41/31.49 [10]~E(x101,x102)+E(f12(x101),f12(x102)) % 31.41/31.49 [11]~E(x111,x112)+E(f3(x111),f3(x112)) % 31.41/31.49 [12]~E(x121,x122)+E(f13(x121,x123),f13(x122,x123)) % 31.41/31.49 [13]~E(x131,x132)+E(f13(x133,x131),f13(x133,x132)) % 31.41/31.49 [14]~E(x141,x142)+E(f5(x141),f5(x142)) % 31.41/31.49 [15]~P1(x151)+P1(x152)+~E(x151,x152) % 31.41/31.49 [16]P3(x162,x163)+~E(x161,x162)+~P3(x161,x163) % 31.41/31.49 [17]P3(x173,x172)+~E(x171,x172)+~P3(x173,x171) % 31.41/31.49 [18]P2(x182,x183)+~E(x181,x182)+~P2(x181,x183) % 31.41/31.49 [19]P2(x193,x192)+~E(x191,x192)+~P2(x193,x191) % 31.41/31.49 % 31.41/31.49 %------------------------------------------- % 31.41/31.49 cnf(53,plain, % 31.41/31.49 (~P3(x531,f11(x532,x533))+P3(x531,x532)), % 31.41/31.49 inference(equality_inference,[],[45])). % 31.41/31.49 cnf(54,plain, % 31.41/31.49 (~P3(x541,x542)+~P3(x541,f11(x543,x542))), % 31.41/31.49 inference(equality_inference,[],[46])). % 31.41/31.49 cnf(55,plain, % 31.41/31.49 (~P3(x551,x552)+P3(x551,f11(x552,x553))+P3(x551,x553)), % 31.41/31.49 inference(equality_inference,[],[48])). % 31.41/31.49 cnf(56,plain, % 31.41/31.49 (~P3(a7,f11(a10,x561))), % 31.41/31.49 inference(scs_inference,[],[32,53])). % 31.41/31.49 cnf(58,plain, % 31.41/31.49 (~P1(a8)), % 31.41/31.49 inference(scs_inference,[],[29,32,53,34])). % 31.41/31.49 cnf(60,plain, % 31.41/31.49 (~P3(x601,a1)), % 31.41/31.49 inference(scs_inference,[],[29,32,20,53,34,38])). % 31.41/31.49 cnf(62,plain, % 31.41/31.49 (E(x621,f11(x621,a1))), % 31.41/31.49 inference(scs_inference,[],[29,32,25,20,53,34,38,2])). % 31.41/31.49 cnf(63,plain, % 31.41/31.49 (~P2(a9,a1)), % 31.41/31.49 inference(scs_inference,[],[29,32,25,20,30,53,34,38,2,40])). % 31.41/31.49 cnf(65,plain, % 31.41/31.49 (P3(f3(a9),a9)), % 31.41/31.49 inference(scs_inference,[],[29,32,27,25,20,30,53,34,38,2,40,41])). % 31.41/31.49 cnf(66,plain, % 31.41/31.49 (P2(f3(x661),x661)), % 31.41/31.49 inference(rename_variables,[],[27])). % 31.41/31.49 cnf(68,plain, % 31.41/31.49 (P3(f3(a9),f11(a9,a1))), % 31.41/31.49 inference(scs_inference,[],[29,32,27,25,20,30,53,34,38,2,40,41,55])). % 31.41/31.49 cnf(70,plain, % 31.41/31.49 (P2(f11(a7,a1),a8)), % 31.41/31.49 inference(scs_inference,[],[23,29,32,27,25,20,30,53,34,38,2,40,41,55,18])). % 31.41/31.49 cnf(71,plain, % 31.41/31.49 (~E(a8,f11(a1,x711))), % 31.41/31.49 inference(scs_inference,[],[23,29,32,27,25,20,30,24,53,34,38,2,40,41,55,18,3])). % 31.41/31.49 cnf(75,plain, % 31.41/31.49 (E(f11(x751,a1),x751)), % 31.41/31.49 inference(rename_variables,[],[25])). % 31.41/31.49 cnf(76,plain, % 31.41/31.49 (P3(f3(a9),f11(f11(a9,a1),a1))), % 31.41/31.49 inference(scs_inference,[],[23,29,32,27,66,25,75,20,30,24,53,34,38,2,40,41,55,18,3,17,19,48])). % 31.41/31.49 cnf(77,plain, % 31.41/31.49 (E(f11(x771,a1),x771)), % 31.41/31.49 inference(rename_variables,[],[25])). % 31.41/31.49 cnf(79,plain, % 31.41/31.49 (~P3(a9,f3(a9))), % 31.41/31.49 inference(scs_inference,[],[23,29,32,27,66,25,75,20,30,24,53,34,38,2,40,41,55,18,3,17,19,48,43])). % 31.41/31.49 cnf(81,plain, % 31.41/31.49 (~P3(f3(a9),f11(x811,a9))), % 31.41/31.49 inference(scs_inference,[],[23,29,32,27,66,25,75,20,30,24,53,34,38,2,40,41,55,18,3,17,19,48,43,54])). % 31.41/31.49 cnf(83,plain, % 31.41/31.49 (P2(x831,f12(x832))+~P3(x831,f12(x832))), % 31.41/31.49 inference(scs_inference,[],[23,29,32,27,66,25,75,20,30,31,24,53,34,38,2,40,41,55,18,3,17,19,48,43,54,42])). % 31.41/31.49 cnf(86,plain, % 31.41/31.49 (E(f11(x861,a1),x861)), % 31.41/31.49 inference(rename_variables,[],[25])). % 31.41/31.49 cnf(88,plain, % 31.41/31.49 (~P1(f11(a9,a1))), % 31.41/31.49 inference(scs_inference,[],[23,29,32,27,66,25,75,77,86,20,30,31,24,53,34,38,2,40,41,55,18,3,17,19,48,43,54,42,46,15])). % 31.41/31.49 cnf(96,plain, % 31.41/31.49 (~P3(f3(a9),f11(x961,f11(a9,a1)))), % 31.41/31.49 inference(scs_inference,[],[33,68,53,54])). % 31.41/31.49 cnf(98,plain, % 31.41/31.49 (~P3(x981,a2)), % 31.41/31.49 inference(scs_inference,[],[33,68,21,53,54,38])). % 31.41/31.49 cnf(100,plain, % 31.41/31.49 (~P3(f11(f11(a9,a1),a1),f3(a9))), % 31.41/31.49 inference(scs_inference,[],[33,76,68,21,53,54,38,43])). % 31.41/31.49 cnf(102,plain, % 31.41/31.49 (E(a1,f11(a1,x1021))), % 31.41/31.49 inference(scs_inference,[],[33,76,68,21,24,53,54,38,43,2])). % 31.41/31.49 cnf(103,plain, % 31.41/31.49 (P3(f3(f11(a9,a1)),f11(a9,a1))), % 31.41/31.49 inference(scs_inference,[],[33,88,76,68,21,27,24,53,54,38,43,2,41])). % 31.41/31.49 cnf(106,plain, % 31.41/31.49 (P3(f4(a1,x1061,a8),a8)), % 31.41/31.49 inference(scs_inference,[],[33,88,76,60,68,71,21,27,24,53,54,38,43,2,41,50])). % 31.41/31.49 cnf(109,plain, % 31.41/31.49 (P2(f3(a9),f11(a9,a1))), % 31.41/31.49 inference(scs_inference,[],[33,88,76,60,68,71,21,27,24,53,54,38,43,2,41,50,42])). % 31.41/31.49 cnf(113,plain, % 31.41/31.50 (P3(f3(a9),f11(a9,f11(x1131,a9)))), % 31.41/31.50 inference(scs_inference,[],[33,65,88,81,76,60,68,71,21,27,24,53,54,38,43,2,41,50,42,40,55])). % 31.41/31.50 cnf(115,plain, % 31.41/31.50 (P2(a7,f11(a8,a1))), % 31.41/31.50 inference(scs_inference,[],[23,33,65,62,88,81,76,60,68,71,21,27,24,53,54,38,43,2,41,50,42,40,55,19])). % 31.41/31.50 cnf(116,plain, % 31.41/31.50 (E(x1161,f11(x1161,a1))), % 31.41/31.50 inference(rename_variables,[],[62])). % 31.41/31.50 cnf(117,plain, % 31.41/31.50 (~E(a9,f11(x1171,a9))), % 31.41/31.50 inference(scs_inference,[],[23,33,65,62,88,81,76,60,68,71,21,27,24,53,54,38,43,2,41,50,42,40,55,19,17])). % 31.41/31.50 cnf(118,plain, % 31.41/31.50 (P1(f11(a2,a1))), % 31.41/31.50 inference(scs_inference,[],[23,33,65,62,116,88,81,76,60,68,71,21,27,24,53,54,38,43,2,41,50,42,40,55,19,17,15])). % 31.41/31.50 cnf(119,plain, % 31.41/31.50 (E(x1191,f11(x1191,a1))), % 31.41/31.50 inference(rename_variables,[],[62])). % 31.41/31.50 cnf(120,plain, % 31.41/31.50 (P3(f11(f3(a9),a1),a9)), % 31.50/31.50 inference(scs_inference,[],[23,33,65,62,116,119,88,81,76,60,68,71,21,27,24,53,54,38,43,2,41,50,42,40,55,19,17,15,16])). % 31.50/31.50 cnf(121,plain, % 31.50/31.50 (E(x1211,f11(x1211,a1))), % 31.50/31.50 inference(rename_variables,[],[62])). % 31.50/31.50 cnf(122,plain, % 31.50/31.50 (P2(f11(a10,a1),f12(a8))), % 31.50/31.50 inference(scs_inference,[],[23,26,33,65,62,116,119,121,88,81,76,60,68,71,21,27,24,53,54,38,43,2,41,50,42,40,55,19,17,15,16,18])). % 31.50/31.50 cnf(132,plain, % 31.50/31.50 (~P3(f3(f11(a9,a1)),f11(x1321,f11(a9,a1)))), % 31.50/31.50 inference(scs_inference,[],[103,79,53,54])). % 31.50/31.50 cnf(136,plain, % 31.50/31.50 (~P3(x1361,f11(a2,a1))), % 31.50/31.50 inference(scs_inference,[],[103,79,118,53,54,43,38])). % 31.50/31.50 cnf(138,plain, % 31.50/31.50 (P3(a7,a8)), % 31.50/31.50 inference(scs_inference,[],[23,103,79,118,58,53,54,43,38,41])). % 31.50/31.50 cnf(140,plain, % 31.50/31.50 (P3(f4(a2,a9,a9),a9)), % 31.50/31.50 inference(scs_inference,[],[23,103,79,98,118,117,58,53,54,43,38,41,50])). % 31.50/31.50 cnf(142,plain, % 31.50/31.50 (~P3(x1421,a2)), % 31.50/31.50 inference(rename_variables,[],[98])). % 31.50/31.50 cnf(144,plain, % 31.50/31.50 (P2(f4(a1,x1441,a8),a8)), % 31.50/31.50 inference(scs_inference,[],[23,103,79,98,118,117,106,58,53,54,43,38,41,50,42])). % 31.50/31.50 cnf(146,plain, % 31.50/31.50 (P3(a7,f11(a8,a10))), % 31.50/31.50 inference(scs_inference,[],[23,32,103,79,98,118,117,106,58,53,54,43,38,41,50,42,55])). % 31.50/31.50 cnf(152,plain, % 31.50/31.50 (P2(a10,f11(f12(a8),a1))), % 31.50/31.50 inference(scs_inference,[],[23,32,26,103,79,98,142,118,117,106,58,62,53,54,43,38,41,50,42,55,40,17,19])). % 31.50/31.50 cnf(153,plain, % 31.50/31.50 (E(x1531,f11(x1531,a1))), % 31.50/31.50 inference(rename_variables,[],[62])). % 31.50/31.50 cnf(154,plain, % 31.50/31.50 (P2(f11(f3(a9),a1),f11(a9,a1))), % 31.50/31.50 inference(scs_inference,[],[23,32,26,103,109,79,98,142,118,117,106,58,62,153,53,54,43,38,41,50,42,55,40,17,19,18])). % 31.50/31.50 cnf(155,plain, % 31.50/31.50 (E(x1551,f11(x1551,a1))), % 31.50/31.50 inference(rename_variables,[],[62])). % 31.50/31.50 cnf(156,plain, % 31.50/31.50 (P3(f11(f3(a9),a1),f11(a9,f11(x1561,a9)))), % 31.50/31.50 inference(scs_inference,[],[23,32,26,103,109,79,113,98,142,118,117,106,58,62,153,155,53,54,43,38,41,50,42,55,40,17,19,18,16])). % 31.50/31.50 cnf(158,plain, % 31.50/31.50 (P1(f11(a1,x1581))), % 31.50/31.50 inference(scs_inference,[],[23,32,26,103,109,79,113,98,142,118,102,117,106,58,62,153,155,20,53,54,43,38,41,50,42,55,40,17,19,18,16,15])). % 31.50/31.50 cnf(160,plain, % 31.50/31.50 (~P3(x1601,f11(f11(a2,a1),x1602))), % 31.50/31.50 inference(scs_inference,[],[136,53])). % 31.50/31.50 cnf(162,plain, % 31.50/31.50 (~P3(a7,f11(x1621,a8))), % 31.50/31.50 inference(scs_inference,[],[138,136,53,54])). % 31.50/31.50 cnf(164,plain, % 31.50/31.50 (~P3(x1641,f11(a1,x1642))), % 31.50/31.50 inference(scs_inference,[],[138,136,158,53,54,38])). % 31.50/31.50 cnf(166,plain, % 31.50/31.50 (~P3(a8,a7)), % 31.50/31.50 inference(scs_inference,[],[138,136,158,53,54,38,43])). % 31.50/31.50 cnf(169,plain, % 31.50/31.50 (E(f11(x1691,a1),x1691)), % 31.50/31.50 inference(rename_variables,[],[25])). % 31.50/31.50 cnf(171,plain, % 31.50/31.50 (P3(a10,f12(a8))), % 31.50/31.50 inference(scs_inference,[],[26,138,25,136,158,31,53,54,38,43,46,41])). % 31.50/31.50 cnf(172,plain, % 31.50/31.50 (~P1(f12(x1721))), % 31.50/31.50 inference(rename_variables,[],[31])). % 31.50/31.50 cnf(174,plain, % 31.50/31.50 (P3(f4(f11(a2,a1),a9,a9),a9)), % 31.50/31.50 inference(scs_inference,[],[26,138,25,136,158,117,31,53,54,38,43,46,41,50])). % 31.50/31.50 cnf(178,plain, % 31.50/31.50 (P3(a7,f11(a8,f13(a8,a10)))), % 31.50/31.50 inference(scs_inference,[],[33,26,138,25,136,158,117,31,53,54,38,43,46,41,50,55])). % 31.50/31.50 cnf(180,plain, % 31.50/31.50 (~P2(f12(x1801),f11(a1,x1802))), % 31.50/31.50 inference(scs_inference,[],[33,26,138,25,136,158,117,31,172,53,54,38,43,46,41,50,55,40])). % 31.50/31.50 cnf(185,plain, % 31.50/31.50 (P2(f11(a7,a1),f11(a8,a1))), % 31.50/31.50 inference(scs_inference,[],[33,26,154,138,25,169,136,158,115,117,31,172,62,53,54,38,43,46,41,50,55,40,17,19,18])). % 31.50/31.50 cnf(186,plain, % 31.50/31.50 (E(x1861,f11(x1861,a1))), % 31.50/31.50 inference(rename_variables,[],[62])). % 31.50/31.50 cnf(187,plain, % 31.50/31.50 (P1(f11(f11(a1,x1871),a1))), % 31.50/31.50 inference(scs_inference,[],[33,26,154,138,25,169,136,158,115,117,31,172,62,186,53,54,38,43,46,41,50,55,40,17,19,18,15])). % 31.50/31.50 cnf(188,plain, % 31.50/31.50 (E(x1881,f11(x1881,a1))), % 31.50/31.50 inference(rename_variables,[],[62])). % 31.50/31.50 cnf(189,plain, % 31.50/31.50 (P3(f11(a7,a1),a8)), % 31.50/31.50 inference(scs_inference,[],[33,26,154,138,25,169,136,158,115,117,31,172,62,186,188,53,54,38,43,46,41,50,55,40,17,19,18,15,16])). % 31.50/31.50 cnf(192,plain, % 31.50/31.50 (~P3(x1921,f11(f11(a1,x1922),x1923))), % 31.50/31.50 inference(scs_inference,[],[164,53])). % 31.50/31.50 cnf(194,plain, % 31.50/31.50 (~P3(a10,f11(x1941,f12(a8)))), % 31.50/31.50 inference(scs_inference,[],[171,164,53,54])). % 31.50/31.50 cnf(196,plain, % 31.50/31.50 (~P3(f12(a8),a10)), % 31.50/31.50 inference(scs_inference,[],[171,164,53,54,43])). % 31.50/31.50 cnf(198,plain, % 31.50/31.50 (~P3(x1981,f6(x1982))), % 31.50/31.50 inference(scs_inference,[],[171,164,22,53,54,43,38])). % 31.50/31.50 cnf(200,plain, % 31.50/31.50 (P3(f11(f3(a9),a1),f11(a9,a1))), % 31.50/31.50 inference(scs_inference,[],[171,154,164,22,88,53,54,43,38,41])). % 31.50/31.50 cnf(202,plain, % 31.50/31.50 (P3(a10,f11(f12(a8),f11(a1,x2021)))), % 31.50/31.50 inference(scs_inference,[],[171,154,164,22,88,53,54,43,38,41,55])). % 31.50/31.50 cnf(208,plain, % 31.50/31.50 (E(x2081,f11(x2081,a1))), % 31.50/31.50 inference(rename_variables,[],[62])). % 31.50/31.50 cnf(209,plain, % 31.50/31.50 (P2(f6(x2091),f11(f12(x2091),a1))), % 31.50/31.50 inference(scs_inference,[],[171,154,164,187,152,28,22,31,62,208,88,53,54,43,38,41,55,40,18,19])). % 31.50/31.50 cnf(210,plain, % 31.50/31.50 (E(x2101,f11(x2101,a1))), % 31.50/31.50 inference(rename_variables,[],[62])). % 31.50/31.50 cnf(211,plain, % 31.50/31.50 (~E(f12(a8),f11(f11(a2,a1),x2111))), % 31.50/31.50 inference(scs_inference,[],[171,154,160,164,187,152,28,22,31,62,208,88,53,54,43,38,41,55,40,18,19,17])). % 31.50/31.50 cnf(213,plain, % 31.50/31.50 (P3(f11(a10,a1),f12(a8))), % 31.50/31.50 inference(scs_inference,[],[171,154,160,164,187,152,28,22,31,62,208,210,88,53,54,43,38,41,55,40,18,19,17,16])). % 31.50/31.50 cnf(226,plain, % 31.50/31.50 (~P3(x2261,f11(f6(x2262),x2263))), % 31.50/31.50 inference(scs_inference,[],[198,53])). % 31.50/31.50 cnf(228,plain, % 31.50/31.50 (~P3(f11(f3(a9),a1),f11(x2281,f11(a9,a1)))), % 31.50/31.50 inference(scs_inference,[],[200,198,53,54])). % 31.50/31.50 cnf(232,plain, % 31.50/31.50 (P3(f4(f11(a2,a1),x2321,f12(a8)),f12(a8))), % 31.50/31.50 inference(scs_inference,[],[200,198,211,136,53,54,43,50])). % 31.50/31.50 cnf(235,plain, % 31.50/31.50 (P3(f11(f3(a9),a1),f11(f11(a9,a1),f6(x2351)))), % 31.50/31.50 inference(scs_inference,[],[200,198,211,136,53,54,43,50,55])). % 31.50/31.50 cnf(236,plain, % 31.50/31.50 (~P3(x2361,f6(x2362))), % 31.50/31.50 inference(rename_variables,[],[198])). % 31.50/31.50 cnf(242,plain, % 31.50/31.50 (P2(f11(f6(x2421),a1),f11(f12(x2421),a1))), % 31.50/31.50 inference(scs_inference,[],[200,30,198,236,209,211,22,136,62,53,54,43,50,55,40,17,18])). % 31.50/31.50 cnf(243,plain, % 31.50/31.50 (E(x2431,f11(x2431,a1))), % 31.50/31.50 inference(rename_variables,[],[62])). % 31.50/31.50 cnf(244,plain, % 31.50/31.50 (P2(f4(a1,x2441,a8),f11(a8,a1))), % 31.50/31.50 inference(scs_inference,[],[200,30,198,236,209,211,144,22,136,62,243,53,54,43,50,55,40,17,18,19])). % 31.50/31.50 cnf(245,plain, % 31.50/31.50 (E(x2451,f11(x2451,a1))), % 31.50/31.50 inference(rename_variables,[],[62])). % 31.50/31.50 cnf(246,plain, % 31.50/31.50 (P3(f11(f4(a2,a9,a9),a1),a9)), % 31.50/31.50 inference(scs_inference,[],[200,30,198,236,140,209,211,144,22,136,62,243,245,53,54,43,50,55,40,17,18,19,16])). % 31.50/31.50 cnf(247,plain, % 31.50/31.50 (E(x2471,f11(x2471,a1))), % 31.50/31.50 inference(rename_variables,[],[62])). % 31.50/31.50 cnf(248,plain, % 31.50/31.50 (P1(f11(f6(x2481),a1))), % 31.50/31.50 inference(scs_inference,[],[200,30,198,236,140,209,211,144,22,136,62,243,245,247,53,54,43,50,55,40,17,18,19,16,15])). % 31.50/31.50 cnf(252,plain, % 31.50/31.50 (~P3(f11(f3(a9),a1),f11(x2521,a9))), % 31.50/31.50 inference(scs_inference,[],[120,100,53,54])). % 31.50/31.50 cnf(256,plain, % 31.50/31.50 (P3(a7,f11(a8,f11(a10,x2561)))), % 31.50/31.50 inference(scs_inference,[],[138,120,235,100,56,53,54,43,55])). % 31.50/31.50 cnf(260,plain, % 31.50/31.50 (~E(a9,f11(f6(x2601),x2602))), % 31.50/31.50 inference(scs_inference,[],[65,138,31,226,120,235,248,100,56,53,54,43,55,40,17])). % 31.50/31.50 cnf(262,plain, % 31.50/31.50 (P2(f11(f4(a1,x2621,a8),a1),f11(a8,a1))), % 31.50/31.50 inference(scs_inference,[],[65,138,31,226,120,235,244,248,100,56,62,53,54,43,55,40,17,18])). % 31.50/31.50 cnf(265,plain, % 31.50/31.50 (E(f11(x2651,a1),x2651)), % 31.50/31.50 inference(rename_variables,[],[25])). % 31.50/31.50 cnf(266,plain, % 31.50/31.50 (P3(f3(a9),f11(f11(a9,a1),f6(x2661)))), % 31.50/31.50 inference(scs_inference,[],[242,65,138,25,265,31,226,120,235,244,248,100,56,62,53,54,43,55,40,17,18,19,16])). % 31.50/31.50 cnf(285,plain, % 31.50/31.50 (~P3(f11(f3(a9),a1),f11(f11(x2851,a9),x2852))), % 31.50/31.50 inference(scs_inference,[],[252,53])). % 31.50/31.50 cnf(287,plain, % 31.50/31.50 (~P3(f11(a7,a1),f11(x2871,a8))), % 31.50/31.50 inference(scs_inference,[],[189,252,53,54])). % 31.50/31.50 cnf(291,plain, % 31.50/31.50 (P3(f4(f6(x2911),x2912,a9),a9)), % 31.50/31.50 inference(scs_inference,[],[189,252,260,198,53,54,43,50])). % 31.50/31.50 cnf(295,plain, % 31.50/31.50 (P3(f11(f3(a9),a1),f11(f11(a9,a1),f11(x2951,a9)))), % 31.50/31.50 inference(scs_inference,[],[200,189,252,260,198,53,54,43,50,55])). % 31.50/31.50 cnf(299,plain, % 31.50/31.50 (~E(f11(a9,a1),f11(f11(a1,x2991),x2992))), % 31.50/31.50 inference(scs_inference,[],[103,200,88,248,192,189,252,260,198,53,54,43,50,55,40,17])). % 31.50/31.50 cnf(302,plain, % 31.50/31.50 (E(x3021,f11(x3021,a1))), % 31.50/31.50 inference(rename_variables,[],[62])). % 31.50/31.50 cnf(303,plain, % 31.50/31.50 (P2(f3(a1),f11(a1,x3031))), % 31.50/31.50 inference(scs_inference,[],[103,200,102,88,248,192,189,252,260,144,27,198,62,53,54,43,50,55,40,17,18,19])). % 31.50/31.50 cnf(305,plain, % 31.50/31.50 (P3(f11(a7,a1),f11(a8,f13(a8,a10)))), % 31.50/31.50 inference(scs_inference,[],[103,200,102,88,248,192,189,178,252,260,144,27,198,62,302,53,54,43,50,55,40,17,18,19,16])). % 31.50/31.50 cnf(307,plain, % 31.50/31.50 (~E(a9,f11(a1,x3071))), % 31.50/31.50 inference(scs_inference,[],[103,200,102,88,248,192,189,178,252,260,144,27,198,62,302,53,54,43,50,55,40,17,18,19,16,5])). % 31.50/31.50 cnf(322,plain, % 31.50/31.50 (~P3(f11(a10,a1),f11(x3221,f12(a8)))), % 31.50/31.50 inference(scs_inference,[],[213,287,53,54])). % 31.50/31.50 cnf(324,plain, % 31.50/31.50 (~P3(f11(a8,f13(a8,a10)),f11(a7,a1))), % 31.50/31.50 inference(scs_inference,[],[305,213,287,53,54,43])). % 31.50/31.50 cnf(326,plain, % 31.50/31.50 (P3(f4(f11(a1,x3261),x3262,f11(a9,a1)),f11(a9,a1))), % 31.50/31.50 inference(scs_inference,[],[305,213,299,287,164,53,54,43,50])). % 31.50/31.50 cnf(330,plain, % 31.50/31.50 (P3(f11(a7,a1),f11(f11(a8,f13(a8,a10)),f11(x3301,a8)))), % 31.50/31.50 inference(scs_inference,[],[305,213,299,287,164,53,54,43,50,55])). % 31.50/31.50 cnf(334,plain, % 31.50/31.50 (~E(f11(a9,a1),f11(x3341,f11(a9,a1)))), % 31.50/31.50 inference(scs_inference,[],[200,30,187,305,228,213,299,287,164,53,54,43,50,55,40,17])). % 31.50/31.50 cnf(337,plain, % 31.50/31.50 (P3(f3(a9),f11(f11(a9,a1),f11(x3371,a9)))), % 31.50/31.50 inference(scs_inference,[],[180,200,25,30,187,305,228,213,295,299,287,303,164,53,54,43,50,55,40,17,18,16])). % 31.50/31.50 cnf(339,plain, % 31.50/31.50 (~E(a1,f11(a9,a1))), % 31.50/31.50 inference(scs_inference,[],[180,200,25,30,187,305,228,213,295,299,287,303,164,53,54,43,50,55,40,17,18,16,6])). % 31.50/31.50 cnf(352,plain, % 31.50/31.50 (~P3(f4(f11(a2,a1),a9,a9),f11(x3521,a9))), % 31.50/31.50 inference(scs_inference,[],[174,324,53,54])). % 31.50/31.50 cnf(356,plain, % 31.50/31.50 (P3(f4(a1,x3561,a9),a9)), % 31.50/31.50 inference(scs_inference,[],[307,174,324,60,53,54,43,50])). % 31.50/31.50 cnf(361,plain, % 31.50/31.50 (P3(a7,f11(a8,f11(x3611,a8)))), % 31.50/31.50 inference(scs_inference,[],[138,30,118,307,174,324,162,60,53,54,43,50,40,55])). % 31.50/31.50 cnf(363,plain, % 31.50/31.50 (~E(f11(a9,a1),f11(f11(x3631,a9),x3632))), % 31.50/31.50 inference(scs_inference,[],[200,138,30,118,307,174,324,285,162,60,53,54,43,50,40,55,17])). % 31.50/31.50 cnf(364,plain, % 31.50/31.50 (P1(f11(f11(a2,a1),a1))), % 31.50/31.50 inference(scs_inference,[],[200,138,30,62,118,307,174,324,285,162,60,53,54,43,50,40,55,17,15])). % 31.50/31.50 cnf(365,plain, % 31.50/31.50 (E(x3651,f11(x3651,a1))), % 31.50/31.50 inference(rename_variables,[],[62])). % 31.50/31.50 cnf(368,plain, % 31.50/31.50 (P3(f11(a7,a1),f11(a8,a10))), % 31.50/31.50 inference(scs_inference,[],[63,200,138,30,62,365,118,307,27,174,324,146,285,162,60,53,54,43,50,40,55,17,15,18,16])). % 31.50/31.50 cnf(370,plain, % 31.50/31.50 (~P3(f12(a8),f11(a10,x3701))), % 31.50/31.50 inference(scs_inference,[],[196,53])). % 31.50/31.50 cnf(374,plain, % 31.50/31.50 (~P3(f11(a8,a10),f11(a7,a1))), % 31.50/31.50 inference(scs_inference,[],[368,196,53,54,43])). % 31.50/31.50 cnf(376,plain, % 31.50/31.50 (P3(f4(f11(f11(a1,x3761),x3762),f11(a9,a1),f11(a9,a1)),f11(a9,a1))), % 31.50/31.50 inference(scs_inference,[],[334,368,196,192,53,54,43,50])). % 31.50/31.50 cnf(380,plain, % 31.50/31.50 (P3(f4(f11(a2,a1),a9,a9),f11(a9,f11(x3801,a9)))), % 31.50/31.50 inference(scs_inference,[],[334,368,196,352,192,174,53,54,43,50,55])). % 31.50/31.50 cnf(384,plain, % 31.50/31.50 (~E(f12(a8),f11(x3841,f12(a8)))), % 31.50/31.50 inference(scs_inference,[],[171,88,158,334,368,196,352,194,192,174,53,54,43,50,55,40,17])). % 31.50/31.50 cnf(385,plain, % 31.50/31.50 (P3(a7,f11(f11(a8,f13(a8,a10)),f11(x3851,a8)))), % 31.50/31.50 inference(scs_inference,[],[171,25,88,158,334,368,330,196,352,194,192,174,53,54,43,50,55,40,17,16])). % 31.50/31.50 cnf(393,plain, % 31.50/31.50 (P3(f4(f11(f11(a2,a1),x3931),f11(a9,a1),f11(a9,a1)),f11(a9,a1))), % 31.50/31.50 inference(scs_inference,[],[334,374,376,326,160,53,54,43,50])). % 31.50/31.50 cnf(399,plain, % 31.50/31.50 (P3(f3(f11(a9,a1)),f11(f11(a9,a1),a2))), % 31.50/31.50 inference(scs_inference,[],[103,30,248,334,374,376,326,160,98,53,54,43,50,40,55])). % 31.50/31.50 cnf(402,plain, % 31.50/31.50 (~E(a9,f11(x4021,f11(a9,a1)))), % 31.50/31.50 inference(scs_inference,[],[103,65,30,248,334,374,376,326,96,160,98,53,54,43,50,40,55,17])). % 31.50/31.50 cnf(403,plain, % 31.50/31.50 (P3(f11(a10,a1),f11(f12(a8),f11(a1,x4031)))), % 31.50/31.50 inference(scs_inference,[],[103,65,30,62,248,334,374,376,326,96,202,160,98,53,54,43,50,40,55,17,16])). % 31.50/31.50 cnf(405,plain, % 31.50/31.50 (~P3(a8,f11(a7,x4051))), % 31.50/31.50 inference(scs_inference,[],[166,53])). % 31.50/31.50 cnf(411,plain, % 31.50/31.50 (P3(f4(a9,a1,a1),a9)), % 31.50/31.50 inference(scs_inference,[],[339,393,166,232,60,53,54,43,50])). % 31.50/31.50 cnf(414,plain, % 31.50/31.50 (P3(f3(f11(a9,a1)),f11(f11(a9,a1),f11(a1,x4141)))), % 31.50/31.50 inference(scs_inference,[],[103,339,393,166,232,164,60,53,54,43,50,55])). % 31.50/31.50 cnf(419,plain, % 31.50/31.50 (~E(f11(a9,a1),f11(f6(x4191),x4192))), % 31.50/31.50 inference(scs_inference,[],[103,88,187,339,393,166,232,226,164,60,53,54,43,50,55,40,17])). % 31.50/31.50 cnf(421,plain, % 31.50/31.50 (P3(f11(a7,a1),f11(a8,f11(a10,x4211)))), % 31.50/31.50 inference(scs_inference,[],[103,88,62,187,339,393,166,232,256,226,164,60,53,54,43,50,55,40,17,16])). % 31.50/31.50 cnf(427,plain, % 31.50/31.50 (~P3(f4(f6(x4271),x4272,a9),f11(x4273,a9))), % 31.50/31.50 inference(scs_inference,[],[419,370,291,5,53,54])). % 31.50/31.51 cnf(431,plain, % 31.50/31.51 (P3(f4(f11(f11(a1,x4311),x4312),f11(a9,a1),a9),a9)), % 31.50/31.51 inference(scs_inference,[],[402,419,399,370,291,192,5,53,54,43,50])). % 31.50/31.51 cnf(437,plain, % 31.50/31.51 (P3(f11(a7,a1),f11(f11(a8,f11(a10,x4371)),f11(x4372,a8)))), % 31.50/31.51 inference(scs_inference,[],[31,402,21,419,399,421,370,291,192,287,5,53,54,43,50,40,55])). % 31.50/31.51 cnf(439,plain, % 31.50/31.51 (~E(f11(f11(a9,a1),a2),f11(x4391,f11(a9,a1)))), % 31.50/31.51 inference(scs_inference,[],[31,402,21,419,399,132,421,370,291,192,287,5,53,54,43,50,40,55,17])). % 31.50/31.51 cnf(440,plain, % 31.50/31.51 (P3(f11(a7,a1),f11(a8,f11(x4401,a8)))), % 31.50/31.51 inference(scs_inference,[],[31,62,402,21,419,399,132,421,370,291,361,192,287,5,53,54,43,50,40,55,17,16])). % 31.50/31.51 cnf(442,plain, % 31.50/31.51 (~E(a2,f11(a9,a1))), % 31.50/31.51 inference(scs_inference,[],[31,62,402,21,419,399,132,421,370,291,361,192,287,5,53,54,43,50,40,55,17,16,6])). % 31.50/31.51 cnf(457,plain, % 31.50/31.51 (~P1(f5(a8))), % 31.50/31.51 inference(scs_inference,[],[29,36,34])). % 31.50/31.51 cnf(464,plain, % 31.50/31.51 (~P1(f11(f11(a9,a1),a2))), % 31.50/31.51 inference(scs_inference,[],[158,439,414,427,431,53,54,43,35])). % 31.50/31.51 cnf(468,plain, % 31.50/31.51 (P3(f3(f5(a8)),f5(a8))), % 31.50/31.51 inference(scs_inference,[],[158,27,439,414,427,457,431,53,54,43,35,41])). % 31.50/31.51 cnf(475,plain, % 31.50/31.51 (P3(f4(f11(f11(a2,a1),x4751),f11(a9,a1),a9),a9)), % 31.50/31.51 inference(scs_inference,[],[31,402,22,158,27,439,414,427,457,431,399,160,53,54,43,35,41,42,40,50])). % 31.50/31.51 cnf(479,plain, % 31.50/31.51 (P3(f4(f6(x4791),x4792,a9),f11(a9,f11(x4793,a9)))), % 31.50/31.51 inference(scs_inference,[],[31,402,22,158,27,439,414,427,457,431,399,160,291,53,54,43,35,41,42,40,50,55])). % 31.50/31.51 cnf(483,plain, % 31.50/31.51 (P3(a7,f11(f11(a8,f11(a10,x4831)),f11(x4832,a8)))), % 31.50/31.51 inference(scs_inference,[],[32,138,25,31,402,22,158,27,439,414,437,427,457,431,399,160,291,53,54,43,35,41,42,40,50,55,17,16])). % 31.50/31.51 cnf(489,plain, % 31.50/31.51 (~P3(f3(f5(a8)),f11(x4891,f5(a8)))), % 31.50/31.51 inference(scs_inference,[],[468,405,53,54])). % 31.50/31.51 cnf(495,plain, % 31.50/31.51 (P3(f4(f6(x4951),x4952,f11(a9,a1)),f11(a9,a1))), % 31.50/31.51 inference(scs_inference,[],[468,58,248,419,405,198,53,54,43,40,50])). % 31.50/31.51 cnf(499,plain, % 31.50/31.51 (P3(f3(f5(a8)),f11(f5(a8),a2))), % 31.50/31.51 inference(scs_inference,[],[468,58,248,419,405,98,198,53,54,43,40,50,55])). % 31.50/31.51 cnf(500,plain, % 31.50/31.51 (~P3(x5001,a2)), % 31.50/31.51 inference(rename_variables,[],[98])). % 31.50/31.51 cnf(504,plain, % 31.50/31.51 (P3(f11(f4(a1,x5041,a9),a1),a9)), % 31.50/31.51 inference(scs_inference,[],[468,58,62,248,419,405,356,98,500,198,53,54,43,40,50,55,17,16])). % 31.50/31.51 cnf(516,plain, % 31.50/31.51 (P3(f4(f11(f6(x5161),a9),x5162,f11(a9,a1)),f11(a9,a1))), % 31.50/31.51 inference(scs_inference,[],[58,187,363,495,352,226,53,54,43,40,50])). % 31.50/31.51 cnf(520,plain, % 31.50/31.51 (P3(f11(a7,a1),f11(f11(a8,f11(x5201,a8)),f11(x5202,a8)))), % 31.50/31.51 inference(scs_inference,[],[58,187,363,495,440,352,226,287,53,54,43,40,50,55])). % 31.50/31.51 cnf(522,plain, % 31.50/31.51 (~E(f5(a8),f11(x5221,f5(a8)))), % 31.50/31.51 inference(scs_inference,[],[468,58,187,363,495,440,489,352,226,287,53,54,43,40,50,55,17])). % 31.50/31.51 cnf(523,plain, % 31.50/31.51 (P3(f11(f4(a9,a1,a1),a1),a9)), % 31.50/31.51 inference(scs_inference,[],[468,58,62,187,363,495,440,489,411,352,226,287,53,54,43,40,50,55,17,16])). % 31.50/31.51 cnf(545,plain, % 31.50/31.51 (P3(f3(f5(a8)),f11(f5(a8),f11(a1,x5451)))), % 31.50/31.51 inference(scs_inference,[],[468,88,118,516,475,56,164,53,54,43,40,55])). % 31.50/31.51 cnf(548,plain, % 31.50/31.51 (P3(f4(f11(f11(a1,x5481),a9),x5482,f11(a9,a1)),f11(a9,a1))), % 31.50/31.51 inference(scs_inference,[],[468,88,118,363,516,475,56,192,164,53,54,43,40,55,50])). % 31.50/31.51 cnf(552,plain, % 31.50/31.51 (~E(f11(f12(a8),f11(a1,x5521)),f11(x5522,f12(a8)))), % 31.50/31.51 inference(scs_inference,[],[468,88,118,363,516,322,403,475,56,192,164,53,54,43,40,55,50,17])). % 31.50/31.51 cnf(553,plain, % 31.50/31.51 (P3(a7,f11(f11(a8,f11(x5531,a8)),f11(x5532,a8)))), % 31.50/31.51 inference(scs_inference,[],[468,25,88,118,363,516,322,520,403,475,56,192,164,53,54,43,40,55,50,17,16])). % 31.50/31.51 cnf(576,plain, % 31.50/31.51 (~P3(f11(f4(a2,a9,a9),a1),f11(x5761,a9))), % 31.50/31.51 inference(scs_inference,[],[246,162,53,54])). % 31.50/31.51 cnf(580,plain, % 31.50/31.51 (~P1(f11(f12(a8),f11(a1,x5801)))), % 31.50/31.51 inference(scs_inference,[],[158,548,552,246,162,53,54,43,35])). % 31.50/31.51 cnf(584,plain, % 31.50/31.51 (P2(f11(a10,a1),f11(f12(a8),f11(a1,x5841)))), % 31.50/31.51 inference(scs_inference,[],[158,548,552,246,403,162,53,54,43,35,42])). % 31.50/31.51 cnf(588,plain, % 31.50/31.51 (P3(f4(f11(f11(a2,a1),a9),x5881,f11(a9,a1)),f11(a9,a1))), % 31.50/31.51 inference(scs_inference,[],[30,21,158,363,548,552,246,403,162,160,53,54,43,35,42,40,50])). % 31.50/31.51 cnf(590,plain, % 31.50/31.51 (~P3(x5901,f11(f11(a2,a1),x5902))), % 31.50/31.51 inference(rename_variables,[],[160])). % 31.50/31.51 cnf(592,plain, % 31.50/31.51 (P3(f11(f3(a9),a1),f11(f11(a9,a1),a2))), % 31.50/31.51 inference(scs_inference,[],[200,30,21,158,363,548,552,246,403,162,160,98,53,54,43,35,42,40,50,55])). % 31.50/31.51 cnf(597,plain, % 31.50/31.51 (~E(f11(a9,a1),f11(f11(a2,a1),x5971))), % 31.50/31.51 inference(scs_inference,[],[200,25,30,21,158,363,548,552,246,403,162,160,590,98,53,54,43,35,42,40,50,55,18,17])). % 31.50/31.51 cnf(599,plain, % 31.50/31.51 (P3(f11(f3(a9),a1),f11(f11(a9,a1),a1))), % 31.50/31.51 inference(scs_inference,[],[200,25,30,62,21,158,363,548,552,246,403,162,76,160,590,98,53,54,43,35,42,40,50,55,18,17,16])). % 31.50/31.51 cnf(603,plain, % 31.50/31.51 (~E(a9,f11(a2,a1))), % 31.50/31.51 inference(scs_inference,[],[597,5])). % 31.50/31.51 cnf(607,plain, % 31.50/31.51 (~P3(f11(f4(a9,a1,a1),a1),f11(x6071,a9))), % 31.50/31.51 inference(scs_inference,[],[597,576,523,5,53,54])). % 31.50/31.51 cnf(619,plain, % 31.50/31.51 (P3(f11(f4(a2,a9,a9),a1),f11(a9,f11(x6191,a9)))), % 31.50/31.51 inference(scs_inference,[],[88,22,522,464,588,592,597,576,523,246,226,5,53,54,43,42,40,50,55])). % 31.50/31.51 cnf(622,plain, % 31.50/31.51 (E(f11(x6221,a1),x6221)), % 31.50/31.51 inference(rename_variables,[],[25])). % 31.50/31.51 cnf(623,plain, % 31.50/31.51 (~E(f11(f5(a8),a2),f11(x6231,f5(a8)))), % 31.50/31.51 inference(scs_inference,[],[25,88,22,522,464,588,592,597,499,576,523,489,246,226,5,53,54,43,42,40,50,55,18,17])). % 31.50/31.51 cnf(624,plain, % 31.50/31.51 (P3(f3(a9),f11(f11(a9,a1),a2))), % 31.50/31.51 inference(scs_inference,[],[25,622,88,22,522,464,588,592,597,499,576,523,489,246,226,5,53,54,43,42,40,50,55,18,17,16])). % 31.50/31.51 cnf(641,plain, % 31.50/31.51 (~P3(f11(f4(a1,x6411,a9),a1),f11(x6412,a9))), % 31.50/31.51 inference(scs_inference,[],[607,504,53,54])). % 31.50/31.51 cnf(657,plain, % 31.50/31.51 (P3(f11(f4(a9,a1,a1),a1),f11(a9,f11(x6571,a9)))), % 31.50/31.51 inference(scs_inference,[],[248,158,457,522,623,380,607,504,499,523,192,53,54,43,35,42,40,50,55])). % 31.50/31.51 cnf(659,plain, % 31.50/31.51 (~E(f11(f11(a9,a1),a1),f11(x6591,f11(a9,a1)))), % 31.50/31.51 inference(scs_inference,[],[248,158,457,522,623,599,380,607,504,228,499,523,192,53,54,43,35,42,40,50,55,17])). % 31.50/31.51 cnf(660,plain, % 31.50/31.51 (P3(f4(a2,a9,a9),f11(a9,f11(x6601,a9)))), % 31.50/31.51 inference(scs_inference,[],[25,248,158,457,522,623,599,380,607,619,504,228,499,523,192,53,54,43,35,42,40,50,55,17,16])). % 31.50/31.51 cnf(668,plain, % 31.50/31.51 (~P3(f11(f11(a9,a1),a2),f3(a9))), % 31.50/31.51 inference(scs_inference,[],[624,641,146,53,54,43])). % 31.50/31.51 cnf(670,plain, % 31.50/31.51 (~P1(f11(f11(a9,a1),a1))), % 31.50/31.51 inference(scs_inference,[],[158,624,659,641,146,53,54,43,35])). % 31.50/31.51 cnf(678,plain, % 31.50/31.51 (P3(f4(f11(a2,a1),x6781,f11(a9,a1)),f11(a9,a1))), % 31.50/31.51 inference(scs_inference,[],[187,158,457,597,624,659,641,146,599,136,53,54,43,35,42,40,50])). % 31.50/31.51 cnf(681,plain, % 31.50/31.51 (P3(f11(f4(a1,x6811,a9),a1),f11(a9,f11(x6812,a9)))), % 31.50/31.51 inference(scs_inference,[],[187,158,457,597,624,659,641,146,599,504,136,53,54,43,35,42,40,50,55])). % 31.50/31.51 cnf(685,plain, % 31.50/31.51 (E(f11(x6851,a1),x6851)), % 31.50/31.51 inference(rename_variables,[],[25])). % 31.50/31.51 cnf(686,plain, % 31.50/31.51 (~E(f11(a9,f11(x6861,a9)),f11(f11(a2,a1),x6862))), % 31.50/31.51 inference(scs_inference,[],[25,187,158,457,597,624,659,660,641,146,599,504,160,136,53,54,43,35,42,40,50,55,18,17])). % 31.50/31.51 cnf(688,plain, % 31.50/31.51 (P3(f4(a9,a1,a1),f11(a9,f11(x6881,a9)))), % 31.50/31.51 inference(scs_inference,[],[25,685,187,158,457,597,624,659,660,657,641,146,599,504,160,136,53,54,43,35,42,40,50,55,18,17,16])). % 31.50/31.51 cnf(698,plain, % 31.50/31.51 (~P1(f11(a9,f11(x6981,a9)))), % 31.50/31.51 inference(scs_inference,[],[364,678,686,668,53,54,43,35])). % 31.50/31.51 cnf(705,plain, % 31.50/31.51 (P3(f4(a2,f5(a8),f5(a8)),f5(a8))), % 31.50/31.51 inference(scs_inference,[],[31,118,364,522,678,686,688,668,98,53,54,43,35,42,40,50])). % 31.50/31.51 cnf(707,plain, % 31.50/31.51 (~P3(x7071,a2)), % 31.50/31.51 inference(rename_variables,[],[98])). % 31.50/31.51 cnf(709,plain, % 31.50/31.51 (P3(f3(f5(a8)),f11(f5(a8),f6(x7091)))), % 31.50/31.51 inference(scs_inference,[],[468,31,118,364,522,678,686,688,668,98,198,53,54,43,35,42,40,50,55])). % 31.50/31.51 cnf(716,plain, % 31.50/31.51 (P3(f4(a1,x7161,a9),f11(a9,f11(x7162,a9)))), % 31.50/31.51 inference(scs_inference,[],[468,25,62,31,118,364,522,678,686,688,668,681,98,707,198,53,54,43,35,42,40,50,55,18,17,16])). % 31.50/31.51 cnf(720,plain, % 31.50/31.51 (~P3(f3(a9),f11(f11(x7201,a9),x7202))), % 31.50/31.51 inference(scs_inference,[],[81,53])). % 31.50/31.51 cnf(731,plain, % 31.50/31.51 (P3(f4(a9,a1,a2),a9)), % 31.50/31.51 inference(scs_inference,[],[58,21,442,156,698,705,81,98,53,54,43,42,40,50])). % 31.50/31.51 cnf(734,plain, % 31.50/31.51 (P3(f11(f3(a9),a1),f11(f11(a9,a1),f11(a1,x7341)))), % 31.50/31.51 inference(scs_inference,[],[200,58,21,442,156,698,705,81,164,98,53,54,43,42,40,50,55])). % 31.50/31.51 cnf(739,plain, % 31.50/31.51 (P3(f11(f4(a1,x7391,a8),a1),a8)), % 31.50/31.51 inference(scs_inference,[],[200,25,62,58,21,442,156,698,705,81,164,98,106,53,54,43,42,40,50,55,18,16])). % 31.50/31.51 cnf(744,plain, % 31.50/31.51 (~P3(x7441,f11(a2,x7442))), % 31.50/31.51 inference(scs_inference,[],[98,53])). % 31.50/31.51 cnf(746,plain, % 31.50/31.51 (~P3(f11(f4(a1,x7461,a8),a1),f11(x7462,a8))), % 31.50/31.51 inference(scs_inference,[],[739,98,53,54])). % 31.50/31.51 cnf(755,plain, % 31.50/31.51 (P3(f4(a2,a1,a9),a9)), % 31.50/31.51 inference(scs_inference,[],[58,22,603,734,479,739,698,98,53,54,43,42,40,50])). % 31.50/31.51 cnf(758,plain, % 31.50/31.51 (P3(a10,f11(f12(a8),f11(a2,a1)))), % 31.50/31.51 inference(scs_inference,[],[171,58,22,603,734,479,739,698,136,98,53,54,43,42,40,50,55])). % 31.50/31.51 cnf(762,plain, % 31.50/31.51 (P3(f3(a9),f11(f11(a9,a1),f11(a1,x7621)))), % 31.50/31.51 inference(scs_inference,[],[171,65,25,58,22,603,734,479,720,739,698,136,98,53,54,43,42,40,50,55,17,16])). % 31.50/31.51 cnf(767,plain, % 31.50/31.51 (~P3(x7671,f11(f11(a2,x7672),x7673))), % 31.50/31.51 inference(scs_inference,[],[744,53])). % 31.50/31.51 cnf(769,plain, % 31.50/31.51 (~P3(f4(a9,a1,a2),f11(x7691,a9))), % 31.50/31.51 inference(scs_inference,[],[744,731,53,54])). % 31.50/31.51 cnf(773,plain, % 31.50/31.51 (P2(f4(a1,x7731,a9),f11(a9,f11(x7732,a9)))), % 31.50/31.51 inference(scs_inference,[],[744,709,716,731,698,53,54,43,42])). % 31.50/31.51 cnf(778,plain, % 31.50/31.51 (P3(f4(f11(a2,x7781),f11(a9,a1),a9),a9)), % 31.50/31.51 inference(scs_inference,[],[402,248,464,744,709,716,731,698,53,54,43,42,40,50])). % 31.50/31.51 cnf(780,plain, % 31.50/31.51 (~P3(x7801,f11(a2,x7802))), % 31.50/31.51 inference(rename_variables,[],[744])). % 31.50/31.51 cnf(783,plain, % 31.50/31.51 (E(x7831,f11(x7831,a1))), % 31.50/31.51 inference(rename_variables,[],[62])). % 31.50/31.51 cnf(784,plain, % 31.50/31.51 (P3(f3(f5(a8)),f11(f5(a8),f11(a2,x7841)))), % 31.50/31.51 inference(scs_inference,[],[185,468,402,62,248,464,744,780,709,716,731,698,53,54,43,42,40,50,19,55])). % 31.50/31.51 cnf(785,plain, % 31.50/31.51 (~P3(x7851,f11(a2,x7852))), % 31.50/31.51 inference(rename_variables,[],[744])). % 31.50/31.51 cnf(788,plain, % 31.50/31.51 (E(x7881,f11(x7881,a1))), % 31.50/31.51 inference(rename_variables,[],[62])). % 31.50/31.51 cnf(789,plain, % 31.50/31.51 (~E(f5(a8),f11(a2,x7891))), % 31.50/31.51 inference(scs_inference,[],[70,185,468,402,62,783,248,464,744,780,785,709,716,731,698,53,54,43,42,40,50,19,55,18,17])). % 31.50/31.51 cnf(791,plain, % 31.50/31.51 (P3(f11(f4(a9,a1,a2),a1),a9)), % 31.50/31.51 inference(scs_inference,[],[70,185,468,402,62,783,788,248,464,744,780,785,709,716,731,698,53,54,43,42,40,50,19,55,18,17,16])). % 31.50/31.51 cnf(797,plain, % 31.50/31.51 (~P3(f4(f11(a2,x7971),f11(a9,a1),a9),f11(x7972,a9))), % 31.50/31.51 inference(scs_inference,[],[769,778,53,54])). % 31.50/31.51 cnf(801,plain, % 31.50/31.51 (P2(f4(a2,a9,a9),f11(a9,f11(x8011,a9)))), % 31.50/31.51 inference(scs_inference,[],[769,545,778,660,698,53,54,43,42])). % 31.50/31.51 cnf(806,plain, % 31.50/31.51 (P3(f4(f11(f11(a2,x8061),x8062),f11(a9,a1),a9),a9)), % 31.50/31.51 inference(scs_inference,[],[402,187,464,767,769,545,778,660,698,53,54,43,42,40,50])). % 31.50/31.51 cnf(808,plain, % 31.50/31.51 (~P3(x8081,f11(f11(a2,x8082),x8083))), % 31.50/31.51 inference(rename_variables,[],[767])). % 31.50/31.51 cnf(810,plain, % 31.50/31.51 (P3(f4(a9,a1,a2),f11(a9,f11(x8101,a9)))), % 31.50/31.51 inference(scs_inference,[],[402,187,464,767,769,545,778,660,731,698,53,54,43,42,40,50,55])). % 31.50/31.51 cnf(812,plain, % 31.50/31.51 (P2(f11(f4(a1,x8121,a8),a1),f11(f11(a8,a1),a1))), % 31.50/31.51 inference(scs_inference,[],[262,402,62,187,464,767,769,545,778,660,731,698,53,54,43,42,40,50,55,19])). % 31.50/31.51 cnf(813,plain, % 31.50/31.51 (E(x8131,f11(x8131,a1))), % 31.50/31.51 inference(rename_variables,[],[62])). % 31.50/31.51 cnf(814,plain, % 31.50/31.51 (P2(f11(f11(a7,a1),a1),f11(a8,a1))), % 31.50/31.51 inference(scs_inference,[],[185,262,402,62,813,187,464,767,769,545,778,660,731,698,53,54,43,42,40,50,55,19,18])). % 31.50/31.51 cnf(815,plain, % 31.50/31.51 (E(x8151,f11(x8151,a1))), % 31.50/31.51 inference(rename_variables,[],[62])). % 31.50/31.51 cnf(816,plain, % 31.50/31.51 (~E(f11(a9,a1),f11(f11(a2,x8161),x8162))), % 31.50/31.51 inference(scs_inference,[],[185,262,103,402,62,813,187,464,767,808,769,545,778,660,731,698,53,54,43,42,40,50,55,19,18,17])). % 31.50/31.51 cnf(818,plain, % 31.50/31.51 (P3(f11(a10,a1),f11(f12(a8),f11(a2,a1)))), % 31.50/31.51 inference(scs_inference,[],[185,262,103,402,62,813,815,187,464,767,808,769,545,758,778,660,731,698,53,54,43,42,40,50,55,19,18,17,16])). % 31.50/31.51 cnf(820,plain, % 31.50/31.51 (~E(a9,f11(a2,x8201))), % 31.50/31.51 inference(scs_inference,[],[185,262,103,402,62,813,815,187,464,767,808,769,545,758,778,660,731,698,53,54,43,42,40,50,55,19,18,17,16,5])). % 31.50/31.51 cnf(827,plain, % 31.50/31.51 (~P3(f11(f12(a8),f11(a2,a1)),f11(a10,a1))), % 31.50/31.51 inference(scs_inference,[],[818,797,806,53,54,43])). % 31.50/31.51 cnf(834,plain, % 31.50/31.51 (P3(f4(f11(f11(a2,x8341),a9),x8342,f11(a9,a1)),f11(a9,a1))), % 31.50/31.51 inference(scs_inference,[],[363,118,457,818,797,810,806,767,698,53,54,43,42,40,50])). % 31.50/31.51 cnf(836,plain, % 31.50/31.51 (~P3(x8361,f11(f11(a2,x8362),x8363))), % 31.50/31.51 inference(rename_variables,[],[767])). % 31.50/31.51 cnf(838,plain, % 31.50/31.51 (P3(f4(f11(a2,x8381),f11(a9,a1),a9),f11(a9,f11(x8382,a9)))), % 31.50/31.51 inference(scs_inference,[],[363,118,457,818,797,810,806,767,778,698,53,54,43,42,40,50,55])). % 31.50/31.51 cnf(842,plain, % 31.50/31.51 (E(x8421,f11(x8421,a1))), % 31.50/31.51 inference(rename_variables,[],[62])). % 31.50/31.51 cnf(843,plain, % 31.50/31.51 (P2(f11(f11(a10,a1),a1),f12(a8))), % 31.50/31.51 inference(scs_inference,[],[122,814,62,842,363,118,457,818,797,810,806,767,778,698,53,54,43,42,40,50,55,19,18])). % 31.50/31.51 cnf(844,plain, % 31.50/31.51 (E(x8441,f11(x8441,a1))), % 31.50/31.51 inference(rename_variables,[],[62])). % 31.50/31.51 cnf(845,plain, % 31.50/31.51 (~E(f12(a8),f11(f11(a2,x8451),x8452))), % 31.50/31.51 inference(scs_inference,[],[122,814,171,62,842,363,118,457,818,797,810,806,767,836,778,698,53,54,43,42,40,50,55,19,18,17])). % 31.50/31.51 cnf(847,plain, % 31.50/31.51 (P3(f11(f11(a10,a1),a1),f11(f12(a8),f11(a2,a1)))), % 31.50/31.51 inference(scs_inference,[],[122,814,171,62,842,844,363,118,457,818,797,810,806,767,836,778,698,53,54,43,42,40,50,55,19,18,17,16])). % 31.50/31.51 cnf(853,plain, % 31.50/31.51 (~P3(f11(f4(a9,a1,a2),a1),f11(x8531,a9))), % 31.50/31.51 inference(scs_inference,[],[827,791,53,54])). % 31.50/31.51 cnf(864,plain, % 31.50/31.51 (~P3(x8641,f11(f11(a2,x8642),x8643))), % 31.50/31.51 inference(rename_variables,[],[767])). % 31.50/31.51 cnf(866,plain, % 31.50/31.51 (P3(f11(f4(a1,x8661,a8),a1),f11(a8,f11(x8662,a8)))), % 31.50/31.51 inference(scs_inference,[],[21,457,522,834,827,838,746,791,739,767,698,53,54,43,42,40,50,55])). % 31.50/31.51 cnf(870,plain, % 31.50/31.51 (E(x8701,f11(x8701,a1))), % 31.50/31.51 inference(rename_variables,[],[62])). % 31.50/31.51 cnf(872,plain, % 31.50/31.51 (E(x8721,f11(x8721,a1))), % 31.50/31.51 inference(rename_variables,[],[62])). % 31.50/31.51 cnf(873,plain, % 31.50/31.51 (~E(f5(a8),f11(f11(a2,x8731),x8732))), % 31.50/31.51 inference(scs_inference,[],[843,468,62,870,21,457,522,584,834,827,838,746,791,739,767,864,698,53,54,43,42,40,50,55,19,18,17])). % 31.50/31.51 cnf(875,plain, % 31.50/31.51 (P3(f11(f4(a2,a1,a9),a1),a9)), % 31.50/31.51 inference(scs_inference,[],[843,468,62,870,872,21,457,522,584,834,827,838,746,791,755,739,767,864,698,53,54,43,42,40,50,55,19,18,17,16])). % 31.50/31.51 cnf(892,plain, % 31.50/31.51 (~P3(f11(f4(a2,a1,a9),a1),f11(x8921,a9))), % 31.50/31.51 inference(scs_inference,[],[853,875,53,54])). % 31.50/31.51 cnf(903,plain, % 31.50/31.51 (~P3(x9031,f11(a2,x9032))), % 31.50/31.51 inference(rename_variables,[],[744])). % 31.50/31.51 cnf(905,plain, % 31.50/31.51 (P3(f11(f4(a9,a1,a2),a1),f11(a9,f11(x9051,a9)))), % 31.50/31.51 inference(scs_inference,[],[117,22,457,784,853,875,380,791,744,698,53,54,43,42,40,50,55])). % 31.50/31.51 cnf(908,plain, % 31.50/31.51 (E(x9081,f11(x9081,a1))), % 31.50/31.51 inference(rename_variables,[],[62])). % 31.50/31.51 cnf(910,plain, % 31.50/31.51 (E(x9101,f11(x9101,a1))), % 31.50/31.51 inference(rename_variables,[],[62])). % 31.50/31.51 cnf(911,plain, % 31.50/31.51 (P3(f11(f11(a10,a1),a1),f12(a8))), % 31.50/31.51 inference(scs_inference,[],[62,908,910,117,115,22,457,801,784,853,875,213,380,791,744,698,53,54,43,42,40,50,55,19,18,16])). % 31.50/31.51 cnf(913,plain, % 31.50/31.51 (~E(f11(f12(a8),f11(a2,a1)),f11(a2,x9131))), % 31.50/31.51 inference(scs_inference,[],[62,908,910,117,115,22,457,847,801,784,853,875,213,380,791,744,903,698,53,54,43,42,40,50,55,19,18,16,17])). % 31.50/31.51 cnf(926,plain, % 31.50/31.51 (~P3(f11(f11(a9,a1),f6(x9261)),f3(a9))), % 31.50/31.51 inference(scs_inference,[],[911,266,892,53,54,43])). % 31.50/31.51 cnf(928,plain, % 31.50/31.51 (~P1(f11(f12(a8),f11(a2,a1)))), % 31.50/31.51 inference(scs_inference,[],[118,913,911,266,892,53,54,43,35])). % 31.50/31.51 cnf(936,plain, % 31.50/31.51 (P3(f4(f11(a2,x9361),x9362,f11(a9,a1)),f11(a9,a1))), % 31.50/31.51 inference(scs_inference,[],[248,118,816,580,913,911,266,905,892,744,698,53,54,43,35,42,40,50])). % 31.50/31.51 cnf(940,plain, % 31.50/31.51 (P3(f11(f4(a2,a1,a9),a1),f11(a9,f11(x9401,a9)))), % 31.50/31.51 inference(scs_inference,[],[248,118,816,580,913,911,266,905,892,875,744,698,53,54,43,35,42,40,50,55])). % 31.50/31.51 cnf(943,plain, % 31.50/31.51 (E(f11(x9431,a1),x9431)), % 31.50/31.51 inference(rename_variables,[],[25])). % 31.50/31.51 cnf(944,plain, % 31.50/31.51 (~E(f11(f11(a9,a1),f6(x9441)),f11(x9442,f11(a9,a1)))), % 31.50/31.51 inference(scs_inference,[],[25,248,118,816,580,913,812,911,266,905,892,96,875,744,698,53,54,43,35,42,40,50,55,18,17])). % 31.50/31.51 cnf(945,plain, % 31.50/31.51 (P3(f4(a1,x9451,a8),f11(a8,f11(x9452,a8)))), % 31.50/31.51 inference(scs_inference,[],[25,943,248,118,816,580,913,812,911,266,905,892,866,96,875,744,698,53,54,43,35,42,40,50,55,18,17,16])). % 31.50/31.51 cnf(956,plain, % 31.50/31.51 (~P1(f11(f11(a9,a1),f6(x9561)))), % 31.50/31.51 inference(scs_inference,[],[158,944,936,926,53,54,43,35])). % 31.50/31.51 cnf(960,plain, % 31.50/31.51 (P2(f11(f11(a10,a1),a1),f11(f12(a8),f11(a2,a1)))), % 31.50/31.51 inference(scs_inference,[],[158,944,936,928,926,847,53,54,43,35,42])). % 31.50/31.51 cnf(964,plain, % 31.50/31.51 (P3(f4(f11(a2,x9641),x9642,f5(a8)),f5(a8))), % 31.50/31.51 inference(scs_inference,[],[187,158,873,670,944,936,928,926,847,744,53,54,43,35,42,40,50])). % 31.50/31.51 cnf(968,plain, % 31.50/31.51 (P3(f4(a9,a1,a2),f11(f11(a9,f11(x9681,a9)),f11(x9682,a9)))), % 31.50/31.51 inference(scs_inference,[],[187,158,873,670,944,936,928,926,847,810,769,744,53,54,43,35,42,40,50,55])). % 31.50/31.51 cnf(972,plain, % 31.50/31.51 (~E(f11(f11(a9,a1),f11(a1,x9721)),f11(f11(x9722,a9),x9723))), % 31.50/31.51 inference(scs_inference,[],[62,187,158,873,670,944,936,928,926,762,773,847,810,720,769,744,53,54,43,35,42,40,50,55,18,17])). % 31.50/31.51 cnf(973,plain, % 31.50/31.51 (P3(f4(a2,a1,a9),f11(a9,f11(x9731,a9)))), % 31.50/31.51 inference(scs_inference,[],[25,62,187,158,873,670,944,936,928,926,762,773,940,847,810,720,769,744,53,54,43,35,42,40,50,55,18,17,16])). % 31.50/31.51 cnf(986,plain, % 31.50/31.51 (~P1(f11(f11(a9,a1),f11(a1,x9861)))), % 31.50/31.51 inference(scs_inference,[],[187,972,968,964,746,53,54,43,35])). % 31.50/31.51 cnf(990,plain, % 31.50/31.51 (P2(f4(a2,a1,a9),f11(a9,f11(x9901,a9)))), % 31.50/31.51 inference(scs_inference,[],[187,698,972,968,964,973,746,53,54,43,35,42])). % 31.50/31.51 cnf(1003,plain, % 31.50/31.51 (~E(f11(f11(a9,a1),f11(x10031,a9)),f11(x10032,f11(a9,a1)))), % 31.50/31.51 inference(scs_inference,[],[103,25,21,187,464,789,698,972,960,968,337,964,973,746,96,744,98,53,54,43,35,42,40,50,55,18,17])). % 31.50/31.51 cnf(1010,plain, % 31.50/31.51 (~P3(f11(a8,f11(x10101,a8)),f4(a1,x10102,a8))), % 31.50/31.51 inference(scs_inference,[],[945,411,54,43])). % 31.50/31.51 cnf(1012,plain, % 31.50/31.51 (~P1(f11(f11(a9,a1),f11(x10121,a9)))), % 31.50/31.51 inference(scs_inference,[],[158,945,411,1003,54,43,35])). % 31.50/31.51 cnf(1023,plain, % 31.50/31.51 (~P3(x10231,f11(a2,x10232))), % 31.50/31.51 inference(rename_variables,[],[744])). % 31.50/31.51 cnf(1029,plain, % 31.50/31.51 (E(x10291,f11(x10291,a1))), % 31.50/31.51 inference(rename_variables,[],[62])). % 31.50/31.51 cnf(1032,plain, % 31.50/31.51 (~E(f11(a8,f11(x10321,a8)),f11(f11(a2,x10322),x10323))), % 31.50/31.51 inference(scs_inference,[],[200,62,1029,22,158,464,845,945,411,421,235,956,1003,990,767,744,1023,54,43,35,42,40,50,55,18,16,17])). % 31.50/31.51 cnf(1036,plain, % 31.50/31.51 (~E(a8,f11(a2,x10361))), % 31.50/31.51 inference(scs_inference,[],[200,62,1029,22,158,464,845,945,411,421,235,956,1003,990,767,744,1023,54,43,35,42,40,50,55,18,16,17,53,5])). % 31.50/31.51 cnf(1055,plain, % 31.50/31.51 (~P3(f4(a2,a1,a9),f11(x10551,a9))), % 31.50/31.51 inference(scs_inference,[],[755,1010,53,54])). % 31.50/31.51 cnf(1057,plain, % 31.50/31.51 (~P3(f11(f11(a8,f13(a8,a10)),f11(x10571,a8)),a7)), % 31.50/31.51 inference(scs_inference,[],[385,755,1010,53,54,43])). % 31.50/31.51 cnf(1059,plain, % 31.50/31.51 (~P1(f11(a8,f11(x10591,a8)))), % 31.50/31.51 inference(scs_inference,[],[364,385,755,1032,1010,53,54,43,35])). % 31.50/31.51 cnf(1068,plain, % 31.50/31.51 (P3(f4(a2,x10681,a9),a9)), % 31.50/31.51 inference(scs_inference,[],[248,364,670,385,820,295,755,986,1032,1010,98,53,54,43,35,42,40,50])). % 31.50/31.51 cnf(1081,plain, % 31.50/31.51 (~P3(f4(a1,x10811,a9),f11(x10812,a9))), % 31.50/31.51 inference(scs_inference,[],[356,1055,53,54])). % 31.50/31.51 cnf(1097,plain, % 31.50/31.51 (P3(f11(f11(a7,a1),a1),a8)), % 31.50/31.51 inference(scs_inference,[],[62,118,464,384,483,762,973,356,189,1012,1055,767,53,54,43,42,40,50,55,16])). % 31.50/31.51 cnf(1118,plain, % 31.50/31.51 (P3(f4(a2,x11181,a8),a8)), % 31.50/31.51 inference(scs_inference,[],[21,580,1036,553,758,106,928,1081,98,53,54,43,42,40,50])). % 31.50/31.51 cnf(1215,plain, % 31.50/31.51 (~P3(f11(f11(a7,a1),a1),f11(x12151,a8))), % 31.50/31.51 inference(scs_inference,[],[1097,1057,53,54])). % 31.50/31.51 cnf(1236,plain, % 31.50/31.51 (~P3(f4(a2,x12361,a9),f11(x12362,a9))), % 31.50/31.51 inference(scs_inference,[],[1215,1068,53,54])). % 31.50/31.51 cnf(1246,plain, % 31.50/31.51 (P3(a10,f11(f12(a8),f11(a2,x12461)))), % 31.50/31.51 inference(scs_inference,[],[171,22,670,619,421,1215,1068,1059,744,53,54,43,42,40,55])). % 31.50/31.51 cnf(1279,plain, % 31.50/31.51 (~E(f11(a8,a10),f13(a8,a10))), % 31.50/31.51 inference(scs_inference,[],[33,62,248,928,657,146,440,660,1236,1246,1118,1059,53,54,43,42,40,55,16,17])). % 31.50/31.51 cnf(2589,plain, % 31.50/31.51 (E(f13(a8,a10),f11(a8,a10))), % 31.50/31.51 inference(scs_inference,[],[171,83,44])). % 31.50/31.51 cnf(2590,plain, % 31.50/31.51 ($false), % 31.50/31.51 inference(scs_inference,[],[1279,2589,2]), % 31.50/31.51 ['proof']). % 31.50/31.51 % SZS output end Proof % 31.50/31.51 % Total time :30.850000s %------------------------------------------------------------------------------