%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU148+2 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n019.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:19 EDT 2024 % Result : Theorem 0.53s 0.72s % Output : CNFRefutation 0.71s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU148+2 : TPTP v8.2.0. Released v3.3.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n019.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:28:23 EDT 2024 % 0.12/0.33 % CPUTime : % 0.50/0.57 start to proof:theBenchmark % 0.53/0.70 %------------------------------------------- % 0.53/0.70 % File :CSE---1.7 % 0.53/0.70 % Problem :theBenchmark % 0.53/0.70 % Transform :cnf % 0.53/0.70 % Format :tptp:raw % 0.53/0.70 % Command :java -jar mcs_scs.jar %d %s % 0.53/0.70 % 0.53/0.70 % Result :Theorem 0.080000s % 0.53/0.70 % Output :CNFRefutation 0.080000s % 0.53/0.70 %------------------------------------------- % 0.53/0.70 %------------------------------------------------------------------------------ % 0.53/0.70 % File : SEU148+2 : TPTP v8.2.0. Released v3.3.0. % 0.53/0.70 % Domain : Set theory % 0.53/0.70 % Problem : MPTP chainy problem t6_zfmisc_1 % 0.53/0.70 % Version : [Urb07] axioms : Especial. % 0.53/0.70 % English : % 0.53/0.70 % 0.53/0.70 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 0.53/0.70 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 0.53/0.70 % Source : [Urb07] % 0.53/0.70 % Names : chainy-t6_zfmisc_1 [Urb07] % 0.53/0.70 % 0.53/0.70 % Status : Theorem % 0.53/0.70 % Rating : 0.11 v7.5.0, 0.12 v7.4.0, 0.03 v7.1.0, 0.04 v7.0.0, 0.03 v6.4.0, 0.08 v6.2.0, 0.20 v6.1.0, 0.27 v6.0.0, 0.26 v5.5.0, 0.19 v5.4.0, 0.21 v5.3.0, 0.26 v5.2.0, 0.05 v5.0.0, 0.12 v4.1.0, 0.17 v4.0.1, 0.22 v4.0.0, 0.25 v3.7.0, 0.20 v3.5.0, 0.21 v3.3.0 % 0.53/0.70 % Syntax : Number of formulae : 71 ( 31 unt; 0 def) % 0.53/0.71 % Number of atoms : 138 ( 41 equ) % 0.53/0.71 % Maximal formula atoms : 6 ( 1 avg) % 0.53/0.71 % Number of connectives : 91 ( 24 ~; 4 |; 20 &) % 0.53/0.71 % ( 23 <=>; 20 =>; 0 <=; 0 <~>) % 0.53/0.71 % Maximal formula depth : 9 ( 4 avg) % 0.53/0.71 % Maximal term depth : 3 ( 1 avg) % 0.53/0.71 % Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty) % 0.53/0.71 % Number of functors : 7 ( 7 usr; 1 con; 0-2 aty) % 0.53/0.71 % Number of variables : 136 ( 132 !; 4 ?) % 0.53/0.71 % SPC : FOF_THM_RFO_SEQ % 0.53/0.71 % 0.53/0.71 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 0.53/0.71 % library, www.mizar.org % 0.53/0.71 %------------------------------------------------------------------------------ % 0.53/0.71 fof(antisymmetry_r2_hidden,axiom, % 0.53/0.71 ! [A,B] : % 0.53/0.71 ( in(A,B) % 0.53/0.71 => ~ in(B,A) ) ). % 0.53/0.71 % 0.53/0.71 fof(antisymmetry_r2_xboole_0,axiom, % 0.53/0.71 ! [A,B] : % 0.53/0.71 ( proper_subset(A,B) % 0.53/0.71 => ~ proper_subset(B,A) ) ). % 0.53/0.71 % 0.53/0.71 fof(commutativity_k2_tarski,axiom, % 0.53/0.71 ! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) ). % 0.53/0.71 % 0.53/0.71 fof(commutativity_k2_xboole_0,axiom, % 0.53/0.71 ! [A,B] : set_union2(A,B) = set_union2(B,A) ). % 0.53/0.71 % 0.53/0.71 fof(commutativity_k3_xboole_0,axiom, % 0.53/0.71 ! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) ). % 0.53/0.71 % 0.53/0.71 fof(d10_xboole_0,axiom, % 0.53/0.71 ! [A,B] : % 0.53/0.71 ( A = B % 0.53/0.71 <=> ( subset(A,B) % 0.53/0.71 & subset(B,A) ) ) ). % 0.53/0.71 % 0.53/0.71 fof(d1_tarski,axiom, % 0.53/0.71 ! [A,B] : % 0.53/0.71 ( B = singleton(A) % 0.53/0.71 <=> ! [C] : % 0.53/0.71 ( in(C,B) % 0.53/0.71 <=> C = A ) ) ). % 0.53/0.71 % 0.53/0.71 fof(d1_xboole_0,axiom, % 0.53/0.71 ! [A] : % 0.53/0.71 ( A = empty_set % 0.53/0.71 <=> ! [B] : ~ in(B,A) ) ). % 0.53/0.71 % 0.53/0.71 fof(d1_zfmisc_1,axiom, % 0.53/0.71 ! [A,B] : % 0.53/0.71 ( B = powerset(A) % 0.53/0.71 <=> ! [C] : % 0.53/0.71 ( in(C,B) % 0.53/0.71 <=> subset(C,A) ) ) ). % 0.53/0.71 % 0.53/0.71 fof(d2_tarski,axiom, % 0.53/0.71 ! [A,B,C] : % 0.53/0.71 ( C = unordered_pair(A,B) % 0.53/0.71 <=> ! [D] : % 0.53/0.71 ( in(D,C) % 0.53/0.71 <=> ( D = A % 0.53/0.71 | D = B ) ) ) ). % 0.53/0.71 % 0.53/0.71 fof(d2_xboole_0,axiom, % 0.53/0.71 ! [A,B,C] : % 0.53/0.71 ( C = set_union2(A,B) % 0.53/0.71 <=> ! [D] : % 0.53/0.71 ( in(D,C) % 0.53/0.71 <=> ( in(D,A) % 0.53/0.71 | in(D,B) ) ) ) ). % 0.53/0.71 % 0.53/0.71 fof(d3_tarski,axiom, % 0.53/0.71 ! [A,B] : % 0.53/0.71 ( subset(A,B) % 0.53/0.71 <=> ! [C] : % 0.53/0.71 ( in(C,A) % 0.53/0.71 => in(C,B) ) ) ). % 0.53/0.71 % 0.53/0.71 fof(d3_xboole_0,axiom, % 0.53/0.71 ! [A,B,C] : % 0.53/0.71 ( C = set_intersection2(A,B) % 0.53/0.71 <=> ! [D] : % 0.53/0.71 ( in(D,C) % 0.53/0.71 <=> ( in(D,A) % 0.53/0.71 & in(D,B) ) ) ) ). % 0.53/0.71 % 0.53/0.71 fof(d4_xboole_0,axiom, % 0.53/0.71 ! [A,B,C] : % 0.53/0.71 ( C = set_difference(A,B) % 0.53/0.71 <=> ! [D] : % 0.53/0.71 ( in(D,C) % 0.53/0.71 <=> ( in(D,A) % 0.53/0.71 & ~ in(D,B) ) ) ) ). % 0.53/0.71 % 0.53/0.71 fof(d7_xboole_0,axiom, % 0.53/0.71 ! [A,B] : % 0.53/0.71 ( disjoint(A,B) % 0.53/0.71 <=> set_intersection2(A,B) = empty_set ) ). % 0.53/0.71 % 0.53/0.71 fof(d8_xboole_0,axiom, % 0.53/0.71 ! [A,B] : % 0.53/0.71 ( proper_subset(A,B) % 0.53/0.71 <=> ( subset(A,B) % 0.53/0.71 & A != B ) ) ). % 0.53/0.71 % 0.53/0.71 fof(dt_k1_tarski,axiom, % 0.53/0.71 $true ). % 0.53/0.71 % 0.53/0.71 fof(dt_k1_xboole_0,axiom, % 0.53/0.71 $true ). % 0.53/0.71 % 0.53/0.71 fof(dt_k1_zfmisc_1,axiom, % 0.53/0.71 $true ). % 0.53/0.71 % 0.53/0.71 fof(dt_k2_tarski,axiom, % 0.53/0.71 $true ). % 0.53/0.71 % 0.53/0.71 fof(dt_k2_xboole_0,axiom, % 0.53/0.71 $true ). % 0.53/0.71 % 0.53/0.71 fof(dt_k3_xboole_0,axiom, % 0.53/0.71 $true ). % 0.53/0.71 % 0.53/0.71 fof(dt_k4_xboole_0,axiom, % 0.53/0.71 $true ). % 0.53/0.71 % 0.53/0.71 fof(fc1_xboole_0,axiom, % 0.53/0.71 empty(empty_set) ). % 0.53/0.71 % 0.53/0.71 fof(fc2_xboole_0,axiom, % 0.53/0.71 ! [A,B] : % 0.53/0.71 ( ~ empty(A) % 0.53/0.71 => ~ empty(set_union2(A,B)) ) ). % 0.53/0.71 % 0.53/0.71 fof(fc3_xboole_0,axiom, % 0.53/0.71 ! [A,B] : % 0.53/0.71 ( ~ empty(A) % 0.53/0.71 => ~ empty(set_union2(B,A)) ) ). % 0.53/0.71 % 0.53/0.71 fof(idempotence_k2_xboole_0,axiom, % 0.53/0.71 ! [A,B] : set_union2(A,A) = A ). % 0.53/0.71 % 0.53/0.71 fof(idempotence_k3_xboole_0,axiom, % 0.53/0.71 ! [A,B] : set_intersection2(A,A) = A ). % 0.53/0.71 % 0.53/0.71 fof(irreflexivity_r2_xboole_0,axiom, % 0.53/0.71 ! [A,B] : ~ proper_subset(A,A) ). % 0.53/0.71 % 0.53/0.71 fof(l1_zfmisc_1,lemma, % 0.53/0.71 ! [A] : singleton(A) != empty_set ). % 0.53/0.71 % 0.53/0.71 fof(l2_zfmisc_1,lemma, % 0.53/0.71 ! [A,B] : % 0.53/0.71 ( subset(singleton(A),B) % 0.53/0.71 <=> in(A,B) ) ). % 0.53/0.71 % 0.53/0.71 fof(l32_xboole_1,lemma, % 0.53/0.71 ! [A,B] : % 0.53/0.71 ( set_difference(A,B) = empty_set % 0.53/0.71 <=> subset(A,B) ) ). % 0.53/0.71 % 0.53/0.71 fof(l3_zfmisc_1,lemma, % 0.53/0.71 ! [A,B,C] : % 0.53/0.71 ( subset(A,B) % 0.53/0.71 => ( in(C,A) % 0.53/0.71 | subset(A,set_difference(B,singleton(C))) ) ) ). % 0.53/0.71 % 0.53/0.71 fof(l4_zfmisc_1,lemma, % 0.53/0.71 ! [A,B] : % 0.53/0.71 ( subset(A,singleton(B)) % 0.53/0.71 <=> ( A = empty_set % 0.53/0.71 | A = singleton(B) ) ) ). % 0.53/0.71 % 0.53/0.71 fof(rc1_xboole_0,axiom, % 0.53/0.71 ? [A] : empty(A) ). % 0.53/0.71 % 0.53/0.71 fof(rc2_xboole_0,axiom, % 0.53/0.71 ? [A] : ~ empty(A) ). % 0.53/0.71 % 0.53/0.71 fof(reflexivity_r1_tarski,axiom, % 0.53/0.71 ! [A,B] : subset(A,A) ). % 0.53/0.71 % 0.53/0.71 fof(symmetry_r1_xboole_0,axiom, % 0.53/0.71 ! [A,B] : % 0.53/0.71 ( disjoint(A,B) % 0.53/0.71 => disjoint(B,A) ) ). % 0.53/0.71 % 0.53/0.71 fof(t12_xboole_1,lemma, % 0.53/0.71 ! [A,B] : % 0.53/0.71 ( subset(A,B) % 0.53/0.71 => set_union2(A,B) = B ) ). % 0.53/0.71 % 0.53/0.71 fof(t17_xboole_1,lemma, % 0.53/0.71 ! [A,B] : subset(set_intersection2(A,B),A) ). % 0.53/0.71 % 0.53/0.71 fof(t19_xboole_1,lemma, % 0.53/0.71 ! [A,B,C] : % 0.53/0.71 ( ( subset(A,B) % 0.53/0.71 & subset(A,C) ) % 0.53/0.71 => subset(A,set_intersection2(B,C)) ) ). % 0.53/0.71 % 0.53/0.71 fof(t1_boole,axiom, % 0.53/0.71 ! [A] : set_union2(A,empty_set) = A ). % 0.53/0.71 % 0.53/0.71 fof(t1_xboole_1,lemma, % 0.53/0.71 ! [A,B,C] : % 0.53/0.71 ( ( subset(A,B) % 0.53/0.71 & subset(B,C) ) % 0.53/0.71 => subset(A,C) ) ). % 0.53/0.71 % 0.53/0.71 fof(t1_zfmisc_1,lemma, % 0.53/0.71 powerset(empty_set) = singleton(empty_set) ). % 0.53/0.71 % 0.53/0.71 fof(t26_xboole_1,lemma, % 0.53/0.71 ! [A,B,C] : % 0.53/0.71 ( subset(A,B) % 0.53/0.71 => subset(set_intersection2(A,C),set_intersection2(B,C)) ) ). % 0.53/0.71 % 0.53/0.71 fof(t28_xboole_1,lemma, % 0.53/0.71 ! [A,B] : % 0.53/0.71 ( subset(A,B) % 0.53/0.71 => set_intersection2(A,B) = A ) ). % 0.53/0.71 % 0.53/0.71 fof(t2_boole,axiom, % 0.53/0.71 ! [A] : set_intersection2(A,empty_set) = empty_set ). % 0.53/0.71 % 0.53/0.71 fof(t2_tarski,axiom, % 0.53/0.71 ! [A,B] : % 0.53/0.71 ( ! [C] : % 0.53/0.71 ( in(C,A) % 0.53/0.71 <=> in(C,B) ) % 0.53/0.71 => A = B ) ). % 0.53/0.71 % 0.53/0.71 fof(t2_xboole_1,lemma, % 0.53/0.71 ! [A] : subset(empty_set,A) ). % 0.53/0.71 % 0.53/0.71 fof(t33_xboole_1,lemma, % 0.53/0.71 ! [A,B,C] : % 0.53/0.71 ( subset(A,B) % 0.53/0.71 => subset(set_difference(A,C),set_difference(B,C)) ) ). % 0.53/0.71 % 0.53/0.71 fof(t36_xboole_1,lemma, % 0.53/0.71 ! [A,B] : subset(set_difference(A,B),A) ). % 0.53/0.71 % 0.53/0.71 fof(t37_xboole_1,lemma, % 0.53/0.72 ! [A,B] : % 0.53/0.72 ( set_difference(A,B) = empty_set % 0.53/0.72 <=> subset(A,B) ) ). % 0.53/0.72 % 0.53/0.72 fof(t39_xboole_1,lemma, % 0.53/0.72 ! [A,B] : set_union2(A,set_difference(B,A)) = set_union2(A,B) ). % 0.53/0.72 % 0.53/0.72 fof(t3_boole,axiom, % 0.53/0.72 ! [A] : set_difference(A,empty_set) = A ). % 0.53/0.72 % 0.53/0.72 fof(t3_xboole_0,lemma, % 0.53/0.72 ! [A,B] : % 0.53/0.72 ( ~ ( ~ disjoint(A,B) % 0.53/0.72 & ! [C] : % 0.53/0.72 ~ ( in(C,A) % 0.53/0.72 & in(C,B) ) ) % 0.53/0.72 & ~ ( ? [C] : % 0.53/0.72 ( in(C,A) % 0.53/0.72 & in(C,B) ) % 0.53/0.72 & disjoint(A,B) ) ) ). % 0.53/0.72 % 0.53/0.72 fof(t3_xboole_1,lemma, % 0.53/0.72 ! [A] : % 0.53/0.72 ( subset(A,empty_set) % 0.53/0.72 => A = empty_set ) ). % 0.53/0.72 % 0.53/0.72 fof(t40_xboole_1,lemma, % 0.53/0.72 ! [A,B] : set_difference(set_union2(A,B),B) = set_difference(A,B) ). % 0.53/0.72 % 0.53/0.72 fof(t45_xboole_1,lemma, % 0.53/0.72 ! [A,B] : % 0.53/0.72 ( subset(A,B) % 0.53/0.72 => B = set_union2(A,set_difference(B,A)) ) ). % 0.53/0.72 % 0.53/0.72 fof(t48_xboole_1,lemma, % 0.53/0.72 ! [A,B] : set_difference(A,set_difference(A,B)) = set_intersection2(A,B) ). % 0.53/0.72 % 0.53/0.72 fof(t4_boole,axiom, % 0.53/0.72 ! [A] : set_difference(empty_set,A) = empty_set ). % 0.53/0.72 % 0.53/0.72 fof(t4_xboole_0,lemma, % 0.53/0.72 ! [A,B] : % 0.53/0.72 ( ~ ( ~ disjoint(A,B) % 0.53/0.72 & ! [C] : ~ in(C,set_intersection2(A,B)) ) % 0.53/0.72 & ~ ( ? [C] : in(C,set_intersection2(A,B)) % 0.53/0.72 & disjoint(A,B) ) ) ). % 0.53/0.72 % 0.53/0.72 fof(t60_xboole_1,lemma, % 0.53/0.72 ! [A,B] : % 0.53/0.72 ~ ( subset(A,B) % 0.53/0.72 & proper_subset(B,A) ) ). % 0.53/0.72 % 0.53/0.72 fof(t63_xboole_1,lemma, % 0.53/0.72 ! [A,B,C] : % 0.53/0.72 ( ( subset(A,B) % 0.53/0.72 & disjoint(B,C) ) % 0.53/0.72 => disjoint(A,C) ) ). % 0.53/0.72 % 0.53/0.72 fof(t69_enumset1,lemma, % 0.53/0.72 ! [A] : unordered_pair(A,A) = singleton(A) ). % 0.53/0.72 % 0.53/0.72 fof(t6_boole,axiom, % 0.53/0.72 ! [A] : % 0.53/0.72 ( empty(A) % 0.53/0.72 => A = empty_set ) ). % 0.53/0.72 % 0.53/0.72 fof(t6_zfmisc_1,conjecture, % 0.53/0.72 ! [A,B] : % 0.53/0.72 ( subset(singleton(A),singleton(B)) % 0.53/0.72 => A = B ) ). % 0.53/0.72 % 0.53/0.72 fof(t7_boole,axiom, % 0.53/0.72 ! [A,B] : % 0.53/0.72 ~ ( in(A,B) % 0.53/0.72 & empty(B) ) ). % 0.53/0.72 % 0.53/0.72 fof(t7_xboole_1,lemma, % 0.53/0.72 ! [A,B] : subset(A,set_union2(A,B)) ). % 0.53/0.72 % 0.53/0.72 fof(t83_xboole_1,lemma, % 0.53/0.72 ! [A,B] : % 0.53/0.72 ( disjoint(A,B) % 0.53/0.72 <=> set_difference(A,B) = A ) ). % 0.53/0.72 % 0.53/0.72 fof(t8_boole,axiom, % 0.53/0.72 ! [A,B] : % 0.53/0.72 ~ ( empty(A) % 0.53/0.72 & A != B % 0.53/0.72 & empty(B) ) ). % 0.53/0.72 % 0.53/0.72 fof(t8_xboole_1,lemma, % 0.53/0.72 ! [A,B,C] : % 0.53/0.72 ( ( subset(A,B) % 0.53/0.72 & subset(C,B) ) % 0.53/0.72 => subset(set_union2(A,C),B) ) ). % 0.53/0.72 % 0.53/0.72 %------------------------------------------------------------------------------ % 0.53/0.72 %------------------------------------------- % 0.53/0.72 % Proof found % 0.53/0.72 % SZS status Theorem for theBenchmark % 0.53/0.72 % SZS output start Proof % 0.53/0.72 %ClaNum:151(EqnAxiom:44) % 0.53/0.72 %VarNum:581(SingletonVarNum:222) % 0.71/0.72 %MaxLitNum:4 % 0.71/0.72 %MaxfuncDepth:2 % 0.71/0.72 %SharedTerms:15 % 0.71/0.72 %goalClause: 62 65 % 0.71/0.72 %singleGoalClaCount:2 % 0.71/0.72 [45]P1(a1) % 0.71/0.72 [46]P1(a2) % 0.71/0.72 [65]~E(a8,a3) % 0.71/0.72 [66]~P1(a4) % 0.71/0.72 [51]E(f20(a1,a1),f18(a1)) % 0.71/0.72 [62]P3(f20(a3,a3),f20(a8,a8)) % 0.71/0.72 [48]P3(a1,x481) % 0.71/0.72 [52]P3(x521,x521) % 0.71/0.72 [68]~P4(x681,x681) % 0.71/0.72 [47]E(f17(a1,x471),a1) % 0.71/0.72 [49]E(f19(x491,a1),x491) % 0.71/0.72 [50]E(f17(x501,a1),x501) % 0.71/0.72 [53]E(f19(x531,x531),x531) % 0.71/0.72 [67]~E(f20(x671,x671),a1) % 0.71/0.72 [56]E(f17(x561,f17(x561,a1)),a1) % 0.71/0.72 [59]E(f17(x591,f17(x591,x591)),x591) % 0.71/0.72 [54]E(f20(x541,x542),f20(x542,x541)) % 0.71/0.72 [55]E(f19(x551,x552),f19(x552,x551)) % 0.71/0.72 [57]P3(x571,f19(x571,x572)) % 0.71/0.72 [58]P3(f17(x581,x582),x581) % 0.71/0.72 [60]E(f19(x601,f17(x602,x601)),f19(x601,x602)) % 0.71/0.72 [61]E(f17(f19(x611,x612),x612),f17(x611,x612)) % 0.71/0.72 [63]E(f17(x631,f17(x631,x632)),f17(x632,f17(x632,x631))) % 0.71/0.72 [69]~P1(x691)+E(x691,a1) % 0.71/0.72 [73]~P3(x731,a1)+E(x731,a1) % 0.71/0.72 [74]P5(f9(x741),x741)+E(x741,a1) % 0.71/0.72 [72]~E(x721,x722)+P3(x721,x722) % 0.71/0.72 [75]~P5(x752,x751)+~E(x751,a1) % 0.71/0.72 [76]~P4(x761,x762)+~E(x761,x762) % 0.71/0.72 [77]~P1(x771)+~P5(x772,x771) % 0.71/0.72 [82]~P4(x821,x822)+P3(x821,x822) % 0.71/0.72 [83]~P2(x832,x831)+P2(x831,x832) % 0.71/0.72 [92]~P5(x922,x921)+~P5(x921,x922) % 0.71/0.72 [93]~P4(x932,x931)+~P4(x931,x932) % 0.71/0.72 [94]~P3(x942,x941)+~P4(x941,x942) % 0.71/0.72 [79]~P3(x791,x792)+E(f17(x791,x792),a1) % 0.71/0.72 [81]P3(x811,x812)+~E(f17(x811,x812),a1) % 0.71/0.72 [84]~P3(x841,x842)+E(f19(x841,x842),x842) % 0.71/0.72 [85]~P2(x851,x852)+E(f17(x851,x852),x851) % 0.71/0.72 [86]P2(x861,x862)+~E(f17(x861,x862),x861) % 0.71/0.72 [91]~E(x911,a1)+P3(x911,f20(x912,x912)) % 0.71/0.72 [100]P1(x1001)+~P1(f19(x1002,x1001)) % 0.71/0.72 [101]P1(x1011)+~P1(f19(x1011,x1012)) % 0.71/0.72 [102]P3(x1021,x1022)+P5(f11(x1021,x1022),x1021) % 0.71/0.72 [103]P2(x1031,x1032)+P5(f5(x1031,x1032),x1032) % 0.71/0.72 [104]P2(x1041,x1042)+P5(f5(x1041,x1042),x1041) % 0.71/0.72 [112]~P5(x1121,x1122)+P3(f20(x1121,x1121),x1122) % 0.71/0.72 [122]P5(x1221,x1222)+~P3(f20(x1221,x1221),x1222) % 0.71/0.72 [123]P3(x1231,x1232)+~P5(f11(x1231,x1232),x1232) % 0.71/0.72 [111]~P2(x1111,x1112)+E(f17(x1111,f17(x1111,x1112)),a1) % 0.71/0.72 [113]~P3(x1131,x1132)+E(f19(x1131,f17(x1132,x1131)),x1132) % 0.71/0.72 [114]~P3(x1141,x1142)+E(f17(x1141,f17(x1141,x1142)),x1141) % 0.71/0.72 [121]P2(x1211,x1212)+~E(f17(x1211,f17(x1211,x1212)),a1) % 0.71/0.72 [136]P2(x1361,x1362)+P5(f7(x1361,x1362),f17(x1361,f17(x1361,x1362))) % 0.71/0.72 [128]~P3(x1281,x1283)+P3(f17(x1281,x1282),f17(x1283,x1282)) % 0.71/0.72 [138]~P2(x1381,x1382)+~P5(x1383,f17(x1381,f17(x1381,x1382))) % 0.71/0.72 [139]~P3(x1391,x1393)+P3(f17(x1391,f17(x1391,x1392)),f17(x1393,f17(x1393,x1392))) % 0.71/0.72 [70]~P1(x702)+~P1(x701)+E(x701,x702) % 0.71/0.72 [87]P4(x871,x872)+~P3(x871,x872)+E(x871,x872) % 0.71/0.72 [97]~P3(x972,x971)+~P3(x971,x972)+E(x971,x972) % 0.71/0.72 [118]E(f10(x1182,x1181),x1182)+P5(f10(x1182,x1181),x1181)+E(x1181,f20(x1182,x1182)) % 0.71/0.72 [124]E(x1241,f20(x1242,x1242))+~P3(x1241,f20(x1242,x1242))+E(x1241,a1) % 0.71/0.72 [125]E(x1251,x1252)+P5(f6(x1251,x1252),x1252)+P5(f6(x1251,x1252),x1251) % 0.71/0.72 [127]P5(f12(x1272,x1271),x1271)+P3(f12(x1272,x1271),x1272)+E(x1271,f18(x1272)) % 0.71/0.72 [131]~E(f10(x1312,x1311),x1312)+~P5(f10(x1312,x1311),x1311)+E(x1311,f20(x1312,x1312)) % 0.71/0.72 [133]E(x1331,x1332)+~P5(f6(x1331,x1332),x1332)+~P5(f6(x1331,x1332),x1331) % 0.71/0.72 [135]~P5(f12(x1352,x1351),x1351)+~P3(f12(x1352,x1351),x1352)+E(x1351,f18(x1352)) % 0.71/0.72 [105]~P3(x1053,x1052)+P5(x1051,x1052)+~P5(x1051,x1053) % 0.71/0.72 [106]~P3(x1061,x1063)+P3(x1061,x1062)+~P3(x1063,x1062) % 0.71/0.72 [107]~P2(x1073,x1072)+P2(x1071,x1072)+~P3(x1071,x1073) % 0.71/0.72 [116]~P2(x1163,x1162)+~P5(x1161,x1162)+~P5(x1161,x1163) % 0.71/0.72 [95]~P3(x951,x953)+P5(x951,x952)+~E(x952,f18(x953)) % 0.71/0.72 [96]~P5(x961,x963)+P3(x961,x962)+~E(x963,f18(x962)) % 0.71/0.72 [98]~P5(x981,x983)+E(x981,x982)+~E(x983,f20(x982,x982)) % 0.71/0.72 [126]~P3(x1262,x1263)+~P3(x1261,x1263)+P3(f19(x1261,x1262),x1263) % 0.71/0.72 [141]P5(f15(x1412,x1413,x1411),x1411)+P5(f15(x1412,x1413,x1411),x1412)+E(x1411,f17(x1412,x1413)) % 0.71/0.72 [144]~E(f13(x1442,x1443,x1441),x1443)+~P5(f13(x1442,x1443,x1441),x1441)+E(x1441,f20(x1442,x1443)) % 0.71/0.72 [145]~E(f13(x1452,x1453,x1451),x1452)+~P5(f13(x1452,x1453,x1451),x1451)+E(x1451,f20(x1452,x1453)) % 0.71/0.72 [146]P5(f15(x1462,x1463,x1461),x1461)+~P5(f15(x1462,x1463,x1461),x1463)+E(x1461,f17(x1462,x1463)) % 0.71/0.72 [148]~P5(f14(x1482,x1483,x1481),x1481)+~P5(f14(x1482,x1483,x1481),x1483)+E(x1481,f19(x1482,x1483)) % 0.71/0.72 [149]~P5(f14(x1492,x1493,x1491),x1491)+~P5(f14(x1492,x1493,x1491),x1492)+E(x1491,f19(x1492,x1493)) % 0.71/0.72 [134]~P3(x1342,x1343)+P5(x1341,x1342)+P3(x1342,f17(x1343,f20(x1341,x1341))) % 0.71/0.72 [137]~P3(x1371,x1373)+~P3(x1371,x1372)+P3(x1371,f17(x1372,f17(x1372,x1373))) % 0.71/0.72 [142]P5(f16(x1422,x1423,x1421),x1421)+P5(f16(x1422,x1423,x1421),x1423)+E(x1421,f17(x1422,f17(x1422,x1423))) % 0.71/0.72 [143]P5(f16(x1432,x1433,x1431),x1431)+P5(f16(x1432,x1433,x1431),x1432)+E(x1431,f17(x1432,f17(x1432,x1433))) % 0.71/0.72 [88]P5(x881,x882)+~E(x881,x883)+~E(x882,f20(x884,x883)) % 0.71/0.72 [89]P5(x891,x892)+~E(x891,x893)+~E(x892,f20(x893,x894)) % 0.71/0.72 [108]~P5(x1081,x1084)+P5(x1081,x1082)+~E(x1082,f19(x1083,x1084)) % 0.71/0.72 [109]~P5(x1091,x1093)+P5(x1091,x1092)+~E(x1092,f19(x1093,x1094)) % 0.71/0.72 [110]~P5(x1101,x1103)+P5(x1101,x1102)+~E(x1103,f17(x1102,x1104)) % 0.71/0.72 [117]~P5(x1174,x1173)+~P5(x1174,x1171)+~E(x1171,f17(x1172,x1173)) % 0.71/0.72 [129]~P5(x1291,x1293)+P5(x1291,x1292)+~E(x1293,f17(x1294,f17(x1294,x1292))) % 0.71/0.72 [140]E(f13(x1402,x1403,x1401),x1403)+E(f13(x1402,x1403,x1401),x1402)+P5(f13(x1402,x1403,x1401),x1401)+E(x1401,f20(x1402,x1403)) % 0.71/0.72 [147]P5(f14(x1472,x1473,x1471),x1471)+P5(f14(x1472,x1473,x1471),x1473)+P5(f14(x1472,x1473,x1471),x1472)+E(x1471,f19(x1472,x1473)) % 0.71/0.72 [150]P5(f15(x1502,x1503,x1501),x1503)+~P5(f15(x1502,x1503,x1501),x1501)+~P5(f15(x1502,x1503,x1501),x1502)+E(x1501,f17(x1502,x1503)) % 0.71/0.72 [151]~P5(f16(x1512,x1513,x1511),x1511)+~P5(f16(x1512,x1513,x1511),x1513)+~P5(f16(x1512,x1513,x1511),x1512)+E(x1511,f17(x1512,f17(x1512,x1513))) % 0.71/0.72 [99]~P5(x991,x994)+E(x991,x992)+E(x991,x993)+~E(x994,f20(x993,x992)) % 0.71/0.72 [119]~P5(x1191,x1194)+P5(x1191,x1192)+P5(x1191,x1193)+~E(x1192,f17(x1194,x1193)) % 0.71/0.72 [120]~P5(x1201,x1204)+P5(x1201,x1202)+P5(x1201,x1203)+~E(x1204,f19(x1203,x1202)) % 0.71/0.72 [132]~P5(x1321,x1324)+~P5(x1321,x1323)+P5(x1321,x1322)+~E(x1322,f17(x1323,f17(x1323,x1324))) % 0.71/0.72 %EqnAxiom % 0.71/0.72 [1]E(x11,x11) % 0.71/0.72 [2]E(x22,x21)+~E(x21,x22) % 0.71/0.72 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.71/0.72 [4]~E(x41,x42)+E(f17(x41,x43),f17(x42,x43)) % 0.71/0.72 [5]~E(x51,x52)+E(f17(x53,x51),f17(x53,x52)) % 0.71/0.72 [6]~E(x61,x62)+E(f19(x61,x63),f19(x62,x63)) % 0.71/0.72 [7]~E(x71,x72)+E(f19(x73,x71),f19(x73,x72)) % 0.71/0.72 [8]~E(x81,x82)+E(f16(x81,x83,x84),f16(x82,x83,x84)) % 0.71/0.72 [9]~E(x91,x92)+E(f16(x93,x91,x94),f16(x93,x92,x94)) % 0.71/0.72 [10]~E(x101,x102)+E(f16(x103,x104,x101),f16(x103,x104,x102)) % 0.71/0.72 [11]~E(x111,x112)+E(f20(x111,x113),f20(x112,x113)) % 0.71/0.72 [12]~E(x121,x122)+E(f20(x123,x121),f20(x123,x122)) % 0.71/0.72 [13]~E(x131,x132)+E(f18(x131),f18(x132)) % 0.71/0.72 [14]~E(x141,x142)+E(f6(x141,x143),f6(x142,x143)) % 0.71/0.72 [15]~E(x151,x152)+E(f6(x153,x151),f6(x153,x152)) % 0.71/0.72 [16]~E(x161,x162)+E(f15(x161,x163,x164),f15(x162,x163,x164)) % 0.71/0.72 [17]~E(x171,x172)+E(f15(x173,x171,x174),f15(x173,x172,x174)) % 0.71/0.72 [18]~E(x181,x182)+E(f15(x183,x184,x181),f15(x183,x184,x182)) % 0.71/0.72 [19]~E(x191,x192)+E(f11(x191,x193),f11(x192,x193)) % 0.71/0.72 [20]~E(x201,x202)+E(f11(x203,x201),f11(x203,x202)) % 0.71/0.72 [21]~E(x211,x212)+E(f5(x211,x213),f5(x212,x213)) % 0.71/0.72 [22]~E(x221,x222)+E(f5(x223,x221),f5(x223,x222)) % 0.71/0.72 [23]~E(x231,x232)+E(f12(x231,x233),f12(x232,x233)) % 0.71/0.72 [24]~E(x241,x242)+E(f12(x243,x241),f12(x243,x242)) % 0.71/0.72 [25]~E(x251,x252)+E(f13(x251,x253,x254),f13(x252,x253,x254)) % 0.71/0.72 [26]~E(x261,x262)+E(f13(x263,x261,x264),f13(x263,x262,x264)) % 0.71/0.72 [27]~E(x271,x272)+E(f13(x273,x274,x271),f13(x273,x274,x272)) % 0.71/0.72 [28]~E(x281,x282)+E(f10(x281,x283),f10(x282,x283)) % 0.71/0.72 [29]~E(x291,x292)+E(f10(x293,x291),f10(x293,x292)) % 0.71/0.72 [30]~E(x301,x302)+E(f14(x301,x303,x304),f14(x302,x303,x304)) % 0.71/0.72 [31]~E(x311,x312)+E(f14(x313,x311,x314),f14(x313,x312,x314)) % 0.71/0.72 [32]~E(x321,x322)+E(f14(x323,x324,x321),f14(x323,x324,x322)) % 0.71/0.72 [33]~E(x331,x332)+E(f7(x331,x333),f7(x332,x333)) % 0.71/0.72 [34]~E(x341,x342)+E(f7(x343,x341),f7(x343,x342)) % 0.71/0.72 [35]~E(x351,x352)+E(f9(x351),f9(x352)) % 0.71/0.72 [36]~P1(x361)+P1(x362)+~E(x361,x362) % 0.71/0.72 [37]P5(x372,x373)+~E(x371,x372)+~P5(x371,x373) % 0.71/0.72 [38]P5(x383,x382)+~E(x381,x382)+~P5(x383,x381) % 0.71/0.72 [39]P3(x392,x393)+~E(x391,x392)+~P3(x391,x393) % 0.71/0.72 [40]P3(x403,x402)+~E(x401,x402)+~P3(x403,x401) % 0.71/0.72 [41]P2(x412,x413)+~E(x411,x412)+~P2(x411,x413) % 0.71/0.72 [42]P2(x423,x422)+~E(x421,x422)+~P2(x423,x421) % 0.71/0.72 [43]P4(x432,x433)+~E(x431,x432)+~P4(x431,x433) % 0.71/0.72 [44]P4(x443,x442)+~E(x441,x442)+~P4(x443,x441) % 0.71/0.72 % 0.71/0.72 %------------------------------------------- % 0.71/0.72 cnf(153,plain, % 0.71/0.72 (~P5(x1531,a1)), % 0.71/0.72 inference(equality_inference,[],[75])). % 0.71/0.72 cnf(157,plain, % 0.71/0.72 (~P5(x1571,f18(x1572))+P3(x1571,x1572)), % 0.71/0.72 inference(equality_inference,[],[96])). % 0.71/0.72 cnf(158,plain, % 0.71/0.72 (~P5(x1581,f20(x1582,x1582))+E(x1581,x1582)), % 0.71/0.72 inference(equality_inference,[],[98])). % 0.71/0.72 cnf(159,plain, % 0.71/0.72 (~P5(x1591,f20(x1592,x1593))+E(x1591,x1593)+E(x1591,x1592)), % 0.71/0.72 inference(equality_inference,[],[99])). % 0.71/0.72 cnf(160,plain, % 0.71/0.72 (~P5(x1601,x1602)+P5(x1601,f19(x1603,x1602))), % 0.71/0.72 inference(equality_inference,[],[108])). % 0.71/0.72 cnf(161,plain, % 0.71/0.72 (~P5(x1611,x1612)+P5(x1611,f19(x1612,x1613))), % 0.71/0.72 inference(equality_inference,[],[109])). % 0.71/0.72 cnf(162,plain, % 0.71/0.72 (~P5(x1621,f17(x1622,x1623))+P5(x1621,x1622)), % 0.71/0.72 inference(equality_inference,[],[110])). % 0.71/0.72 cnf(163,plain, % 0.71/0.72 (~P5(x1631,x1632)+~P5(x1631,f17(x1633,x1632))), % 0.71/0.72 inference(equality_inference,[],[117])). % 0.71/0.72 cnf(164,plain, % 0.71/0.72 (~P5(x1641,x1642)+P5(x1641,f17(x1642,x1643))+P5(x1641,x1643)), % 0.71/0.72 inference(equality_inference,[],[119])). % 0.71/0.72 cnf(165,plain, % 0.71/0.72 (~P5(x1651,f19(x1652,x1653))+P5(x1651,x1653)+P5(x1651,x1652)), % 0.71/0.72 inference(equality_inference,[],[120])). % 0.71/0.72 cnf(166,plain, % 0.71/0.72 (~P5(x1661,f17(x1662,f17(x1662,x1663)))+P5(x1661,x1663)), % 0.71/0.72 inference(equality_inference,[],[129])). % 0.71/0.72 cnf(170,plain, % 0.71/0.72 (~P5(a8,f20(a3,a3))), % 0.71/0.72 inference(scs_inference,[],[62,65,122,158])). % 0.71/0.72 cnf(172,plain, % 0.71/0.72 (E(x1721,f19(x1721,x1721))), % 0.71/0.72 inference(scs_inference,[],[62,65,53,122,158,2])). % 0.71/0.72 cnf(174,plain, % 0.71/0.72 (E(f19(x1741,x1741),x1741)), % 0.71/0.72 inference(rename_variables,[],[53])). % 0.71/0.72 cnf(189,plain, % 0.71/0.72 (~P3(f20(x1891,x1891),a1)), % 0.71/0.72 inference(scs_inference,[],[62,65,53,174,50,67,47,56,122,158,2,75,76,81,86,102,121,69,73])). % 0.71/0.72 cnf(210,plain, % 0.71/0.72 (E(f19(x2101,a1),x2101)), % 0.71/0.72 inference(rename_variables,[],[49])). % 0.71/0.72 cnf(215,plain, % 0.71/0.72 (E(a3,a8)), % 0.71/0.72 inference(scs_inference,[],[62,65,153,58,53,174,49,50,46,67,47,56,122,158,2,75,76,81,86,102,121,69,73,74,77,92,103,160,161,162,163,166,95,97,98])). % 0.71/0.72 cnf(216,plain, % 0.71/0.72 (E(f19(x2161,x2161),x2161)), % 0.71/0.72 inference(rename_variables,[],[53])). % 0.71/0.72 cnf(218,plain, % 0.71/0.72 (P5(f9(f20(a3,a3)),f20(a8,a8))), % 0.71/0.72 inference(scs_inference,[],[62,65,153,58,53,174,49,50,46,67,47,56,122,158,2,75,76,81,86,102,121,69,73,74,77,92,103,160,161,162,163,166,95,97,98,105])). % 0.71/0.72 cnf(221,plain, % 0.71/0.72 (P3(x2211,f19(x2211,x2212))), % 0.71/0.72 inference(rename_variables,[],[57])). % 0.71/0.72 cnf(224,plain, % 0.71/0.72 (~E(f20(x2241,x2241),a1)), % 0.71/0.72 inference(rename_variables,[],[67])). % 0.71/0.72 cnf(227,plain, % 0.71/0.72 (~P5(x2271,a1)), % 0.71/0.72 inference(rename_variables,[],[153])). % 0.71/0.72 cnf(232,plain, % 0.71/0.72 (E(f19(x2321,x2321),x2321)), % 0.71/0.72 inference(rename_variables,[],[53])). % 0.71/0.72 cnf(233,plain, % 0.71/0.72 (~E(a1,f20(a3,a3))), % 0.71/0.72 inference(scs_inference,[],[62,65,48,153,57,58,53,174,216,49,50,46,67,224,47,56,122,158,2,75,76,81,86,102,121,69,73,74,77,92,103,160,161,162,163,166,95,97,98,105,106,124,125,159,3,39])). % 0.71/0.72 cnf(235,plain, % 0.71/0.72 (~E(f19(f20(a3,a3),x2351),a1)), % 0.71/0.72 inference(scs_inference,[],[62,65,48,153,57,221,58,53,174,216,49,50,46,67,224,47,56,122,158,2,75,76,81,86,102,121,69,73,74,77,92,103,160,161,162,163,166,95,97,98,105,106,124,125,159,3,39,40])). % 0.71/0.72 cnf(238,plain, % 0.71/0.72 (E(f19(x2381,a1),x2381)), % 0.71/0.72 inference(rename_variables,[],[49])). % 0.71/0.72 cnf(241,plain, % 0.71/0.72 (E(f19(x2411,a1),x2411)), % 0.71/0.72 inference(rename_variables,[],[49])). % 0.71/0.72 cnf(244,plain, % 0.71/0.72 (E(f19(x2441,x2441),x2441)), % 0.71/0.72 inference(rename_variables,[],[53])). % 0.71/0.72 cnf(247,plain, % 0.71/0.72 (E(f19(x2471,x2471),x2471)), % 0.71/0.72 inference(rename_variables,[],[53])). % 0.71/0.72 cnf(249,plain, % 0.71/0.72 (E(f19(x2491,a1),x2491)), % 0.71/0.72 inference(rename_variables,[],[49])). % 0.71/0.72 cnf(252,plain, % 0.71/0.72 (E(f19(x2521,a1),x2521)), % 0.71/0.72 inference(rename_variables,[],[49])). % 0.71/0.72 cnf(255,plain, % 0.71/0.72 (E(f19(x2551,x2551),x2551)), % 0.71/0.72 inference(rename_variables,[],[53])). % 0.71/0.72 cnf(258,plain, % 0.71/0.72 (E(f19(x2581,a1),x2581)), % 0.71/0.72 inference(rename_variables,[],[49])). % 0.71/0.72 cnf(261,plain, % 0.71/0.72 (~P5(x2611,a1)), % 0.71/0.72 inference(rename_variables,[],[153])). % 0.71/0.72 cnf(267,plain, % 0.71/0.72 (~P5(x2671,a1)), % 0.71/0.72 inference(rename_variables,[],[153])). % 0.71/0.72 cnf(273,plain, % 0.71/0.72 (~P5(x2731,a1)), % 0.71/0.72 inference(rename_variables,[],[153])). % 0.71/0.72 cnf(281,plain, % 0.71/0.72 (~P5(x2811,a1)), % 0.71/0.72 inference(rename_variables,[],[153])). % 0.71/0.72 cnf(283,plain, % 0.71/0.73 (~P5(x2831,f19(f19(a1,a1),f19(a1,a1)))), % 0.71/0.73 inference(scs_inference,[],[62,65,48,153,227,261,267,273,281,57,221,58,53,174,216,232,244,247,255,49,210,238,241,249,252,258,50,46,66,67,224,59,47,56,122,158,2,75,76,81,86,102,121,69,73,74,77,92,103,160,161,162,163,166,95,97,98,105,106,124,125,159,3,39,40,88,89,96,36,108,109,110,117,118,129,164,165,37,38,41,42,99,119,120])). % 0.71/0.73 cnf(308,plain, % 0.71/0.73 (~P5(x3081,f19(f19(a1,a1),f19(a1,a1)))), % 0.71/0.73 inference(rename_variables,[],[283])). % 0.71/0.73 cnf(320,plain, % 0.71/0.73 (~P5(x3201,f19(f19(a1,a1),f19(a1,a1)))), % 0.71/0.73 inference(rename_variables,[],[283])). % 0.71/0.73 cnf(345,plain, % 0.71/0.73 ($false), % 0.71/0.73 inference(scs_inference,[],[65,172,215,170,233,218,235,52,283,308,320,189,59,104,86,161,122,82,103,157,166,163,102,73,160,69,162,92,158,76,2]), % 0.71/0.73 ['proof']). % 0.71/0.73 % SZS output end Proof % 0.71/0.73 % Total time :0.080000s %------------------------------------------------------------------------------