%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU230+3 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n027.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:56 EDT 2024 % Result : Theorem 1.27s 4.42s % Output : CNFRefutation 1.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU230+3 : TPTP v8.2.0. Released v3.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n027.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 12:54:23 EDT 2024 % 0.12/0.33 % CPUTime : % 0.53/3.63 start to proof:theBenchmark % 1.27/4.41 %------------------------------------------- % 1.27/4.41 % File :CSE---1.7 % 1.27/4.41 % Problem :theBenchmark % 1.27/4.41 % Transform :cnf % 1.27/4.41 % Format :tptp:raw % 1.27/4.41 % Command :java -jar mcs_scs.jar %d %s % 1.27/4.41 % 1.27/4.41 % Result :Theorem 0.740000s % 1.27/4.41 % Output :CNFRefutation 0.740000s % 1.27/4.41 %------------------------------------------- % 1.27/4.41 %------------------------------------------------------------------------------ % 1.27/4.41 % File : SEU230+3 : TPTP v8.2.0. Released v3.2.0. % 1.27/4.41 % Domain : Set Theory % 1.27/4.41 % Problem : Ordinal numbers, theorem Ordinal numbers, theorem 10 % 1.27/4.41 % Version : [Urb06] axioms : Especial. % 1.27/4.41 % English : % 1.27/4.41 % 1.27/4.41 % Refs : [Ban90] Bancerek (1990), The Ordinal Numbers % 1.27/4.41 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 1.27/4.41 % Source : [Urb06] % 1.27/4.41 % Names : ordinal1__t10_ordinal1 [Urb06] % 1.27/4.41 % 1.27/4.41 % Status : Theorem % 1.27/4.41 % Rating : 0.14 v8.1.0, 0.11 v7.5.0, 0.12 v7.4.0, 0.03 v7.1.0, 0.04 v7.0.0, 0.07 v6.4.0, 0.08 v6.2.0, 0.20 v6.1.0, 0.30 v5.5.0, 0.15 v5.4.0, 0.18 v5.3.0, 0.22 v5.2.0, 0.00 v5.1.0, 0.05 v5.0.0, 0.17 v4.0.1, 0.22 v4.0.0, 0.21 v3.7.0, 0.15 v3.5.0, 0.11 v3.4.0, 0.16 v3.3.0, 0.07 v3.2.0 % 1.27/4.41 % Syntax : Number of formulae : 34 ( 10 unt; 0 def) % 1.27/4.41 % Number of atoms : 73 ( 9 equ) % 1.27/4.41 % Maximal formula atoms : 6 ( 2 avg) % 1.27/4.41 % Number of connectives : 50 ( 11 ~; 2 |; 23 &) % 1.27/4.41 % ( 4 <=>; 10 =>; 0 <=; 0 <~>) % 1.27/4.41 % Maximal formula depth : 8 ( 4 avg) % 1.27/4.41 % Maximal term depth : 3 ( 1 avg) % 1.27/4.41 % Number of predicates : 9 ( 8 usr; 0 prp; 1-2 aty) % 1.27/4.41 % Number of functors : 4 ( 4 usr; 1 con; 0-2 aty) % 1.27/4.41 % Number of variables : 47 ( 36 !; 11 ?) % 1.27/4.41 % SPC : FOF_THM_RFO_SEQ % 1.27/4.41 % 1.27/4.41 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 1.27/4.41 % library, www.mizar.org % 1.27/4.41 %------------------------------------------------------------------------------ % 1.27/4.41 fof(antisymmetry_r2_hidden,axiom, % 1.27/4.41 ! [A,B] : % 1.27/4.41 ( in(A,B) % 1.27/4.41 => ~ in(B,A) ) ). % 1.27/4.41 % 1.27/4.41 fof(cc1_funct_1,axiom, % 1.27/4.41 ! [A] : % 1.27/4.41 ( empty(A) % 1.27/4.41 => function(A) ) ). % 1.27/4.41 % 1.27/4.41 fof(cc1_relat_1,axiom, % 1.27/4.41 ! [A] : % 1.27/4.41 ( empty(A) % 1.27/4.41 => relation(A) ) ). % 1.27/4.41 % 1.27/4.41 fof(cc2_funct_1,axiom, % 1.27/4.41 ! [A] : % 1.27/4.41 ( ( relation(A) % 1.27/4.41 & empty(A) % 1.27/4.41 & function(A) ) % 1.27/4.41 => ( relation(A) % 1.27/4.41 & function(A) % 1.27/4.41 & one_to_one(A) ) ) ). % 1.27/4.41 % 1.27/4.41 fof(commutativity_k2_xboole_0,axiom, % 1.27/4.41 ! [A,B] : set_union2(A,B) = set_union2(B,A) ). % 1.27/4.41 % 1.27/4.41 fof(d1_ordinal1,axiom, % 1.27/4.41 ! [A] : succ(A) = set_union2(A,singleton(A)) ). % 1.27/4.41 % 1.27/4.41 fof(d1_tarski,axiom, % 1.27/4.41 ! [A,B] : % 1.27/4.41 ( B = singleton(A) % 1.27/4.41 <=> ! [C] : % 1.27/4.41 ( in(C,B) % 1.27/4.41 <=> C = A ) ) ). % 1.27/4.41 % 1.27/4.41 fof(d2_xboole_0,axiom, % 1.27/4.41 ! [A,B,C] : % 1.27/4.41 ( C = set_union2(A,B) % 1.27/4.41 <=> ! [D] : % 1.27/4.41 ( in(D,C) % 1.27/4.41 <=> ( in(D,A) % 1.27/4.41 | in(D,B) ) ) ) ). % 1.27/4.41 % 1.27/4.41 fof(existence_m1_subset_1,axiom, % 1.27/4.41 ! [A] : % 1.27/4.41 ? [B] : element(B,A) ). % 1.27/4.41 % 1.27/4.41 fof(fc12_relat_1,axiom, % 1.27/4.41 ( empty(empty_set) % 1.27/4.41 & relation(empty_set) % 1.27/4.41 & relation_empty_yielding(empty_set) ) ). % 1.27/4.41 % 1.27/4.41 fof(fc1_ordinal1,axiom, % 1.27/4.41 ! [A] : ~ empty(succ(A)) ). % 1.27/4.41 % 1.27/4.41 fof(fc1_xboole_0,axiom, % 1.27/4.41 empty(empty_set) ). % 1.27/4.41 % 1.27/4.41 fof(fc2_relat_1,axiom, % 1.27/4.41 ! [A,B] : % 1.27/4.42 ( ( relation(A) % 1.27/4.42 & relation(B) ) % 1.27/4.42 => relation(set_union2(A,B)) ) ). % 1.27/4.42 % 1.27/4.42 fof(fc2_xboole_0,axiom, % 1.27/4.42 ! [A,B] : % 1.27/4.42 ( ~ empty(A) % 1.27/4.42 => ~ empty(set_union2(A,B)) ) ). % 1.27/4.42 % 1.27/4.42 fof(fc3_xboole_0,axiom, % 1.27/4.42 ! [A,B] : % 1.27/4.42 ( ~ empty(A) % 1.27/4.42 => ~ empty(set_union2(B,A)) ) ). % 1.27/4.42 % 1.27/4.42 fof(fc4_relat_1,axiom, % 1.27/4.42 ( empty(empty_set) % 1.27/4.42 & relation(empty_set) ) ). % 1.27/4.42 % 1.27/4.42 fof(idempotence_k2_xboole_0,axiom, % 1.27/4.42 ! [A,B] : set_union2(A,A) = A ). % 1.27/4.42 % 1.27/4.42 fof(rc1_funct_1,axiom, % 1.27/4.42 ? [A] : % 1.27/4.42 ( relation(A) % 1.27/4.42 & function(A) ) ). % 1.27/4.42 % 1.27/4.42 fof(rc1_relat_1,axiom, % 1.27/4.42 ? [A] : % 1.27/4.42 ( empty(A) % 1.27/4.42 & relation(A) ) ). % 1.27/4.42 % 1.27/4.42 fof(rc1_xboole_0,axiom, % 1.27/4.42 ? [A] : empty(A) ). % 1.27/4.42 % 1.27/4.42 fof(rc2_funct_1,axiom, % 1.27/4.42 ? [A] : % 1.27/4.42 ( relation(A) % 1.27/4.42 & empty(A) % 1.27/4.42 & function(A) ) ). % 1.27/4.42 % 1.27/4.42 fof(rc2_relat_1,axiom, % 1.27/4.42 ? [A] : % 1.27/4.42 ( ~ empty(A) % 1.27/4.42 & relation(A) ) ). % 1.27/4.42 % 1.27/4.42 fof(rc2_xboole_0,axiom, % 1.27/4.42 ? [A] : ~ empty(A) ). % 1.27/4.42 % 1.27/4.42 fof(rc3_funct_1,axiom, % 1.27/4.42 ? [A] : % 1.27/4.42 ( relation(A) % 1.27/4.42 & function(A) % 1.27/4.42 & one_to_one(A) ) ). % 1.27/4.42 % 1.27/4.42 fof(rc3_relat_1,axiom, % 1.27/4.42 ? [A] : % 1.27/4.42 ( relation(A) % 1.27/4.42 & relation_empty_yielding(A) ) ). % 1.27/4.42 % 1.27/4.42 fof(rc4_funct_1,axiom, % 1.27/4.42 ? [A] : % 1.27/4.42 ( relation(A) % 1.27/4.42 & relation_empty_yielding(A) % 1.27/4.42 & function(A) ) ). % 1.27/4.42 % 1.27/4.42 fof(rc5_funct_1,axiom, % 1.27/4.42 ? [A] : % 1.27/4.42 ( relation(A) % 1.27/4.42 & relation_non_empty(A) % 1.27/4.42 & function(A) ) ). % 1.27/4.42 % 1.27/4.42 fof(t10_ordinal1,conjecture, % 1.27/4.42 ! [A] : in(A,succ(A)) ). % 1.27/4.42 % 1.27/4.42 fof(t1_boole,axiom, % 1.27/4.42 ! [A] : set_union2(A,empty_set) = A ). % 1.27/4.42 % 1.27/4.42 fof(t1_subset,axiom, % 1.27/4.42 ! [A,B] : % 1.27/4.42 ( in(A,B) % 1.27/4.42 => element(A,B) ) ). % 1.27/4.42 % 1.27/4.42 fof(t2_subset,axiom, % 1.27/4.42 ! [A,B] : % 1.27/4.42 ( element(A,B) % 1.27/4.42 => ( empty(B) % 1.27/4.42 | in(A,B) ) ) ). % 1.27/4.42 % 1.27/4.42 fof(t6_boole,axiom, % 1.27/4.42 ! [A] : % 1.27/4.42 ( empty(A) % 1.27/4.42 => A = empty_set ) ). % 1.27/4.42 % 1.27/4.42 fof(t7_boole,axiom, % 1.27/4.42 ! [A,B] : % 1.27/4.42 ~ ( in(A,B) % 1.27/4.42 & empty(B) ) ). % 1.27/4.42 % 1.27/4.42 fof(t8_boole,axiom, % 1.27/4.42 ! [A,B] : % 1.27/4.42 ~ ( empty(A) % 1.27/4.42 & A != B % 1.27/4.42 & empty(B) ) ). % 1.27/4.42 % 1.27/4.42 %------------------------------------------------------------------------------ % 1.27/4.42 %------------------------------------------- % 1.27/4.42 % Proof found % 1.27/4.42 % SZS status Theorem for theBenchmark % 1.27/4.42 % SZS output start Proof % 1.27/4.42 %ClaNum:78(EqnAxiom:22) % 1.27/4.42 %VarNum:141(SingletonVarNum:57) % 1.27/4.42 %MaxLitNum:4 % 1.27/4.42 %MaxfuncDepth:2 % 1.27/4.42 %SharedTerms:40 % 1.27/4.42 %goalClause: 55 % 1.27/4.42 %singleGoalClaCount:1 % 1.27/4.42 [25]P1(a1) % 1.27/4.42 [26]P1(a2) % 1.27/4.42 [27]P1(a12) % 1.27/4.42 [28]P1(a13) % 1.27/4.42 [29]P3(a3) % 1.27/4.42 [30]P3(a13) % 1.27/4.42 [31]P3(a4) % 1.27/4.42 [32]P3(a5) % 1.27/4.42 [33]P3(a7) % 1.27/4.42 [35]P4(a1) % 1.27/4.42 [36]P4(a3) % 1.27/4.42 [37]P4(a2) % 1.27/4.42 [38]P4(a13) % 1.27/4.42 [39]P4(a14) % 1.27/4.42 [40]P4(a4) % 1.27/4.42 [41]P4(a6) % 1.27/4.42 [42]P4(a5) % 1.27/4.42 [43]P4(a7) % 1.27/4.42 [44]P5(a4) % 1.27/4.42 [45]P7(a1) % 1.27/4.42 [46]P7(a6) % 1.27/4.42 [47]P7(a5) % 1.27/4.42 [48]P8(a7) % 1.27/4.42 [53]~P1(a14) % 1.27/4.42 [54]~P1(a16) % 1.27/4.42 [55]~P6(a9,f15(a9,f17(a9))) % 1.27/4.42 [49]E(f15(x491,a1),x491) % 1.27/4.42 [50]E(f15(x501,x501),x501) % 1.27/4.42 [51]P2(f8(x511),x511) % 1.27/4.42 [56]~P1(f15(x561,f17(x561))) % 1.27/4.42 [52]E(f15(x521,x522),f15(x522,x521)) % 1.27/4.42 [57]~P1(x571)+E(x571,a1) % 1.27/4.42 [58]~P1(x581)+P3(x581) % 1.27/4.42 [59]~P1(x591)+P4(x591) % 1.27/4.42 [63]~P1(x631)+~P6(x632,x631) % 1.27/4.42 [65]~P6(x651,x652)+P2(x651,x652) % 1.27/4.42 [68]~P6(x682,x681)+~P6(x681,x682) % 1.27/4.42 [69]P1(x691)+~P1(f15(x692,x691)) % 1.27/4.42 [70]P1(x701)+~P1(f15(x701,x702)) % 1.27/4.42 [60]~P1(x602)+~P1(x601)+E(x601,x602) % 1.27/4.42 [66]~P2(x662,x661)+P1(x661)+P6(x662,x661) % 1.27/4.42 [67]~P4(x672)+~P4(x671)+P4(f15(x671,x672)) % 1.27/4.42 [71]E(f10(x712,x711),x712)+P6(f10(x712,x711),x711)+E(x711,f17(x712)) % 1.27/4.42 [75]~E(f10(x752,x751),x752)+~P6(f10(x752,x751),x751)+E(x751,f17(x752)) % 1.27/4.42 [62]P6(x621,x622)+~E(x621,x623)+~E(x622,f17(x623)) % 1.27/4.42 [64]~P6(x641,x643)+E(x641,x642)+~E(x643,f17(x642)) % 1.27/4.42 [77]~P6(f11(x772,x773,x771),x771)+~P6(f11(x772,x773,x771),x773)+E(x771,f15(x772,x773)) % 1.27/4.42 [78]~P6(f11(x782,x783,x781),x781)+~P6(f11(x782,x783,x781),x782)+E(x781,f15(x782,x783)) % 1.27/4.42 [72]~P6(x721,x724)+P6(x721,x722)+~E(x722,f15(x723,x724)) % 1.27/4.42 [73]~P6(x731,x733)+P6(x731,x732)+~E(x732,f15(x733,x734)) % 1.27/4.42 [61]~P1(x611)+~P3(x611)+~P4(x611)+P5(x611) % 1.27/4.42 [76]P6(f11(x762,x763,x761),x761)+P6(f11(x762,x763,x761),x763)+P6(f11(x762,x763,x761),x762)+E(x761,f15(x762,x763)) % 1.27/4.42 [74]~P6(x741,x744)+P6(x741,x742)+P6(x741,x743)+~E(x744,f15(x743,x742)) % 1.27/4.42 %EqnAxiom % 1.27/4.42 [1]E(x11,x11) % 1.27/4.42 [2]E(x22,x21)+~E(x21,x22) % 1.27/4.42 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 1.27/4.42 [4]~E(x41,x42)+E(f15(x41,x43),f15(x42,x43)) % 1.27/4.42 [5]~E(x51,x52)+E(f15(x53,x51),f15(x53,x52)) % 1.27/4.42 [6]~E(x61,x62)+E(f11(x61,x63,x64),f11(x62,x63,x64)) % 1.27/4.42 [7]~E(x71,x72)+E(f11(x73,x71,x74),f11(x73,x72,x74)) % 1.27/4.42 [8]~E(x81,x82)+E(f11(x83,x84,x81),f11(x83,x84,x82)) % 1.27/4.42 [9]~E(x91,x92)+E(f8(x91),f8(x92)) % 1.27/4.42 [10]~E(x101,x102)+E(f17(x101),f17(x102)) % 1.27/4.42 [11]~E(x111,x112)+E(f10(x111,x113),f10(x112,x113)) % 1.27/4.42 [12]~E(x121,x122)+E(f10(x123,x121),f10(x123,x122)) % 1.27/4.42 [13]~P1(x131)+P1(x132)+~E(x131,x132) % 1.27/4.42 [14]P6(x142,x143)+~E(x141,x142)+~P6(x141,x143) % 1.27/4.42 [15]P6(x153,x152)+~E(x151,x152)+~P6(x153,x151) % 1.27/4.42 [16]~P4(x161)+P4(x162)+~E(x161,x162) % 1.27/4.42 [17]~P3(x171)+P3(x172)+~E(x171,x172) % 1.27/4.42 [18]~P5(x181)+P5(x182)+~E(x181,x182) % 1.27/4.42 [19]P2(x192,x193)+~E(x191,x192)+~P2(x191,x193) % 1.27/4.42 [20]P2(x203,x202)+~E(x201,x202)+~P2(x203,x201) % 1.27/4.42 [21]~P8(x211)+P8(x212)+~E(x211,x212) % 1.27/4.42 [22]~P7(x221)+P7(x222)+~E(x221,x222) % 1.27/4.42 % 1.27/4.42 %------------------------------------------- % 1.27/4.42 cnf(79,plain, % 1.27/4.42 (~P6(x791,f17(x792))+E(x791,x792)), % 1.27/4.42 inference(equality_inference,[],[64])). % 1.27/4.42 cnf(80,plain, % 1.27/4.42 (~P6(x801,x802)+P6(x801,f15(x803,x802))), % 1.27/4.42 inference(equality_inference,[],[72])). % 1.27/4.42 cnf(81,plain, % 1.27/4.42 (~P6(x811,x812)+P6(x811,f15(x812,x813))), % 1.27/4.42 inference(equality_inference,[],[73])). % 1.27/4.42 cnf(82,plain, % 1.27/4.42 (~P6(x821,f15(x822,x823))+P6(x821,x823)+P6(x821,x822)), % 1.27/4.42 inference(equality_inference,[],[74])). % 1.27/4.42 cnf(83,plain, % 1.27/4.42 (~P6(x831,a1)), % 1.27/4.42 inference(scs_inference,[],[25,63])). % 1.27/4.42 cnf(85,plain, % 1.27/4.42 (E(x851,f15(x851,x851))), % 1.27/4.42 inference(scs_inference,[],[50,25,63,2])). % 1.27/4.42 cnf(86,plain, % 1.27/4.42 (P6(f8(a14),a14)), % 1.27/4.42 inference(scs_inference,[],[51,50,25,53,63,2,66])). % 1.27/4.42 cnf(87,plain, % 1.27/4.42 (P2(f8(x871),x871)), % 1.27/4.42 inference(rename_variables,[],[51])). % 1.27/4.42 cnf(89,plain, % 1.27/4.42 (P6(f15(x891,x891),f15(f17(x891),a1))), % 1.27/4.42 inference(scs_inference,[],[51,50,49,25,53,63,2,66,62])). % 1.27/4.42 cnf(93,plain, % 1.27/4.42 (E(f15(x931,x931),x931)), % 1.27/4.42 inference(rename_variables,[],[50])). % 1.27/4.42 cnf(96,plain, % 1.27/4.42 (E(f15(x961,x961),x961)), % 1.27/4.42 inference(rename_variables,[],[50])). % 1.27/4.42 cnf(100,plain, % 1.27/4.42 (E(f15(x1001,x1001),x1001)), % 1.27/4.42 inference(rename_variables,[],[50])). % 1.27/4.42 cnf(102,plain, % 1.27/4.42 (~E(a14,f15(a1,a1))), % 1.27/4.42 inference(scs_inference,[],[51,50,93,96,100,49,25,53,63,2,66,62,72,73,15,64,3])). % 1.27/4.42 cnf(103,plain, % 1.27/4.42 (E(f15(x1031,x1031),x1031)), % 1.27/4.42 inference(rename_variables,[],[50])). % 1.27/4.42 cnf(104,plain, % 1.27/4.42 (~P1(f15(a14,a14))), % 1.27/4.42 inference(scs_inference,[],[51,50,93,96,100,103,49,25,53,63,2,66,62,72,73,15,64,3,13])). % 1.27/4.42 cnf(105,plain, % 1.27/4.42 (E(f15(x1051,x1051),x1051)), % 1.27/4.42 inference(rename_variables,[],[50])). % 1.27/4.42 cnf(107,plain, % 1.27/4.42 (P2(f8(x1071),x1071)), % 1.27/4.42 inference(rename_variables,[],[51])). % 1.27/4.42 cnf(108,plain, % 1.27/4.42 (P5(a13)), % 1.27/4.42 inference(scs_inference,[],[51,87,50,93,96,100,103,105,49,25,53,28,30,38,63,2,66,62,72,73,15,64,3,13,20,61])). % 1.27/4.42 cnf(110,plain, % 1.27/4.42 (P6(f8(a14),f15(x1101,a14))), % 1.27/4.42 inference(scs_inference,[],[51,87,50,93,96,100,103,105,49,25,53,28,30,38,63,2,66,62,72,73,15,64,3,13,20,61,80])). % 1.27/4.42 cnf(112,plain, % 1.27/4.42 (P6(f8(a14),f15(a14,x1121))), % 1.27/4.43 inference(scs_inference,[],[51,87,50,93,96,100,103,105,49,25,53,28,30,38,63,2,66,62,72,73,15,64,3,13,20,61,80,81])). % 1.27/4.43 cnf(114,plain, % 1.27/4.43 (~P6(a14,f8(a14))), % 1.27/4.43 inference(scs_inference,[],[51,87,50,93,96,100,103,105,49,25,53,28,30,38,63,2,66,62,72,73,15,64,3,13,20,61,80,81,68])). % 1.27/4.43 cnf(118,plain, % 1.27/4.43 (~P6(f8(a14),f15(a1,a1))), % 1.27/4.43 inference(scs_inference,[],[51,87,50,93,96,100,103,105,49,25,53,28,30,38,63,2,66,62,72,73,15,64,3,13,20,61,80,81,68,79,82])). % 1.27/4.43 cnf(121,plain, % 1.27/4.43 (P2(x1211,x1212)+~E(f8(x1212),x1211)), % 1.27/4.43 inference(scs_inference,[],[51,87,107,50,93,96,100,103,105,49,25,53,28,30,38,63,2,66,62,72,73,15,64,3,13,20,61,80,81,68,79,82,14,19])). % 1.27/4.43 cnf(123,plain, % 1.27/4.43 (~P3(f15(x1231,x1231))+P3(x1231)), % 1.27/4.43 inference(scs_inference,[],[51,87,107,50,93,96,100,103,105,49,25,53,28,30,38,63,2,66,62,72,73,15,64,3,13,20,61,80,81,68,79,82,14,19,16,17])). % 1.27/4.43 cnf(129,plain, % 1.27/4.43 (E(x1291,f15(x1291,x1291))), % 1.27/4.43 inference(rename_variables,[],[85])). % 1.27/4.43 cnf(130,plain, % 1.27/4.43 (~P6(f15(f17(x1301),a1),f15(x1301,x1301))), % 1.27/4.43 inference(scs_inference,[],[89,85,121,68])). % 1.27/4.43 cnf(132,plain, % 1.27/4.43 (~P6(x1321,a2)), % 1.27/4.43 inference(scs_inference,[],[89,85,26,121,68,63])). % 1.27/4.43 cnf(134,plain, % 1.27/4.43 (P6(f8(a14),f15(x1341,f15(x1342,a14)))), % 1.27/4.43 inference(scs_inference,[],[89,110,85,26,121,68,63,80])). % 1.27/4.43 cnf(136,plain, % 1.27/4.43 (P6(f8(a14),f15(f15(x1361,a14),x1362))), % 1.27/4.43 inference(scs_inference,[],[89,110,85,26,121,68,63,80,81])). % 1.27/4.43 cnf(140,plain, % 1.27/4.43 (E(x1401,f15(x1401,a1))), % 1.27/4.43 inference(scs_inference,[],[89,110,85,102,49,26,121,68,63,80,81,79,2])). % 1.27/4.43 cnf(141,plain, % 1.27/4.43 (P7(f15(a1,a1))), % 1.27/4.43 inference(scs_inference,[],[89,110,85,129,102,49,26,45,121,68,63,80,81,79,2,22])). % 1.27/4.43 cnf(142,plain, % 1.27/4.43 (E(x1421,f15(x1421,x1421))), % 1.27/4.43 inference(rename_variables,[],[85])). % 1.27/4.43 cnf(143,plain, % 1.27/4.43 (~P6(f8(a14),f15(f15(a1,a1),f15(a1,a1)))), % 1.27/4.43 inference(scs_inference,[],[89,110,118,85,129,102,49,26,45,121,68,63,80,81,79,2,22,82])). % 1.27/4.43 cnf(145,plain, % 1.27/4.43 (P4(f15(a1,a1))), % 1.27/4.43 inference(scs_inference,[],[89,110,118,85,129,142,102,49,26,35,45,121,68,63,80,81,79,2,22,82,16])). % 1.27/4.43 cnf(146,plain, % 1.27/4.43 (E(x1461,f15(x1461,x1461))), % 1.27/4.43 inference(rename_variables,[],[85])). % 1.27/4.43 cnf(151,plain, % 1.27/4.43 (E(x1511,f15(x1511,x1511))), % 1.27/4.43 inference(rename_variables,[],[85])). % 1.27/4.43 cnf(152,plain, % 1.27/4.43 (~E(f15(f17(x1521),a1),a1)), % 1.27/4.43 inference(scs_inference,[],[86,89,110,118,85,129,142,146,83,102,108,49,26,35,45,121,68,63,80,81,79,2,22,82,16,73,18,15])). % 1.27/4.43 cnf(153,plain, % 1.27/4.43 (~P6(x1531,a1)), % 1.27/4.43 inference(rename_variables,[],[83])). % 1.27/4.43 cnf(156,plain, % 1.27/4.43 (P1(f15(a1,a1))), % 1.27/4.43 inference(scs_inference,[],[86,89,110,118,85,129,142,146,151,83,104,102,108,49,25,26,35,45,121,68,63,80,81,79,2,22,82,16,73,18,15,66,13])). % 1.27/4.43 cnf(157,plain, % 1.27/4.43 (E(x1571,f15(x1571,x1571))), % 1.27/4.43 inference(rename_variables,[],[85])). % 1.27/4.43 cnf(158,plain, % 1.27/4.43 (P8(f15(a7,a7))), % 1.27/4.43 inference(scs_inference,[],[86,89,110,118,85,129,142,146,151,157,83,104,102,108,49,25,26,35,45,48,121,68,63,80,81,79,2,22,82,16,73,18,15,66,13,21])). % 1.27/4.43 cnf(159,plain, % 1.27/4.43 (E(x1591,f15(x1591,x1591))), % 1.27/4.43 inference(rename_variables,[],[85])). % 1.27/4.43 cnf(160,plain, % 1.27/4.43 (P3(f15(a3,a3))), % 1.27/4.43 inference(scs_inference,[],[86,89,110,118,85,129,142,146,151,157,159,83,104,102,108,49,25,26,29,35,45,48,121,68,63,80,81,79,2,22,82,16,73,18,15,66,13,21,17])). % 1.27/4.43 cnf(161,plain, % 1.27/4.43 (E(x1611,f15(x1611,x1611))), % 1.27/4.43 inference(rename_variables,[],[85])). % 1.27/4.43 cnf(162,plain, % 1.27/4.43 (P2(f8(x1621),f15(x1621,x1621))), % 1.27/4.43 inference(scs_inference,[],[86,89,110,118,51,85,129,142,146,151,157,159,161,83,104,102,108,49,25,26,29,35,45,48,121,68,63,80,81,79,2,22,82,16,73,18,15,66,13,21,17,20])). % 1.27/4.43 cnf(163,plain, % 1.27/4.43 (P2(f8(x1631),x1631)), % 1.27/4.43 inference(rename_variables,[],[51])). % 1.27/4.43 cnf(166,plain, % 1.27/4.43 (P6(f15(f8(a14),f8(a14)),a14)), % 1.27/4.43 inference(scs_inference,[],[86,89,110,118,51,163,85,129,142,146,151,157,159,161,83,104,102,108,49,25,26,29,35,45,48,121,68,63,80,81,79,2,22,82,16,73,18,15,66,13,21,17,20,19,14])). % 1.27/4.43 cnf(167,plain, % 1.27/4.43 (E(x1671,f15(x1671,x1671))), % 1.27/4.43 inference(rename_variables,[],[85])). % 1.27/4.43 cnf(168,plain, % 1.27/4.43 (P6(f11(a1,a1,a14),a14)), % 1.27/4.43 inference(scs_inference,[],[86,89,110,118,51,163,85,129,142,146,151,157,159,161,83,153,104,102,108,49,25,26,29,35,45,48,121,68,63,80,81,79,2,22,82,16,73,18,15,66,13,21,17,20,19,14,76])). % 1.27/4.43 cnf(169,plain, % 1.27/4.43 (~P6(x1691,a1)), % 1.27/4.43 inference(rename_variables,[],[83])). % 1.27/4.43 cnf(171,plain, % 1.27/4.43 (P6(f15(a14,a14),f17(a14))), % 1.27/4.43 inference(scs_inference,[],[86,89,110,118,51,163,85,129,142,146,151,157,159,161,83,153,169,52,104,102,108,49,25,26,29,35,45,48,121,68,63,80,81,79,2,22,82,16,73,18,15,66,13,21,17,20,19,14,76,74])). % 1.27/4.43 cnf(178,plain, % 1.27/4.43 (E(a14,f15(f15(a14,a14),a1))), % 1.27/4.43 inference(scs_inference,[],[86,89,110,118,51,163,85,129,142,146,151,157,159,161,167,83,153,169,52,104,102,108,49,25,26,29,35,45,48,121,68,63,80,81,79,2,22,82,16,73,18,15,66,13,21,17,20,19,14,76,74,57,3])). % 1.27/4.43 cnf(182,plain, % 1.27/4.43 (P6(f8(a14),f15(f15(a14,x1821),x1822))), % 1.27/4.43 inference(scs_inference,[],[112,81])). % 1.27/4.43 cnf(187,plain, % 1.27/4.43 (E(x1871,f15(x1871,a1))), % 1.27/4.43 inference(rename_variables,[],[140])). % 1.27/4.43 cnf(190,plain, % 1.27/4.43 (~P6(f15(x1901,f15(x1902,a14)),f8(a14))), % 1.27/4.43 inference(scs_inference,[],[134,112,152,140,81,57,121,80,68])). % 1.27/4.43 cnf(192,plain, % 1.27/4.43 (~P6(x1921,f15(a1,a1))), % 1.27/4.43 inference(scs_inference,[],[134,112,152,156,140,81,57,121,80,68,63])). % 1.27/4.43 cnf(194,plain, % 1.27/4.43 (~P6(f15(f17(x1941),a1),f17(a1))), % 1.27/4.43 inference(scs_inference,[],[134,112,152,156,140,81,57,121,80,68,63,79])). % 1.27/4.43 cnf(197,plain, % 1.27/4.43 (~P6(f15(f17(x1971),a1),f15(f15(x1971,x1971),f15(x1971,x1971)))), % 1.27/4.43 inference(scs_inference,[],[134,112,152,156,130,140,178,81,57,121,80,68,63,79,2,82])). % 1.27/4.43 cnf(199,plain, % 1.27/4.43 (P6(f8(a16),a16)), % 1.27/4.43 inference(scs_inference,[],[134,112,152,51,156,130,140,178,54,81,57,121,80,68,63,79,2,82,66])). % 1.27/4.43 cnf(202,plain, % 1.27/4.43 (P7(f15(f15(a1,a1),a1))), % 1.27/4.43 inference(scs_inference,[],[134,112,152,51,156,130,140,187,178,54,141,81,57,121,80,68,63,79,2,82,66,22])). % 1.27/4.43 cnf(203,plain, % 1.27/4.43 (E(x2031,f15(x2031,a1))), % 1.27/4.43 inference(rename_variables,[],[140])). % 1.27/4.43 cnf(204,plain, % 1.27/4.43 (P1(f15(f15(a1,a1),a1))), % 1.27/4.43 inference(scs_inference,[],[134,112,152,51,156,130,140,187,203,178,54,141,81,57,121,80,68,63,79,2,82,66,22,13])). % 1.27/4.43 cnf(205,plain, % 1.27/4.43 (E(x2051,f15(x2051,a1))), % 1.27/4.43 inference(rename_variables,[],[140])). % 1.27/4.43 cnf(206,plain, % 1.27/4.43 (P4(f15(f15(a1,a1),a1))), % 1.27/4.43 inference(scs_inference,[],[134,112,152,51,156,130,140,187,203,205,178,54,145,141,81,57,121,80,68,63,79,2,82,66,22,13,16])). % 1.27/4.43 cnf(207,plain, % 1.27/4.43 (E(x2071,f15(x2071,a1))), % 1.27/4.43 inference(rename_variables,[],[140])). % 1.27/4.43 cnf(208,plain, % 1.27/4.43 (P3(f15(f15(a3,a3),a1))), % 1.27/4.43 inference(scs_inference,[],[134,112,152,51,156,130,140,187,203,205,207,178,54,145,141,160,81,57,121,80,68,63,79,2,82,66,22,13,16,17])). % 1.27/4.43 cnf(209,plain, % 1.27/4.43 (E(x2091,f15(x2091,a1))), % 1.27/4.43 inference(rename_variables,[],[140])). % 1.27/4.43 cnf(210,plain, % 1.27/4.43 (~E(f15(x2101,f15(x2102,a14)),f15(f15(a1,a1),f15(a1,a1)))), % 1.27/4.43 inference(scs_inference,[],[143,134,112,152,51,156,130,140,187,203,205,207,178,54,145,141,160,81,57,121,80,68,63,79,2,82,66,22,13,16,17,15])). % 1.27/4.43 cnf(211,plain, % 1.27/4.43 (~E(f8(a14),f15(f17(a14),a1))), % 1.27/4.43 inference(scs_inference,[],[143,134,112,152,51,156,130,140,187,203,205,207,178,54,145,141,160,81,57,121,80,68,63,79,2,82,66,22,13,16,17,15,14])). % 1.27/4.43 cnf(214,plain, % 1.27/4.43 (P5(f15(a13,a1))), % 1.27/4.43 inference(scs_inference,[],[143,134,112,152,51,156,130,140,187,203,205,207,209,178,54,108,145,141,160,81,57,121,80,68,63,79,2,82,66,22,13,16,17,15,14,18])). % 1.27/4.43 cnf(215,plain, % 1.27/4.43 (E(x2151,f15(x2151,a1))), % 1.27/4.43 inference(rename_variables,[],[140])). % 1.27/4.43 cnf(216,plain, % 1.27/4.43 (P8(f15(f15(a7,a7),a1))), % 1.27/4.43 inference(scs_inference,[],[143,134,112,152,51,156,130,140,187,203,205,207,209,215,178,54,108,145,141,158,160,81,57,121,80,68,63,79,2,82,66,22,13,16,17,15,14,18,21])). % 1.27/4.43 cnf(218,plain, % 1.27/4.43 (P6(f15(f8(a14),f8(a14)),f15(a14,a14))), % 1.27/4.43 inference(scs_inference,[],[143,134,112,152,166,51,156,130,140,187,203,205,207,209,215,178,54,83,108,145,141,158,160,81,57,121,80,68,63,79,2,82,66,22,13,16,17,15,14,18,21,74])). % 1.27/4.43 cnf(221,plain, % 1.27/4.43 (~E(f15(x2211,a14),f15(a1,a1))), % 1.27/4.43 inference(scs_inference,[],[143,134,112,152,166,51,156,130,140,187,203,205,207,209,215,178,54,83,108,145,141,158,160,81,57,121,80,68,63,79,2,82,66,22,13,16,17,15,14,18,21,74,5])). % 1.27/4.43 cnf(224,plain, % 1.27/4.43 (~P1(f15(x2241,a14))), % 1.27/4.43 inference(scs_inference,[],[143,134,112,152,166,51,156,130,140,187,203,205,207,209,215,178,54,83,108,145,141,158,160,81,57,121,80,68,63,79,2,82,66,22,13,16,17,15,14,18,21,74,5,78,60])). % 1.27/4.43 cnf(230,plain, % 1.27/4.43 (P6(f15(f8(a14),f8(a14)),f15(f15(a14,a14),x2301))), % 1.27/4.43 inference(scs_inference,[],[218,81])). % 1.27/4.43 cnf(234,plain, % 1.27/4.43 (P6(f15(f8(a14),f8(a14)),f15(x2341,f15(a14,a14)))), % 1.27/4.43 inference(scs_inference,[],[218,81,68,80])). % 1.27/4.43 cnf(236,plain, % 1.27/4.43 (~P6(x2361,f15(f15(a1,a1),a1))), % 1.27/4.43 inference(scs_inference,[],[218,204,81,68,80,63])). % 1.27/4.43 cnf(246,plain, % 1.27/4.43 (~E(f15(x2461,f15(x2462,a14)),f15(a1,a1))), % 1.27/4.43 inference(scs_inference,[],[55,210,218,85,192,221,204,56,81,68,80,63,79,82,66,3])). % 1.27/4.43 cnf(247,plain, % 1.27/4.43 (E(x2471,f15(x2471,x2471))), % 1.27/4.43 inference(rename_variables,[],[85])). % 1.27/4.43 cnf(248,plain, % 1.27/4.43 (~E(f15(f15(x2481,a14),x2482),f15(f15(a1,a1),f15(a1,a1)))), % 1.27/4.43 inference(scs_inference,[],[55,210,218,136,143,85,192,221,204,56,81,68,80,63,79,82,66,3,15])). % 1.27/4.43 cnf(249,plain, % 1.27/4.43 (P4(f15(f15(a14,a14),a1))), % 1.27/4.43 inference(scs_inference,[],[55,210,218,136,143,85,178,192,221,204,56,39,81,68,80,63,79,82,66,3,15,16])). % 1.27/4.43 cnf(251,plain, % 1.27/4.43 (E(f15(x2511,x2512),f15(x2512,x2511))), % 1.27/4.43 inference(rename_variables,[],[52])). % 1.27/4.43 cnf(253,plain, % 1.27/4.43 (E(f15(x2531,x2532),f15(x2532,x2531))), % 1.27/4.43 inference(rename_variables,[],[52])). % 1.27/4.43 cnf(254,plain, % 1.27/4.43 (P1(f15(f15(a1,a1),f15(a1,a1)))), % 1.27/4.43 inference(scs_inference,[],[55,210,218,136,143,85,247,178,52,251,156,192,221,204,56,202,208,39,81,68,80,63,79,82,66,3,15,16,17,22,13])). % 1.27/4.43 cnf(263,plain, % 1.27/4.43 (~E(f15(x2631,a14),a1)), % 1.27/4.43 inference(scs_inference,[],[55,210,218,136,143,85,247,178,52,251,253,156,192,221,204,56,130,83,202,208,216,39,81,68,80,63,79,82,66,3,15,16,17,22,13,14,21,76,5])). % 1.27/4.43 cnf(271,plain, % 1.27/4.43 (P6(f15(a14,a14),f15(f17(a14),x2711))), % 1.27/4.43 inference(scs_inference,[],[171,81])). % 1.27/4.43 cnf(277,plain, % 1.27/4.43 (~P6(x2771,f15(f15(a1,a1),f15(a1,a1)))), % 1.27/4.43 inference(scs_inference,[],[230,171,254,246,81,79,68,63])). % 1.27/4.43 cnf(279,plain, % 1.27/4.43 (P6(f15(a14,a14),f15(x2791,f17(a14)))), % 1.27/4.43 inference(scs_inference,[],[230,171,254,246,81,79,68,63,80])). % 1.27/4.43 cnf(283,plain, % 1.27/4.43 (~P1(f15(f15(x2831,a14),x2832))), % 1.27/4.43 inference(scs_inference,[],[248,230,171,254,246,190,81,79,68,63,80,82,60])). % 1.27/4.43 cnf(292,plain, % 1.27/4.43 (~E(f8(a14),f17(a14))), % 1.27/4.43 inference(scs_inference,[],[211,248,197,230,171,140,52,254,246,236,190,206,81,79,68,63,80,82,60,66,15,16,3])). % 1.27/4.43 cnf(294,plain, % 1.27/4.43 (P6(a14,f17(a14))), % 1.27/4.43 inference(scs_inference,[],[211,248,197,230,171,50,140,52,254,246,236,190,206,81,79,68,63,80,82,60,66,15,16,3,14])). % 1.27/4.43 cnf(304,plain, % 1.27/4.43 (P6(f8(a16),f15(a16,x3041))), % 1.27/4.43 inference(scs_inference,[],[199,81])). % 1.27/4.43 cnf(306,plain, % 1.27/4.43 (P6(f8(a16),f15(x3061,a16))), % 1.27/4.43 inference(scs_inference,[],[199,81,80])). % 1.27/4.43 cnf(308,plain, % 1.27/4.43 (~P6(f15(x3081,a14),f17(a1))), % 1.27/4.43 inference(scs_inference,[],[199,263,81,80,79])). % 1.27/4.43 cnf(310,plain, % 1.27/4.43 (~P6(f15(f17(a14),x3101),f15(a14,a14))), % 1.27/4.43 inference(scs_inference,[],[271,199,263,81,80,79,68])). % 1.27/4.43 cnf(312,plain, % 1.27/4.43 (~P6(x3121,a12)), % 1.27/4.43 inference(scs_inference,[],[271,199,263,27,81,80,79,68,63])). % 1.27/4.43 cnf(319,plain, % 1.27/4.43 (P2(f8(x3191),x3191)), % 1.27/4.43 inference(rename_variables,[],[51])). % 1.27/4.43 cnf(320,plain, % 1.27/4.43 (~E(f15(f17(a14),x3201),f15(f15(a1,a1),f15(a1,a1)))), % 1.27/4.43 inference(scs_inference,[],[51,210,271,199,49,254,263,277,114,27,81,80,79,68,63,60,82,20,15])). % 1.27/4.43 cnf(322,plain, % 1.27/4.43 (P4(f15(a14,a14))), % 1.27/4.43 inference(scs_inference,[],[51,210,271,199,49,254,263,277,114,249,27,81,80,79,68,63,60,82,20,15,16])). % 1.27/4.43 cnf(323,plain, % 1.27/4.43 (E(f15(x3231,a1),x3231)), % 1.27/4.43 inference(rename_variables,[],[49])). % 1.27/4.43 cnf(324,plain, % 1.27/4.43 (E(f15(a14,a1),f15(f15(a14,a14),a1))), % 1.27/4.43 inference(scs_inference,[],[51,210,271,199,49,323,178,254,263,277,114,249,27,81,80,79,68,63,60,82,20,15,16,3])). % 1.27/4.43 cnf(326,plain, % 1.27/4.43 (P6(f15(f8(a16),f8(a16)),a16)), % 1.27/4.43 inference(scs_inference,[],[51,210,271,199,49,323,85,178,254,263,277,114,249,27,81,80,79,68,63,60,82,20,15,16,3,14])). % 1.27/4.43 cnf(328,plain, % 1.27/4.43 (~E(f17(a14),f15(a1,a1))), % 1.27/4.43 inference(scs_inference,[],[51,210,271,199,49,323,85,178,254,263,277,114,249,27,81,80,79,68,63,60,82,20,15,16,3,14,4])). % 1.27/4.43 cnf(329,plain, % 1.27/4.43 (E(f15(f15(a14,a14),a1),f15(a14,a1))), % 1.27/4.43 inference(scs_inference,[],[51,210,271,199,49,323,85,178,254,263,277,114,249,27,81,80,79,68,63,60,82,20,15,16,3,14,4,2])). % 1.27/4.43 cnf(337,plain, % 1.27/4.43 (P6(f8(f15(a14,a1)),f15(a14,a1))), % 1.27/4.43 inference(scs_inference,[],[51,319,210,271,199,49,323,85,178,254,263,277,283,114,292,83,249,27,81,80,79,68,63,60,82,20,15,16,3,14,4,2,75,13,76,66])). % 1.27/4.43 cnf(346,plain, % 1.27/4.43 (P6(f8(f15(a14,a1)),f15(f15(a14,a1),x3461))), % 1.27/4.43 inference(scs_inference,[],[337,81])). % 1.27/4.43 cnf(348,plain, % 1.27/4.43 (~P6(x3481,a13)), % 1.27/4.43 inference(scs_inference,[],[337,28,81,63])). % 1.27/4.43 cnf(350,plain, % 1.27/4.43 (P6(f8(f15(a14,a1)),f15(x3501,f15(a14,a1)))), % 1.27/4.43 inference(scs_inference,[],[337,28,81,63,80])). % 1.27/4.43 cnf(356,plain, % 1.27/4.43 (~P6(f15(f17(a14),x3561),f15(f15(a14,a14),f15(a14,a14)))), % 1.27/4.43 inference(scs_inference,[],[337,292,310,28,81,63,80,68,79,82])). % 1.27/4.43 cnf(360,plain, % 1.27/4.43 (~P2(f15(f17(a14),x3601),f15(a14,a14))), % 1.27/4.43 inference(scs_inference,[],[337,320,254,224,292,310,28,81,63,80,68,79,82,60,66])). % 1.27/4.43 cnf(363,plain, % 1.27/4.43 (~E(f15(a14,a1),a2)), % 1.27/4.43 inference(scs_inference,[],[337,320,254,224,292,310,132,28,81,63,80,68,79,82,60,66,15])). % 1.27/4.43 cnf(368,plain, % 1.27/4.43 (E(f15(x3681,x3682),f15(x3682,x3681))), % 1.27/4.43 inference(rename_variables,[],[52])). % 1.27/4.43 cnf(369,plain, % 1.27/4.43 (~E(f8(a16),f15(f17(a16),a1))), % 1.27/4.43 inference(scs_inference,[],[211,337,320,304,85,52,254,224,292,310,132,130,322,28,81,63,80,68,79,82,60,66,15,16,3,14])). % 1.27/4.43 cnf(372,plain, % 1.27/4.43 (P6(f8(f15(a14,a1)),a14)), % 1.27/4.43 inference(scs_inference,[],[211,337,320,304,85,52,368,254,224,292,310,132,130,83,322,28,81,63,80,68,79,82,60,66,15,16,3,14,74])). % 1.27/4.43 cnf(394,plain, % 1.27/4.43 (~P6(f15(a14,a1),f17(a2))), % 1.27/4.43 inference(scs_inference,[],[306,363,81,79])). % 1.27/4.43 cnf(402,plain, % 1.27/4.43 (~P1(f17(a14))), % 1.27/4.43 inference(scs_inference,[],[346,306,363,372,156,329,328,81,79,68,80,73,60])). % 1.27/4.43 cnf(406,plain, % 1.27/4.43 (~E(f15(f15(a14,a1),x4061),a12)), % 1.27/4.43 inference(scs_inference,[],[346,306,363,372,156,329,328,194,312,81,79,68,80,73,60,82,15])). % 1.27/4.43 cnf(408,plain, % 1.27/4.43 (~P2(f15(f17(a14),x4081),f15(f15(a14,a14),f15(a14,a14)))), % 1.27/4.43 inference(scs_inference,[],[346,356,306,363,372,156,329,328,283,194,312,81,79,68,80,73,60,82,15,66])). % 1.27/4.43 cnf(416,plain, % 1.27/4.43 (~E(f15(f8(a14),f8(a14)),f15(f17(a14),x4161))), % 1.27/4.43 inference(scs_inference,[],[346,356,234,306,363,372,50,156,52,324,329,328,283,194,312,214,249,81,79,68,80,73,60,82,15,66,16,18,3,14])). % 1.27/4.43 cnf(418,plain, % 1.27/4.43 (P6(f8(f15(a14,a1)),f15(a14,a14))), % 1.27/4.43 inference(scs_inference,[],[346,356,234,306,363,372,50,178,156,52,324,329,328,283,194,312,83,214,249,81,79,68,80,73,60,82,15,66,16,18,3,14,74])). % 1.27/4.43 cnf(421,plain, % 1.27/4.43 (E(f15(f15(a14,a14),a1),f15(f15(a14,a1),f15(a14,a1)))), % 1.27/4.43 inference(scs_inference,[],[346,356,234,306,363,372,50,178,156,52,324,329,328,283,194,312,83,214,249,81,79,68,80,73,60,82,15,66,16,18,3,14,74,2])). % 1.27/4.43 cnf(437,plain, % 1.27/4.43 (P6(f8(f15(a14,a1)),f15(f15(a14,a14),x4371))), % 1.27/4.43 inference(scs_inference,[],[418,81])). % 1.27/4.43 cnf(439,plain, % 1.27/4.43 (~P6(f15(f15(a14,a1),x4391),f17(a12))), % 1.27/4.43 inference(scs_inference,[],[418,406,81,79])). % 1.27/4.43 cnf(441,plain, % 1.27/4.43 (P6(f8(f15(a14,a1)),f15(x4411,f15(a14,a14)))), % 1.27/4.43 inference(scs_inference,[],[418,406,81,79,80])). % 1.27/4.43 cnf(451,plain, % 1.27/4.43 (P6(f8(f17(a14)),f17(a14))), % 1.27/4.43 inference(scs_inference,[],[360,51,418,406,162,394,402,27,81,79,80,68,82,60,19,66])). % 1.27/4.43 cnf(454,plain, % 1.27/4.43 (~E(f15(a14,a14),a13)), % 1.27/4.43 inference(scs_inference,[],[360,51,418,406,162,394,348,402,27,81,79,80,68,82,60,19,66,15])). % 1.27/4.43 cnf(460,plain, % 1.27/4.43 (E(f15(f15(a14,a14),a1),f15(f15(a14,a1),a1))), % 1.27/4.43 inference(scs_inference,[],[360,51,418,406,49,162,324,421,394,348,402,310,27,249,81,79,80,68,82,60,19,66,15,16,3,14,2])). % 1.27/4.43 cnf(477,plain, % 1.27/4.43 (P6(f8(f17(a14)),f15(f17(a14),x4771))), % 1.27/4.43 inference(scs_inference,[],[451,81])). % 1.27/4.43 cnf(479,plain, % 1.27/4.43 (~P6(f15(a14,a14),f17(a13))), % 1.27/4.43 inference(scs_inference,[],[451,454,81,79])). % 1.27/4.43 cnf(489,plain, % 1.27/4.43 (~E(f15(f15(a14,a14),x4891),f15(a1,a1))), % 1.27/4.43 inference(scs_inference,[],[408,437,451,454,162,439,192,81,79,68,80,82,19,15])). % 1.27/4.43 cnf(492,plain, % 1.27/4.43 (~E(f8(a16),f17(a16))), % 1.27/4.43 inference(scs_inference,[],[408,369,437,451,454,140,162,460,439,192,249,81,79,68,80,82,19,15,16,3])). % 1.27/4.43 cnf(494,plain, % 1.27/4.43 (P6(f15(f15(a14,a14),a1),f17(a14))), % 1.27/4.43 inference(scs_inference,[],[408,369,437,451,454,294,178,140,162,460,439,192,249,81,79,68,80,82,19,15,16,3,14])). % 1.27/4.43 cnf(510,plain, % 1.27/4.43 (P6(f15(f15(a14,a14),a1),f15(f17(a14),x5101))), % 1.27/4.43 inference(scs_inference,[],[494,81])). % 1.27/4.43 cnf(514,plain, % 1.27/4.43 (P6(f15(f15(a14,a14),a1),f15(x5141,f17(a14)))), % 1.27/4.43 inference(scs_inference,[],[489,494,81,79,80])). % 1.27/4.43 cnf(522,plain, % 1.27/4.43 (~P6(f15(a14,a14),f15(f17(a13),f17(a13)))), % 1.27/4.43 inference(scs_inference,[],[489,441,477,494,49,479,81,79,80,68,64,82])). % 1.27/4.43 cnf(524,plain, % 1.27/4.43 (~E(f15(x5241,f15(a14,a1)),f15(f15(a1,a1),f15(a1,a1)))), % 1.27/4.43 inference(scs_inference,[],[489,441,350,477,494,49,479,277,81,79,80,68,64,82,15])). % 1.27/4.43 cnf(530,plain, % 1.27/4.43 (P6(x5301,f15(f17(x5301),a1))), % 1.27/4.43 inference(scs_inference,[],[416,489,441,350,477,494,89,50,49,140,53,479,277,81,79,80,68,64,82,15,13,3,14])). % 1.27/4.43 cnf(532,plain, % 1.27/4.43 (~E(f15(a14,a1),f15(a1,a1))), % 1.27/4.43 inference(scs_inference,[],[416,489,441,350,477,494,89,50,49,140,53,479,277,81,79,80,68,64,82,15,13,3,14,5])). % 1.27/4.43 cnf(533,plain, % 1.27/4.43 (P2(a14,f17(a14))), % 1.27/4.43 inference(scs_inference,[],[416,489,441,350,477,494,89,50,49,140,53,479,277,81,79,80,68,64,82,15,13,3,14,5,121])). % 1.27/4.43 cnf(534,plain, % 1.27/4.43 (E(a14,f8(f17(a14)))), % 1.27/4.43 inference(scs_inference,[],[416,489,441,350,477,494,89,50,49,140,53,479,277,81,79,80,68,64,82,15,13,3,14,5,121,2])). % 1.27/4.43 cnf(539,plain, % 1.27/4.43 (P2(f15(f15(a14,a14),a1),f17(a14))), % 1.27/4.43 inference(scs_inference,[],[416,489,441,350,477,494,89,50,49,178,140,254,53,479,492,277,81,79,80,68,64,82,15,13,3,14,5,121,2,71,60,19])). % 1.27/4.43 cnf(551,plain, % 1.27/4.43 (P6(f15(f8(a16),f8(a16)),f15(a16,x5511))), % 1.27/4.43 inference(scs_inference,[],[326,81])). % 1.27/4.43 cnf(553,plain, % 1.27/4.43 (~P6(f15(x5531,f17(a14)),f15(a14,a14))), % 1.27/4.43 inference(scs_inference,[],[279,326,81,68])). % 1.27/4.43 cnf(555,plain, % 1.27/4.43 (P6(f15(f8(a16),f8(a16)),f15(x5551,a16))), % 1.27/4.43 inference(scs_inference,[],[279,326,81,68,80])). % 1.27/4.43 cnf(563,plain, % 1.27/4.43 (P2(f15(a14,a14),f17(a14))), % 1.27/4.43 inference(scs_inference,[],[524,279,326,49,254,328,539,308,81,68,80,79,82,60,19])). % 1.27/4.43 cnf(565,plain, % 1.27/4.43 (~E(f15(x5651,f17(a14)),f15(f17(a13),f17(a13)))), % 1.27/4.44 inference(scs_inference,[],[524,279,522,326,49,254,328,539,308,81,68,80,79,82,60,19,15])). % 1.27/4.44 cnf(566,plain, % 1.27/4.44 (P2(f15(f15(a14,a14),a1),f15(f17(a14),f17(a14)))), % 1.27/4.44 inference(scs_inference,[],[524,279,522,326,49,85,254,328,539,308,81,68,80,79,82,60,19,15,20])). % 1.27/4.44 cnf(567,plain, % 1.27/4.44 (E(x5671,f15(x5671,x5671))), % 1.27/4.44 inference(rename_variables,[],[85])). % 1.27/4.44 cnf(568,plain, % 1.27/4.44 (E(f15(a14,a14),f8(f17(a14)))), % 1.27/4.44 inference(scs_inference,[],[524,279,522,326,50,49,85,254,328,539,308,534,81,68,80,79,82,60,19,15,20,3])). % 1.27/4.44 cnf(570,plain, % 1.27/4.44 (P6(f15(f11(a1,a1,a14),f11(a1,a1,a14)),a14)), % 1.27/4.44 inference(scs_inference,[],[524,279,522,326,50,49,85,567,254,328,168,539,308,534,81,68,80,79,82,60,19,15,20,3,14])). % 1.27/4.44 cnf(572,plain, % 1.27/4.44 (~E(f17(a14),f17(a13))), % 1.27/4.44 inference(scs_inference,[],[524,279,522,326,50,49,85,567,254,328,168,539,308,534,81,68,80,79,82,60,19,15,20,3,14,5])). % 1.27/4.44 cnf(573,plain, % 1.27/4.44 (E(f8(f17(a14)),f15(a14,a14))), % 1.27/4.44 inference(scs_inference,[],[524,279,522,326,50,49,85,567,254,328,168,539,308,534,81,68,80,79,82,60,19,15,20,3,14,5,2])). % 1.27/4.44 cnf(576,plain, % 1.27/4.44 (P6(f15(f8(a14),f8(a14)),f8(f17(a14)))), % 1.27/4.44 inference(scs_inference,[],[524,279,522,326,166,50,49,85,567,254,328,168,539,308,534,81,68,80,79,82,60,19,15,20,3,14,5,2,75,73])). % 1.27/4.44 cnf(590,plain, % 1.27/4.44 (P6(f15(f8(a16),f8(a16)),f15(x5901,f15(a16,x5902)))), % 1.27/4.44 inference(scs_inference,[],[576,551,492,572,10,81,79,68,80])). % 1.27/4.44 cnf(594,plain, % 1.27/4.44 (P6(f15(f11(a1,a1,a14),f11(a1,a1,a14)),f8(f17(a14)))), % 1.27/4.44 inference(scs_inference,[],[576,551,570,329,492,573,572,10,81,79,68,80,73,72])). % 1.27/4.44 cnf(596,plain, % 1.27/4.44 (~P6(f15(x5961,f17(a14)),f15(f15(a14,a14),f15(a14,a14)))), % 1.27/4.44 inference(scs_inference,[],[576,551,570,329,492,553,573,572,10,81,79,68,80,73,72,82])). % 1.27/4.44 cnf(607,plain, % 1.27/4.44 (P6(f8(a14),f8(f17(a14)))), % 1.27/4.44 inference(scs_inference,[],[248,576,551,570,50,49,85,329,224,492,566,553,573,572,236,10,81,79,68,80,73,72,82,66,19,15,3,14])). % 1.27/4.44 cnf(609,plain, % 1.27/4.44 (P6(f15(f11(a1,a1,a14),f11(a1,a1,a14)),f15(a14,a14))), % 1.27/4.44 inference(scs_inference,[],[248,576,551,570,50,49,178,85,329,224,492,566,553,573,572,236,83,10,81,79,68,80,73,72,82,66,19,15,3,14,74])). % 1.27/4.44 cnf(617,plain, % 1.27/4.44 (P6(f15(f11(a1,a1,a14),f11(a1,a1,a14)),f15(f15(a14,a14),x6171))), % 1.27/4.44 inference(scs_inference,[],[609,81])). % 1.27/4.44 cnf(619,plain, % 1.27/4.44 (P6(f15(f11(a1,a1,a14),f11(a1,a1,a14)),f15(x6191,f15(a14,a14)))), % 1.27/4.44 inference(scs_inference,[],[609,81,80])). % 1.27/4.44 cnf(625,plain, % 1.27/4.44 (P6(f15(f11(a1,a1,a14),f11(a1,a1,a14)),f15(a14,a1))), % 1.27/4.44 inference(scs_inference,[],[609,324,532,81,80,68,79,73])). % 1.27/4.44 cnf(630,plain, % 1.27/4.44 (P2(a14,f15(f17(a14),a1))), % 1.27/4.44 inference(scs_inference,[],[609,596,140,324,283,532,533,81,80,68,79,73,66,20])). % 1.27/4.44 cnf(632,plain, % 1.27/4.44 (P2(f15(a1,f15(a14,a14)),f15(f17(a14),f17(a14)))), % 1.27/4.44 inference(scs_inference,[],[609,596,52,140,324,283,532,533,566,81,80,68,79,73,66,20,19])). % 1.27/4.44 cnf(634,plain, % 1.27/4.44 (~E(f15(a14,a14),a2)), % 1.27/4.44 inference(scs_inference,[],[609,596,52,140,324,283,532,533,566,132,81,80,68,79,73,66,20,19,15])). % 1.27/4.44 cnf(657,plain, % 1.27/4.44 (P6(f15(f11(a1,a1,a14),f11(a1,a1,a14)),f15(f15(a14,a1),x6571))), % 1.27/4.44 inference(scs_inference,[],[625,81])). % 1.27/4.44 cnf(659,plain, % 1.27/4.44 (P6(f15(f11(a1,a1,a14),f11(a1,a1,a14)),f15(x6591,f15(a14,a1)))), % 1.27/4.44 inference(scs_inference,[],[625,81,80])). % 1.27/4.44 cnf(667,plain, % 1.27/4.44 (P2(f15(a14,a14),f15(f17(a14),a1))), % 1.27/4.44 inference(scs_inference,[],[617,625,634,140,563,81,80,79,68,82,20])). % 1.27/4.44 cnf(670,plain, % 1.27/4.44 (~E(f15(x6701,f15(a16,x6702)),f15(a1,a1))), % 1.27/4.44 inference(scs_inference,[],[617,625,590,634,178,140,563,192,630,81,80,79,68,82,20,19,15])). % 1.27/4.44 cnf(673,plain, % 1.27/4.44 (E(f15(x6731,x6731),x6731)), % 1.27/4.44 inference(rename_variables,[],[50])). % 1.27/4.44 cnf(674,plain, % 1.27/4.44 (P6(f11(a1,a1,a14),f15(a14,a1))), % 1.27/4.44 inference(scs_inference,[],[617,625,590,634,50,673,178,140,568,563,192,630,81,80,79,68,82,20,19,15,3,14])). % 1.27/4.44 cnf(676,plain, % 1.27/4.44 (~E(f15(a16,x6761),a1)), % 1.27/4.44 inference(scs_inference,[],[617,625,590,634,50,673,178,140,568,563,192,630,81,80,79,68,82,20,19,15,3,14,5])). % 1.27/4.44 cnf(677,plain, % 1.27/4.44 (E(f8(f17(a14)),f15(f15(a14,a14),f15(a14,a14)))), % 1.27/4.44 inference(scs_inference,[],[617,625,590,634,50,673,178,140,568,563,192,630,81,80,79,68,82,20,19,15,3,14,5,2])). % 1.27/4.44 cnf(693,plain, % 1.27/4.44 (P6(f11(a1,a1,a14),f15(f15(a14,a1),x6931))), % 1.27/4.44 inference(scs_inference,[],[674,676,57,81])). % 1.27/4.44 cnf(695,plain, % 1.27/4.44 (P2(f15(f15(a14,a14),f15(a14,a14)),f17(a14))), % 1.27/4.44 inference(scs_inference,[],[674,677,676,57,81,121])). % 1.27/4.44 cnf(696,plain, % 1.27/4.44 (P6(f11(a1,a1,a14),f15(x6961,f15(a14,a1)))), % 1.27/4.44 inference(scs_inference,[],[674,677,676,57,81,121,80])). % 1.27/4.44 cnf(704,plain, % 1.27/4.44 (~P1(f15(x7041,f15(a16,x7042)))), % 1.27/4.44 inference(scs_inference,[],[619,674,670,156,421,677,676,57,81,121,80,68,79,73,60])). % 1.27/4.44 cnf(709,plain, % 1.27/4.44 (P2(f15(a1,f15(a14,a14)),f17(a14))), % 1.27/4.44 inference(scs_inference,[],[619,674,670,50,156,421,130,677,632,676,57,81,121,80,68,79,73,60,66,20])). % 1.27/4.44 cnf(710,plain, % 1.27/4.44 (E(f15(x7101,x7101),x7101)), % 1.27/4.44 inference(rename_variables,[],[50])). % 1.27/4.44 cnf(711,plain, % 1.27/4.44 (~E(f8(f17(a14)),f15(a1,a1))), % 1.27/4.44 inference(scs_inference,[],[619,607,674,670,50,156,421,192,130,677,632,676,57,81,121,80,68,79,73,60,66,20,15])). % 1.27/4.44 cnf(713,plain, % 1.27/4.44 (P6(f11(a1,a1,a14),f8(f17(a14)))), % 1.27/4.44 inference(scs_inference,[],[619,607,674,670,594,50,710,156,421,192,130,677,632,676,57,81,121,80,68,79,73,60,66,20,15,14])). % 1.27/4.44 cnf(715,plain, % 1.27/4.44 (P6(f11(a1,a1,a14),f15(a14,a14))), % 1.27/4.44 inference(scs_inference,[],[619,607,674,670,594,50,710,156,324,421,192,130,677,632,676,83,57,81,121,80,68,79,73,60,66,20,15,14,74])). % 1.27/4.44 cnf(727,plain, % 1.27/4.44 (P3(a1)), % 1.27/4.44 inference(scs_inference,[],[156,58,123])). % 1.27/4.44 cnf(728,plain, % 1.27/4.44 (P6(f11(a1,a1,a14),f15(f15(a14,a14),x7281))), % 1.27/4.44 inference(scs_inference,[],[715,81])). % 1.27/4.44 cnf(732,plain, % 1.27/4.44 (P6(f11(a1,a1,a14),f15(x7321,f15(a14,a14)))), % 1.27/4.44 inference(scs_inference,[],[715,81,68,80])). % 1.27/4.44 cnf(741,plain, % 1.27/4.44 (E(x7411,f15(x7411,x7411))), % 1.27/4.44 inference(rename_variables,[],[85])). % 1.27/4.44 cnf(742,plain, % 1.27/4.44 (P3(f15(a1,a1))), % 1.27/4.44 inference(scs_inference,[],[715,711,197,85,741,704,695,727,81,68,80,79,66,20,17])). % 1.27/4.44 cnf(744,plain, % 1.27/4.44 (~E(f15(f15(a14,a1),x7441),f15(a1,a1))), % 1.27/4.44 inference(scs_inference,[],[715,693,711,197,85,741,192,704,695,727,81,68,80,79,66,20,17,15])). % 1.27/4.44 cnf(746,plain, % 1.27/4.44 (E(f15(a14,a1),f8(f17(a14)))), % 1.27/4.44 inference(scs_inference,[],[715,693,711,197,49,85,741,534,192,704,695,727,81,68,80,79,66,20,17,15,3])). % 1.27/4.44 cnf(748,plain, % 1.27/4.44 (~E(f11(a1,a1,a14),f15(x7481,f17(a14)))), % 1.27/4.44 inference(scs_inference,[],[715,693,711,197,49,85,741,534,553,192,704,695,727,81,68,80,79,66,20,17,15,3,14])). % 1.27/4.44 cnf(749,plain, % 1.27/4.44 (P5(a1)), % 1.27/4.44 inference(scs_inference,[],[715,693,711,197,49,85,741,534,25,553,192,704,695,727,35,81,68,80,79,66,20,17,15,3,14,61])). % 1.27/4.44 cnf(752,plain, % 1.27/4.44 (E(f8(f17(a14)),f15(a14,a1))), % 1.27/4.44 inference(scs_inference,[],[715,693,711,197,49,85,741,534,25,553,192,704,695,727,35,81,68,80,79,66,20,17,15,3,14,61,4,2])). % 1.27/4.44 cnf(774,plain, % 1.27/4.44 (P6(f15(f8(a16),f8(a16)),f15(f15(x7741,a16),x7742))), % 1.27/4.44 inference(scs_inference,[],[555,81])). % 1.27/4.44 cnf(777,plain, % 1.27/4.44 (~P6(f15(f15(a14,a14),x7771),f11(a1,a1,a14))), % 1.27/4.44 inference(scs_inference,[],[728,555,752,81,121,68])). % 1.27/4.44 cnf(779,plain, % 1.27/4.44 (P6(f15(f8(a16),f8(a16)),f15(x7791,f15(x7792,a16)))), % 1.27/4.44 inference(scs_inference,[],[728,555,752,81,121,68,80])). % 1.27/4.44 cnf(784,plain, % 1.27/4.44 (E(x7841,f15(x7841,x7841))), % 1.27/4.44 inference(rename_variables,[],[85])). % 1.27/4.44 cnf(785,plain, % 1.27/4.44 (P2(f15(a14,a1),f15(f17(a14),f17(a14)))), % 1.27/4.44 inference(scs_inference,[],[728,744,555,85,784,752,749,81,121,68,80,79,18,20])). % 1.27/4.44 cnf(786,plain, % 1.27/4.44 (E(x7861,f15(x7861,x7861))), % 1.27/4.44 inference(rename_variables,[],[85])). % 1.27/4.44 cnf(791,plain, % 1.27/4.44 (~E(f15(x7911,f15(a14,a1)),f15(a1,a1))), % 1.27/4.44 inference(scs_inference,[],[728,744,696,555,49,85,784,786,568,192,752,749,742,81,121,68,80,79,18,20,17,3,15])). % 1.27/4.44 cnf(822,plain, % 1.27/4.44 (E(x8221,f15(x8221,a1))), % 1.27/4.44 inference(rename_variables,[],[140])). % 1.27/4.44 cnf(826,plain, % 1.27/4.44 (E(x8261,f15(x8261,a1))), % 1.27/4.44 inference(rename_variables,[],[140])). % 1.27/4.44 cnf(827,plain, % 1.27/4.44 (~E(f15(f15(x8271,a16),x8272),f15(a1,a1))), % 1.27/4.44 inference(scs_inference,[],[732,791,774,294,50,140,822,746,709,192,742,81,79,68,80,20,3,17,15])). % 1.27/4.44 cnf(829,plain, % 1.27/4.44 (P6(f15(f11(a1,a1,a14),a1),f8(f17(a14)))), % 1.27/4.44 inference(scs_inference,[],[732,791,713,774,294,50,140,822,826,746,709,192,742,81,79,68,80,20,3,17,15,14])). % 1.27/4.44 cnf(831,plain, % 1.27/4.44 (P5(f15(f15(a1,a1),a1))), % 1.27/4.44 inference(scs_inference,[],[732,791,713,774,294,50,140,822,826,204,746,709,192,742,206,81,79,68,80,20,3,17,15,14,61])). % 1.27/4.44 cnf(839,plain, % 1.27/4.44 (P2(f15(f15(a14,a1),f15(a14,a1)),f17(a14))), % 1.27/4.44 inference(scs_inference,[],[565,732,791,713,774,294,50,140,822,826,204,746,709,192,742,206,81,79,68,80,20,3,17,15,14,61,4,2,60,57,121])). % 1.27/4.44 cnf(863,plain, % 1.27/4.44 (~E(f15(x8631,f15(x8632,a16)),f15(a1,a1))), % 1.27/4.44 inference(scs_inference,[],[657,827,779,304,49,52,85,156,746,192,831,839,81,79,80,68,60,20,18,3,15])). % 1.27/4.44 cnf(867,plain, % 1.27/4.44 (P6(f15(f11(a1,a1,a14),a1),a14)), % 1.27/4.44 inference(scs_inference,[],[657,827,779,829,182,596,304,49,52,85,156,573,746,192,831,839,81,79,80,68,60,20,18,3,15,14,74])). % 1.27/4.44 cnf(869,plain, % 1.27/4.44 (E(f8(f17(a14)),f15(f15(a14,a1),a1))), % 1.27/4.44 inference(scs_inference,[],[657,827,779,829,182,596,304,49,52,85,156,573,746,192,831,839,81,79,80,68,60,20,18,3,15,14,74,2])). % 1.27/4.44 cnf(888,plain, % 1.27/4.44 (P6(f15(f11(a1,a1,a14),a1),f15(a14,x8881))), % 1.27/4.44 inference(scs_inference,[],[867,81])). % 1.27/4.44 cnf(897,plain, % 1.27/4.44 (P6(f15(f11(a1,a1,a14),a1),f15(f15(a14,a14),a1))), % 1.27/4.44 inference(scs_inference,[],[659,863,867,329,869,81,121,79,68,80,73])). % 1.27/4.44 cnf(903,plain, % 1.27/4.44 (~E(f15(f17(a14),x9031),f11(a1,a1,a14))), % 1.27/4.44 inference(scs_inference,[],[659,863,510,867,85,156,329,777,869,81,121,79,68,80,73,60,20,15])). % 1.27/4.44 cnf(929,plain, % 1.27/4.44 (P6(f15(f11(a1,a1,a14),a1),f15(f15(a14,x9291),x9292))), % 1.27/4.44 inference(scs_inference,[],[888,81])). % 1.27/4.44 cnf(939,plain, % 1.27/4.44 (~E(f15(x9391,f17(a14)),f15(a1,a1))), % 1.27/4.44 inference(scs_inference,[],[903,514,888,140,695,192,81,80,68,79,20,15])). % 1.27/4.44 cnf(949,plain, % 1.27/4.44 (E(f15(f10(a14,a1),a1),a14)), % 1.27/4.44 inference(scs_inference,[],[748,903,514,897,888,49,140,53,695,192,83,81,80,68,79,20,15,14,5,71,60,13,3])). % 1.27/4.44 cnf(951,plain, % 1.27/4.44 (E(a14,f10(a14,a1))), % 1.27/4.44 inference(scs_inference,[],[748,903,514,897,888,49,140,53,695,192,83,81,80,68,79,20,15,14,5,71,60,13,3,2])). % 1.27/4.44 cnf(952,plain, % 1.27/4.44 (P6(f8(f10(a14,a1)),f10(a14,a1))), % 1.27/4.44 inference(scs_inference,[],[51,748,903,514,897,888,49,140,53,695,192,83,81,80,68,79,20,15,14,5,71,60,13,3,2,66])). % 1.27/4.44 cnf(955,plain, % 1.27/4.44 (P4(f10(a14,a1))), % 1.27/4.44 inference(scs_inference,[],[51,748,903,514,897,888,49,140,53,695,192,83,39,81,80,68,79,20,15,14,5,71,60,13,3,2,66,16])). % 1.27/4.44 cnf(980,plain, % 1.27/4.44 (E(f15(x9801,x9802),f15(x9802,x9801))), % 1.27/4.44 inference(rename_variables,[],[52])). % 1.27/4.44 cnf(982,plain, % 1.27/4.44 (E(f15(x9821,x9822),f15(x9822,x9821))), % 1.27/4.44 inference(rename_variables,[],[52])). % 1.27/4.44 cnf(990,plain, % 1.27/4.44 (P6(x9901,f17(x9901))), % 1.27/4.44 inference(scs_inference,[],[952,939,530,929,356,50,52,980,982,85,156,53,667,785,192,951,949,83,955,81,80,2,79,68,73,60,16,19,20,13,15,3,14,74])). % 1.27/4.44 cnf(1007,plain, % 1.27/4.44 ($false), % 1.27/4.44 inference(scs_inference,[],[55,990,81,68,80]), % 1.27/4.44 ['proof']). % 1.27/4.44 % SZS output end Proof % 1.27/4.44 % Total time :0.740000s %------------------------------------------------------------------------------