%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU045+1 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/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:00:55 EDT 2024 % Result : Theorem 4.42s 4.52s % Output : CNFRefutation 4.42s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SEU045+1 : TPTP v8.2.0. Released v3.2.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n021.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Jun 21 15:09:24 EDT 2024 % 0.12/0.34 % CPUTime : % 0.21/0.57 start to proof:theBenchmark % 4.42/4.51 %------------------------------------------- % 4.42/4.51 % File :CSE---1.7 % 4.42/4.51 % Problem :theBenchmark % 4.42/4.51 % Transform :cnf % 4.42/4.51 % Format :tptp:raw % 4.42/4.51 % Command :java -jar mcs_scs.jar %d %s % 4.42/4.51 % 4.42/4.51 % Result :Theorem 3.890000s % 4.42/4.51 % Output :CNFRefutation 3.890000s % 4.42/4.51 %------------------------------------------- % 4.42/4.51 %------------------------------------------------------------------------------ % 4.42/4.51 % File : SEU045+1 : TPTP v8.2.0. Released v3.2.0. % 4.42/4.51 % Domain : Set theory % 4.42/4.51 % Problem : Functions and their basic properties, theorem 87 % 4.42/4.51 % Version : [Urb06] axioms : Especial. % 4.42/4.51 % English : % 4.42/4.51 % 4.42/4.51 % Refs : [Byl90] Bylinski (1990), Functions and Their Basic Properties % 4.42/4.51 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 4.42/4.51 % Source : [Urb06] % 4.42/4.51 % Names : funct_1__t87_funct_1 [Urb06] % 4.42/4.51 % 4.42/4.51 % Status : Theorem % 4.42/4.51 % Rating : 0.19 v8.2.0, 0.17 v8.1.0, 0.14 v7.5.0, 0.16 v7.4.0, 0.10 v7.3.0, 0.14 v7.1.0, 0.17 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.17 v6.2.0, 0.20 v6.1.0, 0.33 v6.0.0, 0.35 v5.5.0, 0.37 v5.4.0, 0.39 v5.3.0, 0.41 v5.2.0, 0.15 v5.1.0, 0.14 v5.0.0, 0.25 v4.1.0, 0.26 v4.0.0, 0.25 v3.7.0, 0.15 v3.5.0, 0.11 v3.4.0, 0.16 v3.3.0, 0.14 v3.2.0 % 4.42/4.51 % Syntax : Number of formulae : 34 ( 6 unt; 0 def) % 4.42/4.51 % Number of atoms : 88 ( 5 equ) % 4.42/4.51 % Maximal formula atoms : 10 ( 2 avg) % 4.42/4.51 % Number of connectives : 66 ( 12 ~; 1 |; 32 &) % 4.42/4.51 % ( 3 <=>; 18 =>; 0 <=; 0 <~>) % 4.42/4.51 % Maximal formula depth : 11 ( 4 avg) % 4.42/4.51 % Maximal term depth : 3 ( 1 avg) % 4.42/4.51 % Number of predicates : 9 ( 8 usr; 0 prp; 1-2 aty) % 4.42/4.51 % Number of functors : 5 ( 5 usr; 1 con; 0-2 aty) % 4.42/4.51 % Number of variables : 53 ( 42 !; 11 ?) % 4.42/4.51 % SPC : FOF_THM_RFO_SEQ % 4.42/4.51 % 4.42/4.51 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 4.42/4.51 % library, www.mizar.org % 4.42/4.51 %------------------------------------------------------------------------------ % 4.42/4.51 fof(reflexivity_r1_tarski,axiom, % 4.42/4.51 ! [A,B] : subset(A,A) ). % 4.42/4.51 % 4.42/4.51 fof(fc4_relat_1,axiom, % 4.42/4.51 ( empty(empty_set) % 4.42/4.51 & relation(empty_set) ) ). % 4.42/4.51 % 4.42/4.51 fof(fc12_relat_1,axiom, % 4.42/4.51 ( empty(empty_set) % 4.42/4.51 & relation(empty_set) % 4.42/4.51 & relation_empty_yielding(empty_set) ) ). % 4.42/4.51 % 4.42/4.51 fof(fc1_xboole_0,axiom, % 4.42/4.51 empty(empty_set) ). % 4.42/4.51 % 4.42/4.51 fof(existence_m1_subset_1,axiom, % 4.42/4.51 ! [A] : % 4.42/4.51 ? [B] : element(B,A) ). % 4.42/4.51 % 4.42/4.51 fof(cc1_funct_1,axiom, % 4.42/4.51 ! [A] : % 4.42/4.51 ( empty(A) % 4.42/4.51 => function(A) ) ). % 4.42/4.51 % 4.42/4.51 fof(cc2_funct_1,axiom, % 4.42/4.51 ! [A] : % 4.42/4.51 ( ( relation(A) % 4.42/4.51 & empty(A) % 4.42/4.51 & function(A) ) % 4.42/4.51 => ( relation(A) % 4.42/4.52 & function(A) % 4.42/4.52 & one_to_one(A) ) ) ). % 4.42/4.52 % 4.42/4.52 fof(fc1_subset_1,axiom, % 4.42/4.52 ! [A] : ~ empty(powerset(A)) ). % 4.42/4.52 % 4.42/4.52 fof(fc5_relat_1,axiom, % 4.42/4.52 ! [A] : % 4.42/4.52 ( ( ~ empty(A) % 4.42/4.52 & relation(A) ) % 4.42/4.52 => ~ empty(relation_dom(A)) ) ). % 4.42/4.52 % 4.42/4.52 fof(fc7_relat_1,axiom, % 4.42/4.52 ! [A] : % 4.42/4.52 ( empty(A) % 4.42/4.52 => ( empty(relation_dom(A)) % 4.42/4.52 & relation(relation_dom(A)) ) ) ). % 4.42/4.52 % 4.42/4.52 fof(cc1_relat_1,axiom, % 4.42/4.52 ! [A] : % 4.42/4.52 ( empty(A) % 4.42/4.52 => relation(A) ) ). % 4.42/4.52 % 4.42/4.52 fof(t2_subset,axiom, % 4.42/4.52 ! [A,B] : % 4.42/4.52 ( element(A,B) % 4.42/4.52 => ( empty(B) % 4.42/4.52 | in(A,B) ) ) ). % 4.42/4.52 % 4.42/4.52 fof(t3_subset,axiom, % 4.42/4.52 ! [A,B] : % 4.42/4.52 ( element(A,powerset(B)) % 4.42/4.52 <=> subset(A,B) ) ). % 4.42/4.52 % 4.42/4.52 fof(t4_subset,axiom, % 4.42/4.52 ! [A,B,C] : % 4.42/4.52 ( ( in(A,B) % 4.42/4.52 & element(B,powerset(C)) ) % 4.42/4.52 => element(A,C) ) ). % 4.42/4.52 % 4.42/4.52 fof(t5_subset,axiom, % 4.42/4.52 ! [A,B,C] : % 4.42/4.52 ~ ( in(A,B) % 4.42/4.52 & element(B,powerset(C)) % 4.42/4.52 & empty(C) ) ). % 4.42/4.52 % 4.42/4.52 fof(t6_boole,axiom, % 4.42/4.52 ! [A] : % 4.42/4.52 ( empty(A) % 4.42/4.52 => A = empty_set ) ). % 4.42/4.52 % 4.42/4.52 fof(t8_boole,axiom, % 4.42/4.52 ! [A,B] : % 4.42/4.52 ~ ( empty(A) % 4.42/4.52 & A != B % 4.42/4.52 & empty(B) ) ). % 4.42/4.52 % 4.42/4.52 fof(antisymmetry_r2_hidden,axiom, % 4.42/4.52 ! [A,B] : % 4.42/4.52 ( in(A,B) % 4.42/4.52 => ~ in(B,A) ) ). % 4.42/4.52 % 4.42/4.52 fof(dt_k8_relat_1,axiom, % 4.42/4.52 ! [A,B] : % 4.42/4.52 ( relation(B) % 4.42/4.52 => relation(relation_rng_restriction(A,B)) ) ). % 4.42/4.52 % 4.42/4.52 fof(fc5_funct_1,axiom, % 4.42/4.52 ! [A,B] : % 4.42/4.52 ( ( relation(B) % 4.42/4.52 & function(B) ) % 4.42/4.52 => ( relation(relation_rng_restriction(A,B)) % 4.42/4.52 & function(relation_rng_restriction(A,B)) ) ) ). % 4.42/4.52 % 4.42/4.52 fof(rc1_funct_1,axiom, % 4.42/4.52 ? [A] : % 4.42/4.52 ( relation(A) % 4.42/4.52 & function(A) ) ). % 4.42/4.52 % 4.42/4.52 fof(rc2_funct_1,axiom, % 4.42/4.52 ? [A] : % 4.42/4.52 ( relation(A) % 4.42/4.52 & empty(A) % 4.42/4.52 & function(A) ) ). % 4.42/4.52 % 4.42/4.52 fof(rc3_funct_1,axiom, % 4.42/4.52 ? [A] : % 4.42/4.52 ( relation(A) % 4.42/4.52 & function(A) % 4.42/4.52 & one_to_one(A) ) ). % 4.42/4.52 % 4.42/4.52 fof(rc1_subset_1,axiom, % 4.42/4.52 ! [A] : % 4.42/4.52 ( ~ empty(A) % 4.42/4.52 => ? [B] : % 4.42/4.52 ( element(B,powerset(A)) % 4.42/4.52 & ~ empty(B) ) ) ). % 4.42/4.52 % 4.42/4.52 fof(rc2_subset_1,axiom, % 4.42/4.52 ! [A] : % 4.42/4.52 ? [B] : % 4.42/4.52 ( element(B,powerset(A)) % 4.42/4.52 & empty(B) ) ). % 4.42/4.52 % 4.42/4.52 fof(rc1_relat_1,axiom, % 4.42/4.52 ? [A] : % 4.42/4.52 ( empty(A) % 4.42/4.52 & relation(A) ) ). % 4.42/4.52 % 4.42/4.52 fof(rc2_relat_1,axiom, % 4.42/4.52 ? [A] : % 4.42/4.52 ( ~ empty(A) % 4.42/4.52 & relation(A) ) ). % 4.42/4.52 % 4.42/4.52 fof(rc3_relat_1,axiom, % 4.42/4.52 ? [A] : % 4.42/4.52 ( relation(A) % 4.42/4.52 & relation_empty_yielding(A) ) ). % 4.42/4.52 % 4.42/4.52 fof(rc1_xboole_0,axiom, % 4.42/4.52 ? [A] : empty(A) ). % 4.42/4.52 % 4.42/4.52 fof(rc2_xboole_0,axiom, % 4.42/4.52 ? [A] : ~ empty(A) ). % 4.42/4.52 % 4.42/4.52 fof(t1_subset,axiom, % 4.42/4.52 ! [A,B] : % 4.42/4.52 ( in(A,B) % 4.42/4.52 => element(A,B) ) ). % 4.42/4.52 % 4.42/4.52 fof(t7_boole,axiom, % 4.42/4.52 ! [A,B] : % 4.42/4.52 ~ ( in(A,B) % 4.42/4.52 & empty(B) ) ). % 4.42/4.52 % 4.42/4.52 fof(t87_funct_1,conjecture, % 4.42/4.52 ! [A,B,C] : % 4.42/4.52 ( ( relation(C) % 4.42/4.52 & function(C) ) % 4.42/4.52 => ( in(B,relation_dom(relation_rng_restriction(A,C))) % 4.42/4.52 => apply(relation_rng_restriction(A,C),B) = apply(C,B) ) ) ). % 4.42/4.52 % 4.42/4.52 fof(t85_funct_1,axiom, % 4.42/4.52 ! [A,B] : % 4.42/4.52 ( ( relation(B) % 4.42/4.52 & function(B) ) % 4.42/4.52 => ! [C] : % 4.42/4.52 ( ( relation(C) % 4.42/4.52 & function(C) ) % 4.42/4.52 => ( B = relation_rng_restriction(A,C) % 4.42/4.52 <=> ( ! [D] : % 4.42/4.52 ( in(D,relation_dom(B)) % 4.42/4.52 <=> ( in(D,relation_dom(C)) % 4.42/4.52 & in(apply(C,D),A) ) ) % 4.42/4.52 & ! [D] : % 4.42/4.52 ( in(D,relation_dom(B)) % 4.42/4.52 => apply(B,D) = apply(C,D) ) ) ) ) ) ). % 4.42/4.52 % 4.42/4.52 %------------------------------------------------------------------------------ % 4.42/4.52 %------------------------------------------- % 4.42/4.52 % Proof found % 4.42/4.52 % SZS status Theorem for theBenchmark % 4.42/4.52 % SZS output start Proof % 4.42/4.52 %ClaNum:91(EqnAxiom:29) % 4.42/4.52 %VarNum:264(SingletonVarNum:72) % 4.42/4.52 %MaxLitNum:9 % 4.42/4.52 %MaxfuncDepth:2 % 4.42/4.52 %SharedTerms:39 % 4.42/4.52 %goalClause: 44 50 56 60 % 4.42/4.52 %singleGoalClaCount:4 % 4.42/4.52 [32]P1(a1) % 4.42/4.52 [33]P1(a3) % 4.42/4.52 [34]P1(a13) % 4.42/4.52 [35]P1(a4) % 4.42/4.52 [37]P3(a1) % 4.42/4.52 [38]P3(a5) % 4.42/4.52 [39]P3(a3) % 4.42/4.52 [40]P3(a14) % 4.42/4.52 [41]P3(a13) % 4.42/4.52 [42]P3(a17) % 4.42/4.52 [43]P3(a18) % 4.42/4.52 [44]P3(a6) % 4.42/4.52 [45]P7(a1) % 4.42/4.52 [46]P7(a18) % 4.42/4.52 [47]P4(a5) % 4.42/4.52 [48]P4(a3) % 4.42/4.52 [49]P4(a14) % 4.42/4.52 [50]P4(a6) % 4.42/4.52 [51]P5(a14) % 4.42/4.52 [57]~P1(a17) % 4.42/4.52 [58]~P1(a9) % 4.42/4.52 [56]P6(a7,f21(f20(a8,a6))) % 4.42/4.52 [60]~E(f2(f20(a8,a6),a7),f2(a6,a7)) % 4.42/4.52 [53]P8(x531,x531) % 4.42/4.52 [52]P1(f15(x521)) % 4.42/4.52 [54]P2(f10(x541),x541) % 4.42/4.52 [55]P2(f15(x551),f19(x551)) % 4.42/4.52 [59]~P1(f19(x591)) % 4.42/4.52 [61]~P1(x611)+E(x611,a1) % 4.42/4.52 [62]~P1(x621)+P3(x621) % 4.42/4.52 [63]~P1(x631)+P4(x631) % 4.42/4.52 [65]~P1(x651)+P1(f21(x651)) % 4.42/4.52 [66]~P1(x661)+P3(f21(x661)) % 4.42/4.52 [67]P1(x671)+~P1(f16(x671)) % 4.42/4.52 [71]P1(x711)+P2(f16(x711),f19(x711)) % 4.42/4.52 [70]~P1(x701)+~P6(x702,x701) % 4.42/4.52 [72]~P6(x721,x722)+P2(x721,x722) % 4.42/4.52 [78]~P6(x782,x781)+~P6(x781,x782) % 4.42/4.52 [73]~P3(x732)+P3(f20(x731,x732)) % 4.42/4.52 [75]~P8(x751,x752)+P2(x751,f19(x752)) % 4.42/4.52 [79]P8(x791,x792)+~P2(x791,f19(x792)) % 4.42/4.52 [69]~P3(x691)+P1(x691)+~P1(f21(x691)) % 4.42/4.52 [64]~P1(x642)+~P1(x641)+E(x641,x642) % 4.42/4.52 [74]~P2(x742,x741)+P1(x741)+P6(x742,x741) % 4.42/4.52 [77]~P3(x772)+~P4(x772)+P4(f20(x771,x772)) % 4.42/4.52 [80]~P1(x801)+~P6(x802,x803)+~P2(x803,f19(x801)) % 4.42/4.52 [81]P2(x811,x812)+~P6(x811,x813)+~P2(x813,f19(x812)) % 4.42/4.52 [68]~P1(x681)+~P3(x681)+~P4(x681)+P5(x681) % 4.42/4.52 [82]~P3(x823)+~P3(x822)+~P4(x823)+~P4(x822)+~P6(x821,f21(x823))+P6(x821,f21(x822))+~E(x823,f20(x824,x822)) % 4.42/4.52 [83]~P3(x833)+~P3(x831)+~P4(x833)+~P4(x831)+~P6(x832,f21(x831))+E(f2(x831,x832),f2(x833,x832))+~E(x831,f20(x834,x833)) % 4.42/4.52 [84]~P3(x844)+~P3(x841)+~P4(x844)+~P4(x841)+~P6(x842,f21(x844))+P6(f2(x841,x842),x843)+~E(x844,f20(x843,x841)) % 4.42/4.52 [86]~P3(x863)+~P3(x861)+~P4(x863)+~P4(x861)+P6(f11(x862,x861,x863),f21(x863))+P6(f11(x862,x861,x863),f21(x861))+P6(f12(x862,x861,x863),f21(x861))+E(x861,f20(x862,x863)) % 4.42/4.52 [87]~P3(x873)+~P3(x871)+~P4(x873)+~P4(x871)+P6(f11(x872,x871,x873),f21(x871))+P6(f12(x872,x871,x873),f21(x871))+E(x871,f20(x872,x873))+P6(f2(x873,f11(x872,x871,x873)),x872) % 4.42/4.52 [88]~P3(x883)+~P3(x881)+~P4(x883)+~P4(x881)+P6(f11(x882,x881,x883),f21(x883))+P6(f11(x882,x881,x883),f21(x881))+E(x881,f20(x882,x883))+~E(f2(x881,f12(x882,x881,x883)),f2(x883,f12(x882,x881,x883))) % 4.42/4.52 [89]~P3(x893)+~P3(x891)+~P4(x893)+~P4(x891)+P6(f11(x892,x891,x893),f21(x891))+E(x891,f20(x892,x893))+P6(f2(x893,f11(x892,x891,x893)),x892)+~E(f2(x891,f12(x892,x891,x893)),f2(x893,f12(x892,x891,x893))) % 4.42/4.52 [85]~P3(x852)+~P3(x854)+~P4(x852)+~P4(x854)+~P6(x851,f21(x854))+~P6(f2(x854,x851),x853)+P6(x851,f21(x852))+~E(x852,f20(x853,x854)) % 4.42/4.52 [90]~P3(x903)+~P3(x901)+~P4(x903)+~P4(x901)+P6(f12(x902,x901,x903),f21(x901))+~P6(f11(x902,x901,x903),f21(x903))+~P6(f11(x902,x901,x903),f21(x901))+E(x901,f20(x902,x903))+~P6(f2(x903,f11(x902,x901,x903)),x902) % 4.42/4.52 [91]~P3(x913)+~P3(x911)+~P4(x913)+~P4(x911)+~P6(f11(x912,x911,x913),f21(x913))+~P6(f11(x912,x911,x913),f21(x911))+E(x911,f20(x912,x913))+~E(f2(x911,f12(x912,x911,x913)),f2(x913,f12(x912,x911,x913)))+~P6(f2(x913,f11(x912,x911,x913)),x912) % 4.42/4.52 %EqnAxiom % 4.42/4.52 [1]E(x11,x11) % 4.42/4.52 [2]E(x22,x21)+~E(x21,x22) % 4.42/4.52 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 4.42/4.52 [4]~E(x41,x42)+E(f15(x41),f15(x42)) % 4.42/4.52 [5]~E(x51,x52)+E(f10(x51),f10(x52)) % 4.42/4.52 [6]~E(x61,x62)+E(f2(x61,x63),f2(x62,x63)) % 4.42/4.52 [7]~E(x71,x72)+E(f2(x73,x71),f2(x73,x72)) % 4.42/4.52 [8]~E(x81,x82)+E(f19(x81),f19(x82)) % 4.42/4.52 [9]~E(x91,x92)+E(f20(x91,x93),f20(x92,x93)) % 4.42/4.52 [10]~E(x101,x102)+E(f20(x103,x101),f20(x103,x102)) % 4.42/4.52 [11]~E(x111,x112)+E(f21(x111),f21(x112)) % 4.42/4.52 [12]~E(x121,x122)+E(f11(x121,x123,x124),f11(x122,x123,x124)) % 4.42/4.52 [13]~E(x131,x132)+E(f11(x133,x131,x134),f11(x133,x132,x134)) % 4.42/4.52 [14]~E(x141,x142)+E(f11(x143,x144,x141),f11(x143,x144,x142)) % 4.42/4.53 [15]~E(x151,x152)+E(f12(x151,x153,x154),f12(x152,x153,x154)) % 4.42/4.53 [16]~E(x161,x162)+E(f12(x163,x161,x164),f12(x163,x162,x164)) % 4.42/4.53 [17]~E(x171,x172)+E(f12(x173,x174,x171),f12(x173,x174,x172)) % 4.42/4.53 [18]~E(x181,x182)+E(f16(x181),f16(x182)) % 4.42/4.53 [19]~P1(x191)+P1(x192)+~E(x191,x192) % 4.42/4.53 [20]P6(x202,x203)+~E(x201,x202)+~P6(x201,x203) % 4.42/4.53 [21]P6(x213,x212)+~E(x211,x212)+~P6(x213,x211) % 4.42/4.53 [22]~P4(x221)+P4(x222)+~E(x221,x222) % 4.42/4.53 [23]~P3(x231)+P3(x232)+~E(x231,x232) % 4.42/4.53 [24]P2(x242,x243)+~E(x241,x242)+~P2(x241,x243) % 4.42/4.53 [25]P2(x253,x252)+~E(x251,x252)+~P2(x253,x251) % 4.42/4.53 [26]~P5(x261)+P5(x262)+~E(x261,x262) % 4.42/4.53 [27]~P7(x271)+P7(x272)+~E(x271,x272) % 4.42/4.53 [28]P8(x282,x283)+~E(x281,x282)+~P8(x281,x283) % 4.42/4.53 [29]P8(x293,x292)+~E(x291,x292)+~P8(x293,x291) % 4.42/4.53 % 4.42/4.53 %------------------------------------------- % 4.42/4.53 cnf(92,plain, % 4.42/4.53 (~P4(f20(x921,x922))+~P4(x922)+~P3(f20(x921,x922))+~P3(x922)+P6(x923,f21(x922))+~P6(x923,f21(f20(x921,x922)))), % 4.42/4.53 inference(equality_inference,[],[82])). % 4.42/4.53 cnf(93,plain, % 4.42/4.53 (~P4(x931)+~P4(f20(x932,x931))+~P3(x931)+~P3(f20(x932,x931))+E(f2(f20(x932,x931),x933),f2(x931,x933))+~P6(x933,f21(f20(x932,x931)))), % 4.42/4.53 inference(equality_inference,[],[83])). % 4.42/4.53 cnf(94,plain, % 4.42/4.53 (~P4(f20(x941,x942))+~P4(x942)+~P3(f20(x941,x942))+~P3(x942)+P6(f2(x942,x943),x941)+~P6(x943,f21(f20(x941,x942)))), % 4.42/4.53 inference(equality_inference,[],[84])). % 4.42/4.53 cnf(201,plain, % 4.42/4.53 (~P6(x2011,f10(f19(a3)))), % 4.42/4.53 inference(scs_inference,[],[33,54,70,80])). % 4.42/4.53 cnf(225,plain, % 4.42/4.53 (~P4(f20(a8,a6))+~P3(f20(a8,a6))), % 4.42/4.53 inference(scs_inference,[],[44,60,56,50,201,34,38,47,54,80,21,68,94,92,93])). % 4.42/4.53 cnf(909,plain, % 4.42/4.53 (~P4(f20(a8,a6))), % 4.42/4.53 inference(scs_inference,[],[44,225,73])). % 4.42/4.53 cnf(910,plain, % 4.42/4.53 ($false), % 4.42/4.53 inference(scs_inference,[],[44,50,909,77]), % 4.42/4.53 ['proof']). % 4.42/4.53 % SZS output end Proof % 4.42/4.53 % Total time :3.890000s %------------------------------------------------------------------------------