%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU096+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 : n027.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:01:02 EDT 2024 % Result : Theorem 1.33s 1.40s % Output : CNFRefutation 1.33s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SEU096+1 : TPTP v8.2.0. Released v3.2.0. % 0.12/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n027.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 14:51:08 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 1.27/1.38 %------------------------------------------- % 1.27/1.38 % File :CSE---1.7 % 1.27/1.38 % Problem :theBenchmark % 1.27/1.38 % Transform :cnf % 1.27/1.38 % Format :tptp:raw % 1.27/1.38 % Command :java -jar mcs_scs.jar %d %s % 1.27/1.38 % 1.27/1.38 % Result :Theorem 0.780000s % 1.27/1.38 % Output :CNFRefutation 0.780000s % 1.27/1.38 %------------------------------------------- % 1.27/1.38 %------------------------------------------------------------------------------ % 1.27/1.38 % File : SEU096+1 : TPTP v8.2.0. Released v3.2.0. % 1.27/1.38 % Domain : Set theory % 1.27/1.38 % Problem : Finite sets, theorem 27 % 1.27/1.38 % Version : [Urb06] axioms : Especial. % 1.27/1.38 % English : % 1.27/1.38 % 1.27/1.38 % Refs : [Dar90] Darmochwal (1990), Finite Sets % 1.27/1.38 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 1.27/1.38 % Source : [Urb06] % 1.27/1.38 % Names : finset_1__t27_finset_1 [Urb06] % 1.27/1.38 % 1.27/1.38 % Status : Theorem % 1.27/1.38 % Rating : 0.14 v8.1.0, 0.17 v7.5.0, 0.19 v7.4.0, 0.07 v7.3.0, 0.10 v7.1.0, 0.13 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.21 v6.2.0, 0.24 v6.1.0, 0.30 v6.0.0, 0.22 v5.4.0, 0.29 v5.3.0, 0.33 v5.2.0, 0.15 v5.1.0, 0.14 v5.0.0, 0.21 v4.1.0, 0.22 v4.0.0, 0.21 v3.7.0, 0.15 v3.5.0, 0.16 v3.3.0, 0.07 v3.2.0 % 1.27/1.38 % Syntax : Number of formulae : 60 ( 7 unt; 0 def) % 1.27/1.38 % Number of atoms : 196 ( 3 equ) % 1.27/1.38 % Maximal formula atoms : 10 ( 3 avg) % 1.27/1.38 % Number of connectives : 155 ( 19 ~; 1 |; 103 &) % 1.33/1.38 % ( 1 <=>; 31 =>; 0 <=; 0 <~>) % 1.33/1.38 % Maximal formula depth : 12 ( 5 avg) % 1.33/1.38 % Maximal term depth : 3 ( 1 avg) % 1.33/1.38 % Number of predicates : 20 ( 19 usr; 0 prp; 1-2 aty) % 1.33/1.38 % Number of functors : 6 ( 6 usr; 2 con; 0-2 aty) % 1.33/1.38 % Number of variables : 77 ( 51 !; 26 ?) % 1.33/1.38 % SPC : FOF_THM_RFO_SEQ % 1.33/1.38 % 1.33/1.38 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 1.33/1.38 % library, www.mizar.org % 1.33/1.38 %------------------------------------------------------------------------------ % 1.33/1.38 fof(antisymmetry_r2_hidden,axiom, % 1.33/1.38 ! [A,B] : % 1.33/1.38 ( in(A,B) % 1.33/1.38 => ~ in(B,A) ) ). % 1.33/1.38 % 1.33/1.38 fof(cc1_arytm_3,axiom, % 1.33/1.38 ! [A] : % 1.33/1.38 ( ordinal(A) % 1.33/1.38 => ! [B] : % 1.33/1.38 ( element(B,A) % 1.33/1.38 => ( epsilon_transitive(B) % 1.33/1.38 & epsilon_connected(B) % 1.33/1.38 & ordinal(B) ) ) ) ). % 1.33/1.38 % 1.33/1.38 fof(cc1_finset_1,axiom, % 1.33/1.38 ! [A] : % 1.33/1.38 ( empty(A) % 1.33/1.38 => finite(A) ) ). % 1.33/1.38 % 1.33/1.38 fof(cc1_funct_1,axiom, % 1.33/1.38 ! [A] : % 1.33/1.38 ( empty(A) % 1.33/1.38 => function(A) ) ). % 1.33/1.38 % 1.33/1.38 fof(cc1_ordinal1,axiom, % 1.33/1.38 ! [A] : % 1.33/1.38 ( ordinal(A) % 1.33/1.38 => ( epsilon_transitive(A) % 1.33/1.38 & epsilon_connected(A) ) ) ). % 1.33/1.38 % 1.33/1.38 fof(cc1_relat_1,axiom, % 1.33/1.38 ! [A] : % 1.33/1.38 ( empty(A) % 1.33/1.38 => relation(A) ) ). % 1.33/1.38 % 1.33/1.38 fof(cc2_arytm_3,axiom, % 1.33/1.38 ! [A] : % 1.33/1.38 ( ( empty(A) % 1.33/1.38 & ordinal(A) ) % 1.33/1.38 => ( epsilon_transitive(A) % 1.33/1.38 & epsilon_connected(A) % 1.33/1.38 & ordinal(A) % 1.33/1.38 & natural(A) ) ) ). % 1.33/1.38 % 1.33/1.38 fof(cc2_finset_1,axiom, % 1.33/1.38 ! [A] : % 1.33/1.38 ( finite(A) % 1.33/1.38 => ! [B] : % 1.33/1.38 ( element(B,powerset(A)) % 1.33/1.38 => finite(B) ) ) ). % 1.33/1.38 % 1.33/1.38 fof(cc2_funct_1,axiom, % 1.33/1.39 ! [A] : % 1.33/1.39 ( ( relation(A) % 1.33/1.39 & empty(A) % 1.33/1.39 & function(A) ) % 1.33/1.39 => ( relation(A) % 1.33/1.39 & function(A) % 1.33/1.39 & one_to_one(A) ) ) ). % 1.33/1.39 % 1.33/1.39 fof(cc2_ordinal1,axiom, % 1.33/1.39 ! [A] : % 1.33/1.39 ( ( epsilon_transitive(A) % 1.33/1.39 & epsilon_connected(A) ) % 1.33/1.39 => ordinal(A) ) ). % 1.33/1.39 % 1.33/1.39 fof(cc3_ordinal1,axiom, % 1.33/1.39 ! [A] : % 1.33/1.39 ( empty(A) % 1.33/1.39 => ( epsilon_transitive(A) % 1.33/1.39 & epsilon_connected(A) % 1.33/1.39 & ordinal(A) ) ) ). % 1.33/1.39 % 1.33/1.39 fof(cc4_arytm_3,axiom, % 1.33/1.39 ! [A] : % 1.33/1.39 ( element(A,positive_rationals) % 1.33/1.39 => ( ordinal(A) % 1.33/1.39 => ( epsilon_transitive(A) % 1.33/1.39 & epsilon_connected(A) % 1.33/1.39 & ordinal(A) % 1.33/1.39 & natural(A) ) ) ) ). % 1.33/1.39 % 1.33/1.39 fof(existence_m1_subset_1,axiom, % 1.33/1.39 ! [A] : % 1.33/1.39 ? [B] : element(B,A) ). % 1.33/1.39 % 1.33/1.39 fof(fc12_relat_1,axiom, % 1.33/1.39 ( empty(empty_set) % 1.33/1.39 & relation(empty_set) % 1.33/1.39 & relation_empty_yielding(empty_set) ) ). % 1.33/1.39 % 1.33/1.39 fof(fc13_finset_1,axiom, % 1.33/1.39 ! [A,B] : % 1.33/1.39 ( ( relation(A) % 1.33/1.39 & function(A) % 1.33/1.39 & finite(B) ) % 1.33/1.39 => finite(relation_image(A,B)) ) ). % 1.33/1.39 % 1.33/1.39 fof(fc1_subset_1,axiom, % 1.33/1.39 ! [A] : ~ empty(powerset(A)) ). % 1.33/1.39 % 1.33/1.39 fof(fc1_xboole_0,axiom, % 1.33/1.39 empty(empty_set) ). % 1.33/1.39 % 1.33/1.39 fof(fc2_ordinal1,axiom, % 1.33/1.39 ( relation(empty_set) % 1.33/1.39 & relation_empty_yielding(empty_set) % 1.33/1.39 & function(empty_set) % 1.33/1.39 & one_to_one(empty_set) % 1.33/1.39 & empty(empty_set) % 1.33/1.39 & epsilon_transitive(empty_set) % 1.33/1.39 & epsilon_connected(empty_set) % 1.33/1.39 & ordinal(empty_set) ) ). % 1.33/1.39 % 1.33/1.39 fof(fc4_relat_1,axiom, % 1.33/1.39 ( empty(empty_set) % 1.33/1.39 & relation(empty_set) ) ). % 1.33/1.39 % 1.33/1.39 fof(fc6_funct_1,axiom, % 1.33/1.39 ! [A] : % 1.33/1.39 ( ( relation(A) % 1.33/1.39 & relation_non_empty(A) % 1.33/1.39 & function(A) ) % 1.33/1.39 => with_non_empty_elements(relation_rng(A)) ) ). % 1.33/1.39 % 1.33/1.39 fof(fc6_relat_1,axiom, % 1.33/1.39 ! [A] : % 1.33/1.39 ( ( ~ empty(A) % 1.33/1.39 & relation(A) ) % 1.33/1.39 => ~ empty(relation_rng(A)) ) ). % 1.33/1.39 % 1.33/1.39 fof(fc8_arytm_3,axiom, % 1.33/1.39 ~ empty(positive_rationals) ). % 1.33/1.39 % 1.33/1.39 fof(fc8_relat_1,axiom, % 1.33/1.39 ! [A] : % 1.33/1.39 ( empty(A) % 1.33/1.39 => ( empty(relation_rng(A)) % 1.33/1.39 & relation(relation_rng(A)) ) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc1_arytm_3,axiom, % 1.33/1.39 ? [A] : % 1.33/1.39 ( ~ empty(A) % 1.33/1.39 & epsilon_transitive(A) % 1.33/1.39 & epsilon_connected(A) % 1.33/1.39 & ordinal(A) % 1.33/1.39 & natural(A) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc1_finset_1,axiom, % 1.33/1.39 ? [A] : % 1.33/1.39 ( ~ empty(A) % 1.33/1.39 & finite(A) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc1_funcop_1,axiom, % 1.33/1.39 ? [A] : % 1.33/1.39 ( relation(A) % 1.33/1.39 & function(A) % 1.33/1.39 & function_yielding(A) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc1_funct_1,axiom, % 1.33/1.39 ? [A] : % 1.33/1.39 ( relation(A) % 1.33/1.39 & function(A) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc1_ordinal1,axiom, % 1.33/1.39 ? [A] : % 1.33/1.39 ( epsilon_transitive(A) % 1.33/1.39 & epsilon_connected(A) % 1.33/1.39 & ordinal(A) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc1_ordinal2,axiom, % 1.33/1.39 ? [A] : % 1.33/1.39 ( epsilon_transitive(A) % 1.33/1.39 & epsilon_connected(A) % 1.33/1.39 & ordinal(A) % 1.33/1.39 & being_limit_ordinal(A) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc1_relat_1,axiom, % 1.33/1.39 ? [A] : % 1.33/1.39 ( empty(A) % 1.33/1.39 & relation(A) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc1_subset_1,axiom, % 1.33/1.39 ! [A] : % 1.33/1.39 ( ~ empty(A) % 1.33/1.39 => ? [B] : % 1.33/1.39 ( element(B,powerset(A)) % 1.33/1.39 & ~ empty(B) ) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc1_xboole_0,axiom, % 1.33/1.39 ? [A] : empty(A) ). % 1.33/1.39 % 1.33/1.39 fof(rc2_arytm_3,axiom, % 1.33/1.39 ? [A] : % 1.33/1.39 ( element(A,positive_rationals) % 1.33/1.39 & ~ empty(A) % 1.33/1.39 & epsilon_transitive(A) % 1.33/1.39 & epsilon_connected(A) % 1.33/1.39 & ordinal(A) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc2_finset_1,axiom, % 1.33/1.39 ! [A] : % 1.33/1.39 ? [B] : % 1.33/1.39 ( element(B,powerset(A)) % 1.33/1.39 & empty(B) % 1.33/1.39 & relation(B) % 1.33/1.39 & function(B) % 1.33/1.39 & one_to_one(B) % 1.33/1.39 & epsilon_transitive(B) % 1.33/1.39 & epsilon_connected(B) % 1.33/1.39 & ordinal(B) % 1.33/1.39 & natural(B) % 1.33/1.39 & finite(B) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc2_funct_1,axiom, % 1.33/1.39 ? [A] : % 1.33/1.39 ( relation(A) % 1.33/1.39 & empty(A) % 1.33/1.39 & function(A) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc2_ordinal1,axiom, % 1.33/1.39 ? [A] : % 1.33/1.39 ( relation(A) % 1.33/1.39 & function(A) % 1.33/1.39 & one_to_one(A) % 1.33/1.39 & empty(A) % 1.33/1.39 & epsilon_transitive(A) % 1.33/1.39 & epsilon_connected(A) % 1.33/1.39 & ordinal(A) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc2_ordinal2,axiom, % 1.33/1.39 ? [A] : % 1.33/1.39 ( relation(A) % 1.33/1.39 & function(A) % 1.33/1.39 & transfinite_sequence(A) % 1.33/1.39 & ordinal_yielding(A) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc2_relat_1,axiom, % 1.33/1.39 ? [A] : % 1.33/1.39 ( ~ empty(A) % 1.33/1.39 & relation(A) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc2_subset_1,axiom, % 1.33/1.39 ! [A] : % 1.33/1.39 ? [B] : % 1.33/1.39 ( element(B,powerset(A)) % 1.33/1.39 & empty(B) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc2_xboole_0,axiom, % 1.33/1.39 ? [A] : ~ empty(A) ). % 1.33/1.39 % 1.33/1.39 fof(rc3_arytm_3,axiom, % 1.33/1.39 ? [A] : % 1.33/1.39 ( element(A,positive_rationals) % 1.33/1.39 & empty(A) % 1.33/1.39 & epsilon_transitive(A) % 1.33/1.39 & epsilon_connected(A) % 1.33/1.39 & ordinal(A) % 1.33/1.39 & natural(A) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc3_finset_1,axiom, % 1.33/1.39 ! [A] : % 1.33/1.39 ( ~ empty(A) % 1.33/1.39 => ? [B] : % 1.33/1.39 ( element(B,powerset(A)) % 1.33/1.39 & ~ empty(B) % 1.33/1.39 & finite(B) ) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc3_funct_1,axiom, % 1.33/1.39 ? [A] : % 1.33/1.39 ( relation(A) % 1.33/1.39 & function(A) % 1.33/1.39 & one_to_one(A) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc3_ordinal1,axiom, % 1.33/1.39 ? [A] : % 1.33/1.39 ( ~ empty(A) % 1.33/1.39 & epsilon_transitive(A) % 1.33/1.39 & epsilon_connected(A) % 1.33/1.39 & ordinal(A) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc3_relat_1,axiom, % 1.33/1.39 ? [A] : % 1.33/1.39 ( relation(A) % 1.33/1.39 & relation_empty_yielding(A) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc4_funct_1,axiom, % 1.33/1.39 ? [A] : % 1.33/1.39 ( relation(A) % 1.33/1.39 & relation_empty_yielding(A) % 1.33/1.39 & function(A) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc4_ordinal1,axiom, % 1.33/1.39 ? [A] : % 1.33/1.39 ( relation(A) % 1.33/1.39 & function(A) % 1.33/1.39 & transfinite_sequence(A) ) ). % 1.33/1.39 % 1.33/1.39 fof(rc5_funct_1,axiom, % 1.33/1.39 ? [A] : % 1.33/1.39 ( relation(A) % 1.33/1.39 & relation_non_empty(A) % 1.33/1.39 & function(A) ) ). % 1.33/1.39 % 1.33/1.39 fof(reflexivity_r1_tarski,axiom, % 1.33/1.39 ! [A,B] : subset(A,A) ). % 1.33/1.39 % 1.33/1.39 fof(t147_funct_1,axiom, % 1.33/1.39 ! [A,B] : % 1.33/1.39 ( ( relation(B) % 1.33/1.39 & function(B) ) % 1.33/1.39 => ( subset(A,relation_rng(B)) % 1.33/1.39 => relation_image(B,relation_inverse_image(B,A)) = A ) ) ). % 1.33/1.39 % 1.33/1.39 fof(t17_finset_1,axiom, % 1.33/1.39 ! [A,B] : % 1.33/1.39 ( ( relation(B) % 1.33/1.40 & function(B) ) % 1.33/1.40 => ( finite(A) % 1.33/1.40 => finite(relation_image(B,A)) ) ) ). % 1.33/1.40 % 1.33/1.40 fof(t1_subset,axiom, % 1.33/1.40 ! [A,B] : % 1.33/1.40 ( in(A,B) % 1.33/1.40 => element(A,B) ) ). % 1.33/1.40 % 1.33/1.40 fof(t27_finset_1,conjecture, % 1.33/1.40 ! [A,B] : % 1.33/1.40 ( ( relation(B) % 1.33/1.40 & function(B) ) % 1.33/1.40 => ( ( subset(A,relation_rng(B)) % 1.33/1.40 & finite(relation_inverse_image(B,A)) ) % 1.33/1.40 => finite(A) ) ) ). % 1.33/1.40 % 1.33/1.40 fof(t2_subset,axiom, % 1.33/1.40 ! [A,B] : % 1.33/1.40 ( element(A,B) % 1.33/1.40 => ( empty(B) % 1.33/1.40 | in(A,B) ) ) ). % 1.33/1.40 % 1.33/1.40 fof(t3_subset,axiom, % 1.33/1.40 ! [A,B] : % 1.33/1.40 ( element(A,powerset(B)) % 1.33/1.40 <=> subset(A,B) ) ). % 1.33/1.40 % 1.33/1.40 fof(t4_subset,axiom, % 1.33/1.40 ! [A,B,C] : % 1.33/1.40 ( ( in(A,B) % 1.33/1.40 & element(B,powerset(C)) ) % 1.33/1.40 => element(A,C) ) ). % 1.33/1.40 % 1.33/1.40 fof(t5_subset,axiom, % 1.33/1.40 ! [A,B,C] : % 1.33/1.40 ~ ( in(A,B) % 1.33/1.40 & element(B,powerset(C)) % 1.33/1.40 & empty(C) ) ). % 1.33/1.40 % 1.33/1.40 fof(t6_boole,axiom, % 1.33/1.40 ! [A] : % 1.33/1.40 ( empty(A) % 1.33/1.40 => A = empty_set ) ). % 1.33/1.40 % 1.33/1.40 fof(t7_boole,axiom, % 1.33/1.40 ! [A,B] : % 1.33/1.40 ~ ( in(A,B) % 1.33/1.40 & empty(B) ) ). % 1.33/1.40 % 1.33/1.40 fof(t8_boole,axiom, % 1.33/1.40 ! [A,B] : % 1.33/1.40 ~ ( empty(A) % 1.33/1.40 & A != B % 1.33/1.40 & empty(B) ) ). % 1.33/1.40 % 1.33/1.40 %------------------------------------------------------------------------------ % 1.33/1.40 %------------------------------------------- % 1.33/1.40 % Proof found % 1.33/1.40 % SZS status Theorem for theBenchmark % 1.33/1.40 % SZS output start Proof % 1.33/1.40 %ClaNum:181(EqnAxiom:36) % 1.33/1.40 %VarNum:141(SingletonVarNum:69) % 1.33/1.40 %MaxLitNum:4 % 1.33/1.40 %MaxfuncDepth:2 % 1.33/1.40 %SharedTerms:109 % 1.33/1.40 %goalClause: 81 97 126 128 138 % 1.33/1.40 %singleGoalClaCount:5 % 1.33/1.40 [37]P1(a1) % 1.33/1.40 [38]P1(a2) % 1.33/1.40 [39]P1(a23) % 1.33/1.40 [40]P1(a27) % 1.33/1.40 [41]P1(a3) % 1.33/1.40 [42]P1(a5) % 1.33/1.40 [43]P1(a8) % 1.33/1.40 [44]P1(a13) % 1.33/1.40 [45]P2(a1) % 1.33/1.40 [46]P2(a2) % 1.33/1.40 [47]P2(a23) % 1.33/1.40 [48]P2(a27) % 1.33/1.40 [49]P2(a3) % 1.33/1.40 [50]P2(a5) % 1.33/1.40 [51]P2(a8) % 1.33/1.40 [52]P2(a13) % 1.33/1.40 [53]P3(a1) % 1.33/1.40 [54]P3(a2) % 1.33/1.40 [55]P3(a23) % 1.33/1.40 [56]P3(a27) % 1.33/1.40 [57]P3(a3) % 1.33/1.40 [58]P3(a5) % 1.33/1.40 [59]P3(a8) % 1.33/1.40 [60]P3(a13) % 1.33/1.40 [64]P4(a1) % 1.33/1.40 [65]P4(a28) % 1.33/1.40 [66]P4(a4) % 1.33/1.40 [67]P4(a6) % 1.33/1.40 [68]P4(a5) % 1.33/1.40 [69]P4(a8) % 1.33/1.40 [70]P7(a24) % 1.33/1.40 [71]P8(a1) % 1.33/1.40 [72]P8(a25) % 1.33/1.40 [73]P8(a26) % 1.33/1.40 [74]P8(a6) % 1.33/1.40 [75]P8(a5) % 1.33/1.40 [76]P8(a9) % 1.33/1.40 [77]P8(a14) % 1.33/1.40 [78]P8(a17) % 1.33/1.40 [79]P8(a19) % 1.33/1.40 [80]P8(a20) % 1.33/1.40 [81]P8(a21) % 1.33/1.40 [84]P13(a1) % 1.33/1.40 [85]P13(a25) % 1.33/1.40 [86]P13(a26) % 1.33/1.40 [87]P13(a28) % 1.33/1.40 [88]P13(a6) % 1.33/1.40 [89]P13(a5) % 1.33/1.40 [90]P13(a9) % 1.33/1.40 [91]P13(a10) % 1.33/1.40 [92]P13(a14) % 1.33/1.40 [93]P13(a18) % 1.33/1.40 [94]P13(a17) % 1.33/1.40 [95]P13(a19) % 1.33/1.40 [96]P13(a20) % 1.33/1.40 [97]P13(a21) % 1.33/1.40 [98]P9(a2) % 1.33/1.40 [99]P9(a8) % 1.33/1.40 [100]P12(a1) % 1.33/1.40 [101]P12(a5) % 1.33/1.40 [102]P12(a14) % 1.33/1.40 [104]P15(a1) % 1.33/1.40 [105]P15(a18) % 1.33/1.40 [106]P15(a17) % 1.33/1.40 [107]P16(a20) % 1.33/1.40 [108]P10(a25) % 1.33/1.40 [109]P5(a27) % 1.33/1.40 [110]P17(a9) % 1.33/1.40 [111]P17(a19) % 1.33/1.40 [112]P14(a9) % 1.33/1.40 [123]P6(a3,a29) % 1.33/1.40 [124]P6(a8,a29) % 1.33/1.40 [131]~P4(a29) % 1.33/1.40 [132]~P4(a2) % 1.33/1.40 [133]~P4(a24) % 1.33/1.40 [134]~P4(a3) % 1.33/1.40 [135]~P4(a10) % 1.33/1.40 [136]~P4(a12) % 1.33/1.40 [137]~P4(a13) % 1.33/1.40 [138]~P7(a22) % 1.33/1.40 [126]P18(a22,f31(a21)) % 1.33/1.40 [128]P7(f32(a21,a22)) % 1.33/1.40 [125]P18(x1251,x1251) % 1.33/1.40 [113]P1(f7(x1131)) % 1.33/1.40 [114]P2(f7(x1141)) % 1.33/1.40 [115]P3(f7(x1151)) % 1.33/1.40 [116]P4(f7(x1161)) % 1.33/1.40 [117]P4(f11(x1171)) % 1.33/1.40 [118]P7(f7(x1181)) % 1.33/1.40 [119]P8(f7(x1191)) % 1.33/1.40 [120]P13(f7(x1201)) % 1.33/1.40 [121]P9(f7(x1211)) % 1.33/1.40 [122]P12(f7(x1221)) % 1.33/1.40 [127]P6(f15(x1271),x1271) % 1.33/1.40 [129]P6(f7(x1291),f33(x1291)) % 1.33/1.40 [130]P6(f11(x1301),f33(x1301)) % 1.33/1.40 [139]~P4(f33(x1391)) % 1.33/1.40 [140]~P4(x1401)+E(x1401,a1) % 1.33/1.40 [141]~P4(x1411)+P1(x1411) % 1.33/1.40 [142]~P1(x1421)+P2(x1421) % 1.33/1.40 [143]~P4(x1431)+P2(x1431) % 1.33/1.40 [144]~P1(x1441)+P3(x1441) % 1.33/1.40 [145]~P4(x1451)+P3(x1451) % 1.33/1.40 [146]~P4(x1461)+P7(x1461) % 1.33/1.40 [147]~P4(x1471)+P8(x1471) % 1.33/1.40 [148]~P4(x1481)+P13(x1481) % 1.33/1.40 [149]P4(x1491)+P7(f16(x1491)) % 1.33/1.40 [151]~P4(x1511)+P4(f31(x1511)) % 1.33/1.40 [152]~P4(x1521)+P13(f31(x1521)) % 1.33/1.40 [157]P4(x1571)+~P4(f30(x1571)) % 1.33/1.40 [158]P4(x1581)+~P4(f16(x1581)) % 1.33/1.40 [162]P4(x1621)+P6(f30(x1621),f33(x1621)) % 1.33/1.40 [163]P4(x1631)+P6(f16(x1631),f33(x1631)) % 1.33/1.40 [161]~P4(x1611)+~P11(x1612,x1611) % 1.33/1.40 [171]~P11(x1711,x1712)+P6(x1711,x1712) % 1.33/1.40 [175]~P11(x1752,x1751)+~P11(x1751,x1752) % 1.33/1.40 [173]~P18(x1731,x1732)+P6(x1731,f33(x1732)) % 1.33/1.40 [176]P18(x1761,x1762)+~P6(x1761,f33(x1762)) % 1.33/1.40 [153]~P2(x1531)+~P3(x1531)+P1(x1531) % 1.33/1.40 [156]~P1(x1561)+~P4(x1561)+P9(x1561) % 1.33/1.40 [166]~P1(x1661)+P9(x1661)+~P6(x1661,a29) % 1.33/1.40 [160]~P13(x1601)+P4(x1601)+~P4(f31(x1601)) % 1.33/1.40 [150]~P4(x1502)+~P4(x1501)+E(x1501,x1502) % 1.33/1.40 [168]~P6(x1681,x1682)+P1(x1681)+~P1(x1682) % 1.33/1.40 [169]~P6(x1691,x1692)+P2(x1691)+~P1(x1692) % 1.33/1.40 [170]~P6(x1701,x1702)+P3(x1701)+~P1(x1702) % 1.33/1.40 [172]~P6(x1722,x1721)+P4(x1721)+P11(x1722,x1721) % 1.33/1.40 [174]P7(x1741)+~P7(x1742)+~P6(x1741,f33(x1742)) % 1.33/1.40 [179]~P4(x1791)+~P11(x1792,x1793)+~P6(x1793,f33(x1791)) % 1.33/1.40 [180]P6(x1801,x1802)+~P11(x1801,x1803)+~P6(x1803,f33(x1802)) % 1.33/1.40 [159]~P4(x1591)+~P8(x1591)+~P13(x1591)+P12(x1591) % 1.33/1.40 [167]~P8(x1671)+~P13(x1671)+~P16(x1671)+P19(f31(x1671)) % 1.33/1.40 [178]~P7(x1782)+~P8(x1781)+~P13(x1781)+P7(f34(x1781,x1782)) % 1.33/1.40 [181]~P8(x1811)+~P13(x1811)+~P18(x1812,f31(x1811))+E(f34(x1811,f32(x1811,x1812)),x1812) % 1.33/1.40 %EqnAxiom % 1.33/1.40 [1]E(x11,x11) % 1.33/1.40 [2]E(x22,x21)+~E(x21,x22) % 1.33/1.40 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 1.33/1.40 [4]~E(x41,x42)+E(f7(x41),f7(x42)) % 1.33/1.40 [5]~E(x51,x52)+E(f31(x51),f31(x52)) % 1.33/1.40 [6]~E(x61,x62)+E(f34(x61,x63),f34(x62,x63)) % 1.33/1.40 [7]~E(x71,x72)+E(f34(x73,x71),f34(x73,x72)) % 1.33/1.40 [8]~E(x81,x82)+E(f32(x81,x83),f32(x82,x83)) % 1.33/1.40 [9]~E(x91,x92)+E(f32(x93,x91),f32(x93,x92)) % 1.33/1.40 [10]~E(x101,x102)+E(f11(x101),f11(x102)) % 1.33/1.40 [11]~E(x111,x112)+E(f33(x111),f33(x112)) % 1.33/1.40 [12]~E(x121,x122)+E(f16(x121),f16(x122)) % 1.33/1.40 [13]~E(x131,x132)+E(f30(x131),f30(x132)) % 1.33/1.40 [14]~E(x141,x142)+E(f15(x141),f15(x142)) % 1.33/1.40 [15]~P1(x151)+P1(x152)+~E(x151,x152) % 1.33/1.40 [16]P18(x162,x163)+~E(x161,x162)+~P18(x161,x163) % 1.33/1.40 [17]P18(x173,x172)+~E(x171,x172)+~P18(x173,x171) % 1.33/1.40 [18]~P13(x181)+P13(x182)+~E(x181,x182) % 1.33/1.40 [19]~P8(x191)+P8(x192)+~E(x191,x192) % 1.33/1.40 [20]P6(x202,x203)+~E(x201,x202)+~P6(x201,x203) % 1.33/1.40 [21]P6(x213,x212)+~E(x211,x212)+~P6(x213,x211) % 1.33/1.40 [22]P11(x222,x223)+~E(x221,x222)+~P11(x221,x223) % 1.33/1.40 [23]P11(x233,x232)+~E(x231,x232)+~P11(x233,x231) % 1.33/1.40 [24]~P4(x241)+P4(x242)+~E(x241,x242) % 1.33/1.40 [25]~P12(x251)+P12(x252)+~E(x251,x252) % 1.33/1.40 [26]~P2(x261)+P2(x262)+~E(x261,x262) % 1.33/1.40 [27]~P15(x271)+P15(x272)+~E(x271,x272) % 1.33/1.40 [28]~P3(x281)+P3(x282)+~E(x281,x282) % 1.33/1.40 [29]~P17(x291)+P17(x292)+~E(x291,x292) % 1.33/1.40 [30]~P14(x301)+P14(x302)+~E(x301,x302) % 1.33/1.40 [31]~P9(x311)+P9(x312)+~E(x311,x312) % 1.33/1.40 [32]~P7(x321)+P7(x322)+~E(x321,x322) % 1.33/1.40 [33]~P10(x331)+P10(x332)+~E(x331,x332) % 1.33/1.40 [34]~P5(x341)+P5(x342)+~E(x341,x342) % 1.33/1.40 [35]~P16(x351)+P16(x352)+~E(x351,x352) % 1.33/1.40 [36]~P19(x361)+P19(x362)+~E(x361,x362) % 1.33/1.40 % 1.33/1.40 %------------------------------------------- % 1.33/1.40 cnf(182,plain, % 1.33/1.40 (~P4(a22)), % 1.33/1.40 inference(scs_inference,[],[138,146])). % 1.33/1.40 cnf(184,plain, % 1.33/1.40 (P18(f15(f33(x1841)),x1841)), % 1.33/1.40 inference(scs_inference,[],[138,127,146,176])). % 1.33/1.40 cnf(185,plain, % 1.33/1.40 (P6(f15(x1851),x1851)), % 1.33/1.40 inference(rename_variables,[],[127])). % 1.33/1.40 cnf(187,plain, % 1.33/1.40 (~P11(x1871,a1)), % 1.33/1.40 inference(scs_inference,[],[138,64,127,146,176,161])). % 1.33/1.40 cnf(192,plain, % 1.33/1.40 (P11(f15(a29),a29)), % 1.33/1.40 inference(scs_inference,[],[138,128,64,127,185,130,131,146,176,161,174,172])). % 1.33/1.40 cnf(193,plain, % 1.33/1.40 (P6(f15(x1931),x1931)), % 1.33/1.40 inference(rename_variables,[],[127])). % 1.33/1.40 cnf(200,plain, % 1.33/1.40 (~P11(x2001,f15(f33(a1)))), % 1.33/1.40 inference(scs_inference,[],[138,128,64,127,185,193,130,37,41,123,131,146,176,161,174,172,23,156,166,179])). % 1.33/1.40 cnf(201,plain, % 1.33/1.40 (P6(f15(x2011),x2011)), % 1.33/1.40 inference(rename_variables,[],[127])). % 1.33/1.40 cnf(207,plain, % 1.33/1.40 (P18(x2071,f31(a21))+~E(a22,x2071)), % 1.33/1.40 inference(scs_inference,[],[138,126,128,64,67,74,88,127,185,193,130,37,41,123,131,146,176,161,174,172,23,156,166,179,159,175,16])). % 1.33/1.40 cnf(210,plain, % 1.33/1.40 (P6(f15(x2101),x2102)+~E(x2101,x2102)), % 1.33/1.40 inference(scs_inference,[],[138,126,128,64,67,74,88,127,185,193,201,130,37,41,123,131,146,176,161,174,172,23,156,166,179,159,175,16,17,20,21])). % 1.33/1.40 cnf(222,plain, % 1.33/1.40 (P18(f7(x2221),x2221)), % 1.33/1.40 inference(scs_inference,[],[65,129,161,176])). % 1.33/1.40 cnf(227,plain, % 1.33/1.40 (P6(f15(x2271),x2271)), % 1.33/1.40 inference(rename_variables,[],[127])). % 1.33/1.40 cnf(230,plain, % 1.33/1.40 (P6(f7(x2301),f33(x2301))), % 1.33/1.40 inference(rename_variables,[],[129])). % 1.33/1.40 cnf(243,plain, % 1.33/1.40 (P18(x2431,x2432)+~E(x2432,x2431)), % 1.33/1.40 inference(scs_inference,[],[182,64,125,192,65,68,200,129,230,42,127,227,161,176,156,172,179,23,175,166,20,21,180,16])). % 1.33/1.40 cnf(244,plain, % 1.33/1.40 (P18(x2441,x2442)+~E(x2441,x2442)), % 1.33/1.40 inference(scs_inference,[],[182,64,125,192,65,68,200,129,230,42,127,227,161,176,156,172,179,23,175,166,20,21,180,16,17])). % 1.33/1.40 cnf(249,plain, % 1.33/1.40 (~P11(x2491,a4)), % 1.33/1.40 inference(scs_inference,[],[66,161])). % 1.33/1.40 cnf(251,plain, % 1.33/1.40 (P18(f11(x2511),x2511)), % 1.33/1.40 inference(scs_inference,[],[66,130,161,176])). % 1.33/1.40 cnf(253,plain, % 1.33/1.40 (P11(f15(a2),a2)), % 1.33/1.40 inference(scs_inference,[],[66,130,132,127,161,176,172])). % 1.33/1.40 cnf(256,plain, % 1.33/1.40 (~P11(x2561,f11(a1))), % 1.33/1.40 inference(scs_inference,[],[64,66,130,132,127,161,176,172,179])). % 1.33/1.40 cnf(277,plain, % 1.33/1.40 (P11(f15(a24),a24)), % 1.33/1.40 inference(scs_inference,[],[69,133,127,161,172])). % 1.33/1.40 cnf(288,plain, % 1.33/1.40 (P18(f11(x2881),x2882)+~E(x2881,x2882)), % 1.33/1.40 inference(scs_inference,[],[251,253,69,117,124,256,133,127,161,172,23,175,156,22,21,17])). % 1.33/1.40 cnf(296,plain, % 1.33/1.40 (~P11(x2961,f7(x2962))), % 1.33/1.40 inference(scs_inference,[],[116,161])). % 1.33/1.40 cnf(298,plain, % 1.33/1.40 (P11(f15(a3),a3)), % 1.33/1.40 inference(scs_inference,[],[116,134,127,161,172])). % 1.33/1.40 cnf(309,plain, % 1.33/1.40 (P18(f15(f33(x3091)),x3092)+~E(x3091,x3092)), % 1.33/1.40 inference(scs_inference,[],[184,277,116,65,123,187,134,127,161,172,23,175,156,22,21,17])). % 1.33/1.40 cnf(329,plain, % 1.33/1.40 (P18(f7(x3291),x3292)+~E(x3291,x3292)), % 1.33/1.40 inference(scs_inference,[],[298,222,67,296,135,127,161,172,23,175,156,22,17])). % 1.33/1.40 cnf(604,plain, % 1.33/1.40 (E(a22,f34(a21,f32(a21,a22)))), % 1.33/1.40 inference(scs_inference,[],[126,97,81,2,181])). % 1.33/1.40 cnf(617,plain, % 1.33/1.40 ($false), % 1.33/1.40 inference(scs_inference,[],[81,138,97,128,182,298,604,249,207,243,244,288,309,329,210,2,32,24,23,178]), % 1.33/1.40 ['proof']). % 1.33/1.40 % SZS output end Proof % 1.33/1.40 % Total time :0.780000s %------------------------------------------------------------------------------