%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : CAT033+1 : TPTP v8.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n002.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 04:40:25 EDT 2024 % Result : Theorem 23.90s 23.99s % Output : CNFRefutation 23.90s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : CAT033+1 : TPTP v8.2.0. Released v3.4.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n002.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 : Tue Jun 18 12:47:23 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 23.90/23.97 %------------------------------------------- % 23.90/23.97 % File :CSE---1.7 % 23.90/23.97 % Problem :theBenchmark % 23.90/23.97 % Transform :cnf % 23.90/23.97 % Format :tptp:raw % 23.90/23.97 % Command :java -jar mcs_scs.jar %d %s % 23.90/23.97 % 23.90/23.97 % Result :Theorem 23.350000s % 23.90/23.97 % Output :CNFRefutation 23.350000s % 23.90/23.97 %------------------------------------------- % 23.90/23.97 %------------------------------------------------------------------------------ % 23.90/23.97 % File : CAT033+1 : TPTP v8.2.0. Released v3.4.0. % 23.90/23.97 % Domain : Category Theory % 23.90/23.97 % Problem : Yoneda Embedding T02 % 23.90/23.97 % Version : [Urb08] axioms : Especial. % 23.90/23.97 % English : % 23.90/23.97 % 23.90/23.97 % Refs : [Woj97] Wojciechowski (1997), Yoneda Embedding % 23.90/23.97 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 23.90/23.97 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 23.90/23.97 % Source : [Urb08] % 23.90/23.97 % Names : t2_yoneda_1 [Urb08] % 23.90/23.97 % 23.90/23.97 % Status : Theorem % 23.90/23.97 % Rating : 0.25 v7.5.0, 0.31 v7.4.0, 0.17 v7.3.0, 0.21 v7.2.0, 0.17 v7.1.0, 0.22 v7.0.0, 0.23 v6.4.0, 0.31 v6.3.0, 0.29 v6.2.0, 0.36 v6.1.0, 0.40 v6.0.0, 0.35 v5.5.0, 0.33 v5.4.0, 0.36 v5.3.0, 0.41 v5.2.0, 0.25 v5.1.0, 0.24 v5.0.0, 0.38 v4.1.0, 0.43 v4.0.1, 0.39 v4.0.0, 0.42 v3.7.0, 0.30 v3.5.0, 0.32 v3.4.0 % 23.90/23.97 % Syntax : Number of formulae : 53 ( 16 unt; 0 def) % 23.90/23.97 % Number of atoms : 163 ( 11 equ) % 23.90/23.97 % Maximal formula atoms : 20 ( 3 avg) % 23.90/23.98 % Number of connectives : 128 ( 18 ~; 1 |; 71 &) % 23.90/23.98 % ( 2 <=>; 36 =>; 0 <=; 0 <~>) % 23.90/23.98 % Maximal formula depth : 20 ( 5 avg) % 23.90/23.98 % Maximal term depth : 3 ( 1 avg) % 23.90/23.98 % Number of predicates : 16 ( 14 usr; 1 prp; 0-3 aty) % 23.90/23.98 % Number of functors : 15 ( 15 usr; 1 con; 0-6 aty) % 23.90/23.98 % Number of variables : 90 ( 80 !; 10 ?) % 23.90/23.98 % SPC : FOF_THM_RFO_SEQ % 23.90/23.98 % 23.90/23.98 % Comments : Normal version: includes the axioms (which may be theorems from % 23.90/23.98 % other articles) and background that are possibly necessary. % 23.90/23.98 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 23.90/23.98 % : The problem encoding is based on set theory. % 23.90/23.98 %------------------------------------------------------------------------------ % 23.90/23.98 fof(t2_yoneda_1,conjecture, % 23.90/23.98 ! [A] : % 23.90/23.98 ( ( v2_cat_1(A) % 23.90/23.98 & l1_cat_1(A) ) % 23.90/23.98 => ! [B] : % 23.90/23.98 ( m1_subset_1(B,u1_cat_1(A)) % 23.90/23.98 => m2_cat_1(k20_ens_1(A,B),A,k1_yoneda_1(A)) ) ) ). % 23.90/23.98 % 23.90/23.98 fof(rc3_funct_1,axiom, % 23.90/23.98 ? [A] : % 23.90/23.98 ( v1_relat_1(A) % 23.90/23.98 & v1_funct_1(A) % 23.90/23.98 & v2_funct_1(A) ) ). % 23.90/23.98 % 23.90/23.98 fof(cc2_funct_1,axiom, % 23.90/23.98 ! [A] : % 23.90/23.98 ( ( v1_relat_1(A) % 23.90/23.98 & v1_xboole_0(A) % 23.90/23.98 & v1_funct_1(A) ) % 23.90/23.98 => ( v1_relat_1(A) % 23.90/23.98 & v1_funct_1(A) % 23.90/23.98 & v2_funct_1(A) ) ) ). % 23.90/23.98 % 23.90/23.98 fof(rc1_funct_1,axiom, % 23.90/23.98 ? [A] : % 23.90/23.98 ( v1_relat_1(A) % 23.90/23.98 & v1_funct_1(A) ) ). % 23.90/23.98 % 23.90/23.98 fof(rc2_funct_1,axiom, % 23.90/23.98 ? [A] : % 23.90/23.98 ( v1_relat_1(A) % 23.90/23.98 & v1_xboole_0(A) % 23.90/23.98 & v1_funct_1(A) ) ). % 23.90/23.98 % 23.90/23.98 fof(free_g1_cat_1,axiom, % 23.90/23.98 ! [A,B,C,D,E,F] : % 23.90/23.98 ( ( ~ v1_xboole_0(A) % 23.90/23.98 & ~ v1_xboole_0(B) % 23.90/23.98 & v1_funct_1(C) % 23.90/23.98 & v1_funct_2(C,B,A) % 23.90/23.98 & m1_relset_1(C,B,A) % 23.90/23.98 & v1_funct_1(D) % 23.90/23.98 & v1_funct_2(D,B,A) % 23.90/23.98 & m1_relset_1(D,B,A) % 23.90/23.98 & v1_funct_1(E) % 23.90/23.98 & m1_relset_1(E,k2_zfmisc_1(B,B),B) % 23.90/23.98 & v1_funct_1(F) % 23.90/23.98 & v1_funct_2(F,A,B) % 23.90/23.98 & m1_relset_1(F,A,B) ) % 23.90/23.98 => ! [G,H,I,J,K,L] : % 23.90/23.98 ( g1_cat_1(A,B,C,D,E,F) = g1_cat_1(G,H,I,J,K,L) % 23.90/23.98 => ( A = G % 23.90/23.98 & B = H % 23.90/23.98 & C = I % 23.90/23.98 & D = J % 23.90/23.98 & E = K % 23.90/23.98 & F = L ) ) ) ). % 23.90/23.98 % 23.90/23.98 fof(existence_m1_relset_1,axiom, % 23.90/23.98 ! [A,B] : % 23.90/23.98 ? [C] : m1_relset_1(C,A,B) ). % 23.90/23.98 % 23.90/23.98 fof(dt_g1_cat_1,axiom, % 23.90/23.98 ! [A,B,C,D,E,F] : % 23.90/23.98 ( ( ~ v1_xboole_0(A) % 23.90/23.98 & ~ v1_xboole_0(B) % 23.90/23.98 & v1_funct_1(C) % 23.90/23.98 & v1_funct_2(C,B,A) % 23.90/23.98 & m1_relset_1(C,B,A) % 23.90/23.98 & v1_funct_1(D) % 23.90/23.98 & v1_funct_2(D,B,A) % 23.90/23.98 & m1_relset_1(D,B,A) % 23.90/23.98 & v1_funct_1(E) % 23.90/23.98 & m1_relset_1(E,k2_zfmisc_1(B,B),B) % 23.90/23.98 & v1_funct_1(F) % 23.90/23.98 & v1_funct_2(F,A,B) % 23.90/23.98 & m1_relset_1(F,A,B) ) % 23.90/23.98 => ( v1_cat_1(g1_cat_1(A,B,C,D,E,F)) % 23.90/23.98 & l1_cat_1(g1_cat_1(A,B,C,D,E,F)) ) ) ). % 23.90/23.98 % 23.90/23.98 fof(dt_k2_zfmisc_1,axiom, % 23.90/23.98 $true ). % 23.90/23.98 % 23.90/23.98 fof(dt_m1_relset_1,axiom, % 23.90/23.98 $true ). % 23.90/23.98 % 23.90/23.98 fof(dt_u3_cat_1,axiom, % 23.90/23.98 ! [A] : % 23.90/23.98 ( l1_cat_1(A) % 23.90/23.98 => ( v1_funct_1(u3_cat_1(A)) % 23.90/23.98 & v1_funct_2(u3_cat_1(A),u2_cat_1(A),u1_cat_1(A)) % 23.90/23.98 & m2_relset_1(u3_cat_1(A),u2_cat_1(A),u1_cat_1(A)) ) ) ). % 23.90/23.98 % 23.90/23.98 fof(dt_u4_cat_1,axiom, % 23.90/23.98 ! [A] : % 23.90/23.98 ( l1_cat_1(A) % 23.90/23.98 => ( v1_funct_1(u4_cat_1(A)) % 23.90/23.98 & v1_funct_2(u4_cat_1(A),u2_cat_1(A),u1_cat_1(A)) % 23.90/23.98 & m2_relset_1(u4_cat_1(A),u2_cat_1(A),u1_cat_1(A)) ) ) ). % 23.90/23.98 % 23.90/23.98 fof(dt_u5_cat_1,axiom, % 23.90/23.98 ! [A] : % 23.90/23.98 ( l1_cat_1(A) % 23.90/23.98 => ( v1_funct_1(u5_cat_1(A)) % 23.90/23.98 & m2_relset_1(u5_cat_1(A),k2_zfmisc_1(u2_cat_1(A),u2_cat_1(A)),u2_cat_1(A)) ) ) ). % 23.90/23.98 % 23.90/23.98 fof(dt_u6_cat_1,axiom, % 23.90/23.98 ! [A] : % 23.90/23.98 ( l1_cat_1(A) % 23.90/23.98 => ( v1_funct_1(u6_cat_1(A)) % 23.90/23.98 & v1_funct_2(u6_cat_1(A),u1_cat_1(A),u2_cat_1(A)) % 23.90/23.98 & m2_relset_1(u6_cat_1(A),u1_cat_1(A),u2_cat_1(A)) ) ) ). % 23.90/23.98 % 23.90/23.98 fof(cc1_relset_1,axiom, % 23.90/23.98 ! [A,B,C] : % 23.90/23.98 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) % 23.90/23.98 => v1_relat_1(C) ) ). % 23.90/23.98 % 23.90/23.98 fof(antisymmetry_r2_hidden,axiom, % 23.90/23.98 ! [A,B] : % 23.90/23.98 ( r2_hidden(A,B) % 23.90/23.98 => ~ r2_hidden(B,A) ) ). % 23.90/23.98 % 23.90/23.98 fof(abstractness_v1_cat_1,axiom, % 23.90/23.98 ! [A] : % 23.90/23.98 ( l1_cat_1(A) % 23.90/23.98 => ( v1_cat_1(A) % 23.90/23.98 => A = g1_cat_1(u1_cat_1(A),u2_cat_1(A),u3_cat_1(A),u4_cat_1(A),u5_cat_1(A),u6_cat_1(A)) ) ) ). % 23.90/23.98 % 23.90/23.98 fof(existence_m2_relset_1,axiom, % 23.90/23.98 ! [A,B] : % 23.90/23.98 ? [C] : m2_relset_1(C,A,B) ). % 23.90/23.98 % 23.90/23.98 fof(redefinition_m2_relset_1,axiom, % 23.90/23.98 ! [A,B,C] : % 23.90/23.98 ( m2_relset_1(C,A,B) % 23.90/23.98 <=> m1_relset_1(C,A,B) ) ). % 23.90/23.98 % 23.90/23.98 fof(dt_k1_xboole_0,axiom, % 23.90/23.98 $true ). % 23.90/23.98 % 23.90/23.98 fof(dt_k1_zfmisc_1,axiom, % 23.90/23.98 $true ). % 23.90/23.98 % 23.90/23.98 fof(dt_k2_ens_1,axiom, % 23.90/23.98 $true ). % 23.90/23.98 % 23.90/23.98 fof(dt_m2_relset_1,axiom, % 23.90/23.98 ! [A,B,C] : % 23.90/23.98 ( m2_relset_1(C,A,B) % 23.90/23.98 => m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) ). % 23.90/23.98 % 23.90/23.98 fof(dt_u2_cat_1,axiom, % 23.90/23.98 ! [A] : % 23.90/23.98 ( l1_cat_1(A) % 23.90/23.98 => ~ v1_xboole_0(u2_cat_1(A)) ) ). % 23.90/23.98 % 23.90/23.98 fof(fc1_xboole_0,axiom, % 23.90/23.98 v1_xboole_0(k1_xboole_0) ). % 23.90/23.98 % 23.90/23.98 fof(fc2_ens_1,axiom, % 23.90/23.98 ! [A] : % 23.90/23.98 ( ~ v1_xboole_0(A) % 23.90/23.98 => ~ v1_xboole_0(k2_ens_1(A)) ) ). % 23.90/23.98 % 23.90/23.98 fof(t1_subset,axiom, % 23.90/23.98 ! [A,B] : % 23.90/23.98 ( r2_hidden(A,B) % 23.90/23.98 => m1_subset_1(A,B) ) ). % 23.90/23.98 % 23.90/23.98 fof(t4_subset,axiom, % 23.90/23.98 ! [A,B,C] : % 23.90/23.98 ( ( r2_hidden(A,B) % 23.90/23.98 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 23.90/23.98 => m1_subset_1(A,C) ) ). % 23.90/23.98 % 23.90/23.98 fof(t5_subset,axiom, % 23.90/23.98 ! [A,B,C] : % 23.90/23.98 ~ ( r2_hidden(A,B) % 23.90/23.98 & m1_subset_1(B,k1_zfmisc_1(C)) % 23.90/23.98 & v1_xboole_0(C) ) ). % 23.90/23.98 % 23.90/23.98 fof(t8_boole,axiom, % 23.90/23.98 ! [A,B] : % 23.90/23.98 ~ ( v1_xboole_0(A) % 23.90/23.98 & A != B % 23.90/23.98 & v1_xboole_0(B) ) ). % 23.90/23.98 % 23.90/23.98 fof(reflexivity_r1_tarski,axiom, % 23.90/23.98 ! [A,B] : r1_tarski(A,A) ). % 23.90/23.98 % 23.90/23.98 fof(existence_l1_cat_1,axiom, % 23.90/23.98 ? [A] : l1_cat_1(A) ). % 23.90/23.98 % 23.90/23.98 fof(existence_m1_subset_1,axiom, % 23.90/23.98 ! [A] : % 23.90/23.98 ? [B] : m1_subset_1(B,A) ). % 23.90/23.98 % 23.90/23.98 fof(existence_m2_cat_1,axiom, % 23.90/23.98 ! [A,B] : % 23.90/23.98 ( ( v2_cat_1(A) % 23.90/23.98 & l1_cat_1(A) % 23.90/23.98 & v2_cat_1(B) % 23.90/23.98 & l1_cat_1(B) ) % 23.90/23.98 => ? [C] : m2_cat_1(C,A,B) ) ). % 23.90/23.98 % 23.90/23.98 fof(dt_k12_ens_1,axiom, % 23.90/23.98 ! [A] : % 23.90/23.98 ( ~ v1_xboole_0(A) % 23.90/23.98 => l1_cat_1(k12_ens_1(A)) ) ). % 23.90/23.98 % 23.90/23.98 fof(dt_k17_ens_1,axiom, % 23.90/23.98 $true ). % 23.90/23.98 % 23.90/23.98 fof(dt_k1_yoneda_1,axiom, % 23.90/23.98 ! [A] : % 23.90/23.98 ( ( v2_cat_1(A) % 23.90/23.99 & l1_cat_1(A) ) % 23.90/23.99 => ( v2_cat_1(k1_yoneda_1(A)) % 23.90/23.99 & l1_cat_1(k1_yoneda_1(A)) ) ) ). % 23.90/23.99 % 23.90/23.99 fof(dt_k20_ens_1,axiom, % 23.90/23.99 ! [A,B] : % 23.90/23.99 ( ( v2_cat_1(A) % 23.90/23.99 & l1_cat_1(A) % 23.90/23.99 & m1_subset_1(B,u1_cat_1(A)) ) % 23.90/23.99 => ( v1_funct_1(k20_ens_1(A,B)) % 23.90/23.99 & v1_funct_2(k20_ens_1(A,B),u2_cat_1(A),k2_ens_1(k17_ens_1(A))) % 23.90/23.99 & m2_relset_1(k20_ens_1(A,B),u2_cat_1(A),k2_ens_1(k17_ens_1(A))) ) ) ). % 23.90/23.99 % 23.90/23.99 fof(dt_l1_cat_1,axiom, % 23.90/23.99 $true ). % 23.90/23.99 % 23.90/23.99 fof(dt_m1_subset_1,axiom, % 23.90/23.99 $true ). % 23.90/23.99 % 23.90/23.99 fof(dt_m2_cat_1,axiom, % 23.90/23.99 ! [A,B] : % 23.90/23.99 ( ( v2_cat_1(A) % 23.90/23.99 & l1_cat_1(A) % 23.90/23.99 & v2_cat_1(B) % 23.90/23.99 & l1_cat_1(B) ) % 23.90/23.99 => ! [C] : % 23.90/23.99 ( m2_cat_1(C,A,B) % 23.90/23.99 => ( v1_funct_1(C) % 23.90/23.99 & v1_funct_2(C,u2_cat_1(A),u2_cat_1(B)) % 23.90/23.99 & m2_relset_1(C,u2_cat_1(A),u2_cat_1(B)) ) ) ) ). % 23.90/23.99 % 23.90/23.99 fof(dt_u1_cat_1,axiom, % 23.90/23.99 ! [A] : % 23.90/23.99 ( l1_cat_1(A) % 23.90/23.99 => ~ v1_xboole_0(u1_cat_1(A)) ) ). % 23.90/23.99 % 23.90/23.99 fof(cc1_funct_1,axiom, % 23.90/23.99 ! [A] : % 23.90/23.99 ( v1_xboole_0(A) % 23.90/23.99 => v1_funct_1(A) ) ). % 23.90/23.99 % 23.90/23.99 fof(fc4_ens_1,axiom, % 23.90/23.99 ! [A] : % 23.90/23.99 ( ~ v1_xboole_0(A) % 23.90/23.99 => ( v1_cat_1(k12_ens_1(A)) % 23.90/23.99 & v2_cat_1(k12_ens_1(A)) ) ) ). % 23.90/23.99 % 23.90/23.99 fof(fc5_ens_1,axiom, % 23.90/23.99 ! [A] : % 23.90/23.99 ( ( v2_cat_1(A) % 23.90/23.99 & l1_cat_1(A) ) % 23.90/23.99 => ~ v1_xboole_0(k17_ens_1(A)) ) ). % 23.90/23.99 % 23.90/23.99 fof(rc1_xboole_0,axiom, % 23.90/23.99 ? [A] : v1_xboole_0(A) ). % 23.90/23.99 % 23.90/23.99 fof(rc2_xboole_0,axiom, % 23.90/23.99 ? [A] : ~ v1_xboole_0(A) ). % 23.90/23.99 % 23.90/23.99 fof(t2_subset,axiom, % 23.90/23.99 ! [A,B] : % 23.90/23.99 ( m1_subset_1(A,B) % 23.90/23.99 => ( v1_xboole_0(B) % 23.90/23.99 | r2_hidden(A,B) ) ) ). % 23.90/23.99 % 23.90/23.99 fof(t3_subset,axiom, % 23.90/23.99 ! [A,B] : % 23.90/23.99 ( m1_subset_1(A,k1_zfmisc_1(B)) % 23.90/23.99 <=> r1_tarski(A,B) ) ). % 23.90/23.99 % 23.90/23.99 fof(t6_boole,axiom, % 23.90/23.99 ! [A] : % 23.90/23.99 ( v1_xboole_0(A) % 23.90/23.99 => A = k1_xboole_0 ) ). % 23.90/23.99 % 23.90/23.99 fof(t7_boole,axiom, % 23.90/23.99 ! [A,B] : % 23.90/23.99 ~ ( r2_hidden(A,B) % 23.90/23.99 & v1_xboole_0(B) ) ). % 23.90/23.99 % 23.90/23.99 fof(d1_yoneda_1,axiom, % 23.90/23.99 ! [A] : % 23.90/23.99 ( ( v2_cat_1(A) % 23.90/23.99 & l1_cat_1(A) ) % 23.90/23.99 => k1_yoneda_1(A) = k12_ens_1(k17_ens_1(A)) ) ). % 23.90/23.99 % 23.90/23.99 fof(t49_ens_1,axiom, % 23.90/23.99 ! [A] : % 23.90/23.99 ( ~ v1_xboole_0(A) % 23.90/23.99 => ! [B] : % 23.90/23.99 ( ( v2_cat_1(B) % 23.90/23.99 & l1_cat_1(B) ) % 23.90/23.99 => ! [C] : % 23.90/23.99 ( m1_subset_1(C,u1_cat_1(B)) % 23.90/23.99 => ( r1_tarski(k17_ens_1(B),A) % 23.90/23.99 => m2_cat_1(k20_ens_1(B,C),B,k12_ens_1(A)) ) ) ) ) ). % 23.90/23.99 % 23.90/23.99 %------------------------------------------------------------------------------ % 23.90/23.99 %------------------------------------------- % 23.90/23.99 % Proof found % 23.90/23.99 % SZS status Theorem for theBenchmark % 23.90/23.99 % SZS output start Proof % 23.90/23.99 %ClaNum:130(EqnAxiom:56) % 23.90/23.99 %VarNum:541(SingletonVarNum:167) % 23.90/23.99 %MaxLitNum:15 % 23.90/23.99 %MaxfuncDepth:2 % 23.90/23.99 %SharedTerms:28 % 23.90/23.99 %goalClause: 57 58 71 76 % 23.90/23.99 %singleGoalClaCount:4 % 23.90/23.99 [57]P1(a1) % 23.90/23.99 [58]P2(a1) % 23.90/23.99 [59]P2(a5) % 23.90/23.99 [60]P3(a6) % 23.90/23.99 [61]P3(a8) % 23.90/23.99 [62]P3(a9) % 23.90/23.99 [63]P4(a6) % 23.90/23.99 [64]P4(a8) % 23.90/23.99 [65]P4(a9) % 23.90/23.99 [66]P14(a6) % 23.90/23.99 [67]P13(a12) % 23.90/23.99 [68]P13(a9) % 23.90/23.99 [69]P13(a2) % 23.90/23.99 [75]~P13(a4) % 23.90/23.99 [71]P6(a7,f17(a1)) % 23.90/23.99 [76]~P9(f18(a1,a7),a1,f19(a1)) % 23.90/23.99 [70]P5(x701,x701) % 23.90/23.99 [72]P6(f13(x721),x721) % 23.90/23.99 [73]P7(f10(x731,x732),x731,x732) % 23.90/23.99 [74]P8(f11(x741,x742),x741,x742) % 23.90/23.99 [77]~P13(x771)+E(x771,a12) % 23.90/23.99 [78]~P13(x781)+P4(x781) % 23.90/23.99 [79]P13(x791)+P1(f14(x791)) % 23.90/23.99 [80]P13(x801)+P2(f14(x801)) % 23.90/23.99 [81]P13(x811)+P10(f14(x811)) % 23.90/23.99 [83]~P2(x831)+P4(f23(x831)) % 23.90/23.99 [84]~P2(x841)+P4(f25(x841)) % 23.90/23.99 [85]~P2(x851)+P4(f26(x851)) % 23.90/23.99 [86]~P2(x861)+P4(f27(x861)) % 23.90/23.99 [87]P13(x871)+~P13(f21(x871)) % 23.90/23.99 [88]~P2(x881)+~P13(f17(x881)) % 23.90/23.99 [89]~P2(x891)+~P13(f24(x891)) % 23.90/23.99 [104]~P2(x1041)+P12(f23(x1041),f24(x1041),f17(x1041)) % 23.90/23.99 [105]~P2(x1051)+P12(f25(x1051),f24(x1051),f17(x1051)) % 23.90/23.99 [106]~P2(x1061)+P12(f27(x1061),f17(x1061),f24(x1061)) % 23.90/23.99 [107]~P2(x1071)+P8(f23(x1071),f24(x1071),f17(x1071)) % 23.90/23.99 [108]~P2(x1081)+P8(f25(x1081),f24(x1081),f17(x1081)) % 23.90/23.99 [109]~P2(x1091)+P8(f27(x1091),f17(x1091),f24(x1091)) % 23.90/23.99 [113]~P2(x1131)+P8(f26(x1131),f22(f24(x1131),f24(x1131)),f24(x1131)) % 23.90/23.99 [94]~P13(x941)+~P11(x942,x941) % 23.90/23.99 [96]~P11(x961,x962)+P6(x961,x962) % 23.90/23.99 [99]~P11(x992,x991)+~P11(x991,x992) % 23.90/23.99 [98]~P5(x981,x982)+P6(x981,f20(x982)) % 23.90/23.99 [100]P5(x1001,x1002)+~P6(x1001,f20(x1002)) % 23.90/23.99 [114]~P8(x1141,x1142,x1143)+P7(x1141,x1142,x1143) % 23.90/23.99 [115]~P7(x1151,x1152,x1153)+P8(x1151,x1152,x1153) % 23.90/23.99 [111]P3(x1111)+~P6(x1111,f20(f22(x1112,x1113))) % 23.90/23.99 [118]~P8(x1181,x1182,x1183)+P6(x1181,f20(f22(x1182,x1183))) % 23.90/23.99 [90]~P1(x901)+~P2(x901)+P1(f19(x901)) % 23.90/23.99 [91]~P1(x911)+~P2(x911)+P2(f19(x911)) % 23.90/23.99 [95]~P2(x951)+~P1(x951)+~P13(f16(x951)) % 23.90/23.99 [93]~P1(x931)+~P2(x931)+E(f19(x931),f14(f16(x931))) % 23.90/23.99 [122]~P2(x1221)+~P10(x1221)+E(f15(f17(x1221),f24(x1221),f23(x1221),f25(x1221),f26(x1221),f27(x1221)),x1221) % 23.90/23.99 [82]~P13(x822)+~P13(x821)+E(x821,x822) % 23.90/23.99 [97]~P6(x972,x971)+P13(x971)+P11(x972,x971) % 23.90/23.99 [101]~P13(x1011)+~P11(x1012,x1013)+~P6(x1013,f20(x1011)) % 23.90/23.99 [102]P6(x1021,x1022)+~P11(x1021,x1023)+~P6(x1023,f20(x1022)) % 23.90/23.99 [92]~P3(x921)+~P4(x921)+~P13(x921)+P14(x921) % 23.90/23.99 [103]~P1(x1031)+~P2(x1031)+~P6(x1032,f17(x1031))+P4(f18(x1031,x1032)) % 23.90/23.99 [116]~P1(x1161)+~P2(x1161)+~P6(x1162,f17(x1161))+P12(f18(x1161,x1162),f24(x1161),f21(f16(x1161))) % 23.90/23.99 [117]~P1(x1171)+~P2(x1171)+~P6(x1172,f17(x1171))+P8(f18(x1171,x1172),f24(x1171),f21(f16(x1171))) % 23.90/23.99 [110]~P1(x1102)+~P1(x1101)+~P2(x1102)+~P2(x1101)+P9(f3(x1101,x1102),x1101,x1102) % 23.90/23.99 [112]~P2(x1122)+~P2(x1123)+~P9(x1121,x1123,x1122)+P4(x1121)+~P1(x1122)+~P1(x1123) % 23.90/23.99 [119]~P1(x1192)+~P2(x1192)+P13(x1191)+P9(f18(x1192,x1193),x1192,f14(x1191))+~P6(x1193,f17(x1192))+~P5(f16(x1192),x1191) % 23.90/23.99 [120]~P1(x1203)+~P1(x1202)+~P2(x1203)+~P2(x1202)+~P9(x1201,x1202,x1203)+P12(x1201,f24(x1202),f24(x1203)) % 23.90/23.99 [121]~P1(x1213)+~P1(x1212)+~P2(x1213)+~P2(x1212)+~P9(x1211,x1212,x1213)+P8(x1211,f24(x1212),f24(x1213)) % 23.90/23.99 [123]~P4(x1236)+~P4(x1235)+~P4(x1234)+~P4(x1233)+~P12(x1236,x1232,x1231)+~P12(x1234,x1231,x1232)+~P12(x1233,x1231,x1232)+~P7(x1236,x1232,x1231)+~P7(x1234,x1231,x1232)+~P7(x1233,x1231,x1232)+P13(x1231)+P13(x1232)+~P7(x1235,f22(x1231,x1231),x1231)+P2(f15(x1232,x1231,x1233,x1234,x1235,x1236)) % 23.90/23.99 [124]~P4(x1246)+~P4(x1245)+~P4(x1244)+~P4(x1243)+~P12(x1246,x1242,x1241)+~P12(x1244,x1241,x1242)+~P12(x1243,x1241,x1242)+~P7(x1246,x1242,x1241)+~P7(x1244,x1241,x1242)+~P7(x1243,x1241,x1242)+P13(x1241)+P13(x1242)+~P7(x1245,f22(x1241,x1241),x1241)+P10(f15(x1242,x1241,x1243,x1244,x1245,x1246)) % 23.90/23.99 [125]~P4(x1257)+~P4(x1256)+~P4(x1255)+~P4(x1251)+~P12(x1256,x1253,x1254)+~P12(x1255,x1253,x1254)+~P12(x1251,x1254,x1253)+~P7(x1256,x1253,x1254)+~P7(x1255,x1253,x1254)+~P7(x1251,x1254,x1253)+E(x1251,x1252)+P13(x1253)+P13(x1254)+~P7(x1257,f22(x1253,x1253),x1253)+~E(f15(x1254,x1253,x1255,x1256,x1257,x1251),f15(x1258,x1259,x12510,x12511,x12512,x1252)) % 23.90/23.99 [126]~P4(x1267)+~P4(x1266)+~P4(x1265)+~P4(x1261)+~P12(x1267,x1264,x1263)+~P12(x1266,x1263,x1264)+~P12(x1265,x1263,x1264)+~P7(x1267,x1264,x1263)+~P7(x1266,x1263,x1264)+~P7(x1265,x1263,x1264)+E(x1261,x1262)+P13(x1263)+P13(x1264)+~P7(x1261,f22(x1263,x1263),x1263)+~E(f15(x1264,x1263,x1265,x1266,x1261,x1267),f15(x1268,x1269,x12610,x12611,x1262,x12612)) % 23.90/23.99 [127]~P4(x1277)+~P4(x1276)+~P4(x1275)+~P4(x1271)+~P12(x1277,x1274,x1273)+~P12(x1275,x1273,x1274)+~P12(x1271,x1273,x1274)+~P7(x1277,x1274,x1273)+~P7(x1275,x1273,x1274)+~P7(x1271,x1273,x1274)+E(x1271,x1272)+P13(x1273)+P13(x1274)+~P7(x1276,f22(x1273,x1273),x1273)+~E(f15(x1274,x1273,x1275,x1271,x1276,x1277),f15(x1278,x1279,x12710,x1272,x12711,x12712)) % 23.90/23.99 [128]~P4(x1287)+~P4(x1286)+~P4(x1285)+~P4(x1281)+~P12(x1287,x1284,x1283)+~P12(x1285,x1283,x1284)+~P12(x1281,x1283,x1284)+~P7(x1287,x1284,x1283)+~P7(x1285,x1283,x1284)+~P7(x1281,x1283,x1284)+E(x1281,x1282)+P13(x1283)+P13(x1284)+~P7(x1286,f22(x1283,x1283),x1283)+~E(f15(x1284,x1283,x1281,x1285,x1286,x1287),f15(x1288,x1289,x1282,x12810,x12811,x12812)) % 23.90/23.99 [129]P13(x1291)+~P4(x1297)+~P4(x1296)+~P4(x1295)+~P4(x1294)+~P12(x1297,x1293,x1291)+~P12(x1295,x1291,x1293)+~P12(x1294,x1291,x1293)+~P7(x1297,x1293,x1291)+~P7(x1295,x1291,x1293)+~P7(x1294,x1291,x1293)+E(x1291,x1292)+P13(x1293)+~P7(x1296,f22(x1291,x1291),x1291)+~E(f15(x1293,x1291,x1294,x1295,x1296,x1297),f15(x1298,x1292,x1299,x12910,x12911,x12912)) % 23.90/23.99 [130]P13(x1301)+~P4(x1307)+~P4(x1306)+~P4(x1305)+~P4(x1304)+~P12(x1307,x1301,x1303)+~P12(x1305,x1303,x1301)+~P12(x1304,x1303,x1301)+~P7(x1307,x1301,x1303)+~P7(x1305,x1303,x1301)+~P7(x1304,x1303,x1301)+E(x1301,x1302)+P13(x1303)+~P7(x1306,f22(x1303,x1303),x1303)+~E(f15(x1301,x1303,x1304,x1305,x1306,x1307),f15(x1302,x1308,x1309,x13010,x13011,x13012)) % 23.90/23.99 %EqnAxiom % 23.90/23.99 [1]E(x11,x11) % 23.90/23.99 [2]E(x22,x21)+~E(x21,x22) % 23.90/23.99 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 23.90/23.99 [4]~E(x41,x42)+E(f17(x41),f17(x42)) % 23.90/23.99 [5]~E(x51,x52)+E(f13(x51),f13(x52)) % 23.90/23.99 [6]~E(x61,x62)+E(f10(x61,x63),f10(x62,x63)) % 23.90/23.99 [7]~E(x71,x72)+E(f10(x73,x71),f10(x73,x72)) % 23.90/23.99 [8]~E(x81,x82)+E(f11(x81,x83),f11(x82,x83)) % 23.90/23.99 [9]~E(x91,x92)+E(f11(x93,x91),f11(x93,x92)) % 23.90/23.99 [10]~E(x101,x102)+E(f18(x101,x103),f18(x102,x103)) % 23.90/23.99 [11]~E(x111,x112)+E(f18(x113,x111),f18(x113,x112)) % 23.90/23.99 [12]~E(x121,x122)+E(f19(x121),f19(x122)) % 23.90/23.99 [13]~E(x131,x132)+E(f14(x131),f14(x132)) % 23.90/23.99 [14]~E(x141,x142)+E(f15(x141,x143,x144,x145,x146,x147),f15(x142,x143,x144,x145,x146,x147)) % 23.90/23.99 [15]~E(x151,x152)+E(f15(x153,x151,x154,x155,x156,x157),f15(x153,x152,x154,x155,x156,x157)) % 23.90/23.99 [16]~E(x161,x162)+E(f15(x163,x164,x161,x165,x166,x167),f15(x163,x164,x162,x165,x166,x167)) % 23.90/23.99 [17]~E(x171,x172)+E(f15(x173,x174,x175,x171,x176,x177),f15(x173,x174,x175,x172,x176,x177)) % 23.90/23.99 [18]~E(x181,x182)+E(f15(x183,x184,x185,x186,x181,x187),f15(x183,x184,x185,x186,x182,x187)) % 23.90/23.99 [19]~E(x191,x192)+E(f15(x193,x194,x195,x196,x197,x191),f15(x193,x194,x195,x196,x197,x192)) % 23.90/23.99 [20]~E(x201,x202)+E(f22(x201,x203),f22(x202,x203)) % 23.90/23.99 [21]~E(x211,x212)+E(f22(x213,x211),f22(x213,x212)) % 23.90/23.99 [22]~E(x221,x222)+E(f23(x221),f23(x222)) % 23.90/23.99 [23]~E(x231,x232)+E(f25(x231),f25(x232)) % 23.90/23.99 [24]~E(x241,x242)+E(f26(x241),f26(x242)) % 23.90/23.99 [25]~E(x251,x252)+E(f27(x251),f27(x252)) % 23.90/23.99 [26]~E(x261,x262)+E(f21(x261),f21(x262)) % 23.90/23.99 [27]~E(x271,x272)+E(f20(x271),f20(x272)) % 23.90/23.99 [28]~E(x281,x282)+E(f24(x281),f24(x282)) % 23.90/23.99 [29]~E(x291,x292)+E(f3(x291,x293),f3(x292,x293)) % 23.90/23.99 [30]~E(x301,x302)+E(f3(x303,x301),f3(x303,x302)) % 23.90/23.99 [31]~E(x311,x312)+E(f16(x311),f16(x312)) % 23.90/23.99 [32]~P1(x321)+P1(x322)+~E(x321,x322) % 23.90/23.99 [33]~P2(x331)+P2(x332)+~E(x331,x332) % 23.90/23.99 [34]P12(x342,x343,x344)+~E(x341,x342)+~P12(x341,x343,x344) % 23.90/23.99 [35]P12(x353,x352,x354)+~E(x351,x352)+~P12(x353,x351,x354) % 23.90/23.99 [36]P12(x363,x364,x362)+~E(x361,x362)+~P12(x363,x364,x361) % 23.90/23.99 [37]~P3(x371)+P3(x372)+~E(x371,x372) % 23.90/23.99 [38]P7(x382,x383,x384)+~E(x381,x382)+~P7(x381,x383,x384) % 23.90/23.99 [39]P7(x393,x392,x394)+~E(x391,x392)+~P7(x393,x391,x394) % 23.90/23.99 [40]P7(x403,x404,x402)+~E(x401,x402)+~P7(x403,x404,x401) % 23.90/23.99 [41]~P13(x411)+P13(x412)+~E(x411,x412) % 23.90/23.99 [42]~P4(x421)+P4(x422)+~E(x421,x422) % 23.90/23.99 [43]P9(x432,x433,x434)+~E(x431,x432)+~P9(x431,x433,x434) % 23.90/23.99 [44]P9(x443,x442,x444)+~E(x441,x442)+~P9(x443,x441,x444) % 23.90/23.99 [45]P9(x453,x454,x452)+~E(x451,x452)+~P9(x453,x454,x451) % 23.90/23.99 [46]P8(x462,x463,x464)+~E(x461,x462)+~P8(x461,x463,x464) % 23.90/23.99 [47]P8(x473,x472,x474)+~E(x471,x472)+~P8(x473,x471,x474) % 23.90/23.99 [48]P8(x483,x484,x482)+~E(x481,x482)+~P8(x483,x484,x481) % 23.90/23.99 [49]~P14(x491)+P14(x492)+~E(x491,x492) % 23.90/23.99 [50]~P10(x501)+P10(x502)+~E(x501,x502) % 23.90/23.99 [51]P6(x512,x513)+~E(x511,x512)+~P6(x511,x513) % 23.90/23.99 [52]P6(x523,x522)+~E(x521,x522)+~P6(x523,x521) % 23.90/23.99 [53]P5(x532,x533)+~E(x531,x532)+~P5(x531,x533) % 23.90/23.99 [54]P5(x543,x542)+~E(x541,x542)+~P5(x543,x541) % 23.90/23.99 [55]P11(x552,x553)+~E(x551,x552)+~P11(x551,x553) % 23.90/23.99 [56]P11(x563,x562)+~E(x561,x562)+~P11(x563,x561) % 23.90/23.99 % 23.90/23.99 %------------------------------------------- % 23.90/23.99 cnf(140,plain, % 23.90/23.99 (P6(f13(x1401),x1401)), % 23.90/23.99 inference(rename_variables,[],[72])). % 23.90/23.99 cnf(142,plain, % 23.90/23.99 (P11(f13(a4),a4)), % 23.90/23.99 inference(scs_inference,[],[72,140,67,75,94,100,97])). % 23.90/23.99 cnf(185,plain, % 23.90/23.99 (~P11(x1851,a9)), % 23.90/23.99 inference(scs_inference,[],[68,94])). % 23.90/23.99 cnf(233,plain, % 23.90/23.99 (~E(f14(f16(a1)),f19(a1))+P13(f16(a1))), % 23.90/23.99 inference(scs_inference,[],[57,71,76,58,142,70,185,56,119,43,44,45])). % 23.90/23.99 cnf(3636,plain, % 23.90/23.99 (~E(f19(a1),f14(f16(a1)))+P13(f16(a1))), % 23.90/23.99 inference(scs_inference,[],[233,2])). % 23.90/23.99 cnf(4654,plain, % 23.90/23.99 (P13(f16(a1))), % 23.90/23.99 inference(scs_inference,[],[58,57,3636,93])). % 23.90/23.99 cnf(4657,plain, % 23.90/23.99 ($false), % 23.90/23.99 inference(scs_inference,[],[58,57,4654,94,95]), % 23.90/23.99 ['proof']). % 23.90/24.00 % SZS output end Proof % 23.90/24.00 % Total time :23.350000s %------------------------------------------------------------------------------