%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM411+1 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n029.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 58.65s 58.68s % Output : CNFRefutation 58.65s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM411+1 : TPTP v8.2.0. Released v3.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n029.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 : Sat Jun 22 19:22:38 EDT 2024 % 0.12/0.33 % CPUTime : % 0.51/0.58 start to proof:theBenchmark % 58.59/58.66 %------------------------------------------- % 58.59/58.66 % File :CSE---1.7 % 58.59/58.66 % Problem :theBenchmark % 58.59/58.66 % Transform :cnf % 58.59/58.66 % Format :tptp:raw % 58.59/58.66 % Command :java -jar mcs_scs.jar %d %s % 58.59/58.66 % 58.59/58.66 % Result :Theorem 58.040000s % 58.59/58.66 % Output :CNFRefutation 58.040000s % 58.59/58.66 %------------------------------------------- % 58.65/58.67 %------------------------------------------------------------------------------ % 58.65/58.67 % File : NUM411+1 : TPTP v8.2.0. Released v3.2.0. % 58.65/58.67 % Domain : Number Theory (Ordinals) % 58.65/58.67 % Problem : Ordinal numbers, theorem 47 % 58.65/58.67 % Version : [Urb06] axioms : Especial. % 58.65/58.67 % English : % 58.65/58.67 % 58.65/58.67 % Refs : [Ban90] Bancerek (1990), The Ordinal Numbers % 58.65/58.67 % [Urb06] Urban (2006), Email to G. Sutcliffe % 58.65/58.67 % Source : [Urb06] % 58.65/58.67 % Names : ordinal1__t47_ordinal1 [Urb06] % 58.65/58.67 % 58.65/58.67 % Status : Theorem % 58.65/58.67 % Rating : 0.08 v8.1.0, 0.03 v7.1.0, 0.04 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.08 v6.1.0, 0.10 v6.0.0, 0.09 v5.5.0, 0.15 v5.4.0, 0.18 v5.3.0, 0.22 v5.2.0, 0.05 v5.1.0, 0.14 v5.0.0, 0.12 v4.1.0, 0.13 v4.0.1, 0.17 v4.0.0, 0.21 v3.7.0, 0.05 v3.4.0, 0.16 v3.3.0, 0.07 v3.2.0 % 58.65/58.67 % Syntax : Number of formulae : 43 ( 6 unt; 0 def) % 58.65/58.67 % Number of atoms : 123 ( 2 equ) % 58.65/58.67 % Maximal formula atoms : 8 ( 2 avg) % 58.65/58.67 % Number of connectives : 90 ( 10 ~; 1 |; 58 &) % 58.65/58.67 % ( 2 <=>; 19 =>; 0 <=; 0 <~>) % 58.65/58.67 % Maximal formula depth : 8 ( 4 avg) % 58.65/58.67 % Maximal term depth : 2 ( 1 avg) % 58.65/58.67 % Number of predicates : 16 ( 15 usr; 0 prp; 1-2 aty) % 58.65/58.67 % Number of functors : 3 ( 3 usr; 1 con; 0-1 aty) % 58.65/58.67 % Number of variables : 58 ( 42 !; 16 ?) % 58.65/58.67 % SPC : FOF_THM_RFO_SEQ % 58.65/58.67 % 58.65/58.67 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 58.65/58.67 % library, www.mizar.org % 58.65/58.67 %------------------------------------------------------------------------------ % 58.65/58.67 fof(antisymmetry_r2_hidden,axiom, % 58.65/58.67 ! [A,B] : % 58.65/58.67 ( in(A,B) % 58.65/58.67 => ~ in(B,A) ) ). % 58.65/58.67 % 58.65/58.67 fof(cc1_funct_1,axiom, % 58.65/58.67 ! [A] : % 58.65/58.67 ( empty(A) % 58.65/58.67 => function(A) ) ). % 58.65/58.67 % 58.65/58.67 fof(cc1_ordinal1,axiom, % 58.65/58.67 ! [A] : % 58.65/58.67 ( ordinal(A) % 58.65/58.67 => ( epsilon_transitive(A) % 58.65/58.67 & epsilon_connected(A) ) ) ). % 58.65/58.67 % 58.65/58.67 fof(cc1_relat_1,axiom, % 58.65/58.67 ! [A] : % 58.65/58.67 ( empty(A) % 58.65/58.67 => relation(A) ) ). % 58.65/58.67 % 58.65/58.67 fof(cc2_funct_1,axiom, % 58.65/58.67 ! [A] : % 58.65/58.67 ( ( relation(A) % 58.65/58.67 & empty(A) % 58.65/58.67 & function(A) ) % 58.65/58.67 => ( relation(A) % 58.65/58.67 & function(A) % 58.65/58.67 & one_to_one(A) ) ) ). % 58.65/58.67 % 58.65/58.67 fof(cc2_ordinal1,axiom, % 58.65/58.67 ! [A] : % 58.65/58.67 ( ( epsilon_transitive(A) % 58.65/58.67 & epsilon_connected(A) ) % 58.65/58.67 => ordinal(A) ) ). % 58.65/58.67 % 58.65/58.67 fof(cc3_ordinal1,axiom, % 58.65/58.67 ! [A] : % 58.65/58.67 ( empty(A) % 58.65/58.67 => ( epsilon_transitive(A) % 58.65/58.67 & epsilon_connected(A) % 58.65/58.67 & ordinal(A) ) ) ). % 58.65/58.67 % 58.65/58.67 fof(d8_ordinal1,axiom, % 58.65/58.67 ! [A,B] : % 58.65/58.67 ( ( relation(B) % 58.65/58.67 & function(B) % 58.65/58.67 & transfinite_sequence(B) ) % 58.65/58.67 => ( transfinite_sequence_of(B,A) % 58.65/58.67 <=> subset(relation_rng(B),A) ) ) ). % 58.65/58.67 % 58.65/58.67 fof(dt_m1_ordinal1,axiom, % 58.65/58.67 ! [A,B] : % 58.65/58.67 ( transfinite_sequence_of(B,A) % 58.65/58.67 => ( relation(B) % 58.65/58.67 & function(B) % 58.65/58.67 & transfinite_sequence(B) ) ) ). % 58.65/58.67 % 58.65/58.67 fof(existence_m1_ordinal1,axiom, % 58.65/58.67 ! [A] : % 58.65/58.67 ? [B] : transfinite_sequence_of(B,A) ). % 58.65/58.67 % 58.65/58.67 fof(existence_m1_subset_1,axiom, % 58.65/58.67 ! [A] : % 58.65/58.67 ? [B] : element(B,A) ). % 58.65/58.67 % 58.65/58.67 fof(fc12_relat_1,axiom, % 58.65/58.67 ( empty(empty_set) % 58.65/58.67 & relation(empty_set) % 58.65/58.67 & relation_empty_yielding(empty_set) ) ). % 58.65/58.67 % 58.65/58.67 fof(fc1_xboole_0,axiom, % 58.65/58.67 empty(empty_set) ). % 58.65/58.67 % 58.65/58.67 fof(fc2_ordinal1,axiom, % 58.65/58.67 ( relation(empty_set) % 58.65/58.67 & relation_empty_yielding(empty_set) % 58.65/58.67 & function(empty_set) % 58.65/58.67 & one_to_one(empty_set) % 58.65/58.67 & empty(empty_set) % 58.65/58.67 & epsilon_transitive(empty_set) % 58.65/58.67 & epsilon_connected(empty_set) % 58.65/58.67 & ordinal(empty_set) ) ). % 58.65/58.67 % 58.65/58.67 fof(fc4_relat_1,axiom, % 58.65/58.67 ( empty(empty_set) % 58.65/58.67 & relation(empty_set) ) ). % 58.65/58.67 % 58.65/58.67 fof(fc6_funct_1,axiom, % 58.65/58.67 ! [A] : % 58.65/58.67 ( ( relation(A) % 58.65/58.67 & relation_non_empty(A) % 58.65/58.67 & function(A) ) % 58.65/58.67 => with_non_empty_elements(relation_rng(A)) ) ). % 58.65/58.67 % 58.65/58.67 fof(fc6_relat_1,axiom, % 58.65/58.67 ! [A] : % 58.65/58.67 ( ( ~ empty(A) % 58.65/58.67 & relation(A) ) % 58.65/58.67 => ~ empty(relation_rng(A)) ) ). % 58.65/58.67 % 58.65/58.67 fof(fc8_relat_1,axiom, % 58.65/58.67 ! [A] : % 58.65/58.67 ( empty(A) % 58.65/58.67 => ( empty(relation_rng(A)) % 58.65/58.67 & relation(relation_rng(A)) ) ) ). % 58.65/58.67 % 58.65/58.67 fof(rc1_funct_1,axiom, % 58.65/58.67 ? [A] : % 58.65/58.67 ( relation(A) % 58.65/58.67 & function(A) ) ). % 58.65/58.67 % 58.65/58.67 fof(rc1_ordinal1,axiom, % 58.65/58.67 ? [A] : % 58.65/58.67 ( epsilon_transitive(A) % 58.65/58.67 & epsilon_connected(A) % 58.65/58.67 & ordinal(A) ) ). % 58.65/58.67 % 58.65/58.67 fof(rc1_relat_1,axiom, % 58.65/58.67 ? [A] : % 58.65/58.67 ( empty(A) % 58.65/58.67 & relation(A) ) ). % 58.65/58.67 % 58.65/58.67 fof(rc1_xboole_0,axiom, % 58.65/58.67 ? [A] : empty(A) ). % 58.65/58.67 % 58.65/58.67 fof(rc2_funct_1,axiom, % 58.65/58.67 ? [A] : % 58.65/58.67 ( relation(A) % 58.65/58.67 & empty(A) % 58.65/58.67 & function(A) ) ). % 58.65/58.67 % 58.65/58.67 fof(rc2_ordinal1,axiom, % 58.65/58.67 ? [A] : % 58.65/58.67 ( relation(A) % 58.65/58.67 & function(A) % 58.65/58.67 & one_to_one(A) % 58.65/58.67 & empty(A) % 58.65/58.67 & epsilon_transitive(A) % 58.65/58.67 & epsilon_connected(A) % 58.65/58.67 & ordinal(A) ) ). % 58.65/58.67 % 58.65/58.67 fof(rc2_relat_1,axiom, % 58.65/58.67 ? [A] : % 58.65/58.67 ( ~ empty(A) % 58.65/58.67 & relation(A) ) ). % 58.65/58.68 % 58.65/58.68 fof(rc2_xboole_0,axiom, % 58.65/58.68 ? [A] : ~ empty(A) ). % 58.65/58.68 % 58.65/58.68 fof(rc3_funct_1,axiom, % 58.65/58.68 ? [A] : % 58.65/58.68 ( relation(A) % 58.65/58.68 & function(A) % 58.65/58.68 & one_to_one(A) ) ). % 58.65/58.68 % 58.65/58.68 fof(rc3_ordinal1,axiom, % 58.65/58.68 ? [A] : % 58.65/58.68 ( ~ empty(A) % 58.65/58.68 & epsilon_transitive(A) % 58.65/58.68 & epsilon_connected(A) % 58.65/58.68 & ordinal(A) ) ). % 58.65/58.68 % 58.65/58.68 fof(rc3_relat_1,axiom, % 58.65/58.68 ? [A] : % 58.65/58.68 ( relation(A) % 58.65/58.68 & relation_empty_yielding(A) ) ). % 58.65/58.68 % 58.65/58.68 fof(rc4_funct_1,axiom, % 58.65/58.68 ? [A] : % 58.65/58.68 ( relation(A) % 58.65/58.68 & relation_empty_yielding(A) % 58.65/58.68 & function(A) ) ). % 58.65/58.68 % 58.65/58.68 fof(rc4_ordinal1,axiom, % 58.65/58.68 ? [A] : % 58.65/58.68 ( relation(A) % 58.65/58.68 & function(A) % 58.65/58.68 & transfinite_sequence(A) ) ). % 58.65/58.68 % 58.65/58.68 fof(rc5_funct_1,axiom, % 58.65/58.68 ? [A] : % 58.65/58.68 ( relation(A) % 58.65/58.68 & relation_non_empty(A) % 58.65/58.68 & function(A) ) ). % 58.65/58.68 % 58.65/58.68 fof(reflexivity_r1_tarski,axiom, % 58.65/58.68 ! [A,B] : subset(A,A) ). % 58.65/58.68 % 58.65/58.68 fof(t1_subset,axiom, % 58.65/58.68 ! [A,B] : % 58.65/58.68 ( in(A,B) % 58.65/58.68 => element(A,B) ) ). % 58.65/58.68 % 58.65/58.68 fof(t1_xboole_1,axiom, % 58.65/58.68 ! [A,B,C] : % 58.65/58.68 ( ( subset(A,B) % 58.65/58.68 & subset(B,C) ) % 58.65/58.68 => subset(A,C) ) ). % 58.65/58.68 % 58.65/58.68 fof(t2_subset,axiom, % 58.65/58.68 ! [A,B] : % 58.65/58.68 ( element(A,B) % 58.65/58.68 => ( empty(B) % 58.65/58.68 | in(A,B) ) ) ). % 58.65/58.68 % 58.65/58.68 fof(t3_subset,axiom, % 58.65/58.68 ! [A,B] : % 58.65/58.68 ( element(A,powerset(B)) % 58.65/58.68 <=> subset(A,B) ) ). % 58.65/58.68 % 58.65/58.68 fof(t47_ordinal1,conjecture, % 58.65/58.68 ! [A,B] : % 58.65/58.68 ( subset(A,B) % 58.65/58.68 => ! [C] : % 58.65/58.68 ( transfinite_sequence_of(C,A) % 58.65/58.68 => transfinite_sequence_of(C,B) ) ) ). % 58.65/58.68 % 58.65/58.68 fof(t4_subset,axiom, % 58.65/58.68 ! [A,B,C] : % 58.65/58.68 ( ( in(A,B) % 58.65/58.68 & element(B,powerset(C)) ) % 58.65/58.68 => element(A,C) ) ). % 58.65/58.68 % 58.65/58.68 fof(t5_subset,axiom, % 58.65/58.68 ! [A,B,C] : % 58.65/58.68 ~ ( in(A,B) % 58.65/58.68 & element(B,powerset(C)) % 58.65/58.68 & empty(C) ) ). % 58.65/58.68 % 58.65/58.68 fof(t6_boole,axiom, % 58.65/58.68 ! [A] : % 58.65/58.68 ( empty(A) % 58.65/58.68 => A = empty_set ) ). % 58.65/58.68 % 58.65/58.68 fof(t7_boole,axiom, % 58.65/58.68 ! [A,B] : % 58.65/58.68 ~ ( in(A,B) % 58.65/58.68 & empty(B) ) ). % 58.65/58.68 % 58.65/58.68 fof(t8_boole,axiom, % 58.65/58.68 ! [A,B] : % 58.65/58.68 ~ ( empty(A) % 58.65/58.68 & A != B % 58.65/58.68 & empty(B) ) ). % 58.65/58.68 % 58.65/58.68 %------------------------------------------------------------------------------ % 58.65/58.68 %------------------------------------------- % 58.65/58.68 % Proof found % 58.65/58.68 % SZS status Theorem for theBenchmark % 58.65/58.68 % SZS output start Proof % 58.65/58.68 %ClaNum:114(EqnAxiom:26) % 58.65/58.68 %VarNum:108(SingletonVarNum:50) % 58.65/58.68 %MaxLitNum:5 % 58.65/58.68 %MaxfuncDepth:1 % 58.65/58.68 %SharedTerms:68 % 58.65/58.68 %goalClause: 77 78 85 % 58.65/58.68 %singleGoalClaCount:3 % 58.65/58.68 [30]P1(a1) % 58.65/58.68 [31]P1(a2) % 58.65/58.68 [32]P1(a17) % 58.65/58.68 [33]P1(a18) % 58.65/58.68 [34]P1(a19) % 58.65/58.68 [35]P3(a1) % 58.65/58.68 [36]P3(a3) % 58.65/58.68 [37]P3(a18) % 58.65/58.68 [38]P3(a19) % 58.65/58.68 [39]P3(a4) % 58.65/58.68 [40]P3(a6) % 58.65/58.68 [41]P3(a9) % 58.65/58.68 [42]P3(a10) % 58.65/58.68 [43]P6(a1) % 58.65/58.68 [44]P6(a16) % 58.65/58.68 [45]P6(a19) % 58.65/58.68 [46]P6(a7) % 58.65/58.68 [47]P4(a1) % 58.65/58.68 [48]P4(a16) % 58.65/58.68 [49]P4(a19) % 58.65/58.68 [50]P4(a7) % 58.65/58.68 [51]P5(a1) % 58.65/58.68 [52]P5(a16) % 58.65/58.68 [53]P5(a19) % 58.65/58.68 [54]P5(a7) % 58.65/58.68 [57]P9(a1) % 58.65/58.68 [58]P9(a3) % 58.65/58.68 [59]P9(a2) % 58.65/58.68 [60]P9(a18) % 58.65/58.68 [61]P9(a19) % 58.65/58.68 [62]P9(a20) % 58.65/58.68 [63]P9(a4) % 58.65/58.68 [64]P9(a8) % 58.65/58.68 [65]P9(a6) % 58.65/58.68 [66]P9(a9) % 58.65/58.68 [67]P9(a10) % 58.65/58.68 [68]P7(a1) % 58.65/58.68 [69]P7(a19) % 58.65/58.68 [70]P7(a4) % 58.65/58.68 [71]P10(a9) % 58.65/58.68 [73]P11(a1) % 58.65/58.68 [74]P11(a8) % 58.65/58.68 [75]P11(a6) % 58.65/58.68 [76]P12(a10) % 58.65/58.68 [77]P14(a11,a12) % 58.65/58.68 [78]P13(a12,a13) % 58.65/58.68 [82]~P1(a20) % 58.65/58.68 [83]~P1(a5) % 58.65/58.68 [84]~P1(a7) % 58.65/58.68 [85]~P14(a11,a13) % 58.65/58.68 [79]P13(x791,x791) % 58.65/58.68 [80]P14(f14(x801),x801) % 58.65/58.68 [81]P2(f15(x811),x811) % 58.65/58.68 [86]~P1(x861)+E(x861,a1) % 58.65/58.68 [87]~P1(x871)+P3(x871) % 58.65/58.68 [88]~P1(x881)+P6(x881) % 58.65/58.68 [89]~P1(x891)+P4(x891) % 58.65/58.68 [90]~P6(x901)+P4(x901) % 58.65/58.68 [91]~P1(x911)+P5(x911) % 58.65/58.68 [92]~P6(x921)+P5(x921) % 58.65/58.68 [93]~P1(x931)+P9(x931) % 58.65/58.68 [95]~P1(x951)+P1(f21(x951)) % 58.65/58.68 [96]~P1(x961)+P9(f21(x961)) % 58.65/58.68 [99]P3(x991)+~P14(x991,x992) % 58.65/58.68 [100]P9(x1001)+~P14(x1001,x1002) % 58.65/58.68 [101]P10(x1011)+~P14(x1011,x1012) % 58.65/58.68 [103]~P1(x1031)+~P8(x1032,x1031) % 58.65/58.68 [105]~P8(x1051,x1052)+P2(x1051,x1052) % 58.65/58.68 [108]~P8(x1082,x1081)+~P8(x1081,x1082) % 58.65/58.68 [107]~P13(x1071,x1072)+P2(x1071,f22(x1072)) % 58.65/58.68 [109]P13(x1091,x1092)+~P2(x1091,f22(x1092)) % 58.65/58.68 [97]~P4(x971)+~P5(x971)+P6(x971) % 58.65/58.68 [102]~P9(x1021)+P1(x1021)+~P1(f21(x1021)) % 58.65/58.68 [94]~P1(x942)+~P1(x941)+E(x941,x942) % 58.65/58.68 [106]~P2(x1062,x1061)+P1(x1061)+P8(x1062,x1061) % 58.65/58.68 [110]~P13(x1101,x1103)+P13(x1101,x1102)+~P13(x1103,x1102) % 58.65/58.68 [111]~P1(x1111)+~P8(x1112,x1113)+~P2(x1113,f22(x1111)) % 58.65/58.68 [114]P2(x1141,x1142)+~P8(x1141,x1143)+~P2(x1143,f22(x1142)) % 58.65/58.68 [98]~P1(x981)+~P3(x981)+~P9(x981)+P7(x981) % 58.65/58.68 [104]~P3(x1041)+~P9(x1041)+~P12(x1041)+P15(f21(x1041)) % 58.65/58.68 [112]~P3(x1121)+~P9(x1121)+~P10(x1121)+~P14(x1121,x1122)+P13(f21(x1121),x1122) % 58.65/58.68 [113]~P3(x1131)+~P9(x1131)+~P10(x1131)+P14(x1131,x1132)+~P13(f21(x1131),x1132) % 58.65/58.68 %EqnAxiom % 58.65/58.68 [1]E(x11,x11) % 58.65/58.68 [2]E(x22,x21)+~E(x21,x22) % 58.65/58.68 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.65/58.68 [4]~E(x41,x42)+E(f14(x41),f14(x42)) % 58.65/58.68 [5]~E(x51,x52)+E(f15(x51),f15(x52)) % 58.65/58.68 [6]~E(x61,x62)+E(f21(x61),f21(x62)) % 58.65/58.68 [7]~E(x71,x72)+E(f22(x71),f22(x72)) % 58.65/58.68 [8]~P1(x81)+P1(x82)+~E(x81,x82) % 58.65/58.68 [9]P2(x92,x93)+~E(x91,x92)+~P2(x91,x93) % 58.65/58.68 [10]P2(x103,x102)+~E(x101,x102)+~P2(x103,x101) % 58.65/58.68 [11]P8(x112,x113)+~E(x111,x112)+~P8(x111,x113) % 58.65/58.68 [12]P8(x123,x122)+~E(x121,x122)+~P8(x123,x121) % 58.65/58.68 [13]~P15(x131)+P15(x132)+~E(x131,x132) % 58.65/58.68 [14]P13(x142,x143)+~E(x141,x142)+~P13(x141,x143) % 58.65/58.68 [15]P13(x153,x152)+~E(x151,x152)+~P13(x153,x151) % 58.65/58.68 [16]~P10(x161)+P10(x162)+~E(x161,x162) % 58.65/58.68 [17]~P9(x171)+P9(x172)+~E(x171,x172) % 58.65/58.68 [18]~P3(x181)+P3(x182)+~E(x181,x182) % 58.65/58.68 [19]P14(x192,x193)+~E(x191,x192)+~P14(x191,x193) % 58.65/58.68 [20]P14(x203,x202)+~E(x201,x202)+~P14(x203,x201) % 58.65/58.68 [21]~P4(x211)+P4(x212)+~E(x211,x212) % 58.65/58.68 [22]~P11(x221)+P11(x222)+~E(x221,x222) % 58.65/58.68 [23]~P5(x231)+P5(x232)+~E(x231,x232) % 58.65/58.68 [24]~P6(x241)+P6(x242)+~E(x241,x242) % 58.65/58.68 [25]~P7(x251)+P7(x252)+~E(x251,x252) % 58.65/58.68 [26]~P12(x261)+P12(x262)+~E(x261,x262) % 58.65/58.68 % 58.65/58.68 %------------------------------------------- % 58.65/58.68 cnf(116,plain, % 58.65/58.68 (P2(f15(x1161),x1161)), % 58.65/58.68 inference(rename_variables,[],[81])). % 58.65/58.68 cnf(122,plain, % 58.65/58.68 (~E(a12,a13)), % 58.65/58.68 inference(scs_inference,[],[77,85,80,30,81,109,103,19,20])). % 58.65/58.68 cnf(123,plain, % 58.65/58.68 (P8(f15(a20),a20)), % 58.65/58.68 inference(scs_inference,[],[77,85,80,30,82,81,116,109,103,19,20,106])). % 58.65/58.68 cnf(124,plain, % 58.65/58.68 (P2(f15(x1241),x1241)), % 58.65/58.68 inference(rename_variables,[],[81])). % 58.65/58.68 cnf(126,plain, % 58.65/58.68 (~P8(x1261,f15(f22(a1)))), % 58.65/58.68 inference(scs_inference,[],[77,85,80,30,82,81,116,124,109,103,19,20,106,111])). % 58.65/58.68 cnf(127,plain, % 58.65/58.68 (P2(f15(x1271),x1271)), % 58.65/58.68 inference(rename_variables,[],[81])). % 58.65/58.68 cnf(134,plain, % 58.65/58.68 (P13(x1341,a13)+~E(a12,x1341)), % 58.65/58.68 inference(scs_inference,[],[77,78,85,80,30,37,60,33,82,81,116,124,109,103,19,20,106,111,12,98,108,14])). % 58.65/58.68 cnf(139,plain, % 58.65/58.68 (P2(f15(x1391),x1391)), % 58.65/58.68 inference(rename_variables,[],[81])). % 58.65/58.68 cnf(142,plain, % 58.65/58.68 (P2(f15(x1421),x1422)+~E(x1421,x1422)), % 58.65/58.68 inference(scs_inference,[],[77,78,85,80,30,37,60,33,82,81,116,124,127,139,109,103,19,20,106,111,12,98,108,14,15,94,114,9,10])). % 58.65/58.68 cnf(149,plain, % 58.65/58.68 (P8(f15(a5),a5)), % 58.65/58.68 inference(scs_inference,[],[31,83,81,103,106])). % 58.65/58.68 cnf(160,plain, % 58.65/58.68 (P13(x1601,x1602)+~E(x1602,x1601)), % 58.65/58.68 inference(scs_inference,[],[77,122,79,126,123,31,83,81,103,106,12,108,11,19,94,14])). % 58.65/58.68 cnf(161,plain, % 58.65/58.68 (P14(f14(x1611),x1612)+~E(x1611,x1612)), % 58.65/58.68 inference(scs_inference,[],[77,122,79,126,123,80,31,83,81,103,106,12,108,11,19,94,14,20])). % 58.65/58.68 cnf(162,plain, % 58.65/58.68 (P13(x1621,x1622)+~E(x1621,x1622)), % 58.65/58.68 inference(scs_inference,[],[77,122,79,126,123,80,31,83,81,103,106,12,108,11,19,94,14,20,15])). % 58.65/58.68 cnf(172,plain, % 58.65/58.68 (P8(f15(a7),a7)), % 58.65/58.68 inference(scs_inference,[],[149,126,32,84,81,103,12,106])). % 58.65/58.68 cnf(276,plain, % 58.65/58.68 (E(f21(a17),a1)), % 58.65/58.68 inference(scs_inference,[],[32,86,95])). % 58.65/58.68 cnf(281,plain, % 58.65/58.68 (E(a1,f21(a17))), % 58.65/58.68 inference(scs_inference,[],[276,160,161,162,142,2])). % 58.65/58.68 cnf(363,plain, % 58.65/58.68 (~E(a11,x3631)+~P14(a11,a12)+P3(x3631)), % 58.65/58.68 inference(scs_inference,[],[77,99,18])). % 58.65/58.68 cnf(365,plain, % 58.65/58.68 (P3(x3651)+~E(a11,x3651)), % 58.65/58.68 inference(scs_inference,[],[77,363])). % 58.65/58.68 cnf(368,plain, % 58.65/58.68 (P3(a11)), % 58.65/58.68 inference(equality_inference,[],[365])). % 58.65/58.68 cnf(2871,plain, % 58.65/58.68 (P3(f21(a1))), % 58.65/58.68 inference(scs_inference,[],[30,87,95])). % 58.65/58.69 cnf(3382,plain, % 58.65/58.69 (P9(f21(a1))), % 58.65/58.69 inference(scs_inference,[],[30,93,95])). % 58.65/58.69 cnf(3383,plain, % 58.65/58.69 (P7(f21(a1))+~P1(f21(a1))), % 58.65/58.69 inference(scs_inference,[],[3382,2871,98])). % 58.65/58.69 cnf(4014,plain, % 58.65/58.69 (P10(a11)), % 58.65/58.69 inference(scs_inference,[],[77,101])). % 58.65/58.69 cnf(4054,plain, % 58.65/58.69 (P9(a11)), % 58.65/58.69 inference(scs_inference,[],[77,100])). % 58.65/58.69 cnf(5806,plain, % 58.65/58.69 (P1(f21(a19))), % 58.65/58.69 inference(scs_inference,[],[34,31,87,88,89,91,95])). % 58.65/58.69 cnf(5817,plain, % 58.65/58.69 (E(f15(a19),f15(a1))), % 58.65/58.69 inference(scs_inference,[],[34,31,32,79,87,88,89,91,95,96,107,93,86,7,5])). % 58.65/58.69 cnf(5818,plain, % 58.65/58.69 (P13(a1,a19)), % 58.65/58.69 inference(scs_inference,[],[34,31,32,79,87,88,89,91,95,96,107,93,86,7,5,160])). % 58.65/58.69 cnf(5819,plain, % 58.65/58.69 (~P2(a7,f22(a19))), % 58.65/58.69 inference(scs_inference,[],[34,31,32,79,172,87,88,89,91,95,96,107,93,86,7,5,160,111])). % 58.65/58.69 cnf(5827,plain, % 58.65/58.69 (P13(f21(a11),a12)), % 58.65/58.69 inference(scs_inference,[],[77,76,4014,4054,59,62,42,67,34,31,32,79,172,82,368,87,88,89,91,95,96,107,93,86,7,5,160,111,102,104,98,112])). % 58.65/58.69 cnf(5829,plain, % 58.65/58.69 (~P13(f21(a11),a13)), % 58.65/58.69 inference(scs_inference,[],[77,76,4014,4054,59,62,42,67,34,31,32,79,172,82,85,368,87,88,89,91,95,96,107,93,86,7,5,160,111,102,104,98,112,113])). % 58.65/58.69 cnf(5834,plain, % 58.65/58.69 (E(a1,a19)), % 58.65/58.69 inference(scs_inference,[],[77,76,4014,4054,59,62,42,67,34,31,32,79,172,82,85,368,87,88,89,91,95,96,107,93,86,7,5,160,111,102,104,98,112,113,134,4,6,2])). % 58.65/58.69 cnf(5839,plain, % 58.65/58.69 (P13(x58391,x58391)), % 58.65/58.69 inference(rename_variables,[],[79])). % 58.65/58.69 cnf(5841,plain, % 58.65/58.69 (P14(f14(x58411),x58411)), % 58.65/58.69 inference(rename_variables,[],[80])). % 58.65/58.69 cnf(5844,plain, % 58.65/58.69 (P2(f15(x58441),x58441)), % 58.65/58.69 inference(rename_variables,[],[81])). % 58.65/58.69 cnf(5852,plain, % 58.65/58.69 (P7(f21(a1))), % 58.65/58.69 inference(scs_inference,[],[77,76,4014,4054,59,62,42,67,34,80,5841,31,32,79,5839,172,82,85,81,5844,368,281,87,88,89,91,95,96,107,93,86,7,5,160,111,102,104,98,112,113,134,4,6,2,109,24,14,20,8,10,15,9,19,3,3383])). % 58.65/58.69 cnf(5883,plain, % 58.65/58.69 ($false), % 58.65/58.69 inference(scs_inference,[],[5818,5834,5806,5817,5852,5819,5827,5829,73,33,78,96,88,107,86,89,95,87,91,4,6,7,2,160,22,25,10,110]), % 58.65/58.69 ['proof']). % 58.65/58.69 % SZS output end Proof % 58.65/58.69 % Total time :58.040000s %------------------------------------------------------------------------------