%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU294+3 : 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:02:18 EDT 2024 % Result : Theorem 60.05s 60.36s % Output : CNFRefutation 60.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU294+3 : 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 : n021.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 : Fri Jun 21 17:23:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.58 start to proof:theBenchmark % 60.05/60.33 %------------------------------------------- % 60.05/60.33 % File :CSE---1.7 % 60.05/60.33 % Problem :theBenchmark % 60.05/60.33 % Transform :cnf % 60.05/60.33 % Format :tptp:raw % 60.05/60.33 % Command :java -jar mcs_scs.jar %d %s % 60.05/60.33 % 60.05/60.33 % Result :Theorem 59.460000s % 60.05/60.33 % Output :CNFRefutation 59.460000s % 60.05/60.33 %------------------------------------------- % 60.05/60.34 %------------------------------------------------------------------------------ % 60.05/60.34 % File : SEU294+3 : TPTP v8.2.0. Released v3.2.0. % 60.05/60.34 % Domain : Set theory % 60.05/60.34 % Problem : Finite sets, theorem 13 % 60.05/60.34 % Version : [Urb06] axioms : Especial. % 60.05/60.34 % English : % 60.05/60.34 % 60.05/60.34 % Refs : [Dar90] Darmochwal (1990), Finite Sets % 60.05/60.34 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 60.05/60.34 % Source : [Urb06] % 60.05/60.34 % Names : finset_1__t13_finset_1 [Urb06] % 60.05/60.34 % 60.05/60.34 % Status : Theorem % 60.05/60.34 % Rating : 0.03 v7.1.0, 0.00 v7.0.0, 0.03 v6.4.0, 0.08 v6.2.0, 0.04 v6.1.0, 0.07 v6.0.0, 0.04 v5.4.0, 0.07 v5.3.0, 0.11 v5.2.0, 0.00 v3.4.0, 0.05 v3.3.0, 0.00 v3.2.0 % 60.05/60.34 % Syntax : Number of formulae : 54 ( 7 unt; 0 def) % 60.05/60.34 % Number of atoms : 172 ( 2 equ) % 60.05/60.34 % Maximal formula atoms : 10 ( 3 avg) % 60.05/60.34 % Number of connectives : 135 ( 17 ~; 1 |; 94 &) % 60.05/60.34 % ( 1 <=>; 22 =>; 0 <=; 0 <~>) % 60.05/60.34 % Maximal formula depth : 12 ( 5 avg) % 60.05/60.34 % Maximal term depth : 2 ( 1 avg) % 60.05/60.34 % Number of predicates : 19 ( 18 usr; 0 prp; 1-2 aty) % 60.05/60.34 % Number of functors : 3 ( 3 usr; 2 con; 0-1 aty) % 60.05/60.34 % Number of variables : 68 ( 42 !; 26 ?) % 60.05/60.34 % SPC : FOF_THM_RFO_SEQ % 60.05/60.34 % 60.05/60.34 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 60.05/60.34 % library, www.mizar.org % 60.05/60.34 %------------------------------------------------------------------------------ % 60.05/60.34 fof(antisymmetry_r2_hidden,axiom, % 60.05/60.34 ! [A,B] : % 60.05/60.34 ( in(A,B) % 60.05/60.34 => ~ in(B,A) ) ). % 60.05/60.34 % 60.05/60.34 fof(cc1_arytm_3,axiom, % 60.05/60.34 ! [A] : % 60.05/60.34 ( ordinal(A) % 60.05/60.34 => ! [B] : % 60.05/60.34 ( element(B,A) % 60.05/60.34 => ( epsilon_transitive(B) % 60.05/60.34 & epsilon_connected(B) % 60.05/60.34 & ordinal(B) ) ) ) ). % 60.05/60.34 % 60.05/60.34 fof(cc1_finset_1,axiom, % 60.05/60.34 ! [A] : % 60.05/60.34 ( empty(A) % 60.05/60.34 => finite(A) ) ). % 60.05/60.34 % 60.05/60.34 fof(cc1_funct_1,axiom, % 60.05/60.34 ! [A] : % 60.05/60.34 ( empty(A) % 60.05/60.34 => function(A) ) ). % 60.05/60.34 % 60.05/60.34 fof(cc1_ordinal1,axiom, % 60.05/60.34 ! [A] : % 60.05/60.34 ( ordinal(A) % 60.05/60.34 => ( epsilon_transitive(A) % 60.05/60.34 & epsilon_connected(A) ) ) ). % 60.05/60.34 % 60.05/60.34 fof(cc1_relat_1,axiom, % 60.05/60.34 ! [A] : % 60.05/60.34 ( empty(A) % 60.05/60.34 => relation(A) ) ). % 60.05/60.34 % 60.05/60.34 fof(cc2_arytm_3,axiom, % 60.05/60.34 ! [A] : % 60.05/60.34 ( ( empty(A) % 60.05/60.34 & ordinal(A) ) % 60.05/60.34 => ( epsilon_transitive(A) % 60.05/60.34 & epsilon_connected(A) % 60.05/60.34 & ordinal(A) % 60.05/60.34 & natural(A) ) ) ). % 60.05/60.34 % 60.05/60.34 fof(cc2_finset_1,axiom, % 60.05/60.34 ! [A] : % 60.05/60.34 ( finite(A) % 60.05/60.34 => ! [B] : % 60.05/60.34 ( element(B,powerset(A)) % 60.05/60.34 => finite(B) ) ) ). % 60.05/60.34 % 60.05/60.34 fof(cc2_funct_1,axiom, % 60.05/60.34 ! [A] : % 60.05/60.34 ( ( relation(A) % 60.05/60.34 & empty(A) % 60.05/60.34 & function(A) ) % 60.05/60.34 => ( relation(A) % 60.05/60.34 & function(A) % 60.05/60.34 & one_to_one(A) ) ) ). % 60.05/60.34 % 60.05/60.34 fof(cc2_ordinal1,axiom, % 60.05/60.34 ! [A] : % 60.05/60.34 ( ( epsilon_transitive(A) % 60.05/60.34 & epsilon_connected(A) ) % 60.05/60.34 => ordinal(A) ) ). % 60.05/60.34 % 60.05/60.34 fof(cc3_ordinal1,axiom, % 60.05/60.34 ! [A] : % 60.05/60.34 ( empty(A) % 60.05/60.34 => ( epsilon_transitive(A) % 60.05/60.34 & epsilon_connected(A) % 60.05/60.34 & ordinal(A) ) ) ). % 60.05/60.34 % 60.05/60.34 fof(cc4_arytm_3,axiom, % 60.05/60.34 ! [A] : % 60.05/60.35 ( element(A,positive_rationals) % 60.05/60.35 => ( ordinal(A) % 60.05/60.35 => ( epsilon_transitive(A) % 60.05/60.35 & epsilon_connected(A) % 60.05/60.35 & ordinal(A) % 60.05/60.35 & natural(A) ) ) ) ). % 60.05/60.35 % 60.05/60.35 fof(existence_m1_subset_1,axiom, % 60.05/60.35 ! [A] : % 60.05/60.35 ? [B] : element(B,A) ). % 60.05/60.35 % 60.05/60.35 fof(fc12_relat_1,axiom, % 60.05/60.35 ( empty(empty_set) % 60.05/60.35 & relation(empty_set) % 60.05/60.35 & relation_empty_yielding(empty_set) ) ). % 60.05/60.35 % 60.05/60.35 fof(fc1_subset_1,axiom, % 60.05/60.35 ! [A] : ~ empty(powerset(A)) ). % 60.05/60.35 % 60.05/60.35 fof(fc1_xboole_0,axiom, % 60.05/60.35 empty(empty_set) ). % 60.05/60.35 % 60.05/60.35 fof(fc2_ordinal1,axiom, % 60.05/60.35 ( relation(empty_set) % 60.05/60.35 & relation_empty_yielding(empty_set) % 60.05/60.35 & function(empty_set) % 60.05/60.35 & one_to_one(empty_set) % 60.05/60.35 & empty(empty_set) % 60.05/60.35 & epsilon_transitive(empty_set) % 60.05/60.35 & epsilon_connected(empty_set) % 60.05/60.35 & ordinal(empty_set) ) ). % 60.05/60.35 % 60.05/60.35 fof(fc4_relat_1,axiom, % 60.05/60.35 ( empty(empty_set) % 60.05/60.35 & relation(empty_set) ) ). % 60.05/60.35 % 60.05/60.35 fof(fc8_arytm_3,axiom, % 60.05/60.35 ~ empty(positive_rationals) ). % 60.05/60.35 % 60.05/60.35 fof(rc1_arytm_3,axiom, % 60.05/60.35 ? [A] : % 60.05/60.35 ( ~ empty(A) % 60.05/60.35 & epsilon_transitive(A) % 60.05/60.35 & epsilon_connected(A) % 60.05/60.35 & ordinal(A) % 60.05/60.35 & natural(A) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc1_finset_1,axiom, % 60.05/60.35 ? [A] : % 60.05/60.35 ( ~ empty(A) % 60.05/60.35 & finite(A) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc1_funcop_1,axiom, % 60.05/60.35 ? [A] : % 60.05/60.35 ( relation(A) % 60.05/60.35 & function(A) % 60.05/60.35 & function_yielding(A) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc1_funct_1,axiom, % 60.05/60.35 ? [A] : % 60.05/60.35 ( relation(A) % 60.05/60.35 & function(A) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc1_ordinal1,axiom, % 60.05/60.35 ? [A] : % 60.05/60.35 ( epsilon_transitive(A) % 60.05/60.35 & epsilon_connected(A) % 60.05/60.35 & ordinal(A) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc1_ordinal2,axiom, % 60.05/60.35 ? [A] : % 60.05/60.35 ( epsilon_transitive(A) % 60.05/60.35 & epsilon_connected(A) % 60.05/60.35 & ordinal(A) % 60.05/60.35 & being_limit_ordinal(A) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc1_relat_1,axiom, % 60.05/60.35 ? [A] : % 60.05/60.35 ( empty(A) % 60.05/60.35 & relation(A) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc1_subset_1,axiom, % 60.05/60.35 ! [A] : % 60.05/60.35 ( ~ empty(A) % 60.05/60.35 => ? [B] : % 60.05/60.35 ( element(B,powerset(A)) % 60.05/60.35 & ~ empty(B) ) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc1_xboole_0,axiom, % 60.05/60.35 ? [A] : empty(A) ). % 60.05/60.35 % 60.05/60.35 fof(rc2_arytm_3,axiom, % 60.05/60.35 ? [A] : % 60.05/60.35 ( element(A,positive_rationals) % 60.05/60.35 & ~ empty(A) % 60.05/60.35 & epsilon_transitive(A) % 60.05/60.35 & epsilon_connected(A) % 60.05/60.35 & ordinal(A) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc2_finset_1,axiom, % 60.05/60.35 ! [A] : % 60.05/60.35 ? [B] : % 60.05/60.35 ( element(B,powerset(A)) % 60.05/60.35 & empty(B) % 60.05/60.35 & relation(B) % 60.05/60.35 & function(B) % 60.05/60.35 & one_to_one(B) % 60.05/60.35 & epsilon_transitive(B) % 60.05/60.35 & epsilon_connected(B) % 60.05/60.35 & ordinal(B) % 60.05/60.35 & natural(B) % 60.05/60.35 & finite(B) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc2_funct_1,axiom, % 60.05/60.35 ? [A] : % 60.05/60.35 ( relation(A) % 60.05/60.35 & empty(A) % 60.05/60.35 & function(A) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc2_ordinal1,axiom, % 60.05/60.35 ? [A] : % 60.05/60.35 ( relation(A) % 60.05/60.35 & function(A) % 60.05/60.35 & one_to_one(A) % 60.05/60.35 & empty(A) % 60.05/60.35 & epsilon_transitive(A) % 60.05/60.35 & epsilon_connected(A) % 60.05/60.35 & ordinal(A) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc2_ordinal2,axiom, % 60.05/60.35 ? [A] : % 60.05/60.35 ( relation(A) % 60.05/60.35 & function(A) % 60.05/60.35 & transfinite_sequence(A) % 60.05/60.35 & ordinal_yielding(A) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc2_relat_1,axiom, % 60.05/60.35 ? [A] : % 60.05/60.35 ( ~ empty(A) % 60.05/60.35 & relation(A) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc2_subset_1,axiom, % 60.05/60.35 ! [A] : % 60.05/60.35 ? [B] : % 60.05/60.35 ( element(B,powerset(A)) % 60.05/60.35 & empty(B) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc2_xboole_0,axiom, % 60.05/60.35 ? [A] : ~ empty(A) ). % 60.05/60.35 % 60.05/60.35 fof(rc3_arytm_3,axiom, % 60.05/60.35 ? [A] : % 60.05/60.35 ( element(A,positive_rationals) % 60.05/60.35 & empty(A) % 60.05/60.35 & epsilon_transitive(A) % 60.05/60.35 & epsilon_connected(A) % 60.05/60.35 & ordinal(A) % 60.05/60.35 & natural(A) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc3_finset_1,axiom, % 60.05/60.35 ! [A] : % 60.05/60.35 ( ~ empty(A) % 60.05/60.35 => ? [B] : % 60.05/60.35 ( element(B,powerset(A)) % 60.05/60.35 & ~ empty(B) % 60.05/60.35 & finite(B) ) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc3_funct_1,axiom, % 60.05/60.35 ? [A] : % 60.05/60.35 ( relation(A) % 60.05/60.35 & function(A) % 60.05/60.35 & one_to_one(A) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc3_ordinal1,axiom, % 60.05/60.35 ? [A] : % 60.05/60.35 ( ~ empty(A) % 60.05/60.35 & epsilon_transitive(A) % 60.05/60.35 & epsilon_connected(A) % 60.05/60.35 & ordinal(A) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc3_relat_1,axiom, % 60.05/60.35 ? [A] : % 60.05/60.35 ( relation(A) % 60.05/60.35 & relation_empty_yielding(A) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc4_funct_1,axiom, % 60.05/60.35 ? [A] : % 60.05/60.35 ( relation(A) % 60.05/60.35 & relation_empty_yielding(A) % 60.05/60.35 & function(A) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc4_ordinal1,axiom, % 60.05/60.35 ? [A] : % 60.05/60.35 ( relation(A) % 60.05/60.35 & function(A) % 60.05/60.35 & transfinite_sequence(A) ) ). % 60.05/60.35 % 60.05/60.35 fof(rc5_funct_1,axiom, % 60.05/60.35 ? [A] : % 60.05/60.35 ( relation(A) % 60.05/60.35 & relation_non_empty(A) % 60.05/60.35 & function(A) ) ). % 60.05/60.35 % 60.05/60.35 fof(reflexivity_r1_tarski,axiom, % 60.05/60.35 ! [A,B] : subset(A,A) ). % 60.05/60.36 % 60.05/60.36 fof(t13_finset_1,conjecture, % 60.05/60.36 ! [A,B] : % 60.05/60.36 ( ( subset(A,B) % 60.05/60.36 & finite(B) ) % 60.05/60.36 => finite(A) ) ). % 60.05/60.36 % 60.05/60.36 fof(t1_subset,axiom, % 60.05/60.36 ! [A,B] : % 60.05/60.36 ( in(A,B) % 60.05/60.36 => element(A,B) ) ). % 60.05/60.36 % 60.05/60.36 fof(t2_subset,axiom, % 60.05/60.36 ! [A,B] : % 60.05/60.36 ( element(A,B) % 60.05/60.36 => ( empty(B) % 60.05/60.36 | in(A,B) ) ) ). % 60.05/60.36 % 60.05/60.36 fof(t3_subset,axiom, % 60.05/60.36 ! [A,B] : % 60.05/60.36 ( element(A,powerset(B)) % 60.05/60.36 <=> subset(A,B) ) ). % 60.05/60.36 % 60.05/60.36 fof(t4_subset,axiom, % 60.05/60.36 ! [A,B,C] : % 60.05/60.36 ( ( in(A,B) % 60.05/60.36 & element(B,powerset(C)) ) % 60.05/60.36 => element(A,C) ) ). % 60.05/60.36 % 60.05/60.36 fof(t5_subset,axiom, % 60.05/60.36 ! [A,B,C] : % 60.05/60.36 ~ ( in(A,B) % 60.05/60.36 & element(B,powerset(C)) % 60.05/60.36 & empty(C) ) ). % 60.05/60.36 % 60.05/60.36 fof(t6_boole,axiom, % 60.05/60.36 ! [A] : % 60.05/60.36 ( empty(A) % 60.05/60.36 => A = empty_set ) ). % 60.05/60.36 % 60.05/60.36 fof(t7_boole,axiom, % 60.05/60.36 ! [A,B] : % 60.05/60.36 ~ ( in(A,B) % 60.05/60.36 & empty(B) ) ). % 60.05/60.36 % 60.05/60.36 fof(t8_boole,axiom, % 60.05/60.36 ! [A,B] : % 60.05/60.36 ~ ( empty(A) % 60.05/60.36 & A != B % 60.05/60.36 & empty(B) ) ). % 60.05/60.36 % 60.05/60.36 %------------------------------------------------------------------------------ % 60.05/60.36 %------------------------------------------- % 60.05/60.36 % Proof found % 60.05/60.36 % SZS status Theorem for theBenchmark % 60.05/60.36 % SZS output start Proof % 60.05/60.36 %ClaNum:166(EqnAxiom:30) % 60.05/60.36 %VarNum:117(SingletonVarNum:61) % 60.05/60.36 %MaxLitNum:4 % 60.05/60.36 %MaxfuncDepth:1 % 60.05/60.36 %SharedTerms:105 % 60.05/60.36 %goalClause: 65 118 130 % 60.05/60.36 %singleGoalClaCount:3 % 60.05/60.36 [31]P1(a1) % 60.05/60.36 [32]P1(a2) % 60.05/60.36 [33]P1(a23) % 60.05/60.36 [34]P1(a27) % 60.05/60.36 [35]P1(a3) % 60.05/60.36 [36]P1(a5) % 60.05/60.36 [37]P1(a8) % 60.05/60.36 [38]P1(a13) % 60.05/60.36 [39]P2(a1) % 60.05/60.36 [40]P2(a2) % 60.05/60.36 [41]P2(a23) % 60.05/60.36 [42]P2(a27) % 60.05/60.36 [43]P2(a3) % 60.05/60.36 [44]P2(a5) % 60.05/60.36 [45]P2(a8) % 60.05/60.36 [46]P2(a13) % 60.05/60.36 [47]P3(a1) % 60.05/60.36 [48]P3(a2) % 60.05/60.36 [49]P3(a23) % 60.05/60.36 [50]P3(a27) % 60.05/60.36 [51]P3(a3) % 60.05/60.36 [52]P3(a5) % 60.05/60.36 [53]P3(a8) % 60.05/60.36 [54]P3(a13) % 60.05/60.36 [58]P4(a1) % 60.05/60.36 [59]P4(a28) % 60.05/60.36 [60]P4(a4) % 60.05/60.36 [61]P4(a6) % 60.05/60.36 [62]P4(a5) % 60.05/60.36 [63]P4(a8) % 60.05/60.36 [64]P7(a24) % 60.05/60.36 [65]P7(a17) % 60.05/60.36 [66]P8(a1) % 60.05/60.36 [67]P8(a25) % 60.05/60.36 [68]P8(a26) % 60.05/60.36 [69]P8(a6) % 60.05/60.36 [70]P8(a5) % 60.05/60.36 [71]P8(a9) % 60.05/60.36 [72]P8(a14) % 60.05/60.36 [73]P8(a18) % 60.05/60.36 [74]P8(a20) % 60.05/60.36 [75]P8(a21) % 60.05/60.36 [78]P13(a1) % 60.05/60.36 [79]P13(a25) % 60.05/60.36 [80]P13(a26) % 60.05/60.36 [81]P13(a28) % 60.05/60.36 [82]P13(a6) % 60.05/60.36 [83]P13(a5) % 60.05/60.36 [84]P13(a9) % 60.05/60.36 [85]P13(a10) % 60.05/60.36 [86]P13(a14) % 60.05/60.36 [87]P13(a19) % 60.05/60.36 [88]P13(a18) % 60.05/60.36 [89]P13(a20) % 60.05/60.36 [90]P13(a21) % 60.05/60.36 [91]P9(a2) % 60.05/60.36 [92]P9(a8) % 60.05/60.36 [93]P12(a1) % 60.05/60.36 [94]P12(a5) % 60.05/60.36 [95]P12(a14) % 60.05/60.36 [97]P15(a1) % 60.05/60.36 [98]P15(a19) % 60.05/60.36 [99]P15(a18) % 60.05/60.36 [100]P10(a25) % 60.05/60.36 [101]P5(a27) % 60.05/60.36 [102]P16(a9) % 60.05/60.36 [103]P16(a20) % 60.05/60.36 [104]P14(a9) % 60.05/60.36 [105]P17(a21) % 60.05/60.36 [116]P6(a3,a29) % 60.05/60.36 [117]P6(a8,a29) % 60.05/60.36 [118]P18(a22,a17) % 60.05/60.36 [123]~P4(a29) % 60.05/60.36 [124]~P4(a2) % 60.05/60.36 [125]~P4(a24) % 60.05/60.36 [126]~P4(a3) % 60.05/60.36 [127]~P4(a10) % 60.05/60.36 [128]~P4(a12) % 60.05/60.36 [129]~P4(a13) % 60.05/60.36 [130]~P7(a22) % 60.05/60.36 [119]P18(x1191,x1191) % 60.05/60.36 [106]P1(f7(x1061)) % 60.05/60.36 [107]P2(f7(x1071)) % 60.05/60.36 [108]P3(f7(x1081)) % 60.05/60.36 [109]P4(f7(x1091)) % 60.05/60.36 [110]P4(f11(x1101)) % 60.05/60.36 [111]P7(f7(x1111)) % 60.05/60.36 [112]P8(f7(x1121)) % 60.05/60.36 [113]P13(f7(x1131)) % 60.05/60.36 [114]P9(f7(x1141)) % 60.05/60.36 [115]P12(f7(x1151)) % 60.05/60.36 [120]P6(f15(x1201),x1201) % 60.05/60.36 [121]P6(f7(x1211),f31(x1211)) % 60.05/60.36 [122]P6(f11(x1221),f31(x1221)) % 60.05/60.36 [131]~P4(f31(x1311)) % 60.05/60.36 [132]~P4(x1321)+E(x1321,a1) % 60.05/60.36 [133]~P4(x1331)+P1(x1331) % 60.05/60.36 [134]~P1(x1341)+P2(x1341) % 60.05/60.36 [135]~P4(x1351)+P2(x1351) % 60.05/60.36 [136]~P1(x1361)+P3(x1361) % 60.05/60.36 [137]~P4(x1371)+P3(x1371) % 60.05/60.36 [138]~P4(x1381)+P7(x1381) % 60.05/60.36 [139]~P4(x1391)+P8(x1391) % 60.05/60.36 [140]~P4(x1401)+P13(x1401) % 60.05/60.36 [141]P4(x1411)+P7(f16(x1411)) % 60.05/60.36 [147]P4(x1471)+~P4(f30(x1471)) % 60.05/60.36 [148]P4(x1481)+~P4(f16(x1481)) % 60.05/60.36 [151]P4(x1511)+P6(f30(x1511),f31(x1511)) % 60.05/60.36 [152]P4(x1521)+P6(f16(x1521),f31(x1521)) % 60.05/60.36 [150]~P4(x1501)+~P11(x1502,x1501) % 60.05/60.36 [159]~P11(x1591,x1592)+P6(x1591,x1592) % 60.05/60.36 [163]~P11(x1632,x1631)+~P11(x1631,x1632) % 60.05/60.36 [161]~P18(x1611,x1612)+P6(x1611,f31(x1612)) % 60.05/60.36 [164]P18(x1641,x1642)+~P6(x1641,f31(x1642)) % 60.05/60.36 [143]~P2(x1431)+~P3(x1431)+P1(x1431) % 60.05/60.36 [146]~P1(x1461)+~P4(x1461)+P9(x1461) % 60.05/60.36 [155]~P1(x1551)+P9(x1551)+~P6(x1551,a29) % 60.05/60.36 [142]~P4(x1422)+~P4(x1421)+E(x1421,x1422) % 60.05/60.36 [156]~P6(x1561,x1562)+P1(x1561)+~P1(x1562) % 60.05/60.36 [157]~P6(x1571,x1572)+P2(x1571)+~P1(x1572) % 60.05/60.36 [158]~P6(x1581,x1582)+P3(x1581)+~P1(x1582) % 60.05/60.36 [160]~P6(x1602,x1601)+P4(x1601)+P11(x1602,x1601) % 60.05/60.36 [162]P7(x1621)+~P7(x1622)+~P6(x1621,f31(x1622)) % 60.05/60.36 [165]~P4(x1651)+~P11(x1652,x1653)+~P6(x1653,f31(x1651)) % 60.05/60.36 [166]P6(x1661,x1662)+~P11(x1661,x1663)+~P6(x1663,f31(x1662)) % 60.05/60.36 [149]~P4(x1491)+~P8(x1491)+~P13(x1491)+P12(x1491) % 60.05/60.36 %EqnAxiom % 60.05/60.36 [1]E(x11,x11) % 60.05/60.36 [2]E(x22,x21)+~E(x21,x22) % 60.05/60.36 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 60.05/60.36 [4]~E(x41,x42)+E(f7(x41),f7(x42)) % 60.05/60.36 [5]~E(x51,x52)+E(f31(x51),f31(x52)) % 60.05/60.36 [6]~E(x61,x62)+E(f16(x61),f16(x62)) % 60.05/60.36 [7]~E(x71,x72)+E(f30(x71),f30(x72)) % 60.05/60.36 [8]~E(x81,x82)+E(f11(x81),f11(x82)) % 60.05/60.36 [9]~E(x91,x92)+E(f15(x91),f15(x92)) % 60.05/60.36 [10]~P1(x101)+P1(x102)+~E(x101,x102) % 60.05/60.36 [11]P6(x112,x113)+~E(x111,x112)+~P6(x111,x113) % 60.05/60.36 [12]P6(x123,x122)+~E(x121,x122)+~P6(x123,x121) % 60.05/60.36 [13]P11(x132,x133)+~E(x131,x132)+~P11(x131,x133) % 60.05/60.36 [14]P11(x143,x142)+~E(x141,x142)+~P11(x143,x141) % 60.05/60.36 [15]~P3(x151)+P3(x152)+~E(x151,x152) % 60.05/60.36 [16]~P2(x161)+P2(x162)+~E(x161,x162) % 60.05/60.36 [17]~P4(x171)+P4(x172)+~E(x171,x172) % 60.05/60.36 [18]~P7(x181)+P7(x182)+~E(x181,x182) % 60.05/60.36 [19]~P13(x191)+P13(x192)+~E(x191,x192) % 60.05/60.36 [20]~P15(x201)+P15(x202)+~E(x201,x202) % 60.05/60.36 [21]~P12(x211)+P12(x212)+~E(x211,x212) % 60.05/60.36 [22]~P8(x221)+P8(x222)+~E(x221,x222) % 60.05/60.36 [23]~P10(x231)+P10(x232)+~E(x231,x232) % 60.05/60.36 [24]~P5(x241)+P5(x242)+~E(x241,x242) % 60.05/60.36 [25]~P16(x251)+P16(x252)+~E(x251,x252) % 60.05/60.36 [26]~P9(x261)+P9(x262)+~E(x261,x262) % 60.05/60.36 [27]P18(x272,x273)+~E(x271,x272)+~P18(x271,x273) % 60.05/60.36 [28]P18(x283,x282)+~E(x281,x282)+~P18(x283,x281) % 60.05/60.36 [29]~P14(x291)+P14(x292)+~E(x291,x292) % 60.05/60.36 [30]~P17(x301)+P17(x302)+~E(x301,x302) % 60.05/60.36 % 60.05/60.36 %------------------------------------------- % 60.05/60.36 cnf(167,plain, % 60.05/60.36 (~P4(a22)), % 60.05/60.36 inference(scs_inference,[],[130,138])). % 60.05/60.36 cnf(169,plain, % 60.05/60.36 (P18(f15(f31(x1691)),x1691)), % 60.05/60.36 inference(scs_inference,[],[130,120,138,164])). % 60.05/60.36 cnf(170,plain, % 60.05/60.36 (P6(f15(x1701),x1701)), % 60.05/60.36 inference(rename_variables,[],[120])). % 60.05/60.36 cnf(175,plain, % 60.05/60.36 (P6(f15(x1751),x1751)), % 60.05/60.36 inference(rename_variables,[],[120])). % 60.05/60.36 cnf(177,plain, % 60.05/60.36 (P11(f15(a29),a29)), % 60.05/60.36 inference(scs_inference,[],[65,130,120,170,175,58,123,138,164,150,162,160])). % 60.05/60.36 cnf(178,plain, % 60.05/60.36 (P6(f15(x1781),x1781)), % 60.05/60.36 inference(rename_variables,[],[120])). % 60.05/60.36 cnf(180,plain, % 60.05/60.36 (~P11(x1801,f15(f31(a1)))), % 60.05/60.36 inference(scs_inference,[],[65,130,120,170,175,178,58,123,138,164,150,162,160,165])). % 60.05/60.36 cnf(181,plain, % 60.05/60.36 (P6(f15(x1811),x1811)), % 60.05/60.36 inference(rename_variables,[],[120])). % 60.05/60.36 cnf(195,plain, % 60.05/60.36 (P6(f15(x1951),x1951)), % 60.05/60.36 inference(rename_variables,[],[120])). % 60.05/60.36 cnf(198,plain, % 60.05/60.36 (P6(f15(x1981),x1982)+~E(x1981,x1982)), % 60.05/60.36 inference(scs_inference,[],[65,118,130,120,170,175,178,181,195,58,61,123,116,31,35,69,82,138,164,150,162,160,165,146,155,14,149,163,27,28,166,11,12])). % 60.05/60.36 cnf(205,plain, % 60.05/60.36 (P18(f7(x2051),x2051)), % 60.05/60.36 inference(scs_inference,[],[121,164])). % 60.05/60.36 cnf(207,plain, % 60.05/60.36 (~P11(x2071,a28)), % 60.05/60.36 inference(scs_inference,[],[121,59,164,150])). % 60.05/60.36 cnf(214,plain, % 60.05/60.36 (P11(f15(a22),a22)), % 60.05/60.36 inference(scs_inference,[],[65,167,121,122,59,62,120,36,164,150,162,146,160])). % 60.05/60.36 cnf(215,plain, % 60.05/60.36 (P6(f15(x2151),x2151)), % 60.05/60.36 inference(rename_variables,[],[120])). % 60.05/60.36 cnf(217,plain, % 60.05/60.36 (~P11(x2171,f7(a28))), % 60.05/60.36 inference(scs_inference,[],[65,167,121,122,59,62,120,36,164,150,162,146,160,165])). % 60.05/60.36 cnf(218,plain, % 60.05/60.36 (P6(f7(x2181),f31(x2181))), % 60.05/60.36 inference(rename_variables,[],[121])). % 60.05/60.36 cnf(229,plain, % 60.05/60.36 (P18(x2291,x2292)+~E(x2292,x2291)), % 60.05/60.36 inference(scs_inference,[],[65,167,119,180,177,121,218,122,59,62,120,215,36,164,150,162,146,160,165,14,163,166,155,27])). % 60.05/60.36 cnf(231,plain, % 60.05/60.36 (P18(x2311,x2312)+~E(x2311,x2312)), % 60.05/60.36 inference(scs_inference,[],[65,167,119,180,177,121,218,122,59,62,120,215,36,164,150,162,146,160,165,14,163,166,155,27,12,28])). % 60.05/60.36 cnf(232,plain, % 60.05/60.36 (P6(x2321,f31(x2322))+~E(f7(x2322),x2321)), % 60.05/60.36 inference(scs_inference,[],[65,167,119,180,177,121,218,122,59,62,120,215,36,164,150,162,146,160,165,14,163,166,155,27,12,28,11])). % 60.05/60.36 cnf(237,plain, % 60.05/60.36 (P18(f11(x2371),x2371)), % 60.05/60.36 inference(scs_inference,[],[122,164])). % 60.05/60.36 cnf(245,plain, % 60.05/60.36 (P6(f11(x2451),f31(x2451))), % 60.05/60.36 inference(rename_variables,[],[122])). % 60.05/60.36 cnf(258,plain, % 60.05/60.36 (P18(f7(x2581),x2582)+~E(x2581,x2582)), % 60.05/60.36 inference(scs_inference,[],[205,217,214,60,122,245,120,124,164,150,160,165,14,163,146,13,166,12,27,28])). % 60.05/60.36 cnf(265,plain, % 60.05/60.36 (~P11(x2651,f7(a8))), % 60.05/60.36 inference(scs_inference,[],[121,63,150,165])). % 60.05/60.36 cnf(268,plain, % 60.05/60.36 (P11(f15(a24),a24)), % 60.05/60.36 inference(scs_inference,[],[121,63,120,125,150,165,160])). % 60.05/60.36 cnf(284,plain, % 60.05/60.36 (~P11(x2841,f11(f7(x2842)))), % 60.05/60.36 inference(scs_inference,[],[122,109,150,165])). % 60.05/60.36 cnf(287,plain, % 60.05/60.36 (P11(f15(a3),a3)), % 60.05/60.36 inference(scs_inference,[],[122,109,120,126,150,165,160])). % 60.05/60.36 cnf(299,plain, % 60.05/60.36 (P18(f11(x2991),x2992)+~E(x2991,x2992)), % 60.05/60.36 inference(scs_inference,[],[122,237,265,268,109,61,120,117,126,150,165,160,14,163,146,11,12,27,28])). % 60.05/60.36 cnf(324,plain, % 60.05/60.36 (P18(f15(f31(x3241)),x3242)+~E(x3241,x3242)), % 60.05/60.36 inference(scs_inference,[],[122,169,284,287,62,59,120,116,127,150,165,160,14,163,146,11,12,13,27,28])). % 60.05/60.36 cnf(330,plain, % 60.05/60.36 (~P11(x3301,f11(x3302))), % 60.05/60.36 inference(scs_inference,[],[110,150])). % 60.05/60.36 cnf(345,plain, % 60.05/60.36 (P11(f15(a13),a13)), % 60.05/60.36 inference(scs_inference,[],[61,120,129,150,160])). % 60.05/60.36 cnf(356,plain, % 60.05/60.36 (P11(f7(x3561),f31(x3561))), % 60.05/60.36 inference(scs_inference,[],[121,131,160])). % 60.05/60.36 cnf(376,plain, % 60.05/60.36 (P11(x3761,f31(x3762))+~E(f7(x3762),x3761)), % 60.05/60.36 inference(scs_inference,[],[268,356,180,14,13])). % 60.05/60.36 cnf(475,plain, % 60.05/60.36 (~P4(f16(a13))), % 60.05/60.36 inference(scs_inference,[],[345,148,150])). % 60.05/60.36 cnf(485,plain, % 60.05/60.36 (E(a1,a4)), % 60.05/60.36 inference(scs_inference,[],[60,2,132])). % 60.05/60.36 cnf(492,plain, % 60.05/60.36 (E(a4,a1)), % 60.05/60.36 inference(scs_inference,[],[485,229,231,258,299,324,198,2])). % 60.05/60.36 cnf(513,plain, % 60.05/60.36 (P6(f15(a4),a1)), % 60.05/60.36 inference(scs_inference,[],[492,299,324,198])). % 60.05/60.36 cnf(626,plain, % 60.05/60.36 (P6(a1,f31(a4))), % 60.05/60.36 inference(scs_inference,[],[492,161,229])). % 60.05/60.36 cnf(627,plain, % 60.05/60.36 (P11(a1,f31(a4))), % 60.05/60.36 inference(scs_inference,[],[626,131,160])). % 60.05/60.36 cnf(927,plain, % 60.05/60.36 (P1(a28)), % 60.05/60.36 inference(scs_inference,[],[207,120,133,160])). % 60.05/60.36 cnf(933,plain, % 60.05/60.36 (P2(a6)), % 60.05/60.36 inference(scs_inference,[],[61,133,134])). % 60.05/60.36 cnf(936,plain, % 60.05/60.36 (P3(a6)), % 60.05/60.36 inference(scs_inference,[],[61,133,136])). % 60.05/60.36 cnf(937,plain, % 60.05/60.36 (P1(a6)), % 60.05/60.36 inference(scs_inference,[],[933,936,143])). % 60.05/60.36 cnf(969,plain, % 60.05/60.36 (~E(a6,a22)), % 60.05/60.36 inference(scs_inference,[],[61,130,138,18])). % 60.05/60.36 cnf(1624,plain, % 60.05/60.36 (E(a1,a6)), % 60.05/60.36 inference(scs_inference,[],[61,132,2])). % 60.05/60.36 cnf(1625,plain, % 60.05/60.36 (P18(a6,a1)), % 60.05/60.36 inference(scs_inference,[],[1624,229])). % 60.05/60.36 cnf(1627,plain, % 60.05/60.36 (E(a6,a1)), % 60.05/60.36 inference(scs_inference,[],[1624,229,231,2])). % 60.05/60.36 cnf(1631,plain, % 60.05/60.36 (P6(f15(a1),a6)), % 60.05/60.36 inference(scs_inference,[],[1624,229,231,2,299,324,258,198])). % 60.05/60.36 cnf(1753,plain, % 60.05/60.36 (E(f7(a6),f7(a1))), % 60.05/60.36 inference(scs_inference,[],[61,132,4])). % 60.05/60.36 cnf(1762,plain, % 60.05/60.36 (~E(a3,f11(x17621))), % 60.05/60.36 inference(scs_inference,[],[330,287,1753,232,376,231,2,229,258,299,198,14])). % 60.05/60.36 cnf(2238,plain, % 60.05/60.36 (P11(a6,f31(a4))), % 60.05/60.36 inference(scs_inference,[],[1624,513,627,12,13])). % 60.05/60.36 cnf(2437,plain, % 60.05/60.36 (~P6(a22,f31(a17))), % 60.05/60.36 inference(scs_inference,[],[65,927,937,2238,1762,1625,1631,475,124,63,969,59,1627,130,485,134,141,147,148,161,151,152,4,5,6,7,8,9,132,137,139,140,138,2,157,158,156,3,17,165,18,162])). % 60.05/60.36 cnf(2803,plain, % 60.05/60.36 ($false), % 60.05/60.36 inference(scs_inference,[],[2437,118,161]), % 60.05/60.36 ['proof']). % 60.05/60.38 % SZS output end Proof % 60.05/60.38 % Total time :59.460000s %------------------------------------------------------------------------------