%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM388+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 : n028.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 12:24:05 EDT 2024 % Result : Theorem 58.63s 58.70s % Output : CNFRefutation 58.63s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM388+1 : TPTP v8.2.0. Released v3.2.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n028.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 : Sun Jun 23 02:06:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.49/0.57 start to proof:theBenchmark % 58.63/58.68 %------------------------------------------- % 58.63/58.68 % File :CSE---1.7 % 58.63/58.68 % Problem :theBenchmark % 58.63/58.68 % Transform :cnf % 58.63/58.68 % Format :tptp:raw % 58.63/58.68 % Command :java -jar mcs_scs.jar %d %s % 58.63/58.68 % 58.63/58.68 % Result :Theorem 58.050000s % 58.63/58.68 % Output :CNFRefutation 58.050000s % 58.63/58.68 %------------------------------------------- % 58.63/58.69 %------------------------------------------------------------------------------ % 58.63/58.69 % File : NUM388+1 : TPTP v8.2.0. Released v3.2.0. % 58.63/58.69 % Domain : Number Theory (Ordinals) % 58.63/58.69 % Problem : Ordinal numbers, theorem 19 % 58.63/58.69 % Version : [Urb06] axioms : Especial. % 58.63/58.69 % English : % 58.63/58.69 % 58.63/58.69 % Refs : [Ban90] Bancerek (1990), The Ordinal Numbers % 58.63/58.69 % [Urb06] Urban (2006), Email to G. Sutcliffe % 58.63/58.69 % Source : [Urb06] % 58.63/58.69 % Names : ordinal1__t19_ordinal1 [Urb06] % 58.63/58.69 % 58.63/58.69 % Status : Theorem % 58.63/58.69 % Rating : 0.14 v8.1.0, 0.11 v7.5.0, 0.12 v7.4.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.04 v7.0.0, 0.07 v6.4.0, 0.12 v6.2.0, 0.08 v6.1.0, 0.13 v6.0.0, 0.09 v5.5.0, 0.15 v5.4.0, 0.11 v5.3.0, 0.19 v5.2.0, 0.05 v5.0.0, 0.04 v3.7.0, 0.05 v3.4.0, 0.11 v3.3.0, 0.07 v3.2.0 % 58.63/58.69 % Syntax : Number of formulae : 32 ( 5 unt; 0 def) % 58.63/58.69 % Number of atoms : 80 ( 2 equ) % 58.63/58.69 % Maximal formula atoms : 6 ( 2 avg) % 58.63/58.69 % Number of connectives : 55 ( 7 ~; 1 |; 30 &) % 58.63/58.69 % ( 2 <=>; 15 =>; 0 <=; 0 <~>) % 58.63/58.69 % Maximal formula depth : 9 ( 4 avg) % 58.63/58.69 % Maximal term depth : 2 ( 1 avg) % 58.63/58.69 % Number of predicates : 13 ( 12 usr; 0 prp; 1-2 aty) % 58.63/58.69 % Number of functors : 2 ( 2 usr; 1 con; 0-1 aty) % 58.63/58.69 % Number of variables : 44 ( 32 !; 12 ?) % 58.63/58.69 % SPC : FOF_THM_RFO_SEQ % 58.63/58.69 % 58.63/58.69 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 58.63/58.69 % library, www.mizar.org % 58.63/58.69 %------------------------------------------------------------------------------ % 58.63/58.69 fof(antisymmetry_r2_hidden,axiom, % 58.63/58.69 ! [A,B] : % 58.63/58.69 ( in(A,B) % 58.63/58.69 => ~ in(B,A) ) ). % 58.63/58.69 % 58.63/58.69 fof(cc1_funct_1,axiom, % 58.63/58.69 ! [A] : % 58.63/58.69 ( empty(A) % 58.63/58.69 => function(A) ) ). % 58.63/58.69 % 58.63/58.69 fof(cc1_ordinal1,axiom, % 58.63/58.69 ! [A] : % 58.63/58.69 ( ordinal(A) % 58.63/58.70 => ( epsilon_transitive(A) % 58.63/58.70 & epsilon_connected(A) ) ) ). % 58.63/58.70 % 58.63/58.70 fof(cc1_relat_1,axiom, % 58.63/58.70 ! [A] : % 58.63/58.70 ( empty(A) % 58.63/58.70 => relation(A) ) ). % 58.63/58.70 % 58.63/58.70 fof(cc2_funct_1,axiom, % 58.63/58.70 ! [A] : % 58.63/58.70 ( ( relation(A) % 58.63/58.70 & empty(A) % 58.63/58.70 & function(A) ) % 58.63/58.70 => ( relation(A) % 58.63/58.70 & function(A) % 58.63/58.70 & one_to_one(A) ) ) ). % 58.63/58.70 % 58.63/58.70 fof(cc2_ordinal1,axiom, % 58.63/58.70 ! [A] : % 58.63/58.70 ( ( epsilon_transitive(A) % 58.63/58.70 & epsilon_connected(A) ) % 58.63/58.70 => ordinal(A) ) ). % 58.63/58.70 % 58.63/58.70 fof(d2_ordinal1,axiom, % 58.63/58.70 ! [A] : % 58.63/58.70 ( epsilon_transitive(A) % 58.63/58.70 <=> ! [B] : % 58.63/58.70 ( in(B,A) % 58.63/58.70 => subset(B,A) ) ) ). % 58.63/58.70 % 58.63/58.70 fof(existence_m1_subset_1,axiom, % 58.63/58.70 ! [A] : % 58.63/58.70 ? [B] : element(B,A) ). % 58.63/58.70 % 58.63/58.70 fof(fc12_relat_1,axiom, % 58.63/58.70 ( empty(empty_set) % 58.63/58.70 & relation(empty_set) % 58.63/58.70 & relation_empty_yielding(empty_set) ) ). % 58.63/58.70 % 58.63/58.70 fof(fc1_xboole_0,axiom, % 58.63/58.70 empty(empty_set) ). % 58.63/58.70 % 58.63/58.70 fof(fc4_relat_1,axiom, % 58.63/58.70 ( empty(empty_set) % 58.63/58.70 & relation(empty_set) ) ). % 58.63/58.70 % 58.63/58.70 fof(rc1_funct_1,axiom, % 58.63/58.70 ? [A] : % 58.63/58.70 ( relation(A) % 58.63/58.70 & function(A) ) ). % 58.63/58.70 % 58.63/58.70 fof(rc1_ordinal1,axiom, % 58.63/58.70 ? [A] : % 58.63/58.70 ( epsilon_transitive(A) % 58.63/58.70 & epsilon_connected(A) % 58.63/58.70 & ordinal(A) ) ). % 58.63/58.70 % 58.63/58.70 fof(rc1_relat_1,axiom, % 58.63/58.70 ? [A] : % 58.63/58.70 ( empty(A) % 58.63/58.70 & relation(A) ) ). % 58.63/58.70 % 58.63/58.70 fof(rc1_xboole_0,axiom, % 58.63/58.70 ? [A] : empty(A) ). % 58.63/58.70 % 58.63/58.70 fof(rc2_funct_1,axiom, % 58.63/58.70 ? [A] : % 58.63/58.70 ( relation(A) % 58.63/58.70 & empty(A) % 58.63/58.70 & function(A) ) ). % 58.63/58.70 % 58.63/58.70 fof(rc2_relat_1,axiom, % 58.63/58.70 ? [A] : % 58.63/58.70 ( ~ empty(A) % 58.63/58.70 & relation(A) ) ). % 58.63/58.70 % 58.63/58.70 fof(rc2_xboole_0,axiom, % 58.63/58.70 ? [A] : ~ empty(A) ). % 58.63/58.70 % 58.63/58.70 fof(rc3_funct_1,axiom, % 58.63/58.70 ? [A] : % 58.63/58.70 ( relation(A) % 58.63/58.70 & function(A) % 58.63/58.70 & one_to_one(A) ) ). % 58.63/58.70 % 58.63/58.70 fof(rc3_relat_1,axiom, % 58.63/58.70 ? [A] : % 58.63/58.70 ( relation(A) % 58.63/58.70 & relation_empty_yielding(A) ) ). % 58.63/58.70 % 58.63/58.70 fof(rc4_funct_1,axiom, % 58.63/58.70 ? [A] : % 58.63/58.70 ( relation(A) % 58.63/58.70 & relation_empty_yielding(A) % 58.63/58.70 & function(A) ) ). % 58.63/58.70 % 58.63/58.70 fof(rc5_funct_1,axiom, % 58.63/58.70 ? [A] : % 58.63/58.70 ( relation(A) % 58.63/58.70 & relation_non_empty(A) % 58.63/58.70 & function(A) ) ). % 58.63/58.70 % 58.63/58.70 fof(reflexivity_r1_tarski,axiom, % 58.63/58.70 ! [A,B] : subset(A,A) ). % 58.63/58.70 % 58.63/58.70 fof(t19_ordinal1,conjecture, % 58.63/58.70 ! [A] : % 58.63/58.70 ( ordinal(A) % 58.63/58.70 => ! [B] : % 58.63/58.70 ( ordinal(B) % 58.63/58.70 => ! [C] : % 58.63/58.70 ( epsilon_transitive(C) % 58.63/58.70 => ( ( in(C,A) % 58.63/58.70 & in(A,B) ) % 58.63/58.70 => in(C,B) ) ) ) ) ). % 58.63/58.70 % 58.63/58.70 fof(t1_subset,axiom, % 58.63/58.70 ! [A,B] : % 58.63/58.70 ( in(A,B) % 58.63/58.70 => element(A,B) ) ). % 58.63/58.70 % 58.63/58.70 fof(t2_subset,axiom, % 58.63/58.70 ! [A,B] : % 58.63/58.70 ( element(A,B) % 58.63/58.70 => ( empty(B) % 58.63/58.70 | in(A,B) ) ) ). % 58.63/58.70 % 58.63/58.70 fof(t3_subset,axiom, % 58.63/58.70 ! [A,B] : % 58.63/58.70 ( element(A,powerset(B)) % 58.63/58.70 <=> subset(A,B) ) ). % 58.63/58.70 % 58.63/58.70 fof(t4_subset,axiom, % 58.63/58.70 ! [A,B,C] : % 58.63/58.70 ( ( in(A,B) % 58.63/58.70 & element(B,powerset(C)) ) % 58.63/58.70 => element(A,C) ) ). % 58.63/58.70 % 58.63/58.70 fof(t5_subset,axiom, % 58.63/58.70 ! [A,B,C] : % 58.63/58.70 ~ ( in(A,B) % 58.63/58.70 & element(B,powerset(C)) % 58.63/58.70 & empty(C) ) ). % 58.63/58.70 % 58.63/58.70 fof(t6_boole,axiom, % 58.63/58.70 ! [A] : % 58.63/58.70 ( empty(A) % 58.63/58.70 => A = empty_set ) ). % 58.63/58.70 % 58.63/58.70 fof(t7_boole,axiom, % 58.63/58.70 ! [A,B] : % 58.63/58.70 ~ ( in(A,B) % 58.63/58.70 & empty(B) ) ). % 58.63/58.70 % 58.63/58.70 fof(t8_boole,axiom, % 58.63/58.70 ! [A,B] : % 58.63/58.70 ~ ( empty(A) % 58.63/58.70 & A != B % 58.63/58.70 & empty(B) ) ). % 58.63/58.70 % 58.63/58.70 %------------------------------------------------------------------------------ % 58.63/58.70 %------------------------------------------- % 58.63/58.70 % Proof found % 58.63/58.70 % SZS status Theorem for theBenchmark % 58.63/58.70 % SZS output start Proof % 58.63/58.70 %ClaNum:79(EqnAxiom:21) % 58.63/58.70 %VarNum:71(SingletonVarNum:33) % 58.63/58.70 %MaxLitNum:4 % 58.63/58.70 %MaxfuncDepth:1 % 58.63/58.70 %SharedTerms:49 % 58.63/58.70 %goalClause: 34 35 37 54 55 60 % 58.63/58.70 %singleGoalClaCount:6 % 58.63/58.70 [24]P1(a1) % 58.63/58.70 [25]P1(a2) % 58.63/58.70 [26]P1(a14) % 58.63/58.70 [27]P1(a15) % 58.63/58.70 [28]P3(a3) % 58.63/58.70 [29]P3(a15) % 58.63/58.70 [30]P3(a4) % 58.63/58.70 [31]P3(a5) % 58.63/58.70 [32]P3(a7) % 58.63/58.70 [33]P6(a13) % 58.63/58.70 [34]P6(a8) % 58.63/58.70 [35]P6(a9) % 58.63/58.70 [36]P4(a13) % 58.63/58.70 [37]P4(a10) % 58.63/58.70 [38]P5(a13) % 58.63/58.70 [40]P9(a1) % 58.63/58.70 [41]P9(a3) % 58.63/58.70 [42]P9(a2) % 58.63/58.70 [43]P9(a15) % 58.63/58.70 [44]P9(a16) % 58.63/58.70 [45]P9(a4) % 58.63/58.70 [46]P9(a6) % 58.63/58.70 [47]P9(a5) % 58.63/58.70 [48]P9(a7) % 58.63/58.70 [49]P7(a4) % 58.63/58.70 [50]P10(a1) % 58.63/58.70 [51]P10(a6) % 58.63/58.70 [52]P10(a5) % 58.63/58.70 [53]P11(a7) % 58.63/58.70 [54]P8(a8,a9) % 58.63/58.70 [55]P8(a10,a8) % 58.63/58.70 [58]~P1(a16) % 58.63/58.70 [59]~P1(a17) % 58.63/58.70 [60]~P8(a10,a9) % 58.63/58.70 [56]P12(x561,x561) % 58.63/58.70 [57]P2(f11(x571),x571) % 58.63/58.70 [61]~P1(x611)+E(x611,a1) % 58.63/58.70 [62]~P1(x621)+P3(x621) % 58.63/58.70 [63]~P6(x631)+P4(x631) % 58.63/58.70 [64]~P6(x641)+P5(x641) % 58.63/58.70 [65]~P1(x651)+P9(x651) % 58.63/58.70 [68]P4(x681)+P8(f12(x681),x681) % 58.63/58.70 [71]P4(x711)+~P12(f12(x711),x711) % 58.63/58.70 [70]~P1(x701)+~P8(x702,x701) % 58.63/58.70 [72]~P8(x721,x722)+P2(x721,x722) % 58.63/58.70 [76]~P8(x762,x761)+~P8(x761,x762) % 58.63/58.70 [74]~P12(x741,x742)+P2(x741,f18(x742)) % 58.63/58.70 [77]P12(x771,x772)+~P2(x771,f18(x772)) % 58.63/58.70 [67]~P4(x671)+~P5(x671)+P6(x671) % 58.63/58.70 [66]~P1(x662)+~P1(x661)+E(x661,x662) % 58.63/58.70 [73]~P2(x732,x731)+P1(x731)+P8(x732,x731) % 58.63/58.70 [75]~P4(x752)+~P8(x751,x752)+P12(x751,x752) % 58.63/58.70 [78]~P1(x781)+~P8(x782,x783)+~P2(x783,f18(x781)) % 58.63/58.70 [79]P2(x791,x792)+~P8(x791,x793)+~P2(x793,f18(x792)) % 58.63/58.70 [69]~P1(x691)+~P3(x691)+~P9(x691)+P7(x691) % 58.63/58.70 %EqnAxiom % 58.63/58.70 [1]E(x11,x11) % 58.63/58.71 [2]E(x22,x21)+~E(x21,x22) % 58.63/58.71 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.63/58.71 [4]~E(x41,x42)+E(f11(x41),f11(x42)) % 58.63/58.71 [5]~E(x51,x52)+E(f12(x51),f12(x52)) % 58.63/58.71 [6]~E(x61,x62)+E(f18(x61),f18(x62)) % 58.63/58.71 [7]~P1(x71)+P1(x72)+~E(x71,x72) % 58.63/58.71 [8]P2(x82,x83)+~E(x81,x82)+~P2(x81,x83) % 58.63/58.71 [9]P2(x93,x92)+~E(x91,x92)+~P2(x93,x91) % 58.63/58.71 [10]P8(x102,x103)+~E(x101,x102)+~P8(x101,x103) % 58.63/58.71 [11]P8(x113,x112)+~E(x111,x112)+~P8(x113,x111) % 58.63/58.71 [12]~P9(x121)+P9(x122)+~E(x121,x122) % 58.63/58.71 [13]~P3(x131)+P3(x132)+~E(x131,x132) % 58.63/58.71 [14]P12(x142,x143)+~E(x141,x142)+~P12(x141,x143) % 58.63/58.71 [15]P12(x153,x152)+~E(x151,x152)+~P12(x153,x151) % 58.63/58.71 [16]~P11(x161)+P11(x162)+~E(x161,x162) % 58.63/58.71 [17]~P4(x171)+P4(x172)+~E(x171,x172) % 58.63/58.71 [18]~P10(x181)+P10(x182)+~E(x181,x182) % 58.63/58.71 [19]~P6(x191)+P6(x192)+~E(x191,x192) % 58.63/58.71 [20]~P7(x201)+P7(x202)+~E(x201,x202) % 58.63/58.71 [21]~P5(x211)+P5(x212)+~E(x211,x212) % 58.63/58.71 % 58.63/58.71 %------------------------------------------- % 58.63/58.71 cnf(80,plain, % 58.63/58.71 (~P8(x801,a1)), % 58.63/58.71 inference(scs_inference,[],[24,70])). % 58.63/58.71 cnf(82,plain, % 58.63/58.71 (~P8(a9,a8)), % 58.63/58.71 inference(scs_inference,[],[54,24,70,76])). % 58.63/58.71 cnf(86,plain, % 58.63/58.71 (P12(f11(f18(x861)),x861)), % 58.63/58.71 inference(scs_inference,[],[54,57,24,70,76,68,77])). % 58.63/58.71 cnf(87,plain, % 58.63/58.71 (P2(f11(x871),x871)), % 58.63/58.71 inference(rename_variables,[],[57])). % 58.63/58.71 cnf(89,plain, % 58.63/58.71 (P8(f11(a16),a16)), % 58.63/58.71 inference(scs_inference,[],[54,57,87,24,58,70,76,68,77,73])). % 58.63/58.71 cnf(90,plain, % 58.63/58.71 (P2(f11(x901),x901)), % 58.63/58.71 inference(rename_variables,[],[57])). % 58.63/58.71 cnf(93,plain, % 58.63/58.71 (P2(f11(x931),x931)), % 58.63/58.71 inference(rename_variables,[],[57])). % 58.63/58.71 cnf(96,plain, % 58.63/58.71 (~E(a9,f11(f18(a1)))), % 58.63/58.71 inference(scs_inference,[],[54,60,57,87,90,24,58,70,76,68,77,73,78,10,11])). % 58.63/58.71 cnf(100,plain, % 58.63/58.71 (P2(f11(x1001),x1001)), % 58.63/58.71 inference(rename_variables,[],[57])). % 58.63/58.71 cnf(104,plain, % 58.63/58.71 (P2(x1041,x1042)+~E(f11(x1042),x1041)), % 58.63/58.71 inference(scs_inference,[],[54,60,57,87,90,93,100,24,27,58,29,43,70,76,68,77,73,78,10,11,69,79,66,8])). % 58.63/58.71 cnf(106,plain, % 58.63/58.71 (P12(x1061,x1062)+~E(x1062,x1061)), % 58.63/58.71 inference(scs_inference,[],[54,60,57,87,90,93,100,24,27,58,56,29,43,70,76,68,77,73,78,10,11,69,79,66,8,9,14])). % 58.63/58.71 cnf(117,plain, % 58.63/58.71 (P2(f11(x1171),x1171)), % 58.63/58.71 inference(rename_variables,[],[57])). % 58.63/58.71 cnf(119,plain, % 58.63/58.71 (~P8(x1191,f11(f18(a2)))), % 58.63/58.71 inference(scs_inference,[],[55,25,59,57,117,70,76,73,78])). % 58.63/58.71 cnf(129,plain, % 58.63/58.71 (P12(f11(f18(x1291)),x1292)+~E(x1291,x1292)), % 58.63/58.71 inference(scs_inference,[],[55,60,96,82,86,25,59,57,117,70,76,73,78,11,10,68,66,14,15])). % 58.63/58.71 cnf(182,plain, % 58.63/58.71 (~P1(a9)), % 58.63/58.71 inference(scs_inference,[],[54,80,11,61])). % 58.63/58.71 cnf(184,plain, % 58.63/58.71 (~P2(a10,a9)), % 58.63/58.71 inference(scs_inference,[],[54,60,80,11,61,73])). % 58.63/58.71 cnf(232,plain, % 58.63/58.71 (P12(a8,a9)), % 58.63/58.71 inference(scs_inference,[],[35,54,63,75])). % 58.63/58.71 cnf(263,plain, % 58.63/58.71 (~E(x2631,x2632)+P2(x2632,f18(x2631))), % 58.63/58.71 inference(scs_inference,[],[74,106])). % 58.63/58.71 cnf(264,plain, % 58.63/58.71 (P2(x2641,f18(x2641))), % 58.63/58.71 inference(equality_inference,[],[263])). % 58.63/58.71 cnf(426,plain, % 58.63/58.71 (~E(a16,f11(f18(a2)))), % 58.63/58.71 inference(scs_inference,[],[119,89,11])). % 58.63/58.71 cnf(671,plain, % 58.63/58.71 (P12(a10,a8)), % 58.63/58.71 inference(scs_inference,[],[34,55,63,75])). % 58.63/58.71 cnf(3219,plain, % 58.63/58.71 (E(a1,a2)), % 58.63/58.71 inference(scs_inference,[],[25,61,2])). % 58.63/58.71 cnf(3222,plain, % 58.63/58.71 (E(a2,a1)), % 58.63/58.71 inference(scs_inference,[],[3219,129,106,2])). % 58.63/58.71 cnf(4131,plain, % 58.63/58.71 (P2(a8,a9)), % 58.63/58.71 inference(scs_inference,[],[54,72])). % 58.63/58.71 cnf(4146,plain, % 58.63/58.71 (P2(a8,x41461)+~E(a9,x41461)), % 58.63/58.71 inference(scs_inference,[],[426,4131,2,9])). % 58.63/58.71 cnf(4993,plain, % 58.63/58.71 (E(a15,a1)), % 58.63/58.71 inference(scs_inference,[],[671,27,3222,5,74,61])). % 58.63/58.71 cnf(5004,plain, % 58.63/58.71 (~P2(a8,f18(a9))), % 58.63/58.71 inference(scs_inference,[],[182,671,27,3222,26,184,55,57,5,74,61,106,65,4,6,2,73,79])). % 58.63/58.71 cnf(5021,plain, % 58.63/58.71 (P12(x50211,x50211)), % 58.63/58.71 inference(rename_variables,[],[56])). % 58.63/58.71 cnf(5024,plain, % 58.63/58.71 (E(a15,a2)), % 58.63/58.71 inference(scs_inference,[],[182,56,5021,671,264,89,24,27,3222,26,184,55,57,3219,5,74,61,106,65,4,6,2,73,79,78,9,263,4146,72,104,76,75,15,14,3])). % 58.63/58.71 cnf(5031,plain, % 58.63/58.71 ($false), % 58.63/58.71 inference(scs_inference,[],[4993,5024,5004,232,5,263,74]), % 58.63/58.71 ['proof']). % 58.63/58.71 % SZS output end Proof % 58.63/58.71 % Total time :58.050000s %------------------------------------------------------------------------------