%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU223+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 : n001.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:52 EDT 2024 % Result : Theorem 2.36s 2.45s % Output : CNFRefutation 2.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU223+1 : TPTP v8.2.0. Released v3.3.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n001.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 13:17:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.46/0.57 start to proof:theBenchmark % 2.36/2.43 %------------------------------------------- % 2.36/2.43 % File :CSE---1.7 % 2.36/2.43 % Problem :theBenchmark % 2.36/2.43 % Transform :cnf % 2.36/2.43 % Format :tptp:raw % 2.36/2.43 % Command :java -jar mcs_scs.jar %d %s % 2.36/2.43 % 2.36/2.43 % Result :Theorem 1.830000s % 2.36/2.43 % Output :CNFRefutation 1.830000s % 2.36/2.43 %------------------------------------------- % 2.36/2.44 %------------------------------------------------------------------------------ % 2.36/2.44 % File : SEU223+1 : TPTP v8.2.0. Released v3.3.0. % 2.36/2.44 % Domain : Set theory % 2.36/2.44 % Problem : MPTP bushy problem t70_funct_1 % 2.36/2.44 % Version : [Urb07] axioms : Especial. % 2.36/2.44 % English : % 2.36/2.44 % 2.36/2.44 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 2.36/2.44 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 2.36/2.44 % Source : [Urb07] % 2.36/2.44 % Names : bushy-t70_funct_1 [Urb07] % 2.36/2.44 % 2.36/2.44 % Status : Theorem % 2.36/2.44 % Rating : 0.17 v8.2.0, 0.14 v7.5.0, 0.16 v7.4.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.12 v6.2.0, 0.20 v6.1.0, 0.30 v5.4.0, 0.32 v5.3.0, 0.37 v5.2.0, 0.10 v5.0.0, 0.21 v4.1.0, 0.22 v4.0.0, 0.25 v3.7.0, 0.15 v3.5.0, 0.16 v3.4.0, 0.21 v3.3.0 % 2.36/2.44 % Syntax : Number of formulae : 37 ( 12 unt; 0 def) % 2.36/2.44 % Number of atoms : 86 ( 9 equ) % 2.36/2.44 % Maximal formula atoms : 8 ( 2 avg) % 2.36/2.44 % Number of connectives : 57 ( 8 ~; 1 |; 29 &) % 2.36/2.44 % ( 1 <=>; 18 =>; 0 <=; 0 <~>) % 2.36/2.44 % Maximal formula depth : 10 ( 4 avg) % 2.36/2.44 % Maximal term depth : 3 ( 1 avg) % 2.36/2.44 % Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty) % 2.36/2.44 % Number of functors : 5 ( 5 usr; 1 con; 0-2 aty) % 2.36/2.44 % Number of variables : 46 ( 37 !; 9 ?) % 2.36/2.44 % SPC : FOF_THM_RFO_SEQ % 2.36/2.44 % 2.36/2.44 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 2.36/2.44 % library, www.mizar.org % 2.36/2.44 %------------------------------------------------------------------------------ % 2.36/2.44 fof(rc3_relat_1,axiom, % 2.36/2.44 ? [A] : % 2.36/2.44 ( relation(A) % 2.36/2.44 & relation_empty_yielding(A) ) ). % 2.36/2.44 % 2.36/2.44 fof(fc13_relat_1,axiom, % 2.36/2.44 ! [A,B] : % 2.36/2.44 ( ( relation(A) % 2.36/2.44 & relation_empty_yielding(A) ) % 2.36/2.44 => ( relation(relation_dom_restriction(A,B)) % 2.36/2.44 & relation_empty_yielding(relation_dom_restriction(A,B)) ) ) ). % 2.36/2.44 % 2.36/2.44 fof(dt_k1_xboole_0,axiom, % 2.36/2.44 $true ). % 2.36/2.44 % 2.36/2.44 fof(rc3_funct_1,axiom, % 2.36/2.44 ? [A] : % 2.36/2.44 ( relation(A) % 2.36/2.44 & function(A) % 2.36/2.44 & one_to_one(A) ) ). % 2.36/2.44 % 2.36/2.44 fof(fc4_relat_1,axiom, % 2.36/2.44 ( empty(empty_set) % 2.36/2.44 & relation(empty_set) ) ). % 2.36/2.44 % 2.36/2.44 fof(fc12_relat_1,axiom, % 2.36/2.44 ( empty(empty_set) % 2.36/2.44 & relation(empty_set) % 2.36/2.44 & relation_empty_yielding(empty_set) ) ). % 2.36/2.44 % 2.36/2.44 fof(fc1_xboole_0,axiom, % 2.36/2.44 empty(empty_set) ). % 2.36/2.44 % 2.36/2.44 fof(t2_boole,axiom, % 2.36/2.44 ! [A] : set_intersection2(A,empty_set) = empty_set ). % 2.36/2.44 % 2.36/2.44 fof(existence_m1_subset_1,axiom, % 2.36/2.44 ! [A] : % 2.36/2.44 ? [B] : element(B,A) ). % 2.36/2.44 % 2.36/2.44 fof(dt_m1_subset_1,axiom, % 2.36/2.44 $true ). % 2.36/2.44 % 2.36/2.44 fof(cc1_funct_1,axiom, % 2.36/2.44 ! [A] : % 2.36/2.44 ( empty(A) % 2.36/2.44 => function(A) ) ). % 2.36/2.44 % 2.36/2.44 fof(rc2_funct_1,axiom, % 2.36/2.44 ? [A] : % 2.36/2.44 ( relation(A) % 2.36/2.44 & empty(A) % 2.36/2.44 & function(A) ) ). % 2.36/2.44 % 2.36/2.44 fof(cc2_funct_1,axiom, % 2.36/2.44 ! [A] : % 2.36/2.44 ( ( relation(A) % 2.36/2.44 & empty(A) % 2.36/2.44 & function(A) ) % 2.36/2.44 => ( relation(A) % 2.36/2.44 & function(A) % 2.36/2.44 & one_to_one(A) ) ) ). % 2.36/2.44 % 2.36/2.44 fof(rc1_relat_1,axiom, % 2.36/2.44 ? [A] : % 2.36/2.44 ( empty(A) % 2.36/2.44 & relation(A) ) ). % 2.36/2.44 % 2.36/2.44 fof(cc1_relat_1,axiom, % 2.36/2.44 ! [A] : % 2.36/2.44 ( empty(A) % 2.36/2.44 => relation(A) ) ). % 2.36/2.44 % 2.36/2.44 fof(rc2_relat_1,axiom, % 2.36/2.44 ? [A] : % 2.36/2.44 ( ~ empty(A) % 2.36/2.44 & relation(A) ) ). % 2.36/2.44 % 2.36/2.44 fof(fc5_relat_1,axiom, % 2.36/2.44 ! [A] : % 2.36/2.44 ( ( ~ empty(A) % 2.36/2.44 & relation(A) ) % 2.36/2.44 => ~ empty(relation_dom(A)) ) ). % 2.36/2.44 % 2.36/2.44 fof(fc7_relat_1,axiom, % 2.36/2.44 ! [A] : % 2.36/2.44 ( empty(A) % 2.36/2.44 => ( empty(relation_dom(A)) % 2.36/2.44 & relation(relation_dom(A)) ) ) ). % 2.36/2.44 % 2.36/2.44 fof(rc1_xboole_0,axiom, % 2.36/2.44 ? [A] : empty(A) ). % 2.36/2.44 % 2.36/2.44 fof(rc2_xboole_0,axiom, % 2.36/2.44 ? [A] : ~ empty(A) ). % 2.36/2.44 % 2.36/2.44 fof(t2_subset,axiom, % 2.36/2.44 ! [A,B] : % 2.36/2.44 ( element(A,B) % 2.36/2.44 => ( empty(B) % 2.36/2.44 | in(A,B) ) ) ). % 2.36/2.44 % 2.36/2.44 fof(t6_boole,axiom, % 2.36/2.44 ! [A] : % 2.36/2.44 ( empty(A) % 2.36/2.44 => A = empty_set ) ). % 2.36/2.44 % 2.36/2.44 fof(t8_boole,axiom, % 2.36/2.44 ! [A,B] : % 2.36/2.44 ~ ( empty(A) % 2.36/2.44 & A != B % 2.36/2.44 & empty(B) ) ). % 2.36/2.44 % 2.36/2.44 fof(commutativity_k3_xboole_0,axiom, % 2.36/2.44 ! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) ). % 2.36/2.44 % 2.36/2.44 fof(idempotence_k3_xboole_0,axiom, % 2.36/2.44 ! [A,B] : set_intersection2(A,A) = A ). % 2.36/2.44 % 2.36/2.44 fof(antisymmetry_r2_hidden,axiom, % 2.36/2.44 ! [A,B] : % 2.36/2.44 ( in(A,B) % 2.36/2.44 => ~ in(B,A) ) ). % 2.36/2.44 % 2.36/2.44 fof(dt_k1_funct_1,axiom, % 2.36/2.44 $true ). % 2.36/2.44 % 2.36/2.44 fof(dt_k1_relat_1,axiom, % 2.36/2.44 $true ). % 2.36/2.44 % 2.36/2.44 fof(dt_k3_xboole_0,axiom, % 2.36/2.44 $true ). % 2.36/2.44 % 2.36/2.44 fof(dt_k7_relat_1,axiom, % 2.36/2.44 ! [A,B] : % 2.36/2.44 ( relation(A) % 2.36/2.44 => relation(relation_dom_restriction(A,B)) ) ). % 2.36/2.44 % 2.36/2.44 fof(rc1_funct_1,axiom, % 2.36/2.44 ? [A] : % 2.36/2.44 ( relation(A) % 2.36/2.44 & function(A) ) ). % 2.36/2.44 % 2.36/2.44 fof(fc4_funct_1,axiom, % 2.36/2.44 ! [A,B] : % 2.36/2.44 ( ( relation(A) % 2.36/2.44 & function(A) ) % 2.36/2.44 => ( relation(relation_dom_restriction(A,B)) % 2.36/2.44 & function(relation_dom_restriction(A,B)) ) ) ). % 2.36/2.44 % 2.36/2.44 fof(fc1_relat_1,axiom, % 2.36/2.44 ! [A,B] : % 2.36/2.44 ( ( relation(A) % 2.36/2.44 & relation(B) ) % 2.36/2.44 => relation(set_intersection2(A,B)) ) ). % 2.36/2.45 % 2.36/2.45 fof(t1_subset,axiom, % 2.36/2.45 ! [A,B] : % 2.36/2.45 ( in(A,B) % 2.36/2.45 => element(A,B) ) ). % 2.36/2.45 % 2.36/2.45 fof(t7_boole,axiom, % 2.36/2.45 ! [A,B] : % 2.36/2.45 ~ ( in(A,B) % 2.36/2.45 & empty(B) ) ). % 2.36/2.45 % 2.36/2.45 fof(t70_funct_1,conjecture, % 2.36/2.45 ! [A,B,C] : % 2.36/2.45 ( ( relation(C) % 2.36/2.45 & function(C) ) % 2.36/2.45 => ( in(B,relation_dom(relation_dom_restriction(C,A))) % 2.36/2.45 => apply(relation_dom_restriction(C,A),B) = apply(C,B) ) ) ). % 2.36/2.45 % 2.36/2.45 fof(t68_funct_1,axiom, % 2.36/2.45 ! [A,B] : % 2.36/2.45 ( ( relation(B) % 2.36/2.45 & function(B) ) % 2.36/2.45 => ! [C] : % 2.36/2.45 ( ( relation(C) % 2.36/2.45 & function(C) ) % 2.36/2.45 => ( B = relation_dom_restriction(C,A) % 2.36/2.45 <=> ( relation_dom(B) = set_intersection2(relation_dom(C),A) % 2.36/2.45 & ! [D] : % 2.36/2.45 ( in(D,relation_dom(B)) % 2.36/2.45 => apply(B,D) = apply(C,D) ) ) ) ) ) ). % 2.36/2.45 % 2.36/2.45 %------------------------------------------------------------------------------ % 2.36/2.45 %------------------------------------------- % 2.36/2.45 % Proof found % 2.36/2.45 % SZS status Theorem for theBenchmark % 2.36/2.45 % SZS output start Proof % 2.36/2.45 %ClaNum:75(EqnAxiom:23) % 2.36/2.45 %VarNum:117(SingletonVarNum:43) % 2.36/2.45 %MaxLitNum:7 % 2.36/2.45 %MaxfuncDepth:2 % 2.36/2.45 %SharedTerms:39 % 2.36/2.45 %goalClause: 32 38 50 53 % 2.36/2.45 %singleGoalClaCount:4 % 2.36/2.45 [25]P1(a1) % 2.36/2.45 [26]P1(a3) % 2.36/2.45 [27]P1(a8) % 2.36/2.45 [28]P1(a9) % 2.36/2.45 [29]P1(a11) % 2.36/2.45 [30]P1(a12) % 2.36/2.45 [31]P1(a13) % 2.36/2.45 [32]P1(a4) % 2.36/2.45 [33]P7(a1) % 2.36/2.45 [34]P7(a3) % 2.36/2.45 [35]P2(a8) % 2.36/2.45 [36]P2(a9) % 2.36/2.45 [37]P2(a13) % 2.36/2.45 [38]P2(a4) % 2.36/2.45 [39]P5(a8) % 2.36/2.45 [42]P3(a1) % 2.36/2.45 [43]P3(a9) % 2.36/2.45 [44]P3(a11) % 2.36/2.45 [45]P3(a14) % 2.36/2.45 [51]~P3(a12) % 2.36/2.45 [52]~P3(a15) % 2.36/2.45 [50]P6(a5,f18(f17(a4,a6))) % 2.36/2.45 [53]~E(f2(f17(a4,a6),a5),f2(a4,a5)) % 2.36/2.45 [46]E(f16(x461,a1),a1) % 2.36/2.45 [47]E(f16(x471,x471),x471) % 2.36/2.45 [48]P4(f10(x481),x481) % 2.36/2.45 [49]E(f16(x491,x492),f16(x492,x491)) % 2.36/2.45 [54]~P3(x541)+E(x541,a1) % 2.36/2.45 [55]~P3(x551)+P1(x551) % 2.36/2.45 [56]~P3(x561)+P2(x561) % 2.36/2.45 [58]~P3(x581)+P1(f18(x581)) % 2.36/2.45 [59]~P3(x591)+P3(f18(x591)) % 2.36/2.45 [62]~P3(x621)+~P6(x622,x621) % 2.36/2.45 [63]~P6(x631,x632)+P4(x631,x632) % 2.36/2.45 [71]~P6(x712,x711)+~P6(x711,x712) % 2.36/2.45 [64]~P1(x641)+P1(f17(x641,x642)) % 2.36/2.45 [61]~P1(x611)+P3(x611)+~P3(f18(x611)) % 2.36/2.45 [57]~P3(x572)+~P3(x571)+E(x571,x572) % 2.36/2.45 [65]~P4(x652,x651)+P3(x651)+P6(x652,x651) % 2.36/2.45 [68]~P1(x682)+~P1(x681)+P1(f16(x681,x682)) % 2.36/2.45 [69]~P1(x691)+~P7(x691)+P7(f17(x691,x692)) % 2.36/2.45 [70]~P1(x701)+~P2(x701)+P2(f17(x701,x702)) % 2.36/2.45 [60]~P1(x601)+~P2(x601)+~P3(x601)+P5(x601) % 2.36/2.45 [72]~P1(x722)+~P1(x721)+~P2(x722)+~P2(x721)+~E(x721,f17(x722,x723))+E(f18(x721),f16(f18(x722),x723)) % 2.36/2.45 [74]~P1(x742)+~P1(x741)+~P2(x742)+~P2(x741)+P6(f7(x743,x741,x742),f18(x741))+E(x741,f17(x742,x743))+~E(f18(x741),f16(f18(x742),x743)) % 2.36/2.45 [75]~P1(x752)+~P1(x751)+~P2(x752)+~P2(x751)+E(x751,f17(x752,x753))+~E(f18(x751),f16(f18(x752),x753))+~E(f2(x751,f7(x753,x751,x752)),f2(x752,f7(x753,x751,x752))) % 2.36/2.45 [73]~P1(x733)+~P1(x731)+~P2(x733)+~P2(x731)+~P6(x732,f18(x731))+E(f2(x731,x732),f2(x733,x732))+~E(x731,f17(x733,x734)) % 2.36/2.45 %EqnAxiom % 2.36/2.45 [1]E(x11,x11) % 2.36/2.45 [2]E(x22,x21)+~E(x21,x22) % 2.36/2.45 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 2.36/2.45 [4]~E(x41,x42)+E(f16(x41,x43),f16(x42,x43)) % 2.36/2.45 [5]~E(x51,x52)+E(f16(x53,x51),f16(x53,x52)) % 2.36/2.45 [6]~E(x61,x62)+E(f2(x61,x63),f2(x62,x63)) % 2.36/2.45 [7]~E(x71,x72)+E(f2(x73,x71),f2(x73,x72)) % 2.36/2.45 [8]~E(x81,x82)+E(f10(x81),f10(x82)) % 2.36/2.45 [9]~E(x91,x92)+E(f7(x91,x93,x94),f7(x92,x93,x94)) % 2.36/2.45 [10]~E(x101,x102)+E(f7(x103,x101,x104),f7(x103,x102,x104)) % 2.36/2.45 [11]~E(x111,x112)+E(f7(x113,x114,x111),f7(x113,x114,x112)) % 2.36/2.45 [12]~E(x121,x122)+E(f17(x121,x123),f17(x122,x123)) % 2.36/2.45 [13]~E(x131,x132)+E(f17(x133,x131),f17(x133,x132)) % 2.36/2.45 [14]~E(x141,x142)+E(f18(x141),f18(x142)) % 2.36/2.45 [15]~P1(x151)+P1(x152)+~E(x151,x152) % 2.36/2.45 [16]~P2(x161)+P2(x162)+~E(x161,x162) % 2.36/2.45 [17]~P7(x171)+P7(x172)+~E(x171,x172) % 2.36/2.45 [18]~P3(x181)+P3(x182)+~E(x181,x182) % 2.36/2.45 [19]P6(x192,x193)+~E(x191,x192)+~P6(x191,x193) % 2.36/2.45 [20]P6(x203,x202)+~E(x201,x202)+~P6(x203,x201) % 2.36/2.45 [21]P4(x212,x213)+~E(x211,x212)+~P4(x211,x213) % 2.36/2.45 [22]P4(x223,x222)+~E(x221,x222)+~P4(x223,x221) % 2.36/2.45 [23]~P5(x231)+P5(x232)+~E(x231,x232) % 2.36/2.45 % 2.36/2.45 %------------------------------------------- % 2.36/2.45 cnf(76,plain, % 2.36/2.45 (~P2(x761)+~P2(f17(x761,x762))+~P1(x761)+~P1(f17(x761,x762))+E(f18(f17(x761,x762)),f16(f18(x761),x762))), % 2.36/2.45 inference(equality_inference,[],[72])). % 2.36/2.45 cnf(77,plain, % 2.36/2.45 (~P2(x771)+~P2(f17(x771,x772))+~P1(x771)+~P1(f17(x771,x772))+E(f2(f17(x771,x772),x773),f2(x771,x773))+~P6(x773,f18(f17(x771,x772)))), % 2.36/2.45 inference(equality_inference,[],[73])). % 2.36/2.45 cnf(78,plain, % 2.36/2.45 (~P6(x781,a1)), % 2.36/2.45 inference(scs_inference,[],[42,62])). % 2.36/2.45 cnf(82,plain, % 2.36/2.45 (E(x821,f16(x821,x821))), % 2.36/2.45 inference(scs_inference,[],[50,42,47,62,71,2])). % 2.36/2.45 cnf(85,plain, % 2.36/2.45 (E(f16(x851,x851),x851)), % 2.36/2.45 inference(rename_variables,[],[47])). % 2.36/2.45 cnf(86,plain, % 2.36/2.45 (~E(f18(f17(a4,a6)),a1)), % 2.36/2.45 inference(scs_inference,[],[53,50,42,47,62,71,2,6,3,20])). % 2.36/2.45 cnf(87,plain, % 2.36/2.45 (P6(f10(a12),a12)), % 2.36/2.45 inference(scs_inference,[],[53,50,42,51,47,48,62,71,2,6,3,20,65])). % 2.36/2.45 cnf(88,plain, % 2.36/2.45 (P4(f10(x881),x881)), % 2.36/2.45 inference(rename_variables,[],[48])). % 2.36/2.45 cnf(90,plain, % 2.36/2.45 (~P3(f16(a12,a12))), % 2.36/2.45 inference(scs_inference,[],[53,50,42,51,47,85,48,62,71,2,6,3,20,65,18])). % 2.36/2.45 cnf(91,plain, % 2.36/2.45 (E(f16(x911,x911),x911)), % 2.36/2.45 inference(rename_variables,[],[47])). % 2.36/2.45 cnf(92,plain, % 2.36/2.45 (P4(f10(f16(x921,x921)),x921)), % 2.36/2.45 inference(scs_inference,[],[53,50,42,51,47,85,91,48,88,62,71,2,6,3,20,65,18,22])). % 2.36/2.45 cnf(94,plain, % 2.36/2.45 (P5(a9)), % 2.36/2.45 inference(scs_inference,[],[53,50,28,36,42,43,51,47,85,91,48,88,62,71,2,6,3,20,65,18,22,60])). % 2.36/2.45 cnf(98,plain, % 2.36/2.45 (~P3(f17(a4,a6))), % 2.36/2.45 inference(scs_inference,[],[53,50,28,36,42,43,51,47,85,91,48,88,62,71,2,6,3,20,65,18,22,60,54,59])). % 2.36/2.45 cnf(102,plain, % 2.36/2.45 (~P1(f16(x1021,x1021))+P1(x1021)), % 2.36/2.45 inference(scs_inference,[],[53,50,28,36,42,43,51,47,85,91,48,88,62,71,2,6,3,20,65,18,22,60,54,59,57,15])). % 2.36/2.45 cnf(103,plain, % 2.36/2.45 (~P2(f16(x1031,x1031))+P2(x1031)), % 2.36/2.45 inference(scs_inference,[],[53,50,28,36,42,43,51,47,85,91,48,88,62,71,2,6,3,20,65,18,22,60,54,59,57,15,16])). % 2.36/2.45 cnf(104,plain, % 2.36/2.45 (P6(x1041,f18(f17(a4,a6)))+~E(a5,x1041)), % 2.36/2.45 inference(scs_inference,[],[53,50,28,36,42,43,51,47,85,91,48,88,62,71,2,6,3,20,65,18,22,60,54,59,57,15,16,19])). % 2.36/2.45 cnf(108,plain, % 2.36/2.45 (P6(f16(a5,a5),f18(f17(a4,a6)))), % 2.36/2.45 inference(scs_inference,[],[82,104])). % 2.36/2.45 cnf(109,plain, % 2.36/2.45 (E(x1091,f16(x1091,x1091))), % 2.36/2.45 inference(rename_variables,[],[82])). % 2.36/2.45 cnf(110,plain, % 2.36/2.45 (~P6(x1101,a11)), % 2.36/2.45 inference(scs_inference,[],[82,44,104,62])). % 2.36/2.45 cnf(114,plain, % 2.36/2.45 (E(a1,f16(x1141,a1))), % 2.36/2.45 inference(scs_inference,[],[82,87,44,46,104,62,71,2])). % 2.36/2.45 cnf(115,plain, % 2.36/2.45 (P4(f16(f10(x1151),f10(x1151)),x1151)), % 2.36/2.45 inference(scs_inference,[],[82,109,87,44,46,48,104,62,71,2,21])). % 2.36/2.45 cnf(116,plain, % 2.36/2.45 (E(x1161,f16(x1161,x1161))), % 2.36/2.45 inference(rename_variables,[],[82])). % 2.36/2.45 cnf(120,plain, % 2.36/2.45 (P2(f16(a4,a4))), % 2.36/2.45 inference(scs_inference,[],[38,82,109,116,98,87,44,92,46,48,104,62,71,2,21,65,16])). % 2.36/2.45 cnf(121,plain, % 2.36/2.45 (E(x1211,f16(x1211,x1211))), % 2.36/2.45 inference(rename_variables,[],[82])). % 2.36/2.45 cnf(124,plain, % 2.36/2.45 (~E(f18(f17(a4,a6)),f16(x1241,a1))), % 2.36/2.45 inference(scs_inference,[],[38,82,109,116,78,86,98,87,44,92,46,48,104,62,71,2,21,65,16,20,3])). % 2.36/2.45 cnf(125,plain, % 2.36/2.45 (P3(f16(a11,a11))), % 2.36/2.45 inference(scs_inference,[],[38,82,109,116,121,78,86,98,87,44,92,46,48,104,62,71,2,21,65,16,20,3,18])). % 2.36/2.45 cnf(126,plain, % 2.36/2.45 (E(x1261,f16(x1261,x1261))), % 2.36/2.45 inference(rename_variables,[],[82])). % 2.36/2.45 cnf(128,plain, % 2.36/2.45 (E(x1281,f16(x1281,x1281))), % 2.36/2.45 inference(rename_variables,[],[82])). % 2.36/2.45 cnf(129,plain, % 2.36/2.45 (P6(f16(f10(a12),f10(a12)),a12)), % 2.36/2.45 inference(scs_inference,[],[38,82,109,116,121,126,128,78,86,98,87,33,44,92,46,48,104,62,71,2,21,65,16,20,3,18,17,19])). % 2.36/2.45 cnf(130,plain, % 2.36/2.45 (E(x1301,f16(x1301,x1301))), % 2.36/2.45 inference(rename_variables,[],[82])). % 2.36/2.45 cnf(132,plain, % 2.36/2.45 (E(x1321,f16(x1321,x1321))), % 2.36/2.45 inference(rename_variables,[],[82])). % 2.36/2.45 cnf(133,plain, % 2.36/2.45 (P4(f10(x1331),f16(x1331,x1331))), % 2.36/2.45 inference(scs_inference,[],[38,82,109,116,121,126,128,130,132,78,86,94,98,87,33,44,92,46,48,104,62,71,2,21,65,16,20,3,18,17,19,23,22])). % 2.36/2.45 cnf(135,plain, % 2.36/2.45 (P1(f16(a4,a4))), % 2.36/2.45 inference(scs_inference,[],[32,38,82,109,116,121,126,128,130,132,78,86,94,98,87,33,44,92,46,48,104,62,71,2,21,65,16,20,3,18,17,19,23,22,15])). % 2.36/2.45 cnf(144,plain, % 2.36/2.45 (~P6(x1441,f16(a11,a11))), % 2.36/2.45 inference(scs_inference,[],[108,125,71,62])). % 2.36/2.45 cnf(146,plain, % 2.36/2.45 (P6(f10(a12),f16(a12,a12))), % 2.36/2.45 inference(scs_inference,[],[108,90,125,133,71,62,65])). % 2.36/2.45 cnf(147,plain, % 2.36/2.45 (P4(f10(x1471),f16(x1471,x1471))), % 2.36/2.45 inference(rename_variables,[],[133])). % 2.36/2.45 cnf(150,plain, % 2.36/2.45 (E(x1501,f16(x1501,x1501))), % 2.36/2.45 inference(rename_variables,[],[82])). % 2.36/2.45 cnf(151,plain, % 2.36/2.45 (P3(f16(x1511,a1))), % 2.36/2.45 inference(scs_inference,[],[108,114,82,90,125,42,133,147,71,62,65,21,18])). % 2.36/2.45 cnf(154,plain, % 2.36/2.45 (P6(f16(f16(a5,a5),f16(a5,a5)),f18(f17(a4,a6)))), % 2.36/2.45 inference(scs_inference,[],[50,108,110,114,82,150,90,125,42,133,147,71,62,65,21,18,20,19])). % 2.36/2.45 cnf(155,plain, % 2.36/2.45 (E(x1551,f16(x1551,x1551))), % 2.36/2.45 inference(rename_variables,[],[82])). % 2.36/2.45 cnf(159,plain, % 2.36/2.45 (P7(f16(x1591,a1))), % 2.36/2.45 inference(scs_inference,[],[50,108,124,110,114,25,82,150,90,125,33,42,133,147,49,71,62,65,21,18,20,19,15,3,17])). % 2.36/2.45 cnf(160,plain, % 2.36/2.45 (P4(f10(x1601),f16(f16(x1601,x1601),f16(x1601,x1601)))), % 2.36/2.45 inference(scs_inference,[],[50,108,124,110,114,25,82,150,155,90,125,33,42,133,147,49,71,62,65,21,18,20,19,15,3,17,22])). % 2.36/2.45 cnf(168,plain, % 2.36/2.45 (~P6(x1681,f16(x1682,a1))), % 2.36/2.45 inference(scs_inference,[],[154,151,71,62])). % 2.36/2.45 cnf(174,plain, % 2.36/2.45 (E(x1741,f16(x1741,x1741))), % 2.36/2.45 inference(rename_variables,[],[82])). % 2.36/2.45 cnf(175,plain, % 2.36/2.45 (P3(f16(f16(x1751,a1),f16(x1751,a1)))), % 2.36/2.45 inference(scs_inference,[],[154,82,174,151,52,160,115,71,62,65,21,18])). % 2.36/2.45 cnf(176,plain, % 2.36/2.45 (E(x1761,f16(x1761,x1761))), % 2.36/2.45 inference(rename_variables,[],[82])). % 2.36/2.45 cnf(180,plain, % 2.36/2.45 (E(x1801,f16(x1801,x1801))), % 2.36/2.45 inference(rename_variables,[],[82])). % 2.36/2.45 cnf(181,plain, % 2.36/2.45 (P6(f16(f10(a12),f10(a12)),f16(a12,a12))), % 2.36/2.45 inference(scs_inference,[],[50,154,144,82,174,176,180,151,159,146,52,160,115,71,62,65,21,18,20,17,19])). % 2.36/2.45 cnf(192,plain, % 2.36/2.45 (~P6(x1921,f16(f16(x1922,a1),f16(x1922,a1)))), % 2.36/2.45 inference(scs_inference,[],[181,175,71,62])). % 2.36/2.45 cnf(197,plain, % 2.36/2.45 (~E(f16(a12,a12),f16(x1971,a1))), % 2.36/2.45 inference(scs_inference,[],[168,181,175,52,92,71,62,65,20])). % 2.36/2.45 cnf(207,plain, % 2.36/2.45 (~P6(x2071,a14)), % 2.36/2.45 inference(scs_inference,[],[129,45,71,62])). % 2.36/2.45 cnf(210,plain, % 2.36/2.45 (P4(f10(x2101),x2101)), % 2.36/2.45 inference(rename_variables,[],[48])). % 2.36/2.45 cnf(212,plain, % 2.36/2.45 (P3(f16(a14,a14))), % 2.36/2.45 inference(scs_inference,[],[129,82,45,98,48,71,62,65,18])). % 2.36/2.45 cnf(216,plain, % 2.36/2.45 (P4(f10(a1),f16(x2161,a1))), % 2.36/2.45 inference(scs_inference,[],[50,114,192,129,82,45,98,48,210,71,62,65,18,20,22])). % 2.36/2.45 cnf(232,plain, % 2.36/2.45 (E(x2321,f16(x2321,x2321))), % 2.36/2.45 inference(rename_variables,[],[82])). % 2.36/2.45 cnf(239,plain, % 2.36/2.45 (~P2(f17(a4,a6))+~P1(f17(a4,a6))), % 2.36/2.45 inference(scs_inference,[],[32,53,50,38,114,197,135,207,120,82,232,146,212,52,48,216,71,62,65,3,18,20,22,60,76,77])). % 2.36/2.45 cnf(670,plain, % 2.36/2.45 (P1(f17(a4,x6701))), % 2.36/2.45 inference(scs_inference,[],[135,102,64])). % 2.36/2.45 cnf(671,plain, % 2.36/2.45 (~P2(f17(a4,a6))), % 2.36/2.45 inference(scs_inference,[],[670,239])). % 2.36/2.45 cnf(676,plain, % 2.36/2.45 ($false), % 2.36/2.45 inference(scs_inference,[],[38,32,671,103,70]), % 2.36/2.45 ['proof']). % 2.36/2.45 % SZS output end Proof % 2.36/2.45 % Total time :1.830000s %------------------------------------------------------------------------------