%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM412+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 : 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 12:24:08 EDT 2024 % Result : Theorem 58.67s 58.75s % Output : CNFRefutation 58.67s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM412+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 : n026.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 00:08:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.20/0.57 start to proof:theBenchmark % 58.67/58.73 %------------------------------------------- % 58.67/58.73 % File :CSE---1.7 % 58.67/58.73 % Problem :theBenchmark % 58.67/58.73 % Transform :cnf % 58.67/58.73 % Format :tptp:raw % 58.67/58.73 % Command :java -jar mcs_scs.jar %d %s % 58.67/58.73 % 58.67/58.73 % Result :Theorem 58.110000s % 58.67/58.73 % Output :CNFRefutation 58.110000s % 58.67/58.73 %------------------------------------------- % 58.67/58.74 %------------------------------------------------------------------------------ % 58.67/58.74 % File : NUM412+1 : TPTP v8.2.0. Released v3.2.0. % 58.67/58.74 % Domain : Number Theory (Ordinals) % 58.67/58.74 % Problem : Ordinal numbers, theorem 48 % 58.67/58.74 % Version : [Urb06] axioms : Especial. % 58.67/58.74 % English : % 58.67/58.74 % 58.67/58.74 % Refs : [Ban90] Bancerek (1990), The Ordinal Numbers % 58.67/58.74 % [Urb06] Urban (2006), Email to G. Sutcliffe % 58.67/58.74 % Source : [Urb06] % 58.67/58.74 % Names : ordinal1__t48_ordinal1 [Urb06] % 58.67/58.74 % 58.67/58.74 % Status : Theorem % 58.67/58.74 % Rating : 0.14 v7.5.0, 0.16 v7.4.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.17 v6.2.0, 0.16 v6.1.0, 0.20 v6.0.0, 0.17 v5.5.0, 0.22 v5.4.0, 0.29 v5.3.0, 0.30 v5.2.0, 0.10 v5.1.0, 0.14 v5.0.0, 0.17 v4.1.0, 0.22 v4.0.1, 0.26 v4.0.0, 0.25 v3.7.0, 0.10 v3.5.0, 0.11 v3.4.0, 0.16 v3.3.0, 0.07 v3.2.0 % 58.67/58.74 % Syntax : Number of formulae : 48 ( 6 unt; 0 def) % 58.67/58.74 % Number of atoms : 143 ( 3 equ) % 58.67/58.74 % Maximal formula atoms : 8 ( 2 avg) % 58.67/58.74 % Number of connectives : 105 ( 10 ~; 1 |; 67 &) % 58.67/58.74 % ( 2 <=>; 25 =>; 0 <=; 0 <~>) % 58.67/58.74 % Maximal formula depth : 8 ( 4 avg) % 58.67/58.74 % Maximal term depth : 2 ( 1 avg) % 58.67/58.74 % Number of predicates : 16 ( 15 usr; 0 prp; 1-2 aty) % 58.67/58.74 % Number of functors : 5 ( 5 usr; 1 con; 0-2 aty) % 58.67/58.74 % Number of variables : 68 ( 52 !; 16 ?) % 58.67/58.74 % SPC : FOF_THM_RFO_SEQ % 58.67/58.74 % 58.67/58.74 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 58.67/58.74 % library, www.mizar.org % 58.67/58.74 %------------------------------------------------------------------------------ % 58.67/58.74 fof(antisymmetry_r2_hidden,axiom, % 58.67/58.74 ! [A,B] : % 58.67/58.74 ( in(A,B) % 58.67/58.74 => ~ in(B,A) ) ). % 58.67/58.74 % 58.67/58.74 fof(cc1_funct_1,axiom, % 58.67/58.74 ! [A] : % 58.67/58.74 ( empty(A) % 58.67/58.74 => function(A) ) ). % 58.67/58.74 % 58.67/58.74 fof(cc1_ordinal1,axiom, % 58.67/58.74 ! [A] : % 58.67/58.74 ( ordinal(A) % 58.67/58.74 => ( epsilon_transitive(A) % 58.67/58.74 & epsilon_connected(A) ) ) ). % 58.67/58.74 % 58.67/58.74 fof(cc1_relat_1,axiom, % 58.67/58.74 ! [A] : % 58.67/58.74 ( empty(A) % 58.67/58.74 => relation(A) ) ). % 58.67/58.74 % 58.67/58.74 fof(cc2_funct_1,axiom, % 58.67/58.74 ! [A] : % 58.67/58.74 ( ( relation(A) % 58.67/58.74 & empty(A) % 58.67/58.74 & function(A) ) % 58.67/58.74 => ( relation(A) % 58.67/58.74 & function(A) % 58.67/58.74 & one_to_one(A) ) ) ). % 58.67/58.74 % 58.67/58.74 fof(cc2_ordinal1,axiom, % 58.67/58.74 ! [A] : % 58.67/58.74 ( ( epsilon_transitive(A) % 58.67/58.74 & epsilon_connected(A) ) % 58.67/58.74 => ordinal(A) ) ). % 58.67/58.74 % 58.67/58.74 fof(cc3_ordinal1,axiom, % 58.67/58.74 ! [A] : % 58.67/58.74 ( empty(A) % 58.67/58.74 => ( epsilon_transitive(A) % 58.67/58.74 & epsilon_connected(A) % 58.67/58.74 & ordinal(A) ) ) ). % 58.67/58.74 % 58.67/58.74 fof(d8_ordinal1,axiom, % 58.67/58.74 ! [A,B] : % 58.67/58.74 ( ( relation(B) % 58.67/58.74 & function(B) % 58.67/58.74 & transfinite_sequence(B) ) % 58.67/58.74 => ( transfinite_sequence_of(B,A) % 58.67/58.74 <=> subset(relation_rng(B),A) ) ) ). % 58.67/58.74 % 58.67/58.74 fof(dt_k2_ordinal1,axiom, % 58.67/58.74 ! [A,B] : % 58.67/58.74 ( ( relation(A) % 58.67/58.74 & function(A) % 58.67/58.74 & transfinite_sequence(A) % 58.67/58.74 & ordinal(B) ) % 58.67/58.74 => transfinite_sequence_of(tseq_dom_restriction(A,B),relation_rng(A)) ) ). % 58.67/58.74 % 58.67/58.74 fof(dt_k7_relat_1,axiom, % 58.67/58.74 ! [A,B] : % 58.67/58.74 ( relation(A) % 58.67/58.74 => relation(relation_dom_restriction(A,B)) ) ). % 58.67/58.74 % 58.67/58.74 fof(dt_m1_ordinal1,axiom, % 58.67/58.74 ! [A,B] : % 58.67/58.74 ( transfinite_sequence_of(B,A) % 58.67/58.74 => ( relation(B) % 58.67/58.74 & function(B) % 58.67/58.74 & transfinite_sequence(B) ) ) ). % 58.67/58.74 % 58.67/58.74 fof(existence_m1_ordinal1,axiom, % 58.67/58.74 ! [A] : % 58.67/58.74 ? [B] : transfinite_sequence_of(B,A) ). % 58.67/58.74 % 58.67/58.74 fof(existence_m1_subset_1,axiom, % 58.67/58.74 ! [A] : % 58.67/58.74 ? [B] : element(B,A) ). % 58.67/58.74 % 58.67/58.74 fof(fc12_relat_1,axiom, % 58.67/58.74 ( empty(empty_set) % 58.67/58.74 & relation(empty_set) % 58.67/58.74 & relation_empty_yielding(empty_set) ) ). % 58.67/58.74 % 58.67/58.74 fof(fc13_relat_1,axiom, % 58.67/58.74 ! [A,B] : % 58.67/58.74 ( ( relation(A) % 58.67/58.74 & relation_empty_yielding(A) ) % 58.67/58.74 => ( relation(relation_dom_restriction(A,B)) % 58.67/58.74 & relation_empty_yielding(relation_dom_restriction(A,B)) ) ) ). % 58.67/58.74 % 58.67/58.74 fof(fc1_xboole_0,axiom, % 58.67/58.74 empty(empty_set) ). % 58.67/58.74 % 58.67/58.74 fof(fc2_ordinal1,axiom, % 58.67/58.74 ( relation(empty_set) % 58.67/58.74 & relation_empty_yielding(empty_set) % 58.67/58.74 & function(empty_set) % 58.67/58.74 & one_to_one(empty_set) % 58.67/58.74 & empty(empty_set) % 58.67/58.74 & epsilon_transitive(empty_set) % 58.67/58.74 & epsilon_connected(empty_set) % 58.67/58.74 & ordinal(empty_set) ) ). % 58.67/58.74 % 58.67/58.74 fof(fc4_funct_1,axiom, % 58.67/58.74 ! [A,B] : % 58.67/58.74 ( ( relation(A) % 58.67/58.74 & function(A) ) % 58.67/58.74 => ( relation(relation_dom_restriction(A,B)) % 58.67/58.74 & function(relation_dom_restriction(A,B)) ) ) ). % 58.67/58.74 % 58.67/58.74 fof(fc4_relat_1,axiom, % 58.67/58.74 ( empty(empty_set) % 58.67/58.74 & relation(empty_set) ) ). % 58.67/58.74 % 58.67/58.74 fof(fc6_funct_1,axiom, % 58.67/58.74 ! [A] : % 58.67/58.74 ( ( relation(A) % 58.67/58.74 & relation_non_empty(A) % 58.67/58.74 & function(A) ) % 58.67/58.74 => with_non_empty_elements(relation_rng(A)) ) ). % 58.67/58.74 % 58.67/58.74 fof(fc6_relat_1,axiom, % 58.67/58.74 ! [A] : % 58.67/58.74 ( ( ~ empty(A) % 58.67/58.74 & relation(A) ) % 58.67/58.74 => ~ empty(relation_rng(A)) ) ). % 58.67/58.74 % 58.67/58.74 fof(fc8_relat_1,axiom, % 58.67/58.74 ! [A] : % 58.67/58.74 ( empty(A) % 58.67/58.75 => ( empty(relation_rng(A)) % 58.67/58.75 & relation(relation_rng(A)) ) ) ). % 58.67/58.75 % 58.67/58.75 fof(rc1_funct_1,axiom, % 58.67/58.75 ? [A] : % 58.67/58.75 ( relation(A) % 58.67/58.75 & function(A) ) ). % 58.67/58.75 % 58.67/58.75 fof(rc1_ordinal1,axiom, % 58.67/58.75 ? [A] : % 58.67/58.75 ( epsilon_transitive(A) % 58.67/58.75 & epsilon_connected(A) % 58.67/58.75 & ordinal(A) ) ). % 58.67/58.75 % 58.67/58.75 fof(rc1_relat_1,axiom, % 58.67/58.75 ? [A] : % 58.67/58.75 ( empty(A) % 58.67/58.75 & relation(A) ) ). % 58.67/58.75 % 58.67/58.75 fof(rc1_xboole_0,axiom, % 58.67/58.75 ? [A] : empty(A) ). % 58.67/58.75 % 58.67/58.75 fof(rc2_funct_1,axiom, % 58.67/58.75 ? [A] : % 58.67/58.75 ( relation(A) % 58.67/58.75 & empty(A) % 58.67/58.75 & function(A) ) ). % 58.67/58.75 % 58.67/58.75 fof(rc2_ordinal1,axiom, % 58.67/58.75 ? [A] : % 58.67/58.75 ( relation(A) % 58.67/58.75 & function(A) % 58.67/58.75 & one_to_one(A) % 58.67/58.75 & empty(A) % 58.67/58.75 & epsilon_transitive(A) % 58.67/58.75 & epsilon_connected(A) % 58.67/58.75 & ordinal(A) ) ). % 58.67/58.75 % 58.67/58.75 fof(rc2_relat_1,axiom, % 58.67/58.75 ? [A] : % 58.67/58.75 ( ~ empty(A) % 58.67/58.75 & relation(A) ) ). % 58.67/58.75 % 58.67/58.75 fof(rc2_xboole_0,axiom, % 58.67/58.75 ? [A] : ~ empty(A) ). % 58.67/58.75 % 58.67/58.75 fof(rc3_funct_1,axiom, % 58.67/58.75 ? [A] : % 58.67/58.75 ( relation(A) % 58.67/58.75 & function(A) % 58.67/58.75 & one_to_one(A) ) ). % 58.67/58.75 % 58.67/58.75 fof(rc3_ordinal1,axiom, % 58.67/58.75 ? [A] : % 58.67/58.75 ( ~ empty(A) % 58.67/58.75 & epsilon_transitive(A) % 58.67/58.75 & epsilon_connected(A) % 58.67/58.75 & ordinal(A) ) ). % 58.67/58.75 % 58.67/58.75 fof(rc3_relat_1,axiom, % 58.67/58.75 ? [A] : % 58.67/58.75 ( relation(A) % 58.67/58.75 & relation_empty_yielding(A) ) ). % 58.67/58.75 % 58.67/58.75 fof(rc4_funct_1,axiom, % 58.67/58.75 ? [A] : % 58.67/58.75 ( relation(A) % 58.67/58.75 & relation_empty_yielding(A) % 58.67/58.75 & function(A) ) ). % 58.67/58.75 % 58.67/58.75 fof(rc4_ordinal1,axiom, % 58.67/58.75 ? [A] : % 58.67/58.75 ( relation(A) % 58.67/58.75 & function(A) % 58.67/58.75 & transfinite_sequence(A) ) ). % 58.67/58.75 % 58.67/58.75 fof(rc5_funct_1,axiom, % 58.67/58.75 ? [A] : % 58.67/58.75 ( relation(A) % 58.67/58.75 & relation_non_empty(A) % 58.67/58.75 & function(A) ) ). % 58.67/58.75 % 58.67/58.75 fof(redefinition_k2_ordinal1,axiom, % 58.67/58.75 ! [A,B] : % 58.67/58.75 ( ( relation(A) % 58.67/58.75 & function(A) % 58.67/58.75 & transfinite_sequence(A) % 58.67/58.75 & ordinal(B) ) % 58.67/58.75 => tseq_dom_restriction(A,B) = relation_dom_restriction(A,B) ) ). % 58.67/58.75 % 58.67/58.75 fof(reflexivity_r1_tarski,axiom, % 58.67/58.75 ! [A,B] : subset(A,A) ). % 58.67/58.75 % 58.67/58.75 fof(t1_subset,axiom, % 58.67/58.75 ! [A,B] : % 58.67/58.75 ( in(A,B) % 58.67/58.75 => element(A,B) ) ). % 58.67/58.75 % 58.67/58.75 fof(t2_subset,axiom, % 58.67/58.75 ! [A,B] : % 58.67/58.75 ( element(A,B) % 58.67/58.75 => ( empty(B) % 58.67/58.75 | in(A,B) ) ) ). % 58.67/58.75 % 58.67/58.75 fof(t3_subset,axiom, % 58.67/58.75 ! [A,B] : % 58.67/58.75 ( element(A,powerset(B)) % 58.67/58.75 <=> subset(A,B) ) ). % 58.67/58.75 % 58.67/58.75 fof(t47_ordinal1,axiom, % 58.67/58.75 ! [A,B] : % 58.67/58.75 ( subset(A,B) % 58.67/58.75 => ! [C] : % 58.67/58.75 ( transfinite_sequence_of(C,A) % 58.67/58.75 => transfinite_sequence_of(C,B) ) ) ). % 58.67/58.75 % 58.67/58.75 fof(t48_ordinal1,conjecture, % 58.67/58.75 ! [A,B] : % 58.67/58.75 ( transfinite_sequence_of(B,A) % 58.67/58.75 => ! [C] : % 58.67/58.75 ( ordinal(C) % 58.67/58.75 => transfinite_sequence_of(tseq_dom_restriction(B,C),A) ) ) ). % 58.67/58.75 % 58.67/58.75 fof(t4_subset,axiom, % 58.67/58.75 ! [A,B,C] : % 58.67/58.75 ( ( in(A,B) % 58.67/58.75 & element(B,powerset(C)) ) % 58.67/58.75 => element(A,C) ) ). % 58.67/58.75 % 58.67/58.75 fof(t5_subset,axiom, % 58.67/58.75 ! [A,B,C] : % 58.67/58.75 ~ ( in(A,B) % 58.67/58.75 & element(B,powerset(C)) % 58.67/58.75 & empty(C) ) ). % 58.67/58.75 % 58.67/58.75 fof(t6_boole,axiom, % 58.67/58.75 ! [A] : % 58.67/58.75 ( empty(A) % 58.67/58.75 => A = empty_set ) ). % 58.67/58.75 % 58.67/58.75 fof(t7_boole,axiom, % 58.67/58.75 ! [A,B] : % 58.67/58.75 ~ ( in(A,B) % 58.67/58.75 & empty(B) ) ). % 58.67/58.75 % 58.67/58.75 fof(t8_boole,axiom, % 58.67/58.75 ! [A,B] : % 58.67/58.75 ~ ( empty(A) % 58.67/58.75 & A != B % 58.67/58.75 & empty(B) ) ). % 58.67/58.75 % 58.67/58.75 %------------------------------------------------------------------------------ % 58.67/58.75 %------------------------------------------- % 58.67/58.75 % Proof found % 58.67/58.75 % SZS status Theorem for theBenchmark % 58.67/58.75 % SZS output start Proof % 58.67/58.75 %ClaNum:125(EqnAxiom:30) % 58.67/58.75 %VarNum:134(SingletonVarNum:60) % 58.67/58.75 %MaxLitNum:5 % 58.67/58.75 %MaxfuncDepth:1 % 58.67/58.75 %SharedTerms:69 % 58.67/58.75 %goalClause: 51 82 89 % 58.67/58.75 %singleGoalClaCount:3 % 58.67/58.75 [34]P1(a1) % 58.67/58.75 [35]P1(a2) % 58.67/58.75 [36]P1(a17) % 58.67/58.75 [37]P1(a18) % 58.67/58.75 [38]P1(a19) % 58.67/58.75 [39]P3(a1) % 58.67/58.75 [40]P3(a3) % 58.67/58.75 [41]P3(a18) % 58.67/58.75 [42]P3(a19) % 58.67/58.75 [43]P3(a4) % 58.67/58.75 [44]P3(a6) % 58.67/58.75 [45]P3(a9) % 58.67/58.75 [46]P3(a10) % 58.67/58.75 [47]P6(a1) % 58.67/58.75 [48]P6(a16) % 58.67/58.75 [49]P6(a19) % 58.67/58.75 [50]P6(a7) % 58.67/58.75 [51]P6(a11) % 58.67/58.75 [52]P4(a1) % 58.67/58.75 [53]P4(a16) % 58.67/58.75 [54]P4(a19) % 58.67/58.75 [55]P4(a7) % 58.67/58.75 [56]P5(a1) % 58.67/58.75 [57]P5(a16) % 58.67/58.75 [58]P5(a19) % 58.67/58.75 [59]P5(a7) % 58.67/58.75 [62]P9(a1) % 58.67/58.75 [63]P9(a3) % 58.67/58.75 [64]P9(a2) % 58.67/58.75 [65]P9(a18) % 58.67/58.75 [66]P9(a19) % 58.67/58.75 [67]P9(a20) % 58.67/58.75 [68]P9(a4) % 58.67/58.75 [69]P9(a8) % 58.67/58.75 [70]P9(a6) % 58.67/58.75 [71]P9(a9) % 58.67/58.75 [72]P9(a10) % 58.67/58.75 [73]P7(a1) % 58.67/58.75 [74]P7(a19) % 58.67/58.75 [75]P7(a4) % 58.67/58.75 [76]P10(a9) % 58.67/58.75 [78]P11(a1) % 58.67/58.75 [79]P11(a8) % 58.67/58.75 [80]P11(a6) % 58.67/58.75 [81]P12(a10) % 58.67/58.75 [82]P14(a12,a13) % 58.67/58.75 [86]~P1(a20) % 58.67/58.75 [87]~P1(a5) % 58.67/58.75 [88]~P1(a7) % 58.67/58.75 [89]~P14(f21(a12,a11),a13) % 58.67/58.75 [83]P13(x831,x831) % 58.67/58.75 [84]P14(f14(x841),x841) % 58.67/58.75 [85]P2(f15(x851),x851) % 58.67/58.75 [90]~P1(x901)+E(x901,a1) % 58.67/58.75 [91]~P1(x911)+P3(x911) % 58.67/58.75 [92]~P1(x921)+P6(x921) % 58.67/58.75 [93]~P1(x931)+P4(x931) % 58.67/58.75 [94]~P6(x941)+P4(x941) % 58.67/58.75 [95]~P1(x951)+P5(x951) % 58.67/58.75 [96]~P6(x961)+P5(x961) % 58.67/58.75 [97]~P1(x971)+P9(x971) % 58.67/58.75 [99]~P1(x991)+P1(f22(x991)) % 58.67/58.75 [100]~P1(x1001)+P9(f22(x1001)) % 58.67/58.75 [103]P3(x1031)+~P14(x1031,x1032) % 58.67/58.75 [104]P9(x1041)+~P14(x1041,x1042) % 58.67/58.75 [105]P10(x1051)+~P14(x1051,x1052) % 58.67/58.75 [107]~P1(x1071)+~P8(x1072,x1071) % 58.67/58.75 [109]~P8(x1091,x1092)+P2(x1091,x1092) % 58.67/58.75 [117]~P8(x1172,x1171)+~P8(x1171,x1172) % 58.67/58.75 [110]~P9(x1101)+P9(f23(x1101,x1102)) % 58.67/58.75 [112]~P13(x1121,x1122)+P2(x1121,f24(x1122)) % 58.67/58.75 [118]P13(x1181,x1182)+~P2(x1181,f24(x1182)) % 58.67/58.75 [101]~P4(x1011)+~P5(x1011)+P6(x1011) % 58.67/58.75 [106]~P9(x1061)+P1(x1061)+~P1(f22(x1061)) % 58.67/58.75 [98]~P1(x982)+~P1(x981)+E(x981,x982) % 58.67/58.75 [111]~P2(x1112,x1111)+P1(x1111)+P8(x1112,x1111) % 58.67/58.75 [113]~P3(x1131)+~P9(x1131)+P3(f23(x1131,x1132)) % 58.67/58.75 [116]~P9(x1161)+~P11(x1161)+P11(f23(x1161,x1162)) % 58.67/58.75 [120]~P13(x1203,x1202)+P14(x1201,x1202)+~P14(x1201,x1203) % 58.67/58.75 [121]~P1(x1211)+~P8(x1212,x1213)+~P2(x1213,f24(x1211)) % 58.67/58.75 [124]P2(x1241,x1242)+~P8(x1241,x1243)+~P2(x1243,f24(x1242)) % 58.67/58.75 [102]~P1(x1021)+~P3(x1021)+~P9(x1021)+P7(x1021) % 58.67/58.75 [108]~P3(x1081)+~P9(x1081)+~P12(x1081)+P15(f22(x1081)) % 58.67/58.75 [119]~P3(x1191)+~P6(x1192)+~P9(x1191)+~P10(x1191)+E(f21(x1191,x1192),f23(x1191,x1192)) % 58.67/58.75 [122]~P3(x1221)+~P9(x1221)+~P10(x1221)+~P14(x1221,x1222)+P13(f22(x1221),x1222) % 58.67/58.75 [123]~P3(x1231)+~P9(x1231)+~P10(x1231)+P14(x1231,x1232)+~P13(f22(x1231),x1232) % 58.67/58.75 [125]~P3(x1251)+~P6(x1252)+~P9(x1251)+~P10(x1251)+P14(f21(x1251,x1252),f22(x1251)) % 58.67/58.75 %EqnAxiom % 58.67/58.75 [1]E(x11,x11) % 58.67/58.75 [2]E(x22,x21)+~E(x21,x22) % 58.67/58.75 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.67/58.75 [4]~E(x41,x42)+E(f14(x41),f14(x42)) % 58.67/58.75 [5]~E(x51,x52)+E(f15(x51),f15(x52)) % 58.67/58.75 [6]~E(x61,x62)+E(f21(x61,x63),f21(x62,x63)) % 58.67/58.75 [7]~E(x71,x72)+E(f21(x73,x71),f21(x73,x72)) % 58.67/58.75 [8]~E(x81,x82)+E(f22(x81),f22(x82)) % 58.67/58.75 [9]~E(x91,x92)+E(f24(x91),f24(x92)) % 58.67/58.75 [10]~E(x101,x102)+E(f23(x101,x103),f23(x102,x103)) % 58.67/58.75 [11]~E(x111,x112)+E(f23(x113,x111),f23(x113,x112)) % 58.67/58.75 [12]~P1(x121)+P1(x122)+~E(x121,x122) % 58.67/58.75 [13]~P10(x131)+P10(x132)+~E(x131,x132) % 58.67/58.75 [14]~P9(x141)+P9(x142)+~E(x141,x142) % 58.67/58.75 [15]~P6(x151)+P6(x152)+~E(x151,x152) % 58.67/58.75 [16]~P3(x161)+P3(x162)+~E(x161,x162) % 58.67/58.75 [17]P14(x172,x173)+~E(x171,x172)+~P14(x171,x173) % 58.67/58.75 [18]P14(x183,x182)+~E(x181,x182)+~P14(x183,x181) % 58.67/58.75 [19]P2(x192,x193)+~E(x191,x192)+~P2(x191,x193) % 58.67/58.75 [20]P2(x203,x202)+~E(x201,x202)+~P2(x203,x201) % 58.67/58.75 [21]P8(x212,x213)+~E(x211,x212)+~P8(x211,x213) % 58.67/58.75 [22]P8(x223,x222)+~E(x221,x222)+~P8(x223,x221) % 58.67/58.75 [23]~P5(x231)+P5(x232)+~E(x231,x232) % 58.67/58.75 [24]~P4(x241)+P4(x242)+~E(x241,x242) % 58.67/58.75 [25]~P7(x251)+P7(x252)+~E(x251,x252) % 58.67/58.75 [26]P13(x262,x263)+~E(x261,x262)+~P13(x261,x263) % 58.67/58.75 [27]P13(x273,x272)+~E(x271,x272)+~P13(x273,x271) % 58.67/58.75 [28]~P11(x281)+P11(x282)+~E(x281,x282) % 58.67/58.75 [29]~P15(x291)+P15(x292)+~E(x291,x292) % 58.67/58.75 [30]~P12(x301)+P12(x302)+~E(x301,x302) % 58.67/58.75 % 58.67/58.75 %------------------------------------------- % 58.67/58.76 cnf(126,plain, % 58.67/58.76 (~P8(x1261,a1)), % 58.67/58.76 inference(scs_inference,[],[34,107])). % 58.67/58.76 cnf(128,plain, % 58.67/58.76 (P13(f15(f24(x1281)),x1281)), % 58.67/58.76 inference(scs_inference,[],[85,34,107,118])). % 58.67/58.76 cnf(129,plain, % 58.67/58.76 (P2(f15(x1291),x1291)), % 58.67/58.76 inference(rename_variables,[],[85])). % 58.67/58.76 cnf(132,plain, % 58.67/58.76 (P8(f15(a20),a20)), % 58.67/58.76 inference(scs_inference,[],[82,89,85,129,34,86,107,118,17,111])). % 58.67/58.76 cnf(133,plain, % 58.67/58.76 (P2(f15(x1331),x1331)), % 58.67/58.76 inference(rename_variables,[],[85])). % 58.67/58.76 cnf(135,plain, % 58.67/58.76 (~P8(x1351,f15(f24(a1)))), % 58.67/58.76 inference(scs_inference,[],[82,89,85,129,133,34,86,107,118,17,111,121])). % 58.67/58.76 cnf(136,plain, % 58.67/58.76 (P2(f15(x1361),x1361)), % 58.67/58.76 inference(rename_variables,[],[85])). % 58.67/58.76 cnf(143,plain, % 58.67/58.76 (~E(a20,a1)), % 58.67/58.76 inference(scs_inference,[],[82,89,41,65,85,129,133,34,37,86,107,118,17,111,121,102,117,18,22])). % 58.67/58.76 cnf(144,plain, % 58.67/58.76 (P2(x1441,x1442)+~E(f15(x1442),x1441)), % 58.67/58.76 inference(scs_inference,[],[82,89,41,65,85,129,133,136,34,37,86,107,118,17,111,121,102,117,18,22,19])). % 58.67/58.76 cnf(145,plain, % 58.67/58.76 (P2(f15(x1451),x1452)+~E(x1451,x1452)), % 58.67/58.76 inference(scs_inference,[],[82,89,41,65,85,129,133,136,34,37,86,107,118,17,111,121,102,117,18,22,19,20])). % 58.67/58.76 cnf(147,plain, % 58.67/58.76 (P13(x1471,x1472)+~E(x1472,x1471)), % 58.67/58.76 inference(scs_inference,[],[82,89,41,65,83,85,129,133,136,34,37,86,107,118,17,111,121,102,117,18,22,19,20,21,26])). % 58.67/58.76 cnf(148,plain, % 58.67/58.76 (P13(x1481,x1482)+~E(x1481,x1482)), % 58.67/58.76 inference(scs_inference,[],[82,89,41,65,83,85,129,133,136,34,37,86,107,118,17,111,121,102,117,18,22,19,20,21,26,27])). % 58.67/58.76 cnf(157,plain, % 58.67/58.76 (~P8(x1571,f15(f24(a2)))), % 58.67/58.76 inference(scs_inference,[],[35,85,107,121])). % 58.67/58.76 cnf(158,plain, % 58.67/58.76 (P2(f15(x1581),x1581)), % 58.67/58.76 inference(rename_variables,[],[85])). % 58.67/58.76 cnf(160,plain, % 58.67/58.76 (P8(f15(a5),a5)), % 58.67/58.76 inference(scs_inference,[],[35,87,85,158,107,121,111])). % 58.67/58.76 cnf(165,plain, % 58.67/58.76 (~E(f14(a13),f21(a12,a11))), % 58.67/58.76 inference(scs_inference,[],[89,135,132,84,35,87,85,158,107,121,111,22,17])). % 58.67/58.76 cnf(179,plain, % 58.67/58.76 (P2(f15(x1791),x1791)), % 58.67/58.76 inference(rename_variables,[],[85])). % 58.67/58.76 cnf(190,plain, % 58.67/58.76 (P13(f15(f24(x1901)),x1902)+~E(x1901,x1902)), % 58.67/58.76 inference(scs_inference,[],[165,157,160,36,88,128,85,179,107,121,111,22,117,98,27])). % 58.67/58.76 cnf(191,plain, % 58.67/58.76 (P14(f14(x1911),x1912)+~E(x1911,x1912)), % 58.67/58.76 inference(scs_inference,[],[165,157,160,36,88,128,84,85,179,107,121,111,22,117,98,27,18])). % 58.67/58.76 cnf(272,plain, % 58.67/58.76 (~E(a5,a1)), % 58.67/58.76 inference(scs_inference,[],[160,126,22])). % 58.67/58.76 cnf(414,plain, % 58.67/58.76 (E(f22(a17),a1)), % 58.67/58.76 inference(scs_inference,[],[36,90,99])). % 58.67/58.76 cnf(418,plain, % 58.67/58.76 (P13(f22(a17),a1)), % 58.67/58.76 inference(scs_inference,[],[414,191,145,147,148])). % 58.67/58.76 cnf(419,plain, % 58.67/58.76 (E(a1,f22(a17))), % 58.67/58.76 inference(scs_inference,[],[414,191,145,147,148,2])). % 58.67/58.76 cnf(422,plain, % 58.67/58.76 (P1(f22(a17))), % 58.67/58.76 inference(scs_inference,[],[47,143,34,414,191,145,147,148,2,15,3,12])). % 58.67/58.76 cnf(430,plain, % 58.67/58.76 (~P8(x4301,f22(a17))), % 58.67/58.76 inference(scs_inference,[],[47,143,39,62,56,34,414,52,73,78,191,145,147,148,2,15,3,12,14,16,23,24,25,28,190,107])). % 58.67/58.76 cnf(444,plain, % 58.67/58.76 (P14(f14(a1),f22(a17))), % 58.67/58.76 inference(scs_inference,[],[419,191])). % 58.67/58.76 cnf(459,plain, % 58.67/58.76 (~E(a12,x4591)+~P14(a12,a13)+P3(x4591)), % 58.67/58.76 inference(scs_inference,[],[82,103,16])). % 58.67/58.76 cnf(463,plain, % 58.67/58.76 (P3(x4631)+~E(a12,x4631)), % 58.67/58.76 inference(scs_inference,[],[82,160,430,22,459])). % 58.67/58.76 cnf(474,plain, % 58.67/58.76 (P3(a12)), % 58.67/58.76 inference(equality_inference,[],[463])). % 58.67/58.76 cnf(3021,plain, % 58.67/58.76 (P3(a17)+~P9(a17)), % 58.67/58.76 inference(scs_inference,[],[422,91,106])). % 58.67/58.76 cnf(3986,plain, % 58.67/58.76 (P10(a12)), % 58.67/58.76 inference(scs_inference,[],[82,105])). % 58.67/58.76 cnf(5762,plain, % 58.67/58.76 (P3(a2)), % 58.67/58.76 inference(scs_inference,[],[35,91])). % 58.67/58.76 cnf(5770,plain, % 58.67/58.76 (P9(a17)), % 58.67/58.76 inference(scs_inference,[],[35,37,36,91,92,93,95,97])). % 58.67/58.76 cnf(5774,plain, % 58.67/58.76 (P1(f22(a2))), % 58.67/58.76 inference(scs_inference,[],[444,35,37,36,91,92,93,95,97,104,99])). % 58.67/58.76 cnf(5778,plain, % 58.67/58.76 (P3(a17)), % 58.67/58.76 inference(scs_inference,[],[444,35,37,36,91,92,93,95,97,104,99,100,3021])). % 58.67/58.76 cnf(5781,plain, % 58.67/58.76 (P2(x57811,f24(x57811))), % 58.67/58.76 inference(scs_inference,[],[66,444,35,37,36,83,91,92,93,95,97,104,99,100,3021,110,112])). % 58.67/58.76 cnf(5787,plain, % 58.67/58.76 (P13(a1,a2)), % 58.67/58.76 inference(scs_inference,[],[66,444,35,37,36,83,91,92,93,95,97,104,99,100,3021,110,112,90,5,9,147])). % 58.67/58.76 cnf(5788,plain, % 58.67/58.76 (E(f21(a2,x57881),f21(a1,x57881))), % 58.67/58.76 inference(scs_inference,[],[66,444,35,37,36,83,91,92,93,95,97,104,99,100,3021,110,112,90,5,9,147,6])). % 58.67/58.76 cnf(5789,plain, % 58.67/58.76 (E(a1,a2)), % 58.67/58.76 inference(scs_inference,[],[66,444,35,37,36,83,91,92,93,95,97,104,99,100,3021,110,112,90,5,9,147,6,2])). % 58.67/58.76 cnf(5795,plain, % 58.67/58.76 (~P2(a20,f24(a2))), % 58.67/58.76 inference(scs_inference,[],[66,69,42,444,35,37,36,79,132,83,414,91,92,93,95,97,104,99,100,3021,110,112,90,5,9,147,6,2,113,116,3,121])). % 58.67/58.76 cnf(5797,plain, % 58.67/58.76 (P11(a2)), % 58.67/58.76 inference(scs_inference,[],[66,69,42,444,35,78,37,36,79,132,83,414,91,92,93,95,97,104,99,100,3021,110,112,90,5,9,147,6,2,113,116,3,121,28])). % 58.67/58.76 cnf(5806,plain, % 58.67/58.76 (P14(f21(a9,a11),f22(a9))), % 58.67/58.76 inference(scs_inference,[],[51,81,66,67,69,76,71,72,73,42,45,46,444,86,35,78,37,36,79,132,83,414,91,92,93,95,97,104,99,100,3021,110,112,90,5,9,147,6,2,113,116,3,121,28,25,106,20,108,102,125])). % 58.67/58.76 cnf(5808,plain, % 58.67/58.76 (E(f21(a9,a11),f23(a9,a11))), % 58.67/58.76 inference(scs_inference,[],[51,81,66,67,69,76,71,72,73,42,45,46,444,86,35,78,37,36,79,132,83,414,91,92,93,95,97,104,99,100,3021,110,112,90,5,9,147,6,2,113,116,3,121,28,25,106,20,108,102,125,119])). % 58.67/58.76 cnf(5813,plain, % 58.67/58.76 (E(f21(x58131,a2),f21(x58131,a1))), % 58.67/58.76 inference(scs_inference,[],[51,81,66,67,69,76,71,72,73,42,45,46,444,86,35,78,37,36,79,132,83,414,91,92,93,95,97,104,99,100,3021,110,112,90,5,9,147,6,2,113,116,3,121,28,25,106,20,108,102,125,119,144,4,8,7])). % 58.67/58.76 cnf(5814,plain, % 58.67/58.76 (E(f23(a2,x58141),f23(a1,x58141))), % 58.67/58.76 inference(scs_inference,[],[51,81,66,67,69,76,71,72,73,42,45,46,444,86,35,78,37,36,79,132,83,414,91,92,93,95,97,104,99,100,3021,110,112,90,5,9,147,6,2,113,116,3,121,28,25,106,20,108,102,125,119,144,4,8,7,10])). % 58.67/58.76 cnf(5815,plain, % 58.67/58.76 (E(f23(x58151,a2),f23(x58151,a1))), % 58.67/58.76 inference(scs_inference,[],[51,81,66,67,69,76,71,72,73,42,45,46,444,86,35,78,37,36,79,132,83,414,91,92,93,95,97,104,99,100,3021,110,112,90,5,9,147,6,2,113,116,3,121,28,25,106,20,108,102,125,119,144,4,8,7,10,11])). % 58.67/58.76 cnf(5816,plain, % 58.67/58.76 (~P14(f21(a12,a11),x58161)+~P13(x58161,a13)), % 58.67/58.76 inference(scs_inference,[],[51,81,66,67,69,76,71,72,73,42,45,46,444,86,35,78,37,89,36,79,132,83,414,91,92,93,95,97,104,99,100,3021,110,112,90,5,9,147,6,2,113,116,3,121,28,25,106,20,108,102,125,119,144,4,8,7,10,11,120])). % 58.67/58.76 cnf(5818,plain, % 58.67/58.76 (P13(f22(a17),a2)), % 58.67/58.76 inference(scs_inference,[],[51,81,66,67,69,76,71,72,73,42,45,46,444,86,35,78,37,89,36,79,132,83,414,418,91,92,93,95,97,104,99,100,3021,110,112,90,5,9,147,6,2,113,116,3,121,28,25,106,20,108,102,125,119,144,4,8,7,10,11,120,27])). % 58.67/58.76 cnf(5819,plain, % 58.67/58.76 (P14(f23(a9,a11),f22(a9))), % 58.67/58.76 inference(scs_inference,[],[51,81,66,67,69,76,71,72,73,42,45,46,444,86,35,78,37,89,36,79,132,83,414,418,91,92,93,95,97,104,99,100,3021,110,112,90,5,9,147,6,2,113,116,3,121,28,25,106,20,108,102,125,119,144,4,8,7,10,11,120,27,17])). % 58.67/58.76 cnf(5849,plain, % 58.67/58.76 (P1(f22(a19))), % 58.67/58.76 inference(scs_inference,[],[5787,5819,5774,38,104,90,100,91,112,99])). % 58.67/58.76 cnf(5858,plain, % 58.67/58.76 (E(f22(a1),f22(a2))), % 58.67/58.76 inference(scs_inference,[],[5787,5789,5819,5774,38,104,90,100,91,112,99,93,92,7,95,8])). % 58.67/58.76 cnf(5869,plain, % 58.67/58.76 (E(f23(a9,a11),f21(a9,a11))), % 58.67/58.76 inference(scs_inference,[],[5770,5787,5789,5808,5819,5774,38,104,90,100,91,112,99,93,92,7,95,8,110,5,4,144,10,11,147,9,6,2])). % 58.67/58.76 cnf(5879,plain, % 58.67/58.76 (E(f21(a2,a2),f21(a1,a1))), % 58.67/58.76 inference(scs_inference,[],[5762,5770,5787,5789,5797,5781,5788,5813,5808,5819,5774,5795,5818,64,444,38,104,90,100,91,112,99,93,92,7,95,8,110,5,4,144,10,11,147,9,6,2,116,120,113,124,3])). % 58.67/58.76 cnf(5905,plain, % 58.67/58.76 (P1(f22(a18))), % 58.67/58.76 inference(scs_inference,[],[5806,37,104,99])). % 58.67/58.76 cnf(5909,plain, % 58.67/58.76 (E(f22(a19),a1)), % 58.67/58.76 inference(scs_inference,[],[5806,5849,37,104,99,100,90])). % 58.67/58.76 cnf(5929,plain, % 58.67/58.76 (E(f23(a2,a2),f23(a1,a1))), % 58.67/58.76 inference(scs_inference,[],[5778,5806,5869,5814,5815,5849,5879,5770,5818,63,70,37,80,104,99,100,90,92,112,110,93,91,95,147,2,116,113,3])). % 58.67/58.76 cnf(5949,plain, % 58.67/58.76 (E(f22(a18),a1)), % 58.67/58.76 inference(scs_inference,[],[5905,65,84,104,93,92,110,90])). % 58.67/58.76 cnf(5954,plain, % 58.67/58.76 (E(f23(a1,a1),f23(a2,a2))), % 58.67/58.76 inference(scs_inference,[],[5858,5905,5929,65,84,104,93,92,110,90,91,147,2])). % 58.67/58.76 cnf(5993,plain, % 58.67/58.76 ($false), % 58.67/58.76 inference(scs_inference,[],[51,5954,5949,5909,272,3986,67,65,126,41,38,83,82,474,104,90,110,4,10,7,11,9,6,147,2,113,3,22,122,125,123,5816]), % 58.67/58.76 ['proof']). % 58.67/58.76 % SZS output end Proof % 58.67/58.76 % Total time :58.110000s %------------------------------------------------------------------------------