%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU230+1 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n021.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 0.59s 0.68s % Output : CNFRefutation 0.59s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SEU230+1 : TPTP v8.2.0. Released v3.3.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n021.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 10:57:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 0.59/0.67 %------------------------------------------- % 0.59/0.67 % File :CSE---1.7 % 0.59/0.67 % Problem :theBenchmark % 0.59/0.67 % Transform :cnf % 0.59/0.67 % Format :tptp:raw % 0.59/0.67 % Command :java -jar mcs_scs.jar %d %s % 0.59/0.67 % 0.59/0.67 % Result :Theorem 0.070000s % 0.59/0.67 % Output :CNFRefutation 0.070000s % 0.59/0.67 %------------------------------------------- % 0.59/0.67 %------------------------------------------------------------------------------ % 0.59/0.67 % File : SEU230+1 : TPTP v8.2.0. Released v3.3.0. % 0.59/0.67 % Domain : Set theory % 0.59/0.67 % Problem : MPTP bushy problem t10_ordinal1 % 0.59/0.67 % Version : [Urb07] axioms : Especial. % 0.59/0.67 % English : % 0.59/0.67 % 0.59/0.67 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 0.59/0.67 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 0.59/0.67 % Source : [Urb07] % 0.59/0.67 % Names : bushy-t10_ordinal1 [Urb07] % 0.59/0.67 % 0.59/0.67 % Status : Theorem % 0.59/0.67 % 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.33 v6.0.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.25 v3.7.0, 0.20 v3.5.0, 0.16 v3.4.0, 0.21 v3.3.0 % 0.59/0.67 % Syntax : Number of formulae : 38 ( 15 unt; 0 def) % 0.59/0.67 % Number of atoms : 75 ( 9 equ) % 0.59/0.67 % Maximal formula atoms : 6 ( 1 avg) % 0.59/0.67 % Number of connectives : 48 ( 11 ~; 2 |; 21 &) % 0.59/0.67 % ( 4 <=>; 10 =>; 0 <=; 0 <~>) % 0.59/0.67 % Maximal formula depth : 8 ( 3 avg) % 0.59/0.67 % Maximal term depth : 3 ( 1 avg) % 0.59/0.67 % Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty) % 0.59/0.67 % Number of functors : 4 ( 4 usr; 1 con; 0-2 aty) % 0.59/0.67 % Number of variables : 46 ( 36 !; 10 ?) % 0.59/0.67 % SPC : FOF_THM_RFO_SEQ % 0.59/0.67 % 0.59/0.67 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 0.59/0.67 % library, www.mizar.org % 0.59/0.67 %------------------------------------------------------------------------------ % 0.59/0.67 fof(antisymmetry_r2_hidden,axiom, % 0.59/0.67 ! [A,B] : % 0.59/0.67 ( in(A,B) % 0.59/0.67 => ~ in(B,A) ) ). % 0.59/0.67 % 0.59/0.67 fof(cc1_funct_1,axiom, % 0.59/0.67 ! [A] : % 0.59/0.67 ( empty(A) % 0.59/0.67 => function(A) ) ). % 0.59/0.67 % 0.59/0.67 fof(cc1_relat_1,axiom, % 0.59/0.67 ! [A] : % 0.59/0.67 ( empty(A) % 0.59/0.67 => relation(A) ) ). % 0.59/0.67 % 0.59/0.67 fof(cc2_funct_1,axiom, % 0.59/0.67 ! [A] : % 0.59/0.67 ( ( relation(A) % 0.59/0.67 & empty(A) % 0.59/0.67 & function(A) ) % 0.59/0.67 => ( relation(A) % 0.59/0.67 & function(A) % 0.59/0.67 & one_to_one(A) ) ) ). % 0.59/0.67 % 0.59/0.67 fof(commutativity_k2_xboole_0,axiom, % 0.59/0.67 ! [A,B] : set_union2(A,B) = set_union2(B,A) ). % 0.59/0.67 % 0.59/0.67 fof(d1_ordinal1,axiom, % 0.59/0.67 ! [A] : succ(A) = set_union2(A,singleton(A)) ). % 0.59/0.67 % 0.59/0.67 fof(d1_tarski,axiom, % 0.59/0.67 ! [A,B] : % 0.59/0.67 ( B = singleton(A) % 0.59/0.67 <=> ! [C] : % 0.59/0.67 ( in(C,B) % 0.59/0.67 <=> C = A ) ) ). % 0.59/0.67 % 0.59/0.67 fof(d2_xboole_0,axiom, % 0.59/0.67 ! [A,B,C] : % 0.59/0.67 ( C = set_union2(A,B) % 0.59/0.67 <=> ! [D] : % 0.59/0.67 ( in(D,C) % 0.59/0.67 <=> ( in(D,A) % 0.59/0.67 | in(D,B) ) ) ) ). % 0.59/0.67 % 0.59/0.67 fof(dt_k1_ordinal1,axiom, % 0.59/0.67 $true ). % 0.59/0.67 % 0.59/0.67 fof(dt_k1_tarski,axiom, % 0.59/0.67 $true ). % 0.59/0.67 % 0.59/0.67 fof(dt_k1_xboole_0,axiom, % 0.59/0.67 $true ). % 0.59/0.67 % 0.59/0.67 fof(dt_k2_xboole_0,axiom, % 0.59/0.67 $true ). % 0.59/0.67 % 0.59/0.67 fof(dt_m1_subset_1,axiom, % 0.59/0.67 $true ). % 0.59/0.68 % 0.59/0.68 fof(existence_m1_subset_1,axiom, % 0.59/0.68 ! [A] : % 0.59/0.68 ? [B] : element(B,A) ). % 0.59/0.68 % 0.59/0.68 fof(fc12_relat_1,axiom, % 0.59/0.68 ( empty(empty_set) % 0.59/0.68 & relation(empty_set) % 0.59/0.68 & relation_empty_yielding(empty_set) ) ). % 0.59/0.68 % 0.59/0.68 fof(fc1_ordinal1,axiom, % 0.59/0.68 ! [A] : ~ empty(succ(A)) ). % 0.59/0.68 % 0.59/0.68 fof(fc1_xboole_0,axiom, % 0.59/0.68 empty(empty_set) ). % 0.59/0.68 % 0.59/0.68 fof(fc2_relat_1,axiom, % 0.59/0.68 ! [A,B] : % 0.59/0.68 ( ( relation(A) % 0.59/0.68 & relation(B) ) % 0.59/0.68 => relation(set_union2(A,B)) ) ). % 0.59/0.68 % 0.59/0.68 fof(fc2_xboole_0,axiom, % 0.59/0.68 ! [A,B] : % 0.59/0.68 ( ~ empty(A) % 0.59/0.68 => ~ empty(set_union2(A,B)) ) ). % 0.59/0.68 % 0.59/0.68 fof(fc3_xboole_0,axiom, % 0.59/0.68 ! [A,B] : % 0.59/0.68 ( ~ empty(A) % 0.59/0.68 => ~ empty(set_union2(B,A)) ) ). % 0.59/0.68 % 0.59/0.68 fof(fc4_relat_1,axiom, % 0.59/0.68 ( empty(empty_set) % 0.59/0.68 & relation(empty_set) ) ). % 0.59/0.68 % 0.59/0.68 fof(idempotence_k2_xboole_0,axiom, % 0.59/0.68 ! [A,B] : set_union2(A,A) = A ). % 0.59/0.68 % 0.59/0.68 fof(rc1_funct_1,axiom, % 0.59/0.68 ? [A] : % 0.59/0.68 ( relation(A) % 0.59/0.68 & function(A) ) ). % 0.59/0.68 % 0.59/0.68 fof(rc1_relat_1,axiom, % 0.59/0.68 ? [A] : % 0.59/0.68 ( empty(A) % 0.59/0.68 & relation(A) ) ). % 0.59/0.68 % 0.59/0.68 fof(rc1_xboole_0,axiom, % 0.59/0.68 ? [A] : empty(A) ). % 0.59/0.68 % 0.59/0.68 fof(rc2_funct_1,axiom, % 0.59/0.68 ? [A] : % 0.59/0.68 ( relation(A) % 0.59/0.68 & empty(A) % 0.59/0.68 & function(A) ) ). % 0.59/0.68 % 0.59/0.68 fof(rc2_relat_1,axiom, % 0.59/0.68 ? [A] : % 0.59/0.68 ( ~ empty(A) % 0.59/0.68 & relation(A) ) ). % 0.59/0.68 % 0.59/0.68 fof(rc2_xboole_0,axiom, % 0.59/0.68 ? [A] : ~ empty(A) ). % 0.59/0.68 % 0.59/0.68 fof(rc3_funct_1,axiom, % 0.59/0.68 ? [A] : % 0.59/0.68 ( relation(A) % 0.59/0.68 & function(A) % 0.59/0.68 & one_to_one(A) ) ). % 0.59/0.68 % 0.59/0.68 fof(rc3_relat_1,axiom, % 0.59/0.68 ? [A] : % 0.59/0.68 ( relation(A) % 0.59/0.68 & relation_empty_yielding(A) ) ). % 0.59/0.68 % 0.59/0.68 fof(rc4_funct_1,axiom, % 0.59/0.68 ? [A] : % 0.59/0.68 ( relation(A) % 0.59/0.68 & relation_empty_yielding(A) % 0.59/0.68 & function(A) ) ). % 0.59/0.68 % 0.59/0.68 fof(t10_ordinal1,conjecture, % 0.59/0.68 ! [A] : in(A,succ(A)) ). % 0.59/0.68 % 0.59/0.68 fof(t1_boole,axiom, % 0.59/0.68 ! [A] : set_union2(A,empty_set) = A ). % 0.59/0.68 % 0.59/0.68 fof(t1_subset,axiom, % 0.59/0.68 ! [A,B] : % 0.59/0.68 ( in(A,B) % 0.59/0.68 => element(A,B) ) ). % 0.59/0.68 % 0.59/0.68 fof(t2_subset,axiom, % 0.59/0.68 ! [A,B] : % 0.59/0.68 ( element(A,B) % 0.59/0.68 => ( empty(B) % 0.59/0.68 | in(A,B) ) ) ). % 0.59/0.68 % 0.59/0.68 fof(t6_boole,axiom, % 0.59/0.68 ! [A] : % 0.59/0.68 ( empty(A) % 0.59/0.68 => A = empty_set ) ). % 0.59/0.68 % 0.59/0.68 fof(t7_boole,axiom, % 0.59/0.68 ! [A,B] : % 0.59/0.68 ~ ( in(A,B) % 0.59/0.68 & empty(B) ) ). % 0.59/0.68 % 0.59/0.68 fof(t8_boole,axiom, % 0.59/0.68 ! [A,B] : % 0.59/0.68 ~ ( empty(A) % 0.59/0.68 & A != B % 0.59/0.68 & empty(B) ) ). % 0.59/0.68 % 0.59/0.68 %------------------------------------------------------------------------------ % 0.59/0.68 %------------------------------------------- % 0.59/0.68 % Proof found % 0.59/0.68 % SZS status Theorem for theBenchmark % 0.59/0.68 % SZS output start Proof % 0.59/0.68 %ClaNum:74(EqnAxiom:21) % 0.59/0.68 %VarNum:141(SingletonVarNum:57) % 0.59/0.68 %MaxLitNum:4 % 0.59/0.68 %MaxfuncDepth:2 % 0.59/0.68 %SharedTerms:36 % 0.59/0.68 %goalClause: 51 % 0.59/0.68 %singleGoalClaCount:1 % 0.59/0.68 [24]P1(a1) % 0.59/0.68 [25]P1(a2) % 0.59/0.68 [26]P1(a11) % 0.59/0.68 [27]P1(a12) % 0.59/0.68 [28]P3(a3) % 0.59/0.68 [29]P3(a12) % 0.59/0.68 [30]P3(a4) % 0.59/0.68 [31]P3(a5) % 0.59/0.68 [33]P4(a1) % 0.59/0.68 [34]P4(a3) % 0.59/0.68 [35]P4(a2) % 0.59/0.68 [36]P4(a12) % 0.59/0.68 [37]P4(a13) % 0.59/0.68 [38]P4(a4) % 0.59/0.68 [39]P4(a6) % 0.59/0.68 [40]P4(a5) % 0.59/0.68 [41]P5(a4) % 0.59/0.68 [42]P7(a1) % 0.59/0.68 [43]P7(a6) % 0.59/0.68 [44]P7(a5) % 0.59/0.68 [49]~P1(a13) % 0.59/0.68 [50]~P1(a15) % 0.59/0.68 [51]~P6(a8,f14(a8,f16(a8))) % 0.59/0.68 [45]E(f14(x451,a1),x451) % 0.59/0.68 [46]E(f14(x461,x461),x461) % 0.59/0.68 [47]P2(f7(x471),x471) % 0.59/0.68 [52]~P1(f14(x521,f16(x521))) % 0.59/0.68 [48]E(f14(x481,x482),f14(x482,x481)) % 0.59/0.68 [53]~P1(x531)+E(x531,a1) % 0.59/0.68 [54]~P1(x541)+P3(x541) % 0.59/0.68 [55]~P1(x551)+P4(x551) % 0.59/0.68 [59]~P1(x591)+~P6(x592,x591) % 0.59/0.68 [61]~P6(x611,x612)+P2(x611,x612) % 0.59/0.68 [64]~P6(x642,x641)+~P6(x641,x642) % 0.59/0.68 [65]P1(x651)+~P1(f14(x652,x651)) % 0.59/0.68 [66]P1(x661)+~P1(f14(x661,x662)) % 0.59/0.68 [56]~P1(x562)+~P1(x561)+E(x561,x562) % 0.59/0.68 [62]~P2(x622,x621)+P1(x621)+P6(x622,x621) % 0.59/0.68 [63]~P4(x632)+~P4(x631)+P4(f14(x631,x632)) % 0.59/0.68 [67]E(f9(x672,x671),x672)+P6(f9(x672,x671),x671)+E(x671,f16(x672)) % 0.59/0.68 [71]~E(f9(x712,x711),x712)+~P6(f9(x712,x711),x711)+E(x711,f16(x712)) % 0.59/0.68 [58]P6(x581,x582)+~E(x581,x583)+~E(x582,f16(x583)) % 0.59/0.68 [60]~P6(x601,x603)+E(x601,x602)+~E(x603,f16(x602)) % 0.59/0.68 [73]~P6(f10(x732,x733,x731),x731)+~P6(f10(x732,x733,x731),x733)+E(x731,f14(x732,x733)) % 0.59/0.68 [74]~P6(f10(x742,x743,x741),x741)+~P6(f10(x742,x743,x741),x742)+E(x741,f14(x742,x743)) % 0.59/0.68 [68]~P6(x681,x684)+P6(x681,x682)+~E(x682,f14(x683,x684)) % 0.59/0.68 [69]~P6(x691,x693)+P6(x691,x692)+~E(x692,f14(x693,x694)) % 0.59/0.68 [57]~P1(x571)+~P3(x571)+~P4(x571)+P5(x571) % 0.59/0.68 [72]P6(f10(x722,x723,x721),x721)+P6(f10(x722,x723,x721),x723)+P6(f10(x722,x723,x721),x722)+E(x721,f14(x722,x723)) % 0.59/0.68 [70]~P6(x701,x704)+P6(x701,x702)+P6(x701,x703)+~E(x704,f14(x703,x702)) % 0.59/0.68 %EqnAxiom % 0.59/0.68 [1]E(x11,x11) % 0.59/0.68 [2]E(x22,x21)+~E(x21,x22) % 0.59/0.68 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.59/0.68 [4]~E(x41,x42)+E(f14(x41,x43),f14(x42,x43)) % 0.59/0.68 [5]~E(x51,x52)+E(f14(x53,x51),f14(x53,x52)) % 0.59/0.68 [6]~E(x61,x62)+E(f10(x61,x63,x64),f10(x62,x63,x64)) % 0.59/0.68 [7]~E(x71,x72)+E(f10(x73,x71,x74),f10(x73,x72,x74)) % 0.59/0.68 [8]~E(x81,x82)+E(f10(x83,x84,x81),f10(x83,x84,x82)) % 0.59/0.68 [9]~E(x91,x92)+E(f7(x91),f7(x92)) % 0.59/0.68 [10]~E(x101,x102)+E(f16(x101),f16(x102)) % 0.59/0.68 [11]~E(x111,x112)+E(f9(x111,x113),f9(x112,x113)) % 0.59/0.68 [12]~E(x121,x122)+E(f9(x123,x121),f9(x123,x122)) % 0.59/0.68 [13]~P1(x131)+P1(x132)+~E(x131,x132) % 0.59/0.68 [14]P6(x142,x143)+~E(x141,x142)+~P6(x141,x143) % 0.59/0.68 [15]P6(x153,x152)+~E(x151,x152)+~P6(x153,x151) % 0.59/0.68 [16]~P4(x161)+P4(x162)+~E(x161,x162) % 0.59/0.68 [17]~P3(x171)+P3(x172)+~E(x171,x172) % 0.59/0.68 [18]~P5(x181)+P5(x182)+~E(x181,x182) % 0.59/0.68 [19]P2(x192,x193)+~E(x191,x192)+~P2(x191,x193) % 0.59/0.68 [20]P2(x203,x202)+~E(x201,x202)+~P2(x203,x201) % 0.59/0.68 [21]~P7(x211)+P7(x212)+~E(x211,x212) % 0.59/0.68 % 0.59/0.68 %------------------------------------------- % 0.59/0.68 cnf(75,plain, % 0.59/0.68 (~P6(x751,f16(x752))+E(x751,x752)), % 0.59/0.68 inference(equality_inference,[],[60])). % 0.59/0.68 cnf(76,plain, % 0.59/0.68 (~P6(x761,x762)+P6(x761,f14(x763,x762))), % 0.59/0.68 inference(equality_inference,[],[68])). % 0.59/0.68 cnf(77,plain, % 0.59/0.68 (~P6(x771,x772)+P6(x771,f14(x772,x773))), % 0.59/0.68 inference(equality_inference,[],[69])). % 0.59/0.68 cnf(78,plain, % 0.59/0.68 (~P6(x781,f14(x782,x783))+P6(x781,x783)+P6(x781,x782)), % 0.59/0.68 inference(equality_inference,[],[70])). % 0.59/0.68 cnf(79,plain, % 0.59/0.68 (~P6(x791,a1)), % 0.59/0.68 inference(scs_inference,[],[24,59])). % 0.59/0.68 cnf(81,plain, % 0.59/0.68 (E(x811,f14(x811,x811))), % 0.59/0.68 inference(scs_inference,[],[46,24,59,2])). % 0.59/0.68 cnf(82,plain, % 0.59/0.68 (P6(f7(a13),a13)), % 0.59/0.68 inference(scs_inference,[],[47,46,24,49,59,2,62])). % 0.59/0.68 cnf(83,plain, % 0.59/0.68 (P2(f7(x831),x831)), % 0.59/0.68 inference(rename_variables,[],[47])). % 0.59/0.68 cnf(85,plain, % 0.59/0.68 (P6(f14(x851,x851),f14(f16(x851),a1))), % 0.59/0.68 inference(scs_inference,[],[47,46,45,24,49,59,2,62,58])). % 0.59/0.68 cnf(89,plain, % 0.59/0.68 (E(f14(x891,x891),x891)), % 0.59/0.68 inference(rename_variables,[],[46])). % 0.59/0.68 cnf(92,plain, % 0.59/0.68 (E(f14(x921,x921),x921)), % 0.59/0.68 inference(rename_variables,[],[46])). % 0.59/0.68 cnf(96,plain, % 0.59/0.68 (E(f14(x961,x961),x961)), % 0.59/0.68 inference(rename_variables,[],[46])). % 0.59/0.68 cnf(98,plain, % 0.59/0.68 (~E(a13,f14(a1,a1))), % 0.59/0.68 inference(scs_inference,[],[47,46,89,92,96,45,24,49,59,2,62,58,68,69,15,60,3])). % 0.59/0.68 cnf(99,plain, % 0.59/0.68 (E(f14(x991,x991),x991)), % 0.59/0.68 inference(rename_variables,[],[46])). % 0.59/0.68 cnf(100,plain, % 0.59/0.69 (~P1(f14(a13,a13))), % 0.59/0.69 inference(scs_inference,[],[47,46,89,92,96,99,45,24,49,59,2,62,58,68,69,15,60,3,13])). % 0.59/0.69 cnf(101,plain, % 0.59/0.69 (E(f14(x1011,x1011),x1011)), % 0.59/0.69 inference(rename_variables,[],[46])). % 0.59/0.69 cnf(103,plain, % 0.59/0.69 (P2(f7(x1031),x1031)), % 0.59/0.69 inference(rename_variables,[],[47])). % 0.59/0.69 cnf(104,plain, % 0.59/0.69 (P5(a12)), % 0.59/0.69 inference(scs_inference,[],[47,83,46,89,92,96,99,101,45,24,49,27,29,36,59,2,62,58,68,69,15,60,3,13,20,57])). % 0.59/0.69 cnf(106,plain, % 0.59/0.69 (P6(f7(a13),f14(x1061,a13))), % 0.59/0.69 inference(scs_inference,[],[47,83,46,89,92,96,99,101,45,24,49,27,29,36,59,2,62,58,68,69,15,60,3,13,20,57,76])). % 0.59/0.69 cnf(112,plain, % 0.59/0.69 (~P6(a13,f16(a1))), % 0.59/0.69 inference(scs_inference,[],[47,83,46,89,92,96,99,101,45,24,49,27,29,36,59,2,62,58,68,69,15,60,3,13,20,57,76,77,64,75])). % 0.59/0.69 cnf(114,plain, % 0.59/0.69 (~P6(f7(a13),f14(a1,a1))), % 0.59/0.69 inference(scs_inference,[],[47,83,46,89,92,96,99,101,45,24,49,27,29,36,59,2,62,58,68,69,15,60,3,13,20,57,76,77,64,75,78])). % 0.59/0.69 cnf(117,plain, % 0.59/0.69 (P2(x1171,x1172)+~E(f7(x1172),x1171)), % 0.59/0.69 inference(scs_inference,[],[47,83,103,46,89,92,96,99,101,45,24,49,27,29,36,59,2,62,58,68,69,15,60,3,13,20,57,76,77,64,75,78,14,19])). % 0.59/0.69 cnf(125,plain, % 0.59/0.69 (E(x1251,f14(x1251,x1251))), % 0.59/0.69 inference(rename_variables,[],[81])). % 0.59/0.69 cnf(132,plain, % 0.59/0.69 (~P6(x1321,a2)), % 0.59/0.69 inference(scs_inference,[],[106,81,98,25,117,77,75,76,59])). % 0.59/0.69 cnf(134,plain, % 0.59/0.69 (~P6(f14(f16(x1341),a1),f14(x1341,x1341))), % 0.59/0.69 inference(scs_inference,[],[85,106,81,98,25,117,77,75,76,59,64])). % 0.59/0.69 cnf(136,plain, % 0.59/0.69 (E(x1361,f14(x1361,a1))), % 0.59/0.69 inference(scs_inference,[],[85,106,81,98,45,25,117,77,75,76,59,64,2])). % 0.59/0.69 cnf(142,plain, % 0.59/0.69 (P2(f7(x1421),f14(x1421,x1421))), % 0.59/0.69 inference(scs_inference,[],[82,85,106,114,47,81,125,98,45,25,117,77,75,76,59,64,2,78,69,20])). % 0.59/0.69 cnf(144,plain, % 0.59/0.69 (E(a13,f14(f14(a13,a13),a1))), % 0.59/0.69 inference(scs_inference,[],[82,85,106,114,47,81,125,98,45,25,117,77,75,76,59,64,2,78,69,20,3])). % 0.59/0.69 cnf(145,plain, % 0.59/0.69 (E(x1451,f14(x1451,x1451))), % 0.59/0.69 inference(rename_variables,[],[81])). % 0.59/0.69 cnf(146,plain, % 0.59/0.69 (~P2(f14(f16(a13),a1),f14(a13,a13))), % 0.59/0.69 inference(scs_inference,[],[82,85,106,114,47,81,125,100,98,45,25,117,77,75,76,59,64,2,78,69,20,3,62])). % 0.59/0.69 cnf(148,plain, % 0.59/0.69 (~E(f14(f16(a13),a1),a1)), % 0.59/0.69 inference(scs_inference,[],[82,85,106,114,47,81,125,79,100,98,45,25,117,77,75,76,59,64,2,78,69,20,3,62,15])). % 0.59/0.69 cnf(149,plain, % 0.59/0.69 (P6(f14(x1491,x1491),f14(f16(x1491),a1))), % 0.59/0.69 inference(rename_variables,[],[85])). % 0.59/0.69 cnf(150,plain, % 0.59/0.69 (~P6(x1501,a1)), % 0.59/0.69 inference(rename_variables,[],[79])). % 0.59/0.69 cnf(151,plain, % 0.59/0.69 (P6(f14(f7(a13),f7(a13)),a13)), % 0.59/0.69 inference(scs_inference,[],[82,85,106,114,47,81,125,145,79,100,98,45,25,117,77,75,76,59,64,2,78,69,20,3,62,15,14])). % 0.59/0.69 cnf(152,plain, % 0.59/0.69 (E(x1521,f14(x1521,x1521))), % 0.59/0.69 inference(rename_variables,[],[81])). % 0.59/0.69 cnf(153,plain, % 0.59/0.69 (P3(f14(a3,a3))), % 0.59/0.69 inference(scs_inference,[],[82,85,106,114,47,81,125,145,152,79,100,98,45,25,28,117,77,75,76,59,64,2,78,69,20,3,62,15,14,17])). % 0.59/0.69 cnf(154,plain, % 0.59/0.69 (E(x1541,f14(x1541,x1541))), % 0.59/0.69 inference(rename_variables,[],[81])). % 0.59/0.69 cnf(155,plain, % 0.59/0.69 (P1(f14(a1,a1))), % 0.59/0.69 inference(scs_inference,[],[82,85,106,114,47,81,125,145,152,154,79,100,98,45,24,25,28,117,77,75,76,59,64,2,78,69,20,3,62,15,14,17,13])). % 0.59/0.69 cnf(156,plain, % 0.59/0.69 (E(x1561,f14(x1561,x1561))), % 0.59/0.69 inference(rename_variables,[],[81])). % 0.59/0.69 cnf(157,plain, % 0.59/0.69 (P7(f14(a1,a1))), % 0.59/0.69 inference(scs_inference,[],[82,85,106,114,47,81,125,145,152,154,156,79,100,98,45,24,25,28,42,117,77,75,76,59,64,2,78,69,20,3,62,15,14,17,13,21])). % 0.59/0.69 cnf(158,plain, % 0.59/0.69 (E(x1581,f14(x1581,x1581))), % 0.59/0.69 inference(rename_variables,[],[81])). % 0.59/0.69 cnf(159,plain, % 0.59/0.69 (P4(f14(a1,a1))), % 0.59/0.69 inference(scs_inference,[],[82,85,106,114,47,81,125,145,152,154,156,158,79,100,98,45,24,25,28,33,42,117,77,75,76,59,64,2,78,69,20,3,62,15,14,17,13,21,16])). % 0.59/0.69 cnf(160,plain, % 0.59/0.69 (E(x1601,f14(x1601,x1601))), % 0.59/0.69 inference(rename_variables,[],[81])). % 0.59/0.69 cnf(164,plain, % 0.59/0.69 (~P6(x1641,a1)), % 0.59/0.69 inference(rename_variables,[],[79])). % 0.59/0.69 cnf(166,plain, % 0.59/0.69 (P6(f14(x1661,x1661),f16(x1661))), % 0.59/0.69 inference(scs_inference,[],[82,85,149,106,114,47,81,125,145,152,154,156,158,160,79,150,164,48,100,98,104,45,24,25,28,33,42,117,77,75,76,59,64,2,78,69,20,3,62,15,14,17,13,21,16,18,72,70])). % 0.59/0.69 cnf(176,plain, % 0.59/0.69 (P6(f14(x1761,x1761),f14(x1762,f16(x1761)))), % 0.59/0.69 inference(scs_inference,[],[166,76])). % 0.59/0.69 cnf(180,plain, % 0.59/0.69 (~P6(f16(x1801),f14(x1801,x1801))), % 0.59/0.69 inference(scs_inference,[],[166,76,77,64])). % 0.59/0.69 cnf(183,plain, % 0.59/0.69 (E(x1831,f14(x1831,a1))), % 0.59/0.69 inference(rename_variables,[],[136])). % 0.59/0.69 cnf(184,plain, % 0.59/0.69 (~P6(f14(f16(a13),a1),f16(a1))), % 0.59/0.69 inference(scs_inference,[],[166,148,136,76,77,64,117,75])). % 0.59/0.69 cnf(186,plain, % 0.59/0.69 (~P6(x1861,f14(a1,a1))), % 0.59/0.69 inference(scs_inference,[],[166,148,155,136,76,77,64,117,75,59])). % 0.59/0.69 cnf(196,plain, % 0.59/0.69 (P7(f14(f14(a1,a1),a1))), % 0.59/0.69 inference(scs_inference,[],[146,166,148,47,142,155,134,136,183,144,50,157,76,77,64,117,75,59,2,78,62,19,21])). % 0.59/0.69 cnf(197,plain, % 0.59/0.69 (E(x1971,f14(x1971,a1))), % 0.59/0.69 inference(rename_variables,[],[136])). % 0.59/0.69 cnf(199,plain, % 0.59/0.69 (E(x1991,f14(x1991,a1))), % 0.59/0.69 inference(rename_variables,[],[136])). % 0.59/0.69 cnf(201,plain, % 0.59/0.69 (P6(f14(x2011,x2011),f16(x2011))), % 0.59/0.69 inference(rename_variables,[],[166])). % 0.59/0.69 cnf(202,plain, % 0.59/0.69 (~E(f16(x2021),a2)), % 0.59/0.69 inference(scs_inference,[],[146,166,201,148,47,142,155,134,136,183,197,112,132,144,50,104,157,76,77,64,117,75,59,2,78,62,19,21,18,14,15])). % 0.59/0.69 cnf(205,plain, % 0.59/0.69 (E(x2051,f14(x2051,a1))), % 0.59/0.69 inference(rename_variables,[],[136])). % 0.59/0.69 cnf(206,plain, % 0.59/0.69 (P1(f14(f14(a1,a1),a1))), % 0.59/0.69 inference(scs_inference,[],[146,166,201,148,47,142,155,134,136,183,197,199,205,112,132,144,50,104,159,157,76,77,64,117,75,59,2,78,62,19,21,18,14,15,16,13])). % 0.59/0.69 cnf(207,plain, % 0.59/0.69 (E(x2071,f14(x2071,a1))), % 0.59/0.69 inference(rename_variables,[],[136])). % 0.59/0.69 cnf(208,plain, % 0.59/0.69 (P3(f14(f14(a3,a3),a1))), % 0.59/0.69 inference(scs_inference,[],[146,166,201,148,47,142,155,134,136,183,197,199,205,207,112,132,144,50,104,159,157,153,76,77,64,117,75,59,2,78,62,19,21,18,14,15,16,13,17])). % 0.59/0.69 cnf(210,plain, % 0.59/0.69 (P6(f14(f7(a13),f7(a13)),f14(a13,a13))), % 0.59/0.69 inference(scs_inference,[],[146,166,201,148,151,47,142,155,134,136,183,197,199,205,207,112,132,144,50,79,104,159,157,153,76,77,64,117,75,59,2,78,62,19,21,18,14,15,16,13,17,70])). % 0.59/0.69 cnf(215,plain, % 0.59/0.69 (~P1(f16(x2151))), % 0.59/0.69 inference(scs_inference,[],[146,166,201,148,151,47,142,155,134,136,183,197,199,205,207,112,132,144,50,79,104,159,157,153,25,76,77,64,117,75,59,2,78,62,19,21,18,14,15,16,13,17,70,74,56])). % 0.59/0.69 cnf(217,plain, % 0.59/0.69 (~E(f14(a1,a1),f14(f14(a13,a13),a1))), % 0.59/0.69 inference(scs_inference,[],[146,166,201,148,151,47,142,155,134,136,183,197,199,205,207,112,132,144,50,79,104,159,157,153,25,76,77,64,117,75,59,2,78,62,19,21,18,14,15,16,13,17,70,74,56,3])). % 0.59/0.69 cnf(236,plain, % 0.59/0.69 (E(f14(x2361,x2361),x2361)), % 0.59/0.69 inference(rename_variables,[],[46])). % 0.59/0.69 cnf(237,plain, % 0.59/0.69 (~P6(f16(x2371),f14(x2371,x2371))), % 0.59/0.69 inference(rename_variables,[],[180])). % 0.59/0.69 cnf(247,plain, % 0.59/0.69 (E(f14(x2471,x2472),f14(x2472,x2471))), % 0.59/0.69 inference(rename_variables,[],[48])). % 0.59/0.69 cnf(252,plain, % 0.59/0.69 ($false), % 0.59/0.69 inference(scs_inference,[],[51,176,210,202,46,236,48,247,155,180,237,215,186,206,217,184,196,208,4,77,76,64,59,75,58,78,56,62,21,17,15,14]), % 0.59/0.69 ['proof']). % 0.59/0.69 % SZS output end Proof % 0.59/0.69 % Total time :0.070000s %------------------------------------------------------------------------------