%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM414+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 12:24:08 EDT 2024 % Result : Theorem 54.36s 54.50s % Output : CNFRefutation 54.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NUM414+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.11/0.34 % Computer : n021.cluster.edu % 0.11/0.34 % Model : x86_64 x86_64 % 0.11/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.34 % Memory : 8042.1875MB % 0.11/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.34 % CPULimit : 300 % 0.11/0.34 % WCLimit : 300 % 0.11/0.34 % DateTime : Sat Jun 22 21:05:24 EDT 2024 % 0.11/0.34 % CPUTime : % 0.19/0.57 start to proof:theBenchmark % 54.36/54.48 %------------------------------------------- % 54.36/54.48 % File :CSE---1.7 % 54.36/54.48 % Problem :theBenchmark % 54.36/54.48 % Transform :cnf % 54.36/54.48 % Format :tptp:raw % 54.36/54.48 % Command :java -jar mcs_scs.jar %d %s % 54.36/54.48 % 54.36/54.48 % Result :Theorem 53.870000s % 54.36/54.48 % Output :CNFRefutation 53.870000s % 54.36/54.48 %------------------------------------------- % 54.36/54.49 %------------------------------------------------------------------------------ % 54.36/54.49 % File : NUM414+1 : TPTP v8.2.0. Released v3.2.0. % 54.36/54.49 % Domain : Number Theory (Ordinals) % 54.36/54.49 % Problem : Ordinal numbers, theorem 50 % 54.36/54.49 % Version : [Urb06] axioms : Especial. % 54.36/54.49 % English : % 54.36/54.49 % 54.36/54.49 % Refs : [Ban89] Bancerek (1989), The Ordinal Numbers % 54.36/54.49 % [Urb06] Urban (2006), Email to G. Sutcliffe % 54.36/54.49 % Source : [Urb06] % 54.36/54.49 % Names : ordinal1__t50_ordinal1 [Urb06] % 54.36/54.49 % 54.36/54.49 % Status : Theorem % 54.36/54.49 % Rating : 0.17 v8.2.0, 0.14 v8.1.0, 0.08 v7.5.0, 0.09 v7.4.0, 0.10 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.08 v6.2.0, 0.12 v6.1.0, 0.13 v6.0.0, 0.09 v5.5.0, 0.11 v5.4.0, 0.18 v5.3.0, 0.22 v5.2.0, 0.05 v5.1.0, 0.10 v5.0.0, 0.12 v4.1.0, 0.17 v3.7.0, 0.05 v3.4.0, 0.11 v3.3.0, 0.07 v3.2.0 % 54.36/54.49 % Syntax : Number of formulae : 42 ( 6 unt; 0 def) % 54.36/54.49 % Number of atoms : 119 ( 4 equ) % 54.36/54.49 % Maximal formula atoms : 8 ( 2 avg) % 54.36/54.49 % Number of connectives : 92 ( 15 ~; 2 |; 55 &) % 54.36/54.49 % ( 3 <=>; 17 =>; 0 <=; 0 <~>) % 54.36/54.49 % Maximal formula depth : 9 ( 4 avg) % 54.36/54.49 % Maximal term depth : 2 ( 1 avg) % 54.36/54.49 % Number of predicates : 16 ( 15 usr; 0 prp; 1-2 aty) % 54.36/54.49 % Number of functors : 2 ( 2 usr; 1 con; 0-1 aty) % 54.36/54.49 % Number of variables : 57 ( 42 !; 15 ?) % 54.36/54.49 % SPC : FOF_THM_RFO_SEQ % 54.36/54.49 % 54.36/54.49 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 54.36/54.49 % library, www.mizar.org % 54.36/54.49 %------------------------------------------------------------------------------ % 54.36/54.49 fof(antisymmetry_r2_hidden,axiom, % 54.36/54.49 ! [A,B] : % 54.36/54.49 ( in(A,B) % 54.36/54.49 => ~ in(B,A) ) ). % 54.36/54.49 % 54.36/54.49 fof(antisymmetry_r2_xboole_0,axiom, % 54.36/54.49 ! [A,B] : % 54.36/54.49 ( proper_subset(A,B) % 54.36/54.49 => ~ proper_subset(B,A) ) ). % 54.36/54.49 % 54.36/54.49 fof(cc1_funct_1,axiom, % 54.36/54.49 ! [A] : % 54.36/54.49 ( empty(A) % 54.36/54.49 => function(A) ) ). % 54.36/54.49 % 54.36/54.49 fof(cc1_ordinal1,axiom, % 54.36/54.49 ! [A] : % 54.36/54.49 ( ordinal(A) % 54.36/54.49 => ( epsilon_transitive(A) % 54.36/54.49 & epsilon_connected(A) ) ) ). % 54.36/54.49 % 54.36/54.49 fof(cc1_relat_1,axiom, % 54.36/54.49 ! [A] : % 54.36/54.49 ( empty(A) % 54.36/54.49 => relation(A) ) ). % 54.36/54.49 % 54.36/54.49 fof(cc2_funct_1,axiom, % 54.36/54.49 ! [A] : % 54.36/54.50 ( ( relation(A) % 54.36/54.50 & empty(A) % 54.36/54.50 & function(A) ) % 54.36/54.50 => ( relation(A) % 54.36/54.50 & function(A) % 54.36/54.50 & one_to_one(A) ) ) ). % 54.36/54.50 % 54.36/54.50 fof(cc2_ordinal1,axiom, % 54.36/54.50 ! [A] : % 54.36/54.50 ( ( epsilon_transitive(A) % 54.36/54.50 & epsilon_connected(A) ) % 54.36/54.50 => ordinal(A) ) ). % 54.36/54.50 % 54.36/54.50 fof(cc3_ordinal1,axiom, % 54.36/54.50 ! [A] : % 54.36/54.50 ( empty(A) % 54.36/54.50 => ( epsilon_transitive(A) % 54.36/54.50 & epsilon_connected(A) % 54.36/54.50 & ordinal(A) ) ) ). % 54.36/54.50 % 54.36/54.50 fof(connectedness_r1_ordinal1,axiom, % 54.36/54.50 ! [A,B] : % 54.36/54.50 ( ( ordinal(A) % 54.36/54.50 & ordinal(B) ) % 54.36/54.50 => ( ordinal_subset(A,B) % 54.36/54.50 | ordinal_subset(B,A) ) ) ). % 54.36/54.50 % 54.36/54.50 fof(d8_xboole_0,axiom, % 54.36/54.50 ! [A,B] : % 54.36/54.50 ( proper_subset(A,B) % 54.36/54.50 <=> ( subset(A,B) % 54.36/54.50 & A != B ) ) ). % 54.36/54.50 % 54.36/54.50 fof(existence_m1_subset_1,axiom, % 54.36/54.50 ! [A] : % 54.36/54.50 ? [B] : element(B,A) ). % 54.36/54.50 % 54.36/54.50 fof(fc12_relat_1,axiom, % 54.36/54.50 ( empty(empty_set) % 54.36/54.50 & relation(empty_set) % 54.36/54.50 & relation_empty_yielding(empty_set) ) ). % 54.36/54.50 % 54.36/54.50 fof(fc1_xboole_0,axiom, % 54.36/54.50 empty(empty_set) ). % 54.36/54.50 % 54.36/54.50 fof(fc2_ordinal1,axiom, % 54.36/54.50 ( relation(empty_set) % 54.36/54.50 & relation_empty_yielding(empty_set) % 54.36/54.50 & function(empty_set) % 54.36/54.50 & one_to_one(empty_set) % 54.36/54.50 & empty(empty_set) % 54.36/54.50 & epsilon_transitive(empty_set) % 54.36/54.50 & epsilon_connected(empty_set) % 54.36/54.50 & ordinal(empty_set) ) ). % 54.36/54.50 % 54.36/54.50 fof(fc4_relat_1,axiom, % 54.36/54.50 ( empty(empty_set) % 54.36/54.50 & relation(empty_set) ) ). % 54.36/54.50 % 54.36/54.50 fof(irreflexivity_r2_xboole_0,axiom, % 54.36/54.50 ! [A,B] : ~ proper_subset(A,A) ). % 54.36/54.50 % 54.36/54.50 fof(rc1_funct_1,axiom, % 54.36/54.50 ? [A] : % 54.36/54.50 ( relation(A) % 54.36/54.50 & function(A) ) ). % 54.36/54.50 % 54.36/54.50 fof(rc1_ordinal1,axiom, % 54.36/54.50 ? [A] : % 54.36/54.50 ( epsilon_transitive(A) % 54.36/54.50 & epsilon_connected(A) % 54.36/54.50 & ordinal(A) ) ). % 54.36/54.50 % 54.36/54.50 fof(rc1_relat_1,axiom, % 54.36/54.50 ? [A] : % 54.36/54.50 ( empty(A) % 54.36/54.50 & relation(A) ) ). % 54.36/54.50 % 54.36/54.50 fof(rc1_xboole_0,axiom, % 54.36/54.50 ? [A] : empty(A) ). % 54.36/54.50 % 54.36/54.50 fof(rc2_funct_1,axiom, % 54.36/54.50 ? [A] : % 54.36/54.50 ( relation(A) % 54.36/54.50 & empty(A) % 54.36/54.50 & function(A) ) ). % 54.36/54.50 % 54.36/54.50 fof(rc2_ordinal1,axiom, % 54.36/54.50 ? [A] : % 54.36/54.50 ( relation(A) % 54.36/54.50 & function(A) % 54.36/54.50 & one_to_one(A) % 54.36/54.50 & empty(A) % 54.36/54.50 & epsilon_transitive(A) % 54.36/54.50 & epsilon_connected(A) % 54.36/54.50 & ordinal(A) ) ). % 54.36/54.50 % 54.36/54.50 fof(rc2_relat_1,axiom, % 54.36/54.50 ? [A] : % 54.36/54.50 ( ~ empty(A) % 54.36/54.50 & relation(A) ) ). % 54.36/54.50 % 54.36/54.50 fof(rc2_xboole_0,axiom, % 54.36/54.50 ? [A] : ~ empty(A) ). % 54.36/54.50 % 54.36/54.50 fof(rc3_funct_1,axiom, % 54.36/54.50 ? [A] : % 54.36/54.50 ( relation(A) % 54.36/54.50 & function(A) % 54.36/54.50 & one_to_one(A) ) ). % 54.36/54.50 % 54.36/54.50 fof(rc3_ordinal1,axiom, % 54.36/54.50 ? [A] : % 54.36/54.50 ( ~ empty(A) % 54.36/54.50 & epsilon_transitive(A) % 54.36/54.50 & epsilon_connected(A) % 54.36/54.50 & ordinal(A) ) ). % 54.36/54.50 % 54.36/54.50 fof(rc3_relat_1,axiom, % 54.36/54.50 ? [A] : % 54.36/54.50 ( relation(A) % 54.36/54.50 & relation_empty_yielding(A) ) ). % 54.36/54.50 % 54.36/54.50 fof(rc4_funct_1,axiom, % 54.36/54.50 ? [A] : % 54.36/54.50 ( relation(A) % 54.36/54.50 & relation_empty_yielding(A) % 54.36/54.50 & function(A) ) ). % 54.36/54.50 % 54.36/54.50 fof(rc4_ordinal1,axiom, % 54.36/54.50 ? [A] : % 54.36/54.50 ( relation(A) % 54.36/54.50 & function(A) % 54.36/54.50 & transfinite_sequence(A) ) ). % 54.36/54.50 % 54.36/54.50 fof(rc5_funct_1,axiom, % 54.36/54.50 ? [A] : % 54.36/54.50 ( relation(A) % 54.36/54.50 & relation_non_empty(A) % 54.36/54.50 & function(A) ) ). % 54.36/54.50 % 54.36/54.50 fof(redefinition_r1_ordinal1,axiom, % 54.36/54.50 ! [A,B] : % 54.36/54.50 ( ( ordinal(A) % 54.36/54.50 & ordinal(B) ) % 54.36/54.50 => ( ordinal_subset(A,B) % 54.36/54.50 <=> subset(A,B) ) ) ). % 54.36/54.50 % 54.36/54.50 fof(reflexivity_r1_ordinal1,axiom, % 54.36/54.50 ! [A,B] : % 54.36/54.50 ( ( ordinal(A) % 54.36/54.50 & ordinal(B) ) % 54.36/54.50 => ordinal_subset(A,A) ) ). % 54.36/54.50 % 54.36/54.50 fof(reflexivity_r1_tarski,axiom, % 54.36/54.50 ! [A,B] : subset(A,A) ). % 54.36/54.50 % 54.36/54.50 fof(t1_subset,axiom, % 54.36/54.50 ! [A,B] : % 54.36/54.50 ( in(A,B) % 54.36/54.50 => element(A,B) ) ). % 54.36/54.50 % 54.36/54.50 fof(t2_subset,axiom, % 54.36/54.50 ! [A,B] : % 54.36/54.50 ( element(A,B) % 54.36/54.50 => ( empty(B) % 54.36/54.50 | in(A,B) ) ) ). % 54.36/54.50 % 54.36/54.50 fof(t3_subset,axiom, % 54.36/54.50 ! [A,B] : % 54.36/54.50 ( element(A,powerset(B)) % 54.36/54.50 <=> subset(A,B) ) ). % 54.36/54.50 % 54.36/54.50 fof(t4_subset,axiom, % 54.36/54.50 ! [A,B,C] : % 54.36/54.50 ( ( in(A,B) % 54.36/54.50 & element(B,powerset(C)) ) % 54.36/54.50 => element(A,C) ) ). % 54.36/54.50 % 54.36/54.50 fof(t50_ordinal1,conjecture, % 54.36/54.50 ! [A] : % 54.36/54.50 ( ordinal(A) % 54.36/54.50 => ! [B] : % 54.36/54.50 ( ordinal(B) % 54.36/54.50 => ~ ( ~ proper_subset(A,B) % 54.36/54.50 & A != B % 54.36/54.50 & ~ proper_subset(B,A) ) ) ) ). % 54.36/54.50 % 54.36/54.50 fof(t5_subset,axiom, % 54.36/54.50 ! [A,B,C] : % 54.36/54.50 ~ ( in(A,B) % 54.36/54.50 & element(B,powerset(C)) % 54.36/54.50 & empty(C) ) ). % 54.36/54.50 % 54.36/54.50 fof(t6_boole,axiom, % 54.36/54.50 ! [A] : % 54.36/54.50 ( empty(A) % 54.36/54.50 => A = empty_set ) ). % 54.36/54.50 % 54.36/54.50 fof(t7_boole,axiom, % 54.36/54.50 ! [A,B] : % 54.36/54.50 ~ ( in(A,B) % 54.36/54.50 & empty(B) ) ). % 54.36/54.50 % 54.36/54.50 fof(t8_boole,axiom, % 54.36/54.50 ! [A,B] : % 54.36/54.50 ~ ( empty(A) % 54.36/54.50 & A != B % 54.36/54.50 & empty(B) ) ). % 54.36/54.50 % 54.36/54.50 %------------------------------------------------------------------------------ % 54.36/54.50 %------------------------------------------- % 54.36/54.50 % Proof found % 54.36/54.50 % SZS status Theorem for theBenchmark % 54.36/54.50 % SZS output start Proof % 54.36/54.50 %ClaNum:113(EqnAxiom:25) % 54.36/54.50 %VarNum:108(SingletonVarNum:49) % 54.36/54.50 %MaxLitNum:4 % 54.36/54.50 %MaxfuncDepth:1 % 54.36/54.50 %SharedTerms:69 % 54.36/54.50 %goalClause: 46 47 80 84 85 % 54.36/54.50 %singleGoalClaCount:5 % 54.36/54.50 [29]P1(a1) % 54.36/54.50 [30]P1(a2) % 54.36/54.50 [31]P1(a14) % 54.36/54.50 [32]P1(a15) % 54.36/54.50 [33]P1(a16) % 54.36/54.50 [34]P3(a1) % 54.36/54.50 [35]P3(a3) % 54.36/54.50 [36]P3(a15) % 54.36/54.50 [37]P3(a16) % 54.36/54.50 [38]P3(a4) % 54.36/54.50 [39]P3(a5) % 54.36/54.50 [40]P3(a8) % 54.36/54.50 [41]P3(a9) % 54.36/54.50 [42]P6(a1) % 54.36/54.50 [43]P6(a13) % 54.36/54.50 [44]P6(a16) % 54.36/54.50 [45]P6(a6) % 54.36/54.50 [46]P6(a10) % 54.36/54.50 [47]P6(a11) % 54.36/54.50 [48]P4(a1) % 54.36/54.50 [49]P4(a13) % 54.36/54.50 [50]P4(a16) % 54.36/54.50 [51]P4(a6) % 54.36/54.50 [52]P5(a1) % 54.36/54.50 [53]P5(a13) % 54.36/54.50 [54]P5(a16) % 54.36/54.50 [55]P5(a6) % 54.36/54.50 [58]P9(a1) % 54.36/54.50 [59]P9(a3) % 54.36/54.50 [60]P9(a2) % 54.36/54.50 [61]P9(a15) % 54.36/54.50 [62]P9(a16) % 54.36/54.50 [63]P9(a17) % 54.36/54.50 [64]P9(a4) % 54.36/54.50 [65]P9(a7) % 54.36/54.50 [66]P9(a5) % 54.36/54.50 [67]P9(a8) % 54.36/54.51 [68]P9(a9) % 54.36/54.51 [69]P7(a1) % 54.36/54.51 [70]P7(a16) % 54.36/54.51 [71]P7(a4) % 54.36/54.51 [73]P12(a1) % 54.36/54.51 [74]P12(a7) % 54.36/54.51 [75]P12(a5) % 54.36/54.51 [76]P13(a8) % 54.36/54.51 [77]P14(a9) % 54.36/54.51 [80]~E(a11,a10) % 54.36/54.51 [81]~P1(a17) % 54.36/54.51 [82]~P1(a18) % 54.36/54.51 [83]~P1(a6) % 54.36/54.51 [84]~P10(a10,a11) % 54.36/54.51 [85]~P10(a11,a10) % 54.36/54.51 [78]P15(x781,x781) % 54.36/54.51 [86]~P10(x861,x861) % 54.36/54.51 [79]P2(f12(x791),x791) % 54.36/54.51 [87]~P1(x871)+E(x871,a1) % 54.36/54.51 [88]~P1(x881)+P3(x881) % 54.36/54.51 [89]~P1(x891)+P6(x891) % 54.36/54.51 [90]~P1(x901)+P4(x901) % 54.36/54.51 [91]~P6(x911)+P4(x911) % 54.36/54.51 [92]~P1(x921)+P5(x921) % 54.36/54.51 [93]~P6(x931)+P5(x931) % 54.36/54.51 [94]~P1(x941)+P9(x941) % 54.36/54.51 [98]~P10(x981,x982)+~E(x981,x982) % 54.36/54.51 [100]~P1(x1001)+~P8(x1002,x1001) % 54.36/54.51 [101]~P10(x1011,x1012)+P15(x1011,x1012) % 54.36/54.51 [102]~P8(x1021,x1022)+P2(x1021,x1022) % 54.36/54.51 [107]~P8(x1072,x1071)+~P8(x1071,x1072) % 54.36/54.51 [108]~P10(x1082,x1081)+~P10(x1081,x1082) % 54.36/54.51 [105]~P15(x1051,x1052)+P2(x1051,f19(x1052)) % 54.36/54.51 [109]P15(x1091,x1092)+~P2(x1091,f19(x1092)) % 54.36/54.51 [96]~P4(x961)+~P5(x961)+P6(x961) % 54.36/54.51 [95]~P1(x952)+~P1(x951)+E(x951,x952) % 54.36/54.51 [99]~P6(x991)+P11(x991,x991)+~P6(x992) % 54.36/54.51 [103]P10(x1031,x1032)+~P15(x1031,x1032)+E(x1031,x1032) % 54.36/54.51 [104]~P2(x1042,x1041)+P1(x1041)+P8(x1042,x1041) % 54.36/54.51 [112]~P1(x1121)+~P8(x1122,x1123)+~P2(x1123,f19(x1121)) % 54.36/54.51 [113]P2(x1131,x1132)+~P8(x1131,x1133)+~P2(x1133,f19(x1132)) % 54.36/54.51 [97]~P1(x971)+~P3(x971)+~P9(x971)+P7(x971) % 54.36/54.51 [106]P11(x1062,x1061)+~P6(x1061)+~P6(x1062)+P11(x1061,x1062) % 54.36/54.51 [110]~P6(x1102)+~P6(x1101)+~P15(x1101,x1102)+P11(x1101,x1102) % 54.36/54.51 [111]~P6(x1112)+~P6(x1111)+~P11(x1111,x1112)+P15(x1111,x1112) % 54.36/54.51 %EqnAxiom % 54.36/54.51 [1]E(x11,x11) % 54.36/54.51 [2]E(x22,x21)+~E(x21,x22) % 54.36/54.51 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 54.36/54.51 [4]~E(x41,x42)+E(f12(x41),f12(x42)) % 54.36/54.51 [5]~E(x51,x52)+E(f19(x51),f19(x52)) % 54.36/54.51 [6]~P1(x61)+P1(x62)+~E(x61,x62) % 54.36/54.51 [7]P2(x72,x73)+~E(x71,x72)+~P2(x71,x73) % 54.36/54.51 [8]P2(x83,x82)+~E(x81,x82)+~P2(x83,x81) % 54.36/54.51 [9]P8(x92,x93)+~E(x91,x92)+~P8(x91,x93) % 54.36/54.51 [10]P8(x103,x102)+~E(x101,x102)+~P8(x103,x101) % 54.36/54.51 [11]P11(x112,x113)+~E(x111,x112)+~P11(x111,x113) % 54.36/54.51 [12]P11(x123,x122)+~E(x121,x122)+~P11(x123,x121) % 54.36/54.51 [13]P15(x132,x133)+~E(x131,x132)+~P15(x131,x133) % 54.36/54.51 [14]P15(x143,x142)+~E(x141,x142)+~P15(x143,x141) % 54.36/54.51 [15]~P6(x151)+P6(x152)+~E(x151,x152) % 54.36/54.51 [16]~P5(x161)+P5(x162)+~E(x161,x162) % 54.36/54.51 [17]~P4(x171)+P4(x172)+~E(x171,x172) % 54.36/54.51 [18]~P3(x181)+P3(x182)+~E(x181,x182) % 54.36/54.51 [19]~P13(x191)+P13(x192)+~E(x191,x192) % 54.36/54.51 [20]~P12(x201)+P12(x202)+~E(x201,x202) % 54.36/54.51 [21]~P9(x211)+P9(x212)+~E(x211,x212) % 54.36/54.51 [22]P10(x222,x223)+~E(x221,x222)+~P10(x221,x223) % 54.36/54.51 [23]P10(x233,x232)+~E(x231,x232)+~P10(x233,x231) % 54.36/54.51 [24]~P14(x241)+P14(x242)+~E(x241,x242) % 54.36/54.51 [25]~P7(x251)+P7(x252)+~E(x251,x252) % 54.36/54.51 % 54.36/54.51 %------------------------------------------- % 54.36/54.51 cnf(330,plain, % 54.36/54.51 (~P15(a10,a11)), % 54.36/54.51 inference(scs_inference,[],[80,84,2,103])). % 54.36/54.51 cnf(3021,plain, % 54.36/54.51 (~P11(a10,a11)), % 54.36/54.51 inference(scs_inference,[],[46,47,330,111])). % 54.36/54.51 cnf(3942,plain, % 54.36/54.51 (~P11(a11,a10)), % 54.36/54.51 inference(scs_inference,[],[80,46,47,85,103,111])). % 54.36/54.51 cnf(5879,plain, % 54.36/54.51 ($false), % 54.36/54.51 inference(scs_inference,[],[46,47,3942,3021,106]), % 54.36/54.51 ['proof']). % 54.36/54.51 % SZS output end Proof % 54.36/54.51 % Total time :53.870000s %------------------------------------------------------------------------------