%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU188+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 : n026.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 15:01:38 EDT 2024 % Result : Theorem 1.51s 1.56s % Output : CNFRefutation 1.51s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : SEU188+1 : TPTP v8.2.0. Released v3.3.0. % 0.04/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n026.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Fri Jun 21 11:58:53 EDT 2024 % 0.13/0.34 % CPUTime : % 0.57/0.59 start to proof:theBenchmark % 1.51/1.54 %------------------------------------------- % 1.51/1.54 % File :CSE---1.7 % 1.51/1.54 % Problem :theBenchmark % 1.51/1.54 % Transform :cnf % 1.51/1.54 % Format :tptp:raw % 1.51/1.54 % Command :java -jar mcs_scs.jar %d %s % 1.51/1.54 % 1.51/1.54 % Result :Theorem 0.910000s % 1.51/1.54 % Output :CNFRefutation 0.910000s % 1.51/1.54 %------------------------------------------- % 1.51/1.55 %------------------------------------------------------------------------------ % 1.51/1.55 % File : SEU188+1 : TPTP v8.2.0. Released v3.3.0. % 1.51/1.55 % Domain : Set theory % 1.51/1.55 % Problem : MPTP bushy problem t64_relat_1 % 1.51/1.55 % Version : [Urb07] axioms : Especial. % 1.51/1.55 % English : % 1.51/1.55 % 1.51/1.55 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 1.51/1.55 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 1.51/1.55 % Source : [Urb07] % 1.51/1.55 % Names : bushy-t64_relat_1 [Urb07] % 1.51/1.55 % 1.51/1.55 % Status : Theorem % 1.51/1.55 % Rating : 0.17 v8.1.0, 0.14 v7.5.0, 0.16 v7.4.0, 0.07 v7.2.0, 0.03 v7.1.0, 0.04 v7.0.0, 0.03 v6.4.0, 0.08 v6.2.0, 0.16 v6.1.0, 0.23 v6.0.0, 0.13 v5.5.0, 0.15 v5.4.0, 0.18 v5.3.0, 0.19 v5.2.0, 0.00 v5.1.0, 0.05 v5.0.0, 0.12 v4.1.0, 0.13 v4.0.1, 0.17 v4.0.0, 0.21 v3.7.0, 0.15 v3.5.0, 0.16 v3.4.0, 0.21 v3.3.0 % 1.51/1.55 % Syntax : Number of formulae : 34 ( 16 unt; 0 def) % 1.51/1.55 % Number of atoms : 65 ( 10 equ) % 1.51/1.55 % Maximal formula atoms : 4 ( 1 avg) % 1.51/1.55 % Number of connectives : 45 ( 14 ~; 2 |; 10 &) % 1.51/1.55 % ( 4 <=>; 15 =>; 0 <=; 0 <~>) % 1.51/1.55 % Maximal formula depth : 8 ( 4 avg) % 1.51/1.55 % Maximal term depth : 3 ( 1 avg) % 1.51/1.55 % Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty) % 1.51/1.55 % Number of functors : 6 ( 6 usr; 1 con; 0-2 aty) % 1.51/1.55 % Number of variables : 43 ( 36 !; 7 ?) % 1.51/1.55 % SPC : FOF_THM_RFO_SEQ % 1.51/1.55 % 1.51/1.55 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 1.51/1.55 % library, www.mizar.org % 1.51/1.55 %------------------------------------------------------------------------------ % 1.51/1.55 fof(antisymmetry_r2_hidden,axiom, % 1.51/1.55 ! [A,B] : % 1.51/1.55 ( in(A,B) % 1.51/1.55 => ~ in(B,A) ) ). % 1.51/1.55 % 1.51/1.55 fof(cc1_relat_1,axiom, % 1.51/1.55 ! [A] : % 1.51/1.55 ( empty(A) % 1.51/1.55 => relation(A) ) ). % 1.51/1.55 % 1.51/1.55 fof(commutativity_k2_tarski,axiom, % 1.51/1.55 ! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) ). % 1.51/1.55 % 1.51/1.55 fof(d4_relat_1,axiom, % 1.51/1.55 ! [A] : % 1.51/1.55 ( relation(A) % 1.51/1.55 => ! [B] : % 1.51/1.55 ( B = relation_dom(A) % 1.51/1.55 <=> ! [C] : % 1.51/1.55 ( in(C,B) % 1.51/1.55 <=> ? [D] : in(ordered_pair(C,D),A) ) ) ) ). % 1.51/1.55 % 1.51/1.55 fof(d5_relat_1,axiom, % 1.51/1.55 ! [A] : % 1.51/1.55 ( relation(A) % 1.51/1.55 => ! [B] : % 1.51/1.55 ( B = relation_rng(A) % 1.51/1.55 <=> ! [C] : % 1.51/1.55 ( in(C,B) % 1.51/1.55 <=> ? [D] : in(ordered_pair(D,C),A) ) ) ) ). % 1.51/1.55 % 1.51/1.55 fof(d5_tarski,axiom, % 1.51/1.55 ! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)) ). % 1.51/1.55 % 1.51/1.55 fof(dt_k1_relat_1,axiom, % 1.51/1.55 $true ). % 1.51/1.55 % 1.51/1.55 fof(dt_k1_tarski,axiom, % 1.51/1.55 $true ). % 1.51/1.55 % 1.51/1.55 fof(dt_k1_xboole_0,axiom, % 1.51/1.55 $true ). % 1.51/1.55 % 1.51/1.55 fof(dt_k2_relat_1,axiom, % 1.51/1.55 $true ). % 1.51/1.55 % 1.51/1.55 fof(dt_k2_tarski,axiom, % 1.51/1.55 $true ). % 1.51/1.55 % 1.51/1.55 fof(dt_k4_tarski,axiom, % 1.51/1.55 $true ). % 1.51/1.55 % 1.51/1.55 fof(dt_m1_subset_1,axiom, % 1.51/1.55 $true ). % 1.51/1.55 % 1.51/1.55 fof(existence_m1_subset_1,axiom, % 1.51/1.55 ! [A] : % 1.51/1.55 ? [B] : element(B,A) ). % 1.51/1.55 % 1.51/1.55 fof(fc1_xboole_0,axiom, % 1.51/1.55 empty(empty_set) ). % 1.51/1.55 % 1.51/1.55 fof(fc1_zfmisc_1,axiom, % 1.51/1.55 ! [A,B] : ~ empty(ordered_pair(A,B)) ). % 1.51/1.55 % 1.51/1.55 fof(fc2_subset_1,axiom, % 1.51/1.55 ! [A] : ~ empty(singleton(A)) ). % 1.51/1.55 % 1.51/1.55 fof(fc3_subset_1,axiom, % 1.51/1.55 ! [A,B] : ~ empty(unordered_pair(A,B)) ). % 1.51/1.55 % 1.51/1.55 fof(fc4_relat_1,axiom, % 1.51/1.55 ( empty(empty_set) % 1.51/1.55 & relation(empty_set) ) ). % 1.51/1.55 % 1.51/1.55 fof(fc5_relat_1,axiom, % 1.51/1.55 ! [A] : % 1.51/1.55 ( ( ~ empty(A) % 1.51/1.55 & relation(A) ) % 1.51/1.55 => ~ empty(relation_dom(A)) ) ). % 1.51/1.55 % 1.51/1.55 fof(fc6_relat_1,axiom, % 1.51/1.55 ! [A] : % 1.51/1.55 ( ( ~ empty(A) % 1.51/1.55 & relation(A) ) % 1.51/1.55 => ~ empty(relation_rng(A)) ) ). % 1.51/1.55 % 1.51/1.55 fof(fc7_relat_1,axiom, % 1.51/1.55 ! [A] : % 1.51/1.55 ( empty(A) % 1.51/1.55 => ( empty(relation_dom(A)) % 1.51/1.55 & relation(relation_dom(A)) ) ) ). % 1.51/1.55 % 1.51/1.55 fof(fc8_relat_1,axiom, % 1.51/1.55 ! [A] : % 1.51/1.55 ( empty(A) % 1.51/1.55 => ( empty(relation_rng(A)) % 1.51/1.55 & relation(relation_rng(A)) ) ) ). % 1.51/1.55 % 1.51/1.55 fof(rc1_relat_1,axiom, % 1.51/1.55 ? [A] : % 1.51/1.55 ( empty(A) % 1.51/1.55 & relation(A) ) ). % 1.51/1.55 % 1.51/1.55 fof(rc1_xboole_0,axiom, % 1.51/1.55 ? [A] : empty(A) ). % 1.51/1.55 % 1.51/1.55 fof(rc2_relat_1,axiom, % 1.51/1.55 ? [A] : % 1.51/1.55 ( ~ empty(A) % 1.51/1.55 & relation(A) ) ). % 1.51/1.55 % 1.51/1.55 fof(rc2_xboole_0,axiom, % 1.51/1.55 ? [A] : ~ empty(A) ). % 1.51/1.55 % 1.51/1.55 fof(t1_subset,axiom, % 1.51/1.55 ! [A,B] : % 1.51/1.55 ( in(A,B) % 1.51/1.55 => element(A,B) ) ). % 1.51/1.55 % 1.51/1.55 fof(t2_subset,axiom, % 1.51/1.55 ! [A,B] : % 1.51/1.55 ( element(A,B) % 1.51/1.55 => ( empty(B) % 1.51/1.55 | in(A,B) ) ) ). % 1.51/1.55 % 1.51/1.55 fof(t56_relat_1,axiom, % 1.51/1.56 ! [A] : % 1.51/1.56 ( relation(A) % 1.51/1.56 => ( ! [B,C] : ~ in(ordered_pair(B,C),A) % 1.51/1.56 => A = empty_set ) ) ). % 1.51/1.56 % 1.51/1.56 fof(t64_relat_1,conjecture, % 1.51/1.56 ! [A] : % 1.51/1.56 ( relation(A) % 1.51/1.56 => ( ( relation_dom(A) = empty_set % 1.51/1.56 | relation_rng(A) = empty_set ) % 1.51/1.56 => A = empty_set ) ) ). % 1.51/1.56 % 1.51/1.56 fof(t6_boole,axiom, % 1.51/1.56 ! [A] : % 1.51/1.56 ( empty(A) % 1.51/1.56 => A = empty_set ) ). % 1.51/1.56 % 1.51/1.56 fof(t7_boole,axiom, % 1.51/1.56 ! [A,B] : % 1.51/1.56 ~ ( in(A,B) % 1.51/1.56 & empty(B) ) ). % 1.51/1.56 % 1.51/1.56 fof(t8_boole,axiom, % 1.51/1.56 ! [A,B] : % 1.51/1.56 ~ ( empty(A) % 1.51/1.56 & A != B % 1.51/1.56 & empty(B) ) ). % 1.51/1.56 % 1.51/1.56 %------------------------------------------------------------------------------ % 1.51/1.56 %------------------------------------------- % 1.51/1.56 % Proof found % 1.51/1.56 % SZS status Theorem for theBenchmark % 1.51/1.56 % SZS output start Proof % 1.51/1.56 %ClaNum:70(EqnAxiom:31) % 1.51/1.56 %VarNum:144(SingletonVarNum:49) % 1.51/1.56 %MaxLitNum:4 % 1.51/1.56 %MaxfuncDepth:3 % 1.51/1.56 %SharedTerms:20 % 1.51/1.56 %goalClause: 39 42 48 % 1.51/1.56 %singleGoalClaCount:2 % 1.51/1.56 [33]P1(a1) % 1.51/1.56 [34]P1(a2) % 1.51/1.56 [35]P1(a15) % 1.51/1.56 [36]P3(a1) % 1.51/1.56 [37]P3(a2) % 1.51/1.56 [38]P3(a3) % 1.51/1.56 [39]P3(a4) % 1.51/1.56 [42]~E(a4,a1) % 1.51/1.56 [43]~P1(a3) % 1.51/1.56 [44]~P1(a5) % 1.51/1.56 [40]P2(f8(x401),x401) % 1.51/1.56 [45]~P1(f17(x451)) % 1.51/1.56 [41]E(f16(x411,x412),f16(x412,x411)) % 1.51/1.56 [46]~P1(f16(x461,x462)) % 1.51/1.56 [48]E(f18(a4),a1)+E(f19(a4),a1) % 1.51/1.56 [49]~P1(x491)+E(x491,a1) % 1.51/1.56 [50]~P1(x501)+P3(x501) % 1.51/1.56 [52]~P1(x521)+P1(f18(x521)) % 1.51/1.56 [53]~P1(x531)+P1(f19(x531)) % 1.51/1.56 [54]~P1(x541)+P3(f18(x541)) % 1.51/1.56 [55]~P1(x551)+P3(f19(x551)) % 1.51/1.56 [58]~P1(x581)+~P4(x582,x581) % 1.51/1.56 [59]~P4(x591,x592)+P2(x591,x592) % 1.51/1.56 [61]~P4(x612,x611)+~P4(x611,x612) % 1.51/1.56 [56]~P3(x561)+P1(x561)+~P1(f18(x561)) % 1.51/1.56 [57]~P3(x571)+P1(x571)+~P1(f19(x571)) % 1.51/1.56 [62]~P3(x621)+E(x621,a1)+P4(f16(f16(f6(x621),f7(x621)),f17(f6(x621))),x621) % 1.51/1.56 [51]~P1(x512)+~P1(x511)+E(x511,x512) % 1.51/1.56 [60]~P2(x602,x601)+P1(x601)+P4(x602,x601) % 1.51/1.56 [66]~P3(x662)+P4(f10(x662,x661),x661)+E(x661,f18(x662))+P4(f16(f16(f10(x662,x661),f12(x662,x661)),f17(f10(x662,x661))),x662) % 1.51/1.56 [67]~P3(x672)+P4(f9(x672,x671),x671)+E(x671,f19(x672))+P4(f16(f16(f14(x672,x671),f9(x672,x671)),f17(f14(x672,x671))),x672) % 1.51/1.56 [65]~P3(x652)+~P4(f9(x652,x651),x651)+E(x651,f19(x652))+~P4(f16(f16(x653,f9(x652,x651)),f17(x653)),x652) % 1.51/1.56 [69]~P3(x692)+~P4(x691,x693)+~E(x693,f18(x692))+P4(f16(f16(x691,f11(x692,x693,x691)),f17(x691)),x692) % 1.51/1.56 [68]~P3(x682)+~P4(f10(x682,x681),x681)+E(x681,f18(x682))+~P4(f16(f16(f10(x682,x681),x683),f17(f10(x682,x681))),x682) % 1.51/1.56 [70]~P3(x701)+~P4(x703,x702)+~E(x702,f19(x701))+P4(f16(f16(f13(x701,x702,x703),x703),f17(f13(x701,x702,x703))),x701) % 1.51/1.56 [63]~P3(x633)+P4(x631,x632)+~E(x632,f19(x633))+~P4(f16(f16(x634,x631),f17(x634)),x633) % 1.51/1.56 [64]~P3(x643)+P4(x641,x642)+~E(x642,f18(x643))+~P4(f16(f16(x641,x644),f17(x641)),x643) % 1.51/1.56 %EqnAxiom % 1.51/1.56 [1]E(x11,x11) % 1.51/1.56 [2]E(x22,x21)+~E(x21,x22) % 1.51/1.56 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 1.51/1.56 [4]~E(x41,x42)+E(f8(x41),f8(x42)) % 1.51/1.56 [5]~E(x51,x52)+E(f16(x51,x53),f16(x52,x53)) % 1.51/1.56 [6]~E(x61,x62)+E(f16(x63,x61),f16(x63,x62)) % 1.51/1.56 [7]~E(x71,x72)+E(f19(x71),f19(x72)) % 1.51/1.56 [8]~E(x81,x82)+E(f17(x81),f17(x82)) % 1.51/1.56 [9]~E(x91,x92)+E(f12(x91,x93),f12(x92,x93)) % 1.51/1.56 [10]~E(x101,x102)+E(f12(x103,x101),f12(x103,x102)) % 1.51/1.56 [11]~E(x111,x112)+E(f13(x111,x113,x114),f13(x112,x113,x114)) % 1.51/1.56 [12]~E(x121,x122)+E(f13(x123,x121,x124),f13(x123,x122,x124)) % 1.51/1.56 [13]~E(x131,x132)+E(f13(x133,x134,x131),f13(x133,x134,x132)) % 1.51/1.56 [14]~E(x141,x142)+E(f10(x141,x143),f10(x142,x143)) % 1.51/1.56 [15]~E(x151,x152)+E(f10(x153,x151),f10(x153,x152)) % 1.51/1.56 [16]~E(x161,x162)+E(f9(x161,x163),f9(x162,x163)) % 1.51/1.56 [17]~E(x171,x172)+E(f9(x173,x171),f9(x173,x172)) % 1.51/1.56 [18]~E(x181,x182)+E(f18(x181),f18(x182)) % 1.51/1.56 [19]~E(x191,x192)+E(f11(x191,x193,x194),f11(x192,x193,x194)) % 1.51/1.56 [20]~E(x201,x202)+E(f11(x203,x201,x204),f11(x203,x202,x204)) % 1.51/1.56 [21]~E(x211,x212)+E(f11(x213,x214,x211),f11(x213,x214,x212)) % 1.51/1.56 [22]~E(x221,x222)+E(f6(x221),f6(x222)) % 1.51/1.56 [23]~E(x231,x232)+E(f14(x231,x233),f14(x232,x233)) % 1.51/1.56 [24]~E(x241,x242)+E(f14(x243,x241),f14(x243,x242)) % 1.51/1.56 [25]~E(x251,x252)+E(f7(x251),f7(x252)) % 1.51/1.56 [26]~P1(x261)+P1(x262)+~E(x261,x262) % 1.51/1.56 [27]P4(x272,x273)+~E(x271,x272)+~P4(x271,x273) % 1.51/1.56 [28]P4(x283,x282)+~E(x281,x282)+~P4(x283,x281) % 1.51/1.56 [29]~P3(x291)+P3(x292)+~E(x291,x292) % 1.51/1.56 [30]P2(x302,x303)+~E(x301,x302)+~P2(x301,x303) % 1.51/1.56 [31]P2(x313,x312)+~E(x311,x312)+~P2(x313,x311) % 1.51/1.56 % 1.51/1.56 %------------------------------------------- % 1.51/1.56 cnf(72,plain, % 1.51/1.56 (~P3(x721)+P4(x722,f18(x721))+~P4(f16(f16(x722,x723),f17(x722)),x721)), % 1.51/1.56 inference(equality_inference,[],[64])). % 1.51/1.56 cnf(73,plain, % 1.51/1.56 (~P3(x731)+~P4(x732,f18(x731))+P4(f16(f16(x732,f11(x731,f18(x731),x732)),f17(x732)),x731)), % 1.51/1.56 inference(equality_inference,[],[69])). % 1.51/1.56 cnf(75,plain, % 1.51/1.56 (~P1(a4)), % 1.51/1.56 inference(scs_inference,[],[42,49])). % 1.51/1.56 cnf(77,plain, % 1.51/1.56 (~P4(x771,a1)), % 1.51/1.56 inference(scs_inference,[],[42,33,49,58])). % 1.51/1.56 cnf(79,plain, % 1.51/1.56 (~P4(x791,f18(a1))), % 1.51/1.56 inference(scs_inference,[],[42,33,36,49,58,73])). % 1.51/1.56 cnf(81,plain, % 1.51/1.56 (P2(f8(f16(x811,x812)),f16(x812,x811))), % 1.51/1.56 inference(scs_inference,[],[42,40,41,33,36,49,58,73,31])). % 1.51/1.56 cnf(82,plain, % 1.51/1.56 (P2(f8(x821),x821)), % 1.51/1.56 inference(rename_variables,[],[40])). % 1.51/1.56 cnf(89,plain, % 1.51/1.56 (~E(a3,f18(a1))), % 1.51/1.56 inference(scs_inference,[],[42,40,82,41,33,36,43,49,58,73,31,60,61,27,28])). % 1.51/1.56 cnf(96,plain, % 1.51/1.56 (~P4(x961,a2)), % 1.51/1.56 inference(scs_inference,[],[34,58])). % 1.51/1.56 cnf(98,plain, % 1.51/1.56 (E(a2,a1)), % 1.51/1.56 inference(scs_inference,[],[34,37,58,62])). % 1.51/1.56 cnf(105,plain, % 1.51/1.56 (~P4(x1051,f18(a1))), % 1.51/1.56 inference(rename_variables,[],[79])). % 1.51/1.56 cnf(106,plain, % 1.51/1.56 (P4(f10(a1,a3),a3)), % 1.51/1.56 inference(scs_inference,[],[42,79,89,75,77,34,37,40,36,58,62,3,60,28,66])). % 1.51/1.56 cnf(107,plain, % 1.51/1.56 (~P4(x1071,a1)), % 1.51/1.56 inference(rename_variables,[],[77])). % 1.51/1.56 cnf(109,plain, % 1.51/1.56 (E(f18(a1),f19(a1))), % 1.51/1.56 inference(scs_inference,[],[42,79,105,89,75,77,107,34,37,40,36,58,62,3,60,28,66,67])). % 1.51/1.56 cnf(116,plain, % 1.51/1.56 (~P1(f18(a1))+P1(f19(a1))), % 1.51/1.56 inference(scs_inference,[],[42,79,105,89,75,77,107,34,37,40,36,58,62,3,60,28,66,67,2,61,26])). % 1.51/1.56 cnf(123,plain, % 1.51/1.56 (E(f19(a1),f18(a1))), % 1.51/1.56 inference(scs_inference,[],[109,35,58,2])). % 1.51/1.56 cnf(127,plain, % 1.51/1.56 (P2(f8(x1271),x1271)), % 1.51/1.56 inference(rename_variables,[],[40])). % 1.51/1.56 cnf(129,plain, % 1.51/1.56 (~P4(x1291,f18(a2))), % 1.51/1.56 inference(scs_inference,[],[109,106,96,35,44,37,40,58,2,61,60,73])). % 1.51/1.56 cnf(130,plain, % 1.51/1.56 (~P4(x1301,a2)), % 1.51/1.56 inference(rename_variables,[],[96])). % 1.51/1.56 cnf(132,plain, % 1.51/1.56 (~E(a3,f19(a1))), % 1.51/1.56 inference(scs_inference,[],[89,109,106,96,35,44,37,40,58,2,61,60,73,3])). % 1.51/1.56 cnf(134,plain, % 1.51/1.56 (~P4(x1341,f18(a1))), % 1.51/1.56 inference(rename_variables,[],[79])). % 1.51/1.56 cnf(138,plain, % 1.51/1.56 (~P4(x1381,a2)), % 1.51/1.56 inference(rename_variables,[],[96])). % 1.51/1.56 cnf(140,plain, % 1.51/1.56 (E(f18(a1),f18(a2))), % 1.51/1.56 inference(scs_inference,[],[89,109,106,79,134,96,130,138,35,44,37,40,127,58,2,61,60,73,3,28,31,70,66])). % 1.51/1.56 cnf(141,plain, % 1.51/1.56 (~P4(x1411,a2)), % 1.51/1.56 inference(rename_variables,[],[96])). % 1.51/1.56 cnf(147,plain, % 1.51/1.56 (P4(f9(a2,a3),a3)), % 1.51/1.56 inference(scs_inference,[],[89,109,106,79,134,96,130,138,141,35,44,77,37,40,127,36,58,2,61,60,73,3,28,31,70,66,69,67])). % 1.51/1.56 cnf(166,plain, % 1.51/1.56 (P2(f8(x1661),x1661)), % 1.51/1.56 inference(rename_variables,[],[40])). % 1.51/1.56 cnf(168,plain, % 1.51/1.56 (E(f19(a1),f18(a2))), % 1.51/1.56 inference(scs_inference,[],[123,140,147,45,40,2,61,60,3])). % 1.51/1.56 cnf(172,plain, % 1.51/1.56 (~P4(x1721,f18(a2))), % 1.51/1.56 inference(rename_variables,[],[129])). % 1.51/1.56 cnf(173,plain, % 1.51/1.56 (P4(f10(a2,a3),a3)), % 1.51/1.56 inference(scs_inference,[],[98,129,123,140,147,45,96,40,166,37,2,61,60,3,31,28,66])). % 1.51/1.56 cnf(179,plain, % 1.51/1.56 (~P3(f18(a2))+E(f18(a2),a1)), % 1.51/1.56 inference(scs_inference,[],[98,129,172,123,140,132,147,45,96,77,40,166,36,37,2,61,60,3,31,28,66,67,62])). % 1.51/1.56 cnf(194,plain, % 1.51/1.56 (P4(f8(f16(x1941,x1942)),f16(x1942,x1941))), % 1.51/1.56 inference(scs_inference,[],[81,168,173,46,61,2,60])). % 1.51/1.56 cnf(276,plain, % 1.51/1.56 (~P1(f19(a1))+P3(f18(a2))), % 1.51/1.56 inference(scs_inference,[],[168,79,33,194,28,29,55,50])). % 1.51/1.56 cnf(602,plain, % 1.51/1.56 (P2(f16(f16(f6(a4),f7(a4)),f17(f6(a4))),a4)), % 1.51/1.56 inference(scs_inference,[],[42,39,59,62])). % 1.51/1.56 cnf(603,plain, % 1.51/1.56 (P2(f16(f17(f6(a4)),f16(f6(a4),f7(a4))),a4)), % 1.51/1.56 inference(scs_inference,[],[41,602,30])). % 1.51/1.56 cnf(607,plain, % 1.51/1.56 (P1(f19(a1))), % 1.51/1.56 inference(scs_inference,[],[33,116,52])). % 1.51/1.56 cnf(609,plain, % 1.51/1.56 (P3(f18(a2))), % 1.51/1.56 inference(scs_inference,[],[607,276])). % 1.51/1.56 cnf(613,plain, % 1.51/1.56 (P4(f16(f16(f6(a4),f7(a4)),f17(f6(a4))),a4)), % 1.51/1.56 inference(scs_inference,[],[75,603,41,60,27])). % 1.51/1.56 cnf(619,plain, % 1.51/1.56 (E(f18(a2),a1)), % 1.51/1.56 inference(scs_inference,[],[609,179])). % 1.51/1.56 cnf(665,plain, % 1.51/1.56 (P4(f6(a4),f18(a4))), % 1.51/1.56 inference(scs_inference,[],[39,619,613,61,2,72])). % 1.51/1.56 cnf(959,plain, % 1.51/1.56 (~P4(x9591,a1)), % 1.51/1.56 inference(rename_variables,[],[77])). % 1.51/1.56 cnf(961,plain, % 1.51/1.56 (~P4(x9611,a1)), % 1.51/1.56 inference(rename_variables,[],[77])). % 1.51/1.56 cnf(967,plain, % 1.51/1.56 ($false), % 1.51/1.56 inference(scs_inference,[],[77,959,961,39,665,613,28,64,63,48,2]), % 1.51/1.56 ['proof']). % 1.51/1.56 % SZS output end Proof % 1.51/1.56 % Total time :0.910000s %------------------------------------------------------------------------------